# HG changeset patch
# User huffman
# Date 1202351432 -3600
# Node ID 1624b3304bb9c4aabeec4650c97f57688ba8fd3c
# Parent  02aa3f166c7fe6a45badd797c5c9c1f93ad4d0a7
fix broken syntax translations

diff -r 02aa3f166c7f -r 1624b3304bb9 src/HOLCF/Fixrec.thy
--- a/src/HOLCF/Fixrec.thy	Wed Feb 06 22:10:29 2008 +0100
+++ b/src/HOLCF/Fixrec.thy	Thu Feb 07 03:30:32 2008 +0100
@@ -201,11 +201,12 @@
 syntax
   "_pat" :: "'a"
   "_var" :: "'a"
+  "_noargs" :: "'a"
 
 translations
-  "_Case1 p r" => "XCONST branch (_pat p)\<cdot>(_var p r)"
-  "_var (_args x y) r" => "XCONST csplit\<cdot>(_var x (_var y r))"
-  "_var () r" => "XCONST unit_when\<cdot>r"
+  "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_var p r)"
+  "_var (_args x y) r" => "CONST csplit\<cdot>(_var x (_var y r))"
+  "_var _noargs r" => "CONST unit_when\<cdot>r"
 
 parse_translation {*
 (* rewrites (_pat x) => (return) *)
@@ -222,7 +223,7 @@
 print_translation {*
   let
     fun dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax unit_when},_) $ t) =
-          (Syntax.const @{const_syntax Unity}, t)
+          (Syntax.const "_noargs", t)
     |   dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax csplit},_) $ t) =
           let
             val (v1, t1) = dest_LAM t;
@@ -287,14 +288,19 @@
 
 text {* Parse translations (patterns) *}
 translations
-  "_pat (XCONST cpair\<cdot>x\<cdot>y)" => "XCONST cpair_pat (_pat x) (_pat y)"
-  "_pat (XCONST spair\<cdot>x\<cdot>y)" => "XCONST spair_pat (_pat x) (_pat y)"
-  "_pat (XCONST sinl\<cdot>x)" => "XCONST sinl_pat (_pat x)"
-  "_pat (XCONST sinr\<cdot>x)" => "XCONST sinr_pat (_pat x)"
-  "_pat (XCONST up\<cdot>x)" => "XCONST up_pat (_pat x)"
-  "_pat (XCONST TT)" => "XCONST TT_pat"
-  "_pat (XCONST FF)" => "XCONST FF_pat"
-  "_pat (XCONST ONE)" => "XCONST ONE_pat"
+  "_pat (XCONST cpair\<cdot>x\<cdot>y)" => "CONST cpair_pat (_pat x) (_pat y)"
+  "_pat (XCONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
+  "_pat (XCONST sinl\<cdot>x)" => "CONST sinl_pat (_pat x)"
+  "_pat (XCONST sinr\<cdot>x)" => "CONST sinr_pat (_pat x)"
+  "_pat (XCONST up\<cdot>x)" => "CONST up_pat (_pat x)"
+  "_pat (XCONST TT)" => "CONST TT_pat"
+  "_pat (XCONST FF)" => "CONST FF_pat"
+  "_pat (XCONST ONE)" => "CONST ONE_pat"
+
+text {* CONST version is also needed for constructors with special syntax *}
+translations
+  "_pat (CONST cpair\<cdot>x\<cdot>y)" => "CONST cpair_pat (_pat x) (_pat y)"
+  "_pat (CONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
 
 text {* Parse translations (variables) *}
 translations
@@ -303,9 +309,13 @@
   "_var (XCONST sinl\<cdot>x) r" => "_var x r"
   "_var (XCONST sinr\<cdot>x) r" => "_var x r"
   "_var (XCONST up\<cdot>x) r" => "_var x r"
-  "_var (XCONST TT) r" => "_var () r"
-  "_var (XCONST FF) r" => "_var () r"
-  "_var (XCONST ONE) r" => "_var () r"
+  "_var (XCONST TT) r" => "_var _noargs r"
+  "_var (XCONST FF) r" => "_var _noargs r"
+  "_var (XCONST ONE) r" => "_var _noargs r"
+
+translations
+  "_var (CONST cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
+  "_var (CONST spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
 
 text {* Print translations *}
 translations
@@ -316,9 +326,9 @@
   "CONST sinl\<cdot>(_match p1 v1)" <= "_match (CONST sinl_pat p1) v1"
   "CONST sinr\<cdot>(_match p1 v1)" <= "_match (CONST sinr_pat p1) v1"
   "CONST up\<cdot>(_match p1 v1)" <= "_match (CONST up_pat p1) v1"
-  "CONST TT" <= "_match (CONST TT_pat) ()"
-  "CONST FF" <= "_match (CONST FF_pat) ()"
-  "CONST ONE" <= "_match (CONST ONE_pat) ()"
+  "CONST TT" <= "_match (CONST TT_pat) _noargs"
+  "CONST FF" <= "_match (CONST FF_pat) _noargs"
+  "CONST ONE" <= "_match (CONST ONE_pat) _noargs"
 
 lemma cpair_pat1:
   "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = \<bottom>"
@@ -405,19 +415,19 @@
 
 text {* Parse translations (patterns) *}
 translations
-  "_pat _" => "XCONST wild_pat"
-  "_pat (_as_pat x y)" => "XCONST as_pat (_pat y)"
-  "_pat (_lazy_pat x)" => "XCONST lazy_pat (_pat x)"
+  "_pat _" => "CONST wild_pat"
+  "_pat (_as_pat x y)" => "CONST as_pat (_pat y)"
+  "_pat (_lazy_pat x)" => "CONST lazy_pat (_pat x)"
 
 text {* Parse translations (variables) *}
 translations
-  "_var _ r" => "_var () r"
+  "_var _ r" => "_var _noargs r"
   "_var (_as_pat x y) r" => "_var (_args x y) r"
   "_var (_lazy_pat x) r" => "_var x r"
 
 text {* Print translations *}
 translations
-  "_" <= "_match (CONST wild_pat) ()"
+  "_" <= "_match (CONST wild_pat) _noargs"
   "_as_pat x (_match p v)" <= "_match (CONST as_pat p) (_args (_var x) v)"
   "_lazy_pat (_match p v)" <= "_match (CONST lazy_pat p) v"
 
diff -r 02aa3f166c7f -r 1624b3304bb9 src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Wed Feb 06 22:10:29 2008 +0100
+++ b/src/HOLCF/Ssum.thy	Thu Feb 07 03:30:32 2008 +0100
@@ -183,11 +183,11 @@
   "sscase = (\<Lambda> f g s. (\<Lambda><t, x, y>. If t then f\<cdot>x else g\<cdot>y fi)\<cdot>(Rep_Ssum s))"
 
 translations
-  "case s of CONST sinl\<cdot>x \<Rightarrow> t1 | CONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
+  "case s of XCONST sinl\<cdot>x \<Rightarrow> t1 | XCONST sinr\<cdot>y \<Rightarrow> t2" == "CONST sscase\<cdot>(\<Lambda> x. t1)\<cdot>(\<Lambda> y. t2)\<cdot>s"
 
 translations
-  "\<Lambda>(CONST sinl\<cdot>x). t" == "CONST sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
-  "\<Lambda>(CONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
+  "\<Lambda>(XCONST sinl\<cdot>x). t" == "CONST sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
+  "\<Lambda>(XCONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
 
 lemma beta_sscase:
   "sscase\<cdot>f\<cdot>g\<cdot>s = (\<Lambda><t, x, y>. If t then f\<cdot>x else g\<cdot>y fi)\<cdot>(Rep_Ssum s)"
diff -r 02aa3f166c7f -r 1624b3304bb9 src/HOLCF/Tools/domain/domain_syntax.ML
--- a/src/HOLCF/Tools/domain/domain_syntax.ML	Wed Feb 06 22:10:29 2008 +0100
+++ b/src/HOLCF/Tools/domain/domain_syntax.ML	Thu Feb 07 03:30:32 2008 +0100
@@ -91,7 +91,7 @@
 
     fun app_var x = mk_appl (Constant "_var") [x, Variable "rhs"];
     fun app_pat x = mk_appl (Constant "_pat") [x];
-    fun args_list [] = Constant "Unity"
+    fun args_list [] = Constant "_noargs"
     |   args_list xs = foldr1 (app "_args") xs;
   in
     val case_trans = ParsePrintRule
diff -r 02aa3f166c7f -r 1624b3304bb9 src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Wed Feb 06 22:10:29 2008 +0100
+++ b/src/HOLCF/Up.thy	Thu Feb 07 03:30:32 2008 +0100
@@ -233,8 +233,8 @@
   "fup = (\<Lambda> f p. Ifup f p)"
 
 translations
-  "case l of CONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
-  "\<Lambda>(CONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
+  "case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
+  "\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
 
 text {* continuous versions of lemmas for @{typ "('a)u"} *}