Commit b2ed0162 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add an `AsVal` type class.

This class, in combination with `TCForall`, turns out the useful in
LambdaRust to express that lists of expressions are values.
parent 1a4f0348
...@@ -420,7 +420,7 @@ Lemma is_closed_of_val X v : is_closed X (of_val v). ...@@ -420,7 +420,7 @@ Lemma is_closed_of_val X v : is_closed X (of_val v).
Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed. Proof. apply is_closed_weaken_nil. induction v; simpl; auto. Qed.
Lemma is_closed_to_val X e v : to_val e = Some v is_closed X e. Lemma is_closed_to_val X e v : to_val e = Some v is_closed X e.
Proof. intros Hev; rewrite -(of_to_val e v Hev); apply is_closed_of_val. Qed. Proof. intros <-%of_to_val. apply is_closed_of_val. Qed.
Lemma is_closed_subst X e x es : Lemma is_closed_subst X e x es :
is_closed [] es is_closed (x :: X) e is_closed X (subst x es e). is_closed [] es is_closed (x :: X) e is_closed X (subst x es e).
......
...@@ -83,14 +83,12 @@ Qed. ...@@ -83,14 +83,12 @@ Qed.
Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto. Local Ltac solve_exec_safe := intros; subst; do 3 eexists; econstructor; eauto.
Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step. Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pure_exec := Local Ltac solve_pure_exec :=
repeat lazymatch goal with unfold AsRec, IntoVal, AsVal in *; subst;
| H: IntoVal ?e _ |- _ => rewrite -(of_to_val e _ into_val); clear H repeat match goal with H : is_Some _ |- _ => destruct H as [??] end;
| H: AsRec _ _ _ _ |- _ => rewrite H; clear H
end;
apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ]. apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
Global Instance pure_rec f x (erec e1 e2 : expr) (v2 : val) Global Instance pure_rec f x (erec e1 e2 : expr)
`{!IntoVal e2 v2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} : `{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)). PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
...@@ -110,11 +108,11 @@ Global Instance pure_if_false e1 e2 : ...@@ -110,11 +108,11 @@ Global Instance pure_if_false e1 e2 :
PureExec True (If (Lit (LitBool false)) e1 e2) e2. PureExec True (If (Lit (LitBool false)) e1 e2) e2.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_fst e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} : Global Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
PureExec True (Fst (Pair e1 e2)) e1. PureExec True (Fst (Pair e1 e2)) e1.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
Global Instance pure_snd e1 e2 v1 v2 `{!IntoVal e1 v1, !IntoVal e2 v2} : Global Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
PureExec True (Snd (Pair e1 e2)) e2. PureExec True (Snd (Pair e1 e2)) e2.
Proof. solve_pure_exec. Qed. Proof. solve_pure_exec. Qed.
...@@ -128,7 +126,7 @@ Proof. solve_pure_exec. Qed. ...@@ -128,7 +126,7 @@ Proof. solve_pure_exec. Qed.
(** Heap *) (** Heap *)
Lemma wp_alloc E e v : Lemma wp_alloc E e v :
to_val e = Some v IntoVal e v
{{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l v }}}. {{{ True }}} Alloc e @ E {{{ l, RET LitV (LitLoc l); l v }}}.
Proof. Proof.
iIntros (<-%of_to_val Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (<-%of_to_val Φ) "_ HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
...@@ -149,7 +147,7 @@ Proof. ...@@ -149,7 +147,7 @@ Proof.
Qed. Qed.
Lemma wp_store E l v' e v : Lemma wp_store E l v' e v :
to_val e = Some v IntoVal e v
{{{ l v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l v }}}. {{{ l v' }}} Store (Lit (LitLoc l)) e @ E {{{ RET LitV LitUnit; l v }}}.
Proof. Proof.
iIntros (<-%of_to_val Φ) ">Hl HΦ". iIntros (<-%of_to_val Φ) ">Hl HΦ".
...@@ -160,12 +158,12 @@ Proof. ...@@ -160,12 +158,12 @@ Proof.
iModIntro. iSplit=>//. by iApply "HΦ". iModIntro. iSplit=>//. by iApply "HΦ".
Qed. Qed.
Lemma wp_cas_fail E l q v' e1 v1 e2 v2 : Lemma wp_cas_fail E l q v' e1 v1 e2 :
to_val e1 = Some v1 to_val e2 = Some v2 v' v1 IntoVal e1 v1 AsVal e2 v' v1
{{{ l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E {{{ l {q} v' }}} CAS (Lit (LitLoc l)) e1 e2 @ E
{{{ RET LitV (LitBool false); l {q} v' }}}. {{{ RET LitV (LitBool false); l {q} v' }}}.
Proof. Proof.
iIntros (<-%of_to_val <-%of_to_val ? Φ) ">Hl HΦ". iIntros (<-%of_to_val [v2 <-%of_to_val] ? Φ) ">Hl HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto. iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?. iIntros (σ1) "Hσ !>". iDestruct (@gen_heap_valid with "Hσ Hl") as %?.
iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step. iSplit; first by eauto. iNext; iIntros (v2' σ2 efs Hstep); inv_head_step.
...@@ -173,7 +171,7 @@ Proof. ...@@ -173,7 +171,7 @@ Proof.
Qed. Qed.
Lemma wp_cas_suc E l e1 v1 e2 v2 : Lemma wp_cas_suc E l e1 v1 e2 v2 :
to_val e1 = Some v1 to_val e2 = Some v2 IntoVal e1 v1 IntoVal e2 v2
{{{ l v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E {{{ l v1 }}} CAS (Lit (LitLoc l)) e1 e2 @ E
{{{ RET LitV (LitBool true); l v2 }}}. {{{ RET LitV (LitBool true); l v2 }}}.
Proof. Proof.
......
...@@ -108,8 +108,8 @@ Proof. ...@@ -108,8 +108,8 @@ Proof.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono. rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed. Qed.
Lemma tac_wp_cas_fail Δ Δ' E i K l q v e1 v1 e2 v2 Φ : Lemma tac_wp_cas_fail Δ Δ' E i K l q v e1 v1 e2 Φ :
IntoVal e1 v1 IntoVal e2 v2 IntoVal e1 v1 AsVal e2
IntoLaterNEnvs 1 Δ Δ' IntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I v v1 envs_lookup i Δ' = Some (false, l {q} v)%I v v1
(Δ' WP fill K (Lit (LitBool false)) @ E {{ Φ }}) (Δ' WP fill K (Lit (LitBool false)) @ E {{ Φ }})
......
...@@ -210,7 +210,7 @@ Ltac solve_closed := ...@@ -210,7 +210,7 @@ Ltac solve_closed :=
Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances. Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
Ltac solve_to_val := Ltac solve_to_val :=
rewrite /IntoVal; rewrite /AsVal /IntoVal;
try match goal with try match goal with
| |- context E [language.to_val ?e] => | |- context E [language.to_val ?e] =>
let X := context E [to_val e] in change X let X := context E [to_val e] in change X
...@@ -224,6 +224,7 @@ Ltac solve_to_val := ...@@ -224,6 +224,7 @@ Ltac solve_to_val :=
apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
end. end.
Hint Extern 10 (IntoVal _ _) => solve_to_val : typeclass_instances. Hint Extern 10 (IntoVal _ _) => solve_to_val : typeclass_instances.
Hint Extern 10 (AsVal _) => solve_to_val : typeclass_instances.
Ltac solve_atomic := Ltac solve_atomic :=
match goal with match goal with
......
...@@ -126,4 +126,13 @@ Section language. ...@@ -126,4 +126,13 @@ Section language.
(* This is a family of frequent assumptions for PureExec *) (* This is a family of frequent assumptions for PureExec *)
Class IntoVal (e : expr Λ) (v : val Λ) := Class IntoVal (e : expr Λ) (v : val Λ) :=
into_val : to_val e = Some v. into_val : to_val e = Some v.
Class AsVal (e : expr Λ) := as_val : is_Some (to_val e).
(* There is no instance [IntoVal → AsVal] as often one can solve [AsVal] more
efficiently since no witness has to be computed. *)
Global Instance as_vals_of_val vs : TCForall AsVal (of_val <$> vs).
Proof.
apply TCForall_Forall, Forall_fmap, Forall_true=> v.
rewrite /AsVal /= to_of_val; eauto.
Qed.
End language. End language.
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