huffman@35461
|
1 |
(* Title: HOLCF/Tools/holcf_library.ML
|
huffman@35461
|
2 |
Author: Brian Huffman
|
huffman@35461
|
3 |
|
huffman@35461
|
4 |
Functions for constructing HOLCF types and terms.
|
huffman@35461
|
5 |
*)
|
huffman@35461
|
6 |
|
huffman@35461
|
7 |
structure HOLCF_Library =
|
huffman@35461
|
8 |
struct
|
huffman@35461
|
9 |
|
huffman@35462
|
10 |
infixr 6 ->>;
|
huffman@40458
|
11 |
infixr -->>;
|
huffman@35555
|
12 |
infix 9 `;
|
huffman@35462
|
13 |
|
huffman@35461
|
14 |
(*** Operations from Isabelle/HOL ***)
|
huffman@35461
|
15 |
|
huffman@35461
|
16 |
val boolT = HOLogic.boolT;
|
huffman@35475
|
17 |
val natT = HOLogic.natT;
|
huffman@35461
|
18 |
|
huffman@35461
|
19 |
val mk_equals = Logic.mk_equals;
|
huffman@35461
|
20 |
val mk_eq = HOLogic.mk_eq;
|
huffman@35461
|
21 |
val mk_trp = HOLogic.mk_Trueprop;
|
huffman@35461
|
22 |
val mk_fst = HOLogic.mk_fst;
|
huffman@35461
|
23 |
val mk_snd = HOLogic.mk_snd;
|
huffman@35461
|
24 |
val mk_not = HOLogic.mk_not;
|
huffman@35461
|
25 |
val mk_conj = HOLogic.mk_conj;
|
huffman@35461
|
26 |
val mk_disj = HOLogic.mk_disj;
|
huffman@40205
|
27 |
val mk_imp = HOLogic.mk_imp;
|
huffman@35461
|
28 |
|
huffman@35461
|
29 |
fun mk_ex (x, t) = HOLogic.exists_const (fastype_of x) $ Term.lambda x t;
|
huffman@40205
|
30 |
fun mk_all (x, t) = HOLogic.all_const (fastype_of x) $ Term.lambda x t;
|
huffman@35461
|
31 |
|
huffman@35461
|
32 |
|
huffman@35461
|
33 |
(*** Basic HOLCF concepts ***)
|
huffman@35461
|
34 |
|
huffman@35461
|
35 |
fun mk_bottom T = Const (@{const_name UU}, T);
|
huffman@35461
|
36 |
|
huffman@35461
|
37 |
fun below_const T = Const (@{const_name below}, [T, T] ---> boolT);
|
huffman@35461
|
38 |
fun mk_below (t, u) = below_const (fastype_of t) $ t $ u;
|
huffman@35461
|
39 |
|
huffman@35461
|
40 |
fun mk_undef t = mk_eq (t, mk_bottom (fastype_of t));
|
huffman@35461
|
41 |
|
huffman@35461
|
42 |
fun mk_defined t = mk_not (mk_undef t);
|
huffman@35461
|
43 |
|
huffman@40202
|
44 |
fun mk_adm t =
|
huffman@40202
|
45 |
Const (@{const_name adm}, fastype_of t --> boolT) $ t;
|
huffman@40202
|
46 |
|
huffman@35461
|
47 |
fun mk_compact t =
|
huffman@35461
|
48 |
Const (@{const_name compact}, fastype_of t --> boolT) $ t;
|
huffman@35461
|
49 |
|
huffman@35461
|
50 |
fun mk_cont t =
|
huffman@35461
|
51 |
Const (@{const_name cont}, fastype_of t --> boolT) $ t;
|
huffman@35461
|
52 |
|
huffman@35475
|
53 |
fun mk_chain t =
|
huffman@35475
|
54 |
Const (@{const_name chain}, Term.fastype_of t --> boolT) $ t;
|
huffman@35475
|
55 |
|
huffman@35555
|
56 |
fun mk_lub t =
|
huffman@35555
|
57 |
let
|
huffman@35555
|
58 |
val T = Term.range_type (Term.fastype_of t);
|
huffman@35555
|
59 |
val lub_const = Const (@{const_name lub}, (T --> boolT) --> T);
|
huffman@35555
|
60 |
val UNIV_const = @{term "UNIV :: nat set"};
|
huffman@35555
|
61 |
val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT;
|
huffman@35555
|
62 |
val image_const = Const (@{const_name image}, image_type);
|
huffman@35555
|
63 |
in
|
huffman@35555
|
64 |
lub_const $ (image_const $ t $ UNIV_const)
|
huffman@35555
|
65 |
end;
|
huffman@35555
|
66 |
|
huffman@35461
|
67 |
|
huffman@35461
|
68 |
(*** Continuous function space ***)
|
huffman@35461
|
69 |
|
huffman@35511
|
70 |
fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
|
huffman@35461
|
71 |
|
huffman@35462
|
72 |
val (op ->>) = mk_cfunT;
|
huffman@35462
|
73 |
val (op -->>) = Library.foldr mk_cfunT;
|
huffman@35461
|
74 |
|
huffman@35511
|
75 |
fun dest_cfunT (Type(@{type_name cfun}, [T, U])) = (T, U)
|
huffman@35461
|
76 |
| dest_cfunT T = raise TYPE ("dest_cfunT", [T], []);
|
huffman@35461
|
77 |
|
huffman@35461
|
78 |
fun capply_const (S, T) =
|
huffman@40565
|
79 |
Const(@{const_name Rep_cfun}, (S ->> T) --> (S --> T));
|
huffman@35461
|
80 |
|
huffman@35461
|
81 |
fun cabs_const (S, T) =
|
huffman@40565
|
82 |
Const(@{const_name Abs_cfun}, (S --> T) --> (S ->> T));
|
huffman@35461
|
83 |
|
huffman@35461
|
84 |
fun mk_cabs t =
|
huffman@35461
|
85 |
let val T = fastype_of t
|
huffman@35461
|
86 |
in cabs_const (Term.domain_type T, Term.range_type T) $ t end
|
huffman@35461
|
87 |
|
huffman@35461
|
88 |
(* builds the expression (% v1 v2 .. vn. rhs) *)
|
huffman@35461
|
89 |
fun lambdas [] rhs = rhs
|
huffman@35461
|
90 |
| lambdas (v::vs) rhs = Term.lambda v (lambdas vs rhs);
|
huffman@35461
|
91 |
|
huffman@35461
|
92 |
(* builds the expression (LAM v. rhs) *)
|
huffman@35461
|
93 |
fun big_lambda v rhs =
|
huffman@35461
|
94 |
cabs_const (fastype_of v, fastype_of rhs) $ Term.lambda v rhs;
|
huffman@35461
|
95 |
|
huffman@35461
|
96 |
(* builds the expression (LAM v1 v2 .. vn. rhs) *)
|
huffman@35461
|
97 |
fun big_lambdas [] rhs = rhs
|
huffman@35461
|
98 |
| big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs);
|
huffman@35461
|
99 |
|
huffman@35461
|
100 |
fun mk_capply (t, u) =
|
huffman@35461
|
101 |
let val (S, T) =
|
huffman@35461
|
102 |
case fastype_of t of
|
huffman@35511
|
103 |
Type(@{type_name cfun}, [S, T]) => (S, T)
|
huffman@35461
|
104 |
| _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]);
|
huffman@35461
|
105 |
in capply_const (S, T) $ t $ u end;
|
huffman@35461
|
106 |
|
huffman@35555
|
107 |
val (op `) = mk_capply;
|
huffman@35461
|
108 |
|
huffman@35461
|
109 |
val list_ccomb : term * term list -> term = Library.foldl mk_capply;
|
huffman@35461
|
110 |
|
huffman@35461
|
111 |
fun mk_ID T = Const (@{const_name ID}, T ->> T);
|
huffman@35461
|
112 |
|
huffman@35461
|
113 |
fun cfcomp_const (T, U, V) =
|
huffman@35461
|
114 |
Const (@{const_name cfcomp}, (U ->> V) ->> (T ->> U) ->> (T ->> V));
|
huffman@35461
|
115 |
|
huffman@35461
|
116 |
fun mk_cfcomp (f, g) =
|
huffman@35461
|
117 |
let
|
huffman@35461
|
118 |
val (U, V) = dest_cfunT (fastype_of f);
|
huffman@35461
|
119 |
val (T, U') = dest_cfunT (fastype_of g);
|
huffman@35461
|
120 |
in
|
huffman@35461
|
121 |
if U = U'
|
huffman@35461
|
122 |
then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g)
|
huffman@35461
|
123 |
else raise TYPE ("mk_cfcomp", [U, U'], [f, g])
|
huffman@35461
|
124 |
end;
|
huffman@35461
|
125 |
|
huffman@35785
|
126 |
fun strictify_const T = Const (@{const_name strictify}, T ->> T);
|
huffman@35785
|
127 |
fun mk_strictify t = strictify_const (fastype_of t) ` t;
|
huffman@35785
|
128 |
|
huffman@35461
|
129 |
fun mk_strict t =
|
huffman@35461
|
130 |
let val (T, U) = dest_cfunT (fastype_of t);
|
huffman@35461
|
131 |
in mk_eq (t ` mk_bottom T, mk_bottom U) end;
|
huffman@35461
|
132 |
|
huffman@35461
|
133 |
|
huffman@35461
|
134 |
(*** Product type ***)
|
huffman@35461
|
135 |
|
huffman@35461
|
136 |
val mk_prodT = HOLogic.mk_prodT
|
huffman@35461
|
137 |
|
huffman@35461
|
138 |
fun mk_tupleT [] = HOLogic.unitT
|
huffman@35461
|
139 |
| mk_tupleT [T] = T
|
huffman@35461
|
140 |
| mk_tupleT (T :: Ts) = mk_prodT (T, mk_tupleT Ts);
|
huffman@35461
|
141 |
|
huffman@35461
|
142 |
(* builds the expression (v1,v2,..,vn) *)
|
huffman@35461
|
143 |
fun mk_tuple [] = HOLogic.unit
|
huffman@35461
|
144 |
| mk_tuple (t::[]) = t
|
huffman@35461
|
145 |
| mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts);
|
huffman@35461
|
146 |
|
huffman@35461
|
147 |
(* builds the expression (%(v1,v2,..,vn). rhs) *)
|
huffman@35461
|
148 |
fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs
|
huffman@35461
|
149 |
| lambda_tuple (v::[]) rhs = Term.lambda v rhs
|
huffman@35461
|
150 |
| lambda_tuple (v::vs) rhs =
|
huffman@35461
|
151 |
HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs));
|
huffman@35461
|
152 |
|
huffman@35461
|
153 |
|
huffman@35461
|
154 |
(*** Lifted cpo type ***)
|
huffman@35461
|
155 |
|
huffman@35461
|
156 |
fun mk_upT T = Type(@{type_name "u"}, [T]);
|
huffman@35461
|
157 |
|
huffman@35461
|
158 |
fun dest_upT (Type(@{type_name "u"}, [T])) = T
|
huffman@35461
|
159 |
| dest_upT T = raise TYPE ("dest_upT", [T], []);
|
huffman@35461
|
160 |
|
huffman@35461
|
161 |
fun up_const T = Const(@{const_name up}, T ->> mk_upT T);
|
huffman@35461
|
162 |
|
huffman@35461
|
163 |
fun mk_up t = up_const (fastype_of t) ` t;
|
huffman@35461
|
164 |
|
huffman@35461
|
165 |
fun fup_const (T, U) =
|
huffman@35461
|
166 |
Const(@{const_name fup}, (T ->> U) ->> mk_upT T ->> U);
|
huffman@35461
|
167 |
|
huffman@35785
|
168 |
fun mk_fup t = fup_const (dest_cfunT (fastype_of t)) ` t;
|
huffman@35785
|
169 |
|
huffman@35461
|
170 |
fun from_up T = fup_const (T, T) ` mk_ID T;
|
huffman@35461
|
171 |
|
huffman@35461
|
172 |
|
huffman@35785
|
173 |
(*** Lifted unit type ***)
|
huffman@35461
|
174 |
|
huffman@35461
|
175 |
val oneT = @{typ "one"};
|
huffman@35461
|
176 |
|
huffman@40453
|
177 |
fun one_case_const T = Const (@{const_name one_case}, T ->> oneT ->> T);
|
huffman@40453
|
178 |
fun mk_one_case t = one_case_const (fastype_of t) ` t;
|
huffman@35785
|
179 |
|
huffman@35785
|
180 |
|
huffman@35785
|
181 |
(*** Strict product type ***)
|
huffman@35785
|
182 |
|
huffman@35511
|
183 |
fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);
|
huffman@35461
|
184 |
|
huffman@35511
|
185 |
fun dest_sprodT (Type(@{type_name sprod}, [T, U])) = (T, U)
|
huffman@35461
|
186 |
| dest_sprodT T = raise TYPE ("dest_sprodT", [T], []);
|
huffman@35461
|
187 |
|
huffman@35461
|
188 |
fun spair_const (T, U) =
|
huffman@35461
|
189 |
Const(@{const_name spair}, T ->> U ->> mk_sprodT (T, U));
|
huffman@35461
|
190 |
|
huffman@35461
|
191 |
(* builds the expression (:t, u:) *)
|
huffman@35461
|
192 |
fun mk_spair (t, u) =
|
huffman@35461
|
193 |
spair_const (fastype_of t, fastype_of u) ` t ` u;
|
huffman@35461
|
194 |
|
huffman@35461
|
195 |
(* builds the expression (:t1,t2,..,tn:) *)
|
huffman@35461
|
196 |
fun mk_stuple [] = @{term "ONE"}
|
huffman@35461
|
197 |
| mk_stuple (t::[]) = t
|
huffman@35461
|
198 |
| mk_stuple (t::ts) = mk_spair (t, mk_stuple ts);
|
huffman@35461
|
199 |
|
huffman@35461
|
200 |
fun sfst_const (T, U) =
|
huffman@35461
|
201 |
Const(@{const_name sfst}, mk_sprodT (T, U) ->> T);
|
huffman@35461
|
202 |
|
huffman@35461
|
203 |
fun ssnd_const (T, U) =
|
huffman@35461
|
204 |
Const(@{const_name ssnd}, mk_sprodT (T, U) ->> U);
|
huffman@35461
|
205 |
|
huffman@35785
|
206 |
fun ssplit_const (T, U, V) =
|
huffman@35785
|
207 |
Const (@{const_name ssplit}, (T ->> U ->> V) ->> mk_sprodT (T, U) ->> V);
|
huffman@35785
|
208 |
|
huffman@35785
|
209 |
fun mk_ssplit t =
|
huffman@35785
|
210 |
let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t));
|
huffman@35785
|
211 |
in ssplit_const (T, U, V) ` t end;
|
huffman@35785
|
212 |
|
huffman@35461
|
213 |
|
huffman@35461
|
214 |
(*** Strict sum type ***)
|
huffman@35461
|
215 |
|
huffman@35511
|
216 |
fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]);
|
huffman@35461
|
217 |
|
huffman@35511
|
218 |
fun dest_ssumT (Type(@{type_name ssum}, [T, U])) = (T, U)
|
huffman@35461
|
219 |
| dest_ssumT T = raise TYPE ("dest_ssumT", [T], []);
|
huffman@35461
|
220 |
|
huffman@35461
|
221 |
fun sinl_const (T, U) = Const(@{const_name sinl}, T ->> mk_ssumT (T, U));
|
huffman@35461
|
222 |
fun sinr_const (T, U) = Const(@{const_name sinr}, U ->> mk_ssumT (T, U));
|
huffman@35461
|
223 |
|
huffman@35461
|
224 |
(* builds the list [sinl(t1), sinl(sinr(t2)), ... sinr(...sinr(tn))] *)
|
huffman@35461
|
225 |
fun mk_sinjects ts =
|
huffman@35461
|
226 |
let
|
huffman@35461
|
227 |
val Ts = map fastype_of ts;
|
huffman@35461
|
228 |
fun combine (t, T) (us, U) =
|
huffman@35461
|
229 |
let
|
huffman@35461
|
230 |
val v = sinl_const (T, U) ` t;
|
huffman@35461
|
231 |
val vs = map (fn u => sinr_const (T, U) ` u) us;
|
huffman@35461
|
232 |
in
|
huffman@35461
|
233 |
(v::vs, mk_ssumT (T, U))
|
huffman@35461
|
234 |
end
|
huffman@35912
|
235 |
fun inj [] = raise Fail "mk_sinjects: empty list"
|
huffman@35461
|
236 |
| inj ((t, T)::[]) = ([t], T)
|
huffman@35461
|
237 |
| inj ((t, T)::ts) = combine (t, T) (inj ts);
|
huffman@35461
|
238 |
in
|
huffman@35461
|
239 |
fst (inj (ts ~~ Ts))
|
huffman@35461
|
240 |
end;
|
huffman@35461
|
241 |
|
huffman@35461
|
242 |
fun sscase_const (T, U, V) =
|
huffman@35461
|
243 |
Const(@{const_name sscase},
|
huffman@35461
|
244 |
(T ->> V) ->> (U ->> V) ->> mk_ssumT (T, U) ->> V);
|
huffman@35461
|
245 |
|
huffman@35785
|
246 |
fun mk_sscase (t, u) =
|
huffman@35785
|
247 |
let val (T, V) = dest_cfunT (fastype_of t);
|
huffman@35785
|
248 |
val (U, V) = dest_cfunT (fastype_of u);
|
huffman@35785
|
249 |
in sscase_const (T, U, V) ` t ` u end;
|
huffman@35785
|
250 |
|
huffman@35461
|
251 |
fun from_sinl (T, U) =
|
huffman@35461
|
252 |
sscase_const (T, U, T) ` mk_ID T ` mk_bottom (U ->> T);
|
huffman@35461
|
253 |
|
huffman@35461
|
254 |
fun from_sinr (T, U) =
|
huffman@35461
|
255 |
sscase_const (T, U, U) ` mk_bottom (T ->> U) ` mk_ID U;
|
huffman@35461
|
256 |
|
huffman@35461
|
257 |
|
huffman@35461
|
258 |
(*** pattern match monad type ***)
|
huffman@35461
|
259 |
|
huffman@37092
|
260 |
fun mk_matchT T = Type (@{type_name "match"}, [T]);
|
huffman@35461
|
261 |
|
huffman@37092
|
262 |
fun dest_matchT (Type(@{type_name "match"}, [T])) = T
|
huffman@35461
|
263 |
| dest_matchT T = raise TYPE ("dest_matchT", [T], []);
|
huffman@35461
|
264 |
|
huffman@35461
|
265 |
fun mk_fail T = Const (@{const_name "Fixrec.fail"}, mk_matchT T);
|
huffman@35461
|
266 |
|
huffman@37092
|
267 |
fun succeed_const T = Const (@{const_name "Fixrec.succeed"}, T ->> mk_matchT T);
|
huffman@37092
|
268 |
fun mk_succeed t = succeed_const (fastype_of t) ` t;
|
huffman@35461
|
269 |
|
huffman@35461
|
270 |
|
huffman@35461
|
271 |
(*** lifted boolean type ***)
|
huffman@35461
|
272 |
|
huffman@35461
|
273 |
val trT = @{typ "tr"};
|
huffman@35461
|
274 |
|
huffman@35461
|
275 |
|
huffman@35461
|
276 |
(*** theory of fixed points ***)
|
huffman@35461
|
277 |
|
huffman@35461
|
278 |
fun mk_fix t =
|
huffman@35461
|
279 |
let val (T, _) = dest_cfunT (fastype_of t)
|
huffman@35461
|
280 |
in mk_capply (Const(@{const_name fix}, (T ->> T) ->> T), t) end;
|
huffman@35461
|
281 |
|
huffman@35475
|
282 |
fun iterate_const T =
|
huffman@35475
|
283 |
Const (@{const_name iterate}, natT --> (T ->> T) ->> (T ->> T));
|
huffman@35475
|
284 |
|
huffman@35475
|
285 |
fun mk_iterate (n, f) =
|
huffman@35475
|
286 |
let val (T, _) = dest_cfunT (Term.fastype_of f);
|
huffman@35475
|
287 |
in (iterate_const T $ n) ` f ` mk_bottom T end;
|
huffman@35461
|
288 |
|
huffman@35461
|
289 |
end;
|