1 /* Title: Pure/Tools/sql.scala |
|
2 Author: Makarius |
|
3 |
|
4 Generic support for SQL. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 import java.sql.ResultSet |
|
11 |
|
12 |
|
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 |
|
34 def quote_ident(s: String): String = |
|
35 { |
|
36 require(!s.contains('`')) |
|
37 "`" + s + "`" |
|
38 } |
|
39 |
|
40 |
|
41 /* columns */ |
|
42 |
|
43 object Column |
|
44 { |
|
45 def int(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Int] = |
|
46 new Column_Int(name, strict, primary_key) |
|
47 def long(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Long] = |
|
48 new Column_Long(name, strict, primary_key) |
|
49 def double(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Double] = |
|
50 new Column_Double(name, strict, primary_key) |
|
51 def string(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[String] = |
|
52 new Column_String(name, strict, primary_key) |
|
53 def bytes(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Bytes] = |
|
54 new Column_Bytes(name, strict, primary_key) |
|
55 } |
|
56 |
|
57 abstract class Column[+A] private[SQL]( |
|
58 val name: String, val strict: Boolean, val primary_key: Boolean) |
|
59 { |
|
60 def sql_name: String = quote_ident(name) |
|
61 def sql_type: String |
|
62 def sql_decl: String = |
|
63 sql_name + " " + sql_type + |
|
64 (if (strict) " NOT NULL" else "") + |
|
65 (if (primary_key) " PRIMARY KEY" else "") |
|
66 |
|
67 def string(rs: ResultSet): String = |
|
68 { |
|
69 val s = rs.getString(name) |
|
70 if (s == null) "" else s |
|
71 } |
|
72 def apply(rs: ResultSet): A |
|
73 def get(rs: ResultSet): Option[A] = |
|
74 { |
|
75 val x = apply(rs) |
|
76 if (rs.wasNull) None else Some(x) |
|
77 } |
|
78 |
|
79 override def toString: String = sql_decl |
|
80 } |
|
81 |
|
82 class Column_Int private[SQL](name: String, strict: Boolean, primary_key: Boolean) |
|
83 extends Column[Int](name, strict, primary_key) |
|
84 { |
|
85 def sql_type: String = "INTEGER" |
|
86 def apply(rs: ResultSet): Int = rs.getInt(name) |
|
87 } |
|
88 |
|
89 class Column_Long private[SQL](name: String, strict: Boolean, primary_key: Boolean) |
|
90 extends Column[Long](name, strict, primary_key) |
|
91 { |
|
92 def sql_type: String = "INTEGER" |
|
93 def apply(rs: ResultSet): Long = rs.getLong(name) |
|
94 } |
|
95 |
|
96 class Column_Double private[SQL](name: String, strict: Boolean, primary_key: Boolean) |
|
97 extends Column[Double](name, strict, primary_key) |
|
98 { |
|
99 def sql_type: String = "REAL" |
|
100 def apply(rs: ResultSet): Double = rs.getDouble(name) |
|
101 } |
|
102 |
|
103 class Column_String private[SQL](name: String, strict: Boolean, primary_key: Boolean) |
|
104 extends Column[String](name, strict, primary_key) |
|
105 { |
|
106 def sql_type: String = "TEXT" |
|
107 def apply(rs: ResultSet): String = |
|
108 { |
|
109 val s = rs.getString(name) |
|
110 if (s == null) "" else s |
|
111 } |
|
112 } |
|
113 |
|
114 class Column_Bytes private[SQL](name: String, strict: Boolean, primary_key: Boolean) |
|
115 extends Column[Bytes](name, strict, primary_key) |
|
116 { |
|
117 def sql_type: String = "BLOB" |
|
118 def apply(rs: ResultSet): Bytes = |
|
119 { |
|
120 val bs = rs.getBytes(name) |
|
121 if (bs == null) Bytes.empty else Bytes(bs) |
|
122 } |
|
123 } |
|
124 |
|
125 |
|
126 /* tables */ |
|
127 |
|
128 def table(name: String, columns: Column[Any]*): Table = new Table(name, columns.toList) |
|
129 |
|
130 class Table private[SQL](name: String, columns: List[Column[Any]]) |
|
131 { |
|
132 Library.duplicates(columns.map(_.name)) match { |
|
133 case Nil => |
|
134 case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name)) |
|
135 } |
|
136 |
|
137 columns.filter(_.primary_key) match { |
|
138 case bad if bad.length > 1 => |
|
139 error("Multiple primary keys " + commas_quote(bad.map(_.name)) + " for table " + quote(name)) |
|
140 case _ => |
|
141 } |
|
142 |
|
143 def sql_create(strict: Boolean, rowid: Boolean): String = |
|
144 "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") + |
|
145 quote_ident(name) + " " + columns.map(_.sql_decl).mkString("(", ", ", ")") + |
|
146 (if (rowid) "" else " WITHOUT ROWID") |
|
147 |
|
148 def sql_drop(strict: Boolean): String = |
|
149 "DROP TABLE " + (if (strict) "" else "IF EXISTS ") + quote_ident(name) |
|
150 |
|
151 override def toString: String = |
|
152 "TABLE " + quote_ident(name) + " " + columns.map(_.toString).mkString("(", ", ", ")") |
|
153 } |
|
154 } |
|