|
1 (* Title: Pure/Syntax/syn_trans.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow and Markus Wenzel, TU Muenchen |
|
4 |
|
5 Syntax translation functions. |
|
6 *) |
|
7 |
|
8 signature SYN_TRANS0 = |
|
9 sig |
|
10 val eta_contract: bool ref |
|
11 val mk_binder_tr: string * string -> string * (term list -> term) |
|
12 val mk_binder_tr': string * string -> string * (term list -> term) |
|
13 val dependent_tr': string * string -> term list -> term |
|
14 end; |
|
15 |
|
16 signature SYN_TRANS1 = |
|
17 sig |
|
18 include SYN_TRANS0 |
|
19 structure Parser: PARSER |
|
20 local open Parser.SynExt.Ast in |
|
21 val constrainAbsC: string |
|
22 val pure_trfuns: |
|
23 (string * (ast list -> ast)) list * |
|
24 (string * (term list -> term)) list * |
|
25 (string * (term list -> term)) list * |
|
26 (string * (ast list -> ast)) list |
|
27 end |
|
28 end; |
|
29 |
|
30 signature SYN_TRANS = |
|
31 sig |
|
32 include SYN_TRANS1 |
|
33 local open Parser Parser.SynExt Parser.SynExt.Ast in |
|
34 val abs_tr': term -> term |
|
35 val prop_tr': bool -> term -> term |
|
36 val appl_ast_tr': ast * ast list -> ast |
|
37 val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast |
|
38 val ast_to_term: (string -> (term list -> term) option) -> ast -> term |
|
39 end |
|
40 end; |
|
41 |
|
42 functor SynTransFun(structure TypeExt: TYPE_EXT and Parser: PARSER |
|
43 sharing TypeExt.SynExt = Parser.SynExt): SYN_TRANS = |
|
44 struct |
|
45 |
|
46 structure Parser = Parser; |
|
47 open TypeExt Parser.Lexicon Parser.SynExt.Ast Parser.SynExt Parser; |
|
48 |
|
49 |
|
50 (** parse (ast) translations **) |
|
51 |
|
52 (* application *) |
|
53 |
|
54 fun appl_ast_tr (*"_appl"*) [f, args] = Appl (f :: unfold_ast "_args" args) |
|
55 | appl_ast_tr (*"_appl"*) asts = raise_ast "appl_ast_tr" asts; |
|
56 |
|
57 |
|
58 (* abstraction *) |
|
59 |
|
60 fun idtyp_ast_tr (*"_idtyp"*) [x, ty] = Appl [Constant constrainC, x, ty] |
|
61 | idtyp_ast_tr (*"_idtyp"*) asts = raise_ast "idtyp_ast_tr" asts; |
|
62 |
|
63 fun lambda_ast_tr (*"_lambda"*) [idts, body] = |
|
64 fold_ast_p "_abs" (unfold_ast "_idts" idts, body) |
|
65 | lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts; |
|
66 |
|
67 val constrainAbsC = "_constrainAbs"; |
|
68 |
|
69 fun abs_tr (*"_abs"*) [Free (x, T), body] = absfree (x, T, body) |
|
70 | abs_tr (*"_abs"*) (ts as [Const (c, _) $ Free (x, T) $ tT, body]) = |
|
71 if c = constrainC |
|
72 then const constrainAbsC $ absfree (x, T, body) $ tT |
|
73 else raise_term "abs_tr" ts |
|
74 | abs_tr (*"_abs"*) ts = raise_term "abs_tr" ts; |
|
75 |
|
76 |
|
77 (* nondependent abstraction *) |
|
78 |
|
79 fun k_tr (*"_K"*) [t] = Abs ("uu", dummyT, incr_boundvars 1 t) |
|
80 | k_tr (*"_K"*) ts = raise_term "k_tr" ts; |
|
81 |
|
82 |
|
83 (* binder *) |
|
84 |
|
85 fun mk_binder_tr (sy, name) = |
|
86 let |
|
87 fun tr (Free (x, T), t) = const name $ absfree (x, T, t) |
|
88 | tr (Const ("_idts", _) $ idt $ idts, t) = tr (idt, tr (idts, t)) |
|
89 | tr (t1 as Const (c, _) $ Free (x, T) $ tT, t) = |
|
90 if c = constrainC then |
|
91 const name $ (const constrainAbsC $ absfree (x, T, t) $ tT) |
|
92 else raise_term "binder_tr" [t1, t] |
|
93 | tr (t1, t2) = raise_term "binder_tr" [t1, t2]; |
|
94 |
|
95 fun binder_tr (*sy*) [idts, body] = tr (idts, body) |
|
96 | binder_tr (*sy*) ts = raise_term "binder_tr" ts; |
|
97 in |
|
98 (sy, binder_tr) |
|
99 end; |
|
100 |
|
101 |
|
102 (* meta propositions *) |
|
103 |
|
104 fun aprop_tr (*"_aprop"*) [t] = const constrainC $ t $ const "prop" |
|
105 | aprop_tr (*"_aprop"*) ts = raise_term "aprop_tr" ts; |
|
106 |
|
107 fun ofclass_tr (*"_ofclass"*) [ty, cls] = |
|
108 cls $ (const constrainC $ const "TYPE" $ (const "itself" $ ty)) |
|
109 | ofclass_tr (*"_ofclass"*) ts = raise_term "ofclass_tr" ts; |
|
110 |
|
111 |
|
112 (* meta implication *) |
|
113 |
|
114 fun bigimpl_ast_tr (*"_bigimpl"*) [asms, concl] = |
|
115 fold_ast_p "==>" (unfold_ast "_asms" asms, concl) |
|
116 | bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts; |
|
117 |
|
118 |
|
119 (* explode atoms *) |
|
120 |
|
121 fun explode_tr (*"_explode"*) (ts as [consC, nilC, bit0, bit1, txt]) = |
|
122 let |
|
123 fun mk_list [] = nilC |
|
124 | mk_list (t :: ts) = consC $ t $ mk_list ts; |
|
125 |
|
126 fun encode_bit 0 = bit0 |
|
127 | encode_bit 1 = bit1 |
|
128 | encode_bit _ = sys_error "encode_bit"; |
|
129 |
|
130 fun encode_char c = (* FIXME leading 0s (?) *) |
|
131 mk_list (map encode_bit (radixpand (2, (ord c)))); |
|
132 |
|
133 val str = |
|
134 (case txt of |
|
135 Free (s, _) => s |
|
136 | Const (s, _) => s |
|
137 | _ => raise_term "explode_tr" ts); |
|
138 in |
|
139 mk_list (map encode_char (explode str)) |
|
140 end |
|
141 | explode_tr (*"_explode"*) ts = raise_term "explode_tr" ts; |
|
142 |
|
143 |
|
144 |
|
145 (** print (ast) translations **) |
|
146 |
|
147 (* application *) |
|
148 |
|
149 fun appl_ast_tr' (f, []) = raise_ast "appl_ast_tr'" [f] |
|
150 | appl_ast_tr' (f, args) = Appl [Constant "_appl", f, fold_ast "_args" args]; |
|
151 |
|
152 |
|
153 (* abstraction *) |
|
154 |
|
155 fun strip_abss vars_of body_of tm = |
|
156 let |
|
157 val vars = vars_of tm; |
|
158 val body = body_of tm; |
|
159 val rev_new_vars = rename_wrt_term body vars; |
|
160 in |
|
161 (map Free (rev rev_new_vars), |
|
162 subst_bounds (map (free o #1) rev_new_vars, body)) |
|
163 end; |
|
164 |
|
165 (*do (partial) eta-contraction before printing*) |
|
166 |
|
167 val eta_contract = ref false; |
|
168 |
|
169 fun eta_contr tm = |
|
170 let |
|
171 fun eta_abs (Abs (a, T, t)) = |
|
172 (case eta_abs t of |
|
173 t' as f $ u => |
|
174 (case eta_abs u of |
|
175 Bound 0 => |
|
176 if not (0 mem loose_bnos f) then incr_boundvars ~1 f |
|
177 else Abs (a, T, t') |
|
178 | _ => Abs (a, T, t')) |
|
179 | t' => Abs (a, T, t')) |
|
180 | eta_abs t = t; |
|
181 in |
|
182 if ! eta_contract then eta_abs tm else tm |
|
183 end; |
|
184 |
|
185 |
|
186 fun abs_tr' tm = |
|
187 foldr (fn (x, t) => const "_abs" $ x $ t) |
|
188 (strip_abss strip_abs_vars strip_abs_body (eta_contr tm)); |
|
189 |
|
190 |
|
191 fun abs_ast_tr' (*"_abs"*) asts = |
|
192 (case unfold_ast_p "_abs" (Appl (Constant "_abs" :: asts)) of |
|
193 ([], _) => raise_ast "abs_ast_tr'" asts |
|
194 | (xs, body) => Appl [Constant "_lambda", fold_ast "_idts" xs, body]); |
|
195 |
|
196 |
|
197 (* binder *) |
|
198 |
|
199 fun mk_binder_tr' (name, sy) = |
|
200 let |
|
201 fun mk_idts [] = raise Match (*abort translation*) |
|
202 | mk_idts [idt] = idt |
|
203 | mk_idts (idt :: idts) = const "_idts" $ idt $ mk_idts idts; |
|
204 |
|
205 fun tr' t = |
|
206 let |
|
207 val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t; |
|
208 in |
|
209 const sy $ mk_idts xs $ bd |
|
210 end; |
|
211 |
|
212 fun binder_tr' (*name*) (t :: ts) = |
|
213 list_comb (tr' (const name $ t), ts) |
|
214 | binder_tr' (*name*) [] = raise Match; |
|
215 in |
|
216 (name, binder_tr') |
|
217 end; |
|
218 |
|
219 |
|
220 (* idts *) |
|
221 |
|
222 fun idts_ast_tr' (*"_idts"*) [Appl [Constant c, x, ty], xs] = |
|
223 if c = constrainC then |
|
224 Appl [Constant "_idts", Appl [Constant "_idtyp", x, ty], xs] |
|
225 else raise Match |
|
226 | idts_ast_tr' (*"_idts"*) _ = raise Match; |
|
227 |
|
228 |
|
229 (* meta propositions *) |
|
230 |
|
231 fun prop_tr' show_sorts tm = |
|
232 let |
|
233 fun aprop t = const "_aprop" $ t; |
|
234 |
|
235 fun is_prop tys t = |
|
236 fastype_of1 (tys, t) = propT handle TERM _ => false; |
|
237 |
|
238 fun tr' _ (t as Const _) = t |
|
239 | tr' _ (t as Free (x, ty)) = |
|
240 if ty = propT then aprop (free x) else t |
|
241 | tr' _ (t as Var (xi, ty)) = |
|
242 if ty = propT then aprop (var xi) else t |
|
243 | tr' tys (t as Bound _) = |
|
244 if is_prop tys t then aprop t else t |
|
245 | tr' tys (Abs (x, ty, t)) = Abs (x, ty, tr' (ty :: tys) t) |
|
246 | tr' tys (t as t1 $ (t2 as Const ("TYPE", Type ("itself", [ty])))) = |
|
247 if is_prop tys t then |
|
248 const "_ofclass" $ term_of_typ show_sorts ty $ tr' tys t1 |
|
249 else tr' tys t1 $ tr' tys t2 |
|
250 | tr' tys (t as t1 $ t2) = |
|
251 (if is_Const (head_of t) orelse not (is_prop tys t) |
|
252 then I else aprop) (tr' tys t1 $ tr' tys t2); |
|
253 in |
|
254 tr' [] tm |
|
255 end; |
|
256 |
|
257 |
|
258 (* meta implication *) |
|
259 |
|
260 fun impl_ast_tr' (*"==>"*) asts = |
|
261 (case unfold_ast_p "==>" (Appl (Constant "==>" :: asts)) of |
|
262 (asms as _ :: _ :: _, concl) |
|
263 => Appl [Constant "_bigimpl", fold_ast "_asms" asms, concl] |
|
264 | _ => raise Match); |
|
265 |
|
266 |
|
267 (* dependent / nondependent quantifiers *) |
|
268 |
|
269 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) = |
|
270 if 0 mem (loose_bnos B) then |
|
271 let val (x', B') = variant_abs (x, dummyT, B); |
|
272 in list_comb (const q $ Free (x', T) $ A $ B', ts) end |
|
273 else list_comb (const r $ A $ B, ts) |
|
274 | dependent_tr' _ _ = raise Match; |
|
275 |
|
276 |
|
277 (* implode atoms *) |
|
278 |
|
279 fun implode_ast_tr' (*"_implode"*) (asts as [Constant cons_name, nilC, |
|
280 bit0, bit1, bitss]) = |
|
281 let |
|
282 fun err () = raise_ast "implode_ast_tr'" asts; |
|
283 |
|
284 fun strip_list lst = |
|
285 let val (xs, y) = unfold_ast_p cons_name lst |
|
286 in if y = nilC then xs else err () |
|
287 end; |
|
288 |
|
289 fun decode_bit bit = |
|
290 if bit = bit0 then "0" |
|
291 else if bit = bit1 then "1" |
|
292 else err (); |
|
293 |
|
294 fun decode_char bits = |
|
295 chr (#1 (scan_radixint (2, map decode_bit (strip_list bits)))); |
|
296 in |
|
297 Variable (implode (map decode_char (strip_list bitss))) |
|
298 end |
|
299 | implode_ast_tr' (*"_implode"*) asts = raise_ast "implode_ast_tr'" asts; |
|
300 |
|
301 |
|
302 |
|
303 (** pure_trfuns **) |
|
304 |
|
305 val pure_trfuns = |
|
306 ([(applC, appl_ast_tr), ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), |
|
307 ("_bigimpl", bigimpl_ast_tr)], |
|
308 [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr), |
|
309 ("_K", k_tr), ("_explode", explode_tr)], |
|
310 [], |
|
311 [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'), ("==>", impl_ast_tr'), |
|
312 ("_implode", implode_ast_tr')]); |
|
313 |
|
314 |
|
315 |
|
316 (** pt_to_ast **) |
|
317 |
|
318 fun pt_to_ast trf pt = |
|
319 let |
|
320 fun trans a args = |
|
321 (case trf a of |
|
322 None => mk_appl (Constant a) args |
|
323 | Some f => f args handle exn |
|
324 => (writeln ("Error in parse ast translation for " ^ quote a); raise exn)); |
|
325 |
|
326 fun ast_of (Node (a, pts)) = trans a (map ast_of pts) |
|
327 | ast_of (Tip tok) = Variable (str_of_token tok); |
|
328 in |
|
329 ast_of pt |
|
330 end; |
|
331 |
|
332 |
|
333 |
|
334 (** ast_to_term **) |
|
335 |
|
336 fun ast_to_term trf ast = |
|
337 let |
|
338 fun trans a args = |
|
339 (case trf a of |
|
340 None => list_comb (const a, args) |
|
341 | Some f => f args handle exn |
|
342 => (writeln ("Error in parse translation for " ^ quote a); raise exn)); |
|
343 |
|
344 fun term_of (Constant a) = trans a [] |
|
345 | term_of (Variable x) = scan_var x |
|
346 | term_of (Appl (Constant a :: (asts as _ :: _))) = |
|
347 trans a (map term_of asts) |
|
348 | term_of (Appl (ast :: (asts as _ :: _))) = |
|
349 list_comb (term_of ast, map term_of asts) |
|
350 | term_of (ast as Appl _) = raise_ast "ast_to_term: malformed ast" [ast]; |
|
351 in |
|
352 term_of ast |
|
353 end; |
|
354 |
|
355 |
|
356 end; |
|
357 |