Var.hs

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

-- | Datatype representing Indigo variables and utilities for working with
-- them.
module Indigo.Common.Var
  ( -- * Variables
    Var (..)
  , RefId
  , StackVars (..)
  , StackVars'
  , StkEl (..)

  -- * Stack operations
  , emptyStack
  , assignVarAt
  , pushRef
  , pushNoRef
  , popNoRef

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

import Data.Kind qualified as Kind
import Data.Reflection (Given(..))
import Data.Singletons (Sing)
import Data.Type.Equality (TestEquality(..))
import Data.Typeable (eqT)
import Fmt (Buildable(..), pretty)
import Morley.Michelson.Typed.Haskell.Value
import Morley.Util.Peano

import Indigo.Backend.Prelude
import Indigo.Lorentz

----------------------------------------------------------------------------
-- Stack and variable definition
----------------------------------------------------------------------------

-- | Reference id to a stack cell
newtype RefId = RefId Word
  deriving stock (Show, Generic)
  deriving newtype (Eq, Ord, Real, Num, Integral, Enum, Bounded)

instance Buildable RefId where
  build (RefId r) = "#ref" <> pretty r

-- | Stack element of the symbolic interpreter.
--
-- It holds either a reference index that refers to this element
-- or just 'NoRef', indicating that there are no references
-- to this element.
data StkEl a where
  NoRef :: (KnownValue a, KnownIsoT a) => StkEl a
  Ref :: (KnownValue a, KnownIsoT a) => RefId -> StkEl a

instance TestEquality StkEl where
  testEquality NoRef NoRef = eqT
  testEquality (Ref _) (Ref _) = eqT
  testEquality (Ref _) NoRef = eqT
  testEquality NoRef (Ref _) = eqT

type StackVars' stk = Rec StkEl stk

-- | Stack of the symbolic interpreter.
data StackVars (stk :: [Kind.Type]) where
  StkElements  :: Rec StkEl stk -> StackVars stk
  FailureStack :: StackVars stk

-- | A variable referring to an element in the stack.
data Var a = Var RefId
  deriving stock (Generic, Show)

instance Buildable (Var a) where
  build (Var (RefId r)) = "$var" <> pretty r

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

emptyStack :: StackVars '[]
emptyStack = StkElements RNil

instance Default (StackVars '[]) where
  def = emptyStack

instance (KnownValue x, Default (StackVars xs)) => Default (StackVars (x ': xs)) where
  def = case def of
    FailureStack -> error "impossible happened"
    StkElements rc -> StkElements $ NoRef :& rc

-- | Given a 'StackVars' and a @Peano@ singleton for a depth, it puts a new 'Var'
-- at that depth (0-indexed) and returns it with the updated 'StackVars'.
--
-- If there is a 'Var' there already it is used and the 'StackVars' not changed.
assignVarAt
  :: (KnownValue a, a ~ At n inp, RequireLongerThan inp n)
  => Var a
  -> StackVars inp
  -> Sing n
  -> StackVars inp
assignVarAt _ FailureStack = const $ error "You try to assing var against failure stack"
assignVarAt var@(Var varRef) st@(StkElements (top :& xs)) = \case
  SS n -> appendToStack top $ assignVarAt var (StkElements xs) n
  SZ -> case top of
    Ref mdRef | mdRef == varRef -> st
    Ref _ -> error "Tried to assign a Var to an already referenced value"
    NoRef -> StkElements $ Ref varRef :& xs
  where
    appendToStack :: StkEl x -> StackVars inp -> StackVars (x ': inp)
    appendToStack _ FailureStack = error "append to failure stack"
    appendToStack v (StkElements s) = StkElements (v :& s)

-- | Push a new stack element with a reference to it, given the variable.
pushRef :: KnownValue a => Var a -> StackVars inp -> StackVars (a : inp)
pushRef _ FailureStack = error "You try to push ref to failure stack"
pushRef (Var ref) (StkElements xs) = StkElements $ Ref ref :& xs

-- | Push a new stack element without a reference to it.
pushNoRef :: KnownValue a => StackVars inp -> StackVars (a : inp)
pushNoRef FailureStack = error "You try to push no-ref to failure stack"
pushNoRef (StkElements xs) = StkElements $ NoRef :& xs

-- | Remove the top element of the stack.
-- It's supposed that no variable refers to this element.
popNoRef :: StackVars (a : inp) -> StackVars inp
popNoRef FailureStack = error "You try to pop from failure stack"
popNoRef (StkElements (NoRef :& xs)) = StkElements xs
popNoRef (StkElements (Ref refId :& _)) =
  error $ "You try to pop stack element, which is referenced by some variable #" <> pretty 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), KnownValue st)

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