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

{-# LANGUAGE PartialTypeSignatures #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | 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
  , ConstraintDuupXLorentz
  , ConstraintReplaceNLorentz
  , ConstraintUpdateNLorentz
  , DuupX (..)
  , ReplaceN (..)
  , UpdateN (..)
  , dropX
  , cloneX
  , duupX
  , framedN
  , 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

  -- * Buildable utils for additional Morley macros
  , buildView
  , buildViewTuple

  -- * Macros for working with @address@ and @contract@-like types
  , addressToEpAddress
  , pushContractRef
  ) where

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

import qualified Data.Kind as Kind
import Data.Singletons (SingI(..))
import Fmt (Buildable(..), Builder, pretty, tupleF, (+|), (|+))
import Fmt.Internal.Tuple (TupleF)
import qualified GHC.TypeLits as Lit
import GHC.TypeNats (type (-))
import qualified GHC.TypeNats as GHC (Nat)

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.Value
import Michelson.Typed (ConstraintDIG', ConstraintDIPN', ConstraintDUG', T)
import Michelson.Typed.Arith
import Michelson.Typed.Haskell.Value
import Util.Markdown
import Util.Peano
import Util.Type

----------------------------------------------------------------------------
-- 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), SingI (ToT 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
----------------------------------------------------------------------------

-- | Custom Lorentz macro that drops element with given index
-- (starting from 0) from the stack.
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)

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

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

-- | Constraint for duupX that combines kind-agnostic constraint for
-- Lorentz (Haskell) types and for our typed Michelson.
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 =
    -- 'stackType' helps GHC deduce types
    dipNPeano @('S ('S n)) (dup # stackType @(a ': a ': tail)) #
    digPeano @('S ('S 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 it is implemented differently for `n ≤ 2` and for `n > 2`.
-- In the latter case it is implemented using `dipN`, `dig` and `dup`.
-- In the former case it uses specialized versions.
-- There is also a minor difference with the implementation of `DUU*P` in
-- Michelson.
-- They implement `DUUUUP` as `DIP 3 { DUP }; DIG 4`.
-- We implement it as `DIP 3 { DUP }; DIG 3`. These are equivalent.
-- Our version is supposedly cheaper, at least it should be packed
-- more efficiently due to the way numbers are packed.
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

-- | 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.
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

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
    :: (NiceComparable k, KnownValue e)
    => (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 = failingWhenPresent mkErr # mapInsert
instance MapInstrs BigMap where
  mapUpdate = update
  mapInsertNew mkErr = failingWhenPresent mkErr # mapInsert

-- | Insert given element into set.
--
-- This is a separate function from 'updateMap' 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
  :: (NiceComparable e, KnownValue err)
  => (forall s0. e : s0 :-> err : s0)
  -> e & Set e & s :-> Set e & s
setInsertNew desc = dip (push True) # failingWhenPresent desc # 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 :: [Kind.Type]) (a :: Kind.Type)
  (mid :: [Kind.Type]) (tail :: [Kind.Type]) =
  ( ReplaceNConstraint' T n (ToTs s) (ToT a) (ToTs mid) (ToTs tail)
  , ReplaceNConstraint' Kind.Type n s a mid tail
  )

class ReplaceN (n :: Peano) (s :: [Kind.Type]) (a :: Kind.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) =>
  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 :: GHC.Nat) a (s :: [Kind.Type]) (s1 :: [Kind.Type]) (tail :: [Kind.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 :: [Kind.Type]) (a :: Kind.Type) (b :: Kind.Type)
  (mid :: [Kind.Type]) (tail :: [Kind.Type]) =
  ( UpdateNConstraint' T n (ToTs s) (ToT a) (ToT b) (ToTs mid) (ToTs tail)
  , UpdateNConstraint' Kind.Type n s a b mid tail
  )

class UpdateN (n :: Peano) (s :: [Kind.Type]) (a :: Kind.Type) (b :: Kind.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) =>
  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 :: GHC.Nat) a b (s :: [Kind.Type]) (mid :: [Kind.Type]) (tail :: [Kind.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 :: Kind.Type) (r :: Kind.Type) = View
  { viewParam :: a
  , viewCallbackTo :: ContractRef r
  } deriving stock (Eq, Show, Generic)
    deriving anyclass (HasAnnotation)

deriving anyclass instance (WellTypedIsoValue r, WellTypedIsoValue a) => IsoValue (View a r)

instance (CanCastTo a1 a2, CanCastTo r1 r2) => CanCastTo (View a1 r1) (View a2 r2)

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 <>
    [dTypeDep @(), dTypeDep @Integer]
  typeDocHaskellRep =
    haskellRepNoFields $ concreteTypeDocHaskellRep @(View () Integer)
  typeDocMichelsonRep =
    concreteTypeDocMichelsonRep @(View () Integer)

instance {-# OVERLAPPABLE #-} (Buildable a, WellTypedIsoValue r) => Buildable (View a r) where
  build = buildView build

instance {-# OVERLAPPING  #-} (WellTypedIsoValue r) => Buildable (View () r) where
  build = buildView $ const "()"

buildViewTuple :: (WellTypedIsoValue r, TupleF a) => View a r -> Builder
buildViewTuple = buildView tupleF

buildView :: (WellTypedIsoValue 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)
  => (forall s0. a & storage & s0 :-> r : s0)
  -> View a r & storage & s :-> (List Operation, storage) & s
view_ code =
  unwrapView #
  unpair # dip (duupX @2) # code # dip amount #
  transferTokens # nil # swap # cons # pair

-- | @void@ type synonym as described in A1.
data Void_ (a :: Kind.Type) (b :: Kind.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 (WellTypedIsoValue r, WellTypedIsoValue a) => IsoValue (Void_ a r)

instance (CanCastTo a1 a2, CanCastTo r1 r2) => CanCastTo (Void_ a1 r1) (Void_ a2 r2)

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)
      ]
  typeDocDependencies p =
    genericTypeDocDependencies p <>
    [dTypeDep @(), dTypeDep @Integer]
  typeDocHaskellRep p descr = do
    (_, rhs) <- haskellRepNoFields (concreteTypeDocHaskellRep @(Void_ () Integer)) p descr
    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 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 = 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 =
    [dTypeDep @MText, dTypeDep @r]

instance
  ( WellTypedIsoValue (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 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)

-- | 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 :: Kind.Type) (b :: Kind.Type) (s :: [Kind.Type]).
  a ': b ': s :-> a ': b ': a ': b ': s
dupTop2 = duupX @2 # duupX @2