From 08259f116c89b5ba28c46a8dcd7af4ea567539a1 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Fri, 14 Feb 2025 09:44:13 +0100
Subject: [PATCH] Revert "Propagate context in Adt_rel"

This reverts commit 4fb7fffda7c0c384c5a369d1a82ab1f043d1c578.
---
 src/lib/reasoners/adt.ml      |  2 +-
 src/lib/reasoners/adt_rel.ml  | 40 +++++++++--------------------------
 src/lib/reasoners/matching.ml | 33 +++++++++++++++++++++++++++--
 3 files changed, 42 insertions(+), 33 deletions(-)

diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
index 522b94306..2d0693983 100644
--- a/src/lib/reasoners/adt.ml
+++ b/src/lib/reasoners/adt.ml
@@ -194,7 +194,7 @@ module Shostak (X : ALIEN) = struct
       let ctx =
         (* If [t] is a record constructor term of the form
              { x1 = t1; ...; xn = t2 }
-           we generate the equations
+           we generate the equation
              t.x1 = t1, ..., t.xn = tn
            and store them in the context returned by `X.make`. *)
         match cases with
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index 87a5344ec..2dbdda111 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -482,21 +482,8 @@ let build_constr_eq r c =
             CC(X) via [Ccx.add_term]. Since .ki are fresh terms, adding these
             facts could not contribute to any meaningful reasoning. *)
         let r', _ctx = X.make cons in
-        let eqs = [Shostak.L.(view @@ mk_eq r r')] in
-        let eqs =
-          match cases with
-          | [{ destrs; _ }] ->
-            List.fold_left2
-              (fun eqs x (d, d_ty) ->
-                 let access, _ =
-                   X.make @@ E.mk_term (Sy.destruct d) [cons] d_ty
-                 in
-                 let tx, _ = X.make x in
-                 Shostak.L.(view @@ mk_eq tx access) :: eqs
-              ) eqs xs destrs
-          | _ -> eqs
-        in
-        Some (eqs, cons)
+        let eq = Shostak.L.(view @@ mk_eq r r') in
+        Some (eq, cons)
 
       | _ -> assert false
     end
@@ -515,12 +502,9 @@ let propagate_domains new_terms domains =
        match Domain.as_singleton d with
        | Some (c, ex) ->
          begin match build_constr_eq rr c with
-           | Some (eqs, cons) ->
+           | Some (eq, cons) ->
              let new_terms = SE.add cons new_terms in
-             let eqs =
-               List.map (fun eq -> (Literal.LSem eq, ex, Th_util.Other)) eqs
-             in
-             eqs, new_terms
+             (Literal.LSem eq, ex, Th_util.Other) :: eqs, new_terms
            | None ->
              eqs, new_terms
          end
@@ -653,17 +637,16 @@ let pick_domain ~for_model uf =
 
 let split_domain ~for_model env uf =
   let* cd, r, c = pick_domain ~for_model uf in
-  if for_model || can_split env (Numbers.Q.from_int cd) then (
-    (*     assert for_model; None) *)
-    let eqs, _ = Option.get @@ build_constr_eq r c in
-    Some eqs)
+  if for_model || can_split env (Numbers.Q.from_int cd) then
+    let eq, _ = Option.get @@ build_constr_eq r c in
+    Some eq
   else
     None
 
 let next_case_split ~for_model env uf =
   match split_delayed_destructor env with
   | None -> split_domain ~for_model env uf
-  | Some eq -> Some [eq]
+  | r -> r
 
 let case_split env uf ~for_model =
   if Options.get_disable_adts () then
@@ -677,11 +660,8 @@ let case_split env uf ~for_model =
             (Uf.GlobalDomains.find (module Domains) (Uf.domains uf)));
       Log.debug
         (fun k -> k "assume by case splitting:@ %a"
-            Fmt.(braces @@ list ~sep:comma (Xliteral.print_view X.print)) cs);
-      let eqs =
-        List.map (fun eq -> eq, true, Th_util.CS (Th_util.Th_adt, two)) cs
-      in
-      eqs
+            (Xliteral.print_view X.print) cs);
+      [ cs, true, Th_util.CS (Th_util.Th_adt, two)]
     | None ->
       Log.debug (fun k -> k "no case split done");
       []
diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml
index 55e2bf782..df847d1c1 100644
--- a/src/lib/reasoners/matching.ml
+++ b/src/lib/reasoners/matching.ml
@@ -229,6 +229,22 @@ module Make (X : Arg) : S with type theory = X.t = struct
     in
     if info.term_age > age_limite () then env else add_rec env t
 
+  (* let add_term info t env =
+     match E.type_info t with
+     | Tadt (name, args) as ty -> (
+        match Ty.type_body name args with
+        | [{ constr; destrs }] ->
+          let xs =
+            List.map
+              (fun (d, ty) ->
+                  E.mk_term Sy.(Op (Destruct d)) [t] ty
+              ) destrs
+          in
+          let c = E.mk_constr constr xs ty in
+          add_term info c env
+        | _ -> add_term info t env)
+     | _ -> add_term info t env
+  *)
   let add_trigger p env = { env with pats = p :: env.pats }
 
   let all_terms
@@ -367,6 +383,15 @@ module Make (X : Arg) : S with type theory = X.t = struct
         else if E.is_ground p1 then [minus_of_plus t p1 ty] else []
       | _ -> []
 
+  let xs_module_records t name args =
+    let l = Ty.type_body name args in
+    match l with
+    (* | [{ destrs; _ }] ->
+       List.map
+        (fun (d, ty) ->
+          E.mk_term Sy.(Op (Destruct d)) [t] ty) destrs *)
+    | _ -> []
+
   let rec match_term mconf env tbox
       ({ sty = s_ty; gen = g; goal = b; _ } as sg : Matching_types.gsubst)
       pat t =
@@ -405,9 +430,13 @@ module Make (X : Arg) : S with type theory = X.t = struct
           let cl =
             E.Set.fold
               (fun t l ->
-                 let { E.f = f; xs = xs; _ } = E.term_view t in
+                 let { E.f = f; xs = xs; ty; _ } = E.term_view t in
                  if Symbols.compare f_pat f = 0 then xs :: l
-                 else l
+                 else (
+                   match f_pat, ty with
+                   | Sy.(Op Constr _), Ty.Tadt (name, args) ->
+                     (xs_module_records t name args) :: l
+                   | _ -> l)
               ) cl []
           in
           let cl = filter_classes mconf cl tbox in