Agda.Syntax.Treeless

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

Documentation

module Agda.Syntax.Abstract.Name

class Unreachable a where

Methods

isUnreachable :: a -> Bool

Checks if the given expression is unreachable or not.

Instances

Unreachable TAlt

Defined in Agda.Syntax.Treeless

Methods

isUnreachable :: TAlt -> Bool

Unreachable TTerm

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.

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

Data TError

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

Generic TError

Defined in Agda.Syntax.Treeless

Associated Types

type Rep TError :: Type -> Type

Methods

from :: TError -> Rep TError x

to :: Rep TError x -> TError

Show TError

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> TError -> ShowS

show :: TError -> String

showList :: [TError] -> ShowS

NFData TError

Defined in Agda.Syntax.Treeless

Methods

rnf :: TError -> ()

Eq TError

Defined in Agda.Syntax.Treeless

Methods

(==) :: TError -> TError -> Bool

(/=) :: TError -> TError -> Bool

Ord TError

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

type Rep TError

Defined in Agda.Syntax.Treeless

type Rep TError = D1 ('MetaData "TError" "Agda.Syntax.Treeless" "Agda-2.6.2.1.20220327-inplace" '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

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

HasFree TAlt

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: TAlt -> Map Int Occurs

Unreachable TAlt

Defined in Agda.Syntax.Treeless

Methods

isUnreachable :: TAlt -> Bool

Subst TAlt

Defined in Agda.Compiler.Treeless.Subst

Associated Types

type SubstArg TAlt

Methods

applySubst :: Substitution' (SubstArg TAlt) -> TAlt -> TAlt

Data TAlt

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

Generic TAlt

Defined in Agda.Syntax.Treeless

Associated Types

type Rep TAlt :: Type -> Type

Methods

from :: TAlt -> Rep TAlt x

to :: Rep TAlt x -> TAlt

Show TAlt

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> TAlt -> ShowS

show :: TAlt -> String

showList :: [TAlt] -> ShowS

NFData TAlt

Defined in Agda.Syntax.Treeless

Methods

rnf :: TAlt -> ()

Eq TAlt

Defined in Agda.Syntax.Treeless

Methods

(==) :: TAlt -> TAlt -> Bool

(/=) :: TAlt -> TAlt -> Bool

Ord TAlt

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

type SubstArg TAlt

Defined in Agda.Compiler.Treeless.Subst

type SubstArg TAlt = TTerm

type Rep TAlt

Defined in Agda.Syntax.Treeless

type Rep TAlt = D1 ('MetaData "TAlt" "Agda.Syntax.Treeless" "Agda-2.6.2.1.20220327-inplace" '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))))

data CaseInfo

Constructors

CaseInfo

Fields

• caseLazy :: Bool
• caseType :: CaseType

Instances

Data CaseInfo

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

Generic CaseInfo

Defined in Agda.Syntax.Treeless

Associated Types

type Rep CaseInfo :: Type -> Type

Methods

from :: CaseInfo -> Rep CaseInfo x

to :: Rep CaseInfo x -> CaseInfo

Show CaseInfo

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> CaseInfo -> ShowS

show :: CaseInfo -> String

showList :: [CaseInfo] -> ShowS

NFData CaseInfo

Defined in Agda.Syntax.Treeless

Methods

rnf :: CaseInfo -> ()

Eq CaseInfo

Defined in Agda.Syntax.Treeless

Methods

(==) :: CaseInfo -> CaseInfo -> Bool

(/=) :: CaseInfo -> CaseInfo -> Bool

Ord CaseInfo

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

type Rep CaseInfo

Defined in Agda.Syntax.Treeless

type Rep CaseInfo = D1 ('MetaData "CaseInfo" "Agda.Syntax.Treeless" "Agda-2.6.2.1.20220327-inplace" '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

Constructors

CTData Quantity QName

CTNat

CTInt

CTChar

CTString

CTFloat

CTQName

Instances

Data CaseType

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

Generic CaseType

Defined in Agda.Syntax.Treeless

Associated Types

type Rep CaseType :: Type -> Type

Methods

from :: CaseType -> Rep CaseType x

to :: Rep CaseType x -> CaseType

Show CaseType

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> CaseType -> ShowS

show :: CaseType -> String

showList :: [CaseType] -> ShowS

NFData CaseType

Defined in Agda.Syntax.Treeless

Methods

rnf :: CaseType -> ()

Eq CaseType

Defined in Agda.Syntax.Treeless

Methods

(==) :: CaseType -> CaseType -> Bool

(/=) :: CaseType -> CaseType -> Bool

Ord CaseType

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

type Rep CaseType

Defined in Agda.Syntax.Treeless

type Rep CaseType = D1 ('MetaData "CaseType" "Agda.Syntax.Treeless" "Agda-2.6.2.1.20220327-inplace" '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

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

Data TPrim

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

Generic TPrim

Defined in Agda.Syntax.Treeless

Associated Types

type Rep TPrim :: Type -> Type

Methods

from :: TPrim -> Rep TPrim x

to :: Rep TPrim x -> TPrim

Show TPrim

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> TPrim -> ShowS

show :: TPrim -> String

showList :: [TPrim] -> ShowS

NFData TPrim

Defined in Agda.Syntax.Treeless

Methods

rnf :: TPrim -> ()

Eq TPrim

Defined in Agda.Syntax.Treeless

Methods

(==) :: TPrim -> TPrim -> Bool

(/=) :: TPrim -> TPrim -> Bool

Ord TPrim

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

type Rep TPrim

Defined in Agda.Syntax.Treeless

type Rep TPrim = D1 ('MetaData "TPrim" "Agda.Syntax.Treeless" "Agda-2.6.2.1.20220327-inplace" '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

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

HasFree TTerm

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: TTerm -> Map Int Occurs

Unreachable TTerm

Defined in Agda.Syntax.Treeless

Methods

isUnreachable :: TTerm -> Bool

Subst TTerm

Defined in Agda.Compiler.Treeless.Subst

Associated Types

type SubstArg TTerm

Methods

applySubst :: Substitution' (SubstArg TTerm) -> TTerm -> TTerm

DeBruijn TTerm

Defined in Agda.Compiler.Treeless.Subst

Methods

deBruijnVar :: Int -> TTerm

debruijnNamedVar :: String -> Int -> TTerm

deBruijnView :: TTerm -> Maybe Int

Pretty TTerm

Defined in Agda.Compiler.Treeless.Pretty

Methods

pretty :: TTerm -> Doc

prettyPrec :: Int -> TTerm -> Doc

prettyList :: [TTerm] -> Doc

Data TTerm

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

Generic TTerm

Defined in Agda.Syntax.Treeless

Associated Types

type Rep TTerm :: Type -> Type

Methods

from :: TTerm -> Rep TTerm x

to :: Rep TTerm x -> TTerm

Show TTerm

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> TTerm -> ShowS

show :: TTerm -> String

showList :: [TTerm] -> ShowS

NFData TTerm

Defined in Agda.Syntax.Treeless

Methods

rnf :: TTerm -> ()

Eq TTerm

Defined in Agda.Syntax.Treeless

Methods

(==) :: TTerm -> TTerm -> Bool

(/=) :: TTerm -> TTerm -> Bool

Ord TTerm

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

type SubstArg TTerm

Defined in Agda.Compiler.Treeless.Subst

type SubstArg TTerm = TTerm

type Rep TTerm

Defined in Agda.Syntax.Treeless

type Rep TTerm = D1 ('MetaData "TTerm" "Agda.Syntax.Treeless" "Agda-2.6.2.1.20220327-inplace" '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 Args = [TTerm]

data EvaluationStrategy

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

Show EvaluationStrategy

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> EvaluationStrategy -> ShowS

show :: EvaluationStrategy -> String

showList :: [EvaluationStrategy] -> ShowS

Eq EvaluationStrategy

Defined in Agda.Syntax.Treeless

Methods

(==) :: EvaluationStrategy -> EvaluationStrategy -> Bool

(/=) :: EvaluationStrategy -> EvaluationStrategy -> Bool

data ArgUsage

Usage status of function arguments in treeless code.

Constructors

ArgUsed

ArgUnused

Instances

Data ArgUsage

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

Generic ArgUsage

Defined in Agda.Syntax.Treeless

Associated Types

type Rep ArgUsage :: Type -> Type

Methods

from :: ArgUsage -> Rep ArgUsage x

to :: Rep ArgUsage x -> ArgUsage

Show ArgUsage

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> ArgUsage -> ShowS

show :: ArgUsage -> String

showList :: [ArgUsage] -> ShowS

NFData ArgUsage

Defined in Agda.Syntax.Treeless

Methods

rnf :: ArgUsage -> ()

Eq ArgUsage

Defined in Agda.Syntax.Treeless

Methods

(==) :: ArgUsage -> ArgUsage -> Bool

(/=) :: ArgUsage -> ArgUsage -> Bool

Ord ArgUsage

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

type Rep ArgUsage

Defined in Agda.Syntax.Treeless

type Rep ArgUsage = D1 ('MetaData "ArgUsage" "Agda.Syntax.Treeless" "Agda-2.6.2.1.20220327-inplace" 'False) (C1 ('MetaCons "ArgUsed" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ArgUnused" 'PrefixI 'False) (U1 :: Type -> Type))

data Compiled

Constructors

Compiled

Fields

• cTreeless :: TTerm
• cArgUsage :: Maybe [ArgUsage]

  Nothing if treeless usage analysis has not run yet.

Instances

KillRange Compiled

Defined in Agda.Syntax.Treeless

Methods

killRange :: KillRangeT Compiled

Data Compiled

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

Generic Compiled

Defined in Agda.Syntax.Treeless

Associated Types

type Rep Compiled :: Type -> Type

Methods

from :: Compiled -> Rep Compiled x

to :: Rep Compiled x -> Compiled

Show Compiled

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> Compiled -> ShowS

show :: Compiled -> String

showList :: [Compiled] -> ShowS

NFData Compiled

Defined in Agda.Syntax.Treeless

Methods

rnf :: Compiled -> ()

Eq Compiled

Defined in Agda.Syntax.Treeless

Methods

(==) :: Compiled -> Compiled -> Bool

(/=) :: Compiled -> Compiled -> Bool

Ord Compiled

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

type Rep Compiled

Defined in Agda.Syntax.Treeless

type Rep Compiled = D1 ('MetaData "Compiled" "Agda.Syntax.Treeless" "Agda-2.6.2.1.20220327-inplace" '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

pattern TPOp :: TPrim -> TTerm -> TTerm -> TTerm

isPrimEq :: TPrim -> Bool

coerceView :: TTerm -> (Bool, TTerm)

Strip leading coercions and indicate whether there were some.

mkTApp :: TTerm -> Args -> TTerm

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

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

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)

tLamView :: TTerm -> (Int, TTerm)

mkTLam :: Int -> TTerm -> TTerm

mkLet :: TTerm -> TTerm -> TTerm

Introduces a new binding

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]

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 []