Skip to content

Commit 9e44bd9

Browse files
wizard7377wizard7377
committed
docs: added library documentation for Elab 
1 parent 6e52f89 commit 9e44bd9

File tree

3 files changed

+152
-84
lines changed

3 files changed

+152
-84
lines changed

‎libs/base/Language/Reflection.idr‎

Lines changed: 21 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -62,49 +62,49 @@ data Elab : Type -> Type where
6262

6363
ResugarTerm : (maxLineWidth : Maybe Nat) -> TTImp -> Elab String
6464

65-
-- Elaborate a TTImp term to a concrete value
65+
||| Elaborate a TTImp term to a concrete value
6666
Check : TTImp -> Elab expected
67-
-- Quote a concrete expression back to a TTImp
67+
||| Quote a concrete expression back to a TTImp
6868
Quote : (0 _ : val) -> Elab TTImp
6969

70-
-- Elaborate under a lambda
70+
||| Elaborate under a lambda
7171
Lambda : (0 x : Type) ->
7272
{0 ty : x -> Type} ->
7373
((val : x) -> Elab (ty val)) -> Elab ((val : x) -> (ty val))
7474

75-
-- Get the current goal type, if known
76-
-- (it might need to be inferred from the solution)
75+
||| Get the current goal type, if known
76+
||| (it might need to be inferred from the solution)
7777
Goal : Elab (Maybe TTImp)
78-
-- Get the names of local variables in scope
78+
||| Get the names of local variables in scope
7979
LocalVars : Elab (List Name)
80-
-- Generate a new unique name, based on the given string
80+
||| Generate a new unique name, based on the given string
8181
GenSym : String -> Elab Name
82-
-- Put a name in the current namespace
82+
||| Put a name in the current namespace
8383
InCurrentNS : Name -> Elab Name
84-
-- Get the types of every name which matches.
85-
-- There may be ambiguities - returns a list of fully explicit names
86-
-- and their types. If there's no results, the name is undefined.
84+
||| Get the types of every name which matches.
85+
||| There may be ambiguities - returns a list of fully explicit names
86+
||| and their types. If there's no results, the name is undefined.
8787
GetType : Name -> Elab (List (Name, TTImp))
88-
-- Get the metadata associated with a name
88+
||| Get the metadata associated with a name
8989
GetInfo : Name -> Elab (List (Name, NameInfo))
90-
-- Get the visibility associated with a name
90+
||| Get the visibility associated with a name
9191
GetVis : Name -> Elab (List (Name, Visibility))
92-
-- Get the type of a local variable
92+
||| Get the type of a local variable
9393
GetLocalType : Name -> Elab TTImp
94-
-- Get the constructors of a data type. The name must be fully resolved.
94+
||| Get the constructors of a data type. The name must be fully resolved.
9595
GetCons : Name -> Elab (List Name)
96-
-- Get all function definition names referred in a definition. The name must be fully resolved.
96+
||| Get all function definition names referred in a definition. The name must be fully resolved.
9797
GetReferredFns : Name -> Elab (List Name)
98-
-- Get the name of the current and outer functions, if it is applicable
98+
||| Get the name of the current and outer functions, if it is applicable
9999
GetCurrentFn : Elab (SnocList Name)
100-
-- Check a group of top level declarations
100+
||| Check a group of top level declarations
101101
Declare : List Decl -> Elab ()
102102

103-
-- Read the contents of a file, if it is present
103+
||| Read the contents of a file, if it is present
104104
ReadFile : LookupDir -> (path : String) -> Elab $ Maybe String
105-
-- Writes to a file, replacing existing contents, if were present
105+
||| Writes to a file, replacing existing contents, if were present
106106
WriteFile : LookupDir -> (path : String) -> (contents : String) -> Elab ()
107-
-- Returns the specified type of dir related to the current idris project
107+
||| Returns the specified type of dir related to the current idris project
108108
IdrisDir : LookupDir -> Elab String
109109

110110
export

‎libs/base/Language/Reflection/TT.idr‎

Lines changed: 33 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -6,14 +6,14 @@ import public Data.String
66
import Decidable.Equality
77

88
%default total
9-
9+
||| namespace, stored in reverse order
1010
public export
11-
data Namespace = MkNS (List String) -- namespace, stored in reverse order
11+
data Namespace = MkNS (List String)
1212

1313
%name Namespace ns
14-
14+
||| module identifier, stored in reverse order
1515
public export
16-
data ModuleIdent = MkMI (List String) -- module identifier, stored in reverse order
16+
data ModuleIdent = MkMI (List String)
1717

1818
%name ModuleIdent mi
1919

@@ -27,9 +27,9 @@ export
2727
Show Namespace where
2828
show (MkNS ns) = showSep "." (reverse ns)
2929

30-
-- 'FilePos' represents the position of
31-
-- the source information in the file (or REPL).
32-
-- in the form of '(line-no, column-no)'.
30+
||| 'FilePos' represents the position of
31+
||| the source information in the file (or REPL).
32+
||| in the form of '(line-no, column-no)'.
3333
public export
3434
FilePos : Type
3535
FilePos = (Int, Int)
@@ -187,6 +187,7 @@ Show Constant where
187187
show (PrT x) = show x
188188
show WorldVal = "%World"
189189

190+
||| Any name that a user can assign to
190191
public export
191192
data UserName
192193
= Basic String -- default name constructor e.g. map
@@ -195,14 +196,23 @@ data UserName
195196

196197
%name UserName un
197198

198-
public export
199-
data Name = NS Namespace Name -- name in a namespace
200-
| UN UserName -- user defined name
201-
| MN String Int -- machine generated name
202-
| DN String Name -- a name and how to display it
203-
| Nested (Int, Int) Name -- nested function name
204-
| CaseBlock String Int -- case block nested in (resolved) name
205-
| WithBlock String Int -- with block nested in (resolved) name
199+
||| A name in a Idris program
200+
public export
201+
data Name =
202+
||| A qualified name
203+
NS Namespace Name
204+
||| A user defined name
205+
| UN UserName
206+
||| A machine generated name
207+
| MN String Int
208+
||| A name with a display string
209+
| DN String Name
210+
||| Nested function name
211+
| Nested (Int, Int) Name
212+
||| Case block nested in (resolved) name
213+
| CaseBlock String Int
214+
||| With block nested in (resolved) name
215+
| WithBlock String Int
206216

207217
%name Name nm
208218

@@ -251,8 +261,15 @@ record NameInfo where
251261
constructor MkNameInfo
252262
nametype : NameType
253263

264+
||| A multiplicity
254265
public export
255-
data Count = M0 | M1 | MW
266+
data Count =
267+
||| 0 (erased)
268+
M0 |
269+
||| 1 (linear)
270+
M1 |
271+
||| ω (unrestricted)
272+
MW
256273
%name Count rig
257274

258275
export

‎libs/base/Language/Reflection/TTImp.idr‎

Lines changed: 98 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -29,66 +29,96 @@ mutual
2929
| UnderAppliedCon
3030
%name DotReason dr
3131

32+
||| The elaborator representation of an Idris term
33+
||| All of these take a file context `FC` as their first argument
3234
public export
3335
data TTImp : Type where
36+
||| A variable reference, by name
3437
IVar : FC -> Name -> TTImp
35-
IPi : FC -> Count -> PiInfo TTImp -> Maybe Name ->
38+
||| A function type, of the form `(mult binder : argTy) -> retTy`, with implicitness determined by `info`
39+
IPi : FC -> (mult : Count) -> (info : PiInfo TTImp) -> (binder : Maybe Name) ->
3640
(argTy : TTImp) -> (retTy : TTImp) -> TTImp
37-
ILam : FC -> Count -> PiInfo TTImp -> Maybe Name ->
41+
||| A lambda abstraction, of the form`\(mult binder : argTy) => retTy`, with implicitness determined by `info`
42+
ILam : FC -> (mult : Count) -> (info : PiInfo TTImp) -> (binder : Maybe Name) ->
3843
(argTy : TTImp) -> (lamTy : TTImp) -> TTImp
39-
ILet : FC -> (lhsFC : FC) -> Count -> Name ->
44+
||| A let binding, of the form `let mult var : nTy = nVal in scope`
45+
ILet : FC -> (lhsFC : FC) -> (mult : Count) -> (var : Name) ->
4046
(nTy : TTImp) -> (nVal : TTImp) ->
4147
(scope : TTImp) -> TTImp
42-
ICase : FC -> List FnOpt -> TTImp -> (ty : TTImp) ->
43-
List Clause -> TTImp
44-
ILocal : FC -> List Decl -> TTImp -> TTImp
45-
IUpdate : FC -> List IFieldUpdate -> TTImp -> TTImp
46-
47-
IApp : FC -> TTImp -> TTImp -> TTImp
48-
INamedApp : FC -> TTImp -> Name -> TTImp -> TTImp
49-
IAutoApp : FC -> TTImp -> TTImp -> TTImp
48+
||| A case expression `case val : ty of clauses`
49+
ICase : FC -> (opts : List FnOpt) -> (val : TTImp) -> (ty : TTImp) ->
50+
(clauses : List Clause) -> TTImp
51+
||| A list of full declarations local to a term
52+
ILocal : FC -> (context : List Decl) -> (term : TTImp) -> TTImp
53+
||| An update to a record value, `{ updates } val`
54+
IUpdate : FC -> (updates : List IFieldUpdate) -> (val : TTImp) -> TTImp
55+
56+
||| A function application, `f x`
57+
IApp : FC -> (f : TTImp) -> (x : TTImp) -> TTImp
58+
||| A named function application (for named parameters), e.g, `f {arg=x}`
59+
INamedApp : FC -> (f : TTImp) -> (arg : Name) -> (x : TTImp) -> TTImp
60+
||| An explicitly inserted auto implicit, `f @{x}`
61+
IAutoApp : FC -> (f : TTImp) -> (x : TTImp) -> TTImp
62+
||| A view in a `with` rule
5063
IWithApp : FC -> TTImp -> TTImp -> TTImp
5164

65+
||| `%search`
5266
ISearch : FC -> (depth : Nat) -> TTImp
67+
||| This operation is for expression that tries to typecheck expression in the list according to the given AltType and return either one of them, or default one (if present in the AltType), or fails
5368
IAlternative : FC -> AltType -> List TTImp -> TTImp
54-
IRewrite : FC -> TTImp -> TTImp -> TTImp
69+
||| A rewrite expression, `rewrite eq in exp`
70+
IRewrite : FC -> (eq : TTImp) -> (exp : TTImp) -> TTImp
5571

56-
-- Any implicit bindings in the scope should be bound here, using
57-
-- the given binder
72+
||| Any implicit bindings in the scope should be bound here, using
73+
||| the given binder
5874
IBindHere : FC -> BindMode -> TTImp -> TTImp
59-
-- A name which should be implicitly bound
75+
||| A name which should be implicitly bound
6076
IBindVar : FC -> Name -> TTImp
61-
-- An 'as' pattern, valid on the LHS of a clause only
62-
IAs : FC -> (nameFC : FC) -> UseSide -> Name -> TTImp -> TTImp
63-
-- A 'dot' pattern, i.e. one which must also have the given value
64-
-- by unification
77+
||| An 'as' pattern, valid on the LHS of a clause only, `group@pat`
78+
IAs : FC -> (nameFC : FC) -> UseSide -> (group : Name) -> (pat : TTImp) -> TTImp
79+
||| A 'dot' pattern, i.e. one which must also have the given value
80+
||| by unification, `.(...)`
6581
IMustUnify : FC -> DotReason -> TTImp -> TTImp
6682

6783
-- Laziness annotations
68-
IDelayed : FC -> LazyReason -> TTImp -> TTImp -- the type
69-
IDelay : FC -> TTImp -> TTImp -- delay constructor
84+
||| The delay type, `Delay t`
85+
IDelayed : FC -> LazyReason -> TTImp -> TTImp
86+
||| The constructor of `Delay`, `delay t`
87+
IDelay : FC -> TTImp -> TTImp
88+
||| `force`
7089
IForce : FC -> TTImp -> TTImp
7190

72-
-- Quasiquotation
91+
||| Quasi-quotation of expression (`( ... ))
7392
IQuote : FC -> TTImp -> TTImp
93+
||| Quasi-quotation of a name (`{ ... })
7494
IQuoteName : FC -> Name -> TTImp
95+
||| Quasi-quotation of a list of declarations (`[ ... ])
7596
IQuoteDecl : FC -> List Decl -> TTImp
97+
||| Unquote of an expression (~e)
7698
IUnquote : FC -> TTImp -> TTImp
77-
99+
||| A primitive value, such as an integer or string constant.
100+
||| Also any primitive *type*, apart from `Type` itself
78101
IPrimVal : FC -> (c : Constant) -> TTImp
102+
||| The type `Type`
79103
IType : FC -> TTImp
104+
||| A named hole
80105
IHole : FC -> String -> TTImp
81106

82-
-- An implicit value, solved by unification, but which will also be
83-
-- bound (either as a pattern variable or a type variable) if unsolved
84-
-- at the end of elaborator
107+
||| An implicit value, solved by unification, but which will also be
108+
||| bound (either as a pattern variable or a type variable) if unsolved
109+
||| at the end of elaborator.
110+
||| Note that `Implicit False` is `?`, while `Implicit True` is `_`
85111
Implicit : FC -> (bindIfUnsolved : Bool) -> TTImp
86-
IWithUnambigNames : FC -> List (FC, Name) -> TTImp -> TTImp
112+
||| `with name exp`
113+
IWithUnambigNames : FC -> (name : List (FC, Name)) -> (exp : TTImp) -> TTImp
87114
%name TTImp s, t, u
88115

116+
||| A record field update
89117
public export
90118
data IFieldUpdate : Type where
119+
||| `path := val`
91120
ISetField : (path : List String) -> TTImp -> IFieldUpdate
121+
||| `path $= val`
92122
ISetFieldApp : (path : List String) -> TTImp -> IFieldUpdate
93123

94124
%name IFieldUpdate upd
@@ -105,22 +135,23 @@ mutual
105135
NoInline : FnOpt
106136
Deprecate : FnOpt
107137
TCInline : FnOpt
108-
-- Flag means the hint is a direct hint, not a function which might
109-
-- find the result (e.g. chasing parent interface dictionaries)
138+
||| Flag means the hint is a direct hint, not a function which might
139+
||| find the result (e.g. chasing parent interface dictionaries)
110140
Hint : Bool -> FnOpt
111-
-- Flag means to use as a default if all else fails
141+
||| `%globalhint` if true, `%defaulthint` if false
112142
GlobalHint : Bool -> FnOpt
113143
ExternFn : FnOpt
114-
-- Defined externally, list calling conventions
144+
||| Defined externally, list calling conventions
115145
ForeignFn : List TTImp -> FnOpt
116-
-- Mark for export to a foreign language, list calling conventions
146+
||| Mark for export to a foreign language, list calling conventions
117147
ForeignExport : List TTImp -> FnOpt
118-
-- assume safe to cancel arguments in unification
148+
||| assume safe to cancel arguments in unification
119149
Invertible : FnOpt
120150
Totality : TotalReq -> FnOpt
151+
||| `%macro`
121152
Macro : FnOpt
122153
SpecArgs : List Name -> FnOpt
123-
154+
||| A name with an associated type
124155
public export
125156
data ITy : Type where
126157
MkTy : FC -> (n : WithFC Name) -> (ty : TTImp) -> ITy
@@ -129,11 +160,16 @@ mutual
129160

130161
public export
131162
data DataOpt : Type where
132-
SearchBy : List1 Name -> DataOpt -- determining arguments
133-
NoHints : DataOpt -- Don't generate search hints for constructors
134-
UniqueSearch : DataOpt -- auto implicit search must check result is unique
135-
External : DataOpt -- implemented externally
136-
NoNewtype : DataOpt -- don't apply newtype optimisation
163+
||| Determining arguments
164+
SearchBy : List1 Name -> DataOpt
165+
||| Don't generate search hints for constructors
166+
NoHints : DataOpt
167+
||| Auto implicit search must check result is unique
168+
UniqueSearch : DataOpt
169+
||| Implemented externally
170+
External : DataOpt
171+
||| Don't apply newtype optimization
172+
NoNewtype : DataOpt
137173

138174
%name DataOpt dopt
139175

@@ -165,15 +201,18 @@ mutual
165201

166202
public export
167203
data WithFlag = Syntactic
168-
204+
||| A clause in a function definition
169205
public export
170206
data Clause : Type where
207+
||| A simple pattern
171208
PatClause : FC -> (lhs : TTImp) -> (rhs : TTImp) -> Clause
209+
||| A pattern with views
172210
WithClause : FC -> (lhs : TTImp) ->
173211
(rig : Count) -> (wval : TTImp) -> -- with'd expression (& quantity)
174212
(prf : Maybe (Count, Name)) -> -- optional name for the proof (& quantity)
175213
(flags : List WithFlag) ->
176214
List Clause -> Clause
215+
||| An impossible pattern
177216
ImpossibleClause : FC -> (lhs : TTImp) -> Clause
178217

179218
%name Clause cl
@@ -209,22 +248,34 @@ mutual
209248
(opts : List FnOpt) ->
210249
(type : ITy) ->
211250
IClaimData
212-
251+
||| A top-level declaration
213252
public export
214253
data Decl : Type where
215-
IClaim : WithFC IClaimData -> Decl
216-
IData : FC -> WithDefault Visibility Private -> Maybe TotalReq -> Data -> Decl
217-
IDef : FC -> Name -> (cls : List Clause) -> Decl
254+
||| A type ascription, `a : b`.
255+
||| Called a claim because of Curry Howard, the statement `x : p` is equivalent to `x` is a proof of `p`.
256+
IClaim : (claim : WithFC IClaimData) -> Decl
257+
||| A data declaration
258+
IData : FC -> (vis : WithDefault Visibility Private) -> Maybe TotalReq -> (cons : Data) -> Decl
259+
||| A function definition by its clauses
260+
IDef : FC -> (f : Name) -> (cls : List Clause) -> Decl
261+
||| A parameter block
218262
IParameters : FC -> (params : List (Name, Count, PiInfo TTImp, TTImp)) ->
219263
(decls : List Decl) -> Decl
264+
||| A record declaration
265+
||| @ ns Nested namespace
220266
IRecord : FC ->
221-
Maybe String -> -- nested namespace
222-
WithDefault Visibility Private ->
223-
Maybe TotalReq -> Record -> Decl
267+
(ns : Maybe String) ->
268+
(vis : WithDefault Visibility Private) ->
269+
(totality : Maybe TotalReq) -> (rec : Record) -> Decl
270+
||| A namespace declaration, `namespace ns where decls`
224271
INamespace : FC -> Namespace -> (decls : List Decl) -> Decl
272+
||| A transformation declaration
225273
ITransform : FC -> Name -> TTImp -> TTImp -> Decl
274+
||| A top-level elaboration run
226275
IRunElabDecl : FC -> TTImp -> Decl
276+
||| A logging directive
227277
ILog : Maybe (List String, Nat) -> Decl
278+
||| A builtin declaration, `%builtin type name`
228279
IBuiltin : FC -> BuiltinType -> Name -> Decl
229280

230281
%name Decl decl

0 commit comments

Comments
 (0)