io.mlw 1.43 KB
Newer Older
1 2
module StdIO

3 4
  use string.Char
  (*i use string.String *)
5

6
  (** ghost references to represent the standard output *)
7 8 9 10
  use int.Int
  use list.List
  use list.Reverse
  use ref.Ref
MARCHE Claude's avatar
MARCHE Claude committed
11

12
  type prdata = PrChar char | PrInt int
MARCHE Claude's avatar
MARCHE Claude committed
13

14 15 16 17
  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
18

19 20 21 22 23
  (** 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) }
24

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
25 26
  (*i val print_string (s:string) : unit *)
  (*i prints a string on standard output. *)
27

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
28
  val print_int (n: int) : unit
MARCHE Claude's avatar
MARCHE Claude committed
29
    writes  { cur_pos, current_line }
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
30
  (** prints an integer, in decimal, on standard output. *)
31

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
32 33
  (*i val print_real (r:real) : unit *)
  (*i prints a real number on standard output. *)
34

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
35 36 37
  (*i val print_endline (s:string) : unit *)
  (*i prints a string, followed by a newline character, on standard output
      and flushes standard output. *)
38

39 40 41 42 43 44
  (** 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 }
45
    ensures { !flushed = Cons (reverse (old !current_line)) (old !flushed) }
46 47

end