src/HOL/ex/Antiquote.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 61933 cf58b5b794b2
child 69597 ff784d5a5bfb
permissions -rw-r--r--
bundle lifting_syntax;
wenzelm@5368
     1
(*  Title:      HOL/ex/Antiquote.thy
wenzelm@5368
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5368
     3
*)
wenzelm@5368
     4
wenzelm@59031
     5
section \<open>Antiquotations\<close>
wenzelm@10357
     6
wenzelm@35113
     7
theory Antiquote
wenzelm@35113
     8
imports Main
wenzelm@35113
     9
begin
wenzelm@5368
    10
wenzelm@59031
    11
text \<open>A simple example on quote / antiquote in higher-order abstract syntax.\<close>
wenzelm@11586
    12
wenzelm@56233
    13
definition var :: "'a \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"  ("VAR _" [1000] 999)
wenzelm@35113
    14
  where "var x env = env x"
wenzelm@5368
    15
wenzelm@56233
    16
definition Expr :: "(('a \<Rightarrow> nat) \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat"
wenzelm@35113
    17
  where "Expr exp env = exp env"
wenzelm@5368
    18
wenzelm@44603
    19
syntax
wenzelm@56233
    20
  "_Expr" :: "'a \<Rightarrow> 'a"  ("EXPR _" [1000] 999)
wenzelm@44603
    21
wenzelm@59031
    22
parse_translation
wenzelm@59031
    23
  \<open>[Syntax_Trans.quote_antiquote_tr
wenzelm@59031
    24
    @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]\<close>
wenzelm@35113
    25
wenzelm@59031
    26
print_translation
wenzelm@59031
    27
  \<open>[Syntax_Trans.quote_antiquote_tr'
wenzelm@59031
    28
    @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]\<close>
wenzelm@8559
    29
wenzelm@9297
    30
term "EXPR (a + b + c)"
wenzelm@9297
    31
term "EXPR (a + b + c + VAR x + VAR y + 1)"
wenzelm@9297
    32
term "EXPR (VAR (f w) + VAR x)"
wenzelm@5368
    33
wenzelm@61933
    34
term "Expr (\<lambda>env. env x)"    \<comment> \<open>improper\<close>
wenzelm@10357
    35
term "Expr (\<lambda>env. f env)"
wenzelm@61933
    36
term "Expr (\<lambda>env. f env + env x)"    \<comment> \<open>improper\<close>
wenzelm@10357
    37
term "Expr (\<lambda>env. f env y z)"
wenzelm@10357
    38
term "Expr (\<lambda>env. f env + g y env)"
wenzelm@10357
    39
term "Expr (\<lambda>env. f env + g env y + h a env z)"
wenzelm@5368
    40
wenzelm@9297
    41
end