Mercurial > urweb

comparison src/core_env.sml @ 443:bd9ee9aeca2f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Especialize
author Adam Chlipala <adamc@hcoop.net>
date Thu, 30 Oct 2008 16:58:54 -0400
parents e0e9e9eca1cb
children 5c9606deacb6
comparison
equal deleted inserted replaced
442:9095a95a1bf9 443:bd9ee9aeca2f
89 | GREATER => CRel (xn' - 1) 89 | GREATER => CRel (xn' - 1)
90 | LESS => c) 90 | LESS => c)
91 | _ => c, 91 | _ => c,
92 exp = fn _ => fn e => e, 92 exp = fn _ => fn e => e,
93 bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep) 93 bind = fn ((xn, rep), U.Exp.RelC _) => (xn+1, liftConInCon 0 rep)
94 | (ctx, _) => ctx}
95
96 val liftExpInExp =
97 U.Exp.mapB {kind = fn k => k,
98 con = fn _ => fn c => c,
99 exp = fn bound => fn e =>
100 case e of
101 ERel xn =>
102 if xn < bound then
103 e
104 else
105 ERel (xn + 1)
106 | _ => e,
107 bind = fn (bound, U.Exp.RelE _) => bound + 1
108 | (bound, _) => bound}
109
110 val subExpInExp =
111 U.Exp.mapB {kind = fn k => k,
112 con = fn _ => fn c => c,
113 exp = fn (xn, rep) => fn e =>
114 case e of
115 ERel xn' =>
116 (case Int.compare (xn', xn) of
117 EQUAL => #1 rep
118 | GREATER=> ERel (xn' - 1)
119 | LESS => e)
120 | _ => e,
121 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
122 | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep)
94 | (ctx, _) => ctx} 123 | (ctx, _) => ctx}
95 124
96 (* Back to environments *) 125 (* Back to environments *)
97 126
98 exception UnboundRel of int 127 exception UnboundRel of int