eval match: simplify equality of two constructors

src/transform/eval_match.ml

@@ -46,7 +46,7 @@ let is_projection kn ls = match Mid.find ls.ls_name kn with
       not (List.exists constr dl)
   | _ -> false
 
-let apply_projection kn ls t = t_label_copy t (match t.t_node with
+let apply_projection kn ls t = match t.t_node with
   | Tapp (cs,tl) ->
       let ts = match cs.ls_value with
         | Some { ty_node = Tyapp (ts,_) } -> ts
@@ -58,7 +58,7 @@ let apply_projection kn ls t = t_label_copy t (match t.t_node with
         | Some pj when ls_equal pj ls -> v
         | _ -> acc in
       List.fold_left2 find t_true tl pjl
-  | _ -> assert false)
+  | _ -> assert false
 
 let make_flat_case kn t bl =
   let mk_b b = let p,t = t_open_branch b in [p],t in
@@ -104,8 +104,27 @@ let dive_to_constructor kn fn env t =
   in
   dive env t
 
+let rec cs_equ kn env t1 t2 =
+  if t_equal t1 t2 then t_true
+  else match t1,t2 with
+    | { t_node = Tapp (cs,tl) }, t
+    | t, { t_node = Tapp (cs,tl) } when is_constructor kn cs ->
+        let fn = apply_cs_equ kn cs tl in
+        begin try dive_to_constructor kn fn env t
+        with Exit -> t_equ t1 t2 end
+    | _ -> t_equ t1 t2
+
+and apply_cs_equ kn cs1 tl1 env t = match t.t_node with
+  | Tapp (cs2,tl2) when ls_equal cs1 cs2 ->
+      let merge f t1 t2 = t_and_simp f (cs_equ kn env t1 t2) in
+      List.fold_left2 merge t_true tl1 tl2
+  | Tapp _ -> t_false
+  | _ -> assert false
+
 let eval_match ~inline kn t =
   let rec eval env t = t_label_copy t (match t.t_node with
+    | Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
+        cs_equ kn env (eval env t1) (eval env t2)
     | Tapp (ls, [t1]) when is_projection kn ls ->
         let t1 = eval env t1 in
         let fn _env t = apply_projection kn ls t in