{-# 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, if 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
  { forall (sem :: * -> *) a.
ToFer sem a -> forall next. ToF a next -> sem next
tuplesOfFunctions :: forall next. ToF a next -> sem next
  , forall (sem :: * -> *) a. ToFer sem a -> sem a
eithersOfTuples :: sem a
  }

instance (ProductFunctor sem, Monad sem) => ProductFunctor (ToFer sem) where
  ToFer sem a
a <.> :: forall a b. ToFer sem a -> ToFer sem b -> ToFer sem (a, b)
<.> ToFer sem b
b =
    ToFer :: forall (sem :: * -> *) a.
(forall next. ToF a next -> sem next) -> sem a -> ToFer sem a
ToFer
      { tuplesOfFunctions :: forall next. ToF (a, b) next -> sem next
tuplesOfFunctions = ToFer sem a -> forall next. ToF a next -> sem next
forall (sem :: * -> *) a.
ToFer sem a -> forall next. ToF a next -> sem next
tuplesOfFunctions ToFer sem a
a (ToF a (ToFIf (IsToF b) b next) -> sem (ToFIf (IsToF b) b next))
-> (ToFIf (IsToF b) b next -> sem next)
-> ToF a (ToFIf (IsToF b) b next)
-> sem next
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> ToFer sem b -> forall next. ToF b next -> sem next
forall (sem :: * -> *) a.
ToFer sem a -> forall next. ToF a next -> sem next
tuplesOfFunctions ToFer sem b
b
      , eithersOfTuples :: sem (a, b)
eithersOfTuples = ToFer sem a -> sem a
forall (sem :: * -> *) a. ToFer sem a -> sem a
eithersOfTuples ToFer sem a
a sem a -> sem b -> sem (a, b)
forall (sem :: * -> *) a b.
ProductFunctor sem =>
sem a -> sem b -> sem (a, b)
<.> ToFer sem b -> sem b
forall (sem :: * -> *) a. ToFer sem a -> sem a
eithersOfTuples ToFer sem b
b
      }
  ToFer sem ()
a .> :: forall a. ToFer sem () -> ToFer sem a -> ToFer sem a
.> ToFer sem a
b =
    ToFer :: forall (sem :: * -> *) a.
(forall next. ToF a next -> sem next) -> sem a -> ToFer sem a
ToFer
      { tuplesOfFunctions :: forall next. ToF a next -> sem next
tuplesOfFunctions = ToFer sem () -> forall next. ToF () next -> sem next
forall (sem :: * -> *) a.
ToFer sem a -> forall next. ToF a next -> sem next
tuplesOfFunctions ToFer sem ()
a (ToFIf (IsToF a) a next -> sem (ToFIf (IsToF a) a next))
-> (ToFIf (IsToF a) a next -> sem next)
-> ToFIf (IsToF a) a next
-> sem next
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> ToFer sem a -> forall next. ToF a next -> sem next
forall (sem :: * -> *) a.
ToFer sem a -> forall next. ToF a next -> sem next
tuplesOfFunctions ToFer sem a
b
      , eithersOfTuples :: sem a
eithersOfTuples = ToFer sem () -> sem ()
forall (sem :: * -> *) a. ToFer sem a -> sem a
eithersOfTuples ToFer sem ()
a sem () -> sem a -> sem a
forall (sem :: * -> *) a.
ProductFunctor sem =>
sem () -> sem a -> sem a
.> ToFer sem a -> sem a
forall (sem :: * -> *) a. ToFer sem a -> sem a
eithersOfTuples ToFer sem a
b
      }
  ToFer sem a
a <. :: forall a. ToFer sem a -> ToFer sem () -> ToFer sem a
<. ToFer sem ()
b =
    ToFer :: forall (sem :: * -> *) a.
(forall next. ToF a next -> sem next) -> sem a -> ToFer sem a
ToFer
      { tuplesOfFunctions :: forall next. ToF a next -> sem next
tuplesOfFunctions = ToFer sem a -> forall next. ToF a next -> sem next
forall (sem :: * -> *) a.
ToFer sem a -> forall next. ToF a next -> sem next
tuplesOfFunctions ToFer sem a
a (ToF a next -> sem next)
-> (next -> sem next) -> ToF a next -> sem next
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> ToFer sem () -> forall next. ToF () next -> sem next
forall (sem :: * -> *) a.
ToFer sem a -> forall next. ToF a next -> sem next
tuplesOfFunctions ToFer sem ()
b
      , eithersOfTuples :: sem a
eithersOfTuples = ToFer sem a -> sem a
forall (sem :: * -> *) a. ToFer sem a -> sem a
eithersOfTuples ToFer sem a
a sem a -> sem () -> sem a
forall (sem :: * -> *) a.
ProductFunctor sem =>
sem a -> sem () -> sem a
<. ToFer sem () -> sem ()
forall (sem :: * -> *) a. ToFer sem a -> sem a
eithersOfTuples ToFer sem ()
b
      }
instance (SumFunctor sem, AlternativeFunctor sem) => SumFunctor (ToFer sem) where
  ToFer sem a
a <+> :: forall a b. ToFer sem a -> ToFer sem b -> ToFer sem (Either a b)
<+> ToFer sem b
b =
    ToFer :: forall (sem :: * -> *) a.
(forall next. ToF a next -> sem next) -> sem a -> ToFer sem a
ToFer
      { tuplesOfFunctions :: forall next. ToF (Either a b) next -> sem next
tuplesOfFunctions = \(ToFIf (IsToF a) a next
l, ToFIf (IsToF b) b next
r) -> ToFer sem a -> forall next. ToF a next -> sem next
forall (sem :: * -> *) a.
ToFer sem a -> forall next. ToF a next -> sem next
tuplesOfFunctions ToFer sem a
a ToFIf (IsToF a) a next
l sem next -> sem next -> sem next
forall (sem :: * -> *) a.
AlternativeFunctor sem =>
sem a -> sem a -> sem a
<|> ToFer sem b -> forall next. ToF b next -> sem next
forall (sem :: * -> *) a.
ToFer sem a -> forall next. ToF a next -> sem next
tuplesOfFunctions ToFer sem b
b ToFIf (IsToF b) b next
r
      , eithersOfTuples :: sem (Either a b)
eithersOfTuples = ToFer sem a -> sem a
forall (sem :: * -> *) a. ToFer sem a -> sem a
eithersOfTuples ToFer sem a
a sem a -> sem b -> sem (Either a b)
forall (sem :: * -> *) a b.
SumFunctor sem =>
sem a -> sem b -> sem (Either a b)
<+> ToFer sem b -> sem b
forall (sem :: * -> *) a. ToFer sem a -> sem a
eithersOfTuples ToFer sem b
b
      }
instance (Optionable sem, Functor sem) => Optionable (ToFer sem) where
  optional :: forall a. ToFer sem a -> ToFer sem (Maybe a)
optional ToFer sem a
ma = ToFer :: forall (sem :: * -> *) a.
(forall next. ToF a next -> sem next) -> sem a -> ToFer sem a
ToFer{tuplesOfFunctions :: forall next. ToF (Maybe a) next -> sem next
tuplesOfFunctions = ((Maybe a -> next) -> sem (Maybe a) -> sem next
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> sem (Maybe a)
sem), eithersOfTuples :: sem (Maybe a)
eithersOfTuples = sem (Maybe a)
sem}
    where
      sem :: sem (Maybe a)
sem = sem a -> sem (Maybe a)
forall (sem :: * -> *) a. Optionable sem => sem a -> sem (Maybe a)
optional (ToFer sem a -> sem a
forall (sem :: * -> *) a. ToFer sem a -> sem a
eithersOfTuples ToFer sem a
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_ :: forall a.
(Generic a, RepOfEoT a, UnToF a) =>
ToFer sem (EoT (ADT a)) -> ToFer sem a
data_ ToFer sem (EoT (ADT a))
a =
    ToFer :: forall (sem :: * -> *) a.
(forall next. ToF a next -> sem next) -> sem a -> ToFer sem a
ToFer
      { tuplesOfFunctions :: forall next. ToF a next -> sem next
tuplesOfFunctions = \ToF a next
f -> forall (t :: Bool) a next.
UnToFIf t a =>
ToFIf t a next -> a -> next
unToF @(IsToF a) @a ToF a next
f (a -> next) -> (EoT (ADT a) -> a) -> EoT (ADT a) -> next
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. EoT (ADT a) -> a
forall a. (Generic a, RepOfEoT a) => EoT (ADT a) -> a
adtOfeot (EoT (ADT a) -> next) -> sem (EoT (ADT a)) -> sem next
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ToFer sem (EoT (ADT a)) -> sem (EoT (ADT a))
forall (sem :: * -> *) a. ToFer sem a -> sem a
eithersOfTuples ToFer sem (EoT (ADT a))
a
      , eithersOfTuples :: sem a
eithersOfTuples = EoT (ADT a) -> a
forall a. (Generic a, RepOfEoT a) => EoT (ADT a) -> a
adtOfeot (EoT (ADT a) -> a) -> sem (EoT (ADT a)) -> sem a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ToFer sem (EoT (ADT a)) -> sem (EoT (ADT a))
forall (sem :: * -> *) a. ToFer sem a -> sem a
eithersOfTuples ToFer sem (EoT (ADT a))
a
      }