adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
authorbulwahn
Sun Dec 04 20:05:08 2011 +0100 (2011-12-04)
changeset 4575017100f4ce0b5
parent 45749 92c6ddca552e
child 45752 b5db02fa9536
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
adjusting smart quickcheck compilation to new signature of exhaustive generators (cf. 1f5fc44254d7);
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Tools/Predicate_Compile/code_prolog.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Sun Dec 04 18:30:57 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Sun Dec 04 20:05:08 2011 +0100
     1.3 @@ -466,7 +466,7 @@
     1.4  where
     1.5    "cps_not n = (%c. case n (%u. Some []) of None => c () | Some _ => None)"
     1.6  
     1.7 -type_synonym 'a pos_bound_cps = "('a => term list option) => code_numeral => term list option"
     1.8 +type_synonym 'a pos_bound_cps = "('a => (bool * term list) option) => code_numeral => (bool * term list) option"
     1.9  
    1.10  definition pos_bound_cps_empty :: "'a pos_bound_cps"
    1.11  where
    1.12 @@ -515,7 +515,7 @@
    1.13  
    1.14  definition neg_bound_cps_not :: "unit pos_bound_cps => unit neg_bound_cps"
    1.15  where
    1.16 -  "neg_bound_cps_not n = (%c i. case n (%u. Some []) i of None => c (Known ()) | Some _ => No_value)"
    1.17 +  "neg_bound_cps_not n = (%c i. case n (%u. Some (True, [])) i of None => c (Known ()) | Some _ => No_value)"
    1.18  
    1.19  definition pos_bound_cps_not :: "unit neg_bound_cps => unit pos_bound_cps"
    1.20  where
     2.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Dec 04 18:30:57 2011 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sun Dec 04 20:05:08 2011 +0100
     2.3 @@ -1039,7 +1039,7 @@
     2.4        | _ => NONE
     2.5    in
     2.6      Quickcheck.Result
     2.7 -      {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) counterexample,
     2.8 +      {counterexample = Option.map (pair true o curry (op ~~) (Term.add_free_names t [])) counterexample,
     2.9         evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []}
    2.10    end;
    2.11  
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Sun Dec 04 18:30:57 2011 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Sun Dec 04 20:05:08 2011 +0100
     3.3 @@ -114,9 +114,11 @@
     3.4  structure Pos_Bounded_CPS_Comp_Funs =
     3.5  struct
     3.6  
     3.7 -fun mk_monadT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "code_numeral => Code_Evaluation.term list option"}
     3.8 +val resultT = @{typ "(bool * Code_Evaluation.term list) option"}
     3.9 +fun mk_monadT T = (T --> resultT) --> @{typ "code_numeral"} --> resultT
    3.10  
    3.11 -fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "code_numeral => term list option"}])) = T
    3.12 +fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "(bool * term list) option"}]),
    3.13 +  @{typ "code_numeral => (bool * term list) option"}])) = T
    3.14    | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
    3.15  
    3.16  fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_monadT T);
    3.17 @@ -196,7 +198,8 @@
    3.18  fun mk_not t =
    3.19    let
    3.20      val T = mk_monadT HOLogic.unitT
    3.21 -    val pT = @{typ "(unit => Code_Evaluation.term list option) => code_numeral => Code_Evaluation.term list option"}
    3.22 +    val pT = @{typ "(unit => (bool * Code_Evaluation.term list) option)"}
    3.23 +      --> @{typ "code_numeral => (bool * Code_Evaluation.term list) option"}
    3.24    in Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_not}, pT --> T) $ t end
    3.25  
    3.26  fun mk_Enum f = error "not implemented"
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Dec 04 18:30:57 2011 +0100
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Dec 04 20:05:08 2011 +0100
     4.3 @@ -550,7 +550,8 @@
     4.4    mk_random =
     4.5      (fn T => fn additional_arguments =>
     4.6         Const (@{const_name "Quickcheck_Exhaustive.exhaustive"},
     4.7 -       (T --> @{typ "term list option"}) --> @{typ "code_numeral => term list option"})),
     4.8 +       (T --> @{typ "(bool * term list) option"}) -->
     4.9 +         @{typ "code_numeral => (bool * term list) option"})),
    4.10    modify_funT = I,
    4.11    additional_arguments = K [],
    4.12    wrap_compilation = K (K (K (K (K I))))
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sun Dec 04 18:30:57 2011 +0100
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sun Dec 04 20:05:08 2011 +0100
     5.3 @@ -18,7 +18,7 @@
     5.4        Proof.context -> Proof.context;
     5.5    val put_new_dseq_result : (unit -> int -> term list Lazy_Sequence.lazy_sequence) ->
     5.6      Proof.context -> Proof.context
     5.7 -  val put_cps_result : (unit -> int -> term list option) ->
     5.8 +  val put_cps_result : (unit -> int -> (bool * term list) option) ->
     5.9      Proof.context -> Proof.context
    5.10    val test_goals : (Predicate_Compile_Aux.compilation * bool) ->
    5.11      Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list
    5.12 @@ -70,7 +70,7 @@
    5.13  
    5.14  structure CPS_Result = Proof_Data
    5.15  (
    5.16 -  type T = unit -> int -> term list option
    5.17 +  type T = unit -> int -> (bool * term list) option
    5.18    (* FIXME avoid user error with non-user text *)
    5.19    fun init _ () = error "CPS_Result"
    5.20  );
    5.21 @@ -278,8 +278,9 @@
    5.22              mk_split_lambda (map Free vs') (mk_gen_return (HOLogic.mk_list @{typ term}
    5.23              (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))
    5.24          | Pos_Generator_CPS => prog $
    5.25 -            mk_split_lambda (map Free vs') (mk_Some @{typ "term list"} $ (HOLogic.mk_list @{typ term}
    5.26 -            (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))     
    5.27 +            mk_split_lambda (map Free vs') (mk_Some @{typ "bool * term list"} $
    5.28 +            HOLogic.mk_prod (@{term "True"}, HOLogic.mk_list @{typ term}
    5.29 +                (map2 HOLogic.mk_term_of (map snd vs') (map Free vs'))))     
    5.30          | Depth_Limited_Random => fold_rev absdummy
    5.31              [@{typ code_numeral}, @{typ code_numeral}, @{typ code_numeral},
    5.32               @{typ "code_numeral * code_numeral"}]
    5.33 @@ -333,10 +334,10 @@
    5.34                Code_Runtime.dynamic_value_strict
    5.35                  (CPS_Result.get, put_cps_result, "Predicate_Compile_Quickcheck.put_cps_result")
    5.36                  thy4 (SOME target)
    5.37 -                (fn proc => fn g => fn depth => g depth |> Option.map (map proc))
    5.38 +                (fn proc => fn g => fn depth => g depth |> Option.map (apsnd (map proc)))
    5.39                  qc_term []
    5.40            in
    5.41 -            fn size => fn nrandom => compiled_term
    5.42 +            fn size => fn nrandom => Option.map snd o compiled_term
    5.43            end
    5.44         | Depth_Limited_Random =>
    5.45            let
    5.46 @@ -385,7 +386,7 @@
    5.47      val counterexample = try_upto_depth ctxt (c size (!nrandom))
    5.48    in
    5.49      Quickcheck.Result
    5.50 -      {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) counterexample,
    5.51 +      {counterexample = Option.map (pair true o (curry (op ~~)) (Term.add_free_names t [])) counterexample,
    5.52         evaluation_terms = Option.map (K []) counterexample, timings = [], reports = []}
    5.53    end
    5.54