{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE UndecidableInstances #-}

-- | EOT (Either of Tuples) to/from ADT (Algebraic Data Type).
-- to produce or consume custom ADT with @('<:>')@ and @('<+>')@.
--
-- This is like what is done in @generic-sop@:
-- https://hackage.haskell.org/package/generics-sop-0.5.1.0/docs/src/Generics.SOP.GGP.html#gSumFrom
-- but using directly 'Either' and 'Tuples'
-- instead of passing by the intermediary GADTs @NP@ and @NS@.
module Symantic.Syntaxes.ADT where

import Data.Either (Either (..))
import Data.Function (const, id, ($), (.))
import Data.Kind (Type)
import Data.Void (Void, absurd)
import GHC.Generics as Generics

-- * Type family 'EoT'

-- Return an 'Either' of 'Tuples' from the given 'ADT',
-- matching the nesting occuring when using @('<:>')@ and ('<+>')@
-- and their associativity and precedence,
-- with no parenthesis messing around.
type family EoT (adt :: [[Type]]) :: Type where
-- This is 'absurd'
  EoT '[] = Void
-- There Is No Alternative
  EoT '[ps] = Tuples ps
-- The right associativity of @('<+>')@
-- puts leaves on 'Left' and nodes on 'Right'
  EoT (ps ': ss) = Either (Tuples ps) (EoT ss)

-- * Type family 'Tuples'

-- | Return the type of 'snd'-nested 2-tuples
-- from the given list of types.
type family Tuples (as :: [Type]) :: (r :: Type) where
  Tuples '[] = ()
  Tuples '[a] = a
  Tuples (a ': rest) = (a, Tuples rest)

-- * Type 'ADT'

-- | Normalized type-level representation of an Algebraic Data Type.
type ADT (adt :: Type) = ListOfRepSums (Rep adt) '[]

-- ** Type family 'ListOfRepSums'

-- | Collect the alternatives in a continuation passing-style.
type family ListOfRepSums (a :: Type -> Type) (ss :: [[Type]]) :: [[Type]]

type instance ListOfRepSums (a :+: b) ss = ListOfRepSums a (ListOfRepSums b ss)

-- | Meta-information for datatypes
type instance ListOfRepSums (M1 D _c a) ss = ListOfRepSums a ss

-- | Meta-information for constructors
type instance ListOfRepSums (M1 C _c a) ss = ListOfRepProducts a '[] ': ss

-- | Empty datatypes
type instance ListOfRepSums V1 ss = ss

-- ** Type family 'ListOfRepProducts'

-- | Collect the records in a continuation passing-style.
type family ListOfRepProducts (a :: Type -> Type) (ps :: [Type]) :: [Type]

type instance ListOfRepProducts (a :*: b) ps = ListOfRepProducts a (ListOfRepProducts b ps)

-- | Meta-information for record selectors
type instance ListOfRepProducts (M1 S _c a) ps = TypeOfRepField a ': ps

-- | Constructor without fields
type instance ListOfRepProducts U1 ps = ps

-- ** Type family 'TypeOfRepField'
type family TypeOfRepField (a :: Type -> Type) :: Type
type instance TypeOfRepField (K1 _i a) = a

-- * Class 'RepOfEoT'
type RepOfEoT a = RepOfEithers (Rep a) '[]

-- | Morph the 'Either' of 'Tuples' corresponding to an 'ADT'
-- into a constructor of this 'ADT'.
-- This is the reverse of 'eotOfadt'.
adtOfeot :: Generic a => RepOfEoT a => EoT (ADT a) -> a
adtOfeot eot = Generics.to $ repOfEithers @_ @'[] eot id absurd

-- ** Class 'RepOfEithers'
class RepOfEithers (a :: Type -> Type) ss where
  -- | Parse the 'Either' (list-like) binary tree of 'EoT'
  -- into the @(':+:')@ (balanced) binary tree of 'Rep',
  -- using continuation passing-style for performance.
  repOfEithers ::
    EoT (ListOfRepSums a ss) ->
    -- the 'a' 'Rep' is the current alternative in the 'EoT'
    (a x -> r) ->
    -- the 'a' 'Rep' is a following alternative in the 'EoT'
    (EoT ss -> r) ->
    r
instance (RepOfEithers a (ListOfRepSums b ss), RepOfEithers b ss) => RepOfEithers (a :+: b) ss where
  repOfEithers eot ok ko =
    -- try to parse 'a' on the current 'eot'
    repOfEithers @a @(ListOfRepSums b ss)
      eot
      (ok . L1)
      ( \next ->
          -- parsing 'a' failed
          -- try to parse 'b' on the 'Right' of the current 'eot'
          repOfEithers @b @ss
            next
            (ok . R1)
            ko -- parsing 'b' failed: backtrack
      )
instance RepOfEithers a ss => RepOfEithers (M1 D c a) ss where
  repOfEithers eot ok = repOfEithers @a @ss eot (ok . M1)
instance RepOfTuples a '[] => RepOfEithers (M1 C c a) (ps ': ss) where
  repOfEithers eot ok ko =
    case eot of
      -- 'EoT' is a leaf, and 'Rep' too: parsing succeeds
      Left ts -> ok $ M1 $ repOfTuples @a @'[] ts const
      -- 'EoT' is a node, but 'Rep' is a leaf: parsing fails
      Right ss -> ko ss
instance RepOfTuples a '[] => RepOfEithers (M1 C c a) '[] where
  repOfEithers eot ok _ko = ok $ M1 $ repOfTuples @_ @'[] eot const
instance RepOfEithers V1 ss where
  repOfEithers eot _ok ko = ko eot

-- ** Class 'RepOfTuples'
class RepOfTuples (a :: Type -> Type) (xs :: [Type]) where
  -- | Parse the 'Tuples' (list-like) binary tree of 'EoT'
  -- into the @(':*:')@ (balanced) binary tree of 'Rep',
  -- using continuation passing-style for performance.
  repOfTuples ::
    Tuples (ListOfRepProducts a xs) ->
    (a x -> Tuples xs -> r) ->
    r
instance (RepOfTuples a (ListOfRepProducts b ps), RepOfTuples b ps) => RepOfTuples (a :*: b) ps where
  repOfTuples ts k =
    -- uncons 'a'
    repOfTuples @a @(ListOfRepProducts b ps)
      ts
      ( \a ts' ->
          -- uncons 'b'
          repOfTuples @b @ps
            ts'
            (\b -> k (a :*: b))
      )
instance RepOfField a => RepOfTuples (M1 S c a) (p ': ps) where
  repOfTuples (a, ts) k = k (M1 (repOfField a)) ts
instance RepOfField a => RepOfTuples (M1 S c a) '[] where
  repOfTuples a k = k (M1 (repOfField a)) ()
instance RepOfTuples U1 ps where
  repOfTuples ts k = k U1 ts

-- ** Class 'RepOfField'
class RepOfField (a :: Type -> Type) where
  repOfField :: TypeOfRepField a -> a x
instance RepOfField (K1 i a) where
  repOfField = K1

-- * Class 'EoTOfRep'
type EoTOfRep a = EithersOfRep (Rep a) '[]

-- | Morph the constructor of an 'ADT'
-- into the corresponding 'Either' of 'Tuples' of this 'ADT'.
-- This is the reverse of 'adtOfeot'.
eotOfadt :: Generic a => EoTOfRep a => a -> EoT (ADT a)
eotOfadt = eithersOfRepL @_ @'[] . Generics.from

-- ** Class 'EithersOfRep'
class EithersOfRep (a :: Type -> Type) ss where
  eithersOfRepL :: a x -> EoT (ListOfRepSums a ss)
  eithersOfRepR :: EoT ss -> EoT (ListOfRepSums a ss)
instance
  (EithersOfRep a (ListOfRepSums b ss), EithersOfRep b ss) =>
  EithersOfRep (a :+: b) ss
  where
  eithersOfRepL = \case
    L1 a -> eithersOfRepL @a @(ListOfRepSums b ss) a
    R1 b -> eithersOfRepR @a @(ListOfRepSums b ss) (eithersOfRepL @b @ss b)
  eithersOfRepR ss = eithersOfRepR @a @(ListOfRepSums b ss) (eithersOfRepR @b @ss ss)
instance EithersOfRep a ss => EithersOfRep (M1 D c a) ss where
  eithersOfRepL (M1 a) = eithersOfRepL @a @ss a
  eithersOfRepR = eithersOfRepR @a @ss
instance TuplesOfRep a '[] => EithersOfRep (M1 C c a) '[] where
  eithersOfRepL (M1 a) = tuplesOfRep @_ @'[] a ()
  eithersOfRepR = absurd
instance TuplesOfRep a '[] => EithersOfRep (M1 C c a) (ps ': ss) where
  eithersOfRepL (M1 a) = Left $ tuplesOfRep @_ @'[] a ()
  eithersOfRepR = Right
instance EithersOfRep V1 ss where
  eithersOfRepL = \case {}
  eithersOfRepR = id

-- ** Class 'TuplesOfRep'
class TuplesOfRep (a :: Type -> Type) (ps :: [Type]) where
  tuplesOfRep :: a x -> Tuples ps -> Tuples (ListOfRepProducts a ps)
instance (TuplesOfRep a (ListOfRepProducts b ps), TuplesOfRep b ps) => TuplesOfRep (a :*: b) ps where
  tuplesOfRep (a :*: b) ps =
    tuplesOfRep @a @(ListOfRepProducts b ps)
      a
      (tuplesOfRep @b @ps b ps)
instance TuplesOfRep U1 ps where
  tuplesOfRep U1 xs = xs
instance FieldOfRep a => TuplesOfRep (M1 S c a) (x ': ps) where
  tuplesOfRep (M1 a) xs = (fieldOfRep a, xs)
instance FieldOfRep a => TuplesOfRep (M1 S c a) '[] where
  tuplesOfRep (M1 a) _xs = fieldOfRep a

-- ** Class 'FieldOfRep'
class FieldOfRep (a :: Type -> Type) where
  fieldOfRep :: a x -> TypeOfRepField a
instance FieldOfRep (K1 i a) where
  fieldOfRep (K1 a) = a