Mercurial > urweb
changeset 162:06a98129b23f
Add datatype import constructor annotations; datatypes through explify
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 29 Jul 2008 12:30:04 -0400 |
| parents | a5ae7b3e37a4 |
| children | 80192edca30d |
| files | src/corify.sml src/elab.sml src/elab_env.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/expl.sml src/expl_env.sml src/expl_print.sml src/expl_util.sml src/explify.sml |
| diffstat | 11 files changed, 221 insertions(+), 122 deletions(-) [+] |
line wrap: on
line diff
--- a/src/corify.sml Thu Jul 24 16:51:24 2008 -0400 +++ b/src/corify.sml Tue Jul 29 12:30:04 2008 -0400 @@ -384,6 +384,8 @@ in ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) end + | L.DDatatype _ => raise Fail "Corify DDatatype" + | L.DDatatypeImp _ => raise Fail "Corify DDatatypeImp" | L.DVal (x, n, t, e) => let val (st, n) = St.bindVal st x n @@ -568,6 +570,8 @@ fun maxName ds = foldl (fn ((d, _), n) => case d of L.DCon (_, n', _, _) => Int.max (n, n') + | L.DDatatype (_, n', _) => Int.max (n, n') + | L.DDatatypeImp (_, n', _, _, _, _) => Int.max (n, n') | L.DVal (_, n', _, _) => Int.max (n, n') | L.DValRec vis => foldl (fn ((_, n', _, _), n) => Int.max (n, n)) n vis | L.DSgn (_, n', _) => Int.max (n, n')
--- a/src/elab.sml Thu Jul 24 16:51:24 2008 -0400 +++ b/src/elab.sml Tue Jul 29 12:30:04 2008 -0400 @@ -94,7 +94,7 @@ SgiConAbs of string * int * kind | SgiCon of string * int * kind * con | SgiDatatype of string * int * (string * int * con option) list - | SgiDatatypeImp of string * int * int * string list * string + | SgiDatatypeImp of string * int * int * string list * string * (string * int * con option) list | SgiVal of string * int * con | SgiStr of string * int * sgn | SgiSgn of string * int * sgn @@ -114,7 +114,7 @@ datatype decl' = DCon of string * int * kind * con | DDatatype of string * int * (string * int * con option) list - | DDatatypeImp of string * int * int * string list * string + | DDatatypeImp of string * int * int * string list * string * (string * int * con option) list | DVal of string * int * con * exp | DValRec of (string * int * con * exp) list | DSgn of string * int * sgn
--- a/src/elab_env.sml Thu Jul 24 16:51:24 2008 -0400 +++ b/src/elab_env.sml Tue Jul 29 12:30:04 2008 -0400 @@ -353,7 +353,14 @@ | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc)) env xncs end - | SgiDatatypeImp (x, n, m1, ms, x') => pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc)) + | SgiDatatypeImp (x, n, m1, ms, x', xncs) => + let + val env = pushCNamedAs env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc)) + in + foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' (CNamed n, loc) + | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc)) + env xncs + end | SgiVal (x, n, t) => pushENamedAs env x n t | SgiStr (x, n, sgn) => pushStrNamedAs env x n sgn | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn @@ -371,7 +378,7 @@ val cons = case sgi of SgiDatatype (x, n, _) => IM.insert (cons, n, x) - | SgiDatatypeImp (x, n, _, _, _) => IM.insert (cons, n, x) + | SgiDatatypeImp (x, n, _, _, _, _) => IM.insert (cons, n, x) | _ => cons in SOME (v, (sgns, strs, cons)) @@ -381,7 +388,7 @@ SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) - | SgiDatatypeImp (x, n, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) + | SgiDatatypeImp (x, n, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x)) | SgiVal _ => seek (sgis, sgns, strs, cons) | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons) | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons) @@ -529,7 +536,7 @@ (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') => + | SgiDatatypeImp (x, _, m1, ms, x', _) => if x = field then SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn)) else @@ -544,15 +551,7 @@ 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 + | SgiDatatypeImp (x, _, _, _, _, xncs) => if x = field then SOME xncs 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)) @@ -561,33 +560,23 @@ 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 - | 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)) + let + fun seek (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 + in + case sgnSeek (fn SgiVal (x, _, c) => if x = field then SOME c else NONE + | SgiDatatype (_, n, xncs) => seek (n, xncs) + | SgiDatatypeImp (_, n, _, _, _, xncs) => seek (n, xncs) + | _ => NONE) sgis of + NONE => NONE + | SOME (c, subs) => SOME (sgnSubCon (str, subs) c) + end | SgnError => SOME (CError, ErrorMsg.dummySpan) | _ => NONE @@ -607,7 +596,7 @@ | SgiConAbs (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) | SgiCon (x, n, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) | SgiDatatype (x, n, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) - | SgiDatatypeImp (x, n, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) + | SgiDatatypeImp (x, n, _, _, _, _) => seek (sgis, sgns, strs, IM.insert (cons, n, x), acc) | SgiVal _ => seek (sgis, sgns, strs, cons, acc) | SgiSgn (x, n, _) => seek (sgis, IM.insert (sgns, n, x), strs, cons, acc) | SgiStr (x, n, _) => seek (sgis, sgns, IM.insert (strs, n, x), cons, acc) @@ -632,19 +621,10 @@ | ((x', n', SOME t), env) => pushENamedAs env x' n' (TFun (t, (CNamed n, loc)), loc)) env xncs end - | DDatatypeImp (x, n, m, ms, x') => + | DDatatypeImp (x, n, m, ms, x', xncs) => let val t = (CModProj (m, ms, x'), loc) val env = pushCNamedAs env x n (KType, loc) (SOME t) - val (_, sgn) = lookupStrNamed env m - val (str, sgn) = foldl (fn (m, (str, sgn)) => - case projectStr env {sgn = sgn, str = str, field = m} of - NONE => raise Fail "ElabEnv.declBinds: Couldn't projectStr" - | SOME sgn => ((StrProj (str, m), loc), sgn)) - ((StrVar m, loc), sgn) ms - val xncs = case projectDatatype env {sgn = sgn, str = str, field = x'} of - NONE => raise Fail "ElabEnv.declBinds: Couldn't projectDatatype" - | SOME xncs => xncs val t = (CNamed n, loc) in
--- a/src/elab_print.sml Thu Jul 24 16:51:24 2008 -0400 +++ b/src/elab_print.sml Tue Jul 29 12:30:04 2008 -0400 @@ -346,7 +346,7 @@ space, p_con env c] | SgiDatatype x => p_datatype env x - | SgiDatatypeImp (x, _, m1, ms, x') => + | SgiDatatypeImp (x, _, m1, ms, x', _) => let val m1x = #1 (E.lookupStrNamed env m1) handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 @@ -468,7 +468,7 @@ space, p_con env c] | DDatatype x => p_datatype env x - | DDatatypeImp (x, _, m1, ms, x') => + | DDatatypeImp (x, _, m1, ms, x', _) => let val m1x = #1 (E.lookupStrNamed env m1) handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1
--- a/src/elab_util.sml Thu Jul 24 16:51:24 2008 -0400 +++ b/src/elab_util.sml Tue Jul 29 12:30:04 2008 -0400 @@ -386,7 +386,15 @@ fn c' => (x, n, SOME c'))) xncs, fn xncs' => (SgiDatatype (x, n, xncs'), loc)) - | SgiDatatypeImp _ => S.return2 siAll + | SgiDatatypeImp (x, n, m1, ms, s, xncs) => + S.map2 (ListUtil.mapfold (fn (x, n, c) => + case c of + NONE => S.return2 (x, n, c) + | SOME c => + S.map2 (con ctx c, + fn c' => (x, n, SOME c'))) xncs, + fn xncs' => + (SgiDatatypeImp (x, n, m1, ms, s, xncs'), loc)) | SgiVal (x, n, c) => S.map2 (con ctx c, fn c' => @@ -420,7 +428,7 @@ bind (ctx, NamedC (x, k)) | SgiDatatype (x, n, xncs) => bind (ctx, NamedC (x, (KType, loc))) - | SgiDatatypeImp (x, _, _, _, _) => + | SgiDatatypeImp (x, _, _, _, _, _) => bind (ctx, NamedC (x, (KType, loc))) | SgiVal _ => ctx | SgiStr (x, _, sgn) => @@ -541,7 +549,7 @@ end) ctx xncs end - | DDatatypeImp (x, n, m, ms, x') => + | DDatatypeImp (x, n, m, ms, x', _) => bind (ctx, NamedC (x, (KType, loc))) | DVal (x, _, c, _) => bind (ctx, NamedE (x, c)) @@ -598,7 +606,15 @@ fn c' => (x, n, SOME c'))) xncs, fn xncs' => (DDatatype (x, n, xncs'), loc)) - | DDatatypeImp _ => S.return2 dAll + | DDatatypeImp (x, n, m1, ms, s, xncs) => + S.map2 (ListUtil.mapfold (fn (x, n, c) => + case c of + NONE => S.return2 (x, n, c) + | SOME c => + S.map2 (mfc ctx c, + fn c' => (x, n, SOME c'))) xncs, + fn xncs' => + (DDatatypeImp (x, n, m1, ms, s, xncs'), loc)) | DVal vi => S.map2 (mfvi ctx vi, fn vi' =>
--- a/src/elaborate.sml Thu Jul 24 16:51:24 2008 -0400 +++ b/src/elaborate.sml Tue Jul 29 12:30:04 2008 -0400 @@ -1359,7 +1359,7 @@ E.pushENamedAs env x n t end) env xncs in - ([(L'.SgiDatatypeImp (x, n', n, ms, s), loc)], (env, denv, gs)) + ([(L'.SgiDatatypeImp (x, n', n, ms, s, xncs), loc)], (env, denv, gs)) end) | _ => (strError env (NotDatatype loc); ([], (env, denv, []))) @@ -1453,7 +1453,7 @@ (); (SS.add (cons, x), vals, sgns, strs) end - | L'.SgiDatatypeImp (x, _, _, _, _) => + | L'.SgiDatatypeImp (x, _, _, _, _, _) => (if SS.member (cons, x) then sgnError env (DuplicateCon (loc, x)) else @@ -1546,7 +1546,7 @@ (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'.SgiDatatypeImp (x, n, str, strs, x, xncs), 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) @@ -1584,45 +1584,32 @@ case #1 (hnormSgn env sgn) of L'.SgnConst sgis => ListUtil.foldlMap (fn ((sgi, loc), (env', denv')) => - case sgi of - L'.SgiConAbs (x, n, k) => - let - val c = (L'.CModProj (str, strs, x), loc) - in - ((L'.DCon (x, n, k, c), loc), - (E.pushCNamedAs env' x n k (SOME c), denv')) - end - | L'.SgiCon (x, n, k, c) => - ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc), - (E.pushCNamedAs env' x n k (SOME c), denv')) - | L'.SgiDatatype (x, n, xncs) => - let - val k = (L'.KType, loc) - val c = (L'.CModProj (str, strs, x), loc) - in - ((L'.DDatatypeImp (x, n, str, strs, x), loc), - (E.pushCNamedAs env' x n k (SOME c), denv')) - end - | L'.SgiDatatypeImp (x, n, m1, ms, x') => - let - val k = (L'.KType, loc) - val c = (L'.CModProj (m1, ms, x'), loc) - in - ((L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc), - (E.pushCNamedAs env' x n k (SOME c), denv')) - end - | L'.SgiVal (x, n, t) => - ((L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc), - (E.pushENamedAs env' x n t, denv')) - | L'.SgiStr (x, n, sgn) => - ((L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc), - (E.pushStrNamedAs env' x n sgn, denv')) - | L'.SgiSgn (x, n, sgn) => - ((L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc), - (E.pushSgnNamedAs env' x n sgn, denv')) - | L'.SgiConstraint (c1, c2) => - ((L'.DConstraint (c1, c2), loc), - (env', denv))) + let + val d = + case sgi of + L'.SgiConAbs (x, n, k) => + let + val c = (L'.CModProj (str, strs, x), loc) + in + (L'.DCon (x, n, k, c), loc) + end + | L'.SgiCon (x, n, k, c) => + (L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) + | L'.SgiDatatype (x, n, xncs) => + (L'.DDatatypeImp (x, n, str, strs, x, xncs), loc) + | L'.SgiDatatypeImp (x, n, m1, ms, x', xncs) => + (L'.DDatatypeImp (x, n, m1, ms, x', xncs), loc) + | L'.SgiVal (x, n, t) => + (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc) + | L'.SgiStr (x, n, sgn) => + (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc) + | L'.SgiSgn (x, n, sgn) => + (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc) + | L'.SgiConstraint (c1, c2) => + (L'.DConstraint (c1, c2), loc) + in + (d, (E.declBinds env' d, denv')) + end) (env, denv) sgis | _ => (strError env (UnOpenable sgn); ([], (env, denv))) @@ -1729,7 +1716,7 @@ L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE) | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1) | L'.SgiDatatype (x', n1, _) => found (x', n1, (L'.KType, loc), NONE) - | L'.SgiDatatypeImp (x', n1, m1, ms, s) => + | L'.SgiDatatypeImp (x', n1, m1, ms, s, _) => found (x', n1, (L'.KType, loc), SOME (L'.CModProj (m1, ms, s), loc)) | _ => NONE end) @@ -1796,21 +1783,18 @@ found (n1, xncs1) else NONE - | L'.SgiDatatypeImp (x', n1, m1, ms, s) => - let - val (str, sgn) = E.chaseMpath env (m1, ms) - in - case E.projectDatatype env {str = str, sgn = sgn, field = s} of - NONE => NONE - | SOME xncs1 => found (n1, xncs1) - end + | L'.SgiDatatypeImp (x', n1, _, _, _, xncs1) => + if x' = x then + found (n1, xncs1) + else + NONE | _ => NONE end) - | L'.SgiDatatypeImp (x, n2, m11, ms1, s1) => + | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, _) => seek (fn sgi1All as (sgi1, _) => case sgi1 of - L'.SgiDatatypeImp (x', n1, m12, ms2, s2) => + L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _) => if x = x' then let val k = (L'.KType, loc) @@ -2016,7 +2000,7 @@ E.pushENamedAs env x n t end) env xncs in - ([(L'.DDatatypeImp (x, n', n, ms, s), loc)], (env, denv, gs)) + ([(L'.DDatatypeImp (x, n', n, ms, s, xncs), loc)], (env, denv, gs)) end) | _ => (strError env (NotDatatype loc); ([], (env, denv, []))) @@ -2294,7 +2278,7 @@ in ((L'.SgiDatatype (x, n, xncs), loc) :: sgis, cons, vals, sgns, strs) end - | L'.SgiDatatypeImp (x, n, m1, ms, x') => + | L'.SgiDatatypeImp (x, n, m1, ms, x', xncs) => let val (cons, x) = if SS.member (cons, x) then @@ -2302,7 +2286,7 @@ else (SS.add (cons, x), x) in - ((L'.SgiDatatypeImp (x, n, m1, ms, x'), loc) :: sgis, cons, vals, sgns, strs) + ((L'.SgiDatatypeImp (x, n, m1, ms, x', xncs), loc) :: sgis, cons, vals, sgns, strs) end | L'.SgiVal (x, n, c) => let
--- a/src/expl.sml Thu Jul 24 16:51:24 2008 -0400 +++ b/src/expl.sml Tue Jul 29 12:30:04 2008 -0400 @@ -81,6 +81,8 @@ datatype sgn_item' = SgiConAbs of string * int * kind | SgiCon of string * int * kind * con + | SgiDatatype of string * int * (string * int * con option) list + | SgiDatatypeImp of string * int * int * string list * string * (string * int * con option) list | SgiVal of string * int * con | SgiSgn of string * int * sgn | SgiStr of string * int * sgn @@ -97,6 +99,8 @@ datatype decl' = DCon of string * int * kind * con + | DDatatype of string * int * (string * int * con option) list + | DDatatypeImp of string * int * int * string list * string * (string * int * con option) list | DVal of string * int * con * exp | DValRec of (string * int * con * exp) list | DSgn of string * int * sgn
--- a/src/expl_env.sml Thu Jul 24 16:51:24 2008 -0400 +++ b/src/expl_env.sml Tue Jul 29 12:30:04 2008 -0400 @@ -236,9 +236,28 @@ NONE => raise UnboundNamed n | SOME x => x -fun declBinds env (d, _) = +fun declBinds env (d, loc) = case d of DCon (x, n, k, c) => pushCNamed env x n k (SOME c) + | DDatatype (x, n, xncs) => + let + val env = pushCNamed env x n (KType, loc) NONE + in + foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) + | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc)) + env xncs + end + | DDatatypeImp (x, n, m, ms, x', xncs) => + let + val t = (CModProj (m, ms, x'), loc) + val env = pushCNamed env x n (KType, loc) (SOME t) + + val t = (CNamed n, loc) + in + foldl (fn ((x', n', NONE), env) => pushENamed env x' n' t + | ((x', n', SOME t'), env) => pushENamed env x' n' (TFun (t', t), loc)) + env xncs + end | DVal (x, n, t, _) => pushENamed env x n t | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamed env x n t) env vis | DSgn (x, n, sgn) => pushSgnNamed env x n sgn @@ -246,10 +265,26 @@ | DFfiStr (x, n, sgn) => pushStrNamed env x n sgn | DExport _ => env -fun sgiBinds env (sgi, _) = +fun sgiBinds env (sgi, loc) = case sgi of SgiConAbs (x, n, k) => pushCNamed env x n k NONE | SgiCon (x, n, k, c) => pushCNamed env x n k (SOME c) + | SgiDatatype (x, n, xncs) => + let + val env = pushCNamed env x n (KType, loc) NONE + in + foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) + | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc)) + env xncs + end + | SgiDatatypeImp (x, n, m1, ms, x', xncs) => + let + val env = pushCNamed env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc)) + in + foldl (fn ((x', n', NONE), env) => pushENamed env x' n' (CNamed n, loc) + | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc)) + env xncs + end | SgiVal (x, n, t) => pushENamed env x n t | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn | SgiStr (x, n, sgn) => pushStrNamed env x n sgn
--- a/src/expl_print.sml Thu Jul 24 16:51:24 2008 -0400 +++ b/src/expl_print.sml Tue Jul 29 12:30:04 2008 -0400 @@ -274,6 +274,22 @@ else string x +fun p_datatype env (x, n, cons) = + let + val env = E.pushCNamed env x n (KType, ErrorMsg.dummySpan) NONE + in + box [string "datatype", + space, + string x, + space, + string "=", + space, + p_list_sep (box [space, string "|", space]) + (fn (x, _, NONE) => string x + | (x, _, SOME t) => box [string x, space, string "of", space, p_con env t]) + cons] + end + fun p_sgn_item env (sgi, _) = case sgi of SgiConAbs (x, n, k) => box [string "con", @@ -294,6 +310,22 @@ string "=", space, p_con env c] + | SgiDatatype x => p_datatype env x + | SgiDatatypeImp (x, _, m1, ms, x', _) => + let + val m1x = #1 (E.lookupStrNamed env m1) + handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 + in + box [string "datatype", + space, + string x, + space, + string "=", + space, + string "datatype", + space, + p_list_sep (string ".") string (m1x :: ms @ [x'])] + end | SgiVal (x, n, c) => box [string "val", space, p_named x n, @@ -392,6 +424,22 @@ string "=", space, p_con env c] + | DDatatype x => p_datatype env x + | DDatatypeImp (x, _, m1, ms, x', _) => + let + val m1x = #1 (E.lookupStrNamed env m1) + handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 + in + box [string "datatype", + space, + string x, + space, + string "=", + space, + string "datatype", + space, + p_list_sep (string ".") string (m1x :: ms @ [x'])] + end | DVal vi => box [string "val", space, p_vali env vi]
--- a/src/expl_util.sml Thu Jul 24 16:51:24 2008 -0400 +++ b/src/expl_util.sml Tue Jul 29 12:30:04 2008 -0400 @@ -342,7 +342,7 @@ fun sgi ctx si acc = S.bindP (sgi' ctx si acc, sgn_item ctx) - and sgi' ctx (si, loc) = + and sgi' ctx (siAll as (si, loc)) = case si of SgiConAbs (x, n, k) => S.map2 (kind k, @@ -354,6 +354,24 @@ S.map2 (con ctx c, fn c' => (SgiCon (x, n, k', c'), loc))) + | SgiDatatype (x, n, xncs) => + S.map2 (ListUtil.mapfold (fn (x, n, c) => + case c of + NONE => S.return2 (x, n, c) + | SOME c => + S.map2 (con ctx c, + fn c' => (x, n, SOME c'))) xncs, + fn xncs' => + (SgiDatatype (x, n, xncs'), loc)) + | SgiDatatypeImp (x, n, m1, ms, s, xncs) => + S.map2 (ListUtil.mapfold (fn (x, n, c) => + case c of + NONE => S.return2 (x, n, c) + | SOME c => + S.map2 (con ctx c, + fn c' => (x, n, SOME c'))) xncs, + fn xncs' => + (SgiDatatypeImp (x, n, m1, ms, s, xncs'), loc)) | SgiVal (x, n, c) => S.map2 (con ctx c, fn c' => @@ -379,6 +397,10 @@ bind (ctx, NamedC (x, k)) | SgiCon (x, _, k, _) => bind (ctx, NamedC (x, k)) + | SgiDatatype (x, n, xncs) => + bind (ctx, NamedC (x, (KType, loc))) + | SgiDatatypeImp (x, _, _, _, _, _) => + bind (ctx, NamedC (x, (KType, loc))) | SgiVal _ => ctx | SgiStr (x, _, sgn) => bind (ctx, Str (x, sgn))
--- a/src/explify.sml Thu Jul 24 16:51:24 2008 -0400 +++ b/src/explify.sml Tue Jul 29 12:30:04 2008 -0400 @@ -95,8 +95,11 @@ case sgi of L.SgiConAbs (x, n, k) => SOME (L'.SgiConAbs (x, n, explifyKind k), loc) | L.SgiCon (x, n, k, c) => SOME (L'.SgiCon (x, n, explifyKind k, explifyCon c), loc) - | L.SgiDatatype _ => raise Fail "Explify SgiDatatype" - | L.SgiDatatypeImp _ => raise Fail "Explify SgiDatatypeImp" + | L.SgiDatatype (x, n, xncs) => SOME (L'.SgiDatatype (x, n, map (fn (x, n, co) => + (x, n, Option.map explifyCon co)) xncs), loc) + | L.SgiDatatypeImp (x, n, m1, ms, s, xncs) => + SOME (L'.SgiDatatypeImp (x, n, m1, ms, s, map (fn (x, n, co) => + (x, n, Option.map explifyCon co)) xncs), loc) | L.SgiVal (x, n, c) => SOME (L'.SgiVal (x, n, explifyCon c), loc) | L.SgiStr (x, n, sgn) => SOME (L'.SgiStr (x, n, explifySgn sgn), loc) | L.SgiSgn (x, n, sgn) => SOME (L'.SgiSgn (x, n, explifySgn sgn), loc) @@ -114,8 +117,11 @@ fun explifyDecl (d, loc : EM.span) = case d of L.DCon (x, n, k, c) => SOME (L'.DCon (x, n, explifyKind k, explifyCon c), loc) - | L.DDatatype _ => raise Fail "Explify DDatatype" - | L.DDatatypeImp _ => raise Fail "Explify DDatatypeImp" + | L.DDatatype (x, n, xncs) => SOME (L'.DDatatype (x, n, map (fn (x, n, co) => + (x, n, Option.map explifyCon co)) xncs), loc) + | L.DDatatypeImp (x, n, m1, ms, s, xncs) => + SOME (L'.DDatatypeImp (x, n, m1, ms, s, map (fn (x, n, co) => + (x, n, Option.map explifyCon co)) xncs), loc) | L.DVal (x, n, t, e) => SOME (L'.DVal (x, n, explifyCon t, explifyExp e), loc) | L.DValRec vis => SOME (L'.DValRec (map (fn (x, n, t, e) => (x, n, explifyCon t, explifyExp e)) vis), loc)