diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/ast.ml | 2 | ||||
| -rw-r--r-- | lib/lexer.mll | 1 | ||||
| -rw-r--r-- | lib/parser.mly | 3 | ||||
| -rw-r--r-- | lib/program.ml | 40 | ||||
| -rw-r--r-- | lib/program.mli | 22 | ||||
| -rw-r--r-- | lib/vm.ml | 106 | ||||
| -rw-r--r-- | lib/world.ml | 192 | ||||
| -rw-r--r-- | lib/world.mli | 50 |
8 files changed, 342 insertions, 74 deletions
@@ -15,6 +15,8 @@ type node = | Block of string * (string * node) list (** [[Rel l: n ...]] *) | And of node * node | Or of node * node + | Not of node * node + (** [u :not d]: within the universe [u], deny [d]. *) (** A program is a list of statements. A bare block asserts a fact; a directive is a top-level message send such as diff --git a/lib/lexer.mll b/lib/lexer.mll index 53ef04a..417369b 100644 --- a/lib/lexer.mll +++ b/lib/lexer.mll @@ -39,6 +39,7 @@ rule token = parse | '|' { BAR } | ":and" { AND } | ":or" { OR } + | ":not" { NOT } | '-'? digit+ '/' digit+ as s { match String.index_opt s '/' with | Some i -> diff --git a/lib/parser.mly b/lib/parser.mly index c85eccc..4bac905 100644 --- a/lib/parser.mly +++ b/lib/parser.mly @@ -8,7 +8,7 @@ open Ast %token <string> NAME %token <string> LABEL %token LBRACKET RBRACKET LBRACE RBRACE LPAREN RPAREN HASH_LPAREN -%token BAR AND OR EOF +%token BAR AND OR NOT EOF %start <Ast.statement list> program @@ -32,6 +32,7 @@ node: conjunction: | left = conjunction; AND; right = operand { And (left, right) } + | left = conjunction; NOT; right = operand { Not (left, right) } | operand = operand { operand } operand: diff --git a/lib/program.ml b/lib/program.ml new file mode 100644 index 0000000..ac62781 --- /dev/null +++ b/lib/program.ml @@ -0,0 +1,40 @@ +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 + | Ok (_ :: _) -> admit rest + | 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 diff --git a/lib/program.mli b/lib/program.mli new file mode 100644 index 0000000..c271212 --- /dev/null +++ b/lib/program.mli @@ -0,0 +1,22 @@ +(** Whole-program admission: the entry point hosts use. + + The loader admits what it can decide alone; membership criteria + need the solver, so this module finishes admission by running + every pending criterion against the fully loaded world. Order of + facts in the source does not matter: integrity is judged against + the complete extension, the way a committed state would be. *) + +type error = + | Load of World.error + | Integrity of { relation : string; label : string } + (** A fact's attribute failed its membership criterion. *) + | Undecidable_criterion of { relation : string; label : string } + (** The criterion's plan was rejected as non-total. *) + +val pp_error : Format.formatter -> error -> unit + +val load : + Ast.statement list -> (World.Standalone.t * World.expr list, error) result +(** Parses nothing and solves queries for nobody: admits. Returns + the world and the query expressions, ready for + {!Vm.Standalone.solve}. *) @@ -10,19 +10,34 @@ type solution = (string * Pattern.t) list module Make (W : World.WORLD) = struct exception Stuck of string list + (* A goal is a proposition to establish or a denial to refute. + Conjunction flattens; [u :not d] contributes the universe + positively and the denial negatively. *) + type goal = Positive of World.expr | Negated of World.expr + let rec flatten = function | World.And (a, b) -> flatten a @ flatten b - | goal -> [ goal ] + | World.Not (universe, denial) -> flatten universe @ [ Negated denial ] + | expr -> [ Positive expr ] let rec expr_vars = function | World.Apply (_, bindings) -> Label.Map.fold (fun _ p acc -> acc @ Pattern.vars p) bindings [] - | World.And (a, b) | World.Or (a, b) -> expr_vars a @ expr_vars b + | World.And (a, b) | World.Or (a, b) | World.Not (a, b) | World.Forall (a, b) + -> + expr_vars a @ expr_vars b let goal_name = function - | World.Apply (name, _) -> name - | World.And _ -> ":and" - | World.Or _ -> ":or" + | Positive (World.Apply (name, _)) -> name + | Positive (World.Or _) -> ":or" + | Positive (World.And _) -> ":and" + | Positive (World.Not _) | Negated _ -> ":not" + | Positive (World.Forall _) -> "ForAll" + + let unresolved_vars subst expr = + expr_vars expr + |> List.filter (fun v -> + not (Pattern.is_ground (Pattern.Subst.resolve subst (Pattern.Var v)))) (* Rule variables are renamed apart at every unfolding. The suffix character cannot be lexed, so renamed variables are unforgeable @@ -42,6 +57,8 @@ module Make (W : World.WORLD) = struct World.Apply (name, Label.Map.map rename bindings) | World.And (a, b) -> World.And (rename_expr a, rename_expr b) | World.Or (a, b) -> World.Or (rename_expr a, rename_expr b) + | World.Not (a, b) -> World.Not (rename_expr a, rename_expr b) + | World.Forall (a, b) -> World.Forall (rename_expr a, rename_expr b) in (Label.Map.map rename rule.World.head, rename_expr rule.World.body) @@ -59,12 +76,30 @@ module Make (W : World.WORLD) = struct (* Executing one goal yields branches: an extended substitution and the extra goals it owes (rule bodies, disjuncts). [None] - means not decidable yet. *) - let try_goal world subst goal = + means not decidable yet; the planner retries it later, and + rejects the plan if nothing ever runs. *) + let rec try_goal world subst goal = match goal with - | World.Or (a, b) -> Some [ (subst, flatten a); (subst, flatten b) ] - | World.And _ -> Some [ (subst, flatten goal) ] - | World.Apply (name, bindings) -> ( + | Negated denial -> + if unresolved_vars subst denial = [] then + match search world subst (flatten denial) with + | [] -> Some [ (subst, []) ] + | _ -> Some [] + else None + | Positive (World.Or (a, b)) -> Some [ (subst, flatten a); (subst, flatten b) ] + | Positive (World.And _ | World.Not _) -> + Some [ (subst, flatten (match goal with Positive e -> e | _ -> assert false)) ] + | Positive (World.Forall (quantifier, body)) -> ( + (* Universal over the quantifier's solutions. Decidable only + when the quantifier itself is; a stuck quantifier defers + the universal, and an infinite one therefore never runs. *) + match search world subst (flatten quantifier) with + | exception Stuck _ -> None + | quantified -> + let holds s = search world s (flatten body) <> [] in + if List.for_all holds quantified then Some [ (subst, []) ] else Some [] + ) + | Positive (World.Apply (name, bindings)) -> ( match Builtin.run subst name bindings with | Some (Builtin.Solved substs) -> Some (List.map (fun s -> (s, [])) substs) @@ -107,31 +142,42 @@ module Make (W : World.WORLD) = struct rather than a crash. *) None)) + and search world subst goals = + match goals with + | [] -> [ subst ] + | _ -> ( + let rec select scanned = function + | [] -> None + | goal :: rest -> ( + match try_goal world subst goal with + | Some branches -> Some (branches, List.rev_append scanned rest) + | None -> select (goal :: scanned) rest) + in + match select [] goals with + | Some (branches, remaining) -> + List.concat_map + (fun (subst, extra) -> search world subst (extra @ remaining)) + branches + | None -> raise (Stuck (List.map goal_name goals))) + + (* Solution variables: the free variables of the query. Whatever + occurs only under a universal is bound per quantifier solution + and is nobody's answer. *) + let rec outer_vars = function + | World.Apply (_, bindings) -> + Label.Map.fold (fun _ p acc -> acc @ Pattern.vars p) bindings [] + | World.And (a, b) | World.Or (a, b) | World.Not (a, b) -> + outer_vars a @ outer_vars b + | World.Forall _ -> [] + let solve world expr = - let rec search subst goals = - match goals with - | [] -> [ subst ] - | _ -> ( - let rec select scanned = function - | [] -> None - | goal :: rest -> ( - match try_goal world subst goal with - | Some branches -> Some (branches, List.rev_append scanned rest) - | None -> select (goal :: scanned) rest) - in - match select [] goals with - | Some (branches, remaining) -> - List.concat_map - (fun (subst, extra) -> search subst (extra @ remaining)) - branches - | None -> raise (Stuck (List.map goal_name goals))) - in let variables = List.fold_left (fun acc v -> if List.mem v acc then acc else acc @ [ v ]) - [] (expr_vars expr) + [] (outer_vars expr) + |> List.filter (fun v -> not (String.contains v '@')) in - match search Pattern.Subst.empty (flatten expr) with + match search world Pattern.Subst.empty (flatten expr) with | exception Stuck goals -> Error (Non_total_plan goals) | substs -> let read subst = 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 |