-- | ASTs for subset of GHC Haskell syntax.

module Agda.Utils.Haskell.Syntax where

import Data.Text (Text)

-- * Modules

data Module = Module ModuleName [ModulePragma] [ImportDecl] [Decl]

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

data ImportDecl = ImportDecl
  { ImportDecl -> ModuleName
importModule    :: ModuleName
  , ImportDecl -> Bool
importQualified :: Bool
  , ImportDecl -> Maybe (Bool, [ImportSpec])
importSpecs     :: Maybe (Bool, [ImportSpec])
  }

data ImportSpec = IVar Name

-- * Declarations

data Decl = 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
  deriving (Decl -> Decl -> Bool
(Decl -> Decl -> Bool) -> (Decl -> Decl -> Bool) -> Eq Decl
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Decl -> Decl -> Bool
$c/= :: Decl -> Decl -> Bool
== :: Decl -> Decl -> Bool
$c== :: 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
/= :: DataOrNew -> DataOrNew -> Bool
$c/= :: DataOrNew -> DataOrNew -> Bool
== :: DataOrNew -> DataOrNew -> Bool
$c== :: 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
/= :: ConDecl -> ConDecl -> Bool
$c/= :: ConDecl -> ConDecl -> Bool
== :: ConDecl -> ConDecl -> Bool
$c== :: 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
/= :: Strictness -> Strictness -> Bool
$c/= :: Strictness -> Strictness -> Bool
== :: Strictness -> Strictness -> Bool
$c== :: 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
/= :: Binds -> Binds -> Bool
$c/= :: Binds -> Binds -> Bool
== :: Binds -> Binds -> Bool
$c== :: 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
/= :: Rhs -> Rhs -> Bool
$c/= :: Rhs -> Rhs -> Bool
== :: Rhs -> Rhs -> Bool
$c== :: 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
/= :: GuardedRhs -> GuardedRhs -> Bool
$c/= :: GuardedRhs -> GuardedRhs -> Bool
== :: GuardedRhs -> GuardedRhs -> Bool
$c== :: 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
/= :: Match -> Match -> Bool
$c/= :: Match -> Match -> Bool
== :: Match -> Match -> Bool
$c== :: Match -> Match -> Bool
Eq)

-- * Expressions

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
/= :: Type -> Type -> Bool
$c/= :: Type -> Type -> Bool
== :: Type -> Type -> Bool
$c== :: 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
/= :: Pat -> Pat -> Bool
$c/= :: Pat -> Pat -> Bool
== :: Pat -> Pat -> Bool
$c== :: 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
/= :: Stmt -> Stmt -> Bool
$c/= :: Stmt -> Stmt -> Bool
== :: Stmt -> Stmt -> Bool
$c== :: 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
/= :: Exp -> Exp -> Bool
$c/= :: Exp -> Exp -> Bool
== :: Exp -> Exp -> Bool
$c== :: 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
/= :: Alt -> Alt -> Bool
$c/= :: Alt -> Alt -> Bool
== :: Alt -> Alt -> Bool
$c== :: 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
/= :: Literal -> Literal -> Bool
$c/= :: Literal -> Literal -> Bool
== :: Literal -> Literal -> Bool
$c== :: Literal -> Literal -> Bool
Eq)

-- * Names

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
/= :: ModuleName -> ModuleName -> Bool
$c/= :: ModuleName -> ModuleName -> Bool
== :: ModuleName -> ModuleName -> Bool
$c== :: 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
min :: ModuleName -> ModuleName -> ModuleName
$cmin :: ModuleName -> ModuleName -> ModuleName
max :: ModuleName -> ModuleName -> ModuleName
$cmax :: ModuleName -> ModuleName -> ModuleName
>= :: ModuleName -> ModuleName -> Bool
$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
compare :: ModuleName -> ModuleName -> Ordering
$ccompare :: ModuleName -> ModuleName -> Ordering
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
/= :: QName -> QName -> Bool
$c/= :: QName -> QName -> Bool
== :: QName -> QName -> Bool
$c== :: 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
/= :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c== :: 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
/= :: QOp -> QOp -> Bool
$c/= :: QOp -> QOp -> Bool
== :: QOp -> QOp -> Bool
$c== :: 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
/= :: TyVarBind -> TyVarBind -> Bool
$c/= :: TyVarBind -> TyVarBind -> Bool
== :: TyVarBind -> TyVarBind -> Bool
$c== :: TyVarBind -> TyVarBind -> Bool
Eq)

unit_con :: Exp
unit_con :: Exp
unit_con = QName -> Exp
Con (Name -> QName
UnQual (String -> Name
Ident String
"()"))