Mercurial > urweb

comparison src/core_env.sml @ 417:e0e9e9eca1cb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fix nasty de Bruijn substitution bug; TcSum demo
author Adam Chlipala <adamc@hcoop.net>
date Thu, 23 Oct 2008 12:58:35 -0400
parents e976b187d73a
children bd9ee9aeca2f
comparison
equal deleted inserted replaced
416:679b2fbbd4d0 417:e0e9e9eca1cb
80 | (bound, _) => bound} 80 | (bound, _) => bound}
81 81
82 val subConInExp = 82 val subConInExp =
83 U.Exp.mapB {kind = fn k => k, 83 U.Exp.mapB {kind = fn k => k,
84 con = fn (xn, rep) => fn c => 84 con = fn (xn, rep) => fn c =>
85 case c of 85 case c of
86 CRel xn' => 86 CRel xn' =>
87 (case Int.compare (xn', xn) of 87 (case Int.compare (xn', xn) of
88 EQUAL => #1 rep 88 EQUAL => #1 rep
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} 94 | (ctx, _) => ctx}
95 95
96 (* Back to environments *) 96 (* Back to environments *)