1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
#+TITLE: Sol Examples
* Running
From the repository root, with Nix:
#+BEGIN_SRC sh
nix develop -c dune exec sol -- examples/family.sol
#+END_SRC
Or enter the shell once and run them all:
#+BEGIN_SRC sh
nix develop
dune build
for f in examples/*.sol; do echo "== $f"; dune exec sol -- "$f"; done
#+END_SRC
Without a file argument, =dune exec sol= starts a REPL: declarations
accumulate, =Query expression: ...= runs immediately, one statement
per line.
* The files
- =family.sol= :: relations, facts, a rule, joins through shared
variables, decidable denial with =:not=, and the =World= scoped
negation form.
- =arithmetic.sol= :: =Plus= and =Times= evaluating forward and
solving backward through the rationals; minimal shape, where
=1/2 + 1/2= is the integer =1=.
- =recursion.sol= :: structural recursion admitted by the decrease
checker extracted from Rocq, and Even/Odd mutual recursion under a
lexicographic measure.
- =constraints.sol= :: membership is not generation: residuation,
interval propagation, finite ranges enumerating, contradictions
answering no, and explicit bounded generation with =Between=.
- =quantifiers.sol= :: universals over infinite domains proven or
refuted symbolically, including the specification's own true and
false examples and the =Plus= identity; finite quantifiers simply
run.
- =integrity.sol= :: schemas as membership: primitive domains, a
refinement, and a foreign key as a criterion. The comments at the
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
notation, =yes.= for a closed query that holds, =no.= for one that
does not. An answer conditioned on open membership prints its
residual constraints after the bindings, as the propositions they
are.
|
