From 53f6b14fe2995b091c43401853b0a20b8127b861 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Fri, 25 Mar 2016 09:45:39 +0100 Subject: [PATCH] extended printing functions --- examples/use_api/itp.ml | 102 ++++++++++++++++----------------- src/session/controller_itp.ml | 18 +++++- src/session/controller_itp.mli | 5 +- src/session/session_itp.ml | 41 ++++++------- src/session/session_itp.mli | 4 +- 5 files changed, 90 insertions(+), 80 deletions(-) diff --git a/examples/use_api/itp.ml b/examples/use_api/itp.ml index 689386767..b4f9e7736 100644 --- a/examples/use_api/itp.ml +++ b/examples/use_api/itp.ml @@ -46,6 +46,8 @@ let provers : Whyconf.config_prover Whyconf.Mprover.t = (* builds the environment from the [loadpath] *) let env : Env.env = Env.create_env (Whyconf.loadpath main) +open Format + (* loading the drivers *) let provers = Whyconf.Mprover.fold @@ -62,85 +64,77 @@ let provers = provers [] -open Session_itp;; -open Format;; - -let (s,b) = Session_itp.load_session "../bitwalker/why3session.xml";; - -let th = Session_itp.get_theories s;; - -let (_,_,id) = match th with - (n, (thn, _::_::x::_)::_)::_ -> (n,thn,x);; +(* One prover named Alt-Ergo in the config file *) +let alt_ergo : Whyconf.config_prover = + let fp = Whyconf.parse_filter_prover "Alt-Ergo" in + (** all provers that have the name "Alt-Ergo" *) + let provers = Whyconf.filter_provers config fp in + if Whyconf.Mprover.is_empty provers then begin + eprintf "Prover Alt-Ergo not installed or not configured@."; + exit 0 + end else + snd (Whyconf.Mprover.max_binding provers) -let t = Session_itp.get_tree s id;; -printf "%a@." (print_tree s) t;; +(** Testing Session_itp *) -(* let n = Session_itp.get_node s 19;; +let (s,b) = Session_itp.load_session "../bitwalker/why3session.xml" -let s' = Session_itp.graft_transf s n "blabla" [] [];; +let id = + match Session_itp.get_theories s with + | (n, (thn, _::_::x::_)::_)::_ -> x + | _ -> assert false -let t = Session_itp.get_tree s;; - -let _ = Session_itp.remove_transformation s s';; +let () = + printf "%a@." (Session_itp.print_tree s) (Session_itp.get_tree s id) -let _ = remove_transformation s (get_trans s 15);; +let pid = Session_itp.graft_proof_attempt s id alt_ergo.Whyconf.prover ~timelimit:42 -let t = Session_itp.get_tree s;; +let () = + printf "%a@." (Session_itp.print_tree s) (Session_itp.get_tree s id) -let my_session = Session_itp.empty_session "test.xml";; -let s' = Session_itp.graft_transf s n "blabla" [] [];; +(** Testing Controller_itp *) - let t = Session_itp.get_tree s;; *) - -(* excerpt from src/session/session.ml *) - let read_file env ?format fn = - let theories = Env.read_file Env.base_language env ?format fn in - let ltheories = - Stdlib.Mstr.fold - (fun name th acc -> - (* Hack : with WP [name] and [th.Theory.th_name.Ident.id_string] *) - let th_name = - Ident.id_register (Ident.id_derive name th.Theory.th_name) in - match th.Theory.th_name.Ident.id_loc with - | Some l -> (l,th_name,th)::acc - | None -> (Loc.dummy_position,th_name,th)::acc) - theories [] - in - let th = List.sort - (fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2) - ltheories - in - List.map (fun (_,_,a) -> a) th;; - -let my_session = empty_session ();; +let my_session = Session_itp.empty_session () (* adds a file in the new session *) -let file : unit (* Session_itp.file *) = +let () = let fname = "../logic/hello_proof.why" in try - let theories = read_file env fname in - add_file_section my_session fname theories None; + Controller_itp.add_file_to_session env my_session fname with e -> eprintf "@[Error while reading file@ '%s':@ %a@.@]" fname Exn_printer.exn_printer e; - exit 1;; + exit 1 (* explore the theories in that file *) -let theories = get_theories my_session;; +let theories = Session_itp.get_theories my_session + let () = eprintf "%d theories found@." (List.length theories) -let (_,_,id) = match theories with - (n, (thn, x::_)::_)::_ -> (n,thn,x);; +let id = match theories with + | (n, (thn, x::_)::_)::_ -> x + | _ -> assert false -let t = Session_itp.get_tree my_session id;; +let () = Session_itp.print_session my_session -print_session my_session;; +let _id = Session_itp.graft_transf my_session id "toto" [] -let l = graft_transf my_session id "toto" [] [];; +let () = + printf "%a@." (Session_itp.print_tree my_session) + (Session_itp.get_tree my_session id) -printf "%a@." (print_tree my_session) t;; +let () = + let callback st = + printf "callback called with Status = %a@." Controller_itp.print_status st + in + Controller_itp.schedule_proof_attempt my_session id alt_ergo.Whyconf.prover + ~timelimit:5 ~callback + +let () = + printf "%a@." (Session_itp.print_tree my_session) + (Session_itp.get_tree my_session id) (* add proof attempts for each goals in the theories *) (* diff --git a/src/session/controller_itp.ml b/src/session/controller_itp.ml index abe14866f..28c43fe56 100644 --- a/src/session/controller_itp.ml +++ b/src/session/controller_itp.ml @@ -10,7 +10,20 @@ type proof_attempt_status = | Done of Call_provers.prover_result (** external proof done *) | InternalFailure of exn (** external proof aborted by internal error *) -type transformation_status = TSscheduled of transID | TSdone of transID | TSfailed +open Format + +let print_status fmt st = + match st with + | Unedited -> fprintf fmt "Unedited" + | JustEdited -> fprintf fmt "JustEdited" + | Interrupted -> fprintf fmt "Interrupted" + | Scheduled -> fprintf fmt "Scheduled" + | Running -> fprintf fmt "Running" + | Done r -> fprintf fmt "Done(%a)" Call_provers.print_prover_result r + | InternalFailure e -> fprintf fmt "InternalFailure(%a)" Exn_printer.exn_printer e + +type transformation_status = + | TSscheduled of transID | TSdone of transID | TSfailed let schedule_proof_attempt s id pr ~timelimit ~callback = graft_proof_attempt s id pr ~timelimit; @@ -42,3 +55,6 @@ let read_file env ?format fn = let add_file_to_session env s ?format fname = let theories = read_file env ?format fname in add_file_section s fname theories None + +let reload_session_files (_s : session) = + failwith "Controller_itp.reload_session_files not yet implemented" diff --git a/src/session/controller_itp.mli b/src/session/controller_itp.mli index dd3730a81..ff6c3cb17 100644 --- a/src/session/controller_itp.mli +++ b/src/session/controller_itp.mli @@ -21,6 +21,8 @@ type proof_attempt_status = | Done of Call_provers.prover_result (** external proof done *) | InternalFailure of exn (** external proof aborted by internal error *) +val print_status : Format.formatter -> proof_attempt_status -> unit + val schedule_proof_attempt : session -> proofNodeID -> @@ -46,7 +48,8 @@ val schedule_transformations : the transformation status changes. Typically at Scheluded, then Done tid.*) -val add_file_to_session : Env.env -> session -> string -> unit +val add_file_to_session : + Env.env -> session -> ?format:Env.fformat -> string -> unit (** [add_file_to_session env s ?fmt fname] parses the source file [fname] and add the resulting theories to the session [s] *) diff --git a/src/session/session_itp.ml b/src/session/session_itp.ml index 7a6e09b51..ff6b1e292 100644 --- a/src/session/session_itp.ml +++ b/src/session/session_itp.ml @@ -74,12 +74,16 @@ type file = { type tree = Tree of - (proofNodeID * string * (transID * string * tree list) list) + (proofNodeID * string + * proof_attempt list * (transID * string * tree list) list) let rec get_tree s id : tree = let t = Hint.find s.proofNode_table id in + let pal = + Hprover.fold (fun p pa acc -> pa.proofa_attempt::acc) t.proofn_attempts [] + in let trl = List.map (get_trans s) t.proofn_transformations in - Tree (id, t.proofn_name.Ident.id_string, trl) + Tree (id, t.proofn_name.Ident.id_string, pal, trl) and get_trans s id = let tr = Hint.find s.trans_table id in @@ -132,14 +136,23 @@ let get_sub_tasks (s : session) (id : transID) = open Format open Ident -let rec print_tree s fmt (Tree (id, name, l)) = +let print_proof_attempt fmt pa = + fprintf fmt "%a tl=%d %a" + Whyconf.print_prover pa.prover + pa.timelimit + (Pp.print_option Call_provers.print_prover_result) pa.proof_state + +let rec print_tree s fmt (Tree (id, name, pal ,trl)) = let pn = get_proofNode s id in let parent = match pn.proofn_parent with | Theory t -> t.theory_name.id_string | Trans id -> (get_transfNode s id).transf_name in - fprintf fmt "@[ Goal %s;@ parent %s;@ [%a]@]" name parent - (Pp.print_list Pp.semi (print_trans s)) l + fprintf fmt + "@[ Goal %s;@ parent %s;@ @[[%a]@]@ @[[%a]@]@]" + name parent + (Pp.print_list Pp.semi print_proof_attempt) pal + (Pp.print_list Pp.semi (print_trans s)) trl and print_trans s fmt (id, name, l) = let tn = get_transfNode s id in @@ -592,24 +605,6 @@ let load_session (file : string) = session, use_shapes (* add a why file from a session *) -(** Read file and sort theories by location *) -let read_file env ?format fn = - let theories = Env.read_file Env.base_language env ?format fn in - let ltheories = - Mstr.fold - (fun name th acc -> - (* Hack : with WP [name] and [th.Theory.th_name.Ident.id_string] *) - let th_name = - Ident.id_register (Ident.id_derive name th.Theory.th_name) in - match th.Theory.th_name.Ident.id_loc with - | Some l -> (l,th_name,th)::acc - | None -> (Loc.dummy_position,th_name,th)::acc) - theories [] - in - List.sort - (fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2) - ltheories,theories - let add_file_section (s:session) (fn:string) (theories:Theory.theory list) format : unit = let add_theory acc (th : Theory.theory) = let add_goal parent goal id = diff --git a/src/session/session_itp.mli b/src/session/session_itp.mli index a57c65d7e..a4faa0e1b 100644 --- a/src/session/session_itp.mli +++ b/src/session/session_itp.mli @@ -16,7 +16,9 @@ type trans_arg type tree = Tree of - (proofNodeID * string * (transID * string * tree list) list) + (proofNodeID * string + * proof_attempt list (* proof attempts in this node *) + * (transID * string * tree list) list) (* transformation in this node *) val get_theories : session -> (string * (string * proofNodeID list) list) list (** [get_theories s] returns a list of pairs [name,l] where [name] is a -- GitLab