Mercurial > urweb

diff src/elab_ops.sml @ 905:7a4b026e45dd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Library improvements; proper list [un]urlification; remove server-side ServerCalls; eta reduction in type inference
author Adam Chlipala <adamc@hcoop.net>
date Sun, 09 Aug 2009 16:13:27 -0400
parents 12b73f3c108e
children 46803e668a89
line wrap: on
line diff
--- a/src/elab_ops.sml	Thu Aug 06 15:23:04 2009 -0400
+++ b/src/elab_ops.sml	Sun Aug 09 16:13:27 2009 -0400
@@ -131,6 +131,18 @@
                sgn_item = fn sgi => sgi,
                sgn = fn sgn => sgn}
 
+val occurs =
+    U.Con.existsB {kind = fn _ => false,
+                   con = fn (n, c) =>
+                            case c of
+                                CRel n' => n' = n
+                              | _ => false,
+                   bind = fn (n, b) =>
+                             case b of
+                                 U.Con.RelC _ => n + 1
+                               | _ => n}
+                  0
+
 
 fun hnormCon env (cAll as (c, loc)) =
     case c of
@@ -156,6 +168,16 @@
               | SOME (_, SOME c) => hnormCon env c
         end
 
+      (* Eta reduction *)
+      | CAbs (x, k, b) =>
+        (case #1 (hnormCon (E.pushCRel env x k) b) of
+             CApp (f, (CRel 0, _)) =>
+             if occurs f then
+                 cAll
+             else
+                 hnormCon env (subConInCon (0, (CUnit, loc)) f)
+           | _ => cAll)
+
       | CApp (c1, c2) =>
         (case #1 (hnormCon env c1) of
              CAbs (x, k, cb) =>