Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

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]

# 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 Source # (<$) :: a -> NewName b -> NewName a 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 (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`.