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

{-# 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 ((\\))
import qualified Data.Kind as Kind
import qualified Fcf
import Fmt (Buildable(..))
import GHC.Generics ((:*:)(..), (:+:)(..))
import qualified GHC.Generics as G
import qualified Text.Show

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 Michelson.Text
import Michelson.Typed
import Util.Label (Label)
import Util.Markdown
import Util.Type
import Util.TypeLits
import Util.TypeTuple

-- | An entrypoint is described by two types: its name and type of argument.
type EntrypointKind = (Symbol, Kind.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]) = UParamUnsafe (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))
$cp1IsoValue :: forall (entries :: [EntrypointKind]). WellTypedToT (UParam entries)
IsoValue, FollowEntrypointFlag -> Notes (ToT (UParam entries))
(FollowEntrypointFlag -> Notes (ToT (UParam entries)))
-> HasAnnotation (UParam entries)
forall (entries :: [EntrypointKind]).
FollowEntrypointFlag -> Notes (ToT (UParam entries))
forall a.
(FollowEntrypointFlag -> Notes (ToT a)) -> HasAnnotation a
getAnnotation :: FollowEntrypointFlag -> Notes (ToT (UParam entries))
$cgetAnnotation :: forall (entries :: [EntrypointKind]).
FollowEntrypointFlag -> Notes (ToT (UParam entries))
HasAnnotation, ToT (UParam entries) ~ ToT (Unwrappable (UParam entries))
(ToT (UParam entries) ~ ToT (Unwrappable (UParam entries))) =>
Wrappable (UParam entries)
forall (entries :: [EntrypointKind]).
ToT (UParam entries) ~ ToT (Unwrappable (UParam entries))
forall s. (ToT s ~ ToT (Unwrappable s)) => Wrappable s
Wrappable)

-- 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])
             :: Kind.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 :: Label name -> a -> UParam entries
mkUParam label :: Label name
label (a
a :: a) =
  (MText, ByteString) -> UParam entries
forall (entries :: [EntrypointKind]).
(MText, ByteString) -> UParam entries
UParamUnsafe (Label name -> MText
forall (name :: Symbol). Label name -> MText
labelToMText Label name
label, a -> ByteString
forall a. NicePackedValue a => a -> ByteString
lPackValue a
a)
    ((SingI (ToT a), HasNoOp (ToT a), HasNoBigMap (ToT a)) =>
 UParam entries)
-> ((KnownValue a,
     (SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
      FailOnBigMapFound (ContainsBigMap (ToT a))))
    :- (SingI (ToT a), HasNoOp (ToT a), HasNoBigMap (ToT a)))
-> UParam entries
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ (KnownValue a,
 (SingI (ToT a), FailOnOperationFound (ContainsOp (ToT a)),
  FailOnBigMapFound (ContainsBigMap (ToT a))))
:- (SingI (ToT a), HasNoOp (ToT a), HasNoBigMap (ToT a))
forall a. NicePackedValue a :- PackedValScope (ToT a)
nicePackedValueEvi @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 5

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

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

instance Show (ConstrainedSome Show) where
  show :: ConstrainedSome Show -> String
show (ConstrainedSome a :: a
a) = a -> String
forall b a. (Show a, IsString b) => a -> b
show a
a

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

-- | This class is needed to implement `unpackUParam`.
class UnpackUParam (c :: Kind.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 (UParamUnsafe (name :: MText
name, _)) = 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 (UParamUnsafe (name :: MText
name, bytes :: ByteString
bytes))
    | MText
name MText -> MText -> Bool
forall a. Eq a => a -> a -> Bool
== KnownSymbol name => MText
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) a. c a => a -> 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
.
      NiceUnpackedValue arg => ByteString -> Either UnpackError arg
forall a. NiceUnpackedValue a => ByteString -> Either UnpackError a
lUnpackValue @arg (ByteString
 -> Either EntrypointLookupError (MText, ConstrainedSome c))
-> ByteString
-> Either EntrypointLookupError (MText, ConstrainedSome c)
forall a b. (a -> b) -> a -> b
$
      ByteString
bytes
    | Bool
otherwise = UParam entries
-> Either EntrypointLookupError (MText, ConstrainedSome c)
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
UParamUnsafe (MText
name, ByteString
bytes))

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

-- | Helper instruction which extracts content of 'UParam'.
unwrapUParam :: UParam entries : s :-> (MText, ByteString) : s
unwrapUParam :: (UParam entries : s) :-> ((MText, ByteString) : s)
unwrapUParam = (UParam entries : s) :-> ((MText, ByteString) : s)
forall a (s :: [*]). Wrappable a => (a : s) :-> (Unwrappable 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)
(/->) _ = 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 name :: MText
name -> "No such entrypoint: " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> MText -> Builder
forall p. Buildable p => p -> Builder
build MText
name
      ArgumentUnpackFailed -> "UNPACK failed"

type instance ErrorArg "uparamNoSuchEntrypoint" = MText
type instance ErrorArg "uparamArgumentUnpackFailed" = ()

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

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

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

instance CustomErrorHasDoc "uparamArgumentUnpackFailed" where
  customErrClass :: ErrorClass
customErrClass = ErrorClass
ErrClassBadArgument
  customErrDocMdCause :: Builder
customErrDocMdCause = "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 :: 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) -> UParamFallback inp out
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label "uparamNoSuchEntrypoint" -> (MText & inp) :-> out
forall (tag :: Symbol) err (s :: [*]) (any :: [*]).
(err ~ ErrorArg tag, 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.
  caseUParamUnsafe
    :: Rec (CaseClauseU inp out) entries
    -> UParamFallback inp out
    -> (UParam entries : inp) :-> out

instance CaseUParam '[] where
  caseUParamUnsafe :: Rec (CaseClauseU inp out) '[]
-> UParamFallback inp out -> (UParam '[] : inp) :-> out
caseUParamUnsafe RNil fallback :: 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
         , NiceUnpackedValue arg
         ) =>
         CaseUParam ((name ?: arg) ': entries) where
  caseUParamUnsafe :: Rec (CaseClauseU inp out) ((name ?: arg) : entries)
-> UParamFallback inp out
-> (UParam ((name ?: arg) : entries) : inp) :-> out
caseUParamUnsafe (CaseClauseU clause :: (arg : inp) :-> out
clause :& clauses :: Rec (CaseClauseU inp out) rs
clauses) fallback :: UParamFallback inp out
fallback =
    (UParam ((name ?: arg) : rs) & inp)
:-> (UParam ((name ?: arg) : rs)
     & (UParam ((name ?: arg) : rs) & inp))
forall a (s :: [*]). (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 (HasCallStack => Text -> MText
Text -> MText
mkMTextUnsafe (Text -> MText) -> Text -> MText
forall a b. (a -> b) -> a -> b
$ KnownSymbol name => Text
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)
unpack ((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 :: [*])
       (notVoidErrorMsg :: ErrorMessage).
(RequireNoArgError tag notVoidErrorMsg, 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
caseUParamUnsafe Rec (CaseClauseU inp out) rs
clauses UParamFallback inp out
fallback)
    where
      cutUParamEntry :: UParam (e : es) : s :-> UParam es : s
      cutUParamEntry :: (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 :: 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
caseUParamUnsafe

-- | 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 :: IsoRecTuple clauses
-> UParamFallback inp out -> (UParam entries : inp) :-> out
caseUParamT clauses :: IsoRecTuple clauses
clauses fallback :: 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
caseUParamUnsafe (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 :: (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 (s :: [*]). (() & s) :-> s
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 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 :: up -> UParam (UParamLinearized up)
uparamFromAdt = Rep up Any -> UParam (UParamLinearized up)
forall (x :: * -> *) p.
GUParamLinearize x =>
x p -> UParam (GUParamLinearized x)
adtToRec (Rep up Any -> UParam (UParamLinearized up))
-> (up -> Rep up Any) -> up -> UParam (UParamLinearized 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 :: Kind.Type -> Kind.Type) where
  type GUParamLinearized x :: [(Symbol, Kind.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 :: 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))
-> (D1 i x p -> x p) -> D1 i x p -> UParam (GUParamLinearized x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. D1 i x p -> x p
forall i (c :: Meta) k (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 :: (:+:) x y p -> UParam (GUParamLinearized (x :+: y))
adtToRec = \case
    G.L1 x :: x p
x -> let UParamUnsafe up :: (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
UParamUnsafe (MText, ByteString)
up
    G.R1 y :: y p
y -> let UParamUnsafe up :: (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
UParamUnsafe (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 :: 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
a))) = (MText, ByteString) -> UParam '[ '(name, a)]
forall (entries :: [EntrypointKind]).
(MText, ByteString) -> UParam entries
UParamUnsafe
    ( KnownSymbol name => MText
forall (name :: Symbol). KnownSymbol name => MText
symbolToMText @name
    , a -> ByteString
forall a. NicePackedValue a => a -> ByteString
lPackValue a
a
    )

instance
    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 :: C1 i U1 p -> UParam (GUParamLinearized (C1 i U1))
adtToRec = Text -> C1 i U1 p -> UParam (TypeError ...)
forall a. HasCallStack => Text -> a
error "impossible"

instance
    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 :: C1 i (x :*: y) p -> UParam (GUParamLinearized (C1 i (x :*: y)))
adtToRec = Text -> C1 i (x :*: y) p -> UParam (TypeError ...)
forall a. HasCallStack => Text -> a
error "impossible"

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

instance Typeable interface => TypeHasDoc (UParam interface) where
  typeDocName :: Proxy (UParam interface) -> Text
typeDocName _ = "Upgradable parameter"
  typeDocMdReference :: Proxy (UParam interface) -> WithinParens -> Builder
typeDocMdReference p :: Proxy (UParam interface)
p = (Text, DType) -> [DType] -> WithinParens -> Builder
customTypeDocMdReference ("UParam", Proxy (UParam interface) -> DType
forall a. TypeHasDoc a => Proxy a -> DType
DType Proxy (UParam interface)
p) []
  typeDocMdDescription :: Builder
typeDocMdDescription =
    "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. SingI (ToT a) => TypeDocMichelsonRep a
homomorphicTypeDocMichelsonRep

-- | Note that calling given entrypoints involves constructing 'UParam'.
pbsUParam :: forall ctorName. KnownSymbol ctorName => ParamBuildingStep
pbsUParam :: 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
$ KnownSymbol ctorName => Text
forall (s :: Symbol). KnownSymbol s => Text
symbolValT' @ctorName
  in ParamBuildingDesc -> ParamBuildingStep
PbsCustom $WParamBuildingDesc :: Builder -> ParamBuilder -> ParamBuilder -> ParamBuildingDesc
ParamBuildingDesc
      { pbdEnglish :: Builder
pbdEnglish =
          "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
<> " entrypoint."
      , pbdHaskell :: ParamBuilder
pbdHaskell = (Builder -> Builder) -> ParamBuilder
ParamBuilder ((Builder -> Builder) -> ParamBuilder)
-> (Builder -> Builder) -> ParamBuilder
forall a b. (a -> b) -> a -> b
$
          \a :: Builder
a -> "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
forall a. Semigroup a => a -> a -> a
<> Builder
a Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> ")"
      , pbdMichelson :: ParamBuilder
pbdMichelson = (Builder -> Builder) -> ParamBuilder
ParamBuilder ((Builder -> Builder) -> ParamBuilder)
-> (Builder -> Builder) -> ParamBuilder
forall a b. (a -> b) -> a -> b
$
          \a :: Builder
a -> "Pair \"" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
ctor Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> "\" (pack (" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
a Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> "))"
      }