[make simplifier handle beta and pi expansion directly.
John Meacham <john@repetae.net>**20060411044041] hunk ./E/SSimplify.hs 328
+    f e sub inb | (ELam t b,(x:xs)) <- fromAp e = do
+        xs' <- mapM (dosub sub inb) xs
+        b' <- f b (minsert (tvrIdent t) (Susp x sub) sub) inb
+        mtick (toAtom "E.Simplify.f-beta-reduce")
+        h b' xs' inb
+    f e sub inb | (EPi t b,(x:xs)) <- fromAp e = do
+        xs' <- mapM (dosub sub inb) xs
+        b' <- f b (minsert (tvrIdent t) (Susp x sub) sub) inb
+        mtick (toAtom "E.Simplify.f-pi-reduce")
+        h b' xs' inb
hunk ./E/SSimplify.hs 478
+    doCase e t b as d sub inb | isBottom e = do
+        mtick "E.Simplify.case-of-bottom"
+        t' <- dosub sub inb t
+        return $ prim_unsafeCoerce e t'
hunk ./E/SSimplify.hs 492
-        t' <- dosub sub t
-        return ECase { eCaseScrutinee = e, eCaseType = t', eCaseBind = b, eCaseAlts = as'', eCaseDefault = d''} -- XXX     -- we duplicate code so continue for next renaming pass before going further.
-    doCase e t b as d sub inb | isBottom e = do
-        mtick "E.Simplify.case-of-bottom"
hunk ./E/SSimplify.hs 493
-        return $ prim_unsafeCoerce e t'
-
+        return ECase { eCaseScrutinee = e, eCaseType = t', eCaseBind = b, eCaseAlts = as'', eCaseDefault = d''} -- XXX     -- we duplicate code so continue for next renaming pass before going further.
hunk ./E/SSimplify.hs 630
+    app (e,[]) = return e
+    app (e,xs) = app' e xs
+
+    app' (ELit (LitCons n xs t@EPi {})) (a:as)  = do
+        mtick (toAtom $ "E.Simplify.typecon-reduce.{" ++ show n ++ "}" )
+        app (ELit (LitCons n (xs ++ [a]) (eAp t a)),as)
+    --app' (ELam tvr e) (a:as) = do
+    --    mtick (toAtom "E.Simplify.beta-reduce")
+    --    app (subst tvr a e,as)   -- TODO Fix quadradic substitution
+        --app (eLet tvr a e,as)   -- TODO Fix quadradic substitution
+    --app' (EPi tvr e) (a:as) = do
+    --    mtick (toAtom "E.Simplify.pi-reduce")
+    --    app (subst tvr a e,as)     -- Okay, types are small
+    app' ec@ECase {} xs = do
+        mtick (toAtom "E.Simplify.case-application")
+        let f e = app' e xs
+        ec' <- caseBodiesMapM f ec
+        let t = foldl eAp (eCaseType ec') xs
+        return ec' { eCaseType = t }
+    app' (ELetRec ds e) xs = do
+        mtick (toAtom "E.Simplify.let-application")
+        e' <- app' e xs
+        return $ eLetRec ds e'
+    app' (EError s t) xs = do
+        mtick (toAtom "E.Simplify.error-application")
+        return $ EError s (foldl eAp t xs)
+    app' e as = do
+        return $ foldl EAp e as
+