Commit 9f7fbaca authored by Léon Gondelman's avatar Léon Gondelman

fixed argument-evaluating deep embedding for a_invoke

parent 1ab5c71b
......@@ -130,10 +130,10 @@ Notation "'whileᶜ' ( e1 ) { e2 }" := (a_while (λ:<>, e1)%E (λ:<>, e2)%E)
Definition a_invoke: val := λ: "f" "arg",
a_seq_bind (λ: "a", a_atomic (λ: <>, "f" "a")) "arg".
Notation "f ❲ a ❳ " :=
Notation "'callᶜ' ( f , a )" :=
( a_invoke f a)%E
(at level 100, a at level 200,
format "f ❲ a ❳") : expr_scope.
format "'callᶜ' ( f , a )") : expr_scope.
Definition a_ptr_add : val := λ: "x" "y",
"lo" ←ᶜ ("x" ||| "y");;
......
......@@ -211,7 +211,7 @@ Inductive dcexpr : Type :=
| dCUnOp : un_op dcexpr dcexpr
| dCSeq : dcexpr dcexpr dcexpr
| dCPar : dcexpr dcexpr dcexpr
| dCInvoke (f: val) `{!Closed [] f} (de: dcexpr)
| dCInvoke (f: val) (de: dcexpr)
| dCUnknown (e : expr) `{!Closed [] e}.
Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
......@@ -226,7 +226,7 @@ Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
| dCUnOp op de => a_un_op op (dcexpr_interp E de)
| dCSeq de1 de2 => dcexpr_interp E de1 ; dcexpr_interp E de2
| dCPar de1 de2 => dcexpr_interp E de1 ||| dcexpr_interp E de2
| dCInvoke fv de => fv dcexpr_interp E de
| dCInvoke fv de => call (fv, dcexpr_interp E de)
| dCUnknown e1 => e1
end.
......@@ -253,7 +253,7 @@ Fixpoint dcexpr_wf (E: known_locs) (de: dcexpr) : bool :=
Lemma dval_wf_mono (E E': known_locs) (dv: dval) :
dval_wf E dv E `prefix_of` E' dval_wf E' dv.
Proof.
induction dv as [d| | |]; try naive_solver.
induction dv as [d| | |]; try naive_solver.
destruct d as [i|]; last done; simplify_eq /=.
intros Hb Hpre. case_bool_decide; last done.
clear Hb. generalize dependent E. revert E'. induction i as [| i].
......@@ -450,7 +450,7 @@ Proof. intros [-> ?] [-> ?]; split; simpl; auto. Qed.
Global Instance into_dcexpr_invoke E `{Closed [] e1} ef f `{!IntoVal ef f} de1 :
IntoDCexpr E e1 de1
IntoDCexpr E (efe1) (dCInvoke f de1).
IntoDCexpr E (call (ef, e1)) (dCInvoke f de1).
Proof.
intros. unfold IntoVal in *. simplify_eq /=.
split; simpl; auto; f_equal; by inversion H0.
......
......@@ -2,7 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
From iris.algebra Require Import frac.
From iris.bi Require Import big_op.
From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
From iris_c.c_translation Require Import monad translation proofmode.
From iris_c.c_translation Require Import monad translation proofmode derived.
From iris_c.lib Require Import locking_heap U.
Section test.
......@@ -39,7 +39,8 @@ Section test.
l1 C cloc_to_val l2 - l2 C v1 -
r1 C cloc_to_val r2 - r2 C v2 -
awp ( ♯ₗl1 = ♯ₗr1 ; ∗ᶜ ∗ᶜ ♯ₗl1 ) True
(λ w, w = v2 l1 C cloc_to_val r2 l2 C v1 r1 C cloc_to_val r2 - r2 C v2).
(λ w, w = v2
l1 C cloc_to_val r2 l2 C v1 r1 C cloc_to_val r2 - r2 C v2).
Proof.
iIntros "**". vcg_solver. eauto 40.
Qed.
......@@ -62,24 +63,42 @@ Section test.
Definition c_id : val := λ: "v", a_ret ("v").
Global Instance into_dcexpr_invoke E (ef e1 : expr) `{Closed [] e1} f `{!IntoVal ef f} de1 :
IntoDCexpr E e1 de1
IntoDCexpr E (efe1) (dCInvoke f de1) | 1.
Proof.
intros He1. unfold IntoVal in *. simplify_eq /=.
split; simpl; auto; f_equal; by inversion He1.
Qed.
Lemma test_invoke_1 (l: cloc) (v : val) R :
l C v -
AWP c_id❲∗ᶜ ♯ₗl @ R {{ v, v = #73 }}%I.
Lemma test_invoke_1 (l: cloc) R :
l C #42 -
AWP call (c_id, ∗ᶜ ♯ₗl) @ R {{ v, v = #42 l C #42 }}%I.
Proof.
iIntros "Hl". vcg_solver.
Admitted.
iIntros "Hl". awp_lam. awp_ret_value.
vcg_continue. eauto.
Qed.
Definition plus_pair : val := λ: "vv",
let: "v1" := Fst "vv" in
let: "v2" := Snd "vv" in
(a_ret "v1") + (a_ret "v2").
Lemma test_invoke_21 R :
AWP (call (plus_pair, 21 ||| 21)) @ R {{ v, v = #42 }}%I.
Proof.
iIntros. vcg_solver. awp_lam.
do 2 (awp_proj; awp_let).
vcg_solver. by vcg_continue.
Qed.
Lemma test_invoke_22 (l : cloc) R :
l C #21 -
AWP call (plus_pair, (∗ᶜ ♯ₗl ||| ∗ᶜ ♯ₗl)) @ R
{{ v, v = #42 l C #21 }}%I.
Proof.
iIntros. vcg_solver. iIntros "Hl". awp_lam.
do 2 (awp_proj; awp_let).
vcg_solver. iIntros "Hl". vcg_continue.
rewrite Qp_half_half. eauto 42 with iFrame.
Qed.
Lemma test6 (l : cloc) (z0 : Z) R:
Lemma test6 (l : cloc) (z0 : Z) R:
l C #z0 -
AWP ♯ₗl += 1 @ R {{ v, v = #z0 l C[LLvl] #(z0+1) }}.
Proof.
......
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