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