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    ("uncurry", "true"),

    61    ("fast_descrs", "true"),

    62    ("peephole_optim", "true"),

    63    ("timeout", "30 s"),

    64    ("tac_timeout", "500 ms"),

    65    ("sym_break", "20"),

    66    ("sharing_depth", "3"),

    67    ("flatten_props", "false"),

    68    ("max_threads", "0"),

    69    ("debug", "false"),

    70    ("verbose", "false"),

    71    ("overlord", "false"),

    72    ("show_all", "false"),

    73    ("show_skolems", "true"),

    74    ("show_datatypes", "false"),

    75    ("show_consts", "false"),

    76    ("format", "1"),

    77    ("max_potential", "1"),

    78    ("max_genuine", "1"),

    79    ("check_potential", "false"),

    80    ("check_genuine", "false")]

    82 val negated_params =

    83   [("dont_box", "box"),

    84    ("dont_finitize", "finitize"),

    85    ("non_mono", "mono"),

    86    ("non_std", "std"),

    87    ("non_wf", "wf"),

    88    ("non_blocking", "blocking"),

    89    ("satisfy", "falsify"),

    90    ("no_user_axioms", "user_axioms"),

    91    ("no_assms", "assms"),

    92    ("dont_merge_type_vars", "merge_type_vars"),

    93    ("unary_ints", "binary_ints"),

    94    ("dont_destroy_constrs", "destroy_constrs"),

    95    ("dont_specialize", "specialize"),

    96    ("dont_skolemize", "skolemize"),

    97    ("dont_star_linear_preds", "star_linear_preds"),

    98    ("dont_uncurry", "uncurry"),

    99    ("full_descrs", "fast_descrs"),

   100    ("no_peephole_optim", "peephole_optim"),

   101    ("dont_flatten_props", "flatten_props"),

   102    ("no_debug", "debug"),

   103    ("quiet", "verbose"),

   104    ("no_overlord", "overlord"),

   105    ("dont_show_all", "show_all"),

   106    ("hide_skolems", "show_skolems"),

   107    ("hide_datatypes", "show_datatypes"),

   108    ("hide_consts", "show_consts"),

   109    ("trust_potential", "check_potential"),

   110    ("trust_genuine", "check_genuine")]

   112 (* string -> bool *)

   113 fun is_known_raw_param s =

   114   AList.defined (op =) default_default_params s orelse

   115   AList.defined (op =) negated_params s orelse

   116   s = "max" orelse s = "eval" orelse s = "expect" orelse

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

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

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

   121 (* string * 'a -> unit *)

   122 fun check_raw_param (s, _) =

   123   if is_known_raw_param s then ()

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

   126 (* string -> string option *)

   127 fun unnegate_param_name name =

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

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

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

   131             else NONE

   132   | some_name => some_name

   133 (* raw_param -> raw_param *)

   134 fun unnegate_raw_param (name, value) =

   135   case unnegate_param_name name of

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

   137                             ["false"] => ["true"]

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

   139                           | [] => ["false"]

   140                           | _ => value)

   141   | NONE => (name, value)

   143 structure Data = Theory_Data(

   144   type T = raw_param list

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

   146   val extend = I

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

   149 (* raw_param -> theory -> theory *)

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

   151 (* theory -> raw_param list *)

   152 val default_raw_params = Data.get

   154 (* string -> bool *)

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

   157 (* string list -> string *)

   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 (* int -> string -> int *)

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

   167 (* Proof.context -> bool -> raw_param list -> raw_param list -> params *)

   168 fun extract_params ctxt auto default_params override_params =

   169   let

   170     val override_params = map unnegate_raw_param override_params

   171     val raw_params = rev override_params @ rev default_params

   172     (* string -> string *)

   173     val lookup =

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

   175     val lookup_string = the_default "" o lookup

   176     (* bool -> bool option -> string -> bool option *)

   177     fun general_lookup_bool option default_value name =

   178       case lookup name of

   179         SOME s => s |> stringify_raw_param_value

   180                     |> Sledgehammer_Util.parse_bool_option option name

   181       | NONE => default_value

   182     (* string -> bool *)

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

   184     (* string -> bool option *)

   185     val lookup_bool_option = general_lookup_bool true NONE

   186     (* string -> string option -> int *)

   187     fun do_int name value =

   188       case value of

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

   190                      SOME i => i

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

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

   193       | NONE => 0

   194     (* string -> int *)

   195     fun lookup_int name = do_int name (lookup name)

   196     (* string -> int option *)

   197     fun lookup_int_option name =

   198       case lookup name of

   199         SOME "smart" => NONE

   200       | value => SOME (do_int name value)

   201     (* string -> int -> string -> int list *)

   202     fun int_range_from_string name min_int s =

   203       let

   204         val (k1, k2) =

   205           (case space_explode "-" s of

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

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

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

   209            | _ => raise Option)

   210           |> pairself (maxed_int_from_string min_int)

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

   212       handle Option.Option =>

   213              error ("Parameter " ^ quote name ^

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

   215     (* string -> int -> string -> int list *)

   216     fun int_seq_from_string name min_int s =

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

   218     (* string -> int -> int list *)

   219     fun lookup_int_seq name min_int =

   220       case lookup name of

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

   222                      [] => [min_int]

   223                    | value => value)

   224       | NONE => [min_int]

   225     (* (string -> 'a) -> int -> string -> ('a option * int list) list *)

   226     fun lookup_ints_assigns read prefix min_int =

   227       (NONE, lookup_int_seq prefix min_int)

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

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

   230                   value |> stringify_raw_param_value

   231                         |> int_seq_from_string name min_int))

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

   233     (* (string -> 'a) -> string -> ('a option * bool) list *)

   234     fun lookup_bool_assigns read prefix =

   235       (NONE, lookup_bool prefix)

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

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

   238                   value |> stringify_raw_param_value

   239                         |> Sledgehammer_Util.parse_bool_option false name

   240                         |> the))

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

   242     (* (string -> 'a) -> string -> ('a option * bool option) list *)

   243     fun lookup_bool_option_assigns read prefix =

   244       (NONE, lookup_bool_option prefix)

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

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

   247                   value |> stringify_raw_param_value

   248                         |> Sledgehammer_Util.parse_bool_option true name))

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

   250     (* string -> Time.time option *)

   251     fun lookup_time name =

   252       case lookup name of

   253         NONE => NONE

   254       | SOME s => Sledgehammer_Util.parse_time_option name s

   255     (* string -> term list *)

   256     val lookup_term_list =

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

   258     val read_type_polymorphic =

   259       Syntax.read_typ ctxt #> Logic.mk_type

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

   261     (* string -> term *)

   262     val read_term_polymorphic =

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

   264     (* string -> styp *)

   265     val read_const_polymorphic = read_term_polymorphic #> dest_Const

   266     val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1

   267     val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1

   268     val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0

   269     val bitss = lookup_int_seq "bits" 1

   270     val bisim_depths = lookup_int_seq "bisim_depth" ~1

   271     val boxes = lookup_bool_option_assigns read_type_polymorphic "box"

   272     val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"

   273     val monos = lookup_bool_option_assigns read_type_polymorphic "mono"

   274     val stds = lookup_bool_assigns read_type_polymorphic "std"

   275     val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"

   276     val sat_solver = lookup_string "sat_solver"

   277     val blocking = not auto andalso lookup_bool "blocking"

   278     val falsify = lookup_bool "falsify"

   279     val debug = not auto andalso lookup_bool "debug"

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

   281     val overlord = lookup_bool "overlord"

   282     val user_axioms = lookup_bool_option "user_axioms"

   283     val assms = lookup_bool "assms"

   284     val merge_type_vars = lookup_bool "merge_type_vars"

   285     val binary_ints = lookup_bool_option "binary_ints"

   286     val destroy_constrs = lookup_bool "destroy_constrs"

   287     val specialize = lookup_bool "specialize"

   288     val skolemize = lookup_bool "skolemize"

   289     val star_linear_preds = lookup_bool "star_linear_preds"

   290     val uncurry = lookup_bool "uncurry"

   291     val fast_descrs = lookup_bool "fast_descrs"

   292     val peephole_optim = lookup_bool "peephole_optim"

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

   294     val tac_timeout = lookup_time "tac_timeout"

   295     val sym_break = Int.max (0, lookup_int "sym_break")

   296     val sharing_depth = Int.max (1, lookup_int "sharing_depth")

   297     val flatten_props = lookup_bool "flatten_props"

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

   299     val show_all = debug orelse lookup_bool "show_all"

   300     val show_skolems = show_all orelse lookup_bool "show_skolems"

   301     val show_datatypes = show_all orelse lookup_bool "show_datatypes"

   302     val show_consts = show_all orelse lookup_bool "show_consts"

   303     val formats = lookup_ints_assigns read_term_polymorphic "format" 0

   304     val evals = lookup_term_list "eval"

   305     val max_potential =

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

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

   308     val check_potential = lookup_bool "check_potential"

   309     val check_genuine = lookup_bool "check_genuine"

   310     val batch_size = case lookup_int_option "batch_size" of

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

   312                      | NONE => if debug then 1 else 64

   313     val expect = lookup_string "expect"

   314   in

   315     {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,

   316      iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,

   317      boxes = boxes, finitizes = finitizes, monos = monos, stds = stds,

   318      wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,

   319      debug = debug, verbose = verbose, overlord = overlord,

   320      user_axioms = user_axioms, assms = assms,

   321      merge_type_vars = merge_type_vars, binary_ints = binary_ints,

   322      destroy_constrs = destroy_constrs, specialize = specialize,

   323      skolemize = skolemize, star_linear_preds = star_linear_preds,

   324      uncurry = uncurry, fast_descrs = fast_descrs,

   325      peephole_optim = peephole_optim, timeout = timeout,

   326      tac_timeout = tac_timeout, sym_break = sym_break,

   327      sharing_depth = sharing_depth, flatten_props = flatten_props,

   328      max_threads = max_threads, show_skolems = show_skolems,

   329      show_datatypes = show_datatypes, show_consts = show_consts,

   330      formats = formats, evals = evals, max_potential = max_potential,

   331      max_genuine = max_genuine, check_potential = check_potential,

   332      check_genuine = check_genuine, batch_size = batch_size, expect = expect}

   333   end

   335 (* theory -> (string * string) list -> params *)

   336 fun default_params thy =

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

   338   o map (apsnd single)

   340 (* P.token list -> string * P.token list *)

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

   342 (* P.token list -> string list * P.token list *)

   343 val parse_value =

   344   Scan.repeat1 (P.minus >> single

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

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

   347 (* P.token list -> raw_param * P.token list *)

   348 val parse_param =

   349   parse_key -- (Scan.option (P.$$$ "=" |-- parse_value) >> these)

   350 (* P.token list -> raw_param list option * P.token list *)

   351 val parse_params = Scan.option (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]")

   353 (* Proof.context -> ('a -> 'a) -> 'a -> 'a *)

   354 fun handle_exceptions ctxt f x =

   355   f x

   356   handle ARG (loc, details) =>

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

   358        | BAD (loc, details) =>

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

   360        | NOT_SUPPORTED details =>

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

   362        | NUT (loc, us) =>

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

   364                 " (" ^ quote loc ^ "): " ^

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

   366        | REP (loc, Rs) =>

   367          error ("Invalid representation" ^ plural_s_for_list Rs ^

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

   369        | TERM (loc, ts) =>

   370          error ("Invalid term" ^ plural_s_for_list ts ^

   371                 " (" ^ quote loc ^ "): " ^

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

   373        | TOO_LARGE (_, details) =>

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

   375        | TOO_SMALL (_, details) =>

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

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

   378          error ("Invalid type" ^ plural_s_for_list Ts ^

   379                 (if null ts then

   380                    ""

   381                  else

   382                    " for term" ^ plural_s_for_list ts ^ " " ^

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

   384                 " (" ^ quote loc ^ "): " ^

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

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

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

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

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

   391 (* raw_param list -> bool -> int -> int -> Proof.state -> bool * Proof.state *)

   392 fun pick_nits override_params auto i step state =

   393   let

   394     val thy = Proof.theory_of state

   395     val ctxt = Proof.context_of state

   396     val _ = List.app check_raw_param override_params

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

   398       extract_params ctxt auto (default_raw_params thy) override_params

   399     (* unit -> bool * Proof.state *)

   400     fun go () =

   401       (false, state)

   402       |> (if auto then perhaps o try

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

   404           else handle_exceptions ctxt)

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

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

   407   in

   408     if auto orelse blocking then go ()

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

   410   end

   412 (* raw_param list option * int option -> Toplevel.transition

   413    -> Toplevel.transition *)

   414 fun nitpick_trans (opt_params, opt_i) =

   415   Toplevel.keep (fn st =>

   416       (pick_nits (these opt_params) false (the_default 1 opt_i)

   417                  (Toplevel.proof_position_of st) (Toplevel.proof_of st); ()))

   419 (* raw_param -> string *)

   420 fun string_for_raw_param (name, value) =

   421   name ^ " = " ^ stringify_raw_param_value value

   423 (* raw_param list option -> Toplevel.transition -> Toplevel.transition *)

   424 fun nitpick_params_trans opt_params =

   425   Toplevel.theory

   426       (fold set_default_raw_param (these opt_params)

   427        #> tap (fn thy =>

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

   429                            (case rev (default_raw_params thy) of

   430                               [] => "none"

   431                             | params =>

   432                               (map check_raw_param params;

   433                                params |> map string_for_raw_param

   434                                       |> sort_strings |> cat_lines)))))

   436 (* P.token list

   437    -> (Toplevel.transition -> Toplevel.transition) * P.token list *)

   438 val parse_nitpick_command =

   439   (parse_params -- Scan.option P.nat) #>> nitpick_trans

   440 val parse_nitpick_params_command = parse_params #>> nitpick_params_trans

   442 val _ = OuterSyntax.improper_command "nitpick"

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

   444             K.diag parse_nitpick_command

   445 val _ = OuterSyntax.command "nitpick_params"

   446             "set and display the default parameters for Nitpick"

   447             K.thy_decl parse_nitpick_params_command

   449 (* Proof.state -> bool * Proof.state *)

   450 fun auto_nitpick state =

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

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

   455 end;

author	blanchet
	Tue, 23 Mar 2010 11:40:46 +0100
changeset 35962	77f2cb359b49
parent 35866	513074557e06
child 35966	b7f98ff9c7d9
permissions	-rw-r--r--