Mercurial > urweb

comparison src/elab_env.sml @ 31:1c91c5e6840f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Simple signature matching
author Adam Chlipala <adamc@hcoop.net>
date Thu, 12 Jun 2008 17:16:20 -0400
parents 9bd8669d53c2
children 44b5405e74c7
comparison
equal deleted inserted replaced
30:e6ccf961d8a3 31:1c91c5e6840f
78 relC : (string * kind) list, 78 relC : (string * kind) list,
79 namedC : (string * kind * con option) IM.map, 79 namedC : (string * kind * con option) IM.map,
80 80
81 renameE : con var' SM.map, 81 renameE : con var' SM.map,
82 relE : (string * con) list, 82 relE : (string * con) list,
83 namedE : (string * con) IM.map 83 namedE : (string * con) IM.map,
84
85 renameSgn : (int * sgn) SM.map,
86 sgn : (string * sgn) IM.map,
87
88 renameStr : (int * sgn) SM.map,
89 str : (string * sgn) IM.map
84 } 90 }
85 91
86 val namedCounter = ref 0 92 val namedCounter = ref 0
87 93
88 val empty = { 94 val empty = {
90 relC = [], 96 relC = [],
91 namedC = IM.empty, 97 namedC = IM.empty,
92 98
93 renameE = SM.empty, 99 renameE = SM.empty,
94 relE = [], 100 relE = [],
95 namedE = IM.empty 101 namedE = IM.empty,
102
103 renameSgn = SM.empty,
104 sgn = IM.empty,
105
106 renameStr = SM.empty,
107 str = IM.empty
96 } 108 }
97 109
98 fun pushCRel (env : env) x k = 110 fun pushCRel (env : env) x k =
99 let 111 let
100 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) 112 val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k)
104 relC = (x, k) :: #relC env, 116 relC = (x, k) :: #relC env,
105 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env), 117 namedC = IM.map (fn (x, k, co) => (x, k, Option.map lift co)) (#namedC env),
106 118
107 renameE = #renameE env, 119 renameE = #renameE env,
108 relE = map (fn (x, c) => (x, lift c)) (#relE env), 120 relE = map (fn (x, c) => (x, lift c)) (#relE env),
109 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env)} 121 namedE = IM.map (fn (x, c) => (x, lift c)) (#namedE env),
122
123 renameSgn = #renameSgn env,
124 sgn = #sgn env,
125
126 renameStr = #renameStr env,
127 str = #str env
128 }
110 end 129 end
111 130
112 fun lookupCRel (env : env) n = 131 fun lookupCRel (env : env) n =
113 (List.nth (#relC env, n)) 132 (List.nth (#relC env, n))
114 handle Subscript => raise UnboundRel n 133 handle Subscript => raise UnboundRel n
118 relC = #relC env, 137 relC = #relC env,
119 namedC = IM.insert (#namedC env, n, (x, k, co)), 138 namedC = IM.insert (#namedC env, n, (x, k, co)),
120 139
121 renameE = #renameE env, 140 renameE = #renameE env,
122 relE = #relE env, 141 relE = #relE env,
123 namedE = #namedE env} 142 namedE = #namedE env,
143
144 renameSgn = #renameSgn env,
145 sgn = #sgn env,
146
147 renameStr = #renameStr env,
148 str = #str env}
124 149
125 fun pushCNamed env x k co = 150 fun pushCNamed env x k co =
126 let 151 let
127 val n = !namedCounter 152 val n = !namedCounter
128 in 153 in
150 relC = #relC env, 175 relC = #relC env,
151 namedC = #namedC env, 176 namedC = #namedC env,
152 177
153 renameE = SM.insert (renameE, x, Rel' (0, t)), 178 renameE = SM.insert (renameE, x, Rel' (0, t)),
154 relE = (x, t) :: #relE env, 179 relE = (x, t) :: #relE env,
155 namedE = #namedE env} 180 namedE = #namedE env,
181
182 renameSgn = #renameSgn env,
183 sgn = #sgn env,
184
185 renameStr = #renameStr env,
186 str = #str env}
156 end 187 end
157 188
158 fun lookupERel (env : env) n = 189 fun lookupERel (env : env) n =
159 (List.nth (#relE env, n)) 190 (List.nth (#relE env, n))
160 handle Subscript => raise UnboundRel n 191 handle Subscript => raise UnboundRel n
164 relC = #relC env, 195 relC = #relC env,
165 namedC = #namedC env, 196 namedC = #namedC env,
166 197
167 renameE = SM.insert (#renameE env, x, Named' (n, t)), 198 renameE = SM.insert (#renameE env, x, Named' (n, t)),
168 relE = #relE env, 199 relE = #relE env,
169 namedE = IM.insert (#namedE env, n, (x, t))} 200 namedE = IM.insert (#namedE env, n, (x, t)),
201
202 renameSgn = #renameSgn env,
203 sgn = #sgn env,
204
205 renameStr = #renameStr env,
206 str = #str env}
170 207
171 fun pushENamed env x t = 208 fun pushENamed env x t =
172 let 209 let
173 val n = !namedCounter 210 val n = !namedCounter
174 in 211 in
185 case SM.find (#renameE env, x) of 222 case SM.find (#renameE env, x) of
186 NONE => NotBound 223 NONE => NotBound
187 | SOME (Rel' x) => Rel x 224 | SOME (Rel' x) => Rel x
188 | SOME (Named' x) => Named x 225 | SOME (Named' x) => Named x
189 226
227 fun pushSgnNamedAs (env : env) x n sgis =
228 {renameC = #renameC env,
229 relC = #relC env,
230 namedC = #namedC env,
231
232 renameE = #renameE env,
233 relE = #relE env,
234 namedE = #namedE env,
235
236 renameSgn = SM.insert (#renameSgn env, x, (n, sgis)),
237 sgn = IM.insert (#sgn env, n, (x, sgis)),
238
239 renameStr = #renameStr env,
240 str = #str env}
241
242 fun pushSgnNamed env x sgis =
243 let
244 val n = !namedCounter
245 in
246 namedCounter := n + 1;
247 (pushSgnNamedAs env x n sgis, n)
248 end
249
250 fun lookupSgnNamed (env : env) n =
251 case IM.find (#sgn env, n) of
252 NONE => raise UnboundNamed n
253 | SOME x => x
254
255 fun lookupSgn (env : env) x = SM.find (#renameSgn env, x)
256
257 fun pushStrNamedAs (env : env) x n sgis =
258 {renameC = #renameC env,
259 relC = #relC env,
260 namedC = #namedC env,
261
262 renameE = #renameE env,
263 relE = #relE env,
264 namedE = #namedE env,
265
266 renameSgn = #renameSgn env,
267 sgn = #sgn env,
268
269 renameStr = SM.insert (#renameStr env, x, (n, sgis)),
270 str = IM.insert (#str env, n, (x, sgis))}
271
272 fun pushStrNamed env x sgis =
273 let
274 val n = !namedCounter
275 in
276 namedCounter := n + 1;
277 (pushStrNamedAs env x n sgis, n)
278 end
279
280 fun lookupStrNamed (env : env) n =
281 case IM.find (#str env, n) of
282 NONE => raise UnboundNamed n
283 | SOME x => x
284
285 fun lookupStr (env : env) x = SM.find (#renameStr env, x)
286
190 fun declBinds env (d, _) = 287 fun declBinds env (d, _) =
191 case d of 288 case d of
192 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 289 DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
193 | DVal (x, n, t, _) => pushENamedAs env x n t 290 | DVal (x, n, t, _) => pushENamedAs env x n t
291 | DSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
292 | DStr (x, n, sgn, _) => pushStrNamedAs env x n sgn
293
294 fun sgiBinds env (sgi, _) =
295 case sgi of
296 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
297 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
298 | SgiVal (x, n, t) => pushENamedAs env x n t
299 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
300
194 301
195 val ktype = (KType, ErrorMsg.dummySpan) 302 val ktype = (KType, ErrorMsg.dummySpan)
196 303
197 fun bbind env x = #1 (pushCNamed env x ktype NONE) 304 fun bbind env x = #1 (pushCNamed env x ktype NONE)
198 305