-- | SSTG Syntax Definitions
module SSTG.Core.Language.Syntax
    ( module SSTG.Core.Language.Syntax
    ) where

-- | A `Program` is defined as a list of bindings. The @Name@ is an identifier
-- that determines a unique binder to the @var@. In practice, these are defined
-- to be `Name` and `Var` respectively.
newtype Program = Program [Bind] deriving (Show, Eq, Read)

-- | Variables, data constructors, type variables, and type constructors.
data NameSpace = VarNSpace | DataNSpace | TvNSpace | TcClsNSpace
               deriving (Show, Eq, Read, Ord)

-- | The occurrence name is defined as a string, with a `Maybe` module name
-- appearing. The `Int` denotes a `Unique` translated from GHC. For instance,
-- in the case of @Map.empty@, the occurrence name is @"empty"@, while the
-- module name is some variant of @Just \"Data.Map\"@.
data Name = Name String (Maybe String) NameSpace Int
          deriving (Show, Eq, Read, Ord)

-- | Variables consist of a `Name` and a `Type`.
data Var = Var Name Type deriving (Show, Eq, Read)

-- | Literals are largely augmented from the original GHC implementation, with
-- additional annotations to denote `BlankAddr` for lifting, `AddrLit` for
-- value deriviation, `SymLit` for symbolic literals, and `SymLitEval` to
-- represent symbolic literal evaluation, as literal manipulation functions
-- are defined in the Haskell Prelude, and thus outside of scope for us.
data Lit = MachChar Char Type
         | MachStr String Type
         | MachInt Int Type
         | MachWord Int Type
         | MachFloat Rational Type
         | MachDouble Rational Type
         | MachLabel String (Maybe Int) Type
         | MachNullAddr Type
         | BlankAddr
         | AddrLit Int
         | SymLit Var
         | SymLitEval PrimFun [Lit]
         deriving (Show, Eq, Read)

-- | Atomic objects. `VarAtom` may be used for variable lookups, while
-- `LitAtom` is used to denote literals.
data Atom = LitAtom (Lit)
          | VarAtom Var
          deriving (Show, Eq, Read)

-- | Primitive functions.
data PrimFun = PrimFun Name Type deriving (Show, Eq, Read)

-- | Expressions closely correspond to their representation in GHC.
data Expr = Atom Atom
          | PrimApp PrimFun [Atom]
          | ConApp DataCon [Atom]
          | FunApp Var [Atom]
          | Let Bind Expr
          | Case Expr Var [Alt]
          deriving (Show, Eq, Read)

-- | Alternatives utilize an `AltCon`, a list of parameters of that match to
-- the appropriate `DataAlt` as applicable, and an expression for the result.
data Alt = Alt AltCon [Var] Expr deriving (Show, Eq, Read)

-- | Alt Constructor
data AltCon = DataAlt DataCon
            | LitAlt Lit
            | Default
            deriving (Show, Eq, Read)

-- | Bind
data Bind = Bind RecForm [(Var, BindRhs)] deriving (Show, Eq, Read)

-- | Recursive?
data RecForm = Rec | NonRec deriving (Show, Eq, Read)

-- | `BindRhs` taken straight from STG can be either in constructor form, or
-- function form. Empty parameter list denotes a thunk.
data BindRhs = ConForm DataCon [Atom]
             | FunForm [Var] Expr
             deriving (Show, Eq, Read)

-- | Data Constructor consists of its tag, the type that corresponds to its
-- ADT, and a list of paramters it takes.
data DataCon = DataCon Name Type [Type] deriving (Show, Eq, Read)

-- | Types are information that are useful to keep during symbolic execution
-- in order to generate correct feeds into the SMT solver. Overapproxmation is
-- currently performed, and is likely to be cut back in the future.
data Type = TyVarTy Name Type
          | AppTy Type Type
          | ForAllTy TyBinder Type
          | CastTy Type Coercion
          | TyConApp TyCon [Type]
          | CoercionTy Coercion
          | LitTy TyLit
          | FunTy Type Type
          | Bottom
          deriving (Show, Eq, Read)

-- | Type binder for `ForAllTy`.
data TyBinder = NamedTyBndr Name
              | AnonTyBndr
              deriving (Show, Eq, Read)

-- | `Type` literal.
data TyLit = NumTyLit Int
           | StrTyLit String
           deriving (Show, Eq, Read)

-- | Coercion. I have no idea what this does :)
data Coercion = Coercion Type Type deriving (Show, Eq, Read)

-- | Type constructor.
data TyCon = FunTyCon Name [TyBinder]
           | AlgTyCon Name [Name] AlgTyRhs
           | SynonymTyCon Name [Name]
           | FamilyTyCon Name [Name]
           | PrimTyCon Name [TyBinder]
           | Promoted Name [TyBinder] DataCon
           deriving (Show, Eq, Read)

-- | ADT RHS.
data AlgTyRhs = AbstractTyCon Bool
              | DataTyCon [Name]
              | NewTyCon Name
              | TupleTyCon Name
              deriving (Show, Eq, Read)