# HG changeset patch # User bulwahn # Date 1300468782 -3600 # Node ID 2de57cda5b24187b10aaa0aa8eada96358940e4c # Parent 96327c90938912927e1aa24f7aae34a3f2324f19 adapting predicate_compile_quickcheck; tuned diff -r 96327c909389 -r 2de57cda5b24 src/HOL/Predicate_Compile_Examples/IMP_1.thy --- a/src/HOL/Predicate_Compile_Examples/IMP_1.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy Fri Mar 18 18:19:42 2011 +0100 @@ -8,9 +8,8 @@ In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, and IF. *} -types - var = unit - state = bool +type_synonym var = unit +type_synonym state = bool datatype com = Skip | diff -r 96327c909389 -r 2de57cda5b24 src/HOL/Predicate_Compile_Examples/IMP_2.thy --- a/src/HOL/Predicate_Compile_Examples/IMP_2.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy Fri Mar 18 18:19:42 2011 +0100 @@ -8,9 +8,8 @@ In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, IF and While. *} -types - var = unit - state = bool +type_synonym var = unit +type_synonym state = bool datatype com = Skip | diff -r 96327c909389 -r 2de57cda5b24 src/HOL/Predicate_Compile_Examples/IMP_3.thy --- a/src/HOL/Predicate_Compile_Examples/IMP_3.thy Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy Fri Mar 18 18:19:42 2011 +0100 @@ -8,9 +8,8 @@ In this example, the state is one integer variable and the commands are Skip, Ass, Seq, IF, and While. *} -types - var = unit - state = int +type_synonym var = unit +type_synonym state = int datatype com = Skip | diff -r 96327c909389 -r 2de57cda5b24 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Mar 18 18:19:42 2011 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Fri Mar 18 18:19:42 2011 +0100 @@ -22,7 +22,7 @@ val tracing : bool Unsynchronized.ref; val quiet : bool Unsynchronized.ref; val quickcheck_compile_term : Predicate_Compile_Aux.compilation -> bool -> bool -> int -> - Proof.context -> term -> int -> term list option * Quickcheck.report option; + Proof.context -> term * term list -> int -> term list option * Quickcheck.report option; (* val test_term : Proof.context -> bool -> int -> int -> int -> int -> term -> *) val nrandom : int Unsynchronized.ref; val debug : bool Unsynchronized.ref; @@ -218,11 +218,12 @@ val time = Time.toMilliseconds (#cpu (end_timing start)) in (Exn.release result, (description, time)) end -fun compile_term compilation options ctxt t = +fun compile_term compilation options ctxt (t, eval_terms) = let + val t' = list_abs_free (Term.add_frees t [], t) val thy = Theory.copy (ProofContext.theory_of ctxt) val ((((full_constname, constT), vs'), intro), thy1) = - Predicate_Compile_Aux.define_quickcheck_predicate t thy + Predicate_Compile_Aux.define_quickcheck_predicate t' thy val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1 val (thy3, preproc_time) = cpu_time "predicate preprocessing" (fn () => Predicate_Compile.preprocess options (Const (full_constname, constT)) thy2)