Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
from dataclasses import dataclass
from functools import partial
import rtree
@dataclass
class Let:
var: str
assignee: "Expr"
body: "Expr"
def replace(self, reps):
return Let(
self.var,
self.assignee.replace(reps),
self.body.replace(reps),
)
def eval(self, vals=None):
vals = vals or dict()
r = self.assignee.eval(vals)
vals = vals.copy()
vals[self.var] = r
return self.body.eval(vals)
def subterms(self):
yield self
yield from self.assignee.subterms()
yield from self.body.subterms()
def pretty(self, prec=0):
p = f"{self.var} := {self.assignee.pretty(2)}; {self.body.pretty(1)}"
if prec >= 1:
p = f"({p})"
return p
@dataclass
class Add:
lhs: "Expr"
rhs: "Expr"
def replace(self, reps):
return Add(
self.lhs.replace(reps),
self.rhs.replace(reps),
)
def subterms(self):
yield self
yield from self.lhs.subterms()
yield from self.rhs.subterms()
def pretty(self, n=0):
p = f"{self.lhs.pretty(4)} + {self.rhs.pretty(3)}"
if n >= 3:
p = f"({p})"
return p
def eval(self, vals=None):
vals = vals or dict()
lv = self.lhs.eval(vals)
rv = self.rhs.eval(vals)
return lv + rv
@dataclass
class Const:
n: int
def replace(self, _):
return self
def subterms(self):
yield self
def pretty(self, _=0):
return str(self.n)
def eval(self, _vals=None):
return self.n
@dataclass
class Var:
name: str
def replace(self, reps):
return reps.get(self.name, self)
def subterms(self):
yield self
def pretty(self, _=0):
return self.name
def eval(self, vals=None):
vals = vals or dict()
return vals.get(self.name, -1)
Expr = Let | Add | Const | Var
def reduce_expr(expr: Expr, check) -> Expr:
if isinstance(expr, Var):
return expr
elif isinstance(expr, Const):
if not expr.n == 0 and check("1) make zero"):
return Const(0)
return expr
elif isinstance(expr, Add):
lhs_ = reduce_expr(expr.lhs, check)
rhs_ = reduce_expr(expr.rhs, check)
if check("2) reduce to lhs"):
return lhs_
if check("3) reduce to rhs"):
return rhs_
return Add(lhs_, rhs_)
elif isinstance(expr, Let):
assignee_ = reduce_expr(expr.assignee, check)
return assignee_
if check(f"5) inline {expr.var!r}"):
return reduce_expr(expr.body.replace({expr.var: assignee_}), check)
body_ = reduce_expr(expr.body, check)
return Let(expr.var, assignee_, body_)
if __name__ == "__main__":
expr = Let(
"x", Const(2), Add(Const(1), Let("y", Var("x"), Add(Const(3), Var("y"))))
)
def input_format(a):
return f"$\\syn{{{a.pretty()}}}$"
p = rtree.latex(
lambda e: any(isinstance(a, Add) for a in e.subterms()),
query_format=str,
input_format=input_format,
start_count=0,
)
rt = partial(reduce_expr, expr)
p(rtree.Probe(rt, []))
rp = rtree.reduce(p, rt)
print(f"& \\verb|{rtree.pretty(rp)}| & {input_format(rp.input)} & true \\\\")
print()
p = rtree.latex(
lambda e: e.eval() == expr.eval(),
query_format=str,
input_format=input_format,
start_count=0,
)
rt = partial(reduce_expr, expr)
p(rtree.Probe(rt, []))
rp = rtree.reduce(p, rt)