free-compiler-0.3.0.0: A Haskell to Coq compiler.

Safe HaskellNone
LanguageHaskell2010

FreeC.Pass.LetSortPass

Contents

Description

This module contains a compiler pass that brings the bindings of all let-expressions in a module into reverse topological order.

Examples

Example 1

The bindings of the following let-expression are not topologically sorted because the right-hand side of x depends on y but y is defined after x.

let { x = y; y = 42 } in x

This pass transforms the let-expression above into the following form.

let { y = 42; x = y } in x

Example 2

If a let-expression contains (mutually) recursive bindings, a fatal error is reported.

let { x = y; y = x } in x

It is not clear at the moment how mutually recursive local variables can be represented when the sharing effect is used.

Specification

Preconditions

There are no special requirements.

Translations

Every let-expression

let { x₁ = e₁; …; xₙ = eₙ } in e

is transformed into a let-expression

let { y₁ = f₁; …; yₙ = fₙ } in e

where y₁ = f₁, …, yₙ = fₙ is a permutation of x₁ = e₁, …, xₙ = eₙ such that for every 1 ≤ i ≤ n the expression fᵢ contains no free variables xⱼ with j ≥ i, i.e., all variables bound by the new let-expression are not used before they are declared. If there is no such permutation a fatal error is reported.

Postcondition

The bindings of all let-expressions are in reverse topological order and there are no recursive or mutually recursive bindings.

Synopsis

Documentation

letSortPass :: Pass Module Module Source #

A pass that sorts the bindings of let-expressions topologically.

Testing Interface

sortLetExprs :: MonadReporter r => Expr -> r Expr Source #

Sorts all let-expressions in the given expression topologically.