author | nipkow |
Fri, 21 Jun 2013 09:00:26 +0200 | |
changeset 52402 | c2f30ba4bb98 |
parent 44603 | a6f9a70d655d |
child 56233 | 797060c19f5c |
permissions | -rw-r--r-- |
5368 | 1 |
(* Title: HOL/ex/Antiquote.thy |
2 |
Author: Markus Wenzel, TU Muenchen |
|
3 |
*) |
|
4 |
||
10357 | 5 |
header {* Antiquotations *} |
6 |
||
35113 | 7 |
theory Antiquote |
8 |
imports Main |
|
9 |
begin |
|
5368 | 10 |
|
11586 | 11 |
text {* |
12 |
A simple example on quote / antiquote in higher-order abstract |
|
13 |
syntax. |
|
14 |
*} |
|
15 |
||
44603 | 16 |
definition var :: "'a => ('a => nat) => nat" ("VAR _" [1000] 999) |
35113 | 17 |
where "var x env = env x" |
5368 | 18 |
|
44603 | 19 |
definition Expr :: "(('a => nat) => nat) => ('a => nat) => nat" |
35113 | 20 |
where "Expr exp env = exp env" |
5368 | 21 |
|
44603 | 22 |
syntax |
23 |
"_Expr" :: "'a => 'a" ("EXPR _" [1000] 999) |
|
24 |
||
35113 | 25 |
parse_translation {* |
42284 | 26 |
[Syntax_Trans.quote_antiquote_tr |
27 |
@{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}] |
|
35113 | 28 |
*} |
29 |
||
30 |
print_translation {* |
|
42284 | 31 |
[Syntax_Trans.quote_antiquote_tr' |
32 |
@{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}] |
|
35113 | 33 |
*} |
8559 | 34 |
|
9297 | 35 |
term "EXPR (a + b + c)" |
36 |
term "EXPR (a + b + c + VAR x + VAR y + 1)" |
|
37 |
term "EXPR (VAR (f w) + VAR x)" |
|
5368 | 38 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
39 |
term "Expr (\<lambda>env. env x)" -- {* improper *} |
10357 | 40 |
term "Expr (\<lambda>env. f env)" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
41 |
term "Expr (\<lambda>env. f env + env x)" -- {* improper *} |
10357 | 42 |
term "Expr (\<lambda>env. f env y z)" |
43 |
term "Expr (\<lambda>env. f env + g y env)" |
|
44 |
term "Expr (\<lambda>env. f env + g env y + h a env z)" |
|
5368 | 45 |
|
9297 | 46 |
end |