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