src/Pure/Tools/quickcheck.ML
author haftmann
Mon Sep 22 08:00:26 2008 +0200 (2008-09-22)
changeset 28309 c24bc53c815c
parent 28256 4e7f7d52f855
child 28315 d3cf88fe77bc
permissions -rw-r--r--
some steps towards generic quickcheck framework
haftmann@28256
     1
(*  Title:      Pure/Tools/quickcheck.ML
haftmann@28256
     2
    ID:         $Id$
haftmann@28256
     3
    Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
haftmann@28256
     4
haftmann@28256
     5
Generic counterexample search engine.
haftmann@28256
     6
*)
haftmann@28256
     7
haftmann@28256
     8
signature QUICKCHECK =
haftmann@28256
     9
sig
haftmann@28309
    10
  val test_term: string option -> Proof.context -> bool -> int -> int -> term -> (string * term) list option;
haftmann@28256
    11
  val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
haftmann@28256
    12
end;
haftmann@28256
    13
haftmann@28256
    14
structure Quickcheck : QUICKCHECK =
haftmann@28256
    15
struct
haftmann@28256
    16
haftmann@28309
    17
datatype test_params = Test_Params of
haftmann@28309
    18
  { size: int, iterations: int, default_type: typ option };
haftmann@28309
    19
haftmann@28309
    20
fun mk_test_params ((size, iterations), default_type) =
haftmann@28309
    21
  Test_Params { size = size, iterations = iterations, default_type = default_type };
haftmann@28309
    22
fun map_test_params f (Test_Params { size, iterations, default_type}) =
haftmann@28309
    23
  mk_test_params (f ((size, iterations), default_type));
haftmann@28309
    24
fun merge_test_params (Test_Params {size = size1, iterations = iterations1, default_type = default_type1},
haftmann@28309
    25
  Test_Params {size = size2, iterations = iterations2, default_type = default_type2}) =
haftmann@28309
    26
  mk_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
haftmann@28309
    27
    case default_type1 of NONE => default_type2 | _ => default_type1);
haftmann@28309
    28
haftmann@28309
    29
structure Data = TheoryDataFun(
haftmann@28309
    30
  type T = (string * (Proof.context -> term -> int -> term list option)) list
haftmann@28309
    31
    * test_params;
haftmann@28309
    32
  val empty = ([], Test_Params { size = 10, iterations = 100, default_type = NONE });
haftmann@28256
    33
  val copy = I;
haftmann@28256
    34
  val extend = I;
haftmann@28309
    35
  fun merge pp ((generators1, params1), (generators2, params2)) =
haftmann@28309
    36
    (AList.merge (op = : string * string -> bool) (K true) (generators1, generators2),
haftmann@28309
    37
      merge_test_params (params1, params2));
haftmann@28256
    38
)
haftmann@28256
    39
haftmann@28309
    40
val add_generator = Data.map o apfst o AList.update (op =);
haftmann@28309
    41
haftmann@28309
    42
fun mk_tester_select name ctxt =
haftmann@28309
    43
  case AList.lookup (op =) ((fst o Data.get o ProofContext.theory_of) ctxt) name
haftmann@28309
    44
   of NONE => error ("No such quickcheck generator: " ^ name)
haftmann@28309
    45
    | SOME generator => generator ctxt;
haftmann@28309
    46
haftmann@28309
    47
fun mk_testers ctxt t =
haftmann@28309
    48
  (map snd o fst o Data.get o ProofContext.theory_of) ctxt
haftmann@28309
    49
  |> map_filter (fn generator => try (generator ctxt) t);
haftmann@28309
    50
haftmann@28309
    51
fun mk_testers_strict ctxt t =
haftmann@28309
    52
  let
haftmann@28309
    53
    val generators = ((map snd o fst o Data.get o ProofContext.theory_of) ctxt)
haftmann@28309
    54
    val testers = map (fn generator => Exn.capture (generator ctxt) t) generators;
haftmann@28309
    55
  in if forall (is_none o Exn.get_result) testers
haftmann@28309
    56
    then [(Exn.release o snd o split_last) testers]
haftmann@28309
    57
    else map_filter Exn.get_result testers
haftmann@28309
    58
  end;
haftmann@28309
    59
haftmann@28309
    60
fun prep_test_term t =
haftmann@28309
    61
  let
haftmann@28309
    62
    val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
haftmann@28309
    63
      error "Term to be tested contains type variables";
haftmann@28309
    64
    val _ = null (term_vars t) orelse
haftmann@28309
    65
      error "Term to be tested contains schematic variables";
haftmann@28309
    66
    val frees = map dest_Free (term_frees t);
haftmann@28309
    67
  in (map fst frees, list_abs_free (frees, t)) end
haftmann@28256
    68
haftmann@28309
    69
fun test_term generator_name ctxt quiet size i t =
haftmann@28309
    70
  let
haftmann@28309
    71
    val (names, t') = prep_test_term t;
haftmann@28309
    72
    val testers = case generator_name
haftmann@28309
    73
     of NONE => if quiet then mk_testers ctxt t' else mk_testers_strict ctxt t'
haftmann@28309
    74
      | SOME name => [mk_tester_select name ctxt t'];
haftmann@28309
    75
    fun iterate f 0 = NONE
haftmann@28309
    76
      | iterate f k = case f () handle Match => (if quiet then ()
haftmann@28309
    77
             else warning "Exception Match raised during quickcheck"; NONE)
haftmann@28309
    78
          of NONE => iterate f (k - 1) | SOME q => SOME q;
haftmann@28309
    79
    fun with_testers k [] = NONE
haftmann@28309
    80
      | with_testers k (tester :: testers) =
haftmann@28309
    81
          case iterate (fn () => tester k) i
haftmann@28309
    82
           of NONE => with_testers k testers
haftmann@28309
    83
            | SOME q => SOME q;
haftmann@28309
    84
    fun with_size k = if k > size then NONE
haftmann@28309
    85
      else (if quiet then () else priority ("Test data size: " ^ string_of_int k);
haftmann@28309
    86
        case with_testers k testers
haftmann@28309
    87
         of NONE => with_size (k + 1) | SOME q => SOME q);
haftmann@28309
    88
  in case with_size 1
haftmann@28309
    89
   of NONE => NONE
haftmann@28309
    90
    | SOME ts => SOME (names ~~ ts)
haftmann@28309
    91
  end;
haftmann@28309
    92
haftmann@28309
    93
fun monomorphic_term thy insts default_T = 
haftmann@28309
    94
  let
haftmann@28309
    95
    fun subst (T as TFree (v, S)) =
haftmann@28309
    96
          let
haftmann@28309
    97
            val T' = AList.lookup (op =) insts v
haftmann@28309
    98
              |> the_default (the_default T default_T)
haftmann@28309
    99
          in if Sign.of_sort thy (T, S) then T
haftmann@28309
   100
            else error ("Type " ^ Syntax.string_of_typ_global thy T ^
haftmann@28309
   101
              " to be substituted for variable " ^
haftmann@28309
   102
              Syntax.string_of_typ_global thy T ^ "\ndoes not have sort " ^
haftmann@28309
   103
              Syntax.string_of_sort_global thy S)
haftmann@28309
   104
          end
haftmann@28309
   105
      | subst T = T;
haftmann@28309
   106
  in (map_types o map_atyps) subst end;
haftmann@28309
   107
haftmann@28309
   108
fun pretty_counterex ctxt NONE = Pretty.str "No counterexamples found."
haftmann@28309
   109
  | pretty_counterex ctxt (SOME cex) =
haftmann@28309
   110
      Pretty.chunks (Pretty.str "Counterexample found:\n" ::
haftmann@28309
   111
        map (fn (s, t) =>
haftmann@28309
   112
          Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
haftmann@28309
   113
haftmann@28309
   114
fun test_goal generator_name quiet size iterations default_T insts i assms state =
haftmann@28309
   115
  let
haftmann@28309
   116
    val ctxt = Proof.context_of state;
haftmann@28309
   117
    val thy = Proof.theory_of state;
haftmann@28309
   118
    fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
haftmann@28309
   119
      | strip t = t;
haftmann@28309
   120
    val (_, (_, st)) = Proof.get_goal state;
haftmann@28309
   121
    val (gi, frees) = Logic.goal_params (prop_of st) i;
haftmann@28309
   122
    val gi' = Logic.list_implies (assms, subst_bounds (frees, strip gi))
haftmann@28309
   123
      |> monomorphic_term thy insts default_T
haftmann@28309
   124
      |> ObjectLogic.atomize_term thy;
haftmann@28309
   125
  in test_term generator_name ctxt quiet size iterations gi' end;
haftmann@28309
   126
haftmann@28309
   127
val auto = ref false;
haftmann@28309
   128
val auto_time_limit = ref 5000;
haftmann@28256
   129
haftmann@28309
   130
fun test_goal_auto int state =
haftmann@28309
   131
  let
haftmann@28309
   132
    val ctxt = Proof.context_of state;
haftmann@28309
   133
    val assms = map term_of (Assumption.assms_of ctxt);
haftmann@28309
   134
    val Test_Params { size, iterations, default_type } =
haftmann@28309
   135
      (snd o Data.get o Proof.theory_of) state;
haftmann@28309
   136
    fun test () =
haftmann@28309
   137
      let
haftmann@28309
   138
        val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_time_limit))
haftmann@28309
   139
          (try (test_goal NONE true size iterations default_type [] 1 assms)) state;
haftmann@28309
   140
      in
haftmann@28309
   141
        case res of
haftmann@28309
   142
          NONE => state
haftmann@28309
   143
        | SOME NONE => state
haftmann@28309
   144
        | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
haftmann@28309
   145
            Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state
haftmann@28309
   146
      end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
haftmann@28309
   147
  in
haftmann@28309
   148
    if int andalso !auto andalso not (!Toplevel.quiet)
haftmann@28309
   149
    then test ()
haftmann@28309
   150
    else state
haftmann@28309
   151
  end;
haftmann@28309
   152
haftmann@28309
   153
(*val _ = Context.>> (Specification.add_theorem_hook test_goal_auto);*)
haftmann@28309
   154
haftmann@28309
   155
fun test_goal_cmd generator_name i state =
haftmann@28309
   156
  test_goal generator_name false 10 100 NONE [] i [] (Toplevel.proof_of state)
haftmann@28309
   157
  |> pretty_counterex (Toplevel.context_of state)
haftmann@28309
   158
  |> Pretty.writeln;
haftmann@28309
   159
haftmann@28309
   160
local structure P = OuterParse and K = OuterKeyword in
haftmann@28309
   161
haftmann@28309
   162
fun read_nothing x thy = x;
haftmann@28309
   163
fun read_typ raw_ty thy = Syntax.read_typ_global thy raw_ty;
haftmann@28309
   164
haftmann@28309
   165
val parse_test_param = (P.short_ident --| P.$$$ "=" #->
haftmann@28309
   166
  (fn "size" => P.nat >> (apfst o apfst o K)
haftmann@28309
   167
    | "iterations" => P.nat >> (apfst o apsnd o K)
haftmann@28309
   168
    | "default_type" => P.typ >> (apsnd o K)));
haftmann@28309
   169
haftmann@28309
   170
val parse_test_param_inst =
haftmann@28309
   171
  P.type_ident --| P.$$$ "=" -- P.typ >> (apsnd o AList.update (op =))
haftmann@28309
   172
  || parse_test_param >> apfst;
haftmann@28309
   173
haftmann@28309
   174
(*fun quickcheck_test_params_cmd fs thy =
haftmann@28309
   175
  (Data.map o apsnd o map_test_params) (Library.apply fs);*)
haftmann@28309
   176
haftmann@28309
   177
(*val _ =
haftmann@28309
   178
  OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
haftmann@28309
   179
    (P.$$$ "[" |-- P.list1 parse_test_param --| P.$$$ "]" >>
haftmann@28309
   180
      (Toplevel.theory o quickcheck_test_params_cmd));*)
haftmann@28309
   181
haftmann@28309
   182
(*
haftmann@28309
   183
val params =
haftmann@28309
   184
  [("size", P.nat >> (K o set_size)),
haftmann@28309
   185
   ("iterations", P.nat >> (K o set_iterations)),
haftmann@28309
   186
   ("default_type", P.typ >> set_default_type)];
haftmann@28309
   187
haftmann@28309
   188
val parse_test_params = P.short_ident :|-- (fn s =>
haftmann@28309
   189
  P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail));
haftmann@28256
   190
haftmann@28309
   191
fun parse_tyinst xs =
haftmann@28309
   192
  (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
haftmann@28309
   193
    fn (x, ys) => (x, (v, Syntax.read_typ_global thy s) :: ys))) xs;
haftmann@28309
   194
haftmann@28309
   195
haftmann@28309
   196
*)
haftmann@28309
   197
haftmann@28309
   198
val _ = OuterSyntax.improper_command "test_goal" "try to find counterexample for subgoal" K.diag
haftmann@28309
   199
  (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- Scan.optional P.nat 1
haftmann@28309
   200
    >> (fn (some_name, i) => Toplevel.no_timing o Toplevel.keep (test_goal_cmd some_name i)));
haftmann@28309
   201
haftmann@28309
   202
end; (*local*)
haftmann@28309
   203
haftmann@28309
   204
haftmann@28309
   205
haftmann@28309
   206
(*
haftmann@28309
   207
val _ =
haftmann@28309
   208
  OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
haftmann@28309
   209
    (P.$$$ "[" |-- P.list1 parse_test_params --| P.$$$ "]" >>
haftmann@28309
   210
      (fn fs => Toplevel.theory (fn thy =>
haftmann@28309
   211
         map_test_params (Library.apply (map (fn f => f thy) fs)) thy)));
haftmann@28309
   212
haftmann@28309
   213
val _ =
haftmann@28309
   214
  OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
haftmann@28309
   215
  (Scan.option (P.$$$ "[" |-- P.list1
haftmann@28309
   216
    (   parse_test_params >> (fn f => fn thy => apfst (f thy))
haftmann@28309
   217
     || parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >>
haftmann@28309
   218
    (fn (ps, g) => Toplevel.keep (fn st => Toplevel.proof_of st |>
haftmann@28309
   219
      test_goal false (Library.apply (the_default []
haftmann@28309
   220
          (Option.map (map (fn f => f (Toplevel.theory_of st))) ps))
haftmann@28309
   221
        (get_test_params (Toplevel.theory_of st), [])) g [] |>
haftmann@28309
   222
      pretty_counterex (Toplevel.context_of st) |> Pretty.writeln)));
haftmann@28309
   223
haftmann@28309
   224
val auto_quickcheck = ref false;
haftmann@28309
   225
val auto_quickcheck_time_limit = ref 5000;
haftmann@28309
   226
haftmann@28309
   227
fun test_goal' int state =
haftmann@28309
   228
  let
haftmann@28309
   229
    val ctxt = Proof.context_of state;
haftmann@28309
   230
    val assms = map term_of (Assumption.assms_of ctxt);
haftmann@28309
   231
    val params = get_test_params (Proof.theory_of state);
haftmann@28309
   232
    fun test () =
haftmann@28309
   233
      let
haftmann@28309
   234
        val res = TimeLimit.timeLimit (Time.fromMilliseconds (!auto_quickcheck_time_limit))
haftmann@28309
   235
          (try (test_goal true (params, []) 1 assms)) state;
haftmann@28309
   236
      in
haftmann@28309
   237
        case res of
haftmann@28309
   238
          NONE => state
haftmann@28309
   239
        | SOME NONE => state
haftmann@28309
   240
        | SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
haftmann@28309
   241
            Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state
haftmann@28309
   242
      end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
haftmann@28309
   243
  in
haftmann@28309
   244
    if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
haftmann@28309
   245
    then test ()
haftmann@28309
   246
    else state
haftmann@28309
   247
  end;
haftmann@28309
   248
*)
haftmann@28309
   249
haftmann@28309
   250
(*
haftmann@28256
   251
fun value_cmd some_name modes raw_t state =
haftmann@28256
   252
  let
haftmann@28256
   253
    val ctxt = Toplevel.context_of state;
haftmann@28256
   254
    val t = Syntax.read_term ctxt raw_t;
haftmann@28256
   255
    val t' = case some_name
haftmann@28256
   256
     of NONE => value ctxt t
haftmann@28256
   257
      | SOME name => value_select name ctxt t;
haftmann@28256
   258
    val ty' = Term.type_of t';
haftmann@28256
   259
    val ctxt' = Variable.auto_fixes t ctxt;
haftmann@28256
   260
    val p = PrintMode.with_modes modes (fn () =>
haftmann@28256
   261
      Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
haftmann@28256
   262
        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
haftmann@28256
   263
  in Pretty.writeln p end;*)
haftmann@28256
   264
haftmann@28309
   265
end;
haftmann@28256
   266
haftmann@28309
   267
(*val auto_quickcheck = Quickcheck.auto;
haftmann@28309
   268
val auto_quickcheck_time_limit = Quickcheck.auto_time_limit;*)