Merge pull request #3570 from mtzguido/find

Loading plugins from the output dir too.

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

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;
     ]

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
 
 

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
 

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)