Read .holpath directories to allow relocatable developments

If there is a .holpath file in a directory containing a string with a
name for the development under that directory, then the object
files (.uo and .ui) in that directory will be easily relocatable
because they won't use absolute paths, but will instead use
$(devname)/ type paths.

Multiple developments can combine in this way, and there is additional
machinery to make sure that all of the relevant directories are
scanned before reading and writing of object files happens.

tools-poly/builder0.ML

@@ -19,6 +19,24 @@ in
                handle e => OS.Process.exit OS.Process.failure
 end;
 
+val _ = let
+  infix ++
+  val op ++ = OS.Path.concat
+  fun hol_use p s =
+    let
+      val nm = Systeml.HOLDIR ++ p ++ s
+    in
+      use (nm ^ ".sig")
+    ; use (nm ^ ".sml")
+    end
+in
+  List.app (hol_use ("tools" ++ "Holmake"))
+           ["regexpMatch", "parse_glob", "internal_functions",
+            "Holdep_tokens", "Holdep", "Holmake_tools", "Holmake_types",
+            "ReadHMF"]
+end;
+
+
 local
    val rebuild_heaps_var = Systeml.build_after_reloc_envvar
    infix ++

tools-poly/poly/holpathdb.sig

@@ -6,5 +6,7 @@ sig
   val reverse_lookup : {path : string} -> string
   val subst_pathvars : string -> string
                   (* may complain to stdErr about malformed variable things *)
+  val search_for_extensions : (string -> string list) -> string list ->
+                              {vname:string, path:string} list
 
 end

tools-poly/poly/holpathdb.sml

@@ -27,9 +27,11 @@ fun reverse_lookup {path} =
 fun extend_db {vname, path} =
   holpath_db := Binarymap.insert(!holpath_db, vname, path)
 
+fun warn s = TextIO.output(TextIO.stdErr, "WARNING: " ^ s ^ "\n")
+
 fun subst_pathvars modPath =
   let
-    fun die s = (TextIO.output(TextIO.stdErr, "WARNING: " ^ s ^ "\n"); modPath)
+    fun die s = (warn s; modPath)
   in
     if size modPath > 0 andalso String.sub(modPath, 0) = #"$" then
       if size modPath < 2 orelse String.sub(modPath, 1) <> #"(" then
@@ -57,4 +59,66 @@ fun subst_pathvars modPath =
     else modPath
   end
 
+infix ++
+fun p1 ++ p2 = OS.Path.concat(p1,p2)
+
+fun check_insert(m,k,v) =
+  let
+    val _ =
+        case Binarymap.peek(m,k) of
+            NONE => ()
+          | SOME v' => warn((v ++ ".holpath") ^ " overrides value for "^
+                            k ^ " from " ^ (v' ++ ".holpath"))
+  in
+    Binarymap.insert(m,k,v)
+  end
+
+fun readVName d m =
+  let
+    val hp = d ++ ".holpath"
+    val istrm = TextIO.openIn hp
+    val m' =
+        case TextIO.inputLine istrm of
+            NONE => (warn (hp ^ " is empty"); m)
+          | SOME s =>
+            let
+              val sz = size s - 1
+              val nm = if String.sub(s,sz) = #"\n" then
+                         String.extract(s,0,SOME sz)
+                       else s
+            in
+              check_insert(m,nm,d)
+            end
+  in
+    TextIO.closeIn istrm;
+    m'
+  end handle IO.Io _ => m
+
+
+fun search_for_extensions gen dlist =
+  let
+    fun recurse acc visited dlist =
+      case dlist of
+          [] => acc
+        | d::ds =>
+          let
+            val acc' = readVName d acc
+            val pd = OS.Path.getParent d
+            val visited' = Binaryset.add(visited, d)
+            val new_ds =
+                List.filter (fn d => not (Binaryset.member(visited', d)))
+                            (pd :: gen d)
+            val dlist' = new_ds @ ds
+          in
+            recurse acc' visited' dlist'
+          end
+  in
+    Binarymap.foldl (fn (vnm,p,acc) => {vname=vnm,path=p} :: acc)
+                    []
+                    (recurse (Binarymap.mkDict String.compare)
+                             (Binaryset.empty String.compare)
+                             dlist)
+  end
+
+
 end (* struct *)

tools-poly/prelude.ML

@@ -199,10 +199,6 @@ in
   val () =
     ( hol_use ("help" ++ "src-sml") "Database"
     ; hol_use ("tools-poly" ++ "poly") "Help"
-    ; List.app (hol_use ("tools" ++ "Holmake"))
-        ["regexpMatch", "parse_glob", "internal_functions",
-         "Holdep_tokens", "Holdep", "Holmake_tools", "Holmake_types",
-         "ReadHMF"]
     ; PolyML.use (HOLDIR ++ "tools" ++ "makefile-includes.ML")
     ; List.app Meta.fakeload ["PP", "PolyML", "Posix"]
     ; Globals.interactive := true
@@ -236,3 +232,6 @@ in
 end
 
 val _ = HOL_Interactive.toggle_quietdec ()
+val _ = List.app holpathdb.extend_db
+                 (holpathdb.search_for_extensions ReadHMF.find_includes
+                                                  [OS.FileSys.getDir()])

tools/Holmake/ReadHMF.sig

@@ -5,4 +5,16 @@ sig
   type ruledb = Holmake_types.ruledb
   val read : string -> env -> env * ruledb * string option
 
+  val find_includes : string -> string list
+
 end;
+
+(*
+
+   [find_includes dirname] reads the Holmakefile (if any) in directory
+   dirname, and returns the list of directories (in canonical form)
+   that are pointed to by INCLUDES variable declarations. If there is
+   no Holmakefile, the empty list is returned. The directory name in
+   dirname must be a absolute filename.
+
+*)

tools/Holmake/ReadHMF.sml

@@ -304,4 +304,22 @@ fun read fname env =
              Binarymap.mkDict String.compare)
             (empty_condstate, init_buf fname)
 
+fun readlist e vref =
+  map dequote (tokenize (perform_substitution e [VREF vref]))
+
+fun find_includes dirname =
+  let
+    val hm_fname = OS.Path.concat(dirname, "Holmakefile")
+  in
+    if OS.FileSys.access(hm_fname, [OS.FileSys.A_READ]) then
+      let
+        val (e, _, _) = read hm_fname (base_environment())
+        val raw_incs = readlist e "INCLUDES" @ readlist e "PRE_INCLUDES"
+      in
+        map (fn p => OS.Path.mkAbsolute {path = p, relativeTo = dirname})
+            raw_incs
+      end
+    else []
+  end
+
 end (* struct *)

tools/Holmake/poly/BuildCommand.sml

@@ -255,7 +255,10 @@ fun make_build_command (buildinfo : HM_Cline.t buildinfo_t) = let
         p "in end;")
      else
        (p ("val _ = PolyML.SaveState.loadState \"" ^
-           String.toString HOLSTATE ^ "\";\n")));
+           String.toString HOLSTATE ^ "\";\n");
+        p ("val _ = List.app holpathdb.extend_db" ^
+           "(holpathdb.search_for_extensions ReadHMF.find_includes " ^
+           "[OS.FileSys.getDir()])\n")));
     p ("val _ = List.map load [" ^
        String.concatWith "," (List.map (fn f => "\"" ^ f ^ "\"") files) ^
        "] handle x => ((case x of Fail s => print (s^\"\\n\") | _ => ()); \
@@ -473,9 +476,15 @@ fun make_build_command (buildinfo : HM_Cline.t buildinfo_t) = let
                                     time_limit = time_limit,
                                     quiet = quiet_flag, hmenv = hmenv,
                                     jobs = jobs } ii g |> interpret_graph)
+  fun extend_holpaths () =
+    List.app holpathdb.extend_db
+             (holpathdb.search_for_extensions
+                (fn s => [])
+                [OS.FileSys.getDir()])
+
 in
   {extra_impl_deps = [Unhandled HOLSTATE],
-   build_graph = build_graph}
+   build_graph = (fn arg => (extend_holpaths(); build_graph arg))}
 end
 
 end (* struct *)