diff src/elab_env.sml @ 218:a3413288cce1

Signature ascription for type classes
author Adam Chlipala <adamc@hcoop.net>
date Sat, 16 Aug 2008 16:57:21 -0400
parents 56db662ebcfd
children 19e5791923d0
line wrap: on
line diff
--- a/src/elab_env.sml	Sat Aug 16 16:30:07 2008 -0400
+++ b/src/elab_env.sml	Sat Aug 16 16:57:21 2008 -0400
@@ -700,23 +700,31 @@
     case #1 (hnormSgn env sgn) of
         SgnConst sgis =>
         let
-            val (classes, _, _) =
-                foldl (fn (sgi, (classes, newClasses, fmap)) =>
+            val (classes, _, _, _) =
+                foldl (fn (sgi, (classes, newClasses, fmap, env)) =>
                           let
                               fun found (x, n) =
                                   (CM.insert (classes,
                                               ClProj (m1, ms, x),
                                               empty_class),
                                    IM.insert (newClasses, n, x),
-                                   sgiSeek (#1 sgi, fmap))
+                                   sgiSeek (#1 sgi, fmap),
+                                   env)
 
-                              fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap))
+                              fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap), env)
                           in
                               case #1 sgi of
                                   SgiStr (x, _, sgn) =>
                                   (enrichClasses env classes (m1, ms @ [x]) sgn,
                                    newClasses,
-                                   sgiSeek (#1 sgi, fmap))
+                                   sgiSeek (#1 sgi, fmap),
+                                   env)
+                                | SgiSgn (x, n, sgn) =>
+                                  (classes,
+                                   newClasses,
+                                   fmap,
+                                   pushSgnNamedAs env x n sgn)
+
                                 | SgiClassAbs xn => found xn
                                 | SgiClass (x, n, _) => found (x, n)
                                 | SgiVal (x, n, (CApp ((CNamed f, _), a), _)) =>
@@ -737,12 +745,13 @@
                                            in
                                                (CM.insert (classes, cn, class),
                                                 newClasses,
-                                                fmap)
+                                                fmap,
+                                                env)
                                            end)
                                 | SgiVal _ => default ()
                                 | _ => default ()
                           end)
-                (classes, IM.empty, (IM.empty, IM.empty, IM.empty)) sgis
+                      (classes, IM.empty, (IM.empty, IM.empty, IM.empty), env) sgis
         in
             classes
         end