summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-19 16:35:40 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-19 16:35:40 -0400
commite542e7ba2106c5763006e88d90b6834fe9221b85 (patch)
treebf572cb1c2dfec0751f72a61fcfe0a9fd563c933 /src/elaborate.sml
parent7a1c5e1780fd3c56d9c591821905bb3b3bbfa50a (diff)
Elaborating 'where'
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml39
1 files changed, 29 insertions, 10 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 10fa3898..9c96060d 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -239,7 +239,7 @@ fun elabCon env (c, loc) =
((L'.CNamed n, loc), k))
| L.CVar (m1 :: ms, s) =>
(case E.lookupStr env m1 of
- NONE => (conError env (UnboundStrInCon (loc, s));
+ NONE => (conError env (UnboundStrInCon (loc, m1));
(cerror, kerror))
| SOME (n, sgn) =>
let
@@ -824,7 +824,7 @@ fun elabExp env (e, loc) =
| E.Named (n, t) => ((L'.ENamed n, loc), t))
| L.EVar (m1 :: ms, s) =>
(case E.lookupStr env m1 of
- NONE => (expError env (UnboundStrInExp (loc, s));
+ NONE => (expError env (UnboundStrInExp (loc, m1));
(eerror, cerror))
| SOME (n, sgn) =>
let
@@ -969,6 +969,7 @@ datatype sgn_error =
| SgiWrongKind of L'.sgn_item * L'.kind * L'.sgn_item * L'.kind * kunify_error
| SgiWrongCon of L'.sgn_item * L'.con * L'.sgn_item * L'.con * cunify_error
| SgnWrongForm of L'.sgn * L'.sgn
+ | UnWhereable of L'.sgn * string
fun sgnError env err =
case err of
@@ -995,6 +996,10 @@ fun sgnError env err =
(ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:";
eprefaces' [("Sig 1", p_sgn env sgn1),
("Sig 2", p_sgn env sgn2)])
+ | UnWhereable (sgn, x) =>
+ (ErrorMsg.errorAt (#2 sgn) "Unavailable field for 'where'";
+ eprefaces' [("Signature", p_sgn env sgn),
+ ("Field", PD.string x)])
datatype str_error =
UnboundStr of ErrorMsg.span * string
@@ -1004,6 +1009,7 @@ fun strError env err =
UnboundStr (loc, s) =>
ErrorMsg.errorAt loc ("Unbound structure variable " ^ s)
+val hnormSgn = E.hnormSgn
fun elabSgn_item ((sgi, loc), env) =
let
@@ -1110,6 +1116,25 @@ and elabSgn env (sgn, loc) =
in
(L'.SgnFun (m, n, dom', ran'), loc)
end
+ | L.SgnWhere (sgn, x, c) =>
+ let
+ val sgn' = elabSgn env sgn
+ val (c', ck) = elabCon env c
+ in
+ case #1 (hnormSgn env sgn') of
+ L'.SgnError => sgnerror
+ | L'.SgnConst sgis =>
+ if List.exists (fn (L'.SgiConAbs (x, _, k), _) =>
+ (unifyKinds k ck;
+ true)
+ | _ => false) sgis then
+ (L'.SgnWhere (sgn', x, c'), loc)
+ else
+ (sgnError env (UnWhereable (sgn', x));
+ sgnerror)
+ | _ => (sgnError env (UnWhereable (sgn', x));
+ sgnerror)
+ end
fun sgiOfDecl (d, loc) =
case d of
@@ -1118,13 +1143,6 @@ fun sgiOfDecl (d, loc) =
| L'.DSgn _ => NONE
| L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc)
-fun hnormSgn env (all as (sgn, _)) =
- case sgn of
- L'.SgnError => all
- | L'.SgnVar n => hnormSgn env (#2 (E.lookupSgnNamed env n))
- | L'.SgnConst _ => all
- | L'.SgnFun _ => all
-
fun subSgn env sgn1 (sgn2 as (_, loc2)) =
case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
(L'.SgnError, _) => ()
@@ -1240,6 +1258,7 @@ fun selfify env {str, strs, sgn} =
(L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)
| x => x) sgis), #2 sgn)
| L'.SgnFun _ => sgn
+ | L'.SgnWhere _ => sgn
fun elabDecl ((d, loc), env) =
let
@@ -1384,7 +1403,7 @@ and elabStr env (str, loc) =
NONE => actual
| SOME ran =>
let
- val ran' = elabSgn env ran
+ val ran' = elabSgn env' ran
in
subSgn env' actual ran';
ran'