[move match into E.Rules
John Meacham <john@repetae.net>**20061122070014] hunk ./E/Rules.hs 30
+import Control.Monad.Writer
hunk ./E/Rules.hs 42
-import E.TypeCheck
+import E.TypeCheck hiding(match)
hunk ./E/Rules.hs 57
+import qualified Util.Seq as Seq
+
hunk ./E/Rules.hs 250
+applyRules :: MonadStats m => (Id -> Maybe E) -> ARules -> [E] -> m (Maybe (E,[E]))
hunk ./E/Rules.hs 297
+-- | find substitution that will transform the left term into the right one,
+-- only substituting for the vars in the list
+
+match :: Monad m =>
+    (Id -> Maybe E)      -- ^ function to look up values in the environment
+    -> [TVr]              -- ^ vars which may be substituted
+    -> E                  -- ^ pattern to match
+    -> E                  -- ^ input expression
+    -> m [(TVr,E)]
+match lup vs = \e1 e2 -> liftM Seq.toList $ execWriterT (un e1 e2 () (-2::Int)) where
+    bvs :: IdSet
+    bvs = fromList (map tvrIdent vs)
+
+    un _ _ _ c | c `seq` False = undefined
+    un (EAp a b) (EAp a' b') mm c = do
+        un a a' mm c
+        un b b' mm c
+    un (ELam va ea) (ELam vb eb) mm c = lam va ea vb eb mm c
+    un (EPi va ea) (EPi vb eb) mm c = lam va ea vb eb mm c
+    un (EPrim s xs t) (EPrim s' ys t') mm c | length xs == length ys = do
+        sequence_ [ un x y mm c | x <- xs | y <- ys]
+        un t t' mm c
+    un (ESort x) (ESort y) mm c | x == y = return ()
+    un (ELit (LitInt x t1))  (ELit (LitInt y t2)) mm c | x == y = un t1 t2 mm c
+    un (ELit LitCons { litName = n, litArgs = xs, litType = t })  (ELit LitCons { litName = n', litArgs = ys, litType =  t'}) mm c | n == n' && length xs == length ys = do
+        sequence_ [ un x y mm c | x <- xs | y <- ys]
+        un t t' mm c
+
+    un (EVar TVr { tvrIdent = i, tvrType =  t}) (EVar TVr {tvrIdent = j, tvrType =  u}) mm c | i == j = un t u mm c
+    un (EVar TVr { tvrIdent = i, tvrType =  t}) (EVar TVr {tvrIdent = j, tvrType =  u}) mm c | i < 0 || j < 0  = fail "Expressions don't match"
+    un (EVar tvr@TVr { tvrIdent = i, tvrType = t}) b mm c
+        | i `member` bvs = tell (Seq.single (tvr,b))
+        | otherwise = fail $ "Expressions do not unify: " ++ show tvr ++ show b
+    un a (EVar tvr) mm c | Just b <- lup (tvrIdent tvr), not $ isEVar b = un a b mm c
+
+    un a b _ _ = fail $ "Expressions do not unify: " ++ show a ++ show b
+    lam va ea vb eb mm c = do
+        un (tvrType va) (tvrType vb) mm c
+        un (subst va (EVar va { tvrIdent = c }) ea) (subst vb (EVar vb { tvrIdent = c }) eb) mm (c - 2)
+