| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Syntax.Translation.ConcreteToAbstract

Description
Translation from Agda.Syntax.Concrete to Agda.Syntax.Abstract. Involves scope analysis, figuring out infix operator precedences and tidying up definitions.
Synopsis

class ToAbstract concrete abstract | concrete -> abstract where

toAbstract :: concrete -> ScopeM abstract

localToAbstract :: ToAbstract c a => c -> (a -> ScopeM b) -> ScopeM b
concreteToAbstract_ :: ToAbstract c a => c -> ScopeM a
concreteToAbstract :: ToAbstract c a => ScopeInfo -> c -> ScopeM a
newtype NewModuleQName = NewModuleQName QName
newtype OldName = OldName Name
newtype TopLevel a = TopLevel a

data TopLevelInfo = TopLevelInfo {

topLevelDecls :: [Declaration]
outsideScope :: ScopeInfo
insideScope :: ScopeInfo

}

topLevelModuleName :: TopLevelInfo -> ModuleName
data AbstractRHS
data NewModuleName
data OldModuleName
data NewName a
data OldQName
data LeftHandSide
data RightHandSide
data PatName
data APatName
data LetDef
data LetDefs

Documentation

class ToAbstract concrete abstract | concrete -> abstract where | Source

Things that can be translated to abstract syntax are instances of this class.
Methods

toAbstract :: concrete -> ScopeM abstract | Source

Instances

ToAbstract RHS AbstractRHS
ToAbstract RHS AbstractRHS
ToAbstract TypedBinding TypedBinding
ToAbstract TypedBinding TypedBinding
ToAbstract TypedBindings TypedBindings
ToAbstract TypedBindings TypedBindings
ToAbstract LamBinding LamBinding
ToAbstract LamBinding LamBinding
ToAbstract Expr Expr
ToAbstract Expr Expr
ToAbstract Clause Clause
ToAbstract Clause Clause
ToAbstract NiceDefinition Definition
ToAbstract NiceDefinition Definition
ToAbstract NiceDeclaration Declaration
ToAbstract NiceDeclaration Declaration
ToAbstract LeftHandSide LHS
ToAbstract LeftHandSide LHS
ToAbstract AbstractRHS RHS
ToAbstract AbstractRHS RHS
ToAbstract RightHandSide AbstractRHS
ToAbstract RightHandSide AbstractRHS
ToAbstract OldModuleName ModuleName
ToAbstract OldModuleName ModuleName
ToAbstract NewModuleQName ModuleName
ToAbstract NewModuleQName ModuleName
ToAbstract NewModuleName ModuleName
ToAbstract NewModuleName ModuleName
ToAbstract PatName APatName
ToAbstract PatName APatName
ToAbstract OldName QName
ToAbstract OldName QName
ToAbstract OldQName Expr
ToAbstract OldQName Expr
ToAbstract Pragma ([] Pragma)
ToAbstract Pragma ([] Pragma)
ToAbstract Pattern (Pattern' Expr)
ToAbstract Pattern (Pattern' Expr)
ToAbstract LetDef ([] LetBinding)
ToAbstract LetDef ([] LetBinding)
ToAbstract LetDefs ([] LetBinding)
ToAbstract LetDefs ([] LetBinding)
ToAbstract (Constr NiceDeclaration) Declaration
ToAbstract (Constr NiceDeclaration) Declaration
ToAbstract (TopLevel ([] Declaration)) TopLevelInfo
ToAbstract (TopLevel ([] Declaration)) TopLevelInfo
ToAbstract (NewName Name) Name
ToAbstract (NewName Name) Name
ToAbstract (NewName BoundName) Name
ToAbstract (NewName BoundName) Name
ToAbstract c a => ToAbstract ([] c) ([] a)
ToAbstract ([] Declaration) ([] Declaration)
ToAbstract c a => ToAbstract (Maybe c) (Maybe a)
ToAbstract c a => ToAbstract (Arg c) (Arg a)
ToAbstract c a => ToAbstract (Pattern' c) (Pattern' a)
(ToAbstract c1 a1, ToAbstract c2 a2) => ToAbstract ((,) c1 c2) ((,) a1 a2)
ToAbstract c a => ToAbstract (Named name c) (Named name a)
(ToAbstract c1 a1, ToAbstract c2 a2, ToAbstract c3 a3) => ToAbstract ((,,) c1 c2 c3) ((,,) a1 a2 a3)

localToAbstract :: ToAbstract c a => c -> (a -> ScopeM b) -> ScopeM b | Source

This operation does not affect the scope, i.e. the original scope is restored upon completion.

concreteToAbstract_ :: ToAbstract c a => c -> ScopeM a | Source

Computes the range of all the "to" keywords used in a renaming directive.

concreteToAbstract :: ToAbstract c a => ScopeInfo -> c -> ScopeM a | Source

newtype NewModuleQName | Source

Constructors

NewModuleQName QName |

Instances

ToAbstract NewModuleQName ModuleName

newtype OldName | Source

Constructors

OldName Name |

Instances

ToAbstract OldName QName

newtype TopLevel a | Source

Constructors

TopLevel a |

Instances

ToAbstract (TopLevel ([] Declaration)) TopLevelInfo

data TopLevelInfo | Source

Constructors

TopLevelInfo |

topLevelDecls :: [Declaration] |
outsideScope :: ScopeInfo |
insideScope :: ScopeInfo |

Instances

ToAbstract (TopLevel ([] Declaration)) TopLevelInfo

topLevelModuleName :: TopLevelInfo -> ModuleName | Source

The top-level module name.

data AbstractRHS | Source

Instances

ToAbstract RHS AbstractRHS
ToAbstract AbstractRHS RHS
ToAbstract RightHandSide AbstractRHS

data NewModuleName | Source

Instances

ToAbstract NewModuleName ModuleName

data OldModuleName | Source

Instances

ToAbstract OldModuleName ModuleName

data NewName a | Source

Instances

ToAbstract (NewName Name) Name
ToAbstract (NewName BoundName) Name

data OldQName | Source

Instances

ToAbstract OldQName Expr

data LeftHandSide | Source

Instances

ToAbstract LeftHandSide LHS

data RightHandSide | Source

Instances

ToAbstract RightHandSide AbstractRHS

data PatName | Source

Instances

ToAbstract PatName APatName

data APatName | Source

Instances

ToAbstract PatName APatName

data LetDef | Source

Instances

ToAbstract LetDef ([] LetBinding)

data LetDefs | Source

Instances

ToAbstract LetDefs ([] LetBinding)

Produced by Haddock version 2.4.2