Mercurial > urweb

comparison src/elab_env.sml @ 460:d34834af4512

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Cookies through explify
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Nov 2008 10:43:48 -0500
parents f542bc3133dc
children 3f1b9231a37b
comparison
equal deleted inserted replaced
459:f542bc3133dc 460:d34834af4512
586 | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x)) 586 | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x))
587 | SgiVal _ => (sgns, strs, cons) 587 | SgiVal _ => (sgns, strs, cons)
588 | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons) 588 | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons)
589 | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons) 589 | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons)
590 | SgiConstraint _ => (sgns, strs, cons) 590 | SgiConstraint _ => (sgns, strs, cons)
591 | SgiTable _ => (sgns, strs, cons)
592 | SgiSequence _ => (sgns, strs, cons)
593 | SgiClassAbs (x, n) => (sgns, strs, IM.insert (cons, n, x)) 591 | SgiClassAbs (x, n) => (sgns, strs, IM.insert (cons, n, x))
594 | SgiClass (x, n, _) => (sgns, strs, IM.insert (cons, n, x)) 592 | SgiClass (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
595 | SgiCookie _ => (sgns, strs, cons)
596 593
597 fun sgnSeek f sgis = 594 fun sgnSeek f sgis =
598 let 595 let
599 fun seek (sgis, sgns, strs, cons) = 596 fun seek (sgis, sgns, strs, cons) =
600 case sgis of 597 case sgis of
929 | SgiVal (x, n, t) => pushENamedAs env x n t 926 | SgiVal (x, n, t) => pushENamedAs env x n t
930 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn 927 | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
931 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn 928 | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn
932 | SgiConstraint _ => env 929 | SgiConstraint _ => env
933 930
934 | SgiTable (tn, x, n, c) =>
935 let
936 val t = (CApp ((CModProj (tn, [], "sql_table"), loc), c), loc)
937 in
938 pushENamedAs env x n t
939 end
940 | SgiSequence (tn, x, n) =>
941 let
942 val t = (CModProj (tn, [], "sql_sequence"), loc)
943 in
944 pushENamedAs env x n t
945 end
946
947 | SgiClassAbs (x, n) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) NONE 931 | SgiClassAbs (x, n) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) NONE
948 | SgiClass (x, n, c) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) (SOME c) 932 | SgiClass (x, n, c) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) (SOME c)
949
950 | SgiCookie (tn, x, n, c) =>
951 let
952 val t = (CApp ((CModProj (tn, [], "http_cookie"), loc), c), loc)
953 in
954 pushENamedAs env x n t
955 end
956
957 933
958 fun sgnSubCon x = 934 fun sgnSubCon x =
959 ElabUtil.Con.map {kind = id, 935 ElabUtil.Con.map {kind = id,
960 con = sgnS_con x} 936 con = sgnS_con x}
961 937
1097 | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 1073 | SgiDatatype (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
1098 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 1074 | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
1099 | SgiVal _ => seek (sgis, sgns, strs, cons, acc) 1075 | SgiVal _ => seek (sgis, sgns, strs, cons, acc)
1100 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) 1076 | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc)
1101 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) 1077 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc)
1102 | SgiTable _ => seek (sgis, sgns, strs, cons, acc)
1103 | SgiSequence _ => seek (sgis, sgns, strs, cons, acc)
1104 | SgiClassAbs (x, n) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) 1078 | 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) 1079 | SgiClass (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
1106 | SgiCookie _ => seek (sgis, sgns, strs, cons, acc)
1107 in 1080 in
1108 seek (sgis, IM.empty, IM.empty, IM.empty, []) 1081 seek (sgis, IM.empty, IM.empty, IM.empty, [])
1109 end 1082 end
1110 1083
1111 fun projectConstraints env {sgn, str} = 1084 fun projectConstraints env {sgn, str} =