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

module Indigo.Internal.Object
  ( IndigoObjectF (..)
  , NamedFieldVar (..)
  , TypedFieldVar (..)
  , FieldTypes
  , Var
  , namedToTypedRec
  , typedToNamedRec
  , namedToTypedFieldVar
  , typedToNamedFieldVar

  , IsObject
  , complexObjectDict
  , ComplexObjectC
  , castFieldConstructors

  -- * Stack operations
  , withVarAt
  , makeTopVar
  , pushRefMd
  , pushNoRefMd
  , popNoRefMd

  -- * Operations/Storage variables
  , Ops
  , HasSideEffects
  , operationsVar
  , HasStorage
  , storageVar
  ) where

import Data.Vinyl (RMap)
import Data.Vinyl.TypeLevel (AllConstrained)
import Data.Reflection (Given (..))
import Data.Constraint (Dict(..))
import Data.Singletons (Sing)
import qualified GHC.Generics as G

import Indigo.Backend.Prelude
import Indigo.Lorentz
import Indigo.Internal.State
import Michelson.Typed.Haskell.Instr.Product
  ( GetFieldType, ConstructorFieldNames, GetFieldType
  , InstrDeconstructC, FieldConstructor (..), CastFieldConstructors (..))
import Michelson.Typed (IsPrimitiveValue)
import qualified Lorentz.Instr as L
import Util.Peano
import Util.Type (KnownList (..), KList (..))

----------------------------------------------------------------------------
-- IndigoObjectF and Variable
----------------------------------------------------------------------------

-- | A object that can be either
-- stored in the single stack cell or split into fields.
-- Fields are identified by their names.
--
-- @f@ is a functor to be applied to each of field names.
data IndigoObjectF f a where
  -- | Value stored on the stack, it might be
  -- either complex product type, like @(a, b)@, Storage, etc,
  -- or sum type like 'Either', or primitive like 'Int', 'Operation', etc.
  --
  -- Laziness of 'RefId' is needed here to make possible to put
  -- 'error' in a variable.
  -- This is used as a workaround in "Indigo.Compilation.Lambda".
  Cell :: KnownValue a => ~RefId -> IndigoObjectF f a
  -- | Decomposed product type, which is NOT stored
  -- as one cell on the stack.
  Decomposed :: ComplexObjectC a => Rec f (ConstructorFieldNames a) -> IndigoObjectF f a

-- | Auxiliary type family to convert list of field names
-- to list of field types
type family MapGFT a rs where
  MapGFT _ '[] = '[]
  MapGFT a (name ': xs) = GetFieldType a name ': MapGFT a xs

-- | Convert a list of fields from name-based list to type-based one
namedToTypedRec
  :: forall a f g .
    (forall name . f name -> g (GetFieldType a name))
  -> Rec f (ConstructorFieldNames a)
  -> Rec g (FieldTypes a)
namedToTypedRec fun = namedToTypedRecImpl
  where
    namedToTypedRecImpl :: Rec f rs -> Rec g (MapGFT a rs)
    namedToTypedRecImpl RNil = RNil
    namedToTypedRecImpl (v :& xs) = fun v :& namedToTypedRecImpl xs

-- | Convert a list of fields from type-based list to named-based one
typedToNamedRec :: forall a f g . KnownList (ConstructorFieldNames a)
  => (forall name . f (GetFieldType a name) -> g name)
  -> Rec f (FieldTypes a)
  -> Rec g (ConstructorFieldNames a)
typedToNamedRec fun = typedToNamedRecImpl
  where
    typedToNamedRecImpl :: forall rs . KnownList rs => Rec f (MapGFT a rs) -> Rec g rs
    typedToNamedRecImpl re = case (klist @rs, re) of
      (KNil, RNil)  -> RNil
      (KCons (_ :: Proxy nm) (_ :: Proxy rs'), v :& vs) -> fun v :& typedToNamedRecImpl vs

castFieldConstructors
  :: forall a st . CastFieldConstructors (FieldTypes a) (ConstructorFieldTypes a)
  => Rec (FieldConstructor st) (FieldTypes a) -> Rec (FieldConstructor st) (ConstructorFieldTypes a)
castFieldConstructors = castFieldConstructorsImpl

-- | Auxiliary datatype to define a variable.
-- Keeps field name as type param
data NamedFieldVar a name where
  NamedFieldVar
    :: IsObject (GetFieldType a name)
    => { unFieldVar :: Var (GetFieldType a name)
       }
    -> NamedFieldVar a name

-- | Variable exposed to a user.
--
-- 'Var' represents the tree of fields.
-- Each field is 'Var' itself:
-- either a value on the stack or 'Rec' of its direct fields.
type Var a = IndigoObjectF (NamedFieldVar a) a

-- | Like 'NamedFieldVar', but this one doesn't keep name of a field
data TypedFieldVar a where
  TypedFieldVar :: IsObject a => Var a -> TypedFieldVar a

namedToTypedFieldVar :: forall a name . NamedFieldVar a name -> TypedFieldVar (GetFieldType a name)
namedToTypedFieldVar (NamedFieldVar f) = TypedFieldVar f

typedToNamedFieldVar :: forall a name . TypedFieldVar (GetFieldType a name) -> NamedFieldVar a name
typedToNamedFieldVar (TypedFieldVar f) = NamedFieldVar f

----------------------------------------------------------------------------
-- IsObject type class
----------------------------------------------------------------------------

class IsObject' (TypeDecision a) a => IsObject a
instance IsObject' (TypeDecision a) a => IsObject a

type FieldTypes a = MapGFT a (ConstructorFieldNames a)

type ToDeconstructC a =
  ( InstrDeconstructC a
  , KnownList (FieldTypes a)
  , AllConstrained KnownValue (FieldTypes a)
  )

type ToConstructC a =
  ( KnownValue a
  , InstrConstructC a
  , RMap (ConstructorFieldNames a)
  , RMap (ConstructorFieldTypes a)
  , RMap (FieldTypes a)
  , KnownList (ConstructorFieldNames a)
  , CastFieldConstructors (FieldTypes a) (ConstructorFieldTypes a)
  )

type ComplexObjectC a =
  ( ToDeconstructC a
  , ToConstructC a
  , AllConstrained IsObject (FieldTypes a)
  )

-- | Type class instantiated for all possible Indigo types
class KnownValue a => IsObject' (decision :: Decision) a where
  complexObjectDict' :: Maybe (Dict (ComplexObjectC a))

instance KnownValue a => IsObject' 'PrimitiveD a where
  complexObjectDict' = Nothing

instance KnownValue a => IsObject' 'SumTypeD a where
  complexObjectDict' = Nothing

instance ComplexObjectC a => IsObject' 'ProductTypeD a where
  complexObjectDict' = Just Dict

complexObjectDict :: forall a . IsObject a => Maybe (Dict (ComplexObjectC a))
complexObjectDict = complexObjectDict' @(TypeDecision a) @a

-- | Decide whether type is either primitive or ADT
type TypeDecision a = Decide (IsPrimitiveValue a) (IsSumType (G.Rep a))

data Decision
  = PrimitiveD
  | SumTypeD
  | ProductTypeD

type family Decide flagPrimitive flagSumType where
  Decide 'True _ = 'PrimitiveD
  Decide 'False 'True = 'SumTypeD
  Decide 'False 'False = 'ProductTypeD

type family IsSumType x where
  IsSumType (G.D1 _ x) = IsSumType x
  IsSumType (G.C1 _ x) = IsSumType x
  IsSumType (G.M1 _ _ x) = IsSumType x
  IsSumType (_ G.:*: _) = 'False
  IsSumType (G.Rec0 _) = 'False
  IsSumType G.V1 = 'False
  IsSumType G.U1 = 'False
  IsSumType (_ G.:+: _) = 'True

----------------------------------------------------------------------------
-- Stack operations
----------------------------------------------------------------------------

-- | Given a 'MetaData' and a @Peano@ singleton for a depth, it puts a new 'Var'
-- at that depth (0-indexed) and returns it with the updated 'MetaData'.
--
-- If there is a 'Var' there already it is used and the 'MetaData' not changed.
withVarAt
  :: (KnownValue a, a ~ At n inp, RequireLongerThan inp n)
  => MetaData inp
  -> Sing n
  -> (MetaData inp, Var a)
withVarAt md@(MetaData (top :& xs) ref) = \case
  SS n -> first (appendToStack top) $ withVarAt (MetaData xs ref) n
  SZ -> case top of
    Ref matRef -> (md, Cell matRef)
    NoRef -> (MetaData (Ref ref :& xs) (ref + 1), Cell ref)
  where
    appendToStack :: StkEl x -> MetaData inp -> MetaData (x ': inp)
    appendToStack v (MetaData st r) = MetaData (v :& st) r

-- | Create a variable referencing the element on top of the stack.
makeTopVar :: KnownValue x => IndigoState (x & inp) (x & inp) (Var x)
makeTopVar = iget >>= \md ->
  let (newMd, var) = withVarAt md SZ
  in iput $ GenCode var newMd L.nop L.nop

-- | Push a new stack element with a reference to it.
-- Return the variable referencing this element.
pushRefMd :: KnownValue x => MetaData stk -> (Var x, MetaData (x & stk))
pushRefMd (MetaData stk cnt) = (Cell cnt, MetaData (Ref cnt :& stk) (cnt + 1))

-- | Push a new stack element without a reference to it.
pushNoRefMd :: KnownValue a => MetaData inp -> MetaData (a & inp)
pushNoRefMd (MetaData xs ref) = MetaData (NoRef :& xs) ref

-- | Remove the top element of the stack.
-- It's supposed that no variable refers to this element.
popNoRefMd :: MetaData (a & inp) -> MetaData inp
popNoRefMd (MetaData (NoRef :& xs) ref) = MetaData xs ref
popNoRefMd (MetaData (Ref refId :& _) _) =
  error $ "You try to pop stack element, which is referenced by some variable #" <> show refId

----------------------------------------------------------------------------
-- Operations/Storage variables
----------------------------------------------------------------------------

type Ops = [Operation]

-- | Allows to get a variable with operations
type HasSideEffects = Given (Var Ops)

-- | Return a variable which refers to a stack cell with operations
operationsVar :: HasSideEffects => Var Ops
operationsVar = given

-- This storage machinery is here to avoid cyclic deps

-- | Allows to get a variable with storage
type HasStorage st = Given (Var st)

-- | Return a variable which refers to a stack cell with storage
storageVar :: HasStorage st => Var st
storageVar = given