Safe Haskell | None |
---|---|
Language | Haskell2010 |
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 {}
- data TopLevelInfo = TopLevelInfo {}
- 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.
toAbstract :: c -> ScopeM (AbsOfCon c) Source #
Instances
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 #
Instances
ToAbstract NewModuleQName Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon NewModuleQName Source # | |
type AbsOfCon NewModuleQName Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
Temporary data type to scope check a file.
TopLevel | |
|
Instances
ToAbstract (TopLevel [Declaration]) Source # | Top-level declarations are always
|
Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon (TopLevel [Declaration]) Source # toAbstract :: TopLevel [Declaration] -> ScopeM (AbsOfCon (TopLevel [Declaration])) Source # | |
type AbsOfCon (TopLevel [Declaration]) Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
data TopLevelInfo Source #
TopLevelInfo | |
|
topLevelModuleName :: TopLevelInfo -> ModuleName Source #
The top-level module name.
data AbstractRHS Source #
Instances
ToAbstract AbstractRHS Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon AbstractRHS Source # toAbstract :: AbstractRHS -> ScopeM (AbsOfCon AbstractRHS) Source # | |
type AbsOfCon AbstractRHS Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
data NewModuleName Source #
Instances
ToAbstract NewModuleName Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon NewModuleName Source # | |
type AbsOfCon NewModuleName Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
data OldModuleName Source #
Instances
ToAbstract OldModuleName Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract type AbsOfCon OldModuleName Source # | |
type AbsOfCon OldModuleName Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
Instances
Functor NewName Source # | |
ToAbstract (Binder' (NewName BoundName)) Source # | |
ToAbstract (NewName Name) Source # | |
ToAbstract (NewName BoundName) Source # | |
type AbsOfCon (Binder' (NewName BoundName)) Source # | |
type AbsOfCon (NewName Name) Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract | |
type AbsOfCon (NewName BoundName) Source # | |
Defined in Agda.Syntax.Translation.ConcreteToAbstract |
Instances
Instances
importPrimitives :: ScopeM [Declaration] Source #
Declaration open import Agda.Primitive using (Set; Prop)
when optImportSorts
.