-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

module Michelson.Typed.Haskell.ValidateDescription
  ( FieldDescriptions
  , FieldDescriptionsV

  , FieldDescriptionsValid
  ) where

import qualified Data.Kind as Kind
import Data.Singletons (Demote)
import Data.Type.Bool
import qualified GHC.Generics as G
import GHC.TypeLits

-- | 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.
type family FieldDescriptionsValid (descr :: FieldDescriptions) (typ :: Kind.Type) :: Kind.Constraint where
  FieldDescriptionsValid '[] _ = ()
  FieldDescriptionsValid descr typ =
    Assert
      (TypeError
        ('Text "No Generic instance for " ':<>: 'ShowType typ ':<>: 'Text "." ':$$:
         'Text "Generic is needed to validate TypeDocFieldDescriptions.")
      )
      (G.Rep typ)
      (FieldDescriptionsValidImpl descr typ)

-- | Actual recursive implementation for 'FieldDescriptionsValid'.
type family FieldDescriptionsValidImpl (descr :: FieldDescriptions) (typ :: Kind.Type) :: Kind.Constraint 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 family HasConstructor (conName :: Symbol) (g :: Kind.Type -> Kind.Type) :: Bool 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 family HasAllFields (conName :: Symbol) (fields :: [(Symbol, Symbol)]) (typ :: Kind.Type) :: Kind.Constraint where
  HasAllFields conName fields typ =
    If
      (HasConstructor conName (G.Rep typ))
      (HasAllFieldsImpl conName fields typ)
      (TypeError
        ('Text "No constructor " ':<>: 'ShowType conName ':<>: 'Text " in type " ':<>: 'ShowType typ ':<>: 'Text "." )
      )

-- | Actual recursive implementation of 'HasAllFields'.
type family HasAllFieldsImpl (conName :: Symbol) (fields :: [(Symbol, Symbol)]) (typ :: Kind.Type) :: Kind.Constraint where
  HasAllFieldsImpl _ '[] _ = ()
  HasAllFieldsImpl conName ( '(fieldName, _) ': rest ) typ =
    ( If
        (HasField conName fieldName (G.Rep typ))
        (() :: Kind.Constraint)
        (TypeError
          ('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 family HasField (conName :: Symbol) (fieldName :: Symbol) (g :: Kind.Type -> Kind.Type) :: Bool 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 family ConHasField (fieldName :: Symbol) (g :: Kind.Type -> Kind.Type) :: Bool where
  ConHasField fieldName (G.S1 ('G.MetaSel ('Just fieldName) _ _ _) _) = 'True
  ConHasField fieldName (l G.:*: r) = ConHasField fieldName l || ConHasField fieldName r
  ConHasField _ _ = 'False

-- A trick by Csongor Kiss: https://kcsongor.github.io/report-stuck-families/
--
-- 'T1' is a dummy type and 'Assert' will get stuck whenever its argument @break@ is stuck.
--
-- This happens because for stuck argument GHC can't check whether it is equal to 'T1' and therefore
-- can't select one of 'Assert's equations.

data T1 a

type family Assert (err :: Constraint) (break :: Kind.Type -> Kind.Type) (v :: k) :: k where
  Assert _ T1 _ = Any
  Assert _ _ k = k