Merge pull request #3091 from mtzguido/3089

Fixing #3089, and some unifier fixes

examples/miniparse/MiniParse.Impl.List.fst

@@ -325,6 +325,7 @@ let serialize_nlist_impl_inv
     ser == Seq.append (B.as_seq h bl) (serialize (serialize_nlist (n - i) s) ll)
   ))
 
+#push-options "--z3rlimit 128"
 inline_for_extraction
 let serialize_nlist_impl_body
   (n: nat)
@@ -376,6 +377,7 @@ let serialize_nlist_impl_body
     in
     phi ();
     false
+#pop-options
 
 inline_for_extraction
 let serialize_nlist_impl

examples/tactics/Canon.fst

@@ -19,11 +19,6 @@ open FStar.Tactics.V2
 open FStar.Tactics.Canon
 open FStar.Mul
 
-assume val w : int
-assume val x : int
-assume val y : int
-assume val z : int
-
 // Testing the canonicalizer, it should be the only thing needed for this file
 let check_canon () =
     canon ();
@@ -32,11 +27,25 @@ let check_canon () =
             (fun () -> dump "`canon` left the following goals";
                        fail "")
 
-let lem0 =  assert (x * (y * z) == (x * y) * z) by check_canon ()
-let lem0' = assert (w * (x * (y * z)) == ((z * y) * x) * w) by check_canon ()
+let test_neg (b : pos) =
+    assert (b - 1 == b + (-1))
+        by (check_canon ())
 
 // TODO: for now, canon is not enough as we don't collect factors, so we
 // leave the rest to the SMT
+let test_neg2 (b c : pos) =
+    assert (b * (c-1) + b == b*c)
+        by (canon ())
+
+assume val w : int
+assume val x : int
+assume val y : int
+assume val z : int
+
+let lem0 =  assert (x * (y * z) == (x * y) * z) by check_canon ()
+let lem0' = assert (w * (x * (y * z)) == ((z * y) * x) * w) by check_canon ()
+
+// Idem test_neg2
 let lem1 =
     assert ((x + y) * (z + z) == 2 * z * (y + x))
         by canon ()

examples/tactics/Normalization.fst

@@ -62,15 +62,19 @@ let _ = assert True
                 then ()
                 else fail "Test 1")
 
+(* GM, 2023/11/09: this is now no longer true. The unifier does trigger
+primitive steps computations, and the trefl() call above
+will instantiate the RHS with the WHNF of the LHS, which is also 4. *)
+
 (* If we only allow for Delta steps, then there's no primitive computation and we
  * end up with (2 + 1) + 1 *)
-let four' : int = _ by (normalize [delta] (add_2 2))
+(* let four' : int = _ by (normalize [delta] (add_2 2)) *)
 
-let _ = assert True
-            by (let t = def_of four' in
-                if compare_term t (`((2 + 1) + 1)) = FStar.Order.Eq
-                then ()
-                else fail "Test 2")
+(* let _ = assert True *)
+(*             by (let t = def_of four' in *)
+(*                 if compare_term t (`((2 + 1) + 1)) = FStar.Order.Eq *)
+(*                 then () *)
+(*                 else fail "Test 2") *)
 
 (* Here, we allow for primitive computation but don't allow for `add_2` to be expanded to
  * its definition, so the final result is `add_2 1` *)