git.iko.soy/Idris-dev
on master help sign in
A few prelude functions/casts
commit80a2cee33910a2c18b18db108a48c3a7de0d73e6 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 27 Jul 2015, 11:55 (11 years ago) parent51bbaf9
4 files changed+23−6
compare with master
unifiedsplit
libs/base/Data/VectType.idr+1−1 libs/prelude/Prelude/Cast.idr+11−5 libs/prelude/Prelude/Nat.idr+3 libs/prelude/Prelude/Strings.idr+8
libs/base/Data/VectType.idr+1−1
@@ -1,6 +1,6 @@
11module Data.VectType
22
3−import Data.Fin
3+import public Data.Fin
44
55%access public
66%default total
libs/prelude/Prelude/Cast.idr+11−5
@@ -15,7 +15,7 @@ class Cast from to where
1515instance Cast String Int where
1616 cast = prim__fromStrInt
1717
18−instance Cast String Float where
18+instance Cast String Double where
1919 cast = prim__strToFloat
2020
2121instance Cast String Integer where
@@ -26,25 +26,31 @@ instance Cast String Integer where
2626instance Cast Int String where
2727 cast = prim__toStrInt
2828
29−instance Cast Int Float where
29+instance Cast Int Double where
3030 cast = prim__toFloatInt
3131
3232instance Cast Int Integer where
3333 cast = prim__sextInt_BigInt
3434
35−-- Float casts
35+-- Double casts
3636
37−instance Cast Float String where
37+instance Cast Double String where
3838 cast = prim__floatToStr
3939
40−instance Cast Float Int where
40+instance Cast Double Int where
4141 cast = prim__fromFloatInt
4242
43+instance Cast Double Integer where
44+ cast = prim__fromFloatBigInt
45+
4346-- Integer casts
4447
4548instance Cast Integer String where
4649 cast = prim__toStrBigInt
4750
51+instance Cast Integer Double where
52+ cast = prim__toFloatBigInt
53+
4854-- Char casts
4955
5056instance Cast Char Int where
libs/prelude/Prelude/Nat.idr+3
@@ -262,6 +262,9 @@ instance Cast Int Nat where
262262instance Cast Nat Int where
263263 cast = toIntNat
264264
265+instance Cast Nat Double where
266+ cast = cast . toIntegerNat
267+
265268--------------------------------------------------------------------------------
266269-- Auxilliary notions
267270--------------------------------------------------------------------------------
libs/prelude/Prelude/Strings.idr+8
@@ -305,6 +305,14 @@ unlines = pack . unlines' . map unpack
305305length : String -> Nat
306306length = fromInteger . prim__zextInt_BigInt . prim_lenString
307307
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+
308316||| Lowercases all characters in the string.
309317|||
310318||| ```idris example