src/HOL/ex/Multiquote.thy
author wenzelm
Wed Jan 10 00:15:33 2001 +0100 (2001-01-10)
changeset 10838 9423817dee84
parent 10834 a7897aebbffc
child 11020 646c929b6293
permissions -rw-r--r--
use \<acute>;
wenzelm@8569
     1
(*  Title:      HOL/ex/Multiquote.thy
wenzelm@8569
     2
    ID:         $Id$
wenzelm@8569
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@9297
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@8569
     5
wenzelm@8569
     6
Multiple nested quotations and anti-quotations -- basically a
wenzelm@8569
     7
generalized version of de-Bruijn representation.
wenzelm@8569
     8
*)
wenzelm@8569
     9
wenzelm@10357
    10
header {* Multiple nested quotations and anti-quotations *}
wenzelm@10357
    11
wenzelm@9297
    12
theory Multiquote = Main:
wenzelm@8569
    13
wenzelm@8569
    14
syntax
wenzelm@8578
    15
  "_quote" :: "'b => ('a => 'b)"	     (".'(_')." [0] 1000)
wenzelm@10838
    16
  "_antiquote" :: "('a => 'b) => 'b"         ("\<acute>_" [1000] 1000)
wenzelm@8569
    17
wenzelm@8569
    18
parse_translation {*
wenzelm@8569
    19
  let
wenzelm@8569
    20
    fun antiquote_tr i (Const ("_antiquote", _) $ (t as Const ("_antiquote", _) $ _)) =
wenzelm@8569
    21
          skip_antiquote_tr i t
wenzelm@8569
    22
      | antiquote_tr i (Const ("_antiquote", _) $ t) =
wenzelm@8569
    23
          antiquote_tr i t $ Bound i
wenzelm@8569
    24
      | antiquote_tr i (t $ u) = antiquote_tr i t $ antiquote_tr i u
wenzelm@8569
    25
      | antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t)
wenzelm@8569
    26
      | antiquote_tr _ a = a
wenzelm@8569
    27
    and skip_antiquote_tr i ((c as Const ("_antiquote", _)) $ t) =
wenzelm@8569
    28
          c $ skip_antiquote_tr i t
wenzelm@8569
    29
      | skip_antiquote_tr i t = antiquote_tr i t;
wenzelm@8569
    30
wenzelm@8578
    31
    fun quote_tr [t] = Abs ("s", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
wenzelm@8569
    32
      | quote_tr ts = raise TERM ("quote_tr", ts);
wenzelm@8569
    33
  in [("_quote", quote_tr)] end
wenzelm@9297
    34
*}
wenzelm@8569
    35
wenzelm@9297
    36
text {* basic examples *}
wenzelm@9297
    37
term ".(a + b + c)."
wenzelm@10838
    38
term ".(a + b + c + \<acute>x + \<acute>y + 1)."
wenzelm@10838
    39
term ".(\<acute>(f w) + \<acute>x)."
wenzelm@10838
    40
term ".(f \<acute>x \<acute>y z)."
wenzelm@8569
    41
wenzelm@9297
    42
text {* advanced examples *}
wenzelm@10838
    43
term ".(.(\<acute>\<acute>x + \<acute>y).)."
wenzelm@10838
    44
term ".(.(\<acute>\<acute>x + \<acute>y). o \<acute>f)."
wenzelm@10838
    45
term ".(\<acute>(f o \<acute>g))."
wenzelm@10838
    46
term ".(.( \<acute>\<acute>(f o \<acute>g) ).)."
wenzelm@8569
    47
wenzelm@9297
    48
end