(*
  This is the translation of an example from

    First-Class Structures for Standard ML
    Claudio Russo
    ICFP 1999
  
  based on an example in

    Abstract Types have Existential Type
    John C. Mitchell and Gordon D. Plotkin
    ACM Transactions on Programming Languages and Systems 10(3):470-502, July 1988.
*)
module Russo =
struct
  (* An abstract type of integer streams *)
  module type Stream =
  sig
    type state
    val start : state
    val next  : state -> state
    val value : state -> int
  end

  (* An instance of the stream abstract type: the natural numbers starting from 2 *)
  module TwoOnwards : Stream =
  struct
    type state = int
    let start = 2
    let next = fun (i:int) -> succ i
    let value = fun (i:int) -> i
  end

  (* In this implementation of the Sieve of Eratosthenes, the state is
     a stream and the initial state is the stream of natural numbers
     starting from 2 *)
  module type State = Stream
  module Start = (TwoOnwards : State)

  (* One step of the algorithm. *)
  module Next (S:State) : State =
  struct
    type state = S.state
    let rec filter : state -> state =
      fun (s:state) ->
        if (S.value s) mod (S.value S.start) = 0
        then filter (S.next s)
        else s
    let start = filter S.start
    let next = fun (s:state) -> filter (S.next s)
    let value = S.value
  end
    
  (* The sieve, a stream of streams:

        TwoOnwards, Next(TwoOnwards), Next(Next(TwoOnwards)), ...
  *)
  module Sieve : Stream =
  struct
    type state = (module Stream)
    let start = (module TwoOnwards : Stream)
    let next = fun (s:state) ->
                 let module S = (val s : Stream) in
                   (module Next(S) : Stream)
    let value = fun (s:state) ->
                  let module S = (val s : Stream) in
                    S.value S.start
  end
    
  (* The nth state of the sieve algorithm *)
  let rec nthstate : int -> Sieve.state = 
    fun (n:int) ->
      if n = 0
      then Sieve.start
      else Sieve.next (nthstate (pred n))

  (* The nth prime (where 2 is the zeroth) *)
  let nthprime = fun (n:int) -> Sieve.value (nthstate n)
end


(* This is a mechanical translation of Russo's stream example into
   OCaml using polymorphic record fields and the well-known encoding
   of existentials using universals.  The benefits of first-class
   modules over polymorphism are relatively limited here: they're
   neater notationally, but not really any more powerful for this
   example.
*)
module Russo_polymorphism =
struct
  (* An abstract type of integer streams *)

  type 'state stream_ops = {
    start : 'state;
    next  : 'state -> 'state;
    value : 'state -> int;
  }
  type 'ctxt stream_cont = {
    streamk : 'state. 'state stream_ops -> 'ctxt
  }
  type stream  = {
    stream : 'ctxt. 'ctxt stream_cont -> 'ctxt 
  }

  (* An instance of the stream abstract type: the natural numbers starting from 2 *)
  let two_onwards : stream = {
    stream = fun k -> k.streamk {
      start = 2;
      next = (fun (i:int) -> succ i);
      value = (fun (i:int) -> i);
    }
  }

  (* In our implementation of the Sieve of Eratosthenes, the state is a
     stream and the initial state is the stream of natural numbers
     starting from 2 *)
  type state = stream
  let start : state = two_onwards

  (* One step of the algorithm. *)
  let next ss =
    ss.stream {
      streamk = 
        fun { start = s_start; next = s_next; value = s_value; } ->
          let rec filter =
            fun s ->
              if (s_value s) mod (s_value s_start) = 0
              then filter (s_next s)
              else s in
            {
              stream = fun k -> k.streamk {
                start = filter s_start;
                next = (fun s -> filter (s_next s));
                value = s_value;
              }
            }
    }

  (* The sieve:

        two_onwards, next(two_onwards), next(next(two_onwards)), ...
  *)
  module Sieve =
  struct
    type state = stream
    let start = (two_onwards : stream)
    let next = fun (s:state) -> next s
    let value = fun (s:state) -> s.stream { streamk = fun { start; value } -> value start }
  end
    
  (* The nth state of the sieve algorithm *)
  let rec nthstate : int -> Sieve.state = 
    fun (n:int) ->
      if n = 0
      then Sieve.start
      else Sieve.next (nthstate (pred n))

  (* The nth prime (where 2 is the zeroth) *)
  let nthprime = fun (n:int) -> Sieve.value (nthstate n)
end


(* First class modules also make it possible to encode higher-kinded
   existential types, which can *not* be encoded using polymorphic
   records in OCaml.  In particular, it doesn't seems to be possible
   to express the `map' function of the following stream type using
   the encoding based on polymorphic records. *)
module Parameterised_existentials =
struct
  (* The operations of the stream interface *) 
  (*
    ∃(t :: ∗ -> ∗){
      head : ∀α. α t → α,
      tail : ∀α. α t → α t,
      from : ∀α. (int → α) → α t,
      map  : ∀α β. (α → β) → α t → β t
    }
  *)
  module type StreamOps =
  sig
    type 'a t
    val head : 'a t -> 'a
    val tail : 'a t -> 'a t
    val from : (int -> 'a) -> 'a t
    val map  : ('a -> 'b) -> 'a t -> 'b t
  end

  (* The type of a stream value.  We'll expose the type of elements
     ('a'), but leave the type of streams ('t') abstract. *)
  module type Stream =
  sig
    type a
    include StreamOps
    val stream : a t
  end

  (* A convenient shorthand for the type of stream values *)
  type 'a stream = (module Stream with type a = 'a)

  (* An implementation of streams as cons cells with lazy tails *)
  module LazyStream : StreamOps =
  struct
    type 'a t = Cons of 'a * 'a t Lazy.t
    let head (Cons (h, _)) = h
    let tail (Cons (_, lazy t)) = t
    let from f =
      let rec mk n = Cons (f n, lazy (mk (n + 1))) in
        mk 0
    let rec map f (Cons (h, lazy t)) = Cons (f h, lazy (map f t))
  end

  (* An implementation of streams as functions *)
  module FunctionalStream : StreamOps =
  struct
    type 'a t = int -> 'a
    let head s = s 0
    let tail s = fun n -> s (n + 1)
    let from f = f
    let map f s = fun n -> f (s n)
  end

  (* Create a stream from an implementation of the interface and an indexing function *)
  let mk_stream : 'a.(module StreamOps) -> (int -> 'a) -> 'a stream
    = fun (type s) ops f ->
      (module 
       struct
         type a = s
         include (val ops : StreamOps)
         let stream = from f
       end : Stream with type a = s)

  (* Expose the map function as a standalone value. *)
  let map : 'a. ('a -> 'b) -> 'a stream -> 'b stream =
    fun (type s) (type t) f stream -> 
      let module Stream = (val stream : Stream with type a = s) in
        (module
         struct
           type a = t
           include (Stream : StreamOps with type 'a t = 'a Stream.t)
           let stream = Stream.map f Stream.stream
         end : Stream with type a = t)
end