author | wenzelm |
Wed, 12 Feb 2014 13:33:05 +0100 | |
changeset 55437 | 3fd63b92ea3b |
parent 51143 | 0a2371e7ced3 |
child 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 |
|
45461
130c90bb80b4
using more conventional names for monad plus operations
bulwahn
parents:
45450
diff
changeset
|
10 |
fun mk_monadT T = Type (@{type_name Predicate.pred}, [T]) |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
11 |
|
45461
130c90bb80b4
using more conventional names for monad plus operations
bulwahn
parents:
45450
diff
changeset
|
12 |
fun dest_monadT (Type (@{type_name Predicate.pred}, [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 |
|
55437 | 15 |
fun mk_empty T = Const (@{const_name Orderings.bot}, 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 |
55437 | 19 |
in Const(@{const_name Predicate.single}, 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 |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
24 |
Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f |
55437 | 25 |
end |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
26 |
|
55437 | 27 |
val mk_plus = HOLogic.mk_binop @{const_name sup} |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
28 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
29 |
fun mk_if cond = Const (@{const_name Predicate.if_pred}, |
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) = |
46664
1f6c140f9c72
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
haftmann
parents:
46638
diff
changeset
|
33 |
list_comb (Const (@{const_name Predicate.iterate_upto}, |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
34 |
[@{typ natural} --> T, @{typ natural}, @{typ natural}] ---> 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 |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
40 |
in Const (@{const_name Predicate.not_pred}, T --> T) $ t end |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
41 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
42 |
fun mk_Enum f = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
43 |
let val T as Type ("fun", [T', _]) = fastype_of f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
44 |
in |
45461
130c90bb80b4
using more conventional names for monad plus operations
bulwahn
parents:
45450
diff
changeset
|
45 |
Const (@{const_name Predicate.Pred}, 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 |
45461
130c90bb80b4
using more conventional names for monad plus operations
bulwahn
parents:
45450
diff
changeset
|
52 |
Const (@{const_name Predicate.eval}, 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 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
55 |
fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
56 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
57 |
fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map}, |
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 = |
73 |
(T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"} |
|
45450 | 74 |
|
55437 | 75 |
fun dest_monadT |
76 |
(Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = 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 |
|
55437 | 79 |
fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_monadT T) |
45450 | 80 |
|
81 |
fun mk_single t = |
|
82 |
let val T = fastype_of t |
|
55437 | 83 |
in Const(@{const_name Quickcheck_Exhaustive.cps_single}, 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 |
|
88 |
Const (@{const_name Quickcheck_Exhaustive.cps_bind}, fastype_of x --> T --> U) $ x $ f |
|
55437 | 89 |
end |
45450 | 90 |
|
55437 | 91 |
val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus} |
45450 | 92 |
|
93 |
fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.cps_if}, |
|
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 |
45450 | 101 |
in Const (@{const_name Quickcheck_Exhaustive.cps_not}, T --> T) $ t end |
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 |
||
45750
17100f4ce0b5
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
bulwahn
parents:
45461
diff
changeset
|
123 |
val resultT = @{typ "(bool * Code_Evaluation.term list) option"} |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
124 |
fun mk_monadT T = (T --> resultT) --> @{typ "natural"} --> resultT |
45450 | 125 |
|
45750
17100f4ce0b5
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
bulwahn
parents:
45461
diff
changeset
|
126 |
fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "(bool * term list) option"}]), |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
127 |
@{typ "natural => (bool * term list) option"}])) = T |
55437 | 128 |
| dest_monadT T = raise TYPE ("dest_monadT", [T], []) |
45450 | 129 |
|
55437 | 130 |
fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_monadT T) |
45450 | 131 |
|
132 |
fun mk_single t = |
|
133 |
let val T = fastype_of t |
|
55437 | 134 |
in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, 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 |
|
139 |
Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f |
|
140 |
end; |
|
141 |
||
55437 | 142 |
val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus} |
45450 | 143 |
|
55437 | 144 |
fun mk_if cond = |
145 |
Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if}, |
|
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 |
|
152 |
val nT = @{typ "(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 => |
45450 | 154 |
Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"} |
45461
130c90bb80b4
using more conventional names for monad plus operations
bulwahn
parents:
45450
diff
changeset
|
155 |
val T = mk_monadT HOLogic.unitT |
45450 | 156 |
in Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_not}, nT --> T) $ t end |
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 = |
45450 | 179 |
(Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]) |
180 |
--> @{typ "Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}) |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
181 |
--> @{typ "natural => Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"} |
45450 | 182 |
|
55437 | 183 |
fun dest_monadT |
184 |
(Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]), |
|
185 |
@{typ "term list Quickcheck_Exhaustive.three_valued"}]), |
|
186 |
@{typ "natural => term list Quickcheck_Exhaustive.three_valued"}])) = 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 |
|
55437 | 189 |
fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_monadT T) |
45450 | 190 |
|
191 |
fun mk_single t = |
|
192 |
let val T = fastype_of t |
|
55437 | 193 |
in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, 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 |
|
198 |
Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f |
|
199 |
end; |
|
200 |
||
55437 | 201 |
val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus} |
45450 | 202 |
|
203 |
fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_if}, |
|
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 |
45750
17100f4ce0b5
adding genuine flag to predicate_compile_quickcheck and prolog_quickcheck (cf. 5e46c225370e);
bulwahn
parents:
45461
diff
changeset
|
211 |
val pT = @{typ "(unit => (bool * Code_Evaluation.term list) option)"} |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
212 |
--> @{typ "natural => (bool * Code_Evaluation.term list) option"} |
45450 | 213 |
in Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_not}, pT --> T) $ t end |
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 = |
45461
130c90bb80b4
using more conventional names for monad plus operations
bulwahn
parents:
45450
diff
changeset
|
236 |
@{typ Random.seed} --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_monadT T, @{typ Random.seed}) |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
237 |
|
37678
0040bafffdef
"prod" and "sum" replace "*" and "+" respectively
haftmann
parents:
36049
diff
changeset
|
238 |
fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod}, |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
239 |
[Type (@{type_name Predicate.pred}, [T]), @{typ Random.seed}])])) = 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 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
242 |
fun mk_empty T = Const(@{const_name Random_Pred.empty}, 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 |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
248 |
Const (@{const_name Random_Pred.single}, 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 |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
255 |
Const (@{const_name Random_Pred.bind}, 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 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
258 |
val mk_plus = HOLogic.mk_binop @{const_name Random_Pred.union} |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
259 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
260 |
fun mk_if cond = Const (@{const_name Random_Pred.if_randompred}, |
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) = |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
264 |
list_comb (Const (@{const_name Random_Pred.iterate_upto}, |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
265 |
[@{typ natural} --> T, @{typ natural}, @{typ natural}] ---> 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 |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
271 |
in Const (@{const_name Random_Pred.not_randompred}, T --> T) $ t end |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
272 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
273 |
fun mk_map T1 T2 tf tp = Const (@{const_name Random_Pred.map}, |
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 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
288 |
fun mk_dseqT T = Type ("fun", [@{typ natural}, Type ("fun", [@{typ bool}, |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
289 |
Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])]) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
290 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
291 |
fun dest_dseqT (Type ("fun", [@{typ natural}, Type ("fun", [@{typ bool}, |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
292 |
Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
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 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
295 |
fun mk_empty T = Const (@{const_name Limited_Sequence.empty}, 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 |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
299 |
in Const(@{const_name Limited_Sequence.single}, 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 |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
304 |
Const (@{const_name Limited_Sequence.bind}, 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 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
307 |
val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.union}; |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
308 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
309 |
fun mk_if cond = Const (@{const_name Limited_Sequence.if_seq}, |
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 |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
315 |
in Const (@{const_name Limited_Sequence.not_seq}, T --> T) $ t end |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
316 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
317 |
fun mk_map T1 T2 tf tp = Const (@{const_name Limited_Sequence.map}, |
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 = |
55437 | 333 |
@{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [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 |
336 |
(Type ("fun", [@{typ natural}, Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T |
|
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 |
|
55437 | 339 |
fun mk_empty T = Const (@{const_name Limited_Sequence.pos_empty}, 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 |
55437 | 344 |
in Const(@{const_name Limited_Sequence.pos_single}, 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 |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
350 |
Const (@{const_name Limited_Sequence.pos_bind}, 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 |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
357 |
Const (@{const_name Limited_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f |
55437 | 358 |
end |
359 |
||
360 |
val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.pos_union} |
|
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 = |
363 |
Const (@{const_name Limited_Sequence.pos_if_seq}, |
|
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 = |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
372 |
@{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, |
40051
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
373 |
[Type (@{type_name Option.option}, [@{typ unit}])]) |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
374 |
in Const (@{const_name Limited_Sequence.pos_not_seq}, 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 = |
377 |
Const (@{const_name Limited_Sequence.pos_map}, |
|
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 |
|
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
398 |
fun mk_neg_dseqT T = @{typ natural} --> |
40051
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
399 |
Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])]) |
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
400 |
|
55437 | 401 |
fun dest_neg_dseqT |
402 |
(Type ("fun", [@{typ natural}, |
|
403 |
Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) = |
|
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 |
|
55437 | 407 |
fun mk_empty T = Const (@{const_name Limited_Sequence.neg_empty}, 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 |
55437 | 412 |
in Const(@{const_name Limited_Sequence.neg_single}, 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 |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
418 |
Const (@{const_name Limited_Sequence.neg_bind}, 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 |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
425 |
Const (@{const_name Limited_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f |
55437 | 426 |
end |
427 |
||
428 |
val mk_plus = HOLogic.mk_binop @{const_name Limited_Sequence.neg_union} |
|
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 = |
431 |
Const (@{const_name Limited_Sequence.neg_if_seq}, |
|
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 = |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
440 |
@{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, |
40051
b6acda4d1c29
added generator_dseq compilation for a sound depth-limited compilation with small value generators
bulwahn
parents:
40049
diff
changeset
|
441 |
[@{typ unit}]) |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
442 |
in Const (@{const_name Limited_Sequence.neg_not_seq}, 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 = |
445 |
Const (@{const_name Limited_Sequence.neg_map}, |
|
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 = |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
467 |
@{typ natural} --> @{typ natural} --> @{typ Random.seed} --> |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
468 |
@{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [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 |
471 |
(Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural}, |
|
472 |
Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ natural}, |
|
473 |
Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T |
|
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 |
|
55437 | 476 |
fun mk_empty T = Const (@{const_name Random_Sequence.pos_empty}, 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 |
55437 | 481 |
in Const(@{const_name Random_Sequence.pos_single}, 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 |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
487 |
Const (@{const_name Random_Sequence.pos_bind}, 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 |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
494 |
Const (@{const_name Random_Sequence.pos_decr_bind}, 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 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
497 |
val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.pos_union}; |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
498 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
499 |
fun mk_if cond = Const (@{const_name Random_Sequence.pos_if_random_dseq}, |
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) = |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
503 |
list_comb (Const (@{const_name Random_Sequence.pos_iterate_upto}, |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
504 |
[@{typ natural} --> T, @{typ natural}, @{typ natural}] |
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 |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
511 |
val nT = @{typ natural} --> @{typ natural} --> @{typ Random.seed} --> |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
512 |
@{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
513 |
[Type (@{type_name Option.option}, [@{typ unit}])]) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
514 |
|
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
515 |
in Const (@{const_name Random_Sequence.pos_not_random_dseq}, 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 = |
518 |
Const (@{const_name Random_Sequence.pos_map}, |
|
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 = |
55437 | 540 |
@{typ natural} --> @{typ natural} --> @{typ Random.seed} --> |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
541 |
@{typ natural} --> |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
542 |
Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])]) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
543 |
|
55437 | 544 |
fun dest_neg_random_dseqT |
545 |
(Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural}, |
|
546 |
Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ natural}, |
|
547 |
Type (@{type_name Lazy_Sequence.lazy_sequence}, |
|
548 |
[Type (@{type_name Option.option}, [T])])])])])])) = T |
|
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 |
|
55437 | 551 |
fun mk_empty T = Const (@{const_name Random_Sequence.neg_empty}, 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 |
55437 | 556 |
in Const(@{const_name Random_Sequence.neg_single}, 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 |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
562 |
Const (@{const_name Random_Sequence.neg_bind}, 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 |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
569 |
Const (@{const_name Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f |
55437 | 570 |
end |
571 |
||
572 |
val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.neg_union} |
|
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 = |
575 |
Const (@{const_name Random_Sequence.neg_if_random_dseq}, |
|
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) = |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
579 |
list_comb (Const (@{const_name Random_Sequence.neg_iterate_upto}, |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
580 |
[@{typ natural} --> T, @{typ natural}, @{typ natural}] |
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 |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
587 |
val pT = @{typ natural} --> @{typ natural} --> @{typ Random.seed} --> |
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
588 |
@{typ natural} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}]) |
51126
df86080de4cb
reform of predicate compiler / quickcheck theories:
haftmann
parents:
50056
diff
changeset
|
589 |
in Const (@{const_name Random_Sequence.neg_not_random_dseq}, 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 = |
592 |
Const (@{const_name Random_Sequence.neg_map}, |
|
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 = |
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
51126
diff
changeset
|
614 |
@{typ natural} --> @{typ natural} --> @{typ Random.seed} --> |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
615 |
HOLogic.mk_prodT (DSequence_CompFuns.mk_dseqT T, @{typ Random.seed}) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
616 |
|
55437 | 617 |
fun dest_random_dseqT |
618 |
(Type ("fun", [@{typ natural}, Type ("fun", [@{typ natural}, |
|
619 |
Type ("fun", [@{typ Random.seed}, |
|
620 |
Type (@{type_name Product_Type.prod}, [T, @{typ Random.seed}])])])])) = |
|
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 |
|
55437 | 624 |
fun mk_empty T = Const (@{const_name Random_Sequence.empty}, 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 |
55437 | 629 |
in Const(@{const_name Random_Sequence.single}, 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 |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
635 |
Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f |
55437 | 636 |
end |
637 |
||
638 |
val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.union} |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
639 |
|
55437 | 640 |
fun mk_if cond = |
641 |
Const (@{const_name Random_Sequence.if_random_dseq}, |
|
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 |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
649 |
in Const (@{const_name Random_Sequence.not_random_dseq}, T --> T) $ t end |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
650 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
651 |
fun mk_map T1 T2 tf tp = Const (@{const_name Random_Sequence.map}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
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 |