src/rules/correctness/pick.bend checks
raw source on the hub · import 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/correctness/pick.bend as Pick
rule pick: a def calls itself in a branch of a Bool.pick. Bool.pick is a
function, so both branches are evaluated whatever the condition. In both
branches, two recursive calls a step is 2^n work where one was meant (a
per-token scan that took 20 s this way took 20 ms as one pass): bind the
call once above the pick (+more = go(rest)) and pick between x <> more
and more. In one branch, the recursion runs even when the other branch
was the answer: a search never stops early and walks the whole input
(portal-bend's get, bendoom's sorted insert). Match on the Bool instead,
in a helper that takes it as a parameter. A self-call is the def's name
followed by (..): a parameter or a value named like the def is not one. A
pick nested in a branch of one already reported is not reported again; one
nested in its condition is. A
law file, a proof file and a def that is a proof never run, so they are
exempt: a def that returns a proof, or one written with no type at all
(def f(x, y):), which fills the law named f.
7 imports
import Base import ../../src.bend as Src import ../../finding.bend as F import ../../syntax/lex.bend as Lex import ../../syntax/tree.bend as Tree import ../calls.bend as Calls import ../../lazy/lazy.bend as Lazy
Definitions
def both source · line 25 · raw
@+as:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node> -> @+name:String -> Bool
do both branches (the third and fourth arguments) call the def?
def once source · line 29 · raw
@+as:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node> -> @+name:String -> Bool
does either branch call the def?
def mute source · line 34 · raw
@+quiet:Bool -> @+hush:Bool -> @nth:Nat -> Bool
is argument nth of a group quiet: the group's own quiet, or, in a branch (the third or fourth argument) of a reported pick, hushed
def next source · line 48 · raw
@kk:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/lex.TokKind -> @nth:Nat -> Nat
the argument a token leaves the walk in: one further past a top-level comma
def walk source · line 59 · raw
@nn:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @+name:String -> @+path:String -> @+quiet:Bool -> @+hush:Bool -> @+nth:Nat -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>
every Bool.pick(..) in a chain, at any depth, that recurses in both
branches or in one. The chain is argument nth of a group with quiet
(inside a branch of a reported pick) and hush (the group is a reported
pick, so its branches are quiet); a pick in the condition still counts.
def picks source · line 93 · raw
@nn:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @+name:String -> @+path:String -> @+quiet:Bool -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>
every reported pick in a chain walked at quiet, outside any pick's arguments
def check.go source · line 96 · raw
@ds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/calls.Def> -> @+path:String -> @acc:List<&2, List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>
def check source · line 106 · raw
@ss:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/src.Src -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>
the rule