Extract common statements from Either

spectec/src/backend-prose/dune

@@ -8,5 +8,6 @@
     gen
     render
     macro
-    langs)
+    langs
+    eq)
 )

spectec/src/backend-prose/eq.ml

@@ -0,0 +1,43 @@
+open Prose
+
+let eq_list eq l1 l2 =
+  List.length l1 = List.length l2
+  && List.for_all2 eq l1 l2
+
+let eq_cmpop = (=)
+
+let eq_expr = Al.Eq.eq_expr
+
+let rec eq_instr i1 i2 =
+  match (i1, i2) with
+  | LetI (e11, e12), LetI (e21, e22) ->
+      eq_expr e11 e21
+      && eq_expr e12 e22
+  | CmpI (e11, cmp1, e12), CmpI (e21, cmp2, e22) ->
+      eq_expr e11 e21
+      && eq_cmpop cmp1 cmp2
+      && eq_expr e12 e22
+  | MemI (e11, e12), MemI (e21, e22) ->
+      eq_expr e11 e21 && eq_expr e12 e22
+  | IsValidI (opt1, e11, l1), IsValidI (opt2, e21, l2) ->
+      Option.equal eq_expr opt1 opt2
+      && eq_expr e11 e21
+      && eq_list eq_expr l1 l2
+  | MatchesI (e11, e12), MatchesI (e21, e22) ->
+      eq_expr e11 e21
+      && eq_expr e12 e22
+  | IsConstI (opt1, e11), IsConstI (opt2, e21) ->
+      Option.equal eq_expr opt1 opt2
+      && eq_expr e11 e21
+  | IfI (e11, il1), IfI (e21, il2) ->
+      eq_expr e11 e21
+      && List.for_all2 eq_instr il1 il2
+  | ForallI (l1, il1), ForallI (l2, il2) ->
+      eq_list (fun (e11, e12) (e21, e22) -> eq_expr e11 e21 && eq_expr e12 e22) l1 l2
+      && eq_list eq_instr il1 il2
+  | EquivI (e11, e12), EquivI (e21, e22) ->
+      eq_expr e11 e21
+      && eq_expr e12 e22
+  | EitherI (il1), EitherI (il2) ->
+      eq_list (fun l1 l2 -> eq_list eq_instr l1 l2) il1 il2
+  | _, _ -> i1 = i2

spectec/src/backend-prose/eq.mli

@@ -0,0 +1,3 @@
+open Prose
+
+val eq_instr : instr -> instr -> bool

spectec/src/backend-prose/gen.ml

@@ -1,4 +1,6 @@
 open Prose
+open Eq
+
 open Il
 open Al.Al_util
 open Il2al.Translate
@@ -467,6 +469,46 @@ let prose_of_rel rel = match get_rel_kind rel with
 
 let prose_of_rels = List.concat_map prose_of_rel
 
+(** Postprocess of generated prose **)
+let unify_either instrs =
+  let f instr =
+    match instr with
+    | EitherI iss ->
+      let unified, bodies = List.fold_left (fun (commons, instrss) i ->
+        let pairs = List.map (List.partition (eq_instr i)) instrss in
+        let fsts = List.map fst pairs in
+        let snds = List.map snd pairs in
+        if List.for_all (fun l -> List.length l = 1) fsts then
+          i :: commons, snds
+        else
+          commons, instrss
+      ) ([], iss) (List.hd iss) in
+      let unified = List.rev unified in
+      unified @ [ EitherI bodies ]
+    | _ -> [instr]
+  in
+  let rec walk instrs = List.concat_map walk' instrs
+  and walk' instr =
+    f instr
+    |> List.map (function
+      | IfI (e, il) -> IfI (e, walk il)
+      | ForallI (vars, il) -> ForallI (vars, walk il)
+      | EitherI ill -> EitherI (List.map walk ill)
+      | i -> i
+    )
+  in
+  walk instrs
+
+let postprocess_prose defs =
+  List.map (fun def ->
+    match def with
+    | Iff (anchor, e, i, il) ->
+      let new_il = unify_either il in
+      Iff (anchor, e, i, new_il)
+    | Algo _ -> def
+  ) defs
+
+
 (** Entry for generating validation prose **)
 let gen_validation_prose () =
   prose_of_rels !Langs.il
@@ -494,6 +536,7 @@ let gen_prose el il al =
   let execution_prose = gen_execution_prose () in
 
   validation_prose @ execution_prose
+  |> postprocess_prose
 
 (** Main entry for generating stringified prose **)
 let gen_string cfg_latex cfg_prose el il al =