src/HOL/Tools/Nitpick/nitpick_isar.ML
author blanchet
Fri Mar 19 15:07:44 2010 +0100 (2010-03-19)
changeset 35866 513074557e06
parent 35665 ff2bf50505ab
child 35964 77f2cb359b49
permissions -rw-r--r--
move the Sledgehammer Isar commands together into one file;
this will make easier to add options and reorganize them later
     1 (*  Title:      HOL/Tools/Nitpick/nitpick_isar.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2008, 2009, 2010
     4 
     5 Adds the "nitpick" and "nitpick_params" commands to Isabelle/Isar's outer
     6 syntax.
     7 *)
     8 
     9 signature NITPICK_ISAR =
    10 sig
    11   type params = Nitpick.params
    12 
    13   val auto: bool Unsynchronized.ref
    14   val default_params : theory -> (string * string) list -> params
    15   val setup : theory -> theory
    16 end;
    17 
    18 structure Nitpick_Isar : NITPICK_ISAR =
    19 struct
    20 
    21 open Nitpick_Util
    22 open Nitpick_HOL
    23 open Nitpick_Rep
    24 open Nitpick_Nut
    25 open Nitpick
    26 
    27 val auto = Unsynchronized.ref false;
    28 
    29 val _ =
    30   ProofGeneralPgip.add_preference Preferences.category_tracing
    31       (Preferences.bool_pref auto "auto-nitpick"
    32            "Whether to run Nitpick automatically.")
    33 
    34 type raw_param = string * string list
    35 
    36 val default_default_params =
    37   [("card", ["1\<midarrow>8"]),
    38    ("iter", ["0,1,2,4,8,12,16,24"]),
    39    ("bits", ["1,2,3,4,6,8,10,12"]),
    40    ("bisim_depth", ["7"]),
    41    ("box", ["smart"]),
    42    ("finitize", ["smart"]),
    43    ("mono", ["smart"]),
    44    ("std", ["true"]),
    45    ("wf", ["smart"]),
    46    ("sat_solver", ["smart"]),
    47    ("batch_size", ["smart"]),
    48    ("blocking", ["true"]),
    49    ("falsify", ["true"]),
    50    ("user_axioms", ["smart"]),
    51    ("assms", ["true"]),
    52    ("merge_type_vars", ["false"]),
    53    ("binary_ints", ["smart"]),
    54    ("destroy_constrs", ["true"]),
    55    ("specialize", ["true"]),
    56    ("skolemize", ["true"]),
    57    ("star_linear_preds", ["true"]),
    58    ("uncurry", ["true"]),
    59    ("fast_descrs", ["true"]),
    60    ("peephole_optim", ["true"]),
    61    ("timeout", ["30 s"]),
    62    ("tac_timeout", ["500 ms"]),
    63    ("sym_break", ["20"]),
    64    ("sharing_depth", ["3"]),
    65    ("flatten_props", ["false"]),
    66    ("max_threads", ["0"]),
    67    ("verbose", ["false"]),
    68    ("debug", ["false"]),
    69    ("overlord", ["false"]),
    70    ("show_all", ["false"]),
    71    ("show_skolems", ["true"]),
    72    ("show_datatypes", ["false"]),
    73    ("show_consts", ["false"]),
    74    ("format", ["1"]),
    75    ("max_potential", ["1"]),
    76    ("max_genuine", ["1"]),
    77    ("check_potential", ["false"]),
    78    ("check_genuine", ["false"])]
    79 
    80 val negated_params =
    81   [("dont_box", "box"),
    82    ("dont_finitize", "finitize"),
    83    ("non_mono", "mono"),
    84    ("non_std", "std"),
    85    ("non_wf", "wf"),
    86    ("non_blocking", "blocking"),
    87    ("satisfy", "falsify"),
    88    ("no_user_axioms", "user_axioms"),
    89    ("no_assms", "assms"),
    90    ("dont_merge_type_vars", "merge_type_vars"),
    91    ("unary_ints", "binary_ints"),
    92    ("dont_destroy_constrs", "destroy_constrs"),
    93    ("dont_specialize", "specialize"),
    94    ("dont_skolemize", "skolemize"),
    95    ("dont_star_linear_preds", "star_linear_preds"),
    96    ("dont_uncurry", "uncurry"),
    97    ("full_descrs", "fast_descrs"),
    98    ("no_peephole_optim", "peephole_optim"),
    99    ("dont_flatten_props", "flatten_props"),
   100    ("quiet", "verbose"),
   101    ("no_debug", "debug"),
   102    ("no_overlord", "overlord"),
   103    ("dont_show_all", "show_all"),
   104    ("hide_skolems", "show_skolems"),
   105    ("hide_datatypes", "show_datatypes"),
   106    ("hide_consts", "show_consts"),
   107    ("trust_potential", "check_potential"),
   108    ("trust_genuine", "check_genuine")]
   109 
   110 (* string -> bool *)
   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   s = "max" orelse s = "eval" orelse s = "expect" orelse
   115   exists (fn p => String.isPrefix (p ^ " ") s)
   116          ["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
   117           "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"]
   118 
   119 (* string * 'a -> unit *)
   120 fun check_raw_param (s, _) =
   121   if is_known_raw_param s then ()
   122   else error ("Unknown parameter " ^ quote s ^ ".")  
   123 
   124 (* string -> string option *)
   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 (* raw_param -> raw_param *)
   132 fun unnegate_raw_param (name, value) =
   133   case unnegate_param_name name of
   134     SOME name' => (name', case value of
   135                             ["false"] => ["true"]
   136                           | ["true"] => ["false"]
   137                           | [] => ["false"]
   138                           | _ => value)
   139   | NONE => (name, value)
   140 
   141 structure Data = Theory_Data(
   142   type T = {params: raw_param list}
   143   val empty = {params = rev default_default_params}
   144   val extend = I
   145   fun merge ({params = ps1}, {params = ps2}) : T =
   146     {params = AList.merge (op =) (K true) (ps1, ps2)})
   147 
   148 (* raw_param -> theory -> theory *)
   149 fun set_default_raw_param param thy =
   150   let val {params} = Data.get thy in
   151     Data.put {params = AList.update (op =) (unnegate_raw_param param) params}
   152              thy
   153   end
   154 (* theory -> raw_param list *)
   155 val default_raw_params = #params o Data.get
   156 
   157 (* string -> bool *)
   158 fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
   159 
   160 (* string list -> string *)
   161 fun stringify_raw_param_value [] = ""
   162   | stringify_raw_param_value [s] = s
   163   | stringify_raw_param_value (s1 :: s2 :: ss) =
   164     s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^
   165     stringify_raw_param_value (s2 :: ss)
   166 
   167 (* bool -> string -> string -> bool option *)
   168 fun bool_option_from_string option name s =
   169   (case s of
   170      "smart" => if option then NONE else raise Option
   171    | "false" => SOME false
   172    | "true" => SOME true
   173    | "" => SOME true
   174    | _ => raise Option)
   175   handle Option.Option =>
   176          let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
   177            error ("Parameter " ^ quote name ^ " must be assigned " ^
   178                   space_implode " " (serial_commas "or" ss) ^ ".")
   179          end
   180 (* bool -> raw_param list -> bool option -> string -> bool option *)
   181 fun general_lookup_bool option raw_params default_value name =
   182   case AList.lookup (op =) raw_params name of
   183     SOME s => s |> stringify_raw_param_value
   184                 |> bool_option_from_string option name
   185   | NONE => default_value
   186 
   187 (* int -> string -> int *)
   188 fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))
   189 
   190 (* Proof.context -> bool -> raw_param list -> raw_param list -> params *)
   191 fun extract_params ctxt auto default_params override_params =
   192   let
   193     val override_params = map unnegate_raw_param override_params
   194     val raw_params = rev override_params @ rev default_params
   195     val lookup =
   196       Option.map stringify_raw_param_value o AList.lookup (op =) raw_params
   197     (* string -> string *)
   198     fun lookup_string name = the_default "" (lookup name)
   199     (* string -> bool *)
   200     val lookup_bool = the o general_lookup_bool false raw_params (SOME false)
   201     (* string -> bool option *)
   202     val lookup_bool_option = general_lookup_bool true raw_params NONE
   203     (* string -> string option -> int *)
   204     fun do_int name value =
   205       case value of
   206         SOME s => (case Int.fromString s of
   207                      SOME i => i
   208                    | NONE => error ("Parameter " ^ quote name ^
   209                                     " must be assigned an integer value."))
   210       | NONE => 0
   211     (* string -> int *)
   212     fun lookup_int name = do_int name (lookup name)
   213     (* string -> int option *)
   214     fun lookup_int_option name =
   215       case lookup name of
   216         SOME "smart" => NONE
   217       | value => SOME (do_int name value)
   218     (* string -> int -> string -> int list *)
   219     fun int_range_from_string name min_int s =
   220       let
   221         val (k1, k2) =
   222           (case space_explode "-" s of
   223              [s] => the_default (s, s) (first_field "\<midarrow>" s)
   224            | ["", s2] => ("-" ^ s2, "-" ^ s2)
   225            | [s1, s2] => (s1, s2)
   226            | _ => raise Option)
   227           |> pairself (maxed_int_from_string min_int)
   228       in if k1 <= k2 then k1 upto k2 else k1 downto k2 end
   229       handle Option.Option =>
   230              error ("Parameter " ^ quote name ^
   231                     " must be assigned a sequence of integers.")
   232     (* string -> int -> string -> int list *)
   233     fun int_seq_from_string name min_int s =
   234       maps (int_range_from_string name min_int) (space_explode "," s)
   235     (* string -> int -> int list *)
   236     fun lookup_int_seq name min_int =
   237       case lookup name of
   238         SOME s => (case int_seq_from_string name min_int s of
   239                      [] => [min_int]
   240                    | value => value)
   241       | NONE => [min_int]
   242     (* (string -> 'a) -> int -> string -> ('a option * int list) list *)
   243     fun lookup_ints_assigns read prefix min_int =
   244       (NONE, lookup_int_seq prefix min_int)
   245       :: map (fn (name, value) =>
   246                  (SOME (read (String.extract (name, size prefix + 1, NONE))),
   247                   value |> stringify_raw_param_value
   248                         |> int_seq_from_string name min_int))
   249              (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
   250     (* (string -> 'a) -> string -> ('a option * bool) list *)
   251     fun lookup_bool_assigns read prefix =
   252       (NONE, lookup_bool prefix)
   253       :: map (fn (name, value) =>
   254                  (SOME (read (String.extract (name, size prefix + 1, NONE))),
   255                   value |> stringify_raw_param_value
   256                         |> bool_option_from_string false name |> the))
   257              (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
   258     (* (string -> 'a) -> string -> ('a option * bool option) list *)
   259     fun lookup_bool_option_assigns read prefix =
   260       (NONE, lookup_bool_option prefix)
   261       :: map (fn (name, value) =>
   262                  (SOME (read (String.extract (name, size prefix + 1, NONE))),
   263                   value |> stringify_raw_param_value
   264                         |> bool_option_from_string true name))
   265              (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
   266     (* string -> Time.time option *)
   267     fun lookup_time name =
   268       case lookup name of
   269         NONE => NONE
   270       | SOME "none" => NONE
   271       | SOME s =>
   272         let
   273           val msecs =
   274             case space_explode " " s of
   275               [s1, "min"] => 60000 * the (Int.fromString s1)
   276             | [s1, "s"] => 1000 * the (Int.fromString s1)
   277             | [s1, "ms"] => the (Int.fromString s1)
   278             | _ => 0
   279         in
   280           if msecs <= 0 then
   281             error ("Parameter " ^ quote name ^ " must be assigned a positive \
   282                    \time value (e.g., \"60 s\", \"200 ms\") or \"none\".")
   283           else
   284             SOME (Time.fromMilliseconds msecs)
   285         end
   286     (* string -> term list *)
   287     val lookup_term_list =
   288       AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt
   289     val read_type_polymorphic =
   290       Syntax.read_typ ctxt #> Logic.mk_type
   291       #> singleton (Variable.polymorphic ctxt) #> Logic.dest_type
   292     (* string -> term *)
   293     val read_term_polymorphic =
   294       Syntax.read_term ctxt #> singleton (Variable.polymorphic ctxt)
   295     (* string -> styp *)
   296     val read_const_polymorphic = read_term_polymorphic #> dest_Const
   297     val cards_assigns = lookup_ints_assigns read_type_polymorphic "card" 1
   298     val maxes_assigns = lookup_ints_assigns read_const_polymorphic "max" ~1
   299     val iters_assigns = lookup_ints_assigns read_const_polymorphic "iter" 0
   300     val bitss = lookup_int_seq "bits" 1
   301     val bisim_depths = lookup_int_seq "bisim_depth" ~1
   302     val boxes = lookup_bool_option_assigns read_type_polymorphic "box"
   303     val finitizes = lookup_bool_option_assigns read_type_polymorphic "finitize"
   304     val monos = lookup_bool_option_assigns read_type_polymorphic "mono"
   305     val stds = lookup_bool_assigns read_type_polymorphic "std"
   306     val wfs = lookup_bool_option_assigns read_const_polymorphic "wf"
   307     val sat_solver = lookup_string "sat_solver"
   308     val blocking = not auto andalso lookup_bool "blocking"
   309     val falsify = lookup_bool "falsify"
   310     val debug = not auto andalso lookup_bool "debug"
   311     val verbose = debug orelse (not auto andalso lookup_bool "verbose")
   312     val overlord = lookup_bool "overlord"
   313     val user_axioms = lookup_bool_option "user_axioms"
   314     val assms = lookup_bool "assms"
   315     val merge_type_vars = lookup_bool "merge_type_vars"
   316     val binary_ints = lookup_bool_option "binary_ints"
   317     val destroy_constrs = lookup_bool "destroy_constrs"
   318     val specialize = lookup_bool "specialize"
   319     val skolemize = lookup_bool "skolemize"
   320     val star_linear_preds = lookup_bool "star_linear_preds"
   321     val uncurry = lookup_bool "uncurry"
   322     val fast_descrs = lookup_bool "fast_descrs"
   323     val peephole_optim = lookup_bool "peephole_optim"
   324     val timeout = if auto then NONE else lookup_time "timeout"
   325     val tac_timeout = lookup_time "tac_timeout"
   326     val sym_break = Int.max (0, lookup_int "sym_break")
   327     val sharing_depth = Int.max (1, lookup_int "sharing_depth")
   328     val flatten_props = lookup_bool "flatten_props"
   329     val max_threads = Int.max (0, lookup_int "max_threads")
   330     val show_all = debug orelse lookup_bool "show_all"
   331     val show_skolems = show_all orelse lookup_bool "show_skolems"
   332     val show_datatypes = show_all orelse lookup_bool "show_datatypes"
   333     val show_consts = show_all orelse lookup_bool "show_consts"
   334     val formats = lookup_ints_assigns read_term_polymorphic "format" 0
   335     val evals = lookup_term_list "eval"
   336     val max_potential =
   337       if auto then 0 else Int.max (0, lookup_int "max_potential")
   338     val max_genuine = Int.max (0, lookup_int "max_genuine")
   339     val check_potential = lookup_bool "check_potential"
   340     val check_genuine = lookup_bool "check_genuine"
   341     val batch_size = case lookup_int_option "batch_size" of
   342                        SOME n => Int.max (1, n)
   343                      | NONE => if debug then 1 else 64
   344     val expect = lookup_string "expect"
   345   in
   346     {cards_assigns = cards_assigns, maxes_assigns = maxes_assigns,
   347      iters_assigns = iters_assigns, bitss = bitss, bisim_depths = bisim_depths,
   348      boxes = boxes, finitizes = finitizes, monos = monos, stds = stds,
   349      wfs = wfs, sat_solver = sat_solver, blocking = blocking, falsify = falsify,
   350      debug = debug, verbose = verbose, overlord = overlord,
   351      user_axioms = user_axioms, assms = assms,
   352      merge_type_vars = merge_type_vars, binary_ints = binary_ints,
   353      destroy_constrs = destroy_constrs, specialize = specialize,
   354      skolemize = skolemize, star_linear_preds = star_linear_preds,
   355      uncurry = uncurry, fast_descrs = fast_descrs,
   356      peephole_optim = peephole_optim, timeout = timeout,
   357      tac_timeout = tac_timeout, sym_break = sym_break,
   358      sharing_depth = sharing_depth, flatten_props = flatten_props,
   359      max_threads = max_threads, show_skolems = show_skolems,
   360      show_datatypes = show_datatypes, show_consts = show_consts,
   361      formats = formats, evals = evals, max_potential = max_potential,
   362      max_genuine = max_genuine, check_potential = check_potential,
   363      check_genuine = check_genuine, batch_size = batch_size, expect = expect}
   364   end
   365 
   366 (* theory -> (string * string) list -> params *)
   367 fun default_params thy =
   368   extract_params (ProofContext.init thy) false (default_raw_params thy)
   369   o map (apsnd single)
   370 
   371 (* OuterParse.token list -> string * OuterParse.token list *)
   372 val scan_key = Scan.repeat1 OuterParse.typ_group >> space_implode " "
   373 
   374 (* OuterParse.token list -> string list * OuterParse.token list *)
   375 val scan_value =
   376   Scan.repeat1 (OuterParse.minus >> single
   377                 || Scan.repeat1 (Scan.unless OuterParse.minus OuterParse.name)
   378                 || OuterParse.$$$ "," |-- OuterParse.number >> prefix ","
   379                    >> single) >> flat
   380 
   381 (* OuterParse.token list -> raw_param * OuterParse.token list *)
   382 val scan_param =
   383   scan_key -- (Scan.option (OuterParse.$$$ "=" |-- scan_value) >> these)
   384 (* OuterParse.token list -> raw_param list option * OuterParse.token list *)
   385 val scan_params = Scan.option (OuterParse.$$$ "[" |-- OuterParse.list scan_param
   386                                --| OuterParse.$$$ "]")
   387 
   388 (* Proof.context -> ('a -> 'a) -> 'a -> 'a *)
   389 fun handle_exceptions ctxt f x =
   390   f x
   391   handle ARG (loc, details) =>
   392          error ("Bad argument(s) to " ^ quote loc ^ ": " ^ details ^ ".")
   393        | BAD (loc, details) =>
   394          error ("Internal error (" ^ quote loc ^ "): " ^ details ^ ".")
   395        | NOT_SUPPORTED details =>
   396          (warning ("Unsupported case: " ^ details ^ "."); x)
   397        | NUT (loc, us) =>
   398          error ("Invalid intermediate term" ^ plural_s_for_list us ^
   399                 " (" ^ quote loc ^ "): " ^
   400                 commas (map (string_for_nut ctxt) us) ^ ".")
   401        | REP (loc, Rs) =>
   402          error ("Invalid representation" ^ plural_s_for_list Rs ^
   403                 " (" ^ quote loc ^ "): " ^ commas (map string_for_rep Rs) ^ ".")
   404        | TERM (loc, ts) =>
   405          error ("Invalid term" ^ plural_s_for_list ts ^
   406                 " (" ^ quote loc ^ "): " ^
   407                 commas (map (Syntax.string_of_term ctxt) ts) ^ ".")
   408        | TOO_LARGE (_, details) =>
   409          (warning ("Limit reached: " ^ details ^ "."); x)
   410        | TOO_SMALL (_, details) =>
   411          (warning ("Limit reached: " ^ details ^ "."); x)
   412        | TYPE (loc, Ts, ts) =>
   413          error ("Invalid type" ^ plural_s_for_list Ts ^
   414                 (if null ts then
   415                    ""
   416                  else
   417                    " for term" ^ plural_s_for_list ts ^ " " ^
   418                    commas (map (quote o Syntax.string_of_term ctxt) ts)) ^
   419                 " (" ^ quote loc ^ "): " ^
   420                 commas (map (Syntax.string_of_typ ctxt) Ts) ^ ".")
   421        | Kodkod.SYNTAX (_, details) =>
   422          (warning ("Ill-formed Kodkodi output: " ^ details ^ "."); x)
   423        | Refute.REFUTE (loc, details) =>
   424          error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
   425 
   426 
   427 (* raw_param list -> bool -> int -> int -> Proof.state -> bool * Proof.state *)
   428 fun pick_nits override_params auto i step state =
   429   let
   430     val thy = Proof.theory_of state
   431     val ctxt = Proof.context_of state
   432     val _ = List.app check_raw_param override_params
   433     val params as {blocking, debug, ...} =
   434       extract_params ctxt auto (default_raw_params thy) override_params
   435     (* unit -> bool * Proof.state *)
   436     fun go () =
   437       (false, state)
   438       |> (if auto then perhaps o try
   439           else if debug then fn f => fn x => f x
   440           else handle_exceptions ctxt)
   441          (fn (_, state) => pick_nits_in_subgoal state params auto i step
   442                            |>> curry (op =) "genuine")
   443   in
   444     if auto orelse blocking then go ()
   445     else (Toplevel.thread true (fn () => (go (); ())); (false, state))
   446   end
   447 
   448 (* raw_param list option * int option -> Toplevel.transition
   449    -> Toplevel.transition *)
   450 fun nitpick_trans (opt_params, opt_i) =
   451   Toplevel.keep (fn st =>
   452       (pick_nits (these opt_params) false (the_default 1 opt_i)
   453                  (Toplevel.proof_position_of st) (Toplevel.proof_of st); ()))
   454 
   455 (* raw_param -> string *)
   456 fun string_for_raw_param (name, value) =
   457   name ^ " = " ^ stringify_raw_param_value value
   458 
   459 (* raw_param list option -> Toplevel.transition -> Toplevel.transition *)
   460 fun nitpick_params_trans opt_params =
   461   Toplevel.theory
   462       (fold set_default_raw_param (these opt_params)
   463        #> tap (fn thy => 
   464                   writeln ("Default parameters for Nitpick:\n" ^
   465                            (case rev (default_raw_params thy) of
   466                               [] => "none"
   467                             | params =>
   468                               (map check_raw_param params;
   469                                params |> map string_for_raw_param
   470                                       |> sort_strings |> cat_lines)))))
   471 
   472 (* OuterParse.token list
   473    -> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
   474 val scan_nitpick_command =
   475   (scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans
   476 val scan_nitpick_params_command = scan_params #>> nitpick_params_trans
   477 
   478 val _ = OuterSyntax.improper_command "nitpick"
   479             "try to find a counterexample for a given subgoal using Kodkod"
   480             OuterKeyword.diag scan_nitpick_command
   481 val _ = OuterSyntax.command "nitpick_params"
   482             "set and display the default parameters for Nitpick"
   483             OuterKeyword.thy_decl scan_nitpick_params_command
   484 
   485 (* Proof.state -> bool * Proof.state *)
   486 fun auto_nitpick state =
   487   if not (!auto) then (false, state) else pick_nits [] true 1 0 state
   488 
   489 val setup = Auto_Counterexample.register_tool ("nitpick", auto_nitpick)
   490 
   491 end;