Mercurial > urweb
changeset 41:1405d8c26790
Beginning of functor elaboration
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 19 Jun 2008 16:04:28 -0400 |
| parents | e3d3c2791105 |
| children | b3fbbc6cb1e5 |
| files | src/elab.sml src/elab_env.sml src/elab_print.sig src/elab_print.sml src/elab_util.sml src/elaborate.sml src/explify.sml tests/functor.lac |
| diffstat | 8 files changed, 140 insertions(+), 39 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab.sml Thu Jun 19 15:15:00 2008 -0400 +++ b/src/elab.sml Thu Jun 19 16:04:28 2008 -0400 @@ -91,6 +91,7 @@ and sgn' = SgnConst of sgn_item list | SgnVar of int + | SgnFun of string * int * sgn * sgn | SgnError withtype sgn_item = sgn_item' located @@ -106,6 +107,7 @@ StrConst of decl list | StrVar of int | StrProj of str * string + | StrFun of string * int * sgn * sgn * str | StrError withtype decl = decl' located
--- a/src/elab_env.sml Thu Jun 19 15:15:00 2008 -0400 +++ b/src/elab_env.sml Thu Jun 19 16:04:28 2008 -0400 @@ -376,6 +376,7 @@ projectCon env {sgn = sgn, str = str, field = field} end | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan)) + | SgnFun _ => NONE fun projectVal env {sgn = (sgn, _), str, field} = case sgn of @@ -390,6 +391,7 @@ projectVal env {sgn = sgn, str = str, field = field} end | SgnError => SOME (CError, ErrorMsg.dummySpan) + | SgnFun _ => NONE fun projectStr env {sgn = (sgn, _), str, field} = case sgn of @@ -404,6 +406,7 @@ projectStr env {sgn = sgn, str = str, field = field} end | SgnError => SOME (SgnError, ErrorMsg.dummySpan) + | SgnFun _ => NONE val ktype = (KType, ErrorMsg.dummySpan)
--- a/src/elab_print.sig Thu Jun 19 15:15:00 2008 -0400 +++ b/src/elab_print.sig Thu Jun 19 16:04:28 2008 -0400 @@ -34,6 +34,7 @@ val p_exp : ElabEnv.env -> Elab.exp Print.printer val p_decl : ElabEnv.env -> Elab.decl Print.printer val p_sgn_item : ElabEnv.env -> Elab.sgn_item Print.printer + val p_sgn : ElabEnv.env -> Elab.sgn Print.printer val p_file : ElabEnv.env -> Elab.file Print.printer val debug : bool ref
--- a/src/elab_print.sml Thu Jun 19 15:15:00 2008 -0400 +++ b/src/elab_print.sml Thu Jun 19 16:04:28 2008 -0400 @@ -310,6 +310,19 @@ newline, string "end"] | SgnVar n => string (#1 (E.lookupSgnNamed env n)) + | SgnFun (x, n, sgn, sgn') => box [string "functor", + space, + string "(", + string x, + space, + string ":", + space, + p_sgn env sgn, + string ")", + space, + string ":", + space, + p_sgn (E.pushStrNamedAs env x n sgn) sgn'] | SgnError => string "<ERROR>" fun p_decl env ((d, _) : decl) = @@ -367,6 +380,28 @@ | StrProj (str, s) => box [p_str env str, string ".", string s] + | StrFun (x, n, sgn, sgn', str) => + let + val env' = E.pushStrNamedAs env x n sgn + in + box [string "functor", + space, + string "(", + string x, + space, + string ":", + space, + p_sgn env sgn, + string ")", + space, + string ":", + space, + p_sgn env' sgn', + space, + string "=>", + space, + p_str env' str] + end | StrError => string "<ERROR>" and p_file env file =
--- a/src/elab_util.sml Thu Jun 19 15:15:00 2008 -0400 +++ b/src/elab_util.sml Thu Jun 19 16:04:28 2008 -0400 @@ -364,6 +364,12 @@ (SgnConst sgis', loc)) | SgnVar _ => S.return2 sAll + | SgnFun (m, n, s1, s2) => + S.bind2 (sg ctx s1, + fn s1' => + S.map2 (sg (bind (ctx, Str (m, s1'))) s2, + fn s2' => + (SgnFun (m, n, s1', s2'), loc))) | SgnError => S.return2 sAll in sg
--- a/src/elaborate.sml Thu Jun 19 15:15:00 2008 -0400 +++ b/src/elaborate.sml Thu Jun 19 16:04:28 2008 -0400 @@ -968,6 +968,7 @@ | UnmatchedSgi of L'.sgn_item | 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 fun sgnError env err = case err of @@ -990,6 +991,10 @@ ("Con 1", p_con env c1), ("Con 2", p_con env c2)]; cunifyError env cerr) + | SgnWrongForm (sgn1, sgn2) => + (ErrorMsg.errorAt (#2 sgn1) "Incompatible signatures:"; + eprefaces' [("Sig 1", p_sgn env sgn1), + ("Sig 2", p_sgn env sgn2)]) datatype str_error = UnboundStr of ErrorMsg.span * string @@ -1097,7 +1102,14 @@ (sgnError env (UnboundSgn (loc, x)); (L'.SgnError, loc)) | SOME (n, sgis) => (L'.SgnVar n, loc)) - | L.SgnFun _ => raise Fail "Elaborate functor sig" + | L.SgnFun (m, dom, ran) => + let + val dom' = elabSgn env dom + val (env', n) = E.pushStrNamed env m dom' + val ran' = elabSgn env' ran + in + (L'.SgnFun (m, n, dom', ran'), loc) + end fun sgiOfDecl (d, loc) = case d of @@ -1111,15 +1123,13 @@ 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, _) => () | (_, L'.SgnError) => () - | (L'.SgnVar n, _) => raise Fail "subSgn: Variable remains" - | (_, L'.SgnVar n) => raise Fail "subSgn: Variable remains" - | (L'.SgnConst sgis1, L'.SgnConst sgis2) => let fun folder (sgi2All as (sgi, _), env) = @@ -1142,57 +1152,69 @@ L'.SgiConAbs (x, n2, k2) => seek (fn sgi1All as (sgi1, _) => let - fun found (x, n1, k1, co1) = - let - val () = unifyKinds k1 k2 - handle KUnify (k1, k2, err) => - sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) - val env = E.pushCNamedAs env x n1 k1 co1 - in - SOME (if n1 = n2 then - env - else - E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2))) - end + fun found (x', n1, k1, co1) = + if x = x' then + let + val () = unifyKinds k1 k2 + handle KUnify (k1, k2, err) => + sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) + val env = E.pushCNamedAs env x n1 k1 co1 + in + SOME (if n1 = n2 then + env + else + E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2))) + end + else + NONE in case sgi1 of - L'.SgiConAbs (x, n1, k1) => found (x, n1, k1, NONE) - | L'.SgiCon (x, n1, k1, c1) => found (x, n1, k1, SOME c1) + L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE) + | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1) | _ => NONE end) | L'.SgiCon (x, n2, k2, c2) => seek (fn sgi1All as (sgi1, _) => case sgi1 of - L'.SgiCon (x, n1, k1, c1) => - let - val () = unifyCons env c1 c2 - handle CUnify (c1, c2, err) => - sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)) - in - SOME (E.pushCNamedAs env x n2 k2 (SOME c2)) - end + L'.SgiCon (x', n1, k1, c1) => + if x = x' then + let + val () = unifyCons env c1 c2 + handle CUnify (c1, c2, err) => + sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)) + in + SOME (E.pushCNamedAs env x n2 k2 (SOME c2)) + end + else + NONE | _ => NONE) | L'.SgiVal (x, n2, c2) => seek (fn sgi1All as (sgi1, _) => case sgi1 of - L'.SgiVal (x, n1, c1) => - let - val () = unifyCons env c1 c2 - handle CUnify (c1, c2, err) => - sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)) - in - SOME env - end + L'.SgiVal (x', n1, c1) => + if x = x' then + let + val () = unifyCons env c1 c2 + handle CUnify (c1, c2, err) => + sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)) + in + SOME env + end + else + NONE | _ => NONE) | L'.SgiStr (x, n2, sgn2) => seek (fn sgi1All as (sgi1, _) => case sgi1 of - L'.SgiStr (x, n1, sgn1) => - (subSgn env sgn1 sgn2; - SOME env) + L'.SgiStr (x', n1, sgn1) => + if x = x' then + (subSgn env sgn1 sgn2; + SOME env) + else + NONE | _ => NONE) (* Add type equations between structures here some day. *) end @@ -1200,6 +1222,12 @@ ignore (foldl folder env sgis2) end + | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) => + (subSgn env dom2 dom1; + subSgn env ran1 ran2) + + | _ => sgnError env (SgnWrongForm (sgn1, sgn2)) + fun selfify env {str, strs, sgn} = case #1 (hnormSgn env sgn) of L'.SgnError => sgn @@ -1211,6 +1239,7 @@ | (L'.SgiStr (x, n, sgn), loc) => (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) | x => x) sgis), #2 sgn) + | L'.SgnFun _ => sgn fun elabDecl ((d, loc), env) = let @@ -1344,7 +1373,26 @@ (strerror, sgnerror)) | SOME sgn => ((L'.StrProj (str', x), loc), sgn) end - | L.StrFun _ => raise Fail "Elaborate functor" + | L.StrFun (m, dom, ranO, str) => + let + val dom' = elabSgn env dom + val (env', n) = E.pushStrNamed env m dom' + val (str', actual) = elabStr env' str + + val formal = + case ranO of + NONE => actual + | SOME ran => + let + val ran' = elabSgn env ran + in + subSgn env' actual ran'; + ran' + end + in + ((L'.StrFun (m, n, dom', formal, str'), loc), + (L'.SgnFun (m, n, dom', formal), loc)) + end val elabFile = ListUtil.foldlMap elabDecl
--- a/src/explify.sml Thu Jun 19 15:15:00 2008 -0400 +++ b/src/explify.sml Thu Jun 19 16:04:28 2008 -0400 @@ -92,6 +92,7 @@ case sgn of L.SgnConst sgis => (L'.SgnConst (map explifySgi sgis), loc) | L.SgnVar n => (L'.SgnVar n, loc) + | L.SgnFun _ => raise Fail "Explify functor signature" | L.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc) fun explifyDecl (d, loc : EM.span) = @@ -107,6 +108,7 @@ L.StrConst ds => (L'.StrConst (map explifyDecl ds), loc) | L.StrVar n => (L'.StrVar n, loc) | L.StrProj (str, s) => (L'.StrProj (explifyStr str, s), loc) + | L.StrFun _ => raise Fail "Explify functor" | L.StrError => raise Fail ("explifyStr: StrError at " ^ EM.spanToString loc) val explify = map explifyDecl
--- a/tests/functor.lac Thu Jun 19 15:15:00 2008 -0400 +++ b/tests/functor.lac Thu Jun 19 16:04:28 2008 -0400 @@ -9,7 +9,11 @@ val three : t end +signature F = functor (M : S) : T + structure F = functor (M : S) : T => struct - val t = M.t + type t = M.t val three = M.s (M.s (M.s M.z)) end + +structure F2 : F = F