(* * * * * * * * * * *
 * Resource Aware ML *
 * * * * * * * * * * *
 *
 * File:
 *   eratosthenes.raml
 *
 * Author:
 *   Jan Hoffmann (2009)
 *
 * Resource Bound:
 *   O(n^2)
 *
 * Description: 
 *   The Sieve of Eratosthenes.  A nice and simple way to compute prime
 *   numbers.  See for example
 *   http://en.wikipedia.org/wiki/Sieve_of_Eratosthenes.
 *)


eratos : L(int) -> L(int)

eratos l = let _=tick(1) in
            match l with
               | nil -> nil
               | (x::xs) -> x::eratos(filter(x,xs)) ;
(*
eq(eratos(A),1,[],[A=0]).
eq(eratos(A),1,[eratos(As),filter(X,As)],[A>=1,As=A-1]). % %%out_filter(A,B) = B
*)
 filter: (int,L(int)) -> L(int)
 (* Destructive!*)
 
 filter(p,l) =  let _=tick(1) in
                matchD l with
                | nil -> nil
                | (x::xs) -> let xs' = filter(p,xs) in
                             if x mod p == 0 then xs' else x::xs';
(*
eq(out_filter(A,B),0,[],[B=0]).
eq(out_filter(A,B),0,[out_filter(A,Bs)],[B>=1,Bs = B-1]).
eq(out_filter(A,B),1,[out_filter(A,Bs)],[B>=1,Bs = B-1]).

eq(filter(A,B),1,[],[B=0]).
eq(filter(A,B),1,[filter(A,Bs)],[B>=1,Bs = B-1]).
*)

main =()