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

-- TODO [#712]: Remove this next major release
{-# OPTIONS_GHC -Wno-deprecations #-}

module Test.Typecheck
  ( unit_Good_contracts
  , unit_Bad_contracts
  , test_srcPosition
  , unit_Unreachable_code
  , test_Roundtrip
  , test_StackRef
  , test_TCTypeError_display
  , hprop_ValueSeq_as_list
  , test_SELF
  , test_Value_contract
  , test_Nested_Sequences
  , test_Views
  ) where

import Data.Default (def)
import Data.Map qualified as M
import Data.Text.IO.Utf8 qualified as Utf8 (readFile)
import Data.Typeable (typeRep)
import Fmt (build, pretty)
import Hedgehog (Gen, Property, evalNF, forAll, property, (===))
import Hedgehog.Gen qualified as Gen
import Hedgehog.Range qualified as Range
import Test.HUnit (Assertion, assertFailure, (@?=))
import Test.Hspec (expectationFailure)
import Test.Hspec.Expectations (Expectation)
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.HUnit (testCase)
import Test.Tasty.Hedgehog (testProperty)

import Hedgehog.Gen.Michelson.Typed
import Morley.Michelson.ErrorPos (InstrCallStack(..), LetName(..), Pos(..), SrcPos(..), srcPos)
import Morley.Michelson.Parser (MichelsonSource(..), utypeQ)
import Morley.Michelson.Runtime (prepareContractExt)
import Morley.Michelson.Text (MText)
import Morley.Michelson.TypeCheck
import Morley.Michelson.Typed qualified as T
import Morley.Michelson.Untyped (ParameterType(..), buildEpName, noAnn)
import Morley.Michelson.Untyped qualified as Un
import Morley.Tezos.Address (Address(..), mkContractHashHack)
import Morley.Tezos.Core (ChainId, Mutez, Timestamp)
import Morley.Tezos.Crypto (Bls12381Fr, Bls12381G1, Bls12381G2, KeyHash, PublicKey, Signature)
import Morley.Util.Interpolate (itu)
import Morley.Util.MismatchError
import Test.Cleveland.Michelson (failedTest, meanTimeUpperBoundPropNF, sec)
import Test.Cleveland.Michelson.Import (ContractReadError(..), readContract)

import Test.Util.Contracts (getIllTypedContracts, getWellTypedContracts, inContractsDir)

unit_Good_contracts :: Assertion
unit_Good_contracts
  = mapM_ (\f -> do checkFile True f def{ tcVerbose = True } (const pass)
                    checkFile True f def (const pass))
    =<< getWellTypedContracts

unit_Bad_contracts :: Assertion
unit_Bad_contracts
  = mapM_ (\f -> do checkFile False f def{ tcVerbose = True } (const pass)
                    checkFile False f def (const pass))
    =<< getIllTypedContracts

pattern IsSrcPos :: Word -> Word -> InstrCallStack
pattern IsSrcPos l c <- InstrCallStack [] (SrcPos (Pos l) (Pos c))

test_srcPosition :: [TestTree]
test_srcPosition =
  [ testCase "Verify instruction position in a typecheck error" $ do
      checkIllFile (inContractsDir "ill-typed/basic3.tz") $ \case
          TCFailedOnInstr (Un.CONS _) _ (IsSrcPos 8 6) _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/testassert_invalid_stack3.mtz") $ \case
          TCFailedOnInstr Un.DROP _ (IsSrcPos 10 17) _ (Just NotEnoughItemsOnStack) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/testassert_invalid_stack2.mtz") $ \case
          TCExtError _ (IsSrcPos 9 2) (TestAssertError _) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/macro_in_let_fail.mtz") $ \case
          TCFailedOnInstr (Un.COMPARE _) _ (InstrCallStack [LetName "cmpLet"] (SrcPos (Pos 7) (Pos 6))) _
                                              (Just (TypeEqError _)) -> True
          _ -> False
      checkIllFile (inContractsDir "ill-typed/compare_annotation_mismatch.tz") $ \case
          TCFailedOnInstr (Un.COMPARE _) _ _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_map_update.tz") $ \case
          TCFailedOnInstr (Un.UPDATE _) (SomeHST (_ ::& _ ::& (T.NTMap{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_map_get.tz") $ \case
          TCFailedOnInstr (Un.GET _) (SomeHST (_ ::& (T.NTMap{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_map_mem.tz") $ \case
          TCFailedOnInstr (Un.MEM _) (SomeHST (_ ::& (T.NTMap{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_big_map_update.tz") $ \case
          TCFailedOnInstr (Un.UPDATE _) (SomeHST (_ ::& _ ::& (T.NTBigMap{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_big_map_get.tz") $ \case
          TCFailedOnInstr (Un.GET _) (SomeHST (_ ::& (T.NTBigMap{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_big_map_mem.tz") $ \case
          TCFailedOnInstr (Un.MEM _) (SomeHST (_ ::& (T.NTBigMap{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_set_update.tz") $ \case
          TCFailedOnInstr (Un.UPDATE _) (SomeHST (_ ::& _ ::& (T.NTSet{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False

      checkIllFile (inContractsDir "ill-typed/annotation_mismatch_set_mem.tz") $ \case
          TCFailedOnInstr (Un.MEM _) (SomeHST (_ ::& (T.NTSet{}, _, _) ::& SNil)) _ _ (Just (AnnError _)) -> True
          _ -> False
  ]

checkFile
  :: HasCallStack
  => Bool
  -> FilePath
  -> TypeCheckOptions
  -> (TCError -> Expectation)
  -> Expectation
checkFile wellTyped file options onError = do
  c <- prepareContractExt (Just file)
  case typeCheckingWith options $ typeCheckContract c of
    Left err
      | wellTyped ->
        expectationFailure $
        "Typechecker unexpectedly failed on \"" <> file <>
        "\": " <> displayException err
      | otherwise -> onError err
    Right _
      | not wellTyped ->
        assertFailure $
        "Typechecker unexpectedly considered \"" <> file <> "\" well-typed."
      | otherwise -> pass

checkIllFile :: FilePath -> (TCError -> Bool) -> Expectation
checkIllFile file check = checkFile False file def
  \e -> if check e then pass else unexpected file e
  where
    unexpected f e =
      expectationFailure $ "Unexpected typecheck error: " <> displayException e <> " in file: " <> f

unit_Unreachable_code :: Assertion
unit_Unreachable_code = do
  let file = inContractsDir "ill-typed/fail_before_nop.tz"
  let ics = InstrCallStack [] (srcPos 7 13)
  econtract <- readContract @'T.TUnit @'T.TUnit (MSFile file) <$> Utf8.readFile file
  econtract @?= Left (CRETypeCheck (MSFile file) $ TCUnreachableCode ics (one $ Un.WithSrcEx ics $ Un.SeqEx []))

test_Roundtrip :: [TestTree]
test_Roundtrip =
  [ testGroup "Value"
    [ roundtripValue @Integer genValueInt
    , roundtripValue @Timestamp genValueTimestamp
    , roundtripValue @PublicKey $ genValue @'T.TKey
    , roundtripValue @Signature $ genValue @'T.TSignature
    , roundtripValue @ChainId $ genValue @'T.TChainId
    , roundtripValue @(Maybe MText) $ genValue @('T.TOption 'T.TString)
    , roundtripValue @[Maybe Integer] $ genValueList $ genValue @('T.TOption 'T.TInt)
    , roundtripValue @(Set Integer) $ genValue @('T.TSet 'T.TInt)
    , roundtripValue @(Integer, MText) $ genValuePair genValueInt $ genValue @'T.TString
    , roundtripValue @(Integer, (MText, Integer)) $
        genValuePair genValueInt $ genValuePair (genValue @'T.TString) genValueInt
    , roundtripValue @(Either MText Integer) $ genValue @('T.TOr 'T.TString 'T.TInt)
    , roundtripValue @(Map MText Bool) $ genValue @('T.TMap 'T.TString 'T.TBool)
    , roundtripValue @Natural $ genValue @'T.TNat
    , roundtripValue @MText $ genValue @'T.TString
    , roundtripValue @ByteString $ genValue @'T.TBytes
    , roundtripValue @Mutez genValueMutez
    , roundtripValue @Bool $ genValue @'T.TBool
    , roundtripValue @KeyHash genValueKeyHash
    , roundtripValue @Address $ genValue @'T.TAddress
    , roundtripValue @Bls12381Fr $ genValue @'T.TBls12381Fr
    , roundtripValue @Bls12381G1 $ genValue @'T.TBls12381G1
    , roundtripValue @Bls12381G2 $ genValue @'T.TBls12381G2
    ]
  ]
  where
  roundtripValue
    :: forall (a :: Type).
        ( Each [T.SingI, T.HasNoOp] '[T.ToT a]
        , Typeable a
        )
    => Gen (T.Value $ T.ToT a)
    -> TestTree
  roundtripValue gen = testGroup (show $ typeRep (Proxy @a))
    [ roundtripValue' @a T.untypeValue "Readable" gen
    , roundtripValue' @a T.untypeValueOptimized "Optimized" gen
    , roundtripValue' @a T.untypeValueHashable "Hashable" gen
    ]

  roundtripValue'
    :: forall (a :: Type).
       Each [T.SingI, T.HasNoOp] '[T.ToT a]
    => (T.Value $ T.ToT a -> Un.Value)
    -> String
    -> Gen (T.Value $ T.ToT a)
    -> TestTree
  roundtripValue' doUntype name genV =
    testProperty name $ property $ do
      val :: T.Value (T.ToT a) <- forAll $ genV
      let uval = doUntype val
          runTC = typeCheckingWith def . runTypeCheckIsolated . usingReaderT (def @InstrCallStack)
      case runTC $ typeCheckValue uval of
        Right got -> got === val
        Left err -> failedTest $
                    "Type check unexpectedly failed: " <> pretty err

test_StackRef :: [TestTree]
test_StackRef =
  [ testProperty "Typecheck fails when ref is out of bounds" $ property $ do
      let instr = printStRef 2
          hst = stackEl ::& stackEl ::& SNil
      case
        typeCheckingWith def . runTypeCheckIsolated $
        typeCheckList [Un.WithSrcEx def $ Un.PrimEx instr] hst
        of
          Left err -> void $ evalNF err
          Right _ -> failedTest "Typecheck unexpectedly succeded"
  , testProperty "Typecheck time is reasonably bounded" $
      let hst = stackEl ::& SNil
          run i =
            case
              typeCheckingWith def . runTypeCheckIsolated $
              typeCheckList [Un.WithSrcEx def $ Un.PrimEx (printStRef i)] hst
            of
              Left err -> err
              Right _ -> error "Typecheck unexpectedly succeded"
      -- Making code processing performance scale with code size looks like a
      -- good property, so we'd like to avoid scenario when user tries to
      -- access 100500-th element of stack and typecheck hangs as a result
      in  meanTimeUpperBoundPropNF (sec 1) run 100000000000
  ]
  where
    printStRef i = Un.EXT . Un.UPRINT $ Un.PrintComment [Right (Un.StackRef i)]
    stackEl = (T.starNotes @'T.TUnit, T.Dict, noAnn)

test_TCTypeError_display :: [TestTree]
test_TCTypeError_display =
  -- One may say that it's madness to write tests on 'Buildable' instances,
  -- but IMO (martoon) it's worth resulting duplication because tests allow
  -- avoiding silly errors like lost spaces and ensuring general sanity
  -- of used way to display content.
  [ testCase "TypeEqError" $
      build (TypeEqError MkMismatchError{meActual=T.TUnit, meExpected=T.TKey})
      @?= [itu|
        Types not equal:
        Expected: key
        Actual:   unit
        |]

  , testCase "StackEqError" $
      build (StackEqError $ MkMismatchError{meExpected=[T.TUnit, T.TBytes], meActual=[]})
      @?= [itu|
        Stacks not equal:
        Expected: [unit, bytes]
        Actual:   []
        |]

  , testCase "UnsupportedTypes" $
      build (UnsupportedTypeForScope (T.TBigMap T.TInt T.TInt) T.BtHasBigMap)
      @?= "Type 'big_map int int' is unsupported here because it has 'big_map'"

  , testCase "InvalidValueType" $
      build (InvalidValueType T.TUnit)
      @?= "Value type is never a valid `unit`"
  ]

hprop_ValueSeq_as_list :: Property
hprop_ValueSeq_as_list = property $ do
  l <- forAll $ Gen.nonEmpty (Range.linear 0 100) (Gen.integral (Range.linearFrom 0 -1000 1000))
  let
    untypedValue = Un.ValueSeq $ Un.ValueInt <$> l
    typedValue = T.VList $ T.VInt <$> toList l
    runTypeCheckInstr = typeCheckingWith def . runTypeCheckIsolated . usingReaderT def
  runTypeCheckInstr (typeCheckValue untypedValue) === Right typedValue

test_Nested_Sequences :: [TestTree]
test_Nested_Sequences =
  let
    runTC = typeCheckingWith def . runTypeCheckIsolated . usingReaderT (def @InstrCallStack)
    illTypedList = Un.ValueLambda $ Un.SeqEx [Un.SeqEx []] :| [Un.SeqEx []]
    wellTypedList = Un.ValueLambda $ Un.SeqEx [] :| [Un.SeqEx []]
    wellTypedLambda = Un.ValueSeq $ Un.ValueSeq (Un.ValueNil :| []) :| [Un.ValueNil]
  in
    [ testCase "Nested seq with different levels of nesting can't be typechecked as list" $
        case runTC $ typeCheckValue @('T.TList ('T.TList 'T.TInt)) illTypedList of
          Left _      -> pass
          Right other -> assertFailure $ "Unexpected result: " <> pretty other
    , testCase "Nested seq with the same levels of nesting can be typechecked as list" $
        case runTC $ typeCheckValue @('T.TList ('T.TList 'T.TInt)) wellTypedList of
          Right _  -> pass
          Left err -> assertFailure $ "Unexpected error: " <> pretty err
    , testCase "Nested seq with different levels of nesting can be typechecked as lambda" $
        case runTC $ typeCheckValue @('T.TLambda 'T.TInt 'T.TInt) wellTypedLambda of
          Right _  -> pass
          Left err -> assertFailure $ "Unexpected error: " <> pretty err
    ]

test_SELF :: [TestTree]
test_SELF =
  [ testCase "Entrypoint not present" $
      checkFile False (inContractsDir "ill-typed/self-bad-entrypoint.mtz") def $
      \case
        TCFailedOnInstr Un.SELF{} _ _ _ (Just EntrypointNotFound{}) -> pass
        other -> assertFailure $ "Unexpected error: " <> pretty other

  , testCase "Entrypoint type mismatch" $
      checkFile False (inContractsDir "ill-typed/self-entrypoint-type-mismatch.mtz")
        def (const pass)

  , testCase "Entrypoint can be found" $
      checkFile True (inContractsDir "entrypoints/self1.mtz") def
        (const pass)
  ]

test_Value_contract :: [TestTree]
test_Value_contract =
  [ testCase "No contract exists" $
      case typeCheckingWith def $
             typeVerifyParameter @('T.TContract 'T.TUnit) mempty addrUVal1
      of
        Left (TCFailedOnValue _ _ _ _ (Just (UnknownContract _))) -> pass
        res -> assertFailure $ "Unexpected result: " <> either pretty pretty res

  , testCase "Entrypoint does not exist" $
      case typeCheckingWith def $
             typeVerifyParameter @('T.TContract 'T.TKey) env1 addrUVal1
      of
        Left (TCFailedOnValue _ _ _ _ (Just (EntrypointNotFound _))) -> pass
        res -> assertFailure $ "Unexpected result: " <> either pretty pretty res

  , testCase "Correct contract value" $
      case typeCheckingWith def $
             typeVerifyParameter @('T.TContract 'T.TInt) env1 addrUVal2
      of
        Right _ -> pass
        res -> assertFailure $ "Unexpected result: " <> either pretty pretty res
  ]
  where
    addr1' = mkContractHashHack "123"
    addr1 = T.EpAddress (ContractAddress addr1') . unsafe $ buildEpName "a"
    addr2 = T.EpAddress (ContractAddress addr1') . unsafe $ buildEpName "q"
    addrUVal1 = Un.ValueString $ T.mformatEpAddress addr1
    addrUVal2 = Un.ValueString $ T.mformatEpAddress addr2

    env1 = M.fromList
      [ ( addr1',
          unsafe . mkSomeParamType
            $ ParameterType [utypeQ| or (nat %s) (int %q) |] noAnn
        )
      ]

test_Views :: [TestTree]
test_Views =
  [ testCase "Duplicated name" $ do
      checkIllFile (inContractsDir "ill-typed/duplicated_view_name.tz") \case
        TCContractError "Duplicated view name 'add'" _ -> True
        _ -> False

  , testCase "Fully duplicated view" $ do
      checkIllFile (inContractsDir "ill-typed/duplicated_view_full.tz") \case
        TCContractError "Duplicated view name 'add'" _ -> True
        _ -> False

  ]