io.mlw 1.35 KB
Newer Older
1 2 3 4 5 6

module StdIO

use import string.Char
(*i use import string.String *)

MARCHE Claude's avatar
MARCHE Claude committed
7 8 9 10 11 12 13 14 15 16 17 18
(** ghost references to represent the standard output *)
use import int.Int
use import list.List
use list.Reverse
use import ref.Ref

type prdata = PrChar char | PrInt int

val flushed : ref (list (list prdata))
val current_line : ref (list prdata)
val cur_pos : ref int
val cur_linenum: ref int
19 20

(** prints a character on standard output. *)
MARCHE Claude's avatar
MARCHE Claude committed
21 22 23 24
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) }
25 26 27 28 29 30 31 32 33 34 35 36 37 38

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

val print_int (n: int) : unit
(** prints an integer, in decimal, on standard output. *)

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

(*i val print_endline (s:string) : unit *)
(*i 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. *)
MARCHE Claude's avatar
MARCHE Claude committed
39 40 41 42 43 44
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.reverse (old !current_line)) (old !flushed) }
45 46 47 48 49

end