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