Agda-2.5.2: 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

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.

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

Constructors

PAdd 
PSub 
PMul 
PQuot 
PRem 
PGeq 
PLt 
PEqI 
PEqF 
PEqS 
PEqC 
PEqQ 
PIf 
PSeq 

Instances

Eq TPrim Source # 

Methods

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

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

Ord TPrim Source # 

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 # 

Methods

showsPrec :: Int -> TPrim -> ShowS #

show :: TPrim -> String #

showList :: [TPrim] -> ShowS #

mkLet :: TTerm -> TTerm -> TTerm Source #

Introduces a new binding

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 # 

Methods

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

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

Ord TAlt Source # 

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 # 

Methods

showsPrec :: Int -> TAlt -> ShowS #

show :: TAlt -> String #

showList :: [TAlt] -> ShowS #

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.

class Unreachable a where Source #

Minimal complete definition

isUnreachable

Methods

isUnreachable :: a -> Bool Source #

Checks if the given expression is unreachable or not.