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

data ArgUsage Source #

Usage status of function arguments in treeless code.

Constructors

ArgUsed 
ArgUnused 

Instances

Instances details
NFData ArgUsage Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

rnf :: ArgUsage -> ()

Generic ArgUsage Source # 
Instance details

Defined in Agda.Syntax.Treeless

Associated Types

type Rep ArgUsage 
Instance details

Defined in Agda.Syntax.Treeless

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

Methods

from :: ArgUsage -> Rep ArgUsage x

to :: Rep ArgUsage x -> ArgUsage

Show ArgUsage Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> ArgUsage -> ShowS

show :: ArgUsage -> String

showList :: [ArgUsage] -> ShowS

Eq ArgUsage Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

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

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

Ord ArgUsage Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Treeless

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

filterUsed :: [ArgUsage] -> [a] -> [a] Source #

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

data TTerm Source #

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

Instances details
HasFree TTerm Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: TTerm -> Map Int Occurs Source #

Pretty TTerm Source # 
Instance details

Defined in Agda.Compiler.Treeless.Pretty

NamesIn TTerm Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

Unreachable TTerm Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

isUnreachable :: TTerm -> Bool Source #

Subst TTerm Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Associated Types

type SubstArg TTerm 
Instance details

Defined in Agda.Compiler.Treeless.Subst

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 #

NFData TTerm Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

rnf :: TTerm -> ()

Generic TTerm Source # 
Instance details

Defined in Agda.Syntax.Treeless

Associated Types

type Rep TTerm 
Instance details

Defined in Agda.Syntax.Treeless

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

Methods

from :: TTerm -> Rep TTerm x

to :: Rep TTerm x -> TTerm

Show TTerm Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> TTerm -> ShowS

show :: TTerm -> String

showList :: [TTerm] -> ShowS

Eq TTerm Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

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

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

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

type SubstArg TTerm Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

type Rep TTerm Source # 
Instance details

Defined in Agda.Syntax.Treeless

type Rep TTerm = D1 ('MetaData "TTerm" "Agda.Syntax.Treeless" "Agda-2.6.20240714-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 Source #

The treeless compiler can behave differently depending on the target language evaluation strategy. For instance, more aggressive erasure for lazy targets.

Instances

Instances details
Show EvaluationStrategy Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> EvaluationStrategy -> ShowS

show :: EvaluationStrategy -> String

showList :: [EvaluationStrategy] -> ShowS

Eq EvaluationStrategy Source # 
Instance details

Defined in Agda.Syntax.Treeless

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

Introduces a new binding

data Compiled Source #

Constructors

Compiled 

Fields

Instances

Instances details
Pretty Compiled Source # 
Instance details

Defined in Agda.Compiler.Treeless.Pretty

NamesIn Compiled Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

KillRange Compiled Source # 
Instance details

Defined in Agda.Syntax.Treeless

NFData Compiled Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

rnf :: Compiled -> ()

Generic Compiled Source # 
Instance details

Defined in Agda.Syntax.Treeless

Associated Types

type Rep Compiled 
Instance details

Defined in Agda.Syntax.Treeless

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

Methods

from :: Compiled -> Rep Compiled x

to :: Rep Compiled x -> Compiled

Show Compiled Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> Compiled -> ShowS

show :: Compiled -> String

showList :: [Compiled] -> ShowS

Eq Compiled Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

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

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

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

type Rep Compiled Source # 
Instance details

Defined in Agda.Syntax.Treeless

type Rep Compiled = D1 ('MetaData "Compiled" "Agda.Syntax.Treeless" "Agda-2.6.20240714-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] Source #

class Unreachable a where Source #

Methods

isUnreachable :: a -> Bool Source #

Checks if the given expression is unreachable or not.

Instances

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

Instances details
NFData TPrim Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

rnf :: TPrim -> ()

Generic TPrim Source # 
Instance details

Defined in Agda.Syntax.Treeless

Associated Types

type Rep TPrim 
Instance details

Defined in Agda.Syntax.Treeless

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

Methods

from :: TPrim -> Rep TPrim x

to :: Rep TPrim x -> TPrim

Show TPrim Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> TPrim -> ShowS

show :: TPrim -> String

showList :: [TPrim] -> ShowS

Eq TPrim Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

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

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

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

type Rep TPrim Source # 
Instance details

Defined in Agda.Syntax.Treeless

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

Constructors

CaseInfo 

Fields

Instances

Instances details
NamesIn CaseInfo Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NFData CaseInfo Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

rnf :: CaseInfo -> ()

Generic CaseInfo Source # 
Instance details

Defined in Agda.Syntax.Treeless

Associated Types

type Rep CaseInfo 
Instance details

Defined in Agda.Syntax.Treeless

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

Methods

from :: CaseInfo -> Rep CaseInfo x

to :: Rep CaseInfo x -> CaseInfo

Show CaseInfo Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> CaseInfo -> ShowS

show :: CaseInfo -> String

showList :: [CaseInfo] -> ShowS

Eq CaseInfo Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

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

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

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

type Rep CaseInfo Source # 
Instance details

Defined in Agda.Syntax.Treeless

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

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

Fields

TALit 

Fields

Instances

Instances details
HasFree TAlt Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Methods

freeVars :: TAlt -> Map Int Occurs Source #

NamesIn TAlt Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

Unreachable TAlt Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

isUnreachable :: TAlt -> Bool Source #

Subst TAlt Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

Associated Types

type SubstArg TAlt 
Instance details

Defined in Agda.Compiler.Treeless.Subst

NFData TAlt Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

rnf :: TAlt -> ()

Generic TAlt Source # 
Instance details

Defined in Agda.Syntax.Treeless

Associated Types

type Rep TAlt 
Instance details

Defined in Agda.Syntax.Treeless

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

Methods

from :: TAlt -> Rep TAlt x

to :: Rep TAlt x -> TAlt

Show TAlt Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> TAlt -> ShowS

show :: TAlt -> String

showList :: [TAlt] -> ShowS

Eq TAlt Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

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

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

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

type SubstArg TAlt Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

type Rep TAlt Source # 
Instance details

Defined in Agda.Syntax.Treeless

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

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

Instances details
NFData TError Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

rnf :: TError -> ()

Generic TError Source # 
Instance details

Defined in Agda.Syntax.Treeless

Associated Types

type Rep TError 
Instance details

Defined in Agda.Syntax.Treeless

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

Methods

from :: TError -> Rep TError x

to :: Rep TError x -> TError

Show TError Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> TError -> ShowS

show :: TError -> String

showList :: [TError] -> ShowS

Eq TError Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

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

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

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

type Rep TError Source # 
Instance details

Defined in Agda.Syntax.Treeless

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

isPrimEq :: TPrim -> Bool Source #

coerceView :: TTerm -> (Bool, TTerm) Source #

Strip leading coercions and indicate whether there were some.

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

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

tLamView :: TTerm -> (Int, TTerm) Source #

mkTLam :: Int -> TTerm -> TTerm Source #

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 #

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

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

data CaseType Source #

Instances

Instances details
NamesIn CaseType Source # 
Instance details

Defined in Agda.Syntax.Internal.Names

Methods

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

NFData CaseType Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

rnf :: CaseType -> ()

Generic CaseType Source # 
Instance details

Defined in Agda.Syntax.Treeless

Associated Types

type Rep CaseType 
Instance details

Defined in Agda.Syntax.Treeless

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

Methods

from :: CaseType -> Rep CaseType x

to :: Rep CaseType x -> CaseType

Show CaseType Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

showsPrec :: Int -> CaseType -> ShowS

show :: CaseType -> String

showList :: [CaseType] -> ShowS

Eq CaseType Source # 
Instance details

Defined in Agda.Syntax.Treeless

Methods

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

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

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

type Rep CaseType Source # 
Instance details

Defined in Agda.Syntax.Treeless

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