|
(************************************************************************)
(* * 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
(** Idetop : an implementation of [Interface], i.e. mainly an interp
function and a rewind function. *)
(** 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"];
["Diffs"]]
let is_known_option cmd = match Vernacprop.under_control cmd with
| VernacSetOption (_, o, OptionSetTrue)
| VernacSetOption (_, o, OptionSetString _)
| VernacSetOption (_, o, OptionUnset) -> coqide_known_option o
| _ -> false
(** Check whether a command is forbidden in the IDE *)
let ide_cmd_checks ~last_valid {CAst.loc;v=ast} =
let user_error s =
try CErrors.user_err ?loc ~hdr:"IDE" (str s)
with e ->
let (e, info) = CErrors.push e in
let info = Stateid.add info ~valid:last_valid Stateid.dummy in
Exninfo.raise ~info e
in
if is_debug ast then
user_error "Debug mode not available in the IDE"
let ide_cmd_warns ~id {CAst.loc;v=ast} =
let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in
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.Parsable.make (Stream.of_string s) in
match Stm.parse_sentence ~doc sid ~entry:Pvernac.main_entry pa with
| None -> assert false (* s is not an empty string *)
| Some ast ->
ide_cmd_checks ~last_valid:sid ast;
let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose ast in
set_doc doc;
let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in
ide_cmd_warns ~id:newid 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.Parsable.make (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 pa = Pcoq.Parsable.make (Stream.of_string phrase) in
match Stm.parse_sentence ~doc (Stm.get_current_state ~doc) ~entry:Pvernac.main_entry pa with
| None -> Richpp.richpp_of_pp 78 (Pp.mt ())
| Some ast ->
(* XXX: Width should be a parameter of annotate... *)
Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast.CAst.v)
(** 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 =
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 process_goal_diffs diff_goal_map oldp nsigma ng =
let open Evd in
let og_s = match oldp with
| Some oldp ->
let Proof.{ sigma=osigma } = Proof.data oldp in
(try Some { it = Evar.Map.find ng diff_goal_map; sigma = osigma }
with Not_found -> None)
| None -> None
in
let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in
{ Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng }
let export_pre_goals Proof.{ sigma; goals; stack; shelf; given_up } process =
let process = List.map (process sigma) in
{ Interface.fg_goals = process goals
; Interface.bg_goals = List.(map (fun (lg,rg) -> process lg, process rg)) stack
; Interface.shelved_goals = process shelf
; Interface.given_up_goals = process given_up
}
let goals () =
let doc = get_doc () in
set_doc @@ Stm.finish ~doc;
try
let newp = Vernacstate.Proof_global.give_me_the_proof () in
if Proof_diffs.show_diffs () then begin
let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
let diff_goal_map = Proof_diffs.make_goal_map oldp newp in
Some (export_pre_goals Proof.(data newp) (process_goal_diffs diff_goal_map oldp))
end else
Some (export_pre_goals Proof.(data newp) process_goal)
with Vernacstate.Proof_global.NoCurrentProof -> None
[@@ocaml.warning "-3"];;
let evars () =
try
let doc = get_doc () in
set_doc @@ Stm.finish ~doc;
let pfts = Vernacstate.Proof_global.give_me_the_proof () in
let Proof.{ sigma } = Proof.data 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 Vernacstate.Proof_global.NoCurrentProof -> None
[@@ocaml.warning "-3"]
let hints () =
try
let pfts = Vernacstate.Proof_global.give_me_the_proof () in
let Proof.{ goals; sigma } = Proof.data pfts in
match goals with
| [] -> None
| g :: _ ->
let env = Goal.V82.env 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, concl_next_tac)
with Vernacstate.Proof_global.NoCurrentProof -> None
[@@ocaml.warning "-3"]
(** 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 (Vernacstate.Proof_global.get_current_proof_name ()))
with Vernacstate.Proof_global.NoCurrentProof -> None
in
let allproofs =
let l = Vernacstate.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 ());
}
[@@ocaml.warning "-3"]
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 =
let env = Global.env () in
let sigma = Evd.from_env env in
Pp.string_of_ppcmds (pr_lconstr_env env sigma 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.from_env env) constr in
pat
let dirpath_of_string_list s =
let path = String.concat "." s in
let qid = Pcoq.parse_string Pcoq.Constr.global path 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 =
let pstate = Vernacstate.Proof_global.get () in
List.map export_coq_object (Search.interface_search ?pstate (
List.map (fun (c, b) -> (import_search_constraint c, b)) flags)
)
[@@ocaml.warning "-3"]
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 open Goptions in
let iter (name, value) = match import_option_value value with
| BoolValue b -> set_bool_option_value name b
| IntValue i -> set_int_option_value name i
| StringValue s -> set_string_option_value name s
| StringOptValue (Some s) -> set_string_option_value name s
| StringOptValue None -> 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 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
| 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 [coqidetop] 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 Control.protect_sigalrm (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 ~opts:_ ~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 ->
if String.length x > 0 && x.[0] = '-' then
(prerr_endline ("Unknown option " ^ x); exit 1)
else
x :: parse rest
| [] -> []
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"
let islave_init ~opts extra_args =
let args = parse extra_args in
CoqworkmgrApi.(init High);
opts, args
let () =
let open Coqtop in
let custom = { init = islave_init; run = loop; opts = Coqargs.default } in
start_coq custom
¤ Dauer der Verarbeitung: 0.68 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
