Agda-2.8.0: 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 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.