{-# LANGUAGE ViewPatterns #-}
-- |
-- Copyright   : (c) 2010-2012 Benedikt Schmidt
-- License     : GPL v3 (see LICENSE)
--
-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>
--
-- 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..]