module Agda.Utils.Haskell.Syntax where
import Data.Text (Text)
data Module = Module ModuleName [ModulePragma] [ImportDecl] [Decl]
data ModulePragma
= LanguagePragma [Name]
| OtherPragma String
data ImportDecl = ImportDecl
{ ImportDecl -> ModuleName
importModule :: ModuleName
, ImportDecl -> Bool
importQualified :: Bool
, ImportDecl -> Maybe (Bool, [ImportSpec])
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
| String
deriving (Decl -> Decl -> Bool
(Decl -> Decl -> Bool) -> (Decl -> Decl -> Bool) -> Eq Decl
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Decl -> Decl -> Bool
== :: Decl -> Decl -> Bool
$c/= :: Decl -> Decl -> Bool
/= :: Decl -> Decl -> Bool
Eq)
data DataOrNew = DataType | NewType
deriving (DataOrNew -> DataOrNew -> Bool
(DataOrNew -> DataOrNew -> Bool)
-> (DataOrNew -> DataOrNew -> Bool) -> Eq DataOrNew
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: DataOrNew -> DataOrNew -> Bool
== :: DataOrNew -> DataOrNew -> Bool
$c/= :: DataOrNew -> DataOrNew -> Bool
/= :: DataOrNew -> DataOrNew -> Bool
Eq)
data ConDecl = ConDecl Name [(Maybe Strictness, Type)]
deriving (ConDecl -> ConDecl -> Bool
(ConDecl -> ConDecl -> Bool)
-> (ConDecl -> ConDecl -> Bool) -> Eq ConDecl
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ConDecl -> ConDecl -> Bool
== :: ConDecl -> ConDecl -> Bool
$c/= :: ConDecl -> ConDecl -> Bool
/= :: ConDecl -> ConDecl -> Bool
Eq)
data Strictness = Lazy | Strict
deriving (Strictness -> Strictness -> Bool
(Strictness -> Strictness -> Bool)
-> (Strictness -> Strictness -> Bool) -> Eq Strictness
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Strictness -> Strictness -> Bool
== :: Strictness -> Strictness -> Bool
$c/= :: Strictness -> Strictness -> Bool
/= :: Strictness -> Strictness -> Bool
Eq)
type Deriving = (QName, [Type])
data Binds = BDecls [Decl]
deriving (Binds -> Binds -> Bool
(Binds -> Binds -> Bool) -> (Binds -> Binds -> Bool) -> Eq Binds
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Binds -> Binds -> Bool
== :: Binds -> Binds -> Bool
$c/= :: Binds -> Binds -> Bool
/= :: Binds -> Binds -> Bool
Eq)
data Rhs = UnGuardedRhs Exp
| GuardedRhss [GuardedRhs]
deriving (Rhs -> Rhs -> Bool
(Rhs -> Rhs -> Bool) -> (Rhs -> Rhs -> Bool) -> Eq Rhs
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Rhs -> Rhs -> Bool
== :: Rhs -> Rhs -> Bool
$c/= :: Rhs -> Rhs -> Bool
/= :: Rhs -> Rhs -> Bool
Eq)
data GuardedRhs = GuardedRhs [Stmt] Exp
deriving (GuardedRhs -> GuardedRhs -> Bool
(GuardedRhs -> GuardedRhs -> Bool)
-> (GuardedRhs -> GuardedRhs -> Bool) -> Eq GuardedRhs
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: GuardedRhs -> GuardedRhs -> Bool
== :: GuardedRhs -> GuardedRhs -> Bool
$c/= :: GuardedRhs -> GuardedRhs -> Bool
/= :: GuardedRhs -> GuardedRhs -> Bool
Eq)
data Match = Match Name [Pat] Rhs (Maybe Binds)
deriving (Match -> Match -> Bool
(Match -> Match -> Bool) -> (Match -> Match -> Bool) -> Eq Match
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Match -> Match -> Bool
== :: Match -> Match -> Bool
$c/= :: Match -> Match -> Bool
/= :: Match -> Match -> Bool
Eq)
data Type = TyForall [TyVarBind] Type
| TyFun Type Type
| TyCon QName
| TyVar Name
| TyApp Type Type
| FakeType String
deriving (Type -> Type -> Bool
(Type -> Type -> Bool) -> (Type -> Type -> Bool) -> Eq Type
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
/= :: Type -> Type -> Bool
Eq)
data Pat = PVar Name
| PLit Literal
| PAsPat Name Pat
| PWildCard
| PBangPat Pat
| PApp QName [Pat]
| PatTypeSig Pat Type
| PIrrPat Pat
deriving (Pat -> Pat -> Bool
(Pat -> Pat -> Bool) -> (Pat -> Pat -> Bool) -> Eq Pat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Pat -> Pat -> Bool
== :: Pat -> Pat -> Bool
$c/= :: Pat -> Pat -> Bool
/= :: Pat -> Pat -> Bool
Eq)
data Stmt = Qualifier Exp
| Generator Pat Exp
deriving (Stmt -> Stmt -> Bool
(Stmt -> Stmt -> Bool) -> (Stmt -> Stmt -> Bool) -> Eq Stmt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Stmt -> Stmt -> Bool
== :: Stmt -> Stmt -> Bool
$c/= :: Stmt -> Stmt -> Bool
/= :: Stmt -> Stmt -> Bool
Eq)
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
deriving (Exp -> Exp -> Bool
(Exp -> Exp -> Bool) -> (Exp -> Exp -> Bool) -> Eq Exp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Exp -> Exp -> Bool
== :: Exp -> Exp -> Bool
$c/= :: Exp -> Exp -> Bool
/= :: Exp -> Exp -> Bool
Eq)
data Alt = Alt Pat Rhs (Maybe Binds)
deriving (Alt -> Alt -> Bool
(Alt -> Alt -> Bool) -> (Alt -> Alt -> Bool) -> Eq Alt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Alt -> Alt -> Bool
== :: Alt -> Alt -> Bool
$c/= :: Alt -> Alt -> Bool
/= :: Alt -> Alt -> Bool
Eq)
data Literal = Int Integer | Frac Rational | Char Char | String Text
deriving (Literal -> Literal -> Bool
(Literal -> Literal -> Bool)
-> (Literal -> Literal -> Bool) -> Eq Literal
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Literal -> Literal -> Bool
== :: Literal -> Literal -> Bool
$c/= :: Literal -> Literal -> Bool
/= :: Literal -> Literal -> Bool
Eq)
data ModuleName = ModuleName String
deriving (ModuleName -> ModuleName -> Bool
(ModuleName -> ModuleName -> Bool)
-> (ModuleName -> ModuleName -> Bool) -> Eq ModuleName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ModuleName -> ModuleName -> Bool
== :: ModuleName -> ModuleName -> Bool
$c/= :: ModuleName -> ModuleName -> Bool
/= :: ModuleName -> ModuleName -> Bool
Eq, Eq ModuleName
Eq ModuleName
-> (ModuleName -> ModuleName -> Ordering)
-> (ModuleName -> ModuleName -> Bool)
-> (ModuleName -> ModuleName -> Bool)
-> (ModuleName -> ModuleName -> Bool)
-> (ModuleName -> ModuleName -> Bool)
-> (ModuleName -> ModuleName -> ModuleName)
-> (ModuleName -> ModuleName -> ModuleName)
-> Ord ModuleName
ModuleName -> ModuleName -> Bool
ModuleName -> ModuleName -> Ordering
ModuleName -> ModuleName -> ModuleName
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ModuleName -> ModuleName -> Ordering
compare :: ModuleName -> ModuleName -> Ordering
$c< :: ModuleName -> ModuleName -> Bool
< :: ModuleName -> ModuleName -> Bool
$c<= :: ModuleName -> ModuleName -> Bool
<= :: ModuleName -> ModuleName -> Bool
$c> :: ModuleName -> ModuleName -> Bool
> :: ModuleName -> ModuleName -> Bool
$c>= :: ModuleName -> ModuleName -> Bool
>= :: ModuleName -> ModuleName -> Bool
$cmax :: ModuleName -> ModuleName -> ModuleName
max :: ModuleName -> ModuleName -> ModuleName
$cmin :: ModuleName -> ModuleName -> ModuleName
min :: ModuleName -> ModuleName -> ModuleName
Ord)
data QName = Qual ModuleName Name | UnQual Name
deriving (QName -> QName -> Bool
(QName -> QName -> Bool) -> (QName -> QName -> Bool) -> Eq QName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QName -> QName -> Bool
== :: QName -> QName -> Bool
$c/= :: QName -> QName -> Bool
/= :: QName -> QName -> Bool
Eq)
data Name = Ident String | Symbol String
deriving (Name -> Name -> Bool
(Name -> Name -> Bool) -> (Name -> Name -> Bool) -> Eq Name
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
/= :: Name -> Name -> Bool
Eq)
data QOp = QVarOp QName
deriving (QOp -> QOp -> Bool
(QOp -> QOp -> Bool) -> (QOp -> QOp -> Bool) -> Eq QOp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: QOp -> QOp -> Bool
== :: QOp -> QOp -> Bool
$c/= :: QOp -> QOp -> Bool
/= :: QOp -> QOp -> Bool
Eq)
data TyVarBind = UnkindedVar Name
deriving (TyVarBind -> TyVarBind -> Bool
(TyVarBind -> TyVarBind -> Bool)
-> (TyVarBind -> TyVarBind -> Bool) -> Eq TyVarBind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TyVarBind -> TyVarBind -> Bool
== :: TyVarBind -> TyVarBind -> Bool
$c/= :: TyVarBind -> TyVarBind -> Bool
/= :: TyVarBind -> TyVarBind -> Bool
Eq)
unit_con :: Exp
unit_con :: Exp
unit_con = QName -> Exp
Con (Name -> QName
UnQual (String -> Name
Ident String
"()"))