mathlib documentation


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 true 0 none, and reserializing give {"success": true, "verbose": 0, "extras": null}.

Main definitions #

@[protected, instance]
meta structure json_serializable (α : Type) :

A class to indicate that a type is json serializable

Instances of this typeclass
meta def json.typename  :

Describe the type of a json value

Primitive types #

@[protected, instance]
@[protected, instance]

Basic coercions #

@[protected, instance]
@[protected, instance]
meta def subtype.json_serializable {α : Type} [json_serializable α] (p : α → Prop) [decidable_pred p] :
@[protected, instance]
@[protected, instance]

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

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.

Begin parsing fields

Check a field exists and is unique

Check no fields remain

((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

meta def of_json_helper (struct_name : name) (t : expr) (vars : list (name × pexpr)) (js : list (name × option 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.

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) :=
  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})