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