diff options
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 |