From eb81c07047979f3fe53383ff2a42393f0b29bd28 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 03:17:10 -0300 Subject: embedding surface, host world test, deep recursion, line tracking --- README.org | 29 +++++++++++++++++++++++++---- 1 file changed, 25 insertions(+), 4 deletions(-) (limited to 'README.org') 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. -- cgit v1.2.3