io.mlw

(** {1 Basic I/O Functions} *)

module StdIO

  use string.String
  use string.Char
  use int.Int

  (** small trick so that printing vals are extracted to OCaml *)
  type t = private {ghost mutable foo:int}
  val ghost bar:t

  (** prints a string to the standard output *)
  val print_string (s: string) : unit
    writes { bar }

  (** prints a char to the standard output *)
  val print_char (c: char) : unit
    writes { bar }

  (** prints a newline character to the standard output, and flushes it *)
  val print_newline (_u:unit) : unit
    writes { bar }

  (** prints a Why3 int to the standard output *)
  val print_int (i: int) : unit
    writes { bar }

  (***
  use int.Int
  use list.List
  use list.Reverse
  use ref.Ref

  type prdata = PrChar char | PrInt int

  (** ghost references to represent the standard output *)
  val ghost flushed : ref (list (list prdata))
  val ghost current_line : ref (list prdata)
  val ghost cur_pos : ref int
  val ghost cur_linenum: ref int

  (** prints a character on standard output. *)
  val print_char (c:char) : unit
    writes  { cur_pos, current_line }
    ensures { !cur_pos = (old !cur_pos) + 1 }
    ensures { !current_line = Cons (PrChar c) (old !current_line) }

  val print_string (s:string) : unit
  (** prints a string on standard output. *)

  val print_int (n: int) : unit
    writes  { cur_pos, current_line }
  (** prints an integer, in decimal, on standard output. *)

  val print_real (r:real) : unit
  (** prints a real number on standard output. *)

  val print_endline (s:string) : unit
  (** prints a string, followed by a newline character, on standard output
      and flushes standard output. *)

  (** prints a newline character on standard output, and flushes standard output. *)
  val print_newline (_u:unit) : unit
    writes  { cur_pos, current_line, cur_linenum, flushed }
    ensures { !cur_pos = 0 }
    ensures { !current_line = Nil }
    ensures { !cur_linenum = (old !cur_linenum) + 1 }
    ensures { !flushed = Cons (reverse (old !current_line)) (old !flushed) }
  *)

end