src/Pure/General/json_api.scala
author wenzelm
Wed, 15 Dec 2021 23:18:41 +0100
changeset 74946 0dd14d8b16da
child 74962 2c9c4ad4c816
permissions -rw-r--r--
support for JSON:API;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
74946
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/json_api.scala
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
     3
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
     4
Support for JSON:API: https://jsonapi.org/format
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
     5
*/
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
     6
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
     7
package isabelle
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
     8
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
     9
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    10
object JSON_API
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    11
{
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    12
  val mime_type = "application/vnd.api+json"
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    13
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    14
  def api_error(msg: String): Nothing = error("JSON API error: " + msg)
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    15
  def api_errors(msgs: List[String]): Nothing = error(("JSON API errors:" :: msgs).mkString("\n  "))
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    16
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    17
  sealed case class Root(json: JSON.T)
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    18
  {
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    19
    def get_links: Option[Links] = JSON.value(json, "links").map(Links)
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    20
    def get_included: List[Resource] = JSON.list(json, "included", Resource.some).getOrElse(Nil)
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    21
    def get_data: Option[Data] = JSON.value(json, "data").map(Data(_, get_included))
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    22
    def get_errors: Option[List[JSON.T]] = JSON.list(json, "errors", Some(_))
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    23
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    24
    def ok: Boolean = get_errors.isEmpty
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    25
    def check: Root =
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    26
      get_errors match {
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    27
        case None => this
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    28
        case Some(List(err)) => api_error(JSON.Format(err))
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    29
        case Some(errs) => api_errors(errs.map(JSON.Format.apply))
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    30
      }
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    31
    def check_data: Data = check.get_data getOrElse api_error("missing data")
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    32
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    33
    override def toString: String = "Root(" + (if (ok) "ok" else "errors") + ")"
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    34
  }
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    35
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    36
  sealed case class Links(json: JSON.T)
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    37
  {
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    38
    def get_next: Option[Root] =
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    39
      for (next <- JSON.value(json, "next") if next != null) yield Root(next)
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    40
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    41
    override def toString: String =
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    42
      if (get_next.isEmpty) "Links()" else "Links(next)"
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    43
  }
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    44
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    45
  sealed case class Data(data: JSON.T, included: List[Resource])
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    46
  {
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    47
    def is_multi: Boolean = JSON.Value.List.unapply(data, Some(_)).nonEmpty
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    48
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    49
    def resource: Resource =
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    50
      if (is_multi) api_error("singleton resource expected")
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    51
      else Resource.some(data).get
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    52
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    53
    def resources: List[Resource] =
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    54
      JSON.Value.List.unapply(data, Resource.some)
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    55
        .getOrElse(api_error("multiple resources expected"))
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    56
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    57
    override def toString: String =
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    58
      if (is_multi) "Data(resources)" else "Data(resource)"
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    59
  }
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    60
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    61
  object Resource
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    62
  {
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    63
    def some(json: JSON.T): Some[Resource] = Some(Resource(json))
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    64
  }
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    65
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    66
  sealed case class Resource(json: JSON.T)
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    67
  {
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    68
    val id: JSON.T = JSON.value(json, "id") getOrElse api_error("missing id")
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    69
    val type_ : JSON.T = JSON.value(json, "type") getOrElse api_error("missing type")
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    70
    val fields: JSON.Object.T =
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    71
      JSON.value(json, "attributes", JSON.Object.unapply).getOrElse(JSON.Object.empty) ++
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    72
      JSON.value(json, "relationships", JSON.Object.unapply).getOrElse(JSON.Object.empty)
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    73
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    74
    override def toString: String = JSON.Format(json)
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    75
  }
0dd14d8b16da support for JSON:API;
wenzelm
parents:
diff changeset
    76
}