Gate normalization: the phase between parsing and binding classification.
Internal. Turns the Rete.IR.Gate placeholders Rete.DSL.Parser left behind into
the per-condition form of Rete.IR.lhs/0: a single condition struct, or a disjunction
of conjunctions {:or, [[condition, ...], ...]}.
Normalization is per LHS element. The LHS as a whole is never flattened to DNF, which explodes combinatorially. Three steps: lift into a boolean tree, distribute into DNF, simplify. Author order is preserved and nothing depends on map iteration order, so the same input always produces byte-identical output.
not(a, b, ...) and nand mean not(and(...)), nor means not(or(...)), n-ary
xor means exactly one holds, and xnor is its negation. These expansions are
applied literally, which settles the degenerate arities without special casing. A true
element becomes {:or, [[]]} and a false one {:or, []}.
Negation of a disjunction distributes: de Morgan applies there and only there.
Negation of a conjunction becomes a Rete.IR.CompoundNegation, because the
conjuncts share existentially quantified variables and the rewrite would be a stronger
statement. Rete.Compiler.Negation extracts it later.
Distribution is the one step that can explode, so to_dnf/1 refuses to build more than
256 branches for one gate. Compile time sets that limit: escaping 1024
branches costs 32 s. See docs/design/ir.md §2.
Summary
Types
Disjunctive normal form: a disjunction of conjunctions of literals.
A normalized LHS element.
A literal of a normalized conjunction.
The internal boolean tree normalization works on.
Functions
The largest number of disjunctive branches a single gate may normalize into.
Normalizes one parsed LHS element.
Normalizes every element of an LHS, in order.
Prunes a DNF: repeated literals, contradictory branches, absorbed branches and duplicate branches.
Distributes a tree/0 into disjunctive normal form.
Lifts an LHS element into the internal boolean tree/0.
Types
@type dnf() :: [[literal()]]
Disjunctive normal form: a disjunction of conjunctions of literals.
@type element() :: Rete.IR.condition() | {:or, [[Rete.IR.condition()]]}
A normalized LHS element.
@type literal() :: {:pos, Rete.IR.condition()} | {:neg, Rete.IR.condition()} | {:cneg, [literal()]}
A literal of a normalized conjunction.
Either a condition, the negation of a condition, or the negation of a whole conjunction of literals - the case de Morgan is not allowed to touch.
@type tree() :: {:gate, atom(), [tree()]} | {:and, [tree()]} | {:or, [tree()]} | {:not, tree()} | {:lit, Rete.IR.condition()}
The internal boolean tree normalization works on.
{:gate, gate, args} nodes are the Rete.IR.Gate placeholders, which to_dnf/1
rewrites on the way down. :not is always unary here. An n-ary not gate is the
negation of the conjunction of its arguments.
Functions
@spec max_branches() :: pos_integer()
The largest number of disjunctive branches a single gate may normalize into.
Past this, to_dnf/1 raises rather than let a rule take minutes to compile
and build a beta network with thousands of join paths.
@spec normalize(Rete.IR.condition() | element()) :: element()
Normalizes one parsed LHS element.
Returns the element unchanged when it holds no gate, and otherwise a single
condition (possibly a Rete.IR.Negation or a Rete.IR.CompoundNegation) or
{:or, [[condition, ...], ...]}.
Examples
Writing a for a condition, !a for %Rete.IR.Negation{condition: a} and
!(a, b) for %Rete.IR.CompoundNegation{conditions: [a, b]}:
%Gate{gate: :and, args: [a, b]} -> {:or, [[a, b]]}
%Gate{gate: :or, args: [a, b]} -> {:or, [[a], [b]]}
%Gate{gate: :not, args: [a]} -> !a
%Gate{gate: :nand, args: [a, b]} -> !(a, b)
%Gate{gate: :nor, args: [a, b]} -> {:or, [[!a, !b]]}
%Gate{gate: :or, args: []} -> {:or, []}
%Fact{} -> the fact itself@spec normalize_lhs(Rete.IR.lhs()) :: Rete.IR.lhs()
Normalizes every element of an LHS, in order.
Returns a Rete.IR.lhs/0. A conjunction is spliced into the surrounding
element list rather than kept as a one-branch disjunction, and an element that
normalizes to true disappears. An element that normalizes to false is kept
as {:or, []}, because dropping it would change the meaning of the
production.
Prunes a DNF: repeated literals, contradictory branches, absorbed branches and duplicate branches.
A branch that is empty is true, and true or anything is true, so the
whole disjunction collapses to [[]]. No branch is ever dropped because
another subsumes it (a or (a and b) keeps both): branches carry bindings and
the longer one binds more.
Distributes a tree/0 into disjunctive normal form.
The empty disjunction is [] (false) and the empty conjunction is [[]]
(true). Gates are rewritten as they are met, so the gate that overflows the
branch limit can be named in the error.
Raises ArgumentError when a single gate would produce more than
max_branches/0 branches.
@spec to_tree(Rete.IR.condition() | element()) :: tree()
Lifts an LHS element into the internal boolean tree/0.
Gates, Rete.IR.Negation and Rete.IR.CompoundNegation nodes and
{:or, [[condition, ...], ...]} elements become tree nodes; every other
condition becomes an opaque {:lit, condition} leaf. Lifting an already
normalized element back into a tree is what makes normalize/1 idempotent.