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, since that explodes combinatorially. Three steps run: 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. Applying these
expansions literally settles the degenerate arities, with no special casing needed. A
true element becomes {:or, [[]]}, and a false one becomes {:or, []}.
Negation of a disjunction distributes: De Morgan's law applies there, and only
there. Negation of a conjunction becomes a Rete.IR.CompoundNegation instead. 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.
This is either a condition, the negation of a condition, or the negation of a whole conjunction of literals — the case De Morgan's law 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. to_dnf/1 rewrites
them 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 an error instead. Otherwise, a rule could 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, instead of kept as a one-branch disjunction. 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. Since true or anything is true, 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 the walk meets them, so the error can name the gate that
overflows the branch limit.
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 all 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.