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
- | TMeta String
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 Quantity 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 ArgUsage
- = ArgUsed
- | ArgUnused
data Compiled = Compiled {
- cTreeless :: TTerm
- cArgUsage :: Maybe [ArgUsage]
}
pattern TPFn :: TPrim -> TTerm -> TTerm
pattern TPOp :: TPrim -> TTerm -> TTerm -> TTerm
isPrimEq :: TPrim -> Bool
coerceView :: TTerm -> (Bool, TTerm)
mkTApp :: TTerm -> Args -> TTerm
tAppView :: TTerm -> (TTerm, [TTerm])
coerceAppView :: TTerm -> ((Bool, 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
filterUsed :: [ArgUsage] -> [a] -> [a]

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

Instances details

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.
TMeta String	Code which could not be obtained because of a hole in the program. This should throw a runtime error. The string gives some information about the meta variable that got compiled.

Instances

Instances details

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 :: forall r r'. (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 #
Generic TError Source #
Instance details Defined in Agda.Syntax.Treeless Associated Types type Rep TError :: Type -> Type # Methods from :: TError -> Rep TError x # to :: Rep TError x -> TError #
NFData TError Source #
Instance details Defined in Agda.Syntax.Treeless Methods rnf :: TError -> () #
type Rep TError Source #
Instance details Defined in Agda.Syntax.Treeless type Rep TError = D1 ('MetaData "TError" "Agda.Syntax.Treeless" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" 'False) (C1 ('MetaCons "TUnreachable" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TMeta" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

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

Instances details

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 :: forall r r'. (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 #
Generic TAlt Source #
Instance details Defined in Agda.Syntax.Treeless Associated Types type Rep TAlt :: Type -> Type # Methods from :: TAlt -> Rep TAlt x # to :: Rep TAlt x -> TAlt #
NFData TAlt Source #
Instance details Defined in Agda.Syntax.Treeless Methods rnf :: TAlt -> () #
Unreachable TAlt Source #
Instance details Defined in Agda.Syntax.Treeless Methods isUnreachable :: TAlt -> Bool Source #
Subst TAlt Source #
Instance details Defined in Agda.Compiler.Treeless.Subst Associated Types type SubstArg TAlt Source # Methods applySubst :: Substitution' (SubstArg TAlt) -> TAlt -> TAlt Source #
HasFree TAlt Source #
Instance details Defined in Agda.Compiler.Treeless.Subst Methods freeVars :: TAlt -> Map Int Occurs Source #
type Rep TAlt Source #
Instance details Defined in Agda.Syntax.Treeless type Rep TAlt = D1 ('MetaData "TAlt" "Agda.Syntax.Treeless" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" 'False) (C1 ('MetaCons "TACon" 'PrefixI 'True) (S1 ('MetaSel ('Just "aCon") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :: (S1 ('MetaSel ('Just "aArity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: S1 ('MetaSel ('Just "aBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TTerm))) :+: (C1 ('MetaCons "TAGuard" 'PrefixI 'True) (S1 ('MetaSel ('Just "aGuard") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TTerm) :: S1 ('MetaSel ('Just "aBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TTerm)) :+: C1 ('MetaCons "TALit" 'PrefixI 'True) (S1 ('MetaSel ('Just "aLit") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal) :: S1 ('MetaSel ('Just "aBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TTerm))))
type SubstArg TAlt Source #
Instance details Defined in Agda.Compiler.Treeless.Subst type SubstArg TAlt = TTerm

data CaseInfo Source #

Constructors

CaseInfo
Fields caseLazy :: Bool caseType :: CaseType

Instances

Instances details

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 :: forall r r'. (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 #
Generic CaseInfo Source #
Instance details Defined in Agda.Syntax.Treeless Associated Types type Rep CaseInfo :: Type -> Type # Methods from :: CaseInfo -> Rep CaseInfo x # to :: Rep CaseInfo x -> CaseInfo #
NFData CaseInfo Source #
Instance details Defined in Agda.Syntax.Treeless Methods rnf :: CaseInfo -> () #
type Rep CaseInfo Source #
Instance details Defined in Agda.Syntax.Treeless type Rep CaseInfo = D1 ('MetaData "CaseInfo" "Agda.Syntax.Treeless" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" 'False) (C1 ('MetaCons "CaseInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "caseLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "caseType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CaseType)))

data CaseType Source #

Constructors

CTData Quantity QName
CTNat
CTInt
CTChar
CTString
CTFloat
CTQName

Instances

Instances details

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 :: forall r r'. (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 #
Generic CaseType Source #
Instance details Defined in Agda.Syntax.Treeless Associated Types type Rep CaseType :: Type -> Type # Methods from :: CaseType -> Rep CaseType x # to :: Rep CaseType x -> CaseType #
NFData CaseType Source #
Instance details Defined in Agda.Syntax.Treeless Methods rnf :: CaseType -> () #
type Rep CaseType Source #
Instance details Defined in Agda.Syntax.Treeless type Rep CaseType = D1 ('MetaData "CaseType" "Agda.Syntax.Treeless" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" 'False) ((C1 ('MetaCons "CTData" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Quantity) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)) :+: (C1 ('MetaCons "CTNat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CTInt" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "CTChar" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CTString" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CTFloat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CTQName" 'PrefixI 'False) (U1 :: Type -> Type))))

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

Instances details

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 :: forall r r'. (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 #
Generic TPrim Source #
Instance details Defined in Agda.Syntax.Treeless Associated Types type Rep TPrim :: Type -> Type # Methods from :: TPrim -> Rep TPrim x # to :: Rep TPrim x -> TPrim #
NFData TPrim Source #
Instance details Defined in Agda.Syntax.Treeless Methods rnf :: TPrim -> () #
type Rep TPrim Source #
Instance details Defined in Agda.Syntax.Treeless type Rep TPrim = D1 ('MetaData "TPrim" "Agda.Syntax.Treeless" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" 'False) ((((C1 ('MetaCons "PAdd" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PAdd64" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PSub" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PSub64" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PMul" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "PMul64" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PQuot" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PQuot64" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "PRem" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PRem64" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PGeq" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "PLt" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PLt64" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PEqI" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "PEq64" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PEqF" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PEqS" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "PEqC" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PEqQ" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PIf" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "PSeq" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PITo64" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "P64ToI" 'PrefixI 'False) (U1 :: Type -> Type))))))

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

Instances details

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 :: forall r r'. (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 #
Generic TTerm Source #
Instance details Defined in Agda.Syntax.Treeless Associated Types type Rep TTerm :: Type -> Type # Methods from :: TTerm -> Rep TTerm x # to :: Rep TTerm x -> TTerm #
NFData TTerm Source #
Instance details Defined in Agda.Syntax.Treeless Methods rnf :: TTerm -> () #
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 #
Subst TTerm Source #
Instance details Defined in Agda.Compiler.Treeless.Subst Associated Types type SubstArg TTerm Source # Methods applySubst :: Substitution' (SubstArg TTerm) -> TTerm -> TTerm Source #
HasFree TTerm Source #
Instance details Defined in Agda.Compiler.Treeless.Subst Methods freeVars :: TTerm -> Map Int Occurs Source #
type Rep TTerm Source #
Instance details Defined in Agda.Syntax.Treeless type Rep TTerm = D1 ('MetaData "TTerm" "Agda.Syntax.Treeless" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" 'False) (((C1 ('MetaCons "TVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: (C1 ('MetaCons "TPrim" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TPrim)) :+: C1 ('MetaCons "TDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName)))) :+: ((C1 ('MetaCons "TApp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TTerm) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Args)) :+: C1 ('MetaCons "TLam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TTerm))) :+: (C1 ('MetaCons "TLit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Literal)) :+: C1 ('MetaCons "TCon" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName))))) :+: ((C1 ('MetaCons "TLet" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TTerm) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TTerm)) :+: (C1 ('MetaCons "TCase" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CaseInfo)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TTerm) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [TAlt]))) :+: C1 ('MetaCons "TUnit" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TSort" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TErased" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TCoerce" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TTerm)) :+: C1 ('MetaCons "TError" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TError))))))
type SubstArg TTerm Source #
Instance details Defined in Agda.Compiler.Treeless.Subst type SubstArg TTerm = TTerm

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

Instances details

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

data ArgUsage Source #

Usage status of function arguments in treeless code.

Constructors

ArgUsed
ArgUnused

Instances

Instances details

Eq ArgUsage Source #
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: ArgUsage -> ArgUsage -> Bool # (/=) :: ArgUsage -> ArgUsage -> Bool #
Data ArgUsage 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) -> ArgUsage -> c ArgUsage # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ArgUsage # toConstr :: ArgUsage -> Constr # dataTypeOf :: ArgUsage -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ArgUsage) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ArgUsage) # gmapT :: (forall b. Data b => b -> b) -> ArgUsage -> ArgUsage # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ArgUsage -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ArgUsage -> r # gmapQ :: (forall d. Data d => d -> u) -> ArgUsage -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ArgUsage -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ArgUsage -> m ArgUsage # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgUsage -> m ArgUsage # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ArgUsage -> m ArgUsage #
Ord ArgUsage Source #
Instance details Defined in Agda.Syntax.Treeless Methods compare :: ArgUsage -> ArgUsage -> Ordering # (<) :: ArgUsage -> ArgUsage -> Bool # (<=) :: ArgUsage -> ArgUsage -> Bool # (>) :: ArgUsage -> ArgUsage -> Bool # (>=) :: ArgUsage -> ArgUsage -> Bool # max :: ArgUsage -> ArgUsage -> ArgUsage # min :: ArgUsage -> ArgUsage -> ArgUsage #
Show ArgUsage Source #
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> ArgUsage -> ShowS # show :: ArgUsage -> String # showList :: [ArgUsage] -> ShowS #
Generic ArgUsage Source #
Instance details Defined in Agda.Syntax.Treeless Associated Types type Rep ArgUsage :: Type -> Type # Methods from :: ArgUsage -> Rep ArgUsage x # to :: Rep ArgUsage x -> ArgUsage #
NFData ArgUsage Source #
Instance details Defined in Agda.Syntax.Treeless Methods rnf :: ArgUsage -> () #
type Rep ArgUsage Source #
Instance details Defined in Agda.Syntax.Treeless type Rep ArgUsage = D1 ('MetaData "ArgUsage" "Agda.Syntax.Treeless" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" 'False) (C1 ('MetaCons "ArgUsed" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ArgUnused" 'PrefixI 'False) (U1 :: Type -> Type))

data Compiled Source #

Constructors

Compiled
Fields cTreeless :: TTerm cArgUsage :: Maybe [ArgUsage] `Nothing` if treeless usage analysis has not run yet.

Instances

Instances details

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 :: forall r r'. (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 #
Generic Compiled Source #
Instance details Defined in Agda.Syntax.Treeless Associated Types type Rep Compiled :: Type -> Type # Methods from :: Compiled -> Rep Compiled x # to :: Rep Compiled x -> Compiled #
NFData Compiled Source #
Instance details Defined in Agda.Syntax.Treeless Methods rnf :: Compiled -> () #
KillRange Compiled Source #
Instance details Defined in Agda.Syntax.Treeless Methods killRange :: KillRangeT Compiled Source #
type Rep Compiled Source #
Instance details Defined in Agda.Syntax.Treeless type Rep Compiled = D1 ('MetaData "Compiled" "Agda.Syntax.Treeless" "Agda-2.6.2.2-DXbLWdCWC6QEApzM0094If" 'False) (C1 ('MetaCons "Compiled" 'PrefixI 'True) (S1 ('MetaSel ('Just "cTreeless") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TTerm) :*: S1 ('MetaSel ('Just "cArgUsage") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe [ArgUsage]))))

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

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

isPrimEq :: TPrim -> Bool Source #

coerceView :: TTerm -> (Bool, TTerm) Source #

Strip leading coercions and indicate whether there were some.

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

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

coerceAppView :: TTerm -> ((Bool, TTerm), [TTerm]) Source #

Expose the format coerce f args.

We fuse coercions, even if interleaving with applications. We assume that coercion is powerful enough to satisfy coerce (coerce f a) b = coerce f a b

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 #

filterUsed :: [ArgUsage] -> [a] -> [a] Source #

filterUsed used args drops those args which are labelled ArgUnused in list used.

Specification:

  filterUsed used args = [ a | (a, ArgUsed) <- zip args $ used ++ repeat ArgUsed ]

Examples:

  filterUsed []                 == id
  filterUsed (repeat ArgUsed)   == id
  filterUsed (repeat ArgUnused) == const []