Commit 0dbc9ed9 authored by MARCHE Claude's avatar MARCHE Claude

Attempt to add a module for Input/Output

parent b618fbf3
......@@ -247,3 +247,18 @@ module mach.array.Array31
syntax val self_blit "Array.blit"
end
module string.Char
syntax type char "Pervasives.char"
syntax val chr "Why3__BigInt.chr"
syntax val code "Why3__BigInt.code"
syntax function uppercase "Char.uppercase"
syntax function lowercase "Char.lowercase"
end
module io.StdIO
syntax val print_char "Pervasives.print_char"
syntax val print_int "Why3__BigInt.print"
syntax val print_newline "Pervasives.print_newline"
end
......@@ -168,9 +168,15 @@ module Euler001
let n15 = div (n-1) 15 in
div (3 * n3 * (n3+1) + 5 * n5 * (n5+1) - 15 * n15 * (n15+1)) 2
(** Small test. Run it with
why3 examples/euler001.mlw --exec Euler001.run
*)
let run () = solve 1000
(* should return 233168 *)
(** for the Why3 bench *)
exception BenchFailure
let bench () raises { BenchFailure -> true } =
......@@ -178,4 +184,17 @@ module Euler001
if x <> 233168 then raise BenchFailure;
x
(** for extraction *)
use import string.Char
use import io.StdIO
let go () =
print_char (chr 71); (* G *)
print_char (chr 79); (* O *)
print_char (chr 58); (* : *)
print_char (chr 32); (* *)
print_int (run ());
print_newline ()
end
......@@ -5,7 +5,11 @@ ifeq ($(BENCH),yes)
WHY3=../../bin/why3
WHY3SHARE=../../share
else
WHY3=$(BINDIR)/why3
ifeq ($(BINDIR),)
WHY3=why3
else
WHY3=$(BINDIR)/why3
endif
WHY3SHARE=$(shell $(WHY3) --print-datadir)
endif
......
......@@ -11,6 +11,12 @@ let input =
if Array.length Sys.argv <> 2 then usage ();
Sys.argv.(1)
let () =
if input = "go" then begin
Euler001__Euler001.go ();
exit 0
end
let input_num =
try
Why3__BigInt.of_string input
......
......@@ -1026,7 +1026,7 @@
<goal
name="WP_parameter run"
locfile="../euler001.mlw"
loclnum="171" loccnumb="6" loccnume="9"
loclnum="176" loccnumb="6" loccnume="9"
expl="VC for run"
sum="d23ff9ccc58983c27e6aa9eee7a9f1af"
proved="true"
......@@ -1046,7 +1046,7 @@
<goal
name="WP_parameter bench"
locfile="../euler001.mlw"
loclnum="176" loccnumb="6" loccnume="11"
loclnum="182" loccnumb="6" loccnume="11"
expl="VC for bench"
sum="0dcae62fb187df85b26250a70b69538d"
proved="true"
......@@ -1063,6 +1063,23 @@
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter go"
locfile="../euler001.mlw"
loclnum="191" loccnumb="6" loccnume="8"
expl="VC for go"
sum="fbc052aded7f685e7674843a291fd493"
proved="true"
expanded="false"
shape="t">
<label
name="expl:VC for go"/>
<transf
name="split_goal_wp"
proved="true"
expanded="false">
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -79,3 +79,6 @@ let power x y =
try power_big_int_positive_big_int x y
with Invalid_argument _ -> zero
let print n = Pervasives.print_string (to_string n)
let chr n = Pervasives.char_of_int (to_int n)
let code c = of_int (Pervasives.int_of_char c)
......@@ -67,3 +67,6 @@ let of_int64 = big_int_of_int64
let power x y = try power_big x y with Invalid_argument _ -> zero
let print n = Pervasives.print_string (to_string n)
let chr n = Pervasives.char_of_int (to_int n)
let code c = of_int (Pervasives.int_of_char c)
module StdIO
use import string.Char
(*i use import string.String *)
(*i TODO: add a ghost reference to represent the standard output *)
val print_char (c:char) : unit
(** prints a character on standard output. *)
(*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. *)
val print_newline (u:unit) : unit
(** prints a newline character on standard output, and flushes standard output. *)
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment