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