56 "\<ordfeminine>x" \<rightleftharpoons> "x \<acute>CONST snd" |
56 "\<ordfeminine>x" \<rightleftharpoons> "x \<acute>CONST snd" |
57 |
57 |
58 print_translation {* |
58 print_translation {* |
59 let |
59 let |
60 fun quote_tr' f (t :: ts) = |
60 fun quote_tr' f (t :: ts) = |
61 Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts) |
61 Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts) |
62 | quote_tr' _ _ = raise Match; |
62 | quote_tr' _ _ = raise Match; |
63 |
63 |
64 val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"}); |
64 val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"}); |
65 |
65 |
66 fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) = |
66 fun bexp_tr' name ((Const (@{const_syntax Collect}, _) $ t) :: ts) = |
67 quote_tr' (Syntax.const name) (t :: ts) |
67 quote_tr' (Syntax.const name) (t :: ts) |
68 | bexp_tr' _ _ = raise Match; |
68 | bexp_tr' _ _ = raise Match; |
69 |
69 |
70 fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = |
70 fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) = |
71 quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f) |
71 quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f) |
72 (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts) |
72 (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts) |
73 | assign_tr' _ = raise Match; |
73 | assign_tr' _ = raise Match; |
74 in |
74 in |
75 [(@{const_syntax Collect}, assert_tr'), |
75 [(@{const_syntax Collect}, assert_tr'), |
76 (@{const_syntax Basic}, assign_tr'), |
76 (@{const_syntax Basic}, assign_tr'), |
77 (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}), |
77 (@{const_syntax Cond}, bexp_tr' @{syntax_const "_Cond"}), |