Skip to content

proves

rule_add_with(ex, func)

Distribute max/min over add.

call(+, ~a..., call(max/min, ~b...), ~c...) =>
    call(max/min, map(x -> call(+, a..., x, c...), b)...))
Source code in src/finch/finch_notation/proves.py 
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
def rule_add_with(ex, func) -> Call | None:
    """
    Distribute max/min over add.

    ```
    call(+, ~a..., call(max/min, ~b...), ~c...) =>
        call(max/min, map(x -> call(+, a..., x, c...), b)...))
    ```
    """
    match ex:
        case Call(L(op), args) if (
            op == ffuncs.add and (found := _find_first_call(args, L(func))) is not None
        ):
            before, call_args, after = found
            return Call(
                L(func),
                tuple(Call(L(ffuncs.add), (*before, ca, *after)) for ca in call_args),
            )

rule_all_literals(ex)

All args are literals.

Source code in src/finch/finch_notation/proves.py 
27
28
29
30
31
32
33
34
35
36
37
38
def rule_all_literals(ex):
    """All args are literals."""
    match ex:
        case Call(L(op), args):
            lit_args = []
            for arg in args:
                match arg:
                    case L(val):
                        lit_args.append(val)
                    case _:
                        return None
            return L(op(*lit_args))

rule_associative_flatten(ex)

Flatten nested associative ops.

Source code in src/finch/finch_notation/proves.py 
57
58
59
60
61
62
63
64
65
66
67
def rule_associative_flatten(ex) -> Call | None:
    """Flatten nested associative ops."""
    match ex:
        case Call(
            NotationExpression(result_type=FinchOperatorFType() as op_type) as op, args
        ) if (
            is_associative(op_type)
            and (found := _find_first_call(args, op)) is not None
        ):
            before, call_args, after = found
            return Call(op, (*before, *call_args, *after))

rule_disjoint_flat_pair(ex, func1, func2)

Handle two mins/maxes in max/min.

Source code in src/finch/finch_notation/proves.py 
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
def rule_disjoint_flat_pair(ex, func1, func2) -> Call | None:
    """Handle two mins/maxes in max/min."""
    match ex:
        case Call(L(op), args) if (
            op == func1 and (found := _find_first_call(args, L(func2))) is not None
        ):
            before, call_args, after = found
            if (found2 := _find_first_call(after, L(func2))) is not None:
                before2, call_args2, after2 = found2
                if not is_disjoint(call_args, call_args2):
                    intersection = intersect(call_args, call_args2)
                    diff1 = setdiff(call_args, call_args2)
                    diff2 = setdiff(call_args2, call_args)
                    arg = Call(
                        L(func2),
                        (
                            *intersection,
                            Call(
                                L(func1), (Call(L(func2), diff1), Call(L(func2), diff2))
                            ),
                        ),
                    )
                    return Call(L(func1), (*before, arg, *before2, *after2))
            return None

rule_disjoint_flat_single(ex, func1, func2)

Remove min/max from max/min when disjoint.

Source code in src/finch/finch_notation/proves.py 
155
156
157
158
159
160
161
162
163
164
165
166
def rule_disjoint_flat_single(ex, func1, func2) -> Call | None:
    """
    Remove min/max from max/min when disjoint.
    """
    match ex:
        case Call(L(op), args) if (
            op == func1 and (found := _find_first_call(args, L(func2))) is not None
        ):
            before, call_args, after = found
            if not is_disjoint(before, call_args) or not is_disjoint(call_args, after):
                return Call(L(func1), (*before, *after))
            return None

rule_disjoint_nested(ex, func1, func2)

Handle nested max/min in min/max.

Source code in src/finch/finch_notation/proves.py 
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
def rule_disjoint_nested(ex, func1, func2) -> Call | None:
    """Handle nested max/min in min/max."""
    match ex:
        case Call(L(op), args) if (
            op == func1 and (found := _find_first_call(args, L(func2))) is not None
        ):
            before, call_args, after = found
            if (found2 := _find_first_call(call_args, L(func1))) is not None:
                before2, call_args2, after2 = found2
                if not is_disjoint(call_args2, before) or not is_disjoint(
                    call_args2, after
                ):
                    return Call(
                        L(func1),
                        (
                            *before,
                            Call(
                                L(func2),
                                (
                                    *before2,
                                    *setdiff(
                                        call_args2, itertools.chain(before, after)
                                    ),
                                    *after2,
                                ),
                            ),
                            *after,
                        ),
                    )
            return None

rule_equal_same(ex)

Match eq(a, a) => True.

Source code in src/finch/finch_notation/proves.py 
70
71
72
73
74
def rule_equal_same(ex) -> L | None:
    """Match eq(a, a) => True."""
    match ex:
        case Call(L(op), (a, b)) if op == ffuncs.eq and a == b:
            return L(True)

rule_ge(ex)

Transform ge(a, b) => eq(a, max(a, b)).

Source code in src/finch/finch_notation/proves.py 
77
78
79
80
81
def rule_ge(ex) -> Call | None:
    """Transform ge(a, b) => eq(a, max(a, b))."""
    match ex:
        case Call(L(op), (a, b)) if op == ffuncs.ge:
            return Call(L(ffuncs.eq), (a, Call(L(ffuncs.max), (a, b))))

rule_idempotent_unique(ex)

Remove duplicates from idempotent op.

Source code in src/finch/finch_notation/proves.py 
41
42
43
44
45
46
47
def rule_idempotent_unique(ex):
    """Remove duplicates from idempotent op."""
    match ex:
        case Call(
            NotationExpression(result_type=FinchOperatorFType() as op_type) as op, args
        ) if is_idempotent(op_type) and not all_unique(args):
            return Call(op, tuple(set(args)))

rule_le(ex)

Transform le(a, b) => eq(max(a, b), b).

Source code in src/finch/finch_notation/proves.py 
84
85
86
87
88
def rule_le(ex):
    """Transform le(a, b) => eq(max(a, b), b)."""
    match ex:
        case Call(L(op), (a, b)) if op == ffuncs.le:
            return Call(L(ffuncs.eq), (Call(L(ffuncs.max), (a, b)), b))

rule_single_arg(ex)

Collapse single-arg calls.

Source code in src/finch/finch_notation/proves.py 
50
51
52
53
54
def rule_single_arg(ex):
    """Collapse single-arg calls."""
    match ex:
        case Call(L(op), (arg,)) if op in (ffuncs.max, ffuncs.min):
            return arg