Agda-2.8.0: A dependently typed functional programming language and proof assistant

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 Source # (/=) :: CCSubst -> CCSubst -> Bool Source #