blob: d7017e382f10a61fba8d51b45f83904c346eea20 (
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
|
(** The builtin relations every world carries.
Builtins are relations with operational capabilities beyond
scanning: they check membership against the host (the domain
relations), evaluate and solve (arithmetic), unify (equality),
and generate boundedly (Between). The VM consults this module
before the world.
A builtin never enumerates an infinite domain. When its
arguments are too unbound to decide, the answer is {!Stuck}, and
the planner tries it again later or rejects the plan; totality
is preserved either way. *)
type outcome =
| Solved of Pattern.Subst.t list
(** Zero or more ways to satisfy the goal. The empty list is
failure. *)
| Stuck
(** Not decidable at the current bindings; retry once more
variables are ground. *)
val is_builtin : string -> bool
(** Whether a name is a builtin. The loader uses it for reference
checking, so user relations cannot shadow builtins. *)
val run : Pattern.Subst.t -> string -> Pattern.t Label.Map.t -> outcome option
(** Executes one builtin goal under the substitution. [None] when
the name is not a builtin, so the VM falls through to the
world. *)
|
