1structure HM_Cline :> HM_Cline =
2struct
3
4type t = {
5  holstate : string option,
6  multithread : int option,
7  poly : string option,
8  polymllibdir : string option,
9  poly_not_hol : bool,
10  time_limit : Time.time option,
11  relocbuild : bool,
12  core : HM_Core_Cline.t
13}
14
15local
16  open FunctionalRecordUpdate
17  fun makeUpdateT z = makeUpdate8 z
18in
19fun updateT z = let
20  fun from core holstate multithread poly polymllibdir poly_not_hol relocbuild
21           time_limit =
22    {core = core, holstate = holstate, multithread = multithread, poly = poly,
23     polymllibdir = polymllibdir, poly_not_hol = poly_not_hol,
24     relocbuild = relocbuild, time_limit = time_limit}
25  fun from' time_limit relocbuild poly_not_hol polymllibdir poly multithread
26            holstate core =
27    {core = core, holstate = holstate, multithread = multithread, poly = poly,
28     polymllibdir = polymllibdir, poly_not_hol = poly_not_hol,
29     relocbuild = relocbuild, time_limit = time_limit}
30  fun to f {core, holstate, multithread, poly, polymllibdir, poly_not_hol,
31            relocbuild, time_limit} =
32    f core holstate multithread poly polymllibdir poly_not_hol relocbuild
33      time_limit
34in
35  makeUpdateT (from, from', to)
36end z
37val U = U
38val $$ = $$
39end (* local *)
40
41fun fupd_core f t = updateT t (U #core (f (#core t))) $$
42val default_options = {
43  core = HM_Core_Cline.default_core_options,
44  holstate = NONE,
45  multithread = NONE,
46  poly = NONE,
47  polymllibdir = NONE,
48  poly_not_hol = false,
49  relocbuild = false,
50  time_limit = NONE
51}
52
53fun fupdcore f x =
54  let
55    val {update = u, hmakefile, no_hmf} = f x
56  in
57    {update = fn (wn, t : t) => updateT t (U #core (u (wn, #core t))) $$,
58     hmakefile = hmakefile, no_hmf = no_hmf}
59  end
60
61open GetOpt
62
63type core_t = HM_Core_Cline.t
64type 'a cline_result = 'a HM_Core_Cline.cline_result
65type 'a arg_descr = 'a GetOpt.arg_descr
66
67fun resfn f : t cline_result = {update = f, hmakefile = NONE, no_hmf = false}
68
69fun set_poly s =
70  resfn (fn (wn, t : t) =>
71            (if isSome (#poly t) then
72               wn ("Poly executable already set; ignoring earlier spec")
73             else ();
74             updateT t (U #poly (SOME s)) $$))
75fun set_polymllibdir s =
76  resfn (fn (wn, t : t) =>
77            (if isSome (#polymllibdir t) then
78               wn ("Poly/ML lib directory already set; ignoring earlier spec")
79             else ();
80             updateT t (U #polymllibdir (SOME s)) $$))
81fun set_holstate s =
82  resfn (fn (wn, t : t) =>
83            (if isSome (#holstate t) then
84               wn ("HOL state-file already set; ignoring earlier spec")
85             else ();
86             updateT t (U #holstate (SOME s)) $$))
87fun set_time_limit s =
88  resfn (fn (wn, t : t) =>
89            case LargeInt.fromString s of
90                NONE => (wn ("Bad time string: \""^s^"\"; ignored"); t)
91              | SOME i => updateT t
92                                  (U #time_limit (SOME (Time.fromSeconds i)))
93                                  $$)
94
95fun mt_optint sopt =
96  let
97    fun set i =
98      resfn (fn (wn, t : t) =>
99                (if isSome (#multithread t) then
100                   wn ("Multithread count already set; ignoring earlier count")
101                 else ();
102                 updateT t (U #multithread (SOME i)) $$))
103  in
104    case sopt of
105        NONE => set 0
106      | SOME s =>
107        (case Int.fromString s of
108             SOME i => set i
109           | NONE => resfn
110                       (fn (wn, t:t) =>
111                           (wn ("Bad count for multithread; ignoring it");
112                            t)))
113  end
114
115val poly_option_descriptions = [
116  {help = "specify HOL state", long = ["holstate"], short = "",
117   desc = ReqArg (set_holstate, "holstate")},
118  {help = "thread count (0/none = max h/w count)", short = "",
119   long = ["mt"], desc = OptArg (mt_optint, "c")},
120  {help = "specify Poly executable", long = ["poly"], short = "",
121   desc = ReqArg (set_poly, "executable")},
122  {help = "use poly rather than a HOL heap", long = ["poly_not_hol"],
123   short = "",
124   desc = NoArg (fn () =>
125                    resfn (fn (wn,t) => updateT t (U #poly_not_hol true) $$))},
126  {help = "perform a relocation build", long = ["relocbuild"], short = "",
127   desc = NoArg (fn () =>
128                    resfn (fn (_,t) => updateT t (U #relocbuild true) $$))},
129  {help = "specify Poly/ML lib directory", long = ["polymllibdir"],
130   short = "",
131   desc = ReqArg (set_polymllibdir, "directory")},
132  {help = "set time limit (in seconds)", long = ["time_limit"], short = "t",
133   desc = ReqArg (set_time_limit, "delay")}
134]
135
136fun mapd (d : core_t cline_result arg_descr) : t cline_result arg_descr =
137  case d of
138      NoArg f => NoArg(fupdcore f)
139    | ReqArg (f, s) => ReqArg (fupdcore f, s)
140    | OptArg (f, s) => OptArg (fupdcore f, s)
141
142val option_descriptions =
143    HM_Core_Cline.sort_descriptions
144      (map (fn {desc,help,short,long} =>
145               {desc = mapd desc, help = help, long = long, short = short})
146           HM_Core_Cline.core_option_descriptions @
147       poly_option_descriptions)
148
149end
150