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

Safe Haskell | None
Language | Haskell2010

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

- module Agda.Syntax.Abstract.Name
- data TTerm
  - = TVar Int
  - | TPrim TPrim
  - | TDef QName
  - | TApp TTerm Args
  - | TLam TTerm
  - | TLit Literal
  - | TCon QName
  - | TLet TTerm TTerm
  - | TCase Int CaseInfo TTerm [TAlt]
  - | TUnit
  - | TSort
  - | TErased
  - | TCoerce TTerm
  - | TError TError
- data ArgUsage
  - = ArgUsed
  - | ArgUnused
- filterUsed :: [ArgUsage] -> [a] -> [a]
- data EvaluationStrategy
  - = LazyEvaluation
  - | EagerEvaluation
- mkLet :: TTerm -> TTerm -> TTerm
- data Compiled = Compiled {
  - cTreeless :: TTerm
  - cArgUsage :: Maybe [ArgUsage]
  }
- type Args = [TTerm]
- class Unreachable a where
  - isUnreachable :: a -> Bool
- data TPrim
  - = PAdd
  - | PAdd64
  - | PSub
  - | PSub64
  - | PMul
  - | PMul64
  - | PQuot
  - | PQuot64
  - | PRem
  - | PRem64
  - | PGeq
  - | PLt
  - | PLt64
  - | PEqI
  - | PEq64
  - | PEqF
  - | PEqS
  - | PEqC
  - | PEqQ
  - | PIf
  - | PSeq
  - | PITo64
  - | P64ToI
- data CaseInfo = CaseInfo {
  - caseLazy :: Bool
  - caseErased :: Erased
  - caseType :: CaseType
  }
- data TAlt
  - = TACon {
    - aCon :: QName
    - aArity :: Int
    - aBody :: TTerm
    }
  - | TAGuard {
    - aGuard :: TTerm
    - aBody :: TTerm
    }
  - | TALit {
    - aLit :: Literal
    - aBody :: TTerm
    }
- data TError
  - = TUnreachable
  - | TMeta String
- isPrimEq :: TPrim -> Bool
- coerceView :: TTerm -> (Bool, TTerm)
- mkTApp :: TTerm -> Args -> TTerm
- tAppView :: TTerm -> (TTerm, [TTerm])
- coerceAppView :: TTerm -> ((Bool, TTerm), [TTerm])
- 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)
- pattern TPOp :: TPrim -> TTerm -> TTerm -> TTerm
- pattern TPFn :: TPrim -> TTerm -> TTerm
- tUnreachable :: TTerm
- tIfThenElse :: TTerm -> TTerm -> TTerm -> TTerm
- data CaseType
  - = CTData QName
  - | CTNat
  - | CTInt
  - | CTChar
  - | CTString
  - | CTFloat
  - | CTQName

# Documentation

module Agda.Syntax.Abstract.Name

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 -> IntMap Occurs Source #
Pretty TTerm Source # |
Instance details Defined in Agda.Compiler.Treeless.Pretty Methods pretty :: TTerm -> Doc Source # prettyPrec :: Int -> TTerm -> Doc Source # prettyList :: [TTerm] -> Doc Source #
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 type SubstArg TTerm = TTerm

Methods

applySubst :: Substitution' (SubstArg TTerm) -> TTerm -> TTerm 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 #
NFData TTerm Source # |
Instance details Defined in Agda.Syntax.Treeless Methods rnf :: TTerm -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep TTerm x -> TTerm Source #

Show TTerm Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TTerm -> ShowS Source # show :: TTerm -> String Source # showList :: [TTerm] -> ShowS Source #
Eq TTerm Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: TTerm -> TTerm -> Bool Source # (/=) :: TTerm -> TTerm -> Bool Source #
Ord TTerm Source # |
Instance details Defined in Agda.Syntax.Treeless Methods compare :: TTerm -> TTerm -> Ordering Source # (<) :: TTerm -> TTerm -> Bool Source # (<=) :: TTerm -> TTerm -> Bool Source # (>) :: TTerm -> TTerm -> Bool Source # (>=) :: TTerm -> TTerm -> Bool Source # max :: TTerm -> TTerm -> TTerm Source # min :: TTerm -> TTerm -> TTerm Source #
type SubstArg TTerm Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst type SubstArg TTerm = TTerm
type Rep TTerm Source # |

Instance details

Defined in Agda.Syntax.Treeless

type Rep TTerm = D1 ('MetaData "TTerm" "Agda.Syntax.Treeless" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "ArgUsed" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ArgUnused" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: ArgUsage -> Rep ArgUsage x Source #

to :: Rep ArgUsage x -> ArgUsage Source #

Show ArgUsage Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> ArgUsage -> ShowS Source # show :: ArgUsage -> String Source # showList :: [ArgUsage] -> ShowS Source #
Eq ArgUsage Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: ArgUsage -> ArgUsage -> Bool Source # (/=) :: ArgUsage -> ArgUsage -> Bool Source #
Ord ArgUsage Source # |
Instance details Defined in Agda.Syntax.Treeless Methods compare :: ArgUsage -> ArgUsage -> Ordering Source # (<) :: ArgUsage -> ArgUsage -> Bool Source # (<=) :: ArgUsage -> ArgUsage -> Bool Source # (>) :: ArgUsage -> ArgUsage -> Bool Source # (>=) :: ArgUsage -> ArgUsage -> Bool Source # max :: ArgUsage -> ArgUsage -> ArgUsage Source # min :: ArgUsage -> ArgUsage -> ArgUsage Source #
type Rep ArgUsage Source # |
Instance details Defined in Agda.Syntax.Treeless type Rep ArgUsage = D1 ('MetaData "ArgUsage" "Agda.Syntax.Treeless" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 EvaluationStrategy Source #

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

Instances details

Show EvaluationStrategy Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> EvaluationStrategy -> ShowS Source # show :: EvaluationStrategy -> String Source # showList :: [EvaluationStrategy] -> ShowS Source #
Eq EvaluationStrategy Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: EvaluationStrategy -> EvaluationStrategy -> Bool Source # (/=) :: EvaluationStrategy -> EvaluationStrategy -> Bool Source #

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

Introduces a new binding

data Compiled Source #

Constructors

Compiled |

Fields

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

  `Nothing` if treeless usage analysis has not run yet.

#### Instances

Instances details

Pretty Compiled Source # |
Instance details Defined in Agda.Compiler.Treeless.Pretty Methods pretty :: Compiled -> Doc Source # prettyPrec :: Int -> Compiled -> Doc Source # prettyList :: [Compiled] -> Doc Source #
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 Methods killRange :: KillRangeT Compiled Source #
NFData Compiled Source # |
Instance details Defined in Agda.Syntax.Treeless Methods rnf :: Compiled -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep Compiled x -> Compiled Source #

Show Compiled Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> Compiled -> ShowS Source # show :: Compiled -> String Source # showList :: [Compiled] -> ShowS Source #
Eq Compiled Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: Compiled -> Compiled -> Bool Source # (/=) :: Compiled -> Compiled -> Bool Source #
Ord Compiled Source # |
Instance details Defined in Agda.Syntax.Treeless Methods compare :: Compiled -> Compiled -> Ordering Source # (<) :: Compiled -> Compiled -> Bool Source # (<=) :: Compiled -> Compiled -> Bool Source # (>) :: Compiled -> Compiled -> Bool Source # (>=) :: Compiled -> Compiled -> Bool Source # max :: Compiled -> Compiled -> Compiled Source # min :: Compiled -> Compiled -> Compiled Source #
type Rep Compiled Source # |

Instance details

Defined in Agda.Syntax.Treeless

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

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

Instances details

NFData TPrim Source # |
Instance details Defined in Agda.Syntax.Treeless Methods rnf :: TPrim -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep TPrim x -> TPrim Source #

Show TPrim Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TPrim -> ShowS Source # show :: TPrim -> String Source # showList :: [TPrim] -> ShowS Source #
Eq TPrim Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: TPrim -> TPrim -> Bool Source # (/=) :: TPrim -> TPrim -> Bool Source #
Ord TPrim Source # |
Instance details Defined in Agda.Syntax.Treeless Methods compare :: TPrim -> TPrim -> Ordering Source # (<) :: TPrim -> TPrim -> Bool Source # (<=) :: TPrim -> TPrim -> Bool Source # (>) :: TPrim -> TPrim -> Bool Source # (>=) :: TPrim -> TPrim -> Bool Source # max :: TPrim -> TPrim -> TPrim Source # min :: TPrim -> TPrim -> TPrim Source #
type Rep TPrim Source # |

Instance details

Defined in Agda.Syntax.Treeless

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

- caseLazy :: Bool
- caseErased :: Erased

  Is this a match on an erased argument?

- caseType :: CaseType

#### 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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep CaseInfo x -> CaseInfo Source #

Show CaseInfo Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> CaseInfo -> ShowS Source # show :: CaseInfo -> String Source # showList :: [CaseInfo] -> ShowS Source #
Eq CaseInfo Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: CaseInfo -> CaseInfo -> Bool Source # (/=) :: CaseInfo -> CaseInfo -> Bool Source #
Ord CaseInfo Source # |
Instance details Defined in Agda.Syntax.Treeless Methods compare :: CaseInfo -> CaseInfo -> Ordering Source # (<) :: CaseInfo -> CaseInfo -> Bool Source # (<=) :: CaseInfo -> CaseInfo -> Bool Source # (>) :: CaseInfo -> CaseInfo -> Bool Source # (>=) :: CaseInfo -> CaseInfo -> Bool Source # max :: CaseInfo -> CaseInfo -> CaseInfo Source # min :: CaseInfo -> CaseInfo -> CaseInfo Source #
type Rep CaseInfo Source # |

Instance details

Defined in Agda.Syntax.Treeless

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

- 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

Instances details

HasFree TAlt Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst Methods freeVars :: TAlt -> IntMap 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 type SubstArg TAlt = TTerm

Methods

applySubst :: Substitution' (SubstArg TAlt) -> TAlt -> TAlt Source #

NFData TAlt Source # |
Instance details Defined in Agda.Syntax.Treeless Methods rnf :: TAlt -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep TAlt x -> TAlt Source #

Show TAlt Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TAlt -> ShowS Source # show :: TAlt -> String Source # showList :: [TAlt] -> ShowS Source #
Eq TAlt Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: TAlt -> TAlt -> Bool Source # (/=) :: TAlt -> TAlt -> Bool Source #
Ord TAlt Source # |
Instance details Defined in Agda.Syntax.Treeless Methods compare :: TAlt -> TAlt -> Ordering Source # (<) :: TAlt -> TAlt -> Bool Source # (<=) :: TAlt -> TAlt -> Bool Source # (>) :: TAlt -> TAlt -> Bool Source # (>=) :: TAlt -> TAlt -> Bool Source # max :: TAlt -> TAlt -> TAlt Source # min :: TAlt -> TAlt -> TAlt Source #
type SubstArg TAlt Source # |
Instance details Defined in Agda.Compiler.Treeless.Subst type SubstArg TAlt = TTerm
type Rep TAlt Source # |

Instance details

Defined in Agda.Syntax.Treeless

type Rep TAlt = D1 ('MetaData "TAlt" "Agda.Syntax.Treeless" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep TError x -> TError Source #

Show TError Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> TError -> ShowS Source # show :: TError -> String Source # showList :: [TError] -> ShowS Source #
Eq TError Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: TError -> TError -> Bool Source # (/=) :: TError -> TError -> Bool Source #
Ord TError Source # |
Instance details Defined in Agda.Syntax.Treeless Methods compare :: TError -> TError -> Ordering Source # (<) :: TError -> TError -> Bool Source # (<=) :: TError -> TError -> Bool Source # (>) :: TError -> TError -> Bool Source # (>=) :: TError -> TError -> Bool Source # max :: TError -> TError -> TError Source # min :: TError -> TError -> TError Source #
type Rep TError Source # |
Instance details Defined in Agda.Syntax.Treeless type Rep TError = D1 ('MetaData "TError" "Agda.Syntax.Treeless" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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.

mkTApp :: TTerm -> Args -> TTerm Source #

tAppView :: TTerm -> (TTerm, [TTerm]) Source #

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`

tLetView :: TTerm -> ([TTerm], TTerm) Source #

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

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

tInt :: Integer -> TTerm Source #

intView :: TTerm -> Maybe Integer Source #

word64View :: TTerm -> Maybe Word64 Source #

tPlusK :: Integer -> TTerm -> TTerm Source #

tOp :: TPrim -> TTerm -> TTerm -> TTerm Source #

tNegPlusK :: Integer -> TTerm -> TTerm Source #

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

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

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

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

tUnreachable :: TTerm Source #

tIfThenElse :: TTerm -> TTerm -> TTerm -> TTerm Source #

data CaseType Source #

Constructors

CTData QName |
CTNat |
CTInt |
CTChar |
CTString |
CTFloat |
CTQName |

#### 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 -> () Source #
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.8.0-DJrTbcOFazJDzri4fKrI2F" '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 Source #

to :: Rep CaseType x -> CaseType Source #

Show CaseType Source # |
Instance details Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> CaseType -> ShowS Source # show :: CaseType -> String Source # showList :: [CaseType] -> ShowS Source #
Eq CaseType Source # |
Instance details Defined in Agda.Syntax.Treeless Methods (==) :: CaseType -> CaseType -> Bool Source # (/=) :: CaseType -> CaseType -> Bool Source #
Ord CaseType Source # |
Instance details Defined in Agda.Syntax.Treeless Methods compare :: CaseType -> CaseType -> Ordering Source # (<) :: CaseType -> CaseType -> Bool Source # (<=) :: CaseType -> CaseType -> Bool Source # (>) :: CaseType -> CaseType -> Bool Source # (>=) :: CaseType -> CaseType -> Bool Source # max :: CaseType -> CaseType -> CaseType Source # min :: CaseType -> CaseType -> CaseType Source #
type Rep CaseType Source # |

Instance details

Defined in Agda.Syntax.Treeless

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