author | bulwahn |
Wed, 31 Mar 2010 16:44:41 +0200 | |
changeset 36049 | 0ce5b7a5c2fd |
parent 36046 | c3946372f556 |
child 37678 | 0040bafffdef |
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 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
4 |
Structures for different compilations of the predicate compiler |
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 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
7 |
structure PredicateCompFuns = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
8 |
struct |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
9 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
10 |
fun mk_predT T = Type (@{type_name Predicate.pred}, [T]) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
11 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
12 |
fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
13 |
| dest_predT T = raise TYPE ("dest_predT", [T], []); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
14 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
15 |
fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
16 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
17 |
fun mk_single t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
18 |
let val T = fastype_of t |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
19 |
in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
20 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
21 |
fun mk_bind (x, f) = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
22 |
let val T as Type ("fun", [_, U]) = fastype_of f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
23 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
24 |
Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
25 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
26 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
27 |
val mk_sup = HOLogic.mk_binop @{const_name sup}; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
28 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
29 |
fun mk_if cond = Const (@{const_name Predicate.if_pred}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
30 |
HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
31 |
|
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
32 |
fun mk_iterate_upto T (f, from, to) = |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
33 |
list_comb (Const (@{const_name Code_Numeral.iterate_upto}, |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
34 |
[@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_predT T), |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
35 |
[f, from, to]) |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
36 |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
37 |
fun mk_not t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
38 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
39 |
val T = mk_predT HOLogic.unitT |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
40 |
in Const (@{const_name Predicate.not_pred}, T --> T) $ t end |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
41 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
42 |
fun mk_Enum f = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
43 |
let val T as Type ("fun", [T', _]) = fastype_of f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
44 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
45 |
Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
46 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
47 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
48 |
fun mk_Eval (f, x) = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
49 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
50 |
val T = fastype_of x |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
51 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
52 |
Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
53 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
54 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
55 |
fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
56 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
57 |
fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
58 |
(T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
59 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
60 |
val compfuns = Predicate_Compile_Aux.CompilationFuns |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
61 |
{mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot, |
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
62 |
mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
63 |
mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}; |
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
64 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
65 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
66 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
67 |
structure RandomPredCompFuns = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
68 |
struct |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
69 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
70 |
fun mk_randompredT T = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
71 |
@{typ Random.seed} --> HOLogic.mk_prodT (PredicateCompFuns.mk_predT T, @{typ Random.seed}) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
72 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
73 |
fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name "*"}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
74 |
[Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
75 |
| dest_randompredT T = raise TYPE ("dest_randompredT", [T], []); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
76 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
77 |
fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
78 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
79 |
fun mk_single t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
80 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
81 |
val T = fastype_of t |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
82 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
83 |
Const (@{const_name Quickcheck.single}, T --> mk_randompredT T) $ t |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
84 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
85 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
86 |
fun mk_bind (x, f) = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
87 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
88 |
val T as (Type ("fun", [_, U])) = fastype_of f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
89 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
90 |
Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
91 |
end |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
92 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
93 |
val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union} |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
94 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
95 |
fun mk_if cond = Const (@{const_name Quickcheck.if_randompred}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
96 |
HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
97 |
|
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
|
98 |
fun mk_iterate_upto T (f, from, to) = |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
99 |
list_comb (Const (@{const_name Quickcheck.iterate_upto}, |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
100 |
[@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_randompredT T), |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
101 |
[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
|
102 |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
103 |
fun mk_not t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
104 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
105 |
val T = mk_randompredT HOLogic.unitT |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
106 |
in Const (@{const_name Quickcheck.not_randompred}, T --> T) $ t end |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
107 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
108 |
fun mk_map T1 T2 tf tp = Const (@{const_name Quickcheck.map}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
109 |
(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
|
110 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
111 |
val compfuns = Predicate_Compile_Aux.CompilationFuns |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
112 |
{mk_predT = mk_randompredT, dest_predT = dest_randompredT, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
113 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
114 |
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
|
115 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
116 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
117 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
118 |
structure DSequence_CompFuns = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
119 |
struct |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
120 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
121 |
fun mk_dseqT T = Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
122 |
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
|
123 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
124 |
fun dest_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ bool}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
125 |
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
|
126 |
| dest_dseqT T = raise TYPE ("dest_dseqT", [T], []); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
127 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
128 |
fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
129 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
130 |
fun mk_single t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
131 |
let val T = fastype_of t |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
132 |
in Const(@{const_name DSequence.single}, T --> mk_dseqT T) $ t end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
133 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
134 |
fun mk_bind (x, f) = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
135 |
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
|
136 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
137 |
Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
138 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
139 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
140 |
val mk_sup = HOLogic.mk_binop @{const_name DSequence.union}; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
141 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
142 |
fun mk_if cond = Const (@{const_name DSequence.if_seq}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
143 |
HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
144 |
|
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
|
145 |
fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation" |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
146 |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
147 |
fun mk_not t = let val T = mk_dseqT HOLogic.unitT |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
148 |
in Const (@{const_name DSequence.not_seq}, T --> T) $ t end |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
149 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
150 |
fun mk_map T1 T2 tf tp = Const (@{const_name DSequence.map}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
151 |
(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
|
152 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
153 |
val compfuns = Predicate_Compile_Aux.CompilationFuns |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
154 |
{mk_predT = mk_dseqT, dest_predT = dest_dseqT, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
155 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
156 |
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
|
157 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
158 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
159 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
160 |
structure New_Pos_Random_Sequence_CompFuns = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
161 |
struct |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
162 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
163 |
fun mk_pos_random_dseqT T = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
164 |
@{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} --> |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
165 |
@{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [T]) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
166 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
167 |
fun dest_pos_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
168 |
Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
169 |
Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
170 |
| dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
171 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
172 |
fun mk_bot T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
173 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
174 |
fun mk_single t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
175 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
176 |
val T = fastype_of t |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
177 |
in Const(@{const_name New_Random_Sequence.pos_single}, T --> mk_pos_random_dseqT T) $ t end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
178 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
179 |
fun mk_bind (x, f) = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
180 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
181 |
val T as Type ("fun", [_, U]) = fastype_of f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
182 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
183 |
Const (@{const_name New_Random_Sequence.pos_bind}, fastype_of x --> T --> U) $ x $ f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
184 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
185 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
186 |
val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union}; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
187 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
188 |
fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
189 |
HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
190 |
|
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
|
191 |
fun mk_iterate_upto T (f, from, to) = |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
192 |
list_comb (Const (@{const_name New_Random_Sequence.pos_iterate_upto}, |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
193 |
[@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
194 |
---> 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
|
195 |
[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
|
196 |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
197 |
fun mk_not t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
198 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
199 |
val pT = mk_pos_random_dseqT HOLogic.unitT |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
200 |
val nT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} --> |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
201 |
@{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
202 |
[Type (@{type_name Option.option}, [@{typ unit}])]) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
203 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
204 |
in Const (@{const_name New_Random_Sequence.pos_not_random_dseq}, nT --> pT) $ t end |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
205 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
206 |
fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.pos_map}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
207 |
(T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
208 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
209 |
val compfuns = Predicate_Compile_Aux.CompilationFuns |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
210 |
{mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
211 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
212 |
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
|
213 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
214 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
215 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
216 |
structure New_Neg_Random_Sequence_CompFuns = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
217 |
struct |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
218 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
219 |
fun mk_neg_random_dseqT T = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
220 |
@{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} --> |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
221 |
@{typ code_numeral} --> |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
222 |
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
|
223 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
224 |
fun dest_neg_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
225 |
Type ("fun", [@{typ Random.seed}, Type ("fun", [@{typ code_numeral}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
226 |
Type (@{type_name Lazy_Sequence.lazy_sequence}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
227 |
[Type (@{type_name Option.option}, [T])])])])])])) = T |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
228 |
| dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
229 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
230 |
fun mk_bot T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
231 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
232 |
fun mk_single t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
233 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
234 |
val T = fastype_of t |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
235 |
in Const(@{const_name New_Random_Sequence.neg_single}, T --> mk_neg_random_dseqT T) $ t end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
236 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
237 |
fun mk_bind (x, f) = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
238 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
239 |
val T as Type ("fun", [_, U]) = fastype_of f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
240 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
241 |
Const (@{const_name New_Random_Sequence.neg_bind}, fastype_of x --> T --> U) $ x $ f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
242 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
243 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
244 |
val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union}; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
245 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
246 |
fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
247 |
HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
248 |
|
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
249 |
fun mk_iterate_upto T (f, from, to) = |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
250 |
list_comb (Const (@{const_name New_Random_Sequence.neg_iterate_upto}, |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
251 |
[@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
252 |
---> 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
|
253 |
[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
|
254 |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
255 |
fun mk_not t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
256 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
257 |
val nT = mk_neg_random_dseqT HOLogic.unitT |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
258 |
val pT = @{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} --> |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
259 |
@{typ code_numeral} --> Type (@{type_name Lazy_Sequence.lazy_sequence}, [@{typ unit}]) |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
260 |
in Const (@{const_name New_Random_Sequence.neg_not_random_dseq}, pT --> nT) $ t end |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
261 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
262 |
fun mk_map T1 T2 tf tp = Const (@{const_name New_Random_Sequence.neg_map}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
263 |
(T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
264 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
265 |
val compfuns = Predicate_Compile_Aux.CompilationFuns |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
266 |
{mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
267 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
268 |
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
|
269 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
270 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
271 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
272 |
structure Random_Sequence_CompFuns = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
273 |
struct |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
274 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
275 |
fun mk_random_dseqT T = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
276 |
@{typ code_numeral} --> @{typ code_numeral} --> @{typ Random.seed} --> |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
277 |
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
|
278 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
279 |
fun dest_random_dseqT (Type ("fun", [@{typ code_numeral}, Type ("fun", [@{typ code_numeral}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
280 |
Type ("fun", [@{typ Random.seed}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
281 |
Type (@{type_name "*"}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
282 |
| dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
283 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
284 |
fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T); |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
285 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
286 |
fun mk_single t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
287 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
288 |
val T = fastype_of t |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
289 |
in Const(@{const_name Random_Sequence.single}, T --> mk_random_dseqT T) $ t end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
290 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
291 |
fun mk_bind (x, f) = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
292 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
293 |
val T as Type ("fun", [_, U]) = fastype_of f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
294 |
in |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
295 |
Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
296 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
297 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
298 |
val mk_sup = HOLogic.mk_binop @{const_name Random_Sequence.union}; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
299 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
300 |
fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq}, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
301 |
HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
302 |
|
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
|
303 |
fun mk_iterate_upto T (f, from, to) = raise Fail "No iterate_upto compilation" |
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
304 |
|
36046
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
305 |
fun mk_not t = |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
306 |
let |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
307 |
val T = mk_random_dseqT HOLogic.unitT |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
308 |
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
|
309 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
310 |
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
|
311 |
(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
|
312 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
313 |
val compfuns = Predicate_Compile_Aux.CompilationFuns |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
314 |
{mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT, |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
315 |
mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if, |
36049
0ce5b7a5c2fd
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
bulwahn
parents:
36046
diff
changeset
|
316 |
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
|
317 |
|
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
318 |
end; |
c3946372f556
putting compilation setup of predicate compiler in a separate file
bulwahn
parents:
diff
changeset
|
319 |