fix broken syntax translations
authorhuffman
Thu Feb 07 03:30:32 2008 +0100 (2008-02-07)
changeset 260461624b3304bb9
parent 26045 02aa3f166c7f
child 26047 d27b89c95b29
fix broken syntax translations
src/HOLCF/Fixrec.thy
src/HOLCF/Ssum.thy
src/HOLCF/Tools/domain/domain_syntax.ML
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Fixrec.thy	Wed Feb 06 22:10:29 2008 +0100
     1.2 +++ b/src/HOLCF/Fixrec.thy	Thu Feb 07 03:30:32 2008 +0100
     1.3 @@ -201,11 +201,12 @@
     1.4  syntax
     1.5    "_pat" :: "'a"
     1.6    "_var" :: "'a"
     1.7 +  "_noargs" :: "'a"
     1.8  
     1.9  translations
    1.10 -  "_Case1 p r" => "XCONST branch (_pat p)\<cdot>(_var p r)"
    1.11 -  "_var (_args x y) r" => "XCONST csplit\<cdot>(_var x (_var y r))"
    1.12 -  "_var () r" => "XCONST unit_when\<cdot>r"
    1.13 +  "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_var p r)"
    1.14 +  "_var (_args x y) r" => "CONST csplit\<cdot>(_var x (_var y r))"
    1.15 +  "_var _noargs r" => "CONST unit_when\<cdot>r"
    1.16  
    1.17  parse_translation {*
    1.18  (* rewrites (_pat x) => (return) *)
    1.19 @@ -222,7 +223,7 @@
    1.20  print_translation {*
    1.21    let
    1.22      fun dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax unit_when},_) $ t) =
    1.23 -          (Syntax.const @{const_syntax Unity}, t)
    1.24 +          (Syntax.const "_noargs", t)
    1.25      |   dest_LAM (Const (@{const_syntax Rep_CFun},_) $ Const (@{const_syntax csplit},_) $ t) =
    1.26            let
    1.27              val (v1, t1) = dest_LAM t;
    1.28 @@ -287,14 +288,19 @@
    1.29  
    1.30  text {* Parse translations (patterns) *}
    1.31  translations
    1.32 -  "_pat (XCONST cpair\<cdot>x\<cdot>y)" => "XCONST cpair_pat (_pat x) (_pat y)"
    1.33 -  "_pat (XCONST spair\<cdot>x\<cdot>y)" => "XCONST spair_pat (_pat x) (_pat y)"
    1.34 -  "_pat (XCONST sinl\<cdot>x)" => "XCONST sinl_pat (_pat x)"
    1.35 -  "_pat (XCONST sinr\<cdot>x)" => "XCONST sinr_pat (_pat x)"
    1.36 -  "_pat (XCONST up\<cdot>x)" => "XCONST up_pat (_pat x)"
    1.37 -  "_pat (XCONST TT)" => "XCONST TT_pat"
    1.38 -  "_pat (XCONST FF)" => "XCONST FF_pat"
    1.39 -  "_pat (XCONST ONE)" => "XCONST ONE_pat"
    1.40 +  "_pat (XCONST cpair\<cdot>x\<cdot>y)" => "CONST cpair_pat (_pat x) (_pat y)"
    1.41 +  "_pat (XCONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
    1.42 +  "_pat (XCONST sinl\<cdot>x)" => "CONST sinl_pat (_pat x)"
    1.43 +  "_pat (XCONST sinr\<cdot>x)" => "CONST sinr_pat (_pat x)"
    1.44 +  "_pat (XCONST up\<cdot>x)" => "CONST up_pat (_pat x)"
    1.45 +  "_pat (XCONST TT)" => "CONST TT_pat"
    1.46 +  "_pat (XCONST FF)" => "CONST FF_pat"
    1.47 +  "_pat (XCONST ONE)" => "CONST ONE_pat"
    1.48 +
    1.49 +text {* CONST version is also needed for constructors with special syntax *}
    1.50 +translations
    1.51 +  "_pat (CONST cpair\<cdot>x\<cdot>y)" => "CONST cpair_pat (_pat x) (_pat y)"
    1.52 +  "_pat (CONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
    1.53  
    1.54  text {* Parse translations (variables) *}
    1.55  translations
    1.56 @@ -303,9 +309,13 @@
    1.57    "_var (XCONST sinl\<cdot>x) r" => "_var x r"
    1.58    "_var (XCONST sinr\<cdot>x) r" => "_var x r"
    1.59    "_var (XCONST up\<cdot>x) r" => "_var x r"
    1.60 -  "_var (XCONST TT) r" => "_var () r"
    1.61 -  "_var (XCONST FF) r" => "_var () r"
    1.62 -  "_var (XCONST ONE) r" => "_var () r"
    1.63 +  "_var (XCONST TT) r" => "_var _noargs r"
    1.64 +  "_var (XCONST FF) r" => "_var _noargs r"
    1.65 +  "_var (XCONST ONE) r" => "_var _noargs r"
    1.66 +
    1.67 +translations
    1.68 +  "_var (CONST cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
    1.69 +  "_var (CONST spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
    1.70  
    1.71  text {* Print translations *}
    1.72  translations
    1.73 @@ -316,9 +326,9 @@
    1.74    "CONST sinl\<cdot>(_match p1 v1)" <= "_match (CONST sinl_pat p1) v1"
    1.75    "CONST sinr\<cdot>(_match p1 v1)" <= "_match (CONST sinr_pat p1) v1"
    1.76    "CONST up\<cdot>(_match p1 v1)" <= "_match (CONST up_pat p1) v1"
    1.77 -  "CONST TT" <= "_match (CONST TT_pat) ()"
    1.78 -  "CONST FF" <= "_match (CONST FF_pat) ()"
    1.79 -  "CONST ONE" <= "_match (CONST ONE_pat) ()"
    1.80 +  "CONST TT" <= "_match (CONST TT_pat) _noargs"
    1.81 +  "CONST FF" <= "_match (CONST FF_pat) _noargs"
    1.82 +  "CONST ONE" <= "_match (CONST ONE_pat) _noargs"
    1.83  
    1.84  lemma cpair_pat1:
    1.85    "branch p\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> branch (cpair_pat p q)\<cdot>(csplit\<cdot>r)\<cdot>\<langle>x, y\<rangle> = \<bottom>"
    1.86 @@ -405,19 +415,19 @@
    1.87  
    1.88  text {* Parse translations (patterns) *}
    1.89  translations
    1.90 -  "_pat _" => "XCONST wild_pat"
    1.91 -  "_pat (_as_pat x y)" => "XCONST as_pat (_pat y)"
    1.92 -  "_pat (_lazy_pat x)" => "XCONST lazy_pat (_pat x)"
    1.93 +  "_pat _" => "CONST wild_pat"
    1.94 +  "_pat (_as_pat x y)" => "CONST as_pat (_pat y)"
    1.95 +  "_pat (_lazy_pat x)" => "CONST lazy_pat (_pat x)"
    1.96  
    1.97  text {* Parse translations (variables) *}
    1.98  translations
    1.99 -  "_var _ r" => "_var () r"
   1.100 +  "_var _ r" => "_var _noargs r"
   1.101    "_var (_as_pat x y) r" => "_var (_args x y) r"
   1.102    "_var (_lazy_pat x) r" => "_var x r"
   1.103  
   1.104  text {* Print translations *}
   1.105  translations
   1.106 -  "_" <= "_match (CONST wild_pat) ()"
   1.107 +  "_" <= "_match (CONST wild_pat) _noargs"
   1.108    "_as_pat x (_match p v)" <= "_match (CONST as_pat p) (_args (_var x) v)"
   1.109    "_lazy_pat (_match p v)" <= "_match (CONST lazy_pat p) v"
   1.110  
     2.1 --- a/src/HOLCF/Ssum.thy	Wed Feb 06 22:10:29 2008 +0100
     2.2 +++ b/src/HOLCF/Ssum.thy	Thu Feb 07 03:30:32 2008 +0100
     2.3 @@ -183,11 +183,11 @@
     2.4    "sscase = (\<Lambda> f g s. (\<Lambda><t, x, y>. If t then f\<cdot>x else g\<cdot>y fi)\<cdot>(Rep_Ssum s))"
     2.5  
     2.6  translations
     2.7 -  "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"
     2.8 +  "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"
     2.9  
    2.10  translations
    2.11 -  "\<Lambda>(CONST sinl\<cdot>x). t" == "CONST sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
    2.12 -  "\<Lambda>(CONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
    2.13 +  "\<Lambda>(XCONST sinl\<cdot>x). t" == "CONST sscase\<cdot>(\<Lambda> x. t)\<cdot>\<bottom>"
    2.14 +  "\<Lambda>(XCONST sinr\<cdot>y). t" == "CONST sscase\<cdot>\<bottom>\<cdot>(\<Lambda> y. t)"
    2.15  
    2.16  lemma beta_sscase:
    2.17    "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)"
     3.1 --- a/src/HOLCF/Tools/domain/domain_syntax.ML	Wed Feb 06 22:10:29 2008 +0100
     3.2 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML	Thu Feb 07 03:30:32 2008 +0100
     3.3 @@ -91,7 +91,7 @@
     3.4  
     3.5      fun app_var x = mk_appl (Constant "_var") [x, Variable "rhs"];
     3.6      fun app_pat x = mk_appl (Constant "_pat") [x];
     3.7 -    fun args_list [] = Constant "Unity"
     3.8 +    fun args_list [] = Constant "_noargs"
     3.9      |   args_list xs = foldr1 (app "_args") xs;
    3.10    in
    3.11      val case_trans = ParsePrintRule
     4.1 --- a/src/HOLCF/Up.thy	Wed Feb 06 22:10:29 2008 +0100
     4.2 +++ b/src/HOLCF/Up.thy	Thu Feb 07 03:30:32 2008 +0100
     4.3 @@ -233,8 +233,8 @@
     4.4    "fup = (\<Lambda> f p. Ifup f p)"
     4.5  
     4.6  translations
     4.7 -  "case l of CONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
     4.8 -  "\<Lambda>(CONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
     4.9 +  "case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l"
    4.10 +  "\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)"
    4.11  
    4.12  text {* continuous versions of lemmas for @{typ "('a)u"} *}
    4.13