aboutsummaryrefslogtreecommitdiffstats
path: root/docs/vm.org
diff options
context:
space:
mode:
authorMarcos Magueta <maguetamarcos@gmail.com>2026-07-11 03:17:10 -0300
committerMarcos Magueta <maguetamarcos@gmail.com>2026-07-11 03:17:10 -0300
commiteb81c07047979f3fe53383ff2a42393f0b29bd28 (patch)
treee9cac26f28e7f2ca3259be25769dfdd23e04f43b /docs/vm.org
parent40376c3ea009eab4db9ba27837e61d8bec310b8f (diff)
downloadSOL-eb81c07047979f3fe53383ff2a42393f0b29bd28.tar.gz
SOL-eb81c07047979f3fe53383ff2a42393f0b29bd28.zip
embedding surface, host world test, deep recursion, line tracking
Diffstat (limited to '')
-rw-r--r--docs/vm.org10
1 files changed, 10 insertions, 0 deletions
diff --git a/docs/vm.org b/docs/vm.org
index 6f3c454..4253231 100644
--- a/docs/vm.org
+++ b/docs/vm.org
@@ -110,6 +110,16 @@ integer =1=. Comparisons decide once both sides are ground. Between
is the one relation allowed to enumerate, because its range is finite
by construction.
+* Embedding
+
+The solver is a functor over the =WORLD= module type: a host answers
+=find= for its own relations and links the engine in-process. The
+embedding test builds a toy kernel catalog in plain OCaml, compiles
+query text through =World.expr_of_node=, and runs the same solver
+with the same totality guard. That is the RNT shape: Sakura compiles
+Sol (and Karuta lowered to Sol) to expressions, the kernel's catalog
+answers =find=, and no process boundary exists.
+
* Running
=sol file.sol= loads the program and prints each query's answers.