extended printing functions

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 *)
 (*

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"

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] *)
 

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 "@[<hv 2> Goal %s;@ parent %s;@ [%a]@]" name parent
-    (Pp.print_list Pp.semi (print_trans s)) l
+  fprintf fmt
+    "@[<hv 2> Goal %s;@ parent %s;@ @[<hov 2>[%a]@]@ @[<hov 2>[%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 =

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