Lvc.LivenessValidators

Require Import DecSolve IL Annotation Liveness TrueLiveness LengthEq.

Instance argsLive_dec Caller Callee Y Z
      : Computable (argsLive Caller Callee Y Z).
Proof.
  decide(length Y = length Z).
  - general induction Y; destruct Z; isabsurd.
    + left; econstructor.
    + decide (v ∈ Callee → live_exp_sound a Caller);
      edestruct (IHY Caller Callee); try dec_solve; try eassumption;
      try inv an; eauto; try tauto.
  - right; intro. eapply argsLive_length in H. congruence.
Defined.

Definition live_sound_dec i Lv s slv (an:annotation s slv)
      : Computable (live_sound i Lv s slv).
Proof.
  general induction s; destruct slv; try isabsurd.
  + edestruct IHs; eauto; try inv an; eauto;
    decide (getAnn slv\{{x}} ⊆ a);
    decide (live_exp_sound e a);
    decide (x ∈ getAnn slv);
    try dec_solve.
  + edestruct IHs1; try inv an; eauto;
    edestruct IHs2; try inv an; eauto;
    decide (live_exp_sound e a);
    decide (getAnn slv1 ⊆ a);
    decide (getAnn slv2 ⊆ a);
    try dec_solve; try eassumption; try inv an; eauto.
  + destruct (get_dec Lv (counted l)) as [[[blv Z] ?]|?];
    (try (decide (isImperative i); [decide ((blv \ of_list Z) ⊆ a)|]));
    try decide (∀ n y, get Y n y → live_exp_sound y a);
    try decide (length Y = length Z); try dec_solve.
    - left; econstructor; eauto. destruct if; eauto.
    - right; intro. inv H; eauto. destruct if in H5; eauto.
      get_functional; subst. eauto.
    - left; econstructor; eauto. destruct if; eauto. intuition.
  + decide(live_exp_sound e a); try dec_solve.
  + edestruct IHs; eauto; try inv an; eauto;
    decide (getAnn slv \ {{x}} ⊆ a);
    decide (x ∈ getAnn slv);
    try decide (∀ n y, get Y n y → live_exp_sound y a);
    try dec_solve.
  + edestruct IHs1; eauto; try inv an; eauto;
    edestruct IHs2; eauto; try inv an; eauto;
    decide ((of_list Z) ⊆ getAnn slv1);
    decide (getAnn slv2 ⊆ a); try dec_solve.
    decide (isFunctional i).
    decide ((getAnn slv1 \ of_list Z) ⊆ a).
    - left; econstructor; eauto. destruct if; eauto.
    - right; intro. inv H; eauto. destruct if in H10; eauto.
    - left; econstructor; eauto. destruct if; eauto. intuition.
    Grab Existential Variables. eassumption. eassumption. eassumption. eassumption.
Defined.

Instance live_sound_dec_inst i Lv s slv `{Computable(annotation s slv)}
: Computable (live_sound i Lv s slv).
Proof.
  edestruct H.
  eapply live_sound_dec; eauto.
  right; intro. eauto using live_sound_annotation.
Defined.

Definition true_live_sound_dec i Lv s slv (an:annotation s slv)
      : Computable (true_live_sound i Lv s slv).
Proof.
  general induction s; destruct slv; try isabsurd.
  + edestruct IHs; eauto; try inv an; eauto;
    decide (getAnn slv\{{x}} ⊆ a);
    decide (x ∈ getAnn slv → live_exp_sound e a);
    decide (x ∉ getAnn slv → a ⊆ getAnn slv\{{x}});
    try dec_solve.
  + edestruct IHs1; try inv an; eauto;
    edestruct IHs2; try inv an; eauto;
    decide (exp2bool e = None → live_exp_sound e a);
    decide (exp2bool e ≠ Some false → getAnn slv1 ⊆ a);
    decide (exp2bool e ≠ Some true → getAnn slv2 ⊆ a);
    try dec_solve; try eassumption; try inv an; eauto.
  + destruct (get_dec Lv (counted l)) as [[[blv Z] ?]|?];
    try decide (argsLive a blv Y Z); try dec_solve.
    exploit argsLive_length; eauto.
    decide (isImperative i); try dec_solve.
    decide ((blv \ of_list Z) ⊆ a).
    - left; econstructor; eauto. destruct if; eauto.
    - right; intro. inv H; eauto. destruct if in H5; eauto.
      get_functional; subst; eauto.
    - left; econstructor; eauto. destruct if; eauto. intuition.
  + decide(live_exp_sound e a); try dec_solve.
  + edestruct IHs; eauto; try inv an; eauto;
    decide (getAnn slv \ {{x}} ⊆ a);
    try decide (∀ n y, get Y n y → live_exp_sound y a);
    try dec_solve.
  + edestruct IHs1; eauto; try inv an; eauto;
    edestruct IHs2; eauto; try inv an; eauto;
    decide (getAnn slv2 ⊆ a); try dec_solve.
    decide (isFunctional i).
    decide ((getAnn slv1 \ of_list Z) ⊆ a).
    - left; econstructor; eauto. destruct if; eauto.
    - right; intro. inv H; eauto. destruct if in H10; eauto.
    - left; econstructor; eauto. destruct if; eauto. intuition.
    Grab Existential Variables. eassumption. eassumption. eassumption. eassumption.
Defined.

Instance true_live_sound_dec_inst i Lv s slv `{Computable(annotation s slv)}
: Computable (true_live_sound i Lv s slv).
Proof.
  edestruct H.
  eapply true_live_sound_dec; eauto.
  right; intro. eauto using true_live_sound_annotation.
Defined.