changeset 1359:e525ad571e15

Recursive record unification errors, for more detail
author Adam Chlipala <adam@chlipala.net>
date Thu, 23 Dec 2010 11:23:31 -0500
parents 32c8a3509369
children 02fc16faecf3
files include/urweb.h lib/ur/basis.urs src/c/urweb.c src/elab_err.sig src/elab_err.sml src/elaborate.sml src/sqlite.sml
diffstat 7 files changed, 19 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/include/urweb.h	Tue Dec 21 18:01:23 2010 -0500
+++ b/include/urweb.h	Thu Dec 23 11:23:31 2010 -0500
@@ -297,7 +297,7 @@
 
 failure_kind uw_runCallback(uw_context, void (*callback)(uw_context));
 
-uw_Basis_string uw_Basis_timeToStringf(uw_context, const char *fmt, uw_Basis_time);
+uw_Basis_string uw_Basis_timef(uw_context, const char *fmt, uw_Basis_time);
 uw_Basis_time uw_Basis_stringToTimef(uw_context, const char *fmt, uw_Basis_string);
 uw_Basis_time uw_Basis_stringToTimef_error(uw_context, const char *fmt, uw_Basis_string);
 
--- a/lib/ur/basis.urs	Tue Dec 21 18:01:23 2010 -0500
+++ b/lib/ur/basis.urs	Thu Dec 23 11:23:31 2010 -0500
@@ -143,6 +143,7 @@
 val now : transaction time
 val minTime : time
 val minusSeconds : time -> int -> time
+val timef : string -> time -> string (* Uses strftime() format string *)
 
 
 (** HTTP operations *)
--- a/src/c/urweb.c	Tue Dec 21 18:01:23 2010 -0500
+++ b/src/c/urweb.c	Thu Dec 23 11:23:31 2010 -0500
@@ -2582,7 +2582,7 @@
     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;
--- a/src/elab_err.sig	Tue Dec 21 18:01:23 2010 -0500
+++ b/src/elab_err.sig	Thu Dec 23 11:23:31 2010 -0500
@@ -55,7 +55,7 @@
            | 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
--- a/src/elab_err.sml	Tue Dec 21 18:01:23 2010 -0500
+++ b/src/elab_err.sml	Thu Dec 23 11:23:31 2010 -0500
@@ -118,7 +118,7 @@
        | 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 @@
                   [("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))])
--- a/src/elaborate.sml	Tue Dec 21 18:01:23 2010 -0500
+++ b/src/elaborate.sml	Thu Dec 23 11:23:31 2010 -0500
@@ -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
--- a/src/sqlite.sml	Tue Dec 21 18:01:23 2010 -0500
+++ b/src/sqlite.sml	Thu Dec 23 11:23:31 2010 -0500
@@ -597,7 +597,7 @@
                                                      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,