Types and Tailcalls

A Look at the Idris Internals, Part III: From Parsing to Elaboration

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.

Looking throught the idrisMain method in REPL.hs, it seems that code is actually loaded by either the loadInputs function (also in REPL.hs) or the loadModule from Parser.hs.

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 loadFromIFile from 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 elabVal and elabREPL (which is a wrapper with a catch around elabVal) functions.

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.

  1. 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….

comments powered by Disqus