diff --git a/ocaml/fstar-lib/FStarC_Compiler_Util.ml b/ocaml/fstar-lib/FStarC_Compiler_Util.ml index a79418b5617..8538e705878 100644 --- a/ocaml/fstar-lib/FStarC_Compiler_Util.ml +++ b/ocaml/fstar-lib/FStarC_Compiler_Util.ml @@ -1163,3 +1163,6 @@ let array_of_list (l:'a list) = FStar_ImmutableArray_Base.of_list l let array_length (l:'a FStar_ImmutableArray_Base.t) = FStar_ImmutableArray_Base.length l let array_index (l:'a FStar_ImmutableArray_Base.t) (i:Z.t) = FStar_ImmutableArray_Base.index l i + +let putenv k v = Unix.putenv k v +let execvp c args = Unix.execvp c (Array.of_list args) diff --git a/ocaml/fstar-lib/FStarC_Extraction_ML_PrintML.ml b/ocaml/fstar-lib/FStarC_Extraction_ML_PrintML.ml index b83f5ce0ab2..0001a2db940 100644 --- a/ocaml/fstar-lib/FStarC_Extraction_ML_PrintML.ml +++ b/ocaml/fstar-lib/FStarC_Extraction_ML_PrintML.ml @@ -538,7 +538,7 @@ let print (out_dir: string option) (ext: string) (ml: mllib) = let new_doc = FStarC_Extraction_ML_Code.doc_of_mllib ml in iter (fun (n, d) -> FStarC_Compiler_Util.write_file - (FStarC_Options.prepend_output_dir (BatString.concat "" [n;ext])) + (FStarC_Find.prepend_output_dir (BatString.concat "" [n;ext])) (FStarC_Extraction_ML_Code.pretty (Prims.parse_int "120") d) ) new_doc | _ -> failwith "Unrecognized extension" 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 () diff --git a/src/basic/FStarC.Compiler.Plugins.fst b/src/basic/FStarC.Compiler.Plugins.fst index 41bcda5ef0e..4eedcaf8221 100644 --- a/src/basic/FStarC.Compiler.Plugins.fst +++ b/src/basic/FStarC.Compiler.Plugins.fst @@ -89,9 +89,9 @@ let compile_modules dir ms = | None -> "" in let env_setter = BU.format5 "env OCAMLPATH=\"%s/../lib/%s%s/%s%s\"" - Options.fstar_bin_directory + Find.fstar_bin_directory ocamlpath_sep - Options.fstar_bin_directory + Find.fstar_bin_directory ocamlpath_sep old_ocamlpath in diff --git a/src/basic/FStarC.Compiler.Util.fsti b/src/basic/FStarC.Compiler.Util.fsti index d62f85bcd22..e4a08c66911 100644 --- a/src/basic/FStarC.Compiler.Util.fsti +++ b/src/basic/FStarC.Compiler.Util.fsti @@ -391,3 +391,6 @@ val unmarshal: string -> 'a val print_array (f: 'a -> string) (s:FStar.ImmutableArray.Base.t 'a) : string val array_length (s:FStar.ImmutableArray.Base.t 'a) : FStarC.BigInt.t val array_index (s:FStar.ImmutableArray.Base.t 'a) (i:FStarC.BigInt.t) : 'a + +val putenv : string -> string -> unit +val execvp : string -> list string -> unit diff --git a/src/basic/FStarC.Find.fst b/src/basic/FStarC.Find.fst index 0809b25a4cc..325ed663ade 100644 --- a/src/basic/FStarC.Find.fst +++ b/src/basic/FStarC.Find.fst @@ -16,9 +16,69 @@ module FStarC.Find open FStar +open FStarC.Compiler +open FStarC.Compiler.Effect open FStarC.Compiler.List module BU = FStarC.Compiler.Util +let fstar_bin_directory : string = + BU.get_exec_dir () + +let read_fstar_include (fn : string) : option (list string) = + try + let s = BU.file_get_contents fn in + let subdirs = String.split ['\n'] s |> List.filter (fun s -> s <> "" && not (String.get s 0 = '#')) in + Some subdirs + with + | _ -> + failwith ("Could not read " ^ fn); + None + +let rec expand_include_d (dirname : string) : list string = + let dot_inc_path = dirname ^ "/fstar.include" in + if Util.file_exists dot_inc_path then ( + let subdirs = Some?.v <| read_fstar_include dot_inc_path in + dirname :: List.collect (fun subd -> expand_include_d (dirname ^ "/" ^ subd)) subdirs + ) else + [dirname] + +let expand_include_ds (dirnames : list string) : list string = + List.collect expand_include_d dirnames + +(* TODO: normalize these paths. This will probably affect makefiles since +make does not normalize the paths itself. Also, move this whole logic away +from this module. *) +let lib_root () : option string = + (* No default includes means we don't try to find a library on our own. *) + if Options.no_default_includes() then + None + else + (* FSTAR_LIB can be set in the environment to override the library *) + match Util.expand_environment_variable "FSTAR_LIB" with + | Some s -> Some s + | None -> + (* Otherwise, try to find the library in the default locations. It's ulib/ + in the repository, and lib/fstar/ in the binary package. *) + if Util.file_exists (fstar_bin_directory ^ "/../ulib") + then Some (fstar_bin_directory ^ "/../ulib") + else if Util.file_exists (fstar_bin_directory ^ "/../lib/fstar") + then Some (fstar_bin_directory ^ "/../lib/fstar") + else None + +let lib_paths () = + Common.option_to_list (lib_root ()) |> expand_include_ds + +let include_path () = + let cache_dir = + match Options.cache_dir() with + | None -> [] + | Some c -> [c] + in + let include_paths = + Options.include_ () |> expand_include_ds + in + cache_dir @ lib_paths () @ include_paths @ expand_include_d "." + let find_file = let file_map = BU.smap_create 100 in fun filename -> @@ -34,7 +94,7 @@ let find_file = None else (* In reverse, because the last directory has the highest precedence. *) - BU.find_map (List.rev (Options.include_path ())) (fun p -> + BU.find_map (List.rev (include_path ())) (fun p -> let path = if p = "." then filename else BU.join_paths p filename in @@ -48,3 +108,24 @@ let find_file = if Some? result then BU.smap_add file_map filename result; result + + +let prepend_output_dir fname = + match Options.output_dir () with + | None -> fname + | Some x -> Util.join_paths x fname + +let prepend_cache_dir fpath = + match Options.cache_dir () with + | None -> fpath + | Some x -> Util.join_paths x (Util.basename fpath) + +let locate () = + Util.get_exec_dir () |> Util.normalize_file_path + +let locate_lib () = + BU.map_opt (lib_root ()) Util.normalize_file_path + +let locate_ocaml () = + // This is correct right now, but probably should change. + Util.get_exec_dir () ^ "/../lib" |> Util.normalize_file_path diff --git a/src/basic/FStarC.Find.fsti b/src/basic/FStarC.Find.fsti index 17df888310f..dcd791f0e93 100644 --- a/src/basic/FStarC.Find.fsti +++ b/src/basic/FStarC.Find.fsti @@ -14,8 +14,34 @@ limitations under the License. *) module FStarC.Find +(* Utilities for finding files in the include path and related +operations. *) open FStarC.Compiler.Effect +(* A bit silly to have this, but this is the directory where the fstar.exe executable is in. *) +val fstar_bin_directory : string + +(* The root directory of the F* library, if any *) +val lib_root () : option string + +(* The full include path. We search files in all of these directories. *) +val include_path () : list string + (* Try to find a file in the include path with a given basename. *) val find_file (basename : string) : option string + +val prepend_cache_dir : string -> string +val prepend_output_dir : string -> string + + + +(* Return absolute path of directory where fstar.exe lives *) +val locate () : string + +(* Return absolute path of F* library, if any. +(this will be empty with --no_default_includes) *) +val locate_lib () : option string + +(* Return absolute path of OCaml-installed components of F*. *) +val locate_ocaml () : string diff --git a/src/basic/FStarC.Options. b/src/basic/FStarC.Options. deleted file mode 100644 index e69de29bb2d..00000000000 diff --git a/src/basic/FStarC.Options.fst b/src/basic/FStarC.Options.fst index 21d4c86cc26..389c2e13d05 100644 --- a/src/basic/FStarC.Options.fst +++ b/src/basic/FStarC.Options.fst @@ -1835,72 +1835,12 @@ let should_print_message m = then m <> "Prims" else false -let read_fstar_include (fn : string) : option (list string) = - try - let s = file_get_contents fn in - let subdirs = String.split ['\n'] s |> List.filter (fun s -> s <> "" && not (String.get s 0 = '#')) in - Some subdirs - with - | _ -> - failwith ("Could not read " ^ fn); - None - -let rec expand_include_d (dirname : string) : list string = - let dot_inc_path = dirname ^ "/fstar.include" in - if Util.file_exists dot_inc_path then ( - let subdirs = Some?.v <| read_fstar_include dot_inc_path in - dirname :: List.collect (fun subd -> expand_include_d (dirname ^ "/" ^ subd)) subdirs - ) else - [dirname] - -let expand_include_ds (dirnames : list string) : list string = - List.collect expand_include_d dirnames - -(* TODO: normalize these paths. This will probably affect makefiles since -make does not normalize the paths itself. Also, move this whole logic away -from this module. *) -let lib_root () : option string = - (* No default includes means we don't try to find a library on our own. *) - if get_no_default_includes() then - None - else - (* FSTAR_LIB can be set in the environment to override the library *) - match Util.expand_environment_variable "FSTAR_LIB" with - | Some s -> Some s - | None -> - (* Otherwise, try to find the library in the default locations. It's ulib/ - in the repository, and lib/fstar/ in the binary package. *) - if Util.file_exists (fstar_bin_directory ^ "/../ulib") - then Some (fstar_bin_directory ^ "/../ulib") - else if Util.file_exists (fstar_bin_directory ^ "/../lib/fstar") - then Some (fstar_bin_directory ^ "/../lib/fstar") - else None - -let lib_paths () = - Common.option_to_list (lib_root ()) |> expand_include_ds - -let include_path () = - let cache_dir = - match get_cache_dir() with - | None -> [] - | Some c -> [c] - in - let include_paths = - get_include () |> expand_include_ds - in - cache_dir @ lib_paths () @ include_paths @ expand_include_d "." let custom_prims () = get_prims() -let prepend_output_dir fname = - match get_odir() with - | None -> fname - | Some x -> Util.join_paths x fname +let cache_dir () = get_cache_dir () -let prepend_cache_dir fpath = - match get_cache_dir() with - | None -> fpath - | Some x -> Util.join_paths x (Util.basename fpath) +let include_ () = get_include () //Used to parse the options of // --using_facts_from diff --git a/src/basic/FStarC.Options.fsti b/src/basic/FStarC.Options.fsti index 605f744712d..6408a57f5bc 100644 --- a/src/basic/FStarC.Options.fsti +++ b/src/basic/FStarC.Options.fsti @@ -148,9 +148,6 @@ val ide : unit -> bool val ide_id_info_off : unit -> bool val set_ide_filename : string -> unit val ide_filename : unit -> option string -val lib_root : unit -> option string -val lib_paths : unit -> list string -val include_path : unit -> list string val print : unit -> bool val print_in_place : unit -> bool val initial_fuel : unit -> int @@ -183,9 +180,9 @@ val locate_lib : unit -> bool val locate_ocaml : unit -> bool val output_deps_to : unit -> option string val output_dir : unit -> option string -val prepend_cache_dir : string -> string -val prepend_output_dir : string -> string val custom_prims : unit -> option string +val cache_dir : unit -> option string +val include_ : unit -> list string val print_bound_var_types : unit -> bool val print_effect_args : unit -> bool val print_expected_failures : unit -> bool diff --git a/src/fstar.include b/src/fstar.include new file mode 100644 index 00000000000..b8dabaa3e02 --- /dev/null +++ b/src/fstar.include @@ -0,0 +1,15 @@ +basic +class +data +extraction +fstar +parser +prettyprint +reflection +smtencoding +syntax +syntax/print +tactics +tosyntax +typechecker +tests diff --git a/src/fstar/FStarC.Main.fst b/src/fstar/FStarC.Main.fst index 297dcc94752..b0245f4a8e8 100644 --- a/src/fstar/FStarC.Main.fst +++ b/src/fstar/FStarC.Main.fst @@ -153,9 +153,8 @@ let go _ = if Debug.any () then ( Util.print1 "- F* executable: %s\n" (Util.exec_name); - Util.print1 "- F* exec dir: %s\n" (Options.fstar_bin_directory); - Util.print1 "- Library root: %s\n" ((Util.dflt "" (Options.lib_root ()))); - Util.print1 "- Full include path: %s\n" (show (Options.include_path ())); + Util.print1 "- Library root: %s\n" ((Util.dflt "" (Find.lib_root ()))); + Util.print1 "- Full include path: %s\n" (show (Find.include_path ())); Util.print_string "\n"; () ); @@ -210,21 +209,20 @@ let go _ = () else if Options.locate () then ( - Util.print1 "%s\n" (Util.get_exec_dir () |> Util.normalize_file_path); + Util.print1 "%s\n" (Find.locate ()); exit 0 ) else if Options.locate_lib () then ( - match Options.lib_root () with + match Find.locate_lib () with | None -> Util.print_error "No library found (is --no_default_includes set?)\n"; exit 1 | Some s -> - Util.print1 "%s\n" (Util.normalize_file_path s); + Util.print1 "%s\n" s; exit 0 ) else if Options.locate_ocaml () then ( - // This is correct right now, but probably should change. - Util.print1 "%s\n" (Util.get_exec_dir () ^ "/../lib" |> Util.normalize_file_path); + Util.print1 "%s\n" (Find.locate_ocaml ()); exit 0 ) else if Some? (Options.read_krml_file ()) then diff --git a/src/fstar/FStarC.Universal.fst b/src/fstar/FStarC.Universal.fst index a05c3a5241c..944c4026882 100644 --- a/src/fstar/FStarC.Universal.fst +++ b/src/fstar/FStarC.Universal.fst @@ -333,7 +333,7 @@ let emit dep_graph (mllibs:list (uenv & MLSyntax.mllib)) = | Some (_, decls) -> let bindings = FStarC.Extraction.ML.UEnv.bindings_of_uenv env in let deps : list string = Dep.deps_of_modul dep_graph (MLSyntax.string_of_mlpath mname) in - save_value_to_file (Options.prepend_output_dir (filename^ext)) (deps, bindings, decls) + save_value_to_file (Find.prepend_output_dir (filename^ext)) (deps, bindings, decls) | None -> failwith "Unexpected ml modul in Extension extraction mode" ) ms @@ -350,8 +350,8 @@ let emit dep_graph (mllibs:list (uenv & MLSyntax.mllib)) = | Some fname -> fname (* NB: no prepending odir nor adding extension, user chose a explicit path *) | _ -> match programs with - | [ name, _ ] -> name ^ ext |> Options.prepend_output_dir - | _ -> "out" ^ ext |> Options.prepend_output_dir + | [ name, _ ] -> name ^ ext |> Find.prepend_output_dir + | _ -> "out" ^ ext |> Find.prepend_output_dir in save_value_to_file oname bin diff --git a/src/parser/FStarC.Parser.Dep.fst b/src/parser/FStarC.Parser.Dep.fst index c0e384fa57e..0a7e81e8525 100644 --- a/src/parser/FStarC.Parser.Dep.fst +++ b/src/parser/FStarC.Parser.Dep.fst @@ -299,7 +299,7 @@ let cache_file_name = let mname = fn |> module_name_of_file in match Find.find_file (cache_fn |> Util.basename) with | Some path -> - let expected_cache_file = Options.prepend_cache_dir cache_fn in + let expected_cache_file = Find.prepend_cache_dir cache_fn in if Option.isSome (Options.dep()) //if we're in the dependence analysis && not (Options.should_be_already_cached mname) //and checked file is in the && (not (BU.file_exists expected_cache_file) //wrong spot ... complain @@ -331,7 +331,7 @@ let cache_file_name = raise_error0 FStarC.Errors.Error_AlreadyCachedAssertionFailure [ text (BU.format1 "Expected %s to be already checked but could not find it." mname) ]; - FStarC.Options.prepend_cache_dir cache_fn + Find.prepend_cache_dir cache_fn in let memo = Util.smap_create 100 in let memo f x = @@ -455,7 +455,7 @@ let safe_readdir_for_include (d:string) : list string = Return a list of pairs of long names and full paths. *) (* In public interface *) let build_inclusion_candidates_list (): list (string & string) = - let include_directories = Options.include_path () in + let include_directories = Find.include_path () in let include_directories = List.map normalize_file_path include_directories in (* Note that [BatList.unique] keeps the last occurrence, that way one can * always override the precedence order. *) @@ -1432,7 +1432,7 @@ let topological_dependences_of topological_dependences_of' file_system_map dep_graph interfaces_needing_inlining root_files widened let all_files_in_include_paths () = - let paths = Options.include_path () in + let paths = Find.include_path () in List.collect (fun path -> let files = safe_readdir_for_include path in @@ -1759,22 +1759,10 @@ let print_full (outc : out_channel) (deps:deps) : unit = pr "\n\n" in let keys = deps_keys deps.dep_graph in - let no_fstar_stubs_file (s:string) : string = - (* If the original filename begins with FStar.Stubs, then remove that, - consistent with what extraction will actually do. *) - let s1 = "FStar.Stubs." in - let s2 = "FStar." in - let l1 = String.length s1 in - if String.length s >= l1 && String.substring s 0 l1 = s1 then - s2 ^ String.substring s l1 (String.length s - l1) - else - s - in let output_file ext fst_file = let basename = Option.get (check_and_strip_suffix (BU.basename fst_file)) in - let basename = no_fstar_stubs_file basename in let ml_base_name = replace_chars basename '.' "_" in - Options.prepend_output_dir (ml_base_name ^ ext) + Find.prepend_output_dir (ml_base_name ^ ext) in let norm_path s = replace_chars (replace_chars s '\\' "/") ' ' "\\ " in let output_fs_file f = norm_path (output_file ".fs" f) in diff --git a/src/tactics/FStarC.Tactics.Interpreter.fst b/src/tactics/FStarC.Tactics.Interpreter.fst index 8a25c6fd9d8..c1acd4f4fb9 100644 --- a/src/tactics/FStarC.Tactics.Interpreter.fst +++ b/src/tactics/FStarC.Tactics.Interpreter.fst @@ -181,7 +181,7 @@ let unembed_tactic_0 (eb:embedding 'b) (embedded_tac_b:term) (ncb:norm_cb) : tac in Errors.raise_error proof_state.main_context Errors.Fatal_TacticGotStuck [ doc_of_string "Tactic got stuck!"; - doc_of_string "Reduction stopped at: " ^^ pp h_result; + prefix 2 1 (doc_of_string "Reduction stopped at:") (pp h_result); maybe_admit_tip ] diff --git a/tests/error-messages/Bug2899.fst.expected b/tests/error-messages/Bug2899.fst.expected index c98faed40a6..9bad2e4edb9 100644 --- a/tests/error-messages/Bug2899.fst.expected +++ b/tests/error-messages/Bug2899.fst.expected @@ -2,8 +2,8 @@ * Error 170 at Bug2899.fst(7,12-7,18): - Tactic failed - Tactic got stuck! - - Reduction stopped at: FStar.Stubs.Tactics.Result.Success (Prims.admit ()) - "(((proofstate)))" + - Reduction stopped at: + FStar.Stubs.Tactics.Result.Success (Prims.admit ()) "(((proofstate)))" - The term contains an `admit`, which will not reduce. Did you mean `tadmit()`? - See also FStar.Tactics.Effect.fsti(212,48-212,58) @@ -21,8 +21,8 @@ * Error 170 at Bug2899.fst(13,12-13,18): - Tactic failed - Tactic got stuck! - - Reduction stopped at: FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ()) - "(((proofstate)))" + - Reduction stopped at: + FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ()) "(((proofstate)))" - The term contains an `admit`, which will not reduce. Did you mean `tadmit()`? - See also FStar.Tactics.Effect.fsti(212,48-212,58) diff --git a/tests/error-messages/Bug2899.fst.json_expected b/tests/error-messages/Bug2899.fst.json_expected index 740eddb1cc0..1f64a5aee7c 100644 --- a/tests/error-messages/Bug2899.fst.json_expected +++ b/tests/error-messages/Bug2899.fst.json_expected @@ -1,11 +1,11 @@ >> Got issues: [ -{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: FStar.Stubs.Tactics.Result.Success (Prims.admit ())\n \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test0`","While typechecking the top-level declaration `[@@expect_failure] let test0`"]} +{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at:\n FStar.Stubs.Tactics.Result.Success (Prims.admit ()) \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":7,"col":12},"end_pos":{"line":7,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test0`","While typechecking the top-level declaration `[@@expect_failure] let test0`"]} >>] >> Got issues: [ {"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: Prims.admit ()","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":10,"col":12},"end_pos":{"line":10,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test1`","While typechecking the top-level declaration `[@@expect_failure] let test1`"]} >>] >> Got issues: [ -{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ())\n \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":13,"col":12},"end_pos":{"line":13,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]} +{"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at:\n FStar.Stubs.Tactics.V2.Builtins.dump (Prims.admit ()) \"(((proofstate)))\"","The term contains an `admit`, which will not reduce. Did you mean `tadmit()`?"],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":13,"col":12},"end_pos":{"line":13,"col":18}}},"number":170,"ctx":["While preprocessing VC with a tactic","While checking for top-level effects","While typechecking the top-level declaration `let test2`","While typechecking the top-level declaration `[@@expect_failure] let test2`"]} >>] >> Got issues: [ {"msg":["Tactic failed","Tactic got stuck!","Reduction stopped at: reify (tac ()) \"(((proofstate)))\"",""],"level":"Error","range":{"def":{"file_name":"FStar.Tactics.Effect.fsti","start_pos":{"line":212,"col":48},"end_pos":{"line":212,"col":58}},"use":{"file_name":"Bug2899.fst","start_pos":{"line":17,"col":50},"end_pos":{"line":17,"col":66}}},"number":170,"ctx":["While preprocessing VC with a tactic","While typechecking the top-level declaration `let eval_tactic`","While typechecking the top-level declaration `[@@expect_failure] let eval_tactic`"]}