diff --git a/pyrtree/expr.py b/pyrtree/expr.py
new file mode 100644
index 0000000000000000000000000000000000000000..2f5844cdff4e9c3e1eb73ca0996200bced2c59d5
--- /dev/null
+++ b/pyrtree/expr.py
@@ -0,0 +1,161 @@
+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 \\\\")
diff --git a/pyrtree/rtree.py b/pyrtree/rtree.py
index a93abfd274f4dd6b0902c1504fa8a20e31008477..48efc46838366e50fcc81d3b3c94a21ce02c4718 100644
--- a/pyrtree/rtree.py
+++ b/pyrtree/rtree.py
@@ -1,66 +1,121 @@
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
- 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
+
+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:
+ 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 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 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 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 \\\\")
diff --git a/rtree/.hspec b/rtree/.hspec
index c2400d46e778ede4b598040489840e3a5efe5128..79ca47b48447094fd32f3286d03f7df43d69fddb 100644
--- a/rtree/.hspec
+++ b/rtree/.hspec
@@ -1,3 +1 @@
--failure-report .hspec-failures
---rerun
---rerun-all-on-success
diff --git a/rtree/test/expected/double-let-expr-ireda b/rtree/test/expected/double-let-expr-ireda
index 916380397f5dd67cd8a8011cec937fd1f4354720..e82fff577523180cdeabd176699e5a99f431b7cb 100644
--- a/rtree/test/expected/double-let-expr-ireda
+++ b/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
diff --git a/rtree/test/expected/double-overloading-let-expr-ireda b/rtree/test/expected/double-overloading-let-expr-ireda
index 2c814465a1fcf05d0897fe4be8c8c52ff08a42ee..b25d3a5592ed1f3e826435c4afb306ebe04ba931 100644
--- a/rtree/test/expected/double-overloading-let-expr-ireda
+++ b/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
diff --git a/rtree/test/expected/small-let-expr-ireda b/rtree/test/expected/small-let-expr-ireda
index 949bb8c3ffe7e114564b25c74c8aad3eb4f0ba56..7a796202634a54499fd98a24353c10203536cc06 100644
--- a/rtree/test/expected/small-let-expr-ireda
+++ b/rtree/test/expected/small-let-expr-ireda
@@ -1,3 +1,6 @@
***: x := 1; 2 + x True
1***: 2 + 1 True
11: 2 False
+101: 1 False
+1001: 3 False
+1000: 2 + 1 True
diff --git a/rtree/test/expected/small-opr-expr-ireda b/rtree/test/expected/small-opr-expr-ireda
index 3e134353344a847131c401e7c8270252c7e52482..305baee3578ff1ab14d5d8c667c92632c4802264 100644
--- a/rtree/test/expected/small-opr-expr-ireda
+++ b/rtree/test/expected/small-opr-expr-ireda
@@ -1,2 +1,5 @@
***: 1 + 2 True
1: 1 False
+01: 2 False
+001: 3 False
+000: 1 + 2 True
diff --git a/rtree/test/paper-examples/words b/rtree/test/paper-examples/words
new file mode 100644
index 0000000000000000000000000000000000000000..249759b0491e2085c90d7b66863df36947cfbe7a
--- /dev/null
+++ b/rtree/test/paper-examples/words
@@ -0,0 +1,27 @@
+┳â”┳â”┳â”┳â”┳â”┳┠"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"
+ â”—â” ""
diff --git a/rtree/test/paper-examples/words' b/rtree/test/paper-examples/words'
new file mode 100644
index 0000000000000000000000000000000000000000..f2d5d219b63a2d11886824ca6257631fd9c453ae
--- /dev/null
+++ b/rtree/test/paper-examples/words'
@@ -0,0 +1,64 @@
+┳â”┳â”┳â”┳â”┳â”┳┠"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"
+ â”—â” ""
diff --git a/rtree/test/src/Control/Monad/IRTreeSpec.hs b/rtree/test/src/Control/Monad/IRTreeSpec.hs
index 0bf6d60dd0710378d3d63d112081d9f9e4b4c719..d2023db5c298f2a4016f865768f3b78dd9a51194 100644
--- a/rtree/test/src/Control/Monad/IRTreeSpec.hs
+++ b/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
diff --git a/rtree/test/src/Control/Monad/RTreeSpec.hs b/rtree/test/src/Control/Monad/RTreeSpec.hs
index a1aee880bb34ab5a39386356943b8dcdca5dce9b..e6f0f684d5f206fd702de37c4394b5cb77a5bbad 100644
--- a/rtree/test/src/Control/Monad/RTreeSpec.hs
+++ b/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 ())