option to select with or without intros in printing why3 tasks

this required to add an extra boolean argument to the Get_task request

src/core/printer.ml

@@ -36,6 +36,7 @@ type printer_mapping = {
 
 type printer_args = {
   name_table : names_table option;
+  do_intros  : bool;
   env        : Env.env;
   prelude    : prelude;
   th_prelude : prelude_map;

src/core/printer.mli

@@ -37,6 +37,7 @@ type printer_mapping = {
 
 type printer_args = {
   name_table : names_table option;
+  do_intros  : bool;
   env        : Env.env;
   prelude    : prelude;
   th_prelude : prelude_map;

src/driver/driver.ml

@@ -301,13 +301,14 @@ let prepare_task ~cntexample drv task =
   let task = update_task drv task in
   List.fold_left apply task transl
 
-let print_task_prepared ?old ?name_table drv fmt task =
+let print_task_prepared ?old ?name_table ?(do_intros=false) drv fmt task =
   let p = match drv.drv_printer with
     | None -> raise NoPrinter
     | Some p -> p
   in
   let printer_args = { Printer.env = drv.drv_env;
       name_table  = name_table;
+      do_intros   = do_intros;
       prelude     = drv.drv_prelude;
       th_prelude  = drv.drv_thprelude;
       blacklist   = drv.drv_blacklist;
@@ -317,9 +318,9 @@ let print_task_prepared ?old ?name_table drv fmt task =
   fprintf fmt "@[%a@]@?" (printer ?old) task;
   printer_args.printer_mapping
 
-let print_task ?old ?(cntexample=false) ?name_table drv fmt task =
+let print_task ?old ?(cntexample=false) ?(do_intros=false) ?name_table drv fmt task =
   let task = prepare_task ~cntexample drv task in
-  let _ = print_task_prepared ?old ?name_table drv fmt task in
+  let _ = print_task_prepared ?old ?name_table ~do_intros drv fmt task in
   ()
 
 let print_theory ?old ?name_table drv fmt th =

src/driver/driver.mli

@@ -46,6 +46,7 @@ val call_on_buffer :
 val print_task :
   ?old       : in_channel ->
   ?cntexample : bool ->
+  ?do_intros  : bool ->
   ?name_table: Task.names_table ->
   driver -> Format.formatter -> Task.task -> unit
 
@@ -70,6 +71,7 @@ val prepare_task : cntexample:bool -> driver -> Task.task -> Task.task
 val print_task_prepared :
   ?old       : in_channel ->
   ?name_table: Task.names_table ->
+  ?do_intros  : bool ->
   driver -> Format.formatter -> Task.task -> Printer.printer_mapping
 
 val prove_task_prepared :

src/ide/why3ide.ml

@@ -1117,7 +1117,8 @@ let on_selected_row r =
       if detached then
         task_view#source_buffer#set_text ""
       else
-        send_request (Get_task id)
+        let b = gconfig.intro_premises in
+        send_request (Get_task(id,b))
     | NProofAttempt ->
       let (pa, _obs, _l) = Hint.find node_id_pa id in
       (match pa with
@@ -1137,7 +1138,9 @@ let on_selected_row r =
           task_view#source_buffer#set_text "Internal failure"
       | Controller_itp.Uninstalled _p ->
           task_view#source_buffer#set_text "Uninstalled")
-    | _ -> send_request (Get_task id)
+    | _ ->
+       let b = gconfig.intro_premises in
+       send_request (Get_task(id,b))
   with
     | Not_found -> task_view#source_buffer#set_text ""
 

src/ide/why3web.ml

@@ -58,7 +58,8 @@ let interp_request args =
           Command_req (int_of_string n, com)
       | _ -> invalid_arg ("Why3web.interp_request '" ^ args ^ "'"))
   | args when Strings.has_prefix "gettask_" args ->
-      Get_task (int_of_string (Strings.remove_prefix "gettask_" args))
+     let b = false (* TODO: allow user to customize printing with intros or not *) in
+     Get_task (int_of_string (Strings.remove_prefix "gettask_" args),b)
   | _ -> invalid_arg ("Why3web.interp_request '" ^ args ^ "'")
 
 let handle_script s args =

src/printer/why3printer.ml

@@ -482,9 +482,11 @@ let rec print_term_intro tables fmt t =
 (* do not forget these local names, they might be used by the itp *)
 (*      List.iter (forget_var tables) vl*)
 
-let print_goal tables fmt d =
+let print_goal tables do_intros fmt d =
    match d.d_node with
-   | Dprop (Pgoal,_pr,f) -> fprintf fmt "@[%a@]" (print_term_intro tables) f
+   | Dprop (Pgoal,_pr,f) ->
+      if do_intros then fprintf fmt "@[%a@]" (print_term_intro tables) f
+      else fprintf fmt "@[%a@]" (print_term tables) f
    | _ -> assert false
 
 let print_sequent args ?old:_ fmt task =
@@ -501,7 +503,7 @@ let print_sequent args ?old:_ fmt task =
       | [] -> assert false
       | [g] ->
          fprintf fmt "----------------------------- Goal ---------------------------@\n@\n";
-         print_goal tables fmt g
+         print_goal tables args.do_intros fmt g
       | d :: r ->
          fprintf fmt "@[%a@]@\n" (print_decl tables) d;
          aux fmt r

src/session/itp_communication.ml

@@ -99,7 +99,7 @@ type ide_request =
   | Add_file_req            of string
   | Set_max_tasks_req       of int
   | Get_file_contents       of string
-  | Get_task                of node_ID
+  | Get_task                of node_ID * bool
   | Focus_req               of node_ID
   | Unfocus_req
   | Remove_subtree          of node_ID

src/session/itp_communication.mli

@@ -105,7 +105,9 @@ type ide_request =
   | Add_file_req            of string
   | Set_max_tasks_req       of int
   | Get_file_contents       of string
-  | Get_task                of node_ID
+  | Get_task                of node_ID * bool
+    (** [Get_task(id,b) requests for the text of the task in node [id], when [b] is true
+  then quantified variables and hypotheses are introduced as local definitions *)
   | Focus_req               of node_ID
   (* Focus on a node. The server only sends info about descendants of this ID *)
   | Unfocus_req

src/session/itp_server.ml

@@ -263,7 +263,7 @@ let print_request fmt r =
   | Set_max_tasks_req i             -> fprintf fmt "set max tasks %i" i
   | Get_file_contents _f            -> fprintf fmt "get file contents"
   | Get_first_unproven_node _nid    -> fprintf fmt "get first unproven node"
-  | Get_task _nid                   -> fprintf fmt "get task"
+  | Get_task(nid,b)                 -> fprintf fmt "get task(%d,%b)" nid b
   | Focus_req _nid                  -> fprintf fmt "focus"
   | Unfocus_req                     -> fprintf fmt "unfocus"
   | Remove_subtree _nid             -> fprintf fmt "remove subtree"
@@ -884,22 +884,21 @@ end
       get_node_proved node_id any in
     iter_the_files send_node root_node
 
-
   (* -- send the task -- *)
-  let task_of_id d id =
+  let task_of_id d id do_intros =
     let task = get_task d.cont.controller_session id in
     let tables = get_table d.cont.controller_session id in
     (* This function also send source locations associated to the task *)
     let loc_color_list = get_locations task in
     Pp.string_of
-      (Driver.print_task ~cntexample:false ?name_table:tables d.task_driver)
+      (Driver.print_task ~cntexample:false ?name_table:tables ~do_intros d.task_driver)
       task, loc_color_list
 
-  let send_task nid =
+  let send_task nid do_intros =
     let d = get_server_data () in
     match any_from_node_ID nid with
     | APn id ->
-       let s, list_loc = task_of_id d id in
+       let s, list_loc = task_of_id d id do_intros in
        P.notify (Task (nid, s, list_loc))
     | ATh t ->
        P.notify (Task (nid, "Theory " ^ (theory_name t).Ident.id_string, []))
@@ -907,7 +906,7 @@ end
        let pa = get_proof_attempt_node  d.cont.controller_session pid in
        let parid = pa.parent in
        let name = Pp.string_of Whyconf.print_prover pa.prover in
-       let s, list_loc = task_of_id d parid in
+       let s, list_loc = task_of_id d parid do_intros in
        P.notify (Task (nid,s ^ "\n====================> Prover: " ^ name ^ "\n", list_loc))
     | AFile f ->
        P.notify (Task (nid, "File " ^ file_name f, []))
@@ -915,7 +914,7 @@ end
        let name = get_transf_name d.cont.controller_session tid in
        let args = get_transf_args d.cont.controller_session tid in
        let parid = get_trans_parent d.cont.controller_session tid in
-       let s, list_loc = task_of_id d parid in
+       let s, list_loc = task_of_id d parid do_intros in
        P.notify (Task (nid, s ^ "\n====================> Transformation: " ^ String.concat " " (name :: args) ^ "\n", list_loc))
 
   (* -------------------- *)
@@ -1289,7 +1288,7 @@ end
     | Mark_obsolete_req n          -> mark_obsolete n
     | Save_file_req (name, text)   ->
         save_file name text;
-    | Get_task nid                 -> send_task nid
+    | Get_task(nid,b)              -> send_task nid b
     | Replay_req                   -> replay_session ()
     | Interrupt_req                -> C.interrupt ()
     | Command_req (nid, cmd)       ->

src/session/json_util.ml

@@ -192,9 +192,9 @@ let print_request_to_json (r: ide_request): Json_base.json =
   | Set_max_tasks_req n ->
       convert_record ["ide_request", cc r;
            "tasks", Int n]
-  | Get_task n ->
+  | Get_task(n,b) ->
       convert_record ["ide_request", cc r;
-           "node_ID", Int n]
+           "node_ID", Int n; "do_intros", Bool b]
   | Get_file_contents s ->
       convert_record ["ide_request", cc r;
            "file", String s]
@@ -491,7 +491,8 @@ let parse_request (constr: string) j =
 
   | "Get_task" ->
     let n = get_int (get_field j "node_ID") in
-    Get_task n
+    let b = get_bool_opt (get_field j "do_intros") false in
+    Get_task(n,b)
 
   | "Remove_subtree" ->
     let n = get_int (get_field j "node_ID") in

src/tools/why3shell.ml

@@ -336,12 +336,17 @@ let interp _chout fmt cmd =
   begin
     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
+        cur_id := int_of_string n;
+        let b = false (* TODO: allow user to customize printing with intros or not *) in
+        send_request (Get_task(!cur_id,b));
+        print_session fmt
     | _ ->
         begin
           match cmd with
           | "ng" -> cur_id := (!cur_id + 1) mod !max_ID; print_session fmt
-          | "g" -> send_request (Get_task !cur_id)
+          | "g" ->
+             let b = false (* TODO: allow user to customize printing with intros or not *) in
+             send_request (Get_task(!cur_id,b))
           | "p" -> print_session fmt
           | _ -> send_request (Command_req (!cur_id, cmd))
         end

src/util/json_base.ml

@@ -109,3 +109,8 @@ let get_bool j =
   match j with
   | Bool b -> b
   | _ -> raise Not_found
+
+let get_bool_opt j def =
+  match j with
+  | Bool b -> b
+  | _ -> def

src/util/json_base.mli

@@ -72,6 +72,7 @@ val get_int: json -> int
 val get_list: json -> json list
 val get_float: json -> float
 val get_bool: json -> bool
+val get_bool_opt: json -> bool -> bool
 
 (* To parse a json value, use file Json_parser and function json_object. See
    end of session/Json_util.ml for an example use.