Theory Antiquote

(*  Title:      HOL/ex/Antiquote.thy
    Author:     Markus Wenzel, TU Muenchen
*)

section ‹Antiquotations›

theory Antiquote
imports Main
begin

text ‹A simple example on quote / antiquote in higher-order abstract syntax.›

definition var :: "'a ⇒ ('a ⇒ nat) ⇒ nat"  ("VAR _" [1000] 999)
  where "var x env = env x"

definition Expr :: "(('a ⇒ nat) ⇒ nat) ⇒ ('a ⇒ nat) ⇒ nat"
  where "Expr exp env = exp env"

syntax
  "_Expr" :: "'a ⇒ 'a"  ("EXPR _" [1000] 999)

parse_translation
  ‹[Syntax_Trans.quote_antiquote_tr
    \<^syntax_const>‹_Expr› \<^const_syntax>‹var› \<^const_syntax>‹Expr›]›

print_translation
  ‹[Syntax_Trans.quote_antiquote_tr'
    \<^syntax_const>‹_Expr› \<^const_syntax>‹var› \<^const_syntax>‹Expr›]›

term "EXPR (a + b + c)"
term "EXPR (a + b + c + VAR x + VAR y + 1)"
term "EXPR (VAR (f w) + VAR x)"

term "Expr (λenv. env x)"    ― ‹improper›
term "Expr (λenv. f env)"
term "Expr (λenv. f env + env x)"    ― ‹improper›
term "Expr (λenv. f env y z)"
term "Expr (λenv. f env + g y env)"
term "Expr (λenv. f env + g env y + h a env z)"

end