19 |
19 |
20 syntax |
20 syntax |
21 "_TYPEREP" :: "type => logic" ("(1TYPEREP/(1'(_')))") |
21 "_TYPEREP" :: "type => logic" ("(1TYPEREP/(1'(_')))") |
22 |
22 |
23 parse_translation {* |
23 parse_translation {* |
24 let |
24 let |
25 fun typerep_tr (*"_TYPEREP"*) [ty] = |
25 fun typerep_tr (*"_TYPEREP"*) [ty] = |
26 Syntax.const @{const_syntax typerep} $ |
26 Syntax.const @{const_syntax typerep} $ |
27 (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $ |
27 (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "TYPE"} $ |
28 (Syntax.const @{type_syntax itself} $ ty)) |
28 (Syntax.const @{type_syntax itself} $ ty)) |
29 | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts); |
29 | typerep_tr (*"_TYPEREP"*) ts = raise TERM ("typerep_tr", ts); |
30 in [(@{syntax_const "_TYPEREP"}, typerep_tr)] end |
30 in [(@{syntax_const "_TYPEREP"}, K typerep_tr)] end |
31 *} |
31 *} |
32 |
32 |
33 typed_print_translation (advanced) {* |
33 typed_print_translation {* |
34 let |
34 let |
35 fun typerep_tr' ctxt (*"typerep"*) |
35 fun typerep_tr' ctxt (*"typerep"*) |
36 (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _])) |
36 (Type (@{type_name fun}, [Type (@{type_name itself}, [T]), _])) |
37 (Const (@{const_syntax TYPE}, _) :: ts) = |
37 (Const (@{const_syntax TYPE}, _) :: ts) = |
38 Term.list_comb |
38 Term.list_comb |
39 (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts) |
39 (Syntax.const @{syntax_const "_TYPEREP"} $ Syntax_Phases.term_of_typ ctxt T, ts) |
40 | typerep_tr' _ T ts = raise Match; |
40 | typerep_tr' _ T ts = raise Match; |
41 in [(@{const_syntax typerep}, typerep_tr')] end |
41 in [(@{const_syntax typerep}, typerep_tr')] end |
42 *} |
42 *} |
43 |
43 |
44 setup {* |
44 setup {* |
45 let |
45 let |
46 |
46 |