{-# LANGUAGE ConstraintKinds      #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}

{- |
  Type level functions to statically assess
  if a value can be built out of a Registry
-}
module Data.Registry.Solver where

import           Data.Kind
import           GHC.TypeLits

-- | Compute the list of input types for a function
type family Inputs f :: [Type] where
  Inputs (i -> o) = i ': Inputs o
  Inputs x = '[]

-- | Compute the output type for a function
type family Output f :: Type where
  Output (i -> o) = Output o
  Output x = x

-- | Compute if a constructor can be added to a registry
type family CanMake (a :: Type) (els :: [Type]) (target :: Type):: Constraint where
  CanMake a '[] t = TypeError (
    Text "The constructor for " :$$:
    Text "" :$$:
    (Text "  " :<>: ShowType (Output t)) :$$:
    Text "" :$$:
    Text "cannot be added to the registry because" :$$:
    Text "" :$$:
    (Text "  " :<>: ShowType (Output a)) :$$:
    Text "" :$$:
    Text " is not one of the registry outputs" :$$:
    Text "" :$$:
    (Text "The full constructor type for " :<>: ShowType (Output t) :<>: Text " is"):$$:
    Text "" :$$:
    ShowType t :$$:
    Text ""
    )
  CanMake a (a ': _els) _t = ()
  CanMake a (_b ': els) t = CanMake a els t

-- | Compute if each element of a list of types is contained in
-- another list
class IsSubset (ins :: [Type]) (out :: [Type]) (target :: Type)

instance IsSubset '[] out t
instance (CanMake a out t, IsSubset els out t) => IsSubset (a ': els) out t

-- | Compute if each element of a list of types
--   is the same as another in a different order
class IsSameSet (types1 :: [Type]) (types2 :: [Type])

instance (ts1 ~ Normalized types1, ts2 ~ Normalized types2, IsSubset ts1 ts2 (), IsSubset ts1 ts2 ()) => IsSameSet types1 types2

-- | Compute if a type is contained in a list of types
type family Contains (a :: Type) (els :: [Type]) :: Constraint where
  Contains a els = Contains1 a els els

-- | Compute if a type is contained in a list of types
type family Contains1 (a :: Type) (els :: [Type]) (target :: [Type]) :: Constraint where
  Contains1 a '[] target = TypeError ('ShowType a ':<>: Text " cannot be found in " ':<>: 'ShowType target)
  Contains1 a (a ': els) t = ()
  Contains1 a (b ': els) t = Contains1 a els t

-- | Shorthand type alias when many such constraints need to be added to a type signature
type (out :- a) = Contains a out

-- | From the list of all the input types and outputs types of a registry
--   Can we create all the output types?
class Solvable (ins :: [Type]) (out :: [Type])

instance (IsSubset ins out ()) => Solvable ins out

-- | Extracted from the typelevel-sets project and adapted for the Registry datatype
--   This union deduplicates elements only if they appear in contiguously
--   What we really want is typelevel sets but they are too slow for now
--   https://github.com/dorchard/type-level-sets/issues/17
type family (:++) (x :: [k]) (y :: [k]) :: [k] where
  '[]       :++ xs = xs
  (x ': xs) :++ ys = x ': (xs :++ ys)

-- | Return '[a] only if it is not already in the list of types
type family FindUnique (a :: Type) (as :: [Type]) :: [Type] where
  FindUnique a '[] = '[a]
  FindUnique a (a ': _rest) = '[]
  FindUnique a (_b ': rest) = FindUnique a rest

type family Normalized (as :: [Type]) :: [Type] where
  Normalized '[] = '[]
  Normalized '[a] = '[a]
  Normalized (a ': rest) = FindUnique a rest :++ Normalized rest