comparison src/expl_env.sml @ 162:06a98129b23f

Add datatype import constructor annotations; datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Tue, 29 Jul 2008 12:30:04 -0400
parents 541282b81454
children aa54250f58ac
comparison
equal deleted inserted replaced
161:a5ae7b3e37a4 162:06a98129b23f
234 fun lookupStrNamed (env : env) n = 234 fun lookupStrNamed (env : env) n =
235 case IM.find (#str env, n) of 235 case IM.find (#str env, n) of
236 NONE => raise UnboundNamed n 236 NONE => raise UnboundNamed n
237 | SOME x => x 237 | SOME x => x
238 238
239 fun declBinds env (d, _) = 239 fun declBinds env (d, loc) =
240 case d of 240 case d of
241 DCon (x, n, k, c) => pushCNamed env x n k (SOME c) 241 DCon (x, n, k, c) => pushCNamed env x n k (SOME c)
242 | DDatatype (x, n, xncs) =>
243 let
244 val env = pushCNamed env x n (KType, loc) NONE
245 in
246 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc)
247 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc))
248 env xncs
249 end
250 | DDatatypeImp (x, n, m, ms, x', xncs) =>
251 let
252 val t = (CModProj (m, ms, x'), loc)
253 val env = pushCNamed env x n (KType, loc) (SOME t)
254
255 val t = (CNamed n, loc)
256 in
257 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' t
258 | ((x', n', SOME t'), env) => pushENamed env x' n' (TFun (t', t), loc))
259 env xncs
260 end
242 | DVal (x, n, t, _) => pushENamed env x n t 261 | DVal (x, n, t, _) => pushENamed env x n t
243 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamed env x n t) env vis 262 | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamed env x n t) env vis
244 | DSgn (x, n, sgn) => pushSgnNamed env x n sgn 263 | DSgn (x, n, sgn) => pushSgnNamed env x n sgn
245 | DStr (x, n, sgn, _) => pushStrNamed env x n sgn 264 | DStr (x, n, sgn, _) => pushStrNamed env x n sgn
246 | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn 265 | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn
247 | DExport _ => env 266 | DExport _ => env
248 267
249 fun sgiBinds env (sgi, _) = 268 fun sgiBinds env (sgi, loc) =
250 case sgi of 269 case sgi of
251 SgiConAbs (x, n, k) => pushCNamed env x n k NONE 270 SgiConAbs (x, n, k) => pushCNamed env x n k NONE
252 | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c) 271 | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c)
272 | SgiDatatype (x, n, xncs) =>
273 let
274 val env = pushCNamed env x n (KType, loc) NONE
275 in
276 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc)
277 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc))
278 env xncs
279 end
280 | SgiDatatypeImp (x, n, m1, ms, x', xncs) =>
281 let
282 val env = pushCNamed env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc))
283 in
284 foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc)
285 | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc))
286 env xncs
287 end
253 | SgiVal (x, n, t) => pushENamed env x n t 288 | SgiVal (x, n, t) => pushENamed env x n t
254 | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn 289 | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn
255 | SgiStr (x, n, sgn) => pushStrNamed env x n sgn 290 | SgiStr (x, n, sgn) => pushStrNamed env x n sgn
256 291
257 end 292 end