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