~/bend-docscommunity

bolt/rules/calls.bend checks

raw source on the hub · import 0x729eecea86ea5a2cdba3a2856a313bca/bolt/rules/calls.bend as Calls

bolt/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).

5 imports
import Base
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 12 · raw

Data

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

Definitions

def defs.push source · line 16 · raw

@m:Maybe<&2, String> -> @sig:0x729eecea86ea5a2cdba3a2856a313bca/syntax/tree.Node -> @body:0x729eecea86ea5a2cdba3a2856a313bca/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 24 · raw

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

the defs of a parsed source, in order

def args.go source · line 34 · raw

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

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

def args source · line 44 · raw

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

the arguments of a group

def arg source · line 48 · raw

@as:List<&2, 0x729eecea86ea5a2cdba3a2856a313bca/syntax/tree.Node> -> @n:Nat -> 0x729eecea86ea5a2cdba3a2856a313bca/syntax/tree.Node

the nth argument, or nothing

def mentions source · line 58 · raw

@n:0x729eecea86ea5a2cdba3a2856a313bca/syntax/tree.Node -> @+name:String -> Bool

does the name appear anywhere under the node?

def calls source · line 76 · raw

@n:0x729eecea86ea5a2cdba3a2856a313bca/syntax/tree.Node -> @+name:String -> Bool

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

def params.of source · line 96 · raw

@sig:0x729eecea86ea5a2cdba3a2856a313bca/syntax/tree.Node -> 0x729eecea86ea5a2cdba3a2856a313bca/syntax/tree.Node

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

def params source · line 107 · raw

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

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

def param_name source · line 112 · raw

@p:0x729eecea86ea5a2cdba3a2856a313bca/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 123 · raw

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

def names source · line 131 · raw

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

the names of a def's parameters

def has_colon source · line 135 · raw

@p:0x729eecea86ea5a2cdba3a2856a313bca/syntax/tree.Node -> Bool

does a chain hold a top-level colon?

def is_live source · line 146 · raw

@p:0x729eecea86ea5a2cdba3a2856a313bca/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 155 · raw

@p:0x729eecea86ea5a2cdba3a2856a313bca/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 167 · raw

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

def walked source · line 180 · raw

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

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

def seq source · line 184 · raw

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

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

def returns_proof source · line 189 · raw

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

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

def exempt source · line 201 · raw

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

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