Add some tests

examples/typeclasses/Add.fst

@@ -62,3 +62,4 @@ let _ = assert (plus 1 2 = 3)
 let _ = assert (plus false false = false)
 let _ = assert (plus true false = true)
 let _ = assert (plus [1] [2] = [1;2])
+let test #a (x y : a) = assert (plus [x] [y] == [x;y])

tests/micro-benchmarks/StrictArgsUnfoldTest1.fst

@@ -0,0 +1,30 @@
+module StrictArgsUnfoldTest1
+
+noeq
+type ordered (a:eqtype) =
+{
+  leq : a -> a -> bool;
+}
+
+[@@strict_on_arguments_unfold [1]]
+let leq #a (d : ordered a) : a -> a -> bool = d.leq
+
+let transitivity #a (d : ordered a) (x y z: a):
+  Lemma (requires leq d x y /\ leq d y z)
+  (ensures leq d x z)
+= admit() // p.properties
+
+let rec lower_bounded #a (d : ordered a) (l: list a) m: GTot bool =
+  match l with
+  | [] -> true
+  | t::q -> leq d m t && lower_bounded d q m
+
+(* Used to fail with:
+      Failure("Impossible: locally nameless; got t#6")
+*)
+let rec lower_bounded_trans #a (d : ordered a) (l: list a) m1 m2:
+  Lemma (requires lower_bounded d l m1 /\ leq d m2 m1)
+        (ensures lower_bounded d l m2)
+= match l with
+  | [] -> ()
+  | t::q -> (transitivity d m2 m1 t; lower_bounded_trans d q m1 m2)

tests/micro-benchmarks/TCUnivs.fst

@@ -0,0 +1,79 @@
+module TCUnivs
+
+(* This caused a very hard to find failure in the normalizer due to
+pushing un-evaluated universe arguments on the stack. It is a
+shrunk down version of TypeclassesAlt3 from the book, but I'm keeping
+a copy here just in case. -- Guido 2023/11/03 *)
+
+module TC = FStar.Tactics.Typeclasses
+
+class bounded_unsigned_int (a:Type) = {
+   bound      : a;
+   as_nat     : a -> nat;
+   from_nat   : (x:nat { x <= as_nat bound }) -> a;
+}
+
+let fits #a {| bounded_unsigned_int a |}
+            (op: int -> int -> int)
+            (x y:a)
+  : prop
+  = 0 <= op (as_nat x) (as_nat y) /\
+    op (as_nat x) (as_nat y) <= as_nat #a bound
+
+let related_ops #a {| bounded_unsigned_int a |}
+                (iop: int -> int -> int)
+                (bop: (x:a -> y:a { fits iop x y } -> a))
+  = forall (x y:a).  fits iop x y ==> as_nat (bop x y) = as_nat x `iop` as_nat y
+
+class bounded_unsigned_int_ops (a:Type) = {
+   base       : bounded_unsigned_int a;
+   add        : (x:a -> y:a { fits ( + ) x y } -> a);
+   sub        : (x:a -> y:a { fits op_Subtraction x y } -> a);
+   lt         : (a -> a -> bool);
+}
+
+instance ops_base #a {| d : bounded_unsigned_int_ops a |}
+  : bounded_unsigned_int a
+  = d.base
+
+let ( <=^ ) #a {| bounded_unsigned_int_ops a |} (x y : a)
+  : bool
+  = true
+
+module U32 = FStar.UInt32
+instance u32_instance_base : bounded_unsigned_int U32.t =
+  let open U32 in
+  {
+    bound    = 0xfffffffful;
+    as_nat   = v;
+    from_nat = uint_to_t;
+}
+
+instance u32_instance_ops : bounded_unsigned_int_ops U32.t =
+  let open U32 in
+  {
+    base = u32_instance_base;
+    add  = (fun x y -> add x y);
+    sub  = (fun x y -> sub x y);
+    lt   = (fun x y -> lt x y);
+  }
+
+module L = FStar.List.Tot
+let sum #a (d : bounded_unsigned_int_ops a )
+        (l:list a) (acc:a)
+  : option a
+  = admit();
+    L.fold_right
+     (fun (x:a) (acc:option a) ->
+       match acc with
+       | None -> None
+       | Some y ->
+         if x <=^ bound `sub` y
+         then Some (x `add` y)
+         else None)
+     l
+     (Some acc)
+
+let testsum32' : unit =
+  let x = sum #U32.t u32_instance_ops [0x1ul] 0x00ul in
+  assert_norm (Some? x)

tests/micro-benchmarks/Test.Integers.fst

@@ -173,3 +173,10 @@ let g5 = f1 ()
 /// problem instance, we commit to it immediately even if the chosen
 /// solution is incompatible with other problems that may be in scope;
 /// global backtracking is too expensive and unpredictable.
+
+(* A test to check that we can prove that FStar.Integers.int
+is equal to Prims.int with just the unifier. *)
+#push-options "--no_smt"
+let mk_option_int () : option int
+  = (); Some #int 5
+#pop-options

tests/micro-benchmarks/UnifyStrictArgs.fst

@@ -0,0 +1,26 @@
+module UnifyStrictArgs
+
+open FStar.Tactics
+
+type t (k:int) = | Mk of (x:int{x > k})
+
+[@@strict_on_arguments [1]]
+let f1 k (x:t k) : int = match x with | Mk n -> n
+
+let f2 k (x:t k) : int = match x with | Mk n -> n
+
+[@@strict_on_arguments [1]; tcnorm]
+let f3 k (x:t k) : int = match x with | Mk n -> n
+
+[@@strict_on_arguments_unfold [1]; tcnorm]
+let f4 k (x:t k) : int = match x with | Mk n -> n
+
+let _ = assert True by begin
+  if not (unify (`f1 _) (`f2 42)) then fail "1";
+  if not (unify (`f1 _) (`f3 42)) then fail "2";
+  if not (unify (`f1 _) (`f4 42)) then fail "3";
+  if not (unify (`f2 _) (`f3 42)) then fail "4";
+  if not (unify (`f2 _) (`f4 42)) then fail "5";
+  if not (unify (`f3 _) (`f4 42)) then fail "6";
+  ()
+end