src/Pure/Tools/sql.scala
author wenzelm
Sun Sep 04 20:31:23 2016 +0200 (2016-09-04)
changeset 63780 163244cefb4e
parent 63779 9da65bc75610
child 63781 af9fe0b6b78e
permissions -rw-r--r--
more operations;
clarified NULL treatment;
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@63779
    45
    def int(name: String, strict: Boolean = true): Column[Int] = new Column_Int(name, strict)
wenzelm@63779
    46
    def long(name: String, strict: Boolean = true): Column[Long] = new Column_Long(name, strict)
wenzelm@63779
    47
    def double(name: String, strict: Boolean = true): Column[Double] = new Column_Double(name, strict)
wenzelm@63779
    48
    def string(name: String, strict: Boolean = true): Column[String] = new Column_String(name, strict)
wenzelm@63779
    49
    def bytes(name: String, strict: Boolean = true): Column[Bytes] = new Column_Bytes(name, strict)
wenzelm@63779
    50
  }
wenzelm@63779
    51
wenzelm@63780
    52
  abstract class Column[+A] private[SQL](val name: String, val strict: Boolean)
wenzelm@63779
    53
  {
wenzelm@63779
    54
    def sql_name: String = quote_ident(name)
wenzelm@63779
    55
    def sql_type: String
wenzelm@63779
    56
    def sql_decl: String = sql_name + " " + sql_type + (if (strict) " NOT NULL" else "")
wenzelm@63780
    57
    def string(rs: ResultSet): String =
wenzelm@63780
    58
    {
wenzelm@63780
    59
      val s = rs.getString(name)
wenzelm@63780
    60
      if (s == null) "" else s
wenzelm@63780
    61
    }
wenzelm@63780
    62
    def apply(rs: ResultSet): A
wenzelm@63780
    63
    def get(rs: ResultSet): Option[A] =
wenzelm@63780
    64
    {
wenzelm@63780
    65
      val x = apply(rs)
wenzelm@63780
    66
      if (rs.wasNull) None else Some(x)
wenzelm@63780
    67
    }
wenzelm@63779
    68
wenzelm@63779
    69
    override def toString: String = sql_decl
wenzelm@63779
    70
  }
wenzelm@63779
    71
wenzelm@63779
    72
  class Column_Int private[SQL](name: String, strict: Boolean)
wenzelm@63779
    73
    extends Column[Int](name, strict)
wenzelm@63779
    74
  {
wenzelm@63779
    75
    def sql_type: String = "INTEGER"
wenzelm@63780
    76
    def apply(rs: ResultSet): Int = rs.getInt(name)
wenzelm@63779
    77
  }
wenzelm@63779
    78
wenzelm@63779
    79
  class Column_Long private[SQL](name: String, strict: Boolean)
wenzelm@63779
    80
    extends Column[Long](name, strict)
wenzelm@63779
    81
  {
wenzelm@63779
    82
    def sql_type: String = "INTEGER"
wenzelm@63780
    83
    def apply(rs: ResultSet): Long = rs.getLong(name)
wenzelm@63779
    84
  }
wenzelm@63779
    85
wenzelm@63779
    86
  class Column_Double private[SQL](name: String, strict: Boolean)
wenzelm@63779
    87
    extends Column[Double](name, strict)
wenzelm@63779
    88
  {
wenzelm@63779
    89
    def sql_type: String = "REAL"
wenzelm@63780
    90
    def apply(rs: ResultSet): Double = rs.getDouble(name)
wenzelm@63779
    91
  }
wenzelm@63779
    92
wenzelm@63779
    93
  class Column_String private[SQL](name: String, strict: Boolean)
wenzelm@63779
    94
    extends Column[String](name, strict)
wenzelm@63779
    95
  {
wenzelm@63779
    96
    def sql_type: String = "TEXT"
wenzelm@63780
    97
    def apply(rs: ResultSet): String =
wenzelm@63780
    98
    {
wenzelm@63780
    99
      val s = rs.getString(name)
wenzelm@63780
   100
      if (s == null) "" else s
wenzelm@63780
   101
    }
wenzelm@63779
   102
  }
wenzelm@63779
   103
wenzelm@63779
   104
  class Column_Bytes private[SQL](name: String, strict: Boolean)
wenzelm@63779
   105
    extends Column[Bytes](name, strict)
wenzelm@63779
   106
  {
wenzelm@63779
   107
    def sql_type: String = "BLOB"
wenzelm@63780
   108
    def apply(rs: ResultSet): Bytes =
wenzelm@63779
   109
    {
wenzelm@63779
   110
      val bs = rs.getBytes(name)
wenzelm@63780
   111
      if (bs == null) Bytes.empty else Bytes(bs)
wenzelm@63779
   112
    }
wenzelm@63779
   113
  }
wenzelm@63780
   114
wenzelm@63780
   115
wenzelm@63780
   116
  /* tables */
wenzelm@63780
   117
wenzelm@63780
   118
  sealed case class Table(name: String, columns: Column[Any]*)
wenzelm@63780
   119
  {
wenzelm@63780
   120
    def sql_create(strict: Boolean, rowid: Boolean): String =
wenzelm@63780
   121
      "CREATE TABLE " + (if (strict) "" else " IF NOT EXISTS ") +
wenzelm@63780
   122
        quote_ident(name) + " " + columns.map(_.sql_decl).mkString("(", ", ", ")") +
wenzelm@63780
   123
        (if (rowid) "" else " WITHOUT ROWID")
wenzelm@63780
   124
wenzelm@63780
   125
    def sql_drop(strict: Boolean): String =
wenzelm@63780
   126
      "DROP TABLE " + (if (strict) "" else " IF EXISTS ") + quote_ident(name)
wenzelm@63780
   127
  }
wenzelm@63778
   128
}