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
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 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 #

Minimal complete definition

isUnreachable

Methods

isUnreachable :: a -> Bool #

Checks if the given expression is unreachable or not.

Instances

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

data TError #

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 #
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: TError -> TError -> Bool # (/=) :: TError -> TError -> Bool #
Data TError #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TError # toConstr :: TError -> Constr # dataTypeOf :: TError -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TError) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TError) # gmapT :: (forall b. Data b => b -> b) -> TError -> TError # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TError -> r # gmapQ :: (forall d. Data d => d -> u) -> TError -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TError -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TError -> m TError # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TError -> m TError # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TError -> m TError #
Ord TError #
Instance details Defined in Agda.Syntax.Treeless Methods compare :: TError -> TError -> Ordering # (<) :: TError -> TError -> Bool # (<=) :: TError -> TError -> Bool # (>) :: TError -> TError -> Bool # (>=) :: TError -> TError -> Bool # max :: TError -> TError -> TError # min :: TError -> TError -> TError #
Show TError #
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TError -> ShowS # show :: TError -> String # showList :: [TError] -> ShowS #

data TAlt #

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 #
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: TAlt -> TAlt -> Bool # (/=) :: TAlt -> TAlt -> Bool #
Data TAlt #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TAlt # toConstr :: TAlt -> Constr # dataTypeOf :: TAlt -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TAlt) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TAlt) # gmapT :: (forall b. Data b => b -> b) -> TAlt -> TAlt # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TAlt -> r # gmapQ :: (forall d. Data d => d -> u) -> TAlt -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TAlt -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TAlt -> m TAlt # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TAlt -> m TAlt # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TAlt -> m TAlt #
Ord TAlt #
Instance details Defined in Agda.Syntax.Treeless Methods compare :: TAlt -> TAlt -> Ordering # (<) :: TAlt -> TAlt -> Bool # (<=) :: TAlt -> TAlt -> Bool # (>) :: TAlt -> TAlt -> Bool # (>=) :: TAlt -> TAlt -> Bool # max :: TAlt -> TAlt -> TAlt # min :: TAlt -> TAlt -> TAlt #
Show TAlt #
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TAlt -> ShowS # show :: TAlt -> String # showList :: [TAlt] -> ShowS #
Unreachable TAlt #
Instance details Defined in Agda.Syntax.Treeless Methods isUnreachable :: TAlt -> Bool #
HasFree TAlt #
Instance details Defined in Agda.Compiler.Treeless.Subst Methods freeVars :: TAlt -> Map Int Occurs #
Subst TTerm TAlt #
Instance details Defined in Agda.Compiler.Treeless.Subst Methods applySubst :: Substitution' TTerm -> TAlt -> TAlt #

data CaseInfo #

Constructors

CaseInfo
Fields caseLazy :: Bool caseType :: CaseType

Instances

Eq CaseInfo #
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: CaseInfo -> CaseInfo -> Bool # (/=) :: CaseInfo -> CaseInfo -> Bool #
Data CaseInfo #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CaseInfo # toConstr :: CaseInfo -> Constr # dataTypeOf :: CaseInfo -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CaseInfo) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseInfo) # gmapT :: (forall b. Data b => b -> b) -> CaseInfo -> CaseInfo # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CaseInfo -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CaseInfo -> r # gmapQ :: (forall d. Data d => d -> u) -> CaseInfo -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> CaseInfo -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CaseInfo -> m CaseInfo #
Ord CaseInfo #
Instance details Defined in Agda.Syntax.Treeless Methods compare :: CaseInfo -> CaseInfo -> Ordering # (<) :: CaseInfo -> CaseInfo -> Bool # (<=) :: CaseInfo -> CaseInfo -> Bool # (>) :: CaseInfo -> CaseInfo -> Bool # (>=) :: CaseInfo -> CaseInfo -> Bool # max :: CaseInfo -> CaseInfo -> CaseInfo # min :: CaseInfo -> CaseInfo -> CaseInfo #
Show CaseInfo #
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> CaseInfo -> ShowS # show :: CaseInfo -> String # showList :: [CaseInfo] -> ShowS #

data CaseType #

Constructors

CTData QName
CTNat
CTInt
CTChar
CTString
CTFloat
CTQName

Instances

Eq CaseType #
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: CaseType -> CaseType -> Bool # (/=) :: CaseType -> CaseType -> Bool #
Data CaseType #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c CaseType # toConstr :: CaseType -> Constr # dataTypeOf :: CaseType -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c CaseType) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CaseType) # gmapT :: (forall b. Data b => b -> b) -> CaseType -> CaseType # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CaseType -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CaseType -> r # gmapQ :: (forall d. Data d => d -> u) -> CaseType -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> CaseType -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> CaseType -> m CaseType # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CaseType -> m CaseType # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CaseType -> m CaseType #
Ord CaseType #
Instance details Defined in Agda.Syntax.Treeless Methods compare :: CaseType -> CaseType -> Ordering # (<) :: CaseType -> CaseType -> Bool # (<=) :: CaseType -> CaseType -> Bool # (>) :: CaseType -> CaseType -> Bool # (>=) :: CaseType -> CaseType -> Bool # max :: CaseType -> CaseType -> CaseType # min :: CaseType -> CaseType -> CaseType #
Show CaseType #
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> CaseType -> ShowS # show :: CaseType -> String # showList :: [CaseType] -> ShowS #

data TPrim #

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 #
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: TPrim -> TPrim -> Bool # (/=) :: TPrim -> TPrim -> Bool #
Data TPrim #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TPrim # toConstr :: TPrim -> Constr # dataTypeOf :: TPrim -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TPrim) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TPrim) # gmapT :: (forall b. Data b => b -> b) -> TPrim -> TPrim # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TPrim -> r # gmapQ :: (forall d. Data d => d -> u) -> TPrim -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TPrim -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TPrim -> m TPrim # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TPrim -> m TPrim # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TPrim -> m TPrim #
Ord TPrim #
Instance details Defined in Agda.Syntax.Treeless Methods compare :: TPrim -> TPrim -> Ordering # (<) :: TPrim -> TPrim -> Bool # (<=) :: TPrim -> TPrim -> Bool # (>) :: TPrim -> TPrim -> Bool # (>=) :: TPrim -> TPrim -> Bool # max :: TPrim -> TPrim -> TPrim # min :: TPrim -> TPrim -> TPrim #
Show TPrim #
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TPrim -> ShowS # show :: TPrim -> String # showList :: [TPrim] -> ShowS #

data TTerm #

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 #
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: TTerm -> TTerm -> Bool # (/=) :: TTerm -> TTerm -> Bool #
Data TTerm #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c TTerm # toConstr :: TTerm -> Constr # dataTypeOf :: TTerm -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c TTerm) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c TTerm) # gmapT :: (forall b. Data b => b -> b) -> TTerm -> TTerm # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TTerm -> r # gmapQ :: (forall d. Data d => d -> u) -> TTerm -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TTerm -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TTerm -> m TTerm # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TTerm -> m TTerm # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TTerm -> m TTerm #
Ord TTerm #
Instance details Defined in Agda.Syntax.Treeless Methods compare :: TTerm -> TTerm -> Ordering # (<) :: TTerm -> TTerm -> Bool # (<=) :: TTerm -> TTerm -> Bool # (>) :: TTerm -> TTerm -> Bool # (>=) :: TTerm -> TTerm -> Bool # max :: TTerm -> TTerm -> TTerm # min :: TTerm -> TTerm -> TTerm #
Show TTerm #
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TTerm -> ShowS # show :: TTerm -> String # showList :: [TTerm] -> ShowS #
Pretty TTerm #
Instance details Defined in Agda.Compiler.Treeless.Pretty Methods pretty :: TTerm -> Doc # prettyPrec :: Int -> TTerm -> Doc # prettyList :: [TTerm] -> Doc #
Unreachable TTerm #
Instance details Defined in Agda.Syntax.Treeless Methods isUnreachable :: TTerm -> Bool #
DeBruijn TTerm #
Instance details Defined in Agda.Compiler.Treeless.Subst Methods deBruijnVar :: Int -> TTerm # debruijnNamedVar :: String -> Int -> TTerm # deBruijnView :: TTerm -> Maybe Int #
HasFree TTerm #
Instance details Defined in Agda.Compiler.Treeless.Subst Methods freeVars :: TTerm -> Map Int Occurs #
Subst TTerm TAlt #
Instance details Defined in Agda.Compiler.Treeless.Subst Methods applySubst :: Substitution' TTerm -> TAlt -> TAlt #
Subst TTerm TTerm #
Instance details Defined in Agda.Compiler.Treeless.Subst Methods applySubst :: Substitution' TTerm -> TTerm -> TTerm #

type Args = [TTerm] #

data Compiled #

Constructors

Compiled
Fields cTreeless :: TTerm cArgUsage :: [Bool]

Instances

Eq Compiled #
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: Compiled -> Compiled -> Bool # (/=) :: Compiled -> Compiled -> Bool #
Data Compiled #
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 # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Compiled # toConstr :: Compiled -> Constr # dataTypeOf :: Compiled -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Compiled) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Compiled) # gmapT :: (forall b. Data b => b -> b) -> Compiled -> Compiled # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Compiled -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Compiled -> r # gmapQ :: (forall d. Data d => d -> u) -> Compiled -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Compiled -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Compiled -> m Compiled # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Compiled -> m Compiled # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Compiled -> m Compiled #
Ord Compiled #
Instance details Defined in Agda.Syntax.Treeless Methods compare :: Compiled -> Compiled -> Ordering # (<) :: Compiled -> Compiled -> Bool # (<=) :: Compiled -> Compiled -> Bool # (>) :: Compiled -> Compiled -> Bool # (>=) :: Compiled -> Compiled -> Bool # max :: Compiled -> Compiled -> Compiled # min :: Compiled -> Compiled -> Compiled #
Show Compiled #
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> Compiled -> ShowS # show :: Compiled -> String # showList :: [Compiled] -> ShowS #
KillRange Compiled #
Instance details Defined in Agda.Syntax.Treeless Methods killRange :: KillRangeT Compiled #