diff options
| author |  Benjamin Barenblat <bbaren@mit.edu> | 2015-11-22 10:39:36 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@mit.edu> | 2015-11-22 10:39:36 -0500 |
| commit | bf037ce78c2c76a34ecca0fb8bafa5d5be38968a (patch) | |
| tree | 3e91b0d0e8e0fb704c7df444283b6c8c63351f95 /src/elab_env.sml | |
| parent | 7d861ea0debf944cb8e3e38d73a8c0197de574b3 (diff) | |
| parent | 638e838a81e1ccc6594fda1920df441eb21577ae (diff) | |
Merge branch 'upstream' into dfsg_clean20151122+dfsg
Diffstat (limited to 'src/elab_env.sml')
| -rw-r--r-- | src/elab_env.sml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml index 9fbe7bd7..9c9cd14f 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -990,7 +990,7 @@ fun sgiSeek (sgi, (sgns, strs, cons)) = | SgiDatatypeImp (x, n, _, _, _, _, _) => (sgns, strs, IM.insert (cons, n, x)) | SgiVal _ => (sgns, strs, cons) | SgiSgn (x, n, _) => (IM.insert (sgns, n, x), strs, cons) - | SgiStr (x, n, _) => (sgns, IM.insert (strs, n, x), cons) + | SgiStr (_, x, n, _) => (sgns, IM.insert (strs, n, x), cons) | SgiConstraint _ => (sgns, strs, cons) | SgiClassAbs (x, n, _) => (sgns, strs, IM.insert (cons, n, x)) | SgiClass (x, n, _, _) => (sgns, strs, IM.insert (cons, n, x)) @@ -1143,13 +1143,13 @@ and hnormSgn env (all as (sgn, loc)) = else traverse (ms, sgi :: pre, rest) - | (sgi as (SgiStr (x', n, sgn'), loc)) :: rest => + | (sgi as (SgiStr (im, 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, + (SgiStr (im, x', n, rewrite (sgn', ms')), loc) :: rest) else traverse (ms, sgi :: pre, rest)) @@ -1186,7 +1186,7 @@ fun enrichClasses env classes (m1, ms) sgn = fun default () = (classes, newClasses, sgiSeek (#1 sgi, fmap), env) in case #1 sgi of - SgiStr (x, _, sgn) => + SgiStr (Import, x, _, sgn) => let val str = manifest (m1, ms, #2 sgi) val sgn' = sgnSubSgn (str, fmap) sgn @@ -1360,7 +1360,7 @@ fun sgiBinds env (sgi, loc) = env xncs end | SgiVal (x, n, t) => pushENamedAs env x n t - | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn + | SgiStr (_, x, n, sgn) => pushStrNamedAs env x n sgn | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn | SgiConstraint _ => env @@ -1374,7 +1374,7 @@ fun sgnSubCon x = fun projectStr env {sgn, str, field} = case #1 (hnormSgn env sgn) of SgnConst sgis => - (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of + (case sgnSeek (fn SgiStr (_, x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of NONE => NONE | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) | SgnError => SOME (SgnError, ErrorMsg.dummySpan) @@ -1544,7 +1544,7 @@ fun sgnSeekConstraints (str, sgis) = | SgiDatatypeImp (x, n, _, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) | SgiVal _ => seek (sgis, sgns, strs, cons, acc) | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) - | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) + | SgiStr (_, x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), 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) in |