@@ -116,14 +116,56 @@ data NameType =
117||| Types annotations for bound variables in different
117||| Types annotations for bound variables in different
118||| binding contexts
118||| binding contexts
120+||| @ tmTy the terms that can occur inside the binder, as type
121+||| annotations or bound values
119−data Binder a = Lam a
122+data Binder : (tmTy : Type) -> Type where
125+ ||| @ ty the type of the argument
126+ Lam : (ty : a) -> Binder a
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.
120− | Pi a a
134+ Pi : (ty, kind : a) -> Binder a
138+ ||| @ ty the type of the bound variable
139+ ||| @ val the bound value
121− | Let a a
140+ Let : (ty, val : a) -> Binder a
142+ ||| A hole that can occur during elaboration, and must be filled
144+ ||| @ ty the type of the value that will eventually be put into the hole
122− | Hole a
145+ Hole : (ty : a) -> Binder a
147+ ||| A hole that will later become a top-level metavariable
123− | GHole a
148+ GHole : (ty : a) -> Binder a
150+ ||| A hole with a solution in it. Computationally inert.
152+ ||| @ ty the type of the value in the hole
153+ ||| @ val the value in the hole
124− | Guess a a
154+ Guess : (ty, val : a) -> Binder a
156+ ||| A pattern variable. These bindings surround the terms that make
157+ ||| up the left and right sides of pattern-matching definition
160+ ||| @ ty the type of the pattern variable
125− | PVar a
161+ PVar : (ty : a) -> Binder a
163+ ||| The type of a pattern binding. This is to `PVar` as `Pi` is to
166+ ||| @ ty the type of the pattern variable
126− | PVTy a
167+ PVTy : (ty : a) -> Binder a
127%name Binder b, b'
169%name Binder b, b'
129instance Functor Binder where
171instance Functor Binder where
@@ -156,7 +198,7 @@ instance Traversable Binder where
156 traverse f (PVar x) = [| PVar (f x) |]
198 traverse f (PVar x) = [| PVar (f x) |]
157 traverse f (PVTy x) = [| PVTy (f x) |]
199 traverse f (PVTy x) = [| PVTy (f x) |]
159−||| Universes
201+||| The various universes involved in the uniqueness mechanism
160data Universe = NullType | UniqueType | AllTypes
202data Universe = NullType | UniqueType | AllTypes
162||| Reflection of the well typed core language
204||| Reflection of the well typed core language
@@ -195,8 +237,18 @@ data Raw =
195 RConstant Const
237 RConstant Const
196%name Raw tm, tm'
238%name Raw tm, tm'
198−data SourceLocation : Type where
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.
246+ ||| The file name of the source location
199− FileLoc : (filename : String) -> (start : (Int, Int)) -> (end : (Int, Int)) -> SourceLocation
247+ filename : String
248+ ||| The line and column of the beginning of the source span
250+ ||| The line and column of the end of the source span
201%name SourceLocation loc
253%name SourceLocation loc
@@ -214,7 +266,7 @@ data ErrorReportPart =
214 SubReport (List ErrorReportPart)
266 SubReport (List ErrorReportPart)
215%name ErrorReportPart part, p
267%name ErrorReportPart part, p
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
218||| tactic implementations. Generate these using `applyTactic`.
270||| tactic implementations. Generate these using `applyTactic`.
219data Tactic =
271data Tactic =
220 ||| Try the first tactic and resort to the second one on failure
272 ||| Try the first tactic and resort to the second one on failure
@@ -273,6 +325,7 @@ data Tactic =
273 Fail (List ErrorReportPart) |
325 Fail (List ErrorReportPart) |
274 ||| Attempt to fill the hole with source code information
326 ||| Attempt to fill the hole with source code information
276%name Tactic tac, tac'
329%name Tactic tac, tac'