@@ -142,23 +142,34 @@ Also, we currently reject `Constant` (has acceptable cost but not acceptable siz
142142We may want to check their sizes instead of just rejecting them.
143143-}
144144
145- -- | A list of `LamAbs` and `TyAbs`, in order, of a let-binding.
146- type TermOrTypeOrder = [TermOrType ]
145+ {-|
146+ The (syntactic) arity of a term. That is, a record of the arguments that the
147+ term expects before it may do some work. Since we have both type and lambda
148+ abstractions, this is not a simple argument count, but rather a list of values
149+ indicating whether the next argument should be a term or a type.
150+
151+ Note that this is the syntactic arity, i.e. it just corresponds to the number of
152+ syntactic lambda and type abstractions on the outside of the term. It is thus
153+ an under-approximation of how many arguments the term may need.
154+ e.g. consider the term @let id = \x -> x in id@: the variable @id@ has syntactic
155+ arity @[]@, but does in fact need an argument before it does any work.
156+ -}
157+ type Arity = [TermOrType ]
147158
148- -- | Datatype capturing both terms and types.
159+ -- | Is the next argument a term or a type?
149160data TermOrType =
150161 MkTerm | MkType
151162 deriving stock (Eq , Show )
152163
153164instance Pretty TermOrType where
154165 pretty = viaShow
155166
156- -- | Counts the type and term lambdas in the RHS of a binding and returns an ordered list
157- countLam ::
158- Term tyname name uni fun a -- ^ the RHS of the let binding
159- -> TermOrTypeOrder
160- countLam = \ case
161- LamAbs _ _ _ body -> MkTerm : countLam body
162- TyAbs _ _ _ body -> MkType : countLam body
163- -- Whenever we encounter a body that is not a lambda abstraction, we are done counting
167+ -- | Computes the 'Arity' of a term.
168+ computeArity ::
169+ Term tyname name uni fun a
170+ -> Arity
171+ computeArity = \ case
172+ LamAbs _ _ _ body -> MkTerm : computeArity body
173+ TyAbs _ _ _ body -> MkType : computeArity body
174+ -- Whenever we encounter a body that is not a lambda or type abstraction, we are done counting
164175 _ -> []
0 commit comments