module Term.SubtermRule (
StRhs(..)
, StRule(..)
, rRuleToStRule
, stRuleToRRule
, 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
data StRhs = RhsGround LNTerm | RhsPosition Position
deriving (Show,Ord,Eq)
data StRule = StRule LNTerm StRhs
deriving (Show,Ord,Eq)
rRuleToStRule :: RRule LNTerm -> Maybe StRule
rRuleToStRule (lhs `RRule` rhs)
| frees rhs == [] = Just $ StRule lhs (RhsGround rhs)
| otherwise = case findSubterm lhs [] of
[]:_ -> Nothing
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 _) _ = []
stRuleToRRule :: StRule -> RRule LNTerm
stRuleToRRule (StRule lhs rhs) = case rhs of
RhsGround t -> lhs `RRule` t
RhsPosition p -> lhs `RRule` (lhs `atPos` p)
prettyStRule :: HighlightDocument d => StRule -> d
prettyStRule r = case stRuleToRRule r of
(lhs `RRule` rhs) -> sep [ nest 2 $ prettyLNTerm lhs
, operator_ "=" <-> prettyLNTerm rhs ]
$(derive makeBinary ''StRhs)
$(derive makeBinary ''StRule)
$(derive makeNFData ''StRhs)
$(derive makeNFData ''StRule)