{-# LANGUAGE TypeOperators, TemplateHaskell, DeriveDataTypeable, ScopedTypeVariables, TupleSections #-} -- | -- Copyright : (c) 2010-2012 Benedikt Schmidt -- License : GPL v3 (see LICENSE) -- -- Maintainer : Benedikt Schmidt -- Portability : GHC only -- -- Support for reasoning with and about disjunctions of substitutions. module Theory.Proof.EquationStore ( -- * Transformation simp , addEqs , addRuleVariants , splitAtPos , eqSplits , constrainedVarsPos , SplitStrategy(..) -- * simplify a disjunction , simpDisjunction ) where import Term.Unification import Logic.Connectives import Theory.Proof.Types import Control.Monad.Reader import Control.Monad.Fresh import Utils.Misc import Extension.Prelude -- import qualified Debug.Trace as DT import Debug.Trace.Ignore import Data.List import Data.Label hiding ( for ) import Data.Maybe import Data.Monoid import Data.Traversable hiding ( mapM ) import qualified Data.Foldable as F import Control.Basics import Control.Monad.State hiding (get, modify) import qualified Control.Monad.State as MS -- Equation Store ---------------------------------------------------------------------- -- | We use an empty disjunction to denote false. falseDisj :: Disj (LNSubstVFresh) falseDisj = Disj [] data SplitStrategy = SplitNow | SplitLater -- Dealing with equations ---------------------------------------------------------------------- -- | Returns the list of all @SplitId@s corresponding equation disjunctions. eqSplits :: EqStore -> [SplitId] eqSplits eqs = [0.. length (getConj . get eqsConj $ eqs) -1 ] -- | Add a list of term equalities to the equation store. -- Returns the resulting equation store(s) depending -- on the split strategy. addEqs :: MonadFresh m => SplitStrategy -> MaudeHandle -> [Equal LNTerm] -> EqStore -> m [EqStore] addEqs splitStrat hnd eqs0 eqStore = case unifyLNTermFactored eqs `runReader` hnd of (_, []) -> return [set eqsConj falseEqConstrConj eqStore] (subst, substs) -> case splitStrat of SplitLater -> return $ [addDisj (applyEqStore hnd subst eqStore) (Disj substs)] SplitNow -> addEqsAC (modify eqsSubst (compose subst) eqStore) <$> simpDisjunction hnd (Disj substs) where eqs = apply (get eqsSubst eqStore) $ trace (unlines ["addEqs: ", show eqs0]) $ eqs0 addEqsAC eqSt (sfree, Nothing) = [applyEqStore hnd sfree eqSt] addEqsAC eqSt (sfree, Just disj) = fromMaybe (error "addEqsSplit: impossible, splitAtPos failed") (splitAtPos (applyEqStore hnd sfree (addDisj eqSt (Disj disj))) 0) -- | Apply a substitution to an equation store and bring resulting equations into -- normal form again by using unification. applyEqStore :: MaudeHandle -> LNSubst -> EqStore -> EqStore applyEqStore hnd asubst eqStore | dom asubst `intersect` varsRange asubst /= [] || trace (show ("applyEqStore", asubst, eqStore)) False = error $ "applyS2EqStore: dom and vrange not disjoint for `"++show asubst++"'" | otherwise = modify eqsConj (fmap ((Disj . concatMap applyBound . getDisj))) $ set eqsSubst newsubst eqStore where newsubst = asubst `compose` get eqsSubst eqStore applyBound s = map (restrictVFresh (varsRange newsubst ++ domVFresh s)) $ (`runReader` hnd) $ unifyLNTerm [ Equal (apply newsubst (varTerm $ lv)) t | let slist = substToListVFresh s, -- variables in the range are fresh, so we have to rename -- them away from all other variables in unification problem -- NOTE: these variables never enter the global context let ran = renameAvoiding (map snd slist) (domVFresh s ++ varsRange newsubst), (lv,t) <- zip (map fst slist) ran ] {- NOTES for @applyEqStore tau@ to a fresh substitution sigma: [ FIXME: extend explanation to multiple unifiers ] Let dom(sigma) = x1,..,xk, vrange(sigma) = y1, .. yl, vrange(tau) = z1,..,zn Fresh substitution denotes formula exists #y1, .., #yl. x1 = t1 /\ .. /\ xk = tk for variables #yi that do not clash with xi and zi [renameAwayFrom] and with vars(ti) `subsetOf` [#y1, .. #yl]. We apply tau with vrange(tau) = z1,..,zn to the formula to obtain exists ##y1, .., ##yl. tau(x1) = t1 /\ .. /\ tau(xk) = tk unification then yields a lemma forall xi zi #yi. tau(x1) = t1 /\ .. /\ tau(xk) = tk <-> exists vars(s1,..sm). x1 = .. /\ z1 = .. /\ #y1 = .. So we have exists #y1, .., #yl. exists vars(s1,..sm). x1 = .. /\ z1 = .. /\ #y1 = .. <=> exists vars(s1,..sm). x1 = .. /\ z1 = .. /\ (exists #y1, .., #yl. #y1 = ..) <=> [restric] exists vars(s1,..sm). x1 = .. /\ z1 = .. /\ True -} -- | Add the given rule variants. addRuleVariants :: (Disj (LNSubstVFresh)) -> EqStore -> EqStore addRuleVariants (Disj substs) eqStore | dom freeSubst `intersect` concatMap domVFresh substs /= [] = error $ "addRuleVariants: Nonempty intersection between domain of variants and free substitution. " ++"This case has not been implemented, add rule variants earlier." | otherwise = addDisj eqStore (Disj substs) where freeSubst = get eqsSubst eqStore -- | Return the set of variables that is constrained by disjunction at give position. constrainedVarsPos :: EqStore -> Int -> [LVar] constrainedVarsPos eqStore k | k < length conj = frees (conj!!k) | otherwise = [] where conj = getConj . get eqsConj $ eqStore -- Internal functions ---------------------------------------------------------------------- -- | Add a disjunction to the equation store at the beginning addDisj :: EqStore -> (Disj (LNSubstVFresh)) -> EqStore addDisj eqStore disj = modify eqsConj ((Conj [disj]) `mappend`) eqStore -- | @splitEqStoreAt eqs i@ takes the disjunction at position @i@ in @eqs@ -- and returns a list of resulting substitutions and the equality store -- with the remaining equations. splitAtPos :: EqStore -> Int -> Maybe [EqStore] splitAtPos eqStore i | i `notElem` eqSplits eqStore = Nothing | otherwise = Just $ map (\d -> set eqsConj (conjNew d) eqStore) disj where conj = getConj $ get eqsConj eqStore disj = getDisj $ conj !! i conjNew d = Conj $ take i conj ++ [Disj [d]] ++ drop (i+1) conj -- Simplifying disjunctions ---------------------------------------------------------------------- -- | Simplify given disjunction via EqStore simplification. Obtains fresh -- names for variables from the underlying 'MonadFresh'. simpDisjunction :: MonadFresh m => MaudeHandle -> Disj (LNSubstVFresh) -> m (LNSubst, Maybe [LNSubstVFresh]) simpDisjunction hnd disj0 = do eqStore' <- simp hnd eqStore return (get eqsSubst eqStore', wrap $ get eqsConj eqStore') where eqStore = set eqsConj (Conj [disj0]) $ emptyEqStore wrap (Conj []) = Nothing wrap (Conj [Disj disj]) = Just $ disj wrap conj = error ("simplifyDisjunction: imposible, unexpected conjuction `" ++ show conj ++ "'") -- Simplification ---------------------------------------------------------------------- -- | @simp eqStore@ simplifies the equation store. simp :: MonadFresh m => MaudeHandle -> EqStore -> m EqStore simp hnd eqStore = (`execStateT` (trace (show ("eqStore", eqStore)) eqStore)) $ whileTrue (simp1 hnd) -- | @simp1@ tries to execute one simplification step -- for the equation store. It returns @True@ if -- the equation store was modified. simp1 :: MonadFresh m => MaudeHandle -> StateT EqStore m Bool simp1 hnd = do s <- MS.get b1 <- simpMinimize b2 <- simpRemoveRenamings b3 <- simpEmptyDisj b4 <- foreachDisj hnd simpSingleton b5 <- foreachDisj hnd simpAbstractSortedVar b6 <- foreachDisj hnd simpIdentify b7 <- foreachDisj hnd simpAbstractFun b8 <- foreachDisj hnd simpAbstractName s' <- MS.get (trace (show ("simp:", [b1, b2, b3, b4, b5, b6, b7, b8], s, s'))) $ return $ (or [b1, b2, b3, b4, b5, b6, b7, b8]) -- | Remove variable renamings in fresh substitutions. simpRemoveRenamings :: MonadFresh m => StateT EqStore m Bool simpRemoveRenamings = do conj <- gets (get eqsConj) let (conj',changed) = runState (traverse (traverse rmRenamings) conj) False when changed $ MS.modify (set eqsConj conj') return changed where rmRenamings :: LNSubstVFresh -> State Bool LNSubstVFresh rmRenamings subst = do let subst' = removeRenamings subst when (domVFresh subst /= domVFresh subst') $ put True return subst' -- | If empty disjunction is found, the whole conjunct -- can be simplified to False. simpEmptyDisj :: MonadFresh m => StateT EqStore m Bool simpEmptyDisj = do conj <- gets (get eqsConj) if (F.any (==falseDisj) conj && conj /= falseEqConstrConj) then MS.modify (set eqsConj falseEqConstrConj) >> return True else return False -- | If there is a singleton disjunction, it can be -- composed with the free substitution. simpSingleton :: MonadFresh m => Disj LNSubstVFresh -> m (Maybe (Maybe LNSubst, [Disj LNSubstVFresh])) simpSingleton (Disj [subst0]) = do subst <- freshToFree subst0 return (Just (Just subst, [])) simpSingleton _ = return Nothing -- | If all substitutions @si@ map a variable @v@ to terms with the same -- outermost function symbol @f@, then they all contain the common factor -- @{v |-> f(x1,..,xk)}@ for fresh variables xi and we can replace -- @x |-> ..@ by @{x1 |-> ti1, x2 |-> ti2, ..}@ in all substitutions @si@. simpAbstractFun :: MonadFresh m => Disj LNSubstVFresh -> m (Maybe (Maybe LNSubst, [Disj LNSubstVFresh])) simpAbstractFun (Disj []) = return Nothing simpAbstractFun (Disj (subst:others)) = case commonOperators of [] -> return Nothing -- abstract all arguments (v, o, argss@(args:_)):_ | all ((==length args) . length) argss -> do fvars <- mapM (\_ -> freshLVar "x" LSortMsg) args let substs' = zipWith (abstractAll v fvars) (subst:others) argss fsubst = substFromList [(v, FApp o (map varTerm fvars))] return $ Just (Just $ fsubst, [Disj substs']) -- abstract first two arguments (v, o@(AC _), argss):_ -> do fv1 <- freshLVar "x" LSortMsg fv2 <- freshLVar "x" LSortMsg let substs' = zipWith (abstractTwo o v fv1 fv2) (subst:others) argss fsubst = substFromList [(v, FApp o (map varTerm [fv1,fv2]))] return $ Just (Just $ fsubst, [Disj substs']) (_, _ ,_):_ -> error "simpAbstract: impossible, invalid arities or List operator encountered." where commonOperators = do (v, FApp o args) <- substToListVFresh subst let images = map (\s -> imageOfVFresh s v) others argss = [ args' | Just (FApp o' args') <- images, o' == o ] guard (length argss == length others) return (v, o, args:argss) abstractAll v freshVars s args = substFromListVFresh $ filter ((/= v) . fst) (substToListVFresh s) ++ zip freshVars args abstractTwo o v fv1 fv2 s args = substFromListVFresh $ filter ((/= v) . fst) (substToListVFresh s) ++ newMappings args where newMappings [] = error "simpAbstract: impossible, AC symbols must have arity >= 2." newMappings [a1,a2] = [(fv1, a1), (fv2, a2)] -- here we always abstract from left to right and do not -- take advantage of the AC property of o newMappings (a:as) = [(fv1, a), (fv2, FApp o as)] -- | If all substitutions @si@ map a variable @v@ to the same name @n@, -- then they all contain the common factor -- @{v |-> n}@ and we can remove @{v -> n} from all substitutions @si@ simpAbstractName :: MonadFresh m => Disj LNSubstVFresh -> m (Maybe (Maybe LNSubst, [Disj LNSubstVFresh])) simpAbstractName (Disj []) = return Nothing simpAbstractName (Disj (subst:others)) = case commonNames of [] -> return Nothing (v, c):_ -> return $ Just (Just $ substFromList [(v, c)] , [Disj (map (\s -> restrictVFresh (delete v (domVFresh s)) s) (subst:others))]) where commonNames = do (v, c@(Lit (Con _))) <- substToListVFresh subst let images = map (\s -> imageOfVFresh s v) others guard (length images == length [ () | Just c' <- images, c' == c]) return (v, c) -- | If all substitutions @si@ map a variable @v@ to variables @xi@ of the same -- sort @s@ then they all contain the common factor -- @{v |-> y}@ for a fresh variable of sort @s@ -- and we can replace @{v -> xi}@ by @{y -> xi} in all substitutions @si@ simpAbstractSortedVar :: MonadFresh m => Disj LNSubstVFresh -> m (Maybe (Maybe LNSubst, [Disj LNSubstVFresh])) simpAbstractSortedVar (Disj []) = return Nothing simpAbstractSortedVar (Disj (subst:others)) = case commonSortedVar of [] -> return Nothing (v, s, lvs):_ -> do fv <- freshLVar (lvarName v) s return $ Just (Just $ substFromList [(v, varTerm fv)] , [Disj (zipWith (replaceMapping v fv) lvs (subst:others))]) where commonSortedVar = do (v, (Lit (Var lx))) <- substToListVFresh subst guard (sortCompare (lvarSort v) (lvarSort lx) == Just GT) let images = map (\s -> imageOfVFresh s v) others -- FIXME: could be generalized to choose topsort s of all images if s < sortOf v -- could also be generalized to terms of a given sort goodImages = [ ly | Just (Lit (Var ly)) <- images, lvarSort lx == lvarSort ly] guard (length images == length goodImages) return (v, lvarSort lx, (lx:goodImages)) replaceMapping v fv lv sigma = substFromListVFresh $ (filter ((/=v) . fst) $ substToListVFresh sigma) ++ [(fv, varTerm lv)] -- | If all substitutions @si@ map two variables @x@ and @y@ to identical terms @ti@, -- then they all contain the common factor @{x |-> y} for a fresh variable @z@ -- and we can remove @{x |-> ti}@ from all @si@. simpIdentify :: MonadFresh m => Disj (LNSubstVFresh) -> m (Maybe (Maybe LNSubst, [Disj LNSubstVFresh])) simpIdentify (Disj []) = return Nothing simpIdentify (Disj (subst:others)) = case equalImgPairs of [] -> return Nothing ((v,v'):_) -> do let (vkeep, vremove) = case sortCompare (lvarSort v) (lvarSort v') of Just GT -> (v', v) Just _ -> (v, v') Nothing -> error $ "EquationStore.simpIdentify: impossible, variables with incomparable sorts: " ++ show v ++" and "++ show v' return $ Just (Just (substFromList [(vremove, varTerm vkeep)]), [Disj (map (removeMappings [vkeep]) (subst:others))]) where equalImgPairs = do (v,t) <- substToListVFresh subst (v', t') <- substToListVFresh subst guard (t == t' && v < v' && all (agrees_on v v') others) return (v,v') agrees_on v v' s = imageOfVFresh s v == imageOfVFresh s v' && isJust (imageOfVFresh s v) removeMappings vs s = restrictVFresh (domVFresh s \\ vs) s -- | Traverse disjunctions without msgBefore fact in conjunction and -- execute @f@ until it returns @Just (mfreeSubst, disjs)@. -- Then the @disjs@ is inserted at the current position, if @mfreeSubst@ is -- @Just freesubst@, then it is applied to the equation store. @True@ is -- returned if any modifications took place. foreachDisj :: MonadFresh m => MaudeHandle -> (Disj (LNSubstVFresh) -> m (Maybe (Maybe LNSubst, [Disj LNSubstVFresh]))) -> StateT EqStore m Bool foreachDisj hnd f = do conj <- gets (get eqsConj) go [] (getConj conj) where go _ [] = return False go lefts (d:rights) = do b <- lift $ f d case b of Nothing -> go (d:lefts) rights Just (msubst, disjs) -> do MS.modify (set eqsConj (Conj (reverse lefts ++ disjs ++ rights))) maybe (return ()) (\s -> MS.modify (applyEqStore hnd s)) msubst return True -- Renaming and subsumption ---------------------------------------------------------------------- -- | Simplify by removing substitutions that occur twice in a disjunct. -- We could generalize this function by using AC-equality or subsumption. simpMinimize :: MonadFresh m => StateT EqStore m Bool simpMinimize = do eqs <- MS.get let eqs' = modify eqsConj (fmap (Disj . sortednub . getDisj)) eqs MS.put eqs' return (eqs /= eqs') {- t2 = simpAbstract (Disj (map substFromListVFresh [s1,s2])) `evalFresh` nothingUsed where s1 = [(lx1,pair(y1,y2))] s2 = [(lx1,pair(inv(y1),inv(y2)))] t3 = simpAbstract (Disj (map substFromListVFresh [s1,s2,s3])) `evalFresh` nothingUsed where s1 = [(lx1, mult [y1,y2] )] s2 = [(lx1, mult [inv(y1), inv(y2), inv(y3)])] s3 = [(lx1, mult[y5, y6, y7, y8])] t4 = simpIdentify (Disj (map substFromListVFresh [s1,s2])) `evalFresh` nothingUsed where s1 = [(lx1, mult [y1,y2,y3] ), (lx2, mult [y1,y2,y3] )] s2 = [(lx1, mult [inv(y1), inv(y2), inv(y3)]), (lx2, mult [inv(y1), inv(y2), inv(y3)])] -} {- t5 = simpAbstractFun (Disj (map substFromListVFresh [s1,s2,s3])) `evalFresh` nothingUsed where s1 = [(lx1, mult [y1,y2] )] s2 = [(lx1, x3)] s3 = [(lx1, mult[y5, y6, y7, y8])] t6 = simpIdentify (Disj (map substFromListVFresh [s1,s2,s3])) `evalFresh` nothingUsed where s1 = [(lx1, mult [y1,y2,y3] ), (lx2, mult [y1,y2,y3] )] s2 = [(lx1, mult [inv(y1), inv(y2), inv(y3)]), (lx2, mult [inv(y1), inv(y2), inv(y3)])] s3 = [(lx1, y1), (lx2, y2)] -}