diff options
Diffstat (limited to '')
| -rw-r--r-- | lib/world.ml | 10 | ||||
| -rw-r--r-- | lib/world.mli | 35 |
2 files changed, 39 insertions, 6 deletions
diff --git a/lib/world.ml b/lib/world.ml index a053c2c..94fa0a9 100644 --- a/lib/world.ml +++ b/lib/world.ml @@ -22,10 +22,15 @@ type def = | Table of { schema : (Label.t * domain) list; facts : Term.t Label.Map.t list } | Rules of rule list +type transition_result = T_state of Term.t | T_fail | T_stuck + module type WORLD = sig type t - val find : t -> string -> def option + val find : t -> ?at:Term.t -> string -> def option + + val transition : + t -> string -> Pattern.t Label.Map.t -> transition_result option end type error = @@ -227,7 +232,8 @@ module String_map = Map.Make (String) module Standalone = struct type t = def String_map.t - let find world name = String_map.find_opt name world + let find world ?at:_ name = String_map.find_opt name world + let transition _ _ _ = None let schema_of_node ~relation = function | Ast.Seq (entries, None) -> diff --git a/lib/world.mli b/lib/world.mli index 14f82d3..3868261 100644 --- a/lib/world.mli +++ b/lib/world.mli @@ -56,13 +56,34 @@ type def = (** Extensional: a schema and finite stored tuples. *) | Rules of rule list (** Intensional: defined by admitted rules. *) +val member_of_primitive : Term.t -> primitive -> bool +(** Host-decided membership in a primitive domain, with the literal + inclusions of decision 12. Exposed so stateful worlds check + schemas with exactly the loader's judgment. *) + +(** What a transition relation says when consulted (decision 3: + transitions are relations over states, provided by the world, + never by the engine). *) +type transition_result = + | T_state of Term.t + (** The successor state; the VM unifies it with [after:]. *) + | T_fail (** No such transition: integrity violation and kin. *) + | T_stuck (** Arguments not ground yet; the planner defers. *) + (** What a host must answer for the VM to run: which relation lives - under a name. Builtins are the VM's own and are not consulted - here. *) + under a name, optionally at a state ([at:] reads, decision 7), + and which names are transition relations. Builtins are the VM's + own and are not consulted here. The standalone world has one + implicit state and no transitions (decision 5). *) module type WORLD = sig type t - val find : t -> string -> def option + val find : t -> ?at:Term.t -> string -> def option + + val transition : + t -> string -> Pattern.t Label.Map.t -> transition_result option + (** [None] when the name is not a transition relation of this + world. Bindings arrive resolved. *) end type error @@ -94,7 +115,13 @@ val expr_of_node : Ast.node -> (expr, error) result module Standalone : sig type t - val find : t -> string -> def option + val find : t -> ?at:Term.t -> string -> def option + (** [at:] is accepted and ignored: the standalone world is its own + single, eternal state. *) + + val transition : t -> string -> Pattern.t Label.Map.t -> transition_result option + (** Always [None]: no branches, no transitions, the pure + fragment. *) val load : Ast.statement list -> (t * expr list * pending list, error) result (** Admits a program: registers relations, checks every fact |