-- SPDX-FileCopyrightText: 2021 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

{-# OPTIONS_GHC -Wno-orphans #-}

{- | 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 }
@

-}
module Lorentz.Expr
  ( Expr
  , take
  , unaryExpr
  , ($:)
  , binaryExpr
  , (|+|)
  , (|-|)
  , (|*|)
  , (|==|)
  , (|/=|)
  , (|<|)
  , (|>|)
  , (|<=|)
  , (|>=|)
  , (|&|)
  , (|||)
  , (|.|.|)
  , (|^|)
  , (|<<|)
  , (|>>|)
  , (|:|)
  , (|@|)
  , listE
  ) where

import Prelude (foldr)

import Lorentz.Arith
import Lorentz.Base
import Lorentz.Constraints
import Lorentz.Instr
import Lorentz.Macro
import Lorentz.Rebinded
import Lorentz.Value
import Michelson.Typed.Arith

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

-- Stack flows from left to right, so e.g. @ fromNamed #a |<| fromNamed #b @
-- consumes first the value with label @a@ from the stack's top, then the value
-- with label @b@.
type Expr inp out res = inp :-> res : out

{- Note on the type alias ↑

It was pretty difficult to decide whether 'Expr' should be a newtype or type
alias.

Pros of newtype:
* It is safer and clearer.
* It allows defining such 'IsLabel name (Expr ...)' instance that would allow
  writing @ #a |<| #b @ (which should consume values asserting their labels).

It would /not/ allow writing @5 :: Expr ... Natural@, because this way we lose
GHC checks on passing out-of-bounds numbers like @(-1) :: Natural@.

Cons:
* Any non-trivial operation like @push@, @dupL@ and others will require a
  wrapper.

To make all this as simple to use and understand as possible, we used a
type alias.
-}

-- | An expression producing 'Bool' can be placed as condition to 'if'.
instance (i ~ arg, o ~ argl, o ~ argr, r ~ Bool, outb ~ out) =>
         IsCondition (Expr i o r) arg argl argr outb out where
  ifThenElse :: Expr i o r -> (argl :-> outb) -> (argr :-> outb) -> arg :-> out
ifThenElse Expr i o r
e argl :-> outb
l argr :-> outb
r = Expr i o r
e Expr i o r -> ((r : o) :-> outb) -> i :-> outb
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (argl :-> outb) -> (argl :-> outb) -> (Bool : argl) :-> outb
forall (s :: [*]) (s' :: [*]).
(s :-> s') -> (s :-> s') -> (Bool : s) :-> s'
if_ argl :-> outb
l argl :-> outb
argr :-> outb
r

-- | Consume an element at the top of stack. This is just an alias for @nop@.
take :: Expr (a : s) s a
take :: Expr (a : s) s a
take = Expr (a : s) s a
forall (s :: [*]). s :-> s
nop

-- | Lift an instruction to an unary operation on expressions.
unaryExpr
  :: (forall s. a : s :-> r : s)
  -> Expr s0 s1 a -> Expr s0 s1 r
unaryExpr :: (forall (s :: [*]). (a : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s0 s1 r
unaryExpr forall (s :: [*]). (a : s) :-> (r : s)
op Expr s0 s1 a
a = Expr s0 s1 a
a Expr s0 s1 a -> ((a : s1) :-> (r : s1)) -> Expr s0 s1 r
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : s1) :-> (r : s1)
forall (s :: [*]). (a : s) :-> (r : s)
op

-- | An alias for 'unaryExpr'.
infixr 9 $:
($:)
  :: (forall s. a : s :-> r : s)
  -> Expr s0 s1 a -> Expr s0 s1 r
$: :: (forall (s :: [*]). (a : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s0 s1 r
($:) = (forall (s :: [*]). (a : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s0 s1 r
forall a r (s0 :: [*]) (s1 :: [*]).
(forall (s :: [*]). (a : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s0 s1 r
unaryExpr

-- | Lift an instruction to a binary operation on expressions.
binaryExpr
  :: (forall s. a : b : s :-> r : s)
  -> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr :: (forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (r : s)
op Expr s0 s1 a
l Expr s1 s2 b
r = Expr s0 s1 a
l Expr s0 s1 a -> ((a : s1) :-> (a : b : s2)) -> s0 :-> (a : b : s2)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Expr s1 s2 b -> (a : s1) :-> (a : b : s2)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip Expr s1 s2 b
r (s0 :-> (a : b : s2))
-> ((a : b : s2) :-> (r : s2)) -> Expr s0 s2 r
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : b : s2) :-> (r : s2)
forall (s :: [*]). (a : b : s) :-> (r : s)
op

-- | Expressions addition.
infixl 6 |+|
(|+|)
  :: (ArithOpHs Add a b)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Add a b)
|+| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Add a b)
(|+|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Add a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Add a b)
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (ArithResHs Add a b : s)
forall n m (s :: [*]).
ArithOpHs Add n m =>
(n : m : s) :-> (ArithResHs Add n m : s)
add

-- | Expressions subtraction.
infixl 6 |-|
(|-|)
  :: (ArithOpHs Sub a b)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Sub a b)
|-| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Sub a b)
(|-|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Sub a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Sub a b)
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (ArithResHs Sub a b : s)
forall n m (s :: [*]).
ArithOpHs Sub n m =>
(n : m : s) :-> (ArithResHs Sub n m : s)
sub

-- | Expressions multiplication.
infixl 7 |*|
(|*|)
  :: (ArithOpHs Mul a b)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Mul a b)
|*| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Mul a b)
(|*|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Mul a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Mul a b)
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (ArithResHs Mul a b : s)
forall n m (s :: [*]).
ArithOpHs Mul n m =>
(n : m : s) :-> (ArithResHs Mul n m : s)
mul

-- | Expressions comparison.
infix 4 |==|
infix 4 |/=|
infix 4 |<|
infix 4 |>|
infix 4 |<=|
infix 4 |>=|
(|==|), (|/=|), (|<|), (|>|), (|>=|), (|<=|)
  :: (NiceComparable a)
  => Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
|==| :: Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
(|==|) = (forall (s :: [*]). (a : a : s) :-> (Bool : s))
-> Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : a : s) :-> (Bool : s)
forall n (s :: [*]). NiceComparable n => (n : n : s) :-> (Bool : s)
eq
|/=| :: Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
(|/=|) = (forall (s :: [*]). (a : a : s) :-> (Bool : s))
-> Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : a : s) :-> (Bool : s)
forall n (s :: [*]). NiceComparable n => (n : n : s) :-> (Bool : s)
neq
|<| :: Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
(|<|) = (forall (s :: [*]). (a : a : s) :-> (Bool : s))
-> Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : a : s) :-> (Bool : s)
forall n (s :: [*]). NiceComparable n => (n : n : s) :-> (Bool : s)
lt
|>| :: Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
(|>|) = (forall (s :: [*]). (a : a : s) :-> (Bool : s))
-> Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : a : s) :-> (Bool : s)
forall n (s :: [*]). NiceComparable n => (n : n : s) :-> (Bool : s)
gt
|<=| :: Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
(|<=|) = (forall (s :: [*]). (a : a : s) :-> (Bool : s))
-> Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : a : s) :-> (Bool : s)
forall n (s :: [*]). NiceComparable n => (n : n : s) :-> (Bool : s)
le
|>=| :: Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
(|>=|) = (forall (s :: [*]). (a : a : s) :-> (Bool : s))
-> Expr s0 s1 a -> Expr s1 s2 a -> Expr s0 s2 Bool
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : a : s) :-> (Bool : s)
forall n (s :: [*]). NiceComparable n => (n : n : s) :-> (Bool : s)
ge

-- | Bitwise/logical @AND@ on expressions.
infixl 2 |&|
(|&|)
  :: (ArithOpHs And a b)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs And a b)
|&| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs And a b)
(|&|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs And a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs And a b)
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (ArithResHs And a b : s)
forall n m (s :: [*]).
ArithOpHs And n m =>
(n : m : s) :-> (ArithResHs And n m : s)
and

-- | Bitwise/logical @OR@ on expressions.
--
-- In case you find this operator looking weird, see '|.|.|'
infixl 1 |||
(|||)
  :: (ArithOpHs Or a b)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or a b)
||| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or a b)
(|||) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Or a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or a b)
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (ArithResHs Or a b : s)
forall n m (s :: [*]).
ArithOpHs Or n m =>
(n : m : s) :-> (ArithResHs Or n m : s)
or

-- | An alias for '|||'.
infixl 1 |.|.|
(|.|.|)
  :: (ArithOpHs Or a b)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or a b)
|.|.| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or a b)
(|.|.|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Or a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or a b)
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (ArithResHs Or a b : s)
forall n m (s :: [*]).
ArithOpHs Or n m =>
(n : m : s) :-> (ArithResHs Or n m : s)
or

-- | Bitwise/logical @XOR@ on expressions.
infixl 3 |^|
(|^|)
  :: (ArithOpHs Xor a b)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Xor a b)
|^| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Xor a b)
(|^|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Xor a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Xor a b)
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (ArithResHs Xor a b : s)
forall n m (s :: [*]).
ArithOpHs Xor n m =>
(n : m : s) :-> (ArithResHs Xor n m : s)
xor

-- | Left shift on expressions.
infix 8 |<<|
(|<<|)
  :: (ArithOpHs Lsl a b)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsl a b)
|<<| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsl a b)
(|<<|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Lsl a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsl a b)
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (ArithResHs Lsl a b : s)
forall n m (s :: [*]).
ArithOpHs Lsl n m =>
(n : m : s) :-> (ArithResHs Lsl n m : s)
lsl

-- | Right shift on expressions.
infix 8 |>>|
(|>>|)
  :: (ArithOpHs Lsr a b)
  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsr a b)
|>>| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsr a b)
(|>>|) = (forall (s :: [*]). (a : b : s) :-> (ArithResHs Lsr a b : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsr a b)
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> (ArithResHs Lsr a b : s)
forall n m (s :: [*]).
ArithOpHs Lsr n m =>
(n : m : s) :-> (ArithResHs Lsr n m : s)
lsr

-- | 'cons' on expressions.
--
-- @
-- one :: a : s :-> [a] : s
-- one = take |:| nil
-- @
infix 1 |:|
(|:|) :: Expr s0 s1 a -> Expr s1 s2 [a] -> Expr s0 s2 [a]
|:| :: Expr s0 s1 a -> Expr s1 s2 [a] -> Expr s0 s2 [a]
(|:|) = (forall (s :: [*]). (a : [a] : s) :-> ([a] : s))
-> Expr s0 s1 a -> Expr s1 s2 [a] -> Expr s0 s2 [a]
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : [a] : s) :-> ([a] : s)
forall a (s :: [*]). (a : List a : s) :-> (List a : s)
cons

-- | 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 'Lorentz.ADT.constructT'.
infix 0 |@|
(|@|) :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (a, b)
|@| :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (a, b)
(|@|) = (forall (s :: [*]). (a : b : s) :-> ((a, b) : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (a, b)
forall a b r (s0 :: [*]) (s1 :: [*]) (s2 :: [*]).
(forall (s :: [*]). (a : b : s) :-> (r : s))
-> Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r
binaryExpr forall (s :: [*]). (a : b : s) :-> ((a, b) : s)
forall a b (s :: [*]). (a : b : s) :-> ((a, b) : s)
pair

-- | Construct a list given the constructor for each element.
listE :: KnownValue a => [Expr s s a] -> Expr s s [a]
listE :: [Expr s s a] -> Expr s s [a]
listE = (Element [Expr s s a] -> Expr s s [a] -> Expr s s [a])
-> Expr s s [a] -> [Expr s s a] -> Expr s s [a]
forall t b. Container t => (Element t -> b -> b) -> b -> t -> b
foldr (\Element [Expr s s a]
pushElem Expr s s [a]
pushRec -> Element [Expr s s a]
Expr s s a
pushElem Expr s s a -> ((a : s) :-> (a : [a] : s)) -> s :-> (a : [a] : s)
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# Expr s s [a] -> (a : s) :-> (a : [a] : s)
forall a (s :: [*]) (s' :: [*]).
HasCallStack =>
(s :-> s') -> (a : s) :-> (a : s')
dip Expr s s [a]
pushRec (s :-> (a : [a] : s))
-> ((a : [a] : s) :-> ([a] : s)) -> Expr s s [a]
forall (a :: [*]) (b :: [*]) (c :: [*]).
(a :-> b) -> (b :-> c) -> a :-> c
# (a : [a] : s) :-> ([a] : s)
forall a (s :: [*]). (a : List a : s) :-> (List a : s)
cons) Expr s s [a]
forall p (s :: [*]). KnownValue p => s :-> (List p : s)
nil