wneuper/isa: src/HOL/Tools/Nitpick/nitpick

     1 (*  Title:      HOL/Tools/Nitpick/nitpick_isar.ML

     2     Author:     Jasmin Blanchette, TU Muenchen

     3     Copyright   2008, 2009, 2010

     5 Adds the "nitpick" and "nitpick_params" commands to Isabelle/Isar's outer

     6 syntax.

     7 *)

     9 signature NITPICK_ISAR =

    10 sig

    11   type params = Nitpick.params

    13   val auto: bool Unsynchronized.ref

    14   val default_params : theory -> (string * string) list -> params

    15   val setup : theory -> theory

    16 end;

    18 structure Nitpick_Isar : NITPICK_ISAR =

    19 struct

    21 open Nitpick_Util

    22 open Nitpick_HOL

    23 open Nitpick_Rep

    24 open Nitpick_Nut

    25 open Nitpick

    27 structure K = OuterKeyword and P = OuterParse

    29 val auto = Unsynchronized.ref false;

    31 val _ =

    32   ProofGeneralPgip.add_preference Preferences.category_tracing

    33       (Preferences.bool_pref auto "auto-nitpick"

    34            "Whether to run Nitpick automatically.")

    36 type raw_param = string * string list

    38 val default_default_params =

    39   [("card", "1\<midarrow>8"),

    40    ("iter", "0,1,2,4,8,12,16,24"),

    41    ("bits", "1,2,3,4,6,8,10,12"),

    42    ("bisim_depth", "7"),

    43    ("box", "smart"),

    44    ("finitize", "smart"),

    45    ("mono", "smart"),

    46    ("std", "true"),

    47    ("wf", "smart"),

    48    ("sat_solver", "smart"),

    49    ("batch_size", "smart"),

    50    ("blocking", "true"),

    51    ("falsify", "true"),

    52    ("user_axioms", "smart"),

    53    ("assms", "true"),

    54    ("merge_type_vars", "false"),

    55    ("binary_ints", "smart"),

    56    ("destroy_constrs", "true"),

    57    ("specialize", "true"),

    58    ("skolemize", "true"),

    59    ("star_linear_preds", "true"),

    60    ("fast_descrs", "true"),

    61    ("peephole_optim", "true"),

    62    ("timeout", "30 s"),

    63    ("tac_timeout", "500 ms"),

    64    ("max_threads", "0"),

    65    ("debug", "false"),

    66    ("verbose", "false"),

    67    ("overlord", "false"),

    68    ("show_all", "false"),

    69    ("show_skolems", "true"),

    70    ("show_datatypes", "false"),

    71    ("show_consts", "false"),

    72    ("format", "1"),

    73    ("max_potential", "1"),

    74    ("max_genuine", "1"),

    75    ("check_potential", "false"),

    76    ("check_genuine", "false")]

    78 val negated_params =

    79   [("dont_box", "box"),

    80    ("dont_finitize", "finitize"),

    81    ("non_mono", "mono"),

    82    ("non_std", "std"),

    83    ("non_wf", "wf"),

    84    ("non_blocking", "blocking"),

    85    ("satisfy", "falsify"),

    86    ("no_user_axioms", "user_axioms"),

    87    ("no_assms", "assms"),

    88    ("dont_merge_type_vars", "merge_type_vars"),

    89    ("unary_ints", "binary_ints"),

    90    ("dont_destroy_constrs", "destroy_constrs"),

    91    ("dont_specialize", "specialize"),

    92    ("dont_skolemize", "skolemize"),

    93    ("dont_star_linear_preds", "star_linear_preds"),

    94    ("full_descrs", "fast_descrs"),

    95    ("no_peephole_optim", "peephole_optim"),

    96    ("no_debug", "debug"),

    97    ("quiet", "verbose"),

    98    ("no_overlord", "overlord"),

    99    ("dont_show_all", "show_all"),

   100    ("hide_skolems", "show_skolems"),

   101    ("hide_datatypes", "show_datatypes"),

   102    ("hide_consts", "show_consts"),

   103    ("trust_potential", "check_potential"),

   104    ("trust_genuine", "check_genuine")]

   106 fun is_known_raw_param s =

   107   AList.defined (op =) default_default_params s orelse

   108   AList.defined (op =) negated_params s orelse

   109   s = "max" orelse s = "eval" orelse s = "expect" orelse

   110   exists (fn p => String.isPrefix (p ^ " ") s)

   111          ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",

   112           "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"]

   114 fun check_raw_param (s, _) =

   115   if is_known_raw_param s then ()

   116   else error ("Unknown parameter: " ^ quote s ^ ".")

   118 fun unnegate_param_name name =

   119   case AList.lookup (op =) negated_params name of

   120     NONE => if String.isPrefix "dont_" name then SOME (unprefix "dont_" name)

   121             else if String.isPrefix "non_" name then SOME (unprefix "non_" name)

   122             else NONE

   123   | some_name => some_name

   124 fun unnegate_raw_param (name, value) =

   125   case unnegate_param_name name of

   126     SOME name' => (name', case value of

   127                             ["false"] => ["true"]

   128                           | ["true"] => ["false"]

   129                           | [] => ["false"]

   130                           | _ => value)

   131   | NONE => (name, value)

   133 structure Data = Theory_Data(

   134   type T = raw_param list

   135   val empty = default_default_params |> map (apsnd single)

   136   val extend = I

   137   fun merge p : T = AList.merge (op =) (K true) p)

   139 val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param

   140 val default_raw_params = Data.get

   142 fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")

   144 fun stringify_raw_param_value [] = ""

   145   | stringify_raw_param_value [s] = s

   146   | stringify_raw_param_value (s1 :: s2 :: ss) =

   147     s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^

   148     stringify_raw_param_value (s2 :: ss)

   150 fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))

   152 fun extract_params ctxt auto default_params override_params =

   153   let

   154     val override_params = map unnegate_raw_param override_params

   155     val raw_params = rev override_params @ rev default_params

   156     val lookup =

   157       Option.map stringify_raw_param_value o AList.lookup (op =) raw_params

   158     val lookup_string = the_default "" o lookup

   159     fun general_lookup_bool option default_value name =

   160       case lookup name of

   161         SOME s => parse_bool_option option name s

   162       | NONE => default_value

   163     val lookup_bool = the o general_lookup_bool false (SOME false)

   164     val lookup_bool_option = general_lookup_bool true NONE

   165     fun do_int name value =

   166       case value of

   167         SOME s => (case Int.fromString s of

   168                      SOME i => i

   169                    | NONE => error ("Parameter " ^ quote name ^

   170                                     " must be assigned an integer value."))

   171       | NONE => 0

   172     fun lookup_int name = do_int name (lookup name)

   173     fun lookup_int_option name =

   174       case lookup name of

   175         SOME "smart" => NONE

   176       | value => SOME (do_int name value)

   177     fun int_range_from_string name min_int s =

   178       let

   179         val (k1, k2) =

   180           (case space_explode "-" s of

   181              [s] => the_default (s, s) (first_field "\<midarrow>" s)

   182            | ["", s2] => ("-" ^ s2, "-" ^ s2)

   183            | [s1, s2] => (s1, s2)

   184            | _ => raise Option)

   185           |> pairself (maxed_int_from_string min_int)

   186       in if k1 <= k2 then k1 upto k2 else k1 downto k2 end

   187       handle Option.Option =>

   188              error ("Parameter " ^ quote name ^

   189                     " must be assigned a sequence of integers.")

   190     fun int_seq_from_string name min_int s =

   191       maps (int_range_from_string name min_int) (space_explode "," s)

   192     fun lookup_int_seq name min_int =

   193       case lookup name of

   194         SOME s => (case int_seq_from_string name min_int s of

   195                      [] => [min_int]

   196                    | value => value)

   197       | NONE => [min_int]

   198     fun lookup_ints_assigns read prefix min_int =

   199       (NONE, lookup_int_seq prefix min_int)

   200       :: map (fn (name, value) =>

   201                  (SOME (read (String.extract (name, size prefix + 1, NONE))),

   202                   value |> stringify_raw_param_value

   203                         |> int_seq_from_string name min_int))

   204              (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)

   205     fun lookup_bool_assigns read prefix =

   206       (NONE, lookup_bool prefix)

   207       :: map (fn (name, value) =>

   208                  (SOME (read (String.extract (name, size prefix + 1, NONE))),

   209                   value |> stringify_raw_param_value

   210                         |> parse_bool_option false name |> the))

   211              (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)

   212     fun lookup_bool_option_assigns read prefix =

   213       (NONE, lookup_bool_option prefix)

   214       :: map (fn (name, value) =>

   215                  (SOME (read (String.extract (name, size prefix + 1, NONE))),

   216                   value |> stringify_raw_param_value

   217                         |> parse_bool_option true name))

   218              (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)

   219     fun lookup_time name =

   220       case lookup name of

   221         NONE => NONE

   222       | SOME s => parse_time_option name s

   223     val lookup_term_list =

   224       AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt

   225     val read_type_polymorphic =

   226       Syntax.read_typ ctxt #> Logic.mk_type

   227       #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type

   228     val read_term_polymorphic =

   229       Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt)

   230     val read_const_polymorphic = read_term_polymorphic #> dest_Const

   231     val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1

   232     val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1

   233     val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0

   234     val bitss = lookup_int_seq "bits" 1

   235     val bisim_depths = lookup_int_seq "bisim_depth" ~1

   236     val boxes = lookup_bool_option_assigns read_type_polymorphic "box"

   237     val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"

   238     val monos = lookup_bool_option_assigns read_type_polymorphic "mono"

   239     val stds = lookup_bool_assigns read_type_polymorphic "std"

   240     val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"

   241     val sat_solver = lookup_string "sat_solver"

   242     val blocking = not auto andalso lookup_bool "blocking"

   243     val falsify = lookup_bool "falsify"

   244     val debug = not auto andalso lookup_bool "debug"

   245     val verbose = debug orelse (not auto andalso lookup_bool "verbose")

   246     val overlord = lookup_bool "overlord"

   247     val user_axioms = lookup_bool_option "user_axioms"

   248     val assms = lookup_bool "assms"

   249     val merge_type_vars = lookup_bool "merge_type_vars"

   250     val binary_ints = lookup_bool_option "binary_ints"

   251     val destroy_constrs = lookup_bool "destroy_constrs"

   252     val specialize = lookup_bool "specialize"

   253     val skolemize = lookup_bool "skolemize"

   254     val star_linear_preds = lookup_bool "star_linear_preds"

   255     val fast_descrs = lookup_bool "fast_descrs"

   256     val peephole_optim = lookup_bool "peephole_optim"

   257     val timeout = if auto then NONE else lookup_time "timeout"

   258     val tac_timeout = lookup_time "tac_timeout"

   259     val max_threads = Int.max (0, lookup_int "max_threads")

   260     val show_all = debug orelse lookup_bool "show_all"

   261     val show_skolems = show_all orelse lookup_bool "show_skolems"

   262     val show_datatypes = show_all orelse lookup_bool "show_datatypes"

   263     val show_consts = show_all orelse lookup_bool "show_consts"

   264     val formats = lookup_ints_assigns read_term_polymorphic "format" 0

   265     val evals = lookup_term_list "eval"

   266     val max_potential =

   267       if auto then 0 else Int.max (0, lookup_int "max_potential")

   268     val max_genuine = Int.max (0, lookup_int "max_genuine")

   269     val check_potential = lookup_bool "check_potential"

   270     val check_genuine = lookup_bool "check_genuine"

   271     val batch_size = case lookup_int_option "batch_size" of

   272                        SOME n => Int.max (1, n)

   273                      | NONE => if debug then 1 else 64

   274     val expect = lookup_string "expect"

   275   in

   276     {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,

   277      iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,

   278      boxes = boxes, finitizes = finitizes, monos = monos, stds = stds,

   279      wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,

   280      debug = debug, verbose = verbose, overlord = overlord,

   281      user_axioms = user_axioms, assms = assms,

   282      merge_type_vars = merge_type_vars, binary_ints = binary_ints,

   283      destroy_constrs = destroy_constrs, specialize = specialize,

   284      skolemize = skolemize, star_linear_preds = star_linear_preds,

   285      fast_descrs = fast_descrs, peephole_optim = peephole_optim,

   286      timeout = timeout, tac_timeout = tac_timeout, max_threads = max_threads,

   287      show_skolems = show_skolems, show_datatypes = show_datatypes,

   288      show_consts = show_consts, formats = formats, evals = evals,

   289      max_potential = max_potential, max_genuine = max_genuine,

   290      check_potential = check_potential, check_genuine = check_genuine,

   291      batch_size = batch_size, expect = expect}

   292   end

   294 fun default_params thy =

   295   extract_params (ProofContext.init thy) false (default_raw_params thy)

   296   o map (apsnd single)

   298 val parse_key = Scan.repeat1 P.typ_group >> space_implode " "

   299 val parse_value =

   300   Scan.repeat1 (P.minus >> single

   301                 || Scan.repeat1 (Scan.unless P.minus P.name)

   302                 || P.$$$ "," |-- P.number >> prefix "," >> single) >> flat

   303 val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []

   304 val parse_params =

   305   Scan.optional (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]") []

   307 fun handle_exceptions ctxt f x =

   308   f x

   309   handle ARG (loc, details) =>

   310          error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".")

   311        | BAD (loc, details) =>

   312          error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".")

   313        | NOT_SUPPORTED details =>

   314          (warning ("Unsupported case: " ^ details ^ "."); x)

   315        | NUT (loc, us) =>

   316          error ("Invalid intermediate term" ^ plural_s_for_list us ^

   317                 " (" ^ quote loc ^ "): " ^

   318                 commas (map (string_for_nut ctxt) us) ^ ".")

   319        | REP (loc, Rs) =>

   320          error ("Invalid representation" ^ plural_s_for_list Rs ^

   321                 " (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs) ^ ".")

   322        | TERM (loc, ts) =>

   323          error ("Invalid term" ^ plural_s_for_list ts ^

   324                 " (" ^ quote loc ^ "): " ^

   325                 commas (map (Syntax.string_of_term ctxt) ts) ^ ".")

   326        | TOO_LARGE (_, details) =>

   327          (warning ("Limit reached: " ^ details ^ "."); x)

   328        | TOO_SMALL (_, details) =>

   329          (warning ("Limit reached: " ^ details ^ "."); x)

   330        | TYPE (loc, Ts, ts) =>

   331          error ("Invalid type" ^ plural_s_for_list Ts ^

   332                 (if null ts then

   333                    ""

   334                  else

   335                    " for term" ^ plural_s_for_list ts ^ " " ^

   336                    commas (map (quote o Syntax.string_of_term ctxt) ts)) ^

   337                 " (" ^ quote loc ^ "): " ^

   338                 commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".")

   339        | Kodkod.SYNTAX (_, details) =>

   340          (warning ("Ill-formed Kodkodi output: " ^ details ^ "."); x)

   341        | Refute.REFUTE (loc, details) =>

   342          error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")

   344 fun pick_nits override_params auto i step state =

   345   let

   346     val thy = Proof.theory_of state

   347     val ctxt = Proof.context_of state

   348     val _ = List.app check_raw_param override_params

   349     val params as {blocking, debug, ...} =

   350       extract_params ctxt auto (default_raw_params thy) override_params

   351     fun go () =

   352       (false, state)

   353       |> (if auto then perhaps o try

   354           else if debug then fn f => fn x => f x

   355           else handle_exceptions ctxt)

   356          (fn (_, state) => pick_nits_in_subgoal state params auto i step

   357                            |>> curry (op =) "genuine")

   358   in

   359     if auto orelse blocking then go ()

   360     else (Toplevel.thread true (fn () => (go (); ())); (false, state))

   361   end

   363 fun nitpick_trans (params, i) =

   364   Toplevel.keep (fn st =>

   365       (pick_nits params false i (Toplevel.proof_position_of st)

   366                  (Toplevel.proof_of st); ()))

   368 fun string_for_raw_param (name, value) =

   369   name ^ " = " ^ stringify_raw_param_value value

   371 fun nitpick_params_trans params =

   372   Toplevel.theory

   373       (fold set_default_raw_param params

   374        #> tap (fn thy =>

   375                   writeln ("Default parameters for Nitpick:\n" ^

   376                            (case rev (default_raw_params thy) of

   377                               [] => "none"

   378                             | params =>

   379                               (map check_raw_param params;

   380                                params |> map string_for_raw_param

   381                                       |> sort_strings |> cat_lines)))))

   383 val parse_nitpick_command =

   384   (parse_params -- Scan.optional P.nat 1) #>> nitpick_trans

   385 val parse_nitpick_params_command = parse_params #>> nitpick_params_trans

   387 val _ = OuterSyntax.improper_command "nitpick"

   388             "try to find a counterexample for a given subgoal using Kodkod"

   389             K.diag parse_nitpick_command

   390 val _ = OuterSyntax.command "nitpick_params"

   391             "set and display the default parameters for Nitpick"

   392             K.thy_decl parse_nitpick_params_command

   394 fun auto_nitpick state =

   395   if not (!auto) then (false, state) else pick_nits [] true 1 0 state

   397 val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick)

   399 end;

author	blanchet
	Sat, 24 Apr 2010 17:48:21 +0200
changeset 36388	30f7ce76712d
parent 36386	2132f15b366f
child 36389	8228b3a4a2ba
permissions	-rw-r--r--