diff options
Diffstat (limited to '')
| -rw-r--r-- | lib/world.ml | 192 | ||||
| -rw-r--r-- | lib/world.mli | 50 |
2 files changed, 199 insertions, 43 deletions
diff --git a/lib/world.ml b/lib/world.ml index c3d3ef2..6e1e883 100644 --- a/lib/world.ml +++ b/lib/world.ml @@ -2,6 +2,8 @@ type expr = | Apply of string * Pattern.t Label.Map.t | And of expr * expr | Or of expr * expr + | Not of expr * expr + | Forall of expr * expr type rule = { rule_name : string; @@ -10,7 +12,11 @@ type rule = { witness : Label.t option; } -type domain = D_integer | D_natural | D_rational | D_string +type primitive = D_integer | D_natural | D_rational | D_string + +type domain = + | Primitive of primitive + | Criterion of { subject : string; body : expr } type def = | Table of { schema : (Label.t * domain) list; facts : Term.t Label.Map.t list } @@ -38,6 +44,13 @@ type error = | Domain_violation of { relation : string; label : string } | Non_total_rule of string | Mutual_recursion of string list + | Criterion_arity of { relation : string; label : string } + +type pending = { + pending_relation : string; + pending_label : Label.t; + pending_body : expr; +} let pp_error fmt = function | Invalid_label l -> Format.fprintf fmt "invalid label: %s" l @@ -63,6 +76,10 @@ let pp_error fmt = function | Mutual_recursion cycle -> Format.fprintf fmt "mutual recursion rejected: %s" (String.concat " -> " cycle) + | Criterion_arity { relation; label } -> + Format.fprintf fmt + "criterion on %s at %s: must have exactly one free variable, the subject" + relation label let ( let* ) = Result.bind @@ -114,11 +131,53 @@ let rec pattern_of_node (node : Ast.node) : (Pattern.t, error) result = | Ast.Block (head, _) -> Error (Term_expected ("[" ^ head ^ " ...]")) | Ast.And _ -> Error (Term_expected ":and") | Ast.Or _ -> Error (Term_expected ":or") + | Ast.Not _ -> Error (Term_expected ":not") + +(* Renaming a quantified variable apart. The stamp cannot be lexed, + so quantifier scopes are unforgeable from source text. *) +let quantifier_counter = ref 0 + +let rec rename_var ~from ~into = function + | Pattern.Var v when String.equal v from -> Pattern.Var into + | Pattern.Record map -> Pattern.Record (Label.Map.map (rename_var ~from ~into) map) + | other -> other + +let rec rename_var_expr ~from ~into = function + | Apply (name, bindings) -> + Apply (name, Label.Map.map (rename_var ~from ~into) bindings) + | And (a, b) -> And (rename_var_expr ~from ~into a, rename_var_expr ~from ~into b) + | Or (a, b) -> Or (rename_var_expr ~from ~into a, rename_var_expr ~from ~into b) + | Not (a, b) -> Not (rename_var_expr ~from ~into a, rename_var_expr ~from ~into b) + | Forall (a, b) -> + Forall (rename_var_expr ~from ~into a, rename_var_expr ~from ~into b) (* Proposition position: blocks apply relations, combinators - compose. Terms cannot appear here. *) + compose. Terms cannot appear here. Exists and ForAll are the two + higher-order forms; their variable is renamed apart, and Exists + lowers to a conjunction because query variables are existential + already. *) let rec expr_of_node (node : Ast.node) : (expr, error) result = match node with + | Ast.Block (("Exists" | "ForAll") as form, bindings) -> ( + match + ( List.assoc_opt "variable" bindings, + List.assoc_opt "quantifier" bindings, + List.assoc_opt "body" bindings ) + with + | Some (Ast.Name variable), Some quantifier, Some body + when is_uppercase variable && List.length bindings = 3 -> + let* quantifier = expr_of_node quantifier in + let* body = expr_of_node body in + incr quantifier_counter; + let fresh = variable ^ "@q" ^ string_of_int !quantifier_counter in + let quantifier = rename_var_expr ~from:variable ~into:fresh quantifier + and body = rename_var_expr ~from:variable ~into:fresh body in + if String.equal form "Exists" then Ok (And (quantifier, body)) + else Ok (Forall (quantifier, body)) + | _ -> + Error + (Malformed_directive + (form ^ " variable: Name quantifier: [...] body: [...]"))) | Ast.Block (head, bindings) -> let* map = bindings_to_map ~of_node:pattern_of_node bindings in Ok (Apply (head, map)) @@ -130,21 +189,31 @@ let rec expr_of_node (node : Ast.node) : (expr, error) result = let* a = expr_of_node a in let* b = expr_of_node b in Ok (Or (a, b)) + | Ast.Not (a, b) -> + let* a = expr_of_node a in + let* b = expr_of_node b in + Ok (Not (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) +let rec expr_free_vars = function + | Apply (_, bindings) -> + Label.Map.fold (fun _ p acc -> acc @ Pattern.vars p) bindings [] + | And (a, b) | Or (a, b) | Not (a, b) | Forall (a, b) -> + expr_free_vars a @ expr_free_vars b + +let primitive_of_name = function + | "Integer" -> Some D_integer + | "Natural" -> Some D_natural + | "Rational" -> Some D_rational + | "String" -> Some D_string + | _ -> None -(* Membership of a ground term in a builtin domain. Note the +(* Membership of a ground term in a primitive 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 +let member_of_primitive (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) @@ -154,7 +223,8 @@ let member_of_domain (term : Term.t) = function let rec applications = function | Apply (name, bindings) -> [ (name, bindings) ] - | And (a, b) | Or (a, b) -> applications a @ applications b + | And (a, b) | Or (a, b) | Not (a, b) | Forall (a, b) -> + applications a @ applications b module String_map = Map.Make (String) @@ -163,17 +233,37 @@ module Standalone = struct let find world name = String_map.find_opt name world - let schema_of_node = function + let schema_of_node ~relation = 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) ]) -> + | Ast.Block (attr, [ ("domain", domain_node) ]) -> ( 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]")) + match domain_node with + | Ast.Name name when Option.is_some (primitive_of_name name) -> + let primitive = Option.get (primitive_of_name name) in + Ok ((label, Primitive primitive) :: schema) + | Ast.Name other -> Error (Unknown_domain other) + | criterion -> + (* A membership criterion: any relational + expression with exactly one free variable, + the subject. *) + let* body = expr_of_node criterion in + let subjects = + List.sort_uniq String.compare (expr_free_vars body) + in + (match subjects with + | [ subject ] -> + Ok ((label, Criterion { subject; body }) :: schema) + | _ -> + Error + (Criterion_arity + { relation; label = Label.to_string label }))) + | _ -> + Error + (Malformed_directive "schema entries are [attr domain: ...]")) (Ok []) entries |> Result.map List.rev | _ -> Error (Malformed_directive "schema: takes #( ... ) of entries") @@ -221,7 +311,7 @@ module Standalone = struct -> if String_map.mem name world then Error (Already_defined name) else - let* schema = schema_of_node schema in + let* schema = schema_of_node ~relation:name schema in Ok ( String_map.add name (Table { schema; facts = [] }) world, facts, @@ -277,11 +367,25 @@ module Standalone = struct in (* Third pass: admit facts against schemas and domains. This is integrity control at loading, the same check membership always - is. *) - let* world = + is. Primitive domains decide here; criteria need the solver, + so they are handed to Program as pending checks with the + subject already bound to the attribute value. *) + let equal_l = Result.get_ok (label_of_string "left") + and right_l = Result.get_ok (label_of_string "right") in + let bind_subject subject value body = + And + ( Apply + ( "Equal", + Label.Map.( + empty + |> add equal_l (Pattern.Var subject) + |> add right_l (Pattern.of_term value)) ), + body ) + in + let* world, pendings = List.fold_left (fun acc node -> - let* world = acc in + let* world, pendings = acc in let* expr = expr_of_node node in let* relation, bindings = match expr with @@ -311,27 +415,40 @@ module Standalone = struct (Schema_mismatch { relation; detail = "fact labels must match the schema" }) in - let* () = + let* new_pendings = 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 + let* pendings = acc in + let value = Label.Map.find label tuple in + match domain with + | Primitive primitive -> + if member_of_primitive value primitive then Ok pendings + else + Error + (Domain_violation + { relation; label = Label.to_string label }) + | Criterion { subject; body } -> + Ok + ({ + pending_relation = relation; + pending_label = label; + pending_body = bind_subject subject value body; + } + :: pendings)) + (Ok []) schema in Ok - (String_map.add relation - (Table { schema; facts = facts @ [ tuple ] }) - world) + ( String_map.add relation + (Table { schema; facts = facts @ [ tuple ] }) + world, + pendings @ List.rev new_pendings ) | 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 + (Ok (world, [])) + raw_facts in (* Fourth pass: reference checking and the mutual recursion cut. Self recursion is admitted with a witness; longer cycles are @@ -351,7 +468,14 @@ module Standalone = struct (fun _ def acc -> let* () = acc in match def with - | Table _ -> Ok () + | Table { schema; _ } -> + List.fold_left + (fun acc (_, domain) -> + let* () = acc in + match domain with + | Primitive _ -> Ok () + | Criterion { body; _ } -> check_refs body) + (Ok ()) schema | Rules rules -> List.fold_left (fun acc rule -> @@ -406,5 +530,5 @@ module Standalone = struct (Ok []) raw_queries |> Result.map List.rev in - Ok (world, queries) + Ok (world, queries, pendings) end diff --git a/lib/world.mli b/lib/world.mli index 76ad316..0a3bb9a 100644 --- a/lib/world.mli +++ b/lib/world.mli @@ -9,11 +9,21 @@ terminate. *) (** A compiled relational expression: what rule bodies and queries - are made of after names are resolved. *) + are made of after names are resolved. [Exists] is lowered away + at loading: its variable is renamed apart and the form becomes a + conjunction. *) type expr = | Apply of string * Pattern.t Label.Map.t | And of expr * expr | Or of expr * expr + | Not of expr * expr + (** [u :not d]: the universe holds and the denial has no + solutions. Decidable negation only: the VM runs the denial + once its variables are ground. *) + | Forall of expr * expr + (** Every solution of the quantifier satisfies the body. The + VM runs it when the quantifier is decidable, which keeps + universals off infinite domains. *) type rule = { rule_name : string; @@ -26,8 +36,17 @@ type rule = { termination. [None] on non-recursive rules. *) } -(** The builtin domains a schema may constrain an attribute by. *) -type domain = D_integer | D_natural | D_rational | D_string +(** The primitive host-checked domains. *) +type primitive = D_integer | D_natural | D_rational | D_string + +(** What a schema constrains an attribute by: a primitive domain, or + a membership criterion, an arbitrary relational expression with + exactly one free variable, the subject, bound to the attribute + value at admission. Foreign keys are the criterion + [([Department id: D])], nothing more special than that. *) +type domain = + | Primitive of primitive + | Criterion of { subject : string; body : expr } (** How a relation is defined. *) type def = @@ -48,6 +67,18 @@ type error val pp_error : Format.formatter -> error -> unit +(** A fact attribute awaiting a criterion check. The loader cannot + run the solver (the solver sits above it), so criterion + admission is finished by {!Program}, against the fully loaded + world. *) +type pending = { + pending_relation : string; + pending_label : Label.t; + pending_body : expr; + (** The criterion with its subject already bound to the + attribute value; admissible iff it has a solution. *) +} + (** The standalone world: an immutable catalog loaded from program text. This is Sol as a separate language; there are no branches, no transitions, only the pure fragment. *) @@ -56,12 +87,13 @@ module Standalone : sig val find : t -> string -> def option - val load : Ast.statement list -> (t * expr list, error) result + val load : Ast.statement list -> (t * expr list * pending list, error) result (** Admits a program: registers relations, checks every fact - against its schema and domains, compiles rules and queries, - and enforces totality. Rejected, not deferred: a recursive - rule without a structural decrease witness, a mutual + against its schema and primitive domains, compiles rules and + queries, and enforces totality. Rejected, not deferred: a + recursive rule without a structural decrease witness, a mutual recursion cycle, an unknown relation, or an ill-typed fact is - an [error], and no world exists. Returns the world and the - query expressions in program order. *) + an [error], and no world exists. Returns the world, the query + expressions in program order, and the criterion checks for + {!Program} to finish. *) end |