Mercurial > urweb
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)