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  case List.rev(String.explode s) of
46    #"y" :: #"r" :: #"o" :: #"e" :: #"h" :: #"T" :: n::ame =>
47      SOME(String.implode(List.rev (n::ame)))
48  | _ => NONE
49
50fun addThExt s s' ext = addExt (addDir (Path.dir s') s) ext
51fun outname (rcd as {assumes,includes}) cdir linenum (s, res) =
52  case isTheory s of
53    SOME n => 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' "ui" :: 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' "ui" :: res
64          | NONE => res
65        end
66    end
67  | _ => let
68    in
69      case access rcd cdir s "sig" of
70        SOME s' => addExt s' "ui" :: res
71      | _       => let
72        in
73          case access rcd cdir s "sml" of
74            (* this case handles the situation where there is no .sig file
75               locally, but a .sml file instead; compiling this will generate
76               the .ui file too.  We have to say that we're dependent
77               on the .uo file because the automatic logic will then
78               correctly hunt back to the .sml file *)
79            SOME s' => addExt s' "uo" :: res
80          | _       => let
81            in
82              (* this case added to cover the situations where we think we
83                 are dependent on module foo, but we can't find foo.sml or
84                 foo.sig.  This can happen when foo.sml exists in some
85                 HOL directory but no foo.sig.  In this situation, the HOL
86                 build process only copies foo.ui and foo.uo across to
87                 sigobj (and not the .sig file that we usually find there),
88                 so making the dependency analysis ignore foo.  We cover
89                 this possibility by looking to see if we can see a .ui
90                 file; if so, we can retain the dependency *)
91              case access rcd cdir s "ui" of
92                SOME s' => addExt s' "ui" :: res
93              | NONE => res
94            end
95        end
96    end
97  handle Holdep_Error s =>
98    raise Holdep_Error (s ^ " (line " ^ Int.toString linenum ^ ")")
99
100
101fun beginentry objext target = let
102  val targetname = addExt target objext
103in
104  (targetname,
105   if objext = "uo" andalso FileSys.access(addExt target "sig", []) then
106     [addExt target "ui"]
107   else [])
108end;
109
110val escape_space = let
111  fun translation c = if c = #" " then "\\ "
112                      else if c = #"\\" then "\\\\"
113                      else str c
114in
115  String.translate translation
116end
117val escape_spaces = map escape_space
118
119
120fun encode_for_HOLMKfile {tgt, deps} =
121    if null deps then ""
122    else
123      escape_space tgt ^ ": " ^
124      String.concat (spacify (rev ("\n" :: escape_spaces deps)))
125
126fun uqfname_holdep fname =
127  let
128    val reader = QFRead.fileToReader fname
129  in
130    Holdep_tokens.reader_deps (fname, reader)
131  end
132
133fun read {assumes, includes, srcext, objext, filename} = let
134  val mentions = uqfname_holdep (addExt filename srcext)
135  val curr_dir = Path.dir filename
136  val outrcd = {assumes = assumes, includes = includes}
137  val (targetname, res0) = beginentry objext (manglefilename filename)
138  val res = Binarymap.foldl
139              (fn (s, linenum, acc) =>
140                  outname outrcd curr_dir linenum (manglefilename s, acc))
141              res0
142              mentions
143in
144  {tgt = targetname, deps = res}
145end handle Holdep_Error s => raise Holdep_Error (filename ^ ": " ^ s)
146         | Holdep_tokens.LEX_ERROR s => raise Holdep_Error s;
147
148fun processfile {assumes, includes, fname = filename, diag} =
149    let
150	val {base, ext} = Path.splitBaseExt filename
151    in
152	case ext of
153	    SOME "sig" => read {assumes = assumes, srcext = "sig", objext = "ui",
154                                filename = base, includes = includes}
155	  | SOME "sml" => read {assumes = assumes, srcext = "sml", objext = "uo",
156                                filename = base, includes = includes}
157	  | _          => {tgt = filename, deps = []}
158    end
159
160(* assumes parameter is a list of files that we assume can be built in this
161   directory *)
162fun main (r as {assumes, diag, includes, fname}) =
163  let
164    val results = processfile r
165  in
166    diag (fn () => "Holdep: " ^ #tgt results ^ ": " ^
167                   String.concatWith ", " (#deps results) ^ "\n");
168    results
169  end
170   handle e as OS.SysErr (str, _) => (errMsg str; raise e)
171
172end (* struct *)
173