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

type Program  = GenProgram  Name Var

type Lit      = GenLit      Name Var
type Atom     = GenAtom     Name Var
type PrimFun  = GenPrimFun  Name Var
type Expr     = GenExpr     Name Var
type Alt      = GenAlt      Name Var
type AltCon   = GenAltCon   Name Var
type Binding  = GenBinding  Name Var
type BindRhs  = GenBindRhs  Name Var

type ConTag   = GenConTag   Name
type DataCon  = GenDataCon  Name
type Type     = GenType     Name
type TyBinder = GenTyBinder Name
type Coercion = GenCoercion Name
type TyCon    = GenTyCon    Name
type AlgTyRhs = GenAlgTyRhs Name

-- | A Program is defined as a list of bindings. The @bnd@ is an identifier
-- that determines a unique binder to the @var@. In practice, these are defined
-- to be `Name` and `Var` respectively.
newtype GenProgram bnd var = Program [GenBinding bnd var]
                           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 (GenType Name) 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 GenLit bnd var = MachChar   Char     (GenType bnd)
                    | MachStr    String   (GenType bnd)
                    | MachInt    Int      (GenType bnd)
                    | MachWord   Int      (GenType bnd)
                    | MachFloat  Rational (GenType bnd)
                    | MachDouble Rational (GenType bnd)
                    | MachNullAddr        (GenType bnd)
                    | MachLabel  String   (Maybe Int) (GenType bnd)
                    | BlankAddr
                    | AddrLit    Int
                    | SymLit     var
                    | SymLitEval (GenPrimFun bnd var) [GenLit bnd var]
                    deriving (Show, Eq, Read)

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

-- | Primitive functions.
data GenPrimFun bnd var = PrimFun bnd (GenType bnd) deriving (Show, Eq, Read)

-- | Expressions closely correspond to their representation in GHC.
data GenExpr bnd var = Atom    (GenAtom bnd var)
                     | PrimApp (GenPrimFun bnd var)  [GenAtom bnd var]
                     | ConApp  (GenDataCon bnd)      [GenAtom bnd var]
                     | FunApp  var                   [GenAtom bnd var]
                     | Let     (GenBinding bnd var)  (GenExpr bnd var)
                     | Case    (GenExpr bnd var) var [GenAlt bnd var]
                     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 GenAlt bnd var = Alt (GenAltCon bnd var) [var] (GenExpr bnd var)
                    deriving (Show, Eq, Read)

-- | Alt Constructor
data GenAltCon bnd var = DataAlt (GenDataCon bnd)
                       | LitAlt  (GenLit bnd var)
                       | Default
                       deriving (Show, Eq, Read)

-- | Binding
data GenBinding bnd var = Binding RecForm [(var, GenBindRhs bnd var)]
                        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 GenBindRhs bnd var = ConForm (GenDataCon bnd) [GenAtom bnd var]
                        | FunForm [var]            (GenExpr bnd var)
                        deriving (Show, Eq, Read)

-- | Data Constructor tag that uniquely identifiers data constructors.
data GenConTag bnd = ConTag bnd Int 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 GenDataCon bnd = DataCon (GenConTag bnd) (GenType bnd) [GenType bnd]
                    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 GenType bnd = TyVarTy    bnd               (GenType bnd)
                 | AppTy      (GenType bnd)     (GenType bnd)
                 | ForAllTy   (GenTyBinder bnd) (GenType bnd)
                 | CastTy     (GenType bnd)     (GenCoercion bnd)
                 | TyConApp   (GenTyCon bnd)    [GenType bnd]
                 | CoercionTy (GenCoercion bnd)
                 | LitTy      TyLit
                 | FunTy      (GenType bnd)     (GenType bnd)
                 | Bottom
                 deriving (Show, Eq, Read)

-- | Type binder for `ForAllTy`.
data GenTyBinder bnd = NamedTyBndr bnd (GenType bnd)
                     | AnonTyBndr      (GenType bnd)
                     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 GenCoercion bnd = Coercion (GenType bnd) (GenType bnd)
                     deriving (Show, Eq, Read)

-- | Type constructor.
data GenTyCon bnd = FunTyCon     bnd
                  | AlgTyCon     bnd (GenAlgTyRhs bnd)
                  | SynonymTyCon bnd
                  | FamilyTyCon  bnd
                  | PrimTyCon    bnd
                  | Promoted     bnd (GenDataCon bnd)
                  | TcTyCon      bnd
                  deriving (Show, Eq, Read)

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