From 40376c3ea009eab4db9ba27837e61d8bec310b8f Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 03:15:25 -0300 Subject: negation, quantifiers and membership criteria as schema domains --- lib/world.mli | 50 +++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 41 insertions(+), 9 deletions(-) (limited to 'lib/world.mli') 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 -- cgit v1.2.3