From 46d562fc3d06a5ef8b17e90c7a4dfd0547757294 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 13 Dec 2009 11:28:47 -0500 Subject: Better record summary error messages; more tweaking SQL usability --- lib/ur/basis.urs | 3 +++ src/elab_err.sig | 2 +- src/elab_err.sml | 14 ++++++++++---- src/elaborate.sml | 19 ++++++++++++++++++- src/elisp/urweb-mode.el | 4 ++-- src/monoize.sml | 14 ++++++++++++++ src/urweb.grm | 4 +++- src/urweb.lex | 1 + 8 files changed, 52 insertions(+), 9 deletions(-) diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index 4b53659d..9bba1ee1 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -344,6 +344,9 @@ val sql_relop : tables1 ::: {{Type}} -> sql_query1 tables1 selectedFields selectedExps -> sql_query1 tables2 selectedFields selectedExps -> sql_query1 selectedFields selectedFields selectedExps +val sql_forget_tables : tables ::: {{Type}} -> selectedFields ::: {{Type}} -> selectedExps ::: {Type} + -> sql_query1 tables selectedFields selectedExps + -> sql_query1 selectedFields selectedFields selectedExps type sql_direction val sql_asc : sql_direction diff --git a/src/elab_err.sig b/src/elab_err.sig index 18596d04..f6277488 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 + | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con) option val cunifyError : ElabEnv.env -> cunify_error -> unit diff --git a/src/elab_err.sml b/src/elab_err.sml index 6d9bd2e6..80de9497 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -119,7 +119,7 @@ datatype cunify_error = | CIncompatible of con * con | CExplicitness of con * con | CKindof of kind * con * string - | CRecordFailure of con * con + | CRecordFailure of con * con * (con * con * con) option fun cunifyError env err = case err of @@ -144,10 +144,16 @@ fun cunifyError env err = eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")") [("Kind", p_kind env k), ("Con", p_con env c)] - | CRecordFailure (c1, c2) => + | CRecordFailure (c1, c2, fo) => eprefaces "Can't unify record constructors" - [("Summary 1", p_con env c1), - ("Summary 2", p_con env c2)] + (("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)])) datatype exp_error = UnboundExp of ErrorMsg.span * string diff --git a/src/elaborate.sml b/src/elaborate.sml index eccc4840..71842ec2 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -817,7 +817,24 @@ ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) val empty = (L'.CRecord (k, []), loc) - fun failure () = raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2)) + fun failure () = + let + val fs2 = #fields s2 + + fun findPointwise fs1 = + case fs1 of + [] => NONE + | (nm1, c1) :: fs1 => + case List.find (fn (nm2, _) => consEq env loc (nm1, nm2)) fs2 of + NONE => findPointwise fs1 + | SOME (_, c2) => + if consEq env loc (c1, c2) then + findPointwise fs1 + else + SOME (nm1, c1, c2) + in + raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2, findPointwise (#fields s1))) + end in (case (unifs1, fs1, others1, unifs2, fs2, others2) of (_, [], [], [], [], []) => diff --git a/src/elisp/urweb-mode.el b/src/elisp/urweb-mode.el index 42846e6c..72005af9 100644 --- a/src/elisp/urweb-mode.el +++ b/src/elisp/urweb-mode.el @@ -150,7 +150,7 @@ See doc for the variable `urweb-mode-info'." "ASC" "DESC" "INSERT" "INTO" "VALUES" "UPDATE" "SET" "DELETE" "PRIMARY" "KEY" "CONSTRAINT" "UNIQUE" "CHECK" "FOREIGN" "REFERENCES" "ON" "NO" "ACTION" "CASCADE" "RESTRICT" "NULL" - "JOIN" "INNER" "OUTER" "LEFT" "RIGHT" "FULL" "CROSS") + "JOIN" "INNER" "OUTER" "LEFT" "RIGHT" "FULL" "CROSS" "SELECT1") "A regexp that matches SQL keywords.") (defconst urweb-lident-regexp "\\<[a-z_][A-Za-z0-9_']*\\>" @@ -530,7 +530,7 @@ If anyone has a good algorithm for this..." (current-indentation))) (defconst urweb-sql-main-starters - '("SQL" "SELECT" "INSERT" "UPDATE" "DELETE")) + '("SQL" "SELECT" "INSERT" "UPDATE" "DELETE" "FROM" "SELECT1" "WHERE")) (defconst urweb-sql-starters (append urweb-sql-main-starters diff --git a/src/monoize.sml b/src/monoize.sml index f3c8b5f6..3998a49f 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -2292,6 +2292,20 @@ fun monoExp (env, st, fm) (all as (e, loc)) = sc "))"]), loc)), loc)), loc), fm) end + | L.ECApp ( + (L.ECApp ( + (L.ECApp ( + (L.EFfi ("Basis", "sql_forget_tables"), _), + _), _), + _), _), + _) => + let + val s = (L'.TFfi ("Basis", "string"), loc) + fun sc s = (L'.EPrim (Prim.String s), loc) + in + ((L'.EAbs ("x", s, s, (L'.ERel 0, loc)), loc), + fm) + end | L.EFfi ("Basis", "sql_union") => ((L'.EPrim (Prim.String "UNION"), loc), fm) | L.EFfi ("Basis", "sql_intersect") => ((L'.EPrim (Prim.String "INTERSECT"), loc), fm) diff --git a/src/urweb.grm b/src/urweb.grm index da40945a..87a8547d 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -199,7 +199,7 @@ fun patType loc (p : pat) = | ARROW | LARROW | DARROW | STAR | SEMI | KARROW | DKARROW | BANG | FN | PLUSPLUS | MINUSMINUS | MINUSMINUSMINUS | DOLLAR | TWIDDLE | CARET | LET | IN - | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | SQL + | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | SQL | SELECT1 | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS | EXPORT | TABLE | SEQUENCE | VIEW | COOKIE | STYLE | CASE | IF | THEN | ELSE | ANDALSO | ORELSE @@ -1170,6 +1170,7 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) | LPAREN CWHERE sqlexp RPAREN (sqlexp) | LPAREN SQL sqlexp RPAREN (sqlexp) | LPAREN FROM tables RPAREN (#2 tables) + | LPAREN SELECT1 query1 RPAREN (query1) | LPAREN INSERT INTO texp LPAREN fields RPAREN VALUES LPAREN sqlexps RPAREN RPAREN (let @@ -1540,6 +1541,7 @@ tables : fitem (fitem) end) fitem : table' ([#1 table'], #2 table') + | LBRACE LBRACE eexp RBRACE RBRACE ([], eexp) | fitem JOIN fitem ON sqlexp (let val loc = s (fitem1left, sqlexpright) diff --git a/src/urweb.lex b/src/urweb.lex index b6916cb9..ed6e310b 100644 --- a/src/urweb.lex +++ b/src/urweb.lex @@ -420,6 +420,7 @@ notags = [^<{\n]+; "LIMIT" => (Tokens.LIMIT (pos yypos, pos yypos + size yytext)); "OFFSET" => (Tokens.OFFSET (pos yypos, pos yypos + size yytext)); "ALL" => (Tokens.ALL (pos yypos, pos yypos + size yytext)); + "SELECT1" => (Tokens.SELECT1 (pos yypos, pos yypos + size yytext)); "JOIN" => (Tokens.JOIN (pos yypos, pos yypos + size yytext)); "INNER" => (Tokens.INNER (pos yypos, pos yypos + size yytext)); -- cgit v1.2.3