tried having port out

src/AbstractBigraphs.v

@@ -34,7 +34,6 @@ Import ListNotations.
 Module Bigraph.
 
 Definition finite (A : Type) : Type := { l : list A | Listing l }.
-
 Definition acyclic (node site root : Type) (parent : node + site -> node + root) : Prop :=
   forall (n:node), Acc (fun n n' => parent (inl n) = (inl n')) n.
 
@@ -48,10 +47,11 @@ Record bigraph (site: Type) (innername: Type) (root: Type) (outername: Type) (ki
   Big  
   { 
     node : Type ;
+    port : node * nat ;
     edge : Type ;
-    control : node -> kind * nat; (* k * nat *)
+    control : node -> kind * nat; 
     parent : node + site -> node + root ; 
-    link : innername + Port node kind control -> outername + edge; 
+    link : innername + port -> outername + edge; 
     (* sd : EqDec site ;
     sf : finite site ;
     id_ : EqDec innername ;
@@ -60,16 +60,34 @@ Record bigraph (site: Type) (innername: Type) (root: Type) (outername: Type) (ki
     rf : finite root ;
     od : EqDec outername ;
     of : finite outername ; *)
-    (* nd : EqDec node ;
+    pc : forall p:port, snd p < snd (control (fst p)) ;
+    nd : EqDec node ;
     nf : finite node ;
     ed : EqDec edge ;
-    ef : finite edge ;*)
-    (* ap : acyclic parent *)
+    ef : finite edge ;
+    ap : acyclic node site root parent ;
   }.
   (* sortir les preuves des types interface?*)
 
 Check parent.
 
+Fixpoint merge_list {A B : Type} (la : list A) (lb : list B) (acc : list (A + B)) : list (A + B) :=
+  match la with
+  | [] => acc ++ (map inr lb)
+  | ha :: ta => merge_list ta lb ((inl ha) :: acc)
+  end.
+  
+Definition merge {A B : Type} (la : list A) (lb : list B) : list (A + B) :=
+  merge_list la lb [].
+
+(* Fixpoint merge_list {A B: Type} (la: list A) (lb : list B) : list (A + B) :=
+  match la, lb with 
+  | ta :: qa, _ => (inl ta) :: merge_list qa lb
+  | [], tb :: qb => (inr tb) :: merge_list [] qb
+  | [], [] => []
+  end. *)
+
+
 Definition getNode {s i r o k : Type} (bg : bigraph s i r o k) : Type := 
   node s i r o k bg.
 
@@ -161,7 +179,6 @@ Definition mk_new_link {s1 i1 r1 o1 k1 s2 i2 r2 o2 k2 : Type}
                                 | inr e2 => inr (inl e2)
                                 end
                   end
-
       | inl i =>  match i with 
                   |inl i1 =>  match l1 (inl i1) with
                               | inl o1 => inl (inl o1)
@@ -183,7 +200,45 @@ Definition mk_new_link' {s1 i1 r1 o1 k1 s2 i2 r2 o2 k2 : Type}
   -> (o1 + o2) + ((getEdge b1) + (getEdge b2)).
   Admitted.
 
-(*close_scope nat_scope*)
+Definition getNd {s i r o k : Type} (bg : bigraph s i r o k) : 
+  EqDec (getNode bg) :=
+  @nd s i r o k bg.
+Definition mk_new_nd {s1 i1 r1 o1 k1 s2 i2 r2 o2 k2 : Type} 
+  (b1 : bigraph s1 i1 r1 o1 k1) (b2 : bigraph s2 i2 r2 o2 k2) :
+  EqDec ((getNode b1) + (getNode b2)).
+  Proof.  
+    destruct (getNd b1). EqDec. as [l1 H1]. 
+    destruct (getNd b2) as [l2 H2].Admitted.
+Definition getNf {s i r o k : Type} (bg : bigraph s i r o k) : 
+  finite (getNode bg) :=
+  @nf s i r o k bg.
+  
+Definition mk_new_nf {s i r o k : Type} 
+  (bg : bigraph s i r o k) (bg' : bigraph s i r o k) :
+  finite ((getNode bg) + (getNode bg')). 
+  Proof. 
+    destruct (getNf bg) as [l1 H1]. 
+    destruct (getNf bg') as [l2 H2].
+    unfold finite. 
+    exists (merge l1 l2). 
+    unfold merge. unfold merge_list. Admitted.
+Definition mk_new_nf' {s1 i1 r1 o1 k1 s2 i2 r2 o2 k2 : Type} 
+  (b1 : bigraph s1 i1 r1 o1 k1) (b2 : bigraph s2 i2 r2 o2 k2) :
+  finite ((getNode b1) + (getNode b2)). 
+  Proof. 
+    destruct (getNf b1) as [l1 H1]. 
+    destruct (getNf b2) as [l2 H2].
+    unfold finite. Admitted.  
+Definition mk_new_ed {s1 i1 r1 o1 k1 s2 i2 r2 o2 k2 : Type} 
+  (b1 : bigraph s1 i1 r1 o1 k1) (b2 : bigraph s2 i2 r2 o2 k2) :
+  EqDec ((getEdge b1) + (getEdge b2)). Admitted.
+Definition mk_new_ef {s1 i1 r1 o1 k1 s2 i2 r2 o2 k2 : Type} 
+  (b1 : bigraph s1 i1 r1 o1 k1) (b2 : bigraph s2 i2 r2 o2 k2) :
+  finite ((getEdge b1) + (getEdge b2)). Admitted.
+Definition mk_new_ap {s1 i1 r1 o1 k1 s2 i2 r2 o2 k2 : Type} 
+  (b1 : bigraph s1 i1 r1 o1 k1) (b2 : bigraph s2 i2 r2 o2 k2) :
+  acyclic ((getNode b1) + (getNode b2)) (s1 + s2) (r1 + r2) (mk_new_parent b1 b2). Admitted.
+
 Definition juxtaposition {s1 i1 r1 o1 k1 s2 i2 r2 o2 k2 : Type} 
   (b1 : bigraph s1 i1 r1 o1 k1) (b2 : bigraph s2 i2 r2 o2 k2) 
     : bigraph (s1+s2)%type (i1+i2)%type (r1+r2)%type (o1+o2)%type (k1+k2)%type :=
@@ -193,10 +248,15 @@ Definition juxtaposition {s1 i1 r1 o1 k1 s2 i2 r2 o2 k2 : Type}
     control := mk_new_control b1 b2 ;
     parent := mk_new_parent b1 b2 ;
     link := mk_new_link b1 b2 ;
+    nd := mk_new_nd b1 b2 ;
+    nf := mk_new_nf b1 b2 ;
+    ed := mk_new_ed b1 b2 ;
+    ef := mk_new_ef b1 b2 ;
+    ap := mk_new_ap b1 b2 ;
   |}.
 
-  
-  let new_node : Type := (node b1 + node b2)%type in
+(*comments*)
+  (* let new_node : Type := (node b1 + node b2)%type in
   (* let eqdec_newnode := fun a b =>
     match a, b with
     | inl a1, inl b1 => nd a1 b1
@@ -294,7 +354,7 @@ Definition juxtaposition {s1 i1 r1 o1 k1 s2 i2 r2 o2 k2 : Type}
     ed : EqDec edge ;
     ef : Finite edge ; *)
     (* ap := new_ap *)
-  |}.
+  |}. *)
   (* Big new_parent new_link (s1+s2)%type (i1+i2) (r1+r2) (o1+o2) new_node new_edge new_control. 
 
   { node := new_node ;