src/HOL/ex/Multiquote.thy
author urbanc
Tue Jun 05 09:56:19 2007 +0200 (2007-06-05)
changeset 23243 a37d3e6e8323
parent 16417 9bc16273c2d4
child 32960 69916a850301
permissions -rw-r--r--
included Class.thy in the compiling process for Nominal/Examples
     1 (*  Title:      HOL/ex/Multiquote.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 *)
     5 
     6 header {* Multiple nested quotations and anti-quotations *}
     7 
     8 theory Multiquote imports Main begin
     9 
    10 text {*
    11   Multiple nested quotations and anti-quotations -- basically a
    12   generalized version of de-Bruijn representation.
    13 *}
    14 
    15 syntax
    16   "_quote" :: "'b => ('a => 'b)"	     ("\<guillemotleft>_\<guillemotright>" [0] 1000)
    17   "_antiquote" :: "('a => 'b) => 'b"         ("\<acute>_" [1000] 1000)
    18 
    19 parse_translation {*
    20   let
    21     fun antiquote_tr i (Const ("_antiquote", _) $ (t as Const ("_antiquote", _) $ _)) =
    22           skip_antiquote_tr i t
    23       | antiquote_tr i (Const ("_antiquote", _) $ t) =
    24           antiquote_tr i t $ Bound i
    25       | antiquote_tr i (t $ u) = antiquote_tr i t $ antiquote_tr i u
    26       | antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t)
    27       | antiquote_tr _ a = a
    28     and skip_antiquote_tr i ((c as Const ("_antiquote", _)) $ t) =
    29           c $ skip_antiquote_tr i t
    30       | skip_antiquote_tr i t = antiquote_tr i t;
    31 
    32     fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
    33       | quote_tr ts = raise TERM ("quote_tr", ts);
    34   in [("_quote", quote_tr)] end
    35 *}
    36 
    37 text {* basic examples *}
    38 term "\<guillemotleft>a + b + c\<guillemotright>"
    39 term "\<guillemotleft>a + b + c + \<acute>x + \<acute>y + 1\<guillemotright>"
    40 term "\<guillemotleft>\<acute>(f w) + \<acute>x\<guillemotright>"
    41 term "\<guillemotleft>f \<acute>x \<acute>y z\<guillemotright>"
    42 
    43 text {* advanced examples *}
    44 term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright>\<guillemotright>"
    45 term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> o \<acute>f\<guillemotright>"
    46 term "\<guillemotleft>\<acute>(f o \<acute>g)\<guillemotright>"
    47 term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>(f o \<acute>g)\<guillemotright>\<guillemotright>"
    48 
    49 end