Changes from the paper

pyrtree/expr.py

+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):
+        if check("2) reduce to lhs"):
+            return reduce_expr(expr.lhs, check)
+        if check("3) reduce to rhs"):
+            return reduce_expr(expr.rhs, check)
+        lhs_ = reduce_expr(expr.lhs, check)
+        rhs_ = reduce_expr(expr.rhs, check)
+        return Add(lhs_, rhs_)
+    elif isinstance(expr, Let):
+        assignee_ = reduce_expr(expr.assignee, check)
+        if check("4) reduce to lhs"):
+            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"&& {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)
+    print(f"& {rtree.pretty{rp}} & {input_format(rp.input)} & true \\\\")

pyrtree/rtree.py

 from dataclasses import dataclass
 
 
-@dataclass
-class ReducePath:
-    path: list[bool]
-    reasons: list[str]
+class Probe:
+    def __init__(self, rtree, path, guess_depth=0):
+        """Test an rtree with a path, and optional number of guesses"""
+        self.path = path + [True] * guess_depth
+        self.depth = guess_depth
+        self.reasons = []
 
-    @classmethod
-    def empty(cls):
-        return cls([], [])
+        def check(reason: str):
+            """Check the path or default to false"""
+            self.reasons.append(reason)
+            return self.undecided() <= 0 and self.path[len(self.reasons) - 1]
 
-    def explore(self, choice):
-        self.reasons = []
-        self.path.append(choice)
-        return self
+        self.input = rtree(check)
 
-    def left(self):
+    def undecided(self):
+        """The number of choices left on the path"""
         return len(self.reasons) - len(self.path)
 
-    def check(self, reason: str):
-        self.reasons.append(reason)
-        try:
-            return self.path[len(self.reasons) - 1]
-        except IndexError:
-            return False
-
-
-def reduce(predicate, reducer, i):
-    r = ReducePath.empty()
-    j = i
-    ix = reducer(i, r.explore(True))
-    # While we don't consume all choices going down the true branch
-    while r.left() >= 0:
-        print(r.reasons[len(r.path) - 1], "...", end="")
-        if predicate(ix):
-            # If true update the valid input
-            print(" Yes")
-            j = ix
+
+def reduce(predicate, rtree):
+    # Extract the initial reduction probe, from the rightmost branch.
+    rp = Probe(rtree, [])
+    # Run exponential search after the depest sequence of trues
+    # that can be appended to the path without failing the predicate
+    depth = 1
+    # Invariant: predicate(rp) == True
+    while rp.undecided() > 0:
+        # Try to probe the with current path extended by trues trues.
+        if predicate(rp_ := Probe(rtree, rp.path, depth)):
+            rp, depth = rp_, depth * 2
+            continue
+        # Adjust the depth so that none of them are wasted.
+        depth += min(0, rp_.undecided())
+        # Perform a binary search, accepting the nessarary trues, and
+        # reducing the unknown trues to 1:
+        while depth > 1:
+            # Prope the rtree with the current path extended by half the depth.
+            if predicate(rp_ := Probe(rtree, rp.path, depth // 2)):
+                rp = rp_  # Accept the current path.
+                depth -= depth // 2  # And try the remaining half
             else:
-            # If false we have to go down the left branch.
-            print(" No")
-            r.path[-1] = False
-        ix = reducer(i, r.explore(True))
-    return j
+                depth //= 2  # Half the current trues
+        # Store that the next element in the path has to be false
+        rp.path.append(False)
+    # return the input.
+    return rp
 
 
 def debug(predicate):
-    def newpred(i):
-        t = predicate(i)
-        print(" test", i, "...", end="")
+    counter = 0
+
+    def newpred(rp):
+        nonlocal counter
+        counter += 1
+        t = predicate(rp.input)
+        print(
+            f"{counter:02})",
+            ", ".join(rp.reasons[len(rp.path) - rp.depth : len(rp.path)]),
+        )
+        print(f"... P({rp.input!r}) = {t}")
+        return t
+
+    return newpred
+
+
+def latex(
+    predicate,
+    query_format="Remove {}?".format,
+    input_format="\\verb|{}|".format,
+    start_count=0,
+):
+    counter = start_count - 1
+
+    def newpred(rp):
+        nonlocal counter
+        counter += 1
+        t = predicate(rp.input)
+        query = ", ".join(rp.reasons[len(rp.path) - rp.depth : len(rp.path)])
+        theck = "true" if t else "false"
+
+        print(
+            f"{counter:02} & \\verb|{pretty(rp)}| & {query_format(query)} & {input_format(rp.input)} & {theck} \\\\"
+        )
         return t
 
     return newpred
 
 
-def reduce_set(i: set, r) -> set:
-    result: set = set()
-    for e in sorted(i):
-        if not r.check(f"remove {e}?"):
-            result.add(e)
+def pretty(rp):
+    from itertools import zip_longest
+
+    def binary(a):
+        return "1" if a else "0"
+
+    return "".join(
+        a for a, _ in zip_longest(map(binary, rp.path), rp.reasons, fillvalue="*")
+    )
+
+
+def reduce_abc(check) -> str:
+    result = ""
+    for x in "abcdefghijklmnopqrstuvxyz":
+        if not check(f"{x}"):
+            result += x
+        else:
+            result += " "
     return result
 
 
 if __name__ == "__main__":
-    reduce(debug(lambda a: "a" in a), reduce_set, {"a", "b", "c"})
+    p = latex(
+        lambda e: "a" in e or "p" in e,
+        start_count=0,
+    )
+    input_format = "\\verb|{}|".format
+    p(Probe(reduce_abc, []))
+    rp = reduce(p, reduce_abc)
+    print(f"&& {input_format(rp.input)} & true \\\\")

rtree/.hspec

 --failure-report .hspec-failures
---rerun
---rerun-all-on-success

rtree/test/expected/double-let-expr-ireda

@@ -2,3 +2,6 @@
 1***: y := 2; 1 + y True
 11***: 1 + 2 True
 111: 1 False
+1101: 2 False
+11001: 3 False
+11000: 1 + 2 True

rtree/test/expected/double-overloading-let-expr-ireda

@@ -2,3 +2,6 @@
 1***: x := 2; x + x True
 11***: 2 + 2 True
 111: 2 False
+1101: 2 False
+11001: 4 False
+11000: 2 + 2 True

rtree/test/expected/small-let-expr-ireda

 ***: x := 1; 2 + x True
 1***: 2 + 1 True
 11: 2 False
+101: 1 False
+1001: 3 False
+1000: 2 + 1 True

rtree/test/expected/small-opr-expr-ireda

 ***: 1 + 2 True
 1: 1 False
+01: 2 False
+001: 3 False
+000: 1 + 2 True

rtree/test/paper-examples/words

+┳━┳━┳━┳━┳━┳━ "ABc"
+┃ ┃ ┃ ┃ ┃ ┗━ "aBc"
+┃ ┃ ┃ ┃ ┗━┳━ "Abc"
+┃ ┃ ┃ ┃   ┗━ "abc"
+┃ ┃ ┃ ┗━┳━┳━ "ABc"
+┃ ┃ ┃   ┃ ┗━ "aBc"
+┃ ┃ ┃   ┗━┳━ "Abc"
+┃ ┃ ┃     ┗━ "abc"
+┃ ┃ ┗━┳━┳━ "Bc"
+┃ ┃   ┃ ┗━ "bc"
+┃ ┃   ┗━┳━ "Bc"
+┃ ┃     ┗━ "bc"
+┃ ┗━┳━┳━┳━ "Ac"
+┃   ┃ ┃ ┗━ "ac"
+┃   ┃ ┗━┳━ "Ac"
+┃   ┃   ┗━ "ac"
+┃   ┗━┳━ "c"
+┃     ┗━ "c"
+┗━┳━┳━┳━┳━ "AB"
+  ┃ ┃ ┃ ┗━ "aB"
+  ┃ ┃ ┗━┳━ "Ab"
+  ┃ ┃   ┗━ "ab"
+  ┃ ┗━┳━ "B"
+  ┃   ┗━ "b"
+  ┗━┳━┳━ "A"
+    ┃ ┗━ "a"
+    ┗━ ""

rtree/test/paper-examples/words'

+┳━┳━┳━┳━┳━┳━ "ABc"
+┃ ┃ ┃ ┃ ┃ ┗━ "Bc"
+┃ ┃ ┃ ┃ ┗━┳━ "Ac"
+┃ ┃ ┃ ┃   ┗━ "c"
+┃ ┃ ┃ ┗━┳━┳━ "AB"
+┃ ┃ ┃   ┃ ┗━ "B"
+┃ ┃ ┃   ┗━┳━ "A"
+┃ ┃ ┃     ┗━ ""
+┃ ┃ ┗━┳━┳━┳━ "aBc"
+┃ ┃   ┃ ┃ ┗━ "Bc"
+┃ ┃   ┃ ┗━┳━ "ac"
+┃ ┃   ┃   ┗━ "c"
+┃ ┃   ┗━┳━┳━ "aB"
+┃ ┃     ┃ ┗━ "B"
+┃ ┃     ┗━┳━ "a"
+┃ ┃       ┗━ ""
+┃ ┗━┳━┳━┳━┳━ "Abc"
+┃   ┃ ┃ ┃ ┗━ "bc"
+┃   ┃ ┃ ┗━┳━ "Ac"
+┃   ┃ ┃   ┗━ "c"
+┃   ┃ ┗━┳━┳━ "Ab"
+┃   ┃   ┃ ┗━ "b"
+┃   ┃   ┗━┳━ "A"
+┃   ┃     ┗━ ""
+┃   ┗━┳━┳━┳━ "abc"
+┃     ┃ ┃ ┗━ "bc"
+┃     ┃ ┗━┳━ "ac"
+┃     ┃   ┗━ "c"
+┃     ┗━┳━┳━ "ab"
+┃       ┃ ┗━ "b"
+┃       ┗━┳━ "a"
+┃         ┗━ ""
+┗━┳━┳━┳━┳━┳━ "ABc"
+  ┃ ┃ ┃ ┃ ┗━ "Bc"
+  ┃ ┃ ┃ ┗━┳━ "Ac"
+  ┃ ┃ ┃   ┗━ "c"
+  ┃ ┃ ┗━┳━┳━ "AB"
+  ┃ ┃   ┃ ┗━ "B"
+  ┃ ┃   ┗━┳━ "A"
+  ┃ ┃     ┗━ ""
+  ┃ ┗━┳━┳━┳━ "aBc"
+  ┃   ┃ ┃ ┗━ "Bc"
+  ┃   ┃ ┗━┳━ "ac"
+  ┃   ┃   ┗━ "c"
+  ┃   ┗━┳━┳━ "aB"
+  ┃     ┃ ┗━ "B"
+  ┃     ┗━┳━ "a"
+  ┃       ┗━ ""
+  ┗━┳━┳━┳━┳━ "Abc"
+    ┃ ┃ ┃ ┗━ "bc"
+    ┃ ┃ ┗━┳━ "Ac"
+    ┃ ┃   ┗━ "c"
+    ┃ ┗━┳━┳━ "Ab"
+    ┃   ┃ ┗━ "b"
+    ┃   ┗━┳━ "A"
+    ┃     ┗━ ""
+    ┗━┳━┳━┳━ "abc"
+      ┃ ┃ ┗━ "bc"
+      ┃ ┗━┳━ "ac"
+      ┃   ┗━ "c"
+      ┗━┳━┳━ "ab"
+        ┃ ┗━ "b"
+        ┗━┳━ "a"
+          ┗━ ""

rtree/test/src/Control/Monad/IRTreeSpec.hs

@@ -33,8 +33,8 @@ expsearchSpec = describe "expsearch" do
   it "should guess a number between 0 and 10" do
     expsearch (\a -> do pure (a <= 6, 10 - a)) `shouldReturn` (6, True)
     expsearch (\a -> do pure (a <= 3, 10 - a)) `shouldReturn` (3, True)
-    expsearch (\a -> do pure (a <= 9, 10 - a)) `shouldReturn` (9, False)
-    expsearch (\a -> do pure (a <= 12, 10 - a)) `shouldReturn` (9, False)
+    expsearch (\a -> do pure (a <= 9, 10 - a)) `shouldReturn` (9, True)
+    expsearch (\a -> do pure (a <= 12, 10 - a)) `shouldReturn` (9, True)
 
 examplesSpec :: Spec
 examplesSpec = describe "examples" do

rtree/test/src/Control/Monad/RTreeSpec.hs

@@ -8,6 +8,7 @@ module Control.Monad.RTreeSpec where
 import Control.Monad.Identity (Identity (runIdentity))
 import Control.Monad.RTree
 import Control.Monad.Reader
+import qualified Data.Char as Char
 import Data.Expr as Expr
 import Data.Foldable
 import Data.Functor
@@ -30,6 +31,7 @@ spec = do
   rtreeSpec
   rtreeTSpec
   examplesSpec
+  paperSpec
 
 rtreeTSpec :: Spec
 rtreeTSpec = describe "RTreeT" do
@@ -116,3 +118,22 @@ examplesSpec = describe "example" do
       forM_ (iinputs re) \(ii, e') -> do
         p <- toPredicate ii
         reduce p re `shouldReturn` e'
+
+listR :: [a] -> RTree String [a]
+listR [] = pure []
+listR (a : as) = listR as >>= \as' -> pure as' <| pure (a : as')
+
+lowerR :: [Char] -> RTree String [Char]
+lowerR [] = pure []
+lowerR (a : as) = lowerR as >>= \as' -> pure (Char.toLower a : as') <| pure (a : as')
+
+paperSpec :: Spec
+paperSpec = do
+  onGlitter
+    "test/paper-examples/words"
+    (`writeFile` drawRTree showString shows (listR "ABc" >>= lowerR))
+    (pure ())
+  onGlitter
+    "test/paper-examples/words'"
+    (`writeFile` drawRTree showString shows (lowerR "ABc" >>= listR))
+    (pure ())