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>\<open>_Expr\<close> \<^const_syntax>\<open>var\<close> \<^const_syntax>\<open>Expr\<close>]\<close> 25 26print_translation 27 \<open>[Syntax_Trans.quote_antiquote_tr' 28 \<^syntax_const>\<open>_Expr\<close> \<^const_syntax>\<open>var\<close> \<^const_syntax>\<open>Expr\<close>]\<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