Changeset 2883 for src/ERTLptr/liveness.ma

Timestamp:

Mar 15, 2013, 6:33:18 PM (8 years ago)

Author:

piccolo

Message:

partial commit

File:

• src/ERTLptr/liveness.ma (modified) (1 diff)

src/ERTLptr/liveness.ma

@@ -26 +26 @@
     〈set_empty …, set_singleton … r〉.
 
-definition rl_join: register_lattice → register_lattice → register_lattice ≝
-  λleft.
-  λright.
-  let 〈lp, lh〉 ≝ left in
-  let 〈rp, rh〉 ≝ right in
-    〈set_union … lp rp, set_union … lh rh〉.
+definition pairwise : ∀A,B : Type[0]. ∀f : A → A → A. ∀g: B → B → B.
+A × B → A × B → A × B≝
+λA,B,f,g,c1,c2.〈f (\fst c1) (\fst c2) , g (\snd c1) (\snd c2)〉.
+
+definition rl_join: register_lattice → register_lattice → register_lattice ≝ 
+pairwise ?? (set_union …) (set_union …).
 
 definition rl_diff: register_lattice → register_lattice → register_lattice ≝
-  λleft.
-  λright.
-  let 〈lp, lh〉 ≝ left in
-  let 〈rp, rh〉 ≝ right in
-    〈set_diff … lp rp, set_diff … lh rh〉.
+pairwise ?? (set_diff …) (set_diff …).
 
 definition defined ≝