Safe Haskell	None
Language	Haskell2010

Agda.Compiler.ToTreeless

Contents

Default pipeline

Synopsis

toTreelessWith :: CCConfig -> QName -> TCM (Maybe TTerm)
closedTermToTreeless :: CCConfig -> Term -> TCM TTerm
data Pipeline
- = FixedPoint Int Pipeline
- | Sequential [Pipeline]
- | SinglePass CompilerPass
data CompilerPass = CompilerPass {
- passTag :: String
- passVerbosity :: Int
- passName :: String
- passCode :: EvaluationStrategy -> TTerm -> TCM TTerm
}
compilerPass :: String -> Int -> String -> (EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline
type CCConfig = (EvaluationStrategy, CCSubst, BuildPipeline)
data CCSubst
- = EraseUnused
- | IgnoreUnused
compilerPipeline :: BuildPipeline
mkDefaultCCConfig :: EvaluationStrategy -> CCConfig
toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe TTerm)

Documentation

toTreelessWith :: CCConfig -> QName -> TCM (Maybe TTerm) Source #

Converts compiled clauses to treeless syntax.

Note: Do not use any of the concrete names in the returned term for identification purposes! If you wish to do so, first apply the Agda.Compiler.Treeless.NormalizeNames transformation.

closedTermToTreeless :: CCConfig -> Term -> TCM TTerm Source #

data Pipeline Source #

Constructors

FixedPoint Int Pipeline
Sequential [Pipeline]
SinglePass CompilerPass

data CompilerPass Source #

Constructors

CompilerPass
Fields passTag :: String passVerbosity :: Int passName :: String passCode :: EvaluationStrategy -> TTerm -> TCM TTerm

compilerPass :: String -> Int -> String -> (EvaluationStrategy -> TTerm -> TCM TTerm) -> Pipeline Source #

type CCConfig = (EvaluationStrategy, CCSubst, BuildPipeline) Source #

data CCSubst Source #

Constructors

EraseUnused
IgnoreUnused

Instances

Instances details

Eq CCSubst Source #
Instance details Defined in Agda.Compiler.ToTreeless Methods (==) :: CCSubst -> CCSubst -> Bool # (/=) :: CCSubst -> CCSubst -> Bool #

Default pipeline

compilerPipeline :: BuildPipeline Source #

Default compiler pipeline

Backends may use different pipelines

mkDefaultCCConfig :: EvaluationStrategy -> CCConfig Source #

Create default CCConfig using default pipeline

toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe TTerm) Source #

Convert to treeless using default pipeline