summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/corify.sml24
-rw-r--r--src/elab.sml10
-rw-r--r--src/elab_env.sig9
-rw-r--r--src/elab_env.sml141
-rw-r--r--src/elab_print.sml15
-rw-r--r--src/elab_util.sml35
-rw-r--r--src/elaborate.sml172
-rw-r--r--src/expl.sml10
-rw-r--r--src/expl_env.sml73
-rw-r--r--src/expl_print.sml19
-rw-r--r--src/expl_util.sml12
-rw-r--r--src/explify.sml25
-rw-r--r--src/lacweb.grm20
-rw-r--r--src/list_util.sig1
-rw-r--r--src/list_util.sml10
-rw-r--r--src/source.sml4
-rw-r--r--src/source_print.sml3
-rw-r--r--tests/datatypeP.lac10
18 files changed, 395 insertions, 198 deletions
diff --git a/src/corify.sml b/src/corify.sml
index 7e2f2493..6e49ccd5 100644
--- a/src/corify.sml
+++ b/src/corify.sml
@@ -429,7 +429,7 @@ structure St : sig
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 @@ structure St : sig
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 @@ structure St : sig
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 @@ structure St : sig
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 @@ structure St : sig
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 @@ structure St : sig
cmap,
conmap,
st)
- end
+ end*)
| L.SgiVal (x, _, c) =>
(ds,
@@ -811,8 +811,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.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 2bf64f5a..c04b5d23 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -83,7 +83,7 @@ datatype pat' =
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 @@ 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
+ | 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 @@ 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
+ | 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 --git a/src/elab_env.sig b/src/elab_env.sig
index f341bed2..6f0febcc 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -51,13 +51,14 @@ signature ELAB_ENV = sig
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 @@ signature ELAB_ENV = sig
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 --git a/src/elab_env.sml b/src/elab_env.sml
index 23b29155..eac0c662 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -73,7 +73,7 @@ datatype 'a var =
| 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 @@ type env = {
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 @@ fun lookupC (env : env) x =
| 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 @@ fun pushDatatype (env : env) n xncs =
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 @@ fun lookupDatatype (env : env) n =
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 @@ fun sgiBinds env (sgi, loc) =
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 @@ fun sgnSeek f sgis =
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 @@ fun sgnSeek f sgis =
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 @@ fun projectCon env {sgn, str, field} =
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 projectCon env {sgn, str, field} =
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 @@ fun projectVal env {sgn, str, field} =
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 @@ fun sgnSeekConstraints (str, sgis) =
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 projectConstraints env {sgn, str} =
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 --git a/src/elab_print.sml b/src/elab_print.sml
index 122c6c02..ceea43a9 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -216,8 +216,8 @@ fun p_pat' par env (p, _) =
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 @@ fun p_named x n =
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 @@ 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
@@ -523,7 +526,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 d8dd16b8..1c67fbb2 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -396,7 +396,7 @@ 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) =>
+ | 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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
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 @@ 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) =>
+ | 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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
(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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
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 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f
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 --git a/src/elaborate.sml b/src/elaborate.sml
index c999f844..94c51701 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -933,19 +933,32 @@ fun elabPat (pAll as (p, loc), (env, denv, bound)) =
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 @@ fun elabPat (pAll as (p, loc), (env, denv, bound)) =
(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 @@ fun elabPat (pAll as (p, loc), (env, denv, bound)) =
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 @@ fun exhaustive (env, denv, t, ps) =
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 @@ fun exhaustive (env, denv, t, ps) =
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 @@ fun exhaustive (env, denv, t, ps) =
(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 @@ fun exhaustive (env, denv, t, ps) =
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 @@ fun elabExp (env, denv) (eAll as (e, loc)) =
(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 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
([(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 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
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 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
((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 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
(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 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) =
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 @@ and elabSgn (env, denv) (sgn, loc) =
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 @@ 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
@@ -1828,8 +1861,8 @@ fun selfify env {str, strs, sgn} =
| 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 @@ fun dopen (env, denv) {str, strs, sgn} =
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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
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 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
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 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
([(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 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
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 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
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 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
(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 @@ fun elabDecl ((d, loc), (env, denv, gs)) =
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 @@ and elabStr (env, denv) (str, loc) =
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 @@ and elabStr (env, denv) (str, loc) =
((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 @@ and elabStr (env, denv) (str, loc) =
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 --git a/src/expl.sml b/src/expl.sml
index 9fea3f19..4ba835ea 100644
--- a/src/expl.sml
+++ b/src/expl.sml
@@ -69,7 +69,7 @@ datatype pat' =
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 @@ 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
+ | 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 @@ 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
+ | 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 --git a/src/expl_env.sml b/src/expl_env.sml
index 359c92a3..9d715c1b 100644
--- a/src/expl_env.sml
+++ b/src/expl_env.sml
@@ -239,24 +239,42 @@ fun lookupStrNamed (env : env) n =
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 @@ 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) =>
+ | 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 --git a/src/expl_print.sml b/src/expl_print.sml
index 1056dfe4..60075a70 100644
--- a/src/expl_print.sml
+++ b/src/expl_print.sml
@@ -181,10 +181,10 @@ fun p_pat' par env (p, _) =
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 @@ fun p_named x n =
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 @@ 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
@@ -482,7 +485,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/expl_util.sml b/src/expl_util.sml
index 481a96b0..8ec85b19 100644
--- a/src/expl_util.sml
+++ b/src/expl_util.sml
@@ -373,7 +373,7 @@ 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) =>
+ | 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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
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 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} =
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 @@ 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) =>
+ | 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 --git a/src/explify.sml b/src/explify.sml
index 847fbc60..9fe24ebe 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -81,7 +81,7 @@ fun explifyPat (p, loc) =
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 @@ 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 (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 @@ 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 (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 --git a/src/lacweb.grm b/src/lacweb.grm
index 3c3b87d5..0e25c217 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -64,6 +64,7 @@ fun uppercaseFirst "" = ""
| 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 @@ decl : CON SYMBOL EQ cexp (DCon (SYMBOL, NONE, cexp), s (CONleft,
| 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 @@ decl : CON SYMBOL EQ cexp (DCon (SYMBOL, NONE, cexp), s (CONleft,
| 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 @@ sgi : CON SYMBOL DCOLON kind (SgiConAbs (SYMBOL, kind), s (CONleft, k
| 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 --git a/src/list_util.sig b/src/list_util.sig
index 7bc4452c..33474b01 100644
--- a/src/list_util.sig
+++ b/src/list_util.sig
@@ -41,5 +41,6 @@ signature LIST_UTIL = sig
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 --git a/src/list_util.sml b/src/list_util.sml
index 976e4708..616efcf0 100644
--- a/src/list_util.sml
+++ b/src/list_util.sml
@@ -146,4 +146,14 @@ fun mapi f =
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 --git a/src/source.sml b/src/source.sml
index d58feb94..505dd172 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -71,7 +71,7 @@ withtype con = con' located
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 @@ withtype exp = exp' located
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 --git a/src/source_print.sml b/src/source_print.sml
index 960f3ac5..15bb6015 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -278,10 +278,11 @@ fun p_exp' par (e, _) =
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 --git a/tests/datatypeP.lac b/tests/datatypeP.lac
new file mode 100644
index 00000000..12389322
--- /dev/null
+++ b/tests/datatypeP.lac
@@ -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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-02 20:39:10 +0000