diff options
| -rw-r--r-- | README.org | 6 | ||||
| -rw-r--r-- | dune-project | 1 | ||||
| -rw-r--r-- | examples/README.org | 9 | ||||
| -rw-r--r-- | flake.nix | 10 |
4 files changed, 25 insertions, 1 deletions
@@ -71,9 +71,13 @@ It covers: - the catalog as ordinary queryable relations; - subtyping as proven relation inclusion, intensional relation identity, and canonical representatives for quotient domains; +- OCaml for the implementation, Rocq for the proofs, extraction + binding the two; - applications as propositions everywhere: no relation application in term position, statements about results written flat as - membership. + membership; +- relation references as a term kind, written =#Name=: relations as + data for transitions, higher-order arguments, and the catalog. ** Core Design Principles and Pipeline Specification diff --git a/dune-project b/dune-project index 4ba98c7..d490405 100644 --- a/dune-project +++ b/dune-project @@ -22,4 +22,5 @@ (>= 5.1)) zarith (menhir :build) + (coq :build) (alcotest :with-test))) diff --git a/examples/README.org b/examples/README.org index 20b853a..3ab427f 100644 --- a/examples/README.org +++ b/examples/README.org @@ -43,6 +43,15 @@ per line. bottom show facts that make admission reject the whole program; uncomment one and run again to see it happen. +* What is not here + +States, transitions and commit (=[Insert relation: #Person ...]=, +=at:= scoped reads, the branch tip) belong to the stateful world +and do not exist in the standalone binary, by decision 5: standalone +Sol is the pure fragment. The working demonstration of that half +lives in =test/test_branch.ml=, driven through the embedding +interface the way RNT drives it. + * Reading the answers Each query prints one line per answer: variable bindings in Sol @@ -26,6 +26,16 @@ duneVersion = "3"; src = self; + # The parser is menhir-generated, and the proven + # containment/lexicographic checkers are extracted from + # Rocq during the build. + nativeBuildInputs = [ + ocamlPackages.menhir + pkgs.coq + ]; + buildInputs = [ + pkgs.coqPackages.stdlib + ]; propagatedBuildInputs = [ ocamlPackages.zarith ]; |