src/rules/calls.bend checks

raw source on the hub · import 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/calls.bend as Calls

src/rules/calls: what the recursion rules (pick, strict, tail, concat, index) share. A file's defs, each with its name, its signature and its body; a call's arguments; whether a def calls itself; its parameters, and the type of the one it walks; and whether it is exempt (a law or a proof never runs, and a def with no type fills a law: it is a proof).

6 imports

import Base
import ../paths.bend as Paths
import ../syntax/lex.bend as Lex
import ../syntax/tree.bend as Tree
import ../syntax/bind.bend as Bind
import ../lazy/lazy.bend as Lazy

Types

type Def source · line 14 · raw

Data

a def: its name, its own tokens (the signature) and the statements under it

Def

@name:String -> @sig:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @body:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> Def

Definitions

def defs.push source · line 18 · raw

@mm:Maybe<&2, String> -> @sig:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @body:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @acc:List<&2, Def> -> List<&2, Def>

a def with a name joins the others; one without (half-written) does not

def defs source · line 26 · raw

@root:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> List<&2, Def>

the defs of a parsed source, in order

def leaf.kind source · line 36 · raw

@nn:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> Maybe<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/lex.TokKind>

a leaf's kind, none for anything else: kind tests read this, never a text

def kind.colon source · line 56 · raw

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

a :

def kind.upper source · line 64 · raw

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

a capitalized name

def kind.arrow source · line 72 · raw

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

->

def kind.oper source · line 80 · raw

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

a plain operator (-, ~, +)

def leaf.text source · line 88 · raw

@nn:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> String

a leaf's text, "" for anything else

def args.go source · line 96 · raw

@kids:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @+cur:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @+acc:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node> -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node>

the arguments of a group, split at its top-level commas (each a chain)

def args source · line 106 · raw

@kids:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node>

the arguments of a group

def arg source · line 110 · raw

@as:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node> -> @nn:Nat -> 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node

the nth argument, or nothing

def calls source · line 120 · raw

@nn:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @+name:String -> Bool

is there a call of the name, name(..), anywhere under the node?

def params.of source · line 140 · raw

@sig:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node

the kids of a signature's first ( group: the parameters

def params source · line 151 · raw

@sig:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node>

a def's parameters, each its chain up to a comma (+xs: List<&2, U32>)

def param_name source · line 156 · raw

@pp:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> String

a parameter's name: its first lowercase name before the colon ("" for a type parameter like -A: Type)

def names.go source · line 167 · raw

@ps:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node> -> @acc:List<&2, String> -> List<&2, String>

def names source · line 175 · raw

@sig:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> List<&2, String>

the names of a def's parameters

def has_colon source · line 179 · raw

@pp:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> Bool

does a chain hold a top-level colon?

def is_live.sign source · line 187 · raw

@pp:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> Bool

does the chain open with a - or ~ operator?

def is_live source · line 197 · raw

@+pp:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> Bool

a live parameter: typed, and neither erased (-A: Type) nor a template (~f: A -> B); a bare quantity name (a in List.get(a, ..)) is not one

def type_head source · line 202 · raw

@pp:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> @+after:Bool -> String

the head of a parameter's type: the first capitalized name after the colon (List in +xs: +List<A>), "" for none

def walked.go source · line 210 · raw

@ps:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node> -> @found:Maybe<&2, String> -> String

def walked source · line 223 · raw

@sig:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> String

the type head of the first live parameter: the one a self-call must shrink

def seq source · line 227 · raw

@sig:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> Bool

does the def walk a list or a string (its first live parameter's type)?

def returns_proof.or source · line 232 · raw

@+brace:Bool -> @more:Bool -> Bool

a { group after the arrow, or a proof further on

def returns_proof source · line 236 · raw

@sig:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> Bool

does the signature return a proof, -> {a == b : T}?

def has_arrow source · line 249 · raw

@pp:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> Bool

does a chain hold a top-level ->?

def typed source · line 257 · raw

@+sig:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> Bool

does the signature write a type: a : among its parameters, or a ->?

def proof source · line 263 · raw

@+sig:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> Bool

is the def a proof? One that returns a proof (-> {a == b : T}), or one written with no type at all (def f(x, y):), which is how Bend fills the law named f

def exempt source · line 268 · raw

@+path:String -> @sig:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> Bool

a law file, a proof file, or a def that is a proof: none of it runs, so its cost does not matter

Templates

template kind.of source · line 44 · raw

@-test:(@_:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/lex.TokKind -> Bool) -> @mm:Maybe<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/lex.TokKind> -> Bool

a kind test on a kind, when there is one

template kind.leaf source · line 52 · raw

@-test:(@_:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/lex.TokKind -> Bool) -> @nn:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/tree.Node -> Bool

a leaf of this kind?