src/HOL/ex/Multiquote.thy
author wenzelm
Fri Mar 24 17:28:03 2000 +0100 (2000-03-24)
changeset 8569 748a9699f28d
child 8572 794843a9d8b1
permissions -rw-r--r--
added HOL/ex/Multiquote.thy;
     1 (*  Title:      HOL/ex/Multiquote.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Multiple nested quotations and anti-quotations -- basically a
     6 generalized version of de-Bruijn representation.
     7 *)
     8 
     9 theory Multiquote = Main:;
    10 
    11 syntax
    12   "_quote" :: "'b \\<Rightarrow> ('a \\<Rightarrow> 'b)"	     ("{._.}" [0] 1000)
    13   "_antiquote" :: "('a \\<Rightarrow> 'b) \\<Rightarrow> 'b"        ("`_" [1000] 999);
    14 
    15 parse_translation {*
    16   let
    17     fun antiquote_tr i (Const ("_antiquote", _) $ (t as Const ("_antiquote", _) $ _)) =
    18           skip_antiquote_tr i t
    19       | antiquote_tr i (Const ("_antiquote", _) $ t) =
    20           antiquote_tr i t $ Bound i
    21       | antiquote_tr i (t $ u) = antiquote_tr i t $ antiquote_tr i u
    22       | antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t)
    23       | antiquote_tr _ a = a
    24     and skip_antiquote_tr i ((c as Const ("_antiquote", _)) $ t) =
    25           c $ skip_antiquote_tr i t
    26       | skip_antiquote_tr i t = antiquote_tr i t;
    27 
    28     fun quote_tr [t] = Abs ("state", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
    29       | quote_tr ts = raise TERM ("quote_tr", ts);
    30   in [("_quote", quote_tr)] end
    31 *};
    32 
    33 text {* basic examples *};
    34 term "{. a + b + c .}";
    35 term "{. a + b + c + `x + `y + 1 .}";
    36 term "{. `(f w) + `x .}";
    37 term "{. f (`x) (`y) z .}";
    38 
    39 text {* advanced examples *};
    40 term "{. {. `(`x) + `y .} .}";
    41 term "{. {. `(`x) + `y .} o `f .}";
    42 term "{. `(f o `g) .}";
    43 term "{. {. `(`(f o `g)) .} .}";
    44 
    45 end;