Quickcheck callable from ML
authorboehmes
Fri Jul 31 23:30:21 2009 +0200 (2009-07-31)
changeset 322973a4081abb3f7
parent 32294 d00238af17b6
child 32298 8ffc607c345d
Quickcheck callable from ML
src/Tools/quickcheck.ML
     1.1 --- a/src/Tools/quickcheck.ML	Thu Jul 30 23:50:11 2009 +0200
     1.2 +++ b/src/Tools/quickcheck.ML	Fri Jul 31 23:30:21 2009 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4    val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
     1.5      (string * term) list option
     1.6    val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
     1.7 +  val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
     1.8  end;
     1.9  
    1.10  structure Quickcheck : QUICKCHECK =
    1.11 @@ -215,18 +216,21 @@
    1.12      |> (Data.map o apsnd o map_test_params) f
    1.13    end;
    1.14  
    1.15 -fun quickcheck_cmd args i state =
    1.16 +fun quickcheck args i state =
    1.17    let
    1.18 -    val prf = Toplevel.proof_of state;
    1.19 -    val thy = Toplevel.theory_of state;
    1.20 -    val ctxt = Toplevel.context_of state;
    1.21 +    val thy = Proof.theory_of state;
    1.22 +    val ctxt = Proof.context_of state;
    1.23      val default_params = (dest_test_params o snd o Data.get) thy;
    1.24      val f = fold (parse_test_param_inst ctxt) args;
    1.25      val (((size, iterations), default_type), (generator_name, insts)) =
    1.26        f (default_params, (NONE, []));
    1.27 -    val counterex = test_goal false generator_name size iterations
    1.28 -      default_type insts i [] prf;
    1.29 -  in (Pretty.writeln o pretty_counterex ctxt) counterex end;
    1.30 +  in
    1.31 +    test_goal false generator_name size iterations default_type insts i [] state
    1.32 +  end;
    1.33 +
    1.34 +fun quickcheck_cmd args i state =
    1.35 +  quickcheck args i (Toplevel.proof_of state)
    1.36 +  |> Pretty.writeln o pretty_counterex (Toplevel.context_of state);
    1.37  
    1.38  local structure P = OuterParse and K = OuterKeyword in
    1.39