Commit e2e3e1d9 authored by Ralf Jung's avatar Ralf Jung
Browse files

step over call

parent 42fe994a
......@@ -28,26 +28,29 @@ Definition ex1_opt : function :=
Lemma ex1_sim_body fs ft : ⊨ᶠ{fs,ft} ex1 ex1_opt.
Proof.
apply (sim_fun_simple1 10)=>// rf es css et cs vs vt FREL ??. simplify_eq/=.
apply (sim_fun_simple1 10)=>// rarg es css et cs args argt AREL ??. simplify_eq/=.
(* InitCall *)
apply sim_simple_init_call=> c /= {css}.
(* Alloc *)
sim_apply sim_simple_alloc_local=> l t /=.
sim_apply sim_simple_let_place=>/=.
(* Write *)
rewrite (vrel_eq _ _ _ FREL).
rewrite (vrel_eq _ _ _ AREL).
sim_apply sim_simple_write_local. solve_res.
intros s ->. simpl.
intros arg ->. simpl.
sim_apply sim_simple_let_val=>/=.
apply sim_simple_place.
(* Retag. *)
sim_apply sim_simple_let_place=>/=.
destruct vs as [|s' vs]; first by inversion FREL.
apply Forall2_cons_inv in FREL as [FREL FTAIL].
destruct vs as [|]; last by inversion FTAIL. clear FTAIL.
destruct args as [|args args']; first by inversion AREL.
apply Forall2_cons_inv in AREL as [AREL ATAIL].
destruct args' as [|]; last by inversion ATAIL. clear ATAIL.
sim_apply sim_simple_retag_local. solve_res. done. solve_res.
move=>l_i tg_i hplt /= Hl_i.
(* Call *)
sim_apply sim_simple_let_val=>/=.
sim_apply (sim_simple_call 10 [] [] ε). constructor. solve_res.
intros rf frs frt FREL.
apply sim_simple_val.
Abort.
......@@ -105,6 +105,18 @@ Proof.
apply HH; done.
Qed.
(* [Val <$> _] in the goal makes this not work with [apply], but
we'd need tactic support for anything better. *)
Lemma sim_simple_call n' vls vlt rv fs ft r r' n fid css cst Φ :
Forall2 (vrel rv) vls vlt
r r' rv
( r' vs vt, vrel r' vs vt
r r' ⊨ˢ{n',fs,ft} (Val vs, css) (Val vt, cst) : Φ)
r ⊨ˢ{n,fs,ft}
(Call #[ScFnPtr fid] (Val <$> vls), css) (Call #[ScFnPtr fid] (Val <$> vlt), cst) : Φ.
Proof.
Admitted.
(** * Memory *)
Lemma sim_simple_alloc_local fs ft r n T css cst Φ :
( (l: loc) (tg: nat),
......
......@@ -93,6 +93,9 @@ Proof. intros ->. rewrite - !assoc. f_equiv. exact: comm. Qed.
Lemma res_search_found_left (F W : resUR) :
W F F W.
Proof. exact: comm. Qed.
Lemma res_search_found_unit (F W : resUR) :
F F ε.
Proof. rewrite right_id //. Qed.
Lemma res_search_singleton (R W : resUR) :
W ε W.
Proof. rewrite left_id //. Qed.
......@@ -100,6 +103,8 @@ Ltac solve_res :=
match goal with
| |- _ _ _ =>
reflexivity
| |- _ _ ε =>
exact: res_search_found_unit
| |- _ _ _ =>
exact: res_search_found_left
| |- _ _ =>
......
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