Commit 222a71e7 authored by MARCHE Claude's avatar MARCHE Claude

Андрей, вы действительно читать все эти сообщения?

parent 89f94a8f
\chapter{Introduction}
\section{Architecture and Terminology}
Everything in Why3 revolves around the notion of
\emph{task}\index{task}. Why3, as a platform, as a tool that
translates its input to a number of tasks, and dispatches these tasks
to external provers.
Essentially, a task is a sequence of premises followed by a goal
(i.e.~a \emph{logical sequent} with exactly one formula in the
succedent). The language of tasks is based on first-order language
extended with
\begin{itemize}
\item polymorphic types;
\item algebraic types together with pattern matching;
\item definitions of functions and predicates, possibly recursive or
mutually recursive;
\item inductively defined predicates;
\item \texttt{let} and \texttt{if-then-else} constructs;
%\item Hilbert's epsilon construct
\end{itemize}
\section{Organization of this document}
......
......@@ -85,8 +85,8 @@ Should we cite \cite{conchon08smt} here?
\begin{verbatim}
logic f x_1 .. x_n = (g e_1 .. e_k)
\end{verbatim}
when each e_i is either a constant or one of the x_j, and
each x_1 .. x_n occur at most once in the e_i
when each $e_i$ is either a constant or one of the $x_j$, and
each $x_1$ .. $x_n$ occur at most once in the $e_i$
\item[remove\_triggers]
\item[simplify\_array]
......
......@@ -61,8 +61,8 @@ platform~\cite{filliatre07cav} for program verification. The major
change is a completely new design of the architecture for calling
external provers. An important emphasis is put on the genericity,
which allows for the end user to easily add the support for a new
external prover if wanted. An major new feature is also the ability
to use Why programmatically, via an well-defined API.
external prover if wanted. A major new feature is also the ability
to use Why programmatically, via a well-designed API.
\section*{Acknowledgements}
......@@ -86,6 +86,7 @@ We gratefully thank all the people who contributed to this document:
\bibliographystyle{abbrv}
\bibliography{manual}
\end{document}
%%% Local Variables:
......
......@@ -19,7 +19,7 @@ transformation "eliminate_if"
transformation "eliminate_let"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
transformation "intros"
transformation "introduce_premisses"
theory BuiltIn
syntax type int "int"
......
......@@ -52,6 +52,7 @@ module Hls : Hashtbl.S with type key = lsymbol
module Wls : Hashweak.S with type key = lsymbol
val ls_equal : lsymbol -> lsymbol -> bool
(** equality of function and predicate symbols *)
val ls_hash : lsymbol -> int
val create_lsymbol : preid -> ty list -> ty option -> lsymbol
......@@ -362,7 +363,11 @@ val is_fs_tuple : lsymbol -> bool
(** generic term/fmla traversal *)
val t_map : (term -> term) -> (fmla -> fmla) -> term -> term
(** [t_map fnT fnF t] applies function fnT, resp. fnF, to
each immediate subterms, resp. sub-formula, of [t] *)
val f_map : (term -> term) -> (fmla -> fmla) -> fmla -> fmla
(** [f_map fnT fnF f] applies function fnT, resp. fnF, to
each immediate subterms, resp. sub-formula, of [t] *)
val f_map_sign : (term -> term) -> (bool -> fmla -> fmla) ->
bool -> fmla -> fmla
......
......@@ -51,9 +51,12 @@ val fold_map_l : (task_hd -> 'a * task -> ('a * task) list) ->
'a -> task -> task tlist
val map : (task_hd -> task -> task ) -> task -> task trans
(** [map] is the same as fold with 'a = task *)
val map_l : (task_hd -> task -> task list) -> task -> task tlist
val decl : (decl -> decl list ) -> task -> task trans
(** [decl f acc [d1;..;dn]] returns acc@f d1@..@f dn *)
val decl_l : (decl -> decl list list) -> task -> task tlist
val tdecl : (decl -> tdecl list ) -> task -> task trans
......
......@@ -488,7 +488,7 @@ let prover_on_unproved_goals p () =
(*****************************************************)
let split_transformation = Trans.lookup_transform_l "split_goal" gconfig.env
let intro_transformation = Trans.lookup_transform "intros" gconfig.env
let intro_transformation = Trans.lookup_transform "introduce_premises" gconfig.env
let split_unproved_goals () =
List.iter
......
......@@ -26,10 +26,75 @@ open Ident
open Ty
open Term
open Decl
open Theory
open Task
(* Gappa pre-compilation *)
let term_table = Hterm.create 257
let fmla_table = Hfmla.create 257
(*
let real_abs = ref ps_equ
let real_plus = ref ps_equ
let real_minus = ref ps_equ
*)
let real_le = ref ps_equ
let arith_symbols = ref Sls.empty
let arith_rel_symbols = ref Sls.empty
let extra_decls = ref []
let rec abstract_term t : term =
match t.t_node with
| Tconst _ | Tapp(_,[]) -> t
| Tapp(ls,_) when Sls.mem ls !arith_symbols ->
t_map abstract_term abstract_fmla t
| _ ->
begin try Hterm.find term_table t with Not_found ->
let ls = create_fsymbol (id_fresh "abstr") [] t.t_ty in
let tabs = t_app ls [] t.t_ty in
extra_decls := ls :: !extra_decls;
Hterm.add term_table t tabs;
tabs
end
and abstract_fmla f =
match f.f_node with
| Ftrue | Ffalse -> f
| Fnot _ | Fbinop _ ->
f_map abstract_term abstract_fmla f
| Fapp(ls,_) when Sls.mem ls !arith_rel_symbols ->
f_map abstract_term abstract_fmla f
| _ ->
begin try Hfmla.find fmla_table f with Not_found ->
let ls = create_psymbol (id_fresh "abstr") [] in
let fabs = f_app ls [] in
extra_decls := ls :: !extra_decls;
Hfmla.add fmla_table f fabs;
fabs
end
let abstract_decl (d : decl) : decl list =
let d = decl_map abstract_term abstract_fmla d in
let l =
List.fold_left
(fun acc ls -> create_logic_decl [ls,None] :: acc)
[d]
!extra_decls
in
extra_decls := []; l
let abstraction (t: task) : task =
Hfmla.clear fmla_table;
Hterm.clear term_table;
Trans.apply (Trans.decl abstract_decl None) t
(* Gappa printing *)
type info = {
le_real : lsymbol;
info_syn : string Mid.t;
info_rem : Sid.t;
}
......@@ -109,7 +174,7 @@ let rec print_fmla info fmt f =
with Not_found ->
fprintf fmt "%a - %a in [0,0]" term t1 term t2
end
| Fapp (ls, [t1;t2]) when ls_equal ls info.le_real ->
| Fapp (ls, [t1;t2]) when ls_equal ls !real_le ->
begin try
let c1 = constant_value t1 in
fprintf fmt "%a >= %s" term t2 c1
......@@ -177,12 +242,15 @@ unsupportedDecl d
*)
| Dind _ -> unsupportedDecl d
"gappa: inductive definitions are not supported"
| Dprop (Paxiom, pr, _f) ->
| Dprop (Paxiom, pr, f) ->
fprintf fmt "# hypothesis '%a'@\n" print_ident pr.pr_name;
(* fprintf fmt "@[<hv 2>%a@]@\n" (print_hyp info) f *)
fprintf fmt "@[<hv 2>%a ->@]@\n" (print_fmla info) f
| Dprop (Pgoal, pr, f) ->
fprintf fmt "# goal '%a'@\n" print_ident pr.pr_name;
(*
fprintf fmt "@[<hv 2>{ %a@ }@]@\n" (print_fmla info) f
*)
fprintf fmt "@[<hv 2>%a@]@\n" (print_fmla info) f
| Dprop ((Plemma|Pskip), _, _) ->
unsupportedDecl d
"gappa: lemmas are not supported"
......@@ -191,18 +259,32 @@ let print_decl ?old:_ info fmt =
catch_unsupportedDecl (print_decl (* ?old *) info fmt)
let print_decls ?old info fmt dl =
fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl ?old info)) dl
fprintf fmt "@[<hov>{ %a }@\n@]" (print_list nothing (print_decl ?old info)) dl
let get_info env task =
let real_theory = Env.find_theory env ["real"] "Real" in
let le_real = Theory.ns_find_ls real_theory.Theory.th_export ["infix <="] in
{
le_real = le_real;
let find_real = Theory.ns_find_ls real_theory.Theory.th_export in
let real_add = find_real ["infix +"] in
let real_sub = find_real ["infix -"] in
let real_mul = find_real ["infix *"] in
let real_div = find_real ["infix /"] in
real_le := Theory.ns_find_ls real_theory.Theory.th_export ["infix <="];
let real_abs_theory = Env.find_theory env ["real"] "Abs" in
let real_abs = Theory.ns_find_ls real_abs_theory.Theory.th_export ["abs"] in
(* sets of known symbols *)
arith_symbols :=
List.fold_right Sls.add
[real_add; real_sub; real_mul; real_div;
real_abs] Sls.empty ;
arith_rel_symbols :=
List.fold_right Sls.add [!real_le] Sls.empty ;
{
info_syn = get_syntax_map task;
info_rem = get_remove_set task;
}
let print_task env pr thpr ?old fmt task =
let task = abstraction task in
forget_all ident_printer;
print_prelude fmt pr;
print_th_prelude task fmt thpr;
......
......@@ -49,7 +49,7 @@ let rec intros pr f = match f.f_node with
let intros pr f : decl list = intros pr f
let () = Trans.register_transform "introduce_premisses" (Trans.goal intros)
let () = Trans.register_transform "introduce_premises" (Trans.goal intros)
......
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