Commit 6e625cb3 authored by Robbert Krebbers's avatar Robbert Krebbers

Less awkward syntax for call.

parent 816dd71e
...@@ -84,7 +84,7 @@ Definition a_load : val := λ: "x", ...@@ -84,7 +84,7 @@ Definition a_load : val := λ: "x",
end end
). ).
Notation "∗ᶜ e" := Notation "∗ᶜ e" :=
(a_load e)%E (at level 9, right associativity) : expr_scope. (a_load e)%E (at level 20, right associativity) : expr_scope.
Notation "'skipᶜ'" := (a_ret #()). Notation "'skipᶜ'" := (a_ret #()).
...@@ -137,10 +137,10 @@ Notation "'whileVᶜ' ( cnd ) { e }" := (a_while (LamV <> cnd) (LamV <> e)) ...@@ -137,10 +137,10 @@ Notation "'whileVᶜ' ( cnd ) { e }" := (a_while (LamV <> cnd) (LamV <> e))
Definition a_call: val := λ: "f" "arg", Definition a_call: val := λ: "f" "arg",
"a" ←ᶜ "arg" ; a_atomic (λ: <>, "f" "a"). "a" ←ᶜ "arg" ; a_atomic (λ: <>, "f" "a").
Notation "'callᶜ' ( f , a )" := Notation "'callᶜ' f a" :=
(a_call f a)%E (a_call f a)%E
(at level 10, f, a at level 99, (at level 10, f, a at level 9,
format "'callᶜ' ( f , a )") : expr_scope. format "'callᶜ' f a") : expr_scope.
Definition a_un_op (op : un_op) : val := λ: "x", Definition a_un_op (op : un_op) : val := λ: "x",
"v" ←ᶜ "x" ;; a_ret (UnOp op "v"). "v" ←ᶜ "x" ;; a_ret (UnOp op "v").
...@@ -509,7 +509,7 @@ Section proofs. ...@@ -509,7 +509,7 @@ Section proofs.
Lemma a_call_spec R Ψ Φ (f : val) ea : Lemma a_call_spec R Ψ Φ (f : val) ea :
AWP ea @ R {{ Ψ }} - AWP ea @ R {{ Ψ }} -
( a, Ψ a - U (R - AWP f a {{ v, R Φ v }})) - ( a, Ψ a - U (R - AWP f a {{ v, R Φ v }})) -
AWP call (f, ea) @ R {{ Φ }}. AWP call f ea @ R {{ Φ }}.
Proof. Proof.
iIntros "Ha Hfa". iIntros "Ha Hfa".
awp_apply (a_wp_awp R with "Ha"); iIntros (va) "Ha". awp_lam. awp_pures. awp_apply (a_wp_awp R with "Ha"); iIntros (va) "Ha". awp_lam. awp_pures.
......
...@@ -8,7 +8,7 @@ Definition factorial : val := λ: "n", ...@@ -8,7 +8,7 @@ Definition factorial : val := λ: "n",
"r" mut 1; "r" mut 1;
"c" mut 0; "c" mut 0;
while (∗ᶜ (a_ret "c") < a_ret "n") { while (∗ᶜ (a_ret "c") < a_ret "n") {
call (incr, a_ret "c"); call incr (a_ret "c");
a_ret "r" = ∗ᶜ (a_ret "r") * ∗ᶜ (a_ret "c") a_ret "r" = ∗ᶜ (a_ret "r") * ∗ᶜ (a_ret "c")
}; };
∗ᶜ(a_ret "r"). ∗ᶜ(a_ret "r").
......
...@@ -8,7 +8,7 @@ Section tests_vcg. ...@@ -8,7 +8,7 @@ Section tests_vcg.
Lemma test_invoke_1 (l: cloc) R : Lemma test_invoke_1 (l: cloc) R :
l C #42 - l C #42 -
AWP call (c_id, ∗ᶜ ♯ₗl) @ R {{ v, v = #42 l C #42 }}%I. AWP call c_id (∗ᶜ ♯ₗl) @ R {{ v, v = #42 l C #42 }}%I.
Proof. Proof.
iIntros "Hl". vcg. iIntros "Hl !> $". iIntros "Hl". vcg. iIntros "Hl !> $".
awp_lam. vcg. iIntros "Hl". vcg_continue. eauto. awp_lam. vcg. iIntros "Hl". vcg_continue. eauto.
...@@ -20,14 +20,14 @@ Section tests_vcg. ...@@ -20,14 +20,14 @@ Section tests_vcg.
(a_ret "v1") + (a_ret "v2"). (a_ret "v1") + (a_ret "v2").
Lemma test_invoke_2 R : Lemma test_invoke_2 R :
AWP call (plus_pair, 21 ||| 21) @ R {{ v, v = #42 }}%I. AWP call plus_pair (21 ||| 21) @ R {{ v, v = #42 }}%I.
Proof. Proof.
iIntros. vcg. iIntros "!> $". awp_lam. vcg. by vcg_continue. iIntros. vcg. iIntros "!> $". awp_lam. vcg. by vcg_continue.
Qed. Qed.
Lemma test_invoke_3 (l : cloc) R : Lemma test_invoke_3 (l : cloc) R :
l C #21 - l C #21 -
AWP call (plus_pair, (∗ᶜ ♯ₗl ||| ∗ᶜ ♯ₗl)) @ R AWP call plus_pair (∗ᶜ ♯ₗl ||| ∗ᶜ ♯ₗl) @ R
{{ v, v = #42 l C #21 }}%I. {{ v, v = #42 l C #21 }}%I.
Proof. Proof.
iIntros. vcg. iIntros "Hl !> $". awp_lam. vcg. iIntros. vcg. iIntros "Hl !> $". awp_lam. vcg.
......
...@@ -5,7 +5,7 @@ Definition inc : val := λ: "l", ...@@ -5,7 +5,7 @@ Definition inc : val := λ: "l",
a_ret "l" += 1 ; 1. a_ret "l" += 1 ; 1.
Definition par_inc : val := λ: "l", Definition par_inc : val := λ: "l",
call (inc, a_ret "l") + call (inc, a_ret "l"). call inc (a_ret "l") + call inc (a_ret "l").
Section par_inc. Section par_inc.
Context `{amonadG Σ, !inG Σ (frac_authR natR)}. Context `{amonadG Σ, !inG Σ (frac_authR natR)}.
...@@ -25,7 +25,7 @@ Section par_inc. ...@@ -25,7 +25,7 @@ Section par_inc.
iApply (awp_insert_res _ _ par_inc_inv with "[Hγ Hl]"). iApply (awp_insert_res _ _ par_inc_inv with "[Hγ Hl]").
{ iExists 0%nat. iFrame. } { iExists 0%nat. iFrame. }
iAssert ( (own γ (!{1 / 2} 0%nat) - iAssert ( (own γ (!{1 / 2} 0%nat) -
AWP call (inc, a_ret (cloc_to_val cl)) @ par_inc_inv R AWP call inc (a_ret (cloc_to_val cl)) @ par_inc_inv R
{{ v, v = #1 own γ (!{1 / 2} 1%nat) }}))%I as "#H". {{ v, v = #1 own γ (!{1 / 2} 1%nat) }}))%I as "#H".
{ iIntros "!> Hγ'". vcg; iIntros "!> [HR $]". iDestruct "HR" as (n') "[Hl Hγ]". { iIntros "!> Hγ'". vcg; iIntros "!> [HR $]". iDestruct "HR" as (n') "[Hl Hγ]".
iApply awp_fupd. iApply (inc_spec with "[$]"); iIntros "Hl". iApply awp_fupd. iApply (inc_spec with "[$]"); iIntros "Hl".
......
...@@ -254,7 +254,7 @@ Fixpoint dcexpr_interp (E : known_locs) (de : dcexpr) : expr := ...@@ -254,7 +254,7 @@ Fixpoint dcexpr_interp (E : known_locs) (de : dcexpr) : expr :=
| dCPar de1 de2 => dcexpr_interp E de1 ||| dcexpr_interp E de2 | dCPar de1 de2 => dcexpr_interp E de1 ||| dcexpr_interp E de2
| dCWhile de1 de2 => while (dcexpr_interp E de1) { dcexpr_interp E de2 } | dCWhile de1 de2 => while (dcexpr_interp E de1) { dcexpr_interp E de2 }
| dCWhileV de1 de2 => whileV (dcexpr_interp E de1) { dcexpr_interp E de2 } | dCWhileV de1 de2 => whileV (dcexpr_interp E de1) { dcexpr_interp E de2 }
| dCCall fv de => call (fv, dcexpr_interp E de) | dCCall fv de => call fv (dcexpr_interp E de)
| dCUnknown e1 => e1 | dCUnknown e1 => e1
end. end.
......
...@@ -220,7 +220,7 @@ Instance into_dcexpr_whileV E E' E'' e1 e2 de1 de2 : ...@@ -220,7 +220,7 @@ Instance into_dcexpr_whileV E E' E'' e1 e2 de1 de2 :
IntoDCExpr E E'' (whileV(e1) { e2 }) (dCWhileV de1 de2). IntoDCExpr E E'' (whileV(e1) { e2 }) (dCWhileV de1 de2).
Proof. solve_into_dcexpr2. Qed. Proof. solve_into_dcexpr2. Qed.
Instance into_dcexpr_call e1 E E' f de1 : Instance into_dcexpr_call e1 E E' f de1 :
IntoDCExpr E E' e1 de1 IntoDCExpr E E' (call (Val f, e1)) (dCCall f de1). IntoDCExpr E E' e1 de1 IntoDCExpr E E' (call (Val f) e1) (dCCall f de1).
Proof. intros [-> ??]; by split. Qed. Proof. intros [-> ??]; by split. Qed.
Instance into_dcexpr_unknown E e : IntoDCExpr E E e (dCUnknown e) | 100. Instance into_dcexpr_unknown E e : IntoDCExpr E E e (dCUnknown e) | 100.
Proof. done. Qed. Proof. done. Qed.
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