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 nitpickN : string

    14   val nitpick_paramsN : string

    15   val auto : bool Unsynchronized.ref

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

    17   val setup : theory -> theory

    18 end;

    20 structure Nitpick_Isar : NITPICK_ISAR =

    21 struct

    23 open Nitpick_Util

    24 open Nitpick_HOL

    25 open Nitpick_Rep

    26 open Nitpick_Nut

    27 open Nitpick

    29 val nitpickN = "nitpick"

    30 val nitpick_paramsN = "nitpick_params"

    32 val auto = Unsynchronized.ref false

    34 (* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share

    35    its time slot with several other automatic tools. *)

    36 val max_auto_scopes = 6

    38 val _ =

    39   ProofGeneralPgip.add_preference Preferences.category_tracing

    40       (Preferences.bool_pref auto "auto-nitpick"

    41            "Run Nitpick automatically.")

    43 type raw_param = string * string list

    45 val default_default_params =

    46   [("card", "1\<emdash>10"),

    47    ("iter", "0,1,2,4,8,12,16,20,24,28"),

    48    ("bits", "1,2,3,4,6,8,10,12,14,16"),

    49    ("bisim_depth", "9"),

    50    ("box", "smart"),

    51    ("finitize", "smart"),

    52    ("mono", "smart"),

    53    ("std", "true"),

    54    ("wf", "smart"),

    55    ("sat_solver", "smart"),

    56    ("batch_size", "smart"),

    57    ("blocking", "true"),

    58    ("falsify", "true"),

    59    ("user_axioms", "smart"),

    60    ("assms", "true"),

    61    ("merge_type_vars", "false"),

    62    ("binary_ints", "smart"),

    63    ("destroy_constrs", "true"),

    64    ("specialize", "true"),

    65    ("star_linear_preds", "true"),

    66    ("total_consts", "smart"),

    67    ("peephole_optim", "true"),

    68    ("datatype_sym_break", "5"),

    69    ("kodkod_sym_break", "15"),

    70    ("timeout", "30"),

    71    ("tac_timeout", "0.5"),

    72    ("max_threads", "0"),

    73    ("debug", "false"),

    74    ("verbose", "false"),

    75    ("overlord", "false"),

    76    ("show_datatypes", "false"),

    77    ("show_skolems", "true"),

    78    ("show_consts", "false"),

    79    ("format", "1"),

    80    ("max_potential", "1"),

    81    ("max_genuine", "1"),

    82    ("check_potential", "false"),

    83    ("check_genuine", "false")]

    85 val negated_params =

    86   [("dont_box", "box"),

    87    ("dont_finitize", "finitize"),

    88    ("non_mono", "mono"),

    89    ("non_std", "std"),

    90    ("non_wf", "wf"),

    91    ("non_blocking", "blocking"),

    92    ("satisfy", "falsify"),

    93    ("no_user_axioms", "user_axioms"),

    94    ("no_assms", "assms"),

    95    ("dont_merge_type_vars", "merge_type_vars"),

    96    ("unary_ints", "binary_ints"),

    97    ("dont_destroy_constrs", "destroy_constrs"),

    98    ("dont_specialize", "specialize"),

    99    ("dont_star_linear_preds", "star_linear_preds"),

   100    ("partial_consts", "total_consts"),

   101    ("no_peephole_optim", "peephole_optim"),

   102    ("no_debug", "debug"),

   103    ("quiet", "verbose"),

   104    ("no_overlord", "overlord"),

   105    ("hide_datatypes", "show_datatypes"),

   106    ("hide_skolems", "show_skolems"),

   107    ("hide_consts", "show_consts"),

   108    ("trust_potential", "check_potential"),

   109    ("trust_genuine", "check_genuine")]

   111 fun is_known_raw_param s =

   112   AList.defined (op =) default_default_params s orelse

   113   AList.defined (op =) negated_params s orelse

   114   member (op =) ["max", "show_all", "whack", "eval", "need", "atoms",

   115                  "expect"] s orelse

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

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

   118           "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format",

   119           "atoms"]

   121 fun check_raw_param (s, _) =

   122   if is_known_raw_param s then ()

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

   125 fun unnegate_param_name name =

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

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

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

   129             else NONE

   130   | some_name => some_name

   131 fun normalize_raw_param (name, value) =

   132   case unnegate_param_name name of

   133     SOME name' => [(name', case value of

   134                              ["false"] => ["true"]

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

   136                            | [] => ["false"]

   137                            | _ => value)]

   138   | NONE => if name = "show_all" then

   139               [("show_datatypes", value), ("show_skolems", value),

   140                ("show_consts", value)]

   141             else

   142               [(name, value)]

   144 structure Data = Theory_Data

   145 (

   146   type T = raw_param list

   147   val empty = map (apsnd single) default_default_params

   148   val extend = I

   149   fun merge data = AList.merge (op =) (K true) data

   150 )

   152 val set_default_raw_param =

   153   Data.map o fold (AList.update (op =)) o normalize_raw_param

   154 val default_raw_params = Data.get

   156 fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<emdash>")

   158 fun stringify_raw_param_value [] = ""

   159   | stringify_raw_param_value [s] = s

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

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

   162     stringify_raw_param_value (s2 :: ss)

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

   166 fun extract_params ctxt auto default_params override_params =

   167   let

   168     val override_params = maps normalize_raw_param override_params

   169     val raw_params = rev override_params @ rev default_params

   170     val raw_lookup = AList.lookup (op =) raw_params

   171     val lookup = Option.map stringify_raw_param_value o raw_lookup

   172     val lookup_string = the_default "" o lookup

   173     fun general_lookup_bool option default_value name =

   174       case lookup name of

   175         SOME s => parse_bool_option option name s

   176       | NONE => default_value

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

   178     val lookup_bool_option = general_lookup_bool true NONE

   179     fun do_int name value =

   180       case value of

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

   182                      SOME i => i

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

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

   185       | NONE => 0

   186     fun lookup_int name = do_int name (lookup name)

   187     fun lookup_int_option name =

   188       case lookup name of

   189         SOME "smart" => NONE

   190       | value => SOME (do_int name value)

   191     fun int_range_from_string name min_int s =

   192       let

   193         val (k1, k2) =

   194           (case space_explode "-" s of

   195              [s] => the_default (s, s) (first_field "\<emdash>" s)

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

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

   198            | _ => raise Option)

   199           |> pairself (maxed_int_from_string min_int)

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

   201       handle Option.Option =>

   202              error ("Parameter " ^ quote name ^

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

   204     fun int_seq_from_string name min_int s =

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

   206     fun lookup_int_seq name min_int =

   207       case lookup name of

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

   209                      [] => [min_int]

   210                    | value => value)

   211       | NONE => [min_int]

   212     fun lookup_assigns read prefix default convert =

   213       (NONE, convert (the_default default (lookup prefix)))

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

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

   216                   convert (stringify_raw_param_value value)))

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

   218     fun lookup_ints_assigns read prefix min_int =

   219       lookup_assigns read prefix (signed_string_of_int min_int)

   220                      (int_seq_from_string prefix min_int)

   221     fun lookup_bool_assigns read prefix =

   222       lookup_assigns read prefix "" (the o parse_bool_option false prefix)

   223     fun lookup_bool_option_assigns read prefix =

   224       lookup_assigns read prefix "" (parse_bool_option true prefix)

   225     fun lookup_strings_assigns read prefix =

   226       lookup_assigns read prefix "" (space_explode " ")

   227     fun lookup_time name =

   228       case lookup name of

   229         SOME s => parse_time_option name s

   230       | NONE => NONE

   231     val read_type_polymorphic =

   232       Syntax.read_typ ctxt #> Logic.mk_type

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

   234     val read_term_polymorphic =

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

   236     val lookup_term_list_option_polymorphic =

   237       AList.lookup (op =) raw_params #> Option.map (map read_term_polymorphic)

   238     val read_const_polymorphic = read_term_polymorphic #> dest_Const

   239     val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1

   240                         |> auto ? map (apsnd (take max_auto_scopes))

   241     val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1

   242     val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0

   243     val bitss = lookup_int_seq "bits" 1

   244     val bisim_depths = lookup_int_seq "bisim_depth" ~1

   245     val boxes = lookup_bool_option_assigns read_type_polymorphic "box"

   246     val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"

   247     val monos = if auto then [(NONE, SOME true)]

   248                 else lookup_bool_option_assigns read_type_polymorphic "mono"

   249     val stds = lookup_bool_assigns read_type_polymorphic "std"

   250     val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"

   251     val sat_solver = lookup_string "sat_solver"

   252     val blocking = auto orelse lookup_bool "blocking"

   253     val falsify = lookup_bool "falsify"

   254     val debug = not auto andalso lookup_bool "debug"

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

   256     val overlord = lookup_bool "overlord"

   257     val user_axioms = lookup_bool_option "user_axioms"

   258     val assms = lookup_bool "assms"

   259     val whacks = lookup_term_list_option_polymorphic "whack" |> these

   260     val merge_type_vars = lookup_bool "merge_type_vars"

   261     val binary_ints = lookup_bool_option "binary_ints"

   262     val destroy_constrs = lookup_bool "destroy_constrs"

   263     val specialize = lookup_bool "specialize"

   264     val star_linear_preds = lookup_bool "star_linear_preds"

   265     val total_consts = lookup_bool_option "total_consts"

   266     val needs = lookup_term_list_option_polymorphic "need"

   267     val peephole_optim = lookup_bool "peephole_optim"

   268     val datatype_sym_break = lookup_int "datatype_sym_break"

   269     val kodkod_sym_break = lookup_int "kodkod_sym_break"

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

   271     val tac_timeout = lookup_time "tac_timeout"

   272     val max_threads = if auto then 1 else Int.max (0, lookup_int "max_threads")

   273     val show_datatypes = debug orelse lookup_bool "show_datatypes"

   274     val show_skolems = debug orelse lookup_bool "show_skolems"

   275     val show_consts = debug orelse lookup_bool "show_consts"

   276     val evals = lookup_term_list_option_polymorphic "eval" |> these

   277     val formats = lookup_ints_assigns read_term_polymorphic "format" 0

   278     val atomss = lookup_strings_assigns read_type_polymorphic "atoms"

   279     val max_potential =

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

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

   282     val check_potential = lookup_bool "check_potential"

   283     val check_genuine = lookup_bool "check_genuine"

   284     val batch_size =

   285       case lookup_int_option "batch_size" of

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

   287       | NONE => if debug then 1 else 50

   288     val expect = lookup_string "expect"

   289   in

   290     {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,

   291      iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,

   292      boxes = boxes, finitizes = finitizes, monos = monos, stds = stds,

   293      wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,

   294      debug = debug, verbose = verbose, overlord = overlord,

   295      user_axioms = user_axioms, assms = assms, whacks = whacks,

   296      merge_type_vars = merge_type_vars, binary_ints = binary_ints,

   297      destroy_constrs = destroy_constrs, specialize = specialize,

   298      star_linear_preds = star_linear_preds, total_consts = total_consts,

   299      needs = needs, peephole_optim = peephole_optim,

   300      datatype_sym_break = datatype_sym_break,

   301      kodkod_sym_break = kodkod_sym_break, timeout = timeout,

   302      tac_timeout = tac_timeout, max_threads = max_threads,

   303      show_datatypes = show_datatypes, show_skolems = show_skolems,

   304      show_consts = show_consts, evals = evals, formats = formats,

   305      atomss = atomss, max_potential = max_potential, max_genuine = max_genuine,

   306      check_potential = check_potential, check_genuine = check_genuine,

   307      batch_size = batch_size, expect = expect}

   308   end

   310 fun default_params thy =

   311   extract_params (Proof_Context.init_global thy) false (default_raw_params thy)

   312   o map (apsnd single)

   314 val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "

   315 val parse_value =

   316   Scan.repeat1 (Parse.minus >> single

   317                 || Scan.repeat1 (Scan.unless Parse.minus

   318                                              (Parse.name || Parse.float_number))

   319                 || Parse.$$$ "," |-- Parse.number >> prefix "," >> single)

   320   >> flat

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

   322 val parse_params =

   323   Scan.optional (Parse.$$$ "[" |-- Parse.list parse_param --| Parse.$$$ "]") []

   325 fun handle_exceptions ctxt f x =

   326   f x

   327   handle ARG (loc, details) =>

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

   329        | BAD (loc, details) =>

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

   331        | NOT_SUPPORTED details =>

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

   333        | NUT (loc, us) =>

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

   335                 " (" ^ quote loc ^ "): " ^

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

   337        | REP (loc, Rs) =>

   338          error ("Invalid representation" ^ plural_s_for_list Rs ^

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

   340        | TERM (loc, ts) =>

   341          error ("Invalid term" ^ plural_s_for_list ts ^

   342                 " (" ^ quote loc ^ "): " ^

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

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

   345          error ("Invalid type" ^ plural_s_for_list Ts ^

   346                 (if null ts then

   347                    ""

   348                  else

   349                    " for term" ^ plural_s_for_list ts ^ " " ^

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

   351                 " (" ^ quote loc ^ "): " ^

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

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

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

   356 fun pick_nits override_params auto i step state =

   357   let

   358     val thy = Proof.theory_of state

   359     val ctxt = Proof.context_of state

   360     val _ = List.app check_raw_param override_params

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

   362       extract_params ctxt auto (default_raw_params thy) override_params

   363     fun go () =

   364       (unknownN, state)

   365       |> (if auto then perhaps o try

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

   367           else handle_exceptions ctxt)

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

   369   in if blocking then go () else Future.fork (tap go) |> K (unknownN, state) end

   370   |> `(fn (outcome_code, _) => outcome_code = genuineN)

   372 fun nitpick_trans (params, i) =

   373   Toplevel.keep (fn state =>

   374       pick_nits params false i (Toplevel.proof_position_of state)

   375                 (Toplevel.proof_of state) |> K ())

   377 fun string_for_raw_param (name, value) =

   378   name ^ " = " ^ stringify_raw_param_value value

   380 fun nitpick_params_trans params =

   381   Toplevel.theory

   382       (fold set_default_raw_param params

   383        #> tap (fn thy =>

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

   385                            (case rev (default_raw_params thy) of

   386                               [] => "none"

   387                             | params =>

   388                               (map check_raw_param params;

   389                                params |> map string_for_raw_param

   390                                       |> sort_strings |> cat_lines)))))

   392 val parse_nitpick_command =

   393   (parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans

   394 val parse_nitpick_params_command = parse_params #>> nitpick_params_trans

   396 val _ = Outer_Syntax.improper_command nitpickN

   397             "try to find a counterexample for a given subgoal using Nitpick"

   398             Keyword.diag parse_nitpick_command

   399 val _ = Outer_Syntax.command nitpick_paramsN

   400             "set and display the default parameters for Nitpick"

   401             Keyword.thy_decl parse_nitpick_params_command

   403 fun try_nitpick auto = pick_nits [] auto 1 0

   405 val setup = Try.register_tool (nitpickN, (auto, try_nitpick))

   407 end;

author	blanchet
	Fri, 27 May 2011 10:30:08 +0200
changeset 43861	abb5d1f907e4
parent 43859	121aa59b4d17
child 43863	7d3ce43d9464
permissions	-rw-r--r--