[implemented unification
mail@stefanwehr.de**20050519101737] {
hunk ./Entailment.hs 3
+--
+-- standard Haskell typeclass entailment
+--
hunk ./Entailment.hs 7
+-- entails :: [ClassConstraint
hunk ./Error.hs 23
-    phasefail_, panic_,
+    phasefail_, panic_, failwith_,
hunk ./Error.hs 25
-    PException(..), showWithoutLocation
-
+    PException, 
+    showWithoutLocation,
+    FailureCause(..),
+    catchFailure, mkCatchFailure,
+    debug_
hunk ./Error.hs 36
-import Control.Exception as E         ( throwDyn )
+import Control.Exception as E         ( throwDyn, catchDyn )
+import Control.Monad.State
hunk ./Error.hs 47
-data PException
-    = PhaseFailed Location String -- location, message
-    | Panic Location String       -- the `impossible' happened
-  deriving Eq
+data FailureCause 
+    = PhaseFailed
+    | Panic
+    | UnificationFailed
+    | ReductionFailed
+    | MatchingFailed
+      deriving (Eq,Show)
+
+data PException = PException FailureCause Location String
+      deriving Eq  
hunk ./Error.hs 59
-  showsPrec _ e = showString progName . showString ": " . showPException e
-
-showPException :: PException -> ShowS
-showPException (PhaseFailed (fname, lineno) msg)
-    = foldr1 (.) (map showString [ fname, ":", show lineno, ": ", msg]) 
+  show e = show progName ++ ": " ++ showPException e
hunk ./Error.hs 61
-showPException (Panic (fname, lineno) s)
-   = showString $ fname  ++ ":" ++ show lineno ++ ": panic!:\n\t" ++ s ++ "\n\n"
+showPException :: PException -> String
+showPException (PException cause (fname, lineno) msg)
+    = fname  ++ ":" ++ show lineno ++ ": " ++ 
+      show cause ++ "\n\t" ++ msg ++ "\n\n" 
hunk ./Error.hs 67
-showWithoutLocation (PhaseFailed _ msg) = msg
-showWithoutLocation (Panic _ msg) = msg
+showWithoutLocation (PException cause _ msg)
+    = show cause ++ ":\n\t" ++ msg ++ "\n\n" 
hunk ./Error.hs 80
+
+catchFailure :: IO a -> [FailureCause] -> (FailureCause -> IO a) -> IO a
+catchFailure io causes handler = 
+    E.catchDyn io h
+    where h e@(PException cause loc msg) = 
+              if cause `elem` causes then handler cause
+              else E.throwDyn e
+              
+--mkCatch :: ST a -> [FailureCause] -> (FailureCause -> ST a) -> ST a
+mkCatchFailure catch m causes handler = 
+    do state <- get
+       (state', res) <- lift $ catch (evalStateT (patch m) state)
+                               causes 
+                               (\c -> evalStateT (patch (handler c)) state)
+       put state
+       return res
+    where --patch :: ST a -> ST (Symtab, a)
+          patch m = do a <- m
+                       state <- get
+                       return (state, a)
hunk ./Error.hs 105
-panic_ l  x = E.throwDyn (Panic l x)
+panic_ l  x = E.throwDyn (PException Panic l x)
hunk ./Error.hs 108
-phasefail_ l x = E.throwDyn (PhaseFailed l x)
+phasefail_ l x = E.throwDyn (PException PhaseFailed l x)
+
+failwith_ :: Location -> FailureCause -> String -> a
+failwith_ l c x = E.throwDyn (PException c l x)
hunk ./Error.hs 121
+
+
+--
+-- Debugging
+--
+
+debug_ :: MonadIO m => Location -> String -> m ()
+debug_ (fname, lineno) msg = 
+    let s = "[DEBUG] " ++ fname  ++ ":" ++ show lineno ++ ": " ++ msg
+        in liftIO (putStrLn s)
hunk ./KindInference.hs 128
-{-
-debug s = liftST $ liftIO $ putStrLn s
-debugST s = liftIO $ putStrLn s
--}
-debug s = return ()
-debugST s = return ()
hunk ./KindInference.hs 281
-     debugST ("dependency groups: " ++ show groups)
hunk ./ParseSyntax.hs 102
-                                         cc_param :: Type 
+                                         cc_param :: Type
hunk ./ParseSyntax.hs 107
-                                   eqc_right :: Type 
+                                   eqc_right :: Type
hunk ./ParseSyntax.hs 111
+-- simple constraint
hunk ./ParseSyntax.hs 116
+data QualifiedConstraint = QualifiedConstraint [Constraint] ClassConstraint
+      deriving (Read, Show, Eq, Gen.Data, Gen.Typeable)
+
+data ConstraintScheme 
+    = QScheme [TypeVarId] QualifiedConstraint
+    | EqScheme [TypeVarId] EqConstraint
+      deriving (Read, Show, Eq, Gen.Data, Gen.Typeable)
hunk ./ParseSyntax.hs 215
-        let s' = foldr removeFromSubst s quant
+        let s' = removeListFromSubst quant s
hunk ./ParseSyntax.hs 223
+
+instance Substitution TypeVarId Type EqConstraint where
+    applySubst s (EqConstraint t1 t2) = 
+        EqConstraint (applySubst s t1) (applySubst s t2)
+
+instance Types EqConstraint where
+    freeTypeVars (EqConstraint t1 t2) =
+        (freeTypeVars t1 `Set.union` freeTypeVars t2)
+    fixedTypeVars (EqConstraint _ t2) = fixedTypeVars t2
+
+instance Substitution TypeVarId Type ClassConstraint where
+    applySubst s (ClassConstraint id t) = 
+        ClassConstraint id (applySubst s t)
+
+instance Types ClassConstraint where
+    freeTypeVars (ClassConstraint _ t) = 
+        freeTypeVars t
+    fixedTypeVars (ClassConstraint _ _) = Set.empty
hunk ./ParseSyntax.hs 243
-    applySubst s (CC (ClassConstraint id t)) = 
-        CC (ClassConstraint id (applySubst s t))
-    applySubst s (EC (EqConstraint t1 t2)) =
-        EC (EqConstraint (applySubst s t1) (applySubst s t2))
+    applySubst s (CC cc) = CC $ applySubst s cc
+    applySubst s (EC ec) = EC $ applySubst s ec
hunk ./ParseSyntax.hs 247
-    freeTypeVars (CC (ClassConstraint _ t)) = freeTypeVars t
-    freeTypeVars (EC (EqConstraint t1 t2)) = 
-        freeTypeVars t1 `Set.union` freeTypeVars t2
-    fixedTypeVars (CC (ClassConstraint _ _)) = Set.empty
-    fixedTypeVars (EC (EqConstraint _ t2)) = fixedTypeVars t2
+    freeTypeVars (CC cc) = freeTypeVars cc
+    freeTypeVars (EC ec) = freeTypeVars ec
+    fixedTypeVars (CC cc) = fixedTypeVars cc
+    fixedTypeVars (EC ec) = fixedTypeVars ec
hunk ./Substitution.hs 7
-    showSubst, nullSubst, (+->), removeFromSubst, composeSubst,
-    mergeSubst, substLookup, substFromAssocs
+    showSubst, nullSubst, (+->), removeFromSubst, removeListFromSubst, 
+    composeSubst,
+    mergeSubst, substLookup, substFromAssocs, instantiateScheme
hunk ./Substitution.hs 53
-    
+
+removeListFromSubst :: (SubstParams a b) => [a] -> Subst a b -> Subst a b
+removeListFromSubst l s = foldr removeFromSubst s l
+
hunk ./Substitution.hs 82
+
+instantiateScheme :: Substitution a b c => [a] -> [b] -> c -> c
+instantiateScheme as bs c = 
+    applySubst (substFromAssocs (zip as bs)) c
hunk ./Symtab.hs 5
-  ST, liftIO, modify, gets, get, runST,
+  ST, liftIO, runST, catchST,
hunk ./Symtab.hs 10
-  findTypeDef
+  findTypeDef,
hunk ./Symtab.hs 12
+  freshTypeVar, freshTypeVars
hunk ./Symtab.hs 17
+import Control.Exception
hunk ./Symtab.hs 19
+import Prelude hiding (catch)
hunk ./Symtab.hs 24
-
+import qualified UniqIdents
+                   
hunk ./Symtab.hs 30
-      typeDefMap        :: Map.Map TypeId TypeDef
+      typeDefMap        :: Map.Map TypeId TypeDef,
+      typeVarVersion    :: UniqIdents.Version -- next free type var version
hunk ./Symtab.hs 37
-                       typeDefMap = Map.empty }
+                       typeDefMap = Map.empty,
+                       typeVarVersion = UniqIdents.initialVersion - 1 }
hunk ./Symtab.hs 45
+catchST :: ST a -> [FailureCause] -> (FailureCause -> ST a) -> ST a
+catchST st causes handler = mkCatchFailure catchFailure st causes handler
+
hunk ./Symtab.hs 103
+freshTypeVar :: ST TypeVarId
+freshTypeVar = 
+    do cur <- gets typeVarVersion
+       modify (\s -> s { typeVarVersion = cur - 1 })
+       return (UniqIdents.mkTypeVar "v" cur)
hunk ./Symtab.hs 109
+freshTypeVars :: Int -> ST [TypeVarId]
+freshTypeVars n =
+    mapM (\_ -> freshTypeVar) [1..n]
hunk ./Symtab.hs 115
+-- Please note: no kind information available when symbol table
+-- is built.
hunk ./Symtab.hs 120
+FIXME: we cannot do any checks in this early stage!!!
+
hunk ./Symtab.hs 142
-(rule inst) are checked later.
+(rule inst) are checked later. It should be noted that all "output" of
+the rules is recorded in the symbol table.
hunk ./Symtab.hs 153
+           -- step (1)
hunk ./Symtab.hs 156
+           -- step (2)
hunk ./Symtab.hs 158
+           -- step (3)
+
+           -- step (4)
hunk ./Unification.hs 1
+{-# OPTIONS_GHC -fglasgow-exts #-}
+-- for multi-param typeclasses
+
hunk ./Unification.hs 6
-  unifyType
-
+  runUF, UF, UFResult, TypeEq(..), unify,
+  showEqs
hunk ./Unification.hs 10
+import Control.Monad.State
hunk ./Unification.hs 12
+import qualified Control.Exception as E
+import List (intersperse)
hunk ./Unification.hs 19
+import Error
hunk ./Unification.hs 21
-unifyType :: Type -> Type -> ST (Either String TypeSubst)
-unifyType (TyApp l r) (TyApp l' r') = 
-    do s1 <- unifyType  l l'
-       case s1 of
-         err@(Left _) -> return err
-         Right s1' ->
-             do s2 <- unifyType  (applySubst s1' r) (applySubst s1' r')
-                case s2 of
-                  err@(Left _) -> return err
-                  Right s2' -> return $ Right (s2' `composeSubst` s1')
-unifyType (TyVar id) t = varBind id t
-unifyType t (TyVar id) = varBind id t
-unifyType (TyConstruct id1) (TyConstruct id2) 
-    | id1 == id2 = return (Right nullSubst)
-unifyType t1 t2 = 
-    return $ Left ("Types `" ++ showPpr t1 ++ "' and `" ++ showPpr t2 ++
-                   "' do not unify")
hunk ./Unification.hs 22
-varBind u t | t == TyVar u = return (Right nullSubst)
-            | u `Set.member` freeTypeVars t = 
-                return $ Left ("variable `" ++ showPpr u ++ "' occurs in " ++ 
-                               showPpr t)
-            | otherwise = 
-                do k1 <- kindOf u
-                   k2 <- kindOf t
-                   if k1 == k2 
-                      then return $ Right (u +-> t)
-                      else return $ Left ("kind mismatch while unifying `" ++ 
-                                          showPpr u ++ "' with `" ++ showPpr t 
-                                          ++ "'")
+--
+-- Matching
+--
hunk ./Unification.hs 26
+-- 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 TypeSubst
+matchType allowed t1@(TyApp l r) t2@(TyApp l' r') =
+    do sl <- matchType allowed l l'
+       sr <- matchType allowed r r'
+       case mergeSubst sl sr of
+         Nothing -> failwith MatchingFailed 
+                    ("cannot match " ++ showPpr t1 ++ " and " ++ showPpr t2)
+         Just s -> return s
+matchType allowed (TyVar u) t | u `elem` allowed
+    = do ku <- kindOf u
+         kt <- kindOf t
+         if ku == kt 
+            then return (u +-> t)
+            else failwith MatchingFailed "kind mismatch"
+matchType _ (TyVar u) (TyVar u') | u == u' = return nullSubst
+matchType _ (TyConstruct id) (TyConstruct id') | id == id' = return nullSubst
+matchType allowed (TyAssoc (AssocType id params))
+                  (TyAssoc (AssocType id' params')) | id == id'
+    = matchTypes allowed params params'
+matchType _ t1 t2 = failwith MatchingFailed ("cannot match " ++ showPpr t1 ++
+                                             " and " ++ showPpr t2)
+
+matchTypes :: [TypeVarId] -> [Type] -> [Type] -> ST TypeSubst
+matchTypes allowed t1s t2s = 
+    do substs <- mapM (uncurry $ matchType allowed) (zip t1s t2s)
+       case foldM mergeSubst nullSubst substs of
+         Nothing -> failwith MatchingFailed
+                    ("cannot matches types " ++ showPpr t1s ++ " and " ++
+                     showPpr t2s)
+
+
+--
+-- The unification monad
+--
+
+infix 6 :=:  -- binds stronger than :
+data TypeEq = (:=:) Type Type
+
+showEqs :: [TypeEq] -> String
+showEqs eqs = 
+    "[" ++
+    (concat . intersperse ", ") 
+    (map (\ (t1 :=: t2) -> showPpr t1 ++ " = " ++ showPpr t2) eqs)
+    ++ "]"
+
+instance Substitution TypeVarId Type TypeEq where
+    applySubst s (t1 :=: t2) = (applySubst s t1 :=: applySubst s t2)
+
+data UFState = UFState { uf_theta :: [ConstraintScheme] }
+
+type UFResult = ([TypeEq], TypeSubst)
+
+type UF = StateT UFState ST
+
+liftST :: ST a -> UF a
+liftST x = lift x
+
+runUF :: [ConstraintScheme] -> UF a -> ST a
+runUF cs uf = evalStateT uf (UFState cs) 
+
+catchUF :: UF a -> [FailureCause] -> (FailureCause -> UF a) -> UF a
+catchUF st causes handler = mkCatchFailure catchST st causes handler
+
+
+--
+-- The 1-step reduction
+--
+
+reductionFailed succ err = catchUF succ [ReductionFailed] (\_ -> err)
+
+reduceOneStep :: Type -> UF Type
+-- rules lapp_R and rapp_R
+reduceOneStep (TyApp t1 t2) =
+    do t1' <- reduceOneStep t1
+       return $ TyApp t1' t2
+    `reductionFailed`
+    do t2' <- reduceOneStep t2
+       return $ TyApp t1 t2'
+-- rule arg_R and syn_R
+reduceOneStep (TyAssoc (AssocType id params)) =
+    do params' <- reduceParam params
+       return $ TyAssoc (AssocType id params')
+    `reductionFailed`
+    do constrs <- gets uf_theta
+       liftST $ reduceAT id params constrs
+    where 
+    reduceParam [] = failwith ReductionFailed 
+                     "cannot reduce type synonym application"
+    reduceParam (x:xs) = 
+        do x' <- reduceOneStep x
+           return (x':xs)
+        `reductionFailed`
+        do xs' <- reduceParam xs
+           return (x:xs')
+    -- 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 :: AssocTypeId -> [Type] -> [ConstraintScheme] ->  ST Type
+    reduceAT id params [] = 
+        failwith ReductionFailed ("cannot reduce type synonym " ++ showPpr id)
+    reduceAT id params (QScheme _ _:rest) = reduceAT id params rest
+    reduceAT id params (EqScheme quant eq : rest) = 
+        if (assoc_name . eqc_left) eq /= id 
+           then reduceAT id params rest
+           else do -- instantiate the scheme
+                   freshs <- freshTypeVars (length quant)
+                   let eq' = instantiateScheme quant (map TyVar freshs) 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
+                   -- the result of the reduction is the right-hand side
+                   -- of the (instantiated) equality constraint, after
+                   -- performing the substitution
+                   E.assert 
+                        (applySubst subst (assoc_params . eqc_left $ eq') 
+                         == params)
+                        (return $ applySubst subst (eqc_right eq'))
+-- default
+reduceOneStep t = failwith ReductionFailed ("cannot reduce " ++ showPpr t)
+
+--
+-- 1-step unification
+--
+
+emptyEqs = []
+
+unifyOneStep :: TypeEq -> UF UFResult
+-- rule refl_U
+unifyOneStep (t1 :=: t2) | t1 == t2 = return (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 ([l :=: l', r :=: r'], nullSubst)
+-- rule red_U with symm_U
+unifyOneStep (t1@(TyAssoc _) :=: t2) = oneStepAssoc t1 t2
+unifyOneStep (t1 :=: t2@(TyAssoc _)) = oneStepAssoc t1 t2
+
+oneStepVar :: TypeVarId -> Type -> UF UFResult
+oneStepVar u t | t == TyVar u = return (emptyEqs, nullSubst)
+               | u `Set.member` freeTypeVars t = 
+                   failwith UnificationFailed
+                     ("variable `" ++ showPpr u ++ "' occurs in " ++ showPpr t)
+               | otherwise = 
+                   do k1 <- liftST $ kindOf u
+                      k2 <- liftST $ kindOf t
+                      if k1 == k2 
+                         then return (emptyEqs, u +-> t)
+                         else failwith UnificationFailed
+                               ("kind mismatch while unifying `" ++ 
+                                showPpr u ++ "' with `" ++ showPpr t ++ "'")
+
+oneStepAssoc :: Type -> Type -> UF UFResult
+oneStepAssoc at t1 = 
+    do t2 <- reduceOneStep at
+       return ([t2 :=: t1], nullSubst)
+
+--
+-- Unification
+--
+-- (the ~~>! function)
+--
+
+unify :: [TypeEq] -> UF UFResult
+unify eqs = 
+    do x <- tryOneStep eqs
+       case x of
+         Nothing -> 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')
+
+
+oneStepFailed succ err = catchUF succ [ReductionFailed, UnificationFailed] 
+                           (\_ -> err)
+
+tryOneStep :: [TypeEq] -> UF (Maybe ([TypeEq], [TypeEq], TypeSubst))
+tryOneStep [] = return Nothing
+tryOneStep (eq:rest) = 
+    do (u',r') <- unifyOneStep eq
+       return $ Just (rest, u', r')
+    `oneStepFailed`
+    do x <- tryOneStep rest
+       case x of
+         Nothing -> return Nothing
+         Just (u, u', r') -> return $ Just (eq:u, u', r')
hunk ./UniqIdents.hs 12
-  NA, runNA, 
+  NA, runNA, Version, initialVersion,
hunk ./UniqIdents.hs 26
-  enterBlock, exitBlock, freshValVar
+  enterBlock, exitBlock, freshValVar,
hunk ./UniqIdents.hs 28
+  mkTypeVar
hunk ./UniqIdents.hs 43
-type Version = Int
+type Version = Integer
hunk ./UniqIdents.hs 50
-mkId :: ParseId -> Int -> Id
+mkId :: ParseId -> Integer -> Id
hunk ./UniqIdents.hs 121
-              na_versions :: Map.Map ParseId Int }
+              na_versions :: Map.Map ParseId Integer }
hunk ./UniqIdents.hs 156
+initialVersion :: Integer
+initialVersion = 0
+
hunk ./UniqIdents.hs 162
-       let v = Map.findWithDefault 0 id m
+       let v = Map.findWithDefault initialVersion id m
hunk ./UniqIdents.hs 305
+
+-- generates a type variable with the given version. We require the version
+-- number to be smaller than 0, so that the resulting type variable
+-- is fresh with respect to the type variables generated in the NA monad.
+mkTypeVar :: String -> Version -> TypeVarId
+mkTypeVar s v = 
+    if v >= initialVersion
+       then panic ("mkTypeVar called with illegal version number: " ++
+                   show v)
+       else (TypeVarId (Id v s))
hunk ./WellFormedProgram.hs 34
-
+import Substitution
hunk ./WellFormedProgram.hs 55
-          overlap i1 i2 = 
-              do res <- unifyType (inst_type i1) (inst_type i2) 
-                 case res of
-                   Left _ -> return False
-                   Right _ -> return True
+          overlap i1 i2 =
+              let t1 = inst_type i1
+                  t2 = inst_type i2
+                  in do debug ("unifying `" ++ showPpr t1 ++ "' with `" ++
+                               showPpr t2 ++ "'")
+                        (eqs, subst) <- runUF [] (unify [t1 :=: t2])
+                        debug ("Substitution: " ++ showSubst subst)
+                        debug ("Pending equalities: " ++ showEqs eqs)
+                        return False
+{- 
+              do catchST (unifyTypes (inst_type i1) (inst_type i2) 
+                          >> return True)
+                   [UnificationFailed] (\_ -> return False)
+-}
hunk ./pp/macros.m4 6
+define(failwith, (failwith_ `SRC_LOC_'))dnl
+define(debug, (debug_ `SRC_LOC_'))dnl
}