Lorentz.Expr

Evaluation of expressions.

Stack-based languages allow convenient expressions evaluation, for that we just need binary instructions in infix notation, not in Polish postfix notation that add and other primitives provide. Compare:

push 1; push 2; push 3; push 4; mul; rsub; add

vs

push 1 |+| push 2 |-| push 3 |*| push 4

In these expressions each atom is some instruction providing a single value on top of the stack, for example:

nthOdd :: Lambda Natural Natural
nthOdd = take |*| push Natural 2 |+| push Natural 1

For binary operations we provide the respective operators. Unary operations can be lifted with unaryExpr:

implication :: [Bool, Bool] :-> '[Bool]
implication = unaryExpr not take |.|.| take

or with its alias in form of an operator:

implication :: [Bool, Bool] :-> '[Bool]
implication = not $: take |.|.| take

Stack changes are propagated from left to right. If an atom consumes an element at the top of the stack, the next atom will accept only the remainder of the stack.

In most cases you should prefer providing named variables to the formulas in order to avoid messing up with the arguments:

f :: ("a" :! Natural) : ("b" :! Natural) : ("c" :! Natural) : s :-> Integer : s
f = fromNamed #a |+| fromNamed #b |-| fromNamed #c

Instead of putting all the elements on the stack upon applying the formula, you may find it more convenient to evaluate most of the arguments right within the formula:

withinRange
  :: Natural : a : b : c : ("config" :! Config) : s
  :-> Bool : a : b : c : ("config" :! Config) : s
withinRange =
  dup  |>=| do{ dupL #config; toField #minBound } |&|
  take |<=| do{ dupL #config; toField #maxBound }

Documentation

type Expr inp out res = inp :-> (res ': out)

Expression is just an instruction accepting stack inp and producing stack out with evaluation result res at the top.

take :: Expr (a ': s) s a

Consume an element at the top of stack. This is just an alias for nop.

unaryExpr :: (forall s. (a ': s) :-> (r ': s)) -> Expr s0 s1 a -> Expr s0 s1 r

Lift an instruction to an unary operation on expressions.

($:) :: (forall s. (a ': s) :-> (r ': s)) -> Expr s0 s1 a -> Expr s0 s1 r infixr 9

An alias for unaryExpr.

binaryExpr :: (forall s. (a ': (b ': s)) :-> (r ': s)) -> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r

Lift an instruction to a binary operation on expressions.

(|+|) :: ArithOpHs Add a b r => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r infixl 6

Expressions addition.

(|-|) :: ArithOpHs Sub a b r => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r infixl 6

Expressions subtraction.

(|*|) :: ArithOpHs Mul a b r => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r infixl 7

Expressions multiplication.

(|==|) :: NiceComparable a => Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool infix 4

Expressions comparison.

(|/=|) :: NiceComparable a => Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool infix 4

Expressions comparison.

(|<|) :: NiceComparable a => Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool infix 4

Expressions comparison.

(|>|) :: NiceComparable a => Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool infix 4

Expressions comparison.

(|<=|) :: NiceComparable a => Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool infix 4

Expressions comparison.

(|>=|) :: NiceComparable a => Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool infix 4

Expressions comparison.

(|&|) :: ArithOpHs And a b r => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r infixl 2

Bitwise/logical AND on expressions.

(|||) :: ArithOpHs Or a b r => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r infixl 1

Bitwise/logical OR on expressions.

In case you find this operator looking weird, see |.|.|

(|.|.|) :: ArithOpHs Or a b r => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r infixl 1

An alias for |||.

(|^|) :: ArithOpHs Xor a b r => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r infixl 3

Bitwise/logical XOR on expressions.

(|<<|) :: ArithOpHs Lsl a b r => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r infix 8

Left shift on expressions.

(|>>|) :: ArithOpHs Lsr a b r => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r infix 8

Right shift on expressions.

(|:|) :: Expr s0 s1 a -> Expr s1 s2 [a] -> Expr s0 s2 [a] infix 1

cons on expressions.

one :: a : s :-> [a] : s
one = take |:| nil

pairE :: (Expr s0 s1 a, Expr s1 s2 b) -> Expr s0 s2 (a, b)

An alias for |@|.

trivialContract :: ((), storage) :-> ([Operation], Storage)
trivialContract =
  pairE
    ( nil
    , cdr
    )

(|@|) :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (a, b) infix 0

Construct a simple pair.

trivialContract :: ((), storage) :-> ([Operation], Storage)
trivialContract = nil |@| cdr

This is useful as pair appears even in simple contracts. For more advanced types, use constructT.

listE :: KnownValue a => [Expr s s a] -> Expr s s [a]

Construct a list given the constructor for each element.

transferTokensE :: NiceParameter p => ("arg" :! Expr s0 s1 p) -> ("amount" :! Expr s1 s2 Mutez) -> ("contract" :! Expr s2 s3 (ContractRef p)) -> Expr s0 s3 Operation

Version of transferTokens instruction that accepts all the arguments as expressions.

transferTokensE
  ! #arg L.unit
  ! #amount (push zeroMutez)
  ! #contract take
  |:| nil

You can provide arguments in arbitrary order, but direction of stack changes flow is fixed: stack change in arg expression affects stack available in amount expression, and stack changes in amount expression affect stack changes in contract expression.

Orphan instances

(i ~ arg, o ~ argl, o ~ argr, r ~ Bool, outb ~ out) => IsCondition (Expr i o r) arg argl argr outb out

An expression producing Bool can be placed as condition to 'if'.

Methods

ifThenElse :: Expr i o r -> (argl :-> outb) -> (argr :-> outb) -> arg :-> out