summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/corify.sml4
-rw-r--r--src/expl.sml4
-rw-r--r--src/expl_print.sml50
-rw-r--r--src/expl_util.sml13
-rw-r--r--src/explify.sml8
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