Mat.ml

open Definitions
open List
open Path

(** val get_row : ('a1, 'a2) coq_Matrix -> 'a1 -> 'a1 -> 'a2 **)

let get_row m =
  m

(** val get_col : ('a1, 'a2) coq_Matrix -> 'a1 -> 'a1 -> 'a2 **)

let get_col m c d =
  m d c

(** val zero_matrix : 'a2 -> ('a1, 'a2) coq_Matrix **)

let zero_matrix zeroR _ _ =
  zeroR

(** val coq_I : 'a1 brel -> 'a2 -> 'a2 -> ('a1, 'a2) coq_Matrix **)

let coq_I eqN zeroR oneR c d =
  if eqN c d then oneR else zeroR

(** val transpose : ('a1, 'a2) coq_Matrix -> ('a1, 'a2) coq_Matrix **)

let transpose m c d =
  m d c

(** val matrix_add :
    'a2 binary_op -> ('a1, 'a2) coq_Matrix -> ('a1, 'a2) coq_Matrix -> ('a1,
    'a2) coq_Matrix **)

let matrix_add plusR m_UU2081_ m_UU2082_ c d =
  plusR (m_UU2081_ c d) (m_UU2082_ c d)

(** val sum_fn : 'a2 -> 'a2 binary_op -> ('a1 -> 'a2) -> 'a1 list -> 'a2 **)

let sum_fn zeroR plusR f l =
  fold_right (fun x y -> plusR (f x) y) zeroR l

(** val matrix_mul_gen :
    'a2 -> 'a2 binary_op -> 'a2 binary_op -> ('a1, 'a2) coq_Matrix -> ('a1,
    'a2) coq_Matrix -> 'a1 list -> ('a1, 'a2) coq_Matrix **)

let matrix_mul_gen zeroR plusR mulR m_UU2081_ m_UU2082_ l c d =
  sum_fn zeroR plusR (fun y -> mulR (m_UU2081_ c y) (m_UU2082_ y d)) l

(** val matrix_mul :
    'a1 list -> 'a2 -> 'a2 binary_op -> 'a2 binary_op -> ('a1, 'a2)
    coq_Matrix -> ('a1, 'a2) coq_Matrix -> ('a1, 'a2) coq_Matrix **)

let matrix_mul finN zeroR plusR mulR m_UU2081_ m_UU2082_ =
  matrix_mul_gen zeroR plusR mulR m_UU2081_ m_UU2082_ finN

(** val matrix_exp_unary :
    'a1 brel -> 'a1 list -> 'a2 -> 'a2 -> 'a2 binary_op -> 'a2 binary_op ->
    ('a1, 'a2) coq_Matrix -> int -> ('a1, 'a2) coq_Matrix **)

let rec matrix_exp_unary eqN finN zeroR oneR plusR mulR m n =
  (fun fO fS n -> if n=0 then fO () else fS (n-1))
    (fun _ -> coq_I eqN zeroR oneR)
    (fun n' ->
    matrix_mul finN zeroR plusR mulR m
      (matrix_exp_unary eqN finN zeroR oneR plusR mulR m n'))
    n

(** val repeat_op_ntimes_rec :
    'a1 list -> 'a2 -> 'a2 binary_op -> 'a2 binary_op -> ('a1, 'a2)
    coq_Matrix -> int -> ('a1, 'a2) coq_Matrix **)

let rec repeat_op_ntimes_rec finN zeroR plusR mulR e n =
  (fun f2p1 f2p f1 p -> if p<=1 then f1 () else if p mod 2 = 0 then f2p (p/2) else f2p1 (p/2))
    (fun p ->
    let reta = repeat_op_ntimes_rec finN zeroR plusR mulR e p in
    let retb = matrix_mul finN zeroR plusR mulR reta reta in
    matrix_mul finN zeroR plusR mulR e retb)
    (fun p ->
    let ret = repeat_op_ntimes_rec finN zeroR plusR mulR e p in
    matrix_mul finN zeroR plusR mulR ret ret)
    (fun _ -> e)
    n

(** val matrix_exp_binary :
    'a1 brel -> 'a1 list -> 'a2 -> 'a2 -> 'a2 binary_op -> 'a2 binary_op ->
    ('a1, 'a2) coq_Matrix -> int -> ('a1, 'a2) coq_Matrix **)

let matrix_exp_binary eqN finN zeroR oneR plusR mulR e n =
  (fun f0 fp n -> if n=0 then f0 () else fp n)
    (fun _ -> coq_I eqN zeroR oneR)
    (fun p -> repeat_op_ntimes_rec finN zeroR plusR mulR e p)
    n

(** val exp_r : 'a1 -> 'a1 binary_op -> 'a1 -> int -> 'a1 **)

let rec exp_r oneR mulR a n =
  (fun fO fS n -> if n=0 then fO () else fS (n-1))
    (fun _ -> oneR)
    (fun n' -> mulR a (exp_r oneR mulR a n'))
    n

(** val partial_sum_r :
    'a1 -> 'a1 binary_op -> 'a1 binary_op -> 'a1 -> int -> 'a1 **)

let rec partial_sum_r oneR plusR mulR a n =
  (fun fO fS n -> if n=0 then fO () else fS (n-1))
    (fun _ -> oneR)
    (fun n' ->
    plusR (partial_sum_r oneR plusR mulR a n') (exp_r oneR mulR a n))
    n

(** val partial_sum_mat :
    'a1 brel -> 'a1 list -> 'a2 -> 'a2 -> 'a2 binary_op -> 'a2 binary_op ->
    ('a1, 'a2) coq_Matrix -> int -> ('a1, 'a2) coq_Matrix **)

let rec partial_sum_mat eqN finN zeroR oneR plusR mulR m n =
  (fun fO fS n -> if n=0 then fO () else fS (n-1))
    (fun _ -> coq_I eqN zeroR oneR)
    (fun n' ->
    matrix_add plusR (partial_sum_mat eqN finN zeroR oneR plusR mulR m n')
      (matrix_exp_unary eqN finN zeroR oneR plusR mulR m n))
    n