src/HOLCF/Fixrec.thy
changeset 26046 1624b3304bb9
parent 25158 271e499f2d03
child 28891 f199def7a6a5
     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