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 # (/=) :: Decl -> Decl -> Bool #

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 # (/=) :: DataOrNew -> DataOrNew -> Bool #

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 # (/=) :: ConDecl -> ConDecl -> Bool #

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 # (/=) :: Strictness -> Strictness -> Bool #

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 # (/=) :: Binds -> Binds -> Bool #

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 # (/=) :: Rhs -> Rhs -> Bool #

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 # (/=) :: GuardedRhs -> GuardedRhs -> Bool #

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 # (/=) :: Match -> Match -> Bool #

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 # (/=) :: Type -> Type -> Bool #

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 # (/=) :: Pat -> Pat -> Bool #

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 # (/=) :: Stmt -> Stmt -> Bool #

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 # (/=) :: Exp -> Exp -> Bool #

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 # (/=) :: Alt -> Alt -> Bool #

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 # (/=) :: Literal -> Literal -> Bool #

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 # (/=) :: ModuleName -> ModuleName -> Bool #
Ord ModuleName Source #
Instance details Defined in Agda.Utils.Haskell.Syntax Methods compare :: ModuleName -> ModuleName -> Ordering # (<) :: ModuleName -> ModuleName -> Bool # (<=) :: ModuleName -> ModuleName -> Bool # (>) :: ModuleName -> ModuleName -> Bool # (>=) :: ModuleName -> ModuleName -> Bool # max :: ModuleName -> ModuleName -> ModuleName # min :: ModuleName -> ModuleName -> ModuleName #

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 # (/=) :: QName -> QName -> Bool #

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 # (/=) :: Name -> Name -> Bool #

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 # (/=) :: QOp -> QOp -> Bool #

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 # (/=) :: TyVarBind -> TyVarBind -> Bool #

unit_con :: Exp Source #