content: -- |
  -- Copyright   : (c) 2010-2012 Benedikt Schmidt
  -- License     : GPL v3 (see LICENSE)
  --
  --
  -- Computing and checking the variants of a term.
  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
  
  -- | @variantsListCheck ts@ computes all variants of @ts@ considered as a single term
  --   without a bound or symmetry substitution. Before returning the result, it checks
  --   if the set of variants is complete and minimal. If that is not the case, it
  --   fails with an error
  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)
  