session.ml

(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2017   --   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.                           *)
(*                                                                  *)
(********************************************************************)

open Stdlib
open Ty
open Ident
open Decl
open Term
open Theory
open Task

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

let debug = Debug.register_info_flag "session"
  ~desc:"Pring@ debugging@ messages@ about@ Why3@ session@ \
         creation,@ reading@ and@ writing."

(** {2 Type definitions} *)

module PHstr = Hstr

type proof_attempt_status =
    | Unedited (** editor not yet run for interactive proof *)
    | JustEdited (** edited but not run yet *)
    | Interrupted (** external proof has never completed *)
    | Scheduled (** external proof attempt is scheduled *)
    | Running (** external proof attempt is in progress *)
    | 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 hide = 'a option

type ident_path =
  { ip_library : string list;
    ip_theory : string;
    ip_qualid : string list;
  }

let print_ident_path fmt ip =
  Format.fprintf fmt "%a.%s.%a"
    (Pp.print_list Pp.dot Pp.string) ip.ip_library
    ip.ip_theory
    (Pp.print_list Pp.dot Pp.string) ip.ip_qualid

(* dead code

let compare_ident_path x y =
  let c = Lists.compare String.compare x.ip_library y.ip_library in
  if c <> 0 then -c else (* in order to be bottom up *)
  let c = String.compare x.ip_theory y.ip_theory in
  if c <> 0 then c else
  let c = Lists.compare String.compare x.ip_qualid y.ip_qualid in
  c

module Pos = struct
  type t = ident_path
  let compare = compare_ident_path
  let equal x y = (x : t) = y
  let hash x = Hashtbl.hash (x : t)
end

module Mpos = Extmap.Make(Pos)
module Spos = Extset.MakeOfMap(Mpos)
module Hpos = Exthtbl.Make(Pos)

*)

type meta_args = meta_arg list

module Mmeta_args = Extmap.Make(struct
  type t = meta_args

  let meta_arg_id = function
    | MAty _  -> 0
    | MAts _  -> 1
    | MAls _  -> 2
    | MApr _  -> 3
    | MAstr _ -> 4
    | MAint _ -> 5

  let compare_meta_arg x y =
    match x,y with
    (* These hash are in fact tag *)
    | MAty  x, MAty  y -> compare (ty_hash x) (ty_hash y)
    | MAts  x, MAts  y -> compare (ts_hash x) (ts_hash y)
    | MAls  x, MAls  y -> compare (ls_hash x) (ls_hash y)
    | MApr  x, MApr  y -> compare (pr_hash x) (pr_hash y)
    | MAstr x, MAstr y -> String.compare x y
    | MAint x, MAint y -> compare x y
    | _ -> compare (meta_arg_id x) (meta_arg_id y)

  let compare = Lists.compare compare_meta_arg
end)

module Smeta_args = Extset.MakeOfMap(Mmeta_args)

type metas_args = Smeta_args.t Mstr.t

module Mmetas_args = Extmap.Make(struct
  type t = metas_args
  let compare = Mstr.compare Smeta_args.compare
end)

type idpos = {
  idpos_ts : ident_path Mts.t;
  idpos_ls : ident_path Mls.t;
  idpos_pr : ident_path Mpr.t;
}

let empty_idpos =
  {
    idpos_ts = Mts.empty;
    idpos_ls = Mls.empty;
    idpos_pr = Mpr.empty;
  }

(* dead code
let posid_of_idpos idpos =
  let posid = Mpos.empty in
  let posid = Mts.fold (fun ts pos ->
    Mpos.add pos (MAts ts)) idpos.idpos_ts posid  in
  let posid = Mls.fold (fun ls pos ->
    Mpos.add pos (MAls ls)) idpos.idpos_ls posid  in
  let posid = Mpr.fold (fun pr pos ->
    Mpos.add pos (MApr pr)) idpos.idpos_pr posid  in
  posid
*)

type 'a goal =
  { mutable goal_key  : 'a;
    goal_name : Ident.ident;
    mutable goal_expl : string option;
    goal_parent : 'a goal_parent;
    mutable goal_checksum : Tc.checksum option;
    mutable goal_shape : Tc.shape;
    mutable goal_verified : float option;
    mutable goal_task: task_option;
    mutable goal_expanded : bool;
    goal_external_proofs : 'a proof_attempt PHprover.t;
    goal_transformations : 'a transf PHstr.t;
    mutable goal_metas : 'a metas Mmetas_args.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_limit : Call_provers.resource_limit;
    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
  | Parent_metas  of 'a metas

and 'a metas =
  { mutable metas_key : 'a;
    metas_added : metas_args;
    metas_idpos : idpos;
    metas_parent : 'a goal;
    mutable metas_verified : float option;
    mutable metas_goal : 'a goal;
    (** Not mutated after the creation *)
    mutable metas_expanded : bool;
  }

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

and 'a detached =
    { detached_goals: 'a goal list; }

and 'a theory =
    { mutable theory_key : 'a;
      theory_name : Ident.ident;
      theory_parent : 'a file;
      mutable theory_checksum : Termcode.checksum option;
      mutable theory_goals : 'a goal list;
      mutable theory_verified : float option;
      mutable theory_expanded : bool;
      mutable theory_task : Theory.theory hide;
      mutable theory_detached : 'a detached option;
    }

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 : float option;
      mutable file_expanded : bool;
      mutable file_for_recovery : Theory.theory Mstr.t hide;
    }

and 'a session =
    { session_files : 'a file PHstr.t;
      mutable session_shape_version : int;
      session_prover_ids : int PHprover.t;
      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;
      mutable files : Theory.theory Stdlib.Mstr.t Stdlib.Mstr.t;
      session : 'a session}

let goal_key g = g.goal_key
let goal_name g = g.goal_name
let goal_verified g = g.goal_verified
let goal_external_proofs g = g.goal_external_proofs
let goal_transformations g = g.goal_transformations
let goal_metas g = g.goal_metas
let goal_expanded g = g.goal_expanded

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
  | Metas of 'a metas

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;
  Mmetas_args.iter (fun _ t -> metas_iter_proof_attempt f t) g.goal_metas;

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

and metas_iter_proof_attempt f t =
  goal_iter_proof_attempt f t.metas_goal

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

let metas_iter_proof_attempt f m =
  goal_iter_proof_attempt f m.metas_goal

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 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
    | Metas m -> metas_iter_proof_attempt f m

let rec goal_iter_leaf_goal ~unproved_only f g =
  if not (Opt.inhabited 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

let rec fold_all_sub_goals_of_goal f acc g =
  let acc =
    PHstr.fold
      (fun _ tr acc ->
       List.fold_left (fold_all_sub_goals_of_goal f) acc tr.transf_goals)
      g.goal_transformations acc
  in
  let acc =
    Mmetas_args.fold
      (fun _ m acc ->
       fold_all_sub_goals_of_goal f acc m.metas_goal)
      g.goal_metas acc
  in
  f acc g

let fold_all_sub_goals_of_theory f acc th =
  List.fold_left (fold_all_sub_goals_of_goal f) acc th.theory_goals


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

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

let iter_metas f t = f t.metas_goal

let iter_theory f t =
  List.iter f t.theory_goals

let iter_file f fi = List.iter f fi.file_theories

let iter_session f s = PHstr.iter (fun _ th -> f th) s.session_files

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;
  Mmetas_args.iter (fun _ t -> f (Metas t)) g.goal_metas


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

let metas_iter f t =
  f (Goal t.metas_goal)

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
    | Metas m -> metas_iter f m

(** 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 Opt.inhabited f.file_verified
          then f.file_name
          else f.file_name^"?"
        | Theory th ->
          if Opt.inhabited th.theory_verified
          then th.theory_name.Ident.id_string
          else th.theory_name.Ident.id_string^"?"
        | Goal g ->
          if Opt.inhabited 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 Opt.inhabited tr.transf_verified
          then tr.transf_name
          else tr.transf_name^"?"
        | Metas metas ->
          if Opt.inhabited metas.metas_verified
          then "metas..."
          else "metas..."^"?"
      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;
      (* Previously "" was `Filename.basename s.session_dir` but
         the tree depend on the filename given in input and not the content
         which is not easy for diffing
      *)
      "",!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_prover_ids = PHprover.create 7;
    session_dir   = dir;
  }

let create_session ?shape_version project_dir =
  if not (Sys.file_exists project_dir) then
    begin
      Debug.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


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

(* dead code
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
    | Parent_metas  metas -> get_session_metas metas


and get_session_trans transf = get_session_goal transf.transf_parent

and get_session_metas metas = get_session_goal metas.metas_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

let get_used_provers_with_stats session =
  let prover_table = PHprover.create 5 in
  session_iter_proof_attempt
    (fun pa ->
      (* record mostly used pa.proof_timelimit pa.proof_memlimit *)
      let prover = pa.proof_prover in
      let timelimits,steplimits,memlimits =
        try PHprover.find prover_table prover
        with Not_found ->
          let x = (Hashtbl.create 5,Hashtbl.create 5,Hashtbl.create 5) in
          PHprover.add prover_table prover x;
          x
      in
      let lim_time = pa.proof_limit.Call_provers.limit_time in
      let lim_mem = pa.proof_limit.Call_provers.limit_mem in
      let lim_steps = pa.proof_limit.Call_provers.limit_steps in
      let tf = try Hashtbl.find timelimits lim_time with Not_found -> 0 in
      let sf = try Hashtbl.find steplimits lim_steps with Not_found -> 0 in
      let mf = try Hashtbl.find memlimits lim_mem with Not_found -> 0 in
      Hashtbl.replace timelimits lim_time (tf+1);
      Hashtbl.replace steplimits lim_steps (sf+1);
      Hashtbl.replace memlimits lim_mem (mf+1))
    session;
  prover_table

exception NoTask

let goal_task g = Opt.get_exn NoTask g.goal_task
let goal_task_option g = g.goal_task

let goal_expl_lazy g =
  match g.goal_expl with
  | Some s -> s
  | None ->
     match g.goal_task with
     | Some t ->
        let _name,expl,_task = Termcode.goal_expl_task ~root:false t in
        g.goal_expl <- Some expl; expl
     | None -> ""

let goal_expl_or_name g =
  let s = goal_expl_lazy g in
  if s <> "" then s else
    try let _,_,l = restore_path g.goal_name in
        String.concat "." l
    with Not_found -> g.goal_name.Ident.id_string

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

let db_filename = "why3session.xml"
let shape_filename = "why3shapes"
let compressed_shape_filename = "why3shapes.gz"
let session_dir_for_save = ref "."

let save_string = Pp.html_string

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

let save_result fmt r =
  let steps = if  r.Call_provers.pr_steps >= 0 then
                Some  r.Call_provers.pr_steps
              else
                None
  in
  fprintf fmt "<result@ status=\"%s\"@ time=\"%.2f\"%a/>"
    (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.StepLimitExceeded -> "steplimitexceeded"
       | Call_provers.Invalid -> "invalid")
    r.Call_provers.pr_time
    (opt pp_print_int "steps") steps

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


let save_bool_def name def fmt b =
  if b <> def then fprintf fmt "@ %s=\"%b\"" name b

let save_int_def name def fmt n =
  if n <> def then fprintf fmt "@ %s=\"%d\"" name n

let opt_string = opt save_string

let save_proof_attempt fmt ((id,tl,sl,ml),a) =
  fprintf fmt
    "@\n@[<h><proof@ prover=\"%i\"%a%a%a%a%a%a>"
    id
    (save_int_def "timelimit" tl) (a.proof_limit.Call_provers.limit_time)
    (save_int_def "steplimit" sl) (a.proof_limit.Call_provers.limit_steps)
    (save_int_def "memlimit" ml) (a.proof_limit.Call_provers.limit_mem)
    (opt_string "edited") a.proof_edited_as
    (save_bool_def "obsolete" false) a.proof_obsolete
    (save_bool_def "archived" false) a.proof_archived;
  save_status fmt a.proof_state;
  fprintf fmt "</proof>@]"

let save_ident fmt id =
  let n=
    try
      let (_,_,l) = Theory.restore_path id in
      String.concat "." l
    with Not_found -> id.Ident.id_string
  in
  fprintf fmt "name=\"%a\"" save_string n

module Compr = Compress.Compress_z

type save_ctxt = {
  prover_ids : int PHprover.t;
  provers : (int * int * int * int) Mprover.t;
  ch_shapes : Compr.out_channel;
}

let save_checksum fmt s =
  fprintf fmt "%s" (Tc.string_of_checksum s)

let rec save_goal ctxt fmt g =
  let shape = Tc.string_of_shape g.goal_shape in
  assert (shape <> "");
  fprintf fmt
    "@\n@[<v 0>@[<h><goal@ %a%a%a>@]"
    save_ident g.goal_name
    (opt_string "expl") g.goal_expl
    (save_bool_def "expanded" false) g.goal_expanded;
  let sum =
    match g.goal_checksum with
    | None -> assert false
    | Some s -> Tc.string_of_checksum s
  in
  Compr.output_string ctxt.ch_shapes sum;
  Compr.output_char ctxt.ch_shapes ' ';
  Compr.output_string ctxt.ch_shapes shape;
  Compr.output_char ctxt.ch_shapes '\n';
(*
  Ident.Slab.iter (save_label fmt) g.goal_name.Ident.id_label;
*)
  let l = PHprover.fold
    (fun _ a acc -> (Mprover.find a.proof_prover ctxt.provers, a) :: acc)
    g.goal_external_proofs [] in
  let l = List.sort (fun ((i1,_,_,_),_) ((i2,_,_,_),_) -> compare i1 i2) l in
  List.iter (save_proof_attempt fmt) l;
  let l = PHstr.fold (fun _ t acc -> t :: acc) g.goal_transformations [] in
  let l = List.sort (fun t1 t2 -> compare t1.transf_name t2.transf_name) l in
  List.iter (save_trans ctxt fmt) l;
  Mmetas_args.iter (save_metas ctxt fmt) g.goal_metas;
  fprintf fmt "@]@\n</goal>"

and save_trans ctxt fmt t =
  fprintf fmt "@\n@[<hov 1>@[<h><transf@ name=\"%a\"%a>@]"
    save_string t.transf_name
    (save_bool_def "expanded" false) t.transf_expanded;
  List.iter (save_goal ctxt fmt) t.transf_goals;
  fprintf fmt "@]@\n</transf>"

and save_metas ctxt fmt _ m =
  fprintf fmt "@\n@[<hov 1><metas%a>"
    (save_bool_def "expanded" false) m.metas_expanded;
  let save_pos fmt pos =
    fprintf fmt "ip_theory=\"%a\">" save_string pos.ip_theory;
    List.iter (fprintf fmt "@\n@[<hov 1><ip_library@ name=\"%a\"/>@]" save_string)
      pos.ip_library;
    List.iter (fprintf fmt "@\n@[<hov 1><ip_qualid@ name=\"%a\"/>@]" save_string)
      pos.ip_qualid;
  in
  let save_ts_pos fmt ts pos =
    fprintf fmt "@\n@[<hov 1><ts_pos@ name=\"%a\"@ arity=\"%i\"@ \
    id=\"%i\"@ %a@]@\n</ts_pos>"
      save_string ts.ts_name.id_string (List.length ts.ts_args)
      (ts_hash ts) save_pos pos in
  let save_ls_pos fmt ls pos =
    (* TODO: add the signature? *)
    fprintf fmt "@\n@[<hov 1><ls_pos@ name=\"%a\"@ id=\"%i\"@ %a@]@\n</ls_pos>"
      save_string ls.ls_name.id_string
      (ls_hash ls) save_pos pos
  in
  let save_pr_pos fmt pr pos =
    fprintf fmt "@\n@[<hov 1><pr_pos@ name=\"%a\"@ id=\"%i\"@ %a@]@\n</pr_pos>"
      save_string pr.pr_name.id_string
      (pr_hash pr) save_pos pos
  in
  Mts.iter (save_ts_pos fmt) m.metas_idpos.idpos_ts;
  Mls.iter (save_ls_pos fmt) m.metas_idpos.idpos_ls;
  Mpr.iter (save_pr_pos fmt) m.metas_idpos.idpos_pr;
  Mstr.iter (fun s smeta_args ->
    Smeta_args.iter (save_meta_args fmt s) smeta_args) m.metas_added;
  save_goal ctxt fmt m.metas_goal;
  fprintf fmt "@]@\n</metas>"

and save_meta_args fmt s l =
  fprintf fmt "@\n@[<hov 1><meta@ name=\"%a\">" save_string s;
  let save_meta_arg fmt = function
    | MAty ty -> fprintf fmt "@\n@[<hov 1><meta_arg_ty/>";
      save_ty fmt ty;
      fprintf fmt "@]@\n</meta_arg_ty>"
    | MAts ts ->
      fprintf fmt "@\n@[<hov 1><meta_arg_ts@ id=\"%i\"/>@]" (ts_hash ts)
    | MAls ls ->
      fprintf fmt "@\n@[<hov 1><meta_arg_ls@ id=\"%i\"/>@]" (ls_hash ls)
    | MApr pr ->
      fprintf fmt "@\n@[<hov 1><meta_arg_pr@ id=\"%i\"/>@]" (pr_hash pr)
    | MAstr s ->
      fprintf fmt "@\n@[<hov 1><meta_arg_str@ val=\"%s\"/>@]" s
    | MAint i ->
      fprintf fmt "@\n@[<hov 1><meta_arg_int@ val=\"%i\"/>@]" i
  in
  List.iter (save_meta_arg fmt) l;
  fprintf fmt "@]@\n</meta>"

and save_ty fmt ty =
  match ty.ty_node with
  | Tyvar tv ->
    fprintf fmt "@\n@[<hov 1><ty_var@ id=\"%i\"/>@]" (tv_hash tv)
  | Tyapp (ts,l) ->
    fprintf fmt "@\n@[<hov 1><ty_app@ id=\"%i\"/>" (ts_hash ts);
    List.iter (save_ty fmt) l;
    fprintf fmt "@]@\n</ty_app>"

module CombinedTheoryChecksum = struct

 let b = Buffer.create 1024

 let f () g =
    match g.goal_checksum with
    | None -> assert false
    | Some c -> Buffer.add_string b (Tc.string_of_checksum c)

 let compute th =
   let () = fold_all_sub_goals_of_theory f () th in
   let c = Tc.buffer_checksum b in
   Buffer.clear b; c

end

let save_theory ctxt fmt t =
  let c = CombinedTheoryChecksum.compute t in
  t.theory_checksum <- Some c;
  fprintf fmt
    "@\n@[<v 1>@[<h><theory@ %a%a%a>@]"
    save_ident t.theory_name
    (opt save_checksum "sum") t.theory_checksum
    (save_bool_def "expanded" false) t.theory_expanded;
  List.iter (save_goal ctxt fmt) t.theory_goals;
  fprintf fmt "@]@\n</theory>"

let save_file ctxt fmt _ f =
  fprintf fmt
    "@\n@[<v 0>@[<h><file@ name=\"%a\"%a%a>@]"
    save_string f.file_name (opt_string "format")
    f.file_format (save_bool_def "expanded" false) f.file_expanded;
  List.iter (save_theory ctxt fmt) f.file_theories;
  fprintf fmt "@]@\n</file>"

let get_prover_to_save prover_ids p (timelimits,steplimits,memlimits) provers =
  let mostfrequent_timelimit,_ =
    Hashtbl.fold
      (fun t f ((_,f') as t') -> if f > f' then (t,f) else t')
      timelimits
      (0,0)
  in
  let mostfrequent_steplimit,_ =
    Hashtbl.fold
      (fun s f ((_,f') as s') -> if f > f' then (s,f) else s')
      steplimits
      (0,0)
  in
  let mostfrequent_memlimit,_ =
    Hashtbl.fold
      (fun m f ((_,f') as m') -> if f > f' then (m,f) else m')
      memlimits
      (0,0)
  in
  let id =
    try
      PHprover.find prover_ids p
    with Not_found ->
      (* we need to find an unused prover id *)
      let occurs = Hashtbl.create 7 in
      PHprover.iter (fun _ n -> Hashtbl.add occurs n ()) prover_ids;
      let id = ref 0 in
      try
        while true do
          try
            let _ = Hashtbl.find occurs !id in incr id
          with Not_found -> raise Exit
        done;
        assert false
      with Exit ->
        PHprover.add prover_ids p !id;
        !id
  in
  Mprover.add p (id,mostfrequent_timelimit,mostfrequent_steplimit,mostfrequent_memlimit) provers


let save_prover fmt id (p,mostfrequent_timelimit,mostfrequent_steplimit,mostfrequent_memlimit) =
  let steplimit =
    if mostfrequent_steplimit < 0 then None else Some mostfrequent_steplimit
  in
  fprintf fmt "@\n@[<h><prover@ id=\"%i\"@ name=\"%a\"@ \
               version=\"%a\"%a@ timelimit=\"%d\"%a@ memlimit=\"%d\"/>@]"
    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
    mostfrequent_timelimit
    (opt pp_print_int "steplimit") steplimit
    mostfrequent_memlimit

let save fname shfname _config session =
  let ch = open_out fname in
  let chsh = Compr.open_out shfname in
  let fmt = formatter_of_out_channel ch in
  fprintf fmt "<?xml version=\"1.0\" encoding=\"UTF-8\"?>@\n";
  fprintf fmt "<!DOCTYPE why3session PUBLIC \"-//Why3//proof session v5//EN\"@ \"http://why3.lri.fr/why3session.dtd\">@\n";
  (*
    let rel_file = Sysutil.relativize_filename !session_dir_for_save fname in
    fprintf fmt "@[<hov 1><why3session@ name=\"%a\" shape_version=\"%d\">"
    save_string rel_file session.session_shape_version;
  *)
  fprintf fmt "@[<v 0><why3session shape_version=\"%d\">"
    session.session_shape_version;
(*
  Tc.reset_dict ();
*)
  let prover_ids = session.session_prover_ids in
  let provers =
    PHprover.fold (get_prover_to_save prover_ids)
      (get_used_provers_with_stats session) Mprover.empty
  in
  let provers_to_save =
    Mprover.fold
      (fun p (id,mostfrequent_timelimit,mostfrequent_steplimit,mostfrequent_memlimit) acc ->
        Mint.add id (p,mostfrequent_timelimit,mostfrequent_steplimit,mostfrequent_memlimit) acc)
      provers Mint.empty
  in
  Mint.iter (save_prover fmt) provers_to_save;
  let ctxt = { prover_ids = prover_ids; provers = provers; ch_shapes = chsh } in
  PHstr.iter (save_file ctxt fmt) session.session_files;
  fprintf fmt "@]@\n</why3session>";
  fprintf fmt "@.";
  close_out ch;
  Compr.close_out chsh

let save_session config session =
  let f = Filename.concat session.session_dir db_filename in
  Sysutil.backup_file f;
  let fs = Filename.concat session.session_dir shape_filename in
  Sysutil.backup_file fs;
  let fz = Filename.concat session.session_dir compressed_shape_filename in
  Sysutil.backup_file fz;
  session_dir_for_save := session.session_dir;
  let fs = if Compress.compression_supported then fz else fs in
  save f fs config session

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

let compute_verified get l =
  List.fold_left (fun acc t ->
    match acc,get t with
    | Some x, Some y -> Some (x +. y)
    | _ -> None) (Some 0.0) l

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

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

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

let metas_verified m = m.metas_goal.goal_verified

let proof_verified a =
  if a.proof_obsolete then None else
    match a.proof_state with
      | Done { Call_provers.pr_answer = Call_provers.Valid;
               Call_provers.pr_time = t } -> Some t
      | _ -> None

let check_goal_verified g =
  let acc = ref None in
  let accumulate v =
    match v with
    | None -> ()
    | Some t ->
      match !acc with
      | Some x -> acc := Some (x +. t)
      | None -> acc := v
  in
  PHprover.iter
    (fun _ a -> accumulate (proof_verified a))
    g.goal_external_proofs;
  PHstr.iter
    (fun _ t -> accumulate t.transf_verified)
    g.goal_transformations;
  Mmetas_args.iter
      (fun _ t -> accumulate t.metas_verified)
    g.goal_metas;
  !acc

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 = check_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
      | Parent_metas t -> check_metas_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


and check_metas_proved notify m =
  let b = metas_verified m in
  if m.metas_verified <> b then begin
    m.metas_verified <- b;
    notify (Metas m);
    check_goal_proved notify m.metas_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 ~limit ~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_limit = limit;
            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