type Syntax

bend-lint-api@0.2.0.0 · linter/lint.bend:33

import Base

33# What a syntax node is, as Bend's parser reads it: a declaration, a part of one, a term, or a pattern; with what only
34# nodes of its kind have: the global name it declares or uses (`target`, as the check names it; an import's is the path
35# of the file it loads), the binder it declares or a variable uses (numbered per top-level declaration), and its
36# quantity as written (a `~` parameter's is Template). An import's written path is an ImportPath under it; `import
37# Base` writes none. A Definition is `unsafe` if Bend's checker trusts its body (`@unsafe def f`, or `def f?`).
38type Syntax is Data:
39  Import{target: String}
40  ImportPath{}
41  Definition{target: String, unsafe: Bool}
42  Datatype{target: String}
43  Constructor{target: String}
44  Law{target: String}
45  Parameter{binder: U32, quantity: Quantity}
46  Field{binder: U32, quantity: Quantity}
47  Returns{}
48  Body{}
49  Variable{binder: U32}
50  Reference{target: String}
51  Substitution{}
52  Let{}
53  Binding{binder: U32, quantity: Quantity}
54  Sort{}
55  QuantityType{}
56  QuantityLiteral{quantity: Quantity}
57  QuantityMinimum{}
58  Forall{binder: U32, quantity: Quantity}
59  Lambda{binder: U32, quantity: Maybe<&2, Quantity>}
60  Application{}
61  TypeApplication{target: String}
62  Construction{target: String}
63  Literal{target: String}
64  Elimination{target: String}
65  Absurd{}
66  Equality{}
67  Reflexivity{}
68  Rewrite{}
69  Hole{}
70  Annotation{}
71  Match{}
72  Case{}
73  Destructure{quantity: Quantity}
74  PatternVariable{binder: U32, quantity: Quantity}
75  PatternConstructor{target: String}