Skip to content

Commit d8cf8c2

Browse files
palmskogpalmskog
committed
build with latest version of libraries
1 parent d7c52ef commit d8cf8c2

File tree

9 files changed

+107
-113
lines changed

9 files changed

+107
-113
lines changed

‎extraction/aggregation-dynamic/coq/ExtractTreeAggregationDynamic.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Require Import Verdi.ExtrOcamlNatIntExt.
1212

1313
Require Import Verdi.ExtrOcamlBool.
1414
Require Import Verdi.ExtrOcamlList.
15-
Require Import Verdi.ExtrOcamlFin.
15+
Require Import Verdi.ExtrOcamlFinInt.
1616

1717
Require Import ExtractTreeAggregationDynamicDeps.
1818

‎extraction/aggregation/coq/ExtractTreeAggregationStatic.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ Require Import Verdi.ExtrOcamlNatIntExt.
2020

2121
Require Import Verdi.ExtrOcamlBool.
2222
Require Import Verdi.ExtrOcamlList.
23-
Require Import Verdi.ExtrOcamlFin.
23+
Require Import Verdi.ExtrOcamlFinInt.
2424

2525
Require Import ExtractTreeAggregationStaticDeps.
2626

‎extraction/tree-dynamic/coq/ExtractTreeDynamic.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Require Import Verdi.ExtrOcamlNatIntExt.
1515

1616
Require Import Verdi.ExtrOcamlBool.
1717
Require Import Verdi.ExtrOcamlList.
18-
Require Import Verdi.ExtrOcamlFin.
18+
Require Import Verdi.ExtrOcamlFinInt.
1919

2020
Module NumNames : NatValue. Definition n := 5. End NumNames.
2121
Module Names := FinName NumNames.

‎extraction/tree/coq/ExtractTreeStatic.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ Require Import Verdi.ExtrOcamlNatIntExt.
1515

1616
Require Import Verdi.ExtrOcamlBool.
1717
Require Import Verdi.ExtrOcamlList.
18-
Require Import Verdi.ExtrOcamlFin.
18+
Require Import Verdi.ExtrOcamlFinInt.
1919

2020
Module NumNames : NatValue. Definition n := 5. End NumNames.
2121
Module Names := FinName NumNames.

‎extraction/zaggregation-dynamic/coq/ExtractZTreeAggregationDynamic.v

+1-1
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Require Import Verdi.ExtrOcamlNatIntExt.
1313

1414
Require Import Verdi.ExtrOcamlBool.
1515
Require Import Verdi.ExtrOcamlList.
16-
Require Import Verdi.ExtrOcamlFin.
16+
Require Import Verdi.ExtrOcamlFinInt.
1717

1818
Require Import ExtractZTreeAggregationDynamicDeps.
1919

‎lib/BAddGroup.v

+18-58
Original file line numberDiff line numberDiff line change
@@ -2,21 +2,25 @@ From mathcomp.ssreflect
22
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
33
From mathcomp.ssreflect
44
Require Import choice fintype div path bigop prime finset.
5-
From mathcomp.fingroup
6-
Require Import fingroup.
75
From mathcomp.algebra
86
Require Import ssralg finalg.
97

10-
Require Import Bvector ZArith Zdigits.
8+
From mathcomp.fingroup
9+
Require Import fingroup.
10+
Require Import commfingroup.
11+
Require Import serializablecommfingroup.
12+
13+
Require Import Cheerios.Cheerios.
14+
15+
Require Import Bvector.
16+
Require Import ZArith.
17+
Require Import Zdigits.
1118

1219
Require Import BBase.
1320
Require Import BAddMul.
14-
1521
Require Import NatPowLt.
1622

17-
Require Import commfingroup.
18-
19-
Section BitVectorGroup.
23+
Section BVectorFinGroup.
2024

2125
Variable n : nat.
2226

@@ -231,6 +235,7 @@ Qed.
231235
Definition Bvector_finMixin := PcanFinMixin pcancel_Bvector_to_I2n.
232236
Canonical Bvector_finType := Eval hnf in FinType (Bvector n) Bvector_finMixin.
233237
Canonical Bvector_finZmodType := Eval hnf in [finZmodType of Bvector n].
238+
234239
Canonical Bvector_baseFinGroupType := Eval hnf in [baseFinGroupType of Bvector n for +%R].
235240
Canonical Bvector_finGroupType := Eval hnf in [finGroupType of Bvector n for +%R].
236241

@@ -240,7 +245,12 @@ Proof. exact: Bvector_addC. Qed.
240245
Definition Bvector_commFinGroupMixin := CommFinGroupMixin Bvector_mulgC.
241246
Canonical Bvector_commFinGroupType := Eval hnf in CommFinGroupType _ Bvector_commFinGroupMixin.
242247

243-
End BitVectorGroup.
248+
Definition Bvector_serializableCommFinGroupMixin :=
249+
@SerializableCommFinGroupMixin Bvector_commFinGroupType _ _ serialize_deserialize_id.
250+
Canonical Bvector_serializableCommFinGroupType :=
251+
Eval hnf in SerializableCommFinGroupType _ Bvector_serializableCommFinGroupMixin.
252+
253+
End BVectorFinGroup.
244254

245255
Section BitVectorMul.
246256

@@ -277,53 +287,3 @@ Canonical Bvector_comRingType := Eval hnf in ComRingType (Bvector n) (@Bvector_m
277287
Canonical Bvector_finComRingType := Eval hnf in [finComRingType of Bvector n].
278288

279289
End BitVectorRing.
280-
281-
Require Import serializablecommfingroup.
282-
283-
Require Import Cheerios.Cheerios.
284-
285-
Section BitVectorSerialization.
286-
287-
Variable n : nat.
288-
289-
Axiom Bvector_serialize : forall (v : Bvector n), IOStreamWriter.t.
290-
291-
Axiom Bvector_deserialize : ByteListReader.t (Bvector n).
292-
293-
Axiom Bvector_serialize_deserialize_id :
294-
serialize_deserialize_id_spec Bvector_serialize Bvector_deserialize.
295-
296-
(*
297-
Definition serialize (v : Bvector n) : list bool :=
298-
Vector.to_list v.
299-
300-
Fixpoint deserialize_aux k (bs : list bool) : option (Bvector k * list bool) :=
301-
match k, bs with
302-
| 0, bs' => Some (Bnil, bs')
303-
| S k', [::] => None
304-
| S k', (b :: bs')%SEQ =>
305-
match deserialize_aux k' bs' with
306-
| None => None
307-
| Some (v, bs'') => Some (Bcons b k' v, bs'')
308-
end
309-
end.
310-
311-
Definition deserialize (bs : list bool) : option (Bvector n * list bool) :=
312-
deserialize_aux n bs.
313-
314-
Lemma serialize_deserialize_id : serialize_deserialize_id_spec serialize deserialize.
315-
Proof.
316-
rewrite /serialize /deserialize /=.
317-
elim => //=.
318-
move => b n' v IH bs.
319-
by rewrite IH.
320-
Qed.
321-
*)
322-
323-
Definition Bvector_serializableMixin :=
324-
SerializableCommFinGroupMixin Bvector_serialize_deserialize_id.
325-
326-
Canonical Bvector_serializableCommFinGroupType :=
327-
SerializableCommFinGroupType (Bvector_commFinGroupType n) Bvector_serializableMixin.
328-
329-
End BitVectorSerialization.

‎lib/serializable.v

+63
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
Require Import Cheerios.Cheerios.
2+
3+
From mathcomp.ssreflect
4+
Require Import ssreflect ssrbool ssrnat ssrfun bigop eqtype.
5+
6+
Set Implicit Arguments.
7+
Unset Strict Implicit.
8+
Unset Printing Implicit Defensive.
9+
10+
Module Serializable.
11+
12+
Structure mixin_of (T : Type) := Mixin {
13+
ser : T -> IOStreamWriter.t;
14+
deser : ByteListReader.t T;
15+
_ : serialize_deserialize_id_spec ser deser
16+
}.
17+
18+
Structure type : Type := Pack {
19+
sort : Type;
20+
_ : mixin_of sort
21+
}.
22+
23+
Definition mixin T :=
24+
let: Pack _ m := T return mixin_of (sort T) in m.
25+
26+
Module Import Exports.
27+
Coercion sort : type >-> Sortclass.
28+
Coercion mixin : type >-> mixin_of.
29+
Notation serializableType := type.
30+
Notation SerializableMixin := Mixin.
31+
Notation SerializableType T m := (@Pack T m).
32+
End Exports.
33+
34+
End Serializable.
35+
Export Serializable.Exports.
36+
37+
Section SerializableOperations.
38+
39+
Variable T : serializableType.
40+
41+
Definition ser : T -> IOStreamWriter.t := Serializable.ser T.
42+
Definition deser : ByteListReader.t T := Serializable.deser T.
43+
44+
End SerializableOperations.
45+
46+
Section SerializableProps.
47+
48+
Variable T : serializableType.
49+
50+
Local Notation serT := (@ser T).
51+
Local Notation deserT := (@deser T).
52+
53+
Lemma ser_deser_id : serialize_deserialize_id_spec serT deserT.
54+
Proof. by case: T => ? []. Qed.
55+
56+
Global Instance serializable_Serializer : Serializer T :=
57+
{
58+
serialize := serT ;
59+
deserialize := deserT ;
60+
serialize_deserialize_id := ser_deser_id
61+
}.
62+
63+
End SerializableProps.

‎lib/serializablecommfingroup.v

+13-16
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@ From mathcomp
22
Require Import ssreflect ssrfun fingroup.
33

44
Require Import commfingroup.
5-
65
Require Import Cheerios.Cheerios.
6+
Require Import serializable.
77

88
Set Implicit Arguments.
99
Unset Strict Implicit.
@@ -14,9 +14,9 @@ Import GroupScope.
1414
Module SerializableCommFinGroup.
1515

1616
Structure mixin_of (gT : commFinGroupType) := Mixin {
17-
serialize : gT -> IOStreamWriter.t ;
18-
deserialize : ByteListReader.t gT ;
19-
_ : serialize_deserialize_id_spec serialize deserialize
17+
ser_gT : gT -> IOStreamWriter.t ;
18+
deser_gT : ByteListReader.t gT ;
19+
_ : serialize_deserialize_id_spec ser_gT deser_gT
2020
}.
2121

2222
Structure type : Type := Pack {
@@ -38,19 +38,16 @@ End Exports.
3838
End SerializableCommFinGroup.
3939
Export SerializableCommFinGroup.Exports.
4040

41-
Section SerializerDefs.
41+
Section SerializableCommGroupDefs.
42+
43+
Variable gT : serializableCommFinGroupType.
4244

43-
Variable T : serializableCommFinGroupType.
45+
Lemma ser_gT_deser_gT_id :
46+
serialize_deserialize_id_spec (SerializableCommFinGroup.ser_gT gT) (SerializableCommFinGroup.deser_gT gT).
47+
Proof. by case: gT => ? []. Qed.
4448

45-
Lemma serializeg_deserializeg_id :
46-
serialize_deserialize_id_spec (SerializableCommFinGroup.serialize T) (SerializableCommFinGroup.deserialize T).
47-
Proof. by case: T => ? []. Qed.
49+
Definition serCFG_serializableMixin := SerializableMixin ser_gT_deser_gT_id.
4850

49-
Global Instance FinGroupSerializer : Serializer T :=
50-
{
51-
serialize := SerializableCommFinGroup.serialize T ;
52-
deserialize := SerializableCommFinGroup.deserialize T ;
53-
serialize_deserialize_id := serializeg_deserializeg_id
54-
}.
51+
Canonical serCFG_serializableType := Eval hnf in SerializableType gT serCFG_serializableMixin.
5552

56-
End SerializerDefs.
53+
End SerializableCommGroupDefs.

‎systems/TreeAggregationDynamicSerialized.v

+8-34
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Require Import mathcomp.ssreflect.ssrbool.
1212
Require mathcomp.fingroup.fingroup.
1313

1414
Require Import commfingroup.
15+
Require Import serializable.
1516
Require Import serializablecommfingroup.
1617

1718
Require Import TreeAggregationDynamic.
@@ -44,45 +45,17 @@ Module TreeAggregationSerialized (Import NT : NameType)
4445
Module TANS := TreeAggregation NT NOT NSet NOTC NMap RNT SCFG.CFG ANT TA AD.
4546
Import TANS.
4647

47-
Import fingroup.GroupScope.
48-
49-
(*
50-
Definition option_lv_serialize (lvo : option lv) :=
51-
match lvo with
52-
| None => serialize x00
53-
| Some lv => Serializer.append (serialize x01) (serialize lv)
54-
end.
55-
56-
Definition option_lv_deserialize : Deserializer.t (option lv) :=
57-
tag <- deserialize ;;
58-
match tag with
59-
| x00 => Deserializer.ret None
60-
| x01 => Some <$> deserialize
61-
| _ => Deserializer.error
62-
end.
63-
64-
Lemma option_lv_serialize_deserialize_id :
65-
serialize_deserialize_id_spec option_lv_serialize option_lv_deserialize.
66-
Proof.
67-
rewrite /option_lv_serialize /option_lv_deserialize.
68-
case; repeat (cheerios_crush; simpl).
69-
Qed.
70-
71-
Instance option_lv_Serialize : Serializer (option lv) :=
72-
{
73-
serialize := option_lv_serialize ;
74-
deserialize := option_lv_deserialize ;
75-
serialize_deserialize_id := option_lv_serialize_deserialize_id
76-
}.
77-
*)
48+
Notation "a $ b" :=
49+
(IOStreamWriter.append (fun _ => a) (fun _ => b))
50+
(at level 100, right associativity).
7851

7952
Definition Msg_serialize (msg: Msg) :=
8053
match msg with
8154
| Aggregate m =>
82-
IOStreamWriter.append (fun _ => serialize x00) (fun _ => serialize m)
55+
serialize x00 $ serialize m
8356
| Fail => serialize x01
8457
| Level lvo =>
85-
IOStreamWriter.append (fun _ => serialize x02) (fun _ => serialize lvo)
58+
serialize x02 $ serialize lvo
8659
| New => serialize x03
8760
end.
8861

@@ -105,7 +78,8 @@ Lemma Msg_serialize_deserialize_id :
10578
Proof.
10679
rewrite /Msg_serialize /Msg_deserialize.
10780
case; repeat (cheerios_crush; simpl).
108-
by rewrite serializeg_deserializeg_id; cheerios_crush.
81+
rewrite (@serialize_deserialize_id _ (serializable_Serializer _)).
82+
by cheerios_crush.
10983
Qed.
11084

11185
Instance Msg_Serializer : Serializer Msg :=

0 commit comments

Comments
 (0)