src/HOL/Tools/smallvalue_generators.ML
changeset 40639 f1f0e6adca0a
parent 40420 552563ea3304
child 40640 3fa1c2472568
     1.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:41:57 2010 +0100
     1.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Mon Nov 22 10:41:58 2010 +0100
     1.3 @@ -6,7 +6,6 @@
     1.4  
     1.5  signature SMALLVALUE_GENERATORS =
     1.6  sig
     1.7 -  val ensure_smallvalue_datatype: Datatype.config -> string list -> theory -> theory
     1.8    val compile_generator_expr:
     1.9      Proof.context -> term -> int -> term list option * (bool list * bool)
    1.10    val put_counterexample: (unit -> int -> term list option)
    1.11 @@ -51,10 +50,12 @@
    1.12  
    1.13  (** abstract syntax **)
    1.14  
    1.15 +fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"});
    1.16 +
    1.17  val size = @{term "i :: code_numeral"}
    1.18  val size_pred = @{term "(i :: code_numeral) - 1"}
    1.19  val size_ge_zero = @{term "(i :: code_numeral) > 0"}
    1.20 -fun test_function T = Free ("f", T --> @{typ "term list option"})
    1.21 +fun test_function T = Free ("f", termifyT T --> @{typ "term list option"})
    1.22  
    1.23  fun mk_none_continuation (x, y) =
    1.24    let
    1.25 @@ -75,16 +76,23 @@
    1.26  fun smallT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ code_numeral}
    1.27    --> @{typ "Code_Evaluation.term list option"}
    1.28  
    1.29 +val full_smallN = "full_small";
    1.30 +
    1.31 +fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"})
    1.32 +  --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"}
    1.33 + 
    1.34  fun mk_equations thy descr vs tycos (names, auxnames) (Ts, Us) =
    1.35    let
    1.36 -    val smallsN = map (prefix (smallN ^ "_")) (names @ auxnames);
    1.37 -    val smalls = map2 (fn name => fn T => Free (name, smallT T))
    1.38 +    val smallsN = map (prefix (full_smallN ^ "_")) (names @ auxnames);
    1.39 +    val smalls = map2 (fn name => fn T => Free (name, full_smallT T))
    1.40        smallsN (Ts @ Us)
    1.41      fun mk_small_call T =
    1.42        let
    1.43 -        val small = Const (@{const_name "Smallcheck.small_class.small"}, smallT T)        
    1.44 +        val small = Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)        
    1.45        in
    1.46 -        (T, (fn t => small $ absdummy (T, t) $ size_pred))
    1.47 +        (T, (fn t => small $
    1.48 +          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
    1.49 +          $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))
    1.50        end
    1.51      fun mk_small_aux_call fTs (k, _) (tyco, Ts) =
    1.52        let
    1.53 @@ -92,14 +100,23 @@
    1.54          val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
    1.55          val small = nth smalls k
    1.56        in
    1.57 -        (T, (fn t => small $ absdummy (T, t) $ size_pred))
    1.58 +       (T, (fn t => small $
    1.59 +          (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"})
    1.60 +            $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred))  
    1.61        end
    1.62      fun mk_consexpr simpleT (c, xs) =
    1.63        let
    1.64          val (Ts, fns) = split_list xs
    1.65          val constr = Const (c, Ts ---> simpleT)
    1.66 -        val bounds = map Bound (((length xs) - 1) downto 0)
    1.67 -        val start_term = test_function simpleT $ (list_comb (constr, bounds))
    1.68 +        val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0)
    1.69 +        val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0)
    1.70 +        val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT)
    1.71 +        val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT)
    1.72 +        val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"}))
    1.73 +          bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT))
    1.74 +        val start_term = test_function simpleT $ 
    1.75 +        (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"}
    1.76 +          $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term))
    1.77        in fold_rev (fn f => fn t => f t) fns start_term end
    1.78      fun mk_rhs exprs =
    1.79          @{term "If :: bool => term list option => term list option => term list option"}
    1.80 @@ -129,7 +146,7 @@
    1.81          PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st'
    1.82        end
    1.83    | _ => Seq.empty;
    1.84 -
    1.85 +  
    1.86  fun instantiate_smallvalue_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    1.87    let
    1.88      val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
    1.89 @@ -155,45 +172,22 @@
    1.90        Pat_Completeness.pat_completeness_tac ctxt 1
    1.91        THEN auto_tac (clasimpset_of ctxt)
    1.92    in
    1.93 -    thy
    1.94 -    |> Class.instantiation (tycos, vs, @{sort small})
    1.95 +    (thy
    1.96 +    |> Class.instantiation (tycos, vs, @{sort full_small})
    1.97      |> Function.add_function
    1.98        (map (fn (T, (name, _)) =>
    1.99 -          Syntax.no_syn (Binding.conceal (Binding.name name), SOME (smallT T))) eqs)
   1.100 +          Syntax.no_syn (Binding.conceal (Binding.name name), SOME (full_smallT T))) eqs)
   1.101          (map (pair (apfst Binding.conceal Attrib.empty_binding) o snd o snd) eqs)
   1.102          Function_Common.default_config pat_completeness_auto
   1.103      |> snd
   1.104      |> Local_Theory.restore
   1.105      |> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy)
   1.106      |> snd
   1.107 -    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
   1.108 -  end;
   1.109 -
   1.110 -fun ensure_smallvalue_datatype config raw_tycos thy =
   1.111 -  let
   1.112 -    val algebra = Sign.classes_of thy;
   1.113 -    val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
   1.114 -      Datatype.the_descr thy raw_tycos;
   1.115 -    val typerep_vs = (map o apsnd)
   1.116 -      (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
   1.117 -    val smallvalue_insts = (map (rpair @{sort small}) o flat o maps snd o maps snd)
   1.118 -      (Datatype_Aux.interpret_construction descr typerep_vs
   1.119 -        { atyp = single, dtyp = (K o K o K) [] });
   1.120 -    (*val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
   1.121 -      (Datatype_Aux.interpret_construction descr typerep_vs
   1.122 -        { atyp = K [], dtyp = K o K });*)
   1.123 -    val has_inst = exists (fn tyco =>
   1.124 -      can (Sorts.mg_domain algebra tyco) @{sort small}) tycos;
   1.125 -  in if has_inst then thy
   1.126 -    else case Quickcheck_Generators.perhaps_constrain thy smallvalue_insts typerep_vs
   1.127 -     of SOME constrain => (instantiate_smallvalue_datatype config descr
   1.128 -          (map constrain typerep_vs) tycos prfx (names, auxnames)
   1.129 -            ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
   1.130 -            handle FUNCTION_TYPE =>
   1.131 -              (Datatype_Aux.message config
   1.132 -                "Creation of smallvalue generators failed because the datatype contains a function type";
   1.133 -              thy))
   1.134 -      | NONE => thy
   1.135 +    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])))
   1.136 +    handle FUNCTION_TYPE =>
   1.137 +    (Datatype_Aux.message config
   1.138 +      "Creation of smallvalue generators failed because the datatype contains a function type";
   1.139 +    thy)
   1.140    end;
   1.141  
   1.142  (** building and compiling generator expressions **)
   1.143 @@ -209,19 +203,20 @@
   1.144  fun mk_generator_expr thy prop Ts =
   1.145    let
   1.146      val bound_max = length Ts - 1;
   1.147 -    val bounds = map Bound (bound_max downto 0)
   1.148 -    val result = list_comb (prop, bounds);
   1.149 -    val terms = HOLogic.mk_list @{typ term} (map2 HOLogic.mk_term_of Ts bounds);
   1.150 +    val bounds = map_index (fn (i, ty) =>
   1.151 +      (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts;
   1.152 +    val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds);
   1.153 +    val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds);
   1.154      val check =
   1.155        @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $
   1.156          (@{term "If :: bool => term list option => term list option => term list option"}
   1.157 -        $ result $ @{term "None :: term list option"}
   1.158 -        $ (@{term "Some :: term list => term list option"} $ terms))
   1.159 +        $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms))
   1.160        $ @{term "None :: term list option"};
   1.161 -    fun mk_small_closure (depth, T) t =
   1.162 -      Const (@{const_name "Smallcheck.small_class.small"}, smallT T)
   1.163 -        $ absdummy (T, t) $ depth
   1.164 -  in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure (rev bounds ~~ Ts) check) end
   1.165 +    fun mk_small_closure (_, _, i, T) t =
   1.166 +      Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T)
   1.167 +        $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) 
   1.168 +        $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i
   1.169 +  in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end
   1.170  
   1.171  fun compile_generator_expr ctxt t =
   1.172    let
   1.173 @@ -242,7 +237,8 @@
   1.174  (** setup **)
   1.175  
   1.176  val setup =
   1.177 -  Datatype.interpretation ensure_smallvalue_datatype
   1.178 +  Datatype.interpretation
   1.179 +    (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype))
   1.180    #> Context.theory_map
   1.181      (Quickcheck.add_generator ("small", compile_generator_expr));
   1.182