src/HOL/ex/Antiquote.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 44603 a6f9a70d655d
child 56233 797060c19f5c
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (*  Title:      HOL/ex/Antiquote.thy
     2     Author:     Markus Wenzel, TU Muenchen
     3 *)
     4 
     5 header {* Antiquotations *}
     6 
     7 theory Antiquote
     8 imports Main
     9 begin
    10 
    11 text {*
    12   A simple example on quote / antiquote in higher-order abstract
    13   syntax.
    14 *}
    15 
    16 definition var :: "'a => ('a => nat) => nat"  ("VAR _" [1000] 999)
    17   where "var x env = env x"
    18 
    19 definition Expr :: "(('a => nat) => nat) => ('a => nat) => nat"
    20   where "Expr exp env = exp env"
    21 
    22 syntax
    23   "_Expr" :: "'a => 'a"  ("EXPR _" [1000] 999)
    24 
    25 parse_translation {*
    26   [Syntax_Trans.quote_antiquote_tr
    27     @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
    28 *}
    29 
    30 print_translation {*
    31   [Syntax_Trans.quote_antiquote_tr'
    32     @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
    33 *}
    34 
    35 term "EXPR (a + b + c)"
    36 term "EXPR (a + b + c + VAR x + VAR y + 1)"
    37 term "EXPR (VAR (f w) + VAR x)"
    38 
    39 term "Expr (\<lambda>env. env x)"    -- {* improper *}
    40 term "Expr (\<lambda>env. f env)"
    41 term "Expr (\<lambda>env. f env + env x)"    -- {* improper *}
    42 term "Expr (\<lambda>env. f env y z)"
    43 term "Expr (\<lambda>env. f env + g y env)"
    44 term "Expr (\<lambda>env. f env + g env y + h a env z)"
    45 
    46 end