{-# LANGUAGE PartialTypeSignatures #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
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
, dropX
, cloneX
, duupX
, framedN
, caar
, cadr
, cdar
, cddr
, ifRight
, ifSome
, when_
, unless_
, whenSome
, mapCar
, mapCdr
, papair
, ppaiir
, unpair
, setCar
, setCdr
, setInsert
, mapInsert
, setInsertNew
, mapInsertNew
, deleteMap
, setDelete
, View (..)
, Void_ (..)
, VoidResult(..)
, view_
, mkView
, wrapView
, unwrapView
, void_
, mkVoid
, buildView
, buildViewTuple
, addressToEpAddress
, pushContractRef
) where
import Prelude hiding (compare, drop, some, swap)
import qualified Data.Kind as Kind
import Data.Singletons (SingI(..))
import Data.Vinyl.TypeLevel (Nat(..))
import Fmt (Buildable(..), Builder, pretty, tupleF, (+|), (|+))
import Fmt.Internal.Tuple (TupleF)
import GHC.TypeNats (type (-))
import qualified GHC.TypeNats as GHC (Nat)
import Lorentz.Arith
import Lorentz.Base
import Lorentz.Coercions
import Lorentz.Constraints
import Lorentz.Doc
import Lorentz.Errors
import Lorentz.Ext (stackType)
import Lorentz.Instr
import Lorentz.Value
import Michelson.Typed (ConstraintDIG', ConstraintDIPN', T, typeDocDependencies')
import Michelson.Typed.Arith
import Michelson.Typed.Haskell.Value
import Util.Markdown
import Util.Peano
import Util.Type
eq :: NiceComparable n
=> n & n & s :-> Bool & s
eq = compare # eq0
neq :: NiceComparable n
=> n & n & s :-> Bool & s
neq = compare # neq0
gt :: NiceComparable n
=> n & n & s :-> Bool & s
gt = compare # gt0
le :: NiceComparable n
=> n & n & s :-> Bool & s
le = compare # le0
ge :: NiceComparable n
=> n & n & s :-> Bool & s
ge = compare # ge0
lt :: NiceComparable n
=> n & n & s :-> Bool & s
lt = compare # lt0
type IfCmp0Constraints a op =
(UnaryArithOpHs op a, (UnaryArithResHs op a ~ Bool), SingI (ToCT a))
ifEq0
:: (IfCmp0Constraints a Eq')
=> (s :-> s') -> (s :-> s') -> (a & s :-> s')
ifEq0 l r = eq0 # if_ l r
ifNeq0
:: (IfCmp0Constraints a Neq)
=> (s :-> s') -> (s :-> s') -> (a & s :-> s')
ifNeq0 l r = neq0 # if_ l r
ifLt0
:: (IfCmp0Constraints a Lt)
=> (s :-> s') -> (s :-> s') -> (a & s :-> s')
ifLt0 l r = lt0 # if_ l r
ifGt0
:: (IfCmp0Constraints a Gt)
=> (s :-> s') -> (s :-> s') -> (a & s :-> s')
ifGt0 l r = gt0 # if_ l r
ifLe0
:: (IfCmp0Constraints a Le)
=> (s :-> s') -> (s :-> s') -> (a & s :-> s')
ifLe0 l r = le0 # if_ l r
ifGe0
:: (IfCmp0Constraints a Ge)
=> (s :-> s') -> (s :-> s') -> (a & s :-> s')
ifGe0 l r = ge0 # if_ l r
ifEq
:: (NiceComparable a)
=> (s :-> s') -> (s :-> s') -> (a & a & s :-> s')
ifEq l r = eq # if_ l r
ifNeq
:: (NiceComparable a)
=> (s :-> s') -> (s :-> s') -> (a & a & s :-> s')
ifNeq l r = neq # if_ l r
ifLt
:: (NiceComparable a)
=> (s :-> s') -> (s :-> s') -> (a & a & s :-> s')
ifLt l r = lt # if_ l r
ifGt
:: (NiceComparable a)
=> (s :-> s') -> (s :-> s') -> (a & a & s :-> s')
ifGt l r = gt # if_ l r
ifLe
:: (NiceComparable a)
=> (s :-> s') -> (s :-> s') -> (a & a & s :-> s')
ifLe l r = le # if_ l r
ifGe
:: (NiceComparable a)
=> (s :-> s') -> (s :-> s') -> (a & a & s :-> s')
ifGe l r = ge # if_ l r
{-# WARNING fail_ "'fail_' remains in code" #-}
fail_ :: a :-> c
fail_ = unit # failWith
assert :: IsError err => err -> Bool & s :-> s
assert reason = if_ nop (failUsing reason)
assertEq0 :: (IfCmp0Constraints a Eq', IsError err) => err -> a & s :-> s
assertEq0 reason = ifEq0 nop (failUsing reason)
assertNeq0 :: (IfCmp0Constraints a Neq, IsError err) => err -> a & s :-> s
assertNeq0 reason = ifNeq0 nop (failUsing reason)
assertLt0 :: (IfCmp0Constraints a Lt, IsError err) => err -> a & s :-> s
assertLt0 reason = ifLt0 nop (failUsing reason)
assertGt0 :: (IfCmp0Constraints a Gt, IsError err) => err -> a & s :-> s
assertGt0 reason = ifGt0 nop (failUsing reason)
assertLe0 :: (IfCmp0Constraints a Le, IsError err) => err -> a & s :-> s
assertLe0 reason = ifLe0 nop (failUsing reason)
assertGe0 :: (IfCmp0Constraints a Ge, IsError err) => err -> a & s :-> s
assertGe0 reason = ifGe0 nop (failUsing reason)
assertEq :: (NiceComparable a, IsError err) => err -> a & a & s :-> s
assertEq reason = ifEq nop (failUsing reason)
assertNeq :: (NiceComparable a, IsError err) => err -> a & a & s :-> s
assertNeq reason = ifNeq nop (failUsing reason)
assertLt :: (NiceComparable a, IsError err) => err -> a & a & s :-> s
assertLt reason = ifLt nop (failUsing reason)
assertGt :: (NiceComparable a, IsError err) => err -> a & a & s :-> s
assertGt reason = ifGt nop (failUsing reason)
assertLe :: (NiceComparable a, IsError err) => err -> a & a & s :-> s
assertLe reason = ifLe nop (failUsing reason)
assertGe :: (NiceComparable a, IsError err) => err -> a & a & s :-> s
assertGe reason = ifGe nop (failUsing reason)
assertNone :: IsError err => err -> Maybe a & s :-> s
assertNone reason = ifNone nop (failUsing reason)
assertSome :: IsError err => err -> Maybe a & s :-> a & s
assertSome reason = ifNone (failUsing reason) nop
assertLeft :: IsError err => err -> Either a b & s :-> a & s
assertLeft reason = ifLeft nop (failUsing reason)
assertRight :: IsError err => err -> Either a b & s :-> b & s
assertRight reason = ifLeft (failUsing reason) nop
assertUsing
:: IsError a
=> a -> Bool & s :-> s
assertUsing err = if_ nop $ failUsing err
dropX
:: forall (n :: GHC.Nat) a inp out s s'.
( ConstraintDIPNLorentz (ToPeano n) inp out s s'
, s ~ (a ': s')
)
=> inp :-> out
dropX = dipN @n @inp @out @s @s' drop
class CloneX (n :: Peano) a s where
type CloneXT n a s :: [Kind.Type]
cloneXImpl :: a & s :-> CloneXT n a s
instance CloneX 'Z a s where
type CloneXT 'Z a s = a & s
cloneXImpl = nop
instance (CloneX n a s) => CloneX ('S n) a s where
type CloneXT ('S n) a s = a ': CloneXT n a s
cloneXImpl = dup # dip (cloneXImpl @n)
cloneX
:: forall (n :: GHC.Nat) a s. CloneX (ToPeano n) a s
=> a & s :-> CloneXT (ToPeano n) a s
cloneX = cloneXImpl @(ToPeano n)
type DuupXConstraint' kind (n :: Peano)
(s :: [kind]) (a :: kind) (s1 :: [kind]) (tail :: [kind]) =
( tail ~ Drop ('S n) s
, ConstraintDIPN' kind n s s1 (a ': tail) (a ': a ': tail)
, ConstraintDIG' kind n s1 (a ': s) a
)
type ConstraintDuupXLorentz (n :: Peano)
(s :: [Kind.Type]) (a :: Kind.Type)
(s1 :: [Kind.Type]) (tail :: [Kind.Type]) =
( DuupXConstraint' T n (ToTs s) (ToT a) (ToTs s1) (ToTs tail)
, DuupXConstraint' Kind.Type n s a s1 tail
)
class DuupX (n :: Peano) (s :: [Kind.Type]) (a :: Kind.Type) s1 tail where
duupXImpl :: s :-> a ': s
instance {-# OVERLAPPING #-} (s ~ (a ': xs)) => DuupX ('S 'Z) s a s1 tail where
duupXImpl = dup
instance {-# OVERLAPPING #-} DuupX ('S ('S 'Z)) (b ': a ': xs) a s1 tail where
duupXImpl = dip dup # swap
instance {-# OVERLAPPABLE #-} (ConstraintDuupXLorentz ('S ('S n)) s a s1 tail) =>
DuupX ('S ('S ('S n))) s a s1 tail where
duupXImpl =
dipNPeano @('S ('S n)) (dup # stackType @(a ': a ': tail)) #
digPeano @('S ('S n))
duupX :: forall (n :: GHC.Nat) a (s :: [Kind.Type]) (s1 :: [Kind.Type]) (tail :: [Kind.Type]).
( ConstraintDuupXLorentz (ToPeano (n - 1)) s a s1 tail
, DuupX (ToPeano n) s a s1 tail
)
=> s :-> a ': s
duupX = duupXImpl @(ToPeano n) @s @a @s1 @tail
where
_example ::
'[ Integer, (), Bool ] :->
'[ Bool, Integer, (), Bool ]
_example = duupX @3
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 = framed @s
where
_example
:: [Integer, Natural] :-> '[ByteString]
-> Integer : Natural : () : s :-> ByteString : () : s
_example = framedN @2
papair :: a & b & c & s :-> ((a, b), c) & s
papair = pair # pair
ppaiir :: a & b & c & s :-> (a, (b, c)) & s
ppaiir = dip pair # pair
unpair :: (a, b) & s :-> a & b & s
unpair = dup # car # dip cdr
cdar :: (a1, (a2, b)) & s :-> a2 & s
cdar = cdr # car
cddr :: (a1, (a2, b)) & s :-> b & s
cddr = cdr # cdr
caar :: ((a, b1), b2) & s :-> a & s
caar = car # car
cadr :: ((a, b1), b2) & s :-> b1 & s
cadr = car # cdr
setCar :: (a, b1) & (b2 & s) :-> (b2, b1) & s
setCar = cdr # swap # pair
setCdr :: (a, b1) & (b2 & s) :-> (a, b2) & s
setCdr = car # pair
mapCar
:: a & s :-> a1 & s
-> (a, b) & s :-> (a1, b) & s
mapCar op = dup # cdr # dip (car # op) # swap # pair
mapCdr
:: b & (a, b) & s :-> b1 & (a, b) & s
-> (a, b) & s :-> (a, b1) & s
mapCdr op = dup # cdr # op # swap # car # pair
ifRight :: (b & s :-> s') -> (a & s :-> s') -> (Either a b & s :-> s')
ifRight l r = ifLeft r l
ifSome
:: (a & s :-> s') -> (s :-> s') -> (Maybe a & s :-> s')
ifSome s n = ifNone n s
when_ :: (s :-> s) -> (Bool : s :-> s)
when_ i = if_ i nop
unless_ :: (s :-> s) -> (Bool : s :-> s)
unless_ i = if_ nop i
whenSome :: (a : s :-> s) -> (Maybe a : s :-> s)
whenSome i = ifSome i nop
class MapInstrs map where
mapUpdate :: IsComparable k => k : Maybe v : map k v : s :-> map k v : s
mapInsert :: IsComparable k => k : v : map k v : s :-> map k v : s
mapInsert = dip some # mapUpdate
mapInsertNew
:: (IsComparable k, KnownValue e)
=> (forall s0. k : s0 :-> e : s0)
-> k : v : map k v : s :-> map k v : s
deleteMap
:: forall k v s. (IsComparable k, KnownValue k, KnownValue v)
=> k : map k v : s :-> map k v : s
deleteMap = dip (none @v) # mapUpdate
instance MapInstrs Map where
mapUpdate = update
mapInsertNew mkErr = failingWhenPresent mkErr # mapInsert
instance MapInstrs BigMap where
mapUpdate = update
mapInsertNew mkErr = failingWhenPresent mkErr # mapInsert
setInsert :: IsComparable e => e & Set e & s :-> Set e & s
setInsert = dip (push True) # update
setInsertNew
:: (IsComparable e, KnownValue err)
=> (forall s0. e : s0 :-> err : s0)
-> e & Set e & s :-> Set e & s
setInsertNew desc = dip (push True) # failingWhenPresent desc # update
setDelete :: IsComparable e => e & Set e & s :-> Set e & s
setDelete = dip (push False) # update
data View (a :: Kind.Type) (r :: Kind.Type) = View
{ viewParam :: a
, viewCallbackTo :: ContractRef r
} deriving stock (Eq, Show, Generic)
deriving anyclass IsoValue
instance Each [Typeable, TypeHasDoc] [a, r] => TypeHasDoc (View a r) where
typeDocMdDescription =
"`View a r` accepts an argument of type `a` and callback contract \
\which accepts `r` and returns result via calling that contract.\n\
\Read more in [A1 conventions document](https://gitlab.com/tzip/tzip/-/blob/c42e3f0f5e73669e84e615d69bee73281572eb0a/proposals/tzip-4/tzip-4.md#view-entrypoints)."
typeDocMdReference = poly2TypeDocMdReference
typeDocDependencies p =
genericTypeDocDependencies p <>
[SomeTypeWithDoc (Proxy @()), SomeTypeWithDoc (Proxy @Integer)]
typeDocHaskellRep =
haskellRepNoFields $ concreteTypeDocHaskellRep @(View () Integer)
typeDocMichelsonRep =
concreteTypeDocMichelsonRep @(View () Integer)
instance {-# OVERLAPPABLE #-} Buildable a => Buildable (View a r) where
build = buildView build
instance {-# OVERLAPPING #-} Buildable (View () r) where
build = buildView $ const "()"
buildViewTuple :: TupleF a => View a r -> Builder
buildViewTuple = buildView tupleF
buildView :: (a -> Builder) -> View a r -> Builder
buildView bfp (View {..}) =
"(View param: " +| bfp viewParam |+ " callbackTo: " +| viewCallbackTo|+ ")"
mkView :: ToContractRef r contract => a -> contract -> View a r
mkView a c = View a (toContractRef c)
wrapView :: (a, ContractRef r) : s :-> View a r : s
wrapView = forcedCoerce_
unwrapView :: View a r : s :-> (a, ContractRef r) : s
unwrapView = forcedCoerce_
view_ ::
(NiceParameter r)
=> (forall s0. (a, storage) & s0 :-> r : s0)
-> View a r & storage & s :-> (List Operation, storage) & s
view_ code =
unwrapView #
unpair # dip (duupX @2) # pair # code # dip amount #
transferTokens # nil # swap # cons # pair
data Void_ (a :: Kind.Type) (b :: Kind.Type) = Void_
{ voidParam :: a
, voidResProxy :: Lambda b b
} deriving stock (Generic, Show)
deriving anyclass IsoValue
instance Each [Typeable, TypeHasDoc] [a, r] => TypeHasDoc (Void_ a r) where
typeDocName _ = "Void"
typeDocMdDescription =
"`Void a r` accepts an argument of type `a` and returns a value of type \
\`r` as contract error. To comply with general mechanism of contracts \
\custom errors, void entrypoints execute `FAILWITH` instruction on \
\`(\"VoidResult\", r)` value, where `r` is the actual return value of the \
\entrypoint.\n\
\Read more in [A1 conventions document](https://gitlab.com/tzip/tzip/-/blob/c42e3f0f5e73669e84e615d69bee73281572eb0a/proposals/tzip-4/tzip-4.md#void-entrypoints)."
typeDocMdReference tp =
customTypeDocMdReference
("Void", DType tp)
[ DType (Proxy @a)
, DType (Proxy @r)
]
typeDocDependencies p =
genericTypeDocDependencies p <>
[SomeTypeWithDoc (Proxy @()), SomeTypeWithDoc (Proxy @Integer)]
typeDocHaskellRep p = do
(_, rhs) <- haskellRepNoFields (concreteTypeDocHaskellRep @(Void_ () Integer)) p
return (Just "Void () Integer", rhs)
typeDocMichelsonRep p =
let (_, rhs) = concreteTypeDocMichelsonRep @(Void_ () Integer) p
in (Just "Void () Integer", rhs)
instance Buildable a => Buildable (Void_ a b) where
build Void_ {..} = "(Void param: " +| voidParam |+ ")"
newtype VoidResult r = VoidResult { unVoidResult :: r }
deriving stock (Generic)
deriving newtype (Eq)
voidResultTag :: MText
voidResultTag = [mt|VoidResult|]
type VoidResultRep r = (MText, r)
instance (TypeHasDoc r, IsError (VoidResult r)) => TypeHasDoc (VoidResult r) where
typeDocMdDescription = typeDocMdDescriptionReferToError @(VoidResult r)
typeDocMdReference = poly1TypeDocMdReference
typeDocHaskellRep = concreteTypeDocHaskellRepUnsafe @(VoidResultRep Integer)
typeDocMichelsonRep = concreteTypeDocMichelsonRepUnsafe @(VoidResultRep Integer)
instance (Typeable r, NiceConstant r, ErrorHasDoc (VoidResult r)) =>
IsError (VoidResult r) where
errorToVal (VoidResult e) cont =
withDict (niceConstantEvi @r) $
isoErrorToVal @(VoidResultRep r) (voidResultTag, e) cont
errorFromVal fullErr =
isoErrorFromVal fullErr >>= \((tag, e) :: VoidResultRep r) ->
if tag == voidResultTag
then pure $ VoidResult e
else Left $ "Error mismatch, expected VoidResult, got " <> pretty tag
instance TypeHasDoc r => ErrorHasDoc (VoidResult r) where
errorDocName = "VoidResult"
errorDocMdCause =
"Call to entrypoint has succeeded, reporting returned value as error.\n\
\As Tezos contracts normally do not produce any output (not counting storage \
\update), this is the simplest way to return something to the caller in \
\read-only entrypoints."
errorDocHaskellRep =
mdTicked ("(\"" <> pretty (voidResultTag) <> "\", " <> "<return value>" <> ")")
errorDocDependencies =
typeDocDependencies' (Proxy @MText) <> typeDocDependencies' (Proxy @r)
instance CustomErrorNoIsoValue (VoidResult r) => IsoValue (VoidResult r) where
type ToT (VoidResult r) = CustomErrorNoIsoValue (VoidResult r)
toVal = error "impossible"
fromVal = error "impossible"
mkVoid :: forall b a. a -> Void_ a b
mkVoid a = Void_ a nop
void_
:: forall a b s s' anything.
(IsError (VoidResult b), KnownValue b)
=> a & s :-> b & s' -> Void_ a b & s :-> anything
void_ code =
doc (DThrows (Proxy @(VoidResult b))) #
forcedCoerce_ @_ @(_, Lambda b b) #
unpair # swap # dip code # swap # exec #
push voidResultTag # pair # failWith @(MText, b)
addressToEpAddress :: Address : s :-> EpAddress : s
addressToEpAddress = forcedCoerce_
pushContractRef
:: NiceParameter arg
=> (forall s0. FutureContract arg : s :-> s0)
-> ContractRef arg
-> (s :-> ContractRef arg : s)
pushContractRef onContractNotFound (contractRef :: ContractRef arg) =
withDict (niceParameterEvi @arg) $
push (FutureContract contractRef) # dup #
runFutureContract # ifNone onContractNotFound (dip drop)