{-# LANGUAGE PatternGuards, FlexibleContexts #-}
-- |
-- Copyright   : (c) 2010, 2011 Benedikt Schmidt
-- License     : GPL v3 (see LICENSE)
-- 
-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>
--
-- This module implements normalization with respect to DH u AC using class
-- rewriting and an ad-hoc function that uses the @TermAC@ representation of
-- terms modulo AC. 
module Term.Rewriting.Norm (
    norm
  , norm'
  , nf
  , nf'
  , nfSubstVFresh'
  , normSubstVFresh'
) where

import Term.Term
import Term.LTerm
import Term.Rewriting.NormAC
import Term.Substitution
import Term.Maude.Process

import Control.Basics
import Control.Monad.Reader

import System.IO.Unsafe (unsafePerformIO)

-- Normalization using Maude
----------------------------------------------------------------------

-- | @norm t@ normalized the term @t@ using Maude.
norm :: (Show (Lit c LVar), Ord c, IsConst c)
     => (c -> LSort) -> VTerm c LVar -> WithMaude (VTerm c LVar)
norm _      t@(Lit _) = return t
norm sortOf t         = reader $ \hnd -> normAC $ unsafePerformIO $ normViaMaude hnd sortOf t

norm' :: LNTerm -> WithMaude LNTerm
norm' = norm sortOfName

-- | @nf t@ returns @True@ if the term @t@ is in normal form.
nf :: (Show (Lit c LVar), Ord c, IsConst c)
   => (c -> LSort) -> VTerm c LVar -> WithMaude Bool
nf sortOf t = (t ==#) <$>  norm sortOf t

nf' :: LNTerm -> WithMaude Bool
nf' = nf sortOfName

-- Normalization 
----------------------------------------------------

-- | @nfSubst s@ returns @True@ if the substitution @s@ is in normal form.
nfSubstVFresh' ::  LNSubstVFresh -> WithMaude Bool
nfSubstVFresh' s = reader $ \hnd -> all (\t -> runReader (nf' t) hnd) (rangeVFresh s)

{-
-- | @normSubst s@ normalizes the substitution @s@.
normSubst :: (IsConst c, IsVar v, Show (Lit c v)) => Subst c v -> Subst c v
normSubst s = mapRange norm s

-}

-- | @normSubst s@ normalizes the substitution @s@.
normSubstVFresh' :: LNSubstVFresh -> WithMaude LNSubstVFresh
normSubstVFresh' s = reader $ \hnd -> mapRangeVFresh (\t -> norm' t `runReader` hnd) s