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
type SumEithers :: Either l () -> Either l () -> Either l r
type family SumEithers e1 e2 where
SumEithers ('Right '()) e = e
SumEithers ('Left err) _ = 'Left err
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))
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")
type family CheckDupablesDistribution (a :: Type) :: Either (Bool, Maybe Symbol, Type) () where
CheckDupablesDistribution a = GCheckDupablesDistribution (G.Rep a)
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
:: 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)
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>"
type VerifyDupablesDistribution a =
ResToConstraint (CheckDupablesDistribution a)