ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Translation.ConcreteToAbstract

Translation from Agda.Syntax.Concrete to Agda.Syntax.Abstract. Involves scope analysis, figuring out infix operator precedences and tidying up definitions.

10 types
1 class
6 values

PackageAgda-2.7.0.1
Exports17
LanguageHaskell2010
LicenceMIT
SourceConcreteToAbstract.hs

classclass ToAbstract c where

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

Associated types

type family AbsOfCon c

Methods

toAbstract :: c -> ScopeM (AbsOfCon c)

Instances50ToAbstract, …

ToAbstract ExprDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
Scope check an expression.
ToAbstract HoleContentDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
Content of interaction hole.
ToAbstract LHSCoreDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract LamBindingDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract ModuleAssignmentDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract PatternDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract PragmaDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract RHSDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract RewriteEqnDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract TypedBindingDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract ClauseDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract NiceDeclarationDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract AbstractRHSDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract DataConstrDeclDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract DeclarationsDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract GenTelDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract GenTelAndTypeDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract LeftHandSideDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract LetDefDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract LetDefsDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract MaybeOldQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract NewModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract NewModuleQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract OldModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract OldQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract PatNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract RecordConstructorTypeDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract ResolveQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract RightHandSideDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract ()Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract (LHSCore' Expr)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract (Pattern' Expr)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract (Binder' (NewName BoundName))Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract (NewName BoundName)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract (NewName Name)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract (TopLevel [Declaration])Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
Top-level declarations are always (import|open)* -- a bunch of possibly opened imports module ThisModule ... -- the top-level module of this file
ToAbstract (WithHidingInfo Pattern)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
Hiding info is only used for pattern variables.
ToAbstract c => ToAbstract (Arg c)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract c => ToAbstract (Ranged c)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract c => ToAbstract (WithHiding c)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract c => ToAbstract (FieldAssignment' c)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract c => ToAbstract (List1 c)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract c => ToAbstract (Maybe c)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract c => ToAbstract [c]Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToQName a => ToAbstract (OldName a)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract c => ToAbstract (Named name c)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
(ToAbstract c1, ToAbstract c2) => ToAbstract (Either c1 c2)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
(ToAbstract c1, ToAbstract c2) => ToAbstract (c1, c2)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
(ToAbstract c1, ToAbstract c2, ToAbstract c3) => ToAbstract (c1, c2, c3)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract (RewriteEqn' () BindName Pattern Expr)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract

valuelocalToAbstract :: ToAbstract c => c -> (AbsOfCon c -> ScopeM b) -> ScopeM b

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

valueconcreteToAbstract_ :: ToAbstract c => c -> ScopeM (AbsOfCon c)

valueconcreteToAbstract :: ToAbstract c => ScopeInfo -> c -> ScopeM (AbsOfCon c)

newtypenewtype NewModuleQName

Constructors

NewModuleQName QName

Instances2ToAbstract, AbsOfCon

ToAbstract NewModuleQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon NewModuleQName = ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract

datadata TopLevel a

Temporary data type to scope check a file.

Constructors

TopLevel
- 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.

Instances2ToAbstract, AbsOfCon

ToAbstract (TopLevel [Declaration])Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
Top-level declarations are always (import|open)* -- a bunch of possibly opened imports module ThisModule ... -- the top-level module of this file
type AbsOfCon (TopLevel [Declaration]) = TopLevelInfoDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract

datadata TopLevelInfo

Constructors

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

valuetopLevelModuleName :: TopLevelInfo -> ModuleName

The top-level module name.

datadata AbstractRHS

Instances2ToAbstract, AbsOfCon

ToAbstract AbstractRHSDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon AbstractRHS = RHSDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract

newtypenewtype NewModuleName

Instances2ToAbstract, AbsOfCon

ToAbstract NewModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon NewModuleName = ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract

newtypenewtype OldModuleName

Instances2ToAbstract, AbsOfCon

ToAbstract OldModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon OldModuleName = ModuleNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract

datadata NewName a

Instances7Functor, ToAbstract, AbsOfCon, …

Functor NewNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract (Binder' (NewName BoundName))Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract (NewName BoundName)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
ToAbstract (NewName Name)Defined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon (Binder' (NewName BoundName)) = BinderDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon (NewName BoundName) = BindNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon (NewName Name) = NameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract

datadata OldQName

Instances2ToAbstract, AbsOfCon

ToAbstract OldQNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon OldQName = ExprDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract

datadata PatName

Instances2ToAbstract, AbsOfCon

ToAbstract PatNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract
type AbsOfCon PatName = APatNameDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.ConcreteToAbstract

datadata APatName

valueimportPrimitives :: ScopeM [Declaration]

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

valuecheckAttributes :: Attributes -> ScopeM ()

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