Mercurial > urweb
changeset 44:a9f3ce2d1b9b
Elaborating functor applications
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 19 Jun 2008 17:04:08 -0400 |
| parents | d94c484337d0 |
| children | 3c1ce1b4eb3d |
| files | src/elab.sml src/elab_print.sml src/elaborate.sml src/explify.sml src/lacweb.grm src/source.sml src/source_print.sml tests/functor.lac |
| diffstat | 8 files changed, 71 insertions(+), 13 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab.sml Thu Jun 19 16:43:24 2008 -0400 +++ b/src/elab.sml Thu Jun 19 17:04:08 2008 -0400 @@ -109,6 +109,7 @@ | StrVar of int | StrProj of str * string | StrFun of string * int * sgn * sgn * str + | StrApp of str * str | StrError withtype decl = decl' located
--- a/src/elab_print.sml Thu Jun 19 16:43:24 2008 -0400 +++ b/src/elab_print.sml Thu Jun 19 17:04:08 2008 -0400 @@ -413,6 +413,10 @@ space, p_str env' str] end + | StrApp (str1, str2) => box [p_str env str1, + string "(", + p_str env str2, + string ")"] | StrError => string "<ERROR>" and p_file env file =
--- a/src/elaborate.sml Thu Jun 19 16:43:24 2008 -0400 +++ b/src/elaborate.sml Thu Jun 19 17:04:08 2008 -0400 @@ -1014,11 +1014,15 @@ datatype str_error = UnboundStr of ErrorMsg.span * string + | NotFunctor of L'.sgn fun strError env err = case err of UnboundStr (loc, s) => ErrorMsg.errorAt loc ("Unbound structure variable " ^ s) + | NotFunctor sgn => + (ErrorMsg.errorAt (#2 sgn) "Application of non-functor"; + eprefaces' [("Signature", p_sgn env sgn)]) val hnormSgn = E.hnormSgn @@ -1279,6 +1283,22 @@ | L'.SgnFun _ => sgn | L'.SgnWhere _ => sgn +fun selfifyAt env {str, sgn} = + let + fun self (str, _) = + case str of + L'.StrVar x => SOME (x, []) + | L'.StrProj (str, x) => + (case self str of + NONE => NONE + | SOME (m, ms) => SOME (m, ms @ [x])) + | _ => NONE + in + case self str of + NONE => sgn + | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs} + end + fun elabDecl ((d, loc), env) = let @@ -1363,20 +1383,8 @@ val formal = Option.map (elabSgn env) sgno val (str', actual) = elabStr env str - fun self (str, _) = - case str of - L'.StrVar x => SOME (x, []) - | L'.StrProj (str, x) => - (case self str of - NONE => NONE - | SOME (m, ms) => SOME (m, ms @ [x])) - | _ => NONE - val sgn' = case formal of - NONE => - (case self str' of - NONE => actual - | SOME (str, strs) => selfify env {sgn = actual, str = str, strs = strs}) + NONE => selfifyAt env {str = str', sgn = actual} | SOME formal => (subSgn env actual formal; formal) @@ -1431,6 +1439,24 @@ ((L'.StrFun (m, n, dom', formal, str'), loc), (L'.SgnFun (m, n, dom', formal), loc)) end + | L.StrApp (str1, str2) => + let + val (str1', sgn1) = elabStr env str1 + val (str2', sgn2) = elabStr env str2 + in + case #1 (hnormSgn env sgn1) of + L'.SgnError => (strerror, sgnerror) + | L'.SgnFun (m, n, dom, ran) => + (subSgn env sgn2 dom; + case #1 (hnormSgn env ran) of + L'.SgnError => (strerror, sgnerror) + | L'.SgnConst sgis => + ((L'.StrApp (str1', str2'), loc), + (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc)) + | _ => raise Fail "Unable to hnormSgn in functor application") + | _ => (strError env (NotFunctor sgn1); + (strerror, sgnerror)) + end val elabFile = ListUtil.foldlMap elabDecl
--- a/src/explify.sml Thu Jun 19 16:43:24 2008 -0400 +++ b/src/explify.sml Thu Jun 19 17:04:08 2008 -0400 @@ -110,6 +110,7 @@ | L.StrVar n => (L'.StrVar n, loc) | L.StrProj (str, s) => (L'.StrProj (explifyStr str, s), loc) | L.StrFun _ => raise Fail "Explify functor" + | L.StrApp _ => raise Fail "Explify functor app" | L.StrError => raise Fail ("explifyStr: StrError at " ^ EM.spanToString loc) val explify = map explifyDecl
--- a/src/lacweb.grm Thu Jun 19 16:43:24 2008 -0400 +++ b/src/lacweb.grm Thu Jun 19 17:04:08 2008 -0400 @@ -154,6 +154,7 @@ (StrFun (CSYMBOL, sgn, NONE, str), s (FUNCTORleft, strright)) | FUNCTOR LPAREN CSYMBOL COLON sgn RPAREN COLON sgn DARROW str (StrFun (CSYMBOL, sgn1, SOME sgn2, str), s (FUNCTORleft, strright)) + | spath LPAREN str RPAREN (StrApp (spath, str), s (spathleft, RPARENright)) spath : CSYMBOL (StrVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) | spath DOT CSYMBOL (StrProj (spath, CSYMBOL), s (spathleft, CSYMBOLright))
--- a/src/source.sml Thu Jun 19 16:43:24 2008 -0400 +++ b/src/source.sml Thu Jun 19 17:04:08 2008 -0400 @@ -103,6 +103,7 @@ | StrVar of string | StrProj of str * string | StrFun of string * sgn * sgn option * str + | StrApp of str * str withtype decl = decl' located and str = str' located
--- a/src/source_print.sml Thu Jun 19 16:43:24 2008 -0400 +++ b/src/source_print.sml Thu Jun 19 17:04:08 2008 -0400 @@ -375,6 +375,10 @@ string "=>", space, p_str str] + | StrApp (str1, str2) => box [p_str str1, + string "(", + p_str str2, + string ")"] val p_file = p_list_sep newline p_decl
--- a/tests/functor.lac Thu Jun 19 16:43:24 2008 -0400 +++ b/tests/functor.lac Thu Jun 19 17:04:08 2008 -0400 @@ -18,3 +18,23 @@ structure F3 : functor (M : S) : T = F (*structure F4 : functor (M : S) : sig type q end = F*) (*structure F5 : functor (M : S) : T where type t = int = F*) + + +structure O = F (struct + type t = int + val z = 0 + val s = fn x : t => x +end) +val three : int = O.three + +structure S = struct + type t = int + val z = 0 + val s = fn x : t => x +end +structure SO = F (S) +val three : int = SO.three + +structure SS : S = S +structure SSO = F (SS) +val three : SS.t = SSO.three