author | wenzelm |
Thu, 16 Mar 2017 23:27:29 +0100 | |
changeset 65280 | ef37f5236794 |
parent 65022 | cda3d36aceb2 |
child 65292 | e3bd1e7ddd23 |
permissions | -rw-r--r-- |
63788 | 1 |
/* Title: Pure/General/sql.scala |
63778 | 2 |
Author: Makarius |
3 |
||
65006 | 4 |
Support for SQL databases: SQLite and PostgreSQL. |
63778 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
65021 | 9 |
import java.time.OffsetDateTime |
10 |
import java.sql.{DriverManager, Connection, PreparedStatement, ResultSet} |
|
63779 | 11 |
|
12 |
||
63778 | 13 |
object SQL |
14 |
{ |
|
65006 | 15 |
/** SQL language **/ |
16 |
||
63778 | 17 |
/* concrete syntax */ |
18 |
||
19 |
def quote_char(c: Char): String = |
|
20 |
c match { |
|
21 |
case '\u0000' => "\\0" |
|
22 |
case '\'' => "\\'" |
|
23 |
case '\"' => "\\\"" |
|
24 |
case '\b' => "\\b" |
|
25 |
case '\n' => "\\n" |
|
26 |
case '\r' => "\\r" |
|
27 |
case '\t' => "\\t" |
|
28 |
case '\u001a' => "\\Z" |
|
29 |
case '\\' => "\\\\" |
|
30 |
case _ => c.toString |
|
31 |
} |
|
32 |
||
33 |
def quote_string(s: String): String = |
|
34 |
quote(s.map(quote_char(_)).mkString) |
|
35 |
||
63779 | 36 |
def quote_ident(s: String): String = |
65003
4b4ccf86755c
more portable: SQL standard syntax instead of MySQL extension;
wenzelm
parents:
63791
diff
changeset
|
37 |
quote(s.replace("\"", "\"\"")) |
63779 | 38 |
|
63791 | 39 |
def enclosure(ss: Iterable[String]): String = ss.mkString("(", ", ", ")") |
40 |
||
63779 | 41 |
|
65008 | 42 |
/* types */ |
43 |
||
44 |
object Type extends Enumeration |
|
45 |
{ |
|
65011 | 46 |
val Boolean = Value("BOOLEAN") |
65008 | 47 |
val Int = Value("INTEGER") |
48 |
val Long = Value("BIGINT") |
|
49 |
val Double = Value("DOUBLE PRECISION") |
|
50 |
val String = Value("TEXT") |
|
51 |
val Bytes = Value("BLOB") |
|
65014 | 52 |
val Date = Value("TIMESTAMP WITH TIME ZONE") |
65008 | 53 |
} |
54 |
||
65019 | 55 |
def sql_type_default(T: Type.Value): String = T.toString |
65013 | 56 |
|
65019 | 57 |
def sql_type_sqlite(T: Type.Value): String = |
58 |
if (T == Type.Boolean) "INTEGER" |
|
59 |
else if (T == Type.Date) "TEXT" |
|
60 |
else sql_type_default(T) |
|
65013 | 61 |
|
65019 | 62 |
def sql_type_postgresql(T: Type.Value): String = |
63 |
if (T == Type.Bytes) "BYTEA" |
|
64 |
else sql_type_default(T) |
|
65008 | 65 |
|
66 |
||
63779 | 67 |
/* columns */ |
68 |
||
69 |
object Column |
|
70 |
{ |
|
65280 | 71 |
def bool(name: String, strict: Boolean = false, primary_key: Boolean = false): Column = |
65018 | 72 |
Column(name, Type.Boolean, strict, primary_key) |
65280 | 73 |
def int(name: String, strict: Boolean = false, primary_key: Boolean = false): Column = |
65018 | 74 |
Column(name, Type.Int, strict, primary_key) |
65280 | 75 |
def long(name: String, strict: Boolean = false, primary_key: Boolean = false): Column = |
65018 | 76 |
Column(name, Type.Long, strict, primary_key) |
65280 | 77 |
def double(name: String, strict: Boolean = false, primary_key: Boolean = false): Column = |
65018 | 78 |
Column(name, Type.Double, strict, primary_key) |
65280 | 79 |
def string(name: String, strict: Boolean = false, primary_key: Boolean = false): Column = |
65018 | 80 |
Column(name, Type.String, strict, primary_key) |
65280 | 81 |
def bytes(name: String, strict: Boolean = false, primary_key: Boolean = false): Column = |
65018 | 82 |
Column(name, Type.Bytes, strict, primary_key) |
65280 | 83 |
def date(name: String, strict: Boolean = false, primary_key: Boolean = false): Column = |
65018 | 84 |
Column(name, Type.Date, strict, primary_key) |
63779 | 85 |
} |
86 |
||
65018 | 87 |
sealed case class Column( |
65280 | 88 |
name: String, T: Type.Value, strict: Boolean = false, primary_key: Boolean = false) |
63779 | 89 |
{ |
90 |
def sql_name: String = quote_ident(name) |
|
65019 | 91 |
def sql_decl(sql_type: Type.Value => String): String = |
92 |
sql_name + " " + sql_type(T) + |
|
63781 | 93 |
(if (strict) " NOT NULL" else "") + |
94 |
(if (primary_key) " PRIMARY KEY" else "") |
|
95 |
||
65019 | 96 |
override def toString: String = sql_decl(sql_type_default) |
63779 | 97 |
} |
98 |
||
63780 | 99 |
|
100 |
/* tables */ |
|
101 |
||
65018 | 102 |
sealed case class Table(name: String, columns: List[Column]) |
63780 | 103 |
{ |
63790 | 104 |
private val columns_index: Map[String, Int] = |
105 |
columns.iterator.map(_.name).zipWithIndex.toMap |
|
106 |
||
63781 | 107 |
Library.duplicates(columns.map(_.name)) match { |
108 |
case Nil => |
|
109 |
case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name)) |
|
110 |
} |
|
111 |
||
112 |
columns.filter(_.primary_key) match { |
|
113 |
case bad if bad.length > 1 => |
|
114 |
error("Multiple primary keys " + commas_quote(bad.map(_.name)) + " for table " + quote(name)) |
|
115 |
case _ => |
|
116 |
} |
|
117 |
||
65019 | 118 |
def sql_create(strict: Boolean, rowid: Boolean, sql_type: Type.Value => String): String = |
63784 | 119 |
"CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") + |
65019 | 120 |
quote_ident(name) + " " + enclosure(columns.map(_.sql_decl(sql_type))) + |
63780 | 121 |
(if (rowid) "" else " WITHOUT ROWID") |
122 |
||
123 |
def sql_drop(strict: Boolean): String = |
|
63784 | 124 |
"DROP TABLE " + (if (strict) "" else "IF EXISTS ") + quote_ident(name) |
63783 | 125 |
|
63791 | 126 |
def sql_create_index( |
65018 | 127 |
index_name: String, index_columns: List[Column], |
63791 | 128 |
strict: Boolean, unique: Boolean): String = |
129 |
"CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " + |
|
130 |
(if (strict) "" else "IF NOT EXISTS ") + quote_ident(index_name) + " ON " + |
|
131 |
quote_ident(name) + " " + enclosure(index_columns.map(_.name)) |
|
132 |
||
133 |
def sql_drop_index(index_name: String, strict: Boolean): String = |
|
134 |
"DROP INDEX " + (if (strict) "" else "IF EXISTS ") + quote_ident(index_name) |
|
135 |
||
63790 | 136 |
def sql_insert: String = |
63791 | 137 |
"INSERT INTO " + quote_ident(name) + " VALUES " + enclosure(columns.map(_ => "?")) |
138 |
||
65018 | 139 |
def sql_select(select_columns: List[Column], distinct: Boolean): String = |
63791 | 140 |
"SELECT " + (if (distinct) "DISTINCT " else "") + |
141 |
commas(select_columns.map(_.sql_name)) + " FROM " + quote_ident(name) |
|
63790 | 142 |
|
63783 | 143 |
override def toString: String = |
63791 | 144 |
"TABLE " + quote_ident(name) + " " + enclosure(columns.map(_.toString)) |
63780 | 145 |
} |
63790 | 146 |
|
147 |
||
65012 | 148 |
|
149 |
/** SQL database operations **/ |
|
150 |
||
63790 | 151 |
/* results */ |
152 |
||
153 |
def iterator[A](rs: ResultSet)(get: ResultSet => A): Iterator[A] = new Iterator[A] |
|
154 |
{ |
|
155 |
private var _next: Boolean = rs.next() |
|
156 |
def hasNext: Boolean = _next |
|
157 |
def next: A = { val x = get(rs); _next = rs.next(); x } |
|
158 |
} |
|
65006 | 159 |
|
160 |
trait Database |
|
161 |
{ |
|
65008 | 162 |
/* types */ |
163 |
||
65019 | 164 |
def sql_type(T: Type.Value): String |
65008 | 165 |
|
166 |
||
65006 | 167 |
/* connection */ |
168 |
||
169 |
def connection: Connection |
|
170 |
||
171 |
def close() { connection.close } |
|
172 |
||
173 |
def transaction[A](body: => A): A = |
|
174 |
{ |
|
175 |
val auto_commit = connection.getAutoCommit |
|
176 |
try { |
|
177 |
connection.setAutoCommit(false) |
|
65022 | 178 |
val savepoint = connection.setSavepoint |
179 |
try { |
|
180 |
val result = body |
|
181 |
connection.commit |
|
182 |
result |
|
183 |
} |
|
184 |
catch { case exn: Throwable => connection.rollback(savepoint); throw exn } |
|
65006 | 185 |
} |
186 |
finally { connection.setAutoCommit(auto_commit) } |
|
187 |
} |
|
188 |
||
189 |
||
190 |
/* statements */ |
|
191 |
||
192 |
def statement(sql: String): PreparedStatement = connection.prepareStatement(sql) |
|
193 |
||
194 |
def insert_statement(table: Table): PreparedStatement = statement(table.sql_insert) |
|
195 |
||
65018 | 196 |
def select_statement(table: Table, columns: List[Column], |
65006 | 197 |
sql: String = "", distinct: Boolean = false): PreparedStatement = |
198 |
statement(table.sql_select(columns, distinct) + (if (sql == "") "" else " " + sql)) |
|
199 |
||
200 |
||
65020 | 201 |
/* input */ |
202 |
||
203 |
def set_bool(stmt: PreparedStatement, i: Int, x: Boolean) { stmt.setBoolean(i, x) } |
|
204 |
def set_int(stmt: PreparedStatement, i: Int, x: Int) { stmt.setInt(i, x) } |
|
205 |
def set_long(stmt: PreparedStatement, i: Int, x: Long) { stmt.setLong(i, x) } |
|
206 |
def set_double(stmt: PreparedStatement, i: Int, x: Double) { stmt.setDouble(i, x) } |
|
207 |
def set_string(stmt: PreparedStatement, i: Int, x: String) { stmt.setString(i, x) } |
|
208 |
def set_bytes(stmt: PreparedStatement, i: Int, bytes: Bytes) |
|
209 |
{ stmt.setBinaryStream(i, bytes.stream(), bytes.length) } |
|
210 |
def set_date(stmt: PreparedStatement, i: Int, date: Date) |
|
211 |
||
65022 | 212 |
|
65020 | 213 |
/* output */ |
65018 | 214 |
|
215 |
def bool(rs: ResultSet, name: String): Boolean = rs.getBoolean(name) |
|
216 |
def int(rs: ResultSet, name: String): Int = rs.getInt(name) |
|
217 |
def long(rs: ResultSet, name: String): Long = rs.getLong(name) |
|
218 |
def double(rs: ResultSet, name: String): Double = rs.getDouble(name) |
|
219 |
def string(rs: ResultSet, name: String): String = |
|
220 |
{ |
|
221 |
val s = rs.getString(name) |
|
222 |
if (s == null) "" else s |
|
223 |
} |
|
224 |
def bytes(rs: ResultSet, name: String): Bytes = |
|
225 |
{ |
|
226 |
val bs = rs.getBytes(name) |
|
227 |
if (bs == null) Bytes.empty else Bytes(bs) |
|
228 |
} |
|
65021 | 229 |
def date(rs: ResultSet, name: String): Date |
65018 | 230 |
|
231 |
def get[A](rs: ResultSet, name: String, f: (ResultSet, String) => A): Option[A] = |
|
232 |
{ |
|
233 |
val x = f(rs, name) |
|
234 |
if (rs.wasNull) None else Some(x) |
|
235 |
} |
|
236 |
||
237 |
||
65006 | 238 |
/* tables */ |
239 |
||
240 |
def tables: List[String] = |
|
241 |
iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList |
|
242 |
||
65280 | 243 |
def create_table(table: Table, strict: Boolean = false, rowid: Boolean = true): Unit = |
65019 | 244 |
using(statement(table.sql_create(strict, rowid, sql_type)))(_.execute()) |
65006 | 245 |
|
65280 | 246 |
def drop_table(table: Table, strict: Boolean = false): Unit = |
65006 | 247 |
using(statement(table.sql_drop(strict)))(_.execute()) |
248 |
||
65018 | 249 |
def create_index(table: Table, name: String, columns: List[Column], |
65280 | 250 |
strict: Boolean = false, unique: Boolean = false): Unit = |
65006 | 251 |
using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute()) |
252 |
||
65280 | 253 |
def drop_index(table: Table, name: String, strict: Boolean = false): Unit = |
65006 | 254 |
using(statement(table.sql_drop_index(name, strict)))(_.execute()) |
255 |
} |
|
63778 | 256 |
} |
65006 | 257 |
|
258 |
||
259 |
||
260 |
/** SQLite **/ |
|
261 |
||
262 |
object SQLite |
|
263 |
{ |
|
65021 | 264 |
// see https://www.sqlite.org/lang_datefunc.html |
265 |
val date_format: Date.Format = Date.Format("uuuu-MM-dd HH:mm:ss.SSS x") |
|
266 |
||
65006 | 267 |
def open_database(path: Path): Database = |
268 |
{ |
|
269 |
val path0 = path.expand |
|
270 |
val s0 = File.platform_path(path0) |
|
271 |
val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0 |
|
272 |
val connection = DriverManager.getConnection("jdbc:sqlite:" + s1) |
|
65007 | 273 |
new Database(path0.toString, connection) |
65006 | 274 |
} |
275 |
||
65007 | 276 |
class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database |
65006 | 277 |
{ |
65007 | 278 |
override def toString: String = name |
65006 | 279 |
|
65019 | 280 |
def sql_type(T: SQL.Type.Value): String = SQL.sql_type_sqlite(T) |
65011 | 281 |
|
65021 | 282 |
def set_date(stmt: PreparedStatement, i: Int, date: Date): Unit = |
283 |
set_string(stmt, i, date_format(date)) |
|
284 |
def date(rs: ResultSet, name: String): Date = |
|
285 |
date_format.parse(string(rs, name)) |
|
286 |
||
65006 | 287 |
def rebuild { using(statement("VACUUM"))(_.execute()) } |
288 |
} |
|
289 |
} |
|
290 |
||
291 |
||
292 |
||
293 |
/** PostgreSQL **/ |
|
294 |
||
295 |
object PostgreSQL |
|
296 |
{ |
|
297 |
val default_port = 5432 |
|
298 |
||
299 |
def open_database( |
|
300 |
user: String, |
|
301 |
password: String, |
|
302 |
database: String = "", |
|
303 |
host: String = "", |
|
65009 | 304 |
port: Int = default_port, |
305 |
ssh: Option[SSH.Session] = None): Database = |
|
65006 | 306 |
{ |
307 |
require(user != "") |
|
65009 | 308 |
|
309 |
val db_host = if (host != "") host else "localhost" |
|
310 |
val db_port = if (port != default_port) ":" + port else "" |
|
311 |
val db_name = "/" + (if (database != "") database else user) |
|
312 |
||
65010 | 313 |
val (url, name, port_forwarding) = |
65009 | 314 |
ssh match { |
65010 | 315 |
case None => |
316 |
val spec = db_host + db_port + db_name |
|
317 |
val url = "jdbc:postgresql://" + spec |
|
318 |
val name = user + "@" + spec |
|
319 |
(url, name, None) |
|
65009 | 320 |
case Some(ssh) => |
321 |
val fw = ssh.port_forwarding(remote_host = db_host, remote_port = port) |
|
65010 | 322 |
val url = "jdbc:postgresql://localhost:" + fw.local_port + db_name |
323 |
val name = user + "@" + fw + db_name + " via ssh " + ssh |
|
324 |
(url, name, Some(fw)) |
|
65009 | 325 |
} |
326 |
try { |
|
65010 | 327 |
val connection = DriverManager.getConnection(url, user, password) |
328 |
new Database(name, connection, port_forwarding) |
|
65009 | 329 |
} |
330 |
catch { case exn: Throwable => port_forwarding.foreach(_.close); throw exn } |
|
65006 | 331 |
} |
332 |
||
65009 | 333 |
class Database private[PostgreSQL]( |
334 |
name: String, val connection: Connection, port_forwarding: Option[SSH.Port_Forwarding]) |
|
335 |
extends SQL.Database |
|
65006 | 336 |
{ |
65010 | 337 |
override def toString: String = name |
65008 | 338 |
|
65019 | 339 |
def sql_type(T: SQL.Type.Value): String = SQL.sql_type_postgresql(T) |
65009 | 340 |
|
65021 | 341 |
// see https://jdbc.postgresql.org/documentation/head/8-date-time.html |
342 |
def set_date(stmt: PreparedStatement, i: Int, date: Date): Unit = |
|
343 |
stmt.setObject(i, OffsetDateTime.from(date.to_utc.rep)) |
|
344 |
def date(rs: ResultSet, name: String): Date = |
|
345 |
Date.instant(rs.getObject(name, classOf[OffsetDateTime]).toInstant) |
|
346 |
||
65009 | 347 |
override def close() { super.close; port_forwarding.foreach(_.close) } |
65006 | 348 |
} |
349 |
} |