why3shell.ml 10.4 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
  | Information s          -> fprintf fmt "%s@." s
  | Task_Monitor (_t, _s, _r) -> () (* TODO do we want to print something for this? *)
112
  | Parse_Or_Type_Error s  -> fprintf fmt "%s@." s
Sylvain Dailler's avatar
Sylvain Dailler committed
113 114
  | Error s                ->
      fprintf fmt "%s@." s
Sylvain Dailler's avatar
Sylvain Dailler committed
115
  | Open_File_Error s -> fprintf fmt "%s@." s
Sylvain Dailler's avatar
Sylvain Dailler committed
116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133

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
134
  mutable node_proved: bool;
135 136
  mutable children_nodes: node_ID list;
  mutable node_detached: bool
Sylvain Dailler's avatar
Sylvain Dailler committed
137 138 139 140 141 142 143 144 145 146 147 148 149
  }

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
150
  node_proved = false;
151 152
  children_nodes = [];
  node_detached = false
Sylvain Dailler's avatar
Sylvain Dailler committed
153 154 155 156
}

open Stdlib
open Format
157

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

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

186
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
187
  if t = NRoot then () else
Sylvain Dailler's avatar
Sylvain Dailler committed
188 189 190
  let new_node = {
    node_ID = n;
    node_parent = parent;
Sylvain Dailler's avatar
Sylvain Dailler committed
191
    node_name = name;
Sylvain Dailler's avatar
Sylvain Dailler committed
192 193 194 195
    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
196
    node_proved = false;
197 198
    children_nodes = [];
    node_detached = detached
Sylvain Dailler's avatar
Sylvain Dailler committed
199 200 201 202 203 204 205 206 207
  } 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

208
let change_node fmt (n: node_ID) (u: update_info) =
Sylvain Dailler's avatar
Sylvain Dailler committed
209 210
  try
    let node = Hnode.find nodes n in
Sylvain Dailler's avatar
Sylvain Dailler committed
211 212 213 214 215 216
    (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
217 218 219 220 221
  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
222
  | NProofAttempt -> true
223 224
  | _ -> false

Sylvain Dailler's avatar
Sylvain Dailler committed
225 226 227 228 229
let treat_notification fmt n =
  fprintf fmt "Treat notifications@.";
  match n with
  | Node_change (id, info)        ->
    change_node fmt id info
230 231
  | New_node (id, pid, typ, name, detached) ->
    add_new_node fmt id pid typ name detached
Sylvain Dailler's avatar
Sylvain Dailler committed
232 233
  | Remove _id                    -> (* TODO *)
    fprintf fmt "got a Remove notification not yet supported@."
Sylvain Dailler's avatar
Sylvain Dailler committed
234
  | Initialized _g_info           ->
Sylvain Dailler's avatar
Sylvain Dailler committed
235 236 237 238 239 240 241
    (* 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@."
242
  | File_contents _ -> assert false (* TODO *)
Sylvain Dailler's avatar
Sylvain Dailler committed
243 244 245 246 247 248 249 250 251 252 253 254 255 256
  | 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
257

258 259 260
(* _____________________________________________________________________ *)
(* -------------------- printing --------------------------------------- *)

Sylvain Dailler's avatar
Sylvain Dailler committed
261 262 263 264 265 266 267 268 269 270 271 272
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
273
  let current_goal =
Sylvain Dailler's avatar
Sylvain Dailler committed
274
    goal_id = !cur_id
275 276 277
  in
  if current_goal then
    fprintf fmt "**";
Sylvain Dailler's avatar
Sylvain Dailler committed
278
  if goal.node_proved then
279
    fprintf fmt "P";
Sylvain Dailler's avatar
Sylvain Dailler committed
280 281 282 283
  let proof_attempts, transformations =
    List.partition (fun n -> let node = Hnode.find nodes n in
      node.node_type = SProofAttempt) goal.children_nodes
  in
284 285

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

  if current_goal then
293
    fprintf fmt " **"
294

Sylvain Dailler's avatar
Sylvain Dailler committed
295 296 297 298 299 300 301
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
302
  if trans.node_proved then
Clément Fumex's avatar
Clément Fumex committed
303
    fprintf fmt "P";
Sylvain Dailler's avatar
Sylvain Dailler committed
304 305 306
  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
307

Sylvain Dailler's avatar
Sylvain Dailler committed
308 309
let print_theory fmt th_id : unit =
  let th = Hnode.find nodes th_id in
Sylvain Dailler's avatar
Sylvain Dailler committed
310
  if th.node_proved then
Clément Fumex's avatar
Clément Fumex committed
311
    fprintf fmt "P";
Sylvain Dailler's avatar
Sylvain Dailler committed
312 313
  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
314

Sylvain Dailler's avatar
Sylvain Dailler committed
315 316 317 318 319
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
320

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

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

Sylvain Dailler's avatar
Sylvain Dailler committed
328 329 330
(******************)
(*    actions     *)
(******************)
331

Sylvain Dailler's avatar
Sylvain Dailler committed
332 333 334
let interp _chout fmt cmd =
  (* TODO dont use Str. *)
  let l = Str.split (Str.regexp " ") cmd in
335
  begin
Sylvain Dailler's avatar
Sylvain Dailler committed
336 337
    match l with
    | ["goto"; n] when int_of_string n < !max_ID ->
Sylvain Dailler's avatar
Sylvain Dailler committed
338
        cur_id := int_of_string n; send_request (Get_task !cur_id); print_session fmt
339
    | _ ->
Sylvain Dailler's avatar
Sylvain Dailler committed
340 341 342
        begin
          match cmd with
          | "ng" -> cur_id := (!cur_id + 1) mod !max_ID; print_session fmt
Sylvain Dailler's avatar
Sylvain Dailler committed
343
          | "g" -> send_request (Get_task !cur_id)
Sylvain Dailler's avatar
Sylvain Dailler committed
344
          | "p" -> print_session fmt
Sylvain Dailler's avatar
Sylvain Dailler committed
345
          | _ -> send_request (Command_req (!cur_id, cmd))
Sylvain Dailler's avatar
Sylvain Dailler committed
346 347
        end
  end;
Sylvain Dailler's avatar
Sylvain Dailler committed
348 349 350
  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
351 352

let () =
Sylvain Dailler's avatar
Sylvain Dailler committed
353
  printf "Welcome to Why3 shell. Type 'help' for help.@.";
354
  let chout = open_out "why3shell.out" in
Sylvain Dailler's avatar
Sylvain Dailler committed
355
  let fmt = formatter_of_out_channel chout in
Sylvain Dailler's avatar
Sylvain Dailler committed
356 357
  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
358 359 360 361
  Unix_scheduler.timeout ~ms:100
    (fun () -> List.iter
        (fun n -> treat_notification fmt n) (get_notified ()); true);
  Unix_scheduler.main_loop (interp chout fmt)