src/Pure/Tools/quickcheck.ML
changeset 28256 4e7f7d52f855
child 28309 c24bc53c815c
equal deleted inserted replaced
28255:6faea8ad8559 28256:4e7f7d52f855
       
     1 (*  Title:      Pure/Tools/quickcheck.ML
       
     2     ID:         $Id$
       
     3     Author:     Stefan Berghofer, Florian Haftmann, TU Muenchen
       
     4 
       
     5 Generic counterexample search engine.
       
     6 *)
       
     7 
       
     8 signature QUICKCHECK =
       
     9 sig
       
    10   (*val test: Proof.context -> int -> int -> term -> (string * term) list option
       
    11   val test_select: string -> Proof.context -> int -> int -> term -> (string * term) list option
       
    12   val test_cmd: string option -> string list -> string -> Toplevel.state -> unit*)
       
    13   val add_generator: string * (Proof.context -> term -> int -> term list option) -> theory -> theory
       
    14 end;
       
    15 
       
    16 structure Quickcheck : QUICKCHECK =
       
    17 struct
       
    18 
       
    19 structure Generator = TheoryDataFun(
       
    20   type T = (string * (Proof.context -> term -> int -> term list option)) list;
       
    21   val empty = [];
       
    22   val copy = I;
       
    23   val extend = I;
       
    24   fun merge pp = AList.merge (op =) (K true);
       
    25 )
       
    26 
       
    27 val add_generator = Generator.map o AList.update (op =);
       
    28 
       
    29 (*fun value_select name ctxt =
       
    30   case AList.lookup (op =) (Evaluator.get (ProofContext.theory_of ctxt)) name
       
    31    of NONE => error ("No such evaluator: " ^ name)
       
    32     | SOME f => f ctxt;
       
    33 
       
    34 fun value ctxt t = let val evaluators = Evaluator.get (ProofContext.theory_of ctxt)
       
    35   in if null evaluators then error "No evaluators"
       
    36   else let val (evaluators, (_, evaluator)) = split_last evaluators
       
    37     in case get_first (fn (_, f) => try (f ctxt) t) evaluators
       
    38      of SOME t' => t'
       
    39       | NONE => evaluator ctxt t
       
    40   end end;
       
    41 
       
    42 fun value_cmd some_name modes raw_t state =
       
    43   let
       
    44     val ctxt = Toplevel.context_of state;
       
    45     val t = Syntax.read_term ctxt raw_t;
       
    46     val t' = case some_name
       
    47      of NONE => value ctxt t
       
    48       | SOME name => value_select name ctxt t;
       
    49     val ty' = Term.type_of t';
       
    50     val ctxt' = Variable.auto_fixes t ctxt;
       
    51     val p = PrintMode.with_modes modes (fn () =>
       
    52       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
       
    53         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
       
    54   in Pretty.writeln p end;*)
       
    55 
       
    56 (*local structure P = OuterParse and K = OuterKeyword in
       
    57 
       
    58 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
       
    59 
       
    60 val _ = OuterSyntax.improper_command "value" "evaluate and print term" K.diag
       
    61   (Scan.option (P.$$$ "[" |-- P.xname --| P.$$$ "]") -- opt_modes -- P.term
       
    62     >> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
       
    63         (value_cmd some_name modes t)));
       
    64 
       
    65 end; (*local*)*)
       
    66 
       
    67 end;