[make eta expansion apply to subbindings in simplifier, try to apply it to arbitrary subexpressions
John Meacham <john@repetae.net>**20060317042227] hunk ./E/Eta.hs 169
-        mtick ("EtaExpand.def.{" ++ tvrShowName t)
+        if tvrIdent t == 0
+         then mtick ("EtaExpand.random")
+          else mtick ("EtaExpand.def.{" ++ tvrShowName t)
hunk ./E/Eta.hs 182
-etaExpandAp dataTable t as | Just at <- Info.lookup (tvrInfo t),let n = snd (arity at), n > length as = do
-    let e = foldl EAp (EVar t) as
-    let (_,ts) = fromPi' dataTable (getType e)
-        ets = (take (n - length as) ts)
-    mticks (length ets) ("EtaExpand.use.{" ++ tvrShowName t)
-    let tvrs = f mempty [ (tvrIdent t,t { tvrIdent = n }) |  n <- [2,4 :: Int ..], not $ n `Set.member` freeVars (e,ets) | t <- ets ]
-        f map ((n,t):rs) = t { tvrType = substMap map (tvrType t)} : f (Map.insert n (EVar t) map) rs
-        f _ [] = []
-    return (Just $ foldr ELam (foldl EAp e (map EVar tvrs)) tvrs)
+etaExpandAp dataTable t as | Just (Arity n err) <- Info.lookup (tvrInfo t) = case () of
+    () | n > length as -> do
+            let e = foldl EAp (EVar t) as
+            let (_,ts) = fromPi' dataTable (infertype dataTable e)
+                ets = (take (n - length as) ts)
+            mticks (length ets) ("EtaExpand.use.{" ++ tvrShowName t)
+            let tvrs = f mempty [ (tvrIdent t,t { tvrIdent = n }) |  n <- [2,4 :: Int ..], not $ n `Set.member` freeVars (e,ets) | t <- ets ]
+                f map ((n,t):rs) = t { tvrType = substMap map (tvrType t)} : f (Map.insert n (EVar t) map) rs
+                f _ [] = []
+            return (Just $ foldr ELam (foldl EAp e (map EVar tvrs)) tvrs)
+       | err && length as > n -> do
+            let ot = infertype dataTable (foldl EAp (EVar t) as)
+            mticks (length as - n) ("EtaExpand.bottoming.{" ++ tvrShowName t)
+            return $ Just (prim_unsafeCoerce ot (foldl EAp (EVar t) (take n as)))  -- we can drop any extra arguments applied to something that bottoms out.
+       | otherwise -> return Nothing
+
hunk ./E/SSimplify.hs 207
+                (t,e) <- etaExpandDef' (so_dataTable sopts) t e
hunk ./E/SSimplify.hs 211
-                (t,e') <- etaExpandDef' (so_dataTable sopts) t e'
hunk ./E/SSimplify.hs 213
+    go :: E -> Env -> NameMT Int (StatT Identity) E
hunk ./E/SSimplify.hs 217
-    go :: E -> Env -> NameMT Int (StatT Identity) E
hunk ./E/SSimplify.hs 229
-        xs' <- mapM (dosub sub) xs
-        x' <- g x sub inb
-        x'' <- coerceOpt return x'
-        x <- primOpt' (so_dataTable sopts) x''
-        h x xs' inb
-        --app (x,xs')
+        eed <- etaExpandDef (so_dataTable sopts) tvr { tvrIdent = 0 } e
+        case eed of
+            Just (_,e) -> go e inb
+            Nothing -> do
+                xs' <- mapM (dosub sub) xs
+                x' <- g x sub inb
+                x'' <- coerceOpt return x'
+                x <- primOpt' (so_dataTable sopts) x''
+                h x xs' inb
hunk ./E/SSimplify.hs 258
-        e' <- f e sub inb
-        doCase e' (eCaseType ec) b as d sub inb
+        eed <- etaExpandDef (so_dataTable sopts) tvr { tvrIdent = 0 } ec
+        case eed of
+            Just (_,e) -> go e inb
+            Nothing -> do
+                e' <- f e sub inb
+                doCase e' (eCaseType ec) b as d sub inb
hunk ./E/SSimplify.hs 297
+        ds <- sequence [ etaExpandDef' (so_dataTable sopts) t e | (t,e) <- ds]
hunk ./E/SSimplify.hs 480
+{-
hunk ./E/SSimplify.hs 497
-
+  -}
hunk ./E/SSimplify.hs 523
-    h e xs' inb = do
-        app (e,xs')
+    h e xs' inb = do app (e,xs')
hunk ./Main.hs 761
+    wdump FD.EInfo $ putErrLn (show $ tvrInfo tvr)