Commit 9482982d authored by MARCHE Claude's avatar MARCHE Claude

porting why3session to session_itp in progress

parent 6b88767e
......@@ -1125,6 +1125,7 @@ let run_auto_detection gconfig =
(*let () = Debug.dprintf debug "[GUI config] end of configuration initialization@."*)
(*
let uninstalled_prover c eS unknown =
try
Whyconf.get_prover_upgrade_policy c.config unknown
......@@ -1234,7 +1235,7 @@ let uninstalled_prover c eS unknown =
in
c.config <- set_prover_upgrade_policy c.config unknown policy;
policy
*)
(*
......
......@@ -114,8 +114,10 @@ val show_legend_window : unit -> unit
val show_about_window : unit -> unit
val preferences : t -> unit
(*
val uninstalled_prover :
t -> 'key Session.env_session -> Whyconf.prover -> Whyconf.prover_upgrade_policy
*)
(*
val unknown_prover :
......
......@@ -118,8 +118,10 @@ let init_Hpn (s : session) (h: 'a Hpn.t) (d: 'a) : unit =
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 f s.proofNode_table
*)
let session_iter_proof_attempt f s =
Hint.iter f s.proofAttempt_table
......
......@@ -65,6 +65,9 @@ type proof_attempt_node = {
proof_script : string option; (* non empty for external ITP *)
}
val theory_iter_proof_attempt:
session -> (proof_attempt_node -> unit) -> theory -> unit
val session_iter_proof_attempt:
(proofAttemptID -> proof_attempt_node -> unit) -> session -> unit
......
......@@ -72,7 +72,9 @@ let read_env_spec () =
env,config,read_simple_spec ()
let read_update_session ~allow_obsolete env config fname =
let project_dir = Server_utils.get_project_dir fname in
let q = Queue.create () in
Queue.push fname q;
let project_dir = Server_utils.get_session_dir ~allow_mkdir:false q in
let session,use_shapes = S.load_session project_dir in
(*
let ctxt = S.mk_update_context
......@@ -82,16 +84,17 @@ let read_update_session ~allow_obsolete env config fname =
in
S.update_session ~ctxt session env config
*)
let cont = Controller_itp.create_controller config env session in
let found_obs, some_merge_miss =
try
Controller_itp.reload_files cont ~use_shapes;
true, false (* TODO *)
true, false (* TODO: take allow_obsolete, return values *)
with
| e ->
Format.eprintf "%a@." Exn_printer.exn_printer e;
exit 1
in
()
cont, found_obs, some_merge_miss
(** filter *)
type filter_prover =
......@@ -206,10 +209,10 @@ let read_filter_spec whyconf : filters * bool =
status = !opt_status;
},!should_exit
let iter_proof_attempt_by_filter iter filters f session =
let iter_proof_attempt_by_filter cont iter filters f =
(* provers *)
let iter_provers a =
if C.Sprover.mem a.S.proof_prover filters.provers then f a in
if C.Sprover.mem a.S.prover filters.provers then f a in
let f = if C.Sprover.is_empty filters.provers then f else iter_provers in
(* three value *)
let three_value f v p =
......@@ -222,24 +225,36 @@ let iter_proof_attempt_by_filter iter filters f session =
(* obsolete *)
let f = three_value f filters.obsolete (fun a -> a.S.proof_obsolete) in
(* archived *)
(*
let f = three_value f filters.archived (fun a -> a.S.proof_archived) in
*)
(* verified_goal *)
let f = three_value f filters.verified_goal
(fun a -> Opt.inhabited a.S.proof_parent.S.goal_verified) in
(fun a -> Controller_itp.pn_proved cont a.S.parent) in
(* verified *)
let f = three_value f filters.verified
(fun p -> Opt.inhabited (S.proof_verified p)) in
(fun p -> match p.S.proof_state with Some Call_provers.{ pr_answer = Valid } ->
true | _ -> false) in
(* status *)
let f = if filters.status = [] then f else
(fun a -> match a.S.proof_state with
| S.Done pr when List.mem pr.Call_provers.pr_answer filters.status -> f a
| Some pr when List.mem pr.Call_provers.pr_answer filters.status -> f a
| _ -> ()) in
iter f session
iter f cont.Controller_itp.controller_session
let theory_iter_proof_attempt_by_filter cont filters f th =
iter_proof_attempt_by_filter
cont
(fun f s -> S.theory_iter_proof_attempt s f)
filters f th
let session_iter_proof_attempt_by_filter cont filters f s =
iter_proof_attempt_by_filter
cont
(fun f _s ->
S.session_iter_proof_attempt (fun _ x -> f x))
filters f s
let theory_iter_proof_attempt_by_filter filters f th =
iter_proof_attempt_by_filter S.theory_iter_proof_attempt filters f th
let session_iter_proof_attempt_by_filter filters f s =
iter_proof_attempt_by_filter S.session_iter_proof_attempt filters f s
let set_filter_verified_goal t = opt_filter_verified_goal := t
......
......@@ -63,10 +63,12 @@ val filter_spec : spec_list
val read_filter_spec : Whyconf.config -> filters * bool
val theory_iter_proof_attempt_by_filter :
Controller_itp.controller ->
filters ->
(Session_itp.proof_attempt_node -> unit) -> Session_itp.theory -> unit
val session_iter_proof_attempt_by_filter :
Controller_itp.controller ->
filters ->
(Session_itp.proof_attempt_node -> unit) -> Session_itp.session -> unit
......
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