published on March 15, 2016
So after looking at the parser in the last post, this post will explore what happens after an Idris has been parsed, namely how it is desugared and elaborated to a TT program.
loadInputs loads a list of Idris files, meaning that it tries to completely process these files (reading, parsing, elaborating, saving the state in the
IState) and all their dependencies. It uses the
buildTree function from
Chaser.hs to retrieve the actual files along with modification times and indicating if a file needs to be re-loaded. It uses the locally defined
tryLoad function, which uses
Parser.hs which either re-loads an existing IBC file or processes a file via the
loadSource function. Similarly, the
loadModule function also checks if a module is already loaded, if not either loads it from an up-to-date IBC file or ends up loading it from source via
loadSource. So either way
loadSource seems like an important part of processing and loading source files in Idris ;).
loadSource does a lot of things1, such as loading all required IBC files for modules required by that file (which presumably must exist at this point), clears the current IBC cache, parses the file with the
parseProg function and then (dam, dam, dam), goes on to elaborate and typecheck the loaded program by calling
elabDecls on the parsed declarations.
So looking at Idris as a compiler (as opposed to say the REPL functionality), the
elabDecls seems to be the most important entry point into the elaborator. The
process function which seems to be processing REPL commands is also an interesting entry point, as it is processing pieces of Idris code in smaller chunks. It ends up making a few calls to the
elabREPL (which is a wrapper with a catch around
All in all, we’ve basically looked a bit more at how the elaborator ends up being invoked, but not at how it really works. Unfortunately, the latter is really a bit beyond of the scope of these blog posts (at least for now), where I try to familiarize myself with the Idris code base bit by bit. The design and implementation paper (PDF) by Edwin Brady goes into some details of how elaboration works, I am not yet confident to explore this topic here.
I must admit I am a bit unhappy with the plethora of 150+ line monadic functions in the Idris source code, but that’s just a newbie complaining….↩