module Term.Rewriting.Norm (
norm'
, nf'
, nfSubstVFresh'
, normSubstVFresh'
, maybeNotNfSubterms
) where
import Term.LTerm
import Term.Maude.Process
import Term.Maude.Signature
import Term.Substitution
import Term.SubtermRule
import Term.Unification
import Utils.Misc
import Control.Basics
import Control.Monad.Reader
import Data.List
import qualified Data.Set as S
import System.IO.Unsafe (unsafePerformIO)
norm :: (Show (Lit c LVar), Ord c, IsConst c)
=> (c -> LSort) -> LTerm c -> WithMaude (LTerm c)
norm _ t@(viewTerm -> Lit _) = return t
norm sortOf t = reader $ \hnd -> unsafePerformIO $ normViaMaude hnd sortOf t
norm' :: LNTerm -> WithMaude LNTerm
norm' = norm sortOfName
nfViaHaskell :: LNTerm -> WithMaude Bool
nfViaHaskell t0 = reader $ \hnd -> check hnd
where
check hnd = go t0
where
go t = case viewTerm2 t of
FAppNonAC o ts | o `S.member` irreducible -> all go ts
FList ts -> all go ts
FPair t1 t2 -> go t1 && go t2
One -> True
Empty -> True
Zero -> True
Lit2 _ -> True
FAppNonAC _ _ | setAny (struleApplicable t) strules -> False
FExp (viewTerm2 -> FExp _ _) _ | dh -> False
FExp _ (viewTerm2 -> One) | dh -> False
FInv (viewTerm2 -> FInv _) | dh -> False
FInv (viewTerm2 -> FMult ts) | dh && any isInverse ts -> False
FInv (viewTerm2 -> One) | dh -> False
FMult ts | fAppOne `elem` ts || any isProduct ts || invalidMult ts -> False
FXor ts | fAppZero `elem` ts || any isXor ts || not (noDuplicates ts) -> False
FUnion ts | fAppEmpty `elem` ts || any isUnion ts -> False
FExp t1 t2 -> go t1 && go t2
FInv t1 -> go t1
FMult ts -> all go ts
FXor ts -> all go ts
FUnion ts -> all go ts
FAppNonAC _ ts -> all go ts
struleApplicable t (StRule lhs rhs) =
case solveMatchLNTerm (t `matchWith` lhs) `runReader` hnd of
[] -> False
_:_ -> case rhs of
RhsPosition _ -> True
RhsGround s -> not (t == s)
invalidMult ts = case partition isInverse ts of
([],_) -> False
([ viewTerm2 -> FInv (viewTerm2 -> FMult ifactors) ], factors) ->
(ifactors \\ factors /= ifactors) || (factors \\ ifactors /= factors)
([ viewTerm2 -> FInv t ], factors) -> t `elem` factors
(_:_:_, _) -> True
_ -> False
msig = mhMaudeSig hnd
strules = stRules msig
irreducible = irreducibleFunctionSymbols msig
dh = enableDH msig
nf' :: LNTerm -> WithMaude Bool
nf' = nfViaHaskell
nfViaMaude :: (Show (Lit c LVar), Ord c, IsConst c)
=> (c -> LSort) -> LTerm c -> WithMaude Bool
nfViaMaude sortOf t = (t ==) <$> norm sortOf t
_nfCompare' :: LNTerm -> WithMaude Bool
_nfCompare' t0 = reader $ \hnd ->
case ((nfViaMaude sortOfName t0) `runReader` hnd, (nfViaHaskell t0) `runReader` hnd) of
(x, y) | x == y -> x
(x, y) ->
error $ "nfCompare: Maude disagrees with haskell nf: "++ show t0
++" maude: " ++ show x ++ " haskell: "++show y
nfSubstVFresh' :: LNSubstVFresh -> WithMaude Bool
nfSubstVFresh' s = reader $ \hnd -> all (\t -> runReader (nf' t) hnd) (rangeVFresh s)
normSubstVFresh' :: LNSubstVFresh -> WithMaude LNSubstVFresh
normSubstVFresh' s = reader $ \hnd -> mapRangeVFresh (\t -> norm' t `runReader` hnd) s
maybeNotNfSubterms :: MaudeSig -> LNTerm -> [LNTerm]
maybeNotNfSubterms msig t0 = go t0
where irreducible = irreducibleFunctionSymbols msig
go (viewTerm -> Lit _) = []
go (viewTerm -> FApp (NonAC o) as) | o `S.member` irreducible = concatMap go as
go t = [t]