diff options
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 72 |
1 files changed, 61 insertions, 11 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml index 56c23bfc..a96d90c7 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -988,15 +988,15 @@ fun sgnError env err = eprefaces' [("Item", p_sgn_item env sgi)]) | SgiWrongKind (sgi1, k1, sgi2, k2, kerr) => (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:"; - eprefaces' [("Item 1", p_sgn_item env sgi1), - ("Item 2", p_sgn_item env sgi2), + eprefaces' [("Have", p_sgn_item env sgi1), + ("Need", p_sgn_item env sgi2), ("Kind 1", p_kind k1), ("Kind 2", p_kind k2)]; kunifyError kerr) | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) => (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:"; - eprefaces' [("Item 1", p_sgn_item env sgi1), - ("Item 2", p_sgn_item env sgi2), + eprefaces' [("Have", p_sgn_item env sgi1), + ("Need", p_sgn_item env sgi2), ("Con 1", p_con env c1), ("Con 2", p_con env c2)]; cunifyError env cerr) @@ -1110,6 +1110,14 @@ fun elabSgn_item ((sgi, loc), env) = ([(L'.SgiStr (x, n, sgn'), loc)], env') end + | L.SgiSgn (x, sgn) => + let + val sgn' = elabSgn env sgn + val (env', n) = E.pushSgnNamed env x sgn' + in + ([(L'.SgiSgn (x, n, sgn'), loc)], env') + end + | L.SgiInclude sgn => let val sgn' = elabSgn env sgn @@ -1120,6 +1128,7 @@ fun elabSgn_item ((sgi, loc), env) = | _ => (sgnError env (NotIncludable sgn'); ([], env)) end + end and elabSgn env (sgn, loc) = @@ -1163,14 +1172,33 @@ and elabSgn env (sgn, loc) = | _ => (sgnError env (UnWhereable (sgn', x)); sgnerror) end + | L.SgnProj (m, ms, x) => + (case E.lookupStr env m of + NONE => (strError env (UnboundStr (loc, m)); + sgnerror) + | SOME (n, sgn) => + let + val (str, sgn) = foldl (fn (m, (str, sgn)) => + case E.projectStr env {sgn = sgn, str = str, field = m} of + NONE => (strError env (UnboundStr (loc, m)); + (strerror, sgnerror)) + | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) + ((L'.StrVar n, loc), sgn) ms + in + case E.projectSgn env {sgn = sgn, str = str, field = x} of + NONE => (sgnError env (UnboundSgn (loc, x)); + sgnerror) + | SOME _ => (L'.SgnProj (n, ms, x), loc) + end) + fun sgiOfDecl (d, loc) = case d of - L'.DCon (x, n, k, c) => SOME (L'.SgiCon (x, n, k, c), loc) - | L'.DVal (x, n, t, _) => SOME (L'.SgiVal (x, n, t), loc) - | L'.DSgn _ => NONE - | L'.DStr (x, n, sgn, _) => SOME (L'.SgiStr (x, n, sgn), loc) - | L'.DFfiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, sgn), loc) + L'.DCon (x, n, k, c) => (L'.SgiCon (x, n, k, c), loc) + | L'.DVal (x, n, t, _) => (L'.SgiVal (x, n, t), loc) + | L'.DSgn (x, n, sgn) => (L'.SgiSgn (x, n, sgn), loc) + | L'.DStr (x, n, sgn, _) => (L'.SgiStr (x, n, sgn), loc) + | L'.DFfiStr (x, n, sgn) => (L'.SgiStr (x, n, sgn), loc) fun subSgn env sgn1 (sgn2 as (_, loc2)) = case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of @@ -1264,6 +1292,18 @@ fun subSgn env sgn1 (sgn2 as (_, loc2)) = NONE | _ => NONE) (* Add type equations between structures here some day. *) + + | L'.SgiSgn (x, n2, sgn2) => + seek (fn sgi1All as (sgi1, _) => + case sgi1 of + L'.SgiSgn (x', n1, sgn1) => + if x = x' then + (subSgn env sgn1 sgn2; + subSgn env sgn2 sgn1; + SOME env) + else + NONE + | _ => NONE) end in ignore (foldl folder env sgis2) @@ -1296,6 +1336,13 @@ fun selfify env {str, strs, sgn} = | x => x) sgis), #2 sgn) | L'.SgnFun _ => sgn | L'.SgnWhere _ => sgn + | L'.SgnProj (m, ms, x) => + case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) + (L'.StrVar m, #2 sgn) ms, + sgn = #2 (E.lookupStrNamed env m), + field = x} of + NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE" + | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn} fun selfifyAt env {str, sgn} = let @@ -1430,7 +1477,7 @@ and elabStr env (str, loc) = L.StrConst ds => let val (ds', env') = ListUtil.foldlMap elabDecl env ds - val sgis = List.mapPartial sgiOfDecl ds' + val sgis = map sgiOfDecl ds' in ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc)) end @@ -1509,7 +1556,10 @@ fun elabFile basis env file = E.pushENamedAs env' x n t) | L'.SgiStr (x, n, sgn) => ((L'.DStr (x, n, sgn, (L'.StrProj ((L'.StrVar basis_n, loc), x), loc)), loc), - E.pushStrNamedAs env' x n sgn)) + E.pushStrNamedAs env' x n sgn) + | L'.SgiSgn (x, n, sgn) => + ((L'.DSgn (x, n, (L'.SgnProj (basis_n, [], x), loc)), loc), + E.pushSgnNamedAs env' x n sgn)) env' sgis | _ => raise Fail "Non-constant Basis signature" |