Eval_match: treat equality modulo let-bindings

src/mlw/eval_match.ml

@@ -34,19 +34,17 @@ let find_logic_definition kn ({ls_name = id} as ls) =
     | _ -> None in
   find (Mid.find id kn).pd_pure
 
-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
-        | _ -> assert false in
-      let pjl =
-        try List.assq cs (find_constructors kn ts)
-        with Not_found -> assert false in
-      let find acc v = function
-        | Some pj when ls_equal pj ls -> v
-        | _ -> acc in
-      List.fold_left2 find t_true tl pjl
-  | _ -> assert false
+let apply_projection kn ls cs tl =
+  let ts = match cs.ls_value with
+    | Some { ty_node = Tyapp (ts,_) } -> ts
+    | _ -> assert false in
+  let pjl =
+    try List.assq cs (find_constructors kn ts)
+    with Not_found -> assert false in
+  let find acc v = function
+    | Some pj when ls_equal pj ls -> v
+    | _ -> acc in
+  List.fold_left2 find t_true tl pjl
 
 let flat_case t bl =
   let mk_b b = let p,t = t_open_branch b in [p],t in
@@ -114,33 +112,25 @@ let branch_map fn env t1 bl =
     let p,t2,close = t_open_branch_cb b in close p (fn env t2) in
   t_case t1 (List.map mk_b bl)
 
-let dive_to_constructor fn env t =
-  let rec dive env t = t_label_copy t (match t.t_node with
+let rec dive_to_constructor fn env t =
+  let dive env t = dive_to_constructor fn env t in
+  t_label_copy t (match t.t_node with
     | Tvar x -> dive env (Mvs.find_exn Exit x env)
     | Tlet (t1,tb) -> let_map dive env t1 tb
     | Tcase (t1,bl) -> branch_map dive env t1 bl
     | Tif (f,t1,t2) -> t_if_simp f (dive env t1) (dive env t2)
-    | Tapp (ls,_) when ls.ls_constr > 0 -> fn env t
+    | Tapp (ls,tl) when ls.ls_constr > 0 -> fn env t ls tl
     | _ -> raise Exit)
-  in
-  dive env t
 
 let rec cs_equ 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 cs.ls_constr > 0 ->
-        let fn = apply_cs_equ cs tl in
-        begin try dive_to_constructor fn env t
-        with Exit -> t_equ t1 t2 end
-    | _ -> t_equ t1 t2
-
-and apply_cs_equ cs1 tl1 env t = match t.t_node with
-  | Tapp (cs2,tl2) when ls_equal cs1 cs2 ->
-      let merge t1 t2 f = t_and_simp (cs_equ env t1 t2) f in
-      List.fold_right2 merge tl1 tl2 t_true
-  | Tapp _ -> t_false
-  | _ -> assert false
+  if t_equal t1 t2 then t_true else
+  let right cs1 tl1 env _t2 cs2 tl2 =
+    if not (ls_equal cs1 cs2) then t_false else
+    t_and_simp_l (List.map2 (cs_equ env) tl1 tl2) in
+  let left t2 env _t1 cs1 tl1 =
+    dive_to_constructor (right cs1 tl1) env t2 in
+  try dive_to_constructor (left t2) env t1
+  with Exit -> t_equ t1 t2
 
 let rec eval_match kn stop env t =
   let stop = stop || Slab.mem Term.stop_split t.t_label in
@@ -150,7 +140,7 @@ let rec eval_match kn stop env t =
         cs_equ 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
+        let fn _env _t2 cs tl = apply_projection kn ls cs tl in
         begin try dive_to_constructor fn env t1
         with Exit -> t_app ls [t1] t.t_ty end
     | Tapp (ls, tl) ->
@@ -163,7 +153,8 @@ let rec eval_match kn stop env t =
         let_map eval env t1 tb2
     | Tcase (t1, bl1) ->
         let t1 = eval env t1 in
-        let fn env t2 = eval env (Loc.try2 ?loc:t.t_loc flat_case t2 bl1) in
+        let fn env t2 _cs _tl =
+          eval env (Loc.try2 ?loc:t.t_loc flat_case t2 bl1) in
         begin try dive_to_constructor fn env t1
         with Exit -> branch_map eval env t1 bl1 end
     | Tquant (q, qf) ->