# HG changeset patch # User Adam Chlipala # Date 1213735134 14400 # Node ID 44b5405e74c7fcc655eb17f5d669ad70e319ceba # Parent 535c324f0b35784784858474f0126ca7101b6856 Elaborating module projection diff -r 535c324f0b35 -r 44b5405e74c7 src/corify.sml --- a/src/corify.sml Thu Jun 12 17:41:32 2008 -0400 +++ b/src/corify.sml Tue Jun 17 16:38:54 2008 -0400 @@ -50,6 +50,8 @@ | 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 @@ 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 -r 535c324f0b35 -r 44b5405e74c7 src/elab.sml --- a/src/elab.sml Thu Jun 12 17:41:32 2008 -0400 +++ b/src/elab.sml Tue Jun 17 16:38:54 2008 -0400 @@ -51,6 +51,7 @@ | 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 @@ 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 @@ and str' = StrConst of decl list | StrVar of int + | StrProj of str * string | StrError withtype decl = decl' located diff -r 535c324f0b35 -r 44b5405e74c7 src/elab_env.sig --- a/src/elab_env.sig Thu Jun 12 17:41:32 2008 -0400 +++ b/src/elab_env.sig Tue Jun 17 16:38:54 2008 -0400 @@ -76,4 +76,8 @@ 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 -r 535c324f0b35 -r 44b5405e74c7 src/elab_env.sml --- a/src/elab_env.sml Thu Jun 12 17:41:32 2008 -0400 +++ b/src/elab_env.sml Tue Jun 17 16:38:54 2008 -0400 @@ -298,6 +298,113 @@ | 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 -r 535c324f0b35 -r 44b5405e74c7 src/elab_print.sml --- a/src/elab_print.sml Thu Jun 12 17:41:32 2008 -0400 +++ b/src/elab_print.sml Tue Jun 17 16:38:54 2008 -0400 @@ -93,10 +93,22 @@ 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 @@ 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 @@ newline, string "end"] | StrVar n => string (#1 (E.lookupStrNamed env n)) + | StrProj (str, s) => box [p_str env str, + string ".", + string s] | StrError => string "" and p_file env file = diff -r 535c324f0b35 -r 44b5405e74c7 src/elab_util.sig --- a/src/elab_util.sig Thu Jun 12 17:41:32 2008 -0400 +++ b/src/elab_util.sig Tue Jun 17 16:38:54 2008 -0400 @@ -50,6 +50,9 @@ 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 @@ 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 -r 535c324f0b35 -r 44b5405e74c7 src/elab_util.sml --- a/src/elab_util.sml Thu Jun 12 17:41:32 2008 -0400 +++ b/src/elab_util.sml Tue Jun 17 16:38:54 2008 -0400 @@ -109,6 +109,7 @@ | 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 @@ 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 @@ 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 @@ 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 -r 535c324f0b35 -r 44b5405e74c7 src/elaborate.sml --- a/src/elaborate.sml Thu Jun 12 17:41:32 2008 -0400 +++ b/src/elaborate.sml Tue Jun 17 16:38:54 2008 -0400 @@ -108,12 +108,15 @@ 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 @@ ((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 @@ ((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 @@ | 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 @@ 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 @@ (_, _, 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ 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 @@ (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 -r 535c324f0b35 -r 44b5405e74c7 src/lacweb.grm --- a/src/lacweb.grm Thu Jun 12 17:41:32 2008 -0400 +++ b/src/lacweb.grm Tue Jun 17 16:38:54 2008 -0400 @@ -60,6 +60,9 @@ | 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 @@ | 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 @@ 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 @@ | 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 @@ | 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 @@ 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 -r 535c324f0b35 -r 44b5405e74c7 src/list_util.sig --- a/src/list_util.sig Thu Jun 12 17:41:32 2008 -0400 +++ b/src/list_util.sig Tue Jun 17 16:38:54 2008 -0400 @@ -29,6 +29,8 @@ 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 -r 535c324f0b35 -r 44b5405e74c7 src/list_util.sml --- a/src/list_util.sml Thu Jun 12 17:41:32 2008 -0400 +++ b/src/list_util.sml Tue Jun 17 16:38:54 2008 -0400 @@ -45,6 +45,26 @@ 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 -r 535c324f0b35 -r 44b5405e74c7 src/source.sml --- a/src/source.sml Thu Jun 12 17:41:32 2008 -0400 +++ b/src/source.sml Tue Jun 17 16:38:54 2008 -0400 @@ -49,7 +49,7 @@ | 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,21 +62,6 @@ withtype con = con' located -datatype exp' = - EAnnot of exp * con - - | EPrim of Prim.t - | EVar of string - | EApp of exp * exp - | EAbs of string * con option * exp - | ECApp of exp * con - | ECAbs of explicitness * string * kind * exp - - | ERecord of (con * exp) list - | EField of exp * con - -withtype exp = exp' located - datatype sgn_item' = SgiConAbs of string * kind | SgiCon of string * kind option * con @@ -90,6 +75,21 @@ withtype sgn_item = sgn_item' located and sgn = sgn' located +datatype exp' = + EAnnot of exp * con + + | EPrim of Prim.t + | EVar of string list * string + | EApp of exp * exp + | EAbs of string * con option * exp + | ECApp of exp * con + | ECAbs of explicitness * string * kind * exp + + | ERecord of (con * exp) list + | EField of exp * con + +withtype exp = exp' located + datatype decl' = DCon of string * kind option * con | DVal of string * con option * exp @@ -99,6 +99,7 @@ and str' = StrConst of decl list | StrVar of string + | StrProj of str * string withtype decl = decl' located and str = str' located diff -r 535c324f0b35 -r 44b5405e74c7 src/source_print.sml --- a/src/source_print.sml Thu Jun 12 17:41:32 2008 -0400 +++ b/src/source_print.sml Tue Jun 17 16:38:54 2008 -0400 @@ -88,7 +88,7 @@ | 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 @@ 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 @@ 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 -r 535c324f0b35 -r 44b5405e74c7 tests/modproj.lac --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/modproj.lac Tue Jun 17 16:38:54 2008 -0400 @@ -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