Imported Upstream version 8.9.0upstream/8.9.0upstream

1 files changed, 0 insertions, 522 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
deleted file mode 100644
index 6b7efc83..00000000
--- a/ide/ide_slave.ml
+++ /dev/null
@@ -1,522 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open Vernacexpr
-open Vernacprop
-open CErrors
-open Util
-open Pp
-open Printer
-
-module NamedDecl = Context.Named.Declaration
-module CompactedDecl = Context.Compacted.Declaration
-
-(** Ide_slave : an implementation of [Interface], i.e. mainly an interp
-    function and a rewind function. This specialized loop is triggered
-    when the -ideslave option is passed to Coqtop. *)
-
-
-(** Signal handling: we postpone ^C during input and output phases,
-    but make it directly raise a Sys.Break during evaluation of the request. *)
-
-let catch_break = ref false
-
-let init_signal_handler () =
-  let f _ = if !catch_break then raise Sys.Break else Control.interrupt := true in
-  Sys.set_signal Sys.sigint (Sys.Signal_handle f)
-
-let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) s
-
-let pr_error s = pr_with_pid s
-let pr_debug s =
-  if !Flags.debug then pr_with_pid s
-let pr_debug_call q =
-  if !Flags.debug then pr_with_pid ("<-- " ^ Xmlprotocol.pr_call q)
-let pr_debug_answer q r =
-  if !Flags.debug then pr_with_pid ("--> " ^ Xmlprotocol.pr_full_value q r)
-
-(** Categories of commands *)
-
-let coqide_known_option table = List.mem table [
-  ["Printing";"Implicit"];
-  ["Printing";"Coercions"];
-  ["Printing";"Matching"];
-  ["Printing";"Synth"];
-  ["Printing";"Notations"];
-  ["Printing";"All"];
-  ["Printing";"Records"];
-  ["Printing";"Existential";"Instances"];
-  ["Printing";"Universes"];
-  ["Printing";"Unfocused"]]
-
-let is_known_option cmd = match Vernacprop.under_control cmd with
-  | VernacSetOption (_, o, BoolValue true)
-  | VernacUnsetOption (_, o) -> coqide_known_option o
-  | _ -> false
-
-(** Check whether a command is forbidden in the IDE *)
-
-let ide_cmd_checks ~id {CAst.loc;v=ast} =
-  let user_error s = CErrors.user_err ?loc ~hdr:"IDE" (str s) in
-  let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
-  if is_debug ast then
-    user_error "Debug mode not available in the IDE";
-  if is_known_option ast then
-    warn "Set this option from the IDE menu instead";
-  if is_navigation_vernac ast || is_undo ast then
-    warn "Use IDE navigation instead"
-
-(** Interpretation (cf. [Ide_intf.interp]) *)
-
-let ide_doc = ref None
-let get_doc () = Option.get !ide_doc
-let set_doc doc = ide_doc := Some doc
-
-let add ((s,eid),(sid,verbose)) =
-  let doc = get_doc () in
-  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
-  let loc_ast = Stm.parse_sentence ~doc sid pa in
-  let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in
-  set_doc doc;
-  let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
-  ide_cmd_checks ~id:newid loc_ast;
-  (* TODO: the "" parameter is a leftover of the times the protocol
-   * used to include stderr/stdout output.
-   *
-   * Currently, we force all the output meant for the to go via the
-   * feedback mechanism, and we don't manipulate stderr/stdout, which
-   * are left to the client's discrection. The parameter is still there
-   * as not to break the core protocol for this minor change, but it should
-   * be removed in the next version of the protocol.
-   *)
-  newid, (rc, "")
-
-let edit_at id =
-  let doc = get_doc () in
-  match Stm.edit_at ~doc id with
-  | doc, `NewTip -> set_doc doc; CSig.Inl ()
-  | doc, `Focus { Stm.start; stop; tip} -> set_doc doc; CSig.Inr (start, (stop, tip))
-
-(* TODO: the "" parameter is a leftover of the times the protocol
- * used to include stderr/stdout output.
- *
- * Currently, we force all the output meant for the to go via the
- * feedback mechanism, and we don't manipulate stderr/stdout, which
- * are left to the client's discrection. The parameter is still there
- * as not to break the core protocol for this minor change, but it should
- * be removed in the next version of the protocol.
- *)
-let query (route, (s,id)) =
-  let pa = Pcoq.Gram.parsable (Stream.of_string s) in
-  let doc = get_doc () in
-  Stm.query ~at:id ~doc ~route pa
-
-let annotate phrase =
-  let doc = get_doc () in
-  let {CAst.loc;v=ast} =
-    let pa = Pcoq.Gram.parsable (Stream.of_string phrase) in
-    Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa
-  in
-  (* XXX: Width should be a parameter of annotate... *)
-  Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast)
-
-(** Goal display *)
-
-let hyp_next_tac sigma env decl =
-  let id = NamedDecl.get_id decl in
-  let ast = NamedDecl.get_type decl in
-  let id_s = Names.Id.to_string id in
-  let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in
-  [
-    ("clear "^id_s),("clear "^id_s^".");
-    ("apply "^id_s),("apply "^id_s^".");
-    ("exact "^id_s),("exact "^id_s^".");
-    ("generalize "^id_s),("generalize "^id_s^".");
-    ("absurd <"^id_s^">"),("absurd "^type_s^".")
-  ] @ [
-    ("discriminate "^id_s),("discriminate "^id_s^".");
-    ("injection "^id_s),("injection "^id_s^".")
-  ] @ [
-    ("rewrite "^id_s),("rewrite "^id_s^".");
-    ("rewrite <- "^id_s),("rewrite <- "^id_s^".")
-  ] @ [
-    ("elim "^id_s), ("elim "^id_s^".");
-    ("inversion "^id_s), ("inversion "^id_s^".");
-    ("inversion clear "^id_s), ("inversion_clear "^id_s^".")
-  ]
-
-let concl_next_tac sigma concl =
-  let expand s = (s,s^".") in
-  List.map expand ([
-    "intro";
-    "intros";
-    "intuition"
-  ] @ [
-    "reflexivity";
-    "discriminate";
-    "symmetry"
-  ] @ [
-    "assumption";
-    "omega";
-    "ring";
-    "auto";
-    "eauto";
-    "tauto";
-    "trivial";
-    "decide equality";
-    "simpl";
-    "subst";
-    "red";
-    "split";
-    "left";
-    "right"
-  ])
-
-let process_goal sigma g =
-  let env = Goal.V82.env sigma g in
-  let min_env = Environ.reset_context env in
-  let id = Goal.uid g in
-  let ccl =
-    pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
-  in
-  let process_hyp d (env,l) =
-    let d' = CompactedDecl.to_named_context d in
-      (List.fold_right Environ.push_named d' env,
-       (pr_compacted_decl env sigma d) :: l) in
-  let (_env, hyps) =
-    Context.Compacted.fold process_hyp
-      (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in
-  { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
-
-let export_pre_goals pgs =
-  {
-    Interface.fg_goals       = pgs.Proof.fg_goals;
-    Interface.bg_goals       = pgs.Proof.bg_goals;
-    Interface.shelved_goals  = pgs.Proof.shelved_goals;
-    Interface.given_up_goals = pgs.Proof.given_up_goals
-  }
-
-let goals () =
-  let doc = get_doc () in
-  set_doc @@ Stm.finish ~doc;
-  try
-    let pfts = Proof_global.give_me_the_proof () in
-    Some (export_pre_goals (Proof.map_structured_proof pfts process_goal))
-  with Proof_global.NoCurrentProof -> None
-
-let evars () =
-  try
-    let doc = get_doc () in
-    set_doc @@ Stm.finish ~doc;
-    let pfts = Proof_global.give_me_the_proof () in
-    let all_goals, _, _, _, sigma = Proof.proof pfts in
-    let exl = Evar.Map.bindings (Evd.undefined_map sigma) in
-    let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in
-    let el = List.map map_evar exl in
-    Some el
-  with Proof_global.NoCurrentProof -> None
-
-let hints () =
-  try
-    let pfts = Proof_global.give_me_the_proof () in
-    let all_goals, _, _, _, sigma = Proof.proof pfts in
-    match all_goals with
-    | [] -> None
-    | g :: _ ->
-      let env = Goal.V82.env sigma g in
-      let hint_goal = concl_next_tac sigma g in
-      let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in
-      let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in
-      Some (hint_hyps, hint_goal)
-  with Proof_global.NoCurrentProof -> None
-
-
-(** Other API calls *)
-
-let wait () =
-  let doc = get_doc () in
-  set_doc (Stm.wait ~doc)
-
-let status force =
-  (** We remove the initial part of the current [DirPath.t]
-      (usually Top in an interactive session, cf "coqtop -top"),
-      and display the other parts (opened sections and modules) *)
-  set_doc (Stm.finish ~doc:(get_doc ()));
-  if force then
-    set_doc (Stm.join ~doc:(get_doc ()));
-  let path =
-    let l = Names.DirPath.repr (Lib.cwd ()) in
-    List.rev_map Names.Id.to_string l
-  in
-  let proof =
-    try Some (Names.Id.to_string (Proof_global.get_current_proof_name ()))
-    with Proof_global.NoCurrentProof -> None
-  in
-  let allproofs =
-    let l = Proof_global.get_all_proof_names () in
-    List.map Names.Id.to_string l
-  in
-  {
-    Interface.status_path = path;
-    Interface.status_proofname = proof;
-    Interface.status_allproofs = allproofs;
-    Interface.status_proofnum = Stm.current_proof_depth ~doc:(get_doc ());
-  }
-
-let export_coq_object t = {
-  Interface.coq_object_prefix = t.Search.coq_object_prefix;
-  Interface.coq_object_qualid = t.Search.coq_object_qualid;
-  Interface.coq_object_object = Pp.string_of_ppcmds (pr_lconstr_env (Global.env ()) Evd.empty t.Search.coq_object_object)
-}
-
-let pattern_of_string ?env s =
-  let env =
-    match env with
-    | None -> Global.env ()
-    | Some e -> e
-  in
-  let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
-  let (_, pat) = Constrintern.intern_constr_pattern env Evd.empty constr in
-  pat
-
-let dirpath_of_string_list s =
-  let path = String.concat "." s in
-  let m = Pcoq.parse_string Pcoq.Constr.global path in
-  let {CAst.v=qid} = Libnames.qualid_of_reference m in
-  let id =
-    try Nametab.full_name_module qid
-    with Not_found ->
-      CErrors.user_err ~hdr:"Search.interface_search"
-        (str "Module " ++ str path ++ str " not found.")
-  in
-  id
-
-let import_search_constraint = function
-  | Interface.Name_Pattern s    -> Search.Name_Pattern (Str.regexp s)
-  | Interface.Type_Pattern s    -> Search.Type_Pattern (pattern_of_string s)
-  | Interface.SubType_Pattern s -> Search.SubType_Pattern (pattern_of_string s)
-  | Interface.In_Module ms      -> Search.In_Module (dirpath_of_string_list ms)
-  | Interface.Include_Blacklist -> Search.Include_Blacklist
-
-let search flags =
-  List.map export_coq_object (Search.interface_search (
-    List.map (fun (c, b) -> (import_search_constraint c, b)) flags)
-  )
-
-let export_option_value = function
-  | Goptions.BoolValue b   -> Interface.BoolValue b
-  | Goptions.IntValue x    -> Interface.IntValue x
-  | Goptions.StringValue s -> Interface.StringValue s
-  | Goptions.StringOptValue s -> Interface.StringOptValue s
-
-let import_option_value = function
-  | Interface.BoolValue b   -> Goptions.BoolValue b
-  | Interface.IntValue x    -> Goptions.IntValue x
-  | Interface.StringValue s -> Goptions.StringValue s
-  | Interface.StringOptValue s -> Goptions.StringOptValue s
-
-let export_option_state s = {
-  Interface.opt_sync  = true;
-  Interface.opt_depr  = s.Goptions.opt_depr;
-  Interface.opt_name  = s.Goptions.opt_name;
-  Interface.opt_value = export_option_value s.Goptions.opt_value;
-}
-
-let get_options () =
-  let table = Goptions.get_tables () in
-  let fold key state accu = (key, export_option_state state) :: accu in
-  Goptions.OptionMap.fold fold table []
-
-let set_options options =
-  let iter (name, value) = match import_option_value value with
-  | BoolValue b -> Goptions.set_bool_option_value name b
-  | IntValue i -> Goptions.set_int_option_value name i
-  | StringValue s -> Goptions.set_string_option_value name s
-  | StringOptValue (Some s) -> Goptions.set_string_option_value name s
-  | StringOptValue None -> Goptions.unset_option_value_gen name
-  in
-  List.iter iter options
-
-let about () = {
-  Interface.coqtop_version = Coq_config.version;
-  Interface.protocol_version = Xmlprotocol.protocol_version;
-  Interface.release_date = Coq_config.date;
-  Interface.compile_date = Coq_config.compile_date;
-}
-
-let handle_exn (e, info) =
-  let (e, info) = ExplainErr.process_vernac_interp_error (e, info) in
-  let dummy = Stateid.dummy in
-  let loc_of e = match Loc.get_loc e with
-    | Some loc -> Some (Loc.unloc loc)
-    | _        -> None in
-  let mk_msg () = CErrors.print ~info e in
-  match e with
-  | CErrors.Drop -> dummy, None, Pp.str "Drop is not allowed by coqide!"
-  | CErrors.Quit -> dummy, None, Pp.str "Quit is not allowed by coqide!"
-  | e ->
-      match Stateid.get info with
-      | Some (valid, _) -> valid, loc_of info, mk_msg ()
-      | None -> dummy, loc_of info, mk_msg ()
-
-let init =
-  let initialized = ref false in
-  fun file ->
-   if !initialized then anomaly (str "Already initialized.")
-   else begin
-     let init_sid = Stm.get_current_state ~doc:(get_doc ()) in
-     initialized := true;
-     match file with
-     | None -> init_sid
-     | Some file ->
-         let doc, initial_id, _ =
-           get_doc (), init_sid, `NewTip in
-         if Filename.check_suffix file ".v" then
-           Stm.set_compilation_hints file;
-         set_doc (Stm.finish ~doc);
-         initial_id
-   end
-
-(* Retrocompatibility stuff, disabled since 8.7 *)
-let interp ((_raw, verbose), s) =
-  Stateid.dummy, CSig.Inr "The interp call has been disabled, please use Add."
-
-(** When receiving the Quit call, we don't directly do an [exit 0],
-    but rather set this reference, in order to send a final answer
-    before exiting. *)
-
-let quit = ref false
-
-(** Disabled *)
-let print_ast id = Xml_datatype.PCData "ERROR"
-
-(** Grouping all call handlers together + error handling *)
-
-let eval_call c =
-  let interruptible f x =
-    catch_break := true;
-    Control.check_for_interrupt ();
-    let r = f x in
-    catch_break := false;
-    r
-  in
-  let handler = {
-    Interface.add = interruptible add;
-    Interface.edit_at = interruptible edit_at;
-    Interface.query = interruptible query;
-    Interface.goals = interruptible goals;
-    Interface.evars = interruptible evars;
-    Interface.hints = interruptible hints;
-    Interface.status = interruptible status;
-    Interface.search = interruptible search;
-    Interface.get_options = interruptible get_options;
-    Interface.set_options = interruptible set_options;
-    Interface.mkcases = interruptible Vernacentries.make_cases;
-    Interface.quit = (fun () -> quit := true);
-    Interface.init = interruptible init;
-    Interface.about = interruptible about;
-    Interface.wait = interruptible wait;
-    Interface.interp = interruptible interp;
-    Interface.handle_exn = handle_exn;
-    Interface.stop_worker = Stm.stop_worker;
-    Interface.print_ast = print_ast;
-    Interface.annotate = interruptible annotate;
-  } in
-  Xmlprotocol.abstract_eval_call handler c
-
-(** Message dispatching.
-    Since coqtop -ideslave starts 1 thread per slave, and each
-    thread forwards feedback messages from the slave to the GUI on the same
-    xml channel, we need mutual exclusion.  The mutex should be per-channel, but
-    here we only use 1 channel. *)
-let print_xml =
-  let m = Mutex.create () in
-  fun oc xml ->
-    Mutex.lock m;
-    try Xml_printer.print oc xml; Mutex.unlock m
-    with e -> let e = CErrors.push e in Mutex.unlock m; iraise e
-
-let slave_feeder fmt xml_oc msg =
-  let xml = Xmlprotocol.(of_feedback fmt msg) in
-  print_xml xml_oc xml
-
-(** The main loop *)
-
-(** Exceptions during eval_call should be converted into [Interface.Fail]
-    messages by [handle_exn] above. Otherwise, we die badly, without
-    trying to answer malformed requests. *)
-
-let msg_format = ref (fun () ->
-    let margin = Option.default 72 (Topfmt.get_margin ()) in
-    Xmlprotocol.Richpp margin
-  )
-
-(* The loop ignores the command line arguments as the current model delegates
-   its handing to the toplevel container. *)
-let loop _args ~state =
-  let open Vernac.State in
-  set_doc state.doc;
-  init_signal_handler ();
-  catch_break := false;
-  let in_ch, out_ch = Spawned.get_channels ()                        in
-  let xml_oc        = Xml_printer.make (Xml_printer.TChannel out_ch) in
-  let in_lb         = Lexing.from_function (fun s len ->
-                      CThread.thread_friendly_read in_ch s ~off:0 ~len) in
-  (* SEXP parser make *)
-  let xml_ic        = Xml_parser.make (Xml_parser.SLexbuf in_lb) in
-  let () = Xml_parser.check_eof xml_ic false in
-  ignore (Feedback.add_feeder (slave_feeder (!msg_format ()) xml_oc));
-  while not !quit do
-    try
-      let xml_query = Xml_parser.parse xml_ic in
-(*       pr_with_pid (Xml_printer.to_string_fmt xml_query); *)
-      let Xmlprotocol.Unknown q = Xmlprotocol.to_call xml_query in
-      let () = pr_debug_call q in
-      let r  = eval_call q in
-      let () = pr_debug_answer q r in
-(*       pr_with_pid (Xml_printer.to_string_fmt (Xmlprotocol.of_answer q r)); *)
-      print_xml xml_oc Xmlprotocol.(of_answer (!msg_format ()) q r);
-      flush out_ch
-    with
-      | Xml_parser.Error (Xml_parser.Empty, _) ->
-        pr_debug "End of input, exiting gracefully.";
-        exit 0
-      | Xml_parser.Error (err, loc) ->
-        pr_error ("XML syntax error: " ^ Xml_parser.error_msg err)
-      | Serialize.Marshal_error (msg,node) ->
-        pr_error "Unexpected XML message";
-        pr_error ("Expected XML node: " ^ msg);
-        pr_error ("XML tree received: " ^ Xml_printer.to_string_fmt node)
-      | any ->
-        pr_debug ("Fatal exception in coqtop:\n" ^ Printexc.to_string any);
-        exit 1
-  done;
-  pr_debug "Exiting gracefully.";
-  exit 0
-
-let rec parse = function
-  | "--help-XML-protocol" :: rest ->
-        Xmlprotocol.document Xml_printer.to_string_fmt; exit 0
-  | "--xml_format=Ppcmds" :: rest ->
-        msg_format := (fun () -> Xmlprotocol.Ppcmds); parse rest
-  | x :: rest -> x :: parse rest
-  | [] -> []
-
-let () = Coqtop.toploop_init := (fun coq_args extra_args ->
-        let args = parse extra_args in
-        Flags.quiet := true;
-        CoqworkmgrApi.(init High);
-        args)
-
-let () = Coqtop.toploop_run := loop
-
-let () = Usage.add_to_usage "coqidetop"
-"  --xml_format=Ppcmds    serialize pretty printing messages using the std_ppcmds format\
-\n  --help-XML-protocol    print documentation of the Coq XML protocol\n"