{-# 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 AC.
module Term.Rewriting.NormAC (
    (==#)
  , termFlatten
  , normAC
) where

import Term.Term

import Data.List ( sort )

-- Normalization modulo AC = flatten + sort
----------------------------------------------------------------------

-- | @termFlatten t@ converts a term @t@ to its flat representation, i.e.,
--   AC-operator applications are replaced by n-ary, non-nested
--   AC-operator applications.
termFlatten :: (Ord a) => Term a -> Term a
termFlatten t =
    go t
  where
    go (Lit l) = Lit l
    go (FApp (AC o) as) = FApp (AC o) (concatMap collectOTerms (map go as))
      where
        collectOTerms (FApp (AC o') ts) | o == o' = ts
        collectOTerms a                           = [a]
    go (FApp o as)      = FApp o (map go as)

-- | @normAC t@ normalizes the term @t@ wrt. to the equations AC,
-- i.e., by flattening and sorting wrt. Ord.
normAC :: (Ord t) => Term t -> Term t
normAC = foldTerm Lit (\o -> FApp o . sortAC o) . termFlatten
  where
    sortAC (AC _) as = sort as
    sortAC _      as = as

-- | @a ==# b@ returns @True@ if @a@ is equal @b@ modulo AC.
(==#) :: (Ord a) => Term a -> Term a -> Bool
a ==# b = normAC a == normAC b