Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 whereSource
Things that can be translated to abstract syntax are instances of this class.
Methods
toAbstract :: concrete -> ScopeM abstractSource
show/hide 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 bSource
This operation does not affect the scope, i.e. the original scope is restored upon completion.
concreteToAbstract_ :: ToAbstract c a => c -> ScopeM aSource
Computes the range of all the "to" keywords used in a renaming directive.
concreteToAbstract :: ToAbstract c a => ScopeInfo -> c -> ScopeM aSource
newtype NewModuleQName Source
Constructors
NewModuleQName QName
show/hide Instances
newtype OldName Source
Constructors
OldName Name
show/hide Instances
newtype TopLevel a Source
Constructors
TopLevel a
show/hide Instances
data TopLevelInfo Source
Constructors
TopLevelInfo
topLevelDecls :: [Declaration]
outsideScope :: ScopeInfo
insideScope :: ScopeInfo
show/hide Instances
topLevelModuleName :: TopLevelInfo -> ModuleNameSource
The top-level module name.
data AbstractRHS Source
show/hide Instances
data NewModuleName Source
show/hide Instances
data OldModuleName Source
show/hide Instances
data NewName a Source
show/hide Instances
data OldQName Source
show/hide Instances
data LeftHandSide Source
show/hide Instances
data RightHandSide Source
show/hide Instances
data PatName Source
show/hide Instances
data APatName Source
show/hide Instances
data LetDef Source
show/hide Instances
data LetDefs Source
show/hide Instances
Produced by Haddock version 2.4.2