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