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