test new sessions API

examples/use_api/itp.ml

+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
+(*******************
+
+Small text-based interactive prover using new Why3 session format, to be run in OCaml toplevel.
+
+******************)
+
+(*
+
+#load "unix.cma";;
+#load "nums.cma";;
+#load "dynlink.cma";;
+#load "str.cma";;
+#directory "+../menhirLib";;
+#load "menhirLib.cmo";;
+
+#directory "+../zip";;
+#load "zip.cma";;
+
+#directory "../../lib/why3";;
+#load_rec "why3.cma";;
+
+ *)
+
+open Format
+
+
+(* opening the Why3 library *)
+open Why3
+
+(* access to the Why configuration *)
+
+(* reads the config file *)
+let config : Whyconf.config = Whyconf.read_config None
+(* the [main] section of the config file *)
+let main : Whyconf.main = Whyconf.get_main config
+(* all the provers detected, from the config file *)
+let provers : Whyconf.config_prover Whyconf.Mprover.t =
+  Whyconf.get_provers config
+
+(* builds the environment from the [loadpath] *)
+let env : Env.env = Env.create_env (Whyconf.loadpath main)
+
+(* loading the drivers *)
+let provers =
+  Whyconf.Mprover.fold
+    (fun _ p acc ->
+      try
+        let d = Driver.load_driver env p.Whyconf.driver [] in
+        (p,d)::acc
+      with e ->
+        let p = p.Whyconf.prover in
+        eprintf "Failed to load driver for %s %s: %a@."
+          p.Whyconf.prover_name p.Whyconf.prover_version
+          Exn_printer.exn_printer e;
+        exit 1)
+    provers
+    []
+
+
+let (s,b) = Session_itp.load_session "../bitwalker/why3session.xml"
+
+let t = Session_itp.get_tree s;;
+
+let my_session = Session_itp.empty_session "test.xml";;
+
+(* 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
+  List.sort
+    (fun (l1,_,_) (l2,_,_) -> Loc.compare l1 l2)
+    ltheories,theories
+
+(* adds a file in the new session *)
+let file : unit (* Session_itp.file *) =
+  let fname = "../logic/hello_proof.why" in
+  try
+    let ordered_theories,theories = read_file env fname in
+    Session_itp.add_file my_session fname ordered_theories;
+  with e ->
+    eprintf "@[Error while reading file@ '%s':@ %a@.@]" fname
+      Exn_printer.exn_printer e;
+    exit 1
+
+
+
+
+
+(* explore the theories in that file *)
+let theories = file.Session.file_theories
+let () = eprintf "%d theories found@." (List.length theories)
+
+(* add proof attempts for each goals in the theories *)
+
+let add_proofs_attempts g =
+  List.iter
+    (fun (p,d) ->
+      let _pa : unit Session.proof_attempt =
+        Session.add_external_proof
+          ~keygen:dummy_keygen
+          ~obsolete:true
+          ~archived:false
+          ~timelimit:5
+	  ~steplimit:(-1)
+          ~memlimit:1000
+          ~edit:None
+          g p.Whyconf.prover Session.Scheduled
+      in ())
+    provers
+
+let () =
+  List.iter
+    (fun th -> List.iter add_proofs_attempts th.Session.theory_goals)
+    theories
+
+(* save the session on disk *)
+let () = Session.save_session config env_session.Session.session

src/session/session_itp.ml

@@ -73,6 +73,36 @@ type file = {
   session_file_name             : string;
 }
 
+type tree =
+  Tree of
+    (int * string * int * (int * string * int * tree list) list)
+
+let rec get_goal s id : tree =
+  let t = Hint.find s.proofNode_table id in
+  let parent = match t.proofn_parent with
+    | Theory _ -> -1
+    | Trans n -> n
+  in
+  let trl = List.map (get_trans s) t.proofn_transformations in
+  Tree (id,t.proofn_name.Ident.id_string,parent,trl)
+
+and get_trans s id =
+  let tr = Hint.find s.trans_table id in
+  (id,tr.transf_name,tr.transf_parent,List.map (get_goal s) tr.transf_subtasks)
+
+let get_tree s =
+  Hstr.fold
+    (fun fn f acc ->
+     let c =
+       List.map
+         (fun th ->
+          let goals = List.map (get_goal s) th.theory_goals in
+          (th.theory_name.Ident.id_string,goals))
+         f.file_theories
+     in
+     (fn,c) :: acc)
+    s.session_files []
+
 let gen_transID (s : session) =
   let id = s.next_transID in
   s.next_transID <- id + 1;
@@ -109,6 +139,29 @@ let empty_session ?shape_version (file : string) =
     session_file_name = file;
   }
 
+let add_file_section (s:session) (fn:string) ?format (ths:Theory.theory list): unit =
+  let theories = []
+(*
+    List.rev_map
+      (fun (_,thname,th) ->
+       let tasks =
+         List.rev_map
+           (fun t -> t)
+           (Task.split_theory th None None)
+       in
+       { theory_name     = thname;
+         theory_checksum = None;
+         theory_goals    = tasks }) ths
+ *)
+  in
+  let f = { file_name = fn;
+            file_format = format;
+            file_theories = List.rev theories }
+  in
+  Hstr.add s.session_files fn f
+
+exception BadID
+
 let graft_proof_attempt (s : session) (id : proofNodeID) (pa : proof_attempt) =
   let pn = get_proofNode s id in
   let node = { proofa_parent = id; proofa_attempt = pa } in

src/session/session_itp.mli

 type session
-
 type transID
 type proofNodeID
 type proof_attempt
 type trans_arg
 
-(* (\** New Proof sessions ("Refectoire") *\) *)
+(* New Proof sessions ("Refectoire") *)
 
 (* note: la fonction register des transformations doit permettre de
    declarer les types des arguments
@@ -15,7 +14,22 @@ type trans_arg
 
 *)
 
-(* Note for big brother Andrei: grafting is the oposite of pruning *)
+type tree =
+  Tree of
+    (int * string * int * (int * string * int * tree list) list)
+
+val get_tree : session -> (string * (string * tree list) list) list
+
+(* Note for big brother Andrei: grafting is the opposite of pruning *)
+
+val empty_session : ?shape_version:int -> string -> session
+
+val add_file_section :
+  session -> string -> ?format:string -> Theory.theory list -> unit
+(** [add_file_section s fn ths] adds a new 'file' section in session
+    [s], named [fn], containing fresh theory subsections corresponding
+    to theories [ths]. The tasks of each theory nodes generated are
+    computed using [Task.split_theory] *)
 
 val graft_proof_attempt : session -> proofNodeID -> proof_attempt -> unit
 (** [graft_proof_attempt s id pa] adds the proof attempt [pa] as a
@@ -28,6 +42,8 @@ val graft_transf : session -> proofNodeID -> string -> trans_arg list ->
     argument of the transformation; [tl] is the resulting list of
     tasks *)
 
+
+(*
 val remove_proof_attempt : session -> proofNodeID -> Whyconf.prover -> unit
 (** [remove_proof_attempt s id pr] removes the proof attempt from the
     prover [pr] from the proof node [id] of the session [s] *)
@@ -36,12 +52,18 @@ val remove_transformation : session -> transID -> unit
 (** [remove_transformation s id] removes the transformation [id]
     from the session [s] *)
 
-(* val save_session : string -> session -> unit *)
+(*
+val save_session : string -> session -> unit
+ *)
 (** [save_session f s] Save the session [s] in file [f] *)
+ *)
+
 
 val load_session : string -> session * bool
 (** [load_session f] load a session from a file [f]; all the tasks are
     initialised to None *)
+
+
 (*
 
   couche au-dessus: "scheduler" cad modifications asynchrones de la