diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_NamedView.ml b/ocaml/fstar-lib/generated/FStar_Tactics_NamedView.ml index 599dea5b83a..a72fb834740 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_NamedView.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_NamedView.ml @@ -4037,4 +4037,40 @@ let (pack_namedv : namedv -> namedv) = fun x -> x let (inspect_bv : bv -> bv) = fun x -> x let (pack_bv : bv -> bv) = fun x -> x let (inspect_comp : comp -> comp) = fun x -> x -let (pack_comp : comp -> comp) = fun x -> x \ No newline at end of file +let (pack_comp : comp -> comp) = fun x -> x +let (tag_of : term -> (Prims.string, unit) FStar_Tactics_Effect.tac_repr) = + fun t -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.NamedView.fsti" + (Prims.of_int (220)) (Prims.of_int (8)) (Prims.of_int (220)) + (Prims.of_int (17))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.NamedView.fsti" + (Prims.of_int (220)) (Prims.of_int (2)) (Prims.of_int (237)) + (Prims.of_int (28))))) (Obj.magic (inspect t)) + (fun uu___ -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___1 -> + match uu___ with + | Tv_Var bv1 -> "Tv_Var" + | Tv_BVar fv -> "Tv_BVar" + | Tv_FVar fv -> "Tv_FVar" + | Tv_UInst (uu___2, uu___3) -> "Tv_UInst" + | Tv_App (f, x) -> "Tv_App" + | Tv_Abs (x, t1) -> "Tv_Abs" + | Tv_Arrow (x, t1) -> "Tv_Arrow" + | Tv_Type uu___2 -> "Tv_Type" + | Tv_Refine (x, t1) -> "Tv_Refine" + | Tv_Const cst -> "Tv_Const" + | Tv_Uvar (i, t1) -> "Tv_Uvar" + | Tv_Let (r, attrs, b, t1, t2) -> "Tv_Let" + | Tv_Match (t1, uu___2, branches) -> "Tv_Match" + | Tv_AscribedT (uu___2, uu___3, uu___4, uu___5) -> + "Tv_AscribedT" + | Tv_AscribedC (uu___2, uu___3, uu___4, uu___5) -> + "Tv_AscribedC" + | Tv_Unknown -> "Tv_Unknown" + | Tv_Unsupp -> "Tv_Unsupp")) \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml b/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml index d24fd8c7f16..25c097c16f7 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_Typeclasses.ml @@ -1,8 +1,137 @@ open Prims +let (debug : + (unit -> (Prims.string, unit) FStar_Tactics_Effect.tac_repr) -> + (unit, unit) FStar_Tactics_Effect.tac_repr) + = + fun f -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (29)) (Prims.of_int (5)) (Prims.of_int (29)) + (Prims.of_int (17))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (29)) (Prims.of_int (2)) (Prims.of_int (30)) + (Prims.of_int (16))))) + (Obj.magic (FStar_Tactics_V2_Builtins.debugging ())) + (fun uu___ -> + (fun uu___ -> + if uu___ + then + 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 (30)) (Prims.of_int (10)) + (Prims.of_int (30)) (Prims.of_int (16))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (30)) (Prims.of_int (4)) + (Prims.of_int (30)) (Prims.of_int (16))))) + (Obj.magic (f ())) + (fun uu___1 -> + (fun uu___1 -> + Obj.magic + (FStar_Tactics_V2_Builtins.print uu___1)) + uu___1))) + else + Obj.magic + (Obj.repr + (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> ())))) + uu___) let op_At : 'uuuuu . unit -> 'uuuuu Prims.list -> 'uuuuu Prims.list -> 'uuuuu Prims.list = fun uu___ -> FStar_List_Tot_Base.op_At +let (fv_eq : + FStar_Reflection_Types.fv -> FStar_Reflection_Types.fv -> Prims.bool) = + fun fv1 -> + fun fv2 -> + let n1 = FStar_Reflection_V2_Builtins.inspect_fv fv1 in + let n2 = FStar_Reflection_V2_Builtins.inspect_fv fv2 in n1 = n2 +let rec (head_of : + FStar_Tactics_NamedView.term -> + (FStar_Reflection_Types.fv FStar_Pervasives_Native.option, unit) + FStar_Tactics_Effect.tac_repr) + = + fun t -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (57)) (Prims.of_int (8)) (Prims.of_int (57)) + (Prims.of_int (17))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (57)) (Prims.of_int (2)) (Prims.of_int (61)) + (Prims.of_int (13))))) + (Obj.magic (FStar_Tactics_NamedView.inspect t)) + (fun uu___ -> + (fun uu___ -> + match uu___ with + | FStar_Tactics_NamedView.Tv_FVar fv -> + Obj.magic + (Obj.repr + (FStar_Tactics_Effect.lift_div_tac + (fun uu___1 -> FStar_Pervasives_Native.Some fv))) + | FStar_Tactics_NamedView.Tv_UInst (fv, uu___1) -> + Obj.magic + (Obj.repr + (FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> FStar_Pervasives_Native.Some fv))) + | FStar_Tactics_NamedView.Tv_App (h, uu___1) -> + Obj.magic (Obj.repr (head_of h)) + | v -> + Obj.magic + (Obj.repr + (FStar_Tactics_Effect.lift_div_tac + (fun uu___1 -> FStar_Pervasives_Native.None)))) uu___) +let rec (res_typ : + FStar_Tactics_NamedView.term -> + (FStar_Tactics_NamedView.term, unit) FStar_Tactics_Effect.tac_repr) + = + fun t -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (64)) (Prims.of_int (8)) (Prims.of_int (64)) + (Prims.of_int (17))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (64)) (Prims.of_int (2)) (Prims.of_int (70)) + (Prims.of_int (10))))) + (Obj.magic (FStar_Tactics_NamedView.inspect t)) + (fun uu___ -> + (fun uu___ -> + match uu___ with + | FStar_Tactics_NamedView.Tv_Arrow (uu___1, c) -> + Obj.magic + (Obj.repr + (match FStar_Tactics_NamedView.inspect_comp c with + | FStar_Reflection_V2_Data.C_Total t1 -> + Obj.repr (res_typ t1) + | uu___2 -> + Obj.repr + (FStar_Tactics_Effect.lift_div_tac + (fun uu___3 -> t)))) + | uu___1 -> + Obj.magic + (Obj.repr + (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> t)))) + uu___) +exception NoInst +let (uu___is_NoInst : Prims.exn -> Prims.bool) = + fun projectee -> match projectee with | NoInst -> true | uu___ -> false let rec first : 'a 'b . ('a -> ('b, unit) FStar_Tactics_Effect.tac_repr) -> @@ -13,9 +142,7 @@ let rec first : (fun f -> fun l -> match l with - | [] -> - Obj.magic - (Obj.repr (FStar_Tactics_V2_Derived.fail "no cands")) + | [] -> Obj.magic (Obj.repr (FStar_Tactics_Effect.raise NoInst)) | x::xs -> Obj.magic (Obj.repr @@ -23,431 +150,632 @@ let rec first : (fun uu___ -> first f xs)))) uu___1 uu___ let rec (tcresolve' : FStar_Tactics_NamedView.term Prims.list -> - Prims.int -> (unit, unit) FStar_Tactics_Effect.tac_repr) + FStar_Reflection_Types.fv Prims.list -> + Prims.int -> (unit, unit) FStar_Tactics_Effect.tac_repr) = fun seen -> - fun fuel -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (52)) (Prims.of_int (4)) (Prims.of_int (53)) - (Prims.of_int (26))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (54)) (Prims.of_int (4)) (Prims.of_int (59)) - (Prims.of_int (137))))) - (if fuel <= Prims.int_zero - then FStar_Tactics_V2_Derived.fail "out of fuel" - else FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> ())) - (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 (54)) (Prims.of_int (4)) - (Prims.of_int (54)) (Prims.of_int (42))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (54)) (Prims.of_int (43)) - (Prims.of_int (59)) (Prims.of_int (137))))) - (Obj.magic - (FStar_Tactics_V2_Derived.debug - (Prims.strcat "fuel = " (Prims.string_of_int fuel)))) - (fun uu___1 -> - (fun uu___1 -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (55)) - (Prims.of_int (12)) - (Prims.of_int (55)) - (Prims.of_int (23))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (56)) (Prims.of_int (4)) - (Prims.of_int (59)) - (Prims.of_int (137))))) - (Obj.magic - (FStar_Tactics_V2_Derived.cur_goal ())) - (fun uu___2 -> - (fun g -> - Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (56)) - (Prims.of_int (4)) - (Prims.of_int (57)) - (Prims.of_int (17))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (57)) - (Prims.of_int (18)) - (Prims.of_int (59)) - (Prims.of_int (137))))) - (if - FStar_List_Tot_Base.existsb - (FStar_Reflection_V2_Builtins.term_eq - g) seen - then - FStar_Tactics_V2_Derived.fail - "loop" - else - FStar_Tactics_Effect.lift_div_tac - (fun uu___3 -> ())) - (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 (58)) - (Prims.of_int (15)) - (Prims.of_int (58)) - (Prims.of_int (24))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (59)) - (Prims.of_int (4)) - (Prims.of_int (59)) - (Prims.of_int (137))))) - (FStar_Tactics_Effect.lift_div_tac - (fun uu___3 -> g :: - seen)) - (fun uu___3 -> - (fun seen1 -> - Obj.magic - (FStar_Tactics_V2_Derived.or_else - (local seen1 - fuel) - (fun uu___3 -> - FStar_Tactics_V2_Derived.or_else - ( - global - seen1 - fuel) - ( - fun - uu___4 -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (59)) - (Prims.of_int (84)) - (Prims.of_int (59)) - (Prims.of_int (135))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (59)) - (Prims.of_int (79)) - (Prims.of_int (59)) - (Prims.of_int (135))))) - (Obj.magic + fun glb -> + fun fuel -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (96)) (Prims.of_int (4)) (Prims.of_int (97)) + (Prims.of_int (18))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (98)) (Prims.of_int (4)) + (Prims.of_int (113)) (Prims.of_int (34))))) + (if fuel <= Prims.int_zero + then FStar_Tactics_Effect.raise NoInst + else FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> ())) + (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 (98)) (Prims.of_int (4)) + (Prims.of_int (98)) (Prims.of_int (52))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (98)) (Prims.of_int (53)) + (Prims.of_int (113)) (Prims.of_int (34))))) + (Obj.magic + (debug + (fun uu___1 -> + (fun uu___1 -> + Obj.magic + (FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> + Prims.strcat "fuel = " + (Prims.string_of_int fuel)))) + uu___1))) + (fun uu___1 -> + (fun uu___1 -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (100)) + (Prims.of_int (12)) + (Prims.of_int (100)) + (Prims.of_int (23))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (103)) + (Prims.of_int (4)) + (Prims.of_int (113)) + (Prims.of_int (34))))) + (Obj.magic + (FStar_Tactics_V2_Derived.cur_goal ())) + (fun uu___2 -> + (fun g -> + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (103)) + (Prims.of_int (4)) + (Prims.of_int (104)) + (Prims.of_int (18))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (106)) + (Prims.of_int (4)) + (Prims.of_int (113)) + (Prims.of_int (34))))) + (if + FStar_List_Tot_Base.existsb + (FStar_Reflection_V2_TermEq.term_eq + g) seen + then + FStar_Tactics_Effect.raise + NoInst + else + FStar_Tactics_Effect.lift_div_tac + (fun uu___3 -> ())) + (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 (106)) + (Prims.of_int (10)) + (Prims.of_int (106)) + (Prims.of_int (19))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (106)) + (Prims.of_int (4)) + (Prims.of_int (113)) + (Prims.of_int (34))))) + (Obj.magic (head_of g)) + (fun uu___3 -> + (fun uu___3 -> + match uu___3 with + | FStar_Pervasives_Native.None + -> + Obj.magic + (Obj.repr + (FStar_Tactics_V2_Derived.fail + "goal does not look like a typeclass")) + | FStar_Pervasives_Native.Some + head_fv -> + 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 (59)) - (Prims.of_int (118)) - (Prims.of_int (59)) - (Prims.of_int (134))))) + (Prims.of_int (110)) + (Prims.of_int (17)) + (Prims.of_int (110)) + (Prims.of_int (26))))) (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 - g)) + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (111)) + (Prims.of_int (6)) + (Prims.of_int (113)) + (Prims.of_int (34))))) + (FStar_Tactics_Effect.lift_div_tac (fun - uu___5 -> - FStar_Tactics_Effect.lift_div_tac + uu___4 -> + g :: seen)) (fun - uu___6 -> - Prims.strcat - "could not solve constraint: " - uu___5)))) + uu___4 -> (fun - uu___5 -> - FStar_Tactics_V2_Derived.fail - uu___5))))) - uu___3))) uu___2))) - uu___2))) uu___1))) uu___) + seen1 -> + Obj.magic + (FStar_Tactics_V2_Derived.or_else + (local + head_fv + seen1 glb + fuel) + (global + head_fv + seen1 glb + fuel))) + uu___4)))) + uu___3))) uu___2))) + uu___2))) uu___1))) uu___) and (local : - FStar_Tactics_NamedView.term Prims.list -> - Prims.int -> unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) + FStar_Reflection_Types.fv -> + FStar_Tactics_NamedView.term Prims.list -> + FStar_Reflection_Types.fv Prims.list -> + Prims.int -> unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = - fun seen -> - fun fuel -> - fun uu___ -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (61)) (Prims.of_int (13)) - (Prims.of_int (61)) (Prims.of_int (37))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (62)) (Prims.of_int (4)) (Prims.of_int (62)) - (Prims.of_int (69))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (61)) (Prims.of_int (25)) - (Prims.of_int (61)) (Prims.of_int (37))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (61)) (Prims.of_int (13)) - (Prims.of_int (61)) (Prims.of_int (37))))) - (Obj.magic (FStar_Tactics_V2_Derived.cur_env ())) - (fun uu___1 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - FStar_Reflection_V2_Builtins.vars_of_env uu___1)))) - (fun uu___1 -> - (fun bs -> - Obj.magic - (first - (fun b -> - trywith seen fuel - (FStar_Tactics_NamedView.pack - (FStar_Tactics_NamedView.Tv_Var - (FStar_Tactics_V2_SyntaxCoercions.binding_to_namedv - b)))) bs)) uu___1) + fun head_fv -> + fun seen -> + fun glb -> + fun fuel -> + fun uu___ -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (116)) (Prims.of_int (13)) + (Prims.of_int (116)) (Prims.of_int (37))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (117)) (Prims.of_int (4)) + (Prims.of_int (119)) (Prims.of_int (12))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (116)) (Prims.of_int (25)) + (Prims.of_int (116)) (Prims.of_int (37))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (116)) (Prims.of_int (13)) + (Prims.of_int (116)) (Prims.of_int (37))))) + (Obj.magic (FStar_Tactics_V2_Derived.cur_env ())) + (fun uu___1 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___2 -> + FStar_Reflection_V2_Builtins.vars_of_env uu___1)))) + (fun uu___1 -> + (fun bs -> + Obj.magic + (first + (fun b -> + trywith head_fv seen glb fuel + (FStar_Tactics_NamedView.pack + (FStar_Tactics_NamedView.Tv_Var + (FStar_Tactics_V2_SyntaxCoercions.binding_to_namedv + b))) b.FStar_Reflection_V2_Data.sort3) + bs)) uu___1) and (global : - FStar_Tactics_NamedView.term Prims.list -> - Prims.int -> unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) + FStar_Reflection_Types.fv -> + FStar_Tactics_NamedView.term Prims.list -> + FStar_Reflection_Types.fv Prims.list -> + Prims.int -> unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = - fun seen -> - fun fuel -> - fun uu___ -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (64)) (Prims.of_int (16)) - (Prims.of_int (64)) (Prims.of_int (54))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (65)) (Prims.of_int (4)) (Prims.of_int (65)) - (Prims.of_int (65))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (64)) (Prims.of_int (42)) - (Prims.of_int (64)) (Prims.of_int (54))))) - (FStar_Sealed.seal + fun head_fv -> + fun seen -> + fun glb -> + fun fuel -> + fun uu___ -> + first + (fun fv -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (123)) (Prims.of_int (24)) + (Prims.of_int (123)) (Prims.of_int (58))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (124)) (Prims.of_int (14)) + (Prims.of_int (124)) (Prims.of_int (67))))) (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (64)) (Prims.of_int (16)) - (Prims.of_int (64)) (Prims.of_int (54))))) - (Obj.magic (FStar_Tactics_V2_Derived.cur_env ())) - (fun uu___1 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___2 -> - FStar_Reflection_V2_Builtins.lookup_attr - (FStar_Reflection_V2_Builtins.pack_ln - (FStar_Reflection_V2_Data.Tv_FVar - (FStar_Reflection_V2_Builtins.pack_fv - ["FStar"; - "Tactics"; - "Typeclasses"; - "tcinstance"]))) uu___1)))) - (fun uu___1 -> - (fun cands -> - Obj.magic - (first - (fun fv -> - trywith seen fuel - (FStar_Tactics_NamedView.pack - (FStar_Tactics_NamedView.Tv_FVar fv))) cands)) - uu___1) + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (123)) (Prims.of_int (27)) + (Prims.of_int (123)) (Prims.of_int (38))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (123)) (Prims.of_int (24)) + (Prims.of_int (123)) (Prims.of_int (58))))) + (Obj.magic (FStar_Tactics_V2_Derived.cur_env ())) + (fun uu___1 -> + (fun uu___1 -> + Obj.magic + (FStar_Tactics_V2_Builtins.tc uu___1 + (FStar_Tactics_NamedView.pack + (FStar_Tactics_NamedView.Tv_FVar fv)))) + uu___1))) + (fun uu___1 -> + (fun typ -> + Obj.magic + (trywith head_fv seen glb fuel + (FStar_Tactics_NamedView.pack + (FStar_Tactics_NamedView.Tv_FVar fv)) typ)) + uu___1)) glb and (trywith : - FStar_Tactics_NamedView.term Prims.list -> - Prims.int -> - FStar_Tactics_NamedView.term -> - (unit, unit) FStar_Tactics_Effect.tac_repr) + FStar_Reflection_Types.fv -> + FStar_Tactics_NamedView.term Prims.list -> + FStar_Reflection_Types.fv Prims.list -> + Prims.int -> + FStar_Tactics_NamedView.term -> + FStar_Tactics_NamedView.term -> + (unit, unit) FStar_Tactics_Effect.tac_repr) = - fun seen -> - fun fuel -> - fun t -> - FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (67)) (Prims.of_int (4)) (Prims.of_int (67)) - (Prims.of_int (70))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (68)) (Prims.of_int (4)) (Prims.of_int (68)) - (Prims.of_int (73))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind + fun head_fv -> + fun seen -> + fun glb -> + fun fuel -> + fun t -> + fun typ -> + FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (67)) (Prims.of_int (10)) - (Prims.of_int (67)) (Prims.of_int (70))))) + (Prims.of_int (128)) (Prims.of_int (10)) + (Prims.of_int (128)) (Prims.of_int (31))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (67)) (Prims.of_int (4)) - (Prims.of_int (67)) (Prims.of_int (70))))) + (Prims.of_int (128)) (Prims.of_int (4)) + (Prims.of_int (136)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (67)) (Prims.of_int (53)) - (Prims.of_int (67)) (Prims.of_int (69))))) + (Prims.of_int (128)) (Prims.of_int (18)) + (Prims.of_int (128)) (Prims.of_int (31))))) (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 t)) + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (128)) (Prims.of_int (10)) + (Prims.of_int (128)) (Prims.of_int (31))))) + (Obj.magic (res_typ typ)) (fun uu___ -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___1 -> - Prims.strcat - "Trying to apply hypothesis/instance: " uu___)))) + (fun uu___ -> Obj.magic (head_of uu___)) uu___))) (fun uu___ -> (fun uu___ -> - Obj.magic (FStar_Tactics_V2_Derived.debug uu___)) uu___))) - (fun uu___ -> - (fun uu___ -> - Obj.magic - (FStar_Tactics_V2_Derived.seq - (fun uu___1 -> FStar_Tactics_V2_Derived.apply_noinst t) - (fun uu___1 -> tcresolve' seen (fuel - Prims.int_one)))) - uu___) + match uu___ with + | FStar_Pervasives_Native.None -> + Obj.magic + (Obj.repr (FStar_Tactics_Effect.raise NoInst)) + | FStar_Pervasives_Native.Some fv' -> + Obj.magic + (Obj.repr + (if fv_eq fv' head_fv + then + Obj.repr + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (133)) + (Prims.of_int (8)) + (Prims.of_int (133)) + (Prims.of_int (84))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (134)) + (Prims.of_int (8)) + (Prims.of_int (134)) + (Prims.of_int (81))))) + (Obj.magic + (debug + (fun uu___1 -> + FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (133)) + (Prims.of_int (67)) + (Prims.of_int (133)) + (Prims.of_int (83))))) + (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 + t)) + (fun uu___2 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___3 -> + Prims.strcat + "Trying to apply hypothesis/instance: " + uu___2))))) + (fun uu___1 -> + (fun uu___1 -> + Obj.magic + (FStar_Tactics_V2_Derived.seq + (fun uu___2 -> + FStar_Tactics_V2_Derived.apply_noinst + t) + (fun uu___2 -> + tcresolve' seen glb + (fuel - Prims.int_one)))) + uu___1)) + else + Obj.repr + (FStar_Tactics_Effect.raise NoInst)))) + uu___) let rec (maybe_intros : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = fun uu___ -> FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (72)) (Prims.of_int (10)) (Prims.of_int (72)) + (Prims.of_int (140)) (Prims.of_int (10)) (Prims.of_int (140)) (Prims.of_int (21))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (73)) (Prims.of_int (2)) (Prims.of_int (77)) + (Prims.of_int (141)) (Prims.of_int (2)) (Prims.of_int (145)) (Prims.of_int (11))))) (Obj.magic (FStar_Tactics_V2_Derived.cur_goal ())) (fun uu___1 -> (fun g -> - match FStar_Reflection_V2_Builtins.inspect_ln g with - | FStar_Reflection_V2_Data.Tv_Arrow (uu___1, uu___2) -> - 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 (75)) (Prims.of_int (4)) - (Prims.of_int (75)) (Prims.of_int (21))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (76)) (Prims.of_int (4)) - (Prims.of_int (76)) (Prims.of_int (19))))) - (Obj.magic - (FStar_Tactics_Effect.tac_bind - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (75)) - (Prims.of_int (11)) - (Prims.of_int (75)) - (Prims.of_int (21))))) - (FStar_Sealed.seal - (Obj.magic - (FStar_Range.mk_range - "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (75)) (Prims.of_int (4)) - (Prims.of_int (75)) - (Prims.of_int (21))))) - (Obj.magic (FStar_Tactics_V2_Builtins.intro ())) - (fun uu___3 -> - FStar_Tactics_Effect.lift_div_tac - (fun uu___4 -> ())))) - (fun uu___3 -> - (fun uu___3 -> Obj.magic (maybe_intros ())) uu___3))) - | uu___1 -> - Obj.magic - (Obj.repr - (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> ())))) - uu___1) + Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (141)) (Prims.of_int (8)) + (Prims.of_int (141)) (Prims.of_int (17))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (141)) (Prims.of_int (2)) + (Prims.of_int (145)) (Prims.of_int (11))))) + (Obj.magic (FStar_Tactics_NamedView.inspect g)) + (fun uu___1 -> + (fun uu___1 -> + match uu___1 with + | FStar_Tactics_NamedView.Tv_Arrow (uu___2, uu___3) -> + 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 (143)) + (Prims.of_int (4)) + (Prims.of_int (143)) + (Prims.of_int (21))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (144)) + (Prims.of_int (4)) + (Prims.of_int (144)) + (Prims.of_int (19))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (143)) + (Prims.of_int (11)) + (Prims.of_int (143)) + (Prims.of_int (21))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (143)) + (Prims.of_int (4)) + (Prims.of_int (143)) + (Prims.of_int (21))))) + (Obj.magic + (FStar_Tactics_V2_Builtins.intro + ())) + (fun uu___4 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___5 -> ())))) + (fun uu___4 -> + (fun uu___4 -> + Obj.magic (maybe_intros ())) uu___4))) + | uu___2 -> + Obj.magic + (Obj.repr + (FStar_Tactics_Effect.lift_div_tac + (fun uu___3 -> ())))) uu___1))) uu___1) let (tcresolve : unit -> (unit, unit) FStar_Tactics_Effect.tac_repr) = fun uu___ -> FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (84)) (Prims.of_int (4)) (Prims.of_int (84)) + (Prims.of_int (153)) (Prims.of_int (4)) (Prims.of_int (153)) (Prims.of_int (19))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (85)) (Prims.of_int (4)) (Prims.of_int (88)) + (Prims.of_int (153)) (Prims.of_int (20)) (Prims.of_int (166)) (Prims.of_int (18))))) (Obj.magic (maybe_intros ())) (fun uu___1 -> (fun uu___1 -> Obj.magic - (FStar_Tactics_V2_Derived.try_with - (fun uu___2 -> - match () with | () -> tcresolve' [] (Prims.of_int (16))) + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (158)) (Prims.of_int (14)) + (Prims.of_int (158)) (Prims.of_int (52))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (159)) (Prims.of_int (4)) + (Prims.of_int (166)) (Prims.of_int (18))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (158)) (Prims.of_int (40)) + (Prims.of_int (158)) (Prims.of_int (52))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (158)) (Prims.of_int (14)) + (Prims.of_int (158)) (Prims.of_int (52))))) + (Obj.magic (FStar_Tactics_V2_Derived.cur_env ())) + (fun uu___2 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___3 -> + FStar_Reflection_V2_Builtins.lookup_attr + (FStar_Reflection_V2_Builtins.pack_ln + (FStar_Reflection_V2_Data.Tv_FVar + (FStar_Reflection_V2_Builtins.pack_fv + ["FStar"; + "Tactics"; + "Typeclasses"; + "tcinstance"]))) uu___2)))) (fun uu___2 -> - (fun uu___2 -> - match uu___2 with - | FStar_Tactics_Common.TacticFailure s -> - Obj.magic - (FStar_Tactics_V2_Derived.fail - (Prims.strcat "Typeclass resolution failed: " - s)) - | e -> Obj.magic (FStar_Tactics_Effect.raise e)) - uu___2))) uu___1) + (fun glb -> + Obj.magic + (FStar_Tactics_V2_Derived.try_with + (fun uu___2 -> + match () with + | () -> tcresolve' [] glb (Prims.of_int (16))) + (fun uu___2 -> + (fun uu___2 -> + match uu___2 with + | NoInst -> + 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 (163)) + (Prims.of_int (11)) + (Prims.of_int (163)) + (Prims.of_int (73))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (163)) + (Prims.of_int (6)) + (Prims.of_int (163)) + (Prims.of_int (73))))) + (Obj.magic + (FStar_Tactics_Effect.tac_bind + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (163)) + (Prims.of_int (44)) + (Prims.of_int (163)) + (Prims.of_int (72))))) + (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 (163)) + (Prims.of_int (59)) + (Prims.of_int (163)) + (Prims.of_int (72))))) + (FStar_Sealed.seal + (Obj.magic + (FStar_Range.mk_range + "FStar.Tactics.Typeclasses.fst" + (Prims.of_int (163)) + (Prims.of_int (44)) + (Prims.of_int (163)) + (Prims.of_int (72))))) + (Obj.magic + (FStar_Tactics_V2_Derived.cur_goal + ())) + (fun uu___3 -> + (fun uu___3 -> + Obj.magic + (FStar_Tactics_V2_Builtins.term_to_string + uu___3)) + uu___3))) + (fun uu___3 -> + FStar_Tactics_Effect.lift_div_tac + (fun uu___4 -> + Prims.strcat + "Could not solve constraint " + uu___3)))) + (fun uu___3 -> + FStar_Tactics_V2_Derived.fail + uu___3))) + | FStar_Tactics_Common.TacticFailure s -> + Obj.magic + (Obj.repr + (FStar_Tactics_V2_Derived.fail + (Prims.strcat + "Typeclass resolution failed: " + s))) + | e -> + Obj.magic + (Obj.repr + (FStar_Tactics_Effect.raise e))) + uu___2))) uu___2))) uu___1) let _ = FStar_Tactics_Native.register_tactic "FStar.Tactics.Typeclasses.tcresolve" (Prims.of_int (2)) @@ -481,8 +809,8 @@ let rec (mk_abs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (97)) (Prims.of_int (20)) - (Prims.of_int (97)) (Prims.of_int (47))))) + (Prims.of_int (175)) (Prims.of_int (20)) + (Prims.of_int (175)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "dummy" Prims.int_zero @@ -493,14 +821,18 @@ let rec (mk_abs : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (97)) (Prims.of_int (30)) - (Prims.of_int (97)) (Prims.of_int (46))))) + (Prims.of_int (175)) + (Prims.of_int (30)) + (Prims.of_int (175)) + (Prims.of_int (46))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (97)) (Prims.of_int (20)) - (Prims.of_int (97)) (Prims.of_int (47))))) + (Prims.of_int (175)) + (Prims.of_int (20)) + (Prims.of_int (175)) + (Prims.of_int (47))))) (Obj.magic (mk_abs bs1 body)) (fun uu___ -> FStar_Tactics_Effect.lift_div_tac @@ -561,12 +893,12 @@ let (mk_class : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (130)) (Prims.of_int (13)) (Prims.of_int (130)) + (Prims.of_int (208)) (Prims.of_int (13)) (Prims.of_int (208)) (Prims.of_int (26))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (130)) (Prims.of_int (29)) (Prims.of_int (218)) + (Prims.of_int (208)) (Prims.of_int (29)) (Prims.of_int (296)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___ -> FStar_Reflection_V2_Builtins.explode_qn nm)) @@ -577,27 +909,27 @@ let (mk_class : (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (131)) (Prims.of_int (12)) - (Prims.of_int (131)) (Prims.of_int (38))))) + (Prims.of_int (209)) (Prims.of_int (12)) + (Prims.of_int (209)) (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (132)) (Prims.of_int (4)) - (Prims.of_int (218)) (Prims.of_int (35))))) + (Prims.of_int (210)) (Prims.of_int (4)) + (Prims.of_int (296)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_Effect.tac_bind (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (131)) (Prims.of_int (23)) - (Prims.of_int (131)) (Prims.of_int (35))))) + (Prims.of_int (209)) (Prims.of_int (23)) + (Prims.of_int (209)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (131)) (Prims.of_int (12)) - (Prims.of_int (131)) (Prims.of_int (38))))) + (Prims.of_int (209)) (Prims.of_int (12)) + (Prims.of_int (209)) (Prims.of_int (38))))) (Obj.magic (FStar_Tactics_V2_Builtins.top_env ())) (fun uu___ -> FStar_Tactics_Effect.lift_div_tac @@ -612,14 +944,14 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (132)) (Prims.of_int (4)) - (Prims.of_int (132)) (Prims.of_int (19))))) + (Prims.of_int (210)) (Prims.of_int (4)) + (Prims.of_int (210)) (Prims.of_int (19))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (132)) (Prims.of_int (20)) - (Prims.of_int (218)) (Prims.of_int (35))))) + (Prims.of_int (210)) (Prims.of_int (20)) + (Prims.of_int (296)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_Derived.guard (FStar_Pervasives_Native.uu___is_Some r))) @@ -631,17 +963,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (133)) + (Prims.of_int (211)) (Prims.of_int (18)) - (Prims.of_int (133)) + (Prims.of_int (211)) (Prims.of_int (19))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (132)) + (Prims.of_int (210)) (Prims.of_int (20)) - (Prims.of_int (218)) + (Prims.of_int (296)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___1 -> r)) @@ -656,17 +988,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (134)) + (Prims.of_int (212)) (Prims.of_int (23)) - (Prims.of_int (134)) + (Prims.of_int (212)) (Prims.of_int (115))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (134)) + (Prims.of_int (212)) (Prims.of_int (118)) - (Prims.of_int (218)) + (Prims.of_int (296)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun uu___2 -> @@ -691,18 +1023,18 @@ let (mk_class : Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (135)) + (Prims.of_int (213)) (Prims.of_int (13)) - (Prims.of_int (135)) + (Prims.of_int (213)) (Prims.of_int (30))))) (FStar_Sealed.seal ( Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (136)) + (Prims.of_int (214)) (Prims.of_int (4)) - (Prims.of_int (218)) + (Prims.of_int (296)) (Prims.of_int (35))))) (Obj.magic ( @@ -718,17 +1050,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (136)) + (Prims.of_int (214)) (Prims.of_int (4)) - (Prims.of_int (136)) + (Prims.of_int (214)) (Prims.of_int (28))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (136)) + (Prims.of_int (214)) (Prims.of_int (29)) - (Prims.of_int (218)) + (Prims.of_int (296)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_Derived.guard @@ -744,17 +1076,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (137)) + (Prims.of_int (215)) (Prims.of_int (63)) - (Prims.of_int (137)) + (Prims.of_int (215)) (Prims.of_int (65))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (136)) + (Prims.of_int (214)) (Prims.of_int (29)) - (Prims.of_int (218)) + (Prims.of_int (296)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -786,17 +1118,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (141)) + (Prims.of_int (219)) (Prims.of_int (20)) - (Prims.of_int (141)) + (Prims.of_int (219)) (Prims.of_int (29))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (143)) + (Prims.of_int (221)) (Prims.of_int (4)) - (Prims.of_int (218)) + (Prims.of_int (296)) (Prims.of_int (35))))) (Obj.magic (last @@ -812,17 +1144,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (143)) + (Prims.of_int (221)) (Prims.of_int (4)) - (Prims.of_int (143)) + (Prims.of_int (221)) (Prims.of_int (30))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (143)) + (Prims.of_int (221)) (Prims.of_int (31)) - (Prims.of_int (218)) + (Prims.of_int (296)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_Derived.guard @@ -839,17 +1171,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (144)) + (Prims.of_int (222)) (Prims.of_int (25)) - (Prims.of_int (144)) + (Prims.of_int (222)) (Prims.of_int (30))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (143)) + (Prims.of_int (221)) (Prims.of_int (31)) - (Prims.of_int (218)) + (Prims.of_int (296)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -871,17 +1203,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (146)) + (Prims.of_int (224)) (Prims.of_int (18)) - (Prims.of_int (146)) + (Prims.of_int (224)) (Prims.of_int (35))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (144)) + (Prims.of_int (222)) (Prims.of_int (33)) - (Prims.of_int (218)) + (Prims.of_int (296)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_SyntaxHelpers.collect_arr_bs @@ -901,17 +1233,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (147)) + (Prims.of_int (225)) (Prims.of_int (12)) - (Prims.of_int (147)) + (Prims.of_int (225)) (Prims.of_int (28))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (148)) + (Prims.of_int (226)) (Prims.of_int (4)) - (Prims.of_int (218)) + (Prims.of_int (296)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -928,17 +1260,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (148)) + (Prims.of_int (226)) (Prims.of_int (4)) - (Prims.of_int (148)) + (Prims.of_int (226)) (Prims.of_int (22))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (148)) + (Prims.of_int (226)) (Prims.of_int (23)) - (Prims.of_int (218)) + (Prims.of_int (296)) (Prims.of_int (35))))) (Obj.magic (FStar_Tactics_V2_Derived.guard @@ -954,17 +1286,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (149)) + (Prims.of_int (227)) (Prims.of_int (22)) - (Prims.of_int (149)) + (Prims.of_int (227)) (Prims.of_int (23))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (148)) + (Prims.of_int (226)) (Prims.of_int (23)) - (Prims.of_int (218)) + (Prims.of_int (296)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -985,17 +1317,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (158)) + (Prims.of_int (236)) (Prims.of_int (24)) - (Prims.of_int (158)) + (Prims.of_int (236)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (161)) + (Prims.of_int (239)) (Prims.of_int (4)) - (Prims.of_int (218)) + (Prims.of_int (296)) (Prims.of_int (35))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1017,17 +1349,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (162)) + (Prims.of_int (240)) (Prims.of_int (26)) - (Prims.of_int (162)) + (Prims.of_int (240)) (Prims.of_int (42))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (162)) + (Prims.of_int (240)) (Prims.of_int (45)) - (Prims.of_int (217)) + (Prims.of_int (295)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_V2_Derived.name_of_binder @@ -1041,17 +1373,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (163)) + (Prims.of_int (241)) (Prims.of_int (27)) - (Prims.of_int (163)) + (Prims.of_int (241)) (Prims.of_int (40))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (163)) + (Prims.of_int (241)) (Prims.of_int (43)) - (Prims.of_int (217)) + (Prims.of_int (295)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_V2_Derived.cur_module @@ -1066,17 +1398,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (164)) + (Prims.of_int (242)) (Prims.of_int (28)) - (Prims.of_int (164)) + (Prims.of_int (242)) (Prims.of_int (46))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (164)) + (Prims.of_int (242)) (Prims.of_int (49)) - (Prims.of_int (217)) + (Prims.of_int (295)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1095,17 +1427,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (165)) + (Prims.of_int (243)) (Prims.of_int (28)) - (Prims.of_int (165)) + (Prims.of_int (243)) (Prims.of_int (50))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (165)) + (Prims.of_int (243)) (Prims.of_int (53)) - (Prims.of_int (217)) + (Prims.of_int (295)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_V2_Derived.fresh_namedv_named @@ -1120,17 +1452,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (166)) + (Prims.of_int (244)) (Prims.of_int (28)) - (Prims.of_int (166)) + (Prims.of_int (244)) (Prims.of_int (40))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (166)) + (Prims.of_int (244)) (Prims.of_int (43)) - (Prims.of_int (217)) + (Prims.of_int (295)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1152,17 +1484,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (168)) + (Prims.of_int (246)) (Prims.of_int (20)) - (Prims.of_int (172)) + (Prims.of_int (250)) (Prims.of_int (32))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (173)) + (Prims.of_int (251)) (Prims.of_int (22)) - (Prims.of_int (217)) + (Prims.of_int (295)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1170,17 +1502,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (170)) + (Prims.of_int (248)) (Prims.of_int (29)) - (Prims.of_int (170)) + (Prims.of_int (248)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (168)) + (Prims.of_int (246)) (Prims.of_int (20)) - (Prims.of_int (172)) + (Prims.of_int (250)) (Prims.of_int (32))))) (Obj.magic (FStar_Tactics_V2_Builtins.fresh @@ -1217,17 +1549,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (174)) + (Prims.of_int (252)) (Prims.of_int (34)) - (Prims.of_int (174)) + (Prims.of_int (252)) (Prims.of_int (60))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (174)) + (Prims.of_int (252)) (Prims.of_int (63)) - (Prims.of_int (217)) + (Prims.of_int (295)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1235,17 +1567,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (174)) + (Prims.of_int (252)) (Prims.of_int (34)) - (Prims.of_int (174)) + (Prims.of_int (252)) (Prims.of_int (47))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (174)) + (Prims.of_int (252)) (Prims.of_int (34)) - (Prims.of_int (174)) + (Prims.of_int (252)) (Prims.of_int (60))))) (Obj.magic (FStar_Tactics_V2_Derived.cur_module @@ -1272,17 +1604,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (175)) + (Prims.of_int (253)) (Prims.of_int (29)) - (Prims.of_int (175)) + (Prims.of_int (253)) (Prims.of_int (63))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (175)) + (Prims.of_int (253)) (Prims.of_int (66)) - (Prims.of_int (217)) + (Prims.of_int (295)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1301,17 +1633,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (178)) + (Prims.of_int (256)) (Prims.of_int (20)) - (Prims.of_int (183)) + (Prims.of_int (261)) (Prims.of_int (62))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (184)) + (Prims.of_int (262)) (Prims.of_int (20)) - (Prims.of_int (217)) + (Prims.of_int (295)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1319,17 +1651,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (178)) + (Prims.of_int (256)) (Prims.of_int (26)) - (Prims.of_int (178)) + (Prims.of_int (256)) (Prims.of_int (59))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (178)) + (Prims.of_int (256)) (Prims.of_int (20)) - (Prims.of_int (183)) + (Prims.of_int (261)) (Prims.of_int (62))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1337,17 +1669,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (178)) + (Prims.of_int (256)) (Prims.of_int (37)) - (Prims.of_int (178)) + (Prims.of_int (256)) (Prims.of_int (49))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (178)) + (Prims.of_int (256)) (Prims.of_int (26)) - (Prims.of_int (178)) + (Prims.of_int (256)) (Prims.of_int (59))))) (Obj.magic (FStar_Tactics_V2_Builtins.top_env @@ -1384,17 +1716,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (181)) + (Prims.of_int (259)) (Prims.of_int (28)) - (Prims.of_int (181)) + (Prims.of_int (259)) (Prims.of_int (45))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (181)) + (Prims.of_int (259)) (Prims.of_int (22)) - (Prims.of_int (183)) + (Prims.of_int (261)) (Prims.of_int (62))))) (Obj.magic (FStar_Tactics_NamedView.inspect_sigelt @@ -1440,17 +1772,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (187)) + (Prims.of_int (265)) (Prims.of_int (26)) - (Prims.of_int (194)) + (Prims.of_int (272)) (Prims.of_int (49))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (195)) + (Prims.of_int (273)) (Prims.of_int (20)) - (Prims.of_int (217)) + (Prims.of_int (295)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1458,17 +1790,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (188)) + (Prims.of_int (266)) (Prims.of_int (34)) - (Prims.of_int (188)) + (Prims.of_int (266)) (Prims.of_int (63))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (187)) + (Prims.of_int (265)) (Prims.of_int (26)) - (Prims.of_int (194)) + (Prims.of_int (272)) (Prims.of_int (49))))) (Obj.magic (FStar_Tactics_V2_SyntaxHelpers.collect_arr_bs @@ -1488,17 +1820,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (189)) + (Prims.of_int (267)) (Prims.of_int (33)) - (Prims.of_int (189)) + (Prims.of_int (267)) (Prims.of_int (87))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (188)) + (Prims.of_int (266)) (Prims.of_int (66)) - (Prims.of_int (194)) + (Prims.of_int (272)) (Prims.of_int (49))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1537,17 +1869,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (193)) + (Prims.of_int (271)) (Prims.of_int (33)) - (Prims.of_int (193)) + (Prims.of_int (271)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (194)) + (Prims.of_int (272)) (Prims.of_int (24)) - (Prims.of_int (194)) + (Prims.of_int (272)) (Prims.of_int (49))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1580,17 +1912,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (196)) + (Prims.of_int (274)) (Prims.of_int (27)) - (Prims.of_int (203)) + (Prims.of_int (281)) (Prims.of_int (50))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (204)) + (Prims.of_int (282)) (Prims.of_int (20)) - (Prims.of_int (217)) + (Prims.of_int (295)) (Prims.of_int (20))))) (Obj.magic (FStar_Tactics_Effect.tac_bind @@ -1598,17 +1930,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (197)) + (Prims.of_int (275)) (Prims.of_int (35)) - (Prims.of_int (197)) + (Prims.of_int (275)) (Prims.of_int (61))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (196)) + (Prims.of_int (274)) (Prims.of_int (27)) - (Prims.of_int (203)) + (Prims.of_int (281)) (Prims.of_int (50))))) (Obj.magic (FStar_Tactics_V2_SyntaxHelpers.collect_abs @@ -1628,17 +1960,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (198)) + (Prims.of_int (276)) (Prims.of_int (33)) - (Prims.of_int (198)) + (Prims.of_int (276)) (Prims.of_int (87))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (197)) + (Prims.of_int (275)) (Prims.of_int (64)) - (Prims.of_int (203)) + (Prims.of_int (281)) (Prims.of_int (50))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1677,17 +2009,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (202)) + (Prims.of_int (280)) (Prims.of_int (33)) - (Prims.of_int (202)) + (Prims.of_int (280)) (Prims.of_int (55))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (203)) + (Prims.of_int (281)) (Prims.of_int (24)) - (Prims.of_int (203)) + (Prims.of_int (281)) (Prims.of_int (50))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1720,17 +2052,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (208)) + (Prims.of_int (286)) (Prims.of_int (34)) - (Prims.of_int (208)) + (Prims.of_int (286)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (208)) + (Prims.of_int (286)) (Prims.of_int (39)) - (Prims.of_int (217)) + (Prims.of_int (295)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1746,17 +2078,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (209)) + (Prims.of_int (287)) (Prims.of_int (35)) - (Prims.of_int (209)) + (Prims.of_int (287)) (Prims.of_int (38))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (209)) + (Prims.of_int (287)) (Prims.of_int (41)) - (Prims.of_int (217)) + (Prims.of_int (295)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1772,17 +2104,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (210)) + (Prims.of_int (288)) (Prims.of_int (33)) - (Prims.of_int (210)) + (Prims.of_int (288)) (Prims.of_int (36))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (210)) + (Prims.of_int (288)) (Prims.of_int (39)) - (Prims.of_int (217)) + (Prims.of_int (295)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1798,17 +2130,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (212)) + (Prims.of_int (290)) (Prims.of_int (29)) - (Prims.of_int (212)) + (Prims.of_int (290)) (Prims.of_int (82))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (212)) + (Prims.of_int (290)) (Prims.of_int (87)) - (Prims.of_int (217)) + (Prims.of_int (295)) (Prims.of_int (20))))) (FStar_Tactics_Effect.lift_div_tac (fun @@ -1834,17 +2166,17 @@ let (mk_class : (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (213)) + (Prims.of_int (291)) (Prims.of_int (27)) - (Prims.of_int (213)) + (Prims.of_int (291)) (Prims.of_int (71))))) (FStar_Sealed.seal (Obj.magic (FStar_Range.mk_range "FStar.Tactics.Typeclasses.fst" - (Prims.of_int (215)) + (Prims.of_int (293)) (Prims.of_int (27)) - (Prims.of_int (215)) + (Prims.of_int (293)) (Prims.of_int (54))))) (Obj.magic (FStar_Tactics_NamedView.pack_sigelt diff --git a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml index c352337593d..cb7d3fb6742 100644 --- a/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml +++ b/ocaml/fstar-lib/generated/FStar_Tactics_V2_Interpreter.ml @@ -197,8 +197,8 @@ let (__primitive_steps_ref : let (primitive_steps : unit -> FStar_TypeChecker_Primops.primitive_step Prims.list) = fun uu___ -> - let uu___1 = FStar_Compiler_Effect.op_Bang __primitive_steps_ref in - let uu___2 = native_tactics_steps () in + let uu___1 = native_tactics_steps () in + let uu___2 = FStar_Compiler_Effect.op_Bang __primitive_steps_ref in FStar_Compiler_List.op_At uu___1 uu___2 let (register_tactic_primitive_step : FStar_TypeChecker_Primops.primitive_step -> unit) = diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml index fc44af89e57..d8fbbf6ddd2 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Tc.ml @@ -4929,7 +4929,9 @@ let (tc_decls : | (uu___2, env1) -> let r = let uu___3 = - let uu___4 = FStar_Syntax_Print.sigelt_to_string_short se in + let uu___4 = + let uu___5 = FStar_TypeChecker_Env.current_module env1 in + FStar_Ident.string_of_lid uu___5 in FStar_Pervasives_Native.Some uu___4 in FStar_Profiling.profile (fun uu___4 -> process_one_decl acc se) uu___3 diff --git a/src/tactics/FStar.Tactics.V2.Interpreter.fst b/src/tactics/FStar.Tactics.V2.Interpreter.fst index 36c0159ff05..4a29910cf06 100644 --- a/src/tactics/FStar.Tactics.V2.Interpreter.fst +++ b/src/tactics/FStar.Tactics.V2.Interpreter.fst @@ -99,8 +99,8 @@ let __primitive_steps_ref : ref (list PO.primitive_step) = BU.mk_ref [] let primitive_steps () : list PO.primitive_step = - (!__primitive_steps_ref) - @ (native_tactics_steps ()) + (native_tactics_steps ()) + @ (!__primitive_steps_ref) let register_tactic_primitive_step (s : PO.primitive_step) : unit = __primitive_steps_ref := s :: !__primitive_steps_ref diff --git a/src/typechecker/FStar.TypeChecker.Tc.fst b/src/typechecker/FStar.TypeChecker.Tc.fst index 3935c5ab090..17593146b2d 100644 --- a/src/typechecker/FStar.TypeChecker.Tc.fst +++ b/src/typechecker/FStar.TypeChecker.Tc.fst @@ -1110,7 +1110,7 @@ let tc_decls env ses = let r = Profiling.profile (fun () -> process_one_decl acc se) - (Some (Print.sigelt_to_string_short se)) + (Some (Ident.string_of_lid (Env.current_module env))) "FStar.TypeChecker.Tc.process_one_decl" // ^ See a special case for this phase in FStar.Options. --timing // enables it. diff --git a/ulib/FStar.Tactics.NamedView.fsti b/ulib/FStar.Tactics.NamedView.fsti index ecb8e5a2227..ce8c5f6fb26 100644 --- a/ulib/FStar.Tactics.NamedView.fsti +++ b/ulib/FStar.Tactics.NamedView.fsti @@ -215,3 +215,23 @@ let inspect_bv = id #bv let pack_bv = id #bv let inspect_comp = id #comp let pack_comp = id #comp + +let tag_of (t:term) : Tac string = + match inspect t with + | Tv_Var bv -> "Tv_Var" + | Tv_BVar fv -> "Tv_BVar" + | Tv_FVar fv -> "Tv_FVar" + | Tv_UInst _ _ -> "Tv_UInst" + | Tv_App f x -> "Tv_App" + | Tv_Abs x t -> "Tv_Abs" + | Tv_Arrow x t -> "Tv_Arrow" + | Tv_Type _ -> "Tv_Type" + | Tv_Refine x t -> "Tv_Refine" + | Tv_Const cst -> "Tv_Const" + | Tv_Uvar i t -> "Tv_Uvar" + | Tv_Let r attrs b t1 t2 -> "Tv_Let" + | Tv_Match t _ branches -> "Tv_Match" + | Tv_AscribedT _ _ _ _ -> "Tv_AscribedT" + | Tv_AscribedC _ _ _ _ -> "Tv_AscribedC" + | Tv_Unknown -> "Tv_Unknown" + | Tv_Unsupp -> "Tv_Unsupp" diff --git a/ulib/FStar.Tactics.Typeclasses.fst b/ulib/FStar.Tactics.Typeclasses.fst index ab0297a0ba6..dd997c149f4 100644 --- a/ulib/FStar.Tactics.Typeclasses.fst +++ b/ulib/FStar.Tactics.Typeclasses.fst @@ -24,6 +24,11 @@ open FStar.Tactics.V2.Derived open FStar.Tactics.V2.SyntaxCoercions open FStar.Tactics.NamedView +(* Thunked version of debug *) +let debug (f : unit -> Tac string) : Tac unit = + if debugging () then + print (f ()) + module L = FStar.List.Tot.Base let (@) = L.op_At @@ -40,51 +45,124 @@ let tcinstance : unit = () irreducible let no_method : unit = () +val fv_eq : fv -> fv -> Tot bool +let fv_eq fv1 fv2 = + let n1 = inspect_fv fv1 in + let n2 = inspect_fv fv2 in + n1 = n2 + +let rec head_of (t:term) : Tac (option fv) = + (* NB: must use `inspect` to make use of unionfind graph. + inspect_ln won't work. *) + match inspect t with + | Tv_FVar fv + | Tv_UInst fv _ -> Some fv + | Tv_App h _ -> head_of h + | v -> None + +let rec res_typ (t:term) : Tac term = + match inspect t with + | Tv_Arrow _ c -> ( + match inspect_comp c with + | C_Total t -> res_typ t + | _ -> t + ) + | _ -> t + +(* Would be good to use different exceptions for each reason +the search stops, but it takes some work to properly account +for them and report proper errors. *) +exception NoInst + private let rec first (f : 'a -> Tac 'b) (l : list 'a) : Tac 'b = match l with - | [] -> fail "no cands" + | [] -> raise NoInst | x::xs -> (fun () -> f x) `or_else` (fun () -> first f xs) -(* TODO: memoization?. And better errors. *) +(* + tcresolve': the main typeclass instantiation function. + + seen : a list of goals we've seen already in this path of the search, + used to prevent loops + glb : a list of all global instances in scope, for all classes + fuel : amount of steps we allow in this path, we stop if we reach zero + head_fv : the head of the goal we're trying to solve, i.e. the class name + + TODO: some form of memoization +*) private -let rec tcresolve' (seen:list term) (fuel:int) : Tac unit = +let rec tcresolve' (seen : list term) (glb : list fv) (fuel : int) : Tac unit = if fuel <= 0 then - fail "out of fuel"; - debug ("fuel = " ^ string_of_int fuel); + raise NoInst; + debug (fun () -> "fuel = " ^ string_of_int fuel); + let g = cur_goal () in - if L.existsb (term_eq g) seen then - fail "loop"; - let seen = g :: seen in - local seen fuel `or_else` (fun () -> global seen fuel `or_else` (fun () -> fail ("could not solve constraint: " ^ term_to_string g))) -and local (seen:list term) (fuel:int) () : Tac unit = + + (* Try to detect loops *) + if L.existsb (Reflection.V2.TermEq.term_eq g) seen then + raise NoInst; + + match head_of g with + | None -> fail ("goal does not look like a typeclass") + | Some head_fv -> + (* ^ Maybe should check is this really is a class too? *) + let seen = g :: seen in + local head_fv seen glb fuel + `or_else` + global head_fv seen glb fuel + +and local (head_fv : fv) (seen : list term) (glb : list fv) (fuel : int) () : Tac unit = let bs = vars_of_env (cur_env ()) in - first (fun (b:binding) -> trywith seen fuel (pack (Tv_Var b))) bs -and global (seen:list term) (fuel:int) () : Tac unit = - let cands = lookup_attr (`tcinstance) (cur_env ()) in - first (fun fv -> trywith seen fuel (pack (Tv_FVar fv))) cands -and trywith (seen:list term) (fuel:int) (t:term) : Tac unit = - debug ("Trying to apply hypothesis/instance: " ^ term_to_string t); - (fun () -> apply_noinst t) `seq` (fun () -> tcresolve' seen (fuel-1)) + first (fun (b:binding) -> + trywith head_fv seen glb fuel (pack (Tv_Var b)) b.sort) + bs + +and global (head_fv : fv) (seen : list term) (glb : list fv) (fuel : int) () : Tac unit = + first (fun fv -> + let typ = tc (cur_env()) (pack (Tv_FVar fv)) in // FIXME: a bit slow.. but at least it's a simple fvar + trywith head_fv seen glb fuel (pack (Tv_FVar fv)) typ) + glb + +and trywith (head_fv : fv) (seen:list term) (glb : list fv) (fuel:int) (t typ : term) : Tac unit = + match head_of (res_typ typ) with + | None -> raise NoInst + | Some fv' -> + if fv_eq fv' head_fv + then ( + debug (fun () -> "Trying to apply hypothesis/instance: " ^ term_to_string t); + (fun () -> apply_noinst t) `seq` (fun () -> tcresolve' seen glb (fuel-1)) + ) else + raise NoInst private let rec maybe_intros () : Tac unit = let g = cur_goal () in - match inspect_ln g with - | Reflection.V2.Tv_Arrow _ _ -> + match inspect g with + | Tv_Arrow _ _ -> ignore (intro ()); maybe_intros () | _ -> () [@@plugin] let tcresolve () : Tac unit = - //we sometimes get goal type as _ -> t - //so intro if that's the case - //not using intros () directly, since that unfolds aggressively if the term is not an arrow + // We sometimes get goal type as _ -> t + // So intro if that's the case + // Not using intros () directly, since that unfolds aggressively if the term is not an arrow + // TODO: Should we..? Why wouldn't the head always be an FV? maybe_intros (); - try tcresolve' [] 16 + + // Fetch a list of all instances in scope right now. + // TODO: turn this into a hash map per class, ideally one that can be + // stored. + let glb = lookup_attr (`tcinstance) (cur_env ()) in + try + tcresolve' [] glb 16 with - | TacticFailure s -> fail ("Typeclass resolution failed: " ^ s) + | NoInst -> + fail ("Could not solve constraint " ^ term_to_string (cur_goal ())) + | TacticFailure s -> + fail ("Typeclass resolution failed: " ^ s) | e -> raise e (**** Generating methods from a class ****)