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

Safe HaskellNone
LanguageHaskell2010

FreeC.IR.Inlining

Description

This module contains functions for inlining the definition of functions into expressions or other function declarations.

Inlining is performed during the translation of recursive function declarations to inline the definition of the non-recursive main function into the recursive helper functions.

Synopsis

Documentation

inlineFuncDecls :: [FuncDecl] -> FuncDecl -> Converter FuncDecl Source #

Inlines the right-hand sides of the given function declarations into the right-hand sides of another function declaration.

inlineExpr :: [FuncDecl] -> Expr -> Converter Expr Source #

Inlines the right-hand sides of the given function declarations into an expression.

Inlining is repeated until the expression remains unchanged or no more function declarations are available. That is done under the assumption that regarding a certain position of the given expression every given function should be inlined at most once in order to avoid endless inlining.