author | wenzelm |
Sat, 17 Oct 2009 14:43:18 +0200 | |
changeset 32960 | 69916a850301 |
parent 16417 | 9bc16273c2d4 |
child 35113 | 1a0c129bb2e0 |
permissions | -rw-r--r-- |
8569 | 1 |
(* Title: HOL/ex/Multiquote.thy |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
*) |
|
5 |
||
10357 | 6 |
header {* Multiple nested quotations and anti-quotations *} |
7 |
||
16417 | 8 |
theory Multiquote imports Main begin |
8569 | 9 |
|
11586 | 10 |
text {* |
11 |
Multiple nested quotations and anti-quotations -- basically a |
|
12 |
generalized version of de-Bruijn representation. |
|
13 |
*} |
|
14 |
||
8569 | 15 |
syntax |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
16417
diff
changeset
|
16 |
"_quote" :: "'b => ('a => 'b)" ("\<guillemotleft>_\<guillemotright>" [0] 1000) |
10838 | 17 |
"_antiquote" :: "('a => 'b) => 'b" ("\<acute>_" [1000] 1000) |
8569 | 18 |
|
19 |
parse_translation {* |
|
20 |
let |
|
21 |
fun antiquote_tr i (Const ("_antiquote", _) $ (t as Const ("_antiquote", _) $ _)) = |
|
22 |
skip_antiquote_tr i t |
|
23 |
| antiquote_tr i (Const ("_antiquote", _) $ t) = |
|
24 |
antiquote_tr i t $ Bound i |
|
25 |
| antiquote_tr i (t $ u) = antiquote_tr i t $ antiquote_tr i u |
|
26 |
| antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t) |
|
27 |
| antiquote_tr _ a = a |
|
28 |
and skip_antiquote_tr i ((c as Const ("_antiquote", _)) $ t) = |
|
29 |
c $ skip_antiquote_tr i t |
|
30 |
| skip_antiquote_tr i t = antiquote_tr i t; |
|
31 |
||
8578 | 32 |
fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t)) |
8569 | 33 |
| quote_tr ts = raise TERM ("quote_tr", ts); |
34 |
in [("_quote", quote_tr)] end |
|
9297 | 35 |
*} |
8569 | 36 |
|
9297 | 37 |
text {* basic examples *} |
11823 | 38 |
term "\<guillemotleft>a + b + c\<guillemotright>" |
39 |
term "\<guillemotleft>a + b + c + \<acute>x + \<acute>y + 1\<guillemotright>" |
|
40 |
term "\<guillemotleft>\<acute>(f w) + \<acute>x\<guillemotright>" |
|
41 |
term "\<guillemotleft>f \<acute>x \<acute>y z\<guillemotright>" |
|
8569 | 42 |
|
9297 | 43 |
text {* advanced examples *} |
11823 | 44 |
term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright>\<guillemotright>" |
45 |
term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> o \<acute>f\<guillemotright>" |
|
46 |
term "\<guillemotleft>\<acute>(f o \<acute>g)\<guillemotright>" |
|
47 |
term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>(f o \<acute>g)\<guillemotright>\<guillemotright>" |
|
8569 | 48 |
|
9297 | 49 |
end |