<commit_before>{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns, PatternGuards #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}

module Narradar.Processor.SubtermCriterion where

import Control.Monad
import Control.Monad.Failure
import Data.List (insert, maximumBy, sort, sortBy)
import Data.Maybe (listToMaybe)
import qualified Data.Set as Set

import Narradar.Framework
import Narradar.Framework.GraphViz
import Narradar.Types
import qualified Narradar.Types.Problem.InitialGoal as InitialGoal
import qualified Narradar.Types.Problem.NarrowingGen as NarrowingGen
import Narradar.Types.ArgumentFiltering (AF_)
import qualified Narradar.Types.ArgumentFiltering as AF
import Narradar.Utils (on)

data SubtermCriterion         = SubtermCriterion deriving (Eq, Show, Ord)
data SubtermCriterionProof id = SubtermCriterionProof (Proj id) deriving (Eq, Show, Ord)
instance (Pretty (DPIdentifier id), Ord id) => Pretty (SubtermCriterionProof (DPIdentifier id)) where
    pPrint (SubtermCriterionProof pi) = text "Subterm Criterion with the projection:" $$
                                        nest 2 pi

instance (Info info (SubtermCriterionProof id), Ord id, Pretty id) =>
         Processor info SubtermCriterion (Problem Rewriting (NTRS id)) (Problem Rewriting (NTRS id))
  where
   apply SubtermCriterion p0 = case subtermCriterion (getP p0) of
                                Nothing          -> mzero
                                Just (pTRS',prj) -> singleP (SubtermCriterionProof prj) p0 (setP pTRS' p0)

instance (Info info (SubtermCriterionProof id),Ord id, Pretty id) =>
         Processor info SubtermCriterion (Problem IRewriting (NTRS id)) (Problem IRewriting (NTRS id))
  where
   apply SubtermCriterion p0 = case subtermCriterion (getP p0) of
                                Nothing          -> mzero<commit_msg>demand minimality in the subterm criterion for rewriting without strategies<commit_after>{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns, PatternGuards #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}

module Narradar.Processor.SubtermCriterion where

import Control.Monad
import Control.Monad.Failure
import Data.List (insert, maximumBy, sort, sortBy)
import Data.Maybe (listToMaybe)
import qualified Data.Set as Set

import Narradar.Framework
import Narradar.Framework.GraphViz
import Narradar.Types
import qualified Narradar.Types.Problem.InitialGoal as InitialGoal
import qualified Narradar.Types.Problem.NarrowingGen as NarrowingGen
import Narradar.Types.ArgumentFiltering (AF_)
import qualified Narradar.Types.ArgumentFiltering as AF
import Narradar.Utils (on)

data SubtermCriterion         = SubtermCriterion deriving (Eq, Show, Ord)
data SubtermCriterionProof id = SubtermCriterionProof (Proj id)
                              | SubtermCriterionFailMinimality
     deriving (Eq, Show, Ord)

instance (Pretty (DPIdentifier id), Ord id) => Pretty (SubtermCriterionProof (DPIdentifier id)) where
    pPrint SubtermCriterionFailMinimality = text "The problem does not have the minimality property," $$
                                            text "nor is innermost, hence the subterm criterion does not apply"

    pPrint (SubtermCriterionProof pi) = text "Subterm Criterion with the projection:" $$
                                        nest 2 pi

instance (Info info (SubtermCriterionProof id), Ord id, Pretty id) =>
         Processor info SubtermCriterion (Problem Rewriting (NTRS id)) (Problem Rewriting (NTRS id))
  where
   apply SubtermCriterion p0
     | getMinimalityFromProblem p0 /= M = dontKnow (SubtermCriterionFailMinimality ::SubtermCriterionProof id) p0
     | otherwise = case subtermCriterion (getP p0) of
                                Nothing          -> mzero
                                Just (pTRS',prj) -> singleP (SubtermCriterionProof prj) p0 (setP pTRS' p0)

instance (Info info (SubtermCriterionProof id),Ord id, Pretty id) =>
         Processor info SubtermCriterion (Problem IRewriting (NTRS id)) (Problem IRewriting (NTRS id))
  where
   apply SubtermCriterion p0 = case subtermCriterion (getP p0) of
                                Nothing          -> mzero
{'fraction_non_alphanumeric': 0.07354323308270677, 'fraction_numerical': 0.0037593984962406013, 'mean_word_length': 3.31306990881459, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 15, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2355600', 'n_tokens_mistral': 1232, 'n_tokens_neox': 1219, 'n_words': 378}