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

Minimal complete definition

isUnreachable

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 # (/=) :: TError -> TError -> Bool #
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 # 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 Source #
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 Source #
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TError -> ShowS # show :: TError -> String # showList :: [TError] -> ShowS #

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 # (/=) :: TAlt -> TAlt -> Bool #
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 # 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 Source #
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 Source #
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TAlt -> ShowS # show :: TAlt -> String # showList :: [TAlt] -> ShowS #
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 # (/=) :: CaseInfo -> CaseInfo -> Bool #
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 # 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 Source #
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 Source #
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> CaseInfo -> ShowS # show :: CaseInfo -> String # showList :: [CaseInfo] -> ShowS #

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 # (/=) :: CaseType -> CaseType -> Bool #
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 # 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 Source #
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 Source #
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> CaseType -> ShowS # show :: CaseType -> String # showList :: [CaseType] -> ShowS #

data TPrim Source #

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 # (/=) :: TPrim -> TPrim -> Bool #
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 # 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 Source #
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 Source #
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TPrim -> ShowS # show :: TPrim -> String # showList :: [TPrim] -> ShowS #

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 # (/=) :: TTerm -> TTerm -> Bool #
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 # 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 Source #
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 Source #
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TTerm -> ShowS # show :: TTerm -> String # showList :: [TTerm] -> ShowS #
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 Compiled Source #

Constructors

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

Instances

Eq Compiled Source #
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: Compiled -> Compiled -> Bool # (/=) :: Compiled -> Compiled -> Bool #
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 # 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 Source #
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 Source #
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> Compiled -> ShowS # show :: Compiled -> String # showList :: [Compiled] -> ShowS #
KillRange Compiled Source #
Instance details Defined in Agda.Syntax.Treeless Methods killRange :: KillRangeT Compiled Source #