```-- |
-- Copyright   : (c) 2010, 2011 Benedikt Schmidt
--
-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>
--
-- Completeness and minimality checking for the variants of a term.
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 Data.List

import Debug.Trace.Ignore

-- Variant Order
----------------------------------------------------------------------

-- | @isNormalInstance t s s'@ returns @True@ if @s'(norm(s(t)))@ is in normal
--   form.
isNormalInstance :: LNTerm -> LNSubst -> LNSubst -> WithMaude Bool
isNormalInstance t s s' = {- trace ("isnormalInstance " ++ show (t,s,s')) \$ -}
do t' <- norm' (applyVTerm s t)
nf' (applyVTerm s' t')

-- | @leqSubstVariant t s1 s2@ compares two substitutions using the variant order
--   with respect to @t@ and returns @True@ if @s1@ is less or equal than @s2@
--   and @False@ otherwise. Use the more expensive @compareSubstVariant@
--   which uses two AC matchings instead of one if you also want to distinguish
--   @Nothing@, @Just EQ@, and @Just GT@.
--
--   s1 is smaller or equal to s2 wrt. to the variant order (less general) iff there
--   is an s1' such that s1 = s2' . s2 restricted to vars(t) and s2'(norm(s2(t)))
--   is in normal form, or equivalently norm(s1(t)) =AC= s2'(norm(s2(1))). This
--   means s1 is redundant since it is just an AC instance of s2 that does
--   not "require additional normalization steps."
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)
( {- (\x -> trace (show x) x) -} (factorSubstVia tvars s1 s2 `runReader` hnd))
where
tvars = frees t
s1 = restrictVFresh tvars s1_0 `freshToFreeAvoiding` t
s2 = restrictVFresh tvars s2_0 `freshToFreeAvoiding` t

-- Completeness checking for a set of variants
----------------------------------------------------------------------

-- | @checkComplete t substs@ checks if @substs@ is a complete set of variants
--   for @t@ and returns @Just (subst1,subst2)@ if there is a narrowing step
--   from @subst1@ that yields a new variant @subst2@.
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 rules t subst@ returns all the "one-step variants" of
--   @norm (t subst)@ for the given set of @rules@.
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) -- prune substitutions that are not in normal-form
return \$ canonizeSubst \$ removeRenamings \$ substTo

-- | @isMaximalIn s substs t@ returns @True@ if @s@ is minimal in substs wrt.
--   <_Var^t, i.e., the function returns @True@ if there is no s'
--   in substs with s' <=_Var^t s.
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

-- Minimality checking for a set of variants
----------------------------------------------------------------------

-- | @checkMinimal t substs@ checks if @substs@ is a minimal set of variants
--   for @t@ and returns @False@ if there are subst1 /= subst2 in substs with
--   subst1 <=_Var_t subst2.
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
```