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

-- | Test utilities to ensure the proper layout of non-dupable elements
-- within datatypes.
module Lorentz.Test.DupableScan
  ( CheckDupablesDistribution
  , VerifyDupablesDistribution
  , checkDupablesDistribution
  , testDupablesDistribution
  , BadElement (..)
  ) where

import Data.Typeable (TypeRep, typeRep)
import Fmt (Buildable(..), pretty, (+|), (|+))
import GHC.Generics qualified as G
import Prelude.Singletons (demote)
import Test.HUnit (assertFailure)
import Test.Tasty (TestTree)
import Test.Tasty.HUnit (testCase)

import Lorentz
import Morley.Michelson.Typed.Scope
import Morley.Util.Type
import Morley.Util.TypeLits

-- | Bind on 'Either's that return nothing.
type SumEithers :: Either l () -> Either l () -> Either l r
type family SumEithers e1 e2 where
  SumEithers ('Right '()) e = e
  SumEithers ('Left err) _ = 'Left err

-- | Check that the given generic subtree /corresponding to a product part/
-- contains only elements of given dupability (all dupable or all non-dupable).
type family GCheckDupability (expectedDupability :: Bool) (x :: Type -> Type)
    :: Either (Bool, Maybe Symbol, Type) () where
  GCheckDupability dup (x G.:*: y) =
    GCheckDupability dup x `SumEithers` GCheckDupability dup y
  GCheckDupability dup (G.S1 ('G.MetaSel mname _ _ _) (G.Rec0 a)) =
    If (IsDupableScope (ToT a) == dup)
      ('Right '())
      ('Left '(dup, mname, a))

-- | A "generics" helper for 'CheckDupablesDistribution'.
type family GCheckDupablesDistribution (x :: Type -> Type) where
  GCheckDupablesDistribution (G.D1 _ (G.C1 _ (l G.:*: r))) =
    GCheckDupability 'True l `SumEithers` GCheckDupability 'False r
  GCheckDupablesDistribution _ =
    TypeError ('Text "This works only on product types")

-- | For the given type, check that at the left subtree of pairs tree it
-- contains only dupable elements, and at the right - only non-dupable ones.
type family CheckDupablesDistribution (a :: Type) :: Either (Bool, Maybe Symbol, Type) () where
  CheckDupablesDistribution a = GCheckDupablesDistribution (G.Rep a)

-- | Error for 'checkDupablesDistribution'.
data BadElement = BadElement
  { beExpectedDupability :: Bool
  , beRecName :: Maybe Text
  , beRecType :: TypeRep
  } deriving stock (Show, Eq)

instance Buildable BadElement where
  build (BadElement expectedDupable recName recType) =
    "Expected " <> if expectedDupable then "dupable" else "non-dupable" <> "element \
    \in record field " +| (recName ?: "<no info>") |+ " of type " +| show @Text recType |+ ""

class DemoteRes (res :: Either (Bool, Maybe Symbol, Type) ()) where
  demoteRes :: Either BadElement ()
instance DemoteRes ('Right '()) where
  demoteRes = Right ()
instance (SingI dup, SingI mname, Typeable ty) => DemoteRes ('Left '(dup, mname, ty)) where
  demoteRes = Left BadElement
    { beExpectedDupability = demote @dup
    , beRecName = demote @mname
    , beRecType = typeRep (Proxy @ty)
    }

-- | 'CheckDupablesDistribution' for term-level.
checkDupablesDistribution
  :: forall a. (DemoteRes (CheckDupablesDistribution a))
  => Either BadElement ()
checkDupablesDistribution = demoteRes @(CheckDupablesDistribution a)

-- | A term-level version of 'VerifyDupablesDistribution' for tests.
testDupablesDistribution
  :: forall a. (Typeable a, DemoteRes (CheckDupablesDistribution a))
  => TestTree
testDupablesDistribution =
  testCase ("Dupables distribution for " <> show (typeRep $ Proxy @a)) $
    case checkDupablesDistribution @a of
      Right () -> pass
      Left err -> assertFailure $ "Bad dupables distribution: " <> pretty err

type family ResToConstraint (res :: Either (Bool, Maybe Symbol, Type) ()) :: Constraint where
  ResToConstraint ('Right '()) = ()
  ResToConstraint ('Left '(expectedDup, recName, recType)) =
    TypeError
      ( 'Text "Expected " ':<>: 'Text (DupableDesc expectedDup) ':<>: 'Text " element" ':$$:
        'Text "in record field " ':<>: 'ShowType (GetMaybeName recName)
          ':<>: 'Text " of type " ':<>: 'ShowType recType
      )

type family DupableDesc (dup :: Bool) :: Symbol where
  DupableDesc 'True = "dupable"
  DupableDesc 'False = "non-dupable"

type family GetMaybeName (mname :: Maybe Symbol) :: Symbol where
  GetMaybeName ('Just name) = name
  GetMaybeName 'Nothing = "<no info>"

-- | A constraint that, for the given type, checks that at the left subtree
-- of pairs tree it contains only dupable elements, and at the right - only
-- non-dupable ones.
type VerifyDupablesDistribution a =
  ResToConstraint (CheckDupablesDistribution a)