59 (* abstraction *) |
59 (* abstraction *) |
60 |
60 |
61 fun idtyp_ast_tr (*"_idtyp"*) [x, ty] = Appl [Constant constrainC, x, ty] |
61 fun idtyp_ast_tr (*"_idtyp"*) [x, ty] = Appl [Constant constrainC, x, ty] |
62 | idtyp_ast_tr (*"_idtyp"*) asts = raise_ast "idtyp_ast_tr" asts; |
62 | idtyp_ast_tr (*"_idtyp"*) asts = raise_ast "idtyp_ast_tr" asts; |
63 |
63 |
64 fun lambda_ast_tr (*"_lambda"*) [idts, body] = |
64 fun lambda_ast_tr (*"_lambda"*) [pats, body] = |
65 fold_ast_p "_abs" (unfold_ast "_idts" idts, body) |
65 fold_ast_p "_abs" (unfold_ast "_pttrns" pats, body) |
66 | lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts; |
66 | lambda_ast_tr (*"_lambda"*) asts = raise_ast "lambda_ast_tr" asts; |
67 |
67 |
68 val constrainAbsC = "_constrainAbs"; |
68 val constrainAbsC = "_constrainAbs"; |
69 |
69 |
70 fun abs_tr (*"_abs"*) [Free (x, T), body] = absfree (x, T, body) |
70 fun abs_tr (*"_abs"*) [Free (x, T), body] = absfree (x, T, body) |
172 |
172 |
173 |
173 |
174 fun abs_ast_tr' (*"_abs"*) asts = |
174 fun abs_ast_tr' (*"_abs"*) asts = |
175 (case unfold_ast_p "_abs" (Appl (Constant "_abs" :: asts)) of |
175 (case unfold_ast_p "_abs" (Appl (Constant "_abs" :: asts)) of |
176 ([], _) => raise_ast "abs_ast_tr'" asts |
176 ([], _) => raise_ast "abs_ast_tr'" asts |
177 | (xs, body) => Appl [Constant "_lambda", fold_ast "_idts" xs, body]); |
177 | (xs, body) => Appl [Constant "_lambda", fold_ast "_pttrns" xs, body]); |
178 |
178 |
179 |
179 |
180 (* binder *) |
180 (* binder *) |
181 |
181 |
182 fun mk_binder_tr' (name, sy) = |
182 fun mk_binder_tr' (name, sy) = |
198 in |
198 in |
199 (name, binder_tr') |
199 (name, binder_tr') |
200 end; |
200 end; |
201 |
201 |
202 |
202 |
203 (* idts *) |
203 (* idtyp constraints *) |
204 |
204 |
205 fun idts_ast_tr' (*"_idts"*) [Appl [Constant c, x, ty], xs] = |
205 fun idtyp_ast_tr' a [Appl [Constant c, x, ty], xs] = |
206 if c = constrainC then |
206 if c = constrainC then |
207 Appl [Constant "_idts", Appl [Constant "_idtyp", x, ty], xs] |
207 Appl [Constant a, Appl [Constant "_idtyp", x, ty], xs] |
208 else raise Match |
208 else raise Match |
209 | idts_ast_tr' (*"_idts"*) _ = raise Match; |
209 | idtyp_ast_tr' _ _ = raise Match; |
210 |
210 |
211 |
211 |
212 (* meta propositions *) |
212 (* meta propositions *) |
213 |
213 |
214 fun prop_tr' show_sorts tm = |
214 fun prop_tr' show_sorts tm = |
279 ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), |
279 ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), |
280 ("_bigimpl", bigimpl_ast_tr)], |
280 ("_bigimpl", bigimpl_ast_tr)], |
281 [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr), |
281 [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr), |
282 ("_K", k_tr)], |
282 ("_K", k_tr)], |
283 [], |
283 [], |
284 [("_abs", abs_ast_tr'), ("_idts", idts_ast_tr'), ("==>", impl_ast_tr')]); |
284 [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"), |
|
285 ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr')]); |
285 |
286 |
286 val pure_trfunsT = |
287 val pure_trfunsT = |
287 [("_mk_ofclass", mk_ofclass_tr'), ("_mk_ofclassS", mk_ofclassS_tr')]; |
288 [("_mk_ofclass", mk_ofclass_tr'), ("_mk_ofclassS", mk_ofclassS_tr')]; |
288 |
289 |
289 |
290 |