renamed syntax constant "_var" to "_variable", to avoid clash with internal token marker;
authorwenzelm
Fri Jan 02 22:41:42 2009 +0100 (2009-01-02)
changeset 29322ae6f2b1559fa
parent 29321 6b9ecb3a70ab
child 29323 868634981a32
renamed syntax constant "_var" to "_variable", to avoid clash with internal token marker;
src/HOLCF/Fixrec.thy
src/HOLCF/Tools/domain/domain_syntax.ML
     1.1 --- a/src/HOLCF/Fixrec.thy	Fri Jan 02 19:59:26 2009 +0100
     1.2 +++ b/src/HOLCF/Fixrec.thy	Fri Jan 02 22:41:42 2009 +0100
     1.3 @@ -216,19 +216,19 @@
     1.4  
     1.5  syntax
     1.6    "_pat" :: "'a"
     1.7 -  "_var" :: "'a"
     1.8 +  "_variable" :: "'a"
     1.9    "_noargs" :: "'a"
    1.10  
    1.11  translations
    1.12 -  "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_var p r)"
    1.13 -  "_var (_args x y) r" => "CONST csplit\<cdot>(_var x (_var y r))"
    1.14 -  "_var _noargs r" => "CONST unit_when\<cdot>r"
    1.15 +  "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_variable p r)"
    1.16 +  "_variable (_args x y) r" => "CONST csplit\<cdot>(_variable x (_variable y r))"
    1.17 +  "_variable _noargs r" => "CONST unit_when\<cdot>r"
    1.18  
    1.19  parse_translation {*
    1.20  (* rewrites (_pat x) => (return) *)
    1.21 -(* rewrites (_var x t) => (Abs_CFun (%x. t)) *)
    1.22 +(* rewrites (_variable x t) => (Abs_CFun (%x. t)) *)
    1.23    [("_pat", K (Syntax.const "Fixrec.return")),
    1.24 -   mk_binder_tr ("_var", "Abs_CFun")];
    1.25 +   mk_binder_tr ("_variable", "Abs_CFun")];
    1.26  *}
    1.27  
    1.28  text {* Printing Case expressions *}
    1.29 @@ -250,7 +250,7 @@
    1.30              val abs = case t of Abs abs => abs
    1.31                  | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
    1.32              val (x, t') = atomic_abs_tr' abs;
    1.33 -          in (Syntax.const "_var" $ x, t') end
    1.34 +          in (Syntax.const "_variable" $ x, t') end
    1.35      |   dest_LAM _ = raise Match; (* too few vars: abort translation *)
    1.36  
    1.37      fun Case1_tr' [Const(@{const_syntax branch},_) $ p, r] =
    1.38 @@ -261,7 +261,7 @@
    1.39  *}
    1.40  
    1.41  translations
    1.42 -  "x" <= "_match Fixrec.return (_var x)"
    1.43 +  "x" <= "_match Fixrec.return (_variable x)"
    1.44  
    1.45  
    1.46  subsection {* Pattern combinators for data constructors *}
    1.47 @@ -320,18 +320,18 @@
    1.48  
    1.49  text {* Parse translations (variables) *}
    1.50  translations
    1.51 -  "_var (XCONST cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
    1.52 -  "_var (XCONST spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
    1.53 -  "_var (XCONST sinl\<cdot>x) r" => "_var x r"
    1.54 -  "_var (XCONST sinr\<cdot>x) r" => "_var x r"
    1.55 -  "_var (XCONST up\<cdot>x) r" => "_var x r"
    1.56 -  "_var (XCONST TT) r" => "_var _noargs r"
    1.57 -  "_var (XCONST FF) r" => "_var _noargs r"
    1.58 -  "_var (XCONST ONE) r" => "_var _noargs r"
    1.59 +  "_variable (XCONST cpair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
    1.60 +  "_variable (XCONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
    1.61 +  "_variable (XCONST sinl\<cdot>x) r" => "_variable x r"
    1.62 +  "_variable (XCONST sinr\<cdot>x) r" => "_variable x r"
    1.63 +  "_variable (XCONST up\<cdot>x) r" => "_variable x r"
    1.64 +  "_variable (XCONST TT) r" => "_variable _noargs r"
    1.65 +  "_variable (XCONST FF) r" => "_variable _noargs r"
    1.66 +  "_variable (XCONST ONE) r" => "_variable _noargs r"
    1.67  
    1.68  translations
    1.69 -  "_var (CONST cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
    1.70 -  "_var (CONST spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
    1.71 +  "_variable (CONST cpair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
    1.72 +  "_variable (CONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
    1.73  
    1.74  text {* Print translations *}
    1.75  translations
    1.76 @@ -437,14 +437,14 @@
    1.77  
    1.78  text {* Parse translations (variables) *}
    1.79  translations
    1.80 -  "_var _ r" => "_var _noargs r"
    1.81 -  "_var (_as_pat x y) r" => "_var (_args x y) r"
    1.82 -  "_var (_lazy_pat x) r" => "_var x r"
    1.83 +  "_variable _ r" => "_variable _noargs r"
    1.84 +  "_variable (_as_pat x y) r" => "_variable (_args x y) r"
    1.85 +  "_variable (_lazy_pat x) r" => "_variable x r"
    1.86  
    1.87  text {* Print translations *}
    1.88  translations
    1.89    "_" <= "_match (CONST wild_pat) _noargs"
    1.90 -  "_as_pat x (_match p v)" <= "_match (CONST as_pat p) (_args (_var x) v)"
    1.91 +  "_as_pat x (_match p v)" <= "_match (CONST as_pat p) (_args (_variable x) v)"
    1.92    "_lazy_pat (_match p v)" <= "_match (CONST lazy_pat p) v"
    1.93  
    1.94  text {* Lazy patterns in lambda abstractions *}
     2.1 --- a/src/HOLCF/Tools/domain/domain_syntax.ML	Fri Jan 02 19:59:26 2009 +0100
     2.2 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML	Fri Jan 02 22:41:42 2009 +0100
     2.3 @@ -89,7 +89,7 @@
     2.4      fun arg1 n (con,_,args) = foldr cabs (expvar n) (argvars n args);
     2.5      fun when1 n m = if n = m then arg1 n else K (Constant "UU");
     2.6  
     2.7 -    fun app_var x = mk_appl (Constant "_var") [x, Variable "rhs"];
     2.8 +    fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
     2.9      fun app_pat x = mk_appl (Constant "_pat") [x];
    2.10      fun args_list [] = Constant "_noargs"
    2.11      |   args_list xs = foldr1 (app "_args") xs;