continuation of Nitpick's integration into Isabelle;
added examples, and integrated non-Main theories better.
(* Title: HOL/Nitpick/Tools/nitpick_isar.ML
Author: Jasmin Blanchette, TU Muenchen
Copyright 2008, 2009
Adds the "nitpick" and "nitpick_params" commands to Isabelle/Isar's outer
syntax.
*)
signature NITPICK_ISAR =
sig
type params = Nitpick.params
val default_params : theory -> (string * string) list -> params
end
structure NitpickIsar : NITPICK_ISAR =
struct
open NitpickUtil
open NitpickHOL
open NitpickRep
open NitpickNut
open Nitpick
type raw_param = string * string list
val default_default_params =
[("card", ["1\<midarrow>8"]),
("iter", ["0,1,2,4,8,12,16,24"]),
("bisim_depth", ["7"]),
("box", ["smart"]),
("mono", ["smart"]),
("wf", ["smart"]),
("sat_solver", ["smart"]),
("batch_size", ["smart"]),
("auto", ["false"]),
("blocking", ["true"]),
("falsify", ["true"]),
("user_axioms", ["smart"]),
("assms", ["true"]),
("coalesce_type_vars", ["false"]),
("destroy_constrs", ["true"]),
("specialize", ["true"]),
("skolemize", ["true"]),
("star_linear_preds", ["true"]),
("uncurry", ["true"]),
("fast_descrs", ["true"]),
("peephole_optim", ["true"]),
("timeout", ["30 s"]),
("auto_timeout", ["5 s"]),
("tac_timeout", ["500 ms"]),
("sym_break", ["20"]),
("sharing_depth", ["3"]),
("flatten_props", ["false"]),
("max_threads", ["0"]),
("verbose", ["false"]),
("debug", ["false"]),
("overlord", ["false"]),
("show_all", ["false"]),
("show_skolems", ["true"]),
("show_datatypes", ["false"]),
("show_consts", ["false"]),
("format", ["1"]),
("max_potential", ["1"]),
("max_genuine", ["1"]),
("check_potential", ["false"]),
("check_genuine", ["false"])]
val negated_params =
[("dont_box", "box"),
("non_mono", "mono"),
("non_wf", "wf"),
("no_auto", "auto"),
("non_blocking", "blocking"),
("satisfy", "falsify"),
("no_user_axioms", "user_axioms"),
("no_assms", "assms"),
("dont_coalesce_type_vars", "coalesce_type_vars"),
("dont_destroy_constrs", "destroy_constrs"),
("dont_specialize", "specialize"),
("dont_skolemize", "skolemize"),
("dont_star_linear_preds", "star_linear_preds"),
("dont_uncurry", "uncurry"),
("full_descrs", "fast_descrs"),
("no_peephole_optim", "peephole_optim"),
("dont_flatten_props", "flatten_props"),
("quiet", "verbose"),
("no_debug", "debug"),
("no_overlord", "overlord"),
("dont_show_all", "show_all"),
("hide_skolems", "show_skolems"),
("hide_datatypes", "show_datatypes"),
("hide_consts", "show_consts"),
("trust_potential", "check_potential"),
("trust_genuine", "check_genuine")]
(* string -> bool *)
fun is_known_raw_param s =
AList.defined (op =) default_default_params s
orelse AList.defined (op =) negated_params s
orelse s mem ["max", "eval", "expect"]
orelse exists (fn p => String.isPrefix (p ^ " ") s)
["card", "max", "iter", "box", "dont_box", "mono", "non_mono",
"wf", "non_wf", "format"]
(* string * 'a -> unit *)
fun check_raw_param (s, _) =
if is_known_raw_param s then ()
else error ("Unknown parameter " ^ quote s ^ ".")
(* string -> string option *)
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
(* raw_param -> raw_param *)
fun unnegate_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 TheoryData = TheoryDataFun(
type T = {params: raw_param list, registered_auto: bool}
val empty = {params = rev default_default_params, registered_auto = false}
val copy = I
val extend = I
fun merge _ ({params = ps1, registered_auto = a1},
{params = ps2, registered_auto = a2}) =
{params = AList.merge (op =) (op =) (ps1, ps2),
registered_auto = a1 orelse a2})
(* raw_param -> theory -> theory *)
fun set_default_raw_param param thy =
let val {params, registered_auto} = TheoryData.get thy in
TheoryData.put
{params = AList.update (op =) (unnegate_raw_param param) params,
registered_auto = registered_auto} thy
end
(* theory -> raw_param list *)
val default_raw_params = #params o TheoryData.get
(* theory -> theory *)
fun set_registered_auto thy =
TheoryData.put {params = default_raw_params thy, registered_auto = true} thy
(* theory -> bool *)
val is_registered_auto = #registered_auto o TheoryData.get
(* string -> bool *)
fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
(* string list -> string *)
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)
(* bool -> string -> string -> bool option *)
fun bool_option_from_string option name s =
(case s of
"smart" => if option then NONE else raise Option
| "false" => SOME false
| "true" => SOME true
| "" => SOME true
| s => raise Option)
handle Option.Option =>
let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
error ("Parameter " ^ quote name ^ " must be assigned " ^
space_implode " " (serial_commas "or" ss) ^ ".")
end
(* bool -> raw_param list -> bool option -> string -> bool option *)
fun general_lookup_bool option raw_params default_value name =
case AList.lookup (op =) raw_params name of
SOME s => s |> stringify_raw_param_value
|> bool_option_from_string option name
| NONE => default_value
(* int -> string -> int *)
fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))
(* Proof.context -> bool -> raw_param list -> raw_param list -> params *)
fun extract_params ctxt auto default_params override_params =
let
val override_params = map unnegate_raw_param override_params
val raw_params = rev override_params @ rev default_params
val lookup =
Option.map stringify_raw_param_value o AList.lookup (op =) raw_params
(* string -> string *)
fun lookup_string name = the_default "" (lookup name)
(* string -> bool *)
val lookup_bool = the o general_lookup_bool false raw_params (SOME false)
(* string -> bool option *)
val lookup_bool_option = general_lookup_bool true raw_params NONE
(* string -> string option -> int *)
fun do_int name value =
case value of
SOME s => (case Int.fromString s of
SOME i => i
| NONE => error ("Parameter " ^ quote name ^
" must be assigned an integer value."))
| NONE => 0
(* string -> int *)
fun lookup_int name = do_int name (lookup name)
(* string -> int option *)
fun lookup_int_option name =
case lookup name of
SOME "smart" => NONE
| value => SOME (do_int name value)
(* string -> int -> string -> int list *)
fun int_range_from_string name min_int s =
let
val (k1, k2) =
(case space_explode "-" s of
[s] => the_default (s, s) (first_field "\<midarrow>" s)
| ["", s2] => ("-" ^ s2, "-" ^ s2)
| [s1, s2] => (s1, s2)
| _ => raise Option)
|> pairself (maxed_int_from_string min_int)
in if k1 <= k2 then k1 upto k2 else k1 downto k2 end
handle Option.Option =>
error ("Parameter " ^ quote name ^
" must be assigned a sequence of integers.")
(* string -> int -> string -> int list *)
fun int_seq_from_string name min_int s =
maps (int_range_from_string name min_int) (space_explode "," s)
(* string -> int -> int list *)
fun lookup_int_seq name min_int =
case lookup name of
SOME s => (case int_seq_from_string name min_int s of
[] => [min_int]
| value => value)
| NONE => [min_int]
(* (string -> 'a) -> int -> string -> ('a option * int list) list *)
fun lookup_ints_assigns read prefix min_int =
(NONE, lookup_int_seq prefix min_int)
:: map (fn (name, value) =>
(SOME (read (String.extract (name, size prefix + 1, NONE))),
value |> stringify_raw_param_value
|> int_seq_from_string name min_int))
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
(* (string -> 'a) -> string -> ('a option * bool option) list *)
fun lookup_bool_option_assigns read prefix =
(NONE, lookup_bool_option prefix)
:: map (fn (name, value) =>
(SOME (read (String.extract (name, size prefix + 1, NONE))),
value |> stringify_raw_param_value
|> bool_option_from_string true name))
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
(* string -> Time.time option *)
fun lookup_time name =
case lookup name of
NONE => NONE
| SOME "none" => NONE
| SOME s =>
let
val msecs =
case space_explode " " s of
[s1, "min"] => 60000 * the (Int.fromString s1)
| [s1, "s"] => 1000 * the (Int.fromString s1)
| [s1, "ms"] => the (Int.fromString s1)
| _ => 0
in
if msecs <= 0 then
error ("Parameter " ^ quote name ^ " must be assigned a positive \
\time value (e.g., \"60 s\", \"200 ms\") or \"none\".")
else
SOME (Time.fromMilliseconds msecs)
end
(* string -> term list *)
val lookup_term_list =
AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt
val read_type_polymorphic =
Syntax.read_typ ctxt #> Logic.mk_type
#> singleton (Variable.polymorphic ctxt) #> Logic.dest_type
(* string -> term *)
val read_term_polymorphic =
Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt)
(* string -> styp *)
val read_const_polymorphic = read_term_polymorphic #> dest_Const
val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
val bisim_depths = lookup_int_seq "bisim_depth" ~1
val boxes =
lookup_bool_option_assigns read_type_polymorphic "box" @
map_filter (fn (SOME T, _) =>
if is_fun_type T orelse is_pair_type T then
SOME (SOME T, SOME true)
else
NONE
| (NONE, _) => NONE) cards_assigns
val monos = lookup_bool_option_assigns read_type_polymorphic "mono"
val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
val sat_solver = lookup_string "sat_solver"
val blocking = not auto andalso lookup_bool "blocking"
val falsify = lookup_bool "falsify"
val debug = not auto andalso lookup_bool "debug"
val verbose = debug orelse (not auto andalso lookup_bool "verbose")
val overlord = lookup_bool "overlord"
val user_axioms = lookup_bool_option "user_axioms"
val assms = lookup_bool "assms"
val coalesce_type_vars = lookup_bool "coalesce_type_vars"
val destroy_constrs = lookup_bool "destroy_constrs"
val specialize = lookup_bool "specialize"
val skolemize = lookup_bool "skolemize"
val star_linear_preds = lookup_bool "star_linear_preds"
val uncurry = lookup_bool "uncurry"
val fast_descrs = lookup_bool "fast_descrs"
val peephole_optim = lookup_bool "peephole_optim"
val timeout = if auto then lookup_time "auto_timeout"
else lookup_time "timeout"
val tac_timeout = lookup_time "tac_timeout"
val sym_break = Int.max (0, lookup_int "sym_break")
val sharing_depth = Int.max (1, lookup_int "sharing_depth")
val flatten_props = lookup_bool "flatten_props"
val max_threads = Int.max (0, lookup_int "max_threads")
val show_all = debug orelse lookup_bool "show_all"
val show_skolems = show_all orelse lookup_bool "show_skolems"
val show_datatypes = show_all orelse lookup_bool "show_datatypes"
val show_consts = show_all orelse lookup_bool "show_consts"
val formats = lookup_ints_assigns read_term_polymorphic "format" 0
val evals = lookup_term_list "eval"
val max_potential = if auto then 0
else Int.max (0, lookup_int "max_potential")
val max_genuine = Int.max (0, lookup_int "max_genuine")
val check_potential = lookup_bool "check_potential"
val check_genuine = lookup_bool "check_genuine"
val batch_size = case lookup_int_option "batch_size" of
SOME n => Int.max (1, n)
| NONE => if debug then 1 else 64
val expect = lookup_string "expect"
in
{cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
iters_assigns = iters_assigns, bisim_depths = bisim_depths, boxes = boxes,
monos = monos, wfs = wfs, sat_solver = sat_solver, blocking = blocking,
falsify = falsify, debug = debug, verbose = verbose, overlord = overlord,
user_axioms = user_axioms, assms = assms,
coalesce_type_vars = coalesce_type_vars, destroy_constrs = destroy_constrs,
specialize = specialize, skolemize = skolemize,
star_linear_preds = star_linear_preds, uncurry = uncurry,
fast_descrs = fast_descrs, peephole_optim = peephole_optim,
timeout = timeout, tac_timeout = tac_timeout, sym_break = sym_break,
sharing_depth = sharing_depth, flatten_props = flatten_props,
max_threads = max_threads, show_skolems = show_skolems,
show_datatypes = show_datatypes, show_consts = show_consts,
formats = formats, evals = evals, max_potential = max_potential,
max_genuine = max_genuine, check_potential = check_potential,
check_genuine = check_genuine, batch_size = batch_size, expect = expect}
end
(* theory -> (string * string) list -> params *)
fun default_params thy =
extract_params (ProofContext.init thy) false (default_raw_params thy)
o map (apsnd single)
(* OuterParse.token list -> string * OuterParse.token list *)
val scan_key = Scan.repeat1 OuterParse.typ_group >> space_implode " "
(* OuterParse.token list -> string list * OuterParse.token list *)
val scan_value =
Scan.repeat1 (OuterParse.minus >> single
|| Scan.repeat1 (Scan.unless OuterParse.minus OuterParse.name)
|| OuterParse.$$$ "," |-- OuterParse.number >> prefix ","
>> single) >> flat
(* OuterParse.token list -> raw_param * OuterParse.token list *)
val scan_param =
scan_key -- (Scan.option (OuterParse.$$$ "=" |-- scan_value) >> these)
(* OuterParse.token list -> raw_param list option * OuterParse.token list *)
val scan_params = Scan.option (OuterParse.$$$ "[" |-- OuterParse.list scan_param
--| OuterParse.$$$ "]")
(* Proof.context -> ('a -> 'a) -> 'a -> 'a *)
fun handle_exceptions ctxt f x =
f x
handle ARG (loc, details) =>
error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".")
| BAD (loc, details) =>
error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".")
| LIMIT (_, details) =>
(warning ("Limit reached: " ^ details ^ "."); x)
| NOT_SUPPORTED details =>
(warning ("Unsupported case: " ^ details ^ "."); x)
| NUT (loc, us) =>
error ("Invalid intermediate term" ^ plural_s_for_list us ^
" (" ^ quote loc ^ "): " ^
commas (map (string_for_nut ctxt) us) ^ ".")
| REP (loc, Rs) =>
error ("Invalid representation" ^ plural_s_for_list Rs ^
" (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs) ^ ".")
| TERM (loc, ts) =>
error ("Invalid term" ^ plural_s_for_list ts ^
" (" ^ quote loc ^ "): " ^
commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
| TYPE (loc, Ts, ts) =>
error ("Invalid type" ^ plural_s_for_list Ts ^
(if null ts then
""
else
" for term" ^ plural_s_for_list ts ^ " " ^
commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
" (" ^ quote loc ^ "): " ^
commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".")
| Kodkod.SYNTAX (_, details) =>
(warning ("Ill-formed Kodkodi output: " ^ details ^ "."); x)
| Refute.REFUTE (loc, details) =>
error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
(* raw_param list -> bool -> int -> Proof.state -> Proof.state *)
fun pick_nits override_params auto subgoal state =
let
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
val thm = snd (snd (Proof.get_goal state))
val _ = List.app check_raw_param override_params
val params as {blocking, debug, ...} =
extract_params ctxt auto (default_raw_params thy) override_params
(* unit -> Proof.state *)
fun go () =
(if auto then perhaps o try
else if debug then fn f => fn x => f x
else handle_exceptions ctxt)
(fn state => pick_nits_in_subgoal state params auto subgoal |> snd)
state
in
if auto orelse blocking then
go ()
else
(SimpleThread.fork true (fn () => (go (); ()) handle Exn.Interrupt => ());
state)
end
(* (TableFun().key * string list) list option * int option
-> Toplevel.transition -> Toplevel.transition *)
fun nitpick_trans (opt_params, opt_subgoal) =
Toplevel.keep (K ()
o pick_nits (these opt_params) false (the_default 1 opt_subgoal)
o Toplevel.proof_of)
(* raw_param -> string *)
fun string_for_raw_param (name, value) =
name ^ " = " ^ stringify_raw_param_value value
(* bool -> Proof.state -> Proof.state *)
fun pick_nits_auto interactive state =
let val thy = Proof.theory_of state in
((interactive andalso not (!Toplevel.quiet)
andalso the (general_lookup_bool false (default_raw_params thy)
(SOME false) "auto"))
? pick_nits [] true 0) state
end
(* theory -> theory *)
fun register_auto thy =
(not (is_registered_auto thy)
? (set_registered_auto
#> Context.theory_map (Specification.add_theorem_hook pick_nits_auto)))
thy
(* (TableFun().key * string) list option -> Toplevel.transition
-> Toplevel.transition *)
fun nitpick_params_trans opt_params =
Toplevel.theory
(fn thy =>
let val thy = fold set_default_raw_param (these opt_params) thy in
writeln ("Default parameters for Nitpick:\n" ^
(case rev (default_raw_params thy) of
[] => "none"
| params =>
(map check_raw_param params;
params |> map string_for_raw_param |> sort_strings
|> cat_lines)));
register_auto thy
end)
(* OuterParse.token list
-> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
fun scan_nitpick_command tokens =
(scan_params -- Scan.option OuterParse.nat) tokens |>> nitpick_trans
fun scan_nitpick_params_command tokens =
scan_params tokens |>> nitpick_params_trans
val _ = OuterSyntax.improper_command "nitpick"
"try to find a counterexample for a given subgoal using Kodkod"
OuterKeyword.diag scan_nitpick_command
val _ = OuterSyntax.command "nitpick_params"
"set and display the default parameters for Nitpick"
OuterKeyword.thy_decl scan_nitpick_params_command
end;