|
1 (* Title: HOLCF/Tools/domain/domain_constructors.ML |
|
2 Author: Brian Huffman |
|
3 |
|
4 Defines constructor functions for a given domain isomorphism |
|
5 and proves related theorems. |
|
6 *) |
|
7 |
|
8 signature DOMAIN_CONSTRUCTORS = |
|
9 sig |
|
10 val add_domain_constructors : |
|
11 string |
|
12 -> typ * (binding * (bool * binding option * typ) list * mixfix) list |
|
13 -> term * term |
|
14 -> thm * thm |
|
15 -> theory |
|
16 -> { con_consts : term list, |
|
17 con_defs : thm list } |
|
18 * theory; |
|
19 end; |
|
20 |
|
21 |
|
22 structure Domain_Constructors :> DOMAIN_CONSTRUCTORS = |
|
23 struct |
|
24 |
|
25 (******************************************************************************) |
|
26 (************************** building types and terms **************************) |
|
27 (******************************************************************************) |
|
28 |
|
29 |
|
30 (*** Continuous function space ***) |
|
31 |
|
32 (* ->> is taken from holcf_logic.ML *) |
|
33 fun mk_cfunT (T, U) = Type(@{type_name "->"}, [T, U]); |
|
34 |
|
35 infixr 6 ->>; val (op ->>) = mk_cfunT; |
|
36 |
|
37 fun dest_cfunT (Type(@{type_name "->"}, [T, U])) = (T, U) |
|
38 | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []); |
|
39 |
|
40 fun capply_const (S, T) = |
|
41 Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T)); |
|
42 |
|
43 fun cabs_const (S, T) = |
|
44 Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T)); |
|
45 |
|
46 fun mk_cabs t = |
|
47 let val T = Term.fastype_of t |
|
48 in cabs_const (Term.domain_type T, Term.range_type T) $ t end |
|
49 |
|
50 (* builds the expression (LAM v. rhs) *) |
|
51 fun big_lambda v rhs = |
|
52 cabs_const (Term.fastype_of v, Term.fastype_of rhs) $ Term.lambda v rhs; |
|
53 |
|
54 (* builds the expression (LAM v1 v2 .. vn. rhs) *) |
|
55 fun big_lambdas [] rhs = rhs |
|
56 | big_lambdas (v::vs) rhs = big_lambda v (big_lambdas vs rhs); |
|
57 |
|
58 fun mk_capply (t, u) = |
|
59 let val (S, T) = |
|
60 case Term.fastype_of t of |
|
61 Type(@{type_name "->"}, [S, T]) => (S, T) |
|
62 | _ => raise TERM ("mk_capply " ^ ML_Syntax.print_list ML_Syntax.print_term [t, u], [t, u]); |
|
63 in capply_const (S, T) $ t $ u end; |
|
64 |
|
65 infix 9 ` ; val (op `) = mk_capply; |
|
66 |
|
67 |
|
68 (*** Product type ***) |
|
69 |
|
70 fun mk_tupleT [] = HOLogic.unitT |
|
71 | mk_tupleT [T] = T |
|
72 | mk_tupleT (T :: Ts) = HOLogic.mk_prodT (T, mk_tupleT Ts); |
|
73 |
|
74 (* builds the expression (v1,v2,..,vn) *) |
|
75 fun mk_tuple [] = HOLogic.unit |
|
76 | mk_tuple (t::[]) = t |
|
77 | mk_tuple (t::ts) = HOLogic.mk_prod (t, mk_tuple ts); |
|
78 |
|
79 (* builds the expression (%(v1,v2,..,vn). rhs) *) |
|
80 fun lambda_tuple [] rhs = Term.lambda (Free("unit", HOLogic.unitT)) rhs |
|
81 | lambda_tuple (v::[]) rhs = Term.lambda v rhs |
|
82 | lambda_tuple (v::vs) rhs = |
|
83 HOLogic.mk_split (Term.lambda v (lambda_tuple vs rhs)); |
|
84 |
|
85 |
|
86 (*** Lifted cpo type ***) |
|
87 |
|
88 fun mk_upT T = Type(@{type_name "u"}, [T]); |
|
89 |
|
90 fun up_const T = Const(@{const_name up}, T ->> mk_upT T); |
|
91 |
|
92 fun mk_up t = up_const (Term.fastype_of t) ` t; |
|
93 |
|
94 |
|
95 (*** Strict product type ***) |
|
96 |
|
97 val oneT = @{typ "one"}; |
|
98 |
|
99 fun mk_sprodT (T, U) = Type(@{type_name "**"}, [T, U]); |
|
100 |
|
101 fun spair_const (T, U) = |
|
102 Const(@{const_name spair}, T ->> U ->> mk_sprodT (T, U)); |
|
103 |
|
104 (* builds the expression (:t, u:) *) |
|
105 fun mk_spair (t, u) = |
|
106 spair_const (Term.fastype_of t, Term.fastype_of u) ` t ` u; |
|
107 |
|
108 (* builds the expression (:t1,t2,..,tn:) *) |
|
109 fun mk_stuple [] = @{term "ONE"} |
|
110 | mk_stuple (t::[]) = t |
|
111 | mk_stuple (t::ts) = mk_spair (t, mk_stuple ts); |
|
112 |
|
113 |
|
114 (*** Strict sum type ***) |
|
115 |
|
116 fun mk_ssumT (T, U) = Type(@{type_name "++"}, [T, U]); |
|
117 |
|
118 fun dest_ssumT (Type(@{type_name "++"}, [T, U])) = (T, U) |
|
119 | dest_ssumT T = raise TYPE ("dest_ssumT", [T], []); |
|
120 |
|
121 fun sinl_const (T, U) = Const(@{const_name sinl}, T ->> mk_ssumT (T, U)); |
|
122 fun sinr_const (T, U) = Const(@{const_name sinr}, U ->> mk_ssumT (T, U)); |
|
123 |
|
124 (* builds the list [sinl(t1), sinl(sinr(t2)), ... sinr(...sinr(tn))] *) |
|
125 fun mk_sinjects ts = |
|
126 let |
|
127 val Ts = map Term.fastype_of ts; |
|
128 fun combine (t, T) (us, U) = |
|
129 let |
|
130 val v = sinl_const (T, U) ` t; |
|
131 val vs = map (fn u => sinr_const (T, U) ` u) us; |
|
132 in |
|
133 (v::vs, mk_ssumT (T, U)) |
|
134 end |
|
135 fun inj [] = error "mk_sinjects: empty list" |
|
136 | inj ((t, T)::[]) = ([t], T) |
|
137 | inj ((t, T)::ts) = combine (t, T) (inj ts); |
|
138 in |
|
139 fst (inj (ts ~~ Ts)) |
|
140 end; |
|
141 |
|
142 |
|
143 (*** miscellaneous constructions ***) |
|
144 |
|
145 val trT = @{typ "tr"}; |
|
146 |
|
147 val deflT = @{typ "udom alg_defl"}; |
|
148 |
|
149 fun mapT T = |
|
150 let |
|
151 fun argTs (Type (_, Ts)) = Ts | argTs _ = []; |
|
152 fun auto T = T ->> T; |
|
153 in |
|
154 Library.foldr mk_cfunT (map auto (argTs T), auto T) |
|
155 end; |
|
156 |
|
157 val mk_equals = Logic.mk_equals; |
|
158 val mk_eq = HOLogic.mk_eq; |
|
159 val mk_trp = HOLogic.mk_Trueprop; |
|
160 val mk_fst = HOLogic.mk_fst; |
|
161 val mk_snd = HOLogic.mk_snd; |
|
162 |
|
163 fun mk_cont t = |
|
164 let val T = Term.fastype_of t |
|
165 in Const(@{const_name cont}, T --> HOLogic.boolT) $ t end; |
|
166 |
|
167 fun mk_fix t = |
|
168 let val (T, _) = dest_cfunT (Term.fastype_of t) |
|
169 in mk_capply (Const(@{const_name fix}, (T ->> T) ->> T), t) end; |
|
170 |
|
171 fun ID_const T = Const (@{const_name ID}, T ->> T); |
|
172 |
|
173 fun cfcomp_const (T, U, V) = |
|
174 Const (@{const_name cfcomp}, (U ->> V) ->> (T ->> U) ->> (T ->> V)); |
|
175 |
|
176 fun mk_cfcomp (f, g) = |
|
177 let |
|
178 val (U, V) = dest_cfunT (Term.fastype_of f); |
|
179 val (T, U') = dest_cfunT (Term.fastype_of g); |
|
180 in |
|
181 if U = U' |
|
182 then mk_capply (mk_capply (cfcomp_const (T, U, V), f), g) |
|
183 else raise TYPE ("mk_cfcomp", [U, U'], [f, g]) |
|
184 end; |
|
185 |
|
186 fun mk_Rep_of T = |
|
187 Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T; |
|
188 |
|
189 fun coerce_const T = Const (@{const_name coerce}, T); |
|
190 |
|
191 fun isodefl_const T = |
|
192 Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT); |
|
193 |
|
194 (* splits a cterm into the right and lefthand sides of equality *) |
|
195 fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t); |
|
196 |
|
197 fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)); |
|
198 |
|
199 (*** miscellaneous ***) |
|
200 |
|
201 fun declare_consts |
|
202 (decls : (binding * typ * mixfix) list) |
|
203 (thy : theory) |
|
204 : term list * theory = |
|
205 let |
|
206 fun con (b, T, mx) = Const (Sign.full_name thy b, T); |
|
207 val thy = Cont_Consts.add_consts decls thy; |
|
208 in |
|
209 (map con decls, thy) |
|
210 end; |
|
211 |
|
212 fun define_consts |
|
213 (specs : (binding * term * mixfix) list) |
|
214 (thy : theory) |
|
215 : (term list * thm list) * theory = |
|
216 let |
|
217 fun mk_decl (b, t, mx) = (b, Term.fastype_of t, mx); |
|
218 val decls = map mk_decl specs; |
|
219 val thy = Cont_Consts.add_consts decls thy; |
|
220 fun mk_const (b, T, mx) = Const (Sign.full_name thy b, T); |
|
221 val consts = map mk_const decls; |
|
222 fun mk_def c (b, t, mx) = |
|
223 (Binding.suffix_name "_def" b, Logic.mk_equals (c, t)); |
|
224 val defs = map2 mk_def consts specs; |
|
225 val (def_thms, thy) = |
|
226 PureThy.add_defs false (map Thm.no_attributes defs) thy; |
|
227 in |
|
228 ((consts, def_thms), thy) |
|
229 end; |
|
230 |
|
231 (*** argument preprocessing ***) |
|
232 |
|
233 type arg = (bool * binding option * typ) * string; |
|
234 |
|
235 |
|
236 |
|
237 (******************************* main function ********************************) |
|
238 |
|
239 fun add_domain_constructors |
|
240 (dname : string) |
|
241 (lhsT : typ, |
|
242 cons : (binding * (bool * binding option * typ) list * mixfix) list) |
|
243 (rep_const : term, abs_const : term) |
|
244 (rep_iso_thm : thm, abs_iso_thm : thm) |
|
245 (thy : theory) = |
|
246 let |
|
247 (* TODO: re-enable this *) |
|
248 (* val thy = Sign.add_path dname thy; *) |
|
249 |
|
250 (* define constructor functions *) |
|
251 val ((con_consts, con_def_thms), thy) = |
|
252 let |
|
253 fun prep_con (bind, args, mx) = |
|
254 (bind, args ~~ Datatype_Prop.make_tnames (map #3 args), mx); |
|
255 fun var_of ((lazy, sel, T), name) = Free (name, T); |
|
256 fun is_lazy ((lazy, sel, T), name) = lazy; |
|
257 val cons' = map prep_con cons; |
|
258 fun one_arg arg = (if is_lazy arg then mk_up else I) (var_of arg); |
|
259 fun one_con (bind, args, mx) = mk_stuple (map one_arg args); |
|
260 fun mk_abs t = abs_const ` t; |
|
261 val rhss = map mk_abs (mk_sinjects (map one_con cons')); |
|
262 fun mk_def (bind, args, mx) rhs = |
|
263 (bind, big_lambdas (map var_of args) rhs, mx); |
|
264 in |
|
265 define_consts (map2 mk_def cons' rhss) thy |
|
266 end; |
|
267 |
|
268 (* TODO: re-enable this *) |
|
269 (* val thy = Sign.parent_path thy; *) |
|
270 |
|
271 val result = |
|
272 { con_consts = con_consts, |
|
273 con_defs = con_def_thms }; |
|
274 in |
|
275 (result, thy) |
|
276 end; |
|
277 |
|
278 end; |