{-# 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 'ReprKind'
-- | The kind of @repr@(esentations) throughout this library.
type ReprKind = Type -> Type

-- * Class 'Abstractable'
class Abstractable repr where
  -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  lam :: (repr a -> repr b) -> repr (a->b)
  -- | Like 'lam' but whose argument must be used only once,
  -- hence safe to beta-reduce (inline) without duplicating work.
  lam1 :: (repr a -> repr b) -> repr (a->b)
  var :: repr a -> repr a
  -- | Application, aka. unabstract.
  (.@) :: repr (a->b) -> repr a -> repr 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 repr => Derivable repr =>
    (repr a -> repr b) -> repr (a->b)
  default lam1 ::
    FromDerived Abstractable repr => Derivable repr =>
    (repr a -> repr b) -> repr (a->b)
  default var ::
    FromDerived1 Abstractable repr =>
    repr a -> repr a
  default (.@) ::
    FromDerived2 Abstractable repr =>
    repr (a->b) -> repr a -> repr b

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

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

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

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

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

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

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

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

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

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

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

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

-- * Class 'IsoFunctor'
class IsoFunctor repr where
  (<%>) :: Iso a b -> repr a -> repr b; infixl 4 <%>
  (<%>) iso = liftDerived1 (iso <%>)
  default (<%>) ::
    FromDerived1 IsoFunctor repr =>
    Iso a b -> repr a -> repr 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 repr where
  (<.>) :: repr a -> repr b -> repr (a, b); infixr 4 <.>
  (<.>) = liftDerived2 (<.>)
  default (<.>) ::
    FromDerived2 ProductFunctor repr =>
    repr a -> repr b -> repr (a, b)
  (<.) :: repr a -> repr () -> repr a; infixr 4 <.
  ra <. rb = Iso Tuple.fst (, ()) <%> (ra <.> rb)
  default (<.) :: IsoFunctor repr => repr a -> repr () -> repr a
  (.>) :: repr () -> repr a -> repr a; infixr 4 .>
  ra .> rb = Iso Tuple.snd (() ,) <%> (ra <.> rb)
  default (.>) :: IsoFunctor repr => repr () -> repr a -> repr 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 repr where
  (<+>) :: repr a -> repr b -> repr (Either a b); infixr 3 <+>
  (<+>) = liftDerived2 (<+>)
  default (<+>) ::
    FromDerived2 SumFunctor repr =>
    repr a -> repr b -> repr (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 repr where
  (<|>) :: repr a -> repr a -> repr a; infixr 3 <|>
  (<|>) = liftDerived2 (<|>)
  default (<|>) ::
    FromDerived2 AlternativeFunctor repr =>
    repr a -> repr a -> repr a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-- * Class 'Routable'
class Routable repr where
  (<!>) :: repr a -> repr b -> repr (a, b); infixr 4 <!>
  (<!>) = liftDerived2 (<!>)
  default (<!>) ::
    FromDerived2 Routable repr =>
    repr a -> repr b -> repr (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 repr where
  -- | Useful to supply @(a)@ to a @(repr)@ consuming @(a)@,
  -- for example in the format of a printing interpreter.
  void :: a -> repr a -> repr ()
  void = liftDerived1 Fun.. void
  default void ::
    FromDerived1 Voidable repr =>
    a -> repr a -> repr ()

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