@@ -116,14 +116,56 @@ data NameType =
116116
117117||| Types annotations for bound variables in different
118118||| binding contexts
119−data Binder a = Lam a
120− | Pi a a
121− | Let a a
122− | Hole a
123− | GHole a
124− | Guess a a
125− | PVar a
126− | PVTy a
119+|||
120+||| @ tmTy the terms that can occur inside the binder, as type
121+||| annotations or bound values
122+data Binder : (tmTy : Type) -> Type where
123+ ||| Lambdas
124+ |||
125+ ||| @ ty the type of the argument
126+ Lam : (ty : a) -> Binder a
127+
128+ ||| Function types.
129+ |||
130+ ||| @ kind The kind of arrow. Only relevant when dealing with
131+ ||| uniqueness, so you can usually pretend that this
132+ ||| field doesn't exist. For ordinary functions, use the
133+ ||| type of types here.
134+ Pi : (ty, kind : a) -> Binder a
135+
136+ ||| A let binder
137+ |||
138+ ||| @ ty the type of the bound variable
139+ ||| @ val the bound value
140+ Let : (ty, val : a) -> Binder a
141+
142+ ||| A hole that can occur during elaboration, and must be filled
143+ |||
144+ ||| @ ty the type of the value that will eventually be put into the hole
145+ Hole : (ty : a) -> Binder a
146+
147+ ||| A hole that will later become a top-level metavariable
148+ GHole : (ty : a) -> Binder a
149+
150+ ||| A hole with a solution in it. Computationally inert.
151+ |||
152+ ||| @ ty the type of the value in the hole
153+ ||| @ val the value in the hole
154+ Guess : (ty, val : a) -> Binder a
155+
156+ ||| A pattern variable. These bindings surround the terms that make
157+ ||| up the left and right sides of pattern-matching definition
158+ ||| clauses.
159+ |||
160+ ||| @ ty the type of the pattern variable
161+ PVar : (ty : a) -> Binder a
162+
163+ ||| The type of a pattern binding. This is to `PVar` as `Pi` is to
164+ ||| `Lam`.
165+ |||
166+ ||| @ ty the type of the pattern variable
167+ PVTy : (ty : a) -> Binder a
168+
127169%name Binder b, b'
128170
129171instance Functor Binder where
@@ -156,7 +198,7 @@ instance Traversable Binder where
156198 traverse f (PVar x) = [| PVar (f x) |]
157199 traverse f (PVTy x) = [| PVTy (f x) |]
158200
159−||| Universes
201+||| The various universes involved in the uniqueness mechanism
160202data Universe = NullType | UniqueType | AllTypes
161203
162204||| Reflection of the well typed core language
@@ -195,8 +237,18 @@ data Raw =
195237 RConstant Const
196238%name Raw tm, tm'
197239
198−data SourceLocation : Type where
199− FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation
240+||| A source location in an Idris file
241+record SourceLocation where
242+ ||| Either a source span or a source location. `start` and `end`
243+ ||| will be the same if it's a point location.
244+ constructor FileLoc
245+
246+ ||| The file name of the source location
247+ filename : String
248+ ||| The line and column of the beginning of the source span
249+ start : (Int, Int)
250+ ||| The line and column of the end of the source span
251+ end : (Int, Int)
200252
201253%name SourceLocation loc
202254
@@ -214,7 +266,7 @@ data ErrorReportPart =
214266 SubReport (List ErrorReportPart)
215267%name ErrorReportPart part, p
216268
217−||| A representation of Idris's tactics that can be returned from custom
269+||| A representation of Idris's old tactics that can be returned from custom
218270||| tactic implementations. Generate these using `applyTactic`.
219271data Tactic =
220272 ||| Try the first tactic and resort to the second one on failure
@@ -273,6 +325,7 @@ data Tactic =
273325 Fail (List ErrorReportPart) |
274326 ||| Attempt to fill the hole with source code information
275327 SourceFC
328+
276329%name Tactic tac, tac'
277330
278331