Mercurial > urweb

comparison src/elab_env.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 e97c6d335869
children f1c36df29ed7
comparison
equal deleted inserted replaced
12:d89477f07c1e 13:6049e2193bf2
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
34
32 structure IM = IntBinaryMap 35 structure IM = IntBinaryMap
33 structure SM = BinaryMapFn(struct 36 structure SM = BinaryMapFn(struct
34 type ord_key = string 37 type ord_key = string
35 val compare = String.compare 38 val compare = String.compare
36 end) 39 end)
37 40
38 exception UnboundRel of int 41 exception UnboundRel of int
39 exception UnboundNamed of int 42 exception UnboundNamed of int
43
44
45 (* AST utility functions *)
46
47 exception SynUnif
48
49 val liftConInCon =
50 U.Con.mapB {kind = fn k => k,
51 con = fn bound => fn c =>
52 case c of
53 L'.CRel xn =>
54 if xn < bound then
55 c
56 else
57 L'.CRel (xn + 1)
58 | L'.CUnif _ => raise SynUnif
59 | _ => c,
60 bind = fn (bound, U.Con.Rel _) => bound + 1
61 | (bound, _) => bound}
62
63 val lift = liftConInCon 0
64
65
66 (* Back to environments *)
40 67
41 datatype 'a var' = 68 datatype 'a var' =
42 Rel' of int * 'a 69 Rel' of int * 'a
43 | Named' of int * 'a 70 | Named' of int * 'a
44 71
74 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) 101 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
75 | x => x) (#renameC env) 102 | x => x) (#renameC env)
76 in 103 in
77 {renameC = SM.insert (renameC, x, Rel' (0, k)), 104 {renameC = SM.insert (renameC, x, Rel' (0, k)),
78 relC = (x, k) :: #relC env, 105 relC = (x, k) :: #relC env,
79 namedC = #namedC env, 106 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
80 107
81 renameE = #renameE env, 108 renameE = #renameE env,
82 relE = #relE env, 109 relE = map (fn (x, c) => (x, lift c)) (#relE env),
83 namedE = #namedE env} 110 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env)}
84 end 111 end
85 112
86 fun lookupCRel (env : env) n = 113 fun lookupCRel (env : env) n =
87 (List.nth (#relC env, n)) 114 (List.nth (#relC env, n))
88 handle Subscript => raise UnboundRel n 115 handle Subscript => raise UnboundRel n
159 case SM.find (#renameE env, x) of 186 case SM.find (#renameE env, x) of
160 NONE => NotBound 187 NONE => NotBound
161 | SOME (Rel' x) => Rel x 188 | SOME (Rel' x) => Rel x
162 | SOME (Named' x) => Named x 189 | SOME (Named' x) => Named x
163 190
191 fun declBinds env (d, _) =
192 case d of
193 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
194 | DVal (x, n, t, _) => pushENamedAs env x n t
195
164 end 196 end