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