idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

[ refactor ] more efficient implementation of range

Browse Source
This commit is contained in:
Guillaume ALLAIS 2021-03-29 23:01:56 +01:00 committed by G. Allais
parent f255026d1b
commit 09d8e25441
1 changed files with 24 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
libs/base/Data/Vect.idr
View File

@ -1,5 +1,6 @@
module Data.Vect
import Data.DPair
import Data.List
import Data.Nat
import public Data.Fin
@ -755,10 +756,29 @@ diag : Vect len (Vect len elem) -> Vect len elem
diag [] = []
diag ((x::xs)::xss) = x :: diag (map tail xss)
public export
range : {len : Nat} -> Vect len (Fin len)
range {len=Z} = []
range {len=S _} = FZ :: map FS range
namespace Fin
public export
tabulate : {len : Nat} -> (Fin len -> a) -> Vect len a
tabulate {len = Z} f = []
tabulate {len = S _} f = f FZ :: tabulate (f . FS)
public export
range : {len : Nat} -> Vect len (Fin len)
range = tabulate id
namespace Subset
public export
tabulate : {len : Nat} -> (Subset Nat (`LT` len) -> a) -> Vect len a
tabulate {len = Z} f = []
tabulate {len = S _} f
= f (Element Z ltZero)
:: Subset.tabulate (\ (Element n prf) => f (Element (S n) (LTESucc prf)))
public export
range : {len : Nat} -> Vect len (Subset Nat (`LT` len))
range = tabulate id
--------------------------------------------------------------------------------
-- Zippable