{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE UndecidableInstances #-}
module Symantic.Parser.Grammar.Optimizations where

import Data.Bool (Bool)
import Data.Char (Char)
import Data.Either (Either(..), either)
import Data.Eq (Eq(..))
-- import Data.Maybe (Maybe(..))
-- import Data.Typeable
-- import Prelude (undefined)
import qualified Data.Function as Function
import qualified Prelude as Pre

import Symantic.Base.Univariant
import Symantic.Parser.Grammar.Combinators
import Symantic.Parser.Staging hiding (Haskell(..))
import qualified Symantic.Parser.Staging as Hask
-- import qualified Language.Haskell.TH.Syntax as TH

-- * Type 'Comb'
data Comb repr a where
 Pure :: Hask.Haskell Hask.Runtime a -> Comb repr a
 Satisfy :: Hask.Runtime (Char -> Bool) -> Comb repr Char
 Item :: Comb repr Char
 Try :: Comb repr a -> Comb repr a
 Look :: Comb repr a -> Comb repr a
 NegLook :: Comb repr a -> 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 => [Hask.Runtime (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

pattern (:<$>) :: Hask.Haskell Hask.Runtime (a -> b) -> Comb repr a -> Comb repr b
pattern (:$>) :: Comb repr a -> Hask.Haskell Hask.Runtime b -> Comb repr b
pattern (:<$) :: Hask.Haskell Hask.Runtime 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 = Hask.Const :<$> x :<*> p
pattern p :*> x = Hask.Id :<$ p :<*> x

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

instance Applicable (Comb Runtime) where
  pure = Pure Function.. Hask.Haskell
  (<*>) = (:<*>)
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 Charable (Comb repr) where
  satisfy = Satisfy
instance Lookable (Comb repr) where
  look = Look
  negLook = NegLook
type instance Unlift (Comb repr) = repr
instance
 ( Applicable repr
 , Alternable repr
 , Selectable repr
 , Foldable repr
 , Charable repr
 , Lookable repr
 , Matchable repr
 ) => Unliftable (Comb repr) where
  unlift = \case
    Pure a -> pure (unlift 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)

optComb ::
 Comb repr a -> Comb repr a
optComb = \case
  -- Applicable Right Absorption Law
  Empty :<*> _ -> Empty
  Empty  :*> _ -> Empty
  Empty :<*  _ -> Empty
  -- Applicable Failure Weakening Law
  u :<*> Empty -> optComb (u :*> Empty)
  u :<*  Empty -> optComb (u :*> Empty)
  -- Branch Absorption Law
  Branch Empty _ _ -> empty
  -- Branch Weakening Law
  Branch b Empty Empty -> optComb (b :*> Empty)

  -- Applicable Identity Law
  Hask.Id :<$> x -> x
  -- Flip const optimisation
  Hask.Flip Hask.:@ Hask.Const :<$> u -> optComb (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) -> optComb ((Hask.:.) Hask.:@ f Hask.:@ g :<$> p)
  -- Composition Law
  u :<*> (v :<*> w) -> optComb (optComb (optComb ((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 -> optComb (u :*> optComb (v :<*> w))
  -- Interchange Law
  u :<*> Pure x -> optComb (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) -> optComb (optComb (u :<*> v) :<* w)
  -- Reassociation Law 3
  u :<*> (v :$> x) -> optComb (optComb (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 :<|> optComb (v :<|> w)

  -- Identity law
  Pure _ :*> u -> u
  -- Identity law
  (u :$> _) :*> v -> u :*> v
  -- Associativity Law
  u :*> (v :*> w) -> optComb (optComb (u :*> v) :*> w)
  -- Identity law
  u :<* Pure _ -> u
  -- Identity law
  u :<* (v :$> _) -> optComb (u :<* v)
  -- Commutativity Law
  x :<$ u -> optComb (u :$> x)
  -- Associativity Law
  (u :<* v) :<* w -> optComb (u :<* optComb (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) -> optComb (Look (Try p) :*> Pure Hask.unit)
  -- Zero Consumption Law
  NegLook (Try p) -> optComb (NegLook p)
  -- Idempotence Law
  Look (Look p) -> Look p
  -- Right Identity Law
  NegLook (Look p) -> optComb (NegLook p)

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

  -- pure Left/Right laws
  Branch (Pure (unlift -> lr)) l r ->
    case getEval lr of
     Left e -> optComb (l :<*> Pure (Hask.Haskell (Runtime (Eval e) c)))
      where c = Code [|| case $$(getCode lr) of Left x -> x ||]
     Right e -> optComb (r :<*> Pure (Hask.Haskell (Runtime (Eval e) c)))
      where c = Code [|| case $$(getCode lr) of Right x -> x ||]
  -- Generalised Identity law
  Branch b (Pure (unlift -> l)) (Pure (unlift -> r)) ->
    optComb (Hask.Haskell (Runtime e c) :<$> b)
    where
    e = Eval (either (getEval l) (getEval r))
    c = Code [|| either $$(getCode l) $$(getCode r) ||]
  -- Interchange law
  Branch (x :*> y) p q ->
    optComb (x :*> optComb (Branch y p q))
  -- Negated Branch law
  Branch b l Empty ->
    Branch (Pure (Hask.Haskell (Runtime e c)) :<*> b) Empty l
    where
    e = Eval (either Right Left)
    c = Code [||either Right Left||]
  -- Branch Fusion law
  Branch (Branch b Empty (Pure (unlift -> lr))) Empty br ->
    optComb (Branch (optComb (Pure (Hask.Haskell (Runtime (Eval e) c)) :<*> b)) Empty br)
    where
    e Left{} = Left ()
    e (Right r) = case getEval 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 -> optComb (Branch b (optComb ((Hask..@) (Hask..) f :<$> l))
                                           (optComb ((Hask..@) (Hask..) f :<$> r)))

  x -> x