--
-- 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