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

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

     2     Author:     Jasmin Blanchette, TU Muenchen

     3     Copyright   2008, 2009

     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 default_params : theory -> (string * string) list -> params

    14 end

    16 structure NitpickIsar : NITPICK_ISAR =

    17 struct

    19 open NitpickUtil

    20 open NitpickHOL

    21 open NitpickRep

    22 open NitpickNut

    23 open Nitpick

    25 type raw_param = string * string list

    27 val default_default_params =

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

    29    ("iter", ["0,1,2,4,8,12,16,24"]),

    30    ("bisim_depth", ["7"]),

    31    ("box", ["smart"]),

    32    ("mono", ["smart"]),

    33    ("wf", ["smart"]),

    34    ("sat_solver", ["smart"]),

    35    ("batch_size", ["smart"]),

    36    ("auto", ["false"]),

    37    ("blocking", ["true"]),

    38    ("falsify", ["true"]),

    39    ("user_axioms", ["smart"]),

    40    ("assms", ["true"]),

    41    ("coalesce_type_vars", ["false"]),

    42    ("destroy_constrs", ["true"]),

    43    ("specialize", ["true"]),

    44    ("skolemize", ["true"]),

    45    ("star_linear_preds", ["true"]),

    46    ("uncurry", ["true"]),

    47    ("fast_descrs", ["true"]),

    48    ("peephole_optim", ["true"]),

    49    ("timeout", ["30 s"]),

    50    ("auto_timeout", ["5 s"]),

    51    ("tac_timeout", ["500 ms"]),

    52    ("sym_break", ["20"]),

    53    ("sharing_depth", ["3"]),

    54    ("flatten_props", ["false"]),

    55    ("max_threads", ["0"]),

    56    ("verbose", ["false"]),

    57    ("debug", ["false"]),

    58    ("overlord", ["false"]),

    59    ("show_all", ["false"]),

    60    ("show_skolems", ["true"]),

    61    ("show_datatypes", ["false"]),

    62    ("show_consts", ["false"]),

    63    ("format", ["1"]),

    64    ("max_potential", ["1"]),

    65    ("max_genuine", ["1"]),

    66    ("check_potential", ["false"]),

    67    ("check_genuine", ["false"])]

    69 val negated_params =

    70   [("dont_box", "box"),

    71    ("non_mono", "mono"),

    72    ("non_wf", "wf"),

    73    ("no_auto", "auto"),

    74    ("non_blocking", "blocking"),

    75    ("satisfy", "falsify"),

    76    ("no_user_axioms", "user_axioms"),

    77    ("no_assms", "assms"),

    78    ("dont_coalesce_type_vars", "coalesce_type_vars"),

    79    ("dont_destroy_constrs", "destroy_constrs"),

    80    ("dont_specialize", "specialize"),

    81    ("dont_skolemize", "skolemize"),

    82    ("dont_star_linear_preds", "star_linear_preds"),

    83    ("dont_uncurry", "uncurry"),

    84    ("full_descrs", "fast_descrs"),

    85    ("no_peephole_optim", "peephole_optim"),

    86    ("dont_flatten_props", "flatten_props"),

    87    ("quiet", "verbose"),

    88    ("no_debug", "debug"),

    89    ("no_overlord", "overlord"),

    90    ("dont_show_all", "show_all"),

    91    ("hide_skolems", "show_skolems"),

    92    ("hide_datatypes", "show_datatypes"),

    93    ("hide_consts", "show_consts"),

    94    ("trust_potential", "check_potential"),

    95    ("trust_genuine", "check_genuine")]

    97 (* string -> bool *)

    98 fun is_known_raw_param s =

    99   AList.defined (op =) default_default_params s

   100   orelse AList.defined (op =) negated_params s

   101   orelse s mem ["max", "eval", "expect"]

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

   103                 ["card", "max", "iter", "box", "dont_box", "mono", "non_mono",

   104                  "wf", "non_wf", "format"]

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

   107 fun check_raw_param (s, _) =

   108   if is_known_raw_param s then ()

   109   else error ("Unknown parameter " ^ quote s ^ ".")

   111 (* string -> string option *)

   112 fun unnegate_param_name name =

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

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

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

   116             else NONE

   117   | some_name => some_name

   118 (* raw_param -> raw_param *)

   119 fun unnegate_raw_param (name, value) =

   120   case unnegate_param_name name of

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

   122                             ["false"] => ["true"]

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

   124                           | [] => ["false"]

   125                           | _ => value)

   126   | NONE => (name, value)

   128 structure TheoryData = TheoryDataFun(

   129   type T = {params: raw_param list, registered_auto: bool}

   130   val empty = {params = rev default_default_params, registered_auto = false}

   131   val copy = I

   132   val extend = I

   133   fun merge _ ({params = ps1, registered_auto = a1},

   134                {params = ps2, registered_auto = a2}) =

   135     {params = AList.merge (op =) (op =) (ps1, ps2),

   136      registered_auto = a1 orelse a2})

   138 (* raw_param -> theory -> theory *)

   139 fun set_default_raw_param param thy =

   140   let val {params, registered_auto} = TheoryData.get thy in

   141     TheoryData.put

   142       {params = AList.update (op =) (unnegate_raw_param param) params,

   143        registered_auto = registered_auto} thy

   144   end

   145 (* theory -> raw_param list *)

   146 val default_raw_params = #params o TheoryData.get

   148 (* theory -> theory *)

   149 fun set_registered_auto thy =

   150   TheoryData.put {params = default_raw_params thy, registered_auto = true} thy

   151 (* theory -> bool *)

   152 val is_registered_auto = #registered_auto o TheoryData.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 (* bool -> string -> string -> bool option *)

   165 fun bool_option_from_string option name s =

   166   (case s of

   167      "smart" => if option then NONE else raise Option

   168    | "false" => SOME false

   169    | "true" => SOME true

   170    | "" => SOME true

   171    | s => raise Option)

   172   handle Option.Option =>

   173          let val ss = map quote ((option ? cons "smart") ["true", "false"]) in

   174            error ("Parameter " ^ quote name ^ " must be assigned " ^

   175                   space_implode " " (serial_commas "or" ss) ^ ".")

   176          end

   177 (* bool -> raw_param list -> bool option -> string -> bool option *)

   178 fun general_lookup_bool option raw_params default_value name =

   179   case AList.lookup (op =) raw_params name of

   180     SOME s => s |> stringify_raw_param_value

   181                 |> bool_option_from_string option name

   182   | NONE => default_value

   184 (* int -> string -> int *)

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

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

   188 fun extract_params ctxt auto default_params override_params =

   189   let

   190     val override_params = map unnegate_raw_param override_params

   191     val raw_params = rev override_params @ rev default_params

   192     val lookup =

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

   194     (* string -> string *)

   195     fun lookup_string name = the_default "" (lookup name)

   196     (* string -> bool *)

   197     val lookup_bool = the o general_lookup_bool false raw_params (SOME false)

   198     (* string -> bool option *)

   199     val lookup_bool_option = general_lookup_bool true raw_params NONE

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

   201     fun do_int name value =

   202       case value of

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

   204                      SOME i => i

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

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

   207       | NONE => 0

   208     (* string -> int *)

   209     fun lookup_int name = do_int name (lookup name)

   210     (* string -> int option *)

   211     fun lookup_int_option name =

   212       case lookup name of

   213         SOME "smart" => NONE

   214       | value => SOME (do_int name value)

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

   216     fun int_range_from_string name min_int s =

   217       let

   218         val (k1, k2) =

   219           (case space_explode "-" s of

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

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

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

   223            | _ => raise Option)

   224           |> pairself (maxed_int_from_string min_int)

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

   226       handle Option.Option =>

   227              error ("Parameter " ^ quote name ^

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

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

   230     fun int_seq_from_string name min_int s =

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

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

   233     fun lookup_int_seq name min_int =

   234       case lookup name of

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

   236                      [] => [min_int]

   237                    | value => value)

   238       | NONE => [min_int]

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

   240     fun lookup_ints_assigns read prefix min_int =

   241       (NONE, lookup_int_seq prefix min_int)

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

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

   244                   value |> stringify_raw_param_value

   245                         |> int_seq_from_string name min_int))

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

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

   248     fun lookup_bool_option_assigns read prefix =

   249       (NONE, lookup_bool_option prefix)

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

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

   252                   value |> stringify_raw_param_value

   253                         |> bool_option_from_string true name))

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

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

   256     fun lookup_time name =

   257       case lookup name of

   258         NONE => NONE

   259       | SOME "none" => NONE

   260       | SOME s =>

   261         let

   262           val msecs =

   263             case space_explode " " s of

   264               [s1, "min"] => 60000 * the (Int.fromString s1)

   265             | [s1, "s"] => 1000 * the (Int.fromString s1)

   266             | [s1, "ms"] => the (Int.fromString s1)

   267             | _ => 0

   268         in

   269           if msecs <= 0 then

   270             error ("Parameter " ^ quote name ^ " must be assigned a positive \

   271                    \time value (e.g., \"60 s\", \"200 ms\") or \"none\".")

   272           else

   273             SOME (Time.fromMilliseconds msecs)

   274         end

   275     (* string -> term list *)

   276     val lookup_term_list =

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

   278     val read_type_polymorphic =

   279       Syntax.read_typ ctxt #> Logic.mk_type

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

   281     (* string -> term *)

   282     val read_term_polymorphic =

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

   284     (* string -> styp *)

   285     val read_const_polymorphic = read_term_polymorphic #> dest_Const

   286     val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1

   287     val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1

   288     val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0

   289     val bisim_depths = lookup_int_seq "bisim_depth" ~1

   290     val boxes =

   291       lookup_bool_option_assigns read_type_polymorphic "box" @

   292       map_filter (fn (SOME T, _) =>

   293                      if is_fun_type T orelse is_pair_type T then

   294                        SOME (SOME T, SOME true)

   295                      else

   296                        NONE

   297                    | (NONE, _) => NONE) cards_assigns

   298     val monos = lookup_bool_option_assigns read_type_polymorphic "mono"

   299     val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"

   300     val sat_solver = lookup_string "sat_solver"

   301     val blocking = not auto andalso lookup_bool "blocking"

   302     val falsify = lookup_bool "falsify"

   303     val debug = not auto andalso lookup_bool "debug"

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

   305     val overlord = lookup_bool "overlord"

   306     val user_axioms = lookup_bool_option "user_axioms"

   307     val assms = lookup_bool "assms"

   308     val coalesce_type_vars = lookup_bool "coalesce_type_vars"

   309     val destroy_constrs = lookup_bool "destroy_constrs"

   310     val specialize = lookup_bool "specialize"

   311     val skolemize = lookup_bool "skolemize"

   312     val star_linear_preds = lookup_bool "star_linear_preds"

   313     val uncurry = lookup_bool "uncurry"

   314     val fast_descrs = lookup_bool "fast_descrs"

   315     val peephole_optim = lookup_bool "peephole_optim"

   316     val timeout = if auto then lookup_time "auto_timeout"

   317                   else lookup_time "timeout"

   318     val tac_timeout = lookup_time "tac_timeout"

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

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

   321     val flatten_props = lookup_bool "flatten_props"

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

   323     val show_all = debug orelse lookup_bool "show_all"

   324     val show_skolems = show_all orelse lookup_bool "show_skolems"

   325     val show_datatypes = show_all orelse lookup_bool "show_datatypes"

   326     val show_consts = show_all orelse lookup_bool "show_consts"

   327     val formats = lookup_ints_assigns read_term_polymorphic "format" 0

   328     val evals = lookup_term_list "eval"

   329     val max_potential = if auto then 0

   330                         else Int.max (0, lookup_int "max_potential")

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

   332     val check_potential = lookup_bool "check_potential"

   333     val check_genuine = lookup_bool "check_genuine"

   334     val batch_size = case lookup_int_option "batch_size" of

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

   336                      | NONE => if debug then 1 else 64

   337     val expect = lookup_string "expect"

   338   in

   339     {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,

   340      iters_assigns = iters_assigns, bisim_depths = bisim_depths, boxes = boxes,

   341      monos = monos, wfs = wfs, sat_solver = sat_solver, blocking = blocking,

   342      falsify = falsify, debug = debug, verbose = verbose, overlord = overlord,

   343      user_axioms = user_axioms, assms = assms,

   344      coalesce_type_vars = coalesce_type_vars, destroy_constrs = destroy_constrs,

   345      specialize = specialize, skolemize = skolemize,

   346      star_linear_preds = star_linear_preds, uncurry = uncurry,

   347      fast_descrs = fast_descrs, peephole_optim = peephole_optim,

   348      timeout = timeout, tac_timeout = tac_timeout, sym_break = sym_break,

   349      sharing_depth = sharing_depth, flatten_props = flatten_props,

   350      max_threads = max_threads, show_skolems = show_skolems,

   351      show_datatypes = show_datatypes, show_consts = show_consts,

   352      formats = formats, evals = evals, max_potential = max_potential,

   353      max_genuine = max_genuine, check_potential = check_potential,

   354      check_genuine = check_genuine, batch_size = batch_size, expect = expect}

   355   end

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

   358 fun default_params thy =

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

   360   o map (apsnd single)

   362 (* OuterParse.token list -> string * OuterParse.token list *)

   363 val scan_key = Scan.repeat1 OuterParse.typ_group >> space_implode " "

   365 (* OuterParse.token list -> string list * OuterParse.token list *)

   366 val scan_value =

   367   Scan.repeat1 (OuterParse.minus >> single

   368                 || Scan.repeat1 (Scan.unless OuterParse.minus OuterParse.name)

   369                 || OuterParse.$$$ "," |-- OuterParse.number >> prefix ","

   370                    >> single) >> flat

   372 (* OuterParse.token list -> raw_param * OuterParse.token list *)

   373 val scan_param =

   374   scan_key -- (Scan.option (OuterParse.$$$ "=" |-- scan_value) >> these)

   375 (* OuterParse.token list -> raw_param list option * OuterParse.token list *)

   376 val scan_params = Scan.option (OuterParse.$$$ "[" |-- OuterParse.list scan_param

   377                                --| OuterParse.$$$ "]")

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

   380 fun handle_exceptions ctxt f x =

   381   f x

   382   handle ARG (loc, details) =>

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

   384        | BAD (loc, details) =>

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

   386        | LIMIT (_, details) =>

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

   388        | NOT_SUPPORTED details =>

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

   390        | NUT (loc, us) =>

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

   392                 " (" ^ quote loc ^ "): " ^

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

   394        | REP (loc, Rs) =>

   395          error ("Invalid representation" ^ plural_s_for_list Rs ^

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

   397        | TERM (loc, ts) =>

   398          error ("Invalid term" ^ plural_s_for_list ts ^

   399                 " (" ^ quote loc ^ "): " ^

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

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

   402          error ("Invalid type" ^ plural_s_for_list Ts ^

   403                 (if null ts then

   404                    ""

   405                  else

   406                    " for term" ^ plural_s_for_list ts ^ " " ^

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

   408                 " (" ^ quote loc ^ "): " ^

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

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

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

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

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

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

   416 fun pick_nits override_params auto subgoal state =

   417   let

   418     val thy = Proof.theory_of state

   419     val ctxt = Proof.context_of state

   420     val thm = snd (snd (Proof.get_goal state))

   421     val _ = List.app check_raw_param override_params

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

   423       extract_params ctxt auto (default_raw_params thy) override_params

   424     (* unit -> Proof.state *)

   425     fun go () =

   426       (if auto then perhaps o try

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

   428        else handle_exceptions ctxt)

   429       (fn state => pick_nits_in_subgoal state params auto subgoal |> snd)

   430       state

   431   in

   432     if auto orelse blocking then

   433       go ()

   434     else

   435       (SimpleThread.fork true (fn () => (go (); ()) handle Exn.Interrupt => ());

   436        state)

   437   end

   439 (* (TableFun().key * string list) list option * int option

   440    -> Toplevel.transition -> Toplevel.transition *)

   441 fun nitpick_trans (opt_params, opt_subgoal) =

   442   Toplevel.keep (K ()

   443       o pick_nits (these opt_params) false (the_default 1 opt_subgoal)

   444       o Toplevel.proof_of)

   446 (* raw_param -> string *)

   447 fun string_for_raw_param (name, value) =

   448   name ^ " = " ^ stringify_raw_param_value value

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

   451 fun pick_nits_auto interactive state =

   452   let val thy = Proof.theory_of state in

   453     ((interactive andalso not (!Toplevel.quiet)

   454       andalso the (general_lookup_bool false (default_raw_params thy)

   455                   (SOME false) "auto"))

   456      ? pick_nits [] true 0) state

   457   end

   459 (* theory -> theory *)

   460 fun register_auto thy =

   461   (not (is_registered_auto thy)

   462    ? (set_registered_auto

   463       #> Context.theory_map (Specification.add_theorem_hook pick_nits_auto)))

   464   thy

   466 (* (TableFun().key * string) list option -> Toplevel.transition

   467    -> Toplevel.transition *)

   468 fun nitpick_params_trans opt_params =

   469   Toplevel.theory

   470       (fn thy =>

   471           let val thy = fold set_default_raw_param (these opt_params) thy in

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

   473                      (case rev (default_raw_params thy) of

   474                         [] => "none"

   475                       | params =>

   476                         (map check_raw_param params;

   477                          params |> map string_for_raw_param |> sort_strings

   478                                 |> cat_lines)));

   479             register_auto thy

   480           end)

   482 (* OuterParse.token list

   483    -> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)

   484 fun scan_nitpick_command tokens =

   485   (scan_params -- Scan.option OuterParse.nat) tokens |>> nitpick_trans

   486 fun scan_nitpick_params_command tokens =

   487   scan_params tokens |>> nitpick_params_trans

   489 val _ = OuterSyntax.improper_command "nitpick"

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

   491             OuterKeyword.diag scan_nitpick_command

   492 val _ = OuterSyntax.command "nitpick_params"

   493             "set and display the default parameters for Nitpick"

   494             OuterKeyword.thy_decl scan_nitpick_params_command

   496 end;

author	blanchet
	Fri, 23 Oct 2009 18:59:24 +0200
changeset 33197	de6285ebcc05
parent 33192	08a39a957ed7
child 33220	11a1af478dac
permissions	-rw-r--r--