diff 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
line wrap: on
line diff
--- a/src/elab_env.sml	Thu Nov 06 10:04:03 2008 -0500
+++ b/src/elab_env.sml	Thu Nov 06 10:29:55 2008 -0500
@@ -592,6 +592,7 @@
       | SgiSequence _ => (sgns, strs, cons)
       | SgiClassAbs (x, n) => (sgns, strs, IM.insert (cons, n, x))
       | SgiClass (x, n, _) => (sgns, strs, IM.insert (cons, n, x))
+      | SgiCookie _ => (sgns, strs, cons)
 
 fun sgnSeek f sgis =
     let
@@ -945,6 +946,13 @@
 
       | SgiClassAbs (x, n) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) NONE
       | SgiClass (x, n, c) => pushCNamedAs env x n (KArrow ((KType, loc), (KType, loc)), loc) (SOME c)
+
+      | SgiCookie (tn, x, n, c) =>
+        let
+            val t = (CApp ((CModProj (tn, [], "http_cookie"), loc), c), loc)
+        in
+            pushENamedAs env x n t
+        end
         
 
 fun sgnSubCon x =
@@ -1095,6 +1103,7 @@
                   | SgiSequence _ => seek (sgis, sgns, strs, cons, acc)
                   | SgiClassAbs (x, n) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
                   | SgiClass (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc)
+                  | SgiCookie _ => seek (sgis, sgns, strs, cons, acc)
     in
         seek (sgis, IM.empty, IM.empty, IM.empty, [])
     end
@@ -1189,6 +1198,12 @@
             pushClass env n
         end
       | DDatabase _ => env
+      | DCookie (tn, x, n, c) =>
+        let
+            val t = (CApp ((CModProj (tn, [], "cookie"), loc), c), loc)
+        in
+            pushENamedAs env x n t
+        end
 
 fun patBinds env (p, loc) =
     case p of