Minor fixes for sim

- handle M.f(x, y) vs M.f((x, y)) cases
- allow matching local operators

Author: Cameron-Low

src/ecPV.ml

@@ -942,7 +942,8 @@ module Mpv2 = struct
       let local = enter_local env local bds1 bds2 in
       add_eqs_loc env local eqs e1 e2
     | Eint i1, Eint i2 when EcBigInt.equal i1 i2 -> eqs
-    | Elocal x1, Elocal x2 when
+    | Elocal x1, Elocal x2
+     when EcIdent.id_equal x1 x2 ||
         opt_equal EcIdent.id_equal (Some x1) (Mid.find_opt x2 local) -> eqs
     | Evar pv1, Evar pv2
       when EcReduction.EqTest.for_type env e1.e_ty e2.e_ty ->

src/phl/ecPhlEqobs.ml

@@ -218,15 +218,30 @@ and i_eqobs_in il ir sim local (eqo:Mpv2.t) =
   | Sasgn(lvl,el), Sasgn(lvr,er) | Srnd(lvl,el), Srnd(lvr,er) ->
     sim, add_eqs sim local (remove sim lvl lvr eqo) el er
 
-  | Scall(lvl,fl,argsl), Scall(lvr,fr,argsr)
-    when List.length argsl = List.length argsr ->
+  | Scall(lvl,fl,argsl), Scall(lvr,fr,argsr) ->
     let eqo = oremove sim lvl lvr eqo in
     let env = sim.sim_env in
     let modl, modr = f_write env fl, f_write env fr in
     let eqnm = Mpv2.split_nmod env modl modr eqo in
     let outf = Mpv2.split_mod  env modl modr eqo in
     Mpv2.check_glob outf;
     let sim, eqi = f_eqobs_in fl fr sim outf in
+
+    let argsl, argsr =
+      match argsl, argsr with
+      | _, _ when List.length argsl = List.length argsr -> argsl, argsr
+      | [al], _ -> begin
+        match al.e_node with
+        | Etuple argsl -> argsl, argsr
+        | _ -> raise EqObsInError
+      end
+      | _, [ar] -> begin
+        match ar.e_node with
+        | Etuple argsr -> argsl, argsr
+        | _ -> raise EqObsInError
+      end
+      | _ -> raise EqObsInError
+    in
     let eqi = List.fold_left2 (add_eqs sim local) (Mpv2.union eqnm eqi) argsl argsr in
     sim, eqi