1 (* Title: HOL/ex/Antiquote.thy |
1 (* Title: HOL/ex/Antiquote.thy |
2 Author: Markus Wenzel, TU Muenchen |
2 Author: Markus Wenzel, TU Muenchen |
3 *) |
3 *) |
4 |
4 |
5 section {* Antiquotations *} |
5 section \<open>Antiquotations\<close> |
6 |
6 |
7 theory Antiquote |
7 theory Antiquote |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text \<open>A simple example on quote / antiquote in higher-order abstract syntax.\<close> |
12 A simple example on quote / antiquote in higher-order abstract |
|
13 syntax. |
|
14 *} |
|
15 |
12 |
16 definition var :: "'a \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat" ("VAR _" [1000] 999) |
13 definition var :: "'a \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat" ("VAR _" [1000] 999) |
17 where "var x env = env x" |
14 where "var x env = env x" |
18 |
15 |
19 definition Expr :: "(('a \<Rightarrow> nat) \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat" |
16 definition Expr :: "(('a \<Rightarrow> nat) \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat" |
20 where "Expr exp env = exp env" |
17 where "Expr exp env = exp env" |
21 |
18 |
22 syntax |
19 syntax |
23 "_Expr" :: "'a \<Rightarrow> 'a" ("EXPR _" [1000] 999) |
20 "_Expr" :: "'a \<Rightarrow> 'a" ("EXPR _" [1000] 999) |
24 |
21 |
25 parse_translation {* |
22 parse_translation |
26 [Syntax_Trans.quote_antiquote_tr |
23 \<open>[Syntax_Trans.quote_antiquote_tr |
27 @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}] |
24 @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]\<close> |
28 *} |
|
29 |
25 |
30 print_translation {* |
26 print_translation |
31 [Syntax_Trans.quote_antiquote_tr' |
27 \<open>[Syntax_Trans.quote_antiquote_tr' |
32 @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}] |
28 @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]\<close> |
33 *} |
|
34 |
29 |
35 term "EXPR (a + b + c)" |
30 term "EXPR (a + b + c)" |
36 term "EXPR (a + b + c + VAR x + VAR y + 1)" |
31 term "EXPR (a + b + c + VAR x + VAR y + 1)" |
37 term "EXPR (VAR (f w) + VAR x)" |
32 term "EXPR (VAR (f w) + VAR x)" |
38 |
33 |
39 term "Expr (\<lambda>env. env x)" -- {* improper *} |
34 term "Expr (\<lambda>env. env x)" -- \<open>improper\<close> |
40 term "Expr (\<lambda>env. f env)" |
35 term "Expr (\<lambda>env. f env)" |
41 term "Expr (\<lambda>env. f env + env x)" -- {* improper *} |
36 term "Expr (\<lambda>env. f env + env x)" -- \<open>improper\<close> |
42 term "Expr (\<lambda>env. f env y z)" |
37 term "Expr (\<lambda>env. f env y z)" |
43 term "Expr (\<lambda>env. f env + g y env)" |
38 term "Expr (\<lambda>env. f env + g y env)" |
44 term "Expr (\<lambda>env. f env + g env y + h a env z)" |
39 term "Expr (\<lambda>env. f env + g env y + h a env z)" |
45 |
40 |
46 end |
41 end |