{-# 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..]