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).

why3shell.ml 10 KB
Newer Older
Sylvain Dailler's avatar
Sylvain Dailler committed
1 2 3 4 5 6 7 8 9 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 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
(* TODO
  - detached theories
  - obsolete
  - update proof attempt
*)

open Why3
open Unix_scheduler
open Format
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 =
    print_request_debug (fst r);
    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
60 61 62

end

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

let send_request = Protocol_shell.send_request

module Server = Itp_server.Make (Unix_scheduler) (Protocol_shell)
MARCHE Claude's avatar
MARCHE Claude committed
68

MARCHE Claude's avatar
MARCHE Claude committed
69 70 71 72
(************************)
(* parsing command line *)
(************************)

73
(* files of the current task *)
MARCHE Claude's avatar
MARCHE Claude committed
74 75
let files = Queue.create ()

76
let spec = Arg.align []
MARCHE Claude's avatar
MARCHE Claude committed
77

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

Sylvain Dailler's avatar
Sylvain Dailler committed
83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99
(* Parse files *)
let () = Whyconf.Args.parse spec (fun f -> Queue.add f files) usage_str;
  if Queue.is_empty files then
    Whyconf.Args.exit_with_usage spec usage_str

(*************************)
(* 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
100 101 102 103 104
  | 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
105 106 107 108 109 110 111 112 113 114 115 116 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
  | 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

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


(* TODO will evolve *)
type node_info = { proved: bool }

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;
  mutable node_info: node_info;
  mutable children_nodes: node_ID list
  }

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;
  node_info = {proved = false};
  children_nodes = []
}

open Stdlib
open Format
151

Sylvain Dailler's avatar
Sylvain Dailler committed
152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
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
  | NProofAttempt _ -> SProofAttempt

let return_proof_info (t: node_type) =
  match t with
  | NProofAttempt (_pr, _obs) ->
    Some Controller_itp.Scheduled
  | _ -> None
180

Sylvain Dailler's avatar
Sylvain Dailler committed
181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210
let add_new_node fmt (n: node_ID) (parent: node_ID) (t: node_type) (i: Itp_server.node_info) =
  let new_node = {
    node_ID = n;
    node_parent = parent;
    node_name = i.Itp_server.name;
    node_task = None;
    node_proof = return_proof_info t;
    node_trans_args = None; (* TODO *)
    node_type = convert_to_shell_type t;
    node_info = {proved = i.Itp_server.proved};
    children_nodes = []
  } 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

let change_node fmt (n: node_ID) (i: Itp_server.node_info) =
  try
    let node = Hnode.find nodes n in
    node.node_info <- { proved = i.Itp_server.proved }
  with
    Not_found -> fprintf fmt "Could not find node %d@." n

let is_proof_attempt node_type =
  match node_type with
  | NProofAttempt _ -> true
211 212
  | _ -> false

Sylvain Dailler's avatar
Sylvain Dailler committed
213 214 215 216 217 218 219 220 221 222 223 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
  | New_node (id, pid, typ, info) ->
    add_new_node fmt id pid typ info
  | Remove _id                    -> (* TODO *)
    fprintf fmt "got a Remove notification not yet supported@."
  | Initialized _g_info            ->
    (* TODO *)
    fprintf fmt "Initialized@."
  | Saved                         -> (* TODO *)
    fprintf fmt "got a Saved notification not yet supported@."
  | Message (msg)                 -> treat_message_notification fmt msg
  | Proof_update (_id, _pa)         -> (* TODO *)
Sylvain Dailler's avatar
Sylvain Dailler committed
229
    fprintf fmt "got a Update notification not yet supported@."
Sylvain Dailler's avatar
Sylvain Dailler committed
230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245
  | 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
246

247 248 249
(* _____________________________________________________________________ *)
(* -------------------- printing --------------------------------------- *)

Sylvain Dailler's avatar
Sylvain Dailler committed
250 251 252 253 254 255 256 257 258 259 260 261
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
262
  let current_goal =
Sylvain Dailler's avatar
Sylvain Dailler committed
263
    goal_id = !cur_id
264 265 266
  in
  if current_goal then
    fprintf fmt "**";
Sylvain Dailler's avatar
Sylvain Dailler committed
267
  if goal.node_info.proved then
268
    fprintf fmt "P";
Sylvain Dailler's avatar
Sylvain Dailler committed
269 270 271 272
  let proof_attempts, transformations =
    List.partition (fun n -> let node = Hnode.find nodes n in
      node.node_type = SProofAttempt) goal.children_nodes
  in
273 274

  fprintf fmt
Sylvain Dailler's avatar
Sylvain Dailler committed
275 276
    "@[<hv 2>{ Goal=%s, id = %d;@ parent=%s;@ @[<hv 1>[%a]@]@ @[<hv 1>[%a]@] }@]"
    goal.node_name goal_id parent_name
277
    (Pp.print_list Pp.semi print_proof_attempt)
Sylvain Dailler's avatar
Sylvain Dailler committed
278 279
    proof_attempts
    (Pp.print_list Pp.semi print_trans_node) transformations;
280 281

  if current_goal then
282
    fprintf fmt " **"
283

Sylvain Dailler's avatar
Sylvain Dailler committed
284 285 286 287 288 289 290 291
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
  if trans.node_info.proved then
Clément Fumex's avatar
Clément Fumex committed
292
    fprintf fmt "P";
Sylvain Dailler's avatar
Sylvain Dailler committed
293 294 295
  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
296

Sylvain Dailler's avatar
Sylvain Dailler committed
297 298 299
let print_theory fmt th_id : unit =
  let th = Hnode.find nodes th_id in
  if th.node_info.proved then
Clément Fumex's avatar
Clément Fumex committed
300
    fprintf fmt "P";
Sylvain Dailler's avatar
Sylvain Dailler committed
301 302
  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
303

Sylvain Dailler's avatar
Sylvain Dailler committed
304 305 306 307 308
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
309

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

Sylvain Dailler's avatar
Sylvain Dailler committed
313 314 315
let print_session fmt =
  let l = root_node.children_nodes in
  fprintf fmt "root %a@." print_s l
316

Sylvain Dailler's avatar
Sylvain Dailler committed
317 318 319
(******************)
(*    actions     *)
(******************)
320

Sylvain Dailler's avatar
Sylvain Dailler committed
321 322 323
let interp _chout fmt cmd =
  (* TODO dont use Str. *)
  let l = Str.split (Str.regexp " ") cmd in
324
  begin
Sylvain Dailler's avatar
Sylvain Dailler committed
325 326 327
    match l with
    | ["goto"; n] when int_of_string n < !max_ID ->
        cur_id := int_of_string n; send_request (Get_task, !cur_id); print_session fmt
328
    | _ ->
Sylvain Dailler's avatar
Sylvain Dailler committed
329 330 331 332
        begin
          match cmd with
          | "ng" -> cur_id := (!cur_id + 1) mod !max_ID; print_session fmt
          | "g" -> send_request (Get_task, !cur_id)
Sylvain Dailler's avatar
Sylvain Dailler committed
333
          | "p" -> print_session fmt
Sylvain Dailler's avatar
Sylvain Dailler committed
334 335 336
          | _ -> send_request (Command_req cmd, !cur_id)
        end
  end;
Sylvain Dailler's avatar
Sylvain Dailler committed
337 338 339
  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
340 341

let () =
Sylvain Dailler's avatar
Sylvain Dailler committed
342
  printf "Welcome to Why3 shell. Type 'help' for help.@.";
343
  let chout = open_out "why3shell.out" in
Sylvain Dailler's avatar
Sylvain Dailler committed
344 345 346 347 348 349
  let fmt = formatter_of_out_channel chout in
  Queue.iter (fun f -> send_request (Open_req f, Itp_server.root_node)) files;
  Unix_scheduler.timeout ~ms:100
    (fun () -> List.iter
        (fun n -> treat_notification fmt n) (get_notified ()); true);
  Unix_scheduler.main_loop (interp chout fmt)