author | wenzelm |
Thu, 09 Feb 2017 16:58:27 +0100 | |
changeset 65012 | 14641ca387f8 |
parent 65011 | 42bffd1637f0 |
child 65013 | 86308845aa43 |
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 |
||
9 |
||
65006 | 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") |
|
52 |
} |
|
53 |
||
54 |
type Type_Name = Type.Value => String |
|
55 |
def default_type_name(t: Type.Value): String = t.toString |
|
56 |
||
57 |
||
63779 | 58 |
/* columns */ |
59 |
||
60 |
object Column |
|
61 |
{ |
|
65011 | 62 |
def bool(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Boolean] = |
63 |
new Column_Boolean(name, strict, primary_key) |
|
63781 | 64 |
def int(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Int] = |
65 |
new Column_Int(name, strict, primary_key) |
|
66 |
def long(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Long] = |
|
67 |
new Column_Long(name, strict, primary_key) |
|
68 |
def double(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Double] = |
|
69 |
new Column_Double(name, strict, primary_key) |
|
70 |
def string(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[String] = |
|
71 |
new Column_String(name, strict, primary_key) |
|
72 |
def bytes(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Bytes] = |
|
65008 | 73 |
new Column_Bytes(name, strict, primary_key) |
63779 | 74 |
} |
75 |
||
63781 | 76 |
abstract class Column[+A] private[SQL]( |
65008 | 77 |
val name: String, |
78 |
val strict: Boolean, |
|
79 |
val primary_key: Boolean, |
|
80 |
val sql_type: Type.Value) extends Function[ResultSet, A] |
|
63779 | 81 |
{ |
82 |
def sql_name: String = quote_ident(name) |
|
65008 | 83 |
def sql_decl(type_name: Type_Name): String = |
84 |
sql_name + " " + type_name(sql_type) + |
|
63781 | 85 |
(if (strict) " NOT NULL" else "") + |
86 |
(if (primary_key) " PRIMARY KEY" else "") |
|
87 |
||
63780 | 88 |
def string(rs: ResultSet): String = |
89 |
{ |
|
90 |
val s = rs.getString(name) |
|
91 |
if (s == null) "" else s |
|
92 |
} |
|
93 |
def apply(rs: ResultSet): A |
|
94 |
def get(rs: ResultSet): Option[A] = |
|
95 |
{ |
|
96 |
val x = apply(rs) |
|
97 |
if (rs.wasNull) None else Some(x) |
|
98 |
} |
|
63779 | 99 |
|
65008 | 100 |
override def toString: String = sql_decl(default_type_name) |
63779 | 101 |
} |
102 |
||
65011 | 103 |
class Column_Boolean private[SQL](name: String, strict: Boolean, primary_key: Boolean) |
104 |
extends Column[Boolean](name, strict, primary_key, Type.Boolean) |
|
105 |
{ |
|
106 |
def apply(rs: ResultSet): Boolean = rs.getBoolean(name) |
|
107 |
} |
|
108 |
||
63781 | 109 |
class Column_Int private[SQL](name: String, strict: Boolean, primary_key: Boolean) |
65008 | 110 |
extends Column[Int](name, strict, primary_key, Type.Int) |
63779 | 111 |
{ |
63780 | 112 |
def apply(rs: ResultSet): Int = rs.getInt(name) |
63779 | 113 |
} |
114 |
||
63781 | 115 |
class Column_Long private[SQL](name: String, strict: Boolean, primary_key: Boolean) |
65008 | 116 |
extends Column[Long](name, strict, primary_key, Type.Long) |
63779 | 117 |
{ |
63780 | 118 |
def apply(rs: ResultSet): Long = rs.getLong(name) |
63779 | 119 |
} |
120 |
||
63781 | 121 |
class Column_Double private[SQL](name: String, strict: Boolean, primary_key: Boolean) |
65008 | 122 |
extends Column[Double](name, strict, primary_key, Type.Double) |
63779 | 123 |
{ |
63780 | 124 |
def apply(rs: ResultSet): Double = rs.getDouble(name) |
63779 | 125 |
} |
126 |
||
63781 | 127 |
class Column_String private[SQL](name: String, strict: Boolean, primary_key: Boolean) |
65008 | 128 |
extends Column[String](name, strict, primary_key, Type.String) |
63779 | 129 |
{ |
63780 | 130 |
def apply(rs: ResultSet): String = |
131 |
{ |
|
132 |
val s = rs.getString(name) |
|
133 |
if (s == null) "" else s |
|
134 |
} |
|
63779 | 135 |
} |
136 |
||
65008 | 137 |
class Column_Bytes private[SQL](name: String, strict: Boolean, primary_key: Boolean) |
138 |
extends Column[Bytes](name, strict, primary_key, Type.Bytes) |
|
63779 | 139 |
{ |
63780 | 140 |
def apply(rs: ResultSet): Bytes = |
63779 | 141 |
{ |
142 |
val bs = rs.getBytes(name) |
|
63780 | 143 |
if (bs == null) Bytes.empty else Bytes(bs) |
63779 | 144 |
} |
145 |
} |
|
63780 | 146 |
|
147 |
||
148 |
/* tables */ |
|
149 |
||
63791 | 150 |
def table(name: String, columns: List[Column[Any]]): Table = new Table(name, columns) |
63783 | 151 |
|
152 |
class Table private[SQL](name: String, columns: List[Column[Any]]) |
|
63780 | 153 |
{ |
63790 | 154 |
private val columns_index: Map[String, Int] = |
155 |
columns.iterator.map(_.name).zipWithIndex.toMap |
|
156 |
||
63781 | 157 |
Library.duplicates(columns.map(_.name)) match { |
158 |
case Nil => |
|
159 |
case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name)) |
|
160 |
} |
|
161 |
||
162 |
columns.filter(_.primary_key) match { |
|
163 |
case bad if bad.length > 1 => |
|
164 |
error("Multiple primary keys " + commas_quote(bad.map(_.name)) + " for table " + quote(name)) |
|
165 |
case _ => |
|
166 |
} |
|
167 |
||
65008 | 168 |
def sql_create(strict: Boolean, rowid: Boolean, type_name: Type_Name): String = |
63784 | 169 |
"CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") + |
65008 | 170 |
quote_ident(name) + " " + enclosure(columns.map(_.sql_decl(type_name))) + |
63780 | 171 |
(if (rowid) "" else " WITHOUT ROWID") |
172 |
||
173 |
def sql_drop(strict: Boolean): String = |
|
63784 | 174 |
"DROP TABLE " + (if (strict) "" else "IF EXISTS ") + quote_ident(name) |
63783 | 175 |
|
63791 | 176 |
def sql_create_index( |
177 |
index_name: String, index_columns: List[Column[Any]], |
|
178 |
strict: Boolean, unique: Boolean): String = |
|
179 |
"CREATE " + (if (unique) "UNIQUE " else "") + "INDEX " + |
|
180 |
(if (strict) "" else "IF NOT EXISTS ") + quote_ident(index_name) + " ON " + |
|
181 |
quote_ident(name) + " " + enclosure(index_columns.map(_.name)) |
|
182 |
||
183 |
def sql_drop_index(index_name: String, strict: Boolean): String = |
|
184 |
"DROP INDEX " + (if (strict) "" else "IF EXISTS ") + quote_ident(index_name) |
|
185 |
||
63790 | 186 |
def sql_insert: String = |
63791 | 187 |
"INSERT INTO " + quote_ident(name) + " VALUES " + enclosure(columns.map(_ => "?")) |
188 |
||
189 |
def sql_select(select_columns: List[Column[Any]], distinct: Boolean): String = |
|
190 |
"SELECT " + (if (distinct) "DISTINCT " else "") + |
|
191 |
commas(select_columns.map(_.sql_name)) + " FROM " + quote_ident(name) |
|
63790 | 192 |
|
63783 | 193 |
override def toString: String = |
63791 | 194 |
"TABLE " + quote_ident(name) + " " + enclosure(columns.map(_.toString)) |
63780 | 195 |
} |
63790 | 196 |
|
197 |
||
65012 | 198 |
|
199 |
/** SQL database operations **/ |
|
200 |
||
63790 | 201 |
/* results */ |
202 |
||
203 |
def iterator[A](rs: ResultSet)(get: ResultSet => A): Iterator[A] = new Iterator[A] |
|
204 |
{ |
|
205 |
private var _next: Boolean = rs.next() |
|
206 |
def hasNext: Boolean = _next |
|
207 |
def next: A = { val x = get(rs); _next = rs.next(); x } |
|
208 |
} |
|
65006 | 209 |
|
210 |
trait Database |
|
211 |
{ |
|
65008 | 212 |
/* types */ |
213 |
||
65011 | 214 |
def type_name(t: Type.Value): String |
65008 | 215 |
|
216 |
||
65006 | 217 |
/* connection */ |
218 |
||
219 |
def connection: Connection |
|
220 |
||
221 |
def close() { connection.close } |
|
222 |
||
223 |
def transaction[A](body: => A): A = |
|
224 |
{ |
|
225 |
val auto_commit = connection.getAutoCommit |
|
226 |
val savepoint = connection.setSavepoint |
|
227 |
||
228 |
try { |
|
229 |
connection.setAutoCommit(false) |
|
230 |
val result = body |
|
231 |
connection.commit |
|
232 |
result |
|
233 |
} |
|
234 |
catch { case exn: Throwable => connection.rollback(savepoint); throw exn } |
|
235 |
finally { connection.setAutoCommit(auto_commit) } |
|
236 |
} |
|
237 |
||
238 |
||
239 |
/* statements */ |
|
240 |
||
241 |
def statement(sql: String): PreparedStatement = connection.prepareStatement(sql) |
|
242 |
||
243 |
def insert_statement(table: Table): PreparedStatement = statement(table.sql_insert) |
|
244 |
||
245 |
def select_statement(table: Table, columns: List[Column[Any]], |
|
246 |
sql: String = "", distinct: Boolean = false): PreparedStatement = |
|
247 |
statement(table.sql_select(columns, distinct) + (if (sql == "") "" else " " + sql)) |
|
248 |
||
249 |
||
250 |
/* tables */ |
|
251 |
||
252 |
def tables: List[String] = |
|
253 |
iterator(connection.getMetaData.getTables(null, null, "%", null))(_.getString(3)).toList |
|
254 |
||
255 |
def create_table(table: Table, strict: Boolean = true, rowid: Boolean = true): Unit = |
|
65008 | 256 |
using(statement(table.sql_create(strict, rowid, type_name)))(_.execute()) |
65006 | 257 |
|
258 |
def drop_table(table: Table, strict: Boolean = true): Unit = |
|
259 |
using(statement(table.sql_drop(strict)))(_.execute()) |
|
260 |
||
261 |
def create_index(table: Table, name: String, columns: List[Column[Any]], |
|
262 |
strict: Boolean = true, unique: Boolean = false): Unit = |
|
263 |
using(statement(table.sql_create_index(name, columns, strict, unique)))(_.execute()) |
|
264 |
||
265 |
def drop_index(table: Table, name: String, strict: Boolean = true): Unit = |
|
266 |
using(statement(table.sql_drop_index(name, strict)))(_.execute()) |
|
267 |
} |
|
63778 | 268 |
} |
65006 | 269 |
|
270 |
||
271 |
||
272 |
/** SQLite **/ |
|
273 |
||
274 |
object SQLite |
|
275 |
{ |
|
276 |
def open_database(path: Path): Database = |
|
277 |
{ |
|
278 |
val path0 = path.expand |
|
279 |
val s0 = File.platform_path(path0) |
|
280 |
val s1 = if (Platform.is_windows) s0.replace('\\', '/') else s0 |
|
281 |
val connection = DriverManager.getConnection("jdbc:sqlite:" + s1) |
|
65007 | 282 |
new Database(path0.toString, connection) |
65006 | 283 |
} |
284 |
||
65007 | 285 |
class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database |
65006 | 286 |
{ |
65007 | 287 |
override def toString: String = name |
65006 | 288 |
|
65011 | 289 |
def type_name(t: SQL.Type.Value): String = |
290 |
if (t == SQL.Type.Boolean) "INTEGER" |
|
291 |
else SQL.default_type_name(t) |
|
292 |
||
65006 | 293 |
def rebuild { using(statement("VACUUM"))(_.execute()) } |
294 |
} |
|
295 |
} |
|
296 |
||
297 |
||
298 |
||
299 |
/** PostgreSQL **/ |
|
300 |
||
301 |
object PostgreSQL |
|
302 |
{ |
|
303 |
val default_port = 5432 |
|
304 |
||
305 |
def open_database( |
|
306 |
user: String, |
|
307 |
password: String, |
|
308 |
database: String = "", |
|
309 |
host: String = "", |
|
65009 | 310 |
port: Int = default_port, |
311 |
ssh: Option[SSH.Session] = None): Database = |
|
65006 | 312 |
{ |
313 |
require(user != "") |
|
65009 | 314 |
|
315 |
val db_host = if (host != "") host else "localhost" |
|
316 |
val db_port = if (port != default_port) ":" + port else "" |
|
317 |
val db_name = "/" + (if (database != "") database else user) |
|
318 |
||
65010 | 319 |
val (url, name, port_forwarding) = |
65009 | 320 |
ssh match { |
65010 | 321 |
case None => |
322 |
val spec = db_host + db_port + db_name |
|
323 |
val url = "jdbc:postgresql://" + spec |
|
324 |
val name = user + "@" + spec |
|
325 |
(url, name, None) |
|
65009 | 326 |
case Some(ssh) => |
327 |
val fw = ssh.port_forwarding(remote_host = db_host, remote_port = port) |
|
65010 | 328 |
val url = "jdbc:postgresql://localhost:" + fw.local_port + db_name |
329 |
val name = user + "@" + fw + db_name + " via ssh " + ssh |
|
330 |
(url, name, Some(fw)) |
|
65009 | 331 |
} |
332 |
try { |
|
65010 | 333 |
val connection = DriverManager.getConnection(url, user, password) |
334 |
new Database(name, connection, port_forwarding) |
|
65009 | 335 |
} |
336 |
catch { case exn: Throwable => port_forwarding.foreach(_.close); throw exn } |
|
65006 | 337 |
} |
338 |
||
65009 | 339 |
class Database private[PostgreSQL]( |
340 |
name: String, val connection: Connection, port_forwarding: Option[SSH.Port_Forwarding]) |
|
341 |
extends SQL.Database |
|
65006 | 342 |
{ |
65010 | 343 |
override def toString: String = name |
65008 | 344 |
|
65011 | 345 |
def type_name(t: SQL.Type.Value): String = |
65008 | 346 |
if (t == SQL.Type.Bytes) "BYTEA" |
347 |
else SQL.default_type_name(t) |
|
65009 | 348 |
|
349 |
override def close() { super.close; port_forwarding.foreach(_.close) } |
|
65006 | 350 |
} |
351 |
} |