diff options
| -rw-r--r-- | README.org | 29 | ||||
| -rw-r--r-- | docs/vm.org | 10 | ||||
| -rw-r--r-- | lib/lexer.mll | 3 | ||||
| -rw-r--r-- | lib/world.mli | 7 | ||||
| -rw-r--r-- | test/dune | 2 | ||||
| -rw-r--r-- | test/test_embedding.ml | 80 | ||||
| -rw-r--r-- | test/test_vm.ml | 11 |
7 files changed, 136 insertions, 6 deletions
@@ -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. *) @@ -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", [ |