module Term.Narrowing.Variants (
computeVariantsCheck
, module Term.Narrowing.Variants.Compute
, module Term.Narrowing.Variants.Check
) where
import Term.Narrowing.Variants.Compute
import Term.Narrowing.Variants.Check
import Term.Unification
import Control.Monad.Reader
computeVariantsCheck :: LNTerm -> WithMaude [LNSubstVFresh]
computeVariantsCheck t =
reader checkWithMaude
where
checkWithMaude hnd
| not $ run $ checkComplete t vars
= error $ "computeVariantsCheck: variant computation for "++ show t ++" failed. Computed set not complete."
| not $ run $ checkMinimal t vars
= error $ "computeVariantsCheck: variant computation for "++ show t ++" failed. Computed set not minimal."
| otherwise
= vars
where
vars = run $ computeVariants t
run = (`runReader` hnd)