diff --git a/ocaml/fstar-lib/generated/FStar_Tactics.ml b/ocaml/fstar-lib/generated/FStar_Tactics.ml deleted file mode 100644 index e8306abedb2..00000000000 --- a/ocaml/fstar-lib/generated/FStar_Tactics.ml +++ /dev/null @@ -1 +0,0 @@ -open Prims \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_BV.ml b/ocaml/fstar-lib/generated/FStar_Tactics_BV.ml index 18ed09f1192..d053282bccc 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_BV.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_BV.ml @@ -17,12 +17,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (30)) (Prims.of_int (8)) (Prims.of_int (30)) + (Prims.of_int (31)) (Prims.of_int (8)) (Prims.of_int (31)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (31)) (Prims.of_int (8)) (Prims.of_int (32)) + (Prims.of_int (32)) (Prims.of_int (8)) (Prims.of_int (33)) (Prims.of_int (27))))) (Obj.magic uu___1) (fun uu___2 -> (fun uu___2 -> @@ -41,13 +41,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (31)) (Prims.of_int (8)) - (Prims.of_int (31)) (Prims.of_int (33))))) + (Prims.of_int (32)) (Prims.of_int (8)) + (Prims.of_int (32)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (32)) (Prims.of_int (8)) - (Prims.of_int (32)) (Prims.of_int (27))))) + (Prims.of_int (33)) (Prims.of_int (8)) + (Prims.of_int (33)) (Prims.of_int (27))))) (Obj.magic uu___3) (fun uu___4 -> (fun uu___4 -> Obj.magic (arith_expr_to_bv e1)) @@ -63,12 +63,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (30)) (Prims.of_int (8)) (Prims.of_int (30)) + (Prims.of_int (31)) (Prims.of_int (8)) (Prims.of_int (31)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (31)) (Prims.of_int (8)) (Prims.of_int (32)) + (Prims.of_int (32)) (Prims.of_int (8)) (Prims.of_int (33)) (Prims.of_int (27))))) (Obj.magic uu___1) (fun uu___2 -> (fun uu___2 -> @@ -87,13 +87,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (31)) (Prims.of_int (8)) - (Prims.of_int (31)) (Prims.of_int (33))))) + (Prims.of_int (32)) (Prims.of_int (8)) + (Prims.of_int (32)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (32)) (Prims.of_int (8)) - (Prims.of_int (32)) (Prims.of_int (27))))) + (Prims.of_int (33)) (Prims.of_int (8)) + (Prims.of_int (33)) (Prims.of_int (27))))) (Obj.magic uu___3) (fun uu___4 -> (fun uu___4 -> Obj.magic (arith_expr_to_bv e1)) @@ -110,12 +110,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (34)) (Prims.of_int (8)) (Prims.of_int (34)) + (Prims.of_int (35)) (Prims.of_int (8)) (Prims.of_int (35)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (35)) (Prims.of_int (8)) (Prims.of_int (36)) + (Prims.of_int (36)) (Prims.of_int (8)) (Prims.of_int (37)) (Prims.of_int (27))))) (Obj.magic uu___1) (fun uu___2 -> (fun uu___2 -> @@ -134,13 +134,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (35)) (Prims.of_int (8)) - (Prims.of_int (35)) (Prims.of_int (33))))) + (Prims.of_int (36)) (Prims.of_int (8)) + (Prims.of_int (36)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (36)) (Prims.of_int (8)) - (Prims.of_int (36)) (Prims.of_int (27))))) + (Prims.of_int (37)) (Prims.of_int (8)) + (Prims.of_int (37)) (Prims.of_int (27))))) (Obj.magic uu___3) (fun uu___4 -> (fun uu___4 -> Obj.magic (arith_expr_to_bv e1)) @@ -156,12 +156,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (34)) (Prims.of_int (8)) (Prims.of_int (34)) + (Prims.of_int (35)) (Prims.of_int (8)) (Prims.of_int (35)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (35)) (Prims.of_int (8)) (Prims.of_int (36)) + (Prims.of_int (36)) (Prims.of_int (8)) (Prims.of_int (37)) (Prims.of_int (27))))) (Obj.magic uu___1) (fun uu___2 -> (fun uu___2 -> @@ -180,13 +180,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (35)) (Prims.of_int (8)) - (Prims.of_int (35)) (Prims.of_int (33))))) + (Prims.of_int (36)) (Prims.of_int (8)) + (Prims.of_int (36)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (36)) (Prims.of_int (8)) - (Prims.of_int (36)) (Prims.of_int (27))))) + (Prims.of_int (37)) (Prims.of_int (8)) + (Prims.of_int (37)) (Prims.of_int (27))))) (Obj.magic uu___3) (fun uu___4 -> (fun uu___4 -> Obj.magic (arith_expr_to_bv e1)) @@ -203,12 +203,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (38)) (Prims.of_int (8)) (Prims.of_int (38)) + (Prims.of_int (39)) (Prims.of_int (8)) (Prims.of_int (39)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (39)) (Prims.of_int (8)) (Prims.of_int (40)) + (Prims.of_int (40)) (Prims.of_int (8)) (Prims.of_int (41)) (Prims.of_int (27))))) (Obj.magic uu___1) (fun uu___2 -> (fun uu___2 -> @@ -227,13 +227,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (39)) (Prims.of_int (8)) - (Prims.of_int (39)) (Prims.of_int (33))))) + (Prims.of_int (40)) (Prims.of_int (8)) + (Prims.of_int (40)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (40)) (Prims.of_int (8)) - (Prims.of_int (40)) (Prims.of_int (27))))) + (Prims.of_int (41)) (Prims.of_int (8)) + (Prims.of_int (41)) (Prims.of_int (27))))) (Obj.magic uu___3) (fun uu___4 -> (fun uu___4 -> Obj.magic (arith_expr_to_bv e1)) @@ -249,12 +249,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (38)) (Prims.of_int (8)) (Prims.of_int (38)) + (Prims.of_int (39)) (Prims.of_int (8)) (Prims.of_int (39)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (39)) (Prims.of_int (8)) (Prims.of_int (40)) + (Prims.of_int (40)) (Prims.of_int (8)) (Prims.of_int (41)) (Prims.of_int (27))))) (Obj.magic uu___1) (fun uu___2 -> (fun uu___2 -> @@ -273,13 +273,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (39)) (Prims.of_int (8)) - (Prims.of_int (39)) (Prims.of_int (33))))) + (Prims.of_int (40)) (Prims.of_int (8)) + (Prims.of_int (40)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (40)) (Prims.of_int (8)) - (Prims.of_int (40)) (Prims.of_int (27))))) + (Prims.of_int (41)) (Prims.of_int (8)) + (Prims.of_int (41)) (Prims.of_int (27))))) (Obj.magic uu___3) (fun uu___4 -> (fun uu___4 -> Obj.magic (arith_expr_to_bv e1)) @@ -296,12 +296,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (42)) (Prims.of_int (8)) (Prims.of_int (42)) + (Prims.of_int (43)) (Prims.of_int (8)) (Prims.of_int (43)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (43)) (Prims.of_int (8)) (Prims.of_int (44)) + (Prims.of_int (44)) (Prims.of_int (8)) (Prims.of_int (45)) (Prims.of_int (27))))) (Obj.magic uu___1) (fun uu___2 -> (fun uu___2 -> @@ -320,13 +320,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (43)) (Prims.of_int (8)) - (Prims.of_int (43)) (Prims.of_int (33))))) + (Prims.of_int (44)) (Prims.of_int (8)) + (Prims.of_int (44)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (44)) (Prims.of_int (8)) - (Prims.of_int (44)) (Prims.of_int (27))))) + (Prims.of_int (45)) (Prims.of_int (8)) + (Prims.of_int (45)) (Prims.of_int (27))))) (Obj.magic uu___3) (fun uu___4 -> (fun uu___4 -> Obj.magic (arith_expr_to_bv e1)) @@ -342,12 +342,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (42)) (Prims.of_int (8)) (Prims.of_int (42)) + (Prims.of_int (43)) (Prims.of_int (8)) (Prims.of_int (43)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (43)) (Prims.of_int (8)) (Prims.of_int (44)) + (Prims.of_int (44)) (Prims.of_int (8)) (Prims.of_int (45)) (Prims.of_int (27))))) (Obj.magic uu___1) (fun uu___2 -> (fun uu___2 -> @@ -366,13 +366,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (43)) (Prims.of_int (8)) - (Prims.of_int (43)) (Prims.of_int (33))))) + (Prims.of_int (44)) (Prims.of_int (8)) + (Prims.of_int (44)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (44)) (Prims.of_int (8)) - (Prims.of_int (44)) (Prims.of_int (27))))) + (Prims.of_int (45)) (Prims.of_int (8)) + (Prims.of_int (45)) (Prims.of_int (27))))) (Obj.magic uu___3) (fun uu___4 -> (fun uu___4 -> Obj.magic (arith_expr_to_bv e1)) @@ -389,12 +389,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (46)) (Prims.of_int (8)) (Prims.of_int (46)) + (Prims.of_int (47)) (Prims.of_int (8)) (Prims.of_int (47)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (47)) (Prims.of_int (8)) (Prims.of_int (48)) + (Prims.of_int (48)) (Prims.of_int (8)) (Prims.of_int (49)) (Prims.of_int (27))))) (Obj.magic uu___1) (fun uu___2 -> (fun uu___2 -> @@ -413,13 +413,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (47)) (Prims.of_int (8)) - (Prims.of_int (47)) (Prims.of_int (33))))) + (Prims.of_int (48)) (Prims.of_int (8)) + (Prims.of_int (48)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (48)) (Prims.of_int (8)) - (Prims.of_int (48)) (Prims.of_int (27))))) + (Prims.of_int (49)) (Prims.of_int (8)) + (Prims.of_int (49)) (Prims.of_int (27))))) (Obj.magic uu___3) (fun uu___4 -> (fun uu___4 -> Obj.magic (arith_expr_to_bv e1)) @@ -435,12 +435,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (46)) (Prims.of_int (8)) (Prims.of_int (46)) + (Prims.of_int (47)) (Prims.of_int (8)) (Prims.of_int (47)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (47)) (Prims.of_int (8)) (Prims.of_int (48)) + (Prims.of_int (48)) (Prims.of_int (8)) (Prims.of_int (49)) (Prims.of_int (27))))) (Obj.magic uu___1) (fun uu___2 -> (fun uu___2 -> @@ -459,13 +459,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (47)) (Prims.of_int (8)) - (Prims.of_int (47)) (Prims.of_int (33))))) + (Prims.of_int (48)) (Prims.of_int (8)) + (Prims.of_int (48)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (48)) (Prims.of_int (8)) - (Prims.of_int (48)) (Prims.of_int (27))))) + (Prims.of_int (49)) (Prims.of_int (8)) + (Prims.of_int (49)) (Prims.of_int (27))))) (Obj.magic uu___3) (fun uu___4 -> (fun uu___4 -> Obj.magic (arith_expr_to_bv e1)) @@ -482,12 +482,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (50)) (Prims.of_int (8)) (Prims.of_int (50)) + (Prims.of_int (51)) (Prims.of_int (8)) (Prims.of_int (51)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (51)) (Prims.of_int (8)) (Prims.of_int (53)) + (Prims.of_int (52)) (Prims.of_int (8)) (Prims.of_int (54)) (Prims.of_int (27))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -506,13 +506,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (51)) (Prims.of_int (8)) - (Prims.of_int (51)) (Prims.of_int (33))))) + (Prims.of_int (52)) (Prims.of_int (8)) + (Prims.of_int (52)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (52)) (Prims.of_int (8)) - (Prims.of_int (53)) (Prims.of_int (27))))) + (Prims.of_int (53)) (Prims.of_int (8)) + (Prims.of_int (54)) (Prims.of_int (27))))) (Obj.magic uu___2) (fun uu___3 -> (fun uu___3 -> @@ -523,17 +523,17 @@ let rec (arith_expr_to_bv : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (52)) + (Prims.of_int (53)) (Prims.of_int (8)) - (Prims.of_int (52)) + (Prims.of_int (53)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (53)) + (Prims.of_int (54)) (Prims.of_int (8)) - (Prims.of_int (53)) + (Prims.of_int (54)) (Prims.of_int (27))))) (Obj.magic uu___4) (fun uu___5 -> @@ -551,12 +551,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (50)) (Prims.of_int (8)) (Prims.of_int (50)) + (Prims.of_int (51)) (Prims.of_int (8)) (Prims.of_int (51)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (51)) (Prims.of_int (8)) (Prims.of_int (53)) + (Prims.of_int (52)) (Prims.of_int (8)) (Prims.of_int (54)) (Prims.of_int (27))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -575,13 +575,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (51)) (Prims.of_int (8)) - (Prims.of_int (51)) (Prims.of_int (33))))) + (Prims.of_int (52)) (Prims.of_int (8)) + (Prims.of_int (52)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (52)) (Prims.of_int (8)) - (Prims.of_int (53)) (Prims.of_int (27))))) + (Prims.of_int (53)) (Prims.of_int (8)) + (Prims.of_int (54)) (Prims.of_int (27))))) (Obj.magic uu___2) (fun uu___3 -> (fun uu___3 -> @@ -592,17 +592,17 @@ let rec (arith_expr_to_bv : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (52)) + (Prims.of_int (53)) (Prims.of_int (8)) - (Prims.of_int (52)) + (Prims.of_int (53)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (53)) + (Prims.of_int (54)) (Prims.of_int (8)) - (Prims.of_int (53)) + (Prims.of_int (54)) (Prims.of_int (27))))) (Obj.magic uu___4) (fun uu___5 -> @@ -621,12 +621,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (55)) (Prims.of_int (8)) (Prims.of_int (55)) + (Prims.of_int (56)) (Prims.of_int (8)) (Prims.of_int (56)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (56)) (Prims.of_int (8)) (Prims.of_int (58)) + (Prims.of_int (57)) (Prims.of_int (8)) (Prims.of_int (59)) (Prims.of_int (27))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -645,13 +645,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (56)) (Prims.of_int (8)) - (Prims.of_int (56)) (Prims.of_int (33))))) + (Prims.of_int (57)) (Prims.of_int (8)) + (Prims.of_int (57)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (57)) (Prims.of_int (8)) - (Prims.of_int (58)) (Prims.of_int (27))))) + (Prims.of_int (58)) (Prims.of_int (8)) + (Prims.of_int (59)) (Prims.of_int (27))))) (Obj.magic uu___2) (fun uu___3 -> (fun uu___3 -> @@ -662,17 +662,17 @@ let rec (arith_expr_to_bv : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (57)) + (Prims.of_int (58)) (Prims.of_int (8)) - (Prims.of_int (57)) + (Prims.of_int (58)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (58)) + (Prims.of_int (59)) (Prims.of_int (8)) - (Prims.of_int (58)) + (Prims.of_int (59)) (Prims.of_int (27))))) (Obj.magic uu___4) (fun uu___5 -> @@ -690,12 +690,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (55)) (Prims.of_int (8)) (Prims.of_int (55)) + (Prims.of_int (56)) (Prims.of_int (8)) (Prims.of_int (56)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (56)) (Prims.of_int (8)) (Prims.of_int (58)) + (Prims.of_int (57)) (Prims.of_int (8)) (Prims.of_int (59)) (Prims.of_int (27))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -714,13 +714,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (56)) (Prims.of_int (8)) - (Prims.of_int (56)) (Prims.of_int (33))))) + (Prims.of_int (57)) (Prims.of_int (8)) + (Prims.of_int (57)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (57)) (Prims.of_int (8)) - (Prims.of_int (58)) (Prims.of_int (27))))) + (Prims.of_int (58)) (Prims.of_int (8)) + (Prims.of_int (59)) (Prims.of_int (27))))) (Obj.magic uu___2) (fun uu___3 -> (fun uu___3 -> @@ -731,17 +731,17 @@ let rec (arith_expr_to_bv : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (57)) + (Prims.of_int (58)) (Prims.of_int (8)) - (Prims.of_int (57)) + (Prims.of_int (58)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (58)) + (Prims.of_int (59)) (Prims.of_int (8)) - (Prims.of_int (58)) + (Prims.of_int (59)) (Prims.of_int (27))))) (Obj.magic uu___4) (fun uu___5 -> @@ -760,12 +760,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (60)) (Prims.of_int (8)) (Prims.of_int (60)) + (Prims.of_int (61)) (Prims.of_int (8)) (Prims.of_int (61)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (61)) (Prims.of_int (8)) (Prims.of_int (63)) + (Prims.of_int (62)) (Prims.of_int (8)) (Prims.of_int (64)) (Prims.of_int (27))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -784,13 +784,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (61)) (Prims.of_int (8)) - (Prims.of_int (61)) (Prims.of_int (32))))) + (Prims.of_int (62)) (Prims.of_int (8)) + (Prims.of_int (62)) (Prims.of_int (32))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (62)) (Prims.of_int (8)) - (Prims.of_int (63)) (Prims.of_int (27))))) + (Prims.of_int (63)) (Prims.of_int (8)) + (Prims.of_int (64)) (Prims.of_int (27))))) (Obj.magic uu___2) (fun uu___3 -> (fun uu___3 -> @@ -801,17 +801,17 @@ let rec (arith_expr_to_bv : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (62)) + (Prims.of_int (63)) (Prims.of_int (8)) - (Prims.of_int (62)) + (Prims.of_int (63)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (63)) + (Prims.of_int (64)) (Prims.of_int (8)) - (Prims.of_int (63)) + (Prims.of_int (64)) (Prims.of_int (27))))) (Obj.magic uu___4) (fun uu___5 -> @@ -829,12 +829,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (60)) (Prims.of_int (8)) (Prims.of_int (60)) + (Prims.of_int (61)) (Prims.of_int (8)) (Prims.of_int (61)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (61)) (Prims.of_int (8)) (Prims.of_int (63)) + (Prims.of_int (62)) (Prims.of_int (8)) (Prims.of_int (64)) (Prims.of_int (27))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -853,13 +853,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (61)) (Prims.of_int (8)) - (Prims.of_int (61)) (Prims.of_int (32))))) + (Prims.of_int (62)) (Prims.of_int (8)) + (Prims.of_int (62)) (Prims.of_int (32))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (62)) (Prims.of_int (8)) - (Prims.of_int (63)) (Prims.of_int (27))))) + (Prims.of_int (63)) (Prims.of_int (8)) + (Prims.of_int (64)) (Prims.of_int (27))))) (Obj.magic uu___2) (fun uu___3 -> (fun uu___3 -> @@ -870,17 +870,17 @@ let rec (arith_expr_to_bv : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (62)) + (Prims.of_int (63)) (Prims.of_int (8)) - (Prims.of_int (62)) + (Prims.of_int (63)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (63)) + (Prims.of_int (64)) (Prims.of_int (8)) - (Prims.of_int (63)) + (Prims.of_int (64)) (Prims.of_int (27))))) (Obj.magic uu___4) (fun uu___5 -> @@ -899,12 +899,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (65)) (Prims.of_int (8)) (Prims.of_int (65)) + (Prims.of_int (66)) (Prims.of_int (8)) (Prims.of_int (66)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (66)) (Prims.of_int (8)) (Prims.of_int (68)) + (Prims.of_int (67)) (Prims.of_int (8)) (Prims.of_int (69)) (Prims.of_int (27))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -923,13 +923,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (66)) (Prims.of_int (8)) - (Prims.of_int (66)) (Prims.of_int (33))))) + (Prims.of_int (67)) (Prims.of_int (8)) + (Prims.of_int (67)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (67)) (Prims.of_int (8)) - (Prims.of_int (68)) (Prims.of_int (27))))) + (Prims.of_int (68)) (Prims.of_int (8)) + (Prims.of_int (69)) (Prims.of_int (27))))) (Obj.magic uu___2) (fun uu___3 -> (fun uu___3 -> @@ -940,17 +940,17 @@ let rec (arith_expr_to_bv : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (67)) + (Prims.of_int (68)) (Prims.of_int (8)) - (Prims.of_int (67)) + (Prims.of_int (68)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (68)) + (Prims.of_int (69)) (Prims.of_int (8)) - (Prims.of_int (68)) + (Prims.of_int (69)) (Prims.of_int (27))))) (Obj.magic uu___4) (fun uu___5 -> @@ -968,12 +968,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (65)) (Prims.of_int (8)) (Prims.of_int (65)) + (Prims.of_int (66)) (Prims.of_int (8)) (Prims.of_int (66)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (66)) (Prims.of_int (8)) (Prims.of_int (68)) + (Prims.of_int (67)) (Prims.of_int (8)) (Prims.of_int (69)) (Prims.of_int (27))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -992,13 +992,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (66)) (Prims.of_int (8)) - (Prims.of_int (66)) (Prims.of_int (33))))) + (Prims.of_int (67)) (Prims.of_int (8)) + (Prims.of_int (67)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (67)) (Prims.of_int (8)) - (Prims.of_int (68)) (Prims.of_int (27))))) + (Prims.of_int (68)) (Prims.of_int (8)) + (Prims.of_int (69)) (Prims.of_int (27))))) (Obj.magic uu___2) (fun uu___3 -> (fun uu___3 -> @@ -1009,17 +1009,17 @@ let rec (arith_expr_to_bv : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (67)) + (Prims.of_int (68)) (Prims.of_int (8)) - (Prims.of_int (67)) + (Prims.of_int (68)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (68)) + (Prims.of_int (69)) (Prims.of_int (8)) - (Prims.of_int (68)) + (Prims.of_int (69)) (Prims.of_int (27))))) (Obj.magic uu___4) (fun uu___5 -> @@ -1038,12 +1038,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (70)) (Prims.of_int (8)) (Prims.of_int (70)) + (Prims.of_int (71)) (Prims.of_int (8)) (Prims.of_int (71)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (71)) (Prims.of_int (8)) (Prims.of_int (73)) + (Prims.of_int (72)) (Prims.of_int (8)) (Prims.of_int (74)) (Prims.of_int (27))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -1062,13 +1062,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (71)) (Prims.of_int (8)) - (Prims.of_int (71)) (Prims.of_int (33))))) + (Prims.of_int (72)) (Prims.of_int (8)) + (Prims.of_int (72)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (72)) (Prims.of_int (8)) - (Prims.of_int (73)) (Prims.of_int (27))))) + (Prims.of_int (73)) (Prims.of_int (8)) + (Prims.of_int (74)) (Prims.of_int (27))))) (Obj.magic uu___2) (fun uu___3 -> (fun uu___3 -> @@ -1079,17 +1079,17 @@ let rec (arith_expr_to_bv : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (72)) + (Prims.of_int (73)) (Prims.of_int (8)) - (Prims.of_int (72)) + (Prims.of_int (73)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (73)) + (Prims.of_int (74)) (Prims.of_int (8)) - (Prims.of_int (73)) + (Prims.of_int (74)) (Prims.of_int (27))))) (Obj.magic uu___4) (fun uu___5 -> @@ -1107,12 +1107,12 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (70)) (Prims.of_int (8)) (Prims.of_int (70)) + (Prims.of_int (71)) (Prims.of_int (8)) (Prims.of_int (71)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (71)) (Prims.of_int (8)) (Prims.of_int (73)) + (Prims.of_int (72)) (Prims.of_int (8)) (Prims.of_int (74)) (Prims.of_int (27))))) (Obj.magic uu___) (fun uu___1 -> (fun uu___1 -> @@ -1131,13 +1131,13 @@ let rec (arith_expr_to_bv : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (71)) (Prims.of_int (8)) - (Prims.of_int (71)) (Prims.of_int (33))))) + (Prims.of_int (72)) (Prims.of_int (8)) + (Prims.of_int (72)) (Prims.of_int (33))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (72)) (Prims.of_int (8)) - (Prims.of_int (73)) (Prims.of_int (27))))) + (Prims.of_int (73)) (Prims.of_int (8)) + (Prims.of_int (74)) (Prims.of_int (27))))) (Obj.magic uu___2) (fun uu___3 -> (fun uu___3 -> @@ -1148,17 +1148,17 @@ let rec (arith_expr_to_bv : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (72)) + (Prims.of_int (73)) (Prims.of_int (8)) - (Prims.of_int (72)) + (Prims.of_int (73)) (Prims.of_int (27))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (73)) + (Prims.of_int (74)) (Prims.of_int (8)) - (Prims.of_int (73)) + (Prims.of_int (74)) (Prims.of_int (27))))) (Obj.magic uu___4) (fun uu___5 -> @@ -1177,13 +1177,13 @@ let (arith_to_bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (78)) (Prims.of_int (4)) - (Prims.of_int (78)) (Prims.of_int (40))))) + (Prims.of_int (79)) (Prims.of_int (4)) + (Prims.of_int (79)) (Prims.of_int (40))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (78)) (Prims.of_int (41)) - (Prims.of_int (92)) (Prims.of_int (65))))) + (Prims.of_int (79)) (Prims.of_int (41)) + (Prims.of_int (93)) (Prims.of_int (65))))) (Obj.magic uu___2) (fun uu___3 -> (fun uu___3 -> @@ -1193,13 +1193,13 @@ let (arith_to_bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (79)) (Prims.of_int (12)) - (Prims.of_int (79)) (Prims.of_int (23))))) + (Prims.of_int (80)) (Prims.of_int (12)) + (Prims.of_int (80)) (Prims.of_int (23))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (79)) (Prims.of_int (26)) - (Prims.of_int (92)) (Prims.of_int (65))))) + (Prims.of_int (80)) (Prims.of_int (26)) + (Prims.of_int (93)) (Prims.of_int (65))))) (Obj.magic uu___4) (fun uu___5 -> (fun g -> @@ -1211,17 +1211,17 @@ let (arith_to_bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (80)) + (Prims.of_int (81)) (Prims.of_int (12)) - (Prims.of_int (80)) + (Prims.of_int (81)) (Prims.of_int (29))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (81)) + (Prims.of_int (82)) (Prims.of_int (4)) - (Prims.of_int (92)) + (Prims.of_int (93)) (Prims.of_int (65))))) (Obj.magic uu___5) (fun uu___6 -> @@ -1241,17 +1241,17 @@ let (arith_to_bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (83)) + (Prims.of_int (84)) (Prims.of_int (17)) - (Prims.of_int (83)) + (Prims.of_int (84)) (Prims.of_int (41))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (83)) + (Prims.of_int (84)) (Prims.of_int (11)) - (Prims.of_int (89)) + (Prims.of_int (90)) (Prims.of_int (52))))) (Obj.magic uu___7) (fun uu___8 -> @@ -1268,17 +1268,17 @@ let (arith_to_bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (85)) + (Prims.of_int (86)) (Prims.of_int (10)) - (Prims.of_int (85)) + (Prims.of_int (86)) (Prims.of_int (16))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (86)) + (Prims.of_int (87)) (Prims.of_int (10)) - (Prims.of_int (86)) + (Prims.of_int (87)) (Prims.of_int (18))))) (Obj.magic uu___9) @@ -1310,9 +1310,9 @@ let (arith_to_bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (92)) + (Prims.of_int (93)) (Prims.of_int (48)) - (Prims.of_int (92)) + (Prims.of_int (93)) (Prims.of_int (64))))) (FStar_Sealed.seal (Obj.magic @@ -1335,17 +1335,17 @@ let (arith_to_bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (92)) + (Prims.of_int (93)) (Prims.of_int (13)) - (Prims.of_int (92)) + (Prims.of_int (93)) (Prims.of_int (65))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (92)) + (Prims.of_int (93)) (Prims.of_int (8)) - (Prims.of_int (92)) + (Prims.of_int (93)) (Prims.of_int (65))))) (Obj.magic uu___7) (fun uu___8 -> @@ -1369,7 +1369,7 @@ let (bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = FStar_Tactics_V2_Derived.focus (fun uu___1 -> let uu___2 = - FStar_Tactics_MApply.mapply FStar_Tactics_MApply.termable_term + FStar_Tactics_MApply0.mapply0 (FStarC_Reflection_V2_Builtins.pack_ln (FStarC_Reflection_V2_Data.Tv_FVar (FStarC_Reflection_V2_Builtins.pack_fv @@ -1378,19 +1378,18 @@ let (bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (99)) (Prims.of_int (2)) - (Prims.of_int (99)) (Prims.of_int (20))))) + (Prims.of_int (100)) (Prims.of_int (2)) + (Prims.of_int (100)) (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (100)) (Prims.of_int (2)) - (Prims.of_int (105)) (Prims.of_int (8))))) + (Prims.of_int (101)) (Prims.of_int (2)) + (Prims.of_int (106)) (Prims.of_int (8))))) (Obj.magic uu___2) (fun uu___3 -> (fun uu___3 -> let uu___4 = - FStar_Tactics_MApply.mapply - FStar_Tactics_MApply.termable_term + FStar_Tactics_MApply0.mapply0 (FStarC_Reflection_V2_Builtins.pack_ln (FStarC_Reflection_V2_Data.Tv_FVar (FStarC_Reflection_V2_Builtins.pack_fv @@ -1400,13 +1399,13 @@ let (bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (100)) (Prims.of_int (2)) - (Prims.of_int (100)) (Prims.of_int (17))))) + (Prims.of_int (101)) (Prims.of_int (2)) + (Prims.of_int (101)) (Prims.of_int (18))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (101)) (Prims.of_int (2)) - (Prims.of_int (105)) (Prims.of_int (8))))) + (Prims.of_int (102)) (Prims.of_int (2)) + (Prims.of_int (106)) (Prims.of_int (8))))) (Obj.magic uu___4) (fun uu___5 -> (fun uu___5 -> @@ -1417,17 +1416,17 @@ let (bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (101)) + (Prims.of_int (102)) (Prims.of_int (2)) - (Prims.of_int (101)) + (Prims.of_int (102)) (Prims.of_int (20))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (102)) + (Prims.of_int (103)) (Prims.of_int (2)) - (Prims.of_int (105)) + (Prims.of_int (106)) (Prims.of_int (8))))) (Obj.magic uu___6) (fun uu___7 -> @@ -1439,17 +1438,17 @@ let (bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (102)) + (Prims.of_int (103)) (Prims.of_int (2)) - (Prims.of_int (102)) + (Prims.of_int (103)) (Prims.of_int (20))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (103)) + (Prims.of_int (104)) (Prims.of_int (2)) - (Prims.of_int (105)) + (Prims.of_int (106)) (Prims.of_int (8))))) (Obj.magic uu___8) (fun uu___9 -> @@ -1463,17 +1462,17 @@ let (bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (103)) + (Prims.of_int (104)) (Prims.of_int (2)) - (Prims.of_int (103)) + (Prims.of_int (104)) (Prims.of_int (43))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (104)) - (Prims.of_int (2)) (Prims.of_int (105)) + (Prims.of_int (2)) + (Prims.of_int (106)) (Prims.of_int (8))))) (Obj.magic uu___10) (fun uu___11 -> @@ -1487,17 +1486,17 @@ let (bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (104)) + (Prims.of_int (105)) (Prims.of_int (2)) - (Prims.of_int (104)) + (Prims.of_int (105)) (Prims.of_int (14))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (105)) + (Prims.of_int (106)) (Prims.of_int (2)) - (Prims.of_int (105)) + (Prims.of_int (106)) (Prims.of_int (8))))) (Obj.magic uu___12) @@ -1540,13 +1539,13 @@ let (bv_tac_lt : Prims.int -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (109)) (Prims.of_int (11)) - (Prims.of_int (109)) (Prims.of_int (36))))) + (Prims.of_int (110)) (Prims.of_int (11)) + (Prims.of_int (110)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (109)) (Prims.of_int (39)) - (Prims.of_int (115)) (Prims.of_int (8))))) + (Prims.of_int (110)) (Prims.of_int (39)) + (Prims.of_int (116)) (Prims.of_int (8))))) (Obj.magic uu___1) (fun uu___2 -> (fun nn -> @@ -1569,13 +1568,13 @@ let (bv_tac_lt : Prims.int -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (110)) (Prims.of_int (10)) - (Prims.of_int (110)) (Prims.of_int (48))))) + (Prims.of_int (111)) (Prims.of_int (10)) + (Prims.of_int (111)) (Prims.of_int (48))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (111)) (Prims.of_int (2)) - (Prims.of_int (115)) (Prims.of_int (8))))) + (Prims.of_int (112)) (Prims.of_int (2)) + (Prims.of_int (116)) (Prims.of_int (8))))) (Obj.magic uu___2) (fun uu___3 -> (fun t -> @@ -1587,17 +1586,17 @@ let (bv_tac_lt : Prims.int -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (111)) + (Prims.of_int (112)) (Prims.of_int (2)) - (Prims.of_int (111)) + (Prims.of_int (112)) (Prims.of_int (15))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (112)) + (Prims.of_int (113)) (Prims.of_int (2)) - (Prims.of_int (115)) + (Prims.of_int (116)) (Prims.of_int (8))))) (Obj.magic uu___3) (fun uu___4 -> @@ -1609,17 +1608,17 @@ let (bv_tac_lt : Prims.int -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (112)) + (Prims.of_int (113)) (Prims.of_int (2)) - (Prims.of_int (112)) + (Prims.of_int (113)) (Prims.of_int (20))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (113)) + (Prims.of_int (114)) (Prims.of_int (2)) - (Prims.of_int (115)) + (Prims.of_int (116)) (Prims.of_int (8))))) (Obj.magic uu___5) (fun uu___6 -> @@ -1632,17 +1631,17 @@ let (bv_tac_lt : Prims.int -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (113)) + (Prims.of_int (114)) (Prims.of_int (2)) - (Prims.of_int (113)) + (Prims.of_int (114)) (Prims.of_int (20))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (114)) - (Prims.of_int (2)) (Prims.of_int (115)) + (Prims.of_int (2)) + (Prims.of_int (116)) (Prims.of_int (8))))) (Obj.magic uu___7) (fun uu___8 -> @@ -1656,17 +1655,17 @@ let (bv_tac_lt : Prims.int -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (114)) + (Prims.of_int (115)) (Prims.of_int (2)) - (Prims.of_int (114)) + (Prims.of_int (115)) (Prims.of_int (43))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (115)) + (Prims.of_int (116)) (Prims.of_int (2)) - (Prims.of_int (115)) + (Prims.of_int (116)) (Prims.of_int (8))))) (Obj.magic uu___9) @@ -1708,13 +1707,13 @@ let (to_bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (119)) (Prims.of_int (2)) - (Prims.of_int (119)) (Prims.of_int (25))))) + (Prims.of_int (120)) (Prims.of_int (2)) + (Prims.of_int (120)) (Prims.of_int (25))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (120)) (Prims.of_int (2)) - (Prims.of_int (122)) (Prims.of_int (20))))) + (Prims.of_int (121)) (Prims.of_int (2)) + (Prims.of_int (123)) (Prims.of_int (20))))) (Obj.magic uu___2) (fun uu___3 -> (fun uu___3 -> @@ -1729,13 +1728,13 @@ let (to_bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (120)) (Prims.of_int (2)) - (Prims.of_int (120)) (Prims.of_int (22))))) + (Prims.of_int (121)) (Prims.of_int (2)) + (Prims.of_int (121)) (Prims.of_int (22))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (121)) (Prims.of_int (2)) - (Prims.of_int (122)) (Prims.of_int (20))))) + (Prims.of_int (122)) (Prims.of_int (2)) + (Prims.of_int (123)) (Prims.of_int (20))))) (Obj.magic uu___4) (fun uu___5 -> (fun uu___5 -> @@ -1746,17 +1745,17 @@ let (to_bv_tac : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (121)) + (Prims.of_int (122)) (Prims.of_int (2)) - (Prims.of_int (121)) + (Prims.of_int (122)) (Prims.of_int (20))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.BV.fst" - (Prims.of_int (122)) + (Prims.of_int (123)) (Prims.of_int (2)) - (Prims.of_int (122)) + (Prims.of_int (123)) (Prims.of_int (20))))) (Obj.magic uu___6) (fun uu___7 -> diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_CanonCommMonoid.ml b/ocaml/fstar-lib/generated/FStar_Tactics_CanonCommMonoid.ml index 7520de96eb8..8bbd798af29 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_CanonCommMonoid.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_CanonCommMonoid.ml @@ -2211,8 +2211,7 @@ let canon_monoid_aux : -> let uu___14 = - FStar_Tactics_MApply.mapply - FStar_Tactics_MApply.termable_term + FStar_Tactics_MApply0.mapply0 (FStar_Reflection_V2_Derived.mk_app (FStarC_Reflection_V2_Builtins.pack_ln (FStarC_Reflection_V2_Data.Tv_FVar diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_MApply.ml b/ocaml/fstar-lib/generated/FStar_Tactics_MApply.ml index ea0930c9b84..02d0692605b 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_MApply.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_MApply.ml @@ -2,21 +2,21 @@ open Prims type 'a termable = { to_term: - 'a -> (FStar_Tactics_NamedView.term, unit) FStar_Tactics_Effect.tac_repr } + 'a -> (FStarC_Reflection_Types.term, unit) FStar_Tactics_Effect.tac_repr } let __proj__Mktermable__item__to_term : 'a . 'a termable -> 'a -> - (FStar_Tactics_NamedView.term, unit) FStar_Tactics_Effect.tac_repr + (FStarC_Reflection_Types.term, unit) FStar_Tactics_Effect.tac_repr = fun projectee -> match projectee with | { to_term;_} -> to_term let to_term : 'a . 'a termable -> 'a -> - (FStar_Tactics_NamedView.term, unit) FStar_Tactics_Effect.tac_repr + (FStarC_Reflection_Types.term, unit) FStar_Tactics_Effect.tac_repr = fun projectee -> match projectee with | { to_term = to_term1;_} -> to_term1 -let (termable_term : FStar_Tactics_NamedView.term termable) = +let (termable_term : FStarC_Reflection_Types.term termable) = { to_term = (fun uu___ -> @@ -24,7 +24,7 @@ let (termable_term : FStar_Tactics_NamedView.term termable) = Obj.magic (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> t))) uu___) } -let (termable_binding : FStar_Tactics_NamedView.binding termable) = +let (termable_binding : FStarC_Reflection_V2_Data.binding termable) = { to_term = (fun uu___ -> @@ -35,587 +35,6 @@ let (termable_binding : FStar_Tactics_NamedView.binding termable) = FStar_Tactics_V2_SyntaxCoercions.binding_to_term b))) uu___) } -let rec (apply_squash_or_lem : - Prims.nat -> - FStar_Tactics_NamedView.term -> - (unit, unit) FStar_Tactics_Effect.tac_repr) - = - fun d -> - fun t -> - FStar_Tactics_V2_Derived.try_with - (fun uu___ -> match () with | () -> FStar_Tactics_V2_Derived.apply t) - (fun uu___ -> - FStar_Tactics_V2_Derived.try_with - (fun uu___1 -> - match () with - | () -> - let uu___2 = - FStar_Tactics_V2_Derived.apply - (FStarC_Reflection_V2_Builtins.pack_ln - (FStarC_Reflection_V2_Data.Tv_FVar - (FStarC_Reflection_V2_Builtins.pack_fv - ["FStar"; "Squash"; "return_squash"]))) in - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.MApply.fst" - (Prims.of_int (25)) (Prims.of_int (8)) - (Prims.of_int (25)) (Prims.of_int (43))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.MApply.fst" - (Prims.of_int (25)) (Prims.of_int (45)) - (Prims.of_int (25)) (Prims.of_int (52))))) - (Obj.magic uu___2) - (fun uu___3 -> - (fun uu___3 -> - Obj.magic (FStar_Tactics_V2_Derived.apply t)) - uu___3)) - (fun uu___1 -> - FStar_Tactics_V2_Derived.try_with - (fun uu___2 -> - match () with - | () -> FStar_Tactics_V2_Derived.apply_lemma t) - (fun uu___2 -> - (fun uu___2 -> - if d <= Prims.int_zero - then - Obj.magic - (Obj.repr - (FStar_Tactics_V2_Derived.fail - "mapply: out of fuel")) - else - Obj.magic - (Obj.repr - (let uu___4 = - let uu___5 = - FStar_Tactics_V2_Derived.cur_env () in - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (31)) - (Prims.of_int (16)) - (Prims.of_int (31)) - (Prims.of_int (28))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (31)) - (Prims.of_int (13)) - (Prims.of_int (31)) - (Prims.of_int (30))))) - (Obj.magic uu___5) - (fun uu___6 -> - (fun uu___6 -> - Obj.magic - (FStarC_Tactics_V2_Builtins.tc - uu___6 t)) uu___6) in - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (31)) - (Prims.of_int (13)) - (Prims.of_int (31)) - (Prims.of_int (30))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (31)) - (Prims.of_int (33)) - (Prims.of_int (80)) - (Prims.of_int (41))))) - (Obj.magic uu___4) - (fun uu___5 -> - (fun ty -> - let uu___5 = - FStar_Tactics_V2_SyntaxHelpers.collect_arr - ty in - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (32)) - (Prims.of_int (17)) - (Prims.of_int (32)) - (Prims.of_int (31))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (31)) - (Prims.of_int (33)) - (Prims.of_int (80)) - (Prims.of_int (41))))) - (Obj.magic uu___5) - (fun uu___6 -> - (fun uu___6 -> - match uu___6 with - | (tys, c) -> - (match FStar_Tactics_NamedView.inspect_comp - c - with - | FStarC_Reflection_V2_Data.C_Lemma - (pre, post, - uu___7) - -> - Obj.magic - (Obj.repr - (let uu___8 - = - Obj.magic - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___9 -> - FStarC_Reflection_V2_Builtins.pack_ln - (FStarC_Reflection_V2_Data.Tv_App - (post, - ((FStarC_Reflection_V2_Builtins.pack_ln - (FStarC_Reflection_V2_Data.Tv_Const - FStarC_Reflection_V2_Data.C_Unit)), - FStarC_Reflection_V2_Data.Q_Explicit))))) in - FStar_Tactics_Effect.tac_bind - ( - FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (36)) - (Prims.of_int (18)) - (Prims.of_int (36)) - (Prims.of_int (32))))) - ( - FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (36)) - (Prims.of_int (35)) - (Prims.of_int (45)) - (Prims.of_int (41))))) - ( - Obj.magic - uu___8) - ( - fun - uu___9 -> - (fun - post1 -> - let uu___9 - = - FStar_Tactics_V2_Derived.norm_term - [] post1 in - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (37)) - (Prims.of_int (18)) - (Prims.of_int (37)) - (Prims.of_int (35))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (39)) - (Prims.of_int (7)) - (Prims.of_int (45)) - (Prims.of_int (41))))) - (Obj.magic - uu___9) - (fun - uu___10 - -> - (fun - post2 -> - let uu___10 - = - FStar_Reflection_V2_Formula.term_as_formula' - post2 in - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (39)) - (Prims.of_int (13)) - (Prims.of_int (39)) - (Prims.of_int (34))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (39)) - (Prims.of_int (7)) - (Prims.of_int (45)) - (Prims.of_int (41))))) - (Obj.magic - uu___10) - (fun - uu___11 - -> - (fun - uu___11 - -> - match uu___11 - with - | - FStar_Reflection_V2_Formula.Implies - (p, q) -> - Obj.magic - (Obj.repr - (let uu___12 - = - FStar_Tactics_V2_Derived.apply_lemma - (FStarC_Reflection_V2_Builtins.pack_ln - (FStarC_Reflection_V2_Data.Tv_FVar - (FStarC_Reflection_V2_Builtins.pack_fv - ["FStar"; - "Tactics"; - "MApply"; - "push1"]))) in - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (41)) - (Prims.of_int (11)) - (Prims.of_int (41)) - (Prims.of_int (31))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (42)) - (Prims.of_int (11)) - (Prims.of_int (42)) - (Prims.of_int (38))))) - (Obj.magic - uu___12) - (fun - uu___13 - -> - (fun - uu___13 - -> - Obj.magic - (apply_squash_or_lem - (d - - Prims.int_one) - t)) - uu___13))) - | - uu___12 - -> - Obj.magic - (Obj.repr - (FStar_Tactics_V2_Derived.fail - "mapply: can't apply (1)"))) - uu___11))) - uu___10))) - uu___9))) - | FStarC_Reflection_V2_Data.C_Total - rt -> - Obj.magic - (Obj.repr - (match - FStar_Reflection_V2_Derived.unsquash_term - rt - with - | FStar_Pervasives_Native.Some - rt1 -> - let uu___7 - = - FStar_Tactics_V2_Derived.norm_term - [] rt1 in - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (53)) - (Prims.of_int (18)) - (Prims.of_int (53)) - (Prims.of_int (33))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (55)) - (Prims.of_int (9)) - (Prims.of_int (61)) - (Prims.of_int (43))))) - (Obj.magic - uu___7) - (fun - uu___8 -> - (fun rt2 - -> - let uu___8 - = - FStar_Reflection_V2_Formula.term_as_formula' - rt2 in - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (55)) - (Prims.of_int (15)) - (Prims.of_int (55)) - (Prims.of_int (34))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (55)) - (Prims.of_int (9)) - (Prims.of_int (61)) - (Prims.of_int (43))))) - (Obj.magic - uu___8) - (fun - uu___9 -> - (fun - uu___9 -> - match uu___9 - with - | - FStar_Reflection_V2_Formula.Implies - (p, q) -> - Obj.magic - (Obj.repr - (let uu___10 - = - FStar_Tactics_V2_Derived.apply_lemma - (FStarC_Reflection_V2_Builtins.pack_ln - (FStarC_Reflection_V2_Data.Tv_FVar - (FStarC_Reflection_V2_Builtins.pack_fv - ["FStar"; - "Tactics"; - "MApply"; - "push1"]))) in - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (57)) - (Prims.of_int (13)) - (Prims.of_int (57)) - (Prims.of_int (33))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (58)) - (Prims.of_int (13)) - (Prims.of_int (58)) - (Prims.of_int (40))))) - (Obj.magic - uu___10) - (fun - uu___11 - -> - (fun - uu___11 - -> - Obj.magic - (apply_squash_or_lem - (d - - Prims.int_one) - t)) - uu___11))) - | - uu___10 - -> - Obj.magic - (Obj.repr - (FStar_Tactics_V2_Derived.fail - "mapply: can't apply (2)"))) - uu___9))) - uu___8) - | FStar_Pervasives_Native.None - -> - let uu___7 - = - FStar_Tactics_V2_Derived.norm_term - [] rt in - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (68)) - (Prims.of_int (18)) - (Prims.of_int (68)) - (Prims.of_int (33))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (70)) - (Prims.of_int (9)) - (Prims.of_int (77)) - (Prims.of_int (20))))) - (Obj.magic - uu___7) - (fun - uu___8 -> - (fun rt1 - -> - let uu___8 - = - FStar_Reflection_V2_Formula.term_as_formula' - rt1 in - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (70)) - (Prims.of_int (15)) - (Prims.of_int (70)) - (Prims.of_int (34))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (70)) - (Prims.of_int (9)) - (Prims.of_int (77)) - (Prims.of_int (20))))) - (Obj.magic - uu___8) - (fun - uu___9 -> - (fun - uu___9 -> - match uu___9 - with - | - FStar_Reflection_V2_Formula.Implies - (p, q) -> - let uu___10 - = - FStar_Tactics_V2_Derived.apply_lemma - (FStarC_Reflection_V2_Builtins.pack_ln - (FStarC_Reflection_V2_Data.Tv_FVar - (FStarC_Reflection_V2_Builtins.pack_fv - ["FStar"; - "Tactics"; - "MApply"; - "push1"]))) in - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (72)) - (Prims.of_int (13)) - (Prims.of_int (72)) - (Prims.of_int (33))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (73)) - (Prims.of_int (13)) - (Prims.of_int (73)) - (Prims.of_int (40))))) - (Obj.magic - uu___10) - (fun - uu___11 - -> - (fun - uu___11 - -> - Obj.magic - (apply_squash_or_lem - (d - - Prims.int_one) - t)) - uu___11)) - | - uu___10 - -> - let uu___11 - = - FStar_Tactics_V2_Derived.apply - (FStarC_Reflection_V2_Builtins.pack_ln - (FStarC_Reflection_V2_Data.Tv_FVar - (FStarC_Reflection_V2_Builtins.pack_fv - ["FStar"; - "Squash"; - "return_squash"]))) in - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (76)) - (Prims.of_int (13)) - (Prims.of_int (76)) - (Prims.of_int (48))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MApply.fst" - (Prims.of_int (77)) - (Prims.of_int (13)) - (Prims.of_int (77)) - (Prims.of_int (20))))) - (Obj.magic - uu___11) - (fun - uu___12 - -> - (fun - uu___12 - -> - Obj.magic - (FStar_Tactics_V2_Derived.apply - t)) - uu___12))) - uu___9))) - uu___8))) - | uu___7 -> - Obj.magic - (Obj.repr - (FStar_Tactics_V2_Derived.fail - "mapply: can't apply (3)")))) - uu___6))) uu___5)))) uu___2))) -let (mapply0 : - FStar_Tactics_NamedView.term -> (unit, unit) FStar_Tactics_Effect.tac_repr) - = fun t -> apply_squash_or_lem (Prims.of_int (10)) t -let _ = - FStarC_Tactics_Native.register_tactic "FStar.Tactics.MApply.mapply0" - (Prims.of_int (2)) - (fun psc -> - fun ncb -> - fun us -> - fun args -> - FStarC_Tactics_InterpFuns.mk_tactic_interpretation_1 - "FStar.Tactics.MApply.mapply0 (plugin)" - (FStarC_Tactics_Native.from_tactic_1 mapply0) - FStarC_Reflection_V2_Embeddings.e_term - FStarC_Syntax_Embeddings.e_unit psc ncb us args) let mapply : 'ty . 'ty termable -> 'ty -> (unit, unit) FStar_Tactics_Effect.tac_repr = fun uu___ -> @@ -625,11 +44,12 @@ let mapply : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MApply.fsti" - (Prims.of_int (35)) (Prims.of_int (10)) (Prims.of_int (35)) + (Prims.of_int (23)) (Prims.of_int (10)) (Prims.of_int (23)) (Prims.of_int (19))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MApply.fsti" - (Prims.of_int (36)) (Prims.of_int (2)) (Prims.of_int (36)) + (Prims.of_int (24)) (Prims.of_int (2)) (Prims.of_int (24)) (Prims.of_int (11))))) (Obj.magic uu___1) - (fun uu___2 -> (fun t -> Obj.magic (mapply0 t)) uu___2) \ No newline at end of file + (fun uu___2 -> + (fun t -> Obj.magic (FStar_Tactics_MApply0.mapply0 t)) uu___2) \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_MApply0.ml b/ocaml/fstar-lib/generated/FStar_Tactics_MApply0.ml new file mode 100644 index 00000000000..bbe9736c9cb --- /dev/null +++ b/ocaml/fstar-lib/generated/FStar_Tactics_MApply0.ml @@ -0,0 +1,582 @@ +open Prims +let rec (apply_squash_or_lem : + Prims.nat -> + FStar_Tactics_NamedView.term -> + (unit, unit) FStar_Tactics_Effect.tac_repr) + = + fun d -> + fun t -> + FStar_Tactics_V2_Derived.try_with + (fun uu___ -> match () with | () -> FStar_Tactics_V2_Derived.apply t) + (fun uu___ -> + FStar_Tactics_V2_Derived.try_with + (fun uu___1 -> + match () with + | () -> + let uu___2 = + FStar_Tactics_V2_Derived.apply + (FStarC_Reflection_V2_Builtins.pack_ln + (FStarC_Reflection_V2_Data.Tv_FVar + (FStarC_Reflection_V2_Builtins.pack_fv + ["FStar"; "Squash"; "return_squash"]))) in + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.MApply0.fst" + (Prims.of_int (24)) (Prims.of_int (8)) + (Prims.of_int (24)) (Prims.of_int (43))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.MApply0.fst" + (Prims.of_int (24)) (Prims.of_int (45)) + (Prims.of_int (24)) (Prims.of_int (52))))) + (Obj.magic uu___2) + (fun uu___3 -> + (fun uu___3 -> + Obj.magic (FStar_Tactics_V2_Derived.apply t)) + uu___3)) + (fun uu___1 -> + FStar_Tactics_V2_Derived.try_with + (fun uu___2 -> + match () with + | () -> FStar_Tactics_V2_Derived.apply_lemma t) + (fun uu___2 -> + (fun uu___2 -> + if d <= Prims.int_zero + then + Obj.magic + (Obj.repr + (FStar_Tactics_V2_Derived.fail + "mapply: out of fuel")) + else + Obj.magic + (Obj.repr + (let uu___4 = + let uu___5 = + FStar_Tactics_V2_Derived.cur_env () in + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (30)) + (Prims.of_int (16)) + (Prims.of_int (30)) + (Prims.of_int (28))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (30)) + (Prims.of_int (13)) + (Prims.of_int (30)) + (Prims.of_int (30))))) + (Obj.magic uu___5) + (fun uu___6 -> + (fun uu___6 -> + Obj.magic + (FStarC_Tactics_V2_Builtins.tc + uu___6 t)) uu___6) in + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (30)) + (Prims.of_int (13)) + (Prims.of_int (30)) + (Prims.of_int (30))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (30)) + (Prims.of_int (33)) + (Prims.of_int (79)) + (Prims.of_int (41))))) + (Obj.magic uu___4) + (fun uu___5 -> + (fun ty -> + let uu___5 = + FStar_Tactics_V2_SyntaxHelpers.collect_arr + ty in + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (31)) + (Prims.of_int (17)) + (Prims.of_int (31)) + (Prims.of_int (31))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (30)) + (Prims.of_int (33)) + (Prims.of_int (79)) + (Prims.of_int (41))))) + (Obj.magic uu___5) + (fun uu___6 -> + (fun uu___6 -> + match uu___6 with + | (tys, c) -> + (match FStar_Tactics_NamedView.inspect_comp + c + with + | FStarC_Reflection_V2_Data.C_Lemma + (pre, post, + uu___7) + -> + Obj.magic + (Obj.repr + (let uu___8 + = + Obj.magic + (FStar_Tactics_Effect.lift_div_tac + (fun + uu___9 -> + FStarC_Reflection_V2_Builtins.pack_ln + (FStarC_Reflection_V2_Data.Tv_App + (post, + ((FStarC_Reflection_V2_Builtins.pack_ln + (FStarC_Reflection_V2_Data.Tv_Const + FStarC_Reflection_V2_Data.C_Unit)), + FStarC_Reflection_V2_Data.Q_Explicit))))) in + FStar_Tactics_Effect.tac_bind + ( + FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (35)) + (Prims.of_int (18)) + (Prims.of_int (35)) + (Prims.of_int (32))))) + ( + FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (35)) + (Prims.of_int (35)) + (Prims.of_int (44)) + (Prims.of_int (41))))) + ( + Obj.magic + uu___8) + ( + fun + uu___9 -> + (fun + post1 -> + let uu___9 + = + FStar_Tactics_V2_Derived.norm_term + [] post1 in + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (36)) + (Prims.of_int (18)) + (Prims.of_int (36)) + (Prims.of_int (35))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (38)) + (Prims.of_int (7)) + (Prims.of_int (44)) + (Prims.of_int (41))))) + (Obj.magic + uu___9) + (fun + uu___10 + -> + (fun + post2 -> + let uu___10 + = + FStar_Reflection_V2_Formula.term_as_formula' + post2 in + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (38)) + (Prims.of_int (13)) + (Prims.of_int (38)) + (Prims.of_int (34))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (38)) + (Prims.of_int (7)) + (Prims.of_int (44)) + (Prims.of_int (41))))) + (Obj.magic + uu___10) + (fun + uu___11 + -> + (fun + uu___11 + -> + match uu___11 + with + | + FStar_Reflection_V2_Formula.Implies + (p, q) -> + Obj.magic + (Obj.repr + (let uu___12 + = + FStar_Tactics_V2_Derived.apply_lemma + (FStarC_Reflection_V2_Builtins.pack_ln + (FStarC_Reflection_V2_Data.Tv_FVar + (FStarC_Reflection_V2_Builtins.pack_fv + ["FStar"; + "Tactics"; + "MApply0"; + "push1"]))) in + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (40)) + (Prims.of_int (11)) + (Prims.of_int (40)) + (Prims.of_int (31))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (41)) + (Prims.of_int (11)) + (Prims.of_int (41)) + (Prims.of_int (38))))) + (Obj.magic + uu___12) + (fun + uu___13 + -> + (fun + uu___13 + -> + Obj.magic + (apply_squash_or_lem + (d - + Prims.int_one) + t)) + uu___13))) + | + uu___12 + -> + Obj.magic + (Obj.repr + (FStar_Tactics_V2_Derived.fail + "mapply: can't apply (1)"))) + uu___11))) + uu___10))) + uu___9))) + | FStarC_Reflection_V2_Data.C_Total + rt -> + Obj.magic + (Obj.repr + (match + FStar_Reflection_V2_Derived.unsquash_term + rt + with + | FStar_Pervasives_Native.Some + rt1 -> + let uu___7 + = + FStar_Tactics_V2_Derived.norm_term + [] rt1 in + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (52)) + (Prims.of_int (18)) + (Prims.of_int (52)) + (Prims.of_int (33))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (54)) + (Prims.of_int (9)) + (Prims.of_int (60)) + (Prims.of_int (43))))) + (Obj.magic + uu___7) + (fun + uu___8 -> + (fun rt2 + -> + let uu___8 + = + FStar_Reflection_V2_Formula.term_as_formula' + rt2 in + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (54)) + (Prims.of_int (15)) + (Prims.of_int (54)) + (Prims.of_int (34))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (54)) + (Prims.of_int (9)) + (Prims.of_int (60)) + (Prims.of_int (43))))) + (Obj.magic + uu___8) + (fun + uu___9 -> + (fun + uu___9 -> + match uu___9 + with + | + FStar_Reflection_V2_Formula.Implies + (p, q) -> + Obj.magic + (Obj.repr + (let uu___10 + = + FStar_Tactics_V2_Derived.apply_lemma + (FStarC_Reflection_V2_Builtins.pack_ln + (FStarC_Reflection_V2_Data.Tv_FVar + (FStarC_Reflection_V2_Builtins.pack_fv + ["FStar"; + "Tactics"; + "MApply0"; + "push1"]))) in + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (56)) + (Prims.of_int (13)) + (Prims.of_int (56)) + (Prims.of_int (33))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (57)) + (Prims.of_int (13)) + (Prims.of_int (57)) + (Prims.of_int (40))))) + (Obj.magic + uu___10) + (fun + uu___11 + -> + (fun + uu___11 + -> + Obj.magic + (apply_squash_or_lem + (d - + Prims.int_one) + t)) + uu___11))) + | + uu___10 + -> + Obj.magic + (Obj.repr + (FStar_Tactics_V2_Derived.fail + "mapply: can't apply (2)"))) + uu___9))) + uu___8) + | FStar_Pervasives_Native.None + -> + let uu___7 + = + FStar_Tactics_V2_Derived.norm_term + [] rt in + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (67)) + (Prims.of_int (18)) + (Prims.of_int (67)) + (Prims.of_int (33))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (69)) + (Prims.of_int (9)) + (Prims.of_int (76)) + (Prims.of_int (20))))) + (Obj.magic + uu___7) + (fun + uu___8 -> + (fun rt1 + -> + let uu___8 + = + FStar_Reflection_V2_Formula.term_as_formula' + rt1 in + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (69)) + (Prims.of_int (15)) + (Prims.of_int (69)) + (Prims.of_int (34))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (69)) + (Prims.of_int (9)) + (Prims.of_int (76)) + (Prims.of_int (20))))) + (Obj.magic + uu___8) + (fun + uu___9 -> + (fun + uu___9 -> + match uu___9 + with + | + FStar_Reflection_V2_Formula.Implies + (p, q) -> + let uu___10 + = + FStar_Tactics_V2_Derived.apply_lemma + (FStarC_Reflection_V2_Builtins.pack_ln + (FStarC_Reflection_V2_Data.Tv_FVar + (FStarC_Reflection_V2_Builtins.pack_fv + ["FStar"; + "Tactics"; + "MApply0"; + "push1"]))) in + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (71)) + (Prims.of_int (13)) + (Prims.of_int (71)) + (Prims.of_int (33))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (72)) + (Prims.of_int (13)) + (Prims.of_int (72)) + (Prims.of_int (40))))) + (Obj.magic + uu___10) + (fun + uu___11 + -> + (fun + uu___11 + -> + Obj.magic + (apply_squash_or_lem + (d - + Prims.int_one) + t)) + uu___11)) + | + uu___10 + -> + let uu___11 + = + FStar_Tactics_V2_Derived.apply + (FStarC_Reflection_V2_Builtins.pack_ln + (FStarC_Reflection_V2_Data.Tv_FVar + (FStarC_Reflection_V2_Builtins.pack_fv + ["FStar"; + "Squash"; + "return_squash"]))) in + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (75)) + (Prims.of_int (13)) + (Prims.of_int (75)) + (Prims.of_int (48))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MApply0.fst" + (Prims.of_int (76)) + (Prims.of_int (13)) + (Prims.of_int (76)) + (Prims.of_int (20))))) + (Obj.magic + uu___11) + (fun + uu___12 + -> + (fun + uu___12 + -> + Obj.magic + (FStar_Tactics_V2_Derived.apply + t)) + uu___12))) + uu___9))) + uu___8))) + | uu___7 -> + Obj.magic + (Obj.repr + (FStar_Tactics_V2_Derived.fail + "mapply: can't apply (3)")))) + uu___6))) uu___5)))) uu___2))) +let (mapply0 : + FStar_Tactics_NamedView.term -> (unit, unit) FStar_Tactics_Effect.tac_repr) + = fun t -> apply_squash_or_lem (Prims.of_int (10)) t +let _ = + FStarC_Tactics_Native.register_tactic "FStar.Tactics.MApply0.mapply0" + (Prims.of_int (2)) + (fun psc -> + fun ncb -> + fun us -> + fun args -> + FStarC_Tactics_InterpFuns.mk_tactic_interpretation_1 + "FStar.Tactics.MApply0.mapply0 (plugin)" + (FStarC_Tactics_Native.from_tactic_1 mapply0) + FStarC_Reflection_V2_Embeddings.e_term + FStarC_Syntax_Embeddings.e_unit psc ncb us args) \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Parametricity.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Parametricity.ml index 625efda7e42..e4273400666 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Parametricity.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Parametricity.ml @@ -3910,13 +3910,13 @@ let (param_inductive : (Prims.of_int (322)) (Prims.of_int (16)) (Prims.of_int (322)) - (Prims.of_int (54))))) + (Prims.of_int (59))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Parametricity.fst" (Prims.of_int (322)) - (Prims.of_int (57)) + (Prims.of_int (62)) (Prims.of_int (325)) (Prims.of_int (20))))) (Obj.magic diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V1.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V1.ml deleted file mode 100644 index e8306abedb2..00000000000 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V1.ml +++ /dev/null @@ -1 +0,0 @@ -open Prims \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2.ml deleted file mode 100644 index e8306abedb2..00000000000 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2.ml +++ /dev/null @@ -1 +0,0 @@ -open Prims \ No newline at end of file diff --git a/ulib/FStar.Reflection.V2.Arith.fst b/ulib/FStar.Reflection.V2.Arith.fst index c2a97add52f..b7ab5b71c85 100644 --- a/ulib/FStar.Reflection.V2.Arith.fst +++ b/ulib/FStar.Reflection.V2.Arith.fst @@ -15,7 +15,7 @@ *) module FStar.Reflection.V2.Arith -open FStar.Tactics.V2 +open FStar.Tactics.V2.Bare open FStar.Reflection.V2 module O = FStar.Order diff --git a/ulib/FStar.Tactics.Arith.fst b/ulib/FStar.Tactics.Arith.fst index 6fb725a306a..fb5c0e654fd 100644 --- a/ulib/FStar.Tactics.Arith.fst +++ b/ulib/FStar.Tactics.Arith.fst @@ -15,7 +15,7 @@ *) module FStar.Tactics.Arith -open FStar.Tactics.V2 +open FStar.Tactics.V2.Bare open FStar.Reflection.V2.Formula open FStar.Reflection.V2.Arith diff --git a/ulib/FStar.Tactics.BV.fst b/ulib/FStar.Tactics.BV.fst index 8735133fc57..ffc88862410 100644 --- a/ulib/FStar.Tactics.BV.fst +++ b/ulib/FStar.Tactics.BV.fst @@ -15,7 +15,8 @@ *) module FStar.Tactics.BV -open FStar.Tactics.V2 +open FStar.Tactics.V2.Bare +open FStar.Tactics.MApply0 open FStar.Reflection.V2.Formula open FStar.Reflection.V2.Arith open FStar.BV @@ -96,8 +97,8 @@ let arith_to_bv_tac () : Tac unit = focus (fun () -> too. This can be useful, if we have mixed expressions so I'll leave it as is for now *) let bv_tac () = focus (fun () -> - mapply (`eq_to_bv); - mapply (`trans); + mapply0 (`eq_to_bv); + mapply0 (`trans); arith_to_bv_tac (); arith_to_bv_tac (); set_options "--smtencoding.elim_box true"; diff --git a/ulib/FStar.Tactics.Canon.fst b/ulib/FStar.Tactics.Canon.fst index b9567936fca..61a7ef8f431 100644 --- a/ulib/FStar.Tactics.Canon.fst +++ b/ulib/FStar.Tactics.Canon.fst @@ -16,7 +16,7 @@ module FStar.Tactics.Canon open FStar.Reflection.V2 -open FStar.Tactics.V2 +open FStar.Tactics.V2.Bare open FStar.Reflection.V2.Arith open FStar.Mul module O = FStar.Order diff --git a/ulib/FStar.Tactics.CanonCommMonoid.fst b/ulib/FStar.Tactics.CanonCommMonoid.fst index 131b8600628..18553f1ca9f 100644 --- a/ulib/FStar.Tactics.CanonCommMonoid.fst +++ b/ulib/FStar.Tactics.CanonCommMonoid.fst @@ -365,8 +365,8 @@ let canon_monoid_aux // dump ("expected after =" ^ term_to_string (norm_term [delta;primops] // (quote (xsdenote m vm (canon vm p r1) == // xsdenote m vm (canon vm p r2))))); - // mapply (quote (monoid_reflect #a #b p pc)); - mapply (mk_app (`monoid_reflect) [(ta, Q_Implicit); + // mapply0 (quote (monoid_reflect #a #b p pc)); + mapply0 (mk_app (`monoid_reflect) [(ta, Q_Implicit); (tb, Q_Implicit); (tp, Q_Explicit); (tpc, Q_Explicit)]); diff --git a/ulib/FStar.Tactics.CanonCommMonoidSimple.Equiv.fst b/ulib/FStar.Tactics.CanonCommMonoidSimple.Equiv.fst index 8dd74887e21..954d38c4dca 100644 --- a/ulib/FStar.Tactics.CanonCommMonoidSimple.Equiv.fst +++ b/ulib/FStar.Tactics.CanonCommMonoidSimple.Equiv.fst @@ -19,7 +19,7 @@ open FStar.Algebra.CommMonoid.Equiv open FStar.List open FStar.Classical open FStar.Tactics.CanonCommSwaps -open FStar.Tactics.V2 +open FStar.Tactics.V2.Bare private let term_eq = FStar.Reflection.TermEq.Simple.term_eq diff --git a/ulib/FStar.Tactics.CanonCommMonoidSimple.fst b/ulib/FStar.Tactics.CanonCommMonoidSimple.fst index 7f5953f98c1..17305a9d45c 100644 --- a/ulib/FStar.Tactics.CanonCommMonoidSimple.fst +++ b/ulib/FStar.Tactics.CanonCommMonoidSimple.fst @@ -18,7 +18,7 @@ module FStar.Tactics.CanonCommMonoidSimple open FStar.Algebra.CommMonoid open FStar.List open FStar.Reflection.V2 -open FStar.Tactics.V2 +open FStar.Tactics.V2.Bare open FStar.Classical open FStar.Tactics.CanonCommSwaps diff --git a/ulib/FStar.Tactics.CheckLN.fst b/ulib/FStar.Tactics.CheckLN.fst index 29f3aff3232..0b1791a4e7b 100644 --- a/ulib/FStar.Tactics.CheckLN.fst +++ b/ulib/FStar.Tactics.CheckLN.fst @@ -1,6 +1,6 @@ module FStar.Tactics.CheckLN -open FStar.Tactics.V2 +open FStar.Tactics.V2.Bare open FStar.Tactics.Util let rec for_all (p : 'a -> Tac bool) (l : list 'a) : Tac bool = diff --git a/ulib/FStar.Tactics.CheckLN.fsti b/ulib/FStar.Tactics.CheckLN.fsti index dc59d95d712..3f9e4c9d78c 100644 --- a/ulib/FStar.Tactics.CheckLN.fsti +++ b/ulib/FStar.Tactics.CheckLN.fsti @@ -1,6 +1,6 @@ module FStar.Tactics.CheckLN -open FStar.Tactics.V2 +open FStar.Tactics.V2.Bare (* Checks if a term is locally nameless. *) [@@plugin] diff --git a/ulib/FStar.Tactics.MApply.fst b/ulib/FStar.Tactics.MApply.fst index b024a10fd52..5ec9c4a3a7e 100644 --- a/ulib/FStar.Tactics.MApply.fst +++ b/ulib/FStar.Tactics.MApply.fst @@ -1,85 +1,3 @@ module FStar.Tactics.MApply -open FStar.Reflection.V2 -open FStar.Reflection.V2.Formula - -open FStar.Tactics.Effect -open FStar.Stubs.Tactics.V2.Builtins -open FStar.Tactics.NamedView -open FStar.Tactics.V2.SyntaxHelpers -open FStar.Tactics.V2.Derived -open FStar.Tactics.V2.SyntaxCoercions - -open FStar.Tactics.Typeclasses -let push1 #p #q f u = () -let push1' #p #q f u = () - -(* - * Some easier applying, which should prevent frustration - * (or cause more when it doesn't do what you wanted to) - *) -val apply_squash_or_lem : d:nat -> term -> Tac unit -let rec apply_squash_or_lem d t = - (* Before anything, try a vanilla apply and apply_lemma *) - try apply t with | _ -> - try apply (`FStar.Squash.return_squash); apply t with | _ -> - try apply_lemma t with | _ -> - - // Fuel cutoff, just in case. - if d <= 0 then fail "mapply: out of fuel" else begin - - let ty = tc (cur_env ()) t in - let tys, c = collect_arr ty in - match inspect_comp c with - | C_Lemma pre post _ -> - begin - let post = `((`#post) ()) in (* unthunk *) - let post = norm_term [] post in - (* Is the lemma an implication? We can try to intro *) - match term_as_formula' post with - | Implies p q -> - apply_lemma (`push1); - apply_squash_or_lem (d-1) t - - | _ -> - fail "mapply: can't apply (1)" - end - | C_Total rt -> - begin match unsquash_term rt with - (* If the function returns a squash, just apply it, since our goals are squashed *) - | Some rt -> - // DUPLICATED, refactor! - begin - let rt = norm_term [] rt in - (* Is the lemma an implication? We can try to intro *) - match term_as_formula' rt with - | Implies p q -> - apply_lemma (`push1); - apply_squash_or_lem (d-1) t - - | _ -> - fail "mapply: can't apply (2)" - end - - (* If not, we can try to introduce the squash ourselves first *) - | None -> - // DUPLICATED, refactor! - begin - let rt = norm_term [] rt in - (* Is the lemma an implication? We can try to intro *) - match term_as_formula' rt with - | Implies p q -> - apply_lemma (`push1); - apply_squash_or_lem (d-1) t - - | _ -> - apply (`FStar.Squash.return_squash); - apply t - end - end - | _ -> fail "mapply: can't apply (3)" - end - -(* `m` is for `magic` *) -let mapply0 (t : term) : Tac unit = - apply_squash_or_lem 10 t +(* This file just here to trigger extraction. *) diff --git a/ulib/FStar.Tactics.MApply.fsti b/ulib/FStar.Tactics.MApply.fsti index ce9e86cdf81..2a79d8eb5b6 100644 --- a/ulib/FStar.Tactics.MApply.fsti +++ b/ulib/FStar.Tactics.MApply.fsti @@ -1,19 +1,11 @@ module FStar.Tactics.MApply -open FStar.Reflection.V2 +open FStar.Stubs.Reflection.Types +open FStar.Stubs.Reflection.V2.Data open FStar.Tactics.Effect -open FStar.Tactics.Typeclasses open FStar.Tactics.V2.SyntaxCoercions -(* Used by mapply, must be exposed, but not to be used directly *) -private val push1 : (#p:Type) -> (#q:Type) -> - squash (p ==> q) -> - squash p -> - squash q -private val push1' : (#p:Type) -> (#q:Type) -> - (p ==> q) -> - squash p -> - squash q +include FStar.Tactics.MApply0 class termable (a : Type) = { to_term : a -> Tac term @@ -27,10 +19,6 @@ instance termable_binding : termable binding = { to_term = (fun b -> binding_to_term b); } -(* `m` is for `magic` *) -[@@plugin] -val mapply0 (t : term) : Tac unit - let mapply (#ty:Type) {| termable ty |} (x : ty) : Tac unit = let t = to_term x in mapply0 t diff --git a/ulib/FStar.Tactics.MApply0.fst b/ulib/FStar.Tactics.MApply0.fst new file mode 100644 index 00000000000..887e055d02b --- /dev/null +++ b/ulib/FStar.Tactics.MApply0.fst @@ -0,0 +1,84 @@ +module FStar.Tactics.MApply0 + +open FStar.Reflection.V2 +open FStar.Reflection.V2.Formula + +open FStar.Tactics.Effect +open FStar.Stubs.Tactics.V2.Builtins +open FStar.Tactics.NamedView +open FStar.Tactics.V2.SyntaxHelpers +open FStar.Tactics.V2.Derived +open FStar.Tactics.V2.SyntaxCoercions + +let push1 #p #q f u = () +let push1' #p #q f u = () + +(* + * Some easier applying, which should prevent frustration + * (or cause more when it doesn't do what you wanted to) + *) +val apply_squash_or_lem : d:nat -> term -> Tac unit +let rec apply_squash_or_lem d t = + (* Before anything, try a vanilla apply and apply_lemma *) + try apply t with | _ -> + try apply (`FStar.Squash.return_squash); apply t with | _ -> + try apply_lemma t with | _ -> + + // Fuel cutoff, just in case. + if d <= 0 then fail "mapply: out of fuel" else begin + + let ty = tc (cur_env ()) t in + let tys, c = collect_arr ty in + match inspect_comp c with + | C_Lemma pre post _ -> + begin + let post = `((`#post) ()) in (* unthunk *) + let post = norm_term [] post in + (* Is the lemma an implication? We can try to intro *) + match term_as_formula' post with + | Implies p q -> + apply_lemma (`push1); + apply_squash_or_lem (d-1) t + + | _ -> + fail "mapply: can't apply (1)" + end + | C_Total rt -> + begin match unsquash_term rt with + (* If the function returns a squash, just apply it, since our goals are squashed *) + | Some rt -> + // DUPLICATED, refactor! + begin + let rt = norm_term [] rt in + (* Is the lemma an implication? We can try to intro *) + match term_as_formula' rt with + | Implies p q -> + apply_lemma (`push1); + apply_squash_or_lem (d-1) t + + | _ -> + fail "mapply: can't apply (2)" + end + + (* If not, we can try to introduce the squash ourselves first *) + | None -> + // DUPLICATED, refactor! + begin + let rt = norm_term [] rt in + (* Is the lemma an implication? We can try to intro *) + match term_as_formula' rt with + | Implies p q -> + apply_lemma (`push1); + apply_squash_or_lem (d-1) t + + | _ -> + apply (`FStar.Squash.return_squash); + apply t + end + end + | _ -> fail "mapply: can't apply (3)" + end + +(* `m` is for `magic` *) +let mapply0 (t : term) : Tac unit = + apply_squash_or_lem 10 t diff --git a/ulib/FStar.Tactics.MApply0.fsti b/ulib/FStar.Tactics.MApply0.fsti new file mode 100644 index 00000000000..7b923720b1a --- /dev/null +++ b/ulib/FStar.Tactics.MApply0.fsti @@ -0,0 +1,18 @@ +module FStar.Tactics.MApply0 + +open FStar.Stubs.Reflection.Types +open FStar.Tactics.Effect + +(* Used by mapply, must be exposed, but not to be used directly *) +private val push1 : (#p:Type) -> (#q:Type) -> + squash (p ==> q) -> + squash p -> + squash q +private val push1' : (#p:Type) -> (#q:Type) -> + (p ==> q) -> + squash p -> + squash q + +(* `m` is for `magic` *) +[@@plugin] +val mapply0 (t : term) : Tac unit diff --git a/ulib/FStar.Tactics.Parametricity.fst b/ulib/FStar.Tactics.Parametricity.fst index 08e7efcb056..51c68d5855a 100644 --- a/ulib/FStar.Tactics.Parametricity.fst +++ b/ulib/FStar.Tactics.Parametricity.fst @@ -1,7 +1,7 @@ module FStar.Tactics.Parametricity open FStar.List -open FStar.Tactics.V2 +open FStar.Tactics.V2.Bare type bvmap = list (namedv & (binder & binder & binder)) let fvmap = list (fv & fv) @@ -319,7 +319,7 @@ let param_inductive (se:sigelt) (fv0 fv1 : fv) : Tac decls = //Tactics.Util.iter (fun bv -> dump ("param bv = " ^ binder_to_string bv)) param_bs; let typ = mk_e_app (param' s typ) [replace_by s false orig; replace_by s true orig] in (* dump ("new typ = " ^ term_to_string typ); *) - let ctors = Tactics.V2.map (param_ctor nm s) ctors in + let ctors = Tactics.V2.Bare.map (param_ctor nm s) ctors in let se = Sg_Inductive {nm=inspect_fv fv1; univs; params=param_bs; typ; ctors} in (* dump ("param_ind : " ^ term_to_string (quote se)); *) [pack_sigelt se] diff --git a/ulib/FStar.Tactics.TypeRepr.fst b/ulib/FStar.Tactics.TypeRepr.fst index 16b6a6395d7..5fb2055bf7d 100644 --- a/ulib/FStar.Tactics.TypeRepr.fst +++ b/ulib/FStar.Tactics.TypeRepr.fst @@ -2,7 +2,7 @@ module FStar.Tactics.TypeRepr //#set-options "--print_implicits --print_full_names --print_universes" -open FStar.Tactics.V2 +open FStar.Tactics.V2.Bare let add_suffix (s:string) (nm:name) : name = explode_qn (implode_qn nm ^ s) diff --git a/ulib/FStar.Tactics.TypeRepr.fsti b/ulib/FStar.Tactics.TypeRepr.fsti index 8b03aa51cb3..f9730db5dd0 100644 --- a/ulib/FStar.Tactics.TypeRepr.fsti +++ b/ulib/FStar.Tactics.TypeRepr.fsti @@ -1,6 +1,6 @@ module FStar.Tactics.TypeRepr -open FStar.Tactics.V2 +open FStar.Tactics.V2.Bare private let empty_elim (e:empty) (#a:Type) : a = match e with diff --git a/ulib/FStar.Tactics.V1.fst b/ulib/FStar.Tactics.V1.fsti similarity index 100% rename from ulib/FStar.Tactics.V1.fst rename to ulib/FStar.Tactics.V1.fsti diff --git a/ulib/FStar.Tactics.V2.fst b/ulib/FStar.Tactics.V2.Bare.fsti similarity index 86% rename from ulib/FStar.Tactics.V2.fst rename to ulib/FStar.Tactics.V2.Bare.fsti index 3b185f1ff43..8cffaa8dd62 100644 --- a/ulib/FStar.Tactics.V2.fst +++ b/ulib/FStar.Tactics.V2.Bare.fsti @@ -13,9 +13,7 @@ See the License for the specific language governing permissions and limitations under the License. *) -module FStar.Tactics.V2 - -(* REVISIT THIS LIST! *) +module FStar.Tactics.V2.Bare include FStar.Stubs.Reflection.Types include FStar.Reflection.V2 @@ -32,7 +30,6 @@ include FStar.Tactics.Util include FStar.Tactics.Print include FStar.Tactics.Visit include FStar.Tactics.NamedView -include FStar.Tactics.MApply +include FStar.Tactics.SMT -include FStar.Tactics.SMT (* Version agnostic *) -include FStar.Reflection.TermEq.Simple \ No newline at end of file +include FStar.Reflection.TermEq.Simple diff --git a/ulib/FStar.Tactics.V2.fsti b/ulib/FStar.Tactics.V2.fsti new file mode 100644 index 00000000000..5376f07e4b0 --- /dev/null +++ b/ulib/FStar.Tactics.V2.fsti @@ -0,0 +1,24 @@ +(* + Copyright 2008-2018 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module FStar.Tactics.V2 + +(* The bare version, plus some particular things we expose to users +for convenience. Crucially, mapply must be here, so we can open +tactics.v2.bare in typeclasses, and typeclasses in mapply, and not +trigger a cycle. *) +include FStar.Tactics.V2.Bare +include FStar.Tactics.MApply0 +include FStar.Tactics.MApply diff --git a/ulib/FStar.Tactics.fst b/ulib/FStar.Tactics.fsti similarity index 100% rename from ulib/FStar.Tactics.fst rename to ulib/FStar.Tactics.fsti