perf: index once in rewalk, bind.refresh and digest.laws_of (#228)

src/rules/PROOF.bend

@@ -13785,82 +13785,56 @@ def rewalk.single_eq(hh, piece):
         Laws.rewalk.reads(piece, binder, False{}, 0n, False{}, False{}),
         rewalk.reads_eq(piece, binder, False{}, 0n, False{}, False{}))
 
-# a twin keeps its whole result, to the rule and to the law
-law rewalk.full_eq:
-  for b: Bool
-  for +hh: Rewalk.How
-  for +piece: Tree.Node
-  {Rewalk.other_full(b, hh, piece) == Bool.and(b, Bool.not(Laws.rewalk.single(hh, piece))) : Bool}
-
-def rewalk.full_eq(b, hh, piece):
-  match b:
-    case False{}:
-      {==}
-    case True{}:
-      Equal.cong(Bool, Bool, x => Bool.not(x), Rewalk.narrow(hh, piece), Laws.rewalk.single(hh, piece),
-        rewalk.single_eq(hh, piece))
-
-# a twin is read for a single value, to the rule and to the law
-law rewalk.nar_eq:
-  for b: Bool
-  for +hh: Rewalk.How
-  for +piece: Tree.Node
-  {Rewalk.earlier_nar(b, hh, piece) == Bool.and(b, Laws.rewalk.single(hh, piece)) : Bool}
-
-def rewalk.nar_eq(b, hh, piece):
-  match b:
-    case False{}:
-      {==}
-    case True{}:
-      rewalk.single_eq(hh, piece)
-
-# the rule's other_go is the law's whole
+# the rule's other_go over the rated sites is the law's whole
 law rewalk.whole_eq:
   for sites: List<&2, Rewalk.Site>
   for +name: String
   for +args: String
   for +line: U32
   for +col: U32
   for +piece: Tree.Node
-  {Rewalk.other_go(sites, name, args, line, col, piece) == Laws.rewalk.whole(sites, name, args, line, col, piece)
-    : Bool}
+  {Rewalk.other_go(Rewalk.rate(sites, piece), name, args, line, col)
+    == Laws.rewalk.whole(sites, name, args, line, col, piece) : Bool}
 
 def rewalk.whole_eq(sites, name, args, line, col, piece):
   match sites:
     case Nil{}:
       {==}
-    case Con{s, rest}:
+    case Con{s, +rest}:
       match s:
         case Rewalk.Site{+nm, +as, +l, +c, len, +how}:
           +tw = Laws.rewalk.twin(nm, as, l, c, name, args, line, col)
-          %rewalk.full_eq(tw, how, piece) : {Rewalk.other_go(Rewalk.Site{nm, as, l, c, len, how} <> rest, name, args,
-            line, col, piece) == Bool.or(_, Laws.rewalk.whole(rest, name, args, line, col, piece)) : Bool}
-          %rewalk.whole_eq(rest, name, args, line, col, piece) : {Rewalk.other_go(Rewalk.Site{nm, as, l, c, len, how}
-            <> rest, name, args, line, col, piece) == Bool.or(Rewalk.other_full(tw, how, piece), _) : Bool}
+          +lhs = Rewalk.other_go(Rewalk.rate(Rewalk.Site{nm, as, l, c, len, how} <> rest, piece), name, args, line, col)
+          %rewalk.single_eq(how, piece) : {lhs == Bool.or(Bool.and(tw, Bool.not(_)),
+            Laws.rewalk.whole(rest, name, args, line, col, piece)) : Bool}
+          %rewalk.whole_eq(rest, name, args, line, col, piece) : {lhs
+            == Bool.or(Bool.and(tw, Bool.not(Rewalk.narrow(how, piece))), _) : Bool}
           {==}
 
-# the rule's earlier is the law's prior
+# the rule's earlier over the rated sites is the law's prior
 law rewalk.prior_eq:
   for seen: List<&2, Rewalk.Site>
   for +name: String
   for +args: String
   for +line: U32
   for +col: U32
   for +piece: Tree.Node
-  {Rewalk.earlier(seen, name, args, line, col, piece) == Laws.rewalk.prior(seen, name, args, line, col, piece) : Bool}
+  {Rewalk.earlier(Rewalk.rate(seen, piece), name, args, line, col)
+    == Laws.rewalk.prior(seen, name, args, line, col, piece) : Bool}
 
 def rewalk.prior_eq(seen, name, args, line, col, piece):
   match seen:
     case Nil{}:
       {==}
-    case Con{s, rest}:
+    case Con{s, +rest}:
       match s:
         case Rewalk.Site{+nm, +as, +l, +c, len, +how}:
           +tw = Laws.rewalk.twin(nm, as, l, c, name, args, line, col)
-          %rewalk.nar_eq(tw, how, piece) : {Rewalk.earlier(Rewalk.Site{nm, as, l, c, len, how} <> rest, name, args,
-            line, col, piece) == Bool.or(_, Laws.rewalk.prior(rest, name, args, line, col, piece)) : Bool}
-          %rewalk.prior_eq(rest, name, args, line, col, piece) : {Rewalk.earlier(Rewalk.Site{nm, as, l, c, len, how}
-            <> rest, name, args, line, col, piece) == Bool.or(Rewalk.earlier_nar(tw, how, piece), _) : Bool}
+          +lhs = Rewalk.earlier(Rewalk.rate(Rewalk.Site{nm, as, l, c, len, how} <> rest, piece), name, args, line, col)
+          %rewalk.single_eq(how, piece) : {lhs == Bool.or(Bool.and(tw, _),
+            Laws.rewalk.prior(rest, name, args, line, col, piece)) : Bool}
+          %rewalk.prior_eq(rest, name, args, line, col, piece) : {lhs
+            == Bool.or(Bool.and(tw, Rewalk.narrow(how, piece)), _) : Bool}
           {==}
 
 # a narrow site with no narrow twin before it: one finding
@@ -13888,52 +13862,51 @@ def rewalk.nar_len(n, p, _name, _line, _col, _len, _path):
 # finding
 law rewalk.dup_len:
   for d: Bool
-  for +how: Rewalk.How
+  for +nar: Bool
   for +name: String
   for +args: String
   for +line: U32
   for +col: U32
   for +len: U32
-  for +body: Tree.Node
   for +path: String
-  for +seen: List<&2, Rewalk.Site>
-  {List.length(&2, F.Finding, Rewalk.report_dup(d, how, name, args, line, col, len, body, path, seen))
-    == Bool.pick(Nat, Bool.and(d, Bool.and(Rewalk.narrow(how, body), Bool.not(Rewalk.earlier(seen, name, args, line,
-      col, body)))), 1n, 0n) : Nat}
+  for +seen: List<&2, Rewalk.Rated>
+  {List.length(&2, F.Finding, Rewalk.report_dup(d, nar, name, args, line, col, len, path, seen))
+    == Bool.pick(Nat, Bool.and(d, Bool.and(nar, Bool.not(Rewalk.earlier(seen, name, args, line, col)))), 1n, 0n)
+    : Nat}
 
-def rewalk.dup_len(d, how, name, args, line, col, len, body, path, seen):
+def rewalk.dup_len(d, nar, name, args, line, col, len, path, seen):
   match d:
     case False{}:
       {==}
     case True{}:
-      rewalk.nar_len(Rewalk.narrow(how, body), Rewalk.earlier(seen, name, args, line, col, body), name, line, col, len,
-        path)
+      rewalk.nar_len(nar, Rewalk.earlier(seen, name, args, line, col), name, line, col, len, path)
 
-# one site: one finding when the law flags it, none otherwise
+# one site, rated: one finding when the law flags it, none otherwise
 law rewalk.one_len:
   for s: Rewalk.Site
   for +all: List<&2, Rewalk.Site>
   for +body: Tree.Node
   for +path: String
   for +seen: List<&2, Rewalk.Site>
-  {List.length(&2, F.Finding, Rewalk.report_one(s, all, body, path, seen))
-    == Bool.pick(Nat, Laws.rewalk.flag(s, all, body, seen), 1n, 0n) : Nat}
+  {List.length(&2, F.Finding, Rewalk.report_one(Rewalk.rate_one(s, body), Rewalk.rate(all, body), path,
+    Rewalk.rate(seen, body))) == Bool.pick(Nat, Laws.rewalk.flag(s, all, body, seen), 1n, 0n) : Nat}
 
 def rewalk.one_len(s, all, body, path, seen):
   match s:
     case Rewalk.Site{+name, +args, +line, +col, +len, +how}:
-      +lhs = List.length(&2, F.Finding, Rewalk.report_one(Rewalk.Site{name, args, line, col, len, how}, all, body, path,
-        seen))
+      +lhs = List.length(&2, F.Finding, Rewalk.report_one(Rewalk.rate_one(Rewalk.Site{name, args, line, col, len, how},
+        body), Rewalk.rate(all, body), path, Rewalk.rate(seen, body)))
       %rewalk.whole_eq(all, name, args, line, col, body) : {lhs == Bool.pick(Nat, Bool.and(_,
         Bool.and(Laws.rewalk.single(how, body), Bool.not(Laws.rewalk.prior(seen, name, args, line, col, body)))), 1n,
           0n)
         : Nat}
-      %rewalk.single_eq(how, body) : {lhs == Bool.pick(Nat, Bool.and(Rewalk.other_go(all, name, args, line, col, body),
-        Bool.and(_, Bool.not(Laws.rewalk.prior(seen, name, args, line, col, body)))), 1n, 0n) : Nat}
-      %rewalk.prior_eq(seen, name, args, line, col, body) : {lhs == Bool.pick(Nat, Bool.and(Rewalk.other_go(all, name,
-        args, line, col, body), Bool.and(Rewalk.narrow(how, body), Bool.not(_))), 1n, 0n) : Nat}
-      rewalk.dup_len(Rewalk.other_go(all, name, args, line, col, body), how, name, args, line, col, len, body, path,
-        seen)
+      %rewalk.single_eq(how, body) : {lhs == Bool.pick(Nat, Bool.and(Rewalk.other_go(Rewalk.rate(all, body), name,
+        args, line, col), Bool.and(_, Bool.not(Laws.rewalk.prior(seen, name, args, line, col, body)))), 1n, 0n) : Nat}
+      %rewalk.prior_eq(seen, name, args, line, col, body) : {lhs == Bool.pick(Nat, Bool.and(Rewalk.other_go(
+        Rewalk.rate(all, body), name, args, line, col), Bool.and(Rewalk.narrow(how, body), Bool.not(_))), 1n, 0n)
+        : Nat}
+      rewalk.dup_len(Rewalk.other_go(Rewalk.rate(all, body), name, args, line, col), Rewalk.narrow(how, body), name,
+        args, line, col, len, path, Rewalk.rate(seen, body))
 
 # a flag's one or none, onto the rest's count
 law rewalk.add_pick:
@@ -13948,23 +13921,23 @@ def rewalk.add_pick(f, _m):
     case False{}:
       {==}
 
-# the rule's report counts what the law counts
+# the rule's report over the rated sites counts what the law counts
 law rewalk.report_len:
   for sites: List<&2, Rewalk.Site>
   for +all: List<&2, Rewalk.Site>
   for +body: Tree.Node
   for +path: String
   for +seen: List<&2, Rewalk.Site>
-  {List.length(&2, F.Finding, Rewalk.report(sites, all, body, path, seen))
-    == Laws.rewalk.count(sites, all, body, seen) : Nat}
+  {List.length(&2, F.Finding, Rewalk.report(Rewalk.rate(sites, body), Rewalk.rate(all, body), path,
+    Rewalk.rate(seen, body))) == Laws.rewalk.count(sites, all, body, seen) : Nat}
 
 def rewalk.report_len(sites, all, body, path, seen):
   match sites:
     case Nil{}:
       {==}
     case Con{+s, +rest}:
-      +one = Rewalk.report_one(s, all, body, path, seen)
-      +tl = Rewalk.report(rest, all, body, path, s <> seen)
+      +one = Rewalk.report_one(Rewalk.rate_one(s, body), Rewalk.rate(all, body), path, Rewalk.rate(seen, body))
+      +tl = Rewalk.report(Rewalk.rate(rest, body), Rewalk.rate(all, body), path, Rewalk.rate(s <> seen, body))
       +f = Laws.rewalk.flag(s, all, body, seen)
       +m = Laws.rewalk.count(rest, all, body, s <> seen)
       Equal.trans(Nat, List.length(&2, F.Finding, List.append(&2, F.Finding, one, tl)),
@@ -13998,8 +13971,8 @@ def rewalk.sites_eq(nn, self, lp):
 
 def Laws.rewalk_local_counts(nn, self, lp, path):
   +ss = Rewalk.pin(Rewalk.mark(nn), Rewalk.apply(nn, Rewalk.gather(nn, self, lp, Rewalk.binds(nn, []))))
-  %rewalk.sites_eq(nn, self, lp) : {List.length(&2, F.Finding, Rewalk.report(ss, ss, nn, path, []))
-    == Laws.rewalk.count(_, _, nn, []) : Nat}
+  %rewalk.sites_eq(nn, self, lp) : {List.length(&2, F.Finding, Rewalk.report(Rewalk.rate(ss, nn), Rewalk.rate(ss, nn),
+    path, [])) == Laws.rewalk.count(_, _, nn, []) : Nat}
   rewalk.report_len(ss, ss, nn, path, [])
 
 # two finding lists joined: the counts added

src/rules/digest.bend

@@ -307,13 +307,38 @@ def doc_at(items: List<&2, Outline.Item>, +at: U32) -> String:
     case Con{Outline.Item{kk, nn, +ln, sig, +doc, pp}, rest}:
       Lazy.stop(String, U32.is_le(at, ln), Bool.pick(String, U32.is_eq(ln, at), doc, ""), _u => doc_at(rest, at))
 
-# every law of a tree, with whether it binds and its doc lines
+# does the first item sit on or after a line (from_line stops there)?
+def from_line.stop(items: List<&2, Outline.Item>, +at: U32) -> Bool:
+  match items:
+    case Nil{}:
+      True{}
+    case Con{Outline.Item{kk, nn, +ln, sig, doc, pp}, rest}:
+      U32.is_le(at, ln)
+
+# the items from the first on or after a line; the items are in line order,
+# and so are a tree's laws, so an item this drops lies above every later law
+# too. stop is from_line.stop of items, carried so the step stays a loop
+def from_line(items: List<&2, Outline.Item>, +at: U32, +stop: Bool) -> List<&2, Outline.Item>:
+  match items:
+    case Nil{}:
+      Nil{}
+    case Con{h, +rest}:
+      match stop:
+        case True{}:
+          h <> rest
+        case False{}:
+          from_line(rest, at, from_line.stop(rest, at))
+
+# every law of a tree, with whether it binds and its doc lines. items is a
+# cursor: each law's search starts where the last one stopped, so the items
+# are read once over all the laws, not once per law
 def laws_of(root: Tree.Node, +items: List<&2, Outline.Item>) -> List<&2, Law>:
   match root:
     case Tree.NCons{Tree.Stmt{Tree.SLaw{}, +kids, body}, rest}:
       +at = Tree.line(kids)
-      dd = doc_at(items, at)
-      Law{Closed.name.of(Bind.declared(kids)), at, Closed.binds(body), String.lines(dd)} <> laws_of(rest, items)
+      +left = from_line(items, at, from_line.stop(items, at))
+      dd = doc_at(left, at)
+      Law{Closed.name.of(Bind.declared(kids)), at, Closed.binds(body), String.lines(dd)} <> laws_of(rest, left)
     case Tree.NCons{h, rest}:
       laws_of(rest, items)
     case other:

src/rules/suspicious/rewalk.bend

@@ -756,49 +756,46 @@ def pin(+ps: List<&2, Pos>, sites: List<&2, Site>) -> List<&2, Site>:
     case Con{s, rest}:
       pin_one(ps, s) <> pin(ps, rest)
 
-# the other site keeps the whole result
-def other_full(+yes: Bool, how: How, +body: Tree.Node) -> Bool:
-  match yes:
-    case False{}:
-      False{}
-    case True{}:
-      Bool.not(narrow(how, body))
+# a site, with whether its result is read for a single value over the piece
+type Rated is Data:
+  Rated{site: Site, nar: Bool}
+
+# one site, rated: the piece is walked for it here, once
+def rate_one(ss: Site, +body: Tree.Node) -> Rated:
+  Site{+name, +args, +line, +col, +len, +how} = ss
+  Rated{Site{name, args, line, col, len, how}, narrow(how, body)}
+
+# each site, rated once, so the reports below compare ratings and never walk
+# the piece again: a walk per site, not one per pair of sites
+def rate(sites: List<&2, Site>, +body: Tree.Node) -> List<&2, Rated>:
+  match sites:
+    case Nil{}:
+      Nil{}
+    case Con{s, rest}:
+      rate_one(s, body) <> rate(rest, body)
 
 # another site has the same callee and the same arguments, and keeps the whole result
-def other_go(sites: List<&2, Site>, +name: String, +args: String, +line: U32, +col: U32, +body: Tree.Node) -> Bool:
-  match sites:
+def other_go(rs: List<&2, Rated>, +name: String, +args: String, +line: U32, +col: U32) -> Bool:
+  match rs:
     case Nil{}:
       False{}
-    case Con{Site{+nm, +as, +l, +c, len, how}, rest}:
+    case Con{Rated{Site{+nm, +as, +l, +c, len, how}, +nar}, rest}:
       +same = Bool.and(String.eq(nm, name), String.eq(as, args))
       +diff = Bool.not(Bool.and(U32.is_eq(l, line), U32.is_eq(c, col)))
-      +here = other_full(Bool.and(same, diff), how, body)
-      +more = other_go(rest, name, args, line, col, body)
+      +here = Bool.and(Bool.and(same, diff), Bool.not(nar))
+      +more = other_go(rest, name, args, line, col)
       Bool.or(here, more)
 
-# this earlier site is a narrow read of the same call
-def earlier_nar(+yes: Bool, how: How, +body: Tree.Node) -> Bool:
-  match yes:
-    case False{}:
-      False{}
-    case True{}:
-      narrow(how, body)
-
-# this earlier site is a narrow read of the same call
-def earlier_one(ss: Site, +name: String, +args: String, +line: U32, +col: U32, +body: Tree.Node) -> Bool:
-  Site{+nm, +as, +l, +c, len, how} = ss
-  +same = Bool.and(String.eq(nm, name), String.eq(as, args))
-  +diff = Bool.not(Bool.and(U32.is_eq(l, line), U32.is_eq(c, col)))
-  earlier_nar(Bool.and(same, diff), how, body)
-
 # a narrow site of this call already reported
-def earlier(seen: List<&2, Site>, +name: String, +args: String, +line: U32, +col: U32, +body: Tree.Node) -> Bool:
+def earlier(seen: List<&2, Rated>, +name: String, +args: String, +line: U32, +col: U32) -> Bool:
   match seen:
     case Nil{}:
       False{}
-    case Con{s, rest}:
-      +here = earlier_one(s, name, args, line, col, body)
-      +more = earlier(rest, name, args, line, col, body)
+    case Con{Rated{Site{+nm, +as, +l, +c, len, how}, +nar}, rest}:
+      +same = Bool.and(String.eq(nm, name), String.eq(as, args))
+      +diff = Bool.not(Bool.and(U32.is_eq(l, line), U32.is_eq(c, col)))
+      +here = Bool.and(Bool.and(same, diff), nar)
+      +more = earlier(rest, name, args, line, col)
       Bool.or(here, more)
 
 # the finding when no earlier narrow site took this call
@@ -836,53 +833,40 @@ def report_nar(
 # the finding when a duplicate exists and this site is the first narrow one
 def report_dup(
   +dup: Bool,
-  how: How,
+  +nar: Bool,
   +name: String,
   +args: String,
   +line: U32,
   +col: U32,
   +len: U32,
-  +body: Tree.Node,
   +path: String,
-  +seen: List<&2, Site>
+  +seen: List<&2, Rated>
 ) -> List<&2, F.Finding>:
   match dup:
     case False{}:
       Nil{}
     case True{}:
-      report_nar(narrow(how, body), earlier(seen, name, args, line, col, body), name, line, col, len, path)
-
+      report_nar(nar, earlier(seen, name, args, line, col), name, line, col, len, path)
 
 # one site
-def report_one(
-  ss: Site,
-  +all: List<&2, Site>,
-  +body: Tree.Node,
-  +path: String,
-  +seen: List<&2, Site>
-) -> List<&2, F.Finding>:
+def report_one(rr: Rated, +all: List<&2, Rated>, +path: String, +seen: List<&2, Rated>) -> List<&2, F.Finding>:
+  Rated{ss, +nar} = rr
   Site{+name, +args, +line, +col, +len, how} = ss
-  report_dup(other_go(all, name, args, line, col, body), how, name, args, line, col, len, body, path, seen)
+  report_dup(other_go(all, name, args, line, col), nar, name, args, line, col, len, path, seen)
 
 # the first narrow site of each duplicated call
-def report(
-  sites: List<&2, Site>,
-  +all: List<&2, Site>,
-  +body: Tree.Node,
-  +path: String,
-  +seen: List<&2, Site>
-) -> List<&2, F.Finding>:
-  match sites:
+def report(rs: List<&2, Rated>, +all: List<&2, Rated>, +path: String, +seen: List<&2, Rated>) -> List<&2, F.Finding>:
+  match rs:
     case Nil{}:
       Nil{}
-    case Con{+s, rest}:
-      +mine = report_one(s, all, body, path, seen)
-      List.append(&2, F.Finding, mine, report(rest, all, body, path, s <> seen))
+    case Con{+r, rest}:
+      +mine = report_one(r, all, path, seen)
+      List.append(&2, F.Finding, mine, report(rest, all, path, r <> seen))
 
 # findings in one straight region; a case arm is not part of it
 def local(+nn: Tree.Node, +self: String, +lp: List<&2, String>, +path: String) -> List<&2, F.Finding>:
-  +sites = pin(mark(nn), apply(nn, gather(nn, self, lp, binds(nn, []))))
-  report(sites, sites, nn, path, [])
+  +rs = rate(pin(mark(nn), apply(nn, gather(nn, self, lp, binds(nn, [])))), nn)
+  report(rs, rs, path, [])
 
 # each case arm on its own, so two arms are not one path
 def visit(nn: Tree.Node, +self: String, +lp: List<&2, String>, +path: String) -> List<&2, F.Finding>: