reinstated previous forward_move function

1 files changed, 28 insertions, 3 deletions

diff --git a/backend/CSE3analysis.v b/backend/CSE3analysis.v
index 34df644e..dbf1afe2 100644
--- a/backend/CSE3analysis.v
+++ b/backend/CSE3analysis.v
@@ -236,7 +236,30 @@ Section OPERATIONS.
     | nil => before
     end.
 
-  Definition pick_source (l : list reg) :=
+  Definition pick_source (l : list reg) := (* todo: take min? *)
+    match l with
+    | h::t => Some h
+    | nil => None
+    end.
+  
+  Definition forward_move1 (rel : RELATION.t)  (x : reg) : reg :=
+    match pick_source (PSet.elements (PSet.inter rel (eq_moves ctx x))) with
+    | None => x
+    | Some eqno =>
+      match eq_catalog ctx eqno with
+      | Some eq =>
+        if is_smove (eq_op eq) && peq x (eq_lhs eq)
+        then
+          match eq_args eq with
+          | src::nil => src
+          | _ => x
+          end
+        else x
+      | _ => x
+      end
+    end.
+
+  Definition pick_min_source (l : list reg) :=
     match l with
     | h::t => Some (reg_min_rec t h)
     | nil => None
@@ -259,11 +282,13 @@ Section OPERATIONS.
       end
     end.
       
-  Definition forward_move (rel : RELATION.t)  (x : reg) : reg :=
-    match pick_source (get_sources x (PSet.elements (PSet.inter rel (eq_moves ctx x)))) with
+  Definition forward_move2 (rel : RELATION.t)  (x : reg) : reg :=
+    match pick_min_source (get_sources x (PSet.elements (PSet.inter rel (eq_moves ctx x)))) with
     | None => x
     | Some src => src
     end.
+
+  Definition forward_move := forward_move1.
   
   Definition forward_move_l (rel : RELATION.t) : list reg -> list reg :=
     List.map (forward_move rel).