{-# 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.Function ((.))
import qualified Prelude as Pre

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 cs bs a b -> conditional cs (trans Pre.<$> 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 Unlift (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 call to 'optimizeGrammarNode'
  -- where 'Def' or 'Ref' have no matching.
  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
  -- Applicable Right Absorption Law
  Empty :<*> _ -> Empty
  Empty  :*> _ -> Empty
  Empty :<*  _ -> Empty
  -- Applicable Failure Weakening Law
  u :<*> Empty -> optimizeGrammarNode (u :*> Empty)
  u :<*  Empty -> optimizeGrammarNode (u :*> Empty)
  -- Branch Absorption Law
  Branch Empty _ _ -> empty
  -- Branch Weakening Law
  Branch b Empty Empty -> optimizeGrammarNode (b :*> Empty)

  -- Applicable Identity Law
  Hask.Id :<$> x -> x
  -- Flip const optimisation
  Hask.Flip Hask.:@ Hask.Const :<$> u -> optimizeGrammarNode (u :*> Pure Hask.Id)
  -- Homomorphism Law
  f :<$> Pure x -> Pure (f Hask.:@ x)
  -- Functor Composition Law
  -- (a shortcut that could also have been be caught
  -- by the Composition Law and Homomorphism law)
  f :<$> (g :<$> p) -> optimizeGrammarNode ((Hask.:.) Hask.:@ f Hask.:@ g :<$> p)
  -- Composition Law
  u :<*> (v :<*> w) -> optimizeGrammarNode (optimizeGrammarNode (optimizeGrammarNode ((Hask.:.) :<$> u) :<*> v) :<*> w)
  -- Definition of *>
  Hask.Flip Hask.:@ Hask.Const :<$> p :<*> q -> p :*> q
  -- Definition of <*
  Hask.Const :<$> p :<*> q -> p :<* q
  -- Reassociation Law 1
  (u :*> v) :<*> w -> optimizeGrammarNode (u :*> optimizeGrammarNode (v :<*> w))
  -- Pure merge optimisation (useless)
  -- Pure x :<*> Pure y -> Pure (x Hask.:@ y)
  -- Interchange Law
  u :<*> Pure x -> optimizeGrammarNode (Hask.Flip Hask.:@ (Hask.:$) Hask.:@ x :<$> u)
  -- Right Absorption Law
  (_ :<$> p) :*> q -> p :*> q
  -- Left Absorption Law
  p :<* (_ :<$> q) -> p :<* q
  -- Reassociation Law 2
  u :<*> (v :<* w) -> optimizeGrammarNode (optimizeGrammarNode (u :<*> v) :<* w)
  -- Reassociation Law 3
  u :<*> (v :$> x) -> optimizeGrammarNode (optimizeGrammarNode (u :<*> Pure x) :<* v)

  -- Left Catch Law
  p@Pure{} :<|> _ -> p
  -- Left Neutral Law
  Empty :<|> u -> u
  -- Right Neutral Law
  u :<|> Empty -> u
  -- Associativity Law
  (u :<|> v) :<|> w -> u :<|> optimizeGrammarNode (v :<|> w)

  -- Identity law
  Pure _ :*> u -> u
  -- Identity law
  (u :$> _) :*> v -> u :*> v
  -- Associativity Law
  u :*> (v :*> w) -> optimizeGrammarNode (optimizeGrammarNode (u :*> v) :*> w)
  -- Identity law
  u :<* Pure _ -> u
  -- Identity law
  u :<* (v :$> _) -> optimizeGrammarNode (u :<* v)
  -- Commutativity Law
  x :<$ u -> optimizeGrammarNode (u :$> x)
  -- Associativity Law
  (u :<* v) :<* w -> optimizeGrammarNode (u :<* optimizeGrammarNode (v :<* w))

  -- Pure lookahead
  Look p@Pure{} -> p
  -- Dead lookahead
  Look p@Empty -> p
  -- Pure negative-lookahead
  NegLook Pure{} -> Empty

  -- Dead negative-lookahead
  NegLook Empty -> Pure Hask.unit
  -- Double Negation Law
  NegLook (NegLook p) -> optimizeGrammarNode (Look (Try p) :*> Pure Hask.unit)
  -- Zero Consumption Law
  NegLook (Try p) -> optimizeGrammarNode (NegLook p)
  -- Idempotence Law
  Look (Look p) -> Look p
  -- Right Identity Law
  NegLook (Look p) -> optimizeGrammarNode (NegLook p)

  -- Left Identity Law
  Look (NegLook p) -> NegLook p
  -- Transparency Law
  NegLook (Try p :<|> q) -> optimizeGrammarNode (optimizeGrammarNode (NegLook p) :*> optimizeGrammarNode (NegLook q))
  -- Distributivity Law
  Look p :<|> Look q -> optimizeGrammarNode (Look (optimizeGrammarNode (Try p :<|> q)))
  -- Interchange Law
  Look (p :$> x) -> optimizeGrammarNode (optimizeGrammarNode (Look p) :$> x)
  -- Interchange law
  Look (f :<$> p) -> optimizeGrammarNode (f :<$> optimizeGrammarNode (Look p))
  -- Absorption Law
  p :<*> NegLook q -> optimizeGrammarNode (optimizeGrammarNode (p :<*> Pure Hask.unit) :<* NegLook q)
  -- Idempotence Law
  NegLook (p :$> _) -> optimizeGrammarNode (NegLook p)
  -- Idempotence Law
  NegLook (_ :<$> p) -> optimizeGrammarNode (NegLook p)
  -- Interchange Law
  Try (p :$> x) -> optimizeGrammarNode (optimizeGrammarNode (Try p) :$> x)
  -- Interchange law
  Try (f :<$> p) -> optimizeGrammarNode (f :<$> optimizeGrammarNode (Try p))

  -- pure Left/Right laws
  Branch (Pure (trans -> lr)) l r ->
    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 ||]
  -- Generalised Identity law
  Branch b (Pure (trans -> l)) (Pure (trans -> r)) ->
    optimizeGrammarNode (Hask.Haskell (ValueCode v c) :<$> b)
    where
    v = Value (either (getValue l) (getValue r))
    c = Code [|| either $$(getCode l) $$(getCode r) ||]
  -- Interchange law
  Branch (x :*> y) p q ->
    optimizeGrammarNode (x :*> optimizeGrammarNode (Branch y p q))
  -- Negated Branch law
  Branch b l Empty ->
    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 ->
    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 ||]
  -- Distributivity Law
  f :<$> Branch b l r -> optimizeGrammarNode (Branch b (optimizeGrammarNode ((Hask..@) (Hask..) f :<$> l))
                                           (optimizeGrammarNode ((Hask..@) (Hask..) f :<$> r)))

  x -> x