Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Compiler.ToTreeless

Synopsis

toTreeless :: EvaluationStrategy -> QName -> TCM (Maybe TTerm)
toTreelessWith :: BuildPipeline -> 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

Documentation

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

toTreelessWith :: BuildPipeline -> 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 #