Merge branch 'master' of github.com:FStarLang/FStar

src/tests/pars.fs

@@ -123,7 +123,8 @@ let pars s =
 let tc s =
     let tm = pars s in
     let _, tcenv = init() in
-    let tm, _, _ = TcTerm.type_of_tot_term tcenv tm in
+    let tcenv = {tcenv with top_level=false} in
+    let tm, _, _ = TcTerm.tc_tot_or_gtot_term tcenv tm in
     tm
 
 let pars_and_tc_fragment (s:string) =

src/tests/test.fs

@@ -14,8 +14,8 @@ let main argv =
     try
         Pars.init() |> ignore;
         FStar.Tests.Tactics.test();
-//        Norm.run_all ();
-//        Unif.run_all ();
+        Norm.run_all ();
+        Unif.run_all ();
         0
     with Error(msg, r) when not <| Options.trace_error()->
          if r = Range.dummyRange

src/tests/unif.fs

@@ -20,9 +20,6 @@ open FStar.Ident
 open FStar.Range
 open FStar.Tests.Util
 
-let x = S.gen_bv "x" None S.tun |> S.bv_to_name
-let y = S.gen_bv "y" None S.tun |> S.bv_to_name
-
 let tcenv () = Pars.init() |> snd
 
 let guard_to_string g = match g with
@@ -45,12 +42,13 @@ let guard_eq i g g' =
                         Got guard      %s\n" i (guard_to_string g') (guard_to_string g) in
     raise (Error(msg, Range.dummyRange))
 
-let unify i x y g' =
+let unify i x y g' check =
     printfn "%d ..." i;
     FStar.Main.process_args () |> ignore; //set options
     printfn "Unify %s\nand %s\n" (FStar.Syntax.Print.term_to_string x) (FStar.Syntax.Print.term_to_string y);
     let g = Rel.teq (tcenv()) x y |> Rel.solve_deferred_constraints (tcenv()) in
     guard_eq i g.guard_f g';
+    check();
     Options.init()    //reset them; exceptions are fatal, so don't worry about resetting them in case guard_eq fails
 
 let should_fail x y =
@@ -80,10 +78,13 @@ let inst n tm =
 
 let run_all () =
     Printf.printf "Testing the unifier\n";
-    let id  = pars "fun x -> x" in
-    let id' = pars "fun y -> y" in
 
     Options.__set_unit_tests();
+    let unify_check n x y g f = unify n x y g f in
+    let unify n x y g = unify n x y g (fun () -> ()) in
+    let int_t = tc "Prims.int" in
+    let x = S.gen_bv "x" None int_t |> S.bv_to_name in
+    let y = S.gen_bv "y" None int_t |> S.bv_to_name in
 
     //syntactic equality of names
     unify 0 x x Trivial;
@@ -92,22 +93,27 @@ let run_all () =
     unify 1 x y (NonTrivial (U.mk_eq2 U_zero U.t_bool x y));
 
     //equal after some reduction
+    let id = tc "fun x -> x" in
     unify 2 x (app id [x]) Trivial;
 
     //physical equality of terms
+    let id = tc "fun x -> x" in
     unify 3 id id Trivial;
 
     //alpha equivalence
+    let id = tc "fun x -> x" in
+    let id' = tc "fun y -> y" in
     unify 4 id id' Trivial; //(NonTrivial (pars "True /\ (forall x. True)"));
 
     //alpha equivalence 2
-    unify 5 (pars "fun x y -> x")
-            (pars "fun a b -> a")
+
+    unify 5 (tc "fun x y -> x")
+            (tc "fun a b -> a")
             Trivial;
 
     //alpha equivalence 3
-    unify 6 (pars "fun x y z -> y")
-            (pars "fun a b c -> b")
+    unify 6 (tc "fun x y z -> y")
+            (tc "fun a b c -> b")
             Trivial;
 
     //logical equality of distinct lambdas (questionable ... would only work for unit, or inconsistent context)
@@ -116,35 +122,36 @@ let run_all () =
             (NonTrivial (tc "(forall (x:int). (forall (y:int). y==x))"));
 
     //logical equality of distinct lambdas (questionable ... would only work for unit, or inconsistent context)
-    unify 8 (pars "fun (x:int) (y:int) (z:int) -> y")
-            (pars "fun (x:int) (y:int) (z:int) -> z")
+    unify 8 (tc "fun (x:int) (y:int) (z:int) -> y")
+            (tc "fun (x:int) (y:int) (z:int) -> z")
             (NonTrivial (tc "(forall (x:int). (forall (y:int). (forall (z:int). y==z)))"));
 
     //imitation: unifies u to a constant
-    let tm, us = inst 1 (pars "fun u x -> u x") in
-    unify 9 tm
-            (pars "fun x -> tuple2 x x")
-            Trivial;
-
-    always 9 (term_eq (norm (List.hd us))
-                    (norm (pars "fun x -> tuple2 x x")));
+    let tm, us = inst 1 (tc "fun u x -> u x") in
+    let sol = tc "fun x -> c_and x x" in
+    unify_check 9 tm
+            sol
+            Trivial
+            (fun () ->
+                always 9 (term_eq (norm (List.hd us))
+                                  (norm sol)));
 
     //imitation: unifies u to a lambda
-    let tm, us = inst 1 (pars "fun u x -> u x") in
-    unify 10 tm
-            (pars "fun x y -> x + y")
-            Trivial;
-    always 10 (term_eq (norm (List.hd us))
-                    (norm (pars "fun x y -> x + y")));
-
+    let tm, us = inst 1 (tc "fun u x -> u x") in
+    let sol = tc "fun x y -> x + y" in
+    unify_check 10 tm
+            sol
+            Trivial
+            (fun () ->always 10 (term_eq (norm (List.hd us))
+                                (norm sol)));
 
     let tm1 = tc ("x:int -> y:int{eq2 y x} -> bool") in
     let tm2 = tc ("x:int -> y:int -> bool") in
     unify 11 tm1 tm2
             (NonTrivial (tc "forall (x:int). (forall (y:int). y==x <==> True)"));
 
-    let tm1 = pars ("a:Type0 -> b:(a -> Type0) -> x:a -> y:b x -> Tot Type0") in
-    let tm2 = pars ("a:Type0 -> b:(a -> Type0) -> x:a -> y:b x -> Tot Type0") in
+    let tm1 = tc ("a:Type0 -> b:(a -> Type0) -> x:a -> y:b x -> Tot Type0") in
+    let tm2 = tc ("a:Type0 -> b:(a -> Type0) -> x:a -> y:b x -> Tot Type0") in
     unify 12 tm1 tm2
             Trivial;