{-# OPTIONS_GHC -fno-warn-orphans #-}

module Michelson.Typed.Convert
  ( convertContract
  , convertFullContract
  , instrToOps
  , untypeValue
  ) where

import qualified Data.Map as Map
import Data.Singletons (SingI(sing), demote)
import Fmt (pretty)

import Michelson.Text
import Michelson.Typed.Annotation (Notes(..))
import Michelson.Typed.CValue
import Michelson.Typed.EntryPoints
import Michelson.Typed.Extract (mkUType, toUType)
import Michelson.Typed.Instr as Instr
import Michelson.Typed.Scope
import Michelson.Typed.Sing (Sing(..), fromSingCT)
import Michelson.Typed.T (CT(..), T(..))
import Michelson.Typed.Value
import qualified Michelson.Untyped as U
import Tezos.Core (mformatChainId, unMutez)
import Tezos.Crypto (mformatKeyHash, mformatPublicKey, mformatSignature)
import Util.Peano
import Util.Typeable

convertContract
  :: forall param store . (SingI param, SingI store)
  => Contract param store -> U.Contract
convertContract contract =
  U.Contract
    { para = untypeDemoteT @param
    , stor = untypeDemoteT @store
    , code = instrToOps contract
    }

addCtNote :: U.TypeAnn -> U.Comparable -> U.Comparable
addCtNote ta (U.Comparable ct _) = U.Comparable ct ta

convertFullContract
  :: forall param store . (SingI param, SingI store)
  => FullContract param store -> U.Contract
convertFullContract fc =
  let c = convertContract (fcCode fc)
  in c { U.para = mkUType sing (fcParamNotes fc)
       , U.stor = mkUType sing (fcStoreNotes fc) }

-- | Convert a typed 'Val' to an untyped 'Value'.
--
-- For full isomorphism type of the given 'Val' should not contain
-- 'TOperation' - a compile error will be raised otherwise.
-- You can analyse its presence with 'checkOpPresence' function.
untypeValue ::
     forall t . (SingI t, HasNoOp t)
  => Value' Instr t
  -> U.Value
untypeValue val = case (val, sing @t) of
  (VC cVal, _) ->
    untypeCValue cVal
  (VKey b, _) ->
    U.ValueString $ mformatPublicKey b
  (VUnit, _) ->
    U.ValueUnit
  (VSignature b, _) ->
    U.ValueString $ mformatSignature b
  (VChainId b, _) ->
    U.ValueString $ mformatChainId b
  (VOption (Just x), STOption _) ->
    U.ValueSome (untypeValue x)
  (VOption Nothing, STOption _) ->
    U.ValueNone
  (VList l, STList _) ->
    vList U.ValueSeq $ map untypeValue l
  (VSet s, _) ->
    vList U.ValueSeq $ map untypeCValue $ toList s
  (VContract addr sepc, _) ->
    U.ValueString . mformatEpAddress $ EpAddress addr (sepcName sepc)

  (VPair (l, r), STPair lt _) ->
    case checkOpPresence lt of
      OpAbsent -> U.ValuePair (untypeValue l) (untypeValue r)

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

  (VOr (Right x), STOr lt _) ->
    case checkOpPresence lt of
      OpAbsent -> U.ValueRight (untypeValue x)

  (VLam (rfAnyInstr -> ops :: Instr '[inp] '[out]), _) ->
    vList U.ValueLambda $ instrToOps ops

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

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

untypeDemoteT :: forall (t :: T). SingI t => U.Type
untypeDemoteT = toUType $ demote @t

untypeCValue :: CValue t -> U.Value
untypeCValue cVal = case cVal of
  CvInt i -> U.ValueInt i
  CvNat i -> U.ValueInt $ toInteger i
  CvString s -> U.ValueString s
  CvBytes b -> U.ValueBytes $ U.InternalByteString b
  CvMutez m -> U.ValueInt $ toInteger $ unMutez m
  CvBool True -> U.ValueTrue
  CvBool False -> U.ValueFalse
  CvKeyHash h -> U.ValueString $ mformatKeyHash h
  CvTimestamp t -> U.ValueString $ mkMTextUnsafe $ pretty t
  CvAddress a -> U.ValueString $ mformatEpAddress a

instrToOps :: HasCallStack => Instr inp out -> [U.ExpandedOp]
instrToOps instr = case instr of
  Nop -> []
  Seq i1 i2 -> instrToOps i1 <> instrToOps i2
  Nested sq -> one $ U.SeqEx $ instrToOps sq
  DocGroup _ sq -> instrToOps sq
  Ext (ext :: ExtInstr inp) -> (U.PrimEx . U.EXT) <$> extInstrToOps ext
  FrameInstr _ i -> instrToOps i
  InstrWithNotes n i -> case i of
    Nop -> instrToOps i
    Seq _ _ -> instrToOps i
    Nested _ -> instrToOps i
    DocGroup _ _ -> instrToOps i
    Ext _ -> instrToOps i
    InstrWithNotes _ _ -> instrToOps i
    -- For inner instruction, filter out values that we don't want to apply
    -- annotations to and delegate it's conversion to this function itself.
    -- If none of the above, convert a single instruction and copy annotations
    -- to it.
    _ -> [U.PrimEx $ handleInstrAnnotate i n]
  i -> [U.PrimEx $ handleInstr i]
  -- TODO pva701: perphaps, typed instr has to hold a position too
  -- to make it possible to report a precise location of a runtime error
  where
    handleInstrAnnotate
      :: forall inp' out' . HasCallStack
      => Instr inp' out' -> PackedNotes out' -> U.ExpandedInstr
    handleInstrAnnotate ins' (PackedNotes notes' sing') = let
      x = handleInstr ins' in addInstrNote x sing' notes'
      where
        addInstrNote
          :: HasCallStack
          => U.ExpandedInstr -> Sing t -> Notes t -> U.ExpandedInstr
        addInstrNote ins s nte = case (s, ins, nte) of
            (_, U.PUSH va _ v, _) -> U.PUSH va (mkUType s nte) v
            (_, U.SOME _ va, NTOption ta _) -> U.SOME ta va
            (STOption sp, U.NONE _ va _, NTOption ta nt) -> U.NONE ta va (mkUType sp nt)
            (_, U.UNIT _ va, NTUnit ta) -> U.UNIT ta va
            (_, U.PAIR _ va _ _, NTPair ta f1 f2 _ _) -> U.PAIR ta va f1 f2
            (_, U.CAR va f1, _) -> U.CAR va f1
            (_, U.CDR va f1, _) -> U.CDR va f1
            (STOr _ sq, U.LEFT _ va _ _ _, NTOr ta f1 f2 _ n2) ->
              U.LEFT ta va f1 f2 (mkUType sq n2)
            (STOr sp _, U.RIGHT _ va _ _ _, NTOr ta f1 f2 n1 _) ->
              U.RIGHT ta va f1 f2 (mkUType sp n1)
            (STList sp, U.NIL _ va _, NTList ta n) -> U.NIL ta va (mkUType sp n)
            (_, U.EMPTY_SET _ va ct, NTSet ta1 ta2) ->
              U.EMPTY_SET ta1 va (addCtNote ta2 ct)
            (STMap _ sq, U.EMPTY_MAP _ va ct _, NTMap ta1 ta2 n) ->
              U.EMPTY_MAP ta1 va (addCtNote ta2 ct) (mkUType sq n)
            (STBigMap _ sq, U.EMPTY_BIG_MAP _ va ct _, NTBigMap ta1 ta2 n) ->
              U.EMPTY_BIG_MAP ta1 va (addCtNote ta2 ct) (mkUType sq n)
            (STLambda sp sq, U.LAMBDA va _ _ ops, NTLambda _ n1 n2) ->
              U.LAMBDA va (mkUType sp n1) (mkUType sq n2) ops
            (_, U.CAST va _, n) -> U.CAST va (mkUType s n)
            (STOption sp, U.UNPACK _ va _, NTOption ta nt) -> U.UNPACK ta va (mkUType sp nt)
            (STOption (STContract sp), U.CONTRACT va fa _, NTOption _ (NTContract _ nt)) ->
              U.CONTRACT va fa (mkUType sp nt)
            (_, U.CONTRACT va fa t, NTOption _ _) -> U.CONTRACT va fa t
            (_, a@(U.APPLY {}), _) -> a
            (_, a@(U.CHAIN_ID {}), _) -> a
            (_, a@(U.EXT _), _) -> a
            (_, a@(U.DROP), _) -> a
            (_, a@(U.DROPN _), _) -> a
            (_, a@(U.DUP _), _) -> a
            (_, a@(U.SWAP), _) -> a
            (_, a@(U.DIG {}), _) -> a
            (_, a@(U.DUG {}), _) -> a
            (_, a@(U.IF_NONE _ _), _) -> a
            (_, a@(U.CONS _), _) -> a
            (_, a@(U.IF_LEFT _ _), _) -> a
            (_, a@(U.IF_CONS _ _), _) -> a
            (_, a@(U.SIZE _), _) -> a
            (_, a@(U.MAP _ _), _) -> a
            (_, a@(U.ITER _), _) -> a
            (_, a@(U.MEM _), _) -> a
            (_, a@(U.GET _), _) -> a
            (_, a@(U.UPDATE _), _) -> a
            (_, a@(U.IF _ _), _) -> a
            (_, a@(U.LOOP _), _) -> a
            (_, a@(U.LOOP_LEFT _), _) -> a
            (_, a@(U.EXEC _), _) -> a
            (_, a@(U.DIP _), _) -> a
            (_, a@(U.DIPN {}), _) -> a
            (_, a@(U.FAILWITH), _) -> a
            (_, a@(U.RENAME _), _) -> a
            (_, a@(U.PACK _), _) -> a
            (_, a@(U.CONCAT _), _) -> a
            (_, a@(U.SLICE _), _) -> a
            (_, a@(U.ISNAT _), _) -> a
            (_, a@(U.ADD _), _) -> a
            (_, a@(U.SUB _), _) -> a
            (_, a@(U.MUL _), _) -> a
            (_, a@(U.EDIV _), _) -> a
            (_, a@(U.ABS _), _) -> a
            (_, a@(U.NEG _), _) -> a
            (_, a@(U.LSL _), _) -> a
            (_, a@(U.LSR _), _) -> a
            (_, a@(U.OR _), _) -> a
            (_, a@(U.AND _), _) -> a
            (_, a@(U.XOR _), _) -> a
            (_, a@(U.NOT _), _) -> a
            (_, a@(U.COMPARE _), _) -> a
            (_, a@(U.EQ _), _) -> a
            (_, a@(U.NEQ _), _) -> a
            (_, a@(U.LT _), _) -> a
            (_, a@(U.GT _), _) -> a
            (_, a@(U.LE _), _) -> a
            (_, a@(U.GE _), _) -> a
            (_, a@(U.INT _), _) -> a
            (_, a@(U.SELF _ _), _) -> a
            (_, a@(U.TRANSFER_TOKENS _), _) -> a
            (_, a@(U.SET_DELEGATE _), _) -> a
            (_, a@(U.CREATE_CONTRACT {}), _) -> a
            (_, a@(U.IMPLICIT_ACCOUNT _), _) -> a
            (_, a@(U.NOW _), _) -> a
            (_, a@(U.AMOUNT _), _) -> a
            (_, a@(U.BALANCE _), _) -> a
            (_, a@(U.CHECK_SIGNATURE _), _) -> a
            (_, a@(U.SHA256 _), _) -> a
            (_, a@(U.SHA512 _), _) -> a
            (_, a@(U.BLAKE2B _), _) -> a
            (_, a@(U.HASH_KEY _), _) -> a
            (_, a@(U.STEPS_TO_QUOTA _), _) -> a
            (_, a@(U.SOURCE _), _) -> a
            (_, a@(U.SENDER _), _) -> a
            (_, a@(U.ADDRESS _), _) -> a
            (_, b, c) -> error $ "addInstrNote: Unexpected instruction/annotation combination: " <> show (b, c)

    handleInstr :: Instr inp out -> U.ExpandedInstr
    handleInstr (InstrWithNotes _ _) = error "impossible"
    handleInstr (FrameInstr _ _) = error "impossible"
    handleInstr (Seq _ _) = error "impossible"
    handleInstr Nop = error "impossible"
    handleInstr (Ext _) = error "impossible"
    handleInstr (Nested _) = error "impossible"
    handleInstr DocGroup{} = error "impossible"
    handleInstr DROP = U.DROP
    handleInstr (DROPN s) = U.DROPN (fromIntegral $ peanoValSing s)
    handleInstr DUP = U.DUP U.noAnn
    handleInstr SWAP = U.SWAP
    handleInstr (DIG s) = U.DIG (fromIntegral $ peanoValSing s)
    handleInstr (DUG s) = U.DUG (fromIntegral $ peanoValSing s)
    handleInstr i@(PUSH val) | _ :: Instr inp1 (t ': s) <- i =
      let value = untypeValue val
      in U.PUSH U.noAnn (untypeDemoteT @t) value
    handleInstr i@NONE | _ :: Instr inp1 ('TOption a ': inp1) <- i =
      U.NONE U.noAnn U.noAnn (untypeDemoteT @a)
    handleInstr SOME = U.SOME U.noAnn U.noAnn
    handleInstr UNIT = U.UNIT U.noAnn U.noAnn
    handleInstr (IF_NONE i1 i2) = U.IF_NONE (instrToOps i1) (instrToOps i2)
    handleInstr PAIR = U.PAIR U.noAnn U.noAnn U.noAnn U.noAnn
    handleInstr (AnnCAR fn) = U.CAR U.noAnn fn
    handleInstr (AnnCDR fn) = U.CDR U.noAnn fn
    handleInstr i@LEFT | _ :: Instr (a ': s) ('TOr a b ': s) <- i =
      U.LEFT U.noAnn U.noAnn U.noAnn U.noAnn (untypeDemoteT @b)
    handleInstr i@RIGHT | _ :: Instr (b ': s) ('TOr a b ': s) <- i =
      U.RIGHT U.noAnn U.noAnn U.noAnn U.noAnn (untypeDemoteT @a)
    handleInstr (IF_LEFT i1 i2) = U.IF_LEFT (instrToOps i1) (instrToOps i2)
    handleInstr i@NIL | _ :: Instr s ('TList p ': s) <- i =
      U.NIL U.noAnn U.noAnn (untypeDemoteT @p)
    handleInstr CONS = U.CONS U.noAnn
    handleInstr (IF_CONS i1 i2) = U.IF_CONS (instrToOps i1) (instrToOps i2)
    handleInstr SIZE = U.SIZE U.noAnn
    handleInstr i@EMPTY_SET | _ :: Instr s ('TSet e ': s) <- i =
      U.EMPTY_SET U.noAnn U.noAnn (U.Comparable (fromSingCT (sing @e)) U.noAnn)
    handleInstr i@EMPTY_MAP | _ :: Instr s ('TMap a b ': s) <- i =
      U.EMPTY_MAP U.noAnn U.noAnn (U.Comparable (fromSingCT (sing @a)) U.noAnn)
       (untypeDemoteT @b)
    handleInstr i@EMPTY_BIG_MAP | _ :: Instr s ('TBigMap a b ': s) <- i =
      U.EMPTY_BIG_MAP U.noAnn U.noAnn (U.Comparable (fromSingCT (sing @a)) U.noAnn)
       (untypeDemoteT @b)
    handleInstr (MAP op) = U.MAP U.noAnn $ instrToOps op
    handleInstr (ITER op) = U.ITER $ instrToOps op
    handleInstr MEM = U.MEM U.noAnn
    handleInstr GET = U.GET U.noAnn
    handleInstr UPDATE = U.UPDATE U.noAnn
    handleInstr (IF op1 op2) = U.IF (instrToOps op1) (instrToOps op2)
    handleInstr (LOOP op) = U.LOOP (instrToOps op)
    handleInstr (LOOP_LEFT op) = U.LOOP_LEFT (instrToOps op)
    handleInstr i@(LAMBDA {}) | LAMBDA (VLam l) :: Instr s ('TLambda i o ': s) <- i =
      U.LAMBDA U.noAnn (untypeDemoteT @i) (untypeDemoteT @o) (instrToOps $ rfAnyInstr l)
    handleInstr EXEC = U.EXEC U.noAnn
    handleInstr APPLY = U.APPLY U.noAnn
    handleInstr (DIP op) = U.DIP (instrToOps op)
    handleInstr (DIPN s op) =
      U.DIPN (fromIntegral $ peanoValSing s) (instrToOps op)
    handleInstr FAILWITH = U.FAILWITH
    handleInstr i@CAST | _ :: Instr (a ': s) (a ': s) <- i =
      U.CAST U.noAnn (untypeDemoteT @a)
    handleInstr RENAME = U.RENAME U.noAnn
    handleInstr PACK = U.PACK U.noAnn
    handleInstr i@UNPACK
      | _ :: Instr ('Tc 'CBytes ': s) ('TOption a ': s) <- i =
          U.UNPACK U.noAnn U.noAnn (untypeDemoteT @a)
    handleInstr CONCAT = U.CONCAT U.noAnn
    handleInstr CONCAT' = U.CONCAT U.noAnn
    handleInstr SLICE = U.SLICE U.noAnn
    handleInstr ISNAT = U.ISNAT U.noAnn
    handleInstr ADD = U.ADD U.noAnn
    handleInstr SUB = U.SUB U.noAnn
    handleInstr MUL = U.MUL U.noAnn
    handleInstr EDIV = U.EDIV U.noAnn
    handleInstr ABS = U.ABS U.noAnn
    handleInstr NEG = U.NEG U.noAnn
    handleInstr LSL = U.LSL U.noAnn
    handleInstr LSR = U.LSR U.noAnn
    handleInstr OR = U.OR U.noAnn
    handleInstr AND = U.AND U.noAnn
    handleInstr XOR = U.XOR U.noAnn
    handleInstr NOT = U.NOT U.noAnn
    handleInstr COMPARE = U.COMPARE U.noAnn
    handleInstr Instr.EQ = U.EQ U.noAnn
    handleInstr NEQ = U.NEQ U.noAnn
    handleInstr Instr.LT = U.LT U.noAnn
    handleInstr Instr.GT = U.GT U.noAnn
    handleInstr LE = U.LE U.noAnn
    handleInstr GE = U.GE U.noAnn
    handleInstr INT = U.INT U.noAnn
    handleInstr (SELF sepc) =
      U.SELF U.noAnn (epNameToRefAnn $ sepcName sepc)
    handleInstr i@(CONTRACT nt epName)
      | _ :: Instr ('Tc 'CAddress ': s) ('TOption ('TContract p) ': s) <- i =
          let fa = epNameToRefAnn epName
          in U.CONTRACT U.noAnn fa (mkUType (sing @p) nt)
    handleInstr TRANSFER_TOKENS = U.TRANSFER_TOKENS U.noAnn
    handleInstr SET_DELEGATE = U.SET_DELEGATE U.noAnn
    handleInstr i@(CREATE_CONTRACT fullContract)
      | _ :: Instr
          (  'TOption ('Tc 'CKeyHash)
          ': 'Tc 'CMutez
          ': g
          ': s)
          ('TOperation ': 'Tc 'CAddress ': s) <- i =
        U.CREATE_CONTRACT U.noAnn U.noAnn (convertFullContract fullContract)
    handleInstr IMPLICIT_ACCOUNT = U.IMPLICIT_ACCOUNT U.noAnn
    handleInstr NOW = U.NOW U.noAnn
    handleInstr AMOUNT = U.AMOUNT U.noAnn
    handleInstr BALANCE = U.BALANCE U.noAnn
    handleInstr CHECK_SIGNATURE = U.CHECK_SIGNATURE U.noAnn
    handleInstr SHA256 = U.SHA256 U.noAnn
    handleInstr SHA512 = U.SHA512 U.noAnn
    handleInstr BLAKE2B = U.BLAKE2B U.noAnn
    handleInstr HASH_KEY = U.HASH_KEY U.noAnn
    handleInstr STEPS_TO_QUOTA = U.STEPS_TO_QUOTA U.noAnn
    handleInstr SOURCE = U.SOURCE U.noAnn
    handleInstr SENDER = U.SENDER U.noAnn
    handleInstr ADDRESS = U.ADDRESS U.noAnn
    handleInstr CHAIN_ID = U.CHAIN_ID U.noAnn

untypeStackRef :: StackRef s -> U.StackRef
untypeStackRef (StackRef n) = U.StackRef (peanoVal 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{} -> []

-- 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
  i1 == i2 = instrToOps i1 == instrToOps i2

instance Typeable s => Eq (TestAssert s) where
  TestAssert   name1 pattern1 instr1
    ==
    TestAssert name2 pattern2 instr2
    = and
    [ name1 == name2
    , pattern1 `eqParam1` pattern2
    , instr1 `eqParam2` instr2
    ]