Definition stateC : Type := list Clo*list Clo.
Hint Transparent stateC.
Reserved Notation "σ ≻C_ l σ'" (at level 70, l at level 0,format "σ '≻C_' l σ'").
Inductive stepC : label -> stateC -> stateC -> Prop:=
| step_nil E T V:
(retT/E::T,V) ≻C_τ (T,V)
| step_load P E x V p T:
E.[x] = Some p ->
((varT x P)/E::T,V) ≻C_τ (P/E::T,p::V)
| step_pushVal P Q E T V:
((lamT Q P)/E ::T,V) ≻C_τ (P/E::T,Q/E::V)
| step_betaC P E T e Q F V:
((appT P)/E :: T,e :: Q/F ::V) ≻C_β (Q/(e::F) :: P/E :: T,V)
where "σ ≻C_ l σ'" := (stepC l σ σ').
Notation "(≻C_ l )" := (stepC l) (at level 0, format "'(≻C_' l ')'").
(* workaround to prefere "x ≻ y" over "(≻) x y"*) Notation "σ ≻C_ l σ'" := 0.
Notation "σ ≻C_ l σ'" := (stepC l σ σ').
Notation "(≻C)" := (any stepC) (at level 0).
Notation "σ ≻C σ'" := (any stepC σ σ') (at level 70).
Canonical Structure clos_machine := {| M_rel := stepC |}.
Hint Constructors stepC.
Definition closedSC : stateC -> Prop :=
fun '(T,V) => Forall (<C 0) T /\ Forall (<C 1) V.
Definition repsCS (π:stateC) (σ:stateS) : Prop :=
let '(T,V):= π in closedSC (T,V) /\ (map (δC 0) T,map (δC 1) V) = σ.
Notation "(≫CS)" := (repsCS) (at level 0).
Notation "π ≫CS σ" := (repsCS π σ) (at level 70).
Lemma repsCS_functional :
functional (≫CS).
Proof.
intros [] ? ? [? <-] [? <-]. tauto.
Qed.
Local Lemma cbound_cons P e E :
P/E <C 1 -> e <C 1 -> P/(e::E) <C 0.
Proof.
inversion 1. constructor;cbn;intuition (subst;eauto).
Qed.
Lemma reducibility T V:
reducible (≻S) (map (δC 0) T,map (δC 1) V) -> reducible (≻C) (T,V).
Proof.
intros (σ'&l'&R). unfold reducible.
destruct T as [|[[] E]];cbn in R.
-now inv R.
-eauto.
-cbn in R. destruct _ eqn:eq. 2:now inv R.
rewrite <-minus_n_O in eq. apply nth_error_map in eq as (?&?&?). eauto.
-destruct V as [|? [|[]]]. 3:eauto.
all:cbn in R. all:inv R.
-eauto.
Qed.
Ltac inv_closed_clos :=
repeat
match goal with
| [H:closedSC (_,_) |- _] => inv H
| [H:Forall _ (_::_) |- _] => inv H
| [H:_/_ <C _|- _] => inv H
| [H:lamT _ _ <P _ |- _] => inv H
| [H:varT _ _<P _ |- _] => inv H
| [H:appT _<P _ |- _] => inv H
end.
Lemma closedSC_preserved T V T' V' :
closedSC (T,V) -> (T,V) ≻C (T',V') -> closedSC (T',V').
Proof.
intros ? [l R]. inv R.
all:inv_closed_clos.
all:split;repeat apply Forall_cons.
all:eauto using nth_error_In, cbound_cons.
Qed.
Lemma tau_simulation T V T' V':
(T,V) ≻C_τ (T',V') -> (map (δC 0) T,map (δC 1) V) ≻S_τ (map (δC 0) T',map (δC 1) V').
Proof.
intros H. inv H. all:cbn.
2:erewrite <-minus_n_O, map_nth_error.
all:eauto.
Qed.
Lemma beta_simulation T V T' V':
closedSC (T,V) -> (T,V) ≻C_β (T',V') -> (map (δC 0) T,map (δC 1) V) ≻S_β (map (δC 0) T',map (δC 1) V').
Proof.
intros cs H. inv H. cbn.
rewrite substPl_cons.
-constructor.
-inv_closed_clos. eapply Forall_map,Forall_forall. auto using translateC_boundP.
Qed.
Lemma clos_stack_refinement :
refinement_M (≫CS).
Proof.
split;cbn.
-intros [] [] [? [= <- <-]]. apply reducibility.
-split.
all:unfold repsCS.
all:intros [T V] [T' V'] [T0 V0] [cs [= <- <-]] ?.
all:specialize closedSC_preserved with (1:=cs) as ?.
all:eauto 20 using tau_simulation,beta_simulation.
Qed.
Lemma compile_clos_stack P:
closedP P ->
([P/[]],[]) ≫CS ([P],[]).
Proof.
intros cs. split.
-unfold closedSC. eauto.
-cbn. now rewrite substPl_nil.
Qed.
Definition repsCL:= rcomp repsCS repsSL.
Notation "(≫CL)" := (repsCL) (at level 0).
Notation "π ≫CL s" := (repsCL π s) (at level 70).
(*
Lemma repsCL_equiv T V s:
(T,V) ≫CL s <-> closedL s /\ exists A, δV (map (δC 1) V) = Some A /\ δT (map (δC 0) T) A = Some s.
Proof.
unfold repsCL,repsCS,repsSL. split.
-intros (?&? <-&(A&?&?)). split. 2:eauto. admit.
-intros (?&(A&?&?)). eexists;split. split. 2:reflexivity. 2:now cbn;eauto. admit.
Abort. *)
Lemma clos_L_refinement :
refinement_ARS (≫CL).
Proof.
apply (composition clos_stack_refinement stack_L_refinement).
Qed.
Lemma compile_clos_L s:
closedL s ->
([γ s retT/[]],[]) ≫CL s.
Proof.
intros ?. eexists;split.
-apply compile_clos_stack. eauto using bound_compile.
-apply compile_stack_L.
Qed.