{-# OPTIONS_GHC -Wno-orphans #-}
module Lorentz.Zip
( ZipInstr (..)
, ZipInstrs
, zippingStack
, unzippingStack
) where
import Prelude hiding (drop)
import qualified Data.Kind as Kind
import Lorentz.Base
import Michelson.Typed
class ZipInstr (s :: [Kind.Type]) where
type ZippedStack s :: Kind.Type
zipInstr :: s :-> '[ZippedStack s]
unzipInstr :: '[ZippedStack s] :-> s
(##) :: (a :-> b) -> (b :-> c) -> (a :-> c)
l ## r = case (l, r) of
(I Nop, I x) -> I x
(I x, I Nop) -> I x
_ -> l # r
instance ZipInstr '[] where
type ZippedStack '[] = ()
zipInstr = I UNIT
unzipInstr = I DROP
instance ZipInstr '[a] where
type ZippedStack '[a] = a
zipInstr = I Nop
unzipInstr = I Nop
instance ZipInstr ((a, b) ': s) => ZipInstr (a ': b ': s) where
type ZippedStack (a ': b ': s) = ZippedStack ((a, b) ': s)
zipInstr = I PAIR ## zipInstr @((a, b) ': s)
unzipInstr = unzipInstr @((a, b) ': s) ## I (DUP `Seq` CAR `Seq` DIP CDR)
type ZipInstrs ss = Each '[ZipInstr] ss
zippingStack
:: ZipInstrs [inp, out]
=> inp :-> out -> Lambda (ZippedStack inp) (ZippedStack out)
zippingStack code = unzipInstr ## code ## zipInstr
unzippingStack
:: ZipInstrs [inp, out]
=> Lambda (ZippedStack inp) (ZippedStack out) -> inp :-> out
unzippingStack code = zipInstr ## code ## unzipInstr
instance (ZipInstr inp, ZipInstr out) => IsoValue (inp :-> out) where
type ToT (inp :-> out) = 'TLambda (ToT (ZippedStack inp)) (ToT (ZippedStack out))
toVal i = VLam . unLorentzInstr $ zippingStack i
fromVal (VLam i) = zipInstr ## LorentzInstr i ## unzipInstr