mathlib documentation

data.json

Json serialization typeclass #

This file provides helpers for serializing primitive types to json.

@[derive non_null_json_serializable] will make any structure json serializable; for instance,

@[derive non_null_json_serializable]
structure my_struct :=
(success : bool)
(verbose : ℕ := 0)
(extras : option string := none)

can parse {"success": true} as my_struct.mk true 0 none, and reserializing give {"success": true, "verbose": 0, "extras": null}.

Main definitions #

source
@[protected, instance]
meta def exceptional.has_orelse  :
has_orelse exceptional
source
@[class]
meta structure json_serializable (α : Type) :
Type

A class to indicate that a type is json serializable

Instances of this typeclass
source
@[class]
meta structure non_null_json_serializable (α : Type) :
Type

A class for types which never serialize to null

Instances of this typeclass
source
meta def json.typename  :
json → string

Describe the type of a json value

Primitive types #

source
@[protected, instance]
meta def string.non_null_json_serializable  :
non_null_json_serializable string
source
@[protected, instance]
meta def int.non_null_json_serializable  :
non_null_json_serializable ℤ
source
@[protected, instance]
meta def native.float.non_null_json_serializable  :
non_null_json_serializable native.float
source
@[protected, instance]
meta def bool.non_null_json_serializable  :
non_null_json_serializable bool
source
@[protected, instance]
meta def punit.json_serializable  :
json_serializable punit
source
@[protected, instance]
meta def list.non_null_json_serializable {α : Type} [json_serializable α] :
non_null_json_serializable (list α)
source
@[protected, instance]
meta def rbmap.non_null_json_serializable {α : Type} [json_serializable α] :
non_null_json_serializable (rbmap string α has_lt.lt)

Basic coercions #

source
@[protected, instance]
meta def nat.non_null_json_serializable  :
non_null_json_serializable ℕ
source
@[protected, instance]
meta def fin.non_null_json_serializable {n : ℕ} :
non_null_json_serializable (fin n)
source
@[protected, instance]
meta def subtype.json_serializable {α : Type} [json_serializable α] (p : α → Prop) [decidable_pred p] :
json_serializable (subtype p)
source
@[protected, instance]
meta def subtype.non_null_json_serializable {α : Type} [non_null_json_serializable α] (p : α → Prop) [decidable_pred p] :
non_null_json_serializable (subtype p)
source
@[protected, instance]
meta def option.json_serializable {α : Type} [non_null_json_serializable α] :
json_serializable (option α)

Note this only makes sense on types which do not themselves serialize to null

source
meta def list.to_expr {elab : bool} (t : expr elab) (l : level) :
list (expr elab) → expr elab

Flatten a list of (p)exprs into a (p)expr forming a list of type list t.

source
meta def json_serializable.field_starter (j : json) :
exceptional (list (string × json))

Begin parsing fields

source
meta def json_serializable.field_get (l : list (string × json)) (s : string) :
exceptional (option json × list (string × json))

Check a field exists and is unique

source
meta def json_serializable.field_terminator (l : list (string × json)) :
exceptional unit

Check no fields remain

source
meta def get_constructor_and_projections (t : expr) :
tactic (name × (name × expr) × list (name × expr))

((c_name, c_fun), [(p_name, p_fun), ...]) ← get_constructor_and_projections `(struct n) gets the names and partial invocations of the constructor and projections of a structure

source
meta def of_json_helper (struct_name : name) (t : expr) (vars : list (name × pexpr)) (js : list (name × option expr)) :
tactic expr

Generate an expression that builds a term of type t (which is itself a parametrization of the structure struct_name) using the expressions resolving to parsed fields in vars and the expressions resolving to unparsed option json objects in js. This can handled dependently-typed and defaulted (via := which for structures is not the same as opt_param) fields.

source
meta def non_null_json_serializable_handler  :
derive_handler

A derive handler to serialize structures by their fields.

For the following structure:

structure has_default : Type :=
(x : ℕ := 2)
(y : fin x.succ := 3 * fin.of_nat x)
(z : ℕ := 3)

this generates an of_json parser along the lines of

meta def has_default.of_json (j : json) : exceptional (has_default) :=
do
  p ← json_serializable.field_starter j,
  (f_y, p) ← json_serializable.field_get p "y",
  (f_z, p) ← json_serializable.field_get p "z",
  f_y.mmap (of_json _) >>= option.elim
    (f_z.mmap (of_json _) >>= option.elim
      (pure {has_default.})
      (λ z, pure {has_default. z := z})
    )
    (λ y, f_z.mmap (of_json _) >>= option.elim
        (pure {has_default.})
        (λ z, pure {has_default. y := y, z := z})
    )