-- For ifSemantic
{-# LANGUAGE AllowAmbiguousTypes #-}
-- For Syntax
{-# LANGUAGE DataKinds #-}
-- For (:!:)
{-# LANGUAGE PatternSynonyms #-}
-- For ifSemantic
{-# LANGUAGE RankNTypes #-}
-- For Permutation
{-# LANGUAGE TypeFamilyDependencies #-}
-- For Permutation
{-# LANGUAGE UndecidableInstances #-}

-- | This module gathers commonly used tagless-final combinators
-- (the syntax part of symantics).
--
-- Note: combinators in this module conflict with usual ones from the @Prelude@
-- hence they are meant to be imported either explicitely or qualified.
module Symantic.Syntaxes.Classes where

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

import Symantic.Syntaxes.CurryN
import Symantic.Syntaxes.Derive
import Symantic.Syntaxes.EithersOfTuples

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

-- ** Type family 'Syntaxes'

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

-- * Class 'Abstractable'
class Abstractable sem where
  -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  lam :: (sem a -> sem b) -> sem (a -> b)
  lam f = liftDerived (lam (derive Fun.. f Fun.. liftDerived))
  default lam ::
    FromDerived Abstractable sem =>
    Derivable sem =>
    (sem a -> sem b) ->
    sem (a -> b)

-- ** Class 'Abstractable1'
class Abstractable1 sem where
  -- | 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)
  lam1 f = liftDerived (lam1 (derive Fun.. f Fun.. liftDerived))
  default lam1 ::
    FromDerived Abstractable1 sem =>
    Derivable sem =>
    (sem a -> sem b) ->
    sem (a -> b)

-- ** Class 'Varable'
class Varable sem where
  -- | Mark the use of a variable.
  var :: sem a -> sem a
  var = liftDerived1 var
  default var :: FromDerived1 Varable sem => sem a -> sem a

-- ** Class 'Instantiable'
class Instantiable sem where
  -- | Instantiate.
  (.@) :: sem (a -> b) -> sem a -> sem b

  infixl 9 .@
  (.@) = liftDerived2 (.@)
  default (.@) ::
    FromDerived2 Instantiable sem =>
    sem (a -> b) ->
    sem a ->
    sem b

-- ** Class 'Unabstractable'
-- | All operations in lambda calculus can be encoded
-- via abstraction elimination into the SK calculus
-- as binary trees whose leaves are one
-- of the three symbols S ('ap') and K ('const').
class Unabstractable sem where
  -- | S
  ap :: sem ((a -> b -> c) -> (a -> b) -> a -> c)
  -- | K
  const :: sem (a -> b -> a)
  -- | I
  id :: sem (a -> a)
  -- | B
  (.) :: sem ((b -> c) -> (a -> b) -> a -> c)
  infixr 9 .
  -- | C
  flip :: sem ((a -> b -> c) -> b -> a -> c)
  ($) :: sem ((a -> b) -> a -> b)
  infixr 0 $

  ap = liftDerived ap
  const = liftDerived const
  id = liftDerived id
  (.) = liftDerived (.)
  flip = liftDerived flip
  ($) = liftDerived ($)

  default ap ::
    FromDerived Unabstractable sem =>
    sem ((a -> b -> c) -> (a -> b) -> a -> c)
  default const ::
    FromDerived Unabstractable sem =>
    sem (a -> b -> a)
  default id ::
    FromDerived Unabstractable sem =>
    sem (a -> a)
  default (.) ::
    FromDerived Unabstractable sem =>
    sem ((b -> c) -> (a -> b) -> a -> c)
  default flip ::
    FromDerived Unabstractable sem =>
    sem ((a -> b -> c) -> b -> a -> c)
  default ($) ::
    FromDerived Unabstractable 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
  either :: sem ((l -> a) -> (r -> a) -> Either l r -> a)
  left :: sem (l -> Either l r)
  right :: sem (r -> Either l r)
  either = liftDerived either
  left = liftDerived left
  right = liftDerived right
  default either ::
    FromDerived Eitherable sem =>
    sem ((l -> a) -> (r -> a) -> Either l r -> a)
  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`, ==
(==) ::
  Instantiable 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)

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

infixr 4 :!:
{-# COMPLETE (:!:) #-}

-- * 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

-- * Class 'Dataable'

-- | Enable the contruction or deconstruction
-- of an 'ADT' (algebraic data type).
class Dataable a sem where
  dataType :: sem (EoT (ADT a)) -> sem a
  default dataType ::
    Generic a =>
    RepOfEoT a =>
    EoTOfRep a =>
    IsoFunctor sem =>
    sem (EoT (ADT a)) ->
    sem a
  dataType = (<%>) (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`, <>
(<>) ::
  Instantiable 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 '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