equal
deleted
inserted
replaced
1 (* Title: HOL/ex/Multiquote.thy |
1 (* Title: HOL/ex/Multiquote.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 |
5 |
5 Multiple nested quotations and anti-quotations -- basically a |
6 Multiple nested quotations and anti-quotations -- basically a |
6 generalized version of de-Bruijn representation. |
7 generalized version of de-Bruijn representation. |
7 *) |
8 *) |
8 |
9 |
9 theory Multiquote = Main:; |
10 theory Multiquote = Main: |
10 |
11 |
11 syntax |
12 syntax |
12 "_quote" :: "'b => ('a => 'b)" (".'(_')." [0] 1000) |
13 "_quote" :: "'b => ('a => 'b)" (".'(_')." [0] 1000) |
13 "_antiquote" :: "('a => 'b) => 'b" ("`_" [1000] 1000); |
14 "_antiquote" :: "('a => 'b) => 'b" ("`_" [1000] 1000) |
14 |
15 |
15 parse_translation {* |
16 parse_translation {* |
16 let |
17 let |
17 fun antiquote_tr i (Const ("_antiquote", _) $ (t as Const ("_antiquote", _) $ _)) = |
18 fun antiquote_tr i (Const ("_antiquote", _) $ (t as Const ("_antiquote", _) $ _)) = |
18 skip_antiquote_tr i t |
19 skip_antiquote_tr i t |
26 | skip_antiquote_tr i t = antiquote_tr i t; |
27 | skip_antiquote_tr i t = antiquote_tr i t; |
27 |
28 |
28 fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t)) |
29 fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t)) |
29 | quote_tr ts = raise TERM ("quote_tr", ts); |
30 | quote_tr ts = raise TERM ("quote_tr", ts); |
30 in [("_quote", quote_tr)] end |
31 in [("_quote", quote_tr)] end |
31 *}; |
32 *} |
32 |
33 |
33 text {* basic examples *}; |
34 text {* basic examples *} |
34 term ".(a + b + c)."; |
35 term ".(a + b + c)." |
35 term ".(a + b + c + `x + `y + 1)."; |
36 term ".(a + b + c + `x + `y + 1)." |
36 term ".(`(f w) + `x)."; |
37 term ".(`(f w) + `x)." |
37 term ".(f `x `y z)."; |
38 term ".(f `x `y z)." |
38 |
39 |
39 text {* advanced examples *}; |
40 text {* advanced examples *} |
40 term ".(.(` `x + `y).)."; |
41 term ".(.(` `x + `y).)." |
41 term ".(.(` `x + `y). o `f)."; |
42 term ".(.(` `x + `y). o `f)." |
42 term ".(`(f o `g))."; |
43 term ".(`(f o `g))." |
43 term ".(.( ` `(f o `g) ).)."; |
44 term ".(.( ` `(f o `g) ).)." |
44 |
45 |
45 end; |
46 end |