diff --git a/ocaml/fstar-lib/generated/FStar_Class_Show.ml b/ocaml/fstar-lib/generated/FStar_Class_Show.ml index 7e9123402fd..ab58a053cdc 100644 --- a/ocaml/fstar-lib/generated/FStar_Class_Show.ml +++ b/ocaml/fstar-lib/generated/FStar_Class_Show.ml @@ -9,6 +9,24 @@ let printableshow : 'a . 'a FStar_Class_Printable.printable -> 'a showable = fun uu___ -> { show = (FStar_Class_Printable.to_string uu___) } let show_list : 'a . 'a showable -> 'a Prims.list showable = fun uu___ -> { show = ((FStar_Common.string_of_list ()) (show uu___)) } +let show_option : + 'a . 'a showable -> 'a FStar_Pervasives_Native.option showable = + fun uu___ -> { show = (FStar_Common.string_of_option (show uu___)) } +let show_either : + 'a 'b . + 'a showable -> 'b showable -> ('a, 'b) FStar_Pervasives.either showable + = + fun uu___ -> + fun uu___1 -> + { + show = + (fun uu___2 -> + match uu___2 with + | FStar_Pervasives.Inl x -> + let uu___3 = show uu___ x in Prims.op_Hat "Inl " uu___3 + | FStar_Pervasives.Inr y -> + let uu___3 = show uu___1 y in Prims.op_Hat "Inr " uu___3) + } let show_tuple2 : 'a 'b . 'a showable -> 'b showable -> ('a * 'b) showable = fun uu___ -> fun uu___1 -> diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml index 0b276b26f91..e533495b4ce 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings.ml @@ -63,8 +63,11 @@ let lazy_embed : FStar_Compiler_Effect.op_Bang FStar_Options.debug_embedding in if uu___1 then - let uu___2 = FStar_Syntax_Print.term_to_string ta in - let uu___3 = FStar_Syntax_Print.emb_typ_to_string et in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term ta in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Syntax.showable_emb_typ + et in let uu___4 = pa x in FStar_Compiler_Util.print3 "Embedding a %s\n\temb_typ=%s\n\tvalue is %s\n" uu___2 @@ -114,8 +117,12 @@ let lazy_unembed : FStar_Options.debug_embedding in if uu___4 then - let uu___5 = FStar_Syntax_Print.emb_typ_to_string et in - let uu___6 = FStar_Syntax_Print.emb_typ_to_string et' in + let uu___5 = + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_emb_typ et in + let uu___6 = + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_emb_typ et' in let uu___7 = match res with | FStar_Pervasives_Native.None -> "None" @@ -133,7 +140,9 @@ let lazy_unembed : FStar_Options.debug_embedding in if uu___5 then - let uu___6 = FStar_Syntax_Print.emb_typ_to_string et in + let uu___6 = + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_emb_typ et in let uu___7 = pa a1 in FStar_Compiler_Util.print2 "Unembed cancelled for %s\n\tvalue is %s\n" uu___6 @@ -147,7 +156,9 @@ let lazy_unembed : FStar_Options.debug_embedding in if uu___2 then - let uu___3 = FStar_Syntax_Print.emb_typ_to_string et in + let uu___3 = + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_emb_typ et in let uu___4 = FStar_Syntax_Print.term_to_string x1 in let uu___5 = match aopt with diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings_Base.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings_Base.ml index 84927bd3213..f02b9649916 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings_Base.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Embeddings_Base.ml @@ -61,11 +61,10 @@ let __proj__Mkembedding__item__emb_typ : match projectee with | { em; un; typ; print; emb_typ;_} -> emb_typ let emb_typ_of : 'a . 'a embedding -> FStar_Syntax_Syntax.emb_typ = fun e -> e.emb_typ -let unknown_printer : - 'uuuuu . FStar_Syntax_Syntax.term -> 'uuuuu -> Prims.string = +let unknown_printer : 'a . FStar_Syntax_Syntax.term -> 'a -> Prims.string = fun typ -> fun uu___ -> - let uu___1 = FStar_Syntax_Print.term_to_string typ in + let uu___1 = FStar_Class_Show.show FStar_Syntax_Print.showable_term typ in FStar_Compiler_Util.format1 "unknown %s" uu___1 let (term_as_fv : FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.fv) = fun t -> @@ -76,7 +75,8 @@ let (term_as_fv : FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.fv) = | FStar_Syntax_Syntax.Tm_fvar fv -> fv | uu___1 -> let uu___2 = - let uu___3 = FStar_Syntax_Print.term_to_string t in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t in FStar_Compiler_Util.format1 "Embeddings not defined for type %s" uu___3 in failwith uu___2 @@ -187,7 +187,7 @@ let unembed : FStar_Errors_Msg.text "Unembedding failed for type" in let uu___5 = let uu___6 = type_of e in - FStar_Syntax_Print.term_to_doc uu___6 in + FStar_Class_PP.pp FStar_Syntax_Print.pretty_term uu___6 in FStar_Pprint.op_Hat_Slash_Hat uu___4 uu___5 in let uu___4 = let uu___5 = @@ -195,13 +195,15 @@ let unembed : let uu___7 = let uu___8 = let uu___9 = emb_typ_of e in - FStar_Syntax_Print.emb_typ_to_string uu___9 in + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_emb_typ uu___9 in FStar_Pprint.doc_of_string uu___8 in FStar_Pprint.op_Hat_Slash_Hat uu___6 uu___7 in let uu___6 = let uu___7 = let uu___8 = FStar_Errors_Msg.text "Term =" in - let uu___9 = FStar_Syntax_Print.term_to_doc t in + let uu___9 = + FStar_Class_PP.pp FStar_Syntax_Print.pretty_term t in FStar_Pprint.op_Hat_Slash_Hat uu___8 uu___9 in [uu___7] in uu___5 :: uu___6 in @@ -303,8 +305,11 @@ let lazy_embed : FStar_Compiler_Effect.op_Bang FStar_Options.debug_embedding in if uu___1 then - let uu___2 = FStar_Syntax_Print.term_to_string ta in - let uu___3 = FStar_Syntax_Print.emb_typ_to_string et in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term ta in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Syntax.showable_emb_typ + et in let uu___4 = pa x in FStar_Compiler_Util.print3 "Embedding a %s\n\temb_typ=%s\n\tvalue is %s\n" uu___2 @@ -354,8 +359,12 @@ let lazy_unembed : FStar_Options.debug_embedding in if uu___4 then - let uu___5 = FStar_Syntax_Print.emb_typ_to_string et in - let uu___6 = FStar_Syntax_Print.emb_typ_to_string et' in + let uu___5 = + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_emb_typ et in + let uu___6 = + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_emb_typ et' in let uu___7 = match res with | FStar_Pervasives_Native.None -> "None" @@ -373,7 +382,9 @@ let lazy_unembed : FStar_Options.debug_embedding in if uu___5 then - let uu___6 = FStar_Syntax_Print.emb_typ_to_string et in + let uu___6 = + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_emb_typ et in let uu___7 = pa a1 in FStar_Compiler_Util.print2 "Unembed cancelled for %s\n\tvalue is %s\n" uu___6 @@ -387,8 +398,12 @@ let lazy_unembed : FStar_Options.debug_embedding in if uu___2 then - let uu___3 = FStar_Syntax_Print.emb_typ_to_string et in - let uu___4 = FStar_Syntax_Print.term_to_string x1 in + let uu___3 = + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_emb_typ et in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + x1 in let uu___5 = match aopt with | FStar_Pervasives_Native.None -> "None" diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml index 6ad6055fc83..f137c021750 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml @@ -1,18 +1,4 @@ open Prims -let rec (delta_depth_to_string : - FStar_Syntax_Syntax.delta_depth -> Prims.string) = - fun uu___ -> - match uu___ with - | FStar_Syntax_Syntax.Delta_constant_at_level i -> - let uu___1 = FStar_Compiler_Util.string_of_int i in - Prims.op_Hat "Delta_constant_at_level " uu___1 - | FStar_Syntax_Syntax.Delta_equational_at_level i -> - let uu___1 = FStar_Compiler_Util.string_of_int i in - Prims.op_Hat "Delta_equational_at_level " uu___1 - | FStar_Syntax_Syntax.Delta_abstract d -> - let uu___1 = - let uu___2 = delta_depth_to_string d in Prims.op_Hat uu___2 ")" in - Prims.op_Hat "Delta_abstract (" uu___1 let (sli : FStar_Ident.lident -> Prims.string) = fun l -> let uu___ = FStar_Options.print_real_names () in @@ -264,30 +250,6 @@ let (quals_to_string' : | uu___ -> let uu___1 = quals_to_string quals in Prims.op_Hat uu___1 " " let (paren : Prims.string -> Prims.string) = fun s -> Prims.op_Hat "(" (Prims.op_Hat s ")") -let rec (emb_typ_to_string : FStar_Syntax_Syntax.emb_typ -> Prims.string) = - fun uu___ -> - match uu___ with - | FStar_Syntax_Syntax.ET_abstract -> "abstract" - | FStar_Syntax_Syntax.ET_app (h, []) -> h - | FStar_Syntax_Syntax.ET_app (h, args) -> - let uu___1 = - let uu___2 = - let uu___3 = - let uu___4 = - let uu___5 = FStar_Compiler_List.map emb_typ_to_string args in - FStar_Compiler_Effect.op_Bar_Greater uu___5 - (FStar_Compiler_String.concat " ") in - Prims.op_Hat uu___4 ")" in - Prims.op_Hat " " uu___3 in - Prims.op_Hat h uu___2 in - Prims.op_Hat "(" uu___1 - | FStar_Syntax_Syntax.ET_fun (a, b) -> - let uu___1 = - let uu___2 = emb_typ_to_string a in - let uu___3 = - let uu___4 = emb_typ_to_string b in Prims.op_Hat ") -> " uu___4 in - Prims.op_Hat uu___2 uu___3 in - Prims.op_Hat "(" uu___1 let (lkind_to_string : FStar_Syntax_Syntax.lazy_kind -> Prims.string) = fun uu___ -> match uu___ with @@ -306,7 +268,9 @@ let (lkind_to_string : FStar_Syntax_Syntax.lazy_kind -> Prims.string) = | FStar_Syntax_Syntax.Lazy_letbinding -> "Lazy_letbinding" | FStar_Syntax_Syntax.Lazy_embedding (e, uu___1) -> let uu___2 = - let uu___3 = emb_typ_to_string e in Prims.op_Hat uu___3 ")" in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Syntax.showable_emb_typ e in + Prims.op_Hat uu___3 ")" in Prims.op_Hat "Lazy_embedding(" uu___2 | FStar_Syntax_Syntax.Lazy_universe -> "Lazy_universe" | FStar_Syntax_Syntax.Lazy_universe_uvar -> "Lazy_universe_uvar" @@ -1991,6 +1955,17 @@ let (term_to_doc' : then let uu___1 = term_to_string t in FStar_Pprint.arbitrary_string uu___1 else FStar_Syntax_Print_Pretty.term_to_doc' dsenv t +let (univ_to_doc' : + FStar_Syntax_DsEnv.env -> + FStar_Syntax_Syntax.universe -> FStar_Pprint.document) + = + fun dsenv -> + fun t -> + let uu___ = FStar_Options.ugly () in + if uu___ + then + let uu___1 = univ_to_string t in FStar_Pprint.arbitrary_string uu___1 + else FStar_Syntax_Print_Pretty.univ_to_doc' dsenv t let (comp_to_doc' : FStar_Syntax_DsEnv.env -> FStar_Syntax_Syntax.comp -> FStar_Pprint.document) = @@ -2020,6 +1995,13 @@ let (term_to_doc : FStar_Syntax_Syntax.term -> FStar_Pprint.document) = then let uu___1 = term_to_string t in FStar_Pprint.arbitrary_string uu___1 else FStar_Syntax_Print_Pretty.term_to_doc t +let (univ_to_doc : FStar_Syntax_Syntax.universe -> FStar_Pprint.document) = + fun t -> + let uu___ = FStar_Options.ugly () in + if uu___ + then + let uu___1 = univ_to_string t in FStar_Pprint.arbitrary_string uu___1 + else FStar_Syntax_Print_Pretty.univ_to_doc t let (comp_to_doc : FStar_Syntax_Syntax.comp -> FStar_Pprint.document) = fun t -> let uu___ = FStar_Options.ugly () in @@ -2034,16 +2016,22 @@ let (sigelt_to_doc : FStar_Syntax_Syntax.sigelt -> FStar_Pprint.document) = then let uu___1 = sigelt_to_string t in FStar_Pprint.arbitrary_string uu___1 else FStar_Syntax_Print_Pretty.sigelt_to_doc t +let (pretty_term : FStar_Syntax_Syntax.term FStar_Class_PP.pretty) = + { FStar_Class_PP.pp = term_to_doc } +let (pretty_univ : FStar_Syntax_Syntax.universe FStar_Class_PP.pretty) = + { FStar_Class_PP.pp = univ_to_doc } let (pretty_sigelt : FStar_Syntax_Syntax.sigelt FStar_Class_PP.pretty) = { FStar_Class_PP.pp = sigelt_to_doc } let (pretty_comp : FStar_Syntax_Syntax.comp FStar_Class_PP.pretty) = { FStar_Class_PP.pp = comp_to_doc } -let (pretty_term : FStar_Syntax_Syntax.term FStar_Class_PP.pretty) = - { FStar_Class_PP.pp = term_to_doc } -let (showable_sigelt : FStar_Syntax_Syntax.sigelt FStar_Class_Show.showable) - = { FStar_Class_Show.show = sigelt_to_string } let (showable_term : FStar_Syntax_Syntax.term FStar_Class_Show.showable) = { FStar_Class_Show.show = term_to_string } +let (showable_univ : FStar_Syntax_Syntax.universe FStar_Class_Show.showable) + = { FStar_Class_Show.show = univ_to_string } +let (showable_comp : FStar_Syntax_Syntax.comp FStar_Class_Show.showable) = + { FStar_Class_Show.show = comp_to_string } +let (showable_sigelt : FStar_Syntax_Syntax.sigelt FStar_Class_Show.showable) + = { FStar_Class_Show.show = sigelt_to_string } let (showable_bv : FStar_Syntax_Syntax.bv FStar_Class_Show.showable) = { FStar_Class_Show.show = bv_to_string } let (showable_binder : FStar_Syntax_Syntax.binder FStar_Class_Show.showable) diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Print_Pretty.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Print_Pretty.ml index 459193a4dfd..dfce21d4754 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Print_Pretty.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Print_Pretty.ml @@ -13,12 +13,30 @@ let (term_to_doc' : (fun uu___ -> let e = FStar_Syntax_Resugar.resugar_term' env tm in FStar_Parser_ToDocument.term_to_document e) +let (univ_to_doc' : + FStar_Syntax_DsEnv.env -> + FStar_Syntax_Syntax.universe -> FStar_Pprint.document) + = + fun env -> + fun u -> + FStar_GenSym.with_frozen_gensym + (fun uu___ -> + let e = + FStar_Syntax_Resugar.resugar_universe' env u + FStar_Compiler_Range_Type.dummyRange in + FStar_Parser_ToDocument.term_to_document e) let (term_to_string' : FStar_Syntax_DsEnv.env -> FStar_Syntax_Syntax.term -> Prims.string) = fun env -> fun tm -> FStar_GenSym.with_frozen_gensym (fun uu___ -> let d = term_to_doc' env tm in pp d) +let (univ_to_string' : + FStar_Syntax_DsEnv.env -> FStar_Syntax_Syntax.universe -> Prims.string) = + fun env -> + fun u -> + FStar_GenSym.with_frozen_gensym + (fun uu___ -> let d = univ_to_doc' env u in pp d) let (comp_to_doc' : FStar_Syntax_DsEnv.env -> FStar_Syntax_Syntax.comp -> FStar_Pprint.document) = @@ -59,6 +77,14 @@ let (term_to_doc : FStar_Syntax_Syntax.term -> FStar_Pprint.document) = (fun uu___ -> let e = FStar_Syntax_Resugar.resugar_term tm in FStar_Parser_ToDocument.term_to_document e) +let (univ_to_doc : FStar_Syntax_Syntax.universe -> FStar_Pprint.document) = + fun u -> + FStar_GenSym.with_frozen_gensym + (fun uu___ -> + let e = + FStar_Syntax_Resugar.resugar_universe u + FStar_Compiler_Range_Type.dummyRange in + FStar_Parser_ToDocument.term_to_document e) let (comp_to_doc : FStar_Syntax_Syntax.comp -> FStar_Pprint.document) = fun c -> FStar_GenSym.with_frozen_gensym diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml index c6767ae0ebe..cda459007d9 100644 --- a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml +++ b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml @@ -65,6 +65,32 @@ let (uu___is_ET_app : emb_typ -> Prims.bool) = let (__proj__ET_app__item___0 : emb_typ -> (Prims.string * emb_typ Prims.list)) = fun projectee -> match projectee with | ET_app _0 -> _0 +let rec (emb_typ_to_string : emb_typ -> Prims.string) = + fun uu___ -> + match uu___ with + | ET_abstract -> "abstract" + | ET_app (h, []) -> h + | ET_app (h, args) -> + let uu___1 = + let uu___2 = + let uu___3 = + let uu___4 = + let uu___5 = FStar_Compiler_List.map emb_typ_to_string args in + FStar_Compiler_Effect.op_Bar_Greater uu___5 + (FStar_Compiler_String.concat " ") in + Prims.op_Hat uu___4 ")" in + Prims.op_Hat " " uu___3 in + Prims.op_Hat h uu___2 in + Prims.op_Hat "(" uu___1 + | ET_fun (a, b) -> + let uu___1 = + let uu___2 = emb_typ_to_string a in + let uu___3 = + let uu___4 = emb_typ_to_string b in Prims.op_Hat ") -> " uu___4 in + Prims.op_Hat uu___2 uu___3 in + Prims.op_Hat "(" uu___1 +let (showable_emb_typ : emb_typ FStar_Class_Show.showable) = + { FStar_Class_Show.show = emb_typ_to_string } type version = { major: Prims.int ; minor: Prims.int }[@@deriving yojson,show] @@ -159,6 +185,21 @@ let (uu___is_Delta_abstract : delta_depth -> Prims.bool) = match projectee with | Delta_abstract _0 -> true | uu___ -> false let (__proj__Delta_abstract__item___0 : delta_depth -> delta_depth) = fun projectee -> match projectee with | Delta_abstract _0 -> _0 +let rec (delta_depth_to_string : delta_depth -> Prims.string) = + fun uu___ -> + match uu___ with + | Delta_constant_at_level i -> + let uu___1 = FStar_Compiler_Util.string_of_int i in + Prims.op_Hat "Delta_constant_at_level " uu___1 + | Delta_equational_at_level i -> + let uu___1 = FStar_Compiler_Util.string_of_int i in + Prims.op_Hat "Delta_equational_at_level " uu___1 + | Delta_abstract d -> + let uu___1 = + let uu___2 = delta_depth_to_string d in Prims.op_Hat uu___2 ")" in + Prims.op_Hat "Delta_abstract (" uu___1 +let (showable_delta_depth : delta_depth FStar_Class_Show.showable) = + { FStar_Class_Show.show = delta_depth_to_string } type should_check_uvar = | Allow_unresolved of Prims.string | Allow_untyped of Prims.string diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml index 212ba734620..1b89d6e13f1 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml @@ -404,7 +404,8 @@ let (steps_to_string : fsteps -> Prims.string) = let uu___17 = FStar_Compiler_Effect.op_Bar_Greater f.unfold_until (format_opt - FStar_Syntax_Print.delta_depth_to_string) in + (FStar_Class_Show.show + FStar_Syntax_Syntax.showable_delta_depth)) in let uu___18 = let uu___19 = FStar_Compiler_Effect.op_Bar_Greater f.unfold_only diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml index de9c067e7f5..2dbde2cddf0 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml @@ -3722,11 +3722,13 @@ let (delta_depth_of_fv : then let uu___8 = FStar_Syntax_Print.fv_to_string fv in let uu___9 = - FStar_Syntax_Print.delta_depth_to_string + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_delta_depth (FStar_Pervasives_Native.__proj__Some__item__v fv.FStar_Syntax_Syntax.fv_delta) in let uu___10 = - FStar_Syntax_Print.delta_depth_to_string d in + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_delta_depth d in FStar_Compiler_Util.print3 "WARNING WARNING WARNING fv=%s, delta_depth=%s, env.delta_depth=%s\n" uu___8 uu___9 uu___10 @@ -6281,7 +6283,8 @@ let (string_of_delta_level : delta_level -> Prims.string) = | InliningDelta -> "Inlining" | Eager_unfolding_only -> "Eager_unfolding_only" | Unfold d -> - let uu___1 = FStar_Syntax_Print.delta_depth_to_string d in + let uu___1 = + FStar_Class_Show.show FStar_Syntax_Syntax.showable_delta_depth d in Prims.op_Hat "Unfold " uu___1 let (lidents : env -> FStar_Ident.lident Prims.list) = fun env1 -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml index d096750fd2b..ddfda0d6f7b 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_NBETerm.ml @@ -662,7 +662,8 @@ let rec (t_to_string : t -> Prims.string) = FStar_Syntax_Print.term_to_string uu___2 in FStar_Compiler_Util.format1 "Lazy (Inl {%s})" uu___1 | Lazy (FStar_Pervasives.Inr (uu___, et), uu___1) -> - let uu___2 = FStar_Syntax_Print.emb_typ_to_string et in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Syntax.showable_emb_typ et in FStar_Compiler_Util.format1 "Lazy (Inr (?, %s))" uu___2 | LocalLetRec (uu___, l, uu___1, uu___2, uu___3, uu___4, uu___5) -> let uu___6 = @@ -809,7 +810,8 @@ let lazy_embed : 'a . FStar_Syntax_Syntax.emb_typ -> 'a -> (unit -> t) -> t = FStar_Compiler_Effect.op_Bang FStar_Options.debug_embedding in if uu___1 then - let uu___2 = FStar_Syntax_Print.emb_typ_to_string et in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Syntax.showable_emb_typ et in FStar_Compiler_Util.print1 "Embedding\n\temb_typ=%s\n" uu___2 else ()); (let uu___1 = @@ -845,8 +847,12 @@ let lazy_unembed : FStar_Compiler_Effect.op_Bang FStar_Options.debug_embedding in if uu___2 then - let uu___3 = FStar_Syntax_Print.emb_typ_to_string et in - let uu___4 = FStar_Syntax_Print.emb_typ_to_string et' in + let uu___3 = + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_emb_typ et in + let uu___4 = + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_emb_typ et' in FStar_Compiler_Util.print2 "Unembed cancellation failed\n\t%s <> %s\n" uu___3 uu___4 else ()); @@ -857,7 +863,9 @@ let lazy_unembed : FStar_Compiler_Effect.op_Bang FStar_Options.debug_embedding in if uu___3 then - let uu___4 = FStar_Syntax_Print.emb_typ_to_string et in + let uu___4 = + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_emb_typ et in FStar_Compiler_Util.print1 "Unembed cancelled for %s\n" uu___4 else ()); @@ -868,7 +876,9 @@ let lazy_unembed : FStar_Compiler_Effect.op_Bang FStar_Options.debug_embedding in if uu___2 then - let uu___3 = FStar_Syntax_Print.emb_typ_to_string et in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Syntax.showable_emb_typ + et in FStar_Compiler_Util.print1 "Unembedding:\n\temb_typ=%s\n" uu___3 else ()); diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml index d05e854461e..182daa770a9 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml @@ -2036,7 +2036,8 @@ let (should_unfold : let uu___5 = FStar_TypeChecker_Env.delta_depth_of_fv cfg.FStar_TypeChecker_Cfg.tcenv fv in - FStar_Syntax_Print.delta_depth_to_string uu___5 in + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_delta_depth uu___5 in let uu___5 = (FStar_Common.string_of_list ()) FStar_TypeChecker_Env.string_of_delta_level @@ -9008,56 +9009,62 @@ let (term_to_string : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.term -> Prims.string) = fun env1 -> fun t -> - let t1 = - try - (fun uu___ -> - match () with - | () -> - normalize [FStar_TypeChecker_Env.AllowUnboundUniverses] env1 - t) () - with - | uu___ -> - ((let uu___2 = - let uu___3 = - let uu___4 = FStar_Compiler_Util.message_of_exn uu___ in - FStar_Compiler_Util.format1 - "Normalization failed with error %s\n" uu___4 in - (FStar_Errors_Codes.Warning_NormalizationFailure, uu___3) in - FStar_Errors.log_issue t.FStar_Syntax_Syntax.pos uu___2); - t) in - let uu___ = - FStar_Syntax_DsEnv.set_current_module - env1.FStar_TypeChecker_Env.dsenv - env1.FStar_TypeChecker_Env.curmodule in - FStar_Syntax_Print.term_to_string' uu___ t1 + FStar_GenSym.with_frozen_gensym + (fun uu___ -> + let t1 = + try + (fun uu___1 -> + match () with + | () -> + normalize [FStar_TypeChecker_Env.AllowUnboundUniverses] + env1 t) () + with + | uu___1 -> + ((let uu___3 = + let uu___4 = + let uu___5 = FStar_Compiler_Util.message_of_exn uu___1 in + FStar_Compiler_Util.format1 + "Normalization failed with error %s\n" uu___5 in + (FStar_Errors_Codes.Warning_NormalizationFailure, + uu___4) in + FStar_Errors.log_issue t.FStar_Syntax_Syntax.pos uu___3); + t) in + let uu___1 = + FStar_Syntax_DsEnv.set_current_module + env1.FStar_TypeChecker_Env.dsenv + env1.FStar_TypeChecker_Env.curmodule in + FStar_Syntax_Print.term_to_string' uu___1 t1) let (comp_to_string : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.comp -> Prims.string) = fun env1 -> fun c -> - let c1 = - try - (fun uu___ -> - match () with - | () -> - let uu___1 = - FStar_TypeChecker_Cfg.config - [FStar_TypeChecker_Env.AllowUnboundUniverses] env1 in - norm_comp uu___1 [] c) () - with - | uu___ -> - ((let uu___2 = - let uu___3 = - let uu___4 = FStar_Compiler_Util.message_of_exn uu___ in - FStar_Compiler_Util.format1 - "Normalization failed with error %s\n" uu___4 in - (FStar_Errors_Codes.Warning_NormalizationFailure, uu___3) in - FStar_Errors.log_issue c.FStar_Syntax_Syntax.pos uu___2); - c) in - let uu___ = - FStar_Syntax_DsEnv.set_current_module - env1.FStar_TypeChecker_Env.dsenv - env1.FStar_TypeChecker_Env.curmodule in - FStar_Syntax_Print.comp_to_string' uu___ c1 + FStar_GenSym.with_frozen_gensym + (fun uu___ -> + let c1 = + try + (fun uu___1 -> + match () with + | () -> + let uu___2 = + FStar_TypeChecker_Cfg.config + [FStar_TypeChecker_Env.AllowUnboundUniverses] env1 in + norm_comp uu___2 [] c) () + with + | uu___1 -> + ((let uu___3 = + let uu___4 = + let uu___5 = FStar_Compiler_Util.message_of_exn uu___1 in + FStar_Compiler_Util.format1 + "Normalization failed with error %s\n" uu___5 in + (FStar_Errors_Codes.Warning_NormalizationFailure, + uu___4) in + FStar_Errors.log_issue c.FStar_Syntax_Syntax.pos uu___3); + c) in + let uu___1 = + FStar_Syntax_DsEnv.set_current_module + env1.FStar_TypeChecker_Env.dsenv + env1.FStar_TypeChecker_Env.curmodule in + FStar_Syntax_Print.comp_to_string' uu___1 c1) let (normalize_refinement : FStar_TypeChecker_Env.steps -> FStar_TypeChecker_Env.env -> diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml index 0acd6c0ece6..e25560db064 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Rel.ml @@ -879,7 +879,7 @@ let (term_to_string : FStar_Syntax_Syntax.term -> Prims.string) = FStar_Compiler_Util.format1 "@<%s>" uu___3 in let uu___3 = FStar_Syntax_Print.args_to_string args in FStar_Compiler_Util.format3 "%s%s %s" uu___1 uu___2 uu___3 - | uu___1 -> FStar_Syntax_Print.term_to_string t) + | uu___1 -> FStar_Class_Show.show FStar_Syntax_Print.showable_term t) let (prob_to_string : FStar_TypeChecker_Env.env -> FStar_TypeChecker_Common.prob -> Prims.string) = @@ -928,7 +928,8 @@ let (uvi_to_string : FStar_TypeChecker_Env.env -> uvi -> Prims.string) = (let uu___3 = FStar_Syntax_Unionfind.univ_uvar_id u in FStar_Compiler_Effect.op_Bar_Greater uu___3 FStar_Compiler_Util.string_of_int) in - let uu___1 = FStar_Syntax_Print.univ_to_string t in + let uu___1 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ t in FStar_Compiler_Util.format2 "UNIV %s <- %s" x uu___1 | TERM (u, t) -> let x = @@ -956,15 +957,15 @@ let (names_to_string : (FStar_Compiler_List.map FStar_Syntax_Print.bv_to_string) in FStar_Compiler_Effect.op_Bar_Greater uu___ (FStar_Compiler_String.concat ", ") -let args_to_string : - 'uuuuu . (FStar_Syntax_Syntax.term * 'uuuuu) Prims.list -> Prims.string = +let (args_to_string : FStar_Syntax_Syntax.args -> Prims.string) = fun args -> let uu___ = FStar_Compiler_Effect.op_Bar_Greater args (FStar_Compiler_List.map (fun uu___1 -> match uu___1 with - | (x, uu___2) -> FStar_Syntax_Print.term_to_string x)) in + | (x, uu___2) -> + FStar_Class_Show.show FStar_Syntax_Print.showable_term x)) in FStar_Compiler_Effect.op_Bar_Greater uu___ (FStar_Compiler_String.concat " ") let (empty_worklist : FStar_TypeChecker_Env.env -> worklist) = @@ -1750,7 +1751,9 @@ let (base_and_refinement_maybe_delta : (FStar_Pervasives_Native.Some (x1, phi1))) | tt -> let uu___2 = - let uu___3 = FStar_Syntax_Print.term_to_string tt in + let uu___3 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term tt in let uu___4 = FStar_Syntax_Print.tag_of_term tt in FStar_Compiler_Util.format2 "impossible: Got %s ... %s\n" uu___3 uu___4 in @@ -1812,28 +1815,32 @@ let (base_and_refinement_maybe_delta : (t12, FStar_Pervasives_Native.None) | FStar_Syntax_Syntax.Tm_meta uu___ -> let uu___1 = - let uu___2 = FStar_Syntax_Print.term_to_string t12 in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t12 in let uu___3 = FStar_Syntax_Print.tag_of_term t12 in FStar_Compiler_Util.format2 "impossible (outer): Got %s ... %s\n" uu___2 uu___3 in failwith uu___1 | FStar_Syntax_Syntax.Tm_ascribed uu___ -> let uu___1 = - let uu___2 = FStar_Syntax_Print.term_to_string t12 in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t12 in let uu___3 = FStar_Syntax_Print.tag_of_term t12 in FStar_Compiler_Util.format2 "impossible (outer): Got %s ... %s\n" uu___2 uu___3 in failwith uu___1 | FStar_Syntax_Syntax.Tm_delayed uu___ -> let uu___1 = - let uu___2 = FStar_Syntax_Print.term_to_string t12 in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t12 in let uu___3 = FStar_Syntax_Print.tag_of_term t12 in FStar_Compiler_Util.format2 "impossible (outer): Got %s ... %s\n" uu___2 uu___3 in failwith uu___1 | FStar_Syntax_Syntax.Tm_unknown -> let uu___ = - let uu___1 = FStar_Syntax_Print.term_to_string t12 in + let uu___1 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t12 in let uu___2 = FStar_Syntax_Print.tag_of_term t12 in FStar_Compiler_Util.format2 "impossible (outer): Got %s ... %s\n" uu___1 uu___2 in @@ -2042,7 +2049,8 @@ let (ensure_no_uvar_subst : FStar_Syntax_Print.ctx_uvar_to_string uv in let uu___8 = - FStar_Syntax_Print.term_to_string sol in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term sol in FStar_Compiler_Util.print2 "ensure_no_uvar_subst solving %s with %s\n" uu___7 uu___8 @@ -2214,7 +2222,9 @@ let (solve_prob' : then let uu___3 = FStar_Compiler_Util.string_of_int (p_pid prob) in let uu___4 = print_ctx_uvar uv in - let uu___5 = FStar_Syntax_Print.term_to_string phi1 in + let uu___5 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + phi1 in FStar_Compiler_Util.print3 "Solving %s (%s) with formula %s\n" uu___3 uu___4 uu___5 else ()); @@ -2243,7 +2253,8 @@ let (solve_prob' : let uu___2 = let uu___3 = FStar_Syntax_Print.ctx_uvar_to_string uv in let uu___4 = - FStar_Syntax_Print.term_to_string (p_guard prob) in + FStar_Class_Show.show FStar_Syntax_Print.showable_term + (p_guard prob) in FStar_Compiler_Util.format2 "Impossible: this instance %s has already been assigned a solution\n%s\n" uu___3 uu___4 in @@ -2391,7 +2402,8 @@ let (occurs_check : let uu___3 = FStar_Syntax_Print.uvar_to_string uk.FStar_Syntax_Syntax.ctx_uvar_head in - let uu___4 = FStar_Syntax_Print.term_to_string t in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t in FStar_Compiler_Util.format2 "occurs-check failed (%s occurs in %s)" uu___3 uu___4 in FStar_Pervasives_Native.Some uu___2) in @@ -2744,18 +2756,13 @@ let (string_of_match_result : match_result -> Prims.string) = match uu___ with | MisMatch (d1, d2) -> let uu___1 = - let uu___2 = - FStar_Common.string_of_option - FStar_Syntax_Print.delta_depth_to_string d1 in - let uu___3 = - let uu___4 = - let uu___5 = - FStar_Common.string_of_option - FStar_Syntax_Print.delta_depth_to_string d2 in - Prims.op_Hat uu___5 ")" in - Prims.op_Hat ") (" uu___4 in - Prims.op_Hat uu___2 uu___3 in - Prims.op_Hat "MisMatch (" uu___1 + FStar_Class_Show.show + (FStar_Class_Show.show_tuple2 + (FStar_Class_Show.show_option + FStar_Syntax_Syntax.showable_delta_depth) + (FStar_Class_Show.show_option + FStar_Syntax_Syntax.showable_delta_depth)) (d1, d2) in + Prims.op_Hat "MisMatch " uu___1 | HeadMatch u -> let uu___1 = FStar_Compiler_Util.string_of_bool u in Prims.op_Hat "HeadMatch " uu___1 @@ -2871,8 +2878,10 @@ let rec (head_matches : (FStar_Options.Other "RelDelta") in if uu___1 then - ((let uu___3 = FStar_Syntax_Print.term_to_string t11 in - let uu___4 = FStar_Syntax_Print.term_to_string t21 in + ((let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t11 in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t21 in FStar_Compiler_Util.print2 "head_matches %s %s\n" uu___3 uu___4); (let uu___4 = FStar_Syntax_Print.tag_of_term t11 in let uu___5 = FStar_Syntax_Print.tag_of_term t21 in @@ -3039,8 +3048,10 @@ let (head_matches_delta : (FStar_Options.Other "RelDelta") in if uu___1 then - let uu___2 = FStar_Syntax_Print.term_to_string t in - let uu___3 = FStar_Syntax_Print.term_to_string head in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term head in FStar_Compiler_Util.print2 "Head of %s is %s\n" uu___2 uu___3 else ()); (let uu___1 = @@ -3062,7 +3073,9 @@ let (head_matches_delta : (FStar_Options.Other "RelDelta") in if uu___4 then - let uu___5 = FStar_Syntax_Print.term_to_string head in + let uu___5 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head in FStar_Compiler_Util.print1 "No definition found for %s\n" uu___5 else ()); @@ -3100,8 +3113,12 @@ let (head_matches_delta : (FStar_Options.Other "RelDelta") in if uu___7 then - let uu___8 = FStar_Syntax_Print.term_to_string t in - let uu___9 = FStar_Syntax_Print.term_to_string t' in + let uu___8 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t in + let uu___9 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t' in FStar_Compiler_Util.print2 "Inlined %s to %s\n" uu___8 uu___9 else ()); @@ -3142,8 +3159,10 @@ let (head_matches_delta : (FStar_Options.Other "RelDelta") in if uu___1 then - let uu___2 = FStar_Syntax_Print.term_to_string t11 in - let uu___3 = FStar_Syntax_Print.term_to_string t21 in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t11 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t21 in let uu___4 = string_of_match_result r in FStar_Compiler_Util.print3 "head_matches (%s, %s) = %s\n" uu___2 uu___3 uu___4 @@ -3272,8 +3291,10 @@ let (head_matches_delta : (FStar_Options.Other "RelDelta") in if uu___1 then - let uu___2 = FStar_Syntax_Print.term_to_string t1 in - let uu___3 = FStar_Syntax_Print.term_to_string t2 in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t1 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t2 in let uu___4 = string_of_match_result (FStar_Pervasives_Native.fst r) in let uu___5 = @@ -3289,10 +3310,13 @@ let (head_matches_delta : (fun uu___8 -> match uu___8 with | (t11, t21) -> - let uu___9 = FStar_Syntax_Print.term_to_string t11 in + let uu___9 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t11 in let uu___10 = let uu___11 = - FStar_Syntax_Print.term_to_string t21 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t21 in Prims.op_Hat "; " uu___11 in Prims.op_Hat uu___9 uu___10)) in FStar_Compiler_Util.print4 @@ -3756,9 +3780,11 @@ let rec (really_solve_universe_eq : ufailed_thunk (fun uu___3 -> let uu___4 = - FStar_Syntax_Print.univ_to_string u12 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_univ u12 in let uu___5 = - FStar_Syntax_Print.univ_to_string u22 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_univ u22 in FStar_Compiler_Util.format2 "Unable to unify universes: %s and %s" uu___4 uu___5)) @@ -3787,40 +3813,52 @@ let rec (really_solve_universe_eq : | uu___1 -> ufailed_thunk (fun uu___2 -> - let uu___3 = FStar_Syntax_Print.univ_to_string u12 in - let uu___4 = FStar_Syntax_Print.univ_to_string u22 in + let uu___3 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_univ u12 in + let uu___4 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_univ u22 in FStar_Compiler_Util.format3 "Unable to unify universes: %s and %s (%s)" uu___3 uu___4 msg)) in match (u11, u21) with | (FStar_Syntax_Syntax.U_bvar uu___, uu___1) -> let uu___2 = - let uu___3 = FStar_Syntax_Print.univ_to_string u11 in - let uu___4 = FStar_Syntax_Print.univ_to_string u21 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ u11 in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ u21 in FStar_Compiler_Util.format2 "Impossible: found an de Bruijn universe variable or unknown universe: %s, %s" uu___3 uu___4 in failwith uu___2 | (FStar_Syntax_Syntax.U_unknown, uu___) -> let uu___1 = - let uu___2 = FStar_Syntax_Print.univ_to_string u11 in - let uu___3 = FStar_Syntax_Print.univ_to_string u21 in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ u11 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ u21 in FStar_Compiler_Util.format2 "Impossible: found an de Bruijn universe variable or unknown universe: %s, %s" uu___2 uu___3 in failwith uu___1 | (uu___, FStar_Syntax_Syntax.U_bvar uu___1) -> let uu___2 = - let uu___3 = FStar_Syntax_Print.univ_to_string u11 in - let uu___4 = FStar_Syntax_Print.univ_to_string u21 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ u11 in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ u21 in FStar_Compiler_Util.format2 "Impossible: found an de Bruijn universe variable or unknown universe: %s, %s" uu___3 uu___4 in failwith uu___2 | (uu___, FStar_Syntax_Syntax.U_unknown) -> let uu___1 = - let uu___2 = FStar_Syntax_Print.univ_to_string u11 in - let uu___3 = FStar_Syntax_Print.univ_to_string u21 in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ u11 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ u21 in FStar_Compiler_Util.format2 "Impossible: found an de Bruijn universe variable or unknown universe: %s, %s" uu___2 uu___3 in @@ -3851,9 +3889,10 @@ let rec (really_solve_universe_eq : then let uu___1 = let uu___2 = - FStar_Syntax_Print.univ_to_string + FStar_Class_Show.show FStar_Syntax_Print.showable_univ (FStar_Syntax_Syntax.U_unif v1) in - let uu___3 = FStar_Syntax_Print.univ_to_string u3 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ u3 in FStar_Compiler_Util.format2 "Failed occurs check: %s occurs in %s" uu___2 uu___3 in try_umax_components u11 u21 uu___1 @@ -3868,9 +3907,10 @@ let rec (really_solve_universe_eq : then let uu___1 = let uu___2 = - FStar_Syntax_Print.univ_to_string + FStar_Class_Show.show FStar_Syntax_Print.showable_univ (FStar_Syntax_Syntax.U_unif v1) in - let uu___3 = FStar_Syntax_Print.univ_to_string u3 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ u3 in FStar_Compiler_Util.format2 "Failed occurs check: %s occurs in %s" uu___2 uu___3 in try_umax_components u11 u21 uu___1 @@ -4168,7 +4208,8 @@ let (simplify_guard : (FStar_Options.Other "Simplification") in if uu___1 then - let uu___2 = FStar_Syntax_Print.term_to_string f in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term f in FStar_Compiler_Util.print1 "Simplifying guard %s\n" uu___2 else ()); (let f1 = @@ -4186,7 +4227,8 @@ let (simplify_guard : (FStar_Options.Other "Simplification") in if uu___2 then - let uu___3 = FStar_Syntax_Print.term_to_string f1 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term f1 in FStar_Compiler_Util.print1 "Simplified guard to %s\n" uu___3 else ()); (let f2 = @@ -4679,10 +4721,12 @@ let (apply_ad_hoc_indexed_subcomp : if uu___6 then let uu___7 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term f_sort_i in let uu___8 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term c1_i in FStar_Compiler_Util.print3 "Layered Effects (%s) %s = %s\n" @@ -4739,10 +4783,12 @@ let (apply_ad_hoc_indexed_subcomp : if uu___7 then let uu___8 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term g_sort_i in let uu___9 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term c2_i in FStar_Compiler_Util.print3 "Layered Effects (%s) %s = %s\n" @@ -5164,8 +5210,10 @@ and (solve_rigid_flex_or_flex_rigid_subtyping : (FStar_Options.Other "Rel") in if uu___2 then - let uu___3 = FStar_Syntax_Print.term_to_string t1 in - let uu___4 = FStar_Syntax_Print.term_to_string t2 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t1 in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t2 in FStar_Compiler_Util.print2 "[meet/join]: pairwise: %s and %s\n" uu___3 uu___4 else ()); @@ -5432,7 +5480,8 @@ and (solve_rigid_flex_or_flex_rigid_subtyping : if uu___6 then let uu___7 = - FStar_Syntax_Print.term_to_string t12 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t12 in FStar_Compiler_Util.print1 "pairwise fallback2 succeeded: %s" uu___7 @@ -6367,7 +6416,8 @@ and (solve_binders : if uu___6 then let uu___7 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term phi1 in let uu___8 = FStar_Syntax_Print.bv_to_string @@ -6927,7 +6977,9 @@ and (solve_t_flex_rigid_eq : if uu___4 then let uu___5 = flex_t_to_string lhs1 in - let uu___6 = FStar_Syntax_Print.term_to_string rhs1 in + let uu___6 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + rhs1 in FStar_Compiler_Util.print2 "try_first_order\n\tlhs=%s\n\trhs=%s\n" uu___5 uu___6 else ()); @@ -7260,10 +7312,12 @@ and (solve_t_flex_rigid_eq : let uu___20 = FStar_Syntax_Util.ctx_uvar_typ ctx_uv in - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term uu___20 in let uu___20 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t_head in FStar_Compiler_Util.print2 "first-order: head type mismatch:\n\tlhs=%s\n\trhs=%s\n" @@ -7461,7 +7515,8 @@ and (solve_t_flex_flex : if uu___1 then let uu___2 = FStar_Syntax_Print.ctx_uvar_to_string uv in - let uu___3 = FStar_Syntax_Print.term_to_string t in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t in FStar_Compiler_Util.print2 "solve_t_flex_flex: solving meta arg uvar %s with %s\n" uu___2 uu___3 @@ -7838,9 +7893,11 @@ and (solve_t' : tprob -> worklist -> solution) = (FStar_Options.Other "Rel") in if uu___2 then - let uu___3 = FStar_Syntax_Print.term_to_string t1 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t1 in let uu___4 = FStar_Syntax_Print.tag_of_term t1 in - let uu___5 = FStar_Syntax_Print.term_to_string t2 in + let uu___5 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t2 in let uu___6 = FStar_Syntax_Print.tag_of_term t2 in FStar_Compiler_Util.print5 "Heads %s: %s (%s) and %s (%s)\n" (if need_unif then "need unification" else "match") uu___3 @@ -7893,10 +7950,12 @@ and (solve_t' : tprob -> worklist -> solution) = mklstr (fun uu___5 -> let uu___6 = - FStar_Syntax_Print.term_to_string head1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head1 in let uu___7 = args_to_string args1 in let uu___8 = - FStar_Syntax_Print.term_to_string head2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head2 in let uu___9 = args_to_string args2 in FStar_Compiler_Util.format4 "unequal number of arguments: %s[%s] and %s[%s]" @@ -8137,19 +8196,23 @@ and (solve_t' : tprob -> worklist -> solution) = then let uu___19 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t1 in let uu___20 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t1' in let uu___21 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t2 in let uu___22 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t2' in FStar_Compiler_Util.print4 "Unfolding didn't make progress ... got %s ~> %s;\nand %s ~> %s\n" @@ -8332,7 +8395,8 @@ and (solve_t' : tprob -> worklist -> solution) = if uu___7 then let uu___8 = - FStar_Syntax_Print.term_to_string pat_term1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term pat_term1 in FStar_Compiler_Util.print1 "Match heuristic, typechecking the pattern term: %s {\n\n" uu___8 @@ -8351,10 +8415,12 @@ and (solve_t' : tprob -> worklist -> solution) = if uu___9 then let uu___10 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term pat_term2 in let uu___11 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term pat_term_t in FStar_Compiler_Util.print2 "} Match heuristic, typechecked pattern term to %s and type %s\n" @@ -8468,8 +8534,10 @@ and (solve_t' : tprob -> worklist -> solution) = (FStar_Options.Other "Rel") in if uu___2 then - let uu___3 = FStar_Syntax_Print.term_to_string t1 in - let uu___4 = FStar_Syntax_Print.term_to_string t2 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t1 in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t2 in FStar_Compiler_Util.print2 "Trying match heuristic for %s vs. %s\n" uu___3 uu___4 else ()); @@ -8502,7 +8570,8 @@ and (solve_t' : tprob -> worklist -> solution) = if uu___11 then let uu___12 = - FStar_Syntax_Print.term_to_string scrutinee in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term scrutinee in FStar_Compiler_Util.print1 "match head %s is not a flex term\n" uu___12 else ()); @@ -8526,8 +8595,11 @@ and (solve_t' : tprob -> worklist -> solution) = if uu___13 then let uu___14 = - FStar_Syntax_Print.term_to_string scrutinee in - let uu___15 = FStar_Syntax_Print.term_to_string t in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term scrutinee in + let uu___15 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t in FStar_Compiler_Util.print2 "Heuristic applicable with scrutinee %s and other side = %s\n" uu___14 uu___15 @@ -8609,7 +8681,8 @@ and (solve_t' : tprob -> worklist -> solution) = let uu___17 = FStar_Syntax_Print.pat_to_string p in let uu___18 = - FStar_Syntax_Print.term_to_string e in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term e in FStar_Compiler_Util.print2 "Found head matching branch %s -> %s\n" uu___17 uu___18 @@ -8643,7 +8716,8 @@ and (solve_t' : tprob -> worklist -> solution) = if uu___11 then let uu___12 = - FStar_Syntax_Print.term_to_string scrutinee in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term scrutinee in FStar_Compiler_Util.print1 "match head %s is not a flex term\n" uu___12 else ()); @@ -8667,8 +8741,11 @@ and (solve_t' : tprob -> worklist -> solution) = if uu___13 then let uu___14 = - FStar_Syntax_Print.term_to_string scrutinee in - let uu___15 = FStar_Syntax_Print.term_to_string t in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term scrutinee in + let uu___15 = + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t in FStar_Compiler_Util.print2 "Heuristic applicable with scrutinee %s and other side = %s\n" uu___14 uu___15 @@ -8750,7 +8827,8 @@ and (solve_t' : tprob -> worklist -> solution) = let uu___17 = FStar_Syntax_Print.pat_to_string p in let uu___18 = - FStar_Syntax_Print.term_to_string e in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term e in FStar_Compiler_Util.print2 "Found head matching branch %s -> %s\n" uu___17 uu___18 @@ -8783,8 +8861,10 @@ and (solve_t' : tprob -> worklist -> solution) = then let uu___3 = FStar_Syntax_Print.tag_of_term t1 in let uu___4 = FStar_Syntax_Print.tag_of_term t2 in - let uu___5 = FStar_Syntax_Print.term_to_string t1 in - let uu___6 = FStar_Syntax_Print.term_to_string t2 in + let uu___5 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t1 in + let uu___6 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t2 in FStar_Compiler_Util.print4 "rigid_rigid_delta of %s-%s (%s, %s)\n" uu___3 uu___4 uu___5 uu___6 @@ -8976,7 +9056,8 @@ and (solve_t' : tprob -> worklist -> solution) = mklstr (fun uu___10 -> let uu___11 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head1 in let uu___12 = let uu___13 = @@ -8987,13 +9068,15 @@ and (solve_t' : tprob -> worklist -> solution) = uu___14 (fun x -> let uu___15 = - FStar_Syntax_Print.delta_depth_to_string + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_delta_depth x in FStar_Pervasives_Native.Some uu___15) in FStar_Compiler_Util.dflt "" uu___13 in let uu___13 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head2 in let uu___14 = let uu___15 = @@ -9004,7 +9087,8 @@ and (solve_t' : tprob -> worklist -> solution) = uu___16 (fun x -> let uu___17 = - FStar_Syntax_Print.delta_depth_to_string + FStar_Class_Show.show + FStar_Syntax_Syntax.showable_delta_depth x in FStar_Pervasives_Native.Some uu___17) in @@ -9031,9 +9115,11 @@ and (solve_t' : tprob -> worklist -> solution) = mklstr (fun uu___6 -> let uu___7 = - FStar_Syntax_Print.term_to_string t1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t1 in let uu___8 = - FStar_Syntax_Print.term_to_string t2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term t2 in FStar_Compiler_Util.format2 "head mismatch for subtyping (%s vs %s)" uu___7 uu___8) in @@ -9102,13 +9188,15 @@ and (solve_t' : tprob -> worklist -> solution) = let uu___9 = let uu___10 = FStar_Syntax_Print.tag_of_term t1 in let uu___11 = - let uu___12 = FStar_Syntax_Print.term_to_string t1 in + let uu___12 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t1 in Prims.op_Hat "::" uu___12 in Prims.op_Hat uu___10 uu___11 in let uu___10 = let uu___11 = FStar_Syntax_Print.tag_of_term t2 in let uu___12 = - let uu___13 = FStar_Syntax_Print.term_to_string t2 in + let uu___13 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t2 in Prims.op_Hat "::" uu___13 in Prims.op_Hat uu___11 uu___12 in FStar_Compiler_Util.print4 @@ -9375,10 +9463,12 @@ and (solve_t' : tprob -> worklist -> solution) = ((let uu___13 = FStar_Syntax_Print.bv_to_string x12 in let uu___14 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term x12.FStar_Syntax_Syntax.sort in let uu___15 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term phi11 in FStar_Compiler_Util.print3 "ref1 = (%s):(%s){%s}\n" uu___13 @@ -9386,10 +9476,12 @@ and (solve_t' : tprob -> worklist -> solution) = (let uu___13 = FStar_Syntax_Print.bv_to_string x22 in let uu___14 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term x22.FStar_Syntax_Syntax.sort in let uu___15 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term phi21 in FStar_Compiler_Util.print3 "ref2 = (%s):(%s){%s}\n" uu___13 @@ -10350,7 +10442,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool wl.smt_ok in let uu___15 = let uu___16 = - FStar_Syntax_Print.term_to_string head1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head1 in let uu___17 = let uu___18 = let uu___19 = @@ -10363,7 +10456,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool uu___21 in let uu___21 = let uu___22 = - FStar_Syntax_Print.term_to_string head2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head2 in let uu___23 = let uu___24 = let uu___25 = @@ -10486,7 +10580,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool wl.smt_ok in let uu___15 = let uu___16 = - FStar_Syntax_Print.term_to_string head1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head1 in let uu___17 = let uu___18 = let uu___19 = @@ -10499,7 +10594,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool uu___21 in let uu___21 = let uu___22 = - FStar_Syntax_Print.term_to_string head2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head2 in let uu___23 = let uu___24 = let uu___25 = @@ -10622,7 +10718,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool wl.smt_ok in let uu___15 = let uu___16 = - FStar_Syntax_Print.term_to_string head1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head1 in let uu___17 = let uu___18 = let uu___19 = @@ -10635,7 +10732,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool uu___21 in let uu___21 = let uu___22 = - FStar_Syntax_Print.term_to_string head2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head2 in let uu___23 = let uu___24 = let uu___25 = @@ -10758,7 +10856,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool wl.smt_ok in let uu___15 = let uu___16 = - FStar_Syntax_Print.term_to_string head1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head1 in let uu___17 = let uu___18 = let uu___19 = @@ -10771,7 +10870,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool uu___21 in let uu___21 = let uu___22 = - FStar_Syntax_Print.term_to_string head2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head2 in let uu___23 = let uu___24 = let uu___25 = @@ -10894,7 +10994,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool wl.smt_ok in let uu___15 = let uu___16 = - FStar_Syntax_Print.term_to_string head1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head1 in let uu___17 = let uu___18 = let uu___19 = @@ -10907,7 +11008,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool uu___21 in let uu___21 = let uu___22 = - FStar_Syntax_Print.term_to_string head2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head2 in let uu___23 = let uu___24 = let uu___25 = @@ -11030,7 +11132,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool wl.smt_ok in let uu___15 = let uu___16 = - FStar_Syntax_Print.term_to_string head1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head1 in let uu___17 = let uu___18 = let uu___19 = @@ -11043,7 +11146,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool uu___21 in let uu___21 = let uu___22 = - FStar_Syntax_Print.term_to_string head2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head2 in let uu___23 = let uu___24 = let uu___25 = @@ -11166,7 +11270,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool wl.smt_ok in let uu___15 = let uu___16 = - FStar_Syntax_Print.term_to_string head1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head1 in let uu___17 = let uu___18 = let uu___19 = @@ -11179,7 +11284,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool uu___21 in let uu___21 = let uu___22 = - FStar_Syntax_Print.term_to_string head2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head2 in let uu___23 = let uu___24 = let uu___25 = @@ -11302,7 +11408,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool wl.smt_ok in let uu___15 = let uu___16 = - FStar_Syntax_Print.term_to_string head1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head1 in let uu___17 = let uu___18 = let uu___19 = @@ -11315,7 +11422,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool uu___21 in let uu___21 = let uu___22 = - FStar_Syntax_Print.term_to_string head2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head2 in let uu___23 = let uu___24 = let uu___25 = @@ -11438,7 +11546,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool wl.smt_ok in let uu___15 = let uu___16 = - FStar_Syntax_Print.term_to_string head1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head1 in let uu___17 = let uu___18 = let uu___19 = @@ -11451,7 +11560,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool uu___21 in let uu___21 = let uu___22 = - FStar_Syntax_Print.term_to_string head2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head2 in let uu___23 = let uu___24 = let uu___25 = @@ -11574,7 +11684,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool wl.smt_ok in let uu___15 = let uu___16 = - FStar_Syntax_Print.term_to_string head1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head1 in let uu___17 = let uu___18 = let uu___19 = @@ -11587,7 +11698,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool uu___21 in let uu___21 = let uu___22 = - FStar_Syntax_Print.term_to_string head2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head2 in let uu___23 = let uu___24 = let uu___25 = @@ -11710,7 +11822,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool wl.smt_ok in let uu___15 = let uu___16 = - FStar_Syntax_Print.term_to_string head1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head1 in let uu___17 = let uu___18 = let uu___19 = @@ -11723,7 +11836,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool uu___21 in let uu___21 = let uu___22 = - FStar_Syntax_Print.term_to_string head2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head2 in let uu___23 = let uu___24 = let uu___25 = @@ -11846,7 +11960,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool wl.smt_ok in let uu___15 = let uu___16 = - FStar_Syntax_Print.term_to_string head1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head1 in let uu___17 = let uu___18 = let uu___19 = @@ -11859,7 +11974,8 @@ and (solve_t' : tprob -> worklist -> solution) = FStar_Compiler_Util.string_of_bool uu___21 in let uu___21 = let uu___22 = - FStar_Syntax_Print.term_to_string head2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term head2 in let uu___23 = let uu___24 = let uu___25 = @@ -11977,8 +12093,12 @@ and (solve_t' : tprob -> worklist -> solution) = let uu___10 = let uu___11 = FStar_Syntax_Print.tag_of_term t1 in let uu___12 = FStar_Syntax_Print.tag_of_term t2 in - let uu___13 = FStar_Syntax_Print.term_to_string t1 in - let uu___14 = FStar_Syntax_Print.term_to_string t2 in + let uu___13 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + t1 in + let uu___14 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + t2 in FStar_Compiler_Util.format4 "Internal error: unexpected flex-flex of %s and %s\n>>> (%s) -- (%s)" uu___11 uu___12 uu___13 uu___14 in @@ -11990,8 +12110,12 @@ and (solve_t' : tprob -> worklist -> solution) = let uu___10 = let uu___11 = FStar_Syntax_Print.tag_of_term t1 in let uu___12 = FStar_Syntax_Print.tag_of_term t2 in - let uu___13 = FStar_Syntax_Print.term_to_string t1 in - let uu___14 = FStar_Syntax_Print.term_to_string t2 in + let uu___13 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + t1 in + let uu___14 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + t2 in FStar_Compiler_Util.format4 "Internal error: unexpected flex-flex of %s and %s\n>>> (%s) -- (%s)" uu___11 uu___12 uu___13 uu___14 in @@ -12063,10 +12187,10 @@ and (solve_c : then let uu___2 = let uu___3 = FStar_Syntax_Syntax.mk_Comp c1_comp in - FStar_Syntax_Print.comp_to_string uu___3 in + FStar_Class_Show.show FStar_Syntax_Print.showable_comp uu___3 in let uu___3 = let uu___4 = FStar_Syntax_Syntax.mk_Comp c2_comp in - FStar_Syntax_Print.comp_to_string uu___4 in + FStar_Class_Show.show FStar_Syntax_Print.showable_comp uu___4 in FStar_Compiler_Util.print2 "solve_c is using an equality constraint (%s vs %s)\n" uu___2 uu___3 @@ -12237,13 +12361,13 @@ and (solve_c : FStar_Compiler_Effect.op_Bar_Greater c11 FStar_Syntax_Syntax.mk_Comp in FStar_Compiler_Effect.op_Bar_Greater uu___3 - FStar_Syntax_Print.comp_to_string in + (FStar_Class_Show.show FStar_Syntax_Print.showable_comp) in let uu___3 = let uu___4 = FStar_Compiler_Effect.op_Bar_Greater c21 FStar_Syntax_Syntax.mk_Comp in FStar_Compiler_Effect.op_Bar_Greater uu___4 - FStar_Syntax_Print.comp_to_string in + (FStar_Class_Show.show FStar_Syntax_Print.showable_comp) in FStar_Compiler_Util.print2 "solve_layered_sub c1: %s and c2: %s {\n" uu___2 uu___3 else ()); @@ -12430,7 +12554,8 @@ and (solve_c : FStar_Ident.string_of_lid c21.FStar_Syntax_Syntax.effect_name in let uu___12 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term c12.FStar_Syntax_Syntax.result_typ in FStar_Compiler_Util.format3 "Cannot lift erasable expression from %s ~> %s since its type %s is informative" @@ -12477,10 +12602,12 @@ and (solve_c : if uu___16 then let uu___17 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term a1 in let uu___18 = - FStar_Syntax_Print.term_to_string + FStar_Class_Show.show + FStar_Syntax_Print.showable_term a2 in FStar_Compiler_Util.print2 "Layered Effects teq (rel c1 index uvar) %s = %s\n" @@ -12739,9 +12866,11 @@ and (solve_c : let uu___8 = let uu___9 = let uu___10 = - FStar_Syntax_Print.term_to_string c1_repr in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term c1_repr in let uu___11 = - FStar_Syntax_Print.term_to_string c2_repr in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term c2_repr in FStar_Compiler_Util.format2 "sub effect repr: %s <: %s" uu___10 uu___11 in sub_prob wl c1_repr @@ -12847,7 +12976,8 @@ and (solve_c : FStar_TypeChecker_Env.Eager_unfolding; FStar_TypeChecker_Env.Primops; FStar_TypeChecker_Env.Simplify] env g in - FStar_Syntax_Print.term_to_string uu___12 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term uu___12 in FStar_Compiler_Util.print1 "WP guard (simplifed) is (%s)\n" uu___11 else ()); @@ -12881,8 +13011,10 @@ and (solve_c : (FStar_Options.Other "Rel") in if uu___3 then - let uu___4 = FStar_Syntax_Print.comp_to_string c1 in - let uu___5 = FStar_Syntax_Print.comp_to_string c2 in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_comp c1 in + let uu___5 = + FStar_Class_Show.show FStar_Syntax_Print.showable_comp c2 in FStar_Compiler_Util.print3 "solve_c %s %s %s\n" uu___4 (rel_to_string problem.FStar_TypeChecker_Common.relation) uu___5 @@ -13179,7 +13311,7 @@ let (print_pending_implicits : g.FStar_TypeChecker_Common.implicits (FStar_Compiler_List.map (fun i -> - FStar_Syntax_Print.ctx_uvar_to_string + FStar_Class_Show.show FStar_Syntax_Print.showable_ctxu i.FStar_TypeChecker_Common.imp_uvar)) in FStar_Compiler_Effect.op_Bar_Greater uu___ (FStar_Compiler_String.concat ", ") @@ -13192,7 +13324,8 @@ let (ineqs_to_string : let uu___ = FStar_Compiler_Effect.op_Bar_Greater (FStar_Pervasives_Native.fst ineqs) - (FStar_Compiler_List.map FStar_Syntax_Print.univ_to_string) in + (FStar_Compiler_List.map + (FStar_Class_Show.show FStar_Syntax_Print.showable_univ)) in FStar_Compiler_Effect.op_Bar_Greater uu___ (FStar_Compiler_String.concat ", ") in let ineqs1 = @@ -13203,8 +13336,12 @@ let (ineqs_to_string : (fun uu___1 -> match uu___1 with | (u1, u2) -> - let uu___2 = FStar_Syntax_Print.univ_to_string u1 in - let uu___3 = FStar_Syntax_Print.univ_to_string u2 in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ + u1 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ + u2 in FStar_Compiler_Util.format2 "%s < %s" uu___2 uu___3)) in FStar_Compiler_Effect.op_Bar_Greater uu___ (FStar_Compiler_String.concat ", ") in @@ -13454,8 +13591,12 @@ let (try_teq : (FStar_Options.Other "Rel") in if uu___5 then - let uu___6 = FStar_Syntax_Print.term_to_string t1 in - let uu___7 = FStar_Syntax_Print.term_to_string t2 in + let uu___6 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + t1 in + let uu___7 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term + t2 in let uu___8 = FStar_TypeChecker_Env.print_gamma env.FStar_TypeChecker_Env.gamma in @@ -13511,8 +13652,10 @@ let (teq : (FStar_Options.Other "Rel") in if uu___2 then - let uu___3 = FStar_Syntax_Print.term_to_string t1 in - let uu___4 = FStar_Syntax_Print.term_to_string t2 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t1 in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t2 in let uu___5 = guard_to_string env g in FStar_Compiler_Util.print3 "teq of %s and %s succeeded with guard %s\n" uu___3 uu___4 @@ -13533,8 +13676,10 @@ let (get_teq_predicate : (FStar_TypeChecker_Env.debug env) (FStar_Options.Other "Rel") in if uu___1 then - let uu___2 = FStar_Syntax_Print.term_to_string t1 in - let uu___3 = FStar_Syntax_Print.term_to_string t2 in + let uu___2 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t1 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t2 in FStar_Compiler_Util.print2 "get_teq_predicate of %s and %s {\n" uu___2 uu___3 else ()); @@ -13608,8 +13753,10 @@ let (sub_or_eq_comp : (FStar_Options.Other "Rel") in if uu___3 then - let uu___4 = FStar_Syntax_Print.comp_to_string c1 in - let uu___5 = FStar_Syntax_Print.comp_to_string c2 in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_comp c1 in + let uu___5 = + FStar_Class_Show.show FStar_Syntax_Print.showable_comp c2 in FStar_Compiler_Util.print3 "sub_comp of %s --and-- %s --with-- %s\n" uu___4 uu___5 (if rel = FStar_TypeChecker_Common.EQ @@ -13655,9 +13802,11 @@ let (sub_or_eq_comp : if uu___7 then let uu___8 = - FStar_Syntax_Print.comp_to_string c1 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_comp c1 in let uu___9 = - FStar_Syntax_Print.comp_to_string c2 in + FStar_Class_Show.show + FStar_Syntax_Print.showable_comp c2 in let uu___10 = FStar_Compiler_Util.string_of_int ms in FStar_Compiler_Util.print4 @@ -13728,8 +13877,12 @@ let (solve_universe_inequalities' : FStar_Syntax_Unionfind.rollback tx; (let uu___2 = let uu___3 = - let uu___4 = FStar_Syntax_Print.univ_to_string u1 in - let uu___5 = FStar_Syntax_Print.univ_to_string u2 in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ + u1 in + let uu___5 = + FStar_Class_Show.show FStar_Syntax_Print.showable_univ + u2 in FStar_Compiler_Util.format2 "Universe %s and %s are incompatible" uu___4 uu___5 in (FStar_Errors_Codes.Fatal_IncompatibleUniverse, uu___3) in @@ -13846,9 +13999,11 @@ let (solve_universe_inequalities' : if uu___7 then let uu___8 = - FStar_Syntax_Print.univ_to_string u in + FStar_Class_Show.show + FStar_Syntax_Print.showable_univ u in let uu___9 = - FStar_Syntax_Print.univ_to_string v in + FStar_Class_Show.show + FStar_Syntax_Print.showable_univ v in FStar_Compiler_Util.print2 "%s let uu___6 = - FStar_Syntax_Print.term_to_string imp_tm in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term imp_tm in let uu___7 = FStar_Compiler_Range_Ops.string_of_range imp_range in @@ -15105,7 +15276,8 @@ let (resolve_implicits' : if uu___5 then let uu___6 = - FStar_Syntax_Print.term_to_string tm in + FStar_Class_Show.show + FStar_Syntax_Print.showable_term tm in let uu___7 = FStar_Syntax_Print.ctx_uvar_to_string ctx_u in @@ -15538,8 +15710,10 @@ let (layered_effect_teq : else FStar_Compiler_Effect.op_Bar_Greater reason FStar_Compiler_Util.must in - let uu___3 = FStar_Syntax_Print.term_to_string t1 in - let uu___4 = FStar_Syntax_Print.term_to_string t2 in + let uu___3 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t1 in + let uu___4 = + FStar_Class_Show.show FStar_Syntax_Print.showable_term t2 in FStar_Compiler_Util.print3 "Layered Effect (%s) %s = %s\n" uu___2 uu___3 uu___4 else ()); diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcEffect.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcEffect.ml index 83eddbfaf96..aa6ccfde9a8 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcEffect.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcEffect.ml @@ -21,85 +21,108 @@ let (check_and_gen : fun uu___ -> match uu___ with | (us, t) -> - let uu___1 = FStar_Syntax_Subst.open_univ_vars us t in - (match uu___1 with - | (us1, t1) -> - let uu___2 = - let uu___3 = + let uu___1 = + let uu___2 = + let uu___3 = + let uu___4 = + FStar_Class_Show.show + (FStar_Class_Show.show_tuple2 + (FStar_Class_Show.show_list + FStar_Ident.showable_ident) + FStar_Syntax_Print.showable_term) (us, t) in + Prims.op_Hat " = " uu___4 in + Prims.op_Hat comb uu___3 in + Prims.op_Hat "While checking combinator " uu___2 in + FStar_Errors.with_ctx uu___1 + (fun uu___2 -> + let uu___3 = FStar_Syntax_Subst.open_univ_vars us t in + match uu___3 with + | (us1, t1) -> let uu___4 = - FStar_TypeChecker_Env.push_univ_vars env us1 in - FStar_TypeChecker_TcTerm.tc_tot_or_gtot_term uu___4 - t1 in - match uu___3 with - | (t2, lc, g) -> - (FStar_TypeChecker_Rel.force_trivial_guard env g; - (t2, (lc.FStar_TypeChecker_Common.res_typ))) in - (match uu___2 with - | (t2, ty) -> - let uu___3 = - FStar_TypeChecker_Generalize.generalize_universes - env t2 in - (match uu___3 with - | (g_us, t3) -> - let ty1 = - FStar_Syntax_Subst.close_univ_vars g_us ty in - (if (FStar_Compiler_List.length g_us) <> n - then - (let error = - let uu___4 = - FStar_Compiler_Util.string_of_int n in - let uu___5 = - let uu___6 = - FStar_Compiler_Effect.op_Bar_Greater - g_us FStar_Compiler_List.length in - FStar_Compiler_Effect.op_Bar_Greater - uu___6 - FStar_Compiler_Util.string_of_int in - let uu___6 = - FStar_Syntax_Print.tscheme_to_string - (g_us, t3) in - FStar_Compiler_Util.format5 - "Expected %s:%s to be universe-polymorphic in %s universes, but found %s (tscheme: %s)" - eff_name comb uu___4 uu___5 uu___6 in - FStar_Errors.raise_error - (FStar_Errors_Codes.Fatal_MismatchUniversePolymorphic, - error) t3.FStar_Syntax_Syntax.pos; - (match us1 with - | [] -> () - | uu___5 -> - let uu___6 = - ((FStar_Compiler_List.length us1) = - (FStar_Compiler_List.length g_us)) - && - (FStar_Compiler_List.forall2 - (fun u1 -> - fun u2 -> - let uu___7 = - FStar_Syntax_Syntax.order_univ_name - u1 u2 in - uu___7 = Prims.int_zero) - us1 g_us) in - if uu___6 - then () - else - (let uu___8 = - let uu___9 = - let uu___10 = - FStar_Syntax_Print.univ_names_to_string - us1 in - let uu___11 = - FStar_Syntax_Print.univ_names_to_string - g_us in - FStar_Compiler_Util.format4 - "Expected and generalized universes in the declaration for %s:%s are different, input: %s, but after gen: %s" - eff_name comb uu___10 - uu___11 in - (FStar_Errors_Codes.Fatal_UnexpectedNumberOfUniverse, - uu___9) in - FStar_Errors.raise_error uu___8 - t3.FStar_Syntax_Syntax.pos))) - else (); - (g_us, t3, ty1))))) + let uu___5 = + let uu___6 = + FStar_TypeChecker_Env.push_univ_vars env us1 in + FStar_TypeChecker_TcTerm.tc_tot_or_gtot_term + uu___6 t1 in + match uu___5 with + | (t2, lc, g) -> + (FStar_TypeChecker_Rel.force_trivial_guard env + g; + (t2, (lc.FStar_TypeChecker_Common.res_typ))) in + (match uu___4 with + | (t2, ty) -> + let uu___5 = + FStar_TypeChecker_Generalize.generalize_universes + env t2 in + (match uu___5 with + | (g_us, t3) -> + let ty1 = + FStar_Syntax_Subst.close_univ_vars g_us + ty in + (if (FStar_Compiler_List.length g_us) <> n + then + (let error = + let uu___6 = + FStar_Compiler_Util.string_of_int + n in + let uu___7 = + let uu___8 = + FStar_Compiler_Effect.op_Bar_Greater + g_us + FStar_Compiler_List.length in + FStar_Compiler_Effect.op_Bar_Greater + uu___8 + FStar_Compiler_Util.string_of_int in + let uu___8 = + FStar_Syntax_Print.tscheme_to_string + (g_us, t3) in + FStar_Compiler_Util.format5 + "Expected %s:%s to be universe-polymorphic in %s universes, but found %s (tscheme: %s)" + eff_name comb uu___6 uu___7 uu___8 in + FStar_Errors.raise_error + (FStar_Errors_Codes.Fatal_MismatchUniversePolymorphic, + error) t3.FStar_Syntax_Syntax.pos; + (match us1 with + | [] -> () + | uu___7 -> + let uu___8 = + ((FStar_Compiler_List.length + us1) + = + (FStar_Compiler_List.length + g_us)) + && + (FStar_Compiler_List.forall2 + (fun u1 -> + fun u2 -> + let uu___9 = + FStar_Syntax_Syntax.order_univ_name + u1 u2 in + uu___9 = + Prims.int_zero) us1 + g_us) in + if uu___8 + then () + else + (let uu___10 = + let uu___11 = + let uu___12 = + FStar_Syntax_Print.univ_names_to_string + us1 in + let uu___13 = + FStar_Syntax_Print.univ_names_to_string + g_us in + FStar_Compiler_Util.format4 + "Expected and generalized universes in the declaration for %s:%s are different, input: %s, but after gen: %s" + eff_name comb uu___12 + uu___13 in + (FStar_Errors_Codes.Fatal_UnexpectedNumberOfUniverse, + uu___11) in + FStar_Errors.raise_error + uu___10 + t3.FStar_Syntax_Syntax.pos))) + else (); + (g_us, t3, ty1))))) let (pure_wp_uvar : FStar_TypeChecker_Env.env -> FStar_Syntax_Syntax.typ -> diff --git a/src/class/FStar.Class.Show.fst b/src/class/FStar.Class.Show.fst index 9a65b6b4a19..51670f11ea3 100644 --- a/src/class/FStar.Class.Show.fst +++ b/src/class/FStar.Class.Show.fst @@ -11,6 +11,18 @@ instance show_list (a:Type) (_ : showable a) : Tot (showable (list a)) = { show = FStar.Common.string_of_list show; } +instance show_option (a:Type) (_ : showable a) : Tot (showable (option a)) = { + show = FStar.Common.string_of_option show; +} + +instance show_either + (_ : showable 'a) + (_ : showable 'b) += { + show = (function Inl x -> "Inl " ^ show x + | Inr y -> "Inr " ^ show y); +} + instance show_tuple2 (_ : showable 'a) (_ : showable 'b) diff --git a/src/class/FStar.Class.Show.fsti b/src/class/FStar.Class.Show.fsti index ec1e34b9a9d..9dc08feeb4f 100644 --- a/src/class/FStar.Class.Show.fsti +++ b/src/class/FStar.Class.Show.fsti @@ -13,6 +13,13 @@ instance val printableshow (_ : printable 'a) : Tot (showable 'a) instance val show_list (a:Type) (_ : showable a) : Tot (showable (list a)) +instance val show_option (a:Type) (_ : showable a) : Tot (showable (option a)) + +instance val show_either + (_ : showable 'a) + (_ : showable 'b) +: Tot (showable (either 'a 'b)) + instance val show_tuple2 (_ : showable 'a) (_ : showable 'b) diff --git a/src/syntax/FStar.Syntax.Embeddings.Base.fst b/src/syntax/FStar.Syntax.Embeddings.Base.fst index 4cd673f0345..a0c6dde84b2 100644 --- a/src/syntax/FStar.Syntax.Embeddings.Base.fst +++ b/src/syntax/FStar.Syntax.Embeddings.Base.fst @@ -23,6 +23,7 @@ open FStar.Compiler.Range open FStar.Pervasives open FStar.Syntax.Syntax open FStar.Class.Show +open FStar.Class.PP open FStar.Class.Deq module BU = FStar.Compiler.Util @@ -126,13 +127,13 @@ type embedding (a:Type0) = { } let emb_typ_of e = e.emb_typ -let unknown_printer typ _ = - BU.format1 "unknown %s" (Print.term_to_string typ) +let unknown_printer (typ : term) (_ : 'a) : string = + BU.format1 "unknown %s" (show typ) let term_as_fv t = match (SS.compress t).n with | Tm_fvar fv -> fv - | _ -> failwith (BU.format1 "Embeddings not defined for type %s" (Print.term_to_string t)) + | _ -> failwith (BU.format1 "Embeddings not defined for type %s" (show t)) let mk_emb em un fv = let typ = S.fv_to_tm fv in @@ -203,9 +204,9 @@ let unembed (e:embedding 'a) t n = let open FStar.Pprint in if None? r then Err.log_issue_doc t.pos (Err.Warning_NotEmbedded, [ - text "Unembedding failed for type" ^/^ Print.term_to_doc (type_of e); - text "emb_typ = " ^/^ doc_of_string (Print.emb_typ_to_string (emb_typ_of e)); - text "Term =" ^/^ Print.term_to_doc t; + text "Unembedding failed for type" ^/^ pp (type_of e); + text "emb_typ = " ^/^ doc_of_string (show (emb_typ_of e)); + text "Term =" ^/^ pp t; ]); r @@ -237,11 +238,11 @@ let e_lazy #a (k:lazy_kind) (ty : typ) : embedding a = in mk_emb ee uu (term_as_fv ty) -let lazy_embed (pa:printer 'a) (et:emb_typ) rng ta (x:'a) (f:unit -> term) = +let lazy_embed (pa:printer 'a) (et:emb_typ) rng (ta:term) (x:'a) (f:unit -> term) = if !Options.debug_embedding then BU.print3 "Embedding a %s\n\temb_typ=%s\n\tvalue is %s\n" - (Print.term_to_string ta) - (Print.emb_typ_to_string et) + (show ta) + (show et) (pa x); if !Options.eager_embedding then f() @@ -257,24 +258,22 @@ let lazy_unembed (pa:printer 'a) (et:emb_typ) (x:term) (ta:term) (f:term -> opti then let res = f (Thunk.force t) in let _ = if !Options.debug_embedding then BU.print3 "Unembed cancellation failed\n\t%s <> %s\nvalue is %s\n" - (Print.emb_typ_to_string et) - (Print.emb_typ_to_string et') + (show et) + (show et') (match res with None -> "None" | Some x -> "Some " ^ (pa x)) in res else let a = Dyn.undyn b in let _ = if !Options.debug_embedding then BU.print2 "Unembed cancelled for %s\n\tvalue is %s\n" - (Print.emb_typ_to_string et) - (pa a) + (show et) (pa a) in Some a | _ -> let aopt = f x in let _ = if !Options.debug_embedding then BU.print3 "Unembedding:\n\temb_typ=%s\n\tterm is %s\n\tvalue is %s\n" - (Print.emb_typ_to_string et) - (Print.term_to_string x) + (show et) (show x) (match aopt with None -> "None" | Some a -> "Some " ^ pa a) in aopt diff --git a/src/syntax/FStar.Syntax.Embeddings.fst b/src/syntax/FStar.Syntax.Embeddings.fst index 9963d2d25a7..8b197217ad9 100644 --- a/src/syntax/FStar.Syntax.Embeddings.fst +++ b/src/syntax/FStar.Syntax.Embeddings.fst @@ -24,6 +24,8 @@ open FStar.Syntax.Syntax open FStar.Compiler.Range open FStar.VConfig +open FStar.Class.Show + module BU = FStar.Compiler.Util module C = FStar.Const module Err = FStar.Errors @@ -134,11 +136,11 @@ let term_as_fv t = | Tm_fvar fv -> fv | _ -> failwith (BU.format1 "Embeddings not defined for type %s" (Print.term_to_string t)) -let lazy_embed (pa:printer 'a) (et:emb_typ) rng ta (x:'a) (f:unit -> term) = +let lazy_embed (pa:printer 'a) (et:emb_typ) rng (ta:term) (x:'a) (f:unit -> term) = if !Options.debug_embedding then BU.print3 "Embedding a %s\n\temb_typ=%s\n\tvalue is %s\n" - (Print.term_to_string ta) - (Print.emb_typ_to_string et) + (show ta) + (show et) (pa x); if !Options.eager_embedding then f() @@ -154,15 +156,15 @@ let lazy_unembed (pa:printer 'a) (et:emb_typ) (x:term) (ta:term) (f:term -> opti then let res = f (Thunk.force t) in let _ = if !Options.debug_embedding then BU.print3 "Unembed cancellation failed\n\t%s <> %s\nvalue is %s\n" - (Print.emb_typ_to_string et) - (Print.emb_typ_to_string et') + (show et) + (show et') (match res with None -> "None" | Some x -> "Some " ^ (pa x)) in res else let a = Dyn.undyn b in let _ = if !Options.debug_embedding then BU.print2 "Unembed cancelled for %s\n\tvalue is %s\n" - (Print.emb_typ_to_string et) + (show et) (pa a) in Some a @@ -170,7 +172,7 @@ let lazy_unembed (pa:printer 'a) (et:emb_typ) (x:term) (ta:term) (f:term -> opti let aopt = f x in let _ = if !Options.debug_embedding then BU.print3 "Unembedding:\n\temb_typ=%s\n\tterm is %s\n\tvalue is %s\n" - (Print.emb_typ_to_string et) + (show et) (Print.term_to_string x) (match aopt with None -> "None" | Some a -> "Some " ^ pa a) in aopt diff --git a/src/syntax/FStar.Syntax.Print.Pretty.fst b/src/syntax/FStar.Syntax.Print.Pretty.fst index 1846a7eda14..a6e6cb4ea40 100644 --- a/src/syntax/FStar.Syntax.Print.Pretty.fst +++ b/src/syntax/FStar.Syntax.Print.Pretty.fst @@ -32,11 +32,21 @@ let term_to_doc' env (tm:term) : Pprint.document = GenSym.with_frozen_gensym (fu ToDocument.term_to_document e ) +let univ_to_doc' env (u:universe) : Pprint.document = GenSym.with_frozen_gensym (fun () -> + let e = Resugar.resugar_universe' env u Range.dummyRange in + ToDocument.term_to_document e +) + let term_to_string' env (tm:term) : string = GenSym.with_frozen_gensym (fun () -> let d = term_to_doc' env tm in pp d ) +let univ_to_string' env (u:universe) : string = GenSym.with_frozen_gensym (fun () -> + let d = univ_to_doc' env u in + pp d +) + let comp_to_doc' env (c:comp) : Pprint.document = GenSym.with_frozen_gensym (fun () -> let e = Resugar.resugar_comp' env c in ToDocument.term_to_document e @@ -58,7 +68,7 @@ let sigelt_to_string' env (se:sigelt) : string = GenSym.with_frozen_gensym (fun pp d ) -(* These three are duplicated instead of being a special case +(* These are duplicated instead of being a special case of the above so we can reuse the empty_env created at module load time for DsEnv. Otherwise we need to create another empty DsEnv.env here. *) @@ -67,6 +77,11 @@ let term_to_doc (tm:term) : Pprint.document = GenSym.with_frozen_gensym (fun () ToDocument.term_to_document e ) +let univ_to_doc (u:universe) : Pprint.document = GenSym.with_frozen_gensym (fun () -> + let e = Resugar.resugar_universe u Range.dummyRange in + ToDocument.term_to_document e +) + let comp_to_doc (c:comp) : Pprint.document = GenSym.with_frozen_gensym (fun () -> let e = Resugar.resugar_comp c in ToDocument.term_to_document e diff --git a/src/syntax/FStar.Syntax.Print.Pretty.fsti b/src/syntax/FStar.Syntax.Print.Pretty.fsti index 57463abafdd..6c907db2c3e 100644 --- a/src/syntax/FStar.Syntax.Print.Pretty.fsti +++ b/src/syntax/FStar.Syntax.Print.Pretty.fsti @@ -24,23 +24,26 @@ open FStar.Compiler.Util (* Use the 'primed' versions if possible: they abbreviate lidents *) val term_to_doc' : DsEnv.env -> term -> Pprint.document +val univ_to_doc' : DsEnv.env -> universe -> Pprint.document val comp_to_doc' : DsEnv.env -> comp -> Pprint.document val sigelt_to_doc' : DsEnv.env -> sigelt -> Pprint.document val term_to_string' : DsEnv.env -> term -> string +val univ_to_string' : DsEnv.env -> universe -> string val comp_to_string' : DsEnv.env -> comp -> string val sigelt_to_string' : DsEnv.env -> sigelt -> string (* If no DsEnv.env is at hand, these can be used instead. *) val term_to_doc : term -> Pprint.document +val univ_to_doc : universe -> Pprint.document val comp_to_doc : comp -> Pprint.document val sigelt_to_doc : sigelt -> Pprint.document val term_to_string : term -> string +val univ_to_string : universe -> string val comp_to_string : comp -> string val sigelt_to_string : sigelt -> string -val univ_to_string : universe -> string val tscheme_to_string : tscheme -> string val pat_to_string : pat -> string val binder_to_string' : bool -> binder -> string diff --git a/src/syntax/FStar.Syntax.Print.fst b/src/syntax/FStar.Syntax.Print.fst index 8d44e1eabec..717f2cb2d9f 100644 --- a/src/syntax/FStar.Syntax.Print.fst +++ b/src/syntax/FStar.Syntax.Print.fst @@ -36,11 +36,6 @@ module C = FStar.Parser.Const module SU = FStar.Syntax.Util module Pretty = FStar.Syntax.Print.Pretty -let rec delta_depth_to_string = function - | Delta_constant_at_level i -> "Delta_constant_at_level " ^ string_of_int i - | Delta_equational_at_level i -> "Delta_equational_at_level " ^ string_of_int i - | Delta_abstract d -> "Delta_abstract (" ^ delta_depth_to_string d ^ ")" - let sli (l:lident) : string = if Options.print_real_names() then string_of_lid l @@ -52,7 +47,7 @@ let sli (l:lident) : string = let lid_to_string (l:lid) = sli l // let fv_to_string fv = Printf.sprintf "%s@%A" (lid_to_string fv.fv_name.v) fv.fv_delta -let fv_to_string fv = lid_to_string fv.fv_name.v //^ "(@@" ^ delta_depth_to_string fv.fv_delta ^ ")" +let fv_to_string fv = lid_to_string fv.fv_name.v //^ "(@@" ^ showfv.fv_delta ^ ")" let bv_to_string bv = (string_of_id bv.ppname) ^ "#" ^ (string_of_int bv.index) let nm_to_string bv = @@ -155,12 +150,6 @@ let quals_to_string' quals = let paren s = "(" ^ s ^ ")" -let rec emb_typ_to_string = function - | ET_abstract -> "abstract" - | ET_app (h, []) -> h - | ET_app(h, args) -> "(" ^h^ " " ^ (List.map emb_typ_to_string args |> String.concat " ") ^")" - | ET_fun(a, b) -> "(" ^ emb_typ_to_string a ^ ") -> " ^ emb_typ_to_string b - let lkind_to_string = function | BadLazy -> "BadLazy" | Lazy_bv -> "Lazy_bv" @@ -175,7 +164,7 @@ let lkind_to_string = function | Lazy_sigelt -> "Lazy_sigelt" | Lazy_uvar -> "Lazy_uvar" | Lazy_letbinding -> "Lazy_letbinding" - | Lazy_embedding (e, _) -> "Lazy_embedding(" ^ emb_typ_to_string e ^ ")" + | Lazy_embedding (e, _) -> "Lazy_embedding(" ^ show e ^ ")" | Lazy_universe -> "Lazy_universe" | Lazy_universe_uvar -> "Lazy_universe_uvar" | Lazy_issue -> "Lazy_issue" @@ -962,6 +951,11 @@ let term_to_doc' dsenv t = then Pprint.arbitrary_string (term_to_string t) else Pretty.term_to_doc' dsenv t +let univ_to_doc' dsenv t = + if Options.ugly () + then Pprint.arbitrary_string (univ_to_string t) + else Pretty.univ_to_doc' dsenv t + let comp_to_doc' dsenv t = if Options.ugly () then Pprint.arbitrary_string (comp_to_string t) @@ -977,6 +971,11 @@ let term_to_doc t = then Pprint.arbitrary_string (term_to_string t) else Pretty.term_to_doc t +let univ_to_doc t = + if Options.ugly () + then Pprint.arbitrary_string (univ_to_string t) + else Pretty.univ_to_doc t + let comp_to_doc t = if Options.ugly () then Pprint.arbitrary_string (comp_to_string t) @@ -987,12 +986,15 @@ let sigelt_to_doc t = then Pprint.arbitrary_string (sigelt_to_string t) else Pretty.sigelt_to_doc t +instance pretty_term = { pp = term_to_doc; } +instance pretty_univ = { pp = univ_to_doc; } instance pretty_sigelt = { pp = sigelt_to_doc; } instance pretty_comp = { pp = comp_to_doc; } -instance pretty_term = { pp = term_to_doc; } -instance showable_sigelt = { show = sigelt_to_string; } instance showable_term = { show = term_to_string; } +instance showable_univ = { show = univ_to_string; } +instance showable_comp = { show = comp_to_string; } +instance showable_sigelt = { show = sigelt_to_string; } instance showable_bv = { show = bv_to_string; } instance showable_binder = { show = binder_to_string; } instance showable_uvar = { show = uvar_to_string; } diff --git a/src/syntax/FStar.Syntax.Print.fsti b/src/syntax/FStar.Syntax.Print.fsti index 577a69ef414..239d66b14a6 100644 --- a/src/syntax/FStar.Syntax.Print.fsti +++ b/src/syntax/FStar.Syntax.Print.fsti @@ -74,14 +74,11 @@ val quals_to_string : list qualifier -> string val tscheme_to_string : tscheme -> string val cflag_to_string : cflag -> string val cflags_to_string : list cflag -> string -val delta_depth_to_string : delta_depth -> string val action_to_string : action -> string val metadata_to_string : metadata -> string val ctx_uvar_to_string : ctx_uvar -> string val ctx_uvar_to_string_no_reason : ctx_uvar -> string -val emb_typ_to_string: emb_typ -> string - val fv_qual_to_string : fv_qual -> string val term_to_doc' : DsEnv.env -> term -> Pprint.document @@ -93,10 +90,13 @@ val comp_to_doc : comp -> Pprint.document val sigelt_to_doc : sigelt -> Pprint.document instance val pretty_term : pretty term +instance val pretty_univ : pretty universe instance val pretty_comp : pretty comp instance val pretty_sigelt : pretty sigelt instance val showable_term : showable term +instance val showable_univ : showable universe +instance val showable_comp : showable comp instance val showable_sigelt : showable sigelt instance val showable_bv : showable bv instance val showable_binder : showable binder diff --git a/src/syntax/FStar.Syntax.Syntax.fst b/src/syntax/FStar.Syntax.Syntax.fst index 9fc8b85fe7b..bcf543f26ba 100644 --- a/src/syntax/FStar.Syntax.Syntax.fst +++ b/src/syntax/FStar.Syntax.Syntax.fst @@ -31,6 +31,26 @@ module PC = FStar.Parser.Const module Err = FStar.Errors module GS = FStar.GenSym +let rec emb_typ_to_string = function + | ET_abstract -> "abstract" + | ET_app (h, []) -> h + | ET_app(h, args) -> "(" ^h^ " " ^ (List.map emb_typ_to_string args |> String.concat " ") ^")" + | ET_fun(a, b) -> "(" ^ emb_typ_to_string a ^ ") -> " ^ emb_typ_to_string b + +instance showable_emb_typ = { + show = emb_typ_to_string; +} + + +let rec delta_depth_to_string = function + | Delta_constant_at_level i -> "Delta_constant_at_level " ^ string_of_int i + | Delta_equational_at_level i -> "Delta_equational_at_level " ^ string_of_int i + | Delta_abstract d -> "Delta_abstract (" ^ delta_depth_to_string d ^ ")" + +instance showable_delta_depth = { + show = delta_depth_to_string; +} + // This is set in FStar.Main.main, where all modules are in-scope. let lazy_chooser : ref (option (lazy_kind -> lazyinfo -> term)) = mk_ref None diff --git a/src/syntax/FStar.Syntax.Syntax.fsti b/src/syntax/FStar.Syntax.Syntax.fsti index c94d679efbb..7962af809a1 100644 --- a/src/syntax/FStar.Syntax.Syntax.fsti +++ b/src/syntax/FStar.Syntax.Syntax.fsti @@ -66,6 +66,8 @@ type emb_typ = | ET_fun of emb_typ * emb_typ | ET_app of string * list emb_typ +instance val showable_emb_typ : showable emb_typ + //versioning for unification variables [@@ PpxDerivingYoJson; PpxDerivingShow ] type version = { @@ -110,6 +112,8 @@ type delta_depth = | Delta_equational_at_level of int //level 0 is a symbol that may be equated to another by extensional reasoning, n > 0 can be unfolded n times to a Delta_equational_at_level 0 term | Delta_abstract of delta_depth //A symbol marked abstract whose depth is the argument d +instance val showable_delta_depth : showable delta_depth + [@@ PpxDerivingYoJson; PpxDerivingShow ] type should_check_uvar = | Allow_unresolved of string (* Escape hatch for uvars in logical guards that are sometimes left unresolved *) diff --git a/src/typechecker/FStar.TypeChecker.Cfg.fst b/src/typechecker/FStar.TypeChecker.Cfg.fst index a7dd4d36ac1..8eda1955f2b 100644 --- a/src/typechecker/FStar.TypeChecker.Cfg.fst +++ b/src/typechecker/FStar.TypeChecker.Cfg.fst @@ -12,6 +12,8 @@ open FStar.Syntax.Syntax open FStar.TypeChecker open FStar.TypeChecker.Env +open FStar.Class.Show + module S = FStar.Syntax.Syntax module SS = FStar.Syntax.Subst module BU = FStar.Compiler.Util @@ -72,7 +74,7 @@ let steps_to_string f = f.hnf |> b; f.primops |> b; f.do_not_unfold_pure_lets |> b; - f.unfold_until |> format_opt Print.delta_depth_to_string; + f.unfold_until |> format_opt show; f.unfold_only |> format_opt (fun x -> List.map Ident.string_of_lid x |> String.concat ", "); f.unfold_fully |> format_opt (fun x -> List.map Ident.string_of_lid x |> String.concat ", "); f.unfold_attr |> format_opt (fun x -> List.map Ident.string_of_lid x |> String.concat ", "); diff --git a/src/typechecker/FStar.TypeChecker.Env.fst b/src/typechecker/FStar.TypeChecker.Env.fst index f9628db0f97..32053f9ec64 100644 --- a/src/typechecker/FStar.TypeChecker.Env.fst +++ b/src/typechecker/FStar.TypeChecker.Env.fst @@ -29,6 +29,9 @@ open FStar.Compiler.Range open FStar.Errors open FStar.TypeChecker.Common +open FStar.Class.Show +open FStar.Class.PP + module S = FStar.Syntax.Syntax module SS = FStar.Syntax.Subst module BU = FStar.Compiler.Util @@ -794,8 +797,8 @@ let delta_depth_of_fv env fv = && Options.debug_any() then BU.print3 "WARNING WARNING WARNING fv=%s, delta_depth=%s, env.delta_depth=%s\n" (Print.fv_to_string fv) - (Print.delta_depth_to_string (Some?.v fv.fv_delta)) - (Print.delta_depth_to_string d); + (show (Some?.v fv.fv_delta)) + (show d); BU.smap_add env.fv_delta_depths (string_of_lid lid) d; d) @@ -1185,7 +1188,7 @@ instance hasNames_lcomp : hasNames lcomp = { freeNames = (fun lc -> freeNames (fst (lcomp_comp lc))); } -instance pretty_lcomp : FStar.Class.PP.pretty lcomp = { +instance pretty_lcomp : pretty lcomp = { pp = (fun lc -> let open FStar.Pprint in empty); } @@ -1195,11 +1198,11 @@ instance hasNames_guard : hasNames guard_t = { | NonTrivial f -> freeNames f); } -instance pretty_guard : Class.PP.pretty guard_t = { +instance pretty_guard : pretty guard_t = { pp = (fun g -> let open FStar.Pprint in match g.guard_f with | Trivial -> doc_of_string "Trivial" - | NonTrivial f -> doc_of_string "NonTrivial" ^/^ Class.PP.pp f); + | NonTrivial f -> doc_of_string "NonTrivial" ^/^ pp f); } let comp_to_comp_typ (env:env) c = @@ -1728,7 +1731,7 @@ let string_of_delta_level = function | NoDelta -> "NoDelta" | InliningDelta -> "Inlining" | Eager_unfolding_only -> "Eager_unfolding_only" - | Unfold d -> "Unfold " ^ Print.delta_depth_to_string d + | Unfold d -> "Unfold " ^ show d let lidents env : list lident = let keys = List.collect fst env.gamma_sig in diff --git a/src/typechecker/FStar.TypeChecker.NBETerm.fst b/src/typechecker/FStar.TypeChecker.NBETerm.fst index 2006c00540a..69f8ae82a09 100644 --- a/src/typechecker/FStar.TypeChecker.NBETerm.fst +++ b/src/typechecker/FStar.TypeChecker.NBETerm.fst @@ -26,6 +26,7 @@ open FStar.Ident open FStar.Errors open FStar.Char open FStar.String +open FStar.Class.Show friend FStar.Pervasives (* To expose norm_step *) @@ -194,7 +195,7 @@ let rec t_to_string (x:t) = | Reflect t -> "Reflect " ^ t_to_string t | Quote _ -> "Quote _" | Lazy (Inl li, _) -> BU.format1 "Lazy (Inl {%s})" (P.term_to_string (U.unfold_lazy li)) - | Lazy (Inr (_, et), _) -> BU.format1 "Lazy (Inr (?, %s))" (P.emb_typ_to_string et) + | Lazy (Inr (_, et), _) -> BU.format1 "Lazy (Inr (?, %s))" (show et) | LocalLetRec (_, l, _, _, _, _, _) -> "LocalLetRec (" ^ (FStar.Syntax.Print.lbs_to_string [] (true, [l])) ^ ")" | TopLevelLet (lb, _, _) -> "TopLevelLet (" ^ FStar.Syntax.Print.fv_to_string (BU.right lb.lbname) ^ ")" | TopLevelRec (lb, _, _, _) -> "TopLevelRec (" ^ FStar.Syntax.Print.fv_to_string (BU.right lb.lbname) ^ ")" @@ -251,7 +252,7 @@ let make_arrow1 t1 (a:arg) : t = mk_t <| Arrow (Inr ([a], Tot t1)) let lazy_embed (et:emb_typ) (x:'a) (f:unit -> t) = if !Options.debug_embedding then BU.print1 "Embedding\n\temb_typ=%s\n" - (P.emb_typ_to_string et); + (show et); if !Options.eager_embedding then f() else let thunk = Thunk.mk f in @@ -269,21 +270,21 @@ let lazy_unembed (et:emb_typ) (x:t) (f:t -> option 'a) : option 'a = then let res = f (Thunk.force thunk) in let _ = if !Options.debug_embedding then BU.print2 "Unembed cancellation failed\n\t%s <> %s\n" - (P.emb_typ_to_string et) - (P.emb_typ_to_string et') + (show et) + (show et') in res else let a = FStar.Compiler.Dyn.undyn b in let _ = if !Options.debug_embedding then BU.print1 "Unembed cancelled for %s\n" - (P.emb_typ_to_string et) + (show et) in Some a | _ -> let aopt = f x in let _ = if !Options.debug_embedding then BU.print1 "Unembedding:\n\temb_typ=%s\n" - (P.emb_typ_to_string et) in + (show et) in aopt let lazy_unembed_lazy_kind (#a:Type) (k:lazy_kind) (x:t) : option a = diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fst b/src/typechecker/FStar.TypeChecker.Normalize.fst index 77d736f6389..86a0dfc5ec7 100644 --- a/src/typechecker/FStar.TypeChecker.Normalize.fst +++ b/src/typechecker/FStar.TypeChecker.Normalize.fst @@ -35,6 +35,8 @@ open FStar.TypeChecker.Common open FStar.TypeChecker.Env open FStar.TypeChecker.Cfg +open FStar.Class.Show + module S = FStar.Syntax.Syntax module SS = FStar.Syntax.Subst //basic util @@ -931,7 +933,7 @@ let should_unfold cfg should_reify fv qninfo : should_unfold_res = let default_unfolding () = log_unfolding cfg (fun () -> BU.print3 "should_unfold: Reached a %s with delta_depth = %s\n >> Our delta_level is %s\n" (Print.fv_to_string fv) - (Print.delta_depth_to_string (Env.delta_depth_of_fv cfg.tcenv fv)) + (show (Env.delta_depth_of_fv cfg.tcenv fv)) (FStar.Common.string_of_list Env.string_of_delta_level cfg.delta_level)); yesno <| (cfg.delta_level |> BU.for_some (function | NoDelta -> false @@ -3267,19 +3269,19 @@ let term_to_doc env t = in FStar.Syntax.Print.Pretty.term_to_doc' (DsEnv.set_current_module env.dsenv env.curmodule) t -let term_to_string env t = +let term_to_string env t = GenSym.with_frozen_gensym (fun () -> let t = try normalize [AllowUnboundUniverses] env t with e -> Errors.log_issue t.pos (Errors.Warning_NormalizationFailure, (BU.format1 "Normalization failed with error %s\n" (BU.message_of_exn e))) ; t in - Print.term_to_string' (DsEnv.set_current_module env.dsenv env.curmodule) t + Print.term_to_string' (DsEnv.set_current_module env.dsenv env.curmodule) t) -let comp_to_string env c = +let comp_to_string env c = GenSym.with_frozen_gensym (fun () -> let c = try norm_comp (config [AllowUnboundUniverses] env) [] c with e -> Errors.log_issue c.pos (Errors.Warning_NormalizationFailure, (BU.format1 "Normalization failed with error %s\n" (BU.message_of_exn e))) ; c in - Print.comp_to_string' (DsEnv.set_current_module env.dsenv env.curmodule) c + Print.comp_to_string' (DsEnv.set_current_module env.dsenv env.curmodule) c) let normalize_refinement steps env t0 = let t = normalize (steps@[Beta]) env t0 in diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst index d2881c7bda4..38ef675b461 100644 --- a/src/typechecker/FStar.TypeChecker.Rel.fst +++ b/src/typechecker/FStar.TypeChecker.Rel.fst @@ -35,9 +35,11 @@ open FStar.Syntax.Subst open FStar.Ident open FStar.TypeChecker.Common open FStar.Syntax +open FStar.Common + open FStar.Class.Deq +open FStar.Class.Show -open FStar.Common module BU = FStar.Compiler.Util //basic util module U = FStar.Syntax.Util module S = FStar.Syntax.Syntax @@ -330,7 +332,7 @@ let term_to_string t = (Print.ctx_uvar_to_string u) (match fst s with | [] -> "" | s -> BU.format1 "@<%s>" (Print.subst_to_string (List.hd s))) (Print.args_to_string args) - | _ -> Print.term_to_string t + | _ -> show t let prob_to_string env prob = match prob with @@ -358,14 +360,14 @@ let prob_to_string' (wl:worklist) (prob:prob) : string = let uvi_to_string env = function | UNIV (u, t) -> let x = if (Options.hide_uvar_nums()) then "?" else UF.univ_uvar_id u |> string_of_int in - BU.format2 "UNIV %s <- %s" x (Print.univ_to_string t) + BU.format2 "UNIV %s <- %s" x (show t) | TERM (u, t) -> let x = if (Options.hide_uvar_nums()) then "?" else UF.uvar_id u.ctx_uvar_head |> string_of_int in BU.format2 "TERM %s <- %s" x (N.term_to_string env t) let uvis_to_string env uvis = FStar.Common.string_of_list (uvi_to_string env) uvis let names_to_string nms = BU.set_elements nms |> List.map Print.bv_to_string |> String.concat ", " -let args_to_string args = args |> List.map (fun (x, _) -> Print.term_to_string x) |> String.concat " " +let args_to_string (args : S.args) = args |> List.map (fun (x, _) -> show x) |> String.concat " " (* ------------------------------------------------*) (* *) @@ -576,12 +578,12 @@ let set_uvar env u (should_check_opt:option S.should_check_uvar) t = // then ( // BU.print2 "Setting uvar %s to %s\n" // (Print.ctx_uvar_to_string u) - // (Print.term_to_string t); + // (show t); // match Unionfind.find u.ctx_uvar_head with // | None -> () // | Some t -> // BU.print2 "Uvar already set to %s\n%s\n" - // (Print.term_to_string t) + // (show t) // (BU.stack_dump()); // failwith "DIE" // ); @@ -705,7 +707,7 @@ let base_and_refinement_maybe_delta should_delta env t1 = else (match norm_refinement env t1 with | {n=Tm_refine {b=x; phi}} -> (x.sort, Some(x, phi)) | tt -> failwith (BU.format2 "impossible: Got %s ... %s\n" - (Print.term_to_string tt) + (show tt) (Print.tag_of_term tt)) ) @@ -736,7 +738,7 @@ let base_and_refinement_maybe_delta should_delta env t1 = | Tm_meta _ | Tm_ascribed _ //NS: Why are the two previous cases excluded? Because of the whnf/unmeta | Tm_delayed _ - | Tm_unknown -> failwith (BU.format2 "impossible (outer): Got %s ... %s\n" (Print.term_to_string t1) (Print.tag_of_term t1)) in + | Tm_unknown -> failwith (BU.format2 "impossible (outer): Got %s ... %s\n" (show t1) (Print.tag_of_term t1)) in aux false (whnf env t1) @@ -900,7 +902,7 @@ let ensure_no_uvar_subst env (t0:term) (wl:worklist) if Env.debug env <| Options.Other "Rel" then BU.print2 "ensure_no_uvar_subst solving %s with %s\n" (Print.ctx_uvar_to_string uv) - (Print.term_to_string sol); + (show sol); set_uvar env uv (Some Already_checked) sol; (* Make a term for the new uvar, applied to the substitutions of @@ -993,7 +995,7 @@ let solve_prob' resolve_ok prob logical_guard uvis wl = then BU.print3 "Solving %s (%s) with formula %s\n" (string_of_int (p_pid prob)) (print_ctx_uvar uv) - (Print.term_to_string phi); + (show phi); let phi = U.abs xs phi (Some (U.residual_tot U.ktype0)) in def_check_scoped (p_loc prob) ("solve_prob'.sol." ^ string_of_int (p_pid prob)) (List.map (fun b -> b.binder_bv) <| p_scope prob) phi; @@ -1003,7 +1005,7 @@ let solve_prob' resolve_ok prob logical_guard uvis wl = let fail () = failwith (BU.format2 "Impossible: this instance %s has already been assigned a solution\n%s\n" (Print.ctx_uvar_to_string uv) - (Print.term_to_string (p_guard prob))) + (show (p_guard prob))) in let args_as_binders args = args |> @@ -1070,7 +1072,7 @@ let occurs_check (uk:ctx_uvar) t = if not occurs then None else Some (BU.format2 "occurs-check failed (%s occurs in %s)" (Print.uvar_to_string uk.ctx_uvar_head) - (Print.term_to_string t)) in + (show t)) in uvars, not occurs, msg let occurs_full (uk:ctx_uvar) t = let uvars = @@ -1223,10 +1225,7 @@ let pat_vars env ctx args : option binders = (* ------------------------------------------------ *) let string_of_match_result = function - | MisMatch (d1, d2) -> - "MisMatch (" - ^ FStar.Common.string_of_option Print.delta_depth_to_string d1 ^ ") (" - ^ FStar.Common.string_of_option Print.delta_depth_to_string d2 ^ ")" + | MisMatch (d1, d2) -> "MisMatch " ^ show (d1, d2) | HeadMatch u -> "HeadMatch " ^ string_of_bool u | FullMatch -> "FullMatch" @@ -1284,7 +1283,7 @@ let rec head_matches env t1 t2 : match_result = let t1 = U.unmeta t1 in let t2 = U.unmeta t2 in if Env.debug env <| Options.Other "RelDelta" then ( - BU.print2 "head_matches %s %s\n" (Print.term_to_string t1) (Print.term_to_string t2); + BU.print2 "head_matches %s %s\n" (show t1) (show t2); BU.print2 " %s -- %s\n" (Print.tag_of_term t1) (Print.tag_of_term t2); () ); @@ -1330,7 +1329,7 @@ let head_matches_delta env smt_ok t1 t2 : (match_result & option (typ&typ)) = let maybe_inline t = let head = U.head_of (unrefine env t) in if Env.debug env <| Options.Other "RelDelta" then - BU.print2 "Head of %s is %s\n" (Print.term_to_string t) (Print.term_to_string head); + BU.print2 "Head of %s is %s\n" (show t) (show head); match (U.un_uinst head).n with | Tm_fvar fv -> begin @@ -1342,7 +1341,7 @@ let head_matches_delta env smt_ok t1 t2 : (match_result & option (typ&typ)) = with | None -> if Env.debug env <| Options.Other "RelDelta" then - BU.print1 "No definition found for %s\n" (Print.term_to_string head); + BU.print1 "No definition found for %s\n" (show head); None | Some _ -> let basic_steps = @@ -1366,8 +1365,8 @@ let head_matches_delta env smt_ok t1 t2 : (match_result & option (typ&typ)) = then None else let _ = if Env.debug env <| Options.Other "RelDelta" then BU.print2 "Inlined %s to %s\n" - (Print.term_to_string t) - (Print.term_to_string t') in + (show t) + (show t') in Some t' end | _ -> None @@ -1391,8 +1390,8 @@ let head_matches_delta env smt_ok t1 t2 : (match_result & option (typ&typ)) = let r = head_matches env t1 t2 in if Env.debug env <| Options.Other "RelDelta" then BU.print3 "head_matches (%s, %s) = %s\n" - (Print.term_to_string t1) - (Print.term_to_string t2) + (show t1) + (show t2) (string_of_match_result r); let reduce_one_and_try_again (d1:delta_depth) (d2:delta_depth) = let d1_greater_than_d2 = Common.delta_depth_greater_than d1 d2 in @@ -1447,17 +1446,17 @@ let head_matches_delta env smt_ok t1 t2 : (match_result & option (typ&typ)) = let r = aux true 0 t1 t2 in if Env.debug env <| Options.Other "RelDelta" then BU.print4 "head_matches_delta (%s, %s) = %s (%s)\n" - (Print.term_to_string t1) - (Print.term_to_string t2) + (show t1) + (show t2) (string_of_match_result (fst r)) (if Option.isNone (snd r) then "None" else snd r |> must |> (fun (t1, t2) -> - Print.term_to_string t1 + show t1 ^ "; " - ^ Print.term_to_string t2)); + ^ show t2)); r let kind_type (binders:binders) (r:Range.range) = @@ -1645,8 +1644,8 @@ let rec really_solve_universe_eq pid_orig wl u1 u2 = aux wl us1 us2 else ufailed_thunk (fun () -> BU.format2 "Unable to unify universes: %s and %s" - (Print.univ_to_string u1) - (Print.univ_to_string u2)) + (show u1) + (show u2)) end | U_max us, u' | u', U_max us -> @@ -1663,16 +1662,16 @@ let rec really_solve_universe_eq pid_orig wl u1 u2 = | _ -> ufailed_thunk (fun () -> BU.format3 "Unable to unify universes: %s and %s (%s)" - (Print.univ_to_string u1) - (Print.univ_to_string u2) msg) in + (show u1) + (show u2) msg) in match u1, u2 with | U_bvar _, _ | U_unknown, _ | _, U_bvar _ | _, U_unknown -> failwith (BU.format2 "Impossible: found an de Bruijn universe variable or unknown universe: %s, %s" - (Print.univ_to_string u1) - (Print.univ_to_string u2)) + (show u1) + (show u2)) | U_name x, U_name y -> if (string_of_id x) = (string_of_id y) @@ -1696,7 +1695,7 @@ let rec really_solve_universe_eq pid_orig wl u1 u2 = let u = norm_univ wl u in if occurs_univ v1 u then try_umax_components u1 u2 - (BU.format2 "Failed occurs check: %s occurs in %s" (Print.univ_to_string (U_unif v1)) (Print.univ_to_string u)) + (BU.format2 "Failed occurs check: %s occurs in %s" (show (U_unif v1)) (show u)) else USolved (extend_universe_solution pid_orig [UNIV(v1, u)] wl) | U_max _, _ @@ -1854,10 +1853,10 @@ let run_meta_arg_tac (ctx_u:ctx_uvar) : term = let simplify_guard env g = match g.guard_f with | Trivial -> g | NonTrivial f -> - if Env.debug env <| Options.Other "Simplification" then BU.print1 "Simplifying guard %s\n" (Print.term_to_string f); + if Env.debug env <| Options.Other "Simplification" then BU.print1 "Simplifying guard %s\n" (show f); let f = norm_with_steps "FStar.TypeChecker.Rel.norm_with_steps.6" [Env.Beta; Env.Eager_unfolding; Env.Simplify; Env.Primops; Env.NoFullNorm; Env.Exclude Env.Zeta] env f in - if Env.debug env <| Options.Other "Simplification" then BU.print1 "Simplified guard to %s\n" (Print.term_to_string f); + if Env.debug env <| Options.Other "Simplification" then BU.print1 "Simplified guard to %s\n" (show f); let f = let g = U.unmeta f in let g = @@ -2054,7 +2053,7 @@ let apply_ad_hoc_indexed_subcomp (env:Env.env) List.fold_left2 (fun (ps, wl) f_sort_i c1_i -> if debug wl <| Options.Other "LayeredEffectsEqns" then BU.print3 "Layered Effects (%s) %s = %s\n" subcomp_name - (Print.term_to_string f_sort_i) (Print.term_to_string c1_i); + (show f_sort_i) (show c1_i); let p, wl = sub_prob wl f_sort_i EQ c1_i "indices of c1" in ps@[p], wl ) ([], wl) f_sort_is (ct1.effect_args |> List.map fst) in @@ -2071,7 +2070,7 @@ let apply_ad_hoc_indexed_subcomp (env:Env.env) List.fold_left2 (fun (ps, wl) g_sort_i c2_i -> if debug wl <| Options.Other "LayeredEffectsEqns" then BU.print3 "Layered Effects (%s) %s = %s\n" subcomp_name - (Print.term_to_string g_sort_i) (Print.term_to_string c2_i); + (show g_sort_i) (show c2_i); let p, wl = sub_prob wl g_sort_i EQ c2_i "indices of c2" in ps@[p], wl ) ([], wl) g_sort_is (ct2.effect_args |> List.map fst) in @@ -2279,7 +2278,7 @@ and solve_rigid_flex_or_flex_rigid_subtyping in let pairwise t1 t2 wl = if debug wl <| Options.Other "Rel" - then BU.print2 "[meet/join]: pairwise: %s and %s\n" (Print.term_to_string t1) (Print.term_to_string t2); + then BU.print2 "[meet/join]: pairwise: %s and %s\n" (show t1) (show t2); let mr, ts = head_matches_delta (p_env wl (TProb tp)) wl.smt_ok t1 t2 in match mr with | HeadMatch true @@ -2393,7 +2392,7 @@ and solve_rigid_flex_or_flex_rigid_subtyping let t1, ps, wl = combine t1 t2 wl in if debug wl <| Options.Other "Rel" then BU.print1 "pairwise fallback2 succeeded: %s" - (Print.term_to_string t1); + (show t1); t1, ps, wl in let rec aux (out, probs, wl) ts = @@ -2623,12 +2622,12 @@ and imitate_arrow (orig:prob) (wl:worklist) let sub_prob, wl = mk_t_problem wl [] orig lhs' rel arrow None "arrow imitation" in - //printfn "Arrow imitation: %s =?= %s" (Print.term_to_string lhs') (Print.term_to_string rhs); + //printfn "Arrow imitation: %s =?= %s" (show lhs') (show rhs); solve (attempt [sub_prob] (solve_prob orig None [sol] wl)) | ({binder_bv=x;binder_qual=imp;binder_positivity=pqual;binder_attrs=attrs})::formals -> let _ctx_u_x, u_x, wl = copy_uvar u_lhs (bs_lhs@bs) (U.type_u() |> fst) wl in - //printfn "Generated formal %s where %s" (Print.term_to_string t_y) (Print.ctx_uvar_to_string ctx_u_x); + //printfn "Generated formal %s where %s" (show t_y) (Print.ctx_uvar_to_string ctx_u_x); let y = S.new_bv (Some (S.range_of_bv x)) u_x in let b = S.mk_binder_with_attrs y imp pqual attrs in aux (bs@[b]) (bs_terms@[U.arg_of_non_null_binder b]) formals wl @@ -2704,7 +2703,7 @@ and solve_binders (bs1:binders) (bs2:binders) (orig:prob) (wl:worklist) U.mk_conj (p_guard prob) (close_forall (p_env wl prob) [{x with binder_bv=hd1}] phi) in if debug wl <| Options.Other "Rel" - then BU.print2 "Formula is %s\n\thd1=%s\n" (Print.term_to_string phi) (Print.bv_to_string hd1); + then BU.print2 "Formula is %s\n\thd1=%s\n" (show phi) (Print.bv_to_string hd1); Inl (prob::sub_probs, phi), wl | fail -> fail @@ -2973,14 +2972,14 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term) // then BU.print4 "imitate_app 1:\n\tlhs=%s\n\tbs_lhs=%s\n\tt_res_lhs=%s\n\trhs=%s\n" // (flex_t_to_string lhs) // (Print.binders_to_string ", " bs_lhs) - // (Print.term_to_string t_res_lhs) - // (Print.term_to_string rhs); + // (show t_res_lhs) + // (show rhs); let rhs_hd, args = U.head_and_args rhs in let args_rhs, last_arg_rhs = BU.prefix args in let rhs' = S.mk_Tm_app rhs_hd args_rhs rhs.pos in // if debug wl <| Options.Other "Rel" // then BU.print2 "imitate_app 2:\n\trhs'=%s\n\tlast_arg_rhs=%s\n" - // (Print.term_to_string rhs') + // (show rhs') // (Print.args_to_string [last_arg_rhs]); let (Flex (t_lhs, u_lhs, _lhs_args)) = lhs in let lhs', lhs'_last_arg, wl = @@ -3002,8 +3001,8 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term) in // if debug wl <| Options.Other "Rel" // then BU.print2 "imitate_app 3:\n\tlhs'=%s\n\tlast_arg_lhs=%s\n" - // (Print.term_to_string lhs') - // (Print.term_to_string lhs'_last_arg); + // (show lhs') + // (show lhs'_last_arg); let sol = [TERM(u_lhs, U.abs bs_lhs (S.mk_Tm_app lhs' [(lhs'_last_arg, snd last_arg_rhs)] t_lhs.pos) (Some (U.residual_tot t_res_lhs)))] in @@ -3088,7 +3087,7 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term) if debug wl <| Options.Other "Rel" then BU.print2 "try_first_order\n\tlhs=%s\n\trhs=%s\n" (flex_t_to_string lhs) - (Print.term_to_string rhs); + (show rhs); let (Flex (_t1, ctx_uv, args_lhs)) = lhs in let n_args_lhs = List.length args_lhs in let head, args_rhs = U.head_and_args rhs in @@ -3151,8 +3150,8 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term) else ( if debug wl (Options.Other "Rel") then BU.print2 "first-order: head type mismatch:\n\tlhs=%s\n\trhs=%s\n" - (Print.term_to_string (U.ctx_uvar_typ ctx_uv)) - (Print.term_to_string t_head); + (show (U.ctx_uvar_typ ctx_uv)) + (show t_head); let typ_equality_prob wl = let p, wl = mk_t_problem wl [] orig (U.ctx_uvar_typ ctx_uv) EQ t_head None "first-order head type" in [p], wl @@ -3200,7 +3199,7 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term) // FV(rhs) \t= %s\n" // (flex_t_to_string lhs) // (names_to_string fvs1) - // (Print.term_to_string rhs) + // (show rhs) // (names_to_string fvs2); let uvars, occurs_ok, msg = occurs_check ctx_uv rhs in if not occurs_ok @@ -3256,7 +3255,7 @@ and solve_t_flex_flex env orig wl (lhs:flex_t) (rhs:flex_t) : solution = if debug wl <| Options.Other "Rel" then BU.print2 "solve_t_flex_flex: solving meta arg uvar %s with %s\n" (Print.ctx_uvar_to_string uv) - (Print.term_to_string t); + (show t); set_uvar env uv None t; solve (attempt [orig] wl) in @@ -3379,8 +3378,8 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = if debug wl <| Options.Other "Rel" then BU.print5 "Heads %s: %s (%s) and %s (%s)\n" (if need_unif then "need unification" else "match") - (Print.term_to_string t1) (Print.tag_of_term t1) - (Print.term_to_string t2) (Print.tag_of_term t2); + (show t1) (Print.tag_of_term t1) + (show t2) (Print.tag_of_term t2); let head1, args1 = U.head_and_args t1 in let head2, args2 = U.head_and_args t2 in let need_unif = @@ -3404,9 +3403,9 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = then giveup wl (mklstr (fun () -> BU.format4 "unequal number of arguments: %s[%s] and %s[%s]" - (Print.term_to_string head1) + (show head1) (args_to_string args1) - (Print.term_to_string head2) + (show head2) (args_to_string args2))) orig else @@ -3487,10 +3486,10 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = if debug wl <| Options.Other "Rel" then BU.print4 "Unfolding didn't make progress ... got %s ~> %s;\nand %s ~> %s\n" - (Print.term_to_string t1) - (Print.term_to_string t1') - (Print.term_to_string t2) - (Print.term_to_string t2'); + (show t1) + (show t1') + (show t2) + (show t2'); solve_sub_probs env wl //fallback to trying to solve with SMT on | _ -> let torig' = {torig with lhs=t1'; rhs=t2'} in @@ -3593,7 +3592,7 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = |> U.unrefine in if debug wl <| Options.Other "Rel" then BU.print1 "Match heuristic, typechecking the pattern term: %s {\n\n" - (Print.term_to_string pat_term); + (show pat_term); let pat_term, pat_term_t, g_pat_term = env.typeof_tot_or_gtot_term (Env.set_expected_typ env scrutinee_t) @@ -3601,8 +3600,8 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = must_tot in if debug wl <| Options.Other "Rel" then BU.print2 "} Match heuristic, typechecked pattern term to %s and type %s\n" - (Print.term_to_string pat_term) - (Print.term_to_string pat_term_t); + (show pat_term) + (show pat_term_t); pat_term, g_pat_term in // @@ -3648,15 +3647,15 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = | Some (t1, t2) -> if debug wl <| Options.Other "Rel" then BU.print2 "Trying match heuristic for %s vs. %s\n" - (Print.term_to_string t1) - (Print.term_to_string t2); + (show t1) + (show t2); match (s1, U.unmeta t1), (s2, U.unmeta t2) with | (_, {n=Tm_match {scrutinee; brs=branches}}), (s, t) | (s, t), (_, {n=Tm_match {scrutinee; brs=branches}}) -> if not (is_flex scrutinee) then begin if debug wl <| Options.Other "Rel" - then BU.print1 "match head %s is not a flex term\n" (Print.term_to_string scrutinee); + then BU.print1 "match head %s is not a flex term\n" (show scrutinee); Inr None end else if wl.defer_ok = DeferAny @@ -3666,8 +3665,8 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = else begin if debug wl <| Options.Other "Rel" then BU.print2 "Heuristic applicable with scrutinee %s and other side = %s\n" - (Print.term_to_string scrutinee) - (Print.term_to_string t); + (show scrutinee) + (show t); let pat_discriminates = function | ({v=Pat_constant _}, None, _) | ({v=Pat_cons _}, None, _) -> true @@ -3706,7 +3705,7 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = if debug wl <| Options.Other "Rel" then BU.print2 "Found head matching branch %s -> %s\n" (Print.pat_to_string p) - (Print.term_to_string e); + (show e); Inr <| try_solve_branch scrutinee p end @@ -3727,8 +3726,8 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = BU.print4 "rigid_rigid_delta of %s-%s (%s, %s)\n" (Print.tag_of_term t1) (Print.tag_of_term t2) - (Print.term_to_string t1) - (Print.term_to_string t2); + (show t1) + (show t2); let m, o = head_matches_delta (p_env wl orig) wl.smt_ok t1 t2 in match m, o with | (MisMatch _, _) -> //heads definitely do not match @@ -3836,14 +3835,14 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = then let guard, wl = guard_of_prob wl problem t1 t2 in solve (solve_prob orig (Some guard) [] wl) else giveup wl (mklstr (fun () -> BU.format4 "head mismatch (%s (%s) vs %s (%s))" - (Print.term_to_string head1) + (show head1) (BU.dflt "" (BU.bind_opt (delta_depth_of_term wl.tcenv head1) - (fun x -> Some (Print.delta_depth_to_string x)))) - (Print.term_to_string head2) + (fun x -> Some (show x)))) + (show head2) (BU.dflt "" (BU.bind_opt (delta_depth_of_term wl.tcenv head2) - (fun x -> Some (Print.delta_depth_to_string x)))) + (fun x -> Some (show x)))) )) orig end @@ -3855,8 +3854,8 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = then let guard, wl = guard_of_prob wl problem t1 t2 in solve (solve_prob orig (Some guard) [] wl) else giveup wl (mklstr (fun () -> BU.format2 "head mismatch for subtyping (%s vs %s)" - (Print.term_to_string t1) - (Print.term_to_string t2))) + (show t1) + (show t2))) orig | (_, Some (t1, t2)) -> //heads match after some delta steps @@ -3881,8 +3880,8 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = let _ = if debug wl (Options.Other "Rel") then BU.print4 "Attempting %s (%s vs %s); rel = (%s)\n" (string_of_int problem.pid) - (Print.tag_of_term t1 ^ "::" ^ Print.term_to_string t1) - (Print.tag_of_term t2 ^ "::" ^ Print.term_to_string t2) + (Print.tag_of_term t1 ^ "::" ^ show t1) + (Print.tag_of_term t2 ^ "::" ^ show t2) (rel_to_string problem.relation) in match t1.n, t2.n with @@ -3969,11 +3968,11 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = let x2, phi2 = as_refinement false env t2 in if debug wl (Options.Other "Rel") then begin BU.print3 "ref1 = (%s):(%s){%s}\n" (Print.bv_to_string x1) - (Print.term_to_string x1.sort) - (Print.term_to_string phi1); + (show x1.sort) + (show phi1); BU.print3 "ref2 = (%s):(%s){%s}\n" (Print.bv_to_string x2) - (Print.term_to_string x2.sort) - (Print.term_to_string phi2) + (show x2.sort) + (show phi2) end; let base_prob, wl = mk_t_problem wl [] orig x1.sort problem.relation x2.sort problem.element "refinement base type" in let x1 = freshen_bv x1 in @@ -4211,10 +4210,10 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = then BU.print ">> (%s) (smtok=%s)\n>>> head1 = %s [interpreted=%s; no_free_uvars=%s]\n>>> head2 = %s [interpreted=%s;no_free_uvars=%s]\n" [(string_of_int problem.pid); (string_of_bool wl.smt_ok); - (Print.term_to_string head1); + (show head1); (string_of_bool (Env.is_interpreted wl.tcenv head1)); (string_of_bool (no_free_uvars t1)); - (Print.term_to_string head2); + (show head2); (string_of_bool (Env.is_interpreted wl.tcenv head2)); (string_of_bool (no_free_uvars t2))] in @@ -4287,7 +4286,7 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = | _, Tm_let _ -> raise_error (Errors.Fatal_UnificationNotWellFormed, BU.format4 "Internal error: unexpected flex-flex of %s and %s\n>>> (%s) -- (%s)" (Print.tag_of_term t1) (Print.tag_of_term t2) - (Print.term_to_string t1) (Print.term_to_string t2)) t1.pos + (show t1) (show t2)) t1.pos | Tm_lazy li1, Tm_lazy li2 when li1.lkind =? li2.lkind && lazy_complete_repr li1.lkind -> @@ -4306,8 +4305,8 @@ and solve_c (problem:problem comp) (wl:worklist) : solution = let solve_eq c1_comp c2_comp g_lift = let _ = if debug wl <| Options.Other "EQ" then BU.print2 "solve_c is using an equality constraint (%s vs %s)\n" - (Print.comp_to_string (mk_Comp c1_comp)) - (Print.comp_to_string (mk_Comp c2_comp)) in + (show (mk_Comp c1_comp)) + (show (mk_Comp c2_comp)) in if not (lid_equals c1_comp.effect_name c2_comp.effect_name) then giveup wl (mklstr (fun () -> BU.format2 "incompatible effects: %s <> %s" (Print.lid_to_string c1_comp.effect_name) @@ -4367,8 +4366,8 @@ and solve_c (problem:problem comp) (wl:worklist) : solution = let solve_layered_sub c1 c2 = if debug wl <| Options.Other "LayeredEffectsApp" then BU.print2 "solve_layered_sub c1: %s and c2: %s {\n" - (c1 |> S.mk_Comp |> Print.comp_to_string) - (c2 |> S.mk_Comp |> Print.comp_to_string); + (c1 |> S.mk_Comp |> show) + (c2 |> S.mk_Comp |> show); if problem.relation = EQ then solve_eq c1 c2 Env.trivial_guard @@ -4439,7 +4438,7 @@ and solve_c (problem:problem comp) (wl:worklist) : solution = BU.format3 "Cannot lift erasable expression from %s ~> %s since its type %s is informative" (string_of_lid c1.effect_name) (string_of_lid c2.effect_name) - (Print.term_to_string c1.result_typ)) r; + (show c1.result_typ)) r; (* * AR: 04/08: Suppose we have a subcomp problem of the form: @@ -4475,7 +4474,7 @@ and solve_c (problem:problem comp) (wl:worklist) : solution = then begin if debug wl <| Options.Other "LayeredEffectsEqns" then BU.print2 "Layered Effects teq (rel c1 index uvar) %s = %s\n" - (Print.term_to_string a1) (Print.term_to_string a2); + (show a1) (show a2); let p, wl = sub_prob wl a1 EQ a2 "l.h.s. effect index uvar" in p::is_sub_probs, wl end @@ -4564,8 +4563,8 @@ and solve_c (problem:problem comp) (wl:worklist) : solution = let prob, wl = sub_prob wl c1_repr problem.relation c2_repr (BU.format2 "sub effect repr: %s <: %s" - (Print.term_to_string c1_repr) - (Print.term_to_string c2_repr)) + (show c1_repr) + (show c2_repr)) in let wl = solve_prob orig (Some (p_guard prob)) [] wl in solve (attempt [prob] wl) @@ -4589,7 +4588,7 @@ and solve_c (problem:problem comp) (wl:worklist) : solution = mk (Tm_app {hd=inst_effect_fun_with [c2_univ] env c2_decl stronger; args=[as_arg c2.result_typ; as_arg wpc2; wpc1_2]}) r in if debug wl <| Options.Other "Rel" then - BU.print1 "WP guard (simplifed) is (%s)\n" (Print.term_to_string (N.normalize [Env.Iota; Env.Eager_unfolding; Env.Primops; Env.Simplify] env g)); + BU.print1 "WP guard (simplifed) is (%s)\n" (show (N.normalize [Env.Iota; Env.Eager_unfolding; Env.Primops; Env.Simplify] env g)); let base_prob, wl = sub_prob wl c1.result_typ problem.relation c2.result_typ "result type" in let wl = solve_prob orig (Some <| U.mk_conj (p_guard base_prob) g) [] wl in solve (attempt [base_prob] wl) @@ -4599,9 +4598,9 @@ and solve_c (problem:problem comp) (wl:worklist) : solution = then solve (solve_prob orig None [] wl) else let _ = if debug wl <| Options.Other "Rel" then BU.print3 "solve_c %s %s %s\n" - (Print.comp_to_string c1) + (show c1) (rel_to_string problem.relation) - (Print.comp_to_string c2) in + (show c2) in //AR: 10/18: try ghost to pure promotion only if effects are different @@ -4671,19 +4670,19 @@ and solve_c (problem:problem comp) (wl:worklist) : solution = (* top-level interface *) (* -------------------------------------------------------- *) let print_pending_implicits g = - g.implicits |> List.map (fun i -> Print.ctx_uvar_to_string i.imp_uvar) |> String.concat ", " + g.implicits |> List.map (fun i -> show i.imp_uvar) |> String.concat ", " -let ineqs_to_string ineqs = +let ineqs_to_string (ineqs : list universe & list (universe & universe)) = let vars = fst ineqs - |> List.map Print.univ_to_string + |> List.map show |> String.concat ", " in let ineqs = snd ineqs |> List.map (fun (u1, u2) -> BU.format2 "%s < %s" - (Print.univ_to_string u1) - (Print.univ_to_string u2)) + (show u1) + (show u2)) |> String.concat ", " in BU.format2 "Solving for {%s}; inequalities are {%s}" vars ineqs @@ -4766,7 +4765,7 @@ let try_teq smt_ok env t1 t2 : option guard_t = Profiling.profile (fun () -> if Env.debug env <| Options.Other "Rel" then - BU.print3 "try_teq of %s and %s in %s {\n" (Print.term_to_string t1) (Print.term_to_string t2) + BU.print3 "try_teq of %s and %s in %s {\n" (show t1) (show t2) (Env.print_gamma env.gamma); let prob, wl = new_t_problem (empty_worklist env) env t1 EQ t2 None (Env.get_range env) in let g = with_guard env prob <| solve_and_commit (singleton wl prob smt_ok) (fun _ -> None) in @@ -4787,8 +4786,8 @@ let teq env t1 t2 : guard_t = | Some g -> if Env.debug env <| Options.Other "Rel" then BU.print3 "teq of %s and %s succeeded with guard %s\n" - (Print.term_to_string t1) - (Print.term_to_string t2) + (show t1) + (show t2) (guard_to_string env g); g @@ -4800,7 +4799,7 @@ let teq env t1 t2 : guard_t = *) let get_teq_predicate env t1 t2 = if Env.debug env <| Options.Other "Rel" then - BU.print2 "get_teq_predicate of %s and %s {\n" (Print.term_to_string t1) (Print.term_to_string t2); + BU.print2 "get_teq_predicate of %s and %s {\n" (show t1) (show t2); let prob, x, wl = new_t_prob (empty_worklist env) env t1 EQ t2 in let g = with_guard env prob <| solve_and_commit (singleton wl prob true) (fun _ -> None) in if Env.debug env <| Options.Other "Rel" then @@ -4817,7 +4816,7 @@ let sub_or_eq_comp env (use_eq:bool) c1 c2 = Profiling.profile (fun () -> let rel = if use_eq then EQ else SUB in if Env.debug env <| Options.Other "Rel" then - BU.print3 "sub_comp of %s --and-- %s --with-- %s\n" (Print.comp_to_string c1) (Print.comp_to_string c2) (if rel = EQ then "EQ" else "SUB"); + BU.print3 "sub_comp of %s --and-- %s --with-- %s\n" (show c1) (show c2) (if rel = EQ then "EQ" else "SUB"); let prob, wl = new_problem (empty_worklist env) env c1 rel c2 None (Env.get_range env) "sub_comp" in let wl = { wl with repr_subcomp_allowed = true } in let prob = CProb prob in @@ -4826,7 +4825,7 @@ let sub_or_eq_comp env (use_eq:bool) c1 c2 = (fun () -> with_guard env prob <| solve_and_commit (singleton wl prob true) (fun _ -> None)) in if Env.debug env <| Options.Other "RelBench" then - BU.print4 "sub_comp of %s --and-- %s --with-- %s --- solved in %s ms\n" (Print.comp_to_string c1) (Print.comp_to_string c2) (if rel = EQ then "EQ" else "SUB") (string_of_int ms); + BU.print4 "sub_comp of %s --and-- %s --with-- %s --- solved in %s ms\n" (show c1) (show c2) (if rel = EQ then "EQ" else "SUB") (string_of_int ms); r) (Some (Ident.string_of_lid (Env.current_module env))) "FStar.TypeChecker.Rel.sub_comp" @@ -4856,8 +4855,8 @@ let solve_universe_inequalities' tx env (variables, ineqs) : unit = let fail u1 u2 = UF.rollback tx; raise_error (Errors.Fatal_IncompatibleUniverse, (BU.format2 "Universe %s and %s are incompatible" - (Print.univ_to_string u1) - (Print.univ_to_string u2))) (Env.get_range env) + (show u1) + (show u2))) (Env.get_range env) in let equiv v v' = match SS.compress_univ v, SS.compress_univ v' with @@ -4885,7 +4884,7 @@ let solve_universe_inequalities' tx env (variables, ineqs) : unit = let _ = let wl = {empty_worklist env with defer_ok=NoDefer} in sols |> List.map (fun (lb, v) -> - // printfn "Setting %s to its lower bound %s" (Print.univ_to_string v) (Print.univ_to_string lb); + // printfn "Setting %s to its lower bound %s" (show v) (show lb); match solve_universe_eq (-1) wl lb v with | USolved wl -> () | _ -> fail lb v) @@ -4909,7 +4908,7 @@ let solve_universe_inequalities' tx env (variables, ineqs) : unit = if check_ineq (u, v) then true else (if Env.debug env <| Options.Other "GenUniverses" - then BU.print2 "%s if debug then Errors.diag (Env.get_range env) - (BU.format1 "Before normalization VC=\n%s\n" (Print.term_to_string vc)); + (BU.format1 "Before normalization VC=\n%s\n" (show vc)); let vc = Profiling.profile (fun () -> N.normalize [Env.Eager_unfolding; Env.Simplify; Env.Primops; Env.Exclude Env.Zeta] env vc) @@ -5054,7 +5053,7 @@ let discharge_guard' use_env_range_msg env (g:guard_t) (use_smt:bool) : option g in if debug then Errors.diag (Env.get_range env) - (BU.format1 "After normalization VC=\n%s\n" (Print.term_to_string vc)); + (BU.format1 "After normalization VC=\n%s\n" (show vc)); def_check_scoped (Env.get_range env) "discharge_guard'" env vc; match check_trivial vc with | Trivial -> Some ret_g @@ -5062,13 +5061,13 @@ let discharge_guard' use_env_range_msg env (g:guard_t) (use_smt:bool) : option g if not use_smt then ( if debug then Errors.diag (Env.get_range env) - (BU.format1 "Cannot solve without SMT : %s\n" (Print.term_to_string vc)); + (BU.format1 "Cannot solve without SMT : %s\n" (show vc)); None ) else let _ = if debug then Errors.diag (Env.get_range env) - (BU.format1 "Checking VC=\n%s\n" (Print.term_to_string vc)); + (BU.format1 "Checking VC=\n%s\n" (show vc)); let vcs = if Options.use_tactics() then begin @@ -5112,11 +5111,11 @@ let discharge_guard' use_env_range_msg env (g:guard_t) (use_smt:bool) : option g if debug then Errors.diag (Env.get_range env) (BU.format2 "Trying to solve:\n> %s\nWith proof_ns:\n %s\n" - (Print.term_to_string goal) + (show goal) (Env.string_of_proof_ns env)); if debug then Errors.diag (Env.get_range env) - (BU.format1 "Before calling solver VC=\n%s\n" (Print.term_to_string goal)); + (BU.format1 "Before calling solver VC=\n%s\n" (show goal)); env.solver.solve use_env_range_msg env goal ) ) @@ -5267,8 +5266,8 @@ let check_implicit_solution_and_discharge_guard env if Env.debug env <| Options.Other "Rel" then BU.print5 "Checking uvar %s resolved to %s at type %s, introduce for %s at %s\n" (Print.uvar_to_string imp_uvar.ctx_uvar_head) - (Print.term_to_string imp_tm) - (Print.term_to_string uvar_ty) + (show imp_tm) + (show uvar_ty) imp_reason (Range.string_of_range imp_range); @@ -5331,8 +5330,8 @@ let check_implicit_solution_and_discharge_guard env (Print.ctx_uvar_to_string imp_uvar) (string_of_bool is_tac) imp_reason - (Print.term_to_string imp_tm) - (Print.term_to_string uvar_ty)) imp_range + (show imp_tm) + (show uvar_ty)) imp_range end) in if (not force_univ_constraints) && @@ -5342,7 +5341,7 @@ let check_implicit_solution_and_discharge_guard env match discharge_guard' (Some (fun () -> BU.format4 "%s (Introduced at %s for %s resolved at %s)" - (Print.term_to_string imp_tm) + (show imp_tm) (Range.string_of_range imp_range) imp_reason (Range.string_of_range imp_tm.pos))) @@ -5442,7 +5441,7 @@ let resolve_implicits' env is_tac is_gen (implicits:Env.implicits) in if Env.debug env <| Options.Other "Rel" then BU.print3 "resolve_implicits' loop, imp_tm = %s and ctx_u = %s, is_tac: %s\n" - (Print.term_to_string tm) + (show tm) (Print.ctx_uvar_to_string ctx_u) (string_of_bool is_tac); if Allow_unresolved? uvar_decoration_should_check @@ -5565,10 +5564,10 @@ let layered_effect_teq env (t1:term) (t2:term) (reason:option string) : guard_t if Env.debug env <| Options.Other "LayeredEffectsEqns" then BU.print3 "Layered Effect (%s) %s = %s\n" (if reason |> is_none then "_" else reason |> must) - (Print.term_to_string t1) (Print.term_to_string t2); + (show t1) (show t2); teq env t1 t2 //AR: teq_nosmt? let universe_inequality (u1:universe) (u2:universe) : guard_t = - //Printf.printf "Universe inequality %s <= %s\n" (Print.univ_to_string u1) (Print.univ_to_string u2); + //Printf.printf "Universe inequality %s <= %s\n" (show u1) (show u2); {trivial_guard with univ_ineqs=([], [u1,u2])} diff --git a/src/typechecker/FStar.TypeChecker.TcEffect.fst b/src/typechecker/FStar.TypeChecker.TcEffect.fst index 15ee92e12b1..87cc80eb143 100644 --- a/src/typechecker/FStar.TypeChecker.TcEffect.fst +++ b/src/typechecker/FStar.TypeChecker.TcEffect.fst @@ -40,6 +40,7 @@ module TcUtil = FStar.TypeChecker.Util module Gen = FStar.TypeChecker.Generalize module BU = FStar.Compiler.Util +open FStar.Class.Show let dmff_cps_and_elaborate env ed = (* This is only an elaboration rule not a typechecking one *) @@ -56,6 +57,7 @@ let dmff_cps_and_elaborate env ed = * (us, t) is the tscheme to check and generalize (us will be [] in the first phase) *) let check_and_gen env (eff_name:string) (comb:string) (n:int) (us, t) : (univ_names * term * typ) = + Errors.with_ctx ("While checking combinator " ^ comb ^ " = " ^ show (us, t)) (fun () -> let us, t = SS.open_univ_vars us t in let t, ty = let t, lc, g = tc_tot_or_gtot_term (Env.push_univ_vars env us) t in @@ -82,6 +84,7 @@ let check_and_gen env (eff_name:string) (comb:string) (n:int) (us, t) : (univ_na eff_name comb (Print.univ_names_to_string us) (Print.univ_names_to_string g_us))) t.pos in g_us, t, ty + ) (* * A small gadget to get a uvar for pure wp with given result type diff --git a/tests/error-messages/Bug3102.fst.expected b/tests/error-messages/Bug3102.fst.expected index 35456e6b3de..e1ed4ffa893 100644 --- a/tests/error-messages/Bug3102.fst.expected +++ b/tests/error-messages/Bug3102.fst.expected @@ -28,7 +28,7 @@ >>] >> Got issues: [ * Error 56 at Bug3102.fst(49,16-51,7): - - Bound variable 'z#1156' would escape in the type of this letbinding + - Bound variable 'z#1155' would escape in the type of this letbinding - Add a type annotation that does not mention it >>]