Commit 90501084 authored by MARCHE Claude's avatar MARCHE Claude

preliminary support for gappa

parent bd3b16ae
......@@ -604,8 +604,8 @@ testl-type: bin/whyml.byte
test-api: src/why.cma
ocaml unix.cma str.cma nums.cma dynlink.cma ocamlgraph/graph.cma \
src/why.cma -I src examples/use_api.ml
src/why.cma -I src examples/use_api.ml \
|| (printf "Test of Why API calls failed. Please fix it"; exit 2)
## install: install-binary install-lib install-man
##
......
\chapter{The Why3 Application Programming Interface}
\label{chap:api}
\section{Building Terms and Formulas}
......
\chapter{IDE}
\label{chap:ide}
\section{IDE}
......
\chapter{Introduction}
\section{Organization of this document}
This document is organized as follows. The first three chapters are
user manuals, to learn how to use Why3. Other chapters are reference
manuals, giving detailed technical informations.
Chapter~\ref{chap:syntax} presents the input syntax for file defining
Why theories. The semantics is given informally with examples.
Chapter~\ref{chap:ide} explains how to use the Why IDE for visualizing
theories and goals, call external provers for trying to solve them,
apply transformations to simplify them. The two first chapters are
thus to read for the beginners.
Chapter~\ref{chap:api} presents how to use Why3 programmatically,
using the API. It is for the more advanced users, who wants to link
Why3 library with their own code.
Chapter~\ref{chap:manpages} are the technical manual pages for the tools of
the platform. All tool options, and all the configuration files are described in details there.
Chapter~\ref{chap:apidoc} is the technical documentation of the API.
%%% Local Variables:
%%% mode: latex
%%% TeX-PDF-mode: t
%%% TeX-master: "manual"
%%% End:
\chapter{Reference manuals for the Why3 tools}
\label{chap:manpages}
\section{Compilation, Installation}
......
......@@ -68,6 +68,8 @@ to use Why programmatically, via an well-defined API.
We gratefully thank all the people who contributed to this document:
\input{intro.tex}
\input{syntax.tex}
\input{ide.tex}
......@@ -77,6 +79,7 @@ We gratefully thank all the people who contributed to this document:
\input{manpages.tex}
\chapter{Complete API documentation}
\label{chap:apidoc}
\input{./apidoc.tex}
......
\chapter{Syntax}
\label{chap:syntax}
This chapter describes the input syntax, and informally gives its semantics,
illustrated by examples.
......
......@@ -3,8 +3,7 @@
prelude "# this is a prelude for Gappa"
(* printer "gappa" *)
printer "why3"
printer "gappa"
filename "%f-%t-%g.gappa"
valid 0
......
......@@ -122,5 +122,3 @@ let () = printf "@[On task 3, alt-ergo answers %a@."
(* build a theory with all these goals *)
......@@ -70,7 +70,7 @@ let load rc =
tps
let read_auto_detection_data main =
let filename = Filename.concat main.datadir "provers-detection-data.conf" in
let filename = Filename.concat (Whyconf.datadir main) "provers-detection-data.conf" in
try
let rc = Rc.from_file filename in
load rc
......@@ -144,7 +144,7 @@ let detect_prover main acc data =
{name = data.prover_name;
version = ver;
command = c;
driver = Filename.concat main.datadir data.prover_driver;
driver = Filename.concat (datadir main) data.prover_driver;
editor = data.prover_editor} acc
with Not_found ->
begin
......
......@@ -23,17 +23,15 @@ open Rc
(* lib and shared dirs *)
let libdir =
try
Sys.getenv "WHY3LIB"
with Not_found -> default_option Config.libdir Config.localdir
let compilation_libdir = default_option Config.libdir Config.localdir
let datadir =
try
Sys.getenv "WHY3DATA"
with Not_found -> option_apply Config.datadir
let compilation_datadir =
option_apply Config.datadir
(fun d -> Filename.concat d "share") Config.localdir
let compilation_loadpath =
Filename.concat compilation_datadir "theories"
let default_conf_file =
Filename.concat (match Config.localdir with
| None -> Rc.get_home_dir ()
......@@ -50,14 +48,24 @@ type config_prover = {
}
type main = {
libdir : string;
datadir : string;
private_libdir : string;
private_datadir : string;
loadpath : string list;
timelimit : int;
memlimit : int;
running_provers_max : int;
}
let libdir m =
try
Sys.getenv "WHY3LIB"
with Not_found -> m.private_libdir
let datadir m =
try
Sys.getenv "WHY3DATA"
with Not_found -> m.private_datadir
type config = {
conf_file : string; (* "/home/innocent_user/.why.conf" *)
config : Rc.t ;
......@@ -67,9 +75,9 @@ type config = {
let default_main =
{
libdir = libdir;
datadir = datadir;
loadpath = [Filename.concat datadir "theories"];
private_libdir = compilation_libdir;
private_datadir = compilation_datadir;
loadpath = [compilation_loadpath];
timelimit = 10;
memlimit = 0;
running_provers_max = 2;
......@@ -77,8 +85,8 @@ let default_main =
let set_main rc main =
let section = empty_section in
let section = set_string section "libdir" main.libdir in
let section = set_string section "datadir" main.datadir in
let section = set_string section "libdir" main.private_libdir in
let section = set_string section "datadir" main.private_datadir in
let section = set_stringl section "loadpath" main.loadpath in
let section = set_int section "timelimit" main.timelimit in
let section = set_int section "memlimit" main.memlimit in
......@@ -116,8 +124,8 @@ let load_prover dirname provers (id,section) =
} provers
let load_main dirname section =
{ libdir = get_string ~default:default_main.libdir section "libdir";
datadir = get_string ~default:default_main.datadir section "datadir";
{ private_libdir = get_string ~default:default_main.private_libdir section "libdir";
private_datadir = get_string ~default:default_main.private_datadir section "datadir";
loadpath = List.map (absolute_filename dirname)
(get_stringl ~default:default_main.loadpath section "loadpath");
timelimit = get_int ~default:default_main.timelimit section "timelimit";
......
......@@ -30,8 +30,8 @@ type config_prover = {
}
type main = {
libdir : string; (* "/usr/local/lib/why/" *)
datadir : string; (* "/usr/local/share/why/" *)
private_libdir : string; (* "/usr/local/lib/why/" *)
private_datadir : string; (* "/usr/local/share/why/" *)
loadpath : string list; (* "/usr/local/lib/why/theories" *)
timelimit : int; (* default prover time limit in seconds
(0 unlimited) *)
......@@ -41,6 +41,9 @@ type main = {
(* max number of running prover processes *)
}
val libdir: main -> string
val datadir: main -> string
type config
(** A configuration linked to an rc file. Whyconf gives access to
every sections of the rc file ({!Whyconf.get_section},
......
......@@ -154,7 +154,7 @@ let get_main () = (get_main config.config)
let image ?size f =
let main = get_main () in
let n = Filename.concat main.datadir (Filename.concat "images" (f^".png"))
let n = Filename.concat (datadir main) (Filename.concat "images" (f^".png"))
in
match size with
| None ->
......
......@@ -55,7 +55,7 @@ let fname = match !file with
let lang =
let main = get_main () in
let load_path = Filename.concat main.datadir "lang" in
let load_path = Filename.concat (datadir main) "lang" in
let languages_manager =
GSourceView2.source_language_manager ~default:true
in
......
......@@ -19,10 +19,9 @@
(** Gappa printer *)
(*
open Register
open Format
open Pp
open Printer
open Ident
open Ty
open Term
......@@ -30,363 +29,8 @@ open Decl
open Task
(* Gappa terms and formulas *)
(* fields of the float model *)
type float_field = Rounded | Exact | Model
(* formats of the float model *)
type float_fmt = Int | Single | Double | Binary80
(* modes of the float model *)
type mode = RndNE | RndZR | RndUP | RndDN | RndNA
type gterm =
| Gvar of string
| Gfld of float_field * string
| Grnd of float_fmt * mode * gterm
| Gcst of string
| Gsqrt of gterm
| Gneg of gterm
| Gadd of gterm * gterm
| Gsub of gterm * gterm
| Gmul of gterm * gterm
| Gdiv of gterm * gterm
| Gabs of gterm
type gpred =
| Gle of gterm * string
| Gge of gterm * string
| Gin of gterm * string * string
| Grel of gterm * gterm * string
| Gimplies of gpred * gpred
| Gand of gpred * gpred
| Gor of gpred * gpred
| Gnot of gpred
type gobligation = (string * gterm) list * gpred
(* contains the roundings used *)
let rnd_table = Hashtbl.create 10
let get_format = function
| Single -> "ieee_32"
| Double -> "ieee_64"
| Binary80 -> "x86_80"
| Int -> "int"
let get_mode = function
| RndNE -> "ne"
| RndZR -> "zr"
| RndUP -> "up"
| RndDN -> "dn"
| RndNA -> "na"
let rec print_term fmt = function
| Gvar x -> fprintf fmt "%s" x
| Gfld (Rounded, x) -> fprintf fmt "float_%s" x
| Gfld (Exact, x) -> fprintf fmt "exact_%s" x
| Gfld (Model, x) -> fprintf fmt "model_%s" x
| Grnd (f, m, t) ->
fprintf fmt "rnd_%s%s(%a)" (get_format f) (get_mode m) print_term t
| Gcst c -> fprintf fmt "%s" c
| Gneg t -> fprintf fmt "(-%a)" print_term t
| Gadd (t1, t2) -> fprintf fmt "(%a + %a)" print_term t1 print_term t2
| Gsub (t1, t2) -> fprintf fmt "(%a - %a)" print_term t1 print_term t2
| Gmul (t1, t2) -> fprintf fmt "(%a * %a)" print_term t1 print_term t2
| Gdiv (t1, t2) -> fprintf fmt "(%a / %a)" print_term t1 print_term t2
| Gabs t -> fprintf fmt "|%a|" print_term t
| Gsqrt t -> fprintf fmt "sqrt(%a)" print_term t
let rec print_pred_atom fmt = function
| Gle (t, r1) ->
fprintf fmt "%a <= %s" print_term t r1
| Gge (t, r1) ->
fprintf fmt "%a >= %s" print_term t r1
| Gin (t, r1, r2) ->
fprintf fmt "%a in [%s, %s]" print_term t r1 r2
| Grel (t1, t2, r1) ->
fprintf fmt "|%a -/ %a| <= %s" print_term t1 print_term t2 r1
| Gnot p ->
fprintf fmt "not %a" print_pred_atom p
| _ as p ->
fprintf fmt "(%a)" print_pred p
and print_pred_left fmt = function
| Gand (p1, p2) ->
fprintf fmt "@[%a /\\@ %a@]" print_pred_atom p1 print_pred_atom p2
| Gor (p1, p2) ->
fprintf fmt "@[%a \\/@ %a@]" print_pred_atom p1 print_pred_atom p2
| _ as p ->
print_pred_atom fmt p
and print_pred fmt = function
| Gimplies (p1, p2) ->
fprintf fmt "@[%a ->@ %a@]" print_pred_left p1 print_pred p2
| _ as p ->
print_pred_left fmt p
let print_equation fmt (e, x, t) =
let e =
match e with
| Rounded -> "float_"
| Exact -> "exact_"
| Model -> "model_" in
fprintf fmt "@[%s%s = %a;@]" e x print_term t
let print_obligation fmt (eq,p) =
Hashtbl.iter
(fun (f, m) () ->
let m = get_mode m in
match f with
| Int ->
fprintf fmt "@@rnd_int%s = int<%s>;@\n" m m
| _ ->
let f = get_format f in
fprintf fmt "@@rnd_%s%s = float<%s, %s>;@\n" f m f m)
rnd_table;
fprintf fmt "@\n%a@\n@\n" (print_list newline print_equation) eq;
fprintf fmt "{ @[%a@] }@." print_pred p
(*
let print_file fmt = Queue.iter (print_obligation fmt) queue
let output_one_file ~allowedit file =
if allowedit then
begin
let sep = "### DO NOT EDIT ABOVE THIS LINE" in
do_not_edit_above ~file
~before:print_file
~sep
~after:(fun _fmt -> ())
end
else
print_in_file print_file file
let output_file fwe =
let sep = "### DO NOT EDIT ABOVE THIS LINE" in
let i = ref 0 in
Queue.iter
(fun o ->
incr i;
if debug then eprintf "gappa obligation %d@." !i;
let file = fwe ^ "_why_po_" ^ string_of_int !i ^ ".gappa" in
do_not_edit_above ~file
~before:(fun fmt -> print_obligation fmt o)
~sep
~after:(fun _fmt -> ()))
queue
*)
(* compilation to Gappa formulas *)
exception NotGappa
(* TODO: comment faire une table de hash indexée par des termes ? *)
(*
module Termtbl = Hashtbl.Make(HashedTerm)
(* contains all the terms that have been generalized away,
because they were not recognized *)
let gen_table = Termtbl.create 10
(* contains the terms associated to variables, especially gen_float variables *)
let var_table = Hashtbl.create 10
(* contains the names already defined,
so new definitions should be as equalities *)
let def_table = Hashtbl.create 10
(* contains the reverted list of aliases from def_table *)
let def_list = ref []
(* contains the list of format-implied bounds on float variables *)
let bnd_list = ref []
*)
let prelude_to_load = ref true
let dummy_symbol = (Obj.magic 0 : Term.lsymbol)
let symbol_le_int = ref dummy_symbol
let symbol_le_real = ref dummy_symbol
let symbol_ge_int = ref dummy_symbol
let symbol_ge_real = ref dummy_symbol
let symbol_add_int = ref dummy_symbol
let load_prelude (info : Driver.driver_query) =
if !prelude_to_load then
begin
let env = Driver.query_env info in
let int_theory = Env.find_theory env ["int"] "Int" in
let real_theory = Env.find_theory env ["real"] "Real" in
symbol_le_int :=
Theory.ns_find_ls int_theory.Theory.th_export ["infix <="];
symbol_le_real :=
Theory.ns_find_ls real_theory.Theory.th_export ["infix <="];
symbol_ge_int :=
Theory.ns_find_ls int_theory.Theory.th_export ["infix >="];
symbol_ge_real :=
Theory.ns_find_ls real_theory.Theory.th_export ["infix >="];
symbol_add_int :=
Theory.ns_find_ls int_theory.Theory.th_export ["infix +"];
prelude_to_load := false;
end
(* true when id is <= on R or Z *)
let is_le_num id =
ls_equal id !symbol_le_int
|| ls_equal id !symbol_le_real
(* true when id is >= on R or Z *)
let is_ge_num id =
ls_equal id !symbol_ge_int
|| ls_equal id !symbol_ge_real
(* true when id is = *)
let is_eq id = ls_equal id Term.ps_equ
(* true when id is <> *)
let is_neq id = ls_equal id Term.ps_neq
let eval_constant c =
match c with
| ConstInt s -> s
| ConstReal(RConstDecimal(_e,_f,_exp)) -> assert false
| ConstReal(RConstHexa(_e,_f,_exp)) -> assert false
let rec term t =
match t.t_node with
| Tconst c -> Gcst (eval_constant c)
| Tbvar _n -> assert false
| Tvar _v -> assert false
| Tapp(f,[t1;t2]) when ls_equal f !symbol_add_int ->
Gadd (term t1, term t2)
(* TODO: neg, abs, + real, - , * , /, real_of_int,
etc. *)
| Tapp(_,_) -> raise NotGappa
| Tif(_f,_t1,_t2) -> assert false
| Tlet(_t,_tb) -> assert false
| Tcase(_tl,_tbl) -> assert false
| Teps _fb -> assert false
(*
function
| t when is_constant t ->
Gcst (eval_constant t)
| Tconst _ ->
raise NotGappa
| Tvar id ->
Gvar (Ident.string id)
| Tderef id ->
Gvar (Ident.string id)
(* int and real ops *)
| Tapp (id, [t], _) when id == t_neg_real || id = t_neg_int ->
Gneg (term t)
| Tapp (id, [t], _) when id == t_abs_real || id == t_abs_int ->
Gabs (term t)
| Tapp (id, [t], _) when id == t_sqrt_real ->
Gsqrt (term t)
| Tapp (id, [t1; t2], _) when id == t_add_real || id = t_add_int ->
Gadd (term t1, term t2)
| Tapp (id, [t1; t2], _) when id == t_sub_real || id = t_sub_int ->
Gsub (term t1, term t2)
| Tapp (id, [t1; t2], _) when id == t_mul_real || id = t_mul_int ->
Gmul (term t1, term t2)
| Tapp (id, [t1; t2], _) when id == t_div_real ->
Gdiv (term t1, term t2)
(* conversion int -> real *)
| Tapp (id, [t], _) when id == real_of_int ->
term t
(* conversion real -> int by truncate, i.e. towards zero *)
| Tapp (id, [t], _) when id == truncate_real_to_int ->
let mode = RndZR in
Hashtbl.replace rnd_table (Int, mode) ();
Grnd (Int, mode, term t)
(* [Jessie] rounding *)
| Tapp (id, [Tapp (m, [], _); t], _)
when id == round_single ->
let mode = mode_of_id m in
Hashtbl.replace rnd_table (Single, mode) ();
Grnd (Single, mode, term t)
| Tapp (id, [Tapp (m, [], _); t], _)
when id == round_double ->
let mode = mode_of_id m in
Hashtbl.replace rnd_table (Double, mode) ();
Grnd (Double, mode, term t)
| Tapp (id1, [Tapp (id2, l1, l2)], _)
when id1 == single_value && id2 == round_single_logic ->
term (Tapp (round_single, l1, l2))
| Tapp (id1, [Tapp (id2, l1, l2)], _)
when id1 == double_value && id2 == round_double_logic ->
term (Tapp (round_double, l1, l2))
(* casts *)
| Tapp (id1, [Tapp (id2,[Tapp (m, [], _); t] , l2)], _)
when id1 == single_value && id2 == double_to_single ->
let mode = mode_of_id m in
Hashtbl.replace rnd_table (Single, mode) ();
Grnd (Single, mode, term (Tapp (double_value,[t],l2)))
| Tapp (id1, [Tapp (id2,[Tapp (_m, [], _); t] , l2)], _)
when id1 == double_value && id2 == single_to_double ->
term (Tapp (single_value,[t],l2))
| Tapp (id, [t], _)
when (id == single_value || id == double_value || id == single_exact
|| id == double_exact || id == single_model || id == double_model) ->
let v = create_var t in
let f = field_of_id id in
let add_def fmt =
if not (Hashtbl.mem def_table (f, v)) then begin
Hashtbl.add def_table (f, v) ();
Hashtbl.replace rnd_table (fmt, RndNE) ();
def_list := (f, v, Grnd (fmt, RndNE, Gvar ("dummy_float_" ^ v))) :: !def_list;
let b =
if fmt = Single then "0x1.FFFFFEp127" else
if fmt = Double then "0x1.FFFFFFFFFFFFFp1023" else
assert false in
bnd_list := Gin (Gfld (f, v), "-"^b, b) :: !bnd_list
end in
if id == single_value then add_def Single else
if id == double_value then add_def Double;
Gfld (f, v)
| Tapp (id, [t], _)
when id == single_round_error || id == double_round_error ->
let v = create_var t in
Gabs (Gsub (Gfld (Rounded, v), Gfld (Exact, v)))
| Tnamed(_,t) -> term t
(* anything else is generalized as a fresh variable *)
| Tapp _ as t ->
Gvar (create_var t)
*)
(*
let ident_printer =
let bls = [
"ac"; "and"; "array"; "as"; "axiom"; "bool"; "else"; "exists";
"false"; "forall"; "function"; "goal"; "if"; "int"; "bitv";
"logic"; "not"; "or"; "parameter"; "predicate";
"prop"; "real"; "then"; "true"; "type"; "unit"; "void";
]
in
let san = sanitizer char_to_alpha char_to_alnumus in
......@@ -395,64 +39,69 @@ let ident_printer =
let print_ident fmt id =
fprintf fmt "%s" (id_unique ident_printer id)
let print_tvsymbols fmt tv =
let sanitize n = "'" ^ n in
let n = id_unique ident_printer ~sanitizer:sanitize tv.tv_name in
fprintf fmt "%s" n
let forget_var v = forget_id ident_printer v.vs_name
type info = {
info_syn : string Mid.t;
info_rem : Sid.t;
}
let rec print_type info fmt ty = match ty.ty_node with
| Tyvar id ->
print_tvsymbols fmt id
| Tyapp (ts, tl) -> begin match query_syntax info.info_sym ts.ts_name with
| Some s -> syntax_arguments s (print_type info) fmt tl
| None -> fprintf fmt "%a%a" (print_tyapp info) tl print_ident ts.ts_name
end
let constant_value t =
match t.t_node with
| Tconst (ConstInt s) -> s
| _ -> raise Not_found
and print_tyapp info fmt = function
| [] -> ()
| [ty] -> fprintf fmt "%a " (print_type info) ty
| tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl
(* terms *)
let rec print_term info fmt t = match t.t_node with
let print_term fmt t = match t.t_node with
| Tbvar _ ->
assert false
| Tconst c ->
Pretty.print_const fmt c
| Tvar { vs_name = id } ->
print_ident fmt id
| Tapp (ls, tl) -> begin match query_syntax info.info_sym ls.ls_name with
| Tapp (ls, _tl) ->