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