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

{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Lorentz.UParam
  ( UParam (..)
  , EntrypointKind
  , type (?:)

    -- * Construction
  , mkUParam

    -- * Deconstruction
  , ConstrainedSome (..)
  , UnpackUParam
  , unpackUParam

    -- * Casting to homomorphic value
  , SomeInterface
  , UParam_

    -- * Pattern-matching
  , EntrypointsImpl
  , UParamFallback
  , EntrypointLookupError (..)
  , CaseUParam
  , caseUParam
  , caseUParamT
  , uparamFallbackFail

    -- * Constraints
  , LookupEntrypoint
  , RequireUniqueEntrypoints

    -- * Conversion from ADT
  , uparamFromAdt
  , UParamLinearize
  , UParamLinearized

    -- * Documentation
  , pbsUParam

    -- * Internals used for entrypoint-wise migrations
  , unwrapUParam
  ) where

import Data.Constraint (Bottom(..))
import Fcf qualified
import Fmt (Buildable(..))
import GHC.Generics ((:*:)(..), (:+:)(..))
import GHC.Generics qualified as G

import Lorentz.ADT
import Lorentz.Annotation (HasAnnotation)
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints
import Lorentz.Entrypoints.Doc
import Lorentz.Errors
import Lorentz.Instr as L
import Lorentz.Macro
import Lorentz.Pack
import Morley.AsRPC (HasRPCRepr(..))
import Morley.Michelson.Text
import Morley.Michelson.Typed
import Morley.Util.Label (Label)
import Morley.Util.Markdown
import Morley.Util.Type
import Morley.Util.TypeLits
import Morley.Util.TypeTuple

-- | An entrypoint is described by two types: its name and type of argument.
type EntrypointKind = (Symbol, Type)

-- | A convenient alias for type-level name-something pair.
type (n :: Symbol) ?: (a :: k) = '(n, a)

-- | Encapsulates parameter for one of entry points.
-- It keeps entrypoint name and corresponding argument serialized.
--
-- In Haskell world, we keep an invariant of that contained value relates
-- to one of entry points from @entries@ list.
newtype UParam (entries :: [EntrypointKind]) = UnsafeUParam (MText, ByteString)
  deriving stock ((forall x. UParam entries -> Rep (UParam entries) x)
-> (forall x. Rep (UParam entries) x -> UParam entries)
-> Generic (UParam entries)
forall (entries :: [EntrypointKind]) x.
Rep (UParam entries) x -> UParam entries
forall (entries :: [EntrypointKind]) x.
UParam entries -> Rep (UParam entries) x
forall x. Rep (UParam entries) x -> UParam entries
forall x. UParam entries -> Rep (UParam entries) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (entries :: [EntrypointKind]) x.
Rep (UParam entries) x -> UParam entries
$cfrom :: forall (entries :: [EntrypointKind]) x.
UParam entries -> Rep (UParam entries) x
Generic, UParam entries -> UParam entries -> Bool
(UParam entries -> UParam entries -> Bool)
-> (UParam entries -> UParam entries -> Bool)
-> Eq (UParam entries)
forall (entries :: [EntrypointKind]).
UParam entries -> UParam entries -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UParam entries -> UParam entries -> Bool
$c/= :: forall (entries :: [EntrypointKind]).
UParam entries -> UParam entries -> Bool
== :: UParam entries -> UParam entries -> Bool
$c== :: forall (entries :: [EntrypointKind]).
UParam entries -> UParam entries -> Bool
Eq, Int -> UParam entries -> ShowS
[UParam entries] -> ShowS
UParam entries -> String
(Int -> UParam entries -> ShowS)
-> (UParam entries -> String)
-> ([UParam entries] -> ShowS)
-> Show (UParam entries)
forall (entries :: [EntrypointKind]).
Int -> UParam entries -> ShowS
forall (entries :: [EntrypointKind]). [UParam entries] -> ShowS
forall (entries :: [EntrypointKind]). UParam entries -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [UParam entries] -> ShowS
$cshowList :: forall (entries :: [EntrypointKind]). [UParam entries] -> ShowS
show :: UParam entries -> String
$cshow :: forall (entries :: [EntrypointKind]). UParam entries -> String
showsPrec :: Int -> UParam entries -> ShowS
$cshowsPrec :: forall (entries :: [EntrypointKind]).
Int -> UParam entries -> ShowS
Show)
  deriving anyclass (WellTypedToT (UParam entries)
WellTypedToT (UParam entries)
-> (UParam entries -> Value (ToT (UParam entries)))
-> (Value (ToT (UParam entries)) -> UParam entries)
-> IsoValue (UParam entries)
Value (ToT (UParam entries)) -> UParam entries
UParam entries -> Value (ToT (UParam entries))
forall {entries :: [EntrypointKind]}. WellTypedToT (UParam entries)
forall (entries :: [EntrypointKind]).
Value (ToT (UParam entries)) -> UParam entries
forall (entries :: [EntrypointKind]).
UParam entries -> Value (ToT (UParam entries))
forall a.
WellTypedToT a
-> (a -> Value (ToT a)) -> (Value (ToT a) -> a) -> IsoValue a
fromVal :: Value (ToT (UParam entries)) -> UParam entries
$cfromVal :: forall (entries :: [EntrypointKind]).
Value (ToT (UParam entries)) -> UParam entries
toVal :: UParam entries -> Value (ToT (UParam entries))
$ctoVal :: forall (entries :: [EntrypointKind]).
UParam entries -> Value (ToT (UParam entries))
IsoValue, AnnOptions
FollowEntrypointFlag -> Notes (ToT (UParam entries))
(FollowEntrypointFlag -> Notes (ToT (UParam entries)))
-> AnnOptions -> HasAnnotation (UParam entries)
forall (entries :: [EntrypointKind]). AnnOptions
forall (entries :: [EntrypointKind]).
FollowEntrypointFlag -> Notes (ToT (UParam entries))
forall a.
(FollowEntrypointFlag -> Notes (ToT a))
-> AnnOptions -> HasAnnotation a
annOptions :: AnnOptions
$cannOptions :: forall (entries :: [EntrypointKind]). AnnOptions
getAnnotation :: FollowEntrypointFlag -> Notes (ToT (UParam entries))
$cgetAnnotation :: forall (entries :: [EntrypointKind]).
FollowEntrypointFlag -> Notes (ToT (UParam entries))
HasAnnotation, ToT (UParam entries) ~ ToT (Unwrappabled (UParam entries))
(ToT (UParam entries) ~ ToT (Unwrappabled (UParam entries)))
-> Unwrappable (UParam entries)
forall {entries :: [EntrypointKind]}.
ToT (UParam entries) ~ ToT (Unwrappabled (UParam entries))
forall s. (ToT s ~ ToT (Unwrappabled s)) -> Unwrappable s
Unwrappable)

instance HasRPCRepr (UParam entries) where
  type AsRPC (UParam entries) = UParam entries

-- Casting to homomorphic value
----------------------------------------------------------------------------

-- | Pseudo value for 'UParam' type variable.
type SomeInterface = '[ '("SomeEntrypoints", Void) ]

-- | Homomorphic version of 'UParam', forgets the exact interface.
type UParam_ = UParam SomeInterface

-- | Allows casts only between 'UParam_' and 'UParam'.
instance SameEntries entries1 entries2 =>
         UParam entries1 `CanCastTo` UParam entries2

type family SameEntries (es1 :: [EntrypointKind]) (es :: [EntrypointKind])
              :: Constraint where
  SameEntries e e = ()
  SameEntries SomeInterface _ = ()
  SameEntries _ SomeInterface = ()
  SameEntries e1 e2 = (e1 ~ e2)

----------------------------------------------------------------------------
-- Common type-level stuff
----------------------------------------------------------------------------

-- | Get type of entrypoint argument by its name.
type family LookupEntrypoint (name :: Symbol) (entries :: [EntrypointKind])
             :: Type where
  LookupEntrypoint name ('(name, a) ': _) = a
  LookupEntrypoint name (_ ': entries) = LookupEntrypoint name entries
  LookupEntrypoint name '[] =
    TypeError ('Text "Entry point " ':<>: 'ShowType name ':<>:
               'Text " in not in the entry points list")

-- | Ensure that given entry points do no contain duplicated names.
type family RequireUniqueEntrypoints (entries :: [EntrypointKind])
             :: Constraint where
  RequireUniqueEntrypoints entries =
    RequireAllUnique "entrypoint" (Fcf.Eval (Fcf.Map Fcf.Fst entries))

----------------------------------------------------------------------------
-- Construction
----------------------------------------------------------------------------

-- | Construct a 'UParam' safely.
mkUParam
  :: ( NicePackedValue a
     , LookupEntrypoint name entries ~ a
     , RequireUniqueEntrypoints entries
     )
  => Label name -> a -> UParam entries
mkUParam :: forall a (name :: Symbol) (entries :: [EntrypointKind]).
(NicePackedValue a, LookupEntrypoint name entries ~ a,
 RequireUniqueEntrypoints entries) =>
Label name -> a -> UParam entries
mkUParam Label name
label (a
a :: a) =
  (MText, ByteString) -> UParam entries
forall (entries :: [EntrypointKind]).
(MText, ByteString) -> UParam entries
UnsafeUParam (Label name -> MText
forall (name :: Symbol). Label name -> MText
labelToMText Label name
label, a -> ByteString
forall a. NicePackedValue a => a -> ByteString
lPackValueRaw a
a)

-- Example
----------------------------------------------------------------------------

type MyEntrypoints =
  [ "add" ?: Integer
  , "reset" ?: ()
  ]

_mkParamSample1 :: UParam MyEntrypoints
_mkParamSample1 :: UParam MyEntrypoints
_mkParamSample1 = Label "add" -> Integer -> UParam MyEntrypoints
forall a (name :: Symbol) (entries :: [EntrypointKind]).
(NicePackedValue a, LookupEntrypoint name entries ~ a,
 RequireUniqueEntrypoints entries) =>
Label name -> a -> UParam entries
mkUParam IsLabel "add" (Label "add")
Label "add"
#add Integer
5

----------------------------------------------------------------------------
-- Deconstruction
----------------------------------------------------------------------------

-- | This type can store any value that satisfies a certain constraint.
data ConstrainedSome (c :: Type -> Constraint) where
  ConstrainedSome :: c a => a -> ConstrainedSome c

deriving stock instance Show (ConstrainedSome Show)

instance Buildable (ConstrainedSome Buildable) where
  build :: ConstrainedSome Buildable -> Builder
build (ConstrainedSome a
a) = a -> Builder
forall p. Buildable p => p -> Builder
build a
a

-- | This class is needed to implement `unpackUParam`.
class UnpackUParam (c :: Type -> Constraint) entries where
  -- | Turn 'UParam' into a Haskell value.
  -- Since we don't know its type in compile time, we have to erase it using
  -- 'ConstrainedSome'. The user of this function can require arbitrary
  -- constraint to hold (depending on how they want to use the result).
  unpackUParam ::
    UParam entries -> Either EntrypointLookupError (MText, ConstrainedSome c)

instance UnpackUParam c '[] where
  unpackUParam :: UParam '[]
-> Either EntrypointLookupError (MText, ConstrainedSome c)
unpackUParam (UnsafeUParam (MText
name, ByteString
_)) = EntrypointLookupError
-> Either EntrypointLookupError (MText, ConstrainedSome c)
forall a b. a -> Either a b
Left (MText -> EntrypointLookupError
NoSuchEntrypoint MText
name)

instance
  ( KnownSymbol name
  , UnpackUParam c entries
  , NiceUnpackedValue arg
  , c arg
  ) => UnpackUParam c ((name ?: arg) ': entries) where
  unpackUParam :: UParam ((name ?: arg) : entries)
-> Either EntrypointLookupError (MText, ConstrainedSome c)
unpackUParam (UnsafeUParam (MText
name, ByteString
bytes))
    | MText
name MText -> MText -> Bool
forall a. Eq a => a -> a -> Bool
== forall (name :: Symbol). KnownSymbol name => MText
symbolToMText @name =
      (ConstrainedSome c -> (MText, ConstrainedSome c))
-> Either EntrypointLookupError (ConstrainedSome c)
-> Either EntrypointLookupError (MText, ConstrainedSome c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (MText
name,) (Either EntrypointLookupError (ConstrainedSome c)
 -> Either EntrypointLookupError (MText, ConstrainedSome c))
-> (ByteString -> Either EntrypointLookupError (ConstrainedSome c))
-> ByteString
-> Either EntrypointLookupError (MText, ConstrainedSome c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      (UnpackError -> EntrypointLookupError)
-> Either UnpackError (ConstrainedSome c)
-> Either EntrypointLookupError (ConstrainedSome c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (EntrypointLookupError -> UnpackError -> EntrypointLookupError
forall a b. a -> b -> a
const EntrypointLookupError
ArgumentUnpackFailed) (Either UnpackError (ConstrainedSome c)
 -> Either EntrypointLookupError (ConstrainedSome c))
-> (ByteString -> Either UnpackError (ConstrainedSome c))
-> ByteString
-> Either EntrypointLookupError (ConstrainedSome c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      (arg -> ConstrainedSome c)
-> Either UnpackError arg -> Either UnpackError (ConstrainedSome c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap arg -> ConstrainedSome c
forall (c :: * -> Constraint) arg.
c arg =>
arg -> ConstrainedSome c
ConstrainedSome (Either UnpackError arg -> Either UnpackError (ConstrainedSome c))
-> (ByteString -> Either UnpackError arg)
-> ByteString
-> Either UnpackError (ConstrainedSome c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
      forall a. NiceUnpackedValue a => ByteString -> Either UnpackError a
lUnpackValueRaw @arg (ByteString
 -> Either EntrypointLookupError (MText, ConstrainedSome c))
-> ByteString
-> Either EntrypointLookupError (MText, ConstrainedSome c)
forall a b. (a -> b) -> a -> b
$
      ByteString
bytes
    | Bool
otherwise = forall (c :: * -> Constraint) (entries :: [EntrypointKind]).
UnpackUParam c entries =>
UParam entries
-> Either EntrypointLookupError (MText, ConstrainedSome c)
unpackUParam @c @entries ((MText, ByteString) -> UParam entries
forall (entries :: [EntrypointKind]).
(MText, ByteString) -> UParam entries
UnsafeUParam (MText
name, ByteString
bytes))

----------------------------------------------------------------------------
-- Pattern-matching
----------------------------------------------------------------------------

-- | Helper instruction which extracts content of 'UParam'.
unwrapUParam :: UParam entries : s :-> (MText, ByteString) : s
unwrapUParam :: forall (entries :: [EntrypointKind]) (s :: [*]).
(UParam entries : s) :-> ((MText, ByteString) : s)
unwrapUParam = (UParam entries : s) :-> ((MText, ByteString) : s)
forall a (s :: [*]).
Unwrappable a =>
(a : s) :-> (Unwrappabled a : s)
coerceUnwrap

-- | Wrapper for a single "case" branch.
data CaseClauseU inp out (entry :: EntrypointKind) where
  CaseClauseU :: (arg : inp) :-> out -> CaseClauseU inp out '(name, arg)

instance (name ~ name', body ~ ((arg : inp) :-> out)) =>
         CaseArrow name' body (CaseClauseU inp out '(name, arg)) where
  /-> :: Label name' -> body -> CaseClauseU inp out '(name, arg)
(/->) Label name'
_ = body -> CaseClauseU inp out '(name, arg)
forall arg (inp :: [*]) (out :: [*]) (name :: Symbol).
((arg : inp) :-> out) -> CaseClauseU inp out '(name, arg)
CaseClauseU

data EntrypointLookupError
  = NoSuchEntrypoint MText
  | ArgumentUnpackFailed
  deriving stock ((forall x. EntrypointLookupError -> Rep EntrypointLookupError x)
-> (forall x. Rep EntrypointLookupError x -> EntrypointLookupError)
-> Generic EntrypointLookupError
forall x. Rep EntrypointLookupError x -> EntrypointLookupError
forall x. EntrypointLookupError -> Rep EntrypointLookupError x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep EntrypointLookupError x -> EntrypointLookupError
$cfrom :: forall x. EntrypointLookupError -> Rep EntrypointLookupError x
Generic, EntrypointLookupError -> EntrypointLookupError -> Bool
(EntrypointLookupError -> EntrypointLookupError -> Bool)
-> (EntrypointLookupError -> EntrypointLookupError -> Bool)
-> Eq EntrypointLookupError
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EntrypointLookupError -> EntrypointLookupError -> Bool
$c/= :: EntrypointLookupError -> EntrypointLookupError -> Bool
== :: EntrypointLookupError -> EntrypointLookupError -> Bool
$c== :: EntrypointLookupError -> EntrypointLookupError -> Bool
Eq, Int -> EntrypointLookupError -> ShowS
[EntrypointLookupError] -> ShowS
EntrypointLookupError -> String
(Int -> EntrypointLookupError -> ShowS)
-> (EntrypointLookupError -> String)
-> ([EntrypointLookupError] -> ShowS)
-> Show EntrypointLookupError
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EntrypointLookupError] -> ShowS
$cshowList :: [EntrypointLookupError] -> ShowS
show :: EntrypointLookupError -> String
$cshow :: EntrypointLookupError -> String
showsPrec :: Int -> EntrypointLookupError -> ShowS
$cshowsPrec :: Int -> EntrypointLookupError -> ShowS
Show)

instance Buildable EntrypointLookupError where
  build :: EntrypointLookupError -> Builder
build =
    \case
      NoSuchEntrypoint MText
name -> Builder
"No such entrypoint: " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> MText -> Builder
forall p. Buildable p => p -> Builder
build MText
name
      EntrypointLookupError
ArgumentUnpackFailed -> Builder
"UNPACK failed"

type instance ErrorArg "uparamNoSuchEntrypoint" = MText
type instance ErrorArg "uparamArgumentUnpackFailed" = UnitErrorArg

instance Buildable (CustomError "uparamNoSuchEntrypoint") where
  build :: CustomError "uparamNoSuchEntrypoint" -> Builder
build (CustomError Label "uparamNoSuchEntrypoint"
_ (MText
_, MText
name)) = Builder
"No such entrypoint: " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> MText -> Builder
forall p. Buildable p => p -> Builder
build MText
name

instance Buildable (CustomError "uparamArgumentUnpackFailed") where
  build :: CustomError "uparamArgumentUnpackFailed" -> Builder
build (CustomError Label "uparamArgumentUnpackFailed"
_ (MText
_, ())) = Builder
"UNPACK failed"

instance CustomErrorHasDoc "uparamNoSuchEntrypoint" where
  customErrClass :: ErrorClass
customErrClass = ErrorClass
ErrClassBadArgument
  customErrDocMdCause :: Builder
customErrDocMdCause = Builder
"Entrypoint with given name does not exist."

instance CustomErrorHasDoc "uparamArgumentUnpackFailed" where
  customErrClass :: ErrorClass
customErrClass = ErrorClass
ErrClassBadArgument
  customErrDocMdCause :: Builder
customErrDocMdCause = Builder
"Argument of wrong type is provided to the entrypoint."

-- | Implementations of some entry points.
--
-- Note that this thing inherits properties of 'Rec', e.g. you can
-- @Data.Vinyl.Core.rappend@ implementations for two entrypoint sets
-- when assembling scattered parts of a contract.
type EntrypointsImpl inp out entries =
  Rec (CaseClauseU inp out) entries

-- | An action invoked when user-provided entrypoint is not found.
type UParamFallback inp out = ((MText, ByteString) : inp) :-> out

-- | Default implementation for 'UParamFallback', simply reports an error.
uparamFallbackFail :: UParamFallback inp out
uparamFallbackFail :: forall (inp :: [*]) (out :: [*]). UParamFallback inp out
uparamFallbackFail =
  ((MText, ByteString) : inp) :-> (MText : inp)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car (((MText, ByteString) : inp) :-> (MText : inp))
-> ((MText : inp) :-> out) -> ((MText, ByteString) : inp) :-> out
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label "uparamNoSuchEntrypoint" -> (MText : inp) :-> out
forall (tag :: Symbol) err (s :: [*]) (any :: [*]).
(MustHaveErrorArg tag (MText, err), CustomErrorHasDoc tag,
 KnownError err) =>
Label tag -> (err : s) :-> any
failCustom IsLabel "uparamNoSuchEntrypoint" (Label "uparamNoSuchEntrypoint")
Label "uparamNoSuchEntrypoint"
#uparamNoSuchEntrypoint

-- | Make up a "case" over entry points.
class CaseUParam (entries :: [EntrypointKind]) where
  -- | Pattern-match on given @UParam entries@.
  --
  -- You have to provide all case branches and a fallback action on case
  -- when entrypoint is not found.
  --
  -- This function is unsafe because it does not make sure at type-level
  -- that entry points' names do not repeat.
  unsafeCaseUParam
    :: Rec (CaseClauseU inp out) entries
    -> UParamFallback inp out
    -> (UParam entries : inp) :-> out

instance CaseUParam '[] where
  unsafeCaseUParam :: forall (inp :: [*]) (out :: [*]).
Rec (CaseClauseU inp out) '[]
-> UParamFallback inp out -> (UParam '[] : inp) :-> out
unsafeCaseUParam Rec (CaseClauseU inp out) '[]
RNil UParamFallback inp out
fallback = (UParam '[] : inp) :-> ((MText, ByteString) : inp)
forall (entries :: [EntrypointKind]) (s :: [*]).
(UParam entries : s) :-> ((MText, ByteString) : s)
unwrapUParam ((UParam '[] : inp) :-> ((MText, ByteString) : inp))
-> UParamFallback inp out -> (UParam '[] : inp) :-> out
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# UParamFallback inp out
fallback

instance ( KnownSymbol name
         , CaseUParam entries
         , Typeable entries
         , NiceUnpackedValue arg
         ) =>
         CaseUParam ((name ?: arg) ': entries) where
  unsafeCaseUParam :: forall (inp :: [*]) (out :: [*]).
Rec (CaseClauseU inp out) ((name ?: arg) : entries)
-> UParamFallback inp out
-> (UParam ((name ?: arg) : entries) : inp) :-> out
unsafeCaseUParam (CaseClauseU (arg : inp) :-> out
clause :& Rec (CaseClauseU inp out) rs
clauses) UParamFallback inp out
fallback =
    (UParam ((name ?: arg) : rs) : inp)
:-> (UParam ((name ?: arg) : rs)
       : UParam ((name ?: arg) : rs) : inp)
forall a (s :: [*]). Dupable a => (a : s) :-> (a : a : s)
dup ((UParam ((name ?: arg) : rs) : inp)
 :-> (UParam ((name ?: arg) : rs)
        : UParam ((name ?: arg) : rs) : inp))
-> ((UParam ((name ?: arg) : rs)
       : UParam ((name ?: arg) : rs) : inp)
    :-> ((MText, ByteString) : UParam ((name ?: arg) : rs) : inp))
-> (UParam ((name ?: arg) : rs) : inp)
   :-> ((MText, ByteString) : UParam ((name ?: arg) : rs) : inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (UParam ((name ?: arg) : rs) : UParam ((name ?: arg) : rs) : inp)
:-> ((MText, ByteString) : UParam ((name ?: arg) : rs) : inp)
forall (entries :: [EntrypointKind]) (s :: [*]).
(UParam entries : s) :-> ((MText, ByteString) : s)
unwrapUParam ((UParam ((name ?: arg) : rs) : inp)
 :-> ((MText, ByteString) : UParam ((name ?: arg) : rs) : inp))
-> (((MText, ByteString) : UParam ((name ?: arg) : rs) : inp)
    :-> (MText : UParam ((name ?: arg) : rs) : inp))
-> (UParam ((name ?: arg) : rs) : inp)
   :-> (MText : UParam ((name ?: arg) : rs) : inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((MText, ByteString) : UParam ((name ?: arg) : rs) : inp)
:-> (MText : UParam ((name ?: arg) : rs) : inp)
forall a b (s :: [*]). ((a, b) : s) :-> (a : s)
car ((UParam ((name ?: arg) : rs) : inp)
 :-> (MText : UParam ((name ?: arg) : rs) : inp))
-> ((MText : UParam ((name ?: arg) : rs) : inp)
    :-> (MText : MText : UParam ((name ?: arg) : rs) : inp))
-> (UParam ((name ?: arg) : rs) : inp)
   :-> (MText : MText : UParam ((name ?: arg) : rs) : inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
    MText
-> (MText : UParam ((name ?: arg) : rs) : inp)
   :-> (MText : MText : UParam ((name ?: arg) : rs) : inp)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push (Either Text MText -> MText
forall a b. (HasCallStack, Buildable a) => Either a b -> b
unsafe (Either Text MText -> MText)
-> (Text -> Either Text MText) -> Text -> MText
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Either Text MText
mkMText (Text -> MText) -> Text -> MText
forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol). KnownSymbol s => Text
symbolValT' @name) ((UParam ((name ?: arg) : rs) : inp)
 :-> (MText : MText : UParam ((name ?: arg) : rs) : inp))
-> ((MText : MText : UParam ((name ?: arg) : rs) : inp)
    :-> (Bool : UParam ((name ?: arg) : rs) : inp))
-> (UParam ((name ?: arg) : rs) : inp)
   :-> (Bool : UParam ((name ?: arg) : rs) : inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (MText : MText : UParam ((name ?: arg) : rs) : inp)
:-> (Bool : UParam ((name ?: arg) : rs) : inp)
forall n (s :: [*]). NiceComparable n => (n : n : s) :-> (Bool : s)
eq ((UParam ((name ?: arg) : rs) : inp)
 :-> (Bool : UParam ((name ?: arg) : rs) : inp))
-> ((Bool : UParam ((name ?: arg) : rs) : inp) :-> out)
-> (UParam ((name ?: arg) : rs) : inp) :-> out
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
    ((UParam ((name ?: arg) : rs) : inp) :-> out)
-> ((UParam ((name ?: arg) : rs) : inp) :-> out)
-> (Bool : UParam ((name ?: arg) : rs) : inp) :-> out
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ ((UParam ((name ?: arg) : rs) : inp) :-> ((MText, ByteString) : inp)
forall (entries :: [EntrypointKind]) (s :: [*]).
(UParam entries : s) :-> ((MText, ByteString) : s)
unwrapUParam ((UParam ((name ?: arg) : rs) : inp)
 :-> ((MText, ByteString) : inp))
-> (((MText, ByteString) : inp) :-> (ByteString : inp))
-> (UParam ((name ?: arg) : rs) : inp) :-> (ByteString : inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((MText, ByteString) : inp) :-> (ByteString : inp)
forall a b (s :: [*]). ((a, b) : s) :-> (b : s)
cdr ((UParam ((name ?: arg) : rs) : inp) :-> (ByteString : inp))
-> ((ByteString : inp) :-> (Maybe arg : inp))
-> (UParam ((name ?: arg) : rs) : inp) :-> (Maybe arg : inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (ByteString : inp) :-> (Maybe arg : inp)
forall a (s :: [*]).
NiceUnpackedValue a =>
(ByteString : s) :-> (Maybe a : s)
unpackRaw ((UParam ((name ?: arg) : rs) : inp) :-> (Maybe arg : inp))
-> ((Maybe arg : inp) :-> (arg : inp))
-> (UParam ((name ?: arg) : rs) : inp) :-> (arg : inp)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
         ((arg : inp) :-> (arg : inp))
-> (inp :-> (arg : inp)) -> (Maybe arg : inp) :-> (arg : inp)
forall a (s :: [*]) (s' :: [*]).
((a : s) :-> s') -> (s :-> s') -> (Maybe a : s) :-> s'
ifSome (arg : inp) :-> (arg : inp)
forall (s :: [*]). s :-> s
nop (Label "uparamArgumentUnpackFailed" -> inp :-> (arg : inp)
forall (tag :: Symbol) (s :: [*]) (any :: [*]).
(MustHaveErrorArg tag (MText, ()), CustomErrorHasDoc tag) =>
Label tag -> s :-> any
failCustom_ IsLabel
  "uparamArgumentUnpackFailed" (Label "uparamArgumentUnpackFailed")
Label "uparamArgumentUnpackFailed"
#uparamArgumentUnpackFailed) ((UParam ((name ?: arg) : rs) : inp) :-> (arg : inp))
-> ((arg : inp) :-> out)
-> (UParam ((name ?: arg) : rs) : inp) :-> out
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (arg : inp) :-> out
clause)
        ((UParam ((name ?: arg) : rs) : inp) :-> (UParam rs : inp)
forall (e :: EntrypointKind) (es :: [EntrypointKind]) (s :: [*]).
(UParam (e : es) : s) :-> (UParam es : s)
cutUParamEntry ((UParam ((name ?: arg) : rs) : inp) :-> (UParam rs : inp))
-> ((UParam rs : inp) :-> out)
-> (UParam ((name ?: arg) : rs) : inp) :-> out
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Rec (CaseClauseU inp out) rs
-> UParamFallback inp out -> (UParam rs : inp) :-> out
forall (entries :: [EntrypointKind]) (inp :: [*]) (out :: [*]).
CaseUParam entries =>
Rec (CaseClauseU inp out) entries
-> UParamFallback inp out -> (UParam entries : inp) :-> out
unsafeCaseUParam Rec (CaseClauseU inp out) rs
clauses UParamFallback inp out
fallback)
    where
      cutUParamEntry :: UParam (e : es) : s :-> UParam es : s
      cutUParamEntry :: forall (e :: EntrypointKind) (es :: [EntrypointKind]) (s :: [*]).
(UParam (e : es) : s) :-> (UParam es : s)
cutUParamEntry = (UParam (e : es) : s) :-> (UParam es : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_

-- | Pattern-match on given @UParam entries@.
--
-- You have to provide all case branches and a fallback action on case
-- when entrypoint is not found.
caseUParam
  :: (CaseUParam entries, RequireUniqueEntrypoints entries)
  => Rec (CaseClauseU inp out) entries
  -> UParamFallback inp out
  -> (UParam entries : inp) :-> out
caseUParam :: forall (entries :: [EntrypointKind]) (inp :: [*]) (out :: [*]).
(CaseUParam entries, RequireUniqueEntrypoints entries) =>
Rec (CaseClauseU inp out) entries
-> UParamFallback inp out -> (UParam entries : inp) :-> out
caseUParam = Rec (CaseClauseU inp out) entries
-> UParamFallback inp out -> (UParam entries : inp) :-> out
forall (entries :: [EntrypointKind]) (inp :: [*]) (out :: [*]).
CaseUParam entries =>
Rec (CaseClauseU inp out) entries
-> UParamFallback inp out -> (UParam entries : inp) :-> out
unsafeCaseUParam

-- | Like 'caseUParam', but accepts a tuple of clauses, not a 'Rec'.
caseUParamT
  :: forall entries inp out clauses.
     ( clauses ~ Rec (CaseClauseU inp out) entries
     , RecFromTuple clauses
     , CaseUParam entries
     )
  => IsoRecTuple clauses
  -> UParamFallback inp out
  -> (UParam entries : inp) :-> out
caseUParamT :: forall (entries :: [EntrypointKind]) (inp :: [*]) (out :: [*])
       clauses.
(clauses ~ Rec (CaseClauseU inp out) entries, RecFromTuple clauses,
 CaseUParam entries) =>
IsoRecTuple clauses
-> UParamFallback inp out -> (UParam entries : inp) :-> out
caseUParamT IsoRecTuple clauses
clauses UParamFallback inp out
fallback = Rec (CaseClauseU inp out) entries
-> UParamFallback inp out -> (UParam entries : inp) :-> out
forall (entries :: [EntrypointKind]) (inp :: [*]) (out :: [*]).
CaseUParam entries =>
Rec (CaseClauseU inp out) entries
-> UParamFallback inp out -> (UParam entries : inp) :-> out
unsafeCaseUParam (IsoRecTuple (Rec (CaseClauseU inp out) entries)
-> Rec (CaseClauseU inp out) entries
forall r. RecFromTuple r => IsoRecTuple r -> r
recFromTuple IsoRecTuple clauses
IsoRecTuple (Rec (CaseClauseU inp out) entries)
clauses) UParamFallback inp out
fallback

-- Example
----------------------------------------------------------------------------

_caseSample :: UParam MyEntrypoints : s :-> Integer : s
_caseSample :: forall (s :: [*]). (UParam MyEntrypoints : s) :-> (Integer : s)
_caseSample = IsoRecTuple (Rec (CaseClauseU s (Integer : s)) MyEntrypoints)
-> UParamFallback s (Integer : s)
-> (UParam MyEntrypoints : s) :-> (Integer : s)
forall (entries :: [EntrypointKind]) (inp :: [*]) (out :: [*])
       clauses.
(clauses ~ Rec (CaseClauseU inp out) entries, RecFromTuple clauses,
 CaseUParam entries) =>
IsoRecTuple clauses
-> UParamFallback inp out -> (UParam entries : inp) :-> out
caseUParamT
  ( IsLabel "add" (Label "add")
Label "add"
#add Label "add"
-> ((Integer : s) :-> (Integer : s))
-> CaseClauseU s (Integer : s) '("add", Integer)
forall (name :: Symbol) body clause.
CaseArrow name body clause =>
Label name -> body -> clause
/-> (Integer : s) :-> (Integer : s)
forall (s :: [*]). s :-> s
nop
  , IsLabel "reset" (Label "reset")
Label "reset"
#reset Label "reset"
-> ((() : s) :-> (Integer : s))
-> CaseClauseU s (Integer : s) '("reset", ())
forall (name :: Symbol) body clause.
CaseArrow name body clause =>
Label name -> body -> clause
/-> forall a (s :: [*]). (a : s) :-> s
L.drop @() ((() : s) :-> s)
-> (s :-> (Integer : s)) -> (() : s) :-> (Integer : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Integer -> s :-> (Integer : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t : s)
push Integer
0
  ) UParamFallback s (Integer : s)
forall (inp :: [*]) (out :: [*]). UParamFallback inp out
uparamFallbackFail

----------------------------------------------------------------------------
-- ADT conversion
----------------------------------------------------------------------------

{- @martoon: I actually hope no one will use this capability,
   it's here primarily because in other places we also use Generic stuff.

   Representation with type-level list and a datatype made polymorhpic over
   it seems more powerful than Generics.
   1. It's simpler to implement features for it. No extra boilerplate.
   2. 'Data.Vinyl' provides many useful utilities to work with such things.
   3. You are not such constrained in selecting names of entry points as when
      they come from constructor names.
-}

-- | Make up 'UParam' from ADT sum.
--
-- Entry points template will consist of
-- @(constructorName, constructorFieldType)@ pairs.
-- Each constructor is expected to have exactly one field.
uparamFromAdt
  :: UParamLinearize up
  => up -> UParam (UParamLinearized up)
uparamFromAdt :: forall up. UParamLinearize up => up -> UParam (UParamLinearized up)
uparamFromAdt = Rep up Any -> UParam (GUParamLinearized (Rep up))
forall (x :: * -> *) p.
GUParamLinearize x =>
x p -> UParam (GUParamLinearized x)
adtToRec (Rep up Any -> UParam (GUParamLinearized (Rep up)))
-> (up -> Rep up Any) -> up -> UParam (GUParamLinearized (Rep up))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. up -> Rep up Any
forall a x. Generic a => a -> Rep a x
G.from

-- | Constraint required by 'uparamFromAdt'.
type UParamLinearize p = (Generic p, GUParamLinearize (G.Rep p))

-- | Entry points template derived from given ADT sum.
type UParamLinearized p = GUParamLinearized (G.Rep p)

-- | Generic traversal for conversion between ADT sum and 'UParam'.
class GUParamLinearize (x :: Type -> Type) where
  type GUParamLinearized x :: [(Symbol, Type)]
  adtToRec :: x p -> UParam (GUParamLinearized x)

instance GUParamLinearize x => GUParamLinearize (G.D1 i x) where
  type GUParamLinearized (G.D1 i x) = GUParamLinearized x
  adtToRec :: forall p. D1 i x p -> UParam (GUParamLinearized (D1 i x))
adtToRec = x p -> UParam (GUParamLinearized x)
forall (x :: * -> *) p.
GUParamLinearize x =>
x p -> UParam (GUParamLinearized x)
adtToRec (x p -> UParam (GUParamLinearized x))
-> (M1 D i x p -> x p)
-> M1 D i x p
-> UParam (GUParamLinearized x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 D i x p -> x p
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
G.unM1

instance (GUParamLinearize x, GUParamLinearize y) => GUParamLinearize (x :+: y) where
  type GUParamLinearized (x :+: y) = GUParamLinearized x ++ GUParamLinearized y
  adtToRec :: forall p. (:+:) x y p -> UParam (GUParamLinearized (x :+: y))
adtToRec = \case
    G.L1 x p
x -> let UnsafeUParam (MText, ByteString)
up = x p -> UParam (GUParamLinearized x)
forall (x :: * -> *) p.
GUParamLinearize x =>
x p -> UParam (GUParamLinearized x)
adtToRec x p
x in (MText, ByteString)
-> UParam (GUParamLinearized x ++ GUParamLinearized y)
forall (entries :: [EntrypointKind]).
(MText, ByteString) -> UParam entries
UnsafeUParam (MText, ByteString)
up
    G.R1 y p
y -> let UnsafeUParam (MText, ByteString)
up = y p -> UParam (GUParamLinearized y)
forall (x :: * -> *) p.
GUParamLinearize x =>
x p -> UParam (GUParamLinearized x)
adtToRec y p
y in (MText, ByteString)
-> UParam (GUParamLinearized x ++ GUParamLinearized y)
forall (entries :: [EntrypointKind]).
(MText, ByteString) -> UParam entries
UnsafeUParam (MText, ByteString)
up

instance (KnownSymbol name, NicePackedValue a) =>
         GUParamLinearize (G.C1 ('G.MetaCons name _1 _2) (G.S1 si (G.Rec0 a))) where
  type GUParamLinearized (G.C1 ('G.MetaCons name _1 _2) (G.S1 si (G.Rec0 a))) =
    '[ '(name, a) ]

  adtToRec :: forall p.
C1 ('MetaCons name _1 _2) (S1 si (Rec0 a)) p
-> UParam
     (GUParamLinearized (C1 ('MetaCons name _1 _2) (S1 si (Rec0 a))))
adtToRec (G.M1 (G.M1 (G.K1 a
a))) = (MText, ByteString) -> UParam '[ '(name, a)]
forall (entries :: [EntrypointKind]).
(MText, ByteString) -> UParam entries
UnsafeUParam
    ( forall (name :: Symbol). KnownSymbol name => MText
symbolToMText @name
    , a -> ByteString
forall a. NicePackedValue a => a -> ByteString
lPackValueRaw a
a
    )

instance
    ( Bottom
    , TypeError ('Text "UParam linearization requires exactly one field \
                       \in each constructor")) =>
    GUParamLinearize (G.C1 i G.U1) where
  type GUParamLinearized (G.C1 i G.U1) =
    TypeError ('Text "Bad linearized ADT")
  adtToRec :: forall p. C1 i U1 p -> UParam (GUParamLinearized (C1 i U1))
adtToRec = M1 C i U1 p -> UParam (GUParamLinearized (C1 i U1))
forall a. Bottom => a
no

instance
    ( Bottom
    , TypeError ('Text "UParam linearization requires exactly one field \
                       \in each constructor")) =>
    GUParamLinearize (G.C1 i (x :*: y)) where
  type GUParamLinearized (G.C1 i (x :*: y)) =
    TypeError ('Text "Bad linearized ADT")
  adtToRec :: forall p.
C1 i (x :*: y) p -> UParam (GUParamLinearized (C1 i (x :*: y)))
adtToRec = M1 C i (x :*: y) p -> UParam (GUParamLinearized (C1 i (x :*: y)))
forall a. Bottom => a
no

----------------------------------------------------------------------------
-- Documentation
----------------------------------------------------------------------------

instance Typeable interface => TypeHasDoc (UParam interface) where
  typeDocName :: Proxy (UParam interface) -> Text
typeDocName Proxy (UParam interface)
_ = Text
"Upgradable parameter"
  typeDocMdReference :: Proxy (UParam interface) -> WithinParens -> Builder
typeDocMdReference Proxy (UParam interface)
p = (Text, DType) -> [DType] -> WithinParens -> Builder
customTypeDocMdReference (Text
"UParam", Proxy (UParam interface) -> DType
forall a. TypeHasDoc a => Proxy a -> DType
DType Proxy (UParam interface)
p) []
  typeDocMdDescription :: Builder
typeDocMdDescription =
    Builder
"This type encapsulates parameter for one of entry points. \
    \It keeps entry point name and corresponding argument serialized."
  typeDocHaskellRep :: TypeDocHaskellRep (UParam interface)
typeDocHaskellRep = TypeDocHaskellRep (UParam interface)
forall a. (Generic a, GTypeHasDoc (Rep a)) => TypeDocHaskellRep a
homomorphicTypeDocHaskellRep
  typeDocMichelsonRep :: TypeDocMichelsonRep (UParam interface)
typeDocMichelsonRep = TypeDocMichelsonRep (UParam interface)
forall a. KnownIsoT a => TypeDocMichelsonRep a
homomorphicTypeDocMichelsonRep

-- | Note that calling given entrypoints involves constructing 'UParam'.
pbsUParam :: forall ctorName. KnownSymbol ctorName => ParamBuildingStep
pbsUParam :: forall (ctorName :: Symbol).
KnownSymbol ctorName =>
ParamBuildingStep
pbsUParam =
  let ctor :: Builder
ctor = Text -> Builder
forall p. Buildable p => p -> Builder
build (Text -> Builder) -> Text -> Builder
forall a b. (a -> b) -> a -> b
$ forall (s :: Symbol). KnownSymbol s => Text
symbolValT' @ctorName
  in ParamBuildingDesc -> ParamBuildingStep
PbsCustom ParamBuildingDesc :: Builder -> ParamBuilder -> ParamBuilder -> ParamBuildingDesc
ParamBuildingDesc
      { pbdEnglish :: Builder
pbdEnglish =
          Builder
"Wrap into *UParam* as " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder -> Builder
mdTicked Builder
ctor Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" entrypoint."
      , pbdHaskell :: ParamBuilder
pbdHaskell = (Builder -> Builder) -> ParamBuilder
ParamBuilder ((Builder -> Builder) -> ParamBuilder)
-> (Builder -> Builder) -> ParamBuilder
forall a b. (a -> b) -> a -> b
$
          \Builder
a -> Builder
"mkUParam #" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
ctor Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
" (" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
a Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
")"
      , pbdMichelson :: ParamBuilder
pbdMichelson = (Builder -> Builder) -> ParamBuilder
ParamBuilder ((Builder -> Builder) -> ParamBuilder)
-> (Builder -> Builder) -> ParamBuilder
forall a b. (a -> b) -> a -> b
$
          \Builder
a -> Builder
"Pair \"" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
ctor Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"\" (pack (" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
a Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"))"
      }