Module IntermSetDynType

Require Import Coqlib.
Require Import Cplusconcepts.
Require Import LibLists.
Require Import Tactics.
Require Import LibMaps.
Load Param.
Open Scope Z_scope.


Notation var := (ident) (only parsing).


Section Set_dynamic_type.

Variable A : ATOM.t .

Definition list_dynamic_type := (list ((positive * (array_path A * Z * (Class.Inheritance.t * list ident))) * ((Class.Inheritance.t * list ident) * (Class.Inheritance.t * list ident)))).

Variable hierarchy : PTree.t (Class.t A).
Variable obj : positive.
Variable ar : array_path A.
Variable i : Z.

Variable h0 : Class.Inheritance.t.
Variable p0 : list ident.

Inductive set_dynamic_type_non_virtual_aux : Class.Inheritance.t -> list ident -> list ident -> list_dynamic_type -> list_dynamic_type -> Prop :=
| set_dynamic_type_non_virtual_aux_nil : forall h p h' p',
  (h', p') = concat (h0, p0) (h, p) ->
  forall l,
  set_dynamic_type_non_virtual_aux h p nil l (((obj, (ar, i, (h', p'))), ((h0, p0), (h, p))) :: l)
| set_dynamic_type_non_virtual_aux_cons : forall p b,
  forall c, hierarchy ! b = Some c ->
  forall h l l1,
    set_dynamic_type_non_virtual_aux h (p ++ b :: nil)
    (
      (map (fun hb : Class.Inheritance.t * ident => let (_, b) := hb in b) (filter (fun hb : _ * ident =>
    match hb with
      | (Class.Inheritance.Shared, _) => false
      | _ => true
    end
      ) (Class.super c)))
    )
    l l1 ->
    forall lb l2, set_dynamic_type_non_virtual_aux h p lb l1 l2 ->
      set_dynamic_type_non_virtual_aux h p (b :: lb) l l2
      .

Lemma set_dynamic_type_non_virtual_aux_func : forall h p l l1 l2,
  set_dynamic_type_non_virtual_aux h p l l1 l2 ->
  forall l2',
  set_dynamic_type_non_virtual_aux h p l l1 l2' ->
  l2 = l2'.

Lemma set_dynamic_type_non_virtual_aux_same : forall h p l l1 l2,
  set_dynamic_type_non_virtual_aux h p l l1 l2 ->
  forall h' p',
    (h', p') = concat (h0, p0) (h, p) ->
    assoc (@pointer_eq_dec _) (obj, (ar, i, (h', p'))) l2 = Some ((h0, p0), (h, p)).

Lemma set_dynamic_type_non_virtual_aux_other_cell : forall h p l l1 l2,
  set_dynamic_type_non_virtual_aux h p l l1 l2 ->
  forall obj' ar' i',
    (obj', ar', i') <> (obj, ar, i) ->
    forall h' p',
      assoc (@pointer_eq_dec _) (obj', (ar', i', (h', p'))) l2 =
      assoc (@pointer_eq_dec _) (obj', (ar', i', (h', p'))) l1.

Lemma set_dynamic_type_non_virtual_aux_other_path : forall h p l l1 l2,
  set_dynamic_type_non_virtual_aux h p l l1 l2 ->
 forall h' p',
(h', p') <> concat (h0, p0) (h, p) ->
(forall b', In b' l ->
  forall l', is_valid_repeated_subobject hierarchy (b' :: l') = true ->
    (h', p') <> concat (h0, p0) (h, p ++ b' :: l'))
    -> assoc (@pointer_eq_dec _) (obj, (ar, i, (h', p'))) l2 = assoc (@pointer_eq_dec _) (obj, (ar, i, (h', p'))) l1.

Lemma set_dynamic_type_non_virtual_aux_same_path : forall h p l l1 l2,
  set_dynamic_type_non_virtual_aux h p l l1 l2 ->
  p <> nil ->
  forall b, In b l ->
    forall l', is_valid_repeated_subobject hierarchy (b :: l') = true ->
      forall h' p',
        (h', p') = concat (h0, p0) (h, p ++ b :: l') ->
        assoc (@pointer_eq_dec _) (obj, (ar, i, (h', p'))) l2 = Some ((h0, p0), (h, p ++ b :: l'))
.

    
Inductive set_dynamic_type_non_virtual : Class.Inheritance.t -> list ident -> list_dynamic_type -> list_dynamic_type -> Prop :=
| set_dynamic_type_non_virtual_intro : forall p cn,
  last p = Some cn ->
  forall c, hierarchy ! cn = Some c ->
    forall h l1 l2,
      set_dynamic_type_non_virtual_aux h p
      (
        (map (fun hb : Class.Inheritance.t * ident => let (_, b) := hb in b) (filter (fun hb : _ * ident =>
          match hb with
            | (Class.Inheritance.Shared, _) => false
            | _ => true
          end
        ) (Class.super c)))
      )
      l1 l2 ->
      set_dynamic_type_non_virtual h p l1 l2
      .

Lemma set_dynamic_type_non_virtual_func : forall h p l1 l2,
  set_dynamic_type_non_virtual h p l1 l2 ->
  forall l2',
    set_dynamic_type_non_virtual h p l1 l2' ->
    l2 = l2'.

Lemma set_dynamic_type_non_virtual_other_cell : forall h p l1 l2,
  set_dynamic_type_non_virtual h p l1 l2 ->
  forall obj' ar' i',
    (obj', ar', i') <> (obj, ar, i) ->
    forall h' p',
      assoc (@pointer_eq_dec _) (obj', (ar', i', (h', p'))) l2 =
      assoc (@pointer_eq_dec _) (obj', (ar', i', (h', p'))) l1.

Lemma set_dynamic_type_non_virtual_other_path : forall h p from cn,
  path hierarchy cn p from h ->
  forall h' p',
    (forall p1 to, path hierarchy to p1 cn Class.Inheritance.Repeated -> (h', p') <> concat (h0, p0) (concat (h, p) (Class.Inheritance.Repeated, p1))) ->
    forall l1 l2,
      set_dynamic_type_non_virtual h p l1 l2 ->
      assoc (@pointer_eq_dec _) (obj, (ar, i, (h', p'))) l2 =
      assoc (@pointer_eq_dec _) (obj, (ar, i, (h', p'))) l1.

Lemma set_dynamic_type_non_virtual_same_path : forall h p from cn,
  path hierarchy cn p from h ->
  forall p1 to, path hierarchy to p1 cn Class.Inheritance.Repeated ->
    forall h' p',
      (h', p') = concat (h0, p0) (concat (h, p) (Class.Inheritance.Repeated, p1)) ->
      forall l1 l2,
        set_dynamic_type_non_virtual h p l1 l2 ->
        assoc (@pointer_eq_dec _) (obj, (ar, i, (h', p'))) l2 =
        Some ((h0, p0), concat (h, p) (Class.Inheritance.Repeated, p1))
        .

Inductive set_dynamic_type_virtual_aux : list ident -> list_dynamic_type -> list_dynamic_type -> Prop :=
| set_dynamic_type_virtual_aux_nil : forall l,
  set_dynamic_type_virtual_aux nil l l
| set_dynamic_type_virtual_aux_cons : forall b l1 l2,
  set_dynamic_type_non_virtual Class.Inheritance.Shared (b :: nil) l1 l2 ->
  forall l l3,
    set_dynamic_type_virtual_aux l l2 l3 ->
    set_dynamic_type_virtual_aux (b :: l) l1 l3.

Lemma set_dynamic_type_virtual_aux_func : forall l l1 l2,
  set_dynamic_type_virtual_aux l l1 l2 ->
  forall l2', set_dynamic_type_virtual_aux l l1 l2' ->
    l2 = l2'.

Lemma set_dynamic_type_virtual_aux_other_cell : forall l l1 l2,
  set_dynamic_type_virtual_aux l l1 l2 ->
  forall obj' ar' i',
    (obj', ar', i') <> (obj, ar, i) ->
    forall h' p',
      assoc (@pointer_eq_dec _) (obj', (ar', i', (h', p'))) l2 =
      assoc (@pointer_eq_dec _) (obj', (ar', i', (h', p'))) l1.


Section Virtual.

Variable dt : ident.

Lemma set_dynamic_type_virtual_aux_other_path : forall l l1 l2,
  set_dynamic_type_virtual_aux l l1 l2 ->
  (forall b, In b l -> path hierarchy b (b :: nil) dt Class.Inheritance.Shared) ->
  forall h' p',
    (forall b, In b l -> forall p'' to, path hierarchy to (b :: p'') b Class.Inheritance.Repeated -> (h', p') <> (Class.Inheritance.Shared, b :: p'')) ->
    assoc (@pointer_eq_dec _) (obj, (ar, i, (h', p'))) l2 =
    assoc (@pointer_eq_dec _) (obj, (ar, i, (h', p'))) l1.

Lemma set_dynamic_type_virtual_aux_same_path :
  forall l l1 l2,
    set_dynamic_type_virtual_aux l l1 l2 ->
    (forall b, In b l -> path hierarchy b (b :: nil) dt Class.Inheritance.Shared) ->
    forall b, In b l ->
      forall to p, path hierarchy to p b Class.Inheritance.Repeated ->
        assoc (@pointer_eq_dec _) (obj, (ar, i, (Class.Inheritance.Shared, p))) l2 =
        Some ((h0, p0), (Class.Inheritance.Shared, p)).
       

End Virtual.

Inductive set_dynamic_type : list_dynamic_type -> list_dynamic_type -> Prop :=
| set_dynamic_type_intro : forall cn,
  last p0 = Some cn ->
  forall c, hierarchy ! cn = Some c ->
    forall v, vborder_list hierarchy (Class.super c) v ->
      forall l1 l2,
        set_dynamic_type_virtual_aux v l1 l2 ->
        forall l3,
          set_dynamic_type_non_virtual Class.Inheritance.Repeated (cn :: nil) l2 l3 ->
          set_dynamic_type l1 l3.

Lemma set_dynamic_type_func : forall l1 l2,
  set_dynamic_type l1 l2 ->
  forall l2', set_dynamic_type l1 l2' -> l2 = l2'.

Lemma set_dynamic_type_other_cell : forall l1 l2,
  set_dynamic_type l1 l2 ->
  forall obj' ar' i',
    (obj', ar', i') <> (obj, ar, i) ->
    forall h' p',
      assoc (@pointer_eq_dec _) (obj', (ar', i', (h', p'))) l2 =
      assoc (@pointer_eq_dec _) (obj', (ar', i', (h', p'))) l1.


Section Subtract.

Variable U : Type.
Hypothesis U_eq_dec : forall u1 u2 : U, {u1 = u2} + {u1 <> u2}.

Lemma subtract (lshort llong : list U) : {
  lcompl | llong = lshort ++ lcompl
} + {
  forall lcompl, llong <> lshort ++ lcompl
}.

End Subtract.

Variable is_primary_path : list ident -> bool.

Lemma primary_ancestor_dec : forall h' p', {
  p'' : _ & {a | last p' = Some a /\ is_primary_path (a :: p'') = true /\
    (h0, p0) = concat (h', p') (Class.Inheritance.Repeated, a :: p'')}
} + {
  forall a, last p' = Some a -> forall p'', is_primary_path (a :: p'') = true ->
    (h0, p0) = concat (h', p') (Class.Inheritance.Repeated, a :: p'') -> False
}.

Function non_primary_ancestor (objarihphphp :
  ((ident * (array_path A * Z * (Class.Inheritance.t * list ident))) *
    ((Class.Inheritance.t * list ident) * (Class.Inheritance.t * list ident)))
) : bool :=
  match objarihphphp with
    | ((obj', (ar', i', (h', p'))), _) =>
      if prod_eq_dec (prod_eq_dec peq (@array_path_eq_dec _)) Z_eq_dec (obj', ar', i') (obj, ar, i)
        then
          if primary_ancestor_dec h' p' then false else true
        else true
  end.

Definition erase_non_primary_ancestor_dynamic_type (l : list_dynamic_type) : list_dynamic_type := filter non_primary_ancestor l.

Lemma erase_non_primary_ancestor_other_cell : forall obj' ar' i' h' ,
  (obj', ar', i') <> (obj, ar, i) ->
  forall l1 p',
    assoc (@pointer_eq_dec _) (obj', (ar', i', (h', p'))) (erase_non_primary_ancestor_dynamic_type l1) =
      assoc (@pointer_eq_dec _) (obj', (ar', i', (h', p'))) l1.

Corollary set_dynamic_type_strong_other_cell : forall l1 l2,
  set_dynamic_type (erase_non_primary_ancestor_dynamic_type l1) l2 ->
  forall obj' ar' i',
    (obj', ar', i') <> (obj, ar, i) ->
    forall h' p',
      assoc (@pointer_eq_dec _) (obj', (ar', i', (h', p'))) l2 =
      assoc (@pointer_eq_dec _) (obj', (ar', i', (h', p'))) l1.

Lemma erase_non_primary_ancestor_same : forall p' a, last p' = Some a -> forall p'', is_primary_path (a :: p'') = true -> forall h', (h0, p0) = concat (h', p') (Class.Inheritance.Repeated, a :: p'') ->
  forall l1,
    assoc (@pointer_eq_dec _) (obj, (ar, i, (h', p'))) (erase_non_primary_ancestor_dynamic_type l1) = None.

Lemma erase_non_primary_ancestor_other : forall h' p',
 (forall a, last p' = Some a -> forall p'', is_primary_path (a :: p'') = true -> (h0, p0) <> concat (h', p') (Class.Inheritance.Repeated, a :: p'')) ->
  forall l1,
    assoc (@pointer_eq_dec _) (obj, (ar, i, (h', p'))) (erase_non_primary_ancestor_dynamic_type l1) =
    assoc (@pointer_eq_dec _) (obj, (ar, i, (h', p'))) (l1).
 
End Set_dynamic_type.