Commit a9718dfe authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Change instances to use refine (Coq 8.10 compatibility)

parent 94044028
Pipeline #11266 passed with stage
in 3 minutes and 28 seconds
...@@ -10,7 +10,7 @@ From Coq Require Import List. ...@@ -10,7 +10,7 @@ From Coq Require Import List.
Import RecordSetNotations. Import RecordSetNotations.
Import ListNotations. Import ListNotations.
Local Record ChainUpdate := Record ChainUpdate :=
build_chain_update { build_chain_update {
(* Contracts that had their states updated and the new state *) (* Contracts that had their states updated and the new state *)
upd_contracts : FMap Address OakValue; upd_contracts : FMap Address OakValue;
...@@ -114,14 +114,14 @@ Definition lc_interface : ChainInterface := ...@@ -114,14 +114,14 @@ Definition lc_interface : ChainInterface :=
Section ExecuteActions. Section ExecuteActions.
Context (initial_lce : LocalChainEnvironment). Context (initial_lce : LocalChainEnvironment).
Local Record ExecutionContext := Record ExecutionContext :=
build_execution_context { build_execution_context {
block_txs : list Tx; block_txs : list Tx;
new_update : ChainUpdate; new_update : ChainUpdate;
new_contracts : list (Address * WeakContract); new_contracts : list (Address * WeakContract);
}. }.
Local Instance eta_execution_context : Settable _ := Instance eta_execution_context : Settable _ :=
mkSettable mkSettable
((constructor build_execution_context) <*> block_txs ((constructor build_execution_context) <*> block_txs
<*> new_update <*> new_update
......
...@@ -33,7 +33,7 @@ Program Instance empty_set_ordered_type : UsualOrderedType Empty_set. ...@@ -33,7 +33,7 @@ Program Instance empty_set_ordered_type : UsualOrderedType Empty_set.
Solve Obligations with contradiction. Solve Obligations with contradiction.
Set Primitive Projections. Set Primitive Projections.
Local Record OakInterpretation := Record OakInterpretation :=
build_interpretation { build_interpretation {
oi_ty : Type; oi_ty : Type;
oi_order : OrderedType oi_ty; oi_order : OrderedType oi_ty;
...@@ -116,10 +116,11 @@ Instance oak_int_equivalence : OakTypeEquivalence Z := ...@@ -116,10 +116,11 @@ Instance oak_int_equivalence : OakTypeEquivalence Z :=
Instance oak_bool_equivalence : OakTypeEquivalence bool := Instance oak_bool_equivalence : OakTypeEquivalence bool :=
make_trivial_equiv oak_bool. make_trivial_equiv oak_bool.
Instance oak_nat_equivalence : OakTypeEquivalence nat := Instance oak_nat_equivalence : OakTypeEquivalence nat.
{| serialize n := serialize (Z.of_nat n);
deserialize z := do z' <- deserialize z; Some (Z.to_nat z'); |}.
Proof. Proof.
refine {| serialize n := serialize (Z.of_nat n);
deserialize z := do z' <- deserialize z; Some (Z.to_nat z');
ote_equivalence := _; |}.
intros x. intros x.
rewrite ote_equivalence. rewrite ote_equivalence.
simpl. simpl.
...@@ -136,46 +137,50 @@ Generalizable Variables A B. ...@@ -136,46 +137,50 @@ Generalizable Variables A B.
Instance oak_sum_equivalence Instance oak_sum_equivalence
`{e_a : OakTypeEquivalence A} `{e_a : OakTypeEquivalence A}
`{e_b : OakTypeEquivalence B} `{e_b : OakTypeEquivalence B}
: OakTypeEquivalence (A + B)%type := : OakTypeEquivalence (A + B)%type.
{| serialize s :=
let (is_left, ov) :=
match s with
| inl l => (true, serialize l)
| inr r => (false, serialize r)
end in
build_oak_value (oak_pair oak_bool ov.(oak_value_type)) (is_left, ov.(oak_value));
deserialize os :=
match os with
| build_oak_value (oak_pair oak_bool v) (b, val) =>
if b
then do a <- @deserialize _ e_a (build_oak_value v val);
Some (inl a)
else do b <- @deserialize _ e_b (build_oak_value v val);
Some (inr b)
| _ => None
end; |}.
Proof. Proof.
refine
{| serialize s :=
let (is_left, ov) :=
match s with
| inl l => (true, serialize l)
| inr r => (false, serialize r)
end in
build_oak_value (oak_pair oak_bool ov.(oak_value_type)) (is_left, ov.(oak_value));
deserialize os :=
match os with
| build_oak_value (oak_pair oak_bool v) (b, val) =>
if b
then do a <- @deserialize _ e_a (build_oak_value v val);
Some (inl a)
else do b <- @deserialize _ e_b (build_oak_value v val);
Some (inr b)
| _ => None
end;
ote_equivalence := _; |}.
intros [a | b]; simpl; rewrite ote_equivalence; reflexivity. intros [a | b]; simpl; rewrite ote_equivalence; reflexivity.
Defined. Defined.
Instance oak_pair_equivalence Instance oak_pair_equivalence
`{e_a : OakTypeEquivalence A} `{e_a : OakTypeEquivalence A}
`{e_b : OakTypeEquivalence B} `{e_b : OakTypeEquivalence B}
: OakTypeEquivalence (A * B)%type := : OakTypeEquivalence (A * B)%type.
{| serialize '(a, b) := Proof.
let 'build_oak_value a_oty a_val := serialize a in refine
let 'build_oak_value b_oty b_val := serialize b in {| serialize '(a, b) :=
build_oak_value (oak_pair a_oty b_oty) (a_val, b_val); let 'build_oak_value a_oty a_val := serialize a in
deserialize op := let 'build_oak_value b_oty b_val := serialize b in
match op with build_oak_value (oak_pair a_oty b_oty) (a_val, b_val);
| build_oak_value (oak_pair a_ty b_ty) (a_val, b_val) => deserialize op :=
do a <- @deserialize _ e_a (build_oak_value a_ty a_val); match op with
| build_oak_value (oak_pair a_ty b_ty) (a_val, b_val) =>
do a <- @deserialize _ e_a (build_oak_value a_ty a_val);
do b <- @deserialize _ e_b (build_oak_value b_ty b_val); do b <- @deserialize _ e_b (build_oak_value b_ty b_val);
Some (a, b) Some (a, b)
| _ => None | _ => None
end; end;
ote_equivalence := _;
|}. |}.
Proof.
intros [a b]. intros [a b].
simpl. simpl.
repeat rewrite ote_equivalence. repeat rewrite ote_equivalence.
...@@ -184,27 +189,28 @@ Defined. ...@@ -184,27 +189,28 @@ Defined.
Instance oak_list_equivalence Instance oak_list_equivalence
`{OakTypeEquivalence A} `{OakTypeEquivalence A}
: OakTypeEquivalence (list A) := : OakTypeEquivalence (list A).
{| serialize l :=
let go a acc :=
let 'build_oak_value a_oty a_val := serialize a in
let 'build_oak_value acc_oty acc_val := acc in
build_oak_value (oak_pair a_oty acc_oty) (a_val, acc_val) in
fold_right go (build_oak_value oak_unit tt) l;
deserialize ol :=
let fix aux (ty : OakType) (val : interp_type ty) : option (list A) :=
match ty, val with
| oak_pair hd_ty tl_ty, (hd_val, tl_val) =>
do hd <- deserialize (build_oak_value hd_ty hd_val);
do tl <- aux tl_ty tl_val;
Some (hd :: tl)
| oak_unit, _ => Some []
| _, _ => None
end in
let 'build_oak_value ol_ty ol_val := ol in
aux ol_ty ol_val;
|}.
Proof. Proof.
refine
{| serialize l :=
let go a acc :=
let 'build_oak_value a_oty a_val := serialize a in
let 'build_oak_value acc_oty acc_val := acc in
build_oak_value (oak_pair a_oty acc_oty) (a_val, acc_val) in
fold_right go (build_oak_value oak_unit tt) l;
deserialize ol :=
let fix aux (ty : OakType) (val : interp_type ty) : option (list A) :=
match ty, val with
| oak_pair hd_ty tl_ty, (hd_val, tl_val) =>
do hd <- deserialize (build_oak_value hd_ty hd_val);
do tl <- aux tl_ty tl_val;
Some (hd :: tl)
| oak_unit, _ => Some []
| _, _ => None
end in
let 'build_oak_value ol_ty ol_val := ol in
aux ol_ty ol_val;
ote_equivalence := _; |}.
induction x as [| hd tl IHl]. induction x as [| hd tl IHl].
- reflexivity. - reflexivity.
- simpl in *. - simpl in *.
...@@ -217,13 +223,14 @@ Instance oak_map_equivalence ...@@ -217,13 +223,14 @@ Instance oak_map_equivalence
`{OakTypeEquivalence A} `{OakTypeEquivalence A}
`{OrderedType A} `{OrderedType A}
`{OakTypeEquivalence B} `{OakTypeEquivalence B}
: OakTypeEquivalence (FMap A B) := : OakTypeEquivalence (FMap A B).
{| serialize m := serialize (FMap.elements m);
deserialize om :=
do elems <- deserialize om;
Some (FMap.of_list elems);
|}.
Proof. Proof.
refine
{| serialize m := serialize (FMap.elements m);
deserialize om :=
do elems <- deserialize om;
Some (FMap.of_list elems);
ote_equivalence := _; |}.
intros m. intros m.
rewrite ote_equivalence. rewrite ote_equivalence.
simpl. simpl.
...@@ -234,13 +241,14 @@ Defined. ...@@ -234,13 +241,14 @@ Defined.
Instance oak_set_equivalence Instance oak_set_equivalence
`{OakTypeEquivalence A} `{OakTypeEquivalence A}
`{OrderedType A} `{OrderedType A}
: OakTypeEquivalence (FSet A) := : OakTypeEquivalence (FSet A).
{| serialize s := serialize (FSet.elements s);
deserialize os :=
do elems <- deserialize os;
Some (FSet.of_list elems);
|}.
Proof. Proof.
refine
{| serialize s := serialize (FSet.elements s);
deserialize os :=
do elems <- deserialize os;
Some (FSet.of_list elems);
ote_equivalence := _; |}.
intros s. intros s.
rewrite ote_equivalence. rewrite ote_equivalence.
simpl. simpl.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment