Mercurial > urweb
comparison src/elab_env.sml @ 563:44958d74c43f
Initial conversion to arbitrary-kind classes
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Fri, 19 Dec 2008 10:03:31 -0500 |
parents | aceb2d982f8f |
children | 588b9d16b00a |
comparison
equal
deleted
inserted
replaced
562:6daa59a55c43 | 563:44958d74c43f |
---|---|
602 | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x)) | 602 | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x)) |
603 | SgiVal _ => (sgns, strs, cons) | 603 | SgiVal _ => (sgns, strs, cons) |
604 | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons) | 604 | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons) |
605 | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons) | 605 | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons) |
606 | SgiConstraint _ => (sgns, strs, cons) | 606 | SgiConstraint _ => (sgns, strs, cons) |
607 | SgiClassAbs (x, n) => (sgns, strs, IM.insert (cons, n, x)) | 607 | SgiClassAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x)) |
608 | SgiClass (x, n, _) => (sgns, strs, IM.insert (cons, n, x)) | 608 | SgiClass (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x)) |
609 | 609 |
610 fun sgnSeek f sgis = | 610 fun sgnSeek f sgis = |
611 let | 611 let |
612 fun seek (sgis, sgns, strs, cons) = | 612 fun seek (sgis, sgns, strs, cons) = |
613 case sgis of | 613 case sgis of |
786 (classes, | 786 (classes, |
787 newClasses, | 787 newClasses, |
788 fmap, | 788 fmap, |
789 pushSgnNamedAs env x n sgn) | 789 pushSgnNamedAs env x n sgn) |
790 | 790 |
791 | SgiClassAbs xn => found xn | 791 | SgiClassAbs (x, n, _) => found (x, n) |
792 | SgiClass (x, n, _) => found (x, n) | 792 | SgiClass (x, n, _, _) => found (x, n) |
793 | SgiVal (x, n, (CApp (f, a), _)) => | 793 | SgiVal (x, n, (CApp (f, a), _)) => |
794 let | 794 let |
795 fun unravel c = | 795 fun unravel c = |
796 case #1 c of | 796 case #1 c of |
797 CUnif (_, _, _, ref (SOME c)) => unravel c | 797 CUnif (_, _, _, ref (SOME c)) => unravel c |
944 | SgiVal (x, n, t) => pushENamedAs env x n t | 944 | SgiVal (x, n, t) => pushENamedAs env x n t |
945 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn | 945 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn |
946 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn | 946 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn |
947 | SgiConstraint _ => env | 947 | SgiConstraint _ => env |
948 | 948 |
949 | SgiClassAbs (x, n) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) NONE | 949 | SgiClassAbs (x, n, k) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) NONE |
950 | SgiClass (x, n, c) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) (SOME c) | 950 | SgiClass (x, n, k, c) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) (SOME c) |
951 | 951 |
952 fun sgnSubCon x = | 952 fun sgnSubCon x = |
953 ElabUtil.Con.map {kind = id, | 953 ElabUtil.Con.map {kind = id, |
954 con = sgnS_con x} | 954 con = sgnS_con x} |
955 | 955 |
996 in | 996 in |
997 SOME (k', SOME (CModProj (m1, ms, x'), #2 sgn)) | 997 SOME (k', SOME (CModProj (m1, ms, x'), #2 sgn)) |
998 end | 998 end |
999 else | 999 else |
1000 NONE | 1000 NONE |
1001 | SgiClassAbs (x, _) => if x = field then | 1001 | SgiClassAbs (x, _, k) => if x = field then |
1002 SOME ((KArrow ((KType, #2 sgn), (KType, #2 sgn)), #2 sgn), NONE) | 1002 SOME ((KArrow (k, (KType, #2 sgn)), #2 sgn), NONE) |
1003 else | 1003 else |
1004 NONE | 1004 NONE |
1005 | SgiClass (x, _, c) => if x = field then | 1005 | SgiClass (x, _, k, c) => if x = field then |
1006 SOME ((KArrow ((KType, #2 sgn), (KType, #2 sgn)), #2 sgn), SOME c) | 1006 SOME ((KArrow (k, (KType, #2 sgn)), #2 sgn), SOME c) |
1007 else | 1007 else |
1008 NONE | 1008 NONE |
1009 | _ => NONE) sgis of | 1009 | _ => NONE) sgis of |
1010 NONE => NONE | 1010 NONE => NONE |
1011 | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co)) | 1011 | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co)) |
1012 | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan)) | 1012 | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan)) |
1013 | _ => NONE | 1013 | _ => NONE |
1099 | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) | 1099 | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) |
1100 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) | 1100 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) |
1101 | SgiVal _ => seek (sgis, sgns, strs, cons, acc) | 1101 | SgiVal _ => seek (sgis, sgns, strs, cons, acc) |
1102 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) | 1102 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) |
1103 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) | 1103 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) |
1104 | SgiClassAbs (x, n) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) | 1104 | SgiClassAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) |
1105 | SgiClass (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) | 1105 | SgiClass (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) |
1106 in | 1106 in |
1107 seek (sgis, IM.empty, IM.empty, IM.empty, []) | 1107 seek (sgis, IM.empty, IM.empty, IM.empty, []) |
1108 end | 1108 end |
1109 | 1109 |
1110 fun projectConstraints env {sgn, str} = | 1110 fun projectConstraints env {sgn, str} = |
1187 let | 1187 let |
1188 val t = (CModProj (tn, [], "sql_sequence"), loc) | 1188 val t = (CModProj (tn, [], "sql_sequence"), loc) |
1189 in | 1189 in |
1190 pushENamedAs env x n t | 1190 pushENamedAs env x n t |
1191 end | 1191 end |
1192 | DClass (x, n, c) => | 1192 | DClass (x, n, k, c) => |
1193 let | 1193 let |
1194 val k = (KArrow ((KType, loc), (KType, loc)), loc) | 1194 val k = (KArrow (k, (KType, loc)), loc) |
1195 val env = pushCNamedAs env x n k (SOME c) | 1195 val env = pushCNamedAs env x n k (SOME c) |
1196 in | 1196 in |
1197 pushClass env n | 1197 pushClass env n |
1198 end | 1198 end |
1199 | DDatabase _ => env | 1199 | DDatabase _ => env |