Use reductive equality tests, and destruct the last matching operator

Author: Cameron-Low

src/phl/ecPhlEager.ml

@@ -96,7 +96,7 @@ let destruct_on_op id_op tc =
   let env = FApi.tc1_env tc and es = tc1_as_equivS tc in
   let s =
     try
-      let s, _ = split_at_cpos1 env (-1, `ByMatch (None, id_op)) es.es_sl
+      let s, _ = split_at_cpos1 env (-1, `ByMatch (Some (-1), id_op)) es.es_sl
       (* ensure the right statement also contains an [id_op]: *)
       and _, _ = split_at_cpos1 env (1, `ByMatch (None, id_op)) es.es_sr in
       s
@@ -237,7 +237,7 @@ let t_eager_while_r i tc =
     subst_expr (add_memory empty mr ml)
   in
 
-  if (not (e_equal e (sub_to_left_mem _e))) then
+  if (not (ER.EqTest.for_expr env e (sub_to_left_mem _e))) then
     tc_error !!tc "eager: both while guards must be syntactically equal";
 
   let eqMem1 = eq_on_form_and_stmt env i c' and eqI = eq_on_sided_form env i in
@@ -317,7 +317,7 @@ let t_eager_fun_def_r tc =
 let t_eager_fun_abs_r i tc =
   let env, _, _ = FApi.tc1_eflat tc and eg = tc1_as_eagerF tc in
 
-  if not (s_equal eg.eg_sl eg.eg_sr) then
+  if not (ER.EqTest.for_stmt env eg.eg_sl eg.eg_sr) then
     tc_error !!tc "eager: both swapping statements must be identical";
 
   if not (ensure_eq_shape tc i.ml i.mr i.inv) then

tests/eager-lastop.ec

@@ -0,0 +1,45 @@
+module DoubleIf = {
+    proc f() = {
+        var x: int;
+
+        if ((fun x => x) true) {}
+        x <- 0;
+        if (false) {}
+    }
+    proc g() = {
+        var x: int;
+
+        if (false) {}
+        if (true) {}
+        x <- 0;
+    }
+}.
+
+equiv dif: DoubleIf.f ~ DoubleIf.g: true ==> true.
+proof.
+proc.
+eager if; expect 4.
+abort.
+
+module DoubleWhile = {
+    proc f() = {
+        var x: int;
+
+        x <- 0;
+        while ((fun x => x) true) {}
+        while (false) {}
+    }
+    proc g() = {
+        var x: int;
+
+        while (false) {}
+        x <- 0;
+        while (true) {}
+    }
+}.
+
+equiv dwl: DoubleWhile.f ~ DoubleWhile.g: true ==> true.
+proof.
+proc.
+eager while (true); expect 6.
+abort.