Clever Geek Handbook

Basic numbers in Idris

In idris 0.9.17.1,

with inspiration from https://wiki.haskell.org/Prime_numbers , I wrote the following code to generate prime numbers

module Main

concat: List a -> Stream a -> Stream a
concat [] ys = ys
concat (x :: xs) ys = x :: (concat xs ys)

generate: (Num a, Ord a) => (start:a) -> (step:a) -> (max:a) -> List a
generate start step max = if (start < max) then start :: generate (start + step) step max else []

mutual
  sieve: Nat -> Stream Int -> Int -> Stream Int
  sieve k (p::ps) x = concat (start) (sieve (k + 1) ps (p * p)) where
    fs: List Int
    fs = take k (tail primes)
    start: List Int
    start = [n | n <- (generate (x + 2) 2 (p * p - 2)), (all (\i => (n `mod` i) /= 0) fs)]

 primes: Stream Int
 primes = 2 :: 3 :: sieve 0 (tail primes) 3


main:IO()
main = do     
  printLn $ take 10 primes

In the REPL, if I write take 10 primes

, the REPL correctly shows[2, 3, 5, 11, 13, 17, 19, 29, 31, 37] : List Int

But if I try :exec

, nothing happens, and if I try to compile ans to execute the program, I getSegmentation fault: 11

Can someone help me debug this issue?

+3


source to share


1 answer


Your concat function can be made lazy to fix this. Just change its type to

concat : List a -> Lazy (Stream a) -> Stream a


This will do it.

Note: To get all the primes, change the <inside the generate function to <= (Currently some are missing, like 7 and 23).

+2


source






More articles:


All Articles