lorentz-0.10.0: EDSL for the Michelson Language
Safe HaskellNone
LanguageHaskell2010

Lorentz.Instr

Synopsis

Documentation

nop :: s :-> s Source #

comment :: CommentType -> s :-> s Source #

commentAroundFun :: Text -> (i :-> o) -> i :-> o Source #

commentAroundStmt :: Text -> (i :-> o) -> i :-> o Source #

drop :: (a ': s) :-> s Source #

dropN :: forall (n :: Nat) (s :: [Type]). (SingI (ToPeano n), KnownPeano (ToPeano n), RequireLongerOrSameLength (ToTs s) (ToPeano n), Drop (ToPeano n) (ToTs s) ~ ToTs (Drop (ToPeano n) s)) => s :-> Drop (ToPeano n) s Source #

Drop top n elements from the stack.

type ConstraintDUPNLorentz (n :: Peano) (inp :: [Type]) (out :: [Type]) (a :: Type) = (ConstraintDUPN n (ToTs inp) (ToTs out) (ToT a), ConstraintDUPN' Type n inp out a) Source #

dup :: (a ': s) :-> (a ': (a ': s)) Source #

dupNPeano :: forall (n :: Peano) inp out a. ConstraintDUPNLorentz n inp out a => inp :-> out Source #

dupN :: forall (n :: Nat) inp out a. ConstraintDUPNLorentz (ToPeano n) inp out a => inp :-> out Source #

swap :: (a ': (b ': s)) :-> (b ': (a ': s)) Source #

type ConstraintDIGLorentz (n :: Peano) (inp :: [Type]) (out :: [Type]) (a :: Type) = (ConstraintDIG n (ToTs inp) (ToTs out) (ToT a), ConstraintDIG' Type n inp out a) Source #

digPeano :: forall (n :: Peano) inp out a. ConstraintDIGLorentz n inp out a => inp :-> out Source #

Version of dig which uses Peano number. It is intended for internal usage in Lorentz.

dig :: forall (n :: Nat) inp out a. ConstraintDIGLorentz (ToPeano n) inp out a => inp :-> out Source #

type ConstraintDUGLorentz (n :: Peano) (inp :: [Type]) (out :: [Type]) (a :: Type) = (ConstraintDUG n (ToTs inp) (ToTs out) (ToT a), ConstraintDUG' Type n inp out a) Source #

dugPeano :: forall (n :: Peano) inp out a. ConstraintDUGLorentz n inp out a => inp :-> out Source #

Version of dug which uses Peano number. It is intended for internal usage in Lorentz.

dug :: forall (n :: Nat) inp out a. ConstraintDUGLorentz (ToPeano n) inp out a => inp :-> out Source #

push :: forall t s. NiceConstant t => t -> s :-> (t ': s) Source #

some :: (a ': s) :-> (Maybe a ': s) Source #

none :: forall a s. KnownValue a => s :-> (Maybe a ': s) Source #

unit :: s :-> (() ': s) Source #

ifNone :: (s :-> s') -> ((a ': s) :-> s') -> (Maybe a ': s) :-> s' Source #

pair :: (a ': (b ': s)) :-> ((a, b) ': s) Source #

car :: ((a, b) ': s) :-> (a ': s) Source #

cdr :: ((a, b) ': s) :-> (b ': s) Source #

left :: forall a b s. KnownValue b => (a ': s) :-> (Either a b ': s) Source #

right :: forall a b s. KnownValue a => (b ': s) :-> (Either a b ': s) Source #

ifLeft :: ((a ': s) :-> s') -> ((b ': s) :-> s') -> (Either a b ': s) :-> s' Source #

nil :: KnownValue p => s :-> (List p ': s) Source #

cons :: (a ': (List a ': s)) :-> (List a ': s) Source #

size :: SizeOpHs c => (c ': s) :-> (Natural ': s) Source #

emptySet :: NiceComparable e => s :-> (Set e ': s) Source #

emptyMap :: (NiceComparable k, KnownValue v) => s :-> (Map k v ': s) Source #

map :: (MapOpHs c, IsoMapOpRes c b, KnownValue b, HasCallStack) => ((MapOpInpHs c ': s) :-> (b ': s)) -> (c ': s) :-> (MapOpResHs c b ': s) Source #

iter :: (IterOpHs c, HasCallStack) => ((IterOpElHs c ': s) :-> s) -> (c ': s) :-> s Source #

mem :: MemOpHs c => (MemOpKeyHs c ': (c ': s)) :-> (Bool ': s) Source #

get :: (GetOpHs c, KnownValue (GetOpValHs c)) => (GetOpKeyHs c ': (c ': s)) :-> (Maybe (GetOpValHs c) ': s) Source #

type ConstraintPairGetLorentz (n :: Nat) (pair :: Type) = (ConstraintGetN (ToPeano n) (ToT pair), ToT (PairGetHs (ToPeano n) pair) ~ GetN (ToPeano n) (ToT pair)) Source #

type family PairGetHs (ix :: Peano) (pair :: Type) :: Type where ... Source #

Equations

PairGetHs 'Z val = val 
PairGetHs ('S 'Z) (left, _) = left 
PairGetHs ('S ('S n)) (_, right) = PairGetHs n right 

pairGet :: forall (n :: Nat) (pair :: Type) (s :: [Type]). ConstraintPairGetLorentz n pair => (pair ': s) :-> (PairGetHs (ToPeano n) pair ': s) Source #

update :: UpdOpHs c => (UpdOpKeyHs c ': (UpdOpParamsHs c ': (c ': s))) :-> (c ': s) Source #

type ConstraintPairUpdateLorentz (n :: Nat) (val :: Type) (pair :: Type) = (ConstraintUpdateN (ToPeano n) (ToT pair), ToT (PairUpdateHs (ToPeano n) val pair) ~ UpdateN (ToPeano n) (ToT val) (ToT pair)) Source #

type family PairUpdateHs (ix :: Peano) (val :: Type) (pair :: Type) :: Type where ... Source #

Equations

PairUpdateHs 'Z val _ = val 
PairUpdateHs ('S 'Z) val (_, right) = (val, right) 
PairUpdateHs ('S ('S n)) val (left, right) = (left, PairUpdateHs n val right) 

pairUpdate :: forall (n :: Nat) (val :: Type) (pair :: Type) (s :: [Type]). ConstraintPairUpdateLorentz n val pair => (val ': (pair ': s)) :-> (PairUpdateHs (ToPeano n) val pair ': s) Source #

failingWhenPresent :: forall c k s v st e. (MemOpHs c, k ~ MemOpKeyHs c, NiceConstant e, st ~ (k ': (v ': (c ': s)))) => (forall s0. (k ': s0) :-> (e ': s0)) -> st :-> st Source #

Helper instruction.

Checks whether given key present in the storage and fails if it is. This instruction leaves stack intact.

updateNew :: forall c k s e. (UpdOpHs c, MemOpHs c, k ~ UpdOpKeyHs c, k ~ MemOpKeyHs c, NiceConstant e) => (forall s0. (k ': s0) :-> (e ': s0)) -> (k ': (UpdOpParamsHs c ': (c ': s))) :-> (c ': s) Source #

Like update, but throw an error on attempt to overwrite existing entry.

if_ :: (s :-> s') -> (s :-> s') -> (Bool ': s) :-> s' Source #

ifCons :: ((a ': (List a ': s)) :-> s') -> (s :-> s') -> (List a ': s) :-> s' Source #

loop :: (s :-> (Bool ': s)) -> (Bool ': s) :-> s Source #

loopLeft :: ((a ': s) :-> (Either a b ': s)) -> (Either a b ': s) :-> (b ': s) Source #

lambda :: ZipInstrs [i, o] => (i :-> o) -> s :-> ((i :-> o) ': s) Source #

exec :: (a ': (Lambda a b ': s)) :-> (b ': s) Source #

execute :: forall i o s. Each [KnownList, ZipInstr] [i, o] => ((i :-> o) ': (i ++ s)) :-> (o ++ s) Source #

Similar to exec but works for lambdas with arbitrary size of input and output.

Note that this instruction has its arguments flipped, lambda goes first. This seems to be the only reasonable way to achieve good inference.

apply :: forall a b c s. (NiceConstant a, KnownValue b) => (a ': (Lambda (a, b) c ': s)) :-> (Lambda b c ': s) Source #

applicate :: forall a b c inp2nd inpTail s. (NiceConstant a, ZipInstr b, b ~ (inp2nd ': inpTail)) => (a ': (((a ': b) :-> c) ': s)) :-> ((b :-> c) ': s) Source #

Version of apply that works for lambdas with arbitrary length input and output.

dip :: forall a s s'. HasCallStack => (s :-> s') -> (a ': s) :-> (a ': s') Source #

type ConstraintDIPNLorentz (n :: Peano) (inp :: [Type]) (out :: [Type]) (s :: [Type]) (s' :: [Type]) = (ConstraintDIPN n (ToTs inp) (ToTs out) (ToTs s) (ToTs s'), ConstraintDIPN' Type n inp out s s') Source #

dipNPeano :: forall (n :: Peano) (inp :: [Type]) (out :: [Type]) (s :: [Type]) (s' :: [Type]). ConstraintDIPNLorentz n inp out s s' => (s :-> s') -> inp :-> out Source #

Version of dipN which uses Peano number. It is intended for internal usage in Lorentz.

dipN :: forall (n :: Nat) (inp :: [Type]) (out :: [Type]) (s :: [Type]) (s' :: [Type]). ConstraintDIPNLorentz (ToPeano n) inp out s s' => (s :-> s') -> inp :-> out Source #

failWith :: forall a s t. NiceConstant a => (a ': s) :-> t Source #

cast :: KnownValue a => (a ': s) :-> (a ': s) Source #

pack :: forall a s. NicePackedValue a => (a ': s) :-> (Packed a ': s) Source #

unpack :: forall a s. NiceUnpackedValue a => (Packed a ': s) :-> (Maybe a ': s) Source #

packRaw :: forall a s. NicePackedValue a => (a ': s) :-> (ByteString ': s) Source #

unpackRaw :: forall a s. NiceUnpackedValue a => (ByteString ': s) :-> (Maybe a ': s) Source #

concat :: ConcatOpHs c => (c ': (c ': s)) :-> (c ': s) Source #

concat' :: ConcatOpHs c => (List c ': s) :-> (c ': s) Source #

slice :: (SliceOpHs c, KnownValue c) => (Natural ': (Natural ': (c ': s))) :-> (Maybe c ': s) Source #

isNat :: (Integer ': s) :-> (Maybe Natural ': s) Source #

add :: ArithOpHs Add n m => (n ': (m ': s)) :-> (ArithResHs Add n m ': s) Source #

sub :: ArithOpHs Sub n m => (n ': (m ': s)) :-> (ArithResHs Sub n m ': s) Source #

rsub :: ArithOpHs Sub n m => (m ': (n ': s)) :-> (ArithResHs Sub n m ': s) Source #

mul :: ArithOpHs Mul n m => (n ': (m ': s)) :-> (ArithResHs Mul n m ': s) Source #

ediv :: EDivOpHs n m => (n ': (m ': s)) :-> (Maybe (EDivOpResHs n m, EModOpResHs n m) ': s) Source #

abs :: UnaryArithOpHs Abs n => (n ': s) :-> (UnaryArithResHs Abs n ': s) Source #

neg :: UnaryArithOpHs Neg n => (n ': s) :-> (UnaryArithResHs Neg n ': s) Source #

lsl :: ArithOpHs Lsl n m => (n ': (m ': s)) :-> (ArithResHs Lsl n m ': s) Source #

lsr :: ArithOpHs Lsr n m => (n ': (m ': s)) :-> (ArithResHs Lsr n m ': s) Source #

or :: ArithOpHs Or n m => (n ': (m ': s)) :-> (ArithResHs Or n m ': s) Source #

and :: ArithOpHs And n m => (n ': (m ': s)) :-> (ArithResHs And n m ': s) Source #

xor :: ArithOpHs Xor n m => (n ': (m ': s)) :-> (ArithResHs Xor n m ': s) Source #

not :: UnaryArithOpHs Not n => (n ': s) :-> (UnaryArithResHs Not n ': s) Source #

compare :: NiceComparable n => (n ': (n ': s)) :-> (Integer ': s) Source #

eq0 :: UnaryArithOpHs Eq' n => (n ': s) :-> (UnaryArithResHs Eq' n ': s) Source #

neq0 :: UnaryArithOpHs Neq n => (n ': s) :-> (UnaryArithResHs Neq n ': s) Source #

lt0 :: UnaryArithOpHs Lt n => (n ': s) :-> (UnaryArithResHs Lt n ': s) Source #

gt0 :: UnaryArithOpHs Gt n => (n ': s) :-> (UnaryArithResHs Gt n ': s) Source #

le0 :: UnaryArithOpHs Le n => (n ': s) :-> (UnaryArithResHs Le n ': s) Source #

ge0 :: UnaryArithOpHs Ge n => (n ': s) :-> (UnaryArithResHs Ge n ': s) Source #

int :: ToIntegerArithOpHs i => (i ': s) :-> (Integer ': s) Source #

toTAddress_ :: forall cp addr s. ToTAddress_ cp addr => (addr ': s) :-> (TAddress cp ': s) Source #

Cast something appropriate to TAddress.

self :: forall p s. (NiceParameterFull p, ForbidExplicitDefaultEntrypoint p) => s :-> (ContractRef p ': s) Source #

Get a reference to the current contract.

Note that, similar to CONTRACT instruction, in Michelson SELF instruction can accept an entrypoint as field annotation, and without annotation specified it creates a contract value which calls the default entrypoint.

This particular function carries the behaviour of SELF before introduction of lightweight entrypoints feature. Thus the contract must not have explicit "default" entrypoint for this to work.

If you are going to call a specific entrypoint of the contract, see selfCalling.

selfCalling :: forall p mname s. NiceParameterFull p => EntrypointRef mname -> s :-> (ContractRef (GetEntrypointArgCustom p mname) ': s) Source #

Make a reference to the current contract, maybe a specific entrypoint.

Note that, since information about parameter of the current contract is not carried around, in this function you need to specify parameter type p explicitly.

contract :: forall p addr s. (NiceParameterFull p, ForbidExplicitDefaultEntrypoint p, ToTAddress_ p addr) => (addr ': s) :-> (Maybe (ContractRef p) ': s) Source #

Get a reference to a contract by its address.

This instruction carries the behaviour of CONTRACT before introduction of lightweight entrypoints feature. The contract must not have explicit "default" entrypoint for this to work.

If you are going to call a specific entrypoint of the contract, see contractCalling.

contractCalling :: forall cp epRef epArg addr s. (HasEntrypointArg cp epRef epArg, ToTAddress_ cp addr) => epRef -> (addr ': s) :-> (Maybe (ContractRef epArg) ': s) Source #

Make a reference to a contract, maybe a specific entrypoint.

When calling this function, make sure that parameter type is known. It's recommended that you supply TAddress with a concrete parameter as the stack argument.

contractCallingUnsafe :: forall arg s. NiceParameter arg => EpName -> (Address ': s) :-> (Maybe (ContractRef arg) ': s) Source #

Specialized version of contractCalling for the case when you do not have compile-time evidence of appropriate HasEntrypointArg. For instance, if you have untyped EpName you can not have this evidence (the value is only available in runtime). If you have typed EntrypointRef, use eprName to construct EpName.

runFutureContract :: forall p s. NiceParameter p => (FutureContract p ': s) :-> (Maybe (ContractRef p) ': s) Source #

Version of contract instruction which may accept address with already specified entrypoint name.

Also you cannot specify entrypoint name here because this could result in conflict.

epAddressToContract :: forall p s. NiceParameter p => (EpAddress ': s) :-> (Maybe (ContractRef p) ': s) Source #

Similar to runFutureContract, works with EpAddress.

Validity of such operation cannot be ensured at compile time.

transferTokens :: forall p s. NiceParameter p => (p ': (Mutez ': (ContractRef p ': s))) :-> (Operation ': s) Source #

createContract :: forall p g s. (NiceStorage g, NiceParameterFull p) => Contract p g -> (Maybe KeyHash ': (Mutez ': (g ': s))) :-> (Operation ': (Address ': s)) Source #

now :: s :-> (Timestamp ': s) Source #

amount :: s :-> (Mutez ': s) Source #

balance :: s :-> (Mutez ': s) Source #

checkSignature :: BytesLike bs => (PublicKey ': (TSignature bs ': (bs ': s))) :-> (Bool ': s) Source #

sha256 :: BytesLike bs => (bs ': s) :-> (Hash Sha256 bs ': s) Source #

sha512 :: BytesLike bs => (bs ': s) :-> (Hash Sha512 bs ': s) Source #

blake2B :: BytesLike bs => (bs ': s) :-> (Hash Blake2b bs ': s) Source #

sha3 :: BytesLike bs => (bs ': s) :-> (Hash Sha3 bs ': s) Source #

keccak :: BytesLike bs => (bs ': s) :-> (Hash Keccak bs ': s) Source #

hashKey :: (PublicKey ': s) :-> (KeyHash ': s) Source #

source :: s :-> (Address ': s) Source #

Warning: Using source is considered a bad practice. Consider using sender instead until further investigation

sender :: s :-> (Address ': s) Source #

address :: (ContractRef a ': s) :-> (Address ': s) Source #

chainId :: s :-> (ChainId ': s) Source #

level :: s :-> (Natural ': s) Source #

never :: (Never ': s) :-> s' Source #

framed :: forall s i o. (KnownList i, KnownList o) => (i :-> o) -> (i ++ s) :-> (o ++ s) Source #

Execute given instruction on truncated stack.

This instruction requires you to specify the piece of stack to truncate as type argument.

class LorentzFunctor (c :: Type -> Type) where Source #

Methods

lmap :: KnownValue b => ((a ': s) :-> (b ': s)) -> (c a ': s) :-> (c b ': s) Source #

Instances

Instances details
LorentzFunctor Maybe Source # 
Instance details

Defined in Lorentz.Instr

Methods

lmap :: forall b a (s :: [Type]). KnownValue b => ((a ': s) :-> (b ': s)) -> (Maybe a ': s) :-> (Maybe b ': s) Source #

class NonZero t where Source #

Methods

nonZero :: (t ': s) :-> (Maybe t ': s) Source #

Retain the value only if it is not zero.

Instances

Instances details
NonZero Integer Source # 
Instance details

Defined in Lorentz.Instr

Methods

nonZero :: forall (s :: [Type]). (Integer ': s) :-> (Maybe Integer ': s) Source #

NonZero Natural Source # 
Instance details

Defined in Lorentz.Instr

Methods

nonZero :: forall (s :: [Type]). (Natural ': s) :-> (Maybe Natural ': s) Source #