Idris2

Didn't find what you were looking for and then spent ages searching for it with rg (or grep) and find? Please add it here to save the next person (and your future self) the trouble!

Documentation notes

https://github.com/idris-lang/Idris2/blob/main/docs/source/implementation/overview.rst

Interactive Editing

In general, the sources for interactive editing can be found in the src/TTImp/Interactive/ directory.

Case splitting

The case splitting machinery lives in src/TTImp/Interactive/CaseSplit.idr.

Logging

Adding `log` statements

To add a log statement somewhere in the Idris sources, you'll need a log level (e.g. 3), one of the knownTopics from src/Core/Options/Logging.idr, and a string with the stuff you want to log. You may also be interested in the coreLift and/or coreRun functions from src/Core/Core.idr.

Primitives

Mapping primitive operations to backend functions

The data type for primitive functions is PrimFn, found in src/Core/TT.idr. These are converted to names by opName, and to terms in the allPrimitives list, both from src/Core/Primitives.idr. Primitives are added to the compiler context by addPrimitives in src/Core/InitPrimitives.idr.

During code generation in the backends they are compiled to backend code by schOp from src/Compiler/Scheme/Common.idr (for the Scheme backends) and by jsOp from Compiler.ES.Codegen.idr (for the JS backends).

Compiling

In general, the source for the compilers can be found in src/Compiler.

Functionality shared between code gen targets (backends) is typically found in a Common.idr file, for example the Racket Scheme and Chez Scheme backends have some shared functionality found in src/Compiler/Scheme/Common.idr.

Case Trees

The data types describing case trees are found in src/Core/Case/CaseTree.idr. These then get compiled to their runtime representation by the functionality found in src/Core/Case/CaseBuilder.idr

Lexing and Parsing

The parser and lexer are mainly implemented in src/Parser. Within that tree, modules named Source.idr apply to Idris source code, and modules named Package.idr apply to Idris IPKG files. These modules also depend on several standalone types and functions defined in src/Libraries/Text.

There is a blog post from 2021 with additional descriptions of these and other related modules: https://alexhumphreys.github.io/2021/08/29/the-parsers-of-idris2.html. TODO: that information should be summarized here, and reviewed by an Idris core developer.

REPL

Functionality implementing the Idris2 REPL is spread across different modules. The core functionality (handling REPL commands and printing the results) is in module Idris.REPL. Available REPL commands are encoded in data type REPLCmd in module Idris.Syntax. Module Idris.REPL.Common has data types and functionality for describing the current state of the REPL, while options affecting how the REPL operates can be found in Idris.REPL.Opts. Parsing of REPL commands is done in Idris.Parser, from around line 1922 onwards.

Packages

Module Idris.Package is the entry point for all package related stuff. It defines the grammar of .ipkg files as well as handlers for the different package related commands like --build or --typecheck.

The fields available in .ipkg files are defined via data type Idris.Package.Types.PkgDesc.

Finally, module Idris.Package.Init implements the --init command for interactively generating a new .ipkg file in a project.

Documentation

Modules in folder src/Idris/Doc implement the different forms of documentation available in Idris. Module Idris.Doc.String provides functionality for pretty printing doc strings from source files (using the pretty printer from Libraries.Text.PrettyPrint.Prettyprinter), but also provides documentation when running :doc in the REPL (via function getDocs). In module Idris.Doc.HTML prettified doc strings are rendered to HTML when running idris2 --mkdoc. Modules Idris.Doc.Annotations, Idris.Doc.Brackets, and Idris.Doc.Keywords provide documentation for additional concepts available via the :doc command in the REPL. Finally, module Idris.Doc.Display provides pretty printers for Idris terms and definitions.

Idris2 Executable

Command Line Options

Command line options are define in src/Idris/CommandLine.idr. They are parsed in function Idris.CommandLine.getOpts (function Idris.CommandLine.getCmdOpts reads them from the list of command line arguments). Module src/Idris/SetOptions.idr provides the functionality for processing the command line options specified by the user. This is also where the BASH autocompletion script is implemented.

About