Commit f5deefa0 authored by Ralf Jung's avatar Ralf Jung

bind for fn arguments

parent f24dab9d
......@@ -132,6 +132,26 @@ Proof.
pclearbot. right. by apply CIH. }
Qed.
Lemma sim_body_bind_call r n fs ft es σs et σt (fns fnt: result) (pres pret: list result) posts postt Φ :
r {n,fs,ft} (es, σs) (et, σt)
: (λ r' n' rs' σs' rt' σt',
r' {n',fs,ft}
(Call fns ((of_result <$> pres) ++ (of_result rs') :: posts), σs')
(Call fnt ((of_result <$> pret) ++ (of_result rt') :: postt), σt')
: Φ)
r {n,fs,ft}
(Call fns ((of_result <$> pres) ++ es :: posts), σs)
(Call fnt ((of_result <$> pret) ++ et :: postt), σt)
: Φ.
Proof.
intros HH.
eapply sim_body_bind with
(Ks:=[CallRCtx fns pres posts]) (es:=es)
(Kt:=[CallRCtx fnt pret postt]) (et:=et).
simpl. apply HH.
Qed.
Lemma sim_body_result fs ft r n es et σs σt Φ :
( r Φ r n es σs et σt : Prop)
......
......@@ -129,6 +129,50 @@ Proof.
+ apply IHv. done.
Qed.
Lemma sim_simple_call_args' r r' (el1 el2: list expr) (rs rt: result) Φ :
Forall2 (λ e1 e2, core r ⊨ˢ{sem_steps,fs,ft} (e1, css) (e2, cst) : sem_post) el1 el2
( r' (vs vt: list result),
Forall2 (rrel r') vs vt
core r r' ⊨ˢ{sem_steps,fs,ft}
(Call rs (of_result <$> vs), css) (Call rt (of_result <$> vt), cst)
: Φ )
vs vt, Forall2 (rrel r') vs vt
core r r' ⊨ˢ{sem_steps,fs,ft}
(Call rs ((of_result <$> vs) ++ el1), css) (Call rt ((of_result <$> vt) ++ el2), cst)
: Φ.
Proof.
intros He Hcont. revert r'. induction He; intros r'.
{ intros vs vt ?. rewrite !app_nil_r. eapply (Hcont _ vs vt). done. }
clear Hcont. intros vs vt Hvst.
eapply sim_simple_bind_call.
rewrite cmra_core_dup -assoc.
eapply sim_simple_frame_r.
eapply sim_simple_post_mono, H.
intros r'' n' rs' css' rt' cst' (-> & -> & -> & [Hrel ?]%rrel_with_eq).
simplify_eq/=.
rewrite !cons_middle !assoc.
change [rt']%E with (of_result <$> [rt']).
rewrite - !fmap_app. rewrite [r'' core r]comm -assoc=>Hval.
eapply IHHe. eapply Forall2_app.
- eapply Forall2_impl; first done. intros.
eapply rrel_mono; last done; eauto using cmra_valid_included.
- constructor; last done.
eapply rrel_mono; last done; eauto using cmra_valid_included.
Qed.
Lemma sim_simple_call_args r r' (el1 el2: list expr) (rs rt: result) Φ :
Forall2 (λ e1 e2, core r ⊨ˢ{sem_steps,fs,ft} (e1, css) (e2, cst) : sem_post) el1 el2
( r' (vs vt: list result),
Forall2 (rrel r') vs vt
core r r' ⊨ˢ{sem_steps,fs,ft}
(Call rs (of_result <$> vs), css) (Call rt (of_result <$> vt), cst)
: Φ )
core r r' ⊨ˢ{sem_steps,fs,ft} (Call rs el1, css) (Call rt el2, cst) : Φ.
Proof.
intros He Hcont.
eapply sim_simple_call_args' with (vs:=[]) (vt:=[]); auto.
Qed.
Lemma expr_wf_soundness r e :
expr_wf e sem_wf r e e.
Proof.
......@@ -148,10 +192,17 @@ Proof.
eapply (Hxswf (rs, rt)). done.
+ simpl. apply sim_simple_var.
- (* Call *)
move=>[Hwf1 Hwf2] xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
move=>[Hwf1 /Forall_id Hwf2] xs Hxswf /=. sim_bind (subst_map _ e) (subst_map _ e).
eapply sim_simple_frame_core.
eapply sim_simple_post_mono, IHe; [|by auto..].
intros r' n' rs css' rt cst' (-> & -> & -> & Hrel). simpl.
admit.
intros r' n' rs css' rt cst' (-> & -> & -> & Hrel) Hval. simpl.
eapply sim_simple_call_args.
{ induction Hwf2; simpl; first by auto.
destruct (Forall_cons_1 _ _ _ H) as [IHx IHl]. constructor.
- eapply IHx; auto. exact: srel_persistent.
- eapply IHHwf2. done. }
intros r'' rs' rt' Hrel'.
admit. (* needs call lemma that works with any result. *)
- (* InitCall *) done.
- (* EndCall *) done.
- (* Proj *)
......
......@@ -180,6 +180,25 @@ Proof.
clear. simpl. intros r n vs σs vt σt HH. exact: HH.
Qed.
Lemma sim_simple_bind_call r n fs ft es css et cst (fns fnt: result) (pres pret: list result) posts postt Φ :
r ⊨ˢ{n,fs,ft} (es, css) (et, cst)
: (λ r' n' rs' css' rt' cst',
r' ⊨ˢ{n',fs,ft}
(Call fns ((of_result <$> pres) ++ (of_result rs') :: posts), css')
(Call fnt ((of_result <$> pret) ++ (of_result rt') :: postt), cst')
: Φ)
r ⊨ˢ{n,fs,ft}
(Call fns ((of_result <$> pres) ++ es :: posts), css)
(Call fnt ((of_result <$> pret) ++ et :: postt), cst)
: Φ.
Proof.
intros HH σs σt <-<-. apply sim_body_bind_call.
eapply sim_local_body_post_mono; last exact: HH.
clear. simpl. intros r n vs σs vt σt HH. exact: HH.
Qed.
Lemma sim_simple_val fs ft r n (vs vt: value) css cst Φ :
Φ r n vs css vt cst
r ⊨ˢ{n,fs,ft} (vs, css) (vt, cst) : Φ.
......
......@@ -13,8 +13,8 @@ Ltac reshape_expr e tac :=
with go K e :=
match e with
| _ => tac K e
| Call (Val ?v) ?el => go_call K (ValR v) (@nil val) el
| Call (of_result ?r) ?el => go_call K r (@nil val) el
| Call (Val ?v) ?el => go_call K (ValR v) (@nil result) el
| Call (of_result ?r) ?el => go_call K r (@nil result) el
| Call ?e ?el => go (CallLCtx el :: K) e
| EndCall ?e => go (EndCallCtx :: K) e
| BinOp ?op (Val ?v1) ?e2 => go (BinOpRCtx op (ValR v1) :: K) e2
......
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