diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml index 2eb21e20ca4..71641389090 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml @@ -712,28 +712,36 @@ let (is_machine_int : Prims.string -> Prims.bool) = fun m -> (mk_width m) <> FStar_Pervasives_Native.None type env = { + uenv: FStar_Extraction_ML_UEnv.uenv ; names: name Prims.list ; names_t: Prims.string Prims.list ; module_name: Prims.string Prims.list } and name = { pretty: Prims.string } +let (__proj__Mkenv__item__uenv : env -> FStar_Extraction_ML_UEnv.uenv) = + fun projectee -> + match projectee with | { uenv; names; names_t; module_name;_} -> uenv let (__proj__Mkenv__item__names : env -> name Prims.list) = fun projectee -> - match projectee with | { names; names_t; module_name;_} -> names + match projectee with | { uenv; names; names_t; module_name;_} -> names let (__proj__Mkenv__item__names_t : env -> Prims.string Prims.list) = fun projectee -> - match projectee with | { names; names_t; module_name;_} -> names_t + match projectee with | { uenv; names; names_t; module_name;_} -> names_t let (__proj__Mkenv__item__module_name : env -> Prims.string Prims.list) = fun projectee -> - match projectee with | { names; names_t; module_name;_} -> module_name + match projectee with + | { uenv; names; names_t; module_name;_} -> module_name let (__proj__Mkname__item__pretty : name -> Prims.string) = fun projectee -> match projectee with | { pretty;_} -> pretty -let (empty : Prims.string Prims.list -> env) = - fun module_name -> { names = []; names_t = []; module_name } +let (empty : FStar_Extraction_ML_UEnv.uenv -> Prims.string Prims.list -> env) + = + fun uenv -> + fun module_name -> { uenv; names = []; names_t = []; module_name } let (extend : env -> Prims.string -> env) = fun env1 -> fun x -> { + uenv = (env1.uenv); names = ({ pretty = x } :: (env1.names)); names_t = (env1.names_t); module_name = (env1.module_name) @@ -742,6 +750,7 @@ let (extend_t : env -> Prims.string -> env) = fun env1 -> fun x -> { + uenv = (env1.uenv); names = (env1.names); names_t = (x :: (env1.names_t)); module_name = (env1.module_name) @@ -2837,10 +2846,14 @@ let (translate_type_decl' : FStar_Extraction_ML_Syntax.tydecl_defn = uu___4;_} -> ((let uu___6 = let uu___7 = - FStar_Compiler_Util.format1 - "Error extracting type definition %s to KaRaMeL\n" name1 in + let uu___8 = + let uu___9 = + FStar_Compiler_Util.format1 + "Error extracting type definition %s to KaRaMeL." name1 in + FStar_Errors_Msg.text uu___9 in + [uu___8] in (FStar_Errors_Codes.Warning_DefinitionNotTranslated, uu___7) in - FStar_Errors.log_issue FStar_Compiler_Range_Type.dummyRange + FStar_Errors.log_issue_doc FStar_Compiler_Range_Type.dummyRange uu___6); FStar_Pervasives_Native.None) let (translate_let' : @@ -3025,14 +3038,23 @@ let (translate_let' : ((let uu___6 = let uu___7 = let uu___8 = - FStar_Extraction_ML_Syntax.string_of_mlpath name2 in - let uu___9 = FStar_Compiler_Util.print_exn uu___4 in - FStar_Compiler_Util.format2 - "Error extracting %s to KaRaMeL (%s)\n" uu___8 - uu___9 in + let uu___9 = + let uu___10 = + FStar_Extraction_ML_Syntax.string_of_mlpath + name2 in + FStar_Compiler_Util.format1 + "Error extracting %s to KaRaMeL." uu___10 in + FStar_Errors_Msg.text uu___9 in + let uu___9 = + let uu___10 = + let uu___11 = + FStar_Compiler_Util.print_exn uu___4 in + FStar_Pprint.arbitrary_string uu___11 in + [uu___10] in + uu___8 :: uu___9 in (FStar_Errors_Codes.Warning_DefinitionNotTranslated, uu___7) in - FStar_Errors.log_issue + FStar_Errors.log_issue_doc FStar_Compiler_Range_Type.dummyRange uu___6); FStar_Pervasives_Native.Some (DGlobal @@ -3105,59 +3127,66 @@ let (translate_decl : m; []) let (translate_module : - (FStar_Extraction_ML_Syntax.mlpath * (FStar_Extraction_ML_Syntax.mlsig * - FStar_Extraction_ML_Syntax.mlmodule) FStar_Pervasives_Native.option * - FStar_Extraction_ML_Syntax.mllib) -> file) + FStar_Extraction_ML_UEnv.uenv -> + (FStar_Extraction_ML_Syntax.mlpath * (FStar_Extraction_ML_Syntax.mlsig * + FStar_Extraction_ML_Syntax.mlmodule) FStar_Pervasives_Native.option * + FStar_Extraction_ML_Syntax.mllib) -> file) = - fun m -> - let uu___ = m in - match uu___ with - | (module_name, modul, uu___1) -> - let module_name1 = - FStar_Compiler_List.op_At (FStar_Pervasives_Native.fst module_name) - [FStar_Pervasives_Native.snd module_name] in - let program1 = - match modul with - | FStar_Pervasives_Native.Some (_signature, decls) -> - FStar_Compiler_List.collect - (translate_decl (empty module_name1)) decls - | uu___2 -> - FStar_Compiler_Effect.failwith - "Unexpected standalone interface or nested modules" in - ((FStar_Compiler_String.concat "_" module_name1), program1) -let (translate : FStar_Extraction_ML_Syntax.mllib -> file Prims.list) = - fun uu___ -> - match uu___ with - | FStar_Extraction_ML_Syntax.MLLib modules -> - FStar_Compiler_List.filter_map - (fun m -> - let m_name = - let uu___1 = m in - match uu___1 with - | (path, uu___2, uu___3) -> - FStar_Extraction_ML_Syntax.string_of_mlpath path in - try - (fun uu___1 -> - match () with - | () -> - ((let uu___3 = - let uu___4 = FStar_Options.silent () in - Prims.op_Negation uu___4 in - if uu___3 - then - FStar_Compiler_Util.print1 - "Attempting to translate module %s\n" m_name - else ()); - (let uu___3 = translate_module m in - FStar_Pervasives_Native.Some uu___3))) () - with - | uu___1 -> - ((let uu___3 = FStar_Compiler_Util.print_exn uu___1 in - FStar_Compiler_Util.print2 - "Unable to translate module: %s because:\n %s\n" m_name - uu___3); - FStar_Pervasives_Native.None)) modules -let (uu___1703 : unit) = + fun uenv -> + fun m -> + let uu___ = m in + match uu___ with + | (module_name, modul, uu___1) -> + let module_name1 = + FStar_Compiler_List.op_At + (FStar_Pervasives_Native.fst module_name) + [FStar_Pervasives_Native.snd module_name] in + let program1 = + match modul with + | FStar_Pervasives_Native.Some (_signature, decls) -> + FStar_Compiler_List.collect + (translate_decl (empty uenv module_name1)) decls + | uu___2 -> + FStar_Compiler_Effect.failwith + "Unexpected standalone interface or nested modules" in + ((FStar_Compiler_String.concat "_" module_name1), program1) +let (translate : + FStar_Extraction_ML_UEnv.uenv -> + FStar_Extraction_ML_Syntax.mllib -> file Prims.list) + = + fun ue -> + fun uu___ -> + match uu___ with + | FStar_Extraction_ML_Syntax.MLLib modules -> + FStar_Compiler_List.filter_map + (fun m -> + let m_name = + let uu___1 = m in + match uu___1 with + | (path, uu___2, uu___3) -> + FStar_Extraction_ML_Syntax.string_of_mlpath path in + try + (fun uu___1 -> + match () with + | () -> + ((let uu___3 = + let uu___4 = FStar_Options.silent () in + Prims.op_Negation uu___4 in + if uu___3 + then + FStar_Compiler_Util.print1 + "Attempting to translate module %s\n" m_name + else ()); + (let uu___3 = translate_module ue m in + FStar_Pervasives_Native.Some uu___3))) () + with + | uu___1 -> + ((let uu___3 = FStar_Compiler_Util.print_exn uu___1 in + FStar_Compiler_Util.print2 + "Unable to translate module: %s because:\n %s\n" + m_name uu___3); + FStar_Pervasives_Native.None)) modules +let (uu___1711 : unit) = register_post_translate_type_without_decay translate_type_without_decay'; register_post_translate_type translate_type'; register_post_translate_type_decl translate_type_decl'; diff --git a/ocaml/fstar-lib/generated/FStar_Universal.ml b/ocaml/fstar-lib/generated/FStar_Universal.ml index e5151291658..c7b12c4caba 100644 --- a/ocaml/fstar-lib/generated/FStar_Universal.ml +++ b/ocaml/fstar-lib/generated/FStar_Universal.ml @@ -1003,10 +1003,11 @@ let (emit : ms)) mllibs | FStar_Pervasives_Native.Some (FStar_Options.Krml) -> let programs = - let uu___ = - FStar_Compiler_List.map FStar_Pervasives_Native.snd mllibs in - FStar_Compiler_List.collect FStar_Extraction_Krml.translate - uu___ in + FStar_Compiler_List.collect + (fun uu___ -> + match uu___ with + | (ue, mllibs1) -> + FStar_Extraction_Krml.translate ue mllibs1) mllibs in let bin = (FStar_Extraction_Krml.current_version, programs) in (match programs with | (name, uu___)::[] -> @@ -1390,7 +1391,7 @@ let rec (tc_fold_interleave : tc_fold_interleave deps ((FStar_Compiler_List.op_At mods [nmod]), (FStar_Compiler_List.op_At mllibs - (as_list env_before mllib)), env) remaining1))) + (as_list env mllib)), env) remaining1))) let (dbg_dep : Prims.bool FStar_Compiler_Effect.ref) = FStar_Compiler_Debug.get_toggle "Dep" let (batch_mode_tc : diff --git a/src/extraction/FStar.Extraction.Krml.fst b/src/extraction/FStar.Extraction.Krml.fst index 51bc4c74084..7e3c7f36ba1 100644 --- a/src/extraction/FStar.Extraction.Krml.fst +++ b/src/extraction/FStar.Extraction.Krml.fst @@ -24,6 +24,7 @@ open FStar.Compiler.Util open FStar.Extraction open FStar.Extraction.ML open FStar.Extraction.ML.Syntax +open FStar.Extraction.ML.UEnv open FStar.Const open FStar.BaseTypes @@ -286,6 +287,7 @@ let is_machine_int m = (* Environments **************************************************************) type env = { + uenv : uenv; names: list name; names_t: list string; module_name: list string; @@ -295,7 +297,8 @@ and name = { pretty: string; } -let empty module_name = { +let empty uenv module_name = { + uenv = uenv; names = []; names_t = []; module_name = module_name @@ -1149,7 +1152,9 @@ let translate_type_decl' env ty: option decl = ) branches)) | {tydecl_name=name} -> // JP: TODO: figure out why and how this happens - Errors. log_issue Range.dummyRange (Errors.Warning_DefinitionNotTranslated, (BU.format1 "Error extracting type definition %s to KaRaMeL\n" name)); + Errors.log_issue_doc Range.dummyRange (Errors.Warning_DefinitionNotTranslated, [ + Errors.Msg.text <| BU.format1 "Error extracting type definition %s to KaRaMeL." name; + ]); None let translate_let' env flavor lb: option decl = @@ -1237,7 +1242,10 @@ let translate_let' env flavor lb: option decl = let expr = translate_expr env expr in Some (DGlobal (meta, name, List.length tvars, t, expr)) with e -> - Errors. log_issue Range.dummyRange (Errors.Warning_DefinitionNotTranslated, (BU.format2 "Error extracting %s to KaRaMeL (%s)\n" (Syntax.string_of_mlpath name) (BU.print_exn e))); + Errors.log_issue_doc Range.dummyRange (Errors.Warning_DefinitionNotTranslated, [ + Errors.Msg.text <| BU.format1 "Error extracting %s to KaRaMeL." (Syntax.string_of_mlpath name); + Pprint.arbitrary_string (BU.print_exn e); + ]); Some (DGlobal (meta, name, List.length tvars, t, EAny)) end @@ -1293,18 +1301,18 @@ let translate_decl env d: list decl = BU.print1_warning "Not extracting exception %s to KaRaMeL (exceptions unsupported)\n" m; [] -let translate_module (m : mlpath & option (mlsig & mlmodule) & mllib) : file = +let translate_module uenv (m : mlpath & option (mlsig & mlmodule) & mllib) : file = let (module_name, modul, _) = m in let module_name = fst module_name @ [ snd module_name ] in let program = match modul with | Some (_signature, decls) -> - List.collect (translate_decl (empty module_name)) decls + List.collect (translate_decl (empty uenv module_name)) decls | _ -> failwith "Unexpected standalone interface or nested modules" in (String.concat "_" module_name), program -let translate (MLLib modules): list file = +let translate (ue:uenv) (MLLib modules): list file = List.filter_map (fun m -> let m_name = let path, _, _ = m in @@ -1312,7 +1320,7 @@ let translate (MLLib modules): list file = in try if not (Options.silent()) then (BU.print1 "Attempting to translate module %s\n" m_name); - Some (translate_module m) + Some (translate_module ue m) with | e -> BU.print2 "Unable to translate module: %s because:\n %s\n" diff --git a/src/extraction/FStar.Extraction.Krml.fsti b/src/extraction/FStar.Extraction.Krml.fsti index b94be9d590d..bea9e028ea9 100644 --- a/src/extraction/FStar.Extraction.Krml.fsti +++ b/src/extraction/FStar.Extraction.Krml.fsti @@ -25,4 +25,4 @@ type version = int type binary_format = version & list file val current_version: version -val translate : FStar.Extraction.ML.Syntax.mllib -> list file +val translate : Extraction.ML.UEnv.uenv -> FStar.Extraction.ML.Syntax.mllib -> list file diff --git a/src/fstar/FStar.Universal.fst b/src/fstar/FStar.Universal.fst index 8e16a2d83bf..9d49f491c3b 100644 --- a/src/fstar/FStar.Universal.fst +++ b/src/fstar/FStar.Universal.fst @@ -305,7 +305,10 @@ let emit dep_graph (mllibs:list (uenv & MLSyntax.mllib)) = ) mllibs | Some Options.Krml -> - let programs = List.collect Extraction.Krml.translate (List.map snd mllibs) in + let programs = + mllibs |> List.collect (fun (ue, mllibs) -> + Extraction.Krml.translate ue mllibs) + in let bin: Extraction.Krml.binary_format = Extraction.Krml.current_version, programs in begin match programs with | [ name, _ ] -> @@ -548,7 +551,7 @@ let rec tc_fold_interleave (deps:FStar.Parser.Dep.deps) //used to query parsing let remaining, nmod, mllib, env = tc_one_file_from_remaining remaining env_before deps in if not (Options.profile_group_by_decl()) then Profiling.report_and_clear (Ident.string_of_lid nmod.checked_module.name); - tc_fold_interleave deps (mods@[nmod], mllibs@(as_list env_before mllib), env) remaining + tc_fold_interleave deps (mods@[nmod], mllibs@(as_list env mllib), env) remaining (***********************************************************************) (* Batch mode: checking many files *)