Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

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

Documentation

class Unreachable a where Source #

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

TAGuard

Binds no variables

Fields

TALit 

Fields

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

data CaseInfo Source #

Constructors

CaseInfo 

Fields

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 #

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 #

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

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

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

Subst TTerm TTerm Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

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.

Instances
Eq EvaluationStrategy Source # 
Instance details

Defined in Agda.Syntax.Treeless

Show EvaluationStrategy Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> EvaluationStrategy -> ShowS

show :: EvaluationStrategy -> String

showList :: [EvaluationStrategy] -> ShowS

data Compiled Source #

Constructors

Compiled 

Fields

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

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

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

isPrimEq :: TPrim -> Bool 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 #