Object.hs

-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# LANGUAGE QuantifiedConstraints #-}

module Indigo.Common.Object
  ( IndigoObjectF (..)
  , NamedFieldObj (..)
  , TypedFieldObj (..)
  , FieldTypes
  , Object
  , SomeObject (..)
  , namedToTypedRec
  , typedToNamedRec
  , namedToTypedFieldObj
  , typedToNamedFieldObj

  , IsObject
  , complexObjectDict
  , ComplexObjectC
  , castFieldConstructors
  , withInstrDeconstructC
  ) where

import Data.Constraint (Dict(..))
import Data.Vinyl (RMap, RecordToList)
import Data.Vinyl.TypeLevel (AllConstrained)
import GHC.Generics qualified as G

import Indigo.Backend.Prelude
import Indigo.Common.Var (RefId)
import Indigo.Lorentz
import Morley.Michelson.Typed (IsPrimitiveValue, ToTs)
import Morley.Michelson.Typed.Haskell.Instr.Product
  (CastFieldConstructors(..), ConstructorFieldNames, FieldConstructor(..), GetFieldType,
  InstrDeconstructC)
import Morley.Util.Type (KList(..), KnownList(..), type (++))

----------------------------------------------------------------------------
-- IndigoObjectF
----------------------------------------------------------------------------

-- | 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.
  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 Objiable.
-- Keeps field name as type param
data NamedFieldObj a name where
  NamedFieldObj
    :: IsObject (GetFieldType a name)
    => { unFieldObj :: Object (GetFieldType a name)
       }
    -> NamedFieldObj a name

type Object a = IndigoObjectF (NamedFieldObj a) a

data SomeObject where
  SomeObject :: IsObject a => Object a -> SomeObject

-- | Like 'NamedFieldObj', but this one doesn't keep name of a field
data TypedFieldObj a where
  TypedFieldObj :: IsObject a => Object a -> TypedFieldObj a

namedToTypedFieldObj :: forall a name . NamedFieldObj a name -> TypedFieldObj (GetFieldType a name)
namedToTypedFieldObj (NamedFieldObj f) = TypedFieldObj f

typedToNamedFieldObj :: forall a name . TypedFieldObj (GetFieldType a name) -> NamedFieldObj a name
typedToNamedFieldObj (TypedFieldObj f) = NamedFieldObj 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)

-- | Simply a synonym for an unwieldy constraint.
type InstrDeconstructCClassConstraint a st =
  ( InstrDeconstructC a (ToTs st)
  , ToTs (ConstructorFieldTypes a) ++ (ToTs st) ~ ToTs (ConstructorFieldTypes a ++ st)
  )

-- | We need this because 'InstrDeconstructC' is a constraint synonym, and parts
-- of it aren't exported from morley. Hence can't declare a quantified
-- constraint over it. And we really don't want to carry input stack everywhere
-- explicitly, hence why we want a quantified constraint.
class InstrDeconstructCClassConstraint a st => InstrDeconstructCClass (a :: Type) (st :: [Type])
instance InstrDeconstructCClassConstraint a st => InstrDeconstructCClass a st

-- | Simply a synonym for a quantified constraint, because we can't use a
-- quantified constraint in a synonym tuple.
class (forall st. InstrDeconstructCClass a st) => InstrDeconstructCGeneral a
instance (forall st. InstrDeconstructCClass a st) => InstrDeconstructCGeneral a

-- | Produce evidence of 'InstrDeconstructC' for a concrete input stack, and run
-- a computation with it.
withInstrDeconstructC
  :: forall a st r. InstrDeconstructCGeneral a
  => (InstrDeconstructCClass a st => r) -> r
withInstrDeconstructC f = f

type ToDeconstructC a =
  ( InstrDeconstructCGeneral a
  , KnownList (FieldTypes a)
  , AllConstrained KnownValue (FieldTypes a)
  , FieldTypes a ~ ConstructorFieldTypes 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)
  , RecordToList (FieldTypes a) -- for Buildable
  )

-- | 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