translations: use XCONST for input patterns (keeps original spelling of const);
authorwenzelm
Tue Oct 23 13:29:16 2007 +0200 (2007-10-23)
changeset 25158271e499f2d03
parent 25157 8b80535cd017
child 25159 1822da5446bc
translations: use XCONST for input patterns (keeps original spelling of const);
src/HOLCF/Fixrec.thy
     1.1 --- a/src/HOLCF/Fixrec.thy	Tue Oct 23 13:10:19 2007 +0200
     1.2 +++ b/src/HOLCF/Fixrec.thy	Tue Oct 23 13:29:16 2007 +0200
     1.3 @@ -193,7 +193,7 @@
     1.4    "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
     1.5  
     1.6  translations
     1.7 -  "_Case_syntax x ms" == "Fixrec.run\<cdot>(ms\<cdot>x)"
     1.8 +  "_Case_syntax x ms" == "CONST Fixrec.run\<cdot>(ms\<cdot>x)"
     1.9    "_Case2 m ms" == "m \<parallel> ms"
    1.10  
    1.11  text {* Parsing Case expressions *}
    1.12 @@ -203,15 +203,15 @@
    1.13    "_var" :: "'a"
    1.14  
    1.15  translations
    1.16 -  "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_var p r)"
    1.17 -  "_var (_args x y) r" => "CONST csplit\<cdot>(_var x (_var y r))"
    1.18 -  "_var () r" => "CONST unit_when\<cdot>r"
    1.19 +  "_Case1 p r" => "XCONST branch (_pat p)\<cdot>(_var p r)"
    1.20 +  "_var (_args x y) r" => "XCONST csplit\<cdot>(_var x (_var y r))"
    1.21 +  "_var () r" => "XCONST unit_when\<cdot>r"
    1.22  
    1.23  parse_translation {*
    1.24  (* rewrites (_pat x) => (return) *)
    1.25  (* rewrites (_var x t) => (Abs_CFun (%x. t)) *)
    1.26    [("_pat", K (Syntax.const "Fixrec.return")),
    1.27 -   mk_binder_tr ("_var", @{const_syntax Abs_CFun})];
    1.28 +   mk_binder_tr ("_var", "Abs_CFun")];
    1.29  *}
    1.30  
    1.31  text {* Printing Case expressions *}
    1.32 @@ -287,25 +287,25 @@
    1.33  
    1.34  text {* Parse translations (patterns) *}
    1.35  translations
    1.36 -  "_pat (CONST cpair\<cdot>x\<cdot>y)" => "CONST cpair_pat (_pat x) (_pat y)"
    1.37 -  "_pat (CONST spair\<cdot>x\<cdot>y)" => "CONST spair_pat (_pat x) (_pat y)"
    1.38 -  "_pat (CONST sinl\<cdot>x)" => "CONST sinl_pat (_pat x)"
    1.39 -  "_pat (CONST sinr\<cdot>x)" => "CONST sinr_pat (_pat x)"
    1.40 -  "_pat (CONST up\<cdot>x)" => "CONST up_pat (_pat x)"
    1.41 -  "_pat (CONST TT)" => "CONST TT_pat"
    1.42 -  "_pat (CONST FF)" => "CONST FF_pat"
    1.43 -  "_pat (CONST ONE)" => "CONST ONE_pat"
    1.44 +  "_pat (XCONST cpair\<cdot>x\<cdot>y)" => "XCONST cpair_pat (_pat x) (_pat y)"
    1.45 +  "_pat (XCONST spair\<cdot>x\<cdot>y)" => "XCONST spair_pat (_pat x) (_pat y)"
    1.46 +  "_pat (XCONST sinl\<cdot>x)" => "XCONST sinl_pat (_pat x)"
    1.47 +  "_pat (XCONST sinr\<cdot>x)" => "XCONST sinr_pat (_pat x)"
    1.48 +  "_pat (XCONST up\<cdot>x)" => "XCONST up_pat (_pat x)"
    1.49 +  "_pat (XCONST TT)" => "XCONST TT_pat"
    1.50 +  "_pat (XCONST FF)" => "XCONST FF_pat"
    1.51 +  "_pat (XCONST ONE)" => "XCONST ONE_pat"
    1.52  
    1.53  text {* Parse translations (variables) *}
    1.54  translations
    1.55 -  "_var (CONST cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
    1.56 -  "_var (CONST spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
    1.57 -  "_var (CONST sinl\<cdot>x) r" => "_var x r"
    1.58 -  "_var (CONST sinr\<cdot>x) r" => "_var x r"
    1.59 -  "_var (CONST up\<cdot>x) r" => "_var x r"
    1.60 -  "_var (CONST TT) r" => "_var () r"
    1.61 -  "_var (CONST FF) r" => "_var () r"
    1.62 -  "_var (CONST ONE) r" => "_var () r"
    1.63 +  "_var (XCONST cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
    1.64 +  "_var (XCONST spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
    1.65 +  "_var (XCONST sinl\<cdot>x) r" => "_var x r"
    1.66 +  "_var (XCONST sinr\<cdot>x) r" => "_var x r"
    1.67 +  "_var (XCONST up\<cdot>x) r" => "_var x r"
    1.68 +  "_var (XCONST TT) r" => "_var () r"
    1.69 +  "_var (XCONST FF) r" => "_var () r"
    1.70 +  "_var (XCONST ONE) r" => "_var () r"
    1.71  
    1.72  text {* Print translations *}
    1.73  translations
    1.74 @@ -405,9 +405,9 @@
    1.75  
    1.76  text {* Parse translations (patterns) *}
    1.77  translations
    1.78 -  "_pat _" => "CONST wild_pat"
    1.79 -  "_pat (_as_pat x y)" => "CONST as_pat (_pat y)"
    1.80 -  "_pat (_lazy_pat x)" => "CONST lazy_pat (_pat x)"
    1.81 +  "_pat _" => "XCONST wild_pat"
    1.82 +  "_pat (_as_pat x y)" => "XCONST as_pat (_pat y)"
    1.83 +  "_pat (_lazy_pat x)" => "XCONST lazy_pat (_pat x)"
    1.84  
    1.85  text {* Parse translations (variables) *}
    1.86  translations
    1.87 @@ -423,7 +423,7 @@
    1.88  
    1.89  text {* Lazy patterns in lambda abstractions *}
    1.90  translations
    1.91 -  "_cabs (_lazy_pat p) r" == "CONST run oo (_Case1 (_lazy_pat p) r)"
    1.92 +  "_cabs (_lazy_pat p) r" == "CONST Fixrec.run oo (_Case1 (_lazy_pat p) r)"
    1.93  
    1.94  lemma wild_pat [simp]: "branch wild_pat\<cdot>(unit_when\<cdot>r)\<cdot>x = return\<cdot>r"
    1.95  by (simp add: branch_def wild_pat_def)