lysxia / coq-ceres

Coq library for serialization to S-expressions

Cérès

Cérès is a Coq library for serialization to S-expressions.

S-expressions

S-expressions are uniform representations of structured data.

They are an alternative to plain strings as used by Show in Haskell and Debug in Rust for example. S-expressions are more amenable to programmatic consumption, avoiding custom parsers and enabling flexible formatting strategies.

Example

This S-expression...

(example
  (message "I'm a teapot")
  (code 418))

... corresponds to this sexp in Coq.

Definition example : sexp :=
  [ Atom "example"
  ; [ Atom "message" ; Atom (Str "I'm a teapot") ]
  ; [ Atom "code" ; Atom 418%Z ]
  ].

Documentation

The tutorial module is a good place for a quick start.

Link to the rendered documentation.

Simplified overview

This library offers a type sexp with two constructors:

Inductive sexp :=
| Atom (a : atom)
| List (xs : list sexp)
.

Atoms are identifiers (Raw), numbers (Num) or strings (Str).

Variant atom : Set :=
| Num (n : Z)       (* Integers. *)
| Str (s : string)  (* Literal strings. *)
| Raw (s : string)  (* Simple atoms (e.g., ADT tags). *)
                    (* Should fit in this alphabet: [A-Za-z0-9'=+*/:!?@#$%^&<>.,|_~-]. *)
.

Two classes Serialize and Deserialize are provided to define canonical serializers and deserializers between your types and S-expressions. The following functions are provided for conversions to sexp or directly to string:

Definition to_sexp {A} `{Serialize A} : A -> sexp.
Definition from_sexp {A} `{Deserialize A} : sexp -> error + A.

Definition to_string {A} `{Serialize A} : A -> string.
Definition from_string {A} `{Deserialize A} : string -> error + A.

Usage

Import the main module of the library.

Require Import Ceres.Ceres.

This exports:

• CeresS: the core definitions for S-expressions.
• CeresSerialize: the Serialize type class (sexp -> error + mytype).
• CeresDeserialize: the Deserialize type class (mytype -> sexp).
• CeresRoundtrip: roundtrip properties for serializers and deserializers.
• CeresFormat: format S-expressions as strings (sexp -> string).
• CeresParser: S-expression parser (string -> error + sexp).

Other modules in the library:

• CeresParserUtils: low-level primitives for the S-expression parser
• CeresParserRoundtrip, CeresParserRoundtripProof: Correctness proof of the parser. Currently, only soundness is proved (i.e., parse-then-print roundtrip).

Internals:

• CeresUtils: miscellaneous.
• CeresParserInternal: S-expression parser, internals
• CeresString: general string utilities.

Core definitions

The type of S-expressions is actually parameterized by the type of atoms.

Inductive sexp_ (A : Type) :=
| Atom_ (a : A)
| List (xs : list (sexp_ A))
.

By default, it is specialized to the atom type, so that the main S-expression type is sexp := sexp_ atom.

Notation sexp := (sexp_ atom).
Notation Atom := (@Atom_ atom).

Coercion Num : Z >-> atom.
Coercion Raw : string >-> atom.

(* Destructors *)
Definition get_Num : atom -> option Z.
Definition get_Str : atom -> option string.
Definition get_Raw : atom -> option string.

Serialization

Serializers can be defined as instances of the Serialize type class.

Class Serialize (A : Type) : Type :=
  to_sexp : A -> sexp.

S-expressions can be serialized to a string. Thus, so can serializable types.

Definition to_string {A : Type} `{Serialize A} : A -> string.

For numeric types, it is sufficient to define a conversion to Z as an instance of Integral.

Class Integral (A : Type) : Type :=
  to_Z : A -> Z.

Instance Serialize_Integral (A : Type) : Integral A -> Serialize A.

Deserialization

Going the other way requires some additional error handling.

Class Deserialize (A : Type) : Type := ...

Definition from_sexp {A} `{Deserialize A} : sexp -> error + A.
Definition from_string {A} `{Deserialize A} : string -> error + A.

Again, a simplified interface for numeric types is thus provided, with a SemiIntegral class.

Class SemiIntegral (A : Type) : Type :=
  from_Z : Z -> option A.

Instance Deserialize_SemiIntegral (A : Type) : SemiIntegral A -> Deserialize A.

Roundtrip properties

The module CeresRoundtrip defines some roundtripping properties and lemmas to help prove them.

Class CompleteClass {A} `{Serialize A} `{Deserialize A} : Prop.
Class SoundClass {A} `{Serialize A} `{Deserialize A} : Prop.

Generic encoding

There are no strong requirements on the encodings implemented by Serialize and Deserialize instances, but some utilities are provided for the following default encoding for inductive types:

• Nullary constructors are atoms con.
• Non-nullary constructors are lists (con x y z).

Serialization is straightforward by pattern-matching.

For deserialization, the module CeresDeserialize.Deser provides some utilities.

Standard types

• unit, bool, sum and option follow that standard encoding.
• (x, y) : prod A B is encoded as (X Y) where X and Y are the encodings of x and y.
• [x; y; z] : list A is encoded as (X Y Z).
• "somestring" : string is encoded as "somestring".
• "c" : ascii is encoded as "c".
• 33 : Z (or N, nat) is encoded as 33.

Recursive types

Recursive serializers and deserializers can be defined using explicit fixpoints.

For deserializers, that means to bind the expression explicitly, since that's the decreasing argument, but immediately pass it as the last argument of Deser.match_con:

Definition Deserialize_unary : Deserialize nat :=
  fix deser_nat (l : loc) (e : sexp) {struct e} :=
    Deser.match_con "nat"
      [ ("Z", 0%nat) ]
      [ ("S", Deser.con1 S deser_nat) ] l e.

Developer notes

Build the documentation

Extra directories:

• coqdocjs: a clone of coqdocjs
• doc: a clone of this repo's gh-pages branch

make html && rm -r doc/docs && mv html doc/docs
cd doc
git add docs && git commit -m "Update" && git push

See also

• Real World OCaml, Chapter 17, Data Serialization with S-expressions.
• Down with Show!, a blog post by Harry Garrood advocating for using structured representations instead of strings.

coq-ceres's Issues

Deserializers

eqb for sexp

I'm trying to define equivalence for sexp but didn't succeed. Do you have a solution?

(* begin hide *)
Definition uncurry {A B C} (f : A -> B -> C) (ab : A * B) : C :=
  let (a, b) := ab in f a b.

(* Backport for Coq < 8.9 *)
Local Open Scope lazy_bool_scope.
Fixpoint string_eqb s1 s2 : bool :=
 match s1, s2 with
 | EmptyString, EmptyString => true
 | String c1 s1', String c2 s2' => ascii_dec c1 c2 &&& string_eqb s1' s2'
 | _,_ => false
 end.
(* end hide *)

(** ** Equivalence *)

Fixpoint eqb (s1 s2 : sexp) : bool :=
  match s1, s2 with
  | Atom_ (Num n1), Atom_ (Num n2) => Z.eqb n1 n2
  | Atom_ (Str s1), Atom_ (Str s2) => string_eqb s1 s2
  | Atom_ (Raw s1), Atom_ (Raw s2) => string_eqb s1 s2
  | List l1, List l2 =>
    (length l1 =? length l2) &&& forallb (uncurry eqb) (combine l1 l2)
  | _, _ => false
  end.

Error: Cannot guess decreasing argument of fix.

Enable tests for Coq >= 8.10

I can't figure out the syntax to have some steps run conditionally in CI. See last commit on branch correct.

I want to run opam install -t for Coq >= 8.10, and just opam install for Coq <= 8.9

@liyishuai Do you know how to do this?

coq 8.13 support

Please add OPAM package compatible with coq 8.13

coq-8.11 support

The current OPAM package does not support Coq-8.11. Please consider supporting 8.11

Release 0.2.0

Just a reminder to myself that there are some unreleased changes.

Resolve warnings

Probably drop support for old versions of Coq

Deserialize: nullary constructors cannot be numbers

Is it a bug or feature?

Instance Deserialize__unit : Deserialize unit :=
  Deser.match_con "unit type" [("204", tt)] [].

Goal (from_string "204" = inl
        (DeserError [ ]
           ("could not read type '" ++ "unit type" ++ "', " ++
            "unexpected atom (expected list or nullary constructor name)"))).
Proof. reflexivity. Qed.

Instances for id

I'm trying to add Serialize and Deserialize instances for id, but they're not found.
Is this a Coq issue or where did I mess up?

Instance Serialize_id {A} {Serialize_A : Serialize A} : Serialize (id A) :=
  Serialize_A.
Fail Definition id_Z_to_sexp : id Z -> sexp atom := to_sexp.

The command has indeed failed with message:
Unable to satisfy the following constraints:

?Serialize : "Serialize (id Z)"

Pretty-printing

Extract Format.string_of_atom to OCaml

Uncommenting any line breaks the compilation:

(* From Coq Require Import ExtrOcamlNatInt. *)
(* From Coq Require Import ExtrOcamlString. *)
(* From Coq Require Import ExtrOcamlZInt. *)
From Ceres Require Import Format.
Extraction TestCompile string_of_atom.