You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
import std/text/parse
fun test(): parse char {
fun test2(): parse char {
char('r')
}
unsafe-no-div(test2)
}
pub fun main() {
val code = "hi"
val mb = parse(code.slice, test)
println("success")
}
I get a segmentation fault, even though test2 is of course not divergent at all. Replacing unsafe-no-div with unsafe-no-ndet also leads to a segfault, but replacing it with unsafe-total results in printing "success," presumably because it gets rid of the parse effect. All three unsafe functions are of course implemented the same way, except for their typing.
I of course understand that using these unsafe functions are, well, unsafe, but this behavior is so odd that I figured I'd make an issue about it just in case it's caused by an unknown compiler bug.
I also want to add that the reason I got into this experimentation to begin with was wanting to build a recursive parser using the parser combinator library, then realizing that I would have to add the "div" effect to everything I'd written even when I knew that the top-level function expr-parsing function (which was the only recursive one) wasn't divergent. I knew that in std, functions like for use the unsafe functions to get the looping they need without getting the "div" effect. I say all of this just to say that this didn't come out of mindless messing-around with koka but an actual project, hopefully to show that if this is a bug, it's not a too-remote edge case.
The text was updated successfully, but these errors were encountered:
I'm running into the same or very similar issue. In my case it doesn't matter if I use unsafe-no-div or unsafe-total, both will crash.
Here is an example. We define a take function which should turn a divergent iterator into a non-divergent one.
Furthermore, for some reason the to-list function also thinks it is divergent, requiring another unsafe-no-div there.
pub effect iter<a>
ctl yield(elem : a) : ()
pub fun to-list(it : () -> iter<a> ()) : list<a>
with unsafe-no-div()
var result := Nil
with fun yield(elem)
result := Cons(elem, result)
it()
reverse(result) // List was accumulated in reverse order
pub fun take(n : int, it : () -> <div,iter<a>> ()) : iter<a> ()
var count := 0
with ctl yield(elem)
if count < n then
yield(elem) // Forward the yield to our new iterator
count := count + 1
resume(())
else
()
with unsafe-no-div()
it()
And some test code
pub fun test-iter() : div list<int>
fun fib-iter(n1 : int, n2 : int) : <div,iter<int>> ()
val n3 = n1 + n2
yield(n3)
fib-iter(n2, n3)
to-list
take(100)
fib-iter(1,1)
When I run the following code:
I get a segmentation fault, even though
test2
is of course not divergent at all. Replacingunsafe-no-div
withunsafe-no-ndet
also leads to a segfault, but replacing it withunsafe-total
results in printing "success," presumably because it gets rid of the parse effect. All three unsafe functions are of course implemented the same way, except for their typing.I of course understand that using these unsafe functions are, well, unsafe, but this behavior is so odd that I figured I'd make an issue about it just in case it's caused by an unknown compiler bug.
I also want to add that the reason I got into this experimentation to begin with was wanting to build a recursive parser using the parser combinator library, then realizing that I would have to add the "div" effect to everything I'd written even when I knew that the top-level function expr-parsing function (which was the only recursive one) wasn't divergent. I knew that in std, functions like
for
use the unsafe functions to get the looping they need without getting the "div" effect. I say all of this just to say that this didn't come out of mindless messing-around with koka but an actual project, hopefully to show that if this is a bug, it's not a too-remote edge case.The text was updated successfully, but these errors were encountered: