val transpose8x8_2: #t:v_inttype -> vec_t8 t -> vec_t8 t
let transpose8x8_2 #t (v0,v1,v2,v3,v4,v5,v6,v7) =
  let v0' = vec_interleave_low_n 4 v0 v4 in
  let v4' = vec_interleave_high_n 4 v0 v4 in
  let v1' = vec_interleave_low_n 4 v1 v5 in
  let v5' = vec_interleave_high_n 4 v1 v5 in
  let v2' = vec_interleave_low_n 4 v2 v6 in
  let v6' = vec_interleave_high_n 4 v2 v6 in
  let v3' = vec_interleave_low_n 4 v3 v7 in
  let v7' = vec_interleave_high_n 4 v3 v7 in
  (v0',v1',v2',v3',v4',v5',v6',v7')
val transpose8x8_2: #t:v_inttype -> vec_t8 t -> vec_t8 t
let transpose8x8_2 #t (v0, v1, v2, v3, v4, v5, v6, v7) =
let v0' = vec_interleave_low_n 4 v0 v4 in
let v4' = vec_interleave_high_n 4 v0 v4 in
let v1' = vec_interleave_low_n 4 v1 v5 in
let v5' = vec_interleave_high_n 4 v1 v5 in
let v2' = vec_interleave_low_n 4 v2 v6 in
let v6' = vec_interleave_high_n 4 v2 v6 in
let v3' = vec_interleave_low_n 4 v3 v7 in
let v7' = vec_interleave_high_n 4 v3 v7 in
(v0', v1', v2', v3', v4', v5', v6', v7')
Lib.IntVector.Transpose.fst.checked
prims.fst.checked Lib.LoopCombinators.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Lib.IntVector.Transpose.fst
Lib.IntVector.v_inttype Lib.IntVector.Transpose.vec_t8 Lib.IntVector.vec_t FStar.Pervasives.Native.Mktuple8 Lib.IntVector.vec_interleave_high_n Lib.IntVector.vec_interleave_low_n
module Lib.IntVector.Transpose

module Loops = Lib.LoopCombinators


#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

///
///  transpose4x4
///

inline_for_extraction
val transpose4x4_0: #t:v_inttype -> vec_t4 t -> vec_t4 t
let transpose4x4_0 #t (v0,v1,v2,v3) =
  let v0' = vec_interleave_low v0 v1 in
  let v1' = vec_interleave_high v0 v1 in
  let v2' = vec_interleave_low v2 v3 in
  let v3' = vec_interleave_high v2 v3 in

  let v0'' = vec_interleave_low_n 2 v0' v2' in
  let v1'' = vec_interleave_high_n 2 v0' v2' in
  let v2'' = vec_interleave_low_n 2 v1' v3' in
  let v3'' = vec_interleave_high_n 2 v1' v3' in
  (v0'',v2'',v1'',v3'')


inline_for_extraction
val transpose4x4_uint32: #t:v_inttype{t == U32} -> vec_t4 t -> vec_t4 t
let transpose4x4_uint32 #t vs =
  let (v0'',v2'',v1'',v3'') = transpose4x4_0 #t vs in
  (v0'',v1'',v2'',v3'')


inline_for_extraction
val transpose4x4_uint64: #t:v_inttype{t == U64} -> vec_t4 t -> vec_t4 t
let transpose4x4_uint64 #t vs = transpose4x4_0 #t vs


let transpose4x4 #t vs =
  match t with
  | U32 -> transpose4x4_uint32 #t vs
  | U64 -> transpose4x4_uint64 #t vs

///
///   transpose8x8
///

inline_for_extraction
val transpose8x8_0: #t:v_inttype -> vec_t8 t -> vec_t8 t
let transpose8x8_0 #t (v0,v1,v2,v3,v4,v5,v6,v7) =
  let v0' = vec_interleave_low v0 v1 in
  let v1' = vec_interleave_high v0 v1 in
  let v2' = vec_interleave_low v2 v3 in
  let v3' = vec_interleave_high v2 v3 in
  let v4' = vec_interleave_low v4 v5 in
  let v5' = vec_interleave_high v4 v5 in
  let v6' = vec_interleave_low v6 v7 in
  let v7' = vec_interleave_high v6 v7 in
  (v0',v1',v2',v3',v4',v5',v6',v7')


inline_for_extraction
val transpose8x8_1: #t:v_inttype -> vec_t8 t -> vec_t8 t
let transpose8x8_1 #t (v0,v1,v2,v3,v4,v5,v6,v7) =
  let v0' = vec_interleave_low_n 2 v0 v2 in
  let v2' = vec_interleave_high_n 2 v0 v2 in
  let v1' = vec_interleave_low_n 2 v1 v3 in
  let v3' = vec_interleave_high_n 2 v1 v3 in
  let v4' = vec_interleave_low_n 2 v4 v6 in
  let v6' = vec_interleave_high_n 2 v4 v6 in
  let v5' = vec_interleave_low_n 2 v5 v7 in
  let v7' = vec_interleave_high_n 2 v5 v7 in
  (v0',v1',v2',v3',v4',v5',v6',v7')


inline_for_extraction
val transpose8x8_2: #t:v_inttype -> vec_t8 t -> vec_t8 t
_: Lib.IntVector.Transpose.vec_t8 t -> Lib.IntVector.Transpose.vec_t8 t