1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2025 -- Inria - CNRS - Paris-Saclay University *)
(* *)
(* This software is distributed under the terms of the GNU Lesser *)
(* General Public License version 2.1, with the special exception *)
(* on linking described in file LICENSE. *)
(********************************************************************)
(*******************
This file is for testing the creation of epsilon-terms using the Ptree
API and the S-expression parsing and printing
******************)
open Why3
let config : Whyconf.config = Whyconf.init_config None
let main : Whyconf.main = Whyconf.get_main config
let env : Env.env = Env.create_env (Whyconf.loadpath main)
open Ptree
open Ptree_helpers
(* declaration of
module M
use int.Int
goal g : (epsilon x. 0 <= x) + 1 > 0
end
*)
let mlw_source_file = "../epsilon.mlw"
let sexp_file = "examples/use_api/epsilon.sexp"
let loc = Loc.user_position mlw_source_file 1 0 1 1
let mod_M =
(* use int.Int *)
let use_int_Int = use ~loc ~import:false (["int";"Int"]) in
(* goal g *)
let g =
let zero = tconst ~loc 0 in
let le_int = qualid ["Int";Ident.op_infix "<="] in
let id_x = ident ~loc "x" in
let ty_int = PTtyapp(qualid ["int"],[]) in
let zero_le_x = tapp ~loc le_int [zero;tvar ~loc (Qident id_x)] in
let eps = term ~loc (Teps(id_x,ty_int,zero_le_x)) in
let gt_int = qualid ["Int";Ident.op_infix ">"] in
let one = tconst ~loc 1 in
let add_int = qualid ["Int";Ident.op_infix "+"] in
let goal_term = tapp ~loc gt_int [tapp add_int [eps;one]; zero] in
Dprop(Decl.Pgoal, ident ~loc "g", goal_term)
in
(ident ~loc "M",[use_int_Int ; g])
let mlw_file = Modules [mod_M]
open Format
(* Printing back the mlw file, in S-expression format *)
let sexp = Ptree.sexp_of_mlw_file mlw_file
let () = printf "@[%a@]@." Sexplib.Sexp.pp sexp
let () =
let ch = open_out sexp_file in
Sexplib.Sexp.output ch sexp;
close_out ch
let mods =
try
Typing.type_mlw_file env [] sexp_file mlw_file
with Loc.Located _ as e ->
Format.eprintf "%a@." Exn_printer.exn_printer e;
exit 1
(* Checking the VCs *)
let my_tasks : Task.task list =
let mods =
Wstdlib.Mstr.fold
(fun _ m acc ->
List.rev_append
(Task.split_theory m.Pmodule.mod_theory None None) acc)
mods []
in List.rev mods
let provers : Whyconf.config_prover Whyconf.Mprover.t =
Whyconf.get_provers config
let limits =
Call_provers.{empty_limits with
limit_time = Whyconf.timelimit main;
limit_mem = Whyconf.memlimit main }
let alt_ergo : Whyconf.config_prover =
let fp = Whyconf.parse_filter_prover "Alt-Ergo" in
let provers = Whyconf.filter_provers config fp in
if Whyconf.Mprover.is_empty provers then begin
eprintf "Prover Alt-Ergo not installed or not configured@.";
exit 1
end else
snd (Whyconf.Mprover.max_binding provers)
let alt_ergo_driver : Driver.driver =
try
Driver.load_driver_for_prover main env alt_ergo
with e ->
eprintf "Failed to load driver for alt-ergo: %a@."
Exn_printer.exn_printer e;
exit 1
let () =
List.iteri (fun i t ->
let call =
Driver.prove_task ~limits ~config:main
~command:alt_ergo.Whyconf.command alt_ergo_driver t in
let r = Call_provers.wait_on_call call in
printf "@[On task %d, Alt-ergo answers %a@]@." (succ i)
(Call_provers.print_prover_result ~json:false) r)
my_tasks
let () =
printf "You can try the same example in the IDE using@\n";
printf " why3 ide %s@." sexp_file
(*
Local Variables:
compile-command: "make -C ../.. test-api-epsilon"
End:
*)
|
