-- 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 (Int -> RefId -> ShowS
[RefId] -> ShowS
RefId -> String
(Int -> RefId -> ShowS)
-> (RefId -> String) -> ([RefId] -> ShowS) -> Show RefId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RefId] -> ShowS
$cshowList :: [RefId] -> ShowS
show :: RefId -> String
$cshow :: RefId -> String
showsPrec :: Int -> RefId -> ShowS
$cshowsPrec :: Int -> RefId -> ShowS
Show, (forall x. RefId -> Rep RefId x)
-> (forall x. Rep RefId x -> RefId) -> Generic RefId
forall x. Rep RefId x -> RefId
forall x. RefId -> Rep RefId x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep RefId x -> RefId
$cfrom :: forall x. RefId -> Rep RefId x
Generic)
  deriving newtype (RefId -> RefId -> Bool
(RefId -> RefId -> Bool) -> (RefId -> RefId -> Bool) -> Eq RefId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RefId -> RefId -> Bool
$c/= :: RefId -> RefId -> Bool
== :: RefId -> RefId -> Bool
$c== :: RefId -> RefId -> Bool
Eq, Eq RefId
Eq RefId
-> (RefId -> RefId -> Ordering)
-> (RefId -> RefId -> Bool)
-> (RefId -> RefId -> Bool)
-> (RefId -> RefId -> Bool)
-> (RefId -> RefId -> Bool)
-> (RefId -> RefId -> RefId)
-> (RefId -> RefId -> RefId)
-> Ord RefId
RefId -> RefId -> Bool
RefId -> RefId -> Ordering
RefId -> RefId -> RefId
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: RefId -> RefId -> RefId
$cmin :: RefId -> RefId -> RefId
max :: RefId -> RefId -> RefId
$cmax :: RefId -> RefId -> RefId
>= :: RefId -> RefId -> Bool
$c>= :: RefId -> RefId -> Bool
> :: RefId -> RefId -> Bool
$c> :: RefId -> RefId -> Bool
<= :: RefId -> RefId -> Bool
$c<= :: RefId -> RefId -> Bool
< :: RefId -> RefId -> Bool
$c< :: RefId -> RefId -> Bool
compare :: RefId -> RefId -> Ordering
$ccompare :: RefId -> RefId -> Ordering
Ord, Num RefId
Ord RefId
Num RefId -> Ord RefId -> (RefId -> Rational) -> Real RefId
RefId -> Rational
forall a. Num a -> Ord a -> (a -> Rational) -> Real a
toRational :: RefId -> Rational
$ctoRational :: RefId -> Rational
Real, Integer -> RefId
RefId -> RefId
RefId -> RefId -> RefId
(RefId -> RefId -> RefId)
-> (RefId -> RefId -> RefId)
-> (RefId -> RefId -> RefId)
-> (RefId -> RefId)
-> (RefId -> RefId)
-> (RefId -> RefId)
-> (Integer -> RefId)
-> Num RefId
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
fromInteger :: Integer -> RefId
$cfromInteger :: Integer -> RefId
signum :: RefId -> RefId
$csignum :: RefId -> RefId
abs :: RefId -> RefId
$cabs :: RefId -> RefId
negate :: RefId -> RefId
$cnegate :: RefId -> RefId
* :: RefId -> RefId -> RefId
$c* :: RefId -> RefId -> RefId
- :: RefId -> RefId -> RefId
$c- :: RefId -> RefId -> RefId
+ :: RefId -> RefId -> RefId
$c+ :: RefId -> RefId -> RefId
Num, Enum RefId
Real RefId
Real RefId
-> Enum RefId
-> (RefId -> RefId -> RefId)
-> (RefId -> RefId -> RefId)
-> (RefId -> RefId -> RefId)
-> (RefId -> RefId -> RefId)
-> (RefId -> RefId -> (RefId, RefId))
-> (RefId -> RefId -> (RefId, RefId))
-> (RefId -> Integer)
-> Integral RefId
RefId -> Integer
RefId -> RefId -> (RefId, RefId)
RefId -> RefId -> RefId
forall a.
Real a
-> Enum a
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> (a, a))
-> (a -> a -> (a, a))
-> (a -> Integer)
-> Integral a
toInteger :: RefId -> Integer
$ctoInteger :: RefId -> Integer
divMod :: RefId -> RefId -> (RefId, RefId)
$cdivMod :: RefId -> RefId -> (RefId, RefId)
quotRem :: RefId -> RefId -> (RefId, RefId)
$cquotRem :: RefId -> RefId -> (RefId, RefId)
mod :: RefId -> RefId -> RefId
$cmod :: RefId -> RefId -> RefId
div :: RefId -> RefId -> RefId
$cdiv :: RefId -> RefId -> RefId
rem :: RefId -> RefId -> RefId
$crem :: RefId -> RefId -> RefId
quot :: RefId -> RefId -> RefId
$cquot :: RefId -> RefId -> RefId
Integral, Int -> RefId
RefId -> Int
RefId -> [RefId]
RefId -> RefId
RefId -> RefId -> [RefId]
RefId -> RefId -> RefId -> [RefId]
(RefId -> RefId)
-> (RefId -> RefId)
-> (Int -> RefId)
-> (RefId -> Int)
-> (RefId -> [RefId])
-> (RefId -> RefId -> [RefId])
-> (RefId -> RefId -> [RefId])
-> (RefId -> RefId -> RefId -> [RefId])
-> Enum RefId
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: RefId -> RefId -> RefId -> [RefId]
$cenumFromThenTo :: RefId -> RefId -> RefId -> [RefId]
enumFromTo :: RefId -> RefId -> [RefId]
$cenumFromTo :: RefId -> RefId -> [RefId]
enumFromThen :: RefId -> RefId -> [RefId]
$cenumFromThen :: RefId -> RefId -> [RefId]
enumFrom :: RefId -> [RefId]
$cenumFrom :: RefId -> [RefId]
fromEnum :: RefId -> Int
$cfromEnum :: RefId -> Int
toEnum :: Int -> RefId
$ctoEnum :: Int -> RefId
pred :: RefId -> RefId
$cpred :: RefId -> RefId
succ :: RefId -> RefId
$csucc :: RefId -> RefId
Enum, RefId
RefId -> RefId -> Bounded RefId
forall a. a -> a -> Bounded a
maxBound :: RefId
$cmaxBound :: RefId
minBound :: RefId
$cminBound :: RefId
Bounded)

instance Buildable RefId where
  build :: RefId -> Builder
build (RefId Word
r) = Builder
"#ref" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Word -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty Word
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 :: forall a b. StkEl a -> StkEl b -> Maybe (a :~: b)
testEquality StkEl a
NoRef StkEl b
NoRef = Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  testEquality (Ref RefId
_) (Ref RefId
_) = Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  testEquality (Ref RefId
_) StkEl b
NoRef = Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  testEquality StkEl a
NoRef (Ref RefId
_) = Maybe (a :~: b)
forall {k} (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
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 ((forall x. Var a -> Rep (Var a) x)
-> (forall x. Rep (Var a) x -> Var a) -> Generic (Var a)
forall x. Rep (Var a) x -> Var a
forall x. Var a -> Rep (Var a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (a :: k) x. Rep (Var a) x -> Var a
forall k (a :: k) x. Var a -> Rep (Var a) x
$cto :: forall k (a :: k) x. Rep (Var a) x -> Var a
$cfrom :: forall k (a :: k) x. Var a -> Rep (Var a) x
Generic, Int -> Var a -> ShowS
[Var a] -> ShowS
Var a -> String
(Int -> Var a -> ShowS)
-> (Var a -> String) -> ([Var a] -> ShowS) -> Show (Var a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (a :: k). Int -> Var a -> ShowS
forall k (a :: k). [Var a] -> ShowS
forall k (a :: k). Var a -> String
showList :: [Var a] -> ShowS
$cshowList :: forall k (a :: k). [Var a] -> ShowS
show :: Var a -> String
$cshow :: forall k (a :: k). Var a -> String
showsPrec :: Int -> Var a -> ShowS
$cshowsPrec :: forall k (a :: k). Int -> Var a -> ShowS
Show)

instance Buildable (Var a) where
  build :: Var a -> Builder
build (Var (RefId Word
r)) = Builder
"$var" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Word -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty Word
r

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

emptyStack :: StackVars '[]
emptyStack :: StackVars '[]
emptyStack = Rec StkEl '[] -> StackVars '[]
forall (stk :: [*]). Rec StkEl stk -> StackVars stk
StkElements Rec StkEl '[]
forall {u} (a :: u -> *). Rec a '[]
RNil

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

instance (KnownValue x, Default (StackVars xs)) => Default (StackVars (x ': xs)) where
  def :: StackVars (x : xs)
def = case StackVars xs
forall a. Default a => a
def of
    StackVars xs
FailureStack -> Text -> StackVars (x : xs)
forall a. HasCallStack => Text -> a
error Text
"impossible happened"
    StkElements Rec StkEl xs
rc -> Rec StkEl (x : xs) -> StackVars (x : xs)
forall (stk :: [*]). Rec StkEl stk -> StackVars stk
StkElements (Rec StkEl (x : xs) -> StackVars (x : xs))
-> Rec StkEl (x : xs) -> StackVars (x : xs)
forall a b. (a -> b) -> a -> b
$ StkEl x
forall a. (KnownValue a, KnownIsoT a) => StkEl a
NoRef StkEl x -> Rec StkEl xs -> Rec StkEl (x : xs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl xs
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 :: forall a (n :: Peano) (inp :: [*]).
(KnownValue a, a ~ At n inp, RequireLongerThan inp n) =>
Var a -> StackVars inp -> Sing n -> StackVars inp
assignVarAt Var a
_ StackVars inp
FailureStack = StackVars inp -> SingNat n -> StackVars inp
forall a b. a -> b -> a
const (StackVars inp -> SingNat n -> StackVars inp)
-> StackVars inp -> SingNat n -> StackVars inp
forall a b. (a -> b) -> a -> b
$ Text -> StackVars inp
forall a. HasCallStack => Text -> a
error Text
"You try to assing var against failure stack"
assignVarAt var :: Var a
var@(Var RefId
varRef) st :: StackVars inp
st@(StkElements (StkEl r
top :& Rec StkEl rs
xs)) = \case
  SS Sing n
n -> StkEl r -> StackVars rs -> StackVars (r : rs)
forall x (inp :: [*]).
StkEl x -> StackVars inp -> StackVars (x : inp)
appendToStack StkEl r
top (StackVars rs -> StackVars (r : rs))
-> StackVars rs -> StackVars (r : rs)
forall a b. (a -> b) -> a -> b
$ Var a -> StackVars rs -> Sing n -> StackVars rs
forall a (n :: Peano) (inp :: [*]).
(KnownValue a, a ~ At n inp, RequireLongerThan inp n) =>
Var a -> StackVars inp -> Sing n -> StackVars inp
assignVarAt Var a
var (Rec StkEl rs -> StackVars rs
forall (stk :: [*]). Rec StkEl stk -> StackVars stk
StkElements Rec StkEl rs
xs) Sing n
n
  Sing n
SingNat n
SZ -> case StkEl r
top of
    Ref RefId
mdRef | RefId
mdRef RefId -> RefId -> Bool
forall a. Eq a => a -> a -> Bool
== RefId
varRef -> StackVars inp
st
    Ref RefId
_ -> Text -> StackVars inp
forall a. HasCallStack => Text -> a
error Text
"Tried to assign a Var to an already referenced value"
    StkEl r
NoRef -> Rec StkEl (a : rs) -> StackVars (a : rs)
forall (stk :: [*]). Rec StkEl stk -> StackVars stk
StkElements (Rec StkEl (a : rs) -> StackVars (a : rs))
-> Rec StkEl (a : rs) -> StackVars (a : rs)
forall a b. (a -> b) -> a -> b
$ RefId -> StkEl a
forall a. (KnownValue a, KnownIsoT a) => RefId -> StkEl a
Ref RefId
varRef StkEl a -> Rec StkEl rs -> Rec StkEl (a : rs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl rs
xs
  where
    appendToStack :: StkEl x -> StackVars inp -> StackVars (x ': inp)
    appendToStack :: forall x (inp :: [*]).
StkEl x -> StackVars inp -> StackVars (x : inp)
appendToStack StkEl x
_ StackVars inp
FailureStack = Text -> StackVars (x : inp)
forall a. HasCallStack => Text -> a
error Text
"append to failure stack"
    appendToStack StkEl x
v (StkElements Rec StkEl inp
s) = Rec StkEl (x : inp) -> StackVars (x : inp)
forall (stk :: [*]). Rec StkEl stk -> StackVars stk
StkElements (StkEl x
v StkEl x -> Rec StkEl inp -> Rec StkEl (x : inp)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
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 :: forall a (inp :: [*]).
KnownValue a =>
Var a -> StackVars inp -> StackVars (a : inp)
pushRef Var a
_ StackVars inp
FailureStack = Text -> StackVars (a : inp)
forall a. HasCallStack => Text -> a
error Text
"You try to push ref to failure stack"
pushRef (Var RefId
ref) (StkElements Rec StkEl inp
xs) = Rec StkEl (a : inp) -> StackVars (a : inp)
forall (stk :: [*]). Rec StkEl stk -> StackVars stk
StkElements (Rec StkEl (a : inp) -> StackVars (a : inp))
-> Rec StkEl (a : inp) -> StackVars (a : inp)
forall a b. (a -> b) -> a -> b
$ RefId -> StkEl a
forall a. (KnownValue a, KnownIsoT a) => RefId -> StkEl a
Ref RefId
ref StkEl a -> Rec StkEl inp -> Rec StkEl (a : inp)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
xs

-- | Push a new stack element without a reference to it.
pushNoRef :: KnownValue a => StackVars inp -> StackVars (a : inp)
pushNoRef :: forall a (inp :: [*]).
KnownValue a =>
StackVars inp -> StackVars (a : inp)
pushNoRef StackVars inp
FailureStack = Text -> StackVars (a : inp)
forall a. HasCallStack => Text -> a
error Text
"You try to push no-ref to failure stack"
pushNoRef (StkElements Rec StkEl inp
xs) = Rec StkEl (a : inp) -> StackVars (a : inp)
forall (stk :: [*]). Rec StkEl stk -> StackVars stk
StkElements (Rec StkEl (a : inp) -> StackVars (a : inp))
-> Rec StkEl (a : inp) -> StackVars (a : inp)
forall a b. (a -> b) -> a -> b
$ StkEl a
forall a. (KnownValue a, KnownIsoT a) => StkEl a
NoRef StkEl a -> Rec StkEl inp -> Rec StkEl (a : inp)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec StkEl inp
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 :: forall a (inp :: [*]). StackVars (a : inp) -> StackVars inp
popNoRef StackVars (a : inp)
FailureStack = Text -> StackVars inp
forall a. HasCallStack => Text -> a
error Text
"You try to pop from failure stack"
popNoRef (StkElements (StkEl r
NoRef :& Rec StkEl rs
xs)) = Rec StkEl rs -> StackVars rs
forall (stk :: [*]). Rec StkEl stk -> StackVars stk
StkElements Rec StkEl rs
xs
popNoRef (StkElements (Ref RefId
refId :& Rec StkEl rs
_)) =
  Text -> StackVars inp
forall a. HasCallStack => Text -> a
error (Text -> StackVars inp) -> Text -> StackVars inp
forall a b. (a -> b) -> a -> b
$ Text
"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 a b. (Buildable a, FromBuilder b) => a -> b
pretty 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 :: HasSideEffects => 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), KnownValue st)

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