{-  Copyright 2010 Dominique Devriese

    This file is part of the grammar-combinators library.

    The grammar-combinators library is free software: you can
    redistribute it and/or modify it under the terms of the GNU
    Lesser General Public License as published by the Free
    Software Foundation, either version 3 of the License, or (at
    your option) any later version.

    Foobar is distributed in the hope that it will be useful, but
    WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
    GNU Lesser General Public License for more details.

    You should have received a copy of the GNU Lesser General
    Public License along with Foobar. If not, see
    <http://www.gnu.org/licenses/>.
-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Text.GrammarCombinators.Utils.IsDead (
  isDead
  ) where

import Text.GrammarCombinators.Base
import Text.GrammarCombinators.Utils.UnfoldDepthFirst

import Data.Maybe

import Control.Monad.State

data KnownDead phi = MkKD { knownDead :: forall ix. phi ix -> Maybe Bool }
newtype IsDeadRule phi (r :: * -> *) t (rr :: * -> *) v = MkIDR {
  -- second bool means dead or not
  -- first bool means dead state influenced by recursion cut-off
  ruleIsDead :: State (KnownDead phi) (Bool, Bool)
  }
cast :: IsDeadRule phi r t rr v -> IsDeadRule phi r t rr v'
cast = MkIDR . ruleIsDead

seqDead :: (Bool, Bool) -> (Bool, Bool) -> (Bool, Bool)
seqDead (False, True) _ = (False, True)
seqDead _ (False, True) = (False, True)
seqDead (ra, da) (rb, db) = (ra || rb, da || db)
altDead :: (Bool, Bool) -> (Bool, Bool) -> (Bool, Bool)
altDead (False, False) _ = (False, False)
altDead _ (False, False) = (False, False)
altDead (ra, da) (rb, db) = (ra || rb, da && db)

instance ProductionRule (IsDeadRule phi r t rr) where
  ra >>> rb = MkIDR $ liftM2 seqDead (ruleIsDead ra) (ruleIsDead rb)
  ra ||| rb = MkIDR $ liftM2 altDead (ruleIsDead ra) (ruleIsDead rb)
  die = MkIDR $ return (False, True)
  endOfInput = MkIDR $ return (False, False)

instance EpsProductionRule (IsDeadRule phi r t rr) where
  epsilon _ = MkIDR $ return (False, False)

instance LiftableProductionRule (IsDeadRule phi r t rr) where
  epsilonL _ _ = MkIDR $ return (False, False)

instance TokenProductionRule (IsDeadRule phi r t rr) t where
  token _ = anyToken
  anyToken = MkIDR $ return (False, False)

instance PenaltyProductionRule (IsDeadRule phi r t rr) where
  penalty _ r = r

instance BiasedProductionRule (IsDeadRule phi r t rr) where
  (>|||) = (|||)
  (<|||) = (|||)

instance (EqFam phi, MemoFam phi) =>
         SimpleRecProductionRule (IsDeadRule phi r t rr) phi r rr where
  ref' idx r = MkIDR $ do kds <- get
                          case knownDead kds idx of
                            (Just kd) -> return (False, kd)
                            _ -> do (rl,d) <- ruleIsDead r 
                                    unless rl $ putDeath idx d 
                                    return (rl, d)
  cutRecursion _ = MkIDR $ return (True, True)
  
instance (EqFam phi, MemoFam phi) =>
         SimpleLoopProductionRule (IsDeadRule phi r t rr) phi r rr where
  manyRef' _ _ = MkIDR $ return (False, False)
  many1Ref' idx r = cast (ref' idx r)

putDeath :: (EqFam phi, MemoFam phi) => phi ix -> Bool ->
            State (KnownDead phi) ()
putDeath idx d =
  do let setDead kd = MkKD $ memoFamilyK $ overrideIdxK (knownDead kd) idx $ Just d
     modify setDead

-- this is dead slow atm, we must be able to do better..
-- isDead1 :: forall phi t r rr ix. (EqFam phi, MemoFam phi) =>
--            GExtendedContextFreeGrammar phi t r rr ->
--            phi ix -> Bool
-- isDead1 gram idx = 
--   let 
--     ikd :: KnownDead phi
--     ikd = MkKD $ \_ -> Nothing
--   in snd $ evalState (ruleIsDead (unfoldDepthFirst gram idx)) ikd

-- | Detect if a given non-terminal in a given grammar is dead. A 
-- non-terminal is dead if its production rule can never match
-- anything.
isDead :: forall phi t r rr ix. (EqFam phi, FoldFam phi, MemoFam phi) =>
          GExtendedContextFreeGrammar phi t r rr ->
          phi ix -> Bool
isDead gram = 
  let
    ikd :: KnownDead phi
    ikd = MkKD $ \_ -> Nothing
    checkDead idx =
      do (_,d) <- ruleIsDead (unfoldDepthFirst gram idx)
         putDeath idx d
    checkAll = foldFam ((>>) . checkDead) (return ())
  in fromJust . knownDead (execState checkAll ikd)
 
-- foldDead :: forall phi r t rr ix b. (Domain phi) => 
--             GExtendedContextFreeGrammar phi r t rr -> 
--             (forall ix. phi ix -> b -> b) -> b -> b
-- foldDead grammar f n = 
--   let
--     f' :: forall ix. phi ix -> b -> b
--     f' idx n = if isDead grammar idx then f idx n else n
--   in foldFam f' n