{-# LANGUAGE PatternSynonyms #-} -- For Comb
{-# LANGUAGE TemplateHaskell #-} -- For branch
{-# LANGUAGE ViewPatterns #-} -- For unSomeComb
{-# OPTIONS_GHC -fno-warn-orphans #-} -- For MakeLetName TH.Name
-- | Bottom-up optimization of 'Comb'inators,
-- reexamining downward as needed after each optimization.
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

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

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

-- * Type 'OptimizeGrammar'
type OptimizeGrammar = SomeComb

optimizeGrammar ::
  Trans (SomeComb repr) repr =>
  SomeComb repr a -> repr a
optimizeGrammar = trans

-- * Data family 'Comb'
-- | 'Comb'inators of the 'Grammar'.
-- 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.
--
-- The optimizations are directly applied within it,
-- to avoid introducing an extra newtype,
-- this also give a more comprehensible code.
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
  , Alternable repr
  , Lookable repr
  , Matchable repr
  , Selectable repr
  ) => Applicable (SomeComb repr) where
  pure = SomeComb . Pure
  f <$> Comb (Branch b l r) =
    branch b
      ((H..) H..@ f <$> l)
      ((H..) H..@ f <$> r)
    -- & trace "Branch Distributivity Law"
  f <$> Comb (Conditional a ps bs d) =
    conditional a ps
      ((f <$>) Functor.<$> bs)
      (f <$> d)
    -- & trace "Conditional Distributivity Law"
  -- Being careful here to use (<*>),
  -- instead of SomeComb (f <$> unOptComb x),
  -- in order to apply the optimizations of (<*>).
  f <$> x = pure f <*> x

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

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

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

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

-- 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
  , Applicable repr
  , Lookable repr
  , Matchable repr
  , Selectable repr
  ) => Alternable (SomeComb repr) where
  empty = SomeComb Empty

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

  try (Comb (p :$>: x)) = try p $> x
    -- & trace "Try Interchange Law"
  try (Comb (f :<$>: p)) = f <$> try p
    -- & trace "Try Interchange Law"
  try x = SomeComb (Try x)

-- 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
  ( Applicable repr
  , Alternable repr
  , Lookable repr
  , Selectable repr
  , Matchable repr
  ) => Selectable (SomeComb repr) where
  branch (Comb Empty) _ _ = empty
    -- & trace "Branch Absorption Law"
  branch b (Comb Empty) (Comb Empty) = b *> empty
    -- & trace "Branch Weakening Law"
  branch (Comb (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 (Comb (Pure (trans -> l))) (Comb (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 (Comb (x :*>: y)) p q = x *> branch y p q
    -- & trace "Interchange Law"
  branch b l (Comb Empty) =
    branch (pure (trans (H.ValueCode{..})) <*> b) empty l
    -- & trace "Negated Branch Law"
    where
    value = either Right Left
    code = [||either Right Left||]
  branch (Comb (Branch b (Comb Empty) (Comb (Pure (trans -> lr))))) (Comb Empty) br =
    branch (pure (trans H.ValueCode{..}) <*> 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 b l r = SomeComb (Branch b l r)

-- 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
  ( Applicable repr
  , Alternable repr
  , Lookable repr
  , Selectable repr
  , Matchable repr
  ) => Matchable (SomeComb repr) where
  conditional (Comb Empty) _ _ d = d
    -- & trace "Conditional Absorption Law"
  conditional p _ qs (Comb Empty)
    | Foldable.all (\case { Comb Empty -> True; _ -> False }) qs = p *> empty
      -- & trace "Conditional Weakening Law"
  conditional a _ps bs (Comb Empty)
    | Foldable.all (\case { Comb Empty -> True; _ -> False }) bs = a *> empty
      -- & trace "Conditional Weakening Law"
  conditional (Comb (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 a ps bs d = SomeComb (Conditional a ps bs d)

-- 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
  ( Alternable repr
  , Applicable repr
  , Lookable repr
  , Selectable repr
  , Matchable repr
  ) => Lookable (SomeComb repr) where
  look p@(Comb Pure{}) = p
    -- & trace "Pure Look Law"
  look p@(Comb Empty) = p
    -- & trace "Dead Look Law"
  look (Comb (Look x)) = look x
    -- & trace "Idempotence Law"
  look (Comb (NegLook x)) = negLook x
    -- & trace "Left Identity Law"
  look (Comb (p :$>: x)) = look p $> x
    -- & trace "Interchange Law"
  look (Comb (f :<$>: p)) = f <$> look p
    -- & trace "Interchange Law"
  look x = SomeComb (Look x)

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

  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"