Commit 3b27342f authored by Hai Dang's avatar Hai Dang
Browse files

make return case also need to deal with the index

parent cddc8877
......@@ -34,10 +34,11 @@ Record sim_base (sim: SIM_CONFIG) (idx1: nat) (eσ1_src eσ1_tgt: expr * state)
: Prop := mkSimBase {
(* (1) If [eσ1_tgt] gets stuck, [eσ1_src] can also get stuck. *)
sim_stuck :
~ stuck (Λ:= bor_lang fnt) eσ1_tgt.1 eσ1_tgt.2 ;
(terminal eσ1_tgt.1 reducible (Λ:= bor_lang fnt) eσ1_tgt.1 eσ1_tgt.2) ;
(* (2) If [eσ1_tgt] is terminal, then [eσ1_src] terminates with some steps. *)
sim_terminal :
terminal eσ1_tgt.1 eσ2_src, eσ1_src ~{fns}~>* eσ2_src
terminal eσ1_tgt.1 idx2 eσ2_src,
(eσ1_src ~{fns}~>+ eσ2_src ((idx2 < idx1)%nat eσ1_src = eσ2_src))
terminal eσ2_src.1 sim_expr_terminal eσ2_src.1 eσ1_tgt.1 ;
(* (3) If [eσ1_tgt] steps to [eσ2_tgt] with 1 step,
then exists [eσ2_src] s.t. [eσ1_src] steps to [eσ2_src] with * step. *)
......
......@@ -57,7 +57,7 @@ Proof.
{ admit. (* WF *) }
{ admit. (* WF *) }
clear SIM. intro SIM. inv SIM.
exploit sim_step; eauto. i. des.
exploit sim_step; eauto. i. revert sim_stuck. des.
+ inv x0; ss.
rename eσ2_src into conf'_src.
exploit IHTAU; eauto.
......@@ -73,14 +73,17 @@ Proof.
{ admit. (* WF *) }
{ admit. (* WF *) }
clear SIM. intro SIM. inv SIM. inv MAT.
+ exfalso. eapply sim_stuck; eauto.
apply stuck_terminal. ss.
+ exploit sim_terminal; eauto. i. des.
pfold. econs; eauto.
econs 2. rename x2 into SE. by apply SE.
+ pclearbot. exploit sim_step; eauto. i. des.
+ exfalso. destruct sim_stuck as [[v TE]|ST].
* by apply (NT v).
* admit.
+ exploit sim_terminal; eauto. i. revert sim_stuck. intros _. pfold. des.
* econs; eauto. etrans. apply tc_rtc; eauto.
rename x2 into SE.
admit.
* econs; eauto. admit.
+ pclearbot. exploit sim_step; eauto. i. revert sim_stuck. des.
* inv x1; ss.
exploit CIH; eauto. i.
exploit CIH; eauto. intros ?.
apply tc_inv_l in x0. des.
pfold. econs; eauto.
* inv x1; ss. exploit IH; eauto.
......
......@@ -69,7 +69,7 @@ Inductive _sim_local_body_step (r_f : A) (sim_local_body : SIM)
Record sim_local_body_base (r_f: A) (sim_local_body : SIM)
(r: A) (idx: nat) es σs et σt Φ : Prop := {
sim_local_body_stuck :
~ stuck (Λ:= bor_lang fnt) et σt ;
(terminal et reducible (Λ:= bor_lang fnt) et σt) ;
sim_local_body_terminal :
(* if tgt is terminal *)
vt (TERM: to_result et = Some vt),
......
......@@ -107,17 +107,19 @@ Proof.
pfold. ii. inv SIM. punfold LOCAL. exploit LOCAL; eauto.
{ admit. (* never_stuck *) }
clear LOCAL. intro LOCAL. inv LOCAL. econs.
- ii. eapply sim_local_body_stuck. admit. (* stuck_fill_rev *)
- s. i. subst. apply fill_result in H. des. unfold terminal in H. des. subst. ss.
exploit sim_local_body_terminal; eauto. i. des.
- ii. admit. (* stuck_fill_rev *)
- s. i. subst. apply fill_result in H. revert sim_local_body_stuck. des.
unfold terminal in H. des. subst. ss.
exploit sim_local_body_terminal; eauto. intros ?. des.
clear NEVER_STUCK WSAT.
clear sim_local_body_stuck sim_local_body_terminal sim_local_body_step.
clear sim_local_body_terminal sim_local_body_step. intros _.
assert (VS': to_result vs' = Some x) by admit.
induction FRAMES; ss.
{ esplits; eauto; ss. ii. clarify. }
admit. (* global sim should have generalized index *)
admit.
- i. destruct eσ2_tgt as [e2_tgt σ2_tgt].
exploit fill_step_rev; eauto. i. des; cycle 1.
exploit fill_step_rev; eauto. i. revert sim_local_body_stuck. des; cycle 1.
{ (* return *)
admit. (* similar to the above case *)
}
......@@ -125,7 +127,7 @@ Proof.
+ (* step *)
exploit STEP; eauto. intros (es' & σs' & r' & idx' & STEP' & WSAT' & SIM').
pclearbot. esplits; eauto.
* instantiate (1 := (fill K_src0 es', σs')).
* instantiate (1 := (fill K_src0 es', σs')). revert sim_local_body_stuck.
des; [left|right]; esplits; eauto.
{ apply fill_stepp. ss. }
{ inv STEP'0. ss. }
......@@ -139,7 +141,7 @@ Proof.
}
* right. apply CIH. econs.
{ econs 2; eauto. i. instantiate (1 := mk_frame _ _ _). ss.
destruct (CONT _ _ _ _ _ WSAT' VRET).
destruct (CONT _ _ _ σ_src' σ_tgt' VRET).
pclearbot. esplits; eauto.
}
{ admit. (* sim_local_body for the call init *) }
......
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