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
- data CaseInfo = CaseInfo {}
- data CaseType
- data TPrim
- data TTerm
- type Args = [TTerm]
- data EvaluationStrategy
- data ArgUsage
- data Compiled = Compiled {}
- 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 #
Instances
Unreachable TAlt Source # | |
Defined in Agda.Syntax.Treeless Methods isUnreachable :: TAlt -> Bool Source # | |
Unreachable TTerm Source # | |
Defined in Agda.Syntax.Treeless Methods isUnreachable :: TTerm -> Bool 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
Eq TError Source # | |
Data TError Source # | |
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 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 # | |
Show TError Source # | |
Generic TError Source # | |
NFData TError Source # | |
Defined in Agda.Syntax.Treeless | |
type Rep TError Source # | |
Defined in Agda.Syntax.Treeless type Rep TError = D1 ('MetaData "TError" "Agda.Syntax.Treeless" "Agda-2.6.2.2-CCUZrXznmr9DtCyaOqbqEd" 'False) (C1 ('MetaCons "TUnreachable" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TMeta" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) |
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) |
TAGuard | Binds no variables |
TALit | |
Instances
Eq TAlt Source # | |
Data TAlt Source # | |
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 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 # | |
Show TAlt Source # | |
Generic TAlt Source # | |
NFData TAlt Source # | |
Defined in Agda.Syntax.Treeless | |
Unreachable TAlt Source # | |
Defined in Agda.Syntax.Treeless Methods isUnreachable :: TAlt -> Bool Source # | |
Subst TAlt Source # | |
Defined in Agda.Compiler.Treeless.Subst Methods applySubst :: Substitution' (SubstArg TAlt) -> TAlt -> TAlt Source # | |
HasFree TAlt Source # | |
type Rep TAlt Source # | |
Defined in Agda.Syntax.Treeless type Rep TAlt = D1 ('MetaData "TAlt" "Agda.Syntax.Treeless" "Agda-2.6.2.2-CCUZrXznmr9DtCyaOqbqEd" '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 # | |
Defined in Agda.Compiler.Treeless.Subst |
Instances
Eq CaseInfo Source # | |
Data CaseInfo Source # | |
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 # | |
Defined in Agda.Syntax.Treeless | |
Show CaseInfo Source # | |
Generic CaseInfo Source # | |
NFData CaseInfo Source # | |
Defined in Agda.Syntax.Treeless | |
type Rep CaseInfo Source # | |
Defined in Agda.Syntax.Treeless type Rep CaseInfo = D1 ('MetaData "CaseInfo" "Agda.Syntax.Treeless" "Agda-2.6.2.2-CCUZrXznmr9DtCyaOqbqEd" 'False) (C1 ('MetaCons "CaseInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "caseLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "caseType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CaseType))) |
Instances
Eq CaseType Source # | |
Data CaseType Source # | |
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 # | |
Defined in Agda.Syntax.Treeless | |
Show CaseType Source # | |
Generic CaseType Source # | |
NFData CaseType Source # | |
Defined in Agda.Syntax.Treeless | |
type Rep CaseType Source # | |
Defined in Agda.Syntax.Treeless type Rep CaseType = D1 ('MetaData "CaseType" "Agda.Syntax.Treeless" "Agda-2.6.2.2-CCUZrXznmr9DtCyaOqbqEd" '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)))) |
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 # | |
Data TPrim Source # | |
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 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 # | |
Show TPrim Source # | |
Generic TPrim Source # | |
NFData TPrim Source # | |
Defined in Agda.Syntax.Treeless | |
type Rep TPrim Source # | |
Defined in Agda.Syntax.Treeless type Rep TPrim = D1 ('MetaData "TPrim" "Agda.Syntax.Treeless" "Agda-2.6.2.2-CCUZrXznmr9DtCyaOqbqEd" '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)))))) |
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 # | |
Data TTerm Source # | |
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 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 # | |
Show TTerm Source # | |
Generic TTerm Source # | |
NFData TTerm Source # | |
Defined in Agda.Syntax.Treeless | |
Pretty TTerm Source # | |
Unreachable TTerm Source # | |
Defined in Agda.Syntax.Treeless Methods isUnreachable :: TTerm -> Bool Source # | |
DeBruijn TTerm Source # | |
Defined in Agda.Compiler.Treeless.Subst Methods deBruijnVar :: Int -> TTerm Source # debruijnNamedVar :: String -> Int -> TTerm Source # deBruijnView :: TTerm -> Maybe Int Source # | |
Subst TTerm Source # | |
Defined in Agda.Compiler.Treeless.Subst Methods applySubst :: Substitution' (SubstArg TTerm) -> TTerm -> TTerm Source # | |
HasFree TTerm Source # | |
type Rep TTerm Source # | |
Defined in Agda.Syntax.Treeless type Rep TTerm = D1 ('MetaData "TTerm" "Agda.Syntax.Treeless" "Agda-2.6.2.2-CCUZrXznmr9DtCyaOqbqEd" '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 # | |
Defined in Agda.Compiler.Treeless.Subst |
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 # | |
Defined in Agda.Syntax.Treeless Methods (==) :: EvaluationStrategy -> EvaluationStrategy -> Bool (/=) :: EvaluationStrategy -> EvaluationStrategy -> Bool | |
Show EvaluationStrategy Source # | |
Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> EvaluationStrategy -> ShowS show :: EvaluationStrategy -> String showList :: [EvaluationStrategy] -> ShowS |
Usage status of function arguments in treeless code.
Instances
Eq ArgUsage Source # | |
Data ArgUsage Source # | |
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 # | |
Defined in Agda.Syntax.Treeless | |
Show ArgUsage Source # | |
Generic ArgUsage Source # | |
NFData ArgUsage Source # | |
Defined in Agda.Syntax.Treeless | |
type Rep ArgUsage Source # | |
Defined in Agda.Syntax.Treeless type Rep ArgUsage = D1 ('MetaData "ArgUsage" "Agda.Syntax.Treeless" "Agda-2.6.2.2-CCUZrXznmr9DtCyaOqbqEd" 'False) (C1 ('MetaCons "ArgUsed" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ArgUnused" 'PrefixI 'False) (U1 :: Type -> Type)) |
Constructors
Compiled | |
Instances
Eq Compiled Source # | |
Data Compiled Source # | |
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 # | |
Defined in Agda.Syntax.Treeless | |
Show Compiled Source # | |
Generic Compiled Source # | |
NFData Compiled Source # | |
Defined in Agda.Syntax.Treeless | |
KillRange Compiled Source # | |
Defined in Agda.Syntax.Treeless Methods | |
type Rep Compiled Source # | |
Defined in Agda.Syntax.Treeless type Rep Compiled = D1 ('MetaData "Compiled" "Agda.Syntax.Treeless" "Agda-2.6.2.2-CCUZrXznmr9DtCyaOqbqEd" '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])))) |
coerceView :: TTerm -> (Bool, TTerm) Source #
Strip leading coercions and indicate whether there were some.
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
word64View :: TTerm -> Maybe Word64 Source #
negPlusKView :: TTerm -> Maybe (Integer, TTerm) Source #
tUnreachable :: 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 []