residuation: open membership returns residual constraints

1 files changed, 19 insertions, 6 deletions

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