Mercurial > urweb

comparison src/elab_env.sml @ 16:bc7b76ca57e0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Conversion to Core
author Adam Chlipala <adamc@hcoop.net>
date Sun, 08 Jun 2008 13:59:29 -0400
parents f1c36df29ed7
children 9bd8669d53c2
comparison
equal deleted inserted replaced
15:1e645beb3f3b 16:bc7b76ca57e0
27 27
28 structure ElabEnv :> ELAB_ENV = struct 28 structure ElabEnv :> ELAB_ENV = struct
29 29
30 open Elab 30 open Elab
31 31
32 structure L' = Elab
33 structure U = ElabUtil 32 structure U = ElabUtil
34 33
35 structure IM = IntBinaryMap 34 structure IM = IntBinaryMap
36 structure SM = BinaryMapFn(struct 35 structure SM = BinaryMapFn(struct
37 type ord_key = string 36 type ord_key = string
48 47
49 val liftConInCon = 48 val liftConInCon =
50 U.Con.mapB {kind = fn k => k, 49 U.Con.mapB {kind = fn k => k,
51 con = fn bound => fn c => 50 con = fn bound => fn c =>
52 case c of 51 case c of
53 L'.CRel xn => 52 CRel xn =>
54 if xn < bound then 53 if xn < bound then
55 c 54 c
56 else 55 else
57 L'.CRel (xn + 1) 56 CRel (xn + 1)
58 | L'.CUnif _ => raise SynUnif 57 | CUnif _ => raise SynUnif
59 | _ => c, 58 | _ => c,
60 bind = fn (bound, U.Con.Rel _) => bound + 1 59 bind = fn (bound, U.Con.Rel _) => bound + 1
61 | (bound, _) => bound} 60 | (bound, _) => bound}
62 61
63 val lift = liftConInCon 0 62 val lift = liftConInCon 0