diff -r 14571c9e1d50 -r 6273d4c8325b src/HOL/Nunchaku/Tools/nunchaku_commands.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Nunchaku/Tools/nunchaku_commands.ML Mon Oct 24 22:42:07 2016 +0200 @@ -0,0 +1,258 @@ +(* Title: HOL/Nunchaku/Tools/nunchaku_commands.ML + Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII + Copyright 2015, 2016 + +Adds the "nunchaku" and "nunchaku_params" commands to Isabelle/Isar's outer syntax. +*) + +signature NUNCHAKU_COMMANDS = +sig + type params = Nunchaku.params + + val default_params: theory -> (string * string) list -> params +end; + +structure Nunchaku_Commands : NUNCHAKU_COMMANDS = +struct + +open Nunchaku_Util; +open Nunchaku; + +type raw_param = string * string list; + +val default_default_params = + [("assms", "true"), + ("debug", "false"), + ("falsify", "true"), + ("max_genuine", "1"), + ("max_potential", "1"), + ("overlord", "false"), + ("specialize", "true"), + ("spy", "false"), + ("timeout", "30"), + ("verbose", "false"), + ("wf_timeout", "0.5")]; + +val negated_params = + [("dont_whack", "whack"), + ("dont_specialize", "specialize"), + ("dont_spy", "spy"), + ("no_assms", "assms"), + ("no_debug", "debug"), + ("no_overlord", "overlord"), + ("non_mono", "mono"), + ("non_wf", "wf"), + ("quiet", "verbose"), + ("satisfy", "falsify")]; + +fun is_known_raw_param s = + AList.defined (op =) default_default_params s orelse + AList.defined (op =) negated_params s orelse + member (op =) ["atoms", "card", "eval", "expect"] s orelse + exists (fn p => String.isPrefix (p ^ " ") s) + ["atoms", "card", "dont_whack", "mono", "non_mono", "non_wf", "wf", "whack"]; + +fun check_raw_param (s, _) = + if is_known_raw_param s then () else error ("Unknown parameter: " ^ quote s); + +fun unnegate_param_name name = + (case AList.lookup (op =) negated_params name of + NONE => + if String.isPrefix "dont_" name then SOME (unprefix "dont_" name) + else if String.isPrefix "non_" name then SOME (unprefix "non_" name) + else NONE + | some_name => some_name); + +fun normalize_raw_param (name, value) = + (case unnegate_param_name name of + SOME name' => + [(name', + (case value of + ["false"] => ["true"] + | ["true"] => ["false"] + | [] => ["false"] + | _ => value))] + | NONE => [(name, value)]); + +structure Data = Theory_Data +( + type T = raw_param list + val empty = default_default_params |> map (apsnd single) + val extend = I + fun merge data = AList.merge (op =) (K true) data +); + +val set_default_raw_param = Data.map o fold (AList.update (op =)) o normalize_raw_param; +val default_raw_params = Data.get; + +fun is_punctuation s = (s = "," orelse s = "-"); + +fun stringify_raw_param_value [] = "" + | stringify_raw_param_value [s] = s + | stringify_raw_param_value (s1 :: s2 :: ss) = + s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^ + stringify_raw_param_value (s2 :: ss); + +fun extract_params ctxt mode default_params override_params = + let + val override_params = maps normalize_raw_param override_params; + val raw_params = rev override_params @ rev default_params; + val raw_lookup = AList.lookup (op =) raw_params; + val lookup = Option.map stringify_raw_param_value o raw_lookup; + val lookup_string = the_default "" o lookup; + + fun general_lookup_bool option default_value name = + (case lookup name of + SOME s => parse_bool_option option name s + | NONE => default_value); + + val lookup_bool = the o general_lookup_bool false (SOME false); + + fun lookup_int name = + (case lookup name of + SOME s => + (case Int.fromString s of + SOME i => i + | NONE => error ("Parameter " ^ quote name ^ " must be assigned an integer value")) + | NONE => 0); + + fun int_range_from_string name s = + (case space_explode "-" s of + [s] => (s, s) + | [s1, s2] => (s1, s2) + | _ => error ("Parameter " ^ quote name ^ " must be assigned a range of integers")) + |> apply2 Int.fromString; + + fun lookup_assigns read pre of_str = + (case lookup pre of + SOME s => [(NONE, of_str s)] + | NONE => []) @ + map (fn (name, value) => (SOME (read (String.extract (name, size pre + 1, NONE))), + of_str (stringify_raw_param_value value))) + (filter (String.isPrefix (pre ^ " ") o fst) raw_params); + + fun lookup_int_range_assigns read pre = + lookup_assigns read pre (int_range_from_string pre); + + fun lookup_bool_assigns read pre = + lookup_assigns read pre (the o parse_bool_option false pre); + + fun lookup_bool_option_assigns read pre = + lookup_assigns read pre (parse_bool_option true pre); + + fun lookup_strings_assigns read pre = + lookup_assigns read pre (space_explode " "); + + fun lookup_time name = + (case lookup name of + SOME s => parse_time name s + | NONE => Time.zeroTime); + + val read_type_polymorphic = + Syntax.read_typ ctxt #> Logic.mk_type + #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type; + val read_term_polymorphic = + Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt); + val lookup_term_list_option_polymorphic = + AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic); + + fun read_const_polymorphic s = + (case read_term_polymorphic s of + Const x => x + | t => error ("Not a constant: " ^ Syntax.string_of_term ctxt t)); + + val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"; + val whacks = lookup_bool_assigns read_term_polymorphic "whack"; + val cards = lookup_int_range_assigns read_type_polymorphic "card"; + val monos = lookup_bool_option_assigns read_type_polymorphic "mono"; + val falsify = lookup_bool "falsify"; + val debug = (mode <> Auto_Try andalso lookup_bool "debug"); + val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose"); + val overlord = lookup_bool "overlord"; + val spy = getenv "NUNCHAKU_SPY" = "yes" orelse lookup_bool "spy"; + val assms = lookup_bool "assms"; + val specialize = lookup_bool "specialize"; + val timeout = lookup_time "timeout"; + val wf_timeout = lookup_time "wf_timeout"; + val multithread = mode = Normal andalso lookup_bool "multithread"; + val evals = these (lookup_term_list_option_polymorphic "eval"); + val atomss = lookup_strings_assigns read_type_polymorphic "atoms"; + val max_potential = if mode = Normal then Int.max (0, lookup_int "max_potential") else 0; + val max_genuine = Int.max (0, lookup_int "max_genuine"); + val expect = lookup_string "expect"; + + val mode_of_operation_params = + {falsify = falsify, assms = assms, spy = spy, overlord = overlord, + expect = expect}; + + val scope_of_search_params = + {wfs = wfs, whacks = whacks, cards = cards, monos = monos}; + + val output_format_params = + {verbose = verbose, debug = debug, max_potential = max_potential, max_genuine = max_genuine, + evals = evals, atomss = atomss}; + + val optimization_params = + {specialize = specialize, multithread = multithread}; + + val timeout_params = + {timeout = timeout, wf_timeout = wf_timeout}; + in + {mode_of_operation_params = mode_of_operation_params, + scope_of_search_params = scope_of_search_params, + output_format_params = output_format_params, + optimization_params = optimization_params, + timeout_params = timeout_params} + end; + +fun default_params thy = + extract_params (Proof_Context.init_global thy) Normal (default_raw_params thy) + o map (apsnd single); + +val parse_key = Scan.repeat1 Parse.embedded >> space_implode " "; +val parse_value = + Scan.repeat1 (Parse.minus >> single + || Scan.repeat1 (Scan.unless Parse.minus (Parse.name || Parse.float_number)) + || @{keyword ","} |-- Parse.number >> prefix "," >> single) + >> flat; +val parse_param = parse_key -- Scan.optional (@{keyword "="} |-- parse_value) []; +val parse_params = Scan.optional (@{keyword "["} |-- Parse.list parse_param --| @{keyword "]"}) []; + +fun run_chaku override_params mode i state0 = + let + val state = Proof.map_contexts (Try0.silence_methods false) state0; + val thy = Proof.theory_of state; + val ctxt = Proof.context_of state; + val _ = List.app check_raw_param override_params; + val params = extract_params ctxt mode (default_raw_params thy) override_params; + in + (if mode = Auto_Try then perhaps o try else fn f => fn x => f x) + (fn _ => run_chaku_on_subgoal state params mode i) (unknownN, NONE) + |> `(fn (outcome_code, _) => outcome_code = genuineN) + end; + +fun string_for_raw_param (name, value) = + name ^ " = " ^ stringify_raw_param_value value; + +fun nunchaku_params_trans params = + Toplevel.theory (fold set_default_raw_param params + #> tap (fn thy => + let val params = rev (default_raw_params thy) in + List.app check_raw_param params; + writeln ("Default parameters for Nunchaku:\n" ^ + (params |> map string_for_raw_param |> sort_strings |> cat_lines)) + end)); + +val _ = + Outer_Syntax.command @{command_keyword nunchaku} + "try to find a countermodel using Nunchaku" + (parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) => + Toplevel.keep_proof (fn state => + ignore (run_chaku params Normal i (Toplevel.proof_of state))))); + +val _ = + Outer_Syntax.command @{command_keyword nunchaku_params} + "set and display the default parameters for Nunchaku" + (parse_params #>> nunchaku_params_trans); + +end;