src/rules/correctness/hole.bend checks

raw source on the hub · import 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/correctness/hole.bend as Hole

rule hole: a TODO hole left in code, the one bend counts when it prints SOME PROOFS FAIL then "Error: 1 TODO found." or "Error: N TODOs found." and exits 1 (bend 2.0.34): a ? and then the name TODO, with any spaces, newlines or comments between them (?TODO, ? TODO). ?todo, ?TODO_later and ?TODO.x are other names, which bend reports as a type error, not as a TODO, and they are not reported here. The finding spans ? through TODO when both sit on one line, and the ? alone when TODO is on a later line. LAWS.bend is exempt: by convention its laws are open claims, filled by PROOF.bend beside it.

7 imports

import Base
import ../../paths.bend as Paths
import ../../src.bend as Src
import ../../finding.bend as F
import ../../syntax/lex.bend as Lex
import ../../lazy/lazy.bend as Lazy
import ../calls.bend as Calls

Definitions

def check.todo source · line 18 · raw

@toks:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/lex.Tok> -> Bool

True when the first token past spaces, newlines and comments is TODO

def check.width source · line 27 · raw

@toks:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/lex.Tok> -> @+line:U32 -> @+col:U32 -> U32

the width of the hole a ? at line, col starts: through the next token past spaces, newlines and comments when it sits on the same line, else 1

def check.go source · line 35 · raw

@toks:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/lex.Tok> -> @+path:String -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

def check.on source · line 45 · raw

@toks:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/lex.Tok> -> @+path:String -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

def check source · line 49 · raw

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

the rule