------------------------------------------------------------------------------
--- Library for representation and computation of critical pairs.
---
--- @author Jan-Hendrik Matthes
--- @version August 2016
--- @category algorithm
------------------------------------------------------------------------------

module Rewriting.CriticalPairs
  ( CPair
  , showCPair, showCPairs, cPairs, isOrthogonal, isWeakOrthogonal
  ) where

import List (nub)
import Rewriting.Position (eps, positions, (|>), replaceTerm)
import Rewriting.Rules
import Rewriting.Substitution (applySubst)
import Rewriting.Term (Term, showTerm, isConsTerm)
import Rewriting.Unification (unify)

-- ---------------------------------------------------------------------------
-- Representation of critical pairs
-- ---------------------------------------------------------------------------

--- A critical pair represented as a pair of terms and parameterized over the
--- kind of function symbols, e.g., strings.
type CPair f = (Term f, Term f)

-- ---------------------------------------------------------------------------
-- Pretty-printing of critical pairs
-- ---------------------------------------------------------------------------

-- \x3008 = LEFT ANGLE BRACKET
-- \x3009 = RIGHT ANGLE BRACKET

--- Transforms a critical pair into a string representation.
showCPair :: (f -> String) -> CPair f -> String
showCPair s (l, r) = "\x3008" ++ (showTerm s l) ++ ", " ++ (showTerm s r)
                       ++ "\x3009"

--- Transforms a list of critical pairs into a string representation.
showCPairs :: (f -> String) -> [CPair f] -> String
showCPairs s = unlines . (map (showCPair s))

-- ---------------------------------------------------------------------------
-- Computation of critical pairs
-- ---------------------------------------------------------------------------

--- Returns the critical pairs of a term rewriting system.
cPairs :: TRS f -> [CPair f]
cPairs trs
  = let trs' = maybe trs (\v -> renameTRSVars (v + 1) trs) (maxVarInTRS trs)
     in nub [(applySubst sub r1,
              replaceTerm (applySubst sub l1) p (applySubst sub r2)) |
             rule1@(l1, r1) <- trs',
             p <- positions l1, let l1p = l1 |> p, isConsTerm l1p,
             rule2@(l2, r2) <- trs,
             (Right sub) <- [unify [(l1p, l2)]],
             (p /= eps) || (not (isVariantOf rule1 rule2))]

-- ---------------------------------------------------------------------------
-- Functions for term rewriting systems and critical pairs
-- ---------------------------------------------------------------------------

--- Checks whether a term rewriting system is orthogonal.
isOrthogonal :: TRS _ -> Bool
isOrthogonal trs = (isLeftLinear trs) && (null (cPairs trs))

--- Checks whether a term rewriting system is weak-orthogonal.
isWeakOrthogonal :: TRS _ -> Bool
isWeakOrthogonal trs = (isLeftLinear trs) && (all (uncurry (==)) (cPairs trs))