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

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
  - toAbstract :: concrete -> ScopeM abstract
- 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

# Documentation

class ToAbstract concrete abstract | concrete -> abstract where Source #

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

Methods

toAbstract :: concrete -> ScopeM abstract Source #

Instances

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

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

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

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

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

newtype NewModuleQName Source #

Constructors

NewModuleQName QName |

Instances

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

newtype OldName a Source #

Constructors

OldName a |

Instances

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

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

ToAbstract (TopLevel [Declaration]) TopLevelInfo 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 Methods toAbstract :: TopLevel [Declaration] -> ScopeM TopLevelInfo Source #

data TopLevelInfo Source #

Constructors

TopLevelInfo |

Fields

- topLevelDecls :: [Declaration]
- topLevelScope :: ScopeInfo

  as seen from inside the module

Instances

ToAbstract (TopLevel [Declaration]) TopLevelInfo 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 Methods toAbstract :: TopLevel [Declaration] -> ScopeM TopLevelInfo Source #

topLevelModuleName :: TopLevelInfo -> ModuleName Source #

The top-level module name.

data AbstractRHS Source #

Instances

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

data NewModuleName Source #

Instances

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

data OldModuleName Source #

Instances

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

data NewName a Source #

Instances

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

data OldQName Source #

Instances

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

data LeftHandSide Source #

Instances

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

data RightHandSide Source #

Instances

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

data PatName Source #

Instances

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

data APatName Source #

Instances

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