adding postprocessing for maps in term construction of quickcheck; fixed check_all_option definition
authorbulwahn
Wed Dec 15 17:46:46 2010 +0100 (2010-12-15)
changeset 41178f4d3acf0c4cc
parent 41177 810a885decee
child 41179 5391d34b0f4c
adding postprocessing for maps in term construction of quickcheck; fixed check_all_option definition
src/HOL/Smallcheck.thy
src/HOL/Tools/smallvalue_generators.ML
     1.1 --- a/src/HOL/Smallcheck.thy	Wed Dec 15 17:46:46 2010 +0100
     1.2 +++ b/src/HOL/Smallcheck.thy	Wed Dec 15 17:46:46 2010 +0100
     1.3 @@ -281,7 +281,9 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App (Code_Evaluation.term_of (Some :: 'a => 'a option)) (t ())))"
     1.8 +  "check_all f = f (Code_Evaluation.valtermify (None :: 'a option)) orelse check_all (%(x, t). f (Some x, %_. Code_Evaluation.App
     1.9 +    (Code_Evaluation.Const (STR ''Option.option.Some'')
    1.10 +      (Typerep.Typerep (STR ''fun'') [Typerep.typerep TYPE('a),  Typerep.Typerep (STR ''Option.option'') [Typerep.typerep TYPE('a)]])) (t ())))"
    1.11  
    1.12  definition enum_term_of_option :: "'a option itself => unit => term list"
    1.13  where
     2.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 15 17:46:46 2010 +0100
     2.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Wed Dec 15 17:46:46 2010 +0100
     2.3 @@ -280,12 +280,7 @@
     2.4          $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i
     2.5    in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end
     2.6  
     2.7 -fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
     2.8 -  | make_set T1 ((t1, @{const False}) :: tps) = make_set T1 tps
     2.9 -  | make_set T1 ((t1, @{const True}) :: tps) =
    2.10 -    Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
    2.11 -      $ t1 $ (make_set T1 tps)
    2.12 -  | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t])
    2.13 +(** post-processing of function terms **)
    2.14  
    2.15  fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2))
    2.16    | dest_fun_upd t = raise TERM ("dest_fun_upd", [t])
    2.17 @@ -303,14 +298,34 @@
    2.18  
    2.19  fun make_plain_fun T1 T2 tps =
    2.20    fold_rev (mk_fun_upd T1 T2) tps (absdummy (T1, Const ("_", T2)))
    2.21 +
    2.22 +fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool})
    2.23 +  | make_set T1 ((_, @{const False}) :: tps) = make_set T1 tps
    2.24 +  | make_set T1 ((t1, @{const True}) :: tps) =
    2.25 +    Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool})
    2.26 +      $ t1 $ (make_set T1 tps)
    2.27 +  | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t])
    2.28 +
    2.29 +fun make_map T1 T2 [] = Const (@{const_abbrev Map.empty}, T1 --> T2)
    2.30 +  | make_map T1 T2 ((_, Const (@{const_name None}, _)) :: tps) = make_map T1 T2 tps
    2.31 +  | make_map T1 T2 ((t1, t2) :: tps) = mk_fun_upd T1 T2 (t1, t2) (make_map T1 T2 tps)
    2.32    
    2.33  fun post_process_term t =
    2.34    case fastype_of t of
    2.35      Type (@{type_name fun}, [T1, T2]) =>
    2.36 -      dest_plain_fun t |> map (pairself post_process_term) |>
    2.37 -        (if T2 = @{typ bool} then rev #> make_set T1 else make_plain_fun T1 T2)
    2.38 +      (case try dest_plain_fun t of
    2.39 +        SOME tps =>
    2.40 +          tps
    2.41 +          |> map (pairself post_process_term)
    2.42 +          |> (case T2 of
    2.43 +            @{typ bool} => rev #> make_set T1
    2.44 +          | Type (@{type_name option}, _) => make_map T1 T2
    2.45 +          | _ => make_plain_fun T1 T2)
    2.46 +      | NONE => t)
    2.47    | _ => t
    2.48  
    2.49 +(** generator compiliation **)
    2.50 +
    2.51  fun compile_generator_expr ctxt t =
    2.52    let
    2.53      val thy = ProofContext.theory_of ctxt