{-# LANGUAGE NoStarIsType #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
module Lorentz.Macro
(
NiceComparable
, eq
, neq
, lt
, gt
, le
, ge
, ifEq0
, ifGe0
, ifGt0
, ifLe0
, ifLt0
, ifNeq0
, ifEq
, ifGe
, ifGt
, ifLe
, ifLt
, ifNeq
, fail_
, assert
, assertEq0
, assertNeq0
, assertLt0
, assertGt0
, assertLe0
, assertGe0
, assertEq
, assertNeq
, assertLt
, assertGt
, assertLe
, assertGe
, assertNone
, assertSome
, assertLeft
, assertRight
, assertUsing
, 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
, View_ (..)
, Void_ (..)
, VoidResult(..)
, view_
, mkView_
, wrapView_
, unwrapView_
, void_
, mkVoid
, wrapVoid
, unwrapVoid
, voidResultTag
, dupTop2
, fromOption
, isSome
, non
, non'
, isEmpty
, NonZero (..)
, buildView_
, buildViewTuple_
, addressToEpAddress
, pushContractRef
, selfAddress
, view
, IDiv
, IMod
, idiv
, imod
) where
import Prelude hiding (and, compare, drop, some, swap, view)
import Data.Constraint (Bottom(..))
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
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
{-# 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
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
type ErrInstr s = forall serr. s :-> serr
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
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)
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
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 :: 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 :: 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 :: (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 :: (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 :: ((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 :: ((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 :: (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 :: (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
:: (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
:: (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 :: (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
:: (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_ :: (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_ :: (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 :: (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 :: (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
class MapInstrs map where
mapUpdate :: NiceComparable k => k : Maybe v : map k v : s :-> map k v : s
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
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
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)
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
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)
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
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
)
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 =
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 : Head s : (LazyTake n (Tail s) ++ tail)))
-> ((a : Head s : (LazyTake n (Tail s) ++ tail)) :-> 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)
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
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)
)
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 =
forall (n :: Peano) (inp :: [Type]) (out :: [Type]) a.
ConstraintDUGLorentz n inp out a =>
inp :-> out
dugPeano @('S ('S n)) ((a : s)
:-> (Head mid
: Head (Tail mid)
: (LazyTake
n (LazyTake n (Tail (Tail mid)) ++ Drop ('S ('S ('S n))) mid)
++ (a : Drop
n (LazyTake n (Tail (Tail mid)) ++ Drop ('S ('S ('S n))) mid)))))
-> ((Head mid
: Head (Tail mid)
: (LazyTake
n (LazyTake n (Tail (Tail mid)) ++ Drop ('S ('S ('S n))) mid)
++ (a : Drop
n (LazyTake n (Tail (Tail mid)) ++ Drop ('S ('S ('S n))) 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))
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
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, HasNoNestedBigMaps (ToT 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, HasNoNestedBigMaps (ToT r))
=> Buildable (View_ a r) where
build :: View_ a r -> Markdown
build = (a -> Markdown) -> View_ a r -> Markdown
forall r a.
(HasNoOpToT r, HasNoNestedBigMaps (ToT r)) =>
(a -> Markdown) -> View_ a r -> Markdown
buildView_ a -> Markdown
forall p. Buildable p => p -> Markdown
build
instance {-# OVERLAPPING #-} (HasNoOpToT r, HasNoNestedBigMaps (ToT r)) => Buildable (View_ () r) where
build :: View_ () r -> Markdown
build = (() -> Markdown) -> View_ () r -> Markdown
forall r a.
(HasNoOpToT r, HasNoNestedBigMaps (ToT 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, HasNoNestedBigMaps (ToT r), TupleF a) => View_ a r -> Builder
buildViewTuple_ :: forall r a.
(HasNoOpToT r, HasNoNestedBigMaps (ToT r), TupleF a) =>
View_ a r -> Markdown
buildViewTuple_ = (a -> Markdown) -> View_ a r -> Markdown
forall r a.
(HasNoOpToT r, HasNoNestedBigMaps (ToT r)) =>
(a -> Markdown) -> View_ a r -> Markdown
buildView_ a -> Markdown
forall a. TupleF a => a -> Markdown
tupleF
buildView_ :: (HasNoOpToT r, HasNoNestedBigMaps (ToT r)) => (a -> Builder) -> View_ a r -> Builder
buildView_ :: forall r a.
(HasNoOpToT r, HasNoNestedBigMaps (ToT 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
")"
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)
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_
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
data Void_ (a :: Type) (b :: Type) = Void_
{ forall a b. Void_ a b -> a
voidParam :: a
, forall a b. Void_ a b -> Lambda b b
voidResProxy :: Lambda b b
} 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 =
(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)
, 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 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 =
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
( Bottom
, 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 = forall a. Bottom => a
VoidResult r -> Value (ToT (VoidResult r))
no
fromVal :: Value (ToT (VoidResult r)) -> VoidResult r
fromVal = forall a. Bottom => a
Value (ToT (VoidResult r)) -> VoidResult r
no
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)
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_
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_
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) =
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)
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)
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)
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
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
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"
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)
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)
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)] :-> '[q]) -> (Maybe (q, r) : s) :-> (Maybe q : s)
forall (c :: Type -> Type) a b (s :: [Type]).
(LorentzFunctor c a b, KnownValue b) =>
('[a] :-> '[b]) -> (c a : s) :-> (c b : s)
lmap '[(q, r)] :-> '[q]
forall a b (s :: [Type]). ((a, b) : s) :-> (a : s)
car
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
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)] :-> '[r]) -> (Maybe (q, r) : s) :-> (Maybe r : s)
forall (c :: Type -> Type) a b (s :: [Type]).
(LorentzFunctor c a b, KnownValue b) =>
('[a] :-> '[b]) -> (c a : s) :-> (c b : s)
lmap '[(q, r)] :-> '[r]
forall a b (s :: [Type]). ((a, b) : s) :-> (b : s)
cdr
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