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