author | haftmann |
Wed, 21 Oct 2009 08:16:25 +0200 | |
changeset 33039 | 5018f6a76b3f |
parent 32960 | 69916a850301 |
child 35113 | 1a0c129bb2e0 |
permissions | -rw-r--r-- |
5368 | 1 |
(* Title: HOL/ex/Antiquote.thy |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
*) |
|
5 |
||
10357 | 6 |
header {* Antiquotations *} |
7 |
||
16417 | 8 |
theory Antiquote imports Main begin |
5368 | 9 |
|
11586 | 10 |
text {* |
11 |
A simple example on quote / antiquote in higher-order abstract |
|
12 |
syntax. |
|
13 |
*} |
|
14 |
||
5368 | 15 |
syntax |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
16 |
"_Expr" :: "'a => 'a" ("EXPR _" [1000] 999) |
5368 | 17 |
|
18 |
constdefs |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
19 |
var :: "'a => ('a => nat) => nat" ("VAR _" [1000] 999) |
5368 | 20 |
"var x env == env x" |
21 |
||
8559 | 22 |
Expr :: "(('a => nat) => nat) => ('a => nat) => nat" |
9297 | 23 |
"Expr exp env == exp env" |
5368 | 24 |
|
9297 | 25 |
parse_translation {* [Syntax.quote_antiquote_tr "_Expr" "var" "Expr"] *} |
26 |
print_translation {* [Syntax.quote_antiquote_tr' "_Expr" "var" "Expr"] *} |
|
8559 | 27 |
|
9297 | 28 |
term "EXPR (a + b + c)" |
29 |
term "EXPR (a + b + c + VAR x + VAR y + 1)" |
|
30 |
term "EXPR (VAR (f w) + VAR x)" |
|
5368 | 31 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
32 |
term "Expr (\<lambda>env. env x)" -- {* improper *} |
10357 | 33 |
term "Expr (\<lambda>env. f env)" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
34 |
term "Expr (\<lambda>env. f env + env x)" -- {* improper *} |
10357 | 35 |
term "Expr (\<lambda>env. f env y z)" |
36 |
term "Expr (\<lambda>env. f env + g y env)" |
|
37 |
term "Expr (\<lambda>env. f env + g env y + h a env z)" |
|
5368 | 38 |
|
9297 | 39 |
end |