module Morley.Michelson.Typed.Haskell.ValidateDescription
( FieldDescriptions
, FieldDescriptionsV
, FieldDescriptionsValid
) where
import Data.Singletons (Demote)
import Data.Type.Bool (type (||))
import Fcf qualified
import GHC.Generics qualified as G
import GHC.TypeLits (ErrorMessage(..), Symbol)
import Type.Errors (DelayError, IfStuck)
import Morley.Util.Type (FailUnless, FailUnlessElse)
type FieldDescriptions = [(Symbol, (Maybe Symbol, [(Symbol, Symbol)]))]
type FieldDescriptionsV = Demote FieldDescriptions
type FieldDescriptionsValid :: FieldDescriptions -> Type -> Constraint
type family FieldDescriptionsValid descr typ where
FieldDescriptionsValid '[] _ = ()
FieldDescriptionsValid descr typ =
IfStuck (G.Rep typ)
(DelayError
('Text "No Generic instance for " ':<>: 'ShowType typ ':<>: 'Text "." ':$$:
'Text "Generic is needed to validate TypeDocFieldDescriptions.")
)
(Fcf.Pure (FieldDescriptionsValidImpl descr typ))
type FieldDescriptionsValidImpl :: FieldDescriptions -> Type -> Constraint
type family FieldDescriptionsValidImpl descr typ where
FieldDescriptionsValidImpl '[] _ = ()
FieldDescriptionsValidImpl ( '(conName, '(_, fields)) ': rest ) typ =
( HasAllFields conName fields typ
, FieldDescriptionsValidImpl rest typ
)
type HasConstructor :: Symbol -> (Type -> Type) -> Bool
type family HasConstructor conName g where
HasConstructor conName (G.D1 _ cs) = HasConstructor conName cs
HasConstructor conName (G.C1 ('G.MetaCons conName _ _) _) = 'True
HasConstructor conName (l G.:+: r) = HasConstructor conName l || HasConstructor conName r
HasConstructor _ _ = 'False
type HasAllFields :: Symbol -> [(Symbol, Symbol)] -> Type -> Constraint
type family HasAllFields conName fields typ where
HasAllFields conName fields typ =
FailUnlessElse
(HasConstructor conName (G.Rep typ))
('Text "No constructor " ':<>: 'ShowType conName ':<>:
'Text " in type " ':<>: 'ShowType typ ':<>: 'Text "."
)
(HasAllFieldsImpl conName fields typ)
type HasAllFieldsImpl :: Symbol -> [(Symbol, Symbol)] -> Type -> Constraint
type family HasAllFieldsImpl conName fields typ where
HasAllFieldsImpl _ '[] _ = ()
HasAllFieldsImpl conName ( '(fieldName, _) ': rest ) typ =
( FailUnless
(HasField conName fieldName (G.Rep typ))
('Text "No field " ':<>: 'ShowType fieldName ':<>: 'Text " in constructor " ':<>:
'ShowType conName ':<>: 'Text " of type " ':<>: 'ShowType typ ':<>: 'Text "."
)
, HasAllFieldsImpl conName rest typ
)
type HasField :: Symbol -> Symbol -> (Type -> Type) -> Bool
type family HasField conName fieldName g where
HasField conName fieldName (G.D1 _ cs) = HasField conName fieldName cs
HasField conName fieldName (G.C1 ('G.MetaCons conName _ _) c) = ConHasField fieldName c
HasField conName fieldName (l G.:+: r) = HasField conName fieldName l || HasField conName fieldName r
HasField _ _ _ = 'False
type ConHasField :: Symbol -> (Type -> Type) -> Bool
type family ConHasField fieldName g where
ConHasField fieldName (G.S1 ('G.MetaSel ('Just fieldName) _ _ _) _) = 'True
ConHasField fieldName (l G.:*: r) = ConHasField fieldName l || ConHasField fieldName r
ConHasField _ _ = 'False