{-# 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 Data.String (String)

import System.IO (IO)
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 a where
  Pure :: Hask.Haskell a -> Comb a
  Satisfy :: Hask.Haskell (Char -> Bool) -> Comb Char
  Item :: Comb Char
  Try :: Comb a -> Comb a
  Look :: Comb a -> Comb a
  NegLook :: Comb a -> Comb ()
  (:<*>) :: Comb (a -> b) -> Comb a -> Comb b
  (:<|>) :: Comb a -> Comb a -> Comb a
  Empty :: Comb a
  Branch :: Comb (Either a b) -> Comb (a -> c) -> Comb (b -> c) -> Comb c
  Match :: Eq a => [Hask.Haskell (a -> Bool)] -> [Comb b] -> Comb a -> Comb b -> Comb b
  ChainPre :: Comb (a -> a) -> Comb a -> Comb a
  ChainPost :: Comb a -> Comb (a -> a) -> Comb a
  Def :: String -> Comb a -> Comb a
  Ref :: Bool -> String -> Comb a

pattern (:<$>) :: Hask.Haskell (a -> b) -> Comb a -> Comb b
pattern (:$>) :: Comb a -> Hask.Haskell b -> Comb b
pattern (:<$) :: Hask.Haskell a -> Comb b -> Comb a
pattern (:*>) :: Comb a -> Comb b -> Comb b
pattern (:<*) :: Comb a -> Comb b -> Comb 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 where
  pure = Pure
  (<*>) = (:<*>)
instance Alternable Comb where
  (<|>) = (:<|>)
  empty = Empty
  try = Try
instance Selectable Comb where
  branch = Branch
instance Matchable Comb where
  conditional = Match
instance Foldable Comb where
  chainPre = ChainPre
  chainPost = ChainPost
instance Charable Comb where
  satisfy = Satisfy
instance Lookable Comb where
  look = Look
  negLook = NegLook
instance Sharable Comb where
  def = Def
  ref = Ref
instance
  ( Applicable repr
  , Alternable repr
  , Selectable repr
  , Foldable repr
  , Charable repr
  , Lookable repr
  , Matchable repr
  , Sharable repr
  ) =>
  Symantic Comb 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 Comb = repr
instance
  ( Applicable repr
  , Alternable repr
  , Selectable repr
  , Foldable repr
  , Charable repr
  , Lookable repr
  , Matchable repr
  , Sharable repr
  ) => Unliftable Comb 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
  , Sharable repr
  ) => Comb repr a -> repr a
unComb = unlift
-}

optComb :: Comb a -> Comb a
optComb = \case
  Def n x -> Def n (optComb x)
  -- 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


type instance Unlift (Ref repr) = repr
instance Liftable (Ref repr) where
  lift x = let n = x in LetNode (makeParserName n) n
  lift1 f x = let n = f (let_sub x) in LetNode (makeParserName n) n
  lift2 f x y = let n = f (let_sub x) (let_sub y) in LetNode (makeParserName n) n
  lift3 f x y z = let n = f (let_sub x) (let_sub y) (let_sub z) in LetNode (makeParserName n) n
instance Applicable repr => Applicable (Ref repr)

data Ref repr a where
  LetNode :: { let_id :: IO ParserName, let_sub :: repr a } -> Ref repr a
  --LetLeaf :: repr a -> Ref repr a
{-
instance Liftable (Ref (Comb repr)) where
  lift c = case c of
    Pure a -> LetLeaf c
  lift1 f x = case x of
    LetLeaf l -> LetLeaf (f l)
    LetNode l -> LetLeaf (f l)
instance Applicable (Ref (Comb repr)) where
  pure a = LetLeaf (pure a)
  x <*> y = LetNode (mkParserName x) (<*>
instance Applicable (Comb (Ref repr)) where
  pure a = pure a
  x <*> y = LetNode (mkParserName x) (:<*>

-}