From 0886f3c71cf8551e4f8b3726654003a4f29645f0 Mon Sep 17 00:00:00 2001
From: Marcos Magueta <maguetamarcos@gmail.com>
Date: Sat, 11 Jul 2026 22:12:53 -0300
Subject: residuation: open membership returns residual constraints

---
 lib/vm.mli | 25 +++++++++++++++++++------
 1 file changed, 19 insertions(+), 6 deletions(-)

(limited to 'lib/vm.mli')

diff --git a/lib/vm.mli b/lib/vm.mli
index 6ce3f93..4c91be2 100644
--- a/lib/vm.mli
+++ b/lib/vm.mli
@@ -15,15 +15,28 @@
 
 type error =
   | Non_total_plan of string list
-      (** No remaining goal is decidable; the relation names of the
-          stuck goals, for the message. *)
+      (** No remaining goal is decidable or residuatable; the
+          relation names of the stuck goals, for the message. *)
 
 val pp_error : Format.formatter -> error -> unit
 
-(** One answer: each free variable of the query, resolved. Ground in
-    the common case; open exactly when the query admits any value
-    there. *)
-type solution = (string * Pattern.t) list
+(** A residual constraint: a membership goal that stayed
+    underdetermined. It is decidable the moment its variables are
+    ground; returning it is the honest answer to a satisfiable but
+    open query. Only builtin membership residuates; searches never
+    do. *)
+type residual = string * Pattern.t Label.Map.t
+
+val pp_residual : Format.formatter -> residual -> unit
+(** Prints the constraint as the proposition it is, [[Rel l: t ...]]. *)
+
+(** One answer: each free variable of the query resolved, plus the
+    residual constraints the answer is conditioned on. Ground and
+    residue-free in the common case. *)
+type solution = {
+  bindings : (string * Pattern.t) list;
+  residue : residual list;
+}
 
 module Make (W : World.WORLD) : sig
   val solve : W.t -> World.expr -> (solution list, error) result
-- 
cgit v1.2.3