module Term.Narrowing.Variants.Check (
checkComplete
, checkMinimal
, variantsFrom
, isNormalInstance
, leqSubstVariant
) where
import Term.Substitution
import Term.Unification
import Term.Rewriting.Norm
import Term.Subsumption (factorSubstVia,canonizeSubst)
import Term.Narrowing.Narrow
import Extension.Prelude
import Utils.Misc
import Control.Basics
import Control.Monad.Reader
import Data.List
import Debug.Trace.Ignore
isNormalInstance :: LNTerm -> LNSubst -> LNSubst -> WithMaude Bool
isNormalInstance t s s' =
do t' <- norm' (applyVTerm s t)
nf' (applyVTerm s' t')
leqSubstVariant :: LNTerm -> LNSubstVFresh -> LNSubstVFresh -> WithMaude Bool
leqSubstVariant t s1_0 s2_0 = reader $ \hnd ->
s1_0 == s2_0 ||
any (\s -> isNormalInstance t s2 s `runReader` hnd)
( (factorSubstVia tvars s1 s2 `runReader` hnd))
where
tvars = frees t
s1 = restrictVFresh tvars s1_0 `freshToFreeAvoiding` t
s2 = restrictVFresh tvars s2_0 `freshToFreeAvoiding` t
checkComplete :: LNTerm
-> [LNSubstVFresh]
-> WithMaude Bool
checkComplete t substs0 = reader $ \hnd ->
let newSubsts = concatMap ((`runReader` hnd) . variantsFrom t) substs
substs = sortOn (size &&& length . varsRangeVFresh) substs0
in
emptySubstVFresh `elem` substs0 &&
all (\s -> not $ isMaximalIn s substs t `runReader` hnd) newSubsts
variantsFrom :: LNTerm
-> LNSubstVFresh
-> WithMaude [LNSubstVFresh]
variantsFrom t substFrom0 = reader $ \hnd -> (\res -> trace (show ("variantsFrom", t, substFrom0, res)) res) $ sortednub $ do
let substFrom = substFrom0 `freshToFreeAvoiding` t
substTo0 <- (narrowSubsts =<< (norm' (applyVTerm substFrom t))) `runReader` hnd
let substTo = restrictVFresh (frees t) $ composeVFresh substTo0 substFrom
guard (nfSubstVFresh' substTo `runReader` hnd)
return $ canonizeSubst $ removeRenamings $ substTo
isMaximalIn :: LNSubstVFresh -> [LNSubstVFresh] -> LNTerm -> WithMaude Bool
isMaximalIn s substs t = reader $ \hnd ->
all (\s' -> (\res -> trace (show ("isMaximal:", not res , "=", s, "<=", s')) res ) $
not (leqSubstVariant t s s' `runReader` hnd)) substs
checkMinimal :: LNTerm -> [LNSubstVFresh] -> WithMaude Bool
checkMinimal t substs = reader $ \hnd ->
noDuplicates substs &&
all (\s -> (\res -> trace (show (s,substs,res)) res) $
(`runReader` hnd) $ isMaximalIn s (delete s substs) t) substs