Require Import LibLists.
Require Export Cplusconcepts.
Require Import Coqlib.
Require Import LibMaps.
Load Param.



Module Well_formed_hierarchy.
  Section HH.
    Variable A : ATOM.t.
    Variable hierarchy : PTree.t (Class.t A).

    Record prop : Prop := intro {
      well_founded : forall ci c,
        PTree.get ci hierarchy = Some c ->
        forall h cisuper, In (h, cisuper) (Class.super c) ->
          Plt cisuper ci
          ;
      well_founded_struct : forall ci c,
        PTree.get ci hierarchy = Some c ->
        forall fi, In fi (Class.fields c) ->
          forall cl z,
            FieldSignature.type fi = FieldSignature.Struct cl z ->
            Plt cl ci
            ;
      complete : forall ci c,
        PTree.get ci hierarchy = Some c ->
        forall h cisuper, In (h, cisuper) (Class.super c) ->
          PTree.get cisuper hierarchy <> None
          ;
      complete_struct : forall ci c,
        PTree.get ci hierarchy = Some c ->
        forall fi, In fi (Class.fields c) ->
          forall cl z, FieldSignature.type fi = FieldSignature.Struct cl z ->
            hierarchy ! cl <> None
            ;
      bases_no_dup : forall ci c,
        PTree.get ci hierarchy = Some c ->
        NoDup (Class.super c)
        ;
      fields_no_dup : forall ci c,
        PTree.get ci hierarchy = Some c ->
        NoDup (Class.fields c)
    }.

    Hint Resolve well_founded complete.

    Hypothesis hyp : prop.

Well-foundedness properties

    
    Lemma is_virtual_base_of_defined_base :
      forall vb ci,
        is_virtual_base_of hierarchy vb ci ->
        hierarchy ! vb <> None.

    Lemma is_virtual_base_of_lt :
      forall vb ci,
        is_virtual_base_of hierarchy vb ci ->
        Plt vb ci.

    Corollary no_self_virtual_base :
      forall ci, ~ is_virtual_base_of hierarchy ci ci.

    Lemma is_valid_repeated_subobject_le :
      forall l a l',
        l = a :: l' ->
        forall z, Cplusconcepts.last l = Some z ->
          is_valid_repeated_subobject hierarchy l = true ->
          Ple z a.

    Corollary path_le :
      forall to k from p,
        path hierarchy to k from p ->
        Ple to from.

   Lemma self_path_trivial : forall from k p,
     path hierarchy from p from k ->
     (k, p) = (Class.Inheritance.Repeated, from :: nil).
     

Lemma categorize_paths :
  forall to via from,
  forall kind, path hierarchy to via from kind ->
  forall h q, via = h :: q ->
    (h = from <-> kind = Class.Inheritance.Repeated).

Corollary path_eq_hierarchy_eq : forall p h1 from to1,
  path hierarchy to1 p from h1 ->
  forall to2 h2, path hierarchy to2 p from h2 ->
    h1 = h2.

Lemma is_valid_repeated_subobject_sorted : forall l,
  is_valid_repeated_subobject hierarchy l = true ->
  LibLists.sorted (fun a b => Plt b a) l.
 
Lemma array_path_le : forall via to to_n from from_n,
  valid_array_path hierarchy to to_n from from_n via ->
  Ple to from.

Construction of the list of (direct or indirect) virtual bases

 
Function primary_virtual_bases (l : list (Class.Inheritance.t * ident)) : list ident :=
match l with
  | nil => nil
  | (Class.Inheritance.Shared, ci) :: q =>
    ci :: primary_virtual_bases q
  | _ :: q => primary_virtual_bases q
end.


Lemma primary_virtual_bases_correct : forall b l,
  In b (primary_virtual_bases l) -> In (Class.Inheritance.Shared, b) l.

Lemma primary_virtual_bases_complete : forall l b,
  In (Class.Inheritance.Shared, b) l -> In b (primary_virtual_bases l).

Lemma virtual_bases_step : forall n t,
  (forall i, Plt i n -> t ! i <> None) ->
  (forall i l, t ! i = Some l -> forall j, In j l <-> is_virtual_base_of hierarchy j i) ->
  {l : _ & forall j, In j l <-> is_virtual_base_of hierarchy j n}.

Theorem virtual_bases :
  {t |
    (forall cn,
      hierarchy ! cn <> None -> t ! cn <> None) /\
    forall cn l, t ! cn = Some l ->
      forall i, (In i l <-> is_virtual_base_of hierarchy i cn)
  }.

Construction of the list of all paths reachable from classes

Section Path_to.

Variable to : ident.

Lemma path_to_step : forall n t, (forall i, Plt i n -> t ! i <> None) ->
  (forall i l, t ! i = Some l -> forall kp : _ * _, In kp l <-> let (k, p) := kp in path hierarchy to p i k) ->
  {l : _ & forall kp : _ * _, In kp l <-> let (k, p) := kp in path hierarchy to p n k}.

Theorem path_to :
  {t |
    (forall cn,
      hierarchy ! cn <> None -> t ! cn <> None) /\
    forall cn l, t ! cn = Some l ->
      forall i : _ * _, (In i l <-> let (k, p) := i in path hierarchy to p cn k)
  }.

End Path_to.

Theorem paths :
  {T | (forall cn0,
    hierarchy ! cn0 <> None -> T ! cn0 <> None) /\
    forall cn0 t, T ! cn0 = Some t ->
      (forall cn,
        hierarchy ! cn <> None -> t ! cn <> None) /\
      forall cn l, t ! cn = Some l ->
        forall i : _ * _, (In i l <-> let (k, p) := i in path hierarchy cn0 p cn k)
  }.


Lemma path_eq_dec : forall kp1 kp2 : Class.Inheritance.t * list ident,
  {kp1 = kp2} + {kp1 <> kp2}.

Dynamic cast

Lemma dynamic_cast_unique : forall real rk rp from to k1 p1,
  dynamic_cast hierarchy real rk rp from to k1 p1 ->
  forall k2 p2,
    dynamic_cast hierarchy real rk rp from to k2 p2 ->
    (k1, p1) = (k2, p2)
.


Lemma dynamic_cast_dec : forall real real_inheritance real_path from cast,
  {cast_inheritance : _ & {cast_path | dynamic_cast hierarchy real real_inheritance real_path from cast cast_inheritance cast_path}} +
  {forall cast_inheritance cast_path, dynamic_cast hierarchy real real_inheritance real_path from cast cast_inheritance cast_path -> False}.



Function non_virtual_bases (l : list (Class.Inheritance.t * ident)) : list ident :=
match l with
  | nil => nil
  | (Class.Inheritance.Repeated, ci) :: q =>
    ci :: non_virtual_bases q
  | _ :: q => non_virtual_bases q
end.

Lemma non_virtual_bases_correct : forall l b,
  In b (non_virtual_bases l) -> In (Class.Inheritance.Repeated, b) l.

Lemma non_virtual_bases_complete : forall l b,
  In (Class.Inheritance.Repeated, b) l -> In b (non_virtual_bases l).



Section Filtered_paths.

Variable P : ident -> Prop.

Hypothesis P_dec : forall i, {P i} + {~ P i}.

  Lemma filtered_repeated_paths_step : forall n t, (forall i, Plt i n -> t ! i <> None) ->
    (forall i l, t ! i = Some l -> (forall p, In p l <->
      exists l', p = i :: l' /\ is_valid_repeated_subobject hierarchy p = true /\
        forall j, Cplusconcepts.last p = Some j -> P j)) ->
  {l : _ & (forall p, In p l <->
      exists l', p = n :: l' /\ is_valid_repeated_subobject hierarchy p = true /\
        forall j, Cplusconcepts.last p = Some j -> P j)
}.

Theorem filtered_paths_aux :
  {t |
    (forall cn,
      hierarchy ! cn <> None -> t ! cn <> None) /\
    forall cn l, t ! cn = Some l ->
      forall i, (In i l <->
        exists i', i = cn :: i' /\
          is_valid_repeated_subobject hierarchy i = true /\
          forall j, Cplusconcepts.last i = Some j -> P j
)
  } ->
  forall from,
    {l |
      forall k p,
        (In (k, p) l <->
          exists to,
            path hierarchy to p from k /\
            P to
        )
    }
    .

Lemma filtered_repeated_paths :
  {t |
    (forall cn,
      hierarchy ! cn <> None -> t ! cn <> None) /\
    forall cn l, t ! cn = Some l ->
      forall i, (In i l <->
        exists i', i = cn :: i' /\
          is_valid_repeated_subobject hierarchy i = true /\
          forall j, Cplusconcepts.last i = Some j -> P j
)
  }.

Theorem filtered_paths :
  {t |
    (forall cn,
      hierarchy ! cn <> None -> t ! cn <> None) /\
    forall from l, t ! from = Some l ->
      forall k p,
        (In (k, p) l <->
          exists to,
            path hierarchy to p from k /\
            P to
        )
  }
  .

End Filtered_paths.
  

Domination

   Lemma dominates_antisym : forall from kp1 kp2,
     dominates hierarchy from kp1 kp2 ->
     dominates hierarchy from kp2 kp1 ->
     kp1 = kp2.


Lemma dominates_dec_aux_accu : forall kp1 kp2 l accu,
  (forall kp, In kp (rev accu) -> kp2 <> concat kp1 kp) ->
  {kp | In kp (rev accu ++ l) /\ kp2 = concat kp1 kp} +
  {forall kp, In kp (rev accu ++ l) -> kp2 <> concat kp1 kp}.

Corollary dominates_dec_aux : forall kp1 kp2 l,
  {kp | In kp (l) /\ kp2 = concat kp1 kp} +
  {forall kp, In kp (l) -> kp2 <> concat kp1 kp}.

Theorem dominates_dec : forall from kp1 kp2,
  {dominates hierarchy from kp1 kp2} + {~ dominates hierarchy from kp1 kp2}.

Method dispatch

Theorem method_dispatch_dominates : forall ms ac1 rc rck1 rcp1 rk1 rp1,
  method_dispatch hierarchy ms ac1 rc rck1 rcp1 rk1 rp1 ->
  forall ac2 k12 p12,
    path hierarchy ac2 p12 ac1 k12 ->
    forall ak2 ap2 am2,
      path hierarchy am2 ap2 ac2 ak2 ->
      forall amc2,
        hierarchy ! am2 = Some amc2 ->
        Method.find ms (Class.methods amc2) <> None ->
        (forall to k p,
          path hierarchy to p ac2 k ->
          forall c, hierarchy ! to = Some c ->
            Method.find ms (Class.methods c) <> None ->
            dominates hierarchy ac2 (ak2, ap2) (k, p)
        ) ->
        forall rck2 rcp2,
          (rck2, rcp2) = concat (rck1, rcp1) (k12, p12) ->
          method_dispatch hierarchy ms ac2 rc rck2 rcp2 rk1 rp1
        .


Theorem method_dispatch_list : forall
 (ms : MethodSignature.t A) (apparent_class : ident) (real_class : ident) (real_class_inheritance : Class.Inheritance.t) (real_class_path : list ident) ,
 { l | forall (real_inheritance: Class.Inheritance.t) (real_path : list ident),
   In (real_inheritance, real_path) l <->
   method_dispatch hierarchy ms apparent_class real_class real_class_inheritance real_class_path real_inheritance real_path }.



End HH.

  End Well_formed_hierarchy.