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