remove all implicit use of introduce_premises

src/ide/why3ide.ml

@@ -1476,9 +1476,9 @@ let on_selected_row r =
       if detached then
         task_view#source_buffer#set_text ""
       else
-        let b = gconfig.intro_premises in
+        let _b = gconfig.intro_premises in
         let c = gconfig.show_full_context in
-        send_request (Get_task(id,b,c,true))
+        send_request (Get_task(id,c,true))
     | NProofAttempt ->
        let (pa, _obs, _l) = Hint.find node_id_pa id in
        let output_text =
@@ -1508,13 +1508,13 @@ let on_selected_row r =
        if detached then
          task_view#source_buffer#set_text ""
        else
-         let b = gconfig.intro_premises in
+         let _b = gconfig.intro_premises in
          let c = gconfig.show_full_context in
-         send_request (Get_task(id,b,c,true))
+         send_request (Get_task(id,c,true))
     | _ ->
-       let b = gconfig.intro_premises in
+       let _b = gconfig.intro_premises in
        let c = gconfig.show_full_context in
-       send_request (Get_task(id,b,c,true))
+       send_request (Get_task(id,c,true))
   with
     | Not_found -> task_view#source_buffer#set_text ""
 

src/ide/why3web.ml

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

src/session/controller_itp.ml

@@ -354,7 +354,7 @@ let build_prover_call ?proof_script ~cntexample c id pr limit callback ores =
   let command =
     Whyconf.get_complete_command config_pr ~with_steps in
   try
-    let task = Session_itp.get_raw_task c.controller_session id in
+    let task = Session_itp.get_task c.controller_session id in
     Debug.dprintf debug_sched "[build_prover_call] Script file = %a@."
                   (Pp.print_option Pp.string) proof_script;
     let inplace = config_pr.Whyconf.in_place in
@@ -545,7 +545,7 @@ let schedule_proof_attempt c id pr
 let create_file_rel_path c pr pn =
   let session = c.controller_session in
   let driver = snd (Hprover.find c.controller_provers pr) in
-  let task = Session_itp.get_raw_task session pn in
+  let task = Session_itp.get_task session pn in
   let session_dir = Session_itp.get_dir session in
   let th = get_encapsulating_theory session (APn pn) in
   let th_name = (Session_itp.theory_name th).Ident.id_string in
@@ -603,7 +603,7 @@ let prepare_edition c ?file pn pr ~notification =
   in
   let ch = open_out file in
   let fmt = formatter_of_out_channel ch in
-  let task = Session_itp.get_raw_task session pn in
+  let task = Session_itp.get_task session pn in
   let driver = snd (Hprover.find c.controller_provers pr) in
   Driver.print_task ~cntexample:false ?old driver fmt task;
   Opt.iter close_in old;
@@ -940,7 +940,7 @@ let replay_proof_attempt c pr limit (parid: proofNodeID) id ~callback ~notificat
   | Some pr' ->
      try
        if pr' <> pr then callback id (UpgradeProver pr');
-       let _ = get_raw_task c.controller_session parid in
+       let _ = get_task c.controller_session parid in
        schedule_proof_attempt c parid pr' ~counterexmp:false ~limit ~callback ~notification
      with Not_found ->
        callback id Detached
@@ -1229,7 +1229,7 @@ later on. We do has if proof fails. *)
   in
   Debug.dprintf debug "Bisecting with %a started.@."
                 Whyconf.print_prover prover;
-  let t = get_raw_task ses goal_id in
+  let t = get_task ses goal_id in
   match Eliminate_definition.bisect_step t with
   | Eliminate_definition.BSdone _ -> assert false
   | Eliminate_definition.BSstep(rem,kont) -> bisect_step rem kont

src/session/itp_communication.ml

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

src/session/itp_communication.mli

@@ -117,10 +117,9 @@ type ide_request =
   | Add_file_req            of string
   | Set_config_param        of string * int
   | Get_file_contents       of string
-  | Get_task                of node_ID * bool * bool * bool
-  (** [Get_task(id,b,c,loc)] requests for the text of the task in node
-      [id].  When [b] is true then quantified variables and hypotheses
-      are introduced as local definitions. When [c] is true then the
+  | Get_task                of node_ID * bool * bool
+  (** [Get_task(id,b,loc)] requests for the text of the task in node
+      [id].  When [b] is true then the
       full context is show.  When [loc] is false the locations are not
       returned *)
   | Focus_req               of node_ID

src/session/itp_server.ml

@@ -77,7 +77,7 @@ let unproven_goals_below_id cont id =
 (****** Exception handling *********)
 
 let p s id =
-  let _,tables = Session_itp.get_task s id in
+  let _,tables = Session_itp.get_task_name_table s id in
   let pr = tables.Trans.printer in
   let apr = tables.Trans.aprinter in
   (Pretty.create pr apr pr pr false)
@@ -270,7 +270,7 @@ let print_request fmt r =
   | Set_config_param(s,i)           -> fprintf fmt "set config param %s %i" s i
   | Get_file_contents _f            -> fprintf fmt "get file contents"
   | Get_first_unproven_node _nid    -> fprintf fmt "get first unproven node"
-  | Get_task(nid,b,c,loc)           -> fprintf fmt "get task(%d,%b,%b,%b)" nid b c loc
+  | Get_task(nid,b,loc)           -> fprintf fmt "get task(%d,%b,%b)" nid b loc
   | Focus_req _nid                  -> fprintf fmt "focus"
   | Unfocus_req                     -> fprintf fmt "unfocus"
   | Remove_subtree _nid             -> fprintf fmt "remove subtree"
@@ -772,7 +772,7 @@ end
       | Some label_detection ->
           (match node with
           | APn pr_node ->
-              let task = Session_itp.get_raw_task session pr_node in
+              let task = Session_itp.get_task session pr_node in
               let b = label_detection task in
               if b then
                 add_focused_node node
@@ -880,12 +880,8 @@ end
     reset_and_send_the_whole_tree ()
 
   (* -- send the task -- *)
-  let task_of_id d id do_intros show_full_context loc =
-    let task,tables = get_task d.cont.controller_session id in
-    let task =
-      if do_intros then task else
-        get_raw_task d.cont.controller_session id
-    in
+  let task_of_id d id show_full_context loc =
+    let task,tables = get_task_name_table d.cont.controller_session id in
     (* This function also send source locations associated to the task *)
     let loc_color_list = if loc then get_locations task else [] in
     let task_text =
@@ -896,11 +892,11 @@ end
     in
     task_text, loc_color_list
 
-  let send_task nid do_intros show_full_context loc =
+  let send_task nid show_full_context loc =
     let d = get_server_data () in
     match any_from_node_ID nid with
     | APn id ->
-       let s, list_loc = task_of_id d id do_intros show_full_context loc in
+       let s, list_loc = task_of_id d id show_full_context loc in
        P.notify (Task (nid, s, list_loc))
     | ATh t ->
        P.notify (Task (nid, "Theory " ^ (theory_name t).Ident.id_string, []))
@@ -908,7 +904,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 do_intros show_full_context loc in
+       let s, list_loc = task_of_id d parid show_full_context loc in
        let prover_text = s ^ "\n====================> Prover: " ^ name ^ "\n" in
        (* Display the result of the prover *)
        let prover_ce =
@@ -935,7 +931,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 do_intros show_full_context loc in
+       let s, list_loc = task_of_id d parid show_full_context loc in
        P.notify (Task (nid, s ^ "\n====================> Transformation: " ^
                        String.concat " " (name :: args) ^ "\n", list_loc))
 
@@ -1321,7 +1317,7 @@ end
          Hint.mem model_any nid
      | Copy_paste (from_id, to_id) ->
          Hint.mem model_any from_id && Hint.mem model_any to_id
-     | Get_task(nid,_,_,_) ->
+     | Get_task(nid,_,_) ->
          Hint.mem model_any nid
      | Command_req (nid, _) ->
          if not (Itp_communication.is_root nid) then
@@ -1391,7 +1387,7 @@ end
         read_and_send f
     | Save_file_req (name, text)   ->
         save_file name text;
-    | Get_task(nid,b,c,loc)         -> send_task nid b c loc
+    | Get_task(nid,b,loc)         -> send_task nid b loc
     | Interrupt_req                -> C.interrupt ()
     | Command_req (nid, cmd)       ->
       begin

src/session/json_util.ml

@@ -176,9 +176,9 @@ let print_request_to_json (r: ide_request): Json_base.json =
   | Set_config_param(s,n) ->
       convert_record ["ide_request", cc r;
            "param", String s; "value", Int n]
-  | Get_task(n,b,c,loc) ->
+  | Get_task(n,b,loc) ->
       convert_record ["ide_request", cc r;
-           "node_ID", Int n; "do_intros", Bool b; "full_context", Bool c ; "loc", Bool loc]
+           "node_ID", Int n; "full_context", Bool b ; "loc", Bool loc]
   | Get_file_contents s ->
       convert_record ["ide_request", cc r;
            "file", String s]
@@ -432,10 +432,9 @@ let parse_request (constr: string) j =
 
   | "Get_task" ->
     let n = get_int (get_field j "node_ID") in
-    let b = get_bool_opt (get_field j "do_intros") false in
-    let c = get_bool_opt (get_field j "full_context") false in
+    let b = get_bool_opt (get_field j "full_context") false in
     let loc = get_bool_opt (get_field j "loc") false in
-    Get_task(n,b,c,loc)
+    Get_task(n,b,loc)
 
   | "Remove_subtree" ->
     let n = get_int (get_field j "node_ID") in

src/session/server_utils.ml

@@ -372,7 +372,7 @@ type command =
   | Other        of string * string list
 
 let query_on_task cont f id args =
-  let _,table = Session_itp.get_task cont.Controller_itp.controller_session id in
+  let _,table = Session_itp.get_task_name_table cont.Controller_itp.controller_session id in
   try Query (f cont table args) with
     | Undefined_id s -> QError ("No existing id corresponding to " ^ s)
     | Number_of_arguments -> QError "Bad number of arguments"

src/session/session_itp.ml

@@ -122,7 +122,7 @@ type session = {
   session_prover_ids            : int Hprover.t;
   (* tasks *)
   session_raw_tasks : Task.task Hpn.t;
-  session_tasks : (Task.task * Trans.naming_table) Hpn.t;
+  session_task_tables : Trans.naming_table Hpn.t;
   (* proved status *)
   file_state: bool Hstr.t;
   th_state: bool Ident.Hid.t;
@@ -223,18 +223,19 @@ let get_proofNode (s : session) (id : proofNodeID) =
     Hint.find s.proofNode_table id
   with Not_found -> raise BadID
 
-let get_raw_task s id =
+let get_task s id =
   Hpn.find s.session_raw_tasks id
 
-let get_task s n =
-  try
-    Hpn.find s.session_tasks n
+let get_task_name_table s n =
+  let t = get_task s n in
+  let table = try
+    Hpn.find s.session_task_tables n
   with Not_found ->
-    let t = get_raw_task s n in
-    let ti = Trans.apply Introduction.introduce_premises t in
-    let ta = Args_wrapper.build_naming_tables ti in
-    Hpn.add s.session_tasks n (ti,ta);
-    ti,ta
+    let ta = Args_wrapper.build_naming_tables t in
+    Hpn.add s.session_task_tables n ta;
+    ta
+  in
+  t,table
 
 let get_transfNode (s : session) (id : transID) =
   try
@@ -278,7 +279,7 @@ let get_trans_parent (s : session) (id : transID) =
   (get_transfNode s id).transf_parent
 
 let goal_is_detached s pn =
-  try let (_:Task.task) = get_raw_task s pn in false
+  try let (_:Task.task) = get_task s pn in false
   with Not_found -> true
 
 let transf_is_detached s tn =
@@ -527,7 +528,7 @@ let empty_session ?from dir =
     session_shape_version = shape_version;
     session_prover_ids = prover_ids;
     session_raw_tasks = Hpn.create 97;
-    session_tasks = Hpn.create 97;
+    session_task_tables = Hpn.create 97;
     file_state = Hstr.create 3;
     th_state = Ident.Hid.create 7;
     tn_state = Htn.create 97;
@@ -1361,37 +1362,14 @@ let merge_proof new_s ~goal_obsolete new_goal _ old_pa_n =
 exception NoProgress
 
 let apply_trans_to_goal ~allow_no_effect s env name args id =
-  let task, subtasks =
-    let raw_task = get_raw_task s id in
-    let task,table = get_task s id in
-    try
-      let new_task_list = Trans.apply_transform_args name env args table raw_task in
-      (* If any generated task is equal to the former task, then we made no
+  let task,table = get_task_name_table s id in
+  let subtasks = Trans.apply_transform_args name env args table task in
+  (* If any generated task is equal to the former task, then we made no
          progress because we need to prove more lemmas than before *)
-      if List.exists (fun t -> Task.task_equal t raw_task) new_task_list then
-        begin
-          Debug.dprintf debug "[apply_trans_to_goal] apply_transform on raw task made no progress@.";
-          raise NoProgress
-        end
-      else
-        raw_task, new_task_list
-    with
-    (* if apply_transform fails for any reason, we try to apply
-       the same transformation on the "introduced" task instead *)
-    | Generic_arg_trans_utils.Arg_trans _
-    | Trans.TransFailure _
-    | NoProgress as e ->
-       Debug.dprintf debug "[apply_trans_to_goal] info: apply_transform raised exception %a@."
-                     Exn_printer.exn_printer e;
-       task, Trans.apply_transform_args name env args table task
-    | e ->
-       Debug.dprintf debug "[apply_trans_to_goal] warning: apply_transform raised unexpected %a@."
-                     Exn_printer.exn_printer e;
-       task, Trans.apply_transform_args name env args table task
-  in
   match subtasks with
   | [t'] when Task.task_equal t' task && not allow_no_effect ->
-     raise Exit
+     Debug.dprintf debug "[apply_trans_to_goal] apply_transform made no progress@.";
+     raise NoProgress
   | _ -> subtasks
 
 

src/session/session_itp.mli

@@ -87,8 +87,8 @@ val is_below: session -> any -> any -> bool
 type proof_parent = Trans of transID | Theory of theory
 
 
-val get_raw_task : session -> proofNodeID -> Task.task
-val get_task : session -> proofNodeID -> Task.task * Trans.naming_table
+val get_task : session -> proofNodeID -> Task.task
+val get_task_name_table : session -> proofNodeID -> Task.task * Trans.naming_table
 
 val get_transformations : session -> proofNodeID -> transID list
 val get_proof_attempt_ids :
@@ -191,12 +191,13 @@ val graft_proof_attempt : ?file:string -> session -> proofNodeID ->
     proof_script field equal to [file].
 *)
 
+exception NoProgress
 val apply_trans_to_goal :
   allow_no_effect:bool -> session -> Env.env -> string -> string list ->
   proofNodeID -> Task.task list
 (** [apply_trans_to_goal s env tr args id] applies the transformation
   [tr] with arguments [args] to the goal [id], and returns the
-  subtasks.  raises [Exit] if [allow_no_effect] is false and [tr]
+  subtasks.  raises [NoProgress] if [allow_no_effect] is false and [tr]
   returns the task unchanged *)
 
 val graft_transf : session -> proofNodeID -> string -> string list ->

src/tools/why3shell.ml

@@ -353,18 +353,16 @@ let interp _chout fmt cmd =
     match l with
     | ["goto"; n] when int_of_string n < !max_ID ->
         cur_id := int_of_string n;
-        let b = false (* TODO: allow user to customize printing with intros or not *) in
         let c = false (* TODO *) in
-        send_request (Get_task(!cur_id,b,c,false));
+        send_request (Get_task(!cur_id,c,false));
         print_session fmt
     | _ ->
         begin
           match cmd with
           | "ng" -> cur_id := (!cur_id + 1) mod !max_ID; print_session fmt
           | "g" ->
-             let b = false (* TODO: allow user to customize printing with intros or not *) in
              let c = false (* TODO *) in
-             send_request (Get_task(!cur_id,b,c,false))
+             send_request (Get_task(!cur_id,c,false))
           | "p" -> print_session fmt
           | _ -> send_request (Command_req (!cur_id, cmd))
         end

src/transform/introduction.ml

@@ -76,13 +76,14 @@ let () = Trans.register_transform "introduce_premises" introduce_premises
   ~desc:"Introduce@ universal@ quantification@ and@ hypothesis@ in@ the@ \
          goal@ into@ constant@ symbol@ and@ axioms."
 
+(*
 let split_intro =
   Trans.compose_l Split_goal.split_goal_wp (Trans.singleton introduce_premises)
 
 let () = Trans.register_transform_l "split_intro" split_intro
   ~desc:"Same@ as@ split_goal_wp,@ but@ moves@ \
     the@ implication@ antecedents@ to@ premises."
-
+ *)
 
 (** Destruction of existential quantifiers in axioms.
     Contributed by Nicolas Jeannerod [niols@niols.fr] *)
@@ -112,3 +113,25 @@ let () = Trans.register_transform
            "introduce_exists"
            (Trans.decl eliminate_exists None)
            ~desc:"Replace axioms of the form 'exists x. P' by 'constant x axiom P'."
+
+
+let split_goal_wp =
+  Trans.compose_l Split_goal.split_goal_right (Trans.singleton introduce_premises)
+
+let split_all_wp =
+  Trans.compose_l Split_goal.split_all_right (Trans.singleton introduce_premises)
+
+let split_premise_wp =
+  Trans.compose Split_goal.split_premise_right introduce_premises
+
+let () = Trans.register_transform_l
+           "split_goal_wp" split_goal_wp
+           ~desc:"Same@ as@ split_goal_right."
+
+let () = Trans.register_transform_l
+           "split_all_wp" split_all_wp
+           ~desc:"Same@ as@ split_goal_wp,@ but@ also@ split@ premises."
+
+let () = Trans.register_transform
+           "split_premise_wp" split_premise_wp
+           ~desc:"Same@ as@ split_all_wp,@ but@ split@ only@ premises."

src/transform/introduction.mli

@@ -33,5 +33,8 @@ val intros :  Decl.prsymbol -> Term.term -> Decl.decl list
 
 val introduce_premises : Task.task Trans.trans
 
+
+(* superseded by split_goal_wp
 val split_intro : Task.task Trans.tlist
 (** [split_intro] is [split_goal_wp] followed by [introduce_premises] *)
+ *)

src/transform/split_goal.ml

@@ -521,15 +521,12 @@ let prep_premise split = Trans.store (fun t ->
 
 let split_goal_full  = prep_goal full_proof
 let split_goal_right = prep_goal right_proof
-let split_goal_wp    = split_goal_right
 
 let split_all_full  = prep_all full_proof
 let split_all_right = prep_all right_proof
-let split_all_wp    = split_all_right
 
 let split_premise_full  = prep_premise full_proof
 let split_premise_right = prep_premise right_proof
-let split_premise_wp    = split_premise_right
 
 let () = Trans.register_transform_l "split_goal_full" split_goal_full
   ~desc:"Put@ the@ goal@ in@ a@ conjunctive@ form,@ \
@@ -548,11 +545,3 @@ let () = Trans.register_transform_l "split_all_right" split_all_right
   ~desc:"Same@ as@ split_goal_right,@ but@ also@ split@ premises."
 let () = Trans.register_transform "split_premise_right" split_premise_right
   ~desc:"Same@ as@ split_all_right,@ but@ split@ only@ premises."
-
-let () = Trans.register_transform_l "split_goal_wp" split_goal_wp
-  ~desc:"Same@ as@ split_goal_right."
-let () = Trans.register_transform_l "split_all_wp" split_all_wp
-  ~desc:"Same@ as@ split_goal_wp,@ but@ also@ split@ premises."
-let () = Trans.register_transform "split_premise_wp" split_premise_wp
-  ~desc:"Same@ as@ split_all_wp,@ but@ split@ only@ premises."
-

src/transform/split_goal.mli

@@ -56,8 +56,3 @@ val split_premise_full : Task.task Trans.trans
 val split_goal_right : Task.task Trans.tlist
 val split_all_right : Task.task Trans.tlist
 val split_premise_right : Task.task Trans.trans
-
-val split_goal_wp : Task.task Trans.tlist
-val split_all_wp : Task.task Trans.tlist
-val split_premise_wp : Task.task Trans.trans
-