Schulze.ml

open BinNums
open Datatypes
open Mat
open Nat
open Path

type coq_Node =
| A
| B
| C

(** val coq_Node_rect : 'a1 -> 'a1 -> 'a1 -> coq_Node -> 'a1 **)

let coq_Node_rect f f0 f1 = function
| A -> f
| B -> f0
| C -> f1

(** val coq_Node_rec : 'a1 -> 'a1 -> 'a1 -> coq_Node -> 'a1 **)

let coq_Node_rec f f0 f1 = function
| A -> f
| B -> f0
| C -> f1

(** val eqN : coq_Node -> coq_Node -> bool **)

let eqN x y =
  match x with
  | A -> (match y with
          | A -> Coq_true
          | _ -> Coq_false)
  | B -> (match y with
          | B -> Coq_true
          | _ -> Coq_false)
  | C -> (match y with
          | C -> Coq_true
          | _ -> Coq_false)

type coq_R =
| Left of nat
| Infinity

(** val coq_R_rect : (nat -> 'a1) -> 'a1 -> coq_R -> 'a1 **)

let coq_R_rect f f0 = function
| Left n -> f n
| Infinity -> f0

(** val coq_R_rec : (nat -> 'a1) -> 'a1 -> coq_R -> 'a1 **)

let coq_R_rec f f0 = function
| Left n -> f n
| Infinity -> f0

(** val eqR : coq_R -> coq_R -> bool **)

let eqR u v =
  match u with
  | Left x -> (match v with
               | Left y -> eqb x y
               | Infinity -> Coq_false)
  | Infinity -> (match v with
                 | Left _ -> Coq_false
                 | Infinity -> Coq_true)

(** val zeroR : coq_R **)

let zeroR =
  Left O

(** val oneR : coq_R **)

let oneR =
  Infinity

(** val plusR : coq_R -> coq_R -> coq_R **)

let plusR u v =
  match u with
  | Left x -> (match v with
               | Left y -> Left (max x y)
               | Infinity -> Infinity)
  | Infinity -> Infinity

(** val mulR : coq_R -> coq_R -> coq_R **)

let mulR u v =
  match u with
  | Left x -> (match v with
               | Left y -> Left (min x y)
               | Infinity -> Left x)
  | Infinity -> v

(** val finN : coq_Node list **)

let finN =
  Coq_cons (A, (Coq_cons (B, (Coq_cons (C, Coq_nil)))))

(** val schulze :
    (coq_Node, coq_R) coq_Matrix -> (coq_Node, coq_R) coq_Matrix **)

let schulze m =
  matrix_exp_binary eqN finN zeroR oneR plusR mulR m (Npos (Coq_xO Coq_xH))