Mercurial > urweb
comparison src/elab_env.sml @ 459:f542bc3133dc
Cookies through elaborate
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Thu, 06 Nov 2008 10:29:55 -0500 |
parents | 222cbc1da232 |
children | d34834af4512 |
comparison
equal
deleted
inserted
replaced
458:8f65b0fa3b29 | 459:f542bc3133dc |
---|---|
590 | SgiConstraint _ => (sgns, strs, cons) | 590 | SgiConstraint _ => (sgns, strs, cons) |
591 | SgiTable _ => (sgns, strs, cons) | 591 | SgiTable _ => (sgns, strs, cons) |
592 | SgiSequence _ => (sgns, strs, cons) | 592 | SgiSequence _ => (sgns, strs, cons) |
593 | SgiClassAbs (x, n) => (sgns, strs, IM.insert (cons, n, x)) | 593 | SgiClassAbs (x, n) => (sgns, strs, IM.insert (cons, n, x)) |
594 | SgiClass (x, n, _) => (sgns, strs, IM.insert (cons, n, x)) | 594 | SgiClass (x, n, _) => (sgns, strs, IM.insert (cons, n, x)) |
595 | SgiCookie _ => (sgns, strs, cons) | |
595 | 596 |
596 fun sgnSeek f sgis = | 597 fun sgnSeek f sgis = |
597 let | 598 let |
598 fun seek (sgis, sgns, strs, cons) = | 599 fun seek (sgis, sgns, strs, cons) = |
599 case sgis of | 600 case sgis of |
943 pushENamedAs env x n t | 944 pushENamedAs env x n t |
944 end | 945 end |
945 | 946 |
946 | SgiClassAbs (x, n) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) NONE | 947 | SgiClassAbs (x, n) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) NONE |
947 | SgiClass (x, n, c) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) (SOME c) | 948 | 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 | |
948 | 956 |
949 | 957 |
950 fun sgnSubCon x = | 958 fun sgnSubCon x = |
951 ElabUtil.Con.map {kind = id, | 959 ElabUtil.Con.map {kind = id, |
952 con = sgnS_con x} | 960 con = sgnS_con x} |
1093 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) | 1101 | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) |
1094 | SgiTable _ => seek (sgis, sgns, strs, cons, acc) | 1102 | SgiTable _ => seek (sgis, sgns, strs, cons, acc) |
1095 | SgiSequence _ => seek (sgis, sgns, strs, cons, acc) | 1103 | SgiSequence _ => seek (sgis, sgns, strs, cons, acc) |
1096 | 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) |
1097 | 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 | SgiCookie _ => seek (sgis, sgns, strs, cons, acc) | |
1098 in | 1107 in |
1099 seek (sgis, IM.empty, IM.empty, IM.empty, []) | 1108 seek (sgis, IM.empty, IM.empty, IM.empty, []) |
1100 end | 1109 end |
1101 | 1110 |
1102 fun projectConstraints env {sgn, str} = | 1111 fun projectConstraints env {sgn, str} = |
1187 val env = pushCNamedAs env x n k (SOME c) | 1196 val env = pushCNamedAs env x n k (SOME c) |
1188 in | 1197 in |
1189 pushClass env n | 1198 pushClass env n |
1190 end | 1199 end |
1191 | DDatabase _ => env | 1200 | DDatabase _ => env |
1201 | DCookie (tn, x, n, c) => | |
1202 let | |
1203 val t = (CApp ((CModProj (tn, [], "cookie"), loc), c), loc) | |
1204 in | |
1205 pushENamedAs env x n t | |
1206 end | |
1192 | 1207 |
1193 fun patBinds env (p, loc) = | 1208 fun patBinds env (p, loc) = |
1194 case p of | 1209 case p of |
1195 PWild => env | 1210 PWild => env |
1196 | PVar (x, t) => pushERel env x t | 1211 | PVar (x, t) => pushERel env x t |