ModuleAgda-2.8.0.2Haskell2010

Agda.Compiler.ToTreeless

Synopsis

value toTreeless
value toTreelessWith
value closedTermToTreeless
data Pipeline
data CompilerPass
value compilerPass
value compilerPipeline
type CCConfig
data CCSubst

PackageAgda-2.8.0.2
Exports9
LanguageHaskell2010
LicenceMIT
SourceToTreeless.hs

valuetoTreeless :: EvaluationStrategy -> QName -> TCM (Maybe TTerm)

valuetoTreelessWith :: BuildPipeline -> CCConfig -> QName -> TCM (Maybe TTerm)

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.

valueclosedTermToTreeless :: CCConfig -> Term -> TCM TTerm

datadata Pipeline

datadata CompilerPass

Constructors

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

valuecompilerPass

:: String
-> Int
-> String
-> EvaluationStrategy -> TTerm -> TCM TTerm
-> Pipeline

valuecompilerPipeline :: BuildPipeline

typetype CCConfig = (EvaluationStrategy, CCSubst)

datadata CCSubst

EraseUnused IgnoreUnused

Instances1Eq

Eq CCSubstDefined in Agda-2.8.0.2 · Agda.Compiler.ToTreeless