{-# OPTIONS_GHC -fglasgow-exts #-} -- for multi-param typeclasses -- -- 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.Unification ( runUF, UF, UFResult, TypeEq(..), unify, runUnify, runUnifyAssertEmpty, matchType, matchTypes, matchConstraint, normalise, showEqs ) where import Control.Monad.State import Control.Monad.Error import qualified Data.Set as Set import qualified Control.Exception as E import List (intersperse, nub) import Maybe (catMaybes, isJust) import Phrac.AbstractSyntax import Phrac.Substitution import Phrac.Pretty import Phrac.Symtab import Phrac.Kinds import Phrac.Error -- -- Matching -- -- `matchConstraint (A, ts) c' checks if the constraint c is fulfilled -- by the instance declaration A ts. matchConstraint :: (ClassId, [Type]) -> ClassConstraint -> ST (Maybe TypeSubst) matchConstraint (id, ts) (ClassConstraint id' ts') | id /= id' = return Nothing | otherwise = do -- first normalize the type tns <- runUF [] (mapM normalise ts) tns' <- runUF [] (mapM normalise ts') -- then use match to see if there is a substitution s such that -- applySubst s t = t' matchTypes tns tns' matchType :: Type -> Type -> ST (Maybe TypeSubst) matchType t1 t2 = matchType' (freeTypeVarsList t1) t1 t2 matchTypes :: [Type] -> [Type] -> ST (Maybe TypeSubst) matchTypes ts1 ts2 = let frees = Set.unions (map freeTypeVars ts1) in matchTypes' (Set.toList frees) ts1 ts2 -- matchType' l t1 t2 tries to find a substitution s with -- dom(s) \subset l and applySubst s t1 = t2 . -- No reduction on type synonyms is performed! matchType' :: [TypeVarId] -> Type -> Type -> ST (Maybe TypeSubst) matchType' allowed t1@(TyApp l r) t2@(TyApp l' r') = do sl <- matchType' allowed l l' sr <- matchType' allowed r r' case (sl, sr) of (Just sl', Just sr') -> return $ mergeSubst sl' sr' _ -> return Nothing matchType' allowed (TyVar u) t | u `elem` allowed = do ku <- kindOf u kt <- kindOf t if ku == kt then return $ Just (u +-> t) else return Nothing matchType' _ (TyVar u) (TyVar u') | u == u'= return $ Just nullSubst matchType' _ (TyConstruct id) (TyConstruct id') | id == id' = return $ Just nullSubst matchType' allowed (TyAssoc (AssocType id params)) (TyAssoc (AssocType id' params')) | id == id' = matchTypes' allowed params params' matchType' _ t1 t2 = return Nothing matchTypes' :: [TypeVarId] -> [Type] -> [Type] -> ST (Maybe TypeSubst) matchTypes' allowed t1s t2s = do substs <- mapM (uncurry $ matchType' allowed) (zip t1s t2s) if all isJust substs then case foldM mergeSubst nullSubst (catMaybes substs) of Nothing -> return Nothing Just s -> return $ Just s else return Nothing -- -- The unification monad -- infix 6 :=: -- binds stronger than : data TypeEq = (:=:) Type Type deriving (Show,Eq) instance Pretty TypeEq where pprPrec prec (t1 :=: t2) = parens `usedWhen` (prec > minPrec) $ ppr t1 <+> text "=" <+> ppr t2 showEqs :: [TypeEq] -> String showEqs eqs = "{" ++ (concat . intersperse ", ") (map showPpr eqs) ++ "}" instance Substitution TypeVarId Type TypeEq where applySubst s (t1 :=: t2) = (applySubst s t1 :=: applySubst s t2) data UFState = UFState { uf_theta :: [EqualityDefinition] } type UFResult' = ([TypeEq], TypeSubst) type UF = StateT UFState ST liftST :: ST a -> UF a liftST x = lift x -- runUF uses the program's equality definitions implicitly runUF :: [EqualityDefinition] -> UF a -> ST a runUF defs uf = do globals <- getGlobalEqualities evalStateT uf (UFState $ defs ++ globals) -- -- The 1-step reduction -- reduceOneStep :: Type -> UF (Maybe Type) -- rules lapp_R and rapp_R reduceOneStep (TyApp t1 t2) = do t1' <- reduceOneStep t1 case t1' of Just x -> return (Just $ TyApp x t2) Nothing -> do t2' <- reduceOneStep t2 case t2' of Just x -> return (Just $ TyApp t1 x) Nothing -> return Nothing -- rule arg_R and syn_R reduceOneStep (TyAssoc at@(AssocType id params)) = do params' <- reduceParam params case params' of Just x -> return (Just $ TyAssoc (AssocType id x)) Nothing -> do constrs <- gets uf_theta res <- liftST $ reduceAT at constrs return res where reduceParam [] = return Nothing reduceParam (x:xs) = do x' <- reduceOneStep x case x' of Just z -> return $ Just (z:xs) Nothing -> do xs' <- reduceParam xs case xs' of Just zs -> return $ Just (x:zs) Nothing -> return Nothing -- rule syn_R: we search for an equality constraint we can use for -- the reduction and return the rhs of it -- (substitution already applied) reduceAT :: AssocType -> [EqualityDefinition] -> ST (Maybe Type) reduceAT at [] = return Nothing reduceAT at@(AssocType id params) (sc@(EqualityDefinition quants eq) : rest) = if (assoc_name . eqc_left) eq /= id then reduceAT at rest else do -- instantiate the scheme (eq', freshs, _) <- instantiate quants eq -- match the parameters of the synonym application -- with regard to the scheme instantiation, i.e. -- only the fresh variables can be substituted subst <- matchTypes' freshs (assoc_params . eqc_left $ eq') params case subst of Nothing -> reduceAT at rest Just s -> -- the result of the reduction is the right-hand side -- of the (instantiated) equality constraint, after -- performing the substitution let res = applySubst s (eqc_right eq') in do debug ("reduced " ++ showPpr' at ++ " to " ++ showPpr' res ++ " using equality scheme " ++ showPpr sc) return $ Just res -- default reduceOneStep t = return Nothing -- -- Normalisation (multi-step reduction) -- normalise :: Type -> UF Type normalise t = do x <- reduceOneStep t case x of Nothing -> return t Just t' -> normalise t' -- -- 1-step unification -- emptyEqs = [] unifyOneStep :: TypeEq -> UF (Maybe UFResult') -- rule refl_U unifyOneStep (t1 :=: t2) | t1 == t2 = return $ Just (emptyEqs, nullSubst) -- rule var_U with symm_U unifyOneStep (TyVar u :=: t) = oneStepVar u t unifyOneStep (t :=: TyVar u) = oneStepVar u t -- rule app_U unifyOneStep (TyApp l r :=: TyApp l' r') = return $ Just ([l :=: l', r :=: r'], nullSubst) -- rule red_U with symm_U unifyOneStep (t1@(TyAssoc _) :=: t2@(TyAssoc _)) = do res <- oneStepAssoc t1 t2 case res of Nothing -> oneStepAssoc t2 t1 Just x -> return $ Just x unifyOneStep (t1@(TyAssoc _) :=: t2) = oneStepAssoc t1 t2 unifyOneStep (t2 :=: t1@(TyAssoc _)) = oneStepAssoc t1 t2 -- default unifyOneStep (t1 :=: t2) = return Nothing oneStepVar :: TypeVarId -> Type -> UF (Maybe UFResult') oneStepVar u t | t == TyVar u = return $ Just (emptyEqs, nullSubst) | u `Set.member` freeTypeVars t = do debug ("occurs check failed when unifying " ++ showPpr' u ++ " with " ++ showPpr' t) return Nothing | otherwise = do k1 <- liftST $ kindOf u k2 <- liftST $ kindOf t if k1 == k2 then return $ Just (emptyEqs, u +-> t) else do debug ("kind mismatch while unifying " ++ showPpr' u ++ " with " ++ showPpr' t) return Nothing oneStepAssoc :: Type -> Type -> UF (Maybe UFResult') oneStepAssoc at t1 = do t2 <- reduceOneStep at case t2 of Just x -> return $ Just ([x :=: t1], nullSubst) Nothing -> return Nothing -- -- 1-step matching -- matchOneStep :: TypeEq -> UF (Maybe UFResult') -- rule refl_U matchOneStep (t1 :=: t2) | t1 == t2 = return $ Just (emptyEqs, nullSubst) -- rule var_U with symm_U matchOneStep (TyVar u :=: t) = oneStepVar u t -- rule app_U matchOneStep (TyApp l r :=: TyApp l' r') = return $ Just ([l :=: l', r :=: r'], nullSubst) -- rule red_U with symm_U matchOneStep (t1@(TyAssoc _) :=: t2@(TyAssoc _)) = do res <- oneStepAssoc t1 t2 case res of Nothing -> oneStepAssoc t2 t1 Just x -> return $ Just x matchOneStep (t1@(TyAssoc _) :=: t2) = oneStepAssoc t1 t2 matchOneStep (t2 :=: t1@(TyAssoc _)) = oneStepAssoc t1 t2 -- default matchOneStep (t1 :=: t2) = return Nothing -- -- Unification -- -- (the ~~>! function) -- -- Unification uses the program's equality definitions implicitly. type UFResult = Either String ([EqConstraint], TypeSubst) runUnifyAssertEmpty :: [EqualityDefinition] -> [TypeEq] -> ST (Either String TypeSubst) runUnifyAssertEmpty defs eqs = do res <- runUnify defs eqs case res of Left err -> return $ Left err Right (peqs, subst) -> if null peqs then return $ Right subst else panic ("Unification should finished without pending " ++ "equalities, but some equalities are left: " ++ showCommaListed peqs) runUnify :: [EqualityDefinition] -> [TypeEq] -> ST UFResult runUnify defs eqs = runUF defs (unify eqs) unify :: [TypeEq] -> UF UFResult unify eqs = do theta <- gets uf_theta debug ("running unification on " ++ showEqs eqs ++ " under the assumptions " ++ showCommaListed theta) (u, r) <- unify' eqs -- u should only contain constraints of the form `T t1 = t2' where -- T is an associated type synonym and t2 is not a type variable. -- Unsatisfiable constraints (like `Int = Bool') signal unification -- failure case mapM adjustConstraint u of Right u' -> do debug ("unification finished, substitution: " ++ showSubst r ++ ", pending equality constraints: " ++ showCommaListed u') return $ Right (u', r) Left err -> do debug ("Unification failed: " ++ err) return $ Left err where -- note: even a eq constraint if the form T a = b is acceptable, -- because a might be equal to b. adjustConstraint (TyAssoc at :=: t) = Right $ EqConstraint at t adjustConstraint (t :=: TyAssoc at) = Right $ EqConstraint at t adjustConstraint c@(t1 :=: t2) = Left ("Cannot unify " ++ showEqs eqs ++ ". Unsatisfiable equality constraint: " ++ showPpr c) unify' :: [TypeEq] -> UF UFResult' unify' eqs = do x <- tryOneStep eqs case x of Nothing -> do return (eqs, nullSubst) -- rule refl_U* Just (u,u',r') -> -- 2nd premise of trans_U* do (u'',r'') <- unify' ((applySubst r' u) ++ u') return (u'', r'' `composeSubst` r') tryOneStep :: [TypeEq] -> UF (Maybe ([TypeEq], [TypeEq], TypeSubst)) tryOneStep [] = return Nothing tryOneStep l@(eq:rest) = do res <- unifyOneStep eq case res of Just (u',r') -> return $ Just (rest, u', r') Nothing -> do x <- tryOneStep rest case x of Nothing -> return Nothing Just (u, u', r') -> return $ Just (eq:u, u', r')