From 4cbbb0bb751dd9e9dae9d6b621e563ee5c7ae1b4 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 29 Jul 2008 12:30:04 -0400 Subject: Add datatype import constructor annotations; datatypes through explify --- src/corify.sml | 4 +++ src/elab.sml | 4 +-- src/elab_env.sml | 82 ++++++++++++++++++---------------------------- src/elab_print.sml | 4 +-- src/elab_util.sml | 24 +++++++++++--- src/elaborate.sml | 96 +++++++++++++++++++++++------------------------------- src/expl.sml | 4 +++ src/expl_env.sml | 39 ++++++++++++++++++++-- src/expl_print.sml | 48 +++++++++++++++++++++++++++ src/expl_util.sml | 24 +++++++++++++- src/explify.sml | 14 +++++--- 11 files changed, 221 insertions(+), 122 deletions(-) (limited to 'src') diff --git a/src/corify.sml b/src/corify.sml index 4277c35e..0f98e99c 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -384,6 +384,8 @@ fun corifyDecl ((d, loc : EM.span), st) = 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 @@ and corifyStr ((str, _), st) = 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') diff --git a/src/elab.sml b/src/elab.sml index e0ccee25..b258d7e5 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -94,7 +94,7 @@ 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 + | 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 @@ and sgn = sgn' located 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 diff --git a/src/elab_env.sml b/src/elab_env.sml index d28b713f..1fe5dd5a 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -353,7 +353,14 @@ fun sgiBinds env (sgi, loc) = | ((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 @@ fun sgnSeek f sgis = 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 @@ fun sgnSeek f sgis = 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 @@ fun projectCon env {sgn, str, field} = (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 @@ 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 + | 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 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 - | 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 @@ fun sgnSeekConstraints (str, sgis) = | 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 @@ fun declBinds env (d, loc) = | ((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 diff --git a/src/elab_print.sml b/src/elab_print.sml index 19653df9..693bc443 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -346,7 +346,7 @@ fun p_sgn_item env (sgi, _) = 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 @@ fun p_decl env (dAll as (d, _) : decl) = 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 diff --git a/src/elab_util.sml b/src/elab_util.sml index 0ee35320..05f80ad1 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -386,7 +386,15 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = 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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f 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' => diff --git a/src/elaborate.sml b/src/elaborate.sml index 802cef7b..cd2c25d7 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1359,7 +1359,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = 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 @@ and elabSgn (env, denv) (sgn, loc) = (); (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 @@ fun selfify env {str, strs, sgn} = (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 @@ fun dopen (env, denv) {str, strs, sgn} = 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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = 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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = 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 @@ fun elabDecl ((d, loc), (env, denv, gs)) = 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 @@ and elabStr (env, denv) (str, loc) = 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 @@ and elabStr (env, denv) (str, loc) = 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 diff --git a/src/expl.sml b/src/expl.sml index b1a0e389..183dbc31 100644 --- a/src/expl.sml +++ b/src/expl.sml @@ -81,6 +81,8 @@ withtype exp = exp' located 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 @@ and sgn = sgn' located 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 diff --git a/src/expl_env.sml b/src/expl_env.sml index 1871e560..359c92a3 100644 --- a/src/expl_env.sml +++ b/src/expl_env.sml @@ -236,9 +236,28 @@ fun lookupStrNamed (env : env) n = 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 @@ fun declBinds env (d, _) = | 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 diff --git a/src/expl_print.sml b/src/expl_print.sml index 58508097..472d83ae 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -274,6 +274,22 @@ fun p_named x n = 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 @@ fun p_sgn_item env (sgi, _) = 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 @@ fun p_decl env (dAll as (d, _) : decl) = 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] diff --git a/src/expl_util.sml b/src/expl_util.sml index 976df246..e1a5d30f 100644 --- a/src/expl_util.sml +++ b/src/expl_util.sml @@ -342,7 +342,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = 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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = 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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = 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)) diff --git a/src/explify.sml b/src/explify.sml index f179ce36..c193a631 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -95,8 +95,11 @@ fun explifySgi (sgi, loc) = 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 @@ and explifySgn (sgn, loc) = 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) -- cgit v1.2.3