src/HOL/ex/Multiquote.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 59031 4c3bb56b8ce7
child 69597 ff784d5a5bfb
permissions -rw-r--r--
bundle lifting_syntax;
     1 (*  Title:      HOL/ex/Multiquote.thy
     2     Author:     Markus Wenzel, TU Muenchen
     3 *)
     4 
     5 section \<open>Multiple nested quotations and anti-quotations\<close>
     6 
     7 theory Multiquote
     8 imports Main
     9 begin
    10 
    11 text \<open>
    12   Multiple nested quotations and anti-quotations -- basically a
    13   generalized version of de-Bruijn representation.
    14 \<close>
    15 
    16 syntax
    17   "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"    ("\<guillemotleft>_\<guillemotright>" [0] 1000)
    18   "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"    ("\<acute>_" [1000] 1000)
    19 
    20 parse_translation \<open>
    21   let
    22     fun antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $
    23           (t as Const (@{syntax_const "_antiquote"}, _) $ _)) = skip_antiquote_tr i t
    24       | antiquote_tr i (Const (@{syntax_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 (@{syntax_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 [(@{syntax_const "_quote"}, K quote_tr)] end
    36 \<close>
    37 
    38 text \<open>basic examples\<close>
    39 term "\<guillemotleft>a + b + c\<guillemotright>"
    40 term "\<guillemotleft>a + b + c + \<acute>x + \<acute>y + 1\<guillemotright>"
    41 term "\<guillemotleft>\<acute>(f w) + \<acute>x\<guillemotright>"
    42 term "\<guillemotleft>f \<acute>x \<acute>y z\<guillemotright>"
    43 
    44 text \<open>advanced examples\<close>
    45 term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright>\<guillemotright>"
    46 term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> \<circ> \<acute>f\<guillemotright>"
    47 term "\<guillemotleft>\<acute>(f \<circ> \<acute>g)\<guillemotright>"
    48 term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>(f \<circ> \<acute>g)\<guillemotright>\<guillemotright>"
    49 
    50 end