Mercurial > urweb

comparison src/elaborate.sml @ 56:d3cc191cb25f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Separate compilation and automatic basis importation
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Jun 2008 14:23:05 -0400
parents 0a5c312de09a
children fd8a81ecd598
comparison
equal deleted inserted replaced
55:5c97b7cd912b 56:d3cc191cb25f
139 val kerror = (L'.KError, dummy) 139 val kerror = (L'.KError, dummy)
140 val eerror = (L'.EError, dummy) 140 val eerror = (L'.EError, dummy)
141 val sgnerror = (L'.SgnError, dummy) 141 val sgnerror = (L'.SgnError, dummy)
142 val strerror = (L'.StrError, dummy) 142 val strerror = (L'.StrError, dummy)
143 143
144 val int = ref cerror
145 val float = ref cerror
146 val string = ref cerror
147
144 local 148 local
145 val count = ref 0 149 val count = ref 0
146 in 150 in
147 151
148 fun resetKunif () = count := 0 152 fun resetKunif () = count := 0
748 unifyCons env c1 c2 752 unifyCons env c1 c2
749 handle CUnify (c1, c2, err) => 753 handle CUnify (c1, c2, err) =>
750 expError env (Unify (e, c1, c2, err)) 754 expError env (Unify (e, c1, c2, err))
751 755
752 fun primType env p = 756 fun primType env p =
753 let 757 case p of
754 val s = case p of 758 P.Int _ => !int
755 P.Int _ => "int" 759 | P.Float _ => !float
756 | P.Float _ => "float" 760 | P.String _ => !string
757 | P.String _ => "string"
758 in
759 case E.lookupC env s of
760 E.NotBound => raise Fail ("Primitive type " ^ s ^ " unbound")
761 | E.Rel _ => raise Fail ("Primitive type " ^ s ^ " bound as relative")
762 | E.Named (n, (L'.KType, _)) => L'.CNamed n
763 | E.Named _ => raise Fail ("Primitive type " ^ s ^ " bound at non-Type kind")
764 end
765 761
766 fun typeof env (e, loc) = 762 fun typeof env (e, loc) =
767 case e of 763 case e of
768 L'.EPrim p => (primType env p, loc) 764 L'.EPrim p => primType env p
769 | L'.ERel n => #2 (E.lookupERel env n) 765 | L'.ERel n => #2 (E.lookupERel env n)
770 | L'.ENamed n => #2 (E.lookupENamed env n) 766 | L'.ENamed n => #2 (E.lookupENamed env n)
771 | L'.EModProj (n, ms, x) => 767 | L'.EModProj (n, ms, x) =>
772 let 768 let
773 val (_, sgn) = E.lookupStrNamed env n 769 val (_, sgn) = E.lookupStrNamed env n
823 in 819 in
824 checkCon env e' et t'; 820 checkCon env e' et t';
825 (e', t') 821 (e', t')
826 end 822 end
827 823
828 | L.EPrim p => ((L'.EPrim p, loc), (primType env p, loc)) 824 | L.EPrim p => ((L'.EPrim p, loc), primType env p)
829 | L.EVar ([], s) => 825 | L.EVar ([], s) =>
830 (case E.lookupE env s of 826 (case E.lookupE env s of
831 E.NotBound => 827 E.NotBound =>
832 (expError env (UnboundExp (loc, s)); 828 (expError env (UnboundExp (loc, s));
833 (eerror, cerror)) 829 (eerror, cerror))
1476 | _ => raise Fail "Unable to hnormSgn in functor application") 1472 | _ => raise Fail "Unable to hnormSgn in functor application")
1477 | _ => (strError env (NotFunctor sgn1); 1473 | _ => (strError env (NotFunctor sgn1);
1478 (strerror, sgnerror)) 1474 (strerror, sgnerror))
1479 end 1475 end
1480 1476
1481 val elabFile = ListUtil.foldlMap elabDecl 1477 fun elabFile basis env file =
1478 let
1479 val sgn = elabSgn env (L.SgnConst basis, ErrorMsg.dummySpan)
1480 val (env', basis_n) = E.pushStrNamed env "Basis" sgn
1481
1482 val (ds, env') =
1483 case #1 (hnormSgn env' sgn) of
1484 L'.SgnConst sgis =>
1485 ListUtil.foldlMap (fn ((sgi, loc), env') =>
1486 case sgi of
1487 L'.SgiConAbs (x, n, k) =>
1488 ((L'.DCon (x, n, k, (L'.CModProj (basis_n, [], x), loc)), loc),
1489 E.pushCNamedAs env' x n k NONE)
1490 | L'.SgiCon (x, n, k, c) =>
1491 ((L'.DCon (x, n, k, (L'.CModProj (basis_n, [], x), loc)), loc),
1492 E.pushCNamedAs env' x n k (SOME c))
1493 | L'.SgiVal (x, n, t) =>
1494 ((L'.DVal (x, n, t, (L'.EModProj (basis_n, [], x), loc)), loc),
1495 E.pushENamedAs env' x n t)
1496 | L'.SgiStr (x, n, sgn) =>
1497 ((L'.DStr (x, n, sgn, (L'.StrProj ((L'.StrVar basis_n, loc), x), loc)), loc),
1498 E.pushStrNamedAs env' x n sgn))
1499 env' sgis
1500 | _ => raise Fail "Non-constant Basis signature"
1501
1502 fun discoverC r x =
1503 case E.lookupC env' x of
1504 E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis")
1505 | E.Rel _ => raise Fail ("Constructor " ^ x ^ " bound relatively in Basis")
1506 | E.Named (n, (_, loc)) => r := (L'.CNamed n, loc)
1507
1508 val () = discoverC int "int"
1509 val () = discoverC float "float"
1510 val () = discoverC string "string"
1511
1512 val (file, _) = ListUtil.foldlMap elabDecl env' file
1513 in
1514 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
1515 end
1482 1516
1483 end 1517 end