server_utils.ml 15 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12
let debug = Debug.register_flag ~desc:"ITP server" "itp_server"
MARCHE Claude's avatar
MARCHE Claude committed
13

14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
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
  (* The remaining files in [files] are going to be open *)
  let dir =
    if Sys.file_exists first then
      if Sys.is_directory first then
        (* first is a directory *)
        first
      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
          Queue.push first files; (* we need to open [first] *)
          d
        else
          invalid_arg ("'" ^ first ^ "' is not a directory")
40
    else
41 42 43 44
      (* first does not exists *)
      if has_extension first then
        invalid_arg ("file not found: " ^ first)
      else first
45
  in
46 47 48 49 50 51
  if not (Sys.file_exists dir) then
    begin
      if allow_mkdir then Unix.mkdir dir 0o777 else
        invalid_arg ("session directory '" ^ dir ^ "' not found")
    end;
  dir
Sylvain Dailler's avatar
Sylvain Dailler committed
52 53


54 55


Sylvain Dailler's avatar
Sylvain Dailler committed
56 57 58 59
(******************************)
(* Creation of the controller *)
(******************************)

60 61 62
(* [cont_from_session]: returns an option to a boolean which returns None in
   case of failure, true if nothing is left to do and false if sessions was
   loaded but [f] should still be added to the session as a file. *)
63
(*
64 65 66 67
let cont_from_session ~notify cont f : bool option =
  (* If a file is given, find the corresponding directory *)
  let dir = try (Filename.chop_extension f) with
  | Invalid_argument _ -> f in
Sylvain Dailler's avatar
Sylvain Dailler committed
68 69 70
  (* create project directory if needed *)
  if Sys.file_exists dir then
    begin
71 72 73 74 75 76 77
      (* Case of user giving a file that gets chopped to an other file *)
      if not (Sys.is_directory dir) then
        begin
          let s = "Not a directory: " ^ dir in
          Format.eprintf "%s@." s;
          exit 1
        end
Sylvain Dailler's avatar
Sylvain Dailler committed
78 79 80
    end
  else
    begin
MARCHE Claude's avatar
MARCHE Claude committed
81
      Format.eprintf "[session server info] '%s' does not exist. \
Sylvain Dailler's avatar
Sylvain Dailler committed
82 83 84 85 86
               Creating directory of that name for the project@." dir;
      Unix.mkdir dir 0o777
    end;
  (* we load the session *)
  let ses,use_shapes = load_session dir in
MARCHE Claude's avatar
MARCHE Claude committed
87
  Format.eprintf "[session server info] using shapes: %b@." use_shapes;
88 89
  (* temporary, this should not be donne like this ! *)
  Controller_itp.set_session cont ses;
90
  (* update the session *)
91 92 93 94 95 96 97 98 99 100 101 102 103
  try (Controller_itp.reload_files cont ~use_shapes;
    (* Check if the initial file given was a file or not. If it was, we return
       that it should be added to the session.  *)
    if Sys.file_exists f && not (Sys.is_directory f) then
      Some false
    else
      Some true) with
  | e ->
    begin
      let s = Format.asprintf "%a@." Exn_printer.exn_printer e in
      notify (Message (Parse_Or_Type_Error s));
      None
    end
104
*)
Sylvain Dailler's avatar
Sylvain Dailler committed
105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123



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

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

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

let list_transforms () =
    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 ()))

let list_transforms_query _cont _args =
  let l = list_transforms () in
  let print_trans_desc fmt (x,r) =
MARCHE Claude's avatar
MARCHE Claude committed
124
    Format.fprintf fmt "@[<hov 2>%s@\n@[<hov>%a@]@]" x Pp.formatted r
Sylvain Dailler's avatar
Sylvain Dailler committed
125 126 127 128 129 130 131 132 133 134 135 136 137 138 139
  in
  Pp.string_of (Pp.print_list Pp.newline2 print_trans_desc)
    (List.sort sort_pair l)

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


140 141 142 143 144
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
145 146 147 148 149 150 151 152

(* 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*)
153
  let km = tables.Trans.known_map in
154
  let id = try Args_wrapper.find_symbol s tables with
Sylvain Dailler's avatar
Sylvain Dailler committed
155 156
  | Not_found -> raise (Undefined_id s) in
  let d =
157
    try Ident.Mid.find (symbol_name id) km with
Sylvain Dailler's avatar
Sylvain Dailler committed
158 159 160 161
    | Not_found -> raise Not_found (* Should not happen *)
  in
  Pp.string_of (Why3printer.print_decl tables) d

162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200


(* 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) =
  List.exists (fun (_,t) -> occurs_in_term id t) clauses

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)

let do_search km idl =
  Ident.Mid.fold
    (fun _ d acc ->
     if List.for_all (occurs_in_decl d) idl then Decl.Sdecl.add d acc else acc) km Decl.Sdecl.empty

Sylvain Dailler's avatar
Sylvain Dailler committed
201
let search s tables =
202
  let ids = List.rev_map
203 204 205
              (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
206 207 208 209 210 211 212 213 214 215
  in
  let l = do_search tables.Trans.known_map ids in
  if Decl.Sdecl.is_empty l then
       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
    else let l = Decl.Sdecl.elements l in
         Pp.string_of (Pp.print_list Pp.newline2 (Why3printer.print_decl tables)) l
216 217 218 219 220

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
221 222 223

let search_id _cont task args =
  match args with
224 225
  | [] -> raise Number_of_arguments
  | _ -> search args task
Sylvain Dailler's avatar
Sylvain Dailler committed
226 227 228

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

let help_on_queries fmt commands =
232
  let l = Stdlib.Hstr.fold (fun c (h,_) acc -> (c,h)::acc) commands [] in
Sylvain Dailler's avatar
Sylvain Dailler committed
233
  let l = List.sort sort_pair l in
MARCHE Claude's avatar
MARCHE Claude committed
234
  let p fmt (c,help) = Format.fprintf fmt "%20s : %s" c help in
Sylvain Dailler's avatar
Sylvain Dailler committed
235 236 237 238 239 240 241 242 243 244 245 246
  Format.fprintf fmt "%a" (Pp.print_list Pp.newline p) l

let strategies env config loaded_strategies =
  match !loaded_strategies with
    | [] ->
      let strategies = Whyconf.get_strategies config in
      let strategies =
        Stdlib.Mstr.fold_left
          (fun acc _ st ->
            let name = st.Whyconf.strategy_name in
            try
              let code = st.Whyconf.strategy_code in
247
              let code = Strategy_parser.parse env config code in
Sylvain Dailler's avatar
Sylvain Dailler committed
248
              let shortcut = st.Whyconf.strategy_shortcut in
249
              Debug.dprintf debug "[session server info] Strategy '%s' loaded.@." name;
Sylvain Dailler's avatar
Sylvain Dailler committed
250 251
              (name, shortcut, st.Whyconf.strategy_desc, code) :: acc
            with Strategy_parser.SyntaxError msg ->
252
              Debug.dprintf debug
MARCHE Claude's avatar
MARCHE Claude committed
253
                "[session server warning] Loading strategy '%s' failed: %s@." name msg;
Sylvain Dailler's avatar
Sylvain Dailler committed
254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273
              acc)
          []
          strategies
      in
      let strategies = List.rev strategies in
      loaded_strategies := strategies;
      strategies
    | l -> 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
274
    Debug.dprintf debug "Prover corresponding to %s has not been found@." name;
Sylvain Dailler's avatar
Sylvain Dailler committed
275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290
    None
  end else
    Some (snd (Whyconf.Mprover.choose provers))

(* 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 *)
let parse_prover_name config name args :
  (Whyconf.config_prover * Call_provers.resource_limit) option =
  let main = Whyconf.get_main config in
  match (return_prover name config) with
  | None -> None
  | Some prover_config ->
    begin
      if (List.length args > 2) then None else
      match args with
      | [] ->
291 292 293
        let default_limit = Call_provers.{empty_limit with
                                          limit_time = Whyconf.timelimit main;
                                          limit_mem = Whyconf.memlimit main} in
Sylvain Dailler's avatar
Sylvain Dailler committed
294 295 296 297 298
          Some (prover_config, default_limit)
      | [timeout] -> Some (prover_config,
                           Call_provers.{empty_limit with
                                         limit_time = int_of_string timeout})
      | [timeout; oom ] ->
299 300 301
        Some (prover_config, Call_provers.{empty_limit with
                                           limit_time = int_of_string timeout;
                                           limit_mem = int_of_string oom})
Sylvain Dailler's avatar
Sylvain Dailler committed
302 303 304 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
      | _ -> None
    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
Sylvain Dailler's avatar
Sylvain Dailler committed
345
  | Edit         of Whyconf.config_prover
Sylvain Dailler's avatar
Sylvain Dailler committed
346 347 348 349 350
  | Help_message of string
  | Query        of string
  | QError       of string
  | Other        of string * string list

351
let interp_others commands_table config cmd args =
Sylvain Dailler's avatar
Sylvain Dailler committed
352 353
  match parse_prover_name config cmd args with
  | Some (prover_config, limit) ->
Sylvain Dailler's avatar
Sylvain Dailler committed
354 355 356 357
      if prover_config.Whyconf.interactive then
        Edit (prover_config)
      else
        Prove (prover_config, limit)
Sylvain Dailler's avatar
Sylvain Dailler committed
358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375
  | None ->
      match cmd with
      | "auto" ->
          let s =
            match args with
            | "2"::_ -> "2"
            | _ -> "1"
          in
          Strategies s
      | "help" ->
          let text = Pp.sprintf
                          "Please type a command among the following (automatic completion available)@\n\
                           @\n\
                           @ <transformation name> [arguments]@\n\
                           @ <prover name> [<time limit> [<mem limit>]]@\n\
                           @ <query> [arguments]@\n\
                           @ auto [auto level]@\n\
                           @\n\
376
                           Available queries are:@\n@[%a@]" help_on_queries commands_table
Sylvain Dailler's avatar
Sylvain Dailler committed
377 378 379 380 381
          in
          Help_message text
      | _ ->
          Other (cmd, args)

382
let interp commands_table config cont id s =
Sylvain Dailler's avatar
Sylvain Dailler committed
383 384
  let cmd,args = split_args s in
  try
385
    let (_,f) = Stdlib.Hstr.find commands_table cmd in
Sylvain Dailler's avatar
Sylvain Dailler committed
386 387 388 389
    match f,id with
    | Qnotask f, _ -> Query (f cont args)
    | Qtask _, None -> QError "please select a goal first"
    | Qtask f, Some id ->
390
       let table = match Session_itp.get_table cont.Controller_itp.controller_session id with
391
       | None -> raise (Trans.Bad_name_table "Server_utils.interp")
392 393
       | Some table -> table in
       let s = try Query (f cont table args) with
Sylvain Dailler's avatar
Sylvain Dailler committed
394 395 396 397 398
       | Undefined_id s -> QError ("No existing id corresponding to " ^ s)
       | Number_of_arguments -> QError "Bad number of arguments"
       in s
  with Not_found ->
    try
399 400 401 402 403
      if id = None then
        QError ("Please select a valid node id")
      else
        let t = Trans.lookup_trans cont.Controller_itp.controller_env cmd in
        Transform (cmd,t,args)
Sylvain Dailler's avatar
Sylvain Dailler committed
404
    with Trans.UnknownTrans _ ->
405
      interp_others commands_table config cmd args
406 407 408 409 410 411 412 413 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


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

let get_first_unproven_goal_around
    ~proved ~children ~get_parent ~is_goal ~is_pa node =
  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
  match List.rev (look_around node) with
  | [] -> None
  | hd :: _tl  -> Some hd