From 753b8f4aaa78fe1cf8ea033d8cf45e88b5da9d13 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 25 Jun 2014 17:04:35 +0200 Subject: all coqide specific files moved into ide/ lib/interface split into: - lib/feedback subscribe-based feedback bus (also used by coqidetop) - ide/interface definition of coqide protocol messages lib/pp structured info/err/warn messages lib/serialize split into: - lib/serialize generic xml serialization (list, pairs, int, loc, ...) used by coqide but potentially useful to other interfaces - ide/xmlprotocol serialization of protocol messages as in ide/interface the only drawback is that coqidetop needs -thread and I had to pass that option to all files in ide/ --- Makefile.build | 4 +- Makefile.common | 9 +- checker/check.mllib | 3 +- dev/printers.mllib | 2 + grammar/grammar.mllib | 3 +- ide/coq.ml | 56 ++-- ide/coq.mli | 2 +- ide/coqOps.ml | 15 +- ide/coqide.ml | 2 +- ide/coqidetop.mllib | 2 + ide/ide.mllib | 1 + ide/ide_slave.ml | 460 ++++++++++++++++++++++++++ ide/ideutils.ml | 12 +- ide/ideutils.mli | 4 +- ide/interface.mli | 233 ++++++++++++++ ide/wg_MessageView.ml | 8 +- ide/wg_MessageView.mli | 2 +- ide/xmlprotocol.ml | 701 ++++++++++++++++++++++++++++++++++++++++ ide/xmlprotocol.mli | 56 ++++ idetop/coqidetop.mllib | 1 - idetop/ide_slave.ml | 453 -------------------------- interp/dumpglob.ml | 4 +- intf/vernacexpr.mli | 2 +- kernel/term_typing.ml | 2 +- lib/clib.mllib | 5 +- lib/feedback.ml | 96 ++++++ lib/feedback.mli | 36 +++ lib/interface.mli | 267 --------------- lib/pp.ml | 59 +++- lib/pp.mli | 24 +- lib/serialize.ml | 803 +--------------------------------------------- lib/serialize.mli | 79 ++--- library/goptions.ml | 17 +- library/goptions.mli | 17 +- stm/lemmas.ml | 4 +- stm/stm.ml | 42 ++- stm/stm.mli | 2 +- tools/fake_ide.ml | 28 +- toplevel/coqinit.ml | 2 +- toplevel/coqtop.ml | 2 - toplevel/search.ml | 29 +- toplevel/search.mli | 23 +- toplevel/vernacentries.ml | 8 +- 43 files changed, 1867 insertions(+), 1713 deletions(-) create mode 100644 ide/coqidetop.mllib create mode 100644 ide/ide_slave.ml create mode 100644 ide/interface.mli create mode 100644 ide/xmlprotocol.ml create mode 100644 ide/xmlprotocol.mli delete mode 100644 idetop/coqidetop.mllib delete mode 100644 idetop/ide_slave.ml create mode 100644 lib/feedback.ml create mode 100644 lib/feedback.mli delete mode 100644 lib/interface.mli diff --git a/Makefile.build b/Makefile.build index 0f05dc606..6bd638656 100644 --- a/Makefile.build +++ b/Makefile.build @@ -293,7 +293,7 @@ plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ)) # target to build CoqIde coqide: coqide-files coqide-binaries theories/Init/Prelude.vo -COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES) +COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES) -thread .SUFFIXES:.vo @@ -536,7 +536,7 @@ $(COQDOC): $(patsubst %.cma,%$(BESTLIB),$(COQDOCCMO:.cmo=$(BESTOBJ))) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqtop -ideslave -$(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_printer$(BESTOBJ) lib/errors$(BESTOBJ) lib/spawn$(BESTOBJ) ide/document$(BESTOBJ) tools/fake_ide$(BESTOBJ) +$(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_printer$(BESTOBJ) lib/errors$(BESTOBJ) lib/spawn$(BESTOBJ) ide/document$(BESTOBJ) ide/xmlprotocol$(BESTOBJ) tools/fake_ide$(BESTOBJ) $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml,-I ide,str unix) diff --git a/Makefile.common b/Makefile.common index 4b6cc764a..8a70273ad 100644 --- a/Makefile.common +++ b/Makefile.common @@ -72,11 +72,10 @@ PLUGINS:=\ SRCDIRS:=\ $(CORESRCDIRS) \ - tools tools/coqdoc idetop\ + tools tools/coqdoc \ $(addprefix plugins/, $(PLUGINS)) -IDESRCDIRS:=\ - config lib ide/utils ide +IDESRCDIRS:= $(CORESRCDIRS) ide ide/utils # Order is relevent here because kernel and checker contain files # with the same name @@ -214,7 +213,7 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cma=.cmxa) IDEDEPS:=lib/clib.cma lib/xml_lexer.cmo lib/xml_parser.cmo lib/xml_printer.cmo lib/errors.cmo lib/spawn.cmo IDECMA:=ide/ide.cma -IDETOPLOOPCMA=idetop/coqidetop.cma +IDETOPLOOPCMA=ide/coqidetop.cma LINKIDE:=$(IDEDEPS) $(IDECMA) ide/coqide_main.ml LINKIDEOPT:=$(IDEOPTDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.ml @@ -227,7 +226,7 @@ IDEMOD:=$(shell cat ide/ide.mllib) # coqmktop, coqc -COQENVCMO:=lib/clib.cma lib/loc.cmo lib/errors.cmo +COQENVCMO:=lib/clib.cma lib/errors.cmo COQMKTOPCMO:=$(COQENVCMO) tools/tolink.cmo tools/coqmktop.cmo diff --git a/checker/check.mllib b/checker/check.mllib index 766eb4182..cbabd208c 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -15,8 +15,9 @@ Backtrace Flags Control Pp_control -Pp Loc +Serialize +Pp Segmenttree Unicodetable Unicode diff --git a/dev/printers.mllib b/dev/printers.mllib index 81fcc8493..dcd3f0efb 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -18,6 +18,8 @@ Loc Compat Flags Control +Loc +Serialize Pp Segmenttree Unicodetable diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 338d44fbf..a18951f4b 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -14,8 +14,9 @@ Exninfo Backtrace Pp_control Flags -Pp Loc +Serialize +Pp Errors CList CString diff --git a/ide/coq.ml b/ide/coq.ml index af00cc63c..c1555e57f 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -177,7 +177,7 @@ type void = Void Reference: http://alan.petitepomme.net/cwn/2004.01.13.html To rewrite someday with GADT. *) -type 'a poly_ccb = 'a Serialize.call * ('a Interface.value -> void) +type 'a poly_ccb = 'a Xmlprotocol.call * ('a Interface.value -> void) type 't scoped_ccb = { bind_ccb : 'a. 'a poly_ccb -> 't } type ccb = { open_ccb : 't. 't scoped_ccb -> 't } @@ -234,7 +234,7 @@ type coqtop = { (* called whenever coqtop dies *) mutable reset_handler : reset_kind -> unit task; (* called whenever coqtop sends a feedback message *) - mutable feedback_handler : Interface.feedback -> unit; + mutable feedback_handler : Feedback.feedback -> unit; (* actual coqtop process and its status *) mutable handle : handle; mutable status : status; @@ -296,22 +296,22 @@ let rec check_errors = function | `OUT :: _ -> raise (TubeError "OUT") let handle_intermediate_message handle xml = - let message = Serialize.to_message xml in - let level = message.Interface.message_level in - let content = message.Interface.message_content in + let message = Pp.to_message xml in + let level = message.Pp.message_level in + let content = message.Pp.message_content in let logger = match handle.waiting_for with | Some (_, l) -> l | None -> function - | Interface.Error -> Minilib.log ~level:`ERROR - | Interface.Info -> Minilib.log ~level:`INFO - | Interface.Notice -> Minilib.log ~level:`NOTICE - | Interface.Warning -> Minilib.log ~level:`WARNING - | Interface.Debug _ -> Minilib.log ~level:`DEBUG + | Pp.Error -> Minilib.log ~level:`ERROR + | Pp.Info -> Minilib.log ~level:`INFO + | Pp.Notice -> Minilib.log ~level:`NOTICE + | Pp.Warning -> Minilib.log ~level:`WARNING + | Pp.Debug _ -> Minilib.log ~level:`DEBUG in logger level content let handle_feedback feedback_processor xml = - let feedback = Serialize.to_feedback xml in + let feedback = Feedback.to_feedback xml in feedback_processor feedback let handle_final_answer handle xml = @@ -320,7 +320,7 @@ let handle_final_answer handle xml = | None -> raise (AnswerWithoutRequest (Xml_printer.to_string_fmt xml)) | Some (c, _) -> c in let () = handle.waiting_for <- None in - with_ccb ccb { bind_ccb = fun (c, f) -> f (Serialize.to_answer c xml) } + with_ccb ccb { bind_ccb = fun (c, f) -> f (Xmlprotocol.to_answer c xml) } type input_state = { mutable fragment : string; @@ -340,10 +340,10 @@ let unsafe_handle_input handle feedback_processor state conds ~read_all = let l_end = Lexing.lexeme_end lex in state.fragment <- String.sub s l_end (String.length s - l_end); state.lexerror <- None; - if Serialize.is_message xml then begin + if Pp.is_message xml then begin handle_intermediate_message handle xml; loop () - end else if Serialize.is_feedback xml then begin + end else if Feedback.is_feedback xml then begin handle_feedback feedback_processor xml; loop () end else begin @@ -501,22 +501,22 @@ type 'a query = 'a Interface.value task let eval_call ?(logger=default_logger) call handle k = (** Send messages to coqtop and prepare the decoding of the answer *) - Minilib.log ("Start eval_call " ^ Serialize.pr_call call); + Minilib.log ("Start eval_call " ^ Xmlprotocol.pr_call call); assert (handle.alive && handle.waiting_for = None); handle.waiting_for <- Some (mk_ccb (call,k), logger); - Xml_printer.print handle.xml_oc (Serialize.of_call call); + Xml_printer.print handle.xml_oc (Xmlprotocol.of_call call); Minilib.log "End eval_call"; Void -let add ?(logger=default_logger) x = eval_call ~logger (Serialize.add x) -let edit_at i = eval_call (Serialize.edit_at i) -let query ?(logger=default_logger) x = eval_call ~logger (Serialize.query x) -let mkcases s = eval_call (Serialize.mkcases s) -let status ?logger force = eval_call ?logger (Serialize.status force) -let hints x = eval_call (Serialize.hints x) -let search flags = eval_call (Serialize.search flags) -let init x = eval_call (Serialize.init x) -let stop_worker x = eval_call (Serialize.stop_worker x) +let add ?(logger=default_logger) x = eval_call ~logger (Xmlprotocol.add x) +let edit_at i = eval_call (Xmlprotocol.edit_at i) +let query ?(logger=default_logger) x = eval_call ~logger (Xmlprotocol.query x) +let mkcases s = eval_call (Xmlprotocol.mkcases s) +let status ?logger force = eval_call ?logger (Xmlprotocol.status force) +let hints x = eval_call (Xmlprotocol.hints x) +let search flags = eval_call (Xmlprotocol.search flags) +let init x = eval_call (Xmlprotocol.init x) +let stop_worker x = eval_call (Xmlprotocol.stop_worker x) module PrintOpt = struct @@ -573,7 +573,7 @@ struct let mkopt o v acc = (o, Interface.BoolValue v) :: acc in let opts = Hashtbl.fold mkopt current_state [] in let opts = (width, Interface.IntValue !width_state) :: opts in - eval_call (Serialize.set_options opts) h + eval_call (Xmlprotocol.set_options opts) h (function | Interface.Good () -> k () | _ -> failwith "Cannot set options. Resetting coqtop") @@ -581,7 +581,7 @@ struct end let goals ?logger x h k = - PrintOpt.enforce h (fun () -> eval_call ?logger (Serialize.goals x) h k) + PrintOpt.enforce h (fun () -> eval_call ?logger (Xmlprotocol.goals x) h k) let evars x h k = - PrintOpt.enforce h (fun () -> eval_call (Serialize.evars x) h k) + PrintOpt.enforce h (fun () -> eval_call (Xmlprotocol.evars x) h k) diff --git a/ide/coq.mli b/ide/coq.mli index 542cc4462..966c77700 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -63,7 +63,7 @@ val spawn_coqtop : string list -> coqtop val set_reset_handler : coqtop -> (reset_kind -> unit task) -> unit (** Register a handler called when a coqtop dies (badly or on purpose) *) -val set_feedback_handler : coqtop -> (Interface.feedback -> unit) -> unit +val set_feedback_handler : coqtop -> (Feedback.feedback -> unit) -> unit (** Register a handler called when coqtop sends a feedback message *) val init_coqtop : coqtop -> unit task -> unit diff --git a/ide/coqOps.ml b/ide/coqOps.ml index ab1a86f78..cefe18092 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -10,6 +10,7 @@ open Util open Coq open Ideutils open Interface +open Feedback type flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR of string ] type mem_flag = [ `INCOMPLETE | `UNSAFE | `PROCESSING | `ERROR ] @@ -422,7 +423,7 @@ object(self) self#position_error_tag_at_iter start phrase loc; buffer#place_cursor ~where:stop; messages#clear; - messages#push Error msg; + messages#push Pp.Error msg; self#show_goals end else self#show_goals_aux ~move_insert:true () @@ -511,7 +512,7 @@ object(self) let handle_answer = function | Good (id, (Util.Inl (* NewTip *) (), msg)) -> Doc.assign_tip_id document id; - logger Notice msg; + logger Pp.Notice msg; self#commit_queue_transaction sentence; loop id [] | Good (id, (Util.Inr (* Unfocus *) tip, msg)) -> @@ -519,7 +520,7 @@ object(self) let topstack, _ = Doc.context document in self#exit_focus; self#cleanup (Doc.cut_at document tip); - logger Notice msg; + logger Pp.Notice msg; self#mark_as_needed sentence; if Queue.is_empty queue then loop tip [] else loop tip (List.rev topstack) @@ -538,7 +539,7 @@ object(self) let next = function | Good _ -> messages#clear; - messages#push Info "Doc checked"; + messages#push Pp.Info "Doc checked"; Coq.return () | Fail x -> self#handle_failure x in Coq.bind (Coq.status ~logger:messages#push true) next @@ -628,8 +629,8 @@ object(self) self#cleanup (Doc.cut_at document to_id); conclusion () | Fail (safe_id, loc, msg) -> - if loc <> None then messages#push Error "Fixme LOC"; - messages#push Error msg; + if loc <> None then messages#push Pp.Error "Fixme LOC"; + messages#push Pp.Error msg; if Stateid.equal safe_id Stateid.dummy then self#show_goals else undo safe_id (Doc.focused document && Doc.is_in_focus document safe_id)) @@ -647,7 +648,7 @@ object(self) ?(move_insert=false) (safe_id, (loc : (int * int) option), msg) = messages#clear; - messages#push Error msg; + messages#push Pp.Error msg; ignore(self#process_feedback ()); if Stateid.equal safe_id Stateid.dummy then Coq.lift (fun () -> ()) else diff --git a/ide/coqide.ml b/ide/coqide.ml index e20c95b9e..9614c6f3b 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -739,7 +739,7 @@ let coqtop_arguments sn = let args = String.concat " " args in let msg = Printf.sprintf "Invalid arguments: %s" args in let () = sn.messages#clear in - sn.messages#push Interface.Error msg + sn.messages#push Pp.Error msg else dialog#destroy () in let _ = entry#connect#activate ok_cb in diff --git a/ide/coqidetop.mllib b/ide/coqidetop.mllib new file mode 100644 index 000000000..92301dc30 --- /dev/null +++ b/ide/coqidetop.mllib @@ -0,0 +1,2 @@ +Xmlprotocol +Ide_slave diff --git a/ide/ide.mllib b/ide/ide.mllib index 8bc1337ff..944476171 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -15,6 +15,7 @@ Utf8_convert Preferences Project_file Ideutils +Xmlprotocol Coq Coq_lex Sentence diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml new file mode 100644 index 000000000..6b2c52123 --- /dev/null +++ b/ide/ide_slave.ml @@ -0,0 +1,460 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + flush_all (); + Pp_control.std_ft := out_ft; + Pp_control.err_ft := out_ft; + Pp_control.deep_ft := deep_out_ft; + ), + (fun () -> Format.pp_print_flush out_ft (); + let r = Buffer.contents out_buff in + Buffer.clear out_buff; r) + +let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) 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"]] + +let is_known_option cmd = match cmd with + | VernacSetOption (o,BoolValue true) + | VernacUnsetOption o -> coqide_known_option o + | _ -> false + +let is_debug cmd = match cmd with + | VernacSetOption (["Ltac";"Debug"], _) -> true + | _ -> false + +let is_query cmd = match cmd with + | VernacChdir None + | VernacMemOption _ + | VernacPrintOption _ + | VernacCheckMayEval _ + | VernacGlobalCheck _ + | VernacPrint _ + | VernacSearch _ + | VernacLocate _ -> true + | _ -> false + +let is_undo cmd = match cmd with + | VernacUndo _ | VernacUndoTo _ -> true + | _ -> false + +(** Check whether a command is forbidden by CoqIDE *) + +let coqide_cmd_checks (loc,ast) = + let user_error s = Errors.user_err_loc (loc, "CoqIde", str s) in + if is_debug ast then + user_error "Debug mode not available within CoqIDE"; + if is_known_option ast then + msg_warning (strbrk"This will not work. Use CoqIDE display menu instead"); + if Vernac.is_navigation_vernac ast || is_undo ast then + msg_warning (strbrk "Rather use CoqIDE navigation instead"); + if is_query ast then + msg_warning (strbrk "Query commands should not be inserted in scripts") + +(** Interpretation (cf. [Ide_intf.interp]) *) + +let add ((s,eid),(sid,verbose)) = + let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in + let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in + newid, (rc, read_stdout ()) + +let edit_at id = + match Stm.edit_at id with + | `NewTip -> CSig.Inl () + | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip)) + +let query (s,id) = Stm.query ~at:id s; read_stdout () + +(** Goal display *) + +let hyp_next_tac sigma env (id,_,ast) = + let id_s = Names.Id.to_string id in + let type_s = string_of_ppcmds (pr_ltype_env env 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 id = Goal.uid g in + let ccl = + let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in + string_of_ppcmds (pr_goal_concl_style_env env norm_constr) in + let process_hyp h_env d acc = + let d = Context.map_named_declaration (Reductionops.nf_evar sigma) d in + (string_of_ppcmds (pr_var_decl h_env d)) :: acc in + let hyps = + List.rev (Environ.fold_named_context process_hyp env ~init: []) in + { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } + +let goals () = + Stm.finish (); + let s = read_stdout () in + if not (String.is_empty s) then msg_info (str s); + try + let pfts = Proof_global.give_me_the_proof () in + let (goals, zipper, shelf, given_up, sigma) = Proof.proof pfts in + let fg = List.map (process_goal sigma) goals in + let map_zip (lg, rg) = + let lg = List.map (process_goal sigma) lg in + let rg = List.map (process_goal sigma) rg in + (lg, rg) + in + let bg = List.map map_zip zipper in + let shelf = List.map (process_goal sigma) shelf in + let given_up = List.map (process_goal sigma) given_up in + Some { Interface.fg_goals = fg; + Interface.bg_goals = bg; + shelved_goals = shelf; + given_up_goals = given_up; } + with Proof_global.NoCurrentProof -> None + +let evars () = + try + Stm.finish (); + let s = read_stdout () in + if not (String.is_empty s) then msg_info (str s); + let pfts = Proof_global.give_me_the_proof () in + let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in + let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in + let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar 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 { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals 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 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) *) + Stm.finish (); + if force then Stm.join (); + let s = read_stdout () in + if not (String.is_empty s) then msg_info (str s); + 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 (); + } + +let search flags = Search.interface_search flags + +let get_options () = + let table = Goptions.get_tables () in + let fold key state accu = (key, state) :: accu in + Goptions.OptionMap.fold fold table [] + +let set_options options = + let iter (name, value) = match 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 + 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 = + let dummy = Stateid.dummy in + let loc_of e = match Loc.get_loc e with + | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc) + | _ -> None in + let mk_msg e = read_stdout ()^"\n"^string_of_ppcmds (Errors.print e) in + match e with + | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!" + | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!" + | e -> + match Stateid.get e with + | Some (valid, _) -> valid, loc_of e, mk_msg e + | None -> dummy, loc_of e, mk_msg e + +let init = + let initialized = ref false in + fun file -> + if !initialized then anomaly (str "Already initialized") + else begin + initialized := true; + match file with + | None -> Stm.get_current_state () + | Some file -> + let dir = Filename.dirname file in + let open Loadpath in let open CUnix in + let initial_id, _ = + if not (is_in_load_paths (physical_path_of_string dir)) then + Stm.add false ~ontop:(Stm.get_current_state ()) + 0 (Printf.sprintf "Add LoadPath \"%s\". " dir) + else Stm.get_current_state (), `NewTip in + Stm.set_compilation_hints file; + initial_id + end + +(* Retrocompatibility stuff *) +let interp ((_raw, verbose), s) = + let vernac_parse s = + let pa = Pcoq.Gram.parsable (Stream.of_string s) in + Flags.with_option Flags.we_are_parsing (fun () -> + match Pcoq.Gram.entry_parse Pcoq.main_entry pa with + | None -> raise (Invalid_argument "vernac_parse") + | Some ast -> ast) + () in + Stm.interp verbose (vernac_parse s); + Stm.get_current_state (), CSig.Inl (read_stdout ()) + +(** 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 + +(** Grouping all call handlers together + error handling *) + +let eval_call xml_oc log c = + let interruptible f x = + catch_break := true; + Control.check_for_interrupt (); + let r = f x in + catch_break := false; + let out = read_stdout () in + if not (String.is_empty out) then log (str out); + 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.interp = interruptible interp; + Interface.handle_exn = handle_exn; + Interface.stop_worker = Stm.stop_worker; + } 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 = Errors.push e in Mutex.unlock m; raise e + + +let slave_logger xml_oc level message = + (* convert the message into XML *) + let msg = string_of_ppcmds (hov 0 message) in + let message = { + Pp.message_level = level; + Pp.message_content = msg; + } in + let () = pr_debug (Printf.sprintf "-> %S" msg) in + let xml = Pp.of_message message in + print_xml xml_oc xml + +let slave_feeder xml_oc msg = + let xml = Feedback.of_feedback 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 loop () = + 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 + CThread.prepare_in_channel_for_thread_friendly_io in_ch; + let in_lb = Lexing.from_function (fun s len -> + CThread.thread_friendly_read in_ch s ~off:0 ~len) in + let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in + let () = Xml_parser.check_eof xml_ic false in + set_logger (slave_logger xml_oc); + set_feeder (slave_feeder xml_oc); + (* We'll handle goal fetching and display in our own way *) + Vernacentries.enable_goal_printing := false; + Vernacentries.qed_display_script := false; + Flags.make_term_color false; + 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 q = Xmlprotocol.to_call xml_query in + let () = pr_debug_call q in + let r = eval_call xml_oc (slave_logger xml_oc Pp.Notice) 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 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_debug ("Syntax error in query: " ^ Xml_parser.error_msg err); + exit 1 + | Serialize.Marshal_error -> + pr_debug "Incorrect query."; + exit 1 + | 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 + | x :: rest -> x :: parse rest + | [] -> [] + +let () = Coqtop.toploop_init := (fun args -> + let args = parse args in + Flags.make_silent true; + init_stdout (); + args) + +let () = Coqtop.toploop_run := loop diff --git a/ide/ideutils.ml b/ide/ideutils.ml index d8ca34f98..32d2bb97b 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -272,15 +272,15 @@ let textview_width (view : #GText.view_skel) = let char_width = GPango.to_pixels metrics#approx_char_width in pixel_width / char_width -type logger = Interface.message_level -> string -> unit +type logger = Pp.message_level -> string -> unit let default_logger level message = let level = match level with - | Interface.Debug _ -> `DEBUG - | Interface.Info -> `INFO - | Interface.Notice -> `NOTICE - | Interface.Warning -> `WARNING - | Interface.Error -> `ERROR + | Pp.Debug _ -> `DEBUG + | Pp.Info -> `INFO + | Pp.Notice -> `NOTICE + | Pp.Warning -> `WARNING + | Pp.Error -> `ERROR in Minilib.log ~level message diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 5fd97e3a5..5877d1270 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -69,9 +69,9 @@ val requote : string -> string val textview_width : #GText.view_skel -> int (** Returns an approximate value of the character width of a textview *) -type logger = Interface.message_level -> string -> unit +type logger = Pp.message_level -> string -> unit -val default_logger : Interface.message_level -> string -> unit +val default_logger : Pp.message_level -> string -> unit (** Default logger. It logs messages that the casual user should not see. *) (** {6 I/O operations} *) diff --git a/ide/interface.mli b/ide/interface.mli new file mode 100644 index 000000000..4e5e4a9cd --- /dev/null +++ b/ide/interface.mli @@ -0,0 +1,233 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* add_rty; + edit_at : edit_at_sty -> edit_at_rty; + query : query_sty -> query_rty; + goals : goals_sty -> goals_rty; + evars : evars_sty -> evars_rty; + hints : hints_sty -> hints_rty; + status : status_sty -> status_rty; + search : search_sty -> search_rty; + get_options : get_options_sty -> get_options_rty; + set_options : set_options_sty -> set_options_rty; + mkcases : mkcases_sty -> mkcases_rty; + about : about_sty -> about_rty; + stop_worker : stop_worker_sty -> stop_worker_rty; + handle_exn : handle_exn_sty -> handle_exn_rty; + init : init_sty -> init_rty; + quit : quit_sty -> quit_rty; + (* Retrocompatibility stuff *) + interp : interp_sty -> interp_rty; +} + diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index f58cdc647..cd3e31135 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -12,7 +12,7 @@ class type message_view = method clear : unit method add : string -> unit method set : string -> unit - method push : Interface.message_level -> string -> unit + method push : Pp.message_level -> string -> unit (** same as [add], but with an explicit level instead of [Notice] *) method buffer : GText.buffer (** for more advanced text edition *) @@ -43,8 +43,8 @@ let message_view () : message_view = method push level msg = let tags = match level with - | Interface.Error -> [Tags.Message.error] - | Interface.Warning -> [Tags.Message.warning] + | Pp.Error -> [Tags.Message.error] + | Pp.Warning -> [Tags.Message.warning] | _ -> [] in if msg <> "" then begin @@ -52,7 +52,7 @@ let message_view () : message_view = buffer#insert ~tags "\n" end - method add msg = self#push Interface.Notice msg + method add msg = self#push Pp.Notice msg method set msg = self#clear; self#add msg diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index cb84ae733..8a0a2bd85 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -12,7 +12,7 @@ class type message_view = method clear : unit method add : string -> unit method set : string -> unit - method push : Interface.message_level -> string -> unit + method push : Pp.message_level -> string -> unit (** same as [add], but with an explicit level instead of [Notice] *) method buffer : GText.buffer (** for more advanced text edition *) diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml new file mode 100644 index 000000000..09626172d --- /dev/null +++ b/ide/xmlprotocol.ml @@ -0,0 +1,701 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + constructor "search_cst" "name_pattern" [of_string s] + | Type_Pattern s -> + constructor "search_cst" "type_pattern" [of_string s] + | SubType_Pattern s -> + constructor "search_cst" "subtype_pattern" [of_string s] + | In_Module m -> + constructor "search_cst" "in_module" [of_list of_string m] + | Include_Blacklist -> + constructor "search_cst" "include_blacklist" [] +let to_search_cst = do_match "search_cst" (fun s args -> match s with + | "name_pattern" -> Name_Pattern (to_string (singleton args)) + | "type_pattern" -> Type_Pattern (to_string (singleton args)) + | "subtype_pattern" -> SubType_Pattern (to_string (singleton args)) + | "in_module" -> In_Module (to_list to_string (singleton args)) + | "include_blacklist" -> Include_Blacklist + | _ -> raise Marshal_error) + +let of_coq_object f ans = + let prefix = of_list of_string ans.coq_object_prefix in + let qualid = of_list of_string ans.coq_object_qualid in + let obj = f ans.coq_object_object in + Element ("coq_object", [], [prefix; qualid; obj]) + +let to_coq_object f = function +| Element ("coq_object", [], [prefix; qualid; obj]) -> + let prefix = to_list to_string prefix in + let qualid = to_list to_string qualid in + let obj = f obj in { + coq_object_prefix = prefix; + coq_object_qualid = qualid; + coq_object_object = obj; + } +| _ -> raise Marshal_error + +let of_option_value = function + | IntValue i -> constructor "option_value" "intvalue" [of_option of_int i] + | BoolValue b -> constructor "option_value" "boolvalue" [of_bool b] + | StringValue s -> constructor "option_value" "stringvalue" [of_string s] +let to_option_value = do_match "option_value" (fun s args -> match s with + | "intvalue" -> IntValue (to_option to_int (singleton args)) + | "boolvalue" -> BoolValue (to_bool (singleton args)) + | "stringvalue" -> StringValue (to_string (singleton args)) + | _ -> raise Marshal_error) + +let of_option_state s = + Element ("option_state", [], [ + of_bool s.opt_sync; + of_bool s.opt_depr; + of_string s.opt_name; + of_option_value s.opt_value]) +let to_option_state = function + | Element ("option_state", [], [sync; depr; name; value]) -> { + opt_sync = to_bool sync; + opt_depr = to_bool depr; + opt_name = to_string name; + opt_value = to_option_value value } + | _ -> raise Marshal_error + + +let of_value f = function +| Good x -> Element ("value", ["val", "good"], [f x]) +| Fail (id,loc, msg) -> + let loc = match loc with + | None -> [] + | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in + let id = Stateid.to_xml id in + Element ("value", ["val", "fail"] @ loc, [id;PCData msg]) +let to_value f = function +| Element ("value", attrs, l) -> + let ans = massoc "val" attrs in + if ans = "good" then Good (f (singleton l)) + else if ans = "fail" then + let loc = + try + let loc_s = int_of_string (Serialize.massoc "loc_s" attrs) in + let loc_e = int_of_string (Serialize.massoc "loc_e" attrs) in + Some (loc_s, loc_e) + with Marshal_error | Failure _ -> None + in + let id = Stateid.of_xml (List.hd l) in + let msg = raw_string (List.tl l) in + Fail (id, loc, msg) + else raise Marshal_error +| _ -> raise Marshal_error + +let of_status s = + let of_so = of_option of_string in + let of_sl = of_list of_string in + Element ("status", [], [ + of_sl s.status_path; + of_so s.status_proofname; + of_sl s.status_allproofs; + of_int s.status_proofnum; ]) +let to_status = function + | Element ("status", [], [path; name; prfs; pnum]) -> { + status_path = to_list to_string path; + status_proofname = to_option to_string name; + status_allproofs = to_list to_string prfs; + status_proofnum = to_int pnum; } + | _ -> raise Marshal_error + +let of_evar s = Element ("evar", [], [PCData s.evar_info]) +let to_evar = function + | Element ("evar", [], data) -> { evar_info = raw_string data; } + | _ -> raise Marshal_error + +let of_goal g = + let hyp = of_list of_string g.goal_hyp in + let ccl = of_string g.goal_ccl in + let id = of_string g.goal_id in + Element ("goal", [], [id; hyp; ccl]) +let to_goal = function + | Element ("goal", [], [id; hyp; ccl]) -> + let hyp = to_list to_string hyp in + let ccl = to_string ccl in + let id = to_string id in + { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } + | _ -> raise Marshal_error + +let of_goals g = + let of_glist = of_list of_goal in + let fg = of_list of_goal g.fg_goals in + let bg = of_list (of_pair of_glist of_glist) g.bg_goals in + let shelf = of_list of_goal g.shelved_goals in + let given_up = of_list of_goal g.given_up_goals in + Element ("goals", [], [fg; bg; shelf; given_up]) +let to_goals = function + | Element ("goals", [], [fg; bg; shelf; given_up]) -> + let to_glist = to_list to_goal in + let fg = to_list to_goal fg in + let bg = to_list (to_pair to_glist to_glist) bg in + let shelf = to_list to_goal shelf in + let given_up = to_list to_goal given_up in + { fg_goals = fg; bg_goals = bg; shelved_goals = shelf; given_up_goals = given_up } + | _ -> raise Marshal_error + +let of_coq_info info = + let version = of_string info.coqtop_version in + let protocol = of_string info.protocol_version in + let release = of_string info.release_date in + let compile = of_string info.compile_date in + Element ("coq_info", [], [version; protocol; release; compile]) +let to_coq_info = function + | Element ("coq_info", [], [version; protocol; release; compile]) -> { + coqtop_version = to_string version; + protocol_version = to_string protocol; + release_date = to_string release; + compile_date = to_string compile; } + | _ -> raise Marshal_error + +end +include Xml_marshalling + +(* Reification of basic types and type constructors, and functions + from to xml *) +module ReifType : sig + + type 'a val_t + + val unit_t : unit val_t + val string_t : string val_t + val int_t : int val_t + val bool_t : bool val_t + + val option_t : 'a val_t -> 'a option val_t + val list_t : 'a val_t -> 'a list val_t + val pair_t : 'a val_t -> 'b val_t -> ('a * 'b) val_t + val union_t : 'a val_t -> 'b val_t -> ('a ,'b) union val_t + + val goals_t : goals val_t + val evar_t : evar val_t + val state_t : status val_t + val option_state_t : option_state val_t + val option_value_t : option_value val_t + val coq_info_t : coq_info val_t + val coq_object_t : 'a val_t -> 'a coq_object val_t + val state_id_t : state_id val_t + val search_cst_t : search_constraint val_t + + val of_value_type : 'a val_t -> 'a -> xml + val to_value_type : 'a val_t -> xml -> 'a + + val print : 'a val_t -> 'a -> string + + type value_type + val erase : 'a val_t -> value_type + val print_type : value_type -> string + + val document_type_encoding : (xml -> string) -> unit + +end = struct + + type value_type = + | Unit | String | Int | Bool + + | Option of value_type + | List of value_type + | Pair of value_type * value_type + | Union of value_type * value_type + + | Goals | Evar | State | Option_state | Option_value | Coq_info + | Coq_object of value_type + | State_id + | Search_cst + + type 'a val_t = value_type + + let erase (x : 'a val_t) : value_type = x + + let unit_t = Unit + let string_t = String + let int_t = Int + let bool_t = Bool + + let option_t x = Option x + let list_t x = List x + let pair_t x y = Pair (x, y) + let union_t x y = Union (x, y) + + let goals_t = Goals + let evar_t = Evar + let state_t = State + let option_state_t = Option_state + let option_value_t = Option_value + let coq_info_t = Coq_info + let coq_object_t x = Coq_object x + let state_id_t = State_id + let search_cst_t = Search_cst + + let of_value_type (ty : 'a val_t) : 'a -> xml = + let rec convert ty : 'a -> xml = match ty with + | Unit -> Obj.magic of_unit + | Bool -> Obj.magic of_bool + | String -> Obj.magic of_string + | Int -> Obj.magic of_int + | State -> Obj.magic of_status + | Option_state -> Obj.magic of_option_state + | Option_value -> Obj.magic of_option_value + | Coq_info -> Obj.magic of_coq_info + | Goals -> Obj.magic of_goals + | Evar -> Obj.magic of_evar + | List t -> Obj.magic (of_list (convert t)) + | Option t -> Obj.magic (of_option (convert t)) + | Coq_object t -> Obj.magic (of_coq_object (convert t)) + | Pair (t1,t2) -> Obj.magic (of_pair (convert t1) (convert t2)) + | Union (t1,t2) -> Obj.magic (of_union (convert t1) (convert t2)) + | State_id -> Obj.magic Stateid.to_xml + | Search_cst -> Obj.magic of_search_cst + in + convert ty + + let to_value_type (ty : 'a val_t) : xml -> 'a = + let rec convert ty : xml -> 'a = match ty with + | Unit -> Obj.magic to_unit + | Bool -> Obj.magic to_bool + | String -> Obj.magic to_string + | Int -> Obj.magic to_int + | State -> Obj.magic to_status + | Option_state -> Obj.magic to_option_state + | Option_value -> Obj.magic to_option_value + | Coq_info -> Obj.magic to_coq_info + | Goals -> Obj.magic to_goals + | Evar -> Obj.magic to_evar + | List t -> Obj.magic (to_list (convert t)) + | Option t -> Obj.magic (to_option (convert t)) + | Coq_object t -> Obj.magic (to_coq_object (convert t)) + | Pair (t1,t2) -> Obj.magic (to_pair (convert t1) (convert t2)) + | Union (t1,t2) -> Obj.magic (to_union (convert t1) (convert t2)) + | State_id -> Obj.magic Stateid.of_xml + | Search_cst -> Obj.magic to_search_cst + in + convert ty + + let pr_unit () = "" + let pr_string s = Printf.sprintf "%S" s + let pr_int i = string_of_int i + let pr_bool b = Printf.sprintf "%B" b + let pr_goal (g : goals) = + if g.fg_goals = [] then + if g.bg_goals = [] then "Proof completed." + else + let rec pr_focus _ = function + | [] -> assert false + | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg) + | (lg, rg) :: l -> + Printf.sprintf "%i:%a" + (List.length lg + List.length rg) pr_focus l in + Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals + else + let pr_menu s = s in + let pr_goal { goal_hyp = hyps; goal_ccl = goal } = + "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ + pr_menu goal ^ "]" in + String.concat " " (List.map pr_goal g.fg_goals) + let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]" + let pr_status (s : status) = + let path = + let l = String.concat "." s.status_path in + "path=" ^ l ^ ";" in + let name = match s.status_proofname with + | None -> "no proof;" + | Some n -> "proof = " ^ n ^ ";" in + "Status: " ^ path ^ name + let pr_coq_info (i : coq_info) = "FIXME" + let pr_option_value = function + | IntValue None -> "none" + | IntValue (Some i) -> string_of_int i + | StringValue s -> s + | BoolValue b -> if b then "true" else "false" + let pr_option_state (s : option_state) = + Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n" + s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value) + let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]" + let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")" + let pr_coq_object (o : 'a coq_object) = "FIXME" + let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")" + let pr_union pr1 pr2 = function Inl x -> "Inl "^pr1 x | Inr x -> "Inr "^pr2 x + + let pr_search_cst = function + | Name_Pattern s -> "Name_Pattern " ^ s + | Type_Pattern s -> "Type_Pattern " ^ s + | SubType_Pattern s -> "SubType_Pattern " ^ s + | In_Module s -> "In_Module " ^ String.concat "." s + | Include_Blacklist -> "Include_Blacklist" + + let rec print = function + | Unit -> Obj.magic pr_unit + | Bool -> Obj.magic pr_bool + | String -> Obj.magic pr_string + | Int -> Obj.magic pr_int + | State -> Obj.magic pr_status + | Option_state -> Obj.magic pr_option_state + | Option_value -> Obj.magic pr_option_value + | Search_cst -> Obj.magic pr_search_cst + | Coq_info -> Obj.magic pr_coq_info + | Goals -> Obj.magic pr_goal + | Evar -> Obj.magic pr_evar + | List t -> Obj.magic (pr_list (print t)) + | Option t -> Obj.magic (pr_option (print t)) + | Coq_object t -> Obj.magic pr_coq_object + | Pair (t1,t2) -> Obj.magic (pr_pair (print t1) (print t2)) + | Union (t1,t2) -> Obj.magic (pr_union (print t1) (print t2)) + | State_id -> Obj.magic pr_int + + (* This is to break if a rename/refactoring makes the strings below outdated *) + type 'a exists = bool + + let rec print_type = function + | Unit -> "unit" + | Bool -> "bool" + | String -> "string" + | Int -> "int" + | State -> assert(true : status exists); "Interface.status" + | Option_state -> assert(true : option_state exists); "Interface.option_state" + | Option_value -> assert(true : option_value exists); "Interface.option_value" + | Search_cst -> assert(true : search_constraint exists); "Interface.search_constraint" + | Coq_info -> assert(true : coq_info exists); "Interface.coq_info" + | Goals -> assert(true : goals exists); "Interface.goals" + | Evar -> assert(true : evar exists); "Interface.evar" + | List t -> Printf.sprintf "(%s list)" (print_type t) + | Option t -> Printf.sprintf "(%s option)" (print_type t) + | Coq_object t -> assert(true : 'a coq_object exists); + Printf.sprintf "(%s Interface.coq_object)" (print_type t) + | Pair (t1,t2) -> Printf.sprintf "(%s * %s)" (print_type t1) (print_type t2) + | Union (t1,t2) -> assert(true : ('a,'b) CSig.union exists); + Printf.sprintf "((%s, %s) CSig.union)" (print_type t1) (print_type t2) + | State_id -> assert(true : Stateid.t exists); "Stateid.t" + + let document_type_encoding pr_xml = + Printf.printf "\n=== Data encoding by examples ===\n\n"; + Printf.printf "%s:\n\n%s\n\n" (print_type Unit) (pr_xml (of_unit ())); + Printf.printf "%s:\n\n%s\n%s\n\n" (print_type Bool) + (pr_xml (of_bool true)) (pr_xml (of_bool false)); + Printf.printf "%s:\n\n%s\n\n" (print_type String) (pr_xml (of_string "hello")); + Printf.printf "%s:\n\n%s\n\n" (print_type Int) (pr_xml (of_int 256)); + Printf.printf "%s:\n\n%s\n\n" (print_type State_id) (pr_xml (Stateid.to_xml Stateid.initial)); + Printf.printf "%s:\n\n%s\n\n" (print_type (List Int)) (pr_xml (of_list of_int [3;4;5])); + Printf.printf "%s:\n\n%s\n%s\n\n" (print_type (Option Int)) + (pr_xml (of_option of_int (Some 3))) (pr_xml (of_option of_int None)); + Printf.printf "%s:\n\n%s\n\n" (print_type (Pair (Bool,Int))) + (pr_xml (of_pair of_bool of_int (false,3))); + Printf.printf "%s:\n\n%s\n\n" (print_type (Union (Bool,Int))) + (pr_xml (of_union of_bool of_int (Inl false))); + print_endline ("All other types are records represented by a node named like the OCaml\n"^ + "type which contains a flattened n-tuple. We provide one example.\n"); + Printf.printf "%s:\n\n%s\n\n" (print_type Option_state) + (pr_xml (of_option_state { opt_sync = true; opt_depr = false; + opt_name = "name1"; opt_value = IntValue (Some 37) })); + +end +open ReifType + +(** Types reification, checked with explicit casts *) +let add_sty_t : add_sty val_t = + pair_t (pair_t string_t int_t) (pair_t state_id_t bool_t) +let edit_at_sty_t : edit_at_sty val_t = state_id_t +let query_sty_t : query_sty val_t = pair_t string_t state_id_t +let goals_sty_t : goals_sty val_t = unit_t +let evars_sty_t : evars_sty val_t = unit_t +let hints_sty_t : hints_sty val_t = unit_t +let status_sty_t : status_sty val_t = bool_t +let search_sty_t : search_sty val_t = list_t (pair_t search_cst_t bool_t) +let get_options_sty_t : get_options_sty val_t = unit_t +let set_options_sty_t : set_options_sty val_t = + list_t (pair_t (list_t string_t) option_value_t) +let mkcases_sty_t : mkcases_sty val_t = string_t +let quit_sty_t : quit_sty val_t = unit_t +let about_sty_t : about_sty val_t = unit_t +let init_sty_t : init_sty val_t = option_t string_t +let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t +let stop_worker_sty_t : stop_worker_sty val_t = int_t + +let add_rty_t : add_rty val_t = + pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t) +let edit_at_rty_t : edit_at_rty val_t = + union_t unit_t (pair_t state_id_t (pair_t state_id_t state_id_t)) +let query_rty_t : query_rty val_t = string_t +let goals_rty_t : goals_rty val_t = option_t goals_t +let evars_rty_t : evars_rty val_t = option_t (list_t evar_t) +let hints_rty_t : hints_rty val_t = + let hint = list_t (pair_t string_t string_t) in + option_t (pair_t (list_t hint) hint) +let status_rty_t : status_rty val_t = state_t +let search_rty_t : search_rty val_t = list_t (coq_object_t string_t) +let get_options_rty_t : get_options_rty val_t = + list_t (pair_t (list_t string_t) option_state_t) +let set_options_rty_t : set_options_rty val_t = unit_t +let mkcases_rty_t : mkcases_rty val_t = list_t (list_t string_t) +let quit_rty_t : quit_rty val_t = unit_t +let about_rty_t : about_rty val_t = coq_info_t +let init_rty_t : init_rty val_t = state_id_t +let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string_t) +let stop_worker_rty_t : stop_worker_rty val_t = unit_t + +let ($) x = erase x +let calls = [| + "Add", ($)add_sty_t, ($)add_rty_t; + "Edit_at", ($)edit_at_sty_t, ($)edit_at_rty_t; + "Query", ($)query_sty_t, ($)query_rty_t; + "Goal", ($)goals_sty_t, ($)goals_rty_t; + "Evars", ($)evars_sty_t, ($)evars_rty_t; + "Hints", ($)hints_sty_t, ($)hints_rty_t; + "Status", ($)status_sty_t, ($)status_rty_t; + "Search", ($)search_sty_t, ($)search_rty_t; + "GetOptions", ($)get_options_sty_t, ($)get_options_rty_t; + "SetOptions", ($)set_options_sty_t, ($)set_options_rty_t; + "MkCases", ($)mkcases_sty_t, ($)mkcases_rty_t; + "Quit", ($)quit_sty_t, ($)quit_rty_t; + "About", ($)about_sty_t, ($)about_rty_t; + "Init", ($)init_sty_t, ($)init_rty_t; + "Interp", ($)interp_sty_t, ($)interp_rty_t; + "StopWorker", ($)stop_worker_sty_t, ($)stop_worker_rty_t; +|] + +type 'a call = + | Add of add_sty + | Edit_at of edit_at_sty + | Query of query_sty + | Goal of goals_sty + | Evars of evars_sty + | Hints of hints_sty + | Status of status_sty + | Search of search_sty + | GetOptions of get_options_sty + | SetOptions of set_options_sty + | MkCases of mkcases_sty + | Quit of quit_sty + | About of about_sty + | Init of init_sty + | StopWorker of stop_worker_sty + (* retrocompatibility *) + | Interp of interp_sty + +let id_of_call = function + | Add _ -> 0 + | Edit_at _ -> 1 + | Query _ -> 2 + | Goal _ -> 3 + | Evars _ -> 4 + | Hints _ -> 5 + | Status _ -> 6 + | Search _ -> 7 + | GetOptions _ -> 8 + | SetOptions _ -> 9 + | MkCases _ -> 10 + | Quit _ -> 11 + | About _ -> 12 + | Init _ -> 13 + | Interp _ -> 14 + | StopWorker _ -> 15 + +let str_of_call c = pi1 calls.(id_of_call c) + +type unknown + +(** We use phantom types and GADT to protect ourselves against wild casts *) +let add x : add_rty call = Add x +let edit_at x : edit_at_rty call = Edit_at x +let query x : query_rty call = Query x +let goals x : goals_rty call = Goal x +let evars x : evars_rty call = Evars x +let hints x : hints_rty call = Hints x +let status x : status_rty call = Status x +let get_options x : get_options_rty call = GetOptions x +let set_options x : set_options_rty call = SetOptions x +let mkcases x : mkcases_rty call = MkCases x +let search x : search_rty call = Search x +let quit x : quit_rty call = Quit x +let init x : init_rty call = Init x +let interp x : interp_rty call = Interp x +let stop_worker x : stop_worker_rty call = StopWorker x + +let abstract_eval_call handler (c : 'a call) : 'a value = + let mkGood x : 'a value = Good (Obj.magic x) in + try + match c with + | Add x -> mkGood (handler.add x) + | Edit_at x -> mkGood (handler.edit_at x) + | Query x -> mkGood (handler.query x) + | Goal x -> mkGood (handler.goals x) + | Evars x -> mkGood (handler.evars x) + | Hints x -> mkGood (handler.hints x) + | Status x -> mkGood (handler.status x) + | Search x -> mkGood (handler.search x) + | GetOptions x -> mkGood (handler.get_options x) + | SetOptions x -> mkGood (handler.set_options x) + | MkCases x -> mkGood (handler.mkcases x) + | Quit x -> mkGood (handler.quit x) + | About x -> mkGood (handler.about x) + | Init x -> mkGood (handler.init x) + | Interp x -> mkGood (handler.interp x) + | StopWorker x -> mkGood (handler.stop_worker x) + with any -> + Fail (handler.handle_exn any) + +(** brain dead code, edit if protocol messages are added/removed *) +let of_answer (q : 'a call) (v : 'a value) : xml = match q with + | Add _ -> of_value (of_value_type add_rty_t ) (Obj.magic v) + | Edit_at _ -> of_value (of_value_type edit_at_rty_t ) (Obj.magic v) + | Query _ -> of_value (of_value_type query_rty_t ) (Obj.magic v) + | Goal _ -> of_value (of_value_type goals_rty_t ) (Obj.magic v) + | Evars _ -> of_value (of_value_type evars_rty_t ) (Obj.magic v) + | Hints _ -> of_value (of_value_type hints_rty_t ) (Obj.magic v) + | Status _ -> of_value (of_value_type status_rty_t ) (Obj.magic v) + | Search _ -> of_value (of_value_type search_rty_t ) (Obj.magic v) + | GetOptions _ -> of_value (of_value_type get_options_rty_t) (Obj.magic v) + | SetOptions _ -> of_value (of_value_type set_options_rty_t) (Obj.magic v) + | MkCases _ -> of_value (of_value_type mkcases_rty_t ) (Obj.magic v) + | Quit _ -> of_value (of_value_type quit_rty_t ) (Obj.magic v) + | About _ -> of_value (of_value_type about_rty_t ) (Obj.magic v) + | Init _ -> of_value (of_value_type init_rty_t ) (Obj.magic v) + | Interp _ -> of_value (of_value_type interp_rty_t ) (Obj.magic v) + | StopWorker _ -> of_value (of_value_type stop_worker_rty_t) (Obj.magic v) + +let to_answer (q : 'a call) (x : xml) : 'a value = match q with + | Add _ -> Obj.magic (to_value (to_value_type add_rty_t ) x) + | Edit_at _ -> Obj.magic (to_value (to_value_type edit_at_rty_t ) x) + | Query _ -> Obj.magic (to_value (to_value_type query_rty_t ) x) + | Goal _ -> Obj.magic (to_value (to_value_type goals_rty_t ) x) + | Evars _ -> Obj.magic (to_value (to_value_type evars_rty_t ) x) + | Hints _ -> Obj.magic (to_value (to_value_type hints_rty_t ) x) + | Status _ -> Obj.magic (to_value (to_value_type status_rty_t ) x) + | Search _ -> Obj.magic (to_value (to_value_type search_rty_t ) x) + | GetOptions _ -> Obj.magic (to_value (to_value_type get_options_rty_t) x) + | SetOptions _ -> Obj.magic (to_value (to_value_type set_options_rty_t) x) + | MkCases _ -> Obj.magic (to_value (to_value_type mkcases_rty_t ) x) + | Quit _ -> Obj.magic (to_value (to_value_type quit_rty_t ) x) + | About _ -> Obj.magic (to_value (to_value_type about_rty_t ) x) + | Init _ -> Obj.magic (to_value (to_value_type init_rty_t ) x) + | Interp _ -> Obj.magic (to_value (to_value_type interp_rty_t ) x) + | StopWorker _ -> Obj.magic (to_value (to_value_type stop_worker_rty_t) x) + +let of_call (q : 'a call) : xml = + let mkCall x = constructor "call" (str_of_call q) [x] in + match q with + | Add x -> mkCall (of_value_type add_sty_t x) + | Edit_at x -> mkCall (of_value_type edit_at_sty_t x) + | Query x -> mkCall (of_value_type query_sty_t x) + | Goal x -> mkCall (of_value_type goals_sty_t x) + | Evars x -> mkCall (of_value_type evars_sty_t x) + | Hints x -> mkCall (of_value_type hints_sty_t x) + | Status x -> mkCall (of_value_type status_sty_t x) + | Search x -> mkCall (of_value_type search_sty_t x) + | GetOptions x -> mkCall (of_value_type get_options_sty_t x) + | SetOptions x -> mkCall (of_value_type set_options_sty_t x) + | MkCases x -> mkCall (of_value_type mkcases_sty_t x) + | Quit x -> mkCall (of_value_type quit_sty_t x) + | About x -> mkCall (of_value_type about_sty_t x) + | Init x -> mkCall (of_value_type init_sty_t x) + | Interp x -> mkCall (of_value_type interp_sty_t x) + | StopWorker x -> mkCall (of_value_type stop_worker_sty_t x) + +let to_call : xml -> unknown call = + do_match "call" (fun s a -> + let mkCallArg vt a = to_value_type vt (singleton a) in + match s with + | "Add" -> Add (mkCallArg add_sty_t a) + | "Edit_at" -> Edit_at (mkCallArg edit_at_sty_t a) + | "Query" -> Query (mkCallArg query_sty_t a) + | "Goal" -> Goal (mkCallArg goals_sty_t a) + | "Evars" -> Evars (mkCallArg evars_sty_t a) + | "Hints" -> Hints (mkCallArg hints_sty_t a) + | "Status" -> Status (mkCallArg status_sty_t a) + | "Search" -> Search (mkCallArg search_sty_t a) + | "GetOptions" -> GetOptions (mkCallArg get_options_sty_t a) + | "SetOptions" -> SetOptions (mkCallArg set_options_sty_t a) + | "MkCases" -> MkCases (mkCallArg mkcases_sty_t a) + | "Quit" -> Quit (mkCallArg quit_sty_t a) + | "About" -> About (mkCallArg about_sty_t a) + | "Init" -> Init (mkCallArg init_sty_t a) + | "Interp" -> Interp (mkCallArg interp_sty_t a) + | "StopWorker" -> StopWorker (mkCallArg stop_worker_sty_t a) + | _ -> raise Marshal_error) + +(** Debug printing *) + +let pr_value_gen pr = function + | Good v -> "GOOD " ^ pr v + | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^str^"]" + | Fail (id,Some(i,j),str) -> + "FAIL "^Stateid.to_string id^ + " ("^string_of_int i^","^string_of_int j^")["^str^"]" +let pr_value v = pr_value_gen (fun _ -> "FIXME") v +let pr_full_value call value = match call with + | Add _ -> pr_value_gen (print add_rty_t ) (Obj.magic value) + | Edit_at _ -> pr_value_gen (print edit_at_rty_t ) (Obj.magic value) + | Query _ -> pr_value_gen (print query_rty_t ) (Obj.magic value) + | Goal _ -> pr_value_gen (print goals_rty_t ) (Obj.magic value) + | Evars _ -> pr_value_gen (print evars_rty_t ) (Obj.magic value) + | Hints _ -> pr_value_gen (print hints_rty_t ) (Obj.magic value) + | Status _ -> pr_value_gen (print status_rty_t ) (Obj.magic value) + | Search _ -> pr_value_gen (print search_rty_t ) (Obj.magic value) + | GetOptions _ -> pr_value_gen (print get_options_rty_t) (Obj.magic value) + | SetOptions _ -> pr_value_gen (print set_options_rty_t) (Obj.magic value) + | MkCases _ -> pr_value_gen (print mkcases_rty_t ) (Obj.magic value) + | Quit _ -> pr_value_gen (print quit_rty_t ) (Obj.magic value) + | About _ -> pr_value_gen (print about_rty_t ) (Obj.magic value) + | Init _ -> pr_value_gen (print init_rty_t ) (Obj.magic value) + | Interp _ -> pr_value_gen (print interp_rty_t ) (Obj.magic value) + | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) (Obj.magic value) +let pr_call call = match call with + | Add x -> str_of_call call ^ " " ^ print add_sty_t x + | Edit_at x -> str_of_call call ^ " " ^ print edit_at_sty_t x + | Query x -> str_of_call call ^ " " ^ print query_sty_t x + | Goal x -> str_of_call call ^ " " ^ print goals_sty_t x + | Evars x -> str_of_call call ^ " " ^ print evars_sty_t x + | Hints x -> str_of_call call ^ " " ^ print hints_sty_t x + | Status x -> str_of_call call ^ " " ^ print status_sty_t x + | Search x -> str_of_call call ^ " " ^ print search_sty_t x + | GetOptions x -> str_of_call call ^ " " ^ print get_options_sty_t x + | SetOptions x -> str_of_call call ^ " " ^ print set_options_sty_t x + | MkCases x -> str_of_call call ^ " " ^ print mkcases_sty_t x + | Quit x -> str_of_call call ^ " " ^ print quit_sty_t x + | About x -> str_of_call call ^ " " ^ print about_sty_t x + | Init x -> str_of_call call ^ " " ^ print init_sty_t x + | Interp x -> str_of_call call ^ " " ^ print interp_sty_t x + | StopWorker x -> str_of_call call ^ " " ^ print stop_worker_sty_t x + +let document to_string_fmt = + Printf.printf "=== Available calls ===\n\n"; + Array.iter (fun (cname, csty, crty) -> + Printf.printf "%12s : %s\n %14s %s\n" + ("\""^cname^"\"") (print_type csty) "->" (print_type crty)) + calls; + Printf.printf "\n=== Calls XML encoding ===\n\n"; + Printf.printf "A call \"C\" carrying input a is encoded as:\n\n%s\n\n" + (to_string_fmt (constructor "call" "C" [PCData "a"])); + Printf.printf "A response carrying output b can either be:\n\n%s\n\n" + (to_string_fmt (of_value (fun _ -> PCData "b") (Good ()))); + Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n" + (to_string_fmt (of_value (fun _ -> PCData "b") + (Fail (Stateid.initial,Some (15,34),"error message")))); + document_type_encoding to_string_fmt + +(* vim: set foldmethod=marker: *) diff --git a/ide/xmlprotocol.mli b/ide/xmlprotocol.mli new file mode 100644 index 000000000..42defce85 --- /dev/null +++ b/ide/xmlprotocol.mli @@ -0,0 +1,56 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* add_rty call +val edit_at : edit_at_sty -> edit_at_rty call +val query : query_sty -> query_rty call +val goals : goals_sty -> goals_rty call +val hints : hints_sty -> hints_rty call +val status : status_sty -> status_rty call +val mkcases : mkcases_sty -> mkcases_rty call +val evars : evars_sty -> evars_rty call +val search : search_sty -> search_rty call +val get_options : get_options_sty -> get_options_rty call +val set_options : set_options_sty -> set_options_rty call +val quit : quit_sty -> quit_rty call +val init : init_sty -> init_rty call +val stop_worker : stop_worker_sty -> stop_worker_rty call +(* retrocompatibility *) +val interp : interp_sty -> interp_rty call + +val abstract_eval_call : handler -> 'a call -> 'a value + +(** * Protocol version *) + +val protocol_version : string + +(** * XML data marshalling *) + +val of_call : 'a call -> xml +val to_call : xml -> unknown call + +val of_answer : 'a call -> 'a value -> xml +val to_answer : 'a call -> xml -> 'a value + +(* Prints the documentation of this module *) +val document : (xml -> string) -> unit + +(** * Debug printing *) + +val pr_call : 'a call -> string +val pr_value : 'a value -> string +val pr_full_value : 'a call -> 'a value -> string diff --git a/idetop/coqidetop.mllib b/idetop/coqidetop.mllib deleted file mode 100644 index 782687744..000000000 --- a/idetop/coqidetop.mllib +++ /dev/null @@ -1 +0,0 @@ -Ide_slave diff --git a/idetop/ide_slave.ml b/idetop/ide_slave.ml deleted file mode 100644 index 2185084a0..000000000 --- a/idetop/ide_slave.ml +++ /dev/null @@ -1,453 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* - flush_all (); - Pp_control.std_ft := out_ft; - Pp_control.err_ft := out_ft; - Pp_control.deep_ft := deep_out_ft; - ), - (fun () -> Format.pp_print_flush out_ft (); - let r = Buffer.contents out_buff in - Buffer.clear out_buff; r) - -let pr_with_pid s = Printf.eprintf "[pid %d] %s\n%!" (Unix.getpid ()) 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 ("<-- " ^ Serialize.pr_call q) -let pr_debug_answer q r = - if !Flags.debug then pr_with_pid ("--> " ^ Serialize.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"]] - -let is_known_option cmd = match cmd with - | VernacSetOption (o,BoolValue true) - | VernacUnsetOption o -> coqide_known_option o - | _ -> false - -let is_debug cmd = match cmd with - | VernacSetOption (["Ltac";"Debug"], _) -> true - | _ -> false - -let is_query cmd = match cmd with - | VernacChdir None - | VernacMemOption _ - | VernacPrintOption _ - | VernacCheckMayEval _ - | VernacGlobalCheck _ - | VernacPrint _ - | VernacSearch _ - | VernacLocate _ -> true - | _ -> false - -let is_undo cmd = match cmd with - | VernacUndo _ | VernacUndoTo _ -> true - | _ -> false - -(** Check whether a command is forbidden by CoqIDE *) - -let coqide_cmd_checks (loc,ast) = - let user_error s = Errors.user_err_loc (loc, "CoqIde", str s) in - if is_debug ast then - user_error "Debug mode not available within CoqIDE"; - if is_known_option ast then - msg_warning (strbrk"This will not work. Use CoqIDE display menu instead"); - if Vernac.is_navigation_vernac ast || is_undo ast then - msg_warning (strbrk "Rather use CoqIDE navigation instead"); - if is_query ast then - msg_warning (strbrk "Query commands should not be inserted in scripts") - -(** Interpretation (cf. [Ide_intf.interp]) *) - -let add ((s,eid),(sid,verbose)) = - let newid, rc = Stm.add ~ontop:sid verbose ~check:coqide_cmd_checks eid s in - let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in - newid, (rc, read_stdout ()) - -let edit_at id = - match Stm.edit_at id with - | `NewTip -> CSig.Inl () - | `Focus { Stm.start; stop; tip} -> CSig.Inr (start, (stop, tip)) - -let query (s,id) = Stm.query ~at:id s; read_stdout () - -(** Goal display *) - -let hyp_next_tac sigma env (id,_,ast) = - let id_s = Names.Id.to_string id in - let type_s = string_of_ppcmds (pr_ltype_env env 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 id = Goal.uid g in - let ccl = - let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in - string_of_ppcmds (pr_goal_concl_style_env env norm_constr) in - let process_hyp h_env d acc = - let d = Context.map_named_declaration (Reductionops.nf_evar sigma) d in - (string_of_ppcmds (pr_var_decl h_env d)) :: acc in - let hyps = - List.rev (Environ.fold_named_context process_hyp env ~init: []) in - { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } - -let goals () = - Stm.finish (); - let s = read_stdout () in - if not (String.is_empty s) then msg_info (str s); - try - let pfts = Proof_global.give_me_the_proof () in - let (goals, zipper, shelf, given_up, sigma) = Proof.proof pfts in - let fg = List.map (process_goal sigma) goals in - let map_zip (lg, rg) = - let lg = List.map (process_goal sigma) lg in - let rg = List.map (process_goal sigma) rg in - (lg, rg) - in - let bg = List.map map_zip zipper in - let shelf = List.map (process_goal sigma) shelf in - let given_up = List.map (process_goal sigma) given_up in - Some { Interface.fg_goals = fg; - Interface.bg_goals = bg; - shelved_goals = shelf; - given_up_goals = given_up; } - with Proof_global.NoCurrentProof -> None - -let evars () = - try - Stm.finish (); - let s = read_stdout () in - if not (String.is_empty s) then msg_info (str s); - let pfts = Proof_global.give_me_the_proof () in - let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in - let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in - let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar 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 { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals 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 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) *) - Stm.finish (); - if force then Stm.join (); - let s = read_stdout () in - if not (String.is_empty s) then msg_info (str s); - 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 (); - } - -let search flags = Search.interface_search flags - -let get_options () = - let table = Goptions.get_tables () in - let fold key state accu = (key, state) :: accu in - Goptions.OptionMap.fold fold table [] - -let set_options options = - let iter (name, value) = match 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 - in - List.iter iter options - -let about () = { - Interface.coqtop_version = Coq_config.version; - Interface.protocol_version = Serialize.protocol_version; - Interface.release_date = Coq_config.date; - Interface.compile_date = Coq_config.compile_date; -} - -let handle_exn e = - let dummy = Stateid.dummy in - let loc_of e = match Loc.get_loc e with - | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc) - | _ -> None in - let mk_msg e = read_stdout ()^"\n"^string_of_ppcmds (Errors.print e) in - match e with - | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!" - | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!" - | e -> - match Stateid.get e with - | Some (valid, _) -> valid, loc_of e, mk_msg e - | None -> dummy, loc_of e, mk_msg e - -let init = - let initialized = ref false in - fun file -> - if !initialized then anomaly (str "Already initialized") - else begin - initialized := true; - match file with - | None -> Stm.get_current_state () - | Some file -> - let dir = Filename.dirname file in - let open Loadpath in let open CUnix in - let initial_id, _ = - if not (is_in_load_paths (physical_path_of_string dir)) then - Stm.add false ~ontop:(Stm.get_current_state ()) - 0 (Printf.sprintf "Add LoadPath \"%s\". " dir) - else Stm.get_current_state (), `NewTip in - Stm.set_compilation_hints file; - initial_id - end - -(* Retrocompatibility stuff *) -let interp ((_raw, verbose), s) = - let vernac_parse s = - let pa = Pcoq.Gram.parsable (Stream.of_string s) in - Flags.with_option Flags.we_are_parsing (fun () -> - match Pcoq.Gram.entry_parse Pcoq.main_entry pa with - | None -> raise (Invalid_argument "vernac_parse") - | Some ast -> ast) - () in - Stm.interp verbose (vernac_parse s); - Stm.get_current_state (), CSig.Inl (read_stdout ()) - -(** 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 - -(** Grouping all call handlers together + error handling *) - -let eval_call xml_oc log c = - let interruptible f x = - catch_break := true; - Control.check_for_interrupt (); - let r = f x in - catch_break := false; - let out = read_stdout () in - if not (String.is_empty out) then log (str out); - 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.interp = interruptible interp; - Interface.handle_exn = handle_exn; - Interface.stop_worker = Stm.stop_worker; - } in - Serialize.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 = Errors.push e in Mutex.unlock m; raise e - - -let slave_logger xml_oc level message = - (* convert the message into XML *) - let msg = string_of_ppcmds (hov 0 message) in - let message = { - Interface.message_level = level; - Interface.message_content = msg; - } in - let () = pr_debug (Printf.sprintf "-> %S" msg) in - let xml = Serialize.of_message message in - print_xml xml_oc xml - -let slave_feeder xml_oc msg = - let xml = Serialize.of_feedback 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 loop () = - 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 - CThread.prepare_in_channel_for_thread_friendly_io in_ch; - let in_lb = Lexing.from_function (fun s len -> - CThread.thread_friendly_read in_ch s ~off:0 ~len) in - let xml_ic = Xml_parser.make (Xml_parser.SLexbuf in_lb) in - let () = Xml_parser.check_eof xml_ic false in - set_logger (slave_logger xml_oc); - set_feeder (slave_feeder xml_oc); - (* We'll handle goal fetching and display in our own way *) - Vernacentries.enable_goal_printing := false; - Vernacentries.qed_display_script := false; - Flags.make_term_color false; - 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 q = Serialize.to_call xml_query in - let () = pr_debug_call q in - let r = eval_call xml_oc (slave_logger xml_oc Interface.Notice) q in - let () = pr_debug_answer q r in -(* pr_with_pid (Xml_printer.to_string_fmt (Serialize.of_answer q r)); *) - print_xml xml_oc (Serialize.of_answer 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_debug ("Syntax error in query: " ^ Xml_parser.error_msg err); - exit 1 - | Serialize.Marshal_error -> - pr_debug "Incorrect query."; - exit 1 - | any -> - pr_debug ("Fatal exception in coqtop:\n" ^ Printexc.to_string any); - exit 1 - done; - pr_debug "Exiting gracefully."; - exit 0 - -let () = Coqtop.toploop_init := (fun args -> - Flags.make_silent true; - init_stdout (); - args) - -let () = Coqtop.toploop_run := loop diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 80b5830fd..bf9d2c0b9 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -131,7 +131,7 @@ let interval loc = let dump_ref loc filepath modpath ident ty = if !glob_output = Feedback then - Pp.feedback (Interface.GlobRef (loc, filepath, modpath, ident, ty)) + Pp.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty)) else let bl,el = interval loc in dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n" @@ -229,7 +229,7 @@ let dump_binding loc id = () let dump_def ty loc secpath id = if !glob_output = Feedback then - Pp.feedback (Interface.GlobDef (loc, id, secpath, ty)) + Pp.feedback (Feedback.GlobDef (loc, id, secpath, ty)) else let bl,el = interval loc in dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el secpath id) diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 89e1b41f3..af65f6541 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -148,7 +148,7 @@ type obsolete_locality = bool * compatible. If the grammar is fixed removing deprecated syntax, this * bool should go away too *) -type option_value = Interface.option_value = +type option_value = Goptions.option_value = | BoolValue of bool | IntValue of int option | StringValue of string diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index f38ad4742..9f30b7da3 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -105,7 +105,7 @@ let hcons_j j = { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} let feedback_completion_typecheck = - Option.iter (fun state_id -> Pp.feedback ~state_id Interface.Complete) + Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) let check_projection env kn inst body = let cannot_recognize () = error ("Cannot recognize a projection") in diff --git a/lib/clib.mllib b/lib/clib.mllib index ed4894cb9..73839fd9e 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -17,6 +17,8 @@ IStream Pp_control Flags Control +Loc +Serialize Pp Deque CObj @@ -25,9 +27,8 @@ CString CArray CStack Util -Loc Stateid -Serialize +Feedback CUnix Envars Aux_file diff --git a/lib/feedback.ml b/lib/feedback.ml new file mode 100644 index 000000000..b532c2653 --- /dev/null +++ b/lib/feedback.ml @@ -0,0 +1,96 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* match s,a with + | "addedaxiom", _ -> AddedAxiom + | "processed", _ -> Processed + | "processinginmaster", _ -> ProcessingInMaster + | "incomplete", _ -> Incomplete + | "complete", _ -> Complete + | "globref", [loc; filepath; modpath; ident; ty] -> + GlobRef(to_loc loc, to_string filepath, + to_string modpath, to_string ident, to_string ty) + | "globdef", [loc; ident; secpath; ty] -> + GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty) + | "errormsg", [loc; s] -> ErrorMsg (to_loc loc, to_string s) + | "inprogress", [n] -> InProgress (to_int n) + | "slavestatus", [ns] -> + let n, s = to_pair to_int to_string ns in + SlaveStatus(n,s) + | _ -> raise Marshal_error) +let of_feedback_content = function + | AddedAxiom -> constructor "feedback_content" "addedaxiom" [] + | Processed -> constructor "feedback_content" "processed" [] + | ProcessingInMaster -> constructor "feedback_content" "processinginmaster" [] + | Incomplete -> constructor "feedback_content" "incomplete" [] + | Complete -> constructor "feedback_content" "complete" [] + | GlobRef(loc, filepath, modpath, ident, ty) -> + constructor "feedback_content" "globref" [ + of_loc loc; + of_string filepath; + of_string modpath; + of_string ident; + of_string ty ] + | GlobDef(loc, ident, secpath, ty) -> + constructor "feedback_content" "globdef" [ + of_loc loc; + of_string ident; + of_string secpath; + of_string ty ] + | ErrorMsg(loc, s) -> + constructor "feedback_content" "errormsg" [of_loc loc; of_string s] + | InProgress n -> constructor "feedback_content" "inprogress" [of_int n] + | SlaveStatus(n,s) -> + constructor "feedback_content" "slavestatus" + [of_pair of_int of_string (n,s)] + +let of_edit_or_state_id = function + | Edit id -> ["object","edit"], of_edit_id id + | State id -> ["object","state"], Stateid.to_xml id + +let of_feedback msg = + let content = of_feedback_content msg.content in + let obj, id = of_edit_or_state_id msg.id in + Element ("feedback", obj, [id;content]) +let to_feedback xml = match xml with + | Element ("feedback", ["object","edit"], [id;content]) -> { + id = Edit(to_edit_id id); + content = to_feedback_content content } + | Element ("feedback", ["object","state"], [id;content]) -> { + id = State(Stateid.of_xml id); + content = to_feedback_content content } + | _ -> raise Marshal_error + +let is_feedback = function + | Element ("feedback", _, _) -> true + | _ -> false + diff --git a/lib/feedback.mli b/lib/feedback.mli new file mode 100644 index 000000000..e7645ca16 --- /dev/null +++ b/lib/feedback.mli @@ -0,0 +1,36 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* xml +val to_feedback : xml -> feedback +val is_feedback : xml -> bool + diff --git a/lib/interface.mli b/lib/interface.mli deleted file mode 100644 index c8fe068e6..000000000 --- a/lib/interface.mli +++ /dev/null @@ -1,267 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* add_rty; - edit_at : edit_at_sty -> edit_at_rty; - query : query_sty -> query_rty; - goals : goals_sty -> goals_rty; - evars : evars_sty -> evars_rty; - hints : hints_sty -> hints_rty; - status : status_sty -> status_rty; - search : search_sty -> search_rty; - get_options : get_options_sty -> get_options_rty; - set_options : set_options_sty -> set_options_rty; - mkcases : mkcases_sty -> mkcases_rty; - about : about_sty -> about_rty; - stop_worker : stop_worker_sty -> stop_worker_rty; - handle_exn : handle_exn_sty -> handle_exn_rty; - init : init_sty -> init_rty; - quit : quit_sty -> quit_rty; - (* Retrocompatibility stuff *) - interp : interp_sty -> interp_rty; -} - diff --git a/lib/pp.ml b/lib/pp.ml index f9fe53fdf..91ea5230d 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -345,14 +345,49 @@ let msgerrnl x = msgnl_with !err_ft x (* Logging management *) -type level = Interface.message_level = -| Debug of string -| Info -| Notice -| Warning -| Error - -type logger = level -> std_ppcmds -> unit +type message_level = + | Debug of string + | Info + | Notice + | Warning + | Error + +type message = { + message_level : message_level; + message_content : string; +} + +let of_message_level = function + | Debug s -> + Serialize.constructor "message_level" "debug" [Xml_datatype.PCData s] + | Info -> Serialize.constructor "message_level" "info" [] + | Notice -> Serialize.constructor "message_level" "notice" [] + | Warning -> Serialize.constructor "message_level" "warning" [] + | Error -> Serialize.constructor "message_level" "error" [] +let to_message_level = + Serialize.do_match "message_level" (fun s args -> match s with + | "debug" -> Debug (Serialize.raw_string args) + | "info" -> Info + | "notice" -> Notice + | "warning" -> Warning + | "error" -> Error + | _ -> raise Serialize.Marshal_error) + +let of_message msg = + let lvl = of_message_level msg.message_level in + let content = Serialize.of_string msg.message_content in + Xml_datatype.Element ("message", [], [lvl; content]) +let to_message xml = match xml with + | Xml_datatype.Element ("message", [], [lvl; content]) -> { + message_level = to_message_level lvl; + message_content = Serialize.to_string content } + | _ -> raise Serialize.Marshal_error + +let is_message = function + | Xml_datatype.Element ("message", _, _) -> true + | _ -> false + +type logger = message_level -> std_ppcmds -> unit let print_color s x = x (* FIXME *) @@ -387,14 +422,14 @@ let set_logger l = logger := l (** Feedback *) let feeder = ref ignore -let feedback_id = ref (Interface.Edit 0) +let feedback_id = ref (Feedback.Edit 0) let set_id_for_feedback i = feedback_id := i let feedback ?state_id what = !feeder { - Interface.content = what; - Interface.id = + Feedback.content = what; + Feedback.id = match state_id with - | Some id -> Interface.State id + | Some id -> Feedback.State id | None -> !feedback_id; } let set_feeder f = feeder := f diff --git a/lib/pp.mli b/lib/pp.mli index 635a149e8..fe11619c1 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -78,8 +78,19 @@ val close : unit -> std_ppcmds val tclose : unit -> std_ppcmds (** {6 Sending messages to the user} *) +type message_level = + | Debug of string + | Info + | Notice + | Warning + | Error -type logger = Interface.message_level -> std_ppcmds -> unit +type message = { + message_level : message_level; + message_content : string; +} + +type logger = message_level -> std_ppcmds -> unit val msg_info : std_ppcmds -> unit (** Message that displays information, usually in verbose mode, such as [Foobar @@ -104,6 +115,11 @@ val std_logger : logger val set_logger : logger -> unit +val of_message : message -> Xml_datatype.xml +val to_message : Xml_datatype.xml -> message +val is_message : Xml_datatype.xml -> bool + + (** {6 Feedback sent, even asynchronously, to the user interface} *) (* This stuff should be available to most of the system, line msg_* above. @@ -116,10 +132,10 @@ val set_logger : logger -> unit * since the two phases are performed sequentially) *) val feedback : - ?state_id:Interface.state_id -> Interface.feedback_content -> unit + ?state_id:Feedback.state_id -> Feedback.feedback_content -> unit -val set_id_for_feedback : Interface.edit_or_state_id -> unit -val set_feeder : (Interface.feedback -> unit) -> unit +val set_id_for_feedback : Feedback.edit_or_state_id -> unit +val set_feeder : (Feedback.feedback -> unit) -> unit (** {6 Utilities} *) diff --git a/lib/serialize.ml b/lib/serialize.ml index 042b75e2d..7c0c6b86e 100644 --- a/lib/serialize.ml +++ b/lib/serialize.ml @@ -6,21 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Protocol version of this file. This is the date of the last modification. *) - -(** WARNING: TO BE UPDATED WHEN MODIFIED! *) - -let protocol_version = "20140312" - -(** * Interface of calls to Coq by CoqIde *) - -open Util -open Interface open Xml_datatype -(* Marshalling of basic types and type constructors *) -module Xml_marshalling = struct - exception Marshal_error (** Utility functions *) @@ -96,76 +83,16 @@ let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function | Element ("pair", [], [x; y]) -> (f x, g y) | _ -> raise Marshal_error -let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) union -> xml = function - | Inl x -> Element ("union", ["val","in_l"], [f x]) - | Inr x -> Element ("union", ["val","in_r"], [g x]) -let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) union = function - | Element ("union", ["val","in_l"], [x]) -> Inl (f x) - | Element ("union", ["val","in_r"], [x]) -> Inr (g x) +let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) CSig.union -> xml = function + | CSig.Inl x -> Element ("union", ["val","in_l"], [f x]) + | CSig.Inr x -> Element ("union", ["val","in_r"], [g x]) +let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) CSig.union = function + | Element ("union", ["val","in_l"], [x]) -> CSig.Inl (f x) + | Element ("union", ["val","in_r"], [x]) -> CSig.Inr (g x) | _ -> raise Marshal_error (** More elaborate types *) -let of_option_value = function - | IntValue i -> constructor "option_value" "intvalue" [of_option of_int i] - | BoolValue b -> constructor "option_value" "boolvalue" [of_bool b] - | StringValue s -> constructor "option_value" "stringvalue" [of_string s] -let to_option_value = do_match "option_value" (fun s args -> match s with - | "intvalue" -> IntValue (to_option to_int (singleton args)) - | "boolvalue" -> BoolValue (to_bool (singleton args)) - | "stringvalue" -> StringValue (to_string (singleton args)) - | _ -> raise Marshal_error) - -let of_option_state s = - Element ("option_state", [], [ - of_bool s.opt_sync; - of_bool s.opt_depr; - of_string s.opt_name; - of_option_value s.opt_value]) -let to_option_state = function - | Element ("option_state", [], [sync; depr; name; value]) -> { - opt_sync = to_bool sync; - opt_depr = to_bool depr; - opt_name = to_string name; - opt_value = to_option_value value } - | _ -> raise Marshal_error - -let of_search_cst = function - | Name_Pattern s -> - constructor "search_cst" "name_pattern" [of_string s] - | Type_Pattern s -> - constructor "search_cst" "type_pattern" [of_string s] - | SubType_Pattern s -> - constructor "search_cst" "subtype_pattern" [of_string s] - | In_Module m -> - constructor "search_cst" "in_module" [of_list of_string m] - | Include_Blacklist -> - constructor "search_cst" "include_blacklist" [] -let to_search_cst = do_match "search_cst" (fun s args -> match s with - | "name_pattern" -> Name_Pattern (to_string (singleton args)) - | "type_pattern" -> Type_Pattern (to_string (singleton args)) - | "subtype_pattern" -> SubType_Pattern (to_string (singleton args)) - | "in_module" -> In_Module (to_list to_string (singleton args)) - | "include_blacklist" -> Include_Blacklist - | _ -> raise Marshal_error) - -let of_coq_object f ans = - let prefix = of_list of_string ans.coq_object_prefix in - let qualid = of_list of_string ans.coq_object_qualid in - let obj = f ans.coq_object_object in - Element ("coq_object", [], [prefix; qualid; obj]) - -let to_coq_object f = function -| Element ("coq_object", [], [prefix; qualid; obj]) -> - let prefix = to_list to_string prefix in - let qualid = to_list to_string qualid in - let obj = f obj in { - coq_object_prefix = prefix; - coq_object_qualid = qualid; - coq_object_object = obj; - } -| _ -> raise Marshal_error - let of_edit_id i = Element ("edit_id",["val",string_of_int i],[]) let to_edit_id = function | Element ("edit_id",["val",i],[]) -> @@ -174,138 +101,11 @@ let to_edit_id = function id | _ -> raise Marshal_error -let of_state_id id = - try Stateid.to_xml id with Invalid_argument _ -> raise Marshal_error -let to_state_id xml = - try Stateid.of_xml xml with Invalid_argument _ -> raise Marshal_error - -let of_edit_or_state_id = function - | Interface.Edit id -> ["object","edit"], of_edit_id id - | Interface.State id -> ["object","state"], of_state_id id - -let of_value f = function -| Good x -> Element ("value", ["val", "good"], [f x]) -| Fail (id,loc, msg) -> - let loc = match loc with - | None -> [] - | Some (s, e) -> [("loc_s", string_of_int s); ("loc_e", string_of_int e)] in - let id = of_state_id id in - Element ("value", ["val", "fail"] @ loc, [id;PCData msg]) -let to_value f = function -| Element ("value", attrs, l) -> - let ans = massoc "val" attrs in - if ans = "good" then Good (f (singleton l)) - else if ans = "fail" then - let loc = - try - let loc_s = int_of_string (get_attr "loc_s" attrs) in - let loc_e = int_of_string (get_attr "loc_e" attrs) in - Some (loc_s, loc_e) - with Not_found | Failure _ -> None - in - let id = to_state_id (List.hd l) in - let msg = raw_string (List.tl l) in - Fail (id, loc, msg) - else raise Marshal_error -| _ -> raise Marshal_error - -let of_status s = - let of_so = of_option of_string in - let of_sl = of_list of_string in - Element ("status", [], [ - of_sl s.status_path; - of_so s.status_proofname; - of_sl s.status_allproofs; - of_int s.status_proofnum; ]) -let to_status = function - | Element ("status", [], [path; name; prfs; pnum]) -> { - status_path = to_list to_string path; - status_proofname = to_option to_string name; - status_allproofs = to_list to_string prfs; - status_proofnum = to_int pnum; } - | _ -> raise Marshal_error - -let of_evar s = Element ("evar", [], [PCData s.evar_info]) -let to_evar = function - | Element ("evar", [], data) -> { evar_info = raw_string data; } - | _ -> raise Marshal_error - -let of_goal g = - let hyp = of_list of_string g.goal_hyp in - let ccl = of_string g.goal_ccl in - let id = of_string g.goal_id in - Element ("goal", [], [id; hyp; ccl]) -let to_goal = function - | Element ("goal", [], [id; hyp; ccl]) -> - let hyp = to_list to_string hyp in - let ccl = to_string ccl in - let id = to_string id in - { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; } - | _ -> raise Marshal_error - -let of_goals g = - let of_glist = of_list of_goal in - let fg = of_list of_goal g.fg_goals in - let bg = of_list (of_pair of_glist of_glist) g.bg_goals in - let shelf = of_list of_goal g.shelved_goals in - let given_up = of_list of_goal g.given_up_goals in - Element ("goals", [], [fg; bg; shelf; given_up]) -let to_goals = function - | Element ("goals", [], [fg; bg; shelf; given_up]) -> - let to_glist = to_list to_goal in - let fg = to_list to_goal fg in - let bg = to_list (to_pair to_glist to_glist) bg in - let shelf = to_list to_goal shelf in - let given_up = to_list to_goal given_up in - { fg_goals = fg; bg_goals = bg; shelved_goals = shelf; given_up_goals = given_up } - | _ -> raise Marshal_error - -let of_coq_info info = - let version = of_string info.coqtop_version in - let protocol = of_string info.protocol_version in - let release = of_string info.release_date in - let compile = of_string info.compile_date in - Element ("coq_info", [], [version; protocol; release; compile]) -let to_coq_info = function - | Element ("coq_info", [], [version; protocol; release; compile]) -> { - coqtop_version = to_string version; - protocol_version = to_string protocol; - release_date = to_string release; - compile_date = to_string compile; } - | _ -> raise Marshal_error - -let of_message_level = function - | Debug s -> constructor "message_level" "debug" [PCData s] - | Info -> constructor "message_level" "info" [] - | Notice -> constructor "message_level" "notice" [] - | Warning -> constructor "message_level" "warning" [] - | Error -> constructor "message_level" "error" [] -let to_message_level = do_match "message_level" (fun s args -> match s with - | "debug" -> Debug (raw_string args) - | "info" -> Info - | "notice" -> Notice - | "warning" -> Warning - | "error" -> Error - | _ -> raise Marshal_error) - -let of_message msg = - let lvl = of_message_level msg.message_level in - let content = of_string msg.message_content in - Element ("message", [], [lvl; content]) -let to_message xml = match xml with - | Element ("message", [], [lvl; content]) -> { - message_level = to_message_level lvl; - message_content = to_string content } - | _ -> raise Marshal_error - -let is_message = function - | Element ("message", _, _) -> true - | _ -> false - let of_loc loc = let start, stop = Loc.unloc loc in Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[]) -let to_loc xml = match xml with +let to_loc xml = + match xml with | Element ("loc", l,[]) -> (try let start = massoc "start" l in @@ -314,590 +114,3 @@ let to_loc xml = match xml with with Not_found | Invalid_argument _ -> raise Marshal_error) | _ -> raise Marshal_error -let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with - | "addedaxiom", _ -> AddedAxiom - | "processed", _ -> Processed - | "processinginmaster", _ -> ProcessingInMaster - | "incomplete", _ -> Incomplete - | "complete", _ -> Complete - | "globref", [loc; filepath; modpath; ident; ty] -> - GlobRef(to_loc loc, to_string filepath, - to_string modpath, to_string ident, to_string ty) - | "globdef", [loc; ident; secpath; ty] -> - GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty) - | "errormsg", [loc; s] -> ErrorMsg (to_loc loc, to_string s) - | "inprogress", [n] -> InProgress (to_int n) - | "slavestatus", [ns] -> - let n, s = to_pair to_int to_string ns in - SlaveStatus(n,s) - | _ -> raise Marshal_error) -let of_feedback_content = function - | AddedAxiom -> constructor "feedback_content" "addedaxiom" [] - | Processed -> constructor "feedback_content" "processed" [] - | ProcessingInMaster -> constructor "feedback_content" "processinginmaster" [] - | Incomplete -> constructor "feedback_content" "incomplete" [] - | Complete -> constructor "feedback_content" "complete" [] - | GlobRef(loc, filepath, modpath, ident, ty) -> - constructor "feedback_content" "globref" [ - of_loc loc; - of_string filepath; - of_string modpath; - of_string ident; - of_string ty ] - | GlobDef(loc, ident, secpath, ty) -> - constructor "feedback_content" "globdef" [ - of_loc loc; - of_string ident; - of_string secpath; - of_string ty ] - | ErrorMsg(loc, s) -> - constructor "feedback_content" "errormsg" [of_loc loc; of_string s] - | InProgress n -> constructor "feedback_content" "inprogress" [of_int n] - | SlaveStatus(n,s) -> - constructor "feedback_content" "slavestatus" - [of_pair of_int of_string (n,s)] - -let of_feedback msg = - let content = of_feedback_content msg.content in - let obj, id = of_edit_or_state_id msg.id in - Element ("feedback", obj, [id;content]) -let to_feedback xml = match xml with - | Element ("feedback", ["object","edit"], [id;content]) -> { - id = Interface.Edit(to_edit_id id); - content = to_feedback_content content } - | Element ("feedback", ["object","state"], [id;content]) -> { - id = Interface.State(to_state_id id); - content = to_feedback_content content } - | _ -> raise Marshal_error - -end -include Xml_marshalling - -(* Reification of basic types and type constructors, and functions - from to xml *) -module ReifType : sig - - type 'a val_t - - val unit_t : unit val_t - val string_t : string val_t - val int_t : int val_t - val bool_t : bool val_t - - val option_t : 'a val_t -> 'a option val_t - val list_t : 'a val_t -> 'a list val_t - val pair_t : 'a val_t -> 'b val_t -> ('a * 'b) val_t - val union_t : 'a val_t -> 'b val_t -> ('a ,'b) union val_t - - val goals_t : goals val_t - val evar_t : evar val_t - val state_t : status val_t - val option_state_t : option_state val_t - val option_value_t : option_value val_t - val coq_info_t : coq_info val_t - val coq_object_t : 'a val_t -> 'a coq_object val_t - val state_id_t : state_id val_t - val search_cst_t : search_constraint val_t - - val of_value_type : 'a val_t -> 'a -> xml - val to_value_type : 'a val_t -> xml -> 'a - - val print : 'a val_t -> 'a -> string - - type value_type - val erase : 'a val_t -> value_type - val print_type : value_type -> string - - val document_type_encoding : (xml -> string) -> unit - -end = struct - - type value_type = - | Unit | String | Int | Bool - - | Option of value_type - | List of value_type - | Pair of value_type * value_type - | Union of value_type * value_type - - | Goals | Evar | State | Option_state | Option_value | Coq_info - | Coq_object of value_type - | State_id - | Search_cst - - type 'a val_t = value_type - - let erase (x : 'a val_t) : value_type = x - - let unit_t = Unit - let string_t = String - let int_t = Int - let bool_t = Bool - - let option_t x = Option x - let list_t x = List x - let pair_t x y = Pair (x, y) - let union_t x y = Union (x, y) - - let goals_t = Goals - let evar_t = Evar - let state_t = State - let option_state_t = Option_state - let option_value_t = Option_value - let coq_info_t = Coq_info - let coq_object_t x = Coq_object x - let state_id_t = State_id - let search_cst_t = Search_cst - - let of_value_type (ty : 'a val_t) : 'a -> xml = - let rec convert ty : 'a -> xml = match ty with - | Unit -> Obj.magic of_unit - | Bool -> Obj.magic of_bool - | String -> Obj.magic of_string - | Int -> Obj.magic of_int - | State -> Obj.magic of_status - | Option_state -> Obj.magic of_option_state - | Option_value -> Obj.magic of_option_value - | Coq_info -> Obj.magic of_coq_info - | Goals -> Obj.magic of_goals - | Evar -> Obj.magic of_evar - | List t -> Obj.magic (of_list (convert t)) - | Option t -> Obj.magic (of_option (convert t)) - | Coq_object t -> Obj.magic (of_coq_object (convert t)) - | Pair (t1,t2) -> Obj.magic (of_pair (convert t1) (convert t2)) - | Union (t1,t2) -> Obj.magic (of_union (convert t1) (convert t2)) - | State_id -> Obj.magic of_state_id - | Search_cst -> Obj.magic of_search_cst - in - convert ty - - let to_value_type (ty : 'a val_t) : xml -> 'a = - let rec convert ty : xml -> 'a = match ty with - | Unit -> Obj.magic to_unit - | Bool -> Obj.magic to_bool - | String -> Obj.magic to_string - | Int -> Obj.magic to_int - | State -> Obj.magic to_status - | Option_state -> Obj.magic to_option_state - | Option_value -> Obj.magic to_option_value - | Coq_info -> Obj.magic to_coq_info - | Goals -> Obj.magic to_goals - | Evar -> Obj.magic to_evar - | List t -> Obj.magic (to_list (convert t)) - | Option t -> Obj.magic (to_option (convert t)) - | Coq_object t -> Obj.magic (to_coq_object (convert t)) - | Pair (t1,t2) -> Obj.magic (to_pair (convert t1) (convert t2)) - | Union (t1,t2) -> Obj.magic (to_union (convert t1) (convert t2)) - | State_id -> Obj.magic to_state_id - | Search_cst -> Obj.magic to_search_cst - in - convert ty - - let pr_unit () = "" - let pr_string s = Printf.sprintf "%S" s - let pr_int i = string_of_int i - let pr_bool b = Printf.sprintf "%B" b - let pr_goal (g : goals) = - if g.fg_goals = [] then - if g.bg_goals = [] then "Proof completed." - else - let rec pr_focus _ = function - | [] -> assert false - | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg) - | (lg, rg) :: l -> - Printf.sprintf "%i:%a" - (List.length lg + List.length rg) pr_focus l in - Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals - else - let pr_menu s = s in - let pr_goal { goal_hyp = hyps; goal_ccl = goal } = - "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ - pr_menu goal ^ "]" in - String.concat " " (List.map pr_goal g.fg_goals) - let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]" - let pr_status (s : status) = - let path = - let l = String.concat "." s.status_path in - "path=" ^ l ^ ";" in - let name = match s.status_proofname with - | None -> "no proof;" - | Some n -> "proof = " ^ n ^ ";" in - "Status: " ^ path ^ name - let pr_coq_info (i : coq_info) = "FIXME" - let pr_option_value = function - | IntValue None -> "none" - | IntValue (Some i) -> string_of_int i - | StringValue s -> s - | BoolValue b -> if b then "true" else "false" - let pr_option_state (s : option_state) = - Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n" - s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value) - let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]" - let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")" - let pr_coq_object (o : 'a coq_object) = "FIXME" - let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")" - let pr_union pr1 pr2 = function Inl x -> "Inl "^pr1 x | Inr x -> "Inr "^pr2 x - - let pr_search_cst = function - | Name_Pattern s -> "Name_Pattern " ^ s - | Type_Pattern s -> "Type_Pattern " ^ s - | SubType_Pattern s -> "SubType_Pattern " ^ s - | In_Module s -> "In_Module " ^ String.concat "." s - | Include_Blacklist -> "Include_Blacklist" - - let rec print = function - | Unit -> Obj.magic pr_unit - | Bool -> Obj.magic pr_bool - | String -> Obj.magic pr_string - | Int -> Obj.magic pr_int - | State -> Obj.magic pr_status - | Option_state -> Obj.magic pr_option_state - | Option_value -> Obj.magic pr_option_value - | Search_cst -> Obj.magic pr_search_cst - | Coq_info -> Obj.magic pr_coq_info - | Goals -> Obj.magic pr_goal - | Evar -> Obj.magic pr_evar - | List t -> Obj.magic (pr_list (print t)) - | Option t -> Obj.magic (pr_option (print t)) - | Coq_object t -> Obj.magic pr_coq_object - | Pair (t1,t2) -> Obj.magic (pr_pair (print t1) (print t2)) - | Union (t1,t2) -> Obj.magic (pr_union (print t1) (print t2)) - | State_id -> Obj.magic pr_int - - (* This is to break if a rename/refactoring makes the strings below outdated *) - type 'a exists = bool - - let rec print_type = function - | Unit -> "unit" - | Bool -> "bool" - | String -> "string" - | Int -> "int" - | State -> assert(true : status exists); "Interface.status" - | Option_state -> assert(true : option_state exists); "Interface.option_state" - | Option_value -> assert(true : option_value exists); "Interface.option_value" - | Search_cst -> assert(true : search_constraint exists); "Interface.search_constraint" - | Coq_info -> assert(true : coq_info exists); "Interface.coq_info" - | Goals -> assert(true : goals exists); "Interface.goals" - | Evar -> assert(true : evar exists); "Interface.evar" - | List t -> Printf.sprintf "(%s list)" (print_type t) - | Option t -> Printf.sprintf "(%s option)" (print_type t) - | Coq_object t -> assert(true : 'a coq_object exists); - Printf.sprintf "(%s Interface.coq_object)" (print_type t) - | Pair (t1,t2) -> Printf.sprintf "(%s * %s)" (print_type t1) (print_type t2) - | Union (t1,t2) -> assert(true : ('a,'b) CSig.union exists); - Printf.sprintf "((%s, %s) CSig.union)" (print_type t1) (print_type t2) - | State_id -> assert(true : Stateid.t exists); "Stateid.t" - - let document_type_encoding pr_xml = - Printf.printf "\n=== Data encoding by examples ===\n\n"; - Printf.printf "%s:\n\n%s\n\n" (print_type Unit) (pr_xml (of_unit ())); - Printf.printf "%s:\n\n%s\n%s\n\n" (print_type Bool) - (pr_xml (of_bool true)) (pr_xml (of_bool false)); - Printf.printf "%s:\n\n%s\n\n" (print_type String) (pr_xml (of_string "hello")); - Printf.printf "%s:\n\n%s\n\n" (print_type Int) (pr_xml (of_int 256)); - Printf.printf "%s:\n\n%s\n\n" (print_type State_id) (pr_xml (of_state_id Stateid.initial)); - Printf.printf "%s:\n\n%s\n\n" (print_type (List Int)) (pr_xml (of_list of_int [3;4;5])); - Printf.printf "%s:\n\n%s\n%s\n\n" (print_type (Option Int)) - (pr_xml (of_option of_int (Some 3))) (pr_xml (of_option of_int None)); - Printf.printf "%s:\n\n%s\n\n" (print_type (Pair (Bool,Int))) - (pr_xml (of_pair of_bool of_int (false,3))); - Printf.printf "%s:\n\n%s\n\n" (print_type (Union (Bool,Int))) - (pr_xml (of_union of_bool of_int (Inl false))); - print_endline ("All other types are records represented by a node named like the OCaml\n"^ - "type which contains a flattened n-tuple. We provide one example.\n"); - Printf.printf "%s:\n\n%s\n\n" (print_type Option_state) - (pr_xml (of_option_state { opt_sync = true; opt_depr = false; - opt_name = "name1"; opt_value = IntValue (Some 37) })); - -end -open ReifType - -(** Types reification, checked with explicit casts *) -let add_sty_t : add_sty val_t = - pair_t (pair_t string_t int_t) (pair_t state_id_t bool_t) -let edit_at_sty_t : edit_at_sty val_t = state_id_t -let query_sty_t : query_sty val_t = pair_t string_t state_id_t -let goals_sty_t : goals_sty val_t = unit_t -let evars_sty_t : evars_sty val_t = unit_t -let hints_sty_t : hints_sty val_t = unit_t -let status_sty_t : status_sty val_t = bool_t -let search_sty_t : search_sty val_t = list_t (pair_t search_cst_t bool_t) -let get_options_sty_t : get_options_sty val_t = unit_t -let set_options_sty_t : set_options_sty val_t = - list_t (pair_t (list_t string_t) option_value_t) -let mkcases_sty_t : mkcases_sty val_t = string_t -let quit_sty_t : quit_sty val_t = unit_t -let about_sty_t : about_sty val_t = unit_t -let init_sty_t : init_sty val_t = option_t string_t -let interp_sty_t : interp_sty val_t = pair_t (pair_t bool_t bool_t) string_t -let stop_worker_sty_t : stop_worker_sty val_t = int_t - -let add_rty_t : add_rty val_t = - pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t) -let edit_at_rty_t : edit_at_rty val_t = - union_t unit_t (pair_t state_id_t (pair_t state_id_t state_id_t)) -let query_rty_t : query_rty val_t = string_t -let goals_rty_t : goals_rty val_t = option_t goals_t -let evars_rty_t : evars_rty val_t = option_t (list_t evar_t) -let hints_rty_t : hints_rty val_t = - let hint = list_t (pair_t string_t string_t) in - option_t (pair_t (list_t hint) hint) -let status_rty_t : status_rty val_t = state_t -let search_rty_t : search_rty val_t = list_t (coq_object_t string_t) -let get_options_rty_t : get_options_rty val_t = - list_t (pair_t (list_t string_t) option_state_t) -let set_options_rty_t : set_options_rty val_t = unit_t -let mkcases_rty_t : mkcases_rty val_t = list_t (list_t string_t) -let quit_rty_t : quit_rty val_t = unit_t -let about_rty_t : about_rty val_t = coq_info_t -let init_rty_t : init_rty val_t = state_id_t -let interp_rty_t : interp_rty val_t = pair_t state_id_t (union_t string_t string_t) -let stop_worker_rty_t : stop_worker_rty val_t = unit_t - -let ($) x = erase x -let calls = [| - "Add", ($)add_sty_t, ($)add_rty_t; - "Edit_at", ($)edit_at_sty_t, ($)edit_at_rty_t; - "Query", ($)query_sty_t, ($)query_rty_t; - "Goal", ($)goals_sty_t, ($)goals_rty_t; - "Evars", ($)evars_sty_t, ($)evars_rty_t; - "Hints", ($)hints_sty_t, ($)hints_rty_t; - "Status", ($)status_sty_t, ($)status_rty_t; - "Search", ($)search_sty_t, ($)search_rty_t; - "GetOptions", ($)get_options_sty_t, ($)get_options_rty_t; - "SetOptions", ($)set_options_sty_t, ($)set_options_rty_t; - "MkCases", ($)mkcases_sty_t, ($)mkcases_rty_t; - "Quit", ($)quit_sty_t, ($)quit_rty_t; - "About", ($)about_sty_t, ($)about_rty_t; - "Init", ($)init_sty_t, ($)init_rty_t; - "Interp", ($)interp_sty_t, ($)interp_rty_t; - "StopWorker", ($)stop_worker_sty_t, ($)stop_worker_rty_t; -|] - -type 'a call = - | Add of add_sty - | Edit_at of edit_at_sty - | Query of query_sty - | Goal of goals_sty - | Evars of evars_sty - | Hints of hints_sty - | Status of status_sty - | Search of search_sty - | GetOptions of get_options_sty - | SetOptions of set_options_sty - | MkCases of mkcases_sty - | Quit of quit_sty - | About of about_sty - | Init of init_sty - | StopWorker of stop_worker_sty - (* retrocompatibility *) - | Interp of interp_sty - -let id_of_call = function - | Add _ -> 0 - | Edit_at _ -> 1 - | Query _ -> 2 - | Goal _ -> 3 - | Evars _ -> 4 - | Hints _ -> 5 - | Status _ -> 6 - | Search _ -> 7 - | GetOptions _ -> 8 - | SetOptions _ -> 9 - | MkCases _ -> 10 - | Quit _ -> 11 - | About _ -> 12 - | Init _ -> 13 - | Interp _ -> 14 - | StopWorker _ -> 15 - -let str_of_call c = pi1 calls.(id_of_call c) - -type unknown - -(** We use phantom types and GADT to protect ourselves against wild casts *) -let add x : add_rty call = Add x -let edit_at x : edit_at_rty call = Edit_at x -let query x : query_rty call = Query x -let goals x : goals_rty call = Goal x -let evars x : evars_rty call = Evars x -let hints x : hints_rty call = Hints x -let status x : status_rty call = Status x -let get_options x : get_options_rty call = GetOptions x -let set_options x : set_options_rty call = SetOptions x -let mkcases x : mkcases_rty call = MkCases x -let search x : search_rty call = Search x -let quit x : quit_rty call = Quit x -let init x : init_rty call = Init x -let interp x : interp_rty call = Interp x -let stop_worker x : stop_worker_rty call = StopWorker x - -let abstract_eval_call handler (c : 'a call) : 'a value = - let mkGood x : 'a value = Good (Obj.magic x) in - try - match c with - | Add x -> mkGood (handler.add x) - | Edit_at x -> mkGood (handler.edit_at x) - | Query x -> mkGood (handler.query x) - | Goal x -> mkGood (handler.goals x) - | Evars x -> mkGood (handler.evars x) - | Hints x -> mkGood (handler.hints x) - | Status x -> mkGood (handler.status x) - | Search x -> mkGood (handler.search x) - | GetOptions x -> mkGood (handler.get_options x) - | SetOptions x -> mkGood (handler.set_options x) - | MkCases x -> mkGood (handler.mkcases x) - | Quit x -> mkGood (handler.quit x) - | About x -> mkGood (handler.about x) - | Init x -> mkGood (handler.init x) - | Interp x -> mkGood (handler.interp x) - | StopWorker x -> mkGood (handler.stop_worker x) - with any -> - Fail (handler.handle_exn any) - -(** brain dead code, edit if protocol messages are added/removed *) -let of_answer (q : 'a call) (v : 'a value) : xml = match q with - | Add _ -> of_value (of_value_type add_rty_t ) (Obj.magic v) - | Edit_at _ -> of_value (of_value_type edit_at_rty_t ) (Obj.magic v) - | Query _ -> of_value (of_value_type query_rty_t ) (Obj.magic v) - | Goal _ -> of_value (of_value_type goals_rty_t ) (Obj.magic v) - | Evars _ -> of_value (of_value_type evars_rty_t ) (Obj.magic v) - | Hints _ -> of_value (of_value_type hints_rty_t ) (Obj.magic v) - | Status _ -> of_value (of_value_type status_rty_t ) (Obj.magic v) - | Search _ -> of_value (of_value_type search_rty_t ) (Obj.magic v) - | GetOptions _ -> of_value (of_value_type get_options_rty_t) (Obj.magic v) - | SetOptions _ -> of_value (of_value_type set_options_rty_t) (Obj.magic v) - | MkCases _ -> of_value (of_value_type mkcases_rty_t ) (Obj.magic v) - | Quit _ -> of_value (of_value_type quit_rty_t ) (Obj.magic v) - | About _ -> of_value (of_value_type about_rty_t ) (Obj.magic v) - | Init _ -> of_value (of_value_type init_rty_t ) (Obj.magic v) - | Interp _ -> of_value (of_value_type interp_rty_t ) (Obj.magic v) - | StopWorker _ -> of_value (of_value_type stop_worker_rty_t) (Obj.magic v) - -let to_answer (q : 'a call) (x : xml) : 'a value = match q with - | Add _ -> Obj.magic (to_value (to_value_type add_rty_t ) x) - | Edit_at _ -> Obj.magic (to_value (to_value_type edit_at_rty_t ) x) - | Query _ -> Obj.magic (to_value (to_value_type query_rty_t ) x) - | Goal _ -> Obj.magic (to_value (to_value_type goals_rty_t ) x) - | Evars _ -> Obj.magic (to_value (to_value_type evars_rty_t ) x) - | Hints _ -> Obj.magic (to_value (to_value_type hints_rty_t ) x) - | Status _ -> Obj.magic (to_value (to_value_type status_rty_t ) x) - | Search _ -> Obj.magic (to_value (to_value_type search_rty_t ) x) - | GetOptions _ -> Obj.magic (to_value (to_value_type get_options_rty_t) x) - | SetOptions _ -> Obj.magic (to_value (to_value_type set_options_rty_t) x) - | MkCases _ -> Obj.magic (to_value (to_value_type mkcases_rty_t ) x) - | Quit _ -> Obj.magic (to_value (to_value_type quit_rty_t ) x) - | About _ -> Obj.magic (to_value (to_value_type about_rty_t ) x) - | Init _ -> Obj.magic (to_value (to_value_type init_rty_t ) x) - | Interp _ -> Obj.magic (to_value (to_value_type interp_rty_t ) x) - | StopWorker _ -> Obj.magic (to_value (to_value_type stop_worker_rty_t) x) - -let of_call (q : 'a call) : xml = - let mkCall x = constructor "call" (str_of_call q) [x] in - match q with - | Add x -> mkCall (of_value_type add_sty_t x) - | Edit_at x -> mkCall (of_value_type edit_at_sty_t x) - | Query x -> mkCall (of_value_type query_sty_t x) - | Goal x -> mkCall (of_value_type goals_sty_t x) - | Evars x -> mkCall (of_value_type evars_sty_t x) - | Hints x -> mkCall (of_value_type hints_sty_t x) - | Status x -> mkCall (of_value_type status_sty_t x) - | Search x -> mkCall (of_value_type search_sty_t x) - | GetOptions x -> mkCall (of_value_type get_options_sty_t x) - | SetOptions x -> mkCall (of_value_type set_options_sty_t x) - | MkCases x -> mkCall (of_value_type mkcases_sty_t x) - | Quit x -> mkCall (of_value_type quit_sty_t x) - | About x -> mkCall (of_value_type about_sty_t x) - | Init x -> mkCall (of_value_type init_sty_t x) - | Interp x -> mkCall (of_value_type interp_sty_t x) - | StopWorker x -> mkCall (of_value_type stop_worker_sty_t x) - -let to_call : xml -> unknown call = - do_match "call" (fun s a -> - let mkCallArg vt a = to_value_type vt (singleton a) in - match s with - | "Add" -> Add (mkCallArg add_sty_t a) - | "Edit_at" -> Edit_at (mkCallArg edit_at_sty_t a) - | "Query" -> Query (mkCallArg query_sty_t a) - | "Goal" -> Goal (mkCallArg goals_sty_t a) - | "Evars" -> Evars (mkCallArg evars_sty_t a) - | "Hints" -> Hints (mkCallArg hints_sty_t a) - | "Status" -> Status (mkCallArg status_sty_t a) - | "Search" -> Search (mkCallArg search_sty_t a) - | "GetOptions" -> GetOptions (mkCallArg get_options_sty_t a) - | "SetOptions" -> SetOptions (mkCallArg set_options_sty_t a) - | "MkCases" -> MkCases (mkCallArg mkcases_sty_t a) - | "Quit" -> Quit (mkCallArg quit_sty_t a) - | "About" -> About (mkCallArg about_sty_t a) - | "Init" -> Init (mkCallArg init_sty_t a) - | "Interp" -> Interp (mkCallArg interp_sty_t a) - | "StopWorker" -> StopWorker (mkCallArg stop_worker_sty_t a) - | _ -> raise Marshal_error) - -(** misc *) - -let is_feedback = function - | Element ("feedback", _, _) -> true - | _ -> false - -(** Debug printing *) - -let pr_value_gen pr = function - | Good v -> "GOOD " ^ pr v - | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^str^"]" - | Fail (id,Some(i,j),str) -> - "FAIL "^Stateid.to_string id^ - " ("^string_of_int i^","^string_of_int j^")["^str^"]" -let pr_value v = pr_value_gen (fun _ -> "FIXME") v -let pr_full_value call value = match call with - | Add _ -> pr_value_gen (print add_rty_t ) (Obj.magic value) - | Edit_at _ -> pr_value_gen (print edit_at_rty_t ) (Obj.magic value) - | Query _ -> pr_value_gen (print query_rty_t ) (Obj.magic value) - | Goal _ -> pr_value_gen (print goals_rty_t ) (Obj.magic value) - | Evars _ -> pr_value_gen (print evars_rty_t ) (Obj.magic value) - | Hints _ -> pr_value_gen (print hints_rty_t ) (Obj.magic value) - | Status _ -> pr_value_gen (print status_rty_t ) (Obj.magic value) - | Search _ -> pr_value_gen (print search_rty_t ) (Obj.magic value) - | GetOptions _ -> pr_value_gen (print get_options_rty_t) (Obj.magic value) - | SetOptions _ -> pr_value_gen (print set_options_rty_t) (Obj.magic value) - | MkCases _ -> pr_value_gen (print mkcases_rty_t ) (Obj.magic value) - | Quit _ -> pr_value_gen (print quit_rty_t ) (Obj.magic value) - | About _ -> pr_value_gen (print about_rty_t ) (Obj.magic value) - | Init _ -> pr_value_gen (print init_rty_t ) (Obj.magic value) - | Interp _ -> pr_value_gen (print interp_rty_t ) (Obj.magic value) - | StopWorker _ -> pr_value_gen (print stop_worker_rty_t) (Obj.magic value) -let pr_call call = match call with - | Add x -> str_of_call call ^ " " ^ print add_sty_t x - | Edit_at x -> str_of_call call ^ " " ^ print edit_at_sty_t x - | Query x -> str_of_call call ^ " " ^ print query_sty_t x - | Goal x -> str_of_call call ^ " " ^ print goals_sty_t x - | Evars x -> str_of_call call ^ " " ^ print evars_sty_t x - | Hints x -> str_of_call call ^ " " ^ print hints_sty_t x - | Status x -> str_of_call call ^ " " ^ print status_sty_t x - | Search x -> str_of_call call ^ " " ^ print search_sty_t x - | GetOptions x -> str_of_call call ^ " " ^ print get_options_sty_t x - | SetOptions x -> str_of_call call ^ " " ^ print set_options_sty_t x - | MkCases x -> str_of_call call ^ " " ^ print mkcases_sty_t x - | Quit x -> str_of_call call ^ " " ^ print quit_sty_t x - | About x -> str_of_call call ^ " " ^ print about_sty_t x - | Init x -> str_of_call call ^ " " ^ print init_sty_t x - | Interp x -> str_of_call call ^ " " ^ print interp_sty_t x - | StopWorker x -> str_of_call call ^ " " ^ print stop_worker_sty_t x - -let document to_string_fmt = - Printf.printf "=== Available calls ===\n\n"; - Array.iter (fun (cname, csty, crty) -> - Printf.printf "%12s : %s\n %14s %s\n" - ("\""^cname^"\"") (print_type csty) "->" (print_type crty)) - calls; - Printf.printf "\n=== Calls XML encoding ===\n\n"; - Printf.printf "A call \"C\" carrying input a is encoded as:\n\n%s\n\n" - (to_string_fmt (constructor "call" "C" [PCData "a"])); - Printf.printf "A response carrying output b can either be:\n\n%s\n\n" - (to_string_fmt (of_value (fun _ -> PCData "b") (Good ()))); - Printf.printf "or:\n\n%s\n\nwhere the attributes loc_s and loc_c are optional.\n" - (to_string_fmt (of_value (fun _ -> PCData "b") - (Fail (Stateid.initial,Some (15,34),"error message")))); - document_type_encoding to_string_fmt - -(* vim: set foldmethod=marker: *) diff --git a/lib/serialize.mli b/lib/serialize.mli index b8bb1a33a..55c5ff041 100644 --- a/lib/serialize.mli +++ b/lib/serialize.mli @@ -6,61 +6,32 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** * Applicative part of the interface of CoqIde calls to Coq *) - -open Interface open Xml_datatype -type 'a call - -type unknown - -val add : add_sty -> add_rty call -val edit_at : edit_at_sty -> edit_at_rty call -val query : query_sty -> query_rty call -val goals : goals_sty -> goals_rty call -val hints : hints_sty -> hints_rty call -val status : status_sty -> status_rty call -val mkcases : mkcases_sty -> mkcases_rty call -val evars : evars_sty -> evars_rty call -val search : search_sty -> search_rty call -val get_options : get_options_sty -> get_options_rty call -val set_options : set_options_sty -> set_options_rty call -val quit : quit_sty -> quit_rty call -val init : init_sty -> init_rty call -val stop_worker : stop_worker_sty -> stop_worker_rty call -(* retrocompatibility *) -val interp : interp_sty -> interp_rty call - -val abstract_eval_call : handler -> 'a call -> 'a value - -(** * Protocol version *) - -val protocol_version : string - -(** * XML data marshalling *) - exception Marshal_error -val of_call : 'a call -> xml -val to_call : xml -> unknown call - -val of_message : message -> xml -val to_message : xml -> message -val is_message : xml -> bool - -val of_feedback : feedback -> xml -val to_feedback : xml -> feedback -val is_feedback : xml -> bool - -val of_answer : 'a call -> 'a value -> xml -val to_answer : 'a call -> xml -> 'a value - -(* Prints the documentation of this module *) -val document : (xml -> string) -> unit - -(** * Debug printing *) - -val pr_call : 'a call -> string -val pr_value : 'a value -> string -val pr_full_value : 'a call -> 'a value -> string +val massoc: string -> (string * string) list -> string +val constructor: string -> string -> xml list -> xml +val do_match: string -> (string -> xml list -> 'b) -> xml -> 'b +val singleton: 'a list -> 'a +val raw_string: xml list -> string +val of_unit: unit -> xml +val to_unit: xml -> unit +val of_bool: bool -> xml +val to_bool: xml -> bool +val of_list: ('a -> xml) -> 'a list -> xml +val to_list: (xml -> 'a) -> xml -> 'a list +val of_option: ('a -> xml) -> 'a option -> xml +val to_option: (xml -> 'a) -> xml -> 'a option +val of_string: string -> xml +val to_string: xml -> string +val of_int: int -> xml +val to_int: xml -> int +val of_pair: ('a -> xml) -> ('b -> xml) -> 'a * 'b -> xml +val to_pair: (xml -> 'a) -> (xml -> 'b) -> xml -> 'a * 'b +val of_union: ('a -> xml) -> ('b -> xml) -> ('a, 'b) CSig.union -> xml +val to_union: (xml -> 'a) -> (xml -> 'b) -> xml -> ('a, 'b) CSig.union +val of_edit_id: int -> xml +val to_edit_id: xml -> int +val of_loc : Loc.t -> xml +val to_loc : xml -> Loc.t diff --git a/library/goptions.ml b/library/goptions.ml index 8402abd34..c348548e7 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -15,9 +15,19 @@ open Libobject open Libnames open Mod_subst -open Interface - -type option_name = Interface.option_name +type option_name = string list +type option_value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + +(** Summary of an option status *) +type option_state = { + opt_sync : bool; + opt_depr : bool; + opt_name : string; + opt_value : option_value; +} (****************************************************************************) (* 0- Common things *) @@ -354,7 +364,6 @@ let print_option_value key = | _ -> msg_info (str ("Current value of "^name^" is ") ++ msg_option_value (name, s)) - let get_tables () = let tables = !value_tab in let fold key (name, depr, (sync,read,_,_,_)) accu = diff --git a/library/goptions.mli b/library/goptions.mli index 6251b8d2d..f249a97be 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -47,7 +47,7 @@ open Pp open Libnames open Mod_subst -type option_name = Interface.option_name +type option_name = string list (** {6 Tables. } *) @@ -161,7 +161,20 @@ val set_string_option_value : option_name -> string -> unit val print_option_value : option_name -> unit -val get_tables : unit -> Interface.option_state OptionMap.t +type option_value = + | BoolValue of bool + | IntValue of int option + | StringValue of string + +(** Summary of an option status *) +type option_state = { + opt_sync : bool; + opt_depr : bool; + opt_name : string; + opt_value : option_value; +} + +val get_tables : unit -> option_state OptionMap.t val print_tables : unit -> std_ppcmds val error_undeclared_key : option_name -> 'a diff --git a/stm/lemmas.ml b/stm/lemmas.ml index c40000811..5d2babaca 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -323,7 +323,7 @@ let standard_proof_terminator compute_guard hook = let open Proof_global in function | Admitted -> admit hook (); - Pp.feedback Interface.AddedAxiom + Pp.feedback Feedback.AddedAxiom | Proved (is_opaque,idopt,proof) -> let proof = get_proof proof compute_guard hook is_opaque in begin match idopt with @@ -337,7 +337,7 @@ let universe_proof_terminator compute_guard hook = let open Proof_global in function | Admitted -> admit (hook Evd.empty_evar_universe_context) (); - Pp.feedback Interface.AddedAxiom + Pp.feedback Feedback.AddedAxiom | Proved (is_opaque,idopt,proof) -> let proof = get_proof proof compute_guard (hook proof.Proof_global.universes) is_opaque in diff --git a/stm/stm.ml b/stm/stm.ml index 85c3838dc..b53c9fcf8 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -51,7 +51,7 @@ let vernac_interp ?proof id { verbose; loc; expr } = if internal_command expr then begin prerr_endline ("ignoring " ^ string_of_ppcmds(pr_vernac expr)) end else begin - Pp.set_id_for_feedback (Interface.State id); + Pp.set_id_for_feedback (Feedback.State id); Aux_file.record_in_aux_set_at loc; prerr_endline ("interpreting " ^ string_of_ppcmds(pr_vernac expr)); let interp = Hook.get f_interp in @@ -63,7 +63,7 @@ let vernac_interp ?proof id { verbose; loc; expr } = (* Wrapper for Vernac.parse_sentence to set the feedback id *) let vernac_parse eid s = - set_id_for_feedback (Interface.Edit eid); + set_id_for_feedback (Feedback.Edit eid); let pa = Pcoq.Gram.parsable (Stream.of_string s) in Flags.with_option Flags.we_are_parsing (fun () -> match Pcoq.Gram.entry_parse Pcoq.main_entry pa with @@ -570,7 +570,7 @@ end = struct | None -> let loc = Option.default Loc.ghost (Loc.get_loc e) in let msg = string_of_ppcmds (print e) in - Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg)); + Pp.feedback ~state_id:id (Feedback.ErrorMsg (loc, msg)); Stateid.add (Hook.get f_process_error e) ?valid id let define ?(redefine=false) ?(cache=`No) f id = @@ -585,7 +585,7 @@ end = struct else if cache = `Shallow then freeze `Shallow id; prerr_endline ("setting cur id to "^str_id); cur_id := id; - feedback ~state_id:id Interface.Processed; + feedback ~state_id:id Feedback.Processed; VCS.reached id true; if Proof_global.there_are_pending_proofs () then VCS.goals id (Proof_global.get_open_goals ()); @@ -687,7 +687,7 @@ end = struct | RespError of (* err, safe, msg, safe_states *) Stateid.t * Stateid.t * std_ppcmds * (Stateid.t * State.frozen_state) list - | RespFeedback of Interface.feedback + | RespFeedback of Feedback.feedback | RespGetCounterNewUnivLevel type more_data = @@ -825,8 +825,6 @@ end = struct with Not_found -> 0.0 in s,max (time1 +. time2) 0.0001,i) 0 l - open Interface - exception MarshalError of string let marshal_to_channel oc data = @@ -900,7 +898,7 @@ end = struct else let f, assign = Future.create_delegate (State.exn_on id ~valid) in let uuid = Future.uuid f in - Pp.feedback (Interface.InProgress 1); + Pp.feedback (Feedback.InProgress 1); TQueue.push queue (TaskBuildProof (exn_info,start,stop,assign,cancel_switch,loc,uuid,name)); f, cancel_switch @@ -920,7 +918,7 @@ end = struct match !Flags.async_proofs_mode with | Flags.APonParallel n -> n | _ -> assert false in - Pp.feedback ~state_id:Stateid.initial (Interface.SlaveStatus(id, s)) + Pp.feedback ~state_id:Stateid.initial (Feedback.SlaveStatus(id, s)) let rec manage_slave ~cancel:cancel_user_req id_slave respawn = let ic, oc, proc = @@ -962,7 +960,7 @@ end = struct RespBuiltProof(pl, time)-> assign (`Val pl); (* We restart the slave, to avoid memory leaks. We could just - Pp.feedback (Interface.InProgress ~-1) *) + Pp.feedback (Feedback.InProgress ~-1) *) record_pb_time s loc time; last_task := None; raise KillRespawn @@ -972,7 +970,7 @@ end = struct assign (`Exn e); List.iter (fun (id,s) -> State.assign id s) valid_states; (* We restart the slave, to avoid memory leaks. We could just - Pp.feedback (Interface.InProgress ~-1) *) + Pp.feedback (Feedback.InProgress ~-1) *) last_task := None; raise KillRespawn (* marshal_more_data oc (MoreDataLocalUniv *) @@ -982,7 +980,7 @@ end = struct marshal_more_data oc (MoreDataUnivLevel (CList.init 10 (fun _ -> Universes.new_univ_level (Global.current_dirpath ())))); loop () - | _, RespFeedback {id = State state_id; content = msg} -> + | _, RespFeedback {Feedback.id = Feedback.State state_id; content = msg} -> Pp.feedback ~state_id msg; loop () | _, RespFeedback _ -> assert false (* Parsing in master process *) @@ -990,7 +988,7 @@ end = struct loop () with | VCS.Expired -> (* task cancelled: e.g. the user did backtrack *) - Pp.feedback (Interface.InProgress ~-1); + Pp.feedback (Feedback.InProgress ~-1); prerr_endline ("Task expired: " ^ pr_task task) | (Sys_error _ | Invalid_argument _ | End_of_file | KillRespawn) as e -> raise e (* we pass the exception to the external handler *) @@ -1000,7 +998,7 @@ end = struct "Falling back to local, lazy, evaluation.")); let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in assign(`Comp(build_proof_here exn_info loc stop)); - Pp.feedback (Interface.InProgress ~-1) + Pp.feedback (Feedback.InProgress ~-1) | MarshalError s -> pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 1 @@ -1011,11 +1009,11 @@ end = struct done with | KillRespawn -> - Pp.feedback (Interface.InProgress ~-1); + Pp.feedback (Feedback.InProgress ~-1); Worker.kill proc; ignore(Worker.wait proc); manage_slave ~cancel:cancel_user_req id_slave respawn | Sys_error _ | Invalid_argument _ | End_of_file when !task_expired -> - Pp.feedback (Interface.InProgress ~-1); + Pp.feedback (Feedback.InProgress ~-1); ignore(Worker.wait proc); manage_slave ~cancel:cancel_user_req id_slave respawn | Sys_error _ | Invalid_argument _ | End_of_file when !task_cancelled -> @@ -1025,8 +1023,8 @@ end = struct let s = "Worker cancelled by the user" in let e = Stateid.add ~valid:start (RemoteException (strbrk s)) start in assign (`Exn e); - Pp.feedback ~state_id:start (Interface.ErrorMsg (Loc.ghost, s)); - Pp.feedback (Interface.InProgress ~-1); + Pp.feedback ~state_id:start (Feedback.ErrorMsg (Loc.ghost, s)); + Pp.feedback (Feedback.InProgress ~-1); ) !last_task; Worker.kill proc; ignore(Worker.wait proc); manage_slave ~cancel:cancel_user_req id_slave respawn @@ -1037,7 +1035,7 @@ end = struct msg_warning(strbrk "Falling back to local, lazy, evaluation."); let TaskBuildProof (exn_info, _, stop, assign,_,loc,_,_) = task in assign(`Comp(build_proof_here exn_info loc stop)); - Pp.feedback (Interface.InProgress ~-1); + Pp.feedback (Feedback.InProgress ~-1); ) !last_task; Worker.kill proc; ignore(Worker.wait proc); manage_slave ~cancel:cancel_user_req id_slave respawn @@ -1252,7 +1250,7 @@ let known_state ?(redefine_qed=false) ~cache id = prerr_endline ("reaching: " ^ Stateid.to_string id); if not redefine_qed && State.is_cached id then begin State.install_cached id; - feedback ~state_id:id Interface.Processed; + feedback ~state_id:id Feedback.Processed; prerr_endline ("reached (cache)") end else let step, cache_step = @@ -1292,7 +1290,7 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.close_future_proof ~feedback_id:id fp in reach view.next; vernac_interp id ~proof x; - feedback ~state_id:id Interface.Incomplete + feedback ~state_id:id Feedback.Incomplete | VtDrop, _, _ -> reach view.next; Option.iter (vernac_interp start) proof_using_ast; @@ -1347,7 +1345,7 @@ let known_state ?(redefine_qed=false) ~cache id = ), cache in if !Flags.async_proofs_mode = Flags.APonParallel 0 then - Pp.feedback ~state_id:id Interface.ProcessingInMaster; + Pp.feedback ~state_id:id Feedback.ProcessingInMaster; State.define ~cache:cache_step ~redefine:redefine_qed step id; prerr_endline ("reached: "^ Stateid.to_string id) in reach ~redefine_qed id diff --git a/stm/stm.mli b/stm/stm.mli index a58100b5a..fd306425c 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -7,8 +7,8 @@ (************************************************************************) open Vernacexpr -open Interface open Names +open Feedback (** state-transaction-machine interface *) diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 068dfb2ee..df114d059 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -20,23 +20,23 @@ type coqtop = { let logger level content = prerr_endline content let base_eval_call ?(print=true) ?(fail=true) call coqtop = - if print then prerr_endline (Serialize.pr_call call); - let xml_query = Serialize.of_call call in + if print then prerr_endline (Xmlprotocol.pr_call call); + let xml_query = Xmlprotocol.of_call call in Xml_printer.print coqtop.xml_printer xml_query; let rec loop () = let xml = Xml_parser.parse coqtop.xml_parser in - if Serialize.is_message xml then - let message = Serialize.to_message xml in - let level = message.Interface.message_level in - let content = message.Interface.message_content in + if Pp.is_message xml then + let message = Pp.to_message xml in + let level = message.Pp.message_level in + let content = message.Pp.message_content in logger level content; loop () - else if Serialize.is_feedback xml then + else if Feedback.is_feedback xml then loop () - else (Serialize.to_answer call xml) + else (Xmlprotocol.to_answer call xml) in let res = loop () in - if print then prerr_endline (Serialize.pr_full_value call res); + if print then prerr_endline (Xmlprotocol.pr_full_value call res); match res with | Interface.Fail (_,_,s) when fail -> error s | Interface.Fail (_,_,s) as x -> prerr_endline s; x @@ -224,7 +224,7 @@ module GUILogic = struct let to_id, need_unfocus = get_id_pred (fun id _ -> Stateid.equal id safe_id) in after_edit_at (to_id, need_unfocus) - (base_eval_call (Serialize.edit_at to_id) coq) + (base_eval_call (Xmlprotocol.edit_at to_id) coq) | Interface.Good _ -> error "The command was expected to fail but did not" end @@ -233,7 +233,7 @@ open GUILogic let eval_print l coq = let open Parser in - let open Serialize in + let open Xmlprotocol in (* prerr_endline ("Interpreting: " ^ print_toklist l); *) match l with | [ Tok(_,"ADD"); Top []; Tok(_,phrase) ] -> @@ -311,15 +311,15 @@ let main = Xml_parser.check_eof ip false; { xml_printer = op; xml_parser = ip } in let init () = - match base_eval_call ~print:false (Serialize.init None) coq with + match base_eval_call ~print:false (Xmlprotocol.init None) coq with | Interface.Good id -> let dir = Filename.dirname input_file in let phrase = Printf.sprintf "Add LoadPath \"%s\". " dir in let eid, tip = add_sentence ~name:"initial" phrase in - after_add (base_eval_call (Serialize.add ((phrase,eid),(tip,true))) coq) + after_add (base_eval_call (Xmlprotocol.add ((phrase,eid),(tip,true))) coq) | Interface.Fail _ -> error "init call failed" in let finish () = - match base_eval_call (Serialize.status true) coq with + match base_eval_call (Xmlprotocol.status true) coq with | Interface.Good _ -> exit 0 | Interface.Fail (_,_,s) -> error s in (* The main loop *) diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 45aa980b7..2f778be36 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -95,7 +95,7 @@ let init_load_path () = (* main loops *) Mltop.add_ml_dir (coqlib/"toploop"); if Coq_config.local then Mltop.add_ml_dir (coqlib/"stm"); - if Coq_config.local then Mltop.add_ml_dir (coqlib/"idetop"); + if Coq_config.local then Mltop.add_ml_dir (coqlib/"ide"); (* then standard library *) add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false; (* then plugins *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 0523ffd44..d64e3d979 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -389,8 +389,6 @@ let parse_args arglist = |"-emacs" -> set_emacs () |"-filteropts" -> filter_opts := true |"-h"|"-H"|"-?"|"-help"|"--help" -> usage () - |"--help-XML-protocol" -> - Serialize.document Xml_printer.to_string_fmt; exit 0 |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet |"-indices-matter" -> Indtypes.enforce_indices_matter () diff --git a/toplevel/search.ml b/toplevel/search.ml index 37403504d..016b9f22b 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -217,26 +217,39 @@ let search_about items mods = let () = generic_search iter in format_display !ans +type search_constraint = + | Name_Pattern of string + | Type_Pattern of string + | SubType_Pattern of string + | In_Module of string list + | Include_Blacklist + +type 'a coq_object = { + coq_object_prefix : string list; + coq_object_qualid : string list; + coq_object_object : 'a; +} + let interface_search flags = let env = Global.env () in let rec extract_flags name tpe subtpe mods blacklist = function | [] -> (name, tpe, subtpe, mods, blacklist) - | (Interface.Name_Pattern s, b) :: l -> + | (Name_Pattern s, b) :: l -> let regexp = try Str.regexp s with e when Errors.noncritical e -> Errors.error ("Invalid regexp: " ^ s) in extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l - | (Interface.Type_Pattern s, b) :: l -> + | (Type_Pattern s, b) :: l -> let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in let (_, pat) = Constrintern.intern_constr_pattern env constr in extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l - | (Interface.SubType_Pattern s, b) :: l -> + | (SubType_Pattern s, b) :: l -> let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in let (_, pat) = Constrintern.intern_constr_pattern env constr in extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l - | (Interface.In_Module m, b) :: l -> + | (In_Module m, b) :: l -> let path = String.concat "." m in let m = Pcoq.parse_string Pcoq.Constr.global path in let (_, qid) = Libnames.qualid_of_reference m in @@ -246,7 +259,7 @@ let interface_search flags = Errors.error ("Module " ^ path ^ " not found.") in extract_flags name tpe subtpe ((id, b) :: mods) blacklist l - | (Interface.Include_Blacklist, b) :: l -> + | (Include_Blacklist, b) :: l -> extract_flags name tpe subtpe mods b l in let (name, tpe, subtpe, mods, blacklist) = @@ -295,9 +308,9 @@ let interface_search flags = in let (prefix, qualid) = prefix fullpath shortpath [Id.to_string basename] in let answer = { - Interface.coq_object_prefix = prefix; - Interface.coq_object_qualid = qualid; - Interface.coq_object_object = string_of_ppcmds (pr_lconstr_env env constr); + coq_object_prefix = prefix; + coq_object_qualid = qualid; + coq_object_object = string_of_ppcmds (pr_lconstr_env env constr); } in ans := answer :: !ans; in diff --git a/toplevel/search.mli b/toplevel/search.mli index c06a64be1..a69a8db79 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -40,8 +40,27 @@ val search_rewrite : constr_pattern -> DirPath.t list * bool -> std_ppcmds val search_pattern : constr_pattern -> DirPath.t list * bool -> std_ppcmds val search_about : (bool * glob_search_about_item) list -> DirPath.t list * bool -> std_ppcmds -val interface_search : (Interface.search_constraint * bool) list -> - string Interface.coq_object list + +type search_constraint = + (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *) + | Name_Pattern of string + (** Whether the object type satisfies a pattern *) + | Type_Pattern of string + (** Whether some subtype of object type satisfies a pattern *) + | SubType_Pattern of string + (** Whether the object pertains to a module *) + | In_Module of string list + (** Bypass the Search blacklist *) + | Include_Blacklist + +type 'a coq_object = { + coq_object_prefix : string list; + coq_object_qualid : string list; + coq_object_object : 'a; +} + +val interface_search : (search_constraint * bool) list -> + string coq_object list (** {6 Generic search function} *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2e97b74d6..b1ed564d8 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -517,7 +517,7 @@ let vernac_exact_proof c = called only at the begining of a proof. *) let status = by (Tactics.New.exact_proof c) in save_proof (Vernacexpr.Proved(true,None)); - if not status then Pp.feedback Interface.AddedAxiom + if not status then Pp.feedback Feedback.AddedAxiom let vernac_assumption locality poly (local, kind) l nl = let local = enforce_locality_exp locality local in @@ -529,7 +529,7 @@ let vernac_assumption locality poly (local, kind) l nl = if global then Dumpglob.dump_definition lid false "ax" else Dumpglob.dump_definition lid true "var") idl) l; let status = do_assumptions kind nl l in - if not status then Pp.feedback Interface.AddedAxiom + if not status then Pp.feedback Feedback.AddedAxiom let vernac_record k poly finite infer struc binders sort nameopt cfs = let const = match nameopt with @@ -795,7 +795,7 @@ let vernac_instance abst locality poly sup inst props pri = ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri) let vernac_context poly l = - if not (Classes.context poly l) then Pp.feedback Interface.AddedAxiom + if not (Classes.context poly l) then Pp.feedback Feedback.AddedAxiom let vernac_declare_instances locality ids pri = let glob = not (make_section_locality locality) in @@ -825,7 +825,7 @@ let vernac_solve n tcom b = let p = Proof.maximal_unfocus command_focus p in p,status) in print_subgoals(); - if not status then Pp.feedback Interface.AddedAxiom + if not status then Pp.feedback Feedback.AddedAxiom (* A command which should be a tactic. It has been -- cgit v1.2.3