[unification now uses global equality definitions implicitly
mail@stefanwehr.de**20050526040532] {
hunk ./Entailment.hs 43
-    = do eqEnv <- getEqEnv
-         -- first normalize the type
-         tn <- runUF eqEnv (normalise t)
-         tn' <- runUF eqEnv (normalise t')
+    = do -- first normalize the type
+         tn <- runUF [] (normalise t)
+         tn' <- runUF [] (normalise t')
hunk ./Entailment.hs 84
--- entail uses the program's class and equality constraints implicitly,
+-- entail uses the program's class and equality definitions implicitly,
hunk ./Entailment.hs 87
--- FIXME: The constraints in cs and the constraint c are not quantified.
--- Atm, I simply do not quantify over any variable. Don't know if this is ok.
hunk ./Entailment.hs 107
-    do let ps' = mapMaybe toEqScheme ps
-       eqEnv <- getEqEnv
-       ures <- runUnify (eqEnv ++ ps') [TyAssoc left :=: right]
+    do let ps' = mapMaybe toEqDef ps
+       ures <- runUnify ps' [TyAssoc left :=: right]
hunk ./Entailment.hs 112
-    where toEqScheme (CC _) = Nothing
-          toEqScheme (EC e) = Just $ EqScheme [] e
+    where toEqDef (CC _) = Nothing
+          toEqDef (EC e) = Just $ EqualityDefinition [] e
hunk ./ParseSyntax.hs 124
-data EqScheme = EqScheme { eqs_quants     :: [TypeVarId],
-                           eqs_constraint :: EqConstraint 
-                         }
+data EqualityDefinition = EqualityDefinition { eqd_quants     :: [TypeVarId],
+                                               eqd_constraint :: EqConstraint 
+                                             }
hunk ./ParseSyntax.hs 189
-    | EqScheme [TypeVarId] EqConstraint
+    | EqualityDefinition [TypeVarId] EqConstraint
hunk ./ParseSyntax.hs 295
-instance Substitution TypeVarId Type EqScheme where
-    applySubst s (EqScheme quant c) = 
+instance Substitution TypeVarId Type EqualityDefinition where
+    applySubst s (EqualityDefinition quant c) = 
hunk ./ParseSyntax.hs 298
-            in EqScheme quant (applySubst s' c)
+            in EqualityDefinition quant (applySubst s' c)
hunk ./ParseSyntax.hs 300
-instance Types EqScheme where
-    freeTypeVars (EqScheme quant c) = 
+instance Types EqualityDefinition where
+    freeTypeVars (EqualityDefinition quant c) = 
hunk ./ParseSyntax.hs 303
-    fixedTypeVars (EqScheme quant c) = 
+    fixedTypeVars (EqualityDefinition quant c) = 
hunk ./ParseSyntax.hs 442
-instance Pretty EqScheme where
-    pprPrec prec (EqScheme vars ec) =
+instance Pretty EqualityDefinition where
+    pprPrec prec (EqualityDefinition vars ec) =
hunk ./Symtab.hs 25
-  Symtab, buildSymtab, EqEnv,
+  Symtab, buildSymtab, 
hunk ./Symtab.hs 32
-  findTypeDef, getEqEnv, findSuperClasses, findAllSuperClasses,
+  findTypeDef, getGlobalEqualities, findSuperClasses, findAllSuperClasses,
hunk ./Symtab.hs 56
-      eqEnv             :: EqEnv  -- assoc type definitions
+      globalEqualities  :: [EqualityDefinition]  -- assoc type definitions
hunk ./Symtab.hs 64
-                       eqEnv = [] }
-
-type EqEnv = [EqScheme]
+                       globalEqualities = [] }
hunk ./Symtab.hs 137
-getEqEnv :: ST EqEnv
-getEqEnv = gets eqEnv
+getGlobalEqualities :: ST [EqualityDefinition]
+getGlobalEqualities = gets globalEqualities
hunk ./Symtab.hs 278
-    in modify $ addInstance (map (EqScheme quants) eqs)
+    in modify $ addInstance (map (EqualityDefinition quants) eqs)
hunk ./Symtab.hs 286
-                        eqEnv = eqs ++ (eqEnv s) }
+                        globalEqualities = eqs ++ (globalEqualities s) }
hunk ./TypeInference.hs 100
-       eqEnv <- liftST getEqEnv
hunk ./TypeInference.hs 102
-       ures <- liftST $ runUnify eqEnv (eq : eqs)
+       ures <- liftST $ runUnify [] (eq : eqs)
hunk ./TypeInference.hs 217
-           -- empty EqScheme is because quantified variables were replaced
-           -- by fresh type constructors
-           pi2Eqs = map (EqScheme []) (eqConstraints pi2')
-       eqEnv <- liftST getEqEnv
-       ures <- liftST $ runUnify (eqEnv ++ pi2Eqs) [tau1 :=: tau2']
+           -- empty quantifier list is because quantified variables were 
+           -- replaced by fresh type constructors
+           pi2Eqs = map (EqualityDefinition []) (eqConstraints pi2')
+       ures <- liftST $ runUnify pi2Eqs [tau1 :=: tau2']
hunk ./Unification.hs 115
-data UFState = UFState { uf_theta :: EqEnv }
+data UFState = UFState { uf_theta :: [EqualityDefinition] }
hunk ./Unification.hs 124
-runUF :: EqEnv -> UF a -> ST a
-runUF cs uf = evalStateT uf (UFState cs) 
+-- 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)
hunk ./Unification.hs 169
-    reduceAT :: AssocType -> EqEnv ->  ST (Maybe Type)
+    reduceAT :: AssocType -> [EqualityDefinition] ->  ST (Maybe Type)
hunk ./Unification.hs 171
-    reduceAT at@(AssocType id params) (sc@(EqScheme quants eq) : rest) = 
-        if (assoc_name . eqc_left) eq /= id 
+    reduceAT at@(AssocType id params) (sc@(EqualityDefinition quants eq) : rest)
+        = if (assoc_name . eqc_left) eq /= id 
hunk ./Unification.hs 286
--- Unification does not use the program's equality constraints automatically.
--- All assumptions must be supplied explicitly in the first parameter
--- of type EqEnv (functions runUnifyAssertEmpty, runUnify, runUF).
+-- Unification uses the program's equality definitions implicitly.
hunk ./Unification.hs 290
-runUnifyAssertEmpty :: EqEnv -> [TypeEq] -> ST (Either String TypeSubst)
-runUnifyAssertEmpty env eqs = 
-    do res <- runUnify env eqs
+runUnifyAssertEmpty :: [EqualityDefinition] -> [TypeEq] 
+                    -> ST (Either String TypeSubst)
+runUnifyAssertEmpty defs eqs = 
+    do res <- runUnify defs eqs
hunk ./Unification.hs 304
-runUnify :: EqEnv -> [TypeEq] -> ST UFResult
-runUnify env eqs = runUF env (unify eqs)
+runUnify :: [EqualityDefinition] -> [TypeEq] -> ST UFResult
+runUnify defs eqs = runUF defs (unify eqs)
hunk ./WellFormedness.hs 90
-              in do eqEnv <- getEqEnv
-                    ures <- runUnify eqEnv [t1 :=: t2]
+              in do ures <- runUnify [] [t1 :=: t2]
hunk ./WellFormedness.hs 438
-       eqEnv <- getEqEnv
-       let frees = freeTypeVars eqEnv `Set.union` freeTypeVars cs
+       eqDefs <- getGlobalEqualities
+       let frees = freeTypeVars eqDefs `Set.union` freeTypeVars cs
hunk ./tests/examples/TypeSaveEvaluator.phc 58
-foo :: Int -> Int;
-foo n = eval (If (IsZero (Succ (Lit n))) (Lit 42) (Lit n));
+foo n = eval (If (IsZero (Succ n)) (Lit 42) n);
+bar = foo (Lit (-1));
+foobar = bar + 1;
}