-- 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 :: (forall (name :: Symbol). f name -> g (GetFieldType a name))
-> Rec f (ConstructorFieldNames a) -> Rec g (FieldTypes a)
namedToTypedRec fun :: forall (name :: Symbol). f name -> g (GetFieldType a name)
fun = Rec f (ConstructorFieldNames a) -> Rec g (FieldTypes a)
forall (rs :: [Symbol]). Rec f rs -> Rec g (MapGFT a rs)
namedToTypedRecImpl
  where
    namedToTypedRecImpl :: Rec f rs -> Rec g (MapGFT a rs)
    namedToTypedRecImpl :: Rec f rs -> Rec g (MapGFT a rs)
namedToTypedRecImpl RNil = Rec g (MapGFT a rs)
forall u (a :: u -> *). Rec a '[]
RNil
    namedToTypedRecImpl (v :: f r
v :& xs :: Rec f rs
xs) = f r -> g (GetFieldType a r)
forall (name :: Symbol). f name -> g (GetFieldType a name)
fun f r
v g (GetFieldType a r)
-> Rec g (MapGFT a rs) -> Rec g (GetFieldType a r : MapGFT a rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec f rs -> Rec g (MapGFT a rs)
forall (rs :: [Symbol]). Rec f rs -> Rec g (MapGFT a rs)
namedToTypedRecImpl Rec f rs
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 :: (forall (name :: Symbol). f (GetFieldType a name) -> g name)
-> Rec f (FieldTypes a) -> Rec g (ConstructorFieldNames a)
typedToNamedRec fun :: forall (name :: Symbol). f (GetFieldType a name) -> g name
fun = Rec f (FieldTypes a) -> Rec g (ConstructorFieldNames a)
forall (rs :: [Symbol]).
KnownList rs =>
Rec f (MapGFT a rs) -> Rec g rs
typedToNamedRecImpl
  where
    typedToNamedRecImpl :: forall rs . KnownList rs => Rec f (MapGFT a rs) -> Rec g rs
    typedToNamedRecImpl :: Rec f (MapGFT a rs) -> Rec g rs
typedToNamedRecImpl re :: Rec f (MapGFT a rs)
re = case (KnownList rs => KList rs
forall k (l :: [k]). KnownList l => KList l
klist @rs, Rec f (MapGFT a rs)
re) of
      (KNil, RNil)  -> Rec g rs
forall u (a :: u -> *). Rec a '[]
RNil
      (KCons (Proxy x
_ :: Proxy nm) (Proxy xs
_ :: Proxy rs'), v :& vs) -> f (GetFieldType a x) -> g x
forall (name :: Symbol). f (GetFieldType a name) -> g name
fun f r
f (GetFieldType a x)
v g x -> Rec g xs -> Rec g (x : xs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec f (MapGFT a xs) -> Rec g xs
forall (rs :: [Symbol]).
KnownList rs =>
Rec f (MapGFT a rs) -> Rec g rs
typedToNamedRecImpl Rec f rs
Rec f (MapGFT a xs)
vs

castFieldConstructors
  :: forall a st . CastFieldConstructors (FieldTypes a) (ConstructorFieldTypes a)
  => Rec (FieldConstructor st) (FieldTypes a) -> Rec (FieldConstructor st) (ConstructorFieldTypes a)
castFieldConstructors :: Rec (FieldConstructor st) (FieldTypes a)
-> Rec (FieldConstructor st) (ConstructorFieldTypes a)
castFieldConstructors = Rec (FieldConstructor st) (FieldTypes a)
-> Rec (FieldConstructor st) (ConstructorFieldTypes a)
forall (xs :: [*]) (ys :: [*]) k (st :: [k]).
CastFieldConstructors xs ys =>
Rec (FieldConstructor st) xs -> Rec (FieldConstructor st) ys
castFieldConstructorsImpl

-- | Auxiliary datatype to define a variable.
-- Keeps field name as type param
data NamedFieldVar a name where
  NamedFieldVar
    :: IsObject (GetFieldType a name)
    => { NamedFieldVar a name -> Var (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 a name -> TypedFieldVar (GetFieldType a name)
namedToTypedFieldVar (NamedFieldVar f :: Var (GetFieldType a name)
f) = Var (GetFieldType a name) -> TypedFieldVar (GetFieldType a name)
forall a. IsObject a => Var a -> TypedFieldVar a
TypedFieldVar Var (GetFieldType a name)
f

typedToNamedFieldVar :: forall a name . TypedFieldVar (GetFieldType a name) -> NamedFieldVar a name
typedToNamedFieldVar :: TypedFieldVar (GetFieldType a name) -> NamedFieldVar a name
typedToNamedFieldVar (TypedFieldVar f :: Var (GetFieldType a name)
f) = Var (GetFieldType a name) -> NamedFieldVar a name
forall a (name :: Symbol).
IsObject (GetFieldType a name) =>
Var (GetFieldType a name) -> NamedFieldVar a name
NamedFieldVar Var (GetFieldType a name)
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' :: Maybe (Dict (ComplexObjectC a))
complexObjectDict' = Maybe (Dict (ComplexObjectC a))
forall a. Maybe a
Nothing

instance KnownValue a => IsObject' 'SumTypeD a where
  complexObjectDict' :: Maybe (Dict (ComplexObjectC a))
complexObjectDict' = Maybe (Dict (ComplexObjectC a))
forall a. Maybe a
Nothing

instance ComplexObjectC a => IsObject' 'ProductTypeD a where
  complexObjectDict' :: Maybe (Dict (ComplexObjectC a))
complexObjectDict' = Dict
  ((((IsoValue a, Generic a,
      GValueType (Rep a) ~ GValueType (Rep a)),
     GInstrDeconstruct (Rep a)),
    KnownList (MapGFT a (GFieldNames (Rep a))),
    AllConstrained KnownValue (MapGFT a (GFieldNames (Rep a)))),
   (KnownValue a,
    ((IsoValue a, Generic a, GValueType (Rep a) ~ GValueType (Rep a)),
     GInstrConstruct (Rep a)),
    RMap (GFieldNames (Rep a)), RMap (GFieldTypes (Rep a)),
    RMap (MapGFT a (GFieldNames (Rep a))),
    KnownList (GFieldNames (Rep a)),
    CastFieldConstructors
      (MapGFT a (GFieldNames (Rep a))) (GFieldTypes (Rep a))),
   AllConstrained IsObject (MapGFT a (GFieldNames (Rep a))))
-> Maybe
     (Dict
        ((((IsoValue a, Generic a,
            GValueType (Rep a) ~ GValueType (Rep a)),
           GInstrDeconstruct (Rep a)),
          KnownList (MapGFT a (GFieldNames (Rep a))),
          AllConstrained KnownValue (MapGFT a (GFieldNames (Rep a)))),
         (KnownValue a,
          ((IsoValue a, Generic a, GValueType (Rep a) ~ GValueType (Rep a)),
           GInstrConstruct (Rep a)),
          RMap (GFieldNames (Rep a)), RMap (GFieldTypes (Rep a)),
          RMap (MapGFT a (GFieldNames (Rep a))),
          KnownList (GFieldNames (Rep a)),
          CastFieldConstructors
            (MapGFT a (GFieldNames (Rep a))) (GFieldTypes (Rep a))),
         AllConstrained IsObject (MapGFT a (GFieldNames (Rep a)))))
forall a. a -> Maybe a
Just Dict
  ((((IsoValue a, Generic a,
      GValueType (Rep a) ~ GValueType (Rep a)),
     GInstrDeconstruct (Rep a)),
    KnownList (MapGFT a (GFieldNames (Rep a))),
    AllConstrained KnownValue (MapGFT a (GFieldNames (Rep a)))),
   (KnownValue a,
    ((IsoValue a, Generic a, GValueType (Rep a) ~ GValueType (Rep a)),
     GInstrConstruct (Rep a)),
    RMap (GFieldNames (Rep a)), RMap (GFieldTypes (Rep a)),
    RMap (MapGFT a (GFieldNames (Rep a))),
    KnownList (GFieldNames (Rep a)),
    CastFieldConstructors
      (MapGFT a (GFieldNames (Rep a))) (GFieldTypes (Rep a))),
   AllConstrained IsObject (MapGFT a (GFieldNames (Rep a))))
forall (a :: Constraint). a => Dict a
Dict

complexObjectDict :: forall a . IsObject a => Maybe (Dict (ComplexObjectC a))
complexObjectDict :: Maybe (Dict (ComplexObjectC a))
complexObjectDict = IsObject' (TypeDecision a) a => Maybe (Dict (ComplexObjectC a))
forall (decision :: Decision) a.
IsObject' decision a =>
Maybe (Dict (ComplexObjectC a))
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 :: MetaData inp -> Sing n -> (MetaData inp, Var a)
withVarAt md :: MetaData inp
md@(MetaData (top :: StkEl r
top :& xs :: Rec StkEl rs
xs) ref :: RefId
ref) = \case
  SS n -> (MetaData rs -> MetaData (r : rs))
-> (MetaData rs, Var a) -> (MetaData (r : rs), Var a)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (StkEl r -> MetaData rs -> MetaData (r : rs)
forall x (inp :: [*]).
StkEl x -> MetaData inp -> MetaData (x : inp)
appendToStack StkEl r
top) ((MetaData rs, Var a) -> (MetaData inp, Var a))
-> (MetaData rs, Var a) -> (MetaData inp, Var a)
forall a b. (a -> b) -> a -> b
$ MetaData rs -> Sing n1 -> (MetaData rs, Var a)
forall a (n :: Peano) (inp :: [*]).
(KnownValue a, a ~ At n inp, RequireLongerThan inp n) =>
MetaData inp -> Sing n -> (MetaData inp, Var a)
withVarAt (Rec StkEl rs -> RefId -> MetaData rs
forall (stk :: [*]). StackVars stk -> RefId -> MetaData stk
MetaData Rec StkEl rs
xs RefId
ref) SingNat n1
Sing n1
n
  SZ -> case StkEl r
top of
    Ref matRef :: RefId
matRef -> (MetaData inp
md, RefId -> Var a
forall a (f :: Symbol -> *).
KnownValue a =>
RefId -> IndigoObjectF f a
Cell RefId
matRef)
    NoRef -> (StackVars (a : rs) -> RefId -> MetaData (a : rs)
forall (stk :: [*]). StackVars stk -> RefId -> MetaData stk
MetaData (RefId -> StkEl a
forall a. KnownValue a => RefId -> StkEl a
Ref RefId
ref StkEl a -> Rec StkEl rs -> StackVars (a : rs)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
xs) (RefId
ref RefId -> RefId -> RefId
forall a. Num a => a -> a -> a
+ 1), RefId -> Var a
forall a (f :: Symbol -> *).
KnownValue a =>
RefId -> IndigoObjectF f a
Cell RefId
ref)
  where
    appendToStack :: StkEl x -> MetaData inp -> MetaData (x ': inp)
    appendToStack :: StkEl x -> MetaData inp -> MetaData (x : inp)
appendToStack v :: StkEl x
v (MetaData st :: StackVars inp
st r :: RefId
r) = StackVars (x : inp) -> RefId -> MetaData (x : inp)
forall (stk :: [*]). StackVars stk -> RefId -> MetaData stk
MetaData (StkEl x
v StkEl x -> StackVars inp -> StackVars (x : inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StackVars inp
st) RefId
r

-- | Create a variable referencing the element on top of the stack.
makeTopVar :: KnownValue x => IndigoState (x & inp) (x & inp) (Var x)
makeTopVar :: IndigoState (x & inp) (x & inp) (Var x)
makeTopVar = IndigoState (x & inp) (x & inp) (MetaData (x & inp))
forall (inp :: [*]). IndigoState inp inp (MetaData inp)
iget IndigoState (x & inp) (x & inp) (MetaData (x & inp))
-> (MetaData (x & inp) -> IndigoState (x & inp) (x & inp) (Var x))
-> IndigoState (x & inp) (x & inp) (Var x)
forall (inp :: [*]) (out :: [*]) (out1 :: [*]) a b.
IndigoState inp out a
-> (a -> IndigoState out out1 b) -> IndigoState inp out1 b
>>= \md :: MetaData (x & inp)
md ->
  let (newMd :: MetaData (x & inp)
newMd, var :: Var x
var) = MetaData (x & inp) -> Sing 'Z -> (MetaData (x & inp), Var x)
forall a (n :: Peano) (inp :: [*]).
(KnownValue a, a ~ At n inp, RequireLongerThan inp n) =>
MetaData inp -> Sing n -> (MetaData inp, Var a)
withVarAt MetaData (x & inp)
md SingNat 'Z
Sing 'Z
SZ
  in GenCode (x & inp) (x & inp) (Var x)
-> IndigoState (x & inp) (x & inp) (Var x)
forall (inp :: [*]) (out :: [*]) a.
GenCode inp out a -> IndigoState inp out a
iput (GenCode (x & inp) (x & inp) (Var x)
 -> IndigoState (x & inp) (x & inp) (Var x))
-> GenCode (x & inp) (x & inp) (Var x)
-> IndigoState (x & inp) (x & inp) (Var x)
forall a b. (a -> b) -> a -> b
$ Var x
-> MetaData (x & inp)
-> ((x & inp) :-> (x & inp))
-> ((x & inp) :-> (x & inp))
-> GenCode (x & inp) (x & inp) (Var x)
forall (inp :: [*]) (out :: [*]) a.
a
-> MetaData out
-> (inp :-> out)
-> (out :-> inp)
-> GenCode inp out a
GenCode Var x
var MetaData (x & inp)
newMd (x & inp) :-> (x & inp)
forall (s :: [*]). s :-> s
L.nop (x & inp) :-> (x & inp)
forall (s :: [*]). s :-> s
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 -> (Var x, MetaData (x & stk))
pushRefMd (MetaData stk :: StackVars stk
stk cnt :: RefId
cnt) = (RefId -> Var x
forall a (f :: Symbol -> *).
KnownValue a =>
RefId -> IndigoObjectF f a
Cell RefId
cnt, StackVars (x & stk) -> RefId -> MetaData (x & stk)
forall (stk :: [*]). StackVars stk -> RefId -> MetaData stk
MetaData (RefId -> StkEl x
forall a. KnownValue a => RefId -> StkEl a
Ref RefId
cnt StkEl x -> StackVars stk -> StackVars (x & stk)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StackVars stk
stk) (RefId
cnt RefId -> RefId -> RefId
forall a. Num a => a -> a -> a
+ 1))

-- | Push a new stack element without a reference to it.
pushNoRefMd :: KnownValue a => MetaData inp -> MetaData (a & inp)
pushNoRefMd :: MetaData inp -> MetaData (a & inp)
pushNoRefMd (MetaData xs :: StackVars inp
xs ref :: RefId
ref) = StackVars (a & inp) -> RefId -> MetaData (a & inp)
forall (stk :: [*]). StackVars stk -> RefId -> MetaData stk
MetaData (StkEl a
forall a. KnownValue a => StkEl a
NoRef StkEl a -> StackVars inp -> StackVars (a & inp)
forall u (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& StackVars inp
xs) RefId
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 (a & inp) -> MetaData inp
popNoRefMd (MetaData (NoRef :& xs :: Rec StkEl rs
xs) ref :: RefId
ref) = Rec StkEl rs -> RefId -> MetaData rs
forall (stk :: [*]). StackVars stk -> RefId -> MetaData stk
MetaData Rec StkEl rs
xs RefId
ref
popNoRefMd (MetaData (Ref refId :: RefId
refId :& _) _) =
  Text -> MetaData inp
forall a. HasCallStack => Text -> a
error (Text -> MetaData inp) -> Text -> MetaData inp
forall a b. (a -> b) -> a -> b
$ "You try to pop stack element, which is referenced by some variable #" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RefId -> Text
forall b a. (Show a, IsString b) => a -> b
show RefId
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 :: Var Ops
operationsVar = Var Ops
forall a. Given a => a
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 :: Var st
storageVar = Var st
forall a. Given a => a
given