putting compilation setup of predicate compiler in a separate file
authorbulwahn
Wed Mar 31 16:44:41 2010 +0200 (2010-03-31)
changeset 36046c3946372f556
parent 36045 b846881928ea
child 36047 f8297ebb21a7
putting compilation setup of predicate compiler in a separate file
src/HOL/IsaMakefile
src/HOL/Predicate_Compile.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.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/IsaMakefile	Tue Mar 30 15:46:50 2010 -0700
     1.2 +++ b/src/HOL/IsaMakefile	Wed Mar 31 16:44:41 2010 +0200
     1.3 @@ -297,6 +297,7 @@
     1.4    Tools/numeral_syntax.ML \
     1.5    Tools/polyhash.ML \
     1.6    Tools/Predicate_Compile/predicate_compile_aux.ML \
     1.7 +  Tools/Predicate_Compile/predicate_compile_compilations.ML \
     1.8    Tools/Predicate_Compile/predicate_compile_core.ML \
     1.9    Tools/Predicate_Compile/predicate_compile_data.ML \
    1.10    Tools/Predicate_Compile/predicate_compile_fun.ML \
     2.1 --- a/src/HOL/Predicate_Compile.thy	Tue Mar 30 15:46:50 2010 -0700
     2.2 +++ b/src/HOL/Predicate_Compile.thy	Wed Mar 31 16:44:41 2010 +0200
     2.3 @@ -8,6 +8,7 @@
     2.4  imports New_Random_Sequence
     2.5  uses
     2.6    "Tools/Predicate_Compile/predicate_compile_aux.ML"
     2.7 +  "Tools/Predicate_Compile/predicate_compile_compilations.ML"
     2.8    "Tools/Predicate_Compile/predicate_compile_core.ML"
     2.9    "Tools/Predicate_Compile/predicate_compile_data.ML"
    2.10    "Tools/Predicate_Compile/predicate_compile_fun.ML"
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Tue Mar 30 15:46:50 2010 -0700
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Mar 31 16:44:41 2010 +0200
     3.3 @@ -469,10 +469,41 @@
     3.4  val random_compilations = [Random, Depth_Limited_Random,
     3.5    Pos_Random_DSeq, Neg_Random_DSeq, New_Pos_Random_DSeq, New_Neg_Random_DSeq]
     3.6  
     3.7 -(* Different options for compiler *)
     3.8 +(* datastructures and setup for generic compilation *)
     3.9 +
    3.10 +datatype compilation_funs = CompilationFuns of {
    3.11 +  mk_predT : typ -> typ,
    3.12 +  dest_predT : typ -> typ,
    3.13 +  mk_bot : typ -> term,
    3.14 +  mk_single : term -> term,
    3.15 +  mk_bind : term * term -> term,
    3.16 +  mk_sup : term * term -> term,
    3.17 +  mk_if : term -> term,
    3.18 +  mk_not : term -> term,
    3.19 +  mk_map : typ -> typ -> term -> term -> term
    3.20 +};
    3.21  
    3.22 -(*datatype compilation_options =
    3.23 -  Pred | Random of int | Depth_Limited of int | DSeq of int | Annotated*)
    3.24 +fun mk_predT (CompilationFuns funs) = #mk_predT funs
    3.25 +fun dest_predT (CompilationFuns funs) = #dest_predT funs
    3.26 +fun mk_bot (CompilationFuns funs) = #mk_bot funs
    3.27 +fun mk_single (CompilationFuns funs) = #mk_single funs
    3.28 +fun mk_bind (CompilationFuns funs) = #mk_bind funs
    3.29 +fun mk_sup (CompilationFuns funs) = #mk_sup funs
    3.30 +fun mk_if (CompilationFuns funs) = #mk_if funs
    3.31 +fun mk_not (CompilationFuns funs) = #mk_not funs
    3.32 +fun mk_map (CompilationFuns funs) = #mk_map funs
    3.33 +
    3.34 +(** function types and names of different compilations **)
    3.35 +
    3.36 +fun funT_of compfuns mode T =
    3.37 +  let
    3.38 +    val Ts = binder_types T
    3.39 +    val (inTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts
    3.40 +  in
    3.41 +    inTs ---> (mk_predT compfuns (HOLogic.mk_tupleT outTs))
    3.42 +  end;
    3.43 +
    3.44 +(* Different options for compiler *)
    3.45  
    3.46  datatype options = Options of {  
    3.47    expected_modes : (string * mode list) option,
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Wed Mar 31 16:44:41 2010 +0200
     4.3 @@ -0,0 +1,293 @@
     4.4 +(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
     4.5 +    Author:     Lukas Bulwahn, TU Muenchen
     4.6 +
     4.7 +Structures for different compilations of the predicate compiler
     4.8 +*)
     4.9 +
    4.10 +structure PredicateCompFuns =
    4.11 +struct
    4.12 +
    4.13 +fun mk_predT T = Type (@{type_name Predicate.pred}, [T])
    4.14 +
    4.15 +fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T
    4.16 +  | dest_predT T = raise TYPE ("dest_predT", [T], []);
    4.17 +
    4.18 +fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
    4.19 +
    4.20 +fun mk_single t =
    4.21 +  let val T = fastype_of t
    4.22 +  in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end;
    4.23 +
    4.24 +fun mk_bind (x, f) =
    4.25 +  let val T as Type ("fun", [_, U]) = fastype_of f
    4.26 +  in
    4.27 +    Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
    4.28 +  end;
    4.29 +
    4.30 +val mk_sup = HOLogic.mk_binop @{const_name sup};
    4.31 +
    4.32 +fun mk_if cond = Const (@{const_name Predicate.if_pred},
    4.33 +  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
    4.34 +
    4.35 +fun mk_not t =
    4.36 +  let
    4.37 +    val T = mk_predT HOLogic.unitT
    4.38 +  in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
    4.39 +
    4.40 +fun mk_Enum f =
    4.41 +  let val T as Type ("fun", [T', _]) = fastype_of f
    4.42 +  in
    4.43 +    Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f    
    4.44 +  end;
    4.45 +
    4.46 +fun mk_Eval (f, x) =
    4.47 +  let
    4.48 +    val T = fastype_of x
    4.49 +  in
    4.50 +    Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
    4.51 +  end;
    4.52 +
    4.53 +fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x)
    4.54 +
    4.55 +fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
    4.56 +  (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
    4.57 +
    4.58 +val compfuns = Predicate_Compile_Aux.CompilationFuns
    4.59 +    {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
    4.60 +    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
    4.61 +    mk_map = mk_map};
    4.62 +
    4.63 +end;
    4.64 +
    4.65 +structure RandomPredCompFuns =
    4.66 +struct
    4.67 +
    4.68 +fun mk_randompredT T =
    4.69 +  @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed})
    4.70 +
    4.71 +fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"},
    4.72 +  [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
    4.73 +  | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
    4.74 +
    4.75 +fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
    4.76 +
    4.77 +fun mk_single t =
    4.78 +  let               
    4.79 +    val T = fastype_of t
    4.80 +  in
    4.81 +    Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t
    4.82 +  end;
    4.83 +
    4.84 +fun mk_bind (x, f) =
    4.85 +  let
    4.86 +    val T as (Type ("fun", [_, U])) = fastype_of f
    4.87 +  in
    4.88 +    Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f
    4.89 +  end
    4.90 +
    4.91 +val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union}
    4.92 +
    4.93 +fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
    4.94 +  HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
    4.95 +
    4.96 +fun mk_not t =
    4.97 +  let
    4.98 +    val T = mk_randompredT HOLogic.unitT
    4.99 +  in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end
   4.100 +
   4.101 +fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
   4.102 +  (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
   4.103 +
   4.104 +val compfuns = Predicate_Compile_Aux.CompilationFuns
   4.105 +    {mk_predT = mk_randompredT, dest_predT = dest_randompredT,
   4.106 +    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   4.107 +    mk_not = mk_not, mk_map = mk_map};
   4.108 +
   4.109 +end;
   4.110 +
   4.111 +structure DSequence_CompFuns =
   4.112 +struct
   4.113 +
   4.114 +fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
   4.115 +  Type (@{type_name Option.option}, [Type  (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])
   4.116 +
   4.117 +fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
   4.118 +  Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
   4.119 +  | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
   4.120 +
   4.121 +fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T);
   4.122 +
   4.123 +fun mk_single t =
   4.124 +  let val T = fastype_of t
   4.125 +  in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end;
   4.126 +
   4.127 +fun mk_bind (x, f) =
   4.128 +  let val T as Type ("fun", [_, U]) = fastype_of f
   4.129 +  in
   4.130 +    Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
   4.131 +  end;
   4.132 +
   4.133 +val mk_sup = HOLogic.mk_binop @{const_name DSequence.union};
   4.134 +
   4.135 +fun mk_if cond = Const (@{const_name DSequence.if_seq},
   4.136 +  HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
   4.137 +
   4.138 +fun mk_not t = let val T = mk_dseqT HOLogic.unitT
   4.139 +  in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
   4.140 +
   4.141 +fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map},
   4.142 +  (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
   4.143 +
   4.144 +val compfuns = Predicate_Compile_Aux.CompilationFuns
   4.145 +    {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
   4.146 +    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   4.147 +    mk_not = mk_not, mk_map = mk_map}
   4.148 +
   4.149 +end;
   4.150 +
   4.151 +structure New_Pos_Random_Sequence_CompFuns =
   4.152 +struct
   4.153 +
   4.154 +fun mk_pos_random_dseqT T =
   4.155 +  @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
   4.156 +    @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
   4.157 +
   4.158 +fun dest_pos_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
   4.159 +    Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral},
   4.160 +    Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
   4.161 +  | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
   4.162 +
   4.163 +fun mk_bot T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
   4.164 +
   4.165 +fun mk_single t =
   4.166 +  let
   4.167 +    val T = fastype_of t
   4.168 +  in Const(@{const_name New_Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end;
   4.169 +
   4.170 +fun mk_bind (x, f) =
   4.171 +  let
   4.172 +    val T as Type ("fun", [_, U]) = fastype_of f
   4.173 +  in
   4.174 +    Const (@{const_name New_Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
   4.175 +  end;
   4.176 +
   4.177 +val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union};
   4.178 +
   4.179 +fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq},
   4.180 +  HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond;
   4.181 +
   4.182 +fun mk_not t =
   4.183 +  let
   4.184 +    val pT = mk_pos_random_dseqT HOLogic.unitT
   4.185 +    val nT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
   4.186 +      @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
   4.187 +        [Type (@{type_name Option.option}, [@{typ unit}])])
   4.188 +
   4.189 +  in Const (@{const_name New_Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end
   4.190 +
   4.191 +fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.pos_map},
   4.192 +  (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
   4.193 +
   4.194 +val compfuns = Predicate_Compile_Aux.CompilationFuns
   4.195 +    {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT,
   4.196 +    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   4.197 +    mk_not = mk_not, mk_map = mk_map}
   4.198 +
   4.199 +end;
   4.200 +
   4.201 +structure New_Neg_Random_Sequence_CompFuns =
   4.202 +struct
   4.203 +
   4.204 +fun mk_neg_random_dseqT T =
   4.205 +   @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
   4.206 +    @{typ code_numeral} --> 
   4.207 +    Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
   4.208 +
   4.209 +fun dest_neg_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
   4.210 +    Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral},
   4.211 +      Type (@{type_name Lazy_Sequence.lazy_sequence},
   4.212 +        [Type (@{type_name Option.option}, [T])])])])])])) = T
   4.213 +  | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
   4.214 +
   4.215 +fun mk_bot T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
   4.216 +
   4.217 +fun mk_single t =
   4.218 +  let
   4.219 +    val T = fastype_of t
   4.220 +  in Const(@{const_name New_Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end;
   4.221 +
   4.222 +fun mk_bind (x, f) =
   4.223 +  let
   4.224 +    val T as Type ("fun", [_, U]) = fastype_of f
   4.225 +  in
   4.226 +    Const (@{const_name New_Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
   4.227 +  end;
   4.228 +
   4.229 +val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union};
   4.230 +
   4.231 +fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq},
   4.232 +  HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
   4.233 +
   4.234 +fun mk_not t =
   4.235 +  let
   4.236 +    val nT = mk_neg_random_dseqT HOLogic.unitT
   4.237 +    val pT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
   4.238 +    @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}])
   4.239 +  in Const (@{const_name New_Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end
   4.240 +
   4.241 +fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.neg_map},
   4.242 +  (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
   4.243 +
   4.244 +val compfuns = Predicate_Compile_Aux.CompilationFuns
   4.245 +    {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT,
   4.246 +    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   4.247 +    mk_not = mk_not, mk_map = mk_map}
   4.248 +
   4.249 +end;
   4.250 +
   4.251 +structure Random_Sequence_CompFuns =
   4.252 +struct
   4.253 +
   4.254 +fun mk_random_dseqT T =
   4.255 +  @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
   4.256 +    HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, @{typ Random.seed})
   4.257 +
   4.258 +fun dest_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
   4.259 +  Type ("fun", [@{typ Random.seed},
   4.260 +  Type (@{type_name "*"}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
   4.261 +  | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
   4.262 +
   4.263 +fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
   4.264 +
   4.265 +fun mk_single t =
   4.266 +  let
   4.267 +    val T = fastype_of t
   4.268 +  in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end;
   4.269 +
   4.270 +fun mk_bind (x, f) =
   4.271 +  let
   4.272 +    val T as Type ("fun", [_, U]) = fastype_of f
   4.273 +  in
   4.274 +    Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
   4.275 +  end;
   4.276 +
   4.277 +val mk_sup = HOLogic.mk_binop @{const_name Random_Sequence.union};
   4.278 +
   4.279 +fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
   4.280 +  HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
   4.281 +
   4.282 +fun mk_not t =
   4.283 +  let
   4.284 +    val T = mk_random_dseqT HOLogic.unitT
   4.285 +  in Const (@{const_name Random_Sequence.not_random_dseq}, T --> T) $ t end
   4.286 +
   4.287 +fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.map},
   4.288 +  (T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp
   4.289 +
   4.290 +val compfuns = Predicate_Compile_Aux.CompilationFuns
   4.291 +    {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT,
   4.292 +    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   4.293 +    mk_not = mk_not, mk_map = mk_map}
   4.294 +
   4.295 +end;
   4.296 +
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Mar 30 15:46:50 2010 -0700
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Mar 31 16:44:41 2010 +0200
     5.3 @@ -66,9 +66,6 @@
     5.4    val code_pred_intro_attrib : attribute
     5.5    (* used by Quickcheck_Generator *) 
     5.6    (* temporary for testing of the compilation *)
     5.7 -  val pred_compfuns : compilation_funs
     5.8 -  val randompred_compfuns : compilation_funs
     5.9 -  val new_randompred_compfuns : compilation_funs
    5.10    val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
    5.11    val add_depth_limited_random_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
    5.12    val add_random_dseq_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory
    5.13 @@ -724,30 +721,6 @@
    5.14      PredData.map (Graph.map_node name (map_pred_data set))
    5.15    end
    5.16  
    5.17 -(* datastructures and setup for generic compilation *)
    5.18 -
    5.19 -datatype compilation_funs = CompilationFuns of {
    5.20 -  mk_predT : typ -> typ,
    5.21 -  dest_predT : typ -> typ,
    5.22 -  mk_bot : typ -> term,
    5.23 -  mk_single : term -> term,
    5.24 -  mk_bind : term * term -> term,
    5.25 -  mk_sup : term * term -> term,
    5.26 -  mk_if : term -> term,
    5.27 -  mk_not : term -> term,
    5.28 -  mk_map : typ -> typ -> term -> term -> term
    5.29 -};
    5.30 -
    5.31 -fun mk_predT (CompilationFuns funs) = #mk_predT funs
    5.32 -fun dest_predT (CompilationFuns funs) = #dest_predT funs
    5.33 -fun mk_bot (CompilationFuns funs) = #mk_bot funs
    5.34 -fun mk_single (CompilationFuns funs) = #mk_single funs
    5.35 -fun mk_bind (CompilationFuns funs) = #mk_bind funs
    5.36 -fun mk_sup (CompilationFuns funs) = #mk_sup funs
    5.37 -fun mk_if (CompilationFuns funs) = #mk_if funs
    5.38 -fun mk_not (CompilationFuns funs) = #mk_not funs
    5.39 -fun mk_map (CompilationFuns funs) = #mk_map funs
    5.40 -
    5.41  (* registration of alternative function names *)
    5.42  
    5.43  structure Alt_Compilations_Data = Theory_Data
    5.44 @@ -796,306 +769,8 @@
    5.45      (map (fn (mode, (fun_name, random)) => (mode, (functional_compilation fun_name mode, random)))
    5.46      fun_names)
    5.47  
    5.48 -(* structures for different compilations *)
    5.49 -
    5.50 -structure PredicateCompFuns =
    5.51 -struct
    5.52 -
    5.53 -fun mk_predT T = Type (@{type_name Predicate.pred}, [T])
    5.54 -
    5.55 -fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T
    5.56 -  | dest_predT T = raise TYPE ("dest_predT", [T], []);
    5.57 -
    5.58 -fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
    5.59 -
    5.60 -fun mk_single t =
    5.61 -  let val T = fastype_of t
    5.62 -  in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end;
    5.63 -
    5.64 -fun mk_bind (x, f) =
    5.65 -  let val T as Type ("fun", [_, U]) = fastype_of f
    5.66 -  in
    5.67 -    Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
    5.68 -  end;
    5.69 -
    5.70 -val mk_sup = HOLogic.mk_binop @{const_name sup};
    5.71 -
    5.72 -fun mk_if cond = Const (@{const_name Predicate.if_pred},
    5.73 -  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
    5.74 -
    5.75 -fun mk_not t =
    5.76 -  let
    5.77 -    val T = mk_predT HOLogic.unitT
    5.78 -  in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
    5.79 -
    5.80 -fun mk_Enum f =
    5.81 -  let val T as Type ("fun", [T', _]) = fastype_of f
    5.82 -  in
    5.83 -    Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f    
    5.84 -  end;
    5.85 -
    5.86 -fun mk_Eval (f, x) =
    5.87 -  let
    5.88 -    val T = fastype_of x
    5.89 -  in
    5.90 -    Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
    5.91 -  end;
    5.92 -
    5.93 -fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x)
    5.94 -
    5.95 -fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
    5.96 -  (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
    5.97 -
    5.98 -val compfuns = CompilationFuns {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
    5.99 -  mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, mk_not = mk_not,
   5.100 -  mk_map = mk_map};
   5.101 -
   5.102 -end;
   5.103 -
   5.104 -structure RandomPredCompFuns =
   5.105 -struct
   5.106 -
   5.107 -fun mk_randompredT T =
   5.108 -  @{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed})
   5.109 -
   5.110 -fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"},
   5.111 -  [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
   5.112 -  | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
   5.113 -
   5.114 -fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
   5.115 -
   5.116 -fun mk_single t =
   5.117 -  let               
   5.118 -    val T = fastype_of t
   5.119 -  in
   5.120 -    Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t
   5.121 -  end;
   5.122 -
   5.123 -fun mk_bind (x, f) =
   5.124 -  let
   5.125 -    val T as (Type ("fun", [_, U])) = fastype_of f
   5.126 -  in
   5.127 -    Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f
   5.128 -  end
   5.129 -
   5.130 -val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union}
   5.131 -
   5.132 -fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
   5.133 -  HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
   5.134 -
   5.135 -fun mk_not t =
   5.136 -  let
   5.137 -    val T = mk_randompredT HOLogic.unitT
   5.138 -  in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end
   5.139 -
   5.140 -fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map},
   5.141 -  (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
   5.142 -
   5.143 -val compfuns = CompilationFuns {mk_predT = mk_randompredT, dest_predT = dest_randompredT,
   5.144 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   5.145 -    mk_not = mk_not, mk_map = mk_map};
   5.146 -
   5.147 -end;
   5.148 -
   5.149 -structure DSequence_CompFuns =
   5.150 -struct
   5.151 -
   5.152 -fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
   5.153 -  Type (@{type_name Option.option}, [Type  (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])
   5.154 -
   5.155 -fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool},
   5.156 -  Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
   5.157 -  | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
   5.158 -
   5.159 -fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T);
   5.160 -
   5.161 -fun mk_single t =
   5.162 -  let val T = fastype_of t
   5.163 -  in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end;
   5.164 -
   5.165 -fun mk_bind (x, f) =
   5.166 -  let val T as Type ("fun", [_, U]) = fastype_of f
   5.167 -  in
   5.168 -    Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
   5.169 -  end;
   5.170 -
   5.171 -val mk_sup = HOLogic.mk_binop @{const_name DSequence.union};
   5.172 -
   5.173 -fun mk_if cond = Const (@{const_name DSequence.if_seq},
   5.174 -  HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
   5.175 -
   5.176 -fun mk_not t = let val T = mk_dseqT HOLogic.unitT
   5.177 -  in Const (@{const_name DSequence.not_seq}, T --> T) $ t end
   5.178 -
   5.179 -fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map},
   5.180 -  (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
   5.181 -
   5.182 -val compfuns = CompilationFuns {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
   5.183 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   5.184 -    mk_not = mk_not, mk_map = mk_map}
   5.185 -
   5.186 -end;
   5.187 -
   5.188 -structure New_Pos_Random_Sequence_CompFuns =
   5.189 -struct
   5.190 -
   5.191 -fun mk_pos_random_dseqT T =
   5.192 -  @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
   5.193 -    @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])
   5.194 -
   5.195 -fun dest_pos_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
   5.196 -    Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral},
   5.197 -    Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
   5.198 -  | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
   5.199 -
   5.200 -fun mk_bot T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
   5.201 -
   5.202 -fun mk_single t =
   5.203 -  let
   5.204 -    val T = fastype_of t
   5.205 -  in Const(@{const_name New_Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end;
   5.206 -
   5.207 -fun mk_bind (x, f) =
   5.208 -  let
   5.209 -    val T as Type ("fun", [_, U]) = fastype_of f
   5.210 -  in
   5.211 -    Const (@{const_name New_Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f
   5.212 -  end;
   5.213 -
   5.214 -val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union};
   5.215 -
   5.216 -fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq},
   5.217 -  HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond;
   5.218 -
   5.219 -fun mk_not t =
   5.220 -  let
   5.221 -    val pT = mk_pos_random_dseqT HOLogic.unitT
   5.222 -    val nT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
   5.223 -      @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence},
   5.224 -        [Type (@{type_name Option.option}, [@{typ unit}])])
   5.225 -
   5.226 -  in Const (@{const_name New_Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end
   5.227 -
   5.228 -fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.pos_map},
   5.229 -  (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
   5.230 -
   5.231 -val compfuns = CompilationFuns {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT,
   5.232 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   5.233 -    mk_not = mk_not, mk_map = mk_map}
   5.234 -
   5.235 -end;
   5.236 -
   5.237 -structure New_Neg_Random_Sequence_CompFuns =
   5.238 -struct
   5.239 -
   5.240 -fun mk_neg_random_dseqT T =
   5.241 -   @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
   5.242 -    @{typ code_numeral} --> 
   5.243 -    Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])
   5.244 -
   5.245 -fun dest_neg_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
   5.246 -    Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral},
   5.247 -      Type (@{type_name Lazy_Sequence.lazy_sequence},
   5.248 -        [Type (@{type_name Option.option}, [T])])])])])])) = T
   5.249 -  | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
   5.250 -
   5.251 -fun mk_bot T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
   5.252 -
   5.253 -fun mk_single t =
   5.254 -  let
   5.255 -    val T = fastype_of t
   5.256 -  in Const(@{const_name New_Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end;
   5.257 -
   5.258 -fun mk_bind (x, f) =
   5.259 -  let
   5.260 -    val T as Type ("fun", [_, U]) = fastype_of f
   5.261 -  in
   5.262 -    Const (@{const_name New_Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f
   5.263 -  end;
   5.264 -
   5.265 -val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union};
   5.266 -
   5.267 -fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq},
   5.268 -  HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
   5.269 -
   5.270 -fun mk_not t =
   5.271 -  let
   5.272 -    val nT = mk_neg_random_dseqT HOLogic.unitT
   5.273 -    val pT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
   5.274 -    @{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}])
   5.275 -  in Const (@{const_name New_Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end
   5.276 -
   5.277 -fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.neg_map},
   5.278 -  (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
   5.279 -
   5.280 -val compfuns = CompilationFuns {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT,
   5.281 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   5.282 -    mk_not = mk_not, mk_map = mk_map}
   5.283 -
   5.284 -end;
   5.285 -
   5.286 -structure Random_Sequence_CompFuns =
   5.287 -struct
   5.288 -
   5.289 -fun mk_random_dseqT T =
   5.290 -  @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} -->
   5.291 -    HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, @{typ Random.seed})
   5.292 -
   5.293 -fun dest_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral},
   5.294 -  Type ("fun", [@{typ Random.seed},
   5.295 -  Type (@{type_name "*"}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
   5.296 -  | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
   5.297 -
   5.298 -fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
   5.299 -
   5.300 -fun mk_single t =
   5.301 -  let
   5.302 -    val T = fastype_of t
   5.303 -  in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end;
   5.304 -
   5.305 -fun mk_bind (x, f) =
   5.306 -  let
   5.307 -    val T as Type ("fun", [_, U]) = fastype_of f
   5.308 -  in
   5.309 -    Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
   5.310 -  end;
   5.311 -
   5.312 -val mk_sup = HOLogic.mk_binop @{const_name Random_Sequence.union};
   5.313 -
   5.314 -fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
   5.315 -  HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
   5.316 -
   5.317 -fun mk_not t =
   5.318 -  let
   5.319 -    val T = mk_random_dseqT HOLogic.unitT
   5.320 -  in Const (@{const_name Random_Sequence.not_random_dseq}, T --> T) $ t end
   5.321 -
   5.322 -fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.map},
   5.323 -  (T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp
   5.324 -
   5.325 -val compfuns = CompilationFuns {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT,
   5.326 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   5.327 -    mk_not = mk_not, mk_map = mk_map}
   5.328 -
   5.329 -end;
   5.330 -
   5.331 -(* for external use with interactive mode *)
   5.332 -val pred_compfuns = PredicateCompFuns.compfuns
   5.333 -val randompred_compfuns = Random_Sequence_CompFuns.compfuns;
   5.334 -val new_randompred_compfuns = New_Pos_Random_Sequence_CompFuns.compfuns
   5.335 -
   5.336  (* compilation modifiers *)
   5.337  
   5.338 -(* function types and names of different compilations *)
   5.339 -
   5.340 -fun funT_of compfuns mode T =
   5.341 -  let
   5.342 -    val Ts = binder_types T
   5.343 -    val (inTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts
   5.344 -  in
   5.345 -    inTs ---> (mk_predT compfuns (HOLogic.mk_tupleT outTs))
   5.346 -  end;
   5.347 -
   5.348  structure Comp_Mod =
   5.349  struct
   5.350  
     6.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Tue Mar 30 15:46:50 2010 -0700
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Mar 31 16:44:41 2010 +0200
     6.3 @@ -142,19 +142,17 @@
     6.4      (set_function_flattening (!function_flattening)
     6.5        (if !debug then debug_options else options))
     6.6  
     6.7 -fun dest_compfuns (Predicate_Compile_Core.CompilationFuns funs) = funs
     6.8 -val mk_predT = #mk_predT (dest_compfuns Predicate_Compile_Core.pred_compfuns)
     6.9 -val mk_return' = #mk_single (dest_compfuns Predicate_Compile_Core.pred_compfuns)
    6.10 -val mk_bind' = #mk_bind (dest_compfuns Predicate_Compile_Core.pred_compfuns)
    6.11 +val mk_predT = Predicate_Compile_Aux.mk_predT PredicateCompFuns.compfuns
    6.12 +val mk_return' = Predicate_Compile_Aux.mk_single PredicateCompFuns.compfuns
    6.13 +val mk_bind' = Predicate_Compile_Aux.mk_bind PredicateCompFuns.compfuns
    6.14  
    6.15 -val mk_randompredT = #mk_predT (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
    6.16 -val mk_return = #mk_single (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
    6.17 -val mk_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.randompred_compfuns)
    6.18 +val mk_randompredT = Predicate_Compile_Aux.mk_predT RandomPredCompFuns.compfuns
    6.19 +val mk_return = Predicate_Compile_Aux.mk_single RandomPredCompFuns.compfuns
    6.20 +val mk_bind = Predicate_Compile_Aux.mk_bind RandomPredCompFuns.compfuns
    6.21  
    6.22 -val mk_new_randompredT = #mk_predT (dest_compfuns Predicate_Compile_Core.new_randompred_compfuns)
    6.23 -val mk_new_return = #mk_single (dest_compfuns Predicate_Compile_Core.new_randompred_compfuns)
    6.24 -val mk_new_bind = #mk_bind (dest_compfuns Predicate_Compile_Core.new_randompred_compfuns)
    6.25 -
    6.26 +val mk_new_randompredT = Predicate_Compile_Aux.mk_predT New_Pos_Random_Sequence_CompFuns.compfuns
    6.27 +val mk_new_return = Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.compfuns
    6.28 +val mk_new_bind = Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.compfuns
    6.29  
    6.30  fun mk_split_lambda [] t = Abs ("u", HOLogic.unitT, t)
    6.31    | mk_split_lambda [x] t = lambda x t