Mercurial > urweb

comparison src/elab_ops.sml @ 516:11fc77fb8257

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Optimized ElabOps.subConInCon
author Adam Chlipala <adamc@hcoop.net>
date Thu, 27 Nov 2008 10:57:56 -0500
parents 1bbcc3345d12
children 8998114760c1
comparison
equal deleted inserted replaced
515:4929cf86bc03 516:11fc77fb8257
30 open Elab 30 open Elab
31 31
32 structure E = ElabEnv 32 structure E = ElabEnv
33 structure U = ElabUtil 33 structure U = ElabUtil
34 34
35 val liftConInCon = E.liftConInCon 35 fun liftConInCon by =
36
37 val subConInCon =
38 U.Con.mapB {kind = fn k => k, 36 U.Con.mapB {kind = fn k => k,
39 con = fn (xn, rep) => fn c => 37 con = fn bound => fn c =>
40 case c of 38 case c of
41 CRel xn' => 39 CRel xn =>
42 (case Int.compare (xn', xn) of 40 if xn < bound then
43 EQUAL => #1 rep 41 c
44 | GREATER => CRel (xn' - 1) 42 else
45 | LESS => c) 43 CRel (xn + by)
46 (*| CUnif _ => raise SynUnif*) 44 (*| CUnif _ => raise SynUnif*)
47 | _ => c, 45 | _ => c,
48 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) 46 bind = fn (bound, U.Con.Rel _) => bound + 1
47 | (bound, _) => bound}
48
49 fun subConInCon' rep =
50 U.Con.mapB {kind = fn k => k,
51 con = fn (by, xn) => fn c =>
52 case c of
53 CRel xn' =>
54 (case Int.compare (xn', xn) of
55 EQUAL => #1 (liftConInCon by 0 rep)
56 | GREATER => CRel (xn' - 1)
57 | LESS => c)
58 (*| CUnif _ => raise SynUnif*)
59 | _ => c,
60 bind = fn ((by, xn), U.Con.Rel _) => (by+1, xn+1)
49 | (ctx, _) => ctx} 61 | (ctx, _) => ctx}
62
63 val liftConInCon = liftConInCon 1
64
65 fun subConInCon (xn, rep) = subConInCon' rep (0, xn)
50 66
51 fun subStrInSgn (m1, m2) = 67 fun subStrInSgn (m1, m2) =
52 U.Sgn.map {kind = fn k => k, 68 U.Sgn.map {kind = fn k => k,
53 con = fn c as CModProj (m1', ms, x) => 69 con = fn c as CModProj (m1', ms, x) =>
54 if m1 = m1' then 70 if m1 = m1' then