Multivariable linear differential equation solving in Idris2

Diffeq.idr

module Diffeq

import Data.Vect
import Data.Stream

Matrix : (m,n : Nat) -> Type
Matrix m n = Vect m (Vect n Double)

export infixl 10 *

sumVect : {a : Nat} -> (Vect a Double) -> Double
sumVect Nil = 0
sumVect (head :: tail) =  head + (sumVect tail)

ptwiseProd :{n : Nat} -> Vect n Double -> Vect n Double -> Vect n 
ptwiseProd a b = zipWith * a b

(+) : {n : Nat} -> Vect n Double -> Vect n Double -> Vect n Double
(+) a b = zipWith + a b

(*) : {m,n : Nat} -> Matrix m n -> Vect n Double -> Vect m Double
(*) Nil v = Nil
(*) (r1 :: rows) v = (sumVect (ptwiseProd r1 v)) :: ((*) rows v)

Solve : {m : Nat} -> Matrix m m -> Vect m Double -> Stream (Vect m Double)
Solve mat init = iterate (\v => (v + mat * v)) init

-- a diverging simple harmonic oscillator

SHO : Matrix 2 2
SHO = (0.0 :: (-1.3 :: Nil)) 
    :: (-1.0 ::(0.0 :: Nil) ) 
    :: Nil

Traj : Stream (Vect 2 Double)
Traj = Solve SHO (1.0 :: (1.0 :: Nil))

{-- 
Equations> Prelude.take 20 Traj
[[1.0, 1.0],
 [-0.30000000000000004, 0.0],
 [-0.30000000000000004, 0.30000000000000004],
 [-0.6900000000000002, 0.6000000000000001],
 [-1.4700000000000002, 1.2900000000000003],
 [-3.1470000000000007, 2.7600000000000007],
 [-6.735000000000001, 5.907000000000002],
 [-14.414100000000005, 12.642000000000003],
 [-30.848700000000008, 27.056100000000008],
 [-66.02163000000002, 57.904800000000016],
 [-141.29787000000005, 123.92643000000004],
 [-302.4022290000001, 265.2243000000001],
 [-647.1938190000002, 567.6265290000001],
 [-1385.1083067000004, 1214.8203480000002],
 [-2964.374759100001, 2599.9286547000006],
 [-6344.282010210001, 5564.303413800002],
 [-13577.876448150004, 11908.585424010003],
 [-29059.03749936301, 25486.461872160005],
 [-62191.437933171015, 54545.499371523016],
 [-133100.58711615094, 116736.93730469403]]
 --}