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

data ArgUsage

Usage status of function arguments in treeless code.

Constructors

ArgUsed

ArgUnused

Instances

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.3.20230930-inplace" 'False) (C1 ('MetaCons "ArgUsed" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ArgUnused" 'PrefixI 'False) (U1 :: Type -> Type))

data TTerm

Treeless Term. All local variables are using de Bruijn indices.

Constructors

TVar Int

TPrim TPrim

TDef QName

TApp TTerm Args

TLam TTerm

TLit Literal

TCon QName

TLet TTerm TTerm

introduces a new (non-recursive) 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

Pretty TTerm

Defined in Agda.Compiler.Treeless.Pretty

Methods

pretty :: TTerm -> Doc

prettyPrec :: Int -> TTerm -> Doc

prettyList :: [TTerm] -> Doc

NamesIn TTerm

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> TTerm -> m

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

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.3.20230930-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))))))

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 Compiled

Constructors

Compiled

Fields

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

  Nothing if treeless usage analysis has not run yet.

Instances

Pretty Compiled

Defined in Agda.Compiler.Treeless.Pretty

Methods

pretty :: Compiled -> Doc

prettyPrec :: Int -> Compiled -> Doc

prettyList :: [Compiled] -> Doc

NamesIn Compiled

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Compiled -> m

KillRange Compiled

Defined in Agda.Syntax.Treeless

Methods

killRange :: KillRangeT 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.3.20230930-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]))))

type Args = [TTerm]

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

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.3.20230930-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 CaseInfo

Constructors

CaseInfo

Fields

• caseLazy :: Bool
• caseErased :: Erased

  Is this a match on an erased argument?

• caseType :: CaseType

Instances

NamesIn CaseInfo

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CaseInfo -> m

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.3.20230930-inplace" 'False) (C1 ('MetaCons "CaseInfo" 'PrefixI 'True) (S1 ('MetaSel ('Just "caseLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "caseErased") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Erased) :*: S1 ('MetaSel ('Just "caseType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 CaseType))))

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

The guard must only use the variable that the case expression matches on.

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

NamesIn TAlt

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> TAlt -> m

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

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.3.20230930-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 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

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.3.20230930-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 CaseType

Constructors

CTData QName

CTNat

CTInt

CTChar

CTString

CTFloat

CTQName

Instances

NamesIn CaseType

Defined in Agda.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> CaseType -> m

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.3.20230930-inplace" 'False) ((C1 ('MetaCons "CTData" 'PrefixI 'False) (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))))

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

pattern TPFn :: TPrim -> 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 []

mkLet :: TTerm -> TTerm -> TTerm

Introduces a new binding

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

tInt :: Integer -> TTerm

intView :: TTerm -> Maybe Integer

word64View :: TTerm -> Maybe Word64

tPlusK :: Integer -> TTerm -> TTerm

tOp :: TPrim -> TTerm -> TTerm -> TTerm

tNegPlusK :: Integer -> TTerm -> TTerm

plusKView :: TTerm -> Maybe (Integer, TTerm)

negPlusKView :: TTerm -> Maybe (Integer, TTerm)

tUnreachable :: TTerm

tIfThenElse :: TTerm -> TTerm -> TTerm -> TTerm