# HG changeset patch
# User wenzelm
# Date 953915283 -3600
# Node ID 748a9699f28d392a2fba7b9f021cf80d03de2a5e
# Parent  b18540435f26fbf2152f3a7ae5d9e31fcd9e9481
added HOL/ex/Multiquote.thy;

diff -r b18540435f26 -r 748a9699f28d src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Mar 24 14:40:51 2000 +0100
+++ b/src/HOL/IsaMakefile	Fri Mar 24 17:28:03 2000 +0100
@@ -425,7 +425,7 @@
   ex/StringEx.thy ex/Tarski.ML ex/Tarski.thy \
   ex/BinEx.ML ex/BinEx.thy ex/svc_test.thy ex/svc_test.ML ex/MonoidGroup.thy \
   ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML \
-  ex/Antiquote.thy ex/Points.thy
+  ex/Antiquote.thy ex/Multiquote.thy ex/Points.thy
 	@$(ISATOOL) usedir $(OUT)/HOL ex
 
 
diff -r b18540435f26 -r 748a9699f28d src/HOL/ex/Multiquote.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Multiquote.thy	Fri Mar 24 17:28:03 2000 +0100
@@ -0,0 +1,45 @@
+(*  Title:      HOL/ex/Multiquote.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Multiple nested quotations and anti-quotations -- basically a
+generalized version of de-Bruijn representation.
+*)
+
+theory Multiquote = Main:;
+
+syntax
+  "_quote" :: "'b \\<Rightarrow> ('a \\<Rightarrow> 'b)"	     ("{._.}" [0] 1000)
+  "_antiquote" :: "('a \\<Rightarrow> 'b) \\<Rightarrow> 'b"        ("`_" [1000] 999);
+
+parse_translation {*
+  let
+    fun antiquote_tr i (Const ("_antiquote", _) $ (t as Const ("_antiquote", _) $ _)) =
+          skip_antiquote_tr i t
+      | antiquote_tr i (Const ("_antiquote", _) $ t) =
+          antiquote_tr i t $ Bound i
+      | antiquote_tr i (t $ u) = antiquote_tr i t $ antiquote_tr i u
+      | antiquote_tr i (Abs (x, T, t)) = Abs (x, T, antiquote_tr (i + 1) t)
+      | antiquote_tr _ a = a
+    and skip_antiquote_tr i ((c as Const ("_antiquote", _)) $ t) =
+          c $ skip_antiquote_tr i t
+      | skip_antiquote_tr i t = antiquote_tr i t;
+
+    fun quote_tr [t] = Abs ("state", dummyT, antiquote_tr 0 (Term.incr_boundvars 1 t))
+      | quote_tr ts = raise TERM ("quote_tr", ts);
+  in [("_quote", quote_tr)] end
+*};
+
+text {* basic examples *};
+term "{. a + b + c .}";
+term "{. a + b + c + `x + `y + 1 .}";
+term "{. `(f w) + `x .}";
+term "{. f (`x) (`y) z .}";
+
+text {* advanced examples *};
+term "{. {. `(`x) + `y .} .}";
+term "{. {. `(`x) + `y .} o `f .}";
+term "{. `(f o `g) .}";
+term "{. {. `(`(f o `g)) .} .}";
+
+end;
diff -r b18540435f26 -r 748a9699f28d src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Mar 24 14:40:51 2000 +0100
+++ b/src/HOL/ex/ROOT.ML	Fri Mar 24 17:28:03 2000 +0100
@@ -48,6 +48,7 @@
 
 (*expressions with quote / antiquote syntax*)
 time_use_thy "Antiquote";
+time_use_thy "Multiquote";
 
 
 writeln "END: Root file for HOL examples";