summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/elab_env.sig2
-rw-r--r--src/elab_env.sml62
-rw-r--r--src/elaborate.sml124
-rw-r--r--tests/datatypeMod.lac8
4 files changed, 169 insertions, 27 deletions
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 4bc480cc..0afa3114 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -93,4 +93,6 @@ signature ELAB_ENV = sig
val newNamed : unit -> int
+ val chaseMpath : env -> (int * string list) -> Elab.str * Elab.sgn
+
end
diff --git a/src/elab_env.sml b/src/elab_env.sml
index fc6560e7..d28b713f 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -366,7 +366,16 @@ fun sgnSeek f sgis =
[] => NONE
| (sgi, _) :: sgis =>
case f sgi of
- SOME v => SOME (v, (sgns, strs, cons))
+ SOME v =>
+ let
+ val cons =
+ case sgi of
+ SgiDatatype (x, n, _) => IM.insert (cons, n, x)
+ | SgiDatatypeImp (x, n, _, _, _) => IM.insert (cons, n, x)
+ | _ => cons
+ in
+ SOME (v, (sgns, strs, cons))
+ end
| NONE =>
case sgi of
SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x))
@@ -503,12 +512,28 @@ fun projectStr env {sgn, str, field} =
| SgnError => SOME (SgnError, ErrorMsg.dummySpan)
| _ => NONE
+fun chaseMpath env (n, ms) =
+ let
+ val (_, sgn) = lookupStrNamed env n
+ in
+ foldl (fn (m, (str, sgn)) =>
+ case projectStr env {sgn = sgn, str = str, field = m} of
+ NONE => raise Fail "kindof: Unknown substructure"
+ | SOME sgn => ((StrProj (str, m), #2 sgn), sgn))
+ ((StrVar n, #2 sgn), sgn) ms
+ end
+
fun projectCon env {sgn, str, field} =
case #1 (hnormSgn env sgn) of
SgnConst sgis =>
(case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE
| SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE
| SgiDatatype (x, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE
+ | SgiDatatypeImp (x, _, m1, ms, x') =>
+ if x = field then
+ SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn))
+ else
+ NONE
| _ => NONE) sgis of
NONE => NONE
| SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
@@ -519,6 +544,15 @@ fun projectDatatype env {sgn, str, field} =
case #1 (hnormSgn env sgn) of
SgnConst sgis =>
(case sgnSeek (fn SgiDatatype (x, _, xncs) => if x = field then SOME xncs else NONE
+ | SgiDatatypeImp (x, _, m1, ms, x') =>
+ if x = field then
+ let
+ val (str, sgn) = chaseMpath env (m1, ms)
+ in
+ projectDatatype env {sgn = sgn, str = str, field = x'}
+ end
+ else
+ NONE
| _ => NONE) sgis of
NONE => NONE
| SOME (xncs, subs) => SOME (map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs))
@@ -527,7 +561,31 @@ fun projectDatatype env {sgn, str, field} =
fun projectVal env {sgn, str, field} =
case #1 (hnormSgn env sgn) of
SgnConst sgis =>
- (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE | _ => NONE) sgis of
+ (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE
+ | SgiDatatype (_, n, xncs) =>
+ ListUtil.search (fn (x, _, to) =>
+ if x = field then
+ SOME (case to of
+ NONE => (CNamed n, #2 sgn)
+ | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn))
+ else
+ NONE) xncs
+ | SgiDatatypeImp (_, n, m1, ms, x') =>
+ let
+ val (str, sgn) = chaseMpath env (m1, ms)
+ in
+ case projectDatatype env {sgn = sgn, str = str, field = x'} of
+ NONE => NONE
+ | SOME xncs =>
+ ListUtil.search (fn (x, _, to) =>
+ if x = field then
+ SOME (case to of
+ NONE => (CNamed n, #2 sgn)
+ | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn))
+ else
+ NONE) xncs
+ end
+ | _ => NONE) sgis of
NONE => NONE
| SOME (c, subs) => SOME (sgnSubCon (str, subs) c))
| SgnError => SOME (CError, ErrorMsg.dummySpan)
diff --git a/src/elaborate.sml b/src/elaborate.sml
index f5efdd96..9cc695e1 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1237,6 +1237,7 @@ datatype str_error =
| UnOpenable of L'.sgn
| NotType of L'.kind * (L'.kind * L'.kind * kunify_error)
| DuplicateConstructor of string * ErrorMsg.span
+ | NotDatatype of ErrorMsg.span
fun strError env err =
case err of
@@ -1258,6 +1259,8 @@ fun strError env err =
kunifyError ue)
| DuplicateConstructor (x, loc) =>
ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x)
+ | NotDatatype loc =>
+ ErrorMsg.errorAt loc "Trying to import non-datatype as a datatype"
val hnormSgn = E.hnormSgn
@@ -1319,7 +1322,44 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
([(L'.SgiDatatype (x, n, xcs), loc)], (env, denv, gs))
end
- | L.SgiDatatypeImp _ => raise Fail "Elaborate SgiDatatypeImp"
+ | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp"
+
+ | L.SgiDatatypeImp (x, m1 :: ms, s) =>
+ (case E.lookupStr env m1 of
+ NONE => (strError env (UnboundStr (loc, m1));
+ ([], (env, denv, gs)))
+ | SOME (n, sgn) =>
+ let
+ val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+ case E.projectStr env {sgn = sgn, str = str, field = m} of
+ NONE => (conError env (UnboundStrInCon (loc, m));
+ (strerror, sgnerror))
+ | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+ ((L'.StrVar n, loc), sgn) ms
+ in
+ case E.projectDatatype env {sgn = sgn, str = str, field = s} of
+ NONE => (conError env (UnboundDatatype (loc, s));
+ ([], (env, denv, gs)))
+ | SOME xncs =>
+ let
+ val k = (L'.KType, loc)
+ val t = (L'.CModProj (n, ms, s), loc)
+ val (env, n') = E.pushCNamed env x k (SOME t)
+ val env = E.pushDatatype env n' xncs
+
+ val t = (L'.CNamed n', loc)
+ val env = foldl (fn ((x, n, to), env) =>
+ let
+ val t = case to of
+ NONE => t
+ | SOME t' => (L'.TFun (t', t), loc)
+ in
+ E.pushENamedAs env x n t
+ end) env xncs
+ in
+ ([(L'.SgiDatatypeImp (x, n', n, ms, s), loc)], (env, denv, []))
+ end
+ end)
| L.SgiVal (x, c) =>
let
@@ -1501,6 +1541,8 @@ fun selfify env {str, strs, sgn} =
| L'.SgnConst sgis =>
(L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) =>
(L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)
+ | (L'.SgiDatatype (x, n, xncs), loc) =>
+ (L'.SgiDatatypeImp (x, n, str, strs, x), loc)
| (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)
@@ -1745,7 +1787,35 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
end
| _ => NONE)
- | L'.SgiDatatypeImp _ => raise Fail "SgiDatatypeImp in subsgn"
+ | L'.SgiDatatypeImp (x, n2, m11, ms1, s1) =>
+ seek (fn sgi1All as (sgi1, _) =>
+ case sgi1 of
+ L'.SgiDatatypeImp (x', n1, m12, ms2, s2) =>
+ if x = x' then
+ let
+ val k = (L'.KType, loc)
+ val t1 = (L'.CModProj (m11, ms1, s1), loc)
+ val t2 = (L'.CModProj (m12, ms2, s2), loc)
+
+ fun good () =
+ let
+ val env = E.pushCNamedAs env x n1 k (SOME t1)
+ val env = E.pushCNamedAs env x n2 k (SOME t2)
+ in
+ SOME (env, denv)
+ end
+ in
+ (case unifyCons (env, denv) t1 t2 of
+ [] => good ()
+ | _ => NONE)
+ handle CUnify (c1, c2, err) =>
+ (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
+ good ())
+ end
+ else
+ NONE
+
+ | _ => NONE)
| L'.SgiVal (x, n2, c2) =>
seek (fn sgi1All as (sgi1, _) =>
@@ -1904,28 +1974,32 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
| SOME sgn => ((L'.StrProj (str, m), loc), sgn))
((L'.StrVar n, loc), sgn) ms
in
- case E.projectDatatype env {sgn = sgn, str = str, field = s} of
- NONE => (conError env (UnboundDatatype (loc, s));
- ([], (env, denv, gs)))
- | SOME xncs =>
- let
- val k = (L'.KType, loc)
- val t = (L'.CModProj (n, ms, s), loc)
- val (env, n') = E.pushCNamed env x k (SOME t)
- val env = E.pushDatatype env n' xncs
-
- val t = (L'.CNamed n', loc)
- val env = foldl (fn ((x, n, to), env) =>
- let
- val t = case to of
- NONE => t
- | SOME t' => (L'.TFun (t', t), loc)
- in
- E.pushENamedAs env x n t
- end) env xncs
- in
- ([(L'.DDatatypeImp (x, n', n, ms, s), loc)], (env, denv, []))
- end
+ case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of
+ ((L'.CModProj (n, ms, s), _), gs) =>
+ (case E.projectDatatype env {sgn = sgn, str = str, field = s} of
+ NONE => (conError env (UnboundDatatype (loc, s));
+ ([], (env, denv, gs)))
+ | SOME xncs =>
+ let
+ val k = (L'.KType, loc)
+ val t = (L'.CModProj (n, ms, s), loc)
+ val (env, n') = E.pushCNamed env x k (SOME t)
+ val env = E.pushDatatype env n' xncs
+
+ val t = (L'.CNamed n', loc)
+ val env = foldl (fn ((x, n, to), env) =>
+ let
+ val t = case to of
+ NONE => t
+ | SOME t' => (L'.TFun (t', t), loc)
+ in
+ E.pushENamedAs env x n t
+ end) env xncs
+ in
+ ([(L'.DDatatypeImp (x, n', n, ms, s), loc)], (env, denv, gs))
+ end)
+ | _ => (strError env (NotDatatype loc);
+ ([], (env, denv, [])))
end)
| L.DVal (x, co, e) =>
@@ -2035,7 +2109,7 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
val (str', actual, gs2) = elabStr (env, denv) str
in
- subSgn (env, denv) actual formal;
+ subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal;
(str', formal, gs1 @ gs2)
end
diff --git a/tests/datatypeMod.lac b/tests/datatypeMod.lac
index 558275c8..e6e321f4 100644
--- a/tests/datatypeMod.lac
+++ b/tests/datatypeMod.lac
@@ -2,7 +2,15 @@ structure M : sig datatype t = A | B end = struct
datatype t = A | B
end
+val a = M.A
+
datatype u = datatype M.t
val a : M.t = A
val a2 : u = a
+
+structure M2 = M
+structure M3 : sig datatype t = datatype M.t end = M2
+structure M4 : sig datatype t = datatype M.t end = M
+
+val b : M3.t = M4.B
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-15 05:32:55 +0000