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