splitting exhaustive and full_exhaustive into separate type classes
authorbulwahn
Fri Apr 08 16:31:14 2011 +0200 (2011-04-08)
changeset 42310c664cc5cc5e9
parent 42309 74ea14d13247
child 42311 eb32a8474a57
splitting exhaustive and full_exhaustive into separate type classes
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Tools/Quickcheck/exhaustive_generators.ML
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 08 16:31:14 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Fri Apr 08 16:31:14 2011 +0200
     1.3 @@ -17,9 +17,11 @@
     1.4  
     1.5  class exhaustive = term_of +
     1.6    fixes exhaustive :: "('a \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
     1.7 +  
     1.8 +class full_exhaustive = term_of +
     1.9    fixes full_exhaustive :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    1.10  
    1.11 -instantiation code_numeral :: exhaustive
    1.12 +instantiation code_numeral :: full_exhaustive
    1.13  begin
    1.14  
    1.15  function full_exhaustive_code_numeral' :: "(code_numeral * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.16 @@ -33,6 +35,13 @@
    1.17  
    1.18  definition "full_exhaustive f d = full_exhaustive_code_numeral' f d 0"
    1.19  
    1.20 +instance ..
    1.21 +
    1.22 +end
    1.23 +
    1.24 +instantiation code_numeral :: exhaustive
    1.25 +begin
    1.26 +
    1.27  function exhaustive_code_numeral' :: "(code_numeral => term list option) => code_numeral => code_numeral => term list option"
    1.28    where "exhaustive_code_numeral' f d i =
    1.29      (if d < i then None
    1.30 @@ -44,7 +53,6 @@
    1.31  
    1.32  definition "exhaustive f d = exhaustive_code_numeral' f d 0"
    1.33  
    1.34 -
    1.35  instance ..
    1.36  
    1.37  end
    1.38 @@ -54,6 +62,13 @@
    1.39  
    1.40  definition "exhaustive f d = exhaustive (%x. f (Code_Numeral.nat_of x)) d"
    1.41  
    1.42 +instance ..
    1.43 +
    1.44 +end
    1.45 +
    1.46 +instantiation nat :: full_exhaustive
    1.47 +begin
    1.48 +
    1.49  definition "full_exhaustive f d = full_exhaustive (%(x, xt). f (Code_Numeral.nat_of x, %_. Code_Evaluation.term_of (Code_Numeral.nat_of x))) d"
    1.50  
    1.51  instance ..
    1.52 @@ -72,6 +87,13 @@
    1.53  
    1.54  definition "exhaustive f d = exhaustive' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))"
    1.55  
    1.56 +instance ..
    1.57 +
    1.58 +end
    1.59 +
    1.60 +instantiation int :: full_exhaustive
    1.61 +begin
    1.62 +
    1.63  function full_exhaustive' :: "(int * (unit => term) => term list option) => int => int => term list option"
    1.64    where "full_exhaustive' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_exhaustive' f d (i + 1)))"
    1.65  by pat_completeness auto
    1.66 @@ -91,6 +113,13 @@
    1.67  definition
    1.68    "exhaustive f d = exhaustive (%x. exhaustive (%y. f ((x, y))) d) d"
    1.69  
    1.70 +instance ..
    1.71 +
    1.72 +end
    1.73 +
    1.74 +instantiation prod :: (full_exhaustive, full_exhaustive) full_exhaustive
    1.75 +begin
    1.76 +
    1.77  definition
    1.78    "full_exhaustive f d = full_exhaustive (%(x, t1). full_exhaustive (%(y, t2). f ((x, y),
    1.79      %u. let T1 = (Typerep.typerep (TYPE('a)));
    1.80 @@ -118,6 +147,12 @@
    1.81  where
    1.82    "exhaustive_fun f d = exhaustive_fun' f d d" 
    1.83  
    1.84 +instance ..
    1.85 +
    1.86 +end
    1.87 +
    1.88 +instantiation "fun" :: ("{equal, full_exhaustive}", full_exhaustive) full_exhaustive
    1.89 +begin
    1.90  
    1.91  fun full_exhaustive_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option"
    1.92  where
     2.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
     2.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Fri Apr 08 16:31:14 2011 +0200
     2.3 @@ -187,7 +187,7 @@
     2.4      fun mk_call T =
     2.5        let
     2.6          val full_exhaustive =
     2.7 -          Const (@{const_name "Quickcheck_Exhaustive.exhaustive_class.full_exhaustive"},
     2.8 +          Const (@{const_name "Quickcheck_Exhaustive.full_exhaustive_class.full_exhaustive"},
     2.9              full_exhaustiveT T)
    2.10        in
    2.11          (T, (fn t => full_exhaustive $
    2.12 @@ -251,13 +251,26 @@
    2.13    let
    2.14      val _ = Datatype_Aux.message config "Creating exhaustive generators...";
    2.15      val exhaustivesN = map (prefix (exhaustiveN ^ "_")) (names @ auxnames)
    2.16 -    val full_exhaustivesN = map (prefix (full_exhaustiveN ^ "_")) (names @ auxnames)
    2.17    in
    2.18      thy
    2.19      |> Class.instantiation (tycos, vs, @{sort exhaustive})
    2.20      |> Quickcheck_Common.define_functions
    2.21          (fn functerms => mk_equations functerms (descr, vs, Ts @ Us), SOME termination_tac)
    2.22          prfx ["f", "i"] exhaustivesN (map exhaustiveT (Ts @ Us))
    2.23 +    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    2.24 +  end handle FUNCTION_TYPE =>
    2.25 +    (Datatype_Aux.message config
    2.26 +      "Creation of exhaustive generators failed because the datatype contains a function type";
    2.27 +    thy)
    2.28 +
    2.29 +
    2.30 +fun instantiate_full_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    2.31 +  let
    2.32 +    val _ = Datatype_Aux.message config "Creating exhaustive generators...";
    2.33 +    val full_exhaustivesN = map (prefix (full_exhaustiveN ^ "_")) (names @ auxnames)
    2.34 +  in
    2.35 +    thy
    2.36 +    |> Class.instantiation (tycos, vs, @{sort full_exhaustive})
    2.37      |> Quickcheck_Common.define_functions
    2.38          (fn functerms => mk_full_equations functerms (descr, vs, Ts @ Us), SOME termination_tac)
    2.39          prfx ["f", "i"] full_exhaustivesN (map full_exhaustiveT (Ts @ Us))
    2.40 @@ -266,7 +279,7 @@
    2.41      (Datatype_Aux.message config
    2.42        "Creation of exhaustive generators failed because the datatype contains a function type";
    2.43      thy)
    2.44 -
    2.45 +     
    2.46  fun instantiate_fast_exhaustive_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    2.47    let
    2.48      val _ = Datatype_Aux.message config "Creating fast exhaustive generators...";
    2.49 @@ -549,9 +562,11 @@
    2.50    Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    2.51        (((@{sort typerep}, @{sort term_of}), @{sort exhaustive}), instantiate_exhaustive_datatype))
    2.52    #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    2.53 -      (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))
    2.54 +      (((@{sort typerep}, @{sort term_of}), @{sort full_exhaustive}), instantiate_full_exhaustive_datatype))
    2.55    #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    2.56        (((@{sort typerep}, @{sort term_of}), @{sort fast_exhaustive}), instantiate_fast_exhaustive_datatype))
    2.57 +  #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
    2.58 +      (((@{sort type}, @{sort type}), @{sort bounded_forall}), instantiate_bounded_forall_datatype))
    2.59    #> setup_smart_quantifier
    2.60    #> setup_full_support
    2.61    #> setup_fast