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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Haskell.Syntax

Contents

- Modules
- Declarations
- Expressions
- Names

Description

ASTs for subset of GHC Haskell syntax.

Synopsis

- data Module = Module ModuleName [ModulePragma] [ImportDecl] [Decl]
- data ModulePragma
  - = LanguagePragma [Name]
  - | OtherPragma String
- data ImportDecl = ImportDecl {
  - importModule :: ModuleName
  - importQualified :: Bool
  - importSpecs :: Maybe (Bool, [ImportSpec])
  }
- data ImportSpec = IVar Name
- data Decl
  - = TypeDecl Name [TyVarBind] Type
  - | DataDecl DataOrNew Name [TyVarBind] [ConDecl] [Deriving]
  - | TypeSig [Name] Type
  - | FunBind [Match]
  - | LocalBind Strictness Name Rhs
  - | PatSyn Pat Pat
  - | FakeDecl String
  - | Comment String
- data DataOrNew
  - = DataType
  - | NewType
- data ConDecl = ConDecl Name [(Maybe Strictness, Type)]
- data Strictness
  - = Lazy
  - | Strict
- type Deriving = (QName, [Type])
- data Binds = BDecls [Decl]
- data Rhs
  - = UnGuardedRhs Exp
  - | GuardedRhss [GuardedRhs]
- data GuardedRhs = GuardedRhs [Stmt] Exp
- data Match = Match Name [Pat] Rhs (Maybe Binds)
- data Type
  - = TyForall [TyVarBind] Type
  - | TyFun Type Type
  - | TyCon QName
  - | TyVar Name
  - | TyApp Type Type
  - | FakeType String
- data Pat
  - = PVar Name
  - | PLit Literal
  - | PAsPat Name Pat
  - | PWildCard
  - | PBangPat Pat
  - | PApp QName [Pat]
  - | PatTypeSig Pat Type
  - | PIrrPat Pat
- data Stmt
  - = Qualifier Exp
  - | Generator Pat Exp
- data Exp
  - = Var QName
  - | Con QName
  - | Lit Literal
  - | InfixApp Exp QOp Exp
  - | Ann Exp Type
  - | App Exp Exp
  - | Lambda [Pat] Exp
  - | Let Binds Exp
  - | If Exp Exp Exp
  - | Case Exp [Alt]
  - | ExpTypeSig Exp Type
  - | NegApp Exp
  - | FakeExp String
- data Alt = Alt Pat Rhs (Maybe Binds)
- data Literal
  - = Int Integer
  - | Frac Rational
  - | Char Char
  - | String Text
- data ModuleName = ModuleName String
- data QName
  - = Qual ModuleName Name
  - | UnQual Name
- data Name
  - = Ident String
  - | Symbol String
- data QOp = QVarOp QName
- data TyVarBind = UnkindedVar Name
- unit_con :: Exp

# Modules

data Module Source #

Constructors

Module ModuleName [ModulePragma] [ImportDecl] [Decl] |

#### Instances

Instances details

MakeStrict Module Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Strict Methods makeStrict :: Module -> Module Source #
Pretty Module Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Module -> Doc Source # prettyPrec :: Int -> Module -> Doc Source # prettyList :: [Module] -> Doc Source #

data ModulePragma Source #

Constructors

LanguagePragma [Name] |
OtherPragma String | Unstructured pragma (Andreas, 2017-08-23, issue #2712).

#### Instances

Instances details

Pretty ModulePragma Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: ModulePragma -> Doc Source # prettyPrec :: Int -> ModulePragma -> Doc Source # prettyList :: [ModulePragma] -> Doc Source #

data ImportDecl Source #

Constructors

ImportDecl |

Fields

- importModule :: ModuleName
- importQualified :: Bool
- importSpecs :: Maybe (Bool, [ImportSpec])

#### Instances

Instances details

Pretty ImportDecl Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: ImportDecl -> Doc Source # prettyPrec :: Int -> ImportDecl -> Doc Source # prettyList :: [ImportDecl] -> Doc Source #

data ImportSpec Source #

Constructors

IVar Name |

#### Instances

Instances details

Pretty ImportSpec Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: ImportSpec -> Doc Source # prettyPrec :: Int -> ImportSpec -> Doc Source # prettyList :: [ImportSpec] -> Doc Source #

# Declarations

data Decl Source #

Constructors

TypeDecl Name [TyVarBind] Type |
DataDecl DataOrNew Name [TyVarBind] [ConDecl] [Deriving] |
TypeSig [Name] Type |
FunBind [Match] | Should not be used when `LocalBind` could be used.
LocalBind Strictness Name Rhs | Should only be used in `let` or `where`.
PatSyn Pat Pat |
FakeDecl String |
Comment String |

#### Instances

Instances details

MakeStrict Decl Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Strict Methods makeStrict :: Decl -> Decl Source #
Pretty Decl Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Decl -> Doc Source # prettyPrec :: Int -> Decl -> Doc Source # prettyList :: [Decl] -> Doc Source #
Eq Decl Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: Decl -> Decl -> Bool Source # (/=) :: Decl -> Decl -> Bool Source #

data DataOrNew Source #

Constructors

DataType |
NewType |

#### Instances

Instances details

Pretty DataOrNew Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: DataOrNew -> Doc Source # prettyPrec :: Int -> DataOrNew -> Doc Source # prettyList :: [DataOrNew] -> Doc Source #
Eq DataOrNew Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: DataOrNew -> DataOrNew -> Bool Source # (/=) :: DataOrNew -> DataOrNew -> Bool Source #

data ConDecl Source #

Constructors

ConDecl Name [(Maybe Strictness, Type)] |

#### Instances

Instances details

Pretty ConDecl Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: ConDecl -> Doc Source # prettyPrec :: Int -> ConDecl -> Doc Source # prettyList :: [ConDecl] -> Doc Source #
Eq ConDecl Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: ConDecl -> ConDecl -> Bool Source # (/=) :: ConDecl -> ConDecl -> Bool Source #

data Strictness Source #

Constructors

Lazy |
Strict |

#### Instances

Instances details

Pretty Strictness Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Strictness -> Doc Source # prettyPrec :: Int -> Strictness -> Doc Source # prettyList :: [Strictness] -> Doc Source #
Eq Strictness Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: Strictness -> Strictness -> Bool Source # (/=) :: Strictness -> Strictness -> Bool Source #

type Deriving = (QName, [Type]) Source #

data Binds Source #

Constructors

BDecls [Decl] |

#### Instances

Instances details

MakeStrict Binds Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Strict Methods makeStrict :: Binds -> Binds Source #
Pretty Binds Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Binds -> Doc Source # prettyPrec :: Int -> Binds -> Doc Source # prettyList :: [Binds] -> Doc Source #
Eq Binds Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: Binds -> Binds -> Bool Source # (/=) :: Binds -> Binds -> Bool Source #

data Rhs Source #

Constructors

UnGuardedRhs Exp |
GuardedRhss [GuardedRhs] |

#### Instances

Instances details

MakeStrict Rhs Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Strict Methods makeStrict :: Rhs -> Rhs Source #
Eq Rhs Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: Rhs -> Rhs -> Bool Source # (/=) :: Rhs -> Rhs -> Bool Source #

data GuardedRhs Source #

Constructors

GuardedRhs [Stmt] Exp |

#### Instances

Instances details

MakeStrict GuardedRhs Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Strict Methods makeStrict :: GuardedRhs -> GuardedRhs Source #
Eq GuardedRhs Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: GuardedRhs -> GuardedRhs -> Bool Source # (/=) :: GuardedRhs -> GuardedRhs -> Bool Source #

data Match Source #

Constructors

Match Name [Pat] Rhs (Maybe Binds) |

#### Instances

Instances details

MakeStrict Match Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Strict Methods makeStrict :: Match -> Match Source #
Pretty Match Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Match -> Doc Source # prettyPrec :: Int -> Match -> Doc Source # prettyList :: [Match] -> Doc Source #
Eq Match Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: Match -> Match -> Bool Source # (/=) :: Match -> Match -> Bool Source #

# Expressions

data Type Source #

Constructors

TyForall [TyVarBind] Type |
TyFun Type Type |
TyCon QName |
TyVar Name |
TyApp Type Type |
FakeType String |

#### Instances

Instances details

Pretty Type Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Type -> Doc Source # prettyPrec :: Int -> Type -> Doc Source # prettyList :: [Type] -> Doc Source #
Eq Type Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: Type -> Type -> Bool Source # (/=) :: Type -> Type -> Bool Source #

data Pat Source #

Constructors

PVar Name |
PLit Literal |
PAsPat Name Pat |
PWildCard |
PBangPat Pat |
PApp QName [Pat] |
PatTypeSig Pat Type |
PIrrPat Pat |

#### Instances

Instances details

MakeStrict Pat Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Strict Methods makeStrict :: Pat -> Pat Source #
Pretty Pat Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Pat -> Doc Source # prettyPrec :: Int -> Pat -> Doc Source # prettyList :: [Pat] -> Doc Source #
Eq Pat Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: Pat -> Pat -> Bool Source # (/=) :: Pat -> Pat -> Bool Source #

data Stmt Source #

Constructors

Qualifier Exp |
Generator Pat Exp |

#### Instances

Instances details

MakeStrict Stmt Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Strict Methods makeStrict :: Stmt -> Stmt Source #
Pretty Stmt Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Stmt -> Doc Source # prettyPrec :: Int -> Stmt -> Doc Source # prettyList :: [Stmt] -> Doc Source #
Eq Stmt Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: Stmt -> Stmt -> Bool Source # (/=) :: Stmt -> Stmt -> Bool Source #

data Exp Source #

Constructors

Var QName |
Con QName |
Lit Literal |
InfixApp Exp QOp Exp |
Ann Exp Type |
App Exp Exp |
Lambda [Pat] Exp |
Let Binds Exp |
If Exp Exp Exp |
Case Exp [Alt] |
ExpTypeSig Exp Type |
NegApp Exp |
FakeExp String |

#### Instances

Instances details

MakeStrict Exp Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Strict Methods makeStrict :: Exp -> Exp Source #
Pretty Exp Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Exp -> Doc Source # prettyPrec :: Int -> Exp -> Doc Source # prettyList :: [Exp] -> Doc Source #
Eq Exp Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: Exp -> Exp -> Bool Source # (/=) :: Exp -> Exp -> Bool Source #

data Alt Source #

Constructors

Alt Pat Rhs (Maybe Binds) |

#### Instances

Instances details

MakeStrict Alt Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Strict Methods makeStrict :: Alt -> Alt Source #
Pretty Alt Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Alt -> Doc Source # prettyPrec :: Int -> Alt -> Doc Source # prettyList :: [Alt] -> Doc Source #
Eq Alt Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: Alt -> Alt -> Bool Source # (/=) :: Alt -> Alt -> Bool Source #

data Literal Source #

Constructors

Int Integer |
Frac Rational |
Char Char |
String Text |

#### Instances

Instances details

Pretty Literal Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Literal -> Doc Source # prettyPrec :: Int -> Literal -> Doc Source # prettyList :: [Literal] -> Doc Source #
Eq Literal Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: Literal -> Literal -> Bool Source # (/=) :: Literal -> Literal -> Bool Source #

# Names

data ModuleName Source #

Constructors

ModuleName String |

#### Instances

Instances details

Pretty ModuleName Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: ModuleName -> Doc Source # prettyPrec :: Int -> ModuleName -> Doc Source # prettyList :: [ModuleName] -> Doc Source #
Eq ModuleName Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: ModuleName -> ModuleName -> Bool Source # (/=) :: ModuleName -> ModuleName -> Bool Source #
Ord ModuleName Source # |

Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

compare :: ModuleName -> ModuleName -> Ordering Source #

(<) :: ModuleName -> ModuleName -> Bool Source #

(<=) :: ModuleName -> ModuleName -> Bool Source #

(>) :: ModuleName -> ModuleName -> Bool Source #

(>=) :: ModuleName -> ModuleName -> Bool Source #

max :: ModuleName -> ModuleName -> ModuleName Source #

min :: ModuleName -> ModuleName -> ModuleName Source #

data QName Source #

Constructors

Qual ModuleName Name |
UnQual Name |

#### Instances

Instances details

Pretty QName Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: QName -> Doc Source # prettyPrec :: Int -> QName -> Doc Source # prettyList :: [QName] -> Doc Source #
Eq QName Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: QName -> QName -> Bool Source # (/=) :: QName -> QName -> Bool Source #

data Name Source #

Constructors

Ident String |
Symbol String |

#### Instances

Instances details

Pretty Name Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: Name -> Doc Source # prettyPrec :: Int -> Name -> Doc Source # prettyList :: [Name] -> Doc Source #
Eq Name Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: Name -> Name -> Bool Source # (/=) :: Name -> Name -> Bool Source #

data QOp Source #

Constructors

QVarOp QName |

#### Instances

Instances details

Pretty QOp Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: QOp -> Doc Source # prettyPrec :: Int -> QOp -> Doc Source # prettyList :: [QOp] -> Doc Source #
Eq QOp Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: QOp -> QOp -> Bool Source # (/=) :: QOp -> QOp -> Bool Source #

data TyVarBind Source #

Constructors

UnkindedVar Name |

#### Instances

Instances details

Pretty TyVarBind Source # |
Instance details Defined in Agda.Compiler.MAlonzo.Pretty Methods pretty :: TyVarBind -> Doc Source # prettyPrec :: Int -> TyVarBind -> Doc Source # prettyList :: [TyVarBind] -> Doc Source #
Eq TyVarBind Source # |
Instance details Defined in Agda.Utils.Haskell.Syntax Methods (==) :: TyVarBind -> TyVarBind -> Bool Source # (/=) :: TyVarBind -> TyVarBind -> Bool Source #

unit_con :: Exp Source #