-- |
-- Copyright   : (c) 2010-2012 Benedikt Schmidt
-- License     : GPL v3 (see LICENSE)
-- 
-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>
--
-- One-step narrowing from a term.
module Term.Narrowing.Narrow (
    narrowSubsts
  ) where

import           Term.Unification
import           Term.Positions

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