summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/elab.sml3
-rw-r--r--src/elab_print.sml55
-rw-r--r--src/elab_util.sml21
-rw-r--r--src/elaborate.sml306
-rw-r--r--src/lacweb.grm7
-rw-r--r--src/source.sml3
-rw-r--r--src/source_print.sml13
-rw-r--r--tests/stuff.lac20
8 files changed, 373 insertions, 55 deletions
diff --git a/src/elab.sml b/src/elab.sml
index a289d633..b08d9a6c 100644
--- a/src/elab.sml
+++ b/src/elab.sml
@@ -72,6 +72,9 @@ datatype exp' =
| ECApp of exp * con
| ECAbs of explicitness * string * kind * exp
+ | ERecord of (con * exp) list
+ | EField of exp * con * { field : con, rest : con }
+
| EError
withtype exp = exp' located
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 83e8f814..c11b0da1 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -115,15 +115,26 @@ fun p_con' par env (c, _) =
| CName s => box [string "#", string s]
- | CRecord (k, xcs) => parenIf par (box [string "[",
- p_list (fn (x, c) =>
- box [p_con env x,
- space,
- string "=",
- space,
- p_con env c]) xcs,
- string "]::",
- p_kind k])
+ | CRecord (k, xcs) =>
+ if !debug then
+ parenIf par (box [string "[",
+ p_list (fn (x, c) =>
+ box [p_con env x,
+ space,
+ string "=",
+ space,
+ p_con env c]) xcs,
+ string "]::",
+ p_kind k])
+ else
+ parenIf par (box [string "[",
+ p_list (fn (x, c) =>
+ box [p_con env x,
+ space,
+ string "=",
+ space,
+ p_con env c]) xcs,
+ string "]"])
| CConcat (c1, c2) => parenIf par (box [p_con' true env c1,
space,
string "++",
@@ -181,6 +192,32 @@ fun p_exp' par env (e, _) =
space,
p_exp (E.pushCRel env x k) e])
+ | ERecord xes => box [string "{",
+ p_list (fn (x, e) =>
+ box [p_con env x,
+ space,
+ string "=",
+ space,
+ p_exp env e]) xes,
+ string "}"]
+ | EField (e, c, {field, rest}) =>
+ if !debug then
+ box [p_exp' true env e,
+ string ".",
+ p_con' true env c,
+ space,
+ string "[",
+ p_con env field,
+ space,
+ string " in ",
+ space,
+ p_con env rest,
+ string "]"]
+ else
+ box [p_exp' true env e,
+ string ".",
+ p_con' true env c]
+
| EError => string "<ERROR>"
and p_exp env = p_exp' false env
diff --git a/src/elab_util.sml b/src/elab_util.sml
index 2550f638..56be1328 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -233,6 +233,27 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
fn e' =>
(ECAbs (expl, x, k', e'), loc)))
+ | ERecord xes =>
+ S.map2 (ListUtil.mapfold (fn (x, e) =>
+ S.bind2 (mfc ctx x,
+ fn x' =>
+ S.map2 (mfe ctx e,
+ fn e' =>
+ (x', e'))))
+ xes,
+ fn xes' =>
+ (ERecord xes', loc))
+ | EField (e, c, {field, rest}) =>
+ S.bind2 (mfe ctx e,
+ fn e' =>
+ S.bind2 (mfc ctx c,
+ fn c' =>
+ S.bind2 (mfc ctx field,
+ fn field' =>
+ S.map2 (mfc ctx rest,
+ fn rest' =>
+ (EField (e', c', {field = field', rest = rest'}), loc)))))
+
| EError => S.return2 eAll
in
mfe
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 0b705fea..9d672869 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -136,6 +136,7 @@ val dummy = ErrorMsg.dummySpan
val ktype = (L'.KType, dummy)
val kname = (L'.KName, dummy)
+val ktype_record = (L'.KRecord ktype, dummy)
val cerror = (L'.CError, dummy)
val kerror = (L'.KError, dummy)
@@ -313,6 +314,8 @@ datatype cunify_error =
| COccursCheckFailed of L'.con * L'.con
| CIncompatible of L'.con * L'.con
| CExplicitness of L'.con * L'.con
+ | CKindof of L'.con
+ | CRecordFailure
exception CUnify' of cunify_error
@@ -335,8 +338,212 @@ fun cunifyError env err =
eprefaces "Differing constructor function explicitness"
[("Con 1", p_con env c1),
("Con 2", p_con env c2)]
+ | CKindof c =>
+ eprefaces "Kind unification variable blocks kindof calculation"
+ [("Con", p_con env c)]
+ | CRecordFailure =>
+ eprefaces "Can't unify record constructors" []
-fun hnormCon env (cAll as (c, _)) =
+exception SynUnif
+
+val liftConInCon =
+ U.Con.mapB {kind = fn k => k,
+ con = fn bound => fn c =>
+ case c of
+ L'.CRel xn =>
+ if xn < bound then
+ c
+ else
+ L'.CRel (xn + 1)
+ | L'.CUnif _ => raise SynUnif
+ | _ => c,
+ bind = fn (bound, U.Con.Rel _) => bound + 1
+ | (bound, _) => bound}
+
+val subConInCon =
+ U.Con.mapB {kind = fn k => k,
+ con = fn (xn, rep) => fn c =>
+ case c of
+ L'.CRel xn' =>
+ if xn = xn' then
+ #1 rep
+ else
+ c
+ | L'.CUnif _ => raise SynUnif
+ | _ => c,
+ bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
+ | (ctx, _) => ctx}
+
+type record_summary = {
+ fields : (L'.con * L'.con) list,
+ unifs : (L'.con * L'.con option ref) list,
+ others : L'.con list
+}
+
+fun summaryToCon {fields, unifs, others} =
+ let
+ val c = (L'.CRecord (ktype, []), dummy)
+ val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others
+ val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs
+ in
+ (L'.CConcat ((L'.CRecord (ktype, fields), dummy), c), dummy)
+ end
+
+fun p_summary env s = p_con env (summaryToCon s)
+
+exception CUnify of L'.con * L'.con * cunify_error
+
+fun hnormKind (kAll as (k, _)) =
+ case k of
+ L'.KUnif (_, ref (SOME k)) => hnormKind k
+ | _ => kAll
+
+fun kindof env (c, loc) =
+ case c of
+ L'.TFun _ => ktype
+ | L'.TCFun _ => ktype
+ | L'.TRecord _ => ktype
+
+ | L'.CRel xn => #2 (E.lookupCRel env xn)
+ | L'.CNamed xn => #2 (E.lookupCNamed env xn)
+ | L'.CApp (c, _) =>
+ (case #1 (hnormKind (kindof env c)) of
+ L'.KArrow (_, k) => k
+ | L'.KError => kerror
+ | _ => raise CUnify' (CKindof c))
+ | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc)
+
+ | L'.CName _ => kname
+
+ | L'.CRecord (k, _) => (L'.KRecord k, loc)
+ | L'.CConcat (c, _) => kindof env c
+
+ | L'.CError => kerror
+ | L'.CUnif (k, _, _) => k
+
+fun unifyRecordCons env (c1, c2) =
+ let
+ val k1 = kindof env c1
+ val k2 = kindof env c2
+ in
+ unifyKinds k1 k2;
+ unifySummaries env (k1, recordSummary env c1, recordSummary env c2)
+ end
+
+and recordSummary env c : record_summary =
+ case hnormCon env c of
+ (L'.CRecord (_, xcs), _) => {fields = xcs, unifs = [], others = []}
+ | (L'.CConcat (c1, c2), _) =>
+ let
+ val s1 = recordSummary env c1
+ val s2 = recordSummary env c2
+ in
+ {fields = #fields s1 @ #fields s2,
+ 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 = []}
+ | c' => {fields = [], unifs = [], others = [c']}
+
+and consEq env (c1, c2) =
+ (unifyCons env c1 c2;
+ true)
+ handle CUnify _ => false
+
+and unifySummaries env (k, s1 : record_summary, s2 : record_summary) =
+ let
+ val () = eprefaces "Summaries" [("#1", p_summary env s1),
+ ("#2", p_summary env s2)]
+
+ fun eatMatching p (ls1, ls2) =
+ let
+ fun em (ls1, ls2, passed1) =
+ case ls1 of
+ [] => (rev passed1, ls2)
+ | h1 :: t1 =>
+ let
+ fun search (ls2', passed2) =
+ case ls2' of
+ [] => em (t1, ls2, h1 :: passed1)
+ | h2 :: t2 =>
+ if p (h1, h2) then
+ em (t1, List.revAppend (passed2, t2), passed1)
+ else
+ search (t2, h2 :: passed2)
+ in
+ search (ls2, [])
+ end
+ in
+ em (ls1, ls2, [])
+ end
+
+ val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) =>
+ if consEq env (x1, x2) then
+ (unifyCons env c1 c2;
+ true)
+ else
+ false) (#fields s1, #fields s2)
+ val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}),
+ ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]
+ val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2)
+ val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2)
+
+ fun unifFields (fs, others, unifs) =
+ case (fs, others, unifs) of
+ ([], [], _) => ([], [], unifs)
+ | (_, _, []) => (fs, others, [])
+ | (_, _, (_, r) :: rest) =>
+ let
+ val r' = ref NONE
+ val cr' = (L'.CUnif (k, "recd", r'), dummy)
+
+ val prefix = case (fs, others) of
+ ([], other :: others) =>
+ List.foldl (fn (other, c) =>
+ (L'.CConcat (c, other), dummy))
+ other others
+ | (fs, []) =>
+ (L'.CRecord (k, fs), dummy)
+ | (fs, others) =>
+ List.foldl (fn (other, c) =>
+ (L'.CConcat (c, other), dummy))
+ (L'.CRecord (k, fs), dummy) others
+ in
+ r := SOME (L'.CConcat (prefix, cr'), dummy);
+ ([], [], (cr', r') :: rest)
+ end
+
+ val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2)
+ val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1)
+
+ val clear1 = case (fs1, others1) of
+ ([], []) => true
+ | _ => false
+ val clear2 = case (fs2, others2) of
+ ([], []) => true
+ | _ => false
+ val empty = (L'.CRecord (k, []), dummy)
+ fun pairOffUnifs (unifs1, unifs2) =
+ case (unifs1, unifs2) of
+ ([], _) =>
+ if clear1 then
+ List.app (fn (_, r) => r := SOME empty) unifs2
+ else
+ raise CUnify' CRecordFailure
+ | (_, []) =>
+ if clear2 then
+ List.app (fn (_, r) => r := SOME empty) unifs1
+ else
+ raise CUnify' CRecordFailure
+ | ((c1, _) :: rest1, (_, r2) :: rest2) =>
+ (r2 := SOME c1;
+ pairOffUnifs (rest1, rest2))
+ in
+ pairOffUnifs (unifs1, unifs2)
+ end
+
+and hnormCon env (cAll as (c, _)) =
case c of
L'.CUnif (_, _, ref (SOME c)) => hnormCon env c
@@ -345,14 +552,29 @@ fun hnormCon env (cAll as (c, _)) =
(_, _, SOME c') => hnormCon env c'
| _ => cAll)
+ | L'.CApp (c1, c2) =>
+ (case hnormCon env c1 of
+ (L'.CAbs (_, _, cb), _) =>
+ ((hnormCon env (subConInCon (0, c2) cb))
+ handle SynUnif => cAll)
+ | _ => cAll)
+
+ | L'.CConcat (c1, c2) =>
+ (case (hnormCon env c1, hnormCon env c2) of
+ ((L'.CRecord (k, xcs1), loc), (L'.CRecord (_, xcs2), _)) =>
+ (L'.CRecord (k, xcs1 @ xcs2), loc)
+ | _ => cAll)
+
| _ => cAll
-fun unifyCons' env c1 c2 =
+and unifyCons' env c1 c2 =
unifyCons'' env (hnormCon env c1) (hnormCon env c2)
and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) =
let
fun err f = raise CUnify' (f (c1All, c2All))
+
+ fun isRecord () = unifyRecordCons env (c1All, c2All)
in
case (c1, c2) of
(L'.TFun (d1, r1), L'.TFun (d2, r2)) =>
@@ -390,17 +612,6 @@ and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) =
else
err CIncompatible
- | (L'.CRecord (k1, rs1), L'.CRecord (k2, rs2)) =>
- (unifyKinds k1 k2;
- ((ListPair.appEq (fn ((n1, v1), (n2, v2)) =>
- (unifyCons' env n1 n2;
- unifyCons' env v1 v2)) (rs1, rs2))
- handle ListPair.UnequalLengths => err CIncompatible))
- | (L'.CConcat (d1, r1), L'.CConcat (d2, r2)) =>
- (unifyCons' env d1 d2;
- unifyCons' env r1 r2)
-
-
| (L'.CError, _) => ()
| (_, L'.CError) => ()
@@ -425,12 +636,15 @@ and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) =
else
r := SOME c1All
+ | (L'.CRecord _, _) => isRecord ()
+ | (_, L'.CRecord _) => isRecord ()
+ | (L'.CConcat _, _) => isRecord ()
+ | (_, L'.CConcat _) => isRecord ()
+
| _ => err CIncompatible
end
-exception CUnify of L'.con * L'.con * cunify_error
-
-fun unifyCons env c1 c2 =
+and unifyCons env c1 c2 =
unifyCons' env c1 c2
handle CUnify' err => raise CUnify (c1, c2, err)
| KUnify args => raise CUnify (c1, c2, CKind args)
@@ -464,36 +678,6 @@ fun checkCon env e c1 c2 =
handle CUnify (c1, c2, err) =>
expError env (Unify (e, c1, c2, err))
-exception SynUnif
-
-val liftConInCon =
- U.Con.mapB {kind = fn k => k,
- con = fn bound => fn c =>
- case c of
- L'.CRel xn =>
- if xn < bound then
- c
- else
- L'.CRel (xn + 1)
- | L'.CUnif _ => raise SynUnif
- | _ => c,
- bind = fn (bound, U.Con.Rel _) => bound + 1
- | (bound, _) => bound}
-
-val subConInCon =
- U.Con.mapB {kind = fn k => k,
- con = fn (xn, rep) => fn c =>
- case c of
- L'.CRel xn' =>
- if xn = xn' then
- #1 rep
- else
- c
- | L'.CUnif _ => raise SynUnif
- | _ => c,
- bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep)
- | (ctx, _) => ctx}
-
fun elabExp env (e, loc) =
case e of
L.EAnnot (e, t) =>
@@ -576,6 +760,35 @@ fun elabExp env (e, loc) =
(L'.TCFun (expl', x, k', et), loc))
end
+ | L.ERecord xes =>
+ let
+ val xes' = map (fn (x, e) =>
+ let
+ val (x', xk) = elabCon env x
+ val (e', et) = elabExp env e
+ in
+ checkKind env x' xk kname;
+ (x', e', et)
+ end) xes
+ in
+ ((L'.ERecord (map (fn (x', e', _) => (x', e')) xes'), loc),
+ (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc))
+ end
+
+ | L.EField (e, c) =>
+ let
+ val (e', et) = elabExp env e
+ val (c', ck) = elabCon env c
+
+ val ft = cunif ktype
+ val rest = cunif 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);
+ ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft)
+ end
+
+
datatype decl_error =
KunifsRemainKind of ErrorMsg.span * L'.kind
| KunifsRemainCon of ErrorMsg.span * L'.con
@@ -603,6 +816,7 @@ fun declError env err =
fun elabDecl env (d, loc) =
(resetKunif ();
+ resetCunif ();
case d of
L.DCon (x, ko, c) =>
let
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 9d7079e4..80b35510 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -62,6 +62,7 @@ val s = ErrorMsg.spanOf
| eexp of exp
| eapps of exp
| eterm of exp
+ | rexp of (con * exp) list
%verbose (* print summary of errors *)
%pos int (* positions *)
@@ -147,7 +148,13 @@ eexp : eapps (eapps)
| FN SYMBOL DARROW eexp (EAbs (SYMBOL, NONE, eexp), s (FNleft, eexpright))
| LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright))
+ | eterm DOT ident (EField (eterm, ident), s (etermleft, identright))
eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright))
| SYMBOL (EVar SYMBOL, s (SYMBOLleft, SYMBOLright))
+ | LBRACE rexp RBRACE (ERecord rexp, s (LBRACEleft, RBRACEright))
+
+rexp : ([])
+ | ident EQ eexp ([(ident, eexp)])
+ | ident EQ eexp COMMA rexp ((ident, eexp) :: rexp)
diff --git a/src/source.sml b/src/source.sml
index d574141c..05b2973f 100644
--- a/src/source.sml
+++ b/src/source.sml
@@ -68,6 +68,9 @@ datatype exp' =
| ECApp of exp * con
| ECAbs of explicitness * string * kind * exp
+ | ERecord of (con * exp) list
+ | EField of exp * con
+
withtype exp = exp' located
datatype decl' =
diff --git a/src/source_print.sml b/src/source_print.sml
index b81a82df..de9e2c7c 100644
--- a/src/source_print.sml
+++ b/src/source_print.sml
@@ -170,6 +170,19 @@ fun p_exp' par (e, _) =
space,
p_exp e])
+ | ERecord xes => box [string "{",
+ p_list (fn (x, e) =>
+ box [p_con x,
+ space,
+ string "=",
+ space,
+ p_exp e]) xes,
+ string "}"]
+ | EField (e, c) => box [p_exp' true e,
+ string ".",
+ p_con' true c]
+
+
and p_exp e = p_exp' false e
fun p_decl ((d, _) : decl) =
diff --git a/tests/stuff.lac b/tests/stuff.lac
index 8348f5a1..806e4dfe 100644
--- a/tests/stuff.lac
+++ b/tests/stuff.lac
@@ -16,3 +16,23 @@ con c10 = ([]) :: {Type}
val v1 = fn t :: Type => fn x : t => x
val v2 = v1 [t :: Type -> t -> t] v1
+
+val r = {X = v1, Y = v2}
+val v1_again = r.X
+val v2_again = r.Y
+
+val r2 = {X = {}, Y = v2, Z = {}}
+val r2_X = r2.X
+val r2_Y = r2.Y
+val r2_Z = r2.Z
+
+val f = fn fs :: {Type} => fn x : $([X = {}] ++ fs) => x.X
+val f2 = fn fs :: {Type} => fn x : $(fs ++ [X = {}]) => x.X
+val f3 = fn fs :: {Type} => fn x : $([X = {}, Y = {Z : {}}] ++ fs) => x.X
+val f4 = fn fs :: {Type} => fn x : $([X = {}, Y = {Z : {}}] ++ fs) => x.Y
+val f5 = fn fs1 :: {Type} => fn fs2 :: {Type} => fn x : $(fs1 ++ [X = {}] ++ fs2) => x.X
+val f6 = fn fs1 :: {Type} => fn fs2 :: {Type} => fn x : $(fs1 ++ [X = {}] ++ fs2 ++ [Y = {Z : {}}]) => x.X
+val f7 = fn fs1 :: {Type} => fn fs2 :: {Type} => fn x : $(fs1 ++ [X = {}] ++ fs2 ++ [Y = {Z : {}}]) => x.Y
+
+val test = f [[Y = t :: Type -> t -> t, Z = {}]] r2
+val test = f7 [[Y = t :: Type -> t -> t]] [[Z = {}]] r2
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 05:51:28 +0000