session.ml

(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-2012                                               *)
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
(*    Guillaume Melquiond                                                 *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

open Stdlib
open Debug
open Util

module Mprover = Whyconf.Mprover
module Sprover = Whyconf.Sprover
module PHprover = Whyconf.Hprover
module C = Whyconf
module Tc = Termcode

let debug = Debug.register_flag "session"
  ~desc:"About the why3 session creation, reading and writing."

(** {2 Type definitions} *)

module PHstr = Util.Hstr

type undone_proof =
    | Scheduled (** external proof attempt is scheduled *)
    | Interrupted
    | Running (** external proof attempt is in progress *)
    | Unedited
    | JustEdited

type proof_attempt_status =
    | Undone of undone_proof
    | Done of Call_provers.prover_result (** external proof done *)
    | InternalFailure of exn (** external proof aborted by internal error *)

type task_option = Task.task option

type 'a goal =
  { mutable goal_key  : 'a;
    goal_name : Ident.ident;
    goal_expl : string option;
    goal_parent : 'a goal_parent;
    mutable goal_checksum : Tc.checksum;
    mutable goal_shape : Tc.shape;
    mutable goal_verified : bool;
    goal_task: task_option;
    mutable goal_expanded : bool;
    goal_external_proofs : 'a proof_attempt PHprover.t;
    goal_transformations : 'a transf PHstr.t;
  }

and 'a proof_attempt =
  { proof_key : 'a;
    mutable proof_prover : Whyconf.prover;
    proof_parent : 'a goal;
    mutable proof_state : proof_attempt_status;
    mutable proof_timelimit : int;
    mutable proof_memlimit : int;
    mutable proof_obsolete : bool;
    mutable proof_archived : bool;
    mutable proof_edited_as : string option;
  }

and 'a goal_parent =
  | Parent_theory of 'a theory
  | Parent_transf of 'a transf

and 'a transf =
    { mutable transf_key : 'a;
      transf_name : string;
      (** Why3 tranformation name *)
      transf_parent : 'a goal;
      mutable transf_verified : bool;
      mutable transf_goals : 'a goal list;
      (** Not mutated after the creation of the session *)
      mutable transf_expanded : bool;
    }

and 'a theory =
    { mutable theory_key : 'a;
      theory_name : Ident.ident;
      theory_parent : 'a file;
      mutable theory_goals : 'a goal list;
      mutable theory_verified : bool;
      mutable theory_expanded : bool;
    }

and 'a file =
    { mutable file_key : 'a;
      file_name : string;
      file_format : string option;
      file_parent : 'a session;
      mutable file_theories: 'a theory list;
      (** Not mutated after the creation *)
      mutable file_verified : bool;
      mutable file_expanded : bool;
    }

and 'a session =
    { session_files : 'a file PHstr.t;
      mutable session_shape_version : int;
      session_dir   : string; (** Absolute path *)
    }

type loaded_prover =
    { prover_config : Whyconf.config_prover;
      prover_driver : Driver.driver}

type loaded_provers = loaded_prover option PHprover.t

type 'a env_session =
    { env : Env.env;
      mutable whyconf : Whyconf.config;
      loaded_provers : loaded_provers;
      session : 'a session}

let update_env_session_config e c = e.whyconf <- c

(*************************)
(**       Iterators      *)
(*************************)
type 'a any =
  | File of 'a file
  | Theory of 'a theory
  | Goal of 'a goal
  | Proof_attempt of 'a proof_attempt
  | Transf of 'a transf

let rec goal_iter_proof_attempt f g =
  PHprover.iter (fun _ a -> f a) g.goal_external_proofs;
  PHstr.iter (fun _ t -> transf_iter_proof_attempt f t) g.goal_transformations

and transf_iter_proof_attempt f t =
  List.iter (goal_iter_proof_attempt f) t.transf_goals

let theory_iter_proof_attempt f t =
  List.iter (goal_iter_proof_attempt f) t.theory_goals

let file_iter_proof_attempt f t =
  List.iter (theory_iter_proof_attempt f) t.file_theories

let session_iter_proof_attempt f s =
  PHstr.iter (fun _ file -> file_iter_proof_attempt f file) s.session_files

let rec iter_proof_attempt f = function
    | Goal g -> goal_iter_proof_attempt f g
    | Theory th -> theory_iter_proof_attempt f th
    | File file -> file_iter_proof_attempt f file
    | Proof_attempt a -> f a
    | Transf tr -> transf_iter_proof_attempt f tr

let rec goal_iter_leaf_goal ~unproved_only f g =
  if not (g.goal_verified && unproved_only) then
    let r = ref true in
    PHstr.iter
      (fun _ t -> r := false;
        List.iter (goal_iter_leaf_goal ~unproved_only f) t.transf_goals)
      g.goal_transformations;
    if !r then f g

(** iterators not reccursive *)
let iter_goal fp ft g =
  PHprover.iter (fun _ a -> fp a) g.goal_external_proofs;
  PHstr.iter (fun _ t -> ft t) g.goal_transformations

let iter_transf f t =
  List.iter (fun g -> f g) t.transf_goals

let goal_iter f g =
  PHprover.iter
    (fun _ a -> f (Proof_attempt a)) g.goal_external_proofs;
  PHstr.iter (fun _ t -> f (Transf t)) g.goal_transformations

let transf_iter f t =
  List.iter (fun g -> f (Goal g)) t.transf_goals

let theory_iter f t =
  List.iter (fun g -> f (Goal g)) t.theory_goals

let file_iter f t =
  List.iter (fun th -> f (Theory th)) t.file_theories

let session_iter f s =
  PHstr.iter (fun _ file -> f (File file)) s.session_files

let iter f = function
    | Goal g -> goal_iter f g
    | Theory th -> theory_iter f th
    | File file -> file_iter f file
    | Proof_attempt _ -> ()
    | Transf tr -> transf_iter f tr

(** Print session *)


module PTreeT = struct
  type 'a t = | Any of 'a any | Session of 'a session
  let decomp = function
    | Any t ->
      let s = match t with
        | File f ->
          if f.file_verified
          then f.file_name
          else f.file_name^"?"
        | Theory th ->
          if th.theory_verified
          then th.theory_name.Ident.id_string
          else th.theory_name.Ident.id_string^"?"
        | Goal g ->
          if g.goal_verified
          then g.goal_name.Ident.id_string
          else g.goal_name.Ident.id_string^"?"
        | Proof_attempt pr ->
          Pp.sprintf_wnl "%a%s%s%s%s"
            Whyconf.print_prover pr.proof_prover
            (match pr.proof_state with
              | Done { Call_provers.pr_answer = Call_provers.Valid} -> ""
              | InternalFailure _ -> "!"
              | _ -> "?")
            (if pr.proof_obsolete || pr.proof_archived then " " else "")
            (if pr.proof_obsolete then "O" else "")
            (if pr.proof_archived then "A" else "")
        | Transf tr ->
          if tr.transf_verified
          then tr.transf_name
          else tr.transf_name^"?" in
      let l = ref [] in
      iter (fun a -> l := (Any a)::!l) t;
      s,!l
    | Session s ->
      let l = ref [] in
      session_iter (fun a -> l := (Any a)::!l) s;
      Filename.basename s.session_dir,!l

end

module PTree = Print_tree.PMake(PTreeT)

let print_any fmt any = PTree.print fmt (PTreeT.Any any)

let print_session fmt s = PTree.print fmt (PTreeT.Session s)

(** 2 Create a session *)

let empty_session ?shape_version dir =
  let shape_version = match shape_version with
    | Some v -> v
    | None -> Termcode.current_shape_version
  in
  { session_files = PHstr.create 3;
    session_shape_version = shape_version;
    session_dir   = dir;
  }

let create_session ?shape_version project_dir =
  if not (Sys.file_exists project_dir) then
    begin
      dprintf debug
        "[Info] '%s' does not exists. Creating directory of that name \
 for the project@." project_dir;
      Unix.mkdir project_dir 0o777
    end;
  empty_session ?shape_version project_dir


let load_env_session ?(includes=[]) session conf_path_opt =
  let config = Whyconf.read_config conf_path_opt in
  let loadpath = (Whyconf.loadpath (Whyconf.get_main config)) @ includes in
  let env = Env.create_env loadpath in
  { session = session;
    env = env;
    whyconf = config;
    loaded_provers = PHprover.create 5;
  }

(************************)
(* session accessor     *)
(************************)

let get_session_file file = file.file_parent

let get_session_theory th = get_session_file th.theory_parent

let rec get_session_goal goal =
  match goal.goal_parent with
    | Parent_transf trans -> get_session_trans trans
    | Parent_theory th    -> get_session_theory th

and get_session_trans transf = get_session_goal transf.transf_parent

let get_session_proof_attempt pa = get_session_goal pa.proof_parent

let get_used_provers session =
  let sprover = ref Sprover.empty in
  session_iter_proof_attempt
    (fun pa -> sprover := Sprover.add pa.proof_prover !sprover)
    session;
  !sprover

exception NoTask

let goal_task g = Util.exn_option NoTask g.goal_task
let goal_task_option g = g.goal_task

let goal_expl g = Util.def_option g.goal_name.Ident.id_string g.goal_expl

(************************)
(* saving state on disk *)
(************************)
open Format

let db_filename = "why3session.xml"

let save_string fmt s =
  for i=0 to String.length s - 1 do
    match String.get s i with
      | '\"' -> pp_print_string fmt "&quot;"
      | '\'' -> pp_print_string fmt "&apos;"
      | '<' -> pp_print_string fmt "&lt;"
      | '>' -> pp_print_string fmt "&gt;"
      | '&' -> pp_print_string fmt "&amp;"
      | c -> pp_print_char fmt c
  done


let save_result fmt r =
  fprintf fmt "@\n<result status=\"%s\" time=\"%.2f\"/>"
    (match r.Call_provers.pr_answer with
       | Call_provers.Valid -> "valid"
       | Call_provers.Failure _ -> "failure"
       | Call_provers.Unknown _ -> "unknown"
       | Call_provers.HighFailure -> "highfailure"
       | Call_provers.Timeout -> "timeout"
       | Call_provers.OutOfMemory -> "outofmemory"
       | Call_provers.Invalid -> "invalid")
    r.Call_provers.pr_time

let save_status fmt s =
  match s with
    | Undone Unedited ->
        fprintf fmt "<unedited/>@\n"
    | Undone _ ->
        fprintf fmt "<undone/>@\n"
    | InternalFailure msg ->
        fprintf fmt "<internalfailure reason=\"%a\"/>@\n"
          save_string (Printexc.to_string msg)
    | Done r -> save_result fmt r


let opt lab fmt = function
  | None -> ()
  | Some s -> fprintf fmt "%s=\"%a\"@ " lab save_string s

let save_proof_attempt provers fmt _key a =
  fprintf fmt
    "@\n@[<v 1><proof@ prover=\"%i\"@ timelimit=\"%d\"@ \
memlimit=\"%d\"@ %aobsolete=\"%b\"@ archived=\"%b\">"
    (Mprover.find a.proof_prover provers) a.proof_timelimit
    a.proof_memlimit
    (opt "edited") a.proof_edited_as a.proof_obsolete
    a.proof_archived;
  save_status fmt a.proof_state;
  fprintf fmt "@]@\n</proof>"

let save_ident fmt id =
  fprintf fmt "name=\"%a\"" save_string id.Ident.id_string;
  match id.Ident.id_loc with
    | None -> ()
    | Some loc ->
      let file,lnum,cnumb,cnume = Loc.get loc in
      fprintf fmt
        "@ locfile=\"%a\"@ loclnum=\"%i\" loccnumb=\"%i\" loccnume=\"%i\""
        save_string file lnum cnumb cnume

let save_label fmt s =
  fprintf fmt "@\n@[<v 1><label@ name=\"%a\"/>@]" save_string s.Ident.lab_string

let rec save_goal provers fmt g =
  assert (Tc.string_of_shape g.goal_shape <> "");
  fprintf fmt
    "@\n@[<v 1><goal@ %a@ %asum=\"%a\"@ proved=\"%b\"@ \
expanded=\"%b\"@ shape=\"%a\">"
    save_ident g.goal_name
    (opt "expl") g.goal_expl
    save_string (Tc.string_of_checksum g.goal_checksum)
    g.goal_verified  g.goal_expanded
    save_string (Tc.string_of_shape g.goal_shape);
  Ident.Slab.iter (save_label fmt) g.goal_name.Ident.id_label;
  PHprover.iter (save_proof_attempt provers fmt) g.goal_external_proofs;
  PHstr.iter (save_trans provers fmt) g.goal_transformations;
  fprintf fmt "@]@\n</goal>"

and save_trans provers fmt _ t =
  fprintf fmt "@\n@[<v 1><transf@ name=\"%a\"@ proved=\"%b\"@ expanded=\"%b\">"
    save_string t.transf_name t.transf_verified t.transf_expanded;
  List.iter (save_goal provers fmt) t.transf_goals;
  fprintf fmt "@]@\n</transf>"

let save_theory provers fmt t =
  fprintf fmt
    "@\n@[<v 1><theory@ %a@ verified=\"%b\"@ expanded=\"%b\">"
    save_ident t.theory_name
    t.theory_verified t.theory_expanded;
  Ident.Slab.iter (save_label fmt) t.theory_name.Ident.id_label;
  List.iter (save_goal provers fmt) t.theory_goals;
  fprintf fmt "@]@\n</theory>"

let save_file provers fmt _ f =
  fprintf fmt
    "@\n@[<v 1><file@ name=\"%a\"@ %averified=\"%b\"@ expanded=\"%b\">"
    save_string f.file_name (opt "format")
    f.file_format f.file_verified f.file_expanded;
  List.iter (save_theory provers fmt) f.file_theories;
  fprintf fmt "@]@\n</file>"

let save_prover fmt p (provers,id) =
  fprintf fmt "@\n@[<v 1><prover@ id=\"%i\"@ \
name=\"%a\"@ version=\"%a\"%a/>@]"
    id save_string p.C.prover_name save_string p.C.prover_version
    (fun fmt s -> if s <> "" then fprintf fmt "@ alternative=\"%a\""
        save_string s)
    p.C.prover_altern;
  Mprover.add p id provers, id+1

let save fname config session =
  let ch = open_out fname in
  let fmt = formatter_of_out_channel ch in
  fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
  fprintf fmt "<!DOCTYPE why3session SYSTEM \"%a\">@\n"
    save_string (Filename.concat (Whyconf.datadir (Whyconf.get_main config))
                   "why3session.dtd");
  fprintf fmt "@[<v 1><why3session@ name=\"%a\" shape_version=\"%d\">"
    save_string fname session.session_shape_version;
  let provers,_ = Sprover.fold (save_prover fmt) (get_used_provers session)
    (Mprover.empty,0) in
  PHstr.iter (save_file provers fmt) session.session_files;
  fprintf fmt "@]@\n</why3session>";
  fprintf fmt "@.";
  close_out ch

let save_session config session =
  let f = Filename.concat session.session_dir db_filename in
  Sysutil.backup_file f;
  save f config session

(*******************************)
(*          explanations       *)
(*******************************)

let expl_regexp = Str.regexp "expl:\\(.*\\)"

exception Found of string

let check_expl lab =
  let lab = lab.Ident.lab_string in
  if Str.string_match expl_regexp lab 0 then
    raise (Found (Str.matched_group 1 lab))

let rec get_expl_fmla f =
  Ident.Slab.iter check_expl f.Term.t_label;
  (match f.Term.t_node with
    | Term.Tbinop(Term.Timplies,_,f) -> get_expl_fmla f
    | Term.Tquant(Term.Tforall,fq) ->
      let (_,_,f) = Term.t_open_quant fq in get_expl_fmla f
    | Term.Tlet(_,fb) ->
      let (_,f) = Term.t_open_bound fb in get_expl_fmla f
    | Term.Tcase(_,[fb]) ->
      let (_,f) = Term.t_open_branch fb in get_expl_fmla f
    | _ -> ())

type expl = string option

let get_explanation id task =
  let fmla = Task.task_goal_fmla task in
  try
    get_expl_fmla fmla;
    Ident.Slab.iter check_expl id.Ident.id_label;
    None
  with Found e -> Some e


(*****************************)
(*   update verified field   *)
(*****************************)
type 'a notify = 'a any -> unit
let notify : 'a notify = fun _ -> ()

let file_verified f =
  List.for_all (fun t -> t.theory_verified) f.file_theories

let theory_verified t =
  List.for_all (fun g -> g.goal_verified) t.theory_goals

let transf_verified t =
  List.for_all (fun g -> g.goal_verified) t.transf_goals

let proof_verified a =
  (not a.proof_obsolete) &&
    match a.proof_state with
      | Done { Call_provers.pr_answer = Call_provers.Valid} -> true
      | _ -> false

let goal_verified g =
    try
      PHprover.iter
        (fun _ a ->
          if proof_verified a
          then raise Exit)
        g.goal_external_proofs;
      PHstr.iter
        (fun _ t -> if t.transf_verified then raise Exit)
        g.goal_transformations;
      false
    with Exit -> true

let check_file_verified notify f =
  let b = file_verified f in
  if f.file_verified <> b then begin
    f.file_verified <- b;
    notify (File f)
  end

let check_theory_proved notify t =
  let b = theory_verified t in
  if t.theory_verified <> b then begin
    t.theory_verified <- b;
    notify (Theory t);
    check_file_verified notify t.theory_parent
  end

let rec check_goal_proved notify g =
  let b = goal_verified g in
  if g.goal_verified <> b then begin
    g.goal_verified <- b;
    notify (Goal g);
    match g.goal_parent with
      | Parent_theory t -> check_theory_proved notify t
      | Parent_transf t -> check_transf_proved notify t
  end

and check_transf_proved notify t =
  let b = transf_verified t in
  if t.transf_verified <> b then begin
    t.transf_verified <- b;
    notify (Transf t);
    check_goal_proved notify t.transf_parent
  end

(******************************)
(* raw additions to the model *)
(******************************)
type 'a keygen = ?parent:'a -> unit -> 'a

let add_external_proof
    ?(notify=notify)
    ~(keygen:'a keygen) ~obsolete
    ~archived ~timelimit ~memlimit ~edit (g:'a goal) p result =
  assert (edit <> Some "");
  let key = keygen ~parent:g.goal_key () in
  let a = { proof_prover = p;
            proof_parent = g;
            proof_key = key;
            proof_obsolete = obsolete;
            proof_archived = archived;
            proof_state = result;
            proof_timelimit = timelimit;
            proof_memlimit = memlimit;
            proof_edited_as = edit;
          }
  in
  PHprover.replace g.goal_external_proofs p a;
  check_goal_proved notify g;
  a

let remove_external_proof ?(notify=notify) a =
  let g = a.proof_parent in
  PHprover.remove g.goal_external_proofs a.proof_prover;
  check_goal_proved notify g


let set_proof_state ?(notify=notify) ~obsolete ~archived res a =
  a.proof_state <- res;
  a.proof_obsolete <- obsolete;
  a.proof_archived <- archived;
  notify (Proof_attempt a);
  check_goal_proved notify a.proof_parent

let change_prover a p =
  let g = a.proof_parent in
  PHprover.remove g.goal_external_proofs a.proof_prover;
  PHprover.add g.goal_external_proofs p a;
  a.proof_prover <- p;
  a.proof_obsolete <- true

let set_edited_as edited_as a = a.proof_edited_as <- edited_as

let set_timelimit timelimit a = a.proof_timelimit <- timelimit
let set_memlimit memlimit a = a.proof_memlimit <- memlimit

let set_obsolete ?(notify=notify) a =
  a.proof_obsolete <- true;
  notify (Proof_attempt a);
  check_goal_proved notify a.proof_parent

let set_archived a b = a.proof_archived <- b

let get_edited_as_abs session pr =
  option_map (Filename.concat session.session_dir) pr.proof_edited_as

(* [raw_add_goal parent name expl sum t] adds a goal to the given parent
   DOES NOT record the new goal in its parent, thus this should not be exported
*)
let raw_add_no_task ~(keygen:'a keygen) parent name expl sum shape exp =
  let parent_key = match parent with
    | Parent_theory mth -> mth.theory_key
    | Parent_transf mtr -> mtr.transf_key
  in
  let key = keygen ~parent:parent_key () in
  let goal = { goal_name = name;
               goal_expl = expl;
               goal_parent = parent;
               goal_task = None ;
               goal_checksum = sum;
               goal_shape = shape;
               goal_key = key;
               goal_external_proofs = PHprover.create 7;
               goal_transformations = PHstr.create 3;
               goal_verified = false;
               goal_expanded = exp;
             }
  in
  goal

let raw_add_task ~version ~(keygen:'a keygen) parent name expl t exp =
  let parent_key = match parent with
    | Parent_theory mth -> mth.theory_key
    | Parent_transf mtr -> mtr.transf_key
  in
  let key = keygen ~parent:parent_key () in
  let sum = Termcode.task_checksum ~version t in
  let shape = Termcode.t_shape_buf ~version
    (Task.task_goal_fmla t) in
  let goal = { goal_name = name;
               goal_expl = expl;
               goal_parent = parent;
               goal_task = Some t ;
               goal_checksum = sum;
               goal_shape = shape;
               goal_key = key;
               goal_external_proofs = PHprover.create 7;
               goal_transformations = PHstr.create 3;
               goal_verified = false;
               goal_expanded = exp;
             }
  in
  goal


(* [raw_add_transformation g name adds a transformation to the given goal g
   Adds no subgoals, thus this should not be exported
*)
let raw_add_transformation ~(keygen:'a keygen) g name exp =
  let parent = g.goal_key in
  let key = keygen ~parent () in
  let tr = { transf_name = name;
             transf_parent = g;
             transf_verified = false;
             transf_key = key;
             transf_goals = [];
             transf_expanded = exp;
           }
  in
  PHstr.replace g.goal_transformations name tr;
  tr

let raw_add_theory ~(keygen:'a keygen) mfile thname exp =
  let parent = mfile.file_key in
  let key = keygen ~parent () in
  let mth = { theory_name = thname;
              theory_key = key;
              theory_parent = mfile;
              theory_goals = [];
              theory_verified = false;
              theory_expanded = exp;
            }
  in
  mth

let raw_add_file ~(keygen:'a keygen) session f fmt exp =
  let key = keygen () in
  let mfile = { file_name = f;
                file_key = key;
                file_format = fmt;
                file_theories = [];
                file_verified = false;
                file_expanded = exp;
                file_parent  = session;
              }
  in
  PHstr.replace session.session_files f mfile;
  mfile


(****************************)
(*     session opening      *)
(****************************)

exception LoadError of Xml.element * string
(** LoadError (xml,messg) *)

let bool_attribute field r def =
  try
    match List.assoc field r.Xml.attributes with
      | "true" -> true
      | "false" -> false
      | _ -> assert false
  with Not_found -> def

let int_attribute field r def =
  try
    int_of_string (List.assoc field r.Xml.attributes)
  with Not_found | Invalid_argument _ -> def

let string_attribute_def field r def=
  try
    List.assoc field r.Xml.attributes
  with Not_found -> def

let string_attribute field r =
  try
    List.assoc field r.Xml.attributes
  with Not_found ->
    eprintf "[Error] missing required attribute '%s' from element '%s'@."
      field r.Xml.name;
    assert false

let keygen ?parent:_ () = ()

let load_result r =
  match r.Xml.name with
    | "result" ->
        let status = string_attribute "status" r in
        let answer =
          match status with
            | "valid" -> Call_provers.Valid
            | "invalid" -> Call_provers.Invalid
            | "unknown" -> Call_provers.Unknown ""
            | "timeout" -> Call_provers.Timeout
            | "outofmemory" -> Call_provers.OutOfMemory
            | "failure" -> Call_provers.Failure ""
            | "highfailure" -> Call_provers.Failure ""
            | s ->
                eprintf
                  "[Warning] Session.load_result: unexpected status '%s'@." s;
                Call_provers.Failure ""
        in
        let time =
          try float_of_string (List.assoc "time" r.Xml.attributes)
          with Not_found -> 0.0
        in
        Done {
          Call_provers.pr_answer = answer;
          Call_provers.pr_time = time;
          Call_provers.pr_output = "";
          Call_provers.pr_status = Unix.WEXITED 0
        }
    | "undone" -> Undone Interrupted
    | "unedited" -> Undone Unedited
    | s ->
        eprintf "[Warning] Session.load_result: unexpected element '%s'@." s;
        Undone Interrupted

let load_option attr g =
  try Some (List.assoc attr g.Xml.attributes)
  with Not_found -> None

let load_ident elt =
  let name = string_attribute "name" elt in
  let label = List.fold_left
    (fun acc label ->
      match label with
        | {Xml.name = "label"} ->
            let lab = string_attribute "name" label in
            Ident.Slab.add (Ident.create_label lab) acc
        | _ -> acc
    ) Ident.Slab.empty elt.Xml.elements in
  let preid =
    try
      let load_exn attr g = List.assoc attr g.Xml.attributes in
      let file = load_exn "locfile" elt in
      let lnum =  int_of_string (load_exn "loclnum" elt) in
      let cnumb = int_of_string (load_exn "loccnumb" elt) in
      let cnume = int_of_string (load_exn "loccnume" elt) in
      let pos = Loc.user_position file lnum cnumb cnume in
      Ident.id_user ~label name pos
    with Not_found | Invalid_argument _ ->
      Ident.id_fresh ~label name in
  Ident.id_register preid

let rec load_goal ~old_provers parent acc g =
  match g.Xml.name with
    | "goal" ->
        let gname = load_ident g in
        let expl = load_option "expl" g in
        let sum = Tc.checksum_of_string (string_attribute_def "sum" g "") in
        let shape = Tc.shape_of_string (string_attribute_def "shape" g "") in
        let exp = bool_attribute "expanded" g true in
        let mg = raw_add_no_task ~keygen parent gname expl sum shape exp in
        List.iter (load_proof_or_transf ~old_provers mg) g.Xml.elements;
        mg.goal_verified <- goal_verified mg;
        mg::acc
    | "label" -> acc
    | s ->
        eprintf "[Warning] Session.load_goal: unexpected element '%s'@." s;
        acc

and load_proof_or_transf ~old_provers mg a =
  match a.Xml.name with
    | "proof" ->
        let prover = string_attribute "prover" a in
        let p =
          try
            let p = Util.Mstr.find prover old_provers in
            p
          with Not_found ->
            eprintf "[Error] prover not listing in header '%s'@." prover;
            raise (LoadError (a,"prover not listing in header"))
        in
        let res = match a.Xml.elements with
          | [r] -> load_result r
          | [] -> Undone Interrupted
          | _ ->
            eprintf "[Error] Too many result elements@.";
            raise (LoadError (a,"too many result elements"))

        in
        let edit = load_option "edited" a in
        let edit = match edit with None | Some "" -> None | _ -> edit in
        let obsolete = bool_attribute "obsolete" a true in
        let archived = bool_attribute "archived" a false in
        let timelimit = int_attribute "timelimit" a 2 in
        let memlimit = int_attribute "memlimit" a 0 in
(*
        if timelimit < 0 then begin
            eprintf "[Error] incorrect or unspecified  timelimit '%i'@."
              timelimit;
            raise (LoadError (a,sprintf "incorrect or unspecified timelimit %i"
              timelimit))
        end;
*)
        let (_ : 'a proof_attempt) =
          add_external_proof ~keygen ~archived ~obsolete
            ~timelimit ~memlimit ~edit mg p res
        in
        ()
    | "transf" ->
        let trname = string_attribute "name" a in
        let exp = bool_attribute "expanded" a true in
        let mtr = raw_add_transformation ~keygen mg trname exp in
        mtr.transf_goals <-
          List.rev
          (List.fold_left
             (load_goal ~old_provers (Parent_transf mtr))
             [] a.Xml.elements);
        (* already done by raw_add_transformation
           Hashtbl.add mg.transformations trname mtr *)
        mtr.transf_verified <- transf_verified mtr
    | "label" -> ()
    | s ->
        eprintf
          "[Warning] Session.load_proof_or_transf: unexpected element '%s'@."
          s

let load_theory ~old_provers mf acc th =
  match th.Xml.name with
    | "theory" ->
        let thname = load_ident th in
        let exp = bool_attribute "expanded" th true in
        let mth = raw_add_theory ~keygen mf thname exp in
        mth.theory_goals <-
          List.rev
          (List.fold_left
             (load_goal ~old_provers (Parent_theory mth))
             [] th.Xml.elements);
        mth.theory_verified <- theory_verified mth;
        mth::acc
    | s ->
        eprintf "[Warning] Session.load_theory: unexpected element '%s'@." s;
        acc

let load_file session old_provers f =
  match f.Xml.name with
    | "file" ->
        let fn = string_attribute "name" f in
        let fmt = load_option "format" f in
        let exp = bool_attribute "expanded" f true in
        let mf = raw_add_file ~keygen session fn fmt exp in
        mf.file_theories <-
          List.rev
          (List.fold_left
             (load_theory ~old_provers mf) [] f.Xml.elements);
        mf.file_verified <- file_verified mf;
        old_provers
    | "prover" ->
      (** The id is just for the session file *)
        let id = string_attribute "id" f in
        let name = string_attribute "name" f in
        let version = string_attribute "version" f in
        let altern = string_attribute_def "alternative" f "" in
        let p = {C.prover_name = name;
                   prover_version = version;
                   prover_altern = altern} in
        Util.Mstr.add id p old_provers
    | s ->
        eprintf "[Warning] Session.load_file: unexpected element '%s'@." s;
        old_provers

let old_provers = ref Util.Mstr.empty
let get_old_provers () = !old_provers

let load_session session xml =
  match xml.Xml.name with
    | "why3session" ->
      let shape_version = int_attribute "shape_version" xml 1 in
      session.session_shape_version <- shape_version;
      dprintf debug "[Info] load_session: shape version is %d@\n" shape_version;
      (** just to keep the old_provers somewhere *)
      old_provers :=
        List.fold_left (load_file session) Util.Mstr.empty xml.Xml.elements;
      dprintf debug "[Info] load_session: done@\n"
    | s ->
        eprintf "[Warning] Session.load_session: unexpected element '%s'@." s

exception OpenError of string
type notask = unit
let read_session dir =
  if not (Sys.file_exists dir && Sys.is_directory dir) then
    raise (OpenError (Pp.sprintf "%s is not an existing directory" dir));
  let xml_filename = Filename.concat dir db_filename in
  let session = empty_session dir in
  (** If the xml is present we read it, otherwise we consider it empty *)
  if Sys.file_exists xml_filename then begin
    try
      let xml = Xml.from_file xml_filename in
      try
        load_session session xml.Xml.content;
      with Sys_error msg ->
        failwith ("Open session: sys error " ^ msg)
    with
      | Sys_error _msg ->
      (* xml does not exist yet *)
        raise (OpenError "Can't open")
      | Xml.Parse_error s ->
        Format.eprintf "XML database corrupted, ignored (%s)@." s;
      (* failwith
         ("Open session: XML database corrupted (%s)@." ^ s) *)
        raise (OpenError "XML corrupted")
  end;
  session


(*******************************)
(* Session modification        *)
(* expansion, add childs, ...  *)
(*******************************)

let rec set_goal_expanded g b =
  g.goal_expanded <- b;
  if not b then
    PHstr.iter (fun _ tr -> set_transf_expanded tr b) g.goal_transformations

and set_transf_expanded tr b =
  tr.transf_expanded <- b;
  if not b then
    List.iter (fun g -> set_goal_expanded g b) tr.transf_goals

let set_theory_expanded t b =
  t.theory_expanded <- b;
  if not b then
    List.iter (fun th -> set_goal_expanded th b) t.theory_goals

let set_file_expanded f b =
  f.file_expanded <- b;
  if not b then
    List.iter (fun th -> set_theory_expanded th b) f.file_theories