Mercurial > urweb

comparison src/elaborate.sml @ 14:f1c36df29ed7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Primitive type constants
author Adam Chlipala <adamc@hcoop.net>
date Sun, 08 Jun 2008 12:27:08 -0400
parents 6049e2193bf2
children 1e645beb3f3b
comparison
equal deleted inserted replaced
13:6049e2193bf2 14:f1c36df29ed7
25 * POSSIBILITY OF SUCH DAMAGE. 25 * POSSIBILITY OF SUCH DAMAGE.
26 *) 26 *)
27 27
28 structure Elaborate :> ELABORATE = struct 28 structure Elaborate :> ELABORATE = struct
29 29
30 structure P = Prim
30 structure L = Source 31 structure L = Source
31 structure L' = Elab 32 structure L' = Elab
32 structure E = ElabEnv 33 structure E = ElabEnv
33 structure U = ElabUtil 34 structure U = ElabUtil
34 35
438 true) 439 true)
439 handle CUnify _ => false 440 handle CUnify _ => false
440 441
441 and unifySummaries env (k, s1 : record_summary, s2 : record_summary) = 442 and unifySummaries env (k, s1 : record_summary, s2 : record_summary) =
442 let 443 let
443 val () = eprefaces "Summaries" [("#1", p_summary env s1), 444 (*val () = eprefaces "Summaries" [("#1", p_summary env s1),
444 ("#2", p_summary env s2)] 445 ("#2", p_summary env s2)]*)
445 446
446 fun eatMatching p (ls1, ls2) = 447 fun eatMatching p (ls1, ls2) =
447 let 448 let
448 fun em (ls1, ls2, passed1) = 449 fun em (ls1, ls2, passed1) =
449 case ls1 of 450 case ls1 of
469 if consEq env (x1, x2) then 470 if consEq env (x1, x2) then
470 (unifyCons env c1 c2; 471 (unifyCons env c1 c2;
471 true) 472 true)
472 else 473 else
473 false) (#fields s1, #fields s2) 474 false) (#fields s1, #fields s2)
474 val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}), 475 (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
475 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})] 476 ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*)
476 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2) 477 val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
477 val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2) 478 val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2)
478 479
479 fun unifFields (fs, others, unifs) = 480 fun unifFields (fs, others, unifs) =
480 case (fs, others, unifs) of 481 case (fs, others, unifs) of
663 fun checkCon env e c1 c2 = 664 fun checkCon env e c1 c2 =
664 unifyCons env c1 c2 665 unifyCons env c1 c2
665 handle CUnify (c1, c2, err) => 666 handle CUnify (c1, c2, err) =>
666 expError env (Unify (e, c1, c2, err)) 667 expError env (Unify (e, c1, c2, err))
667 668
669 fun primType env p =
670 let
671 val s = case p of
672 P.Int _ => "int"
673 | P.Float _ => "float"
674 | P.String _ => "string"
675 in
676 case E.lookupC env s of
677 E.NotBound => raise Fail ("Primitive type " ^ s ^ " unbound")
678 | E.Rel _ => raise Fail ("Primitive type " ^ s ^ " bound as relative")
679 | E.Named (n, (L'.KType, _)) => L'.CNamed n
680 | E.Named _ => raise Fail ("Primitive type " ^ s ^ " bound at non-Type kind")
681 end
682
668 fun elabExp env (e, loc) = 683 fun elabExp env (e, loc) =
669 case e of 684 case e of
670 L.EAnnot (e, t) => 685 L.EAnnot (e, t) =>
671 let 686 let
672 val (e', et) = elabExp env e 687 val (e', et) = elabExp env e
674 in 689 in
675 checkCon env e' et t'; 690 checkCon env e' et t';
676 (e', t') 691 (e', t')
677 end 692 end
678 693
694 | L.EPrim p => ((L'.EPrim p, loc), (primType env p, loc))
679 | L.EVar s => 695 | L.EVar s =>
680 (case E.lookupE env s of 696 (case E.lookupE env s of
681 E.NotBound => 697 E.NotBound =>
682 (expError env (UnboundExp (loc, s)); 698 (expError env (UnboundExp (loc, s));
683 (eerror, cerror)) 699 (eerror, cerror))