Safe Haskell	None
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
compilerPipeline :: BuildPipeline
type CCConfig = (EvaluationStrategy, CCSubst)
data CCSubst
- = EraseUnused
- | IgnoreUnused

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 #

compilerPipeline :: BuildPipeline Source #

type CCConfig = (EvaluationStrategy, CCSubst) 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 #