mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-25 12:42:02 +03:00
Merge pull request #896 from Russoul/toString-iterators
Add withIteratorString
This commit is contained in:
commit
efae2682bd
@ -32,6 +32,17 @@ export
|
||||
withString : (str : String) -> ((it : StringIterator str) -> a) -> a
|
||||
withString str f = f (fromString str)
|
||||
|
||||
||| Runs the action `f` on the slice `res` of the original string `str` represented by the
|
||||
||| iterator `it`
|
||||
%foreign
|
||||
"scheme:blodwen-string-iterator-to-string"
|
||||
"javascript:stringIterator:toString"
|
||||
export
|
||||
withIteratorString : (str : String)
|
||||
-> (1 it : StringIterator str)
|
||||
-> (f : (res : String) -> a)
|
||||
-> a
|
||||
|
||||
-- We use a custom data type instead of Maybe (Char, StringIterator)
|
||||
-- to remove one level of pointer indirection
|
||||
-- in every iteration of something that's likely to be a hot loop,
|
||||
|
@ -64,19 +64,16 @@ addStringIteratorToPreamble =
|
||||
do
|
||||
let defs = "
|
||||
function __prim_stringIteratorNew(str) {
|
||||
return str[Symbol.iterator]();
|
||||
return 0;
|
||||
}
|
||||
function __prim_stringIteratorToString(_, str, it, f) {
|
||||
return f(str.slice(it));
|
||||
}
|
||||
function __prim_stringIteratorNext(str, it) {
|
||||
const char = it.next();
|
||||
if (char.done) {
|
||||
return {h: 0}; // EOF
|
||||
} else {
|
||||
return {
|
||||
h: 1, // Character
|
||||
a1: char.value,
|
||||
a2: it
|
||||
};
|
||||
}
|
||||
if (it >= str.length)
|
||||
return {h: 0};
|
||||
else
|
||||
return {h: 1, a1: str.charAt(it), a2: it + 1};
|
||||
}"
|
||||
let name = "stringIterator"
|
||||
let newName = esName name
|
||||
@ -332,7 +329,8 @@ makeForeign n x =
|
||||
case def of
|
||||
"new" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorNew;\n"
|
||||
"next" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorNext;\n"
|
||||
_ => throw (InternalError $ "invalid string iterator function: " ++ def ++ ", supported functions are \"new\", \"next\"")
|
||||
"toString" => pure $ "const " ++ jsName n ++ " = __prim_stringIteratorToString;\n"
|
||||
_ => throw (InternalError $ "invalid string iterator function: " ++ def ++ ", supported functions are \"new\", \"next\", \"toString\"")
|
||||
|
||||
|
||||
_ => throw (InternalError $ "invalid foreign type : " ++ ty ++ ", supported types are \"lambda\", \"support\"")
|
||||
|
@ -89,6 +89,9 @@
|
||||
(define (blodwen-string-iterator-new s)
|
||||
0)
|
||||
|
||||
(define (blodwen-string-iterator-to-string _ s ofs f)
|
||||
(f (substring s ofs (string-length s))))
|
||||
|
||||
(define (blodwen-string-iterator-next s ofs)
|
||||
(if (>= ofs (string-length s))
|
||||
(vector 0) ; EOF
|
||||
|
@ -101,6 +101,9 @@
|
||||
(define (blodwen-string-iterator-new s)
|
||||
0)
|
||||
|
||||
(define (blodwen-string-iterator-to-string _ s ofs f)
|
||||
(f (substring s ofs (string-length s))))
|
||||
|
||||
(define (blodwen-string-iterator-next s ofs)
|
||||
(if (>= ofs (string-length s))
|
||||
(vector 0) ; EOF
|
||||
|
@ -80,6 +80,9 @@
|
||||
(define (blodwen-string-iterator-new s)
|
||||
0)
|
||||
|
||||
(define (blodwen-string-iterator-to-string _ s ofs f)
|
||||
(f (substring s ofs (string-length s))))
|
||||
|
||||
(define (blodwen-string-iterator-next s ofs)
|
||||
(if (>= ofs (string-length s))
|
||||
(vector 0) ; EOF
|
||||
|
Loading…
Reference in New Issue
Block a user