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

module Test.Interpreter.Annotations
  ( test_cast_notes
  , test_complex_instructions_notes
  , test_interpret_stack
  , test_update_notes
  , test_create_contract_notes
  , unit_PAIRN_doesnt_convert_anns_but_UNPAIRN_does
  , unit_GETN_adds_var_ann
  , unit_GET_0_deletes_var_ann
  , unit_UPDATEN_field_anns
  , unit_UPDATEN_var_anns
  , unit_GET_AND_UPDATE_anns
  , test_dupn
  , test_nested_annots
  , unit_CARk_CDRk_interact_with_annotations
  , unit_CAR_special_annotations
  , unit_CDR_special_annotations
  , unit_UNPAIR_special_annotations
  , test_special_annotations
  ) where

import Debug qualified (show)
import Prelude hiding (Const)
import Unsafe qualified

import Control.Lens (ix, makeLensesFor, (<<%=))
import Control.Monad.RWS.Strict (RWST, runRWST)
import Data.List qualified as List
import Data.Map.Strict qualified as Map
import Data.Vinyl (Rec(..))
import Data.Vinyl.Functor (Const(..))
import Data.Vinyl.Recursive (recordToList, rmap)
import Fmt (pretty)
import Test.Tasty (TestTree)
import Test.Tasty.HUnit (Assertion, assertEqual, assertFailure, testCase)

import Morley.Michelson.ErrorPos (InstrCallStack(..), srcPos)
import Morley.Michelson.Interpret
  (ContractEnv, InstrRunner, InterpreterState(..), InterpreterStateMonad(..),
  MichelsonFailureWithStack(..), MorleyLogsBuilder, StkEl(..), initInterpreterState, mkInitStack,
  runInstrImpl, starNotesStkEl)
import Morley.Michelson.Parser (notes)
import Morley.Michelson.Runtime.Dummy (dummyBigMapCounter, dummyContractEnv, dummyGlobalCounter)
import Morley.Michelson.Runtime.GState (genesisAddress)
import Morley.Michelson.Text (MText)
import Morley.Michelson.Typed (Notes(..), Operation, Value'(..), starNotes, starParamNotes, toVal)
import Morley.Michelson.Typed qualified as T
import Morley.Michelson.Untyped (noAnn)
import Morley.Michelson.Untyped qualified as U
import Morley.Tezos.Address (Address, parseAddress)
import Morley.Util.Sing (eqParamSing)
import Test.Cleveland.Instances ()
import Test.Cleveland.Michelson (importContract)
import Text.Show qualified

import Test.Util.Contracts (contractsDir, (</>))

data SomeStackElem = forall t. SomeStackElem (StkEl t)

instance Eq SomeStackElem where
  SomeStackElem (StkEl v1 vn1 n1) == SomeStackElem (StkEl v2 vn2 n2) =
    v1 `T.eqValueExt` v2
      && vn1 == vn2
      && T.withValueTypeSanity v1 (T.withValueTypeSanity v2 (n1 `eqParamSing` n2))

data SomeStack where
  SomeStack :: forall s. Rec StkEl s -> SomeStack

instance Show SomeStack where
  show (SomeStack v) = case v of
    RNil -> "[]"
    x :& xs -> Debug.show x <> " :& " <> Debug.show (SomeStack xs)

instance Eq SomeStack where
  a == b = stackToElems a == stackToElems b
    where
      stackToElems :: SomeStack -> [SomeStackElem]
      stackToElems (SomeStack stack) = recordToList $ rmap (Const . SomeStackElem) stack

data TestInterpreterState = TestInterpreterState
  { _tisInterpreterState :: InterpreterState
  , _tisStacks :: [Maybe SomeStack]
    -- ^ A list of the stacks we expect to see after running each instruction.
    -- Use 'Nothing' when you don't care what the stack looks like at that step.
  }

makeLensesFor [("_tisStacks", "tisStacks")] ''TestInterpreterState

someStack :: Rec StkEl s -> Maybe SomeStack
someStack = Just . SomeStack

ignoreStack :: Maybe SomeStack
ignoreStack = Nothing

instance (Monad m, Monoid w) => InterpreterStateMonad (RWST r w TestInterpreterState m) where
  stateInterpreterState f = state
      (\TestInterpreterState{..} ->
        let (a, newSt) = f _tisInterpreterState in (a, TestInterpreterState{_tisInterpreterState=newSt,..}))

type TestInstrRunner = InstrRunner (ExceptT MichelsonFailureWithStack $ RWST ContractEnv MorleyLogsBuilder TestInterpreterState IO)

runInstrTest :: HasCallStack => TestInstrRunner
runInstrTest = runInstrTestImpl False

runInstrTestImpl :: HasCallStack => Bool -> TestInstrRunner
runInstrTestImpl skipInstr instr stack = do
  actualStack <- runInstrImpl (runInstrTestImpl $ isAnnotated instr) instr stack
  when (isRealInstr instr && not skipInstr) do
    (tisStacks <<%= Unsafe.tail) <&> Unsafe.head >>= \case
      Nothing ->
        -- We don't care what the stack looks like at this step, so we do nothing here.
        pass
      Just expectedStack ->
        -- We care what the stack looks like at this step,
        -- so we check whether it matches our expectation.
        liftIO $
          assertEqual
            (List.unlines
              [ "Actual stack did not match the expected stack after running this instruction:"
              , "  " <> pretty (T.instrToOps instr)
              ]
            )
            expectedStack
            (SomeStack actualStack)
  pure actualStack

isAnnotated :: T.Instr a b -> Bool
isAnnotated = \case
  T.InstrWithVarNotes{} -> True
  T.InstrWithVarAnns{} -> True
  T.InstrWithNotes{} -> True
  _ -> False

isRealInstr :: T.Instr a b -> Bool
isRealInstr = \case
  T.DocGroup{} -> False
  T.Seq{} -> False
  T.Nop -> False
  T.WithLoc{} -> False
  T.Nested{} -> False
  _ -> True

stackAnnotationsTest
  :: HasCallStack
  => String
  -> Rec StkEl (T.ContractInp cp st)
  -> [Maybe SomeStack]
  -> T.Contract cp st
  -> TestTree
stackAnnotationsTest description initialStack expectedStacks contract =
  testCase description $
    stackAnnotationsAssertion initialStack expectedStacks contract

stackAnnotationsAssertion
  :: HasCallStack
  => Rec StkEl (T.ContractInp cp st)
  -> [Maybe SomeStack]
  -> T.Contract cp st
  -> Assertion
stackAnnotationsAssertion initialStack expectedStacks contract = do
  let initialState =
        TestInterpreterState
          (initInterpreterState dummyGlobalCounter dummyBigMapCounter dummyContractEnv)
          expectedStacks
  let action = runInstrImpl runInstrTest (T.cCode contract) initialStack
  (result, finalState, _logs) <- runRWST (runExceptT action) dummyContractEnv initialState

  assertEqual
    "Finished interpreting contract, but we still expected more instructions to be run."
    []
    (finalState ^. tisStacks)

  whenLeft result (assertFailure . pretty)

ops :: T.Value ('T.TList 'T.TOperation)
ops = T.VList []

test_complex_instructions_notes :: IO [TestTree]
test_complex_instructions_notes = concat <$> sequenceA
  [ importContract (contractsDir </> "if-none-annots.tz") <&> \contract ->
    [ stackAnnotationsTest
        "IF_NONE preserves its annotations with None (morley-debugger#4)"
        (starNotesStkEl (T.VPair (T.VOption Nothing, T.VInt 0)) :& RNil)
        expectedStacksIF_NONE_None
        contract
    , stackAnnotationsTest
        "IF_NONE preserves its annotations with Some (morley-debugger#4)"
        (starNotesStkEl (T.VPair (T.VOption $ Just $ T.VInt 6, T.VInt 0)) :& RNil)
        expectedStacksIF_NONE_Some
        contract
    ]
  , importContract (contractsDir </> "if-left-annots.tz") <&> \contract ->
    [ stackAnnotationsTest
        "IF_LEFT preserves its annotations with Left (morley-debugger#4)"
        (starNotesStkEl (T.VPair (T.VOr $ Left $ T.VInt 6, T.VInt 0)) :& RNil)
        expectedStacksIF_LEFT_Left
        contract
    , stackAnnotationsTest
        "IF_LEFT preserves its annotations with Right (morley-debugger#4)"
        (starNotesStkEl (T.VPair (T.VOr $ Right $ T.VInt 7, T.VInt 0)) :& RNil)
        expectedStacksIF_LEFT_Right
        contract
    ]
  , importContract (contractsDir </> "if-cons-annots.tz") <&> \contract ->
    [ stackAnnotationsTest
        "IF_CONS preserves its annotations with {10} (morley-debugger#4)"
        (starNotesStkEl (T.VPair (T.VList [T.VInt 10], T.VInt 0)) :& RNil)
        expectedStacksIF_CONS_Cons
        contract
    , stackAnnotationsTest
        "IF_CONS preserves its annotations with {} (morley-debugger#4)"
        (starNotesStkEl (T.VPair (T.VList [], T.VInt 0)) :& RNil)
        expectedStacksIF_CONS_Nil
        contract
    ]
  ]
  where
    y :: T.Notes 'T.TInt
    y = [notes|int :y|]

    param = "parameter"

    expectedStacksIF_NONE_None :: [Maybe SomeStack]
    expectedStacksIF_NONE_None =
      [ -- CAR
        someStack $ StkEl (T.VOption @'T.TInt Nothing) param [notes|option (int :y)|] :& RNil
        -- PUSH (int :y) 0
      , someStack $ StkEl (T.VInt 0) U.noAnn y :& RNil
        -- IF_NONE
      , someStack $ StkEl (T.VInt 0) U.noAnn y :& RNil
        -- NIL operation
        -- PAIR
      , ignoreStack, ignoreStack
      ]

    expectedStacksIF_NONE_Some :: [Maybe SomeStack]
    expectedStacksIF_NONE_Some =
      [ -- CAR
        someStack $ StkEl (T.VOption $ Just $ T.VInt 6) param [notes|option (int :y)|] :& RNil
        -- PUSH (int :y) 1
      , someStack $ StkEl (T.VInt 1) U.noAnn y :& StkEl (T.VInt 6) param y :& RNil
        -- ADD
      , someStack $ StkEl (T.VInt 7) U.noAnn y :& RNil
        -- IF_NONE
      , someStack $ StkEl (T.VInt 7) U.noAnn y :& RNil
        -- NIL operation
        -- PAIR
      , ignoreStack, ignoreStack
      ]

    expectedStacksIF_LEFT_Left :: [Maybe SomeStack]
    expectedStacksIF_LEFT_Left =
      [ -- CAR
        someStack $ StkEl (T.VOr @'T.TInt $ Left $ T.VInt 6) param [notes|or (int :y) (int :y)|] :& RNil
        -- PUSH (int :y) 1
      , someStack $ StkEl (T.VInt 1) U.noAnn y :& StkEl (T.VInt 6) param y :& RNil
        -- ADD
      , someStack $ StkEl (T.VInt 7) U.noAnn y :& RNil
        -- IF_LEFT
      , someStack $ StkEl (T.VInt 7) U.noAnn y :& RNil
        -- NIL operation
        -- PAIR
      , ignoreStack, ignoreStack
      ]

    expectedStacksIF_LEFT_Right :: [Maybe SomeStack]
    expectedStacksIF_LEFT_Right =
      [ -- CAR
        someStack $ StkEl (T.VOr @'T.TInt $ Right $ T.VInt 7) param [notes|or (int :y) (int :y)|] :& RNil
        -- PUSH (int :y) 2
      , someStack $ StkEl (T.VInt 2) U.noAnn y :& StkEl (T.VInt 7) param y :& RNil
        -- ADD
      , someStack $ StkEl (T.VInt 9) U.noAnn y :& RNil
        -- IF_LEFT
      , someStack $ StkEl (T.VInt 9) U.noAnn y :& RNil
        -- NIL operation
        -- PAIR
      , ignoreStack, ignoreStack
      ]

    expectedStacksIF_CONS_Cons :: [Maybe SomeStack]
    expectedStacksIF_CONS_Cons =
      [ -- CAR
        someStack $ StkEl (T.VList [T.VInt 10]) param [notes|list (int :y)|] :& RNil
        -- DROP
      , someStack $ RNil
        -- DIP
      , someStack $ StkEl (T.VInt 10) param y :& RNil
        -- IF_CONS
      , someStack $ StkEl (T.VInt 10) param y :& RNil
        -- NIL operation
        -- TODO: This param should not be here, probably related to #507
      , someStack $ starNotesStkEl ops :& StkEl (T.VInt 10) param y :& RNil
        -- PAIR
      , ignoreStack
      ]

    expectedStacksIF_CONS_Nil :: [Maybe SomeStack]
    expectedStacksIF_CONS_Nil =
      [ -- CAR
        someStack $ StkEl (T.VList @'T.TInt []) param [notes|list (int :y)|] :& RNil
        -- PUSH (int :y) 0
      , someStack $ StkEl (T.VInt 0) U.noAnn y :& RNil
        -- IF_CONS
      , someStack $ StkEl (T.VInt 0) U.noAnn y :& RNil
        -- NIL operation
        -- PAIR
      , ignoreStack, ignoreStack
      ]

test_cast_notes :: IO [TestTree]
test_cast_notes = sequenceA
  [ importContract (contractsDir </> "cast-annots.tz") <&>
    stackAnnotationsTest
      "CAST can remove and add annotations (morley-debugger#2, morley-debugger#4)"
      (starNotesStkEl (T.VPair (T.VUnit, T.VPair (T.VInt 0, T.VInt 0))) :& RNil)
      expectedStacksCast
  ]
  where
    notesPair :: T.Notes ('T.TPair 'T.TInt 'T.TInt)
    notesPair = [notes|pair :q (int :x) (int :y)|]

    pair :: T.Value ('T.TPair 'T.TInt 'T.TInt)
    pair = T.VPair (T.VInt 1, T.VInt 2)

    expectedStacksCast :: [Maybe SomeStack]
    expectedStacksCast =
      [ -- DROP
        someStack RNil
        -- PUSH @ab (pair :p (int :a) (int :b)) (Pair 1 2)
      , someStack $ StkEl
        pair
        "ab"
        [notes|pair :p (int :a) (int :b)|] :& RNil
        -- CAST (pair int int)
      , someStack $ StkEl pair "ab" T.starNotes :& RNil
        -- CAST @xy (pair (int :x) (int :y))
      , someStack $ StkEl pair "xy" notesPair :& RNil
        -- NIL operation
      , ignoreStack
        -- PAIR
      , someStack $ StkEl (T.VPair (ops, pair)) noAnn (NTPair noAnn noAnn noAnn noAnn "xy" starNotes notesPair) :& RNil
      ]

test_interpret_stack :: IO [TestTree]
test_interpret_stack = sequenceA
  [ importContract (contractsDir </> "loop-annots.tz") <&>
    stackAnnotationsTest
      "Annotations should be preserved in LOOP (morley-debugger#4)"
      (starNotesStkEl (T.VPair (T.VUnit, T.VInt 0)) :& RNil)
      expectedStacksLoop
  , importContract (contractsDir </> "map-annots.tz") <&>
    stackAnnotationsTest
      "Annotations should be preserved in MAP (morley-debugger#4)"
      (starNotesStkEl (T.VPair (T.VUnit, T.VInt 0)) :& RNil)
      expectedStacksMap
  ]
  where
    q :: T.Notes 'T.TInt
    q = [notes|int :q|]

    qv :: U.VarAnn
    qv = "q"

    expectedStacksLoop :: [Maybe SomeStack]
    expectedStacksLoop =
      [ -- DROP
        someStack RNil
        -- PUSH @q (int :q) 2
      , someStack $ StkEl (T.VInt 2) qv q :& RNil
        -- PUSH bool True
      , someStack $ starNotesStkEl (T.VBool True) :& StkEl (T.VInt 2) qv q :& RNil
        -- CAST int
      , someStack $ StkEl (T.VInt 2) qv T.starNotes :& RNil
        -- RENAME
      , someStack $ starNotesStkEl (T.VInt 2) :& RNil
        -- PUSH int -1
      , someStack $ starNotesStkEl (T.VInt (-1)) :& starNotesStkEl (T.VInt 2) :& RNil
        -- ADD
      , someStack $ starNotesStkEl (T.VInt 1) :& RNil
        -- DUP
      , someStack $ starNotesStkEl (T.VInt 1) :& starNotesStkEl (T.VInt 1) :& RNil
        -- GT
      , someStack $ starNotesStkEl (T.VBool True) :& starNotesStkEl (T.VInt 1) :& RNil
        -- CAST int
      , someStack $ StkEl (T.VInt 1) qv T.starNotes :& RNil
        -- RENAME
      , someStack $ starNotesStkEl (T.VInt 1) :& RNil
        -- PUSH int -1
      , someStack $ starNotesStkEl (T.VInt (-1)) :& starNotesStkEl (T.VInt 1) :& RNil
        -- ADD
      , someStack $ starNotesStkEl (T.VInt 0) :& RNil
        -- DUP
      , someStack $ starNotesStkEl (T.VInt 0) :& starNotesStkEl (T.VInt 0) :& RNil
        -- GT
      , someStack $ starNotesStkEl (T.VBool False) :& starNotesStkEl (T.VInt 0) :& RNil
        -- n.b.: these LOOP instructions are an implementation detail in Morley
        -- and do not appear in tezos-client while running an script with the
        -- --trace-stack flag.
        -- LOOP
      , someStack $ StkEl (T.VInt 0) U.noAnn T.starNotes :& RNil
        -- LOOP
      , someStack $ StkEl (T.VInt 0) U.noAnn T.starNotes :& RNil
        -- LOOP
      , someStack $ StkEl (T.VInt 0) qv q :& RNil
        -- NIL operation
      , ignoreStack
        -- PAIR
      , someStack $ StkEl (T.VPair (ops, T.VInt 0)) noAnn (NTPair noAnn noAnn noAnn noAnn "q" starNotes q) :& RNil
      ]

    y :: T.Notes 'T.TInt
    y = [notes|int :y|]

    yv :: U.VarAnn
    yv = "y"

    expectedStacksMap :: [Maybe SomeStack]
    expectedStacksMap =
      [ -- DROP
        someStack $ RNil
        -- PUSH @y (int :y) 42
      , someStack $ StkEl (T.VInt 42) yv y :& RNil
        -- PUSH @list (list :l int) {1; 10}
      , someStack $ StkEl (T.VList [T.VInt 1, T.VInt 10]) "list" [notes|list :list int|] :& StkEl (T.VInt 42) yv y :& RNil
        -- CAST @q (int :q)
      , someStack $ StkEl (T.VInt 1) qv q :& StkEl (T.VInt 42) yv y :& RNil
        -- CAST int
      , someStack $ StkEl (T.VInt 42) yv T.starNotes :& RNil
        -- DIP
      , someStack $ StkEl (T.VInt 1) qv q :& StkEl (T.VInt 42) yv T.starNotes :& RNil
        -- CAST @q (int :q)
      , someStack $ StkEl (T.VInt 10) qv q :& StkEl (T.VInt 42) yv T.starNotes :& RNil
        -- CAST int
      , someStack $ StkEl (T.VInt 42) yv T.starNotes :& RNil
        -- DIP
      , someStack $ StkEl (T.VInt 10) qv q :& StkEl (T.VInt 42) yv T.starNotes :& RNil
        -- MAP
      , someStack $ StkEl (T.VList [T.VInt 1, T.VInt 10]) U.noAnn [notes|list (int :q)|] :& StkEl (T.VInt 42) yv T.starNotes :& RNil
        -- DROP
      , someStack $ StkEl (T.VInt 42) yv T.starNotes :& RNil
        -- NIL operation
      , ignoreStack
        -- PAIR
      , someStack $ StkEl (T.VPair (ops, T.VInt 42)) noAnn (NTPair noAnn noAnn noAnn noAnn yv starNotes starNotes) :& RNil
      ]

test_update_notes :: IO [TestTree]
test_update_notes = sequenceA
  [ importContract (contractsDir </> "update-annots.tz") <&>
    stackAnnotationsTest
      "UPDATE keeps its annotations (morley-debugger#4)"
      (starNotesStkEl (T.VPair (T.VUnit, T.VMap @'T.TInt @'T.TInt Map.empty)) :& RNil)
      expectedStacksUpdate
  ]
  where
    m :: T.Notes ('T.TMap 'T.TInt 'T.TInt)
    m = [notes|map :m (int :k) (int :v)|]

    k :: T.Notes 'T.TInt
    k = [notes|int :k|]

    v :: T.Notes ('T.TOption 'T.TInt)
    v = [notes|option (int :v)|]

    mv, kv, vv :: U.VarAnn
    mv = "m"
    kv = "k"
    vv = "v"

    intMap :: T.Value ('T.TMap 'T.TInt 'T.TInt)
    intMap = T.VMap $ Map.fromList [(T.VInt 0, T.VInt 1), (T.VInt 1, T.VInt 2), (T.VInt 2, T.VInt 0)]

    intMap' :: T.Value ('T.TMap 'T.TInt 'T.TInt)
    intMap' = T.VMap $ Map.fromList [(T.VInt 0, T.VInt 1), (T.VInt 1, T.VInt 2)]

    expectedStacksUpdate :: [Maybe SomeStack]
    expectedStacksUpdate =
      [ -- DROP
        someStack RNil
        -- PUSH @s (map :m int int) {Elt 0 1; Elt 1 2; Elt 2 0}
      , someStack $ StkEl intMap mv m :& RNil
        -- NONE @v (int :v)
      , someStack $ StkEl (T.VOption Nothing) vv v :& StkEl intMap mv m :& RNil
        -- PUSH @k (int :k) 2
      , someStack $ StkEl (T.VInt 2) kv k :& StkEl (T.VOption Nothing) vv v :& StkEl intMap mv m :& RNil
        -- UPDATE
      , someStack $ StkEl intMap' mv m :& RNil
        -- NIL operation
      , ignoreStack
        -- PAIR
      , someStack $ StkEl (T.VPair (ops, intMap')) noAnn (NTPair noAnn noAnn noAnn noAnn "m" starNotes m) :& RNil
      ]

test_create_contract_notes :: IO [TestTree]
test_create_contract_notes = sequenceA
  [ importContract (contractsDir </> "create-contract-annots.tz") <&>
    stackAnnotationsTest
      "CREATE_CONTRACT produces two annotations (morley-debugger#4)"
      (starNotesStkEl (T.VPair (T.VUnit, storage)) :& RNil)
      expectedStacksCreateContract
  ]
  where
    address :: Address
    address = unsafe $ parseAddress "KT1Cb7mVHmedj3Q1vfXvaiRqeNDMqpLbMKjD"

    storage :: T.Value 'T.TAddress
    storage = T.VAddress $ T.EpAddress address T.DefEpName

    op :: T.Value ('T.TOption 'T.TKeyHash)
    op = T.VOption Nothing

    mutez :: T.Value 'T.TMutez
    mutez = T.VMutez 100

    contract :: T.Value 'T.TOperation
    contract = T.VOp $ T.OpCreateContract T.CreateContract
      { T.ccOriginator = genesisAddress
      , T.ccDelegate = Nothing
      , T.ccBalance = 100
      , T.ccStorageVal = T.VUnit
      , T.ccContract = T.defaultContract $
        let loc c = T.WithLoc $ InstrCallStack [] $ srcPos 12 c in
        loc 19 T.CDR
        `T.Seq` loc 24 T.NIL
        `T.Seq` loc 39 T.PAIR :: T.Instr (T.ContractInp 'T.TUnit 'T.TUnit) (T.ContractOut 'T.TUnit)
      , T.ccCounter = 1
      }

    expectedStacksCreateContract :: [Maybe SomeStack]
    expectedStacksCreateContract =
      [ -- DROP
        someStack RNil
      , -- UNIT
        someStack $ starNotesStkEl T.VUnit :& RNil
      , -- AMOUNT
        someStack $ starNotesStkEl mutez :& starNotesStkEl T.VUnit :& RNil
      , -- NONE key_hash
        someStack $ starNotesStkEl op :& starNotesStkEl mutez :& starNotesStkEl T.VUnit :& RNil
      , -- CREATE_CONTRACT @op @addr
        someStack $ StkEl contract "op" T.starNotes :& StkEl storage "addr" T.starNotes :& RNil
      , -- NIL operation
        someStack $ starNotesStkEl ops :& StkEl contract "op" T.starNotes :& StkEl storage "addr" T.starNotes :& RNil
      , -- SWAP
        someStack $ StkEl contract "op" T.starNotes :& starNotesStkEl ops :& StkEl storage "addr" T.starNotes :& RNil
      , -- CONS
        someStack $ starNotesStkEl (T.VList [contract]) :& StkEl storage "addr" T.starNotes :& RNil
      , -- PAIR
        someStack $ StkEl (T.VPair (T.VList [contract], storage)) noAnn (NTPair noAnn noAnn noAnn noAnn "addr" starNotes starNotes) :& RNil
      ]

unit_PAIRN_doesnt_convert_anns_but_UNPAIRN_does :: Assertion
unit_PAIRN_doesnt_convert_anns_but_UNPAIRN_does = do
  contract <- importContract (contractsDir </> "pair_n_unpair_n.tz")
  stackAnnotationsAssertion
    (StkEl contractInput noAnn contractInputNotes :& RNil)
    expectedStacks
    contract
  where
    pairNotes = [notes|pair (int :a %aa) (int :b %bb) (int :c %cc)|]

    pairNotes' = [notes|pair (int :a) (int :b) (int :c)|]

    paramN = "parameter"

    storage = (1, (2, 3)) :: (Integer, (Integer, Integer))
    param = (4, (5, 6)) :: (Integer, (Integer, Integer))
    contractInput = toVal (param, storage)
    contractInputNotes =
      NTPair
        noAnn noAnn noAnn paramN noAnn
        pairNotes -- parameter
        pairNotes -- storage

    expectedStacks :: [Maybe SomeStack]
    expectedStacks =
      [ -- CAR
        someStack $
          StkEl (toVal param) paramN pairNotes :&
          RNil
        -- UNPAIR 3
      , someStack $
          StkEl (toVal @Integer 4) "aa" [notes|int :a|] :&
          StkEl (toVal @Integer 5) "bb" [notes|int :b|] :&
          StkEl (toVal @Integer 6) "cc" [notes|int :c|] :&
          RNil
        -- PAIR @newStorage 3;
      , someStack $
          StkEl (toVal param) "newStorage" pairNotes' :&
          RNil
        -- NIL operation;
      , someStack $
          starNotesStkEl ops :&
          StkEl (toVal param) "newStorage" pairNotes' :&
          RNil
        -- PAIR 2;
      , someStack $
          StkEl
            (toVal ([] :: [Operation], param))
            noAnn
            (NTPair noAnn noAnn noAnn noAnn noAnn starNotes pairNotes') :&
          RNil
      ]

unit_GETN_adds_var_ann :: Assertion
unit_GETN_adds_var_ann = do
  contract <- importContract (contractsDir </> "get_n.tz")
  stackAnnotationsAssertion
    (StkEl contractInput noAnn contractInputNotes :& RNil)
    expectedStacks
    contract
  where
    paramNotes = [notes|pair (int :a %aa) (int :b %bb) (int :c %cc)|]

    storageNotes = [notes|pair (int :a %aa) (int :b %bb)|]

    storage = (5, 6) :: (Integer, Integer)
    param = (1, (2, 3)) :: (Integer, (Integer, Integer))
    contractInput = toVal (param, storage)
    contractInputNotes =
      NTPair
        noAnn noAnn noAnn "parameter" "storage"
        paramNotes
        storageNotes

    expectedStacks :: [Maybe SomeStack]
    expectedStacks =
      [ -- CAR
       ignoreStack
        -- DUP
      , someStack $
          StkEl (toVal param) "parameter" paramNotes :&
          StkEl (toVal param) "parameter" paramNotes :&
          RNil
        -- GET 3;
      , someStack $
          StkEl (toVal @Integer 2) noAnn [notes|int :b|] :&
          StkEl (toVal param) "parameter" paramNotes :&
          RNil
        -- SWAP;
      , someStack $
          StkEl (toVal param) "parameter" paramNotes :&
          StkEl (toVal @Integer 2) noAnn [notes|int :b|] :&
          RNil
        -- GET @aa 1
      , someStack $
          StkEl (toVal @Integer 1) "aa" [notes|int :a|] :&
          StkEl (toVal @Integer 2) noAnn [notes|int :b|] :&
          RNil
        -- PAIR 2
        -- NIL operation;
        -- PAIR 2;
      , ignoreStack, ignoreStack, ignoreStack
      ]

unit_GET_0_deletes_var_ann :: Assertion
unit_GET_0_deletes_var_ann = do
  contract <- importContract (contractsDir </> "get_0.tz")
  stackAnnotationsAssertion
    (starNotesStkEl (toVal ((), 0 :: Integer)) :& RNil)
    expectedStacks
    contract
  where
    expectedStacks :: [Maybe SomeStack]
    expectedStacks =
      [ -- DROP
        ignoreStack
        -- PUSH @var (int :i) 1
      , someStack $
          StkEl (toVal @Integer 1) "var" [notes|int :i|] :&
          RNil
        -- GET 0;
      , someStack $
          StkEl (toVal @Integer 1) noAnn [notes|int :i|] :&
          RNil
        -- NIL operation;
        -- PAIR 2;
      , ignoreStack, ignoreStack
      ]

unit_UPDATEN_field_anns :: Assertion
unit_UPDATEN_field_anns = do
  contract <- importContract (contractsDir </> "update_n_field_anns.tz")
  stackAnnotationsAssertion
    (starNotesStkEl (toVal ((), (0 :: Natural, 0 :: Natural))) :& RNil)
    expectedStacks
    contract
  where
    expectedStacks :: [Maybe SomeStack]
    expectedStacks =
      [ -- DROP
        ignoreStack
        -- PUSH (pair :t0 (int :t1 %f1) (string :t2 %f2) (unit :t3 %f3)) { 0; "a"; Unit };
      , someStack $
          StkEl
            (toVal (0 :: Integer, ("a" :: MText, ())))
            noAnn
            [notes|(pair :t0 (int :t1 %f1) (string :t2 %f2) (unit :t3 %f3))|] :&
          RNil

        -- PUSH (nat :t4) 0; UPDATE 1;
        -- PUSH (nat :t5) 0; UPDATE 3;
        -- PUSH (nat :t6) 0; UPDATE 4;
      , ignoreStack, ignoreStack
      , ignoreStack, ignoreStack
      , ignoreStack
      , someStack $
          StkEl
            (toVal (0 :: Natural, (0 :: Natural, 0 :: Natural)))
            noAnn
            [notes|(pair :t0 (nat :t4 %f1) (nat :t5 %f2) (nat :t6 %f3))|] :&
          RNil

        -- PUSH (pair (nat :t7 %f7) (nat :t8 %f8)) (Pair 0 0);
        -- UPDATE 2;
      , ignoreStack
      , someStack $
          StkEl
            (toVal (0 :: Natural, (0 :: Natural, 0 :: Natural)))
            noAnn
            [notes|pair :t0 (nat :t4 %f1) (nat :t7 %f7) (nat :t8 %f8)|] :&
          RNil

        -- PUSH (nat :t9) 0;
        -- UPDATE 2;
      , ignoreStack
      , someStack $
          StkEl
            (toVal (0 :: Natural, 0 :: Natural))
            noAnn
            [notes|pair :t0 (nat :t4 %f1) (nat :t9)|] :&
          RNil
        -- NIL operation; PAIR;
      , ignoreStack, ignoreStack
      ]

unit_UPDATEN_var_anns :: Assertion
unit_UPDATEN_var_anns = do
  contract <- importContract (contractsDir </> "update_n_var_anns.tz")
  stackAnnotationsAssertion
    (starNotesStkEl (toVal ((), (0 :: Integer, 0 :: Integer))) :& RNil)
    expectedStacks
    contract
  where
    expectedStacks :: [Maybe SomeStack]
    expectedStacks =
      [ -- DROP;
        -- PUSH @v1 (pair int int) (Pair 0 0);
        -- PUSH @v2 int 0;
        ignoreStack, ignoreStack
      , someStack $
          StkEl (toVal (0 :: Integer))               "v2" starNotes :&
          StkEl (toVal (0 :: Integer, 0 :: Integer)) "v1" starNotes :&
          RNil

        -- UPDATE 1
      , someStack $
          StkEl (toVal (0 :: Integer, 0 :: Integer)) "" starNotes :&
          RNil

        -- PUSH int 0;
        -- UPDATE @v3 1;
      , ignoreStack
      , someStack $
          StkEl (toVal (0 :: Integer, 0 :: Integer)) "v3" starNotes :&
          RNil

        -- NIL operation; PAIR;
      , ignoreStack, ignoreStack
      ]

unit_GET_AND_UPDATE_anns :: Assertion
unit_GET_AND_UPDATE_anns = do
  contract <- importContract (contractsDir </> "get_and_update_anns.tz")
  stackAnnotationsAssertion
    (starNotesStkEl (toVal ((), ())) :& RNil)
    expectedStacks
    contract
  where
    expectedStacks :: [Maybe SomeStack]
    expectedStacks =
      [ -- DROP;
        -- EMPTY_MAP :map @varMap (int :k) (nat :v);
        -- PUSH @varVal (option (nat :v)) (Some 1);
        -- PUSH @varKey (int :k) 1;
        ignoreStack, ignoreStack, ignoreStack, ignoreStack

        -- GET_AND_UPDATE
      , someStack $
          StkEl (toVal (Nothing :: Maybe Natural))          "varVal" [notes|option (nat :v)|] :&
          StkEl (toVal (one (1, 1) :: Map Integer Natural)) "varMap" [notes|map :map (int :k) (nat :v)|] :&
          RNil

        -- PUSH @varKey (int :k) 1;
        -- GET_AND_UPDATE @newVarMap;
      , ignoreStack
      , someStack $
          StkEl (toVal (Just 1 :: Maybe Natural))       "varVal"    [notes|option (nat :v)|] :&
          StkEl (toVal (mempty :: Map Integer Natural)) "newVarMap" [notes|map :map (int :k) (nat :v)|] :&
          RNil

        -- DROP 2;
        -- UNIT; NIL operation; PAIR
      , ignoreStack, ignoreStack, ignoreStack, ignoreStack
      ]

test_dupn :: IO TestTree
test_dupn = importContract (contractsDir </> "dup-n.tz") <&>
  stackAnnotationsTest
    "Check that annotations behave as intended with DUP n (#471)"
    (StkEl (T.VPair (T.VUnit, store)) noAnn [notes|pair unit (int :x)|] :& RNil)
    expectedStacks
  where
    store :: T.Value 'T.TInt
    store = T.VInt 42

    x :: T.Notes 'T.TInt
    x = [notes|int :x|]

    kek :: T.Value 'T.TString
    kek = T.VString "kek"

    expectedStacks :: [Maybe SomeStack]
    expectedStacks =
      [ -- CDR
        someStack $ StkEl store "storage" x :& RNil
        -- RENAME @x
      , someStack $ StkEl store "x" x :& RNil
        -- PUSH string "kek"
      , someStack $ starNotesStkEl kek :& StkEl store "x" x :& RNil
        -- DUP 2
        -- n.b.: DUP n doesn't duplicate variable annotations. This is consistent with tezos-client.
      , someStack $ StkEl store U.noAnn x :& starNotesStkEl kek :& StkEl store "x" x :& RNil
        -- SWAP
      , someStack $ starNotesStkEl kek :& StkEl store U.noAnn x :& StkEl store "x" x :& RNil
        -- DROP 2
      , someStack $ StkEl store "x" x :& RNil
        -- DUP @z 1
      , someStack $ StkEl store "z" x :& StkEl store "x" x :& RNil
        -- DROP
      , someStack $ StkEl store "x" x :& RNil
        -- NIL operation
      , ignoreStack
        -- PAIR
      , someStack $ StkEl (VPair (ops, store)) noAnn (NTPair noAnn noAnn noAnn noAnn "x" starNotes x) :& RNil
      ]

test_nested_annots :: IO [TestTree]
test_nested_annots = sequenceA
  [ importContract (contractsDir </> "nested-pair-annots.tz") <&>
    stackAnnotationsTest
      "CAR interacts with annotations (morley-debugger#13)"
      (mkInitStack (VNat 1) starParamNotes (VNat 2) starNotes)
      expectedStacks1
  , importContract (contractsDir </> "nested-pair-annots-2.tz") <&>
    stackAnnotationsTest
      "CAR @a overrides annotations (morley-debugger#13)"
      (mkInitStack (VNat 1) starParamNotes (VNat 2) starNotes)
      expectedStacks2
  ]
  where
    parameterStk = StkEl (VNat 1) "parameter" starNotes

    storageStk = StkEl (VNat 2) "storage" starNotes

    expectedStacks1 :: [Maybe SomeStack]
    expectedStacks1 =
      [ -- UNPAIR
        someStack $ parameterStk :& storageStk :& RNil
        -- UNIT @something
      , someStack $
          StkEl VUnit "something" starNotes :&
          parameterStk :&
          storageStk :&
          RNil
        -- PAIR
      , someStack $
          StkEl (VPair (VUnit, VNat 1)) noAnn (NTPair noAnn noAnn noAnn "something" "parameter" starNotes starNotes) :&
          storageStk :&
          RNil
        -- CAR
      , someStack $ StkEl VUnit "something" starNotes :& storageStk :& RNil
        -- DROP
      , ignoreStack
        -- NIL operation
      , ignoreStack
        -- PAIR
      , someStack $
          StkEl (VPair (ops, VNat 2)) noAnn (NTPair noAnn noAnn noAnn noAnn "storage" starNotes starNotes) :&
          RNil
      ]

    expectedStacks2 :: [Maybe SomeStack]
    expectedStacks2 = expectedStacks1 & ix 3 .~
      -- CAR @a
      ( someStack $ StkEl VUnit "a" starNotes :& storageStk :& RNil
      )

unit_CARk_CDRk_interact_with_annotations :: Assertion
unit_CARk_CDRk_interact_with_annotations = do
  contract <- importContract (contractsDir </> "carn_and_cdrn.tz")
  stackAnnotationsAssertion
    (StkEl (toVal (param, ())) noAnn starNotes :& RNil)
    expectedStacks
    contract
  where
    param = (1, 2, ()) :: (Natural, Natural, ())
    paramNotes = [notes|pair nat nat (unit :last)|]

    expectedStacks :: [Maybe SomeStack]
    expectedStacks =
      [ -- CAR
        someStack $ StkEl (toVal param) "parameter" paramNotes :& RNil
        -- GET 0
      , someStack $ StkEl (toVal param) noAnn paramNotes :& RNil
        -- CDR 0 (macro expanded above)
      , someStack $ StkEl (toVal param) noAnn paramNotes :& RNil
        -- DUP
      , ignoreStack
        -- CAR 0
      , someStack $
          StkEl (toVal @Natural 1) noAnn starNotes :&
          StkEl (toVal param) noAnn paramNotes :&
          RNil
        -- DROP
      , ignoreStack
        -- DUP
      , ignoreStack
        -- CAR 1
      , someStack $
          StkEl (toVal @Natural 2) noAnn starNotes :&
          StkEl (toVal param) noAnn paramNotes :&
          RNil
        -- DROP
      , ignoreStack
        -- GET @kek 4
      , someStack $ StkEl VUnit "kek" [notes|unit :last|] :& RNil
        -- CDR @kek 2 (macro expanded above)
      , someStack $ StkEl VUnit "kek" [notes|unit :last|] :& RNil
        -- NIL operation
      , ignoreStack
        -- PAIR
      , someStack $
          StkEl
            (VPair (ops, VUnit))
            noAnn
            (NTPair noAnn noAnn noAnn noAnn "kek" starNotes (NTUnit "last")) :&
          RNil
      ]

unit_CAR_special_annotations :: Assertion
unit_CAR_special_annotations = do
  contract <- importContract (contractsDir </> "car_special_annots.tz")
  stackAnnotationsAssertion
    (starNotesStkEl (toVal ((), ())) :& RNil)
    expectedStacks
    contract
  where
    expectedStacks :: [Maybe SomeStack]
    expectedStacks =

      replicate 28 ignoreStack
        -- When the pair has no annotations
        & ix 2 .~ (someStack $ StkEl (toVal ()) "" starNotes :& RNil)
        & ix 5 .~ (someStack $ StkEl (toVal ()) "" starNotes :& RNil)

        -- When the pair has a var annotation
        & ix 8 .~ (someStack $ StkEl (toVal ()) "" starNotes :& RNil)
        & ix 11 .~ (someStack $ StkEl (toVal ()) "pair" starNotes :& RNil)
        -- TODO [#534]: should be `pair.car` -----^^^^

        -- When the pair has field annotations
        & ix 14 .~ (someStack $ StkEl (toVal ()) "aa" starNotes :& RNil)
        & ix 17 .~ (someStack $ StkEl (toVal ()) "aa" starNotes :& RNil)

        -- When the pair has var + field annotations
        & ix 20 .~ (someStack $ StkEl (toVal ()) "aa" starNotes :& RNil)
        & ix 23 .~ (someStack $ StkEl (toVal ()) "pair.aa" starNotes :& RNil)

unit_CDR_special_annotations :: Assertion
unit_CDR_special_annotations = do
  contract <- importContract (contractsDir </> "cdr_special_annots.tz")
  stackAnnotationsAssertion
    (starNotesStkEl (toVal ((), ())) :& RNil)
    expectedStacks
    contract
  where
    expectedStacks :: [Maybe SomeStack]
    expectedStacks =

      replicate 28 ignoreStack
        -- When the pair has no annotations
        & ix 2 .~ (someStack $ StkEl (toVal ()) "" starNotes :& RNil)
        & ix 5 .~ (someStack $ StkEl (toVal ()) "" starNotes :& RNil)

        -- When the pair has a var annotation
        & ix 8 .~ (someStack $ StkEl (toVal ()) "" starNotes :& RNil)
        & ix 11 .~ (someStack $ StkEl (toVal ()) "pair" starNotes :& RNil)
        -- TODO [#534]: should be `pair.cdr` -----^^^^

        -- When the pair has field annotations
        & ix 14 .~ (someStack $ StkEl (toVal ()) "bb" starNotes :& RNil)
        & ix 17 .~ (someStack $ StkEl (toVal ()) "bb" starNotes :& RNil)

        -- When the pair has var + field annotations
        & ix 20 .~ (someStack $ StkEl (toVal ()) "bb" starNotes :& RNil)
        & ix 23 .~ (someStack $ StkEl (toVal ()) "pair.bb" starNotes :& RNil)

unit_UNPAIR_special_annotations :: Assertion
unit_UNPAIR_special_annotations = do
  contract <- importContract (contractsDir </> "unpair_special_annots.tz")
  stackAnnotationsAssertion
    (starNotesStkEl (toVal ((), ())) :& RNil)
    expectedStacks
    contract
  where
    expectedStacks :: [Maybe SomeStack]
    expectedStacks =

      replicate 16 ignoreStack
        -- When the pair has no annotations
        & ix 2 .~ (someStack $ StkEl (toVal ()) "" starNotes :& StkEl (toVal ()) "" starNotes :& RNil)

        -- When the pair has a var annotation
        & ix 5 .~ (someStack $ StkEl (toVal ()) "" starNotes :& StkEl (toVal ()) "pair" starNotes :& RNil)
        -- TODO [#534]: should be `pair.cdr` -------------------------------------^^^^

        -- When the pair has field annotations
        & ix 8 .~ (someStack $ StkEl (toVal ()) "aa" starNotes :& StkEl (toVal ()) "bb" starNotes :& RNil)

        -- When the pair has var + field annotations
        & ix 11 .~ (someStack $ StkEl (toVal ()) "aa" starNotes :& StkEl (toVal ()) "pair.bb" starNotes :& RNil)

test_special_annotations :: IO TestTree
test_special_annotations = importContract (contractsDir </> "right_special_anns.tz") <&>
    stackAnnotationsTest
      "RIGHT uses special field annotations (#439)"
      (starNotesStkEl (VPair (VUnit, VUnit)) :& RNil)
      expectedStacksRIGHTSpecial
  where
    expectedStacksRIGHTSpecial :: [Maybe SomeStack]
    expectedStacksRIGHTSpecial =
      [ -- CAR
        someStack $ StkEl (VUnit) "p.y" starNotes :& RNil
        -- RIGHT % %@ never
      , someStack $ StkEl (VOr @'T.TNever $ Right $ VUnit) "p" [notes|or never (unit %y)|] :& RNil
        -- DROP
        -- PUSH unit Unit
        -- NUL operation
        -- PAIR
      , ignoreStack, ignoreStack, ignoreStack, ignoreStack
      ]