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

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Treeless

Description

The treeless syntax is intended to be used as input for the compiler backends. It is more low-level than Internal syntax and is not used for type checking.

Some of the features of treeless syntax are: - case expressions instead of case trees - no instantiated datatypes / constructors

Synopsis

- module Agda.Syntax.Abstract.Name
- class Unreachable a where
  - isUnreachable :: a -> Bool
- data TError = TUnreachable
- data TAlt
  - = TACon {
    - aCon :: QName
    - aArity :: Int
    - aBody :: TTerm
    }
  - | TAGuard {
    - aGuard :: TTerm
    - aBody :: TTerm
    }
  - | TALit {
    - aLit :: Literal
    - aBody :: TTerm
    }
- data CaseInfo = CaseInfo {
  - caseLazy :: Bool
  - caseType :: CaseType
  }
- data CaseType
  - = CTData QName
  - | CTNat
  - | CTInt
  - | CTChar
  - | CTString
  - | CTFloat
  - | CTQName
- data TPrim
  - = PAdd
  - | PAdd64
  - | PSub
  - | PSub64
  - | PMul
  - | PMul64
  - | PQuot
  - | PQuot64
  - | PRem
  - | PRem64
  - | PGeq
  - | PLt
  - | PLt64
  - | PEqI
  - | PEq64
  - | PEqF
  - | PEqS
  - | PEqC
  - | PEqQ
  - | PIf
  - | PSeq
  - | PITo64
  - | P64ToI
- data TTerm
  - = TVar Int
  - | TPrim TPrim
  - | TDef QName
  - | TApp TTerm Args
  - | TLam TTerm
  - | TLit Literal
  - | TCon QName
  - | TLet TTerm TTerm
  - | TCase Int CaseInfo TTerm [TAlt]
  - | TUnit
  - | TSort
  - | TErased
  - | TCoerce TTerm
  - | TError TError
- type Args = [TTerm]
- data EvaluationStrategy
  - = LazyEvaluation
  - | EagerEvaluation
- data Compiled = Compiled {
  - cTreeless :: TTerm
  - cArgUsage :: [Bool]
  }
- pattern TPFn :: TPrim -> TTerm -> TTerm
- pattern TPOp :: TPrim -> TTerm -> TTerm -> TTerm
- isPrimEq :: TPrim -> Bool
- mkTApp :: TTerm -> Args -> TTerm
- tAppView :: TTerm -> [TTerm]
- tLetView :: TTerm -> ([TTerm], TTerm)
- tLamView :: TTerm -> (Int, TTerm)
- mkTLam :: Int -> TTerm -> TTerm
- mkLet :: TTerm -> TTerm -> TTerm
- tInt :: Integer -> TTerm
- intView :: TTerm -> Maybe Integer
- word64View :: TTerm -> Maybe Word64
- tPlusK :: Integer -> TTerm -> TTerm
- tNegPlusK :: Integer -> TTerm -> TTerm
- plusKView :: TTerm -> Maybe (Integer, TTerm)
- negPlusKView :: TTerm -> Maybe (Integer, TTerm)
- tOp :: TPrim -> TTerm -> TTerm -> TTerm
- tUnreachable :: TTerm
- tIfThenElse :: TTerm -> TTerm -> TTerm -> TTerm

# Documentation

module Agda.Syntax.Abstract.Name

class Unreachable a where Source #

Methods

isUnreachable :: a -> Bool Source #

Checks if the given expression is unreachable or not.

Instances

Unreachable TAlt Source # |
Instance details Defined in Agda.Syntax.Treeless Methods isUnreachable :: TAlt -> Bool Source #
Unreachable TTerm Source # |
Instance details Defined in Agda.Syntax.Treeless Methods isUnreachable :: TTerm -> Bool Source #

data TError Source #

Constructors

TUnreachable | Code which is unreachable. E.g. absurd branches or missing case defaults. Runtime behaviour of unreachable code is undefined, but preferably the program will exit with an error message. The compiler is free to assume that this code is unreachable and to remove it.

Instances

Eq TError Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: TError -> TError -> Bool Source # (/=) :: TError -> TError -> Bool Source #
Data TError Source # |

Instance details

Defined in Agda.Syntax.Treeless

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TError -> c TError Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TError Source #

toConstr :: TError -> Constr Source #

dataTypeOf :: TError -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TError) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TError) Source #

gmapT :: (forall b. Data b => b -> b) -> TError -> TError Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> TError -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TError -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TError -> m TError Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TError -> m TError Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TError -> m TError Source #

Ord TError Source # |
Instance details Defined in Agda.Syntax.Treeless Methods compare :: TError -> TError -> Ordering Source # (<) :: TError -> TError -> Bool Source # (<=) :: TError -> TError -> Bool Source # (>) :: TError -> TError -> Bool Source # (>=) :: TError -> TError -> Bool Source # max :: TError -> TError -> TError Source # min :: TError -> TError -> TError Source #
Show TError Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TError -> ShowS Source # show :: TError -> String Source # showList :: [TError] -> ShowS Source #

data TAlt Source #

Constructors

TACon | Matches on the given constructor. If the match succeeds, the pattern variables are prepended to the current environment (pushes all existing variables aArity steps further away)

Fields

- aCon :: QName
- aArity :: Int
- aBody :: TTerm

TAGuard | Binds no variables

Fields

- aGuard :: TTerm
- aBody :: TTerm

TALit |

Fields

- aLit :: Literal
- aBody :: TTerm

Instances

Eq TAlt Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: TAlt -> TAlt -> Bool Source # (/=) :: TAlt -> TAlt -> Bool Source #
Data TAlt Source # |

Instance details

Defined in Agda.Syntax.Treeless

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TAlt -> c TAlt Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TAlt Source #

toConstr :: TAlt -> Constr Source #

dataTypeOf :: TAlt -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TAlt) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TAlt) Source #

gmapT :: (forall b. Data b => b -> b) -> TAlt -> TAlt Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> TAlt -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TAlt -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TAlt -> m TAlt Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TAlt -> m TAlt Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TAlt -> m TAlt Source #

Ord TAlt Source # |
Instance details Defined in Agda.Syntax.Treeless Methods compare :: TAlt -> TAlt -> Ordering Source # (<) :: TAlt -> TAlt -> Bool Source # (<=) :: TAlt -> TAlt -> Bool Source # (>) :: TAlt -> TAlt -> Bool Source # (>=) :: TAlt -> TAlt -> Bool Source # max :: TAlt -> TAlt -> TAlt Source # min :: TAlt -> TAlt -> TAlt Source #
Show TAlt Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TAlt -> ShowS Source # show :: TAlt -> String Source # showList :: [TAlt] -> ShowS Source #
Unreachable TAlt Source # |
Instance details Defined in Agda.Syntax.Treeless Methods isUnreachable :: TAlt -> Bool Source #
HasFree TAlt Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods freeVars :: TAlt -> Map Int Occurs Source #
Subst TTerm TAlt Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods applySubst :: Substitution' TTerm -> TAlt -> TAlt Source #

data CaseInfo Source #

Constructors

CaseInfo |

Fields

- caseLazy :: Bool
- caseType :: CaseType

Instances

Eq CaseInfo Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: CaseInfo -> CaseInfo -> Bool Source # (/=) :: CaseInfo -> CaseInfo -> Bool Source #
Data CaseInfo Source # |

Instance details

Defined in Agda.Syntax.Treeless

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CaseInfo -> c CaseInfo Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CaseInfo Source #

toConstr :: CaseInfo -> Constr Source #

dataTypeOf :: CaseInfo -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CaseInfo) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseInfo) Source #

gmapT :: (forall b. Data b => b -> b) -> CaseInfo -> CaseInfo Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CaseInfo -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CaseInfo -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> CaseInfo -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> CaseInfo -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo Source #

Ord CaseInfo Source # |
Instance details Defined in Agda.Syntax.Treeless Methods compare :: CaseInfo -> CaseInfo -> Ordering Source # (<) :: CaseInfo -> CaseInfo -> Bool Source # (<=) :: CaseInfo -> CaseInfo -> Bool Source # (>) :: CaseInfo -> CaseInfo -> Bool Source # (>=) :: CaseInfo -> CaseInfo -> Bool Source # max :: CaseInfo -> CaseInfo -> CaseInfo Source # min :: CaseInfo -> CaseInfo -> CaseInfo Source #
Show CaseInfo Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> CaseInfo -> ShowS Source # show :: CaseInfo -> String Source # showList :: [CaseInfo] -> ShowS Source #

data CaseType Source #

Constructors

CTData QName |
CTNat |
CTInt |
CTChar |
CTString |
CTFloat |
CTQName |

Instances

Eq CaseType Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: CaseType -> CaseType -> Bool Source # (/=) :: CaseType -> CaseType -> Bool Source #
Data CaseType Source # |

Instance details

Defined in Agda.Syntax.Treeless

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CaseType -> c CaseType Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CaseType Source #

toConstr :: CaseType -> Constr Source #

dataTypeOf :: CaseType -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CaseType) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseType) Source #

gmapT :: (forall b. Data b => b -> b) -> CaseType -> CaseType Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CaseType -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CaseType -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> CaseType -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> CaseType -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CaseType -> m CaseType Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CaseType -> m CaseType Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CaseType -> m CaseType Source #

Ord CaseType Source # |
Instance details Defined in Agda.Syntax.Treeless Methods compare :: CaseType -> CaseType -> Ordering Source # (<) :: CaseType -> CaseType -> Bool Source # (<=) :: CaseType -> CaseType -> Bool Source # (>) :: CaseType -> CaseType -> Bool Source # (>=) :: CaseType -> CaseType -> Bool Source # max :: CaseType -> CaseType -> CaseType Source # min :: CaseType -> CaseType -> CaseType Source #
Show CaseType Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> CaseType -> ShowS Source # show :: CaseType -> String Source # showList :: [CaseType] -> ShowS Source #

data TPrim Source #

Compiler-related primitives. This are NOT the same thing as primitives in Agda's surface or internal syntax! Some of the primitives have a suffix indicating which type of arguments they take, using the following naming convention: Char | Type C | Character F | Float I | Integer Q | QName S | String

Constructors

PAdd |
PAdd64 |
PSub |
PSub64 |
PMul |
PMul64 |
PQuot |
PQuot64 |
PRem |
PRem64 |
PGeq |
PLt |
PLt64 |
PEqI |
PEq64 |
PEqF |
PEqS |
PEqC |
PEqQ |
PIf |
PSeq |
PITo64 |
P64ToI |

Instances

Eq TPrim Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: TPrim -> TPrim -> Bool Source # (/=) :: TPrim -> TPrim -> Bool Source #
Data TPrim Source # |

Instance details

Defined in Agda.Syntax.Treeless

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TPrim -> c TPrim Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TPrim Source #

toConstr :: TPrim -> Constr Source #

dataTypeOf :: TPrim -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TPrim) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TPrim) Source #

gmapT :: (forall b. Data b => b -> b) -> TPrim -> TPrim Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> TPrim -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TPrim -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TPrim -> m TPrim Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TPrim -> m TPrim Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TPrim -> m TPrim Source #

Ord TPrim Source # |
Instance details Defined in Agda.Syntax.Treeless Methods compare :: TPrim -> TPrim -> Ordering Source # (<) :: TPrim -> TPrim -> Bool Source # (<=) :: TPrim -> TPrim -> Bool Source # (>) :: TPrim -> TPrim -> Bool Source # (>=) :: TPrim -> TPrim -> Bool Source # max :: TPrim -> TPrim -> TPrim Source # min :: TPrim -> TPrim -> TPrim Source #
Show TPrim Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TPrim -> ShowS Source # show :: TPrim -> String Source # showList :: [TPrim] -> ShowS Source #

data TTerm Source #

Constructors

TVar Int |
TPrim TPrim |
TDef QName |
TApp TTerm Args |
TLam TTerm |
TLit Literal |
TCon QName |
TLet TTerm TTerm | introduces a new local binding. The bound term MUST only be evaluated if it is used inside the body. Sharing may happen, but is optional. It is also perfectly valid to just inline the bound term in the body.
TCase Int CaseInfo TTerm [TAlt] | Case scrutinee (always variable), case type, default value, alternatives First, all TACon alternatives are tried; then all TAGuard alternatives in top to bottom order. TACon alternatives must not overlap.
TUnit |
TSort |
TErased |
TCoerce TTerm | Used by the GHC backend
TError TError | A runtime error, something bad has happened.

Instances

Eq TTerm Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: TTerm -> TTerm -> Bool Source # (/=) :: TTerm -> TTerm -> Bool Source #
Data TTerm Source # |

Instance details

Defined in Agda.Syntax.Treeless

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TTerm -> c TTerm Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TTerm Source #

toConstr :: TTerm -> Constr Source #

dataTypeOf :: TTerm -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TTerm) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TTerm) Source #

gmapT :: (forall b. Data b => b -> b) -> TTerm -> TTerm Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> TTerm -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> TTerm -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> TTerm -> m TTerm Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TTerm -> m TTerm Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TTerm -> m TTerm Source #

Ord TTerm Source # |
Instance details Defined in Agda.Syntax.Treeless Methods compare :: TTerm -> TTerm -> Ordering Source # (<) :: TTerm -> TTerm -> Bool Source # (<=) :: TTerm -> TTerm -> Bool Source # (>) :: TTerm -> TTerm -> Bool Source # (>=) :: TTerm -> TTerm -> Bool Source # max :: TTerm -> TTerm -> TTerm Source # min :: TTerm -> TTerm -> TTerm Source #
Show TTerm Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TTerm -> ShowS Source # show :: TTerm -> String Source # showList :: [TTerm] -> ShowS Source #
Pretty TTerm Source # |
Instance details Defined in Agda.Compiler.Treeless.Pretty Methods pretty :: TTerm -> Doc Source # prettyPrec :: Int -> TTerm -> Doc Source # prettyList :: [TTerm] -> Doc Source #
Unreachable TTerm Source # |
Instance details Defined in Agda.Syntax.Treeless Methods isUnreachable :: TTerm -> Bool Source #
DeBruijn TTerm Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods deBruijnVar :: Int -> TTerm Source # debruijnNamedVar :: String -> Int -> TTerm Source # deBruijnView :: TTerm -> Maybe Int Source #
HasFree TTerm Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods freeVars :: TTerm -> Map Int Occurs Source #
Subst TTerm TAlt Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods applySubst :: Substitution' TTerm -> TAlt -> TAlt Source #
Subst TTerm TTerm Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods applySubst :: Substitution' TTerm -> TTerm -> TTerm Source #

type Args = [TTerm] Source #

data EvaluationStrategy Source #

The treeless compiler can behave differently depending on the target language evaluation strategy. For instance, more aggressive erasure for lazy targets.

Constructors

LazyEvaluation |
EagerEvaluation |

Instances

Eq EvaluationStrategy Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: EvaluationStrategy -> EvaluationStrategy -> Bool Source # (/=) :: EvaluationStrategy -> EvaluationStrategy -> Bool Source #
Show EvaluationStrategy Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> EvaluationStrategy -> ShowS Source # show :: EvaluationStrategy -> String Source # showList :: [EvaluationStrategy] -> ShowS Source #

data Compiled Source #

Constructors

Compiled |

Fields

- cTreeless :: TTerm
- cArgUsage :: [Bool]

Instances

Eq Compiled Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: Compiled -> Compiled -> Bool Source # (/=) :: Compiled -> Compiled -> Bool Source #
Data Compiled Source # |

Instance details

Defined in Agda.Syntax.Treeless

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Compiled -> c Compiled Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Compiled Source #

toConstr :: Compiled -> Constr Source #

dataTypeOf :: Compiled -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Compiled) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Compiled) Source #

gmapT :: (forall b. Data b => b -> b) -> Compiled -> Compiled Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Compiled -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Compiled -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Compiled -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Compiled -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Compiled -> m Compiled Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Compiled -> m Compiled Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Compiled -> m Compiled Source #

Ord Compiled Source # |
Instance details Defined in Agda.Syntax.Treeless Methods compare :: Compiled -> Compiled -> Ordering Source # (<) :: Compiled -> Compiled -> Bool Source # (<=) :: Compiled -> Compiled -> Bool Source # (>) :: Compiled -> Compiled -> Bool Source # (>=) :: Compiled -> Compiled -> Bool Source # max :: Compiled -> Compiled -> Compiled Source # min :: Compiled -> Compiled -> Compiled Source #
Show Compiled Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> Compiled -> ShowS Source # show :: Compiled -> String Source # showList :: [Compiled] -> ShowS Source #
KillRange Compiled Source # |
Instance details Defined in Agda.Syntax.Treeless Methods killRange :: KillRangeT Compiled Source #

pattern TPFn :: TPrim -> TTerm -> TTerm Source #

pattern TPOp :: TPrim -> TTerm -> TTerm -> TTerm Source #

isPrimEq :: TPrim -> Bool Source #

mkTApp :: TTerm -> Args -> TTerm Source #

tAppView :: TTerm -> [TTerm] Source #

tLetView :: TTerm -> ([TTerm], TTerm) Source #

tLamView :: TTerm -> (Int, TTerm) Source #

mkTLam :: Int -> TTerm -> TTerm Source #

mkLet :: TTerm -> TTerm -> TTerm Source #

Introduces a new binding

tInt :: Integer -> TTerm Source #

intView :: TTerm -> Maybe Integer Source #

word64View :: TTerm -> Maybe Word64 Source #

tPlusK :: Integer -> TTerm -> TTerm Source #

tNegPlusK :: Integer -> TTerm -> TTerm Source #

plusKView :: TTerm -> Maybe (Integer, TTerm) Source #

negPlusKView :: TTerm -> Maybe (Integer, TTerm) Source #

tOp :: TPrim -> TTerm -> TTerm -> TTerm Source #

tUnreachable :: TTerm Source #

tIfThenElse :: TTerm -> TTerm -> TTerm -> TTerm Source #