Module CPP

Require Import LibLists.
Require Import Cplusconcepts.
Require Import Coqlib.
Require Import Tactics.
Require Import CplusWf.
Require Import LibMaps.
Require Import LayoutConstraints.
Require Import LibPos.
Load Param.

A class is dynamic if, and only if, one of the following conditions holds:

it has a virtual method
it has a direct virtual base
it has a direct dynamic base

This definition is common to both algorithms studied in POPL 2011, Section 6. Moreover, it is formalized in the C++ Standard (since 1999) as "to have a polymorphic behaviour". However, it plays no role in the correctness of conditions stated in Section 4 and proved in Section 5.

Section Is_dynamic.

Variable A : ATOM.t.

Section DYN.

Variable hierarchy : PTree.t (Class.t A).

Inductive is_dynamic : ident -> Prop :=
| is_dynamic_virtual_methods : forall i c
  (H_i_c : hierarchy ! i = Some c)
  (H_methods : exists m, In m (Class.methods c) /\ Method.virtual m = true),
    is_dynamic i
| is_dynamic_direct_virtual_base : forall i c
  (H_i_c : hierarchy ! i = Some c)
  b
  (Hb : In (Class.Inheritance.Shared, b) (Class.super c)),
  is_dynamic i
| is_dynamic_base : forall i c
  (H_i_c : hierarchy ! i = Some c)
  h b
  (H_h_b : In (h, b) (Class.super c))
  (H_is_dynamic_b : is_dynamic b),
  is_dynamic i
.

Lemma is_dynamic_virtual_base : forall i b,
  is_virtual_base_of hierarchy b i ->
  is_dynamic i.

Proof.

  induction 1.
  eauto using is_dynamic_direct_virtual_base.
  eauto using is_dynamic_base.
Qed.

Lemma is_dynamic_path : forall to via from by
  (Hpath : path hierarchy to via from by)
  (H_dyn_to : is_dynamic to),
  is_dynamic from.

Proof.

  intros.
  generalize (path_path2 Hpath).
  clear Hpath.
  intro Hpath.
  revert H_dyn_to.
  induction Hpath ; intros ; eauto 10 using is_dynamic_base.
Qed.

Hypothesis hierarchy_wf : Well_formed_hierarchy.prop hierarchy.

Lemma is_dynamic_dec : forall i, {is_dynamic i} + {~ is_dynamic i}.

Proof.

induction i using (well_founded_induction Plt_wf).
rename H into IHi.
case_eq (hierarchy ! i).
  intros c Hc.
  case_eq (List.filter (Method.virtual (A := A)) (Class.methods c)).
   intros H_no_methods.
   pose (f := (fun (x : _ * ident) => match x with (Class.Inheritance.Shared, _) => true | _ => false end)).
   case_eq (List.filter f (Class.super c)).
    intros H_no_direct_virtual_bases.
    generalize (Well_formed_hierarchy.well_founded hierarchy_wf Hc).
    intros Hlt.
    generalize (fun (hc : _ * _) Hc =>
      match hc as hc' return In hc' (Class.super c) -> Plt (let (_, cisuper) := hc' in cisuper) _ with
        | pair h cisuper => fun Hin => Hlt h cisuper Hin
      end Hc
    ).
    intro Hlt'.
    generalize (tag_list Hlt').
    intros [l' Hl'].
    pose (g := fun (x : sigT (fun hc : (Class.Inheritance.t * _) => Plt (let (h, cisuper) := hc in cisuper) i)) =>
      match x with
        | existT hc hlt =>
          match hc as hc' return (Plt (let (_, cisuper) := hc' in cisuper) i -> bool) with
            | (h, cisuper) => fun hlt' => if IHi cisuper hlt' then true else false
          end hlt
      end
    ).
    case_eq (filter g l').

     intro H_no_dynamic_bases.
     right.
     intro Habs.
     inversion Habs ; try congruence.
      subst i0.
      destruct H_methods.
      destruct H.
      generalize (filter_In (Method.virtual (A := A)) x (Class.methods c)).
      rewrite H_no_methods.
      simpl.
      replace c0 with c in * by congruence.
      tauto.
      subst i0.
      replace c0 with c in * by congruence.
      generalize (filter_In f (Class.Inheritance.Shared, b) (Class.super c)).
      intros [_ Hin].
      simpl in Hin.
      generalize (Hin (conj Hb (refl_equal _))).
      rewrite H_no_direct_virtual_bases.
      tauto.
     subst i0.
     replace c0 with c in * by congruence.
     generalize (Hl' (h, b)).
     intros [Hin_l' _].
     generalize (Hin_l' H_h_b).
     intros [p Hp].
     assert (g (existT _ (h, b) p) = true) as Hg.
      simpl.
      destruct (IHi b p).
       trivial.
       contradiction.
      generalize (filter_In g (existT _ (h, b) p) l').
      intros [_ Hin].
      generalize (Hin (conj Hp Hg)).
      rewrite H_no_dynamic_bases.
      tauto.

     intros s l Hs.
     assert (In s (filter g l')) as Hin_g.
      rewrite Hs.
      simpl. tauto.
     generalize (filter_In g s l').
     intros [Hin_g_l' _].
     generalize (Hin_g_l' Hin_g).
     intros [Hin_l' Hg].
     destruct s as [h p].
     generalize (Hl' h).
     intros [_ Hin_super].
     generalize (Hin_super (ex_intro _ p Hin_l')).
     intros.
     destruct h.
     simpl in Hg.
     left.
      eapply is_dynamic_base.
      eassumption.
      eassumption.
      destruct (IHi p0 p).
      assumption.
      congruence.

    intros h l Hh.
    assert (In h (filter f (Class.super c))) as Hin_f.
     rewrite Hh.
     simpl. tauto.
    generalize (filter_In f h (Class.super c)).
    intros [Hin_h _].
    generalize (Hin_h Hin_f).
    intros [? Hf].
    destruct h as [t ?].
    simpl in Hf.
    destruct t ; try congruence.
    left.
    eapply is_dynamic_direct_virtual_base.
    eassumption.
    eassumption.

  intros.
  left.
  eapply is_dynamic_virtual_methods.
  eassumption.
  exists t.
  generalize (filter_In (Method.virtual (A := A)) t (Class.methods c)).
  rewrite H.
  simpl.
  tauto.

  intros.
  right.
  intro Habs.
  inversion Habs ; congruence.

Qed.

End DYN.

Record CPPOPTIM : Type := CppOptim {
is_empty : PTree.t (Class.t A) -> ident -> Prop;
is_empty_prop : forall hierarchy, Is_empty.prop hierarchy (is_empty hierarchy);

4.3

dynamic_nonempty : forall hierarchy id, is_dynamic hierarchy id -> is_empty hierarchy id -> False
}.

Section Optim.

Variable C : CPPOPTIM.

Definition Optim := Optim (is_empty_prop C) (dynamic_nonempty (c := C)).

End Optim.

End Is_dynamic.