embedding surface, host world test, deep recursion, line tracking

7 files changed, 136 insertions, 6 deletions

diff --git a/README.org b/README.org
index 5de75cf..4485f07 100644
--- a/README.org
+++ b/README.org
@@ -164,13 +164,34 @@ In particular, it should make clear how the VM distinguishes:
 
 * Current Status
 
-At the moment, the project has a working conceptual direction and a
-language specification draft.
+The language has a specification, a set of normative integration
+decisions, and a working first implementation in OCaml:
+
+- a parser for the surface syntax under the delimiter law;
+- a loader whose admission enforces totality: structural decrease
+  witnesses on recursive rules, schema and domain checks on facts,
+  membership criteria (refinements and foreign keys) solved against
+  the complete extension;
+- a solver with dynamic goal selection, so conjunction is
+  commutative in fact and non total plans are rejected instead of
+  attempted;
+- decidable negation, Exists and ForAll;
+- backward-solving arithmetic over the integers and rationals with
+  minimal shape preserved;
+- a =WORLD= functor for embedding, exercised by a host-defined
+  catalog in the tests, and a standalone binary with a REPL.
+
+See =docs/vm.org= for behavior, =docs/terms.org= for the term
+algebra.
+
+Build with =nix develop -c dune build=; run the tests with =nix
+develop -c dune runtest=; run a program with =dune exec sol --
+file.sol=.
 
 The next documents to produce are:
 
 1. =docs/core-design-and-pipeline.org=
 2. =docs/virtual-machine-specification.org=
 
-These should build on the language specification and clarify how Sol
-can be implemented while preserving totality.
+These should build on the language specification, the integration
+decisions, and the implementation as it stands.
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.
diff --git a/lib/lexer.mll b/lib/lexer.mll
index 417369b..90beacf 100644
--- a/lib/lexer.mll
+++ b/lib/lexer.mll
@@ -27,7 +27,8 @@ let ident = ['A'-'Z' 'a'-'z'] ['A'-'Z' 'a'-'z' '0'-'9' '_']*
 let string_body = ([^ '"' '\\'] | '\\' _)*
 
 rule token = parse
-  | [' ' '\t' '\r' '\n']+     { token lexbuf }
+  | '\n'                      { Lexing.new_line lexbuf; token lexbuf }
+  | [' ' '\t' '\r']+          { token lexbuf }
   | '%' [^ '\n']*             { token lexbuf }
   | "#("                      { HASH_LPAREN }
   | '('                       { LPAREN }
diff --git a/lib/world.mli b/lib/world.mli
index 0a3bb9a..51ee078 100644
--- a/lib/world.mli
+++ b/lib/world.mli
@@ -79,6 +79,13 @@ type pending = {
           attribute value; admissible iff it has a solution. *)
 }
 
+val expr_of_node : Ast.node -> (expr, error) result
+(** Compiles one surface expression: names resolve by context,
+    [Exists] lowers, quantified variables rename apart. This is the
+    embedding hosts' way in: they compile queries themselves and
+    answer for their own relations, so no standalone reference
+    checking happens here. *)
+
 (** The standalone world: an immutable catalog loaded from program
     text. This is Sol as a separate language; there are no branches,
     no transitions, only the pure fragment. *)
diff --git a/test/dune b/test/dune
index 0c5313b..6e5e6eb 100644
--- a/test/dune
+++ b/test/dune
@@ -1,3 +1,3 @@
 (tests
- (names test_term test_vm)
+ (names test_term test_vm test_embedding)
  (libraries sol zarith alcotest))
diff --git a/test/test_embedding.ml b/test/test_embedding.ml
new file mode 100644
index 0000000..32effc2
--- /dev/null
+++ b/test/test_embedding.ml
@@ -0,0 +1,80 @@
+(* Decision 4, exercised: a host builds its own world in OCaml, no
+   parsing involved, and links the same solver. This is the shape of
+   the RNT embedding: the kernel's catalog answers [find], and the
+   engine runs in-process. *)
+
+let label s =
+  match Sol.Label.of_string s with
+  | Ok l -> l
+  | Error (`Invalid_label s) -> Alcotest.failf "invalid label: %s" s
+
+let int n = Sol.Term.integer (Z.of_int n)
+
+(* A toy kernel catalog: one stored relation, served from an OCaml
+   structure rather than program text. *)
+module Kernel_world = struct
+  type t = unit
+
+  let tuple pairs =
+    List.fold_left
+      (fun map (name, term) -> Sol.Label.Map.add (label name) term map)
+      Sol.Label.Map.empty pairs
+
+  let sensors =
+    Sol.World.Table
+      {
+        schema = [ (label "id", Sol.World.Primitive Sol.World.D_integer) ];
+        facts =
+          [
+            tuple [ ("id", int 1); ("reading", int 40) ];
+            tuple [ ("id", int 2); ("reading", int 75) ];
+            tuple [ ("id", int 3); ("reading", int 12) ];
+          ];
+      }
+
+  let find () name =
+    match name with "Sensor" -> Some sensors | _ -> None
+end
+
+module Kernel_vm = Sol.Vm.Make (Kernel_world)
+
+(* The host compiles query text itself through the exposed
+   expression compiler; its own catalog answers for relations. *)
+let solve source =
+  match Sol.Front.parse_string ("Query expression: " ^ source) with
+  | Error message -> Alcotest.failf "parse error: %s" message
+  | Ok [ Sol.Ast.Directive ("Query", [ ("expression", node) ]) ] -> (
+      match Sol.World.expr_of_node node with
+      | Error error -> Alcotest.failf "compile error: %a" Sol.World.pp_error error
+      | Ok query -> Kernel_vm.solve () query)
+  | Ok _ -> Alcotest.fail "expected one query statement"
+
+let show solutions =
+  solutions
+  |> List.map (fun solution ->
+         solution
+         |> List.map (fun (v, p) -> Format.asprintf "%s=%a" v Sol.Pattern.pp p)
+         |> String.concat ",")
+  |> String.concat "; "
+
+let test_kernel_scan () =
+  match solve {| [Sensor id: I reading: R] :and [GreaterThan left: R right: 30] |} with
+  | Ok solutions ->
+      Alcotest.(check string) "hot sensors" "I=1,R=40; I=2,R=75" (show solutions)
+  | Error error -> Alcotest.failf "solve error: %a" Sol.Vm.pp_error error
+
+let test_kernel_totality () =
+  match solve {| [Integer value: X] |} with
+  | Error (Sol.Vm.Non_total_plan _) -> ()
+  | Ok _ -> Alcotest.fail "the embedded engine must keep the totality guard"
+
+let () =
+  Alcotest.run "sol-embedding"
+    [
+      ( "kernel world",
+        [
+          Alcotest.test_case "scan over host relations" `Quick test_kernel_scan;
+          Alcotest.test_case "totality guard survives embedding" `Quick
+            test_kernel_totality;
+        ] );
+    ]
diff --git a/test/test_vm.ml b/test/test_vm.ml
index e564a83..38bbcc9 100644
--- a/test/test_vm.ml
+++ b/test/test_vm.ml
@@ -101,6 +101,16 @@ let test_length_of_strings () =
    ^ {| Query expression: [Length list: #("a" "b") result: R] |})
     "R=2"
 
+let test_deep_recursion () =
+  (* The witness shrinks a thousand times; the engine must neither
+     loop nor exhaust the stack on realistic depths. *)
+  let items = String.concat " " (List.init 1000 (fun _ -> "0")) in
+  check_answers "length of a thousand elements"
+    (length_rules
+    ^ Printf.sprintf {| Query expression: [Length list: #(%s) result: R] |}
+        items)
+    "R=1000"
+
 (* Bounded generation is the only enumeration. *)
 
 let test_between_generates () =
@@ -283,6 +293,7 @@ let () =
         [
           Alcotest.test_case "length" `Quick test_length;
           Alcotest.test_case "length over strings" `Quick test_length_of_strings;
+          Alcotest.test_case "deep recursion" `Quick test_deep_recursion;
         ] );
       ( "search",
         [