src/Pure/Tools/sql.scala
author wenzelm
Sun Sep 04 21:09:18 2016 +0200 (2016-09-04)
changeset 63781 af9fe0b6b78e
parent 63780 163244cefb4e
child 63783 baa20f3b6cea
permissions -rw-r--r--
support for (single) primary key;
more operations;
wenzelm@63778
     1
/*  Title:      Pure/Tools/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@63781
    58
    val name: String, val strict: Boolean, val primary_key: Boolean)
wenzelm@63779
    59
  {
wenzelm@63779
    60
    def sql_name: String = quote_ident(name)
wenzelm@63779
    61
    def sql_type: String
wenzelm@63781
    62
    def sql_decl: String =
wenzelm@63781
    63
      sql_name + " " + sql_type +
wenzelm@63781
    64
      (if (strict) " NOT NULL" else "") +
wenzelm@63781
    65
      (if (primary_key) " PRIMARY KEY" else "")
wenzelm@63781
    66
wenzelm@63780
    67
    def string(rs: ResultSet): String =
wenzelm@63780
    68
    {
wenzelm@63780
    69
      val s = rs.getString(name)
wenzelm@63780
    70
      if (s == null) "" else s
wenzelm@63780
    71
    }
wenzelm@63780
    72
    def apply(rs: ResultSet): A
wenzelm@63780
    73
    def get(rs: ResultSet): Option[A] =
wenzelm@63780
    74
    {
wenzelm@63780
    75
      val x = apply(rs)
wenzelm@63780
    76
      if (rs.wasNull) None else Some(x)
wenzelm@63780
    77
    }
wenzelm@63779
    78
wenzelm@63779
    79
    override def toString: String = sql_decl
wenzelm@63779
    80
  }
wenzelm@63779
    81
wenzelm@63781
    82
  class Column_Int private[SQL](name: String, strict: Boolean, primary_key: Boolean)
wenzelm@63781
    83
    extends Column[Int](name, strict, primary_key)
wenzelm@63779
    84
  {
wenzelm@63779
    85
    def sql_type: String = "INTEGER"
wenzelm@63780
    86
    def apply(rs: ResultSet): Int = rs.getInt(name)
wenzelm@63779
    87
  }
wenzelm@63779
    88
wenzelm@63781
    89
  class Column_Long private[SQL](name: String, strict: Boolean, primary_key: Boolean)
wenzelm@63781
    90
    extends Column[Long](name, strict, primary_key)
wenzelm@63779
    91
  {
wenzelm@63779
    92
    def sql_type: String = "INTEGER"
wenzelm@63780
    93
    def apply(rs: ResultSet): Long = rs.getLong(name)
wenzelm@63779
    94
  }
wenzelm@63779
    95
wenzelm@63781
    96
  class Column_Double private[SQL](name: String, strict: Boolean, primary_key: Boolean)
wenzelm@63781
    97
    extends Column[Double](name, strict, primary_key)
wenzelm@63779
    98
  {
wenzelm@63779
    99
    def sql_type: String = "REAL"
wenzelm@63780
   100
    def apply(rs: ResultSet): Double = rs.getDouble(name)
wenzelm@63779
   101
  }
wenzelm@63779
   102
wenzelm@63781
   103
  class Column_String private[SQL](name: String, strict: Boolean, primary_key: Boolean)
wenzelm@63781
   104
    extends Column[String](name, strict, primary_key)
wenzelm@63779
   105
  {
wenzelm@63779
   106
    def sql_type: String = "TEXT"
wenzelm@63780
   107
    def apply(rs: ResultSet): String =
wenzelm@63780
   108
    {
wenzelm@63780
   109
      val s = rs.getString(name)
wenzelm@63780
   110
      if (s == null) "" else s
wenzelm@63780
   111
    }
wenzelm@63779
   112
  }
wenzelm@63779
   113
wenzelm@63781
   114
  class Column_Bytes private[SQL](name: String, strict: Boolean, primary_key: Boolean)
wenzelm@63781
   115
    extends Column[Bytes](name, strict, primary_key)
wenzelm@63779
   116
  {
wenzelm@63779
   117
    def sql_type: String = "BLOB"
wenzelm@63780
   118
    def apply(rs: ResultSet): Bytes =
wenzelm@63779
   119
    {
wenzelm@63779
   120
      val bs = rs.getBytes(name)
wenzelm@63780
   121
      if (bs == null) Bytes.empty else Bytes(bs)
wenzelm@63779
   122
    }
wenzelm@63779
   123
  }
wenzelm@63780
   124
wenzelm@63780
   125
wenzelm@63780
   126
  /* tables */
wenzelm@63780
   127
wenzelm@63781
   128
  sealed case class Table(name: String, columns: List[Column[Any]])
wenzelm@63780
   129
  {
wenzelm@63781
   130
    Library.duplicates(columns.map(_.name)) match {
wenzelm@63781
   131
      case Nil =>
wenzelm@63781
   132
      case bad => error("Duplicate column names " + commas_quote(bad) + " for table " + quote(name))
wenzelm@63781
   133
    }
wenzelm@63781
   134
wenzelm@63781
   135
    columns.filter(_.primary_key) match {
wenzelm@63781
   136
      case bad if bad.length > 1 =>
wenzelm@63781
   137
        error("Multiple primary keys " + commas_quote(bad.map(_.name)) + " for table " + quote(name))
wenzelm@63781
   138
      case _ =>
wenzelm@63781
   139
    }
wenzelm@63781
   140
wenzelm@63780
   141
    def sql_create(strict: Boolean, rowid: Boolean): String =
wenzelm@63780
   142
      "CREATE TABLE " + (if (strict) "" else " IF NOT EXISTS ") +
wenzelm@63780
   143
        quote_ident(name) + " " + columns.map(_.sql_decl).mkString("(", ", ", ")") +
wenzelm@63780
   144
        (if (rowid) "" else " WITHOUT ROWID")
wenzelm@63780
   145
wenzelm@63780
   146
    def sql_drop(strict: Boolean): String =
wenzelm@63780
   147
      "DROP TABLE " + (if (strict) "" else " IF EXISTS ") + quote_ident(name)
wenzelm@63780
   148
  }
wenzelm@63778
   149
}