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

module Lorentz.Lambda
  ( WrappedLambda(..)
  , Lambda
  , mkLambda
  , mkLambdaRec
  ) where

import Data.Singletons (demote)

import Lorentz.Annotation
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Instr.Framed
import Lorentz.Value
import Lorentz.Zip
import Morley.AsRPC
import Morley.Michelson.Doc
import Morley.Michelson.Typed hiding (Contract, pattern S)
import Morley.Michelson.Typed.Contract (giveNotInView)
import Morley.Michelson.Untyped (noAnn)
import Morley.Util.Markdown
import Morley.Util.Type

-- | A helper type to construct Lorentz lambda values; Use this for lambda
-- values outside of Lorentz contracts or with @push@.
data WrappedLambda i o
  = WrappedLambda (i :-> o)
  | RecLambda (i ++ '[WrappedLambda i o] :-> o)
  deriving stock (Int -> WrappedLambda i o -> ShowS
[WrappedLambda i o] -> ShowS
WrappedLambda i o -> String
(Int -> WrappedLambda i o -> ShowS)
-> (WrappedLambda i o -> String)
-> ([WrappedLambda i o] -> ShowS)
-> Show (WrappedLambda i o)
forall (i :: [*]) (o :: [*]). Int -> WrappedLambda i o -> ShowS
forall (i :: [*]) (o :: [*]). [WrappedLambda i o] -> ShowS
forall (i :: [*]) (o :: [*]). WrappedLambda i o -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [WrappedLambda i o] -> ShowS
$cshowList :: forall (i :: [*]) (o :: [*]). [WrappedLambda i o] -> ShowS
show :: WrappedLambda i o -> String
$cshow :: forall (i :: [*]) (o :: [*]). WrappedLambda i o -> String
showsPrec :: Int -> WrappedLambda i o -> ShowS
$cshowsPrec :: forall (i :: [*]) (o :: [*]). Int -> WrappedLambda i o -> ShowS
Show, WrappedLambda i o -> WrappedLambda i o -> Bool
(WrappedLambda i o -> WrappedLambda i o -> Bool)
-> (WrappedLambda i o -> WrappedLambda i o -> Bool)
-> Eq (WrappedLambda i o)
forall (i :: [*]) (o :: [*]).
WrappedLambda i o -> WrappedLambda i o -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: WrappedLambda i o -> WrappedLambda i o -> Bool
$c/= :: forall (i :: [*]) (o :: [*]).
WrappedLambda i o -> WrappedLambda i o -> Bool
== :: WrappedLambda i o -> WrappedLambda i o -> Bool
$c== :: forall (i :: [*]) (o :: [*]).
WrappedLambda i o -> WrappedLambda i o -> Bool
Eq, (forall x. WrappedLambda i o -> Rep (WrappedLambda i o) x)
-> (forall x. Rep (WrappedLambda i o) x -> WrappedLambda i o)
-> Generic (WrappedLambda i o)
forall (i :: [*]) (o :: [*]) x.
Rep (WrappedLambda i o) x -> WrappedLambda i o
forall (i :: [*]) (o :: [*]) x.
WrappedLambda i o -> Rep (WrappedLambda i o) x
forall x. Rep (WrappedLambda i o) x -> WrappedLambda i o
forall x. WrappedLambda i o -> Rep (WrappedLambda i o) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (i :: [*]) (o :: [*]) x.
Rep (WrappedLambda i o) x -> WrappedLambda i o
$cfrom :: forall (i :: [*]) (o :: [*]) x.
WrappedLambda i o -> Rep (WrappedLambda i o) x
Generic)

instance (KnownList i, ZipInstr i, ZipInstr o) => IsoValue (WrappedLambda i o) where
  type ToT (WrappedLambda i o) = 'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))
  toVal :: WrappedLambda i o -> Value (ToT (WrappedLambda i o))
toVal (WrappedLambda i :-> o
i) = (IsNotInView =>
 RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)])
-> Value'
     Instr ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)))
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
(IsNotInView => RemFail instr '[inp] '[out])
-> Value' instr ('TLambda inp out)
mkVLam ((IsNotInView =>
  RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)])
 -> Value'
      Instr ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))))
-> (IsNotInView =>
    RemFail Instr '[ToT (ZippedStack i)] '[ToT (ZippedStack o)])
-> Value'
     Instr ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)))
forall a b. (a -> b) -> a -> b
$ ('[ZippedStack i] :-> '[ZippedStack o])
-> RemFail Instr (ToTs '[ZippedStack i]) (ToTs '[ZippedStack o])
forall (inp :: [*]) (out :: [*]).
(inp :-> out) -> RemFail Instr (ToTs inp) (ToTs out)
unLorentzInstr (('[ZippedStack i] :-> '[ZippedStack o])
 -> RemFail Instr (ToTs '[ZippedStack i]) (ToTs '[ZippedStack o]))
-> ('[ZippedStack i] :-> '[ZippedStack o])
-> RemFail Instr (ToTs '[ZippedStack i]) (ToTs '[ZippedStack o])
forall a b. (a -> b) -> a -> b
$ (i :-> o) -> '[ZippedStack i] :-> '[ZippedStack o]
forall (inp :: [*]) (out :: [*]).
ZipInstrs '[inp, out] =>
(inp :-> out) -> Fn (ZippedStack inp) (ZippedStack out)
zippingStack i :-> o
i
  toVal (RecLambda (i ++ '[WrappedLambda i o]) :-> o
i) = (IsNotInView =>
 RemFail
   Instr
   '[ToT (ZippedStack i),
     'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))]
   '[ToT (ZippedStack o)])
-> Value'
     Instr ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)))
forall (inp :: T) (out :: T) (instr :: [T] -> [T] -> *).
(SingI inp, SingI out,
 forall (i :: [T]) (o :: [T]). Show (instr i o),
 forall (i :: [T]) (o :: [T]). Eq (instr i o),
 forall (i :: [T]) (o :: [T]). NFData (instr i o)) =>
(IsNotInView => RemFail instr '[inp, 'TLambda inp out] '[out])
-> Value' instr ('TLambda inp out)
mkVLamRec ((IsNotInView =>
  RemFail
    Instr
    '[ToT (ZippedStack i),
      'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))]
    '[ToT (ZippedStack o)])
 -> Value'
      Instr ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))))
-> (IsNotInView =>
    RemFail
      Instr
      '[ToT (ZippedStack i),
        'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))]
      '[ToT (ZippedStack o)])
-> Value'
     Instr ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)))
forall a b. (a -> b) -> a -> b
$ ('[ZippedStack i, WrappedLambda i o] :-> '[ZippedStack o])
-> RemFail
     Instr
     (ToTs '[ZippedStack i, WrappedLambda i o])
     (ToTs '[ZippedStack o])
forall (inp :: [*]) (out :: [*]).
(inp :-> out) -> RemFail Instr (ToTs inp) (ToTs out)
unLorentzInstr (('[ZippedStack i, WrappedLambda i o] :-> '[ZippedStack o])
 -> RemFail
      Instr
      (ToTs '[ZippedStack i, WrappedLambda i o])
      (ToTs '[ZippedStack o]))
-> ('[ZippedStack i, WrappedLambda i o] :-> '[ZippedStack o])
-> RemFail
     Instr
     (ToTs '[ZippedStack i, WrappedLambda i o])
     (ToTs '[ZippedStack o])
forall a b. (a -> b) -> a -> b
$
    forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed @'[WrappedLambda i o] (forall (s :: [*]). ZipInstr s => '[ZippedStack s] :-> s
unzipInstr @i)
    ## i
    ## zipInstr
  fromVal :: Value (ToT (WrappedLambda i o)) -> WrappedLambda i o
fromVal (VLam (LambdaCode RemFail Instr '[inp] '[out]
i)) = (i :-> o) -> WrappedLambda i o
forall (i :: [*]) (o :: [*]). (i :-> o) -> WrappedLambda i o
WrappedLambda ((i :-> o) -> WrappedLambda i o) -> (i :-> o) -> WrappedLambda i o
forall a b. (a -> b) -> a -> b
$ ('[ZippedStack i] :-> '[ZippedStack o]) -> i :-> o
forall (inp :: [*]) (out :: [*]).
ZipInstrs '[inp, out] =>
Fn (ZippedStack inp) (ZippedStack out) -> inp :-> out
unzippingStack (('[ZippedStack i] :-> '[ZippedStack o]) -> i :-> o)
-> ('[ZippedStack i] :-> '[ZippedStack o]) -> i :-> o
forall a b. (a -> b) -> a -> b
$ RemFail Instr (ToTs '[ZippedStack i]) (ToTs '[ZippedStack o])
-> '[ZippedStack i] :-> '[ZippedStack o]
forall (inp :: [*]) (out :: [*]).
RemFail Instr (ToTs inp) (ToTs out) -> inp :-> out
LorentzInstr RemFail Instr '[inp] '[out]
RemFail Instr (ToTs '[ZippedStack i]) (ToTs '[ZippedStack o])
i
  fromVal (VLam (LambdaCodeRec RemFail Instr '[inp, 'TLambda inp out] '[out]
i)) = ((i ++ '[WrappedLambda i o]) :-> o) -> WrappedLambda i o
forall (i :: [*]) (o :: [*]).
((i ++ '[WrappedLambda i o]) :-> o) -> WrappedLambda i o
RecLambda (((i ++ '[WrappedLambda i o]) :-> o) -> WrappedLambda i o)
-> ((i ++ '[WrappedLambda i o]) :-> o) -> WrappedLambda i o
forall a b. (a -> b) -> a -> b
$
    forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed @'[WrappedLambda i o] (forall (s :: [*]). ZipInstr s => s :-> '[ZippedStack s]
zipInstr @i)
    ## LorentzInstr i
    ## unzipInstr

instance MapLorentzInstr (WrappedLambda inp out) where
  mapLorentzInstr
    :: (forall i o. (i :-> o) -> (i :-> o))
    -> WrappedLambda inp out
    -> WrappedLambda inp out
  mapLorentzInstr :: (forall (i :: [*]) (o :: [*]). (i :-> o) -> i :-> o)
-> WrappedLambda inp out -> WrappedLambda inp out
mapLorentzInstr forall (i :: [*]) (o :: [*]). (i :-> o) -> i :-> o
f = \case
    WrappedLambda inp :-> out
i -> (inp :-> out) -> WrappedLambda inp out
forall (i :: [*]) (o :: [*]). (i :-> o) -> WrappedLambda i o
WrappedLambda ((inp :-> out) -> WrappedLambda inp out)
-> (inp :-> out) -> WrappedLambda inp out
forall a b. (a -> b) -> a -> b
$ (inp :-> out) -> inp :-> out
forall (i :: [*]) (o :: [*]). (i :-> o) -> i :-> o
f inp :-> out
i
    RecLambda (inp ++ '[WrappedLambda inp out]) :-> out
i -> ((inp ++ '[WrappedLambda inp out]) :-> out)
-> WrappedLambda inp out
forall (i :: [*]) (o :: [*]).
((i ++ '[WrappedLambda i o]) :-> o) -> WrappedLambda i o
RecLambda (((inp ++ '[WrappedLambda inp out]) :-> out)
 -> WrappedLambda inp out)
-> ((inp ++ '[WrappedLambda inp out]) :-> out)
-> WrappedLambda inp out
forall a b. (a -> b) -> a -> b
$ ((inp ++ '[WrappedLambda inp out]) :-> out)
-> (inp ++ '[WrappedLambda inp out]) :-> out
forall (i :: [*]) (o :: [*]). (i :-> o) -> i :-> o
f (inp ++ '[WrappedLambda inp out]) :-> out
i

instance (Each '[HasAnnotation] '[ZippedStack i, ZippedStack o])
  => HasAnnotation (WrappedLambda i o) where
  getAnnotation :: FollowEntrypointFlag -> Notes (ToT (WrappedLambda i o))
getAnnotation FollowEntrypointFlag
b = TypeAnn
-> Notes (ToT (ZippedStack i))
-> Notes (ToT (ZippedStack o))
-> Notes ('TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o)))
forall (p :: T) (q :: T).
TypeAnn -> Notes p -> Notes q -> Notes ('TLambda p q)
NTLambda TypeAnn
forall {k} (a :: k). Annotation a
noAnn
    (forall a. HasAnnotation a => FollowEntrypointFlag -> Notes (ToT a)
getAnnotation @(ZippedStack i) FollowEntrypointFlag
b)
    (forall a. HasAnnotation a => FollowEntrypointFlag -> Notes (ToT a)
getAnnotation @(ZippedStack o) FollowEntrypointFlag
b)

instance HasRPCRepr (WrappedLambda i o) where type AsRPC (WrappedLambda i o) = WrappedLambda i o

-- | A constructor providing the required constraint for 'WrappedLambda'. This is
-- the only way to construct a lambda that uses operations forbidden in views.
mkLambda :: (IsNotInView => i :-> o) -> WrappedLambda i o
mkLambda :: forall (i :: [*]) (o :: [*]).
(IsNotInView => i :-> o) -> WrappedLambda i o
mkLambda IsNotInView => i :-> o
i = (i :-> o) -> WrappedLambda i o
forall (i :: [*]) (o :: [*]). (i :-> o) -> WrappedLambda i o
WrappedLambda ((i :-> o) -> WrappedLambda i o) -> (i :-> o) -> WrappedLambda i o
forall a b. (a -> b) -> a -> b
$ (IsNotInView => i :-> o) -> i :-> o
forall r. (IsNotInView => r) -> r
giveNotInView IsNotInView => i :-> o
i

-- | A constructor providing the required constraint for 'WrappedLambda'. This is
-- the only way to construct a lambda that uses operations forbidden in views.
mkLambdaRec :: (IsNotInView => i ++ '[WrappedLambda i o] :-> o) -> WrappedLambda i o
mkLambdaRec :: forall (i :: [*]) (o :: [*]).
(IsNotInView => (i ++ '[WrappedLambda i o]) :-> o)
-> WrappedLambda i o
mkLambdaRec IsNotInView => (i ++ '[WrappedLambda i o]) :-> o
i = ((i ++ '[WrappedLambda i o]) :-> o) -> WrappedLambda i o
forall (i :: [*]) (o :: [*]).
((i ++ '[WrappedLambda i o]) :-> o) -> WrappedLambda i o
RecLambda (((i ++ '[WrappedLambda i o]) :-> o) -> WrappedLambda i o)
-> ((i ++ '[WrappedLambda i o]) :-> o) -> WrappedLambda i o
forall a b. (a -> b) -> a -> b
$ (IsNotInView => (i ++ '[WrappedLambda i o]) :-> o)
-> (i ++ '[WrappedLambda i o]) :-> o
forall r. (IsNotInView => r) -> r
giveNotInView IsNotInView => (i ++ '[WrappedLambda i o]) :-> o
i

-- | A type synonym representing Michelson lambdas.
type Lambda i o = WrappedLambda '[i] '[o]

instance (Each [Typeable, ReifyList TypeHasDoc] [i, o])
  => TypeHasDoc (WrappedLambda i o) where
  typeDocName :: Proxy (WrappedLambda i o) -> Text
typeDocName Proxy (WrappedLambda i o)
_ = Text
"WrappedLambda (extended lambda)"
  typeDocMdReference :: Proxy (WrappedLambda i o) -> WithinParens -> Markdown
typeDocMdReference Proxy (WrappedLambda i o)
tp WithinParens
wp =
    let DocItemRef DocItemId
ctorDocItemId = DType
-> DocItemRef (DocItemPlacement DType) (DocItemReferenced DType)
forall d.
DocItem d =>
d -> DocItemRef (DocItemPlacement d) (DocItemReferenced d)
docItemRef (Proxy (WrappedLambda i o) -> DType
forall a. TypeHasDoc a => Proxy a -> DType
DType Proxy (WrappedLambda i o)
tp)
        refToThis :: Markdown
refToThis = Markdown -> DocItemId -> Markdown
forall anchor. ToAnchor anchor => Markdown -> anchor -> Markdown
mdLocalRef (Markdown -> Markdown
mdTicked Markdown
"WrappedLambda") DocItemId
ctorDocItemId
    in WithinParens -> Markdown -> Markdown
applyWithinParens WithinParens
wp (Markdown -> Markdown) -> Markdown -> Markdown
forall a b. (a -> b) -> a -> b
$
      [Markdown] -> Markdown
forall a. Monoid a => [a] -> a
mconcat ([Markdown] -> Markdown) -> [Markdown] -> Markdown
forall a b. (a -> b) -> a -> b
$ Markdown -> [Markdown] -> [Markdown]
forall a. a -> [a] -> [a]
intersperse Markdown
" " [Markdown
refToThis, forall (s :: [*]). ReifyList TypeHasDoc s => Markdown
refToStack @i, forall (s :: [*]). ReifyList TypeHasDoc s => Markdown
refToStack @o]
    where
    refToStack :: forall s. ReifyList TypeHasDoc s => Markdown
    refToStack :: forall (s :: [*]). ReifyList TypeHasDoc s => Markdown
refToStack =
      let stack :: [Markdown]
stack = forall k (c :: k -> Constraint) (l :: [k]) r.
ReifyList c l =>
(forall (a :: k). c a => Proxy a -> r) -> [r]
reifyList @_ @TypeHasDoc @s (\Proxy a
p -> Proxy a -> WithinParens -> Markdown
forall a. TypeHasDoc a => Proxy a -> WithinParens -> Markdown
typeDocMdReference Proxy a
p (Bool -> WithinParens
WithinParens Bool
False))
      in [Markdown] -> Markdown
forall a. Monoid a => [a] -> a
mconcat
          [ Markdown -> Markdown
mdBold Markdown
"["
          , case [Markdown]
stack of
              [] -> Markdown
" "
              [Markdown]
st -> [Markdown] -> Markdown
forall a. Monoid a => [a] -> a
mconcat ([Markdown] -> Markdown) -> [Markdown] -> Markdown
forall a b. (a -> b) -> a -> b
$ Markdown -> [Markdown] -> [Markdown]
forall a. a -> [a] -> [a]
intersperse (Markdown -> Markdown
mdBold Markdown
"," Markdown -> Markdown -> Markdown
forall a. Semigroup a => a -> a -> a
<> Markdown
" ") [Markdown]
st
          , Markdown -> Markdown
mdBold Markdown
"]"
          ]

  typeDocMdDescription :: Markdown
typeDocMdDescription =
    Markdown
"`WrappedLambda i o` stands for a sequence of instructions which accepts stack \
    \of type `i` and returns stack of type `o`.\n\n\
    \When both `i` and `o` are of length 1, this primitive corresponds to \
    \the Michelson lambda. In more complex cases code is surrounded with `pair`\
    \and `unpair` instructions until fits into mentioned restriction.\
    \"
  typeDocDependencies :: Proxy (WrappedLambda i o) -> [SomeDocDefinitionItem]
typeDocDependencies Proxy (WrappedLambda i o)
_ = [[SomeDocDefinitionItem]] -> [SomeDocDefinitionItem]
forall a. Monoid a => [a] -> a
mconcat
    [ forall k (c :: k -> Constraint) (l :: [k]) r.
ReifyList c l =>
(forall (a :: k). c a => Proxy a -> r) -> [r]
reifyList @_ @TypeHasDoc @i forall a. TypeHasDoc a => Proxy a -> SomeDocDefinitionItem
dTypeDepP
    , forall k (c :: k -> Constraint) (l :: [k]) r.
ReifyList c l =>
(forall (a :: k). c a => Proxy a -> r) -> [r]
reifyList @_ @TypeHasDoc @o forall a. TypeHasDoc a => Proxy a -> SomeDocDefinitionItem
dTypeDepP
    , [ forall t. TypeHasDoc t => SomeDocDefinitionItem
dTypeDep @Integer
      , forall t. TypeHasDoc t => SomeDocDefinitionItem
dTypeDep @Natural
      , forall t. TypeHasDoc t => SomeDocDefinitionItem
dTypeDep @MText
      ]
    ]
  typeDocHaskellRep :: TypeDocHaskellRep (WrappedLambda i o)
typeDocHaskellRep Proxy (WrappedLambda i o)
_ FieldDescriptionsV
_ = Maybe (Maybe DocTypeRepLHS, ADTRep SomeTypeWithDoc)
forall a. Maybe a
Nothing
  typeDocMichelsonRep :: TypeDocMichelsonRep (WrappedLambda i o)
typeDocMichelsonRep Proxy (WrappedLambda i o)
_ =
    ( DocTypeRepLHS -> Maybe DocTypeRepLHS
forall a. a -> Maybe a
Just DocTypeRepLHS
"WrappedLambda [Integer, Natural, MText, ()] [ByteString]"
    , forall {k} (a :: k). (SingKind k, SingI a) => Demote k
forall (a :: T). (SingKind T, SingI a) => Demote T
demote @(ToT (WrappedLambda [Integer, Natural, MText, ()] '[ByteString]))
    )

instance ( CanCastTo (ZippedStack inp1) (ZippedStack inp2)
         , CanCastTo (ZippedStack out1) (ZippedStack out2)
         , CanCastTo (ZippedStack (inp1 ++ '[WrappedLambda inp1 out1]))
                     (ZippedStack (inp2 ++ '[WrappedLambda inp2 out2]))
         )
  => WrappedLambda inp1 out1 `CanCastTo` WrappedLambda inp2 out2 where
  castDummy :: Proxy (WrappedLambda inp1 out1)
-> Proxy (WrappedLambda inp2 out2) -> ()
castDummy = Proxy (WrappedLambda inp1 out1)
-> Proxy (WrappedLambda inp2 out2) -> ()
forall a b.
(Generic a, Generic b, GCanCastTo (Rep a) (Rep b)) =>
Proxy a -> Proxy b -> ()
castDummyG