summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/corify.sml3
-rw-r--r--src/elab.sml3
-rw-r--r--src/elab_env.sig4
-rw-r--r--src/elab_env.sml107
-rw-r--r--src/elab_print.sml35
-rw-r--r--src/elab_util.sig31
-rw-r--r--src/elab_util.sml97
-rw-r--r--src/elaborate.sml112
-rw-r--r--src/lacweb.grm17
-rw-r--r--src/list_util.sig2
-rw-r--r--src/list_util.sml20
-rw-r--r--src/source.sml31
-rw-r--r--src/source_print.sml7
-rw-r--r--tests/modproj.lac11
14 files changed, 451 insertions, 29 deletions
diff --git a/src/corify.sml b/src/corify.sml
index a5309dec..61634a5d 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -50,6 +50,8 @@ fun corifyCon (c, loc) =
| L.CRel n => (L'.CRel n, loc)
| L.CNamed n => (L'.CNamed n, loc)
+ | L.CModProj _ => raise Fail "Corify CModProj"
+
| L.CApp (c1, c2) => (L'.CApp (corifyCon c1, corifyCon c2), loc)
| L.CAbs (x, k, c) => (L'.CAbs (x, corifyKind k, corifyCon c), loc)
@@ -67,6 +69,7 @@ fun corifyExp (e, loc) =
L.EPrim p => (L'.EPrim p, loc)
| L.ERel n => (L'.ERel n, loc)
| L.ENamed n => (L'.ENamed n, loc)
+ | L.EModProj _ => raise Fail "Corify EModProj"
| L.EApp (e1, e2) => (L'.EApp (corifyExp e1, corifyExp e2), loc)
| L.EAbs (x, dom, ran, e1) => (L'.EAbs (x, corifyCon dom, corifyCon ran, corifyExp e1), loc)
| L.ECApp (e1, c) => (L'.ECApp (corifyExp e1, corifyCon c), loc)
diff --git a/src/elab.sml b/src/elab.sml
index 14664c0f..da64febf 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -51,6 +51,7 @@ datatype con' =
| CRel of int
| CNamed of int
+ | CModProj of int * string list * string
| CApp of con * con
| CAbs of string * kind * con
@@ -68,6 +69,7 @@ datatype exp' =
EPrim of Prim.t
| ERel of int
| ENamed of int
+ | EModProj of int * string list * string
| EApp of exp * exp
| EAbs of string * con * con * exp
| ECApp of exp * con
@@ -103,6 +105,7 @@ datatype decl' =
and str' =
StrConst of decl list
| StrVar of int
+ | StrProj of str * string
| StrError
withtype decl = decl' located
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 05badecf..89d5fb60 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -76,4 +76,8 @@ signature ELAB_ENV = sig
val declBinds : env -> Elab.decl -> env
val sgiBinds : env -> Elab.sgn_item -> env
+ val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option
+ val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option
+ val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option
+
end
diff --git a/src/elab_env.sml b/src/elab_env.sml
index fd078e05..b10882a7 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -298,6 +298,113 @@ fun sgiBinds env (sgi, _) =
| SgiVal (x, n, t) => pushENamedAs env x n t
| SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn
+fun sgnSeek f sgis =
+ let
+ fun seek (sgis, strs, cons) =
+ case sgis of
+ [] => NONE
+ | (sgi, _) :: sgis =>
+ case f sgi of
+ SOME v => SOME (v, (strs, cons))
+ | NONE =>
+ case sgi of
+ SgiConAbs (x, n, _) => seek (sgis, strs, IM.insert (cons, n, x))
+ | SgiCon (x, n, _, _) => seek (sgis, strs, IM.insert (cons, n, x))
+ | SgiVal _ => seek (sgis, strs, cons)
+ | SgiStr (x, n, _) => seek (sgis, IM.insert (strs, n, x), cons)
+ in
+ seek (sgis, IM.empty, IM.empty)
+ end
+
+fun id x = x
+
+fun unravelStr (str, _) =
+ case str of
+ StrVar x => (x, [])
+ | StrProj (str, m) =>
+ let
+ val (x, ms) = unravelStr str
+ in
+ (x, ms @ [m])
+ end
+ | _ => raise Fail "unravelStr"
+
+fun sgnS_con (str, (strs, cons)) c =
+ case c of
+ CModProj (m1, ms, x) =>
+ (case IM.find (strs, m1) of
+ NONE => c
+ | SOME m1x =>
+ let
+ val (m1, ms') = unravelStr str
+ in
+ CModProj (m1, ms' @ m1x :: ms, x)
+ end)
+ | CNamed n =>
+ (case IM.find (cons, n) of
+ NONE => c
+ | SOME nx =>
+ let
+ val (m1, ms) = unravelStr str
+ in
+ CModProj (m1, ms, nx)
+ end)
+ | _ => c
+
+fun sgnSubCon (str, (strs, cons)) =
+ ElabUtil.Con.map {kind = id,
+ con = sgnS_con (str, (strs, cons))}
+
+fun sgnSubSgn (str, (strs, cons)) =
+ ElabUtil.Sgn.map {kind = id,
+ con = sgnS_con (str, (strs, cons)),
+ sgn_item = id,
+ sgn = id}
+
+fun projectCon env {sgn = (sgn, _), str, field} =
+ case 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
+ | _ => NONE) sgis of
+ NONE => NONE
+ | SOME ((k, co), subs) => SOME (k, Option.map (sgnSubCon (str, subs)) co))
+ | SgnVar n =>
+ let
+ val (_, sgn) = lookupSgnNamed env n
+ in
+ projectCon env {sgn = sgn, str = str, field = field}
+ end
+ | SgnError => SOME ((KError, ErrorMsg.dummySpan), SOME (CError, ErrorMsg.dummySpan))
+
+fun projectVal env {sgn = (sgn, _), str, field} =
+ case sgn of
+ SgnConst sgis =>
+ (case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE | _ => NONE) sgis of
+ NONE => NONE
+ | SOME (c, subs) => SOME (sgnSubCon (str, subs) c))
+ | SgnVar n =>
+ let
+ val (_, sgn) = lookupSgnNamed env n
+ in
+ projectVal env {sgn = sgn, str = str, field = field}
+ end
+ | SgnError => SOME (CError, ErrorMsg.dummySpan)
+
+fun projectStr env {sgn = (sgn, _), str, field} =
+ case sgn of
+ SgnConst sgis =>
+ (case sgnSeek (fn SgiStr (x, _, sgn) => if x = field then SOME sgn else NONE | _ => NONE) sgis of
+ NONE => NONE
+ | SOME (sgn, subs) => SOME (sgnSubSgn (str, subs) sgn))
+ | SgnVar n =>
+ let
+ val (_, sgn) = lookupSgnNamed env n
+ in
+ projectStr env {sgn = sgn, str = str, field = field}
+ end
+ | SgnError => SOME (SgnError, ErrorMsg.dummySpan)
+
val ktype = (KType, ErrorMsg.dummySpan)
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 435ea13d..b214d5d4 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -93,10 +93,22 @@ fun p_con' par env (c, _) =
else
string (#1 (E.lookupCRel env n))
| CNamed n =>
- if !debug then
- string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n)
- else
- string (#1 (E.lookupCNamed env n))
+ ((if !debug then
+ string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n)
+ else
+ string (#1 (E.lookupCNamed env n)))
+ handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n))
+ | CModProj (m1, ms, x) =>
+ let
+ val (m1x, sgn) = E.lookupStrNamed env m1
+
+ val m1s = if !debug then
+ m1x ^ "__" ^ Int.toString m1
+ else
+ m1x
+ in
+ p_list_sep (string ".") string (m1x :: ms @ [x])
+ end
| CApp (c1, c2) => parenIf par (box [p_con env c1,
space,
@@ -167,6 +179,18 @@ fun p_exp' par env (e, _) =
string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n)
else
string (#1 (E.lookupENamed env n))
+ | EModProj (m1, ms, x) =>
+ let
+ val (m1x, sgn) = E.lookupStrNamed env m1
+
+ val m1s = if !debug then
+ m1x ^ "__" ^ Int.toString m1
+ else
+ m1x
+ in
+ p_list_sep (string ".") string (m1x :: ms @ [x])
+ end
+
| EApp (e1, e2) => parenIf par (box [p_exp env e1,
space,
p_exp' true env e2])
@@ -340,6 +364,9 @@ and p_str env (str, _) =
newline,
string "end"]
| StrVar n => string (#1 (E.lookupStrNamed env n))
+ | StrProj (str, s) => box [p_str env str,
+ string ".",
+ string s]
| StrError => string "<ERROR>"
and p_file env file =
diff --git a/src/elab_util.sig b/src/elab_util.sig
index 80d04465..0917d126 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -50,6 +50,9 @@ structure Con : sig
con : 'context -> Elab.con' -> Elab.con',
bind : 'context * binder -> 'context}
-> 'context -> (Elab.con -> Elab.con)
+ val map : {kind : Elab.kind' -> Elab.kind',
+ con : Elab.con' -> Elab.con'}
+ -> Elab.con -> Elab.con
val exists : {kind : Elab.kind' -> bool,
con : Elab.con' -> bool} -> Elab.con -> bool
end
@@ -75,4 +78,32 @@ structure Exp : sig
exp : Elab.exp' -> bool} -> Elab.exp -> bool
end
+structure Sgn : sig
+ datatype binder =
+ RelC of string * Elab.kind
+ | NamedC of string * Elab.kind
+ | Str of string * Elab.sgn
+
+ val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+ con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
+ sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
+ sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB,
+ bind : 'context * binder -> 'context}
+ -> ('context, Elab.sgn, 'state, 'abort) Search.mapfolderB
+
+
+ val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+ con : (Elab.con', 'state, 'abort) Search.mapfolder,
+ sgn_item : (Elab.sgn_item', 'state, 'abort) Search.mapfolder,
+ sgn : (Elab.sgn', 'state, 'abort) Search.mapfolder}
+ -> (Elab.sgn, 'state, 'abort) Search.mapfolder
+
+ val map : {kind : Elab.kind' -> Elab.kind',
+ con : Elab.con' -> Elab.con',
+ sgn_item : Elab.sgn_item' -> Elab.sgn_item',
+ sgn : Elab.sgn' -> Elab.sgn'}
+ -> Elab.sgn -> Elab.sgn
+
+end
+
end
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 39020652..24e772d6 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -109,6 +109,7 @@ fun mapfoldB {kind = fk, con = fc, bind} =
| CRel _ => S.return2 cAll
| CNamed _ => S.return2 cAll
+ | CModProj _ => S.return2 cAll
| CApp (c1, c2) =>
S.bind2 (mfc ctx c1,
fn c1' =>
@@ -160,7 +161,13 @@ fun mapB {kind, con, bind} ctx c =
con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
bind = bind} ctx c () of
S.Continue (c, ()) => c
- | S.Return _ => raise Fail "Con.mapB: Impossible"
+ | S.Return _ => raise Fail "ElabUtil.Con.mapB: Impossible"
+
+fun map {kind, con} s =
+ case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
+ con = fn c => fn () => S.Continue (con c, ())} s () of
+ S.Return () => raise Fail "ElabUtil.Con.map: Impossible"
+ | S.Continue (s, ()) => s
fun exists {kind, con} k =
case mapfold {kind = fn k => fn () =>
@@ -208,6 +215,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
EPrim _ => S.return2 eAll
| ERel _ => S.return2 eAll
| ENamed _ => S.return2 eAll
+ | EModProj _ => S.return2 eAll
| EApp (e1, e2) =>
S.bind2 (mfe ctx e1,
fn e1' =>
@@ -291,4 +299,91 @@ fun exists {kind, con, exp} k =
end
+structure Sgn = struct
+
+datatype binder =
+ RelC of string * Elab.kind
+ | NamedC of string * Elab.kind
+ | Str of string * Elab.sgn
+
+fun mapfoldB {kind, con, sgn_item, sgn, bind} =
+ let
+ fun bind' (ctx, b) =
+ let
+ val b' = case b of
+ Con.Rel x => RelC x
+ | Con.Named x => NamedC x
+ in
+ bind (ctx, b')
+ end
+ val con = Con.mapfoldB {kind = kind, con = con, bind = bind'}
+
+ val kind = Kind.mapfold kind
+
+ fun sgi ctx si acc =
+ S.bindP (sgi' ctx si acc, sgn_item ctx)
+
+ and sgi' ctx (si, loc) =
+ case si of
+ SgiConAbs (x, n, k) =>
+ S.map2 (kind k,
+ fn k' =>
+ (SgiConAbs (x, n, k'), loc))
+ | SgiCon (x, n, k, c) =>
+ S.bind2 (kind k,
+ fn k' =>
+ S.map2 (con ctx c,
+ fn c' =>
+ (SgiCon (x, n, k', c'), loc)))
+ | SgiVal (x, n, c) =>
+ S.map2 (con ctx c,
+ fn c' =>
+ (SgiVal (x, n, c'), loc))
+ | SgiStr (x, n, s) =>
+ S.map2 (sg ctx s,
+ fn s' =>
+ (SgiStr (x, n, s'), loc))
+
+ and sg ctx s acc =
+ S.bindP (sg' ctx s acc, sgn ctx)
+
+ and sg' ctx (sAll as (s, loc)) =
+ case s of
+ SgnConst sgis =>
+ S.map2 (ListUtil.mapfoldB (fn (ctx, si) =>
+ (case #1 si of
+ SgiConAbs (x, _, k) =>
+ bind (ctx, NamedC (x, k))
+ | SgiCon (x, _, k, _) =>
+ bind (ctx, NamedC (x, k))
+ | SgiVal _ => ctx
+ | SgiStr (x, _, sgn) =>
+ bind (ctx, Str (x, sgn)),
+ sgi ctx si)) ctx sgis,
+ fn sgis' =>
+ (SgnConst sgis', loc))
+
+ | SgnVar _ => S.return2 sAll
+ | SgnError => S.return2 sAll
+ in
+ sg
+ end
+
+fun mapfold {kind, con, sgn_item, sgn} =
+ mapfoldB {kind = kind,
+ con = fn () => con,
+ sgn_item = fn () => sgn_item,
+ sgn = fn () => sgn,
+ bind = fn ((), _) => ()} ()
+
+fun map {kind, con, sgn_item, sgn} s =
+ case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
+ con = fn c => fn () => S.Continue (con c, ()),
+ sgn_item = fn si => fn () => S.Continue (sgn_item si, ()),
+ sgn = fn s => fn () => S.Continue (sgn s, ())} s () of
+ S.Return () => raise Fail "Elab_util.Sgn.map"
+ | S.Continue (s, ()) => s
+
+end
+
end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index b232a980..7cc510ec 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -108,12 +108,15 @@ fun unifyKinds k1 k2 =
datatype con_error =
UnboundCon of ErrorMsg.span * string
+ | UnboundStrInCon of ErrorMsg.span * string
| WrongKind of L'.con * L'.kind * L'.kind * kunify_error
fun conError env err =
case err of
UnboundCon (loc, s) =>
ErrorMsg.errorAt loc ("Unbound constructor variable " ^ s)
+ | UnboundStrInCon (loc, s) =>
+ ErrorMsg.errorAt loc ("Unbound structure " ^ s)
| WrongKind (c, k1, k2, kerr) =>
(ErrorMsg.errorAt (#2 c) "Wrong kind";
eprefaces' [("Constructor", p_con env c),
@@ -225,7 +228,7 @@ fun elabCon env (c, loc) =
((L'.TRecord c', loc), ktype)
end
- | L.CVar s =>
+ | L.CVar ([], s) =>
(case E.lookupC env s of
E.NotBound =>
(conError env (UnboundCon (loc, s));
@@ -234,6 +237,27 @@ fun elabCon env (c, loc) =
((L'.CRel n, loc), k)
| E.Named (n, k) =>
((L'.CNamed n, loc), k))
+ | L.CVar (m1 :: ms, s) =>
+ (case E.lookupStr env m1 of
+ NONE => (conError env (UnboundStrInCon (loc, s));
+ (cerror, kerror))
+ | 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
+
+ val k = case E.projectCon env {sgn = sgn, str = str, field = s} of
+ NONE => (conError env (UnboundCon (loc, s));
+ kerror)
+ | SOME (k, _) => k
+ in
+ ((L'.CModProj (n, ms, s), loc), k)
+ end)
+
| L.CApp (c1, c2) =>
let
val (c1', k1) = elabCon env c1
@@ -404,6 +428,20 @@ fun kindof env (c, loc) =
| L'.CRel xn => #2 (E.lookupCRel env xn)
| L'.CNamed xn => #2 (E.lookupCNamed env xn)
+ | L'.CModProj (n, ms, x) =>
+ let
+ val (_, sgn) = E.lookupStrNamed env n
+ val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+ case E.projectStr env {sgn = sgn, str = str, field = m} of
+ NONE => raise Fail "kindof: Unknown substructure"
+ | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+ ((L'.StrVar n, loc), sgn) ms
+ in
+ case E.projectCon env {sgn = sgn, str = str, field = x} of
+ NONE => raise Fail "kindof: Unknown con in structure"
+ | SOME (k, _) => k
+ end
+
| L'.CApp (c, _) =>
(case #1 (hnormKind (kindof env c)) of
L'.KArrow (_, k) => k
@@ -541,7 +579,7 @@ and unifySummaries env (k, s1 : record_summary, s2 : record_summary) =
pairOffUnifs (unifs1, unifs2)
end
-and hnormCon env (cAll as (c, _)) =
+and hnormCon env (cAll as (c, loc)) =
case c of
L'.CUnif (_, _, ref (SOME c)) => hnormCon env c
@@ -550,6 +588,21 @@ and hnormCon env (cAll as (c, _)) =
(_, _, SOME c') => hnormCon env c'
| _ => cAll)
+ | L'.CModProj (n, ms, x) =>
+ let
+ val (_, sgn) = E.lookupStrNamed env n
+ val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+ case E.projectStr env {sgn = sgn, str = str, field = m} of
+ NONE => raise Fail "hnormCon: Unknown substructure"
+ | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+ ((L'.StrVar n, loc), sgn) ms
+ in
+ case E.projectCon env {sgn = sgn, str = str, field = x} of
+ NONE => raise Fail "kindof: Unknown con in structure"
+ | SOME (_, NONE) => cAll
+ | SOME (_, SOME c) => hnormCon env c
+ end
+
| L'.CApp (c1, c2) =>
(case hnormCon env c1 of
(L'.CAbs (_, _, cb), _) =>
@@ -610,6 +663,12 @@ and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) =
else
err CIncompatible
+ | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) =>
+ if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then
+ ()
+ else
+ err CIncompatible
+
| (L'.CError, _) => ()
| (_, L'.CError) => ()
@@ -649,6 +708,7 @@ and unifyCons env c1 c2 =
datatype exp_error =
UnboundExp of ErrorMsg.span * string
+ | UnboundStrInExp of ErrorMsg.span * string
| Unify of L'.exp * L'.con * L'.con * cunify_error
| Unif of string * L'.con
| WrongForm of string * L'.exp * L'.con
@@ -657,6 +717,8 @@ fun expError env err =
case err of
UnboundExp (loc, s) =>
ErrorMsg.errorAt loc ("Unbound expression variable " ^ s)
+ | UnboundStrInExp (loc, s) =>
+ ErrorMsg.errorAt loc ("Unbound structure " ^ s)
| Unify (e, c1, c2, uerr) =>
(ErrorMsg.errorAt (#2 e) "Unification failure";
eprefaces' [("Expression", p_exp env e),
@@ -695,6 +757,20 @@ fun typeof env (e, loc) =
L'.EPrim p => (primType env p, loc)
| L'.ERel n => #2 (E.lookupERel env n)
| L'.ENamed n => #2 (E.lookupENamed env n)
+ | L'.EModProj (n, ms, x) =>
+ let
+ val (_, sgn) = E.lookupStrNamed env n
+ val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+ case E.projectStr env {sgn = sgn, str = str, field = m} of
+ NONE => raise Fail "kindof: Unknown substructure"
+ | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+ ((L'.StrVar n, loc), sgn) ms
+ in
+ case E.projectVal env {sgn = sgn, str = str, field = x} of
+ NONE => raise Fail "typeof: Unknown val in structure"
+ | SOME t => t
+ end
+
| L'.EApp (e1, _) =>
(case #1 (typeof env e1) of
L'.TFun (_, c) => c
@@ -739,13 +815,34 @@ fun elabExp env (e, loc) =
end
| L.EPrim p => ((L'.EPrim p, loc), (primType env p, loc))
- | L.EVar s =>
+ | L.EVar ([], s) =>
(case E.lookupE env s of
E.NotBound =>
(expError env (UnboundExp (loc, s));
(eerror, cerror))
| E.Rel (n, t) => ((L'.ERel n, loc), t)
| E.Named (n, t) => ((L'.ENamed n, loc), t))
+ | L.EVar (m1 :: ms, s) =>
+ (case E.lookupStr env m1 of
+ NONE => (expError env (UnboundStrInExp (loc, s));
+ (eerror, cerror))
+ | 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
+
+ val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
+ NONE => (expError env (UnboundExp (loc, s));
+ cerror)
+ | SOME t => t
+ in
+ ((L'.EModProj (n, ms, s), loc), t)
+ end)
+
| L.EApp (e1, e2) =>
let
val (e1', t1) = elabExp env e1
@@ -1209,6 +1306,15 @@ and elabStr env (str, loc) =
(strError env (UnboundStr (loc, x));
(strerror, sgnerror))
| SOME (n, sgn) => ((L'.StrVar n, loc), sgn))
+ | L.StrProj (str, x) =>
+ let
+ val (str', sgn) = elabStr env str
+ in
+ case E.projectStr env {str = str', sgn = sgn, field = x} of
+ NONE => (strError env (UnboundStr (loc, x));
+ (strerror, sgnerror))
+ | SOME sgn => ((L'.StrProj (str', x), loc), sgn)
+ end
val elabFile = ListUtil.foldlMap elabDecl
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 0c708699..f8f54fca 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -60,6 +60,9 @@ val s = ErrorMsg.spanOf
| kind of kind
| kcolon of explicitness
+ | path of string list * string
+ | spath of str
+
| cexp of con
| capps of con
| cterm of con
@@ -126,7 +129,10 @@ sgis : ([])
| sgi sgis (sgi :: sgis)
str : STRUCT decls END (StrConst decls, s (STRUCTleft, ENDright))
- | CSYMBOL (StrVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
+ | spath (spath)
+
+spath : CSYMBOL (StrVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
+ | spath DOT CSYMBOL (StrProj (spath, CSYMBOL), s (spathleft, CSYMBOLright))
kind : TYPE (KType, s (TYPEleft, TYPEright))
| NAME (KName, s (NAMEleft, NAMEright))
@@ -153,6 +159,9 @@ cexp : capps (capps)
kcolon : DCOLON (Explicit)
| TCOLON (Implicit)
+path : SYMBOL ([], SYMBOL)
+ | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end)
+
cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright))
| LBRACK rcon RBRACK (CRecord rcon, s (LBRACKleft, RBRACKright))
| LBRACE rcone RBRACE (TRecord (CRecord rcone, s (LBRACEleft, RBRACEright)),
@@ -160,7 +169,7 @@ cterm : LPAREN cexp RPAREN (#1 cexp, s (LPARENleft, RPARENright))
| DOLLAR cterm (TRecord cterm, s (DOLLARleft, ctermright))
| HASH CSYMBOL (CName CSYMBOL, s (HASHleft, CSYMBOLright))
- | SYMBOL (CVar SYMBOL, s (SYMBOLleft, SYMBOLright))
+ | path (CVar path, s (pathleft, pathright))
| UNDER (CWild (KWild, s (UNDERleft, UNDERright)), s (UNDERleft, UNDERright))
rcon : ([])
@@ -172,7 +181,7 @@ rcone : ([])
| ident COLON cexp COMMA rcone ((ident, cexp) :: rcone)
ident : CSYMBOL (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright))
- | SYMBOL (CVar SYMBOL, s (SYMBOLleft, SYMBOLright))
+ | SYMBOL (CVar ([], SYMBOL), s (SYMBOLleft, SYMBOLright))
eapps : eterm (eterm)
| eapps eterm (EApp (eapps, eterm), s (eappsleft, etermright))
@@ -188,7 +197,7 @@ eexp : eapps (eapps)
eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
- | SYMBOL (EVar SYMBOL, s (SYMBOLleft, SYMBOLright))
+ | path (EVar path, s (pathleft, pathright))
| LBRACE rexp RBRACE (ERecord rexp, s (LBRACEleft, RBRACEright))
| INT (EPrim (Prim.Int INT), s (INTleft, INTright))
diff --git a/src/list_util.sig b/src/list_util.sig
index 62013d25..76d08d23 100644
--- a/src/list_util.sig
+++ b/src/list_util.sig
@@ -29,6 +29,8 @@ signature LIST_UTIL = sig
val mapfold : ('data, 'state, 'abort) Search.mapfolder
-> ('data list, 'state, 'abort) Search.mapfolder
+ val mapfoldB : ('context * 'data -> 'context * ('state -> ('data * 'state, 'abort) Search.result))
+ -> ('context, 'data list, 'state, 'abort) Search.mapfolderB
val foldlMap : ('data1 * 'state -> 'data2 * 'state) -> 'state -> 'data1 list -> 'data2 list * 'state
diff --git a/src/list_util.sml b/src/list_util.sml
index 7d3f8333..e3d8515e 100644
--- a/src/list_util.sml
+++ b/src/list_util.sml
@@ -45,6 +45,26 @@ fun mapfold f =
mf
end
+fun mapfoldB f =
+ let
+ fun mf ctx ls s =
+ case ls of
+ nil => S.Continue (nil, s)
+ | h :: t =>
+ let
+ val (ctx, r) = f (ctx, h)
+ in
+ case r s of
+ S.Return x => S.Return x
+ | S.Continue (h', s) =>
+ case mf ctx t s of
+ S.Return x => S.Return x
+ | S.Continue (t', s) => S.Continue (h' :: t', s)
+ end
+ in
+ mf
+ end
+
fun foldlMap f s =
let
fun fm (ls', s) ls =
diff --git a/src/source.sml b/src/source.sml
index 6fe07255..a7ff04c6 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -49,7 +49,7 @@ datatype con' =
| TCFun of explicitness * string * kind * con
| TRecord of con
- | CVar of string
+ | CVar of string list * string
| CApp of con * con
| CAbs of string * kind * con
@@ -62,11 +62,24 @@ datatype con' =
withtype con = con' located
+datatype sgn_item' =
+ SgiConAbs of string * kind
+ | SgiCon of string * kind option * con
+ | SgiVal of string * con
+ | SgiStr of string * sgn
+
+and sgn' =
+ SgnConst of sgn_item list
+ | SgnVar of string
+
+withtype sgn_item = sgn_item' located
+and sgn = sgn' located
+
datatype exp' =
EAnnot of exp * con
| EPrim of Prim.t
- | EVar of string
+ | EVar of string list * string
| EApp of exp * exp
| EAbs of string * con option * exp
| ECApp of exp * con
@@ -77,19 +90,6 @@ datatype exp' =
withtype exp = exp' located
-datatype sgn_item' =
- SgiConAbs of string * kind
- | SgiCon of string * kind option * con
- | SgiVal of string * con
- | SgiStr of string * sgn
-
-and sgn' =
- SgnConst of sgn_item list
- | SgnVar of string
-
-withtype sgn_item = sgn_item' located
-and sgn = sgn' located
-
datatype decl' =
DCon of string * kind option * con
| DVal of string * con option * exp
@@ -99,6 +99,7 @@ datatype decl' =
and str' =
StrConst of decl list
| StrVar of string
+ | StrProj of str * string
withtype decl = decl' located
and str = str' located
diff --git a/src/source_print.sml b/src/source_print.sml
index 5a2412a9..2005d09f 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -88,7 +88,7 @@ fun p_con' par (c, _) =
| TRecord c => box [string "$",
p_con' true c]
- | CVar s => string s
+ | CVar (ss, s) => p_list_sep (string ".") string (ss @ [s])
| CApp (c1, c2) => parenIf par (box [p_con c1,
space,
p_con' true c2])
@@ -143,7 +143,7 @@ fun p_exp' par (e, _) =
string ")"]
| EPrim p => Prim.p_t p
- | EVar s => string s
+ | EVar (ss, s) => p_list_sep (string ".") string (ss @ [s])
| EApp (e1, e2) => parenIf par (box [p_exp e1,
space,
p_exp' true e2])
@@ -321,6 +321,9 @@ and p_str (str, _) =
newline,
string "end"]
| StrVar x => string x
+ | StrProj (str, x) => box [p_str str,
+ string ".",
+ string x]
val p_file = p_list_sep newline p_decl
diff --git a/tests/modproj.lac b/tests/modproj.lac
new file mode 100644
index 00000000..ef2364d1
--- /dev/null
+++ b/tests/modproj.lac
@@ -0,0 +1,11 @@
+signature S = sig
+ type t
+ val zero : t
+end
+structure S : S = struct
+ type t = int
+ val zero = 0
+end
+
+type t = S.t
+val zero : t = S.zero
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-22 05:40:52 +0000