-
Notifications
You must be signed in to change notification settings - Fork 395
Map of the Source Code
Trying to fix a bug or hack on a feature but don't know where to start? This page will hopefully help!
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!
https://github.com/idris-lang/Idris2/blob/main/docs/source/implementation/overview.rst
In general, the sources for interactive editing can be found in the src/TTImp/Interactive/ directory.
The case splitting machinery lives in src/TTImp/Interactive/CaseSplit.idr.
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.
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).
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.
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
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.
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.
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.
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.
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.