merge two sides

Author: namasikanam

src/phl/ecPhlRnd.ml

@@ -463,7 +463,7 @@ module Core = struct
         let goal = f_imp (f_in_supp ab g_app) post_subst in
         let goal = f_forall_simpl [(a_id, GTty tyL); (b_id, GTty tyR)] goal in
         f_and iscoupling_pred goal
-      | Some `Left  ->
+      | Some side ->
         (* Goal: dmap d1 g = d2 /\ forall a b, b = g(a) => psi[x -> a, y -> b] *)
         let dmap_op = EcPath.extend EcCoreLib.p_top ["Distr"; "dmap"] in
         let dmap_ty = tfun (tdistr tyL) (tfun (tfun tyL tyR) (tdistr tyR)) in
@@ -477,24 +477,12 @@ module Core = struct
         let post_subst = subst_form_lv env (EcMemory.memory es.es_ml) lvL a post in
         let post_subst = subst_form_lv env (EcMemory.memory es.es_mr) lvR b post_subst in
 
-        let goal = f_imp (f_eq (f_app_simpl g [a] tyR) b) post_subst in
-        let goal = f_forall_simpl [(a_id, GTty tyL); (b_id, GTty tyR)] goal in
-        f_and dmap_pred goal
-      | Some `Right ->
-        (* Goal: dmap d2 g = d1 /\ forall a b, a = g(b) => psi[x -> a, y -> b] *)
-        let dmap_op = EcPath.extend EcCoreLib.p_top ["Distr"; "dmap"] in
-        let dmap_ty = tfun (tdistr tyR) (tfun (tfun tyR tyL) (tdistr tyL)) in
-        let dmap_pred = f_eq (f_app (f_op dmap_op [tyR; tyL] dmap_ty) [muR; g] tyL) muL in
-
-        let a_id = EcIdent.create "a" in
-        let b_id = EcIdent.create "b" in
-        let a = f_local a_id tyL in
-        let b = f_local b_id tyR in
-        let post = es.es_po in
-        let post_subst = subst_form_lv env (EcMemory.memory es.es_ml) lvL a post in
-        let post_subst = subst_form_lv env (EcMemory.memory es.es_mr) lvR b post_subst in
+        let eq_condition = 
+          match side with
+          | `Left  -> f_eq (f_app_simpl g [a] tyR) b
+          | `Right -> f_eq a (f_app_simpl g [b] tyL) in
 
-        let goal = f_imp (f_eq a (f_app_simpl g [b] tyL)) post_subst in
+        let goal = f_imp eq_condition post_subst in
         let goal = f_forall_simpl [(a_id, GTty tyL); (b_id, GTty tyR)] goal in
         f_and dmap_pred goal
     in