module Indigo.Common.Var
(
Var (..)
, RefId
, StackVars (..)
, StackVars'
, StkEl (..)
, emptyStack
, assignVarAt
, pushRef
, pushNoRef
, popNoRef
, 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
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
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
data StackVars (stk :: [Kind.Type]) where
StkElements :: Rec StkEl stk -> StackVars stk
FailureStack :: StackVars stk
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
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
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)
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
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
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
type Ops = [Operation]
type HasSideEffects = Given (Var Ops)
operationsVar :: HasSideEffects => Var Ops
operationsVar :: HasSideEffects => Var Ops
operationsVar = Var Ops
forall a. Given a => a
given
type HasStorage st = (Given (Var st), KnownValue st)
storageVar :: HasStorage st => Var st
storageVar :: forall st. HasStorage st => Var st
storageVar = Var st
forall a. Given a => a
given