1.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Mon Jul 18 10:34:21 2011 +0200
     1.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Mon Jul 18 10:34:21 2011 +0200
     1.3 @@ -6,58 +6,55 @@
     1.4  
     1.5  signature MUTABELLE =
     1.6  sig
     1.7 - val testgen_name : string Unsynchronized.ref
     1.8 - exception WrongPath of string;
     1.9 - exception WrongArg of string;
    1.10 - val freeze : term -> term
    1.11 - val mutate_exc : term -> string list -> int -> term list 
    1.12 - val mutate_sign : term -> theory -> (string * string) list -> int -> term list 
    1.13 - val mutate_mix : term -> theory -> string list -> 
    1.14 +  exception WrongPath of string;
    1.15 +  exception WrongArg of string;
    1.16 +  val freeze : term -> term
    1.17 +  val mutate_exc : term -> string list -> int -> term list 
    1.18 +  val mutate_sign : term -> theory -> (string * string) list -> int -> term list 
    1.19 +  val mutate_mix : term -> theory -> string list -> 
    1.20     (string * string) list -> int -> term list
    1.21 - val qc_test : term list -> (typ * typ) list -> theory ->
    1.22 +(*  val qc_test : term list -> (typ * typ) list -> theory ->
    1.23    int -> int -> int * Thm.cterm list * int * (Thm.cterm * (string * Thm.cterm) list) list
    1.24 - val qc_test_file : bool -> term list -> (typ * typ) list 
    1.25 +  val qc_test_file : bool -> term list -> (typ * typ) list 
    1.26     -> theory -> int -> int -> string -> unit
    1.27 - val mutqc_file_exc : theory -> string list ->
    1.28 +  val mutqc_file_exc : theory -> string list ->
    1.29    int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit
    1.30 - val mutqc_file_sign : theory -> (string * string) list ->
    1.31 +  val mutqc_file_sign : theory -> (string * string) list ->
    1.32    int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit
    1.33 - val mutqc_file_mix : theory -> string list -> (string * string) list ->
    1.34 +  val mutqc_file_mix : theory -> string list -> (string * string) list ->
    1.35    int -> Thm.thm -> (typ * typ) list -> int -> int -> string -> unit
    1.36 - val mutqc_file_rec_exc : theory -> string list -> int ->
    1.37 +  val mutqc_file_rec_exc : theory -> string list -> int ->
    1.38    Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit
    1.39 - val mutqc_file_rec_sign : theory -> (string * string) list -> int ->
    1.40 +  val mutqc_file_rec_sign : theory -> (string * string) list -> int ->
    1.41    Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit
    1.42 - val mutqc_file_rec_mix : theory -> string list -> (string * string) list ->
    1.43 +  val mutqc_file_rec_mix : theory -> string list -> (string * string) list ->
    1.44    int -> Thm.thm list -> (typ * typ) list -> int -> int -> string list -> unit
    1.45 - val mutqc_thy_exc : theory -> theory ->
    1.46 +  val mutqc_thy_exc : theory -> theory ->
    1.47    string list -> int -> (typ * typ) list -> int -> int -> string -> unit
    1.48 - val mutqc_thy_sign : theory -> theory -> (string * string) list ->
    1.49 +  val mutqc_thy_sign : theory -> theory -> (string * string) list ->
    1.50    int -> (typ * typ) list -> int -> int -> string -> unit
    1.51 - val mutqc_thy_mix : theory -> theory -> string list -> (string * string) list ->
    1.52 +  val mutqc_thy_mix : theory -> theory -> string list -> (string * string) list ->
    1.53    int -> (typ * typ) list -> int -> int -> string -> unit
    1.54 - val mutqc_file_stat_sign : theory -> (string * string) list ->
    1.55 +  val mutqc_file_stat_sign : theory -> (string * string) list ->
    1.56    int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit
    1.57 - val mutqc_file_stat_exc : theory -> string list ->
    1.58 +  val mutqc_file_stat_exc : theory -> string list ->
    1.59    int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit
    1.60 - val mutqc_file_stat_mix : theory -> string list -> (string * string) list ->
    1.61 +  val mutqc_file_stat_mix : theory -> string list -> (string * string) list ->
    1.62    int -> Thm.thm list -> (typ * typ) list -> int -> int -> string -> unit
    1.63 - val mutqc_thystat_exc : (string -> thm -> bool) -> theory -> theory ->
    1.64 +  val mutqc_thystat_exc : (string -> thm -> bool) -> theory -> theory ->
    1.65    string list -> int -> (typ * typ) list -> int -> int -> string -> unit
    1.66 - val mutqc_thystat_sign : (string -> thm -> bool) -> theory -> theory -> (string * string) list ->
    1.67 +  val mutqc_thystat_sign : (string -> thm -> bool) -> theory -> theory -> (string * string) list ->
    1.68    int -> (typ * typ) list -> int -> int -> string -> unit
    1.69 - val mutqc_thystat_mix : (string -> thm -> bool) -> theory -> theory -> string list -> 
    1.70 +  val mutqc_thystat_mix : (string -> thm -> bool) -> theory -> theory -> string list -> 
    1.71    (string * string) list -> int -> (typ * typ) list -> int -> int -> string -> unit
    1.72 - val canonize_term: term -> string list -> term
    1.73 - 
    1.74 - val all_unconcealed_thms_of : theory -> (string * thm) list
    1.75 +  val canonize_term: term -> string list -> term
    1.76 +*)  
    1.77 +  val all_unconcealed_thms_of : theory -> (string * thm) list
    1.78  end;
    1.79  
    1.80  structure Mutabelle : MUTABELLE = 
    1.81  struct
    1.82  
    1.83 -val testgen_name = Unsynchronized.ref "random";
    1.84 -
    1.85  fun all_unconcealed_thms_of thy =
    1.86    let
    1.87      val facts = Global_Theory.facts_of thy
    1.88 @@ -495,44 +492,17 @@
    1.89   (map_types (inst_type insts) (freeze t));
    1.90  
    1.91  fun is_executable thy insts th =
    1.92 -  ((Quickcheck.test_term 
    1.93 -      (Proof_Context.init_global thy
    1.94 +  let
    1.95 +    val ctxt' = Proof_Context.init_global thy
    1.96        |> Config.put Quickcheck.size 1
    1.97        |> Config.put Quickcheck.iterations 1
    1.98 -      |> Config.put Quickcheck.tester (!testgen_name))
    1.99 -      (true, false) (preprocess thy insts (prop_of th), []);
   1.100 -    Output.urgent_message "executable"; true) handle ERROR s =>
   1.101 -    (Output.urgent_message ("not executable: " ^ s); false));
   1.102 -
   1.103 -fun qc_recursive usedthy [] insts sz qciter acc = rev acc
   1.104 - | qc_recursive usedthy (x::xs) insts sz qciter acc = qc_recursive usedthy xs insts sz qciter 
   1.105 -     (Output.urgent_message ("qc_recursive: " ^ string_of_int (length xs));
   1.106 -     ((x, pretty (the_default [] (Quickcheck.counterexample_of (Quickcheck.test_term
   1.107 -       ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter
   1.108 -        #> Config.put Quickcheck.tester (!testgen_name))
   1.109 -         (Proof_Context.init_global usedthy))
   1.110 -       (true, false) (preprocess usedthy insts x, []))))) :: acc))
   1.111 -          handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);
   1.112 -
   1.113 -
   1.114 -(*quickcheck-test the mutants created by function mutate with type-instantiation insts, 
   1.115 -quickcheck-theory usedthy and qciter quickcheck-iterations *)
   1.116 -
   1.117 -fun qc_test mutated insts usedthy sz qciter = 
   1.118 - let 
   1.119 -   val checked = map (apsnd (map (apsnd (cterm_of usedthy))))
   1.120 -     (qc_recursive usedthy mutated insts sz qciter []);
   1.121 -   fun combine (passednum,passed) (cenum,ces) [] = (passednum,passed,cenum,ces)
   1.122 -     | combine (passednum,passed) (cenum,ces) ((t, []) :: xs) =
   1.123 -       combine (passednum+1,(cterm_of usedthy t)::passed) (cenum,ces) xs
   1.124 -     | combine (passednum,passed) (cenum,ces) ((t, x) :: xs) =
   1.125 -       combine (passednum,passed) 
   1.126 -         (cenum+1,(cterm_of usedthy t, x) :: ces) xs
   1.127 - in
   1.128 -   combine (0,[]) (0,[]) checked
   1.129 - end;
   1.130 -
   1.131 -
   1.132 +    val test = Quickcheck.test_term Exhaustive_Generators.compile_generator_expr ctxt' (true, false)
   1.133 +  in  
   1.134 +    case try test (preprocess thy insts (prop_of th), []) of
   1.135 +      SOME _ => (Output.urgent_message "executable"; true)
   1.136 +    | NONE => (Output.urgent_message ("not executable"); false)
   1.137 +  end;
   1.138 +(*
   1.139  (*create a string of a list of terms*)
   1.140  
   1.141  fun string_of_ctermlist thy [] acc = acc
   1.142 @@ -767,5 +737,6 @@
   1.143  
   1.144  fun mutqc_thystat_mix p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename =
   1.145   mutqc_thystat 2 p mutthy usedthy commutatives forbidden_funs iter insts sz qciter filename;
   1.146 +*)
   1.147  
   1.148  end

     2.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Jul 18 10:34:21 2011 +0200
     2.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Jul 18 10:34:21 2011 +0200
     2.3 @@ -122,7 +122,7 @@
     2.4    TimeLimit.timeLimit (seconds (!Try.auto_time_limit))
     2.5        (fn _ =>
     2.6            let
     2.7 -            val [result] = Quickcheck.test_goal_terms (change_options (Proof_Context.init_global thy))
     2.8 +            val SOME [result] = Quickcheck.test_goal_terms (change_options (Proof_Context.init_global thy))
     2.9                (false, false) [] [(t, [])]
    2.10            in
    2.11              case Quickcheck.counterexample_of result of 

     3.1 --- a/src/Tools/quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
     3.2 +++ b/src/Tools/quickcheck.ML	Mon Jul 18 10:34:21 2011 +0200
     3.3 @@ -63,7 +63,8 @@
     3.4      Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list
     3.5    (* testing terms and proof states *)
     3.6    val test_term: compile_generator -> Proof.context -> bool * bool -> term * term list -> result
     3.7 -  (*val test_goal_terms : tester*)
     3.8 +  val test_goal_terms :
     3.9 +    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list option
    3.10    val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
    3.11    (* testing a batch of terms *)
    3.12    val test_terms: