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

{-# LANGUAGE NoStarIsType #-}

{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

-- | 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
  , ErrInstr
  , ConstraintReplaceNLorentz
  , ConstraintUpdateNLorentz
  , ReplaceN (..)
  , UpdateN (..)
  , dropX
  , cloneX
  , duupX
  , framedN
  , carN
  , cdrN
  , 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
  , fromOption
  , isSome
  , non
  , non'
  , isEmpty
  , NonZero (..)

  -- * Buildable utils for additional Morley macros
  , buildView_
  , buildViewTuple_

  -- * Macros for working with @address@ and @contract@-like types
  , addressToEpAddress
  , pushContractRef
  , selfAddress
  , view

  -- * Integer division
  , IDiv
  , IMod
  , idiv
  , imod
  ) where

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

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

import Lorentz.ADT
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.Lambda
import Lorentz.Polymorphic
import Lorentz.Value
import Lorentz.ViewBase
import Morley.AsRPC (HasRPCRepr(..))
import Morley.Michelson.Typed (ConstraintDIPN', ConstraintDUG', T, viewNameToMText)
import Morley.Michelson.Typed.Arith
import Morley.Michelson.Typed.Haskell.Value
import Morley.Michelson.Typed.Scope
import Morley.Util.Markdown
import Morley.Util.Peano
import Morley.Util.Type
import Morley.Util.TypeLits

-- $setup
-- >>> :m +Lorentz.Base Lorentz.Run.Simple Lorentz.Instr
-- >>> import Prelude hiding (drop, not, compare, swap)

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

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

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

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

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

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

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

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

ifEq0
  :: (IfCmp0Constraints a Eq')
  => (s :-> s') -> (s :-> s') -> (a : s :-> s')
ifEq0 :: forall a (s :: [Type]) (s' :: [Type]).
IfCmp0Constraints a Eq' =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifEq0 s :-> s'
l s :-> s'
r = (a : s) :-> (Bool : s)
forall n (s :: [Type]).
UnaryArithOpHs Eq' n =>
(n : s) :-> (UnaryArithResHs Eq' n : s)
eq0 ((a : s) :-> (Bool : s)) -> ((Bool : s) :-> s') -> (a : s) :-> s'
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [Type]) (s' :: [Type]).
(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 :: forall a (s :: [Type]) (s' :: [Type]).
IfCmp0Constraints a Neq =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifNeq0 s :-> s'
l s :-> s'
r = (a : s) :-> (Bool : s)
forall n (s :: [Type]).
UnaryArithOpHs Neq n =>
(n : s) :-> (UnaryArithResHs Neq n : s)
neq0 ((a : s) :-> (Bool : s)) -> ((Bool : s) :-> s') -> (a : s) :-> s'
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [Type]) (s' :: [Type]).
(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 :: forall a (s :: [Type]) (s' :: [Type]).
IfCmp0Constraints a Lt =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifLt0 s :-> s'
l s :-> s'
r = (a : s) :-> (Bool : s)
forall n (s :: [Type]).
UnaryArithOpHs Lt n =>
(n : s) :-> (UnaryArithResHs Lt n : s)
lt0 ((a : s) :-> (Bool : s)) -> ((Bool : s) :-> s') -> (a : s) :-> s'
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [Type]) (s' :: [Type]).
(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 :: forall a (s :: [Type]) (s' :: [Type]).
IfCmp0Constraints a Gt =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifGt0 s :-> s'
l s :-> s'
r = (a : s) :-> (Bool : s)
forall n (s :: [Type]).
UnaryArithOpHs Gt n =>
(n : s) :-> (UnaryArithResHs Gt n : s)
gt0 ((a : s) :-> (Bool : s)) -> ((Bool : s) :-> s') -> (a : s) :-> s'
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [Type]) (s' :: [Type]).
(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 :: forall a (s :: [Type]) (s' :: [Type]).
IfCmp0Constraints a Le =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifLe0 s :-> s'
l s :-> s'
r = (a : s) :-> (Bool : s)
forall n (s :: [Type]).
UnaryArithOpHs Le n =>
(n : s) :-> (UnaryArithResHs Le n : s)
le0 ((a : s) :-> (Bool : s)) -> ((Bool : s) :-> s') -> (a : s) :-> s'
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [Type]) (s' :: [Type]).
(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 :: forall a (s :: [Type]) (s' :: [Type]).
IfCmp0Constraints a Ge =>
(s :-> s') -> (s :-> s') -> (a : s) :-> s'
ifGe0 s :-> s'
l s :-> s'
r = (a : s) :-> (Bool : s)
forall n (s :: [Type]).
UnaryArithOpHs Ge n =>
(n : s) :-> (UnaryArithResHs Ge n : s)
ge0 ((a : s) :-> (Bool : s)) -> ((Bool : s) :-> s') -> (a : s) :-> s'
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [Type]) (s' :: [Type]).
(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 :: forall a (s :: [Type]) (s' :: [Type]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifEq s :-> s'
l s :-> s'
r = (a : a : s) :-> (Bool : s)
forall n (s :: [Type]).
NiceComparable n =>
(n : n : s) :-> (Bool : s)
eq ((a : a : s) :-> (Bool : s))
-> ((Bool : s) :-> s') -> (a : a : s) :-> s'
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [Type]) (s' :: [Type]).
(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 :: forall a (s :: [Type]) (s' :: [Type]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifNeq s :-> s'
l s :-> s'
r = (a : a : s) :-> (Bool : s)
forall n (s :: [Type]).
NiceComparable n =>
(n : n : s) :-> (Bool : s)
neq ((a : a : s) :-> (Bool : s))
-> ((Bool : s) :-> s') -> (a : a : s) :-> s'
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [Type]) (s' :: [Type]).
(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 :: forall a (s :: [Type]) (s' :: [Type]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifLt s :-> s'
l s :-> s'
r = (a : a : s) :-> (Bool : s)
forall n (s :: [Type]).
NiceComparable n =>
(n : n : s) :-> (Bool : s)
lt ((a : a : s) :-> (Bool : s))
-> ((Bool : s) :-> s') -> (a : a : s) :-> s'
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [Type]) (s' :: [Type]).
(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 :: forall a (s :: [Type]) (s' :: [Type]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifGt s :-> s'
l s :-> s'
r = (a : a : s) :-> (Bool : s)
forall n (s :: [Type]).
NiceComparable n =>
(n : n : s) :-> (Bool : s)
gt ((a : a : s) :-> (Bool : s))
-> ((Bool : s) :-> s') -> (a : a : s) :-> s'
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [Type]) (s' :: [Type]).
(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 :: forall a (s :: [Type]) (s' :: [Type]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifLe s :-> s'
l s :-> s'
r = (a : a : s) :-> (Bool : s)
forall n (s :: [Type]).
NiceComparable n =>
(n : n : s) :-> (Bool : s)
le ((a : a : s) :-> (Bool : s))
-> ((Bool : s) :-> s') -> (a : a : s) :-> s'
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [Type]) (s' :: [Type]).
(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 :: forall a (s :: [Type]) (s' :: [Type]).
NiceComparable a =>
(s :-> s') -> (s :-> s') -> (a : a : s) :-> s'
ifGe s :-> s'
l s :-> s'
r = (a : a : s) :-> (Bool : s)
forall n (s :: [Type]).
NiceComparable n =>
(n : n : s) :-> (Bool : s)
ge ((a : a : s) :-> (Bool : s))
-> ((Bool : s) :-> s') -> (a : a : s) :-> s'
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
forall (s :: [Type]) (s' :: [Type]).
(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_ :: forall (a :: [Type]) (c :: [Type]). a :-> c
fail_ = a :-> (() : a)
forall (s :: [Type]). s :-> (() : s)
unit (a :-> (() : a)) -> ((() : a) :-> c) -> a :-> c
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (() : a) :-> c
forall a (s :: [Type]) (t :: [Type]).
NiceConstant a =>
(a : s) :-> t
failWith

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

assertUsing
  :: IsError a
  => a -> Bool : s :-> s
assertUsing :: forall err (s :: [Type]). IsError err => err -> (Bool : s) :-> s
assertUsing a
err = (s :-> s) -> (s :-> s) -> (Bool : s) :-> s
forall (s :: [Type]) (s' :: [Type]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ s :-> s
forall (s :: [Type]). 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 :: [Type]) (t :: [Type]).
(IsError e, IsError e) =>
e -> s :-> t
failUsing a
err

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

-- | An instruction that always fails.
type ErrInstr s = forall serr. s :-> serr

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

class CloneX (n :: Peano) a s where
  type CloneXT n a s :: [Type]
  cloneXImpl :: a : s :-> a : CloneXT n a s

instance CloneX 'Z a s where
  type CloneXT 'Z a s = s
  cloneXImpl :: (a : s) :-> (a : CloneXT 'Z a s)
cloneXImpl = (a : s) :-> (a : CloneXT 'Z a s)
forall (s :: [Type]). s :-> s
nop

instance (CloneX n a s, Dupable a) => CloneX ('S n) a s where
  type CloneXT ('S n) a s = a : CloneXT n a s
  cloneXImpl :: (a : s) :-> (a : CloneXT ('S n) a s)
cloneXImpl = forall (n :: Peano) a (s :: [Type]).
CloneX n a s =>
(a : s) :-> (a : CloneXT n a s)
cloneXImpl @n ((a : s) :-> (a : CloneXT n a s))
-> ((a : CloneXT n a s) :-> (a : a : CloneXT n a s))
-> (a : s) :-> (a : a : CloneXT n a s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : CloneXT n a s) :-> (a : a : CloneXT n a s)
forall a (s :: [Type]). Dupable a => (a : s) :-> (a : a : s)
dup

-- | Duplicate the top of the stack @n@ times.
--
-- For example, `cloneX @3` has type `a : s :-> a : a : a : a : s`.
cloneX
  :: forall (n :: Nat) a s. CloneX (ToPeano n) a s
  => a : s :-> a : CloneXT (ToPeano n) a s
cloneX :: forall (n :: Nat) a (s :: [Type]).
CloneX (ToPeano n) a s =>
(a : s) :-> (a : CloneXT (ToPeano n) a s)
cloneX = forall (n :: Peano) a (s :: [Type]).
CloneX n a s =>
(a : s) :-> (a : CloneXT n a s)
cloneXImpl @(ToPeano 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 @DUU+P@ has since been added as the @DUP n@ instruction and so this
-- macro is defined simply as follows:
--
-- > duupX = dupN @n
duupX
  :: forall (n :: Nat) a s s'.
     (ConstraintDUPNLorentz (ToPeano n) s s' a, Dupable a)
  => s :-> a ': s
duupX :: forall (n :: Nat) a (s :: [Type]) (s' :: [Type]).
(ConstraintDUPNLorentz (ToPeano n) s s' a, Dupable a) =>
s :-> (a : s)
duupX = forall (n :: Nat) a (inp :: [Type]) (out :: [Type]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @n

-- | 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.
--
-- Given a stack of 3 elements,
-- >>> arg = (1 :: Integer) ::: (2 :: Integer) ::: (3 :: Integer)
--
-- @framedN@ will have access to exactly the number of elements specified,
-- >>> framedN @1 drop -$ arg
-- 2 ::: 3
-- >>> framedN @1 (drop # drop) -$ arg
-- ...
-- ... error:
-- ... Couldn't match type: '[]
-- ...                with: a0 : o'0
-- ...
--
-- When the number of elements is larger than the size of the stack, @framedN@
-- will have access to all of them:
-- >>> framedN @5 (drop # drop) -$ arg
-- 3
--
-- But not more than there are on stack:
-- >>> framedN @5 (drop # drop # drop # drop) -$ arg
-- ...
-- ... error:
-- ... Couldn't match type ‘ZippedStackRepr a1 (ZippedStackRepr a0 out)’
-- ... with ‘Integer’
-- ...

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 :: forall (n :: Nat) (nNat :: Peano) (s :: [Type]) (i :: [Type])
       (i' :: [Type]) (o :: [Type]) (o' :: [Type]).
(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 = forall (s :: [Type]) (i :: [Type]) (o :: [Type]).
(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 :: [Type]) (i :: [Type])
       (i' :: [Type]) (o :: [Type]) (o' :: [Type]).
(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 @2

carN
  :: forall (n :: Nat) (pair :: Type) (s :: [Type]).
     ConstraintPairGetLorentz (2 * n + 1) pair
  => pair : s :-> PairGetHs (ToPeano (2 * n + 1)) pair : s
carN :: forall (n :: Nat) pair (s :: [Type]).
ConstraintPairGetLorentz ((2 * n) + 1) pair =>
(pair : s) :-> (PairGetHs (ToPeano ((2 * n) + 1)) pair : s)
carN = forall (n :: Nat) pair (s :: [Type]).
ConstraintPairGetLorentz n pair =>
(pair : s) :-> (PairGetHs (ToPeano n) pair : s)
pairGet @(2 * n + 1)
  where
    _example :: '[ (String, (Integer, ())) ] :-> '[ String ]
    _example :: '[(String, (Integer, ()))] :-> '[String]
_example = forall (n :: Nat) pair (s :: [Type]).
ConstraintPairGetLorentz ((2 * n) + 1) pair =>
(pair : s) :-> (PairGetHs (ToPeano ((2 * n) + 1)) pair : s)
carN @0

    _example' :: '[ (String, (Integer, ())) ] :-> '[ Integer ]
    _example' :: '[(String, (Integer, ()))] :-> '[Integer]
_example' = forall (n :: Nat) pair (s :: [Type]).
ConstraintPairGetLorentz ((2 * n) + 1) pair =>
(pair : s) :-> (PairGetHs (ToPeano ((2 * n) + 1)) pair : s)
carN @1

cdrN
  :: forall (n :: Nat) (pair :: Type) (s :: [Type]).
     ConstraintPairGetLorentz (2 * n) pair
  => pair : s :-> PairGetHs (ToPeano (2 * n)) pair : s
cdrN :: forall (n :: Nat) pair (s :: [Type]).
ConstraintPairGetLorentz (2 * n) pair =>
(pair : s) :-> (PairGetHs (ToPeano (2 * n)) pair : s)
cdrN = forall (n :: Nat) pair (s :: [Type]).
ConstraintPairGetLorentz n pair =>
(pair : s) :-> (PairGetHs (ToPeano n) pair : s)
pairGet @(2 * n)
  where
    _example :: '[ (String, (Integer, ())) ] :-> '[ (String, (Integer, ())) ]
    _example :: '[(String, (Integer, ()))] :-> '[(String, (Integer, ()))]
_example = forall (n :: Nat) pair (s :: [Type]).
ConstraintPairGetLorentz (2 * n) pair =>
(pair : s) :-> (PairGetHs (ToPeano (2 * n)) pair : s)
cdrN @0

    _example' :: '[ (String, (Integer, ())) ] :-> '[ (Integer, ()) ]
    _example' :: '[(String, (Integer, ()))] :-> '[(Integer, ())]
_example' = forall (n :: Nat) pair (s :: [Type]).
ConstraintPairGetLorentz (2 * n) pair =>
(pair : s) :-> (PairGetHs (ToPeano (2 * n)) pair : s)
cdrN @1

    _example'' :: '[ (String, (Integer, ())) ] :-> '[ () ]
    _example'' :: '[(String, (Integer, ()))] :-> '[()]
_example'' = forall (n :: Nat) pair (s :: [Type]).
ConstraintPairGetLorentz (2 * n) pair =>
(pair : s) :-> (PairGetHs (ToPeano (2 * n)) pair : s)
cdrN @2

-- |
-- >>> papair == pair # pair
-- True
--
-- >>> papair -$ True ::: 1 ::: ()
-- ((True,1),())
papair :: a : b : c : s :-> ((a, b), c) : s
papair :: forall a b c (s :: [Type]). (a : b : c : s) :-> (((a, b), c) : s)
papair = (a : b : c : s) :-> ((a, b) : c : s)
forall a b (s :: [Type]). (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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, b) : c : s) :-> (((a, b), c) : s)
forall a b (s :: [Type]). (a : b : s) :-> ((a, b) : s)
pair

-- |
-- >>> ppaiir == dip pair # pair
-- True
--
-- >>> ppaiir -$ True ::: 1 ::: ()
-- (True,(1,()))
ppaiir :: a : b : c : s :-> (a, (b, c)) : s
ppaiir :: forall a b c (s :: [Type]). (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 :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (b : c : s) :-> ((b, c) : s)
forall a b (s :: [Type]). (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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : (b, c) : s) :-> ((a, (b, c)) : s)
forall a b (s :: [Type]). (a : b : s) :-> ((a, b) : s)
pair

-- |
-- >>> cdar == cdr # car
-- True
--
-- >>> cdar -$ (True, (1, ()))
-- 1
cdar :: (a1, (a2, b)) : s :-> a2 : s
cdar :: forall a1 a2 b (s :: [Type]). ((a1, (a2, b)) : s) :-> (a2 : s)
cdar = ((a1, (a2, b)) : s) :-> ((a2, b) : s)
forall a b (s :: [Type]). ((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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a2, b) : s) :-> (a2 : s)
forall a b (s :: [Type]). ((a, b) : s) :-> (a : s)
car

-- |
-- >>> cddr == cdr # cdr
-- True
--
-- >>> cddr -$ (True, (1, ()))
-- ()
cddr :: (a1, (a2, b)) : s :-> b : s
cddr :: forall a1 a2 b (s :: [Type]). ((a1, (a2, b)) : s) :-> (b : s)
cddr = ((a1, (a2, b)) : s) :-> ((a2, b) : s)
forall a b (s :: [Type]). ((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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a2, b) : s) :-> (b : s)
forall a b (s :: [Type]). ((a, b) : s) :-> (b : s)
cdr

-- |
-- >>> caar == car # car
-- True
--
-- >>> caar -$ ((True, 1), ())
-- True
caar :: ((a, b1), b2) : s :-> a : s
caar :: forall a b1 b2 (s :: [Type]). (((a, b1), b2) : s) :-> (a : s)
caar = (((a, b1), b2) : s) :-> ((a, b1) : s)
forall a b (s :: [Type]). ((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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, b1) : s) :-> (a : s)
forall a b (s :: [Type]). ((a, b) : s) :-> (a : s)
car

-- |
-- >>> cadr == car # cdr
-- True
--
-- >>> cadr -$ ((True, 1), ())
-- 1
cadr :: ((a, b1), b2) : s :-> b1 : s
cadr :: forall a b1 b2 (s :: [Type]). (((a, b1), b2) : s) :-> (b1 : s)
cadr = (((a, b1), b2) : s) :-> ((a, b1) : s)
forall a b (s :: [Type]). ((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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a, b1) : s) :-> (b1 : s)
forall a b (s :: [Type]). ((a, b) : s) :-> (b : s)
cdr

-- |
-- >>> setCar == cdr # swap # pair
-- True
--
-- >>> setCar -$ (True, 1) ::: ()
-- ((),1)
setCar :: (a, b1) : (b2 : s) :-> (b2, b1) : s
setCar :: forall a b1 b2 (s :: [Type]). ((a, b1) : b2 : s) :-> ((b2, b1) : s)
setCar = ((a, b1) : b2 : s) :-> (b1 : b2 : s)
forall a b (s :: [Type]). ((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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b1 : b2 : s) :-> (b2 : b1 : s)
forall a b (s :: [Type]). (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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b2 : b1 : s) :-> ((b2, b1) : s)
forall a b (s :: [Type]). (a : b : s) :-> ((a, b) : s)
pair

-- |
-- >>> setCdr == car # pair
-- True
--
-- >>> setCdr -$ (True, 1) ::: ()
-- (True,())
setCdr :: (a, b1) : (b2 : s) :-> (a, b2) : s
setCdr :: forall a b1 b2 (s :: [Type]). ((a, b1) : b2 : s) :-> ((a, b2) : s)
setCdr = ((a, b1) : b2 : s) :-> (a : b2 : s)
forall a b (s :: [Type]). ((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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : b2 : s) :-> ((a, b2) : s)
forall a b (s :: [Type]). (a : b : s) :-> ((a, b) : s)
pair

-- |
-- >>> mapCar (not @Bool) == unpair # (not @Bool) # pair
-- True
--
-- >>> mapCar not -$ (True, 1)
-- (False,1)
mapCar
  :: (forall s0. a : s0 :-> a1 : s0)
  -> (a, b) : s :-> (a1, b) : s
mapCar :: forall a a1 b (s :: [Type]).
(forall (s0 :: [Type]). (a : s0) :-> (a1 : s0))
-> ((a, b) : s) :-> ((a1, b) : s)
mapCar forall (s0 :: [Type]). (a : s0) :-> (a1 : s0)
op = ((a, b) : s) :-> (a : b : s)
forall a b (s :: [Type]). ((a, b) : s) :-> (a : b : s)
unpair (((a, b) : s) :-> (a : b : s))
-> ((a : b : s) :-> (a1 : b : s)) -> ((a, b) : s) :-> (a1 : b : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : b : s) :-> (a1 : b : s)
forall (s0 :: [Type]). (a : s0) :-> (a1 : s0)
op (((a, b) : s) :-> (a1 : b : s))
-> ((a1 : b : s) :-> ((a1, b) : s))
-> ((a, b) : s) :-> ((a1, b) : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a1 : b : s) :-> ((a1, b) : s)
forall a b (s :: [Type]). (a : b : s) :-> ((a, b) : s)
pair

-- |
-- >>> mapCdr (not @Bool) == unpair # dip (not @Bool) # pair
-- True
--
-- >>> mapCdr not -$ (1, True)
-- (1,False)
mapCdr
  :: (forall s0. b : s0 :-> b1 : s0)
  -> (a, b) : s :-> (a, b1) : s
mapCdr :: forall b b1 a (s :: [Type]).
(forall (s0 :: [Type]). (b : s0) :-> (b1 : s0))
-> ((a, b) : s) :-> ((a, b1) : s)
mapCdr forall (s0 :: [Type]). (b : s0) :-> (b1 : s0)
op = ((a, b) : s) :-> (a : b : s)
forall a b (s :: [Type]). ((a, b) : s) :-> (a : b : s)
unpair (((a, b) : s) :-> (a : b : s))
-> ((a : b : s) :-> (a : b1 : s)) -> ((a, b) : s) :-> (a : b1 : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((b : s) :-> (b1 : s)) -> (a : b : s) :-> (a : b1 : s)
forall a (s :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (b : s) :-> (b1 : s)
forall (s0 :: [Type]). (b : s0) :-> (b1 : s0)
op (((a, b) : s) :-> (a : b1 : s))
-> ((a : b1 : s) :-> ((a, b1) : s))
-> ((a, b) : s) :-> ((a, b1) : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : b1 : s) :-> ((a, b1) : s)
forall a b (s :: [Type]). (a : b : s) :-> ((a, b) : s)
pair

-- |
-- >>> ifRight (not @Bool) (dup @Integer # compare # eq0) == ifLeft (dup @Integer # compare # eq0) (not @Bool)
-- True
--
-- >>> ifRight not (dup # compare # eq0) -$ (Right True :: Either Integer Bool)
-- False
--
-- >>> ifRight not (dup # compare # eq0) -$ (Left 1 :: Either Integer Bool)
-- True
ifRight :: (b : s :-> s') -> (a : s :-> s') -> (Either a b : s :-> s')
ifRight :: forall b (s :: [Type]) (s' :: [Type]) a.
((b : s) :-> s') -> ((a : s) :-> s') -> (Either a b : s) :-> s'
ifRight (b : s) :-> s'
l (a : s) :-> s'
r = ((a : s) :-> s') -> ((b : s) :-> s') -> (Either a b : s) :-> s'
forall a (s :: [Type]) (s' :: [Type]) b.
((a : s) :-> s') -> ((b : s) :-> s') -> (Either a b : s) :-> s'
ifLeft (a : s) :-> s'
r (b : s) :-> s'
l


-- |
-- >>> ifSome (dup @Integer # compare # eq0) (push False) == ifNone (push False) (dup @Integer # compare # eq0)
-- True
--
-- >>> ifSome (dup # compare # eq0) (push False) -$ (Just 1 :: Maybe Integer)
-- True
--
-- >>> ifSome (dup # compare # eq0) (push False) -$ (Nothing :: Maybe Integer)
-- False
ifSome
  :: (a : s :-> s') -> (s :-> s') -> (Maybe a : s :-> s')
ifSome :: forall a (s :: [Type]) (s' :: [Type]).
((a : s) :-> s') -> (s :-> s') -> (Maybe a : s) :-> s'
ifSome (a : s) :-> s'
s s :-> s'
n = (s :-> s') -> ((a : s) :-> s') -> (Maybe a : s) :-> s'
forall (s :: [Type]) (s' :: [Type]) a.
(s :-> s') -> ((a : s) :-> s') -> (Maybe a : s) :-> s'
ifNone s :-> s'
n (a : s) :-> s'
s


-- |
-- >>> when_ (push 5 # add @Integer @Integer) == if_ (push 5 # add @Integer @Integer) nop
-- True
--
-- >>> when_ (push 5 # add @Integer) -$ True ::: 3
-- 8
--
-- >>> when_ (push 5 # add @Integer) -$ False ::: 3
-- 3
when_ :: (s :-> s) -> (Bool : s :-> s)
when_ :: forall (s :: [Type]). (s :-> s) -> (Bool : s) :-> s
when_ s :-> s
i = (s :-> s) -> (s :-> s) -> (Bool : s) :-> s
forall (s :: [Type]) (s' :: [Type]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ s :-> s
i s :-> s
forall (s :: [Type]). s :-> s
nop

-- |
-- >>> unless_ (push 5 # add @Integer @Integer) == if_ nop (push 5 # add @Integer @Integer)
-- True
--
-- >>> unless_ (push 5 # add @Integer) -$ True ::: 3
-- 3
--
-- >>> unless_ (push 5 # add @Integer) -$ False ::: 3
-- 8
unless_ :: (s :-> s) -> (Bool : s :-> s)
unless_ :: forall (s :: [Type]). (s :-> s) -> (Bool : s) :-> s
unless_ s :-> s
i = (s :-> s) -> (s :-> s) -> (Bool : s) :-> s
forall (s :: [Type]) (s' :: [Type]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ s :-> s
forall (s :: [Type]). s :-> s
nop s :-> s
i

-- |
-- >>> whenSome drop == ifSome drop nop
-- True
--
-- >>> whenSome drop -$ Just 1 ::: ()
-- ()
whenSome :: (a : s :-> s) -> (Maybe a : s :-> s)
whenSome :: forall a (s :: [Type]). ((a : s) :-> s) -> (Maybe a : s) :-> s
whenSome (a : s) :-> s
i = ((a : s) :-> s) -> (s :-> s) -> (Maybe a : s) :-> s
forall a (s :: [Type]) (s' :: [Type]).
((a : s) :-> s') -> (s :-> s') -> (Maybe a : s) :-> s'
ifSome (a : s) :-> s
i s :-> s
forall (s :: [Type]). s :-> s
nop

-- |
-- >>> whenNone (push True) == ifNone (push True) nop
-- True
--
-- >>> whenNone (push 1) -$ (Nothing :: Maybe Integer)
-- 1
whenNone :: (s :-> a : s) -> (Maybe a : s :-> a : s)
whenNone :: forall (s :: [Type]) a.
(s :-> (a : s)) -> (Maybe a : s) :-> (a : s)
whenNone s :-> (a : s)
i = (s :-> (a : s))
-> ((a : s) :-> (a : s)) -> (Maybe a : s) :-> (a : s)
forall (s :: [Type]) (s' :: [Type]) a.
(s :-> s') -> ((a : s) :-> s') -> (Maybe a : s) :-> s'
ifNone s :-> (a : s)
i (a : s) :-> (a : s)
forall (s :: [Type]). 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 :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (v : map k v : s) :-> (Maybe v : map k v : s)
forall a (s :: [Type]). (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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k : Maybe v : map k v : s) :-> (map k v : s)
forall (map :: Type -> Type -> Type) k v (s :: [Type]).
(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
    :: (IsoValue (map k v), NiceComparable k, NiceConstant e, Dupable k, KnownValue v)
    => (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 :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (forall a (s :: [Type]). 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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k : Maybe v : map k v : s) :-> (map k v : s)
forall (map :: Type -> Type -> Type) k v (s :: [Type]).
(MapInstrs map, NiceComparable k) =>
(k : Maybe v : map k v : s) :-> (map k v : s)
mapUpdate

instance MapInstrs Map where
  mapUpdate :: forall k v (s :: [Type]).
NiceComparable k =>
(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 :: [Type]).
UpdOpHs c =>
(UpdOpKeyHs c : UpdOpParamsHs c : c : s) :-> (c : s)
update
  mapInsertNew :: forall k v e (s :: [Type]).
(IsoValue (Map k v), NiceComparable k, NiceConstant e, Dupable k,
 KnownValue v) =>
(forall (s0 :: [Type]). (k : s0) :-> (e : s0))
-> (k : v : Map k v : s) :-> (Map k v : s)
mapInsertNew forall (s0 :: [Type]). (k : s0) :-> (e : s0)
mkErr =
    ((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 :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (v : Map k v : s) :-> (Maybe v : Map k v : s)
forall a (s :: [Type]). (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)
    :-> (k : k : Maybe v : Map k v : s))
-> (k : v : Map k v : s) :-> (k : k : Maybe v : Map k v : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k : Maybe v : Map k v : s) :-> (k : k : Maybe v : Map k v : s)
forall a (s :: [Type]). Dupable a => (a : s) :-> (a : a : s)
dup ((k : v : Map k v : s) :-> (k : k : Maybe v : Map k v : s))
-> ((k : k : Maybe v : Map k v : s)
    :-> (k : Maybe v : Map k v : s))
-> (k : v : Map k v : s) :-> (k : Maybe v : Map k v : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((k : Maybe v : Map k v : s) :-> (Maybe v : Map k v : s))
-> (k : k : Maybe v : Map k v : s) :-> (k : Maybe v : Map k v : s)
forall a (s :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (k : Maybe v : Map k v : s) :-> (Maybe v : Map k v : s)
forall c (s :: [Type]).
(GetOpHs c, UpdOpHs c, KnownValue (GetOpValHs c),
 UpdOpKeyHs c ~ GetOpKeyHs c) =>
(UpdOpKeyHs c : UpdOpParamsHs c : c : s)
:-> (Maybe (GetOpValHs c) : c : s)
getAndUpdate ((k : v : Map k v : s) :-> (k : Maybe v : Map k v : s))
-> ((k : Maybe v : Map k v : s) :-> (Maybe v : k : Map k v : s))
-> (k : v : Map k v : s) :-> (Maybe v : k : Map k v : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k : Maybe v : Map k v : s) :-> (Maybe v : k : Map k v : s)
forall a b (s :: [Type]). (a : b : s) :-> (b : a : s)
swap ((k : v : Map k v : s) :-> (Maybe v : k : Map k v : s))
-> ((Maybe v : k : Map k v : s) :-> (Map k v : s))
-> (k : v : Map k v : s) :-> (Map k v : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((k : Map k v : s) :-> (Map k v : s))
-> ((v : k : Map k v : s) :-> (Map k v : s))
-> (Maybe v : k : Map k v : s) :-> (Map k v : s)
forall (s :: [Type]) (s' :: [Type]) a.
(s :-> s') -> ((a : s) :-> s') -> (Maybe a : s) :-> s'
ifNone (k : Map k v : s) :-> (Map k v : s)
forall a (s :: [Type]). (a : s) :-> s
drop ((v : k : Map k v : s) :-> (k : Map k v : s)
forall a (s :: [Type]). (a : s) :-> s
drop ((v : k : Map k v : s) :-> (k : Map k v : s))
-> ((k : Map k v : s) :-> (e : Map k v : s))
-> (v : k : Map k v : s) :-> (e : Map k v : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k : Map k v : s) :-> (e : Map k v : s)
forall (s0 :: [Type]). (k : s0) :-> (e : s0)
mkErr ((v : k : Map k v : s) :-> (e : Map k v : s))
-> ((e : Map k v : s) :-> (Map k v : s))
-> (v : k : Map k v : s) :-> (Map k v : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (e : Map k v : s) :-> (Map k v : s)
forall a (s :: [Type]) (t :: [Type]).
NiceConstant a =>
(a : s) :-> t
failWith)
instance MapInstrs BigMap where
  mapUpdate :: forall k v (s :: [Type]).
NiceComparable k =>
(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 :: [Type]).
UpdOpHs c =>
(UpdOpKeyHs c : UpdOpParamsHs c : c : s) :-> (c : s)
update
  mapInsertNew :: forall k v e (s :: [Type]).
(IsoValue (BigMap k v), NiceComparable k, NiceConstant e,
 Dupable k, KnownValue v) =>
(forall (s0 :: [Type]). (k : s0) :-> (e : s0))
-> (k : v : BigMap k v : s) :-> (BigMap k v : s)
mapInsertNew forall (s0 :: [Type]). (k : s0) :-> (e : s0)
mkErr =
    ((v : BigMap k v : s) :-> (Maybe v : BigMap k v : s))
-> (k : v : BigMap k v : s) :-> (k : Maybe v : BigMap k v : s)
forall a (s :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (v : BigMap k v : s) :-> (Maybe v : BigMap k v : s)
forall a (s :: [Type]). (a : s) :-> (Maybe a : s)
some ((k : v : BigMap k v : s) :-> (k : Maybe v : BigMap k v : s))
-> ((k : Maybe v : BigMap k v : s)
    :-> (k : k : Maybe v : BigMap k v : s))
-> (k : v : BigMap k v : s) :-> (k : k : Maybe v : BigMap k v : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k : Maybe v : BigMap k v : s)
:-> (k : k : Maybe v : BigMap k v : s)
forall a (s :: [Type]). Dupable a => (a : s) :-> (a : a : s)
dup ((k : v : BigMap k v : s) :-> (k : k : Maybe v : BigMap k v : s))
-> ((k : k : Maybe v : BigMap k v : s)
    :-> (k : Maybe v : BigMap k v : s))
-> (k : v : BigMap k v : s) :-> (k : Maybe v : BigMap k v : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((k : Maybe v : BigMap k v : s) :-> (Maybe v : BigMap k v : s))
-> (k : k : Maybe v : BigMap k v : s)
   :-> (k : Maybe v : BigMap k v : s)
forall a (s :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (k : Maybe v : BigMap k v : s) :-> (Maybe v : BigMap k v : s)
forall c (s :: [Type]).
(GetOpHs c, UpdOpHs c, KnownValue (GetOpValHs c),
 UpdOpKeyHs c ~ GetOpKeyHs c) =>
(UpdOpKeyHs c : UpdOpParamsHs c : c : s)
:-> (Maybe (GetOpValHs c) : c : s)
getAndUpdate ((k : v : BigMap k v : s) :-> (k : Maybe v : BigMap k v : s))
-> ((k : Maybe v : BigMap k v : s)
    :-> (Maybe v : k : BigMap k v : s))
-> (k : v : BigMap k v : s) :-> (Maybe v : k : BigMap k v : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k : Maybe v : BigMap k v : s) :-> (Maybe v : k : BigMap k v : s)
forall a b (s :: [Type]). (a : b : s) :-> (b : a : s)
swap ((k : v : BigMap k v : s) :-> (Maybe v : k : BigMap k v : s))
-> ((Maybe v : k : BigMap k v : s) :-> (BigMap k v : s))
-> (k : v : BigMap k v : s) :-> (BigMap k v : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((k : BigMap k v : s) :-> (BigMap k v : s))
-> ((v : k : BigMap k v : s) :-> (BigMap k v : s))
-> (Maybe v : k : BigMap k v : s) :-> (BigMap k v : s)
forall (s :: [Type]) (s' :: [Type]) a.
(s :-> s') -> ((a : s) :-> s') -> (Maybe a : s) :-> s'
ifNone (k : BigMap k v : s) :-> (BigMap k v : s)
forall a (s :: [Type]). (a : s) :-> s
drop ((v : k : BigMap k v : s) :-> (k : BigMap k v : s)
forall a (s :: [Type]). (a : s) :-> s
drop ((v : k : BigMap k v : s) :-> (k : BigMap k v : s))
-> ((k : BigMap k v : s) :-> (e : BigMap k v : s))
-> (v : k : BigMap k v : s) :-> (e : BigMap k v : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (k : BigMap k v : s) :-> (e : BigMap k v : s)
forall (s0 :: [Type]). (k : s0) :-> (e : s0)
mkErr ((v : k : BigMap k v : s) :-> (e : BigMap k v : s))
-> ((e : BigMap k v : s) :-> (BigMap k v : s))
-> (v : k : BigMap k v : s) :-> (BigMap k v : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (e : BigMap k v : s) :-> (BigMap k v : s)
forall a (s :: [Type]) (t :: [Type]).
NiceConstant a =>
(a : s) :-> t
failWith)

-- | Insert given element into set.
--
-- This is a separate function from 'mapUpdate' because stacks they operate with
-- differ in length.
setInsert :: NiceComparable e => e : Set e : s :-> Set e : s
setInsert :: forall e (s :: [Type]).
NiceComparable e =>
(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 :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Bool -> (Set e : s) :-> (Bool : Set e : s)
forall t (s :: [Type]). 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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (e : Bool : Set e : s) :-> (Set e : s)
forall c (s :: [Type]).
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
  :: (NiceConstant err, NiceComparable e, Dupable e, Dupable (Set e))
  => (forall s0. e : s0 :-> err : s0)
  -> e : Set e : s :-> Set e : s
setInsertNew :: forall err e (s :: [Type]).
(NiceConstant err, NiceComparable e, Dupable e, Dupable (Set e)) =>
(forall (s0 :: [Type]). (e : s0) :-> (err : s0))
-> (e : Set e : s) :-> (Set e : s)
setInsertNew forall (s0 :: [Type]). (e : s0) :-> (err : s0)
desc =
  (e : Set e : s) :-> (e : Set e : e : Set e : s)
forall a b (s :: [Type]).
(Dupable a, Dupable b) =>
(a : b : s) :-> (a : b : a : b : s)
dupTop2 ((e : Set e : s) :-> (e : Set e : e : Set e : s))
-> ((e : Set e : e : Set e : s) :-> (Bool : e : Set e : s))
-> (e : Set e : s) :-> (Bool : e : Set e : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (e : Set e : e : Set e : s) :-> (Bool : e : Set e : s)
forall c (s :: [Type]).
MemOpHs c =>
(MemOpKeyHs c : c : s) :-> (Bool : s)
mem ((e : Set e : s) :-> (Bool : e : Set e : s))
-> ((Bool : e : Set e : s) :-> (Set e : s))
-> (e : Set e : s) :-> (Set e : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  ((e : Set e : s) :-> (Set e : s))
-> ((e : Set e : s) :-> (Set e : s))
-> (Bool : e : Set e : s) :-> (Set e : s)
forall (s :: [Type]) (s' :: [Type]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ ((e : Set e : s) :-> (err : Set e : s)
forall (s0 :: [Type]). (e : s0) :-> (err : s0)
desc ((e : Set e : s) :-> (err : Set e : s))
-> ((err : Set e : s) :-> (Set e : s))
-> (e : Set e : s) :-> (Set e : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (err : Set e : s) :-> (Set e : s)
forall a (s :: [Type]) (t :: [Type]).
NiceConstant a =>
(a : s) :-> t
failWith) (((Set e : s) :-> (Bool : Set e : s))
-> (e : Set e : s) :-> (e : Bool : Set e : s)
forall a (s :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Bool -> (Set e : s) :-> (Bool : Set e : s)
forall t (s :: [Type]). 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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (e : Bool : Set e : s) :-> (Set e : s)
forall c (s :: [Type]).
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 :: forall e (s :: [Type]).
NiceComparable e =>
(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 :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (Bool -> (Set e : s) :-> (Bool : Set e : s)
forall t (s :: [Type]). 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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (e : Bool : Set e : s) :-> (Set e : s)
forall c (s :: [Type]).
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 :: [Type]) (a :: Type)
  (mid :: [Type]) (tail :: [Type]) =
  ( ReplaceNConstraint' T n (ToTs s) (ToT a) (ToTs mid) (ToTs tail)
  , ReplaceNConstraint' Type n s a mid tail
  )

class ReplaceN (n :: Peano) (s :: [Type]) (a :: 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 :: [Type]). (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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : a : xs) :-> (a : xs)
forall a (s :: [Type]). (a : s) :-> s
drop

instance {-# OVERLAPPABLE #-} (ConstraintReplaceNLorentz ('S n) s a mid tail, SingI n) =>
  ReplaceN ('S ('S n)) s a mid tail where
  replaceNImpl :: (a : s) :-> s
replaceNImpl =
    -- 'stackType' helps GHC deduce types
    forall (n :: Peano) (inp :: [Type]) (out :: [Type]) (s :: [Type])
       (s' :: [Type]).
ConstraintDIPNLorentz n inp out s s' =>
(s :-> s') -> inp :-> out
dipNPeano @('S ('S n)) (forall (s :: [Type]). s :-> s
stackType @(a ': tail) ((a : tail) :-> (a : tail))
-> ((a : tail) :-> tail) -> (a : tail) :-> tail
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : tail) :-> tail
forall a (s :: [Type]). (a : s) :-> s
drop) ((a : s) :-> (a : Drop ('S 'Z) mid))
-> ((a : Drop ('S 'Z) mid) :-> s) -> (a : s) :-> s
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall (n :: Peano) (inp :: [Type]) (out :: [Type]) 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 :: Nat) a (s :: [Type]) (s1 :: [Type]) (tail :: [Type]).
  ( ConstraintReplaceNLorentz (ToPeano (n - 1)) s a s1 tail
  , ReplaceN (ToPeano n) s a s1 tail
  )
  => a ': s :-> s
replaceN :: forall (n :: Nat) a (s :: [Type]) (s1 :: [Type]) (tail :: [Type]).
(ConstraintReplaceNLorentz (ToPeano (n - 1)) s a s1 tail,
 ReplaceN (ToPeano n) s a s1 tail) =>
(a : s) :-> s
replaceN = forall {k} {k} (n :: Peano) (s :: [Type]) a (mid :: k) (tail :: k).
ReplaceN n s a mid tail =>
(a : s) :-> s
forall (n :: Peano) (s :: [Type]) a (mid :: [Type])
       (tail :: [Type]).
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 (n :: Nat) a (s :: [Type]) (s1 :: [Type]) (tail :: [Type]).
(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 :: [Type]) (a :: Type) (b :: Type)
  (mid :: [Type]) (tail :: [Type]) =
  ( UpdateNConstraint' T n (ToTs s) (ToT a) (ToT b) (ToTs mid) (ToTs tail)
  , UpdateNConstraint' Type n s a b mid tail
  )

class UpdateN (n :: Peano) (s :: [Type]) (a :: Type) (b :: 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 '[a, b] :-> '[b]
instr = ('[a, b] :-> '[b]) -> ('[a, b] ++ tail) :-> ('[b] ++ tail)
forall (s :: [Type]) (i :: [Type]) (o :: [Type]).
(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 '[a, b] :-> '[b]
instr = (a : x : b : tail) :-> (x : a : b : tail)
forall a b (s :: [Type]). (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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a : b : tail) :-> (b : tail))
-> (x : a : b : tail) :-> (x : b : tail)
forall a (s :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (('[a, b] :-> '[b]) -> ('[a, b] ++ tail) :-> ('[b] ++ tail)
forall (s :: [Type]) (i :: [Type]) (o :: [Type]).
(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, SingI n) =>
  UpdateN ('S ('S ('S n))) s a b mid tail where
  updateNImpl :: ('[a, b] :-> '[b]) -> (a : s) :-> s
updateNImpl '[a, b] :-> '[b]
instr =
    -- 'stackType' helps GHC deduce types
    forall (n :: Peano) (inp :: [Type]) (out :: [Type]) a.
ConstraintDUGLorentz n inp out a =>
inp :-> out
dugPeano @('S ('S n)) ((a : s) :-> mid) -> (mid :-> s) -> (a : s) :-> s
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall (n :: Peano) (inp :: [Type]) (out :: [Type]) (s :: [Type])
       (s' :: [Type]).
ConstraintDIPNLorentz n inp out s s' =>
(s :-> s') -> inp :-> out
dipNPeano @('S ('S n)) (('[a, b] :-> '[b]) -> ('[a, b] ++ tail) :-> ('[b] ++ tail)
forall (s :: [Type]) (i :: [Type]) (o :: [Type]).
(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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall (s :: [Type]). 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 :: Nat) a b (s :: [Type]) (mid :: [Type]) (tail :: [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 :: forall (n :: Nat) a b (s :: [Type]) (mid :: [Type])
       (tail :: [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]
instr = forall {k} {k} (n :: Peano) (s :: [Type]) a b (mid :: k)
       (tail :: k).
UpdateN n s a b mid tail =>
('[a, b] :-> '[b]) -> (a : s) :-> s
forall (n :: Peano) (s :: [Type]) a b (mid :: [Type])
       (tail :: [Type]).
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 = forall (n :: Nat) a b (s :: [Type]) (mid :: [Type])
       (tail :: [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 @3 '[Integer, [Integer]] :-> '[[Integer]]
forall a (s :: [Type]). (a : List a : s) :-> (List a : s)
cons

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

-- | @view@ type synonym as described in A1.
data View_ (a :: Type) (r :: Type) = View_
  { forall a r. View_ a r -> a
viewParam :: a
  , forall a r. 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 (HasNoOpToT r, WellTypedToT a) => IsoValue (View_ a r)

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

instance HasRPCRepr a => HasRPCRepr (View_ a r) where
  type AsRPC (View_ a r) = View_ (AsRPC a) r

instance Each [Typeable, TypeHasDoc] [a, r] => TypeHasDoc (View_ a r) where
  typeDocName :: Proxy (View_ a r) -> Text
typeDocName Proxy (View_ a r)
_ = Text
"View"
  typeDocMdDescription :: Markdown
typeDocMdDescription =
    Markdown
"`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 :: Type -> Type -> Type) 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 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
<>
    [forall t. TypeHasDoc t => SomeDocDefinitionItem
dTypeDep @MText, 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 a b.
(Typeable a, GenericIsoValue a, GTypeHasDoc (Rep a),
 HaveCommonTypeCtor b a) =>
TypeDocHaskellRep b
concreteTypeDocHaskellRep @(View_ MText Integer)
  typeDocMichelsonRep :: TypeDocMichelsonRep (View_ a r)
typeDocMichelsonRep =
    forall a b.
(Typeable a, KnownIsoT a, HaveCommonTypeCtor b a) =>
TypeDocMichelsonRep b
forall {k} a (b :: k).
(Typeable a, KnownIsoT a, HaveCommonTypeCtor b a) =>
TypeDocMichelsonRep b
concreteTypeDocMichelsonRep @(View_ MText Integer)

instance {-# OVERLAPPABLE #-} (Buildable a, HasNoOpToT r) => Buildable (View_ a r) where
  build :: View_ a r -> Markdown
build = (a -> Markdown) -> View_ a r -> Markdown
forall r a.
HasNoOpToT r =>
(a -> Markdown) -> View_ a r -> Markdown
buildView_ a -> Markdown
forall p. Buildable p => p -> Markdown
build

instance {-# OVERLAPPING  #-} (HasNoOpToT r) => Buildable (View_ () r) where
  build :: View_ () r -> Markdown
build = (() -> Markdown) -> View_ () r -> Markdown
forall r a.
HasNoOpToT 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 Markdown
"()"

buildViewTuple_ :: (HasNoOpToT r, TupleF a) => View_ a r -> Builder
buildViewTuple_ :: forall r a. (HasNoOpToT r, TupleF a) => View_ a r -> Markdown
buildViewTuple_ = (a -> Markdown) -> View_ a r -> Markdown
forall r a.
HasNoOpToT r =>
(a -> Markdown) -> View_ a r -> Markdown
buildView_ a -> Markdown
forall a. TupleF a => a -> Markdown
tupleF

buildView_ :: (HasNoOpToT r) => (a -> Builder) -> View_ a r -> Builder
buildView_ :: forall r a.
HasNoOpToT r =>
(a -> Markdown) -> View_ a r -> Markdown
buildView_ a -> Markdown
bfp (View_ {a
ContractRef r
viewCallbackTo :: ContractRef r
viewParam :: a
viewCallbackTo :: forall a r. View_ a r -> ContractRef r
viewParam :: forall a r. View_ a r -> a
..}) =
  Markdown
"(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
|+ Markdown
" callbackTo: " Markdown -> Markdown -> Markdown
forall b. FromBuilder b => Markdown -> Markdown -> b
+| ContractRef r
viewCallbackTo ContractRef r -> Markdown -> Markdown
forall a b. (Buildable a, FromBuilder b) => a -> Markdown -> b
|+ Markdown
")"

-- | Polymorphic version of 'View_' constructor.
mkView_ :: ToContractRef r contract => a -> contract -> View_ a r
mkView_ :: forall r contract a.
ToContractRef r contract =>
a -> contract -> View_ a r
mkView_ a
a 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_ :: forall a r (s :: [Type]).
((a, ContractRef r) : s) :-> (View_ a r : s)
wrapView_ = ((a, ContractRef r) : s) :-> (View_ a r : s)
forall a b (s :: [Type]).
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_ :: forall a r (s :: [Type]).
(View_ a r : s) :-> ((a, ContractRef r) : s)
unwrapView_ = (View_ a r : s) :-> ((a, ContractRef r) : s)
forall a b (s :: [Type]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_

view_ ::
     (NiceParameter r, Dupable storage, IsNotInView)
  => (forall s0. a : storage : s0 :-> r : s0)
  -> View_ a r : storage : s :-> (List Operation, storage) : s
view_ :: forall r storage a (s :: [Type]).
(NiceParameter r, Dupable storage, IsNotInView) =>
(forall (s0 :: [Type]). (a : storage : s0) :-> (r : s0))
-> (View_ a r : storage : s) :-> ((List Operation, storage) : s)
view_ forall (s0 :: [Type]). (a : storage : s0) :-> (r : s0)
code =
  (View_ a r : storage : s) :-> ((a, ContractRef r) : storage : s)
forall a r (s :: [Type]).
(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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  ((a, ContractRef r) : storage : s)
:-> (a : ContractRef r : storage : s)
forall a b (s :: [Type]). ((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 :: [Type]) (b :: [Type]) (c :: [Type]).
(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 :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (forall (n :: Nat) a (inp :: [Type]) (out :: [Type]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : storage : ContractRef r : storage : s)
:-> (r : ContractRef r : storage : s)
forall (s0 :: [Type]). (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 :: [Type]) (b :: [Type]) (c :: [Type]).
(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 :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (ContractRef r : storage : s)
:-> (Mutez : ContractRef r : storage : s)
forall (s :: [Type]). 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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  (r : Mutez : ContractRef r : storage : s)
:-> (Operation : storage : s)
forall p (s :: [Type]).
(NiceParameter p, IsNotInView) =>
(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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Operation : storage : s)
:-> (List Operation : Operation : storage : s)
forall p (s :: [Type]). 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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (List Operation : Operation : storage : s)
:-> (Operation : List Operation : storage : s)
forall a b (s :: [Type]). (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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Operation : List Operation : storage : s)
:-> (List Operation : storage : s)
forall a (s :: [Type]). (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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (List Operation : storage : s) :-> ((List Operation, storage) : s)
forall a b (s :: [Type]). (a : b : s) :-> ((a, b) : s)
pair

-- | @void@ type synonym as described in A1.
data Void_ (a :: Type) (b :: Type) = Void_
  { forall a b. Void_ a b -> a
voidParam :: a
    -- ^ Entry point argument.
  , forall a b. 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 (WellTypedToT r, WellTypedToT a) => IsoValue (Void_ a r)

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

instance HasRPCRepr a => HasRPCRepr (Void_ a r) where
  type AsRPC (Void_ a r) = Void_ (AsRPC a) r

instance Each [Typeable, TypeHasDoc] [a, r] => TypeHasDoc (Void_ a r) where
  typeDocName :: Proxy (Void_ a r) -> Text
typeDocName Proxy (Void_ a r)
_ = Text
"Void"
  typeDocMdDescription :: Markdown
typeDocMdDescription =
    Markdown
"`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 Proxy (Void_ a r)
tp =
    -- Avoiding trailing underscore
    (Text, DType) -> [DType] -> WithinParens -> Markdown
customTypeDocMdReference
      (Text
"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 (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)
      , Proxy r -> DType
forall a. TypeHasDoc a => Proxy a -> DType
DType (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @r)

        -- for examples
      , Proxy MText -> DType
forall a. TypeHasDoc a => Proxy a -> DType
DType (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @MText)
      , Proxy Integer -> DType
forall a. TypeHasDoc a => Proxy a -> DType
DType (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Integer)
      ]
  typeDocDependencies :: Proxy (Void_ a r) -> [SomeDocDefinitionItem]
typeDocDependencies 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
<>
    [forall t. TypeHasDoc t => SomeDocDefinitionItem
dTypeDep @(), forall t. TypeHasDoc t => SomeDocDefinitionItem
dTypeDep @Integer]
  typeDocHaskellRep :: TypeDocHaskellRep (Void_ a r)
typeDocHaskellRep Proxy (Void_ a r)
p FieldDescriptionsV
descr = do
    (Maybe DocTypeRepLHS
_, ADTRep SomeTypeWithDoc
rhs) <- TypeDocHaskellRep (Void_ a r) -> TypeDocHaskellRep (Void_ a r)
forall a. TypeDocHaskellRep a -> TypeDocHaskellRep a
haskellRepNoFields (forall a b.
(Typeable a, GenericIsoValue a, GTypeHasDoc (Rep a),
 HaveCommonTypeCtor b a) =>
TypeDocHaskellRep b
concreteTypeDocHaskellRep @(Void_ MText Integer)) Proxy (Void_ a r)
p FieldDescriptionsV
descr
    (Maybe DocTypeRepLHS, ADTRep SomeTypeWithDoc)
-> Maybe (Maybe DocTypeRepLHS, ADTRep SomeTypeWithDoc)
forall (m :: Type -> Type) a. Monad m => a -> m a
return (DocTypeRepLHS -> Maybe DocTypeRepLHS
forall a. a -> Maybe a
Just DocTypeRepLHS
"Void MText Integer", ADTRep SomeTypeWithDoc
rhs)
  typeDocMichelsonRep :: TypeDocMichelsonRep (Void_ a r)
typeDocMichelsonRep Proxy (Void_ a r)
p =
    let (Maybe DocTypeRepLHS
_, T
rhs) = forall a b.
(Typeable a, KnownIsoT a, HaveCommonTypeCtor b a) =>
TypeDocMichelsonRep b
forall {k} a (b :: k).
(Typeable a, KnownIsoT a, HaveCommonTypeCtor b a) =>
TypeDocMichelsonRep b
concreteTypeDocMichelsonRep @(Void_ MText Integer) Proxy (Void_ a r)
p
    in (DocTypeRepLHS -> Maybe DocTypeRepLHS
forall a. a -> Maybe a
Just DocTypeRepLHS
"Void MText Integer", T
rhs)

instance Buildable a => Buildable (Void_ a b) where
  build :: Void_ a b -> Markdown
build Void_ {a
Lambda b b
voidResProxy :: Lambda b b
voidParam :: a
voidResProxy :: forall a b. Void_ a b -> Lambda b b
voidParam :: forall a b. Void_ a b -> a
..} = Markdown
"(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
|+ Markdown
")"

-- | 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 { forall r. 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 = forall e. IsError e => Markdown
typeDocMdDescriptionReferToError @(VoidResult r)
  typeDocMdReference :: Proxy (VoidResult r) -> WithinParens -> Markdown
typeDocMdReference = Proxy (VoidResult r) -> WithinParens -> Markdown
forall (t :: Type -> Type) r a.
(r ~ t a, Typeable t, Each '[TypeHasDoc] '[r, a],
 IsHomomorphic t) =>
Proxy r -> WithinParens -> Markdown
poly1TypeDocMdReference
  typeDocHaskellRep :: TypeDocHaskellRep (VoidResult r)
typeDocHaskellRep = forall a b.
(Typeable a, GenericIsoValue a, GTypeHasDoc (Rep a)) =>
TypeDocHaskellRep b
unsafeConcreteTypeDocHaskellRep @(VoidResultRep Integer)
  typeDocMichelsonRep :: TypeDocMichelsonRep (VoidResult r)
typeDocMichelsonRep = forall a b. (Typeable a, KnownIsoT a) => TypeDocMichelsonRep b
forall {k} a (b :: k).
(Typeable a, KnownIsoT a) =>
TypeDocMichelsonRep b
unsafeConcreteTypeDocMichelsonRep @(VoidResultRep Integer)

instance (NiceConstant r, ErrorHasDoc (VoidResult r)) =>
         IsError (VoidResult r) where
  errorToVal :: forall r.
VoidResult r
-> (forall (t :: T). ErrorScope t => Value t -> r) -> r
errorToVal (VoidResult r
e) 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 (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
$
    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 :: forall (t :: T). SingI t => Value t -> Either Text (VoidResult r)
errorFromVal Value t
fullErr =
    Value t -> Either Text (VoidResultRep r)
forall (t :: T) e.
(SingI t, KnownIsoT 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 :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \((MText
tag, 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 :: Type -> Type) 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
$ Text
"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 = Text
"VoidResult"
  errorDocMdCause :: Markdown
errorDocMdCause =
    Markdown
"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 -> 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 -> Markdown
forall a. Semigroup a => a -> a -> a
<> Markdown
"<return value>" Markdown -> Markdown -> Markdown
forall a. Semigroup a => a -> a -> a
<> Markdown
")")
  errorDocDependencies :: [SomeDocDefinitionItem]
errorDocDependencies =
    [forall t. TypeHasDoc t => SomeDocDefinitionItem
dTypeDep @MText, forall t. TypeHasDoc t => SomeDocDefinitionItem
dTypeDep @r]

instance
  ( WellTypedToT (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 Text
"impossible"
  fromVal :: Value (ToT (VoidResult r)) -> VoidResult r
fromVal = Text -> Value (TypeError ...) -> VoidResult r
forall a. HasCallStack => Text -> a
error Text
"impossible"

mkVoid :: forall b a. a -> Void_ a b
mkVoid :: forall b a. a -> Void_ a b
mkVoid a
a = a -> Lambda b b -> Void_ a b
forall a b. a -> Lambda b b -> Void_ a b
Void_ a
a ((IsNotInView => '[b] :-> '[b]) -> Lambda b b
forall (i :: [Type]) (o :: [Type]).
(IsNotInView => i :-> o) -> WrappedLambda i o
mkLambda IsNotInView => '[b] :-> '[b]
forall (s :: [Type]). s :-> s
nop)

void_
  :: forall a b s s' anything.
      (IsError (VoidResult b), NiceConstant b)
  => a : s :-> b : s' -> Void_ a b : s :-> anything
void_ :: forall a b (s :: [Type]) (s' :: [Type]) (anything :: [Type]).
(IsError (VoidResult b), NiceConstant b) =>
((a : s) :-> (b : s')) -> (Void_ a b : s) :-> anything
void_ (a : s) :-> (b : s')
code =
  DThrows -> (Void_ a b : s) :-> (Void_ a b : s)
forall di (s :: [Type]). DocItem di => di -> s :-> s
doc (Proxy (VoidResult b) -> DThrows
forall e. ErrorHasDoc e => Proxy e -> DThrows
DThrows (forall {t}. Proxy t
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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  (Void_ a b : s) :-> ((a, Lambda b b) : s)
forall a b (s :: [Type]). (Void_ a b : s) :-> ((a, Lambda b b) : s)
unwrapVoid ((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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  ((a, Lambda b b) : s) :-> (a : Lambda b b : s)
forall a b (s :: [Type]). ((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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : Lambda b b : s) :-> (Lambda b b : a : s)
forall a b (s :: [Type]). (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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a : s) :-> (b : s'))
-> (Lambda b b : a : s) :-> (Lambda b b : b : s')
forall a (s :: [Type]) (s' :: [Type]).
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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Lambda b b : b : s') :-> (b : Lambda b b : s')
forall a b (s :: [Type]). (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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (b : Lambda b b : s') :-> (b : s')
forall a b (s :: [Type]). (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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  MText -> (b : s') :-> (MText : b : s')
forall t (s :: [Type]). 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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (MText : b : s') :-> ((MText, b) : s')
forall a b (s :: [Type]). (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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall a (s :: [Type]) (t :: [Type]).
NiceConstant 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 :: forall a b (s :: [Type]). ((a, Lambda b b) : s) :-> (Void_ a b : s)
wrapVoid = ((a, Lambda b b) : s) :-> (Void_ a b : s)
forall a b (s :: [Type]).
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 :: forall a b (s :: [Type]). (Void_ a b : s) :-> ((a, Lambda b b) : s)
unwrapVoid = (Void_ a b : s) :-> ((a, Lambda b b) : s)
forall a b (s :: [Type]).
MichelsonCoercible a b =>
(a : s) :-> (b : s)
forcedCoerce_

addressToEpAddress :: Address : s :-> EpAddress : s
addressToEpAddress :: forall (s :: [Type]). (Address : s) :-> (EpAddress : s)
addressToEpAddress = (Address : s) :-> (EpAddress : s)
forall a b (s :: [Type]).
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 arg (s :: [Type]).
NiceParameter arg =>
(forall (s0 :: [Type]). (FutureContract arg : s) :-> s0)
-> ContractRef arg -> s :-> (ContractRef arg : s)
pushContractRef forall (s0 :: [Type]). (FutureContract arg : s) :-> s0
onContractNotFound (ContractRef arg
contractRef :: ContractRef arg) =
  (NiceParameter 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 (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 :: [Type]). 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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (FutureContract arg : s)
:-> (FutureContract arg : FutureContract arg : s)
forall a (s :: [Type]). Dupable a => (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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
#
    (FutureContract arg : FutureContract arg : s)
:-> (Maybe (ContractRef arg) : FutureContract arg : s)
forall p (s :: [Type]).
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 :: [Type]) (b :: [Type]) (c :: [Type]).
(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 :: [Type]) (s' :: [Type]) a.
(s :-> s') -> ((a : s) :-> s') -> (Maybe a : s) :-> s'
ifNone (FutureContract arg : s) :-> (ContractRef arg : s)
forall (s0 :: [Type]). (FutureContract arg : s) :-> s0
onContractNotFound (((FutureContract arg : s) :-> s)
-> (ContractRef arg : FutureContract arg : s)
   :-> (ContractRef arg : s)
forall a (s :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (FutureContract arg : s) :-> s
forall a (s :: [Type]). (a : s) :-> s
drop)

-- | Duplicate two topmost items on top of the stack.
dupTop2
  :: forall (a :: Type) (b :: Type) (s :: [Type]).
     (Dupable a, Dupable b)
  => a ': b ': s :-> a ': b ': a ': b ': s
dupTop2 :: forall a b (s :: [Type]).
(Dupable a, Dupable b) =>
(a : b : s) :-> (a : b : a : b : s)
dupTop2 = forall (n :: Nat) a (inp :: [Type]) (out :: [Type]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @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 :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall (n :: Nat) a (inp :: [Type]) (out :: [Type]).
(ConstraintDUPNLorentz (ToPeano n) inp out a, Dupable a) =>
inp :-> out
dupN @2

fromOption
  :: (NiceConstant a)
  => a -> Maybe a : s :-> a : s
fromOption :: forall a (s :: [Type]).
NiceConstant a =>
a -> (Maybe a : s) :-> (a : s)
fromOption a
a = ((a : s) :-> (a : s))
-> (s :-> (a : s)) -> (Maybe a : s) :-> (a : s)
forall a (s :: [Type]) (s' :: [Type]).
((a : s) :-> s') -> (s :-> s') -> (Maybe a : s) :-> s'
ifSome (a : s) :-> (a : s)
forall (s :: [Type]). s :-> s
nop (a -> s :-> (a : s)
forall t (s :: [Type]). NiceConstant t => t -> s :-> (t : s)
push a
a)

isSome :: Maybe a : s :-> Bool : s
isSome :: forall a (s :: [Type]). (Maybe a : s) :-> (Bool : s)
isSome = ((a : s) :-> (Bool : s))
-> (s :-> (Bool : s)) -> (Maybe a : s) :-> (Bool : s)
forall a (s :: [Type]) (s' :: [Type]).
((a : s) :-> s') -> (s :-> s') -> (Maybe a : s) :-> s'
ifSome ((a : s) :-> s
forall a (s :: [Type]). (a : s) :-> s
drop ((a : s) :-> s) -> (s :-> (Bool : s)) -> (a : s) :-> (Bool : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# Bool -> s :-> (Bool : s)
forall t (s :: [Type]). NiceConstant t => t -> s :-> (t : s)
push Bool
True) (Bool -> s :-> (Bool : s)
forall t (s :: [Type]). NiceConstant t => t -> s :-> (t : s)
push Bool
False)

-- | Retain the value if it is not equal to the given one.
--
-- >>> non 0 -$ 5
-- Just 5
-- >>> non 0 -$ 0
-- Nothing
non
  :: (NiceConstant a, NiceComparable a)
  => a -> a : s :-> Maybe a : s
non :: forall a (s :: [Type]).
(NiceConstant a, NiceComparable a) =>
a -> (a : s) :-> (Maybe a : s)
non a
a = ('[a] :-> '[Bool]) -> (a : s) :-> (Maybe a : s)
forall a (s :: [Type]).
NiceConstant a =>
('[a] :-> '[Bool]) -> (a : s) :-> (Maybe a : s)
non' (a -> '[a] :-> '[a, a]
forall t (s :: [Type]). NiceConstant t => t -> s :-> (t : s)
push a
a ('[a] :-> '[a, a]) -> ('[a, a] :-> '[Bool]) -> '[a] :-> '[Bool]
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# '[a, a] :-> '[Bool]
forall n (s :: [Type]).
NiceComparable n =>
(n : n : s) :-> (Bool : s)
eq)

-- | Version of 'non' with a custom predicate.
--
-- >>> non' eq0 -$ 5
-- Just 5
-- >>> non' eq0 -$ 0
-- Nothing
non'
  :: (NiceConstant a)
  => ('[a] :-> '[Bool]) -> a : s :-> Maybe a : s
non' :: forall a (s :: [Type]).
NiceConstant a =>
('[a] :-> '[Bool]) -> (a : s) :-> (Maybe a : s)
non' '[a] :-> '[Bool]
p = (a : s) :-> (a : a : s)
forall a (s :: [Type]). Dupable a => (a : s) :-> (a : a : s)
dup ((a : s) :-> (a : a : s))
-> ((a : a : s) :-> (Bool : a : s)) -> (a : s) :-> (Bool : a : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ('[a] :-> '[Bool]) -> ('[a] ++ (a : s)) :-> ('[Bool] ++ (a : s))
forall (s :: [Type]) (i :: [Type]) (o :: [Type]).
(KnownList i, KnownList o) =>
(i :-> o) -> (i ++ s) :-> (o ++ s)
framed '[a] :-> '[Bool]
p ((a : s) :-> (Bool : a : s))
-> ((Bool : a : s) :-> (Maybe a : s)) -> (a : s) :-> (Maybe a : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((a : s) :-> (Maybe a : s))
-> ((a : s) :-> (Maybe a : s)) -> (Bool : a : s) :-> (Maybe a : s)
forall (s :: [Type]) (s' :: [Type]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ ((a : s) :-> s
forall a (s :: [Type]). (a : s) :-> s
drop ((a : s) :-> s)
-> (s :-> (Maybe a : s)) -> (a : s) :-> (Maybe a : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# s :-> (Maybe a : s)
forall a (s :: [Type]). KnownValue a => s :-> (Maybe a : s)
none) (a : s) :-> (Maybe a : s)
forall a (s :: [Type]). (a : s) :-> (Maybe a : s)
some

-- | Check whether container is empty.
isEmpty :: SizeOpHs c => c : s :-> Bool : s
isEmpty :: forall c (s :: [Type]). SizeOpHs c => (c : s) :-> (Bool : s)
isEmpty = (c : s) :-> (Natural : s)
forall c (s :: [Type]). SizeOpHs c => (c : s) :-> (Natural : s)
size ((c : s) :-> (Natural : s))
-> ((Natural : s) :-> (Integer : s)) -> (c : s) :-> (Integer : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : s) :-> (Integer : s)
forall i (s :: [Type]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int ((c : s) :-> (Integer : s))
-> ((Integer : s) :-> (Bool : s)) -> (c : s) :-> (Bool : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : s) :-> (Bool : s)
forall n (s :: [Type]).
UnaryArithOpHs Eq' n =>
(n : s) :-> (UnaryArithResHs Eq' n : s)
eq0

class NonZero t where
  -- | Retain the value only if it is not zero.
  nonZero :: t : s :-> Maybe t : s

instance NonZero Integer where
  nonZero :: forall (s :: [Type]). (Integer : s) :-> (Maybe Integer : s)
nonZero = (Integer : s) :-> (Integer : Integer : s)
forall a (s :: [Type]). Dupable a => (a : s) :-> (a : a : s)
dup ((Integer : s) :-> (Integer : Integer : s))
-> ((Integer : Integer : s) :-> (Bool : Integer : s))
-> (Integer : s) :-> (Bool : Integer : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Integer : s) :-> (Bool : Integer : s)
forall n (s :: [Type]).
UnaryArithOpHs Eq' n =>
(n : s) :-> (UnaryArithResHs Eq' n : s)
eq0 ((Integer : s) :-> (Bool : Integer : s))
-> ((Bool : Integer : s) :-> (Maybe Integer : s))
-> (Integer : s) :-> (Maybe Integer : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((Integer : s) :-> (Maybe Integer : s))
-> ((Integer : s) :-> (Maybe Integer : s))
-> (Bool : Integer : s) :-> (Maybe Integer : s)
forall (s :: [Type]) (s' :: [Type]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ ((Integer : s) :-> s
forall a (s :: [Type]). (a : s) :-> s
drop ((Integer : s) :-> s)
-> (s :-> (Maybe Integer : s))
-> (Integer : s) :-> (Maybe Integer : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# s :-> (Maybe Integer : s)
forall a (s :: [Type]). KnownValue a => s :-> (Maybe a : s)
none) (Integer : s) :-> (Maybe Integer : s)
forall a (s :: [Type]). (a : s) :-> (Maybe a : s)
some

instance NonZero Natural where
  nonZero :: forall (s :: [Type]). (Natural : s) :-> (Maybe Natural : s)
nonZero = (Natural : s) :-> (Natural : Natural : s)
forall a (s :: [Type]). Dupable a => (a : s) :-> (a : a : s)
dup ((Natural : s) :-> (Natural : Natural : s))
-> ((Natural : Natural : s) :-> (Integer : Natural : s))
-> (Natural : s) :-> (Integer : Natural : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Natural : s) :-> (Integer : Natural : s)
forall i (s :: [Type]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int ((Natural : s) :-> (Integer : Natural : s))
-> ((Integer : Natural : s) :-> (Bool : Natural : s))
-> (Natural : s) :-> (Bool : Natural : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Natural : s) :-> (Bool : Natural : s)
forall n (s :: [Type]).
UnaryArithOpHs Eq' n =>
(n : s) :-> (UnaryArithResHs Eq' n : s)
eq0 ((Natural : s) :-> (Bool : Natural : s))
-> ((Bool : Natural : s) :-> (Maybe Natural : s))
-> (Natural : s) :-> (Maybe Natural : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((Natural : s) :-> (Maybe Natural : s))
-> ((Natural : s) :-> (Maybe Natural : s))
-> (Bool : Natural : s) :-> (Maybe Natural : s)
forall (s :: [Type]) (s' :: [Type]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ ((Natural : s) :-> s
forall a (s :: [Type]). (a : s) :-> s
drop ((Natural : s) :-> s)
-> (s :-> (Maybe Natural : s))
-> (Natural : s) :-> (Maybe Natural : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# s :-> (Maybe Natural : s)
forall a (s :: [Type]). KnownValue a => s :-> (Maybe a : s)
none) (Natural : s) :-> (Maybe Natural : s)
forall a (s :: [Type]). (a : s) :-> (Maybe a : s)
some

instance (NiceComparable d) => NonZero (Ticket d) where
  nonZero :: forall (s :: [Type]). (Ticket d : s) :-> (Maybe (Ticket d) : s)
nonZero =
    (Ticket d : s) :-> (ReadTicket d : Ticket d : s)
forall a (s :: [Type]).
(Ticket a : s) :-> (ReadTicket a : Ticket a : s)
readTicket ((Ticket d : s) :-> (ReadTicket d : Ticket d : s))
-> ((ReadTicket d : Ticket d : s) :-> (Natural : Ticket d : s))
-> (Ticket d : s) :-> (Natural : Ticket d : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label "rtAmount"
-> (ReadTicket d : Ticket d : s)
   :-> (GetFieldType (ReadTicket d) "rtAmount" : Ticket d : s)
forall dt (name :: Symbol) (st :: [Type]).
InstrGetFieldC dt name =>
Label name -> (dt : st) :-> (GetFieldType dt name : st)
toField IsLabel "rtAmount" (Label "rtAmount")
Label "rtAmount"
#rtAmount ((Ticket d : s) :-> (Natural : Ticket d : s))
-> ((Natural : Ticket d : s) :-> (Integer : Ticket d : s))
-> (Ticket d : s) :-> (Integer : Ticket d : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Natural : Ticket d : s) :-> (Integer : Ticket d : s)
forall i (s :: [Type]).
ToIntegerArithOpHs i =>
(i : s) :-> (Integer : s)
int ((Ticket d : s) :-> (Integer : Ticket d : s))
-> ((Integer : Ticket d : s) :-> (Bool : Ticket d : s))
-> (Ticket d : s) :-> (Bool : Ticket d : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (Integer : Ticket d : s) :-> (Bool : Ticket d : s)
forall n (s :: [Type]).
UnaryArithOpHs Eq' n =>
(n : s) :-> (UnaryArithResHs Eq' n : s)
eq0 ((Ticket d : s) :-> (Bool : Ticket d : s))
-> ((Bool : Ticket d : s) :-> (Maybe (Ticket d) : s))
-> (Ticket d : s) :-> (Maybe (Ticket d) : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# ((Ticket d : s) :-> (Maybe (Ticket d) : s))
-> ((Ticket d : s) :-> (Maybe (Ticket d) : s))
-> (Bool : Ticket d : s) :-> (Maybe (Ticket d) : s)
forall (s :: [Type]) (s' :: [Type]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ ((Ticket d : s) :-> s
forall a (s :: [Type]). (a : s) :-> s
drop ((Ticket d : s) :-> s)
-> (s :-> (Maybe (Ticket d) : s))
-> (Ticket d : s) :-> (Maybe (Ticket d) : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# s :-> (Maybe (Ticket d) : s)
forall a (s :: [Type]). KnownValue a => s :-> (Maybe a : s)
none) (Ticket d : s) :-> (Maybe (Ticket d) : s)
forall a (s :: [Type]). (a : s) :-> (Maybe a : s)
some

type instance ErrorArg "no_view" = MText
instance CustomErrorHasDoc "no_view" where
  customErrClass :: ErrorClass
customErrClass = ErrorClass
ErrClassBadArgument
  customErrDocMdCause :: Markdown
customErrDocMdCause =
    Markdown
"Failed to call on-chain view. \
    \Check whether the view with the given name exists in the called contract, \
    \and that argument and return types match the expected ones."
  customErrArgumentSemantics :: Maybe Markdown
customErrArgumentSemantics = Markdown -> Maybe Markdown
forall a. a -> Maybe a
Just Markdown
"view name"

-- | Call a view.
--
-- Accepts the view name via a type annotation.
-- This internally asserts the view to be present, as if the supplied
-- @TAddress@ argument is valid, the view is guaranteed to be called
-- successfully.
view
  :: forall name arg ret p vd s.
    ( HasCallStack, KnownSymbol name, KnownValue arg
    , NiceViewable ret, HasView vd name arg ret
    )
  => arg : TAddress p vd : s :-> ret : s
view :: forall (name :: Symbol) arg ret p vd (s :: [Type]).
(HasCallStack, KnownSymbol name, KnownValue arg, NiceViewable ret,
 HasView vd name arg ret) =>
(arg : TAddress p vd : s) :-> (ret : s)
view =
  ((TAddress p vd : s) :-> (Address : s))
-> (arg : TAddress p vd : s) :-> (arg : Address : s)
forall a (s :: [Type]) (s' :: [Type]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip (TAddress p vd : s) :-> (Address : s)
forall a b (s :: [Type]). Castable_ a b => (a : s) :-> (b : s)
checkedCoerce_ ((arg : TAddress p vd : s) :-> (arg : Address : s))
-> ((arg : Address : s) :-> (Maybe ret : s))
-> (arg : TAddress p vd : s) :-> (Maybe ret : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# forall (name :: Symbol) ret arg (s :: [Type]).
(HasCallStack, KnownSymbol name, KnownValue arg,
 NiceViewable ret) =>
(arg : Address : s) :-> (Maybe ret : s)
view' @name ((arg : TAddress p vd : s) :-> (Maybe ret : s))
-> ((Maybe ret : s) :-> (ret : s))
-> (arg : TAddress p vd : s) :-> (ret : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
#
  ((ret : s) :-> (ret : s))
-> (s :-> (ret : s)) -> (Maybe ret : s) :-> (ret : s)
forall a (s :: [Type]) (s' :: [Type]).
((a : s) :-> s') -> (s :-> s') -> (Maybe a : s) :-> s'
ifSome (ret : s) :-> (ret : s)
forall (s :: [Type]). s :-> s
nop (MText -> s :-> (MText : s)
forall t (s :: [Type]). NiceConstant t => t -> s :-> (t : s)
push (ViewName -> MText
viewNameToMText ViewName
viewName) (s :-> (MText : s))
-> ((MText : s) :-> (ret : s)) -> s :-> (ret : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# Label "no_view" -> (MText : s) :-> (ret : s)
forall (tag :: Symbol) err (s :: [Type]) (any :: [Type]).
(MustHaveErrorArg tag (MText, err), CustomErrorHasDoc tag,
 KnownError err) =>
Label tag -> (err : s) :-> any
failCustom IsLabel "no_view" (Label "no_view")
Label "no_view"
#no_view)
  (ViewableScope (ToT ret) =>
 (arg : TAddress p vd : s) :-> (ret : s))
-> (NiceViewable ret :- ViewableScope (ToT ret))
-> (arg : TAddress p vd : s) :-> (ret : s)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall a. NiceViewable a :- ViewableScope (ToT a)
niceViewableEvi @ret
  where
    viewName :: ViewName
viewName = forall (name :: Symbol).
(KnownSymbol name, HasCallStack) =>
ViewName
demoteViewName @name
    _needHasView :: Dict (HasView vd name arg ret)
_needHasView = forall (a :: Constraint). a => Dict a
Dict @(HasView vd name arg ret)

-- | Michelson supports only `EDiv`, which gives both the quotient and the
-- remainder for integers. For convenience, we also offer `IDiv`, which gives
-- just the quotient.
data IDiv

instance (ArithOpHs EDiv n d (Maybe (q, r)), mq ~ Maybe q, KnownValue q) => ArithOpHs IDiv n d mq where
  evalArithOpHs :: forall (s :: [Type]). (n : d : s) :-> (mq : s)
evalArithOpHs = forall aop n m r (s :: [Type]).
ArithOpHs aop n m r =>
(n : m : s) :-> (r : s)
evalArithOpHs @EDiv @n @d @(Maybe (q, r)) ((n : d : s) :-> (Maybe (q, r) : s))
-> ((Maybe (q, r) : s) :-> (Maybe q : s))
-> (n : d : s) :-> (Maybe q : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (((q, r) : s) :-> (q : s)) -> (Maybe (q, r) : s) :-> (Maybe q : s)
forall (c :: Type -> Type) b a (s :: [Type]).
(LorentzFunctor c, KnownValue b) =>
((a : s) :-> (b : s)) -> (c a : s) :-> (c b : s)
lmap ((q, r) : s) :-> (q : s)
forall a b (s :: [Type]). ((a, b) : s) :-> (a : s)
car

-- | Integer division.
--
-- >>> idiv -$ (5 :: Integer) ::: (2 :: Integer)
-- Just 2
--
-- >>> idiv -$ (5 :: Integer) ::: (0 :: Integer)
-- Nothing
idiv
  :: ArithOpHs IDiv n d q
  => n : d : s :-> q : s
idiv :: forall n d q (s :: [Type]).
ArithOpHs IDiv n d q =>
(n : d : s) :-> (q : s)
idiv = forall aop n m r (s :: [Type]).
ArithOpHs aop n m r =>
(n : m : s) :-> (r : s)
evalArithOpHs @IDiv

-- | Michelson supports only `EDiv`, which gives both the quotient and the
-- remainder for integers. For convenience, we also offer `IMod`, which gives
-- just the remainder.
data IMod

instance (ArithOpHs EDiv n d (Maybe (q, r)), mr ~ Maybe r, KnownValue r) => ArithOpHs IMod n d mr where
  evalArithOpHs :: forall (s :: [Type]). (n : d : s) :-> (mr : s)
evalArithOpHs = forall aop n m r (s :: [Type]).
ArithOpHs aop n m r =>
(n : m : s) :-> (r : s)
evalArithOpHs @EDiv @n @d @(Maybe (q, r)) ((n : d : s) :-> (Maybe (q, r) : s))
-> ((Maybe (q, r) : s) :-> (Maybe r : s))
-> (n : d : s) :-> (Maybe r : s)
forall (a :: [Type]) (b :: [Type]) (c :: [Type]).
(a :-> b) -> (b :-> c) -> a :-> c
# (((q, r) : s) :-> (r : s)) -> (Maybe (q, r) : s) :-> (Maybe r : s)
forall (c :: Type -> Type) b a (s :: [Type]).
(LorentzFunctor c, KnownValue b) =>
((a : s) :-> (b : s)) -> (c a : s) :-> (c b : s)
lmap ((q, r) : s) :-> (r : s)
forall a b (s :: [Type]). ((a, b) : s) :-> (b : s)
cdr

-- | Integer modulus.
--
-- >>> imod -$ (5 :: Integer) ::: (2 :: Integer)
-- Just 1
--
-- >>> imod -$ (5 :: Integer) ::: (0 :: Integer)
-- Nothing
imod
  :: ArithOpHs IMod n d r
  => n : d : s :-> r : s
imod :: forall n d r (s :: [Type]).
ArithOpHs IMod n d r =>
(n : d : s) :-> (r : s)
imod = forall aop n m r (s :: [Type]).
ArithOpHs aop n m r =>
(n : m : s) :-> (r : s)
evalArithOpHs @IMod