diff options
| author | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-11 03:17:10 -0300 |
|---|---|---|
| committer | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-11 03:17:10 -0300 |
| commit | eb81c07047979f3fe53383ff2a42393f0b29bd28 (patch) | |
| tree | e9cac26f28e7f2ca3259be25769dfdd23e04f43b /docs | |
| parent | 40376c3ea009eab4db9ba27837e61d8bec310b8f (diff) | |
| download | SOL-eb81c07047979f3fe53383ff2a42393f0b29bd28.tar.gz SOL-eb81c07047979f3fe53383ff2a42393f0b29bd28.zip | |
embedding surface, host world test, deep recursion, line tracking
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/vm.org | 10 |
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. |