src/rules/calls.bend source
src/rules/calls.bend on the hub · documented module
# 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).import Baseimport ../paths.bend as Pathsimport ../syntax/lex.bend as Leximport ../syntax/tree.bend as Treeimport ../syntax/bind.bend as Bindimport ../lazy/lazy.bend as Lazy# a def: its name, its own tokens (the signature) and the statements under ittype Def is Data: Def{name: String, sig: Tree.Node, body: Tree.Node}# a def with a name joins the others; one without (half-written) does notdef defs.push(mm: Maybe<&2, String>, sig: Tree.Node, body: Tree.Node, acc: List<&2, Def>) -> List<&2, Def>: match mm: case None{}: acc case Some{name}: Def{name, sig, body} <> acc# the defs of a parsed source, in orderdef defs(root: Tree.Node) -> List<&2, Def>: match root: case Tree.NCons{Tree.Stmt{Tree.SDef{}, +kids, body}, rest}: defs.push(Bind.declared(kids), kids, body, defs(rest)) case Tree.NCons{h, rest}: defs(rest) case other: Nil{}# a leaf's kind, none for anything else: kind tests read this, never a textdef leaf.kind(nn: Tree.Node) -> Maybe<&2, Lex.TokKind>: match nn: case Tree.Leaf{Lex.Tok{k, t, l, c}}: Some{k} case other: None{}# a kind test on a kind, when there is onedef kind.of(~test: Lex.TokKind -> Bool, mm: Maybe<&2, Lex.TokKind>) -> Bool: match mm: case None{}: False{} case Some{k}: test(k)# a leaf of this kind?def kind.leaf(~test: Lex.TokKind -> Bool, nn: Tree.Node) -> Bool: kind.of(~test, leaf.kind(nn))# a `:`def kind.colon(kk: Lex.TokKind) -> Bool: match kk: case Lex.TColon{}: True{} case other: False{}# a capitalized namedef kind.upper(kk: Lex.TokKind) -> Bool: match kk: case Lex.TUpper{}: True{} case other: False{}# `->`def kind.arrow(kk: Lex.TokKind) -> Bool: match kk: case Lex.TArrow{}: True{} case other: False{}# a plain operator (`-`, `~`, `+`)def kind.oper(kk: Lex.TokKind) -> Bool: match kk: case Lex.TOp{}: True{} case other: False{}# a leaf's text, "" for anything elsedef leaf.text(nn: Tree.Node) -> String: match nn: case Tree.Leaf{Lex.Tok{k, t, l, c}}: t case other: ""# the arguments of a group, split at its top-level commas (each a chain)def args.go(kids: Tree.Node, +cur: Tree.Node, +acc: List<&2, Tree.Node>) -> List<&2, Tree.Node>: match kids: case Tree.NCons{+h, +rest}: Lazy.either(List<&2, Tree.Node>, kind.leaf(~Lex.is_comma, h), _u => args.go(rest, Tree.NNil{}, Tree.reverse(cur, Tree.NNil{}) <> acc), _v => args.go(rest, Tree.NCons{h, cur}, acc)) case other: List.reverse(&2, Tree.Node, Tree.reverse(cur, Tree.NNil{}) <> acc)# the arguments of a groupdef args(kids: Tree.Node) -> List<&2, Tree.Node>: args.go(kids, Tree.NNil{}, [])# the nth argument, or nothingdef arg(as: List<&2, Tree.Node>, nn: Nat) -> Tree.Node: match as nn: case Con{h, t} 0n: h case Con{h, t} 1n+p: arg(t, p) case Nil{} m: Tree.NNil{}# is there a call of the name, `name(..)`, anywhere under the node?def calls(nn: Tree.Node, +name: String) -> Bool: match nn: case Tree.NCons{Tree.Leaf{Lex.Tok{k, +t, l, c}}, Tree.NCons{Tree.Group{Lex.Tok{_, +o, _, _}, kids, _}, rest}}: +a = calls(kids, name) +b = calls(rest, name) Bool.or(Bool.and(String.eq(o, "("), String.eq(t, name)), Bool.or(a, b)) case Tree.Group{open, kids, close}: calls(kids, name) case Tree.Stmt{kind, kids, body}: +a = calls(kids, name) +b = calls(body, name) Bool.or(a, b) case Tree.NCons{h, t}: +a = calls(h, name) +b = calls(t, name) Bool.or(a, b) case other: False{}# the kids of a signature's first `(` group: the parametersdef params.of(sig: Tree.Node) -> Tree.Node: match sig: case Tree.NCons{Tree.Group{Lex.Tok{k, +o, l, c}, +kids, close}, rest}: +more = params.of(rest) Bool.pick(Tree.Node, String.eq(o, "("), kids, more) case Tree.NCons{h, rest}: params.of(rest) case other: Tree.NNil{}# a def's parameters, each its chain up to a comma (`+xs: List<&2, U32>`)def params(sig: Tree.Node) -> List<&2, Tree.Node>: args(params.of(sig))# a parameter's name: its first lowercase name before the colon ("" for a# type parameter like `-A: Type`)def param_name(pp: Tree.Node) -> String: match pp: case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TName{}, t, l, c}}, rest}: t case Tree.NCons{Tree.Leaf{Lex.Tok{Lex.TColon{}, t, l, c}}, rest}: "" case Tree.NCons{h, rest}: param_name(rest) case other: ""def names.go(ps: List<&2, Tree.Node>, acc: List<&2, String>) -> List<&2, String>: match ps: case Nil{}: List.reverse(&2, String, acc) case Con{p, rest}: names.go(rest, param_name(p) <> acc)# the names of a def's parametersdef names(sig: Tree.Node) -> List<&2, String>: names.go(params(sig), [])# does a chain hold a top-level colon?def has_colon(pp: Tree.Node) -> Bool: match pp: case Tree.NCons{h, rest}: Lazy.or_else(kind.leaf(~kind.colon, h), _u => has_colon(rest)) case other: False{}# does the chain open with a `-` or `~` operator?def is_live.sign(pp: Tree.Node) -> Bool: match pp: case Tree.NCons{+h, rest}: +t = leaf.text(h) Bool.and(kind.leaf(~kind.oper, h), Bool.or(String.eq(t, "-"), String.eq(t, "~"))) case other: False{}# 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 onedef is_live(+pp: Tree.Node) -> Bool: Bool.and(Bool.not(is_live.sign(pp)), has_colon(pp))# the head of a parameter's type: the first capitalized name after the colon# (`List` in `+xs: +List<A>`), "" for nonedef type_head(pp: Tree.Node, +after: Bool) -> String: match pp: case Tree.NCons{+h, rest}: +more = type_head(rest, Bool.or(after, kind.leaf(~kind.colon, h))) Bool.pick(String, Bool.and(after, kind.leaf(~kind.upper, h)), leaf.text(h), more) case other: ""def walked.go(ps: List<&2, Tree.Node>, found: Maybe<&2, String>) -> String: match ps found: case Con{+p, rest} None{}: walked.go(rest, Lazy.stop(Maybe<&2, String>, Bool.not(is_live(p)), None{}, _u => Some{type_head(p, False{})})) case Con{p, rest} Some{t}: t case Nil{} Some{t}: t case Nil{} None{}: ""# the type head of the first live parameter: the one a self-call must shrinkdef walked(sig: Tree.Node) -> String: walked.go(params(sig), None{})# does the def walk a list or a string (its first live parameter's type)?def seq(sig: Tree.Node) -> Bool: +h = walked(sig) Bool.or(String.eq(h, "List"), String.eq(h, "String"))# a `{` group after the arrow, or a proof further ondef returns_proof.or(+brace: Bool, more: Bool) -> Bool: Bool.or(brace, more)# does the signature return a proof, `-> {a == b : T}`?def returns_proof(sig: Tree.Node) -> Bool: match sig: case Tree.NCons{h, +rest}: match rest: case Tree.NCons{+g, r2}: Lazy.either(Bool, kind.leaf(~kind.arrow, h), _u => returns_proof.or(Tree.opens(g, "{"), returns_proof(r2)), _v => returns_proof(rest)) case _r: returns_proof(rest) case other: False{}# does a chain hold a top-level `->`?def has_arrow(pp: Tree.Node) -> Bool: match pp: case Tree.NCons{h, rest}: Lazy.or_else(kind.leaf(~kind.arrow, h), _u => has_arrow(rest)) case other: False{}# does the signature write a type: a `:` among its parameters, or a `->`?def typed(+sig: Tree.Node) -> Bool: Lazy.or_else(has_colon(params.of(sig)), _u => has_arrow(sig))# 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 fdef proof(+sig: Tree.Node) -> Bool: Bool.or(returns_proof(sig), Bool.not(typed(sig)))# a law file, a proof file, or a def that is a proof: none of it runs, so its# cost does not matterdef exempt(+path: String, sig: Tree.Node) -> Bool: Bool.or(Paths.is_law_file(path), proof(sig))