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

{-# OPTIONS_GHC -Wno-orphans #-}

module Morley.Michelson.Typed.Convert
  ( convertParamNotes
  , convertView
  , convertSomeView
  , convertContractCode
  , convertContract
  , instrToOps
  , instrToOpsOptimized
  , untypeDemoteT
  , untypeValue
  , untypeValueHashable
  , untypeValueOptimized

  -- Helper for generating documentation
  , sampleTypedValue

  -- * Misc
  , flattenEntrypoints
  , U.HandleImplicitDefaultEp(..)
  , eqInstrExt
  ) where

import Data.ByteArray qualified as ByteArray
import Data.Constraint (Dict(..), (\\))
import Data.List.NonEmpty ((<|))
import Data.Map qualified as Map
import Data.Singletons (Sing, demote, withSingI)
import Fmt (Buildable(..), fmt, listF, pretty)
import Text.PrettyPrint.Leijen.Text (Doc)
import Unsafe qualified (fromIntegral)

import Morley.Michelson.Printer.Util
import Morley.Michelson.Text
import Morley.Michelson.Typed.Aliases
import Morley.Michelson.Typed.Annotation (annotateInstr, mkUType)
import Morley.Michelson.Typed.Contract
import Morley.Michelson.Typed.Entrypoints
import Morley.Michelson.Typed.Extract (toUType)
import Morley.Michelson.Typed.Instr as Instr
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.Sing (SingT(..))
import Morley.Michelson.Typed.T (T(..))
import Morley.Michelson.Typed.Value
import Morley.Michelson.Typed.View
import Morley.Michelson.Untyped qualified as U
import Morley.Michelson.Untyped.Annotation (Annotation(unAnnotation))
import Morley.Tezos.Address
import Morley.Tezos.Core
  (ChainId(unChainId), mformatChainId, parseChainId, timestampFromSeconds, timestampToSeconds, tz,
  unMutez)
import Morley.Tezos.Crypto
import Morley.Tezos.Crypto.BLS12381 qualified as BLS
import Morley.Tezos.Crypto.Ed25519 qualified as Ed25519
import Morley.Tezos.Crypto.P256 qualified as P256
import Morley.Tezos.Crypto.Secp256k1 qualified as Secp256k1
import Morley.Tezos.Crypto.Timelock (chestBytes, chestKeyBytes)
import Morley.Util.PeanoNatural (fromPeanoNatural, singPeanoVal)
import Morley.Util.Sing (eqParamSing)

-- | Convert typed parameter annotations to an untyped 'U.ParameterType'.
convertParamNotes :: ParamNotes cp -> U.ParameterType
convertParamNotes (ParamNotes notes rootAnn) =
  U.ParameterType (mkUType notes) rootAnn

-- | Convert typed t'ContractCode' to an untyped t'U.Contract'.
convertContractCode
  :: forall param store . (SingI param, SingI store)
  => ContractCode param store -> U.Contract
convertContractCode contract =
  U.Contract
    { contractParameter = U.ParameterType (untypeDemoteT @param) U.noAnn
    , contractStorage = untypeDemoteT @store
    , contractCode = instrToOps $ unContractCode contract
    , entriesOrder = U.canonicalEntriesOrder
    , contractViews = []
    }

convertView :: forall arg store ret. View arg store ret -> U.View
convertView View{..} =
  U.View
    { viewName = vName
    , viewArgument = untypeDemoteT @arg
    , viewReturn = untypeDemoteT @ret
    , viewCode = instrToOps vCode
    }

convertSomeView :: SomeView st -> U.View
convertSomeView (SomeView v) = convertView v

-- | Convert typed t'Contract' to an untyped t'U.Contract'.
convertContract :: Contract param store -> U.Contract
convertContract fc@Contract{} =
  let c = convertContractCode (cCode fc)
  in c { U.contractParameter = convertParamNotes (cParamNotes fc)
       , U.contractStorage = mkUType (cStoreNotes fc)
       , U.entriesOrder = cEntriesOrder fc
       , U.contractViews = convertSomeView <$> toList (cViews fc)
       }

-- Note: if you change this type, check 'untypeValueImpl' wildcard patterns.
data UntypingOptions
  = Readable
  -- ^ Convert value to human-readable representation
  | Optimized
  -- ^ Convert value to optimized representation
  | Hashable
  -- ^ Like 'Optimized', but without list notation for pairs.
  -- Created to match @octez-client hash data@ behavior for typed values.
  -- See https://gitlab.com/morley-framework/morley/-/issues/611
  deriving stock (Eq, Show)

-- | Convert a typed value to an untyped human-readable representation
untypeValue :: HasNoOp t => Value' Instr t -> U.Value
untypeValue = untypeValueImpl' Readable

-- | Like 'untypeValueOptimized', but without list notation for pairs.
--
-- Created to match @octez-client hash data@ behaviour for typed values.
untypeValueHashable :: HasNoOp t => Value' Instr t -> U.Value
untypeValueHashable = untypeValueImpl' Hashable

-- | Convert a typed value to an untyped optimized representation
untypeValueOptimized :: HasNoOp t => Value' Instr t -> U.Value
untypeValueOptimized = untypeValueImpl' Optimized

untypeValueImpl'
  :: HasNoOp t
  => UntypingOptions
  -> Value' Instr t
  -> U.Value
untypeValueImpl' opts val = untypeValueImpl opts (sing \\ valueTypeSanity val) val

-- | Convert a typed t'Morley.Michelson.Typed.Aliases.Value' to an untyped 'Value'.
--
-- For full isomorphism type of the given t'Morley.Michelson.Typed.Aliases.Value' should not contain
-- 'TOperation' - a compile error will be raised otherwise.
-- You can analyse its presence with 'checkOpPresence' function.
untypeValueImpl
  :: HasNoOp t
  => UntypingOptions
  -> Sing t
  -> Value' Instr t
  -> U.Value
untypeValueImpl opts sng val = case (val, sng) of
  (VInt i, _) -> U.ValueInt i
  (VNat i, _) -> U.ValueInt $ toInteger i
  (VString s, _) -> U.ValueString s
  (VBytes b, _) -> U.ValueBytes $ U.InternalByteString b
  (VMutez m, _) -> U.ValueInt $ toInteger $ unMutez m
  (VBool True, _) -> U.ValueTrue
  (VBool False, _) -> U.ValueFalse
  (VKeyHash h, _) ->
    case opts of
      Readable  -> U.ValueString $ mformatHash h
      _         -> U.ValueBytes $ U.InternalByteString $ hashToBytes h
  (VBls12381Fr v, _) ->
    case opts of
      Readable  -> U.ValueInt $ toInteger v
      _         -> U.ValueBytes . U.InternalByteString $ BLS.toMichelsonBytes v
  (VBls12381G1 v, _) ->
    U.ValueBytes . U.InternalByteString $ BLS.toMichelsonBytes v
  (VBls12381G2 v, _) ->
    U.ValueBytes . U.InternalByteString $ BLS.toMichelsonBytes v
  (VTimestamp t, _) ->
    case opts of
      Readable   -> U.ValueString . unsafe . mkMText $ pretty t
      _          -> U.ValueInt $ timestampToSeconds t
  (VAddress a, _) ->
    case opts of
      Readable  -> U.ValueString $ mformatEpAddress a
      _         -> U.ValueBytes . U.InternalByteString  $ encodeEpAddress a
  (VTxRollupL2Address (TxRollupL2Address a), _) ->
    case opts of
      Readable  -> U.ValueString $ mformatHash a
      _         -> U.ValueBytes . U.InternalByteString  $ hashToBytes a
  (VKey b, _) ->
    case opts of
      Readable  -> U.ValueString $ mformatPublicKey b
      _         -> U.ValueBytes . U.InternalByteString $ keyToBytes b
  (VUnit, _) ->
    U.ValueUnit
  (VSignature b, _) ->
    case opts of
      Readable  -> U.ValueString $ mformatSignature b
      _         -> U.ValueBytes . U.InternalByteString $ signatureToBytes b
  (VChainId b, _) ->
    case opts of
      Readable  -> U.ValueString $ mformatChainId b
      _         ->
        U.ValueBytes . U.InternalByteString $ ByteArray.convert (unChainId b)
  (VOption (Just x), STOption op) ->
    U.ValueSome (untypeValueImpl opts op x)
  (VOption Nothing, STOption _) ->
    U.ValueNone
  (VList l, STList lt) ->
    vList U.ValueSeq $ map (untypeValueImpl opts lt) l
  (VSet s, STSet st) ->
    case checkOpPresence st of
      OpAbsent -> vList U.ValueSeq $ map (untypeValueImpl opts st) $ toList s
  (VContract addr sepc, _) ->
    case opts of
      Readable  ->
        U.ValueString . mformatEpAddress $ EpAddress' addr (sepcName sepc)
      _         -> U.ValueBytes . U.InternalByteString . encodeEpAddress $
        EpAddress' addr (sepcName sepc)
  (VChest c, _) -> U.ValueBytes . U.InternalByteString $ chestBytes c
  (VChestKey c, _) -> U.ValueBytes . U.InternalByteString $ chestKeyBytes c
  (VTicket s v a, STTicket vt) ->
    case valueTypeSanity v of
      Dict ->
        let us = untypeValueImpl opts STAddress $ VAddress (EpAddress' s DefEpName)
            uv = untypeValueImpl opts vt v
            ua = untypeValueImpl opts STNat $ VNat a
        in case opts of
          Optimized -> U.ValueSeq $ us :| [uv, ua]
          _         -> U.ValuePair us (U.ValuePair uv ua)
  p@(VPair (l, r), STPair lt rt) ->
    case checkOpPresence lt of
      OpAbsent -> case opts of
        Optimized -> U.ValueSeq $ pairToSeq p
        _         -> U.ValuePair (untypeValueImpl opts lt l) (untypeValueImpl opts rt r)

  (VOr (Left x), STOr lt _) ->
    case checkOpPresence lt of
      OpAbsent -> U.ValueLeft (untypeValueImpl opts lt x)

  (VOr (Right x), STOr lt rt) ->
    case checkOpPresence lt of
      OpAbsent -> U.ValueRight (untypeValueImpl opts rt x)

  (VLam (LambdaCode (rfAnyInstr -> ops)), _) ->
    vList U.ValueLambda $ instrToOpsImpl opts ops

  (VLam (LambdaCodeRec (rfAnyInstr -> ops)), _) ->
    vList U.ValueLamRec $ instrToOpsImpl opts ops

  (VMap m, STMap kt vt) ->
    case (checkOpPresence kt, checkOpPresence vt) of
      (OpAbsent, OpAbsent) ->
        vList U.ValueMap $ Map.toList m <&> \(k, v) ->
        U.Elt (untypeValueImpl opts kt k) (untypeValueImpl opts vt v)

  (VBigMap _ m, STBigMap kt vt) ->
    case (checkOpPresence kt, checkOpPresence vt) of
      (OpAbsent, OpAbsent) ->
        vList U.ValueMap $ Map.toList m <&> \(k, v) ->
        U.Elt (untypeValueImpl opts kt k) (untypeValueImpl opts vt v)
  where
    vList ctor = maybe U.ValueNil ctor . nonEmpty

    pairToSeq :: HasNoOp ty
              => (Value ty, Sing ty)
              -> NonEmpty U.Value
    pairToSeq = \case
      (VPair (a, b), STPair l r) -> case checkOpPresence l of
        OpAbsent -> untypeValueImpl opts l a <| pairToSeq (b, r)
      (v, vt) -> untypeValueImpl opts vt v :| []

    hashToBytes :: Hash kind -> ByteString
    hashToBytes Hash{..} = (<> hBytes) $
      case hTag of
        HashKey KeyTypeEd25519 -> "\x00"
        HashKey KeyTypeSecp256k1 -> "\x01"
        HashKey KeyTypeP256 -> "\x02"
        HashContract -> ""
        HashBLS -> ""
        HashTXR -> ""

    keyToBytes :: PublicKey -> ByteString
    keyToBytes = \case
      PublicKeyEd25519 pk -> "\x00" <> Ed25519.publicKeyToBytes pk
      PublicKeySecp256k1 pk -> "\x01" <> Secp256k1.publicKeyToBytes pk
      PublicKeyP256 pk -> "\x02" <> P256.publicKeyToBytes pk

    encodeEpAddress :: EpAddress -> ByteString
    encodeEpAddress (EpAddress addr epName) =
      encodeAddress addr <> encodeEpName epName

    encodeAddress :: KindedAddress kind -> ByteString
    encodeAddress = \case
      ImplicitAddress keyHash ->
        "\x00" <> hashToBytes keyHash
      ContractAddress hash ->
        "\x01" <> hashToBytes hash <> "\x00"
      TxRollupAddress hash ->
        "\x02" <> hashToBytes hash <> "\x00"

    encodeEpName :: EpName -> ByteString
    encodeEpName = encodeUtf8 . unAnnotation . epNameToRefAnn . canonicalize
      where
        canonicalize :: EpName -> EpName
        canonicalize (UnsafeEpName "default") = DefEpName
        canonicalize epName                   = epName

-- | Convert a Haskell type-level type tag into an
-- untyped value representation.
--
-- This function is intended to be used with @TypeApplications@.
untypeDemoteT :: forall (t :: T). SingI t => U.Ty
untypeDemoteT = toUType $ demote @t

-- | Convert Haskell-typed 'Instr' to a list of optimized untyped operations
instrToOpsOptimized :: HasCallStack => Instr inp out -> [U.ExpandedOp]
instrToOpsOptimized = instrToOpsImpl Optimized

-- | Convert Haskell-typed 'Instr' to a list of human-readable untyped operations
instrToOps :: HasCallStack => Instr inp out -> [U.ExpandedOp]
instrToOps = instrToOpsImpl Readable

instrToOpsImpl :: HasCallStack
               => UntypingOptions
               -> Instr inp out
               -> [U.ExpandedOp]
instrToOpsImpl opts = \case
  Nop -> []
  Seq i1 i2 -> instrToOpsImpl opts i1 <> instrToOpsImpl opts i2
  Nested sq -> one $ U.SeqEx $ instrToOps sq
  DocGroup _ sq -> instrToOpsImpl opts sq
  Ext (ext :: ExtInstr inp) -> (U.PrimEx . U.EXT) <$> extInstrToOps ext
  FrameInstr _ i -> instrToOpsImpl opts i
  -- TODO [#283]: After representation of locations is polished,
  -- this place should be updated to pass it from typed to untyped ASTs.
  WithLoc _ i -> instrToOpsImpl opts i
  Meta _ i -> instrToOpsImpl opts i
  i -> pure $ U.PrimEx $ case i of
    DROP -> U.DROP
    DROPN s -> U.DROPN (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural s)
    AnnDUP ann -> annotateInstr ann U.DUP
    AnnDUPN ann s -> annotateInstr ann U.DUPN (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural s)
    SWAP -> U.SWAP
    DIG s -> U.DIG (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural s)
    DUG s -> U.DUG (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural s)
    AnnPUSH ann val | _ :: Instr inp1 (t ': s) <- i ->
      let value = untypeValueImpl opts (sing @t) val
      in annotateInstr ann U.PUSH value
    AnnNONE ann | _ :: Instr inp1 ('TOption a ': inp1) <- i ->
      annotateInstr ann U.NONE
    AnnSOME ann -> annotateInstr ann U.SOME
    AnnUNIT ann -> annotateInstr ann U.UNIT
    IF_NONE i1 i2 -> U.IF_NONE (instrToOpsImpl opts i1) (instrToOpsImpl opts i2)
    AnnPAIR ann -> annotateInstr ann U.PAIR
    AnnUNPAIR ann -> annotateInstr ann U.UNPAIR
    AnnPAIRN ann n -> annotateInstr ann U.PAIRN (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural n)
    UNPAIRN n -> U.UNPAIRN (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural n)
    AnnCAR ann -> annotateInstr ann U.CAR
    AnnCDR ann -> annotateInstr ann U.CDR
    AnnLEFT ann | _ :: Instr (a ': s) ('TOr a b ': s) <- i ->
      annotateInstr ann U.LEFT
    AnnRIGHT ann | _ :: Instr (b ': s) ('TOr a b ': s) <- i ->
      annotateInstr ann U.RIGHT
    IF_LEFT i1 i2 -> U.IF_LEFT (instrToOpsImpl opts i1) (instrToOpsImpl opts i2)
    AnnNIL ann | _ :: Instr s ('TList p ': s) <- i ->
      annotateInstr ann U.NIL
    AnnCONS ann -> annotateInstr ann U.CONS
    IF_CONS i1 i2 -> U.IF_CONS (instrToOpsImpl opts i1) (instrToOpsImpl opts i2)
    AnnSIZE ann -> annotateInstr ann U.SIZE
    AnnEMPTY_SET ann | _ :: Instr s ('TSet e ': s) <- i ->
      annotateInstr ann U.EMPTY_SET
    AnnEMPTY_MAP ann | _ :: Instr s ('TMap a b ': s) <- i ->
      annotateInstr ann U.EMPTY_MAP
    AnnEMPTY_BIG_MAP ann | _ :: Instr s ('TBigMap a b ': s) <- i ->
      annotateInstr ann U.EMPTY_BIG_MAP
    AnnMAP ann op -> annotateInstr ann U.MAP $ instrToOpsImpl opts op
    ITER op -> U.ITER $ instrToOpsImpl opts op
    AnnMEM ann -> annotateInstr ann U.MEM
    AnnGET ann -> annotateInstr ann U.GET
    AnnGETN ann n -> annotateInstr ann U.GETN (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural n)
    AnnUPDATE ann -> annotateInstr ann U.UPDATE
    AnnUPDATEN ann n -> annotateInstr ann U.UPDATEN (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural n)
    AnnGET_AND_UPDATE ann -> annotateInstr ann U.GET_AND_UPDATE
    IF op1 op2 -> U.IF (instrToOpsImpl opts op1) (instrToOpsImpl opts op2)
    LOOP op -> U.LOOP (instrToOpsImpl opts op)
    LOOP_LEFT op -> U.LOOP_LEFT (instrToOpsImpl opts op)
    AnnLAMBDA ann l -> annotateInstr ann U.LAMBDA (instrToOpsImpl opts $ rfAnyInstr l)
    AnnLAMBDA_REC ann l -> annotateInstr ann U.LAMBDA_REC (instrToOpsImpl opts $ rfAnyInstr l)
    AnnEXEC ann -> annotateInstr ann U.EXEC
    AnnAPPLY ann -> annotateInstr ann U.APPLY
    DIP op -> U.DIP (instrToOpsImpl opts op)
    DIPN s op ->
      U.DIPN (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural s) (instrToOpsImpl opts op)
    FAILWITH -> U.FAILWITH
    AnnCAST ann | _ :: Instr (a ': s) (a ': s) <- i ->
      annotateInstr ann U.CAST
    AnnRENAME ann -> annotateInstr ann U.RENAME
    AnnPACK ann -> annotateInstr ann U.PACK
    AnnUNPACK ann
      | _ :: Instr ('TBytes ': s) ('TOption a ': s) <- i ->
          annotateInstr ann U.UNPACK
    AnnCONCAT ann -> annotateInstr ann U.CONCAT
    AnnCONCAT' ann -> annotateInstr ann U.CONCAT
    AnnSLICE ann -> annotateInstr ann U.SLICE
    AnnISNAT ann -> annotateInstr ann U.ISNAT
    AnnADD ann -> annotateInstr ann U.ADD
    AnnSUB ann -> annotateInstr ann U.SUB
    AnnSUB_MUTEZ ann -> annotateInstr ann U.SUB_MUTEZ
    AnnMUL ann -> annotateInstr ann U.MUL
    AnnEDIV ann -> annotateInstr ann U.EDIV
    AnnABS ann -> annotateInstr ann U.ABS
    AnnNEG ann -> annotateInstr ann U.NEG
    AnnLSL ann -> annotateInstr ann U.LSL
    AnnLSR ann -> annotateInstr ann U.LSR
    AnnOR ann -> annotateInstr ann U.OR
    AnnAND ann -> annotateInstr ann U.AND
    AnnXOR ann -> annotateInstr ann U.XOR
    AnnNOT ann -> annotateInstr ann U.NOT
    AnnCOMPARE ann -> annotateInstr ann U.COMPARE
    AnnEQ ann -> annotateInstr ann U.EQ
    AnnNEQ ann -> annotateInstr ann U.NEQ
    AnnLT ann -> annotateInstr ann U.LT
    AnnGT ann -> annotateInstr ann U.GT
    AnnLE ann -> annotateInstr ann U.LE
    AnnGE ann -> annotateInstr ann U.GE
    AnnINT ann -> annotateInstr ann U.INT
    AnnVIEW ann viewName -> annotateInstr ann (flip U.VIEW viewName)
    AnnSELF ann sepc ->
      annotateInstr ann U.SELF (epNameToRefAnn $ sepcName sepc)
    AnnCONTRACT ann epName
      | _ :: Instr ('TAddress ': s) ('TOption ('TContract p) ': s) <- i ->
          let fa = epNameToRefAnn epName
          in annotateInstr ann (flip U.CONTRACT fa)
    AnnTRANSFER_TOKENS ann -> annotateInstr ann U.TRANSFER_TOKENS
    AnnSET_DELEGATE ann -> annotateInstr ann U.SET_DELEGATE
    AnnCREATE_CONTRACT ann contract
      | _ :: Instr
          (  'TOption ('TKeyHash)
          ': 'TMutez
          ': g
          ': s)
          ('TOperation ': 'TAddress ': s) <- i ->
        annotateInstr ann U.CREATE_CONTRACT (convertContract contract)
    AnnIMPLICIT_ACCOUNT ann -> annotateInstr ann U.IMPLICIT_ACCOUNT
    AnnNOW ann -> annotateInstr ann U.NOW
    AnnAMOUNT ann -> annotateInstr ann U.AMOUNT
    AnnBALANCE ann -> annotateInstr ann U.BALANCE
    AnnVOTING_POWER ann -> annotateInstr ann U.VOTING_POWER
    AnnTOTAL_VOTING_POWER ann -> annotateInstr ann U.TOTAL_VOTING_POWER
    AnnCHECK_SIGNATURE ann -> annotateInstr ann U.CHECK_SIGNATURE
    AnnSHA256 ann -> annotateInstr ann U.SHA256
    AnnSHA512 ann -> annotateInstr ann U.SHA512
    AnnBLAKE2B ann -> annotateInstr ann U.BLAKE2B
    AnnSHA3 ann -> annotateInstr ann U.SHA3
    AnnKECCAK ann -> annotateInstr ann U.KECCAK
    AnnHASH_KEY ann -> annotateInstr ann U.HASH_KEY
    AnnPAIRING_CHECK ann -> annotateInstr ann U.PAIRING_CHECK
    AnnSOURCE ann -> annotateInstr ann U.SOURCE
    AnnSENDER ann -> annotateInstr ann U.SENDER
    AnnADDRESS ann -> annotateInstr ann U.ADDRESS
    AnnCHAIN_ID ann -> annotateInstr ann U.CHAIN_ID
    AnnLEVEL ann -> annotateInstr ann U.LEVEL
    AnnSELF_ADDRESS ann -> annotateInstr ann U.SELF_ADDRESS
    NEVER -> U.NEVER
    AnnTICKET ann -> annotateInstr ann U.TICKET
    AnnTICKET_DEPRECATED ann -> annotateInstr ann U.TICKET_DEPRECATED
    AnnREAD_TICKET ann -> annotateInstr ann U.READ_TICKET
    AnnSPLIT_TICKET ann -> annotateInstr ann U.SPLIT_TICKET
    AnnJOIN_TICKETS ann -> annotateInstr ann U.JOIN_TICKETS
    AnnOPEN_CHEST ann -> annotateInstr ann U.OPEN_CHEST
    AnnSAPLING_EMPTY_STATE ann s ->
      annotateInstr ann U.SAPLING_EMPTY_STATE (singPeanoVal s)
    AnnSAPLING_VERIFY_UPDATE ann -> annotateInstr ann U.SAPLING_VERIFY_UPDATE
    AnnMIN_BLOCK_TIME ann -> U.MIN_BLOCK_TIME ann
    AnnEMIT va tag ty -> annotateInstr va U.EMIT tag $ mkUType <$> ty

untypeStackRef :: StackRef s -> U.StackRef
untypeStackRef (StackRef n) = U.StackRef (fromPeanoNatural n)

untypePrintComment :: PrintComment s -> U.PrintComment
untypePrintComment (PrintComment pc) = U.PrintComment $ map (second untypeStackRef) pc

extInstrToOps :: ExtInstr s -> [U.ExtInstrAbstract U.ExpandedOp]
extInstrToOps = \case
  PRINT pc -> one $ U.UPRINT (untypePrintComment pc)
  TEST_ASSERT (TestAssert nm pc i) ->
    one $ U.UTEST_ASSERT $
    U.TestAssert nm (untypePrintComment pc) (instrToOps i)
  DOC_ITEM{} -> []
  COMMENT_ITEM tp ->
    case tp of
      FunctionStarts name -> one $ U.UCOMMENT $ name <> " [user func starts]"
      FunctionEnds name -> one $ U.UCOMMENT $ name <> " [user func ends]"
      StatementStarts name -> one $ U.UCOMMENT $ name <> " [user stmt starts]"
      StatementEnds name -> one $ U.UCOMMENT $ name <> " [user stmt ends]"
      JustComment com -> one $ U.UCOMMENT com
      StackTypeComment (Just stack) -> one $ U.UCOMMENT $ pretty (listF stack)
      StackTypeComment Nothing -> one $ U.UCOMMENT $ fmt "any stack type"
  STACKTYPE s -> one $ U.STACKTYPE s

-- | Extended equality of 'Instr' - this behaves like '(==)'
-- but does not require the compared instructions to be of strictly
-- the same type.
eqInstrExt :: Instr i1 o1 -> Instr i2 o2 -> Bool
eqInstrExt i1 i2 = instrToOps i1 == instrToOps i2

-- It's an orphan instance, but it's better than checking all cases manually.
-- We can also move this convertion to the place where `Instr` is defined,
-- but then there will be a very large module (as we'll have to move a lot of
-- stuff as well).
instance Eq (Instr inp out) where
  (==) = eqInstrExt

instance SingI s => Eq (TestAssert s) where
  TestAssert   name1 pattern1 instr1
    ==
    TestAssert name2 pattern2 instr2
    = and
    [ name1 == name2
    , pattern1 `eqParamSing` pattern2
    , instr1 `eqInstrExt` instr2
    ]

instance HasNoOp t => RenderDoc (Value' Instr t) where
  renderDoc pn = renderDoc pn . untypeValue

instance Buildable (Value' Instr t) where
  build val = printDocB True $ let tv = withValueTypeSanity val sing
    in renderDocSing doesntNeedParens (checkOpPresence tv) (val, tv)

instance Buildable (Instr inp out) where
  build = buildRenderDocExtended

instance RenderDoc (Instr inp out) where
  renderDoc context = renderDocList context . instrToOps

-- | Generate a value used for generating examples in documentation.
--
-- Since not for all types it is possible to produce a sensible example,
-- the result is optional. E.g. for operations, @never@, not proper
-- types like @contract operation@ we return 'Nothing'.
sampleTypedValue :: forall t. Sing t -> Maybe (Value t)
sampleTypedValue = \case
    STInt              -> Just $ VInt -1
    STNat              -> Just $ VNat 0
    STString           -> Just $ VString [mt|hello|]
    STMutez            -> Just $ VMutez [tz|100u|]
    STBool             -> Just $ VBool True
    STKey              -> Just $ VKey samplePublicKey
    STKeyHash          -> Just $ VKeyHash $ hashKey samplePublicKey
    STBls12381Fr       -> Just $ VBls12381Fr 1
    STBls12381G1       -> Just $ VBls12381G1 BLS.g1One
    STBls12381G2       -> Just $ VBls12381G2 BLS.g2One
    STTimestamp        -> Just $ VTimestamp $ timestampFromSeconds 1564142952
    STBytes            -> Just $ VBytes "\10"
    STAddress          -> Just $ VAddress $ sampleAddress
    STUnit             -> Just $ VUnit
    STSignature        -> Just $ VSignature $ sampleSignature
    STChainId          -> Just $ VChainId sampleChainId
    STOperation        -> Nothing
    -- It's not hard to generate a chest with a matching key, but
    -- representing those in source is extremely unwieldy due to large
    -- primes involved.
    STChest            -> Nothing
    STChestKey         -> Nothing
    STTxRollupL2Address -> Just $ VTxRollupL2Address $ TxRollupL2Address $
      unsafe $ parseHash "tz4LVHYD4P4T5NHCuwJbxQvwVURF62seE3Qa"
    STNever            -> Nothing
    STSaplingState _   -> Nothing
    STSaplingTransaction _ -> Nothing
    STOption t ->
      withSingI t $ VOption . Just <$> sampleTypedValue t
    STList t ->
      withSingI t $ VList . one <$> sampleTypedValue t
    STSet t -> withSingI t $ do
      Dict <- comparabilityPresence t
      VSet . one <$> sampleTypedValue t
    STContract t -> withSingI t $ do
      Dict <- rightToMaybe $ getWTP @t
      Dict <- opAbsense t
      Dict <- nestedBigMapsAbsense t
      pure . VContract (eaAddress sampleAddress) $ SomeEpc unsafeEpcCallRoot
    STTicket t -> withSingI t $ do
      cmpProof <- comparabilityPresence t
      dat <- sampleTypedValue t
      VNat amount <- sampleTypedValue STNat
      case cmpProof of
        Dict -> return $ VTicket (MkAddress sampleCTAddress) dat amount
    STPair t1 t2 -> withSingI t1 $ withSingI t2 $ do
      val1 <- sampleTypedValue t1
      val2 <- sampleTypedValue t2
      pure $ VPair (val1, val2)
    STOr tl tr -> withSingI tl $ withSingI tr $ asum
      [ VOr . Left <$> sampleTypedValue tl
      , VOr . Right <$> sampleTypedValue tr
      ]
    STMap t1 t2 -> withSingI t1 $ withSingI t2 $ do
      val1 <- sampleTypedValue t1
      val2 <- sampleTypedValue t2
      case checkComparability t1 of
        CanBeCompared -> pure $ VMap $ Map.fromList [(val1, val2)]
        CannotBeCompared -> Nothing
    STBigMap t1 t2 -> withSingI t1 $ withSingI t2 $ do
      val1 <- sampleTypedValue t1
      val2 <- sampleTypedValue t2
      case (checkComparability t1, bigMapAbsense t2) of
        (CanBeCompared, Just Dict) -> pure $ VBigMap Nothing $ Map.fromList [(val1, val2)]
        _                          -> Nothing
    STLambda v (t2 :: Sing t2) -> withSingI v $ withSingI t2 $
      case checkScope @(ConstantScope t2) of
        Right Dict -> do
          val <- sampleTypedValue t2
          pure $ mkVLam $ RfNormal (DROP `Seq` PUSH val)
        _ -> pure $ mkVLam $ RfAlwaysFails (PUSH (VString [mt|lambda sample|]) `Seq` FAILWITH)
    where
      sampleCTAddress = [ta|KT1AEseqMV6fk2vtvQCVyA7ZCaxv7cpxtXdB|]
      sampleAddress = unsafe . parseEpAddress $ formatAddress sampleCTAddress
      samplePublicKey = fromRight (error "impossible") $ parsePublicKey
        "edpkuwTWKgQNnhR5v17H2DYHbfcxYepARyrPGbf1tbMoGQAj8Ljr3V"
      sampleSignature = fromRight (error "impossible") $ parseSignature
        "edsigtrs8bK7vNfiR4Kd9dWasVa1bAWaQSu2ipnmLGZuwQa8ktCEMYVKqbWsbJ7zTS8dgYT9tiSUKorWCPFHosL5zPsiDwBQ6vb"
      sampleChainId = fromRight (error "impossible") $ parseChainId "NetXUdfLh6Gm88t"

-- Misc
----------------------------------------------------------------------------

-- | Flatten a provided list of notes to a map of its entrypoints and its
-- corresponding utype. Please refer to 'U.mkEntrypointsMap' in regards to how
-- duplicate entrypoints are handled.
flattenEntrypoints :: U.HandleImplicitDefaultEp ->  ParamNotes t -> Map EpName U.Ty
flattenEntrypoints hide = U.mkEntrypointsMap hide . convertParamNotes

-------------------------------------------------------------------------------
-- Rendering helpers
-------------------------------------------------------------------------------

-- | An extended version of renderDoc for typed values that handles VOp
-- accepts explicit singleton
renderDocSing :: RenderContext -> OpPresence t -> (Value' Instr t, Sing t) -> Doc
renderDocSing pn = \case
  OpAbsent -> renderDoc pn . untypeValue . fst
  OpPresent -> \case
    (VOp op, _) -> renderAnyBuildable op
    -- other cases try to mimic instance RenderDoc U.Value, see "Michelson.Untyped.Value"
    (VOption Nothing, _) -> U.renderNone
    (VOption (Just x), STOption tx) -> U.renderSome pn $ \ctx -> renderDocSing ctx OpPresent (x, tx)
    (VList xs, STList txs) -> renderList OpPresent txs xs
    (VSet ss, STSet tss) -> renderList OpPresent tss $ toList ss
    (VTicket s v a, STTicket tv) -> renderDocSing
      needsParens
      OpPresent
      (VPair (VAddress (EpAddress' s DefEpName), VPair (v, VNat a))
        , STPair STAddress (STPair tv STNat))
    val@(VPair (_, (VPair (_, _))), _) ->
      U.renderValuesList id $ renderLinearizedRightCombValuePair val
    (VPair (l, r), STPair tl tr) -> U.renderPair pn (render tl l) (render tr r)
    (VOr (Left l), STOr tl _) -> U.renderLeft pn $ render tl l
    (VOr (Right r), STOr _ tr) -> U.renderRight pn $ render tr r
    (VMap m, STMap tk tv) -> renderMap (tk, tv, checkOpPresence tk, checkOpPresence tv) m
    (VBigMap _ m, STBigMap tk tv) -> renderMap (tk, tv, checkOpPresence tk, checkOpPresence tv) m
  where render sg v ctx = renderDocSing ctx (checkOpPresence sg) (v, sg)

renderList :: OpPresence t -> Sing t -> [Value' Instr t] -> Doc
renderList osg sg = renderList' $ renderDocSing doesntNeedParens osg . (, sg)

renderMap :: (Sing tk, Sing tv, OpPresence tk, OpPresence tv)
          -> Map (Value' Instr tk) (Value' Instr tv) -> Doc
renderMap ctx = renderList' (renderElt ctx) . Map.toList

renderList' :: (a -> Doc) -> [a] -> Doc
renderList' f = maybe "{ }" (U.renderValuesList f) . nonEmpty

renderElt :: (Sing tk, Sing tv, OpPresence tk, OpPresence tv)
          -> (Value' Instr tk, Value' Instr tv) -> Doc
renderElt (tk, tv, otk, otv) (k, v) =
  U.renderElt' (render otk k tk) (render otv v tv)
  where render o x tx ctx = renderDocSing ctx o (x, tx)

-- | Mimics U.linearizeRightCombValuePair, but for typed values;
-- however, unlike U.linearizeRightCombValuePair renders values on-the-fly.
renderLinearizedRightCombValuePair :: (Value' Instr t, Sing t) -> NonEmpty Doc
renderLinearizedRightCombValuePair = \case
  (VPair (l, r), STPair tl tr) -> renderDocSing doesntNeedParens (checkOpPresence tl) (l, tl)
                               <| renderLinearizedRightCombValuePair (r, tr)
  val@(_, tv)                  -> renderDocSing doesntNeedParens (checkOpPresence tv) val :| []