1.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Mar 23 11:39:21 2010 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Mar 23 11:40:46 2010 +0100
1.3 @@ -24,6 +24,8 @@
1.4 open Nitpick_Nut
1.5 open Nitpick
1.6
1.7 +structure K = OuterKeyword and P = OuterParse
1.8 +
1.9 val auto = Unsynchronized.ref false;
1.10
1.11 val _ =
1.12 @@ -34,48 +36,48 @@
1.13 type raw_param = string * string list
1.14
1.15 val default_default_params =
1.16 - [("card", ["1\<midarrow>8"]),
1.17 - ("iter", ["0,1,2,4,8,12,16,24"]),
1.18 - ("bits", ["1,2,3,4,6,8,10,12"]),
1.19 - ("bisim_depth", ["7"]),
1.20 - ("box", ["smart"]),
1.21 - ("finitize", ["smart"]),
1.22 - ("mono", ["smart"]),
1.23 - ("std", ["true"]),
1.24 - ("wf", ["smart"]),
1.25 - ("sat_solver", ["smart"]),
1.26 - ("batch_size", ["smart"]),
1.27 - ("blocking", ["true"]),
1.28 - ("falsify", ["true"]),
1.29 - ("user_axioms", ["smart"]),
1.30 - ("assms", ["true"]),
1.31 - ("merge_type_vars", ["false"]),
1.32 - ("binary_ints", ["smart"]),
1.33 - ("destroy_constrs", ["true"]),
1.34 - ("specialize", ["true"]),
1.35 - ("skolemize", ["true"]),
1.36 - ("star_linear_preds", ["true"]),
1.37 - ("uncurry", ["true"]),
1.38 - ("fast_descrs", ["true"]),
1.39 - ("peephole_optim", ["true"]),
1.40 - ("timeout", ["30 s"]),
1.41 - ("tac_timeout", ["500 ms"]),
1.42 - ("sym_break", ["20"]),
1.43 - ("sharing_depth", ["3"]),
1.44 - ("flatten_props", ["false"]),
1.45 - ("max_threads", ["0"]),
1.46 - ("verbose", ["false"]),
1.47 - ("debug", ["false"]),
1.48 - ("overlord", ["false"]),
1.49 - ("show_all", ["false"]),
1.50 - ("show_skolems", ["true"]),
1.51 - ("show_datatypes", ["false"]),
1.52 - ("show_consts", ["false"]),
1.53 - ("format", ["1"]),
1.54 - ("max_potential", ["1"]),
1.55 - ("max_genuine", ["1"]),
1.56 - ("check_potential", ["false"]),
1.57 - ("check_genuine", ["false"])]
1.58 + [("card", "1\<midarrow>8"),
1.59 + ("iter", "0,1,2,4,8,12,16,24"),
1.60 + ("bits", "1,2,3,4,6,8,10,12"),
1.61 + ("bisim_depth", "7"),
1.62 + ("box", "smart"),
1.63 + ("finitize", "smart"),
1.64 + ("mono", "smart"),
1.65 + ("std", "true"),
1.66 + ("wf", "smart"),
1.67 + ("sat_solver", "smart"),
1.68 + ("batch_size", "smart"),
1.69 + ("blocking", "true"),
1.70 + ("falsify", "true"),
1.71 + ("user_axioms", "smart"),
1.72 + ("assms", "true"),
1.73 + ("merge_type_vars", "false"),
1.74 + ("binary_ints", "smart"),
1.75 + ("destroy_constrs", "true"),
1.76 + ("specialize", "true"),
1.77 + ("skolemize", "true"),
1.78 + ("star_linear_preds", "true"),
1.79 + ("uncurry", "true"),
1.80 + ("fast_descrs", "true"),
1.81 + ("peephole_optim", "true"),
1.82 + ("timeout", "30 s"),
1.83 + ("tac_timeout", "500 ms"),
1.84 + ("sym_break", "20"),
1.85 + ("sharing_depth", "3"),
1.86 + ("flatten_props", "false"),
1.87 + ("max_threads", "0"),
1.88 + ("debug", "false"),
1.89 + ("verbose", "false"),
1.90 + ("overlord", "false"),
1.91 + ("show_all", "false"),
1.92 + ("show_skolems", "true"),
1.93 + ("show_datatypes", "false"),
1.94 + ("show_consts", "false"),
1.95 + ("format", "1"),
1.96 + ("max_potential", "1"),
1.97 + ("max_genuine", "1"),
1.98 + ("check_potential", "false"),
1.99 + ("check_genuine", "false")]
1.100
1.101 val negated_params =
1.102 [("dont_box", "box"),
1.103 @@ -97,8 +99,8 @@
1.104 ("full_descrs", "fast_descrs"),
1.105 ("no_peephole_optim", "peephole_optim"),
1.106 ("dont_flatten_props", "flatten_props"),
1.107 + ("no_debug", "debug"),
1.108 ("quiet", "verbose"),
1.109 - ("no_debug", "debug"),
1.110 ("no_overlord", "overlord"),
1.111 ("dont_show_all", "show_all"),
1.112 ("hide_skolems", "show_skolems"),
1.113 @@ -119,7 +121,7 @@
1.114 (* string * 'a -> unit *)
1.115 fun check_raw_param (s, _) =
1.116 if is_known_raw_param s then ()
1.117 - else error ("Unknown parameter " ^ quote s ^ ".")
1.118 + else error ("Unknown parameter: " ^ quote s ^ ".")
1.119
1.120 (* string -> string option *)
1.121 fun unnegate_param_name name =
1.122 @@ -139,20 +141,15 @@
1.123 | NONE => (name, value)
1.124
1.125 structure Data = Theory_Data(
1.126 - type T = {params: raw_param list}
1.127 - val empty = {params = rev default_default_params}
1.128 + type T = raw_param list
1.129 + val empty = default_default_params |> map (apsnd single)
1.130 val extend = I
1.131 - fun merge ({params = ps1}, {params = ps2}) : T =
1.132 - {params = AList.merge (op =) (K true) (ps1, ps2)})
1.133 + fun merge p : T = AList.merge (op =) (K true) p)
1.134
1.135 (* raw_param -> theory -> theory *)
1.136 -fun set_default_raw_param param thy =
1.137 - let val {params} = Data.get thy in
1.138 - Data.put {params = AList.update (op =) (unnegate_raw_param param) params}
1.139 - thy
1.140 - end
1.141 +val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
1.142 (* theory -> raw_param list *)
1.143 -val default_raw_params = #params o Data.get
1.144 +val default_raw_params = Data.get
1.145
1.146 (* string -> bool *)
1.147 fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
1.148 @@ -164,26 +161,6 @@
1.149 s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^
1.150 stringify_raw_param_value (s2 :: ss)
1.151
1.152 -(* bool -> string -> string -> bool option *)
1.153 -fun bool_option_from_string option name s =
1.154 - (case s of
1.155 - "smart" => if option then NONE else raise Option
1.156 - | "false" => SOME false
1.157 - | "true" => SOME true
1.158 - | "" => SOME true
1.159 - | _ => raise Option)
1.160 - handle Option.Option =>
1.161 - let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
1.162 - error ("Parameter " ^ quote name ^ " must be assigned " ^
1.163 - space_implode " " (serial_commas "or" ss) ^ ".")
1.164 - end
1.165 -(* bool -> raw_param list -> bool option -> string -> bool option *)
1.166 -fun general_lookup_bool option raw_params default_value name =
1.167 - case AList.lookup (op =) raw_params name of
1.168 - SOME s => s |> stringify_raw_param_value
1.169 - |> bool_option_from_string option name
1.170 - | NONE => default_value
1.171 -
1.172 (* int -> string -> int *)
1.173 fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))
1.174
1.175 @@ -192,14 +169,20 @@
1.176 let
1.177 val override_params = map unnegate_raw_param override_params
1.178 val raw_params = rev override_params @ rev default_params
1.179 + (* string -> string *)
1.180 val lookup =
1.181 Option.map stringify_raw_param_value o AList.lookup (op =) raw_params
1.182 - (* string -> string *)
1.183 - fun lookup_string name = the_default "" (lookup name)
1.184 + val lookup_string = the_default "" o lookup
1.185 + (* bool -> bool option -> string -> bool option *)
1.186 + fun general_lookup_bool option default_value name =
1.187 + case lookup name of
1.188 + SOME s => s |> stringify_raw_param_value
1.189 + |> Sledgehammer_Util.parse_bool_option option name
1.190 + | NONE => default_value
1.191 (* string -> bool *)
1.192 - val lookup_bool = the o general_lookup_bool false raw_params (SOME false)
1.193 + val lookup_bool = the o general_lookup_bool false (SOME false)
1.194 (* string -> bool option *)
1.195 - val lookup_bool_option = general_lookup_bool true raw_params NONE
1.196 + val lookup_bool_option = general_lookup_bool true NONE
1.197 (* string -> string option -> int *)
1.198 fun do_int name value =
1.199 case value of
1.200 @@ -253,7 +236,8 @@
1.201 :: map (fn (name, value) =>
1.202 (SOME (read (String.extract (name, size prefix + 1, NONE))),
1.203 value |> stringify_raw_param_value
1.204 - |> bool_option_from_string false name |> the))
1.205 + |> Sledgehammer_Util.parse_bool_option false name
1.206 + |> the))
1.207 (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
1.208 (* (string -> 'a) -> string -> ('a option * bool option) list *)
1.209 fun lookup_bool_option_assigns read prefix =
1.210 @@ -261,28 +245,13 @@
1.211 :: map (fn (name, value) =>
1.212 (SOME (read (String.extract (name, size prefix + 1, NONE))),
1.213 value |> stringify_raw_param_value
1.214 - |> bool_option_from_string true name))
1.215 + |> Sledgehammer_Util.parse_bool_option true name))
1.216 (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
1.217 (* string -> Time.time option *)
1.218 fun lookup_time name =
1.219 case lookup name of
1.220 NONE => NONE
1.221 - | SOME "none" => NONE
1.222 - | SOME s =>
1.223 - let
1.224 - val msecs =
1.225 - case space_explode " " s of
1.226 - [s1, "min"] => 60000 * the (Int.fromString s1)
1.227 - | [s1, "s"] => 1000 * the (Int.fromString s1)
1.228 - | [s1, "ms"] => the (Int.fromString s1)
1.229 - | _ => 0
1.230 - in
1.231 - if msecs <= 0 then
1.232 - error ("Parameter " ^ quote name ^ " must be assigned a positive \
1.233 - \time value (e.g., \"60 s\", \"200 ms\") or \"none\".")
1.234 - else
1.235 - SOME (Time.fromMilliseconds msecs)
1.236 - end
1.237 + | SOME s => Sledgehammer_Util.parse_time_option name s
1.238 (* string -> term list *)
1.239 val lookup_term_list =
1.240 AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt
1.241 @@ -368,22 +337,18 @@
1.242 extract_params (ProofContext.init thy) false (default_raw_params thy)
1.243 o map (apsnd single)
1.244
1.245 -(* OuterParse.token list -> string * OuterParse.token list *)
1.246 -val scan_key = Scan.repeat1 OuterParse.typ_group >> space_implode " "
1.247 -
1.248 -(* OuterParse.token list -> string list * OuterParse.token list *)
1.249 -val scan_value =
1.250 - Scan.repeat1 (OuterParse.minus >> single
1.251 - || Scan.repeat1 (Scan.unless OuterParse.minus OuterParse.name)
1.252 - || OuterParse.$$$ "," |-- OuterParse.number >> prefix ","
1.253 - >> single) >> flat
1.254 -
1.255 -(* OuterParse.token list -> raw_param * OuterParse.token list *)
1.256 -val scan_param =
1.257 - scan_key -- (Scan.option (OuterParse.$$$ "=" |-- scan_value) >> these)
1.258 -(* OuterParse.token list -> raw_param list option * OuterParse.token list *)
1.259 -val scan_params = Scan.option (OuterParse.$$$ "[" |-- OuterParse.list scan_param
1.260 - --| OuterParse.$$$ "]")
1.261 +(* P.token list -> string * P.token list *)
1.262 +val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
1.263 +(* P.token list -> string list * P.token list *)
1.264 +val parse_value =
1.265 + Scan.repeat1 (P.minus >> single
1.266 + || Scan.repeat1 (Scan.unless P.minus P.name)
1.267 + || P.$$$ "," |-- P.number >> prefix "," >> single) >> flat
1.268 +(* P.token list -> raw_param * P.token list *)
1.269 +val parse_param =
1.270 + parse_key -- (Scan.option (P.$$$ "=" |-- parse_value) >> these)
1.271 +(* P.token list -> raw_param list option * P.token list *)
1.272 +val parse_params = Scan.option (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]")
1.273
1.274 (* Proof.context -> ('a -> 'a) -> 'a -> 'a *)
1.275 fun handle_exceptions ctxt f x =
1.276 @@ -423,7 +388,6 @@
1.277 | Refute.REFUTE (loc, details) =>
1.278 error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
1.279
1.280 -
1.281 (* raw_param list -> bool -> int -> int -> Proof.state -> bool * Proof.state *)
1.282 fun pick_nits override_params auto i step state =
1.283 let
1.284 @@ -469,18 +433,18 @@
1.285 params |> map string_for_raw_param
1.286 |> sort_strings |> cat_lines)))))
1.287
1.288 -(* OuterParse.token list
1.289 - -> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
1.290 -val scan_nitpick_command =
1.291 - (scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans
1.292 -val scan_nitpick_params_command = scan_params #>> nitpick_params_trans
1.293 +(* P.token list
1.294 + -> (Toplevel.transition -> Toplevel.transition) * P.token list *)
1.295 +val parse_nitpick_command =
1.296 + (parse_params -- Scan.option P.nat) #>> nitpick_trans
1.297 +val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
1.298
1.299 val _ = OuterSyntax.improper_command "nitpick"
1.300 "try to find a counterexample for a given subgoal using Kodkod"
1.301 - OuterKeyword.diag scan_nitpick_command
1.302 + K.diag parse_nitpick_command
1.303 val _ = OuterSyntax.command "nitpick_params"
1.304 "set and display the default parameters for Nitpick"
1.305 - OuterKeyword.thy_decl scan_nitpick_params_command
1.306 + K.thy_decl parse_nitpick_params_command
1.307
1.308 (* Proof.state -> bool * Proof.state *)
1.309 fun auto_nitpick state =