diff src/reduce.sml @ 315:e21d0dddda09

Unpoly non-recursive function
author Adam Chlipala <adamc@hcoop.net>
date Thu, 11 Sep 2008 09:36:47 -0400
parents 2f574c07df2e
children f307cdd08d81
line wrap: on
line diff
--- a/src/reduce.sml	Tue Sep 09 12:36:13 2008 -0400
+++ b/src/reduce.sml	Thu Sep 11 09:36:47 2008 -0400
@@ -65,33 +65,8 @@
                 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
                         | (ctx, _) => ctx}
 
-val liftConInExp =
-    U.Exp.mapB {kind = fn k => k,
-                con = fn bound => fn c =>
-                                     case c of
-                                         CRel xn =>
-                                         if xn < bound then
-                                             c
-                                         else
-                                             CRel (xn + 1)
-                                       | _ => c,
-                exp = fn _ => fn e => e,
-                bind = fn (bound, U.Exp.RelC _) => bound + 1
-                        | (bound, _) => bound}
-
-val subConInExp =
-    U.Exp.mapB {kind = fn k => k,
-                con = fn (xn, rep) => fn c =>
-                                  case c of
-                                      CRel xn' =>
-                                      (case Int.compare (xn', xn) of
-                                           EQUAL => #1 rep
-                                         | GREATER => CRel (xn' - 1)
-                                         | LESS => c)
-                                    | _ => c,
-                exp = fn _ => fn e => e,
-                bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep)
-                        | (ctx, _) => ctx}
+val liftConInExp = E.liftConInExp
+val subConInExp = E.subConInExp
 
 fun bindC (env, b) =
     case b of