diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-08-16 16:57:21 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-08-16 16:57:21 -0400 |
| commit | 7910af6db28602b2fb5d3c9c5227bcc3c076acdc (patch) | |
| tree | c204f7a2b75e936a7d0dcfdd76693a1ce1a56daa /src/elab_env.sml | |
| parent | 2c64a768d33ed6cbead84259a5cefae7d9c6f4e1 (diff) | |
Signature ascription for type classes
Diffstat (limited to 'src/elab_env.sml')
| -rw-r--r-- | src/elab_env.sml | 23 |
1 files changed, 16 insertions, 7 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml index 392fcf02..49eb1d86 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -700,23 +700,31 @@ fun enrichClasses env classes (m1, ms) sgn = 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 @@ fun enrichClasses env classes (m1, ms) sgn = 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 |