src/rules/correctness/arms.bend checks

raw source on the hub · import 0x013e0f9a479bbebad5ed196725eede95/src/rules/correctness/arms.bend as Arms

rule arms: a Nat arm no value can reach. case kn+p: matches every Nat from k up, so a later case jn+q: with j >= k, or a later case mn: with m >= k, never runs. The checker accepts it and the match quietly returns the earlier arm (nohzafk pat_bad: 0n, 1n+p, 2n+p gives f(2n) = 1; bend 2.0.16 still does). Put the narrower arms first: the literals, then the larger n+p. Succ{p} and Succ{_} count as 1n+p. Only a single-scrutinee match is read: a column of a multi-scrutinee match is skipped.

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 ../../lazy/lazy.bend as Lazy
import ../tokens.bend as T

Types

type Arm source · line 18 · raw

Data

what an arm matches: from k up (text is its pattern), exactly k, or other

APlus

@k:U32 -> @text:String -> @line:U32 -> @col:U32 -> @len:U32 -> Arm

ALit

@k:U32 -> @line:U32 -> @col:U32 -> @len:U32 -> Arm

AOther
```
Arm
```

type Wide source · line 24 · raw

Data

the widest n+p arm so far: its k and its pattern

Wide
```
@k:U32 -> @text:String -> Wide
```

Definitions

def binder source · line 28 · raw

@kk:0x013e0f9a479bbebad5ed196725eede95/src/syntax/lex.TokKind -> Bool

a lone binder, inside Succ{..} or after kn+: a name or _

def lit.shape source · line 38 · raw

@rest:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> @+kk:U32 -> @+tt:String -> @+line:U32 -> @+col:U32 -> Arm

kn+p: (p a name or _) or kn:

def lit.of source · line 50 · raw

@mm:Maybe<&2, U32> -> @+tt:String -> @+rest:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> @+line:U32 -> @+col:U32 -> Arm

a Nat literal token's arm, once its value is read

def arm source · line 58 · raw

@pat:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> Arm

a case pattern's arm

def widen source · line 70 · raw

@ww:Maybe<&2, Wide> -> @aa:Arm -> Maybe<&2, Wide>

the widest n+p arm after this one

def verdict.on source · line 80 · raw

@+kk:U32 -> @+text:String -> @aa:Arm -> @+path:String -> @+more:List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/finding.Finding> -> List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/finding.Finding>

a finding when the arm is inside the widest one above

def verdict source · line 98 · raw

@ww:Maybe<&2, Wide> -> @aa:Arm -> @+path:String -> @more:List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/finding.Finding> -> List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/finding.Finding>

the arm against the widest one above, if any

def arms source · line 106 · raw

@body:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> @+wide:Maybe<&2, Wide> -> @+path:String -> List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/finding.Finding>

a match's arms in order, against the widest n+p arm above each

def single source · line 117 · raw

@kids:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> Bool

match x:: one scrutinee

def walk source · line 126 · raw

@nn:0x013e0f9a479bbebad5ed196725eede95/src/syntax/tree.Node -> @+path:String -> List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/finding.Finding>

every statement, at any depth; a single-scrutinee match's arms are read

def check source · line 137 · raw

@ss:0x013e0f9a479bbebad5ed196725eede95/src/src.Src -> List<&2, 0x013e0f9a479bbebad5ed196725eede95/src/finding.Finding>

the rule