From f52efd20120cf5ceeae28da2c04d57acc6e46f14 Mon Sep 17 00:00:00 2001
From: Marcos Magueta <maguetamarcos@gmail.com>
Date: Sun, 12 Jul 2026 10:11:38 -0300
Subject: branch world: state scoped reads, insert transitions, tip commit

---
 lib/world.mli | 35 +++++++++++++++++++++++++++++++----
 1 file changed, 31 insertions(+), 4 deletions(-)

(limited to 'lib/world.mli')

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
-- 
cgit v1.2.3