mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
73 lines
2.0 KiB
Plaintext
73 lines
2.0 KiB
Plaintext
(** {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
|