<commit_before>{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances, FlexibleInstances #-}
{-# LANGUAGE RecordWildCards #-}
module Narradar.Processor.RelativeProblem where

import Data.Monoid

import Narradar.Constraints.Modularity
import Narradar.Framework
import Narradar.Framework.Ppr
import Narradar.Types

data RelativeToRegular = RelativeToRegular
data RelativeToRegularProof = RelativeToRegularProof | RelativeToRegularProofFail
          deriving (Eq, Ord, Show)

instance Pretty RelativeToRegularProof where
    pPrint RelativeToRegularProof = text "The two systems form a Generalized Hierarchical Combination" $$
                                    text "and hence the result from LOPSTR09 applies." $$
                                    text "Termination of the following DP problem implies relative termination."
    pPrint RelativeToRegularProofFail = text "The two systems do not form a Generalized" $$
                                        text "Hierarchical Combination and hence we cannot apply" $$
                                        text "the result from LOPSTR09."

instance ( MkProblem base trs
         , SignatureId trs ~ TermId t
         , Ord (t(Term t v)), Ord v, Enum v, HasId t, Match t
         , Monoid trs, HasRules t v trs, HasSignature trs
         , Info info RelativeToRegularProof<commit_msg>- Generalized<commit_after>{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances, FlexibleInstances #-}
{-# LANGUAGE RecordWildCards #-}
module Narradar.Processor.RelativeProblem where

import Data.Monoid

import Narradar.Constraints.Modularity
import Narradar.Framework
import Narradar.Framework.Ppr
import Narradar.Types

data RelativeToRegular = RelativeToRegular
data RelativeToRegularProof = RelativeToRegularProof | RelativeToRegularProofFail
          deriving (Eq, Ord, Show)

instance Pretty RelativeToRegularProof where
    pPrint RelativeToRegularProof = text "The two systems form a  Hierarchical Combination" $$
                                    text "and hence the result from LOPSTR09 applies." $$
                                    text "Termination of the following DP problem implies relative termination."
    pPrint RelativeToRegularProofFail = text "The two systems do not form a " $$
                                        text "Hierarchical Combination and hence we cannot apply" $$
                                        text "the result from LOPSTR09."

instance ( MkProblem base trs
         , SignatureId trs ~ TermId t
         , Ord (t(Term t v)), Ord v, Enum v, HasId t, Match t
         , Monoid trs, HasRules t v trs, HasSignature trs
         , Info info RelativeToRegularProof
{'fraction_non_alphanumeric': 0.06218181818181818, 'fraction_numerical': 0.002909090909090909, 'mean_word_length': 2.663115845539281, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 16, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3941895', 'n_tokens_mistral': 770, 'n_tokens_neox': 707, 'n_words': 244}