<commit_before>{-# LANGUAGE TypeOperators, ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances, OverlappingInstances #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}

module Narradar.TRS where

import Control.Applicative
import Control.Monad
import Control.Monad.List
import Control.Monad.State
import Control.Monad.Supply
import Control.Parallel.Strategies
import Data.Array.IArray as A
import Data.Graph (Graph, edges, buildG)
import Data.Foldable as F (Foldable, foldMap, toList, concatMap)
import Data.List ((\\))
import Data.Maybe (catMaybes)
import Data.Monoid
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Set (Set)
import Data.Strict.Tuple ((:!:), Pair(..))
import Data.Traversable (Traversable)
import qualified Data.Traversable as T
import Text.PrettyPrint
import Prelude hiding (concatMap)

import TRS hiding (Ppr, ppr, unify, unifies, apply, (!))
import qualified TRS
import Narradar.ArgumentFiltering (apply, ApplyAF(..))
import qualified Narradar.ArgumentFiltering as AF
import Narradar.DPIdentifiers
import Narradar.Labellings
import Narradar.ProblemType
import Narradar.Unify
import Narradar.Utils
import qualified Language.Prolog.Syntax as Prolog
import Language.Prolog.Syntax (Ident)

#ifdef HOOD
import Debug.Observe
#endif

type DP a = Rule a

-- --------------------
-- TRSs in our setting
-- --------------------

{-
DPTRS contains an additional payload to cache:
1) the graph
2) the unifiers between the pairs computed by the EDG processor.
3) the unifiers computed by the star EDG processor
The unifiers are cached in a matrix (an (rhs,lhs) array) with the following layout
in the case of 2), and the opposite layout in the case of 3)

\ LHS|     |     |
 \   |pair1|pair2|
RHS\ |     |     |
------------------
pair1|_____|_____|
pair2|_____|_____|
.....|     |     |
-}

data NarradarTRS id f where
    TRS       :: (Ord id, TRSC f, T id :<: f) => Set (Rule f)                                 -> Signature id -> NarradarTRS id f
    PrologTRS :: (Ord id, TRSC f, T id :<: f) => Set (Ident, Rule f)                          -> Signature id -> NarradarTRS id f
    DPTRS     :: (Ord id, TRSC f, T id :<: f) => Array Int (Rule f) -> !Graph -> Unifiers f :!: Unifiers f -> Signature id -> NarradarTRS id f

type Unifiers        f = Array (Int,Int) (Maybe (Subst f))

instance (Ord id, Ord (Term f), TRSC f, T id :<: f) => Ord (NarradarTRS id f) where
    {-# SPECIALIZE instance Ord(NarradarTRS Id  BasicId) #-}
    {-# SPECIALIZE instance Ord(NarradarTRS Id  BBasicId) #-}
    {-# off SPECIALIZE instance Ord(NarradarTRS LId BBasicLId) #-}
    compare TRS{} _             = GT
    compare DPTRS{} TRS{}       = LT
    compare DPTRS{} PrologTRS{} = GT
    compare PrologTRS{} _       = LT
    compare (TRS rr1 _)       (TRS rr2 _)       = compare rr1 rr2
    compare (PrologTRS rr1 _) (PrologTRS rr2 _) = compare rr1 rr2
    compare (DPTRS rr1 _ _ _) (DPTRS rr2 _ _ _)   = compare rr1 rr2

instance (Ord id, T id :<: f, TRSC f) => TRS (NarradarTRS id f) id f where
    {-# SPECIALIZE instance TRS(NarradarTRS Id BasicId) Id BasicId #-}
    {-# SPECIALIZE instance TRS(NarradarTRS Id BBasicId) Id BBasicId #-}
    {-# off SPECIALIZE instance TRS(NarradarTRS LId BBasicLId) LId BBasicLId #-}
    rules(TRS       rr _)   = toList rr
    rules(PrologTRS rr _)   = map snd (toList rr)
    rules(DPTRS     rr _ _ _) = elems rr
    tRS = narradarTRS

tRS' rr sig  = TRS (Set.fromList rr) sig

prologTRS :: forall id f. (Ord id, TRSC f, T id :<: f) => [(Ident, Rule f)] -> NarradarTRS id f
prologTRS rr = prologTRS' (Set.fromList rr)

prologTRS' :: forall id f. (Ord id, TRSC f, T id :<: f) => Set(Ident, Rule f) -> NarradarTRS id f
prologTRS' rr = PrologTRS rr (getSignature (snd <$> toList rr))

{-# SPECIALIZE narradarTRS ::  [Rule BBasicId] -> NarradarTRS Id BBasicId #-}
narradarTRS rules = TRS (Set.fromList rules) (getSignature rules)
--dpTRS :: (T id :<: d) => ProblemType id -> NarradarTRS id f -> [DP f] -> Graph -> NarradarTRS id f
dpTRS typ trs dps edges = dpTRS' typ trs dps' edges
  where dps' = listArray (0, length dps - 1) (refreshRules [0..] dps)

-- | Assumes that the rules have already been renamed apart
--dpTRS' :: (T id :<: d) => ProblemType id -> NarradarTRS id f -> Array Int (DP f) -> Graph -> NarradarTRS id f
dpTRS' typ trs dps edges = DPTRS dps edges (computeDPUnifiers typ trs $ elems dps)
                                           (getSignature $ elems dps)

-- | Assumes that the rules have already been renamed apart
dpTRS'' dps edges unifiers = DPTRS dps edges unifiers (getSignature $ elems dps)

refreshRules ids  = (`runSupply'` ids) . mapM doRule where
        doRule r = do
          let vv = foldMap vars' r
          newvv <- replicateM (length vv) next
          return (replace (Prelude.zipWith leftName vv newvv) <$> r)

        leftName v1 i2 = (v1, var' (varName v1) i2)
--        leftName v1 i2 = (v1, var i2)

        varName (open -> Just (Var n _)) = n
        varName _ = Nothing

--computeDPUnifiers _ _ dps | trace ("computeDPUnifiers dps=" ++ show(length dps)) False = undefined
computeDPUnifiers :: (DPMark f, TRS trs id f, ApplyAF trs id, MonadPlus m, unif ~ Array (Int,Int) (m(Subst f)))=> ProblemType id -> trs -> [DP f] -> unif :!: unif
computeDPUnifiers typ trs dps = unif :!: unifInv where
   unif = array ( (0,0), (length dps -1 , length dps - 1) )
           [((x,y), unify' l (if x/=y then r' else head(variant' [r'] [l])))
              | (x, _ :-> r) <- zip [0..] dps
              , (y, l :-> _) <- zip [0..] dps
              , let r' = runSupply' (icap trs r >>= mbren) ids ]
   unifInv = array ( (0,0), (length dps -1 , length dps - 1) )
           [((x,y), unify' r (if x/=y then l' else head(variant' [l'] [r])))
              | (x, _ :-> r) <- zip [0..] dps
              , (y, l :-> _) <- zip [0..] dps
              , let trs' = tRS (swapRule <$> mbUsableRules [r]) `asTypeOf` trs
              , let l' = runSupply' (icap trs' l >>= ren) ids ]

   ids = [0..] \\ (concatMap.concatMap) collectVars dps
   (mbren, mbUsableRules) = if (isBNarrowing .|. isGNarrowing) typ
                              then (return,iUsableRules trs Nothing)
                              else (ren,const (rules trs))

restrictDPTRS (DPTRS dps gr (unif :!: unifInv) sig) indexes =
    DPTRS dps' gr' unif' sig
  where
   newIndexes = Map.fromList (zip indexes [0..])
   nindexes   = length indexes -1
   dps'       = extractIxx dps indexes
   gr'        = A.amap (catMaybes . map (`Map.lookup` newIndexes)) (extractIxx gr indexes)
   extractIxx arr nodes = A.listArray (0, length nodes - 1) [arr A.! n | n <- nodes]
   unif' = (reindexArray unif :!: reindexArray unifInv)
   reindexArray arr =
           A.array ( (0,0), (nindexes, nindexes) )
                   [ ( (x',y'), sigma) | ((x,y),sigma) <- A.assocs arr
                                       , Just x' <- [Map.lookup x newIndexes]
                                       , Just y' <- [Map.lookup y newIndexes]]

dpUnify    (DPTRS _ _ (unifs :!: _) _) l r = unifs ! (r,l)
dpUnifyInv (DPTRS _ _ (_ :!: unifs) _) l r = unifs ! (r,l)

--expandDPair :: ProblemG id f -> Int -> [DP f] -> ProblemG id f
--expandDPair (Problem typ rules (DPTRS dps gr unif sig)) i newdps | trace ("expandDPair i="++ show i ++ " dps=" ++ show(numElements dps) ++ " newdps=" ++ show (length newdps)) False = undefined
expandDPair typ trs (DPTRS dps gr (unif :!: unifInv) sig) i newdps =
    dptrs' `demanding` rnf unif' `demanding` rnf unifInv'
  where
    dptrs' = dpTRS'' a_dps' gr' (unif' :!: unifInv')
    unif'  = mkUnif' unif unif_new          `asTypeOf` unif
    unifInv' = mkUnif' unifInv unifInv_new  `asTypeOf` unif
    a_dps' = A.listArray (0,length dps' - 1) dps'
    dps'   = dps1 ++  dps2 ++ refreshRules ids newdps
    (dps1,_:dps2) = splitAt i (elems dps)
    ids = [0..] \\ (concatMap.concatMap) collectVars dps

    gr' = buildG (0, l_dps' - 1)
                   ([(adjust x,adjust y) | (x,y) <- edges gr, x/=i, y/=i] ++
                    [(n,n') | n' <- new_nodes
                            , (n,m) <- edges gr, n/=i, m == i ] ++
                    [(n',n) | n <- gr ! i, n' <- new_nodes] ++
                    [(n',n'') | n' <- new_nodes, n'' <- new_nodes, i `elem` gr ! i])

    mkUnif' arr arr' =
       A.array ((0,0), (length dps' - 1, length dps' - 1))
                       ([((adjust x,adjust y), sigma) | ((x,y), sigma) <- assocs arr
                                                      , x /= i, y /= i] ++
                        concat [ [(in1, arr' ! in1), (in2, arr' ! in2)]
--                                 [ (in1, computeDPUnifier typ rules a_dps' in1)
--                                 , (in2, computeDPUnifier typ rules a_dps' in2)]
                                 | j <- new_nodes, k <- [0..l_dps'-1]
                                 , let in1 = (j,k), let in2 = (k,j)])
    (unif_new :!: unifInv_new) = computeDPUnifiers typ trs dps'
    adjust x = if x < i then x else x-1
    !l_dps'   = length dps'<commit_msg>Fix a name capturing bug in computeDPUnifiers<commit_after>{-# LANGUAGE TypeOperators, ScopedTypeVariables #-}
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances, OverlappingInstances #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}

module Narradar.TRS where

import Control.Applicative
import Control.Monad
import Control.Monad.List
import Control.Monad.State
import Control.Monad.Supply
import Control.Parallel.Strategies
import Data.Array.IArray as A
import Data.Graph (Graph, edges, buildG)
import Data.Foldable as F (Foldable, foldMap, toList, concatMap)
import Data.List ((\\))
import Data.Maybe (catMaybes)
import Data.Monoid
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Set (Set)
import Data.Strict.Tuple ((:!:), Pair(..))
import Data.Traversable (Traversable)
import qualified Data.Traversable as T
import Text.PrettyPrint
import Prelude hiding (concatMap)

import TRS hiding (Ppr, ppr, unify, unifies, apply, (!))
import qualified TRS
import Narradar.ArgumentFiltering (apply, ApplyAF(..))
import qualified Narradar.ArgumentFiltering as AF
import Narradar.DPIdentifiers
import Narradar.Labellings
import Narradar.ProblemType
import Narradar.Unify
import Narradar.Utils
import qualified Language.Prolog.Syntax as Prolog
import Language.Prolog.Syntax (Ident)

#ifdef HOOD
import Debug.Observe
#endif

type DP a = Rule a

-- --------------------
-- TRSs in our setting
-- --------------------

{-
DPTRS contains an additional payload to cache:
1) the graph
2) the unifiers between the pairs computed by the EDG processor.
3) the unifiers computed by the star EDG processor
The unifiers are cached in a matrix (an (rhs,lhs) array) with the following layout
in the case of 2), and the opposite layout in the case of 3)

\ LHS|     |     |
 \   |pair1|pair2|
RHS\ |     |     |
------------------
pair1|_____|_____|
pair2|_____|_____|
.....|     |     |
-}

data NarradarTRS id f where
    TRS       :: (Ord id, TRSC f, T id :<: f) => Set (Rule f)                                 -> Signature id -> NarradarTRS id f
    PrologTRS :: (Ord id, TRSC f, T id :<: f) => Set (Ident, Rule f)                          -> Signature id -> NarradarTRS id f
    DPTRS     :: (Ord id, TRSC f, T id :<: f) => Array Int (Rule f) -> !Graph -> Unifiers f :!: Unifiers f -> Signature id -> NarradarTRS id f

type Unifiers        f = Array (Int,Int) (Maybe (Subst f))

instance (Ord id, Ord (Term f), TRSC f, T id :<: f) => Ord (NarradarTRS id f) where
    {-# SPECIALIZE instance Ord(NarradarTRS Id  BasicId) #-}
    {-# SPECIALIZE instance Ord(NarradarTRS Id  BBasicId) #-}
    {-# off SPECIALIZE instance Ord(NarradarTRS LId BBasicLId) #-}
    compare TRS{} _             = GT
    compare DPTRS{} TRS{}       = LT
    compare DPTRS{} PrologTRS{} = GT
    compare PrologTRS{} _       = LT
    compare (TRS rr1 _)       (TRS rr2 _)       = compare rr1 rr2
    compare (PrologTRS rr1 _) (PrologTRS rr2 _) = compare rr1 rr2
    compare (DPTRS rr1 _ _ _) (DPTRS rr2 _ _ _)   = compare rr1 rr2

instance (Ord id, T id :<: f, TRSC f) => TRS (NarradarTRS id f) id f where
    {-# SPECIALIZE instance TRS(NarradarTRS Id BasicId) Id BasicId #-}
    {-# SPECIALIZE instance TRS(NarradarTRS Id BBasicId) Id BBasicId #-}
    {-# off SPECIALIZE instance TRS(NarradarTRS LId BBasicLId) LId BBasicLId #-}
    rules(TRS       rr _)   = toList rr
    rules(PrologTRS rr _)   = map snd (toList rr)
    rules(DPTRS     rr _ _ _) = elems rr
    tRS = narradarTRS

tRS' rr sig  = TRS (Set.fromList rr) sig

prologTRS :: forall id f. (Ord id, TRSC f, T id :<: f) => [(Ident, Rule f)] -> NarradarTRS id f
prologTRS rr = prologTRS' (Set.fromList rr)

prologTRS' :: forall id f. (Ord id, TRSC f, T id :<: f) => Set(Ident, Rule f) -> NarradarTRS id f
prologTRS' rr = PrologTRS rr (getSignature (snd <$> toList rr))

{-# SPECIALIZE narradarTRS ::  [Rule BBasicId] -> NarradarTRS Id BBasicId #-}
narradarTRS rules = TRS (Set.fromList rules) (getSignature rules)
--dpTRS :: (T id :<: d) => ProblemType id -> NarradarTRS id f -> [DP f] -> Graph -> NarradarTRS id f
dpTRS typ trs dps edges = dpTRS' typ trs dps' edges
  where dps' = listArray (0, length dps - 1) (refreshRules [0..] dps)

-- | Assumes that the rules have already been renamed apart
--dpTRS' :: (T id :<: d) => ProblemType id -> NarradarTRS id f -> Array Int (DP f) -> Graph -> NarradarTRS id f
dpTRS' typ trs dps edges = DPTRS dps edges (computeDPUnifiers typ trs $ elems dps)
                                           (getSignature $ elems dps)

-- | Assumes that the rules have already been renamed apart
dpTRS'' dps edges unifiers = DPTRS dps edges unifiers (getSignature $ elems dps)

refreshRules ids  = (`runSupply'` ids) . mapM doRule where
        doRule r = do
          let vv = foldMap vars' r
          newvv <- replicateM (length vv) next
          return (replace (Prelude.zipWith leftName vv newvv) <$> r)

        leftName v1 i2 = (v1, var' (varName v1) i2)
--        leftName v1 i2 = (v1, var i2)

        varName (open -> Just (Var n _)) = n
        varName _ = Nothing

--computeDPUnifiers _ _ dps | trace ("computeDPUnifiers dps=" ++ show(length dps)) False = undefined
computeDPUnifiers :: (DPMark f, TRS trs id f, ApplyAF trs id, MonadPlus m, unif ~ Array (Int,Int) (m(Subst f)))=> ProblemType id -> trs -> [DP f] -> unif :!: unif
computeDPUnifiers typ trs dps = unif :!: unifInv where
   unif = array ( (0,0), (length dps -1 , length dps - 1) )
           [((x,y), unify l (if x/=y then r' else rename r'))
              | (x, _ :-> r) <- zip [0..] dps
              , (y, l :-> _) <- zip [0..] dps
              , let r' = runSupply' (icap trs r >>= mbren) ids ]
   unifInv = array ( (0,0), (length dps -1 , length dps - 1) )
           [((x,y), unify r (if x/=y then l' else rename l'))
              | (x, _ :-> r) <- zip [0..] dps
              , (y, l :-> _) <- zip [0..] dps
              , let trs' = tRS (swapRule <$> mbUsableRules [r]) `asTypeOf` trs
              , let l' = runSupply' (icap trs' l >>= ren) ids ]

   rename t = head $ runSupply' (variant [t]) ids
   ids = [0..] \\ (concatMap.concatMap) collectVars dps
   (mbren, mbUsableRules) = if (isBNarrowing .|. isGNarrowing) typ
                              then (return,iUsableRules trs Nothing)
                              else (ren,const (rules trs))

restrictDPTRS (DPTRS dps gr (unif :!: unifInv) sig) indexes =
    DPTRS dps' gr' unif' sig
  where
   newIndexes = Map.fromList (zip indexes [0..])
   nindexes   = length indexes -1
   dps'       = extractIxx dps indexes
   gr'        = A.amap (catMaybes . map (`Map.lookup` newIndexes)) (extractIxx gr indexes)
   extractIxx arr nodes = A.listArray (0, length nodes - 1) [arr A.! n | n <- nodes]
   unif' = (reindexArray unif :!: reindexArray unifInv)
   reindexArray arr =
           A.array ( (0,0), (nindexes, nindexes) )
                   [ ( (x',y'), sigma) | ((x,y),sigma) <- A.assocs arr
                                       , Just x' <- [Map.lookup x newIndexes]
                                       , Just y' <- [Map.lookup y newIndexes]]

dpUnify    (DPTRS _ _ (unifs :!: _) _) l r = unifs ! (r,l)
dpUnifyInv (DPTRS _ _ (_ :!: unifs) _) l r = unifs ! (r,l)

--expandDPair :: ProblemG id f -> Int -> [DP f] -> ProblemG id f
--expandDPair (Problem typ rules (DPTRS dps gr unif sig)) i newdps | trace ("expandDPair i="++ show i ++ " dps=" ++ show(numElements dps) ++ " newdps=" ++ show (length newdps)) False = undefined
expandDPair typ trs (DPTRS dps gr (unif :!: unifInv) sig) i newdps =
    dptrs' `demanding` rnf unif' `demanding` rnf unifInv'
  where
    dptrs'   = dpTRS'' a_dps' gr' (unif' :!: unifInv')
    unif'    = mkUnif' unif    unif_new     `asTypeOf` unif
    unifInv' = mkUnif' unifInv unifInv_new  `asTypeOf` unif
    a_dps'   = A.listArray (0,length dps' - 1) dps'
    dps'     = dps1 ++  dps2 ++ refreshRules ids newdps
    ids      = [0..] \\ (concatMap.concatMap) collectVars dps
    (dps1,_:dps2) = splitAt i (elems dps)

    gr' = buildG (0, l_dps' - 1)
                   ([(adjust x,adjust y) | (x,y) <- edges gr, x/=i, y/=i] ++
                    [(n,n') | n' <- new_nodes
                            , (n,m) <- edges gr, n/=i, m == i ] ++
                    [(n',n) | n <- gr ! i, n' <- new_nodes] ++
                    [(n',n'') | n' <- new_nodes, n'' <- new_nodes, i `elem` gr ! i])

    mkUnif' arr arr' =
       A.array ((0,0), (length dps' - 1, length dps' - 1))
                       ([((adjust x,adjust y), sigma) | ((x,y), sigma) <- assocs arr
                                                      , x /= i, y /= i] ++
                        concat [ [(in1, arr' ! in1), (in2, arr' ! in2)]
--                                 [ (in1, computeDPUnifier typ rules a_dps' in1)
--                                 , (in2, computeDPUnifier typ rules a_dps' in2)]
                                 | j <- new_nodes, k <- [0..l_dps'-1]
                                 , let in1 = (j,k), let in2 = (k,j)])
    (unif_new :!: unifInv_new) = computeDPUnifiers typ trs dps'
    adjust x = if x < i then x else x-1
    !l_dps'   = length dps'
{'fraction_non_alphanumeric': 0.14046301767202019, 'fraction_numerical': 0.008379438147929312, 'mean_word_length': 2.3069271758436947, 'pattern_counts': {'":': 0, '<': 67, '<?xml version=': 0, '>': 97, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 26, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2805996', 'n_tokens_mistral': 6995, 'n_tokens_neox': 6701, 'n_words': 2106}