# HG changeset patch # User haftmann # Date 1221629524 -7200 # Node ID 4e7f7d52f855112b7e3fb4863357f3cfb355d541 # Parent 6faea8ad855999d64f11a7ecb1c0d5722649cc3d added quickcheck.ML diff -r 6faea8ad8559 -r 4e7f7d52f855 src/Pure/Tools/quickcheck.ML --- /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;