blob: 6ce3f9348f998541cdabf21f4ace78a42a569866 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
(** 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
|
