diff --git a/ocaml/fstar-lib/generated/FStar_Class_Add.ml b/ocaml/fstar-lib/generated/FStar_Class_Add.ml index 1c94f0adfb1..18a6c380f40 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Add.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Add.ml @@ -3,14 +3,13 @@ type 'a additive = { zero: 'a ; plus: 'a -> 'a -> 'a } let __proj__Mkadditive__item__zero : 'a . 'a additive -> 'a = - fun projectee -> match projectee with | { zero; plus;_} -> zero -let __proj__Mkadditive__item__plus : 'a . 'a additive -> 'a -> 'a -> 'a = - fun projectee -> match projectee with | { zero; plus;_} -> plus + fun x4 -> match x4 with | { zero = azero; plus = aplus;_} -> azero let zero : 'a . 'a additive -> 'a = - fun projectee -> match projectee with | { zero = zero1; plus;_} -> zero1 + fun x4 -> __proj__Mkadditive__item__zero x4 +let __proj__Mkadditive__item__plus : 'a . 'a additive -> 'a -> 'a -> 'a = + fun x5 -> match x5 with | { zero = azero; plus = aplus;_} -> aplus let plus : 'a . 'a additive -> 'a -> 'a -> 'a = - fun projectee -> - match projectee with | { zero = zero1; plus = plus1;_} -> plus1 + fun x5 -> __proj__Mkadditive__item__plus x5 let op_Plus_Plus : 'a . 'a additive -> 'a -> 'a -> 'a = plus let (add_int : Prims.int additive) = { zero = Prims.int_zero; plus = (+) } let (add_bool : Prims.bool additive) = { zero = false; plus = (||) } diff --git a/ocaml/fstar-lib/generated/FStar_Class_Binders.ml b/ocaml/fstar-lib/generated/FStar_Class_Binders.ml index 4b59d1215d7..8a9d926562e 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Binders.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Binders.ml @@ -6,14 +6,12 @@ let __proj__MkhasNames__item__freeNames : 'a . 'a hasNames -> 'a -> FStar_Syntax_Syntax.bv FStar_Compiler_FlatSet.flat_set - = fun projectee -> match projectee with | { freeNames;_} -> freeNames + = fun x3 -> match x3 with | { freeNames = afreeNames;_} -> afreeNames let freeNames : 'a . 'a hasNames -> 'a -> FStar_Syntax_Syntax.bv FStar_Compiler_FlatSet.flat_set - = - fun projectee -> - match projectee with | { freeNames = freeNames1;_} -> freeNames1 + = fun x3 -> __proj__MkhasNames__item__freeNames x3 type 'a hasBinders = { boundNames: 'a -> FStar_Syntax_Syntax.bv FStar_Compiler_FlatSet.flat_set } @@ -21,14 +19,12 @@ let __proj__MkhasBinders__item__boundNames : 'a . 'a hasBinders -> 'a -> FStar_Syntax_Syntax.bv FStar_Compiler_FlatSet.flat_set - = fun projectee -> match projectee with | { boundNames;_} -> boundNames + = fun x3 -> match x3 with | { boundNames = aboundNames;_} -> aboundNames let boundNames : 'a . 'a hasBinders -> 'a -> FStar_Syntax_Syntax.bv FStar_Compiler_FlatSet.flat_set - = - fun projectee -> - match projectee with | { boundNames = boundNames1;_} -> boundNames1 + = fun x3 -> __proj__MkhasBinders__item__boundNames x3 let (hasNames_term : FStar_Syntax_Syntax.term hasNames) = { freeNames = FStar_Syntax_Free.names } let (hasNames_comp : FStar_Syntax_Syntax.comp hasNames) = diff --git a/ocaml/fstar-lib/generated/FStar_Class_Deq.ml b/ocaml/fstar-lib/generated/FStar_Class_Deq.ml index dc8123b2a79..d5c02c171b1 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Deq.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Deq.ml @@ -3,12 +3,11 @@ type 'a deq = { op_Equals_Question: 'a -> 'a -> Prims.bool } let __proj__Mkdeq__item__op_Equals_Question : 'a . 'a deq -> 'a -> 'a -> Prims.bool = - fun projectee -> - match projectee with | { op_Equals_Question;_} -> op_Equals_Question + fun x3 -> + match x3 with + | { op_Equals_Question = aop_Equals_Question;_} -> aop_Equals_Question let op_Equals_Question : 'a . 'a deq -> 'a -> 'a -> Prims.bool = - fun projectee -> - match projectee with - | { op_Equals_Question = op_Equals_Question1;_} -> op_Equals_Question1 + fun x3 -> __proj__Mkdeq__item__op_Equals_Question x3 let op_Less_Greater_Question : 'a . 'a deq -> 'a -> 'a -> Prims.bool = fun uu___ -> fun x -> diff --git a/ocaml/fstar-lib/generated/FStar_Class_Embeddable.ml b/ocaml/fstar-lib/generated/FStar_Class_Embeddable.ml index b16b908853a..b1ce916a21e 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Embeddable.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Embeddable.ml @@ -5,15 +5,14 @@ type 'a embeddable = typ: FStar_Reflection_Types.term } let __proj__Mkembeddable__item__embed : 'a . 'a embeddable -> 'a -> FStar_Reflection_Types.term = - fun projectee -> match projectee with | { embed; typ;_} -> embed + fun x4 -> match x4 with | { embed = aembed; typ = atyp;_} -> aembed +let embed : 'a . 'a embeddable -> 'a -> FStar_Reflection_Types.term = + fun x4 -> __proj__Mkembeddable__item__embed x4 let __proj__Mkembeddable__item__typ : 'a . 'a embeddable -> FStar_Reflection_Types.term = - fun projectee -> match projectee with | { embed; typ;_} -> typ -let embed : 'a . 'a embeddable -> 'a -> FStar_Reflection_Types.term = - fun projectee -> match projectee with | { embed = embed1; typ;_} -> embed1 + fun x5 -> match x5 with | { embed = aembed; typ = atyp;_} -> atyp let typ : 'a . 'a embeddable -> FStar_Reflection_Types.term = - fun projectee -> - match projectee with | { embed = embed1; typ = typ1;_} -> typ1 + fun x5 -> __proj__Mkembeddable__item__typ x5 let (embeddable_string : Prims.string embeddable) = { embed = diff --git a/ocaml/fstar-lib/generated/FStar_Class_Eq.ml b/ocaml/fstar-lib/generated/FStar_Class_Eq.ml index 57ebdad99c6..b7e10b5a7ae 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Eq.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Eq.ml @@ -4,9 +4,9 @@ type 'a deq = { raw: 'a FStar_Class_Eq_Raw.deq ; eq_dec: unit } let __proj__Mkdeq__item__raw : 'a . 'a deq -> 'a FStar_Class_Eq_Raw.deq = - fun projectee -> match projectee with | { raw; eq_dec;_} -> raw + fun x4 -> match x4 with | { raw = araw; eq_dec = aeq_dec;_} -> araw let raw : 'a . 'a deq -> 'a FStar_Class_Eq_Raw.deq = - fun projectee -> match projectee with | { raw = raw1; eq_dec;_} -> raw1 + fun x4 -> __proj__Mkdeq__item__raw x4 let deq_raw_deq : 'a . 'a deq -> 'a FStar_Class_Eq_Raw.deq = fun d -> d.raw let eq : 'a . 'a deq -> 'a -> 'a -> Prims.bool = fun d -> fun x -> fun y -> (d.raw).FStar_Class_Eq_Raw.eq x y diff --git a/ocaml/fstar-lib/generated/FStar_Class_Eq_Raw.ml b/ocaml/fstar-lib/generated/FStar_Class_Eq_Raw.ml index bd77b03b44d..2725d31686f 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Eq_Raw.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Eq_Raw.ml @@ -2,9 +2,9 @@ open Prims type 'a deq = { eq: 'a -> 'a -> Prims.bool } let __proj__Mkdeq__item__eq : 'a . 'a deq -> 'a -> 'a -> Prims.bool = - fun projectee -> match projectee with | { eq;_} -> eq + fun x3 -> match x3 with | { eq = aeq;_} -> aeq let eq : 'a . 'a deq -> 'a -> 'a -> Prims.bool = - fun projectee -> match projectee with | { eq = eq1;_} -> eq1 + fun x3 -> __proj__Mkdeq__item__eq x3 let eq_instance_of_eqtype : 'a . unit -> 'a deq = fun uu___ -> { eq = (fun x -> fun y -> x = y) } let (int_has_eq : Prims.int deq) = eq_instance_of_eqtype () diff --git a/ocaml/fstar-lib/generated/FStar_Class_HasRange.ml b/ocaml/fstar-lib/generated/FStar_Class_HasRange.ml index 359765f9910..09a19f677c0 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_HasRange.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_HasRange.ml @@ -5,13 +5,11 @@ type 'a hasRange = setPos: FStar_Compiler_Range_Type.range -> 'a -> 'a } let __proj__MkhasRange__item__pos : 'a . 'a hasRange -> 'a -> FStar_Compiler_Range_Type.range = - fun projectee -> match projectee with | { pos; setPos;_} -> pos + fun x4 -> match x4 with | { pos = apos; setPos = asetPos;_} -> apos +let pos : 'a . 'a hasRange -> 'a -> FStar_Compiler_Range_Type.range = + fun x4 -> __proj__MkhasRange__item__pos x4 let __proj__MkhasRange__item__setPos : 'a . 'a hasRange -> FStar_Compiler_Range_Type.range -> 'a -> 'a = - fun projectee -> match projectee with | { pos; setPos;_} -> setPos -let pos : 'a . 'a hasRange -> 'a -> FStar_Compiler_Range_Type.range = - fun projectee -> match projectee with | { pos = pos1; setPos;_} -> pos1 + fun x5 -> match x5 with | { pos = apos; setPos = asetPos;_} -> asetPos let setPos : 'a . 'a hasRange -> FStar_Compiler_Range_Type.range -> 'a -> 'a - = - fun projectee -> - match projectee with | { pos = pos1; setPos = setPos1;_} -> setPos1 \ No newline at end of file + = fun x5 -> __proj__MkhasRange__item__setPos x5 \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Class_Hashable.ml b/ocaml/fstar-lib/generated/FStar_Class_Hashable.ml index a8dd25810d3..cc3121b561d 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Hashable.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Hashable.ml @@ -3,9 +3,9 @@ type 'a hashable = { hash: 'a -> FStar_Hash.hash_code } let __proj__Mkhashable__item__hash : 'a . 'a hashable -> 'a -> FStar_Hash.hash_code = - fun projectee -> match projectee with | { hash;_} -> hash + fun x3 -> match x3 with | { hash = ahash;_} -> ahash let hash : 'a . 'a hashable -> 'a -> FStar_Hash.hash_code = - fun projectee -> match projectee with | { hash = hash1;_} -> hash1 + fun x3 -> __proj__Mkhashable__item__hash x3 let (showable_hash_code : FStar_Hash.hash_code FStar_Class_Show.showable) = { FStar_Class_Show.show = FStar_Hash.string_of_hash_code } let (eq_hash_code : FStar_Hash.hash_code FStar_Class_Deq.deq) = diff --git a/ocaml/fstar-lib/generated/FStar_Class_Monad.ml b/ocaml/fstar-lib/generated/FStar_Class_Monad.ml index 26aa4f5294b..6a9670adb58 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Monad.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Monad.ml @@ -4,19 +4,18 @@ type 'm monad = return: unit -> Obj.t -> 'm ; op_let_Bang: unit -> unit -> 'm -> (Obj.t -> 'm) -> 'm } let __proj__Mkmonad__item__return : 'm . 'm monad -> unit -> Obj.t -> 'm = - fun projectee -> match projectee with | { return; op_let_Bang;_} -> return + fun x4 -> + match x4 with + | { return = areturn; op_let_Bang = aop_let_Bang;_} -> areturn +let return : 'm . 'm monad -> unit -> Obj.t -> 'm = + fun x4 -> __proj__Mkmonad__item__return x4 let __proj__Mkmonad__item__op_let_Bang : 'm . 'm monad -> unit -> unit -> 'm -> (Obj.t -> 'm) -> 'm = - fun projectee -> - match projectee with | { return; op_let_Bang;_} -> op_let_Bang -let return : 'm . 'm monad -> unit -> Obj.t -> 'm = - fun projectee -> - match projectee with | { return = return1; op_let_Bang;_} -> return1 + fun x5 -> + match x5 with + | { return = areturn; op_let_Bang = aop_let_Bang;_} -> aop_let_Bang let op_let_Bang : 'm . 'm monad -> unit -> unit -> 'm -> (Obj.t -> 'm) -> 'm - = - fun projectee -> - match projectee with - | { return = return1; op_let_Bang = op_let_Bang1;_} -> op_let_Bang1 + = fun x5 -> __proj__Mkmonad__item__op_let_Bang x5 let (monad_option : unit FStar_Pervasives_Native.option monad) = { return = diff --git a/ocaml/fstar-lib/generated/FStar_Class_Monoid.ml b/ocaml/fstar-lib/generated/FStar_Class_Monoid.ml index 8f7b5d9b55a..2f0d1401fc0 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Monoid.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Monoid.ml @@ -3,15 +3,12 @@ type 'a monoid = { mzero: 'a ; mplus: 'a -> 'a -> 'a } let __proj__Mkmonoid__item__mzero : 'a . 'a monoid -> 'a = - fun projectee -> match projectee with | { mzero; mplus;_} -> mzero + fun x4 -> match x4 with | { mzero = amzero; mplus = amplus;_} -> amzero +let mzero : 'a . 'a monoid -> 'a = fun x4 -> __proj__Mkmonoid__item__mzero x4 let __proj__Mkmonoid__item__mplus : 'a . 'a monoid -> 'a -> 'a -> 'a = - fun projectee -> match projectee with | { mzero; mplus;_} -> mplus -let mzero : 'a . 'a monoid -> 'a = - fun projectee -> - match projectee with | { mzero = mzero1; mplus;_} -> mzero1 + fun x5 -> match x5 with | { mzero = amzero; mplus = amplus;_} -> amplus let mplus : 'a . 'a monoid -> 'a -> 'a -> 'a = - fun projectee -> - match projectee with | { mzero = mzero1; mplus = mplus1;_} -> mplus1 + fun x5 -> __proj__Mkmonoid__item__mplus x5 let msum : 'a . 'a monoid -> 'a Prims.list -> 'a = fun uu___ -> fun xs -> FStar_Compiler_List.fold_left (mplus uu___) (mzero uu___) xs diff --git a/ocaml/fstar-lib/generated/FStar_Class_Ord.ml b/ocaml/fstar-lib/generated/FStar_Class_Ord.ml index 2a0c546051d..ced09fc787a 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Ord.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Ord.ml @@ -4,15 +4,14 @@ type 'a ord = super: 'a FStar_Class_Deq.deq ; cmp: 'a -> 'a -> FStar_Compiler_Order.order } let __proj__Mkord__item__super : 'a . 'a ord -> 'a FStar_Class_Deq.deq = - fun projectee -> match projectee with | { super; cmp;_} -> super + fun x4 -> match x4 with | { super = asuper; cmp = acmp;_} -> asuper +let super : 'a . 'a ord -> 'a FStar_Class_Deq.deq = + fun x4 -> __proj__Mkord__item__super x4 let __proj__Mkord__item__cmp : 'a . 'a ord -> 'a -> 'a -> FStar_Compiler_Order.order = - fun projectee -> match projectee with | { super; cmp;_} -> cmp -let super : 'a . 'a ord -> 'a FStar_Class_Deq.deq = - fun projectee -> match projectee with | { super = super1; cmp;_} -> super1 + fun x5 -> match x5 with | { super = asuper; cmp = acmp;_} -> acmp let cmp : 'a . 'a ord -> 'a -> 'a -> FStar_Compiler_Order.order = - fun projectee -> - match projectee with | { super = super1; cmp = cmp1;_} -> cmp1 + fun x5 -> __proj__Mkord__item__cmp x5 let op_Less_Question : 'a . 'a ord -> 'a -> 'a -> Prims.bool = fun uu___ -> fun x -> diff --git a/ocaml/fstar-lib/generated/FStar_Class_PP.ml b/ocaml/fstar-lib/generated/FStar_Class_PP.ml index 9b536c6c907..f10c77bf2d0 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_PP.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_PP.ml @@ -3,9 +3,9 @@ type 'a pretty = { pp: 'a -> FStar_Pprint.document } let __proj__Mkpretty__item__pp : 'a . 'a pretty -> 'a -> FStar_Pprint.document = - fun projectee -> match projectee with | { pp;_} -> pp + fun x3 -> match x3 with | { pp = app;_} -> app let pp : 'a . 'a pretty -> 'a -> FStar_Pprint.document = - fun projectee -> match projectee with | { pp = pp1;_} -> pp1 + fun x3 -> __proj__Mkpretty__item__pp x3 let (pp_unit : unit pretty) = { pp = (fun uu___ -> FStar_Pprint.doc_of_string "()") } let (pp_int : Prims.int pretty) = diff --git a/ocaml/fstar-lib/generated/FStar_Class_Printable.ml b/ocaml/fstar-lib/generated/FStar_Class_Printable.ml index a6c581cf4d4..83194d1e008 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Printable.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Printable.ml @@ -3,10 +3,9 @@ type 'a printable = { to_string: 'a -> Prims.string } let __proj__Mkprintable__item__to_string : 'a . 'a printable -> 'a -> Prims.string = - fun projectee -> match projectee with | { to_string;_} -> to_string + fun x3 -> match x3 with | { to_string = ato_string;_} -> ato_string let to_string : 'a . 'a printable -> 'a -> Prims.string = - fun projectee -> - match projectee with | { to_string = to_string1;_} -> to_string1 + fun x3 -> __proj__Mkprintable__item__to_string x3 let (printable_unit : unit printable) = { to_string = (fun uu___ -> "()") } let (printable_bool : Prims.bool printable) = { to_string = Prims.string_of_bool } diff --git a/ocaml/fstar-lib/generated/FStar_Class_Setlike.ml b/ocaml/fstar-lib/generated/FStar_Class_Setlike.ml index c9d1be35da4..5e43d1eb395 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Setlike.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Setlike.ml @@ -18,274 +18,236 @@ type ('e, 's) setlike = collect: ('e -> 's) -> 'e Prims.list -> 's ; from_list: 'e Prims.list -> 's ; addn: 'e Prims.list -> 's -> 's } -let __proj__Mksetlike__item__empty : 'e 's . ('e, 's) setlike -> unit -> 's = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> empty -let __proj__Mksetlike__item__singleton : 'e 's . ('e, 's) setlike -> 'e -> 's - = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> singleton -let __proj__Mksetlike__item__is_empty : - 'e 's . ('e, 's) setlike -> 's -> Prims.bool = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> is_empty -let __proj__Mksetlike__item__add : 'e 's . ('e, 's) setlike -> 'e -> 's -> 's - = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> add -let __proj__Mksetlike__item__remove : - 'e 's . ('e, 's) setlike -> 'e -> 's -> 's = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> remove -let __proj__Mksetlike__item__mem : - 'e 's . ('e, 's) setlike -> 'e -> 's -> Prims.bool = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> mem -let __proj__Mksetlike__item__equal : - 'e 's . ('e, 's) setlike -> 's -> 's -> Prims.bool = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> equal -let __proj__Mksetlike__item__subset : - 'e 's . ('e, 's) setlike -> 's -> 's -> Prims.bool = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> subset -let __proj__Mksetlike__item__union : - 'e 's . ('e, 's) setlike -> 's -> 's -> 's = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> union -let __proj__Mksetlike__item__inter : - 'e 's . ('e, 's) setlike -> 's -> 's -> 's = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> inter -let __proj__Mksetlike__item__diff : - 'e 's . ('e, 's) setlike -> 's -> 's -> 's = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> diff -let __proj__Mksetlike__item__for_all : - 'e 's . ('e, 's) setlike -> ('e -> Prims.bool) -> 's -> Prims.bool = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> for_all -let __proj__Mksetlike__item__for_any : - 'e 's . ('e, 's) setlike -> ('e -> Prims.bool) -> 's -> Prims.bool = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> for_any -let __proj__Mksetlike__item__elems : - 'e 's . ('e, 's) setlike -> 's -> 'e Prims.list = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> elems -let __proj__Mksetlike__item__collect : - 'e 's . ('e, 's) setlike -> ('e -> 's) -> 'e Prims.list -> 's = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> collect -let __proj__Mksetlike__item__from_list : - 'e 's . ('e, 's) setlike -> 'e Prims.list -> 's = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> from_list -let __proj__Mksetlike__item__addn : - 'e 's . ('e, 's) setlike -> 'e Prims.list -> 's -> 's = - fun projectee -> - match projectee with - | { empty; singleton; is_empty; add; remove; mem; equal; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> addn +let __proj__Mksetlike__item__empty : + 'e . unit -> ('e, Obj.t) setlike -> unit -> Obj.t = + fun s -> + fun x21 -> + match x21 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> + aempty let empty : 'e . unit -> ('e, Obj.t) setlike -> unit -> Obj.t = + fun s -> fun x21 -> __proj__Mksetlike__item__empty () x21 +let __proj__Mksetlike__item__singleton : + 'e . unit -> ('e, Obj.t) setlike -> 'e -> Obj.t = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton; is_empty; add; remove; mem; equal; - subset; union; inter; diff; for_all; for_any; elems; collect; - from_list; addn;_} -> empty1 + fun x22 -> + match x22 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> + asingleton let singleton : 'e . unit -> ('e, Obj.t) setlike -> 'e -> Obj.t = + fun s -> fun x22 -> __proj__Mksetlike__item__singleton () x22 +let __proj__Mksetlike__item__is_empty : + 'e . unit -> ('e, Obj.t) setlike -> Obj.t -> Prims.bool = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty; add; remove; - mem; equal; subset; union; inter; diff; for_all; for_any; elems; - collect; from_list; addn;_} -> singleton1 + fun x23 -> + match x23 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> + ais_empty let is_empty : 'e . unit -> ('e, Obj.t) setlike -> Obj.t -> Prims.bool = + fun s -> fun x23 -> __proj__Mksetlike__item__is_empty () x23 +let __proj__Mksetlike__item__add : + 'e . unit -> ('e, Obj.t) setlike -> 'e -> Obj.t -> Obj.t = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty = is_empty1; - add; remove; mem; equal; subset; union; inter; diff; for_all; - for_any; elems; collect; from_list; addn;_} -> is_empty1 + fun x24 -> + match x24 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> aadd let add : 'e . unit -> ('e, Obj.t) setlike -> 'e -> Obj.t -> Obj.t = + fun s -> fun x24 -> __proj__Mksetlike__item__add () x24 +let __proj__Mksetlike__item__remove : + 'e . unit -> ('e, Obj.t) setlike -> 'e -> Obj.t -> Obj.t = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty = is_empty1; - add = add1; remove; mem; equal; subset; union; inter; diff; - for_all; for_any; elems; collect; from_list; addn;_} -> add1 + fun x25 -> + match x25 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> + aremove let remove : 'e . unit -> ('e, Obj.t) setlike -> 'e -> Obj.t -> Obj.t = + fun s -> fun x25 -> __proj__Mksetlike__item__remove () x25 +let __proj__Mksetlike__item__mem : + 'e . unit -> ('e, Obj.t) setlike -> 'e -> Obj.t -> Prims.bool = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty = is_empty1; - add = add1; remove = remove1; mem; equal; subset; union; inter; - diff; for_all; for_any; elems; collect; from_list; addn;_} -> - remove1 + fun x26 -> + match x26 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> amem let mem : 'e . unit -> ('e, Obj.t) setlike -> 'e -> Obj.t -> Prims.bool = + fun s -> fun x26 -> __proj__Mksetlike__item__mem () x26 +let __proj__Mksetlike__item__equal : + 'e . unit -> ('e, Obj.t) setlike -> Obj.t -> Obj.t -> Prims.bool = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty = is_empty1; - add = add1; remove = remove1; mem = mem1; equal; subset; union; - inter; diff; for_all; for_any; elems; collect; from_list; addn;_} - -> mem1 + fun x27 -> + match x27 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> + aequal let equal : 'e . unit -> ('e, Obj.t) setlike -> Obj.t -> Obj.t -> Prims.bool - = + = fun s -> fun x27 -> __proj__Mksetlike__item__equal () x27 +let __proj__Mksetlike__item__subset : + 'e . unit -> ('e, Obj.t) setlike -> Obj.t -> Obj.t -> Prims.bool = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty = is_empty1; - add = add1; remove = remove1; mem = mem1; equal = equal1; subset; - union; inter; diff; for_all; for_any; elems; collect; from_list; - addn;_} -> equal1 + fun x28 -> + match x28 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> + asubset let subset : 'e . unit -> ('e, Obj.t) setlike -> Obj.t -> Obj.t -> Prims.bool - = + = fun s -> fun x28 -> __proj__Mksetlike__item__subset () x28 +let __proj__Mksetlike__item__union : + 'e . unit -> ('e, Obj.t) setlike -> Obj.t -> Obj.t -> Obj.t = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty = is_empty1; - add = add1; remove = remove1; mem = mem1; equal = equal1; - subset = subset1; union; inter; diff; for_all; for_any; elems; - collect; from_list; addn;_} -> subset1 + fun x29 -> + match x29 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> + aunion let union : 'e . unit -> ('e, Obj.t) setlike -> Obj.t -> Obj.t -> Obj.t = + fun s -> fun x29 -> __proj__Mksetlike__item__union () x29 +let __proj__Mksetlike__item__inter : + 'e . unit -> ('e, Obj.t) setlike -> Obj.t -> Obj.t -> Obj.t = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty = is_empty1; - add = add1; remove = remove1; mem = mem1; equal = equal1; - subset = subset1; union = union1; inter; diff; for_all; for_any; - elems; collect; from_list; addn;_} -> union1 + fun x30 -> + match x30 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> + ainter let inter : 'e . unit -> ('e, Obj.t) setlike -> Obj.t -> Obj.t -> Obj.t = + fun s -> fun x30 -> __proj__Mksetlike__item__inter () x30 +let __proj__Mksetlike__item__diff : + 'e . unit -> ('e, Obj.t) setlike -> Obj.t -> Obj.t -> Obj.t = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty = is_empty1; - add = add1; remove = remove1; mem = mem1; equal = equal1; - subset = subset1; union = union1; inter = inter1; diff; for_all; - for_any; elems; collect; from_list; addn;_} -> inter1 + fun x31 -> + match x31 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> + adiff let diff : 'e . unit -> ('e, Obj.t) setlike -> Obj.t -> Obj.t -> Obj.t = + fun s -> fun x31 -> __proj__Mksetlike__item__diff () x31 +let __proj__Mksetlike__item__for_all : + 'e . + unit -> ('e, Obj.t) setlike -> ('e -> Prims.bool) -> Obj.t -> Prims.bool + = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty = is_empty1; - add = add1; remove = remove1; mem = mem1; equal = equal1; - subset = subset1; union = union1; inter = inter1; diff = diff1; - for_all; for_any; elems; collect; from_list; addn;_} -> diff1 + fun x32 -> + match x32 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> + afor_all let for_all : + 'e . + unit -> ('e, Obj.t) setlike -> ('e -> Prims.bool) -> Obj.t -> Prims.bool + = fun s -> fun x32 -> __proj__Mksetlike__item__for_all () x32 +let __proj__Mksetlike__item__for_any : 'e . unit -> ('e, Obj.t) setlike -> ('e -> Prims.bool) -> Obj.t -> Prims.bool = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty = is_empty1; - add = add1; remove = remove1; mem = mem1; equal = equal1; - subset = subset1; union = union1; inter = inter1; diff = diff1; - for_all = for_all1; for_any; elems; collect; from_list; addn;_} -> - for_all1 + fun x33 -> + match x33 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> + afor_any let for_any : 'e . unit -> ('e, Obj.t) setlike -> ('e -> Prims.bool) -> Obj.t -> Prims.bool - = + = fun s -> fun x33 -> __proj__Mksetlike__item__for_any () x33 +let __proj__Mksetlike__item__elems : + 'e . unit -> ('e, Obj.t) setlike -> Obj.t -> 'e Prims.list = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty = is_empty1; - add = add1; remove = remove1; mem = mem1; equal = equal1; - subset = subset1; union = union1; inter = inter1; diff = diff1; - for_all = for_all1; for_any = for_any1; elems; collect; from_list; - addn;_} -> for_any1 + fun x34 -> + match x34 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> + aelems let elems : 'e . unit -> ('e, Obj.t) setlike -> Obj.t -> 'e Prims.list = + fun s -> fun x34 -> __proj__Mksetlike__item__elems () x34 +let __proj__Mksetlike__item__collect : + 'e . unit -> ('e, Obj.t) setlike -> ('e -> Obj.t) -> 'e Prims.list -> Obj.t + = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty = is_empty1; - add = add1; remove = remove1; mem = mem1; equal = equal1; - subset = subset1; union = union1; inter = inter1; diff = diff1; - for_all = for_all1; for_any = for_any1; elems = elems1; collect; - from_list; addn;_} -> elems1 + fun x35 -> + match x35 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> + acollect let collect : 'e . unit -> ('e, Obj.t) setlike -> ('e -> Obj.t) -> 'e Prims.list -> Obj.t - = + = fun s -> fun x35 -> __proj__Mksetlike__item__collect () x35 +let __proj__Mksetlike__item__from_list : + 'e . unit -> ('e, Obj.t) setlike -> 'e Prims.list -> Obj.t = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty = is_empty1; - add = add1; remove = remove1; mem = mem1; equal = equal1; - subset = subset1; union = union1; inter = inter1; diff = diff1; - for_all = for_all1; for_any = for_any1; elems = elems1; - collect = collect1; from_list; addn;_} -> collect1 + fun x36 -> + match x36 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> + afrom_list let from_list : 'e . unit -> ('e, Obj.t) setlike -> 'e Prims.list -> Obj.t = + fun s -> fun x36 -> __proj__Mksetlike__item__from_list () x36 +let __proj__Mksetlike__item__addn : + 'e . unit -> ('e, Obj.t) setlike -> 'e Prims.list -> Obj.t -> Obj.t = fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty = is_empty1; - add = add1; remove = remove1; mem = mem1; equal = equal1; - subset = subset1; union = union1; inter = inter1; diff = diff1; - for_all = for_all1; for_any = for_any1; elems = elems1; - collect = collect1; from_list = from_list1; addn;_} -> from_list1 + fun x37 -> + match x37 with + | { empty = aempty; singleton = asingleton; is_empty = ais_empty; + add = aadd; remove = aremove; mem = amem; equal = aequal; + subset = asubset; union = aunion; inter = ainter; diff = adiff; + for_all = afor_all; for_any = afor_any; elems = aelems; + collect = acollect; from_list = afrom_list; addn = aaddn;_} -> + aaddn let addn : 'e . unit -> ('e, Obj.t) setlike -> 'e Prims.list -> Obj.t -> Obj.t = - fun s -> - fun projectee -> - match projectee with - | { empty = empty1; singleton = singleton1; is_empty = is_empty1; - add = add1; remove = remove1; mem = mem1; equal = equal1; - subset = subset1; union = union1; inter = inter1; diff = diff1; - for_all = for_all1; for_any = for_any1; elems = elems1; - collect = collect1; from_list = from_list1; addn = addn1;_} -> - addn1 + fun s -> fun x37 -> __proj__Mksetlike__item__addn () x37 let symdiff : 'e 's . ('e, 's) setlike -> 's -> 's -> 's = fun uu___2 -> fun uu___1 -> diff --git a/ocaml/fstar-lib/generated/FStar_Class_Show.ml b/ocaml/fstar-lib/generated/FStar_Class_Show.ml index d79429eca09..2e6801eb5d5 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Show.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Show.ml @@ -2,9 +2,9 @@ open Prims type 'a showable = { show: 'a -> Prims.string } let __proj__Mkshowable__item__show : 'a . 'a showable -> 'a -> Prims.string = - fun projectee -> match projectee with | { show;_} -> show + fun x3 -> match x3 with | { show = ashow;_} -> ashow let show : 'a . 'a showable -> 'a -> Prims.string = - fun projectee -> match projectee with | { show = show1;_} -> show1 + fun x3 -> __proj__Mkshowable__item__show x3 let printableshow : 'a . 'a FStar_Class_Printable.printable -> 'a showable = fun uu___ -> { show = (FStar_Class_Printable.to_string uu___) } let show_list : 'a . 'a showable -> 'a Prims.list showable = diff --git a/ocaml/fstar-lib/generated/FStar_Class_TotalOrder_Raw.ml b/ocaml/fstar-lib/generated/FStar_Class_TotalOrder_Raw.ml index f7f7f7b778c..b5d761cab70 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_TotalOrder_Raw.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_TotalOrder_Raw.ml @@ -10,9 +10,9 @@ type 'a totalorder = { compare: 'a raw_comparator } let __proj__Mktotalorder__item__compare : 'a . 'a totalorder -> 'a raw_comparator = - fun projectee -> match projectee with | { compare;_} -> compare + fun x3 -> match x3 with | { compare = acompare;_} -> acompare let compare : 'a . 'a totalorder -> 'a raw_comparator = - fun projectee -> match projectee with | { compare = compare1;_} -> compare1 + fun x3 -> __proj__Mktotalorder__item__compare x3 let op_Less : 't . 't totalorder -> 't -> 't -> Prims.bool = fun uu___ -> fun x -> fun y -> (compare uu___ x y) = FStar_Order.Lt let op_Greater : 't . 't totalorder -> 't -> 't -> Prims.bool = diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml index e2fd958dd2e..74bc7114fb9 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml @@ -512,8 +512,6 @@ let (meta_projectors_attr : FStar_Ident.lid) = fstar_tactics_lid' ["MkProjectors"; "meta_projectors"] let (mk_projs_lid : FStar_Ident.lid) = fstar_tactics_lid' ["MkProjectors"; "mk_projs"] -let (mk_class_lid : FStar_Ident.lid) = - fstar_tactics_lid' ["Typeclasses"; "mk_class"] let (tcresolve_lid : FStar_Ident.lid) = fstar_tactics_lid' ["Typeclasses"; "tcresolve"] let (tcclass_lid : FStar_Ident.lid) = diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml index 34d4616195b..87f9fe42a1e 100644 --- a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml +++ b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml @@ -1361,8 +1361,10 @@ let (collect_one : | FStar_Parser_AST.Tycon (uu___1, tc, ts) -> (if tc then - add_to_parsing_data - (P_lid FStar_Parser_Const.tcclass_lid) + (add_to_parsing_data + (P_lid FStar_Parser_Const.tcclass_lid); + add_to_parsing_data + (P_lid FStar_Parser_Const.mk_projs_lid)) else (); FStar_Compiler_List.iter collect_tycon ts) | FStar_Parser_AST.Exception (uu___1, t) -> @@ -1485,7 +1487,9 @@ let (collect_one : collect_term t | FStar_Pervasives_Native.Some (FStar_Parser_AST.TypeClassArg) -> - add_to_parsing_data (P_lid FStar_Parser_Const.tcresolve_lid) + (add_to_parsing_data + (P_lid FStar_Parser_Const.tcresolve_lid); + add_to_parsing_data (P_lid FStar_Parser_Const.mk_projs_lid)) | uu___2 -> () and collect_term t = collect_term' t.FStar_Parser_AST.tm and collect_constant uu___1 = diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings_Base.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings_Base.ml index d1533f4bcda..58b0d069577 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings_Base.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings_Base.ml @@ -42,42 +42,43 @@ type 'a embedding = typ: unit -> FStar_Syntax_Syntax.typ ; e_typ: unit -> FStar_Syntax_Syntax.emb_typ } let __proj__Mkembedding__item__em : 'a . 'a embedding -> 'a -> embed_t = - fun projectee -> - match projectee with | { em; un; print; typ; e_typ;_} -> em + fun x7 -> + match x7 with + | { em = aem; un = aun; print = aprint; typ = atyp; e_typ = ae_typ;_} -> + aem +let em : 'a . 'a embedding -> 'a -> embed_t = + fun x7 -> __proj__Mkembedding__item__em x7 let __proj__Mkembedding__item__un : 'a . 'a embedding -> FStar_Syntax_Syntax.term -> 'a unembed_t = - fun projectee -> - match projectee with | { em; un; print; typ; e_typ;_} -> un + fun x8 -> + match x8 with + | { em = aem; un = aun; print = aprint; typ = atyp; e_typ = ae_typ;_} -> + aun +let un : 'a . 'a embedding -> FStar_Syntax_Syntax.term -> 'a unembed_t = + fun x8 -> __proj__Mkembedding__item__un x8 let __proj__Mkembedding__item__print : 'a . 'a embedding -> 'a printer = - fun projectee -> - match projectee with | { em; un; print; typ; e_typ;_} -> print + fun x9 -> + match x9 with + | { em = aem; un = aun; print = aprint; typ = atyp; e_typ = ae_typ;_} -> + aprint +let print : 'a . 'a embedding -> 'a printer = + fun x9 -> __proj__Mkembedding__item__print x9 let __proj__Mkembedding__item__typ : 'a . 'a embedding -> unit -> FStar_Syntax_Syntax.typ = - fun projectee -> - match projectee with | { em; un; print; typ; e_typ;_} -> typ + fun x10 -> + match x10 with + | { em = aem; un = aun; print = aprint; typ = atyp; e_typ = ae_typ;_} -> + atyp +let typ : 'a . 'a embedding -> unit -> FStar_Syntax_Syntax.typ = + fun x10 -> __proj__Mkembedding__item__typ x10 let __proj__Mkembedding__item__e_typ : 'a . 'a embedding -> unit -> FStar_Syntax_Syntax.emb_typ = - fun projectee -> - match projectee with | { em; un; print; typ; e_typ;_} -> e_typ -let em : 'a . 'a embedding -> 'a -> embed_t = - fun projectee -> - match projectee with | { em = em1; un; print; typ; e_typ;_} -> em1 -let un : 'a . 'a embedding -> FStar_Syntax_Syntax.term -> 'a unembed_t = - fun projectee -> - match projectee with | { em = em1; un = un1; print; typ; e_typ;_} -> un1 -let print : 'a . 'a embedding -> 'a printer = - fun projectee -> - match projectee with - | { em = em1; un = un1; print = print1; typ; e_typ;_} -> print1 -let typ : 'a . 'a embedding -> unit -> FStar_Syntax_Syntax.typ = - fun projectee -> - match projectee with - | { em = em1; un = un1; print = print1; typ = typ1; e_typ;_} -> typ1 + fun x11 -> + match x11 with + | { em = aem; un = aun; print = aprint; typ = atyp; e_typ = ae_typ;_} -> + ae_typ let e_typ : 'a . 'a embedding -> unit -> FStar_Syntax_Syntax.emb_typ = - fun projectee -> - match projectee with - | { em = em1; un = un1; print = print1; typ = typ1; e_typ = e_typ1;_} -> - e_typ1 + fun x11 -> __proj__Mkembedding__item__e_typ x11 let emb_typ_of : 'a . 'a embedding -> unit -> FStar_Syntax_Syntax.emb_typ = fun e -> fun uu___ -> e.e_typ () let unknown_printer : 'a . FStar_Syntax_Syntax.term -> 'a -> Prims.string = diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_VisitM.ml b/ocaml/fstar-lib/generated/FStar_Syntax_VisitM.ml index 578ec5d8795..1fe2138f666 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_VisitM.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_VisitM.ml @@ -13,113 +13,94 @@ type 'm lvm = proc_quotes: Prims.bool } let __proj__Mklvm__item__lvm_monad : 'm . 'm lvm -> 'm FStar_Class_Monad.monad = - fun projectee -> - match projectee with - | { lvm_monad; f_term; f_binder; f_binding_bv; f_br; f_comp; - f_residual_comp; f_univ; proc_quotes;_} -> lvm_monad + fun x11 -> + match x11 with + | { lvm_monad = alvm_monad; f_term = af_term; f_binder = af_binder; + f_binding_bv = af_binding_bv; f_br = af_br; f_comp = af_comp; + f_residual_comp = af_residual_comp; f_univ = af_univ; + proc_quotes = aproc_quotes;_} -> alvm_monad +let lvm_monad : 'm . 'm lvm -> 'm FStar_Class_Monad.monad = + fun x11 -> __proj__Mklvm__item__lvm_monad x11 let __proj__Mklvm__item__f_term : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.term) endo = - fun projectee -> - match projectee with - | { lvm_monad; f_term; f_binder; f_binding_bv; f_br; f_comp; - f_residual_comp; f_univ; proc_quotes;_} -> f_term + fun x12 -> + match x12 with + | { lvm_monad = alvm_monad; f_term = af_term; f_binder = af_binder; + f_binding_bv = af_binding_bv; f_br = af_br; f_comp = af_comp; + f_residual_comp = af_residual_comp; f_univ = af_univ; + proc_quotes = aproc_quotes;_} -> af_term +let f_term : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.term) endo = + fun x12 -> __proj__Mklvm__item__f_term x12 let __proj__Mklvm__item__f_binder : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.binder) endo = - fun projectee -> - match projectee with - | { lvm_monad; f_term; f_binder; f_binding_bv; f_br; f_comp; - f_residual_comp; f_univ; proc_quotes;_} -> f_binder + fun x13 -> + match x13 with + | { lvm_monad = alvm_monad; f_term = af_term; f_binder = af_binder; + f_binding_bv = af_binding_bv; f_br = af_br; f_comp = af_comp; + f_residual_comp = af_residual_comp; f_univ = af_univ; + proc_quotes = aproc_quotes;_} -> af_binder +let f_binder : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.binder) endo = + fun x13 -> __proj__Mklvm__item__f_binder x13 let __proj__Mklvm__item__f_binding_bv : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.bv) endo = - fun projectee -> - match projectee with - | { lvm_monad; f_term; f_binder; f_binding_bv; f_br; f_comp; - f_residual_comp; f_univ; proc_quotes;_} -> f_binding_bv + fun x14 -> + match x14 with + | { lvm_monad = alvm_monad; f_term = af_term; f_binder = af_binder; + f_binding_bv = af_binding_bv; f_br = af_br; f_comp = af_comp; + f_residual_comp = af_residual_comp; f_univ = af_univ; + proc_quotes = aproc_quotes;_} -> af_binding_bv +let f_binding_bv : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.bv) endo = + fun x14 -> __proj__Mklvm__item__f_binding_bv x14 let __proj__Mklvm__item__f_br : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.branch) endo = - fun projectee -> - match projectee with - | { lvm_monad; f_term; f_binder; f_binding_bv; f_br; f_comp; - f_residual_comp; f_univ; proc_quotes;_} -> f_br + fun x15 -> + match x15 with + | { lvm_monad = alvm_monad; f_term = af_term; f_binder = af_binder; + f_binding_bv = af_binding_bv; f_br = af_br; f_comp = af_comp; + f_residual_comp = af_residual_comp; f_univ = af_univ; + proc_quotes = aproc_quotes;_} -> af_br +let f_br : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.branch) endo = + fun x15 -> __proj__Mklvm__item__f_br x15 let __proj__Mklvm__item__f_comp : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.comp) endo = - fun projectee -> - match projectee with - | { lvm_monad; f_term; f_binder; f_binding_bv; f_br; f_comp; - f_residual_comp; f_univ; proc_quotes;_} -> f_comp + fun x16 -> + match x16 with + | { lvm_monad = alvm_monad; f_term = af_term; f_binder = af_binder; + f_binding_bv = af_binding_bv; f_br = af_br; f_comp = af_comp; + f_residual_comp = af_residual_comp; f_univ = af_univ; + proc_quotes = aproc_quotes;_} -> af_comp +let f_comp : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.comp) endo = + fun x16 -> __proj__Mklvm__item__f_comp x16 let __proj__Mklvm__item__f_residual_comp : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.residual_comp) endo = - fun projectee -> - match projectee with - | { lvm_monad; f_term; f_binder; f_binding_bv; f_br; f_comp; - f_residual_comp; f_univ; proc_quotes;_} -> f_residual_comp -let __proj__Mklvm__item__f_univ : - 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.universe) endo = - fun projectee -> - match projectee with - | { lvm_monad; f_term; f_binder; f_binding_bv; f_br; f_comp; - f_residual_comp; f_univ; proc_quotes;_} -> f_univ -let __proj__Mklvm__item__proc_quotes : 'm . 'm lvm -> Prims.bool = - fun projectee -> - match projectee with - | { lvm_monad; f_term; f_binder; f_binding_bv; f_br; f_comp; - f_residual_comp; f_univ; proc_quotes;_} -> proc_quotes -let lvm_monad : 'm . 'm lvm -> 'm FStar_Class_Monad.monad = - fun projectee -> - match projectee with - | { lvm_monad = lvm_monad1; f_term; f_binder; f_binding_bv; f_br; - f_comp; f_residual_comp; f_univ; proc_quotes;_} -> lvm_monad1 -let f_term : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.term) endo = - fun projectee -> - match projectee with - | { lvm_monad = lvm_monad1; f_term = f_term1; f_binder; f_binding_bv; - f_br; f_comp; f_residual_comp; f_univ; proc_quotes;_} -> f_term1 -let f_binder : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.binder) endo = - fun projectee -> - match projectee with - | { lvm_monad = lvm_monad1; f_term = f_term1; f_binder = f_binder1; - f_binding_bv; f_br; f_comp; f_residual_comp; f_univ; proc_quotes;_} - -> f_binder1 -let f_binding_bv : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.bv) endo = - fun projectee -> - match projectee with - | { lvm_monad = lvm_monad1; f_term = f_term1; f_binder = f_binder1; - f_binding_bv = f_binding_bv1; f_br; f_comp; f_residual_comp; - f_univ; proc_quotes;_} -> f_binding_bv1 -let f_br : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.branch) endo = - fun projectee -> - match projectee with - | { lvm_monad = lvm_monad1; f_term = f_term1; f_binder = f_binder1; - f_binding_bv = f_binding_bv1; f_br = f_br1; f_comp; f_residual_comp; - f_univ; proc_quotes;_} -> f_br1 -let f_comp : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.comp) endo = - fun projectee -> - match projectee with - | { lvm_monad = lvm_monad1; f_term = f_term1; f_binder = f_binder1; - f_binding_bv = f_binding_bv1; f_br = f_br1; f_comp = f_comp1; - f_residual_comp; f_univ; proc_quotes;_} -> f_comp1 + fun x17 -> + match x17 with + | { lvm_monad = alvm_monad; f_term = af_term; f_binder = af_binder; + f_binding_bv = af_binding_bv; f_br = af_br; f_comp = af_comp; + f_residual_comp = af_residual_comp; f_univ = af_univ; + proc_quotes = aproc_quotes;_} -> af_residual_comp let f_residual_comp : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.residual_comp) endo = - fun projectee -> - match projectee with - | { lvm_monad = lvm_monad1; f_term = f_term1; f_binder = f_binder1; - f_binding_bv = f_binding_bv1; f_br = f_br1; f_comp = f_comp1; - f_residual_comp = f_residual_comp1; f_univ; proc_quotes;_} -> - f_residual_comp1 + fun x17 -> __proj__Mklvm__item__f_residual_comp x17 +let __proj__Mklvm__item__f_univ : + 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.universe) endo = + fun x18 -> + match x18 with + | { lvm_monad = alvm_monad; f_term = af_term; f_binder = af_binder; + f_binding_bv = af_binding_bv; f_br = af_br; f_comp = af_comp; + f_residual_comp = af_residual_comp; f_univ = af_univ; + proc_quotes = aproc_quotes;_} -> af_univ let f_univ : 'm . 'm lvm -> ('m, FStar_Syntax_Syntax.universe) endo = - fun projectee -> - match projectee with - | { lvm_monad = lvm_monad1; f_term = f_term1; f_binder = f_binder1; - f_binding_bv = f_binding_bv1; f_br = f_br1; f_comp = f_comp1; - f_residual_comp = f_residual_comp1; f_univ = f_univ1; proc_quotes;_} - -> f_univ1 + fun x18 -> __proj__Mklvm__item__f_univ x18 +let __proj__Mklvm__item__proc_quotes : 'm . 'm lvm -> Prims.bool = + fun x19 -> + match x19 with + | { lvm_monad = alvm_monad; f_term = af_term; f_binder = af_binder; + f_binding_bv = af_binding_bv; f_br = af_br; f_comp = af_comp; + f_residual_comp = af_residual_comp; f_univ = af_univ; + proc_quotes = aproc_quotes;_} -> aproc_quotes let proc_quotes : 'm . 'm lvm -> Prims.bool = - fun projectee -> - match projectee with - | { lvm_monad = lvm_monad1; f_term = f_term1; f_binder = f_binder1; - f_binding_bv = f_binding_bv1; f_br = f_br1; f_comp = f_comp1; - f_residual_comp = f_residual_comp1; f_univ = f_univ1; - proc_quotes = proc_quotes1;_} -> proc_quotes1 + fun x19 -> __proj__Mklvm__item__proc_quotes x19 let _lvm_monad : 'm . 'm lvm -> 'm FStar_Class_Monad.monad = fun uu___ -> lvm_monad uu___ let novfs : 'm . 'm FStar_Class_Monad.monad -> 'm lvm = diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_MApply.ml b/ocaml/fstar-lib/generated/FStar_Tactics_MApply.ml index 155b6a55ce8..cfbda56a6b3 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_MApply.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_MApply.ml @@ -8,14 +8,13 @@ let __proj__Mktermable__item__to_term : 'a termable -> 'a -> (FStar_Tactics_NamedView.term, unit) FStar_Tactics_Effect.tac_repr - = fun projectee -> match projectee with | { to_term;_} -> to_term + = fun x3 -> match x3 with | { to_term = ato_term;_} -> ato_term let to_term : 'a . 'a termable -> 'a -> (FStar_Tactics_NamedView.term, unit) FStar_Tactics_Effect.tac_repr - = - fun projectee -> match projectee with | { to_term = to_term1;_} -> to_term1 + = fun x3 -> __proj__Mktermable__item__to_term x3 let (termable_term : FStar_Tactics_NamedView.term termable) = { to_term = diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml b/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml index 78bdf02c17b..f38fcfe0f84 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_MkProjectors.ml @@ -633,203 +633,213 @@ let (embed_string : Prims.string -> FStar_Tactics_NamedView.term) = FStar_Reflection_V2_Builtins.pack_ln (FStar_Reflection_V2_Data.Tv_Const (FStar_Reflection_V2_Data.C_String s)) +let (substitute_attr : FStar_Tactics_NamedView.term) = + FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_FVar + (FStar_Reflection_V2_Builtins.pack_fv + ["FStar"; "Pervasives"; "Substitute"])) let (mk_proj_decl : Prims.bool -> - FStar_Reflection_Types.name -> - Prims.string Prims.list -> - FStar_Tactics_NamedView.univ_name Prims.list -> - FStar_Tactics_NamedView.binder Prims.list -> - Prims.nat -> - FStar_Tactics_NamedView.binder -> - FStar_Tactics_NamedView.term -> - (FStar_Tactics_NamedView.namedv * - FStar_Reflection_Types.fv) Prims.list -> - ((FStar_Reflection_Types.sigelt Prims.list * - FStar_Reflection_Types.fv), - unit) FStar_Tactics_Effect.tac_repr) + FStar_Tactics_NamedView.term Prims.list -> + FStar_Reflection_V2_Data.qualifier Prims.list -> + FStar_Reflection_Types.name -> + Prims.string Prims.list -> + FStar_Tactics_NamedView.univ_name Prims.list -> + FStar_Tactics_NamedView.binder Prims.list -> + Prims.nat -> + FStar_Tactics_NamedView.binder -> + FStar_Tactics_NamedView.term -> + (FStar_Tactics_NamedView.namedv * + FStar_Reflection_Types.fv) Prims.list -> + ((FStar_Reflection_Types.sigelt Prims.list * + FStar_Reflection_Types.fv), + unit) FStar_Tactics_Effect.tac_repr) = fun is_method -> - fun tyqn -> - fun ctorname -> - fun univs -> - fun params -> - fun idx -> - fun field -> - fun unfold_names_tm -> - fun smap -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (107)) (Prims.of_int (2)) - (Prims.of_int (107)) (Prims.of_int (61))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (108)) (Prims.of_int (2)) - (Prims.of_int (190)) (Prims.of_int (35))))) - (Obj.magic - (debug - (fun uu___ -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (107)) - (Prims.of_int (41)) - (Prims.of_int (107)) - (Prims.of_int (60))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "prims.fst" - (Prims.of_int (590)) - (Prims.of_int (19)) - (Prims.of_int (590)) - (Prims.of_int (31))))) - (Obj.magic - (FStar_Tactics_Unseal.unseal - field.FStar_Tactics_NamedView.ppname)) - (fun uu___1 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - Prims.strcat "Processing field " - uu___1))))) - (fun uu___ -> - (fun uu___ -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (108)) - (Prims.of_int (2)) - (Prims.of_int (108)) - (Prims.of_int (62))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (108)) - (Prims.of_int (63)) - (Prims.of_int (190)) - (Prims.of_int (35))))) - (Obj.magic - (debug - (fun uu___1 -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (108)) - (Prims.of_int (36)) - (Prims.of_int (108)) - (Prims.of_int (61))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "prims.fst" - (Prims.of_int (590)) - (Prims.of_int (19)) - (Prims.of_int (590)) - (Prims.of_int (31))))) - (Obj.magic - (FStar_Tactics_V2_Builtins.term_to_string - field.FStar_Tactics_NamedView.sort)) - (fun uu___2 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___3 -> - Prims.strcat - "Field typ = " uu___2))))) - (fun uu___1 -> - (fun uu___1 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (109)) - (Prims.of_int (11)) - (Prims.of_int (109)) - (Prims.of_int (24))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (109)) - (Prims.of_int (27)) - (Prims.of_int (190)) - (Prims.of_int (35))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - FStar_List_Tot_Base.length - params)) - (fun uu___2 -> - (fun np -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (110)) - (Prims.of_int (13)) - (Prims.of_int (110)) - (Prims.of_int (25))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (110)) - (Prims.of_int (28)) - (Prims.of_int (190)) - (Prims.of_int (35))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - FStar_Reflection_V2_Builtins.pack_fv - tyqn)) - (fun uu___2 -> - (fun tyfv -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + fun attrs -> + fun quals -> + fun tyqn -> + fun ctorname -> + fun univs -> + fun params -> + fun idx -> + fun field -> + fun unfold_names_tm -> + fun smap -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (115)) (Prims.of_int (2)) + (Prims.of_int (115)) (Prims.of_int (61))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (116)) (Prims.of_int (2)) + (Prims.of_int (205)) (Prims.of_int (35))))) + (Obj.magic + (debug + (fun uu___ -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (115)) + (Prims.of_int (41)) + (Prims.of_int (115)) + (Prims.of_int (60))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "prims.fst" + (Prims.of_int (590)) + (Prims.of_int (19)) + (Prims.of_int (590)) + (Prims.of_int (31))))) + (Obj.magic + (FStar_Tactics_Unseal.unseal + field.FStar_Tactics_NamedView.ppname)) + (fun uu___1 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> + Prims.strcat "Processing field " + uu___1))))) + (fun uu___ -> + (fun uu___ -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (116)) + (Prims.of_int (2)) + (Prims.of_int (116)) + (Prims.of_int (62))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (116)) + (Prims.of_int (63)) + (Prims.of_int (205)) + (Prims.of_int (35))))) + (Obj.magic + (debug + (fun uu___1 -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (116)) + (Prims.of_int (36)) + (Prims.of_int (116)) + (Prims.of_int (61))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "prims.fst" + (Prims.of_int (590)) + (Prims.of_int (19)) + (Prims.of_int (590)) + (Prims.of_int (31))))) + (Obj.magic + (FStar_Tactics_V2_Builtins.term_to_string + field.FStar_Tactics_NamedView.sort)) + (fun uu___2 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___3 -> + Prims.strcat + "Field typ = " + uu___2))))) + (fun uu___1 -> + (fun uu___1 -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (117)) + (Prims.of_int (11)) + (Prims.of_int (117)) + (Prims.of_int (24))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (117)) + (Prims.of_int (27)) + (Prims.of_int (205)) + (Prims.of_int (35))))) + (FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> + FStar_List_Tot_Base.length + params)) + (fun uu___2 -> + (fun np -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (118)) + (Prims.of_int (13)) + (Prims.of_int (118)) + (Prims.of_int (25))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (118)) + (Prims.of_int (28)) + (Prims.of_int (205)) + (Prims.of_int (35))))) + (FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> + FStar_Reflection_V2_Builtins.pack_fv + tyqn)) + (fun uu___2 -> + (fun tyfv -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (119)) (Prims.of_int (18)) - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (102))))) - (FStar_Sealed.seal + (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (105)) - (Prims.of_int (190)) + (Prims.of_int (205)) (Prims.of_int (35))))) - (Obj.magic + (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (18)) - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (31))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (18)) - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (102))))) (Obj.magic (FStar_Tactics_V2_Derived.cur_module @@ -844,17 +854,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (34)) - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (102))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (18)) - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (102))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -862,17 +872,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (35)) - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (101))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (34)) - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (102))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -880,9 +890,9 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (48)) - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (101))))) (FStar_Sealed.seal (Obj.magic @@ -898,17 +908,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (48)) - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (66))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (48)) - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (101))))) (Obj.magic (list_last @@ -923,9 +933,9 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (69)) - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (101))))) (FStar_Sealed.seal (Obj.magic @@ -941,9 +951,9 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (82)) - (Prims.of_int (111)) + (Prims.of_int (119)) (Prims.of_int (101))))) (FStar_Sealed.seal (Obj.magic @@ -996,8 +1006,8 @@ let (mk_proj_decl : uu___2 uu___3)))) uu___2))) - (fun uu___2 - -> + (fun + uu___2 -> (fun nm -> Obj.magic @@ -1006,17 +1016,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (112)) + (Prims.of_int (120)) (Prims.of_int (11)) - (Prims.of_int (112)) + (Prims.of_int (120)) (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (112)) + (Prims.of_int (120)) (Prims.of_int (24)) - (Prims.of_int (190)) + (Prims.of_int (205)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1033,17 +1043,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (113)) + (Prims.of_int (121)) (Prims.of_int (18)) - (Prims.of_int (115)) + (Prims.of_int (123)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (116)) + (Prims.of_int (124)) (Prims.of_int (4)) - (Prims.of_int (190)) + (Prims.of_int (205)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1072,17 +1082,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (117)) + (Prims.of_int (125)) (Prims.of_int (20)) - (Prims.of_int (117)) + (Prims.of_int (125)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (117)) + (Prims.of_int (125)) (Prims.of_int (39)) - (Prims.of_int (190)) + (Prims.of_int (205)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_Derived.fresh_binder @@ -1097,17 +1107,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (126)) (Prims.of_int (15)) - (Prims.of_int (120)) + (Prims.of_int (128)) (Prims.of_int (73))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (122)) + (Prims.of_int (130)) (Prims.of_int (2)) - (Prims.of_int (190)) + (Prims.of_int (205)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1115,17 +1125,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (120)) + (Prims.of_int (128)) (Prims.of_int (26)) - (Prims.of_int (120)) + (Prims.of_int (128)) (Prims.of_int (73))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (118)) + (Prims.of_int (126)) (Prims.of_int (15)) - (Prims.of_int (120)) + (Prims.of_int (128)) (Prims.of_int (73))))) (Obj.magic (subst_map @@ -1156,17 +1166,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (122)) + (Prims.of_int (130)) (Prims.of_int (2)) - (Prims.of_int (122)) + (Prims.of_int (130)) (Prims.of_int (57))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (122)) + (Prims.of_int (130)) (Prims.of_int (58)) - (Prims.of_int (190)) + (Prims.of_int (205)) (Prims.of_int (35))))) (Obj.magic (debug @@ -1177,9 +1187,9 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (122)) + (Prims.of_int (130)) (Prims.of_int (35)) - (Prims.of_int (122)) + (Prims.of_int (130)) (Prims.of_int (56))))) (FStar_Sealed.seal (Obj.magic @@ -1210,17 +1220,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (123)) + (Prims.of_int (131)) (Prims.of_int (16)) - (Prims.of_int (137)) + (Prims.of_int (145)) (Prims.of_int (7))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (138)) + (Prims.of_int (146)) (Prims.of_int (4)) - (Prims.of_int (190)) + (Prims.of_int (205)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_NamedView.pack_sigelt @@ -1302,17 +1312,58 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (140)) + (Prims.of_int (147)) + (Prims.of_int (21)) + (Prims.of_int (147)) + (Prims.of_int (90))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (147)) + (Prims.of_int (93)) + (Prims.of_int (205)) + (Prims.of_int (35))))) + (FStar_Tactics_Effect.lift_div_tac + (fun + uu___3 -> + FStar_List_Tot_Base.filter + (fun + uu___4 -> + match uu___4 + with + | + FStar_Reflection_V2_Data.RecordType + uu___5 -> + false + | + FStar_Reflection_V2_Data.Noeq + -> false + | + uu___5 -> + true))) + (fun + uu___3 -> + (fun + filter_quals + -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (149)) (Prims.of_int (4)) - (Prims.of_int (173)) + (Prims.of_int (187)) (Prims.of_int (8))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (190)) + (Prims.of_int (205)) (Prims.of_int (2)) - (Prims.of_int (190)) + (Prims.of_int (205)) (Prims.of_int (35))))) (if Prims.op_Negation @@ -1351,17 +1402,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (18)) - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (65))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (68)) - (Prims.of_int (173)) + (Prims.of_int (187)) (Prims.of_int (8))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1369,17 +1420,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (26)) - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (65))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (18)) - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (65))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1387,17 +1438,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (27)) - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (40))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (26)) - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (65))))) (Obj.magic (FStar_Tactics_V2_Derived.cur_module @@ -1412,17 +1463,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (43)) - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (64))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (26)) - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (65))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1430,17 +1481,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (44)) - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (63))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (43)) - (Prims.of_int (142)) + (Prims.of_int (151)) (Prims.of_int (64))))) (Obj.magic (FStar_Tactics_Unseal.unseal @@ -1478,17 +1529,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (143)) + (Prims.of_int (152)) (Prims.of_int (15)) - (Prims.of_int (143)) + (Prims.of_int (152)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (143)) + (Prims.of_int (152)) (Prims.of_int (66)) - (Prims.of_int (173)) + (Prims.of_int (187)) (Prims.of_int (8))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1527,17 +1578,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (144)) + (Prims.of_int (153)) (Prims.of_int (17)) - (Prims.of_int (146)) + (Prims.of_int (155)) (Prims.of_int (75))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (147)) + (Prims.of_int (156)) (Prims.of_int (6)) - (Prims.of_int (173)) + (Prims.of_int (187)) (Prims.of_int (8))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1545,17 +1596,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (146)) + (Prims.of_int (155)) (Prims.of_int (28)) - (Prims.of_int (146)) + (Prims.of_int (155)) (Prims.of_int (75))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (144)) + (Prims.of_int (153)) (Prims.of_int (17)) - (Prims.of_int (146)) + (Prims.of_int (155)) (Prims.of_int (75))))) (Obj.magic (subst_map @@ -1587,17 +1638,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (150)) + (Prims.of_int (159)) (Prims.of_int (6)) - (Prims.of_int (152)) - (Prims.of_int (38))))) + (Prims.of_int (172)) + (Prims.of_int (41))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (166)) - (Prims.of_int (4)) (Prims.of_int (173)) + (Prims.of_int (6)) + (Prims.of_int (187)) (Prims.of_int (8))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1658,17 +1709,17 @@ let (mk_proj_decl : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (166)) - (Prims.of_int (5)) - (Prims.of_int (173)) - (Prims.of_int (7))))) + (Prims.of_int (176)) + (Prims.of_int (13)) + (Prims.of_int (183)) + (Prims.of_int (9))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (166)) + (Prims.of_int (187)) (Prims.of_int (4)) - (Prims.of_int (173)) + (Prims.of_int (187)) (Prims.of_int (8))))) (Obj.magic (FStar_Tactics_NamedView.pack_sigelt @@ -1690,12 +1741,35 @@ let (mk_proj_decl : = lb_def }] }))) - (fun - uu___5 -> + (fun se + -> FStar_Tactics_Effect.lift_div_tac (fun - uu___6 -> - [uu___5])))) + uu___5 -> + [ + FStar_Reflection_V2_Builtins.set_sigelt_quals + (FStar_List_Tot_Base.op_At + (filter_quals + quals) + (FStar_Reflection_V2_Builtins.sigelt_quals + (FStar_Reflection_V2_Builtins.set_sigelt_attrs + (FStar_List_Tot_Base.op_At + (substitute_attr + :: + (field.FStar_Tactics_NamedView.attrs)) + (FStar_List_Tot_Base.op_At + attrs + (FStar_Reflection_V2_Builtins.sigelt_attrs + se))) se))) + (FStar_Reflection_V2_Builtins.set_sigelt_attrs + (FStar_List_Tot_Base.op_At + (substitute_attr + :: + (field.FStar_Tactics_NamedView.attrs)) + (FStar_List_Tot_Base.op_At + attrs + (FStar_Reflection_V2_Builtins.sigelt_attrs + se))) se)])))) uu___5))) uu___5))) uu___5))) @@ -1707,24 +1781,45 @@ let (mk_proj_decl : (fun uu___3 -> ((( - FStar_Reflection_V2_Builtins.set_sigelt_attrs + FStar_Reflection_V2_Builtins.set_sigelt_quals (FStar_List_Tot_Base.op_At - field.FStar_Tactics_NamedView.attrs + (filter_quals + quals) + (FStar_Reflection_V2_Builtins.sigelt_quals + (FStar_Reflection_V2_Builtins.set_sigelt_attrs + (FStar_List_Tot_Base.op_At + (substitute_attr + :: + (field.FStar_Tactics_NamedView.attrs)) + (FStar_List_Tot_Base.op_At + attrs (FStar_Reflection_V2_Builtins.sigelt_attrs + se_proj))) + se_proj))) + (FStar_Reflection_V2_Builtins.set_sigelt_attrs + (FStar_List_Tot_Base.op_At + (substitute_attr + :: + (field.FStar_Tactics_NamedView.attrs)) + (FStar_List_Tot_Base.op_At + attrs + (FStar_Reflection_V2_Builtins.sigelt_attrs + se_proj))) se_proj)) - se_proj) :: maybe_se_method), fv))))) uu___3))) + uu___3))) uu___2))) uu___2))) uu___2))) uu___2))) uu___2))) uu___2))) - uu___2))) uu___2))) - uu___1))) uu___) + uu___2))) + uu___2))) uu___1))) + uu___) let (mk_projs : Prims.bool -> Prims.string -> @@ -1737,16 +1832,22 @@ let (mk_projs : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (194)) (Prims.of_int (2)) (Prims.of_int (194)) - (Prims.of_int (51))))) + (Prims.of_int (209)) (Prims.of_int (2)) (Prims.of_int (209)) + (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (194)) (Prims.of_int (52)) - (Prims.of_int (224)) (Prims.of_int (29))))) + (Prims.of_int (209)) (Prims.of_int (62)) + (Prims.of_int (241)) (Prims.of_int (29))))) (Obj.magic - (FStar_Tactics_V2_Builtins.print - (Prims.strcat "!! mk_projs tactic called on: " tyname))) + (debug + (fun uu___ -> + (fun uu___ -> + Obj.magic + (FStar_Tactics_Effect.lift_div_tac + (fun uu___1 -> + Prims.strcat "!! mk_projs tactic called on: " + tyname))) uu___))) (fun uu___ -> (fun uu___ -> Obj.magic @@ -1755,14 +1856,14 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (195)) (Prims.of_int (13)) - (Prims.of_int (195)) (Prims.of_int (30))))) + (Prims.of_int (210)) (Prims.of_int (13)) + (Prims.of_int (210)) (Prims.of_int (30))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (196)) (Prims.of_int (2)) - (Prims.of_int (224)) (Prims.of_int (29))))) + (Prims.of_int (211)) (Prims.of_int (2)) + (Prims.of_int (241)) (Prims.of_int (29))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> FStar_Reflection_V2_Builtins.explode_qn tyname)) @@ -1774,17 +1875,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (196)) + (Prims.of_int (211)) (Prims.of_int (8)) - (Prims.of_int (196)) + (Prims.of_int (211)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (196)) + (Prims.of_int (211)) (Prims.of_int (2)) - (Prims.of_int (224)) + (Prims.of_int (241)) (Prims.of_int (29))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1792,17 +1893,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (196)) + (Prims.of_int (211)) (Prims.of_int (19)) - (Prims.of_int (196)) + (Prims.of_int (211)) (Prims.of_int (31))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (196)) + (Prims.of_int (211)) (Prims.of_int (8)) - (Prims.of_int (196)) + (Prims.of_int (211)) (Prims.of_int (36))))) (Obj.magic (FStar_Tactics_V2_Builtins.top_env ())) @@ -1827,70 +1928,122 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (200)) - (Prims.of_int (10)) - (Prims.of_int (200)) - (Prims.of_int (27))))) + (Prims.of_int (215)) + (Prims.of_int (16)) + (Prims.of_int (215)) + (Prims.of_int (31))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (200)) - (Prims.of_int (4)) - (Prims.of_int (224)) + (Prims.of_int (215)) + (Prims.of_int (34)) + (Prims.of_int (241)) (Prims.of_int (29))))) - (Obj.magic - (FStar_Tactics_NamedView.inspect_sigelt - se)) - (fun uu___2 -> + (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> - match uu___2 with - | FStar_Tactics_NamedView.Sg_Inductive - { - FStar_Tactics_NamedView.nm - = nm; - FStar_Tactics_NamedView.univs1 - = univs; - FStar_Tactics_NamedView.params - = params; - FStar_Tactics_NamedView.typ - = typ; - FStar_Tactics_NamedView.ctors - = ctors;_} - -> - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal + FStar_Reflection_V2_Builtins.sigelt_quals + se)) + (fun uu___2 -> + (fun quals -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (216)) + (Prims.of_int (16)) + (Prims.of_int (216)) + (Prims.of_int (31))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (217)) + (Prims.of_int (4)) + (Prims.of_int (241)) + (Prims.of_int (29))))) + (FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> + FStar_Reflection_V2_Builtins.sigelt_attrs + se)) + (fun uu___2 -> + (fun attrs -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (217)) + (Prims.of_int (10)) + (Prims.of_int (217)) + (Prims.of_int (27))))) + (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (202)) + (Prims.of_int (217)) + (Prims.of_int (4)) + (Prims.of_int (241)) + (Prims.of_int (29))))) + (Obj.magic + (FStar_Tactics_NamedView.inspect_sigelt + se)) + (fun + uu___2 -> + (fun + uu___2 -> + match uu___2 + with + | + FStar_Tactics_NamedView.Sg_Inductive + { + FStar_Tactics_NamedView.nm + = nm; + FStar_Tactics_NamedView.univs1 + = univs; + FStar_Tactics_NamedView.params + = params; + FStar_Tactics_NamedView.typ + = typ; + FStar_Tactics_NamedView.ctors + = ctors;_} + -> + Obj.magic + (Obj.repr + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.MkProjectors.fst" + (Prims.of_int (219)) (Prims.of_int (6)) - (Prims.of_int (203)) + (Prims.of_int (220)) (Prims.of_int (57))))) - (FStar_Sealed.seal + (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (203)) + (Prims.of_int (220)) (Prims.of_int (58)) - (Prims.of_int (222)) + (Prims.of_int (239)) (Prims.of_int (11))))) - (if + (if (FStar_List_Tot_Base.length ctors) <> Prims.int_one - then + then FStar_Tactics_V2_Derived.fail "Expected an inductive with one constructor" - else + else FStar_Tactics_Effect.lift_div_tac (fun uu___4 -> ())) - (fun uu___3 - -> + (fun + uu___3 -> (fun uu___3 -> Obj.magic @@ -1899,17 +2052,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (204)) + (Prims.of_int (221)) (Prims.of_int (20)) - (Prims.of_int (204)) + (Prims.of_int (221)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (205)) - (Prims.of_int (6)) (Prims.of_int (222)) + (Prims.of_int (6)) + (Prims.of_int (239)) (Prims.of_int (11))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1917,17 +2070,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (204)) + (Prims.of_int (221)) (Prims.of_int (24)) - (Prims.of_int (204)) + (Prims.of_int (221)) (Prims.of_int (44))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (204)) + (Prims.of_int (221)) (Prims.of_int (20)) - (Prims.of_int (204)) + (Prims.of_int (221)) (Prims.of_int (44))))) (Obj.magic (FStar_Tactics_V2_SyntaxHelpers.collect_arr_bs @@ -1950,17 +2103,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (205)) + (Prims.of_int (222)) (Prims.of_int (6)) - (Prims.of_int (206)) + (Prims.of_int (223)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (206)) + (Prims.of_int (223)) (Prims.of_int (43)) - (Prims.of_int (222)) + (Prims.of_int (239)) (Prims.of_int (11))))) (if Prims.uu___is_Cons @@ -1983,17 +2136,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (207)) + (Prims.of_int (224)) (Prims.of_int (33)) - (Prims.of_int (207)) + (Prims.of_int (224)) (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (206)) + (Prims.of_int (223)) (Prims.of_int (43)) - (Prims.of_int (222)) + (Prims.of_int (239)) (Prims.of_int (11))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2015,17 +2168,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (210)) + (Prims.of_int (227)) (Prims.of_int (24)) - (Prims.of_int (210)) + (Prims.of_int (227)) (Prims.of_int (45))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (207)) + (Prims.of_int (224)) (Prims.of_int (41)) - (Prims.of_int (222)) + (Prims.of_int (239)) (Prims.of_int (11))))) (Obj.magic (FStar_Tactics_V2_SyntaxHelpers.collect_arr_bs @@ -2046,17 +2199,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (211)) + (Prims.of_int (228)) (Prims.of_int (28)) - (Prims.of_int (211)) + (Prims.of_int (228)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (211)) + (Prims.of_int (228)) (Prims.of_int (45)) - (Prims.of_int (222)) + (Prims.of_int (239)) (Prims.of_int (11))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -2085,17 +2238,17 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (213)) + (Prims.of_int (230)) (Prims.of_int (8)) - (Prims.of_int (220)) + (Prims.of_int (237)) (Prims.of_int (14))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (211)) + (Prims.of_int (228)) (Prims.of_int (45)) - (Prims.of_int (222)) + (Prims.of_int (239)) (Prims.of_int (11))))) (Obj.magic (FStar_Tactics_Util.fold_left @@ -2115,21 +2268,23 @@ let (mk_projs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (214)) + (Prims.of_int (231)) (Prims.of_int (25)) - (Prims.of_int (214)) - (Prims.of_int (104))))) + (Prims.of_int (231)) + (Prims.of_int (116))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.MkProjectors.fst" - (Prims.of_int (213)) + (Prims.of_int (230)) (Prims.of_int (78)) - (Prims.of_int (218)) + (Prims.of_int (235)) (Prims.of_int (17))))) (Obj.magic (mk_proj_decl is_class + attrs + quals tyqn ctorname univs @@ -2203,11 +2358,14 @@ let (mk_projs : uu___4))) uu___4))) uu___3))) - | uu___3 -> - Obj.magic - (Obj.repr - (FStar_Tactics_V2_Derived.fail - "not an inductive"))) + | + uu___3 -> + Obj.magic + (Obj.repr + (FStar_Tactics_V2_Derived.fail + "not an inductive"))) + uu___2))) + uu___2))) uu___2)))) uu___1))) uu___1))) uu___) let _ = diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml index 522f4511c02..6d0efe8797b 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml @@ -2323,2127 +2323,4 @@ let _ = (FStar_Tactics_Native.from_tactic_1 tcresolve) FStar_Syntax_Embeddings.e_unit FStar_Syntax_Embeddings.e_unit psc ncb us args) -let rec (mk_abs : - FStar_Tactics_NamedView.binder Prims.list -> - FStar_Tactics_NamedView.term -> - (FStar_Tactics_NamedView.term, unit) FStar_Tactics_Effect.tac_repr) - = - fun uu___1 -> - fun uu___ -> - (fun bs -> - fun body -> - match bs with - | [] -> - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> body))) - | b::bs1 -> - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (318)) (Prims.of_int (20)) - (Prims.of_int (318)) (Prims.of_int (47))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "dummy" Prims.int_zero - Prims.int_zero Prims.int_zero Prims.int_zero))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (318)) - (Prims.of_int (30)) - (Prims.of_int (318)) - (Prims.of_int (46))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (318)) - (Prims.of_int (20)) - (Prims.of_int (318)) - (Prims.of_int (47))))) - (Obj.magic (mk_abs bs1 body)) - (fun uu___ -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___1 -> - FStar_Tactics_NamedView.Tv_Abs - (b, uu___))))) - (fun uu___ -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___1 -> FStar_Tactics_NamedView.pack uu___))))) - uu___1 uu___ -let rec last : 'a . 'a Prims.list -> ('a, unit) FStar_Tactics_Effect.tac_repr - = - fun uu___ -> - (fun l -> - match l with - | [] -> - Obj.magic - (Obj.repr (FStar_Tactics_V2_Derived.fail "last: empty list")) - | x::[] -> - Obj.magic - (Obj.repr (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> x))) - | uu___::xs -> Obj.magic (Obj.repr (last xs))) uu___ -let (filter_no_method_binders : - FStar_Tactics_NamedView.binders -> FStar_Tactics_NamedView.binders) = - fun bs -> - let has_no_method_attr b = - FStar_List_Tot_Base.existsb - (FStar_Reflection_TermEq_Simple.term_eq - (FStar_Reflection_V2_Builtins.pack_ln - (FStar_Reflection_V2_Data.Tv_FVar - (FStar_Reflection_V2_Builtins.pack_fv - ["FStar"; "Tactics"; "Typeclasses"; "no_method"])))) - b.FStar_Tactics_NamedView.attrs in - FStar_List_Tot_Base.filter - (fun b -> Prims.op_Negation (has_no_method_attr b)) bs -let (binder_set_meta : - FStar_Tactics_NamedView.binder -> - FStar_Tactics_NamedView.term -> FStar_Tactics_NamedView.binder) - = - fun b -> - fun t -> - { - FStar_Tactics_NamedView.uniq = (b.FStar_Tactics_NamedView.uniq); - FStar_Tactics_NamedView.ppname = (b.FStar_Tactics_NamedView.ppname); - FStar_Tactics_NamedView.sort = (b.FStar_Tactics_NamedView.sort); - FStar_Tactics_NamedView.qual = (FStar_Reflection_V2_Data.Q_Meta t); - FStar_Tactics_NamedView.attrs = (b.FStar_Tactics_NamedView.attrs) - } -let (mk_class : - Prims.string -> - (FStar_Reflection_Types.decls, unit) FStar_Tactics_Effect.tac_repr) - = - fun nm -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (342)) (Prims.of_int (13)) (Prims.of_int (342)) - (Prims.of_int (26))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (342)) (Prims.of_int (29)) (Prims.of_int (432)) - (Prims.of_int (5))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___ -> FStar_Reflection_V2_Builtins.explode_qn nm)) - (fun uu___ -> - (fun ns -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (343)) (Prims.of_int (12)) - (Prims.of_int (343)) (Prims.of_int (38))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (344)) (Prims.of_int (4)) - (Prims.of_int (432)) (Prims.of_int (5))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (343)) (Prims.of_int (23)) - (Prims.of_int (343)) (Prims.of_int (35))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (343)) (Prims.of_int (12)) - (Prims.of_int (343)) (Prims.of_int (38))))) - (Obj.magic (FStar_Tactics_V2_Builtins.top_env ())) - (fun uu___ -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___1 -> - FStar_Reflection_V2_Builtins.lookup_typ uu___ - ns)))) - (fun uu___ -> - (fun r -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (344)) (Prims.of_int (4)) - (Prims.of_int (344)) (Prims.of_int (19))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (344)) (Prims.of_int (20)) - (Prims.of_int (432)) (Prims.of_int (5))))) - (Obj.magic - (FStar_Tactics_V2_Derived.guard - (FStar_Pervasives_Native.uu___is_Some r))) - (fun uu___ -> - (fun uu___ -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (345)) - (Prims.of_int (18)) - (Prims.of_int (345)) - (Prims.of_int (19))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (344)) - (Prims.of_int (20)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___1 -> r)) - (fun uu___1 -> - (fun uu___1 -> - match uu___1 with - | FStar_Pervasives_Native.Some - se -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (346)) - (Prims.of_int (23)) - (Prims.of_int (346)) - (Prims.of_int (115))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (346)) - (Prims.of_int (118)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - FStar_List_Tot_Base.filter - (fun uu___3 -> - match uu___3 - with - | FStar_Reflection_V2_Data.Inline_for_extraction - -> true - | FStar_Reflection_V2_Data.NoExtract - -> true - | uu___4 -> - false) - (FStar_Reflection_V2_Builtins.sigelt_quals - se))) - (fun uu___2 -> - (fun to_propagate -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - ( - Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (347)) - (Prims.of_int (13)) - (Prims.of_int (347)) - (Prims.of_int (30))))) - (FStar_Sealed.seal - ( - Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (348)) - (Prims.of_int (4)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (Obj.magic - ( - FStar_Tactics_NamedView.inspect_sigelt - se)) - (fun uu___2 - -> - (fun sv - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (348)) - (Prims.of_int (4)) - (Prims.of_int (348)) - (Prims.of_int (28))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (348)) - (Prims.of_int (29)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (Obj.magic - (FStar_Tactics_V2_Derived.guard - (FStar_Tactics_NamedView.uu___is_Sg_Inductive - sv))) - (fun - uu___2 -> - (fun - uu___2 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (349)) - (Prims.of_int (63)) - (Prims.of_int (349)) - (Prims.of_int (65))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (348)) - (Prims.of_int (29)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___3 -> - sv)) - (fun - uu___3 -> - (fun - uu___3 -> - match uu___3 - with - | - FStar_Tactics_NamedView.Sg_Inductive - { - FStar_Tactics_NamedView.nm - = name; - FStar_Tactics_NamedView.univs1 - = us; - FStar_Tactics_NamedView.params - = params; - FStar_Tactics_NamedView.typ - = ity; - FStar_Tactics_NamedView.ctors - = ctors;_} - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (350)) - (Prims.of_int (4)) - (Prims.of_int (350)) - (Prims.of_int (87))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (351)) - (Prims.of_int (4)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (Obj.magic - (debug - (fun - uu___4 -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (350)) - (Prims.of_int (35)) - (Prims.of_int (350)) - (Prims.of_int (86))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "prims.fst" - (Prims.of_int (590)) - (Prims.of_int (19)) - (Prims.of_int (590)) - (Prims.of_int (31))))) - (Obj.magic - (FStar_Tactics_Util.string_of_list - FStar_Tactics_V2_Derived.binder_to_string - params)) - (fun - uu___5 -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___6 -> - Prims.strcat - "params = " - uu___5))))) - (fun - uu___4 -> - (fun - uu___4 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (351)) - (Prims.of_int (4)) - (Prims.of_int (351)) - (Prims.of_int (57))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (352)) - (Prims.of_int (4)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (Obj.magic - (debug - (fun - uu___5 -> - (fun - uu___5 -> - Obj.magic - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___6 -> - Prims.strcat - "got it, name = " - (FStar_Reflection_V2_Builtins.implode_qn - name)))) - uu___5))) - (fun - uu___5 -> - (fun - uu___5 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (352)) - (Prims.of_int (4)) - (Prims.of_int (352)) - (Prims.of_int (59))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (352)) - (Prims.of_int (60)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (Obj.magic - (debug - (fun - uu___6 -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (352)) - (Prims.of_int (40)) - (Prims.of_int (352)) - (Prims.of_int (58))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "prims.fst" - (Prims.of_int (590)) - (Prims.of_int (19)) - (Prims.of_int (590)) - (Prims.of_int (31))))) - (Obj.magic - (FStar_Tactics_V2_Builtins.term_to_string - ity)) - (fun - uu___7 -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___8 -> - Prims.strcat - "got it, ity = " - uu___7))))) - (fun - uu___6 -> - (fun - uu___6 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (353)) - (Prims.of_int (20)) - (Prims.of_int (353)) - (Prims.of_int (29))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (355)) - (Prims.of_int (4)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (Obj.magic - (last - name)) - (fun - uu___7 -> - (fun - ctor_name - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (355)) - (Prims.of_int (4)) - (Prims.of_int (355)) - (Prims.of_int (30))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (355)) - (Prims.of_int (31)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (Obj.magic - (FStar_Tactics_V2_Derived.guard - ((FStar_List_Tot_Base.length - ctors) = - Prims.int_one))) - (fun - uu___7 -> - (fun - uu___7 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (356)) - (Prims.of_int (25)) - (Prims.of_int (356)) - (Prims.of_int (30))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (355)) - (Prims.of_int (31)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___8 -> - ctors)) - (fun - uu___8 -> - (fun - uu___8 -> - match uu___8 - with - | - (c_name, - ty)::[] - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (357)) - (Prims.of_int (4)) - (Prims.of_int (357)) - (Prims.of_int (87))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (357)) - (Prims.of_int (88)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (Obj.magic - (debug - (fun - uu___9 -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (357)) - (Prims.of_int (35)) - (Prims.of_int (357)) - (Prims.of_int (86))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "prims.fst" - (Prims.of_int (590)) - (Prims.of_int (19)) - (Prims.of_int (590)) - (Prims.of_int (31))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (357)) - (Prims.of_int (55)) - (Prims.of_int (357)) - (Prims.of_int (86))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "prims.fst" - (Prims.of_int (590)) - (Prims.of_int (19)) - (Prims.of_int (590)) - (Prims.of_int (31))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (357)) - (Prims.of_int (69)) - (Prims.of_int (357)) - (Prims.of_int (86))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "prims.fst" - (Prims.of_int (590)) - (Prims.of_int (19)) - (Prims.of_int (590)) - (Prims.of_int (31))))) - (Obj.magic - (FStar_Tactics_V2_Builtins.term_to_string - ty)) - (fun - uu___10 - -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___11 - -> - Prims.strcat - " of type " - uu___10)))) - (fun - uu___10 - -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___11 - -> - Prims.strcat - (FStar_Reflection_V2_Builtins.implode_qn - c_name) - uu___10)))) - (fun - uu___10 - -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___11 - -> - Prims.strcat - "got ctor " - uu___10))))) - (fun - uu___9 -> - (fun - uu___9 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (358)) - (Prims.of_int (18)) - (Prims.of_int (358)) - (Prims.of_int (35))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (357)) - (Prims.of_int (88)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (Obj.magic - (FStar_Tactics_V2_SyntaxHelpers.collect_arr_bs - ty)) - (fun - uu___10 - -> - (fun - uu___10 - -> - match uu___10 - with - | - (bs, cod) - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (359)) - (Prims.of_int (12)) - (Prims.of_int (359)) - (Prims.of_int (28))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (360)) - (Prims.of_int (4)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___11 - -> - FStar_Tactics_NamedView.inspect_comp - cod)) - (fun - uu___11 - -> - (fun r1 - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (360)) - (Prims.of_int (4)) - (Prims.of_int (360)) - (Prims.of_int (22))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (360)) - (Prims.of_int (23)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (Obj.magic - (FStar_Tactics_V2_Derived.guard - (FStar_Reflection_V2_Data.uu___is_C_Total - r1))) - (fun - uu___11 - -> - (fun - uu___11 - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (361)) - (Prims.of_int (22)) - (Prims.of_int (361)) - (Prims.of_int (23))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (360)) - (Prims.of_int (23)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___12 - -> r1)) - (fun - uu___12 - -> - (fun - uu___12 - -> - match uu___12 - with - | - FStar_Reflection_V2_Data.C_Total - cod1 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (363)) - (Prims.of_int (4)) - (Prims.of_int (363)) - (Prims.of_int (87))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (364)) - (Prims.of_int (4)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (Obj.magic - (debug - (fun - uu___13 - -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (363)) - (Prims.of_int (35)) - (Prims.of_int (363)) - (Prims.of_int (86))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "prims.fst" - (Prims.of_int (590)) - (Prims.of_int (19)) - (Prims.of_int (590)) - (Prims.of_int (31))))) - (Obj.magic - (FStar_Tactics_Util.string_of_list - FStar_Tactics_V2_Derived.binder_to_string - params)) - (fun - uu___14 - -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___15 - -> - Prims.strcat - "params = " - uu___14))))) - (fun - uu___13 - -> - (fun - uu___13 - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (364)) - (Prims.of_int (4)) - (Prims.of_int (364)) - (Prims.of_int (81))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (365)) - (Prims.of_int (4)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (Obj.magic - (debug - (fun - uu___14 - -> - (fun - uu___14 - -> - Obj.magic - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___15 - -> - Prims.strcat - "n_params = " - (Prims.string_of_int - (FStar_List_Tot_Base.length - params))))) - uu___14))) - (fun - uu___14 - -> - (fun - uu___14 - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (365)) - (Prims.of_int (4)) - (Prims.of_int (365)) - (Prims.of_int (76))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (366)) - (Prims.of_int (4)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (Obj.magic - (debug - (fun - uu___15 - -> - (fun - uu___15 - -> - Obj.magic - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___16 - -> - Prims.strcat - "n_univs = " - (Prims.string_of_int - (FStar_List_Tot_Base.length - us))))) - uu___15))) - (fun - uu___15 - -> - (fun - uu___15 - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (366)) - (Prims.of_int (4)) - (Prims.of_int (366)) - (Prims.of_int (51))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (366)) - (Prims.of_int (52)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (Obj.magic - (debug - (fun - uu___16 - -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (366)) - (Prims.of_int (32)) - (Prims.of_int (366)) - (Prims.of_int (50))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "prims.fst" - (Prims.of_int (590)) - (Prims.of_int (19)) - (Prims.of_int (590)) - (Prims.of_int (31))))) - (Obj.magic - (FStar_Tactics_V2_Builtins.term_to_string - cod1)) - (fun - uu___17 - -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___18 - -> - Prims.strcat - "cod = " - uu___17))))) - (fun - uu___16 - -> - (fun - uu___16 - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (370)) - (Prims.of_int (24)) - (Prims.of_int (370)) - (Prims.of_int (61))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (373)) - (Prims.of_int (4)) - (Prims.of_int (432)) - (Prims.of_int (5))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___17 - -> - Prims.strcat - "__proj__Mk" - (Prims.strcat - ctor_name - "__item__"))) - (fun - uu___17 - -> - (fun base - -> - Obj.magic - (FStar_Tactics_Util.map - (fun b -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (375)) - (Prims.of_int (14)) - (Prims.of_int (375)) - (Prims.of_int (30))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (376)) - (Prims.of_int (6)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (Obj.magic - (FStar_Tactics_V2_Derived.name_of_binder - b)) - (fun - uu___17 - -> - (fun s -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (376)) - (Prims.of_int (6)) - (Prims.of_int (376)) - (Prims.of_int (48))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (376)) - (Prims.of_int (49)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (Obj.magic - (debug - (fun - uu___17 - -> - (fun - uu___17 - -> - Obj.magic - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___18 - -> - Prims.strcat - "processing method " - s))) - uu___17))) - (fun - uu___17 - -> - (fun - uu___17 - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (377)) - (Prims.of_int (15)) - (Prims.of_int (377)) - (Prims.of_int (28))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (377)) - (Prims.of_int (31)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (Obj.magic - (FStar_Tactics_V2_Derived.cur_module - ())) - (fun - uu___18 - -> - (fun ns1 - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (378)) - (Prims.of_int (16)) - (Prims.of_int (378)) - (Prims.of_int (34))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (378)) - (Prims.of_int (37)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___18 - -> - FStar_Reflection_V2_Builtins.pack_fv - ((op_At - ()) ns1 - [s]))) - (fun - uu___18 - -> - (fun sfv - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (379)) - (Prims.of_int (16)) - (Prims.of_int (379)) - (Prims.of_int (38))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (379)) - (Prims.of_int (41)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (Obj.magic - (FStar_Tactics_V2_Derived.fresh_namedv_named - "d")) - (fun - uu___18 - -> - (fun dbv - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (380)) - (Prims.of_int (16)) - (Prims.of_int (380)) - (Prims.of_int (28))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (380)) - (Prims.of_int (31)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___18 - -> - FStar_Reflection_V2_Builtins.pack_ln - (FStar_Reflection_V2_Data.Tv_FVar - (FStar_Reflection_V2_Builtins.pack_fv - ["FStar"; - "Tactics"; - "Typeclasses"; - "tcresolve"])))) - (fun - uu___18 - -> - (fun tcr - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (382)) - (Prims.of_int (8)) - (Prims.of_int (386)) - (Prims.of_int (20))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (387)) - (Prims.of_int (10)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (384)) - (Prims.of_int (17)) - (Prims.of_int (384)) - (Prims.of_int (24))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (382)) - (Prims.of_int (8)) - (Prims.of_int (386)) - (Prims.of_int (20))))) - (Obj.magic - (FStar_Tactics_V2_Builtins.fresh - ())) - (fun - uu___18 - -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___19 - -> - { - FStar_Tactics_NamedView.uniq - = uu___18; - FStar_Tactics_NamedView.ppname - = - (FStar_Sealed.seal - "dict"); - FStar_Tactics_NamedView.sort - = cod1; - FStar_Tactics_NamedView.qual - = - (FStar_Reflection_V2_Data.Q_Meta - tcr); - FStar_Tactics_NamedView.attrs - = [] - })))) - (fun - uu___18 - -> - (fun - tcdict -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (388)) - (Prims.of_int (22)) - (Prims.of_int (388)) - (Prims.of_int (48))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (388)) - (Prims.of_int (51)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (388)) - (Prims.of_int (22)) - (Prims.of_int (388)) - (Prims.of_int (35))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (388)) - (Prims.of_int (22)) - (Prims.of_int (388)) - (Prims.of_int (48))))) - (Obj.magic - (FStar_Tactics_V2_Derived.cur_module - ())) - (fun - uu___18 - -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___19 - -> - (op_At ()) - uu___18 - [ - Prims.strcat - base s])))) - (fun - uu___18 - -> - (fun - proj_name - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (389)) - (Prims.of_int (17)) - (Prims.of_int (389)) - (Prims.of_int (51))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (389)) - (Prims.of_int (54)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___18 - -> - FStar_Tactics_NamedView.pack - (FStar_Tactics_NamedView.Tv_FVar - (FStar_Reflection_V2_Builtins.pack_fv - proj_name)))) - (fun - uu___18 - -> - (fun proj - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (392)) - (Prims.of_int (8)) - (Prims.of_int (397)) - (Prims.of_int (50))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (398)) - (Prims.of_int (8)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (392)) - (Prims.of_int (14)) - (Prims.of_int (392)) - (Prims.of_int (47))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (392)) - (Prims.of_int (8)) - (Prims.of_int (397)) - (Prims.of_int (50))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (392)) - (Prims.of_int (25)) - (Prims.of_int (392)) - (Prims.of_int (37))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (392)) - (Prims.of_int (14)) - (Prims.of_int (392)) - (Prims.of_int (47))))) - (Obj.magic - (FStar_Tactics_V2_Builtins.top_env - ())) - (fun - uu___18 - -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___19 - -> - FStar_Reflection_V2_Builtins.lookup_typ - uu___18 - proj_name)))) - (fun - uu___18 - -> - (fun - uu___18 - -> - match uu___18 - with - | - FStar_Pervasives_Native.None - -> - Obj.magic - (Obj.repr - (FStar_Tactics_V2_Derived.fail - "mk_class: proj not found?")) - | - FStar_Pervasives_Native.Some - se1 -> - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (395)) - (Prims.of_int (16)) - (Prims.of_int (395)) - (Prims.of_int (33))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (395)) - (Prims.of_int (10)) - (Prims.of_int (397)) - (Prims.of_int (50))))) - (Obj.magic - (FStar_Tactics_NamedView.inspect_sigelt - se1)) - (fun - uu___19 - -> - (fun - uu___19 - -> - match uu___19 - with - | - FStar_Tactics_NamedView.Sg_Let - { - FStar_Tactics_NamedView.isrec - = uu___20; - FStar_Tactics_NamedView.lbs - = lbs;_} - -> - Obj.magic - (Obj.repr - (FStar_Tactics_V2_SyntaxHelpers.lookup_lb - lbs - proj_name)) - | - uu___20 - -> - Obj.magic - (Obj.repr - (FStar_Tactics_V2_Derived.fail - "mk_class: proj not Sg_Let?"))) - uu___19)))) - uu___18))) - (fun - uu___18 - -> - (fun - proj_lb - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (401)) - (Prims.of_int (14)) - (Prims.of_int (408)) - (Prims.of_int (37))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (409)) - (Prims.of_int (8)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (402)) - (Prims.of_int (22)) - (Prims.of_int (402)) - (Prims.of_int (51))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (401)) - (Prims.of_int (14)) - (Prims.of_int (408)) - (Prims.of_int (37))))) - (Obj.magic - (FStar_Tactics_V2_SyntaxHelpers.collect_arr_bs - proj_lb.FStar_Tactics_NamedView.lb_typ)) - (fun - uu___18 - -> - (fun - uu___18 - -> - match uu___18 - with - | - (bs1, - cod2) -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (403)) - (Prims.of_int (21)) - (Prims.of_int (403)) - (Prims.of_int (75))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (402)) - (Prims.of_int (54)) - (Prims.of_int (408)) - (Prims.of_int (37))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___19 - -> - FStar_List_Tot_Base.splitAt - (FStar_List_Tot_Base.length - params) - bs1)) - (fun - uu___19 - -> - (fun - uu___19 - -> - match uu___19 - with - | - (ps, bs2) - -> - (match bs2 - with - | - [] -> - Obj.magic - (Obj.repr - (FStar_Tactics_V2_Derived.fail - "mk_class: impossible, no binders")) - | - b1::bs' - -> - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (407)) - (Prims.of_int (21)) - (Prims.of_int (407)) - (Prims.of_int (43))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (408)) - (Prims.of_int (12)) - (Prims.of_int (408)) - (Prims.of_int (37))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___20 - -> - binder_set_meta - b1 tcr)) - (fun - uu___20 - -> - (fun b11 - -> - Obj.magic - (FStar_Tactics_V2_SyntaxHelpers.mk_arr - ((op_At - ()) ps - (b11 :: - bs')) - cod2)) - uu___20))))) - uu___19))) - uu___18))) - (fun - uu___18 - -> - (fun ty1 - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (410)) - (Prims.of_int (15)) - (Prims.of_int (417)) - (Prims.of_int (38))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (419)) - (Prims.of_int (6)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (411)) - (Prims.of_int (23)) - (Prims.of_int (411)) - (Prims.of_int (49))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (410)) - (Prims.of_int (15)) - (Prims.of_int (417)) - (Prims.of_int (38))))) - (Obj.magic - (FStar_Tactics_V2_SyntaxHelpers.collect_abs - proj_lb.FStar_Tactics_NamedView.lb_def)) - (fun - uu___18 - -> - (fun - uu___18 - -> - match uu___18 - with - | - (bs1, - body) -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (412)) - (Prims.of_int (21)) - (Prims.of_int (412)) - (Prims.of_int (75))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (411)) - (Prims.of_int (52)) - (Prims.of_int (417)) - (Prims.of_int (38))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___19 - -> - FStar_List_Tot_Base.splitAt - (FStar_List_Tot_Base.length - params) - bs1)) - (fun - uu___19 - -> - (fun - uu___19 - -> - match uu___19 - with - | - (ps, bs2) - -> - (match bs2 - with - | - [] -> - Obj.magic - (Obj.repr - (FStar_Tactics_V2_Derived.fail - "mk_class: impossible, no binders")) - | - b1::bs' - -> - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (416)) - (Prims.of_int (21)) - (Prims.of_int (416)) - (Prims.of_int (43))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (417)) - (Prims.of_int (12)) - (Prims.of_int (417)) - (Prims.of_int (38))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___20 - -> - binder_set_meta - b1 tcr)) - (fun - uu___20 - -> - (fun b11 - -> - Obj.magic - (mk_abs - ((op_At - ()) ps - (b11 :: - bs')) - body)) - uu___20))))) - uu___19))) - uu___18))) - (fun - uu___18 - -> - (fun def - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (419)) - (Prims.of_int (6)) - (Prims.of_int (419)) - (Prims.of_int (53))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (420)) - (Prims.of_int (6)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (Obj.magic - (debug - (fun - uu___18 - -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (419)) - (Prims.of_int (34)) - (Prims.of_int (419)) - (Prims.of_int (52))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "prims.fst" - (Prims.of_int (590)) - (Prims.of_int (19)) - (Prims.of_int (590)) - (Prims.of_int (31))))) - (Obj.magic - (FStar_Tactics_V2_Builtins.term_to_string - def)) - (fun - uu___19 - -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___20 - -> - Prims.strcat - "def = " - uu___19))))) - (fun - uu___18 - -> - (fun - uu___18 - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (420)) - (Prims.of_int (6)) - (Prims.of_int (420)) - (Prims.of_int (52))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (420)) - (Prims.of_int (53)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (Obj.magic - (debug - (fun - uu___19 - -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (420)) - (Prims.of_int (34)) - (Prims.of_int (420)) - (Prims.of_int (51))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "prims.fst" - (Prims.of_int (590)) - (Prims.of_int (19)) - (Prims.of_int (590)) - (Prims.of_int (31))))) - (Obj.magic - (FStar_Tactics_V2_Builtins.term_to_string - ty1)) - (fun - uu___20 - -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___21 - -> - Prims.strcat - "ty = " - uu___20))))) - (fun - uu___19 - -> - (fun - uu___19 - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (422)) - (Prims.of_int (22)) - (Prims.of_int (422)) - (Prims.of_int (24))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (422)) - (Prims.of_int (27)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___20 - -> ty1)) - (fun - uu___20 - -> - (fun ty2 - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (423)) - (Prims.of_int (23)) - (Prims.of_int (423)) - (Prims.of_int (26))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (423)) - (Prims.of_int (29)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___20 - -> def)) - (fun - uu___20 - -> - (fun def1 - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (424)) - (Prims.of_int (21)) - (Prims.of_int (424)) - (Prims.of_int (24))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (424)) - (Prims.of_int (27)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___20 - -> sfv)) - (fun - uu___20 - -> - (fun sfv1 - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (426)) - (Prims.of_int (17)) - (Prims.of_int (426)) - (Prims.of_int (70))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (426)) - (Prims.of_int (75)) - (Prims.of_int (431)) - (Prims.of_int (8))))) - (FStar_Tactics_Effect.lift_div_tac - (fun - uu___20 - -> - { - FStar_Tactics_NamedView.lb_fv - = sfv1; - FStar_Tactics_NamedView.lb_us - = - (proj_lb.FStar_Tactics_NamedView.lb_us); - FStar_Tactics_NamedView.lb_typ - = ty2; - FStar_Tactics_NamedView.lb_def - = def1 - })) - (fun - uu___20 - -> - (fun lb - -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (427)) - (Prims.of_int (15)) - (Prims.of_int (427)) - (Prims.of_int (59))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (429)) - (Prims.of_int (15)) - (Prims.of_int (429)) - (Prims.of_int (42))))) - (Obj.magic - (FStar_Tactics_NamedView.pack_sigelt - (FStar_Tactics_NamedView.Sg_Let - { - FStar_Tactics_NamedView.isrec - = false; - FStar_Tactics_NamedView.lbs - = [lb] - }))) - (fun se1 - -> - FStar_Tactics_Effect.lift_div_tac - (fun - uu___20 - -> - FStar_Reflection_V2_Builtins.set_sigelt_attrs - b.FStar_Tactics_NamedView.attrs - (FStar_Reflection_V2_Builtins.set_sigelt_quals - to_propagate - se1))))) - uu___20))) - uu___20))) - uu___20))) - uu___20))) - uu___19))) - uu___18))) - uu___18))) - uu___18))) - uu___18))) - uu___18))) - uu___18))) - uu___18))) - uu___18))) - uu___18))) - uu___18))) - uu___18))) - uu___17))) - uu___17)) - (filter_no_method_binders - bs))) - uu___17))) - uu___16))) - uu___15))) - uu___14))) - uu___13))) - uu___12))) - uu___11))) - uu___11))) - uu___10))) - uu___9))) - uu___8))) - uu___7))) - uu___7))) - uu___6))) - uu___5))) - uu___4))) - uu___3))) - uu___2))) - uu___2))) - uu___2))) uu___1))) - uu___))) uu___))) uu___) -let _ = - FStar_Tactics_Native.register_tactic "FStar.Tactics.Typeclasses.mk_class" - (Prims.of_int (2)) - (fun psc -> - fun ncb -> - fun us -> - fun args -> - FStar_Tactics_InterpFuns.mk_tactic_interpretation_1 - "FStar.Tactics.Typeclasses.mk_class (plugin)" - (FStar_Tactics_Native.from_tactic_1 mk_class) - FStar_Syntax_Embeddings.e_string - (FStar_Syntax_Embeddings.e_list - FStar_Reflection_V2_Embeddings.e_sigelt) psc ncb us args) let solve : 'a . 'a -> 'a = fun ev -> ev \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml index f46191942e0..ec5cdfb7960 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Basic.ml @@ -3318,6 +3318,110 @@ let (intro : tts uu___4 uu___5 in fail1 "goal is not an arrow (%s)" uu___3))) uu___2)) in FStar_Tactics_Monad.wrap_err "intro" uu___1 +let (intros : + unit -> FStar_Reflection_V2_Data.binding Prims.list FStar_Tactics_Monad.tac) + = + fun uu___ -> + let uu___1 = + Obj.magic + (FStar_Class_Monad.op_let_Bang FStar_Tactics_Monad.monad_tac () () + (Obj.magic FStar_Tactics_Monad.cur_goal) + (fun uu___2 -> + (fun goal -> + let goal = Obj.magic goal in + let uu___2 = + let uu___3 = FStar_Tactics_Types.goal_type goal in + FStar_Syntax_Util.arrow_formals_comp_ln uu___3 in + match uu___2 with + | (bs, c) -> + Obj.magic + (Obj.repr + (FStar_Tactics_Monad.fail "Codomain is effectful")) + | ([], uu___3) -> + Obj.magic + (Obj.repr + (let uu___4 = + let uu___5 = FStar_Tactics_Types.goal_env goal in + let uu___6 = FStar_Tactics_Types.goal_type goal in + tts uu___5 uu___6 in + fail1 "goal is not an arrow (%s)" uu___4)) + | (bs, c) -> + Obj.magic + (Obj.repr + (let uu___3 = + let uu___4 = FStar_Tactics_Types.goal_env goal in + FStar_TypeChecker_Core.open_binders_in_comp + uu___4 bs c in + match uu___3 with + | (env', bs1, c1) -> + let typ' = FStar_Syntax_Util.comp_result c1 in + let uu___4 = + let uu___5 = + let uu___6 = should_check_goal_uvar goal in + FStar_Pervasives_Native.Some uu___6 in + let uu___6 = + FStar_Tactics_Monad.goal_typedness_deps + goal in + FStar_Tactics_Monad.new_uvar "intros" env' + typ' uu___5 uu___6 (rangeof goal) in + FStar_Class_Monad.op_let_Bang + FStar_Tactics_Monad.monad_tac () () + (Obj.magic uu___4) + (fun uu___5 -> + (fun uu___5 -> + let uu___5 = Obj.magic uu___5 in + match uu___5 with + | (body, ctx_uvar) -> + let sol = + let uu___6 = + let uu___7 = + FStar_Syntax_Util.residual_comp_of_comp + c1 in + FStar_Pervasives_Native.Some + uu___7 in + FStar_Syntax_Util.abs bs1 body + uu___6 in + let uu___6 = set_solution goal sol in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Tactics_Monad.monad_tac + () () uu___6 + (fun uu___7 -> + (fun uu___7 -> + let uu___7 = + Obj.magic uu___7 in + let g = + FStar_Tactics_Types.mk_goal + env' ctx_uvar + goal.FStar_Tactics_Types.opts + goal.FStar_Tactics_Types.is_guard + goal.FStar_Tactics_Types.label in + let uu___8 = + bnorm_and_replace g in + Obj.magic + (FStar_Class_Monad.op_let_Bang + FStar_Tactics_Monad.monad_tac + () () uu___8 + (fun uu___9 -> + (fun uu___9 -> + let uu___9 = + Obj.magic + uu___9 in + let uu___10 + = + FStar_Compiler_List.map + binder_to_binding + bs1 in + Obj.magic + (FStar_Class_Monad.return + FStar_Tactics_Monad.monad_tac + () + (Obj.magic + uu___10))) + uu___9))) + uu___7))) uu___5)))) + uu___2)) in + FStar_Tactics_Monad.wrap_err "intros" uu___1 let (intro_rec : unit -> (FStar_Reflection_V2_Data.binding * FStar_Reflection_V2_Data.binding) diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Primops.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Primops.ml index ba9d752abb3..7a73ef6596f 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Primops.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Primops.ml @@ -261,157 +261,170 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = let uu___37 = let uu___38 = FStar_Tactics_InterpFuns.mk_tac_step_1 - Prims.int_zero "intro_rec" + Prims.int_zero "intros" FStar_Syntax_Embeddings.e_unit - (FStar_Syntax_Embeddings.e_tuple2 - FStar_Reflection_V2_Embeddings.e_binding + (FStar_Syntax_Embeddings.e_list FStar_Reflection_V2_Embeddings.e_binding) FStar_TypeChecker_NBETerm.e_unit - (FStar_TypeChecker_NBETerm.e_tuple2 - FStar_Reflection_V2_NBEEmbeddings.e_binding + (FStar_TypeChecker_NBETerm.e_list FStar_Reflection_V2_NBEEmbeddings.e_binding) - FStar_Tactics_V2_Basic.intro_rec - FStar_Tactics_V2_Basic.intro_rec in + FStar_Tactics_V2_Basic.intros + FStar_Tactics_V2_Basic.intros in let uu___39 = let uu___40 = FStar_Tactics_InterpFuns.mk_tac_step_1 - Prims.int_zero "norm" - (FStar_Syntax_Embeddings.e_list - FStar_Syntax_Embeddings.e_norm_step) + Prims.int_zero "intro_rec" FStar_Syntax_Embeddings.e_unit - (FStar_TypeChecker_NBETerm.e_list - FStar_TypeChecker_NBETerm.e_norm_step) + (FStar_Syntax_Embeddings.e_tuple2 + FStar_Reflection_V2_Embeddings.e_binding + FStar_Reflection_V2_Embeddings.e_binding) FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.norm - FStar_Tactics_V2_Basic.norm in + (FStar_TypeChecker_NBETerm.e_tuple2 + FStar_Reflection_V2_NBEEmbeddings.e_binding + FStar_Reflection_V2_NBEEmbeddings.e_binding) + FStar_Tactics_V2_Basic.intro_rec + FStar_Tactics_V2_Basic.intro_rec in let uu___41 = let uu___42 = - FStar_Tactics_InterpFuns.mk_tac_step_3 - Prims.int_zero - "norm_term_env" - FStar_Reflection_V2_Embeddings.e_env + FStar_Tactics_InterpFuns.mk_tac_step_1 + Prims.int_zero "norm" (FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_norm_step) - uu___2 uu___2 - FStar_Reflection_V2_NBEEmbeddings.e_env + FStar_Syntax_Embeddings.e_unit (FStar_TypeChecker_NBETerm.e_list FStar_TypeChecker_NBETerm.e_norm_step) - FStar_Reflection_V2_NBEEmbeddings.e_attribute - FStar_Reflection_V2_NBEEmbeddings.e_attribute - FStar_Tactics_V2_Basic.norm_term_env - FStar_Tactics_V2_Basic.norm_term_env in + FStar_TypeChecker_NBETerm.e_unit + FStar_Tactics_V2_Basic.norm + FStar_Tactics_V2_Basic.norm in let uu___43 = let uu___44 = - FStar_Tactics_InterpFuns.mk_tac_step_2 + FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero - "norm_binding_type" + "norm_term_env" + FStar_Reflection_V2_Embeddings.e_env (FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_norm_step) - FStar_Reflection_V2_Embeddings.e_binding - FStar_Syntax_Embeddings.e_unit + uu___2 uu___2 + FStar_Reflection_V2_NBEEmbeddings.e_env (FStar_TypeChecker_NBETerm.e_list FStar_TypeChecker_NBETerm.e_norm_step) - FStar_Reflection_V2_NBEEmbeddings.e_binding - FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.norm_binding_type - FStar_Tactics_V2_Basic.norm_binding_type in + FStar_Reflection_V2_NBEEmbeddings.e_attribute + FStar_Reflection_V2_NBEEmbeddings.e_attribute + FStar_Tactics_V2_Basic.norm_term_env + FStar_Tactics_V2_Basic.norm_term_env in let uu___45 = let uu___46 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero - "rename_to" + "norm_binding_type" + (FStar_Syntax_Embeddings.e_list + FStar_Syntax_Embeddings.e_norm_step) FStar_Reflection_V2_Embeddings.e_binding - FStar_Syntax_Embeddings.e_string - FStar_Reflection_V2_Embeddings.e_binding - FStar_Reflection_V2_NBEEmbeddings.e_binding - FStar_TypeChecker_NBETerm.e_string + FStar_Syntax_Embeddings.e_unit + (FStar_TypeChecker_NBETerm.e_list + FStar_TypeChecker_NBETerm.e_norm_step) FStar_Reflection_V2_NBEEmbeddings.e_binding - FStar_Tactics_V2_Basic.rename_to - FStar_Tactics_V2_Basic.rename_to in + FStar_TypeChecker_NBETerm.e_unit + FStar_Tactics_V2_Basic.norm_binding_type + FStar_Tactics_V2_Basic.norm_binding_type in let uu___47 = let uu___48 = - FStar_Tactics_InterpFuns.mk_tac_step_1 + FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero - "var_retype" + "rename_to" FStar_Reflection_V2_Embeddings.e_binding - FStar_Syntax_Embeddings.e_unit + FStar_Syntax_Embeddings.e_string + FStar_Reflection_V2_Embeddings.e_binding + FStar_Reflection_V2_NBEEmbeddings.e_binding + FStar_TypeChecker_NBETerm.e_string FStar_Reflection_V2_NBEEmbeddings.e_binding - FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.var_retype - FStar_Tactics_V2_Basic.var_retype in + FStar_Tactics_V2_Basic.rename_to + FStar_Tactics_V2_Basic.rename_to in let uu___49 = let uu___50 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero - "revert" + "var_retype" + FStar_Reflection_V2_Embeddings.e_binding FStar_Syntax_Embeddings.e_unit - FStar_Syntax_Embeddings.e_unit - FStar_TypeChecker_NBETerm.e_unit + FStar_Reflection_V2_NBEEmbeddings.e_binding FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.revert - FStar_Tactics_V2_Basic.revert in + FStar_Tactics_V2_Basic.var_retype + FStar_Tactics_V2_Basic.var_retype in let uu___51 = let uu___52 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero - "clear_top" + "revert" FStar_Syntax_Embeddings.e_unit FStar_Syntax_Embeddings.e_unit FStar_TypeChecker_NBETerm.e_unit FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.clear_top - FStar_Tactics_V2_Basic.clear_top in + FStar_Tactics_V2_Basic.revert + FStar_Tactics_V2_Basic.revert in let uu___53 = let uu___54 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero - "clear" - FStar_Reflection_V2_Embeddings.e_binding + "clear_top" + FStar_Syntax_Embeddings.e_unit FStar_Syntax_Embeddings.e_unit - FStar_Reflection_V2_NBEEmbeddings.e_binding FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.clear - FStar_Tactics_V2_Basic.clear in + FStar_TypeChecker_NBETerm.e_unit + FStar_Tactics_V2_Basic.clear_top + FStar_Tactics_V2_Basic.clear_top in let uu___55 = let uu___56 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero - "rewrite" + "clear" FStar_Reflection_V2_Embeddings.e_binding FStar_Syntax_Embeddings.e_unit FStar_Reflection_V2_NBEEmbeddings.e_binding FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.rewrite - FStar_Tactics_V2_Basic.rewrite in + FStar_Tactics_V2_Basic.clear + FStar_Tactics_V2_Basic.clear in let uu___57 = let uu___58 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero - "refine_intro" - FStar_Syntax_Embeddings.e_unit + "rewrite" + FStar_Reflection_V2_Embeddings.e_binding FStar_Syntax_Embeddings.e_unit + FStar_Reflection_V2_NBEEmbeddings.e_binding FStar_TypeChecker_NBETerm.e_unit - FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.refine_intro - FStar_Tactics_V2_Basic.refine_intro in + FStar_Tactics_V2_Basic.rewrite + FStar_Tactics_V2_Basic.rewrite in let uu___59 = let uu___60 = - FStar_Tactics_InterpFuns.mk_tac_step_3 + FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero - "t_exact" - FStar_Syntax_Embeddings.e_bool - FStar_Syntax_Embeddings.e_bool - uu___2 + "refine_intro" FStar_Syntax_Embeddings.e_unit - FStar_TypeChecker_NBETerm.e_bool - FStar_TypeChecker_NBETerm.e_bool - FStar_Reflection_V2_NBEEmbeddings.e_attribute + FStar_Syntax_Embeddings.e_unit + FStar_TypeChecker_NBETerm.e_unit FStar_TypeChecker_NBETerm.e_unit - FStar_Tactics_V2_Basic.t_exact - FStar_Tactics_V2_Basic.t_exact in + FStar_Tactics_V2_Basic.refine_intro + FStar_Tactics_V2_Basic.refine_intro in let uu___61 = let uu___62 = - FStar_Tactics_InterpFuns.mk_tac_step_4 + FStar_Tactics_InterpFuns.mk_tac_step_3 + Prims.int_zero + "t_exact" + FStar_Syntax_Embeddings.e_bool + FStar_Syntax_Embeddings.e_bool + uu___2 + FStar_Syntax_Embeddings.e_unit + FStar_TypeChecker_NBETerm.e_bool + FStar_TypeChecker_NBETerm.e_bool + FStar_Reflection_V2_NBEEmbeddings.e_attribute + FStar_TypeChecker_NBETerm.e_unit + FStar_Tactics_V2_Basic.t_exact + FStar_Tactics_V2_Basic.t_exact in + let uu___63 = + let uu___64 + = + FStar_Tactics_InterpFuns.mk_tac_step_4 Prims.int_zero "t_apply" FStar_Syntax_Embeddings.e_bool @@ -426,8 +439,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.t_apply FStar_Tactics_V2_Basic.t_apply in - let uu___63 = - let uu___64 + let uu___65 + = + let uu___66 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -442,9 +456,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.t_apply_lemma FStar_Tactics_V2_Basic.t_apply_lemma in - let uu___65 + let uu___67 = - let uu___66 + let uu___68 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -455,9 +469,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.set_options FStar_Tactics_V2_Basic.set_options in - let uu___67 + let uu___69 = - let uu___68 + let uu___70 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -470,9 +484,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_comp FStar_Tactics_V2_Basic.tcc FStar_Tactics_V2_Basic.tcc in - let uu___69 + let uu___71 = - let uu___70 + let uu___72 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -485,9 +499,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_V2_Basic.tc FStar_Tactics_V2_Basic.tc in - let uu___71 + let uu___73 = - let uu___72 + let uu___74 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -498,9 +512,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.unshelve FStar_Tactics_V2_Basic.unshelve in - let uu___73 + let uu___75 = - let uu___74 + let uu___76 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_one @@ -513,16 +527,16 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_any FStar_Tactics_V2_Basic.unquote (fun - uu___75 + uu___77 -> fun - uu___76 + uu___78 -> FStar_Compiler_Effect.failwith "NBE unquote") in - let uu___75 + let uu___77 = - let uu___76 + let uu___78 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -533,9 +547,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.prune FStar_Tactics_V2_Basic.prune in - let uu___77 + let uu___79 = - let uu___78 + let uu___80 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -546,9 +560,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.addns FStar_Tactics_V2_Basic.addns in - let uu___79 + let uu___81 = - let uu___80 + let uu___82 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -559,9 +573,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.print FStar_Tactics_V2_Basic.print in - let uu___81 + let uu___83 = - let uu___82 + let uu___84 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -572,9 +586,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_V2_Basic.debugging FStar_Tactics_V2_Basic.debugging in - let uu___83 + let uu___85 = - let uu___84 + let uu___86 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -585,9 +599,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_V2_Basic.ide FStar_Tactics_V2_Basic.ide in - let uu___85 + let uu___87 = - let uu___86 + let uu___88 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -598,9 +612,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.dump FStar_Tactics_V2_Basic.dump in - let uu___87 + let uu___89 = - let uu___88 + let uu___90 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -613,9 +627,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.dump_all FStar_Tactics_V2_Basic.dump_all in - let uu___89 + let uu___91 = - let uu___90 + let uu___92 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -628,29 +642,29 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.dump_uvars_of FStar_Tactics_V2_Basic.dump_uvars_of in - let uu___91 + let uu___93 = - let uu___92 + let uu___94 = - let uu___93 + let uu___95 = FStar_Tactics_Interpreter.e_tactic_1 FStar_Reflection_V2_Embeddings.e_term (FStar_Syntax_Embeddings.e_tuple2 FStar_Syntax_Embeddings.e_bool FStar_Tactics_Embedding.e_ctrl_flag) in - let uu___94 + let uu___96 = FStar_Tactics_Interpreter.e_tactic_thunk FStar_Syntax_Embeddings.e_unit in - let uu___95 + let uu___97 = FStar_Tactics_Interpreter.e_tactic_nbe_1 FStar_Reflection_V2_NBEEmbeddings.e_term (FStar_TypeChecker_NBETerm.e_tuple2 FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_Embedding.e_ctrl_flag_nbe) in - let uu___96 + let uu___98 = FStar_Tactics_Interpreter.e_tactic_nbe_thunk FStar_TypeChecker_NBETerm.e_unit in @@ -658,18 +672,18 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "ctrl_rewrite" FStar_Tactics_Embedding.e_direction - uu___93 - uu___94 - FStar_Syntax_Embeddings.e_unit - FStar_Tactics_Embedding.e_direction_nbe uu___95 uu___96 + FStar_Syntax_Embeddings.e_unit + FStar_Tactics_Embedding.e_direction_nbe + uu___97 + uu___98 FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_CtrlRewrite.ctrl_rewrite FStar_Tactics_CtrlRewrite.ctrl_rewrite in - let uu___93 + let uu___95 = - let uu___94 + let uu___96 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -680,9 +694,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.t_trefl FStar_Tactics_V2_Basic.t_trefl in - let uu___95 + let uu___97 = - let uu___96 + let uu___98 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -693,9 +707,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.dup FStar_Tactics_V2_Basic.dup in - let uu___97 + let uu___99 = - let uu___98 + let uu___100 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -706,9 +720,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.tadmit_t FStar_Tactics_V2_Basic.tadmit_t in - let uu___99 + let uu___101 = - let uu___100 + let uu___102 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -719,9 +733,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.join FStar_Tactics_V2_Basic.join in - let uu___101 + let uu___103 = - let uu___102 + let uu___104 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -738,9 +752,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_int)) FStar_Tactics_V2_Basic.t_destruct FStar_Tactics_V2_Basic.t_destruct in - let uu___103 + let uu___105 = - let uu___104 + let uu___106 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -751,9 +765,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Tactics_V2_Basic.top_env FStar_Tactics_V2_Basic.top_env in - let uu___105 + let uu___107 = - let uu___106 + let uu___108 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -764,9 +778,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_int FStar_Tactics_V2_Basic.fresh FStar_Tactics_V2_Basic.fresh in - let uu___107 + let uu___109 = - let uu___108 + let uu___110 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -777,9 +791,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_int FStar_Tactics_V2_Basic.curms FStar_Tactics_V2_Basic.curms in - let uu___109 + let uu___111 = - let uu___110 + let uu___112 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -794,9 +808,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_V2_Basic.uvar_env FStar_Tactics_V2_Basic.uvar_env in - let uu___111 + let uu___113 = - let uu___112 + let uu___114 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -809,9 +823,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_V2_Basic.ghost_uvar_env FStar_Tactics_V2_Basic.ghost_uvar_env in - let uu___113 + let uu___115 = - let uu___114 + let uu___116 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -822,9 +836,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_V2_Basic.fresh_universe_uvar FStar_Tactics_V2_Basic.fresh_universe_uvar in - let uu___115 + let uu___117 = - let uu___116 + let uu___118 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -839,9 +853,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_V2_Basic.unify_env FStar_Tactics_V2_Basic.unify_env in - let uu___117 + let uu___119 = - let uu___118 + let uu___120 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -856,9 +870,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_V2_Basic.unify_guard_env FStar_Tactics_V2_Basic.unify_guard_env in - let uu___119 + let uu___121 = - let uu___120 + let uu___122 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -873,9 +887,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_V2_Basic.match_env FStar_Tactics_V2_Basic.match_env in - let uu___121 + let uu___123 = - let uu___122 + let uu___124 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -890,9 +904,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_string FStar_Tactics_V2_Basic.launch_process FStar_Tactics_V2_Basic.launch_process in - let uu___123 + let uu___125 = - let uu___124 + let uu___126 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -903,9 +917,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.change FStar_Tactics_V2_Basic.change in - let uu___125 + let uu___127 = - let uu___126 + let uu___128 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -916,9 +930,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Tactics_Embedding.e_guard_policy_nbe FStar_Tactics_V2_Basic.get_guard_policy FStar_Tactics_V2_Basic.get_guard_policy in - let uu___127 + let uu___129 = - let uu___128 + let uu___130 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -929,9 +943,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.set_guard_policy FStar_Tactics_V2_Basic.set_guard_policy in - let uu___129 + let uu___131 = - let uu___130 + let uu___132 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -942,9 +956,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_V2_Basic.lax_on FStar_Tactics_V2_Basic.lax_on in - let uu___131 + let uu___133 = - let uu___132 + let uu___134 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_one @@ -957,16 +971,16 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_any FStar_Tactics_V2_Basic.lget (fun - uu___133 + uu___135 -> fun - uu___134 + uu___136 -> FStar_Tactics_Monad.fail "sorry, `lget` does not work in NBE") in - let uu___133 + let uu___135 = - let uu___134 + let uu___136 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_one @@ -981,19 +995,19 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.lset (fun - uu___135 + uu___137 -> fun - uu___136 + uu___138 -> fun - uu___137 + uu___139 -> FStar_Tactics_Monad.fail "sorry, `lset` does not work in NBE") in - let uu___135 + let uu___137 = - let uu___136 + let uu___138 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_one @@ -1004,9 +1018,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.set_urgency FStar_Tactics_V2_Basic.set_urgency in - let uu___137 + let uu___139 = - let uu___138 + let uu___140 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_one @@ -1017,9 +1031,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.set_dump_on_failure FStar_Tactics_V2_Basic.set_dump_on_failure in - let uu___139 + let uu___141 = - let uu___140 + let uu___142 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_one @@ -1030,9 +1044,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.t_commute_applied_match FStar_Tactics_V2_Basic.t_commute_applied_match in - let uu___141 + let uu___143 = - let uu___142 + let uu___144 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1043,9 +1057,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.gather_explicit_guards_for_resolved_goals FStar_Tactics_V2_Basic.gather_explicit_guards_for_resolved_goals in - let uu___143 + let uu___145 = - let uu___144 + let uu___146 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1058,9 +1072,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_V2_Basic.string_to_term FStar_Tactics_V2_Basic.string_to_term in - let uu___145 + let uu___147 = - let uu___146 + let uu___148 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1077,9 +1091,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_binding) FStar_Tactics_V2_Basic.push_bv_dsenv FStar_Tactics_V2_Basic.push_bv_dsenv in - let uu___147 + let uu___149 = - let uu___148 + let uu___150 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1090,9 +1104,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_string FStar_Tactics_V2_Basic.term_to_string FStar_Tactics_V2_Basic.term_to_string in - let uu___149 + let uu___151 = - let uu___150 + let uu___152 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1103,9 +1117,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_string FStar_Tactics_V2_Basic.comp_to_string FStar_Tactics_V2_Basic.comp_to_string in - let uu___151 + let uu___153 = - let uu___152 + let uu___154 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1116,9 +1130,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_document FStar_Tactics_V2_Basic.term_to_doc FStar_Tactics_V2_Basic.term_to_doc in - let uu___153 + let uu___155 = - let uu___154 + let uu___156 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1129,9 +1143,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_document FStar_Tactics_V2_Basic.comp_to_doc FStar_Tactics_V2_Basic.comp_to_doc in - let uu___155 + let uu___157 = - let uu___156 + let uu___158 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1142,9 +1156,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_string FStar_Tactics_V2_Basic.range_to_string FStar_Tactics_V2_Basic.range_to_string in - let uu___157 + let uu___159 = - let uu___158 + let uu___160 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1157,15 +1171,15 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_bool FStar_Tactics_V2_Basic.term_eq_old FStar_Tactics_V2_Basic.term_eq_old in - let uu___159 + let uu___161 = - let uu___160 + let uu___162 = - let uu___161 + let uu___163 = FStar_Tactics_Interpreter.e_tactic_thunk FStar_Syntax_Embeddings.e_any in - let uu___162 + let uu___164 = FStar_Tactics_Interpreter.e_tactic_nbe_thunk FStar_TypeChecker_NBETerm.e_any in @@ -1174,23 +1188,23 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = "with_compat_pre_core" FStar_Syntax_Embeddings.e_any FStar_Syntax_Embeddings.e_int - uu___161 + uu___163 FStar_Syntax_Embeddings.e_any FStar_TypeChecker_NBETerm.e_any FStar_TypeChecker_NBETerm.e_int - uu___162 + uu___164 FStar_TypeChecker_NBETerm.e_any (fun - uu___163 + uu___165 -> FStar_Tactics_V2_Basic.with_compat_pre_core) (fun - uu___163 + uu___165 -> FStar_Tactics_V2_Basic.with_compat_pre_core) in - let uu___161 + let uu___163 = - let uu___162 + let uu___164 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1201,9 +1215,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_vconfig FStar_Tactics_V2_Basic.get_vconfig FStar_Tactics_V2_Basic.get_vconfig in - let uu___163 + let uu___165 = - let uu___164 + let uu___166 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1214,9 +1228,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.set_vconfig FStar_Tactics_V2_Basic.set_vconfig in - let uu___165 + let uu___167 = - let uu___166 + let uu___168 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1227,9 +1241,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.t_smt_sync FStar_Tactics_V2_Basic.t_smt_sync in - let uu___167 + let uu___169 = - let uu___168 + let uu___170 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1242,9 +1256,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_int) FStar_Tactics_V2_Basic.free_uvars FStar_Tactics_V2_Basic.free_uvars in - let uu___169 + let uu___171 = - let uu___170 + let uu___172 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1261,9 +1275,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_string)) FStar_Tactics_V2_Basic.all_ext_options FStar_Tactics_V2_Basic.all_ext_options in - let uu___171 + let uu___173 = - let uu___172 + let uu___174 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1274,9 +1288,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_string FStar_Tactics_V2_Basic.ext_getv FStar_Tactics_V2_Basic.ext_getv in - let uu___173 + let uu___175 = - let uu___174 + let uu___176 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1293,9 +1307,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_string)) FStar_Tactics_V2_Basic.ext_getns FStar_Tactics_V2_Basic.ext_getns in - let uu___175 + let uu___177 = - let uu___176 + let uu___178 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_one @@ -1309,16 +1323,16 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = (FStar_Tactics_Embedding.e_tref_nbe ()) (fun - uu___177 + uu___179 -> FStar_Tactics_V2_Basic.alloc) (fun - uu___177 + uu___179 -> FStar_Tactics_V2_Basic.alloc) in - let uu___177 + let uu___179 = - let uu___178 + let uu___180 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_one @@ -1332,16 +1346,16 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = ()) FStar_TypeChecker_NBETerm.e_any (fun - uu___179 + uu___181 -> FStar_Tactics_V2_Basic.read) (fun - uu___179 + uu___181 -> FStar_Tactics_V2_Basic.read) in - let uu___179 + let uu___181 = - let uu___180 + let uu___182 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_one @@ -1357,16 +1371,16 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_any FStar_TypeChecker_NBETerm.e_unit (fun - uu___181 + uu___183 -> FStar_Tactics_V2_Basic.write) (fun - uu___181 + uu___183 -> FStar_Tactics_V2_Basic.write) in - let uu___181 + let uu___183 = - let uu___182 + let uu___184 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1387,9 +1401,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_is_non_informative FStar_Tactics_V2_Basic.refl_is_non_informative in - let uu___183 + let uu___185 = - let uu___184 + let uu___186 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -1412,9 +1426,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_check_subtyping FStar_Tactics_V2_Basic.refl_check_subtyping in - let uu___185 + let uu___187 = - let uu___186 + let uu___188 = FStar_Tactics_InterpFuns.mk_tac_step_5 Prims.int_zero @@ -1441,9 +1455,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.t_refl_check_equiv FStar_Tactics_V2_Basic.t_refl_check_equiv in - let uu___187 + let uu___189 = - let uu___188 + let uu___190 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1468,9 +1482,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_core_compute_term_type FStar_Tactics_V2_Basic.refl_core_compute_term_type in - let uu___189 + let uu___191 = - let uu___190 + let uu___192 = FStar_Tactics_InterpFuns.mk_tac_step_4 Prims.int_zero @@ -1495,9 +1509,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_core_check_term FStar_Tactics_V2_Basic.refl_core_check_term in - let uu___191 + let uu___193 = - let uu___192 + let uu___194 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -1520,9 +1534,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_core_check_term_at_type FStar_Tactics_V2_Basic.refl_core_check_term_at_type in - let uu___193 + let uu___195 = - let uu___194 + let uu___196 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1551,9 +1565,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_tc_term FStar_Tactics_V2_Basic.refl_tc_term in - let uu___195 + let uu___197 = - let uu___196 + let uu___198 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1574,9 +1588,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_universe_of FStar_Tactics_V2_Basic.refl_universe_of in - let uu___197 + let uu___199 = - let uu___198 + let uu___200 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1597,9 +1611,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_check_prop_validity FStar_Tactics_V2_Basic.refl_check_prop_validity in - let uu___199 + let uu___201 = - let uu___200 + let uu___202 = FStar_Tactics_InterpFuns.mk_tac_step_4 Prims.int_zero @@ -1630,11 +1644,11 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_binding)))) FStar_Tactics_V2_Basic.refl_check_match_complete FStar_Tactics_V2_Basic.refl_check_match_complete in - let uu___201 + let uu___203 = - let uu___202 + let uu___204 = - let uu___203 + let uu___205 = e_ret_t (FStar_Syntax_Embeddings.e_tuple3 @@ -1647,7 +1661,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = uu___2) (solve uu___2)) in - let uu___204 + let uu___206 = nbe_e_ret_t (FStar_TypeChecker_NBETerm.e_tuple3 @@ -1667,26 +1681,26 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = uu___2 (FStar_Syntax_Embeddings.e_option uu___2) - uu___203 + uu___205 FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Reflection_V2_NBEEmbeddings.e_attribute (FStar_TypeChecker_NBETerm.e_option FStar_Reflection_V2_NBEEmbeddings.e_attribute) - uu___204 + uu___206 FStar_Tactics_V2_Basic.refl_instantiate_implicits FStar_Tactics_V2_Basic.refl_instantiate_implicits in - let uu___203 + let uu___205 = - let uu___204 + let uu___206 = - let uu___205 + let uu___207 = e_ret_t (FStar_Syntax_Embeddings.e_list (FStar_Syntax_Embeddings.e_tuple2 FStar_Reflection_V2_Embeddings.e_namedv FStar_Reflection_V2_Embeddings.e_term)) in - let uu___206 + let uu___208 = nbe_e_ret_t (FStar_TypeChecker_NBETerm.e_list @@ -1703,7 +1717,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_Embeddings.e_term)) uu___2 uu___2 - uu___205 + uu___207 FStar_Reflection_V2_NBEEmbeddings.e_env (FStar_TypeChecker_NBETerm.e_list (FStar_TypeChecker_NBETerm.e_tuple2 @@ -1711,12 +1725,12 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_term)) FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Reflection_V2_NBEEmbeddings.e_attribute - uu___206 + uu___208 FStar_Tactics_V2_Basic.refl_try_unify FStar_Tactics_V2_Basic.refl_try_unify in - let uu___205 + let uu___207 = - let uu___206 + let uu___208 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -1739,9 +1753,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_maybe_relate_after_unfolding FStar_Tactics_V2_Basic.refl_maybe_relate_after_unfolding in - let uu___207 + let uu___209 = - let uu___208 + let uu___210 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1762,9 +1776,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.refl_maybe_unfold_head FStar_Tactics_V2_Basic.refl_maybe_unfold_head in - let uu___209 + let uu___211 = - let uu___210 + let uu___212 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -1781,9 +1795,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_attribute FStar_Tactics_V2_Basic.refl_norm_well_typed_term FStar_Tactics_V2_Basic.refl_norm_well_typed_term in - let uu___211 + let uu___213 = - let uu___212 + let uu___214 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1796,9 +1810,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Tactics_V2_Basic.push_open_namespace FStar_Tactics_V2_Basic.push_open_namespace in - let uu___213 + let uu___215 = - let uu___214 + let uu___216 = FStar_Tactics_InterpFuns.mk_tac_step_3 Prims.int_zero @@ -1813,9 +1827,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_env FStar_Tactics_V2_Basic.push_module_abbrev FStar_Tactics_V2_Basic.push_module_abbrev in - let uu___215 + let uu___217 = - let uu___216 + let uu___218 = FStar_Tactics_InterpFuns.mk_tac_step_2 Prims.int_zero @@ -1836,9 +1850,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_Reflection_V2_NBEEmbeddings.e_fv))) FStar_Tactics_V2_Basic.resolve_name FStar_Tactics_V2_Basic.resolve_name in - let uu___217 + let uu___219 = - let uu___218 + let uu___220 = FStar_Tactics_InterpFuns.mk_tac_step_1 Prims.int_zero @@ -1851,15 +1865,15 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_unit FStar_Tactics_V2_Basic.log_issues FStar_Tactics_V2_Basic.log_issues in - let uu___219 + let uu___221 = - let uu___220 + let uu___222 = - let uu___221 + let uu___223 = FStar_Tactics_Interpreter.e_tactic_thunk FStar_Syntax_Embeddings.e_unit in - let uu___222 + let uu___224 = FStar_Tactics_Interpreter.e_tactic_nbe_thunk FStar_TypeChecker_NBETerm.e_unit in @@ -1867,7 +1881,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = Prims.int_zero "call_subtac" FStar_Reflection_V2_Embeddings.e_env - uu___221 + uu___223 FStar_Reflection_V2_Embeddings.e_universe uu___2 (FStar_Syntax_Embeddings.e_tuple2 @@ -1876,7 +1890,7 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = (FStar_Syntax_Embeddings.e_list FStar_Syntax_Embeddings.e_issue)) FStar_Reflection_V2_NBEEmbeddings.e_env - uu___222 + uu___224 FStar_Reflection_V2_NBEEmbeddings.e_universe FStar_Reflection_V2_NBEEmbeddings.e_attribute (FStar_TypeChecker_NBETerm.e_tuple2 @@ -1886,9 +1900,9 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.call_subtac FStar_Tactics_V2_Basic.call_subtac in - let uu___221 + let uu___223 = - let uu___222 + let uu___224 = FStar_Tactics_InterpFuns.mk_tac_step_4 Prims.int_zero @@ -1913,7 +1927,10 @@ let (ops : FStar_TypeChecker_Primops_Base.primitive_step Prims.list) = FStar_TypeChecker_NBETerm.e_issue)) FStar_Tactics_V2_Basic.call_subtac_tm FStar_Tactics_V2_Basic.call_subtac_tm in - [uu___222] in + [uu___224] in + uu___222 + :: + uu___223 in uu___220 :: uu___221 in diff --git a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml index d12f0c4948c..def146ac9c8 100644 --- a/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml +++ b/ocaml/fstar-lib/generated/FStar_ToSyntax_ToSyntax.ml @@ -9215,38 +9215,21 @@ and (desugar_decl_core : let r = FStar_Ident.range_of_lid lid in let body = let uu___2 = - FStar_Syntax_Util.has_attribute d_attrs - FStar_Parser_Const.meta_projectors_attr in - if uu___2 - then - let uu___3 = - FStar_Syntax_Syntax.tabbrev - FStar_Parser_Const.mk_projs_lid in + FStar_Syntax_Syntax.tabbrev + FStar_Parser_Const.mk_projs_lid in + let uu___3 = let uu___4 = - let uu___5 = - let uu___6 = FStar_Syntax_Util.exp_bool true in - FStar_Syntax_Syntax.as_arg uu___6 in + let uu___5 = FStar_Syntax_Util.exp_bool true in + FStar_Syntax_Syntax.as_arg uu___5 in + let uu___5 = let uu___6 = let uu___7 = - let uu___8 = - let uu___9 = FStar_Ident.string_of_lid lid in - FStar_Syntax_Util.exp_string uu___9 in - FStar_Syntax_Syntax.as_arg uu___8 in - [uu___7] in - uu___5 :: uu___6 in - FStar_Syntax_Util.mk_app uu___3 uu___4 - else - (let uu___4 = - FStar_Syntax_Syntax.tabbrev - FStar_Parser_Const.mk_class_lid in - let uu___5 = - let uu___6 = - let uu___7 = - let uu___8 = FStar_Ident.string_of_lid lid in - FStar_Syntax_Util.exp_string uu___8 in - FStar_Syntax_Syntax.as_arg uu___7 in - [uu___6] in - FStar_Syntax_Util.mk_app uu___4 uu___5) in + let uu___8 = FStar_Ident.string_of_lid lid in + FStar_Syntax_Util.exp_string uu___8 in + FStar_Syntax_Syntax.as_arg uu___7 in + [uu___6] in + uu___4 :: uu___5 in + FStar_Syntax_Util.mk_app uu___2 uu___3 in let uu___2 = let uu___3 = let uu___4 = @@ -9416,7 +9399,14 @@ and (desugar_decl_core : FStar_Syntax_Syntax.fvar_with_dd FStar_Parser_Const.tcclass_lid FStar_Pervasives_Native.None in - uu___5 :: (se.FStar_Syntax_Syntax.sigattrs) in + let uu___6 = + let uu___7 = + FStar_Syntax_Syntax.fvar_with_dd + FStar_Parser_Const.meta_projectors_attr + FStar_Pervasives_Native.None in + uu___7 :: + (se.FStar_Syntax_Syntax.sigattrs) in + uu___5 :: uu___6 in FStar_Syntax_Util.deduplicate_terms uu___4 in { FStar_Syntax_Syntax.sigel = @@ -9444,7 +9434,14 @@ and (desugar_decl_core : FStar_Syntax_Syntax.fvar_with_dd FStar_Parser_Const.tcclass_lid FStar_Pervasives_Native.None in - uu___6 :: (se.FStar_Syntax_Syntax.sigattrs) in + let uu___7 = + let uu___8 = + FStar_Syntax_Syntax.fvar_with_dd + FStar_Parser_Const.meta_projectors_attr + FStar_Pervasives_Native.None in + uu___8 :: + (se.FStar_Syntax_Syntax.sigattrs) in + uu___6 :: uu___7 in FStar_Syntax_Util.deduplicate_terms uu___5 in { FStar_Syntax_Syntax.sigel = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml index 3eec03cdace..59218bfe716 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml @@ -790,29 +790,32 @@ type 'a embedding = typ: unit -> t ; e_typ: unit -> FStar_Syntax_Syntax.emb_typ } let __proj__Mkembedding__item__em : 'a . 'a embedding -> nbe_cbs -> 'a -> t = - fun projectee -> match projectee with | { em; un; typ; e_typ;_} -> em + fun x6 -> + match x6 with + | { em = aem; un = aun; typ = atyp; e_typ = ae_typ;_} -> aem +let em : 'a . 'a embedding -> nbe_cbs -> 'a -> t = + fun x6 -> __proj__Mkembedding__item__em x6 let __proj__Mkembedding__item__un : 'a . 'a embedding -> nbe_cbs -> t -> 'a FStar_Pervasives_Native.option = - fun projectee -> match projectee with | { em; un; typ; e_typ;_} -> un -let __proj__Mkembedding__item__typ : 'a . 'a embedding -> unit -> t = - fun projectee -> match projectee with | { em; un; typ; e_typ;_} -> typ -let __proj__Mkembedding__item__e_typ : - 'a . 'a embedding -> unit -> FStar_Syntax_Syntax.emb_typ = - fun projectee -> match projectee with | { em; un; typ; e_typ;_} -> e_typ -let em : 'a . 'a embedding -> nbe_cbs -> 'a -> t = - fun projectee -> - match projectee with | { em = em1; un; typ; e_typ;_} -> em1 + fun x7 -> + match x7 with + | { em = aem; un = aun; typ = atyp; e_typ = ae_typ;_} -> aun let un : 'a . 'a embedding -> nbe_cbs -> t -> 'a FStar_Pervasives_Native.option = - fun projectee -> - match projectee with | { em = em1; un = un1; typ; e_typ;_} -> un1 + fun x7 -> __proj__Mkembedding__item__un x7 +let __proj__Mkembedding__item__typ : 'a . 'a embedding -> unit -> t = + fun x8 -> + match x8 with + | { em = aem; un = aun; typ = atyp; e_typ = ae_typ;_} -> atyp let typ : 'a . 'a embedding -> unit -> t = - fun projectee -> - match projectee with | { em = em1; un = un1; typ = typ1; e_typ;_} -> typ1 + fun x8 -> __proj__Mkembedding__item__typ x8 +let __proj__Mkembedding__item__e_typ : + 'a . 'a embedding -> unit -> FStar_Syntax_Syntax.emb_typ = + fun x9 -> + match x9 with + | { em = aem; un = aun; typ = atyp; e_typ = ae_typ;_} -> ae_typ let e_typ : 'a . 'a embedding -> unit -> FStar_Syntax_Syntax.emb_typ = - fun projectee -> - match projectee with - | { em = em1; un = un1; typ = typ1; e_typ = e_typ1;_} -> e_typ1 + fun x9 -> __proj__Mkembedding__item__e_typ x9 let (iapp_cb : nbe_cbs -> t -> args -> t) = fun cbs -> fun h -> fun a -> cbs.iapp h a let (translate_cb : nbe_cbs -> FStar_Syntax_Syntax.term -> t) = diff --git a/src/parser/FStar.Parser.Const.fst b/src/parser/FStar.Parser.Const.fst index 567e2c655c2..3e7d036b4f9 100644 --- a/src/parser/FStar.Parser.Const.fst +++ b/src/parser/FStar.Parser.Const.fst @@ -497,7 +497,6 @@ let tactic_lid = fstar_tactics_lid' ["Effect"; "tactic"] let meta_projectors_attr = fstar_tactics_lid' ["MkProjectors"; "meta_projectors"] let mk_projs_lid = fstar_tactics_lid' ["MkProjectors"; "mk_projs"] -let mk_class_lid = fstar_tactics_lid' ["Typeclasses"; "mk_class"] let tcresolve_lid = fstar_tactics_lid' ["Typeclasses"; "tcresolve"] let tcclass_lid = fstar_tactics_lid' ["Typeclasses"; "tcclass"] let tcinstance_lid = fstar_tactics_lid' ["Typeclasses"; "tcinstance"] diff --git a/src/parser/FStar.Parser.Dep.fst b/src/parser/FStar.Parser.Dep.fst index 7920aabb755..9bbb2a87ed0 100644 --- a/src/parser/FStar.Parser.Dep.fst +++ b/src/parser/FStar.Parser.Dep.fst @@ -837,8 +837,10 @@ let collect_one collect_term t1 | Tycon (_, tc, ts) -> begin - if tc then - add_to_parsing_data (P_lid Const.tcclass_lid); + if tc then ( + add_to_parsing_data (P_lid Const.tcclass_lid); + add_to_parsing_data (P_lid Const.mk_projs_lid) + ); List.iter collect_tycon ts end | Exception (_, t) -> @@ -920,7 +922,9 @@ let collect_one and collect_aqual = function | Some (Meta t) -> collect_term t - | Some TypeClassArg -> add_to_parsing_data (P_lid Const.tcresolve_lid) + | Some TypeClassArg -> + add_to_parsing_data (P_lid Const.tcresolve_lid); + add_to_parsing_data (P_lid Const.mk_projs_lid) | _ -> () and collect_term t = diff --git a/src/tactics/FStar.Tactics.V2.Basic.fst b/src/tactics/FStar.Tactics.V2.Basic.fst index 277802812f1..5f80fd80c99 100644 --- a/src/tactics/FStar.Tactics.V2.Basic.fst +++ b/src/tactics/FStar.Tactics.V2.Basic.fst @@ -789,6 +789,31 @@ let intro () : tac RD.binding = wrap_err "intro" <| ( fail1 "goal is not an arrow (%s)" (tts (goal_env goal) (goal_type goal)) ) +(* As [intro], but will introduce n binders at once when the expected type is a +literal arrow. *) +let intros () : tac (list RD.binding) = wrap_err "intros" <| ( + let! goal = cur_goal in + match U.arrow_formals_comp_ln (goal_type goal) with + | bs, c -> + fail "Codomain is effectful" + | [], _ -> + fail1 "goal is not an arrow (%s)" (tts (goal_env goal) (goal_type goal)) + + | bs, c -> + let env', bs, c = FStar.TypeChecker.Core.open_binders_in_comp (goal_env goal) bs c in + let typ' = U.comp_result c in + let! body, ctx_uvar = + new_uvar "intros" env' typ' + (Some (should_check_goal_uvar goal)) + (goal_typedness_deps goal) + (rangeof goal) in + let sol = U.abs bs body (Some (U.residual_comp_of_comp c)) in + set_solution goal sol ;! + let g = mk_goal env' ctx_uvar goal.opts goal.is_guard goal.label in + bnorm_and_replace g ;! + return (List.map binder_to_binding bs) + ) + // TODO: missing: precedes clause, and somehow disabling fixpoints only as needed let intro_rec () : tac (RD.binding & RD.binding) = let! goal = cur_goal in diff --git a/src/tactics/FStar.Tactics.V2.Basic.fsti b/src/tactics/FStar.Tactics.V2.Basic.fsti index c65bfc16678..050346c7d46 100644 --- a/src/tactics/FStar.Tactics.V2.Basic.fsti +++ b/src/tactics/FStar.Tactics.V2.Basic.fsti @@ -58,6 +58,7 @@ val norm : list Pervasives.norm_step -> tac unit val norm_term_env : env -> list Pervasives.norm_step -> term -> tac term val norm_binding_type : list Pervasives.norm_step -> RD.binding -> tac unit val intro : unit -> tac RD.binding +val intros : unit -> tac (list RD.binding) val intro_rec : unit -> tac (RD.binding & RD.binding) val rename_to : RD.binding -> string -> tac RD.binding val revert : unit -> tac unit diff --git a/src/tactics/FStar.Tactics.V2.Primops.fst b/src/tactics/FStar.Tactics.V2.Primops.fst index 5e84c0b4427..9b25896cdf4 100644 --- a/src/tactics/FStar.Tactics.V2.Primops.fst +++ b/src/tactics/FStar.Tactics.V2.Primops.fst @@ -117,6 +117,7 @@ let ops = [ (fun _ -> recover); mk_tac_step_1 0 "intro" intro intro; + mk_tac_step_1 0 "intros" intros intros; mk_tac_step_1 0 "intro_rec" intro_rec intro_rec; mk_tac_step_1 0 "norm" norm norm; mk_tac_step_3 0 "norm_term_env" norm_term_env norm_term_env; diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst index 49c254bc837..ccbbf527970 100644 --- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst +++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst @@ -3802,15 +3802,10 @@ and desugar_decl_core env (d_attrs:list S.term) (d:decl) : (env_t & sigelts) = let mkclass lid = let r = range_of_lid lid in let body = - if U.has_attribute d_attrs C.meta_projectors_attr then (* new meta projectors *) U.mk_app (S.tabbrev C.mk_projs_lid) - [S.as_arg (U.exp_bool true); + [S.as_arg (U.exp_bool true); S.as_arg (U.exp_string (string_of_lid lid))] - else - (* old mk_class *) - U.mk_app (S.tabbrev C.mk_class_lid) - [S.as_arg (U.exp_string (string_of_lid lid))] in U.abs [S.mk_binder (S.new_bv (Some r) (tun_r r))] body None in @@ -3886,14 +3881,14 @@ and desugar_decl_core env (d_attrs:list S.term) (d:decl) : (env_t & sigelts) = let ses = List.map add_class_attr ses in { se with sigel = Sig_bundle {ses; lids} ; sigattrs = U.deduplicate_terms - (S.fvar_with_dd FStar.Parser.Const.tcclass_lid None - :: se.sigattrs) } + (S.fvar_with_dd FStar.Parser.Const.tcclass_lid None :: + S.fvar_with_dd FStar.Parser.Const.meta_projectors_attr None :: se.sigattrs) } | Sig_inductive_typ _ -> { se with sigattrs = U.deduplicate_terms - (S.fvar_with_dd FStar.Parser.Const.tcclass_lid None - :: se.sigattrs) } + (S.fvar_with_dd FStar.Parser.Const.tcclass_lid None :: + S.fvar_with_dd FStar.Parser.Const.meta_projectors_attr None :: se.sigattrs) } | _ -> se in diff --git a/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti b/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti index 52191caab3b..29dd63cec1c 100644 --- a/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti +++ b/ulib/FStar.Stubs.Tactics.V2.Builtins.fsti @@ -108,6 +108,12 @@ FStar.Tactics.Logic for that. *) val intro : unit -> Tac binding +(** Like [intro] but pushes many binders at once. The goal has to be +a literal arrow, we will not normalize it nor unfold it. This can be +faster than repeatedly calling intros, and furthermore it will solve the +witness to a flat abstraction instead of many nested ones. *) +val intros : unit -> Tac (list binding) + (** Similar to intros, but allows to build a recursive function. Currently broken (c.f. issue #1103) *) diff --git a/ulib/FStar.Tactics.MkProjectors.fst b/ulib/FStar.Tactics.MkProjectors.fst index dd563277a63..7adab02c936 100644 --- a/ulib/FStar.Tactics.MkProjectors.fst +++ b/ulib/FStar.Tactics.MkProjectors.fst @@ -94,14 +94,22 @@ let embed_string (s:string) : term = let open FStar.Reflection.V2 in pack_ln (Tv_Const (C_String s)) -let mk_proj_decl (is_method:bool) - (tyqn:name) ctorname - (univs : list univ_name) - (params : list binder) - (idx:nat) - (field : binder) - (unfold_names_tm : term) - (smap : list (namedv & fv)) +(* For compatibility: the typechecker sets this attribute for all +projectors. Karamel relies on it to do inlining. *) +let substitute_attr : term = + `Pervasives.Substitute + +let mk_proj_decl + (is_method:bool) + (attrs : list term) + (quals : list qualifier) + (tyqn:name) ctorname + (univs : list univ_name) + (params : list binder) + (idx:nat) + (field : binder) + (unfold_names_tm : term) + (smap : list (namedv & fv)) : Tac (list sigelt & fv) = debug (fun () -> "Processing field " ^ unseal field.ppname); @@ -136,6 +144,7 @@ let mk_proj_decl (is_method:bool) (`#(embed_int idx))))) }]} in + let filter_quals = List.Tot.filter (function | RecordType _ | Noeq -> false | _ -> true) in let maybe_se_method : list sigelt = if not is_method then [] else if List.existsb (Reflection.TermEq.Simple.term_eq (`Typeclasses.no_method)) field.attrs then [] else @@ -147,34 +156,40 @@ let mk_proj_decl (is_method:bool) in (* The method is just defined based on the projector. *) let lb_def = - (`(_ by (mk_one_method - (`#(embed_string (implode_qn nm))) - (`#(embed_int np))))) - (* NB: if we wanted a 'direct' definition of the method, - using a match instead of calling the projector, the following - will do. The same mk_one_projector tactic should handle it - well. - - (`(_ by (mk_one_projector - (`#unfold_names_tm) - (`#(embed_int np)) - (`#(embed_int idx))))) - *) + if true + then + (* This generates a method defined to be equal to the projector + i.e. method {| c |} = c.method *) + (`(_ by (mk_one_method + (`#(embed_string (implode_qn nm))) + (`#(embed_int np))))) + else + (* This defines the method in the same way as the projector + i.e. method {| c |} = match c with | Mk ... method ... -> method *) + (`(_ by (mk_one_projector + (`#unfold_names_tm) + (`#(embed_int np)) + (`#(embed_int idx))))) in (* dump ("returning se with name " ^ unseal field.ppname); *) (* dump ("def = " ^ term_to_string lb_def); *) - [pack_sigelt <| Sg_Let { + let se = pack_sigelt <| Sg_Let { isrec = false; lbs = [{ lb_fv = meth_fv; lb_us = univs; lb_typ = projty; lb_def = lb_def; - }]}] + }]} + in + let se = set_sigelt_attrs (substitute_attr :: field.attrs @ attrs @ sigelt_attrs se) se in + let se = set_sigelt_quals (filter_quals quals @ sigelt_quals se) se in + [se] in (* Propagate binder attributes, i.e. attributes in the field decl, to the method itself. *) - let se_proj = set_sigelt_attrs (field.attrs @ sigelt_attrs se_proj) se_proj in + let se_proj = set_sigelt_attrs (substitute_attr :: field.attrs @ attrs @ sigelt_attrs se_proj) se_proj in + let se_proj = set_sigelt_quals (filter_quals quals @ sigelt_quals se_proj) se_proj in (* Do we need to set the sigelt's Projector qual? If so, here is how to do it, but F* currently rejects tactics @@ -191,12 +206,14 @@ let mk_proj_decl (is_method:bool) [@@plugin] let mk_projs (is_class:bool) (tyname:string) : Tac decls = - print ("!! mk_projs tactic called on: " ^ tyname); + debug (fun () -> "!! mk_projs tactic called on: " ^ tyname); let tyqn = explode_qn tyname in match lookup_typ (top_env ()) tyqn with | None -> raise NotFound | Some se -> + let quals = sigelt_quals se in + let attrs = sigelt_attrs se in match inspect_sigelt se with | Sg_Inductive {nm; univs; params; typ; ctors} -> if (length ctors <> 1) then @@ -211,7 +228,7 @@ let mk_projs (is_class:bool) (tyname:string) : Tac decls = let unfold_names_tm = `(Nil #string) in let (decls, _, _, _) = fold_left (fun (decls, smap, unfold_names_tm, idx) (field : binder) -> - let (ds, fv) = mk_proj_decl is_class tyqn ctorname univs params idx field unfold_names_tm smap in + let (ds, fv) = mk_proj_decl is_class attrs quals tyqn ctorname univs params idx field unfold_names_tm smap in (decls @ ds, (binder_to_namedv field, fv)::smap, (`(Cons #string (`#(embed_string (implode_qn (inspect_fv fv)))) (`#unfold_names_tm))), diff --git a/ulib/FStar.Tactics.Typeclasses.fst b/ulib/FStar.Tactics.Typeclasses.fst index a83c22643d5..784021f7c41 100644 --- a/ulib/FStar.Tactics.Typeclasses.fst +++ b/ulib/FStar.Tactics.Typeclasses.fst @@ -307,126 +307,3 @@ let tcresolve () : Tac unit = | TacticFailure (msg,r) -> fail_doc_at ([text "Typeclass resolution failed."] @ msg) r | e -> raise e - -(**** Generating methods from a class ****) - -(* In TAC, not Tot *) -private -let rec mk_abs (bs : list binder) (body : term) : Tac term (decreases bs) = - match bs with - | [] -> body - | b::bs -> pack (Tv_Abs b (mk_abs bs body)) - -private -let rec last (l : list 'a) : Tac 'a = - match l with - | [] -> fail "last: empty list" - | [x] -> x - | _::xs -> last xs - -private -let filter_no_method_binders (bs:binders) - : binders - = let open FStar.Reflection.TermEq.Simple in - let has_no_method_attr (b:binder) : bool = - L.existsb (term_eq (`no_method)) b.attrs - in - bs |> L.filter (fun b -> not (has_no_method_attr b)) - -private -let binder_set_meta (b : binder) (t : term) : binder = - { b with qual = Q_Meta t } - -[@@plugin] -let mk_class (nm:string) : Tac decls = - let ns = explode_qn nm in - let r = lookup_typ (top_env ()) ns in - guard (Some? r); - let Some se = r in - let to_propagate = L.filter (function Inline_for_extraction | NoExtract -> true | _ -> false) (sigelt_quals se) in - let sv = inspect_sigelt se in - guard (Sg_Inductive? sv); - let Sg_Inductive {nm=name;univs=us;params;typ=ity;ctors} = sv in - debug (fun () -> "params = " ^ Tactics.Util.string_of_list binder_to_string params); - debug (fun () -> "got it, name = " ^ implode_qn name); - debug (fun () -> "got it, ity = " ^ term_to_string ity); - let ctor_name = last name in - // Must have a single constructor - guard (L.length ctors = 1); - let [(c_name, ty)] = ctors in - debug (fun () -> "got ctor " ^ implode_qn c_name ^ " of type " ^ term_to_string ty); - let bs, cod = collect_arr_bs ty in - let r = inspect_comp cod in - guard (C_Total? r); - let C_Total cod = r in (* must be total *) - - debug (fun () -> "params = " ^ Tactics.Util.string_of_list binder_to_string params); - debug (fun () -> "n_params = " ^ string_of_int (List.Tot.Base.length params)); - debug (fun () -> "n_univs = " ^ string_of_int (List.Tot.Base.length us)); - debug (fun () -> "cod = " ^ term_to_string cod); - - (* print ("n_bs = " ^ string_of_int (List.Tot.Base.length bs)); *) - - let base : string = "__proj__Mk" ^ ctor_name ^ "__item__" in - - (* Make a sigelt for each method *) - filter_no_method_binders bs - |> Tactics.Util.map (fun (b:binder) -> - let s = name_of_binder b in - debug (fun () -> "processing method " ^ s); - let ns = cur_module () in - let sfv = pack_fv (ns @ [s]) in - let dbv = fresh_namedv_named "d" in - let tcr = (`tcresolve) in - let tcdict = { - ppname = seal "dict"; - sort = cod; - uniq = fresh(); - qual = Q_Meta tcr; - attrs = []; - } in - let proj_name = cur_module () @ [base ^ s] in - let proj = pack (Tv_FVar (pack_fv proj_name)) in - - let proj_lb = - match lookup_typ (top_env ()) proj_name with - | None -> fail "mk_class: proj not found?" - | Some se -> - match inspect_sigelt se with - | Sg_Let {lbs} -> lookup_lb lbs proj_name - | _ -> fail "mk_class: proj not Sg_Let?" - in - (* print ("proj_ty = " ^ term_to_string proj_lb.lb_typ); *) - - let ty = - let bs, cod = collect_arr_bs proj_lb.lb_typ in - let ps, bs = List.Tot.Base.splitAt (List.Tot.Base.length params) bs in - match bs with - | [] -> fail "mk_class: impossible, no binders" - | b1::bs' -> - let b1 = binder_set_meta b1 tcr in - mk_arr (ps@(b1::bs')) cod - in - let def = - let bs, body = collect_abs proj_lb.lb_def in - let ps, bs = List.Tot.Base.splitAt (List.Tot.Base.length params) bs in - match bs with - | [] -> fail "mk_class: impossible, no binders" - | b1::bs' -> - let b1 = binder_set_meta b1 tcr in - mk_abs (ps@(b1::bs')) body - in - debug (fun () -> "def = " ^ term_to_string def); - debug (fun () -> "ty = " ^ term_to_string ty); - - let ty : term = ty in - let def : term = def in - let sfv : fv = sfv in - - let lb = { lb_fv=sfv; lb_us=proj_lb.lb_us; lb_typ=ty; lb_def=def } in - let se = pack_sigelt (Sg_Let {isrec=false; lbs=[lb]}) in - let se = set_sigelt_quals to_propagate se in - let se = set_sigelt_attrs b.attrs se in - //debug (fun () -> "trying to return : " ^ term_to_string (quote se)); - se - ) diff --git a/ulib/FStar.Tactics.Typeclasses.fsti b/ulib/FStar.Tactics.Typeclasses.fsti index eac4b77fc7b..eb5eee4bfea 100644 --- a/ulib/FStar.Tactics.Typeclasses.fsti +++ b/ulib/FStar.Tactics.Typeclasses.fsti @@ -40,10 +40,8 @@ val no_method : unit run this tactics without having to know its definition in the .fst *) val tcresolve : unit -> Tac unit -(* The metaprogram to generate class methods. Also a plugin. This -is inserted automatically by the desugaring phase for any `class` -declaration. *) -val mk_class (nm:string) : Tac decls +(* NB: The generation of methods for a class is implemented in +FStar.Tactics.MkProjectors.fst *) (* Helper to solve an explicit argument by typeclass resolution *) [@@tcnorm]