itp_server.ml 59.7 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)

12
open Format
13
open Wstdlib
14 15
open Session_itp
open Controller_itp
Sylvain Dailler's avatar
Sylvain Dailler committed
16
open Server_utils
17
open Itp_communication
18 19 20 21 22 23 24 25 26

(**********************************)
(* list unproven goal and related *)
(**********************************)

(* If the transformation is proved, return acc.
   Else, return the concatenation of the reversed list of unproven
   goals below the transformation and acc *)
let rec unproven_goals_below_tn cont acc tn =
27 28
  let s = cont.controller_session in
  if tn_proved s tn then
29 30
    acc                         (* we ignore "dead" goals *)
  else
31
    let sub_tasks = get_sub_tasks s tn in
32 33 34 35 36
    List.fold_left (unproven_goals_below_pn cont) acc sub_tasks

(* Same as unproven_goals_below_tn; note that if goal is not proved
   and there is no transformation, goal is returned (else it is not) *)
and unproven_goals_below_pn cont acc goal =
37 38
  let s = cont.controller_session in
  if pn_proved s goal then
39 40
    acc                         (* we ignore "dead" transformations *)
  else
41
    match get_transformations s goal with
42 43 44 45 46
    | [] -> goal :: acc
    | tns -> List.fold_left (unproven_goals_below_tn cont) acc tns

(* Same as unproven_goals_below_tn *)
let unproven_goals_below_th cont acc th =
47 48
  let s = cont.controller_session in
  if th_proved s th then
49 50 51 52 53 54 55
    acc
  else
    let goals = theory_goals th in
    List.fold_left (unproven_goals_below_pn cont) acc goals

(* Same as unproven_goals_below_tn *)
let unproven_goals_below_file cont file =
56 57
  let s = cont.controller_session in
  if file_proved s file then
58 59
    []
  else
60
    let theories = file_theories file in
61 62
    List.fold_left (unproven_goals_below_th cont) [] theories

63 64 65 66 67 68 69 70 71 72 73 74 75
let unproven_goals_below_id cont id =
  match id  with
  | APn pnid   -> [pnid]
  | APa panid  ->
     let ses = cont.controller_session in
     [get_proof_attempt_parent ses panid]
  | ATn tn     ->
     List.rev (unproven_goals_below_tn cont [] tn)
  | AFile file ->
     List.rev (unproven_goals_below_file cont file)
  | ATh th     ->
     List.rev (unproven_goals_below_th cont [] th)

76 77
(****** Exception handling *********)

78
let p s id =
79
  let _,tables = Session_itp.get_task_name_table s id in
80 81 82 83 84
  (* We use snapshots of printers to avoid registering new values inside it
     only for exception messages.
  *)
  let pr = Ident.duplicate_ident_printer tables.Trans.printer in
  let apr = Ident.duplicate_ident_printer tables.Trans.aprinter in
85 86
  (Pretty.create pr apr pr pr false)

87
let print_opt_type ~print_type fmt t =
Sylvain Dailler's avatar
Sylvain Dailler committed
88 89
  match t with
  | None -> Format.fprintf fmt "bool"
90
  | Some t -> print_type fmt t
91

92 93 94 95
(* Exception reporting *)

(* TODO remove references to id.id_string in this function *)
let bypass_pretty s id =
96
  let module P = (val (p s id)) in
97 98 99
  begin fun fmt exn -> match exn with
  | Ty.TypeMismatch (t1,t2) ->
      fprintf fmt "Type mismatch between %a and %a"
100
        P.print_ty t1 P.print_ty t2
101
  | Ty.BadTypeArity ({Ty.ts_args = []} as ts, _) ->
102
      fprintf fmt "Type symbol %a expects no arguments" P.print_ts ts
103 104 105
  | Ty.BadTypeArity (ts, app_arg) ->
      let i = List.length ts.Ty.ts_args in
      fprintf fmt "Type symbol %a expects %i argument%s but is applied to %i"
106
        P.print_ts ts i (if i = 1 then "" else "s") app_arg
107
  | Ty.DuplicateTypeVar tv ->
108
      fprintf fmt "Type variable %a is used twice" P.print_tv tv
109
  | Ty.UnboundTypeVar tv ->
110
      fprintf fmt "Unbound type variable: %a" P.print_tv tv
111 112 113 114
  | Ty.UnexpectedProp ->
      fprintf fmt "Unexpected propositional type"
  | Term.BadArity ({Term.ls_args = []} as ls, _) ->
      fprintf fmt "%s %a expects no arguments"
115
        (if ls.Term.ls_value = None then "Predicate" else "Function") P.print_ls ls
116 117 118 119
  | Term.BadArity (ls, app_arg) ->
      let i = List.length ls.Term.ls_args in
      fprintf fmt "%s %a expects %i argument%s but is applied to %i"
        (if ls.Term.ls_value = None then "Predicate" else "Function")
120
        P.print_ls ls i (if i = 1 then "" else "s") app_arg
121 122 123
  | Term.EmptyCase ->
      fprintf fmt "Empty match expression"
  | Term.DuplicateVar vs ->
124
      fprintf fmt "Variable %a is used twice" P.print_vsty vs
125
  | Term.UncoveredVar vs ->
126
      fprintf fmt "Variable %a uncovered in \"or\"-pattern" P.print_vsty vs
127
  | Term.FunctionSymbolExpected ls ->
128
      fprintf fmt "Not a function symbol: %a" P.print_ls ls
129
  | Term.PredicateSymbolExpected ls ->
130
      fprintf fmt "Not a predicate symbol: %a" P.print_ls ls
131 132
  | Term.ConstructorExpected ls ->
      fprintf fmt "%s %a is not a constructor"
133
        (if ls.Term.ls_value = None then "Predicate" else "Function") P.print_ls ls
134
  | Term.TermExpected t ->
135
      fprintf fmt "Not a term: %a" P.print_term t
136
  | Term.FmlaExpected t ->
137
      fprintf fmt "Not a formula: %a" P.print_term t
138 139
  | Pattern.ConstructorExpected (ls,ty) ->
      fprintf fmt "%s %a is not a constructor of type %a"
140 141
        (if ls.Term.ls_value = None then "Predicate" else "Function") P.print_ls ls
        P.print_ty ty
142 143
  | Pattern.NonExhaustive pl ->
      fprintf fmt "Pattern not covered by a match:@\n  @[%a@]"
144
        P.print_pat (List.hd pl)
145
  | Decl.BadConstructor ls ->
146
      fprintf fmt "Bad constructor: %a" P.print_ls ls
147
  | Decl.BadRecordField ls ->
148
      fprintf fmt "Not a record field: %a" P.print_ls ls
149
  | Decl.RecordFieldMissing ls ->
150
      fprintf fmt "Field %a is missing" P.print_ls ls
151
  | Decl.DuplicateRecordField ls ->
152
      fprintf fmt "Field %a is used twice in the same constructor" P.print_ls ls
153 154 155
  | Decl.IllegalTypeAlias ts ->
      fprintf fmt
        "Type symbol %a is a type alias and cannot be declared as algebraic"
156
        P.print_ts ts
157
  | Decl.NonFoundedTypeDecl ts ->
158
      fprintf fmt "Cannot construct a value of type %a" P.print_ts ts
159 160 161
  | Decl.NonPositiveTypeDecl (_ts, ls, ty) ->
      fprintf fmt "Constructor %a \
          contains a non strictly positive occurrence of type %a"
162
        P.print_ls ls P.print_ty ty
163 164
  | Decl.InvalidIndDecl (_ls, pr) ->
      fprintf fmt "Ill-formed inductive clause %a"
165
        P.print_pr pr
166 167 168
  | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
      fprintf fmt "Inductive clause %a contains \
          a non strictly positive occurrence of symbol %a"
169
        P.print_pr pr P.print_ls ls1
170 171
  | Decl.BadLogicDecl (ls1,ls2) ->
      fprintf fmt "Ill-formed definition: symbols %a and %a are different"
172
        P.print_ls ls1 P.print_ls ls2
173
  | Decl.UnboundVar vs ->
174
      fprintf fmt "Unbound variable:\n%a" P.print_vsty vs
175 176 177 178 179
  | Decl.ClashIdent id ->
      fprintf fmt "Ident %s is defined twice" id.Ident.id_string
  | Decl.EmptyDecl ->
      fprintf fmt "Empty declaration"
  | Decl.EmptyAlgDecl ts ->
180
      fprintf fmt "Algebraic type %a has no constructors" P.print_ts ts
181
  | Decl.EmptyIndDecl ls ->
182
      fprintf fmt "Inductive predicate %a has no constructors" P.print_ls ls
183 184 185 186 187 188 189 190
  | Decl.KnownIdent id ->
      fprintf fmt "Ident %s is already declared" id.Ident.id_string
  | Decl.UnknownIdent id ->
      fprintf fmt "Ident %s is not yet declared" id.Ident.id_string
  | Decl.RedeclaredIdent id ->
      fprintf fmt "Ident %s is already declared, with a different declaration"
        id.Ident.id_string
  | Decl.NoTerminationProof ls ->
191
      fprintf fmt "Cannot prove the termination of %a" P.print_ls ls
192 193 194
  | _ -> Format.fprintf fmt "Uncaught: %a" Exn_printer.exn_printer exn
  end

195
let get_exception_message ses id e =
196
  let module P = (val (p ses id)) in
197
  match e with
198
  | Session_itp.NoProgress ->
199
      Pp.sprintf "Transformation made no progress\n", Loc.dummy_position, ""
200 201
  | Generic_arg_trans_utils.Arg_trans s ->
      Pp.sprintf "Error in transformation function: %s \n" s, Loc.dummy_position, ""
202 203
  | Generic_arg_trans_utils.Arg_trans_decl (s, ld) ->
      Pp.sprintf "Error in transformation %s during inclusion of following declarations:\n%a" s
204
        (Pp.print_list (fun fmt () -> Format.fprintf fmt "\n") P.print_tdecl) ld,
205
      Loc.dummy_position, ""
206 207
  | Generic_arg_trans_utils.Arg_trans_term (s, t) ->
      Pp.sprintf "Error in transformation %s during with term:\n %a : %a " s
208
        P.print_term t (print_opt_type ~print_type:P.print_ty) t.Term.t_ty,
209 210
      Loc.dummy_position, ""
  | Generic_arg_trans_utils.Arg_trans_term2 (s, t1, t2) ->
Sylvain Dailler's avatar
Sylvain Dailler committed
211
      Pp.sprintf "Error in transformation %s during unification of following two terms:\n %a : %a \n %a : %a" s
212 213
        P.print_term t1 (print_opt_type ~print_type:P.print_ty) t1.Term.t_ty
        P.print_term t2 (print_opt_type ~print_type:P.print_ty) t2.Term.t_ty,
Sylvain Dailler's avatar
Sylvain Dailler committed
214
      Loc.dummy_position, ""
215 216 217 218 219 220
  | Generic_arg_trans_utils.Arg_trans_term3 (s, t1, t2, t3) ->
      Pp.sprintf "Error in transformation %s during unification of following two terms:\n %a : %a \n %a : %a\n\n%a is already matched with %a" s
        P.print_term t1 (print_opt_type ~print_type:P.print_ty) t1.Term.t_ty
        P.print_term t2 (print_opt_type ~print_type:P.print_ty) t2.Term.t_ty
        P.print_term t1 P.print_term t3,
      Loc.dummy_position, ""
221 222
  | Generic_arg_trans_utils.Arg_trans_pattern (s, pa1, pa2) ->
      Pp.sprintf "Error in transformation %s during unification of the following terms:\n %a \n %a"
223
        s P.print_pat pa1 P.print_pat pa2, Loc.dummy_position, ""
224
  | Generic_arg_trans_utils.Arg_trans_type (s, ty1, ty2) ->
Sylvain Dailler's avatar
Sylvain Dailler committed
225
      Pp.sprintf "Error in transformation %s during unification of the following types:\n %a \n %a"
226 227 228 229 230
        s P.print_ty ty1 P.print_ty ty2, Loc.dummy_position, ""
  | Generic_arg_trans_utils.Arg_trans_missing (s, svs) ->
      Pp.sprintf "Error in transformation function: %s %a\n" s
        (Pp.print_list Pp.space P.print_vs) (Term.Svs.elements svs),
      Loc.dummy_position, ""
231 232
  | Generic_arg_trans_utils.Arg_bad_hypothesis ("rewrite", _t) ->
      Pp.sprintf "Not a rewrite hypothesis", Loc.dummy_position, ""
233 234
  | Generic_arg_trans_utils.Cannot_infer_type s ->
      Pp.sprintf "Error in transformation %s. Cannot infer type of polymorphic element" s, Loc.dummy_position, ""
235 236
  | Args_wrapper.Arg_qid_not_found q ->
      Pp.sprintf "Following hypothesis was not found: %a \n" Typing.print_qualid q, Loc.dummy_position, ""
237
  | Args_wrapper.Arg_pr_not_found pr ->
238
      Pp.sprintf "Property not found: %a" P.print_pr pr, Loc.dummy_position, ""
239 240
  | Args_wrapper.Arg_error s ->
      Pp.sprintf "Transformation raised a general error: %s \n" s, Loc.dummy_position, ""
241
  | Args_wrapper.Arg_theory_not_found s ->
242
      Pp.sprintf "Theory not found: %s" s, Loc.dummy_position, ""
243
  | Args_wrapper.Arg_parse_type_error (loc, arg, e) ->
244
      Pp.sprintf "Parsing error: %a" Exn_printer.exn_printer e, loc, arg
Sylvain Dailler's avatar
Sylvain Dailler committed
245
  | Trans.Unnecessary_arguments l ->
Sylvain Dailler's avatar
Sylvain Dailler committed
246
      Pp.sprintf "First arguments were parsed and typed correctly but the last following are useless:\n%a"
247
        (Pp.print_list Pp.newline (fun fmt s -> Format.fprintf fmt "%s" s)) l, Loc.dummy_position, ""
248
  | Generic_arg_trans_utils.Unnecessary_terms l ->
Sylvain Dailler's avatar
Sylvain Dailler committed
249
      Pp.sprintf "First arguments were parsed and typed correctly but the last following are useless:\n%a"
250
        (Pp.print_list Pp.newline
251
           (fun fmt s -> Format.fprintf fmt "%a" P.print_term s)) l, Loc.dummy_position, ""
252
  | Args_wrapper.Arg_expected_none s ->
253
      Pp.sprintf "An argument was expected of type %s, none were given" s, Loc.dummy_position, ""
254
  | e ->
255
      (Pp.sprintf "%a" (bypass_pretty ses id) e), Loc.dummy_position, ""
256 257


Clément Fumex's avatar
Clément Fumex committed
258
module type Protocol = sig
Clément Fumex's avatar
Clément Fumex committed
259 260
  val get_requests : unit -> ide_request list
  val notify : notification -> unit
Clément Fumex's avatar
Clément Fumex committed
261 262
end

263
module Make (S:Controller_itp.Scheduler) (Pr:Protocol) = struct
264

265
module C = Controller_itp.Make(S)
Clément Fumex's avatar
Clément Fumex committed
266

267
let debug = Debug.register_flag "itp_server" ~desc:"ITP server"
Clément Fumex's avatar
Clément Fumex committed
268

269 270
let debug_attrs = Debug.register_info_flag "print_model_attrs"
  ~desc:"Print@ attrs@ of@ identifiers@ and@ expressions@ in prover@ results."
271 272 273 274 275

(****************)
(* Command list *)
(****************)

276
let interrupt_query _cont _args = C.interrupt (); "interrupted"
277

278
let commands_table = Hstr.create 17
279

280
let register_command c d f = Hstr.add commands_table c (d,f)
281 282 283 284 285 286 287 288 289 290

let () =
  List.iter (fun (c,d,f) -> register_command c d f)
    [
    "interrupt", "interrupt all scheduled or running proof tasks",
    Qnotask interrupt_query;
    "list-transforms", "list available transformations",
    Qnotask list_transforms_query;
    "list-provers", "list available provers",
    Qnotask list_provers;
291 292 293
(*
    "list-strategies", "list available strategies", list_strategies;
*)
294 295
    "print", "<id> print the declaration where <id> was defined",
    Qtask print_id;
296
    "search", "<ids> print the declarations where all <ids> appears",
Sylvain Dailler's avatar
Sylvain Dailler committed
297 298 299
    Qtask (search_id ~search_both:false);
    "search_all", "<ids> print the declarations where one of <ids> appears",
    Qtask (search_id ~search_both:true);
300 301 302 303 304 305 306 307 308 309 310 311
(*
    "r", "reload the session (test only)", test_reload;
    "s", "save the current session", test_save_session;
    "ng", "go to the next goal", then_print (move_to_goal_ret_p next_node);
    "pg", "go to the prev goal", then_print (move_to_goal_ret_p prev_node);
    "gu", "go to the goal up",  then_print (move_to_goal_ret_p zipper_up);
    "gd", "go to the goal down",  then_print (move_to_goal_ret_p zipper_down);
    "gr", "go to the goal right",  then_print (move_to_goal_ret_p zipper_right);
    "gl", "go to the goal left",  then_print (move_to_goal_ret_p zipper_left)
 *)
  ]

312
  type server_data =
313
    { (* task_driver : Driver.driver; *)
314
      cont : Controller_itp.controller;
315 316 317
      send_source: bool;
      (* If true the server is parametered to send source mlw files as
         notifications *)
318
      global_infos : Itp_communication.global_information;
319
    }
Clément Fumex's avatar
Clément Fumex committed
320

321
  let server_data = ref None
Clément Fumex's avatar
Clément Fumex committed
322

323
  let get_server_data () =
324 325
    match !server_data with
    | None ->
326
       Format.eprintf "get_server_data(): fatal error, server not yet initialized@.";
327 328
       exit 1
    | Some x -> x
Clément Fumex's avatar
Clément Fumex committed
329

330 331 332 333 334 335 336 337 338 339 340 341 342
(* fresh gives new fresh "names" for node_ID using a counter.
   reset resets the counter so that we can regenerate node_IDs as if session
   was fresh *)
  let reset, fresh =
    let count = ref 0 in
    (fun () ->
      count := 0),
    fun () ->
      count := !count + 1;
      !count

  let model_any : any Hint.t = Hint.create 17

343 344 345
  let any_from_node_ID (nid:node_ID) : any option =
    try Some (Hint.find model_any nid) with
    | Not_found -> None
346 347 348 349 350

  let pan_to_node_ID  : node_ID Hpan.t = Hpan.create 17
  let pn_to_node_ID   : node_ID Hpn.t = Hpn.create 17
  let tn_to_node_ID   : node_ID Htn.t = Htn.create 17
  let th_to_node_ID   : node_ID Ident.Hid.t = Ident.Hid.create 7
351
  let file_to_node_ID : node_ID Hfile.t = Hfile.create 3
352 353 354 355 356

  let node_ID_from_pan  pan  = Hpan.find pan_to_node_ID pan
  let node_ID_from_pn   pn   = Hpn.find pn_to_node_ID pn
  let node_ID_from_tn   tn   = Htn.find tn_to_node_ID tn
  let node_ID_from_th   th   = Ident.Hid.find th_to_node_ID (theory_name th)
357
  let node_ID_from_file file = Hfile.find file_to_node_ID (file_id file)
358 359 360 361 362 363 364 365 366 367 368 369

  let node_ID_from_any  any  =
    match any with
    | AFile file -> node_ID_from_file file
    | ATh th     -> node_ID_from_th th
    | ATn tn     -> node_ID_from_tn tn
    | APn pn     -> node_ID_from_pn pn
    | APa pan    -> node_ID_from_pan pan

  let remove_any_node_ID any =
    match any with
    | AFile file ->
370
        let nid = Hfile.find file_to_node_ID (file_id file) in
371
        Hint.remove model_any nid;
372
        Hfile.remove file_to_node_ID (file_id file)
373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391
    | ATh th     ->
        let nid = Ident.Hid.find th_to_node_ID (theory_name th) in
        Hint.remove model_any nid;
        Ident.Hid.remove th_to_node_ID (theory_name th)
    | ATn tn     ->
        let nid = Htn.find tn_to_node_ID tn in
        Hint.remove model_any nid;
        Htn.remove tn_to_node_ID tn
    | APn pn     ->
        let nid = Hpn.find pn_to_node_ID pn in
        Hint.remove model_any nid;
        Hpn.remove pn_to_node_ID pn
    | APa pa     ->
        let nid = Hpan.find pan_to_node_ID pa in
        Hint.remove model_any nid;
        Hpan.remove pan_to_node_ID pa

  let add_node_to_table node new_id =
    match node with
392
    | AFile file -> Hfile.add file_to_node_ID (file_id file) new_id
393 394 395 396 397 398
    | ATh th     -> Ident.Hid.add th_to_node_ID (theory_name th) new_id
    | ATn tn     -> Htn.add tn_to_node_ID tn new_id
    | APn pn     -> Hpn.add pn_to_node_ID pn new_id
    | APa pan    -> Hpan.add pan_to_node_ID pan new_id


399 400 401 402 403 404 405 406
(*******************************)
(* Compute color for locations *)
(*******************************)

(* This section is used to get colored source as a function of the task *)

exception No_loc_on_goal

407 408 409 410 411 412 413 414 415
let get_locations (task: Task.task) =
  let list = ref [] in
  let file_cache = Hstr.create 17 in
  let session_dir =
    let d = get_server_data () in
    Session_itp.get_dir d.cont.controller_session in
  let relativize f =
    try Hstr.find file_cache f
    with Not_found ->
MARCHE Claude's avatar
MARCHE Claude committed
416 417
      let path = Sysutil.relativize_filename session_dir f in
      (* FIXME: this an abusive use of Sysutil.system_dependent_absolute_path *)
418
      let g = Sysutil.system_dependent_absolute_path session_dir path in
419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449
      Hstr.replace file_cache f g;
      g in
  let color_loc ~color ~loc =
    let (f,l,b,e) = Loc.get loc in
    let loc = Loc.user_position (relativize f) l b e in
    list := (loc, color) :: !list in
  let rec color_locs ~color formula =
    Opt.iter (fun loc -> color_loc ~color ~loc) formula.Term.t_loc;
    Term.t_iter (fun subf -> color_locs ~color subf) formula in
  let rec color_t_locs ~premise f =
    match f.Term.t_node with
    | Term.Tbinop (Term.Timplies,f1,f2) when not premise ->
      color_t_locs ~premise:true f1;
      color_t_locs ~premise:false f2
    | Term.Tbinop (Term.Tand,f1,f2) when premise ->
      color_t_locs ~premise f1;
      color_t_locs ~premise f2
    | Term.Tlet (_,fb) ->
      let _,f1 = Term.t_open_bound fb in
      color_t_locs ~premise f1
    | Term.Tquant (Term.Tforall,fq) when not premise ->
      let _,_,f1 = Term.t_open_quant fq in
      color_t_locs ~premise f1
    | Term.Tnot f1 when premise && f.Term.t_loc = None ->
      color_locs ~color:Neg_premise_color f1
    | _ when premise ->
      color_locs ~color:Premise_color f
    | _ ->
      color_locs ~color:Goal_color f in
  let color_goal = function
    | None ->
450 451 452 453 454
      (* This case can happen when after some transformations: for example, in
         an assert, the new goal asserted is not tagged with locations *)
      (* This error is harmless but we want to detect it when debugging. *)
      if Debug.test_flag Debug.stack_trace then
        raise No_loc_on_goal
455
    | Some loc -> color_loc ~color:Goal_color ~loc in
456
  let goal_id : Ident.ident = (Task.task_goal task).Decl.pr_name in
457
  color_goal goal_id.Ident.id_loc;
458
  let rec scan = function
459
    | Some
460 461
        { Task.task_prev = prev;
          Task.task_decl =
462
            { Theory.td_node =
463 464
                Theory.Decl { Decl.d_node = Decl.Dprop (k, _, f) }}} ->
      begin match k with
465 466
      | Decl.Pgoal  -> color_t_locs ~premise:false f
      | Decl.Paxiom -> color_t_locs ~premise:true  f
467 468 469 470 471
      | _ -> assert false
      end;
      scan prev
    | Some { Task.task_prev = prev } -> scan prev
    | _ -> () in
472 473
  scan task;
  !list
474

475 476
let get_modified_node n =
  match n with
477
  | Reset_whole_tree -> None
478 479 480 481 482
  | New_node (nid, _, _, _, _) -> Some nid
  | Node_change  (nid, _) -> Some nid
  | Remove nid -> Some nid
  | Next_Unproven_Node_Id (_, nid) -> Some nid
  | Initialized _ -> None
483
  | Saved | Saving_needed _ -> None
484 485 486 487
  | Message _ -> None
  | Dead _ -> None
  | Task (nid, _, _) -> Some nid
  | File_contents _ -> None
488
  | Source_and_ce _ -> None
489

490

491 492
type focus =
  | Unfocused
493 494
(* We can focus on several nodes at once *)
  | Focus_on of Session_itp.any list
495 496
  | Wait_focus

497
(* Focus on a node *)
498 499 500
let focused_node = ref Unfocused
let get_focused_label = ref None

501 502
let focus_on_loading (f: Task.task -> bool) =
  focused_node := Wait_focus;
503
  get_focused_label := Some f
504 505 506 507 508 509

(* TODO *)
module P = struct

  let get_requests = Pr.get_requests

510 511
  (* true if nid is below f_node or does not exists (in which case the
     notification is a remove). false if not below.  *)
512
  let is_below s nid f_nodes =
513
    let any = any_from_node_ID nid in
514 515
    match any with
    | None -> true
516 517
    | Some any ->
        List.exists (Session_itp.is_below s any) f_nodes
518

519 520 521
  let notify n =
    let d = get_server_data() in
    let s = d.cont.controller_session in
522 523 524 525 526 527 528 529 530 531 532 533 534 535 536
    match n with
    | Initialized _ | Saved | Message _ | Dead _ -> Pr.notify n
    | _ ->
      begin
        match !focused_node with
        | Wait_focus -> () (* Do not notify at all *)
        | Unfocused -> Pr.notify n
        | Focus_on f_nodes ->
            let updated_node = get_modified_node n in
            match updated_node with
            | None -> Pr.notify n
            | Some nid when is_below s nid f_nodes ->
                Pr.notify n
            | _ -> ()
      end
537 538 539

end

540 541 542 543 544 545 546
  (*********************)
  (* File input/output *)
  (*********************)

  let read_and_send f =
    try
      let d = get_server_data() in
547
      if d.send_source then
548 549
(*
        let fn = Sysutil.absolutize_path
550
            (Session_itp.get_dir d.cont.controller_session) f in
551 552
 *)
        let s = Sysutil.file_contents f in
553
        P.notify (File_contents (f, s))
554 555 556 557 558
    with Invalid_argument s ->
      P.notify (Message (Error s))

  let save_file f file_content =
    try
559
(*
560 561
      let d = get_server_data() in
      let fn = Sysutil.absolutize_filename
562
                 (Session_itp.get_dir d.cont.controller_session) f in
563 564 565
 *)
      Sysutil.backup_file f;
      Sysutil.write_file f file_content;
566 567 568 569
      P.notify (Message (File_Saved f))
    with Invalid_argument s ->
      P.notify (Message (Error s))

570 571
  let relativize_location s loc =
    let f, l, b, e = Loc.get loc in
MARCHE Claude's avatar
MARCHE Claude committed
572 573 574
    let path = Sysutil.relativize_filename (Session_itp.get_dir s) f in
    (* FIXME: this an abusive use of Sysutil.system_dependent_absolute_path *)
    let f = Sysutil.system_dependent_absolute_path "" path in
575 576
    Loc.user_position f l b e

577
  let capture_parse_or_type_errors f cont =
578 579 580 581
    List.map
      (function
        | Loc.Located (loc, e) ->
           let rel_loc = relativize_location cont.controller_session loc in
582 583
           let s = Format.asprintf "%a: %a" Loc.gen_report_position rel_loc
                                   Exn_printer.exn_printer e in
584 585 586 587 588 589
           (loc, rel_loc, s)
        | e when not (Debug.test_flag Debug.stack_trace) ->
           let s = Format.asprintf "%a" Exn_printer.exn_printer e in
           (Loc.dummy_position, Loc.dummy_position, s)
        | e -> raise e)
      (f cont)
590 591 592

  (* Reload_files that is used even if the controller is not correct. It can
     be incorrect and end up in a correct state. *)
593
  let reload_files cont ~shape_version =
594
    capture_parse_or_type_errors
595
      (fun c ->
596
        try let (_,_) = reload_files ~shape_version c in [] with
597
        | Errors_list le -> le) cont
598

599
  let add_file cont ?format fname =
600 601
    capture_parse_or_type_errors
      (fun c ->
602 603
        try add_file c ?format fname; [] with
        | Errors_list le -> le) cont
604

605

606
  (* -----------------------------------   ------------------------------------- *)
Clément Fumex's avatar
Clément Fumex committed
607

608 609 610
  let get_node_type (node: any) =
    match node with
    | AFile _ -> NFile
Sylvain Dailler's avatar
Sylvain Dailler committed
611 612 613 614
    | ATh _   -> NTheory
    | ATn _   -> NTransformation
    | APn _   -> NGoal
    | APa _   -> NProofAttempt
615 616

  let get_node_name (node: any) =
617
    let d = get_server_data () in
618
    match node with
619
    | AFile file -> Session_itp.basename (file_path file)
620
    | ATh th -> (theory_name th).Ident.id_string
621
    | ATn tn ->
622 623 624 625 626 627
       let name = get_transf_name d.cont.controller_session tn in
       let args = get_transf_args d.cont.controller_session tn in
       let full = String.concat " " (name :: args) in
       if String.length full >= 40 then
         String.sub full 0 40 ^ " ..."
       else full
628
    | APn pn ->
629
       let name = (get_proof_name d.cont.controller_session pn).Ident.id_string in
630 631 632 633
       (* Reduce the name of the goal to the minimum, by taking the
          part after the last dot: "0" instead of "WP_Parameter.0" for
          example.  *)
       let name = List.hd (Strings.rev_split '.' name) in
634
       let expl = get_proof_expl d.cont.controller_session pn in
635
       if expl = "" then name else name ^ " [" ^ expl ^ "]"
636
    | APa pa ->
637
      let pa = get_proof_attempt_node d.cont.controller_session pa in
638 639
      Pp.string_of Whyconf.print_prover pa.prover

640 641 642 643
  let get_node_detached (node: any) =
    let d = get_server_data () in
    is_detached d.cont.controller_session node

644 645 646
  let get_node_proved new_id (node: any) =
    let d = get_server_data () in
    let cont = d.cont in
647
    let s = cont.controller_session in
648
    match node with
649
    | AFile file ->
650
      P.notify (Node_change (new_id, Proved (file_proved s file)))
651
    | ATh th ->
652
      P.notify (Node_change (new_id, Proved (th_proved s th)))
653
    | ATn tn ->
654
      P.notify (Node_change (new_id, Proved (tn_proved s tn)))
655
    | APn pn ->
656
      P.notify (Node_change (new_id, Proved (pn_proved s pn)))
657
    | APa pa ->
658
      let pa = get_proof_attempt_node s pa in
659 660 661
      let obs = pa.proof_obsolete in
      let limit = pa.limit in
      let res =
662
        match pa.Session_itp.proof_state with
663
        | Some pa -> Done pa
664
        | _ -> Undone
665 666 667
      in
      P.notify (Node_change (new_id, Proof_status_change(res, obs, limit)))

668

669
(*
670 671 672 673 674
  let get_info_and_type ses (node: any) =
    match node with
    | AFile file ->
        let name = file.file_name in
        let proved = file_proved cont file in
675
        NFile, {name; proved}
676 677 678
    | ATh th     ->
        let name = (theory_name th).Ident.id_string in
        let proved = th_proved cont th in
679
        NTheory, {name; proved}
680 681 682
    | ATn tn     ->
        let name = get_transf_name ses tn in
        let proved = tn_proved cont tn in
683
        NTransformation, {name; proved}
684 685 686
    | APn pn     ->
        let name = (get_proof_name ses pn).Ident.id_string in
        let proved = pn_proved cont pn in
687
          NGoal, {name; proved}
688 689 690
    | APa pan    ->
        let pa = get_proof_attempt_node ses pan in
        let name = Pp.string_of Whyconf.print_prover pa.prover in
Clément Fumex's avatar
Clément Fumex committed
691 692 693
        let pr, proved = match pa.Session_itp.proof_state with
        | Some pr -> Some pr.pr_answer, pr.pr_answer = Valid
        | None -> None, false
694
        in
Clément Fumex's avatar
Clément Fumex committed
695 696
        (NProofAttempt (pr, pa.proof_obsolete)),
        {name; proved}
697
*)
698

699 700 701 702 703
  let add_focused_node node =
    match !focused_node with
    | Focus_on l -> focused_node := Focus_on (node :: l)
    | _ -> focused_node := Focus_on [node]

704 705 706 707
  (* Focus on label: this is used to automatically focus on the first task
     having a given property (label_detection) in the session tree. To change
     the property, one need to call function register_label_detection. *)
  let focus_on_label node =
708 709 710 711 712 713 714
    let d = get_server_data () in
    let session = d.cont.Controller_itp.controller_session in
    if not (Session_itp.is_detached session node) then
      match !get_focused_label with
      | Some label_detection ->
          (match node with
          | APn pr_node ->
715
              let task = Session_itp.get_task session pr_node in
716 717 718 719 720
              let b = label_detection task in
              if b then
                add_focused_node node
          | _ -> ())
      | None -> ()
721

Sylvain Dailler's avatar
Sylvain Dailler committed
722
  (* Create a new node in the_tree, update the tables and send a
Clément Fumex's avatar
Clément Fumex committed
723
     notification about it *)
724
  let new_node ~parent node : node_ID =
725 726
    let new_id = fresh () in
      Hint.add model_any new_id node;
727 728
      let node_type = get_node_type node in
      let node_name = get_node_name node in
729
      let node_detached = get_node_detached node in
730
      add_node_to_table node new_id;
731 732
      (* Specific to auto-focus at initialization of itp_server *)
      focus_on_label node;
733 734 735 736 737 738 739 740
      begin
        (* Do not send theories that do not contain any goal *)
        match node with
        | ATh th when theory_goals th = [] -> ()
        | _ ->
            P.notify (New_node (new_id, parent, node_type, node_name, node_detached));
            get_node_proved new_id node
      end;
Clément Fumex's avatar
Clément Fumex committed
741 742
      new_id

743 744 745 746
  (* Same as new_node but do not return the node. *)
  let create_node ~parent node =
    let _: node_ID = new_node ~parent node in ()

Sylvain Dailler's avatar
Sylvain Dailler committed
747 748 749
  (****************************)
  (* Iter on the session tree *)
  (****************************)
750

751 752 753 754
  (* Iter on the session tree with a function [f parent current] with type
     node_ID -> any -> unit *)
  let iter_subtree_proof_attempt_from_goal
    (f: parent:node_ID -> any -> unit) parent id =
755
    let d = get_server_data () in
Clément Fumex's avatar
Clément Fumex committed
756
    Whyconf.Hprover.iter
757
      (fun _pa panid -> f ~parent (APa panid))
758
      (get_proof_attempt_ids d.cont.controller_session id)
Clément Fumex's avatar
Clément Fumex committed
759

760 761
  let rec iter_subtree_from_goal
    (f: parent:node_ID -> any -> unit) parent id =
762 763
    let d = get_server_data () in
    let ses = d.cont.controller_session in
764 765
    f ~parent (APn id);
    let nid = node_ID_from_pn id in
Clément Fumex's avatar
Clément Fumex committed
766
    List.iter
767
      (fun trans_id -> iter_subtree_from_trans f nid trans_id)
Clément Fumex's avatar
Clément Fumex committed
768
      (get_transformations ses id);
769
    iter_subtree_proof_attempt_from_goal f nid id
Clément Fumex's avatar
Clément Fumex committed
770

771 772
  and iter_subtree_from_trans
    (f: parent:node_ID -> any -> unit) parent trans_id =
773 774
    let d = get_server_data () in
    let ses = d.cont.controller_session in
775 776
    f ~parent (ATn trans_id);
    let nid = node_ID_from_tn trans_id in
Clément Fumex's avatar
Clément Fumex committed
777
    List.iter
778
      (fun goal_id -> (iter_subtree_from_goal f nid goal_id))
779
      (get_sub_tasks ses trans_id)
Clément Fumex's avatar
Clément Fumex committed
780

781 782 783 784 785 786 787
  let iter_subtree_from_theory
    (f: parent:node_ID -> any -> unit) parent theory_id =
    f ~parent (ATh theory_id);
    let nid = node_ID_from_th theory_id in
    List.iter (iter_subtree_from_goal f nid)
               (theory_goals theory_id)

788 789
  let iter_subtree_from_file (f: parent:node_ID -> any -> unit) file =
    f ~parent:root_node (AFile file);
790
    let nid = node_ID_from_file file in
791
    List.iter (iter_subtree_from_theory f nid) (file_theories file)
792

793 794
  let iter_on_files ~(on_file: file -> unit)
                    ~(on_subtree: parent:node_ID -> any -> unit) : unit =
795 796
    let d = get_server_data () in
    let ses = d.cont.controller_session in
Clément Fumex's avatar
Clément Fumex committed
797
    let files = get_files ses in
798
    Hfile.iter
Clément Fumex's avatar
Clément Fumex committed
799
      (fun _ file ->
800 801
       on_file file;
       iter_subtree_from_file on_subtree file)
802
      files
Clément Fumex's avatar
Clément Fumex committed
803

Sylvain Dailler's avatar
Sylvain Dailler committed
804 805 806 807
  (**********************************)
  (* Initialization of session tree *)
  (**********************************)

808

809
  let send_new_subtree_from_trans parent trans_id : unit =
Clément Fumex's avatar
Clément Fumex committed
810
    iter_subtree_from_trans
811
      create_node parent trans_id
812

813
  let send_new_subtree_from_file f =
814
    iter_subtree_from_file create_node f
Sylvain Dailler's avatar
Sylvain Dailler committed
815

816 817
  let reset_and_send_the_whole_tree (): unit =
    P.notify Reset_whole_tree;
818 819 820 821 822 823
    let d = get_server_data () in
    let ses = d.cont.controller_session in
    let on_file f =
      read_and_send (Session_itp.system_path ses f)
    in
    iter_on_files ~on_file ~on_subtree:create_node
824

825 826 827
  let unfocus () =
    focused_node := Unfocused;
    reset_and_send_the_whole_tree ()
828

Clément Fumex's avatar
Clément Fumex committed
829
  (* -- send the task -- *)
830 831
  let task_of_id d id show_full_context loc =
    let task,tables = get_task_name_table d.cont.controller_session id in
832
    (* This function also send source locations associated to the task *)
833
    let loc_color_list = if loc then get_locations task else [] in
834
    let task_text =
835 836 837
      let pr = tables.Trans.printer in
      let apr = tables.Trans.aprinter in
      let module P = (val Pretty.create pr apr pr pr false) in
838
      Pp.string_of (if show_full_context then P.print_task else P.print_sequent) task
839 840
    in
    task_text, loc_color_list
841

842
  let create_ce_tab ~print_attrs s res any list_loc =
843
    let f = get_encapsulating_file s any in
844
    let filename = Session_itp.system_path s f in
845
    let source_code = Sysutil.file_contents filename in
846
    Model_parser.interleave_with_source ~print_attrs ?start_comment:None ?end_comment:None
847
      ?me_name_trans:None res.Call_provers.pr_model ~rel_filename:filename
848
      ~source_code:source_code ~locations:list_loc
849

850
  let send_task nid show_full_context loc =
851
    let d = get_server_data () in
852
    let any = any_from_node_ID nid in
853 854 855 856
    match any with
    | None ->
      P.notify (Message (Error "Please select a node id"))
    | Some any ->
857 858 859 860 861 862 863 864 865 866 867 868 869
    if Session_itp.is_detached d.cont.controller_session any then
      match any with
      | APn _id ->
        let s = "Goal is detached and cannot be printed" in
        P.notify (Task (nid, s, []))
      | ATh t ->
          P.notify (Task (nid, "Detached theory " ^ (theory_name t).Ident.id_string, []))
      | APa pid ->
          let pa = get_proof_attempt_node  d.cont.controller_session pid in
          let name = Pp.string_of Whyconf.print_prover pa.prover in
          let prover_text = "Detached prover\n====================> Prover: " ^ name ^ "\n" in
          P.notify (Task (nid, prover_text, []))
      | AFile f ->
870
          P.notify (Task (nid, "Detached file " ^ (basename (file_path f)), []))
871 872 873 874 875 876 877 878 879 880 881 882 883
      | ATn tid ->
          let name = get_transf_name d.cont.controller_session tid in
          let args = get_transf_args d.cont.controller_session tid in
          P.notify (Task (nid, "Detached transformation\n====================> Transformation: " ^
                          String.concat " " (name :: args) ^ "\n", []))
    else
      match any with
      | APn id ->
          let s, list_loc = task_of_id d id show_full_context loc in
          P.notify (Task (nid, s, list_loc))
      | ATh t ->
          P.notify (Task (nid, "Theory " ^ (theory_name t).Ident.id_string, []))
      | APa pid ->
884
          let print_attrs = Debug.test_flag debug_attrs in
885 886 887
          let pa = get_proof_attempt_node  d.cont.controller_session pid in
          let parid = pa.parent in
          let name = Pp.string_of Whyconf.print_prover pa.prover in
888
          let s, old_list_loc = task_of_id d parid show_full_context loc in
889 890
          let prover_text = s ^ "\n====================> Prover: " ^ name ^ "\n" in
          (* Display the result of the prover *)
891
          begin
892 893 894 895 896 897 898
            match pa.proof_state with
            | Some res ->
                let result =
                  Pp.string_of Call_provers.print_prover_answer
                    res.Call_provers.pr_answer
                in
                let ce_result =
899
                  Pp.string_of (Model_parser.print_model_human ~print_attrs ?me_name_trans:None)
900
                  res.Call_provers.pr_model
901 902
                in
                if ce_result = "" then
903 904 905 906
                  let result_pr =
                    result ^ "\n\n" ^ "The prover did not return counterexamples."
                  in
                  P.notify (Task (nid, prover_text ^ result_pr, old_list_loc))
907
                else
908
                  begin
909 910 911 912
                    let result_pr =
                      result ^ "\n\n" ^ "Counterexample suggested by the prover:\n\n" ^ ce_result
                    in
                    let (source_result, list_loc) =
913
                      create_ce_tab d.cont.controller_session ~print_attrs res any old_list_loc
914 915 916
                    in
                    P.notify (Source_and_ce (source_result, list_loc));
                    P.notify (Task (nid, prover_text ^ result_pr, old_list_loc))
917
                  end
918 919
            | None -> P.notify (Task (nid, "Result of the prover not available.\n", old_list_loc))
          end
920
      | AFile f ->
921
          P.notify (Task (nid, "File " ^ (basename (file_path f)), []))
922 923 924 925 926 927 928
      | ATn tid ->
          let name = get_transf_name d.cont.controller_session tid in
          let args = get_transf_args d.cont.controller_session tid in
          let parid = get_trans_parent d.cont.controller_session tid in
          let s, list_loc = task_of_id d parid show_full_context loc in
          P.notify (Task (nid, s ^ "\n====================> Transformation: " ^
                          String.concat " " (name :: args) ^ "\n", list_loc))
929

Sylvain Dailler's avatar
Sylvain Dailler committed
930 931
  (* -------------------- *)

932 933 934
  (* True when session differs from the saved session *)
  let session_needs_saving = ref false

Sylvain Dailler's avatar
Sylvain Dailler committed
935 936 937 938
  (* Add a file into the session when (Add_file_req f) is sent *)
  (* Note that f is the path from execution directory to the file and fn is the
     path from the session directory to the file. *)
  let add_file_to_session cont f =
939 940
    let dir = get_dir cont.controller_session in
    let fn = Sysutil.relativize_filename dir f in
941
    try
942 943
      let (_ : file) = find_file_from_path cont.controller_session fn in
      P.notify (Message (Information ("File already in session: " ^ f)))
944
    with Not_found ->
945
      if (Sys.file_exists f) then
MARCHE Claude's avatar
MARCHE Claude committed
946 947 948 949
        let l = add_file cont f in
        let file = find_file_from_path cont.controller_session fn in
        send_new_subtree_from_file file;
        read_and_send (Session_itp.system_path cont.controller_session file);
950
        begin
MARCHE Claude's avatar
MARCHE Claude committed
951
          match l with
952
          | [] ->
953
             session_needs_saving := true;
954 955 956 957 958 959 960 961 962 963
             P.notify (Message (Information "file added in session"))
          | l ->
             List.iter
               (function
                 | (loc,rel_loc,s) ->
                    P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s))))
               l
        end
      else
        P.notify (Message (Open_File_Error ("File not found: " ^ f)))
964 965


966
  (* ------------ init server ------------ *)
967

968
  let init_server ?(send_source=true) config env f =
969
    Debug.dprintf debug "loading session %s@." f;
970
    let ses,shape_version = Session_itp.load_session f in
971
    Debug.dprintf debug "creating controller@.";
972
    let c = create_controller config env ses in
973 974 975 976 977
    let shortcuts =
      Mstr.fold
        (fun s p acc -> Whyconf.Mprover.add p s acc)
        (Whyconf.get_prover_shortcuts config) Whyconf.Mprover.empty
    in
978
    let prover_list =
979 980 981 982 983 984 985 986 987
      Whyconf.Mprover.fold
        (fun pr _ acc ->
         let s = try
             Whyconf.Mprover.find pr shortcuts
           with Not_found -> ""
         in
         let n = Pp.sprintf "%a" Whyconf.print_prover pr in
         let p = Pp.sprintf "%a" Whyconf.print_prover_parseable_format pr in
         (s,n,p) :: acc) (Whyconf.get_provers config) []
988
    in
989
    load_strategies c;
990 991 992
    let transformation_list = List.map
      (fun (a, b) -> (a, Format.sprintf "@[%(%)@]" b))
      (list_transforms ()) in
993
    let strategies_list = list_strategies c in
994 995 996 997 998 999
    let infos =
      {
        provers = prover_list;
        transformations = transformation_list;
        strategies = strategies_list;
        commands =
1000
          Hstr.fold (fun c _ acc -> c :: acc) commands_table []
1001 1002
      }
    in
1003 1004 1005 1006 1007
    server_data := Some
                     { cont = c;
                       send_source = send_source;
                       global_infos = infos;
                     };
1008
    Debug.dprintf debug "reloading source files@.";
1009
    let d = get_server_data () in
1010
    let x = reload_files d.cont ~shape_version in
1011 1012
    reset_and_send_the_whole_tree ();
    (* After initial sending, we don't check anymore that there is a need to
1013
           focus on a specific node. *)
1014 1015
    get_focused_label := None;
    match x with
1016
    | [] ->
MARCHE Claude's avatar
MARCHE Claude committed
1017
       P.notify (Message (Information "Session initialized successfully"))
1018 1019 1020 1021 1022
    | l ->
       List.iter
         (function (loc,rel_loc,s) ->
                   P.notify (Message (Parse_Or_Type_Error(loc,rel_loc,s))))
         l
1023

1024

Clément Fumex's avatar
Clément Fumex committed
1025 1026
  (* ----------------- Schedule proof attempt -------------------- *)

1027 1028
  exception Return

Clément Fumex's avatar
Clément Fumex committed
1029 1030 1031
  (* Callback of a proof_attempt *)
  let callback_update_tree_proof cont panid pa_status =
    let ses = cont.controller_session in
1032 1033 1034 1035 1036 1037 1038 1039
    let node_id =
      try
        node_ID_from_pan panid
      with Not_found ->
        let parent_id = get_proof_attempt_parent ses panid in
        let parent = node_ID_from_pn parent_id in
        new_node ~parent (APa panid)
    in
1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056
    try
      begin match pa_status with
            | UpgradeProver _ ->
               let n = get_node_name (APa panid) in
               P.notify (Node_change (node_id, Name_change n))
            | Removed _ -> P.notify (Remove node_id); raise Return
            | Uninstalled _ -> ()
            | Undone | Scheduled | Running
            | Interrupted | Detached | Done _
            | InternalFailure _ -> ()
      end;
      let pa = get_proof_attempt_node ses panid in
      let new_status =
        Proof_status_change (pa_status, pa.proof_obsolete, pa.limit)
      in
      P.notify (Node_change (node_id, new_status))
    with Return -> ()
Clément Fumex's avatar
Clément Fumex committed
1057

1058 1059
  let notify_change_proved c x =
    try
1060
      let node_ID = node_ID_from_any x in
1061
      let b = any_proved c.controller_session x in
1062 1063 1064
      P.notify (Node_change (node_ID, Proved b));
      match x with
      | APa pa ->
1065 1066
         let pa = get_proof_attempt_node c.controller_session pa in
         let res = match pa.Session_itp.proof_state with
1067
           | None -> Undone
1068 1069 1070
           | Some r -> Done r
         in
         let obs = pa.proof_obsolete in
1071 1072
         Debug.dprintf debug
                       "[Itp_server.notify_change_proved: obsolete = %b@." obs;
1073 1074
         let limit = pa.limit in
         P.notify (Node_change (node_ID, Proof_status_change(res, obs, limit)))
1075
      | _ -> ()
1076
    with Not_found when not (Debug.test_flag Debug.stack_trace)->
1077
      Format.eprintf "Fatal anomaly in Itp_server.notify_change_proved@.";
1078
      exit 1
1079

1080
  let schedule_proof_attempt nid (p: Whyconf.config_prover) limit =
1081
    let d = get_server_data () in
Clément Fumex's avatar
Clément Fumex committed
1082
    let prover = p.Whyconf.prover in
1083
    let callback = callback_update_tree_proof d.cont in
1084 1085 1086 1087 1088 1089 1090 1091
    let any = any_from_node_ID nid in
    match any with
    | None -> P.notify (Message (Error "Please select a node id"))
    | Some any ->
        let unproven_goals = unproven_goals_below_id d.cont any in
        List.iter (fun id -> C.schedule_proof_attempt ?save_to:None d.cont id
            prover ~limit ~callback ~notification:(notify_change_proved d.cont))
          unproven_goals
Clément Fumex's avatar
Clément Fumex committed
1092

1093
  let schedule_edition (nid: node_ID) (prover: Whyconf.prover) =
Sylvain Dailler's avatar
Sylvain Dailler committed
1094
    let d = get_server_data () in
1095
    let callback = callback_update_tree_proof d.cont in
1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114
    let any = any_from_node_ID nid in
    match any with
    | None -> P.notify (Message (Error "Please select a node id"));
    | Some any ->
        try
          let id =
            match any with
            | APn id -> id
            | APa panid ->
                get_proof_attempt_parent d.cont.controller_session panid
            | _ -> raise Not_found
          in
          C.schedule_edition d.cont id prover
            ~callback ~notification:(notify_change_proved d.cont)
        with Not_found ->
          P.notify
            (Message
               (Error
                  "for edition you must select a proof attempt node"))
Sylvain Dailler's avatar
Sylvain Dailler committed
1115

Clément Fumex's avatar
Clément Fumex committed
1116 1117
  (* ----------------- Schedule transformation -------------------- *)

1118 1119 1120 1121
  (* Callback of a transformation.
     This contains arguments of the transformation only for pretty printing of
     errors*)
  let callback_update_tree_transform tr args status =
1122
    let d = get_server_data () in
Clément Fumex's avatar
Clément Fumex committed
1123 1124
    match status with
    | TSdone trans_id ->
1125
      let ses = d.cont.controller_session in
Clément Fumex's avatar
Clément Fumex committed
1126 1127
      let id = get_trans_parent ses trans_id in
      let nid = node_ID_from_pn id in
1128
      send_new_subtree_from_trans nid trans_id
1129 1130
    | TSfailed (_, NoProgress) ->
        P.notify (Message (Information "The transformation made no progress"))
Clément Fumex's avatar
Clément Fumex committed
1131
    | TSfailed (id, e) ->
1132 1133 1134
      let doc = try
        Pp.sprintf "%s\n%a" tr Pp.formatted (Trans.lookup_trans_desc tr)
      with | _ -> "" in
1135
      let msg, loc, arg_opt = get_exception_message d.cont.controller_session id e in
1136
      let tr_applied = tr ^ " " ^ (List.fold_left (fun x acc -> x ^ " " ^ acc) "" args) in
Sylvain Dailler's avatar
Sylvain Dailler committed
1137 1138 1139 1140 1141 1142 1143 1144 1145
      P.notify (Message (Transf_error (false, node_ID_from_pn id, tr_applied, arg_opt, loc, msg, doc)))
    | TSscheduled -> ()
    | TSfatal (id, e) ->
      let doc = try
        Pp.sprintf "%s\n%a" tr Pp.formatted (Trans.lookup_trans_desc tr)
      with | _ -> "" in
      let msg, loc, arg_opt = get_exception_message d.cont.controller_session id e in
      let tr_applied = tr ^ " " ^ (List.fold_left (fun x acc -> x ^ " " ^ acc) "" args) in
      P.notify (Message (Transf_error (true, node_ID_from_pn id, tr_applied, arg_opt, loc, msg, doc)))
Clément Fumex's avatar
Clément Fumex committed
1146

1147
  let apply_transform node_id t args =
1148
    let d = get_server_data () in
1149 1150 1151 1152

    let rec apply_transform nid t args =
      match nid with
      | APn id ->