Skip to content

docs: added library documentation for Elab #3635

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

docs: added library documentation for Elab #3635

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9e44bd9
docs: added library documentation for `Elab`
wizard7377 Aug 31, 2025
17616e9
fix: made doc changes non-breaking
wizard7377 Sep 1, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 21 additions & 21 deletions libs/base/Language/Reflection.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,49 +62,49 @@ data Elab : Type -> Type where

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

-- Elaborate a TTImp term to a concrete value
||| Elaborate a TTImp term to a concrete value
Check : TTImp -> Elab expected
-- Quote a concrete expression back to a TTImp
||| Quote a concrete expression back to a TTImp
Quote : (0 _ : val) -> Elab TTImp

-- Elaborate under a lambda
||| Elaborate under a lambda
Lambda : (0 x : Type) ->
{0 ty : x -> Type} ->
((val : x) -> Elab (ty val)) -> Elab ((val : x) -> (ty val))

-- Get the current goal type, if known
-- (it might need to be inferred from the solution)
||| Get the current goal type, if known
||| (it might need to be inferred from the solution)
Goal : Elab (Maybe TTImp)
-- Get the names of local variables in scope
||| Get the names of local variables in scope
LocalVars : Elab (List Name)
-- Generate a new unique name, based on the given string
||| Generate a new unique name, based on the given string
GenSym : String -> Elab Name
-- Put a name in the current namespace
||| Put a name in the current namespace
InCurrentNS : Name -> Elab Name
-- Get the types of every name which matches.
-- There may be ambiguities - returns a list of fully explicit names
-- and their types. If there's no results, the name is undefined.
||| Get the types of every name which matches.
||| There may be ambiguities - returns a list of fully explicit names
||| and their types. If there's no results, the name is undefined.
GetType : Name -> Elab (List (Name, TTImp))
-- Get the metadata associated with a name
||| Get the metadata associated with a name
GetInfo : Name -> Elab (List (Name, NameInfo))
-- Get the visibility associated with a name
||| Get the visibility associated with a name
GetVis : Name -> Elab (List (Name, Visibility))
-- Get the type of a local variable
||| Get the type of a local variable
GetLocalType : Name -> Elab TTImp
-- Get the constructors of a data type. The name must be fully resolved.
||| Get the constructors of a data type. The name must be fully resolved.
GetCons : Name -> Elab (List Name)
-- Get all function definition names referred in a definition. The name must be fully resolved.
||| Get all function definition names referred in a definition. The name must be fully resolved.
GetReferredFns : Name -> Elab (List Name)
-- Get the name of the current and outer functions, if it is applicable
||| Get the name of the current and outer functions, if it is applicable
GetCurrentFn : Elab (SnocList Name)
-- Check a group of top level declarations
||| Check a group of top level declarations
Declare : List Decl -> Elab ()

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

export
Expand Down
49 changes: 33 additions & 16 deletions libs/base/Language/Reflection/TT.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,14 +6,14 @@ import public Data.String
import Decidable.Equality

%default total

||| namespace, stored in reverse order
public export
data Namespace = MkNS (List String) -- namespace, stored in reverse order
data Namespace = MkNS (List String)

%name Namespace ns

||| module identifier, stored in reverse order
public export
data ModuleIdent = MkMI (List String) -- module identifier, stored in reverse order
data ModuleIdent = MkMI (List String)

%name ModuleIdent mi

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

-- 'FilePos' represents the position of
-- the source information in the file (or REPL).
-- in the form of '(line-no, column-no)'.
||| 'FilePos' represents the position of
||| the source information in the file (or REPL).
||| in the form of '(line-no, column-no)'.
public export
FilePos : Type
FilePos = (Int, Int)
Expand Down Expand Up @@ -187,6 +187,7 @@ Show Constant where
show (PrT x) = show x
show WorldVal = "%World"

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

%name UserName un

public export
data Name = NS Namespace Name -- name in a namespace
| UN UserName -- user defined name
| MN String Int -- machine generated name
| DN String Name -- a name and how to display it
| Nested (Int, Int) Name -- nested function name
| CaseBlock String Int -- case block nested in (resolved) name
| WithBlock String Int -- with block nested in (resolved) name
||| A name in a Idris program
public export
data Name : Type where
||| A qualified name
NS : Namespace -> Name -> Name
||| A user defined name
UN : UserName -> Name
||| A machine generated name
MN : String -> Int -> Name
||| A name with a display string
DN : String -> Name -> Name
||| Nested function name
Nested : (Int, Int) -> Name -> Name
||| Case block nested in (resolved) name
CaseBlock : String -> Int -> Name
||| With block nested in (resolved) name
WithBlock : String -> Int -> Name

%name Name nm

Expand Down Expand Up @@ -251,8 +261,15 @@ record NameInfo where
constructor MkNameInfo
nametype : NameType

||| A multiplicity
public export
data Count = M0 | M1 | MW
data Count : Type where
||| 0 (erased)
M0 : Count
||| 1 (linear)
M1 : Count
||| ω (unrestricted)
MW : Count
%name Count rig

export
Expand Down
145 changes: 98 additions & 47 deletions libs/base/Language/Reflection/TTImp.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,66 +29,96 @@ mutual
| UnderAppliedCon
%name DotReason dr

||| The elaborator representation of an Idris term
||| All of these take a file context `FC` as their first argument
public export
data TTImp : Type where
||| A variable reference, by name
IVar : FC -> Name -> TTImp
IPi : FC -> Count -> PiInfo TTImp -> Maybe Name ->
||| A function type, of the form `(mult binder : argTy) -> retTy`, with implicitness determined by `info`
IPi : FC -> (mult : Count) -> (info : PiInfo TTImp) -> (binder : Maybe Name) ->
Comment on lines +38 to +39
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Could you please change info to piinfo, because info seems to be too generic

(argTy : TTImp) -> (retTy : TTImp) -> TTImp
ILam : FC -> Count -> PiInfo TTImp -> Maybe Name ->
||| A lambda abstraction, of the form`\(mult binder : argTy) => retTy`, with implicitness determined by `info`
ILam : FC -> (mult : Count) -> (info : PiInfo TTImp) -> (binder : Maybe Name) ->
(argTy : TTImp) -> (lamTy : TTImp) -> TTImp
ILet : FC -> (lhsFC : FC) -> Count -> Name ->
||| A let binding, of the form `let mult var : nTy = nVal in scope`
ILet : FC -> (lhsFC : FC) -> (mult : Count) -> (var : Name) ->
(nTy : TTImp) -> (nVal : TTImp) ->
(scope : TTImp) -> TTImp
ICase : FC -> List FnOpt -> TTImp -> (ty : TTImp) ->
List Clause -> TTImp
ILocal : FC -> List Decl -> TTImp -> TTImp
IUpdate : FC -> List IFieldUpdate -> TTImp -> TTImp

IApp : FC -> TTImp -> TTImp -> TTImp
INamedApp : FC -> TTImp -> Name -> TTImp -> TTImp
IAutoApp : FC -> TTImp -> TTImp -> TTImp
||| A case expression `case val : ty of clauses`
ICase : FC -> (opts : List FnOpt) -> (val : TTImp) -> (ty : TTImp) ->
(clauses : List Clause) -> TTImp
||| A list of full declarations local to a term
ILocal : FC -> (context : List Decl) -> (term : TTImp) -> TTImp
||| An update to a record value, `{ updates } val`
IUpdate : FC -> (updates : List IFieldUpdate) -> (val : TTImp) -> TTImp

||| A function application, `f x`
IApp : FC -> (f : TTImp) -> (x : TTImp) -> TTImp
||| A named function application (for named parameters), e.g, `f {arg=x}`
INamedApp : FC -> (f : TTImp) -> (arg : Name) -> (x : TTImp) -> TTImp
||| An explicitly inserted auto implicit, `f @{x}`
IAutoApp : FC -> (f : TTImp) -> (x : TTImp) -> TTImp
||| A view in a `with` rule
IWithApp : FC -> TTImp -> TTImp -> TTImp
Comment on lines +62 to 63
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is not a view. View with with-rule is done through appropriate WithClause consturctor of the Clause data type. IWithApp is an application in form of f | arg which can be used only inside with-clauses.


||| `%search`
ISearch : FC -> (depth : Nat) -> TTImp
||| 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
IAlternative : FC -> AltType -> List TTImp -> TTImp
Copy link
Collaborator

@buzden buzden Sep 1, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Author

@wizard7377 wizard7377 Sep 1, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Because I'm not familiar with this, I'm just going to copy paste your description if that's alright with you

Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it's okay

IRewrite : FC -> TTImp -> TTImp -> TTImp
||| A rewrite expression, `rewrite eq in exp`
IRewrite : FC -> (eq : TTImp) -> (exp : TTImp) -> TTImp

-- Any implicit bindings in the scope should be bound here, using
-- the given binder
||| Any implicit bindings in the scope should be bound here, using
||| the given binder
IBindHere : FC -> BindMode -> TTImp -> TTImp
Comment on lines +72 to 74
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd say "A bound for implicit bindings to be automatically bound using the given bind mode"

-- A name which should be implicitly bound
||| A name which should be implicitly bound
IBindVar : FC -> Name -> TTImp
-- An 'as' pattern, valid on the LHS of a clause only
IAs : FC -> (nameFC : FC) -> UseSide -> Name -> TTImp -> TTImp
-- A 'dot' pattern, i.e. one which must also have the given value
-- by unification
||| An 'as' pattern, valid on the LHS of a clause only, `group@pat`
IAs : FC -> (nameFC : FC) -> UseSide -> (group : Name) -> (pat : TTImp) -> TTImp
||| A 'dot' pattern, i.e. one which must also have the given value
||| by unification, `.(...)`
IMustUnify : FC -> DotReason -> TTImp -> TTImp

-- Laziness annotations
IDelayed : FC -> LazyReason -> TTImp -> TTImp -- the type
IDelay : FC -> TTImp -> TTImp -- delay constructor
||| The delay type, `Delay t`
IDelayed : FC -> LazyReason -> TTImp -> TTImp
Comment on lines +84 to +85
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Delay types are Lazy and Inf (depending on the LazyReason argument). Delay is a constructor of a lazy value, it is of type a -> Lazy a or a -> Inf a depending on the context

||| The constructor of `Delay`, `delay t`
IDelay : FC -> TTImp -> TTImp
Comment on lines +86 to +87
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

delay is just a library function, the constructor-like thing in the surface language is Delay (with an upper-case letter`

||| `force`
IForce : FC -> TTImp -> TTImp
Comment on lines +88 to 89
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The same for above, IForce corresponds to the Force pseudo-constuctor, force is just a function


-- Quasiquotation
||| Quasi-quotation of expression (`( ... ))
IQuote : FC -> TTImp -> TTImp
||| Quasi-quotation of a name (`{ ... })
IQuoteName : FC -> Name -> TTImp
||| Quasi-quotation of a list of declarations (`[ ... ])
IQuoteDecl : FC -> List Decl -> TTImp
||| Unquote of an expression (~e)
IUnquote : FC -> TTImp -> TTImp

||| A primitive value, such as an integer or string constant.
||| Also any primitive *type*, apart from `Type` itself
IPrimVal : FC -> (c : Constant) -> TTImp
||| The type `Type`
IType : FC -> TTImp
||| A named hole
IHole : FC -> String -> TTImp

-- An implicit value, solved by unification, but which will also be
-- bound (either as a pattern variable or a type variable) if unsolved
-- at the end of elaborator
||| An implicit value, solved by unification, but which will also be
||| bound (either as a pattern variable or a type variable) if unsolved
||| at the end of elaborator.
Comment on lines +108 to +109
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't understand what is said about the bound. I mean, if Implicit False is used, unsolvedness of this expression is a compilation error. But when it is unsolved and it is Implicit True, then this expression is bound to a fresh variable.

||| Note that `Implicit False` is `?`, while `Implicit True` is `_`
Implicit : FC -> (bindIfUnsolved : Bool) -> TTImp
IWithUnambigNames : FC -> List (FC, Name) -> TTImp -> TTImp
||| `with name exp`
IWithUnambigNames : FC -> (name : List (FC, Name)) -> (exp : TTImp) -> TTImp
Comment on lines +112 to +113
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd add that except it is with name exp, this is a disambiguation expression, i.e. when a name matches with one of names given in the list, it disambiguates to these names instead of searching for all applicable names. Also, please, rename the name argument, since it is a list. I think names should apply

%name TTImp s, t, u

||| A record field update
public export
data IFieldUpdate : Type where
||| `path := val`
ISetField : (path : List String) -> TTImp -> IFieldUpdate
||| `path $= val`
ISetFieldApp : (path : List String) -> TTImp -> IFieldUpdate

%name IFieldUpdate upd
Expand All @@ -105,22 +135,23 @@ mutual
NoInline : FnOpt
Deprecate : FnOpt
TCInline : FnOpt
-- Flag means the hint is a direct hint, not a function which might
-- find the result (e.g. chasing parent interface dictionaries)
||| Flag means the hint is a direct hint, not a function which might
||| find the result (e.g. chasing parent interface dictionaries)
Hint : Bool -> FnOpt
-- Flag means to use as a default if all else fails
||| `%globalhint` if true, `%defaulthint` if false
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
||| `%globalhint` if true, `%defaulthint` if false
||| A hint that is searched if direct hints search failed.
||| `%globalhint` if the argument is `True`, `%defaulthint` if `False`.

GlobalHint : Bool -> FnOpt
ExternFn : FnOpt
-- Defined externally, list calling conventions
||| Defined externally, list calling conventions
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
||| Defined externally, list calling conventions
||| Defined externally, takes a list of calling conventions

ForeignFn : List TTImp -> FnOpt
-- Mark for export to a foreign language, list calling conventions
||| Mark for export to a foreign language, list calling conventions
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
||| Mark for export to a foreign language, list calling conventions
||| Mark for export to a foreign language, takes a list of calling conventions

ForeignExport : List TTImp -> FnOpt
-- assume safe to cancel arguments in unification
||| assume safe to cancel arguments in unification
Invertible : FnOpt
Totality : TotalReq -> FnOpt
||| `%macro`
Macro : FnOpt
SpecArgs : List Name -> FnOpt

||| A name with an associated type
public export
data ITy : Type where
MkTy : FC -> (n : WithFC Name) -> (ty : TTImp) -> ITy
Expand All @@ -129,11 +160,16 @@ mutual

public export
data DataOpt : Type where
SearchBy : List1 Name -> DataOpt -- determining arguments
NoHints : DataOpt -- Don't generate search hints for constructors
UniqueSearch : DataOpt -- auto implicit search must check result is unique
External : DataOpt -- implemented externally
NoNewtype : DataOpt -- don't apply newtype optimisation
||| Determining arguments
SearchBy : List1 Name -> DataOpt
||| Don't generate search hints for constructors
NoHints : DataOpt
||| Auto implicit search must check result is unique
UniqueSearch : DataOpt
||| Implemented externally
External : DataOpt
||| Don't apply newtype optimization
NoNewtype : DataOpt

%name DataOpt dopt

Expand Down Expand Up @@ -165,15 +201,18 @@ mutual

public export
data WithFlag = Syntactic

||| A clause in a function definition
public export
data Clause : Type where
||| A simple pattern
PatClause : FC -> (lhs : TTImp) -> (rhs : TTImp) -> Clause
||| A pattern with views
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe, we could add the surface syntax here, like

<lhs> with <rig> (<wval>) proof <prf>
  <subclauses>

WithClause : FC -> (lhs : TTImp) ->
(rig : Count) -> (wval : TTImp) -> -- with'd expression (& quantity)
(prf : Maybe (Count, Name)) -> -- optional name for the proof (& quantity)
(flags : List WithFlag) ->
List Clause -> Clause
||| An impossible pattern
ImpossibleClause : FC -> (lhs : TTImp) -> Clause

%name Clause cl
Expand Down Expand Up @@ -209,22 +248,34 @@ mutual
(opts : List FnOpt) ->
(type : ITy) ->
IClaimData

||| A top-level declaration
public export
data Decl : Type where
IClaim : WithFC IClaimData -> Decl
IData : FC -> WithDefault Visibility Private -> Maybe TotalReq -> Data -> Decl
IDef : FC -> Name -> (cls : List Clause) -> Decl
||| A type ascription, `a : b`.
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Type ascription term is used then you try to refine the type of an expression. I think, this should be called "a function signature"

||| Called a claim because of Curry Howard, the statement `x : p` is equivalent to `x` is a proof of `p`.
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure this line is a valid one. I thought it is a claim because it starts definition of a function, but does not define its body

IClaim : (claim : WithFC IClaimData) -> Decl
||| A data declaration
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
||| A data declaration
||| A data type declaration

IData : FC -> (vis : WithDefault Visibility Private) -> Maybe TotalReq -> (cons : Data) -> Decl
||| A function definition by its clauses
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
||| A function definition by its clauses
||| A function body definition

IDef : FC -> (f : Name) -> (cls : List Clause) -> Decl
||| A parameter block
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd suggest giving an example here, something like

Suggested change
||| A parameter block
||| A parameters block, e.g. `parameters {0 m : _} {auto _ : Monad m} (level : Nat)

IParameters : FC -> (params : List (Name, Count, PiInfo TTImp, TTImp)) ->
(decls : List Decl) -> Decl
||| A record declaration
||| @ ns Nested namespace
IRecord : FC ->
Maybe String -> -- nested namespace
WithDefault Visibility Private ->
Maybe TotalReq -> Record -> Decl
(ns : Maybe String) ->
(vis : WithDefault Visibility Private) ->
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there any need for names here? I suppose, their types are self expanatory and they are not used on the documentation either, so these names, I think, just clutter reading. What do you think?

(totality : Maybe TotalReq) -> (rec : Record) -> Decl
||| A namespace declaration, `namespace ns where decls`
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In namespace syntax where is not where, a newline with a indent or { ... } should go there

INamespace : FC -> Namespace -> (decls : List Decl) -> Decl
||| A transformation declaration
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
||| A transformation declaration
||| A transformation rule declaration

ITransform : FC -> Name -> TTImp -> TTImp -> Decl
||| A top-level elaboration run
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
||| A top-level elaboration run
||| A top-level elaborator script run, `%runElab`

IRunElabDecl : FC -> TTImp -> Decl
||| A logging directive
Copy link
Collaborator

@buzden buzden Sep 2, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
||| A logging directive
||| A directive for enabling compile-time logging, `%logging "<topic>" <level>`

ILog : Maybe (List String, Nat) -> Decl
||| A builtin declaration, `%builtin type name`
IBuiltin : FC -> BuiltinType -> Name -> Decl

%name Decl decl
Expand Down