Mercurial > urweb

comparison src/elaborate.sml @ 13:6049e2193bf2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Lifting cons in ElabEnv
author Adam Chlipala <adamc@hcoop.net>
date Sun, 08 Jun 2008 11:32:48 -0400
parents d89477f07c1e
children f1c36df29ed7
comparison
equal deleted inserted replaced
12:d89477f07c1e 13:6049e2193bf2
342 eprefaces "Kind unification variable blocks kindof calculation" 342 eprefaces "Kind unification variable blocks kindof calculation"
343 [("Con", p_con env c)] 343 [("Con", p_con env c)]
344 | CRecordFailure => 344 | CRecordFailure =>
345 eprefaces "Can't unify record constructors" [] 345 eprefaces "Can't unify record constructors" []
346 346
347 exception SynUnif 347 exception SynUnif = E.SynUnif
348 348 val liftConInCon = E.liftConInCon
349 val liftConInCon =
350 U.Con.mapB {kind = fn k => k,
351 con = fn bound => fn c =>
352 case c of
353 L'.CRel xn =>
354 if xn < bound then
355 c
356 else
357 L'.CRel (xn + 1)
358 | L'.CUnif _ => raise SynUnif
359 | _ => c,
360 bind = fn (bound, U.Con.Rel _) => bound + 1
361 | (bound, _) => bound}
362 349
363 val subConInCon = 350 val subConInCon =
364 U.Con.mapB {kind = fn k => k, 351 U.Con.mapB {kind = fn k => k,
365 con = fn (xn, rep) => fn c => 352 con = fn (xn, rep) => fn c =>
366 case c of 353 case c of