diff src/cjrize.sml @ 993:10114d7b7477

SELECT DISTINCT; eta expansion during Cjrization
author Adam Chlipala <adamc@hcoop.net>
date Tue, 06 Oct 2009 15:39:27 -0400
parents 7a4b026e45dd
children 7a4a55e05081
line wrap: on
line diff
--- a/src/cjrize.sml	Tue Oct 06 13:11:03 2009 -0400
+++ b/src/cjrize.sml	Tue Oct 06 15:39:27 2009 -0400
@@ -520,9 +520,14 @@
                                           in
                                               ((ax, dom) :: args, t, e)
                                           end
-                                        | (L'.TFun _, _) =>
-                                          (ErrorMsg.errorAt loc "Function isn't explicit at code generation";
-                                           ([], tAll, eAll))
+                                        | (L'.TFun (dom, ran), _) =>
+                                          let
+                                              val e = MonoEnv.liftExpInExp 0 eAll
+                                              val e = (L.EApp (e, (L.ERel 0, loc)), loc)
+                                              val (args, t, e) = unravel (ran, e)
+                                          in
+                                              (("x", dom) :: args, t, e)
+                                          end
                                         | _ => ([], tAll, eAll)
 
                                   val (args, ran, e) = unravel (t, e)