Mercurial > urweb

comparison src/elab_env.sml @ 59:abb2b32c19fb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Subsignatures
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Jun 2008 19:10:38 -0400
parents d3cc191cb25f
children 7bab29834cd6
comparison
equal deleted inserted replaced
58:fd8a81ecd598 59:abb2b32c19fb
296 case sgi of 296 case sgi of
297 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE 297 SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE
298 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) 298 | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c)
299 | SgiVal (x, n, t) => pushENamedAs env x n t 299 | SgiVal (x, n, t) => pushENamedAs env x n t
300 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn 300 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
301 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
301 302
302 fun sgnSeek f sgis = 303 fun sgnSeek f sgis =
303 let 304 let
304 fun seek (sgis, strs, cons) = 305 fun seek (sgis, sgns, strs, cons) =
305 case sgis of 306 case sgis of
306 [] => NONE 307 [] => NONE
307 | (sgi, _) :: sgis => 308 | (sgi, _) :: sgis =>
308 case f sgi of 309 case f sgi of
309 SOME v => SOME (v, (strs, cons)) 310 SOME v => SOME (v, (sgns, strs, cons))
310 | NONE => 311 | NONE =>
311 case sgi of 312 case sgi of
312 SgiConAbs (x, n, _) => seek (sgis, strs, IM.insert (cons, n, x)) 313 SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
313 | SgiCon (x, n, _, _) => seek (sgis, strs, IM.insert (cons, n, x)) 314 | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
314 | SgiVal _ => seek (sgis, strs, cons) 315 | SgiVal _ => seek (sgis, sgns, strs, cons)
315 | SgiStr (x, n, _) => seek (sgis, IM.insert (strs, n, x), cons) 316 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons)
316 in 317 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons)
317 seek (sgis, IM.empty, IM.empty) 318 in
319 seek (sgis, IM.empty, IM.empty, IM.empty)
318 end 320 end
319 321
320 fun id x = x 322 fun id x = x
321 323
322 fun unravelStr (str, _) = 324 fun unravelStr (str, _) =
328 in 330 in
329 (x, ms @ [m]) 331 (x, ms @ [m])
330 end 332 end
331 | _ => raise Fail "unravelStr" 333 | _ => raise Fail "unravelStr"
332 334
333 fun sgnS_con (str, (strs, cons)) c = 335 fun sgnS_con (str, (sgns, strs, cons)) c =
334 case c of 336 case c of
335 CModProj (m1, ms, x) => 337 CModProj (m1, ms, x) =>
336 (case IM.find (strs, m1) of 338 (case IM.find (strs, m1) of
337 NONE => c 339 NONE => c
338 | SOME m1x => 340 | SOME m1x =>
350 in 352 in
351 CModProj (m1, ms, nx) 353 CModProj (m1, ms, nx)
352 end) 354 end)
353 | _ => c 355 | _ => c
354 356
355 fun sgnSubCon (str, (strs, cons)) = 357 fun sgnS_sgn (str, (sgns, strs, cons)) sgn =
358 case sgn of
359 SgnProj (m1, ms, x) =>
360 (case IM.find (strs, m1) of
361 NONE => sgn
362 | SOME m1x =>
363 let
364 val (m1, ms') = unravelStr str
365 in
366 SgnProj (m1, ms' @ m1x :: ms, x)
367 end)
368 | SgnVar n =>
369 (case IM.find (sgns, n) of
370 NONE => sgn
371 | SOME nx =>
372 let
373 val (m1, ms) = unravelStr str
374 in
375 SgnProj (m1, ms, nx)
376 end)
377 | _ => sgn
378
379 fun sgnSubCon x =
356 ElabUtil.Con.map {kind = id, 380 ElabUtil.Con.map {kind = id,
357 con = sgnS_con (str, (strs, cons))} 381 con = sgnS_con x}
358 382
359 fun sgnSubSgn (str, (strs, cons)) = 383 fun sgnSubSgn x =
360 ElabUtil.Sgn.map {kind = id, 384 ElabUtil.Sgn.map {kind = id,
361 con = sgnS_con (str, (strs, cons)), 385 con = sgnS_con x,
362 sgn_item = id, 386 sgn_item = id,
363 sgn = id} 387 sgn = sgnS_sgn x}
364 388
365 fun hnormSgn env (all as (sgn, loc)) = 389 fun hnormSgn env (all as (sgn, loc)) =
366 case sgn of 390 case sgn of
367 SgnError => all 391 SgnError => all
368 | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n)) 392 | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n))
369 | SgnConst _ => all 393 | SgnConst _ => all
370 | SgnFun _ => all 394 | SgnFun _ => all
395 | SgnProj (m, ms, x) =>
396 let
397 val (_, sgn) = lookupStrNamed env m
398 in
399 case projectSgn env {str = foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms,
400 sgn = sgn,
401 field = x} of
402 NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed"
403 | SOME sgn => sgn
404 end
371 | SgnWhere (sgn, x, c) => 405 | SgnWhere (sgn, x, c) =>
372 case #1 (hnormSgn env sgn) of 406 case #1 (hnormSgn env sgn) of
373 SgnError => (SgnError, loc) 407 SgnError => (SgnError, loc)
374 | SgnConst sgis => 408 | SgnConst sgis =>
375 let 409 let
387 in 421 in
388 (SgnConst sgis, loc) 422 (SgnConst sgis, loc)
389 end 423 end
390 | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]" 424 | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]"
391 425
426 and projectSgn env {sgn, str, field} =
427 case #1 (hnormSgn env sgn) of
428 SgnConst sgis =>
429 (case sgnSeek (fn SgiSgn (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
430 NONE => NONE
431 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
432 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
433 | _ => NONE
434
435 fun projectStr env {sgn, str, field} =
436 case #1 (hnormSgn env sgn) of
437 SgnConst sgis =>
438 (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
439 NONE => NONE
440 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
441 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
442 | _ => NONE
443
392 fun projectCon env {sgn, str, field} = 444 fun projectCon env {sgn, str, field} =
393 case #1 (hnormSgn env sgn) of 445 case #1 (hnormSgn env sgn) of
394 SgnConst sgis => 446 SgnConst sgis =>
395 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE 447 (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
396 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE 448 | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
407 NONE => NONE 459 NONE => NONE
408 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c)) 460 | SOME (c, subs) => SOME (sgnSubCon (str, subs) c))
409 | SgnError => SOME (CError, ErrorMsg.dummySpan) 461 | SgnError => SOME (CError, ErrorMsg.dummySpan)
410 | _ => NONE 462 | _ => NONE
411 463
412 fun projectStr env {sgn, str, field} =
413 case #1 (hnormSgn env sgn) of
414 SgnConst sgis =>
415 (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
416 NONE => NONE
417 | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
418 | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
419 | _ => NONE
420 464
421 end 465 end