Commit 44759644 authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

Refactored encodable and minor clean up

parent f5bd0369
......@@ -3,6 +3,7 @@
theories/typing/involutive.v
theories/typing/side.v
theories/typing/stype.v
theories/encodings/encodable.v
theories/encodings/list.v
theories/encodings/auth_excl.v
theories/encodings/channel.v
......
From iris.heap_lang Require Import proofmode notation.
Class Encodable A := encode : A -> val.
Instance val_encodable : Encodable val := id.
Instance int_encodable : Encodable Z := λ n, #n.
Instance bool_encodable : Encodable bool := λ b, #b.
Instance unit_encodable : Encodable unit := λ _, #().
Instance loc_encodable : Encodable loc := λ l, #l.
Class Decodable A := decode : val -> option A.
Instance val_decodable : Decodable val := id $ Some.
Instance int_decodable : Decodable Z :=
λ v, match v with
| LitV (LitInt z) => Some z
| _ => None
end.
Instance bool_decodable : Decodable bool :=
λ v, match v with
| LitV (LitBool b) => Some b
| _ => None
end.
Instance loc_decodable : Decodable loc :=
λ v, match v with
| LitV (LitLoc l) => Some l
| _ => None
end.
Class EncDec (A : Type) {EA : Encodable A} {DA : Decodable A} :=
{
encdec : v, decode (encode v) = Some v;
decenc : (v : val) (w : A) , decode v = Some w -> encode w = v
}.
Ltac solve_encdec := intros v; by unfold decode, encode.
Ltac solve_decenc :=
intros v w H;
destruct v as [l | | | | ]; try by inversion H;
destruct l; try by inversion H.
Ltac solve_encdec_decenc :=
split; [solve_encdec | solve_decenc].
Instance val_encdec : EncDec val.
Proof.
split.
- intros v. unfold decode, encode. eauto.
- intros v w H. by destruct v; inversion H.
Qed.
Instance int_encdec : EncDec Z.
Proof. solve_encdec_decenc. Qed.
Instance bool_encdec : EncDec bool.
Proof. solve_encdec_decenc. Qed.
Instance loc_encdec : EncDec loc.
Proof. solve_encdec_decenc. Qed.
Lemma enc_dec {A : Type} `{ED : EncDec A}
v (w : A) : encode w = v <-> decode v = Some w.
Proof.
split.
- intros.
rewrite -encdec.
rewrite -H.
reflexivity.
- intros.
apply decenc. eauto.
Qed.
......@@ -273,7 +273,6 @@ Section stype_specs.
iApply (st_eval_send with "HP").
by iRewrite -"Heq".
}
iModIntro. iFrame. rewrite /is_st. auto.
Qed.
......
......@@ -3,72 +3,7 @@ From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import list auth excl.
From iris.base_logic Require Import invariants.
From osiris.encodings Require Export stype.
Class Encodable A := encode : A -> val.
Instance val_encodable : Encodable val := id.
Instance int_encodable : Encodable Z := λ n, #n.
Instance bool_encodable : Encodable bool := λ b, #b.
Instance unit_encodable : Encodable unit := λ _, #().
Instance loc_encodable : Encodable loc := λ l, #l.
Class Decodable A := decode : val -> option A.
Instance val_decodable : Decodable val := id $ Some.
Instance int_decodable : Decodable Z :=
λ v, match v with
| LitV (LitInt z) => Some z
| _ => None
end.
Instance bool_decodable : Decodable bool :=
λ v, match v with
| LitV (LitBool b) => Some b
| _ => None
end.
Instance loc_decodable : Decodable loc :=
λ v, match v with
| LitV (LitLoc l) => Some l
| _ => None
end.
Class EncDec (A : Type) {EA : Encodable A} {DA : Decodable A} :=
{
encdec : v, decode (encode v) = Some v;
decenc : (v : val) (w : A) , decode v = Some w -> encode w = v
}.
Ltac solve_encdec := intros v; by unfold decode, encode.
Ltac solve_decenc :=
intros v w H;
destruct v as [l | | | | ]; try by inversion H;
destruct l; try by inversion H.
Ltac solve_encdec_decenc :=
split; [solve_encdec | solve_decenc].
Instance val_encdec : EncDec val.
Proof.
split.
- intros v. unfold decode, encode. eauto.
- intros v w H. by destruct v; inversion H.
Qed.
Instance int_encdec : EncDec Z.
Proof. solve_encdec_decenc. Qed.
Instance bool_encdec : EncDec bool.
Proof. solve_encdec_decenc. Qed.
Instance loc_encdec : EncDec loc.
Proof. solve_encdec_decenc. Qed.
Lemma enc_dec {A : Type} `{ED : EncDec A}
v (w : A) : encode w = v <-> decode v = Some w.
Proof.
split.
- intros.
rewrite -encdec.
rewrite -H.
reflexivity.
- intros.
apply decenc. eauto.
Qed.
From osiris.encodings Require Export encodable stype.
Section DualStypeEnc.
Context `{EncDec V} `{PROP: bi} .
......
......@@ -57,8 +57,8 @@ Section ExampleProofsEnc.
Lemma heaplet_proof :
{{{ True }}} heaplet_example {{{ v l, RET v; v = #5 l v }}}.
Proof.
iIntros (Φ H) "HΦ".
rewrite /heaplet_example.
iIntros (Φ H) "HΦ".
wp_apply (new_chan_st_spec N (<!> v @ (v #5), TEnd))=> //;
iIntros (c γ) "[Hstl Hstr]"=> /=.
wp_apply (wp_fork with "[Hstl]").
......
......@@ -39,13 +39,13 @@ Notation "<!> x @ P , st" :=
Notation "<?> x @ P , st" :=
(TSR Receive (λ x, P%I) (λ x, st%stype))
(at level 200, x pattern, st at level 200) : stype_scope.
Notation "<!> x , st" := (<!> x @ True, (st x))%stype
Notation "<!> x , st" := (<!> x @ True, st%stype)%stype
(at level 200, x pattern, st at level 200) : stype_scope.
Notation "<?> x , st" := (<?> x @ True, (st x))%stype
Notation "<?> x , st" := (<?> x @ True, st%stype)%stype
(at level 200, x pattern, st at level 200) : stype_scope.
Notation "<!> @ P , st" := (<!> dummy__ @ P dummy__, st dummy__)%stype
Notation "<!> @ P , st" := (<!> x @ P x, st x)%stype
(at level 200, st at level 200) : stype_scope.
Notation "<?> @ P , st" := (<?> dummy__ @ P dummy__, st dummy__)%stype
Notation "<?> @ P , st" := (<?> x @ P x, st x)%stype
(at level 200, st at level 200) : stype_scope.
Section stype_ofe.
......
Markdown is supported
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