{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
module Symantic.Parser.Grammar.Optimize where

import Data.Bool (Bool(..))
import Data.Char (Char)
import Data.Either (Either(..), either)
import Data.Eq (Eq(..))
import Data.Foldable (all, foldr)
import Data.Function ((.))
import Debug.Trace (trace)
import Data.Function (($))
import qualified Data.Functor as Functor
import qualified Data.List as List

import Symantic.Parser.Grammar.Combinators as Comb
import Symantic.Parser.Staging (ValueCode(..), Value(..),  Code(..), getValue, getCode)
import Symantic.Univariant.Letable
import Symantic.Univariant.Trans
import qualified Language.Haskell.TH.Syntax as TH
import qualified Symantic.Parser.Staging as Hask

-- * Type 'Grammar'
data Grammar a where
  Pure :: Hask.Haskell a -> Grammar a
  Satisfy :: Hask.Haskell (Char -> Bool) -> Grammar Char
  Item :: Grammar Char
  Try :: Grammar a -> Grammar a
  Look :: Grammar a -> Grammar a
  NegLook :: Grammar a -> Grammar ()
  (:<*>) :: Grammar (a -> b) -> Grammar a -> Grammar b
  (:<|>) :: Grammar a -> Grammar a -> Grammar a
  Empty :: Grammar a
  Branch :: Grammar (Either a b) -> Grammar (a -> c) -> Grammar (b -> c) -> Grammar c
  Match :: Eq a => [Hask.Haskell (a -> Bool)] -> [Grammar b] -> Grammar a -> Grammar b -> Grammar b
  ChainPre :: Grammar (a -> a) -> Grammar a -> Grammar a
  ChainPost :: Grammar a -> Grammar (a -> a) -> Grammar a
  Def :: TH.Name -> Grammar a -> Grammar a
  Ref :: Bool -> TH.Name -> Grammar a

pattern (:<$>) :: Hask.Haskell (a -> b) -> Grammar a -> Grammar b
pattern (:$>) :: Grammar a -> Hask.Haskell b -> Grammar b
pattern (:<$) :: Hask.Haskell a -> Grammar b -> Grammar a
pattern (:*>) :: Grammar a -> Grammar b -> Grammar b
pattern (:<*) :: Grammar a -> Grammar b -> Grammar a
pattern x :<$> p = Pure x :<*> p
pattern p :$> x = p :*> Pure x
pattern x :<$ p = Pure x :<* p
pattern x :<* p = Hask.Const :<$> x :<*> p
pattern p :*> x = Hask.Id :<$ p :<*> x

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

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

instance Letable letName repr =>
         Letable letName (Any repr)
instance
  ( Applicable repr
  , Alternable repr
  , Selectable repr
  , Foldable repr
  , Charable repr
  , Lookable repr
  , Matchable repr
  , Letable TH.Name repr
  ) =>
  Trans Grammar (Any repr) where
  trans = \case
    Pure a -> pure a
    Satisfy p -> satisfy p
    Item -> item
    Try x -> try (trans x)
    Look x -> look (trans x)
    NegLook x -> negLook (trans x)
    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 'OptimizeGrammar'
-- Bottom-up application of 'optimizeGrammarNode'.
newtype OptimizeGrammar letName a = OptimizeGrammar { unOptimizeGrammar ::
  Grammar a }

optimizeGrammar :: OptimizeGrammar TH.Name a -> Grammar a
optimizeGrammar = unOptimizeGrammar

type instance Output (OptimizeGrammar letName) = Grammar
instance Trans Grammar (OptimizeGrammar letName) where
  trans = OptimizeGrammar . optimizeGrammarNode
instance Trans1 Grammar (OptimizeGrammar letName)
instance Trans2 Grammar (OptimizeGrammar letName)
instance Trans3 Grammar (OptimizeGrammar letName)
instance Trans (OptimizeGrammar letName) Grammar where
  trans = unOptimizeGrammar

instance
  Letable letName Grammar =>
  Letable letName (OptimizeGrammar letName) where
  -- Disable useless calls to 'optimizeGrammarNode'
  -- 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)
instance Comb.Alternable (OptimizeGrammar letName)
instance Comb.Charable (OptimizeGrammar letName)
instance Comb.Selectable (OptimizeGrammar letName)
instance Comb.Matchable (OptimizeGrammar letName)
instance Comb.Lookable (OptimizeGrammar letName)
instance Comb.Foldable (OptimizeGrammar letName)

optimizeGrammarNode :: Grammar a -> Grammar a
optimizeGrammarNode = \case
  -- Pure merge optimisation
  -- Pure x :<*> Pure y -> Pure (x Hask.:@ y)

  -- Functor Identity Law
  Hask.Id :<$> x ->
    trace "Functor Identity Law" $
    x
  -- Functor Commutativity Law
  x :<$ u ->
    trace "Functor Commutativity Law" $
    optimizeGrammarNode (u :$> x)
  -- Functor Flip Const Law
  Hask.Flip Hask.:@ Hask.Const :<$> u ->
    trace "Functor Flip Const Law" $
    optimizeGrammarNode (u :*> Pure Hask.Id)
  -- Functor Homomorphism Law
  f :<$> Pure x ->
    trace "Functor Homomorphism Law" $
    Pure (f Hask.:@ 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" $
    optimizeGrammarNode (optimizeGrammarNode (optimizeGrammarNode ((Hask.:.) :<$> u) :<*> v) :<*> w)
  -- App Interchange Law
  u :<*> Pure x ->
    trace "App Interchange Law" $
    optimizeGrammarNode (Hask.Flip Hask.:@ (Hask.:$) Hask.:@ 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" $
    optimizeGrammarNode (u :<* v)
  -- App Left Associativity Law
  (u :<* v) :<* w ->
    trace "App Left Associativity Law" $
    optimizeGrammarNode (u :<* optimizeGrammarNode (v :<* w))

  -- Alt Left Catch Law
  p@Pure{} :<|> _ ->
    trace "Alt Left Catch 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 :<|> optimizeGrammarNode (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 Hask.unit
  -- NegLook Double Negation Law
  NegLook (NegLook p) ->
    trace "NegLook Double Negation Law" $
    optimizeGrammarNode (Look (Try p) :*> Pure Hask.unit)
  -- NegLook Zero Consumption Law
  NegLook (Try p) ->
    trace "NegLook Zero Consumption Law" $
    optimizeGrammarNode (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" $
    optimizeGrammarNode (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" $
    optimizeGrammarNode (optimizeGrammarNode (NegLook p) :*> optimizeGrammarNode (NegLook q))
  -- Look Distributivity Law
  Look p :<|> Look q ->
    trace "Look Distributivity Law" $
    optimizeGrammarNode (Look (optimizeGrammarNode (Try p :<|> q)))
  -- Look Interchange Law
  Look (f :<$> p) ->
    trace "Look Interchange Law" $
    optimizeGrammarNode (f :<$> optimizeGrammarNode (Look p))
  -- NegLook Absorption Law
  p :<*> NegLook q ->
    trace "Neglook Absorption Law" $
    optimizeGrammarNode (optimizeGrammarNode (p :<*> Pure Hask.unit) :<* NegLook q)
  -- NegLook Idempotence Right Law
  NegLook (_ :<$> p) ->
    trace "NegLook Idempotence Law" $
    optimizeGrammarNode (NegLook p)
  -- Try Interchange Law
  Try (f :<$> p) ->
    trace "Try Interchange Law" $
    optimizeGrammarNode (f :<$> optimizeGrammarNode (Try p))

  -- Branch Absorption Law
  Branch Empty _ _ ->
    trace "Branch Absorption Law" $
    empty
  -- Branch Weakening Law
  Branch b Empty Empty ->
    trace "Branch Weakening Law" $
    optimizeGrammarNode (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 -> optimizeGrammarNode (l :<*> Pure (Hask.Haskell (ValueCode (Value v) c)))
      where c = Code [|| case $$(getCode lr) of Left x -> x ||]
     Right v -> optimizeGrammarNode (r :<*> Pure (Hask.Haskell (ValueCode (Value v) c)))
      where c = Code [|| case $$(getCode lr) of Right x -> x ||]
  -- Branch Generalised Identity Law
  Branch b (Pure (trans -> l)) (Pure (trans -> r)) ->
    trace "Branch Generalised Identity Law" $
    optimizeGrammarNode (Hask.Haskell (ValueCode v c) :<$> b)
    where
    v = Value (either (getValue l) (getValue r))
    c = Code [|| either $$(getCode l) $$(getCode r) ||]
  -- Branch Interchange Law
  Branch (x :*> y) p q ->
    trace "Branch Interchange Law" $
    optimizeGrammarNode (x :*> optimizeGrammarNode (Branch y p q))
  -- Branch Empty Right Law
  Branch b l Empty ->
    trace " Branch Empty Right Law" $
    Branch (Pure (Hask.Haskell (ValueCode v c)) :<*> b) Empty l
    where
    v = Value (either Right Left)
    c = Code [||either Right Left||]
  -- Branch Fusion Law
  Branch (Branch b Empty (Pure (trans -> lr))) Empty br ->
    trace "Branch Fusion Law" $
    optimizeGrammarNode (Branch (optimizeGrammarNode (Pure (Hask.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 = Code [|| \case Left{} -> Left ()
                       Right r -> case $$(getCode lr) r of
                                   Left _ -> Left ()
                                   Right rr -> Right rr ||]
  -- Branch Distributivity Law
  f :<$> Branch b l r ->
    trace "Branch Distributivity Law" $
    optimizeGrammarNode (Branch b (optimizeGrammarNode ((Hask..@) (Hask..) f :<$> l)) (optimizeGrammarNode ((Hask..@) (Hask..) 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" $
      optimizeGrammarNode (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 (optimizeGrammarNode . (f :<$>) Functor.<$> bs) a (optimizeGrammarNode (f :<$> d))

  {- Possibly useless laws to be tested
  Empty  :*> _ -> Empty
  Empty :<*  _ -> Empty
  -- App Definition of *> Law
  Hask.Flip Hask.:@ Hask.Const :<$> p :<*> q ->
    trace "EXTRALAW: App Definition of *> Law" $
    p :*> q
  -- App Definition of <* Law
  Hask.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" $
    optimizeGrammarNode ((Hask.:.) Hask.:@ f Hask.:@ g :<$> p)
  -- Applicable Failure Weakening Law
  u :<*  Empty ->
    trace "EXTRALAW: App Failure Weakening Law" $
    optimizeGrammarNode (u :*> Empty)
  Try (p :$> x) ->
    trace "EXTRALAW: Try Interchange Right Law" $
    optimizeGrammarNode (optimizeGrammarNode (Try p) :$> x)
  -- App Reassociation Law 1
  (u :*> v) :<*> w ->
    trace "EXTRALAW: App Reassociation Law 1" $
    optimizeGrammarNode (u :*> optimizeGrammarNode (v :<*> w))
  -- App Reassociation Law 2
  u :<*> (v :<* w) ->
    trace "EXTRALAW: App Reassociation Law 2" $
    optimizeGrammarNode (optimizeGrammarNode (u :<*> v) :<* w)
  -- App Right Associativity Law
  u :*> (v :*> w) ->
    trace "EXTRALAW: App Right Associativity Law" $
    optimizeGrammarNode (optimizeGrammarNode (u :*> v) :*> w)
  -- App Reassociation Law 3
  u :<*> (v :$> x) ->
    trace "EXTRALAW: App Reassociation Law 3" $
    optimizeGrammarNode (optimizeGrammarNode (u :<*> Pure x) :<* v)

  Look (p :$> x) ->
    optimizeGrammarNode (optimizeGrammarNode (Look p) :$> x)
  NegLook (p :$> _) -> optimizeGrammarNode (NegLook p)
  -}

  x -> x