Une nouvelle version du portail de gestion des comptes externes sera mise en production lundi 09 août. Elle permettra d'allonger la validité d'un compte externe jusqu'à 3 ans. Pour plus de détails sur cette version consulter : https://doc-si.inria.fr/x/FCeS

why3shell.ml 10.3 KB
Newer Older
Sylvain Dailler's avatar
Sylvain Dailler committed
1 2 3 4 5 6 7 8
(* TODO
  - detached theories
  - obsolete
  - update proof attempt
*)
open Why3
open Unix_scheduler
open Format
9
open Itp_communication
Sylvain Dailler's avatar
Sylvain Dailler committed
10 11 12 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 40 41
open Itp_server

(*************************)
(* Protocol of the shell *)
(*************************)
module Protocol_shell = struct

  let debug_proto = Debug.register_flag "shell_proto"
      ~desc:"Print@ debugging@ messages@ about@ Why3Ide@ protocol@"

  let print_request_debug r =
    Debug.dprintf debug_proto "[request]";
    Debug.dprintf debug_proto "%a" print_request r

  let print_msg_debug m =
    Debug.dprintf debug_proto "[message]";
    Debug.dprintf debug_proto "%a@." print_msg m

  let print_notify_debug n =
    Debug.dprintf debug_proto "[notification]";
    Debug.dprintf debug_proto "%a@." print_notify n

  let list_requests: ide_request list ref = ref []

  let get_requests () =
    if List.length !list_requests > 0 then
      Debug.dprintf debug_proto "get requests@.";
    let l = List.rev !list_requests in
    list_requests := [];
    l

  let send_request r =
Sylvain Dailler's avatar
Sylvain Dailler committed
42
    print_request_debug r;
Sylvain Dailler's avatar
Sylvain Dailler committed
43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
    Debug.dprintf debug_proto "@.";
    list_requests := r :: !list_requests

  let notification_list: notification list ref = ref []

  let notify n =
    print_notify_debug n;
    Debug.dprintf debug_proto "@.";
    notification_list := n :: !notification_list

  let get_notified () =
    if List.length !notification_list > 0 then
      Debug.dprintf debug_proto "get notified@.";
    let l = List.rev !notification_list in
    notification_list := [];
    l
MARCHE Claude's avatar
MARCHE Claude committed
59 60 61

end

Sylvain Dailler's avatar
Sylvain Dailler committed
62 63 64 65
let get_notified = Protocol_shell.get_notified

let send_request = Protocol_shell.send_request

MARCHE Claude's avatar
MARCHE Claude committed
66 67 68 69
(************************)
(* parsing command line *)
(************************)

70
(* files of the current task *)
MARCHE Claude's avatar
MARCHE Claude committed
71 72
let files = Queue.create ()

73
let spec = Arg.align []
MARCHE Claude's avatar
MARCHE Claude committed
74

75
(* --help *)
MARCHE Claude's avatar
MARCHE Claude committed
76
let usage_str = Format.sprintf
77
  "Usage: %s [options] [ <file.xml> | <f1.why> <f2.mlw> ...]"
MARCHE Claude's avatar
MARCHE Claude committed
78 79
  (Filename.basename Sys.argv.(0))

Sylvain Dailler's avatar
Sylvain Dailler committed
80
(* Parse files *)
Sylvain Dailler's avatar
Sylvain Dailler committed
81 82 83
let config, base_config, env =
  let config, base_config, env =
    Whyconf.Args.initialize spec (fun f -> Queue.add f files) usage_str in
Sylvain Dailler's avatar
Sylvain Dailler committed
84
  if Queue.is_empty files then
Sylvain Dailler's avatar
Sylvain Dailler committed
85 86 87 88 89 90 91
    Whyconf.Args.exit_with_usage spec usage_str;
  (config, base_config, env)

module Server = Itp_server.Make (Unix_scheduler) (Protocol_shell)

(* Initialize the server *)
let () = Server.init_server config env
Sylvain Dailler's avatar
Sylvain Dailler committed
92 93 94 95 96 97 98 99 100 101 102 103 104

(*************************)
(* Notification Handling *)
(*************************)

let treat_message_notification fmt msg = match msg with
  (* TODO: do something ! *)
  | Proof_error (_id, s)   -> fprintf fmt "%s@." s
  | Transf_error (_id, s)  -> fprintf fmt "%s@." s
  | Strat_error (_id, s)   -> fprintf fmt "%s@." s
  | Replay_Info s          -> fprintf fmt "%s@." s
  | Query_Info (_id, s)    -> fprintf fmt "%s@." s
  | Query_Error (_id, s)   -> fprintf fmt "%s@." s
Sylvain Dailler's avatar
Sylvain Dailler committed
105 106 107 108 109
  | Help s                 -> fprintf fmt "%s@. Additionally for shell:\n\
goto n -> focuse on n\n\
ng -> next node\n\
g -> print the current task\n\
p -> print the session@." s
Sylvain Dailler's avatar
Sylvain Dailler committed
110 111 112 113
  | Information s          -> fprintf fmt "%s@." s
  | Task_Monitor (_t, _s, _r) -> () (* TODO do we want to print something for this? *)
  | Error s                ->
      fprintf fmt "%s@." s
Sylvain Dailler's avatar
Sylvain Dailler committed
114
  | Open_File_Error s -> fprintf fmt "%s@." s
Sylvain Dailler's avatar
Sylvain Dailler committed
115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132

type shell_node_type =
  | SRoot
  | SFile
  | STheory
  | STransformation
  | SGoal
  | SProofAttempt


type node = {
  node_ID: node_ID;
  node_parent: node_ID;
  node_name: string;
  mutable node_task: string option;
  node_proof: Controller_itp.proof_attempt_status option;
  node_trans_args: string list option;
  node_type: shell_node_type;
Sylvain Dailler's avatar
Sylvain Dailler committed
133
  mutable node_proved: bool;
134 135
  mutable children_nodes: node_ID list;
  mutable node_detached: bool
Sylvain Dailler's avatar
Sylvain Dailler committed
136 137 138 139 140 141 142 143 144 145 146 147 148
  }

let root_node_ID = root_node
let max_ID = ref 1

let root_node = {
  node_ID = root_node_ID;
  node_parent = root_node_ID;
  node_name = "root";
  node_task = None;
  node_proof = None;
  node_trans_args = None;
  node_type = SRoot;
Sylvain Dailler's avatar
Sylvain Dailler committed
149
  node_proved = false;
150 151
  children_nodes = [];
  node_detached = false
Sylvain Dailler's avatar
Sylvain Dailler committed
152 153 154 155
}

open Stdlib
open Format
156

Sylvain Dailler's avatar
Sylvain Dailler committed
157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176
module Hnode = Hint
let nodes : node Hnode.t = Hnode.create 17
let () = Hnode.add nodes root_node_ID root_node

(* Current node_ID *)
let cur_id = ref root_node_ID

let print_goal fmt n =
  let node = Hnode.find nodes n in
  match node.node_task with
  | None -> fprintf fmt "No goal@."
  | Some s -> fprintf fmt "Goal is: \n %s@." s

let convert_to_shell_type t =
  match t with
  | NRoot -> SRoot
  | NFile -> SFile
  | NTheory -> STheory
  | NTransformation -> STransformation
  | NGoal -> SGoal
Sylvain Dailler's avatar
Sylvain Dailler committed
177
  | NProofAttempt -> SProofAttempt
Sylvain Dailler's avatar
Sylvain Dailler committed
178 179 180

let return_proof_info (t: node_type) =
  match t with
Sylvain Dailler's avatar
Sylvain Dailler committed
181
  | NProofAttempt ->
Sylvain Dailler's avatar
Sylvain Dailler committed
182 183
    Some Controller_itp.Scheduled
  | _ -> None
184

185
let add_new_node fmt (n: node_ID) (parent: node_ID) (t: node_type) (name: string) (detached: bool) =
Sylvain Dailler's avatar
Sylvain Dailler committed
186
  if t = NRoot then () else
Sylvain Dailler's avatar
Sylvain Dailler committed
187 188 189
  let new_node = {
    node_ID = n;
    node_parent = parent;
Sylvain Dailler's avatar
Sylvain Dailler committed
190
    node_name = name;
Sylvain Dailler's avatar
Sylvain Dailler committed
191 192 193 194
    node_task = None;
    node_proof = return_proof_info t;
    node_trans_args = None; (* TODO *)
    node_type = convert_to_shell_type t;
Sylvain Dailler's avatar
Sylvain Dailler committed
195
    node_proved = false;
196 197
    children_nodes = [];
    node_detached = detached
Sylvain Dailler's avatar
Sylvain Dailler committed
198 199 200 201 202 203 204 205 206
  } in
  try
    let parent = Hnode.find nodes parent in
    parent.children_nodes <- parent.children_nodes @ [n];
    Hnode.add nodes n new_node;
    max_ID := !max_ID + 1
  with
    Not_found -> fprintf fmt "Could not find node %d@." parent

207
let change_node fmt (n: node_ID) (u: update_info) =
Sylvain Dailler's avatar
Sylvain Dailler committed
208 209
  try
    let node = Hnode.find nodes n in
Sylvain Dailler's avatar
Sylvain Dailler committed
210 211 212 213 214 215
    (match u with
    | Proved b ->
        node.node_proved <- b
    | Proof_status_change (_pas, _b, _rl) when node.node_type = SProofAttempt ->
        fprintf fmt "Not yet supported@." (* TODO *)
    | _ -> fprintf fmt "Not yet supported@.") (* TODO *)
Sylvain Dailler's avatar
Sylvain Dailler committed
216 217 218 219 220
  with
    Not_found -> fprintf fmt "Could not find node %d@." n

let is_proof_attempt node_type =
  match node_type with
Sylvain Dailler's avatar
Sylvain Dailler committed
221
  | NProofAttempt -> true
222 223
  | _ -> false

Sylvain Dailler's avatar
Sylvain Dailler committed
224 225 226 227 228
let treat_notification fmt n =
  fprintf fmt "Treat notifications@.";
  match n with
  | Node_change (id, info)        ->
    change_node fmt id info
229 230
  | New_node (id, pid, typ, name, detached) ->
    add_new_node fmt id pid typ name detached
Sylvain Dailler's avatar
Sylvain Dailler committed
231 232
  | Remove _id                    -> (* TODO *)
    fprintf fmt "got a Remove notification not yet supported@."
Sylvain Dailler's avatar
Sylvain Dailler committed
233
  | Initialized _g_info           ->
Sylvain Dailler's avatar
Sylvain Dailler committed
234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254
    (* TODO *)
    fprintf fmt "Initialized@."
  | Saved                         -> (* TODO *)
    fprintf fmt "got a Saved notification not yet supported@."
  | Message (msg)                 -> treat_message_notification fmt msg
  | Dead _s                       -> (* TODO *)
    fprintf fmt "got a Dead notification not yet supported@."
  | Task (id, s)                  ->
    try
      let node = Hnode.find nodes id in
      node.node_task <- Some s;
      if id = !cur_id then print_goal fmt !cur_id
    with
      Not_found -> fprintf fmt "Could not find node %d@." id

let get_result pa =
  match pa with
  | None -> None
  | Some pr -> match pr with
    | Controller_itp.Done pr -> Some pr
    | _ -> None
255

256 257 258
(* _____________________________________________________________________ *)
(* -------------------- printing --------------------------------------- *)

Sylvain Dailler's avatar
Sylvain Dailler committed
259 260 261 262 263 264 265 266 267 268 269 270
let print_proof_attempt fmt pa_id =
  let pa = Hnode.find nodes pa_id in
  match pa.node_proof with
  | None -> fprintf fmt "%s" pa.node_name
  | Some _pr ->
    fprintf fmt "%s %a"
      pa.node_name (Pp.print_option Call_provers.print_prover_result) (get_result pa.node_proof)

let rec print_proof_node (fmt: Format.formatter) goal_id =
  let goal = Hnode.find nodes goal_id in
  let parent = Hnode.find nodes goal.node_parent in
  let parent_name = parent.node_name in
271
  let current_goal =
Sylvain Dailler's avatar
Sylvain Dailler committed
272
    goal_id = !cur_id
273 274 275
  in
  if current_goal then
    fprintf fmt "**";
Sylvain Dailler's avatar
Sylvain Dailler committed
276
  if goal.node_proved then
277
    fprintf fmt "P";
Sylvain Dailler's avatar
Sylvain Dailler committed
278 279 280 281
  let proof_attempts, transformations =
    List.partition (fun n -> let node = Hnode.find nodes n in
      node.node_type = SProofAttempt) goal.children_nodes
  in
282 283

  fprintf fmt
Sylvain Dailler's avatar
Sylvain Dailler committed
284 285
    "@[<hv 2>{ Goal=%s, id = %d;@ parent=%s;@ @[<hv 1>[%a]@]@ @[<hv 1>[%a]@] }@]"
    goal.node_name goal_id parent_name
286
    (Pp.print_list Pp.semi print_proof_attempt)
Sylvain Dailler's avatar
Sylvain Dailler committed
287 288
    proof_attempts
    (Pp.print_list Pp.semi print_trans_node) transformations;
289 290

  if current_goal then
291
    fprintf fmt " **"
292

Sylvain Dailler's avatar
Sylvain Dailler committed
293 294 295 296 297 298 299
and print_trans_node fmt id =
  let trans = Hnode.find nodes id in
  let name = trans.node_name in
  let l = trans.children_nodes in
  let args = trans.node_trans_args in
  let parent = Hnode.find nodes trans.node_parent in
  let parent_name = parent.node_name in
Sylvain Dailler's avatar
Sylvain Dailler committed
300
  if trans.node_proved then
Clément Fumex's avatar
Clément Fumex committed
301
    fprintf fmt "P";
Sylvain Dailler's avatar
Sylvain Dailler committed
302 303 304
  fprintf fmt "@[<hv 2>{ Trans=%s;@ args=%a;@ parent=%s;@ [%a] }@]" name
    (Pp.print_option (Pp.print_list Pp.semi pp_print_string)) args parent_name
    (Pp.print_list Pp.semi print_proof_node) l
305

Sylvain Dailler's avatar
Sylvain Dailler committed
306 307
let print_theory fmt th_id : unit =
  let th = Hnode.find nodes th_id in
Sylvain Dailler's avatar
Sylvain Dailler committed
308
  if th.node_proved then
Clément Fumex's avatar
Clément Fumex committed
309
    fprintf fmt "P";
Sylvain Dailler's avatar
Sylvain Dailler committed
310 311
  fprintf fmt "@[<hv 1> Theory %s, id: %d;@ [%a]@]" th.node_name th_id
    (Pp.print_list Pp.semi print_proof_node) th.children_nodes
312

Sylvain Dailler's avatar
Sylvain Dailler committed
313 314 315 316 317
let print_file fmt file_ID =
  let file = Hnode.find nodes file_ID in
  assert (file.node_type = SFile);
  fprintf fmt "@[<hv 1> File %s, id %d;@ [%a];@]" file.node_name file.node_ID
    (Pp.print_list Pp.semi print_theory) file.children_nodes
318

Sylvain Dailler's avatar
Sylvain Dailler committed
319 320
let print_s fmt files =
  fprintf fmt "@[%a@]" (Pp.print_list Pp.semi print_file) files
321

Sylvain Dailler's avatar
Sylvain Dailler committed
322 323 324
let print_session fmt =
  let l = root_node.children_nodes in
  fprintf fmt "root %a@." print_s l
325

Sylvain Dailler's avatar
Sylvain Dailler committed
326 327 328
(******************)
(*    actions     *)
(******************)
329

Sylvain Dailler's avatar
Sylvain Dailler committed
330 331 332
let interp _chout fmt cmd =
  (* TODO dont use Str. *)
  let l = Str.split (Str.regexp " ") cmd in
333
  begin
Sylvain Dailler's avatar
Sylvain Dailler committed
334 335
    match l with
    | ["goto"; n] when int_of_string n < !max_ID ->
Sylvain Dailler's avatar
Sylvain Dailler committed
336
        cur_id := int_of_string n; send_request (Get_task !cur_id); print_session fmt
337
    | _ ->
Sylvain Dailler's avatar
Sylvain Dailler committed
338 339 340
        begin
          match cmd with
          | "ng" -> cur_id := (!cur_id + 1) mod !max_ID; print_session fmt
Sylvain Dailler's avatar
Sylvain Dailler committed
341
          | "g" -> send_request (Get_task !cur_id)
Sylvain Dailler's avatar
Sylvain Dailler committed
342
          | "p" -> print_session fmt
Sylvain Dailler's avatar
Sylvain Dailler committed
343
          | _ -> send_request (Command_req (!cur_id, cmd))
Sylvain Dailler's avatar
Sylvain Dailler committed
344 345
        end
  end;
Sylvain Dailler's avatar
Sylvain Dailler committed
346 347 348
  let node = Hnode.find nodes !cur_id in
  if node.node_type = SGoal then
    print_goal fmt !cur_id
MARCHE Claude's avatar
MARCHE Claude committed
349 350

let () =
Sylvain Dailler's avatar
Sylvain Dailler committed
351
  printf "Welcome to Why3 shell. Type 'help' for help.@.";
352
  let chout = open_out "why3shell.out" in
Sylvain Dailler's avatar
Sylvain Dailler committed
353
  let fmt = formatter_of_out_channel chout in
Sylvain Dailler's avatar
Sylvain Dailler committed
354 355
  let f = Queue.pop files in send_request (Open_session_req f);
  (*Queue.iter (fun f -> send_request (Add_file_req f)) files;*)
Sylvain Dailler's avatar
Sylvain Dailler committed
356 357 358 359
  Unix_scheduler.timeout ~ms:100
    (fun () -> List.iter
        (fun n -> treat_notification fmt n) (get_notified ()); true);
  Unix_scheduler.main_loop (interp chout fmt)