{-# LANGUAGE PatternSynonyms #-} -- For Comb and OptC
{-# LANGUAGE TemplateHaskell #-} -- For branch
{-# LANGUAGE ViewPatterns #-} -- For unSomeComb
{-# OPTIONS_GHC -fno-warn-orphans #-} -- For MakeLetName TH.Name
module Symantic.Parser.Grammar.Optimize where

import Data.Bool (Bool(..))
import Data.Either (Either(..), either)
import Data.Eq (Eq(..))
import Data.Function ((.))
import Data.Maybe (Maybe(..))
import qualified Data.Functor as Functor
import qualified Data.Foldable as Foldable
import qualified Data.List as List
import qualified Language.Haskell.TH.Syntax as TH
import Data.Kind (Constraint, Type)
import Type.Reflection (Typeable, typeRep, eqTypeRep, (:~~:)(..))

import Symantic.Parser.Grammar.Combinators as Comb
import Symantic.Parser.Haskell ()
import Symantic.Univariant.Letable
import Symantic.Univariant.Trans
import qualified Symantic.Parser.Haskell as H

{-
import Data.Function (($), flip)
import Debug.Trace (trace)

(&) = flip ($)
infix 0 &
-}

-- * Data family 'Comb'
-- | 'Comb'uctions for the 'Machine'.
-- This is an extensible data-type.
data family Comb
  (comb :: ReprComb -> Constraint)
  (repr :: ReprComb)
  :: ReprComb

-- | Convenient utility to pattern-match a 'SomeComb'.
pattern Comb :: Typeable comb =>
  Comb comb repr a ->
  SomeComb repr a
pattern Comb x <- (unSomeComb -> Just x)

-- ** Type 'ReprComb'
type ReprComb = Type -> Type

-- ** Type 'SomeComb'
-- | Some 'Comb'inator existentialized over the actual combinator symantic class.
-- Useful to handle a list of 'Comb'inators
-- without requiring impredicative quantification.
-- Must be used by pattern-matching
-- on the 'SomeComb' data-constructor,
-- to bring the constraints in scope.
data SomeComb repr a =
  forall comb.
  (Trans (Comb comb repr) repr, Typeable comb) =>
  SomeComb (Comb comb repr a)

instance Trans (SomeComb repr) repr where
  trans (SomeComb x) = trans x

-- | @(unSomeComb c :: 'Maybe' ('Comb' comb repr a))@
-- extract the data-constructor from the given 'SomeComb'
-- iif. it belongs to the @('Comb' comb repr a)@ data-instance.
unSomeComb ::
  forall comb repr a.
  Typeable comb =>
  SomeComb repr a -> Maybe (Comb comb repr a)
unSomeComb (SomeComb (c::Comb c repr a)) =
  case typeRep @comb `eqTypeRep` typeRep @c of
    Just HRefl -> Just c
    Nothing -> Nothing

-- Applicable
data instance Comb Applicable repr a where
  Pure :: TermGrammar a -> Comb Applicable repr a
  (:<*>:) :: SomeComb repr (a -> b) -> SomeComb repr a -> Comb Applicable repr b
  (:<*:) :: SomeComb repr a -> SomeComb repr b -> Comb Applicable repr a
  (:*>:) :: SomeComb repr a -> SomeComb repr b -> Comb Applicable repr b
infixl 4 :<*>:, :<*:, :*>:
pattern (:<$>:) :: TermGrammar (a -> b) -> SomeComb repr a -> Comb Applicable repr b
pattern t :<$>: x <- Comb (Pure t) :<*>: x
pattern (:$>:) :: SomeComb repr a -> TermGrammar b -> Comb Applicable repr b
pattern x :$>: t <- x :*>: Comb (Pure t)
instance Applicable repr => Trans (Comb Applicable repr) repr where
  trans = \case
    Pure x -> pure (H.optimizeTerm x)
    f :<*>: x -> trans f <*> trans x
    x :<*: y -> trans x <* trans y
    x :*>: y -> trans x *> trans y
instance Applicable repr => Applicable (SomeComb repr) where
  pure = SomeComb . Pure
  (<*>) f = SomeComb . (:<*>:) f
  (<*) x = SomeComb . (:<*:) x
  (*>) x = SomeComb . (:*>:) x

-- Alternable
data instance Comb Alternable repr a where
  Empty :: Comb Alternable repr a
  (:<|>:) :: SomeComb repr a -> SomeComb repr a -> Comb Alternable repr a
  Try :: SomeComb repr a -> Comb Alternable repr a
infixl 3 :<|>:
instance Alternable repr => Trans (Comb Alternable repr) repr where
  trans = \case
    Empty -> empty
    f :<|>: x -> trans f <|> trans x
    Try x -> try (trans x)
instance Alternable repr => Alternable (SomeComb repr) where
  empty = SomeComb Empty
  (<|>) f = SomeComb . (:<|>:) f
  try = SomeComb . Try

-- Selectable
data instance Comb Selectable repr a where
  Branch ::
    SomeComb repr (Either a b) ->
    SomeComb repr (a -> c) ->
    SomeComb repr (b -> c) ->
    Comb Selectable repr c
instance Selectable repr => Trans (Comb Selectable repr) repr where
  trans = \case
    Branch lr l r -> branch (trans lr) (trans l) (trans r)
instance Selectable repr => Selectable (SomeComb repr) where
  branch lr l = SomeComb . Branch lr l

-- Matchable
data instance Comb Matchable repr a where
  Conditional :: Eq a =>
    SomeComb repr a ->
    [TermGrammar (a -> Bool)] ->
    [SomeComb repr b] ->
    SomeComb repr b ->
    Comb Matchable repr b
instance Matchable repr => Trans (Comb Matchable repr) repr where
  trans = \case
    Conditional a ps bs b -> conditional (trans a) ps (trans Functor.<$> bs) (trans b)
instance Matchable repr => Matchable (SomeComb repr) where
  conditional a ps bs = SomeComb . Conditional a ps bs

-- Foldable
data instance Comb Foldable repr a where
  ChainPreC :: SomeComb repr (a -> a) -> SomeComb repr a -> Comb Foldable repr a
  ChainPostC :: SomeComb repr a -> SomeComb repr (a -> a) -> Comb Foldable repr a
instance Foldable repr => Trans (Comb Foldable repr) repr where
  trans = \case
    ChainPreC x y -> chainPre (trans x) (trans y)
    ChainPostC x y -> chainPost (trans x) (trans y)
instance Foldable repr => Foldable (SomeComb repr) where
  chainPre x = SomeComb . ChainPreC x
  chainPost x = SomeComb . ChainPostC x

-- Lookable
data instance Comb Lookable repr a where
  Look :: SomeComb repr a -> Comb Lookable repr a
  NegLook :: SomeComb repr a -> Comb Lookable repr ()
  Eof :: Comb Lookable repr ()
instance Lookable repr => Trans (Comb Lookable repr) repr where
  trans = \case
    Look x -> look (trans x)
    NegLook x -> negLook (trans x)
    Eof -> eof
instance Lookable repr => Lookable (SomeComb repr) where
  look = SomeComb . Look
  negLook = SomeComb . NegLook
  eof = SomeComb Eof

-- Satisfiable
data instance Comb (Satisfiable tok) repr a where
  Satisfy ::
    Satisfiable tok repr =>
    [ErrorItem tok] ->
    TermGrammar (tok -> Bool) ->
    Comb (Satisfiable tok) repr tok
  Item ::
    Satisfiable tok repr =>
    Comb (Satisfiable tok) repr tok
instance Satisfiable tok repr => Trans (Comb (Satisfiable tok) repr) repr where
  trans = \case
    Satisfy es p -> satisfy es p
    Item -> item
instance
  (Satisfiable tok repr, Typeable tok) =>
  Satisfiable tok (SomeComb repr) where
  satisfy es = SomeComb . Satisfy es
  item = SomeComb Item

-- Letable
data instance Comb (Letable letName) repr a where
  Def :: letName -> SomeComb repr a -> Comb (Letable letName) repr a
  Ref :: Bool -> letName -> Comb (Letable letName) repr a
instance Letable letName repr => Trans (Comb (Letable letName) repr) repr where
  trans = \case
    Def n v -> def n (trans v)
    Ref isRec n -> ref isRec n
instance
  (Letable letName repr, Typeable letName) =>
  Letable letName (SomeComb repr) where
  def n = SomeComb . Def n
  ref isRec = SomeComb . Ref isRec
instance MakeLetName TH.Name where
  makeLetName _ = TH.qNewName "name"

-- * Type 'OptimizeGrammar'
type OptimizeGrammar = OptComb

optimizeGrammar ::
  Trans (OptComb TH.Name repr) repr =>
  OptComb TH.Name repr a -> repr a
optimizeGrammar = trans

-- ** Type 'OptComb'
newtype OptComb letName repr a =
        OptComb { unOptComb :: SomeComb repr a }
-- | Matching an 'OptComb'.
pattern OptC :: Typeable comb => Comb comb repr a -> OptComb letName repr a
pattern OptC x <- (unSomeComb . unOptComb -> Just x)
instance
  Trans (SomeComb repr) repr =>
  Trans (OptComb letName repr) repr where
  trans = trans . unOptComb

instance
  ( Applicable repr
  , Alternable repr
  , Lookable repr
  , Selectable repr
  , Matchable repr
  ) => Applicable (OptComb letName repr) where
  pure = OptComb . pure

  f <$> OptC (Branch b l r) =
    branch (OptComb b)
      ((H..) H..@ f <$> OptComb l)
      ((H..) H..@ f <$> OptComb r)
    -- & trace "Branch Distributivity Law"
  f <$> OptC (Conditional a ps bs d) =
    conditional (OptComb a) ps
      ((f <$>) . OptComb Functor.<$> bs)
      (f <$> OptComb d)
    -- & trace "Conditional Distributivity Law"
  -- Being careful here to use (<*>),
  -- instead of OptComb (f <$> unOptComb x),
  -- in order to apply the optimizations of (<*>).
  f <$> x = pure f <*> x

  x <$ u = u $> x
    -- & trace "Commutativity Law"

  OptC Empty <*> _ = empty
    -- & trace "App Right Absorption Law"
  u <*> OptC Empty = u *> empty
    -- & trace "App Failure Weakening Law"
  OptC (Pure f) <*> OptC (Pure x) = pure (f H..@ x)
    -- & trace "Homomorphism Law"
  OptC (Pure f) <*> OptC (g :<$>: p) =
    -- This is basically a shortcut,
    -- it can be caught by the Composition Law
    -- and Homomorphism Law.
    (H..) H..@ f H..@ g <$> OptComb p
    -- & trace "Functor Composition Law"
  u <*> OptC (v :<*>: w) =
    (((H..) <$> u) <*> OptComb v) <*> OptComb w
    -- & trace "Composition Law"
  u <*> OptC (Pure x) =
    H.flip H..@ (H.$) H..@ x <$> u
    -- & trace "Interchange Law"
  OptC (u :*>: v) <*> w =
    OptComb u *> (OptComb v <*> w)
    -- & trace "Reassociation Law 1"
  u <*> OptC (v :<*: w) =
    (u <*> OptComb v) <* OptComb w
    -- & trace "Reassociation Law 2"
  u <*> OptC (v :$>: x) =
    (u <*> pure x) <* OptComb v
    -- & trace "Reassociation Law 3"
  p <*> OptC (NegLook q) =
    (p <*> pure H.unit) <* negLook (OptComb q)
    -- & trace "Absorption Law"
  OptComb x <*> OptComb y = OptComb (x <*> y)

  OptC Empty *> _ = empty
    -- & trace "App Right Absorption Law"
  OptC (_ :<$>: p) *> q = OptComb p *> q
    -- & trace "Right Absorption Law"
  OptC Pure{} *> u = u
    -- & trace "Identity Law"
  OptC (u :$>: _) *> v = OptComb u *> v
    -- & trace "Identity Law"
  u *> OptC (v :*>: w) =
    (u *> OptComb v) *> OptComb w
    -- & trace "Associativity Law"
  OptComb x *> OptComb y = OptComb (x *> y)

  OptC Empty <* _ = empty
    -- & trace "App Right Absorption Law"
  u <* OptC Empty = u *> empty
    -- & trace "App Failure Weakening Law"
  p <* OptC (_ :<$>: q) = p <* OptComb q
    -- & trace "Left Absorption Law"
  u <* OptC Pure{} = u
    -- & trace "Identity Law"
  u <* OptC (v :$>: _) = u <* OptComb v
    -- & trace "Identity Law"
  OptC (u :<*: v) <* w = OptComb u <* (OptComb v <* w)
    -- & trace "Associativity Law"
  OptComb x <* OptComb y = OptComb (x <* y)
instance
  ( Applicable repr
  , Alternable repr
  , Lookable repr
  , Selectable repr
  , Matchable repr
  ) => Alternable (OptComb letName repr) where
  empty = OptComb empty

  p@(OptC Pure{}) <|> _ = p
    -- & trace "Left Catch Law"
  OptC Empty <|> u = u
    -- & trace "Left Neutral Law"
  u <|> OptC Empty = u
    -- & trace "Right Neutral Law"
  OptC (u :<|>: v) <|> w = OptComb u <|> (OptComb v <|> w)
    -- & trace "Associativity Law"
  OptC (Look p) <|> OptC (Look q) =
    look (try (OptComb p) <|> OptComb q)
    -- & trace "Distributivity Law"
  OptComb x <|> OptComb y = OptComb (x <|> y)

  try (OptC (p :$>: x)) = try (OptComb p) $> x
    -- & trace "Try Interchange Law"
  try (OptC (f :<$>: p)) = f <$> try (OptComb p)
    -- & trace "Try Interchange Law"
  try (OptComb x) = OptComb (try x)
instance
  ( Applicable repr
  , Alternable repr
  , Lookable repr
  , Selectable repr
  , Matchable repr
  ) => Lookable (OptComb letName repr) where
  look p@(OptC Pure{}) = p
    -- & trace "Pure Look Law"
  look p@(OptC Empty) = p
    -- & trace "Dead Look Law"
  look (OptC (Look x)) = look (OptComb x)
    -- & trace "Idempotence Law"
  look (OptC (NegLook x)) = negLook (OptComb x)
    -- & trace "Left Identity Law"
  look (OptC (p :$>: x)) = look (OptComb p) $> x
    -- & trace "Interchange Law"
  look (OptC (f :<$>: p)) = f <$> look (OptComb p)
    -- & trace "Interchange Law"
  look (OptComb x) = OptComb (look x)

  negLook (OptC Pure{}) = empty
    -- & trace "Pure Negative-Look"
  negLook (OptC Empty) = pure H.unit
    -- & trace "Dead Negative-Look"
  negLook (OptC (NegLook x)) =
    look (try (OptComb x) *> pure H.unit)
    -- & trace "Double Negation Law"
  negLook (OptC (Try x)) = negLook (OptComb x)
    -- & trace "Zero Consumption Law"
  negLook (OptC (Look x)) = negLook (OptComb x)
    -- & trace "Right Identity Law"
  negLook (OptC (Comb (Try p) :<|>: q)) =
    negLook (OptComb p) *> negLook (OptComb q)
    -- & trace "Transparency Law"
  negLook (OptC (p :$>: _)) = negLook (OptComb p)
    -- & trace "NegLook Idempotence Law"
  negLook (OptComb x) = OptComb (negLook x)

  eof = OptComb eof
instance
  ( Applicable repr
  , Alternable repr
  , Lookable repr
  , Selectable repr
  , Matchable repr
  ) => Selectable (OptComb letName repr) where
  branch (OptC Empty) _ _ = empty
    -- & trace "Branch Absorption Law"
  branch b (OptC Empty) (OptC Empty) = b *> empty
    -- & trace "Branch Weakening Law"
  branch (OptC (Pure (trans -> lr))) l r =
    case H.value lr of
      Left value -> l <*> pure (trans H.ValueCode{..})
        where code = [|| case $$(H.code lr) of Left x -> x ||]
      Right value -> r <*> pure (trans H.ValueCode{..})
        where code = [|| case $$(H.code lr) of Right x -> x ||]
    -- & trace "Branch Pure Left/Right Law" $
  branch b (OptC (Pure (trans -> l))) (OptC (Pure (trans -> r))) =
    trans H.ValueCode{..} <$> b
    -- & trace "Branch Generalised Identity Law"
    where
    value = either (H.value l) (H.value r)
    code = [|| either $$(H.code l) $$(H.code r) ||]
  branch (OptC (x :*>: y)) p q =
    OptComb x *> branch (OptComb y) p q
    -- & trace "Interchange Law"
  branch b l (OptC Empty) =
    branch (pure (trans (H.ValueCode{..})) <*> b) empty l
    -- & trace "Negated Branch Law"
    where
    value = either Right Left
    code = [||either Right Left||]
  branch (OptC (Branch b (Comb Empty) (Comb (Pure (trans -> lr))))) (OptC Empty) br =
    branch (pure (trans H.ValueCode{..}) <*> OptComb b) empty br
    -- & trace "Branch Fusion Law"
    where
    value Left{} = Left ()
    value (Right r) = case H.value lr r of
                        Left _ -> Left ()
                        Right rr -> Right rr
    code = [|| \case Left{} -> Left ()
                     Right r -> case $$(H.code lr) r of
                                  Left _ -> Left ()
                                  Right rr -> Right rr ||]
  branch (OptComb b) (OptComb l) (OptComb r) =
    OptComb (branch b l r)
instance
  ( Applicable repr
  , Alternable repr
  , Lookable repr
  , Selectable repr
  , Matchable repr
  ) => Matchable (OptComb letName repr) where
  conditional (OptC Empty) _ _ d = d
    -- & trace "Conditional Absorption Law"
  conditional p _ qs (OptC Empty)
    | Foldable.all (\case { OptC Empty -> True; _ -> False }) qs = p *> empty
      -- & trace "Conditional Weakening Law"
  conditional a _ps bs (OptC Empty)
    | Foldable.all (\case { OptC Empty -> True; _ -> False }) bs = a *> empty
      -- & trace "Conditional Weakening Law"
  conditional (OptC (Pure (trans -> a))) ps bs d =
    Foldable.foldr (\(trans -> p, b) next ->
      if H.value p (H.value a) then b else next
    ) d (List.zip ps bs)
    -- & trace "Conditional Pure Law"
  conditional (OptComb a) ps bs (OptComb d) =
    OptComb (conditional a ps (unOptComb Functor.<$> bs) d)
instance
  (Letable letName repr, Typeable letName) =>
  Letable letName (OptComb letName repr) where
  def n (OptComb x) = OptComb (def n x)
  ref isRec n = OptComb (ref isRec n)
instance
  Foldable repr =>
  Foldable (OptComb letName repr) where
  chainPre (OptComb f) (OptComb x) = OptComb (chainPre f x)
  chainPost (OptComb x) (OptComb f) = OptComb (chainPost x f)
instance
  (Satisfiable tok repr, Typeable tok) =>
  Satisfiable tok (OptComb letName repr) where
  satisfy es p = OptComb (satisfy es p)