{-# 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.Liftable
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
  ( Applicable repr
  , Alternable repr
  , Selectable repr
  , Foldable repr
  , Charable repr
  , Lookable repr
  , Matchable repr
  , Letable TH.Name repr
  ) =>
  Symantic Grammar repr where
  sym = \case
    Pure a -> pure a
    Satisfy p -> satisfy p
    Item -> item
    Try x -> try (sym x)
    Look x -> look (sym x)
    NegLook x -> negLook (sym x)
    x :<*> y -> sym x <*> sym y
    x :<|> y -> sym x <|> sym y
    Empty -> empty
    Branch lr l r -> branch (sym lr) (sym l) (sym r)
    Match cs bs a b -> conditional cs (sym Pre.<$> bs) (sym a) (sym b)
    ChainPre x y -> chainPre (sym x) (sym y)
    ChainPost x y -> chainPost (sym x) (sym y)
    Def n x -> def n (sym x)
    Ref r n -> ref r n
{-
type instance Unlift Grammar = repr
instance
  ( Applicable repr
  , Alternable repr
  , Selectable repr
  , Foldable repr
  , Charable repr
  , Lookable repr
  , Matchable repr
  , Letable repr
  ) => Unliftable Grammar where
  unlift = \case
    Pure a -> pure a
    Satisfy p -> satisfy p
    Item -> item
    Try x -> try (unlift x)
    Look x -> look (unlift x)
    NegLook x -> negLook (unlift x)
    x :<*> y -> unlift x <*> unlift y
    x :<|> y -> unlift x <|> unlift y
    Empty -> empty
    Branch lr l r -> branch (unlift lr) (unlift l) (unlift r)
    Match cs bs a b -> conditional cs (unlift Pre.<$> bs) (unlift a) (unlift b)
    ChainPre x y -> chainPre (unlift x) (unlift y)
    ChainPost x y -> chainPost (unlift x) (unlift y)
    Ref{..} -> let_ let_rec let_name

unComb ::
  ( Applicable repr
  , Alternable repr
  , Selectable repr
  , Foldable repr
  , Charable repr
  , Lookable repr
  , Matchable repr
  , Letable repr
  ) => Grammar repr a -> repr a
unComb = unlift
-}

-- * Type 'OptimizeGrammar'
newtype OptimizeGrammar letName a = OptimizeGrammar { unOptimizeGrammar ::
  Grammar a }

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

type instance Unlift (OptimizeGrammar letName) = Grammar
instance Unliftable (OptimizeGrammar letName) where
  unlift = unOptimizeGrammar
instance Liftable (OptimizeGrammar letName) where
  lift = OptimizeGrammar . optimizeGrammarNode
instance
  Letable letName Grammar =>
  Letable letName (OptimizeGrammar letName)
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
  -- Recurse into shared and/or recursive 'let' definition
  Def n x -> Def n (optimizeGrammarNode x)

  -- 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
  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 (unlift -> 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 (unlift -> l)) (Pure (unlift -> 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 (unlift -> 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