reimplemented Case syntax using print/parse translations; moved as-patterns to separate section
authorhuffman
Mon Nov 07 23:33:01 2005 +0100 (2005-11-07)
changeset 18112dc1d6f588204
parent 18111 2b56f74fd605
child 18113 fb76eea85835
reimplemented Case syntax using print/parse translations; moved as-patterns to separate section
src/HOLCF/Fixrec.thy
     1.1 --- a/src/HOLCF/Fixrec.thy	Mon Nov 07 23:30:49 2005 +0100
     1.2 +++ b/src/HOLCF/Fixrec.thy	Mon Nov 07 23:33:01 2005 +0100
     1.3 @@ -138,29 +138,34 @@
     1.4  
     1.5  lemmas fatbar_simps = fatbar1 fatbar2 fatbar3
     1.6  
     1.7 +lemma run_fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = \<bottom>"
     1.8 +by (simp add: fatbar_def)
     1.9 +
    1.10 +lemma run_fatbar2: "m\<cdot>x = fail \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = run\<cdot>(ms\<cdot>x)"
    1.11 +by (simp add: fatbar_def)
    1.12 +
    1.13 +lemma run_fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = y"
    1.14 +by (simp add: fatbar_def)
    1.15 +
    1.16 +lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
    1.17 +
    1.18  subsection {* Pattern combinators *}
    1.19  
    1.20 -types ('a,'b,'c) pattern = "'b \<rightarrow> 'a \<rightarrow> 'c maybe"
    1.21 +types ('a,'b,'c) pat = "'b \<rightarrow> 'a \<rightarrow> 'c maybe"
    1.22  
    1.23  constdefs
    1.24 -  wild_pat :: "('a, 'b, 'b) pattern"
    1.25 +  wild_pat :: "('a, 'b, 'b) pat"
    1.26    "wild_pat \<equiv> \<Lambda> r a. return\<cdot>r"
    1.27  
    1.28 -  var_pat :: "('a, 'a \<rightarrow> 'b, 'b) pattern"
    1.29 +  var_pat :: "('a, 'a \<rightarrow> 'b, 'b) pat"
    1.30    "var_pat \<equiv> \<Lambda> r a. return\<cdot>(r\<cdot>a)"
    1.31  
    1.32 -  as_pat :: "('a, 'b, 'c) pattern \<Rightarrow> ('a, 'a \<rightarrow> 'b, 'c) pattern"
    1.33 -  "as_pat p \<equiv> \<Lambda> r a. p\<cdot>(r\<cdot>a)\<cdot>a"
    1.34 -
    1.35  lemma wild_pat [simp]: "wild_pat\<cdot>r\<cdot>a = return\<cdot>r"
    1.36  by (simp add: wild_pat_def)
    1.37  
    1.38  lemma var_pat [simp]: "var_pat\<cdot>r\<cdot>a = return\<cdot>(r\<cdot>a)"
    1.39  by (simp add: var_pat_def)
    1.40  
    1.41 -lemma as_pat [simp]: "as_pat p\<cdot>r\<cdot>a = p\<cdot>(r\<cdot>a)\<cdot>a"
    1.42 -by (simp add: as_pat_def)
    1.43 -
    1.44  subsection {* Case syntax *}
    1.45  
    1.46  nonterminals
    1.47 @@ -171,86 +176,134 @@
    1.48    "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ =>/ _)" 10)
    1.49    ""            :: "Case_syn => Cases_syn"               ("_")
    1.50    "_Case2"      :: "[Case_syn, Cases_syn] => Cases_syn"  ("_/ | _")
    1.51 -  "_as_pattern" :: "[idt, 'a] \<Rightarrow> 'a"                     (* infixr "as" 10 *)
    1.52  
    1.53  syntax (xsymbols)
    1.54    "_Case1"      :: "['a, 'b] => Case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
    1.55  
    1.56 +text {* Intermediate tags for parsing/printing *}
    1.57  syntax
    1.58 -  "_match"   :: "'a \<Rightarrow> Case_syn" (* or Cases_syn *)
    1.59 -  "_as"      :: "[pttrn, Case_syn] \<Rightarrow> Case_syn"
    1.60 -  "_matches" :: "['a, Case_syn, 'a list] \<Rightarrow> Case_syn"
    1.61 -  "_cons"    :: "['a, 'a list] \<Rightarrow> 'a list"
    1.62 -  "_nil"     :: "'a list"
    1.63 +  "_pat" :: "'a"
    1.64 +  "_var" :: "'a"
    1.65 +  "_match" :: "'a"
    1.66 +
    1.67 +text {* Parsing Case expressions *}
    1.68  
    1.69  translations
    1.70 -  "_Case_syntax x (_match m)"     == "run\<cdot>(m\<cdot>x)"
    1.71 -  "_Case2 (_match c) (_match cs)" == "_match (c \<parallel> cs)"
    1.72 -  "_Case1 dummy_pattern r"        == "_match (wild_pat\<cdot>r)"
    1.73 -  "_as x (_match (p\<cdot>t))"          == "_match ((as_pat p)\<cdot>(\<Lambda> x. t))"
    1.74 -  "_Case1 (_as_pattern x e) r"    == "_as x (_Case1 e r)"
    1.75 -  "_Case1 x t"                    == "_match (var_pat\<cdot>(\<Lambda> x. t))"
    1.76 -  "_Case1 (f\<cdot>e) r" == "_matches f (_Case1 e r) _nil"
    1.77 -  "_matches (f\<cdot>e) (_match (p\<cdot>r)) ps" == "_matches f (_Case1 e r) (_cons p ps)"
    1.78 +  "_Case_syntax x cs" => "run\<cdot>(cs\<cdot>x)"
    1.79 +  "_Case2 c cs" => "fatbar\<cdot>c\<cdot>cs"
    1.80 +  "_Case1 p r" => "_match (_var p) r"
    1.81 +  "_var _" => "wild_pat"
    1.82 +
    1.83 +parse_translation {*
    1.84 +  let
    1.85 +    fun capp (t,u) = Syntax.const "Rep_CFun" $ t $ u;
    1.86 +    fun cabs (x,t) = (snd (mk_binder_tr ("_cabs", "Abs_CFun"))) [x,t];
    1.87 +
    1.88 +    fun get_vars (Const ("_var",_) $ x) = [x]
    1.89 +    |   get_vars (t $ u) = get_vars t @ get_vars u
    1.90 +    |   get_vars t = [];
    1.91 +
    1.92 +    fun rem_vars (Const ("_var",_) $ x) = Syntax.const "var_pat"
    1.93 +    |   rem_vars (t $ u) = rem_vars t $ rem_vars u
    1.94 +    |   rem_vars t = t;
    1.95 +
    1.96 +    fun match_tr [pat, rhs] =
    1.97 +          capp (rem_vars pat, foldr cabs rhs (get_vars pat))
    1.98 +    |   match_tr ts = raise TERM ("match_tr", ts);
    1.99 +
   1.100 +  in [("_match", match_tr)] end;
   1.101 +*}
   1.102 +
   1.103 +text {* Printing Case expressions *}
   1.104 +
   1.105 +translations
   1.106 +  "_" <= "_pat wild_pat"
   1.107 +  "x" <= "_pat (_var x)"
   1.108  
   1.109 -lemma run_fatbar1: "m\<cdot>x = \<bottom> \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = \<bottom>"
   1.110 -by (simp add: fatbar_def)
   1.111 +print_translation {*
   1.112 +  let
   1.113 +    fun dest_cabs (Const ("Abs_CFun",_) $ t) =
   1.114 +          let val abs = case t of Abs abs => abs
   1.115 +                  | _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
   1.116 +          in atomic_abs_tr' abs end
   1.117 +    |   dest_cabs _ = raise Match; (* too few vars: abort translation *)
   1.118  
   1.119 -lemma run_fatbar2: "m\<cdot>x = fail \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = run\<cdot>(ms\<cdot>x)"
   1.120 -by (simp add: fatbar_def)
   1.121 +    fun put_vars (Const ("var_pat",_), rhs) =
   1.122 +          let val (x, rhs') = dest_cabs rhs;
   1.123 +          in (Syntax.const "_var" $ x, rhs') end
   1.124 +    |   put_vars (t $ u, rhs) =
   1.125 +          let
   1.126 +            val (t', rhs') = put_vars (t,rhs);
   1.127 +            val (u', rhs'') = put_vars (u,rhs');
   1.128 +          in (t' $ u', rhs'') end
   1.129 +    |   put_vars (t, rhs) = (t, rhs);
   1.130  
   1.131 -lemma run_fatbar3: "m\<cdot>x = return\<cdot>y \<Longrightarrow> run\<cdot>((m \<parallel> ms)\<cdot>x) = y"
   1.132 -by (simp add: fatbar_def)
   1.133 +    fun Case1_tr' (_ $ pat $ rhs) = let
   1.134 +          val (pat', rhs') = put_vars (pat, rhs);
   1.135 +        in Syntax.const "_Case1" $ (Syntax.const "_pat" $ pat') $ rhs' end;
   1.136  
   1.137 -lemmas run_fatbar_simps [simp] = run_fatbar1 run_fatbar2 run_fatbar3
   1.138 +    fun Case2_tr' (_ $ (_ $ Const ("fatbar",_) $ m) $ ms) =
   1.139 +          Syntax.const "_Case2" $ Case1_tr' m $ Case2_tr' ms
   1.140 +    |   Case2_tr' t = Case1_tr' t;
   1.141 +
   1.142 +    fun Case_syntax_tr' [Const ("run",_), _ $ ms $ x] =
   1.143 +          Syntax.const "_Case_syntax" $ x $ Case2_tr' ms;
   1.144 +
   1.145 +  in [("Rep_CFun", Case_syntax_tr')] end;
   1.146 +*}
   1.147  
   1.148  subsection {* Pattern combinators for built-in types *}
   1.149  
   1.150  constdefs
   1.151 -  cpair_pat :: "_"
   1.152 +  cpair_pat :: "('a, _, _) pat \<Rightarrow> ('b, _, _) pat \<Rightarrow> ('a \<times> 'b, _, _) pat"
   1.153    "cpair_pat p1 p2 \<equiv> \<Lambda> r1 \<langle>x1,x2\<rangle>. bind\<cdot>(p1\<cdot>r1\<cdot>x1)\<cdot>(\<Lambda> r2. p2\<cdot>r2\<cdot>x2)"
   1.154  
   1.155 -  spair_pat :: "_"
   1.156 +  spair_pat :: "(_, _, _) pat \<Rightarrow> (_, _, _) pat \<Rightarrow> (_, _, _) pat"
   1.157    "spair_pat p1 p2 \<equiv> \<Lambda> r (:x,y:). cpair_pat p1 p2\<cdot>r\<cdot>\<langle>x,y\<rangle>"
   1.158  
   1.159 -  sinl_pat :: "_"
   1.160 +  sinl_pat :: "(_, _, _) pat \<Rightarrow> (_, _, _) pat"
   1.161    "sinl_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x | sinr\<cdot>y \<Rightarrow> fail"
   1.162  
   1.163 -  sinr_pat :: "_"
   1.164 +  sinr_pat :: "(_, _, _) pat \<Rightarrow> (_, _, _) pat"
   1.165    "sinr_pat p \<equiv> \<Lambda> r a. case a of sinl\<cdot>x \<Rightarrow> fail | sinr\<cdot>y \<Rightarrow> p\<cdot>r\<cdot>y"
   1.166  
   1.167 -  up_pat :: "_"
   1.168 +  up_pat :: "('a, _, _) pat \<Rightarrow> ('a u, _, _) pat"
   1.169    "up_pat p \<equiv> \<Lambda> r a. case a of up\<cdot>x \<Rightarrow> p\<cdot>r\<cdot>x"
   1.170  
   1.171 -  Def_pat :: "'a::type \<Rightarrow> ('a lift, 'b, 'b) pattern"
   1.172 +  Def_pat :: "'a::type \<Rightarrow> ('a lift, _, _) pat"
   1.173    "Def_pat x \<equiv> \<Lambda> r. FLIFT y. if x = y then return\<cdot>r else fail"
   1.174  
   1.175 -  ONE_pat :: "_"
   1.176 +  ONE_pat :: "(one, _, _) pat"
   1.177    "ONE_pat \<equiv> \<Lambda> r ONE. return\<cdot>r"
   1.178  
   1.179 -  TT_pat :: "(tr, _, _) pattern"
   1.180 +  TT_pat :: "(tr, _, _) pat"
   1.181    "TT_pat \<equiv> \<Lambda> r b. If b then return\<cdot>r else fail fi"
   1.182  
   1.183 -  FF_pat :: "(tr, _, _) pattern"
   1.184 +  FF_pat :: "(tr, _, _) pat"
   1.185    "FF_pat \<equiv> \<Lambda> r b. If b then fail else return\<cdot>r fi"
   1.186  
   1.187 -translations
   1.188 -  "_matches cpair (_match (p1\<cdot>r)) (_cons p2 _nil)"
   1.189 -    == "_match ((cpair_pat p1 p2)\<cdot>r)"
   1.190 -
   1.191 -  "_matches spair (_match (p1\<cdot>r)) (_cons p2 _nil)"
   1.192 -    == "_match ((spair_pat p1 p2)\<cdot>r)"
   1.193 -
   1.194 +text {* Parse translations *}
   1.195  translations
   1.196 -  "_matches sinl (_match (p1\<cdot>r)) _nil" == "_match ((sinl_pat p1)\<cdot>r)"
   1.197 -  "_matches sinr (_match (p1\<cdot>r)) _nil" == "_match ((sinr_pat p1)\<cdot>r)"
   1.198 -  "_matches up (_match (p1\<cdot>r)) _nil" == "_match ((up_pat p1)\<cdot>r)"
   1.199 +  "_var (cpair\<cdot>p1\<cdot>p2)" => "cpair_pat (_var p1) (_var p2)"
   1.200 +  "_var (spair\<cdot>p1\<cdot>p2)" => "spair_pat (_var p1) (_var p2)"
   1.201 +  "_var (sinl\<cdot>p1)"     => "sinl_pat (_var p1)"
   1.202 +  "_var (sinr\<cdot>p1)"     => "sinr_pat (_var p1)"
   1.203 +  "_var (up\<cdot>p1)"       => "up_pat (_var p1)"
   1.204 +  "_var (Def x)"       => "Def_pat x"
   1.205 +  "_var ONE"           => "ONE_pat"
   1.206 +  "_var TT"            => "TT_pat"
   1.207 +  "_var FF"            => "FF_pat"
   1.208  
   1.209 +text {* Print translations *}
   1.210  translations
   1.211 -  "_Case1 (Def x) r" == "_match (Def_pat x\<cdot>r)"
   1.212 -  "_Case1 ONE r" == "_match (ONE_pat\<cdot>r)"
   1.213 -  "_Case1 TT r" == "_match (TT_pat\<cdot>r)"
   1.214 -  "_Case1 FF r" == "_match (FF_pat\<cdot>r)"
   1.215 +  "cpair\<cdot>(_pat p1)\<cdot>(_pat p2)" <= "_pat (cpair_pat p1 p2)"
   1.216 +  "spair\<cdot>(_pat p1)\<cdot>(_pat p2)" <= "_pat (spair_pat p1 p2)"
   1.217 +  "sinl\<cdot>(_pat p1)"            <= "_pat (sinl_pat p1)"
   1.218 +  "sinr\<cdot>(_pat p1)"            <= "_pat (sinr_pat p1)"
   1.219 +  "up\<cdot>(_pat p1)"              <= "_pat (up_pat p1)"
   1.220 +  "Def x"                     <= "_pat (Def_pat x)"
   1.221 +  "TT"                        <= "_pat (TT_pat)"
   1.222 +  "FF"                        <= "_pat (FF_pat)"
   1.223  
   1.224  lemma cpair_pat_simps [simp]:
   1.225    "p1\<cdot>r\<cdot>x = \<bottom> \<Longrightarrow> cpair_pat p1 p2\<cdot>r\<cdot><x,y> = \<bottom>"
   1.226 @@ -303,6 +356,23 @@
   1.227    "FF_pat\<cdot>r\<cdot>FF = return\<cdot>r"
   1.228  by (simp_all add: FF_pat_def)
   1.229  
   1.230 +subsection {* As-patterns *}
   1.231 +
   1.232 +syntax
   1.233 +  "_as_pattern" :: "['a, 'a] \<Rightarrow> 'a" (* infixr "as" 10 *)
   1.234 +  (* TODO: choose a non-ambiguous syntax for as-patterns *)
   1.235 +
   1.236 +constdefs
   1.237 +  as_pat :: "('a,'b,'c) pat \<Rightarrow> ('a,'c,'d) pat \<Rightarrow> ('a,'b,'d) pat"
   1.238 +  "as_pat p1 p2 \<equiv> \<Lambda> r a. cpair_pat p1 p2\<cdot>r\<cdot>\<langle>a, a\<rangle>"
   1.239 +
   1.240 +translations
   1.241 +  "_var (_as_pattern p1 p2)" => "as_pat (_var p1) (_var p2)"
   1.242 +  "_as_pattern (_pat p1) (_pat p2)" <= "_pat (as_pat p1 p2)"
   1.243 +
   1.244 +lemma as_pat [simp]: "as_pat p1 p2\<cdot>r\<cdot>a = cpair_pat p1 p2\<cdot>r\<cdot>\<langle>a, a\<rangle>"
   1.245 +by (simp add: as_pat_def)
   1.246 +
   1.247  subsection {* Match functions for built-in types *}
   1.248  
   1.249  defaultsort pcpo