src/Pure/General/sql.scala
author wenzelm
Mon Sep 05 11:51:25 2016 +0200 (2016-09-05)
changeset 63790 3d723062dc70
parent 63788 3160826b92f8
child 63791 c6cbdfaae19e
permissions -rw-r--r--
more operations;
tuned;
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@63779
    40
wenzelm@63779
    41
  /* columns */
wenzelm@63779
    42
wenzelm@63779
    43
  object Column
wenzelm@63779
    44
  {
wenzelm@63781
    45
    def int(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Int] =
wenzelm@63781
    46
      new Column_Int(name, strict, primary_key)
wenzelm@63781
    47
    def long(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Long] =
wenzelm@63781
    48
      new Column_Long(name, strict, primary_key)
wenzelm@63781
    49
    def double(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Double] =
wenzelm@63781
    50
      new Column_Double(name, strict, primary_key)
wenzelm@63781
    51
    def string(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[String] =
wenzelm@63781
    52
      new Column_String(name, strict, primary_key)
wenzelm@63781
    53
    def bytes(name: String, strict: Boolean = true, primary_key: Boolean = false): Column[Bytes] =
wenzelm@63781
    54
      new Column_Bytes(name, strict, primary_key)
wenzelm@63779
    55
  }
wenzelm@63779
    56
wenzelm@63781
    57
  abstract class Column[+A] private[SQL](
wenzelm@63790
    58
      val name: String, val strict: Boolean, val primary_key: Boolean)
wenzelm@63790
    59
    extends Function[ResultSet, A]
wenzelm@63779
    60
  {
wenzelm@63779
    61
    def sql_name: String = quote_ident(name)
wenzelm@63779
    62
    def sql_type: String
wenzelm@63781
    63
    def sql_decl: String =
wenzelm@63781
    64
      sql_name + " " + sql_type +
wenzelm@63781
    65
      (if (strict) " NOT NULL" else "") +
wenzelm@63781
    66
      (if (primary_key) " PRIMARY KEY" else "")
wenzelm@63781
    67
wenzelm@63780
    68
    def string(rs: ResultSet): String =
wenzelm@63780
    69
    {
wenzelm@63780
    70
      val s = rs.getString(name)
wenzelm@63780
    71
      if (s == null) "" else s
wenzelm@63780
    72
    }
wenzelm@63780
    73
    def apply(rs: ResultSet): A
wenzelm@63780
    74
    def get(rs: ResultSet): Option[A] =
wenzelm@63780
    75
    {
wenzelm@63780
    76
      val x = apply(rs)
wenzelm@63780
    77
      if (rs.wasNull) None else Some(x)
wenzelm@63780
    78
    }
wenzelm@63779
    79
wenzelm@63779
    80
    override def toString: String = sql_decl
wenzelm@63779
    81
  }
wenzelm@63779
    82
wenzelm@63781
    83
  class Column_Int private[SQL](name: String, strict: Boolean, primary_key: Boolean)
wenzelm@63781
    84
    extends Column[Int](name, strict, primary_key)
wenzelm@63779
    85
  {
wenzelm@63779
    86
    def sql_type: String = "INTEGER"
wenzelm@63780
    87
    def apply(rs: ResultSet): Int = rs.getInt(name)
wenzelm@63779
    88
  }
wenzelm@63779
    89
wenzelm@63781
    90
  class Column_Long private[SQL](name: String, strict: Boolean, primary_key: Boolean)
wenzelm@63781
    91
    extends Column[Long](name, strict, primary_key)
wenzelm@63779
    92
  {
wenzelm@63779
    93
    def sql_type: String = "INTEGER"
wenzelm@63780
    94
    def apply(rs: ResultSet): Long = rs.getLong(name)
wenzelm@63779
    95
  }
wenzelm@63779
    96
wenzelm@63781
    97
  class Column_Double private[SQL](name: String, strict: Boolean, primary_key: Boolean)
wenzelm@63781
    98
    extends Column[Double](name, strict, primary_key)
wenzelm@63779
    99
  {
wenzelm@63779
   100
    def sql_type: String = "REAL"
wenzelm@63780
   101
    def apply(rs: ResultSet): Double = rs.getDouble(name)
wenzelm@63779
   102
  }
wenzelm@63779
   103
wenzelm@63781
   104
  class Column_String private[SQL](name: String, strict: Boolean, primary_key: Boolean)
wenzelm@63781
   105
    extends Column[String](name, strict, primary_key)
wenzelm@63779
   106
  {
wenzelm@63779
   107
    def sql_type: String = "TEXT"
wenzelm@63780
   108
    def apply(rs: ResultSet): String =
wenzelm@63780
   109
    {
wenzelm@63780
   110
      val s = rs.getString(name)
wenzelm@63780
   111
      if (s == null) "" else s
wenzelm@63780
   112
    }
wenzelm@63779
   113
  }
wenzelm@63779
   114
wenzelm@63781
   115
  class Column_Bytes private[SQL](name: String, strict: Boolean, primary_key: Boolean)
wenzelm@63781
   116
    extends Column[Bytes](name, strict, primary_key)
wenzelm@63779
   117
  {
wenzelm@63779
   118
    def sql_type: String = "BLOB"
wenzelm@63780
   119
    def apply(rs: ResultSet): Bytes =
wenzelm@63779
   120
    {
wenzelm@63779
   121
      val bs = rs.getBytes(name)
wenzelm@63780
   122
      if (bs == null) Bytes.empty else Bytes(bs)
wenzelm@63779
   123
    }
wenzelm@63779
   124
  }
wenzelm@63780
   125
wenzelm@63780
   126
wenzelm@63780
   127
  /* tables */
wenzelm@63780
   128
wenzelm@63783
   129
  def table(name: String, columns: Column[Any]*): Table = new Table(name, columns.toList)
wenzelm@63783
   130
wenzelm@63783
   131
  class Table private[SQL](name: String, columns: List[Column[Any]])
wenzelm@63780
   132
  {
wenzelm@63790
   133
    private val columns_index: Map[String, Int] =
wenzelm@63790
   134
      columns.iterator.map(_.name).zipWithIndex.toMap
wenzelm@63790
   135
wenzelm@63781
   136
    Library.duplicates(columns.map(_.name)) match {
wenzelm@63781
   137
      case Nil =>
wenzelm@63781
   138
      case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name))
wenzelm@63781
   139
    }
wenzelm@63781
   140
wenzelm@63781
   141
    columns.filter(_.primary_key) match {
wenzelm@63781
   142
      case bad if bad.length > 1 =>
wenzelm@63781
   143
        error("Multiple primary keys " + commas_quote(bad.map(_.name)) + " for table " + quote(name))
wenzelm@63781
   144
      case _ =>
wenzelm@63781
   145
    }
wenzelm@63781
   146
wenzelm@63780
   147
    def sql_create(strict: Boolean, rowid: Boolean): String =
wenzelm@63784
   148
      "CREATE TABLE " + (if (strict) "" else "IF NOT EXISTS ") +
wenzelm@63780
   149
        quote_ident(name) + " " + columns.map(_.sql_decl).mkString("(", ", ", ")") +
wenzelm@63780
   150
        (if (rowid) "" else " WITHOUT ROWID")
wenzelm@63780
   151
wenzelm@63780
   152
    def sql_drop(strict: Boolean): String =
wenzelm@63784
   153
      "DROP TABLE " + (if (strict) "" else "IF EXISTS ") + quote_ident(name)
wenzelm@63783
   154
wenzelm@63790
   155
    def sql_insert: String =
wenzelm@63790
   156
      "INSERT INTO " + quote_ident(name) +
wenzelm@63790
   157
      " VALUES " + columns.map(_ => "?").mkString("(", ", ", ")")
wenzelm@63790
   158
wenzelm@63783
   159
    override def toString: String =
wenzelm@63783
   160
      "TABLE " + quote_ident(name) + " " + columns.map(_.toString).mkString("(", ", ", ")")
wenzelm@63780
   161
  }
wenzelm@63790
   162
wenzelm@63790
   163
wenzelm@63790
   164
  /* results */
wenzelm@63790
   165
wenzelm@63790
   166
  def iterator[A](rs: ResultSet)(get: ResultSet => A): Iterator[A] = new Iterator[A]
wenzelm@63790
   167
  {
wenzelm@63790
   168
    private var _next: Boolean = rs.next()
wenzelm@63790
   169
    def hasNext: Boolean = _next
wenzelm@63790
   170
    def next: A = { val x = get(rs); _next = rs.next(); x }
wenzelm@63790
   171
  }
wenzelm@63778
   172
}