Skip to content

Commit 72a1159

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

File tree

1 file changed

+70
-20
lines changed

1 file changed

+70
-20
lines changed

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

Lines changed: 70 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -29,59 +29,104 @@ 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 arguement
3234
public export
3335
data TTImp : Type where
36+
||| A variable reference, by name
3437
IVar : FC -> Name -> TTImp
38+
||| A function type
39+
||| @ Count the multiplicity of the arguement
40+
||| @ PiInfo If the arguement is implicit, explicit, auto implicit or a default implicit
41+
||| @ (Maybe Name) the optional index, such as `x` in `(x : Type) -> Type`
42+
||| @ argTy the type of the argument
43+
||| @ retTy the return type
3544
IPi : FC -> Count -> PiInfo TTImp -> Maybe Name ->
3645
(argTy : TTImp) -> (retTy : TTImp) -> TTImp
46+
||| A lambda abstraction
47+
||| @ Count the multiplicity of the arguement
48+
||| @ PiInfo If the arguement is implicit, explicit, auto implicit or a default implicit
49+
||| @ (Maybe Name) the optional arguement
50+
||| @ argTy the type of the argument
51+
||| @ lamTy the return type
3752
ILam : FC -> Count -> PiInfo TTImp -> Maybe Name ->
3853
(argTy : TTImp) -> (lamTy : TTImp) -> TTImp
54+
||| A let binding
55+
||| @ lhsFC The file context of the left-hand side
56+
||| @ Count the multiplicity of the binding
57+
||| @ Name the name being bound
58+
||| @ nTy the type of the binding
59+
||| @ nVal the value to bind `Name` to
60+
||| @ scope the body of the let expression
3961
ILet : FC -> (lhsFC : FC) -> Count -> Name ->
4062
(nTy : TTImp) -> (nVal : TTImp) ->
4163
(scope : TTImp) -> TTImp
64+
||| A case expression
65+
||| @ (List FnOpt) options for when the case expression is lifted
66+
||| @ TTImp the scrutinee
67+
||| @ ty the type of the scrutinee
68+
||| @ (List Clause) the branches of the case expression
4269
ICase : FC -> List FnOpt -> TTImp -> (ty : TTImp) ->
4370
List Clause -> TTImp
71+
||| A list of full declerations local to a term
72+
||| @ (List Decl) the list of declerations
73+
||| @ TTImp the body of the local declaration
4474
ILocal : FC -> List Decl -> TTImp -> TTImp
75+
||| An update to a record value
76+
||| @ (List IFieldUpdate) the list of field update descriptions
77+
||| @ TTImp the record value being updated
4578
IUpdate : FC -> List IFieldUpdate -> TTImp -> TTImp
46-
79+
||| A function application
4780
IApp : FC -> TTImp -> TTImp -> TTImp
81+
||| A named function application (for named parameters), e.g, `f {x=3}`
4882
INamedApp : FC -> TTImp -> Name -> TTImp -> TTImp
83+
||| An explicitly inserted auto implicit, `f @{x}`
4984
IAutoApp : FC -> TTImp -> TTImp -> TTImp
85+
||| A view in a `with` rule
5086
IWithApp : FC -> TTImp -> TTImp -> TTImp
51-
87+
||| `%search`
5288
ISearch : FC -> (depth : Nat) -> TTImp
5389
IAlternative : FC -> AltType -> List TTImp -> TTImp
90+
||| A rewrite expression, `rewrite p in q`
5491
IRewrite : FC -> TTImp -> TTImp -> TTImp
5592

56-
-- Any implicit bindings in the scope should be bound here, using
57-
-- the given binder
93+
||| Any implicit bindings in the scope should be bound here, using
94+
||| the given binder
5895
IBindHere : FC -> BindMode -> TTImp -> TTImp
59-
-- A name which should be implicitly bound
96+
||| A name which should be implicitly bound
6097
IBindVar : FC -> Name -> TTImp
61-
-- An 'as' pattern, valid on the LHS of a clause only
98+
||| An 'as' pattern, valid on the LHS of a clause only
6299
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
100+
||| A 'dot' pattern, i.e. one which must also have the given value
101+
||| by unification
65102
IMustUnify : FC -> DotReason -> TTImp -> TTImp
66103

67-
-- Laziness annotations
104+
||| Laziness annotations
105+
||| The delay type, `Delay t`
68106
IDelayed : FC -> LazyReason -> TTImp -> TTImp -- the type
107+
||| The constructor of `Delay`, `delay t`
69108
IDelay : FC -> TTImp -> TTImp -- delay constructor
109+
||| `force`
70110
IForce : FC -> TTImp -> TTImp
71111

72-
-- Quasiquotation
112+
||| Quasi-quotation of expression (`( ... ))
73113
IQuote : FC -> TTImp -> TTImp
114+
||| Quasi-quotation of a name (`{ ... })
74115
IQuoteName : FC -> Name -> TTImp
116+
||| Quasi-quotation of a list of declarations (`[ ... ])
75117
IQuoteDecl : FC -> List Decl -> TTImp
118+
||| Unquote of an expression (~e)
76119
IUnquote : FC -> TTImp -> TTImp
77-
120+
||| A primitive value, such as an integer or string constant
78121
IPrimVal : FC -> (c : Constant) -> TTImp
122+
||| The type `Type`
79123
IType : FC -> TTImp
124+
||| A named hole
80125
IHole : FC -> String -> TTImp
81126

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
127+
||| An implicit value, solved by unification, but which will also be
128+
||| bound (either as a pattern variable or a type variable) if unsolved
129+
||| at the end of elaborator
85130
Implicit : FC -> (bindIfUnsolved : Bool) -> TTImp
86131
IWithUnambigNames : FC -> List (FC, Name) -> TTImp -> TTImp
87132
%name TTImp s, t, u
@@ -105,17 +150,17 @@ mutual
105150
NoInline : FnOpt
106151
Deprecate : FnOpt
107152
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)
153+
||| Flag means the hint is a direct hint, not a function which might
154+
||| find the result (e.g. chasing parent interface dictionaries)
110155
Hint : Bool -> FnOpt
111-
-- Flag means to use as a default if all else fails
156+
||| Flag means to use as a default if all else fails
112157
GlobalHint : Bool -> FnOpt
113158
ExternFn : FnOpt
114-
-- Defined externally, list calling conventions
159+
||| Defined externally, list calling conventions
115160
ForeignFn : List TTImp -> FnOpt
116-
-- Mark for export to a foreign language, list calling conventions
161+
||| Mark for export to a foreign language, list calling conventions
117162
ForeignExport : List TTImp -> FnOpt
118-
-- assume safe to cancel arguments in unification
163+
||| assume safe to cancel arguments in unification
119164
Invertible : FnOpt
120165
Totality : TotalReq -> FnOpt
121166
Macro : FnOpt
@@ -129,10 +174,15 @@ mutual
129174

130175
public export
131176
data DataOpt : Type where
177+
||| Determing arguements
132178
SearchBy : List1 Name -> DataOpt -- determining arguments
179+
||| Don't generate search hints for constructors
133180
NoHints : DataOpt -- Don't generate search hints for constructors
181+
||| Auto implicit search must check result is unique
134182
UniqueSearch : DataOpt -- auto implicit search must check result is unique
183+
||| Implemented externally
135184
External : DataOpt -- implemented externally
185+
||| Don't apply newtype optimisation
136186
NoNewtype : DataOpt -- don't apply newtype optimisation
137187

138188
%name DataOpt dopt

0 commit comments

Comments
 (0)