From 2c90e2906a4ab8089a5bd559a9807a7db9d78db3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 22 Aug 2024 23:42:42 -0700 Subject: [PATCH] snap --- .../fstar-lib/generated/FStar_Parser_Const.ml | 2 - .../generated/FStar_Tactics_Typeclasses.ml | 2123 ----------------- 2 files changed, 2125 deletions(-) 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_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