diff --git a/ocaml/fstar-lib/generated/FStarC_Compiler_Plugins.ml b/ocaml/fstar-lib/generated/FStarC_Compiler_Plugins.ml index 280207791cd..0eecbcebf3c 100644 --- a/ocaml/fstar-lib/generated/FStarC_Compiler_Plugins.ml +++ b/ocaml/fstar-lib/generated/FStarC_Compiler_Plugins.ml @@ -120,8 +120,8 @@ let (compile_modules : Prims.string -> Prims.string Prims.list -> unit) = let env_setter = FStarC_Compiler_Util.format5 "env OCAMLPATH=\"%s/../lib/%s%s/%s%s\"" - FStarC_Options.fstar_bin_directory ocamlpath_sep - FStarC_Options.fstar_bin_directory ocamlpath_sep old_ocamlpath in + FStarC_Find.fstar_bin_directory ocamlpath_sep + FStarC_Find.fstar_bin_directory ocamlpath_sep old_ocamlpath in let cmd = FStarC_Compiler_String.concat " " (env_setter :: "ocamlfind" :: args) in diff --git a/ocaml/fstar-lib/generated/FStarC_Find.ml b/ocaml/fstar-lib/generated/FStarC_Find.ml index fe43cc592ff..12410c7d652 100644 --- a/ocaml/fstar-lib/generated/FStarC_Find.ml +++ b/ocaml/fstar-lib/generated/FStarC_Find.ml @@ -1,4 +1,92 @@ open Prims +let (fstar_bin_directory : Prims.string) = + FStarC_Compiler_Util.get_exec_dir () +let (read_fstar_include : + Prims.string -> Prims.string Prims.list FStar_Pervasives_Native.option) = + fun fn -> + try + (fun uu___ -> + match () with + | () -> + let s = FStarC_Compiler_Util.file_get_contents fn in + let subdirs = + FStarC_Compiler_List.filter + (fun s1 -> + (s1 <> "") && + (let uu___1 = + let uu___2 = + FStarC_Compiler_String.get s1 Prims.int_zero in + uu___2 = 35 in + Prims.op_Negation uu___1)) + (FStarC_Compiler_String.split [10] s) in + FStar_Pervasives_Native.Some subdirs) () + with + | uu___ -> + (failwith (Prims.strcat "Could not read " fn); + FStar_Pervasives_Native.None) +let rec (expand_include_d : Prims.string -> Prims.string Prims.list) = + fun dirname -> + let dot_inc_path = Prims.strcat dirname "/fstar.include" in + if FStarC_Compiler_Util.file_exists dot_inc_path + then + let subdirs = + let uu___ = read_fstar_include dot_inc_path in + FStar_Pervasives_Native.__proj__Some__item__v uu___ in + let uu___ = + FStarC_Compiler_List.collect + (fun subd -> + expand_include_d (Prims.strcat dirname (Prims.strcat "/" subd))) + subdirs in + dirname :: uu___ + else [dirname] +let (expand_include_ds : Prims.string Prims.list -> Prims.string Prims.list) + = fun dirnames -> FStarC_Compiler_List.collect expand_include_d dirnames +let (lib_root : unit -> Prims.string FStar_Pervasives_Native.option) = + fun uu___ -> + let uu___1 = FStarC_Options.no_default_includes () in + if uu___1 + then FStar_Pervasives_Native.None + else + (let uu___3 = + FStarC_Compiler_Util.expand_environment_variable "FSTAR_LIB" in + match uu___3 with + | FStar_Pervasives_Native.Some s -> FStar_Pervasives_Native.Some s + | FStar_Pervasives_Native.None -> + if + FStarC_Compiler_Util.file_exists + (Prims.strcat fstar_bin_directory "/../ulib") + then + FStar_Pervasives_Native.Some + (Prims.strcat fstar_bin_directory "/../ulib") + else + if + FStarC_Compiler_Util.file_exists + (Prims.strcat fstar_bin_directory "/../lib/fstar") + then + FStar_Pervasives_Native.Some + (Prims.strcat fstar_bin_directory "/../lib/fstar") + else FStar_Pervasives_Native.None) +let (lib_paths : unit -> Prims.string Prims.list) = + fun uu___ -> + let uu___1 = + let uu___2 = lib_root () in FStarC_Common.option_to_list uu___2 in + expand_include_ds uu___1 +let (include_path : unit -> Prims.string Prims.list) = + fun uu___ -> + let cache_dir = + let uu___1 = FStarC_Options.cache_dir () in + match uu___1 with + | FStar_Pervasives_Native.None -> [] + | FStar_Pervasives_Native.Some c -> [c] in + let include_paths = + let uu___1 = FStarC_Options.include_ () in expand_include_ds uu___1 in + let uu___1 = + let uu___2 = lib_paths () in + let uu___3 = + let uu___4 = expand_include_d "." in + FStarC_Compiler_List.op_At include_paths uu___4 in + FStarC_Compiler_List.op_At uu___2 uu___3 in + FStarC_Compiler_List.op_At cache_dir uu___1 let (find_file : Prims.string -> Prims.string FStar_Pervasives_Native.option) = let file_map = FStarC_Compiler_Util.smap_create (Prims.of_int (100)) in @@ -21,8 +109,8 @@ let (find_file : Prims.string -> Prims.string FStar_Pervasives_Native.option) else FStar_Pervasives_Native.None) else (let uu___4 = - let uu___5 = FStarC_Options.include_path () in - FStar_List_Tot_Base.rev uu___5 in + let uu___5 = include_path () in + FStarC_Compiler_List.rev uu___5 in FStarC_Compiler_Util.find_map uu___4 (fun p -> let path = @@ -36,4 +124,34 @@ let (find_file : Prims.string -> Prims.string FStar_Pervasives_Native.option) (if FStar_Pervasives_Native.uu___is_Some result then FStarC_Compiler_Util.smap_add file_map filename result else (); - result) \ No newline at end of file + result) +let (prepend_output_dir : Prims.string -> Prims.string) = + fun fname -> + let uu___ = FStarC_Options.output_dir () in + match uu___ with + | FStar_Pervasives_Native.None -> fname + | FStar_Pervasives_Native.Some x -> + FStarC_Compiler_Util.join_paths x fname +let (prepend_cache_dir : Prims.string -> Prims.string) = + fun fpath -> + let uu___ = FStarC_Options.cache_dir () in + match uu___ with + | FStar_Pervasives_Native.None -> fpath + | FStar_Pervasives_Native.Some x -> + let uu___1 = FStarC_Compiler_Util.basename fpath in + FStarC_Compiler_Util.join_paths x uu___1 +let (locate : unit -> Prims.string) = + fun uu___ -> + let uu___1 = FStarC_Compiler_Util.get_exec_dir () in + FStarC_Compiler_Util.normalize_file_path uu___1 +let (locate_lib : unit -> Prims.string FStar_Pervasives_Native.option) = + fun uu___ -> + let uu___1 = lib_root () in + FStarC_Compiler_Util.map_opt uu___1 + FStarC_Compiler_Util.normalize_file_path +let (locate_ocaml : unit -> Prims.string) = + fun uu___ -> + let uu___1 = + let uu___2 = FStarC_Compiler_Util.get_exec_dir () in + Prims.strcat uu___2 "/../lib" in + FStarC_Compiler_Util.normalize_file_path uu___1 \ No newline at end of file diff --git a/ocaml/fstar-lib/generated/FStarC_Main.ml b/ocaml/fstar-lib/generated/FStarC_Main.ml index 3950fdeb9b0..be4b9025da6 100644 --- a/ocaml/fstar-lib/generated/FStarC_Main.ml +++ b/ocaml/fstar-lib/generated/FStarC_Main.ml @@ -180,21 +180,19 @@ let go : 'uuuuu . 'uuuuu -> unit = then (FStarC_Compiler_Util.print1 "- F* executable: %s\n" FStarC_Compiler_Util.exec_name; - FStarC_Compiler_Util.print1 "- F* exec dir: %s\n" - FStarC_Options.fstar_bin_directory; + (let uu___8 = + let uu___9 = FStarC_Find.lib_root () in + FStarC_Compiler_Util.dflt "" uu___9 in + FStarC_Compiler_Util.print1 "- Library root: %s\n" uu___8); (let uu___9 = - let uu___10 = FStarC_Options.lib_root () in - FStarC_Compiler_Util.dflt "" uu___10 in - FStarC_Compiler_Util.print1 "- Library root: %s\n" uu___9); - (let uu___10 = - let uu___11 = FStarC_Options.include_path () in + 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___11 in + uu___10 in FStarC_Compiler_Util.print1 "- Full include path: %s\n" - uu___10); + uu___9); FStarC_Compiler_Util.print_string "\n") else ()); load_native_tactics (); @@ -301,18 +299,14 @@ let go : 'uuuuu . 'uuuuu -> unit = (let uu___15 = FStarC_Options.locate () in if uu___15 then - ((let uu___17 = - let uu___18 = - FStarC_Compiler_Util.get_exec_dir () in - FStarC_Compiler_Util.normalize_file_path - uu___18 in + ((let uu___17 = FStarC_Find.locate () in FStarC_Compiler_Util.print1 "%s\n" uu___17); FStarC_Compiler_Effect.exit Prims.int_zero) else (let uu___17 = FStarC_Options.locate_lib () in if uu___17 then - let uu___18 = FStarC_Options.lib_root () in + let uu___18 = FStarC_Find.locate_lib () in match uu___18 with | FStar_Pervasives_Native.None -> (FStarC_Compiler_Util.print_error @@ -320,11 +314,7 @@ let go : 'uuuuu . 'uuuuu -> unit = FStarC_Compiler_Effect.exit Prims.int_one) | FStar_Pervasives_Native.Some s -> - ((let uu___20 = - FStarC_Compiler_Util.normalize_file_path - s in - FStarC_Compiler_Util.print1 "%s\n" - uu___20); + (FStarC_Compiler_Util.print1 "%s\n" s; FStarC_Compiler_Effect.exit Prims.int_zero) else @@ -333,13 +323,7 @@ let go : 'uuuuu . 'uuuuu -> unit = if uu___19 then ((let uu___21 = - let uu___22 = - let uu___23 = - FStarC_Compiler_Util.get_exec_dir - () in - Prims.strcat uu___23 "/../lib" in - FStarC_Compiler_Util.normalize_file_path - uu___22 in + FStarC_Find.locate_ocaml () in FStarC_Compiler_Util.print1 "%s\n" uu___21); FStarC_Compiler_Effect.exit diff --git a/ocaml/fstar-lib/generated/FStarC_Options.ml b/ocaml/fstar-lib/generated/FStarC_Options.ml index f37ffcc1b50..a40aed6b8c3 100644 --- a/ocaml/fstar-lib/generated/FStarC_Options.ml +++ b/ocaml/fstar-lib/generated/FStarC_Options.ml @@ -4120,120 +4120,12 @@ let (module_name_eq : Prims.string -> Prims.string -> Prims.bool) = let (should_print_message : Prims.string -> Prims.bool) = fun m -> let uu___ = should_verify m in if uu___ then m <> "Prims" else false -let (read_fstar_include : - Prims.string -> Prims.string Prims.list FStar_Pervasives_Native.option) = - fun fn -> - try - (fun uu___ -> - match () with - | () -> - let s = FStarC_Compiler_Util.file_get_contents fn in - let subdirs = - FStarC_Compiler_List.filter - (fun s1 -> - (s1 <> "") && - (let uu___3 = - let uu___4 = - FStarC_Compiler_String.get s1 Prims.int_zero in - uu___4 = 35 in - Prims.op_Negation uu___3)) - (FStarC_Compiler_String.split [10] s) in - FStar_Pervasives_Native.Some subdirs) () - with - | uu___ -> - ((let uu___4 = FStarC_Compiler_String.op_Hat "Could not read " fn in - failwith uu___4); - FStar_Pervasives_Native.None) -let rec (expand_include_d : Prims.string -> Prims.string Prims.list) = - fun dirname -> - let dot_inc_path = FStarC_Compiler_String.op_Hat dirname "/fstar.include" in - if FStarC_Compiler_Util.file_exists dot_inc_path - then - let subdirs = - let uu___ = read_fstar_include dot_inc_path in - FStar_Pervasives_Native.__proj__Some__item__v uu___ in - let uu___ = - FStarC_Compiler_List.collect - (fun subd -> - let uu___3 = - let uu___4 = FStarC_Compiler_String.op_Hat "/" subd in - FStarC_Compiler_String.op_Hat dirname uu___4 in - expand_include_d uu___3) subdirs in - dirname :: uu___ - else [dirname] -let (expand_include_ds : Prims.string Prims.list -> Prims.string Prims.list) - = fun dirnames -> FStarC_Compiler_List.collect expand_include_d dirnames -let (lib_root : unit -> Prims.string FStar_Pervasives_Native.option) = - fun uu___ -> - let uu___3 = get_no_default_includes () in - if uu___3 - then FStar_Pervasives_Native.None - else - (let uu___5 = - FStarC_Compiler_Util.expand_environment_variable "FSTAR_LIB" in - match uu___5 with - | FStar_Pervasives_Native.Some s -> FStar_Pervasives_Native.Some s - | FStar_Pervasives_Native.None -> - let uu___6 = - let uu___7 = - FStarC_Compiler_String.op_Hat fstar_bin_directory "/../ulib" in - FStarC_Compiler_Util.file_exists uu___7 in - if uu___6 - then - let uu___7 = - FStarC_Compiler_String.op_Hat fstar_bin_directory "/../ulib" in - FStar_Pervasives_Native.Some uu___7 - else - (let uu___8 = - let uu___9 = - FStarC_Compiler_String.op_Hat fstar_bin_directory - "/../lib/fstar" in - FStarC_Compiler_Util.file_exists uu___9 in - if uu___8 - then - let uu___9 = - FStarC_Compiler_String.op_Hat fstar_bin_directory - "/../lib/fstar" in - FStar_Pervasives_Native.Some uu___9 - else FStar_Pervasives_Native.None)) -let (lib_paths : unit -> Prims.string Prims.list) = - fun uu___ -> - let uu___3 = - let uu___4 = lib_root () in FStarC_Common.option_to_list uu___4 in - expand_include_ds uu___3 -let (include_path : unit -> Prims.string Prims.list) = - fun uu___ -> - let cache_dir = - let uu___3 = get_cache_dir () in - match uu___3 with - | FStar_Pervasives_Native.None -> [] - | FStar_Pervasives_Native.Some c -> [c] in - let include_paths = - let uu___3 = get_include () in expand_include_ds uu___3 in - let uu___3 = - let uu___4 = lib_paths () in - let uu___5 = - let uu___6 = expand_include_d "." in - FStarC_Compiler_List.op_At include_paths uu___6 in - FStarC_Compiler_List.op_At uu___4 uu___5 in - FStarC_Compiler_List.op_At cache_dir uu___3 let (custom_prims : unit -> Prims.string FStar_Pervasives_Native.option) = fun uu___ -> get_prims () -let (prepend_output_dir : Prims.string -> Prims.string) = - fun fname -> - let uu___ = get_odir () in - match uu___ with - | FStar_Pervasives_Native.None -> fname - | FStar_Pervasives_Native.Some x -> - FStarC_Compiler_Util.join_paths x fname -let (prepend_cache_dir : Prims.string -> Prims.string) = - fun fpath -> - let uu___ = get_cache_dir () in - match uu___ with - | FStar_Pervasives_Native.None -> fpath - | FStar_Pervasives_Native.Some x -> - let uu___3 = FStarC_Compiler_Util.basename fpath in - FStarC_Compiler_Util.join_paths x uu___3 +let (cache_dir : unit -> Prims.string FStar_Pervasives_Native.option) = + fun uu___ -> get_cache_dir () +let (include_ : unit -> Prims.string Prims.list) = + fun uu___ -> get_include () let (path_of_text : Prims.string -> Prims.string Prims.list) = fun text -> FStarC_Compiler_String.split [46] text let (parse_settings : diff --git a/ocaml/fstar-lib/generated/FStarC_Parser_Dep.ml b/ocaml/fstar-lib/generated/FStarC_Parser_Dep.ml index 972cd7ef6eb..2ef5c7d92c6 100644 --- a/ocaml/fstar-lib/generated/FStarC_Parser_Dep.ml +++ b/ocaml/fstar-lib/generated/FStarC_Parser_Dep.ml @@ -528,7 +528,7 @@ let (cache_file_name : Prims.string -> Prims.string) = FStarC_Find.find_file uu___1 in match uu___ with | FStar_Pervasives_Native.Some path -> - let expected_cache_file = FStarC_Options.prepend_cache_dir cache_fn in + let expected_cache_file = FStarC_Find.prepend_cache_dir cache_fn in ((let uu___2 = ((let uu___3 = FStarC_Options.dep () in FStarC_Compiler_Option.isSome uu___3) && @@ -605,7 +605,7 @@ let (cache_file_name : Prims.string -> Prims.string) = (Obj.magic FStarC_Errors_Msg.is_error_message_list_doc) (Obj.magic uu___4) else ()); - FStarC_Options.prepend_cache_dir cache_fn) in + FStarC_Find.prepend_cache_dir cache_fn) in let memo = FStarC_Compiler_Util.smap_create (Prims.of_int (100)) in let memo1 f x = let uu___ = FStarC_Compiler_Util.smap_try_find memo x in @@ -808,7 +808,7 @@ let (safe_readdir_for_include : Prims.string -> Prims.string Prims.list) = let (build_inclusion_candidates_list : unit -> (Prims.string * Prims.string) Prims.list) = fun uu___ -> - let include_directories = FStarC_Options.include_path () in + let include_directories = FStarC_Find.include_path () in let include_directories1 = FStarC_Compiler_List.map FStarC_Compiler_Util.normalize_file_path include_directories in @@ -2139,7 +2139,7 @@ let (topological_dependences_of : interfaces_needing_inlining root_files widened let (all_files_in_include_paths : unit -> Prims.string Prims.list) = fun uu___ -> - let paths = FStarC_Options.include_path () in + let paths = FStarC_Find.include_path () in FStarC_Compiler_List.collect (fun path -> let files = safe_readdir_for_include path in @@ -2532,32 +2532,14 @@ let (print_full : FStarC_Compiler_Util.out_channel -> deps -> unit) = let print_entry target first_dep all_deps = pr target; pr ": "; pr first_dep; pr "\\\n\t"; pr all_deps; pr "\n\n" in let keys = deps_keys deps1.dep_graph in - let no_fstar_stubs_file s = - let s1 = "FStar.Stubs." in - let s2 = "FStar." in - let l1 = FStarC_Compiler_String.length s1 in - let uu___ = - ((FStarC_Compiler_String.length s) >= l1) && - (let uu___1 = - FStarC_Compiler_String.substring s Prims.int_zero l1 in - uu___1 = s1) in - if uu___ - then - let uu___1 = - FStarC_Compiler_String.substring s l1 - ((FStarC_Compiler_String.length s) - l1) in - Prims.strcat s2 uu___1 - else s in let output_file ext fst_file = let basename = let uu___ = let uu___1 = FStarC_Compiler_Util.basename fst_file in check_and_strip_suffix uu___1 in FStarC_Compiler_Option.get uu___ in - let basename1 = no_fstar_stubs_file basename in - let ml_base_name = - FStarC_Compiler_Util.replace_chars basename1 46 "_" in - FStarC_Options.prepend_output_dir (Prims.strcat ml_base_name ext) in + let ml_base_name = FStarC_Compiler_Util.replace_chars basename 46 "_" in + FStarC_Find.prepend_output_dir (Prims.strcat ml_base_name ext) in let norm_path s = FStarC_Compiler_Util.replace_chars (FStarC_Compiler_Util.replace_chars s 92 "/") 32 "\\ " in diff --git a/ocaml/fstar-lib/generated/FStarC_Tactics_Interpreter.ml b/ocaml/fstar-lib/generated/FStarC_Tactics_Interpreter.ml index 16b9d9a7507..825d2f296f3 100644 --- a/ocaml/fstar-lib/generated/FStarC_Tactics_Interpreter.ml +++ b/ocaml/fstar-lib/generated/FStarC_Tactics_Interpreter.ml @@ -235,13 +235,14 @@ let unembed_tactic_0 : let uu___3 = let uu___4 = FStarC_Pprint.doc_of_string - "Reduction stopped at: " in + "Reduction stopped at:" in let uu___5 = FStarC_Class_PP.pp FStarC_Syntax_Print.pretty_term h_result in - FStarC_Pprint.op_Hat_Hat uu___4 - uu___5 in + FStarC_Pprint.prefix + (Prims.of_int (2)) Prims.int_one + uu___4 uu___5 in [uu___3; maybe_admit_tip] in uu___1 :: uu___2 in FStarC_Errors.raise_error diff --git a/ocaml/fstar-lib/generated/FStarC_Universal.ml b/ocaml/fstar-lib/generated/FStarC_Universal.ml index 20711b4acee..5008c09fb9c 100644 --- a/ocaml/fstar-lib/generated/FStarC_Universal.ml +++ b/ocaml/fstar-lib/generated/FStarC_Universal.ml @@ -1082,7 +1082,7 @@ let (emit : FStarC_Parser_Dep.deps_of_modul dep_graph uu___5 in let uu___5 = - FStarC_Options.prepend_output_dir + FStarC_Find.prepend_output_dir (Prims.strcat filename ext) in FStarC_Compiler_Util.save_value_to_file uu___5 (deps, bindings, decls) @@ -1105,10 +1105,9 @@ let (emit : | uu___1 -> (match programs with | (name, uu___2)::[] -> - FStarC_Options.prepend_output_dir - (Prims.strcat name ext) + FStarC_Find.prepend_output_dir (Prims.strcat name ext) | uu___2 -> - FStarC_Options.prepend_output_dir + FStarC_Find.prepend_output_dir (Prims.strcat "out" ext)) in FStarC_Compiler_Util.save_value_to_file oname bin | uu___ -> fail ()