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