1(* Holdep -- computing dependencies for a (list of) Moscow ML
2   source files. Also has knowledge of HOL script and theory files.
3   Handles strings and nested comments correctly;
4
5   DOES NOT normalize file names under DOS. (yet)
6
7  This has been adapted from the mosmldep in the MoscowML compiler
8  sources, first by Ken Larsen and later by Konrad Slind and
9  Michael Norrish.
10*)
11structure Holdep :> Holdep =
12struct
13
14structure Process = OS.Process
15structure Path = OS.Path
16structure FileSys = OS.FileSys
17exception Holdep_Error of string
18
19fun normPath s = Path.toString(Path.fromString s)
20fun manglefilename s = normPath s
21fun errMsg str = TextIO.output(TextIO.stdErr, str ^ "\n\n")
22
23fun addExt s ""  = normPath s
24  | addExt s ext = normPath s^"."^ext;
25fun addDir dir s = Path.joinDirFile{dir=normPath dir,file=s}
26
27val space = " ";
28fun spacify [] = []
29  | spacify [x] = [x]
30  | spacify (h::t) = h::space::spacify t;
31
32fun access {assumes, includes} cdir s ext = let
33  val sext = addExt s ext
34  fun inDir dir = FileSys.access (addDir dir sext, [])
35in
36  if inDir cdir orelse List.exists (fn nm => nm = sext) assumes then SOME s
37  else
38    case List.find inDir includes of
39      SOME dir => SOME(addDir dir s)
40    | NONE     => NONE
41end handle OS.Path.InvalidArc =>
42  raise Holdep_Error ("Bad module name \"" ^ s ^ "\"")
43
44fun isTheory s =
45    if String.isSuffix "Theory" s andalso size s > 6 then
46      SOME (String.substring(s, 0, size s - 6))
47    else NONE
48
49fun addThExt s s' ext = addExt (addDir (Path.dir s') s) ext
50fun outname (rcd as {assumes,includes}) cdir linenum (s, res) =
51  case isTheory s of
52    SOME n =>
53    let
54    in
55      (* allow a dependency on a theory if we can see a script.sml file *)
56      case access rcd cdir (n^"Script") "sml" of
57        SOME s' => addThExt s s' "uo" :: res
58      | NONE => let
59        in
60          (* or, if we can see the theory.ui file already; which might
61             happen if the theory file is in sigobj *)
62          case access rcd cdir (n^"Theory") "ui" of
63            SOME s' => addThExt s s' "uo" :: res
64          | NONE => res
65        end
66    end
67  | _ =>
68    let
69    in
70      case access rcd cdir s "sig" of
71        SOME s' => addExt s' "uo" :: res
72      | _       => let
73        in
74          case access rcd cdir s "sml" of
75            (* this case handles the situation where there is no .sig file
76               locally, but a .sml file instead; compiling this will generate
77               the .ui file too.  We have to say that we're dependent
78               on the .uo file because the automatic logic will then
79               correctly hunt back to the .sml file *)
80            SOME s' => addExt s' "uo" :: res
81          | _       => let
82            in
83              (* this case added to cover the situations where we think we
84                 are dependent on module foo, but we can't find foo.sml or
85                 foo.sig.  This can happen when foo.sml exists in some
86                 HOL directory but no foo.sig.  In this situation, the HOL
87                 build process only copies foo.ui and foo.uo across to
88                 sigobj (and not the .sig file that we usually find there),
89                 so making the dependency analysis ignore foo.  We cover
90                 this possibility by looking to see if we can see a .ui
91                 file; if so, we can retain the dependency *)
92              case access rcd cdir s "ui" of
93                SOME s' => addExt s' "uo" :: res
94              | NONE => res
95            end
96        end
97    end
98
99fun beginentry objext target = let
100  val targetname = addExt target objext
101in
102  (targetname,
103   if objext = "uo" andalso FileSys.access(addExt target "sig", []) then
104     [addExt target "ui"]
105   else [])
106end;
107
108val escape_space = let
109  fun translation c = if c = #" " then "\\ "
110                      else if c = #"\\" then "\\\\"
111                      else str c
112in
113  String.translate translation
114end
115val escape_spaces = map escape_space
116
117
118fun encode_for_HOLMKfile {tgt, deps} =
119    if null deps then ""
120    else
121      escape_space tgt ^ ": " ^
122      String.concat (spacify (rev ("\n" :: escape_spaces deps)))
123
124fun uqfname_holdep fname =
125  let
126    val reader = QFRead.fileToReader fname
127  in
128    Holdep_tokens.reader_deps (fname, #read reader)
129  end
130
131fun read {assumes, includes, srcext, objext, filename} = let
132  val mentions = uqfname_holdep (addExt filename srcext)
133  val curr_dir = Path.dir filename
134  val outrcd = {assumes = assumes, includes = includes}
135  val (targetname, res0) = beginentry objext (manglefilename filename)
136  val res = Binarymap.foldl
137              (fn (s, linenum, acc) =>
138                  outname outrcd curr_dir linenum (manglefilename s, acc))
139              res0
140              mentions
141in
142  {tgt = targetname, deps = res}
143end handle Holdep_Error s => raise Holdep_Error (filename ^ ": " ^ s)
144         | Holdep_tokens.LEX_ERROR s => raise Holdep_Error s;
145
146fun processfile {assumes, includes, fname = filename, diag} =
147    let
148	val {base, ext} = Path.splitBaseExt filename
149    in
150	case ext of
151	    SOME "sig" => read {assumes = assumes, srcext = "sig", objext = "ui",
152                                filename = base, includes = includes}
153	  | SOME "sml" => read {assumes = assumes, srcext = "sml", objext = "uo",
154                                filename = base, includes = includes}
155	  | _          => {tgt = filename, deps = []}
156    end
157
158(* assumes parameter is a list of files that we assume can be built in this
159   directory *)
160fun main (r as {assumes, diag, includes, fname}) =
161  let
162    val results = processfile r
163  in
164    diag (fn () => "Holdep: " ^ #tgt results ^ ": " ^
165                   String.concatWith ", " (#deps results));
166    results
167  end
168   handle e as OS.SysErr (str, _) => (errMsg str; raise e)
169
170end (* struct *)
171