author | bulwahn |
Fri, 11 Nov 2011 08:32:45 +0100 | |
changeset 45450 | dc2236b19a3d |
parent 41941 | f823f7fae9a2 |
child 45461 | 130c90bb80b4 |
permissions | -rw-r--r-- |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
2 |
Author: Lukas Bulwahn, TU Muenchen |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
3 |
|
41941 | 4 |
Structures for different compilations of the predicate compiler. |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
5 |
*) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
6 |
|
45450 | 7 |
structure Predicate_Comp_Funs = |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
8 |
struct |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
9 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
10 |
fun mk_predT T = Type (@{type_name Predicate.pred}, [T]) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
11 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
12 |
fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
13 |
| dest_predT T = raise TYPE ("dest_predT", [T], []); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
14 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
15 |
fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
16 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
17 |
fun mk_single t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
18 |
let val T = fastype_of t |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
19 |
in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
20 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
21 |
fun mk_bind (x, f) = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
22 |
let val T as Type ("fun", [_, U]) = fastype_of f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
23 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
24 |
Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
25 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
26 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
27 |
val mk_sup = HOLogic.mk_binop @{const_name sup}; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
28 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
29 |
fun mk_if cond = Const (@{const_name Predicate.if_pred}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
30 |
HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
31 |
|
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
32 |
fun mk_iterate_upto T (f, from, to) = |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
33 |
list_comb (Const (@{const_name Code_Numeral.iterate_upto}, |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
34 |
[@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_predT T), |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
35 |
[f, from, to]) |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
36 |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
37 |
fun mk_not t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
38 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
39 |
val T = mk_predT HOLogic.unitT |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
40 |
in Const (@{const_name Predicate.not_pred}, T --> T) $ t end |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
41 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
42 |
fun mk_Enum f = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
43 |
let val T as Type ("fun", [T', _]) = fastype_of f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
44 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
45 |
Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
46 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
47 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
48 |
fun mk_Eval (f, x) = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
49 |
let |
39648
655307cb8489
rewriting function mk_Eval_of in predicate compiler
bulwahn
parents:
37678
diff
changeset
|
50 |
val T = dest_predT (fastype_of f) |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
51 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
52 |
Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
53 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
54 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
55 |
fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
56 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
57 |
fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
58 |
(T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
59 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
60 |
val compfuns = Predicate_Compile_Aux.CompilationFuns |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
61 |
{mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot, |
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
62 |
mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
63 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}; |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
64 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
65 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
66 |
|
45450 | 67 |
structure CPS_Comp_Funs = |
68 |
struct |
|
69 |
||
70 |
fun mk_predT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"} |
|
71 |
||
72 |
fun dest_predT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = T |
|
73 |
| dest_predT T = raise TYPE ("dest_predT", [T], []); |
|
74 |
||
75 |
fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_predT T); |
|
76 |
||
77 |
fun mk_single t = |
|
78 |
let val T = fastype_of t |
|
79 |
in Const(@{const_name Quickcheck_Exhaustive.cps_single}, T --> mk_predT T) $ t end; |
|
80 |
||
81 |
fun mk_bind (x, f) = |
|
82 |
let val T as Type ("fun", [_, U]) = fastype_of f |
|
83 |
in |
|
84 |
Const (@{const_name Quickcheck_Exhaustive.cps_bind}, fastype_of x --> T --> U) $ x $ f |
|
85 |
end; |
|
86 |
||
87 |
val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus}; |
|
88 |
||
89 |
fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.cps_if}, |
|
90 |
HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond; |
|
91 |
||
92 |
fun mk_iterate_upto T (f, from, to) = error "not implemented yet" |
|
93 |
||
94 |
fun mk_not t = |
|
95 |
let |
|
96 |
val T = mk_predT HOLogic.unitT |
|
97 |
in Const (@{const_name Quickcheck_Exhaustive.cps_not}, T --> T) $ t end |
|
98 |
||
99 |
fun mk_Enum f = error "not implemented" |
|
100 |
||
101 |
fun mk_Eval (f, x) = error "not implemented" |
|
102 |
||
103 |
fun dest_Eval t = error "not implemented" |
|
104 |
||
105 |
fun mk_map T1 T2 tf tp = error "not implemented" |
|
106 |
||
107 |
val compfuns = Predicate_Compile_Aux.CompilationFuns |
|
108 |
{mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot, |
|
109 |
mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
|
110 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}; |
|
111 |
||
112 |
end; |
|
113 |
||
114 |
structure Pos_Bounded_CPS_Comp_Funs = |
|
115 |
struct |
|
116 |
||
117 |
fun mk_predT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "code_numeral => Code_Evaluation.term list option"} |
|
118 |
||
119 |
fun dest_predT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "code_numeral => term list option"}])) = T |
|
120 |
| dest_predT T = raise TYPE ("dest_predT", [T], []); |
|
121 |
||
122 |
fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_predT T); |
|
123 |
||
124 |
fun mk_single t = |
|
125 |
let val T = fastype_of t |
|
126 |
in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, T --> mk_predT T) $ t end; |
|
127 |
||
128 |
fun mk_bind (x, f) = |
|
129 |
let val T as Type ("fun", [_, U]) = fastype_of f |
|
130 |
in |
|
131 |
Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f |
|
132 |
end; |
|
133 |
||
134 |
val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus}; |
|
135 |
||
136 |
fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if}, |
|
137 |
HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond; |
|
138 |
||
139 |
fun mk_iterate_upto T (f, from, to) = error "not implemented yet" |
|
140 |
||
141 |
fun mk_not t = |
|
142 |
let |
|
143 |
val nT = @{typ "(unit Quickcheck_Exhaustive.unknown => |
|
144 |
Code_Evaluation.term list Quickcheck_Exhaustive.three_valued) => code_numeral => |
|
145 |
Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"} |
|
146 |
val T = mk_predT HOLogic.unitT |
|
147 |
in Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_not}, nT --> T) $ t end |
|
148 |
||
149 |
fun mk_Enum f = error "not implemented" |
|
150 |
||
151 |
fun mk_Eval (f, x) = error "not implemented" |
|
152 |
||
153 |
fun dest_Eval t = error "not implemented" |
|
154 |
||
155 |
fun mk_map T1 T2 tf tp = error "not implemented" |
|
156 |
||
157 |
val compfuns = Predicate_Compile_Aux.CompilationFuns |
|
158 |
{mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot, |
|
159 |
mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
|
160 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}; |
|
161 |
||
162 |
end; |
|
163 |
||
164 |
structure Neg_Bounded_CPS_Comp_Funs = |
|
165 |
struct |
|
166 |
||
167 |
fun mk_predT T = |
|
168 |
(Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]) |
|
169 |
--> @{typ "Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}) |
|
170 |
--> @{typ "code_numeral => Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"} |
|
171 |
||
172 |
fun dest_predT (Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]), |
|
173 |
@{typ "term list Quickcheck_Exhaustive.three_valued"}]), |
|
174 |
@{typ "code_numeral => term list Quickcheck_Exhaustive.three_valued"}])) = T |
|
175 |
| dest_predT T = raise TYPE ("dest_predT", [T], []); |
|
176 |
||
177 |
fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_predT T); |
|
178 |
||
179 |
fun mk_single t = |
|
180 |
let val T = fastype_of t |
|
181 |
in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, T --> mk_predT T) $ t end; |
|
182 |
||
183 |
fun mk_bind (x, f) = |
|
184 |
let val T as Type ("fun", [_, U]) = fastype_of f |
|
185 |
in |
|
186 |
Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f |
|
187 |
end; |
|
188 |
||
189 |
val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus}; |
|
190 |
||
191 |
fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_if}, |
|
192 |
HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond; |
|
193 |
||
194 |
fun mk_iterate_upto T (f, from, to) = error "not implemented" |
|
195 |
||
196 |
fun mk_not t = |
|
197 |
let |
|
198 |
val T = mk_predT HOLogic.unitT |
|
199 |
val pT = @{typ "(unit => Code_Evaluation.term list option) => code_numeral => Code_Evaluation.term list option"} |
|
200 |
in Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_not}, pT --> T) $ t end |
|
201 |
||
202 |
fun mk_Enum f = error "not implemented" |
|
203 |
||
204 |
fun mk_Eval (f, x) = error "not implemented" |
|
205 |
||
206 |
fun dest_Eval t = error "not implemented" |
|
207 |
||
208 |
fun mk_map T1 T2 tf tp = error "not implemented" |
|
209 |
||
210 |
val compfuns = Predicate_Compile_Aux.CompilationFuns |
|
211 |
{mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot, |
|
212 |
mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
|
213 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}; |
|
214 |
||
215 |
end; |
|
216 |
||
217 |
||
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
218 |
structure RandomPredCompFuns = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
219 |
struct |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
220 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
221 |
fun mk_randompredT T = |
45450 | 222 |
@{typ Random.seed} --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_predT T, @{typ Random.seed}) |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
223 |
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36049
diff
changeset
|
224 |
fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod}, |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
225 |
[Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
226 |
| dest_randompredT T = raise TYPE ("dest_randompredT", [T], []); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
227 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
228 |
fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
229 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
230 |
fun mk_single t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
231 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
232 |
val T = fastype_of t |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
233 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
234 |
Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
235 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
236 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
237 |
fun mk_bind (x, f) = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
238 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
239 |
val T as (Type ("fun", [_, U])) = fastype_of f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
240 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
241 |
Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
242 |
end |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
243 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
244 |
val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union} |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
245 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
246 |
fun mk_if cond = Const (@{const_name Quickcheck.if_randompred}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
247 |
HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
248 |
|
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
249 |
fun mk_iterate_upto T (f, from, to) = |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
250 |
list_comb (Const (@{const_name Quickcheck.iterate_upto}, |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
251 |
[@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_randompredT T), |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
252 |
[f, from, to]) |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
253 |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
254 |
fun mk_not t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
255 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
256 |
val T = mk_randompredT HOLogic.unitT |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
257 |
in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
258 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
259 |
fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
260 |
(T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
261 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
262 |
val compfuns = Predicate_Compile_Aux.CompilationFuns |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
263 |
{mk_predT = mk_randompredT, dest_predT = dest_randompredT, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
264 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
265 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}; |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
266 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
267 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
268 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
269 |
structure DSequence_CompFuns = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
270 |
struct |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
271 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
272 |
fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
273 |
Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])]) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
274 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
275 |
fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
276 |
Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
277 |
| dest_dseqT T = raise TYPE ("dest_dseqT", [T], []); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
278 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
279 |
fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
280 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
281 |
fun mk_single t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
282 |
let val T = fastype_of t |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
283 |
in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
284 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
285 |
fun mk_bind (x, f) = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
286 |
let val T as Type ("fun", [_, U]) = fastype_of f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
287 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
288 |
Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
289 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
290 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
291 |
val mk_sup = HOLogic.mk_binop @{const_name DSequence.union}; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
292 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
293 |
fun mk_if cond = Const (@{const_name DSequence.if_seq}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
294 |
HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
295 |
|
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
296 |
fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation" |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
297 |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
298 |
fun mk_not t = let val T = mk_dseqT HOLogic.unitT |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
299 |
in Const (@{const_name DSequence.not_seq}, T --> T) $ t end |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
300 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
301 |
fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
302 |
(T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
303 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
304 |
val compfuns = Predicate_Compile_Aux.CompilationFuns |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
305 |
{mk_predT = mk_dseqT, dest_predT = dest_dseqT, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
306 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
307 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
308 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
309 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
310 |
|
40051
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
311 |
structure New_Pos_DSequence_CompFuns = |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
312 |
struct |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
313 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
314 |
fun mk_pos_dseqT T = |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
315 |
@{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T]) |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
316 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
317 |
fun dest_pos_dseqT (Type ("fun", [@{typ code_numeral}, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
318 |
Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
319 |
| dest_pos_dseqT T = raise TYPE ("dest_pos_dseqT", [T], []); |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
320 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
321 |
fun mk_bot T = Const (@{const_name New_DSequence.pos_empty}, mk_pos_dseqT T); |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
322 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
323 |
fun mk_single t = |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
324 |
let |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
325 |
val T = fastype_of t |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
326 |
in Const(@{const_name New_DSequence.pos_single}, T --> mk_pos_dseqT T) $ t end; |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
327 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
328 |
fun mk_bind (x, f) = |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
329 |
let |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
330 |
val T as Type ("fun", [_, U]) = fastype_of f |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
331 |
in |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
332 |
Const (@{const_name New_DSequence.pos_bind}, fastype_of x --> T --> U) $ x $ f |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
333 |
end; |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
334 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
335 |
fun mk_decr_bind (x, f) = |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
336 |
let |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
337 |
val T as Type ("fun", [_, U]) = fastype_of f |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
338 |
in |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
339 |
Const (@{const_name New_DSequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
340 |
end; |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
341 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
342 |
val mk_sup = HOLogic.mk_binop @{const_name New_DSequence.pos_union}; |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
343 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
344 |
fun mk_if cond = Const (@{const_name New_DSequence.pos_if_seq}, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
345 |
HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond; |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
346 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
347 |
fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation" |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
348 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
349 |
fun mk_not t = |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
350 |
let |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
351 |
val pT = mk_pos_dseqT HOLogic.unitT |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
352 |
val nT = |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
353 |
@{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
354 |
[Type (@{type_name Option.option}, [@{typ unit}])]) |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
355 |
in Const (@{const_name New_DSequence.pos_not_seq}, nT --> pT) $ t end |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
356 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
357 |
fun mk_map T1 T2 tf tp = Const (@{const_name New_DSequence.pos_map}, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
358 |
(T1 --> T2) --> mk_pos_dseqT T1 --> mk_pos_dseqT T2) $ tf $ tp |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
359 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
360 |
val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
361 |
{mk_predT = mk_pos_dseqT, dest_predT = dest_pos_dseqT, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
362 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
363 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
364 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
365 |
val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
366 |
{mk_predT = mk_pos_dseqT, dest_predT = dest_pos_dseqT, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
367 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
368 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
369 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
370 |
end; |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
371 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
372 |
structure New_Neg_DSequence_CompFuns = |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
373 |
struct |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
374 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
375 |
fun mk_neg_dseqT T = @{typ code_numeral} --> |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
376 |
Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])]) |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
377 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
378 |
fun dest_neg_dseqT (Type ("fun", [@{typ code_numeral}, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
379 |
Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) = T |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
380 |
| dest_neg_dseqT T = raise TYPE ("dest_neg_dseqT", [T], []); |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
381 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
382 |
fun mk_bot T = Const (@{const_name New_DSequence.neg_empty}, mk_neg_dseqT T); |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
383 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
384 |
fun mk_single t = |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
385 |
let |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
386 |
val T = fastype_of t |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
387 |
in Const(@{const_name New_DSequence.neg_single}, T --> mk_neg_dseqT T) $ t end; |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
388 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
389 |
fun mk_bind (x, f) = |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
390 |
let |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
391 |
val T as Type ("fun", [_, U]) = fastype_of f |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
392 |
in |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
393 |
Const (@{const_name New_DSequence.neg_bind}, fastype_of x --> T --> U) $ x $ f |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
394 |
end; |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
395 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
396 |
fun mk_decr_bind (x, f) = |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
397 |
let |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
398 |
val T as Type ("fun", [_, U]) = fastype_of f |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
399 |
in |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
400 |
Const (@{const_name New_DSequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
401 |
end; |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
402 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
403 |
val mk_sup = HOLogic.mk_binop @{const_name New_DSequence.neg_union}; |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
404 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
405 |
fun mk_if cond = Const (@{const_name New_DSequence.neg_if_seq}, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
406 |
HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond; |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
407 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
408 |
fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation" |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
409 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
410 |
fun mk_not t = |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
411 |
let |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
412 |
val nT = mk_neg_dseqT HOLogic.unitT |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
413 |
val pT = |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
414 |
@{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
415 |
[@{typ unit}]) |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
416 |
in Const (@{const_name New_DSequence.neg_not_seq}, pT --> nT) $ t end |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
417 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
418 |
fun mk_map T1 T2 tf tp = Const (@{const_name New_DSequence.neg_map}, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
419 |
(T1 --> T2) --> mk_neg_dseqT T1 --> mk_neg_dseqT T2) $ tf $ tp |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
420 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
421 |
val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
422 |
{mk_predT = mk_neg_dseqT, dest_predT = dest_neg_dseqT, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
423 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
424 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
425 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
426 |
val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
427 |
{mk_predT = mk_neg_dseqT, dest_predT = dest_neg_dseqT, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
428 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
429 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
430 |
|
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
431 |
end; |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
432 |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
433 |
structure New_Pos_Random_Sequence_CompFuns = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
434 |
struct |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
435 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
436 |
fun mk_pos_random_dseqT T = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
437 |
@{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} --> |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
438 |
@{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T]) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
439 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
440 |
fun dest_pos_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
441 |
Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
442 |
Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
443 |
| dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
444 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
445 |
fun mk_bot T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
446 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
447 |
fun mk_single t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
448 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
449 |
val T = fastype_of t |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
450 |
in Const(@{const_name New_Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
451 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
452 |
fun mk_bind (x, f) = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
453 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
454 |
val T as Type ("fun", [_, U]) = fastype_of f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
455 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
456 |
Const (@{const_name New_Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
457 |
end; |
40051
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
458 |
|
40049
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
459 |
fun mk_decr_bind (x, f) = |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
460 |
let |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
461 |
val T as Type ("fun", [_, U]) = fastype_of f |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
462 |
in |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
463 |
Const (@{const_name New_Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
464 |
end; |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
465 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
466 |
val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union}; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
467 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
468 |
fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
469 |
HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
470 |
|
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
471 |
fun mk_iterate_upto T (f, from, to) = |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
472 |
list_comb (Const (@{const_name New_Random_Sequence.pos_iterate_upto}, |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
473 |
[@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
474 |
---> mk_pos_random_dseqT T), |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
475 |
[f, from, to]) |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
476 |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
477 |
fun mk_not t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
478 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
479 |
val pT = mk_pos_random_dseqT HOLogic.unitT |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
480 |
val nT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} --> |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
481 |
@{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
482 |
[Type (@{type_name Option.option}, [@{typ unit}])]) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
483 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
484 |
in Const (@{const_name New_Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
485 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
486 |
fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.pos_map}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
487 |
(T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
488 |
|
40049
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
489 |
val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
490 |
{mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT, |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
491 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if, |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
492 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
493 |
|
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
494 |
val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
495 |
{mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
496 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
497 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
498 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
499 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
500 |
structure New_Neg_Random_Sequence_CompFuns = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
501 |
struct |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
502 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
503 |
fun mk_neg_random_dseqT T = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
504 |
@{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} --> |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
505 |
@{typ code_numeral} --> |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
506 |
Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])]) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
507 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
508 |
fun dest_neg_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
509 |
Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
510 |
Type (@{type_name Lazy_Sequence.lazy_sequence}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
511 |
[Type (@{type_name Option.option}, [T])])])])])])) = T |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
512 |
| dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
513 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
514 |
fun mk_bot T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
515 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
516 |
fun mk_single t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
517 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
518 |
val T = fastype_of t |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
519 |
in Const(@{const_name New_Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
520 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
521 |
fun mk_bind (x, f) = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
522 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
523 |
val T as Type ("fun", [_, U]) = fastype_of f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
524 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
525 |
Const (@{const_name New_Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
526 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
527 |
|
40049
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
528 |
fun mk_decr_bind (x, f) = |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
529 |
let |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
530 |
val T as Type ("fun", [_, U]) = fastype_of f |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
531 |
in |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
532 |
Const (@{const_name New_Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
533 |
end; |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
534 |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
535 |
val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union}; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
536 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
537 |
fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
538 |
HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
539 |
|
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
540 |
fun mk_iterate_upto T (f, from, to) = |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
541 |
list_comb (Const (@{const_name New_Random_Sequence.neg_iterate_upto}, |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
542 |
[@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
543 |
---> mk_neg_random_dseqT T), |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
544 |
[f, from, to]) |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
545 |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
546 |
fun mk_not t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
547 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
548 |
val nT = mk_neg_random_dseqT HOLogic.unitT |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
549 |
val pT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} --> |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
550 |
@{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}]) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
551 |
in Const (@{const_name New_Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
552 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
553 |
fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.neg_map}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
554 |
(T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
555 |
|
40049
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
556 |
val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
557 |
{mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT, |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
558 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if, |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
559 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} |
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
560 |
|
75d9f57123d6
adding decreasing bind and non-decreasing bind; depth-limited and depth-unlimited compilation possible
bulwahn
parents:
39648
diff
changeset
|
561 |
val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
562 |
{mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
563 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
564 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
565 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
566 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
567 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
568 |
structure Random_Sequence_CompFuns = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
569 |
struct |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
570 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
571 |
fun mk_random_dseqT T = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
572 |
@{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} --> |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
573 |
HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, @{typ Random.seed}) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
574 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
575 |
fun dest_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
576 |
Type ("fun", [@{typ Random.seed}, |
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36049
diff
changeset
|
577 |
Type (@{type_name Product_Type.prod}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
578 |
| dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
579 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
580 |
fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
581 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
582 |
fun mk_single t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
583 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
584 |
val T = fastype_of t |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
585 |
in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
586 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
587 |
fun mk_bind (x, f) = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
588 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
589 |
val T as Type ("fun", [_, U]) = fastype_of f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
590 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
591 |
Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
592 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
593 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
594 |
val mk_sup = HOLogic.mk_binop @{const_name Random_Sequence.union}; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
595 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
596 |
fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
597 |
HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
598 |
|
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
599 |
fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation" |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
600 |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
601 |
fun mk_not t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
602 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
603 |
val T = mk_random_dseqT HOLogic.unitT |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
604 |
in Const (@{const_name Random_Sequence.not_random_dseq}, T --> T) $ t end |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
605 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
606 |
fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.map}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
607 |
(T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
608 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
609 |
val compfuns = Predicate_Compile_Aux.CompilationFuns |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
610 |
{mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
611 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
612 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map} |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
613 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
614 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
615 |