idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-21 02:31:50 +03:00
Code Issues Projects Releases Wiki Activity

[ cleanup ] remove 1 suffix from Vector1 functions

Browse Source
This commit is contained in:
Justus Matthiesen 2023-11-02 10:54:20 +00:00 committed by Justus Matthiesen
parent 291d60da08
commit 39f3aeeb08
2 changed files with 12 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Core/Termination/SizeChange.idr
View File

@ -217,7 +217,7 @@ checkNonDesc : Graph -> Maybe Graph
checkNonDesc a = if any selfDecArc a.change then Nothing else Just a checkNonDesc a = if any selfDecArc a.change then Nothing else Just a
where where
selfDecArc : (Nat, Vector1 SizeChange) -> Bool selfDecArc : (Nat, Vector1 SizeChange) -> Bool
selfDecArc (i, xs) = lookupOrd1 i xs == Just Smaller selfDecArc (i, xs) = lookupOrd i xs == Just Smaller
||| Finding non-terminating loops ||| Finding non-terminating loops
findLoops : SCSet -> findLoops : SCSet ->

22
src/Libraries/Data/SparseMatrix.idr
View File

@ -76,28 +76,28 @@ namespace Vector1
Vector1 a = List1 (Nat, a) Vector1 a = List1 (Nat, a)
export export
fromList1 : (Eq a, Semiring a) => List a -> Maybe (Vector1 a) fromList : (Eq a, Semiring a) => List a -> Maybe (Vector1 a)
fromList1 = Data.List1.fromList . Vector.fromList fromList = Data.List1.fromList . Vector.fromList
export export
insert1 : Nat -> a -> Vector1 a -> Vector1 a insert : Nat -> a -> Vector1 a -> Vector1 a
insert1 i x ys@((j, y) ::: ys') = insert i x ys@((j, y) ::: ys') =
case compare i j of case compare i j of
LT => (i, x) ::: (j, y) :: ys' LT => (i, x) ::: (j, y) :: ys'
EQ => ys -- keep EQ => ys -- keep
GT => (j, y) ::: insert i x ys' GT => (j, y) ::: insert i x ys'
export export
lookupOrd1 : Ord k => k -> List1 (k, a) -> Maybe a lookupOrd : Ord k => k -> List1 (k, a) -> Maybe a
lookupOrd1 i ((k, x) ::: xs) = lookupOrd i ((k, x) ::: xs) =
case compare i k of case compare i k of
LT => Nothing LT => Nothing
EQ => Just x EQ => Just x
GT => lookupOrd i xs GT => lookupOrd i xs
export export
maxIndex1 : Vector1 a -> Nat maxIndex : Vector1 a -> Nat
maxIndex1 ((i, x) ::: xs) = maybe i fst (last' xs) maxIndex ((i, x) ::: xs) = maybe i fst (last' xs)
||| A sparse matrix is a sparse vector of (non-empty) sparse vectors. ||| A sparse matrix is a sparse vector of (non-empty) sparse vectors.
public export public export
@ -106,7 +106,7 @@ Matrix a = Vector (Vector1 a)
export export
fromListList : (Eq a, Semiring a) => List (List a) -> Matrix a fromListList : (Eq a, Semiring a) => List (List a) -> Matrix a
fromListList = mapMaybe (\(i, xs) => map (i,) (fromList1 xs)) . withIndex fromListList = mapMaybe (\(i, xs) => map (i,) (Vector1.fromList xs)) . withIndex
where where
-- may contain empty lists -- may contain empty lists
withIndex : List (List a) -> List (Nat, List a) withIndex : List (List a) -> List (Nat, List a)
@ -126,7 +126,7 @@ transpose ((i, xs) :: xss) = spreadHeads i (toList xs) (transpose xss) where
spreadHeads i xs@((j, x) :: xs') yss@((j', ys) :: yss') = spreadHeads i xs@((j, x) :: xs') yss@((j', ys) :: yss') =
case compare j j' of case compare j j' of
LT => (j, singleton (i,x)) :: spreadHeads i xs' yss LT => (j, singleton (i,x)) :: spreadHeads i xs' yss
EQ => (j', insert1 i x ys) :: spreadHeads i xs' yss' EQ => (j', insert i x ys) :: spreadHeads i xs' yss'
GT => (j', ys) :: spreadHeads i xs yss' GT => (j', ys) :: spreadHeads i xs yss'
multRow : (Eq a, Semiring a) => Matrix a -> Vector1 a -> Vector a multRow : (Eq a, Semiring a) => Matrix a -> Vector1 a -> Vector a
@ -152,7 +152,7 @@ mult = multTranspose . transpose
||| Find largest column index. ||| Find largest column index.
maxIndexInner : Matrix a -> Nat maxIndexInner : Matrix a -> Nat
maxIndexInner = foldMap @{%search} @{MkMonoid @{MkSemigroup max} 0} (maxIndex1 . snd) maxIndexInner = foldMap @{%search} @{MkMonoid @{MkSemigroup max} 0} (maxIndex . snd)
namespace Pretty namespace Pretty
header : (columnWidth : Int) -> (rowLength : Nat) -> List (Doc ann) header : (columnWidth : Int) -> (rowLength : Nat) -> List (Doc ann)