Safe Haskell	Safe-Inferred
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 c where
- type AbsOfCon c
- toAbstract :: c -> ScopeM (AbsOfCon c)
localToAbstract :: ToAbstract c => c -> (AbsOfCon c -> ScopeM b) -> ScopeM b
concreteToAbstract_ :: ToAbstract c => c -> ScopeM (AbsOfCon c)
concreteToAbstract :: ToAbstract c => ScopeInfo -> c -> ScopeM (AbsOfCon c)
newtype NewModuleQName = NewModuleQName QName
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
importPrimitives :: ScopeM [Declaration]
checkCohesionAttributes :: CohesionAttributes -> ScopeM ()

Documentation

class ToAbstract c where Source #

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

Associated Types

type AbsOfCon c Source #

Methods

toAbstract :: c -> ScopeM (AbsOfCon c) Source #

Instances

Instances details

ToAbstract Expr Source #	Scope check an expression.
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon Expr Source # Methods toAbstract :: Expr -> ScopeM (AbsOfCon Expr) Source #
ToAbstract HoleContent Source #	Content of interaction hole.
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon HoleContent Source # Methods toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent) Source #
ToAbstract LHSCore Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon LHSCore Source # Methods toAbstract :: LHSCore -> ScopeM (AbsOfCon LHSCore) Source #
ToAbstract LamBinding Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon LamBinding Source # Methods toAbstract :: LamBinding -> ScopeM (AbsOfCon LamBinding) Source #
ToAbstract ModuleAssignment Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon ModuleAssignment Source # Methods toAbstract :: ModuleAssignment -> ScopeM (AbsOfCon ModuleAssignment) Source #
ToAbstract Pattern Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon Pattern Source # Methods toAbstract :: Pattern -> ScopeM (AbsOfCon Pattern) Source #
ToAbstract Pragma Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon Pragma Source # Methods toAbstract :: Pragma -> ScopeM (AbsOfCon Pragma) Source #
ToAbstract RHS Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon RHS Source # Methods toAbstract :: RHS -> ScopeM (AbsOfCon RHS) Source #
ToAbstract RewriteEqn Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon RewriteEqn Source # Methods toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn) Source #
ToAbstract TypedBinding Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon TypedBinding Source # Methods toAbstract :: TypedBinding -> ScopeM (AbsOfCon TypedBinding) Source #
ToAbstract Clause Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon Clause Source # Methods toAbstract :: Clause -> ScopeM (AbsOfCon Clause) Source #
ToAbstract NiceDeclaration Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon NiceDeclaration Source # Methods toAbstract :: NiceDeclaration -> ScopeM (AbsOfCon NiceDeclaration) Source #
ToAbstract AbstractRHS Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon AbstractRHS Source # Methods toAbstract :: AbstractRHS -> ScopeM (AbsOfCon AbstractRHS) Source #
ToAbstract NewModuleName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon NewModuleName Source # Methods toAbstract :: NewModuleName -> ScopeM (AbsOfCon NewModuleName) Source #
ToAbstract NewModuleQName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon NewModuleQName Source # Methods toAbstract :: NewModuleQName -> ScopeM (AbsOfCon NewModuleQName) Source #
ToAbstract OldModuleName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon OldModuleName Source # Methods toAbstract :: OldModuleName -> ScopeM (AbsOfCon OldModuleName) Source #
ToAbstract OldQName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon OldQName Source # Methods toAbstract :: OldQName -> ScopeM (AbsOfCon OldQName) Source #
ToAbstract PatName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon PatName Source # Methods toAbstract :: PatName -> ScopeM (AbsOfCon PatName) Source #
ToAbstract () Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon () Source # Methods toAbstract :: () -> ScopeM (AbsOfCon ()) Source #
ToAbstract (LHSCore' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (LHSCore' Expr) Source # Methods toAbstract :: LHSCore' Expr -> ScopeM (AbsOfCon (LHSCore' Expr)) Source #
ToAbstract (Pattern' Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Pattern' Expr) Source # Methods toAbstract :: Pattern' Expr -> ScopeM (AbsOfCon (Pattern' Expr)) Source #
ToAbstract c => ToAbstract (Arg c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Arg c) Source # Methods toAbstract :: Arg c -> ScopeM (AbsOfCon (Arg c)) Source #
ToAbstract c => ToAbstract (WithHiding c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (WithHiding c) Source # Methods toAbstract :: WithHiding c -> ScopeM (AbsOfCon (WithHiding c)) Source #
ToAbstract (Binder' (NewName BoundName)) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Binder' (NewName BoundName)) Source # Methods toAbstract :: Binder' (NewName BoundName) -> ScopeM (AbsOfCon (Binder' (NewName BoundName))) Source #
ToAbstract c => ToAbstract (FieldAssignment' c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (FieldAssignment' c) Source # Methods toAbstract :: FieldAssignment' c -> ScopeM (AbsOfCon (FieldAssignment' c)) Source #
ToAbstract (NewName BoundName) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (NewName BoundName) Source # Methods toAbstract :: NewName BoundName -> ScopeM (AbsOfCon (NewName BoundName)) Source #
ToAbstract (NewName Name) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (NewName Name) Source # Methods toAbstract :: NewName Name -> ScopeM (AbsOfCon (NewName Name)) Source #
ToAbstract (TopLevel [Declaration]) 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 Associated Types type AbsOfCon (TopLevel [Declaration]) Source # Methods toAbstract :: TopLevel [Declaration] -> ScopeM (AbsOfCon (TopLevel [Declaration])) Source #
ToAbstract c => ToAbstract (List1 c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (List1 c) Source # Methods toAbstract :: List1 c -> ScopeM (AbsOfCon (List1 c)) Source #
ToAbstract c => ToAbstract (Maybe c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Maybe c) Source # Methods toAbstract :: Maybe c -> ScopeM (AbsOfCon (Maybe c)) Source #
ToAbstract c => ToAbstract [c] Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon [c] Source # Methods toAbstract :: [c] -> ScopeM (AbsOfCon [c]) Source #
ToAbstract c => ToAbstract (Named name c) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Named name c) Source # Methods toAbstract :: Named name c -> ScopeM (AbsOfCon (Named name c)) Source #
(ToAbstract c1, ToAbstract c2) => ToAbstract (Either c1 c2) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Either c1 c2) Source # Methods toAbstract :: Either c1 c2 -> ScopeM (AbsOfCon (Either c1 c2)) Source #
(ToAbstract c1, ToAbstract c2) => ToAbstract (c1, c2) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (c1, c2) Source # Methods toAbstract :: (c1, c2) -> ScopeM (AbsOfCon (c1, c2)) Source #
(ToAbstract c1, ToAbstract c2, ToAbstract c3) => ToAbstract (c1, c2, c3) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (c1, c2, c3) Source # Methods toAbstract :: (c1, c2, c3) -> ScopeM (AbsOfCon (c1, c2, c3)) Source #
ToAbstract (RewriteEqn' () BindName Pattern Expr) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # Methods toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source #

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

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

concreteToAbstract_ :: ToAbstract c => c -> ScopeM (AbsOfCon c) Source #

concreteToAbstract :: ToAbstract c => ScopeInfo -> c -> ScopeM (AbsOfCon c) Source #

newtype NewModuleQName Source #

Constructors

NewModuleQName QName

Instances

Instances details

ToAbstract NewModuleQName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon NewModuleQName Source # Methods toAbstract :: NewModuleQName -> ScopeM (AbsOfCon NewModuleQName) Source #
type AbsOfCon NewModuleQName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon NewModuleQName = ModuleName

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

Instances details

ToAbstract (TopLevel [Declaration]) 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 Associated Types type AbsOfCon (TopLevel [Declaration]) Source # Methods toAbstract :: TopLevel [Declaration] -> ScopeM (AbsOfCon (TopLevel [Declaration])) Source #
type AbsOfCon (TopLevel [Declaration]) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (TopLevel [Declaration]) = TopLevelInfo

data TopLevelInfo Source #

Constructors

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

topLevelModuleName :: TopLevelInfo -> ModuleName Source #

The top-level module name.

data AbstractRHS Source #

Instances

Instances details

ToAbstract AbstractRHS Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon AbstractRHS Source # Methods toAbstract :: AbstractRHS -> ScopeM (AbsOfCon AbstractRHS) Source #
type AbsOfCon AbstractRHS Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon AbstractRHS = RHS

data NewModuleName Source #

Instances

Instances details

ToAbstract NewModuleName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon NewModuleName Source # Methods toAbstract :: NewModuleName -> ScopeM (AbsOfCon NewModuleName) Source #
type AbsOfCon NewModuleName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon NewModuleName = ModuleName

data OldModuleName Source #

Instances

Instances details

ToAbstract OldModuleName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon OldModuleName Source # Methods toAbstract :: OldModuleName -> ScopeM (AbsOfCon OldModuleName) Source #
type AbsOfCon OldModuleName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon OldModuleName = ModuleName

data NewName a Source #

Instances

Instances details

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)) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (Binder' (NewName BoundName)) Source # Methods toAbstract :: Binder' (NewName BoundName) -> ScopeM (AbsOfCon (Binder' (NewName BoundName))) Source #
ToAbstract (NewName BoundName) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (NewName BoundName) Source # Methods toAbstract :: NewName BoundName -> ScopeM (AbsOfCon (NewName BoundName)) Source #
ToAbstract (NewName Name) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon (NewName Name) Source # Methods toAbstract :: NewName Name -> ScopeM (AbsOfCon (NewName Name)) Source #
type AbsOfCon (Binder' (NewName BoundName)) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Binder' (NewName BoundName)) = Binder
type AbsOfCon (NewName BoundName) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (NewName BoundName) = BindName
type AbsOfCon (NewName Name) Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (NewName Name) = Name

data OldQName Source #

Instances

Instances details

ToAbstract OldQName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon OldQName Source # Methods toAbstract :: OldQName -> ScopeM (AbsOfCon OldQName) Source #
type AbsOfCon OldQName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon OldQName = Expr

data PatName Source #

Instances

Instances details

ToAbstract PatName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract Associated Types type AbsOfCon PatName Source # Methods toAbstract :: PatName -> ScopeM (AbsOfCon PatName) Source #
type AbsOfCon PatName Source #
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon PatName = APatName

data APatName Source #

importPrimitives :: ScopeM [Declaration] Source #

Declaration open import Agda.Primitive using (Set; Prop) when optImportSorts.

checkCohesionAttributes :: CohesionAttributes -> ScopeM () Source #

Raises an error if the list of cohesion attributes is non-empty and cohesion modalities are not supported.