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