stdlib/io.mlw

   1 (** {1 Basic I/O Functions} *)
   2
   3 module StdIO
   4
   5   use string.String
   6   use string.Char
   7   use int.Int
   8
   9   (** small trick so that printing vals are extracted to OCaml *)
  10   type t = private {ghost mutable foo:int}
  11   val ghost bar:t
  12
  13   (** prints a string to the standard output *)
  14   val print_string (s: string) : unit
  15     writes { bar }
  16
  17   (** prints a char to the standard output *)
  18   val print_char (c: char) : unit
  19     writes { bar }
  20
  21   (** prints a newline character to the standard output, and flushes it *)
  22   val print_newline (_u:unit) : unit
  23     writes { bar }
  24
  25   (** prints a Why3 int to the standard output *)
  26   val print_int (i: int) : unit
  27     writes { bar }
  28
  29   (***
  30   use int.Int
  31   use list.List
  32   use list.Reverse
  33   use ref.Ref
  34
  35   type prdata = PrChar char | PrInt int
  36
  37   (** ghost references to represent the standard output *)
  38   val ghost flushed : ref (list (list prdata))
  39   val ghost current_line : ref (list prdata)
  40   val ghost cur_pos : ref int
  41   val ghost cur_linenum: ref int
  42
  43   (** prints a character on standard output. *)
  44   val print_char (c:char) : unit
  45     writes  { cur_pos, current_line }
  46     ensures { !cur_pos = (old !cur_pos) + 1 }
  47     ensures { !current_line = Cons (PrChar c) (old !current_line) }
  48
  49   val print_string (s:string) : unit
  50   (** prints a string on standard output. *)
  51
  52   val print_int (n: int) : unit
  53     writes  { cur_pos, current_line }
  54   (** prints an integer, in decimal, on standard output. *)
  55
  56   val print_real (r:real) : unit
  57   (** prints a real number on standard output. *)
  58
  59   val print_endline (s:string) : unit
  60   (** prints a string, followed by a newline character, on standard output
  61       and flushes standard output. *)
  62
  63   (** prints a newline character on standard output, and flushes standard output. *)
  64   val print_newline (_u:unit) : unit
  65     writes  { cur_pos, current_line, cur_linenum, flushed }
  66     ensures { !cur_pos = 0 }
  67     ensures { !current_line = Nil }
  68     ensures { !cur_linenum = (old !cur_linenum) + 1 }
  69     ensures { !flushed = Cons (reverse (old !current_line)) (old !flushed) }
  70   *)
  71
  72 end