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