1structure HM_Core_Cline :> HM_Core_Cline =
2struct
3
4local
5  open FunctionalRecordUpdate
6  fun makeUpdateT z = makeUpdate22 z
7in
8fun updateT z = let
9  fun from debug do_logging fast help hmakefile holdir includes
10           interactive jobs keep_going no_action no_hmakefile no_lastmaker_check
11           no_overlay
12           no_prereqs opentheory quiet
13           quit_on_failure rebuild_deps recursive_build recursive_clean
14           verbose =
15    {
16      debug = debug, do_logging = do_logging,
17      fast = fast, help = help, hmakefile = hmakefile, holdir = holdir,
18      includes = includes, interactive = interactive, jobs = jobs,
19      keep_going = keep_going,
20      no_action = no_action, no_hmakefile = no_hmakefile,
21      no_lastmaker_check = no_lastmaker_check, no_overlay = no_overlay,
22      no_prereqs = no_prereqs, opentheory = opentheory,
23      quiet = quiet, quit_on_failure = quit_on_failure,
24      rebuild_deps = rebuild_deps, recursive_build = recursive_build,
25      recursive_clean = recursive_clean, verbose = verbose
26    }
27  fun from' verbose recursive_clean recursive_build rebuild_deps quit_on_failure
28            quiet opentheory
29            no_prereqs
30            no_overlay no_lastmaker_check no_hmakefile no_action keep_going
31            jobs interactive
32            includes holdir
33            hmakefile help fast do_logging debug =
34    {
35      debug = debug, do_logging = do_logging,
36      fast = fast, help = help, hmakefile = hmakefile, holdir = holdir,
37      includes = includes, interactive = interactive, jobs = jobs,
38      keep_going = keep_going,
39      no_action = no_action, no_hmakefile = no_hmakefile,
40      no_lastmaker_check = no_lastmaker_check, no_overlay = no_overlay,
41      no_prereqs = no_prereqs, opentheory = opentheory,
42      quiet = quiet, quit_on_failure = quit_on_failure,
43      rebuild_deps = rebuild_deps, recursive_build = recursive_build,
44      recursive_clean = recursive_clean, verbose = verbose
45    }
46  fun to f {debug, do_logging, fast, help, hmakefile, holdir,
47            includes, interactive, jobs, keep_going, no_action, no_hmakefile,
48            no_lastmaker_check,
49            no_overlay, no_prereqs, opentheory,
50            quiet, quit_on_failure, rebuild_deps, recursive_build,
51            recursive_clean, verbose} =
52    f debug do_logging fast help hmakefile holdir includes
53      interactive jobs keep_going no_action no_hmakefile no_lastmaker_check
54      no_overlay
55      no_prereqs opentheory quiet
56      quit_on_failure rebuild_deps recursive_build recursive_clean verbose
57in
58  makeUpdateT (from, from', to)
59end z
60val U = U
61val $$ = $$
62end (* local *)
63
64fun fupd_jobs f t = updateT t (U #jobs (f (#jobs t))) $$
65fun fupd_includes f t = updateT t (U #includes (f (#includes t))) $$
66
67type t = {
68  debug : {ins : string list, outs : string list} option,
69  do_logging : bool,
70  fast : bool,
71  help : bool,
72  hmakefile : string option,
73  holdir : string option,
74  includes : string list,
75  interactive : bool,
76  jobs : int,
77  keep_going : bool,
78  no_action : bool,
79  no_hmakefile : bool,
80  no_lastmaker_check : bool,
81  no_overlay : bool,
82  no_prereqs : bool,
83  opentheory : string option,
84  quiet : bool,
85  quit_on_failure : bool,
86  rebuild_deps : bool,
87  recursive_build : bool,
88  recursive_clean : bool,
89  verbose : bool
90}
91
92val default_core_options : t =
93{
94  debug = NONE,
95  do_logging = false,
96  fast = false,
97  help = false,
98  hmakefile = NONE,
99  holdir = NONE,
100  includes = [],
101  interactive = false,
102  jobs = 4,
103  keep_going = false,
104  no_action = false,
105  no_hmakefile = false,
106  no_lastmaker_check = false,
107  no_overlay = false,
108  no_prereqs = false,
109  opentheory = NONE,
110  quiet = false,
111  quit_on_failure = true,
112  rebuild_deps = false,
113  recursive_build = false,
114  recursive_clean = false,
115  verbose = false
116}
117
118type 'a cline_result =
119     { update: (string -> unit) * 'a -> 'a,
120       hmakefile : string option,
121       no_hmf : bool }
122
123fun resfn f : t cline_result = {update = f, hmakefile = NONE, no_hmf = false}
124
125open GetOpt
126val setNOHMF =
127    NoArg (fn () => {update = fn (wn,t) => updateT t (U #no_hmakefile true) $$,
128                     hmakefile = NONE, no_hmf = true})
129fun mkBoolT sel =
130  NoArg (fn () => resfn (fn (wn,t) => updateT t (U sel true) $$))
131fun mkBoolF sel =
132  NoArg (fn () => resfn (fn (wn,t) => updateT t (U sel false) $$))
133fun cons_includes x =
134  resfn (fn (wn,t) => updateT t (U #includes (x :: #includes t)) $$)
135fun change_jobs nstr =
136  resfn (fn (wn,t) =>
137            case Int.fromString nstr of
138                NONE => (wn ("Couldn't parse "^nstr^
139                             " as a number; ignoring it"); t)
140              | SOME n => if n < 1 then
141                            (wn "Ignoring non-positive job count"; t)
142                          else updateT t (U #jobs n) $$)
143
144fun set_hmakefile s =
145  { update = fn (wn,t) =>
146                (if isSome (#hmakefile t) then
147                   wn "Multiple Holmakefile specs; ignoring earlier spec"
148                 else ();
149                 updateT t (U #hmakefile (SOME s)) $$),
150    hmakefile = SOME s, no_hmf = false }
151fun set_holdir s =
152  resfn (fn (wn, t) =>
153            (if isSome (#holdir t) then
154               wn "Multiple holdir specs; ignoring earlier spec"
155             else ();
156             updateT t (U #holdir (SOME s)) $$))
157fun set_openthy s =
158  resfn (fn (wn, t) =>
159            (if isSome (#opentheory t) then
160               wn "Multiple opentheory specs; ignoring earlier spec"
161             else ();
162             updateT t (U #opentheory (SOME s)) $$))
163fun addDbg sopt =
164    resfn (fn (wn, t) =>
165              let
166                fun process (x as {ins,outs}) sopt =
167                    case sopt of
168                        NONE => SOME x
169                      | SOME s =>
170                        if String.sub(s,0) = #"-" then
171                          if size s > 1 then
172                            SOME{ins=ins,
173                                 outs = String.extract(s,1,NONE) :: outs}
174                          else (wn "Ignoring bogus -d- option"; SOME x)
175                        else
176                          SOME{ins = s::ins, outs = outs}
177                val newvalue =
178                    case #debug t of
179                        NONE => process {ins=[],outs=[]} sopt
180                      | SOME x => process x sopt
181              in
182                updateT t (U #debug newvalue) $$
183              end)
184
185val core_option_descriptions = [
186  { help = "turn on diagnostic messages", long = ["dbg"], short = "d",
187    desc = OptArg (addDbg, "diag-cat")},
188  { help = "fast build (replace tactics w/cheat)", long = ["fast"], short = "",
189    desc = mkBoolT #fast },
190  { help = "show this message", long = ["help"], short = "h",
191    desc = mkBoolT #help },
192  { help = "use different HOLDIR", long = ["holdir"], short = "",
193    desc = ReqArg (set_holdir, "directory") },
194  { help = "use different holmakefile", long = ["holmakefile"], short = "",
195    desc = ReqArg (set_hmakefile, "file") },
196  { help = "make session 'interactive'", long = ["interactive"], short = "i",
197    desc = mkBoolT #interactive },
198  { help = "include directory", long = [], short = "I",
199    desc = ReqArg (cons_includes, "directory") },
200  { help = "max number of parallel jobs", long = ["jobs"], short = "j",
201    desc = ReqArg (change_jobs, "n") },
202  { help = "try to build all targets", long = ["keep-going"], short = "k",
203    desc = mkBoolT #keep_going },
204  { help = "enable time logging", long = ["logging"], short = "",
205    desc = mkBoolT #do_logging },
206  { help = "print what would be executed", long = ["no_action"], short = "n",
207    desc = mkBoolT #no_action },
208  { help = "don't use a Holmakefile", long = ["no_hmakefile"], short = "",
209    desc = setNOHMF },
210  { help = "don't check which Holmake was last used", long = ["nolmbc"],
211    short = "", desc = mkBoolT #no_lastmaker_check },
212  { help = "don't use Overlay.sml file", long = ["no_overlay"],
213    short = "", desc = mkBoolT #no_overlay },
214  { help = "don't build recursively in INCLUDES",
215    long = ["no_prereqs"], short = "", desc = mkBoolT #no_prereqs },
216  { help = "don't quit on failure", long = ["noqof"], short = "",
217    desc = mkBoolF #quit_on_failure },
218  { help = "use file as opentheory logging .uo",
219    long = ["ot"], short = "", desc = ReqArg (set_openthy, "file")},
220  { help = "be quieter with output", short = "q", long = ["quiet"],
221    desc = NoArg
222             (fn () =>
223                 resfn (fn (wn,t) =>
224                           (if #verbose t then
225                              wn "Quiet and verbose incompatible; \
226                                 \taking verbose"
227                            else () ;
228                            updateT t (U #quiet true) $$))) },
229  { help = "quit on failure", short = "", long = ["qof"],
230    desc = mkBoolT #quit_on_failure },
231  { help = "rebuild cached dependency files", short = "",
232    long = ["rebuild_deps"], desc = mkBoolT #rebuild_deps },
233  { help = "both --recursive-{build,clean}", short = "r", long = [],
234    desc = NoArg (
235      fn () => resfn (
236                fn (wn,t) => updateT t
237                                     (U #recursive_build true)
238                                     (U #recursive_clean true) $$
239              )
240    )},
241  { help = "build all targets recursively", short = "",
242    long = ["recursive-build"], desc = mkBoolT #recursive_build},
243  { help = "clean recursively", short = "",
244    long = ["recursive-clean"], desc = mkBoolT #recursive_clean},
245  { help = "verbose output", short = "v", long = ["verbose"],
246    desc = NoArg
247             (fn () =>
248                 resfn (fn (wn,t) =>
249                           (if #quiet t then
250                              wn "Quiet and verbose incompatible; \
251                                 \taking verbose"
252                            else ();
253                            updateT t (U #verbose true) $$))) }
254]
255
256fun descr_key (d:'a GetOpt.opt_descr) =
257  str (String.sub(#short d, 0))
258  handle Subscript => hd (#long d) handle Empty => ""
259
260fun descr_compare (d1, d2) = String.compare(descr_key d1, descr_key d2)
261
262fun sort_descriptions dl = Listsort.sort descr_compare dl
263
264
265end
266