# HG changeset patch # User Adam Chlipala # Date 1218205712 14400 # Node ID aa54250f58ac05b76f1cfb8dcc57e5961521ce8b # Parent 3eb53c957d102bbff41ea320793b13f6a863f926 Parametrized datatypes through explify diff -r 3eb53c957d10 -r aa54250f58ac src/corify.sml --- a/src/corify.sml Thu Aug 07 13:09:26 2008 -0400 +++ b/src/corify.sml Fri Aug 08 10:28:32 2008 -0400 @@ -429,7 +429,7 @@ L.PWild => (L'.PWild, loc) | L.PVar (x, t) => (L'.PVar (x, corifyCon st t), loc) | L.PPrim p => (L'.PPrim p, loc) - | L.PCon (dk, pc, po) => (L'.PCon (dk, corifyPatCon st pc, Option.map (corifyPat st) po), loc) + | L.PCon (dk, pc, ts, po) => raise Fail "Corify PCon" (*(L'.PCon (dk, corifyPatCon st pc, Option.map (corifyPat st) po), loc)*) | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, corifyPat st p, corifyCon st t)) xps), loc) fun corifyExp st (e, loc) = @@ -512,8 +512,8 @@ in ([(L'.DCon (x, n, corifyKind k, corifyCon st c), loc)], st) end - | L.DDatatype (x, n, xncs) => - let + | L.DDatatype (x, n, xs, xncs) => raise Fail "Corify DDatatype" + (*let val (st, n) = St.bindCon st x n val (xncs, st) = ListUtil.foldlMap (fn ((x, n, co), st) => let @@ -541,9 +541,9 @@ end) xncs in ((L'.DDatatype (x, n, xncs), loc) :: dcons, st) - end - | L.DDatatypeImp (x, n, m1, ms, s, xncs) => - let + end*) + | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => raise Fail "Corify DDatatypeImp" + (*let val (st, n) = St.bindCon st x n val c = corifyCon st (L.CModProj (m1, ms, s), loc) @@ -571,7 +571,7 @@ end) xncs in ((L'.DCon (x, n, (L'.KType, loc), c), loc) :: cds, st) - end + end*) | L.DVal (x, n, t, e) => let val (st, n) = St.bindVal st x n @@ -648,8 +648,8 @@ st) end - | L.SgiDatatype (x, n, xnts) => - let + | L.SgiDatatype (x, n, xs, xnts) => raise Fail "Corify FFI SgiDatatype" + (*let val dk = ExplUtil.classifyDatatype xnts val (st, n') = St.bindCon st x n val (xnts, (ds', st, cmap, conmap)) = @@ -698,7 +698,7 @@ cmap, conmap, st) - end + end*) | L.SgiVal (x, _, c) => (ds, @@ -811,8 +811,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.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 -r 3eb53c957d10 -r aa54250f58ac src/elab.sml --- a/src/elab.sml Thu Aug 07 13:09:26 2008 -0400 +++ b/src/elab.sml Fri Aug 08 10:28:32 2008 -0400 @@ -83,7 +83,7 @@ PWild | PVar of string * con | PPrim of Prim.t - | PCon of datatype_kind * patCon * pat option + | PCon of datatype_kind * patCon * con list * pat option | PRecord of (string * pat * con) list withtype pat = pat' located @@ -112,8 +112,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 + | SgiDatatype of string * int * string list * (string * int * con option) list + | SgiDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list | SgiVal of string * int * con | SgiStr of string * int * sgn | SgiSgn of string * int * sgn @@ -132,8 +132,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 + | DDatatype of string * int * string list * (string * int * con option) list + | DDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list | DVal of string * int * con * exp | DValRec of (string * int * con * exp) list | DSgn of string * int * sgn diff -r 3eb53c957d10 -r aa54250f58ac src/elab_env.sig --- a/src/elab_env.sig Thu Aug 07 13:09:26 2008 -0400 +++ b/src/elab_env.sig Fri Aug 08 10:28:32 2008 -0400 @@ -51,13 +51,14 @@ val lookupC : env -> string -> Elab.kind var - val pushDatatype : env -> int -> (string * int * Elab.con option) list -> env + val pushDatatype : env -> int -> string list -> (string * int * Elab.con option) list -> env type datatyp val lookupDatatype : env -> int -> datatyp val lookupDatatypeConstructor : datatyp -> int -> string * Elab.con option + val datatypeArgs : datatyp -> string list val constructors : datatyp -> (string * int * Elab.con option) list - val lookupConstructor : env -> string -> (Elab.datatype_kind * int * Elab.con option * int) option + val lookupConstructor : env -> string -> (Elab.datatype_kind * int * string list * Elab.con option * int) option val pushERel : env -> string -> Elab.con -> env val lookupERel : env -> int -> string * Elab.con @@ -87,9 +88,9 @@ val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option val projectDatatype : env -> { sgn : Elab.sgn, str : Elab.str, field : string } - -> (string * int * Elab.con option) list option + -> (string list * (string * int * Elab.con option) list) option val projectConstructor : env -> { sgn : Elab.sgn, str : Elab.str, field : string } - -> (Elab.datatype_kind * int * Elab.con option * Elab.con) option + -> (Elab.datatype_kind * int * string list * Elab.con option * Elab.con) option val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option val projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option diff -r 3eb53c957d10 -r aa54250f58ac src/elab_env.sml --- a/src/elab_env.sml Thu Aug 07 13:09:26 2008 -0400 +++ b/src/elab_env.sml Fri Aug 08 10:28:32 2008 -0400 @@ -73,7 +73,7 @@ | Rel of int * 'a | Named of int * 'a -type datatyp = (string * con option) IM.map +type datatyp = string list * (string * con option) IM.map type env = { renameC : kind var' SM.map, @@ -81,7 +81,7 @@ namedC : (string * kind * con option) IM.map, datatypes : datatyp IM.map, - constructors : (datatype_kind * int * con option * int) SM.map, + constructors : (datatype_kind * int * string list * con option * int) SM.map, renameE : con var' SM.map, relE : (string * con) list, @@ -188,7 +188,7 @@ | SOME (Rel' x) => Rel x | SOME (Named' x) => Named x -fun pushDatatype (env : env) n xncs = +fun pushDatatype (env : env) n xs xncs = let val dk = U.classifyDatatype xncs in @@ -197,10 +197,10 @@ namedC = #namedC env, datatypes = IM.insert (#datatypes env, n, - foldl (fn ((x, n, to), cons) => - IM.insert (cons, n, (x, to))) IM.empty xncs), + (xs, foldl (fn ((x, n, to), cons) => + IM.insert (cons, n, (x, to))) IM.empty xncs)), constructors = foldl (fn ((x, n', to), cmap) => - SM.insert (cmap, x, (dk, n', to, n))) + SM.insert (cmap, x, (dk, n', xs, to, n))) (#constructors env) xncs, renameE = #renameE env, @@ -219,14 +219,15 @@ NONE => raise UnboundNamed n | SOME x => x -fun lookupDatatypeConstructor dt n = +fun lookupDatatypeConstructor (_, dt) n = case IM.find (dt, n) of NONE => raise UnboundNamed n | SOME x => x fun lookupConstructor (env : env) s = SM.find (#constructors env, s) -fun constructors dt = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt +fun datatypeArgs (xs, _) = xs +fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt fun pushERel (env : env) x t = let @@ -362,20 +363,40 @@ case sgi of SgiConAbs (x, n, k) => pushCNamedAs env x n k NONE | SgiCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) - | SgiDatatype (x, n, xncs) => + | SgiDatatype (x, n, xs, xncs) => let val env = pushCNamedAs env x n (KType, loc) NONE 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)) + foldl (fn ((x', n', to), env) => + let + val t = + case to of + NONE => (CNamed n, loc) + | SOME t => (TFun (t, (CNamed n, loc)), loc) + + val k = (KType, loc) + val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs + in + pushENamedAs env x' n' t + end) env xncs end - | SgiDatatypeImp (x, n, m1, ms, x', xncs) => + | SgiDatatypeImp (x, n, m1, ms, x', xs, 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)) + foldl (fn ((x', n', to), env) => + let + val t = + case to of + NONE => (CNamed n, loc) + | SOME t => (TFun (t, (CNamed n, loc)), loc) + + val k = (KType, loc) + val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs + in + pushENamedAs env x' n' t + end) env xncs end | SgiVal (x, n, t) => pushENamedAs env x n t @@ -394,8 +415,8 @@ let val cons = case sgi of - SgiDatatype (x, n, _) => IM.insert (cons, n, x) - | SgiDatatypeImp (x, n, _, _, _, _) => IM.insert (cons, n, x) + SgiDatatype (x, n, _, _) => IM.insert (cons, n, x) + | SgiDatatypeImp (x, n, _, _, _, _, _) => IM.insert (cons, n, x) | _ => cons in SOME (v, (sgns, strs, cons)) @@ -404,8 +425,8 @@ case sgi of 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)) + | SgiDatatype (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) @@ -552,8 +573,8 @@ SgnConst sgis => (case sgnSeek (fn SgiConAbs (x, _, k) => if x = field then SOME (k, NONE) else NONE | SgiCon (x, _, k, c) => if x = field then SOME (k, SOME c) else NONE - | SgiDatatype (x, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE - | SgiDatatypeImp (x, _, m1, ms, x', _) => + | SgiDatatype (x, _, _, _) => if x = field then SOME ((KType, #2 sgn), NONE) else NONE + | SgiDatatypeImp (x, _, m1, ms, x', _, _) => if x = field then SOME ((KType, #2 sgn), SOME (CModProj (m1, ms, x'), #2 sgn)) else @@ -567,30 +588,31 @@ 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, _, _, _, _, xncs) => if x = field then SOME xncs else NONE + (case sgnSeek (fn SgiDatatype (x, _, xs, xncs) => if x = field then SOME (xs, xncs) else NONE + | SgiDatatypeImp (x, _, _, _, _, xs, xncs) => if x = field then SOME (xs, 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)) + | SOME ((xs, xncs), subs) => SOME (xs, + map (fn (x, n, to) => (x, n, Option.map (sgnSubCon (str, subs)) to)) xncs)) | _ => NONE fun projectConstructor env {sgn, str, field} = case #1 (hnormSgn env sgn) of SgnConst sgis => let - fun consider (n, xncs) = + fun consider (n, xs, xncs) = ListUtil.search (fn (x, n', to) => if x <> field then NONE else - SOME (U.classifyDatatype xncs, n', to, (CNamed n, #2 str))) xncs + SOME (U.classifyDatatype xncs, n', xs, to, (CNamed n, #2 str))) xncs in - case sgnSeek (fn SgiDatatype (_, n, xncs) => consider (n, xncs) - | SgiDatatypeImp (_, n, _, _, _, xncs) => consider (n, xncs) + case sgnSeek (fn SgiDatatype (_, n, xs, xncs) => consider (n, xs, xncs) + | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => consider (n, xs, xncs) | _ => NONE) sgis of NONE => NONE - | SOME ((dk, n, to, t), subs) => SOME (dk, n, Option.map (sgnSubCon (str, subs)) to, - sgnSubCon (str, subs) t) + | SOME ((dk, n, xs, to, t), subs) => SOME (dk, n, xs, Option.map (sgnSubCon (str, subs)) to, + sgnSubCon (str, subs) t) end | _ => NONE @@ -598,18 +620,25 @@ case #1 (hnormSgn env sgn) of SgnConst sgis => let - fun seek (n, xncs) = + fun seek (n, xs, 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)) + SOME (let + val t = + case to of + NONE => (CNamed n, #2 sgn) + | SOME t => (TFun (t, (CNamed n, #2 sgn)), #2 sgn) + val k = (KType, #2 sgn) + in + foldr (fn (x, t) => (TCFun (Explicit, x, k, t), #2 sgn)) + t xs + end) 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) + | SgiDatatype (_, n, xs, xncs) => seek (n, xs, xncs) + | SgiDatatypeImp (_, n, _, _, _, xs, xncs) => seek (n, xs, xncs) | _ => NONE) sgis of NONE => NONE | SOME (c, subs) => SOME (sgnSubCon (str, subs) c) @@ -632,8 +661,8 @@ end | 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) + | 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) | 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) @@ -650,26 +679,44 @@ fun declBinds env (d, loc) = case d of DCon (x, n, k, c) => pushCNamedAs env x n k (SOME c) - | DDatatype (x, n, xncs) => + | DDatatype (x, n, xs, xncs) => let val env = pushCNamedAs env x n (KType, loc) NONE - val env = pushDatatype env n xncs + val env = pushDatatype env n xs xncs 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 + foldl (fn ((x', n', to), env) => + let + val t = + case to of + NONE => (CNamed n, loc) + | SOME t => (TFun (t, (CNamed n, loc)), loc) + val k = (KType, loc) + val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs + in + pushENamedAs env x' n' t + end) + env xncs end - | DDatatypeImp (x, n, m, ms, x', xncs) => + | DDatatypeImp (x, n, m, ms, x', xs, xncs) => let val t = (CModProj (m, ms, x'), loc) val env = pushCNamedAs env x n (KType, loc) (SOME t) - val env = pushDatatype env n xncs + val env = pushDatatype env n xs xncs val t = (CNamed n, loc) in - foldl (fn ((x', n', NONE), env) => pushENamedAs env x' n' t - | ((x', n', SOME t'), env) => pushENamedAs env x' n' (TFun (t', t), loc)) - env xncs + foldl (fn ((x', n', to), env) => + let + val t = + case to of + NONE => (CNamed n, loc) + | SOME t => (TFun (t, (CNamed n, loc)), loc) + val k = (KType, loc) + val t = foldr (fn (x, t) => (TCFun (Explicit, x, k, t), loc)) t xs + in + pushENamedAs env x' n' t + end) + env xncs end | DVal (x, n, t, _) => pushENamedAs env x n t | DValRec vis => foldl (fn ((x, n, t, _), env) => pushENamedAs env x n t) env vis diff -r 3eb53c957d10 -r aa54250f58ac src/elab_print.sml --- a/src/elab_print.sml Thu Aug 07 13:09:26 2008 -0400 +++ b/src/elab_print.sml Fri Aug 08 10:28:32 2008 -0400 @@ -216,8 +216,8 @@ PWild => string "_" | PVar (s, _) => string s | PPrim p => Prim.p_t p - | PCon (_, pc, NONE) => p_patCon env pc - | PCon (_, pc, SOME p) => parenIf par (box [p_patCon env pc, + | PCon (_, pc, _, NONE) => p_patCon env pc + | PCon (_, pc, _, SOME p) => parenIf par (box [p_patCon env pc, space, p_pat' true env p]) | PRecord xps => @@ -364,13 +364,16 @@ else string x -fun p_datatype env (x, n, cons) = +fun p_datatype env (x, n, xs, cons) = let - val env = E.pushCNamedAs env x n (KType, ErrorMsg.dummySpan) NONE + val k = (KType, ErrorMsg.dummySpan) + val env = E.pushCNamedAs env x n k NONE + val env = foldl (fn (x, env) => E.pushCRel env x k) env xs in box [string "datatype", space, string x, + p_list_sep (box []) (fn x => box [space, string x]) xs, space, string "=", space, @@ -401,7 +404,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 @@ -523,7 +526,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 diff -r 3eb53c957d10 -r aa54250f58ac src/elab_util.sml --- a/src/elab_util.sml Thu Aug 07 13:09:26 2008 -0400 +++ b/src/elab_util.sml Fri Aug 08 10:28:32 2008 -0400 @@ -396,7 +396,7 @@ S.map2 (con ctx c, fn c' => (SgiCon (x, n, k', c'), loc))) - | SgiDatatype (x, n, xncs) => + | SgiDatatype (x, n, xs, xncs) => S.map2 (ListUtil.mapfold (fn (x, n, c) => case c of NONE => S.return2 (x, n, c) @@ -404,8 +404,8 @@ 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) => + (SgiDatatype (x, n, xs, xncs'), loc)) + | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) => S.map2 (ListUtil.mapfold (fn (x, n, c) => case c of NONE => S.return2 (x, n, c) @@ -413,7 +413,7 @@ S.map2 (con ctx c, fn c' => (x, n, SOME c'))) xncs, fn xncs' => - (SgiDatatypeImp (x, n, m1, ms, s, xncs'), loc)) + (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc)) | SgiVal (x, n, c) => S.map2 (con ctx c, fn c' => @@ -445,9 +445,9 @@ bind (ctx, NamedC (x, k)) | SgiCon (x, _, k, _) => bind (ctx, NamedC (x, k)) - | SgiDatatype (x, n, xncs) => + | 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) => @@ -553,7 +553,7 @@ (case #1 d of DCon (x, _, k, _) => bind (ctx, NamedC (x, k)) - | DDatatype (x, n, xncs) => + | DDatatype (x, n, xs, xncs) => let val ctx = bind (ctx, NamedC (x, (KType, loc))) in @@ -563,12 +563,21 @@ case co of NONE => CNamed n | SOME t => TFun (t, (CNamed n, loc)) + + val k = (KType, loc) + val t = (t, loc) + val t = foldr (fn (x, t) => + (TCFun (Explicit, + x, + k, + t), loc)) + t xs in - bind (ctx, NamedE (x, (t, loc))) + bind (ctx, NamedE (x, t)) 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)) @@ -616,7 +625,7 @@ S.map2 (mfc ctx c, fn c' => (DCon (x, n, k', c'), loc))) - | DDatatype (x, n, xncs) => + | DDatatype (x, n, xs, xncs) => S.map2 (ListUtil.mapfold (fn (x, n, c) => case c of NONE => S.return2 (x, n, c) @@ -624,8 +633,8 @@ S.map2 (mfc ctx c, fn c' => (x, n, SOME c'))) xncs, fn xncs' => - (DDatatype (x, n, xncs'), loc)) - | DDatatypeImp (x, n, m1, ms, s, xncs) => + (DDatatype (x, n, xs, xncs'), loc)) + | DDatatypeImp (x, n, m1, ms, s, xs, xncs) => S.map2 (ListUtil.mapfold (fn (x, n, c) => case c of NONE => S.return2 (x, n, c) @@ -633,7 +642,7 @@ S.map2 (mfc ctx c, fn c' => (x, n, SOME c'))) xncs, fn xncs' => - (DDatatypeImp (x, n, m1, ms, s, xncs'), loc)) + (DDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc)) | DVal vi => S.map2 (mfvi ctx vi, fn vi' => diff -r 3eb53c957d10 -r aa54250f58ac src/elaborate.sml --- a/src/elaborate.sml Thu Aug 07 13:09:26 2008 -0400 +++ b/src/elaborate.sml Fri Aug 08 10:28:32 2008 -0400 @@ -933,19 +933,32 @@ val pterror = (perror, terror) val rerror = (pterror, (env, bound)) - fun pcon (pc, po, to, dn, dk) = + fun pcon (pc, po, xs, to, dn, dk) = case (po, to) of (NONE, SOME _) => (expError env (PatHasNoArg loc); rerror) | (SOME _, NONE) => (expError env (PatHasArg loc); rerror) - | (NONE, NONE) => (((L'.PCon (dk, pc, NONE), loc), dn), - (env, bound)) + | (NONE, NONE) => + let + val k = (L'.KType, loc) + val unifs = map (fn _ => cunif (loc, k)) xs + val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs + in + (((L'.PCon (dk, pc, unifs, NONE), loc), dn), + (env, bound)) + end | (SOME p, SOME t) => let val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound)) + + val k = (L'.KType, loc) + val unifs = map (fn _ => cunif (loc, k)) xs + val t = ListUtil.foldli (fn (i, u, t) => subConInCon (i, u) t) t unifs + val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs in - (((L'.PCon (dk, pc, SOME p'), loc), dn), + ignore (checkPatCon (env, denv) p' pt t); + (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn), (env, bound)) end in @@ -969,7 +982,7 @@ (case E.lookupConstructor env x of NONE => (expError env (UnboundConstructor (loc, [], x)); rerror) - | SOME (dk, n, to, dn) => pcon (L'.PConVar n, po, to, (L'.CNamed dn, loc), dk)) + | SOME (dk, n, xs, to, dn) => pcon (L'.PConVar n, po, xs, to, (L'.CNamed dn, loc), dk)) | L.PCon (m1 :: ms, x, po) => (case E.lookupStr env m1 of NONE => (expError env (UnboundStrInExp (loc, m1)); @@ -985,7 +998,7 @@ case E.projectConstructor env {str = str, sgn = sgn, field = x} of NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x)); rerror) - | SOME (dk, _, to, dn) => pcon (L'.PConProj (n, ms, x), po, to, dn, dk) + | SOME (dk, _, xs, to, dn) => pcon (L'.PConProj (n, ms, x), po, xs, to, dn, dk) end) | L.PRecord (xps, flex) => @@ -1035,7 +1048,7 @@ in case E.projectConstructor env {str = str, sgn = sgn, field = x} of NONE => raise Fail "exhaustive: Can't project constructor" - | SOME (_, n, _, _) => n + | SOME (_, n, _, _, _) => n end fun coverage (p, _) = @@ -1043,8 +1056,8 @@ L'.PWild => Wild | L'.PVar _ => Wild | L'.PPrim _ => None - | L'.PCon (_, pc, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild)) - | L'.PCon (_, pc, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p)) + | L'.PCon (_, pc, _, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild)) + | L'.PCon (_, pc, _, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p)) | L'.PRecord xps => Record [foldl (fn ((x, p, _), fmap) => SM.insert (fmap, x, coverage p)) SM.empty xps] @@ -1158,8 +1171,13 @@ (total, gs' @ gs) end) (true, gs) cons + + fun unapp t = + case t of + L'.CApp ((t, _), _) => unapp t + | _ => t in - case t of + case unapp t of L'.CNamed n => let val dt = E.lookupDatatype env n @@ -1173,7 +1191,7 @@ in case E.projectDatatype env {str = str, sgn = sgn, field = x} of NONE => raise Fail "isTotal: Can't project datatype" - | SOME cons => dtype cons + | SOME (_, cons) => dtype cons end | L'.CError => (true, gs) | _ => raise Fail "isTotal: Not a datatype" @@ -1206,7 +1224,11 @@ (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, [])) + | E.Named (n, t) => + if Char.isUpper (String.sub (s, 0)) then + elabHead (env, denv) (L'.ENamed n, loc) t + else + ((L'.ENamed n, loc), t, [])) | L.EVar (m1 :: ms, s) => (case E.lookupStr env m1 of NONE => (expError env (UnboundStrInExp (loc, m1)); @@ -1572,11 +1594,13 @@ ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) end - | L.SgiDatatype (x, xcs) => + | L.SgiDatatype (x, xs, xcs) => let val k = (L'.KType, loc) - val (env, n) = E.pushCNamed env x k NONE + val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs + val (env, n) = E.pushCNamed env x k' NONE val t = (L'.CNamed n, loc) + val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel i, loc)), loc)) t xs val (xcs, (used, env, gs)) = ListUtil.foldlMap @@ -1591,6 +1615,7 @@ checkKind env t' tk k; (SOME t', (L'.TFun (t', t), loc), gs' @ gs) end + val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs val (env, n') = E.pushENamed env x t in @@ -1601,8 +1626,10 @@ ((x, n', to), (SS.add (used, x), env, gs')) end) (SS.empty, env, []) xcs + + val env = E.pushDatatype env n xs xcs in - ([(L'.SgiDatatype (x, n, xcs), loc)], (env, denv, gs)) + ([(L'.SgiDatatype (x, n, xs, xcs), loc)], (env, denv, gs)) end | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp" @@ -1625,12 +1652,14 @@ (case E.projectDatatype env {sgn = sgn, str = str, field = s} of NONE => (conError env (UnboundDatatype (loc, s)); ([], (env, denv, gs))) - | SOME xncs => + | SOME (xs, xncs) => let val k = (L'.KType, loc) + val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs + val t = (L'.CModProj (n, ms, s), loc) - val (env, n') = E.pushCNamed env x k (SOME t) - val env = E.pushDatatype env n' xncs + val (env, n') = E.pushCNamed env x k' (SOME t) + val env = E.pushDatatype env n' xs xncs val t = (L'.CNamed n', loc) val env = foldl (fn ((x, n, to), env) => @@ -1638,11 +1667,15 @@ val t = case to of NONE => t | SOME t' => (L'.TFun (t', t), loc) + + val t = foldr (fn (x, t) => + (L'.TCFun (L'.Implicit, x, k, t), loc)) + t xs in E.pushENamedAs env x n t end) env xncs in - ([(L'.SgiDatatypeImp (x, n', n, ms, s, xncs), loc)], (env, denv, gs)) + ([(L'.SgiDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs)) end) | _ => (strError env (NotDatatype loc); ([], (env, denv, []))) @@ -1720,7 +1753,7 @@ else (); (SS.add (cons, x), vals, sgns, strs)) - | L'.SgiDatatype (x, _, xncs) => + | L'.SgiDatatype (x, _, _, xncs) => let val vals = foldl (fn ((x, _, _), vals) => (if SS.member (vals, x) then @@ -1736,7 +1769,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 @@ -1828,8 +1861,8 @@ | L'.SgnConst sgis => (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) => (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) - | (L'.SgiDatatype (x, n, xncs), loc) => - (L'.SgiDatatypeImp (x, n, str, strs, x, xncs), loc) + | (L'.SgiDatatype (x, n, xs, xncs), loc) => + (L'.SgiDatatypeImp (x, n, str, strs, x, xs, 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) @@ -1878,10 +1911,10 @@ 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'.SgiDatatype (x, n, xs, xncs) => + (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc) + | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => + (L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc) | L'.SgiVal (x, n, t) => (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc) | L'.SgiStr (x, n, sgn) => @@ -1998,9 +2031,20 @@ case sgi1 of 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, _) => - found (x', n1, (L'.KType, loc), SOME (L'.CModProj (m1, ms, s), loc)) + | L'.SgiDatatype (x', n1, xs, _) => + let + val k = (L'.KType, loc) + val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs + in + found (x', n1, k', NONE) + end + | L'.SgiDatatypeImp (x', n1, m1, ms, s, xs, _) => + let + val k = (L'.KType, loc) + val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs + in + found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc)) + end | _ => NONE end) @@ -2023,15 +2067,18 @@ NONE | _ => NONE) - | L'.SgiDatatype (x, n2, xncs2) => + | L'.SgiDatatype (x, n2, xs2, xncs2) => seek (fn sgi1All as (sgi1, _) => let - fun found (n1, xncs1) = + fun found (n1, xs1, xncs1) = let fun mismatched ue = (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue)); SOME (env, denv)) + val k = (L'.KType, loc) + val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1 + fun good () = let val env = E.sgiBinds env sgi2All @@ -2044,6 +2091,7 @@ SOME (env, denv) end + val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1 fun xncBad ((x1, _, t1), (x2, _, t2)) = String.compare (x1, x2) <> EQUAL orelse case (t1, t2) of @@ -2052,7 +2100,8 @@ not (List.null (unifyCons (env, denv) t1 t2)) | _ => true in - (if length xncs1 <> length xncs2 + (if xs1 <> xs2 + orelse length xncs1 <> length xncs2 orelse ListPair.exists xncBad (xncs1, xncs2) then mismatched NONE else @@ -2061,33 +2110,34 @@ end in case sgi1 of - L'.SgiDatatype (x', n1, xncs1) => + L'.SgiDatatype (x', n1, xs, xncs1) => if x' = x then - found (n1, xncs1) + found (n1, xs, xncs1) else NONE - | L'.SgiDatatypeImp (x', n1, _, _, _, xncs1) => + | L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) => if x' = x then - found (n1, xncs1) + found (n1, xs, xncs1) else NONE | _ => NONE end) - | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, _) => + | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) => seek (fn sgi1All as (sgi1, _) => case sgi1 of - L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _) => + L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) => if x = x' then let val k = (L'.KType, loc) + val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs val t1 = (L'.CModProj (m11, ms1, s1), loc) val t2 = (L'.CModProj (m12, ms2, s2), loc) fun good () = let - val env = E.pushCNamedAs env x n1 k (SOME t1) - val env = E.pushCNamedAs env x n2 k (SOME t2) + val env = E.pushCNamedAs env x n1 k' (SOME t1) + val env = E.pushCNamedAs env x n2 k' (SOME t2) in SOME (env, denv) end @@ -2213,11 +2263,17 @@ ([(L'.DCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) end - | L.DDatatype (x, xcs) => + | L.DDatatype (x, xs, xcs) => let val k = (L'.KType, loc) - val (env, n) = E.pushCNamed env x k NONE + val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs + val (env, n) = E.pushCNamed env x k' NONE val t = (L'.CNamed n, loc) + val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel i, loc)), loc)) t xs + + val (env', denv') = foldl (fn (x, (env', denv')) => + (E.pushCRel env' x k, + D.enter denv')) (env, denv) xs val (xcs, (used, env, gs)) = ListUtil.foldlMap @@ -2227,11 +2283,12 @@ NONE => (NONE, t, gs) | SOME t' => let - val (t', tk, gs') = elabCon (env, denv) t' + val (t', tk, gs') = elabCon (env', denv') t' in - checkKind env t' tk k; + checkKind env' t' tk k; (SOME t', (L'.TFun (t', t), loc), gs' @ gs) end + val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs val (env, n') = E.pushENamed env x t in @@ -2243,9 +2300,9 @@ end) (SS.empty, env, []) xcs - val env = E.pushDatatype env n xcs + val env = E.pushDatatype env n xs xcs in - ([(L'.DDatatype (x, n, xcs), loc)], (env, denv, gs)) + ([(L'.DDatatype (x, n, xs, xcs), loc)], (env, denv, gs)) end | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp" @@ -2268,12 +2325,13 @@ (case E.projectDatatype env {sgn = sgn, str = str, field = s} of NONE => (conError env (UnboundDatatype (loc, s)); ([], (env, denv, gs))) - | SOME xncs => + | SOME (xs, xncs) => let val k = (L'.KType, loc) + val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs val t = (L'.CModProj (n, ms, s), loc) - val (env, n') = E.pushCNamed env x k (SOME t) - val env = E.pushDatatype env n' xncs + val (env, n') = E.pushCNamed env x k' (SOME t) + val env = E.pushDatatype env n' xs xncs val t = (L'.CNamed n', loc) val env = foldl (fn ((x, n, to), env) => @@ -2281,11 +2339,15 @@ val t = case to of NONE => t | SOME t' => (L'.TFun (t', t), loc) + + val t = foldr (fn (x, t) => + (L'.TCFun (L'.Implicit, x, k, t), loc)) + t xs in E.pushENamedAs env x n t end) env xncs in - ([(L'.DDatatypeImp (x, n', n, ms, s, xncs), loc)], (env, denv, gs)) + ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs)) end) | _ => (strError env (NotDatatype loc); ([], (env, denv, []))) @@ -2544,7 +2606,7 @@ in ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs) end - | L'.SgiDatatype (x, n, xncs) => + | L'.SgiDatatype (x, n, xs, xncs) => let val (cons, x) = if SS.member (cons, x) then @@ -2561,9 +2623,9 @@ ((x, n, t), SS.add (vals, x))) vals xncs in - ((L'.SgiDatatype (x, n, xncs), loc) :: sgis, cons, vals, sgns, strs) + ((L'.SgiDatatype (x, n, xs, xncs), loc) :: sgis, cons, vals, sgns, strs) end - | L'.SgiDatatypeImp (x, n, m1, ms, x', xncs) => + | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => let val (cons, x) = if SS.member (cons, x) then @@ -2571,7 +2633,7 @@ else (SS.add (cons, x), x) in - ((L'.SgiDatatypeImp (x, n, m1, ms, x', xncs), loc) :: sgis, cons, vals, sgns, strs) + ((L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs), loc) :: sgis, cons, vals, sgns, strs) end | L'.SgiVal (x, n, c) => let diff -r 3eb53c957d10 -r aa54250f58ac src/expl.sml --- a/src/expl.sml Thu Aug 07 13:09:26 2008 -0400 +++ b/src/expl.sml Fri Aug 08 10:28:32 2008 -0400 @@ -69,7 +69,7 @@ PWild | PVar of string * con | PPrim of Prim.t - | PCon of datatype_kind * patCon * pat option + | PCon of datatype_kind * patCon * con list * pat option | PRecord of (string * pat * con) list withtype pat = pat' located @@ -98,8 +98,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 + | SgiDatatype of string * int * string list * (string * int * con option) list + | SgiDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list | SgiVal of string * int * con | SgiSgn of string * int * sgn | SgiStr of string * int * sgn @@ -116,8 +116,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 + | DDatatype of string * int * string list * (string * int * con option) list + | DDatatypeImp of string * int * int * string list * string * string list * (string * int * con option) list | DVal of string * int * con * exp | DValRec of (string * int * con * exp) list | DSgn of string * int * sgn diff -r 3eb53c957d10 -r aa54250f58ac src/expl_env.sml --- a/src/expl_env.sml Thu Aug 07 13:09:26 2008 -0400 +++ b/src/expl_env.sml Fri Aug 08 10:28:32 2008 -0400 @@ -239,24 +239,42 @@ fun declBinds env (d, loc) = case d of DCon (x, n, k, c) => pushCNamed env x n k (SOME c) - | DDatatype (x, n, xncs) => + | DDatatype (x, n, xs, 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 + foldl (fn ((x', n', to), env) => + let + val t = + case to of + NONE => (CNamed n, loc) + | SOME t => (TFun (t, (CNamed n, loc)), loc) + val k = (KType, loc) + val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs + in + pushENamed env x' n' t + end) + env xncs end - | DDatatypeImp (x, n, m, ms, x', xncs) => + | DDatatypeImp (x, n, m, ms, x', xs, 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 + foldl (fn ((x', n', to), env) => + let + val t = + case to of + NONE => (CNamed n, loc) + | SOME t => (TFun (t, (CNamed n, loc)), loc) + val k = (KType, loc) + val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs + in + pushENamed env x' n' t + end) + 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 @@ -269,21 +287,42 @@ 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) => + | SgiDatatype (x, n, xs, 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 + foldl (fn ((x', n', to), env) => + let + val t = + case to of + NONE => (CNamed n, loc) + | SOME t => (TFun (t, (CNamed n, loc)), loc) + val k = (KType, loc) + val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs + in + pushENamed env x' n' t + end) + env xncs end - | SgiDatatypeImp (x, n, m1, ms, x', xncs) => + | SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => let - val env = pushCNamed env x n (KType, loc) (SOME (CModProj (m1, ms, x'), loc)) + val t = (CModProj (m1, 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' (CNamed n, loc) - | ((x', n', SOME t), env) => pushENamed env x' n' (TFun (t, (CNamed n, loc)), loc)) - env xncs + foldl (fn ((x', n', to), env) => + let + val t = + case to of + NONE => (CNamed n, loc) + | SOME t => (TFun (t, (CNamed n, loc)), loc) + val k = (KType, loc) + val t = foldr (fn (x, t) => (TCFun (x, k, t), loc)) t xs + in + pushENamed env x' n' t + end) + env xncs end | SgiVal (x, n, t) => pushENamed env x n t | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn diff -r 3eb53c957d10 -r aa54250f58ac src/expl_print.sml --- a/src/expl_print.sml Thu Aug 07 13:09:26 2008 -0400 +++ b/src/expl_print.sml Fri Aug 08 10:28:32 2008 -0400 @@ -181,10 +181,10 @@ PWild => string "_" | PVar (s, _) => string s | PPrim p => Prim.p_t p - | PCon (_, pc, NONE) => p_patCon env pc - | PCon (_, pc, SOME p) => parenIf par (box [p_patCon env pc, - space, - p_pat' true env p]) + | PCon (_, pc, _, NONE) => p_patCon env pc + | PCon (_, pc, _, SOME p) => parenIf par (box [p_patCon env pc, + space, + p_pat' true env p]) | PRecord xps => box [string "{", p_list_sep (box [string ",", space]) (fn (x, p, _) => @@ -329,13 +329,16 @@ else string x -fun p_datatype env (x, n, cons) = +fun p_datatype env (x, n, xs, cons) = let - val env = E.pushCNamed env x n (KType, ErrorMsg.dummySpan) NONE + val k = (KType, ErrorMsg.dummySpan) + val env = E.pushCNamed env x n k NONE + val env = foldl (fn (x, env) => E.pushCRel env x k) env xs in box [string "datatype", space, string x, + p_list_sep (box []) (fn x => box [space, string x]) xs, space, string "=", space, @@ -368,7 +371,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 @@ -482,7 +485,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 diff -r 3eb53c957d10 -r aa54250f58ac src/expl_util.sml --- a/src/expl_util.sml Thu Aug 07 13:09:26 2008 -0400 +++ b/src/expl_util.sml Fri Aug 08 10:28:32 2008 -0400 @@ -373,7 +373,7 @@ S.map2 (con ctx c, fn c' => (SgiCon (x, n, k', c'), loc))) - | SgiDatatype (x, n, xncs) => + | SgiDatatype (x, n, xs, xncs) => S.map2 (ListUtil.mapfold (fn (x, n, c) => case c of NONE => S.return2 (x, n, c) @@ -381,8 +381,8 @@ 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) => + (SgiDatatype (x, n, xs, xncs'), loc)) + | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) => S.map2 (ListUtil.mapfold (fn (x, n, c) => case c of NONE => S.return2 (x, n, c) @@ -390,7 +390,7 @@ S.map2 (con ctx c, fn c' => (x, n, SOME c'))) xncs, fn xncs' => - (SgiDatatypeImp (x, n, m1, ms, s, xncs'), loc)) + (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc)) | SgiVal (x, n, c) => S.map2 (con ctx c, fn c' => @@ -416,9 +416,9 @@ bind (ctx, NamedC (x, k)) | SgiCon (x, _, k, _) => bind (ctx, NamedC (x, k)) - | SgiDatatype (x, n, xncs) => + | 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) => diff -r 3eb53c957d10 -r aa54250f58ac src/explify.sml --- a/src/explify.sml Thu Aug 07 13:09:26 2008 -0400 +++ b/src/explify.sml Fri Aug 08 10:28:32 2008 -0400 @@ -81,7 +81,7 @@ L.PWild => (L'.PWild, loc) | L.PVar (x, t) => (L'.PVar (x, explifyCon t), loc) | L.PPrim p => (L'.PPrim p, loc) - | L.PCon (dk, pc, po) => (L'.PCon (dk, explifyPatCon pc, Option.map explifyPat po), loc) + | L.PCon (dk, pc, cs, po) => (L'.PCon (dk, explifyPatCon pc, map explifyCon cs, Option.map explifyPat po), loc) | L.PRecord xps => (L'.PRecord (map (fn (x, p, t) => (x, explifyPat p, explifyCon t)) xps), loc) fun explifyExp (e, loc) = @@ -113,11 +113,12 @@ 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 (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.SgiDatatype (x, n, xs, xncs) => SOME (L'.SgiDatatype (x, n, xs, + map (fn (x, n, co) => + (x, n, Option.map explifyCon co)) xncs), loc) + | L.SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) => + SOME (L'.SgiDatatypeImp (x, n, m1, ms, s, xs, 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) @@ -135,11 +136,13 @@ 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 (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.DDatatype (x, n, xs, xncs) => SOME (L'.DDatatype (x, n, xs, + map (fn (x, n, co) => + (x, n, Option.map explifyCon co)) xncs), loc) + | L.DDatatypeImp (x, n, m1, ms, s, xs, xncs) => + SOME (L'.DDatatypeImp (x, n, m1, ms, s, xs, + 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) diff -r 3eb53c957d10 -r aa54250f58ac src/lacweb.grm --- a/src/lacweb.grm Thu Aug 07 13:09:26 2008 -0400 +++ b/src/lacweb.grm Fri Aug 08 10:28:32 2008 -0400 @@ -64,6 +64,7 @@ | vali of string * con option * exp | valis of (string * con option * exp) list + | dargs of string list | barOpt of unit | dcons of (string * con option) list | dcon of string * con option @@ -142,9 +143,11 @@ | CON SYMBOL DCOLON kind EQ cexp (DCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright)) | LTYPE SYMBOL EQ cexp (DCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp), s (LTYPEleft, cexpright)) - | DATATYPE SYMBOL EQ barOpt dcons(DDatatype (SYMBOL, dcons), s (DATATYPEleft, dconsright)) - | DATATYPE SYMBOL EQ DATATYPE CSYMBOL DOT path - (DDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright)) + | DATATYPE SYMBOL dargs EQ barOpt dcons(DDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright)) + | DATATYPE SYMBOL dargs EQ DATATYPE CSYMBOL DOT path + (case dargs of + [] => (DDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright)) + | _ => raise Fail "Arguments specified for imported datatype") | VAL vali (DVal vali, s (VALleft, valiright)) | VAL REC valis (DValRec valis, s (VALleft, valisright)) @@ -169,6 +172,9 @@ | CONSTRAINT cterm TWIDDLE cterm (DConstraint (cterm1, cterm2), s (CONSTRAINTleft, ctermright)) | EXPORT spath (DExport spath, s (EXPORTleft, spathright)) +dargs : ([]) + | SYMBOL dargs (SYMBOL :: dargs) + barOpt : () | BAR () @@ -207,9 +213,11 @@ | CON SYMBOL DCOLON kind EQ cexp (SgiCon (SYMBOL, SOME kind, cexp), s (CONleft, cexpright)) | LTYPE SYMBOL EQ cexp (SgiCon (SYMBOL, SOME (KType, s (LTYPEleft, cexpright)), cexp), s (LTYPEleft, cexpright)) - | DATATYPE SYMBOL EQ barOpt dcons(SgiDatatype (SYMBOL, dcons), s (DATATYPEleft, dconsright)) - | DATATYPE SYMBOL EQ DATATYPE CSYMBOL DOT path - (SgiDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright)) + | DATATYPE SYMBOL dargs EQ barOpt dcons(SgiDatatype (SYMBOL, dargs, dcons), s (DATATYPEleft, dconsright)) + | DATATYPE SYMBOL dargs EQ DATATYPE CSYMBOL DOT path + (case dargs of + [] => (SgiDatatypeImp (SYMBOL, CSYMBOL :: #1 path, #2 path), s (DATATYPEleft, pathright)) + | _ => raise Fail "Arguments specified for imported datatype") | VAL SYMBOL COLON cexp (SgiVal (SYMBOL, cexp), s (VALleft, cexpright)) | STRUCTURE CSYMBOL COLON sgn (SgiStr (CSYMBOL, sgn), s (STRUCTUREleft, sgnright)) diff -r 3eb53c957d10 -r aa54250f58ac src/list_util.sig --- a/src/list_util.sig Thu Aug 07 13:09:26 2008 -0400 +++ b/src/list_util.sig Fri Aug 08 10:28:32 2008 -0400 @@ -41,5 +41,6 @@ val search : ('a -> 'b option) -> 'a list -> 'b option val mapi : (int * 'a -> 'b) -> 'a list -> 'b list + val foldli : (int * 'a * 'b -> 'b) -> 'b -> 'a list -> 'b end diff -r 3eb53c957d10 -r aa54250f58ac src/list_util.sml --- a/src/list_util.sml Thu Aug 07 13:09:26 2008 -0400 +++ b/src/list_util.sml Fri Aug 08 10:28:32 2008 -0400 @@ -146,4 +146,14 @@ m 0 [] end +fun foldli f = + let + fun m i acc ls = + case ls of + [] => acc + | h :: t => m (i + 1) (f (i, h, acc)) t + in + m 0 + end + end diff -r 3eb53c957d10 -r aa54250f58ac src/source.sml --- a/src/source.sml Thu Aug 07 13:09:26 2008 -0400 +++ b/src/source.sml Fri Aug 08 10:28:32 2008 -0400 @@ -71,7 +71,7 @@ datatype sgn_item' = SgiConAbs of string * kind | SgiCon of string * kind option * con - | SgiDatatype of string * (string * con option) list + | SgiDatatype of string * string list * (string * con option) list | SgiDatatypeImp of string * string list * string | SgiVal of string * con | SgiStr of string * sgn @@ -120,7 +120,7 @@ datatype decl' = DCon of string * kind option * con - | DDatatype of string * (string * con option) list + | DDatatype of string * string list * (string * con option) list | DDatatypeImp of string * string list * string | DVal of string * con option * exp | DValRec of (string * con option * exp) list diff -r 3eb53c957d10 -r aa54250f58ac src/source_print.sml --- a/src/source_print.sml Thu Aug 07 13:09:26 2008 -0400 +++ b/src/source_print.sml Fri Aug 08 10:28:32 2008 -0400 @@ -278,10 +278,11 @@ and p_exp e = p_exp' false e -fun p_datatype (x, cons) = +fun p_datatype (x, xs, cons) = box [string "datatype", space, string x, + p_list_sep (box []) (fn x => box [space, string x]) xs, space, string "=", space, diff -r 3eb53c957d10 -r aa54250f58ac tests/datatypeP.lac --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/datatypeP.lac Fri Aug 08 10:28:32 2008 -0400 @@ -0,0 +1,10 @@ +datatype option a = None | Some of a + +val none : option int = None +val some_1 : option int = Some 1 + +val f = fn t ::: Type => fn x : option t => + case x of None => None | Some x => Some (Some x) + +val none_again = f none +val some_1_again = f some_1