diff options
Diffstat (limited to 'lib/vm.mli')
| -rw-r--r-- | lib/vm.mli | 25 |
1 files changed, 19 insertions, 6 deletions
@@ -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 |