summaryrefslogtreecommitdiff
path: root/src/elab_env.sml
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2015-11-22 10:39:36 -0500
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2015-11-22 10:39:36 -0500
commitbf037ce78c2c76a34ecca0fb8bafa5d5be38968a (patch)
tree3e91b0d0e8e0fb704c7df444283b6c8c63351f95 /src/elab_env.sml
parent7d861ea0debf944cb8e3e38d73a8c0197de574b3 (diff)
parent638e838a81e1ccc6594fda1920df441eb21577ae (diff)
Merge branch 'upstream' into dfsg_clean20151122+dfsg
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r--src/elab_env.sml14
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