{-# LANGUAGE TemplateHaskell, FlexibleInstances, DeriveDataTypeable, ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
  -- spurious warnings for view patterns
-- |
-- Copyright   : (c) 2011-2012 Benedikt Schmidt
-- License     : GPL v3 (see LICENSE)
-- 
-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>
--
-- Subterm rewriting rules.
module Term.SubtermRule (
      StRhs(..)
    , StRule(..)
    , rRuleToStRule
    , stRuleToRRule

    -- * Pretty Printing
    , prettyStRule
    , module Term.Rewriting.Definitions
    ) where

import Control.DeepSeq

import Data.DeriveTH
import Data.Binary

import Term.LTerm
import Term.Positions
import Term.Rewriting.Definitions
import Text.PrettyPrint.Highlight

-- | The righthand-side of a subterm rewrite rule.
--   Does not enforce that the term for RhsGround must be ground.
data StRhs = RhsGround LNTerm | RhsPosition Position
    deriving (Show,Ord,Eq)

-- | A subterm rewrite rule.
data StRule = StRule LNTerm StRhs
    deriving (Show,Ord,Eq)

-- | Convert a rewrite rule to a subterm rewrite rule if possible.
rRuleToStRule :: RRule LNTerm -> Maybe StRule
rRuleToStRule (lhs `RRule` rhs)
  | frees rhs == [] = Just $ StRule lhs (RhsGround rhs)
  | otherwise       = case findSubterm lhs [] of
                        []:_     -> Nothing  -- proper subterm required
                        pos:_    -> Just $ StRule lhs (RhsPosition (reverse pos))
                        []       -> Nothing
  where
    findSubterm t rpos | t == rhs  = [rpos]
    findSubterm (viewTerm -> FApp _ args) rpos =
        concat $ zipWith (\t i -> findSubterm t (i:rpos)) args [0..]
    findSubterm (viewTerm -> Lit _)         _  = []

-- | Convert a subterm rewrite rule to a rewrite rule.
stRuleToRRule :: StRule -> RRule LNTerm
stRuleToRRule (StRule lhs rhs) = case rhs of
                                     RhsGround t   -> lhs `RRule` t
                                     RhsPosition p -> lhs `RRule` (lhs `atPos` p)

------------------------------------------------------------------------------
-- Pretty Printing
------------------------------------------------------------------------------

-- | Pretty print an 'StRule'
prettyStRule :: HighlightDocument d => StRule -> d
prettyStRule r = case stRuleToRRule r of
  (lhs `RRule` rhs) -> sep [ nest 2 $ prettyLNTerm lhs
                           , operator_ "=" <-> prettyLNTerm rhs ]

-- derived instances
--------------------

$(derive makeBinary ''StRhs)
$(derive makeBinary ''StRule)

$(derive makeNFData ''StRhs)
$(derive makeNFData ''StRule)