Mercurial > urweb

comparison src/elaborate.sml @ 413:6a0e54400805

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Sum prose
author Adam Chlipala <adamc@hcoop.net>
date Tue, 21 Oct 2008 19:56:20 -0400
parents df4cbd90a26e
children dfc8c991abd0
comparison
equal deleted inserted replaced
412:df4cbd90a26e 413:6a0e54400805
479 479
480 | L'.CApp (c, _) => 480 | L'.CApp (c, _) =>
481 (case hnormKind (kindof env c) of 481 (case hnormKind (kindof env c) of
482 (L'.KArrow (_, k), _) => k 482 (L'.KArrow (_, k), _) => k
483 | (L'.KError, _) => kerror 483 | (L'.KError, _) => kerror
484 | k => raise CUnify' (CKindof (k, c))) 484 | k => raise CUnify' (CKindof (k, c, "arrow")))
485 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc) 485 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
486 | L'.CDisjoint (_, _, _, c) => kindof env c 486 | L'.CDisjoint (_, _, _, c) => kindof env c
487 487
488 | L'.CName _ => kname 488 | L'.CName _ => kname
489 489
495 495
496 | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc) 496 | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc)
497 | L'.CProj (c, n) => 497 | L'.CProj (c, n) =>
498 (case hnormKind (kindof env c) of 498 (case hnormKind (kindof env c) of
499 (L'.KTuple ks, _) => List.nth (ks, n - 1) 499 (L'.KTuple ks, _) => List.nth (ks, n - 1)
500 | k => raise CUnify' (CKindof (k, c))) 500 | k => raise CUnify' (CKindof (k, c, "tuple")))
501 501
502 | L'.CError => kerror 502 | L'.CError => kerror
503 | L'.CUnif (_, k, _, _) => k 503 | L'.CUnif (_, k, _, _) => k
504 504
505 val hnormCon = D.hnormCon 505 val hnormCon = D.hnormCon
544 let 544 let
545 fun rkindof c = 545 fun rkindof c =
546 case hnormKind (kindof env c) of 546 case hnormKind (kindof env c) of
547 (L'.KRecord k, _) => k 547 (L'.KRecord k, _) => k
548 | (L'.KError, _) => kerror 548 | (L'.KError, _) => kerror
549 | k => raise CUnify' (CKindof (k, c)) 549 | k => raise CUnify' (CKindof (k, c, "record"))
550 550
551 val k1 = rkindof c1 551 val k1 = rkindof c1
552 val k2 = rkindof c2 552 val k2 = rkindof c2
553 553
554 val (r1, gs1) = recordSummary (env, denv) c1 554 val (r1, gs1) = recordSummary (env, denv) c1
2316 let 2316 let
2317 val env = E.sgiBinds env sgi2All 2317 val env = E.sgiBinds env sgi2All
2318 val env = if n1 = n2 then 2318 val env = if n1 = n2 then
2319 env 2319 env
2320 else 2320 else
2321 E.pushCNamedAs env x n1 (L'.KType, loc) 2321 E.pushCNamedAs env x n1 k'
2322 (SOME (L'.CNamed n2, loc)) 2322 (SOME (L'.CNamed n2, loc))
2323 in 2323 in
2324 SOME (env, denv) 2324 SOME (env, denv)
2325 end 2325 end
2326 2326