Mercurial > urweb
changeset 59:abb2b32c19fb
Subsignatures
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 22 Jun 2008 19:10:38 -0400 |
| parents | fd8a81ecd598 |
| children | 8bce148070a7 |
| files | src/elab.sml src/elab_env.sig src/elab_env.sml src/elab_print.sml src/elab_util.sig src/elab_util.sml src/elaborate.sml src/explify.sml src/lacweb.grm src/source.sml src/source_print.sml |
| diffstat | 11 files changed, 182 insertions(+), 34 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab.sml Sun Jun 22 18:17:21 2008 -0400 +++ b/src/elab.sml Sun Jun 22 19:10:38 2008 -0400 @@ -87,12 +87,14 @@ | SgiCon of string * int * kind * con | SgiVal of string * int * con | SgiStr of string * int * sgn + | SgiSgn of string * int * sgn and sgn' = SgnConst of sgn_item list | SgnVar of int | SgnFun of string * int * sgn * sgn | SgnWhere of sgn * string * con + | SgnProj of int * string list * string | SgnError withtype sgn_item = sgn_item' located
--- a/src/elab_env.sig Sun Jun 22 18:17:21 2008 -0400 +++ b/src/elab_env.sig Sun Jun 22 19:10:38 2008 -0400 @@ -79,6 +79,7 @@ val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option + val projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option end
--- a/src/elab_env.sml Sun Jun 22 18:17:21 2008 -0400 +++ b/src/elab_env.sml Sun Jun 22 19:10:38 2008 -0400 @@ -298,23 +298,25 @@ | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) | SgiVal (x, n, t) => pushENamedAs env x n t | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn + | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn fun sgnSeek f sgis = let - fun seek (sgis, strs, cons) = + fun seek (sgis, sgns, strs, cons) = case sgis of [] => NONE | (sgi, _) :: sgis => case f sgi of - SOME v => SOME (v, (strs, cons)) + SOME v => SOME (v, (sgns, strs, cons)) | NONE => case sgi of - SgiConAbs (x, n, _) => seek (sgis, strs, IM.insert (cons, n, x)) - | SgiCon (x, n, _, _) => seek (sgis, strs, IM.insert (cons, n, x)) - | SgiVal _ => seek (sgis, strs, cons) - | SgiStr (x, n, _) => seek (sgis, IM.insert (strs, n, x), cons) + SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) + | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) + | SgiVal _ => seek (sgis, sgns, strs, cons) + | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons) + | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons) in - seek (sgis, IM.empty, IM.empty) + seek (sgis, IM.empty, IM.empty, IM.empty) end fun id x = x @@ -330,7 +332,7 @@ end | _ => raise Fail "unravelStr" -fun sgnS_con (str, (strs, cons)) c = +fun sgnS_con (str, (sgns, strs, cons)) c = case c of CModProj (m1, ms, x) => (case IM.find (strs, m1) of @@ -352,15 +354,37 @@ end) | _ => c -fun sgnSubCon (str, (strs, cons)) = +fun sgnS_sgn (str, (sgns, strs, cons)) sgn = + case sgn of + SgnProj (m1, ms, x) => + (case IM.find (strs, m1) of + NONE => sgn + | SOME m1x => + let + val (m1, ms') = unravelStr str + in + SgnProj (m1, ms' @ m1x :: ms, x) + end) + | SgnVar n => + (case IM.find (sgns, n) of + NONE => sgn + | SOME nx => + let + val (m1, ms) = unravelStr str + in + SgnProj (m1, ms, nx) + end) + | _ => sgn + +fun sgnSubCon x = ElabUtil.Con.map {kind = id, - con = sgnS_con (str, (strs, cons))} + con = sgnS_con x} -fun sgnSubSgn (str, (strs, cons)) = +fun sgnSubSgn x = ElabUtil.Sgn.map {kind = id, - con = sgnS_con (str, (strs, cons)), + con = sgnS_con x, sgn_item = id, - sgn = id} + sgn = sgnS_sgn x} fun hnormSgn env (all as (sgn, loc)) = case sgn of @@ -368,6 +392,16 @@ | SgnVar n => hnormSgn env (#2 (lookupSgnNamed env n)) | SgnConst _ => all | SgnFun _ => all + | SgnProj (m, ms, x) => + let + val (_, sgn) = lookupStrNamed env m + in + case projectSgn env {str = foldl (fn (m, str) => (StrProj (str, m), loc)) (StrVar m, loc) ms, + sgn = sgn, + field = x} of + NONE => raise Fail "ElabEnv.hnormSgn: projectSgn failed" + | SOME sgn => sgn + end | SgnWhere (sgn, x, c) => case #1 (hnormSgn env sgn) of SgnError => (SgnError, loc) @@ -389,6 +423,24 @@ end | _ => raise Fail "ElabEnv.hnormSgn: Can't reduce 'where' [2]" +and projectSgn env {sgn, str, field} = + case #1 (hnormSgn env sgn) of + SgnConst sgis => + (case sgnSeek (fn SgiSgn (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) + | _ => NONE + +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 + NONE => NONE + | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) + | SgnError => SOME (SgnError, ErrorMsg.dummySpan) + | _ => NONE + fun projectCon env {sgn, str, field} = case #1 (hnormSgn env sgn) of SgnConst sgis => @@ -409,13 +461,5 @@ | SgnError => SOME (CError, ErrorMsg.dummySpan) | _ => NONE -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 - NONE => NONE - | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn)) - | SgnError => SOME (SgnError, ErrorMsg.dummySpan) - | _ => NONE end
--- a/src/elab_print.sml Sun Jun 22 18:17:21 2008 -0400 +++ b/src/elab_print.sml Sun Jun 22 19:10:38 2008 -0400 @@ -294,6 +294,13 @@ string ":", space, p_sgn env sgn] + | SgiSgn (x, n, sgn) => box [string "signature", + space, + p_named x n, + space, + string "=", + space, + p_sgn env sgn] and p_sgn env (sgn, _) = case sgn of @@ -334,6 +341,17 @@ string "=", space, p_con env c] + | SgnProj (m1, ms, x) => + let + val (m1x, sgn) = E.lookupStrNamed env m1 + + val m1s = if !debug then + m1x ^ "__" ^ Int.toString m1 + else + m1x + in + p_list_sep (string ".") string (m1x :: ms @ [x]) + end | SgnError => string "<ERROR>" fun p_decl env ((d, _) : decl) =
--- a/src/elab_util.sig Sun Jun 22 18:17:21 2008 -0400 +++ b/src/elab_util.sig Sun Jun 22 19:10:38 2008 -0400 @@ -83,6 +83,7 @@ RelC of string * Elab.kind | NamedC of string * Elab.kind | Str of string * Elab.sgn + | Sgn of string * Elab.sgn val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
--- a/src/elab_util.sml Sun Jun 22 18:17:21 2008 -0400 +++ b/src/elab_util.sml Sun Jun 22 19:10:38 2008 -0400 @@ -305,6 +305,7 @@ RelC of string * Elab.kind | NamedC of string * Elab.kind | Str of string * Elab.sgn + | Sgn of string * Elab.sgn fun mapfoldB {kind, con, sgn_item, sgn, bind} = let @@ -343,6 +344,10 @@ S.map2 (sg ctx s, fn s' => (SgiStr (x, n, s'), loc)) + | SgiSgn (x, n, s) => + S.map2 (sg ctx s, + fn s' => + (SgiSgn (x, n, s'), loc)) and sg ctx s acc = S.bindP (sg' ctx s acc, sgn ctx) @@ -358,7 +363,9 @@ bind (ctx, NamedC (x, k)) | SgiVal _ => ctx | SgiStr (x, _, sgn) => - bind (ctx, Str (x, sgn)), + bind (ctx, Str (x, sgn)) + | SgiSgn (x, _, sgn) => + bind (ctx, Sgn (x, sgn)), sgi ctx si)) ctx sgis, fn sgis' => (SgnConst sgis', loc)) @@ -370,6 +377,7 @@ S.map2 (sg (bind (ctx, Str (m, s1'))) s2, fn s2' => (SgnFun (m, n, s1', s2'), loc))) + | SgnProj _ => S.return2 sAll | SgnWhere (sgn, x, c) => S.bind2 (sg ctx sgn, fn sgn' =>
--- a/src/elaborate.sml Sun Jun 22 18:17:21 2008 -0400 +++ b/src/elaborate.sml Sun Jun 22 19:10:38 2008 -0400 @@ -988,15 +988,15 @@ 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 @@ ([(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 @@ | _ => (sgnError env (NotIncludable sgn'); ([], env)) end + end and elabSgn env (sgn, loc) = @@ -1163,14 +1172,33 @@ | _ => (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 @@ 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 @@ | 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 @@ 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 @@ 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"
--- a/src/explify.sml Sun Jun 22 18:17:21 2008 -0400 +++ b/src/explify.sml Sun Jun 22 19:10:38 2008 -0400 @@ -87,6 +87,7 @@ | L.SgiCon (x, n, k, c) => (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc) | L.SgiVal (x, n, c) => (L'.SgiVal (x, n, explifyCon c), loc) | L.SgiStr (x, n, sgn) => (L'.SgiStr (x, n, explifySgn sgn), loc) + | L.SgiSgn _ => raise Fail "Explify SgiSgn" and explifySgn (sgn, loc) = case sgn of @@ -94,6 +95,7 @@ | L.SgnVar n => (L'.SgnVar n, loc) | L.SgnFun (m, n, dom, ran) => (L'.SgnFun (m, n, explifySgn dom, explifySgn ran), loc) | L.SgnWhere (sgn, x, c) => (L'.SgnWhere (explifySgn sgn, x, explifyCon c), loc) + | L.SgnProj _ => raise Fail "Explify SgnProj" | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc) fun explifyDecl (d, loc : EM.span) =
--- a/src/lacweb.grm Sun Jun 22 18:17:21 2008 -0400 +++ b/src/lacweb.grm Sun Jun 22 19:10:38 2008 -0400 @@ -63,6 +63,7 @@ | path of string list * string | spath of str + | mpath of string list | cexp of con | capps of con @@ -128,7 +129,13 @@ (SgnFun (CSYMBOL, sgn1, sgn2), s (FUNCTORleft, sgn2right)) sgntm : SIG sgis END (SgnConst sgis, s (SIGleft, ENDright)) - | CSYMBOL (SgnVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) + | mpath (case mpath of + [] => raise Fail "Impossible mpath parse" + | [x] => SgnVar x + | m :: ms => SgnProj (m, + List.take (ms, length ms - 1), + List.nth (ms, length ms - 1)), + s (mpathleft, mpathright)) | sgntm WHERE CON SYMBOL EQ cexp (SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright)) | sgntm WHERE LTYPE SYMBOL EQ cexp(SgnWhere (sgntm, SYMBOL, cexp), s (sgntmleft, cexpright)) | LPAREN sgn RPAREN (sgn) @@ -143,6 +150,7 @@ | VAL SYMBOL COLON cexp (SgiVal (SYMBOL, cexp), s (VALleft, cexpright)) | STRUCTURE CSYMBOL COLON sgn (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright)) + | SIGNATURE CSYMBOL EQ sgn (SgiSgn (CSYMBOL, sgn), s (SIGNATUREleft, sgnright)) | FUNCTOR CSYMBOL LPAREN CSYMBOL COLON sgn RPAREN COLON sgn (SgiStr (CSYMBOL1, (SgnFun (CSYMBOL2, sgn1, sgn2), s (FUNCTORleft, sgn2right))), @@ -191,6 +199,9 @@ path : SYMBOL ([], SYMBOL) | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end) +mpath : CSYMBOL ([CSYMBOL]) + | CSYMBOL DOT mpath (CSYMBOL :: mpath) + cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright)) | LBRACK rcon RBRACK (CRecord rcon, s (LBRACKleft, RBRACKright)) | LBRACE rcone RBRACE (TRecord (CRecord rcone, s (LBRACEleft, RBRACEright)),
--- a/src/source.sml Sun Jun 22 18:17:21 2008 -0400 +++ b/src/source.sml Sun Jun 22 19:10:38 2008 -0400 @@ -67,6 +67,7 @@ | SgiCon of string * kind option * con | SgiVal of string * con | SgiStr of string * sgn + | SgiSgn of string * sgn | SgiInclude of sgn and sgn' = @@ -74,6 +75,7 @@ | SgnVar of string | SgnFun of string * sgn * sgn | SgnWhere of sgn * string * con + | SgnProj of string * string list * string withtype sgn_item = sgn_item' located and sgn = sgn' located
--- a/src/source_print.sml Sun Jun 22 18:17:21 2008 -0400 +++ b/src/source_print.sml Sun Jun 22 19:10:38 2008 -0400 @@ -238,6 +238,13 @@ string ":", space, p_sgn sgn] + | SgiSgn (x, sgn) => box [string "signature", + space, + string x, + space, + string "=", + space, + p_sgn sgn] | SgiInclude sgn => box [string "include", space, p_sgn sgn] @@ -273,6 +280,8 @@ string "=", space, p_con c] + | SgnProj (m, ms, x) => p_list_sep (string ".") string (m :: ms @ [x]) + fun p_decl ((d, _) : decl) = case d of