Commit f4a218c2 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

syntax of agathe problem

parent a7401045
...@@ -25,6 +25,7 @@ ...@@ -25,6 +25,7 @@
7.8 why.conf (TODO Francois) 7.8 why.conf (TODO Francois)
7.9 drivers (TODO Francois) 7.9 drivers (TODO Francois)
7.10 transformations (TODO) 7.10 transformations (TODO)
** citation cruanes10 inexistent
8 API: Andrei + Francois 8 API: Andrei + Francois
(should we really add that in the doc ?) (should we really add that in the doc ?)
......
...@@ -137,6 +137,8 @@ echo "" ...@@ -137,6 +137,8 @@ echo ""
echo "=== Type-checking good files ===" echo "=== Type-checking good files ==="
goods bench/typing/good --type-only goods bench/typing/good --type-only
goods examples --type-only
goods examples/tptp --type-only
echo "" echo ""
echo "=== Type-checking theories ===" echo "=== Type-checking theories ==="
......
...@@ -96,7 +96,7 @@ external prover if wanted. A major new feature is also the ability ...@@ -96,7 +96,7 @@ external prover if wanted. A major new feature is also the ability
to use Why programmatically, via a well-designed API. to use Why programmatically, via a well-designed API.
\subsection*{Availability} \subsection{Availability}
\why\ project page is \url{https://gforge.inria.fr/projects/why3}. The \why\ project page is \url{https://gforge.inria.fr/projects/why3}. The
last distribution is available, in source format, together with this last distribution is available, in source format, together with this
...@@ -109,7 +109,7 @@ See the file \texttt{INSTALL} for quick installation instructions, and ...@@ -109,7 +109,7 @@ See the file \texttt{INSTALL} for quick installation instructions, and
Section~\ref{sec:install} of this document for more detailed Section~\ref{sec:install} of this document for more detailed
instructions. instructions.
\subsection*{Contact} \subsection{Contact}
There is a public mailing list for users' discussions: There is a public mailing list for users' discussions:
\url{http://lists.gforge.inria.fr/mailman/listinfo/why3-club}. \url{http://lists.gforge.inria.fr/mailman/listinfo/why3-club}.
...@@ -118,12 +118,12 @@ Report any bug to the \why\ Bug Tracking System: ...@@ -118,12 +118,12 @@ Report any bug to the \why\ Bug Tracking System:
\url{https://gforge.inria.fr/tracker/?atid=10293&group_id=2990&func=browse}. \url{https://gforge.inria.fr/tracker/?atid=10293&group_id=2990&func=browse}.
\section*{Acknowledgements} \subsection{Acknowledgements}
We gratefully thank the people who contributed to \why: Simon Cruanes, We gratefully thank the people who contributed to \why: Simon Cruanes,
Johannes Kanig, St\'ephane Lescuyer, Sim\~ao Melo de Sousa. Johannes Kanig, St\'ephane Lescuyer, Sim\~ao Melo de Sousa.
\section*{Release notes} \subsection{Release notes}
\paragraph{Version 0.10} \paragraph{Version 0.10}
Initial release. Initial release.
...@@ -146,7 +146,7 @@ Initial release. ...@@ -146,7 +146,7 @@ Initial release.
\tableofcontents \tableofcontents
\input{intro.tex} % \input{intro.tex}
\part{Tutorial} \part{Tutorial}
......
...@@ -3,61 +3,50 @@ theory Agatha ...@@ -3,61 +3,50 @@ theory Agatha
type person = Agatha | Butler | Charles type person = Agatha | Butler | Charles
logic hates(person, person) logic hates person person
logic richer(person, person) logic richer person person
logic lives(person) logic lives person
logic killed(person, person) logic killed person person
axiom Lives1 : lives(Agatha) axiom Lives1 : lives Agatha
axiom Lives2 : lives(Charles) axiom Lives2 : lives Charles
axiom Lives3 : lives(Butler) axiom Lives3 : lives Butler
axiom NoOneLivesForever : axiom NoOneLivesForever :
forall x:person. forall x:person.
lives(x) -> x = Agatha or x = Charles or x = Butler lives x -> x = Agatha or x = Charles or x = Butler
axiom MURDER : axiom MURDER :
exists x:person. exists x:person.
lives(x) and killed(x, Agatha) lives x and killed x Agatha
axiom Hate_and_killed : axiom Hate_and_killed :
forall p1:person. forall p2:person. forall p1 p2:person. killed p1 p2 -> hates p1 p2
killed(p1, p2) -> hates(p1, p2)
axiom Killed_and_wealth : axiom Killed_and_wealth :
forall p1:person. forall p2:person. forall p1 p2:person. killed p1 p2 -> not (richer p1 p2)
killed(p1, p2) -> not (richer(p1, p2))
axiom Diff1 : lemma Diff1 : Agatha <> Butler
Agatha <> Butler
axiom Diff2 :
Agatha <> Charles
axiom Diff3 :
Charles <> Butler
lemma Diff2 : Agatha <> Charles
lemma Diff3 : Charles <> Butler
axiom H1 : axiom H1 :
forall x:person. forall x:person. hates Agatha x -> not (hates Charles x)
hates(Agatha, x) -> not (hates(Charles, x))
axiom H2 : axiom H2 :
forall x:person. forall x:person. x <> Butler -> hates Agatha x
x <> Butler -> hates(Agatha, x)
axiom H3 : axiom H3 :
forall x:person. forall x:person. not (richer x Agatha) -> hates Butler x
not (richer(x, Agatha)) -> hates(Butler, x)
axiom H4 : axiom H4 :
forall x:person. forall x:person. hates Agatha x -> hates Butler x
hates(Agatha, x) -> hates(Butler, x)
axiom H5 : axiom H5 :
forall x:person. forall x:person. exists y:person. not (hates x y)
exists y:person.
not (hates(x,y))
goal Enigma: goal Enigma: killed Agatha Agatha
killed(Agatha, Agatha)
end end
...@@ -411,11 +411,11 @@ let tools_window_vbox = ...@@ -411,11 +411,11 @@ let tools_window_vbox =
GPack.vbox ~packing:(hb#pack ~expand:false) () GPack.vbox ~packing:(hb#pack ~expand:false) ()
with Gtk.Error _ -> assert false with Gtk.Error _ -> assert false
let context_frame = let context_frame =
GBin.frame ~label:"Context" GBin.frame ~label:"Context"
~packing:(tools_window_vbox#pack ~expand:false) () ~packing:(tools_window_vbox#pack ~expand:false) ()
let context_box = let context_box =
GPack.button_box `VERTICAL ~border_width:5 GPack.button_box `VERTICAL ~border_width:5
~spacing:5 ~spacing:5
~packing:context_frame#add () ~packing:context_frame#add ()
...@@ -423,23 +423,23 @@ let context_box = ...@@ -423,23 +423,23 @@ let context_box =
let context_unproved_goals_only = ref true let context_unproved_goals_only = ref true
let () = let () =
let b1 = GButton.radio_button let b1 = GButton.radio_button
~packing:context_box#add ~label:"Unproved goals only" () ~packing:context_box#add ~label:"Unproved goals only" ()
in in
let (_ : GtkSignal.id) = let (_ : GtkSignal.id) =
b1#connect#clicked b1#connect#clicked
~callback:(fun () -> context_unproved_goals_only := true) ~callback:(fun () -> context_unproved_goals_only := true)
in in
let b2 = GButton.radio_button let b2 = GButton.radio_button
~group:b1#group ~packing:context_box#add ~label:"All goals" () ~group:b1#group ~packing:context_box#add ~label:"All goals" ()
in in
let (_ : GtkSignal.id) = let (_ : GtkSignal.id) =
b2#connect#clicked b2#connect#clicked
~callback:(fun () -> context_unproved_goals_only := false) ~callback:(fun () -> context_unproved_goals_only := false)
in () in ()
let provers_frame = let provers_frame =
GBin.frame ~label:"Provers" GBin.frame ~label:"Provers"
~packing:(tools_window_vbox#pack ~expand:false) () ~packing:(tools_window_vbox#pack ~expand:false) ()
...@@ -454,7 +454,7 @@ let transf_frame = ...@@ -454,7 +454,7 @@ let transf_frame =
let transf_box = let transf_box =
GPack.button_box `VERTICAL ~border_width:5 ~packing:transf_frame#add () GPack.button_box `VERTICAL ~border_width:5 ~packing:transf_frame#add ()
let tools_frame = let tools_frame =
GBin.frame ~label:"Tools" GBin.frame ~label:"Tools"
~packing:(tools_window_vbox#pack ~expand:false) () ~packing:(tools_window_vbox#pack ~expand:false) ()
...@@ -745,7 +745,7 @@ end ...@@ -745,7 +745,7 @@ end
(*********************************) (*********************************)
(* (*
type trans = type trans =
| Trans_one of Task.task Trans.trans | Trans_one of Task.task Trans.trans
| Trans_list of Task.task Trans.tlist | Trans_list of Task.task Trans.tlist
...@@ -761,7 +761,7 @@ let split_transformation = lookup_trans "split_goal" ...@@ -761,7 +761,7 @@ let split_transformation = lookup_trans "split_goal"
let unfold_transformation = lookup_trans "inline_goal" let unfold_transformation = lookup_trans "inline_goal"
let intro_transformation = lookup_trans "introduce_premises" let intro_transformation = lookup_trans "introduce_premises"
let apply_trans t task = let apply_trans t task =
match t with match t with
| Trans_one t -> [Trans.apply t task] | Trans_one t -> [Trans.apply t task]
| Trans_list t -> Trans.apply t task | Trans_list t -> Trans.apply t task
...@@ -776,25 +776,29 @@ let rec reimport_any_goal parent gname t db_goal goal_obsolete = ...@@ -776,25 +776,29 @@ let rec reimport_any_goal parent gname t db_goal goal_obsolete =
let external_proofs = Db.external_proofs db_goal in let external_proofs = Db.external_proofs db_goal in
Db.Hprover.iter Db.Hprover.iter
(fun pid a -> (fun pid a ->
let p = let pname = Db.prover_name pid in
Util.Mstr.find (Db.prover_name pid) gconfig.provers try
in let p = Util.Mstr.find pname gconfig.provers in
let s,t,o,edit = Db.status_and_time a in let s,t,o,edit = Db.status_and_time a in
if goal_obsolete && not o then Db.set_obsolete a; if goal_obsolete && not o then Db.set_obsolete a;
let obsolete = goal_obsolete or o in let obsolete = goal_obsolete or o in
let s = match s with let s = match s with
| Db.Undone -> Model.HighFailure | Db.Undone -> Model.HighFailure
| Db.Success -> | Db.Success ->
if not obsolete then proved := true; if not obsolete then proved := true;
Model.Success Model.Success
| Db.Unknown -> Model.Unknown | Db.Unknown -> Model.Unknown
| Db.Timeout -> Model.Timeout | Db.Timeout -> Model.Timeout
| Db.Failure -> Model.HighFailure | Db.Failure -> Model.HighFailure
in in
let (_pa : Model.proof_attempt) = let (_pa : Model.proof_attempt) =
Helpers.add_external_proof_row ~obsolete ~edit goal p a s t Helpers.add_external_proof_row ~obsolete ~edit goal p a s t
in in
((* something TODO ?*)) ((* something TODO ?*))
with Not_found ->
eprintf
"Warning: prover %s appears in database but is not installed.@."
pname
) )
external_proofs; external_proofs;
let transformations = Db.transformations db_goal in let transformations = Db.transformations db_goal in
...@@ -813,13 +817,13 @@ let rec reimport_any_goal parent gname t db_goal goal_obsolete = ...@@ -813,13 +817,13 @@ let rec reimport_any_goal parent gname t db_goal goal_obsolete =
let subgoal_name = gname ^ "." ^ (string_of_int count) in let subgoal_name = gname ^ "." ^ (string_of_int count) in
let sum = task_checksum subtask in let sum = task_checksum subtask in
let subtask_db,db_subgoals = let subtask_db,db_subgoals =
try try
let g = Util.Mstr.find sum db_subgoals in let g = Util.Mstr.find sum db_subgoals in
(* a subgoal has the same check sum *) (* a subgoal has the same check sum *)
(Some g, Util.Mstr.remove sum db_subgoals) (Some g, Util.Mstr.remove sum db_subgoals)
with Not_found -> None,db_subgoals with Not_found -> None,db_subgoals
in in
((count,subgoal_name,subtask,sum,subtask_db) :: acc, ((count,subgoal_name,subtask,sum,subtask_db) :: acc,
db_subgoals, db_subgoals,
count+1)) count+1))
([],db_subgoals,1) subgoals ([],db_subgoals,1) subgoals
...@@ -830,13 +834,13 @@ let rec reimport_any_goal parent gname t db_goal goal_obsolete = ...@@ -830,13 +834,13 @@ let rec reimport_any_goal parent gname t db_goal goal_obsolete =
db_subgoals db_subgoals
[] []
in in
let other_goals = let other_goals =
List.sort (fun (s1,_) (s2,_) -> String.compare s1 s2) other_goals List.sort (fun (s1,_) (s2,_) -> String.compare s1 s2) other_goals
in in
let rec merge_goals new_goals old_goals proved acc = let rec merge_goals new_goals old_goals proved acc =
match new_goals with match new_goals with
| [] -> acc, proved | [] -> acc, proved
| (_,subgoal_name,subtask,sum,g_opt)::rem -> | (_,subgoal_name,subtask,sum,g_opt)::rem ->
let db_g,subgoal_obsolete,old_goals = let db_g,subgoal_obsolete,old_goals =
match g_opt with match g_opt with
| Some g -> g,false,old_goals | Some g -> g,false,old_goals
...@@ -844,7 +848,7 @@ let rec reimport_any_goal parent gname t db_goal goal_obsolete = ...@@ -844,7 +848,7 @@ let rec reimport_any_goal parent gname t db_goal goal_obsolete =
match old_goals with match old_goals with
| [] -> | [] ->
(* create a new goal in db *) (* create a new goal in db *)
Db.add_subgoal tr subgoal_name sum, Db.add_subgoal tr subgoal_name sum,
false, old_goals false, old_goals
| (_goal_name,g) :: r -> | (_goal_name,g) :: r ->
g, true, r g, true, r
...@@ -852,9 +856,9 @@ let rec reimport_any_goal parent gname t db_goal goal_obsolete = ...@@ -852,9 +856,9 @@ let rec reimport_any_goal parent gname t db_goal goal_obsolete =
let subgoal,subgoal_proved = let subgoal,subgoal_proved =
reimport_any_goal reimport_any_goal
(Model.Transf mtr) subgoal_name subtask db_g (Model.Transf mtr) subgoal_name subtask db_g
subgoal_obsolete subgoal_obsolete
in in
merge_goals rem old_goals (proved && subgoal_proved) merge_goals rem old_goals (proved && subgoal_proved)
(subgoal :: acc) (subgoal :: acc)
in in
let goals, subgoals_proved = let goals, subgoals_proved =
...@@ -1769,7 +1773,7 @@ let confirm_remove_row r = ...@@ -1769,7 +1773,7 @@ let confirm_remove_row r =
| Model.Row_file _file -> | Model.Row_file _file ->
info_window `ERROR "Cannot remove a file" info_window `ERROR "Cannot remove a file"
| Model.Row_proof_attempt a -> | Model.Row_proof_attempt a ->
info_window info_window
~callback:(fun () -> remove_proof_attempt a) ~callback:(fun () -> remove_proof_attempt a)
`QUESTION `QUESTION
"Do you really want to remove the selected proof attempt?" "Do you really want to remove the selected proof attempt?"
......
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