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