{-# 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 (Runtimeable(..), OptRuntime(..))
import qualified Symantic.Parser.Staging as S
import qualified Language.Haskell.TH.Syntax as TH

-- * Type 'OptGram'
data OptGram repr a where
 Pure :: S.OptRuntime S.Runtime a -> OptGram repr a
 Satisfy :: S.Runtime (Char -> Bool) -> OptGram repr Char
 Item :: OptGram repr Char
 Try :: OptGram repr a -> OptGram repr a
 Look :: OptGram repr a -> OptGram repr a
 NegLook :: OptGram repr a -> OptGram repr ()
 (:<*>) :: OptGram repr (a -> b) -> OptGram repr a -> OptGram repr b
 (:<|>) :: OptGram repr a -> OptGram repr a -> OptGram repr a
 Empty :: OptGram repr a
 Branch :: OptGram repr (Either a b) -> OptGram repr (a -> c) -> OptGram repr (b -> c) -> OptGram repr c
 Match :: Eq a => [S.Runtime (a -> Bool)] -> [OptGram repr b] -> OptGram repr a -> OptGram repr b -> OptGram repr b
 ChainPre :: OptGram repr (a -> a) -> OptGram repr a -> OptGram repr a
 ChainPost :: OptGram repr a -> OptGram repr (a -> a) -> OptGram repr a

pattern (:<$>) :: S.OptRuntime S.Runtime (a -> b) -> OptGram repr a -> OptGram repr b
pattern (:$>) :: OptGram repr a -> S.OptRuntime S.Runtime b -> OptGram repr b
pattern (:<$) :: S.OptRuntime S.Runtime a -> OptGram repr b -> OptGram repr a
pattern (:*>) :: OptGram repr a -> OptGram repr b -> OptGram repr b
pattern (:<*) :: OptGram repr a -> OptGram repr b -> OptGram repr a
pattern x :<$> p = Pure x :<*> p
pattern p :$> x = p :*> Pure x
pattern x :<$ p = Pure x :<* p
pattern x :<* p = S.Const :<$> x :<*> p
pattern p :*> x = S.Id :<$ p :<*> x

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

instance Applicable (OptGram Runtime) where
  pure = Pure Function.. S.OptRuntime
  (<*>) = (:<*>)
instance Alternable (OptGram repr) where
  (<|>) = (:<|>)
  empty = Empty
  try = Try
instance Selectable (OptGram repr) where
  branch = Branch
instance Matchable (OptGram repr) where
  conditional = Match
instance Foldable (OptGram repr) where
  chainPre = ChainPre
  chainPost = ChainPost
instance Charable (OptGram repr) where
  satisfy = Satisfy
instance Lookable (OptGram repr) where
  look = Look
  negLook = NegLook
type instance Unlift (OptGram repr) = repr
instance
 ( Applicable repr
 , Alternable repr
 , Selectable repr
 , Foldable repr
 , Charable repr
 , Lookable repr
 , Matchable repr
 ) => Unliftable (OptGram 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)

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

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

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

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

  -- pure Left/Right laws
  Branch (Pure (unlift -> lr)) l r ->
    case getEval lr of
     Left e -> optGram (l :<*> Pure (S.OptRuntime (Runtime (Eval e) c)))
      where c = Code [|| case $$(getCode lr) of Left x -> x ||]
     Right e -> optGram (r :<*> Pure (S.OptRuntime (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)) ->
    optGram (S.OptRuntime (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 ->
    optGram (x :*> optGram (Branch y p q))
  -- Negated Branch law
  Branch b l Empty ->
    Branch (Pure (S.OptRuntime (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 ->
    optGram (Branch (optGram (Pure (S.OptRuntime (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 -> optGram (Branch b (optGram ((S..@) (S..) f :<$> l))
                                           (optGram ((S..@) (S..) f :<$> r)))

  x -> x