Pipeline

Documentation on the Juvix compiler pipeline

Pipeline

This section provides an overview of the compiler pipeline, from a source text file to the specific backend calls to produce the binary.

The in code explanation in that image can be itself be more boxed into what we see in app/main.hs

  Compile fin fout (Michelson backend) ->
    liftIO (readFile fin)
      >>= Pipeline.parse
      >>= Pipeline.typecheck @Pipeline.BMichelson
      >>= Pipeline.compile @Pipeline.BMichelson
      >>= Pipeline.writeout fout
      >>= liftIO . print

Parsing

The first set of phases to happen is that the text file is turned into a structured document, namely an ML AST.

Transition

This is a long phase of the compiler where we do a few things.

The first is that we desugar the expression using baked in expansions. This happens for function definitions, punned arguments, etc.
After that, we then take the desugared s-expressions and put them in our global "context". We do some extra processing in this stage as well like resolving what modules open each other.
- A context is like a primitive image. It can access all the information in a nested hashtable of sorts.
We still have a few more passes to run, as phases like symbol resolution and infix resolution can be run now.
Finally we have one last pass, translating what is left of the S-expression AST into a format where Core understands.

Core

Currently in our compiler the Pipeline.typecheck and Pipeline.compile function are backend specific, however the general transformations are similar regardless of the backend.

HR

This layer of core stand for Human Readable, as we have variable names instead of hairy de-bruijn indices. This phase is shortly lived, as most processing at this level wants to work on some extension of the Internal Representation as names create issues for the various algorithms.

IR

This is where the main process of type checking happens.

Names are reduced to de-bruijn indices.
We have many extensions with metadata that fluctuate depending on what pass of core is run.

Eliminations

In this phase of Core, we remove the types from the terms, as they don't serve any computation purpose. By this point we've done most of the processing we need.

In the future I suspect inlining algorithms will either be done here or in IR right above.

Pipeline

Pipeline

Parsing

Transition

Core

HR

IR

Eliminations

Backends

Michelson

LLVM

Arithmetic Circuit

Idealized Pipeline