Mercurial > urweb
comparison src/core_env.sml @ 315:e21d0dddda09
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 |