adapting predicate_compile_quickcheck; tuned
authorbulwahn
Fri Mar 18 18:19:42 2011 +0100 (2011-03-18)
changeset 420312de57cda5b24
parent 42030 96327c909389
child 42032 143f37194911
adapting predicate_compile_quickcheck; tuned
src/HOL/Predicate_Compile_Examples/IMP_1.thy
src/HOL/Predicate_Compile_Examples/IMP_2.thy
src/HOL/Predicate_Compile_Examples/IMP_3.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
     1.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Fri Mar 18 18:19:42 2011 +0100
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy	Fri Mar 18 18:19:42 2011 +0100
     1.3 @@ -8,9 +8,8 @@
     1.4    In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, and IF.
     1.5  *}
     1.6  
     1.7 -types
     1.8 -  var = unit
     1.9 -  state = bool
    1.10 +type_synonym var = unit
    1.11 +type_synonym state = bool
    1.12  
    1.13  datatype com =
    1.14    Skip |
     2.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Mar 18 18:19:42 2011 +0100
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy	Fri Mar 18 18:19:42 2011 +0100
     2.3 @@ -8,9 +8,8 @@
     2.4    In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, IF and While.
     2.5  *}
     2.6  
     2.7 -types
     2.8 -  var = unit
     2.9 -  state = bool
    2.10 +type_synonym var = unit
    2.11 +type_synonym state = bool
    2.12  
    2.13  datatype com =
    2.14    Skip |
     3.1 --- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Mar 18 18:19:42 2011 +0100
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy	Fri Mar 18 18:19:42 2011 +0100
     3.3 @@ -8,9 +8,8 @@
     3.4    In this example, the state is one integer variable and the commands are Skip, Ass, Seq, IF, and While.
     3.5  *}
     3.6  
     3.7 -types
     3.8 -  var = unit
     3.9 -  state = int
    3.10 +type_synonym var = unit
    3.11 +type_synonym state = int
    3.12  
    3.13  datatype com =
    3.14    Skip |
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Mar 18 18:19:42 2011 +0100
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Mar 18 18:19:42 2011 +0100
     4.3 @@ -22,7 +22,7 @@
     4.4    val tracing : bool Unsynchronized.ref;
     4.5    val quiet : bool Unsynchronized.ref;
     4.6    val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int ->
     4.7 -    Proof.context -> term -> int -> term list option * Quickcheck.report option;
     4.8 +    Proof.context -> term * term list -> int -> term list option * Quickcheck.report option;
     4.9  (*  val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *)
    4.10    val nrandom : int Unsynchronized.ref;
    4.11    val debug : bool Unsynchronized.ref;
    4.12 @@ -218,11 +218,12 @@
    4.13      val time = Time.toMilliseconds (#cpu (end_timing start))
    4.14    in (Exn.release result, (description, time)) end
    4.15  
    4.16 -fun compile_term compilation options ctxt t =
    4.17 +fun compile_term compilation options ctxt (t, eval_terms) =
    4.18    let
    4.19 +    val t' = list_abs_free (Term.add_frees t [], t)
    4.20      val thy = Theory.copy (ProofContext.theory_of ctxt)
    4.21      val ((((full_constname, constT), vs'), intro), thy1) =
    4.22 -      Predicate_Compile_Aux.define_quickcheck_predicate t thy
    4.23 +      Predicate_Compile_Aux.define_quickcheck_predicate t' thy
    4.24      val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
    4.25      val (thy3, preproc_time) = cpu_time "predicate preprocessing"
    4.26          (fn () => Predicate_Compile.preprocess options (Const (full_constname, constT)) thy2)