{-# LANGUAGE ViewPatterns #-}

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

import Data.Default (def)
import qualified Data.Kind as Kind
import qualified Data.Map as M
import Data.Singletons (SingI(..))
import Data.Typeable (typeRep)
import Fmt (build, pretty)
import Test.Hspec (expectationFailure)
import Test.Hspec.Expectations (Expectation)
import Test.HUnit (Assertion, assertFailure, (@?=))
import Test.QuickCheck (Arbitrary, Property, arbitrary, forAll, property, total, within)
import Test.QuickCheck.Instances.Semigroup ()
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.HUnit (testCase)
import Test.Tasty.QuickCheck (testProperty)

import Michelson.ErrorPos (InstrCallStack(..), LetName(..), Pos(..), SrcPos(..), srcPos)
import Michelson.Parser (utypeQ)
import Michelson.Runtime (prepareContract)
import Michelson.Test.Gen ()
import Michelson.Test.Import (ImportContractError(..), readContract)
import Michelson.TypeCheck
import qualified Michelson.Typed as T
import Michelson.Untyped (Type(..), noAnn)
import qualified Michelson.Untyped as Un
import Tezos.Address (Address(..), ContractHash, mkContractHashRaw)
import Tezos.Core (Timestamp)
import Util.IO (readFileUtf8)

import Test.Util.Contracts (getIllTypedContracts, getWellTypedContracts)

unit_Good_contracts :: Assertion
unit_Good_contracts = mapM_ (\f -> checkFile [] True f (const pass)) =<< getWellTypedContracts

unit_Bad_contracts :: Assertion
unit_Bad_contracts = mapM_ (\f -> checkFile [] False f (const pass)) =<< getIllTypedContracts

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

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

      checkIllFile "contracts/ill-typed/testassert_invalid_stack3.mtz" $ \case
          TCFailedOnInstr Un.DROP _ _ (IsSrcPos 6 17) Nothing -> True
          _ -> False

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

      checkIllFile "contracts/ill-typed/macro_in_let_fail.mtz" $ \case
          TCFailedOnInstr (Un.COMPARE _) _ _ (InstrCallStack [LetName "cmpLet"] (SrcPos (Pos 3) (Pos 6)))
                                              (Just (TypeEqError _ _)) -> True
          _ -> False
      checkIllFile "contracts/ill-typed/compare_annotation_mismatch.tz" $ \case
          TCFailedOnInstr (Un.COMPARE _) _ _ _ (Just (AnnError _)) -> True
          _ -> False
  ]
  where
    unexpected f e =
      expectationFailure $ "Unexpected typecheck error: " <> displayException e <> " in file: " <> f
    checkIllFile file check = checkFile [] False file $
      \e -> if check e then pass else unexpected file e

checkFile
  :: HasCallStack
  => [(ContractHash, Type)]
  -> Bool
  -> FilePath
  -> (TCError -> Expectation)
  -> Expectation
checkFile originatedContracts wellTyped file onError = do
  c <- prepareContract (Just file)
  case doTC c of
    Left err
      | wellTyped ->
        expectationFailure $
        "Typechecker unexpectedly failed on " <> show file <> ": " <> displayException err
      | otherwise -> onError err
    Right _
      | not wellTyped ->
        assertFailure $
        "Typechecker unexpectedly considered " <> show file <> " well-typed."
      | otherwise -> pass
  where
    doTC = typeCheckContract (M.fromList originatedContracts)

unit_Unreachable_code :: Assertion
unit_Unreachable_code = do
  let file = "contracts/ill-typed/fail_before_nop.tz"
  let ics = InstrCallStack [] (srcPos 3 13)
  econtract <- readContract @'T.TUnit @'T.TUnit file <$> readFileUtf8 file
  econtract @?= Left (ICETypeCheck $ TCUnreachableCode ics (one $ Un.WithSrcEx ics $ Un.SeqEx []))

test_Roundtrip :: [TestTree]
test_Roundtrip =
  [ testGroup "Value"
    [ roundtripValue @Integer
    , roundtripValue @Timestamp
    ]
  ]
  where
  roundtripValue
    :: forall (a :: Kind.Type).
        ( Each [Typeable, SingI, T.HasNoOp] '[T.ToT a]
        , Typeable a, Arbitrary (T.Value $ T.ToT a)
        )
    => TestTree
  roundtripValue =
    testProperty (show $ typeRep (Proxy @a)) $
      property $ \(val :: T.Value (T.ToT a)) ->
        let uval = T.untypeValue val
            runTC = runTypeCheckIsolated . usingReaderT (def @InstrCallStack)
        in case runTC $ typeVerifyValue uval of
            Right got -> got @?= val
            Left err -> expectationFailure $
                        "Type check unexpectedly failed: " <> pretty err

test_StackRef :: [TestTree]
test_StackRef =
  [ testProperty "Typecheck fails when ref is out of bounds" $
      let instr = printStRef 2
          hst = stackEl ::& stackEl ::& SNil
      in case
          runTypeCheck (error "no contract param") mempty $
          typeCheckList [Un.WithSrcEx def $ Un.PrimEx instr] hst
          of
            Left err -> total $ show @Text err
            Right _ -> error "Typecheck unexpectedly succeded"
  , testProperty "Typecheck time is reasonably bounded" $ within 1000 $
    -- 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
    let instr = printStRef 100000000000
        hst = stackEl ::& SNil
    in case
        runTypeCheck (error "no contract param") mempty $
        typeCheckList [Un.WithSrcEx def $ Un.PrimEx instr] hst
      of
        Left err -> total $ show @Text err
        Right _ -> error "Typecheck unexpectedly succeded"
  ]
  where
    printStRef i = Un.EXT . Un.UPRINT $ Un.PrintComment [Right (Un.StackRef i)]
    stackEl = (sing @'T.TUnit, T.starNotes, 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 T.TUnit T.TKey)
      @?= "Types not equal: unit /= key"

  , testCase "StackEqError" $
      build (StackEqError [T.TUnit, T.Tc T.CBytes] [])
      @?= "Stacks not equal: [unit, bytes] /= []"

  , testCase "UnsupportedTypes" $
      build (UnsupportedTypes [T.TUnit])
      @?= "Unsupported types: [unit]"

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

prop_ValueSeq_as_list :: Property
prop_ValueSeq_as_list =
  forAll @(NonEmpty Integer) arbitrary $ \l ->
  let
    untypedValue = Un.ValueSeq $ Un.ValueInt <$> l
    typedValue = T.VList $ (T.VC . T.CvInt) <$> toList l
    runTypeCheckInstr = runTypeCheckIsolated . usingReaderT def
  in runTypeCheckInstr (typeVerifyValue untypedValue) == Right typedValue

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

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

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

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

  , testCase "Entrypoint does not exist" $
      case doTypeCheckVal @('T.TContract 'T.TKey) env1 addrUVal1 of
        Left (TCFailedOnValue _ _ _ _ (Just (EntryPointNotFound _))) -> pass
        res -> assertFailure $ "Unexpected result: " <> show res

  , testCase "Correct contract value" $
      case doTypeCheckVal @('T.TContract ('T.Tc 'T.CInt)) env1 addrUVal2 of
        Right _ -> pass
        res -> assertFailure $ "Unexpected result: " <> show res
  ]
  where
    addr1' = mkContractHashRaw "123"
    addr1 = T.EpAddress (ContractAddress addr1') (T.EpNameUnsafe "a")
    addr2 = T.EpAddress (ContractAddress addr1') (T.EpNameUnsafe "q")
    addrUVal1 = Un.ValueString $ T.mformatEpAddress addr1
    addrUVal2 = Un.ValueString $ T.mformatEpAddress addr2

    env1 = M.fromList
      [ ( addr1'
        , [utypeQ| ( nat %s | int %q ) |]
        )
      ]

    doTypeCheckVal
      :: (Typeable t, SingI t)
      => TcOriginatedContracts -> Un.Value -> Either TCError (T.Value t)
    doTypeCheckVal env uval =
      runTypeCheck (error "hello there") env $ usingReaderT def $
        typeVerifyValue uval