Mercurial > urweb

comparison src/core_env.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 42dfb0d61cf0
children e976b187d73a
comparison
equal deleted inserted replaced
314:a07f476d9b61 315:e21d0dddda09
63 | _ => c, 63 | _ => c,
64 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) 64 bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
65 | (ctx, _) => ctx} 65 | (ctx, _) => ctx}
66 66
67 67
68 val liftConInExp =
69 U.Exp.mapB {kind = fn k => k,
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
68 (* Back to environments *) 96 (* Back to environments *)
69 97
70 exception UnboundRel of int 98 exception UnboundRel of int
71 exception UnboundNamed of int 99 exception UnboundNamed of int
72 100