path: root/lib/vm.mli

(** The solver: proof search over an admitted world.

    Functorized over {!World.WORLD} (decision 4): the standalone
    binary instantiates it with {!World.Standalone}; RNT instantiates
    it with its own catalog and links the same engine in-process.

    Execution is dynamic goal selection: at each step the engine
    runs any goal that is decidable at the current bindings, so
    conjunction stays honestly commutative and order on the page
    means nothing. A conjunction where no goal can ever run (an
    unbounded membership, an unbounded recursion) is rejected as a
    non-total plan, never attempted. Together with admission-time
    rule checking, this is what makes every accepted query
    terminate. *)

type error =
  | Non_total_plan of string list
      (** No remaining goal is decidable; 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

module Make (W : World.WORLD) : sig
  val solve : W.t -> World.expr -> (solution list, error) result
  (** All answers to the query, duplicates collapsed. Total: the
      world was admitted, so search terminates; the only failure is
      a plan the engine refuses to run. *)
end

module Standalone : sig
  val solve : World.Standalone.t -> World.expr -> (solution list, error) result
end