-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# LANGUAGE NoStarIsType #-}

{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

-- | Common Michelson macros defined using Lorentz syntax.
module Lorentz.Macro
  ( -- * Compare
    NiceComparable
  , eq
  , neq
  , lt
  , gt
  , le
  , ge
  , ifEq0
  , ifGe0
  , ifGt0
  , ifLe0
  , ifLt0
  , ifNeq0
  , ifEq
  , ifGe
  , ifGt
  , ifLe
  , ifLt
  , ifNeq

  -- * Fail
  , fail_

  -- * Assertion macros
  -- |
  -- They differ from the same macros in Michelson, because those
  -- macros use FAIL macro which is not informative (fails with unit).
  -- If you __really__ want Michelson versions (maybe to produce exact
  -- copy of an existing contract), you can pass 'UnspecifiedError', then
  -- FAILWITH will be called with unit.
  , assert
  , assertEq0
  , assertNeq0
  , assertLt0
  , assertGt0
  , assertLe0
  , assertGe0
  , assertEq
  , assertNeq
  , assertLt
  , assertGt
  , assertLe
  , assertGe
  , assertNone
  , assertSome
  , assertLeft
  , assertRight
  , assertUsing

  -- * Syntactic Conveniences
  , 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

  -- * Additional Morley macros
  , View_ (..)
  , Void_ (..)
  , VoidResult(..)
  , view_
  , mkView_
  , wrapView_
  , unwrapView_
  , void_
  , mkVoid
  , wrapVoid
  , unwrapVoid
  , voidResultTag
  , dupTop2
  , fromOption
  , isSome
  , non
  , non'
  , isEmpty
  , NonZero (..)

  -- * Buildable utils for additional Morley macros
  , buildView_
  , buildViewTuple_

  -- * Macros for working with @address@ and @contract@-like types
  , addressToEpAddress
  , pushContractRef
  , selfAddress
  , view

  -- * Integer division
  , IDiv
  , IMod
  , idiv
  , imod
  ) where

import Prelude hiding (and, compare, drop, some, swap, view)

import Data.Constraint ((\\))
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

-- $setup
-- >>> :m +Lorentz.Base Lorentz.Run.Simple Lorentz.Instr
-- >>> import Prelude hiding (drop, not, compare, swap)

----------------------------------------------------------------------------
-- Compare
----------------------------------------------------------------------------

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), KnownIsoT 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

----------------------------------------------------------------------------
-- Fail
----------------------------------------------------------------------------

-- | Analog of the FAIL macro in Michelson. Its usage is discouraged
-- because it doesn't carry any information about failure.
{-# WARNING fail_ "'fail_' remains in code" #-}
fail_ :: a :-> c
fail_ = unit # failWith

----------------------------------------------------------------------------
-- Assertions
----------------------------------------------------------------------------

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

----------------------------------------------------------------------------
-- Syntactic Conveniences
----------------------------------------------------------------------------

-- | An instruction that always fails.
type ErrInstr s = forall serr. s :-> serr

-- | Custom Lorentz macro that drops element with given index
-- (starting from 0) from the stack.
dropX
  :: forall (n :: Nat) a inp out s s'.
  ( ConstraintDIPNLorentz (ToPeano n) inp out s s'
  , s ~ (a ': s')
  , SingIPeano n
  )
  => inp :-> out
dropX = dipN @n @inp @out @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 = 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 = cloneXImpl @n # dup

-- | Duplicate the top of the stack @n@ times.
--
-- For example, `cloneX @3` has type `a : s :-> a : a : a : a : s`.
cloneX
  :: forall (n :: Nat) a s. CloneX (ToPeano n) a s
  => a : s :-> a : CloneXT (ToPeano n) a s
cloneX = cloneXImpl @(ToPeano n)

-- | @DUU+P@ macro. For example, @duupX @3@ is @DUUUP@, it puts
-- the 3-rd (starting from 1) element to the top of the stack.
--
-- Note that @DUU+P@ has since been added as the @DUP n@ instruction and so this
-- macro is defined simply as follows:
--
-- > duupX = dupN @n
duupX
  :: forall (n :: Nat) a s s'.
     (ConstraintDUPNLorentz (ToPeano n) s s' a, Dupable a)
  => s :-> a ': s
duupX = dupN @n

-- | Version of 'framed' which accepts number of elements on input stack
-- which should be preserved.
--
-- You can treat this macro as calling a Michelson function with given number
-- of arguments.
--
-- Given a stack of 3 elements,
-- >>> arg = (1 :: Integer) ::: (2 :: Integer) ::: (3 :: Integer)
--
-- @framedN@ will have access to exactly the number of elements specified,
-- >>> framedN @1 drop -$ arg
-- 2 ::: 3
-- >>> framedN @1 (drop # drop) -$ arg
-- ...
-- ... error:
-- ... Couldn't match type: '[]
-- ...                with: a0 : o'0
-- ...
--
-- When the number of elements is larger than the size of the stack, @framedN@
-- will have access to all of them:
-- >>> framedN @5 (drop # drop) -$ arg
-- 3
--
-- But not more than there are on stack:
-- >>> framedN @5 (drop # drop # drop # drop) -$ arg
-- ...
-- ... error:
-- ... Couldn't match type ‘ZippedStackRepr a1 (ZippedStackRepr a0 out)’
-- ... with ‘Integer’
-- ...

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

carN
  :: forall (n :: Nat) (pair :: Type) (s :: [Type]).
     ConstraintPairGetLorentz (2 * n + 1) pair
  => pair : s :-> PairGetHs (ToPeano (2 * n + 1)) pair : s
carN = pairGet @(2 * n + 1)
  where
    _example :: '[ (String, (Integer, ())) ] :-> '[ String ]
    _example = carN @0

    _example' :: '[ (String, (Integer, ())) ] :-> '[ Integer ]
    _example' = carN @1

cdrN
  :: forall (n :: Nat) (pair :: Type) (s :: [Type]).
     ConstraintPairGetLorentz (2 * n) pair
  => pair : s :-> PairGetHs (ToPeano (2 * n)) pair : s
cdrN = pairGet @(2 * n)
  where
    _example :: '[ (String, (Integer, ())) ] :-> '[ (String, (Integer, ())) ]
    _example = cdrN @0

    _example' :: '[ (String, (Integer, ())) ] :-> '[ (Integer, ()) ]
    _example' = cdrN @1

    _example'' :: '[ (String, (Integer, ())) ] :-> '[ () ]
    _example'' = cdrN @2

-- |
-- >>> papair == pair # pair
-- True
--
-- >>> papair -$ True ::: 1 ::: ()
-- ((True,1),())
papair :: a : b : c : s :-> ((a, b), c) : s
papair = pair # pair

-- |
-- >>> ppaiir == dip pair # pair
-- True
--
-- >>> ppaiir -$ True ::: 1 ::: ()
-- (True,(1,()))
ppaiir :: a : b : c : s :-> (a, (b, c)) : s
ppaiir = dip pair # pair

-- |
-- >>> cdar == cdr # car
-- True
--
-- >>> cdar -$ (True, (1, ()))
-- 1
cdar :: (a1, (a2, b)) : s :-> a2 : s
cdar = cdr # car

-- |
-- >>> cddr == cdr # cdr
-- True
--
-- >>> cddr -$ (True, (1, ()))
-- ()
cddr :: (a1, (a2, b)) : s :-> b : s
cddr = cdr # cdr

-- |
-- >>> caar == car # car
-- True
--
-- >>> caar -$ ((True, 1), ())
-- True
caar :: ((a, b1), b2) : s :-> a : s
caar = car # car

-- |
-- >>> cadr == car # cdr
-- True
--
-- >>> cadr -$ ((True, 1), ())
-- 1
cadr :: ((a, b1), b2) : s :-> b1 : s
cadr = car # cdr

-- |
-- >>> setCar == cdr # swap # pair
-- True
--
-- >>> setCar -$ (True, 1) ::: ()
-- ((),1)
setCar :: (a, b1) : (b2 : s) :-> (b2, b1) : s
setCar = cdr # swap # pair

-- |
-- >>> setCdr == car # pair
-- True
--
-- >>> setCdr -$ (True, 1) ::: ()
-- (True,())
setCdr :: (a, b1) : (b2 : s) :-> (a, b2) : s
setCdr = car # pair

-- |
-- >>> mapCar (not @Bool) == unpair # (not @Bool) # pair
-- True
--
-- >>> mapCar not -$ (True, 1)
-- (False,1)
mapCar
  :: (forall s0. a : s0 :-> a1 : s0)
  -> (a, b) : s :-> (a1, b) : s
mapCar op = unpair # op # pair

-- |
-- >>> mapCdr (not @Bool) == unpair # dip (not @Bool) # pair
-- True
--
-- >>> mapCdr not -$ (1, True)
-- (1,False)
mapCdr
  :: (forall s0. b : s0 :-> b1 : s0)
  -> (a, b) : s :-> (a, b1) : s
mapCdr op = unpair # dip op # pair

-- |
-- >>> ifRight (not @Bool) (dup @Integer # compare # eq0) == ifLeft (dup @Integer # compare # eq0) (not @Bool)
-- True
--
-- >>> ifRight not (dup # compare # eq0) -$ (Right True :: Either Integer Bool)
-- False
--
-- >>> ifRight not (dup # compare # eq0) -$ (Left 1 :: Either Integer Bool)
-- True
ifRight :: (b : s :-> s') -> (a : s :-> s') -> (Either a b : s :-> s')
ifRight l r = ifLeft r l


-- |
-- >>> ifSome (dup @Integer # compare # eq0) (push False) == ifNone (push False) (dup @Integer # compare # eq0)
-- True
--
-- >>> ifSome (dup # compare # eq0) (push False) -$ (Just 1 :: Maybe Integer)
-- True
--
-- >>> ifSome (dup # compare # eq0) (push False) -$ (Nothing :: Maybe Integer)
-- False
ifSome
  :: (a : s :-> s') -> (s :-> s') -> (Maybe a : s :-> s')
ifSome s n = ifNone n s


-- |
-- >>> when_ (push 5 # add @Integer @Integer) == if_ (push 5 # add @Integer @Integer) nop
-- True
--
-- >>> when_ (push 5 # add @Integer) -$ True ::: 3
-- 8
--
-- >>> when_ (push 5 # add @Integer) -$ False ::: 3
-- 3
when_ :: (s :-> s) -> (Bool : s :-> s)
when_ i = if_ i nop

-- |
-- >>> unless_ (push 5 # add @Integer @Integer) == if_ nop (push 5 # add @Integer @Integer)
-- True
--
-- >>> unless_ (push 5 # add @Integer) -$ True ::: 3
-- 3
--
-- >>> unless_ (push 5 # add @Integer) -$ False ::: 3
-- 8
unless_ :: (s :-> s) -> (Bool : s :-> s)
unless_ i = if_ nop i

-- |
-- >>> whenSome drop == ifSome drop nop
-- True
--
-- >>> whenSome drop -$ Just 1 ::: ()
-- ()
whenSome :: (a : s :-> s) -> (Maybe a : s :-> s)
whenSome i = ifSome i nop

-- |
-- >>> whenNone (push True) == ifNone (push True) nop
-- True
--
-- >>> whenNone (push 1) -$ (Nothing :: Maybe Integer)
-- 1
whenNone :: (s :-> a : s) -> (Maybe a : s :-> a : s)
whenNone i = ifNone i nop

-- | Various convenient instructions on maps.
class MapInstrs map where
  -- | Specialized version of 'update'.
  mapUpdate :: NiceComparable k => k : Maybe v : map k v : s :-> map k v : s

  -- | Insert given element into map.
  mapInsert :: NiceComparable k => k : v : map k v : s :-> map k v : s
  mapInsert = dip some # mapUpdate

  -- | Insert given element into map, ensuring that it does not overwrite
  -- any existing entry.
  --
  -- As first argument accepts container name (for error message).
  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

  -- | Delete element from the map.
  deleteMap
    :: forall k v s. (NiceComparable 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 =
    dip some # dup # dip getAndUpdate # swap # ifNone drop (drop # mkErr # failWith)
instance MapInstrs BigMap where
  mapUpdate = update
  mapInsertNew mkErr =
    dip some # dup # dip getAndUpdate # swap # ifNone drop (drop # mkErr # failWith)

-- | Insert given element into set.
--
-- This is a separate function from 'mapUpdate' because stacks they operate with
-- differ in length.
setInsert :: NiceComparable e => e : Set e : s :-> Set e : s
setInsert = dip (push True) # update

-- | Insert given element into set, ensuring that it does not overwrite
-- any existing entry.
--
-- As first argument accepts container name.
setInsertNew
  :: (NiceConstant err, NiceComparable e, Dupable e, Dupable (Set e))
  => (forall s0. e : s0 :-> err : s0)
  -> e : Set e : s :-> Set e : s
setInsertNew desc =
  dupTop2 # mem #
  if_ (desc # failWith) (dip (push True) # update)

-- | Delete given element from the set.
setDelete :: NiceComparable e => e : Set e : s :-> Set e : s
setDelete = dip (push False) # update

-- | Kind-agnostic constraint for replaceN
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
  )

-- | Constraint for replaceN that combines kind-agnostic constraint for
-- Lorentz (Haskell) types and for our typed Michelson.
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 = swap # drop

instance {-# OVERLAPPABLE #-} (ConstraintReplaceNLorentz ('S n) s a mid tail, SingI n) =>
  ReplaceN ('S ('S n)) s a mid tail where
  replaceNImpl =
    -- 'stackType' helps GHC deduce types
    dipNPeano @('S ('S n)) (stackType @(a ': tail) # drop) # dugPeano @('S n)

-- | Replace nth element (0-indexed) with the one on the top of the stack.
-- For example, `replaceN @3` replaces the 3rd element with the 0th one.
-- `replaceN @0` is not a valid operation (and it is not implemented).
-- `replaceN @1` is equivalent to `swap # drop` (and is the only one implemented
-- like this).
-- In all other cases `replaceN @n` will drop the nth element (`dipN @n drop`)
-- and then put the 0th one in its place (`dug @(n-1)`).
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 = replaceNImpl @(ToPeano n) @s @a @s1 @tail
  where
    _example ::
      '[ Integer, (), Integer, Bool ] :->
      '[ (), Integer, Bool ]
    _example = replaceN @2

-- | Kind-agnostic constraint for updateN
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)
  )

-- | Constraint for updateN that combines kind-agnostic constraint for
-- Lorentz (Haskell) types and for our typed Michelson.
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 instr = framed instr

instance {-# OVERLAPPING #-} (s ~ (x ': b ': tail)) => UpdateN ('S ('S 'Z)) s a b mid tail where
  updateNImpl instr = swap # dip (framed 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 instr =
    -- 'stackType' helps GHC deduce types
    dugPeano @('S ('S n)) # dipNPeano @('S ('S n)) (framed instr # stackType @(b ': tail))

-- | Replaces the nth element (0-indexed) with the result of the given "updating"
-- instruction (binary with the return type equal to the second argument) applied
-- to the 0th element and the nth element itself.
-- For example, @updateN \@3 cons@ replaces the 3rd element with the result of
-- @cons@ applied to the topmost element and the 3rd one.
-- @updateN \@0 instr@ is not a valid operation (and it is not implemented).
-- @updateN \@1 instr@ is equivalent to @instr@ (and so is implemented).
-- @updateN \@2 instr@ is equivalent to @swap # dip instr@ (and so is implemented).
-- In all other cases @updateN \@n instr@ will put the topmost element right above
-- the nth one (@dug \@(n-1)@) and then apply the function to them in place
-- (@dipN \@(n-1) instr@).
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 instr = updateNImpl @(ToPeano n) @s @a @b @mid @tail instr
  where
    _example ::
      '[ Integer, (), (), [Integer], Bool ] :->
      '[ (), (), [Integer], Bool ]
    _example = updateN @3 cons

----------------------------------------------------------------------------
-- Additional Morley macros
----------------------------------------------------------------------------

-- | @view@ type synonym as described in A1.
data View_ (a :: Type) (r :: Type) = View_
  { viewParam :: a
  , viewCallbackTo :: ContractRef r
  } deriving stock (Eq, Show, Generic)
    deriving anyclass (HasAnnotation)

deriving anyclass instance (HasNoOpToT 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 _ = "View"
  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 <>
    [dTypeDep @MText, dTypeDep @Integer]
  typeDocHaskellRep =
    haskellRepNoFields $ concreteTypeDocHaskellRep @(View_ MText Integer)
  typeDocMichelsonRep =
    concreteTypeDocMichelsonRep @(View_ MText Integer)

instance {-# OVERLAPPABLE #-} (Buildable a, HasNoOpToT r) => Buildable (View_ a r) where
  build = buildView_ build

instance {-# OVERLAPPING  #-} (HasNoOpToT r) => Buildable (View_ () r) where
  build = buildView_ $ const "()"

buildViewTuple_ :: (HasNoOpToT r, TupleF a) => View_ a r -> Builder
buildViewTuple_ = buildView_ tupleF

buildView_ :: (HasNoOpToT r) => (a -> Builder) -> View_ a r -> Builder
buildView_ bfp (View_ {..}) =
  "(View param: " +| bfp viewParam |+ " callbackTo: " +| viewCallbackTo |+ ")"

-- | Polymorphic version of 'View_' constructor.
mkView_ :: ToContractRef r contract => a -> contract -> View_ a r
mkView_ a c = View_ a (toContractRef c)

-- | Wrap internal representation of view into 'View_' itself.
--
-- 'View_' is part of public standard and should not change often.
wrapView_ :: (a, ContractRef r) : s :-> View_ a r : s
wrapView_ = forcedCoerce_

-- | Unwrap 'View_' into its internal representation.
--
-- 'View_' is part of public standard and should not change often.
unwrapView_ :: View_ a r : s :-> (a, ContractRef r) : s
unwrapView_ = forcedCoerce_

view_ ::
     (NiceParameter r, Dupable storage, IsNotInView)
  => (forall s0. a : storage : s0 :-> r : s0)
  -> View_ a r : storage : s :-> (List Operation, storage) : s
view_ code =
  unwrapView_ #
  unpair # dip (dupN @2) # code # dip amount #
  transferTokens # nil # swap # cons # pair

-- | @void@ type synonym as described in A1.
data Void_ (a :: Type) (b :: Type) = Void_
  { voidParam :: a
    -- ^ Entry point argument.
  , voidResProxy :: Lambda b b
    -- ^ Type of result reported via 'failWith'.
  } deriving stock (Generic, Show)
    deriving anyclass (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 _ = "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 =
    -- Avoiding trailing underscore
    customTypeDocMdReference
      ("Void", DType tp)
      [ DType (Proxy @a)
      , DType (Proxy @r)

        -- for examples
      , DType (Proxy @MText)
      , DType (Proxy @Integer)
      ]
  typeDocDependencies p =
    genericTypeDocDependencies p <>
    [dTypeDep @(), dTypeDep @Integer]
  typeDocHaskellRep p descr = do
    (_, rhs) <- haskellRepNoFields (concreteTypeDocHaskellRep @(Void_ MText Integer)) p descr
    return (Just "Void MText Integer", rhs)
  typeDocMichelsonRep p =
    let (_, rhs) = concreteTypeDocMichelsonRep @(Void_ MText Integer) p
    in (Just "Void MText Integer", rhs)

instance Buildable a => Buildable (Void_ a b) where
  build Void_ {..} = "(Void param: " +| voidParam |+ ")"

-- | Newtype over void result type used in tests to
-- distinguish successful void result from other errors.
--
-- Usage example:
-- lExpectFailWith (== VoidResult roleMaster)`
--
-- This error is special - it can contain arguments of different types
-- depending on entrypoint which raises it.
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 = unsafeConcreteTypeDocHaskellRep @(VoidResultRep Integer)
  typeDocMichelsonRep = unsafeConcreteTypeDocMichelsonRep @(VoidResultRep Integer)

instance (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 =
    [dTypeDep @MText, dTypeDep @r]

instance
  ( 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 = error "impossible"
  fromVal = error "impossible"

mkVoid :: forall b a. a -> Void_ a b
mkVoid a = Void_ a (mkLambda nop)

void_
  :: forall a b s s' anything.
      (IsError (VoidResult b), NiceConstant b)
  => a : s :-> b : s' -> Void_ a b : s :-> anything
void_ code =
  doc (DThrows (Proxy @(VoidResult b))) #
  unwrapVoid #
  unpair # swap # dip code # swap # exec #
  push voidResultTag # pair # failWith @(MText, b)

-- | Wrap internal representation of void into 'Void_' itself.
--
-- 'Void_' is part of public standard and should not change often.
wrapVoid :: (a, Lambda b b) : s :-> Void_ a b : s
wrapVoid = forcedCoerce_

-- | Unwrap 'Void_' into its internal representation.
--
-- 'Void_' is part of public standard and should not change often.
unwrapVoid :: Void_ a b : s :-> (a, Lambda b b) : s
unwrapVoid = forcedCoerce_

addressToEpAddress :: Address : s :-> EpAddress : s
addressToEpAddress = forcedCoerce_

-- | Push a value of @contract@ type.
--
-- Doing this via 'push' instruction is not possible, so we need to perform
-- extra actions here.
--
-- Aside from @contract@ value itself you will need to specify which error to
-- throw in case this value is not valid.
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)

-- | Duplicate two topmost items on top of the stack.
dupTop2
  :: forall (a :: Type) (b :: Type) (s :: [Type]).
     (Dupable a, Dupable b)
  => a ': b ': s :-> a ': b ': a ': b ': s
dupTop2 = dupN @2 # dupN @2

fromOption
  :: (NiceConstant a)
  => a -> Maybe a : s :-> a : s
fromOption a = ifSome nop (push a)

isSome :: Maybe a : s :-> Bool : s
isSome = ifSome (drop # push True) (push False)

-- | Retain the value if it is not equal to the given one.
--
-- >>> non 0 -$ 5
-- Just 5
-- >>> non 0 -$ 0
-- Nothing
non
  :: (NiceConstant a, NiceComparable a)
  => a -> a : s :-> Maybe a : s
non a = non' (push a # eq)

-- | Version of 'non' with a custom predicate.
--
-- >>> non' eq0 -$ 5
-- Just 5
-- >>> non' eq0 -$ 0
-- Nothing
non'
  :: (NiceConstant a)
  => ('[a] :-> '[Bool]) -> a : s :-> Maybe a : s
non' p = dup # framed p # if_ (drop # none) some

-- | Check whether container is empty.
isEmpty :: SizeOpHs c => c : s :-> Bool : s
isEmpty = size # int # eq0

class NonZero t where
  -- | Retain the value only if it is not zero.
  nonZero :: t : s :-> Maybe t : s

instance NonZero Integer where
  nonZero = dup # eq0 # if_ (drop # none) some

instance NonZero Natural where
  nonZero = dup # int # eq0 # if_ (drop # none) some

instance (NiceComparable d) => NonZero (Ticket d) where
  nonZero =
    readTicket # toField #rtAmount # int # eq0 # if_ (drop # none) some

type instance ErrorArg "no_view" = MText
instance CustomErrorHasDoc "no_view" where
  customErrClass = ErrClassBadArgument
  customErrDocMdCause =
    "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 = Just "view name"

-- | Call a view.
--
-- Accepts the view name via a type annotation.
-- This internally asserts the view to be present, as if the supplied
-- @TAddress@ argument is valid, the view is guaranteed to be called
-- successfully.
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 =
  dip checkedCoerce_ # view' @name #
  ifSome nop (push (viewNameToMText viewName) # failCustom #no_view)
  \\ niceViewableEvi @ret
  where
    viewName = demoteViewName @name
    _needHasView = Dict @(HasView vd name arg ret)

-- | Michelson supports only `EDiv`, which gives both the quotient and the
-- remainder for integers. For convenience, we also offer `IDiv`, which gives
-- just the quotient.
data IDiv

instance (ArithOpHs EDiv n d (Maybe (q, r)), mq ~ Maybe q, KnownValue q) => ArithOpHs IDiv n d mq where
  evalArithOpHs = evalArithOpHs @EDiv @n @d @(Maybe (q, r)) # lmap car

-- | Integer division.
--
-- >>> idiv -$ (5 :: Integer) ::: (2 :: Integer)
-- Just 2
--
-- >>> idiv -$ (5 :: Integer) ::: (0 :: Integer)
-- Nothing
idiv
  :: ArithOpHs IDiv n d q
  => n : d : s :-> q : s
idiv = evalArithOpHs @IDiv

-- | Michelson supports only `EDiv`, which gives both the quotient and the
-- remainder for integers. For convenience, we also offer `IMod`, which gives
-- just the remainder.
data IMod

instance (ArithOpHs EDiv n d (Maybe (q, r)), mr ~ Maybe r, KnownValue r) => ArithOpHs IMod n d mr where
  evalArithOpHs = evalArithOpHs @EDiv @n @d @(Maybe (q, r)) # lmap cdr

-- | Integer modulus.
--
-- >>> imod -$ (5 :: Integer) ::: (2 :: Integer)
-- Just 1
--
-- >>> imod -$ (5 :: Integer) ::: (0 :: Integer)
-- Nothing
imod
  :: ArithOpHs IMod n d r
  => n : d : s :-> r : s
imod = evalArithOpHs @IMod