summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-06-29 10:39:43 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-06-29 10:39:43 -0400
commitd8ceac1d02caeffbe44865dfd2573863adc535ba (patch)
tree4d65fe41ebe08884d1e701a3caa3cd93b0698b18
parentabd57cd85a78e243185e7c6f528b3f21344319ea (diff)
Broaden unification context
-rw-r--r--src/elab.sml4
-rw-r--r--src/elab_print.sml12
-rw-r--r--src/elab_util.sig44
-rw-r--r--src/elab_util.sml219
-rw-r--r--src/elaborate.sml484
-rw-r--r--src/explify.sml4
-rw-r--r--tests/broad_unif.lac15
7 files changed, 493 insertions, 289 deletions
diff --git a/src/elab.sml b/src/elab.sml
index 7c3ec6b1..1b0e3ea1 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -36,7 +36,7 @@ datatype kind' =
| KRecord of kind
| KError
- | KUnif of string * kind option ref
+ | KUnif of ErrorMsg.span * string * kind option ref
withtype kind = kind' located
@@ -62,7 +62,7 @@ datatype con' =
| CFold of kind * kind
| CError
- | CUnif of kind * string * con option ref
+ | CUnif of ErrorMsg.span * kind * string * con option ref
withtype con = con' located
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 9158a6ae..8c51be11 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -50,8 +50,8 @@ fun p_kind' par (k, _) =
| KRecord k => box [string "{", p_kind k, string "}"]
| KError => string "<ERROR>"
- | KUnif (_, ref (SOME k)) => p_kind' par k
- | KUnif (s, _) => string ("<UNIF:" ^ s ^ ">")
+ | KUnif (_, _, ref (SOME k)) => p_kind' par k
+ | KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">")
and p_kind k = p_kind' false k
@@ -156,10 +156,10 @@ fun p_con' par env (c, _) =
| CFold _ => string "fold"
| CError => string "<ERROR>"
- | CUnif (_, _, ref (SOME c)) => p_con' par env c
- | CUnif (k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),
- p_kind k,
- string ">"]
+ | CUnif (_, _, _, ref (SOME c)) => p_con' par env c
+ | CUnif (_, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),
+ p_kind k,
+ string ">"]
and p_con env = p_con' false env
diff --git a/src/elab_util.sig b/src/elab_util.sig
index d6d8acaa..1ecd6201 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -107,4 +107,48 @@ structure Sgn : sig
end
+structure Decl : sig
+ datatype binder =
+ RelC of string * Elab.kind
+ | NamedC of string * Elab.kind
+ | RelE of string * Elab.con
+ | NamedE of string * Elab.con
+ | Str of string * Elab.sgn
+ | Sgn of string * Elab.sgn
+
+ val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+ con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
+ exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB,
+ sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
+ sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB,
+ str : ('context, Elab.str', 'state, 'abort) Search.mapfolderB,
+ decl : ('context, Elab.decl', 'state, 'abort) Search.mapfolderB,
+ bind : 'context * binder -> 'context}
+ -> ('context, Elab.decl, 'state, 'abort) Search.mapfolderB
+ val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
+ con : (Elab.con', 'state, 'abort) Search.mapfolder,
+ exp : (Elab.exp', 'state, 'abort) Search.mapfolder,
+ sgn_item : (Elab.sgn_item', 'state, 'abort) Search.mapfolder,
+ sgn : (Elab.sgn', 'state, 'abort) Search.mapfolder,
+ str : (Elab.str', 'state, 'abort) Search.mapfolder,
+ decl : (Elab.decl', 'state, 'abort) Search.mapfolder}
+ -> (Elab.decl, 'state, 'abort) Search.mapfolder
+ val exists : {kind : Elab.kind' -> bool,
+ con : Elab.con' -> bool,
+ exp : Elab.exp' -> bool,
+ sgn_item : Elab.sgn_item' -> bool,
+ sgn : Elab.sgn' -> bool,
+ str : Elab.str' -> bool,
+ decl : Elab.decl' -> bool}
+ -> Elab.decl -> bool
+ val search : {kind : Elab.kind' -> 'a option,
+ con : Elab.con' -> 'a option,
+ exp : Elab.exp' -> 'a option,
+ sgn_item : Elab.sgn_item' -> 'a option,
+ sgn : Elab.sgn' -> 'a option,
+ str : Elab.str' -> 'a option,
+ decl : Elab.decl' -> 'a option}
+ -> Elab.decl -> 'a option
+end
+
end
diff --git a/src/elab_util.sml b/src/elab_util.sml
index f764395d..45446a4e 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -58,7 +58,7 @@ fun mapfold f =
| KError => S.return2 kAll
- | KUnif (_, ref (SOME k)) => mfk' k
+ | KUnif (_, _, ref (SOME k)) => mfk' k
| KUnif _ => S.return2 kAll
in
mfk
@@ -151,7 +151,7 @@ fun mapfoldB {kind = fk, con = fc, bind} =
(CFold (k1', k2'), loc)))
| CError => S.return2 cAll
- | CUnif (_, _, ref (SOME c)) => mfc' ctx c
+ | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c
| CUnif _ => S.return2 cAll
in
mfc
@@ -417,4 +417,219 @@ fun map {kind, con, sgn_item, sgn} s =
end
+structure Decl = struct
+
+datatype binder =
+ RelC of string * Elab.kind
+ | NamedC of string * Elab.kind
+ | RelE of string * Elab.con
+ | NamedE of string * Elab.con
+ | Str of string * Elab.sgn
+ | Sgn of string * Elab.sgn
+
+fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} =
+ let
+ val mfk = Kind.mapfold fk
+
+ fun bind' (ctx, b) =
+ let
+ val b' = case b of
+ Con.Rel x => RelC x
+ | Con.Named x => NamedC x
+ in
+ bind (ctx, b')
+ end
+ val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
+
+ fun bind' (ctx, b) =
+ let
+ val b' = case b of
+ Exp.RelC x => RelC x
+ | Exp.NamedC x => NamedC x
+ | Exp.RelE x => RelE x
+ | Exp.NamedE x => NamedE x
+ in
+ bind (ctx, b')
+ end
+ val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind'}
+
+ fun bind' (ctx, b) =
+ let
+ val b' = case b of
+ Sgn.RelC x => RelC x
+ | Sgn.NamedC x => NamedC x
+ | Sgn.Sgn x => Sgn x
+ | Sgn.Str x => Str x
+ in
+ bind (ctx, b')
+ end
+ val mfsg = Sgn.mapfoldB {kind = fk, con = fc, sgn_item = fsgi, sgn = fsg, bind = bind'}
+
+ fun mfst ctx str acc =
+ S.bindP (mfst' ctx str acc, fst ctx)
+
+ and mfst' ctx (strAll as (str, loc)) =
+ case str of
+ StrConst ds =>
+ S.map2 (ListUtil.mapfoldB (fn (ctx, d) =>
+ (case #1 d of
+ DCon (x, _, k, _) =>
+ bind (ctx, NamedC (x, k))
+ | DVal (x, _, c, _) =>
+ bind (ctx, NamedE (x, c))
+ | DSgn (x, _, sgn) =>
+ bind (ctx, Sgn (x, sgn))
+ | DStr (x, _, sgn, _) =>
+ bind (ctx, Str (x, sgn))
+ | DFfiStr (x, _, sgn) =>
+ bind (ctx, Str (x, sgn)),
+ mfd ctx d)) ctx ds,
+ fn ds' => (StrConst ds', loc))
+ | StrVar _ => S.return2 strAll
+ | StrProj (str, x) =>
+ S.map2 (mfst ctx str,
+ fn str' =>
+ (StrProj (str', x), loc))
+ | StrFun (x, n, sgn1, sgn2, str) =>
+ S.bind2 (mfsg ctx sgn1,
+ fn sgn1' =>
+ S.bind2 (mfsg ctx sgn2,
+ fn sgn2' =>
+ S.map2 (mfst ctx str,
+ fn str' =>
+ (StrFun (x, n, sgn1', sgn2', str'), loc))))
+ | StrApp (str1, str2) =>
+ S.bind2 (mfst ctx str1,
+ fn str1' =>
+ S.map2 (mfst ctx str2,
+ fn str2' =>
+ (StrApp (str1', str2'), loc)))
+ | StrError => S.return2 strAll
+
+ and mfd ctx d acc =
+ S.bindP (mfd' ctx d acc, fd ctx)
+
+ and mfd' ctx (dAll as (d, loc)) =
+ case d of
+ DCon (x, n, k, c) =>
+ S.bind2 (mfk k,
+ fn k' =>
+ S.map2 (mfc ctx c,
+ fn c' =>
+ (DCon (x, n, k', c'), loc)))
+ | DVal (x, n, c, e) =>
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (DVal (x, n, c', e'), loc)))
+ | DSgn (x, n, sgn) =>
+ S.map2 (mfsg ctx sgn,
+ fn sgn' =>
+ (DSgn (x, n, sgn'), loc))
+ | DStr (x, n, sgn, str) =>
+ S.bind2 (mfsg ctx sgn,
+ fn sgn' =>
+ S.map2 (mfst ctx str,
+ fn str' =>
+ (DStr (x, n, sgn', str'), loc)))
+ | DFfiStr (x, n, sgn) =>
+ S.map2 (mfsg ctx sgn,
+ fn sgn' =>
+ (DFfiStr (x, n, sgn'), loc))
+ in
+ mfd
+ end
+
+fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} =
+ mapfoldB {kind = kind,
+ con = fn () => con,
+ exp = fn () => exp,
+ sgn_item = fn () => sgn_item,
+ sgn = fn () => sgn,
+ str = fn () => str,
+ decl = fn () => decl,
+ bind = fn ((), _) => ()} ()
+
+fun exists {kind, con, exp, sgn_item, sgn, str, decl} k =
+ case mapfold {kind = fn k => fn () =>
+ if kind k then
+ S.Return ()
+ else
+ S.Continue (k, ()),
+ con = fn c => fn () =>
+ if con c then
+ S.Return ()
+ else
+ S.Continue (c, ()),
+ exp = fn e => fn () =>
+ if exp e then
+ S.Return ()
+ else
+ S.Continue (e, ()),
+ sgn_item = fn sgi => fn () =>
+ if sgn_item sgi then
+ S.Return ()
+ else
+ S.Continue (sgi, ()),
+ sgn = fn x => fn () =>
+ if sgn x then
+ S.Return ()
+ else
+ S.Continue (x, ()),
+ str = fn x => fn () =>
+ if str x then
+ S.Return ()
+ else
+ S.Continue (x, ()),
+ decl = fn x => fn () =>
+ if decl x then
+ S.Return ()
+ else
+ S.Continue (x, ())} k () of
+ S.Return _ => true
+ | S.Continue _ => false
+
+fun search {kind, con, exp, sgn_item, sgn, str, decl} k =
+ case mapfold {kind = fn x => fn () =>
+ case kind x of
+ NONE => S.Continue (x, ())
+ | SOME v => S.Return v,
+
+ con = fn x => fn () =>
+ case con x of
+ NONE => S.Continue (x, ())
+ | SOME v => S.Return v,
+
+ exp = fn x => fn () =>
+ case exp x of
+ NONE => S.Continue (x, ())
+ | SOME v => S.Return v,
+
+ sgn_item = fn x => fn () =>
+ case sgn_item x of
+ NONE => S.Continue (x, ())
+ | SOME v => S.Return v,
+
+ sgn = fn x => fn () =>
+ case sgn x of
+ NONE => S.Continue (x, ())
+ | SOME v => S.Return v,
+
+ str = fn x => fn () =>
+ case str x of
+ NONE => S.Continue (x, ())
+ | SOME v => S.Return v,
+
+ decl = fn x => fn () =>
+ case decl x of
+ NONE => S.Continue (x, ())
+ | SOME v => S.Return v
+
+ } k () of
+ S.Return x => SOME x
+ | S.Continue _ => NONE
+
+end
+
end
diff --git a/src/elaborate.sml b/src/elaborate.sml
index d8d29fa0..307af12e 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -47,7 +47,7 @@ fun elabExplicitness e =
| L.Implicit => L'.Implicit
fun occursKind r =
- U.Kind.exists (fn L'.KUnif (_, r') => r = r'
+ U.Kind.exists (fn L'.KUnif (_, _, r') => r = r'
| _ => false)
datatype kunify_error =
@@ -82,21 +82,21 @@ fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) =
| (L'.KError, _) => ()
| (_, L'.KError) => ()
- | (L'.KUnif (_, ref (SOME k1All)), _) => unifyKinds' k1All k2All
- | (_, L'.KUnif (_, ref (SOME k2All))) => unifyKinds' k1All k2All
+ | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All
+ | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' k1All k2All
- | (L'.KUnif (_, r1), L'.KUnif (_, r2)) =>
+ | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) =>
if r1 = r2 then
()
else
r1 := SOME k2All
- | (L'.KUnif (_, r), _) =>
+ | (L'.KUnif (_, _, r), _) =>
if occursKind r k2All then
err KOccursCheckFailed
else
r := SOME k2All
- | (_, L'.KUnif (_, r)) =>
+ | (_, L'.KUnif (_, _, r)) =>
if occursKind r k1All then
err KOccursCheckFailed
else
@@ -159,7 +159,7 @@ in
fun resetKunif () = count := 0
-fun kunif () =
+fun kunif loc =
let
val n = !count
val s = if n <= 26 then
@@ -168,7 +168,7 @@ fun kunif () =
"U" ^ Int.toString (n - 26)
in
count := n + 1;
- (L'.KUnif (s, ref NONE), dummy)
+ (L'.KUnif (loc, s, ref NONE), dummy)
end
end
@@ -179,7 +179,7 @@ in
fun resetCunif () = count := 0
-fun cunif k =
+fun cunif (loc, k) =
let
val n = !count
val s = if n <= 26 then
@@ -188,7 +188,7 @@ fun cunif k =
"U" ^ Int.toString (n - 26)
in
count := n + 1;
- (L'.CUnif (k, s, ref NONE), dummy)
+ (L'.CUnif (loc, k, s, ref NONE), dummy)
end
end
@@ -199,7 +199,7 @@ fun elabKind (k, loc) =
| L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc)
| L.KName => (L'.KName, loc)
| L.KRecord k => (L'.KRecord (elabKind k), loc)
- | L.KWild => kunif ()
+ | L.KWild => kunif loc
fun foldKind (dom, ran, loc)=
(L'.KArrow ((L'.KArrow ((L'.KName, loc),
@@ -282,8 +282,8 @@ fun elabCon env (c, loc) =
let
val (c1', k1) = elabCon env c1
val (c2', k2) = elabCon env c2
- val dom = kunif ()
- val ran = kunif ()
+ val dom = kunif loc
+ val ran = kunif loc
in
checkKind env c1' k1 (L'.KArrow (dom, ran), loc);
checkKind env c2' k2 dom;
@@ -292,7 +292,7 @@ fun elabCon env (c, loc) =
| L.CAbs (x, ko, t) =>
let
val k' = case ko of
- NONE => kunif ()
+ NONE => kunif loc
| SOME k => elabKind k
val env' = E.pushCRel env x k'
val (t', tk) = elabCon env' t
@@ -306,7 +306,7 @@ fun elabCon env (c, loc) =
| L.CRecord xcs =>
let
- val k = kunif ()
+ val k = kunif loc
val xcs' = map (fn (x, c) =>
let
@@ -327,7 +327,7 @@ fun elabCon env (c, loc) =
let
val (c1', k1) = elabCon env c1
val (c2', k2) = elabCon env c2
- val ku = kunif ()
+ val ku = kunif loc
val k = (L'.KRecord ku, loc)
in
checkKind env c1' k1 k;
@@ -336,8 +336,8 @@ fun elabCon env (c, loc) =
end
| L.CFold =>
let
- val dom = kunif ()
- val ran = kunif ()
+ val dom = kunif loc
+ val ran = kunif loc
in
((L'.CFold (dom, ran), loc),
foldKind (dom, ran, loc))
@@ -347,34 +347,37 @@ fun elabCon env (c, loc) =
let
val k' = elabKind k
in
- (cunif k', k')
+ (cunif (loc, k'), k')
end
fun kunifsRemain k =
case k of
- L'.KUnif (_, ref NONE) => true
+ L'.KUnif (_, _, ref NONE) => true
| _ => false
fun cunifsRemain c =
case c of
- L'.CUnif (_, _, ref NONE) => true
- | _ => false
-
-val kunifsInKind = U.Kind.exists kunifsRemain
-val kunifsInCon = U.Con.exists {kind = kunifsRemain,
- con = fn _ => false}
-val kunifsInExp = U.Exp.exists {kind = kunifsRemain,
- con = fn _ => false,
- exp = fn _ => false}
-
-val cunifsInCon = U.Con.exists {kind = fn _ => false,
- con = cunifsRemain}
-val cunifsInExp = U.Exp.exists {kind = fn _ => false,
- con = cunifsRemain,
- exp = fn _ => false}
+ L'.CUnif (loc, _, _, ref NONE) => SOME loc
+ | _ => NONE
+
+val kunifsInDecl = U.Decl.exists {kind = kunifsRemain,
+ con = fn _ => false,
+ exp = fn _ => false,
+ sgn_item = fn _ => false,
+ sgn = fn _ => false,
+ str = fn _ => false,
+ decl = fn _ => false}
+
+val cunifsInDecl = U.Decl.search {kind = fn _ => NONE,
+ con = cunifsRemain,
+ exp = fn _ => NONE,
+ sgn_item = fn _ => NONE,
+ sgn = fn _ => NONE,
+ str = fn _ => NONE,
+ decl = fn _ => NONE}
fun occursCon r =
U.Con.exists {kind = fn _ => false,
- con = fn L'.CUnif (_, _, r') => r = r'
+ con = fn L'.CUnif (_, _, _, r') => r = r'
| _ => false}
datatype cunify_error =
@@ -461,7 +464,7 @@ exception CUnify of L'.con * L'.con * cunify_error
fun hnormKind (kAll as (k, _)) =
case k of
- L'.KUnif (_, ref (SOME k)) => hnormKind k
+ L'.KUnif (_, _, ref (SOME k)) => hnormKind k
| _ => kAll
fun kindof env (c, loc) =
@@ -500,7 +503,7 @@ fun kindof env (c, loc) =
| L'.CFold (dom, ran) => foldKind (dom, ran, loc)
| L'.CError => kerror
- | L'.CUnif (k, _, _) => k
+ | L'.CUnif (_, k, _, _) => k
fun unifyRecordCons env (c1, c2) =
let
@@ -523,8 +526,8 @@ and recordSummary env c : record_summary =
unifs = #unifs s1 @ #unifs s2,
others = #others s1 @ #others s2}
end
- | (L'.CUnif (_, _, ref (SOME c)), _) => recordSummary env c
- | c' as (L'.CUnif (_, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
+ | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary env c
+ | c' as (L'.CUnif (_, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
| c' => {fields = [], unifs = [], others = [c']}
and consEq env (c1, c2) =
@@ -577,7 +580,7 @@ and unifySummaries env (k, s1 : record_summary, s2 : record_summary) =
| (_, _, (_, r) :: rest) =>
let
val r' = ref NONE
- val cr' = (L'.CUnif (k, "recd", r'), dummy)
+ val cr' = (L'.CUnif (dummy, k, "recd", r'), dummy)
val prefix = case (fs, others) of
([], other :: others) =>
@@ -626,7 +629,7 @@ and unifySummaries env (k, s1 : record_summary, s2 : record_summary) =
and hnormCon env (cAll as (c, loc)) =
case c of
- L'.CUnif (_, _, ref (SOME c)) => hnormCon env c
+ L'.CUnif (_, _, _, ref (SOME c)) => hnormCon env c
| L'.CNamed xn =>
(case E.lookupCNamed env xn of
@@ -758,22 +761,22 @@ and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) =
| (L'.CError, _) => ()
| (_, L'.CError) => ()
- | (L'.CUnif (_, _, ref (SOME c1All)), _) => unifyCons' env c1All c2All
- | (_, L'.CUnif (_, _, ref (SOME c2All))) => unifyCons' env c1All c2All
+ | (L'.CUnif (_, _, _, ref (SOME c1All)), _) => unifyCons' env c1All c2All
+ | (_, L'.CUnif (_, _, _, ref (SOME c2All))) => unifyCons' env c1All c2All
- | (L'.CUnif (k1, _, r1), L'.CUnif (k2, _, r2)) =>
+ | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) =>
if r1 = r2 then
()
else
(unifyKinds k1 k2;
r1 := SOME c2All)
- | (L'.CUnif (_, _, r), _) =>
+ | (L'.CUnif (_, _, _, r), _) =>
if occursCon r c2All then
err COccursCheckFailed
else
r := SOME c2All
- | (_, L'.CUnif (_, _, r)) =>
+ | (_, L'.CUnif (_, _, _, r)) =>
if occursCon r c1All then
err COccursCheckFailed
else
@@ -898,7 +901,7 @@ fun elabHead env (e as (_, loc)) t =
case hnormCon env t of
(L'.TCFun (L'.Implicit, x, k, t'), _) =>
let
- val u = cunif k
+ val u = cunif (loc, k)
in
unravel (subConInCon (0, u) t',
(L'.ECApp (e, u), loc))
@@ -954,8 +957,8 @@ fun elabExp env (e, loc) =
val (e1', t1) = elabHead env e1' t1
val (e2', t2) = elabExp env e2
- val dom = cunif ktype
- val ran = cunif ktype
+ val dom = cunif (loc, ktype)
+ val ran = cunif (loc, ktype)
val t = (L'.TFun (dom, ran), dummy)
in
checkCon env e1' t1 t;
@@ -965,7 +968,7 @@ fun elabExp env (e, loc) =
| L.EAbs (x, to, e) =>
let
val t' = case to of
- NONE => cunif ktype
+ NONE => cunif (loc, ktype)
| SOME t =>
let
val (t', tk) = elabCon env t
@@ -1034,8 +1037,8 @@ fun elabExp env (e, loc) =
val (e', et) = elabExp env e
val (c', ck) = elabCon env c
- val ft = cunif ktype
- val rest = cunif ktype_record
+ val ft = cunif (loc, ktype)
+ val rest = cunif (loc, ktype_record)
in
checkKind env c' ck kname;
checkCon env e' et (L'.TRecord (L'.CConcat ((L'.CRecord (ktype, [(c', ft)]), loc), rest), loc), loc);
@@ -1044,36 +1047,22 @@ fun elabExp env (e, loc) =
| L.EFold =>
let
- val dom = kunif ()
+ val dom = kunif loc
in
((L'.EFold dom, loc), foldType (dom, loc))
end
datatype decl_error =
- KunifsRemainKind of ErrorMsg.span * L'.kind
- | KunifsRemainCon of ErrorMsg.span * L'.con
- | KunifsRemainExp of ErrorMsg.span * L'.exp
- | CunifsRemainCon of ErrorMsg.span * L'.con
- | CunifsRemainExp of ErrorMsg.span * L'.exp
+ KunifsRemain of ErrorMsg.span
+ | CunifsRemain of ErrorMsg.span
fun declError env err =
case err of
- KunifsRemainKind (loc, k) =>
- (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in kind";
- eprefaces' [("Kind", p_kind k)])
- | KunifsRemainCon (loc, c) =>
- (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in constructor";
- eprefaces' [("Constructor", p_con env c)])
- | KunifsRemainExp (loc, e) =>
- (ErrorMsg.errorAt loc "Some kind unification variables are undetermined in expression";
- eprefaces' [("Expression", p_exp env e)])
- | CunifsRemainCon (loc, c) =>
- (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in constructor";
- eprefaces' [("Constructor", p_con env c)])
- | CunifsRemainExp (loc, e) =>
- (ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in expression";
- eprefaces' [("Expression", p_exp env e)])
+ KunifsRemain loc =>
+ ErrorMsg.errorAt loc "Some kind unification variables are undetermined in declaration"
+ | CunifsRemain loc =>
+ ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in declaration"
datatype sgn_error =
UnboundSgn of ErrorMsg.span * string
@@ -1164,107 +1153,68 @@ fun strError env err =
val hnormSgn = E.hnormSgn
fun elabSgn_item ((sgi, loc), env) =
- let
-
- in
- resetKunif ();
- resetCunif ();
- case sgi of
- L.SgiConAbs (x, k) =>
- let
- val k' = elabKind k
-
- val (env', n) = E.pushCNamed env x k' NONE
- in
- if ErrorMsg.anyErrors () then
- ()
- else (
- if kunifsInKind k' then
- declError env (KunifsRemainKind (loc, k'))
- else
- ()
- );
-
- ([(L'.SgiConAbs (x, n, k'), loc)], env')
- end
-
- | L.SgiCon (x, ko, c) =>
- let
- val k' = case ko of
- NONE => kunif ()
- | SOME k => elabKind k
-
- val (c', ck) = elabCon env c
- val (env', n) = E.pushCNamed env x k' (SOME c')
- in
- checkKind env c' ck k';
-
- if ErrorMsg.anyErrors () then
- ()
- else (
- if kunifsInKind k' then
- declError env (KunifsRemainKind (loc, k'))
- else
- ();
+ case sgi of
+ L.SgiConAbs (x, k) =>
+ let
+ val k' = elabKind k
- if kunifsInCon c' then
- declError env (KunifsRemainCon (loc, c'))
- else
- ()
- );
+ val (env', n) = E.pushCNamed env x k' NONE
+ in
+ ([(L'.SgiConAbs (x, n, k'), loc)], env')
+ end
- ([(L'.SgiCon (x, n, k', c'), loc)], env')
- end
+ | L.SgiCon (x, ko, c) =>
+ let
+ val k' = case ko of
+ NONE => kunif loc
+ | SOME k => elabKind k
- | L.SgiVal (x, c) =>
- let
- val (c', ck) = elabCon env c
+ val (c', ck) = elabCon env c
+ val (env', n) = E.pushCNamed env x k' (SOME c')
+ in
+ checkKind env c' ck k';
- val (env', n) = E.pushENamed env x c'
- in
- (unifyKinds ck ktype
- handle KUnify ue => strError env (NotType (ck, ue)));
+ ([(L'.SgiCon (x, n, k', c'), loc)], env')
+ end
- if ErrorMsg.anyErrors () then
- ()
- else (
- if kunifsInCon c' then
- declError env (KunifsRemainCon (loc, c'))
- else
- ()
- );
+ | L.SgiVal (x, c) =>
+ let
+ val (c', ck) = elabCon env c
- ([(L'.SgiVal (x, n, c'), loc)], env')
- end
+ val (env', n) = E.pushENamed env x c'
+ in
+ (unifyKinds ck ktype
+ handle KUnify ue => strError env (NotType (ck, ue)));
- | L.SgiStr (x, sgn) =>
- let
- val sgn' = elabSgn env sgn
- val (env', n) = E.pushStrNamed env x sgn'
- in
- ([(L'.SgiStr (x, n, sgn'), loc)], env')
- end
+ ([(L'.SgiVal (x, n, c'), loc)], env')
+ end
- | L.SgiSgn (x, sgn) =>
- let
- val sgn' = elabSgn env sgn
- val (env', n) = E.pushSgnNamed env x sgn'
- in
- ([(L'.SgiSgn (x, n, sgn'), loc)], env')
- end
+ | L.SgiStr (x, sgn) =>
+ let
+ val sgn' = elabSgn env sgn
+ val (env', n) = E.pushStrNamed env x sgn'
+ in
+ ([(L'.SgiStr (x, n, sgn'), loc)], env')
+ end
- | L.SgiInclude sgn =>
- let
- val sgn' = elabSgn env sgn
- in
- case #1 (hnormSgn env sgn') of
- L'.SgnConst sgis =>
- (sgis, foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis)
- | _ => (sgnError env (NotIncludable sgn');
- ([], env))
- end
+ | L.SgiSgn (x, sgn) =>
+ let
+ val sgn' = elabSgn env sgn
+ val (env', n) = E.pushSgnNamed env x sgn'
+ in
+ ([(L'.SgiSgn (x, n, sgn'), loc)], env')
+ end
- end
+ | L.SgiInclude sgn =>
+ let
+ val sgn' = elabSgn env sgn
+ in
+ case #1 (hnormSgn env sgn') of
+ L'.SgnConst sgis =>
+ (sgis, foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis)
+ | _ => (sgnError env (NotIncludable sgn');
+ ([], env))
+ end
and elabSgn env (sgn, loc) =
case sgn of
@@ -1580,133 +1530,90 @@ fun subSgn env sgn1 (sgn2 as (_, loc2)) =
fun elabDecl ((d, loc), env) =
- let
-
- in
- resetKunif ();
- resetCunif ();
- case d of
- L.DCon (x, ko, c) =>
- let
- val k' = case ko of
- NONE => kunif ()
- | SOME k => elabKind k
-
- val (c', ck) = elabCon env c
- val (env', n) = E.pushCNamed env x k' (SOME c')
- in
- checkKind env c' ck k';
-
- if ErrorMsg.anyErrors () then
- ()
- else (
- if kunifsInKind k' then
- declError env (KunifsRemainKind (loc, k'))
- else
- ();
-
- if kunifsInCon c' then
- declError env (KunifsRemainCon (loc, c'))
- else
- ()
- );
+ case d of
+ L.DCon (x, ko, c) =>
+ let
+ val k' = case ko of
+ NONE => kunif loc
+ | SOME k => elabKind k
- ([(L'.DCon (x, n, k', c'), loc)], env')
- end
- | L.DVal (x, co, e) =>
- let
- val (c', ck) = case co of
- NONE => (cunif ktype, ktype)
- | SOME c => elabCon env c
+ val (c', ck) = elabCon env c
+ val (env', n) = E.pushCNamed env x k' (SOME c')
+ in
+ checkKind env c' ck k';
- val (e', et) = elabExp env e
- val (env', n) = E.pushENamed env x c'
- in
- checkCon env e' et c';
+ ([(L'.DCon (x, n, k', c'), loc)], env')
+ end
+ | L.DVal (x, co, e) =>
+ let
+ val (c', ck) = case co of
+ NONE => (cunif (loc, ktype), ktype)
+ | SOME c => elabCon env c
- if ErrorMsg.anyErrors () then
- ()
- else (
- if kunifsInCon c' then
- declError env (KunifsRemainCon (loc, c'))
- else
- ();
+ val (e', et) = elabExp env e
+ val (env', n) = E.pushENamed env x c'
+ in
+ checkCon env e' et c';
- if cunifsInCon c' then
- declError env (CunifsRemainCon (loc, c'))
- else
- ();
+ ([(L'.DVal (x, n, c', e'), loc)], env')
+ end
- if kunifsInExp e' then
- declError env (KunifsRemainExp (loc, e'))
- else
- ();
+ | L.DSgn (x, sgn) =>
+ let
+ val sgn' = elabSgn env sgn
+ val (env', n) = E.pushSgnNamed env x sgn'
+ in
+ ([(L'.DSgn (x, n, sgn'), loc)], env')
+ end
- if cunifsInExp e' then
- declError env (CunifsRemainExp (loc, e'))
- else
- ());
+ | L.DStr (x, sgno, str) =>
+ let
+ val formal = Option.map (elabSgn env) sgno
+ val (str', actual) = elabStr env str
- ([(L'.DVal (x, n, c', e'), loc)], env')
- end
+ val sgn' = case formal of
+ NONE => selfifyAt env {str = str', sgn = actual}
+ | SOME formal =>
+ (subSgn env actual formal;
+ formal)
- | L.DSgn (x, sgn) =>
- let
- val sgn' = elabSgn env sgn
- val (env', n) = E.pushSgnNamed env x sgn'
- in
- ([(L'.DSgn (x, n, sgn'), loc)], env')
- end
+ val (env', n) = E.pushStrNamed env x sgn'
+ in
+ case #1 (hnormSgn env sgn') of
+ L'.SgnFun _ =>
+ (case #1 str' of
+ L'.StrFun _ => ()
+ | _ => strError env (FunctorRebind loc))
+ | _ => ();
- | L.DStr (x, sgno, str) =>
- let
- val formal = Option.map (elabSgn env) sgno
- val (str', actual) = elabStr env str
+ ([(L'.DStr (x, n, sgn', str'), loc)], env')
+ end
- val sgn' = case formal of
- NONE => selfifyAt env {str = str', sgn = actual}
- | SOME formal =>
- (subSgn env actual formal;
- formal)
+ | L.DFfiStr (x, sgn) =>
+ let
+ val sgn' = elabSgn env sgn
- val (env', n) = E.pushStrNamed env x sgn'
- in
- case #1 (hnormSgn env sgn') of
- L'.SgnFun _ =>
- (case #1 str' of
- L'.StrFun _ => ()
- | _ => strError env (FunctorRebind loc))
- | _ => ();
-
- ([(L'.DStr (x, n, sgn', str'), loc)], env')
- end
+ val (env', n) = E.pushStrNamed env x sgn'
+ in
+ ([(L'.DFfiStr (x, n, sgn'), loc)], env')
+ end
- | L.DFfiStr (x, sgn) =>
+ | L.DOpen (m, ms) =>
+ case E.lookupStr env m of
+ NONE => (strError env (UnboundStr (loc, m));
+ ([], env))
+ | SOME (n, sgn) =>
let
- val sgn' = elabSgn env sgn
-
- val (env', n) = E.pushStrNamed env x sgn'
+ val (_, sgn) = foldl (fn (m, (str, sgn)) =>
+ case E.projectStr env {str = str, sgn = sgn, field = m} of
+ NONE => (strError env (UnboundStr (loc, m));
+ (strerror, sgnerror))
+ | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+ ((L'.StrVar n, loc), sgn) ms
in
- ([(L'.DFfiStr (x, n, sgn'), loc)], env')
+ dopen env {str = n, strs = ms, sgn = sgn}
end
- | L.DOpen (m, ms) =>
- (case E.lookupStr env m of
- NONE => (strError env (UnboundStr (loc, m));
- ([], env))
- | SOME (n, sgn) =>
- let
- val (_, sgn) = foldl (fn (m, (str, sgn)) =>
- case E.projectStr env {str = str, sgn = sgn, field = m} of
- NONE => (strError env (UnboundStr (loc, m));
- (strerror, sgnerror))
- | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
- ((L'.StrVar n, loc), sgn) ms
- in
- dopen env {str = n, strs = ms, sgn = sgn}
- end)
- end
-
and elabStr env (str, loc) =
case str of
L.StrConst ds =>
@@ -1844,7 +1751,30 @@ fun elabFile basis env file =
val () = discoverC float "float"
val () = discoverC string "string"
- val (file, _) = ListUtil.foldlMapConcat elabDecl env' file
+ fun elabDecl' (d, env) =
+ let
+ val () = resetKunif ()
+ val () = resetCunif ()
+ val (ds, env) = elabDecl (d, env)
+ in
+ if ErrorMsg.anyErrors () then
+ ()
+ else (
+ if List.exists kunifsInDecl ds then
+ declError env (KunifsRemain (#2 d))
+ else
+ ();
+
+ case ListUtil.search cunifsInDecl ds of
+ NONE => ()
+ | SOME loc =>
+ declError env (CunifsRemain loc)
+ );
+
+ (ds, env)
+ end
+
+ val (file, _) = ListUtil.foldlMapConcat elabDecl' env' file
in
(L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ file
end
diff --git a/src/explify.sml b/src/explify.sml
index 91accd81..0f416067 100644
--- a/src/explify.sml
+++ b/src/explify.sml
@@ -39,7 +39,7 @@ fun explifyKind (k, loc) =
| L.KRecord k => (L'.KRecord (explifyKind k), loc)
| L.KError => raise Fail ("explifyKind: KError at " ^ EM.spanToString loc)
- | L.KUnif (_, ref (SOME k)) => explifyKind k
+ | L.KUnif (_, _, ref (SOME k)) => explifyKind k
| L.KUnif _ => raise Fail ("explifyKind: KUnif at " ^ EM.spanToString loc)
fun explifyCon (c, loc) =
@@ -62,7 +62,7 @@ fun explifyCon (c, loc) =
| L.CFold (dom, ran) => (L'.CFold (explifyKind dom, explifyKind ran), loc)
| L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc)
- | L.CUnif (_, _, ref (SOME c)) => explifyCon c
+ | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c
| L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc)
fun explifyExp (e, loc) =
diff --git a/tests/broad_unif.lac b/tests/broad_unif.lac
new file mode 100644
index 00000000..bebd9104
--- /dev/null
+++ b/tests/broad_unif.lac
@@ -0,0 +1,15 @@
+structure M = struct
+ type t = int
+ val f = fn x => x
+ val y = f 0
+end
+
+signature S = sig
+ type t
+ val f : t -> t
+end
+
+structure M : S = struct
+ type t = int
+ val f = fn x => x
+end