diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2010-12-23 11:23:31 -0500 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2010-12-23 11:23:31 -0500 |
| commit | 867a11af44827af8974250e6dbb5e96b6268b44f (patch) | |
| tree | fcdcc73abd3ef7b68fe8a02e5b11901e0fec5c92 /src | |
| parent | 17ecbd235ad9b7692dfc029329fb13103eb55d9c (diff) | |
Recursive record unification errors, for more detail
Diffstat (limited to 'src')
| -rw-r--r-- | src/c/urweb.c | 2 | ||||
| -rw-r--r-- | src/elab_err.sig | 2 | ||||
| -rw-r--r-- | src/elab_err.sml | 23 | ||||
| -rw-r--r-- | src/elaborate.sml | 2 | ||||
| -rw-r--r-- | src/sqlite.sml | 2 |
5 files changed, 17 insertions, 14 deletions
diff --git a/src/c/urweb.c b/src/c/urweb.c index d3b8c770..a09978cd 100644 --- a/src/c/urweb.c +++ b/src/c/urweb.c @@ -2582,7 +2582,7 @@ uw_Basis_string uw_Basis_timeToString(uw_context ctx, uw_Basis_time t) { return "<Invalid time>"; } -uw_Basis_string uw_Basis_timeToStringf(uw_context ctx, const char *fmt, uw_Basis_time t) { +uw_Basis_string uw_Basis_timef(uw_context ctx, const char *fmt, uw_Basis_time t) { size_t len; char *r; struct tm stm; diff --git a/src/elab_err.sig b/src/elab_err.sig index 3dfd5d4e..a66cf61f 100644 --- a/src/elab_err.sig +++ b/src/elab_err.sig @@ -55,7 +55,7 @@ signature ELAB_ERR = sig | CIncompatible of Elab.con * Elab.con | CExplicitness of Elab.con * Elab.con | CKindof of Elab.kind * Elab.con * string - | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con) option + | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con * cunify_error option) option | TooLifty of ErrorMsg.span * ErrorMsg.span | TooUnify of Elab.con * Elab.con | TooDeep diff --git a/src/elab_err.sml b/src/elab_err.sml index 7d5e6be8..a03bc096 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -118,7 +118,7 @@ datatype cunify_error = | CIncompatible of con * con | CExplicitness of con * con | CKindof of kind * con * string - | CRecordFailure of con * con * (con * con * con) option + | CRecordFailure of con * con * (con * con * con * cunify_error option) option | TooLifty of ErrorMsg.span * ErrorMsg.span | TooUnify of con * con | TooDeep @@ -147,15 +147,18 @@ fun cunifyError env err = [("Kind", p_kind env k), ("Con", p_con env c)] | CRecordFailure (c1, c2, fo) => - eprefaces "Can't unify record constructors" - (("Summary 1", p_con env c1) - :: ("Summary 2", p_con env c2) - :: (case fo of - NONE => [] - | SOME (nm, t1, t2) => - [("Field", p_con env nm), - ("Value 1", p_con env t1), - ("Value 2", p_con env t2)])) + (eprefaces "Can't unify record constructors" + (("Summary 1", p_con env c1) + :: ("Summary 2", p_con env c2) + :: (case fo of + NONE => [] + | SOME (nm, t1, t2, _) => + [("Field", p_con env nm), + ("Value 1", p_con env t1), + ("Value 2", p_con env t2)])); + case fo of + SOME (_, _, _, SOME err') => cunifyError env err' + | _ => ()) | TooLifty (loc1, loc2) => (ErrorMsg.errorAt loc1 "Can't unify two unification variables that both have suspended liftings"; eprefaces' [("Other location", Print.PD.string (ErrorMsg.spanToString loc2))]) diff --git a/src/elaborate.sml b/src/elaborate.sml index c791cff6..4e59a8ed 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -907,7 +907,7 @@ if consEq env loc (c1, c2) then findPointwise fs1 else - SOME (nm1, c1, c2) + SOME (nm1, c1, c2, (unifyCons env loc c1 c2; NONE) handle CUnify (_, _, err) => SOME err) in raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2, findPointwise (#fields s1))) end diff --git a/src/sqlite.sml b/src/sqlite.sml index e668f53a..efa6eb12 100644 --- a/src/sqlite.sml +++ b/src/sqlite.sml @@ -597,7 +597,7 @@ fun p_inputs loc = string ")"] | Time => box [string "sqlite3_bind_text(stmt, ", string (Int.toString (i + 1)), - string ", uw_Basis_timeToStringf(ctx, ", + string ", uw_Basis_timef(ctx, ", string fmt, string ", ", arg, |