diff --git a/ocaml/fstar-lib/generated/FStarC_Compiler_Range_Ops.ml b/ocaml/fstar-lib/generated/FStarC_Compiler_Range_Ops.ml index cf25997322d..f02f6db234f 100644 --- a/ocaml/fstar-lib/generated/FStarC_Compiler_Range_Ops.ml +++ b/ocaml/fstar-lib/generated/FStarC_Compiler_Range_Ops.ml @@ -63,35 +63,11 @@ let (string_of_pos : FStarC_Compiler_Range_Type.pos -> Prims.string) = let uu___1 = FStarC_Compiler_Util.string_of_int pos.FStarC_Compiler_Range_Type.col in FStarC_Compiler_Util.format2 "%s,%s" uu___ uu___1 -let (string_of_file_name : Prims.string -> Prims.string) = - fun f -> - let uu___ = - let uu___1 = FStarC_Options_Ext.get "fstar:no_absolute_paths" in - uu___1 = "1" in - if uu___ - then FStarC_Compiler_Util.basename f - else - (let uu___2 = FStarC_Options.ide () in - if uu___2 - then - try - (fun uu___3 -> - match () with - | () -> - let uu___4 = - let uu___5 = FStarC_Compiler_Util.basename f in - FStarC_Find.find_file uu___5 in - (match uu___4 with - | FStar_Pervasives_Native.None -> f - | FStar_Pervasives_Native.Some absolute_path -> - absolute_path)) () - with | uu___3 -> f - else f) let (file_of_range : FStarC_Compiler_Range_Type.range -> Prims.string) = fun r -> let f = (r.FStarC_Compiler_Range_Type.def_range).FStarC_Compiler_Range_Type.file_name in - string_of_file_name f + FStarC_Compiler_Range_Type.string_of_file_name f let (set_file_of_range : FStarC_Compiler_Range_Type.range -> Prims.string -> FStarC_Compiler_Range_Type.range) @@ -113,7 +89,9 @@ let (set_file_of_range : } let (string_of_rng : FStarC_Compiler_Range_Type.rng -> Prims.string) = fun r -> - let uu___ = string_of_file_name r.FStarC_Compiler_Range_Type.file_name in + let uu___ = + FStarC_Compiler_Range_Type.string_of_file_name + r.FStarC_Compiler_Range_Type.file_name in let uu___1 = string_of_pos r.FStarC_Compiler_Range_Type.start_pos in let uu___2 = string_of_pos r.FStarC_Compiler_Range_Type.end_pos in FStarC_Compiler_Util.format3 "%s(%s-%s)" uu___ uu___1 uu___2 diff --git a/ocaml/fstar-lib/generated/FStarC_Compiler_Range_Type.ml b/ocaml/fstar-lib/generated/FStarC_Compiler_Range_Type.ml index 93f704953a4..2f47269e8fa 100644 --- a/ocaml/fstar-lib/generated/FStarC_Compiler_Range_Type.ml +++ b/ocaml/fstar-lib/generated/FStarC_Compiler_Range_Type.ml @@ -75,6 +75,30 @@ let (mk_rng : Prims.string -> pos -> pos -> rng) = fun end_pos -> { file_name = file_name1; start_pos; end_pos } let (mk_range : Prims.string -> pos -> pos -> range) = fun f -> fun b -> fun e -> let r = mk_rng f b e in range_of_rng r r +let (string_of_file_name : Prims.string -> Prims.string) = + fun f -> + let uu___ = + let uu___1 = FStarC_Options_Ext.get "fstar:no_absolute_paths" in + uu___1 = "1" in + if uu___ + then FStarC_Compiler_Util.basename f + else + (let uu___2 = FStarC_Options.ide () in + if uu___2 + then + try + (fun uu___3 -> + match () with + | () -> + let uu___4 = + let uu___5 = FStarC_Compiler_Util.basename f in + FStarC_Find.find_file uu___5 in + (match uu___4 with + | FStar_Pervasives_Native.None -> f + | FStar_Pervasives_Native.Some absolute_path -> + absolute_path)) () + with | uu___3 -> f + else f) let (json_of_pos : pos -> FStarC_Json.json) = fun r -> FStarC_Json.JsonAssoc @@ -85,13 +109,18 @@ let (json_of_rng : rng -> FStarC_Json.json) = let uu___ = let uu___1 = let uu___2 = - let uu___3 = json_of_pos r.start_pos in ("start_pos", uu___3) in + let uu___3 = string_of_file_name r.file_name in + FStarC_Json.JsonStr uu___3 in + ("file_name", uu___2) in + let uu___2 = let uu___3 = - let uu___4 = - let uu___5 = json_of_pos r.end_pos in ("end_pos", uu___5) in - [uu___4] in - uu___2 :: uu___3 in - ("file_name", (FStarC_Json.JsonStr (r.file_name))) :: uu___1 in + let uu___4 = json_of_pos r.start_pos in ("start_pos", uu___4) in + let uu___4 = + let uu___5 = + let uu___6 = json_of_pos r.end_pos in ("end_pos", uu___6) in + [uu___5] in + uu___3 :: uu___4 in + uu___1 :: uu___2 in FStarC_Json.JsonAssoc uu___ let (json_of_range : range -> FStarC_Json.json) = fun r -> diff --git a/ocaml/fstar-lib/generated/FStarC_Find.ml b/ocaml/fstar-lib/generated/FStarC_Find.ml index 12410c7d652..764347f0428 100644 --- a/ocaml/fstar-lib/generated/FStarC_Find.ml +++ b/ocaml/fstar-lib/generated/FStarC_Find.ml @@ -87,42 +87,67 @@ let (include_path : unit -> Prims.string Prims.list) = 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 (do_find : + Prims.string Prims.list -> + Prims.string -> Prims.string FStar_Pervasives_Native.option) + = + fun paths -> + fun filename -> + let uu___ = FStarC_Compiler_Util.is_path_absolute filename in + if uu___ + then + (if FStarC_Compiler_Util.file_exists filename + then FStar_Pervasives_Native.Some filename + else FStar_Pervasives_Native.None) + else + (try + (fun uu___2 -> + match () with + | () -> + FStarC_Compiler_Util.find_map + (FStarC_Compiler_List.rev paths) + (fun p -> + let path = + if p = "." + then filename + else FStarC_Compiler_Util.join_paths p filename in + if FStarC_Compiler_Util.file_exists path + then FStar_Pervasives_Native.Some path + else FStar_Pervasives_Native.None)) () + with | uu___2 -> FStar_Pervasives_Native.None) let (find_file : Prims.string -> Prims.string FStar_Pervasives_Native.option) = - let file_map = FStarC_Compiler_Util.smap_create (Prims.of_int (100)) in + let cache = FStarC_Compiler_Util.smap_create (Prims.of_int (100)) in + fun filename -> + let uu___ = FStarC_Compiler_Util.smap_try_find cache filename in + match uu___ with + | FStar_Pervasives_Native.Some f -> f + | FStar_Pervasives_Native.None -> + let result = let uu___1 = include_path () in do_find uu___1 filename in + (if FStar_Pervasives_Native.uu___is_Some result + then FStarC_Compiler_Util.smap_add cache filename result + else (); + result) +let (find_file_odir : + Prims.string -> Prims.string FStar_Pervasives_Native.option) = + let cache = FStarC_Compiler_Util.smap_create (Prims.of_int (100)) in fun filename -> - let uu___ = FStarC_Compiler_Util.smap_try_find file_map filename in + let uu___ = FStarC_Compiler_Util.smap_try_find cache filename in match uu___ with | FStar_Pervasives_Native.Some f -> f | FStar_Pervasives_Native.None -> + let odir = + let uu___1 = FStarC_Options.output_dir () in + match uu___1 with + | FStar_Pervasives_Native.Some d -> [d] + | FStar_Pervasives_Native.None -> [] in let result = - try - (fun uu___1 -> - match () with - | () -> - let uu___2 = - FStarC_Compiler_Util.is_path_absolute filename in - if uu___2 - then - (if FStarC_Compiler_Util.file_exists filename - then FStar_Pervasives_Native.Some filename - else FStar_Pervasives_Native.None) - else - (let uu___4 = - let uu___5 = include_path () in - FStarC_Compiler_List.rev uu___5 in - FStarC_Compiler_Util.find_map uu___4 - (fun p -> - let path = - if p = "." - then filename - else FStarC_Compiler_Util.join_paths p filename in - if FStarC_Compiler_Util.file_exists path - then FStar_Pervasives_Native.Some path - else FStar_Pervasives_Native.None))) () - with | uu___1 -> FStar_Pervasives_Native.None in + let uu___1 = + let uu___2 = include_path () in + FStarC_Compiler_List.op_At uu___2 odir in + do_find uu___1 filename in (if FStar_Pervasives_Native.uu___is_Some result - then FStarC_Compiler_Util.smap_add file_map filename result + then FStarC_Compiler_Util.smap_add cache filename result else (); result) let (prepend_output_dir : Prims.string -> Prims.string) = diff --git a/ocaml/fstar-lib/generated/FStarC_Main.ml b/ocaml/fstar-lib/generated/FStarC_Main.ml index fdb11effc24..a8146727a44 100644 --- a/ocaml/fstar-lib/generated/FStarC_Main.ml +++ b/ocaml/fstar-lib/generated/FStarC_Main.ml @@ -71,7 +71,7 @@ let (load_native_tactics : unit -> unit) = let uu___1 = ml_module_name m in Prims.strcat uu___1 ".ml" in let cmxs_file m = let cmxs = let uu___1 = ml_module_name m in Prims.strcat uu___1 ".cmxs" in - let uu___1 = FStarC_Find.find_file cmxs in + let uu___1 = FStarC_Find.find_file_odir cmxs in match uu___1 with | FStar_Pervasives_Native.Some f -> f | FStar_Pervasives_Native.None -> @@ -85,7 +85,7 @@ let (load_native_tactics : unit -> unit) = (Obj.magic uu___2) else (let uu___3 = - let uu___4 = ml_file m in FStarC_Find.find_file uu___4 in + let uu___4 = ml_file m in FStarC_Find.find_file_odir uu___4 in match uu___3 with | FStar_Pervasives_Native.None -> let uu___4 = @@ -101,7 +101,7 @@ let (load_native_tactics : unit -> unit) = let dir = FStarC_Compiler_Util.dirname ml in ((let uu___5 = let uu___6 = ml_module_name m in [uu___6] in FStarC_Compiler_Plugins.compile_modules dir uu___5); - (let uu___5 = FStarC_Find.find_file cmxs in + (let uu___5 = FStarC_Find.find_file_odir cmxs in match uu___5 with | FStar_Pervasives_Native.None -> let uu___6 = diff --git a/src/basic/FStarC.Compiler.Range.Ops.fst b/src/basic/FStarC.Compiler.Range.Ops.fst index 98205363c00..2e87067a096 100644 --- a/src/basic/FStarC.Compiler.Range.Ops.fst +++ b/src/basic/FStarC.Compiler.Range.Ops.fst @@ -51,17 +51,6 @@ let rng_included r1 r2 = let string_of_pos pos = format2 "%s,%s" (string_of_int pos.line) (string_of_int pos.col) -let string_of_file_name f = - if Options.Ext.get "fstar:no_absolute_paths" = "1" then - basename f - else if Options.ide () then - try - match Find.find_file (basename f) with - | None -> f //couldn't find file; just return the relative path - | Some absolute_path -> - absolute_path - with _ -> f - else f let file_of_range r = let f = r.def_range.file_name in string_of_file_name f diff --git a/src/basic/FStarC.Compiler.Range.Type.fst b/src/basic/FStarC.Compiler.Range.Type.fst index a9460c42811..53af897b478 100644 --- a/src/basic/FStarC.Compiler.Range.Type.fst +++ b/src/basic/FStarC.Compiler.Range.Type.fst @@ -15,10 +15,12 @@ *) module FStarC.Compiler.Range.Type +open FStarC open FStarC.Compiler.Effect open FStarC.Class.Deq open FStarC.Class.Ord open FStarC.Compiler.Order +module BU = FStarC.Compiler.Util [@@ PpxDerivingYoJson; PpxDerivingShow ] type file_name = string @@ -90,6 +92,18 @@ let mk_rng file_name start_pos end_pos = { let mk_range f b e = let r = mk_rng f b e in range_of_rng r r +let string_of_file_name f = + if Options.Ext.get "fstar:no_absolute_paths" = "1" then + BU.basename f + else if Options.ide () then + try + match Find.find_file (BU.basename f) with + | None -> f //couldn't find file; just return the relative path + | Some absolute_path -> + absolute_path + with _ -> f + else f + open FStarC.Json let json_of_pos (r: pos): json = JsonAssoc [ @@ -98,7 +112,7 @@ let json_of_pos (r: pos): json ] let json_of_rng (r: rng): json = JsonAssoc [ - "file_name", JsonStr r.file_name; + "file_name", JsonStr (string_of_file_name r.file_name); "start_pos", json_of_pos r.start_pos; "end_pos", json_of_pos r.end_pos; ] diff --git a/src/basic/FStarC.Find.fst b/src/basic/FStarC.Find.fst index 325ed663ade..e4bc5d9a172 100644 --- a/src/basic/FStarC.Find.fst +++ b/src/basic/FStarC.Find.fst @@ -79,34 +79,49 @@ let include_path () = in cache_dir @ lib_paths () @ include_paths @ expand_include_d "." +let do_find (paths : list string) (filename : string) : option string = + if BU.is_path_absolute filename then + if BU.file_exists filename then + Some filename + else + None + else + try + (* In reverse, because the last directory has the highest precedence. *) + (* FIXME: We should fail if we find two files with the same name *) + BU.find_map (List.rev paths) (fun p -> + let path = + if p = "." then filename + else BU.join_paths p filename in + if BU.file_exists path then + Some path + else + None) + with + | _ -> None + // ^ to deal with issues like passing bogus strings as paths like " input" + let find_file = - let file_map = BU.smap_create 100 in + let cache = BU.smap_create 100 in + fun filename -> + match BU.smap_try_find cache filename with + | Some f -> f + | None -> + let result = do_find (include_path ()) filename in + if Some? result + then BU.smap_add cache filename result; + result + +let find_file_odir = + let cache = BU.smap_create 100 in fun filename -> - match BU.smap_try_find file_map filename with + match BU.smap_try_find cache filename with | Some f -> f | None -> - let result = - (try - if BU.is_path_absolute filename then - if BU.file_exists filename then - Some filename - else - None - else - (* In reverse, because the last directory has the highest precedence. *) - BU.find_map (List.rev (include_path ())) (fun p -> - let path = - if p = "." then filename - else BU.join_paths p filename in - if BU.file_exists path then - Some path - else - None) - with | _ -> //to deal with issues like passing bogus strings as paths like " input" - None) - in + let odir = match Options.output_dir () with Some d -> [d] | None -> [] in + let result = do_find (include_path () @ odir) filename in if Some? result - then BU.smap_add file_map filename result; + then BU.smap_add cache filename result; result diff --git a/src/basic/FStarC.Find.fsti b/src/basic/FStarC.Find.fsti index dcd791f0e93..be459e0e42a 100644 --- a/src/basic/FStarC.Find.fsti +++ b/src/basic/FStarC.Find.fsti @@ -31,11 +31,13 @@ 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 +(* As above, but also looks in the output directory (--odir). This is useful to find +plugins that we might have created. *) +val find_file_odir (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 diff --git a/src/fstar/FStarC.Main.fst b/src/fstar/FStarC.Main.fst index e575fdcced8..1ae7ad8c1b4 100644 --- a/src/fstar/FStarC.Main.fst +++ b/src/fstar/FStarC.Main.fst @@ -79,20 +79,20 @@ let load_native_tactics () = let ml_file m = ml_module_name m ^ ".ml" in let cmxs_file m = let cmxs = ml_module_name m ^ ".cmxs" in - match Find.find_file cmxs with + match Find.find_file_odir cmxs with | Some f -> f | None -> if List.contains m cmxs_to_load //if this module comes from the cmxs list, fail hard then E.raise_error0 E.Fatal_FailToCompileNativeTactic (Util.format1 "Could not find %s to load" cmxs) else //else try to find and compile the ml file - match Find.find_file (ml_file m) with + match Find.find_file_odir (ml_file m) with | None -> E.raise_error0 E.Fatal_FailToCompileNativeTactic (Util.format1 "Failed to compile native tactic; extracted module %s not found" (ml_file m)) | Some ml -> let dir = Util.dirname ml in Plugins.compile_modules dir [ml_module_name m]; - begin match Find.find_file cmxs with + begin match Find.find_file_odir cmxs with | None -> E.raise_error0 E.Fatal_FailToCompileNativeTactic (Util.format1 "Failed to compile native tactic; compiled object %s not found" cmxs)