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

-- | Type-level field description validators
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)

-- | Description of constructors and fields of some datatype.
--
-- This type is just two nested maps represented as associative lists. It is supposed to
-- be interpreted like this:
--
-- > [(Constructor name, (Maybe constructor description, [(Field name, Field description)]))]
--
-- Example with a concrete data type:
--
-- > data Foo
-- >   = Foo
-- >       { fFoo :: Int
-- >       }
-- >   | Bar
-- >       { fBar :: Text
-- >       }
-- >   deriving (Generic)
-- >
-- > type FooDescriptions =
-- >   '[ '( "Foo", '( 'Just "foo constructor",
-- >       , '[ '("fFoo", "some number")
-- >          ])
-- >       )
-- >    , '( "Bar", '( 'Nothing,
-- >       , '[ '("fBar", "some string")
-- >          ])
-- >       )
-- >    ]
type FieldDescriptions = [(Symbol, (Maybe Symbol, [(Symbol, Symbol)]))]

-- | Value-level counterpart to 'FieldDescriptions'.
type FieldDescriptionsV = Demote FieldDescriptions

{- | This type family checks that field descriptions mention only existing constructors and fields.

When @descr@ is empty this family does nothing, to avoid breaking for built-in, non-ADT types.

When @descr@ is not empty, this family will demand 'G.Generic' instance for @typ@ and fail with a
@TypeError@ if there none.

>>> data Foo = Foo { fooField :: () } -- no Generic instance
>>> () :: FieldDescriptionsValid '[ '("Foo", '(Nothing, '[ '("fooField", "")]))] Foo => ()
...
... No Generic instance for Foo.
... Generic is needed to validate TypeDocFieldDescriptions.
...
>>> data Foo = Foo { fooField :: () } deriving Generic
>>> () :: FieldDescriptionsValid '[ '("Foo", '(Nothing, '[ '("fooField", "")]))] Foo => ()
()
-}
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))

-- Note: This module doesn't use 'Morley.Util.Generic.GRep' because it's already guarded.

-- | Actual recursive implementation for 'FieldDescriptionsValid'.
type FieldDescriptionsValidImpl :: FieldDescriptions -> Type -> Constraint
type family FieldDescriptionsValidImpl descr typ where
  FieldDescriptionsValidImpl '[] _ = ()
  FieldDescriptionsValidImpl ( '(conName, '(_, fields)) ': rest ) typ =
    ( HasAllFields conName fields typ
    , FieldDescriptionsValidImpl rest typ
    )

-- | Check whether given constructor name @conName@ is present in 'G.Rep' of a datatype.
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

-- | Check whether all fields described for given constructor @conName@ are present in the datatype.
--
-- This family also checks whether the constructor is present and fails with a @TypeError@
-- otherwise.
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)

-- | Actual recursive implementation of 'HasAllFields'.
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
    )

-- | Check that Generic 'G.Rep' has given field @fieldName@ in a given constructor @conName@.
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

-- | Check that Generic representation for a constructor has given field @fieldName@.
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