{-# 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.Foldable (all, foldr)
import Data.Function ((.))
import Data.Kind (Type)
import qualified Data.Functor as Functor
import qualified Data.List as List
import qualified Language.Haskell.TH.Syntax as TH

import Symantic.Parser.Grammar.Combinators as Comb
import Symantic.Parser.Staging (ValueCode(..), Value(..), getValue, code)
import Symantic.Univariant.Letable
import Symantic.Univariant.Trans
import qualified Symantic.Parser.Staging 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 'DumpComb' or 'Instr'uctions).
--
-- 2. Avoid overlapping instances between
--    @('Trans' ('Comb' repr) repr)@ and
--    @('Trans' ('Comb' repr) ('OptimizeComb' letName repr))@
data Comb (repr :: Type -> Type) a where
  Pure :: H.Haskell a -> Comb repr a
  Satisfy ::
    Satisfiable repr tok =>
    [ErrorItem tok] ->
    H.Haskell (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 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 =>
    [H.Haskell (a -> Bool)] ->
    [Comb repr b] -> Comb repr a -> 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

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

infixl 3 :<|>
infixl 4 :<*>, :<*, :*>
infixl 4 :<$>, :<$, :$>

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 'optimizeComb').
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 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
    Empty -> empty
    Branch lr l r -> branch (trans lr) (trans l) (trans r)
    Match ps bs a b -> conditional ps (trans Functor.<$> bs) (trans a) (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 'OptimizeComb'
-- Bottom-up application of 'optimizeCombNode'.
newtype OptimizeComb letName repr a =
        OptimizeComb { unOptimizeComb :: Comb repr a }

optimizeComb ::
  Trans (OptimizeComb TH.Name repr) repr =>
  OptimizeComb TH.Name repr a -> repr a
optimizeComb = trans
instance
  Trans (Comb repr) repr =>
  Trans (OptimizeComb letName repr) repr where
  trans = trans . unOptimizeComb

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

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

optimizeCombNode :: Comb repr a -> Comb repr a
optimizeCombNode = \case
  -- Functor Identity Law
  H.Id :<$> x ->
    -- trace "Functor Identity Law" $
    x
  -- Functor Commutativity Law
  x :<$ u ->
    -- trace "Functor Commutativity Law" $
    optimizeCombNode (u :$> x)
  -- Functor Flip Const Law
  H.Flip H.:@ H.Const :<$> u ->
    -- trace "Functor Flip Const Law" $
    optimizeCombNode (u :*> Pure H.Id)
  -- Functor Homomorphism Law
  f :<$> Pure x ->
    -- trace "Functor Homomorphism Law" $
    Pure (f H..@ x)

  -- App Right Absorption Law
  Empty :<*> _ ->
    -- trace "App Right Absorption Law" $
    Empty
  _ :<*> Empty ->
    -- In Parsley: this is only a weakening to u :*> Empty
    -- but here :*> is an alias to :<*>
    -- hence it would loop on itself forever.
    -- trace "App Left Absorption Law" $
    Empty
  -- App Composition Law
  u :<*> (v :<*> w) ->
    -- trace "App Composition Law" $
    optimizeCombNode (optimizeCombNode (optimizeCombNode ((H.:.) :<$> u) :<*> v) :<*> w)
  -- App Interchange Law
  u :<*> Pure x ->
    -- trace "App Interchange Law" $
    optimizeCombNode (H.Flip H..@ (H.:$) H..@ x :<$> u)
  -- App Left Absorption Law
  p :<* (_ :<$> q) ->
    -- trace "App Left Absorption Law" $
    p :<* q
  -- App Right Absorption Law
  (_ :<$> p) :*> q ->
    -- trace "App Right Absorption Law" $
    p :*> q
  -- App Pure Left Identity Law
  Pure _ :*> u ->
    -- trace "App Pure Left Identity Law" $
    u
  -- App Functor Left Identity Law
  (u :$> _) :*> v ->
    -- trace "App Functor Left Identity Law" $
    u :*> v
  -- App Pure Right Identity Law
  u :<* Pure _ ->
    -- trace "App Pure Right Identity Law" $
    u
  -- App Functor Right Identity Law
  u :<* (v :$> _) ->
    -- trace "App Functor Right Identity Law" $
    optimizeCombNode (u :<* v)
  -- App Left Associativity Law
  (u :<* v) :<* w ->
    -- trace "App Left Associativity Law" $
    optimizeCombNode (u :<* optimizeCombNode (v :<* w))

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

  -- Look Pure Law
  Look p@Pure{} ->
    -- trace "Look Pure Law" $
    p
  -- Look Empty Law
  Look p@Empty ->
    -- trace "Look Empty Law" $
    p
  -- NegLook Pure Law
  NegLook Pure{} ->
    -- trace "NegLook Pure Law" $
    Empty
  -- NegLook Empty Law
  NegLook Empty ->
    -- trace "NegLook Dead Law" $
    Pure H.unit
  -- NegLook Double Negation Law
  NegLook (NegLook p) ->
    -- trace "NegLook Double Negation Law" $
    optimizeCombNode (Look (Try p) :*> Pure H.unit)
  -- NegLook Zero Consumption Law
  NegLook (Try p) ->
    -- trace "NegLook Zero Consumption Law" $
    optimizeCombNode (NegLook p)
  -- Idempotence Law
  Look (Look p) ->
    -- trace "Look Idempotence Law" $
    Look p
  -- Look Right Identity Law
  NegLook (Look p) ->
    -- trace "Look Right Identity Law" $
    optimizeCombNode (NegLook p)
  -- Look Left Identity Law
  Look (NegLook p) ->
    -- trace "Look Left Identity Law" $
    NegLook p
  -- NegLook Transparency Law
  NegLook (Try p :<|> q) ->
    -- trace "NegLook Transparency Law" $
    optimizeCombNode (optimizeCombNode (NegLook p) :*> optimizeCombNode (NegLook q))
  -- Look Distributivity Law
  Look p :<|> Look q ->
    -- trace "Look Distributivity Law" $
    optimizeCombNode (Look (optimizeCombNode (Try p :<|> q)))
  -- Look Interchange Law
  Look (f :<$> p) ->
    -- trace "Look Interchange Law" $
    optimizeCombNode (f :<$> optimizeCombNode (Look p))
  -- NegLook Idempotence Right Law
  NegLook (_ :<$> p) ->
    -- trace "NegLook Idempotence Law" $
    optimizeCombNode (NegLook p)
  -- Try Interchange Law
  Try (f :<$> p) ->
    -- trace "Try Interchange Law" $
    optimizeCombNode (f :<$> optimizeCombNode (Try p))

  -- Branch Absorption Law
  Branch Empty _ _ ->
    -- trace "Branch Absorption Law" $
    empty
  -- Branch Weakening Law
  Branch b Empty Empty ->
    -- trace "Branch Weakening Law" $
    optimizeCombNode (b :*> Empty)
  -- Branch Pure Left/Right Laws
  Branch (Pure (trans -> lr)) l r ->
    -- trace "Branch Pure Left/Right Law" $
    case getValue lr of
     Left v -> optimizeCombNode (l :<*> Pure (H.Haskell (ValueCode (Value v) c)))
      where c = [|| case $$(code lr) of Left x -> x ||]
     Right v -> optimizeCombNode (r :<*> Pure (H.Haskell (ValueCode (Value v) c)))
      where c = [|| case $$(code lr) of Right x -> x ||]
  -- Branch Generalised Identity Law
  Branch b (Pure (trans -> l)) (Pure (trans -> r)) ->
    -- trace "Branch Generalised Identity Law" $
    optimizeCombNode (H.Haskell (ValueCode v c) :<$> b)
    where
    v = Value (either (getValue l) (getValue r))
    c = [|| either $$(code l) $$(code r) ||]
  -- Branch Interchange Law
  Branch (x :*> y) p q ->
    -- trace "Branch Interchange Law" $
    optimizeCombNode (x :*> optimizeCombNode (Branch y p q))
  -- Branch Empty Right Law
  Branch b l Empty ->
    -- trace " Branch Empty Right Law" $
    Branch (Pure (H.Haskell (ValueCode v c)) :<*> b) Empty l
    where
    v = Value (either Right Left)
    c = [||either Right Left||]
  -- Branch Fusion Law
  Branch (Branch b Empty (Pure (trans -> lr))) Empty br ->
    -- trace "Branch Fusion Law" $
    optimizeCombNode (Branch (optimizeCombNode (Pure (H.Haskell (ValueCode (Value v) c)) :<*> b))
                             Empty br)
    where
    v Left{} = Left ()
    v (Right r) = case getValue lr r of
                   Left _ -> Left ()
                   Right rr -> Right rr
    c = [|| \case Left{} -> Left ()
                  Right r -> case $$(code lr) r of
                              Left _ -> Left ()
                              Right rr -> Right rr ||]
  -- Branch Distributivity Law
  f :<$> Branch b l r ->
    -- trace "Branch Distributivity Law" $
    optimizeCombNode (Branch b (optimizeCombNode ((H..@) (H..) f :<$> l))
                               (optimizeCombNode ((H..@) (H..) f :<$> r)))

  -- Match Absorption Law
  Match _ _ Empty d ->
    -- trace "Match Absorption Law" $
    d
  -- Match Weakening Law
  Match _ bs a Empty
    | all (\case {Empty -> True; _ -> False}) bs ->
      -- trace "Match Weakening Law" $
      optimizeCombNode (a :*> Empty)
  -- Match Pure Law
  Match ps bs (Pure (trans -> a)) d ->
    -- trace "Match Pure Law" $
    foldr (\(trans -> p, b) next ->
      if getValue p (getValue a) then b else next
    ) d (List.zip ps bs)
  -- Match Distributivity Law
  f :<$> Match ps bs a d ->
    -- trace "Match Distributivity Law" $
    Match ps (optimizeCombNode . (f :<$>) Functor.<$> bs) a
             (optimizeCombNode (f :<$> d))

  {- Possibly useless laws to be tested
  Empty  :*> _ -> Empty
  Empty :<*  _ -> Empty
  -- App Definition of *> Law
  H.Flip H..@ H.Const :<$> p :<*> q ->
    -- -- trace "EXTRALAW: App Definition of *> Law" $
    p :*> q
  -- App Definition of <* Law
  H.Const :<$> p :<*> q ->
    -- -- trace "EXTRALAW: App Definition of <* Law" $
    p :<* q

  -- Functor Composition Law
  -- (a shortcut that could also have been be caught
  -- by the Composition Law and Homomorphism Law)
  f :<$> (g :<$> p) ->
    -- -- trace "EXTRALAW: Functor Composition Law" $
    optimizeCombNode ((H.:.) H..@ f H..@ g :<$> p)
  -- Applicable Failure Weakening Law
  u :<*  Empty ->
    -- -- trace "EXTRALAW: App Failure Weakening Law" $
    optimizeCombNode (u :*> Empty)
  Try (p :$> x) ->
    -- -- trace "EXTRALAW: Try Interchange Right Law" $
    optimizeCombNode (optimizeCombNode (Try p) :$> x)
  -- App Reassociation Law 1
  (u :*> v) :<*> w ->
    -- -- trace "EXTRALAW: App Reassociation Law 1" $
    optimizeCombNode (u :*> optimizeCombNode (v :<*> w))
  -- App Reassociation Law 2
  u :<*> (v :<* w) ->
    -- -- trace "EXTRALAW: App Reassociation Law 2" $
    optimizeCombNode (optimizeCombNode (u :<*> v) :<* w)
  -- App Right Associativity Law
  u :*> (v :*> w) ->
    -- -- trace "EXTRALAW: App Right Associativity Law" $
    optimizeCombNode (optimizeCombNode (u :*> v) :*> w)
  -- App Reassociation Law 3
  u :<*> (v :$> x) ->
    -- -- trace "EXTRALAW: App Reassociation Law 3" $
    optimizeCombNode (optimizeCombNode (u :<*> Pure x) :<* v)

  Look (p :$> x) ->
    optimizeCombNode (optimizeCombNode (Look p) :$> x)
  NegLook (p :$> _) -> optimizeCombNode (NegLook p)

  -- NegLook Absorption Law
  p :<*> NegLook q ->
    -- trace "EXTRALAW: Neglook Absorption Law" $
    optimizeCombNode (optimizeCombNode (p :<*> Pure H.unit) :<* NegLook q)
    -- Infinite loop, because :<* expands to :<*>
  -}

  x -> x