{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}

module Symantic.Semantics.ToFer where

import Control.Monad (Monad, (>=>))
import Data.Function qualified as Fun
import Data.Functor (Functor, (<$>))
import GHC.Generics (Generic)

import Symantic.Syntaxes.Classes
import Symantic.Syntaxes.EithersOfTuples
import Symantic.Syntaxes.TuplesOfFunctions

-- * Type 'TuplesOfFunctions'

-- | The 'ToFer' intermediate interpreter
-- return Tuples-of-Functions instead of Eithers-of-Tuples.
--
-- In other words, it transforms 'SumFunctor' into functions returning @(sem next)@
-- and 'ProductFunctor' into arguments of those functions.
--
-- This is like using an extension parameter introduced in
-- https://okmij.org/ftp/typed-formatting/index.html#DSL-FIn
-- but here only a single type parameter @(a)@ is exposed
-- instead of two.
--
-- Useful to avoid declaring and pattern-matching
-- an algebraic datatype of type @(a)@,
-- as the corresponding function will be called directly,
-- given as arguments the terms that would have been
-- pattern-matched from a constructor
-- of such algebraic datatype.
data ToFer sem a = ToFer
  { tuplesOfFunctions :: forall next. ToF a next -> sem next
  , eithersOfTuples :: sem a
  }

instance (ProductFunctor sem, Monad sem) => ProductFunctor (ToFer sem) where
  a <.> b =
    ToFer
      { tuplesOfFunctions = tuplesOfFunctions a >=> tuplesOfFunctions b
      , eithersOfTuples = eithersOfTuples a <.> eithersOfTuples b
      }
  a .> b =
    ToFer
      { tuplesOfFunctions = tuplesOfFunctions a >=> tuplesOfFunctions b
      , eithersOfTuples = eithersOfTuples a .> eithersOfTuples b
      }
  a <. b =
    ToFer
      { tuplesOfFunctions = tuplesOfFunctions a >=> tuplesOfFunctions b
      , eithersOfTuples = eithersOfTuples a <. eithersOfTuples b
      }
instance (SumFunctor sem, AlternativeFunctor sem) => SumFunctor (ToFer sem) where
  a <+> b =
    ToFer
      { tuplesOfFunctions = \(l, r) -> tuplesOfFunctions a l <|> tuplesOfFunctions b r
      , eithersOfTuples = eithersOfTuples a <+> eithersOfTuples b
      }
instance (Optionable sem, Functor sem) => Optionable (ToFer sem) where
  optional ma = ToFer{tuplesOfFunctions = (<$> sem), eithersOfTuples = sem}
    where
      sem = optional (eithersOfTuples ma)
instance Functor sem => Dataable (ToFer sem) where
  data_ ::
    forall a.
    Generic a =>
    RepOfEoT a =>
    UnToF a =>
    ToFer sem (EoT (ADT a)) ->
    ToFer sem a
  data_ a =
    ToFer
      { tuplesOfFunctions = \f -> unToF @(IsToF a) @a f Fun.. adtOfeot <$> eithersOfTuples a
      , eithersOfTuples = adtOfeot <$> eithersOfTuples a
      }