Safe Haskell	None
Language	Haskell2010

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 a = OldName a
data TopLevel a = TopLevel {
- topLevelPath :: AbsolutePath
- topLevelExpectedName :: TopLevelModuleName
- topLevelTheThing :: a
}
data TopLevelInfo = TopLevelInfo {
- topLevelDecls :: [Declaration]
- topLevelScope :: ScopeInfo
}
topLevelModuleName :: TopLevelInfo -> ModuleName
data AbstractRHS
data NewModuleName
data OldModuleName
data NewName a
data OldQName
data PatName
data APatName

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 () () Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: () -> ScopeM () Source #
ToAbstract HoleContent HoleContent Source #	Content of interaction hole.
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: HoleContent0 -> ScopeM HoleContent Source #
ToAbstract RHS AbstractRHS Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RHS -> ScopeM AbstractRHS Source #
ToAbstract TypedBinding TypedBinding Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: TypedBinding0 -> ScopeM TypedBinding Source #
ToAbstract LamBinding LamBinding Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LamBinding0 -> ScopeM LamBinding Source #
ToAbstract Expr Expr Source #	Scope check an expression.
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Expr0 -> ScopeM Expr Source #
ToAbstract Clause Clause Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Clause -> ScopeM Clause0 Source #
ToAbstract NiceDeclaration Declaration Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NiceDeclaration -> ScopeM Declaration Source #
ToAbstract AbstractRHS RHS Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: AbstractRHS -> ScopeM RHS Source #
ToAbstract OldModuleName ModuleName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: OldModuleName -> ScopeM ModuleName Source #
ToAbstract NewModuleQName ModuleName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewModuleQName -> ScopeM ModuleName Source #
ToAbstract NewModuleName ModuleName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewModuleName -> ScopeM ModuleName Source #
ToAbstract PatName APatName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: PatName -> ScopeM APatName Source #
ToAbstract OldQName Expr Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: OldQName -> ScopeM Expr Source #
ToAbstract Pragma [Pragma] Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pragma0 -> ScopeM [Pragma] Source #
ToAbstract LHSCore (LHSCore' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LHSCore -> ScopeM (LHSCore' Expr) Source #
ToAbstract Pattern (Pattern' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pattern -> ScopeM (Pattern' Expr) Source #
ToAbstract ModuleAssignment (ModuleName, [LetBinding]) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: ModuleAssignment -> ScopeM (ModuleName, [LetBinding]) Source #
ToAbstract RewriteEqn (RewriteEqn' () Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RewriteEqn -> ScopeM (RewriteEqn' () Pattern Expr) Source #
ToAbstract (Binder' (NewName BoundName)) Binder Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Binder' (NewName BoundName) -> ScopeM Binder Source #
ToAbstract (TopLevel [Declaration]) TopLevelInfo Source #	Top-level declarations are always `(import\|open)* -- a bunch of possibly opened imports module ThisModule ... -- the top-level module of this file`
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: TopLevel [Declaration] -> ScopeM TopLevelInfo Source #
(Show a, ToQName a) => ToAbstract (OldName a) QName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: OldName a -> ScopeM QName Source #
ToAbstract (NewName Name) Name Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewName Name0 -> ScopeM Name Source #
ToAbstract (NewName BoundName) BindName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewName BoundName -> ScopeM BindName Source #
ToAbstract c a => ToAbstract [c] [a] Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: [c] -> ScopeM [a] Source #
ToAbstract [Declaration] [Declaration] Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: [Declaration0] -> ScopeM [Declaration] Source #
ToAbstract c a => ToAbstract (Maybe c) (Maybe a) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Maybe c -> ScopeM (Maybe a) Source #
ToAbstract c a => ToAbstract (Arg c) (Arg a) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Arg c -> ScopeM (Arg a) Source #
ToAbstract c a => ToAbstract (WithHiding c) (WithHiding a) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: WithHiding c -> ScopeM (WithHiding a) Source #
ToAbstract c a => ToAbstract (FieldAssignment' c) (FieldAssignment' a) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: FieldAssignment' c -> ScopeM (FieldAssignment' a) Source #
ToAbstract (Pattern' Expr) (Pattern' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pattern' Expr0 -> ScopeM (Pattern' Expr) Source #
ToAbstract (LHSCore' Expr) (LHSCore' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LHSCore' Expr0 -> ScopeM (LHSCore' Expr) Source #
(ToAbstract c1 a1, ToAbstract c2 a2) => ToAbstract (Either c1 c2) (Either a1 a2) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Either c1 c2 -> ScopeM (Either a1 a2) Source #
(ToAbstract c1 a1, ToAbstract c2 a2) => ToAbstract (c1, c2) (a1, a2) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: (c1, c2) -> ScopeM (a1, a2) Source #
ToAbstract c a => ToAbstract (Named name c) (Named name a) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Named name c -> ScopeM (Named name a) Source #
ToAbstract (RewriteEqn' () Pattern Expr) RewriteEqn Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RewriteEqn' () Pattern Expr -> ScopeM RewriteEqn Source #
(ToAbstract c1 a1, ToAbstract c2 a2, ToAbstract c3 a3) => ToAbstract (c1, c2, c3) (a1, a2, a3) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: (c1, c2, c3) -> ScopeM (a1, a2, a3) Source #

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 #

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

newtype NewModuleQName Source #

Constructors

NewModuleQName QName

Instances

ToAbstract NewModuleQName ModuleName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewModuleQName -> ScopeM ModuleName Source #

newtype OldName a Source #

Constructors

OldName a

Instances

(Show a, ToQName a) => ToAbstract (OldName a) QName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: OldName a -> ScopeM QName Source #

data TopLevel a Source #

Temporary data type to scope check a file.

Constructors

TopLevel
Fields topLevelPath :: AbsolutePath The file path from which we loaded this module. topLevelExpectedName :: TopLevelModuleName The expected module name (coming from the import statement that triggered scope checking this file). topLevelTheThing :: a The file content.

Instances

ToAbstract (TopLevel [Declaration]) TopLevelInfo Source #	Top-level declarations are always `(import\|open)* -- a bunch of possibly opened imports module ThisModule ... -- the top-level module of this file`
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: TopLevel [Declaration] -> ScopeM TopLevelInfo Source #

data TopLevelInfo Source #

Constructors

TopLevelInfo
Fields topLevelDecls :: [Declaration] topLevelScope :: ScopeInfo as seen from inside the module

Instances

ToAbstract (TopLevel [Declaration]) TopLevelInfo Source #	Top-level declarations are always `(import\|open)* -- a bunch of possibly opened imports module ThisModule ... -- the top-level module of this file`
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: TopLevel [Declaration] -> ScopeM TopLevelInfo Source #

topLevelModuleName :: TopLevelInfo -> ModuleName Source #

The top-level module name.

data AbstractRHS Source #

Instances

ToAbstract RHS AbstractRHS Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RHS -> ScopeM AbstractRHS Source #
ToAbstract AbstractRHS RHS Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: AbstractRHS -> ScopeM RHS Source #

data NewModuleName Source #

Instances

ToAbstract NewModuleName ModuleName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewModuleName -> ScopeM ModuleName Source #

data OldModuleName Source #

Instances

ToAbstract OldModuleName ModuleName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: OldModuleName -> ScopeM ModuleName Source #

data NewName a Source #

Instances

Functor NewName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods fmap :: (a -> b) -> NewName a -> NewName b # (<$) :: a -> NewName b -> NewName a #
ToAbstract (Binder' (NewName BoundName)) Binder Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Binder' (NewName BoundName) -> ScopeM Binder Source #
ToAbstract (NewName Name) Name Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewName Name0 -> ScopeM Name Source #
ToAbstract (NewName BoundName) BindName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewName BoundName -> ScopeM BindName Source #

data OldQName Source #

Instances

ToAbstract OldQName Expr Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: OldQName -> ScopeM Expr Source #

data PatName Source #

Instances

ToAbstract PatName APatName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: PatName -> ScopeM APatName Source #

data APatName Source #

Instances

ToAbstract PatName APatName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: PatName -> ScopeM APatName Source #