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

Safe Haskell | None

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 = OldName Name
- newtype TopLevel a = TopLevel a
- data TopLevelInfo = TopLevelInfo {
  - topLevelDecls :: [Declaration]
  - outsideScope :: ScopeInfo
  - insideScope :: ScopeInfo
  }
- topLevelModuleName :: TopLevelInfo -> ModuleName
- data AbstractRHS
- data NewModuleName
- data OldModuleName
- data NewName a
- data OldQName
- data LeftHandSide
- data RightHandSide
- data PatName
- data APatName
- data LetDef
- data LetDefs

# Documentation

class ToAbstract concrete abstract | concrete -> abstract where

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

Methods

toAbstract :: concrete -> ScopeM abstract

Instances

ToAbstract RHS AbstractRHS |
ToAbstract TypedBinding TypedBinding |
ToAbstract TypedBindings TypedBindings |
ToAbstract LamBinding LamBinding |
ToAbstract Expr Expr |
ToAbstract Clause Clause |
ToAbstract NiceDeclaration Declaration |
ToAbstract LeftHandSide LHS |
ToAbstract AbstractRHS RHS |
ToAbstract RightHandSide AbstractRHS |
ToAbstract OldModuleName ModuleName |
ToAbstract NewModuleQName ModuleName |
ToAbstract NewModuleName ModuleName |
ToAbstract PatName APatName |
ToAbstract OldName QName |
ToAbstract OldQName Expr |
ToAbstract Pragma [Pragma] |
ToAbstract LHSCore (LHSCore' Expr) |
ToAbstract Pattern (Pattern' Expr) |
ToAbstract LetDef [LetBinding] |
ToAbstract LetDefs [LetBinding] |
ToAbstract (TopLevel [Declaration]) TopLevelInfo |
ToAbstract (NewName Name) Name |
ToAbstract (NewName BoundName) Name |
ToAbstract c a => ToAbstract [c] [a] |
ToAbstract [Declaration] [Declaration] |
ToAbstract c a => ToAbstract (Maybe c) (Maybe a) |
ToAbstract c a => ToAbstract (Arg c) (Arg a) |
ToAbstract (Pattern' Expr) (Pattern' Expr) |
ToAbstract (LHSCore' Expr) (LHSCore' Expr) |
(ToAbstract c1 a1, ToAbstract c2 a2) => ToAbstract (c1, c2) (a1, a2) |
ToAbstract c a => ToAbstract (Named name c) (Named name a) |
(ToAbstract c1 a1, ToAbstract c2 a2, ToAbstract c3 a3) => ToAbstract (c1, c2, c3) (a1, a2, a3) |

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

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

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

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

newtype NewModuleQName

Constructors

NewModuleQName QName |

Instances

ToAbstract NewModuleQName ModuleName |

newtype OldName

Constructors

OldName Name |

Instances

ToAbstract OldName QName |

newtype TopLevel a

Constructors

TopLevel a |

Instances

ToAbstract (TopLevel [Declaration]) TopLevelInfo |

data TopLevelInfo

Constructors

TopLevelInfo |

Fields

topLevelDecls :: [Declaration]
outsideScope :: ScopeInfo
insideScope :: ScopeInfo

Instances

ToAbstract (TopLevel [Declaration]) TopLevelInfo |

topLevelModuleName :: TopLevelInfo -> ModuleName

The top-level module name.

data AbstractRHS

Instances

ToAbstract RHS AbstractRHS |
ToAbstract AbstractRHS RHS |
ToAbstract RightHandSide AbstractRHS |

data NewModuleName

Instances

ToAbstract NewModuleName ModuleName |

data OldModuleName

Instances

ToAbstract OldModuleName ModuleName |

data NewName a

Instances

ToAbstract (NewName Name) Name |
ToAbstract (NewName BoundName) Name |

data OldQName

Instances

ToAbstract OldQName Expr |

data LeftHandSide

Instances

ToAbstract LeftHandSide LHS |

data RightHandSide

Instances

ToAbstract RightHandSide AbstractRHS |

data PatName

Instances

ToAbstract PatName APatName |

data APatName

Instances

ToAbstract PatName APatName |

data LetDef

Instances

ToAbstract LetDef [LetBinding] |

data LetDefs

Instances

ToAbstract LetDefs [LetBinding] |