idris-1.3.0: Functional Programming Language with Dependent Types

LicenseBSD3
MaintainerThe Idris Community.
Safe HaskellNone
LanguageHaskell2010

Idris.Inliner

Description

 

Synopsis

Documentation

inlineDef :: IState -> [([Name], Term, Term)] -> [([Name], Term, Term)] Source #

inlineTerm :: IState -> Term -> Term Source #

Inlining is either top level (i.e. not in a function arg) or argument level

For each application in a term: * Check if the function is inlinable (Dictionaries are inlinable in an argument, not otherwise) - If so, try inlining without reducing its arguments + If successful, then continue on the result (top level) + If not, reduce the arguments (argument level) and try again - If not, inline all the arguments (top level)