Mercurial > urweb

comparison src/elab_env.sml @ 459:f542bc3133dc

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