Binding

Require Import Intro.
Require Import Interface.

Components are connected throught bindings on their interfaces. One such binding is composed by two intervenients: the client interface and the server interface. These are identified by the identifier of the component holding the interface and the identifier of the interface itself.

Inductive binding : Type :=
  | Normal : path -> ident -> ident -> ident -> ident -> binding
  | Export : path -> ident -> ident -> ident -> binding
  | Import : path -> ident -> ident -> ident -> binding.

Function beq_binding (b1 b2: binding) : bool :=
  match b1, b2 with
     Normal p idC1 idI1 idC2 idI2, Normal p' idC1' idI1' idC2' idI2' =>
       beq_path p p' && beq_ident idC1 idC1' && beq_ident idI1 idI1' &&
                       beq_ident idC2 idC2' && beq_ident idI2 idI2'
  | Normal _ _ _ _ _, _ => false
  | Export p idI1 idC2 idI2, Export p' idI1' idC2' idI2' =>
       beq_path p p' && beq_ident idI1 idI1' &&
                        beq_ident idC2 idC2' && beq_ident idI2 idI2'
  | Export _ _ _ _, _ => false
  | Import p idI1 idC2 idI2, Import p' idI1' idC2' idI2' =>
       beq_path p p' && beq_ident idI1 idI1' &&
                      beq_ident idC2 idC2' && beq_ident idI2 idI2'
  | Import _ _ _ _, _ => false
  end.

Lemma binding_dec:
  forall b b' : binding, {b = b'} + {b <> b'}.
Proof.
  intros.
  decide equality; decide equality.
Qed.

Hint Resolve binding_dec.

Bind Scope binding_scope with binding.
Delimit Scope binding_scope with bind.
Notation "b1 '==' b2" := (beq_binding b1 b2) (at level 80) : binding_scope.
Notation "b1 '!=' b2" := (~~ beq_binding b1 b2) (at level 80) : binding_scope.

Binding

Nothing special here, just the respective projections and notations for them.

Definition projectionBindingClientPath (b:binding) : path :=
   match b with
     | Normal p idComp1 idInt1 idComp2 idInt2 => p
     | Export p idInt1 idSubComp idInt2 => p
     | Import p idInt1 idSubComp idInt2 => p
  end.

Definition projectionNormalBindingComp1Id (b:binding) : ident :=
   match b with
     | Normal p idComp1 idInt1 idComp2 idInt2 => idComp1
     | _ => ErrorIdent
   end.

Definition projectionNormalBindingInt1Id (b:binding) : ident :=
   match b with
     | Normal p idComp1 idInt1 idComp2 idInt2 => idInt1
     | _ => ErrorIdent
   end.

Definition projectionNormalBindingComp2Id (b:binding) : ident :=
   match b with
     | Normal p idComp1 idInt1 idComp2 idInt2 => idComp2
     | _ => ErrorIdent
   end.

Definition projectionNormalBindingInt2Id (b:binding) : ident :=
   match b with
     | Normal p idComp1 idInt1 idComp2 idInt2 => idInt2
     | _ => ErrorIdent
   end.

Definition projectionBindingIntId (b:binding) : ident :=
   match b with
     | Export p idInt1 idSubComp idInt2 => idInt1
     | Import p idInt1 idSubComp idInt2 => idInt1
     | _ => ErrorIdent
  end.

Definition projectionBindingIntId2 (b:binding) : ident :=
   match b with
     | Export p idInt1 idSubComp idInt2 => idInt2
     | Import p idInt1 idSubComp idInt2 => idInt2
     | _ => ErrorIdent
  end.

Definition projectionBindingSubComponent (b:binding) : ident :=
   match b with
     | Export p idInt1 idSubComp idInt2 => idSubComp
     | Import p idInt1 idSubComp idInt2 => idSubComp
     | _ => ErrorIdent
  end.

Notation "b '->path' " := (projectionBindingClientPath b) (at level 80, right associativity) : binding_scope.

Lemma path_equality_bool2Prop:
   forall p p',
   (p == p')%path = true ->
   p = p'.
Proof.
  intros.
  functional induction beq_path p p'; try congruence.
  assert ((id == id')=true).
    auto.
  assert (id = id' /\ r = r').
    split; auto.
  destruct H1; subst; auto.
Qed.

Hint Resolve path_equality_bool2Prop.

Lemma binding_equality_bool2Prop:
   forall b b',
   (b == b')%bind = true ->
   b = b'.
Proof.
  intros.
  functional induction beq_binding b b'; try congruence.
  Case "1/3".
    assert
      (p = p' /\ idC1 = idC1' /\ idI1 = idI1' /\ idC2 = idC2' /\ idI2 = idI2').
        rewrite !andb_true_iff in H.
        destruct H as ((((Hp, Hidc1), Hidi1), Hidc2), Hidi2).
        repeat split; auto.
    destruct H0 as (Hp, (Hidc1, (Hidi1, (Hidc2, Hidi2)))).
    subst.
    reflexivity.
  Case "2/3".
    assert ((p = p')%path /\ idI1 = idI1' /\ idC2 = idC2' /\ idI2 = idI2').
      rewrite !andb_true_iff in H.
      destruct H as (((Hp, Hidc1), Hidi1), Hidc2).
      repeat split; auto.
    destruct H0 as (Hp, (Hidi1, (Hidc2, Hidi2))).
    subst.
    reflexivity.
  Case "3/3".
    assert ((p = p')%path /\ idI1 = idI1' /\ idC2 = idC2' /\ idI2 = idI2').
      rewrite !andb_true_iff in H.
      destruct H as (((Hp, Hidc1), Hidi1), Hidc2).
      repeat split; auto.
    destruct H0 as (Hp, (Hidi1, (Hidc2, Hidi2))).
    subst.
    reflexivity.
Qed.

Hint Resolve binding_equality_bool2Prop.

Lemma path_equality_Prop2bool:
   forall p p',
   p = p' ->
   (p == p')%path = true.
Proof.
  intros.
  functional induction beq_path p p'; auto.
  Case "1/3".
    inversion H; subst.
    assert ((id' == id') = false).
      auto.
    assert (id' <> id').
      auto.
    congruence.
  Case "2/3".
    apply IHb.
    inversion H; auto.
  Case "3/3".
    destruct p;
    inversion y.
Qed.

Hint Resolve path_equality_Prop2bool.

Lemma binding_equality_Prop2bool:
   forall b b',
   b = b' ->
   (b == b')%bind = true.
Proof.
  intros.
  functional induction beq_binding b b'; eauto;
    rewrite !andb_true_iff;
    inversion H;
    repeat split; auto.
Qed.

Hint Resolve binding_equality_Prop2bool.