diff src/reduce_local.sml @ 721:9864b64b1700

Classes as optional arguments to Basis.tag
author Adam Chlipala <adamc@hcoop.net>
date Sun, 12 Apr 2009 14:19:15 -0400
parents f152f215a02c
children 8688e01ae469
line wrap: on
line diff
--- a/src/reduce_local.sml	Sun Apr 12 12:31:54 2009 -0400
+++ b/src/reduce_local.sml	Sun Apr 12 14:19:15 2009 -0400
@@ -72,6 +72,11 @@
       | EFfi _ => all
       | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
 
+      | EApp ((ECApp ((ECAbs (_, _, (EAbs (_, (CRel 0, _), _,
+                                           (ECon (dk, pc, [(CRel 0, loc)], SOME (ERel 0, _)), _)), _)), _),
+                      t), _), e) =>
+        (ECon (dk, pc, [t], SOME (exp env e)), loc)
+
       | EApp (e1, e2) =>
         let
             val e1 = exp env e1
@@ -84,6 +89,9 @@
 
       | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc)
 
+      | ECApp ((ECAbs (_, _, (ECon (dk, pc, [(CRel 0, loc)], NONE), _)), _), t) =>
+        (ECon (dk, pc, [t], NONE), loc)
+
       | ECApp (e, c) => (ECApp (exp env e, c), loc)
       | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc)