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 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)
data TopLevel a = TopLevel {
- topLevelSourceFile :: SourceFile
- topLevelExpectedName :: TopLevelModuleName
- topLevelTheThing :: a
}
data TopLevelInfo = TopLevelInfo {
- topLevelDecls :: [Declaration]
- topLevelScope :: ScopeInfo
}
topLevelModuleName :: TopLevelInfo -> ModuleName
importPrimitives :: ScopeM [Declaration]
checkAttributes :: Attributes -> 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
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon Expr = Expr

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
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon HoleContent = HoleContent

Methods

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

ToAbstract LHSCore Source #

Scope-check a LHSCore not of a DisplayForm.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LHSCore
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon LHSCore = LHSCore' Expr

Methods

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

ToAbstract LamBinding Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon LamBinding = Maybe LamBinding

Methods

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

ToAbstract ModuleAssignment Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon ModuleAssignment
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon ModuleAssignment = (ModuleName, Maybe LetBinding)

Methods

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

ToAbstract Pattern Source #

Scope check a Pattern not belonging to a DisplayForm.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pattern
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon Pattern = Pattern' Expr

Methods

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

ToAbstract Pragma Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pragma
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon Pragma = [Pragma]

Methods

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

ToAbstract RHS Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RHS
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon RHS

Methods

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

ToAbstract RewriteEqn Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RewriteEqn
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon RewriteEqn = RewriteEqn' () BindName Pattern Expr

Methods

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

ToAbstract TypedBinding Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon TypedBinding
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon TypedBinding = Maybe TypedBinding

Methods

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

ToAbstract Clause Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Clause
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon Clause = Clause

Methods

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

ToAbstract NiceDeclaration Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon NiceDeclaration
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon NiceDeclaration = Declaration

Methods

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

ToAbstract () Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon ()
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon () = ()

Methods

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

ToAbstract (LHSCore' Expr) Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (LHSCore' Expr)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (LHSCore' Expr) = LHSCore' Expr

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)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Pattern' Expr) = Pattern' Expr

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)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Arg c) = Arg (AbsOfCon c)

Methods

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

ToAbstract c => ToAbstract (Ranged c) Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Ranged c)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Ranged c) = Ranged (AbsOfCon c)

Methods

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

ToAbstract c => ToAbstract (WithHiding c) Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (WithHiding c)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (WithHiding c) = WithHiding (AbsOfCon c)

Methods

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

ToAbstract c => ToAbstract (FieldAssignment' c) Source #

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (FieldAssignment' c)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (FieldAssignment' c) = FieldAssignment' (AbsOfCon c)

Methods

toAbstract :: FieldAssignment' c -> ScopeM (AbsOfCon (FieldAssignment' c)) 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])
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (TopLevel [Declaration]) = TopLevelInfo

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)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (List1 c) = List1 (AbsOfCon c)

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)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Maybe c) = Maybe (AbsOfCon c)

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]
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon [c] = [AbsOfCon c]

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)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Named name c) = Named name (AbsOfCon c)

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)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (Either c1 c2) = Either (AbsOfCon c1) (AbsOfCon c2)

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)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (c1, c2) = (AbsOfCon c1, AbsOfCon c2)

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)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (c1, c2, c3) = (AbsOfCon c1, AbsOfCon c2, AbsOfCon c3)

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)
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (RewriteEqn' () BindName Pattern Expr) = RewriteEqn

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 #

data TopLevel a Source #

Temporary data type to scope check a file.

Constructors

TopLevel
Fields topLevelSourceFile :: SourceFile The file 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])
Instance details Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (TopLevel [Declaration]) = TopLevelInfo

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.

importPrimitives :: ScopeM [Declaration] Source #

Declaration open import Agda.Primitive using (Set) when optImportSorts. Prop is added when optProp, and SSet when optTwoLevel.

checkAttributes :: Attributes -> ScopeM () Source #

Raises an error if the list of attributes contains an unsupported attribute.