path: root/lib/program.mli

(** Whole-program admission: the entry point hosts use.

    The loader admits what it can decide alone; membership criteria
    need the solver, so this module finishes admission by running
    every pending criterion against the fully loaded world. Order of
    facts in the source does not matter: integrity is judged against
    the complete extension, the way a committed state would be. *)

type error =
  | Load of World.error
  | Integrity of { relation : string; label : string }
      (** A fact's attribute failed its membership criterion. *)
  | Undecidable_criterion of { relation : string; label : string }
      (** The criterion's plan was rejected as non-total. *)

val pp_error : Format.formatter -> error -> unit

val load :
  Ast.statement list -> (World.Standalone.t * World.expr list, error) result
(** Parses nothing and solves queries for nobody: admits. Returns
    the world and the query expressions, ready for
    {!Vm.Standalone.solve}. *)