1(* this is an -*- sml -*- file *) 2val _ = use "poly/poly-init.ML"; 3 4val _ = use "../tools/Holmake/Systeml.sig"; 5val _ = use "Holmake/Systeml.sml" 6 7val _ = use "../tools/Holmake/QuoteFilter.sml"; 8val _ = use "../tools/Holmake/HM_SimpleBuffer.sig"; 9val _ = use "../tools/Holmake/HM_SimpleBuffer.sml"; 10val _ = use "../tools/Holmake/QFRead.sig"; 11val _ = use "../tools/Holmake/QFRead.sml"; 12val _ = use "poly/quse.sig"; 13val _ = use "poly/quse.sml"; 14 15local 16 17 fun die s = (TextIO.output(TextIO.stdErr, s ^ "\n"); 18 TextIO.flushOut TextIO.stdErr; 19 raise Fail s) 20 21 fun warn s = (TextIO.output(TextIO.stdErr, "WARNING: " ^ s ^ "\n"); 22 TextIO.flushOut TextIO.stdErr) 23 24 val redirected_files = ["mlibOmegaint.sml"]; 25 val meta_debug = ref false 26 27 fun MDBG s = if !meta_debug then 28 TextIO.output(TextIO.stdOut, "META_DEBUG: " ^ s() ^ "\n") 29 else () 30 31 (* used to stand for "has double quote", but the same analysis is necessary 32 even for files that contain single quotes because of the special 33 treatment that the filter gives to things like `s1 ^ s2` 34 *) 35 fun try_remove f = ((OS.FileSys.remove f) handle OS.SysErr _ => ()); 36 fun has_dq file = 37 let 38 val istrm = TextIO.openIn file 39 fun loop() = 40 case TextIO.input1 istrm of 41 NONE => false 42 | SOME #"`" => true 43 | SOME c => Char.ord c > 127 orelse loop() 44 in 45 loop() before TextIO.closeIn istrm 46 end handle IO.Io _ => false 47 infix ++ 48 fun p1 ++ p2 = OS.Path.concat (p1, p2) 49 open Systeml 50 fun unquote_to file1 file2 = 51 systeml [HOLDIR ++ "bin" ++ "unquote", file1, file2]; 52 53structure FS = OS.FileSys 54 55val loadpathdb = 56 ref (Binarymap.mkDict String.compare : (string,string) Binarymap.dict) 57 58fun quse s = let 59 val _ = if FS.access (s, [FS.A_READ]) then () 60 else die ("Use: non-existent file "^s) 61 val _ = MDBG (fn _ => "Call quse " ^ s) 62 val full = OS.Path.mkCanonical 63 (OS.Path.mkAbsolute{path = s, relativeTo = OS.FileSys.getDir()}) 64in 65 if has_dq s then QUse.use s else PolyML.use s ; 66 loadpathdb := Binarymap.insert(!loadpathdb,OS.Path.file full,OS.Path.dir full) 67end handle OS.Path.Path => die ("Path exception in quse "^s) 68 | e => (TextIO.output(TextIO.stdErr, 69 "error in quse " ^ s ^ " : " ^ 70 General.exnMessage e ^ "\n"); 71 TextIO.flushOut TextIO.stdErr; 72 raise e) 73 74fun myuse f = 75 let val op ++ = OS.Path.concat 76 val file = OS.Path.file f 77 val pd = !PolyML.Compiler.printDepth 78 in 79 PolyML.print_depth 0; 80 ((if List.exists (fn f => f = file) redirected_files then 81 quse (Systeml.HOLDIR ++ "tools-poly" ++ "poly" ++ "redirects" ++ file) 82 else 83 quse f) 84 handle e => (PolyML.print_depth pd; raise e)); 85 PolyML.print_depth pd 86 end handle OS.Path.Path => die ("Path exception in myuse "^f) 87 88val loadPath : string list ref = ref [OS.Path.concat(HOLDIR, "sigobj")]; 89 90val loadedMods = ref (Binaryset.empty String.compare); 91val _ = 92 loadedMods := Binaryset.addList (!loadedMods, 93 ["Real", "Int", "List", "Binaryset", "Binarymap", "Listsort", 94 "Array", "Array2", "Vector"]) 95 96fun findUo modPath [] = NONE 97 | findUo modPath (search::rest) = 98 let val path = 99 OS.Path.mkAbsolute 100 {path = modPath, relativeTo = OS.Path.mkAbsolute 101 {path=search, 102 relativeTo = OS.FileSys.getDir ()}}; 103 in 104 if OS.FileSys.access (path, []) then 105 SOME path 106 else 107 findUo modPath rest 108 end; 109 110val _ = holpathdb.extend_db {vname = "HOLDIR", path = Systeml.HOLDIR} 111 112fun loadUo ps uo = 113 let 114 val i = TextIO.openIn uo 115 val files = 116 String.tokens (fn c => c = #"\n") (TextIO.inputAll i) 117 val _ = TextIO.closeIn i 118 fun str f = ">" ^ f ^ "< -- " ^ String.concatWith " -- " ps 119 fun loadOne f = 120 (case OS.Path.ext f of 121 SOME "sml" => myuse (holpathdb.subst_pathvars f) 122 | SOME "sig" => myuse (holpathdb.subst_pathvars f) 123 | _ => load (uo::ps) f) 124 handle 125 OS.Path.InvalidArc => die ("Invalid arc exception in loading "^str f) 126 | OS.Path.Path => die ("Path exception in loading "^str f) 127 | OS.SysErr(msg,_) => die ("System error '"^msg^"' in loading "^str f) 128 in 129 List.app loadOne files 130 end 131and load ps modPath = 132 let 133 val _ = MDBG (fn _ => "Call load " ^ modPath) 134 val modPath = holpathdb.subst_pathvars modPath 135 val modName = OS.Path.file modPath 136 fun l ext = 137 case findUo (modPath ^ ext) ("."::(!loadPath)) of 138 NONE => die ("Cannot find file " ^ modPath ^ ext) 139 | SOME uo => loadUo ps uo 140 in 141 if Binaryset.member (!loadedMods, modName) then 142 () 143 else 144 (loadedMods := Binaryset.add (!loadedMods, modName); 145 (l ".ui"; l ".uo") 146 handle e => 147 (loadedMods := Binaryset.delete (!loadedMods, modName); 148 raise e)) 149 end handle e => (TextIO.output(TextIO.stdErr, 150 "error in load " ^ modPath ^ " : " ^ 151 General.exnMessage e ^ "\n"); 152 TextIO.flushOut TextIO.stdErr; 153 raise e) 154in 155 156 structure Meta = struct 157 val meta_debug = meta_debug 158 val load = load [] 159 val loadPath = loadPath; 160 fun loaded () = Binaryset.listItems (!loadedMods); 161 fun fakeload s = 162 loadedMods := Binaryset.add(!loadedMods,s) 163 fun findMod modname = findUo (modname ^ ".uo") ("." :: !loadPath) 164 fun fileDirMap () = !loadpathdb 165 end; 166 167open Meta; 168 169end; 170 171 172structure PolyWord8 = Word8; 173(* awfulness to make the environment look like Moscow ML's *) 174 175(* In Poly/ML "before" is 'a * 'b -> 'a and General.before is 'a * unit -> 'a. 176 The Basis library says both should be 'a * unit -> 'a, but in Moscow ML, 177 before is 'a * 'b -> 'a too. Ick. *) 178 179structure Word8 = struct 180 open PolyWord8; 181 fun toLargeWord w = 182 Word.fromLargeWord (PolyWord8.toLargeWord w); 183end; 184 185structure Path = OS.Path; 186structure Process = OS.Process; 187structure FileSys = OS.FileSys; 188 189exception Interrupt = SML90.Interrupt; 190exception Io = IO.Io; 191exception SysErr = OS.SysErr; 192