Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

itp_server.ml 54.1 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   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 78

(****** Exception handling *********)

79
let p s id =
80
  let _,tables = Session_itp.get_task_name_table s id in
81 82 83 84 85 86
  let pr = tables.Trans.printer in
  let apr = tables.Trans.aprinter in
  (Pretty.create pr apr pr pr false)

let print_term s id fmt t =
  let module P = (val (p s id)) in P.print_term fmt t
87 88

let print_type s id fmt t =
89
  let module P = (val (p s id)) in P.print_ty fmt t
90

Sylvain Dailler's avatar
Sylvain Dailler committed
91 92 93 94 95
let print_opt_type s id fmt t =
  match t with
  | None -> Format.fprintf fmt "bool"
  | Some t -> print_type s id fmt t

96
let print_ts s id fmt t =
97
  let module P = (val (p s id)) in P.print_ts fmt t
98 99

let print_ls s id fmt t =
100
  let module P = (val (p s id)) in P.print_ls fmt t
101 102

let print_tv s id fmt t =
103
  let module P = (val (p s id)) in P.print_tv fmt t
104 105

let print_vsty s id fmt t =
106
  let module P = (val (p s id)) in P.print_vsty fmt t
107 108

let print_pr s id fmt t =
109
  let module P = (val (p s id)) in P.print_pr fmt t
110 111

let print_pat s id fmt t =
112
  let module P = (val (p s id)) in P.print_pat fmt t
113

114 115 116
let print_tdecl s id fmt t =
  let module P = (val (p s id)) in P.print_tdecl fmt t

117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172
(* Exception reporting *)

(* TODO remove references to id.id_string in this function *)
let bypass_pretty s id =
  begin fun fmt exn -> match exn with
  | Ty.TypeMismatch (t1,t2) ->
      fprintf fmt "Type mismatch between %a and %a"
        (print_type s id) t1 (print_type s id) t2
  | Ty.BadTypeArity ({Ty.ts_args = []} as ts, _) ->
      fprintf fmt "Type symbol %a expects no arguments" (print_ts s id) ts
  | 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"
        (print_ts s id) ts i (if i = 1 then "" else "s") app_arg
  | Ty.DuplicateTypeVar tv ->
      fprintf fmt "Type variable %a is used twice" (print_tv s id) tv
  | Ty.UnboundTypeVar tv ->
      fprintf fmt "Unbound type variable: %a" (print_tv s id) tv
  | Ty.UnexpectedProp ->
      fprintf fmt "Unexpected propositional type"
  | Term.BadArity ({Term.ls_args = []} as ls, _) ->
      fprintf fmt "%s %a expects no arguments"
        (if ls.Term.ls_value = None then "Predicate" else "Function") (print_ls s id) ls
  | 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")
        (print_ls s id) ls i (if i = 1 then "" else "s") app_arg
  | Term.EmptyCase ->
      fprintf fmt "Empty match expression"
  | Term.DuplicateVar vs ->
      fprintf fmt "Variable %a is used twice" (print_vsty s id) vs
  | Term.UncoveredVar vs ->
      fprintf fmt "Variable %a uncovered in \"or\"-pattern" (print_vsty s id) vs
  | Term.FunctionSymbolExpected ls ->
      fprintf fmt "Not a function symbol: %a" (print_ls s id) ls
  | Term.PredicateSymbolExpected ls ->
      fprintf fmt "Not a predicate symbol: %a" (print_ls s id) ls
  | Term.ConstructorExpected ls ->
      fprintf fmt "%s %a is not a constructor"
        (if ls.Term.ls_value = None then "Predicate" else "Function") (print_ls s id) ls
  | Term.TermExpected t ->
      fprintf fmt "Not a term: %a" (print_term s id) t
  | Term.FmlaExpected t ->
      fprintf fmt "Not a formula: %a" (print_term s id) t
  | Pattern.ConstructorExpected (ls,ty) ->
      fprintf fmt "%s %a is not a constructor of type %a"
        (if ls.Term.ls_value = None then "Predicate" else "Function") (print_ls s id) ls
        (print_type s id) ty
  | Pattern.NonExhaustive pl ->
      fprintf fmt "Pattern not covered by a match:@\n  @[%a@]"
        (print_pat s id) (List.hd pl)
  | Decl.BadConstructor ls ->
      fprintf fmt "Bad constructor: %a" (print_ls s id) ls
  | Decl.BadRecordField ls ->
      fprintf fmt "Not a record field: %a" (print_ls s id) ls
173
  | Decl.RecordFieldMissing ls ->
174
      fprintf fmt "Field %a is missing" (print_ls s id) ls
175
  | Decl.DuplicateRecordField ls ->
176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197
      fprintf fmt "Field %a is used twice in the same constructor" (print_ls s id) ls
  | Decl.IllegalTypeAlias ts ->
      fprintf fmt
        "Type symbol %a is a type alias and cannot be declared as algebraic"
        (print_ts s id) ts
  | Decl.NonFoundedTypeDecl ts ->
      fprintf fmt "Cannot construct a value of type %a" (print_ts s id) ts
  | Decl.NonPositiveTypeDecl (_ts, ls, ty) ->
      fprintf fmt "Constructor %a \
          contains a non strictly positive occurrence of type %a"
        (print_ls s id) ls (print_type s id) ty
  | Decl.InvalidIndDecl (_ls, pr) ->
      fprintf fmt "Ill-formed inductive clause %a"
        (print_pr s id) pr
  | Decl.NonPositiveIndDecl (_ls, pr, ls1) ->
      fprintf fmt "Inductive clause %a contains \
          a non strictly positive occurrence of symbol %a"
        (print_pr s id) pr (print_ls s id) ls1
  | Decl.BadLogicDecl (ls1,ls2) ->
      fprintf fmt "Ill-formed definition: symbols %a and %a are different"
        (print_ls s id) ls1 (print_ls s id) ls2
  | Decl.UnboundVar vs ->
198
      fprintf fmt "Unbound variable:\n%a" (print_vsty s id) vs
199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218
  | Decl.ClashIdent id ->
      fprintf fmt "Ident %s is defined twice" id.Ident.id_string
  | Decl.EmptyDecl ->
      fprintf fmt "Empty declaration"
  | Decl.EmptyAlgDecl ts ->
      fprintf fmt "Algebraic type %a has no constructors" (print_ts s id) ts
  | Decl.EmptyIndDecl ls ->
      fprintf fmt "Inductive predicate %a has no constructors" (print_ls s id) ls
  | 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 ->
      fprintf fmt "Cannot prove the termination of %a" (print_ls s id) ls
  | _ -> Format.fprintf fmt "Uncaught: %a" Exn_printer.exn_printer exn
  end

219
let get_exception_message ses id e =
220
  match e with
221
  | Controller_itp.Noprogress ->
222
      Pp.sprintf "Transformation made no progress\n", Loc.dummy_position, ""
223 224
  | Generic_arg_trans_utils.Arg_trans s ->
      Pp.sprintf "Error in transformation function: %s \n" s, Loc.dummy_position, ""
225 226 227 228
  | Generic_arg_trans_utils.Arg_trans_decl (s, ld) ->
      Pp.sprintf "Error in transformation %s during inclusion of following declarations:\n%a" s
        (Pp.print_list (fun fmt () -> Format.fprintf fmt "\n") (print_tdecl ses id)) ld,
      Loc.dummy_position, ""
229 230 231 232 233
  | Generic_arg_trans_utils.Arg_trans_term (s, t) ->
      Pp.sprintf "Error in transformation %s during with term:\n %a : %a " s
        (print_term ses id) t (print_opt_type ses id) t.Term.t_ty,
      Loc.dummy_position, ""
  | Generic_arg_trans_utils.Arg_trans_term2 (s, t1, t2) ->
Sylvain Dailler's avatar
Sylvain Dailler committed
234 235 236 237
      Pp.sprintf "Error in transformation %s during unification of following two terms:\n %a : %a \n %a : %a" s
        (print_term ses id) t1 (print_opt_type ses id) t1.Term.t_ty
        (print_term ses id) t2 (print_opt_type ses id) t2.Term.t_ty,
      Loc.dummy_position, ""
238 239 240 241
  | 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"
        s (print_pat ses id) pa1 (print_pat ses id) pa2, Loc.dummy_position, ""
  | Generic_arg_trans_utils.Arg_trans_type (s, ty1, ty2) ->
Sylvain Dailler's avatar
Sylvain Dailler committed
242
      Pp.sprintf "Error in transformation %s during unification of the following types:\n %a \n %a"
243
        s (print_type ses id) ty1 (print_type ses id) ty2, Loc.dummy_position, ""
244 245
  | Generic_arg_trans_utils.Arg_bad_hypothesis ("rewrite", _t) ->
      Pp.sprintf "Not a rewrite hypothesis", Loc.dummy_position, ""
246 247
  | Generic_arg_trans_utils.Cannot_infer_type s ->
      Pp.sprintf "Error in transformation %s. Cannot infer type of polymorphic element" s, Loc.dummy_position, ""
248 249 250 251
  | Args_wrapper.Arg_qid_not_found q ->
      Pp.sprintf "Following hypothesis was not found: %a \n" Typing.print_qualid q, Loc.dummy_position, ""
  | Args_wrapper.Arg_error s ->
      Pp.sprintf "Transformation raised a general error: %s \n" s, Loc.dummy_position, ""
252
  | Args_wrapper.Arg_theory_not_found s ->
253
      Pp.sprintf "Theory not found: %s" s, Loc.dummy_position, ""
254
  | Args_wrapper.Arg_parse_type_error (loc, arg, e) ->
255
      Pp.sprintf "Parsing error: %a" Exn_printer.exn_printer e, loc, arg
256
  | Args_wrapper.Unnecessary_arguments l ->
Sylvain Dailler's avatar
Sylvain Dailler committed
257
      Pp.sprintf "First arguments were parsed and typed correctly but the last following are useless:\n%a"
258
        (Pp.print_list Pp.newline (fun fmt s -> Format.fprintf fmt "%s" s)) l, Loc.dummy_position, ""
259
  | Generic_arg_trans_utils.Unnecessary_terms l ->
Sylvain Dailler's avatar
Sylvain Dailler committed
260
      Pp.sprintf "First arguments were parsed and typed correctly but the last following are useless:\n%a"
261 262
        (Pp.print_list Pp.newline
           (fun fmt s -> Format.fprintf fmt "%a" (print_term ses id) s)) l, Loc.dummy_position, ""
263
  | Args_wrapper.Arg_expected_none s ->
264
      Pp.sprintf "An argument was expected of type %s, none were given" s, Loc.dummy_position, ""
265
  | e ->
266
      (Pp.sprintf "%a" (bypass_pretty ses id) e), Loc.dummy_position, ""
267 268


Clément Fumex's avatar
Clément Fumex committed
269
module type Protocol = sig
Clément Fumex's avatar
Clément Fumex committed
270 271
  val get_requests : unit -> ide_request list
  val notify : notification -> unit
Clément Fumex's avatar
Clément Fumex committed
272 273
end

Sylvain Dailler's avatar
Sylvain Dailler committed
274
module Make (S:Controller_itp.Scheduler) (Pr:Protocol) = struct
275

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

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

280 281 282 283 284

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

285
let interrupt_query _cont _args = C.interrupt (); "interrupted"
286

287
let commands_table = Hstr.create 17
288

289
let register_command c d f = Hstr.add commands_table c (d,f)
290 291 292 293 294 295 296 297 298 299

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;
300 301 302
(*
    "list-strategies", "list available strategies", list_strategies;
*)
303 304
    "print", "<id> print the declaration where <id> was defined",
    Qtask print_id;
305
    "search", "<ids> print the declarations where all <ids> appears",
Sylvain Dailler's avatar
Sylvain Dailler committed
306 307 308
    Qtask (search_id ~search_both:false);
    "search_all", "<ids> print the declarations where one of <ids> appears",
    Qtask (search_id ~search_both:true);
309 310 311 312 313 314 315 316 317 318 319 320
(*
    "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)
 *)
  ]

321
  type server_data =
322
    { (* task_driver : Driver.driver; *)
323
      cont : Controller_itp.controller;
324 325 326
      send_source: bool;
      (* If true the server is parametered to send source mlw files as
         notifications *)
327
      global_infos : Itp_communication.global_information;
328
    }
Clément Fumex's avatar
Clément Fumex committed
329

330
  let server_data = ref None
Clément Fumex's avatar
Clément Fumex committed
331

332
  let get_server_data () =
333 334
    match !server_data with
    | None ->
335
       Format.eprintf "get_server_data(): fatal error, server not yet initialized@.";
336 337
       exit 1
    | Some x -> x
Clément Fumex's avatar
Clément Fumex committed
338

Sylvain Dailler's avatar
Sylvain Dailler committed
339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363
(* 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

  let any_from_node_ID (nid:node_ID) : any = Hint.find model_any nid

  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
  let file_to_node_ID : node_ID Hstr.t = Hstr.create 3

  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)
364
  let node_ID_from_file file = Hstr.find file_to_node_ID (file_name file)
Sylvain Dailler's avatar
Sylvain Dailler committed
365 366 367 368 369 370 371 372 373 374 375 376

  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 ->
377
        let nid = Hstr.find file_to_node_ID (file_name file) in
Sylvain Dailler's avatar
Sylvain Dailler committed
378
        Hint.remove model_any nid;
379
        Hstr.remove file_to_node_ID (file_name file)
Sylvain Dailler's avatar
Sylvain Dailler committed
380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398
    | 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
399
    | AFile file -> Hstr.add file_to_node_ID (file_name file) new_id
Sylvain Dailler's avatar
Sylvain Dailler committed
400 401 402 403 404 405
    | 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


406 407 408 409 410 411 412 413
(*******************************)
(* Compute color for locations *)
(*******************************)

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

exception No_loc_on_goal

414 415 416 417 418 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 450 451 452 453 454
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 ->
      let g = Sysutil.relativize_filename session_dir f in
      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 ->
455 456 457 458 459
      (* 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
460
    | Some loc -> color_loc ~color:Goal_color ~loc in
461
  let goal_id : Ident.ident = (Task.task_goal task).Decl.pr_name in
462
  color_goal goal_id.Ident.id_loc;
463
  let rec scan = function
464
    | Some
465 466
        { Task.task_prev = prev;
          Task.task_decl =
467
            { Theory.td_node =
468 469
                Theory.Decl { Decl.d_node = Decl.Dprop (k, _, f) }}} ->
      begin match k with
470 471
      | Decl.Pgoal  -> color_t_locs ~premise:false f
      | Decl.Paxiom -> color_t_locs ~premise:true  f
472 473 474 475 476
      | _ -> assert false
      end;
      scan prev
    | Some { Task.task_prev = prev } -> scan prev
    | _ -> () in
477 478
  scan task;
  !list
479

Sylvain Dailler's avatar
Sylvain Dailler committed
480 481
let get_modified_node n =
  match n with
482
  | Reset_whole_tree -> None
Sylvain Dailler's avatar
Sylvain Dailler committed
483 484 485 486 487 488 489 490 491 492
  | New_node (nid, _, _, _, _) -> Some nid
  | Node_change  (nid, _) -> Some nid
  | Remove nid -> Some nid
  | Next_Unproven_Node_Id (_, nid) -> Some nid
  | Initialized _ -> None
  | Saved -> None
  | Message _ -> None
  | Dead _ -> None
  | Task (nid, _, _) -> Some nid
  | File_contents _ -> None
493
  | Source_and_ce _ -> None
Sylvain Dailler's avatar
Sylvain Dailler committed
494

495

496 497
type focus =
  | Unfocused
498 499
(* We can focus on several nodes at once *)
  | Focus_on of Session_itp.any list
500 501
  | Wait_focus

Sylvain Dailler's avatar
Sylvain Dailler committed
502
(* Focus on a node *)
503 504 505
let focused_node = ref Unfocused
let get_focused_label = ref None

506 507
let focus_on_loading (f: Task.task -> bool) =
  focused_node := Wait_focus;
508
  get_focused_label := Some f
Sylvain Dailler's avatar
Sylvain Dailler committed
509 510 511 512 513 514

(* TODO *)
module P = struct

  let get_requests = Pr.get_requests

515 516
  (* true if nid is below f_node or does not exists (in which case the
     notification is a remove). false if not below.  *)
517
  let is_below s nid f_nodes =
518 519 520
    let any = try Some (any_from_node_ID nid) with _ -> None in
    match any with
    | None -> true
521 522
    | Some any ->
        List.exists (Session_itp.is_below s any) f_nodes
523

Sylvain Dailler's avatar
Sylvain Dailler committed
524 525 526
  let notify n =
    let d = get_server_data() in
    let s = d.cont.controller_session in
527 528 529 530 531 532 533 534 535 536 537 538 539 540 541
    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
Sylvain Dailler's avatar
Sylvain Dailler committed
542 543 544

end

545 546 547 548 549 550 551
  (*********************)
  (* File input/output *)
  (*********************)

  let read_and_send f =
    try
      let d = get_server_data() in
552 553 554 555 556
      if d.send_source then
        let fn = Sysutil.absolutize_filename
            (Session_itp.get_dir d.cont.controller_session) f in
        let s = Sysutil.file_contents fn in
        P.notify (File_contents (f, s))
557 558 559 560 561 562 563
    with Invalid_argument s ->
      P.notify (Message (Error s))

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

Sylvain Dailler's avatar
Sylvain Dailler committed
571 572 573 574 575
  let relativize_location s loc =
    let f, l, b, e = Loc.get loc in
    let f = Sysutil.relativize_filename (Session_itp.get_dir s) f in
    Loc.user_position f l b e

576
  let capture_parse_or_type_errors f cont =
577 578 579 580
    List.map
      (function
        | Loc.Located (loc, e) ->
           let rel_loc = relativize_location cont.controller_session loc in
MARCHE Claude's avatar
MARCHE Claude committed
581 582
           let s = Format.asprintf "%a: %a" Loc.gen_report_position rel_loc
                                   Exn_printer.exn_printer e in
583 584 585 586 587 588
           (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)
589 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. *)
  let reload_files cont ~use_shapes =
593
    capture_parse_or_type_errors
594 595 596
      (fun c ->
        try let (_,_) = reload_files ~use_shapes c in [] with
        | Errors_list le -> le) cont
597

Sylvain Dailler's avatar
Sylvain Dailler committed
598
  let add_file cont ?format fname =
599 600
    capture_parse_or_type_errors
      (fun c ->
601 602
        try add_file c ?format fname; [] with
        | Errors_list le -> le) cont
603

604

Sylvain Dailler's avatar
Sylvain Dailler committed
605
  (* -----------------------------------   ------------------------------------- *)
Clément Fumex's avatar
Clément Fumex committed
606

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

  let get_node_name (node: any) =
616
    let d = get_server_data () in
617
    match node with
618 619
    | AFile file -> file_name file
    | ATh th -> (theory_name th).Ident.id_string
620
    | ATn tn ->
621 622 623 624 625 626
       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
627
    | APn pn ->
628
       let name = (get_proof_name d.cont.controller_session pn).Ident.id_string in
629 630 631 632
       (* 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
MARCHE Claude's avatar
MARCHE Claude committed
633
       let expl = get_proof_expl d.cont.controller_session pn in
634
       if expl = "" then name else name ^ " [" ^ expl ^ "]"
635
    | APa pa ->
636
      let pa = get_proof_attempt_node d.cont.controller_session pa in
637 638
      Pp.string_of Whyconf.print_prover pa.prover

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

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

667

668
(*
Sylvain Dailler's avatar
Sylvain Dailler committed
669 670 671 672 673
  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
674
        NFile, {name; proved}
Sylvain Dailler's avatar
Sylvain Dailler committed
675 676 677
    | ATh th     ->
        let name = (theory_name th).Ident.id_string in
        let proved = th_proved cont th in
678
        NTheory, {name; proved}
Sylvain Dailler's avatar
Sylvain Dailler committed
679 680 681
    | ATn tn     ->
        let name = get_transf_name ses tn in
        let proved = tn_proved cont tn in
682
        NTransformation, {name; proved}
Sylvain Dailler's avatar
Sylvain Dailler committed
683 684 685
    | APn pn     ->
        let name = (get_proof_name ses pn).Ident.id_string in
        let proved = pn_proved cont pn in
686
          NGoal, {name; proved}
Sylvain Dailler's avatar
Sylvain Dailler committed
687 688 689
    | 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
690 691 692
        let pr, proved = match pa.Session_itp.proof_state with
        | Some pr -> Some pr.pr_answer, pr.pr_answer = Valid
        | None -> None, false
Sylvain Dailler's avatar
Sylvain Dailler committed
693
        in
Clément Fumex's avatar
Clément Fumex committed
694 695
        (NProofAttempt (pr, pa.proof_obsolete)),
        {name; proved}
696
*)
Sylvain Dailler's avatar
Sylvain Dailler committed
697

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

703 704 705 706
  (* 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 =
707 708 709 710 711 712 713
    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 ->
714
              let task = Session_itp.get_task session pr_node in
715 716 717 718 719
              let b = label_detection task in
              if b then
                add_focused_node node
          | _ -> ())
      | None -> ()
720

Sylvain Dailler's avatar
Sylvain Dailler committed
721
  (* Create a new node in the_tree, update the tables and send a
Clément Fumex's avatar
Clément Fumex committed
722
     notification about it *)
Sylvain Dailler's avatar
Sylvain Dailler committed
723
  let new_node ~parent node : node_ID =
724 725
    let new_id = fresh () in
      Hint.add model_any new_id node;
726 727
      let node_type = get_node_type node in
      let node_name = get_node_name node in
728
      let node_detached = get_node_detached node in
Sylvain Dailler's avatar
Sylvain Dailler committed
729
      add_node_to_table node new_id;
730 731
      (* Specific to auto-focus at initialization of itp_server *)
      focus_on_label node;
732 733 734 735 736 737 738 739
      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
740 741
      new_id

742 743 744 745
  (* 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
746 747 748
  (****************************)
  (* Iter on the session tree *)
  (****************************)
Sylvain Dailler's avatar
Sylvain Dailler committed
749

750 751 752 753
  (* 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 =
754
    let d = get_server_data () in
Clément Fumex's avatar
Clément Fumex committed
755
    Whyconf.Hprover.iter
756
      (fun _pa panid -> f ~parent (APa panid))
757
      (get_proof_attempt_ids d.cont.controller_session id)
Clément Fumex's avatar
Clément Fumex committed
758

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

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

780 781 782 783 784 785 786
  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)

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

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

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

807

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

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

815 816
  let reset_and_send_the_whole_tree (): unit =
    P.notify Reset_whole_tree;
817 818
    iter_on_files
      ~on_file:(fun file -> read_and_send (file_name file))
819
      ~on_subtree:create_node
820

821 822 823
  let unfocus () =
    focused_node := Unfocused;
    reset_and_send_the_whole_tree ()
824

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

838
  let create_ce_tab s res any list_loc =
839 840 841 842 843
    let f = get_encapsulating_file s any in
    let filename = Sysutil.absolutize_filename
      (Session_itp.get_dir s) (file_name f)
    in
    let source_code = Sysutil.file_contents filename in
844
    Model_parser.interleave_with_source ?start_comment:None ?end_comment:None
845
      ?me_name_trans:None res.Call_provers.pr_model ~rel_filename:(file_name f)
846
      ~source_code:source_code ~locations:list_loc
847

848
  let send_task nid show_full_context loc =
849
    let d = get_server_data () in
850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880
    let any = any_from_node_ID nid in
    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 ->
          P.notify (Task (nid, "Detached file " ^ file_name f, []))
      | 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 ->
          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
881
          let s, old_list_loc = task_of_id d parid show_full_context loc in
882 883
          let prover_text = s ^ "\n====================> Prover: " ^ name ^ "\n" in
          (* Display the result of the prover *)
884
          begin
885 886 887 888 889 890 891 892
            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 =
                  Pp.string_of (Model_parser.print_model_human ?me_name_trans:None)
893
                  res.Call_provers.pr_model
894 895
                in
                if ce_result = "" then
896 897 898 899
                  let result_pr =
                    result ^ "\n\n" ^ "The prover did not return counterexamples."
                  in
                  P.notify (Task (nid, prover_text ^ result_pr, old_list_loc))
900
                else
901
                  begin
902 903 904 905 906 907 908 909
                    let result_pr =
                      result ^ "\n\n" ^ "Counterexample suggested by the prover:\n\n" ^ ce_result
                    in
                    let (source_result, list_loc) =
                      create_ce_tab d.cont.controller_session res any old_list_loc
                    in
                    P.notify (Source_and_ce (source_result, list_loc));
                    P.notify (Task (nid, prover_text ^ result_pr, old_list_loc))
910
                  end
911 912
            | None -> P.notify (Task (nid, "Result of the prover not available.\n", old_list_loc))
          end
913 914 915 916 917 918 919 920 921
      | AFile f ->
          P.notify (Task (nid, "File " ^ file_name f, []))
      | 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))
922

Sylvain Dailler's avatar
Sylvain Dailler committed
923 924 925 926 927 928 929
  (* -------------------- *)

  (* 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 =
    let fn = Sysutil.relativize_filename
930 931 932 933 934 935 936 937 938
      (get_dir cont.controller_session) f in
    let fn_exists =
      try Some (get_file cont.controller_session fn)
      with | Not_found -> None
    in
    match fn_exists with
    | None ->
        if (Sys.file_exists f) then
          begin
939
            match add_file cont f with