122 (* type reflection *) |
122 (* type reflection *) |
123 |
123 |
124 fun type_tr (*"_TYPE"*) [ty] = |
124 fun type_tr (*"_TYPE"*) [ty] = |
125 const constrainC $ const "TYPE" $ (const "itself" $ ty) |
125 const constrainC $ const "TYPE" $ (const "itself" $ ty) |
126 | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts); |
126 | type_tr (*"_TYPE"*) ts = raise TERM ("type_tr", ts); |
|
127 |
|
128 |
|
129 (* binds *) |
|
130 |
|
131 fun bind_ast_tr (*"_BIND"*) [Variable x] = Variable (string_of_vname (binding x, 0)) |
|
132 | bind_ast_tr (*"_BIND"*) asts = raise AST ("bind_ast_tr", asts); |
127 |
133 |
128 |
134 |
129 (* quote / antiquote *) |
135 (* quote / antiquote *) |
130 |
136 |
131 fun quote_antiquote_tr quoteN antiquoteN name = |
137 fun quote_antiquote_tr quoteN antiquoteN name = |
324 (** pure_trfuns **) |
330 (** pure_trfuns **) |
325 |
331 |
326 val pure_trfuns = |
332 val pure_trfuns = |
327 ([("_appl", appl_ast_tr), ("_applC", applC_ast_tr), |
333 ([("_appl", appl_ast_tr), ("_applC", applC_ast_tr), |
328 ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), |
334 ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), |
329 ("_bigimpl", bigimpl_ast_tr)], |
335 ("_bigimpl", bigimpl_ast_tr), ("_BIND", bind_ast_tr)], |
330 [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr), |
336 [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr), |
331 ("_TYPE", type_tr), ("_K", k_tr)], |
337 ("_TYPE", type_tr), ("_K", k_tr)], |
332 []: (string * (term list -> term)) list, |
338 []: (string * (term list -> term)) list, |
333 [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"), |
339 [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"), |
334 ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr')]); |
340 ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr')]); |