[eta expand functions that are always called with at least a certain number of arguments
John Meacham <john@repetae.net>**20060814104920] hunk ./E/Eta.hs 110
-    f (t,e) = etaExpandDef' (progDataTable prog) t e
+    f (t,e) = etaExpandDef' (progDataTable prog) 0 t e
hunk ./E/Eta.hs 146
-etaExpandDef' dataTable t e = etaExpandDef dataTable t e >>= \x -> case x of
+etaExpandDef' dataTable n t e = etaExpandDef dataTable n t e >>= \x -> case x of
hunk ./E/Eta.hs 153
-etaExpandDef :: (NameMonad Id m,Stats.MonadStats m) => DataTable -> TVr -> E -> m (Maybe (TVr,E))
-etaExpandDef _ _ e | isAtomic e = return Nothing -- will be inlined
-etaExpandDef dataTable t e  = ans where
+etaExpandDef :: (NameMonad Id m,Stats.MonadStats m)
+    => DataTable
+    -> Int        -- ^ eta expand at least this far, independent of calculated amount
+    -> TVr
+    -> E
+    -> m (Maybe (TVr,E))
+etaExpandDef _ _ _ e | isAtomic e = return Nothing -- will be inlined
+etaExpandDef dataTable min t e  = ans where
hunk ./E/Eta.hs 171
-        (ne,flag) <- f at e (expandPis dataTable $ infertype dataTable e) nameSupply
+        (ne,flag) <- f min at e (expandPis dataTable $ infertype dataTable e) nameSupply
hunk ./E/Eta.hs 173
-    f (AFun _ a) (ELam tvr e) (EPi tvr' rt) _ns = do
-        (ne,flag) <- f a e (subst tvr' (EVar tvr) rt) _ns
+    f min (AFun _ a) (ELam tvr e) (EPi tvr' rt) _ns = do
+        (ne,flag) <- f (min - 1) a e (subst tvr' (EVar tvr) rt) _ns
hunk ./E/Eta.hs 176
-    f (AFun _ a) e (EPi tt rt) _nns = do
+    f min (AFun _ a) e (EPi tt rt) _nns = do
hunk ./E/Eta.hs 183
-        (ne,_) <- f a eb (subst tt (EVar nv) rt) _nns
+        (ne,_) <- f (min - 1) a eb (subst tt (EVar nv) rt) _nns
hunk ./E/Eta.hs 185
-    f _ e _ _ = do
+    f min a e (EPi tt rt) _nns | min > 0 = do
+        if tvrIdent t == 0
+         then Stats.mtick ("EtaExpand.min." ++ zeroName)
+          else Stats.mtick ("EtaExpand.min.def.{" ++ tvrShowName t)
+        n <- newName
+        let nv = tt { tvrIdent = n }
+            eb = EAp e (EVar nv)
+        (ne,_) <- f (min - 1) a eb (subst tt (EVar nv) rt) _nns
+        return (ELam nv ne,True)
+    f _ _ e _ _ = do
hunk ./E/Eta.hs 202
-    r <- etaExpandDef dataTable tvr { tvrIdent = 0} (foldl EAp (EVar tvr) xs)
+    r <- etaExpandDef dataTable 0 tvr { tvrIdent = 0} (foldl EAp (EVar tvr) xs)
hunk ./E/SSimplify.hs 475
-        eed <- etaExpandDef (so_dataTable sopts) tvr { tvrIdent = 0 } e
+        eed <- etaExpandDef (so_dataTable sopts) 0 tvr { tvrIdent = 0 } e
hunk ./E/SSimplify.hs 829
-        ds' <- sequence [ etaExpandDef' (so_dataTable sopts) t e | (t,e) <- ds']
+        let minArgs t = case Info.lookup (tvrInfo t) of
+                Just (UseInfo { minimumArgs = min }) -> min
+                Nothing -> 0
+
+        ds' <- sequence [ etaExpandDef' (so_dataTable sopts) (minArgs t) t e | (t,e) <- ds']
hunk ./Main.hs 427
-            (v,lc) <- Stats.runStatIO stats (runNameMT $ etaExpandDef' fullDataTable v lc)
+            (v,lc) <- Stats.runStatIO stats (runNameMT $ etaExpandDef' fullDataTable 0 v lc)
hunk ./Main.hs 438
-            (v,lc) <- Stats.runStatIO stats (runNameMT $ etaExpandDef' fullDataTable v lc)
+            (v,lc) <- Stats.runStatIO stats (runNameMT $ etaExpandDef' fullDataTable 0 v lc)