Safe Haskell	None
Language	Haskell98

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

module Agda.Syntax.Abstract.Name

data Compiled Source

Constructors

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

Instances

Eq Compiled Source
Ord Compiled Source
Show Compiled Source
KillRange Compiled Source

type Args = [TTerm] Source

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 CaseType 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
TError TError	A runtime error, something bad has happened.

Instances

Eq TTerm Source
Ord TTerm Source
Show TTerm Source
Unreachable TTerm Source
HasFree TTerm Source

data TPrim Source

Compiler-related primitives. This are NOT the same thing as primitives in Agda's surface or internal syntax!

Constructors

PAdd
PSub
PMul
PQuot
PRem
PGeq
PLt
PEq
PIf
PSeq

Instances

Eq TPrim Source
Ord TPrim Source
Show TPrim Source

mkTApp :: TTerm -> Args -> TTerm Source

tAppView :: TTerm -> [TTerm] Source

mkLet :: TTerm -> TTerm -> TTerm Source

Introduces a new binding

tInt :: Integer -> TTerm Source

intView :: TTerm -> Maybe Integer 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

data CaseType Source

Constructors

CTData QName
CTChar
CTString
CTQName

Instances

Eq CaseType Source
Ord CaseType Source
Show CaseType Source

data TAlt Source

Constructors

TACon	Matches on the given constructor. If the match succeeds, the pattern variables are prepended to the current environment (pushes all existing variables aArity steps further away)
Fields aCon :: QName aArity :: Int aBody :: TTerm
TAGuard	Binds no variables
Fields aGuard :: TTerm aBody :: TTerm
TALit
Fields aLit :: Literal aBody :: TTerm

Instances

Eq TAlt Source
Ord TAlt Source
Show TAlt Source
Unreachable TAlt Source
HasFree TAlt 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
Ord TError Source
Show TError Source

class Unreachable a where Source

Methods

isUnreachable :: a -> Bool Source

Checks if the given expression is unreachable or not.

Instances

Unreachable TAlt Source
Unreachable TTerm Source