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
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 LeftHandSide
data RightHandSide
data PatName
data APatName
data LetDef
data LetDefs

Documentation

class ToAbstract concrete abstract | concrete -> abstract where #

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

Minimal complete definition

toAbstract

Methods

toAbstract :: concrete -> ScopeM abstract #

Instances

ToAbstract HoleContent HoleContent #	Content of interaction hole.
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: HoleContent0 -> ScopeM HoleContent #
ToAbstract RHS AbstractRHS #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RHS -> ScopeM AbstractRHS #
ToAbstract TypedBinding TypedBinding #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: TypedBinding0 -> ScopeM TypedBinding #
ToAbstract TypedBindings TypedBindings #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: TypedBindings0 -> ScopeM TypedBindings #
ToAbstract LamBinding LamBinding #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LamBinding0 -> ScopeM LamBinding #
ToAbstract Expr Expr #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Expr0 -> ScopeM Expr #
ToAbstract Clause Clause #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Clause -> ScopeM Clause0 #
ToAbstract NiceDeclaration Declaration #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NiceDeclaration -> ScopeM Declaration #
ToAbstract LeftHandSide LHS #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LeftHandSide -> ScopeM LHS #
ToAbstract AbstractRHS RHS #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: AbstractRHS -> ScopeM RHS #
ToAbstract RightHandSide AbstractRHS #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: RightHandSide -> ScopeM AbstractRHS #
ToAbstract OldModuleName ModuleName #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: OldModuleName -> ScopeM ModuleName #
ToAbstract NewModuleQName ModuleName #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewModuleQName -> ScopeM ModuleName #
ToAbstract NewModuleName ModuleName #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewModuleName -> ScopeM ModuleName #
ToAbstract PatName APatName #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: PatName -> ScopeM APatName #
ToAbstract OldQName Expr #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: OldQName -> ScopeM Expr #
ToAbstract Pragma [Pragma] #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pragma0 -> ScopeM [Pragma] #
ToAbstract LHSCore (LHSCore' Expr) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LHSCore -> ScopeM (LHSCore' Expr) #
ToAbstract Pattern (Pattern' Expr) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pattern -> ScopeM (Pattern' Expr) #
ToAbstract LetDef [LetBinding] #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LetDef -> ScopeM [LetBinding] #
ToAbstract LetDefs [LetBinding] #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LetDefs -> ScopeM [LetBinding] #
ToAbstract ModuleAssignment (ModuleName, [LetBinding]) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: ModuleAssignment -> ScopeM (ModuleName, [LetBinding]) #
ToAbstract (TopLevel [Declaration]) TopLevelInfo #	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 #
(Show a, ToQName a) => ToAbstract (OldName a) QName #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: OldName a -> ScopeM QName #
ToAbstract (NewName Name) Name #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewName Name0 -> ScopeM Name #
ToAbstract (NewName BoundName) Name #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewName BoundName -> ScopeM Name #
ToAbstract c a => ToAbstract [c] [a] #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: [c] -> ScopeM [a] #
ToAbstract [Declaration] [Declaration] #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: [Declaration0] -> ScopeM [Declaration] #
ToAbstract c a => ToAbstract (Maybe c) (Maybe a) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Maybe c -> ScopeM (Maybe a) #
ToAbstract c a => ToAbstract (Arg c) (Arg a) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Arg c -> ScopeM (Arg a) #
ToAbstract c a => ToAbstract (WithHiding c) (WithHiding a) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: WithHiding c -> ScopeM (WithHiding a) #
ToAbstract c a => ToAbstract (FieldAssignment' c) (FieldAssignment' a) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: FieldAssignment' c -> ScopeM (FieldAssignment' a) #
ToAbstract (Pattern' Expr) (Pattern' Expr) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Pattern' Expr0 -> ScopeM (Pattern' Expr) #
ToAbstract (LHSCore' Expr) (LHSCore' Expr) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LHSCore' Expr0 -> ScopeM (LHSCore' Expr) #
(ToAbstract c1 a1, ToAbstract c2 a2) => ToAbstract (Either c1 c2) (Either a1 a2) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Either c1 c2 -> ScopeM (Either a1 a2) #
(ToAbstract c1 a1, ToAbstract c2 a2) => ToAbstract (c1, c2) (a1, a2) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: (c1, c2) -> ScopeM (a1, a2) #
ToAbstract c a => ToAbstract (Named name c) (Named name a) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: Named name c -> ScopeM (Named name a) #
(ToAbstract c1 a1, ToAbstract c2 a2, ToAbstract c3 a3) => ToAbstract (c1, c2, c3) (a1, a2, a3) #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: (c1, c2, c3) -> ScopeM (a1, a2, a3) #

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

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

concreteToAbstract_ :: ToAbstract c a => c -> ScopeM a #

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

newtype NewModuleQName #

Constructors

NewModuleQName QName

Instances

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

newtype OldName a #

Constructors

OldName a

Instances

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

data TopLevel a #

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 #	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 #

data TopLevelInfo #

Constructors

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

Instances

ToAbstract (TopLevel [Declaration]) TopLevelInfo #	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 #

topLevelModuleName :: TopLevelInfo -> ModuleName #

The top-level module name.

data AbstractRHS #

Instances

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

data NewModuleName #

Instances

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

data OldModuleName #

Instances

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

data NewName a #

Instances

ToAbstract (NewName Name) Name #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewName Name0 -> ScopeM Name #
ToAbstract (NewName BoundName) Name #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: NewName BoundName -> ScopeM Name #

data OldQName #

Instances

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

data LeftHandSide #

Instances

ToAbstract LeftHandSide LHS #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LeftHandSide -> ScopeM LHS #

data RightHandSide #

Instances

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

data PatName #

Instances

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

data APatName #

Instances

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

data LetDef #

Instances

ToAbstract LetDef [LetBinding] #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LetDef -> ScopeM [LetBinding] #

data LetDefs #

Instances

ToAbstract LetDefs [LetBinding] #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Methods toAbstract :: LetDefs -> ScopeM [LetBinding] #