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