-- 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
  { BadElement -> Bool
beExpectedDupability :: Bool
  , BadElement -> Maybe Text
beRecName :: Maybe Text
  , BadElement -> TypeRep
beRecType :: TypeRep
  } deriving stock (Int -> BadElement -> ShowS
[BadElement] -> ShowS
BadElement -> String
(Int -> BadElement -> ShowS)
-> (BadElement -> String)
-> ([BadElement] -> ShowS)
-> Show BadElement
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BadElement] -> ShowS
$cshowList :: [BadElement] -> ShowS
show :: BadElement -> String
$cshow :: BadElement -> String
showsPrec :: Int -> BadElement -> ShowS
$cshowsPrec :: Int -> BadElement -> ShowS
Show, BadElement -> BadElement -> Bool
(BadElement -> BadElement -> Bool)
-> (BadElement -> BadElement -> Bool) -> Eq BadElement
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BadElement -> BadElement -> Bool
$c/= :: BadElement -> BadElement -> Bool
== :: BadElement -> BadElement -> Bool
$c== :: BadElement -> BadElement -> Bool
Eq)

instance Buildable BadElement where
  build :: BadElement -> Builder
build (BadElement Bool
expectedDupable Maybe Text
recName TypeRep
recType) =
    Builder
"Expected " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> if Bool
expectedDupable then Builder
"dupable" else Builder
"non-dupable" Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
"element \
    \in record field " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| (Maybe Text
recName Maybe Text -> Text -> Text
forall a. Maybe a -> a -> a
?: Text
"<no info>") Text -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
" of type " Builder -> Builder -> Builder
forall b. FromBuilder b => Builder -> Builder -> b
+| forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show @Text TypeRep
recType Text -> Builder -> Builder
forall a b. (Buildable a, FromBuilder b) => a -> Builder -> b
|+ Builder
""

class DemoteRes (res :: Either (Bool, Maybe Symbol, Type) ()) where
  demoteRes :: Either BadElement ()
instance DemoteRes ('Right '()) where
  demoteRes :: Either BadElement ()
demoteRes = () -> Either BadElement ()
forall a b. b -> Either a b
Right ()
instance (SingI dup, SingI mname, Typeable ty) => DemoteRes ('Left '(dup, mname, ty)) where
  demoteRes :: Either BadElement ()
demoteRes = BadElement -> Either BadElement ()
forall a b. a -> Either a b
Left BadElement :: Bool -> Maybe Text -> TypeRep -> BadElement
BadElement
    { beExpectedDupability :: Bool
beExpectedDupability = forall (a :: Bool). (SingKind Bool, SingI a) => Demote Bool
forall {k} (a :: k). (SingKind k, SingI a) => Demote k
demote @dup
    , beRecName :: Maybe Text
beRecName = forall (a :: Maybe Symbol).
(SingKind (Maybe Symbol), SingI a) =>
Demote (Maybe Symbol)
forall {k} (a :: k). (SingKind k, SingI a) => Demote k
demote @mname
    , beRecType :: TypeRep
beRecType = Proxy ty -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @ty)
    }

-- | 'CheckDupablesDistribution' for term-level.
checkDupablesDistribution
  :: forall a. (DemoteRes (CheckDupablesDistribution a))
  => Either BadElement ()
checkDupablesDistribution :: forall a.
DemoteRes (CheckDupablesDistribution a) =>
Either BadElement ()
checkDupablesDistribution = forall (res :: Either (Bool, Maybe Symbol, *) ()).
DemoteRes res =>
Either BadElement ()
demoteRes @(CheckDupablesDistribution a)

-- | A term-level version of 'VerifyDupablesDistribution' for tests.
testDupablesDistribution
  :: forall a. (Typeable a, DemoteRes (CheckDupablesDistribution a))
  => TestTree
testDupablesDistribution :: forall a.
(Typeable a, DemoteRes (CheckDupablesDistribution a)) =>
TestTree
testDupablesDistribution =
  String -> Assertion -> TestTree
testCase (String
"Dupables distribution for " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> TypeRep -> String
forall b a. (PrettyShow a, Show a, IsString b) => a -> b
show (Proxy a -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep (Proxy a -> TypeRep) -> Proxy a -> TypeRep
forall a b. (a -> b) -> a -> b
$ forall {t}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @a)) (Assertion -> TestTree) -> Assertion -> TestTree
forall a b. (a -> b) -> a -> b
$
    case forall a.
DemoteRes (CheckDupablesDistribution a) =>
Either BadElement ()
checkDupablesDistribution @a of
      Right () -> Assertion
forall (f :: * -> *). Applicative f => f ()
pass
      Left BadElement
err -> String -> Assertion
forall a. HasCallStack => String -> IO a
assertFailure (String -> Assertion) -> String -> Assertion
forall a b. (a -> b) -> a -> b
$ String
"Bad dupables distribution: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> BadElement -> String
forall a b. (Buildable a, FromBuilder b) => a -> b
pretty BadElement
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)