From 963f27384febc7ad2af7c719562ae8b835f83205 Mon Sep 17 00:00:00 2001
From: Kiana Sheibani <kiana.a.sheibani@gmail.com>
Date: Sun, 28 Apr 2024 00:30:52 -0400
Subject: [PATCH] Remove believe_me calls blocking evaluation

---
 src/Data/NumIdr.idr                   |  1 +
 src/Data/NumIdr/Matrix.idr            |  7 ++++---
 src/Data/NumIdr/PrimArray/Delayed.idr |  5 +++--
 src/Data/NumIdr/PrimArray/Linked.idr  | 14 ++++++++++----
 src/Data/NumIdr/Vector.idr            |  3 ++-
 5 files changed, 20 insertions(+), 10 deletions(-)

diff --git a/src/Data/NumIdr.idr b/src/Data/NumIdr.idr
index 9634f05..8351d86 100644
--- a/src/Data/NumIdr.idr
+++ b/src/Data/NumIdr.idr
@@ -2,6 +2,7 @@ module Data.NumIdr
 
 import public Data.Permutation
 
+import Data.NumIdr.PrimArray
 import public Data.NumIdr.Interfaces
 import public Data.NumIdr.Array
 import public Data.NumIdr.Scalar
diff --git a/src/Data/NumIdr/Matrix.idr b/src/Data/NumIdr/Matrix.idr
index 0d7be3b..9a43a44 100644
--- a/src/Data/NumIdr/Matrix.idr
+++ b/src/Data/NumIdr/Matrix.idr
@@ -168,7 +168,8 @@ diagonal {n} mat with (viewShape mat)
 export
 -- TODO: throw an actual proof in here to avoid the unsafety
 minor : Fin (S m) -> Fin (S n) -> Matrix (S m) (S n) a -> Matrix m n a
-minor i j mat = believe_me $ mat!!..[Filter (/=i), Filter (/=j)]
+minor i j mat = replace {p = flip Array a} (believe_me $ Refl {x = ()})
+  $ mat!!..[Filter (/=i), Filter (/=j)]
 
 
 filterInd : Num a => (Nat -> Nat -> Bool) -> Matrix m n a -> Matrix m n a
@@ -568,7 +569,7 @@ solveLowerTri' {n} mat b with (viewShape b)
     construct {i=S i} (b :: bs) =
       let xs = construct bs
           i' = assert_total $ case natToFin i n of Just i' => i'
-      in (b - sum (zipWith (*) xs (reverse $ toVect $ believe_me $
+      in (b - sum (zipWith (*) xs (reverse $ toVect $ replace {p = flip Array a} (believe_me $ Refl {x=()}) $
                   mat !!.. [One i', EndBound (weaken i')]))) / mat!#[i,i] :: xs
 
 
@@ -581,7 +582,7 @@ solveUpperTri' {n} mat b with (viewShape b)
     construct i (b :: bs) =
       let xs = construct (S i) bs
           i' = assert_total $ case natToFin i n of Just i' => i'
-      in (b - sum (zipWith (*) xs (toVect $ believe_me $
+      in (b - sum (zipWith (*) xs (toVect $ replace {p = flip Array a} (believe_me $ Refl {x=()}) $
                   mat !!.. [One i', StartBound (FS i')]))) / mat!#[i,i] :: xs
 
 
diff --git a/src/Data/NumIdr/PrimArray/Delayed.idr b/src/Data/NumIdr/PrimArray/Delayed.idr
index e90ae86..a3c2e04 100644
--- a/src/Data/NumIdr/PrimArray/Delayed.idr
+++ b/src/Data/NumIdr/PrimArray/Delayed.idr
@@ -4,6 +4,7 @@ import Data.List
 import Data.Vect
 import Data.NumIdr.Array.Rep
 import Data.NumIdr.Array.Coords
+import Data.NumIdr.PrimArray.Linked
 
 %default total
 
@@ -21,8 +22,8 @@ export
 indexRange : {s : _} -> (rs : CoordsRange s) -> PrimArrayDelayed s a -> PrimArrayDelayed (newShape rs) a
 indexRange [] v = v
 indexRange (r :: rs) v with (cRangeToList r)
-  _ | Left i = indexRange rs (\is' => v (believe_me i :: is'))
-  _ | Right is = \(i::is') => indexRange rs (\is'' => v (believe_me (Vect.index i (fromList is)) :: is'')) is'
+  _ | Left i = indexRange rs (\is' => v (assertFin i :: is'))
+  _ | Right is = \(i::is') => indexRange rs (\is'' => v (assertFin (Vect.index i (fromList is)) :: is'')) is'
 
 export
 indexSetRange : {s : _} -> (rs : CoordsRange s) -> PrimArrayDelayed (newShape rs) a
diff --git a/src/Data/NumIdr/PrimArray/Linked.idr b/src/Data/NumIdr/PrimArray/Linked.idr
index 1fbce1b..35a8712 100644
--- a/src/Data/NumIdr/PrimArray/Linked.idr
+++ b/src/Data/NumIdr/PrimArray/Linked.idr
@@ -23,19 +23,25 @@ update : Coords s -> (a -> a) -> Vects s a -> Vects s a
 update [] f v = f v
 update (i :: is) f v = updateAt i (update is f) v
 
+export %unsafe
+assertFin : Nat -> Fin n
+assertFin n = natToFinLt n @{believe_me Oh}
+
 export
 indexRange : {s : _} -> (rs : CoordsRange s) -> Vects s a -> Vects (newShape rs) a
 indexRange [] v = v
 indexRange (r :: rs) v with (cRangeToList r)
-  _ | Left i = indexRange rs (Vect.index (believe_me i) v)
-  _ | Right is = believe_me $ map (\i => indexRange rs (Vect.index (believe_me i) v)) is
+  _ | Left i = indexRange rs (Vect.index (assertFin i) v)
+  _ | Right is = assert_total $
+        case toVect _ (map (\i => indexRange rs (Vect.index (assertFin i) v)) is) of
+          Just v => v
 
 export
 indexSetRange : {s : _} -> (rs : CoordsRange s) -> Vects (newShape rs) a -> Vects s a -> Vects s a
 indexSetRange {s=[]} [] rv _ = rv
 indexSetRange {s=_::_} (r :: rs) rv v with (cRangeToList r)
-  _ | Left i = updateAt (believe_me i) (indexSetRange rs rv) v
-  _ | Right is = foldl (\v,i => updateAt (believe_me i) (indexSetRange rs (Vect.index (believe_me i) rv)) v) v is
+  _ | Left i = updateAt (assertFin i) (indexSetRange rs rv) v
+  _ | Right is = foldl (\v,i => updateAt (assertFin i) (indexSetRange rs (Vect.index (assertFin i) rv)) v) v is
 
 
 export
diff --git a/src/Data/NumIdr/Vector.idr b/src/Data/NumIdr/Vector.idr
index 0ca6de3..7f28638 100644
--- a/src/Data/NumIdr/Vector.idr
+++ b/src/Data/NumIdr/Vector.idr
@@ -40,7 +40,8 @@ vector v = rewrite sym (lengthCorrect v)
 ||| Convert a vector into a `Vect`.
 export
 toVect : Vector n a -> Vect n a
-toVect v = believe_me $ Vect.fromList $ Prelude.toList v
+toVect v = replace {p = flip Vect a} (believe_me $ Refl {x=()}) $
+  Vect.fromList $ Prelude.toList v
 
 ||| Return the `i`-th basis vector.
 export