diff options
Diffstat (limited to 'lib/world.ml')
| -rw-r--r-- | lib/world.ml | 410 |
1 files changed, 410 insertions, 0 deletions
diff --git a/lib/world.ml b/lib/world.ml new file mode 100644 index 0000000..c3d3ef2 --- /dev/null +++ b/lib/world.ml @@ -0,0 +1,410 @@ +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 |