content: {-# LANGUAGE ViewPatterns #-}
  -- |
  -- Copyright   : (c) 2010-2012 Benedikt Schmidt
  -- License     : GPL v3 (see LICENSE)
  --
  --
  -- Subsumption of terms and substitutions.
  module Term.Subsumption (
      compareTermSubs
    , eqTermSubs
  
    , factorSubstVia
  
    -- * Canonical representations for substitutions
    --   modulo renaming
    , canonizeSubst
  
    -- * for testing only
    , varOccurences
  ) where
  
  -- import Control.Basics
  
  -- import Data.Monoid
  
  import Extension.Prelude
  
  import Term.LTerm
  import Term.Unification
  
  
  ----------------------------------------------------------------------
  -- Subsumption order on terms and substitutions
  ----------------------------------------------------------------------
  
  -- | Compare terms @t1@ and @t2@ with respect to the subsumption order modulo AC.
  compareTermSubs :: LNTerm -> LNTerm -> WithMaude (Maybe Ordering)
  compareTermSubs t1 t2 = do
      check <$> solveMatchLNTerm (t1 `matchWith` t2)
            <*> solveMatchLNTerm (t2 `matchWith` t1)
    where
      check []    []    = Nothing
      check (_:_) []    = Just GT
      check []    (_:_) = Just LT
      check (_:_) (_:_) = Just EQ
  
  -- | Returns True if @s1@ and @s2@ are equal with respect to the subsumption order modulo AC.
  eqTermSubs :: LNTerm -> LNTerm -> WithMaude Bool
  eqTermSubs s1 s2 = (== Just EQ) <$> compareTermSubs s1 s2
  
  -- | @factorSubstOn s1 s2 vs@ factors the free substitution @s1@
  --   through free substitution @s2@ on @vs@,
  --   i.e., find a complete set of free substitutions s such that for all
  --   vars @x `elem` vs@:
  --   >  applyVTerm s1 x =AC= applyVTerm s (applyVTerm s2 x).
  factorSubstVia :: [LVar] -> LNSubst -> LNSubst -> WithMaude [LNSubst]
  factorSubstVia vs s1 s2 =
      solveMatchLNTerm (mconcat matches)
    where
      matches :: [Match LNTerm]
      matches = zipWith matchWith (substToListOn vs s1) (substToListOn vs s2)
  
  ----------------------------------------------------------------------
  -- Equality of substitutions modulo AC and renaming
  ----------------------------------------------------------------------
  
  -- | Returns a substitution that is equivalent modulo renaming to the given substitution.
  canonizeSubst :: LNSubstVFresh -> LNSubstVFresh
  canonizeSubst subst =
      mapRangeVFresh (applyVTerm renaming) subst
    where
      occs         = varOccurences $ rangeVFresh subst
      vrangeSorted = sortOn (`lookup` occs) (varsRangeVFresh subst)
      renaming = substFromList $
                   zipWith (\lv i -> (lv, varTerm $ LVar "x" (lvarSort lv) i))
                           vrangeSorted [1..]