src/HOL/ex/Multiquote.thy
author wenzelm
Thu Sep 27 15:42:08 2001 +0200 (2001-09-27)
changeset 11586 d8a7f6318457
parent 11020 646c929b6293
child 11823 5a3fcd84e55e
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 
     7 header {* Multiple nested quotations and anti-quotations *}
     8 
     9 theory Multiquote = Main:
    10 
    11 text {*
    12   Multiple nested quotations and anti-quotations -- basically a
    13   generalized version of de-Bruijn representation.
    14 *}
    15 
    16 syntax
    17   "_quote" :: "'b => ('a => 'b)"	     (".'(_')." [0] 1000)
    18   "_antiquote" :: "('a => 'b) => 'b"         ("\<acute>_" [1000] 1000)
    19 
    20 parse_translation {*
    21   let
    22     fun antiquote_tr i (Const ("_antiquote", _) $ (t as Const ("_antiquote", _) $ _)) =
    23           skip_antiquote_tr i t
    24       | antiquote_tr i (Const ("_antiquote", _) $ t) =
    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
    29     and skip_antiquote_tr i ((c as Const ("_antiquote", _)) $ t) =
    30           c $ skip_antiquote_tr i t
    31       | skip_antiquote_tr i t = antiquote_tr i t;
    32 
    33     fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
    34       | quote_tr ts = raise TERM ("quote_tr", ts);
    35   in [("_quote", quote_tr)] end
    36 *}
    37 
    38 text {* basic examples *}
    39 term ".(a + b + c)."
    40 term ".(a + b + c + \<acute>x + \<acute>y + 1)."
    41 term ".(\<acute>(f w) + \<acute>x)."
    42 term ".(f \<acute>x \<acute>y z)."
    43 
    44 text {* advanced examples *}
    45 term ".(.(\<acute>\<acute>x + \<acute>y).)."
    46 term ".(.(\<acute>\<acute>x + \<acute>y). \<circ> \<acute>f)."
    47 term ".(\<acute>(f \<circ> \<acute>g))."
    48 term ".(.( \<acute>\<acute>(f \<circ> \<acute>g) ).)."
    49 
    50 end