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

Safe HaskellNone
LanguageHaskell2010

FreeC.Pass.EffectAnalysisPass

Description

This module contains a compiler pass that updates the effect information of function declaration environment entries.

Example

Example 1

The FreeC.Pass.DefineDeclPass would add a environment entry whose entryEffects list is empty for the following function declaration.

head :: [a] -> a
head xs = case xs of
  []      -> undefined
  x : xs' -> x

This pass recognizes that the right-hand side of the function declaration for head refers to the built-in function undefined. Since undefined is partial, head is also partial. Thus, the environment entry of head is updated such that entryEffects contains Partiality.

Example 2

Sharing is also modeled as an effect by the compiler. In contrast to other effects that are introduced by function declarations, the sharing effect is required by a function if it contains let-expressions.

double :: (Int -> Int) -> Int -> Int
double f x = let x' = f x in x' + x'

Since the right-hand side contains a let-expression the pass updates the environment entry of double such that Sharing is part of entryEffects.

Specification

Preconditions

The environment contains entries for all function declarations with no effects in entryEffects.

Translation

No modifications are made to the AST.

If a function declaration's right-hand side contains a reference to a function whose entry contains effects, it gets those effects as well.

If there are mutually recursive function declaration's and one of them gets effects by the rule above, then all need to get those effects.

Postconditions

All occurring effects of functions are added to entryEffects of the corresponding environment entries.

Synopsis

Documentation

effectAnalysisPass :: DependencyAwarePass FuncDecl Source #

A compiler pass that updates the effect information of function declaration environment entries.