Mefresa.GCM.Component

In this section we define the core notions of the GCM Component Model: Component, Interface and Binding.
Require Export Mefresa.GCM.Base.
Require Export Mefresa.GCM.Interface.
Require Export Mefresa.GCM.Binding.
Require Import Coq.Bool.Bool.

Core Elements

In the following we show how we encode Interfaces, Bindings and Components in Coq and prove some general properties about them.

Component

A component is constituted by a type, a path, subcomponents, interfaces, bindings between its subcomponents and a control level. This last element, is defined as follows:

Control Level


Inductive controlLevel : Type :=
  | Lowest : controlLevel
  | Introspection : controlLevel
  | Configuration : controlLevel.
Function beq_controlLevel (cl1 cl2: controlLevel) : bool :=
  match cl1, cl2 with
    | Lowest , Lowest => true
    | Introspection, Introspection => true
    | Configuration, Configuration => true
    | _ , _ => false
  end.

Lemma controlLevel_dec:
  forall cl cl': controlLevel, {cl = cl'} + {cl <> cl'}.
Proof.
  decide equality.
Qed.

Bind Scope controlLevel_scope with controlLevel.
Delimit Scope controlLevel_scope with ctlvl.
Notation "cl1 '==' cl2" := (beq_controlLevel cl1 cl2) (at level 80) : controlLevel_scope.
Notation "cl1 '!=' cl2" := (~~ beq_controlLevel cl1 cl2) (at level 80) : controlLevel_scope.

Lemma controlLevel_eq_reflection:
  forall cl1 cl2, (cl1 == cl2)%ctlvl = true <-> cl1=cl2.
Proof.
  destruct cl1; destruct cl2; split; simpl; intro; try congruence.
Qed.
As for components, there are defined analagously to interfaces.

Implementation Class


Definition implementationClass := string.

Lemma implementationClass_dec:
  forall ic ic' : implementationClass, {ic = ic'} + {ic <> ic'}.
Proof.
  apply string_dec.
Qed.

Function beq_implementationClass ic1 ic2 : bool := beq_string ic1 ic2.

Bind Scope implementationClass_scope with implementationClass.
Delimit Scope implementationClass_scope with iclass.
Notation "ic1 '==' ic2" := (beq_implementationClass ic1 ic2) (at level 80) : implementationClass_scope.
Notation "ic1 '!=' ic2" := (~~ beq_implementationClass ic1 ic2) (at level 80) : implementationClass_scope.

Lemma implementationClass_eq_reflection:
  forall ic1 ic2 : implementationClass, (ic1 == ic2)%iclass = true <-> ic1=ic2.
Proof.
  intros.
  rewrite beq_string_reflection.
  unfold beq_implementationClass.
  intuition.
Qed.

Inductive component :=
  | Component : ident ->
                               path ->
                               implementationClass ->
                               controlLevel ->
                               list component ->
                               list interface ->
                               list binding ->
                               component.
Proving the decidability of component's equality is more tricky since it refers itself as one of its projections. Therefore we need the following tricks.

Hint Resolve binding_dec interface_dec controlLevel_dec implementationClass_dec.

Definition list_dec {A} (eqd : forall (a b : A), {a=b}+{a<>b})
: forall (a b : list A), {a=b}+{a<>b}.
    decide equality.
Defined.

Fixpoint component_eq_dec (a b : component) : {a=b}+{a<>b}.
  decide equality;
  [ apply list_dec; auto
  | apply list_dec; auto
  | apply list_dec; auto
  | apply list_dec; auto].
Defined.
Lemma component_dec:
  forall c c' : component, {c = c'} + {c <> c'}.
Proof.
  intros.
  apply component_eq_dec.
Qed.
Following the rationale of the previous definitions, two components are equal if all their constituents are equal. As such, we will need to define comparison operators for lists of interfaces, lists of bindings and lists of components.

Function beq_list_interface (li li': list interface) {struct li} : bool :=
  match li, li' with
    | nil, nil => true
    | i :: r, i' :: r' => (i == i')%int && (beq_list_interface r r')
    | _, _ => false
  end.

Bind Scope list_interface_scope with list interface.
Delimit Scope list_interface_scope with l_int.
Notation "li1 '==' li2" := (beq_list_interface li1 li2) (at level 80) : list_interface_scope.

Lemma list_interface_eq_reflection:
    forall li li', (li == li')%l_int = true <-> li = li'.
Proof.
  induction li; induction li'; split; simpl; intro; try congruence.
  Case "1/2".
    rewrite andb_true_iff in H.
    destruct H.
    assert (a=a0).
      apply interface_eq_reflection; auto.
    subst.
    apply f_equal.
    apply IHli;auto.
  Case "2/2".
    inversion H; subst.
    rewrite andb_true_iff; split.
    SCase "Same Head".
      apply interface_eq_reflection; auto.
    SCase "Same Tail".
      apply IHli;auto.
Qed.

Function beq_list_binding (lb lb': list binding) {struct lb} : bool :=
  match lb, lb' with
    | nil, nil => true
    | b :: r, b' :: r' => (b == b')%bind && (beq_list_binding r r')
    | _, _ => false
  end.

Bind Scope list_binding_scope with list binding.
Delimit Scope list_binding_scope with l_bind.
Notation "lb1 '==' lb2" := (beq_list_binding lb1 lb2) (at level 80) : list_binding_scope.

Lemma list_binding_eq_reflection:
    forall lb lb', (lb == lb')%l_bind = true <-> lb = lb'.
Proof.
  induction lb; induction lb'; split; simpl; intro; try congruence.
  Case "1/2".
    rewrite andb_true_iff in H.
    destruct H.
    assert (a=a0).
      apply binding_eq_reflection; auto.
    subst.
    apply f_equal.
    apply IHlb;auto.
  Case "2/2".
    inversion H; subst.
    rewrite andb_true_iff; split.
    SCase "Same Head".
      apply binding_eq_reflection; auto.
    SCase "Same Tail".
      apply IHlb;auto.
Qed.

Fixpoint beq_comp (c c':component) : bool :=
  match c, c' with
   | Component id p iclass cl lc li lb, Component id' p' iclass' cl' lc' li' lb' =>
     (id == id') && (p == p')%path && (iclass == iclass')%iclass &&
     (cl == cl')%ctlvl && (li == li')%l_int && (lb == lb')%l_bind &&
     ((fix beq_lc (lc1 lc2: list component) {struct lc1} : bool :=
      match lc1, lc2 with
        | nil , nil => true
        | c1 :: r1, c2 :: r2 => if beq_comp c1 c2 then beq_lc r1 r2 else false
        | _ , _ => false
      end) lc lc')
    
  end.

Definition beq_component := beq_comp.

Bind Scope component_scope with component.
Delimit Scope component_scope with comp.
Notation "c1 '==' c2" := (beq_comp c1 c2) (at level 80) : component_scope.
All the fields of our Component definition should pose no doubt on its intended meaning. The only subtlety may arise from the path field.
As discussed above, GCM is an hierarchical component model, and this is implicity captured by the fact that a component is defined as being composed by a list of components. Indeed, this recursive definition seamlessly models this structure.
As such, a component must contain a path indicating its position in the hierarchy. This path can be just represented as a list of identifiers, determining the components to be traversed in order to reach the intended component.

Component Projections

As we did for interfaces and bindings, we start by defining the projections and the notations for them.

Definition projectionComponentId (c:component) : ident :=
   match c with
     | Component componentId p iclass controlLevel subComponents interfaces bindings => componentId
   end.

Definition projectionComponentPath (c:component) : path :=
   match c with
     | Component componentId p iclass controlLevel subComponents interfaces bindings => p
   end.

Definition projectionComponentImplementationClass (c:component) : implementationClass :=
   match c with
     | Component componentId p iclass controlLevel subComponents interfaces bindings => iclass
   end.

Definition projectionComponentControlLevel (c:component) : controlLevel :=
   match c with
     | Component componentId p iclass controlLevel subComponents interfaces bindings => controlLevel
   end.

Definition projectionComponentSubComponents (c:component) : list component :=
   match c with
     | Component componentId p iclass controlLevel subComponents interfaces bindings => subComponents
   end.

Definition projectionComponentInterfaces (c:component) : list interface :=
   match c with
     | Component componentId p iclass controlLevel subComponents interfaces bindings => interfaces
   end.

Definition projectionComponentBindings (c:component) : list binding :=
   match c with
     | Component componentId p iclass controlLevel subComponents interfaces bindings => bindings
   end.

Notation "c '->id' " := (projectionComponentId c) (at level 80, right associativity) : component_scope.
Notation "c '->path' " := (projectionComponentPath c) (at level 80, right associativity) : component_scope.
Notation "c '->iclass' " := (projectionComponentImplementationClass c) (at level 80, right associativity) : component_scope.
Notation "c '->controlLevel' " := (projectionComponentControlLevel c) (at level 80, right associativity) : component_scope.
Notation "c '->subComponents' " := (projectionComponentSubComponents c) (at level 80, right associativity) : component_scope.
Notation "c '->subcomps' " := (projectionComponentSubComponents c) (at level 80, right associativity) : component_scope.
Notation "c '->interfaces' " := (projectionComponentInterfaces c) (at level 80, right associativity) : component_scope.
Notation "c '->itfs' " := (projectionComponentInterfaces c) (at level 80, right associativity) : component_scope.
Notation "c '->bindings' " := (projectionComponentBindings c) (at level 80, right associativity) : component_scope.
Notation "c '->bnds' " := (projectionComponentBindings c) (at level 80, right associativity) : component_scope.

Lemma beq_comp_id_fact:
     forall c c', (c==c')%comp=true ->
                  ((c->id%comp) == (c'->id%comp)) = true.
Proof.
  intros.
  unfold beq_comp in H.
  destruct c; destruct c'.
  repeat rewrite andb_true_iff in H.
  do 6 (destruct H).
  simpl; auto.
Qed.