path: root/lib/program.ml

type error =
  | Load of World.error
  | Integrity of { relation : string; label : string }
  | Undecidable_criterion of { relation : string; label : string }

let pp_error fmt = function
  | Load error -> World.pp_error fmt error
  | Integrity { relation; label } ->
      Format.fprintf fmt "integrity violation on %s at %s:" relation label
  | Undecidable_criterion { relation; label } ->
      Format.fprintf fmt "criterion on %s at %s: is not decidable" relation label

let load statements =
  match World.Standalone.load statements with
  | Error error -> Error (Load error)
  | Ok (world, queries, pendings) ->
      let rec admit = function
        | [] -> Ok (world, queries)
        | pending :: rest -> (
            let { World.pending_relation; pending_label; pending_body } =
              pending
            in
            match Vm.Standalone.solve world pending_body with
            (* 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
                     {
                       relation = pending_relation;
                       label = Label.to_string pending_label;
                     })
            | Error (Vm.Non_total_plan _) ->
                Error
                  (Undecidable_criterion
                     {
                       relation = pending_relation;
                       label = Label.to_string pending_label;
                     }))
      in
      admit pendings