{-# LANGUAGE PatternSynonyms #-} -- For aliased combinators
{-# LANGUAGE TemplateHaskell #-} -- For optimizeCombNode
{-# LANGUAGE ViewPatterns #-} -- For optimizeCombNode
{-# 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 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 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 Debug.Trace (trace)

-- * Type 'Comb'
-- | Pattern-matchable 'Comb'inators of the grammar.
-- @(repr)@ is not strictly necessary since it's only a phantom type
-- (no constructor use it as a value), but having it:
--
-- 1. emphasizes that those 'Comb'inators will be 'trans'formed again
--    (eg. in 'ViewGrammar' or 'Instr'uctions).
--
-- 2. Avoid overlapping instances between
--    @('Trans' ('Comb' repr) repr)@ and
--    @('Trans' ('Comb' repr) ('OptimizeGrammar' letName repr))@
data Comb repr a where
  Pure :: TermGrammar a -> Comb repr a
  Satisfy ::
    Satisfiable repr tok =>
    [ErrorItem tok] ->
    TermGrammar (tok -> Bool) -> Comb repr tok
  Item :: Satisfiable repr tok => Comb repr tok
  Try :: Comb repr a -> Comb repr a
  Look :: Comb repr a -> Comb repr a
  NegLook :: Comb repr a -> Comb repr ()
  Eof :: Comb repr ()
  (:<*>) :: Comb repr (a -> b) -> Comb repr a -> Comb repr b
  (:<*) :: Comb repr a -> Comb repr b -> Comb repr a
  (:*>) :: Comb repr a -> Comb repr b -> Comb repr b
  (:<|>) :: Comb repr a -> Comb repr a -> Comb repr a
  Empty :: Comb repr a
  Branch ::
    Comb repr (Either a b) ->
    Comb repr (a -> c) -> Comb repr (b -> c) -> Comb repr c
  Match :: Eq a =>
    Comb repr a ->
    [TermGrammar (a -> Bool)] ->
    [Comb repr b] -> Comb repr b -> Comb repr b
  ChainPre :: Comb repr (a -> a) -> Comb repr a -> Comb repr a
  ChainPost :: Comb repr a -> Comb repr (a -> a) -> Comb repr a
  Def :: TH.Name -> Comb repr a -> Comb repr a
  Ref :: Bool -> TH.Name -> Comb repr a
infixl 3 :<|>
infixl 4 :<*>
infixl 4 :<*, :*>

pattern (:<$>) :: TermGrammar (a -> b) -> Comb repr a -> Comb repr b
pattern x :<$> p = Pure x :<*> p
pattern (:$>) :: Comb repr a -> TermGrammar b -> Comb repr b
pattern (:<$) :: TermGrammar a -> Comb repr b -> Comb repr a
pattern p :$> x = p :*> Pure x
pattern x :<$ p = Pure x :<* p
infixl 4 :<$>, :<$, :$>

{-
pattern (:*>) :: Comb repr a -> Comb repr b -> Comb repr b
pattern (:<*) :: Comb repr a -> Comb repr b -> Comb repr a
pattern x :<* p = H.Const :<$> x :<*> p
pattern p :*> x = H.Id :<$ p :<*> x
x .<* p = H.const :<$> x :<*> p
x .<$ p = Pure x .<* p
p .*> x = H.id .<$ p :<*> x
p .$> x = p .*> Pure x
-}

{-
pattern (:<$>) :: Defunc (a -> b) -> Fix Combinator a -> Combinator (Fix Combinator) b
pattern f :<$> p = (Pure f) :<*> p
pattern (:$>) :: Fix Combinator a -> Defunc b -> Combinator (Fix Combinator) b
pattern p :$> x = p :*> (Pure x)
pattern (:<$) :: Defunc a -> Fix Combinator b -> Combinator (Fix Combinator) a
pattern x :<$ p = (Pure x) :<* p
-}


instance Applicable (Comb repr) where
  pure = Pure
  (<*>) = (:<*>)
  (<*) = (:<*)
  (*>) = (:*>)
instance Alternable (Comb repr) where
  (<|>) = (:<|>)
  empty = Empty
  try = Try
instance Selectable (Comb repr) where
  branch = Branch
instance Matchable (Comb repr) where
  conditional = Match
instance Foldable (Comb repr) where
  chainPre = ChainPre
  chainPost = ChainPost
instance Satisfiable repr tok => Satisfiable (Comb repr) tok where
  satisfy = Satisfy
instance Lookable (Comb repr) where
  look = Look
  negLook = NegLook
  eof = Eof
instance Letable TH.Name (Comb repr) where
  def = Def
  ref = Ref
instance MakeLetName TH.Name where
  makeLetName _ = TH.qNewName "name"

-- Pattern-matchable 'Comb'inators keep enough structure
-- to have some of the symantics producing them interpreted again
-- (eg. after being modified by 'optimizeGrammar').
type instance Output (Comb repr) = repr
instance
  ( Applicable repr
  , Alternable repr
  , Selectable repr
  , Foldable repr
  , Lookable repr
  , Matchable repr
  , Letable TH.Name repr
  ) => Trans (Comb repr) repr where
  trans = \case
    Pure a -> pure (H.optimizeTerm a)
    Satisfy es p -> satisfy es p
    Item -> item
    Try x -> try (trans x)
    Look x -> look (trans x)
    NegLook x -> negLook (trans x)
    Eof -> eof
    x :<* y -> trans x <* trans y
    x :*> y -> trans x *> trans y
    x :<*> y -> trans x <*> trans y
    x :<|> y -> trans x <|> trans y
    Empty -> empty
    Branch lr l r -> branch (trans lr) (trans l) (trans r)
    Match a ps bs b -> conditional (trans a) ps (trans Functor.<$> bs) (trans b)
    ChainPre x y -> chainPre (trans x) (trans y)
    ChainPost x y -> chainPost (trans x) (trans y)
    Def n x -> def n (trans x)
    Ref r n -> ref r n

{-
-- * Type 'OptimizeHaskell'
newtype OptimizeHaskell letName repr a =
        OptimizeHaskell { unOptimizeHaskell :: Comb repr a }
instance
  Letable letName (Comb repr) =>
  Letable letName (OptimizeGrammar letName repr)
instance Comb.Applicable (OptimizeGrammar letName repr) where
  pure a = pure (optimizeTerm a)
instance Comb.Alternable (OptimizeGrammar letName repr)
instance Comb.Satisfiable repr tok =>
         Comb.Satisfiable (OptimizeGrammar letName repr) tok
instance Comb.Selectable (OptimizeGrammar letName repr)
instance Comb.Matchable (OptimizeGrammar letName repr)
instance Comb.Lookable (OptimizeGrammar letName repr)
instance Comb.Foldable (OptimizeGrammar letName repr)
-}

-- * Type 'OptimizeGrammar'
-- | Bottom-up application of 'optimizeCombNode'.
newtype OptimizeGrammar letName repr a =
        OptimizeGrammar { unOptimizeGrammar :: Comb repr a }

optimizeGrammar ::
  Trans (OptimizeGrammar TH.Name repr) repr =>
  OptimizeGrammar TH.Name repr a -> repr a
optimizeGrammar = trans
instance
  Trans (Comb repr) repr =>
  Trans (OptimizeGrammar letName repr) repr where
  trans = trans . unOptimizeGrammar

type instance Output (OptimizeGrammar _letName repr) = Comb repr
instance Trans (OptimizeGrammar letName repr) (Comb repr) where
  trans = unOptimizeGrammar
instance Trans (Comb repr) (OptimizeGrammar letName repr) where
  trans = OptimizeGrammar . optimizeCombNode
instance Trans1 (Comb repr) (OptimizeGrammar letName repr)
instance Trans2 (Comb repr) (OptimizeGrammar letName repr)
instance Trans3 (Comb repr) (OptimizeGrammar letName repr)

instance
  Letable letName (Comb repr) =>
  Letable letName (OptimizeGrammar letName repr) where
  -- Disable useless calls to 'optimizeCombNode'
  -- because 'Def' or 'Ref' have no matching in it.
  def n = OptimizeGrammar . def n . unOptimizeGrammar
  ref r n = OptimizeGrammar (ref r n)
instance Comb.Applicable (OptimizeGrammar letName repr)
instance Comb.Alternable (OptimizeGrammar letName repr)
instance Comb.Satisfiable repr tok =>
         Comb.Satisfiable (OptimizeGrammar letName repr) tok
instance Comb.Selectable (OptimizeGrammar letName repr)
instance Comb.Matchable (OptimizeGrammar letName repr)
instance Comb.Lookable (OptimizeGrammar letName repr)
instance Comb.Foldable (OptimizeGrammar letName repr)


optimizeCombNode :: Comb repr a -> Comb repr a

----------------------------------------------
-- Destructive optimizations
----------------------------------------------

optimizeCombNode (Empty :<*> _) =
  -- trace "App Right Absorption Law" $
  Empty
optimizeCombNode (u :<*> Empty) =
  -- trace "App Failure Weakening Law" $
  optimizeCombNode (u :*> Empty)
optimizeCombNode (Empty :*> _) =
  -- trace "App Right Absorption Law" $
  Empty
optimizeCombNode (Empty :<* _) =
  -- trace "App Right Absorption Law" $
  Empty
optimizeCombNode (u :<* Empty) =
  -- trace "App Failure Weakening Law" $
  optimizeCombNode (u :*> Empty)
optimizeCombNode (Branch Empty _ _) =
  -- trace "Branch Absorption Law" $
  Empty
optimizeCombNode (Branch b Empty Empty) =
  -- trace "Branch Weakening Law" $
  optimizeCombNode (b :*> Empty)
optimizeCombNode (Match Empty _ _ d) =
  -- trace "Match Absorption Law" $
  d
optimizeCombNode (Match p _ qs Empty)
  | Foldable.all (\case {Empty -> True; _ -> False}) qs =
  -- trace "Match Weakening Law" $
  optimizeCombNode (p :*> Empty)


----------------------------------------------
-- Applicative optimizations
----------------------------------------------

{- Those laws require to pattern match on some singled-out pure constructors,
 - but 'optimizeHaskellNode' is normalizing them using lambda abstractions
 - and thus they will no longer match.

optimizeCombNode (H.Id :<$> u) =
  -- trace "Identity Law" $
  u
optimizeCombNode ((H.Flip H.:@ H.Const) :<$> u) =
  -- trace "Flip Const Optimisation" $
  optimizeCombNode (u :*> Pure H.id)
optimizeCombNode (((H.Flip H.:@ H.Const) :<$> p) :<*> q) =
  -- trace "Definition of *>" $
  p :*> q
optimizeCombNode ((H.Const :<$> p) :<*> q) =
  -- trace "Definition of <*" $
  p :<* q
-}
optimizeCombNode (f :<$> Pure x) =
  -- trace "Homomorphism Law" $
  Pure (f H..@ x)
optimizeCombNode (f :<$> (g :<$> p)) =
  -- NOTE: This is basically a shortcut, it can be caught by the Composition Law and Homomorphism Law
  -- trace "Functor Composition Law" $
  optimizeCombNode ((H..) H..@ f H..@ g :<$> p)
optimizeCombNode (u :<*> (v :<*> w)) =
  -- trace "Composition Law" $
  optimizeCombNode (optimizeCombNode (optimizeCombNode ((H..) :<$> u) :<*> v) :<*> w)
optimizeCombNode ((u :*> v) :<*> w) =
  -- trace "Reassociation Law 1" $
  optimizeCombNode (u :*> (optimizeCombNode (v :<*> w)))
optimizeCombNode (u :<*> (Pure x)) =
  -- trace "Interchange Law" $
  optimizeCombNode (H.flip H..@ (H.$) H..@ x :<$> u)
optimizeCombNode ((_ :<$> p) :*> q) =
  -- trace "Right Absorption Law" $
  p :*> q
optimizeCombNode (p :<* (_ :<$> q)) =
  -- trace "Left Absorption Law"
  p :<* q
optimizeCombNode (u :<*> (v :<* w)) =
  -- trace "Reassociation Law 2" $
  optimizeCombNode (optimizeCombNode (u :<*> v) :<* w)
optimizeCombNode (u :<*> (v :$> x)) =
  -- trace "Reassociation Law 3" $
  optimizeCombNode (optimizeCombNode (u :<*> Pure x) :<* v)

----------------------------------------------
-- Alternative optimizations
----------------------------------------------

optimizeCombNode (p@Pure{} :<|> _) =
  -- trace "Left Catch Law" $
  p
optimizeCombNode (Empty :<|> u) =
  -- trace "Left Neutral Law" $
  u
optimizeCombNode (u :<|> Empty) =
  -- trace "Right Neutral Law" $
  u
optimizeCombNode ((u :<|> v) :<|> w) =
  -- trace "Associativity Law" $
  u :<|> optimizeCombNode (v :<|> w)

----------------------------------------------
-- Sequencing optimizations
----------------------------------------------

optimizeCombNode ((Pure _) :*> u) =
  -- trace "Identity Law" $
  u
optimizeCombNode ((u :$> _) :*> v) =
  -- trace "Identity Law" $
  u :*> v
optimizeCombNode (u :*> (v :*> w)) =
  -- trace "Associativity Law" $
  optimizeCombNode (optimizeCombNode (u :*> v) :*> w)
optimizeCombNode (u :<* (Pure _)) =
  -- trace "Identity Law" $
  u
optimizeCombNode (u :<* (v :$> _)) =
  -- trace "Identity Law" $
  optimizeCombNode (u :<* v)
optimizeCombNode (x :<$ u) =
  -- trace "Commutativity Law" $
  optimizeCombNode (u :$> x)
optimizeCombNode ((u :<* v) :<* w) =
  -- trace "Associativity Law" $
  optimizeCombNode (u :<* optimizeCombNode (v :<* w))
optimizeCombNode (Look p@Pure{}) =
  -- trace "Pure Look Law" $
  p
optimizeCombNode (Look p@Empty) =
  -- trace "Dead Look Law" $
  p
optimizeCombNode (NegLook Pure{}) =
  -- trace "Pure Negative-Look" $
  Empty
optimizeCombNode (NegLook Empty) =
  -- trace "Dead Negative-Look" $
  Pure H.unit
optimizeCombNode (NegLook (NegLook p)) =
  -- trace "Double Negation Law" $
  optimizeCombNode (Look (Try p :*> Pure H.unit))
optimizeCombNode (NegLook (Try p)) =
  -- trace "Zero Consumption Law" $
  optimizeCombNode (NegLook p)
optimizeCombNode (Look (Look p)) =
  -- trace "Idempotence Law" $
  Look p
optimizeCombNode (NegLook (Look p)) =
  -- trace "Right Identity Law" $
  optimizeCombNode (NegLook p)
optimizeCombNode (Look (NegLook p)) =
  -- trace "Left Identity Law" $
  NegLook p
optimizeCombNode (NegLook (Try p :<|> q)) =
  -- trace "Transparency Law" $
  optimizeCombNode (optimizeCombNode (NegLook p) :*> optimizeCombNode (NegLook q))
optimizeCombNode (Look p :<|> Look q) =
  -- trace "Distributivity Law" $
  optimizeCombNode (Look (optimizeCombNode ((Try p) :<|> q)))
optimizeCombNode (Look (p :$> x)) =
  -- trace "Interchange Law" $
  optimizeCombNode (optimizeCombNode (Look p) :$> x)
optimizeCombNode (Look (f :<$> p)) =
  -- trace "Interchange Law" $
  optimizeCombNode (f :<$> optimizeCombNode (Look p))
optimizeCombNode (p :<*> NegLook q) =
  -- trace "Absorption Law" $
  optimizeCombNode (optimizeCombNode (p :<*> Pure H.unit) :<* NegLook q)
optimizeCombNode (NegLook ((p :$> _))) =
  -- trace "NegLookIdempotence Law" $
  optimizeCombNode (NegLook p)
optimizeCombNode (NegLook ((_ :<$> p))) =
  -- trace "NegLook Idempotence Law" $
  optimizeCombNode (NegLook p)
optimizeCombNode (Try (p :$> x)) =
  -- trace "Try Interchange Law" $
  optimizeCombNode (optimizeCombNode (Try p) :$> x)
optimizeCombNode (Try (f :<$> p)) =
  -- trace "Try Interchange Law" $
  optimizeCombNode (f :<$> optimizeCombNode (Try p))
optimizeCombNode (Branch (Pure (trans -> lr)) l r) =
  -- trace "Branch Pure Left/Right Law" $
  case H.value lr of
    Left value -> optimizeCombNode (l :<*> Pure (trans H.ValueCode{..}))
      where code = [|| case $$(H.code lr) of Left x -> x ||]
    Right value -> optimizeCombNode (r :<*> Pure (trans H.ValueCode{..}))
      where code = [|| case $$(H.code lr) of Right x -> x ||]
optimizeCombNode (Branch b (Pure (trans -> l)) (Pure (trans -> r))) =
  -- trace "Branch Generalised Identity Law" $
  optimizeCombNode (trans H.ValueCode{..} :<$> b)
  where
  value = either (H.value l) (H.value r)
  code = [|| either $$(H.code l) $$(H.code r) ||]
optimizeCombNode (Branch (x :*> y) p q) =
  -- trace "Interchange Law" $
  optimizeCombNode (x :*> optimizeCombNode (Branch y p q))
optimizeCombNode (Branch b l Empty) =
  -- trace "Negated Branch Law" $
  Branch (Pure (trans (H.ValueCode{..})) :<*> b) Empty l
  where
  value = either Right Left
  code = [||either Right Left||]
optimizeCombNode (Branch (Branch b Empty (Pure (trans -> lr))) Empty br) =
  -- trace "Branch Fusion Law" $
  optimizeCombNode (Branch (optimizeCombNode (Pure (trans H.ValueCode{..}) :<*> b)) Empty br)
  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 ||]
optimizeCombNode (f :<$> Branch b l r) =
  -- trace "Branch Distributivity Law" $
  optimizeCombNode (Branch b (optimizeCombNode ((H..) H..@ f :<$> l))
                             (optimizeCombNode ((H..) H..@ f :<$> r)))
optimizeCombNode (Match a _ps bs Empty)
  | Foldable.all (\case { Empty -> True; _ -> False }) bs =
    -- trace "Match Weakening Law" $
    optimizeCombNode (a :*> Empty)
optimizeCombNode (Match (Pure (trans -> a)) ps bs d) =
  -- trace "Match Pure Law" $
  Foldable.foldr (\(trans -> p, b) next ->
    if H.value p (H.value a) then b else next
  ) d (List.zip ps bs)
optimizeCombNode (f :<$> Match a ps bs d) =
  -- trace "Match Distributivity Law" $
  Match a ps (optimizeCombNode . (f :<$>) Functor.<$> bs)
            (optimizeCombNode (f :<$> d))

optimizeCombNode x = x