-- -- Copyright (C) 2005 Stefan Wehr - http://www.stefanwehr.de -- -- This program is free software; you can redistribute it and/or -- modify it under the terms of the GNU General Public License as -- published by the Free Software Foundation; either version 2 of -- the License, or (at your option) any later version. -- -- This program is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -- General Public License for more details. -- -- You should have received a copy of the GNU General Public License -- along with this program; if not, write to the Free Software -- Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -- 02111-1307, USA. -- module Phrac.Entailment where import Monad ( msum, filterM, liftM ) import Maybe ( mapMaybe ) import List ( partition ) import Phrac.Symtab import Phrac.AbstractSyntax import Phrac.Substitution import Phrac.Unification import Phrac.Error import Phrac.Pretty -- `bySuper p' returns the constraints that are implied by p through -- the superclass relation. bySuper :: ClassConstraint -> ST [ClassConstraint] bySuper p@(ClassConstraint i ts) = do cdec <- findClass i let s = substFromAssocs (zip (class_params cdec) ts) superConstraints <- findAllSuperConstraints i let res = p : (applySubst s superConstraints) debug ("bySuper " ++ showPpr p ++ " = " ++ showCommaListed res) return res -- `byInst p' returns `Just l' if p matches any instance declaration. `l' is -- then the list of subgoals. byInst :: ClassConstraint -> ST (Maybe [Constraint]) byInst p@(ClassConstraint i _) = do insts <- findInstances i candidates <- sequence [tryInst it | it <- insts] case msum candidates of Nothing -> do debug ("constraint " ++ showPpr' p ++ " is not satisfied by any instance declaration") return Nothing Just (ci, goals) -> do debug ("Constraint " ++ showPpr' p ++ " is satisfied by the " ++ "instance declaration " ++ showInstHead ci ++ ", provided the following subgoals are satisfied: " ++ showCommaListed goals) return $ Just goals where tryInst ci = do u <- matchConstraint (inst_class ci, inst_types ci) p case u of Nothing -> return Nothing Just u' -> return $ Just (ci, map (applySubst u') (inst_constraints ci)) -- -- NOTE: don't know if entailment is correct. I think I should apply the -- substitution returned from unification (when checking entailment for -- eq-constraints) to something. -- -- entail uses the program's class and equality definitions implicitly, -- i.e. `entail cs c' checks if `Theta, cs ||- c' holds, where Theta are -- the program constraints. entail :: [Constraint] -> Constraint -> ST Bool entail cs c = do debug ("checking if " ++ dumpConstraints cs ++ " entail " ++ showPpr' c) answ <- entail' cs c if answ then debug (dumpConstraints cs ++ " entail " ++ showPpr' c) else debug (dumpConstraints cs ++ " do not entail " ++ showPpr' c) return answ entail' ps (CC cc@(ClassConstraint c ts)) = do ts' <- mapM (\t -> runUF (toEqDefs ps) (normalise t)) ts let p = ClassConstraint c ts' debug ("checking entailment of class constraint " ++ showPpr' cc ++ ", so normalizing rhs first. Result: " ++ showPpr' p) supers <- mapM bySuper (classConstraints ps) if any (p `elem`) supers then return True else do insts <- byInst p case insts of Nothing -> return False Just qs -> do l <- mapM (entail ps) qs return (and l) entail' ps (EC e@(EqConstraint left right)) = do let ps' = toEqDefs ps ures <- runUnify ps' [TyAssoc left :=: right] case ures of Right (peqs, _) -> return (null peqs) Left _ -> return False toEqDefs :: [Constraint] -> [EqualityDefinition] toEqDefs ps = mapMaybe toEqDef ps toEqDef (CC _) = Nothing toEqDef (EC e) = Just $ EqualityDefinition [] e -- We try to bring the class constraints into HNF. However, if this fails -- for some constraint, we return the constraint unchanged rather than -- reporting an error. simplifyToplevel :: [Constraint] -> ST [Constraint] simplifyToplevel ps = let (cs,es) = splitConstraints ps in do qs <- toHnfs' cs return (qs ++ map EC es) where toHnfs' :: [ClassConstraint] -> ST [Constraint] toHnfs' ps = do pss <- mapM toHnf ps return (concat pss) toHnf :: ClassConstraint -> ST [Constraint] toHnf p | inHnf p = return [CC p] | otherwise = do subs <- byInst p case subs of Nothing -> return [CC p] Just ps -> simplifyToplevel ps inHnf cc = all hnf (cc_params cc) where hnf (TyVar _) = True hnf (TyApp l _) = hnf l hnf (TyConstruct _) = False hnf (TyAssoc _) = False reduceToplevel :: [Constraint] -> ST [Constraint] reduceToplevel ps = do debug ("performing top-level context reduction on " ++ showCommaListed ps) ps' <- simplifyToplevel ps debug ("constraints for context reduction are now in HNF: " ++ showCommaListed ps') res <- simplify ps' debug ("reduced " ++ showCommaListed ps ++ " to " ++ showCommaListed res) return res simplify :: [Constraint] -> ST [Constraint] simplify = loop [] where loop rs [] = return rs loop rs (p:ps) = do b <- entail (rs++ps) p if b then loop rs ps else loop (p:rs) ps elimTauts :: [Constraint] -> ST [Constraint] elimTauts ps = filterM (liftM not . entail []) ps reduce :: [Constraint] -> ST [Constraint] reduce ps = do debug ("performing context reduction on " ++ showCommaListed ps) ps' <- simplify ps res <- elimTauts ps' debug ("reduced " ++ showCommaListed ps ++ " to " ++ showCommaListed res) return res split' :: ([Constraint] -> ST [Constraint]) -- the reduce function -> [TypeVarId] -- variables in the assumptions -> [TypeVarId] -- variables we want to quantify over -> [Constraint] -> ST ([Constraint], -- deferred constraints [Constraint]) -- retained constraints split' red fs gs ps = do debug ("splitting constraints " ++ showCommaListed ps ++ ". fixed variables: " ++ showCommaListed fs ++ ". variables selected for quantification: " ++ showCommaListed gs) ps' <- red ps let (ds, rs) = partition (all (`elem` fs) . freeTypeVarsList) ps' debug ("splitting finished, deferred constraints: " ++ showCommaListed ds ++ ", retained constraints: " ++ showCommaListed rs) return (ds, rs) split = split' reduce splitToplevel = split' reduceToplevel