path: root/lib/world.ml

type expr =
  | Apply of string * Pattern.t Label.Map.t
  | And of expr * expr
  | Or of expr * expr

type rule = {
  rule_name : string;
  head : Pattern.t Label.Map.t;
  body : expr;
  witness : Label.t option;
}

type domain = D_integer | D_natural | D_rational | D_string

type def =
  | Table of { schema : (Label.t * domain) list; facts : Term.t Label.Map.t list }
  | Rules of rule list

module type WORLD = sig
  type t

  val find : t -> string -> def option
end

type error =
  | Invalid_label of string
  | Duplicate_label of string
  | Zero_denominator
  | Lowercase_name of string
  | Term_expected of string
  | Proposition_expected of string
  | Malformed_directive of string
  | Unknown_domain of string
  | Unknown_relation of string
  | Already_defined of string
  | Fact_not_ground of string
  | Schema_mismatch of { relation : string; detail : string }
  | Domain_violation of { relation : string; label : string }
  | Non_total_rule of string
  | Mutual_recursion of string list

let pp_error fmt = function
  | Invalid_label l -> Format.fprintf fmt "invalid label: %s" l
  | Duplicate_label l -> Format.fprintf fmt "duplicate label: %s:" l
  | Zero_denominator -> Format.fprintf fmt "rational literal with zero denominator"
  | Lowercase_name n ->
      Format.fprintf fmt "lowercase name %s cannot be a variable or relation here" n
  | Term_expected d -> Format.fprintf fmt "a term was expected: %s" d
  | Proposition_expected d -> Format.fprintf fmt "a proposition was expected: %s" d
  | Malformed_directive d -> Format.fprintf fmt "malformed directive: %s" d
  | Unknown_domain d -> Format.fprintf fmt "unknown domain: %s" d
  | Unknown_relation r -> Format.fprintf fmt "unknown relation: %s" r
  | Already_defined r -> Format.fprintf fmt "relation already defined: %s" r
  | Fact_not_ground r -> Format.fprintf fmt "fact for %s is not ground" r
  | Schema_mismatch { relation; detail } ->
      Format.fprintf fmt "schema mismatch on %s: %s" relation detail
  | Domain_violation { relation; label } ->
      Format.fprintf fmt "domain violation on %s at %s:" relation label
  | Non_total_rule name ->
      Format.fprintf fmt
        "rule %S rejected: no structurally decreasing argument in its recursive call"
        name
  | Mutual_recursion cycle ->
      Format.fprintf fmt "mutual recursion rejected: %s"
        (String.concat " -> " cycle)

let ( let* ) = Result.bind

let is_uppercase s = String.length s > 0 && s.[0] >= 'A' && s.[0] <= 'Z'

let label_of_string s =
  match Label.of_string s with
  | Ok l -> Ok l
  | Error (`Invalid_label l) -> Error (Invalid_label l)

let bindings_to_map ~of_node bindings =
  List.fold_left
    (fun acc (name, node) ->
      let* map = acc in
      let* label = label_of_string name in
      if Label.Map.mem label map then Error (Duplicate_label name)
      else
        let* value = of_node node in
        Ok (Label.Map.add label value map))
    (Ok Label.Map.empty) bindings

(* Term position: uppercase names are variables. Blocks and
   combinators are propositions and cannot appear here. *)
let rec pattern_of_node (node : Ast.node) : (Pattern.t, error) result =
  match node with
  | Ast.Name n ->
      if is_uppercase n then Ok (Pattern.Var n) else Error (Lowercase_name n)
  | Ast.Int z -> Ok (Pattern.Integer z)
  | Ast.Rat (num, den) -> (
      match Term.rational ~num ~den with
      | Ok t -> Ok (Pattern.of_term t)
      | Error `Zero_denominator -> Error Zero_denominator)
  | Ast.Str s -> Ok (Pattern.String s)
  | Ast.Record fields ->
      let* map = bindings_to_map ~of_node:pattern_of_node fields in
      Ok (Pattern.Record map)
  | Ast.Seq (items, tail) ->
      let* tail =
        match tail with
        | None -> Ok Pattern.Nil
        | Some node -> pattern_of_node node
      in
      List.fold_right
        (fun item acc ->
          let* acc = acc in
          let* head = pattern_of_node item in
          Ok (Pattern.cons ~head ~tail:acc))
        items (Ok tail)
  | Ast.Block (head, _) -> Error (Term_expected ("[" ^ head ^ " ...]"))
  | Ast.And _ -> Error (Term_expected ":and")
  | Ast.Or _ -> Error (Term_expected ":or")

(* Proposition position: blocks apply relations, combinators
   compose. Terms cannot appear here. *)
let rec expr_of_node (node : Ast.node) : (expr, error) result =
  match node with
  | Ast.Block (head, bindings) ->
      let* map = bindings_to_map ~of_node:pattern_of_node bindings in
      Ok (Apply (head, map))
  | Ast.And (a, b) ->
      let* a = expr_of_node a in
      let* b = expr_of_node b in
      Ok (And (a, b))
  | Ast.Or (a, b) ->
      let* a = expr_of_node a in
      let* b = expr_of_node b in
      Ok (Or (a, b))
  | Ast.Name n -> Error (Proposition_expected n)
  | Ast.Int _ | Ast.Rat _ | Ast.Str _ | Ast.Record _ | Ast.Seq _ ->
      Error (Proposition_expected "a literal")

let domain_of_name = function
  | "Integer" -> Ok D_integer
  | "Natural" -> Ok D_natural
  | "Rational" -> Ok D_rational
  | "String" -> Ok D_string
  | other -> Error (Unknown_domain other)

(* Membership of a ground term in a builtin domain. Note the
   inclusions of decision 12: a Natural is an Integer, an Integer is
   a Rational, all literally. *)
let member_of_domain (term : Term.t) = function
  | D_integer -> ( match term with Term.Integer _ -> true | _ -> false)
  | D_natural -> (
      match term with Term.Integer z -> Z.geq z Z.zero | _ -> false)
  | D_rational -> (
      match term with Term.Integer _ | Term.Rational _ -> true | _ -> false)
  | D_string -> ( match term with Term.String _ -> true | _ -> false)

let rec applications = function
  | Apply (name, bindings) -> [ (name, bindings) ]
  | And (a, b) | Or (a, b) -> applications a @ applications b

module String_map = Map.Make (String)

module Standalone = struct
  type t = def String_map.t

  let find world name = String_map.find_opt name world

  let schema_of_node = function
    | Ast.Seq (entries, None) ->
        List.fold_left
          (fun acc entry ->
            let* schema = acc in
            match entry with
            | Ast.Block (attr, [ ("domain", Ast.Name domain_name) ]) ->
                let* label = label_of_string attr in
                let* domain = domain_of_name domain_name in
                Ok ((label, domain) :: schema)
            | _ -> Error (Malformed_directive "schema entries are [attr domain: Name]"))
          (Ok []) entries
        |> Result.map List.rev
    | _ -> Error (Malformed_directive "schema: takes #( ... ) of entries")

  (* The structural decrease check of decision 10, rung one. Every
     self-recursive application must have an argument strictly
     contained in the head's argument at the same label; that label
     is kept as the runtime witness. *)
  let admit_rule ~relation rule_name head body =
    let recursive =
      applications body |> List.filter (fun (name, _) -> String.equal name relation)
    in
    match recursive with
    | [] -> Ok { rule_name; head; body; witness = None }
    | _ ->
        let witness_for (_, call_bindings) =
          Label.Map.fold
            (fun label head_arg found ->
              match found with
              | Some _ -> found
              | None -> (
                  match Label.Map.find_opt label call_bindings with
                  | Some call_arg
                    when Pattern.strictly_contains head_arg ~sub:call_arg ->
                      Some label
                  | _ -> None))
            head None
        in
        let witnesses = List.map witness_for recursive in
        if List.for_all Option.is_some witnesses then
          (* All recursive calls decrease; any common witness works
             at runtime, and per-call witnesses agree by label here
             because they are all drawn from the same head. *)
          Ok { rule_name; head; body; witness = List.nth witnesses 0 }
        else Error (Non_total_rule rule_name)

  let load statements =
    (* First pass: declare tables, collect raw material. *)
    let* world, raw_facts, raw_rules, raw_queries =
      List.fold_left
        (fun acc statement ->
          let* world, facts, rules, queries = acc in
          match (statement : Ast.statement) with
          | Ast.Directive ("Relation", [ ("named", Ast.Name name); ("schema", schema) ])
            ->
              if String_map.mem name world then Error (Already_defined name)
              else
                let* schema = schema_of_node schema in
                Ok
                  ( String_map.add name (Table { schema; facts = [] }) world,
                    facts,
                    rules,
                    queries )
          | Ast.Directive ("Relation", _) ->
              Error (Malformed_directive "Relation named: Name schema: #( ... )")
          | Ast.Directive
              ("Rule", [ ("name", Ast.Str rule_name); ("head", head); ("body", body) ])
            ->
              Ok (world, facts, (rule_name, head, body) :: rules, queries)
          | Ast.Directive ("Rule", _) ->
              Error (Malformed_directive "Rule name: \"...\" head: [...] body: ...")
          | Ast.Directive ("Query", [ ("expression", body) ]) ->
              Ok (world, facts, rules, body :: queries)
          | Ast.Directive ("Query", _) ->
              Error (Malformed_directive "Query expression: ...")
          | Ast.Directive (name, _) -> Error (Malformed_directive name)
          | Ast.Assert node -> Ok (world, node :: facts, rules, queries))
        (Ok (String_map.empty, [], [], []))
        statements
    in
    let raw_facts = List.rev raw_facts
    and raw_rules = List.rev raw_rules
    and raw_queries = List.rev raw_queries in
    (* Second pass: compile rules, group them by head relation, admit
       each with the totality check. *)
    let* compiled_rules =
      List.fold_left
        (fun acc (rule_name, head_node, body_node) ->
          let* grouped = acc in
          let* head_expr = expr_of_node head_node in
          let* relation, head =
            match head_expr with
            | Apply (name, bindings) -> Ok (name, bindings)
            | _ -> Error (Malformed_directive "a rule head is a single [...] block")
          in
          let* body = expr_of_node body_node in
          let* rule = admit_rule ~relation rule_name head body in
          let existing =
            Option.value ~default:[] (String_map.find_opt relation grouped)
          in
          Ok (String_map.add relation (existing @ [ rule ]) grouped))
        (Ok String_map.empty) raw_rules
    in
    let* world =
      String_map.fold
        (fun relation rules acc ->
          let* world = acc in
          if String_map.mem relation world then Error (Already_defined relation)
          else Ok (String_map.add relation (Rules rules) world))
        compiled_rules (Ok world)
    in
    (* Third pass: admit facts against schemas and domains. This is
       integrity control at loading, the same check membership always
       is. *)
    let* world =
      List.fold_left
        (fun acc node ->
          let* world = acc in
          let* expr = expr_of_node node in
          let* relation, bindings =
            match expr with
            | Apply (name, bindings) -> Ok (name, bindings)
            | _ -> Error (Malformed_directive "a fact is a single [...] block")
          in
          match String_map.find_opt relation world with
          | Some (Table { schema; facts }) ->
              let* tuple =
                Label.Map.fold
                  (fun label pattern acc ->
                    let* tuple = acc in
                    match Pattern.to_term pattern with
                    | Some term -> Ok (Label.Map.add label term tuple)
                    | None -> Error (Fact_not_ground relation))
                  bindings (Ok Label.Map.empty)
              in
              let* () =
                if
                  List.length schema = Label.Map.cardinal tuple
                  && List.for_all
                       (fun (label, _) -> Label.Map.mem label tuple)
                       schema
                then Ok ()
                else
                  Error
                    (Schema_mismatch
                       { relation; detail = "fact labels must match the schema" })
              in
              let* () =
                List.fold_left
                  (fun acc (label, domain) ->
                    let* () = acc in
                    if member_of_domain (Label.Map.find label tuple) domain then Ok ()
                    else
                      Error
                        (Domain_violation
                           { relation; label = Label.to_string label }))
                  (Ok ()) schema
              in
              Ok
                (String_map.add relation
                   (Table { schema; facts = facts @ [ tuple ] })
                   world)
          | Some (Rules _) ->
              Error
                (Schema_mismatch
                   { relation; detail = "facts cannot be asserted on a rule-defined relation" })
          | None -> Error (Unknown_relation relation))
        (Ok world) raw_facts
    in
    (* Fourth pass: reference checking and the mutual recursion cut.
       Self recursion is admitted with a witness; longer cycles are
       rejected outright. *)
    let known name =
      Builtin.is_builtin name || String_map.mem name world
    in
    let check_refs body =
      List.fold_left
        (fun acc (name, _) ->
          let* () = acc in
          if known name then Ok () else Error (Unknown_relation name))
        (Ok ()) (applications body)
    in
    let* () =
      String_map.fold
        (fun _ def acc ->
          let* () = acc in
          match def with
          | Table _ -> Ok ()
          | Rules rules ->
              List.fold_left
                (fun acc rule ->
                  let* () = acc in
                  check_refs rule.body)
                (Ok ()) rules)
        world (Ok ())
    in
    let dependencies relation =
      match String_map.find_opt relation world with
      | Some (Rules rules) ->
          List.concat_map
            (fun rule ->
              applications rule.body
              |> List.filter_map (fun (name, _) ->
                     if
                       (not (String.equal name relation))
                       && (match String_map.find_opt name world with
                          | Some (Rules _) -> true
                          | _ -> false)
                     then Some name
                     else None))
            rules
      | _ -> []
    in
    let* () =
      let rec visit path relation =
        if List.mem relation path then
          Error (Mutual_recursion (List.rev (relation :: path)))
        else
          List.fold_left
            (fun acc dep ->
              let* () = acc in
              visit (relation :: path) dep)
            (Ok ())
            (dependencies relation)
      in
      String_map.fold
        (fun relation def acc ->
          let* () = acc in
          match def with Rules _ -> visit [] relation | Table _ -> Ok ())
        world (Ok ())
    in
    (* Queries compile last, against the full catalog. *)
    let* queries =
      List.fold_left
        (fun acc node ->
          let* queries = acc in
          let* expr = expr_of_node node in
          let* () = check_refs expr in
          Ok (expr :: queries))
        (Ok []) raw_queries
      |> Result.map List.rev
    in
    Ok (world, queries)
end