From 5765efc372a628ede62d8b27c799708f530a3456 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@hcoop.net>
Date: Tue, 6 Oct 2009 15:39:27 -0400
Subject: SELECT DISTINCT; eta expansion during Cjrization

---
 src/cjrize.sml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'src/cjrize.sml')

diff --git a/src/cjrize.sml b/src/cjrize.sml
index 6a79b4e6..bf814266 100644
--- a/src/cjrize.sml
+++ b/src/cjrize.sml
@@ -520,9 +520,14 @@ fun cifyDecl ((d, loc), sm) =
                                           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)
-- 
cgit v1.2.3