diff options
| -rw-r--r-- | src/corify.sml | 4 | ||||
| -rw-r--r-- | src/expl.sml | 4 | ||||
| -rw-r--r-- | src/expl_print.sml | 50 | ||||
| -rw-r--r-- | src/expl_util.sml | 13 | ||||
| -rw-r--r-- | src/explify.sml | 8 |
5 files changed, 75 insertions, 4 deletions
diff --git a/src/corify.sml b/src/corify.sml index 607d173a..94e3d421 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -257,6 +257,8 @@ and corifyStr ((str, _), st) = 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 @@ and maxNameStr (str, _) = 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 diff --git a/src/expl.sml b/src/expl.sml index b3ab20c0..295aa9b2 100644 --- a/src/expl.sml +++ b/src/expl.sml @@ -79,6 +79,8 @@ datatype sgn_item' = 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 @@ datatype decl' = 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 diff --git a/src/expl_print.sml b/src/expl_print.sml index 4841f0c7..0e7f66eb 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -293,6 +293,30 @@ and p_sgn env (sgn, _) = 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 @@ and p_str env (str, _) = | 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 diff --git a/src/expl_util.sml b/src/expl_util.sml index 8c2a0f58..ebdd22d2 100644 --- a/src/expl_util.sml +++ b/src/expl_util.sml @@ -353,6 +353,19 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = (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 diff --git a/src/explify.sml b/src/explify.sml index 2df414a9..2d52083a 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -92,8 +92,8 @@ and explifySgn (sgn, loc) = 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 @@ and explifyStr (str, loc) = 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 |