--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/quickcheck.ML Wed Sep 17 07:32:04 2008 +0200
@@ -0,0 +1,67 @@
+(* Title: Pure/Tools/quickcheck.ML
+ ID: $Id$
+ Author: Stefan Berghofer, Florian Haftmann, TU Muenchen
+
+Generic counterexample search engine.
+*)
+
+signature QUICKCHECK =
+sig
+ (*val test: Proof.context -> int -> int -> term -> (string * term) list option
+ val test_select: string -> Proof.context -> int -> int -> term -> (string * term) list option
+ val test_cmd: string option -> string list -> string -> Toplevel.state -> unit*)
+ val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
+end;
+
+structure Quickcheck : QUICKCHECK =
+struct
+
+structure Generator = TheoryDataFun(
+ type T = (string * (Proof.context -> term -> int -> term list option)) list;
+ val empty = [];
+ val copy = I;
+ val extend = I;
+ fun merge pp = AList.merge (op =) (K true);
+)
+
+val add_generator = Generator.map o AList.update (op =);
+
+(*fun value_select name ctxt =
+ case AList.lookup (op =) (Evaluator.get (ProofContext.theory_of ctxt)) name
+ of NONE => error ("No such evaluator: " ^ name)
+ | SOME f => f ctxt;
+
+fun value ctxt t = let val evaluators = Evaluator.get (ProofContext.theory_of ctxt)
+ in if null evaluators then error "No evaluators"
+ else let val (evaluators, (_, evaluator)) = split_last evaluators
+ in case get_first (fn (_, f) => try (f ctxt) t) evaluators
+ of SOME t' => t'
+ | NONE => evaluator ctxt t
+ end end;
+
+fun value_cmd some_name modes raw_t state =
+ let
+ val ctxt = Toplevel.context_of state;
+ val t = Syntax.read_term ctxt raw_t;
+ val t' = case some_name
+ of NONE => value ctxt t
+ | SOME name => value_select name ctxt t;
+ val ty' = Term.type_of t';
+ val ctxt' = Variable.auto_fixes t ctxt;
+ val p = PrintMode.with_modes modes (fn () =>
+ Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
+ Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
+ in Pretty.writeln p end;*)
+
+(*local structure P = OuterParse and K = OuterKeyword in
+
+val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
+
+val _ = OuterSyntax.improper_command "value" "evaluate and print term" K.diag
+ (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- opt_modes -- P.term
+ >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
+ (value_cmd some_name modes t)));
+
+end; (*local*)*)
+
+end;