diff --git a/ocaml/fstar-lib/generated/FStarC_CheckedFiles.ml b/ocaml/fstar-lib/generated/FStarC_CheckedFiles.ml index f233a7b6417..1f4e3c4bf35 100644 --- a/ocaml/fstar-lib/generated/FStarC_CheckedFiles.ml +++ b/ocaml/fstar-lib/generated/FStarC_CheckedFiles.ml @@ -91,15 +91,11 @@ let (uu___0 : tc_result_t FStarC_Class_Show.showable) = | Unknown -> "Unknown" | Invalid s -> let uu___1 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string) s in + FStarC_Class_Show.show FStarC_Class_Show.showable_string s in Prims.strcat "Invalid " uu___1 | Valid s -> let uu___1 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string) s in + FStarC_Class_Show.show FStarC_Class_Show.showable_string s in Prims.strcat "Valid " uu___1) } type cache_t = diff --git a/ocaml/fstar-lib/generated/FStarC_Class_Show.ml b/ocaml/fstar-lib/generated/FStarC_Class_Show.ml index 61bf22f3465..8de949d5b09 100644 --- a/ocaml/fstar-lib/generated/FStarC_Class_Show.ml +++ b/ocaml/fstar-lib/generated/FStarC_Class_Show.ml @@ -5,8 +5,12 @@ let __proj__Mkshowable__item__show : 'a . 'a showable -> 'a -> Prims.string = fun projectee -> match projectee with | { show;_} -> show let show : 'a . 'a showable -> 'a -> Prims.string = fun projectee -> match projectee with | { show = show1;_} -> show1 -let printableshow : 'a . 'a FStar_Class_Printable.printable -> 'a showable = - fun uu___ -> { show = (FStar_Class_Printable.to_string uu___) } +let (showable_unit : unit showable) = { show = (fun uu___ -> "()") } +let (showable_bool : Prims.bool showable) = { show = Prims.string_of_bool } +let (showable_nat : Prims.nat showable) = { show = Prims.string_of_int } +let (showable_int : Prims.int showable) = { show = Prims.string_of_int } +let (showable_string : Prims.string showable) = + { show = (fun x -> Prims.strcat "\"" (Prims.strcat x "\"")) } let show_list : 'a . 'a showable -> 'a Prims.list showable = fun uu___ -> { show = ((FStarC_Common.string_of_list ()) (show uu___)) } let show_option : diff --git a/ocaml/fstar-lib/generated/FStarC_Compiler_MachineInts.ml b/ocaml/fstar-lib/generated/FStarC_Compiler_MachineInts.ml index 59e3087d9e3..0db9159bfce 100644 --- a/ocaml/fstar-lib/generated/FStarC_Compiler_MachineInts.ml +++ b/ocaml/fstar-lib/generated/FStarC_Compiler_MachineInts.ml @@ -160,9 +160,8 @@ let (showable_bounded_k : let uu___1 = let uu___2 = let uu___3 = FStarC_BigInt.to_int_fs x in - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) uu___3 in + FStarC_Class_Show.show FStarC_Class_Show.showable_int + uu___3 in let uu___3 = let uu___4 = module_name_for k in Prims.strcat "@@" uu___4 in Prims.strcat uu___2 uu___3 in diff --git a/ocaml/fstar-lib/generated/FStarC_Compiler_Plugins.ml b/ocaml/fstar-lib/generated/FStarC_Compiler_Plugins.ml index 0eecbcebf3c..36e502db0f3 100644 --- a/ocaml/fstar-lib/generated/FStarC_Compiler_Plugins.ml +++ b/ocaml/fstar-lib/generated/FStarC_Compiler_Plugins.ml @@ -54,8 +54,7 @@ let (dynlink : Prims.string -> unit) = FStarC_Errors.errno FStarC_Errors_Codes.Error_PluginDynlink in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) uu___14 in + FStarC_Class_Show.showable_int uu___14 in FStarC_Compiler_Util.format1 "Remove the `--load` option or use `--warn_error -%s` to ignore and continue." uu___13 in @@ -135,9 +134,7 @@ let (compile_modules : Prims.string -> Prims.string Prims.list -> unit) = let uu___3 = let uu___4 = let uu___5 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) rc in + FStarC_Class_Show.show FStarC_Class_Show.showable_int rc in FStarC_Compiler_Util.format2 "Command\n`%s`\nreturned with exit code %s" cmd uu___5 in FStarC_Errors_Msg.text uu___4 in diff --git a/ocaml/fstar-lib/generated/FStarC_Extraction_Krml.ml b/ocaml/fstar-lib/generated/FStarC_Extraction_Krml.ml index 4c70aedc2ac..55f14b8bbc7 100644 --- a/ocaml/fstar-lib/generated/FStarC_Extraction_Krml.ml +++ b/ocaml/fstar-lib/generated/FStarC_Extraction_Krml.ml @@ -706,10 +706,8 @@ let rec (typ_to_doc : typ -> FStarC_Pprint.document) = FStarC_Class_Show.show (FStarC_Class_Show.show_tuple2 (FStarC_Class_Show.show_list - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string)) - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string)) x in + FStarC_Class_Show.showable_string) + FStarC_Class_Show.showable_string) x in FStarC_Pprint.doc_of_string uu___2 in [uu___1] in ctor "TQualified" uu___ @@ -733,10 +731,8 @@ let rec (typ_to_doc : typ -> FStarC_Pprint.document) = FStarC_Class_Show.show (FStarC_Class_Show.show_tuple2 (FStarC_Class_Show.show_list - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string)) - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string)) x in + FStarC_Class_Show.showable_string) + FStarC_Class_Show.showable_string) x in FStarC_Pprint.doc_of_string uu___2 in let uu___2 = let uu___3 = pp_list' typ_to_doc xs in [uu___3] in uu___1 :: uu___2 in diff --git a/ocaml/fstar-lib/generated/FStarC_Extraction_ML_RemoveUnusedParameters.ml b/ocaml/fstar-lib/generated/FStarC_Extraction_ML_RemoveUnusedParameters.ml index bcda2b53f14..51a9ce9e6c6 100644 --- a/ocaml/fstar-lib/generated/FStarC_Extraction_ML_RemoveUnusedParameters.ml +++ b/ocaml/fstar-lib/generated/FStarC_Extraction_ML_RemoveUnusedParameters.ml @@ -396,14 +396,10 @@ let (elim_tydef : ((let uu___7 = let uu___8 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) - i in + FStarC_Class_Show.showable_int i in let uu___9 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) - i in + FStarC_Class_Show.showable_int i in FStarC_Compiler_Util.format3 "Parameter %s of %s is unused and must be eliminated for F#; add `[@@ remove_unused_type_parameters [%s; ...]]` to the interface signature; \nThis type definition is being dropped" uu___8 name uu___9 in diff --git a/ocaml/fstar-lib/generated/FStarC_Main.ml b/ocaml/fstar-lib/generated/FStarC_Main.ml index 834232e780e..fdb11effc24 100644 --- a/ocaml/fstar-lib/generated/FStarC_Main.ml +++ b/ocaml/fstar-lib/generated/FStarC_Main.ml @@ -287,9 +287,8 @@ let (go_normal : unit -> unit) = (Obj.magic uu___4) | FStar_Pervasives_Native.Some (version, files) -> ((let uu___5 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) version in + FStarC_Class_Show.show FStarC_Class_Show.showable_int + version in FStarC_Compiler_Util.print1 "Karamel format version: %s\n" uu___5); FStarC_Compiler_List.iter @@ -365,9 +364,7 @@ let (go_normal : unit -> unit) = let uu___10 = FStarC_Find.include_path () in FStarC_Class_Show.show (FStarC_Class_Show.show_list - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string)) - uu___10 in + FStarC_Class_Show.showable_string) uu___10 in FStarC_Compiler_Util.print1 "- Full include path: %s\n" uu___9); FStarC_Compiler_Util.print_string "\n") diff --git a/ocaml/fstar-lib/generated/FStarC_Options.ml b/ocaml/fstar-lib/generated/FStarC_Options.ml index 2ee31ae438b..e067383b3ec 100644 --- a/ocaml/fstar-lib/generated/FStarC_Options.ml +++ b/ocaml/fstar-lib/generated/FStarC_Options.ml @@ -437,28 +437,18 @@ let rec (option_val_to_string : option_val -> Prims.string) = fun v -> match v with | Bool b -> - let uu___ = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) b in + let uu___ = FStarC_Class_Show.show FStarC_Class_Show.showable_bool b in FStarC_Compiler_String.op_Hat "Bool " uu___ | String s -> let uu___ = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string) s in + FStarC_Class_Show.show FStarC_Class_Show.showable_string s in FStarC_Compiler_String.op_Hat "String " uu___ | Path s -> let uu___ = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string) s in + FStarC_Class_Show.show FStarC_Class_Show.showable_string s in FStarC_Compiler_String.op_Hat "Path " uu___ | Int i -> - let uu___ = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) i in + let uu___ = FStarC_Class_Show.show FStarC_Class_Show.showable_int i in FStarC_Compiler_String.op_Hat "Int " uu___ | List vs -> let uu___ = (FStarC_Common.string_of_list ()) option_val_to_string vs in @@ -539,14 +529,8 @@ let (show_options : unit -> Prims.string) = | String s1 -> let uu___1 = FStarC_Compiler_String.op_Hat s1 "\"" in FStarC_Compiler_String.op_Hat "\"" uu___1 - | Bool b -> - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) b - | Int i -> - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) i + | Bool b -> FStarC_Class_Show.show FStarC_Class_Show.showable_bool b + | Int i -> FStarC_Class_Show.show FStarC_Class_Show.showable_int i | Path s1 -> s1 | List s1 -> let uu___1 = FStarC_Compiler_List.map show_optionval s1 in diff --git a/ocaml/fstar-lib/generated/FStarC_Parser_Dep.ml b/ocaml/fstar-lib/generated/FStarC_Parser_Dep.ml index 2ef5c7d92c6..391006d4195 100644 --- a/ocaml/fstar-lib/generated/FStarC_Parser_Dep.ml +++ b/ocaml/fstar-lib/generated/FStarC_Parser_Dep.ml @@ -2899,9 +2899,7 @@ let (do_print : "# This .depend was generated by F* %s\n" uu___2); (let uu___3 = let uu___4 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string) + FStarC_Class_Show.show FStarC_Class_Show.showable_string FStarC_Compiler_Util.exec_name in [uu___4] in FStarC_Compiler_Util.fprint outc "# Executable: %s\n" uu___3); @@ -2915,9 +2913,8 @@ let (do_print : let uu___7 = let uu___8 = FStarC_Compiler_Util.getcwd () in FStarC_Compiler_Util.normalize_file_path uu___8 in - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string) uu___7 in + FStarC_Class_Show.show FStarC_Class_Show.showable_string + uu___7 in [uu___6] in FStarC_Compiler_Util.fprint outc "# Running in directory %s\n" uu___5); @@ -2926,8 +2923,7 @@ let (do_print : let uu___8 = FStarC_Compiler_Util.get_cmd_args () in FStarC_Class_Show.show (FStarC_Class_Show.show_list - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string)) uu___8 in + FStarC_Class_Show.showable_string) uu___8 in [uu___7] in FStarC_Compiler_Util.fprint outc "# Command line arguments: \"%s\"\n" uu___6); diff --git a/ocaml/fstar-lib/generated/FStarC_Reflection_V1_Builtins.ml b/ocaml/fstar-lib/generated/FStarC_Reflection_V1_Builtins.ml index 34b99258b53..3b560474794 100644 --- a/ocaml/fstar-lib/generated/FStarC_Reflection_V1_Builtins.ml +++ b/ocaml/fstar-lib/generated/FStarC_Reflection_V1_Builtins.ml @@ -1194,9 +1194,7 @@ let (inspect_bv : FStarC_Class_Show.show FStarC_Syntax_Print.showable_term bv.FStarC_Syntax_Syntax.sort in let uu___4 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int bv.FStarC_Syntax_Syntax.index in FStarC_Compiler_Util.format3 "inspect_bv: index is negative (%s : %s), index = %s" uu___2 @@ -1226,9 +1224,7 @@ let (pack_bv : FStarC_Reflection_V1_Data.bv_view -> FStarC_Syntax_Syntax.bv) let uu___3 = let uu___4 = FStarC_BigInt.to_int_fs bvv.FStarC_Reflection_V1_Data.bv_index in - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) uu___4 in + FStarC_Class_Show.show FStarC_Class_Show.showable_int uu___4 in FStarC_Compiler_Util.format2 "pack_bv: index is negative (%s), index = %s" (FStarC_Compiler_Sealed.unseal diff --git a/ocaml/fstar-lib/generated/FStarC_Reflection_V2_Builtins.ml b/ocaml/fstar-lib/generated/FStarC_Reflection_V2_Builtins.ml index 8b319c89e2b..5c880154fc7 100644 --- a/ocaml/fstar-lib/generated/FStarC_Reflection_V2_Builtins.ml +++ b/ocaml/fstar-lib/generated/FStarC_Reflection_V2_Builtins.ml @@ -1091,9 +1091,7 @@ let (pack_namedv : let uu___3 = let uu___4 = FStarC_BigInt.to_int_fs vv.FStarC_Reflection_V2_Data.uniq in - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) uu___4 in + FStarC_Class_Show.show FStarC_Class_Show.showable_int uu___4 in FStarC_Compiler_Util.format2 "pack_namedv: uniq is negative (%s), uniq = %s" (FStarC_Compiler_Sealed.unseal vv.FStarC_Reflection_V2_Data.ppname) @@ -1154,9 +1152,7 @@ let (pack_bv : FStarC_Reflection_V2_Data.bv_view -> FStarC_Syntax_Syntax.bv) let uu___3 = let uu___4 = FStarC_BigInt.to_int_fs bvv.FStarC_Reflection_V2_Data.index in - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) uu___4 in + FStarC_Class_Show.show FStarC_Class_Show.showable_int uu___4 in FStarC_Compiler_Util.format2 "pack_bv: index is negative (%s), index = %s" (FStarC_Compiler_Sealed.unseal diff --git a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_EncodeTerm.ml b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_EncodeTerm.ml index 3a344effbc2..1107daa68ae 100644 --- a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_EncodeTerm.ml +++ b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_EncodeTerm.ml @@ -258,13 +258,9 @@ let raise_arity_mismatch : fun rng -> let uu___ = let uu___1 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) arity in + FStarC_Class_Show.show FStarC_Class_Show.showable_int arity in let uu___2 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) n_args in + FStarC_Class_Show.show FStarC_Class_Show.showable_int n_args in FStarC_Compiler_Util.format3 "Head symbol %s expects at least %s arguments; got only %s" head uu___1 uu___2 in diff --git a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Pruning.ml b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Pruning.ml index 0d03d2ef94b..e944bc5ac95 100644 --- a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Pruning.ml +++ b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Pruning.ml @@ -89,8 +89,7 @@ let (print_pruning_state : pruning_state -> Prims.string) = FStarC_Class_Show.show (FStarC_Class_Show.show_list (FStarC_Compiler_RBSet.showable_rbset - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string))) v in + FStarC_Class_Show.showable_string)) v in FStarC_Compiler_Util.format2 "[%s -> %s]" k uu___1 in uu___ :: acc) [] in let macros = @@ -102,19 +101,15 @@ let (print_pruning_state : pruning_state -> Prims.string) = let uu___1 = FStarC_Class_Show.show (FStarC_Class_Show.show_list - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string)) v in + FStarC_Class_Show.showable_string) v in FStarC_Compiler_Util.format2 "[%s -> %s]" k uu___1 in uu___ :: acc) [] in let uu___ = let uu___1 = FStarC_Compiler_List.map (FStarC_Class_Show.show - (FStarC_Class_Show.show_tuple2 - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string) - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int))) t_to_a1 in + (FStarC_Class_Show.show_tuple2 FStarC_Class_Show.showable_string + FStarC_Class_Show.showable_int)) t_to_a1 in FStarC_Compiler_String.concat "\n\t" uu___1 in FStarC_Compiler_Util.format3 "Pruning state:\n\tTriggers to assumptions:\n\t%s\nAssumptions to triggers:\n\t%s\nMacros:\n\t%s\n" diff --git a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Solver.ml b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Solver.ml index 2349abf0042..a0028b9eefb 100644 --- a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Solver.ml +++ b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Solver.ml @@ -165,17 +165,11 @@ let (__proj__Mkerrors__item__error_messages : let (error_to_short_string : errors -> Prims.string) = fun err -> let uu___ = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow FStar_Class_Printable.printable_int) - err.error_rlimit in + FStarC_Class_Show.show FStarC_Class_Show.showable_int err.error_rlimit in let uu___1 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow FStar_Class_Printable.printable_int) - err.error_fuel in + FStarC_Class_Show.show FStarC_Class_Show.showable_int err.error_fuel in let uu___2 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow FStar_Class_Printable.printable_int) - err.error_ifuel in + FStarC_Class_Show.show FStarC_Class_Show.showable_int err.error_ifuel in FStarC_Compiler_Util.format5 "%s (rlimit=%s; fuel=%s; ifuel=%s%s)" err.error_reason uu___ uu___1 uu___2 (if FStarC_Compiler_Option.isSome err.error_hint @@ -187,17 +181,14 @@ let (error_to_is_timeout : errors -> Prims.string Prims.list) = then let uu___ = let uu___1 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) err.error_rlimit in + FStarC_Class_Show.show FStarC_Class_Show.showable_int + err.error_rlimit in let uu___2 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) err.error_fuel in + FStarC_Class_Show.show FStarC_Class_Show.showable_int + err.error_fuel in let uu___3 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) err.error_ifuel in + FStarC_Class_Show.show FStarC_Class_Show.showable_int + err.error_ifuel in FStarC_Compiler_Util.format5 "timeout (rlimit=%s; fuel=%s; ifuel=%s; %s)" err.error_reason uu___1 uu___2 uu___3 @@ -967,34 +958,29 @@ let (query_info : query_settings -> FStarC_SMTEncoding_Z3.z3result -> unit) = let uu___6 = let uu___7 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.showable_int settings.query_index in let uu___8 = let uu___9 = let uu___10 = let uu___11 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.showable_int z3result.FStarC_SMTEncoding_Z3.z3result_time in let uu___12 = let uu___13 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.showable_int settings.query_fuel in let uu___14 = let uu___15 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.showable_int settings.query_ifuel in let uu___16 = let uu___17 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.showable_int settings.query_rlimit in [uu___17] in uu___15 :: uu___16 in @@ -1231,25 +1217,16 @@ let (uu___0 : answer FStarC_Class_Show.showable) = FStarC_Class_Show.show = (fun ans -> let uu___ = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) ans.ok in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool ans.ok in let uu___1 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) ans.nsuccess in + FStarC_Class_Show.show FStarC_Class_Show.showable_int ans.nsuccess in let uu___2 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) ans.lo in + FStarC_Class_Show.show FStarC_Class_Show.showable_int ans.lo in let uu___3 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) ans.hi in + FStarC_Class_Show.show FStarC_Class_Show.showable_int ans.hi in let uu___4 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) ans.tried_recovery in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + ans.tried_recovery in FStarC_Compiler_Util.format5 "ok=%s nsuccess=%s lo=%s hi=%s tried_recovery=%s" uu___ uu___1 uu___2 uu___3 uu___4) @@ -1800,9 +1777,7 @@ let (maybe_save_failing_query : FStarC_Compiler_Effect.op_Bang failing_query_ctr in let file_name = let uu___2 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) n in + FStarC_Class_Show.show FStarC_Class_Show.showable_int n in FStarC_Compiler_Util.format2 "failedQueries-%s-%s.smt2" mod1 uu___2 in let query_str = diff --git a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_SolverState.ml b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_SolverState.ml index 94f51c44fee..f05966fe2d5 100644 --- a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_SolverState.ml +++ b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_SolverState.ml @@ -125,31 +125,23 @@ let (solver_state_to_string : solver_state -> Prims.string) = FStarC_Compiler_List.map (fun level -> let uu___ = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.show FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length level.all_decls_at_level_rev) in let uu___1 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.show FStarC_Class_Show.showable_bool level.given_some_decls in let uu___2 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.show FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length level.to_flush_rev) in FStarC_Compiler_Util.format3 "Level { all_decls=%s; given_decls=%s; to_flush=%s }" uu___ uu___1 uu___2) s.levels in let uu___ = FStarC_Class_Show.show - (FStarC_Class_Show.show_list - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string)) levels in + (FStarC_Class_Show.show_list FStarC_Class_Show.showable_string) + levels in let uu___1 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow FStar_Class_Printable.printable_nat) + FStarC_Class_Show.show FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length s.pending_flushes_rev) in FStarC_Compiler_Util.format2 "Solver state { levels=%s; pending_flushes=%s }" uu___ uu___1 diff --git a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Term.ml b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Term.ml index 1e87378220b..4922281c0b8 100644 --- a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Term.ml +++ b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Term.ml @@ -2079,15 +2079,11 @@ let rec (declToSmt' : Prims.bool -> Prims.string -> decl -> Prims.string) = "(echo \"\")\n(get-unsat-core)\n(echo \"\")" | Push n -> let uu___ = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) n in + FStarC_Class_Show.show FStarC_Class_Show.showable_int n in FStarC_Compiler_Util.format1 "(push) ;; push{%s" uu___ | Pop n -> let uu___ = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) n in + FStarC_Class_Show.show FStarC_Class_Show.showable_int n in FStarC_Compiler_Util.format1 "(pop) ;; %s}pop" uu___ | SetOption (s, v) -> FStarC_Compiler_Util.format2 "(set-option :%s %s)" s v @@ -2532,16 +2528,10 @@ let (decl_to_string_short : decl -> Prims.string) = | Echo s -> Prims.strcat "Echo " s | RetainAssumptions uu___ -> "RetainAssumptions" | Push n -> - let uu___ = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) n in + let uu___ = FStarC_Class_Show.show FStarC_Class_Show.showable_int n in FStarC_Compiler_Util.format1 "push %s" uu___ | Pop n -> - let uu___ = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) n in + let uu___ = FStarC_Class_Show.show FStarC_Class_Show.showable_int n in FStarC_Compiler_Util.format1 "pop %s" uu___ | CheckSat -> "check-sat" | GetUnsatCore -> "get-unsat-core" diff --git a/ocaml/fstar-lib/generated/FStarC_Syntax_Compress.ml b/ocaml/fstar-lib/generated/FStarC_Syntax_Compress.ml index 9decadf3e94..d85455c9eda 100644 --- a/ocaml/fstar-lib/generated/FStarC_Syntax_Compress.ml +++ b/ocaml/fstar-lib/generated/FStarC_Syntax_Compress.ml @@ -105,9 +105,7 @@ let (compress1_u : let uu___ = let uu___1 = let uu___2 = FStarC_Syntax_Unionfind.univ_uvar_id uv in - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) uu___2 in + FStarC_Class_Show.show FStarC_Class_Show.showable_int uu___2 in FStarC_Compiler_Util.format1 "Internal error: unexpected unresolved (universe) uvar in deep_compress: %s" uu___1 in diff --git a/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml b/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml index 7f98c148920..f78b51f4af0 100644 --- a/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml +++ b/ocaml/fstar-lib/generated/FStarC_Syntax_DsEnv.ml @@ -3113,8 +3113,7 @@ let elab_restriction : | nth2 -> let uu___5 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.showable_int (nth2 + Prims.int_one) in Prims.strcat uu___5 "th" in let uu___5 = @@ -3149,8 +3148,7 @@ let elab_restriction : let uu___4 = let uu___5 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.showable_int ((FStarC_Compiler_List.length others) + Prims.int_one) in Prims.strcat uu___5 " times" in diff --git a/ocaml/fstar-lib/generated/FStarC_Syntax_Print.ml b/ocaml/fstar-lib/generated/FStarC_Syntax_Print.ml index 98e9df4edab..c8c141e0e71 100644 --- a/ocaml/fstar-lib/generated/FStarC_Syntax_Print.ml +++ b/ocaml/fstar-lib/generated/FStarC_Syntax_Print.ml @@ -21,9 +21,7 @@ let (bv_to_string : FStarC_Syntax_Syntax.bv -> Prims.string) = bv.FStarC_Syntax_Syntax.ppname in let uu___2 = let uu___3 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int bv.FStarC_Syntax_Syntax.index in Prims.strcat "#" uu___3 in Prims.strcat uu___1 uu___2 diff --git a/ocaml/fstar-lib/generated/FStarC_Syntax_Util.ml b/ocaml/fstar-lib/generated/FStarC_Syntax_Util.ml index eb723624819..50679025adf 100644 --- a/ocaml/fstar-lib/generated/FStarC_Syntax_Util.ml +++ b/ocaml/fstar-lib/generated/FStarC_Syntax_Util.ml @@ -322,9 +322,7 @@ let rec (univ_kernel : let uu___1 = let uu___2 = let uu___3 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) i in + FStarC_Class_Show.show FStarC_Class_Show.showable_int i in Prims.strcat uu___3 ")" in Prims.strcat "Imposible: univ_kernel (U_bvar " uu___2 in failwith uu___1 diff --git a/ocaml/fstar-lib/generated/FStarC_Tactics_Hooks.ml b/ocaml/fstar-lib/generated/FStarC_Tactics_Hooks.ml index 372fc7ed26f..266149b4852 100644 --- a/ocaml/fstar-lib/generated/FStarC_Tactics_Hooks.ml +++ b/ocaml/fstar-lib/generated/FStarC_Tactics_Hooks.ml @@ -640,9 +640,7 @@ let (preprocess : then let uu___7 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) - n in + FStarC_Class_Show.showable_int n in let uu___8 = let uu___9 = FStarC_Tactics_Types.goal_type g in @@ -1536,8 +1534,7 @@ let (spinoff_strictly_positive_goals : let uu___7 = let uu___8 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length gs3) in FStarC_Compiler_Util.format1 "Split query into %s sub-goals" uu___8 in @@ -1629,9 +1626,7 @@ let (solve_implicits : if uu___3 then let uu___4 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.show FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length gs) in FStarC_Compiler_Util.print1 "solve_implicits produced %s goals\n" uu___4 @@ -1866,8 +1861,7 @@ let (splice : let uu___10 = let uu___11 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length uvs) in FStarC_Compiler_Util.format1 diff --git a/ocaml/fstar-lib/generated/FStarC_Tactics_Interpreter.ml b/ocaml/fstar-lib/generated/FStarC_Tactics_Interpreter.ml index 825d2f296f3..ccfb59906b9 100644 --- a/ocaml/fstar-lib/generated/FStarC_Tactics_Interpreter.ml +++ b/ocaml/fstar-lib/generated/FStarC_Tactics_Interpreter.ml @@ -1051,8 +1051,7 @@ let run_unembedded_tactic_on_ps : then let uu___8 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length ps3.FStarC_Tactics_Types.all_implicits) in let uu___9 = @@ -1073,8 +1072,7 @@ let run_unembedded_tactic_on_ps : then let uu___9 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length ps3.FStarC_Tactics_Types.all_implicits) in let uu___10 = @@ -1177,8 +1175,7 @@ let run_tactic_on_ps' : FStarC_Syntax_Print.showable_term tactic in let uu___3 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool tactic_already_typed in FStarC_Compiler_Util.print2 "Typechecking tactic: (%s) (already_typed: %s) {\n" diff --git a/ocaml/fstar-lib/generated/FStarC_Tactics_Monad.ml b/ocaml/fstar-lib/generated/FStarC_Tactics_Monad.ml index dd8ac2f21c6..a9f18c8829c 100644 --- a/ocaml/fstar-lib/generated/FStarC_Tactics_Monad.ml +++ b/ocaml/fstar-lib/generated/FStarC_Tactics_Monad.ml @@ -169,9 +169,7 @@ let (register_goal : FStarC_Tactics_Types.goal -> unit) = if uu___7 then let uu___8 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) i in + FStarC_Class_Show.show FStarC_Class_Show.showable_int i in FStarC_Compiler_Util.print1 "(%s) Registering goal\n" uu___8 else ()); (let should_register = is_goal_safe_as_well_typed g in @@ -183,9 +181,7 @@ let (register_goal : FStarC_Tactics_Types.goal -> unit) = (if uu___8 then let uu___9 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) i in + FStarC_Class_Show.show FStarC_Class_Show.showable_int i in FStarC_Compiler_Util.print1 "(%s) Not registering goal since it has unresolved uvar deps\n" uu___9 @@ -197,9 +193,7 @@ let (register_goal : FStarC_Tactics_Types.goal -> unit) = if uu___9 then let uu___10 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) i in + FStarC_Class_Show.show FStarC_Class_Show.showable_int i in let uu___11 = FStarC_Class_Show.show FStarC_Syntax_Print.showable_ctxu uv in diff --git a/ocaml/fstar-lib/generated/FStarC_Tactics_Printing.ml b/ocaml/fstar-lib/generated/FStarC_Tactics_Printing.ml index 07485268460..27a02733fc5 100644 --- a/ocaml/fstar-lib/generated/FStarC_Tactics_Printing.ml +++ b/ocaml/fstar-lib/generated/FStarC_Tactics_Printing.ml @@ -39,9 +39,7 @@ let (unshadow : let t1 = let uu___ = let uu___1 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) i in + FStarC_Class_Show.show FStarC_Class_Show.showable_int i in Prims.strcat "'" uu___1 in Prims.strcat b uu___ in let uu___ = f t1 in if uu___ then t1 else aux (i + Prims.int_one) in @@ -115,13 +113,9 @@ let (goal_to_string : | FStar_Pervasives_Native.None -> "" | FStar_Pervasives_Native.Some (i, n) -> let uu___ = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) i in + FStarC_Class_Show.show FStarC_Class_Show.showable_int i in let uu___1 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) n in + FStarC_Class_Show.show FStarC_Class_Show.showable_int n in FStarC_Compiler_Util.format2 " %s/%s" uu___ uu___1 in let maybe_label = match g.FStarC_Tactics_Types.label with @@ -214,9 +208,7 @@ let (ps_to_string : let uu___2 = let uu___3 = let uu___4 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int ps.FStarC_Tactics_Types.depth in FStarC_Compiler_Util.format2 "State dump @ depth %s (%s):\n" uu___4 msg in diff --git a/ocaml/fstar-lib/generated/FStarC_Tactics_V1_Basic.ml b/ocaml/fstar-lib/generated/FStarC_Tactics_V1_Basic.ml index 39878e68e2d..6faaf0fb771 100644 --- a/ocaml/fstar-lib/generated/FStarC_Tactics_V1_Basic.ml +++ b/ocaml/fstar-lib/generated/FStarC_Tactics_V1_Basic.ml @@ -3474,17 +3474,13 @@ let (t_apply : FStarC_Tactics_Monad.if_verbose (fun uu___2 -> let uu___3 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) uopt in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + uopt in let uu___4 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) only_match in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + only_match in let uu___5 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.show FStarC_Class_Show.showable_bool tc_resolved_uvars1 in let uu___6 = FStarC_Class_Show.show FStarC_Syntax_Print.showable_term @@ -5146,9 +5142,8 @@ let (clear : FStarC_Syntax_Syntax.binder -> unit FStarC_Tactics_Monad.tac) = let uu___6 = FStarC_Tactics_Types.goal_env goal in FStarC_TypeChecker_Env.all_binders uu___6 in FStarC_Compiler_List.length uu___5 in - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) uu___4 in + FStarC_Class_Show.show FStarC_Class_Show.showable_nat + uu___4 in FStarC_Compiler_Util.print2 "Clear of (%s), env has %s binders\n" uu___2 uu___3) in Obj.magic diff --git a/ocaml/fstar-lib/generated/FStarC_Tactics_V2_Basic.ml b/ocaml/fstar-lib/generated/FStarC_Tactics_V2_Basic.ml index 1529f4cb115..851089a67b4 100644 --- a/ocaml/fstar-lib/generated/FStarC_Tactics_V2_Basic.ml +++ b/ocaml/fstar-lib/generated/FStarC_Tactics_V2_Basic.ml @@ -1863,9 +1863,7 @@ let meas : match uu___ with | (r, ms) -> ((let uu___2 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) ms in + FStarC_Class_Show.show FStarC_Class_Show.showable_int ms in FStarC_Compiler_Util.print2 "++ Tactic %s ran in \t\t%sms\n" s uu___2); r)) @@ -2718,9 +2716,7 @@ let (binding_to_string : FStarC_Reflection_V2_Data.binding -> Prims.string) = let uu___1 = let uu___2 = FStarC_BigInt.to_int_fs b.FStarC_Reflection_V2_Data.uniq1 in - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) uu___2 in + FStarC_Class_Show.show FStarC_Class_Show.showable_int uu___2 in Prims.strcat "#" uu___1 in Prims.strcat (FStarC_Compiler_Sealed.unseal b.FStarC_Reflection_V2_Data.ppname3) @@ -4123,17 +4119,13 @@ let (t_apply : FStarC_Tactics_Monad.if_verbose (fun uu___2 -> let uu___3 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) uopt in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + uopt in let uu___4 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) only_match in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + only_match in let uu___5 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.show FStarC_Class_Show.showable_bool tc_resolved_uvars1 in let uu___6 = FStarC_Class_Show.show FStarC_Syntax_Print.showable_term @@ -6297,9 +6289,8 @@ let (clear : let uu___6 = FStarC_Tactics_Types.goal_env goal in FStarC_TypeChecker_Env.all_binders uu___6 in FStarC_Compiler_List.length uu___5 in - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) uu___4 in + FStarC_Class_Show.show FStarC_Class_Show.showable_nat + uu___4 in FStarC_Compiler_Util.print2 "Clear of (%s), env has %s binders\n" uu___2 uu___3) in Obj.magic @@ -10641,8 +10632,7 @@ let (refl_is_non_informative : (fun uu___4 -> let uu___5 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) b in + FStarC_Class_Show.showable_bool b in FStarC_Compiler_Util.format1 "refl_is_non_informative: returned %s" uu___5); if b diff --git a/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml b/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml index c7536450885..0488b062bb7 100644 --- a/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml +++ b/ocaml/fstar-lib/generated/FStarC_ToSyntax_ToSyntax.ml @@ -9315,19 +9315,13 @@ and (desugar_decl_maybe_fail_attr : let uu___12 = let uu___13 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) - e in + FStarC_Class_Show.showable_int e in let uu___14 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) - n2 in + FStarC_Class_Show.showable_int n2 in let uu___15 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) - n1 in + FStarC_Class_Show.showable_int n1 in FStarC_Compiler_Util.format3 "Error #%s was raised %s times, instead of %s." uu___13 uu___14 uu___15 in diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Cfg.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Cfg.ml index 90f688bb614..7e078eb6359 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Cfg.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Cfg.ml @@ -418,44 +418,31 @@ let (steps_to_string : fsteps -> Prims.string) = let b = FStarC_Compiler_Util.string_of_bool in let uu___ = let uu___1 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) f.beta in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool f.beta in let uu___2 = let uu___3 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) f.iota in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool f.iota in let uu___4 = let uu___5 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) f.zeta in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool f.zeta in let uu___6 = let uu___7 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) f.zeta_full in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + f.zeta_full in let uu___8 = let uu___9 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) f.weak in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool f.weak in let uu___10 = let uu___11 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) f.hnf in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + f.hnf in let uu___12 = let uu___13 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) f.primops in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + f.primops in let uu___14 = let uu___15 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.show FStarC_Class_Show.showable_bool f.do_not_unfold_pure_lets in let uu___16 = let uu___17 = @@ -489,8 +476,7 @@ let (steps_to_string : fsteps -> Prims.string) = FStarC_Class_Show.show (FStarC_Class_Show.show_option (FStarC_Class_Show.show_list - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string))) + FStarC_Class_Show.showable_string)) f.unfold_qual in let uu___26 = let uu___27 = @@ -500,12 +486,9 @@ let (steps_to_string : fsteps -> Prims.string) = (FStarC_Class_Show.show_list (FStarC_Class_Show.show_tuple2 (FStarC_Class_Show.show_list - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string)) - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool))) - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool))) + FStarC_Class_Show.showable_string) + FStarC_Class_Show.showable_bool)) + FStarC_Class_Show.showable_bool)) f.unfold_namespace in let uu___28 = let uu___29 = @@ -517,100 +500,83 @@ let (steps_to_string : fsteps -> Prims.string) = let uu___30 = let uu___31 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.pure_subterms_within_computations in let uu___32 = let uu___33 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.simplify in let uu___34 = let uu___35 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.erase_universes in let uu___36 = let uu___37 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.allow_unbound_universes in let uu___38 = let uu___39 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.reify_ in let uu___40 = let uu___41 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.compress_uvars in let uu___42 = let uu___43 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.no_full_norm in let uu___44 = let uu___45 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.check_no_uvars in let uu___46 = let uu___47 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.unmeta in let uu___48 = let uu___49 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.unascribe in let uu___50 = let uu___51 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.in_full_norm_request in let uu___52 = let uu___53 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.weakly_reduce_scrutinee in let uu___54 = let uu___55 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.for_extraction in let uu___56 = let uu___57 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.unrefine in let uu___58 = let uu___59 = FStarC_Class_Show.show - ( - FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.default_univs_to_zero in let uu___60 = let uu___61 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool f.tactics in [uu___61] in uu___59 :: diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Core.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Core.ml index 3a244f47e12..86b650ee70a 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Core.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Core.ml @@ -429,21 +429,18 @@ let (showable_context : context FStarC_Class_Show.showable) = FStarC_Class_Show.show = (fun context1 -> let uu___ = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) context1.no_guard in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + context1.no_guard in let uu___1 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) context1.unfolding_ok in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + context1.unfolding_ok in let uu___2 = let uu___3 = FStarC_Compiler_List.map FStar_Pervasives_Native.fst context1.error_context in FStarC_Class_Show.show - (FStarC_Class_Show.show_list - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string)) uu___3 in + (FStarC_Class_Show.show_list FStarC_Class_Show.showable_string) + uu___3 in FStarC_Compiler_Util.format3 "{no_guard=%s; unfolding_ok=%s; error_context=%s}" uu___ uu___1 uu___2) @@ -7962,9 +7959,7 @@ let (check_term_top_gh : then let uu___2 = let uu___3 = get_goal_ctr () in - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) uu___3 in + FStarC_Class_Show.show FStarC_Class_Show.showable_int uu___3 in FStarC_Compiler_Util.print1 "(%s) Entering core ... \n" uu___2 else ()); (let uu___2 = @@ -7974,9 +7969,7 @@ let (check_term_top_gh : then let uu___3 = let uu___4 = get_goal_ctr () in - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) uu___4 in + FStarC_Class_Show.show FStarC_Class_Show.showable_int uu___4 in let uu___4 = FStarC_Class_Show.show FStarC_Syntax_Print.showable_term e in let uu___5 = @@ -8206,13 +8199,11 @@ let (check_term_equality : let uu___3 = FStarC_Class_Show.show FStarC_Syntax_Print.showable_term t1 in let uu___4 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) guard_ok in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + guard_ok in let uu___5 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) unfolding_ok1 in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + unfolding_ok1 in FStarC_Compiler_Util.print4 "Entering check_term_equality with %s and %s (guard_ok=%s; unfolding_ok=%s) {\n" uu___2 uu___3 uu___4 uu___5 @@ -8236,8 +8227,7 @@ let (check_term_equality : FStarC_Class_Show.show (showable_result (FStarC_Class_Show.show_tuple2 - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_unit) + FStarC_Class_Show.showable_unit (FStarC_Class_Show.show_option FStarC_Syntax_Print.showable_term))) r in FStarC_Compiler_Util.print3 diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_DMFF.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_DMFF.ml index 04eb13bc702..833313ca41a 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_DMFF.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_DMFF.ml @@ -2958,8 +2958,7 @@ and (infer : FStarC_Compiler_Util.string_of_int (n' - n) in let uu___7 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) n in + FStarC_Class_Show.showable_nat n in FStarC_Compiler_Util.format3 "The head of this application, after being applied to %s arguments, is an effectful computation (leaving %s arguments to be applied). Please let-bind the head applied to the %s first arguments." uu___5 uu___6 uu___7 in diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Env.ml index 6ffc8427b59..00c47d6e62d 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Env.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Env.ml @@ -241,16 +241,14 @@ let rec (step_to_string : step -> Prims.string) = | UnfoldQual strs1 -> let uu___ = FStarC_Class_Show.show - (FStarC_Class_Show.show_list - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string)) strs1 in + (FStarC_Class_Show.show_list FStarC_Class_Show.showable_string) + strs1 in Prims.strcat "UnfoldQual " uu___ | UnfoldNamespace strs1 -> let uu___ = FStarC_Class_Show.show - (FStarC_Class_Show.show_list - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string)) strs1 in + (FStarC_Class_Show.show_list FStarC_Class_Show.showable_string) + strs1 in Prims.strcat "UnfoldNamespace " uu___ | DontUnfoldAttr lids1 -> let uu___ = @@ -5138,14 +5136,10 @@ let rec (unfold_effect_abbrev : then (let uu___4 = let uu___5 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.show FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length binders1) in let uu___6 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int ((FStarC_Compiler_List.length c.FStarC_Syntax_Syntax.effect_args) + Prims.int_one) in diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Generalize.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Generalize.ml index b003d8addee..56d0cd6a18b 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Generalize.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Generalize.ml @@ -608,9 +608,8 @@ let (generalize' : FStarC_Syntax_Print.showable_bv FStarC_Syntax_Print.showable_fv) lb) lecs in FStarC_Class_Show.show - (FStarC_Class_Show.show_list - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string)) uu___4 in + (FStarC_Class_Show.show_list FStarC_Class_Show.showable_string) + uu___4 in FStarC_Compiler_Util.print1 "Generalizing: %s\n" uu___3 else ()); (let univnames_lecs = diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_NBE.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_NBE.ml index c021c8124a0..bd693ee0c9b 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_NBE.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_NBE.ml @@ -1537,13 +1537,11 @@ and (iapp : FStarC_Syntax_Print.showable_fv) lb.FStarC_Syntax_Syntax.lbname in let uu___4 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) arity in + FStarC_Class_Show.show FStarC_Class_Show.showable_int + arity in let uu___5 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) n_args_rev in + FStarC_Class_Show.show FStarC_Class_Show.showable_nat + n_args_rev in FStarC_Compiler_Util.print3 "Reached iapp for %s with arity %s and n_args = %s\n" uu___3 uu___4 uu___5); @@ -2121,8 +2119,7 @@ and (translate_letbinding : lb.FStarC_Syntax_Syntax.lbname in let uu___7 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) arity in + FStarC_Class_Show.showable_int arity in FStarC_Compiler_Util.print2 "Making TopLevelLet for %s with arity %s\n" uu___6 uu___7); diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_NBETerm.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_NBETerm.ml index 714f4299e20..f1e7d4e8d7f 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_NBETerm.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_NBETerm.ml @@ -726,9 +726,7 @@ let rec (t_to_string : t -> Prims.string) = let uu___6 = let uu___7 = FStarC_Class_Show.show - (FStarC_Class_Show.show_tuple2 - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + (FStarC_Class_Show.show_tuple2 FStarC_Class_Show.showable_bool (FStarC_Class_Show.show_list FStarC_Syntax_Print.showable_letbinding)) (true, [l]) in Prims.strcat uu___7 ")" in @@ -763,9 +761,7 @@ and (atom_to_string : atom -> Prims.string) = let uu___ = let uu___1 = FStarC_Class_Show.show - (FStarC_Class_Show.show_tuple2 - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + (FStarC_Class_Show.show_tuple2 FStarC_Class_Show.showable_bool (FStarC_Class_Show.show_list FStarC_Syntax_Print.showable_letbinding)) (false, [lb]) in Prims.strcat uu___1 " in ...)" in @@ -774,9 +770,7 @@ and (atom_to_string : atom -> Prims.string) = let uu___1 = let uu___2 = FStarC_Class_Show.show - (FStarC_Class_Show.show_tuple2 - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + (FStarC_Class_Show.show_tuple2 FStarC_Class_Show.showable_bool (FStarC_Class_Show.show_list FStarC_Syntax_Print.showable_letbinding)) (true, lbs) in let uu___3 = diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Normalize.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Normalize.ml index 7975f23357b..2b21b2161c3 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Normalize.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Normalize.ml @@ -23,9 +23,7 @@ let (maybe_debug : let uu___2 = FStarC_Compiler_Util.time_diff time_then time_now in FStar_Pervasives_Native.snd uu___2 in - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) uu___1 in + FStarC_Class_Show.show FStarC_Class_Show.showable_int uu___1 in let uu___1 = FStarC_Class_Show.show FStarC_Syntax_Print.showable_term tm in let uu___2 = @@ -277,9 +275,7 @@ let (showable_stack_elt : stack_elt FStarC_Class_Show.showable) = | MemoLazy uu___1 -> "MemoLazy" | Abs (uu___1, bs, uu___2, uu___3, uu___4) -> let uu___5 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.show FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length bs) in FStarC_Compiler_Util.format1 "Abs %s" uu___5 | UnivArgs uu___1 -> "UnivArgs" @@ -746,13 +742,10 @@ let (reduce_primops : prim_step.FStarC_TypeChecker_Primops_Base.name in let uu___7 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) - l in + FStarC_Class_Show.showable_nat l in let uu___8 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.showable_int prim_step.FStarC_TypeChecker_Primops_Base.arity in FStarC_Compiler_Util.print3 "primop: found partially applied %s (%s/%s args)\n" @@ -2158,16 +2151,12 @@ let rec (norm : FStarC_Class_Tagged.tag_of FStarC_Syntax_Syntax.tagged_term t1 in let uu___3 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.show FStarC_Class_Show.showable_bool (cfg.FStarC_TypeChecker_Cfg.steps).FStarC_TypeChecker_Cfg.no_full_norm in let uu___4 = FStarC_Class_Show.show FStarC_Syntax_Print.showable_term t1 in let uu___5 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.show FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length env1) in let uu___6 = let uu___7 = @@ -2436,8 +2425,7 @@ let rec (norm : FStarC_Compiler_Util.time_diff start fin in FStar_Pervasives_Native.snd uu___7 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) uu___6 in + FStarC_Class_Show.showable_int uu___6 in let uu___6 = FStarC_Class_Show.show FStarC_Syntax_Print.showable_term tm' in @@ -4364,8 +4352,7 @@ and (do_reify_monadic : ed.FStarC_Syntax_Syntax.mname in let uu___15 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.showable_int num_fixed_binders in let uu___16 = let uu___17 = @@ -5022,9 +5009,7 @@ and (norm_comp : let uu___2 = FStarC_Class_Show.show FStarC_Syntax_Print.showable_comp comp in let uu___3 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.show FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length env1) in FStarC_Compiler_Util.print2 ">>> %s\nNormComp with with %s env elements\n" uu___2 uu___3); @@ -5189,9 +5174,8 @@ and (maybe_simplify : FStarC_Class_Show.show FStarC_Syntax_Print.showable_term tm' in let uu___4 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) renorm in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + renorm in FStarC_Compiler_Util.print4 "%sSimplified\n\t%s to\n\t%s\nrenorm = %s\n" (if @@ -6589,9 +6573,7 @@ and (rebuild : let uu___4 = FStarC_Class_Show.show FStarC_Syntax_Print.showable_term t in let uu___5 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.show FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length env1) in let uu___6 = let uu___7 = @@ -7703,8 +7685,7 @@ let (normalize_with_primitive_steps : FStarC_Syntax_Print.showable_term r in let uu___12 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) ms in + FStarC_Class_Show.showable_int ms in FStarC_Compiler_Util.print3 "}\nNormalization%s result = (%s) in %s ms\n" maybe_nbe uu___11 uu___12); @@ -7779,8 +7760,7 @@ let (normalize_comp : FStarC_Syntax_Print.showable_comp c1 in let uu___11 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) ms in + FStarC_Class_Show.showable_int ms in FStarC_Compiler_Util.print2 "}\nNormalization result = (%s) in %s ms\n" uu___10 uu___11); diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Normalize_Unfolding.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Normalize_Unfolding.ml index 0e8c0511e97..4ae38df052d 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Normalize_Unfolding.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Normalize_Unfolding.ml @@ -94,9 +94,8 @@ let (should_unfold : FStarC_Class_Show.show FStarC_Syntax_Print.showable_fv fv in let uu___3 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) b in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + b in FStarC_Compiler_Util.print2 "should_unfold: For DM4F action %s, should_reify = %s\n" uu___2 uu___3); @@ -723,12 +722,9 @@ let (should_unfold : let uu___4 = FStarC_Class_Show.show (FStarC_Class_Show.show_tuple3 - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool)) res in + FStarC_Class_Show.showable_bool + FStarC_Class_Show.showable_bool + FStarC_Class_Show.showable_bool) res in FStarC_Compiler_Util.print3 "should_unfold: For %s (%s), unfolding res = %s\n" uu___2 uu___3 uu___4); @@ -743,12 +739,9 @@ let (should_unfold : let uu___3 = FStarC_Class_Show.show (FStarC_Class_Show.show_tuple3 - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool)) res in + FStarC_Class_Show.showable_bool + FStarC_Class_Show.showable_bool + FStarC_Class_Show.showable_bool) res in FStarC_Compiler_Util.format1 "Unexpected unfolding result: %s" uu___3 in failwith uu___2 in diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Rel.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Rel.ml index ad02ba4cab7..7d56c825e76 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Rel.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Rel.ml @@ -1123,8 +1123,7 @@ let (prob_to_string : let uu___8 = let uu___9 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool p.FStarC_TypeChecker_Common.logical in [uu___9] in (match p.FStarC_TypeChecker_Common.reason with @@ -4391,13 +4390,9 @@ let (should_defer_flex_to_user_tac : worklist -> flex_t -> Prims.bool) = let uu___5 = FStarC_Class_Show.show FStarC_Syntax_Print.showable_ctxu u in let uu___6 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) b in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool b in let uu___7 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.show FStarC_Class_Show.showable_bool (wl.tcenv).FStarC_TypeChecker_Env.enable_defer_to_tac in FStarC_Compiler_Util.print3 "Rel.should_defer_flex_to_user_tac for %s returning %s (env.enable_defer_to_tac: %s)\n" @@ -6241,9 +6236,7 @@ and (solve_rigid_flex_or_flex_rigid_subtyping : if uu___5 then let uu___6 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int tp.FStarC_TypeChecker_Common.pid in FStarC_Compiler_Util.print1 "Trying to solve by meeting refinements:%s\n" uu___6 @@ -9981,9 +9974,7 @@ and (solve_t' : tprob -> worklist -> solution) = Prims.strcat "::" uu___13 in Prims.strcat uu___11 uu___12 in let uu___11 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.show FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length wl.attempting) in FStarC_Compiler_Util.print5 "Attempting %s (%s vs %s); rel = (%s); number of problems in wl = %s\n" @@ -11292,16 +11283,12 @@ and (solve_t' : tprob -> worklist -> solution) = then let uu___11 = let uu___12 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int problem.FStarC_TypeChecker_Common.pid in let uu___13 = let uu___14 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - wl.smt_ok in + FStarC_Class_Show.showable_bool wl.smt_ok in let uu___15 = let uu___16 = FStarC_Class_Show.show @@ -11312,16 +11299,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___19 in + FStarC_Class_Show.showable_bool uu___19 in let uu___19 = let uu___20 = let uu___21 = no_free_uvars t1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___21 in + FStarC_Class_Show.showable_bool uu___21 in let uu___21 = let uu___22 = FStarC_Class_Show.show @@ -11332,15 +11315,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___25 in + FStarC_Class_Show.showable_bool uu___25 in let uu___25 = let uu___26 = let uu___27 = no_free_uvars t2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool uu___27 in [uu___26] in uu___24 :: uu___25 in @@ -11447,16 +11427,12 @@ and (solve_t' : tprob -> worklist -> solution) = then let uu___11 = let uu___12 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int problem.FStarC_TypeChecker_Common.pid in let uu___13 = let uu___14 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - wl.smt_ok in + FStarC_Class_Show.showable_bool wl.smt_ok in let uu___15 = let uu___16 = FStarC_Class_Show.show @@ -11467,16 +11443,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___19 in + FStarC_Class_Show.showable_bool uu___19 in let uu___19 = let uu___20 = let uu___21 = no_free_uvars t1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___21 in + FStarC_Class_Show.showable_bool uu___21 in let uu___21 = let uu___22 = FStarC_Class_Show.show @@ -11487,15 +11459,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___25 in + FStarC_Class_Show.showable_bool uu___25 in let uu___25 = let uu___26 = let uu___27 = no_free_uvars t2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool uu___27 in [uu___26] in uu___24 :: uu___25 in @@ -11602,16 +11571,12 @@ and (solve_t' : tprob -> worklist -> solution) = then let uu___11 = let uu___12 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int problem.FStarC_TypeChecker_Common.pid in let uu___13 = let uu___14 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - wl.smt_ok in + FStarC_Class_Show.showable_bool wl.smt_ok in let uu___15 = let uu___16 = FStarC_Class_Show.show @@ -11622,16 +11587,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___19 in + FStarC_Class_Show.showable_bool uu___19 in let uu___19 = let uu___20 = let uu___21 = no_free_uvars t1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___21 in + FStarC_Class_Show.showable_bool uu___21 in let uu___21 = let uu___22 = FStarC_Class_Show.show @@ -11642,15 +11603,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___25 in + FStarC_Class_Show.showable_bool uu___25 in let uu___25 = let uu___26 = let uu___27 = no_free_uvars t2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool uu___27 in [uu___26] in uu___24 :: uu___25 in @@ -11757,16 +11715,12 @@ and (solve_t' : tprob -> worklist -> solution) = then let uu___11 = let uu___12 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int problem.FStarC_TypeChecker_Common.pid in let uu___13 = let uu___14 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - wl.smt_ok in + FStarC_Class_Show.showable_bool wl.smt_ok in let uu___15 = let uu___16 = FStarC_Class_Show.show @@ -11777,16 +11731,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___19 in + FStarC_Class_Show.showable_bool uu___19 in let uu___19 = let uu___20 = let uu___21 = no_free_uvars t1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___21 in + FStarC_Class_Show.showable_bool uu___21 in let uu___21 = let uu___22 = FStarC_Class_Show.show @@ -11797,15 +11747,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___25 in + FStarC_Class_Show.showable_bool uu___25 in let uu___25 = let uu___26 = let uu___27 = no_free_uvars t2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool uu___27 in [uu___26] in uu___24 :: uu___25 in @@ -11912,16 +11859,12 @@ and (solve_t' : tprob -> worklist -> solution) = then let uu___11 = let uu___12 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int problem.FStarC_TypeChecker_Common.pid in let uu___13 = let uu___14 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - wl.smt_ok in + FStarC_Class_Show.showable_bool wl.smt_ok in let uu___15 = let uu___16 = FStarC_Class_Show.show @@ -11932,16 +11875,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___19 in + FStarC_Class_Show.showable_bool uu___19 in let uu___19 = let uu___20 = let uu___21 = no_free_uvars t1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___21 in + FStarC_Class_Show.showable_bool uu___21 in let uu___21 = let uu___22 = FStarC_Class_Show.show @@ -11952,15 +11891,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___25 in + FStarC_Class_Show.showable_bool uu___25 in let uu___25 = let uu___26 = let uu___27 = no_free_uvars t2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool uu___27 in [uu___26] in uu___24 :: uu___25 in @@ -12067,16 +12003,12 @@ and (solve_t' : tprob -> worklist -> solution) = then let uu___11 = let uu___12 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int problem.FStarC_TypeChecker_Common.pid in let uu___13 = let uu___14 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - wl.smt_ok in + FStarC_Class_Show.showable_bool wl.smt_ok in let uu___15 = let uu___16 = FStarC_Class_Show.show @@ -12087,16 +12019,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___19 in + FStarC_Class_Show.showable_bool uu___19 in let uu___19 = let uu___20 = let uu___21 = no_free_uvars t1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___21 in + FStarC_Class_Show.showable_bool uu___21 in let uu___21 = let uu___22 = FStarC_Class_Show.show @@ -12107,15 +12035,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___25 in + FStarC_Class_Show.showable_bool uu___25 in let uu___25 = let uu___26 = let uu___27 = no_free_uvars t2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool uu___27 in [uu___26] in uu___24 :: uu___25 in @@ -12222,16 +12147,12 @@ and (solve_t' : tprob -> worklist -> solution) = then let uu___11 = let uu___12 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int problem.FStarC_TypeChecker_Common.pid in let uu___13 = let uu___14 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - wl.smt_ok in + FStarC_Class_Show.showable_bool wl.smt_ok in let uu___15 = let uu___16 = FStarC_Class_Show.show @@ -12242,16 +12163,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___19 in + FStarC_Class_Show.showable_bool uu___19 in let uu___19 = let uu___20 = let uu___21 = no_free_uvars t1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___21 in + FStarC_Class_Show.showable_bool uu___21 in let uu___21 = let uu___22 = FStarC_Class_Show.show @@ -12262,15 +12179,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___25 in + FStarC_Class_Show.showable_bool uu___25 in let uu___25 = let uu___26 = let uu___27 = no_free_uvars t2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool uu___27 in [uu___26] in uu___24 :: uu___25 in @@ -12377,16 +12291,12 @@ and (solve_t' : tprob -> worklist -> solution) = then let uu___11 = let uu___12 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int problem.FStarC_TypeChecker_Common.pid in let uu___13 = let uu___14 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - wl.smt_ok in + FStarC_Class_Show.showable_bool wl.smt_ok in let uu___15 = let uu___16 = FStarC_Class_Show.show @@ -12397,16 +12307,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___19 in + FStarC_Class_Show.showable_bool uu___19 in let uu___19 = let uu___20 = let uu___21 = no_free_uvars t1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___21 in + FStarC_Class_Show.showable_bool uu___21 in let uu___21 = let uu___22 = FStarC_Class_Show.show @@ -12417,15 +12323,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___25 in + FStarC_Class_Show.showable_bool uu___25 in let uu___25 = let uu___26 = let uu___27 = no_free_uvars t2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool uu___27 in [uu___26] in uu___24 :: uu___25 in @@ -12532,16 +12435,12 @@ and (solve_t' : tprob -> worklist -> solution) = then let uu___11 = let uu___12 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int problem.FStarC_TypeChecker_Common.pid in let uu___13 = let uu___14 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - wl.smt_ok in + FStarC_Class_Show.showable_bool wl.smt_ok in let uu___15 = let uu___16 = FStarC_Class_Show.show @@ -12552,16 +12451,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___19 in + FStarC_Class_Show.showable_bool uu___19 in let uu___19 = let uu___20 = let uu___21 = no_free_uvars t1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___21 in + FStarC_Class_Show.showable_bool uu___21 in let uu___21 = let uu___22 = FStarC_Class_Show.show @@ -12572,15 +12467,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___25 in + FStarC_Class_Show.showable_bool uu___25 in let uu___25 = let uu___26 = let uu___27 = no_free_uvars t2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool uu___27 in [uu___26] in uu___24 :: uu___25 in @@ -12687,16 +12579,12 @@ and (solve_t' : tprob -> worklist -> solution) = then let uu___11 = let uu___12 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int problem.FStarC_TypeChecker_Common.pid in let uu___13 = let uu___14 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - wl.smt_ok in + FStarC_Class_Show.showable_bool wl.smt_ok in let uu___15 = let uu___16 = FStarC_Class_Show.show @@ -12707,16 +12595,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___19 in + FStarC_Class_Show.showable_bool uu___19 in let uu___19 = let uu___20 = let uu___21 = no_free_uvars t1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___21 in + FStarC_Class_Show.showable_bool uu___21 in let uu___21 = let uu___22 = FStarC_Class_Show.show @@ -12727,15 +12611,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___25 in + FStarC_Class_Show.showable_bool uu___25 in let uu___25 = let uu___26 = let uu___27 = no_free_uvars t2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool uu___27 in [uu___26] in uu___24 :: uu___25 in @@ -12842,16 +12723,12 @@ and (solve_t' : tprob -> worklist -> solution) = then let uu___11 = let uu___12 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int problem.FStarC_TypeChecker_Common.pid in let uu___13 = let uu___14 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - wl.smt_ok in + FStarC_Class_Show.showable_bool wl.smt_ok in let uu___15 = let uu___16 = FStarC_Class_Show.show @@ -12862,16 +12739,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___19 in + FStarC_Class_Show.showable_bool uu___19 in let uu___19 = let uu___20 = let uu___21 = no_free_uvars t1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___21 in + FStarC_Class_Show.showable_bool uu___21 in let uu___21 = let uu___22 = FStarC_Class_Show.show @@ -12882,15 +12755,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___25 in + FStarC_Class_Show.showable_bool uu___25 in let uu___25 = let uu___26 = let uu___27 = no_free_uvars t2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool uu___27 in [uu___26] in uu___24 :: uu___25 in @@ -12997,16 +12867,12 @@ and (solve_t' : tprob -> worklist -> solution) = then let uu___11 = let uu___12 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.show FStarC_Class_Show.showable_int problem.FStarC_TypeChecker_Common.pid in let uu___13 = let uu___14 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - wl.smt_ok in + FStarC_Class_Show.showable_bool wl.smt_ok in let uu___15 = let uu___16 = FStarC_Class_Show.show @@ -13017,16 +12883,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___19 in + FStarC_Class_Show.showable_bool uu___19 in let uu___19 = let uu___20 = let uu___21 = no_free_uvars t1 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___21 in + FStarC_Class_Show.showable_bool uu___21 in let uu___21 = let uu___22 = FStarC_Class_Show.show @@ -13037,15 +12899,12 @@ and (solve_t' : tprob -> worklist -> solution) = FStarC_TypeChecker_Env.is_interpreted wl.tcenv head2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - uu___25 in + FStarC_Class_Show.showable_bool uu___25 in let uu___25 = let uu___26 = let uu___27 = no_free_uvars t2 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool uu___27 in [uu___26] in uu___24 :: uu___25 in @@ -14396,9 +14255,8 @@ let (print_pending_implicits : i.FStarC_TypeChecker_Common.imp_uvar) g.FStarC_TypeChecker_Common.implicits in FStarC_Class_Show.show - (FStarC_Compiler_CList.showable_clist - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string)) uu___ + (FStarC_Compiler_CList.showable_clist FStarC_Class_Show.showable_string) + uu___ let (ineqs_to_string : (FStarC_Syntax_Syntax.universe FStarC_Compiler_CList.clist * (FStarC_Syntax_Syntax.universe * FStarC_Syntax_Syntax.universe) @@ -14428,8 +14286,7 @@ let (ineqs_to_string : let uu___2 = FStarC_Class_Show.show (FStarC_Compiler_CList.showable_clist - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_string)) ineqs2 in + FStarC_Class_Show.showable_string) ineqs2 in FStarC_Compiler_Util.format2 "Solving for %s; inequalities are %s" uu___1 uu___2 let (guard_to_string : @@ -15263,14 +15120,12 @@ let (try_solve_deferred_constraints : let uu___5 = FStarC_Class_Show.show uu___0 defer_ok in let uu___6 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool deferred_to_tac_ok in let uu___7 = FStarC_Class_Show.show showable_wl wl in let uu___8 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length imps_l) in FStarC_Compiler_Util.print4 "Trying to solve carried problems (defer_ok=%s) (deferred_to_tac_ok=%s): begin\n\t%s\nend\n and %s implicits\n" @@ -15347,8 +15202,7 @@ let (try_solve_deferred_constraints : g2.FStarC_TypeChecker_Common.implicits in FStarC_Compiler_List.length uu___10 in FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) uu___9 in + FStarC_Class_Show.showable_nat uu___9 in FStarC_Compiler_Util.print2 "ResolveImplicitsHook: Solved deferred to tactic goals, remaining guard is\n%s (and %s implicits)\n" uu___7 uu___8 @@ -16240,9 +16094,7 @@ let (check_implicit_solution_and_discharge_guard : imp_uvar in let uu___7 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - is_tac in + FStarC_Class_Show.showable_bool is_tac in let uu___8 = FStarC_Class_Show.show FStarC_Syntax_Print.showable_term imp_tm in @@ -16496,9 +16348,7 @@ let (resolve_implicits' : ctx_u in let uu___9 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) - is_tac in + FStarC_Class_Show.showable_bool is_tac in let uu___10 = FStarC_Class_Show.show FStarC_Syntax_Syntax.showable_should_check_uvar diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Tc.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Tc.ml index e4620fee333..7987a9c6fc0 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Tc.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Tc.ml @@ -2305,18 +2305,15 @@ let (tc_decl' : let uu___15 = let uu___16 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.showable_int e in let uu___17 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.showable_int n2 in let uu___18 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.showable_int n1 in FStarC_Compiler_Util.format3 "Error #%s was raised %s times, instead of %s." @@ -4328,9 +4325,7 @@ let (tc_decl : if uu___3 then let uu___4 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.show FStarC_Class_Show.showable_bool env2.FStarC_TypeChecker_Env.admit in let uu___5 = FStarC_Class_Show.show FStarC_Syntax_Print.showable_sigelt se in @@ -4587,9 +4582,8 @@ let (add_sigelt_to_env : then let uu___2 = FStarC_Syntax_Print.sigelt_to_string_short se in let uu___3 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) from_cache in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + from_cache in FStarC_Compiler_Util.print2 ">>>>>>>>>>>>>>Adding top-level decl to environment: %s (from_cache:%s)\n" uu___2 uu___3 @@ -5627,9 +5621,8 @@ let (finish_partial_modul : let uu___6 = let uu___7 = let uu___8 = FStarC_Options.depth () in - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) uu___8 in + FStarC_Class_Show.show FStarC_Class_Show.showable_int + uu___8 in Prims.strcat uu___7 "." in Prims.strcat "Some #push-options have not been popped. Current depth is " diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcEffect.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcEffect.ml index f345d5e3e58..c5b548e2735 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcEffect.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcEffect.ml @@ -4075,8 +4075,7 @@ let (tc_layered_eff_decl : ed.FStarC_Syntax_Syntax.mname in let uu___9 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) n in + FStarC_Class_Show.showable_int n in let uu___10 = FStarC_Class_Tagged.tag_of FStarC_Syntax_Syntax.tagged_term t in @@ -9799,8 +9798,7 @@ let (tc_effect_abbrev : lid in let uu___14 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length uvs2) in let uu___15 = diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcTerm.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcTerm.ml index b21de050299..20b2f2f0b45 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcTerm.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_TcTerm.ml @@ -860,8 +860,7 @@ let (check_expected_effect : expected_c in let uu___12 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.showable_bool use_eq in FStarC_Compiler_Util.print4 "In check_expected_effect, asking rel to solve the problem on e=(%s) and c=(%s), expected_c=(%s), and use_eq=%s\n" @@ -3455,15 +3454,11 @@ and (tc_maybe_toplevel_term : then let uu___8 = let uu___9 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.show FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length uc.FStarC_Syntax_Syntax.uc_fields) in let uu___10 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.show FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length fields) in FStarC_Compiler_Util.format2 "Could not resolve constructor; expected %s fields but only found %s" @@ -4943,14 +4938,10 @@ and (tc_value : FStarC_Class_Show.show FStarC_Syntax_Print.showable_fv fv1 in let uu___8 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.show FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length us1) in let uu___9 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_nat) + FStarC_Class_Show.show FStarC_Class_Show.showable_nat (FStarC_Compiler_List.length us') in FStarC_Compiler_Util.format3 "Unexpected number of universe instantiations for \"%s\" (%s vs %s)" @@ -6642,12 +6633,9 @@ and (tc_abs : (FStarC_Class_Show.show_option (FStarC_Class_Show.show_tuple2 FStarC_Syntax_Print.showable_term - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool))) topt in + FStarC_Class_Show.showable_bool)) topt in let uu___4 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) + FStarC_Class_Show.show FStarC_Class_Show.showable_bool env1.FStarC_TypeChecker_Env.top_level in FStarC_Compiler_Util.print2 "!!!!!!!!!!!!!!!Expected type is (%s), top_level=%s\n" @@ -6675,9 +6663,7 @@ and (tc_abs : (FStarC_Class_Show.show_option (FStarC_Class_Show.show_tuple2 FStarC_Syntax_Print.showable_term - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool))) - uu___8 in + FStarC_Class_Show.showable_bool)) uu___8 in FStarC_Compiler_Util.print3 "After expected_function_typ, tfun_opt: %s, c_opt: %s, and expected type in envbody: %s\n" uu___5 uu___6 uu___7 diff --git a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Util.ml b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Util.ml index 4c20aa84009..54999681fbf 100644 --- a/ocaml/fstar-lib/generated/FStarC_TypeChecker_Util.ml +++ b/ocaml/fstar-lib/generated/FStarC_TypeChecker_Util.ml @@ -5982,9 +5982,8 @@ let (weaken_result_typ : if uu___1 then let uu___2 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool) use_eq in + FStarC_Class_Show.show FStarC_Class_Show.showable_bool + use_eq in let uu___3 = FStarC_Class_Show.show FStarC_Syntax_Print.showable_term e in let uu___4 = FStarC_TypeChecker_Common.lcomp_to_string lc in @@ -6698,8 +6697,7 @@ let (maybe_instantiate : (FStarC_Class_Show.show_option (FStarC_Class_Show.show_tuple2 FStarC_Syntax_Print.showable_term - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_bool))) uu___6 in + FStarC_Class_Show.showable_bool)) uu___6 in FStarC_Compiler_Util.print3 "maybe_instantiate: starting check for (%s) of type (%s), expected type is %s\n" uu___3 uu___4 uu___5 @@ -8063,13 +8061,9 @@ let (get_field_projector_name : let uu___3 = FStarC_Class_Show.show FStarC_Ident.showable_lident datacon in let uu___4 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) n in + FStarC_Class_Show.show FStarC_Class_Show.showable_int n in let uu___5 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) index in + FStarC_Class_Show.show FStarC_Class_Show.showable_int index in FStarC_Compiler_Util.format3 "Data constructor %s does not have enough binders (has %s, tried %s)" uu___3 uu___4 uu___5 in diff --git a/ocaml/fstar-tests/generated/FStarC_Tests_Data.ml b/ocaml/fstar-tests/generated/FStarC_Tests_Data.ml index 0d6aed5c7ed..b3fe2acc290 100644 --- a/ocaml/fstar-tests/generated/FStarC_Tests_Data.ml +++ b/ocaml/fstar-tests/generated/FStarC_Tests_Data.ml @@ -62,9 +62,7 @@ let (run_all : unit -> unit) = match uu___2 with | (f, ms) -> ((let uu___4 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) ms in + FStarC_Class_Show.show FStarC_Class_Show.showable_int ms in FStarC_Compiler_Util.print1 "FlatSet insert: %s\n" uu___4); (let uu___4 = FStarC_Compiler_Util.record_time @@ -75,9 +73,7 @@ let (run_all : unit -> unit) = match uu___4 with | (f_ok, ms1) -> ((let uu___6 = - FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) ms1 in + FStarC_Class_Show.show FStarC_Class_Show.showable_int ms1 in FStarC_Compiler_Util.print1 "FlatSet all_mem: %s\n" uu___6); (let uu___6 = FStarC_Compiler_Util.record_time @@ -89,8 +85,7 @@ let (run_all : unit -> unit) = | (f1, ms2) -> ((let uu___8 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) ms2 in + FStarC_Class_Show.showable_int ms2 in FStarC_Compiler_Util.print1 "FlatSet all_remove: %s\n" uu___8); if Prims.op_Negation f_ok @@ -122,8 +117,7 @@ let (run_all : unit -> unit) = | (rb, ms3) -> ((let uu___12 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) ms3 in + FStarC_Class_Show.showable_int ms3 in FStarC_Compiler_Util.print1 "RBSet insert: %s\n" uu___12); (let uu___12 = @@ -136,9 +130,7 @@ let (run_all : unit -> unit) = | (rb_ok, ms4) -> ((let uu___14 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) - ms4 in + FStarC_Class_Show.showable_int ms4 in FStarC_Compiler_Util.print1 "RBSet all_mem: %s\n" uu___14); (let uu___14 = @@ -151,8 +143,7 @@ let (run_all : unit -> unit) = | (rb1, ms5) -> ((let uu___16 = FStarC_Class_Show.show - (FStarC_Class_Show.printableshow - FStar_Class_Printable.printable_int) + FStarC_Class_Show.showable_int ms5 in FStarC_Compiler_Util.print1 "RBSet all_remove: %s\n" uu___16); diff --git a/src/class/FStarC.Class.Show.fst b/src/class/FStarC.Class.Show.fst index ad15749a627..f424dad8a57 100644 --- a/src/class/FStarC.Class.Show.fst +++ b/src/class/FStarC.Class.Show.fst @@ -1,10 +1,30 @@ module FStarC.Class.Show open FStarC.Compiler.Effect -open FStar.Class.Printable -instance printableshow (_ : printable 'a) : Tot (showable 'a) = { - show = to_string; +instance showable_unit : showable unit = +{ + show = (fun _ -> "()") +} + +instance showable_bool : showable bool = +{ + show = Prims.string_of_bool +} + +instance showable_nat : showable nat = +{ + show = Prims.string_of_int +} + +instance showable_int : showable int = +{ + show = Prims.string_of_int +} + +instance showable_string : showable string = +{ + show = fun x -> "\"" ^ x ^ "\"" } instance show_list (a:Type) (_ : showable a) : Tot (showable (list a)) = { diff --git a/src/class/FStarC.Class.Show.fsti b/src/class/FStarC.Class.Show.fsti index 1837266c107..0c3dc7f50a6 100644 --- a/src/class/FStarC.Class.Show.fsti +++ b/src/class/FStarC.Class.Show.fsti @@ -1,16 +1,17 @@ module FStarC.Class.Show open FStarC.Compiler.Effect -open FStar.Class.Printable module BU = FStarC.Compiler.Util class showable (a:Type) = { show : a -> ML string; } -(* This extends the printable class from ulib, but also allows for an -ML effect of the `printer. *) -instance val printableshow (_ : printable 'a) : Tot (showable 'a) +instance val showable_unit : showable unit +instance val showable_bool : showable bool +instance val showable_nat : showable nat +instance val showable_int : showable int +instance val showable_string : showable string instance val show_list (a:Type) (_ : showable a) : Tot (showable (list a))