Ceres.CeresSerialize
Serialization to S-expressions.
Serialize a value to a string.
Integers are serializable.
Instance Serialize_Integral {A : Type} `(Integral A) : Serialize A :=
fun z => Atom (to_Z z).
Instance Integral_nat : Integral nat := Z.of_nat.
Instance Integral_N : Integral N := Z.of_N.
Instance Integral_Z : Integral Z := id.
fun z => Atom (to_Z z).
Instance Integral_nat : Integral nat := Z.of_nat.
Instance Integral_N : Integral N := Z.of_N.
Instance Integral_Z : Integral Z := id.
Instance Serialize_bool : Serialize bool
:= fun b => Atom (string_of_bool b).
Instance Serialize_option {A} `(Serialize A) : Serialize (option A)
:= fun oa =>
match oa with
| None => Atom "None"%string
| Some a => [ Atom "Some"%string ; to_sexp a ]%sexp
end.
Instance Serialize_sum {A B} `(Serialize A) `(Serialize B)
: Serialize (A + B)
:= fun ab =>
match ab with
| inl a => [ Atom "inl"%string ; to_sexp a ]%sexp
| inr b => [ Atom "inr"%string ; to_sexp b ]%sexp
end.
Instance Serialize_product {A B} `(Serialize A) `(Serialize B)
: Serialize (A * B)
:= fun ab => [ to_sexp (fst ab) ; to_sexp (snd ab) ]%sexp.
Instance Serialize_Empty_set : Serialize Empty_set
:= fun v => match v with end.
Instance Serialize_unit : Serialize unit
:= fun _ => Atom "tt"%string.
Instance Serialize_ascii : Serialize ascii
:= fun a => Atom (Str (String a "")).
Instance Serialize_string : Serialize string
:= fun s => Atom (Str s).
Instance Serialize_list {A} `{Serialize A} : Serialize (list A)
:= fun xs => List (List.map to_sexp xs).
Instance Serialize_sexp : Serialize sexp := id.