Commit a723970c authored by Clément Fumex's avatar Clément Fumex
Browse files

fix proof state code

parent c64827ba
......@@ -41,7 +41,7 @@ type proof_state = {
pn_state : bool Hpn.t;
}
let init_proof_state () =
let init_proof_state ses =
{th_state = Hid.create 7;
tn_state = Htn.create 42;
pn_state = Hpn.create 42}
......@@ -55,18 +55,14 @@ type controller =
let create_controller env s = {
controller_session = s;
proof_state = init_proof_state ();
proof_state = init_proof_state s;
controller_env = env;
controller_provers = Whyconf.Hprover.create 7;
}
let find_tn c tid =
try Htn.find c.proof_state.tn_state tid with
| Not_found -> false
let find_pn c id =
try Hpn.find c.proof_state.pn_state id with
| Not_found -> false
let tn_proved c tid = Htn.find_def c.proof_state.tn_state false tid
let pn_proved c pid = Hpn.find_def c.proof_state.pn_state false pid
let th_proved c th = Hid.find_def c.proof_state.th_state false th
(* Update the result of the theory according to its children *)
let update_theory th ps =
......@@ -76,8 +72,8 @@ let update_theory th ps =
let rec propagate_proof c (id: Session_itp.proofNodeID) =
let tr_list = get_transformations c.controller_session id in
let new_state = List.exists (fun id -> find_tn c id) tr_list in
if new_state != find_pn c id then
let new_state = List.exists (fun id -> tn_proved c id) tr_list in
if new_state != pn_proved c id then
begin
Hpn.replace c.proof_state.pn_state id new_state;
update_proof c id
......@@ -85,8 +81,8 @@ let rec propagate_proof c (id: Session_itp.proofNodeID) =
and propagate_trans c (tid: Session_itp.transID) =
let proof_list = get_sub_tasks c.controller_session tid in
let cur_state = find_tn c tid in
let new_state = List.for_all (fun id -> find_pn c id) proof_list in
let cur_state = tn_proved c tid in
let new_state = List.for_all (fun id -> pn_proved c id) proof_list in
if cur_state != new_state then
begin
Htn.replace c.proof_state.tn_state tid new_state;
......@@ -208,7 +204,7 @@ let schedule_proof_attempt_r c id pr ~limit ~callback =
let schedule_proof_attempt c id pr ~limit ~callback =
let callback s = (match s with
| Done pr -> update_proof_node c id true
| Done pr -> update_proof_node c id (pr.Call_provers.pr_answer == Call_provers.Valid)
| Interrupted | InternalFailure _ -> update_proof_node c id false
| _ -> ());
callback s
......
......@@ -78,8 +78,10 @@ val update_proof_node: controller -> Session_itp.proofNodeID -> bool -> unit
according to the result (id,b) *)
val update_trans_node: controller -> Session_itp.transID -> bool -> unit
(** Used to find if a proof node is proved or not TODO remove *)
val find_pn: controller -> Session_itp.proofNodeID -> bool
(** Used to find if a proof/trans node or theory is proved or not *)
val tn_proved: controller -> Session_itp.transID -> bool
val pn_proved: controller -> Session_itp.proofNodeID -> bool
val th_proved: controller -> Ident.ident -> bool
module Make(S : Scheduler) : sig
......
......@@ -84,16 +84,12 @@ type session = {
session_prover_ids : int Hprover.t;
}
(*
(* TODO replace *)
let init_Hpn (s : session) (h: 'a Hpn.t) (d: 'a) : unit =
Hint.iter (fun k _pn -> Hpn.replace h k d) s.proofNode_table
let init_Htn (s : session) (h: 'a Htn.t) (d: 'a) : unit =
Hint.iter (fun k _pn -> Htn.replace h k d) s.trans_table
*)
let session_iter_proofNode f s =
Hint.iter
......
......@@ -22,6 +22,8 @@ type transID
module Hpn: Exthtbl.S with type key = proofNodeID
module Htn: Exthtbl.S with type key = transID
val init_Hpn: session ->'a Hpn.t -> 'a -> unit
val init_Htn: session ->'a Htn.t -> 'a -> unit
type theory
......@@ -36,8 +38,6 @@ type file = private {
val get_files : session -> file Stdlib.Hstr.t
(** {2 Proof trees}
Each goal
......
......@@ -365,15 +365,9 @@ let rec print_proof_node s (fmt: Format.formatter) p =
| Some pn -> pn = p
| _ -> false
in
(* TODO proved or not to be done on the whole tree. Just a test *)
let is_proved () =
match is_goal_cursor () with
| Some p -> Controller_itp.find_pn cont p
| _ -> false
in
if current_goal then
fprintf fmt "**";
if is_proved () then
if Controller_itp.pn_proved cont p then
fprintf fmt "P";
fprintf fmt
......@@ -391,10 +385,14 @@ and print_trans_node s fmt id =
let args = get_transf_args s id in
let l = get_sub_tasks s id in
let parent = (get_proof_name s (get_trans_parent s id)).Ident.id_string in
if Controller_itp.tn_proved cont id then
fprintf fmt "P";
fprintf fmt "@[<hv 2> Trans %s; args %a; parent %s;@ [%a]@]" name (Pp.print_list Pp.semi pp_print_string) args parent
(Pp.print_list Pp.semi (print_proof_node s)) l
let print_theory s fmt th : unit =
if Controller_itp.th_proved cont (theory_name th) then
fprintf fmt "P";
fprintf fmt "@[<hv 2> Theory %s;@ [%a]@]" (theory_name th).Ident.id_string
(Pp.print_list Pp.semi (fun fmt a -> print_proof_node s fmt a)) (theory_goals th)
......@@ -638,12 +636,15 @@ let interp chout fmt s =
close_out chout;
exit 0
| _ ->
try
let f = Stdlib.Hstr.find commands_table cmd in
f fmt args
with Not_found ->
printf "unknown command '%s'@." cmd
let f =
try
Some (Stdlib.Hstr.find commands_table cmd)
with Not_found ->
None
in
match f with
| Some f -> f fmt args
| None -> printf "unknown command '%s'@." cmd
let () =
printf "Welcome to Why3 shell. Type '?' for help.@.";
......
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