server_utils.ml 20.3 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 13
open Wstdlib

14
let debug = Debug.register_flag ~desc:"ITP server" "itp_server"
15

16 17 18 19 20 21 22 23 24 25 26 27 28
let has_extension f =
  try
    let _ = Filename.chop_extension f in true
  with Invalid_argument _ -> false

let get_session_dir ~allow_mkdir files =
  if Queue.is_empty files then invalid_arg "no files given";
  let first = Queue.pop files in
  let dir =
    if Sys.file_exists first then
      if Sys.is_directory first then
        (* first is a directory *)
        first
29 30 31
      else if Filename.basename first = "why3session.xml" then
        (* first is a session file *)
        Filename.dirname first
32 33 34 35 36 37 38 39
      else
        if Queue.is_empty files then
          (* first was the only file *)
          let d =
            try Filename.chop_extension first
            with Invalid_argument _ ->
              invalid_arg ("'" ^ first ^ "' has no extension and is not a directory")
          in
40
          Queue.push first files;
41 42 43
          d
        else
          invalid_arg ("'" ^ first ^ "' is not a directory")
44
    else
45
      (* first does not exist *)
46 47 48
      if has_extension first then
        invalid_arg ("file not found: " ^ first)
      else first
49
  in
50 51
  if not (Sys.file_exists dir) then
    begin
52
      if allow_mkdir then Unix.mkdir dir 0o700 else
53 54 55
        invalid_arg ("session directory '" ^ dir ^ "' not found")
    end;
  dir
Sylvain Dailler's avatar
Sylvain Dailler committed
56 57 58 59 60 61 62 63 64 65 66


(******************)
(* Simple queries *)
(******************)

(**** interpretation of command-line ****)

let sort_pair (x,_) (y,_) = String.compare x y

let list_transforms () =
67
  let l =
Sylvain Dailler's avatar
Sylvain Dailler committed
68 69 70
    List.rev_append
      (List.rev_append (Trans.list_transforms ()) (Trans.list_transforms_l ()))
      (List.rev_append (Trans.list_transforms_with_args ()) (Trans.list_transforms_with_args_l ()))
71
  in List.sort sort_pair l
Sylvain Dailler's avatar
Sylvain Dailler committed
72 73 74 75

let list_transforms_query _cont _args =
  let l = list_transforms () in
  let print_trans_desc fmt (x,r) =
76
    Format.fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" x Pp.formatted r
Sylvain Dailler's avatar
Sylvain Dailler committed
77
  in
78
  Pp.string_of (Pp.print_list Pp.newline2 print_trans_desc) l
Sylvain Dailler's avatar
Sylvain Dailler committed
79 80 81 82 83 84 85 86 87 88 89

let list_provers cont _args =
  let l =
    Whyconf.Hprover.fold
      (fun p _ acc -> (Pp.sprintf "%a" Whyconf.print_prover p)::acc)
      cont.Controller_itp.controller_provers
      []
  in
  let l = List.sort String.compare l in
  Pp.sprintf "%a" (Pp.print_list Pp.newline Pp.string) l

90 91 92 93
let load_strategies cont =
  let config = cont.Controller_itp.controller_config in
  let env = cont.Controller_itp.controller_env in
  let strategies = Whyconf.get_strategies config in
94
  Mstr.iter
95 96 97 98 99 100 101
    (fun _ st ->
     let name = st.Whyconf.strategy_name in
     try
       let code = st.Whyconf.strategy_code in
       let code = Strategy_parser.parse env config code in
       let shortcut = st.Whyconf.strategy_shortcut in
       Debug.dprintf debug "[session server info] Strategy '%s' loaded.@." name;
102
       Hstr.add cont.Controller_itp.controller_strategies name
MARCHE Claude's avatar
MARCHE Claude committed
103
                       (name, shortcut, st.Whyconf.strategy_desc, code)
104
     with Strategy_parser.SyntaxError msg ->
105
       Format.eprintf "Fatal: loading strategy '%s' failed: %s \nSolve this problem in your why3.conf file and retry.@." name msg;
106
       exit 1)
107 108 109
    strategies

let list_strategies cont =
110
  Hstr.fold (fun _ (name,short,_,_) acc -> (short,name)::acc) cont.Controller_itp.controller_strategies []
111

112 113 114 115 116
let symbol_name s =
  match s with
  | Args_wrapper.Tstysymbol ts -> ts.Ty.ts_name
  | Args_wrapper.Tsprsymbol pr -> pr.Decl.pr_name
  | Args_wrapper.Tslsymbol ls -> ls.Term.ls_name
Sylvain Dailler's avatar
Sylvain Dailler committed
117

118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136
(* Prints a constructor in a string using the inductive list definition
   containing the constructor *)
let print_constr_string ~print_term ~print_pr il pr =
  (* The inductive type is an lsymbol: we are sure to get a constructor *)
      let constr_def =
        List.fold_left (fun acc (_, ind_decl) ->
            List.fold_left (fun acc x ->
                if Decl.pr_equal (fst x) pr then
                  Some x
                else
                  acc) acc ind_decl)
          None il
      in
      match constr_def with
      | None -> raise Not_found (* construct was not found: should not happen *)
      | Some (_, t_def) ->
          let s = Pp.string_of print_term t_def in
          Pp.string_of print_pr pr ^ ": " ^ s

Sylvain Dailler's avatar
Sylvain Dailler committed
137 138 139 140 141 142 143
(* The id you are trying to use is undefined *)
exception Undefined_id of string
(* Bad number of arguments *)
exception Number_of_arguments

let print_id s tables =
  (* let tables = Args_wrapper.build_name_tables task in*)
144
  let km = tables.Trans.known_map in
145 146
  let table_id =
    try Args_wrapper.find_symbol s tables with
Sylvain Dailler's avatar
Sylvain Dailler committed
147 148
    | Args_wrapper.Arg_parse_type_error _
    | Args_wrapper.Arg_qid_not_found _ -> raise (Undefined_id s)
Sylvain Dailler's avatar
Sylvain Dailler committed
149
  in
150 151 152 153
  (* Check that the symbol is defined *)
  let d = (* Not_found should not happend *)
    Ident.Mid.find (symbol_name table_id) km
  in
154 155 156 157 158
  (* We use snapshots of printers to avoid registering new value insides it only
     to print info messages to the user.
  *)
  let pr = Ident.duplicate_ident_printer tables.Trans.printer in
  let apr = Ident.duplicate_ident_printer tables.Trans.aprinter in
159
  let module P = (val Pretty.create pr apr pr pr false) in
160 161 162 163 164
  (* Different constructs are printed differently *)
  match d.Decl.d_node, table_id with
  | Decl.Dind (_, il), Args_wrapper.Tsprsymbol pr ->
      print_constr_string ~print_term:P.print_term ~print_pr:P.print_pr il pr
  | _ -> Pp.string_of P.print_decl d
165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181

(* searching ids in declarations *)

let occurs_in_type id = Ty.ty_s_any (fun ts -> Ident.id_equal ts.Ty.ts_name id)

let occurs_in_term id =
  Term.t_s_any (occurs_in_type id) (fun ls -> Ident.id_equal id ls.Term.ls_name)

let occurs_in_constructor id (cs,projs) =
  Ident.id_equal cs.Term.ls_name id ||
    List.exists (function Some ls -> Ident.id_equal ls.Term.ls_name id | None -> false) projs

let occurs_in_defn id (ls,def) =
  Ident.id_equal ls.Term.ls_name id ||
  let (_vl,t) = Decl.open_ls_defn def in occurs_in_term id t

let occurs_in_ind_decl id (_,clauses) =
182 183
  List.exists (fun (pr,t) ->
      Ident.id_equal id pr.Decl.pr_name || occurs_in_term id t) clauses
184 185 186 187 188 189 190 191 192 193 194 195 196 197 198

let occurs_in_decl d id =
  Decl.(match d.d_node with
  | Decl.Dtype ts -> Ident.id_equal ts.Ty.ts_name id (* look through ts.ys_def *)
  | Decl.Ddata dl ->
      List.exists
        (fun ((ts,c): data_decl) ->
         Ident.id_equal ts.Ty.ts_name id || List.exists (occurs_in_constructor id) c)
        dl
  | Decl.Dparam ls -> Ident.id_equal ls.Term.ls_name id
  | Decl.Dlogic dl -> List.exists (occurs_in_defn id) dl
  | Decl.Dind (_, il) -> List.exists (occurs_in_ind_decl id) il
  | Dprop ((Paxiom|Plemma), pr, t) -> Ident.id_equal pr.pr_name id || occurs_in_term id t
  | Dprop _ -> false)

Sylvain Dailler's avatar
Sylvain Dailler committed
199
let do_search ~search_both km idl =
200 201
  Ident.Mid.fold
    (fun _ d acc ->
Sylvain Dailler's avatar
Sylvain Dailler committed
202 203 204
      if search_both then
        (if List.exists (occurs_in_decl d) idl then Decl.Sdecl.add d acc else acc)
      else
205 206
        (if List.for_all (occurs_in_decl d) idl then Decl.Sdecl.add d acc else acc))
    km Decl.Sdecl.empty
207

Sylvain Dailler's avatar
Sylvain Dailler committed
208
let search ~search_both s tables =
209
  let ids = List.rev_map
210 211 212
              (fun s -> try symbol_name (Args_wrapper.find_symbol s tables)
                        with Args_wrapper.Arg_parse_type_error _ |
                             Args_wrapper.Arg_qid_not_found _ -> raise (Undefined_id s)) s
213
  in
Sylvain Dailler's avatar
Sylvain Dailler committed
214
  let l = do_search ~search_both tables.Trans.known_map ids in
215
  if Decl.Sdecl.is_empty l then
Sylvain Dailler's avatar
Sylvain Dailler committed
216 217
    (* In case where search_both is true, this error cannot appear because there
       is at least one declaration: the definition of the ident. *)
218 219 220 221 222
       Pp.sprintf
         "No declaration contain all the %d identifiers @[%a@]"
         (List.length ids)
         (Pp.print_list Pp.space (fun fmt id -> Pp.string fmt id.Ident.id_string))
         ids
223 224 225 226 227 228 229 230 231
    else
      let l = Decl.Sdecl.elements l in
      (* We use snapshots of printers to avoid registering new value insides it
         only to print info messages to the user.
      *)
      let pr = Ident.duplicate_ident_printer tables.Trans.printer in
      let apr = Ident.duplicate_ident_printer tables.Trans.aprinter in
      let module P = (val Pretty.create pr apr pr pr false) in
      Pp.string_of (Pp.print_list Pp.newline2 P.print_decl) l
232 233 234 235 236

let print_id _cont task args =
  match args with
  | [s] -> print_id s task
  | _ -> raise Number_of_arguments
Sylvain Dailler's avatar
Sylvain Dailler committed
237

Sylvain Dailler's avatar
Sylvain Dailler committed
238
let search_id ~search_both _cont task args =
Sylvain Dailler's avatar
Sylvain Dailler committed
239
  match args with
240
  | [] -> raise Number_of_arguments
Sylvain Dailler's avatar
Sylvain Dailler committed
241
  | _ -> search ~search_both args task
Sylvain Dailler's avatar
Sylvain Dailler committed
242 243 244

type query =
  | Qnotask of (Controller_itp.controller -> string list -> string)
245
  | Qtask of (Controller_itp.controller -> Trans.naming_table -> string list -> string)
Sylvain Dailler's avatar
Sylvain Dailler committed
246

Sylvain Dailler's avatar
Sylvain Dailler committed
247

Sylvain Dailler's avatar
Sylvain Dailler committed
248
let help_on_queries fmt commands =
249
  let l = Hstr.fold (fun c (h,_) acc -> (c,h)::acc) commands [] in
Sylvain Dailler's avatar
Sylvain Dailler committed
250
  let l = List.sort sort_pair l in
251
  let p fmt (c,help) = Format.fprintf fmt "%20s : %s" c help in
Sylvain Dailler's avatar
Sylvain Dailler committed
252 253 254 255 256 257 258 259 260 261 262 263
  Format.fprintf fmt "%a" (Pp.print_list Pp.newline p) l

(* Return the prover corresponding to given name. name is of the form
  | name
  | name, version
  | name, altern
  | name, version, altern *)
let return_prover name config =
  let fp = Whyconf.parse_filter_prover name in
  (** all provers that have the name/version/altern name *)
  let provers = Whyconf.filter_provers config fp in
  if Whyconf.Mprover.is_empty provers then begin
264
    Debug.dprintf debug "Prover corresponding to %s has not been found@." name;
Sylvain Dailler's avatar
Sylvain Dailler committed
265 266 267 268
    None
  end else
    Some (snd (Whyconf.Mprover.choose provers))

269 270 271 272 273
type command_prover =
  | Bad_Arguments of Whyconf.prover
  | Not_Prover
  | Prover of (Whyconf.config_prover * Call_provers.resource_limit)

Sylvain Dailler's avatar
Sylvain Dailler committed
274 275
(* Parses the Other command. If it fails to parse it, it answers None otherwise
   it returns the config of the prover together with the ressource_limit *)
276
let parse_prover_name config name args : command_prover =
Sylvain Dailler's avatar
Sylvain Dailler committed
277
  match (return_prover name config) with
278
  | None -> Not_Prover
Sylvain Dailler's avatar
Sylvain Dailler committed
279 280
  | Some prover_config ->
    begin
281 282 283 284 285
      let prover = prover_config.Whyconf.prover in
      try
        if (List.length args > 2) then Bad_Arguments prover else
        match args with
        | [] ->
286 287
            let limit_time = Whyconf.timelimit (Whyconf.get_main config) in
            let limit_mem = Whyconf.memlimit (Whyconf.get_main config) in
288
            let default_limit = Call_provers.{empty_limit with
289 290
                                              limit_time = limit_time;
                                              limit_mem = limit_mem} in
291
            Prover (prover_config, default_limit)
292 293 294 295 296 297
        | [timeout] ->
            let limit_mem = Whyconf.memlimit (Whyconf.get_main config) in
            Prover (prover_config,
                    Call_provers.{empty_limit with
                                  limit_time = int_of_string timeout;
                                  limit_mem = limit_mem})
298 299 300 301 302 303 304
        | [timeout; oom ] ->
            Prover (prover_config, Call_provers.{empty_limit with
                                                 limit_time = int_of_string timeout;
                                                 limit_mem = int_of_string oom})
        | _ -> Bad_Arguments prover
      with
      | Failure _ -> Bad_Arguments prover
Sylvain Dailler's avatar
Sylvain Dailler committed
305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346
    end

(*******************************)
(* Prover command line parsing *)
(*******************************)


(* splits input string [s] into substrings separated by space
   spaces inside quotes or parentheses are not separator.
   implemented as a hardcoded automaton:
*)
let split_args s =
  let args = ref [] in
  let par_depth = ref 0 in
  let b = Buffer.create 17 in
  let push_arg () =
    let x = Buffer.contents b in
    if String.length x > 0 then (args := x :: !args; Buffer.clear b)
  in
  let push_char c = Buffer.add_char b c in
  let state = ref 0 in
  for i = 0 to String.length s - 1 do
    let c = s.[i] in
    match !state, c with
    | 0,' ' -> if !par_depth > 0 then push_char c else push_arg ()
    | 0,'(' -> incr par_depth; push_char c
    | 0,')' -> decr par_depth; push_char c
    | 0,'"' -> state := 1; if !par_depth > 0 then push_char c
    | 0,_ -> push_char c
    | 1,'"' -> state := 0; if !par_depth > 0 then push_char c
    | 1,_ -> push_char c
    | _ -> assert false
  done;
  push_arg ();
  match List.rev !args with
    | a::b -> a,b
    | [] -> "",[]

type command =
  | Transform    of string * Trans.gentrans * string list
  | Prove        of Whyconf.config_prover * Call_provers.resource_limit
  | Strategies   of string
347
  | Edit         of Whyconf.prover
348
  | Get_ce
349
  | Bisect
350
  | Replay       of bool
Sylvain Dailler's avatar
Sylvain Dailler committed
351 352
  | Clean
  | Mark_Obsolete
353 354
  | Focus_req
  | Unfocus_req
Sylvain Dailler's avatar
Sylvain Dailler committed
355 356 357 358 359
  | Help_message of string
  | Query        of string
  | QError       of string
  | Other        of string * string list

360
let query_on_task cont f id args =
361
  let _,table = Session_itp.get_task_name_table cont.Controller_itp.controller_session id in
362 363 364 365
  try Query (f cont table args) with
    | Undefined_id s -> QError ("No existing id corresponding to " ^ s)
    | Number_of_arguments -> QError "Bad number of arguments"

366 367 368 369 370 371 372 373 374
let help_message commands_table =
  Pp.sprintf
    "Please type a command among the following (automatic completion available)@\n\
     @\n\
     @ <transformation name> [arguments]@\n\
     @ <prover shortcut> [<time limit> [<mem limit>]]@\n\
     @ <query> [arguments]@\n\
     @ <strategy shortcut>@\n\
     @ bisect @\n\
375 376
     @ clean @\n\
     @ edit @\n\
377
     @ get-ce @\n\
378
     @ Focus @\n\
379 380
     @ help <transformation_name> @\n\
     @ list_ide_command @ \n\
381 382 383
     @ mark @\n\
     @ replay [all]@\n\
     @ Unfocus @\n\
384 385
     @\n\
     Available queries are:@\n@[%a@]" help_on_queries commands_table
386

387
let interp commands_table cont id s =
Sylvain Dailler's avatar
Sylvain Dailler committed
388
  let cmd,args = split_args s in
389
  (* We first try to apply a command from commands_table (itp_server.ml) *)
390
  match Hstr.find commands_table cmd with
Sylvain Dailler's avatar
Sylvain Dailler committed
391 392 393 394 395
  | (_, f) ->
    begin
      match f,id with
      | Qnotask f, _ -> Query (f cont args)
      | Qtask f, Some (Session_itp.APn id) ->
396 397 398 399 400 401
          query_on_task cont f id args
      | Qtask f, Some (Session_itp.APa pid) ->
          let id = Session_itp.get_proof_attempt_parent
              cont.Controller_itp.controller_session pid
          in
          query_on_task cont f id args
Sylvain Dailler's avatar
Sylvain Dailler committed
402 403 404
      | Qtask _, _ -> QError "please select a goal first"
    end
  | exception Not_found ->
405 406 407 408 409 410 411 412 413
     (* If the command entered is not in the commands_table, we first try to
        apply a transformation, then a prover, then a strategy and finally an
        interactive command.
      *)
   if id != None &&
     Session_itp.is_detached cont.Controller_itp.controller_session (Opt.get id)
   then
      match cmd, args with
      | "help", _ ->
414 415
          let text = help_message commands_table in
          Help_message text
416 417
      | _ -> QError ("Command cannot be applied on a detached node")
   else
Sylvain Dailler's avatar
Sylvain Dailler committed
418
     begin
419 420 421
       try
         let t = Trans.lookup_trans cont.Controller_itp.controller_env cmd in
         match id with
422 423
         | Some _ -> Transform (cmd,t,args)
         | None -> QError ("Please select a goal or trans node in the task tree")
424 425 426
       with
       | Trans.UnknownTrans _ ->
          match parse_prover_name cont.Controller_itp.controller_config cmd args with
427
          | Prover (prover_config, limit) ->
428 429 430 431 432 433 434 435 436
             begin
               match id with
               | None -> QError ("Please select a node in the task tree")
               | Some _id ->
                   if prover_config.Whyconf.interactive then
                     Edit prover_config.Whyconf.prover
                   else
                     Prove (prover_config, limit)
             end
437 438 439
          | Bad_Arguments prover ->
              QError (Format.asprintf "Prover %a was recognized but arguments were not parsed" Whyconf.print_prover prover)
          | Not_Prover ->
440
             if Hstr.mem cont.Controller_itp.controller_strategies cmd then
441 442 443
               match id with
               | None   -> QError ("Please select a node in the task tree")
               | Some _ -> Strategies cmd
444 445 446 447 448 449 450 451 452
             else
               match cmd, args with
               | "edit", _ ->
                  begin
                    match id with
                    | Some (Session_itp.APa id) ->
                       let pa =
                         Session_itp.get_proof_attempt_node
                           cont.Controller_itp.controller_session id in
453
                       Edit pa.Session_itp.prover
454 455
                    | _ ->  QError ("Please select a proof node in the task tree")
                  end
456 457 458 459 460 461 462
               | "get-ce", _ ->
                   begin
                     match id with
                    | Some (Session_itp.APa _) ->
                       Get_ce
                    | _ ->  QError ("Please select a proof node in the task tree")
                   end
463 464 465 466 467 468
               | "bisect", _ ->
                  begin
                    match id with
                    | Some (Session_itp.APa _) -> Bisect
                    | _ ->  QError ("Please select a proof node in the task tree")
                  end
469
               | "replay", args ->
Sylvain Dailler's avatar
Sylvain Dailler committed
470
                   begin
471 472 473 474
                     match args with
                     | [] -> Replay true
                     | ["all"] -> Replay false
                     | _ -> QError ("replay expects either no arguments or `all`")
Sylvain Dailler's avatar
Sylvain Dailler committed
475 476
                   end
               | "mark", _ ->
477
                   Mark_Obsolete
478
               | "Focus", _ ->
479 480 481 482 483 484
                   begin
                     match id with
                     | None ->
                         QError ("Select at least one node of the task tree")
                     | Some _ -> Focus_req
                   end
485 486
               | "Unfocus", _ ->
                   Unfocus_req
Sylvain Dailler's avatar
Sylvain Dailler committed
487
               | "clean", _ ->
488
                   Clean
489 490 491 492 493 494 495 496 497 498
               | "help", [trans] ->
                  let print_trans_desc fmt r =
                    Format.fprintf fmt "@[%s:\n%a@]" trans Pp.formatted r
                  in
                  (try
                      let desc = Trans.lookup_trans_desc trans in
                      Help_message (Pp.string_of print_trans_desc desc)
                    with
                    | Not_found -> QError (Pp.sprintf "Transformation %s does not exists" trans))
               | "help", _ ->
499
                  let text = help_message commands_table in
500 501 502
                  Help_message text
               | _ ->
                  Other (cmd, args)
Sylvain Dailler's avatar
Sylvain Dailler committed
503
      end
504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520

(***********************)
(* First Unproven goal *)
(***********************)

(* Children should not give the proof attempts *)
let rec unproven_goals_below_node ~proved ~children ~is_goal acc node =
  if proved node then
    acc
  else
    let nodes = children node in
    if is_goal node && nodes = [] then
      node :: acc
    else
      List.fold_left (unproven_goals_below_node ~proved ~children ~is_goal)
        acc nodes

Sylvain Dailler's avatar
Sylvain Dailler committed
521 522 523 524 525 526 527 528 529 530 531 532 533 534
(* [split_list l node] returns a pair of list which contains the elements that
   appear before node (respectively after node). *)
let split_list l node =
  let rec split_list l acc =
    match l with
    | [] -> ([], List.rev acc)
    | hd :: tl ->
        if hd = node then
          (List.rev acc, tl)
        else
          split_list tl (hd :: acc)
  in
  split_list l []

535
let get_first_unproven_goal_around
536
    ~always_send ~proved ~children ~get_parent ~is_goal ~is_pa node =
537 538 539 540 541 542 543 544 545 546
  let rec look_around node =
    match get_parent node with
    | None -> unproven_goals_below_node ~proved ~children ~is_goal [] node
    | Some parent ->
        if proved parent then
          look_around parent
        else
          unproven_goals_below_node ~proved ~children ~is_goal [] parent
  in
  let node = if is_pa node then Opt.get (get_parent node) else node in
Sylvain Dailler's avatar
Sylvain Dailler committed
547 548 549 550 551 552 553 554 555
  let node_list = look_around node in
  (* We look into this list of brothers in case the original node is inside it.
     If it is inside the list, we want to get the first non proved node after
     the original node. *)
  let (before_node, after_node) = split_list (List.rev node_list) node in
  match after_node with
  | [] ->
    begin
      match before_node with
556
      | [] -> if always_send then Some node else None
Sylvain Dailler's avatar
Sylvain Dailler committed
557 558
      | hd :: _tl -> Some hd
    end
559
  | hd :: _tl  -> Some hd