src/HOL/ex/Multiquote.thy
changeset 8569 748a9699f28d
child 8572 794843a9d8b1
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Multiquote.thy	Fri Mar 24 17:28:03 2000 +0100
     1.3 @@ -0,0 +1,45 @@
     1.4 +(*  Title:      HOL/ex/Multiquote.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Multiple nested quotations and anti-quotations -- basically a
     1.9 +generalized version of de-Bruijn representation.
    1.10 +*)
    1.11 +
    1.12 +theory Multiquote = Main:;
    1.13 +
    1.14 +syntax
    1.15 +  "_quote" :: "'b \\<Rightarrow> ('a \\<Rightarrow> 'b)"	     ("{._.}" [0] 1000)
    1.16 +  "_antiquote" :: "('a \\<Rightarrow> 'b) \\<Rightarrow> 'b"        ("`_" [1000] 999);
    1.17 +
    1.18 +parse_translation {*
    1.19 +  let
    1.20 +    fun antiquote_tr i (Const ("_antiquote", _) $ (t as Const ("_antiquote", _) $ _)) =
    1.21 +          skip_antiquote_tr i t
    1.22 +      | antiquote_tr i (Const ("_antiquote", _) $ t) =
    1.23 +          antiquote_tr i t $ Bound i
    1.24 +      | antiquote_tr i (t $ u) = antiquote_tr i t $ antiquote_tr i u
    1.25 +      | antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t)
    1.26 +      | antiquote_tr _ a = a
    1.27 +    and skip_antiquote_tr i ((c as Const ("_antiquote", _)) $ t) =
    1.28 +          c $ skip_antiquote_tr i t
    1.29 +      | skip_antiquote_tr i t = antiquote_tr i t;
    1.30 +
    1.31 +    fun quote_tr [t] = Abs ("state", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
    1.32 +      | quote_tr ts = raise TERM ("quote_tr", ts);
    1.33 +  in [("_quote", quote_tr)] end
    1.34 +*};
    1.35 +
    1.36 +text {* basic examples *};
    1.37 +term "{. a + b + c .}";
    1.38 +term "{. a + b + c + `x + `y + 1 .}";
    1.39 +term "{. `(f w) + `x .}";
    1.40 +term "{. f (`x) (`y) z .}";
    1.41 +
    1.42 +text {* advanced examples *};
    1.43 +term "{. {. `(`x) + `y .} .}";
    1.44 +term "{. {. `(`x) + `y .} o `f .}";
    1.45 +term "{. `(f o `g) .}";
    1.46 +term "{. {. `(`(f o `g)) .} .}";
    1.47 +
    1.48 +end;