adding regression tests for FStarLang#1206 FStarLang#1271 and FStarLa…

…ng#1305

examples/bug-reports/Makefile

@@ -29,7 +29,7 @@ SHOULD_VERIFY_CLOSED=bug022.fst bug024.fst bug025.fst bug026.fst bug026b.fst bug
   bug710.fst bug712.fst bug713.fst bug736.fst bug765.fst bug769c.fst bug836.fst bug844.fst bug989.fst\
   BugWildcardTelescopes.fst NormalizingGhostSubterms.fst UnificationCrash.fst bug1150.fst bug1076.fst\
   bug1121.fst bug1341.fst bug1345.fst bug1346.fst bug1348.fst bug1362.fst bug1291.fst \
-  bug1287.fst bug1347.fst bug1347b.fst
+  bug1287.fst bug1347.fst bug1347b.fst bug1206.fst bug1271.fst bug1305.fst
 SHOULD_VERIFY_INTERFACE_CLOSED=bug771.fsti bug771b.fsti
 SHOULD_VERIFY_AND_WARN_CLOSED=bug016.fst
 

examples/bug-reports/bug1206.fst

@@ -0,0 +1,29 @@
+module Bug1206
+
+open FStar.Tactics
+open FStar.HyperStack.ST
+
+#reset-options "--max_fuel 1 --max_ifuel 1"
+
+type bslice =
+| BSlice : len:nat -> bslice
+
+let serializer_ty  = buf:bslice -> Stack (option (off:nat{off <= buf.len}))
+  (requires (fun h0 -> True))
+  (ensures (fun h0 r h1 -> True))
+
+let ser_id (s1: serializer_ty) : serializer_ty =
+  fun buf -> match s1 buf with
+  | Some off -> Some off
+  | None -> None
+
+assume val ser : serializer_ty
+
+let normalize (#t:Type) (x:t) : tactic unit =
+  dup;;
+  exact (quote x);;
+  norm [delta];;
+  trefl
+
+let ser' : serializer_ty =
+  synth_by_tactic (normalize (ser_id ser))

examples/bug-reports/bug1271.fst

@@ -0,0 +1,14 @@
+module Bug1271
+
+open FStar.Tactics
+
+let test =
+  assert_by_tactic (True ==> True)
+    (b <-- implies_intro;
+     qb <-- quote b;
+     qf <-- quote (fun (b: binder) -> print "f"); // f: tactic unit
+     let q_fofb = mk_app qf [(qb, Q_Explicit)] in
+     print ("::: " ^ term_to_string q_fofb);;
+     tac <-- unquote #(tactic unit) q_fofb;
+     tac;;
+     trivial)

examples/bug-reports/bug1305.fst

@@ -0,0 +1,10 @@
+module Bug1305
+
+open FStar.Tactics
+
+let _ =
+  assert_by_tactic True
+                   (fun () ->
+                     admit ();
+                     let x = quote 1 () in
+                     ())