Commit c9fd6128 authored by Ralf Jung's avatar Ralf Jung

free some things

parent f6a84ee7
......@@ -12,8 +12,9 @@ Definition ex1_unopt : function :=
Call #[ScFnPtr "f"] [] ;;
*{int} "x" <- #[42] ;;
Call #[ScFnPtr "g"] [] ;;
Copy *{int} "x"
(* FIXME: should deallocate `x` *)
let: "v" := Copy *{int} "x" in
Free "x" ;; Free "i" ;;
"v"
.
Definition ex1_opt : function :=
......@@ -24,7 +25,7 @@ Definition ex1_opt : function :=
*{int} "x" <- #[42] ;;
let: "v" := Copy *{int} "x" in
Call #[ScFnPtr "g"] [] ;;
(* FIXME: should deallocate `x` *)
Free "x" ;; Free "i" ;;
"v"
.
......@@ -74,7 +75,7 @@ Proof.
apply: sim_body_result=>_. simpl.
apply: sim_body_let_r. simpl. (* FIXME: figure out why [sim_apply_r] does the wrong thing here *)
(* We can go back to simple mode! *)
eapply sim_simplify. { by eauto. }
eapply (sim_simplify (fun_post_simple c)). { by eauto. }
simplify_eq/=. clear- AREL FREL LOOK.
(* Call *)
sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|].
......@@ -89,13 +90,21 @@ Proof.
sim_apply_l sim_body_deref_l. simpl.
sim_apply_l sim_body_copy_unique_l; [try solve_sim..|].
{ rewrite lookup_insert. done. }
apply: sim_body_result=>Hval. simpl.
apply: sim_body_let_l. simpl.
(* Free stuff *)
eapply (sim_simplify (fun_post_simple c)). { by eauto. }
sim_apply sim_simple_free; [try solve_sim..|]. admit. simpl.
sim_apply sim_simple_let=>/=.
sim_apply sim_simple_free; [try solve_sim..|]. admit. simpl.
sim_apply sim_simple_let=>/=.
(* Finishing up. *)
(* eapply sim_body_viewshift.
{ do 5 eapply viewshift_frame_r. eapply vs_call_empty_public. } *)
apply: sim_body_result=>Hval. do 2 (split; first done). split.
apply: sim_simple_result. split.
- solve_res.
- constructor; simpl; auto.
Qed.
Admitted.
(** Top-level theorem: Two programs that only differ in the
"ex1" function are related. *)
......
......@@ -290,9 +290,15 @@ Proof using Type*.
sim_bind (subst_map _ e) (subst_map _ e).
eapply sim_simple_post_mono, IHe; [|by auto..].
intros r' n' rs rt (-> & Hrel). simpl.
eapply sim_simple_dealloc; eauto.
apply: sim_simple_free; eauto.
split; first done. constructor; done.
- (* Retag *)
move=>Hwf xs Hxswf /=.
sim_bind (subst_map _ e) (subst_map _ e).
eapply sim_simple_post_mono, IHe; [|by auto..].
intros r' n' rs rt (-> & Hrel). simpl.
eapply sim_simple_retag_public; eauto.
split; first done. constructor; done.
- (* Retag *) admit.
- (* Let *)
move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
eapply sim_simple_frame_core.
......@@ -319,7 +325,7 @@ Proof using Type*.
eapply (Forall_lookup_1 _ _ _ _ H Hlk).
+ eapply (Forall_lookup_1 _ _ _ _ Hwf2 Hlk).
+ eauto.
Admitted.
Qed.
End sem.
......
......@@ -341,12 +341,13 @@ Proof.
intros HH σs σt. apply sim_body_alloc_public=>/=; eauto.
Qed.
Lemma sim_simple_dealloc fs ft r rs rt n Φ :
Lemma sim_simple_free fs ft r es rs et rt n Φ :
IntoResult es rs IntoResult et rt
rrel r rs rt
Φ r n (ValR [%S]) (ValR [%S])
r ⊨ˢ{n,fs,ft} Free rs Free rt : Φ.
r ⊨ˢ{n,fs,ft} Free es Free et : Φ.
Proof.
intros [Hrel <-]%rrel_with_eq HH σs σt. eapply sim_body_free; eauto.
intros <- <- [Hrel <-]%rrel_with_eq HH σs σt. eapply sim_body_free; eauto.
Qed.
Lemma sim_simple_write_public fs ft r n (rs1 rs2 rt1 rt2: result) Φ :
......@@ -377,7 +378,7 @@ Lemma sim_simple_retag_public fs ft r n (rs rt: result) k Φ :
r ⊨ˢ{n,fs,ft} Retag rs k Retag rt k : Φ.
Proof.
intros [Hrel ?]%rrel_with_eq. simplify_eq.
Abort.
Admitted.
(** * Pure *)
Lemma sim_simple_let fs ft r n x (vs1 vt1: result) es1 et1 es2 et2 Φ :
......
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