summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-19 16:04:28 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-19 16:04:28 -0400
commit7a1c5e1780fd3c56d9c591821905bb3b3bbfa50a (patch)
tree1ea265b32102b42663cc227b04c8c4e86e4b136f /src
parent5a4ddea95a551c5f95f0dcbda433fe457b61d25a (diff)
Beginning of functor elaboration
Diffstat (limited to 'src')
-rw-r--r--src/elab.sml2
-rw-r--r--src/elab_env.sml3
-rw-r--r--src/elab_print.sig1
-rw-r--r--src/elab_print.sml35
-rw-r--r--src/elab_util.sml6
-rw-r--r--src/elaborate.sml124
-rw-r--r--src/explify.sml2
7 files changed, 135 insertions, 38 deletions
diff --git a/src/elab.sml b/src/elab.sml
index da64febf..07bb7f8d 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -91,6 +91,7 @@ datatype sgn_item' =
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 @@ datatype decl' =
StrConst of decl list
| StrVar of int
| StrProj of str * string
+ | StrFun of string * int * sgn * sgn * str
| StrError
withtype decl = decl' located
diff --git a/src/elab_env.sml b/src/elab_env.sml
index b10882a7..9d308ddc 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -376,6 +376,7 @@ fun projectCon env {sgn = (sgn, _), str, field} =
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 @@ fun projectVal env {sgn = (sgn, _), str, field} =
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 @@ fun projectStr env {sgn = (sgn, _), str, field} =
projectStr env {sgn = sgn, str = str, field = field}
end
| SgnError => SOME (SgnError, ErrorMsg.dummySpan)
+ | SgnFun _ => NONE
val ktype = (KType, ErrorMsg.dummySpan)
diff --git a/src/elab_print.sig b/src/elab_print.sig
index 49af2ded..9ab9eae7 100644
--- a/src/elab_print.sig
+++ b/src/elab_print.sig
@@ -34,6 +34,7 @@ signature ELAB_PRINT = sig
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
diff --git a/src/elab_print.sml b/src/elab_print.sml
index b214d5d4..03792e03 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -310,6 +310,19 @@ 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.pushStrNamedAs env x n sgn) sgn']
| SgnError => string "<ERROR>"
fun p_decl env ((d, _) : decl) =
@@ -367,6 +380,28 @@ 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.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 =
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 24e772d6..e2b4f113 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -364,6 +364,12 @@ 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)))
| SgnError => S.return2 sAll
in
sg
diff --git a/src/elaborate.sml b/src/elaborate.sml
index d482f9a0..10fa3898 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -968,6 +968,7 @@ datatype sgn_error =
| 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 @@ fun sgnError env err =
("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 @@ and elabSgn env (sgn, loc) =
(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 @@ fun hnormSgn env (all as (sgn, _)) =
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 @@ fun subSgn env sgn1 (sgn2 as (_, loc2)) =
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 @@ fun subSgn env sgn1 (sgn2 as (_, loc2)) =
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 @@ fun selfify env {str, strs, sgn} =
| (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 @@ and elabStr env (str, loc) =
(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
diff --git a/src/explify.sml b/src/explify.sml
index a1953fab..caba15d1 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -92,6 +92,7 @@ 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.SgnError => raise Fail ("explifySgn: SgnError at " ^ EM.spanToString loc)
fun explifyDecl (d, loc : EM.span) =
@@ -107,6 +108,7 @@ 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.StrError => raise Fail ("explifyStr: StrError at " ^ EM.spanToString loc)
val explify = map explifyDecl