git.iko.soy/Idris-dev
on master help sign in
Fix totality of chr

It returns NUL if out of range, which is probably not ideal behaviour but is better than crashing. Fixes #2264. (Better in general would be to have a proof argument. One for later...)

commit521ef9b2eef8b21c5fa18ab1c8aca096982bde88 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 17 May 2015, 17:38 (11 years ago) parentcc865aa
4 files changed+13−8
compare with master
unifiedsplit
libs/prelude/Prelude/Bits.idr+1 libs/prelude/Prelude/Cast.idr+1−3 libs/prelude/Prelude/Chars.idr+10−4 src/Idris/Primitives.hs+1−1
libs/prelude/Prelude/Bits.idr+1
@@ -5,6 +5,7 @@ import Builtins
55import Prelude.Basics
66import Prelude.Bool
77import Prelude.Cast
8+import Prelude.Chars
89import Prelude.Classes
910import Prelude.Foldable
1011import Prelude.Nat
libs/prelude/Prelude/Cast.idr+1−3
@@ -1,5 +1,6 @@
11module Prelude.Cast
22
3+import Prelude.Bool
34import public Builtins
45
56||| Type class for transforming a instance of a data type to another type.
@@ -31,9 +32,6 @@ instance Cast Int Float where
3132instance Cast Int Integer where
3233 cast = prim__sextInt_BigInt
3334
34−instance Cast Int Char where
35− cast = prim__intToChar
36−
3735-- Float casts
3836
3937instance Cast Float String where
libs/prelude/Prelude/Chars.idr+10−4
@@ -1,14 +1,20 @@
1−module Prelude.Char
1+module Prelude.Chars
22-- Functions operating over Chars
33
44import Prelude.Bool
55import Prelude.Classes
66import Prelude.List
7+import Prelude.Cast
78import Builtins
89
910||| Return the ASCII representation of the character.
1011chr : Int -> Char
11−chr x = prim__intToChar x
12+chr x = if (x >= 0 && x < 0x11000)
13+ then assert_total (prim__intToChar x)
14+ else '\0'
15+
16+instance Cast Int Char where
17+ cast = chr
1218
1319||| Convert the number to its ASCII equivalent.
1420ord : Char -> Int
@@ -48,14 +54,14 @@ isNL x = x == '\r' || x == '\n'
4854||| Non-letters are ignored.
4955toUpper : Char -> Char
5056toUpper x = if (isLower x)
51− then (prim__intToChar (prim__charToInt x - 32))
57+ then assert_total (prim__intToChar (prim__charToInt x - 32))
5258 else x
5359
5460||| Convert a letter to the corresponding lower-case letter, if any.
5561||| Non-letters are ignored.
5662toLower : Char -> Char
5763toLower x = if (isUpper x)
58− then (prim__intToChar (prim__charToInt x + 32))
64+ then assert_total (prim__intToChar (prim__charToInt x + 32))
5965 else x
6066
6167||| Returns true if the character is a hexadecimal digit i.e. in the range [0-9][a-f][A-F]
src/Idris/Primitives.hs+1−1
@@ -124,7 +124,7 @@ primitives =
124124 Prim (sUN "prim__charToInt") (ty [(AType (ATInt ITChar))] (AType (ATInt ITNative))) 1 (c_charToInt)
125125 (1, LChInt ITNative) total,
126126 Prim (sUN "prim__intToChar") (ty [(AType (ATInt ITNative))] (AType (ATInt ITChar))) 1 (c_intToChar)
127− (1, LIntCh ITNative) total,
127+ (1, LIntCh ITNative) partial,
128128 Prim (sUN "prim__strToFloat") (ty [StrType] (AType ATFloat)) 1 (c_strToFloat)
129129 (1, LStrFloat) total,
130130 Prim (sUN "prim__floatToStr") (ty [(AType ATFloat)] StrType) 1 (c_floatToStr)