{-# LANGUAGE DataKinds #-} -- For ReprKind
{-# LANGUAGE PatternSynonyms #-} -- For (:!:)
{-# LANGUAGE TypeFamilyDependencies #-} -- For Permutation
{-# LANGUAGE UndecidableInstances #-} -- For Permutation
-- | Combinators in this module conflict with usual ones from the @Prelude@
-- hence they are meant to be imported either explicitely or qualified.
module Symantic.Classes where

import Data.Bool (Bool(..))
import Data.Char (Char)
import Data.Either (Either(..))
import Data.Eq (Eq)
import Data.Int (Int)
import Data.Kind (Type)
import Data.Maybe (Maybe(..), fromJust)
import Data.Proxy (Proxy(..))
import Data.Semigroup (Semigroup)
import Data.String (String)
import GHC.Generics (Generic)
import Numeric.Natural (Natural)
import qualified Control.Category as Cat
import qualified Data.Function as Fun
import qualified Data.Tuple as Tuple

import Symantic.Derive
import Symantic.ADT
import Symantic.CurryN

-- * Type 'Syntax'
type Syntax = Semantic -> Constraint

-- ** Type family 'Syntaxes'
-- | Merge several 'Syntax'es into a single one.
--
-- Useful in 'IfSemantic'.
type family Syntaxes (syns :: [Syntax]) (sem :: Semantic) :: Constraint where
  Syntaxes '[] sem = ()
  Syntaxes (syn ': syns) sem = (syn sem, Syntaxes syns sem)

-- * Type 'Semantic'
-- | The kind of @sem@(antics) throughout this library.
type Semantic = Type -> Type

-- * Class 'Abstractable'
class Abstractable sem where
  -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  lam :: (sem a -> sem b) -> sem (a->b)
  -- | Like 'lam' but whose argument must be used only once,
  -- hence safe to beta-reduce (inline) without duplicating work.
  lam1 :: (sem a -> sem b) -> sem (a->b)
  var :: sem a -> sem a
  -- | Application, aka. unabstract.
  (.@) :: sem (a->b) -> sem a -> sem b; infixl 9 .@
  lam f = liftDerived (lam (derive Fun.. f Fun.. liftDerived))
  lam1 f = liftDerived (lam1 (derive Fun.. f Fun.. liftDerived))
  var = liftDerived1 var
  (.@) = liftDerived2 (.@)
  default lam ::
    FromDerived Abstractable sem => Derivable sem =>
    (sem a -> sem b) -> sem (a->b)
  default lam1 ::
    FromDerived Abstractable sem => Derivable sem =>
    (sem a -> sem b) -> sem (a->b)
  default var ::
    FromDerived1 Abstractable sem =>
    sem a -> sem a
  default (.@) ::
    FromDerived2 Abstractable sem =>
    sem (a->b) -> sem a -> sem b

-- ** Class 'Functionable'
class Functionable sem where
  const :: sem (a -> b -> a)
  flip :: sem ((a -> b -> c) -> b -> a -> c)
  id :: sem (a->a)
  (.) :: sem ((b->c) -> (a->b) -> a -> c); infixr 9 .
  ($) :: sem ((a->b) -> a -> b); infixr 0 $
  const = liftDerived const
  flip = liftDerived flip
  id = liftDerived id
  (.) = liftDerived (.)
  ($) = liftDerived ($)
  default const ::
    FromDerived Functionable sem =>
    sem (a -> b -> a)
  default flip ::
    FromDerived Functionable sem =>
    sem ((a -> b -> c) -> b -> a -> c)
  default id ::
    FromDerived Functionable sem =>
    sem (a->a)
  default (.) ::
    FromDerived Functionable sem =>
    sem ((b->c) -> (a->b) -> a -> c)
  default ($) ::
    FromDerived Functionable sem =>
    sem ((a->b) -> a -> b)

-- * Class 'Anythingable'
class Anythingable sem where
  anything :: sem a -> sem a
  anything = Fun.id

-- * Class 'Bottomable'
class Bottomable sem where
  bottom :: sem a

-- * Class 'Constantable'
class Constantable c sem where
  constant :: c -> sem c
  constant = liftDerived Fun.. constant
  default constant ::
    FromDerived (Constantable c) sem =>
    c -> sem c

-- * Class 'Eitherable'
class Eitherable sem where
  left :: sem (l -> Either l r)
  right :: sem (r -> Either l r)
  left = liftDerived left
  right = liftDerived right
  default left ::
    FromDerived Eitherable sem =>
    sem (l -> Either l r)
  default right ::
    FromDerived Eitherable sem =>
    sem (r -> Either l r)

-- * Class 'Equalable'
class Equalable sem where
  equal :: Eq a => sem (a -> a -> Bool)
  equal = liftDerived equal
  default equal ::
    FromDerived Equalable sem =>
    Eq a => sem (a -> a -> Bool)

infix 4 `equal`, ==
(==) ::
  Abstractable sem => Equalable sem => Eq a =>
  sem a -> sem a -> sem Bool
(==) x y = equal .@ x .@ y

-- * Class 'IfThenElseable'
class IfThenElseable sem where
  ifThenElse :: sem Bool -> sem a -> sem a -> sem a
  ifThenElse = liftDerived3 ifThenElse
  default ifThenElse ::
    FromDerived3 IfThenElseable sem =>
    sem Bool -> sem a -> sem a -> sem a

-- * Class 'Inferable'
class Inferable a sem where
  infer :: sem a
  default infer :: FromDerived (Inferable a) sem => sem a
  infer = liftDerived infer

unit :: Inferable () sem => sem ()
unit = infer
bool :: Inferable Bool sem => sem Bool
bool = infer
char :: Inferable Char sem => sem Char
char = infer
int :: Inferable Int sem => sem Int
int = infer
natural :: Inferable Natural sem => sem Natural
natural = infer
string :: Inferable String sem => sem String
string = infer

-- * Class 'Listable'
class Listable sem where
  cons :: sem (a -> [a] -> [a])
  nil :: sem [a]
  cons = liftDerived cons
  nil = liftDerived nil
  default cons ::
    FromDerived Listable sem =>
    sem (a -> [a] -> [a])
  default nil ::
    FromDerived Listable sem =>
    sem [a]

-- * Class 'Maybeable'
class Maybeable sem where
  nothing :: sem (Maybe a)
  just :: sem (a -> Maybe a)
  nothing = liftDerived nothing
  just = liftDerived just
  default nothing ::
    FromDerived Maybeable sem =>
    sem (Maybe a)
  default just ::
    FromDerived Maybeable sem =>
    sem (a -> Maybe a)

-- * Class 'IsoFunctor'
class IsoFunctor sem where
  (<%>) :: Iso a b -> sem a -> sem b; infixl 4 <%>
  (<%>) iso = liftDerived1 (iso <%>)
  default (<%>) ::
    FromDerived1 IsoFunctor sem =>
    Iso a b -> sem a -> sem b

-- ** Type 'Iso'
data Iso a b = Iso { a2b :: a->b, b2a :: b->a }
instance Cat.Category Iso where
  id = Iso Cat.id Cat.id
  f . g = Iso (a2b f Cat.. a2b g) (b2a g Cat.. b2a f)

-- * Class 'ProductFunctor'
-- | Beware that this is an @infixr@,
-- not @infixl@ like 'Control.Applicative.<*>';
-- this is to follow what is expected by 'ADT'.
class ProductFunctor sem where
  (<.>) :: sem a -> sem b -> sem (a, b); infixr 4 <.>
  (<.>) = liftDerived2 (<.>)
  default (<.>) ::
    FromDerived2 ProductFunctor sem =>
    sem a -> sem b -> sem (a, b)
  (<.) :: sem a -> sem () -> sem a; infixr 4 <.
  ra <. rb = Iso Tuple.fst (, ()) <%> (ra <.> rb)
  default (<.) :: IsoFunctor sem => sem a -> sem () -> sem a
  (.>) :: sem () -> sem a -> sem a; infixr 4 .>
  ra .> rb = Iso Tuple.snd (() ,) <%> (ra <.> rb)
  default (.>) :: IsoFunctor sem => sem () -> sem a -> sem a

-- * Class 'SumFunctor'
-- | Beware that this is an @infixr@,
-- not @infixl@ like 'Control.Applicative.<|>';
-- this is to follow what is expected by 'ADT'.
class SumFunctor sem where
  (<+>) :: sem a -> sem b -> sem (Either a b); infixr 3 <+>
  (<+>) = liftDerived2 (<+>)
  default (<+>) ::
    FromDerived2 SumFunctor sem =>
    sem a -> sem b -> sem (Either a b)

-- * Class 'AlternativeFunctor'
-- | Beware that this is an @infixr@,
-- not @infixl@ like 'Control.Applicative.<|>';
-- this is to follow what is expected by 'ADT'.
class AlternativeFunctor sem where
  (<|>) :: sem a -> sem a -> sem a; infixr 3 <|>
  (<|>) = liftDerived2 (<|>)
  default (<|>) ::
    FromDerived2 AlternativeFunctor sem =>
    sem a -> sem a -> sem a

-- * Class 'Dicurryable'
class Dicurryable sem where
  dicurry ::
    CurryN args =>
    proxy args ->
    (args-..->a) -> -- construction
    (a->Tuples args) -> -- destruction
    sem (Tuples args) ->
    sem a
  dicurry args constr destr = liftDerived1 (dicurry args constr destr)
  default dicurry ::
    FromDerived1 Dicurryable sem =>
    CurryN args =>
    proxy args ->
    (args-..->a) ->
    (a->Tuples args) ->
    sem (Tuples args) ->
    sem a

construct ::
  forall args a sem.
  Dicurryable sem =>
  Generic a =>
  EoTOfRep a =>
  CurryN args =>
  Tuples args ~ EoT (ADT a) =>
  (args ~ Args (args-..->a)) =>
  (args-..->a) ->
  sem (Tuples args) ->
  sem a
construct f = dicurry (Proxy::Proxy args) f eotOfadt

adt ::
  forall adt sem.
  IsoFunctor sem =>
  Generic adt =>
  RepOfEoT adt =>
  EoTOfRep adt =>
  sem (EoT (ADT adt)) ->
  sem adt
adt = (<%>) (Iso adtOfeot eotOfadt)

-- * Class 'IfSemantic'
-- | 'IfSemantic' enables to change the 'Syntax' for a specific 'Semantic'.
--
-- Useful when a 'Semantic' does not implement some 'Syntax'es used by other 'Semantic's.
class
  IfSemantic
    (thenSyntaxes :: [Syntax])
    (elseSyntaxes :: [Syntax])
    thenSemantic
    elseSemantic
  where
  ifSemantic ::
    (Syntaxes thenSyntaxes thenSemantic => thenSemantic a) ->
    (Syntaxes elseSyntaxes elseSemantic => elseSemantic a) ->
    elseSemantic a
instance
  {-# OVERLAPPING #-}
  Syntaxes thenSyntaxes thenSemantic =>
  IfSemantic thenSyntaxes elseSyntaxes thenSemantic thenSemantic where
  ifSemantic thenSyntax _elseSyntax = thenSyntax
instance
  Syntaxes elseSyntaxes elseSemantic =>
  IfSemantic thenSyntaxes elseSyntaxes thenSemantic elseSemantic where
  ifSemantic _thenSyntax elseSyntax = elseSyntax

-- * Class 'Monoidable'
class
  ( Emptyable sem
  , Semigroupable sem
  ) => Monoidable sem
instance
  ( Emptyable sem
  , Semigroupable sem
  ) => Monoidable sem

-- ** Class 'Emptyable'
class Emptyable sem where
  empty :: sem a
  empty = liftDerived empty
  default empty ::
    FromDerived Emptyable sem =>
    sem a

-- ** Class 'Semigroupable'
class Semigroupable sem where
  concat :: Semigroup a => sem (a -> a -> a)
  concat = liftDerived concat
  default concat ::
    FromDerived Semigroupable sem =>
    Semigroup a =>
    sem (a -> a -> a)

infixr 6 `concat`, <>
(<>) ::
  Abstractable sem => Semigroupable sem => Semigroup a =>
  sem a -> sem a -> sem a
(<>) x y = concat .@ x .@ y

-- ** Class 'Optionable'
class Optionable sem where
  optional :: sem a -> sem (Maybe a)
  optional = liftDerived1 optional
  default optional ::
    FromDerived1 Optionable sem =>
    sem a -> sem (Maybe a)

-- * Class 'Repeatable'
class Repeatable sem where
  many0 :: sem a -> sem [a]
  many1 :: sem a -> sem [a]
  many0 = liftDerived1 many0
  many1 = liftDerived1 many1
  default many0 ::
    FromDerived1 Repeatable sem =>
    sem a -> sem [a]
  default many1 ::
    FromDerived1 Repeatable sem =>
    sem a -> sem [a]

-- | Alias to 'many0'.
many :: Repeatable sem => sem a -> sem [a]
many = many0

-- | Alias to 'many1'.
some :: Repeatable sem => sem a -> sem [a]
some = many1

-- * Class 'Permutable'
class Permutable sem where
  -- Use @TypeFamilyDependencies@ to help type-inference infer @(sem)@.
  type Permutation (sem:: Semantic) = (r :: Semantic) | r -> sem
  type Permutation sem = Permutation (Derived sem)
  permutable :: Permutation sem a -> sem a
  perm :: sem a -> Permutation sem a
  noPerm :: Permutation sem ()
  permWithDefault :: a -> sem a -> Permutation sem a
  optionalPerm ::
    Eitherable sem => IsoFunctor sem => Permutable sem =>
    sem a -> Permutation sem (Maybe a)
  optionalPerm = permWithDefault Nothing Fun.. (<%>) (Iso Just fromJust)

(<&>) ::
  Permutable sem =>
  ProductFunctor (Permutation sem) =>
  sem a ->
  Permutation sem b ->
  Permutation sem (a, b)
x <&> y = perm x <.> y
infixr 4 <&>
{-# INLINE (<&>)  #-}

(<?&>) ::
  Eitherable sem =>
  IsoFunctor sem =>
  Permutable sem =>
  ProductFunctor (Permutation sem) =>
  sem a ->
  Permutation sem b ->
  Permutation sem (Maybe a, b)
x <?&> y = optionalPerm x <.> y
infixr 4 <?&>
{-# INLINE (<?&>) #-}

(<*&>) ::
  Eitherable sem =>
  Repeatable sem =>
  IsoFunctor sem =>
  Permutable sem =>
  ProductFunctor (Permutation sem) =>
  sem a ->
  Permutation sem b ->
  Permutation sem ([a],b)
x <*&> y = permWithDefault [] (many1 x) <.> y
infixr 4 <*&>
{-# INLINE (<*&>) #-}

(<+&>) ::
  Eitherable sem =>
  Repeatable sem =>
  IsoFunctor sem =>
  Permutable sem =>
  ProductFunctor (Permutation sem) =>
  sem a ->
  Permutation sem b ->
  Permutation sem ([a], b)
x <+&> y = perm (many1 x) <.> y
infixr 4 <+&>
{-# INLINE (<+&>) #-}

-- * Class 'Routable'
class Routable sem where
  (<!>) :: sem a -> sem b -> sem (a, b); infixr 4 <!>
  (<!>) = liftDerived2 (<!>)
  default (<!>) ::
    FromDerived2 Routable sem =>
    sem a -> sem b -> sem (a, b)

-- | Like @(,)@ but @infixr@.
-- Mostly useful for clarity when using 'Routable'.
pattern (:!:) :: a -> b -> (a, b)
pattern a:!:b <- (a, b)
  where a:!:b = (a, b)
infixr 4 :!:

-- * Class 'Voidable'
class Voidable sem where
  -- | Useful to supply @(a)@ to a @(sem)@ consuming @(a)@,
  -- for example in the format of a printing interpreter.
  void :: a -> sem a -> sem ()
  void = liftDerived1 Fun.. void
  default void ::
    FromDerived1 Voidable sem =>
    a -> sem a -> sem ()

-- * Class 'Substractable'
class Substractable sem where
  (<->) :: sem a -> sem b -> sem a; infixr 3 <->
  (<->) = liftDerived2 (<->)
  default (<->) ::
    FromDerived2 Substractable sem =>
    sem a -> sem b -> sem a