mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-27 10:41:08 +03:00
parent
19bcefb25e
commit
560449e087
1
dist/rts/idris_rts.c
vendored
1
dist/rts/idris_rts.c
vendored
@ -572,6 +572,7 @@ VAL idris_concat(VM* vm, VAL l, VAL r) {
|
||||
String * cl = allocStr(vm, llen + rlen, 0);
|
||||
memcpy(cl->str, ls, llen);
|
||||
memcpy(cl->str + llen, rs, rlen);
|
||||
cl->str[llen+rlen] = '\0';
|
||||
return (VAL)cl;
|
||||
}
|
||||
|
||||
|
2
dist/rts/idris_utf8.c
vendored
2
dist/rts/idris_utf8.c
vendored
@ -105,7 +105,7 @@ char* idris_utf8_advance(char* str, int i) {
|
||||
|
||||
int idris_utf8_findOffset(char* str, int i) {
|
||||
int offset = 0;
|
||||
while(i > 0) {
|
||||
while(i > 0 && str != '\0') {
|
||||
int len = idris_utf8_charlen(str);
|
||||
str+=len;
|
||||
offset+=len;
|
||||
|
@ -1065,8 +1065,12 @@ reverse = prim__strReverse
|
||||
||| @ subject The string to return a portion of
|
||||
public export
|
||||
substr : (index : Nat) -> (len : Nat) -> (subject : String) -> String
|
||||
substr s e = prim__strSubstr (prim__cast_IntegerInt (natToInteger s))
|
||||
(prim__cast_IntegerInt (natToInteger e))
|
||||
substr s e subj
|
||||
= if s < length subj
|
||||
then prim__strSubstr (prim__cast_IntegerInt (natToInteger s))
|
||||
(prim__cast_IntegerInt (natToInteger e))
|
||||
subj
|
||||
else ""
|
||||
|
||||
||| Adds a character to the front of the specified string.
|
||||
|||
|
||||
|
@ -41,7 +41,9 @@
|
||||
(b (max 0 off))
|
||||
(x (max 0 len))
|
||||
(end (min l (+ b x))))
|
||||
(substring s b end)))
|
||||
(if (> b l)
|
||||
""
|
||||
(substring s b end))))
|
||||
|
||||
(define either-left
|
||||
(lambda (x)
|
||||
|
Loading…
Reference in New Issue
Block a user