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