Mercurial > urweb

comparison src/reduce.sml @ 315:e21d0dddda09

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Unpoly non-recursive function
author Adam Chlipala <adamc@hcoop.net>
date Thu, 11 Sep 2008 09:36:47 -0400
parents 2f574c07df2e
children f307cdd08d81
comparison
equal deleted inserted replaced
314:a07f476d9b61 315:e21d0dddda09
63 | LESS => e) 63 | LESS => e)
64 | _ => e, 64 | _ => e,
65 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) 65 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
66 | (ctx, _) => ctx} 66 | (ctx, _) => ctx}
67 67
68 val liftConInExp = 68 val liftConInExp = E.liftConInExp
69 U.Exp.mapB {kind = fn k => k, 69 val subConInExp = E.subConInExp
70 con = fn bound => fn c =>
71 case c of
72 CRel xn =>
73 if xn < bound then
74 c
75 else
76 CRel (xn + 1)
77 | _ => c,
78 exp = fn _ => fn e => e,
79 bind = fn (bound, U.Exp.RelC _) => bound + 1
80 | (bound, _) => bound}
81
82 val subConInExp =
83 U.Exp.mapB {kind = fn k => k,
84 con = fn (xn, rep) => fn c =>
85 case c of
86 CRel xn' =>
87 (case Int.compare (xn', xn) of
88 EQUAL => #1 rep
89 | GREATER => CRel (xn' - 1)
90 | LESS => c)
91 | _ => c,
92 exp = fn _ => fn e => e,
93 bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep)
94 | (ctx, _) => ctx}
95 70
96 fun bindC (env, b) = 71 fun bindC (env, b) =
97 case b of 72 case b of
98 U.Con.Rel (x, k) => E.pushCRel env x k 73 U.Con.Rel (x, k) => E.pushCRel env x k
99 | U.Con.Named (x, n, k, co) => E.pushCNamed env x n k co 74 | U.Con.Named (x, n, k, co) => E.pushCNamed env x n k co