module Algebra.MatrixData.Base where

open import Level using (Level)
open import Function
open import Data.Nat as ℕ using (ℕ)
open import Data.Vec

import Data.Vec.Functional as F

import Algebra.Matrix as F

private variable
  a : Level
  A : Set a
  m n p : ℕ

Matrix : Set a → (n m : ℕ) → Set a
Matrix A n m = Vec (Vec A m) n

matrixFunc→Data : F.Matrix A n m → Matrix A n m
matrixFunc→Data = tabulate ∘ (tabulate ∘_)

matrixData→Fun : Matrix A n m → F.Matrix A n m
matrixData→Fun = (lookup ∘_) ∘ lookup

m→v : ∀ {n} → Matrix A n  → Vec A n
m→v [] = []
m→v ((x ∷ []) ∷ A₂) = x ∷ m→v A₂