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

module Michelson.Typed.Existential
  ( SomeConstant (..)
  , SomeConstrainedValue (..)
  , SomeContract (..)
  , SomeContractAndStorage (..)
  , SomeIsoValue (..)
  , SomeValue (..)
  , SomeStorage(..)
  ) where

import Fmt (Buildable(..))

import Michelson.Typed.Aliases
import Michelson.Typed.Convert ()
import Michelson.Typed.Haskell.Value (KnownIsoT)
import Michelson.Typed.Instr (Contract(..))
import Michelson.Typed.Scope
import Michelson.Typed.T (T(..))
import Util.Sing (eqParamSing)

data SomeConstrainedValue (c :: T -> Constraint) where
  SomeConstrainedValue
    :: forall (t :: T) (c :: T -> Constraint)
    . (c t)
    => Value t
    -> SomeConstrainedValue c

deriving stock instance Show (SomeConstrainedValue c)

-- TODO
-- @gromak: perhaps we should implement `SomeValue` in terms of
-- `SomeConstrainedValue`, but it will require changing quite a lot of code,
-- so it is postponed.

data SomeValue where
  SomeValue :: SingI t => Value t -> SomeValue

deriving stock instance Show SomeValue

instance Eq SomeValue where
  SomeValue Value t
v1 == :: SomeValue -> SomeValue -> Bool
== SomeValue Value t
v2 = Value t
v1 Value t -> Value t -> Bool
forall k (a1 :: k) (a2 :: k) (t :: k -> *).
(SingI a1, SingI a2, SDecide k, Eq (t a1)) =>
t a1 -> t a2 -> Bool
`eqParamSing` Value t
v2

data SomeConstant where
  SomeConstant :: (ConstantScope t, SingI t) => Value t -> SomeConstant

instance Buildable SomeConstant where
  build :: SomeConstant -> Builder
build (SomeConstant Value t
v) = Value t -> Builder
forall p. Buildable p => p -> Builder
build Value t
v

-- | Hides some Haskell value put in line with Michelson 'Value'.
data SomeIsoValue where
  SomeIsoValue :: (KnownIsoT a) => a -> SomeIsoValue

data SomeContract where
  SomeContract :: Contract cp st -> SomeContract

instance NFData SomeContract where
  rnf :: SomeContract -> ()
rnf (SomeContract Contract cp st
c) = Contract cp st -> ()
forall a. NFData a => a -> ()
rnf Contract cp st
c

deriving stock instance Show SomeContract

-- | Represents a typed contract & a storage value of the type expected by the contract.
data SomeContractAndStorage where
  SomeContractAndStorage
    :: forall cp st.
       (StorageScope st, ParameterScope cp)
       => Contract cp st
       -> Value st
       -> SomeContractAndStorage

deriving stock instance Show SomeContractAndStorage

data SomeStorage where
  SomeStorage :: forall st. StorageScope st => Value st -> SomeStorage

deriving stock instance Show SomeStorage