diff options
| author | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-11 22:12:53 -0300 |
|---|---|---|
| committer | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-11 22:12:53 -0300 |
| commit | 0886f3c71cf8551e4f8b3726654003a4f29645f0 (patch) | |
| tree | 884176834dc4f20b0af2cf4ab72c48b945203107 /lib/program.ml | |
| parent | f22834d3aaed2b2dd2c5d4203e937fc8fb4b5507 (diff) | |
| download | SOL-0886f3c71cf8551e4f8b3726654003a4f29645f0.tar.gz SOL-0886f3c71cf8551e4f8b3726654003a4f29645f0.zip | |
residuation: open membership returns residual constraints
Diffstat (limited to 'lib/program.ml')
| -rw-r--r-- | lib/program.ml | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/lib/program.ml b/lib/program.ml index ac62781..b0e363b 100644 --- a/lib/program.ml +++ b/lib/program.ml @@ -21,7 +21,19 @@ let load statements = pending in match Vm.Standalone.solve world pending_body with - | Ok (_ :: _) -> admit rest + (* Membership must be proven outright: an answer that is + itself conditioned on residual constraints does not + admit a fact. *) + | Ok solutions + when List.exists (fun s -> s.Vm.residue = []) solutions -> + admit rest + | Ok (_ :: _) -> + Error + (Undecidable_criterion + { + relation = pending_relation; + label = Label.to_string pending_label; + }) | Ok [] -> Error (Integrity |