--- a/src/HOL/Nunchaku/Tools/nunchaku_commands.ML Thu Sep 07 23:13:15 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,265 +0,0 @@
-(* 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"),
- ("solvers", "cvc4 kodkod paradox smbc"),
- ("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;
- val lookup_strings = these o Option.map (space_explode " ") 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 solvers = lookup_strings "solvers";
- val falsify = lookup_bool "falsify";
- val assms = lookup_bool "assms";
- val spy = getenv "NUNCHAKU_SPY" = "yes" orelse lookup_bool "spy";
- val overlord = lookup_bool "overlord";
- val expect = lookup_string "expect";
-
- 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 debug = (mode <> Auto_Try andalso lookup_bool "debug");
- val verbose = debug orelse (mode <> Auto_Try andalso lookup_bool "verbose");
- 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 evals = these (lookup_term_list_option_polymorphic "eval");
- val atomss = lookup_strings_assigns read_type_polymorphic "atoms";
-
- val specialize = lookup_bool "specialize";
- val multithread = mode = Normal andalso lookup_bool "multithread";
-
- val timeout = lookup_time "timeout";
- val wf_timeout = lookup_time "wf_timeout";
-
- val mode_of_operation_params =
- {solvers = solvers, 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;