This the multi-page printable view of this section. Click here to print.

Return to the regular view of this page.

IR

1 - Representation

Representation

Global

  • A lot of the global information predates the frontend context. A lot can probably be integrated.

  • Raw Globals Type is a term, which may not be correct (what the user wrote), Regular global the types are values, which can be checked for equality eaiser.

    • Only safe to eval something after it's been type checked

    • Way to unify?

2 - Extensions

Extensions

Extensions are an important part of Core IR. They allow certain kinds of transformations

Transformation

3 - Evaluator

Evaluation of the internal representation in Juvix plays an important part in the compilation pipeline: it simplifies the program before passing it to the backend. As the internal representation is closely related to the λ-calculus with de Bruijn indices, the evaluator implements all necessary functions to do so.

In addition to the evaluation functions, the module provides functions for inlining globals (inlineAllGlobals / inlineAllGlobalsElim), turning function definitions into anonymous functions (toLambda), lookup functions for variables and filtering functions for extensions.

For more information on the λ-calculus with de Bruijn indices, see Wikipedia article. This document will describe the way the theory is implemented for Juvix, and expects a basic understanding of the λ-calculus with de Bruijn indices.

Substitution boils down to replacing the variables bound under the current λ, after which the free variables in the term need to be updated to reflect the removal of an abstraction layer, this is the task of weakening.

Substitution

Substitution lies at the core of evaluation, replacing bound variables with terms. Currently the compiler contains several closely related substitution implementations, both for terms and patterns. All of them serve the same purpose, but differ slightly in their types.

Term substitution

  • substWith: Substitutes any term a with an IR.Elim', but results in a term of type a.

  • substTermWith: Substitutes any term a with an IR.Elim', and results in an IR.Elim'.

  • gsubstWith: Generic substitution of f t with an IR.Elim', and results an f t again. This generic is used for automatic deriving of instances using GHC.Generics.

Pattern substitution

The functions are for substituting patterns, each of them take:

  • A number indicating the current traversal depth.

  • A IR.PatternMap containing pairs of pattern variables and terms.

All the functions return an Either with a PatternVar in case not substitution has happened, and the resulting term in case of a substitution.

  • patSubst': Substitutes any term a with any of the patterns provided in the map, and results in an a.

  • patSubstTerm': Substitutes any term a with any of the patterns provided in the map, and results in an IR.Term'.

  • gpatSubst': Generic substitution any term f t with any of the patterns provided in the map, and results in an f t. This generic is used for automatic deriving of instances using GHC.Generics.

Weakening

Weakening or shifting of de Bruijn indices is a central part of the evaluation. After performing β-reduction, any free variables need to be decreased to account for removal of the λ-abstraction.

The basic weakening function is weakBy', which takes:

  • An natural number, denoting the amount to shift free variables.

  • A cutoff value, for which all variables less than or equal are bound, and all variables greater than that are free. Typically this value will be 0, to denote that we want to account for removal of the outermost abstraction.

  • A term a to perform weakening / shifting on.

weakBy' will return a term a again, on which the weakening has been executed. The generic function gweakBy' is similar, but takes an f t as term and returns an f t. It is used for automatic deriving of instances using GHC.Generics.