git.iko.soy/Idris-dev
on master help sign in
A few prelude functions/casts
80a2ceeEdwin Brady
libs/base/Data/VectType.idr+1−1
compare with master
unifiedsplit
@@ -1,6 +1,6 @@
1module Data.VectType
1module Data.VectType
2
2
3−import Data.Fin
3+import public Data.Fin
4
4
5%access public
5%access public
6%default total
6%default total
libs/prelude/Prelude/Cast.idr+11−5
@@ -15,7 +15,7 @@ class Cast from to where
15instance Cast String Int where
15instance Cast String Int where
16 cast = prim__fromStrInt
16 cast = prim__fromStrInt
17
17
18−instance Cast String Float where
18+instance Cast String Double where
19 cast = prim__strToFloat
19 cast = prim__strToFloat
20
20
21instance Cast String Integer where
21instance Cast String Integer where
@@ -26,25 +26,31 @@ instance Cast String Integer where
26instance Cast Int String where
26instance Cast Int String where
27 cast = prim__toStrInt
27 cast = prim__toStrInt
28
28
29−instance Cast Int Float where
29+instance Cast Int Double where
30 cast = prim__toFloatInt
30 cast = prim__toFloatInt
31
31
32instance Cast Int Integer where
32instance Cast Int Integer where
33 cast = prim__sextInt_BigInt
33 cast = prim__sextInt_BigInt
34
34
35−-- Float casts
35+-- Double casts
36
36
37−instance Cast Float String where
37+instance Cast Double String where
38 cast = prim__floatToStr
38 cast = prim__floatToStr
39
39
40−instance Cast Float Int where
40+instance Cast Double Int where
41 cast = prim__fromFloatInt
41 cast = prim__fromFloatInt
42
42
43+instance Cast Double Integer where
44+ cast = prim__fromFloatBigInt
45+
43-- Integer casts
46-- Integer casts
44
47
45instance Cast Integer String where
48instance Cast Integer String where
46 cast = prim__toStrBigInt
49 cast = prim__toStrBigInt
47
50
51+instance Cast Integer Double where
52+ cast = prim__toFloatBigInt
53+
48-- Char casts
54-- Char casts
49
55
50instance Cast Char Int where
56instance Cast Char Int where
libs/prelude/Prelude/Nat.idr+3
@@ -262,6 +262,9 @@ instance Cast Int Nat where
262instance Cast Nat Int where
262instance Cast Nat Int where
263 cast = toIntNat
263 cast = toIntNat
264
264
265+instance Cast Nat Double where
266+ cast = cast . toIntegerNat
267+
265--------------------------------------------------------------------------------
268--------------------------------------------------------------------------------
266-- Auxilliary notions
269-- Auxilliary notions
267--------------------------------------------------------------------------------
270--------------------------------------------------------------------------------
libs/prelude/Prelude/Strings.idr+8
@@ -305,6 +305,14 @@ unlines = pack . unlines' . map unpack
305length : String -> Nat
305length : String -> Nat
306length = fromInteger . prim__zextInt_BigInt . prim_lenString
306length = fromInteger . prim__zextInt_BigInt . prim_lenString
307
307
308+||| Returns a substring of a given string
309+||| @index The (zero based) index of the string to extract. If this is
310+||| beyond the end of the String, the function returns the empty string.
311+||| @len The desired length of the substring. Truncated if this exceeds
312+||| the length of the input.
313+substr : (index : Nat) -> (len : Nat) -> String -> String
314+substr i len = pack . List.take len . drop i . unpack
315+
308||| Lowercases all characters in the string.
316||| Lowercases all characters in the string.
309|||
317|||
310||| ```idris example
318||| ```idris example