content: -- |
  -- Copyright   : (c) 2010-2012 Benedikt Schmidt
  -- License     : GPL v3 (see LICENSE)
  --
  --
  -- One-step narrowing from a term.
  module Term.Narrowing.Narrow (
      narrowSubsts
    ) where
  
  import           Term.Unification
  import           Term.Positions
  
  import           Control.Monad
  import           Control.Monad.Reader
  
  import           Extension.Prelude
  import qualified Data.Set as S
  
  import           Debug.Trace.Ignore
  
  -- Narrowing
  ----------------------------------------------------------------------
  
  -- | @narrowSubsts rules t@ returns all substitutions @s@ such that there is a
  --   narrowing step for the term @t@ and the given rules.
  --   Formally: If there is a step @(t,s(t[r]p),p,s,l->r)@ such that @p@ is a
  --   non-variable position of @t@ and @s@ is an element of the complete set of
  --   unifiers of @t|_p@ with @l@ (wrt. to 'unifyLNTerm') for the rule @l -> r@,
  --   then @s@ is included in the list of returned substitutions.
  narrowSubsts :: LNTerm -> WithMaude [LNSubstVFresh]
  narrowSubsts t = reader $ \hnd -> sortednub $ do
      let rules0 = S.toList . rrulesForMaudeSig $ mhMaudeSig hnd
      (l `RRule` _r) <- renameAvoiding rules0 t
      p <- positionsNonVar t
      subst <- unifyLNTerm [Equal (t `atPos` p) l] `runReader` hnd
      guard (trace ("narrowSubsts"++ (show ((t `atPos` p), l, restrictVFresh (frees t) subst))) True)
      return $ restrictVFresh (frees t) subst
  