-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- | 'Expr' data type and its generalizations

module Indigo.Internal.Expr.Types
  ( -- * The Expr data type
    Expr (..)

  -- * Generalizations of Expr
  , IsExpr
  , AreExprs
  , ToExpr
  , ExprType
  , (:~>)
  , toExpr

  -- * Arithmetic Expr
  , IsArithExpr
  , IsUnaryArithExpr

  -- * Polymorphic Expr
  , IsConcatExpr
  , IsConcatListExpr
  , IsDivExpr
  , IsModExpr
  , IsGetExpr
  , IsMemExpr
  , IsSizeExpr
  , IsSliceExpr
  , IsUpdExpr

  , ObjectManipulation (..)
  , ObjectExpr
  , NamedFieldExpr (..)
  ) where

import qualified Data.Kind as Kind
import Data.Vinyl.Core (RMap(..))

import Indigo.Prelude (Either (..), id)
import Indigo.Lorentz
import Indigo.Internal.Field
import Indigo.Internal.Object (Var, IndigoObjectF (..), FieldTypes, ComplexObjectC)
import qualified Michelson.Typed.Arith as M
import Michelson.Typed.Haskell.Instr.Product (GetFieldType)

----------------------------------------------------------------------------
-- The Expr data type
----------------------------------------------------------------------------

data Expr a where
  C :: NiceConstant a => a -> Expr a

  V :: KnownValue a => Var a -> Expr a

  ObjMan :: ObjectManipulation a -> Expr a

  Cast
    :: (ex :~> a)
    => ex -> Expr a

  Size :: (IsExpr exc c, SizeOpHs c)
       => exc -> Expr Natural

  Update
    :: ( UpdOpHs c
       , IsExpr exKey (UpdOpKeyHs c)
       , IsExpr exVal (UpdOpParamsHs c)
       , IsExpr exStructure c
       )
    => exStructure -> exKey -> exVal -> Expr c

  Add :: (AreExprs ex1 ex2 n m, ArithOpHs M.Add n m, KnownValue (ArithResHs M.Add n m))
      => ex1 -> ex2 -> Expr (ArithResHs M.Add n m)

  Sub :: (AreExprs ex1 ex2 n m, ArithOpHs M.Sub n m, KnownValue (ArithResHs M.Sub n m))
      => ex1 -> ex2 -> Expr (ArithResHs M.Sub n m)

  Mul :: (AreExprs ex1 ex2 n m, ArithOpHs M.Mul n m, KnownValue (ArithResHs M.Mul n m))
      => ex1 -> ex2 -> Expr (ArithResHs M.Mul n m)

  Div :: (AreExprs ex1 ex2 n m, EDivOpHs n m, KnownValue (EDivOpResHs n m))
      => ex1 -> ex2 -> Expr (EDivOpResHs n m)

  Mod :: (AreExprs ex1 ex2 n m, EDivOpHs n m, KnownValue (EModOpResHs n m))
      => ex1 -> ex2 -> Expr (EModOpResHs n m)

  Abs :: (IsExpr ex n, UnaryArithOpHs M.Abs n, KnownValue (UnaryArithResHs M.Abs n))
      => ex -> Expr (UnaryArithResHs M.Abs n)

  Neg :: (IsExpr ex n, UnaryArithOpHs M.Neg n, KnownValue (UnaryArithResHs M.Neg n))
      => ex -> Expr (UnaryArithResHs M.Neg n)


  Lsl :: (AreExprs ex1 ex2 n m, ArithOpHs M.Lsl n m, KnownValue (ArithResHs M.Lsl n m))
      => ex1 -> ex2 -> Expr (ArithResHs M.Lsl n m)

  Lsr :: (AreExprs ex1 ex2 n m, ArithOpHs M.Lsr n m, KnownValue (ArithResHs M.Lsr n m))
      => ex1 -> ex2 -> Expr (ArithResHs M.Lsr n m)


  Eq' :: ( AreExprs ex1 ex2 n n
         , NiceComparable n
         )
      => ex1 -> ex2 -> Expr Bool

  Neq :: ( AreExprs ex1 ex2 n n
         , NiceComparable n
         )
      => ex1 -> ex2 -> Expr Bool

  Le :: ( AreExprs ex1 ex2 n n
        , NiceComparable n
        )
     => ex1 -> ex2 -> Expr Bool

  Lt :: ( AreExprs ex1 ex2 n n
        , NiceComparable n
        )
     => ex1 -> ex2 -> Expr Bool

  Ge :: ( AreExprs ex1 ex2 n n
        , NiceComparable n
        )
     => ex1 -> ex2 -> Expr Bool

  Gt :: ( AreExprs ex1 ex2 n n
        , NiceComparable n
        )
     => ex1 -> ex2 -> Expr Bool

  Or :: (AreExprs ex1 ex2 n m, ArithOpHs M.Or n m, KnownValue (ArithResHs M.Or n m))
     => ex1 -> ex2 -> Expr (ArithResHs M.Or n m)

  Xor :: (AreExprs ex1 ex2 n m, ArithOpHs M.Xor n m, KnownValue (ArithResHs M.Xor n m))
      => ex1 -> ex2 -> Expr (ArithResHs M.Xor n m)

  And :: (AreExprs ex1 ex2 n m, ArithOpHs M.And n m, KnownValue (ArithResHs M.And n m))
      => ex1 -> ex2 -> Expr (ArithResHs M.And n m)

  Not :: (IsExpr op n, UnaryArithOpHs M.Not n, KnownValue (UnaryArithResHs M.Not n))
      => op -> Expr (UnaryArithResHs M.Not n)

  Int'
    :: IsExpr ex Natural
    => ex -> Expr Integer

  IsNat
    :: IsExpr ex Integer
    => ex -> Expr (Maybe Natural)


  Fst :: (IsExpr op (n, m), KnownValue n) => op -> Expr n
  Snd :: (IsExpr op (n, m), KnownValue m) => op -> Expr m

  Pair :: (AreExprs ex1 ex2 n m, KnownValue (n, m)) => ex1 -> ex2 -> Expr (n, m)

  Some :: (IsExpr ex t, KnownValue (Maybe t)) => ex -> Expr (Maybe t)
  None :: KnownValue t => Expr (Maybe t)

  Right' :: (IsExpr ex x, KnownValue y, KnownValue (Either y x)) => ex -> Expr (Either y x)
  Left' :: (IsExpr ex y, KnownValue x, KnownValue (Either y x)) => ex -> Expr (Either y x)

  Mem
    :: ( MemOpHs c
       , IsExpr exc c
       , IsExpr exck (MemOpKeyHs c)
       )
    => exck -> exc -> Expr Bool

  UGet
    :: ( HasUStore name key value store
       , IsExpr exKey key
       , IsExpr exStore (UStore store)
       , KnownValue value
       )
    => Label name -> exKey -> exStore -> Expr (Maybe value)

  UInsertNew
    :: ( HasUStore name key value store
       , IsError err
       , IsExpr exKey key
       , IsExpr exVal value
       , IsExpr exStore (UStore store)
       )
    => Label name -> err
    -> exKey -> exVal -> exStore -> Expr (UStore store)

  UInsert
    :: ( HasUStore name key value store
       , IsExpr exKey key
       , IsExpr exVal value
       , IsExpr exStore (UStore store)
       )
    => Label name
    -> exKey -> exVal -> exStore -> Expr (UStore store)

  UMem
    :: ( HasUStore name key val store
       , exKey :~> key
       , exStore :~> UStore store
       , KnownValue val
       )
    => Label name -> exKey -> exStore -> Expr Bool

  UUpdate
    :: ( HasUStore name key val store
       , exKey :~> key
       , exVal :~> Maybe val
       , exStore :~> UStore store
       )
    => Label name -> exKey -> exVal -> exStore -> Expr (UStore store)

  UDelete
    :: ( HasUStore name key val store
       , exKey :~> key
       , exStore :~> UStore store
       )
    => Label name -> exKey -> exStore -> Expr (UStore store)

  Construct
    :: ( InstrConstructC dt
       , RMap (ConstructorFieldTypes dt)
       , KnownValue dt
       )
    => Rec Expr (ConstructorFieldTypes dt) -> Expr dt

  -- TODO remove Construct and rename this one
  ConstructWithoutNamed
    :: ComplexObjectC dt
    => Rec Expr (FieldTypes dt) -> Expr dt

  Name
    :: (IsExpr ex t, KnownValue (name :! t))
    => Label name -> ex -> Expr (name :! t)
  UnName
    :: (IsExpr ex (name :! t), KnownValue t)
    => Label name -> ex -> Expr t

  EmptySet
    :: (NiceComparable key, KnownValue (Set key))
    => Expr (Set key)

  Get
    :: ( GetOpHs c
       , KnownValue (Maybe (GetOpValHs c))
       , IsExpr exKey (GetOpKeyHs c)
       , IsExpr exMap c
       , KnownValue (GetOpValHs c)
       )
    => exKey -> exMap -> Expr (Maybe (GetOpValHs c))

  EmptyMap
    :: (KnownValue value, NiceComparable key, KnownValue (Map key value))
    => Expr (Map key value)

  EmptyBigMap
    :: (KnownValue value, NiceComparable key, KnownValue (BigMap key value))
    => Expr (BigMap key value)

  Pack
    :: (IsExpr ex a, NicePackedValue a)
    => ex -> Expr ByteString

  Unpack
    :: ( NiceUnpackedValue a
       , IsExpr bsExpr ByteString
       )
    => bsExpr -> Expr (Maybe a)

  Cons
    :: ( IsExpr ex1 a
       , IsExpr ex2 (List a)
       )
    => ex1 -> ex2 -> Expr (List a)

  Nil :: KnownValue a => Expr (List a)

  Concat
    :: ( IsExpr ex1 c
       , IsExpr ex2 c
       , ConcatOpHs c
       )
    => ex1 -> ex2 -> Expr c

  Concat'
    :: ( IsExpr ex (List c)
       , ConcatOpHs c
       , KnownValue c
       )
    => ex -> Expr c

  Slice
    :: ( IsExpr ex c
       , SliceOpHs c
       , IsExpr an Natural
       , IsExpr bn Natural
       )
    => an -> bn -> ex -> Expr (Maybe c)

  Contract
    :: ( NiceParameterFull p
       , NoExplicitDefaultEntryPoint p
       , ToTAddress p addr
       , ToT addr ~ ToT Address
       , IsExpr exAddr addr
       )
    => exAddr -> Expr (Maybe (ContractRef p))

  Self
    :: ( NiceParameterFull p
       , NoExplicitDefaultEntryPoint p
       )
    => Expr (ContractRef p)

  ContractAddress
    :: IsExpr exc (ContractRef p)
    => exc -> Expr Address

  ContractCallingUnsafe
    :: ( NiceParameter arg
       , IsExpr exAddr Address
       )
    => EpName -> exAddr -> Expr (Maybe (ContractRef arg))

  RunFutureContract
    :: ( NiceParameter p
       , IsExpr conExpr (FutureContract p)
       )
    => conExpr -> Expr (Maybe (ContractRef p))

  ImplicitAccount
    :: (IsExpr exkh KeyHash)
    => exkh -> Expr (ContractRef ())

  ConvertEpAddressToContract
    :: ( NiceParameter p
       , IsExpr epExpr EpAddress
       )
    => epExpr -> Expr (Maybe (ContractRef p))

  MakeView
    :: ( KnownValue (View a r)
       , exa :~> a
       , exCRef :~> ContractRef r
       )
    => exa -> exCRef -> Expr (View a r)

  MakeVoid
    :: ( KnownValue (Void_ a b)
       , exa :~> a
       , exCRef :~> Lambda b b
       )
    => exa -> exCRef -> Expr (Void_ a b)

  CheckSignature
    :: ( IsExpr pkExpr PublicKey
       , IsExpr sigExpr Signature
       , IsExpr hashExpr ByteString
       )
    => pkExpr -> sigExpr -> hashExpr -> Expr Bool

  Sha256 :: (IsExpr hashExpr ByteString) => hashExpr -> Expr ByteString
  Sha512 :: (IsExpr hashExpr ByteString) => hashExpr -> Expr ByteString
  Blake2b :: (IsExpr hashExpr ByteString) => hashExpr -> Expr ByteString
  HashKey :: (IsExpr keyExpr PublicKey) => keyExpr -> Expr KeyHash

  ChainId :: Expr ChainId

  Now :: Expr Timestamp
  Amount :: Expr Mutez
  Balance :: Expr Mutez
  Sender :: Expr Address

  Exec
    :: ( IsExpr exA a, IsExpr exLambda (Lambda a b)
       , KnownValue b
       )
    => exA -> exLambda -> Expr b

  NonZero
    :: (IsExpr ex n, NonZero n, KnownValue (Maybe n))
    => ex -> Expr (Maybe n)

----------------------------------------------------------------------------
-- Object manipulation
----------------------------------------------------------------------------

-- | Datatype describing access to an inner fields of object, like
-- @object !. field1 !. field2 ~. (field3, value3) ~. (field4, value4)@
data ObjectManipulation a where
  Object :: Expr a -> ObjectManipulation a

  ToField
    :: HasField dt fname ftype
    => ObjectManipulation dt
    -> Label fname
    -> ObjectManipulation ftype

  -- NB. @SetField (Object expr) field1
  --       (ObjMan $ SetField (ToField (Object expr) field1) field2 targetExpr)@
  -- is a bad representation, which will cause generation of not optimal code
  -- (like expr would be materialized object),
  -- so it would be nice to enforce only
  -- @SetField (Object expr) (field1 . field2) targetExpr@ representation.
  SetField
    :: HasField dt fname ftype
    => ObjectManipulation dt
    -> Label fname
    -> Expr ftype
    -> ObjectManipulation dt

-- | Auxiliary datatype where each field refers to
-- an expression the field equals to. It's not recursive one.
data NamedFieldExpr a name where
  NamedFieldExpr
    :: { unNamedFieldExpr :: Expr (GetFieldType a name) }
    -> NamedFieldExpr a name

type ObjectExpr a = IndigoObjectF (NamedFieldExpr a) a

----------------------------------------------------------------------------
-- Generalizations of Expr
----------------------------------------------------------------------------

type IsExpr op n = (ToExpr op, ExprType op ~ n, KnownValue n)
type (:~>) op n = IsExpr op n

type AreExprs ex1 ex2 n m = (IsExpr ex1 n, IsExpr ex2 m)

type ExprType a = ExprType' (Decide a) a

toExpr :: forall a . ToExpr a => a -> Expr (ExprType a)
toExpr = toExpr' @(Decide a) @a

class ToExpr' (Decide x) x => ToExpr x
instance ToExpr' (Decide x) x => ToExpr x

-- This type class is needed to cope with overlapping instances.
class ToExpr' decision c where
  type family ExprType' decision c :: Kind.Type
  toExpr' :: c -> Expr (ExprType' decision c)

-- Instance for a var
instance KnownValue (a :: Kind.Type) => ToExpr' 'VarD (Var a) where
  type instance ExprType' 'VarD (Var a) = a
  toExpr' = V

-- Instance for a value
instance NiceConstant a => ToExpr' 'ValD a where
  type instance ExprType' 'ValD a = a
  toExpr' = C

-- Instance for StructManipulation
instance ToExpr' 'ObjManD (ObjectManipulation a) where
  type instance ExprType' 'ObjManD (ObjectManipulation a) = a
  toExpr' = ObjMan

-- Instance for Expr itself
instance ToExpr' 'ExprD (Expr a) where
  type instance ExprType' 'ExprD (Expr a) = a
  toExpr' = id

data Decision = VarD | ValD | ExprD | ObjManD

type family Decide x :: Decision where
  Decide (Var _) = 'VarD
  Decide (Expr _) = 'ExprD
  Decide (ObjectManipulation _) = 'ObjManD
  Decide _ = 'ValD

type IsUnaryArithExpr exN a n =
  ( exN :~> n
  , UnaryArithOpHs a n
  , KnownValue (UnaryArithResHs a n)
  )

type IsArithExpr exN exM a n m =
  ( AreExprs exN exM n m
  , ArithOpHs a n m
  , KnownValue (ArithResHs a n m)
  )

type IsDivExpr exN exM n m =
  ( AreExprs exN exM n m
  , EDivOpHs n m
  , KnownValue (EDivOpResHs n m)
  )

type IsModExpr exN exM n m =
  ( AreExprs exN exM n m
  , EDivOpHs n m
  , KnownValue (EModOpResHs n m)
  )

type IsConcatExpr exN1 exN2 n =
  ( exN1 :~> n
  , exN2 :~> n
  , ConcatOpHs n
  )

type IsConcatListExpr exN n =
  ( exN :~> List n
  , ConcatOpHs n
  , KnownValue n
  )

type IsSliceExpr exN n =
  ( exN :~> n
  , SliceOpHs n
  )

type IsGetExpr exKey exMap map =
  ( exKey :~> GetOpKeyHs map
  , exMap :~> map
  , GetOpHs map
  , KnownValue (GetOpValHs map)
  )

type IsUpdExpr exKey exVal exMap map =
  ( exKey :~> UpdOpKeyHs map
  , exVal :~> UpdOpParamsHs map
  , exMap :~> map
  , UpdOpHs map
  )

type IsMemExpr exKey exN n =
  ( exKey :~> MemOpKeyHs n
  , exN :~> n
  , MemOpHs n
  )

type IsSizeExpr exN n =
  ( exN :~> n
  , SizeOpHs n
  )