Mercurial > urweb

comparison src/elab_env.sml @ 448:85819353a84f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
First Unnest tests working
author Adam Chlipala <adamc@hcoop.net>
date Sat, 01 Nov 2008 15:58:55 -0400
parents b77863cd0be2
children 222cbc1da232
comparison
equal deleted inserted replaced
447:b77863cd0be2 448:85819353a84f
59 bind = fn (bound, U.Con.Rel _) => bound + 1 59 bind = fn (bound, U.Con.Rel _) => bound + 1
60 | (bound, _) => bound} 60 | (bound, _) => bound}
61 61
62 val lift = liftConInCon 0 62 val lift = liftConInCon 0
63 63
64 val liftConInExp =
65 U.Exp.mapB {kind = fn k => k,
66 con = fn bound => fn c =>
67 case c of
68 CRel xn =>
69 if xn < bound then
70 c
71 else
72 CRel (xn + 1)
73 | _ => c,
74 exp = fn _ => fn e => e,
75 bind = fn (bound, U.Exp.RelC _) => bound + 1
76 | (bound, _) => bound}
77
64 val liftExpInExp = 78 val liftExpInExp =
65 U.Exp.mapB {kind = fn k => k, 79 U.Exp.mapB {kind = fn k => k,
66 con = fn _ => fn c => c, 80 con = fn _ => fn c => c,
67 exp = fn bound => fn e => 81 exp = fn bound => fn e =>
68 case e of 82 case e of
75 bind = fn (bound, U.Exp.RelE _) => bound + 1 89 bind = fn (bound, U.Exp.RelE _) => bound + 1
76 | (bound, _) => bound} 90 | (bound, _) => bound}
77 91
78 92
79 val liftExp = liftExpInExp 0 93 val liftExp = liftExpInExp 0
94
95 val subExpInExp =
96 U.Exp.mapB {kind = fn k => k,
97 con = fn _ => fn c => c,
98 exp = fn (xn, rep) => fn e =>
99 case e of
100 ERel xn' =>
101 (case Int.compare (xn', xn) of
102 EQUAL => #1 rep
103 | GREATER=> ERel (xn' - 1)
104 | LESS => e)
105 | _ => e,
106 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
107 | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep)
108 | (ctx, _) => ctx}
80 109
81 (* Back to environments *) 110 (* Back to environments *)
82 111
83 datatype 'a var' = 112 datatype 'a var' =
84 Rel' of int * 'a 113 Rel' of int * 'a