From Coq Require Import Setoid.
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import RelationPairs.
From Coq Require Import Lt.
From Coq Require Import NArith.
From Coq Require Import Lia.

From Padec Require Import SetoidUtil.
From Padec Require Import Algorithm.
From Padec Require Import NatUtils.
From Padec Require Import ListUtils.

Open Scope signature_scope.
Open Scope nat_scope.
Set Implicit Arguments.

Section make_net.

  Variable (matrix: list (list N)).
  Definition K := match length matrix with O => 1%N | n => N.of_nat n end.

  Lemma Kpos: (0<K)%N.

  Definition node_matrix :=
    map (map_filter (ltK_inj K)) matrix.

  Fixpoint channel_error n (l: list (ltK K)) i:=
    match l with
      nil => None
    | n'::q => if (N.eq_dec n (proj1_sig n')) then Some i
               else channel_error n q (S i)
    end.

  Lemma channel_error_prop: forall n l i,
      channel_error (proj1_sig n) (l: list (ltK K)) 0 == Some i ->
      nth_error l i == Some n.

  Definition row (n: N) :=
    nth (N.to_nat n) node_matrix nil.

  Definition peer_ (n: N) (c:nat) :=
    let l := row n in
    match nth_error l c with
      Some n' =>
      if (N.eq_dec n (proj1_sig n')) then None else
        match channel_error (proj1_sig n') l 0 with
          Some c' =>if (PeanoNat.Nat.eq_dec c c') then Some n' else None
        | None => None end
    | None => None
    end.

  Lemma peer_prop: forall n c n',
    peer_ n c == Some n' ->
      nth_error (row n) c == Some n' /\
      channel_error (proj1_sig n') (row n) 0 == Some c /\
      ~ n == (proj1_sig n').

  Definition link_ (n: N) (n': N) :=
    if N.eq_dec n' n then None else channel_error n' (row n) 0.

  Definition peers_ n l :=
    map_filter
      (fun n' => if N.eq_dec (proj1_sig n') n then None else
                   channel_error (proj1_sig n') l 0) l.

  Definition reply_to_ n c:=
    match peer_ n c with
      None => 0
    | Some n' =>
      match channel_error n (row (proj1_sig n')) 0 with
        None => 0
      | Some c' => c'
      end end.

  Instance Chans: Channels := {| Channel := nat; Channel_dec := PeanoNat.Nat.eq_dec |}.

  Program Definition Net: Network (Chans:=Chans) :=
    {|
      Node := ltK K;
      Node_dec := ltK_dec (K := K);
      peer:=peer_;
      link:=link_;
      all_nodes:=Kenum K;
      all_nodes_prop := ltK_in_Kenum (K := K)
    |}.
End make_net.


Close Scope signature_scope.
Close Scope nat_scope.
Unset Implicit Arguments.