Mercurial > urweb
changeset 45:3c1ce1b4eb3d
Explifying functors
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Thu, 19 Jun 2008 17:11:24 -0400 |
| parents | a9f3ce2d1b9b |
| children | 44a1bc863f0f |
| files | src/corify.sml src/expl.sml src/expl_print.sml src/expl_util.sml src/explify.sml |
| diffstat | 5 files changed, 75 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/src/corify.sml Thu Jun 19 17:04:08 2008 -0400 +++ b/src/corify.sml Thu Jun 19 17:11:24 2008 -0400 @@ -257,6 +257,8 @@ in (ds, {inner = St.lookupStrByName (x, inner), outer = outer}) end + | L.StrFun _ => raise Fail "Corify functor" + | L.StrApp _ => raise Fail "Corify functor app" fun maxName ds = foldl (fn ((d, _), n) => case d of @@ -271,6 +273,8 @@ L.StrConst ds => maxName ds | L.StrVar n => n | L.StrProj (str, _) => maxNameStr str + | L.StrFun (_, _, _, _, str) => maxNameStr str + | L.StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2) fun corify ds = let
--- a/src/expl.sml Thu Jun 19 17:04:08 2008 -0400 +++ b/src/expl.sml Thu Jun 19 17:11:24 2008 -0400 @@ -79,6 +79,8 @@ and sgn' = SgnConst of sgn_item list | SgnVar of int + | SgnFun of string * int * sgn * sgn + | SgnWhere of sgn * string * con withtype sgn_item = sgn_item' located and sgn = sgn' located @@ -93,6 +95,8 @@ StrConst of decl list | StrVar of int | StrProj of str * string + | StrFun of string * int * sgn * sgn * str + | StrApp of str * str withtype decl = decl' located and str = str' located
--- a/src/expl_print.sml Thu Jun 19 17:04:08 2008 -0400 +++ b/src/expl_print.sml Thu Jun 19 17:11:24 2008 -0400 @@ -293,6 +293,30 @@ 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.pushStrNamed env x n sgn) sgn'] + | SgnWhere (sgn, x, c) => box [p_sgn env sgn, + space, + string "where", + space, + string "con", + space, + string x, + space, + string "=", + space, + p_con env c] fun p_decl env ((d, _) : decl) = case d of @@ -349,6 +373,32 @@ | StrProj (str, s) => box [p_str env str, string ".", string s] + | StrFun (x, n, sgn, sgn', str) => + let + val env' = E.pushStrNamed 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 + | StrApp (str1, str2) => box [p_str env str1, + string "(", + p_str env str2, + string ")"] and p_file env file = let
--- a/src/expl_util.sml Thu Jun 19 17:04:08 2008 -0400 +++ b/src/expl_util.sml Thu Jun 19 17:11:24 2008 -0400 @@ -353,6 +353,19 @@ (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))) + | SgnWhere (sgn, x, c) => + S.bind2 (sg ctx sgn, + fn sgn' => + S.map2 (con ctx c, + fn c' => + (SgnWhere (sgn', x, c'), loc))) in sg end
--- a/src/explify.sml Thu Jun 19 17:04:08 2008 -0400 +++ b/src/explify.sml Thu Jun 19 17:11:24 2008 -0400 @@ -92,8 +92,8 @@ 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.SgnWhere _ => raise Fail "Explify where" + | 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.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc) fun explifyDecl (d, loc : EM.span) = @@ -109,8 +109,8 @@ 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.StrApp _ => raise Fail "Explify functor app" + | L.StrFun (m, n, dom, ran, str) => (L'.StrFun (m, n, explifySgn dom, explifySgn ran, explifyStr str), loc) + | L.StrApp (str1, str2) => (L'.StrApp (explifyStr str1, explifyStr str2), loc) | L.StrError => raise Fail ("explifyStr: StrError at " ^ EM.spanToString loc) val explify = map explifyDecl