improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
authorbulwahn
Fri Dec 03 08:40:46 2010 +0100 (2010-12-03)
changeset 40899ef6fde932f4c
parent 40898 882e860a1e83
child 40900 1d5f76d79856
improving readability of Smallcheck theory; adding constant orelse to improve performance of the function package
src/HOL/Smallcheck.thy
src/HOL/Tools/smallvalue_generators.ML
     1.1 --- a/src/HOL/Smallcheck.thy	Fri Dec 03 08:40:46 2010 +0100
     1.2 +++ b/src/HOL/Smallcheck.thy	Fri Dec 03 08:40:46 2010 +0100
     1.3 @@ -48,7 +48,7 @@
     1.4  
     1.5  end
     1.6  
     1.7 -section {* full small value generator type classes *}
     1.8 +subsection {* full small value generator type classes *}
     1.9  
    1.10  class full_small = term_of +
    1.11  fixes full_small :: "('a * (unit => term) \<Rightarrow> term list option) \<Rightarrow> code_numeral \<Rightarrow> term list option"
    1.12 @@ -80,7 +80,7 @@
    1.13  
    1.14  instantiation prod :: (full_small, full_small) full_small
    1.15  begin
    1.16 -ML {* @{const_name "Pair"} *}
    1.17 +
    1.18  definition
    1.19    "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y),
    1.20      %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d"
    1.21 @@ -97,14 +97,16 @@
    1.22    "full_small_fun' f i d = (if i > 1 then
    1.23      full_small (%(a, at). full_small (%(b, bt).
    1.24        full_small_fun' (%(g, gt). f (g(a := b),
    1.25 -        (%_. let T1 = (Typerep.typerep (TYPE('a))); T2 = (Typerep.typerep (TYPE('b))) in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
    1.26 -         
    1.27 -(Code_Evaluation.Const (STR ''Fun.fun_upd'')
    1.28 -
    1.29 -(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
    1.30 -
    1.31 - (gt ())) (at ())) (bt ())))) (i - 1) d) d) d else (if i > 0 then
    1.32 -  full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
    1.33 +        (%_. let T1 = (Typerep.typerep (TYPE('a)));
    1.34 +                 T2 = (Typerep.typerep (TYPE('b)))
    1.35 +             in
    1.36 +               Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App
    1.37 +                 (Code_Evaluation.Const (STR ''Fun.fun_upd'')
    1.38 +                    (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2],
    1.39 +                       Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]]))
    1.40 +               (gt ())) (at ())) (bt ())))) (i - 1) d) d) d
    1.41 +  else (if i > 0 then
    1.42 +    full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))"
    1.43  
    1.44  definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option"
    1.45  where
    1.46 @@ -117,6 +119,11 @@
    1.47  
    1.48  subsection {* Defining combinators for any first-order data type *}
    1.49  
    1.50 +definition orelse :: "'a option => 'a option => 'a option"
    1.51 +where
    1.52 +  [code_unfold]: "orelse x y = (case x of Some x' => Some x' | None => y)"
    1.53 +
    1.54 +
    1.55  definition catch_match :: "term list option => term list option => term list option"
    1.56  where
    1.57    [code del]: "catch_match t1 t2 = (SOME t. t = t1 \<or> t = t2)"
    1.58 @@ -130,7 +137,7 @@
    1.59  setup {* Smallvalue_Generators.setup *}
    1.60  *)
    1.61  
    1.62 -hide_fact catch_match_def
    1.63 -hide_const (open) catch_match
    1.64 +hide_fact orelse_def catch_match_def
    1.65 +hide_const (open) orelse catch_match
    1.66  
    1.67  end
    1.68 \ No newline at end of file
     2.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:46 2010 +0100
     2.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:46 2010 +0100
     2.3 @@ -50,8 +50,8 @@
     2.4    let
     2.5      val (T as Type(@{type_name "option"}, [T'])) = fastype_of x
     2.6    in
     2.7 -    Const (@{const_name Option.option_case}, T --> (T' --> T) --> T --> T)
     2.8 -      $ y $ Const (@{const_name Some}, T' --> T) $ x
     2.9 +    Const (@{const_name "Smallcheck.orelse"}, T --> T --> T)
    2.10 +      $ x $ y
    2.11    end
    2.12  
    2.13  (** datatypes **)