Mercurial > urweb

comparison src/elab_env.sml @ 563:44958d74c43f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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