src/HOL/ex/Multiquote.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 56233 797060c19f5c
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
wenzelm@8569
     1
(*  Title:      HOL/ex/Multiquote.thy
wenzelm@8569
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8569
     3
*)
wenzelm@8569
     4
wenzelm@10357
     5
header {* Multiple nested quotations and anti-quotations *}
wenzelm@10357
     6
wenzelm@35113
     7
theory Multiquote
wenzelm@35113
     8
imports Main
wenzelm@35113
     9
begin
wenzelm@8569
    10
wenzelm@11586
    11
text {*
wenzelm@11586
    12
  Multiple nested quotations and anti-quotations -- basically a
wenzelm@11586
    13
  generalized version of de-Bruijn representation.
wenzelm@11586
    14
*}
wenzelm@11586
    15
wenzelm@8569
    16
syntax
wenzelm@56233
    17
  "_quote" :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"    ("\<guillemotleft>_\<guillemotright>" [0] 1000)
wenzelm@56233
    18
  "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"    ("\<acute>_" [1000] 1000)
wenzelm@8569
    19
wenzelm@8569
    20
parse_translation {*
wenzelm@8569
    21
  let
wenzelm@35113
    22
    fun antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $
wenzelm@35113
    23
          (t as Const (@{syntax_const "_antiquote"}, _) $ _)) = skip_antiquote_tr i t
wenzelm@35113
    24
      | antiquote_tr i (Const (@{syntax_const "_antiquote"}, _) $ t) =
wenzelm@8569
    25
          antiquote_tr i t $ Bound i
wenzelm@8569
    26
      | antiquote_tr i (t $ u) = antiquote_tr i t $ antiquote_tr i u
wenzelm@8569
    27
      | antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t)
wenzelm@8569
    28
      | antiquote_tr _ a = a
wenzelm@35113
    29
    and skip_antiquote_tr i ((c as Const (@{syntax_const "_antiquote"}, _)) $ t) =
wenzelm@8569
    30
          c $ skip_antiquote_tr i t
wenzelm@8569
    31
      | skip_antiquote_tr i t = antiquote_tr i t;
wenzelm@8569
    32
wenzelm@8578
    33
    fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
wenzelm@8569
    34
      | quote_tr ts = raise TERM ("quote_tr", ts);
wenzelm@52143
    35
  in [(@{syntax_const "_quote"}, K quote_tr)] end
wenzelm@9297
    36
*}
wenzelm@8569
    37
wenzelm@9297
    38
text {* basic examples *}
wenzelm@11823
    39
term "\<guillemotleft>a + b + c\<guillemotright>"
wenzelm@11823
    40
term "\<guillemotleft>a + b + c + \<acute>x + \<acute>y + 1\<guillemotright>"
wenzelm@11823
    41
term "\<guillemotleft>\<acute>(f w) + \<acute>x\<guillemotright>"
wenzelm@11823
    42
term "\<guillemotleft>f \<acute>x \<acute>y z\<guillemotright>"
wenzelm@8569
    43
wenzelm@9297
    44
text {* advanced examples *}
wenzelm@11823
    45
term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright>\<guillemotright>"
wenzelm@56233
    46
term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>x + \<acute>y\<guillemotright> \<circ> \<acute>f\<guillemotright>"
wenzelm@56233
    47
term "\<guillemotleft>\<acute>(f \<circ> \<acute>g)\<guillemotright>"
wenzelm@56233
    48
term "\<guillemotleft>\<guillemotleft>\<acute>\<acute>(f \<circ> \<acute>g)\<guillemotright>\<guillemotright>"
wenzelm@8569
    49
wenzelm@9297
    50
end