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

{-# LANGUAGE PartialTypeSignatures #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | Common Michelson macros defined using Lorentz syntax.
module Lorentz.Macro
  ( -- * Compare
    NiceComparable
  , eq
  , neq
  , lt
  , gt
  , le
  , ge
  , ifEq0
  , ifGe0
  , ifGt0
  , ifLe0
  , ifLt0
  , ifNeq0
  , ifEq
  , ifGe
  , ifGt
  , ifLe
  , ifLt
  , ifNeq

  -- * Fail
  , fail_

  -- * Assertion macros
  -- |
  -- They differ from the same macros in Michelson, because those
  -- macros use FAIL macro which is not informative (fails with unit).
  -- If you __really__ want Michelson versions (maybe to produce exact
  -- copy of an existing contract), you can pass 'UnspecifiedError', then
  -- FAILWITH will be called with unit.
  , assert
  , assertEq0
  , assertNeq0
  , assertLt0
  , assertGt0
  , assertLe0
  , assertGe0
  , assertEq
  , assertNeq
  , assertLt
  , assertGt
  , assertLe
  , assertGe
  , assertNone
  , assertSome
  , assertLeft
  , assertRight
  , assertUsing

  -- * Syntactic Conveniences
  , ConstraintDuupXLorentz
  , ConstraintReplaceNLorentz
  , ConstraintUpdateNLorentz
  , DuupX (..)
  , ReplaceN (..)
  , UpdateN (..)
  , dropX
  , cloneX
  , duupX
  , framedN
  , caar
  , cadr
  , cdar
  , cddr
  , ifRight
  , ifSome
  , when_
  , unless_
  , whenSome
  , whenNone
  , mapCar
  , mapCdr
  , papair
  , ppaiir
  , unpair
  , setCar
  , setCdr
  , setInsert
  , mapInsert
  , setInsertNew
  , mapInsertNew
  , deleteMap
  , setDelete
  , replaceN
  , updateN

  -- * Additional Morley macros
  , View (..)
  , Void_ (..)
  , VoidResult(..)
  , view_
  , mkView
  , wrapView
  , unwrapView
  , void_
  , mkVoid
  , wrapVoid
  , unwrapVoid
  , voidResultTag
  , dupTop2

  -- * Buildable utils for additional Morley macros
  , buildView
  , buildViewTuple

  -- * Macros for working with @address@ and @contract@-like types
  , addressToEpAddress
  , pushContractRef
  ) where

import Prelude hiding (compare, drop, some, swap)

import qualified Data.Kind as Kind
import Data.Singletons (SingI(..))
import Fmt (Buildable(..), Builder, pretty, tupleF, (+|), (|+))
import Fmt.Internal.Tuple (TupleF)
import qualified GHC.TypeLits as Lit
import GHC.TypeNats (type (-))
import qualified GHC.TypeNats as GHC (Nat)

import Lorentz.Annotation
import Lorentz.Arith
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints
import Lorentz.Doc
import Lorentz.Errors
import Lorentz.Ext (stackType)
import Lorentz.Instr
import Lorentz.Value
import Michelson.Typed (ConstraintDIG', ConstraintDIPN', ConstraintDUG', T)
import Michelson.Typed.Arith
import Michelson.Typed.Haskell.Value
import Util.Markdown
import Util.Peano
import Util.Type

----------------------------------------------------------------------------
-- Compare
----------------------------------------------------------------------------

eq :: NiceComparable n
   => n & n & s :-> Bool & s
eq :: (n & (n & s)) :-> (Bool & s)
eq = (n & (n & s)) :-> (Integer & s)
forall n (s :: [*]).
NiceComparable n =>
(n & (n & s)) :-> (Integer & s)
compare ((n & (n & s)) :-> (Integer & s))
-> ((Integer & s) :-> (Bool & s)) -> (n & (n & s)) :-> (Bool & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer & s) :-> (Bool & s)
forall n (s :: [*]).
UnaryArithOpHs Eq' n =>
(n & s) :-> (UnaryArithResHs Eq' n & s)
eq0

neq :: NiceComparable n
   => n & n & s :-> Bool & s
neq :: (n & (n & s)) :-> (Bool & s)
neq = (n & (n & s)) :-> (Integer & s)
forall n (s :: [*]).
NiceComparable n =>
(n & (n & s)) :-> (Integer & s)
compare ((n & (n & s)) :-> (Integer & s))
-> ((Integer & s) :-> (Bool & s)) -> (n & (n & s)) :-> (Bool & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer & s) :-> (Bool & s)
forall n (s :: [*]).
UnaryArithOpHs Neq n =>
(n & s) :-> (UnaryArithResHs Neq n & s)
neq0

gt :: NiceComparable n
   => n & n & s :-> Bool & s
gt :: (n & (n & s)) :-> (Bool & s)
gt = (n & (n & s)) :-> (Integer & s)
forall n (s :: [*]).
NiceComparable n =>
(n & (n & s)) :-> (Integer & s)
compare ((n & (n & s)) :-> (Integer & s))
-> ((Integer & s) :-> (Bool & s)) -> (n & (n & s)) :-> (Bool & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer & s) :-> (Bool & s)
forall n (s :: [*]).
UnaryArithOpHs Gt n =>
(n & s) :-> (UnaryArithResHs Gt n & s)
gt0

le :: NiceComparable n
   => n & n & s :-> Bool & s
le :: (n & (n & s)) :-> (Bool & s)
le = (n & (n & s)) :-> (Integer & s)
forall n (s :: [*]).
NiceComparable n =>
(n & (n & s)) :-> (Integer & s)
compare ((n & (n & s)) :-> (Integer & s))
-> ((Integer & s) :-> (Bool & s)) -> (n & (n & s)) :-> (Bool & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer & s) :-> (Bool & s)
forall n (s :: [*]).
UnaryArithOpHs Le n =>
(n & s) :-> (UnaryArithResHs Le n & s)
le0

ge :: NiceComparable n
   => n & n & s :-> Bool & s
ge :: (n & (n & s)) :-> (Bool & s)
ge = (n & (n & s)) :-> (Integer & s)
forall n (s :: [*]).
NiceComparable n =>
(n & (n & s)) :-> (Integer & s)
compare ((n & (n & s)) :-> (Integer & s))
-> ((Integer & s) :-> (Bool & s)) -> (n & (n & s)) :-> (Bool & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer & s) :-> (Bool & s)
forall n (s :: [*]).
UnaryArithOpHs Ge n =>
(n & s) :-> (UnaryArithResHs Ge n & s)
ge0

lt :: NiceComparable n
   => n & n & s :-> Bool & s
lt :: (n & (n & s)) :-> (Bool & s)
lt = (n & (n & s)) :-> (Integer & s)
forall n (s :: [*]).
NiceComparable n =>
(n & (n & s)) :-> (Integer & s)
compare ((n & (n & s)) :-> (Integer & s))
-> ((Integer & s) :-> (Bool & s)) -> (n & (n & s)) :-> (Bool & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer & s) :-> (Bool & s)
forall n (s :: [*]).
UnaryArithOpHs Lt n =>
(n & s) :-> (UnaryArithResHs Lt n & s)
lt0

type IfCmp0Constraints a op =
  (UnaryArithOpHs op a, (UnaryArithResHs op a ~ Bool), SingI (ToT a))

ifEq0
  :: (IfCmp0Constraints a Eq')
  => (s :-> s') -> (s :-> s') -> (a & s :-> s')
ifEq0 :: (s :-> s') -> (s :-> s') -> (a & s) :-> s'
ifEq0 l :: s :-> s'
l r :: s :-> s'
r = (a & s) :-> (Bool : s)
forall n (s :: [*]).
UnaryArithOpHs Eq' n =>
(n & s) :-> (UnaryArithResHs Eq' n & s)
eq0 ((a & s) :-> (Bool : s)) -> ((Bool : s) :-> s') -> (a & s) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s'
l s :-> s'
r

ifNeq0
  :: (IfCmp0Constraints a Neq)
  => (s :-> s') -> (s :-> s') -> (a & s :-> s')
ifNeq0 :: (s :-> s') -> (s :-> s') -> (a & s) :-> s'
ifNeq0 l :: s :-> s'
l r :: s :-> s'
r = (a & s) :-> (Bool : s)
forall n (s :: [*]).
UnaryArithOpHs Neq n =>
(n & s) :-> (UnaryArithResHs Neq n & s)
neq0 ((a & s) :-> (Bool : s)) -> ((Bool : s) :-> s') -> (a & s) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s'
l s :-> s'
r

ifLt0
  :: (IfCmp0Constraints a Lt)
  => (s :-> s') -> (s :-> s') -> (a & s :-> s')
ifLt0 :: (s :-> s') -> (s :-> s') -> (a & s) :-> s'
ifLt0 l :: s :-> s'
l r :: s :-> s'
r = (a & s) :-> (Bool : s)
forall n (s :: [*]).
UnaryArithOpHs Lt n =>
(n & s) :-> (UnaryArithResHs Lt n & s)
lt0 ((a & s) :-> (Bool : s)) -> ((Bool : s) :-> s') -> (a & s) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s'
l s :-> s'
r

ifGt0
  :: (IfCmp0Constraints a Gt)
  => (s :-> s') -> (s :-> s') -> (a & s :-> s')
ifGt0 :: (s :-> s') -> (s :-> s') -> (a & s) :-> s'
ifGt0 l :: s :-> s'
l r :: s :-> s'
r = (a & s) :-> (Bool : s)
forall n (s :: [*]).
UnaryArithOpHs Gt n =>
(n & s) :-> (UnaryArithResHs Gt n & s)
gt0 ((a & s) :-> (Bool : s)) -> ((Bool : s) :-> s') -> (a & s) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s'
l s :-> s'
r

ifLe0
  :: (IfCmp0Constraints a Le)
  => (s :-> s') -> (s :-> s') -> (a & s :-> s')
ifLe0 :: (s :-> s') -> (s :-> s') -> (a & s) :-> s'
ifLe0 l :: s :-> s'
l r :: s :-> s'
r = (a & s) :-> (Bool : s)
forall n (s :: [*]).
UnaryArithOpHs Le n =>
(n & s) :-> (UnaryArithResHs Le n & s)
le0 ((a & s) :-> (Bool : s)) -> ((Bool : s) :-> s') -> (a & s) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s'
l s :-> s'
r

ifGe0
  :: (IfCmp0Constraints a Ge)
  => (s :-> s') -> (s :-> s') -> (a & s :-> s')
ifGe0 :: (s :-> s') -> (s :-> s') -> (a & s) :-> s'
ifGe0 l :: s :-> s'
l r :: s :-> s'
r = (a & s) :-> (Bool : s)
forall n (s :: [*]).
UnaryArithOpHs Ge n =>
(n & s) :-> (UnaryArithResHs Ge n & s)
ge0 ((a & s) :-> (Bool : s)) -> ((Bool : s) :-> s') -> (a & s) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s'
l s :-> s'
r

ifEq
  :: NiceComparable a
  => (s :-> s') -> (s :-> s') -> (a & a & s :-> s')
ifEq :: (s :-> s') -> (s :-> s') -> (a & (a & s)) :-> s'
ifEq l :: s :-> s'
l r :: s :-> s'
r = (a & (a & s)) :-> (Bool & s)
forall n (s :: [*]).
NiceComparable n =>
(n & (n & s)) :-> (Bool & s)
eq ((a & (a & s)) :-> (Bool & s))
-> ((Bool & s) :-> s') -> (a & (a & s)) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s'
l s :-> s'
r

ifNeq
  :: NiceComparable a
  => (s :-> s') -> (s :-> s') -> (a & a & s :-> s')
ifNeq :: (s :-> s') -> (s :-> s') -> (a & (a & s)) :-> s'
ifNeq l :: s :-> s'
l r :: s :-> s'
r = (a & (a & s)) :-> (Bool & s)
forall n (s :: [*]).
NiceComparable n =>
(n & (n & s)) :-> (Bool & s)
neq ((a & (a & s)) :-> (Bool & s))
-> ((Bool & s) :-> s') -> (a & (a & s)) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s'
l s :-> s'
r

ifLt
  :: NiceComparable a
  => (s :-> s') -> (s :-> s') -> (a & a & s :-> s')
ifLt :: (s :-> s') -> (s :-> s') -> (a & (a & s)) :-> s'
ifLt l :: s :-> s'
l r :: s :-> s'
r = (a & (a & s)) :-> (Bool & s)
forall n (s :: [*]).
NiceComparable n =>
(n & (n & s)) :-> (Bool & s)
lt ((a & (a & s)) :-> (Bool & s))
-> ((Bool & s) :-> s') -> (a & (a & s)) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s'
l s :-> s'
r

ifGt
  :: NiceComparable a
  => (s :-> s') -> (s :-> s') -> (a & a & s :-> s')
ifGt :: (s :-> s') -> (s :-> s') -> (a & (a & s)) :-> s'
ifGt l :: s :-> s'
l r :: s :-> s'
r = (a & (a & s)) :-> (Bool & s)
forall n (s :: [*]).
NiceComparable n =>
(n & (n & s)) :-> (Bool & s)
gt ((a & (a & s)) :-> (Bool & s))
-> ((Bool & s) :-> s') -> (a & (a & s)) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s'
l s :-> s'
r

ifLe
  :: NiceComparable a
  => (s :-> s') -> (s :-> s') -> (a & a & s :-> s')
ifLe :: (s :-> s') -> (s :-> s') -> (a & (a & s)) :-> s'
ifLe l :: s :-> s'
l r :: s :-> s'
r = (a & (a & s)) :-> (Bool & s)
forall n (s :: [*]).
NiceComparable n =>
(n & (n & s)) :-> (Bool & s)
le ((a & (a & s)) :-> (Bool & s))
-> ((Bool & s) :-> s') -> (a & (a & s)) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s'
l s :-> s'
r

ifGe
  :: NiceComparable a
  => (s :-> s') -> (s :-> s') -> (a & a & s :-> s')
ifGe :: (s :-> s') -> (s :-> s') -> (a & (a & s)) :-> s'
ifGe l :: s :-> s'
l r :: s :-> s'
r = (a & (a & s)) :-> (Bool & s)
forall n (s :: [*]).
NiceComparable n =>
(n & (n & s)) :-> (Bool & s)
ge ((a & (a & s)) :-> (Bool & s))
-> ((Bool & s) :-> s') -> (a & (a & s)) :-> s'
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s'
l s :-> s'
r

----------------------------------------------------------------------------
-- Fail
----------------------------------------------------------------------------

-- | Analog of the FAIL macro in Michelson. Its usage is discouraged
-- because it doesn't carry any information about failure.
{-# WARNING fail_ "'fail_' remains in code" #-}
fail_ :: a :-> c
fail_ :: a :-> c
fail_ = a :-> (() & a)
forall (s :: [*]). s :-> (() & s)
unit (a :-> (() & a)) -> ((() & a) :-> c) -> a :-> c
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (() & a) :-> c
forall a (s :: [*]) (t :: [*]). KnownValue a => (a & s) :-> t
failWith

----------------------------------------------------------------------------
-- Assertions
----------------------------------------------------------------------------

assert :: IsError err => err -> Bool & s :-> s
assert :: err -> (Bool & s) :-> s
assert reason :: err
reason = (s :-> s) -> (s :-> s) -> (Bool & s) :-> s
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s
forall (s :: [*]). s :-> s
nop (err -> s :-> s
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason)

assertEq0 :: (IfCmp0Constraints a Eq', IsError err) => err -> a & s :-> s
assertEq0 :: err -> (a & s) :-> s
assertEq0 reason :: err
reason = (s :-> s) -> (s :-> s) -> (a & s) :-> s
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Eq' =>
(s :-> s') -> (s :-> s') -> (a & s) :-> s'
ifEq0 s :-> s
forall (s :: [*]). s :-> s
nop (err -> s :-> s
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason)

assertNeq0 :: (IfCmp0Constraints a Neq, IsError err) => err -> a & s :-> s
assertNeq0 :: err -> (a & s) :-> s
assertNeq0 reason :: err
reason = (s :-> s) -> (s :-> s) -> (a & s) :-> s
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Neq =>
(s :-> s') -> (s :-> s') -> (a & s) :-> s'
ifNeq0 s :-> s
forall (s :: [*]). s :-> s
nop (err -> s :-> s
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason)

assertLt0 :: (IfCmp0Constraints a Lt, IsError err) => err -> a & s :-> s
assertLt0 :: err -> (a & s) :-> s
assertLt0 reason :: err
reason = (s :-> s) -> (s :-> s) -> (a & s) :-> s
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Lt =>
(s :-> s') -> (s :-> s') -> (a & s) :-> s'
ifLt0 s :-> s
forall (s :: [*]). s :-> s
nop (err -> s :-> s
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason)

assertGt0 :: (IfCmp0Constraints a Gt, IsError err) => err -> a & s :-> s
assertGt0 :: err -> (a & s) :-> s
assertGt0 reason :: err
reason = (s :-> s) -> (s :-> s) -> (a & s) :-> s
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Gt =>
(s :-> s') -> (s :-> s') -> (a & s) :-> s'
ifGt0 s :-> s
forall (s :: [*]). s :-> s
nop (err -> s :-> s
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason)

assertLe0 :: (IfCmp0Constraints a Le, IsError err) => err -> a & s :-> s
assertLe0 :: err -> (a & s) :-> s
assertLe0 reason :: err
reason = (s :-> s) -> (s :-> s) -> (a & s) :-> s
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Le =>
(s :-> s') -> (s :-> s') -> (a & s) :-> s'
ifLe0 s :-> s
forall (s :: [*]). s :-> s
nop (err -> s :-> s
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason)

assertGe0 :: (IfCmp0Constraints a Ge, IsError err) => err -> a & s :-> s
assertGe0 :: err -> (a & s) :-> s
assertGe0 reason :: err
reason = (s :-> s) -> (s :-> s) -> (a & s) :-> s
forall a (s :: [*]) (s' :: [*]).
IfCmp0Constraints a Ge =>
(s :-> s') -> (s :-> s') -> (a & s) :-> s'
ifGe0 s :-> s
forall (s :: [*]). s :-> s
nop (err -> s :-> s
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason)

assertEq :: (NiceComparable a, IsError err) => err -> a & a & s :-> s
assertEq :: err -> (a & (a & s)) :-> s
assertEq reason :: err
reason = (s :-> s) -> (s :-> s) -> (a & (a & s)) :-> s
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a & (a & s)) :-> s'
ifEq s :-> s
forall (s :: [*]). s :-> s
nop (err -> s :-> s
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason)

assertNeq :: (NiceComparable a, IsError err) => err -> a & a & s :-> s
assertNeq :: err -> (a & (a & s)) :-> s
assertNeq reason :: err
reason = (s :-> s) -> (s :-> s) -> (a & (a & s)) :-> s
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a & (a & s)) :-> s'
ifNeq s :-> s
forall (s :: [*]). s :-> s
nop (err -> s :-> s
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason)

assertLt :: (NiceComparable a, IsError err) => err -> a & a & s :-> s
assertLt :: err -> (a & (a & s)) :-> s
assertLt reason :: err
reason = (s :-> s) -> (s :-> s) -> (a & (a & s)) :-> s
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a & (a & s)) :-> s'
ifLt s :-> s
forall (s :: [*]). s :-> s
nop (err -> s :-> s
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason)

assertGt :: (NiceComparable a, IsError err) => err -> a & a & s :-> s
assertGt :: err -> (a & (a & s)) :-> s
assertGt reason :: err
reason = (s :-> s) -> (s :-> s) -> (a & (a & s)) :-> s
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a & (a & s)) :-> s'
ifGt s :-> s
forall (s :: [*]). s :-> s
nop (err -> s :-> s
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason)

assertLe :: (NiceComparable a, IsError err) => err -> a & a & s :-> s
assertLe :: err -> (a & (a & s)) :-> s
assertLe reason :: err
reason = (s :-> s) -> (s :-> s) -> (a & (a & s)) :-> s
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a & (a & s)) :-> s'
ifLe s :-> s
forall (s :: [*]). s :-> s
nop (err -> s :-> s
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason)

assertGe :: (NiceComparable a, IsError err) => err -> a & a & s :-> s
assertGe :: err -> (a & (a & s)) :-> s
assertGe reason :: err
reason = (s :-> s) -> (s :-> s) -> (a & (a & s)) :-> s
forall a (s :: [*]) (s' :: [*]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a & (a & s)) :-> s'
ifGe s :-> s
forall (s :: [*]). s :-> s
nop (err -> s :-> s
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason)

assertNone :: IsError err => err -> Maybe a & s :-> s
assertNone :: err -> (Maybe a & s) :-> s
assertNone reason :: err
reason = (s :-> s) -> ((a & s) :-> s) -> (Maybe a & s) :-> s
forall (s :: [*]) (s' :: [*]) a.
(s :-> s') -> ((a & s) :-> s') -> (Maybe a & s) :-> s'
ifNone s :-> s
forall (s :: [*]). s :-> s
nop (err -> (a & s) :-> s
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason)

assertSome :: IsError err => err -> Maybe a & s :-> a & s
assertSome :: err -> (Maybe a & s) :-> (a & s)
assertSome reason :: err
reason = (s :-> (a & s))
-> ((a & s) :-> (a & s)) -> (Maybe a & s) :-> (a & s)
forall (s :: [*]) (s' :: [*]) a.
(s :-> s') -> ((a & s) :-> s') -> (Maybe a & s) :-> s'
ifNone (err -> s :-> (a & s)
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason) (a & s) :-> (a & s)
forall (s :: [*]). s :-> s
nop

assertLeft :: IsError err => err -> Either a b & s :-> a & s
assertLeft :: err -> (Either a b & s) :-> (a & s)
assertLeft reason :: err
reason = ((a & s) :-> (a & s))
-> ((b & s) :-> (a & s)) -> (Either a b & s) :-> (a & s)
forall a (s :: [*]) (s' :: [*]) b.
((a & s) :-> s') -> ((b & s) :-> s') -> (Either a b & s) :-> s'
ifLeft (a & s) :-> (a & s)
forall (s :: [*]). s :-> s
nop (err -> (b & s) :-> (a & s)
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason)

assertRight :: IsError err => err -> Either a b & s :-> b & s
assertRight :: err -> (Either a b & s) :-> (b & s)
assertRight reason :: err
reason = ((a & s) :-> (b & s))
-> ((b & s) :-> (b & s)) -> (Either a b & s) :-> (b & s)
forall a (s :: [*]) (s' :: [*]) b.
((a & s) :-> s') -> ((b & s) :-> s') -> (Either a b & s) :-> s'
ifLeft (err -> (a & s) :-> (b & s)
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing err
reason) (b & s) :-> (b & s)
forall (s :: [*]). s :-> s
nop

assertUsing
  :: IsError a
  => a -> Bool & s :-> s
assertUsing :: a -> (Bool & s) :-> s
assertUsing err :: a
err = (s :-> s) -> (s :-> s) -> (Bool & s) :-> s
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s
forall (s :: [*]). s :-> s
nop ((s :-> s) -> (Bool & s) :-> s) -> (s :-> s) -> (Bool & s) :-> s
forall a b. (a -> b) -> a -> b
$ a -> s :-> s
forall e (s :: [*]) (t :: [*]). IsError e => e -> s :-> t
failUsing a
err

----------------------------------------------------------------------------
-- Syntactic Conveniences
----------------------------------------------------------------------------

-- | Custom Lorentz macro that drops element with given index
-- (starting from 0) from the stack.
dropX
  :: forall (n :: GHC.Nat) a inp out s s'.
  ( ConstraintDIPNLorentz (ToPeano n) inp out s s'
  , s ~ (a ': s')
  )
  => inp :-> out
dropX :: inp :-> out
dropX = (s :-> s') -> inp :-> out
forall (n :: Nat) (inp :: [*]) (out :: [*]) (s :: [*]) (s' :: [*]).
ConstraintDIPNLorentz (ToPeano n) inp out s s' =>
(s :-> s') -> inp :-> out
dipN @n @inp @out @s @s' s :-> s'
forall a (s :: [*]). (a & s) :-> s
drop

class CloneX (n :: Peano) a s where
  type CloneXT n a s :: [Kind.Type]
  cloneXImpl :: a & s :-> CloneXT n a s
instance CloneX 'Z a s where
  type CloneXT 'Z a s = a & s
  cloneXImpl :: (a & s) :-> CloneXT 'Z a s
cloneXImpl = (a & s) :-> CloneXT 'Z a s
forall (s :: [*]). s :-> s
nop
instance (CloneX n a s) => CloneX ('S n) a s where
  type CloneXT ('S n) a s = a ': CloneXT n a s
  cloneXImpl :: (a & s) :-> CloneXT ('S n) a s
cloneXImpl = (a & s) :-> (a & (a & s))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
dup ((a & s) :-> (a & (a & s)))
-> ((a & (a & s)) :-> (a & CloneXT n a s))
-> (a & s) :-> (a & CloneXT n a s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a & s) :-> CloneXT n a s)
-> (a & (a & s)) :-> (a & CloneXT n a s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (forall a (s :: [*]). CloneX n a s => (a & s) :-> CloneXT n a s
forall (n :: Peano) a (s :: [*]).
CloneX n a s =>
(a & s) :-> CloneXT n a s
cloneXImpl @n)

-- | Duplicate the top of the stack @n@ times.
--
-- For example, `cloneX @3` has type `a & s :-> a & a & a & a & s`.
cloneX
  :: forall (n :: GHC.Nat) a s. CloneX (ToPeano n) a s
  => a & s :-> CloneXT (ToPeano n) a s
cloneX :: (a & s) :-> CloneXT (ToPeano n) a s
cloneX = forall a (s :: [*]).
CloneX (ToPeano n) a s =>
(a & s) :-> CloneXT (ToPeano n) a s
forall (n :: Peano) a (s :: [*]).
CloneX n a s =>
(a & s) :-> CloneXT n a s
cloneXImpl @(ToPeano n)

-- | Kind-agnostic constraint for duupX
type DuupXConstraint' kind (n :: Peano)
  (s :: [kind]) (a :: kind) (s1 :: [kind]) (tail :: [kind]) =
  ( tail ~ Drop ('S n) s
  , ConstraintDIPN' kind n s s1 (a ': tail) (a ': a ': tail)
  , ConstraintDIG' kind n s1 (a ': s) a
  )

-- | Constraint for duupX that combines kind-agnostic constraint for
-- Lorentz (Haskell) types and for our typed Michelson.
type ConstraintDuupXLorentz (n :: Peano)
  (s :: [Kind.Type]) (a :: Kind.Type)
  (s1 :: [Kind.Type]) (tail :: [Kind.Type]) =
  ( DuupXConstraint' T n (ToTs s) (ToT a) (ToTs s1) (ToTs tail)
  , DuupXConstraint' Kind.Type n s a s1 tail
  )

class DuupX (n :: Peano) (s :: [Kind.Type]) (a :: Kind.Type) s1 tail where
  duupXImpl :: s :-> a ': s

instance {-# OVERLAPPING #-} (s ~ (a ': xs)) => DuupX ('S 'Z) s a s1 tail where
  duupXImpl :: s :-> (a : s)
duupXImpl = s :-> (a : s)
forall a (s :: [*]). (a & s) :-> (a & (a & s))
dup

instance {-# OVERLAPPING #-} DuupX ('S ('S 'Z)) (b ': a ': xs) a s1 tail where
  duupXImpl :: (b : a : xs) :-> (a : b : a : xs)
duupXImpl = ((a : xs) :-> (a & (a : xs)))
-> (b : a : xs) :-> (b & (a & (a : xs)))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (a : xs) :-> (a & (a : xs))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
dup ((b : a : xs) :-> (b & (a & (a : xs))))
-> ((b & (a & (a : xs))) :-> (a : b : a : xs))
-> (b : a : xs) :-> (a : b : a : xs)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b & (a & (a : xs))) :-> (a : b : a : xs)
forall a b (s :: [*]). (a & (b & s)) :-> (b & (a & s))
swap

instance {-# OVERLAPPABLE #-} (ConstraintDuupXLorentz ('S ('S n)) s a s1 tail) =>
  DuupX ('S ('S ('S n))) s a s1 tail where
  duupXImpl :: s :-> (a : s)
duupXImpl =
    -- 'stackType' helps GHC deduce types
    ((a & tail) :-> (a : (a & tail))) -> s :-> s1
forall (n :: Peano) (inp :: [*]) (out :: [*]) (s :: [*])
       (s' :: [*]).
ConstraintDIPNLorentz n inp out s s' =>
(s :-> s') -> inp :-> out
dipNPeano @('S ('S n)) ((a & tail) :-> (a : (a & tail))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
dup ((a & tail) :-> (a : (a & tail)))
-> ((a : (a & tail)) :-> (a : (a & tail)))
-> (a & tail) :-> (a : (a & tail))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : (a & tail)) :-> (a : (a & tail))
forall (s :: [*]). s :-> s
stackType @(a ': a ': tail)) (s :-> s1) -> (s1 :-> (a : s)) -> s :-> (a : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
    forall (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz ('S ('S n)) inp out a =>
inp :-> out
forall (n :: Peano) (inp :: [*]) (out :: [*]) a.
ConstraintDIGLorentz n inp out a =>
inp :-> out
digPeano @('S ('S n))

-- | @DUU+P@ macro. For example, `duupX @3` is `DUUUP`, it puts
-- the 3-rd (starting from 1) element to the top of the stack.
-- Note that it is implemented differently for `n ≤ 2` and for `n > 2`.
-- In the latter case it is implemented using `dipN`, `dig` and `dup`.
-- In the former case it uses specialized versions.
-- There is also a minor difference with the implementation of `DUU*P` in
-- Michelson.
-- They implement `DUUUUP` as `DIP 3 { DUP }; DIG 4`.
-- We implement it as `DIP 3 { DUP }; DIG 3`. These are equivalent.
-- Our version is supposedly cheaper, at least it should be packed
-- more efficiently due to the way numbers are packed.
duupX :: forall (n :: GHC.Nat) a (s :: [Kind.Type]) (s1 :: [Kind.Type]) (tail :: [Kind.Type]).
  ( ConstraintDuupXLorentz (ToPeano (n - 1)) s a s1 tail
  , DuupX (ToPeano n) s a s1 tail
  )
  => s :-> a ': s
duupX :: s :-> (a : s)
duupX = DuupX (ToPeano n) s a s1 tail => s :-> (a : s)
forall k k (n :: Peano) (s :: [*]) a (s1 :: k) (tail :: k).
DuupX n s a s1 tail =>
s :-> (a : s)
duupXImpl @(ToPeano n) @s @a @s1 @tail
  where
    _example ::
      '[ Integer, (), Bool ] :->
      '[ Bool, Integer, (), Bool ]
    _example :: '[Integer, (), Bool] :-> '[Bool, Integer, (), Bool]
_example = forall a (s :: [*]) (s1 :: [*]) (tail :: [*]).
(ConstraintDuupXLorentz (ToPeano (3 - 1)) s a s1 tail,
 DuupX (ToPeano 3) s a s1 tail) =>
s :-> (a : s)
forall (n :: Nat) a (s :: [*]) (s1 :: [*]) (tail :: [*]).
(ConstraintDuupXLorentz (ToPeano (n - 1)) s a s1 tail,
 DuupX (ToPeano n) s a s1 tail) =>
s :-> (a : s)
duupX @3

-- | Version of 'framed' which accepts number of elements on input stack
-- which should be preserved.
--
-- You can treat this macro as calling a Michelson function with given number
-- of arguments.
framedN
  :: forall n nNat s i i' o o'.
     ( nNat ~ ToPeano n
     , i' ~ Take nNat i, s ~ Drop nNat i
     , i ~ (i' ++ s), o ~ (o' ++ s)
     , KnownList i', KnownList o'
     )
  => (i' :-> o') -> (i :-> o)
framedN :: (i' :-> o') -> i :-> o
framedN = forall (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed @s
  where
  _example
    :: [Integer, Natural] :-> '[ByteString]
    -> Integer : Natural : () : s :-> ByteString : () : s
  _example :: ('[Integer, Natural] :-> '[ByteString])
-> (Integer : Natural : () : s) :-> (ByteString : () : s)
_example = forall (n :: Nat) (nNat :: Peano) (s :: [*]) (i :: [*]) (i' :: [*])
       (o :: [*]) (o' :: [*]).
(nNat ~ ToPeano n, i' ~ Take nNat i, s ~ Drop nNat i,
 i ~ (i' ++ s), o ~ (o' ++ s), KnownList i', KnownList o') =>
(i' :-> o') -> i :-> o
forall (nNat :: Peano) (s :: [*]) (i :: [*]) (i' :: [*]) (o :: [*])
       (o' :: [*]).
(nNat ~ ToPeano 2, i' ~ Take nNat i, s ~ Drop nNat i,
 i ~ (i' ++ s), o ~ (o' ++ s), KnownList i', KnownList o') =>
(i' :-> o') -> i :-> o
framedN @2

papair :: a & b & c & s :-> ((a, b), c) & s
papair :: (a & (b & (c & s))) :-> (((a, b), c) & s)
papair = (a & (b & (c & s))) :-> ((a, b) & (c & s))
forall a b (s :: [*]). (a & (b & s)) :-> ((a, b) & s)
pair ((a & (b & (c & s))) :-> ((a, b) & (c & s)))
-> (((a, b) & (c & s)) :-> (((a, b), c) & s))
-> (a & (b & (c & s))) :-> (((a, b), c) & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, b) & (c & s)) :-> (((a, b), c) & s)
forall a b (s :: [*]). (a & (b & s)) :-> ((a, b) & s)
pair

ppaiir :: a & b & c & s :-> (a, (b, c)) & s
ppaiir :: (a & (b & (c & s))) :-> ((a, (b, c)) & s)
ppaiir = ((b & (c & s)) :-> ((b, c) & s))
-> (a & (b & (c & s))) :-> (a & ((b, c) & s))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (b & (c & s)) :-> ((b, c) & s)
forall a b (s :: [*]). (a & (b & s)) :-> ((a, b) & s)
pair ((a & (b & (c & s))) :-> (a & ((b, c) & s)))
-> ((a & ((b, c) & s)) :-> ((a, (b, c)) & s))
-> (a & (b & (c & s))) :-> ((a, (b, c)) & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a & ((b, c) & s)) :-> ((a, (b, c)) & s)
forall a b (s :: [*]). (a & (b & s)) :-> ((a, b) & s)
pair

unpair :: (a, b) & s :-> a & b & s
unpair :: ((a, b) & s) :-> (a & (b & s))
unpair = ((a, b) & s) :-> ((a, b) & ((a, b) & s))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
dup (((a, b) & s) :-> ((a, b) & ((a, b) & s)))
-> (((a, b) & ((a, b) & s)) :-> (a & ((a, b) & s)))
-> ((a, b) & s) :-> (a & ((a, b) & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, b) & ((a, b) & s)) :-> (a & ((a, b) & s))
forall a b (s :: [*]). ((a, b) & s) :-> (a & s)
car (((a, b) & s) :-> (a & ((a, b) & s)))
-> ((a & ((a, b) & s)) :-> (a & (b & s)))
-> ((a, b) & s) :-> (a & (b & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (((a, b) & s) :-> (b & s)) -> (a & ((a, b) & s)) :-> (a & (b & s))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip ((a, b) & s) :-> (b & s)
forall a b (s :: [*]). ((a, b) & s) :-> (b & s)
cdr

cdar :: (a1, (a2, b)) & s :-> a2 & s
cdar :: ((a1, (a2, b)) & s) :-> (a2 & s)
cdar = ((a1, (a2, b)) & s) :-> ((a2, b) & s)
forall a b (s :: [*]). ((a, b) & s) :-> (b & s)
cdr (((a1, (a2, b)) & s) :-> ((a2, b) & s))
-> (((a2, b) & s) :-> (a2 & s)) -> ((a1, (a2, b)) & s) :-> (a2 & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a2, b) & s) :-> (a2 & s)
forall a b (s :: [*]). ((a, b) & s) :-> (a & s)
car

cddr :: (a1, (a2, b)) & s :-> b & s
cddr :: ((a1, (a2, b)) & s) :-> (b & s)
cddr = ((a1, (a2, b)) & s) :-> ((a2, b) & s)
forall a b (s :: [*]). ((a, b) & s) :-> (b & s)
cdr (((a1, (a2, b)) & s) :-> ((a2, b) & s))
-> (((a2, b) & s) :-> (b & s)) -> ((a1, (a2, b)) & s) :-> (b & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a2, b) & s) :-> (b & s)
forall a b (s :: [*]). ((a, b) & s) :-> (b & s)
cdr

caar :: ((a, b1), b2) & s :-> a & s
caar :: (((a, b1), b2) & s) :-> (a & s)
caar = (((a, b1), b2) & s) :-> ((a, b1) & s)
forall a b (s :: [*]). ((a, b) & s) :-> (a & s)
car ((((a, b1), b2) & s) :-> ((a, b1) & s))
-> (((a, b1) & s) :-> (a & s)) -> (((a, b1), b2) & s) :-> (a & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, b1) & s) :-> (a & s)
forall a b (s :: [*]). ((a, b) & s) :-> (a & s)
car

cadr :: ((a, b1), b2) & s :-> b1 & s
cadr :: (((a, b1), b2) & s) :-> (b1 & s)
cadr = (((a, b1), b2) & s) :-> ((a, b1) & s)
forall a b (s :: [*]). ((a, b) & s) :-> (a & s)
car ((((a, b1), b2) & s) :-> ((a, b1) & s))
-> (((a, b1) & s) :-> (b1 & s)) -> (((a, b1), b2) & s) :-> (b1 & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, b1) & s) :-> (b1 & s)
forall a b (s :: [*]). ((a, b) & s) :-> (b & s)
cdr

setCar :: (a, b1) & (b2 & s) :-> (b2, b1) & s
setCar :: ((a, b1) & (b2 & s)) :-> ((b2, b1) & s)
setCar = ((a, b1) & (b2 & s)) :-> (b1 & (b2 & s))
forall a b (s :: [*]). ((a, b) & s) :-> (b & s)
cdr (((a, b1) & (b2 & s)) :-> (b1 & (b2 & s)))
-> ((b1 & (b2 & s)) :-> (b2 & (b1 & s)))
-> ((a, b1) & (b2 & s)) :-> (b2 & (b1 & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b1 & (b2 & s)) :-> (b2 & (b1 & s))
forall a b (s :: [*]). (a & (b & s)) :-> (b & (a & s))
swap (((a, b1) & (b2 & s)) :-> (b2 & (b1 & s)))
-> ((b2 & (b1 & s)) :-> ((b2, b1) & s))
-> ((a, b1) & (b2 & s)) :-> ((b2, b1) & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b2 & (b1 & s)) :-> ((b2, b1) & s)
forall a b (s :: [*]). (a & (b & s)) :-> ((a, b) & s)
pair

setCdr :: (a, b1) & (b2 & s) :-> (a, b2) & s
setCdr :: ((a, b1) & (b2 & s)) :-> ((a, b2) & s)
setCdr = ((a, b1) & (b2 & s)) :-> (a & (b2 & s))
forall a b (s :: [*]). ((a, b) & s) :-> (a & s)
car (((a, b1) & (b2 & s)) :-> (a & (b2 & s)))
-> ((a & (b2 & s)) :-> ((a, b2) & s))
-> ((a, b1) & (b2 & s)) :-> ((a, b2) & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a & (b2 & s)) :-> ((a, b2) & s)
forall a b (s :: [*]). (a & (b & s)) :-> ((a, b) & s)
pair

mapCar
  :: a & s :-> a1 & s
  -> (a, b) & s :-> (a1, b) & s
mapCar :: ((a & s) :-> (a1 & s)) -> ((a, b) & s) :-> ((a1, b) & s)
mapCar op :: (a & s) :-> (a1 & s)
op = ((a, b) & s) :-> ((a, b) & ((a, b) & s))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
dup (((a, b) & s) :-> ((a, b) & ((a, b) & s)))
-> (((a, b) & ((a, b) & s)) :-> (b & ((a, b) & s)))
-> ((a, b) & s) :-> (b & ((a, b) & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, b) & ((a, b) & s)) :-> (b & ((a, b) & s))
forall a b (s :: [*]). ((a, b) & s) :-> (b & s)
cdr (((a, b) & s) :-> (b & ((a, b) & s)))
-> ((b & ((a, b) & s)) :-> (b & (a1 & s)))
-> ((a, b) & s) :-> (b & (a1 & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (((a, b) & s) :-> (a1 & s))
-> (b & ((a, b) & s)) :-> (b & (a1 & s))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (((a, b) & s) :-> (a & s)
forall a b (s :: [*]). ((a, b) & s) :-> (a & s)
car (((a, b) & s) :-> (a & s))
-> ((a & s) :-> (a1 & s)) -> ((a, b) & s) :-> (a1 & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a & s) :-> (a1 & s)
op) (((a, b) & s) :-> (b & (a1 & s)))
-> ((b & (a1 & s)) :-> (a1 & (b & s)))
-> ((a, b) & s) :-> (a1 & (b & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b & (a1 & s)) :-> (a1 & (b & s))
forall a b (s :: [*]). (a & (b & s)) :-> (b & (a & s))
swap (((a, b) & s) :-> (a1 & (b & s)))
-> ((a1 & (b & s)) :-> ((a1, b) & s))
-> ((a, b) & s) :-> ((a1, b) & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a1 & (b & s)) :-> ((a1, b) & s)
forall a b (s :: [*]). (a & (b & s)) :-> ((a, b) & s)
pair

mapCdr
  :: b & (a, b) & s :-> b1 & (a, b) & s
  -> (a, b) & s :-> (a, b1) & s
mapCdr :: ((b & ((a, b) & s)) :-> (b1 & ((a, b) & s)))
-> ((a, b) & s) :-> ((a, b1) & s)
mapCdr op :: (b & ((a, b) & s)) :-> (b1 & ((a, b) & s))
op = ((a, b) & s) :-> ((a, b) & ((a, b) & s))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
dup (((a, b) & s) :-> ((a, b) & ((a, b) & s)))
-> (((a, b) & ((a, b) & s)) :-> (b & ((a, b) & s)))
-> ((a, b) & s) :-> (b & ((a, b) & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, b) & ((a, b) & s)) :-> (b & ((a, b) & s))
forall a b (s :: [*]). ((a, b) & s) :-> (b & s)
cdr (((a, b) & s) :-> (b & ((a, b) & s)))
-> ((b & ((a, b) & s)) :-> (b1 & ((a, b) & s)))
-> ((a, b) & s) :-> (b1 & ((a, b) & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b & ((a, b) & s)) :-> (b1 & ((a, b) & s))
op (((a, b) & s) :-> (b1 & ((a, b) & s)))
-> ((b1 & ((a, b) & s)) :-> ((a, b) & (b1 & s)))
-> ((a, b) & s) :-> ((a, b) & (b1 & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b1 & ((a, b) & s)) :-> ((a, b) & (b1 & s))
forall a b (s :: [*]). (a & (b & s)) :-> (b & (a & s))
swap (((a, b) & s) :-> ((a, b) & (b1 & s)))
-> (((a, b) & (b1 & s)) :-> (a & (b1 & s)))
-> ((a, b) & s) :-> (a & (b1 & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, b) & (b1 & s)) :-> (a & (b1 & s))
forall a b (s :: [*]). ((a, b) & s) :-> (a & s)
car (((a, b) & s) :-> (a & (b1 & s)))
-> ((a & (b1 & s)) :-> ((a, b1) & s))
-> ((a, b) & s) :-> ((a, b1) & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a & (b1 & s)) :-> ((a, b1) & s)
forall a b (s :: [*]). (a & (b & s)) :-> ((a, b) & s)
pair

ifRight :: (b & s :-> s') -> (a & s :-> s') -> (Either a b & s :-> s')
ifRight :: ((b & s) :-> s') -> ((a & s) :-> s') -> (Either a b & s) :-> s'
ifRight l :: (b & s) :-> s'
l r :: (a & s) :-> s'
r = ((a & s) :-> s') -> ((b & s) :-> s') -> (Either a b & s) :-> s'
forall a (s :: [*]) (s' :: [*]) b.
((a & s) :-> s') -> ((b & s) :-> s') -> (Either a b & s) :-> s'
ifLeft (a & s) :-> s'
r (b & s) :-> s'
l

ifSome
  :: (a & s :-> s') -> (s :-> s') -> (Maybe a & s :-> s')
ifSome :: ((a & s) :-> s') -> (s :-> s') -> (Maybe a & s) :-> s'
ifSome s :: (a & s) :-> s'
s n :: s :-> s'
n = (s :-> s') -> ((a & s) :-> s') -> (Maybe a & s) :-> s'
forall (s :: [*]) (s' :: [*]) a.
(s :-> s') -> ((a & s) :-> s') -> (Maybe a & s) :-> s'
ifNone s :-> s'
n (a & s) :-> s'
s

when_ :: (s :-> s) -> (Bool : s :-> s)
when_ :: (s :-> s) -> (Bool : s) :-> s
when_ i :: s :-> s
i = (s :-> s) -> (s :-> s) -> (Bool : s) :-> s
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s
i s :-> s
forall (s :: [*]). s :-> s
nop

unless_ :: (s :-> s) -> (Bool : s :-> s)
unless_ :: (s :-> s) -> (Bool : s) :-> s
unless_ i :: s :-> s
i = (s :-> s) -> (s :-> s) -> (Bool : s) :-> s
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool & s) :-> s'
if_ s :-> s
forall (s :: [*]). s :-> s
nop s :-> s
i

whenSome :: (a : s :-> s) -> (Maybe a : s :-> s)
whenSome :: ((a : s) :-> s) -> (Maybe a : s) :-> s
whenSome i :: (a : s) :-> s
i = ((a : s) :-> s) -> (s :-> s) -> (Maybe a : s) :-> s
forall a (s :: [*]) (s' :: [*]).
((a & s) :-> s') -> (s :-> s') -> (Maybe a & s) :-> s'
ifSome (a : s) :-> s
i s :-> s
forall (s :: [*]). s :-> s
nop

whenNone :: (s :-> a : s) -> (Maybe a : s :-> a : s)
whenNone :: (s :-> (a : s)) -> (Maybe a : s) :-> (a : s)
whenNone i :: s :-> (a : s)
i = (s :-> (a : s))
-> ((a : s) :-> (a : s)) -> (Maybe a : s) :-> (a : s)
forall (s :: [*]) (s' :: [*]) a.
(s :-> s') -> ((a & s) :-> s') -> (Maybe a & s) :-> s'
ifNone s :-> (a : s)
i (a : s) :-> (a : s)
forall (s :: [*]). s :-> s
nop

-- | Various convenient instructions on maps.
class MapInstrs map where
  -- | Specialized version of 'update'.
  mapUpdate :: NiceComparable k => k : Maybe v : map k v : s :-> map k v : s

  -- | Insert given element into map.
  mapInsert :: NiceComparable k => k : v : map k v : s :-> map k v : s
  mapInsert = ((v : map k v : s) :-> (Maybe v & (map k v : s)))
-> (k : v : map k v : s) :-> (k & (Maybe v & (map k v : s)))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (v : map k v : s) :-> (Maybe v & (map k v : s))
forall a (s :: [*]). (a & s) :-> (Maybe a & s)
some ((k : v : map k v : s) :-> (k & (Maybe v & (map k v : s))))
-> ((k & (Maybe v & (map k v : s))) :-> (map k v : s))
-> (k : v : map k v : s) :-> (map k v : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k & (Maybe v & (map k v : s))) :-> (map k v : s)
forall (map :: * -> * -> *) k v (s :: [*]).
(MapInstrs map, NiceComparable k) =>
(k : Maybe v : map k v : s) :-> (map k v : s)
mapUpdate

  -- | Insert given element into map, ensuring that it does not overwrite
  -- any existing entry.
  --
  -- As first argument accepts container name (for error message).
  mapInsertNew
    :: (NiceComparable k, KnownValue e)
    => (forall s0. k : s0 :-> e : s0)
    -> k : v : map k v : s :-> map k v : s

  -- | Delete element from the map.
  deleteMap
    :: forall k v s. (NiceComparable k, KnownValue v)
    => k : map k v : s :-> map k v : s
  deleteMap = ((map k v : s) :-> (Maybe v & (map k v : s)))
-> (k : map k v : s) :-> (k & (Maybe v & (map k v : s)))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (forall (s :: [*]). KnownValue v => s :-> (Maybe v & s)
forall a (s :: [*]). KnownValue a => s :-> (Maybe a & s)
none @v) ((k : map k v : s) :-> (k & (Maybe v & (map k v : s))))
-> ((k & (Maybe v & (map k v : s))) :-> (map k v : s))
-> (k : map k v : s) :-> (map k v : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k & (Maybe v & (map k v : s))) :-> (map k v : s)
forall (map :: * -> * -> *) k v (s :: [*]).
(MapInstrs map, NiceComparable k) =>
(k : Maybe v : map k v : s) :-> (map k v : s)
mapUpdate

instance MapInstrs Map where
  mapUpdate :: (k : Maybe v : Map k v : s) :-> (Map k v : s)
mapUpdate = (k : Maybe v : Map k v : s) :-> (Map k v : s)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c & (UpdOpParamsHs c & (c & s))) :-> (c & s)
update
  mapInsertNew :: (forall (s0 :: [*]). (k : s0) :-> (e : s0))
-> (k : v : Map k v : s) :-> (Map k v : s)
mapInsertNew mkErr :: forall (s0 :: [*]). (k : s0) :-> (e : s0)
mkErr = (forall (s0 :: [*]). (k : s0) :-> (e : s0))
-> (k : v : Map k v : s) :-> (k : v : Map k v : s)
forall c k (s :: [*]) v (st :: [*]) e.
(MemOpHs c, k ~ MemOpKeyHs c, KnownValue e,
 st ~ (k & (v & (c & s)))) =>
(forall (s0 :: [*]). (k : s0) :-> (e : s0)) -> st :-> st
failingWhenPresent forall (s0 :: [*]). (k : s0) :-> (e : s0)
mkErr ((k : v : Map k v : s) :-> (k : v : Map k v : s))
-> ((k : v : Map k v : s) :-> (Map k v : s))
-> (k : v : Map k v : s) :-> (Map k v : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k : v : Map k v : s) :-> (Map k v : s)
forall (map :: * -> * -> *) k v (s :: [*]).
(MapInstrs map, NiceComparable k) =>
(k : v : map k v : s) :-> (map k v : s)
mapInsert
instance MapInstrs BigMap where
  mapUpdate :: (k : Maybe v : BigMap k v : s) :-> (BigMap k v : s)
mapUpdate = (k : Maybe v : BigMap k v : s) :-> (BigMap k v : s)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c & (UpdOpParamsHs c & (c & s))) :-> (c & s)
update
  mapInsertNew :: (forall (s0 :: [*]). (k : s0) :-> (e : s0))
-> (k : v : BigMap k v : s) :-> (BigMap k v : s)
mapInsertNew mkErr :: forall (s0 :: [*]). (k : s0) :-> (e : s0)
mkErr = (forall (s0 :: [*]). (k : s0) :-> (e : s0))
-> (k : v : BigMap k v : s) :-> (k : v : BigMap k v : s)
forall c k (s :: [*]) v (st :: [*]) e.
(MemOpHs c, k ~ MemOpKeyHs c, KnownValue e,
 st ~ (k & (v & (c & s)))) =>
(forall (s0 :: [*]). (k : s0) :-> (e : s0)) -> st :-> st
failingWhenPresent forall (s0 :: [*]). (k : s0) :-> (e : s0)
mkErr ((k : v : BigMap k v : s) :-> (k : v : BigMap k v : s))
-> ((k : v : BigMap k v : s) :-> (BigMap k v : s))
-> (k : v : BigMap k v : s) :-> (BigMap k v : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k : v : BigMap k v : s) :-> (BigMap k v : s)
forall (map :: * -> * -> *) k v (s :: [*]).
(MapInstrs map, NiceComparable k) =>
(k : v : map k v : s) :-> (map k v : s)
mapInsert

-- | Insert given element into set.
--
-- This is a separate function from 'updateMap' because stacks they operate with
-- differ in length.
setInsert :: NiceComparable e => e & Set e & s :-> Set e & s
setInsert :: (e & (Set e & s)) :-> (Set e & s)
setInsert = ((Set e & s) :-> (Bool & (Set e & s)))
-> (e & (Set e & s)) :-> (e & (Bool & (Set e & s)))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (Bool -> (Set e & s) :-> (Bool & (Set e & s))
forall t (s :: [*]). NiceConstant t => t -> s :-> (t & s)
push Bool
True) ((e & (Set e & s)) :-> (e & (Bool & (Set e & s))))
-> ((e & (Bool & (Set e & s))) :-> (Set e & s))
-> (e & (Set e & s)) :-> (Set e & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (e & (Bool & (Set e & s))) :-> (Set e & s)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c & (UpdOpParamsHs c & (c & s))) :-> (c & s)
update

-- | Insert given element into set, ensuring that it does not overwrite
-- any existing entry.
--
-- As first argument accepts container name.
setInsertNew
  :: (NiceComparable e, KnownValue err)
  => (forall s0. e : s0 :-> err : s0)
  -> e & Set e & s :-> Set e & s
setInsertNew :: (forall (s0 :: [*]). (e : s0) :-> (err : s0))
-> (e & (Set e & s)) :-> (Set e & s)
setInsertNew desc :: forall (s0 :: [*]). (e : s0) :-> (err : s0)
desc = ((Set e & s) :-> (Bool & (Set e & s)))
-> (e & (Set e & s)) :-> (e & (Bool & (Set e & s)))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (Bool -> (Set e & s) :-> (Bool & (Set e & s))
forall t (s :: [*]). NiceConstant t => t -> s :-> (t & s)
push Bool
True) ((e & (Set e & s)) :-> (e & (Bool & (Set e & s))))
-> ((e & (Bool & (Set e & s))) :-> (e & (Bool & (Set e & s))))
-> (e & (Set e & s)) :-> (e & (Bool & (Set e & s)))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (forall (s0 :: [*]). (e : s0) :-> (err : s0))
-> (e & (Bool & (Set e & s))) :-> (e & (Bool & (Set e & s)))
forall c k (s :: [*]) v (st :: [*]) e.
(MemOpHs c, k ~ MemOpKeyHs c, KnownValue e,
 st ~ (k & (v & (c & s)))) =>
(forall (s0 :: [*]). (k : s0) :-> (e : s0)) -> st :-> st
failingWhenPresent forall (s0 :: [*]). (e : s0) :-> (err : s0)
desc ((e & (Set e & s)) :-> (e & (Bool & (Set e & s))))
-> ((e & (Bool & (Set e & s))) :-> (Set e & s))
-> (e & (Set e & s)) :-> (Set e & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (e & (Bool & (Set e & s))) :-> (Set e & s)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c & (UpdOpParamsHs c & (c & s))) :-> (c & s)
update

-- | Delete given element from the set.
setDelete :: NiceComparable e => e & Set e & s :-> Set e & s
setDelete :: (e & (Set e & s)) :-> (Set e & s)
setDelete = ((Set e & s) :-> (Bool & (Set e & s)))
-> (e & (Set e & s)) :-> (e & (Bool & (Set e & s)))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (Bool -> (Set e & s) :-> (Bool & (Set e & s))
forall t (s :: [*]). NiceConstant t => t -> s :-> (t & s)
push Bool
False) ((e & (Set e & s)) :-> (e & (Bool & (Set e & s))))
-> ((e & (Bool & (Set e & s))) :-> (Set e & s))
-> (e & (Set e & s)) :-> (Set e & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (e & (Bool & (Set e & s))) :-> (Set e & s)
forall c (s :: [*]).
UpdOpHs c =>
(UpdOpKeyHs c & (UpdOpParamsHs c & (c & s))) :-> (c & s)
update

-- | Kind-agnostic constraint for replaceN
type ReplaceNConstraint' kind (n :: Peano)
  (s :: [kind]) (a :: kind) (mid :: [kind]) (tail :: [kind]) =
  ( tail ~ Drop ('S n) s
  , ConstraintDIPN' kind ('S n) (a ': s) mid (a ': tail) tail
  , ConstraintDUG' kind n mid s a
  )

-- | Constraint for replaceN that combines kind-agnostic constraint for
-- Lorentz (Haskell) types and for our typed Michelson.
type ConstraintReplaceNLorentz (n :: Peano)
  (s :: [Kind.Type]) (a :: Kind.Type)
  (mid :: [Kind.Type]) (tail :: [Kind.Type]) =
  ( ReplaceNConstraint' T n (ToTs s) (ToT a) (ToTs mid) (ToTs tail)
  , ReplaceNConstraint' Kind.Type n s a mid tail
  )

class ReplaceN (n :: Peano) (s :: [Kind.Type]) (a :: Kind.Type) mid tail where
  replaceNImpl :: a ': s :-> s

instance {-# OVERLAPPING #-} (s ~ (a ': xs)) => ReplaceN ('S 'Z) s a mid tail where
  replaceNImpl :: (a : s) :-> s
replaceNImpl = (a & (a : xs)) :-> (a & (a : xs))
forall a b (s :: [*]). (a & (b & s)) :-> (b & (a & s))
swap ((a & (a : xs)) :-> (a & (a : xs)))
-> ((a & (a : xs)) :-> (a : xs)) -> (a & (a : xs)) :-> (a : xs)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a & (a : xs)) :-> (a : xs)
forall a (s :: [*]). (a & s) :-> s
drop

instance {-# OVERLAPPABLE #-} (ConstraintReplaceNLorentz ('S n) s a mid tail) =>
  ReplaceN ('S ('S n)) s a mid tail where
  replaceNImpl :: (a : s) :-> s
replaceNImpl =
    -- 'stackType' helps GHC deduce types
    ((a : tail) :-> tail) -> (a : s) :-> (a : Drop ('S 'Z) mid)
forall (n :: Peano) (inp :: [*]) (out :: [*]) (s :: [*])
       (s' :: [*]).
ConstraintDIPNLorentz n inp out s s' =>
(s :-> s') -> inp :-> out
dipNPeano @('S ('S n)) ((a : tail) :-> (a : tail)
forall (s :: [*]). s :-> s
stackType @(a ': tail) ((a : tail) :-> (a : tail))
-> ((a : tail) :-> tail) -> (a : tail) :-> tail
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : tail) :-> tail
forall a (s :: [*]). (a & s) :-> s
drop) ((a : s) :-> (a : Drop ('S 'Z) mid))
-> ((a : Drop ('S 'Z) mid) :-> s) -> (a : s) :-> s
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz ('S n) inp out a =>
inp :-> out
forall (n :: Peano) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz n inp out a =>
inp :-> out
dugPeano @('S n)

-- | Replace nth element (0-indexed) with the one on the top of the stack.
-- For example, `replaceN @3` replaces the 3rd element with the 0th one.
-- `replaceN @0` is not a valid operation (and it is not implemented).
-- `replaceN @1` is equivalent to `swap # drop` (and is the only one implemented
-- like this).
-- In all other cases `replaceN @n` will drop the nth element (`dipN @n drop`)
-- and then put the 0th one in its place (`dug @(n-1)`).
replaceN :: forall (n :: GHC.Nat) a (s :: [Kind.Type]) (s1 :: [Kind.Type]) (tail :: [Kind.Type]).
  ( ConstraintReplaceNLorentz (ToPeano (n - 1)) s a s1 tail
  , ReplaceN (ToPeano n) s a s1 tail
  )
  => a ': s :-> s
replaceN :: (a : s) :-> s
replaceN = ReplaceN (ToPeano n) s a s1 tail => (a : s) :-> s
forall k k (n :: Peano) (s :: [*]) a (mid :: k) (tail :: k).
ReplaceN n s a mid tail =>
(a : s) :-> s
replaceNImpl @(ToPeano n) @s @a @s1 @tail
  where
    _example ::
      '[ Integer, (), Integer, Bool ] :->
      '[ (), Integer, Bool ]
    _example :: '[Integer, (), Integer, Bool] :-> '[(), Integer, Bool]
_example = forall a (s :: [*]) (s1 :: [*]) (tail :: [*]).
(ConstraintReplaceNLorentz (ToPeano (2 - 1)) s a s1 tail,
 ReplaceN (ToPeano 2) s a s1 tail) =>
(a : s) :-> s
forall (n :: Nat) a (s :: [*]) (s1 :: [*]) (tail :: [*]).
(ConstraintReplaceNLorentz (ToPeano (n - 1)) s a s1 tail,
 ReplaceN (ToPeano n) s a s1 tail) =>
(a : s) :-> s
replaceN @2

-- | Kind-agnostic constraint for updateN
type UpdateNConstraint' kind (n :: Peano)
  (s :: [kind]) (a :: kind) (b :: kind) (mid :: [kind]) (tail :: [kind]) =
  ( tail ~ Drop ('S n) s
  , ConstraintDUG' kind n (a ': s) mid a
  , ConstraintDIPN' kind n mid s (a ': b ': tail) (b ': tail)
  )

-- | Constraint for updateN that combines kind-agnostic constraint for
-- Lorentz (Haskell) types and for our typed Michelson.
type ConstraintUpdateNLorentz (n :: Peano)
  (s :: [Kind.Type]) (a :: Kind.Type) (b :: Kind.Type)
  (mid :: [Kind.Type]) (tail :: [Kind.Type]) =
  ( UpdateNConstraint' T n (ToTs s) (ToT a) (ToT b) (ToTs mid) (ToTs tail)
  , UpdateNConstraint' Kind.Type n s a b mid tail
  )

class UpdateN (n :: Peano) (s :: [Kind.Type]) (a :: Kind.Type) (b :: Kind.Type) mid tail where
  updateNImpl
    :: '[a, b] :-> '[b]
    -> a ': s :-> s

instance {-# OVERLAPPING #-} (s ~ (b ': tail)) => UpdateN ('S 'Z) s a b mid tail where
  updateNImpl :: ('[a, b] :-> '[b]) -> (a : s) :-> s
updateNImpl instr :: '[a, b] :-> '[b]
instr = ('[a, b] :-> '[b]) -> ('[a, b] ++ tail) :-> ('[b] ++ tail)
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed '[a, b] :-> '[b]
instr

instance {-# OVERLAPPING #-} (s ~ (x ': b ': tail)) => UpdateN ('S ('S 'Z)) s a b mid tail where
  updateNImpl :: ('[a, b] :-> '[b]) -> (a : s) :-> s
updateNImpl instr :: '[a, b] :-> '[b]
instr = (a & (x : b : tail)) :-> (x & (a & (b : tail)))
forall a b (s :: [*]). (a & (b & s)) :-> (b & (a & s))
swap ((a & (x : b : tail)) :-> (x & (a & (b : tail))))
-> ((x & (a & (b : tail))) :-> (x : b : tail))
-> (a & (x : b : tail)) :-> (x : b : tail)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a & (b : tail)) :-> (b : tail))
-> (x & (a & (b : tail))) :-> (x : b : tail)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (('[a, b] :-> '[b]) -> ('[a, b] ++ tail) :-> ('[b] ++ tail)
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed '[a, b] :-> '[b]
instr)

instance {-# OVERLAPPABLE #-} (ConstraintUpdateNLorentz ('S ('S n)) s a b mid tail) =>
  UpdateN ('S ('S ('S n))) s a b mid tail where
  updateNImpl :: ('[a, b] :-> '[b]) -> (a : s) :-> s
updateNImpl instr :: '[a, b] :-> '[b]
instr =
    -- 'stackType' helps GHC deduce types
    forall (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz ('S ('S n)) inp out a =>
inp :-> out
forall (n :: Peano) (inp :: [*]) (out :: [*]) a.
ConstraintDUGLorentz n inp out a =>
inp :-> out
dugPeano @('S ('S n)) ((a : s) :-> mid) -> (mid :-> s) -> (a : s) :-> s
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a : b : tail) :-> (b : tail)) -> mid :-> s
forall (n :: Peano) (inp :: [*]) (out :: [*]) (s :: [*])
       (s' :: [*]).
ConstraintDIPNLorentz n inp out s s' =>
(s :-> s') -> inp :-> out
dipNPeano @('S ('S n)) (('[a, b] :-> '[b]) -> ('[a, b] ++ tail) :-> ('[b] ++ tail)
forall (s :: [*]) (i :: [*]) (o :: [*]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed '[a, b] :-> '[b]
instr ((a : b : tail) :-> (b : tail))
-> ((b : tail) :-> (b : tail)) -> (a : b : tail) :-> (b : tail)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b : tail) :-> (b : tail)
forall (s :: [*]). s :-> s
stackType @(b ': tail))

-- | Replaces the nth element (0-indexed) with the result of the given "updating"
-- instruction (binary with the return type equal to the second argument) applied
-- to the 0th element and the nth element itself.
-- For example, `updateN @3 cons` replaces the 3rd element with the result of
-- `cons` applied to the topmost element and the 3rd one.
-- `updateN @0 instr` is not a valid operation (and it is not implemented).
-- `updateN @1 instr` is equivalent to `instr` (and so is implemented).
-- `updateN @2 instr` is equivalent to `swap # dip instr` (and so is implemented).
-- In all other cases `updateN @n instr` will put the topmost element right above
-- the nth one (`dug @(n-1)`) and then apply the function to them in place
-- (`dipN @(n-1) instr`).
updateN :: forall (n :: GHC.Nat) a b (s :: [Kind.Type]) (mid :: [Kind.Type]) (tail :: [Kind.Type]).
  ( ConstraintUpdateNLorentz (ToPeano (n - 1)) s a b mid tail
  , UpdateN (ToPeano n) s a b mid tail
  )
  => '[a, b] :-> '[b]
  -> a ': s :-> s
updateN :: ('[a, b] :-> '[b]) -> (a : s) :-> s
updateN instr :: '[a, b] :-> '[b]
instr = ('[a, b] :-> '[b]) -> (a : s) :-> s
forall k k (n :: Peano) (s :: [*]) a b (mid :: k) (tail :: k).
UpdateN n s a b mid tail =>
('[a, b] :-> '[b]) -> (a : s) :-> s
updateNImpl @(ToPeano n) @s @a @b @mid @tail '[a, b] :-> '[b]
instr
  where
    _example ::
      '[ Integer, (), (), [Integer], Bool ] :->
      '[ (), (), [Integer], Bool ]
    _example :: '[Integer, (), (), [Integer], Bool] :-> '[(), (), [Integer], Bool]
_example = ('[Integer, [Integer]] :-> '[[Integer]])
-> '[Integer, (), (), [Integer], Bool]
   :-> '[(), (), [Integer], Bool]
forall (n :: Nat) a b (s :: [*]) (mid :: [*]) (tail :: [*]).
(ConstraintUpdateNLorentz (ToPeano (n - 1)) s a b mid tail,
 UpdateN (ToPeano n) s a b mid tail) =>
('[a, b] :-> '[b]) -> (a : s) :-> s
updateN @3 '[Integer, [Integer]] :-> '[[Integer]]
forall a (s :: [*]). (a & (List a & s)) :-> (List a & s)
cons

----------------------------------------------------------------------------
-- Additional Morley macros
----------------------------------------------------------------------------

-- | @view@ type synonym as described in A1.
data View (a :: Kind.Type) (r :: Kind.Type) = View
  { View a r -> a
viewParam :: a
  , View a r -> ContractRef r
viewCallbackTo :: ContractRef r
  } deriving stock (View a r -> View a r -> Bool
(View a r -> View a r -> Bool)
-> (View a r -> View a r -> Bool) -> Eq (View a r)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a r. Eq a => View a r -> View a r -> Bool
/= :: View a r -> View a r -> Bool
$c/= :: forall a r. Eq a => View a r -> View a r -> Bool
== :: View a r -> View a r -> Bool
$c== :: forall a r. Eq a => View a r -> View a r -> Bool
Eq, Int -> View a r -> ShowS
[View a r] -> ShowS
View a r -> String
(Int -> View a r -> ShowS)
-> (View a r -> String) -> ([View a r] -> ShowS) -> Show (View a r)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a r. Show a => Int -> View a r -> ShowS
forall a r. Show a => [View a r] -> ShowS
forall a r. Show a => View a r -> String
showList :: [View a r] -> ShowS
$cshowList :: forall a r. Show a => [View a r] -> ShowS
show :: View a r -> String
$cshow :: forall a r. Show a => View a r -> String
showsPrec :: Int -> View a r -> ShowS
$cshowsPrec :: forall a r. Show a => Int -> View a r -> ShowS
Show, (forall x. View a r -> Rep (View a r) x)
-> (forall x. Rep (View a r) x -> View a r) -> Generic (View a r)
forall x. Rep (View a r) x -> View a r
forall x. View a r -> Rep (View a r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a r x. Rep (View a r) x -> View a r
forall a r x. View a r -> Rep (View a r) x
$cto :: forall a r x. Rep (View a r) x -> View a r
$cfrom :: forall a r x. View a r -> Rep (View a r) x
Generic)
    deriving anyclass (AnnOptions
FollowEntrypointFlag -> Notes (ToT (View a r))
(FollowEntrypointFlag -> Notes (ToT (View a r)))
-> AnnOptions -> HasAnnotation (View a r)
forall a.
(FollowEntrypointFlag -> Notes (ToT a))
-> AnnOptions -> HasAnnotation a
forall a r. (HasAnnotation a, HasAnnotation r) => AnnOptions
forall a r.
(HasAnnotation a, HasAnnotation r) =>
FollowEntrypointFlag -> Notes (ToT (View a r))
annOptions :: AnnOptions
$cannOptions :: forall a r. (HasAnnotation a, HasAnnotation r) => AnnOptions
getAnnotation :: FollowEntrypointFlag -> Notes (ToT (View a r))
$cgetAnnotation :: forall a r.
(HasAnnotation a, HasAnnotation r) =>
FollowEntrypointFlag -> Notes (ToT (View a r))
HasAnnotation)

deriving anyclass instance (WellTypedIsoValue r, WellTypedIsoValue a) => IsoValue (View a r)

instance (CanCastTo a1 a2, CanCastTo r1 r2) => CanCastTo (View a1 r1) (View a2 r2)

instance Each [Typeable, TypeHasDoc] [a, r] => TypeHasDoc (View a r) where
  typeDocMdDescription :: Markdown
typeDocMdDescription =
    "`View a r` accepts an argument of type `a` and callback contract \
    \which accepts `r` and returns result via calling that contract.\n\
    \Read more in [A1 conventions document](https://gitlab.com/tzip/tzip/-/blob/c42e3f0f5e73669e84e615d69bee73281572eb0a/proposals/tzip-4/tzip-4.md#view-entrypoints)."
  typeDocMdReference :: Proxy (View a r) -> WithinParens -> Markdown
typeDocMdReference = Proxy (View a r) -> WithinParens -> Markdown
forall (t :: * -> * -> *) r a b.
(r ~ t a b, Typeable t, Each '[TypeHasDoc] '[r, a, b],
 IsHomomorphic t) =>
Proxy r -> WithinParens -> Markdown
poly2TypeDocMdReference
  typeDocDependencies :: Proxy (View a r) -> [SomeDocDefinitionItem]
typeDocDependencies p :: Proxy (View a r)
p =
    Proxy (View a r) -> [SomeDocDefinitionItem]
forall a.
(Generic a, GTypeHasDoc (Rep a)) =>
Proxy a -> [SomeDocDefinitionItem]
genericTypeDocDependencies Proxy (View a r)
p [SomeDocDefinitionItem]
-> [SomeDocDefinitionItem] -> [SomeDocDefinitionItem]
forall a. Semigroup a => a -> a -> a
<>
    [TypeHasDoc () => SomeDocDefinitionItem
forall t. TypeHasDoc t => SomeDocDefinitionItem
dTypeDep @(), TypeHasDoc Integer => SomeDocDefinitionItem
forall t. TypeHasDoc t => SomeDocDefinitionItem
dTypeDep @Integer]
  typeDocHaskellRep :: TypeDocHaskellRep (View a r)
typeDocHaskellRep =
    TypeDocHaskellRep (View a r) -> TypeDocHaskellRep (View a r)
forall a. TypeDocHaskellRep a -> TypeDocHaskellRep a
haskellRepNoFields (TypeDocHaskellRep (View a r) -> TypeDocHaskellRep (View a r))
-> TypeDocHaskellRep (View a r) -> TypeDocHaskellRep (View a r)
forall a b. (a -> b) -> a -> b
$ forall b.
(Typeable (View () Integer), GenericIsoValue (View () Integer),
 GTypeHasDoc (Rep (View () Integer)),
 HaveCommonTypeCtor b (View () Integer)) =>
TypeDocHaskellRep b
forall a b.
(Typeable a, GenericIsoValue a, GTypeHasDoc (Rep a),
 HaveCommonTypeCtor b a) =>
TypeDocHaskellRep b
concreteTypeDocHaskellRep @(View () Integer)
  typeDocMichelsonRep :: TypeDocMichelsonRep (View a r)
typeDocMichelsonRep =
    forall b.
(Typeable (View () Integer), SingI (ToT (View () Integer)),
 HaveCommonTypeCtor b (View () Integer)) =>
TypeDocMichelsonRep b
forall k a (b :: k).
(Typeable a, SingI (ToT a), HaveCommonTypeCtor b a) =>
TypeDocMichelsonRep b
concreteTypeDocMichelsonRep @(View () Integer)

instance {-# OVERLAPPABLE #-} (Buildable a, WellTypedIsoValue r) => Buildable (View a r) where
  build :: View a r -> Markdown
build = (a -> Markdown) -> View a r -> Markdown
forall r a.
WellTypedIsoValue r =>
(a -> Markdown) -> View a r -> Markdown
buildView a -> Markdown
forall p. Buildable p => p -> Markdown
build

instance {-# OVERLAPPING  #-} (WellTypedIsoValue r) => Buildable (View () r) where
  build :: View () r -> Markdown
build = (() -> Markdown) -> View () r -> Markdown
forall r a.
WellTypedIsoValue r =>
(a -> Markdown) -> View a r -> Markdown
buildView ((() -> Markdown) -> View () r -> Markdown)
-> (() -> Markdown) -> View () r -> Markdown
forall a b. (a -> b) -> a -> b
$ Markdown -> () -> Markdown
forall a b. a -> b -> a
const "()"

buildViewTuple :: (WellTypedIsoValue r, TupleF a) => View a r -> Builder
buildViewTuple :: View a r -> Markdown
buildViewTuple = (a -> Markdown) -> View a r -> Markdown
forall r a.
WellTypedIsoValue r =>
(a -> Markdown) -> View a r -> Markdown
buildView a -> Markdown
forall a. TupleF a => a -> Markdown
tupleF

buildView :: (WellTypedIsoValue r) => (a -> Builder) -> View a r -> Builder
buildView :: (a -> Markdown) -> View a r -> Markdown
buildView bfp :: a -> Markdown
bfp (View {..}) =
  "(View param: " Markdown -> Markdown -> Markdown
forall b. FromBuilder b => Markdown -> Markdown -> b
+| a -> Markdown
bfp a
viewParam Markdown -> Markdown -> Markdown
forall a b. (Buildable a, FromBuilder b) => a -> Markdown -> b
|+ " callbackTo: " Markdown -> Markdown -> Markdown
forall b. FromBuilder b => Markdown -> Markdown -> b
+| ContractRef r
viewCallbackToContractRef r -> Markdown -> Markdown
forall a b. (Buildable a, FromBuilder b) => a -> Markdown -> b
|+ ")"

-- | Polymorphic version of 'View' constructor.
mkView :: ToContractRef r contract => a -> contract -> View a r
mkView :: a -> contract -> View a r
mkView a :: a
a c :: contract
c = a -> ContractRef r -> View a r
forall a r. a -> ContractRef r -> View a r
View a
a (contract -> ContractRef r
forall cp contract.
(ToContractRef cp contract, HasCallStack) =>
contract -> ContractRef cp
toContractRef contract
c)

-- | Wrap internal representation of view into 'View' itself.
--
-- 'View' is part of public standard and should not change often.
wrapView :: (a, ContractRef r) : s :-> View a r : s
wrapView :: ((a, ContractRef r) : s) :-> (View a r : s)
wrapView = ((a, ContractRef r) : s) :-> (View a r : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a & s) :-> (b & s)
forcedCoerce_

-- | Unwrap 'View' into its internal representation.
--
-- 'View' is part of public standard and should not change often.
unwrapView :: View a r : s :-> (a, ContractRef r) : s
unwrapView :: (View a r : s) :-> ((a, ContractRef r) : s)
unwrapView = (View a r : s) :-> ((a, ContractRef r) : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a & s) :-> (b & s)
forcedCoerce_

view_ ::
     (NiceParameter r)
  => (forall s0. a & storage & s0 :-> r : s0)
  -> View a r & storage & s :-> (List Operation, storage) & s
view_ :: (forall (s0 :: [*]). (a & (storage & s0)) :-> (r : s0))
-> (View a r & (storage & s)) :-> ((List Operation, storage) & s)
view_ code :: forall (s0 :: [*]). (a & (storage & s0)) :-> (r : s0)
code =
  (View a r & (storage & s)) :-> ((a, ContractRef r) : (storage & s))
forall a r (s :: [*]). (View a r : s) :-> ((a, ContractRef r) : s)
unwrapView ((View a r & (storage & s))
 :-> ((a, ContractRef r) : (storage & s)))
-> (((a, ContractRef r) : (storage & s))
    :-> (a & (ContractRef r & (storage & s))))
-> (View a r & (storage & s))
   :-> (a & (ContractRef r & (storage & s)))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  ((a, ContractRef r) : (storage & s))
:-> (a & (ContractRef r & (storage & s)))
forall a b (s :: [*]). ((a, b) & s) :-> (a & (b & s))
unpair ((View a r & (storage & s))
 :-> (a & (ContractRef r & (storage & s))))
-> ((a & (ContractRef r & (storage & s)))
    :-> (a & (storage : (ContractRef r & (storage & s)))))
-> (View a r & (storage & s))
   :-> (a & (storage : (ContractRef r & (storage & s))))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((ContractRef r & (storage & s))
 :-> (storage : (ContractRef r & (storage & s))))
-> (a & (ContractRef r & (storage & s)))
   :-> (a & (storage : (ContractRef r & (storage & s))))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (forall a (s :: [*]) (s1 :: [*]) (tail :: [*]).
(ConstraintDuupXLorentz (ToPeano (2 - 1)) s a s1 tail,
 DuupX (ToPeano 2) s a s1 tail) =>
s :-> (a : s)
forall (n :: Nat) a (s :: [*]) (s1 :: [*]) (tail :: [*]).
(ConstraintDuupXLorentz (ToPeano (n - 1)) s a s1 tail,
 DuupX (ToPeano n) s a s1 tail) =>
s :-> (a : s)
duupX @2) ((View a r & (storage & s))
 :-> (a & (storage : (ContractRef r & (storage & s)))))
-> ((a & (storage : (ContractRef r & (storage & s))))
    :-> (r : (ContractRef r & (storage & s))))
-> (View a r & (storage & s))
   :-> (r : (ContractRef r & (storage & s)))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a & (storage : (ContractRef r & (storage & s))))
:-> (r : (ContractRef r & (storage & s)))
forall (s0 :: [*]). (a & (storage & s0)) :-> (r : s0)
code ((View a r & (storage & s))
 :-> (r : (ContractRef r & (storage & s))))
-> ((r : (ContractRef r & (storage & s)))
    :-> (r & (Mutez & (ContractRef r & (storage & s)))))
-> (View a r & (storage & s))
   :-> (r & (Mutez & (ContractRef r & (storage & s))))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((ContractRef r & (storage & s))
 :-> (Mutez & (ContractRef r & (storage & s))))
-> (r : (ContractRef r & (storage & s)))
   :-> (r & (Mutez & (ContractRef r & (storage & s))))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (ContractRef r & (storage & s))
:-> (Mutez & (ContractRef r & (storage & s)))
forall (s :: [*]). s :-> (Mutez & s)
amount ((View a r & (storage & s))
 :-> (r & (Mutez & (ContractRef r & (storage & s)))))
-> ((r & (Mutez & (ContractRef r & (storage & s))))
    :-> (Operation & (storage & s)))
-> (View a r & (storage & s)) :-> (Operation & (storage & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  (r & (Mutez & (ContractRef r & (storage & s))))
:-> (Operation & (storage & s))
forall p (s :: [*]).
NiceParameter p =>
(p & (Mutez & (ContractRef p & s))) :-> (Operation & s)
transferTokens ((View a r & (storage & s)) :-> (Operation & (storage & s)))
-> ((Operation & (storage & s))
    :-> (List Operation & (Operation & (storage & s))))
-> (View a r & (storage & s))
   :-> (List Operation & (Operation & (storage & s)))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Operation & (storage & s))
:-> (List Operation & (Operation & (storage & s)))
forall p (s :: [*]). KnownValue p => s :-> (List p & s)
nil ((View a r & (storage & s))
 :-> (List Operation & (Operation & (storage & s))))
-> ((List Operation & (Operation & (storage & s)))
    :-> (Operation & (List Operation & (storage & s))))
-> (View a r & (storage & s))
   :-> (Operation & (List Operation & (storage & s)))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (List Operation & (Operation & (storage & s)))
:-> (Operation & (List Operation & (storage & s)))
forall a b (s :: [*]). (a & (b & s)) :-> (b & (a & s))
swap ((View a r & (storage & s))
 :-> (Operation & (List Operation & (storage & s))))
-> ((Operation & (List Operation & (storage & s)))
    :-> (List Operation & (storage & s)))
-> (View a r & (storage & s)) :-> (List Operation & (storage & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Operation & (List Operation & (storage & s)))
:-> (List Operation & (storage & s))
forall a (s :: [*]). (a & (List a & s)) :-> (List a & s)
cons ((View a r & (storage & s)) :-> (List Operation & (storage & s)))
-> ((List Operation & (storage & s))
    :-> ((List Operation, storage) & s))
-> (View a r & (storage & s)) :-> ((List Operation, storage) & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (List Operation & (storage & s))
:-> ((List Operation, storage) & s)
forall a b (s :: [*]). (a & (b & s)) :-> ((a, b) & s)
pair

-- | @void@ type synonym as described in A1.
data Void_ (a :: Kind.Type) (b :: Kind.Type) = Void_
  { Void_ a b -> a
voidParam :: a
    -- ^ Entry point argument.
  , Void_ a b -> Lambda b b
voidResProxy :: Lambda b b
    -- ^ Type of result reported via 'failWith'.
  } deriving stock ((forall x. Void_ a b -> Rep (Void_ a b) x)
-> (forall x. Rep (Void_ a b) x -> Void_ a b)
-> Generic (Void_ a b)
forall x. Rep (Void_ a b) x -> Void_ a b
forall x. Void_ a b -> Rep (Void_ a b) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a b x. Rep (Void_ a b) x -> Void_ a b
forall a b x. Void_ a b -> Rep (Void_ a b) x
$cto :: forall a b x. Rep (Void_ a b) x -> Void_ a b
$cfrom :: forall a b x. Void_ a b -> Rep (Void_ a b) x
Generic, Int -> Void_ a b -> ShowS
[Void_ a b] -> ShowS
Void_ a b -> String
(Int -> Void_ a b -> ShowS)
-> (Void_ a b -> String)
-> ([Void_ a b] -> ShowS)
-> Show (Void_ a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. Show a => Int -> Void_ a b -> ShowS
forall a b. Show a => [Void_ a b] -> ShowS
forall a b. Show a => Void_ a b -> String
showList :: [Void_ a b] -> ShowS
$cshowList :: forall a b. Show a => [Void_ a b] -> ShowS
show :: Void_ a b -> String
$cshow :: forall a b. Show a => Void_ a b -> String
showsPrec :: Int -> Void_ a b -> ShowS
$cshowsPrec :: forall a b. Show a => Int -> Void_ a b -> ShowS
Show)
    deriving anyclass (AnnOptions
FollowEntrypointFlag -> Notes (ToT (Void_ a b))
(FollowEntrypointFlag -> Notes (ToT (Void_ a b)))
-> AnnOptions -> HasAnnotation (Void_ a b)
forall a.
(FollowEntrypointFlag -> Notes (ToT a))
-> AnnOptions -> HasAnnotation a
forall a r. (HasAnnotation a, HasAnnotation r) => AnnOptions
forall a b.
(HasAnnotation a, HasAnnotation b) =>
FollowEntrypointFlag -> Notes (ToT (Void_ a b))
annOptions :: AnnOptions
$cannOptions :: forall a r. (HasAnnotation a, HasAnnotation r) => AnnOptions
getAnnotation :: FollowEntrypointFlag -> Notes (ToT (Void_ a b))
$cgetAnnotation :: forall a b.
(HasAnnotation a, HasAnnotation b) =>
FollowEntrypointFlag -> Notes (ToT (Void_ a b))
HasAnnotation)

deriving anyclass instance (WellTypedIsoValue r, WellTypedIsoValue a) => IsoValue (Void_ a r)

instance (CanCastTo a1 a2, CanCastTo r1 r2) => CanCastTo (Void_ a1 r1) (Void_ a2 r2)

instance Each [Typeable, TypeHasDoc] [a, r] => TypeHasDoc (Void_ a r) where
  typeDocName :: Proxy (Void_ a r) -> Text
typeDocName _ = "Void"
  typeDocMdDescription :: Markdown
typeDocMdDescription =
    "`Void a r` accepts an argument of type `a` and returns a value of type \
    \`r` as contract error. To comply with general mechanism of contracts \
    \custom errors, void entrypoints execute `FAILWITH` instruction on \
    \`(\"VoidResult\", r)` value, where `r` is the actual return value of the \
    \entrypoint.\n\
    \Read more in [A1 conventions document](https://gitlab.com/tzip/tzip/-/blob/c42e3f0f5e73669e84e615d69bee73281572eb0a/proposals/tzip-4/tzip-4.md#void-entrypoints)."
  typeDocMdReference :: Proxy (Void_ a r) -> WithinParens -> Markdown
typeDocMdReference tp :: Proxy (Void_ a r)
tp =
    -- Avoiding trailing underscore
    (Text, DType) -> [DType] -> WithinParens -> Markdown
customTypeDocMdReference
      ("Void", Proxy (Void_ a r) -> DType
forall a. TypeHasDoc a => Proxy a -> DType
DType Proxy (Void_ a r)
tp)
      [ Proxy a -> DType
forall a. TypeHasDoc a => Proxy a -> DType
DType (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
      , Proxy r -> DType
forall a. TypeHasDoc a => Proxy a -> DType
DType (Proxy r
forall k (t :: k). Proxy t
Proxy @r)
      ]
  typeDocDependencies :: Proxy (Void_ a r) -> [SomeDocDefinitionItem]
typeDocDependencies p :: Proxy (Void_ a r)
p =
    Proxy (Void_ a r) -> [SomeDocDefinitionItem]
forall a.
(Generic a, GTypeHasDoc (Rep a)) =>
Proxy a -> [SomeDocDefinitionItem]
genericTypeDocDependencies Proxy (Void_ a r)
p [SomeDocDefinitionItem]
-> [SomeDocDefinitionItem] -> [SomeDocDefinitionItem]
forall a. Semigroup a => a -> a -> a
<>
    [TypeHasDoc () => SomeDocDefinitionItem
forall t. TypeHasDoc t => SomeDocDefinitionItem
dTypeDep @(), TypeHasDoc Integer => SomeDocDefinitionItem
forall t. TypeHasDoc t => SomeDocDefinitionItem
dTypeDep @Integer]
  typeDocHaskellRep :: TypeDocHaskellRep (Void_ a r)
typeDocHaskellRep p :: Proxy (Void_ a r)
p descr :: FieldDescriptionsV
descr = do
    (_, rhs :: ADTRep SomeTypeWithDoc
rhs) <- TypeDocHaskellRep (Void_ a r) -> TypeDocHaskellRep (Void_ a r)
forall a. TypeDocHaskellRep a -> TypeDocHaskellRep a
haskellRepNoFields (forall b.
(Typeable (Void_ () Integer), GenericIsoValue (Void_ () Integer),
 GTypeHasDoc (Rep (Void_ () Integer)),
 HaveCommonTypeCtor b (Void_ () Integer)) =>
TypeDocHaskellRep b
forall a b.
(Typeable a, GenericIsoValue a, GTypeHasDoc (Rep a),
 HaveCommonTypeCtor b a) =>
TypeDocHaskellRep b
concreteTypeDocHaskellRep @(Void_ () Integer)) Proxy (Void_ a r)
p FieldDescriptionsV
descr
    (Maybe DocTypeRepLHS, ADTRep SomeTypeWithDoc)
-> Maybe (Maybe DocTypeRepLHS, ADTRep SomeTypeWithDoc)
forall (m :: * -> *) a. Monad m => a -> m a
return (DocTypeRepLHS -> Maybe DocTypeRepLHS
forall a. a -> Maybe a
Just "Void () Integer", ADTRep SomeTypeWithDoc
rhs)
  typeDocMichelsonRep :: TypeDocMichelsonRep (Void_ a r)
typeDocMichelsonRep p :: Proxy (Void_ a r)
p =
    let (_, rhs :: T
rhs) = TypeDocMichelsonRep (Void_ a r)
forall k a (b :: k).
(Typeable a, SingI (ToT a), HaveCommonTypeCtor b a) =>
TypeDocMichelsonRep b
concreteTypeDocMichelsonRep @(Void_ () Integer) Proxy (Void_ a r)
p
    in (DocTypeRepLHS -> Maybe DocTypeRepLHS
forall a. a -> Maybe a
Just "Void () Integer", T
rhs)

instance Buildable a => Buildable (Void_ a b) where
  build :: Void_ a b -> Markdown
build Void_ {..} = "(Void param: " Markdown -> Markdown -> Markdown
forall b. FromBuilder b => Markdown -> Markdown -> b
+| a
voidParam a -> Markdown -> Markdown
forall a b. (Buildable a, FromBuilder b) => a -> Markdown -> b
|+ ")"

-- | Newtype over void result type used in tests to
-- distinguish successful void result from other errors.
--
-- Usage example:
-- lExpectFailWith (== VoidResult roleMaster)`
--
-- This error is special - it can contain arguments of different types
-- depending on entrypoint which raises it.
newtype VoidResult r = VoidResult { VoidResult r -> r
unVoidResult :: r }
  deriving stock ((forall x. VoidResult r -> Rep (VoidResult r) x)
-> (forall x. Rep (VoidResult r) x -> VoidResult r)
-> Generic (VoidResult r)
forall x. Rep (VoidResult r) x -> VoidResult r
forall x. VoidResult r -> Rep (VoidResult r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall r x. Rep (VoidResult r) x -> VoidResult r
forall r x. VoidResult r -> Rep (VoidResult r) x
$cto :: forall r x. Rep (VoidResult r) x -> VoidResult r
$cfrom :: forall r x. VoidResult r -> Rep (VoidResult r) x
Generic)
  deriving newtype (VoidResult r -> VoidResult r -> Bool
(VoidResult r -> VoidResult r -> Bool)
-> (VoidResult r -> VoidResult r -> Bool) -> Eq (VoidResult r)
forall r. Eq r => VoidResult r -> VoidResult r -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: VoidResult r -> VoidResult r -> Bool
$c/= :: forall r. Eq r => VoidResult r -> VoidResult r -> Bool
== :: VoidResult r -> VoidResult r -> Bool
$c== :: forall r. Eq r => VoidResult r -> VoidResult r -> Bool
Eq)

voidResultTag :: MText
voidResultTag :: MText
voidResultTag = [mt|VoidResult|]

type VoidResultRep r = (MText, r)

instance (TypeHasDoc r, IsError (VoidResult r)) => TypeHasDoc (VoidResult r) where
  typeDocMdDescription :: Markdown
typeDocMdDescription = IsError (VoidResult r) => Markdown
forall e. IsError e => Markdown
typeDocMdDescriptionReferToError @(VoidResult r)
  typeDocMdReference :: Proxy (VoidResult r) -> WithinParens -> Markdown
typeDocMdReference = Proxy (VoidResult r) -> WithinParens -> Markdown
forall (t :: * -> *) r a.
(r ~ t a, Typeable t, Each '[TypeHasDoc] '[r, a],
 IsHomomorphic t) =>
Proxy r -> WithinParens -> Markdown
poly1TypeDocMdReference
  typeDocHaskellRep :: TypeDocHaskellRep (VoidResult r)
typeDocHaskellRep = forall b.
(Typeable (VoidResultRep Integer),
 GenericIsoValue (VoidResultRep Integer),
 GTypeHasDoc (Rep (VoidResultRep Integer))) =>
TypeDocHaskellRep b
forall a b.
(Typeable a, GenericIsoValue a, GTypeHasDoc (Rep a)) =>
TypeDocHaskellRep b
concreteTypeDocHaskellRepUnsafe @(VoidResultRep Integer)
  typeDocMichelsonRep :: TypeDocMichelsonRep (VoidResult r)
typeDocMichelsonRep = forall b.
(Typeable (VoidResultRep Integer),
 SingI (ToT (VoidResultRep Integer))) =>
TypeDocMichelsonRep b
forall k a (b :: k).
(Typeable a, SingI (ToT a)) =>
TypeDocMichelsonRep b
concreteTypeDocMichelsonRepUnsafe @(VoidResultRep Integer)

instance (Typeable r, NiceConstant r, ErrorHasDoc (VoidResult r)) =>
         IsError (VoidResult r) where
  errorToVal :: VoidResult r
-> (forall (t :: T). ErrorScope t => Value t -> r) -> r
errorToVal (VoidResult e :: r
e) cont :: forall (t :: T). ErrorScope t => Value t -> r
cont =
    (NiceConstant r :- ConstantScope (ToT r))
-> (ConstantScope (ToT r) => r) -> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (NiceConstant r :- ConstantScope (ToT r)
forall a. NiceConstant a :- ConstantScope (ToT a)
niceConstantEvi @r) ((ConstantScope (ToT r) => r) -> r)
-> (ConstantScope (ToT r) => r) -> r
forall a b. (a -> b) -> a -> b
$
    VoidResultRep r
-> (forall (t :: T). ErrorScope t => Value t -> r) -> r
forall e r.
(KnownError e, IsoValue e) =>
e -> (forall (t :: T). ErrorScope t => Value t -> r) -> r
isoErrorToVal @(VoidResultRep r) (MText
voidResultTag, r
e) forall (t :: T). ErrorScope t => Value t -> r
cont
  errorFromVal :: Value t -> Either Text (VoidResult r)
errorFromVal fullErr :: Value t
fullErr =
    Value t -> Either Text (VoidResultRep r)
forall (t :: T) e.
(Typeable t, Typeable (ToT e), IsoValue e) =>
Value t -> Either Text e
isoErrorFromVal Value t
fullErr Either Text (VoidResultRep r)
-> (VoidResultRep r -> Either Text (VoidResult r))
-> Either Text (VoidResult r)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \((tag :: MText
tag, e :: r
e) :: VoidResultRep r) ->
      if MText
tag MText -> MText -> Bool
forall a. Eq a => a -> a -> Bool
== MText
voidResultTag
      then VoidResult r -> Either Text (VoidResult r)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VoidResult r -> Either Text (VoidResult r))
-> VoidResult r -> Either Text (VoidResult r)
forall a b. (a -> b) -> a -> b
$ r -> VoidResult r
forall r. r -> VoidResult r
VoidResult r
e
      else Text -> Either Text (VoidResult r)
forall a b. a -> Either a b
Left (Text -> Either Text (VoidResult r))
-> Text -> Either Text (VoidResult r)
forall a b. (a -> b) -> a -> b
$ "Error mismatch, expected VoidResult, got " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> MText -> Text
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty MText
tag

instance TypeHasDoc r => ErrorHasDoc (VoidResult r) where
  errorDocName :: Text
errorDocName = "VoidResult"
  errorDocMdCause :: Markdown
errorDocMdCause =
    "Call to entrypoint has succeeded, reporting returned value as error.\n\
    \As Tezos contracts normally do not produce any output (not counting storage \
    \update), this is the simplest way to return something to the caller in \
    \read-only entrypoints."
  errorDocHaskellRep :: Markdown
errorDocHaskellRep =
    Markdown -> Markdown
mdTicked ("(\"" Markdown -> Markdown -> Markdown
forall a. Semigroup a => a -> a -> a
<> MText -> Markdown
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty MText
voidResultTag Markdown -> Markdown -> Markdown
forall a. Semigroup a => a -> a -> a
<> "\", " Markdown -> Markdown -> Markdown
forall a. Semigroup a => a -> a -> a
<> "<return value>" Markdown -> Markdown -> Markdown
forall a. Semigroup a => a -> a -> a
<> ")")
  errorDocDependencies :: [SomeDocDefinitionItem]
errorDocDependencies =
    [TypeHasDoc MText => SomeDocDefinitionItem
forall t. TypeHasDoc t => SomeDocDefinitionItem
dTypeDep @MText, TypeHasDoc r => SomeDocDefinitionItem
forall t. TypeHasDoc t => SomeDocDefinitionItem
dTypeDep @r]

instance
  ( WellTypedIsoValue (VoidResult r)
  , Lit.TypeError ('Lit.Text "No IsoValue instance for VoidResult " 'Lit.:<>: 'Lit.ShowType r)
  ) => IsoValue (VoidResult r) where
  type ToT (VoidResult r) =
    Lit.TypeError ('Lit.Text "No IsoValue instance for VoidResult " 'Lit.:<>: 'Lit.ShowType r)
  toVal :: VoidResult r -> Value (ToT (VoidResult r))
toVal = Text -> VoidResult r -> Value (TypeError ...)
forall a. HasCallStack => Text -> a
error "impossible"
  fromVal :: Value (ToT (VoidResult r)) -> VoidResult r
fromVal = Text -> Value (TypeError ...) -> VoidResult r
forall a. HasCallStack => Text -> a
error "impossible"

mkVoid :: forall b a. a -> Void_ a b
mkVoid :: a -> Void_ a b
mkVoid a :: a
a = a -> Lambda b b -> Void_ a b
forall a b. a -> Lambda b b -> Void_ a b
Void_ a
a Lambda b b
forall (s :: [*]). s :-> s
nop

void_
  :: forall a b s s' anything.
      (IsError (VoidResult b), KnownValue b)
  => a & s :-> b & s' -> Void_ a b & s :-> anything
void_ :: ((a & s) :-> (b & s')) -> (Void_ a b & s) :-> anything
void_ code :: (a & s) :-> (b & s')
code =
  DThrows -> (Void_ a b & s) :-> (Void_ a b & s)
forall di (s :: [*]). DocItem di => di -> s :-> s
doc (Proxy (VoidResult b) -> DThrows
forall e. ErrorHasDoc e => Proxy e -> DThrows
DThrows (Proxy (VoidResult b)
forall k (t :: k). Proxy t
Proxy @(VoidResult b))) ((Void_ a b & s) :-> (Void_ a b & s))
-> ((Void_ a b & s) :-> ((a, Lambda b b) & s))
-> (Void_ a b & s) :-> ((a, Lambda b b) & s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  forall (s :: [*]).
MichelsonCoercible (Void_ a b) (a, Lambda b b) =>
(Void_ a b & s) :-> ((a, Lambda b b) & s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a & s) :-> (b & s)
forcedCoerce_ @_ @(_, Lambda b b) ((Void_ a b & s) :-> ((a, Lambda b b) & s))
-> (((a, Lambda b b) & s) :-> (a & (Lambda b b & s)))
-> (Void_ a b & s) :-> (a & (Lambda b b & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  ((a, Lambda b b) & s) :-> (a & (Lambda b b & s))
forall a b (s :: [*]). ((a, b) & s) :-> (a & (b & s))
unpair ((Void_ a b & s) :-> (a & (Lambda b b & s)))
-> ((a & (Lambda b b & s)) :-> (Lambda b b & (a & s)))
-> (Void_ a b & s) :-> (Lambda b b & (a & s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a & (Lambda b b & s)) :-> (Lambda b b & (a & s))
forall a b (s :: [*]). (a & (b & s)) :-> (b & (a & s))
swap ((Void_ a b & s) :-> (Lambda b b & (a & s)))
-> ((Lambda b b & (a & s)) :-> (Lambda b b & (b & s')))
-> (Void_ a b & s) :-> (Lambda b b & (b & s'))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a & s) :-> (b & s'))
-> (Lambda b b & (a & s)) :-> (Lambda b b & (b & s'))
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (a & s) :-> (b & s')
code ((Void_ a b & s) :-> (Lambda b b & (b & s')))
-> ((Lambda b b & (b & s')) :-> (b & (Lambda b b & s')))
-> (Void_ a b & s) :-> (b & (Lambda b b & s'))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Lambda b b & (b & s')) :-> (b & (Lambda b b & s'))
forall a b (s :: [*]). (a & (b & s)) :-> (b & (a & s))
swap ((Void_ a b & s) :-> (b & (Lambda b b & s')))
-> ((b & (Lambda b b & s')) :-> (b & s'))
-> (Void_ a b & s) :-> (b & s')
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b & (Lambda b b & s')) :-> (b & s')
forall a b (s :: [*]). (a & (Lambda a b & s)) :-> (b & s)
exec ((Void_ a b & s) :-> (b & s'))
-> ((b & s') :-> (MText & (b & s')))
-> (Void_ a b & s) :-> (MText & (b & s'))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  MText -> (b & s') :-> (MText & (b & s'))
forall t (s :: [*]). NiceConstant t => t -> s :-> (t & s)
push MText
voidResultTag ((Void_ a b & s) :-> (MText & (b & s')))
-> ((MText & (b & s')) :-> ((MText, b) & s'))
-> (Void_ a b & s) :-> ((MText, b) & s')
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (MText & (b & s')) :-> ((MText, b) & s')
forall a b (s :: [*]). (a & (b & s)) :-> ((a, b) & s)
pair ((Void_ a b & s) :-> ((MText, b) & s'))
-> (((MText, b) & s') :-> anything) -> (Void_ a b & s) :-> anything
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall (s :: [*]) (t :: [*]).
KnownValue (MText, b) =>
((MText, b) & s) :-> t
forall a (s :: [*]) (t :: [*]). KnownValue a => (a & s) :-> t
failWith @(MText, b)

-- | Wrap internal representation of void into 'Void_' itself.
--
-- 'Void_' is part of public standard and should not change often.
wrapVoid :: (a, Lambda b b) : s :-> Void_ a b : s
wrapVoid :: ((a, Lambda b b) : s) :-> (Void_ a b : s)
wrapVoid = ((a, Lambda b b) : s) :-> (Void_ a b : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a & s) :-> (b & s)
forcedCoerce_

-- | Unwrap 'Void_' into its internal representation.
--
-- 'Void_' is part of public standard and should not change often.
unwrapVoid :: Void_ a b : s :-> (a, Lambda b b) : s
unwrapVoid :: (Void_ a b : s) :-> ((a, Lambda b b) : s)
unwrapVoid = (Void_ a b : s) :-> ((a, Lambda b b) : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a & s) :-> (b & s)
forcedCoerce_

addressToEpAddress :: Address : s :-> EpAddress : s
addressToEpAddress :: (Address : s) :-> (EpAddress : s)
addressToEpAddress = (Address : s) :-> (EpAddress : s)
forall a b (s :: [*]).
MichelsonCoercible a b =>
(a & s) :-> (b & s)
forcedCoerce_

-- | Push a value of @contract@ type.
--
-- Doing this via 'push' instruction is not possible, so we need to perform
-- extra actions here.
--
-- Aside from @contract@ value itself you will need to specify which error to
-- throw in case this value is not valid.
pushContractRef
  :: NiceParameter arg
  => (forall s0. FutureContract arg : s :-> s0)
  -> ContractRef arg
  -> (s :-> ContractRef arg : s)
pushContractRef :: (forall (s0 :: [*]). (FutureContract arg : s) :-> s0)
-> ContractRef arg -> s :-> (ContractRef arg : s)
pushContractRef onContractNotFound :: forall (s0 :: [*]). (FutureContract arg : s) :-> s0
onContractNotFound (ContractRef arg
contractRef :: ContractRef arg) =
  ((KnownValue arg,
  (KnownT (ToT arg), FailOnOperationFound (ContainsOp (ToT arg)),
   FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT arg))))
 :- ParameterScope (ToT arg))
-> (ParameterScope (ToT arg) => s :-> (ContractRef arg : s))
-> s :-> (ContractRef arg : s)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict ((KnownValue arg,
 (KnownT (ToT arg), FailOnOperationFound (ContainsOp (ToT arg)),
  FailOnNestedBigMapsFound (ContainsNestedBigMaps (ToT arg))))
:- ParameterScope (ToT arg)
forall a. NiceParameter a :- ParameterScope (ToT a)
niceParameterEvi @arg) ((ParameterScope (ToT arg) => s :-> (ContractRef arg : s))
 -> s :-> (ContractRef arg : s))
-> (ParameterScope (ToT arg) => s :-> (ContractRef arg : s))
-> s :-> (ContractRef arg : s)
forall a b. (a -> b) -> a -> b
$
    FutureContract arg -> s :-> (FutureContract arg : s)
forall t (s :: [*]). NiceConstant t => t -> s :-> (t & s)
push (ContractRef arg -> FutureContract arg
forall arg. ContractRef arg -> FutureContract arg
FutureContract ContractRef arg
contractRef) (s :-> (FutureContract arg : s))
-> ((FutureContract arg : s)
    :-> (FutureContract arg & (FutureContract arg : s)))
-> s :-> (FutureContract arg & (FutureContract arg : s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (FutureContract arg : s)
:-> (FutureContract arg & (FutureContract arg : s))
forall a (s :: [*]). (a & s) :-> (a & (a & s))
dup (s :-> (FutureContract arg & (FutureContract arg : s)))
-> ((FutureContract arg & (FutureContract arg : s))
    :-> (Maybe (ContractRef arg) & (FutureContract arg : s)))
-> s :-> (Maybe (ContractRef arg) & (FutureContract arg : s))
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
#
    (FutureContract arg & (FutureContract arg : s))
:-> (Maybe (ContractRef arg) & (FutureContract arg : s))
forall p (s :: [*]).
NiceParameter p =>
(FutureContract p & s) :-> (Maybe (ContractRef p) & s)
runFutureContract (s :-> (Maybe (ContractRef arg) & (FutureContract arg : s)))
-> ((Maybe (ContractRef arg) & (FutureContract arg : s))
    :-> (ContractRef arg : s))
-> s :-> (ContractRef arg : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((FutureContract arg : s) :-> (ContractRef arg : s))
-> ((ContractRef arg & (FutureContract arg : s))
    :-> (ContractRef arg : s))
-> (Maybe (ContractRef arg) & (FutureContract arg : s))
   :-> (ContractRef arg : s)
forall (s :: [*]) (s' :: [*]) a.
(s :-> s') -> ((a & s) :-> s') -> (Maybe a & s) :-> s'
ifNone (FutureContract arg : s) :-> (ContractRef arg : s)
forall (s0 :: [*]). (FutureContract arg : s) :-> s0
onContractNotFound (((FutureContract arg : s) :-> s)
-> (ContractRef arg & (FutureContract arg : s))
   :-> (ContractRef arg : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a & s) :-> (a & s')
dip (FutureContract arg : s) :-> s
forall a (s :: [*]). (a & s) :-> s
drop)

-- | Duplicate two topmost items on top of the stack.
dupTop2 ::
  forall (a :: Kind.Type) (b :: Kind.Type) (s :: [Kind.Type]).
  a ': b ': s :-> a ': b ': a ': b ': s
dupTop2 :: (a : b : s) :-> (a : b : a : b : s)
dupTop2 = forall a (s :: [*]) (s1 :: [*]) (tail :: [*]).
(ConstraintDuupXLorentz (ToPeano (2 - 1)) s a s1 tail,
 DuupX (ToPeano 2) s a s1 tail) =>
s :-> (a : s)
forall (n :: Nat) a (s :: [*]) (s1 :: [*]) (tail :: [*]).
(ConstraintDuupXLorentz (ToPeano (n - 1)) s a s1 tail,
 DuupX (ToPeano n) s a s1 tail) =>
s :-> (a : s)
duupX @2 ((a : b : s) :-> (b : a : b : s))
-> ((b : a : b : s) :-> (a : b : a : b : s))
-> (a : b : s) :-> (a : b : a : b : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall a (s :: [*]) (s1 :: [*]) (tail :: [*]).
(ConstraintDuupXLorentz (ToPeano (2 - 1)) s a s1 tail,
 DuupX (ToPeano 2) s a s1 tail) =>
s :-> (a : s)
forall (n :: Nat) a (s :: [*]) (s1 :: [*]) (tail :: [*]).
(ConstraintDuupXLorentz (ToPeano (n - 1)) s a s1 tail,
 DuupX (ToPeano n) s a s1 tail) =>
s :-> (a : s)
duupX @2