Use automatic Serializable derivation

theories/Congress.v

@@ -26,6 +26,7 @@ Context {BaseTypes : ChainBase}.
 
 Local Open Scope Z.
 Set Primitive Projections.
+Set Nonrecursive Elimination Schemes.
 
 Definition ProposalId := nat.
 
@@ -81,126 +82,25 @@ Instance state_settable : Settable _ :=
 
 Section Serialization.
 
-Definition deserialize_rules (v : SerializedValue) : option Rules :=
-  do '(a, b, c) <- deserialize v;
-  Some (build_rules a b c).
-
-Global Program Instance rules_serializable : Serializable Rules :=
-  {| serialize r := let (a, b, c) := r in serialize (a, b, c);
-     (* Why does
-     deserialize v :=
-       do '((a, b), c) <- deserialize v;
-       Some (build_rules a b c); |}.
-       not work here? *)
-     deserialize := deserialize_rules; |}.
-Next Obligation.
-  intros x. unfold deserialize_rules.
-  rewrite deserialize_serialize.
-  reflexivity.
-Qed.
+Global Instance rules_serializable : Serializable Rules :=
+  Derive Serializable Rules_rect <build_rules>.
 
-Global Program Instance setup_serializable : Serializable Setup :=
-  {| serialize s := serialize s.(setup_rules);
-     deserialize or :=
-       do rules <- deserialize or;
-       Some (build_setup rules); |}.
-Next Obligation.
-  intros x.
-  cbn.
-  rewrite deserialize_serialize.
-  reflexivity.
-Qed.
+Global Instance setup_serializable : Serializable Setup :=
+  Derive Serializable Setup_rect <build_setup>.
 
-Definition deserialize_congress_action (v : SerializedValue) : option CongressAction :=
-  do val <- deserialize v;
-  Some (match val with
-  | inl (to, amount) => cact_transfer to amount
-  | inr (to, amount, msg) => cact_call to amount msg
-  end).
-
-Global Program Instance congress_action_serializable : Serializable CongressAction :=
-  {| serialize ca :=
-       serialize
-         match ca with
-         | cact_transfer to amount => inl (to, amount)
-         | cact_call to amount msg => inr (to, amount, msg)
-         end;
-     deserialize := deserialize_congress_action; |}.
-Next Obligation.
-  intros ca.
-  unfold deserialize_congress_action.
-  rewrite deserialize_serialize.
-  destruct ca; reflexivity.
-Qed.
+Global Instance congress_action_serializable : Serializable CongressAction :=
+  Derive Serializable CongressAction_rect <cact_transfer, cact_call>.
 
-Definition deserialize_proposal (v : SerializedValue) : option Proposal :=
-  do '(a, b, c, d) <- deserialize v;
-  Some (build_proposal a b c d).
-
-Global Program Instance proposal_serializable : Serializable Proposal :=
-  {| serialize p :=
-       let (a, b, c, d) := p in
-       serialize (a, b, c, d);
-     deserialize := deserialize_proposal;
-  |}.
-Next Obligation.
-  intros p.
-  unfold deserialize_proposal.
-  rewrite deserialize_serialize.
-  destruct p; reflexivity.
-Qed.
+Global Instance proposal_serializable : Serializable Proposal :=
+  Derive Serializable Proposal_rect <build_proposal>.
 
-Definition serialize_msg (m : Msg) : SerializedValue :=
-  serialize
-    match m with
-    | transfer_ownership a => (0, serialize a)
-    | change_rules r => (1, serialize r)
-    | add_member a => (2, serialize a)
-    | remove_member a => (3, serialize a)
-    | create_proposal l => (4, serialize l)
-    | vote_for_proposal pid => (5, serialize pid)
-    | vote_against_proposal pid => (6, serialize pid)
-    | retract_vote pid => (7, serialize pid)
-    | finish_proposal pid => (8, serialize pid)
-    end.
+Global Instance msg_serializable : Serializable Msg :=
+  Derive Serializable Msg_rect <transfer_ownership, change_rules, add_member, remove_member,
+                                create_proposal, vote_for_proposal, vote_against_proposal,
+                                retract_vote, finish_proposal>.
 
-Definition deserialize_msg (v : SerializedValue) : option Msg :=
-  do '(tag, v) <- deserialize v;
-  match tag with
-  | 0 => option_map transfer_ownership (deserialize v)
-  | 1 => option_map change_rules (deserialize v)
-  | 2 => option_map add_member (deserialize v)
-  | 3 => option_map remove_member (deserialize v)
-  | 4 => option_map create_proposal (deserialize v)
-  | 5 => option_map vote_for_proposal (deserialize v)
-  | 6 => option_map vote_against_proposal (deserialize v)
-  | 7 => option_map retract_vote (deserialize v)
-  | 8 => option_map finish_proposal (deserialize v)
-  | _ => None
-  end.
-
-Global Program Instance msg_serializable : Serializable Msg :=
-  {| serialize := serialize_msg; deserialize := deserialize_msg; |}.
-Next Obligation.
-  intros msg.
-  unfold serialize_msg, deserialize_msg.
-  destruct msg; repeat (cbn; rewrite deserialize_serialize); reflexivity.
-Qed.
-
-Definition serialize_state (s : State) : SerializedValue :=
-  let (a, b, c, d, e) := s in
-  serialize (a, b, c, d, e).
-
-Definition deserialize_state (v : SerializedValue) : option State :=
-  do '(a, b, c, d, e) <- deserialize v;
-  Some (build_state a b c d e).
-
-Global Program Instance state_serializable : Serializable State :=
-  {| serialize := serialize_state; deserialize := deserialize_state; |}.
-Next Obligation.
-  unfold serialize_state, deserialize_state.
-  destruct x; repeat (cbn; rewrite deserialize_serialize); reflexivity.
-Qed.
+Global Instance state_serializable : Serializable State :=
+  Derive Serializable State_rect <build_state>.
 
 End Serialization.