Mercurial > urweb

comparison src/elaborate.sml @ 141:63c699450281

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial form support
author Adam Chlipala <adamc@hcoop.net>
date Sun, 20 Jul 2008 11:33:23 -0400
parents f214c535d253
children 80ac94b54e41
comparison
equal deleted inserted replaced
140:f214c535d253 141:63c699450281
442 datatype cunify_error = 442 datatype cunify_error =
443 CKind of L'.kind * L'.kind * kunify_error 443 CKind of L'.kind * L'.kind * kunify_error
444 | COccursCheckFailed of L'.con * L'.con 444 | COccursCheckFailed of L'.con * L'.con
445 | CIncompatible of L'.con * L'.con 445 | CIncompatible of L'.con * L'.con
446 | CExplicitness of L'.con * L'.con 446 | CExplicitness of L'.con * L'.con
447 | CKindof of L'.con 447 | CKindof of L'.kind * L'.con
448 | CRecordFailure 448 | CRecordFailure
449 449
450 exception CUnify' of cunify_error 450 exception CUnify' of cunify_error
451 451
452 fun cunifyError env err = 452 fun cunifyError env err =
466 ("Con 2", p_con env c2)] 466 ("Con 2", p_con env c2)]
467 | CExplicitness (c1, c2) => 467 | CExplicitness (c1, c2) =>
468 eprefaces "Differing constructor function explicitness" 468 eprefaces "Differing constructor function explicitness"
469 [("Con 1", p_con env c1), 469 [("Con 1", p_con env c1),
470 ("Con 2", p_con env c2)] 470 ("Con 2", p_con env c2)]
471 | CKindof c => 471 | CKindof (k, c) =>
472 eprefaces "Kind unification variable blocks kindof calculation" 472 eprefaces "Kind unification variable blocks kindof calculation"
473 [("Con", p_con env c)] 473 [("Kind", p_kind k),
474 ("Con", p_con env c)]
474 | CRecordFailure => 475 | CRecordFailure =>
475 eprefaces "Can't unify record constructors" [] 476 eprefaces "Can't unify record constructors" []
476 477
477 exception SynUnif = E.SynUnif 478 exception SynUnif = E.SynUnif
478 479
524 NONE => raise Fail "kindof: Unknown con in structure" 525 NONE => raise Fail "kindof: Unknown con in structure"
525 | SOME (k, _) => k 526 | SOME (k, _) => k
526 end 527 end
527 528
528 | L'.CApp (c, _) => 529 | L'.CApp (c, _) =>
529 (case #1 (hnormKind (kindof env c)) of 530 (case hnormKind (kindof env c) of
530 L'.KArrow (_, k) => k 531 (L'.KArrow (_, k), _) => k
531 | L'.KError => kerror 532 | (L'.KError, _) => kerror
532 | _ => raise CUnify' (CKindof c)) 533 | k => raise CUnify' (CKindof (k, c)))
533 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc) 534 | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
534 | L'.CDisjoint (_, _, c) => kindof env c 535 | L'.CDisjoint (_, _, c) => kindof env c
535 536
536 | L'.CName _ => kname 537 | L'.CName _ => kname
537 538
549 fun unifyRecordCons (env, denv) (c1, c2) = 550 fun unifyRecordCons (env, denv) (c1, c2) =
550 let 551 let
551 fun rkindof c = 552 fun rkindof c =
552 case kindof env c of 553 case kindof env c of
553 (L'.KRecord k, _) => k 554 (L'.KRecord k, _) => k
554 | _ => raise CUnify' (CKindof c) 555 | (L'.KError, _) => kerror
556 | k => raise CUnify' (CKindof (k, c))
555 557
556 val k1 = rkindof c1 558 val k1 = rkindof c1
557 val k2 = rkindof c2 559 val k2 = rkindof c2
558 560
559 val (r1, gs1) = recordSummary (env, denv) c1 561 val (r1, gs1) = recordSummary (env, denv) c1
641 ([], [], _) => ([], [], unifs) 643 ([], [], _) => ([], [], unifs)
642 | (_, _, []) => (fs, others, []) 644 | (_, _, []) => (fs, others, [])
643 | (_, _, (_, r) :: rest) => 645 | (_, _, (_, r) :: rest) =>
644 let 646 let
645 val r' = ref NONE 647 val r' = ref NONE
646 val cr' = (L'.CUnif (dummy, k, "recd", r'), dummy) 648 val kr = (L'.KRecord k, dummy)
649 val cr' = (L'.CUnif (dummy, kr, "recd", r'), dummy)
647 650
648 val prefix = case (fs, others) of 651 val prefix = case (fs, others) of
649 ([], other :: others) => 652 ([], other :: others) =>
650 List.foldl (fn (other, c) => 653 List.foldl (fn (other, c) =>
651 (L'.CConcat (c, other), dummy)) 654 (L'.CConcat (c, other), dummy))