Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/Pure/General/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 3 kB image not shown  

Quellcode-Bibliothek json_api.scala   Sprache: Scala

 
/*  Title:      Pure/General/json_api.scala
    Author:     Makarius

Support for JSON:API: https://jsonapi.org/format
*/


package isabelle


object JSON_API {
  val mime_type = "application/vnd.api+json"

  def api_error(msg: String): Nothing = error("JSON API error: " + msg)
  def api_errors(msgs: List[String]): Nothing = error(("JSON API errors:" :: msgs).mkString("\n "))

  class Service(val url: Url) {
    override def toString: String = url.toString

    def get(route: String): HTTP.Content =
      HTTP.Client.get(url.resolve(route))

    def get_root(route: String = ""): Root =
      Root(get(if_proper(route, "/" + route)).json)
  }

  sealed case class Root(json: JSON.T) {
    def get_links: Option[Links] = JSON.value(json, "links").map(Links.apply)
    def get_next: Option[Service] = get_links.flatMap(_.get_next)

    def get_included: List[Resource] = JSON.list(json, "included", Resource.some).getOrElse(Nil)
    def get_data: Option[Data] = JSON.value(json, "data").map(Data(_, get_included))

    def get_errors: Option[List[JSON.T]] = JSON.list(json, "errors", Some(_))

    def ok: Boolean = get_errors.isEmpty
    def check: Root =
      get_errors match {
        case None => this
        case Some(List(err)) => api_error(JSON.Format(err))
        case Some(errs) => api_errors(errs.map(JSON.Format.apply))
      }
    def check_data: Data = check.get_data getOrElse api_error("missing data")
    def check_resource: Resource = check_data.resource
    def check_resources: List[Resource] = check_data.resources

    def iterator: Iterator[Root] = {
      val init = Some(this)
      new Iterator[Root] {
        private var state: Option[Root] = init
        def hasNext: Boolean = state.nonEmpty
        def next(): Root =
          state match {
            case None => Iterator.empty.next()
            case Some(res) =>
              state = res.get_next.map(_.get_root())
              res
          }
      }
    }
    def iterator_data: Iterator[Data] = iterator.map(_.check_data)
    def iterator_resource: Iterator[Resource] = iterator.map(_.check_resource)
    def iterator_resources: Iterator[Resource] = iterator.flatMap(_.check_resources)

    override def toString: String = "Root(" + (if (ok) "ok" else "errors") + ")"
  }

  sealed case class Links(json: JSON.T) {
    def get_next: Option[Service] =
      for {
        case JSON.Value.String(next) <- JSON.value(json, "next")
        if Url.is_wellformed(next)
      } yield new Service(Url(next))

    override def toString: String =
      if (get_next.isEmpty) "Links()" else "Links(next)"
  }

  sealed case class Data(data: JSON.T, included: List[Resource]) {
    def is_multi: Boolean = JSON.Value.List.unapply(data, Some(_)).nonEmpty

    def resource: Resource =
      if (is_multi) api_error("singleton resource expected")
      else Resource.some(data).get

    def resources: List[Resource] =
      JSON.Value.List.unapply(data, Resource.some)
        .getOrElse(api_error("multiple resources expected"))

    override def toString: String =
      if (is_multi) "Data(resources)" else "Data(resource)"
  }

  object Resource {
    def some(json: JSON.T): Some[Resource] = Some(Resource(json))
  }

  sealed case class Resource(json: JSON.T) {
    val id: JSON.T = JSON.value(json, "id") getOrElse api_error("missing id")
    val type_ : JSON.T = JSON.value(json, "type") getOrElse api_error("missing type")
    val fields: JSON.Object.T =
      JSON.value(json, "attributes", JSON.Object.unapply).getOrElse(JSON.Object.empty) ++
      JSON.value(json, "relationships", JSON.Object.unapply).getOrElse(JSON.Object.empty)

    override def toString: String = JSON.Format(json)
  }
}

100%


¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.22Bemerkung:  (vorverarbeitet)  ¤

*Bot Zugriff






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.