Skip to content

simplification

LogicSimplify

Bases: UnvalidatedForm, LogicLoader

Simplify a logic program before it is lowered.

Source code in src/finch/finch_logic/simplification.py 
42
43
44
45
46
47
48
49
50
51
52
53
54
55
class LogicSimplify(UnvalidatedForm, LogicLoader):
    """Simplify a logic program before it is lowered."""

    def __init__(self, ctx: LogicLoader):
        self.ctx = ctx

    def lower(
        self,
        prgm: lgc.LogicStatement,
        bindings: dict[lgc.Alias, TensorFType],
        stats: dict[lgc.Alias, TensorStats],
        stats_factory: StatsFactory,
    ):
        return self.ctx(simplify_logic(prgm), bindings, stats, stats_factory)

simplify_logic(prgm)

Algebraically simplify a logic program.

annihilate is deliberately left out. An operand of a MapJoin carries the fields that give the result its extent, so discarding one discards a dimension.

Source code in src/finch/finch_logic/simplification.py 
27
28
29
30
31
32
33
34
35
36
37
38
39
def simplify_logic(prgm: lgc.LogicNode) -> lgc.LogicNode:
    """
    Algebraically simplify a logic program.

    `annihilate` is deliberately left out. An operand of a MapJoin carries the
    fields that give the result its extent, so discarding one discards a
    dimension.
    """
    rules = [rule for rule in simplify_rules() if rule is not annihilate]
    # `unwrap_literal` belongs in the chain, not before it: `PostWalk` visits
    # children first, so an operand is unwrapped in time for the algebraic
    # rules to see a `LiteralTerm` when the parent call is examined.
    return Rewrite(Fixpoint(PostWalk(Chain([*rules, unwrap_literal]))))(prgm)

unwrap_literal(node)

Reorder(Literal(v), ()) => Literal(v), and likewise for Relabel.

A literal is zero-dimensional, so reordering or relabelling it by no fields is the identity. Without this the algebraic rules see nothing: optimize leaves every literal operand wrapped, so LiteralTerm never matches.

Source code in src/finch/finch_logic/simplification.py 
11
12
13
14
15
16
17
18
19
20
21
22
23
24
def unwrap_literal(node: lgc.LogicNode) -> lgc.LogicNode | None:
    """
    `Reorder(Literal(v), ())` => `Literal(v)`, and likewise for `Relabel`.

    A literal is zero-dimensional, so reordering or relabelling it by no fields
    is the identity. Without this the algebraic rules see nothing: `optimize`
    leaves every literal operand wrapped, so `LiteralTerm` never matches.
    """
    match node:
        case lgc.Reorder(lgc.Literal(_) as lit, ()) | lgc.Relabel(
            lgc.Literal(_) as lit, ()
        ):
            return lit
    return None