1 2use "../src/portableML/GetOpt.sig"; 3use "../src/portableML/GetOpt.sml"; 4use "../tools-poly/poly/Binaryset.sig"; 5use "../tools-poly/poly/Binaryset.sml"; 6use "../tools-poly/poly/Binarymap.sig"; 7use "../tools-poly/poly/Binarymap.sml"; 8use "../tools/Holmake/Systeml.sig"; 9use "../tools-poly/Holmake/Systeml.sml"; 10use "../tools/Holmake/holpathdb.sig"; 11use "../tools/Holmake/holpathdb.sml"; 12 13val _ = holpathdb.extend_db {vname = "HOLDIR", path = Systeml.HOLDIR} 14 15infix |> 16fun x |> f = f x 17 18fun die s = (TextIO.output(TextIO.stdErr, s ^ "\n"); 19 OS.Process.exit OS.Process.failure) 20 21fun mkBuffer () = let 22 val buf = ref ([] : string list) 23 fun push s = buf := s :: !buf 24 fun read () = let 25 val contents = String.concat (List.rev (!buf)) 26 in 27 buf := [contents]; 28 contents 29 end 30 fun reset() = buf := [] 31in 32 (push, read, reset) 33end; 34 35val _ = use "../tools/Holmake/QuoteFilter.sml"; 36val _ = use "../tools/Holmake/QFRead.sig"; 37val _ = use "../tools/Holmake/QFRead.sml"; 38val _ = use "../tools/Holmake/Holdep_tokens.sig" 39val _ = use "../tools/Holmake/Holdep_tokens.sml"; 40 41 42infix ^^ 43val op^^ = OS.Path.concat 44 45fun addIfReadable src fname rest = 46 if OS.FileSys.access(fname, [OS.FileSys.A_READ]) then (src,fname)::rest 47 else rest 48 49fun ToplevelLoad {worklist, alreadySeen, acc} (src,s) = 50 let 51 val basefname = if OS.Path.isRelative s then Systeml.HOLDIR ^^ "sigobj" ^^ s 52 else s 53 val uo = basefname ^ ".uo" 54 val ui = basefname ^ ".ui" 55 in 56 {worklist = worklist |> addIfReadable src uo |> addIfReadable src ui, 57 alreadySeen = Binaryset.add(alreadySeen, s), 58 acc = acc} 59 end 60 61fun load1 (S as {worklist, alreadySeen, acc}) (src,s) = 62 let 63 fun doSource () = 64 {worklist = worklist, 65 alreadySeen = Binaryset.add(alreadySeen, s), 66 acc = s::acc} 67 fun doUOI () = 68 let 69 val instrm = TextIO.openIn s 70 fun recurse acc lnum = 71 case TextIO.inputLine instrm of 72 NONE => (TextIO.closeIn instrm ; acc) 73 | SOME line => 74 let 75 val newfile = String.substring(line, 0, size line - 1) 76 |> holpathdb.subst_pathvars 77 in 78 recurse ((s ^ ":" ^ Int.toString lnum, newfile) :: acc) 79 (lnum + 1) 80 end 81 in 82 {worklist = List.rev (recurse [] 1) @ worklist, 83 alreadySeen = Binaryset.add(alreadySeen, s), 84 acc = acc} 85 end 86 in 87 if Binaryset.member(alreadySeen, s) then S 88 else 89 case OS.Path.ext s of 90 SOME "sig" => doSource() 91 | SOME "sml" => doSource() 92 | SOME "uo" => doUOI() 93 | SOME "ui" => doUOI() 94 | SOME _ => die ("Can't handle " ^ s ^ " (from " ^ src ^ ")") 95 | NONE => ToplevelLoad S (src,s) 96 end 97 98fun dowork {worklist, alreadySeen, acc} = 99 case worklist of 100 [] => List.rev acc 101 | h :: rest => 102 dowork (load1 {worklist = rest, alreadySeen = alreadySeen, acc = acc} h) 103 104type config = {dohelp : bool, prefix : string, prelude : string, 105 suffix : string} 106 107val default_config = {dohelp = false, prefix = "", prelude = "", suffix = ""} 108 109val HOLprelude = 110 "local val dir = OS.FileSys.getDir()\n\ 111 \val _ = OS.FileSys.chDir \"" ^ Systeml.HOLDIR ^^ "tools-poly" ^ "\";\n" ^ 112 "val _ = use \"poly/poly-init2.ML\";\n\ 113 \val _ = OS.FileSys.chDir dir in end;\n" 114 115fun turnOnHelp _ = {dohelp = true, prefix = "", prelude = "", suffix = ""} 116fun turnOnHOL {dohelp,...} = {dohelp = dohelp, prefix = "use \"", 117 suffix = "\";", 118 prelude = HOLprelude} 119fun setPrefix s {prefix,dohelp,suffix,prelude} = 120 {prefix = s, dohelp = dohelp, suffix = suffix, prelude = prelude} 121fun setSuffix s {prefix,dohelp,suffix,prelude} = 122 {prefix = prefix, dohelp = dohelp, suffix = s, prelude = prelude} 123 124val options : (config -> config) GetOpt.opt_descr list = let 125 open GetOpt 126in 127 [{short = "h", long = ["help"], 128 help = "Show some help information", 129 desc = NoArg (fn () => turnOnHelp)}, 130 {short = "", long = ["hol"], 131 help = "Generate a poly-usable source file", 132 desc = NoArg (fn () => turnOnHOL)}, 133 {short = "p", long = ["prefix"], 134 help = "String to be emitted before each line of output", 135 desc = ReqArg (setPrefix, "prefix")}, 136 {short = "s", long = ["suffix"], 137 help = "String emitted after each line of output (before \\n)", 138 desc = ReqArg (setPrefix, "prefix")} 139 ] 140end 141 142 143fun usage() = 144 print (GetOpt.usageInfo { 145 header = "Usage:\n "^CommandLine.name()^ 146 " [options] fname\n\nOptions:", 147 options = options}); 148 149val optionConfig = {argOrder = GetOpt.RequireOrder, 150 errFn = die, 151 options = options} 152 153fun main () = 154 let 155 val (optChanges,fnames) = 156 GetOpt.getOpt optionConfig (CommandLine.arguments()) 157 handle e => die (General.exnMessage e) 158 val config = List.foldl (fn (f,acc) => f acc) default_config optChanges 159 in 160 if #dohelp config then 161 (usage(); OS.Process.exit OS.Process.success) 162 else 163 case fnames of 164 [fname] => 165 let 166 val deps = Holdep_tokens.file_deps fname 167 handle e => die (General.exnMessage e) 168 val result = 169 dowork {worklist = 170 Binaryset.foldr (fn (s,acc) => ("toplevel", s) :: acc) 171 [] 172 deps, 173 acc = [], alreadySeen = Binaryset.empty String.compare} 174 in 175 print (#prelude config) ; 176 List.app 177 (fn s => print (#prefix config ^ s ^ #suffix config ^ "\n")) 178 result 179 end 180 | _ => (usage(); die "") 181 end 182