From 2c30f47ac532fab616cc6071ca132d19b70d65c6 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 16:58:36 +0000 Subject: [PATCH 1/2] perf: index once in rewalk, bind.refresh and digest.laws_of (#228) - rewalk: rate each site once (narrow over the piece) before reporting, so other_go, earlier and report compare ratings instead of walking the piece for every pair of twin sites. The proofs of rewalk_local_counts now go through Rewalk.rate; no law changed. - bind.refresh: read the annotated binders with a cursor (binders are in source order) instead of one full binder search per environment entry; a binder before the last one read starts the cursor over. - digest.laws_of: carry the outline items forward as a cursor instead of searching them from the start for each law. unused (reportable over the foreign header lines) is left as is: a faster lookup cannot be proved equal to the List.contains that unused_counts states. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B --- src/rules/PROOF.bend | 115 ++++++++++++------------------- src/rules/digest.bend | 20 +++++- src/rules/suspicious/rewalk.bend | 98 +++++++++++--------------- src/syntax/bind.bend | 48 +++++++++++-- 4 files changed, 146 insertions(+), 135 deletions(-) diff --git a/src/rules/PROOF.bend b/src/rules/PROOF.bend index 57c0c23..8ac9d7f 100644 --- a/src/rules/PROOF.bend +++ b/src/rules/PROOF.bend @@ -13785,36 +13785,7 @@ 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 @@ -13822,24 +13793,25 @@ law rewalk.whole_eq: 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 @@ -13847,20 +13819,22 @@ law rewalk.prior_eq: 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 diff --git a/src/rules/digest.bend b/src/rules/digest.bend index e003d5a..1116294 100644 --- a/src/rules/digest.bend +++ b/src/rules/digest.bend @@ -307,13 +307,27 @@ 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 +# 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 +def from_line(+items: List<&2, Outline.Item>, +at: U32) -> List<&2, Outline.Item>: + match items: + case Nil{}: + Nil{} + case Con{Outline.Item{kk, nn, +ln, sig, doc, pp}, rest}: + Lazy.stop(List<&2, Outline.Item>, U32.is_le(at, ln), Outline.Item{kk, nn, ln, sig, doc, pp} <> rest, + _u => from_line(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) + 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: diff --git a/src/rules/suspicious/rewalk.bend b/src/rules/suspicious/rewalk.bend index 787067d..30b1824 100644 --- a/src/rules/suspicious/rewalk.bend +++ b/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>: diff --git a/src/syntax/bind.bend b/src/syntax/bind.bend index 1b95cde..f46ce2a 100644 --- a/src/syntax/bind.bend +++ b/src/syntax/bind.bend @@ -953,13 +953,53 @@ def noted(mm: Maybe<&2, Bind>, bb: Bind) -> Bind: case Some{full}: full -# each binder of an environment, with the note its annotated twin carries -def refresh(env: List<&2, Bind>, +binds: List<&2, Bind>) -> List<&2, Bind>: - match env: +# does (l1, c1) come before (l2, c2) in the source? +def before(+l1: U32, +c1: U32, +l2: U32, +c2: U32) -> Bool: + Bool.or(U32.is_lt(l1, l2), Bool.and(U32.is_eq(l1, l2), U32.is_lt(c1, c2))) + +# the binders from the first one not before a position on; the binders are in +# source order, so none this drops sits at the position +def seek(+binds: List<&2, Bind>, +line: U32, +col: U32) -> List<&2, Bind>: + match binds: case Nil{}: Nil{} case Con{Bind{name, +l, +c, kind, note}, rest}: - noted(binder(binds, l, c), Bind{name, l, c, kind, note}) <> refresh(rest, binds) + Lazy.stop(List<&2, Bind>, Bool.not(before(l, c, line, col)), Bind{name, l, c, kind, note} <> rest, + _u => seek(rest, line, col)) + +# the binder at the head of a cursor, when it sits at the position +def seek.head(cur: List<&2, Bind>, +line: U32, +col: U32) -> Maybe<&2, Bind>: + match cur: + case Nil{}: + None{} + case Con{Bind{name, +l, +c, kind, note}, rest}: + Bool.pick(Maybe<&2, Bind>, Bool.and(U32.is_eq(l, line), U32.is_eq(c, col)), Some{Bind{name, l, c, kind, note}}, + None{}) + +# each binder of an environment, outermost first, with the note its annotated +# twin carries, pushed onto acc (so acc ends innermost first again). cur is a +# cursor into binds that drops only binders before (tl, tc), the last one +# read: an environment's binders were pushed in source order, so each lookup +# picks up where the last stopped and binds is read once, not once per +# binder. A binder before the last one read starts the cursor over +def refresh.go( + env: List<&2, Bind>, + +binds: List<&2, Bind>, + +cur: List<&2, Bind>, + +tl: U32, + +tc: U32, + acc: List<&2, Bind> +) -> List<&2, Bind>: + match env: + case Nil{}: + acc + case Con{Bind{name, +l, +c, kind, note}, rest}: + +from = seek(Bool.pick(List<&2, Bind>, before(l, c, tl, tc), binds, cur), l, c) + refresh.go(rest, binds, from, l, c, noted(seek.head(from, l, c), Bind{name, l, c, kind, note}) <> acc) + +# each binder of an environment, with the note its annotated twin carries +def refresh(env: List<&2, Bind>, +binds: List<&2, Bind>) -> List<&2, Bind>: + refresh.go(List.reverse(&2, Bind, env), binds, binds, 0, 0, []) # the names in scope at a line: those of the statement on it, else of the # nearest statement above From c0f88dd6a3b6463079f9786eb15bf5a299b89c33 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 17:03:09 +0000 Subject: [PATCH 2/2] perf: carry the stop test in seek and from_line instead of a thunk The two new cursors wrapped their recursive step in Lazy.stop, the lone thunk AGENTS.md warns against for a search (thunk, U015). Carry the head's test as a Bool into the next call and match on it after the list, so the step stays a tail call. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01X7i62UAece6mwMRV3Y1b9B --- src/rules/digest.bend | 23 +++++++++++++++++------ src/syntax/bind.bend | 25 +++++++++++++++++++------ 2 files changed, 36 insertions(+), 12 deletions(-) diff --git a/src/rules/digest.bend b/src/rules/digest.bend index 1116294..aded53b 100644 --- a/src/rules/digest.bend +++ b/src/rules/digest.bend @@ -307,16 +307,27 @@ 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)) +# 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 -def from_line(+items: List<&2, Outline.Item>, +at: U32) -> List<&2, Outline.Item>: +# 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{Outline.Item{kk, nn, +ln, sig, doc, pp}, rest}: - Lazy.stop(List<&2, Outline.Item>, U32.is_le(at, ln), Outline.Item{kk, nn, ln, sig, doc, pp} <> rest, - _u => from_line(rest, at)) + 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 @@ -325,7 +336,7 @@ 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) - +left = from_line(items, at) + +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}: diff --git a/src/syntax/bind.bend b/src/syntax/bind.bend index f46ce2a..b9773da 100644 --- a/src/syntax/bind.bend +++ b/src/syntax/bind.bend @@ -957,15 +957,27 @@ def noted(mm: Maybe<&2, Bind>, bb: Bind) -> Bind: def before(+l1: U32, +c1: U32, +l2: U32, +c2: U32) -> Bool: Bool.or(U32.is_lt(l1, l2), Bool.and(U32.is_eq(l1, l2), U32.is_lt(c1, c2))) +# does a cursor's head sit at or after a position (the seek stops there)? +def seek.stop(cur: List<&2, Bind>, +line: U32, +col: U32) -> Bool: + match cur: + case Nil{}: + True{} + case Con{Bind{name, +l, +c, kind, note}, rest}: + Bool.not(before(l, c, line, col)) + # the binders from the first one not before a position on; the binders are in -# source order, so none this drops sits at the position -def seek(+binds: List<&2, Bind>, +line: U32, +col: U32) -> List<&2, Bind>: +# source order, so none this drops sits at the position. stop is seek.stop of +# binds, carried so the step stays a loop +def seek(binds: List<&2, Bind>, +line: U32, +col: U32, +stop: Bool) -> List<&2, Bind>: match binds: case Nil{}: Nil{} - case Con{Bind{name, +l, +c, kind, note}, rest}: - Lazy.stop(List<&2, Bind>, Bool.not(before(l, c, line, col)), Bind{name, l, c, kind, note} <> rest, - _u => seek(rest, line, col)) + case Con{h, +rest}: + match stop: + case True{}: + h <> rest + case False{}: + seek(rest, line, col, seek.stop(rest, line, col)) # the binder at the head of a cursor, when it sits at the position def seek.head(cur: List<&2, Bind>, +line: U32, +col: U32) -> Maybe<&2, Bind>: @@ -994,7 +1006,8 @@ def refresh.go( case Nil{}: acc case Con{Bind{name, +l, +c, kind, note}, rest}: - +from = seek(Bool.pick(List<&2, Bind>, before(l, c, tl, tc), binds, cur), l, c) + +start = Bool.pick(List<&2, Bind>, before(l, c, tl, tc), binds, cur) + +from = seek(start, l, c, seek.stop(start, l, c)) refresh.go(rest, binds, from, l, c, noted(seek.head(from, l, c), Bind{name, l, c, kind, note}) <> acc) # each binder of an environment, with the note its annotated twin carries