diff options
author | Adam Chlipala <adam@chlipala.net> | 2013-08-19 12:25:32 -0400 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2013-08-19 12:25:32 -0400 |
commit | bcaa5ca71b45500fa2df7ca1d19202fe7807ab36 (patch) | |
tree | b7581cc191267590b2ee407d91161bd2950e3604 /src/elab_env.sml | |
parent | 9734b34421533a3a70a09629b11d7e2105ef4a1a (diff) |
Allow [where con] to descend within submodule structure; open submodule constraints while checking later signature items
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r-- | src/elab_env.sml | 58 |
1 files changed, 38 insertions, 20 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml index 5d684817..465fb7e4 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -1126,26 +1126,44 @@ and hnormSgn env (all as (sgn, loc)) = NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed" | SOME sgn => hnormSgn env sgn end - | SgnWhere (sgn, x, c) => - case #1 (hnormSgn env sgn) of - SgnError => (SgnError, loc) - | SgnConst sgis => - let - fun traverse (pre, post) = - case post of - [] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]" - | (sgi as (SgiConAbs (x', n, k), loc)) :: rest => - if x = x' then - List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest) - else - traverse (sgi :: pre, rest) - | sgi :: rest => traverse (sgi :: pre, rest) - - val sgis = traverse ([], sgis) - in - (SgnConst sgis, loc) - end - | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]" + | SgnWhere (sgn, ms, x, c) => + let + fun rewrite (sgn, ms) = + case #1 (hnormSgn env sgn) of + SgnError => (SgnError, loc) + | SgnConst sgis => + let + fun traverse (ms, pre, post) = + case post of + [] => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [1]" + + | (sgi as (SgiConAbs (x', n, k), loc)) :: rest => + if List.null ms andalso x = x' then + List.revAppend (pre, (SgiCon (x', n, k, c), loc) :: rest) + else + traverse (ms, sgi :: pre, rest) + + | (sgi as (SgiStr (x', n, sgn'), loc)) :: rest => + (case ms of + [] => traverse (ms, sgi :: pre, rest) + | x :: ms' => + if x = x' then + List.revAppend (pre, + (SgiStr (x', n, + rewrite (sgn', ms')), loc) :: rest) + else + traverse (ms, sgi :: pre, rest)) + + | sgi :: rest => traverse (ms, sgi :: pre, rest) + + val sgis = traverse (ms, [], sgis) + in + (SgnConst sgis, loc) + end + | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]" + in + rewrite (sgn, ms) + end fun manifest (m, ms, loc) = foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms |