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

{-# OPTIONS_GHC -Wno-orphans #-}

module Morley.Michelson.Typed.Convert
  ( convertParamNotes
  , convertView
  , convertSomeView
  , convertContractCode
  , convertContractCodeOptimized
  , convertContract
  , convertContractOptimized
  , 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.Default (def)
import Data.List.NonEmpty ((<|))
import Data.Map qualified as Map
import Data.Singletons (Sing, demote)
import Fmt (Buildable(..), Doc, fmt, listF, pretty)
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.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 = convertContractCode' Readable

-- | Convert typed t'ContractCode' to an untyped t'U.Contract' using optimized
-- representation.
convertContractCodeOptimized
  :: forall param store . (SingI param, SingI store)
  => ContractCode param store -> U.Contract
convertContractCodeOptimized = convertContractCode' Optimized

convertContractCode'
  :: forall param store . (SingI param, SingI store)
  => UntypingOptions -> ContractCode param store -> U.Contract
convertContractCode' opts contract =
  U.Contract
    { contractParameter = U.ParameterType (untypeDemoteT @param) U.noAnn
    , contractStorage = untypeDemoteT @store
    , contractCode = seqOrSingleOp $ instrToOpsImpl opts $ unContractCode contract
    , entriesOrder = U.canonicalEntriesOrder
    , contractViews = def
    }

convertView :: forall arg store ret. View arg store ret -> U.View
convertView = convertView' Readable

convertView' :: forall arg store ret. UntypingOptions -> View arg store ret -> U.View
convertView' opts View{..} =
  U.View
    { viewName = vName
    , viewArgument = untypeDemoteT @arg
    , viewReturn = untypeDemoteT @ret
    , viewCode = seqOrSingleOp $ instrToOpsImpl opts vCode
    }

seqOrSingleOp :: [U.ExpandedOp] -> U.ExpandedOp
seqOrSingleOp = \case
  [x] -> x
  xs -> U.SeqEx xs

convertSomeView :: SomeView st -> U.View
convertSomeView = convertSomeView' Readable

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

-- | Convert typed t'Contract' to an untyped t'U.Contract'.
convertContract :: Contract param store -> U.Contract
convertContract = convertContract' Readable

-- | Convert typed t'Contract' to untyped t'U.Contract' using optimized
-- representation.
convertContractOptimized :: Contract param store -> U.Contract
convertContractOptimized = convertContract' Optimized

convertContract' :: UntypingOptions -> Contract param store -> U.Contract
convertContract' opts Contract{..} =
  let c = convertContractCode' opts cCode
  in c { U.contractParameter = convertParamNotes cParamNotes
       , U.contractStorage = mkUType cStoreNotes
       , U.entriesOrder = cEntriesOrder
       , U.contractViews = U.ViewsSet $ convertSomeView' opts <$> unViewsSet cViews
       }

-- 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 :: ForbidOp 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 :: ForbidOp t => Value' Instr t -> U.Value
untypeValueHashable = untypeValueImpl' Hashable

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

untypeValueImpl'
  :: ForbidOp 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 'checkTPresence' function.
untypeValueImpl
  :: ForbidOp t
  => UntypingOptions
  -> Sing t
  -> Value' Instr t
  -> U.Value
untypeValueImpl opts sng val = case val 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
  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 <- sng ->
    U.ValueSome (untypeValueImpl opts op x)
  VOption Nothing -> U.ValueNone
  VList l | STList lt <- sng ->
    vList U.ValueSeq $ map (untypeValueImpl opts lt) l
  VSet s | STSet st <- sng ->
    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 <- sng ->
    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)
  VPair (l, r) -> case opts of
      Optimized -> U.ValueSeq $ pairToSeq (val, sng)
      _ | STPair lt rt <- sng -> deMorganForbidT SPSOp lt rt $
        U.ValuePair (untypeValueImpl opts lt l) (untypeValueImpl opts rt r)

  VOr (Left x) | STOr lt rt <- sng -> deMorganForbidT SPSOp lt rt $
    U.ValueLeft (untypeValueImpl opts lt x)

  VOr (Right x) | STOr lt rt <- sng -> deMorganForbidT SPSOp lt rt $
    U.ValueRight (untypeValueImpl opts rt x)

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

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

  VMap m | STMap kt vt <- sng -> deMorganForbidT SPSOp kt vt $
    vList U.ValueMap $ Map.toList m <&> \(k, v) ->
      U.Elt (untypeValueImpl opts kt k) (untypeValueImpl opts vt v)

  VBigMap _ m | STBigMap kt vt <- sng -> deMorganForbidT SPSOp kt vt $
    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 :: ForbidOp ty
              => (Value ty, Sing ty)
              -> NonEmpty U.Value
    pairToSeq = \case
      (VPair (a, b), STPair l r) -> deMorganForbidT SPSOp l r $
        untypeValueImpl opts l a <| pairToSeq (b, r)
      (v, vt) -> untypeValueImpl opts vt v :| []

    hashToBytes :: Hash kind -> ByteString
    hashToBytes Hash{..} = (<> hBytes) $
      case hTag of
        HashKey kt -> one $ keyTypeTag kt
        HashContract -> ""
        HashSR  -> ""

    keyToBytes :: PublicKey -> ByteString
    keyToBytes x = one (keyTypeTag $ publicKeyType x) <> publicKeyToBytes x

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

    encodeAddress :: forall kind. KindedAddress kind -> ByteString
    encodeAddress addr = one (addressKindTag ak) <> case addr of
      ImplicitAddress keyHash -> hashToBytes keyHash
      ContractAddress hash -> hashToBytes hash <> "\x00"
      SmartRollupAddress hash -> hashToBytes hash <> "\x00"
      where ak = demote @kind \\ addressKindSanity addr

    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 $ instrToOpsImpl opts sq
  DocGroup _ sq -> instrToOpsImpl opts sq
  Ext (ext :: ExtInstr inp) -> (U.PrimEx . U.EXT) <$> extInstrToOps ext
  -- 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
    AnnNAT ann -> annotateInstr ann U.NAT
    AnnBYTES ann -> annotateInstr ann U.BYTES
    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' opts 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.ExpandedExtInstr]
extInstrToOps = \case
  PRINT pc -> one $ U.UPRINT (untypePrintComment pc)
  TEST_ASSERT (TestAssert nm pc i) ->
    one $ U.UTEST_ASSERT $
    U.TestAssert nm (untypePrintComment pc) (instrToOpsImpl Readable 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 ForbidOp t => RenderDoc (Value' Instr t) where
  renderDoc pn = renderDoc pn . untypeValue

instance Buildable (Value' Instr t) where
  build val = let tv = withValueTypeSanity val sing
    in renderDocSing doesntNeedParens (checkTPresence SPSOp tv) (val, tv)

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. WellTyped 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
    STNever            -> Nothing
    STSaplingState _   -> Nothing
    STSaplingTransaction _ -> Nothing
    STOption t -> VOption . Just <$> sampleTypedValue t
    STList t -> VList . one <$> sampleTypedValue t
    STSet t -> VSet . one <$> sampleTypedValue t
    STContract _ -> pure . VContract (eaAddress sampleAddress) $ SomeEpc unsafeEpcCallRoot
    STTicket t -> do
      dat <- sampleTypedValue t
      VNat amount <- sampleTypedValue STNat
      pure $ VTicket (MkAddress sampleCTAddress) dat amount
    STPair t1 t2 -> VPair ... (,) <$> sampleTypedValue t1 <*> sampleTypedValue t2
    STOr tl tr ->
          VOr . Left <$> sampleTypedValue tl
      <|> VOr . Right <$> sampleTypedValue tr
    STMap t1 t2 ->
      (\k v -> VMap $ Map.fromList [(k, v)]) <$> sampleTypedValue t1 <*> sampleTypedValue t2
    STBigMap t1 t2 -> (\k v -> VBigMap Nothing $ Map.fromList [(k, v)]) <$>
      sampleTypedValue t1 <*> sampleTypedValue t2
    STLambda _ (t2 :: Sing 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 -> TPresence 'PSOp t -> (Value' Instr t, Sing t) -> Doc
renderDocSing pn = \case
  TAbsent -> renderDoc pn . untypeValue . fst
  TPresent -> \case
    (VOp op, _) -> build 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 TPresent (x, tx)
    (VList xs, STList txs) -> renderList TPresent txs xs
    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, TPresent) m \\ comparableImplies tk
    (VBigMap _ m, STBigMap tk tv) -> renderMap (tk, tv, TPresent) m \\ comparableImplies tk
    (VSet{}, STSet tv) -> case checkComparability tv of
    (VTicket{}, STTicket tv) -> case checkComparability tv of
  where render sg v ctx = renderDocSing ctx (checkTPresence SPSOp sg) (v, sg)

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

renderMap
  :: ForbidOp tk
  => (Sing tk, Sing tv, TPresence 'PSOp 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
  :: ForbidOp tk
  => (Sing tk, Sing tv, TPresence 'PSOp tv)
  -> (Value' Instr tk, Value' Instr tv) -> Doc
renderElt (tk, tv, otv) (k, v) =
  U.renderElt' (render TAbsent 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 (checkTPresence SPSOp tl) (l, tl)
                               <| renderLinearizedRightCombValuePair (r, tr)
  val@(_, tv)                  -> renderDocSing doesntNeedParens (checkTPresence SPSOp tv) val :| []