1structure Systeml :> Systeml = struct
2
3(* This is the WINDOWS implementation of the Systeml functionality.
4   It is the very first thing compiled by the HOL build process so it
5   absolutely can not depend on any other HOL source code. *)
6
7structure Process = OS.Process
8structure Path = OS.Path
9structure FileSys = OS.FileSys
10
11fun dquote s = concat ["\"", s, "\""]
12
13fun concat_wspaces munge strl = String.concatWith " " (map munge strl)
14
15fun systeml l = let
16  val command = "call "^concat_wspaces dquote l
17in
18  Process.system command
19end
20
21fun systeml_out {outfile} c =
22  Process.system
23    ("call " ^ concat_wspaces dquote c ^ " > " ^ dquote outfile ^ " 2>&1")
24
25
26(* would like to be using Posix.Process.exec, but this seems flakey on
27   various machines (and is entirely unavailable on Moscow ML) *)
28fun exec (comm, args) = OS.Process.exit (systeml (comm::tl args))
29
30val protect = dquote
31
32(* the _ps suffix stands for 'protected string', as opposed to the 'l'
33   of systeml, which stands for 'list' of strings (all of which are
34   presumed unprotected).  The problem is that on Windows, if you pass
35   system a (protected) string such as
36      "c:/program files/bar/baz" "arg1"
37   then it has a fit.  It seems the only way of getting it to play nicely
38   is to prefix the commandline with "call". *)
39fun system_ps s = Process.system ("call " ^ s)
40
41fun xable_string s = s^".exe"
42fun mk_xable file =
43    let val exe = file^".exe"
44        val _ = FileSys.remove exe handle _ => ()
45    in
46      FileSys.rename{old=file, new=exe};
47      OS.Process.success
48    end
49
50fun normPath s = Path.toString(Path.fromString s)
51
52fun fullPath slist =
53    normPath (List.foldl (fn (p1,p2) => Path.concat(p2,p1))
54                         (hd slist) (tl slist))
55
56  fun get_first f [] = NONE
57    | get_first f (h::t) = case f h of NONE => get_first f t
58                                     | x => x
59
60
61  fun find_my_path () = let
62    (* assumes directory hasn't been changed yet *)
63    val myname = CommandLine.name()
64    val {dir,file} = Path.splitDirFile myname
65  in
66    if dir = "" then let
67        val pathdirs = String.tokens (fn c => c = #";")
68                                     (valOf (Process.getEnv "PATH"))
69        open FileSys
70        fun checkdir d = let
71          val f = Path.concat(d,file)
72        in
73          if access(f, [A_READ, A_EXEC]) then SOME f else NONE
74        end
75      in
76        valOf (get_first checkdir pathdirs)
77      end
78    else
79      Path.mkAbsolute {path = myname, relativeTo = FileSys.getDir()}
80  end
81
82
83val HOLDIR = ""
84val MOSMLDIR = ""
85val OS = ""
86val POLY = ""
87val POLYC = ""
88val POLY_VERSION = 0
89val POLYMLLIBDIR = ""
90val POLY_LDFLAGS = []
91val POLY_LDFLAGS_STATIC = []
92val CC = ""
93val DEPDIR = ""
94val GNUMAKE = ""
95val DYNLIB = ""
96val version = ""
97val ML_SYSNAME = ""
98val release = ""
99val DOT_PATH = ""
100val DEFAULT_STATE = fullPath [HOLDIR, "bin", "hol.state"]
101
102val isUnix = false
103local val cast : 'a -> int = Obj.magic
104in
105  fun pointer_eq (x:'a, y:'a) = (cast x = cast y)
106end
107
108val build_log_dir = fullPath [HOLDIR, "tools", "build-logs"]
109val build_log_file = fullPath [build_log_dir, "current-build-log"]
110val make_log_file = "current-make-log"
111val build_after_reloc_envvar = "HOL_REBUILD_HEAPS_ONLY"
112
113local
114  fun fopen file = (FileSys.remove file handle _ => (); TextIO.openOut file)
115  fun munge s = String.translate (fn #"/" => "\\" | c => str c) s
116  fun q s = "\""^munge s^"\""
117in
118fun emit_hol_script target qend _ =
119 let val ostrm = fopen(target^".bat")
120     fun output s = TextIO.output(ostrm, s)
121     val sigobj = q (fullPath [HOLDIR, "sigobj"])
122     val std_prelude = q (fullPath [HOLDIR, "std.prelude"])
123     val mosml = q (fullPath [MOSMLDIR, "mosml"])
124 in
125    output "@echo off\n";
126    output "rem The bare HOL script\n";
127    output "rem (automatically generated by HOL configuration)\n\n";
128    output (String.concat["call ", mosml, " -P full -I ", sigobj, " ",
129                          std_prelude, " %* ", q qend, "\n"]);
130    TextIO.closeOut ostrm;
131    target
132 end
133
134
135fun emit_hol_unquote_script target qend _ =
136 let val ostrm = fopen(target^".bat")
137     fun output s = TextIO.output(ostrm, s)
138     val qfilter = q (fullPath [HOLDIR, "bin", "unquote"])
139     val sigobj = q (fullPath [HOLDIR, "sigobj"])
140     val std_prelude = q (fullPath [HOLDIR, "std.prelude"])
141     val mosml = q (fullPath [MOSMLDIR, "mosml"])
142     val qinit = q (fullPath [HOLDIR, "tools", "unquote-init.sml"])
143 in
144    output "@echo off\n";
145    output "rem The HOL script (with quote preprocessing)\n";
146    output "rem (automatically generated by HOL configuration)\n\n";
147    output  (String.concat ["call ", qfilter, " | ", mosml,
148                          " -P full -I ", sigobj, " ",
149                            std_prelude, " ", qinit, " %* ",
150                            q qend, "\n"]);
151    TextIO.closeOut ostrm;
152    target
153 end
154end (* local *)
155
156fun quietbind s = ()
157fun bindstr s = s
158
159end; (* struct *)
160