diff --git a/theories/c_translation/translation.v b/theories/c_translation/translation.v index 7f7ff122814641eb228e272a871cf1ae4c91fdf0..1ab3d0157e4bed7c6d04a3f3dfcaa2e60bd802d5 100644 --- a/theories/c_translation/translation.v +++ b/theories/c_translation/translation.v @@ -84,7 +84,7 @@ Definition a_load : val := λ: "x", end ). 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 #()). @@ -137,10 +137,10 @@ Notation "'whileVᶜ' ( cnd ) { e }" := (a_while (LamV <> cnd) (LamV <> e)) Definition a_call: val := λ: "f" "arg", "a" ←ᶜ "arg" ;ᶜ a_atomic (λ: <>, "f" "a"). -Notation "'callᶜ' ( f , a )" := +Notation "'callᶜ' f a" := (a_call f a)%E - (at level 10, f, a at level 99, - format "'callᶜ' ( f , a )") : expr_scope. + (at level 10, f, a at level 9, + format "'callᶜ' f a") : expr_scope. Definition a_un_op (op : un_op) : val := λ: "x", "v" ←ᶜ "x" ;;ᶜ a_ret (UnOp op "v"). @@ -509,7 +509,7 @@ Section proofs. Lemma a_call_spec R Ψ Φ (f : val) ea : AWP ea @ R {{ Ψ }} -∗ (∀ a, Ψ a -∗ U (R -∗ AWP f a {{ v, R ∗ Φ v }})) -∗ - AWP callᶜ (f, ea) @ R {{ Φ }}. + AWP callᶜ f ea @ R {{ Φ }}. Proof. iIntros "Ha Hfa". awp_apply (a_wp_awp R with "Ha"); iIntros (va) "Ha". awp_lam. awp_pures. diff --git a/theories/tests/fact.v b/theories/tests/fact.v index 36d9ad43dd7b06dbe3510418fa07d05a81dbb90f..2369ff8030fb2b8d242d2af3b594bee4f9615a10 100644 --- a/theories/tests/fact.v +++ b/theories/tests/fact.v @@ -8,7 +8,7 @@ Definition factorial : val := λ: "n", "r" ←mutᶜ ♯1;ᶜ "c" ←mutᶜ ♯0;ᶜ 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"). diff --git a/theories/tests/invoke.v b/theories/tests/invoke.v index e933a944467535c7726bba3c624a3902bd9e9a89..076d0dfc88550d3375d6c344a39fc79f43de3533 100644 --- a/theories/tests/invoke.v +++ b/theories/tests/invoke.v @@ -8,7 +8,7 @@ Section tests_vcg. Lemma test_invoke_1 (l: cloc) R : 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. iIntros "Hl". vcg. iIntros "Hl !> \$". awp_lam. vcg. iIntros "Hl". vcg_continue. eauto. @@ -20,14 +20,14 @@ Section tests_vcg. (a_ret "v1") +ᶜ (a_ret "v2"). 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. iIntros. vcg. iIntros "!> \$". awp_lam. vcg. by vcg_continue. Qed. Lemma test_invoke_3 (l : cloc) R : l ↦C #21 -∗ - AWP callᶜ (plus_pair, (∗ᶜ ♯ₗl |||ᶜ ∗ᶜ ♯ₗl)) @ R + AWP callᶜ plus_pair (∗ᶜ ♯ₗl |||ᶜ ∗ᶜ ♯ₗl) @ R {{ v, ⌜v = #42⌝ ∗ l ↦C #21 }}%I. Proof. iIntros. vcg. iIntros "Hl !> \$". awp_lam. vcg. diff --git a/theories/tests/par_inc.v b/theories/tests/par_inc.v index 9655ab8f231cefbfd8edca0419993b504c8fb643..b50cc76ec5fac8e2dbc3cb155b4b4a572b8a3fc4 100644 --- a/theories/tests/par_inc.v +++ b/theories/tests/par_inc.v @@ -5,7 +5,7 @@ Definition inc : val := λ: "l", a_ret "l" +=ᶜ ♯ 1 ;ᶜ ♯ 1. 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. Context `{amonadG Σ, !inG Σ (frac_authR natR)}. @@ -25,7 +25,7 @@ Section par_inc. iApply (awp_insert_res _ _ par_inc_inv with "[Hγ Hl]"). { iExists 0%nat. iFrame. } 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". { iIntros "!> Hγ'". vcg; iIntros "!> [HR \$]". iDestruct "HR" as (n') "[Hl Hγ]". iApply awp_fupd. iApply (inc_spec with "[\$]"); iIntros "Hl". diff --git a/theories/vcgen/dcexpr.v b/theories/vcgen/dcexpr.v index d722ae5d63d72e8939a7cfa1e3ed4f7acadc367f..fc2a0be785d6594dd138298066b8358234849109 100644 --- a/theories/vcgen/dcexpr.v +++ b/theories/vcgen/dcexpr.v @@ -254,7 +254,7 @@ Fixpoint dcexpr_interp (E : known_locs) (de : dcexpr) : expr := | dCPar de1 de2 => 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 } - | dCCall fv de => callᶜ (fv, dcexpr_interp E de) + | dCCall fv de => callᶜ fv (dcexpr_interp E de) | dCUnknown e1 => e1 end. diff --git a/theories/vcgen/reification.v b/theories/vcgen/reification.v index ad69279a13f25cd2f3c92a7137ba2f646259e255..24b3afbe3c4374e432d86324ac8793cf5d0344c5 100644 --- a/theories/vcgen/reification.v +++ b/theories/vcgen/reification.v @@ -220,7 +220,7 @@ Instance into_dcexpr_whileV E E' E'' e1 e2 de1 de2 : IntoDCExpr E E'' (whileVᶜ(e1) { e2 }) (dCWhileV de1 de2). Proof. solve_into_dcexpr2. Qed. 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. Instance into_dcexpr_unknown E e : IntoDCExpr E E e (dCUnknown e) | 100. Proof. done. Qed.