Require Import List.
Import ListNotations.
Require Vector String.

Require Import Cheerios.BasicSerializers.
Require Import Cheerios.Core.
Require Import Cheerios.DeserializerMonad.
Require Import Cheerios.Tactics.
Require Import Cheerios.Types.

Require Import StructTact.StructTactics.
Import DeserializerNotations.

(* These functions are either missing obvious implicits, or have
   implicit arguments that are not marked "maximally inserted", which
   means they cannot easily be used with map or fmap. *)
Arguments Some {_} _.
Arguments cons {_} _ _.
Arguments option_map {_ _} _ _.
Arguments Vector.nil {_}.
Arguments Vector.cons {_} _ {_} _.

(* This section gives instances for various type constructors, including pairs
    and lists. *)

Section BasicCombinators.
  Variables A B : Type.
  Variable sA : Serializer A.
  Variable sB : Serializer B.

  Definition option_serialize (x : option A) : IOStreamWriter.t :=
    match x with
    | Some a => IOStreamWriter.append (fun _ => serialize true)
                              (fun _ => serialize a)
    | None => serialize false
    end.

  Definition option_deserialize : ByteListReader.t (option A) :=
    b <- deserialize ;;
      match b with
      | true => Some <$> deserialize
      | false => ByteListReader.ret None
      end.

  Lemma option_serialize_deserialize_id :
    serialize_deserialize_id_spec option_serialize option_deserialize.
  Proof using.
(* Goal: forall (a : A) (l : list A), @eq (list byte) (IOStreamWriter.unwrap (list_serialize_rec (@app A l (@cons A a (@nil A))))) (@app byte (IOStreamWriter.unwrap (list_serialize_rec l)) (IOStreamWriter.unwrap (@serialize A sA a))) *)
    intros.
(* Goal: @eq (option (prod (option A) (list byte))) (@ByteListReader.unwrap (option A) option_deserialize (@app byte (IOStreamWriter.unwrap (option_serialize a)) bytes)) (@Some (prod (option A) (list byte)) (@pair (option A) (list byte) a bytes)) *)
    unfold option_serialize, option_deserialize.
    destruct a;
      repeat (cheerios_crush; simpl).
  Qed.

  Global Instance option_Serializer : Serializer (option A).
  Proof.
    exact {| serialize := option_serialize;
             deserialize := option_deserialize;
             serialize_deserialize_id := option_serialize_deserialize_id |}.
  Qed.


  Definition pair_serialize (x : A * B) : IOStreamWriter.t :=
    let (a, b) := x in IOStreamWriter.append (fun _ => serialize a)
                                     (fun _ => serialize b).

  Definition pair_deserialize : ByteListReader.t (A * B) :=
    a <- deserialize ;;
      b <- deserialize ;;
      ByteListReader.ret (a, b).

  Lemma pair_serialize_deserialize_id :
    serialize_deserialize_id_spec pair_serialize pair_deserialize.
  Proof using.
(* Goal: forall (a : A) (l : list A), @eq (list byte) (IOStreamWriter.unwrap (list_serialize_rec (@app A l (@cons A a (@nil A))))) (@app byte (IOStreamWriter.unwrap (list_serialize_rec l)) (IOStreamWriter.unwrap (@serialize A sA a))) *)
    intros.
(* Goal: @eq (option (prod (prod A B) (list byte))) (@ByteListReader.unwrap (prod A B) pair_deserialize (@app byte (IOStreamWriter.unwrap (pair_serialize a)) bytes)) (@Some (prod (prod A B) (list byte)) (@pair (prod A B) (list byte) a bytes)) *)
    unfold pair_serialize, pair_deserialize.
(* Goal: @eq (option (prod (prod A B) (list byte))) (@ByteListReader.unwrap (prod A B) (@ByteListReader.bind A (prod A B) (@deserialize A sA) (fun a : A => @ByteListReader.bind B (prod A B) (@deserialize B sB) (fun b : B => @ByteListReader.ret (prod A B) (@pair A B a b)))) (@app byte (IOStreamWriter.unwrap (let (a, b) := a in IOStreamWriter.append (fun _ : unit => @serialize A sA a) (fun _ : unit => @serialize B sB b))) bytes)) (@Some (prod (prod A B) (list byte)) (@pair (prod A B) (list byte) a bytes)) *)
    destruct a.
(* Goal: forall (a : String.string) (bytes : list byte), @eq (option (prod String.string (list byte))) (@ByteListReader.unwrap String.string (@ByteListReader.map (list Ascii.ascii) String.string list_to_string (@deserialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer))) (@app byte (IOStreamWriter.unwrap (@serialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer) (string_to_list a))) bytes)) (@Some (prod String.string (list byte)) (@pair String.string (list byte) a bytes)) *)
    cheerios_crush.
  Qed.

  Global Instance pair_Serializer : Serializer (A * B).
  Proof.
    exact {| serialize := pair_serialize;
             deserialize := pair_deserialize;
             serialize_deserialize_id := pair_serialize_deserialize_id |}.
  Qed.

  Definition sum_serialize (x : A + B) : IOStreamWriter.t :=
    match x with
    | inl a => IOStreamWriter.append (fun _ => serialize true)
                             (fun _ => serialize a)
    | inr b => IOStreamWriter.append (fun _ => serialize false)
                             (fun _ => serialize b)
    end.

  Definition sum_deserialize : ByteListReader.t (A + B) :=
    b <- deserialize ;;
      match b with
      | true => inl <$> deserialize
      | false => inr <$> deserialize
      end.

  Lemma sum_serialize_deserialize_id :
    serialize_deserialize_id_spec sum_serialize sum_deserialize.
  Proof using.
(* Goal: forall (a : sum A B) (bytes : list byte), @eq (option (prod (sum A B) (list byte))) (@ByteListReader.unwrap (sum A B) sum_deserialize (@app byte (IOStreamWriter.unwrap (sum_serialize a)) bytes)) (@Some (prod (sum A B) (list byte)) (@pair (sum A B) (list byte) a bytes)) *)
    unfold sum_serialize, sum_deserialize.
(* Goal: forall (a : String.string) (bytes : list byte), @eq (option (prod String.string (list byte))) (@ByteListReader.unwrap String.string (@ByteListReader.map (list Ascii.ascii) String.string list_to_string (@deserialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer))) (@app byte (IOStreamWriter.unwrap (@serialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer) (string_to_list a))) bytes)) (@Some (prod String.string (list byte)) (@pair String.string (list byte) a bytes)) *)
    destruct a; cheerios_crush.
  Qed.

  Global Instance sum_Serializer : Serializer (A + B).
  Proof.
    exact {| serialize := sum_serialize;
             deserialize := sum_deserialize;
             serialize_deserialize_id := sum_serialize_deserialize_id
          |}.
  Qed.

  Fixpoint list_serialize_rec (l : list A) : IOStreamWriter.t :=
    match l with
    | [] => IOStreamWriter.empty
    | a :: l' => IOStreamWriter.append (fun _ => serialize a)
                               (fun _ => list_serialize_rec l')
    end.

  Definition list_serialize (l : list A) : IOStreamWriter.t :=
    IOStreamWriter.append (fun _ => serialize (length l))
                  (fun _ => list_serialize_rec l).

  Fixpoint list_deserialize_rec (n : nat) : ByteListReader.t (list A) :=
    match n with
    | 0 => ByteListReader.ret []
    | S n' => cons <$> deserialize <*> list_deserialize_rec n'
    end.

  Definition list_deserialize : ByteListReader.t (list A) :=
    deserialize >>= list_deserialize_rec.

  Lemma list_serialize_deserialize_id_rec :
    forall l bin, ByteListReader.unwrap (list_deserialize_rec (length l))
                                (IOStreamWriter.unwrap (list_serialize_rec l) ++ bin)
                  = Some(l, bin).
  Proof using.
(* Goal: forall (a : A) (l : list A), @eq (list byte) (IOStreamWriter.unwrap (list_serialize_rec (@app A l (@cons A a (@nil A))))) (@app byte (IOStreamWriter.unwrap (list_serialize_rec l)) (IOStreamWriter.unwrap (@serialize A sA a))) *)
    intros.
(* Goal: @eq (option (prod (list A) (list byte))) (@ByteListReader.unwrap (list A) (list_deserialize_rec (@length A l)) (@app byte (IOStreamWriter.unwrap (list_serialize_rec l)) bin)) (@Some (prod (list A) (list byte)) (@pair (list A) (list byte) l bin)) *)
    unfold list_serialize_rec.
(* Goal: forall (a : String.string) (bytes : list byte), @eq (option (prod String.string (list byte))) (@ByteListReader.unwrap String.string (@ByteListReader.map (list Ascii.ascii) String.string list_to_string (@deserialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer))) (@app byte (IOStreamWriter.unwrap (@serialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer) (string_to_list a))) bytes)) (@Some (prod String.string (list byte)) (@pair String.string (list byte) a bytes)) *)
    cheerios_crush. simpl.
(* Goal: @eq (list byte) (IOStreamWriter.unwrap (list_serialize_rec (@app A l (@cons A a (@nil A))))) (@app byte (IOStreamWriter.unwrap (list_serialize_rec l)) (IOStreamWriter.unwrap (@serialize A sA a))) *)
    induction l.
(* Goal: forall (a : String.string) (bytes : list byte), @eq (option (prod String.string (list byte))) (@ByteListReader.unwrap String.string (@ByteListReader.map (list Ascii.ascii) String.string list_to_string (@deserialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer))) (@app byte (IOStreamWriter.unwrap (@serialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer) (string_to_list a))) bytes)) (@Some (prod String.string (list byte)) (@pair String.string (list byte) a bytes)) *)
    - simpl. cheerios_crush.
(* Goal: @eq (option (prod (Vector.t A (S n)) (list byte))) (@ByteListReader.unwrap (Vector.t A (S n)) (@vector_deserialize (S n)) (@app byte (IOStreamWriter.unwrap (@vector_serialize (S n) (Vector.cons A h n a))) bytes)) (@Some (prod (Vector.t A (S n)) (list byte)) (@pair (Vector.t A (S n)) (list byte) (Vector.cons A h n a) bytes)) *)
    - simpl.
(* Goal: @eq (option (prod (list A) (list byte))) (@ByteListReader.unwrap (list A) (@sequence (list A) (list A) (@ByteListReader.map A (forall _ : list A, list A) (@cons A) (@deserialize A sA)) (list_deserialize_rec (@length A l))) (@app byte (IOStreamWriter.unwrap (IOStreamWriter.append (fun _ : unit => @serialize A sA a) (fun _ : unit => (fix list_serialize_rec (l : list A) : IOStreamWriter.t := match l with | nil => IOStreamWriter.empty | cons a l' => IOStreamWriter.append (fun _ : unit => @serialize A sA a) (fun _ : unit => list_serialize_rec l') end) l))) bin)) (@Some (prod (list A) (list byte)) (@pair (list A) (list byte) (@cons A a l) bin)) *)
      rewrite sequence_rewrite.
(* Goal: @eq (option (prod (list A) (list byte))) (@ByteListReader.unwrap (list A) (@ByteListReader.bind (list A) (list A) (list_deserialize_rec (@length A l)) (fun a0 : list A => @ByteListReader.ret (list A) (@cons A a a0))) (@app byte (IOStreamWriter.unwrap ((fix list_serialize_rec (l : list A) : IOStreamWriter.t := match l with | nil => IOStreamWriter.empty | cons a l' => IOStreamWriter.append (fun _ : unit => @serialize A sA a) (fun _ : unit => list_serialize_rec l') end) l)) bin)) (@Some (prod (list A) (list byte)) (@pair (list A) (list byte) (@cons A a l) bin)) *)
      rewrite ByteListReader.bind_unwrap.
(* Goal: @eq (option (prod (list A) (list byte))) match @ByteListReader.unwrap (forall _ : list A, list A) (@ByteListReader.map A (forall _ : list A, list A) (@cons A) (@deserialize A sA)) (@app byte (IOStreamWriter.unwrap (IOStreamWriter.append (fun _ : unit => @serialize A sA a) (fun _ : unit => (fix list_serialize_rec (l : list A) : IOStreamWriter.t := match l with | nil => IOStreamWriter.empty | cons a l' => IOStreamWriter.append (fun _ : unit => @serialize A sA a) (fun _ : unit => list_serialize_rec l') end) l))) bin) with | Some (pair v bytes as p) => @ByteListReader.unwrap (list A) (@ByteListReader.bind (list A) (list A) (list_deserialize_rec (@length A l)) (fun a : list A => @ByteListReader.ret (list A) (v a))) bytes | None => @None (prod (list A) (list byte)) end (@Some (prod (list A) (list byte)) (@pair (list A) (list byte) (@cons A a l) bin)) *)
      rewrite ByteListReader.map_unwrap.
(* Goal: @eq (option (prod (list A) (list byte))) match match @ByteListReader.unwrap A (@deserialize A sA) (@app byte (IOStreamWriter.unwrap (IOStreamWriter.append (fun _ : unit => @serialize A sA a) (fun _ : unit => (fix list_serialize_rec (l : list A) : IOStreamWriter.t := match l with | nil => IOStreamWriter.empty | cons a l' => IOStreamWriter.append (fun _ : unit => @serialize A sA a) (fun _ : unit => list_serialize_rec l') end) l))) bin) with | Some (pair v bin as p) => @Some (prod (forall _ : list A, list A) (list byte)) (@pair (forall _ : list A, list A) (list byte) (@cons A v) bin) | None => @None (prod (forall _ : list A, list A) (list byte)) end with | Some (pair v bytes as p) => @ByteListReader.unwrap (list A) (@ByteListReader.bind (list A) (list A) (list_deserialize_rec (@length A l)) (fun a : list A => @ByteListReader.ret (list A) (v a))) bytes | None => @None (prod (list A) (list byte)) end (@Some (prod (list A) (list byte)) (@pair (list A) (list byte) (@cons A a l) bin)) *)
      rewrite IOStreamWriter.append_unwrap.
(* Goal: @eq (option (prod (list A) (list byte))) match match @ByteListReader.unwrap A (@deserialize A sA) (@app byte (@app byte (IOStreamWriter.unwrap (@serialize A sA a)) (IOStreamWriter.unwrap ((fix list_serialize_rec (l : list A) : IOStreamWriter.t := match l with | nil => IOStreamWriter.empty | cons a l' => IOStreamWriter.append (fun _ : unit => @serialize A sA a) (fun _ : unit => list_serialize_rec l') end) l))) bin) with | Some (pair v bin as p) => @Some (prod (forall _ : list A, list A) (list byte)) (@pair (forall _ : list A, list A) (list byte) (@cons A v) bin) | None => @None (prod (forall _ : list A, list A) (list byte)) end with | Some (pair v bytes as p) => @ByteListReader.unwrap (list A) (@ByteListReader.bind (list A) (list A) (list_deserialize_rec (@length A l)) (fun a : list A => @ByteListReader.ret (list A) (v a))) bytes | None => @None (prod (list A) (list byte)) end (@Some (prod (list A) (list byte)) (@pair (list A) (list byte) (@cons A a l) bin)) *)
      rewrite app_ass.
(* Goal: @eq (option (prod (list A) (list byte))) match match @ByteListReader.unwrap A (@deserialize A sA) (@app byte (IOStreamWriter.unwrap (@serialize A sA a)) (@app byte (IOStreamWriter.unwrap ((fix list_serialize_rec (l : list A) : IOStreamWriter.t := match l with | nil => IOStreamWriter.empty | cons a l' => IOStreamWriter.append (fun _ : unit => @serialize A sA a) (fun _ : unit => list_serialize_rec l') end) l)) bin)) with | Some (pair v bin as p) => @Some (prod (forall _ : list A, list A) (list byte)) (@pair (forall _ : list A, list A) (list byte) (@cons A v) bin) | None => @None (prod (forall _ : list A, list A) (list byte)) end with | Some (pair v bytes as p) => @ByteListReader.unwrap (list A) (@ByteListReader.bind (list A) (list A) (list_deserialize_rec (@length A l)) (fun a : list A => @ByteListReader.ret (list A) (v a))) bytes | None => @None (prod (list A) (list byte)) end (@Some (prod (list A) (list byte)) (@pair (list A) (list byte) (@cons A a l) bin)) *)
      rewrite serialize_deserialize_id.
(* Goal: @eq (option (prod (list A) (list byte))) (@ByteListReader.unwrap (list A) (@ByteListReader.bind (list A) (list A) (list_deserialize_rec (@length A l)) (fun a0 : list A => @ByteListReader.ret (list A) (@cons A a a0))) (@app byte (IOStreamWriter.unwrap ((fix list_serialize_rec (l : list A) : IOStreamWriter.t := match l with | nil => IOStreamWriter.empty | cons a l' => IOStreamWriter.append (fun _ : unit => @serialize A sA a) (fun _ : unit => list_serialize_rec l') end) l)) bin)) (@Some (prod (list A) (list byte)) (@pair (list A) (list byte) (@cons A a l) bin)) *)
      rewrite ByteListReader.bind_unwrap.
(* Goal: @eq (list byte) (@app byte (IOStreamWriter.unwrap (@serialize A sA a0)) (IOStreamWriter.unwrap (list_serialize_rec (@app A l (@cons A a (@nil A)))))) (@app byte (IOStreamWriter.unwrap (@serialize A sA a0)) (@app byte (IOStreamWriter.unwrap (list_serialize_rec l)) (IOStreamWriter.unwrap (@serialize A sA a)))) *)
      rewrite IHl.
(* Goal: forall (a : String.string) (bytes : list byte), @eq (option (prod String.string (list byte))) (@ByteListReader.unwrap String.string (@ByteListReader.map (list Ascii.ascii) String.string list_to_string (@deserialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer))) (@app byte (IOStreamWriter.unwrap (@serialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer) (string_to_list a))) bytes)) (@Some (prod String.string (list byte)) (@pair String.string (list byte) a bytes)) *)
      cheerios_crush.
  Qed.

  Lemma serialize_snoc : forall (a : A) l,
      (IOStreamWriter.unwrap
         (list_serialize_rec (l ++ [a]))) =
      (IOStreamWriter.unwrap (list_serialize_rec l) ++ IOStreamWriter.unwrap (serialize a)).
  Proof using.
(* Goal: forall (a : A) (l : list A), @eq (list byte) (IOStreamWriter.unwrap (list_serialize_rec (@app A l (@cons A a (@nil A))))) (@app byte (IOStreamWriter.unwrap (list_serialize_rec l)) (IOStreamWriter.unwrap (@serialize A sA a))) *)
    intros.
(* Goal: @eq (list byte) (IOStreamWriter.unwrap (list_serialize_rec (@app A l (@cons A a (@nil A))))) (@app byte (IOStreamWriter.unwrap (list_serialize_rec l)) (IOStreamWriter.unwrap (@serialize A sA a))) *)
    induction l.
(* Goal: forall (a : String.string) (bytes : list byte), @eq (option (prod String.string (list byte))) (@ByteListReader.unwrap String.string (@ByteListReader.map (list Ascii.ascii) String.string list_to_string (@deserialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer))) (@app byte (IOStreamWriter.unwrap (@serialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer) (string_to_list a))) bytes)) (@Some (prod String.string (list byte)) (@pair String.string (list byte) a bytes)) *)
    - simpl. cheerios_crush.
(* Goal: @eq (list byte) (@app byte (IOStreamWriter.unwrap (@serialize A sA a)) (@nil byte)) (@app byte (@nil byte) (IOStreamWriter.unwrap (@serialize A sA a))) *)
      rewrite app_nil_r.
(* Goal: @eq (list byte) (@app byte (IOStreamWriter.unwrap (@serialize A sA a0)) (@app byte (IOStreamWriter.unwrap (list_serialize_rec l)) (IOStreamWriter.unwrap (@serialize A sA a)))) (@app byte (IOStreamWriter.unwrap (@serialize A sA a0)) (@app byte (IOStreamWriter.unwrap (list_serialize_rec l)) (IOStreamWriter.unwrap (@serialize A sA a)))) *)
      reflexivity.
(* Goal: @eq (option (prod (Vector.t A (S n)) (list byte))) (@ByteListReader.unwrap (Vector.t A (S n)) (@vector_deserialize (S n)) (@app byte (IOStreamWriter.unwrap (@vector_serialize (S n) (Vector.cons A h n a))) bytes)) (@Some (prod (Vector.t A (S n)) (list byte)) (@pair (Vector.t A (S n)) (list byte) (Vector.cons A h n a) bytes)) *)
    - simpl.
(* Goal: forall (a : String.string) (bytes : list byte), @eq (option (prod String.string (list byte))) (@ByteListReader.unwrap String.string (@ByteListReader.map (list Ascii.ascii) String.string list_to_string (@deserialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer))) (@app byte (IOStreamWriter.unwrap (@serialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer) (string_to_list a))) bytes)) (@Some (prod String.string (list byte)) (@pair String.string (list byte) a bytes)) *)
      cheerios_crush.
(* Goal: @eq (list byte) (@app byte (IOStreamWriter.unwrap (@serialize A sA a0)) (IOStreamWriter.unwrap (list_serialize_rec (@app A l (@cons A a (@nil A)))))) (@app byte (IOStreamWriter.unwrap (@serialize A sA a0)) (@app byte (IOStreamWriter.unwrap (list_serialize_rec l)) (IOStreamWriter.unwrap (@serialize A sA a)))) *)
      rewrite IHl.
(* Goal: @eq (list byte) (@app byte (IOStreamWriter.unwrap (@serialize A sA a0)) (@app byte (IOStreamWriter.unwrap (list_serialize_rec l)) (IOStreamWriter.unwrap (@serialize A sA a)))) (@app byte (IOStreamWriter.unwrap (@serialize A sA a0)) (@app byte (IOStreamWriter.unwrap (list_serialize_rec l)) (IOStreamWriter.unwrap (@serialize A sA a)))) *)
      reflexivity.
  Qed.

  Lemma list_serialize_deserialize_id :
    serialize_deserialize_id_spec list_serialize list_deserialize.
  Proof using.
(* Goal: forall (a : list A) (bytes : list byte), @eq (option (prod (list A) (list byte))) (@ByteListReader.unwrap (list A) list_deserialize (@app byte (IOStreamWriter.unwrap (list_serialize a)) bytes)) (@Some (prod (list A) (list byte)) (@pair (list A) (list byte) a bytes)) *)
    unfold list_serialize, list_deserialize.
(* Goal: forall (a : String.string) (bytes : list byte), @eq (option (prod String.string (list byte))) (@ByteListReader.unwrap String.string (@ByteListReader.map (list Ascii.ascii) String.string list_to_string (@deserialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer))) (@app byte (IOStreamWriter.unwrap (@serialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer) (string_to_list a))) bytes)) (@Some (prod String.string (list byte)) (@pair String.string (list byte) a bytes)) *)
    cheerios_crush.
(* Goal: @eq (option (prod (list A) (list byte))) (@ByteListReader.unwrap (list A) (list_deserialize_rec (@length A a)) (@app byte (IOStreamWriter.unwrap (list_serialize_rec a)) bytes)) (@Some (prod (list A) (list byte)) (@pair (list A) (list byte) a bytes)) *)
    now rewrite list_serialize_deserialize_id_rec.
  Qed.

  Global Instance list_Serializer : Serializer (list A).
  Proof.
    exact {| serialize := list_serialize;
             deserialize := list_deserialize;
             serialize_deserialize_id := list_serialize_deserialize_id
          |}.
  Qed.

  Fixpoint vector_serialize {n} (v : Vector.t A n) : IOStreamWriter.t :=
    match v with
    | Vector.nil => IOStreamWriter.empty
    | Vector.cons a v' => IOStreamWriter.append (fun _ => serialize a)
                                        (fun _ => vector_serialize v')
    end.

  Fixpoint vector_deserialize {n} : ByteListReader.t (Vector.t A n) :=
    match n as n0 return ByteListReader.t (Vector.t A n0) with
    | 0 => ByteListReader.ret Vector.nil
    | S n' => a <- deserialize ;;
                v <- vector_deserialize ;;
                ByteListReader.ret (Vector.cons a v)
    end.

  Lemma vector_serialize_deserialize_id :
    forall n, serialize_deserialize_id_spec vector_serialize (@vector_deserialize n).
  Proof using.
(* Goal: forall (a : A) (l : list A), @eq (list byte) (IOStreamWriter.unwrap (list_serialize_rec (@app A l (@cons A a (@nil A))))) (@app byte (IOStreamWriter.unwrap (list_serialize_rec l)) (IOStreamWriter.unwrap (@serialize A sA a))) *)
    induction n; intros.
    - destruct a using Vector.case0. auto. unfold vector_serialize,  vector_deserialize.
(* Goal: forall (a : String.string) (bytes : list byte), @eq (option (prod String.string (list byte))) (@ByteListReader.unwrap String.string (@ByteListReader.map (list Ascii.ascii) String.string list_to_string (@deserialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer))) (@app byte (IOStreamWriter.unwrap (@serialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer) (string_to_list a))) bytes)) (@Some (prod String.string (list byte)) (@pair String.string (list byte) a bytes)) *)
      cheerios_crush.
    - destruct a using Vector.caseS'.
(* Goal: @eq (option (prod (Vector.t A (S n)) (list byte))) (@ByteListReader.unwrap (Vector.t A (S n)) (@vector_deserialize (S n)) (@app byte (IOStreamWriter.unwrap (@vector_serialize (S n) (Vector.cons A h n a))) bytes)) (@Some (prod (Vector.t A (S n)) (list byte)) (@pair (Vector.t A (S n)) (list byte) (Vector.cons A h n a) bytes)) *)
      simpl.
(* Goal: forall (a : String.string) (bytes : list byte), @eq (option (prod String.string (list byte))) (@ByteListReader.unwrap String.string (@ByteListReader.map (list Ascii.ascii) String.string list_to_string (@deserialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer))) (@app byte (IOStreamWriter.unwrap (@serialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer) (string_to_list a))) bytes)) (@Some (prod String.string (list byte)) (@pair String.string (list byte) a bytes)) *)
      cheerios_crush.
(* Goal: @eq (option (prod (Vector.t A (S n)) (list byte))) match @ByteListReader.unwrap (Vector.t A n) (@vector_deserialize n) (@app byte (IOStreamWriter.unwrap (@vector_serialize n a)) bytes) with | Some (pair v bytes as p) => @ByteListReader.unwrap (Vector.t A (S n)) (@ByteListReader.ret (Vector.t A (S n)) (Vector.cons A h n v)) bytes | None => @None (prod (Vector.t A (S n)) (list byte)) end (@Some (prod (Vector.t A (S n)) (list byte)) (@pair (Vector.t A (S n)) (list byte) (Vector.cons A h n a) bytes)) *)
      rewrite IHn.
(* Goal: forall (a : String.string) (bytes : list byte), @eq (option (prod String.string (list byte))) (@ByteListReader.unwrap String.string (@ByteListReader.map (list Ascii.ascii) String.string list_to_string (@deserialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer))) (@app byte (IOStreamWriter.unwrap (@serialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer) (string_to_list a))) bytes)) (@Some (prod String.string (list byte)) (@pair String.string (list byte) a bytes)) *)
      cheerios_crush.
  Qed.

  Global Instance vector_Serializer n : Serializer (Vector.t A n).
  Proof.
    exact {| serialize := vector_serialize;
             deserialize := vector_deserialize;
             serialize_deserialize_id := vector_serialize_deserialize_id n
          |}.
  Qed.
End BasicCombinators.


(* This has to go here because it depends on having a serializer for
   lists available. *)

Fixpoint string_to_list s :=
  match s with
  | String.EmptyString => nil
  | String.String c s' => c :: (string_to_list s')
  end.

Fixpoint list_to_string l :=
  match l with
  | nil => String.EmptyString
  | h::l' => String.String h (list_to_string l')
  end.

Lemma string_to_list_to_string :
  forall s, list_to_string (string_to_list s) = s.
Proof.
(* Goal: @eq (option (prod (Vector.t A (S n)) (list byte))) (@ByteListReader.unwrap (Vector.t A (S n)) (@vector_deserialize (S n)) (@app byte (IOStreamWriter.unwrap (@vector_serialize (S n) (Vector.cons A h n a))) bytes)) (@Some (prod (Vector.t A (S n)) (list byte)) (@pair (Vector.t A (S n)) (list byte) (Vector.cons A h n a) bytes)) *)
  induction s; auto; simpl.
(* Goal: @eq String.string (String.String a (list_to_string (string_to_list s))) (String.String a s) *)
  now rewrite IHs.
Qed.

Definition string_serialize (s : String.string) :=
  serialize (string_to_list s).

Definition string_deserialize : ByteListReader.t String.string :=
  list_to_string <$> deserialize.

Lemma string_serialize_deserialize_id :
  serialize_deserialize_id_spec string_serialize string_deserialize.
Proof.
(* Goal: forall (a : String.string) (bytes : list byte), @eq (option (prod String.string (list byte))) (@ByteListReader.unwrap String.string string_deserialize (@app byte (IOStreamWriter.unwrap (string_serialize a)) bytes)) (@Some (prod String.string (list byte)) (@pair String.string (list byte) a bytes)) *)
  unfold string_deserialize, string_serialize.
(* Goal: forall (a : String.string) (bytes : list byte), @eq (option (prod String.string (list byte))) (@ByteListReader.unwrap String.string (@ByteListReader.map (list Ascii.ascii) String.string list_to_string (@deserialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer))) (@app byte (IOStreamWriter.unwrap (@serialize (list Ascii.ascii) (list_Serializer Ascii.ascii ascii_Serializer) (string_to_list a))) bytes)) (@Some (prod String.string (list byte)) (@pair String.string (list byte) a bytes)) *)
  cheerios_crush.
(* Goal: @eq (option (prod String.string (list byte))) (@Some (prod String.string (list byte)) (@pair String.string (list byte) (list_to_string (string_to_list a)) bytes)) (@Some (prod String.string (list byte)) (@pair String.string (list byte) a bytes)) *)
  now rewrite string_to_list_to_string.
Qed.

Instance string_Serializer : Serializer String.string.
Proof.
  exact {| serialize := string_serialize;
           deserialize := string_deserialize;
           serialize_deserialize_id := string_serialize_deserialize_id
        |}.
Qed.
