63788
|
1 |
/* Title: Pure/General/sql.scala
|
63778
|
2 |
Author: Makarius
|
|
3 |
|
63779
|
4 |
Generic support for SQL.
|
63778
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
|
63779
|
10 |
import java.sql.ResultSet
|
|
11 |
|
|
12 |
|
63778
|
13 |
object SQL
|
|
14 |
{
|
|
15 |
/* concrete syntax */
|
|
16 |
|
|
17 |
def quote_char(c: Char): String =
|
|
18 |
c match {
|
|
19 |
case '\u0000' => "\\0"
|
|
20 |
case '\'' => "\\'"
|
|
21 |
case '\"' => "\\\""
|
|
22 |
case '\b' => "\\b"
|
|
23 |
case '\n' => "\\n"
|
|
24 |
case '\r' => "\\r"
|
|
25 |
case '\t' => "\\t"
|
|
26 |
case '\u001a' => "\\Z"
|
|
27 |
case '\\' => "\\\\"
|
|
28 |
case _ => c.toString
|
|
29 |
}
|
|
30 |
|
|
31 |
def quote_string(s: String): String =
|
|
32 |
quote(s.map(quote_char(_)).mkString)
|
|
33 |
|
63779
|
34 |
def quote_ident(s: String): String =
|
|
35 |
{
|
|
36 |
require(!s.contains('`'))
|
|
37 |
"`" + s + "`"
|
|
38 |
}
|
|
39 |
|
63791
|
40 |
def enclosure(ss: Iterable[String]): String = ss.mkString("(", ", ", ")")
|
|
41 |
|
63779
|
42 |
|
|
43 |
/* columns */
|
|
44 |
|
|
45 |
object Column
|
|
46 |
{
|
63781
|
47 |
def int(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Int] =
|
|
48 |
new Column_Int(name, strict, primary_key)
|
|
49 |
def long(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Long] =
|
|
50 |
new Column_Long(name, strict, primary_key)
|
|
51 |
def double(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Double] =
|
|
52 |
new Column_Double(name, strict, primary_key)
|
|
53 |
def string(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[String] =
|
|
54 |
new Column_String(name, strict, primary_key)
|
|
55 |
def bytes(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Bytes] =
|
|
56 |
new Column_Bytes(name, strict, primary_key)
|
63779
|
57 |
}
|
|
58 |
|
63781
|
59 |
abstract class Column[+A] private[SQL](
|
63790
|
60 |
val name: String, val strict: Boolean, val primary_key: Boolean)
|
|
61 |
extends Function[ResultSet, A]
|
63779
|
62 |
{
|
|
63 |
def sql_name: String = quote_ident(name)
|
|
64 |
def sql_type: String
|
63781
|
65 |
def sql_decl: String =
|
|
66 |
sql_name + " " + sql_type +
|
|
67 |
(if (strict) " NOT NULL" else "") +
|
|
68 |
(if (primary_key) " PRIMARY KEY" else "")
|
|
69 |
|
63780
|
70 |
def string(rs: ResultSet): String =
|
|
71 |
{
|
|
72 |
val s = rs.getString(name)
|
|
73 |
if (s == null) "" else s
|
|
74 |
}
|
|
75 |
def apply(rs: ResultSet): A
|
|
76 |
def get(rs: ResultSet): Option[A] =
|
|
77 |
{
|
|
78 |
val x = apply(rs)
|
|
79 |
if (rs.wasNull) None else Some(x)
|
|
80 |
}
|
63779
|
81 |
|
|
82 |
override def toString: String = sql_decl
|
|
83 |
}
|
|
84 |
|
63781
|
85 |
class Column_Int private[SQL](name: String, strict: Boolean, primary_key: Boolean)
|
|
86 |
extends Column[Int](name, strict, primary_key)
|
63779
|
87 |
{
|
|
88 |
def sql_type: String = "INTEGER"
|
63780
|
89 |
def apply(rs: ResultSet): Int = rs.getInt(name)
|
63779
|
90 |
}
|
|
91 |
|
63781
|
92 |
class Column_Long private[SQL](name: String, strict: Boolean, primary_key: Boolean)
|
|
93 |
extends Column[Long](name, strict, primary_key)
|
63779
|
94 |
{
|
|
95 |
def sql_type: String = "INTEGER"
|
63780
|
96 |
def apply(rs: ResultSet): Long = rs.getLong(name)
|
63779
|
97 |
}
|
|
98 |
|
63781
|
99 |
class Column_Double private[SQL](name: String, strict: Boolean, primary_key: Boolean)
|
|
100 |
extends Column[Double](name, strict, primary_key)
|
63779
|
101 |
{
|
|
102 |
def sql_type: String = "REAL"
|
63780
|
103 |
def apply(rs: ResultSet): Double = rs.getDouble(name)
|
63779
|
104 |
}
|
|
105 |
|
63781
|
106 |
class Column_String private[SQL](name: String, strict: Boolean, primary_key: Boolean)
|
|
107 |
extends Column[String](name, strict, primary_key)
|
63779
|
108 |
{
|
|
109 |
def sql_type: String = "TEXT"
|
63780
|
110 |
def apply(rs: ResultSet): String =
|
|
111 |
{
|
|
112 |
val s = rs.getString(name)
|
|
113 |
if (s == null) "" else s
|
|
114 |
}
|
63779
|
115 |
}
|
|
116 |
|
63781
|
117 |
class Column_Bytes private[SQL](name: String, strict: Boolean, primary_key: Boolean)
|
|
118 |
extends Column[Bytes](name, strict, primary_key)
|
63779
|
119 |
{
|
|
120 |
def sql_type: String = "BLOB"
|
63780
|
121 |
def apply(rs: ResultSet): Bytes =
|
63779
|
122 |
{
|
|
123 |
val bs = rs.getBytes(name)
|
63780
|
124 |
if (bs == null) Bytes.empty else Bytes(bs)
|
63779
|
125 |
}
|
|
126 |
}
|
63780
|
127 |
|
|
128 |
|
|
129 |
/* tables */
|
|
130 |
|
63791
|
131 |
def table(name: String, columns: List[Column[Any]]): Table = new Table(name, columns)
|
63783
|
132 |
|
|
133 |
class Table private[SQL](name: String, columns: List[Column[Any]])
|
63780
|
134 |
{
|
63790
|
135 |
private val columns_index: Map[String, Int] =
|
|
136 |
columns.iterator.map(_.name).zipWithIndex.toMap
|
|
137 |
|
63781
|
138 |
Library.duplicates(columns.map(_.name)) match {
|
|
139 |
case Nil =>
|
|
140 |
case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name))
|
|
141 |
}
|
|
142 |
|
|
143 |
columns.filter(_.primary_key) match {
|
|
144 |
case bad if bad.length > 1 =>
|
|
145 |
error("Multiple primary keys " + commas_quote(bad.map(_.name)) + " for table " + quote(name))
|
|
146 |
case _ =>
|
|
147 |
}
|
|
148 |
|
63780
|
149 |
def sql_create(strict: Boolean, rowid: Boolean): String =
|
63784
|
150 |
"CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
|
63791
|
151 |
quote_ident(name) + " " + enclosure(columns.map(_.sql_decl)) +
|
63780
|
152 |
(if (rowid) "" else " WITHOUT ROWID")
|
|
153 |
|
|
154 |
def sql_drop(strict: Boolean): String =
|
63784
|
155 |
"DROP TABLE " + (if (strict) "" else "IF EXISTS ") + quote_ident(name)
|
63783
|
156 |
|
63791
|
157 |
def sql_create_index(
|
|
158 |
index_name: String, index_columns: List[Column[Any]],
|
|
159 |
strict: Boolean, unique: Boolean): String =
|
|
160 |
"CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " +
|
|
161 |
(if (strict) "" else "IF NOT EXISTS ") + quote_ident(index_name) + " ON " +
|
|
162 |
quote_ident(name) + " " + enclosure(index_columns.map(_.name))
|
|
163 |
|
|
164 |
def sql_drop_index(index_name: String, strict: Boolean): String =
|
|
165 |
"DROP INDEX " + (if (strict) "" else "IF EXISTS ") + quote_ident(index_name)
|
|
166 |
|
63790
|
167 |
def sql_insert: String =
|
63791
|
168 |
"INSERT INTO " + quote_ident(name) + " VALUES " + enclosure(columns.map(_ => "?"))
|
|
169 |
|
|
170 |
def sql_select(select_columns: List[Column[Any]], distinct: Boolean): String =
|
|
171 |
"SELECT " + (if (distinct) "DISTINCT " else "") +
|
|
172 |
commas(select_columns.map(_.sql_name)) + " FROM " + quote_ident(name)
|
63790
|
173 |
|
63783
|
174 |
override def toString: String =
|
63791
|
175 |
"TABLE " + quote_ident(name) + " " + enclosure(columns.map(_.toString))
|
63780
|
176 |
}
|
63790
|
177 |
|
|
178 |
|
|
179 |
/* results */
|
|
180 |
|
|
181 |
def iterator[A](rs: ResultSet)(get: ResultSet => A): Iterator[A] = new Iterator[A]
|
|
182 |
{
|
|
183 |
private var _next: Boolean = rs.next()
|
|
184 |
def hasNext: Boolean = _next
|
|
185 |
def next: A = { val x = get(rs); _next = rs.next(); x }
|
|
186 |
}
|
63778
|
187 |
}
|