| 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
- data ArgUsage
- filterUsed :: [ArgUsage] -> [a] -> [a]
- data EvaluationStrategy
- mkLet :: TTerm -> TTerm -> TTerm
- data Compiled = Compiled {}
- type Args = [TTerm]
- class Unreachable a where
- isUnreachable :: a -> Bool
- data TPrim
- data CaseInfo = CaseInfo {}
- data TAlt
- data TError
- 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
Documentation
module Agda.Syntax.Abstract.Name
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
Usage status of function arguments in treeless code.
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
| Show EvaluationStrategy Source # | |
Defined in Agda.Syntax.Treeless Methods showsPrec :: Int -> EvaluationStrategy -> ShowS # show :: EvaluationStrategy -> String # showList :: [EvaluationStrategy] -> ShowS # | |
| Eq EvaluationStrategy Source # | |
Defined in Agda.Syntax.Treeless Methods (==) :: EvaluationStrategy -> EvaluationStrategy -> Bool # (/=) :: EvaluationStrategy -> EvaluationStrategy -> Bool # | |
Constructors
| Compiled | |
Instances
| Pretty Compiled Source # | |||||
| NamesIn Compiled Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
| KillRange Compiled Source # | |||||
Defined in Agda.Syntax.Treeless Methods | |||||
| Generic Compiled Source # | |||||
Defined in Agda.Syntax.Treeless Associated Types
| |||||
| Show Compiled Source # | |||||
| NFData Compiled Source # | |||||
Defined in Agda.Syntax.Treeless | |||||
| Eq Compiled Source # | |||||
| Ord Compiled Source # | |||||
Defined in Agda.Syntax.Treeless | |||||
| type Rep Compiled Source # | |||||
Defined in Agda.Syntax.Treeless type Rep Compiled = D1 ('MetaData "Compiled" "Agda.Syntax.Treeless" "Agda-2.6.4.3-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])))) | |||||
class Unreachable a where Source #
Instances
| Unreachable TAlt Source # | |
Defined in Agda.Syntax.Treeless Methods isUnreachable :: TAlt -> Bool Source # | |
| Unreachable TTerm Source # | |
Defined in Agda.Syntax.Treeless Methods isUnreachable :: TTerm -> Bool 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
| Generic TPrim Source # | |||||
Defined in Agda.Syntax.Treeless Associated Types
| |||||
| Show TPrim Source # | |||||
| NFData TPrim Source # | |||||
Defined in Agda.Syntax.Treeless | |||||
| Eq TPrim Source # | |||||
| Ord TPrim Source # | |||||
| type Rep TPrim Source # | |||||
Defined in Agda.Syntax.Treeless type Rep TPrim = D1 ('MetaData "TPrim" "Agda.Syntax.Treeless" "Agda-2.6.4.3-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)))))) | |||||
Constructors
| CaseInfo | |
Instances
| NamesIn CaseInfo Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
| Generic CaseInfo Source # | |||||
Defined in Agda.Syntax.Treeless Associated Types
| |||||
| Show CaseInfo Source # | |||||
| NFData CaseInfo Source # | |||||
Defined in Agda.Syntax.Treeless | |||||
| Eq CaseInfo Source # | |||||
| Ord CaseInfo Source # | |||||
Defined in Agda.Syntax.Treeless | |||||
| type Rep CaseInfo Source # | |||||
Defined in Agda.Syntax.Treeless type Rep CaseInfo = D1 ('MetaData "CaseInfo" "Agda.Syntax.Treeless" "Agda-2.6.4.3-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)))) | |||||
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) |
| TAGuard | Binds no variables The guard must only use the variable that the case expression matches on. |
| TALit | |
Instances
| HasFree TAlt Source # | |||||
| NamesIn TAlt Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
| Unreachable TAlt Source # | |||||
Defined in Agda.Syntax.Treeless Methods isUnreachable :: TAlt -> Bool Source # | |||||
| Subst TAlt Source # | |||||
Defined in Agda.Compiler.Treeless.Subst Associated Types
Methods applySubst :: Substitution' (SubstArg TAlt) -> TAlt -> TAlt Source # | |||||
| Generic TAlt Source # | |||||
Defined in Agda.Syntax.Treeless Associated Types
| |||||
| Show TAlt Source # | |||||
| NFData TAlt Source # | |||||
Defined in Agda.Syntax.Treeless | |||||
| Eq TAlt Source # | |||||
| Ord TAlt Source # | |||||
| type SubstArg TAlt Source # | |||||
Defined in Agda.Compiler.Treeless.Subst | |||||
| type Rep TAlt Source # | |||||
Defined in Agda.Syntax.Treeless type Rep TAlt = D1 ('MetaData "TAlt" "Agda.Syntax.Treeless" "Agda-2.6.4.3-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)))) | |||||
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 Source # | |||||
Defined in Agda.Syntax.Treeless Associated Types
| |||||
| Show TError Source # | |||||
| NFData TError Source # | |||||
Defined in Agda.Syntax.Treeless | |||||
| Eq TError Source # | |||||
| Ord TError Source # | |||||
| type Rep TError Source # | |||||
Defined in Agda.Syntax.Treeless type Rep TError = D1 ('MetaData "TError" "Agda.Syntax.Treeless" "Agda-2.6.4.3-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))) | |||||
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
tUnreachable :: TTerm Source #
Instances
| NamesIn CaseType Source # | |||||
Defined in Agda.Syntax.Internal.Names | |||||
| Generic CaseType Source # | |||||
Defined in Agda.Syntax.Treeless Associated Types
| |||||
| Show CaseType Source # | |||||
| NFData CaseType Source # | |||||
Defined in Agda.Syntax.Treeless | |||||
| Eq CaseType Source # | |||||
| Ord CaseType Source # | |||||
Defined in Agda.Syntax.Treeless | |||||
| type Rep CaseType Source # | |||||
Defined in Agda.Syntax.Treeless type Rep CaseType = D1 ('MetaData "CaseType" "Agda.Syntax.Treeless" "Agda-2.6.4.3-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)))) | |||||