[checkpoint before removing the MethodId type
mail@stefanwehr.de**20050521031244] {
hunk ./Entailment.hs 3
+import Monad ( msum )
+import Maybe ( mapMaybe )
+import List ( partition )
+import Symtab
+import AbstractSyntax
+import Substitution
+import Unification
+import Error
+import Pretty
+
hunk ./Entailment.hs 17
---entails :: [ConstraintScheme]
+-- `matchConstraint (A, t) c' checks if the constraint c is fulfilled
+-- by the instance declaration A t.
+matchConstraint :: (ClassId, Type) -> ClassConstraint -> ST (Maybe TypeSubst)
+matchConstraint (id, t) (ClassConstraint id' t') | id /= id' 
+    = return Nothing
+                                                 | otherwise
+    = do eqEnv <- getEqEnv 
+         catchST (runUnifyAssertEmpty eqEnv [t :=: t'] 
+                  >>= \s -> return (Just s))
+               [UnificationFailed] (\_ -> return Nothing)
+
+
+-- `bySuper p' returns the constraints that are implied by p through
+-- the superclass relation.
+bySuper :: ClassConstraint -> ST [ClassConstraint]
+bySuper p@(ClassConstraint i t) = 
+    do superClasses <- findSuperClasses i
+       transitives <- sequence 
+                      [bySuper (ClassConstraint i' t) | i' <- superClasses]
+       return (p : concat transitives)
+
+-- `byInst p' returns `Just l' if p matches any instance declaration. `l' is
+-- then the list of subgols.
+byInst :: ClassConstraint -> ST (Maybe [Constraint])
+byInst p@(ClassConstraint i t) = 
+    do insts <- findInstances i
+       candidates <- sequence [tryInst it | it <- insts]
+       return $ msum candidates
+    where tryInst ci =
+              do u <- matchConstraint (inst_class ci, inst_type ci) p
+                 case u of
+                   Nothing -> return Nothing
+                   Just u' -> 
+                       return $ Just (map (applySubst u') (inst_constraints ci))
+
+entail :: [Constraint] -> Constraint -> ST Bool
+entail ps (CC p) = 
+    do 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 (EqConstraint left right)) =
+    do -- FIXME: don't know how to quantify the equality scheme.
+       -- For now, I do not quantify over any variables
+       let ps' = mapMaybe toEqScheme ps
+       eqEnv <- getEqEnv
+       catchST (runUnifyAssertEmpty (eqEnv ++ ps') 
+                  [TyAssoc left :=: right] >> return True)
+               [UnificationFailed] (\_ -> return False)
+    where toEqScheme (CC _) = Nothing
+          toEqScheme (EC e) = Just $ EqScheme [] e
+
+-- only class constraints are brought into HNF, equality constraints
+-- are returned untouched
+toHnfs :: [Constraint] -> ST [Constraint]
+toHnfs 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 -> phasefail ("context reduction failed for "
+                                                 ++ showPpr p)
+                           Just ps -> toHnfs ps
+          inHnf cc = hnf (cc_param cc)
+              where hnf (TyVar _) = True
+                    hnf (TyApp l _) = hnf l
+                    hnf (TyConstruct _) = False
+                    hnf (TyAssoc _) = False  -- FIXME: not sure here
+
+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
+
+reduce :: [Constraint] -> ST [Constraint]
+reduce ps = 
+    do ps' <- toHnfs ps
+       simplify ps'
+
+split :: [TypeVarId]        -- variables in the assumptions
+      -> [TypeVarId]        -- variables we want to quantify over
+      -> [Constraint]
+      -> ST ([Constraint],  -- deferred constraints
+             [Constraint])  -- retained constraints
+split fs gs ps = 
+    do ps' <- reduce ps
+       let (ds, rs) = partition (all (`elem` fs) . freeTypeVarsList) ps'
+       return (ds, rs)
+
hunk ./ParseSyntax.hs 112
+data EqScheme = EqScheme { eqs_quants     :: [TypeVarId],
+                           eqs_constraint :: EqConstraint 
+                         }
+                    deriving (Read, Show, Eq, Gen.Data, Gen.Typeable)
+
hunk ./ParseSyntax.hs 122
+classConstraints :: [Constraint] -> [ClassConstraint]
+classConstraints [] = []
+classConstraints (EC _ : rest) = classConstraints rest
+classConstraints (CC c : rest) = c : classConstraints rest
+
+eqConstraints :: [Constraint] -> [EqConstraint]
+eqConstraints [] = []
+eqConstraints (EC e : rest) = e : eqConstraints rest
+eqConstraints (CC _ : rest) = eqConstraints rest
+
+splitConstraints :: [Constraint] -> ([ClassConstraint], [EqConstraint])
+splitConstraints [] = ([], [])
+splitConstraitns (x:xs) =
+    let (cs,es) = splitConstraints xs
+    in case x of
+         EC e -> (cs, e:es)
+         CC c -> (c:cs, es)
+
+mergeConstraints :: ([ClassConstraint], [EqConstraint]) -> [Constraint]
+mergeConstraints (cs,es) = 
+    map CC cs ++ map EC es
+
+isClassConstraint :: Constraint -> Bool
+isClassConstraint (CC _) = True
+isClassConstraint _ = False
+
+isEqConstraint :: Constraint -> Bool
+isEqConstraint (EC _) = True
+isEqConstraint _ = False
+
+{-
hunk ./ParseSyntax.hs 160
+-}
hunk ./Symtab.hs 6
-  Symtab, buildSymtab,
+  Symtab, buildSymtab, EqEnv,
hunk ./Symtab.hs 13
-  findTypeDef,
+  findTypeDef, getEqEnv, findSuperClasses,
hunk ./Symtab.hs 35
-      typeVarVersion    :: UniqIdents.Version -- next free type var version
+      typeVarVersion    :: UniqIdents.Version, -- next free type var version
+      eqEnv             :: EqEnv  -- assoc type definitions
hunk ./Symtab.hs 43
-                       typeVarVersion = UniqIdents.initialVersion - 1 }
+                       typeVarVersion = UniqIdents.initialVersion - 1,
+                       eqEnv = [] }
+
+type EqEnv = [EqScheme]
hunk ./Symtab.hs 73
+
+-- `findSuperClasses c' returns the _direct_ superclasses of c
+findSuperClasses :: ClassId -> ST [ClassId]
+findSuperClasses cid = 
+    do cdec <- findClass cid
+       return (map cc_name (class_constraints cdec))
hunk ./Symtab.hs 95
+
+getEqEnv :: ST EqEnv
+getEqEnv = gets eqEnv
hunk ./Symtab.hs 216
-    modify addInstance
-    where addInstance s = 
+    let -- add the assoc type definition
+        quants = freeTypeVarsList (inst_type ci)
+        assoc = inst_typeBind ci
+        left = AssocType (assocBind_name assoc) 
+                 (assocBind_index assoc : map TyVar (assocBind_params assoc))
+        right = assocBind_def assoc
+    in modify $ addInstance (EqScheme quants (EqConstraint left right))
+    where addInstance eq s = 
hunk ./Symtab.hs 229
-                                     (cdec, ci:insts) m}
+                                     (cdec, ci:insts) m,
+                        eqEnv = eq : (eqEnv s) }
hunk ./Unification.hs 6
-  runUF, UF, UFResult, TypeEq(..), unify,
+  runUF, UF, UFResult, TypeEq(..), unify, runUnify, runUnifyAssertEmpty,
hunk ./Unification.hs 83
-type InstanceEnv = [ConstraintScheme]
+data UFState = UFState { uf_theta :: EqEnv }
hunk ./Unification.hs 85
-data UFState = UFState { uf_theta :: InstanceEnv }
-
--- FIXME: type UFResult = ([EqConstraint], TypeSubst)
hunk ./Unification.hs 92
-runUF :: InstanceEnv -> UF a -> ST a
+runUF :: EqEnv -> UF a -> ST a
hunk ./Unification.hs 132
-    reduceAT :: AssocTypeId -> [Type] -> [ConstraintScheme] ->  ST Type
+    reduceAT :: AssocTypeId -> [Type] -> EqEnv ->  ST Type
hunk ./Unification.hs 135
-    reduceAT id params (QScheme _ _:rest) = reduceAT id params rest
hunk ./Unification.hs 198
+
+runUnifyAssertEmpty :: EqEnv -> [TypeEq] -> ST TypeSubst
+runUnifyAssertEmpty env eqs = 
+    do (peqs, subst) <- runUnify env eqs
+       if null peqs 
+          then return subst
+          else panic
+                 ("Unification should finished without pending equalities, " ++
+                  "but some equalities are left: " ++ showCommaListed peqs)
+
+runUnify :: EqEnv -> [TypeEq] -> ST ([EqConstraint], TypeSubst)
+runUnify env eqs = runUF env (unify eqs)
}