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

module Indigo.Internal.Var
  ( -- * Variables
    Var (..)
  , RefId
  , StackVars (..)
  , StackVars'
  , StkEl (..)

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

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

import qualified Data.Kind as Kind
import Data.Reflection (Given(..))
import Data.Singletons (Sing)
import Data.Type.Equality (TestEquality(..))
import Data.Typeable (eqT)
import Fmt (Buildable(..), pretty)

import Indigo.Backend.Prelude
import Indigo.Lorentz
import Util.Peano

----------------------------------------------------------------------------
-- 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
$cp1Ord :: Eq RefId
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
$cp2Real :: Ord RefId
$cp1Real :: Num RefId
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, 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 r :: Word
r) = "#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 => StkEl a
  Ref :: KnownValue a => RefId -> StkEl a

instance TestEquality StkEl where
  testEquality :: StkEl a -> StkEl b -> Maybe (a :~: b)
testEquality NoRef NoRef = Maybe (a :~: b)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  testEquality (Ref _) (Ref _) = Maybe (a :~: b)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  testEquality (Ref _) NoRef = Maybe (a :~: b)
forall k (a :: k) (b :: k).
(Typeable a, Typeable b) =>
Maybe (a :~: b)
eqT
  testEquality NoRef (Ref _) = 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 r :: Word
r)) = "$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
    FailureStack -> Text -> StackVars (x : xs)
forall a. HasCallStack => Text -> a
error "impossible happened"
    StkElements rc :: 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 => 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 :: Var a -> StackVars inp -> Sing n -> StackVars inp
assignVarAt _ FailureStack = StackVars inp -> Sing n -> StackVars inp
forall a b. a -> b -> a
const (StackVars inp -> Sing n -> StackVars inp)
-> StackVars inp -> Sing n -> StackVars inp
forall a b. (a -> b) -> a -> b
$ Text -> StackVars inp
forall a. HasCallStack => Text -> a
error "You try to assing var against failure stack"
assignVarAt var :: Var a
var@(Var varRef :: RefId
varRef) st :: StackVars inp
st@(StkElements (top :: StkEl r
top :& xs :: Rec StkEl rs
xs)) = \case
  SS 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 inp) -> StackVars rs -> StackVars inp
forall a b. (a -> b) -> a -> b
$ Var a -> StackVars rs -> Sing n1 -> 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 n1
SingNat n1
n
  SZ -> case StkEl r
top of
    Ref mdRef :: RefId
mdRef | RefId
mdRef RefId -> RefId -> Bool
forall a. Eq a => a -> a -> Bool
== RefId
varRef -> StackVars inp
st
    Ref _ -> Text -> StackVars inp
forall a. HasCallStack => Text -> a
error "Tried to assign a Var to an already referenced value"
    NoRef -> Rec StkEl (a : rs) -> StackVars inp
forall (stk :: [*]). Rec StkEl stk -> StackVars stk
StkElements (Rec StkEl (a : rs) -> StackVars inp)
-> Rec StkEl (a : rs) -> StackVars inp
forall a b. (a -> b) -> a -> b
$ RefId -> StkEl a
forall a. KnownValue 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 :: StkEl x -> StackVars inp -> StackVars (x : inp)
appendToStack _ FailureStack = Text -> StackVars (x : inp)
forall a. HasCallStack => Text -> a
error "append to failure stack"
    appendToStack v :: StkEl x
v (StkElements s :: 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 :: Var a -> StackVars inp -> StackVars (a : inp)
pushRef _ FailureStack = Text -> StackVars (a : inp)
forall a. HasCallStack => Text -> a
error "You try to push ref to failure stack"
pushRef (Var ref :: RefId
ref) (StkElements xs :: 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 => 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 :: StackVars inp -> StackVars (a : inp)
pushNoRef FailureStack = Text -> StackVars (a : inp)
forall a. HasCallStack => Text -> a
error "You try to push no-ref to failure stack"
pushNoRef (StkElements xs :: 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 => 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 :: StackVars (a : inp) -> StackVars inp
popNoRef FailureStack = Text -> StackVars inp
forall a. HasCallStack => Text -> a
error "You try to pop from failure stack"
popNoRef (StkElements (NoRef :& xs :: 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
refId :& _)) =
  Text -> StackVars inp
forall a. HasCallStack => Text -> a
error (Text -> StackVars inp) -> Text -> StackVars 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), KnownValue 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