{-# 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 qualified Prelude as Pre

import Symantic.Base.Univariant
import Symantic.Parser.Grammar.Combinators
import Symantic.Parser.Grammar.Observations
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 a -> Comb repr a
  Satisfy :: Hask.Haskell (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.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
  Let :: { let_rec :: Bool, let_name :: ParserName } -> Comb repr a

pattern (:<$>) :: Hask.Haskell (a -> b) -> Comb repr a -> Comb repr b
pattern (:$>) :: Comb repr a -> Hask.Haskell b -> Comb repr b
pattern (:<$) :: Hask.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 = Hask.Const :<$> x :<*> p
pattern p :*> x = Hask.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 Charable (Comb repr) where
  satisfy = Satisfy
instance Lookable (Comb repr) where
  look = Look
  negLook = NegLook
instance Letable (Comb repr) where
  let_ let_rec let_name = Let{..}
type instance Unlift (Comb repr) = repr
instance
  ( Applicable repr
  , Alternable repr
  , Selectable repr
  , Foldable repr
  , Charable repr
  , Lookable repr
  , Matchable repr
  , Letable repr
  ) => Unliftable (Comb repr) 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)
    Let{..} -> let_ let_rec let_name

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

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 getValue lr of
     Left v -> optComb (l :<*> Pure (Hask.Haskell (ValueCode (Value v) c)))
      where c = Code [|| case $$(getCode lr) of Left x -> x ||]
     Right v -> optComb (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)) ->
    optComb (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 ->
    optComb (x :*> optComb (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 ->
    optComb (Branch (optComb (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 -> optComb (Branch b (optComb ((Hask..@) (Hask..) f :<$> l))
                                           (optComb ((Hask..@) (Hask..) f :<$> r)))

  x -> x