diff options
99 files changed, 2732 insertions, 1309 deletions
diff --git a/Makefile.build b/Makefile.build index 6d12063ca8..6bd6386562 100644 --- a/Makefile.build +++ b/Makefile.build @@ -210,7 +210,7 @@ miniopt: $(COQTOPEXE) pluginsopt minibyte: $(COQTOPBYTE) pluginsbyte ifeq ($(BEST),opt) -$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) +$(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -thread -o $@ $(STRIP) $@ @@ -219,7 +219,7 @@ $(COQTOPEXE): $(COQTOPBYTE) cp $< $@ endif -$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) +$(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -thread -o $@ @@ -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 @@ -301,8 +301,8 @@ IDEFILES=$(wildcard ide/coq*.lang) ide/coq_style.xml ide/coq.png ide/mac_default coqide-binaries: coqide-$(HASCOQIDE) coqide-no: -coqide-byte: $(COQIDEBYTE) $(COQIDE) -coqide-opt: $(COQIDEBYTE) $(COQIDE) +coqide-byte: $(COQIDEBYTE) $(COQIDE) $(IDETOPLOOPCMA) +coqide-opt: $(COQIDEBYTE) $(COQIDE) $(IDETOPLOOPCMA) $(IDETOPLOOPCMA:.cma=.cmxs) coqide-files: $(IDEFILES) ifeq ($(HASCOQIDE),opt) @@ -334,6 +334,11 @@ endif install-ide-bin: $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQIDE) $(FULLBINDIR) + $(MKDIR) $(FULLCOQLIB)/toploop + $(INSTALLBIN) $(IDETOPLOOPCMA) $(FULLCOQLIB)/toploop/ +ifeq ($(BEST),opt) + $(INSTALLBIN) $(IDETOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ +endif install-ide-devfiles: $(MKDIR) $(FULLCOQLIB) @@ -531,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) @@ -618,6 +623,12 @@ install-coqlight: install-binaries install-library-light install-binaries: install-tools $(MKDIR) $(FULLBINDIR) $(INSTALLBIN) $(COQC) $(COQTOPBYTE) $(COQTOPEXE) $(CHICKEN) $(FULLBINDIR) + $(MKDIR) $(FULLCOQLIB)/toploop + $(INSTALLBIN) $(TOPLOOPCMA) $(FULLCOQLIB)/toploop/ +ifeq ($(BEST),opt) + $(INSTALLBIN) $(TOPLOOPCMA:.cma=.cmxs) $(FULLCOQLIB)/toploop/ +endif + install-tools: $(MKDIR) $(FULLBINDIR) diff --git a/Makefile.common b/Makefile.common index d971e9b2eb..8a70273ad0 100644 --- a/Makefile.common +++ b/Makefile.common @@ -75,8 +75,7 @@ SRCDIRS:=\ 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 @@ -159,6 +158,8 @@ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma tactics/hightactics.cma +TOPLOOPCMA:=stm/stmworkertop.cma + GRAMMARCMA:=tools/compat5.cmo grammar/grammar.cma OMEGACMA:=plugins/omega/omega_plugin.cma @@ -212,6 +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=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 @@ -224,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 766eb41827..cbabd208c9 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 81fcc8493f..dcd3f0efbf 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 338d44fbf9..a18951f4bb 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 af00cc63cd..c1555e57f2 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 542cc44620..966c77700e 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 ab1a86f78a..cefe18092b 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 e20c95b9eb..9614c6f3b1 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 0000000000..92301dc30e --- /dev/null +++ b/ide/coqidetop.mllib @@ -0,0 +1,2 @@ +Xmlprotocol +Ide_slave diff --git a/ide/ide.mllib b/ide/ide.mllib index 8bc1337ff1..9444761716 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/toplevel/ide_slave.ml b/ide/ide_slave.ml index 8f2fa69a00..6b2c52123d 100644 --- a/toplevel/ide_slave.ml +++ b/ide/ide_slave.ml @@ -50,9 +50,9 @@ 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) + if !Flags.debug then pr_with_pid ("<-- " ^ Xmlprotocol.pr_call q) let pr_debug_answer q r = - if !Flags.debug then pr_with_pid ("--> " ^ Serialize.pr_full_value q r) + if !Flags.debug then pr_with_pid ("--> " ^ Xmlprotocol.pr_full_value q r) (** Categories of commands *) @@ -277,7 +277,7 @@ let set_options options = let about () = { Interface.coqtop_version = Coq_config.version; - Interface.protocol_version = Serialize.protocol_version; + Interface.protocol_version = Xmlprotocol.protocol_version; Interface.release_date = Coq_config.date; Interface.compile_date = Coq_config.compile_date; } @@ -365,7 +365,7 @@ let eval_call xml_oc log c = Interface.handle_exn = handle_exn; Interface.stop_worker = Stm.stop_worker; } in - Serialize.abstract_eval_call handler c + Xmlprotocol.abstract_eval_call handler c (** Message dispatching. Since coqtop -ideslave starts 1 thread per slave, and each @@ -384,15 +384,15 @@ 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; + Pp.message_level = level; + Pp.message_content = msg; } in let () = pr_debug (Printf.sprintf "-> %S" msg) in - let xml = Serialize.of_message message in + let xml = Pp.of_message message in print_xml xml_oc xml let slave_feeder xml_oc msg = - let xml = Serialize.of_feedback msg in + let xml = Feedback.of_feedback msg in print_xml xml_oc xml (** The main loop *) @@ -421,12 +421,12 @@ let loop () = 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 q = Xmlprotocol.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 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 (Serialize.of_answer q r)); *) - print_xml xml_oc (Serialize.of_answer q r); +(* 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, _) -> @@ -444,3 +444,17 @@ let loop () = 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 d8ca34f982..32d2bb97b3 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 5fd97e3a55..5877d1270a 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/lib/interface.mli b/ide/interface.mli index c8fe068e60..4e5e4a9cd7 100644 --- a/lib/interface.mli +++ b/ide/interface.mli @@ -55,13 +55,13 @@ type hint = (string * string) list type option_name = string list -type option_value = +type option_value = Goptions.option_value = | BoolValue of bool | IntValue of int option | StringValue of string (** Summary of an option status *) -type option_state = { +type option_state = Goptions.option_state = { opt_sync : bool; (** Whether an option is synchronous *) opt_depr : bool; @@ -72,7 +72,7 @@ type option_state = { (** The current value of the option *) } -type search_constraint = +type search_constraint = Search.search_constraint = (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *) | Name_Pattern of string (** Whether the object type satisfies a pattern *) @@ -92,7 +92,7 @@ type search_flags = (search_constraint * bool) list the user. [coq_object_prefix] is the missing part to recover the fully qualified name, i.e [fully_qualified = coq_object_prefix + coq_object_qualid]. [coq_object_object] is the actual content of the object. *) -type 'a coq_object = { +type 'a coq_object = 'a Search.coq_object = { coq_object_prefix : string list; coq_object_qualid : string list; coq_object_object : 'a; @@ -105,45 +105,11 @@ type coq_info = { compile_date : string; } -(** Coq unstructured messages *) - -type message_level = - | Debug of string - | Info - | Notice - | Warning - | Error - -type message = { - message_level : message_level; - message_content : string; -} - -(** Coq "semantic" infos obtained during parsing/execution *) -type edit_id = int -type state_id = Stateid.t -type edit_or_state_id = Edit of edit_id | State of state_id - -type feedback_content = - | AddedAxiom - | Processed - | Incomplete - | Complete - | GlobRef of Loc.t * string * string * string * string - | GlobDef of Loc.t * string * string * string - | ErrorMsg of Loc.t * string - | InProgress of int - | SlaveStatus of int * string - | ProcessingInMaster - -type feedback = { - id : edit_or_state_id; - content : feedback_content; -} - (** Calls result *) type location = (int * int) option (* start and end of the error *) +type state_id = Feedback.state_id +type edit_id = Feedback.edit_id (* The fail case carries the current state_id of the prover, the GUI should probably retract to that point *) diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index f58cdc6477..cd3e311358 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 cb84ae7337..8a0a2bd851 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 0000000000..09626172de --- /dev/null +++ b/ide/xmlprotocol.ml @@ -0,0 +1,701 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * 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 Serialize +open Xml_datatype + +(* Marshalling of basic types and type constructors *) +module Xml_marshalling = struct + +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_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 0000000000..42defce85b --- /dev/null +++ b/ide/xmlprotocol.mli @@ -0,0 +1,56 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * 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 *) + +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/interp/dumpglob.ml b/interp/dumpglob.ml index 80b5830fd1..bf9d2c0b99 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 89e1b41f39..af65f65414 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 f38ad47420..9f30b7da38 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/kernel/univ.ml b/kernel/univ.ml index 7c9a5ca322..1e7d2c83cb 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -223,7 +223,7 @@ module HList = struct let rec mem e l = match l.Hcons.node with | Nil -> false - | Cons (x, ll) -> x == e || mem e ll + | Cons (x, ll) -> H.equal x e || mem e ll let rec compare cmp l1 l2 = if l1 == l2 then 0 diff --git a/lib/clib.mllib b/lib/clib.mllib index ed4894cb93..73839fd9e5 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 0000000000..b532c26533 --- /dev/null +++ b/lib/feedback.ml @@ -0,0 +1,96 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Xml_datatype +open Serialize + +type edit_id = int +type state_id = Stateid.t +type edit_or_state_id = Edit of edit_id | State of state_id + +type feedback_content = + | AddedAxiom + | Processed + | Incomplete + | Complete + | GlobRef of Loc.t * string * string * string * string + | GlobDef of Loc.t * string * string * string + | ErrorMsg of Loc.t * string + | InProgress of int + | SlaveStatus of int * string + | ProcessingInMaster + +type feedback = { + id : edit_or_state_id; + content : feedback_content; +} + +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_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 0000000000..e7645ca169 --- /dev/null +++ b/lib/feedback.mli @@ -0,0 +1,36 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Xml_datatype + +(** Coq "semantic" infos obtained during parsing/execution *) +type edit_id = int +type state_id = Stateid.t +type edit_or_state_id = Edit of edit_id | State of state_id + +type feedback_content = + | AddedAxiom + | Processed + | Incomplete + | Complete + | GlobRef of Loc.t * string * string * string * string + | GlobDef of Loc.t * string * string * string + | ErrorMsg of Loc.t * string + | InProgress of int + | SlaveStatus of int * string + | ProcessingInMaster + +type feedback = { + id : edit_or_state_id; + content : feedback_content; +} + +val of_feedback : feedback -> xml +val to_feedback : xml -> feedback +val is_feedback : xml -> bool + @@ -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 635a149e88..fe11619c1d 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 042b75e2d4..7c0c6b86ee 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 b8bb1a33a3..55c5ff041f 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 8402abd342..c348548e72 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 6251b8d2d2..f249a97be7 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/pretyping/cases.ml b/pretyping/cases.ml index b5aeeae3ab..3f1bead369 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1559,7 +1559,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t = map_constr_with_full_binders push_binder aux x t | Evar ev -> let ty = get_type_of env sigma t in - let ty = Evarutil.evd_comb1 (refresh_universes false env) evdref ty in + let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in let inst = List.map_i (fun i _ -> @@ -1577,7 +1577,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t = let vl = List.map pi1 good in let ty = let ty = get_type_of env !evdref t in - Evarutil.evd_comb1 (refresh_universes false env) evdref ty + Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in let ty = lift (-k) (aux x ty) in let depvl = free_rels ty in @@ -2155,6 +2155,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in + let _btype = evd_comb1 (Typing.e_type_of env) evdref bbody in let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in let branch = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 2761dcbe33..e9d152de2d 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -882,7 +882,8 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = force_instantiation evd !evsref | [] -> let evd = - try Evarsolve.check_evar_instance evd evk rhs (evar_conv_x ts) + try Evarsolve.check_evar_instance evd evk rhs + (evar_conv_x full_transparent_state) with IllTypedInstance _ -> raise (TypingFailed evd) in Evd.define evk rhs evd diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 9522f9c249..13421bcde4 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -42,7 +42,12 @@ let get_polymorphic_positions f = templ.template_param_levels) | _ -> assert false -let refresh_universes ?(onlyalg=false) dir env evd t = +(** + forall A (l : list A) -> typeof A = Type i <= Datatypes.j -> i not refreshed + hd ?A (l : list t) -> A = t + +*) +let refresh_universes ?(onlyalg=false) pbty env evd t = let evdref = ref evd in let modified = ref false in let rec refresh dir t = @@ -88,7 +93,10 @@ let refresh_universes ?(onlyalg=false) dir env evd t = in aux 0 pos in let t' = - if isArity t then refresh dir t + if isArity t then + (match pbty with + | None -> t + | Some dir -> refresh dir t) else (refresh_term_evars false t; t) in if !modified then !evdref, t' else !evdref, t @@ -553,7 +561,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let id = next_name_away na avoid in let evd,t_in_sign = let s = Retyping.get_sort_of env evd t_in_env in - let evd,ty_t_in_sign = refresh_universes false env evd (mkSort s) in + let evd,ty_t_in_sign = refresh_universes (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd t_in_env ty_t_in_sign sign filter inst_in_env in let evd,b_in_sign = match b with @@ -572,7 +580,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = in let evd,ev2ty_in_sign = let s = Retyping.get_sort_of env evd ty_in_env in - let evd,ty_t_in_sign = refresh_universes false env evd (mkSort s) in + let evd,ty_t_in_sign = refresh_universes (Some false) env evd (mkSort s) in define_evar_from_virtual_equation define_fun env evd ty_in_env ty_t_in_sign sign2 filter2 inst2_in_env in let evd,ev2_in_sign = @@ -1417,7 +1425,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = * context "hyps" and not referring to itself. *) -and evar_define conv_algo ?(choose=false) ?(dir=false) env evd pbty (evk,argsv as ev) rhs = +and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = match kind_of_term rhs with | Evar (evk2,argsv2 as ev2) -> if Evar.equal evk evk2 then @@ -1436,7 +1444,7 @@ and evar_define conv_algo ?(choose=false) ?(dir=false) env evd pbty (evk,argsv a (* so we recheck acyclicity *) if occur_evar evk body then raise (OccurCheckIn (evd',body)); (* needed only if an inferred type *) - let evd', body = refresh_universes dir env evd' body in + let evd', body = refresh_universes pbty env evd' body in (* Cannot strictly type instantiations since the unification algorithm * does not unify applications from left to right. * e.g problem f x == g y yields x==y and f==g (in that order) @@ -1520,8 +1528,7 @@ let reconsider_conv_pbs conv_algo evd = let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) = try let t2 = whd_betaiota evd t2 in (* includes whd_evar *) - let dir = match pbty with Some d -> d | None -> false in - let evd = evar_define conv_algo ~choose ~dir env evd pbty ev1 t2 in + let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in reconsider_conv_pbs conv_algo evd with | NotInvertibleUsingOurAlgorithm t -> diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 6de8f5c8dc..16a4aff5bf 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -31,11 +31,11 @@ type conv_fun = type conv_fun_bool = env -> evar_map -> conv_pb -> constr -> constr -> bool -val evar_define : conv_fun -> ?choose:bool -> ?dir:bool -> env -> evar_map -> +val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map val refresh_universes : ?onlyalg:bool (* Only algebraic universes *) -> - bool (* direction: true for levels lower than the existing levels *) -> + bool option (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map -> diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 21395af027..c64cd35e53 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -480,14 +480,16 @@ let rec instantiate_universes env evdref scl is = function d :: instantiate_universes env evdref scl is (sign, exp) | (na,None,ty)::sign, Some u::exp -> let ctx,_ = Reduction.dest_arity env ty in + let u = Univ.Universe.make u in let s = (* Does the sort of parameter [u] appear in (or equal) the sort of inductive [is] ? *) - if univ_depends (Univ.Universe.make u) is then + if univ_depends u is then scl (* constrained sort: replace by scl *) else - (* unconstriained sort: replace by fresh universe *) + (* unconstrained sort: replace by fresh universe *) let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in + let evm = Evd.set_leq_sort evm s (Sorts.sort_of_univ u) in evdref := evm; s in (na,None,mkArity(ctx,s)):: instantiate_universes env evdref scl is (sign, exp) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 27abdbade8..6d7403031a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -595,7 +595,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = refreshed right away. *) let sigma = !evdref in let c = mkApp (f,Array.map (whd_evar sigma) args) in - let c = evd_comb1 (Evarsolve.refresh_universes true env) evdref c in + let c = evd_comb1 (Evarsolve.refresh_universes (Some true) env) evdref c in let t = Retyping.get_type_of env !evdref c in make_judge c (* use this for keeping evars: resj.uj_val *) t else resj diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 1c41a5bb3a..92bdd35ecf 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -290,7 +290,7 @@ let e_type_of ?(refresh=false) env evd c = let j = execute env evdref c in (* side-effect on evdref *) if refresh then - Evarsolve.refresh_universes ~onlyalg:true false env !evdref j.uj_type + Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type else !evdref, j.uj_type let solve_evars env evdref c = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 4ad8f833e6..219d03b9e7 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -442,7 +442,7 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst) tyM tyN = | None -> sigma | Some n -> if is_ground_term sigma m && is_ground_term sigma n then - let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta env sigma m n in + let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n in if b then sigma else error_cannot_unify env sigma (m,n) else sigma @@ -936,7 +936,7 @@ let w_coerce env evd mv c = w_coerce_to_type env evd c cty mvty let unify_to_type env sigma flags c status u = - let sigma, c = refresh_universes false env sigma c in + let sigma, c = refresh_universes (Some false) env sigma c in let t = get_type_of env sigma (nf_meta sigma c) in let t = nf_betaiota sigma (nf_meta sigma t) in unify_0 env sigma CUMUL flags t u diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index b2fea6fd10..589cb5bdaa 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -82,7 +82,7 @@ open Unification let dft = default_unify_flags -let res_pf clenv ?(with_evars=false) ?(flags=dft ()) = +let res_pf ?(with_evars=false) ?(flags=dft ()) clenv = Proofview.Goal.raw_enter begin fun gl -> let clenv gl = clenv_unique_resolver ~flags clenv gl in clenv_refine with_evars (Tacmach.New.of_old clenv (Proofview.Goal.assume gl)) diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 789a21c247..bede509e79 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -15,7 +15,7 @@ open Unification (** Tactics *) val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic val clenv_refine : evars_flag -> ?with_classes:bool -> clausenv -> unit Proofview.tactic -val res_pf : clausenv -> ?with_evars:evars_flag -> ?flags:unify_flags -> unit Proofview.tactic +val res_pf : ?with_evars:evars_flag -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv val clenv_value_cast_meta : clausenv -> constr diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 410335b47e..06afc2fa9a 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -269,7 +269,10 @@ let close_proof ?feedback_id ~now fpl = let poly = pi2 strength (* Polymorphic *) in let initial_goals = Proof.initial_goals proof in let fpl, univs = Future.split2 fpl in - let universes = Future.force univs in + let universes = + if poly || now then Future.force univs + else Proof.in_proof proof (fun x -> Evd.evar_universe_context x) + in let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None) (Evd.evar_universe_context_subst universes) in let make_body = diff --git a/stm/lemmas.ml b/stm/lemmas.ml index c400008113..5d2babaca9 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 85c3838dc7..b53c9fcf8f 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 a58100b5a0..fd306425c1 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/toplevel/ide_slave.mli b/stm/stmworkertop.ml index fb927cf33f..50afd97ab5 100644 --- a/toplevel/ide_slave.mli +++ b/stm/stmworkertop.ml @@ -6,12 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** [Ide_slave] : an implementation of [Ide_intf], i.e. mainly an interp - function and a rewind function. This specialized loop is triggered - when the -ideslave option is passed to Coqtop. Currently CoqIDE is - the only one using this mode, but we try here to be as generic as - possible, so this may change in the future... *) +let () = Coqtop.toploop_init := (fun args -> + Flags.make_silent true; + Stm.slave_init_stdout (); + args) -val init_stdout : unit -> unit +let () = Coqtop.toploop_run := Stm.slave_main_loop -val loop : unit -> unit diff --git a/stm/stmworkertop.mllib b/stm/stmworkertop.mllib new file mode 100644 index 0000000000..78b54b2ea9 --- /dev/null +++ b/stm/stmworkertop.mllib @@ -0,0 +1 @@ +Stmworkertop diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 98e7d3ff5f..0e9d3dcdc8 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -282,10 +282,18 @@ module SearchProblem = struct { depth = s.depth; tacres = res; last_tactic = pp; prev = ps; dblist = s.dblist; localdb = List.tl s.localdb } else - { depth = pred s.depth; tacres = res; - dblist = s.dblist; last_tactic = pp; prev = ps; - localdb = - List.addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb }) + let newlocal = + let hyps = pf_hyps g in + List.map (fun gl -> + let gls = {Evd.it = gl; sigma = lgls.Evd.sigma } in + let hyps' = pf_hyps gls in + if hyps' == hyps then List.hd s.localdb + else make_local_hint_db ~ts:full_transparent_state true [] gls) + (List.firstn ((nbgl'-nbgl) + 1) (sig_it lgls)) + in + { depth = pred s.depth; tacres = res; + dblist = s.dblist; last_tactic = pp; prev = ps; + localdb = newlocal @ List.tl s.localdb }) l in List.sort compare (assumption_tacs @ intro_tac @ rec_tacs) diff --git a/tactics/equality.ml b/tactics/equality.ml index 81f133ddc3..63bb846139 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -987,7 +987,7 @@ let find_sigma_data env s = build_sigma_type () let make_tuple env sigma (rterm,rty) lind = assert (dependent (mkRel lind) rty); let sigdata = find_sigma_data env (get_sort_of env sigma rty) in - let a = type_of env sigma (mkRel lind) in + let sigma, a = e_type_of ~refresh:true env sigma (mkRel lind) in let (na,_,_) = lookup_rel lind env in (* We move [lind] to [1] and lift other rels > [lind] by 1 *) let rty = lift (1-lind) (liftn lind (lind+1) rty) in @@ -1089,7 +1089,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let w_type = type_of env sigma w in if Evarconv.e_cumul env evdref w_type a then let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in - applist(exist_term,[w_type;p_i_minus_1;w;tuple_tail]) + applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) else error "Cannot solve a unification problem." | None -> anomaly (Pp.str "Not enough components to build the dependent tuple") diff --git a/tactics/inv.ml b/tactics/inv.ml index dc88795216..ee875ce27d 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -74,7 +74,7 @@ let make_inv_predicate env evd indf realargs id status concl = | NoDep -> (* We push the arity and leave concl unchanged *) let hyps_arity,_ = get_arity env indf in - (hyps_arity,concl) + (hyps_arity,concl) | Dep dflt_concl -> if not (occur_var env id concl) then errorlabstrm "make_inv_predicate" @@ -129,6 +129,7 @@ let make_inv_predicate env evd indf realargs id status concl = in let (newconcl, args) = build_concl [] [] 0 realargs in let predicate = it_mkLambda_or_LetIn_name env newconcl hyps in + let _ = Evarutil.evd_comb1 (Typing.e_type_of env) evd predicate in (* OK - this predicate should now be usable by res_elimination_then to do elimination on the conclusion. *) predicate, args diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index aa32e0e5c4..06d0a04cc2 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -53,7 +53,9 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l) let try_find_global_reference dir s = let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in - Nametab.global_of_path sp + try Nametab.global_of_path sp + with Not_found -> + anomaly (str ("Global reference " ^ s ^ " not found in generalized rewriting")) let find_reference dir s = let gr = lazy (try_find_global_reference dir s) in @@ -1527,7 +1529,6 @@ let cl_rewrite_clause_strat strat clause = tclTHEN (tactic_init_setoid ()) (fun gl -> let meta = Evarutil.new_meta() in - (* let gl = { gl with sigma = Typeclasses.mark_unresolvables gl.sigma } in *) try cl_rewrite_clause_tac strat (mkMeta meta) clause gl with RewriteFailure e -> tclFAIL 0 (str"setoid rewrite failed: " ++ e) gl @@ -1888,7 +1889,7 @@ let unification_rewrite flags l2r c1 c2 cl car rel but gl = and car = nf car and rel = nf rel in check_evar_map_of_evars_defs cl'.evd; let prf = nf (Clenv.clenv_value cl') and prfty = nf (Clenv.clenv_type cl') in - let sort = sort_of_rel env evd' (pf_concl gl) in + let sort = sort_of_rel env evd' but in let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty; evd = Evd.diff cl'.evd (project gl) } in @@ -1942,6 +1943,7 @@ let general_s_rewrite_clause x = match x with | None -> general_s_rewrite None | Some id -> general_s_rewrite (Some id) + let general_s_rewrite_clause x y z w ~new_goals = newtactic_init_setoid () <*> Proofview.V82.tactic (general_s_rewrite_clause x y z w ~new_goals) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3c0016830c..8dfd1b14bf 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1227,8 +1227,11 @@ let exact_check c = Proofview.Goal.raw_enter begin fun gl -> (** We do not need to normalize the goal because we just check convertibility *) let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in - let ct = Tacmach.New.pf_type_of gl c in - Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c) + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, ct = Typing.e_type_of env sigma c in + Proofview.V82.tclEVARS sigma <*> + Tacticals.New.tclTHEN (convert_leq ct concl) (new_exact_no_check c) end let exact_no_check = refine_no_check @@ -1884,31 +1887,36 @@ let letin_tac_gen with_eq abs ty = let env = Proofview.Goal.env gl in let (id,depdecls,lastlhyp,ccl,(tac,c)) = make_abstraction abs gl in let t = match ty with Some t -> t | _ -> typ_of env (Proofview.Goal.sigma gl) c in - let (sigma,newcl,eq_tac) = match with_eq with + let eq_tac gl = match with_eq with | Some (lr,(loc,ido)) -> let heq = match ido with | IntroAnonymous -> new_fresh_id [id] (add_prefix "Heq" id) gl | IntroFresh heq_base -> new_fresh_id [id] heq_base gl | IntroIdentifier id -> id | _ -> Errors.error "Expect an introduction pattern naming one hypothesis." in - let eqdata = build_coq_eq_data () in - let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in - let sigma, eq = Evd.fresh_global env (Proofview.Goal.sigma gl) eqdata.eq in - let sigma, refl = Evd.fresh_global env sigma eqdata.refl in - let eq = applist (eq,args) in - let refl = applist (refl, [t;mkVar id]) in - sigma, - mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)), - Tacticals.New.tclTHEN - (intro_gen loc (IntroMustBe heq) lastlhyp true false) - (Proofview.V82.tactic (thin_body [heq;id])) + let eqdata = build_coq_eq_data () in + let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in + let sigma, eq = Evd.fresh_global env (Proofview.Goal.sigma gl) eqdata.eq in + let sigma, refl = Evd.fresh_global env sigma eqdata.refl in + let eq = applist (eq,args) in + let refl = applist (refl, [t;mkVar id]) in + let term = mkNamedLetIn id c t (mkLetIn (Name heq, refl, eq, ccl)) in + let sigma, _ = Typing.e_type_of env sigma term in + sigma, term, + Tacticals.New.tclTHEN + (intro_gen loc (IntroMustBe heq) lastlhyp true false) + (Proofview.V82.tactic (thin_body [heq;id])) | None -> (Proofview.Goal.sigma gl, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in - Tacticals.New.tclTHENLIST - [ Proofview.V82.tclEVARS sigma; tac; Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast); - intro_gen dloc (IntroMustBe id) lastlhyp true false; - Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls); - eq_tac ] + Proofview.tclBIND tac (fun () -> + Proofview.Goal.enter (fun gl -> + let (sigma,newcl,eq_tac) = eq_tac gl in + Tacticals.New.tclTHENLIST + [ Proofview.V82.tclEVARS sigma; + Proofview.V82.tactic (convert_concl_no_check newcl DEFAULTcast); + intro_gen dloc (IntroMustBe id) lastlhyp true false; + Proofview.V82.tactic (tclMAP convert_hyp_no_check depdecls); + eq_tac ])) end let letin_tac with_eq name c ty occs = diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v index ab39633f87..35c69db2fe 100644 --- a/test-suite/bugs/closed/2378.v +++ b/test-suite/bugs/closed/2378.v @@ -503,6 +503,9 @@ Qed. Require Export Coq.Logic.FunctionalExtensionality. Print PLanguage. + +Unset Standard Proposition Elimination Names. + Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): Transformation (PLanguage l1) (PLanguage l2) := mkTransformation (PLanguage l1) (PLanguage l2) diff --git a/test-suite/bugs/closed/2966.v b/test-suite/bugs/closed/2966.v index e1c8d00474..debada8539 100644 --- a/test-suite/bugs/closed/2966.v +++ b/test-suite/bugs/closed/2966.v @@ -7,7 +7,7 @@ Set Asymmetric Patterns. Module MemSig. Definition t: Type := list Type. - Definition Nth (sig: t) (n: nat): Type := + Definition Nth (sig: t) (n: nat) := nth n sig unit. End MemSig. diff --git a/test-suite/bugs/closed/3036.v b/test-suite/bugs/closed/3036.v index c1ead05573..451bec9b20 100644 --- a/test-suite/bugs/closed/3036.v +++ b/test-suite/bugs/closed/3036.v @@ -165,4 +165,5 @@ Section Stack. | None => [False] end) * emp. Proof. - intros. apply himp_ex_conc_trivial. + intros. + try apply himp_ex_conc_trivial. diff --git a/test-suite/bugs/closed/3260.v b/test-suite/bugs/closed/3260.v new file mode 100644 index 0000000000..9f0231d91b --- /dev/null +++ b/test-suite/bugs/closed/3260.v @@ -0,0 +1,7 @@ +Require Import Setoid. +Goal forall m n, n = m -> n+n = m+m. +intros. +replace n with m at 2. +lazymatch goal with +|- n + m = m + m => idtac +end. diff --git a/test-suite/bugs/closed/3264.v b/test-suite/bugs/closed/3264.v new file mode 100644 index 0000000000..4eb218906f --- /dev/null +++ b/test-suite/bugs/closed/3264.v @@ -0,0 +1,45 @@ +Module File1. + Module Export DirA. + Module A. + Inductive paths {A : Type} (a : A) : A -> Type := + idpath : paths a a. + + Arguments idpath {A a} , [A] a. + + Notation "x = y :> A" := (@paths A x y) : type_scope. + Notation "x = y" := (x = y :>_) : type_scope. + End A. + End DirA. +End File1. + +Module File2. + Module Export DirA. + Module B. + Import File1. + Export A. + Lemma foo : forall x y : Type, x = y -> y = x. + Proof. + intros x y H. + rewrite <- H. + constructor. + Qed. + End B. + End DirA. +End File2. + +Module File3. + Module Export DirA. + Module C. + Import File1. + Export A. + Lemma bar : forall x y : Type, x = y -> y = x. + Proof. + intros x y H. + rewrite <- H. + constructor. + Defined. + Definition bar' + := Eval cbv beta iota zeta delta [bar internal_paths_rew] in bar. + End C. + End DirA. +End File3. diff --git a/test-suite/bugs/closed/3266.v b/test-suite/bugs/closed/3266.v new file mode 100644 index 0000000000..fd4cbff85c --- /dev/null +++ b/test-suite/bugs/closed/3266.v @@ -0,0 +1,3 @@ +Class A := a : nat. +Lemma p : True. +Proof. cut A; [tauto | exact 1]. Qed. diff --git a/test-suite/bugs/closed/3267.v b/test-suite/bugs/closed/3267.v new file mode 100644 index 0000000000..5ce1ddf0c4 --- /dev/null +++ b/test-suite/bugs/closed/3267.v @@ -0,0 +1,36 @@ +Module a. + Local Hint Extern 0 => progress subst. + Goal forall T (x y : T) (P Q : _ -> Prop), x = y -> (P x -> Q x) -> P y -> Q y. + Proof. + intros. + (* this should not fail *) + progress eauto. + Defined. +End a. + +Module b. + Local Hint Extern 0 => progress subst. + Goal forall T (x y : T) (P Q : _ -> Prop), y = x -> (P x -> Q x) -> P y -> Q y. + Proof. + intros. + eauto. + Defined. +End b. + +Module c. + Local Hint Extern 0 => progress subst; eauto. + Goal forall T (x y : T) (P Q : _ -> Prop), x = y -> (P x -> Q x) -> P y -> Q y. + Proof. + intros. + eauto. + Defined. +End c. + +Module d. + Local Hint Extern 0 => progress subst; repeat match goal with H : _ |- _ => revert H end. + Goal forall T (x y : T) (P Q : _ -> Prop), x = y -> (P x -> Q x) -> P y -> Q y. + Proof. + intros. + debug eauto. + Defined. +End d. diff --git a/test-suite/bugs/closed/328.v b/test-suite/bugs/closed/328.v new file mode 100644 index 0000000000..52cfbbc496 --- /dev/null +++ b/test-suite/bugs/closed/328.v @@ -0,0 +1,40 @@ +Module Type TITI. +Parameter B:Set. +Parameter x:B. +Inductive A:Set:= +a1:B->A. +Definition f2: A ->B +:= fun (a:A) => +match a with + (a1 b)=>b +end. +Definition f: A -> B:=fun (a:A) => x. +End TITI. + + +Module Type TIT. +Declare Module t:TITI. +End TIT. + +Module Seq(titi:TIT). +Module t:=titi.t. +Inductive toto:t.A->t.B->Set:= +t1:forall (a:t.A), (toto a (t.f a)) +| t2:forall (a:t.A), (toto a (t.f2 a)). +End Seq. + +Module koko(tit:TIT). +Module seq:=Seq tit. +Module t':=tit.t. + +Definition def:forall (a:t'.A), (seq.toto a (t'.f a)). +intro ; constructor 1. +Defined. + +Definition def2: forall (a:t'.A), (seq.toto a (t'.f2 a)). +intro; constructor 2. +(* Toplevel input, characters 0-13 + constructor 2. + ^^^^^^^^^^^^^ +Error: Impossible to unify (seq.toto ?3 (seq.t.f2 ?3)) with + (seq.toto a (t'.f2 a)).*) diff --git a/test-suite/bugs/closed/3286.v b/test-suite/bugs/closed/3286.v new file mode 100644 index 0000000000..b08b7ab3cc --- /dev/null +++ b/test-suite/bugs/closed/3286.v @@ -0,0 +1,41 @@ +Require Import FunctionalExtensionality. + +Ltac make_apply_under_binders_in lem H := + let tac := make_apply_under_binders_in in + match type of H with + | forall x : ?T, @?P x + => let ret := constr:(fun x' : T => + let Hx := H x' in + $(let ret' := tac lem Hx in + exact ret')$) in + match eval cbv zeta in ret with + | fun x => Some (@?P x) => let P' := (eval cbv zeta in P) in + constr:(Some P') + end + | _ => let ret := constr:($(match goal with + | _ => (let H' := fresh in + pose H as H'; + apply lem in H'; + exact (Some H')) + | _ => exact (@None nat) + end + )$) in + let ret' := (eval cbv beta zeta in ret) in + constr:(ret') + | _ => constr:(@None nat) + end. + +Ltac apply_under_binders_in lem H := + let H' := make_apply_under_binders_in lem H in + let H'0 := match H' with Some ?H'0 => constr:(H'0) end in + let H'' := fresh in + pose proof H'0 as H''; + clear H; + rename H'' into H. + +Goal forall A B C (f g : forall (x : A) (y : B x), C x y), (forall x y, f x y = g x y) -> True. +Proof. + intros A B C f g H. + let lem := constr:(@functional_extensionality_dep) in + apply_under_binders_in lem H. +(* Anomaly: Uncaught exception Not_found(_). Please report. *) diff --git a/test-suite/bugs/closed/329.v b/test-suite/bugs/closed/329.v new file mode 100644 index 0000000000..def6ed98dd --- /dev/null +++ b/test-suite/bugs/closed/329.v @@ -0,0 +1,100 @@ +Module Sylvain_Boulme. +Module Type Essai. +Parameter T: Type. +Parameter my_eq: T -> T -> Prop. +Parameter my_eq_refl: forall (x:T), (my_eq x x). +Parameter c: T. +End Essai. + +Module Type Essai2. +Declare Module M: Essai. +Parameter c2: M.T. +End Essai2. + +Module Type Essai3. +Declare Module M: Essai. +Parameter c3: M.T. +End Essai3. + +Module Type Lift. +Declare Module Core: Essai. +Declare Module M: Essai. +Parameter lift: Core.T -> M.T. +Parameter lift_prop:forall (x:Core.T), (Core.my_eq x Core.c)->(M.my_eq (lift x) M.c). +End Lift. + +Module I2 (X:Essai) <: Essai2. + Module Core := X. + Module M<:Essai. + Definition T:Type :=Prop. + Definition my_eq:=(@eq Prop). + Definition c:=True. + Lemma my_eq_refl: forall (x:T), (my_eq x x). + Proof. + unfold my_eq; auto. + Qed. + End M. + Definition c2:=False. + Definition lift:=fun (_:Core.T) => M.c. + Definition lift_prop: forall (x:Core.T), (Core.my_eq x Core.c)->(M.my_eq (lift x) M.c). + Proof. + unfold lift, M.my_eq; auto. + Qed. +End I2. + +Module I4(X:Essai3) (L: Lift with Module Core := X.M) <: Essai3 with Module +M:=L.M. + Module M:=L.M. + Definition c3:=(L.lift X.c3). +End I4. + +Module I5(X:Essai3). + Module Toto<: Lift with Module Core := X.M := I2(X.M). + Module E4<: Essai3 with Module M:=Toto.M := I4(X)(Toto). +(* +Le typage de E4 echoue avec le message + Error: Signature components for label my_eq_refl do not match + *) + + Module E3<: Essai3 := I4(X)(Toto). + + Definition zarb: forall (x:Toto.M.T), (Toto.M.my_eq x x) := E3.M.my_eq_refl. +End I5. +End Sylvain_Boulme. + + +Module Jacek. + + Module Type SIG. + End SIG. + Module N. + Definition A:=Set. + End N. + Module Type SIG2. + Declare Module M:SIG. + Parameter B:Type. + End SIG2. + Module F(X:SIG2 with Module M:=N) (Y:SIG2 with Definition B:=X.M.A). + End F. +End Jacek. + + +Module anoun. + Module Type TITI. + Parameter X: Set. + End TITI. + + Module Type Ex. + Declare Module t: TITI. + Parameter X : t.X -> t.X -> Set. + End Ex. + + Module unionEx(X1: Ex) (X2:Ex with Module t :=X1.t): Ex. + Module t:=X1.t. + Definition X :=fun (a b:t.X) => ((X1.X a b)+(X2.X a b))%type. + End unionEx. +End anoun. +(* Le warning qui s'affiche lors de la compilation est le suivant : + TODO:replace module after with! + Est ce qu'il y'a qq1 qui pourrait m'aider à comprendre le probleme?! + Je vous remercie d'avance *) diff --git a/test-suite/bugs/closed/3300.v b/test-suite/bugs/closed/3300.v new file mode 100644 index 0000000000..a28144b9ca --- /dev/null +++ b/test-suite/bugs/closed/3300.v @@ -0,0 +1,7 @@ +Set Primitive Projections. +Record Box (T : Type) : Prop := wrap {prop : T}. + +Definition down (x : Type) : Prop := Box x. +Definition up (x : Prop) : Type := x. + +Fail Definition back A : up (down A) -> A := @prop A. diff --git a/test-suite/bugs/closed/331.v b/test-suite/bugs/closed/331.v new file mode 100644 index 0000000000..9ef796faf7 --- /dev/null +++ b/test-suite/bugs/closed/331.v @@ -0,0 +1,20 @@ +Module Type TIT. + +Inductive X:Set:= + b:X. +End TIT. + + +Module Type TOTO. +Declare Module t:TIT. +Inductive titi:Set:= + a:t.X->titi. +End TOTO. + + +Module toto (ta:TOTO). +Module ti:=ta.t. + +Definition ex1:forall (c d:ti.X), (ta.a d)=(ta.a c) -> d=c. +intros. +injection H. diff --git a/test-suite/bugs/opened/3329.v b/test-suite/bugs/closed/3329.v index efe1abcd20..f7e368f8f4 100644 --- a/test-suite/bugs/opened/3329.v +++ b/test-suite/bugs/closed/3329.v @@ -70,7 +70,7 @@ Local Open Scope functor_scope. Context `{Funext}. Variable D : PreCategory. Set Printing Universes. -Fail Check hom_functor D o 1. +Check hom_functor D o 1. (* Toplevel input, characters 20-44: Error: Illegal application: The term "@set_cat" of type "(Funext -> PreCategory)%type" diff --git a/test-suite/bugs/closed/3332.v b/test-suite/bugs/closed/3332.v new file mode 100644 index 0000000000..d86470cdee --- /dev/null +++ b/test-suite/bugs/closed/3332.v @@ -0,0 +1,6 @@ +(* -*- coq-prog-args: ("-emacs" "-time") -*- *) +Definition foo : True. +Proof. +Abort. (* Toplevel input, characters 15-21: +Anomaly: Backtrack.backto to a state with no vcs_backup. Please report. *) +(* Anomaly: VernacAbort not handled by Stm. Please report. *) diff --git a/test-suite/bugs/closed/3350.v b/test-suite/bugs/closed/3350.v new file mode 100644 index 0000000000..bab197ed03 --- /dev/null +++ b/test-suite/bugs/closed/3350.v @@ -0,0 +1,115 @@ +Require Coq.Vectors.Fin. +Require Coq.Vectors.Vector. + +Local Generalizable All Variables. +Set Implicit Arguments. + +Arguments Fin.F1 : clear implicits. + +Lemma fin_0_absurd : notT (Fin.t 0). +Proof. hnf. apply Fin.case0. Qed. + +Fixpoint lower {n:nat} (p:Fin.t (S n)) {struct p} : + forall (i:Fin.t (S n)), option (Fin.t n) + := match p in Fin.t (S n1) + return Fin.t (S n1) -> option (Fin.t n1) + with + | @Fin.F1 n1 => + fun (i:Fin.t (S n1)) => + match i in Fin.t (S n2) return option (Fin.t n2) with + | @Fin.F1 n2 => None + | @Fin.FS n2 i2 => Some i2 + end + | @Fin.FS n1 p1 => + fun (i:Fin.t (S n1)) => + match i in Fin.t (S n2) return Fin.t n2 -> option (Fin.t n2) with + | @Fin.F1 n2 => + match n2 as n3 return Fin.t n3 -> option (Fin.t n3) with + | 0 => fun p2 => False_rect _ (fin_0_absurd p2) + | S n3 => fun p2 => Some (Fin.F1 n3) + end + | @Fin.FS n2 i2 => + match n2 as n3 return Fin.t n3 -> Fin.t n3 -> option (Fin.t n3) with + | 0 => fun i3 p3 => False_rect _ (fin_0_absurd p3) + | S n3 => fun (i3 p3:Fin.t (S n3)) => + option_map (@Fin.FS _) (lower p3 i3) + end i2 + end p1 + end. + +Lemma lower_ind (P: forall n (p i:Fin.t (S n)), option (Fin.t n) -> Prop) + (c11 : forall n, P n (Fin.F1 n) (Fin.F1 n) None) + (c1S : forall n (i:Fin.t n), P n (Fin.F1 n) (Fin.FS i) (Some i)) + (cS1 : forall n (p:Fin.t (S n)), + P (S n) (Fin.FS p) (Fin.F1 (S n)) (Some (Fin.F1 n))) + (cSSS : forall n (p i:Fin.t (S n)) (i':Fin.t n) + (Elow:lower p i = Some i'), + P n p i (Some i') -> + P (S n) (Fin.FS p) (Fin.FS i) (Some (Fin.FS i'))) + (cSSN : forall n (p i:Fin.t (S n)) + (Elow:lower p i = None), + P n p i None -> + P (S n) (Fin.FS p) (Fin.FS i) None) : + forall n (p i:Fin.t (S n)), P n p i (lower p i). +Proof. + fix 2. intros n p. + refine (match p as p1 in Fin.t (S n1) + return forall (i1:Fin.t (S n1)), P n1 p1 i1 (lower p1 i1) + with + | @Fin.F1 n1 => _ + | @Fin.FS n1 p1 => _ + end); clear n p. + { revert n1. refine (@Fin.caseS _ _ _); cbn; intros. + apply c11. apply c1S. } + { intros i1. revert p1. + pattern n1, i1; refine (@Fin.caseS _ _ _ _ _); + clear n1 i1; + (intros [|n] i; [refine (False_rect _ (fin_0_absurd i)) | cbn ]). + { apply cS1. } + { intros p. pose proof (lower_ind n p i) as H. + destruct (lower p i) eqn:E. + { apply cSSS; assumption. } + { cbn. apply cSSN; assumption. } } } +Qed. + +Section squeeze. + Context {A:Type} (x:A). + Notation vec := (Vector.t A). + + Fixpoint squeeze {n} (v:vec n) (i:Fin.t (S n)) {struct i} : vec (S n) := + match i in Fin.t (S _n) return vec _n -> vec (S _n) + with + | @Fin.F1 n' => fun v' => Vector.cons _ x _ v' + | @Fin.FS n' i' => + fun v' => + match n' as _n return vec _n -> Fin.t _n -> vec (S _n) + with + | 0 => fun u i' => False_rect _ (fin_0_absurd i') + | S m => + fun (u:vec (S m)) => + match u in Vector.t _ (S _m) + return Fin.t (S _m) -> vec (S (S _m)) + with + | Vector.nil _ => tt + | Vector.cons _ h _ u' => + fun j' => Vector.cons _ h _ (squeeze u' j') + end + end v' i' + end v. +End squeeze. + +Lemma squeeze_nth (A:Type) (x:A) (n:nat) (v:Vector.t A n) p i : + Vector.nth (squeeze x v p) i = match lower p i with + | Some j => Vector.nth v j + | None => x + end. +Proof. + (* alternatively: [functional induction (lower p i) using lower_ind] *) + revert v. pattern n, p, i, (lower p i). + refine (@lower_ind _ _ _ _ _ _ n p i); + intros; cbn; auto. + + (*** Fails here with "Conversion test raised an anomaly" ***) + revert v. + +Abort. diff --git a/test-suite/bugs/closed/3372.v b/test-suite/bugs/closed/3372.v new file mode 100644 index 0000000000..91e3df76dd --- /dev/null +++ b/test-suite/bugs/closed/3372.v @@ -0,0 +1,7 @@ +Set Universe Polymorphism. +Definition hProp : Type := sigT (fun _ : Type => True). +Goal Type. +Fail exact hProp@{Set}. (* test that it fails, but is not an anomaly *) +try (exact hProp@{Set}; fail 1). (* Toplevel input, characters 15-32: +Anomaly: Uncaught exception Invalid_argument("Array.iter2", _). +Please report. *) diff --git a/test-suite/bugs/closed/3373.v b/test-suite/bugs/closed/3373.v index 16b137091d..5ecf280153 100644 --- a/test-suite/bugs/closed/3373.v +++ b/test-suite/bugs/closed/3373.v @@ -5,15 +5,29 @@ from 369 lines to 351 lines, then from 350 lines to 340 lines, then from 348 lines to 320 lines, then from 328 lines to 302 lines, then from 332 lines to 21 lines *) Set Universe Polymorphism. -Axiom admit : forall {T}, T. -Definition UU := Set. -Definition UU' := Type. -Definition hSet:= sigT (fun X : UU' => admit) . -Definition pr1hSet:= @projT1 UU (fun X : UU' => admit) : hSet -> Type. -Coercion pr1hSet: hSet >-> Sortclass. -Axiom binop : UU -> Type. -Axiom setwithbinop : Type. -Definition pr1setwithbinop : setwithbinop -> hSet. -Goal True. -pose (( @projT1 _ ( fun X : hSet@{Set j k} => binop X ) ) : _ -> hSet). -Admitted.
\ No newline at end of file +Module short. + Record foo := { bar : Type }. + Coercion baz (x : foo@{Set}) : Set := bar x. + Goal True. + Proof. + Fail pose ({| bar := Set |} : Type). (* check that it fails *) + try pose ({| bar := Set |} : Type). (* Anomaly: apply_coercion_args: mismatch between arguments and coercion. +Please report. *) + Admitted. +End short. + +Module long. + Axiom admit : forall {T}, T. + Definition UU := Set. + Definition UU' := Type. + Definition hSet:= sigT (fun X : UU' => admit) . + Definition pr1hSet:= @projT1 UU (fun X : UU' => admit) : hSet -> Type. + Coercion pr1hSet: hSet >-> Sortclass. + Axiom binop : UU -> Type. + Axiom setwithbinop : Type. + Goal True. + Proof. + Fail pose (( @projT1 _ ( fun X : hSet@{i j k} => binop X ) ) : _ -> hSet). (* check that it fails *) + try pose (( @projT1 _ ( fun X : hSet@{i j k} => binop X ) ) : _ -> hSet). (* check that it's not an anomaly *) + Admitted. +End long. diff --git a/test-suite/bugs/closed/3382.v b/test-suite/bugs/closed/3382.v new file mode 100644 index 0000000000..1d8e916747 --- /dev/null +++ b/test-suite/bugs/closed/3382.v @@ -0,0 +1,63 @@ +(* File reduced by coq-bug-finder from 9039 lines to 7786 lines, then from 7245 lines to 476 lines, then from 417 lines to 249 lines, then from 171 lines to 127 lines, then from 139 lines to 114 lines, then from 93 lines to 77 lines *) + +Set Implicit Arguments. +Definition admit {T} : T. +Admitted. +Delimit Scope object_scope with object. +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope functor_scope with functor. +Reserved Infix "o" (at level 40, left associativity). +Record PreCategory := + { Object :> Type; + Morphism : Object -> Object -> Type; + Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' where "f 'o' g" := (Compose f g) }. +Bind Scope category_scope with PreCategory. +Infix "o" := (@Compose _ _ _ _) : morphism_scope. +Local Open Scope morphism_scope. +Record Functor (C D : PreCategory) := + { ObjectOf :> C -> D; + MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d); + FCompositionOf : forall s d d' (m1 : C.(Morphism) s d) (m2: C.(Morphism) d d'), + MorphismOf _ _ (m2 o m1) = (MorphismOf _ _ m2) o (MorphismOf _ _ m1) }. +Bind Scope functor_scope with Functor. +Arguments MorphismOf [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. +Definition ComposeFunctors C D E + (G : Functor D E) (F : Functor C D) : Functor C E + := Build_Functor C E (fun c => G (F c)) admit admit. +Infix "o" := ComposeFunctors : functor_scope. +Record NaturalTransformation C D (F G : Functor C D) := + { ComponentsOf :> forall c, D.(Morphism) (F c) (G c); + Commutes : forall s d (m : C.(Morphism) s d), + ComponentsOf d o F.(MorphismOf) m = G.(MorphismOf) m o ComponentsOf s }. +Definition NTComposeT C D (F F' F'' : Functor C D) + (T' : NaturalTransformation F' F'') + (T : NaturalTransformation F F') + (CO := fun c => T' c o T c) +: NaturalTransformation F F''. + exact (Build_NaturalTransformation F F'' + (fun c => T' c o T c) + (admit : forall s d (m : Morphism C s d), CO d o MorphismOf F m = MorphismOf F'' m o CO s)). +Defined. +Definition NTWhiskerR C D E (F F' : Functor D E) (T : NaturalTransformation F F') + (G : Functor C D) + := Build_NaturalTransformation (F o G) (F' o G) (fun c => T (G c)) admit. +Axiom NTWhiskerR_CompositionOf +: forall C D + (F G H : Functor C D) + (T : NaturalTransformation G H) + (T' : NaturalTransformation F G) B (I : Functor B C), + NTComposeT (NTWhiskerR T I) (NTWhiskerR T' I) = NTWhiskerR (NTComposeT T T') I. +Definition FunctorCategory C D : PreCategory + := @Build_PreCategory (Functor C D) + (NaturalTransformation (C := C) (D := D)) + admit. +Notation "[ C , D ]" := (FunctorCategory C D) : category_scope. +Class silly {T} := term : T. +Timeout 1 Fail Definition NTWhiskerR_Functorial (C D E : PreCategory) (G : [C, D]%category) +: [[D, E], [C, E]]%category + := Build_Functor + [C, D] [C, E] + (fun F => _ : silly) + (fun _ _ T => _ : silly) + (fun _ _ _ _ _ => NTWhiskerR_CompositionOf _ _ _). diff --git a/test-suite/bugs/closed/3386.v b/test-suite/bugs/closed/3386.v new file mode 100644 index 0000000000..0e236c2172 --- /dev/null +++ b/test-suite/bugs/closed/3386.v @@ -0,0 +1,16 @@ +Set Universe Polymorphism. +Set Printing Universes. +Record Cat := { Obj :> Type }. +Definition set_cat := {| Obj := Type |}. +Goal Type@{i} = Type@{j}. +Proof. + (* 1 subgoals +, subgoal 1 (ID 3) + + ============================ + Type@{Top.368} = Type@{Top.370} +(dependent evars:) *) + Fail change Type@{i} with (Obj set_cat@{i}). (* check that it fails *) + try change Type@{i} with (Obj set_cat@{i}). (* check that it's not an anomaly *) +(* Anomaly: Uncaught exception Invalid_argument("Array.iter2", _). +Please report. *) diff --git a/test-suite/bugs/closed/3387.v b/test-suite/bugs/closed/3387.v new file mode 100644 index 0000000000..feff8af2a5 --- /dev/null +++ b/test-suite/bugs/closed/3387.v @@ -0,0 +1,21 @@ +Set Universe Polymorphism. +Set Printing Universes. +Record Cat := { Obj :> Type }. +Definition set_cat := {| Obj := Type |}. +Goal Type@{i} = Type@{j}. +Proof. + (* 1 subgoals +, subgoal 1 (ID 3) + + ============================ + Type@{Top.368} = Type@{Top.370} +(dependent evars:) *) + let x := constr:(Type) in + let y := constr:(Obj set_cat) in + unify x y. (* success *) + let x := constr:(Type) in + let y := constr:(Obj set_cat) in + first [ unify x y | fail 2 "no unify" ]; + change x with y. (* Error: Not convertible. *) + reflexivity. +Defined.
\ No newline at end of file diff --git a/test-suite/bugs/closed/3390.v b/test-suite/bugs/closed/3390.v new file mode 100644 index 0000000000..eb3c4f4b9c --- /dev/null +++ b/test-suite/bugs/closed/3390.v @@ -0,0 +1,9 @@ +Tactic Notation "basicapply" open_constr(R) "using" tactic3(tac) "sideconditions" tactic0(tacfin) := idtac. +Tactic Notation "basicapply" open_constr(R) := basicapply R using (fun Hlem => idtac) sideconditions (autounfold with spred; idtac). +(* segfault in coqtop *) + + +Tactic Notation "basicapply" tactic0(tacfin) := idtac. + +Goal True. +basicapply subst. diff --git a/test-suite/bugs/closed/3392.v b/test-suite/bugs/closed/3392.v new file mode 100644 index 0000000000..43acb7bb48 --- /dev/null +++ b/test-suite/bugs/closed/3392.v @@ -0,0 +1,40 @@ +(* File reduced by coq-bug-finder from original input, then from 12105 lines to 142 lines, then from 83 lines to 57 lines *) +Generalizable All Variables. +Axiom admit : forall {T}, T. +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. +Arguments idpath {A a} , [A] a. +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing). +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end. +Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y): transport _ p (f x) = f y := admit. +Definition Sect {A B : Type} (s : A -> B) (r : B -> A) := forall x : A, r (s x) = x. +Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { + equiv_inv : B -> A ; + eisretr : Sect equiv_inv f; + eissect : Sect f equiv_inv; + eisadj : forall x : A, eisretr (f x) = ap f (eissect x) }. +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3). +Axiom path_forall : forall {A : Type} {P : A -> Type} (f g : forall x : A, P x), (forall x, f x = g x) -> f = g. +Axiom isequiv_adjointify : forall {A B} (f : A -> B) (g : B -> A) (isretr : Sect g f) (issect : Sect f g), IsEquiv f. +Definition functor_forall `{P : A -> Type} `{Q : B -> Type} (f0 : B -> A) (f1 : forall b:B, P (f0 b) -> Q b) +: (forall a:A, P a) -> (forall b:B, Q b) := (fun g b => f1 _ (g (f0 b))). +Goal forall `{P : A -> Type} `{Q : B -> Type} `{IsEquiv B A f} `{forall b, @IsEquiv (P (f b)) (Q b) (g b)}, + IsEquiv (functor_forall f g). +Proof. + intros. + refine (isequiv_adjointify (functor_forall f g) + (functor_forall (f^-1) + (fun (x:A) (y:Q (f^-1 x)) => @eisretr _ _ f _ x # (g (f^-1 x))^-1 y + )) _ _); + intros h. + - abstract ( + apply path_forall; intros b; unfold functor_forall; + rewrite eisadj; + admit + ). + - abstract ( + apply path_forall; intros a; unfold functor_forall; + rewrite eissect; + apply apD + ). +Defined. diff --git a/test-suite/bugs/closed/3393.v b/test-suite/bugs/closed/3393.v new file mode 100644 index 0000000000..ec25e68297 --- /dev/null +++ b/test-suite/bugs/closed/3393.v @@ -0,0 +1,152 @@ +(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* File reduced by coq-bug-finder from original input, then from 8760 lines to 7519 lines, then from 7050 lines to 909 lines, then from 846 lines to 578 lines, then from 497 lines to 392 lines, then from 365 lines to 322 lines, then from 252 lines to 205 lines, then from 215 lines to 204 lines, then from 210 lines to 182 lines, then from 175 lines to 157 lines *) +Set Universe Polymorphism. +Axiom admit : forall {T}, T. +Set Implicit Arguments. +Generalizable All Variables. +Reserved Notation "g 'o' f" (at level 40, left associativity). +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "a = b" := (@paths _ a b) : type_scope. +Arguments idpath {A a} , [A] a. +Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g) : forall x, f x = g x := fun x => match h with idpath => idpath end. +Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A }. +Delimit Scope equiv_scope with equiv. +Local Open Scope equiv_scope. +Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope. +Class Funext := { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }. +Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) : (forall x, f x = g x) -> f = g := (@apD10 A P f g)^-1. +Record PreCategory := + { object :> Type; + morphism : object -> object -> Type; + compose : forall s d d', morphism d d' -> morphism s d -> morphism s d' where "f 'o' g" := (compose f g); + associativity : forall x1 x2 x3 x4 (m1 : morphism x1 x2) (m2 : morphism x2 x3) (m3 : morphism x3 x4), (m3 o m2) o m1 = m3 o (m2 o m1) + }. +Bind Scope category_scope with PreCategory. +Bind Scope morphism_scope with morphism. +Infix "o" := (@compose _ _ _ _) : morphism_scope. +Delimit Scope functor_scope with functor. +Record Functor (C D : PreCategory) := + { object_of :> C -> D; + morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d) }. +Bind Scope functor_scope with Functor. +Notation "F '_1' m" := (@morphism_of _ _ F _ _ m) (at level 10, no associativity) : morphism_scope. +Class IsIsomorphism {C : PreCategory} {s d} (m : morphism C s d) := { morphism_inverse : morphism C d s }. +Local Notation "m ^-1" := (morphism_inverse (m := m)) : morphism_scope. +Class Isomorphic {C : PreCategory} s d := + { morphism_isomorphic :> morphism C s d; + isisomorphism_isomorphic :> IsIsomorphism morphism_isomorphic }. +Coercion morphism_isomorphic : Isomorphic >-> morphism. +Definition isisomorphism_inverse `(@IsIsomorphism C x y m) : IsIsomorphism m^-1 := {| morphism_inverse := m |}. + +Global Instance isisomorphism_compose `(@IsIsomorphism C y z m0) `(@IsIsomorphism C x y m1) : IsIsomorphism (m0 o m1). +Admitted. +Infix "<~=~>" := Isomorphic (at level 70, no associativity) : category_scope. +Definition composef C D E (G : Functor D E) (F : Functor C D) : Functor C E + := Build_Functor + C E + (fun c => G (F c)) + (fun _ _ m => @morphism_of _ _ G _ _ (@morphism_of _ _ F _ _ m)). +Infix "o" := composef : functor_scope. +Delimit Scope natural_transformation_scope with natural_transformation. + +Local Open Scope morphism_scope. +Record NaturalTransformation C D (F G : Functor C D) := + { components_of :> forall c, morphism D (F c) (G c); + commutes : forall s d (m : morphism C s d), components_of d o F _1 m = G _1 m o components_of s }. + +Definition composet C D (F F' F'' : Functor C D) (T' : NaturalTransformation F' F'') (T : NaturalTransformation F F') +: NaturalTransformation F F'' + := Build_NaturalTransformation F F'' (fun c => T' c o T c) admit. +Infix "o" := composet : natural_transformation_scope. +Section path_natural_transformation. + Context `{Funext}. + Variable C : PreCategory. + Variable D : PreCategory. + Variables F G : Functor C D. + Section path. + Variables T U : NaturalTransformation F G. + Lemma path'_natural_transformation + : components_of T = components_of U + -> T = U. + admit. + Defined. + Lemma path_natural_transformation + : (forall x, components_of T x = components_of U x) + -> T = U. + Proof. + intros. + apply path'_natural_transformation. + apply path_forall; assumption. + Qed. + End path. +End path_natural_transformation. +Ltac path_natural_transformation := + repeat match goal with + | _ => intro + | _ => apply path_natural_transformation; simpl + end. + +Local Open Scope natural_transformation_scope. +Definition associativityt `{fs : Funext} + C D F G H I + (V : @NaturalTransformation C D F G) + (U : @NaturalTransformation C D G H) + (T : @NaturalTransformation C D H I) +: (T o U) o V = T o (U o V). +Proof. + path_natural_transformation. + apply associativity. +Qed. +Definition functor_category `{Funext} (C D : PreCategory) : PreCategory + := @Build_PreCategory (Functor C D) (@NaturalTransformation C D) (@composet C D) (@associativityt _ C D). +Notation "C -> D" := (functor_category C D) : category_scope. +Definition NaturalIsomorphism `{Funext} (C D : PreCategory) F G := @Isomorphic (C -> D) F G. +Infix "<~=~>" := NaturalIsomorphism : natural_transformation_scope. +Global Instance isisomorphism_compose' `{Funext} + `(T' : @NaturalTransformation C D F' F'') + `(T : @NaturalTransformation C D F F') + `{@IsIsomorphism (C -> D) F' F'' T'} + `{@IsIsomorphism (C -> D) F F' T} +: @IsIsomorphism (C -> D) F F'' (T' o T)%natural_transformation + := @isisomorphism_compose (C -> D) _ _ T' _ _ T _. +Section lemmas. + Context `{Funext}. + Variable C : PreCategory. + Variable F : C -> PreCategory. + Context + {w y z} + {f : Functor (F w) (F z)} {f0 : Functor (F w) (F y)} + {f2 : Functor (F y) (F z)} + {f5 : Functor (F w) (F z)} + {n2 : f <~=~> (f2 o f0)%functor}. + Lemma p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper' XX + : @IsIsomorphism + (F w -> F z) f5 f + (n2 ^-1 o XX)%natural_transformation. + Proof. + eapply isisomorphism_compose'. + eapply isisomorphism_inverse. (* Toplevel input, characters 22-43: +Error: +In environment +H : Funext +C : PreCategory +F : C -> PreCategory +w : C +y : C +z : C +f : Functor (F w) (F z) +f0 : Functor (F w) (F y) +f2 : Functor (F y) (F z) +f5 : Functor (F w) (F z) +n2 : f <~=~> (f2 o f0)%functor +XX : NaturalTransformation f5 (f2 o f0) +Unable to unify + "{| + object := Functor (F w) (F z); + morphism := NaturalTransformation (D:=F z); + compose := composet (D:=F z); + associativity := associativityt (D:=F z) |}" with + "{| + object := Functor (F w) (F z); + morphism := NaturalTransformation (D:=F z); + compose := composet (D:=F z); + associativity := associativityt (D:=F z) |}". *) diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v index cae0fa9341..91cd099103 100644 --- a/test-suite/bugs/opened/1596.v +++ b/test-suite/bugs/opened/1596.v @@ -2,6 +2,8 @@ Require Import Relations. Require Import FSets. Require Import Arith. +Require Import Omega. +Unset Standard Proposition Elimination Names. Lemma Bool_elim_bool : forall (b:bool),b=true \/ b=false. destruct b;try tauto. @@ -253,7 +255,7 @@ n). induction m;simpl;intro. elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros. apply SynInc;apply H.mem_2;trivial. - + Fail rewrite H in H0. (* !! impossible here !! *) Abort. (* discriminate H0. diff --git a/test-suite/bugs/opened/3263.v b/test-suite/bugs/opened/3263.v new file mode 100644 index 0000000000..6de13f74e3 --- /dev/null +++ b/test-suite/bugs/opened/3263.v @@ -0,0 +1,231 @@ +(* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines, 2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *) +Generalizable All Variables. +Set Implicit Arguments. + +Arguments fst {_ _} _. +Arguments snd {_ _} _. + +Axiom cheat : forall {T}, T. + +Reserved Notation "g 'o' f" (at level 40, left associativity). + +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. +Arguments idpath {A a} , [A] a. +Notation "x = y" := (paths x y) : type_scope. + +Definition symmetry {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. + +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope object_scope with object. +Record PreCategory (object : Type) := + Build_PreCategory' { + object :> Type := object; + morphism : object -> object -> Type; + identity : forall x, morphism x x; + compose : forall s d d', + morphism d d' + -> morphism s d + -> morphism s d' + where "f 'o' g" := (compose f g); + associativity : forall x1 x2 x3 x4 + (m1 : morphism x1 x2) + (m2 : morphism x2 x3) + (m3 : morphism x3 x4), + (m3 o m2) o m1 = m3 o (m2 o m1); + associativity_sym : forall x1 x2 x3 x4 + (m1 : morphism x1 x2) + (m2 : morphism x2 x3) + (m3 : morphism x3 x4), + m3 o (m2 o m1) = (m3 o m2) o m1; + left_identity : forall a b (f : morphism a b), identity b o f = f; + right_identity : forall a b (f : morphism a b), f o identity a = f; + identity_identity : forall x, identity x o identity x = identity x + }. +Bind Scope category_scope with PreCategory. +Arguments PreCategory {_}. +Arguments identity {_} [!C%category] x%object : rename. + +Arguments compose {_} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename. + +Infix "o" := compose : morphism_scope. + +Delimit Scope functor_scope with functor. +Local Open Scope morphism_scope. +Record Functor `(C : @PreCategory objC, D : @PreCategory objD) := + { + object_of :> C -> D; + morphism_of : forall s d, morphism C s d + -> morphism D (object_of s) (object_of d); + composition_of : forall s d d' + (m1 : morphism C s d) (m2: morphism C d d'), + morphism_of _ _ (m2 o m1) + = (morphism_of _ _ m2) o (morphism_of _ _ m1); + identity_of : forall x, morphism_of _ _ (identity x) + = identity (object_of x) + }. +Bind Scope functor_scope with Functor. + +Arguments morphism_of {_} [C%category] {_} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. + +Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope. + +Class IsIsomorphism `{C : @PreCategory objC} {s d} (m : morphism C s d) := + { + morphism_inverse : morphism C d s; + left_inverse : morphism_inverse o m = identity _; + right_inverse : m o morphism_inverse = identity _ + }. + +Definition opposite `(C : @PreCategory objC) : PreCategory + := @Build_PreCategory' + C + (fun s d => morphism C d s) + (identity (C := C)) + (fun _ _ _ m1 m2 => m2 o m1) + (fun _ _ _ _ _ _ _ => @associativity_sym _ _ _ _ _ _ _ _ _) + (fun _ _ _ _ _ _ _ => @associativity _ _ _ _ _ _ _ _ _) + (fun _ _ => @right_identity _ _ _ _) + (fun _ _ => @left_identity _ _ _ _) + (@identity_identity _ C). + +Notation "C ^op" := (opposite C) (at level 3) : category_scope. + +Definition prod `(C : @PreCategory objC, D : @PreCategory objD) : @PreCategory (objC * objD). + refine (@Build_PreCategory' + (C * D)%type + (fun s d => (morphism C (fst s) (fst d) + * morphism D (snd s) (snd d))%type) + (fun x => (identity (fst x), identity (snd x))) + (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1)) + _ + _ + _ + _ + _); admit. +Defined. +Infix "*" := prod : category_scope. + +Definition compose_functor `(C : @PreCategory objC, D : @PreCategory objD, E : @PreCategory objE) (G : Functor D E) (F : Functor C D) : Functor C E + := Build_Functor + C E + (fun c => G (F c)) + (fun _ _ m => morphism_of G (morphism_of F m)) + cheat + cheat. + +Infix "o" := compose_functor : functor_scope. + +Record NaturalTransformation `(C : @PreCategory objC, D : @PreCategory objD) (F G : Functor C D) := + Build_NaturalTransformation' { + components_of :> forall c, morphism D (F c) (G c); + commutes : forall s d (m : morphism C s d), + components_of d o F _1 m = G _1 m o components_of s; + + commutes_sym : forall s d (m : C.(morphism) s d), + G _1 m o components_of s = components_of d o F _1 m + }. +Definition functor_category `(C : @PreCategory objC, D : @PreCategory objD) : PreCategory + := @Build_PreCategory' (Functor C D) + (@NaturalTransformation _ C _ D) + cheat + cheat + cheat + cheat + cheat + cheat + cheat. + +Definition opposite_functor `(F : @Functor objC C objD D) : Functor C^op D^op + := Build_Functor (C^op) (D^op) + (object_of F) + (fun s d => morphism_of F (s := d) (d := s)) + (fun d' d s m1 m2 => composition_of F s d d' m2 m1) + (identity_of F). + +Definition opposite_invL `(F : @Functor objC C^op objD D) : Functor C D^op + := Build_Functor C (D^op) + (object_of F) + (fun s d => morphism_of F (s := d) (d := s)) + (fun d' d s m1 m2 => composition_of F s d d' m2 m1) + (identity_of F). +Notation "F ^op" := (opposite_functor F) : functor_scope. + +Notation "F ^op'L" := (opposite_invL F) (at level 3) : functor_scope. +Definition fst `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) C + := Build_Functor (C * D) C + (@fst _ _) + (fun _ _ => @fst _ _) + (fun _ _ _ _ _ => idpath) + (fun _ => idpath). + +Definition snd `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) D + := Build_Functor (C * D) D + (@snd _ _) + (fun _ _ => @snd _ _) + (fun _ _ _ _ _ => idpath) + (fun _ => idpath). +Definition prod_functor `(F : @Functor objC C objD D, F' : @Functor objC C objD' D') +: Functor C (D * D') + := Build_Functor + C (D * D') + (fun c => (F c, F' c)) + (fun s d m => (F _1 m, F' _1 m))%morphism + cheat + cheat. +Definition pair `(F : @Functor objC C objD D, F' : @Functor objC' C' objD' D') : Functor (C * C') (D * D') + := (prod_functor (F o fst) (F' o snd))%functor. +Notation cat_of obj := + (@Build_PreCategory' obj + (fun x y => forall _ : x, y) + (fun _ x => x) + (fun _ _ _ f g x => f (g x))%core + (fun _ _ _ _ _ _ _ => idpath) + (fun _ _ _ _ _ _ _ => idpath) + (fun _ _ _ => idpath) + (fun _ _ _ => idpath) + (fun _ => idpath)). + +Definition hom_functor `(C : @PreCategory objC) : Functor (C^op * C) (cat_of Type) + := Build_Functor _ _ cheat cheat cheat cheat. + +Definition induced_hom_natural_transformation `(F : @Functor objC C objD D) +: NaturalTransformation (hom_functor C) (hom_functor D o pair F^op F) + := Build_NaturalTransformation' _ _ cheat cheat cheat. + +Class IsFullyFaithful `(F : @Functor objC C objD D) + := is_fully_faithful + : forall x y : C, + IsIsomorphism (induced_hom_natural_transformation F (x, y)). + +Definition coyoneda `(A : @PreCategory objA) : Functor A^op (@functor_category _ A _ (cat_of Type)) + := cheat. + +Definition yoneda `(A : @PreCategory objA) : Functor A (@functor_category _ A^op _ (cat_of Type)) + := (((coyoneda A^op)^op'L)^op'L)%functor. +Definition coyoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@coyoneda _ A). +Admitted. + +Definition yoneda_embedding_fast `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). +Proof. + intros a b. + pose proof (coyoneda_embedding A^op a b) as CYE. + unfold yoneda. + Time let t := (type of CYE) in + let t' := (eval simpl in t) in pose proof ((fun (x : t) => (x : t')) CYE) as CYE'. (* Finished transaction in 0. secs (0.216013u,0.004s) *) + Fail Timeout 1 let t := match goal with |- ?G => constr:(G) end in + let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). + Time let t := match goal with |- ?G => constr:(G) end in + let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). (* Finished transaction in 0. secs (0.248016u,0.s) *) +Fail Timeout 2 Defined. +Time Defined. (* Finished transaction in 1. secs (0.432027u,0.s) *) + +Definition yoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). +Proof. + intros a b. + pose proof (coyoneda_embedding A^op a b) as CYE. + unfold yoneda; simpl in *. + Fail Timeout 1 exact CYE. + Time exact CYE. (* Finished transaction in 0. secs (0.012001u,0.s) *) +Fail Timeout 60 Defined. (* Timeout! *) diff --git a/test-suite/bugs/opened/3277.v b/test-suite/bugs/opened/3277.v new file mode 100644 index 0000000000..19ed787d1e --- /dev/null +++ b/test-suite/bugs/opened/3277.v @@ -0,0 +1,7 @@ +Tactic Notation "evarr" open_constr(x) := let y := constr:(x) in exact y. + +Goal True. + evarr _. +Admitted. +Goal True. + Fail exact $(evarr _)$. (* Error: Cannot infer this placeholder. *) diff --git a/test-suite/bugs/opened/3278.v b/test-suite/bugs/opened/3278.v new file mode 100644 index 0000000000..2c6d391a0c --- /dev/null +++ b/test-suite/bugs/opened/3278.v @@ -0,0 +1,25 @@ +Module a. + Fail Check let x' := _ in + $(exact x')$. + + Notation foo x := (let x' := x in $(exact x')$). + + Fail Check foo _. (* Error: +Cannot infer an internal placeholder of type "Type" in environment: + +x' := ?42 : ?41 +. *) +End a. + +Module b. + Notation foo x := (let x' := x in let y := ($(exact I)$ : True) in I). + Notation bar x := (let x' := x in let y := (I : True) in I). + + Check let x' := _ in $(exact I)$. (* let x' := ?5 in I *) + Check bar _. (* let x' := ?9 in let y := I in I *) + Fail Check foo _. (* Error: +Cannot infer an internal placeholder of type "Type" in environment: + +x' := ?42 : ?41 +. *) +End b. diff --git a/test-suite/bugs/opened/3301.v b/test-suite/bugs/opened/3301.v deleted file mode 100644 index 955cfc3aa0..0000000000 --- a/test-suite/bugs/opened/3301.v +++ /dev/null @@ -1,120 +0,0 @@ -Section Hurkens. - -Definition Type2 := Type. -Definition Type1 := Type : Type2. - -(** Assumption of a retract from Type into Prop *) - -Variable down : Type1 -> Prop. -Variable up : Prop -> Type1. - -Hypothesis back : forall A, up (down A) -> A. - -Hypothesis forth : forall A, A -> up (down A). - -Hypothesis backforth : forall (A:Type) (P:A->Type) (a:A), - P (back A (forth A a)) -> P a. - -Hypothesis backforth_r : forall (A:Type) (P:A->Type) (a:A), - P a -> P (back A (forth A a)). - -(** Proof *) - -Definition V : Type1 := forall A:Prop, ((up A -> Prop) -> up A -> Prop) -> up A -> Prop. -Definition U : Type1 := V -> Prop. - -Definition sb (z:V) : V := fun A r a => r (z A r) a. -Definition le (i:U -> Prop) (x:U) : Prop := x (fun A r a => i (fun v => sb v A r a)). -Definition le' (i:up (down U) -> Prop) (x:up (down U)) : Prop := le (fun a:U => i (forth _ a)) (back _ x). -Definition induct (i:U -> Prop) : Type1 := forall x:U, up (le i x) -> up (i x). -Definition WF : U := fun z => down (induct (fun a => z (down U) le' (forth _ a))). -Definition I (x:U) : Prop := - (forall i:U -> Prop, up (le i x) -> up (i (fun v => sb v (down U) le' (forth _ x)))) -> False. - -Lemma Omega : forall i:U -> Prop, induct i -> up (i WF). -Proof. -intros i y. -apply y. -unfold le, WF, induct. -apply forth. -intros x H0. -apply y. -unfold sb, le', le. -compute. -apply backforth_r. -exact H0. -Qed. - -Lemma lemma1 : induct (fun u => down (I u)). -Proof. -unfold induct. -intros x p. -apply forth. -intro q. -generalize (q (fun u => down (I u)) p). -intro r. -apply back in r. -apply r. -intros i j. -unfold le, sb, le', le in j |-. -apply backforth in j. -specialize q with (i := fun y => i (fun v:V => sb v (down U) le' (forth _ y))). -apply q. -exact j. -Qed. - -Lemma lemma2 : (forall i:U -> Prop, induct i -> up (i WF)) -> False. -Proof. -intro x. -generalize (x (fun u => down (I u)) lemma1). -intro r; apply back in r. -apply r. -intros i H0. -apply (x (fun y => i (fun v => sb v (down U) le' (forth _ y)))). -unfold le, WF in H0. -apply back in H0. -exact H0. -Qed. - -Theorem paradox : False. -Proof. -exact (lemma2 Omega). -Qed. - -End Hurkens. - -Definition informative (x : bool) := - match x with - | true => Type - | false => Prop - end. - -Definition depsort (T : Type) (x : bool) : informative x := - match x with - | true => T - | false => True - end. - -(* The projection prop should not be definable *) -Set Primitive Projections. -Record Box (T : Type) : Prop := wrap {prop : T}. - -Definition down (x : Type) : Prop := Box x. -Definition up (x : Prop) : Type := x. - -Definition back A : up (down A) -> A := @prop A. - -Definition forth A : A -> up (down A) := wrap A. - -Definition backforth (A:Type) (P:A->Type) (a:A) : - P (back A (forth A a)) -> P a := fun H => H. - -Definition backforth_r (A:Type) (P:A->Type) (a:A) : - P a -> P (back A (forth A a)) := fun H => H. - -Theorem pandora : False. -apply (paradox down up back forth backforth backforth_r). -Qed. - -Print Assumptions pandora. -(* Closed under the global context *) diff --git a/test-suite/bugs/opened/3304.v b/test-suite/bugs/opened/3304.v new file mode 100644 index 0000000000..529cc737df --- /dev/null +++ b/test-suite/bugs/opened/3304.v @@ -0,0 +1,3 @@ +Fail Notation "( x , y , .. , z )" := $(let r := constr:(prod .. (prod x y) .. z) in r)$. +(* The command has indeed failed with message: +=> Error: Special token .. is for use in the Notation command. *) diff --git a/test-suite/bugs/opened/3309.v b/test-suite/bugs/opened/3309.v index 90f2a29cb7..fcebdec728 100644 --- a/test-suite/bugs/opened/3309.v +++ b/test-suite/bugs/opened/3309.v @@ -11,8 +11,8 @@ Unset Automatic Introduction. Definition UU := Set. -Definition dirprod ( X Y : UU ) := sigT ( fun x : X => Y ) . -Definition dirprodpair { X Y : UU } := existT ( fun x : X => Y ) . +Definition dirprod ( X Y : UU ) := sigT' ( fun x : X => Y ) . +Definition dirprodpair { X Y : UU } := existT' ( fun x : X => Y ) . Definition ddualand { X Y P : UU } (xp : ( X -> P ) -> P ) ( yp : ( Y -> P ) -> P ) : ( dirprod X Y -> P ) -> P. Proof. @@ -30,12 +30,12 @@ Definition invweq { X Y : UU } ( w : weq X Y ) : weq Y X . admit. Defined. -Definition hProp := sigT (fun X : Type => admit). +Definition hProp := sigT' (fun X : Type => admit). -Definition hProppair ( X : UU ) ( is : admit ) : hProp@{Set i}. -intros; exact (existT (fun X : UU => admit ) X is ). +Definition hProppair ( X : UU ) ( is : admit ) : hProp@{i j Set k}. +intros; exact (existT' (fun X : UU => admit ) X is ). Defined. -Definition hProptoType := @projT1 _ _ : hProp -> Type . +Definition hProptoType := @projT1' _ _ : hProp -> Type . Coercion hProptoType: hProp >-> Sortclass. Definition ishinh_UU ( X : UU ) : UU := forall P: Set, ( ( X -> P ) -> P ). @@ -55,18 +55,18 @@ intros; exact ( fun P:_ => ddualand (inx1 P) (iny1 P)) . Defined. Definition UU' := Type. -Definition hSet:= sigT (fun X : UU' => admit) . -Definition hSetpair := existT (fun X : UU' => admit). -Definition pr1hSet:= @projT1 UU (fun X : UU' => admit) : hSet -> Type. +Definition hSet:= sigT' (fun X : UU' => admit) . +Definition hSetpair := existT' (fun X : UU' => admit). +Definition pr1hSet:= @projT1' UU (fun X : UU' => admit) : hSet -> Type. Coercion pr1hSet: hSet >-> Sortclass. -Definition hPropset : hSet := existT _ hProp admit . +Definition hPropset : hSet := existT' _ hProp admit . Definition hsubtypes ( X : UU ) : Type. intros; exact (X -> hProp ). Defined. Definition carrier { X : UU } ( A : hsubtypes X ) : Type. -intros; exact (sigT A). +intros; exact (sigT' A). Defined. Coercion carrier : hsubtypes >-> Sortclass. @@ -96,9 +96,9 @@ admit. Defined. Definition eqrel ( X : UU ) : Type. -intros; exact ( sigT ( fun R : hrel X => iseqrel R ) ). +intros; exact ( sigT' ( fun R : hrel X => iseqrel R ) ). Defined. -Definition pr1eqrel ( X : UU ) : eqrel X -> ( X -> ( X -> hProp ) ) := @projT1 _ _ . +Definition pr1eqrel ( X : UU ) : eqrel X -> ( X -> ( X -> hProp ) ) := @projT1' _ _ . Coercion pr1eqrel : eqrel >-> Funclass . Definition hreldirprod { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) : hrel ( dirprod X Y ) . @@ -116,7 +116,7 @@ intros. hnf. apply dirprodpair. exact ax0. apply dirprodpair. exact ax1. exact a Defined. Definition eqax0 { X : UU } { R : hrel X } { A : hsubtypes X } : iseqclass R A -> ishinh ( carrier A ) . -intros X R A; exact ( fun is : iseqclass R A => projT1 is ). +intros X R A; exact ( fun is : iseqclass R A => projT1' _ is ). Defined. Lemma iseqclassdirprod { X Y : UU } { R : hrel X } { Q : hrel Y } { A : hsubtypes X } { B : hsubtypes Y } ( isa : iseqclass R A ) ( isb : iseqclass Q B ) : iseqclass ( hreldirprod R Q ) ( subtypesdirprod A B ) . @@ -130,10 +130,10 @@ Proof . Defined . Definition image { X Y : UU } ( f : X -> Y ) : Type. -intros; exact ( sigT ( fun y : Y => admit ) ). +intros; exact ( sigT' ( fun y : Y => admit ) ). Defined. Definition pr1image { X Y : UU } ( f : X -> Y ) : image f -> Y. -intros X Y f; exact ( @projT1 _ ( fun y : Y => admit ) ). +intros X Y f; exact ( @projT1' _ ( fun y : Y => admit ) ). Defined. Definition prtoimage { X Y : UU } (f : X -> Y) : X -> image f. @@ -141,14 +141,14 @@ Definition prtoimage { X Y : UU } (f : X -> Y) : X -> image f. Defined. Definition setquot { X : UU } ( R : hrel X ) : Type. -intros; exact ( sigT ( fun A : _ => iseqclass R A ) ). +intros; exact ( sigT' ( fun A : _ => iseqclass R A ) ). Defined. Definition setquotpair { X : UU } ( R : hrel X ) ( A : hsubtypes X ) ( is : iseqclass R A ) : setquot R. -intros; exact (existT _ A is ). +intros; exact (existT' _ A is ). Defined. Definition pr1setquot { X : UU } ( R : hrel X ) : setquot R -> ( hsubtypes X ). intros X R. -exact ( @projT1 _ ( fun A : _ => iseqclass R A ) ). +exact ( @projT1' _ ( fun A : _ => iseqclass R A ) ). Defined. Coercion pr1setquot : setquot >-> hsubtypes . @@ -157,7 +157,7 @@ intros; exact ( hSetpair (setquot R) admit) . Defined. Definition dirprodtosetquot { X Y : UU } ( RX : hrel X ) ( RY : hrel Y ) (cd : dirprod ( setquot RX ) ( setquot RY ) ) : setquot ( hreldirprod RX RY ). -intros; exact ( setquotpair _ _ ( iseqclassdirprod ( projT2 ( projT1 cd ) ) ( projT2 ( projT2 cd ) ) ) ). +intros; exact ( setquotpair _ _ ( iseqclassdirprod ( projT2' _ ( projT1' _ cd ) ) ( projT2' _ ( projT2' _ cd ) ) ) ). Defined. Definition iscomprelfun2 { X Y : UU } ( R : hrel X ) ( f : X -> X -> Y ) := forall x x' x0 x0' : X , R x x' -> R x0 x0' -> paths ( f x x0 ) ( f x' x0' ) . @@ -167,16 +167,16 @@ intros; exact ( X -> X -> X ). Defined. Definition setwithbinop : Type. -exact (sigT ( fun X : hSet => binop X ) ). +exact (sigT' ( fun X : hSet => binop X ) ). Defined. -Definition pr1setwithbinop : setwithbinop -> hSet@{Set j}. +Definition pr1setwithbinop : setwithbinop -> hSet@{j k Set l}. unfold setwithbinop. -exact ( @projT1 _ ( fun X : hSet@{Set j} => binop@{Set} X ) ). +exact ( @projT1' _ ( fun X : hSet@{j k Set l} => binop@{Set} X ) ). Defined. Coercion pr1setwithbinop : setwithbinop >-> hSet . Definition op { X : setwithbinop } : binop X. -intros; exact ( projT2 X ). +intros; exact ( projT2' _ X ). Defined. Definition subsetswithbinop { X : setwithbinop } : Type. @@ -190,11 +190,11 @@ Defined. Coercion carrierofasubsetwithbinop : subsetswithbinop >-> setwithbinop . Definition binopeqrel { X : setwithbinop } : Type. -intros; exact (sigT ( fun R : eqrel X => admit ) ). +intros; exact (sigT' ( fun R : eqrel X => admit ) ). Defined. -Definition binopeqrelpair { X : setwithbinop } := existT ( fun R : eqrel X => admit ). +Definition binopeqrelpair { X : setwithbinop } := existT' ( fun R : eqrel X => admit ). Definition pr1binopeqrel ( X : setwithbinop ) : @binopeqrel X -> eqrel X. -intros X; exact ( @projT1 _ ( fun R : eqrel X => admit ) ) . +intros X; exact ( @projT1' _ ( fun R : eqrel X => admit ) ) . Defined. Coercion pr1binopeqrel : binopeqrel >-> eqrel . @@ -203,10 +203,10 @@ admit. Defined. Definition monoid : Type. -exact ( sigT ( fun X : setwithbinop => admit ) ). +exact ( sigT' ( fun X : setwithbinop => admit ) ). Defined. -Definition monoidpair := existT ( fun X : setwithbinop => admit ) . -Definition pr1monoid : monoid -> setwithbinop := @projT1 _ _ . +Definition monoidpair := existT' ( fun X : setwithbinop => admit ) . +Definition pr1monoid : monoid -> setwithbinop := @projT1' _ _ . Coercion pr1monoid : monoid >-> setwithbinop . Notation "x + y" := ( op x y ) : addmonoid_scope . @@ -221,11 +221,11 @@ Defined. Coercion submonoidstosubsetswithbinop : submonoids >-> subsetswithbinop . Definition abmonoid : Type. -exact (sigT ( fun X : setwithbinop => admit ) ). +exact (sigT' ( fun X : setwithbinop => admit ) ). Defined. Definition abmonoidtomonoid : abmonoid -> monoid. -exact (fun X : _ => monoidpair ( projT1 X ) admit ). +exact (fun X : _ => monoidpair ( projT1' _ X ) admit ). Defined. Coercion abmonoidtomonoid : abmonoid >-> monoid . @@ -261,9 +261,9 @@ Defined. Theorem setquotuniv { X : UU } ( R : hrel X ) ( Y : hSet ) ( f : X -> Y ) ( c : setquot R ) : Y . Proof. intros. - apply ( pr1image ( fun x : c => f ( projT1 x ) ) ) . - apply ( @hinhuniv ( projT1 c ) ( hProppair _ admit ) ( prtoimage ( fun x : c => f ( projT1 x ) ) ) ) . - pose ( eqax0 ( projT2 c ) ) as h. + apply ( pr1image ( fun x : c => f ( projT1' _ x ) ) ) . + apply ( @hinhuniv ( projT1' _ c ) ( hProppair _ admit ) ( prtoimage ( fun x : c => f ( projT1' _ x ) ) ) ) . + pose ( eqax0 ( projT2' _ c ) ) as h. simpl in *. Set Printing Universes. exact h. @@ -315,4 +315,12 @@ Definition abmonoidfracrel ( X : abmonoid ) ( A : @submonoids X ) : hrel (@setq intros; exact (@quotrel _ _). Defined. -Fail Timeout 3 Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit. +Fail Timeout 1 Axiom ispartlbinopabmonoidfracrel : forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ) , @abmonoidfracrel X A ( ( admit + z ) )admit. + +Definition ispartlbinopabmonoidfracrel_type : Type := + forall ( X : abmonoid ) ( A : @subabmonoids X ) { L : hrel X } ( z : abmonoidfrac X A ), + @abmonoidfracrel X A ( ( admit + z ) )admit. + +Axiom ispartlbinopabmonoidfracrel : $(let t:= eval unfold ispartlbinopabmonoidfracrel_type in + ispartlbinopabmonoidfracrel_type in exact t)$. + diff --git a/test-suite/bugs/opened/3377.v b/test-suite/bugs/opened/3377.v new file mode 100644 index 0000000000..9ad3779d16 --- /dev/null +++ b/test-suite/bugs/opened/3377.v @@ -0,0 +1,8 @@ +Set Primitive Projections. +Record prod A B := pair { fst : A; snd : B}. + +Goal fst (@pair Type Type Type Type). +Set Printing All. +Fail match goal with |- ?f _ => idtac end. +(* Toplevel input, characters 7-44: +Error: No matching clauses for match. *) diff --git a/test-suite/bugs/opened/3383.v b/test-suite/bugs/opened/3383.v new file mode 100644 index 0000000000..9a14641a57 --- /dev/null +++ b/test-suite/bugs/opened/3383.v @@ -0,0 +1,7 @@ +Goal forall b : bool, match b as b' return if b' then True else True with true => I | false => I end = match b as b' return if b' then True else True with true => I | false => I end. +intro. +Fail lazymatch goal with +| [ |- appcontext[match ?b as b' return @?P b' with true => ?t | false => ?f end] ] + => change (match b as b' return P b with true => t | false => f end) with (@bool_rect P t f) +end. (* Toplevel input, characters 153-154: +Error: The reference P was not found in the current environment. *) diff --git a/test-suite/bugs/opened/3388.v b/test-suite/bugs/opened/3388.v new file mode 100644 index 0000000000..d0ea72e1fd --- /dev/null +++ b/test-suite/bugs/opened/3388.v @@ -0,0 +1,57 @@ +Inductive test : bool -> bool -> Type := +| test00 : test false false +| test01 : test false true +| test10 : test true false +. + +(* This does not work *) +Fail Definition test_a (t : test true false) : test true false := + match t with + | test10 => test10 + end. + +(* The following definition shows that test_a SHOULD work *) +Definition test_a_workaround (t : test true false) : test true false := + match t with + | test10 => test10 + | _ => tt + end. + +(* Surprisingly, this works *) +Definition test_b (t : test false true) : test false true := + match t with + | test01 => test01 + end. + + +(* This, too, works *) +Definition test_c x (t : test false x) : test false x := + match t with + | test00 => test00 + | test01 => test01 + end. + +Inductive test2 : bool -> bool -> Type := +| test201 : test2 false true +| test210 : test2 true false +| test211 : test2 true true +. + +(* Now this works *) +Definition test2_a (t : test2 true false) : test2 true false := + match t with + | test210 => test210 + end. + +(* Accordingly, this now fails *) +Fail Definition test2_b (t : test2 false true) : test2 false true := + match t with + | test201 => test201 + end. + + +(* This, too, fails *) +Fail Definition test2_c x (t : test2 false x) : test2 false x := + match t with + | test201 => test201 + end. diff --git a/test-suite/bugs/opened/3395.v b/test-suite/bugs/opened/3395.v new file mode 100644 index 0000000000..ff0dbf9745 --- /dev/null +++ b/test-suite/bugs/opened/3395.v @@ -0,0 +1,230 @@ +(* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines, 2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *) +Generalizable All Variables. +Set Implicit Arguments. + +Arguments fst {_ _} _. +Arguments snd {_ _} _. + +Axiom cheat : forall {T}, T. + +Reserved Notation "g 'o' f" (at level 40, left associativity). + +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. +Arguments idpath {A a} , [A] a. +Notation "x = y" := (paths x y) : type_scope. + +Definition symmetry {A : Type} {x y : A} (p : x = y) : y = x + := match p with idpath => idpath end. + +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope object_scope with object. +Record PreCategory (object : Type) := + Build_PreCategory' { + object :> Type := object; + morphism : object -> object -> Type; + identity : forall x, morphism x x; + compose : forall s d d', + morphism d d' + -> morphism s d + -> morphism s d' + where "f 'o' g" := (compose f g); + associativity : forall x1 x2 x3 x4 + (m1 : morphism x1 x2) + (m2 : morphism x2 x3) + (m3 : morphism x3 x4), + (m3 o m2) o m1 = m3 o (m2 o m1); + associativity_sym : forall x1 x2 x3 x4 + (m1 : morphism x1 x2) + (m2 : morphism x2 x3) + (m3 : morphism x3 x4), + m3 o (m2 o m1) = (m3 o m2) o m1; + left_identity : forall a b (f : morphism a b), identity b o f = f; + right_identity : forall a b (f : morphism a b), f o identity a = f; + identity_identity : forall x, identity x o identity x = identity x + }. +Bind Scope category_scope with PreCategory. +Arguments PreCategory {_}. +Arguments identity {_} [!C%category] x%object : rename. + +Arguments compose {_} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename. + +Infix "o" := compose : morphism_scope. + +Delimit Scope functor_scope with functor. +Local Open Scope morphism_scope. +Record Functor `(C : @PreCategory objC, D : @PreCategory objD) := + { + object_of :> C -> D; + morphism_of : forall s d, morphism C s d + -> morphism D (object_of s) (object_of d); + composition_of : forall s d d' + (m1 : morphism C s d) (m2: morphism C d d'), + morphism_of _ _ (m2 o m1) + = (morphism_of _ _ m2) o (morphism_of _ _ m1); + identity_of : forall x, morphism_of _ _ (identity x) + = identity (object_of x) + }. +Bind Scope functor_scope with Functor. + +Arguments morphism_of {_} [C%category] {_} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. + +Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope. + +Class IsIsomorphism `{C : @PreCategory objC} {s d} (m : morphism C s d) := + { + morphism_inverse : morphism C d s; + left_inverse : morphism_inverse o m = identity _; + right_inverse : m o morphism_inverse = identity _ + }. + +Definition opposite `(C : @PreCategory objC) : PreCategory + := @Build_PreCategory' + C + (fun s d => morphism C d s) + (identity (C := C)) + (fun _ _ _ m1 m2 => m2 o m1) + (fun _ _ _ _ _ _ _ => @associativity_sym _ _ _ _ _ _ _ _ _) + (fun _ _ _ _ _ _ _ => @associativity _ _ _ _ _ _ _ _ _) + (fun _ _ => @right_identity _ _ _ _) + (fun _ _ => @left_identity _ _ _ _) + (@identity_identity _ C). + +Notation "C ^op" := (opposite C) (at level 3) : category_scope. + +Definition prod `(C : @PreCategory objC, D : @PreCategory objD) : @PreCategory (objC * objD). + refine (@Build_PreCategory' + (C * D)%type + (fun s d => (morphism C (fst s) (fst d) + * morphism D (snd s) (snd d))%type) + (fun x => (identity (fst x), identity (snd x))) + (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1)) + _ + _ + _ + _ + _); admit. +Defined. +Infix "*" := prod : category_scope. + +Definition compose_functor `(C : @PreCategory objC, D : @PreCategory objD, E : @PreCategory objE) (G : Functor D E) (F : Functor C D) : Functor C E + := Build_Functor + C E + (fun c => G (F c)) + (fun _ _ m => morphism_of G (morphism_of F m)) + cheat + cheat. + +Infix "o" := compose_functor : functor_scope. + +Record NaturalTransformation `(C : @PreCategory objC, D : @PreCategory objD) (F G : Functor C D) := + Build_NaturalTransformation' { + components_of :> forall c, morphism D (F c) (G c); + commutes : forall s d (m : morphism C s d), + components_of d o F _1 m = G _1 m o components_of s; + + commutes_sym : forall s d (m : C.(morphism) s d), + G _1 m o components_of s = components_of d o F _1 m + }. +Definition functor_category `(C : @PreCategory objC, D : @PreCategory objD) : PreCategory + := @Build_PreCategory' (Functor C D) + (@NaturalTransformation _ C _ D) + cheat + cheat + cheat + cheat + cheat + cheat + cheat. + +Definition opposite_functor `(F : @Functor objC C objD D) : Functor C^op D^op + := Build_Functor (C^op) (D^op) + (object_of F) + (fun s d => morphism_of F (s := d) (d := s)) + (fun d' d s m1 m2 => composition_of F s d d' m2 m1) + (identity_of F). + +Definition opposite_invL `(F : @Functor objC C^op objD D) : Functor C D^op + := Build_Functor C (D^op) + (object_of F) + (fun s d => morphism_of F (s := d) (d := s)) + (fun d' d s m1 m2 => composition_of F s d d' m2 m1) + (identity_of F). +Notation "F ^op" := (opposite_functor F) : functor_scope. + +Notation "F ^op'L" := (opposite_invL F) (at level 3) : functor_scope. +Definition fst `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) C + := Build_Functor (C * D) C + (@fst _ _) + (fun _ _ => @fst _ _) + (fun _ _ _ _ _ => idpath) + (fun _ => idpath). + +Definition snd `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) D + := Build_Functor (C * D) D + (@snd _ _) + (fun _ _ => @snd _ _) + (fun _ _ _ _ _ => idpath) + (fun _ => idpath). +Definition prod_functor `(F : @Functor objC C objD D, F' : @Functor objC C objD' D') +: Functor C (D * D') + := Build_Functor + C (D * D') + (fun c => (F c, F' c)) + (fun s d m => (F _1 m, F' _1 m))%morphism + cheat + cheat. +Definition pair `(F : @Functor objC C objD D, F' : @Functor objC' C' objD' D') : Functor (C * C') (D * D') + := (prod_functor (F o fst) (F' o snd))%functor. +Notation cat_of obj := + (@Build_PreCategory' obj + (fun x y => forall _ : x, y) + (fun _ x => x) + (fun _ _ _ f g x => f (g x))%core + (fun _ _ _ _ _ _ _ => idpath) + (fun _ _ _ _ _ _ _ => idpath) + (fun _ _ _ => idpath) + (fun _ _ _ => idpath) + (fun _ => idpath)). + +Definition hom_functor `(C : @PreCategory objC) : Functor (C^op * C) (cat_of Type) + := Build_Functor _ _ cheat cheat cheat cheat. + +Definition induced_hom_natural_transformation `(F : @Functor objC C objD D) +: NaturalTransformation (hom_functor C) (hom_functor D o pair F^op F) + := Build_NaturalTransformation' _ _ cheat cheat cheat. + +Class IsFullyFaithful `(F : @Functor objC C objD D) + := is_fully_faithful + : forall x y : C, + IsIsomorphism (induced_hom_natural_transformation F (x, y)). + +Definition coyoneda `(A : @PreCategory objA) : Functor A^op (@functor_category _ A _ (cat_of Type)) + := cheat. + +Definition yoneda `(A : @PreCategory objA) : Functor A (@functor_category _ A^op _ (cat_of Type)) + := (((coyoneda A^op)^op'L)^op'L)%functor. +Definition coyoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@coyoneda _ A). +Admitted. + +Definition yoneda_embedding_fast `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). +Proof. + intros a b. + pose proof (coyoneda_embedding A^op a b) as CYE. + unfold yoneda. + Time let t := (type of CYE) in + let t' := (eval simpl in t) in pose proof ((fun (x : t) => (x : t')) CYE) as CYE'. (* Finished transaction in 0. secs (0.216013u,0.004s) *) + Fail Timeout 1 let t := match goal with |- ?G => constr:(G) end in + let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). + Time let t := match goal with |- ?G => constr:(G) end in + let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). (* Finished transaction in 0. secs (0.248016u,0.s) *) +Fail Timeout 2 Defined. +Time Defined. (* Finished transaction in 1. secs (0.432027u,0.s) *) + +Definition yoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). +Proof. + intros a b. + pose proof (coyoneda_embedding A^op a b) as CYE. + unfold yoneda; simpl in *. + Fail Timeout 1 exact CYE. + Time exact CYE. (* Finished transaction in 0. secs (0.012001u,0.s) *) diff --git a/test-suite/bugs/opened/HoTT_coq_078.v b/test-suite/bugs/opened/HoTT_coq_078.v index 6c02cad567..a2c97d0675 100644 --- a/test-suite/bugs/opened/HoTT_coq_078.v +++ b/test-suite/bugs/opened/HoTT_coq_078.v @@ -35,7 +35,7 @@ Definition transport_prod' {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a') | idpath => idpath end. (* success *) -Definition transport_prod {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a') +Fail Definition transport_prod {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a') (z : P a * Q a) : transport (fun a => P a * Q a) p z = (transport _ p (fst z), transport _ p (snd z)) := match p with diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 068dfb2ee0..df114d059a 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/command.ml b/toplevel/command.ml index 1f9d725b83..faa4b12dfd 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -935,7 +935,7 @@ let interp_recursive isfix fixl notations = List.fold_left2 (fun env' id t -> if Flags.is_program_mode () then - let sort = Retyping.get_type_of env !evdref t in + let sort = Evarutil.evd_comb1 (Typing.e_type_of ~refresh:true env) evdref t in let fixprot = try let app = mkApp (delayed_force fix_proto, [|sort; t|]) in diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 85a59c50ee..2f778be364 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -92,6 +92,10 @@ let init_load_path () = (* NOTE: These directories are searched from last to first *) (* first, developer specific directory to open *) if Coq_config.local then coq_add_path (coqlib/"dev") "dev"; + (* 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/"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 a4770b348a..d64e3d979d 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -38,6 +38,20 @@ let print_header () = ppnl (str ("Welcome to Coq "^ver^" ("^rev^")")); pp_flush () +let warning s = msg_warning (strbrk s) + +let toploop = ref None +let toploop_init = ref (fun x -> x) +let toploop_run = ref (fun () -> + if Dumpglob.dump () then begin + if_verbose warning "Dumpglob cannot be used in interactive mode."; + Dumpglob.noglob () + end; + Coqloop.loop(); + (* Initialise and launch the Ocaml toplevel *) + Coqinit.init_ocaml_path(); + Mltop.ocaml_toploop()) + let output_context = ref false let memory_stat = ref false @@ -201,8 +215,6 @@ let error_missing_arg s = prerr_endline "See --help for the syntax of supported options"; exit 1 -let warning s = msg_warning (strbrk s) - let filter_opts = ref false let exitcode () = if !filter_opts then 2 else 0 @@ -217,6 +229,7 @@ let get_async_proofs_mode opt next = function | "on" -> Flags.APonParallel 0 | "worker" -> let n = int_of_string (next()) in assert (n > 0); + toploop := Some "stmworkertop"; Flags.APonParallel n | "lazy" -> Flags.APonLazy | _ -> prerr_endline ("Error: on/off/lazy/worker expected after "^opt); exit 1 @@ -341,7 +354,7 @@ let parse_args arglist = |"-async-proofs-j" -> Flags.async_proofs_n_workers := (get_int opt (next ())) |"-async-proofs-worker-flags" -> - Flags.async_proofs_worker_flags := Some (next ()) + Flags.async_proofs_worker_flags := Some (next ()); |"-compat" -> Flags.compat_version := get_compat_version (next ()) |"-compile" -> add_compile false (next ()) |"-compile-verbose" -> add_compile true (next ()) @@ -363,6 +376,7 @@ let parse_args arglist = |"-main-channel" -> Spawned.main_channel := get_host_port opt (next()) |"-control-channel" -> Spawned.control_channel := get_host_port opt (next()) |"-vi2vo" -> add_compile false (next ()); Flags.compilation_mode := Vi2Vo + |"-toploop" -> toploop := Some (next ()) (* Options with zero arg *) |"-batch" -> set_batch_mode () @@ -375,9 +389,7 @@ 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" -> Flags.ide_slave := true + |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet |"-indices-matter" -> Indtypes.enforce_indices_matter () |"-just-parsing" -> Vernac.just_parsing := true @@ -436,27 +448,22 @@ let init arglist = begin try let extras = parse_args arglist in - if not (List.is_empty extras) && not !filter_opts then begin - prerr_endline ("Don't know what to do with " ^ String.concat " " extras); - prerr_endline "See --help for the list of supported options"; - exit 1 - end; (* If we have been spawned by the Spawn module, this has to be done * early since the master waits us to connect back *) Spawned.init_channels (); Envars.set_coqlib Errors.error; - if !print_where then (print_endline (Envars.coqlib ()); exit (exitcode ())); + if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ())); if !print_config then (Usage.print_config (); exit (exitcode ())); if !filter_opts then (print_string (String.concat "\n" extras); exit 0); - if !Flags.ide_slave then begin - Flags.make_silent true; - Ide_slave.init_stdout () - end else if Flags.async_proofs_is_worker () then begin - Flags.make_silent true; - Stm.slave_init_stdout () + init_load_path (); + Option.iter Mltop.load_ml_object_raw !toploop; + let extras = !toploop_init extras in + if not (List.is_empty extras) then begin + prerr_endline ("Don't know what to do with "^String.concat " " extras); + prerr_endline "See --help for the list of supported options"; + exit 1 end; if_verbose print_header (); - init_load_path (); inputstate (); Mltop.init_known_plugins (); set_vm_opt (); @@ -500,18 +507,7 @@ let start () = let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in (* In batch mode, Coqtop has already exited at this point. In interactive one, dump glob is nothing but garbage ... *) - if !Flags.ide_slave then - Ide_slave.loop () - else if Flags.async_proofs_is_worker () then - Stm.slave_main_loop () - else - let () = if Dumpglob.dump () then - let () = if_verbose warning "Dumpglob cannot be used in interactive mode." in - Dumpglob.noglob () in - Coqloop.loop(); - (* Initialise and launch the Ocaml toplevel *) - Coqinit.init_ocaml_path(); - Mltop.ocaml_toploop(); + !toploop_run (); exit 1 (* [Coqtop.start] will be called by the code produced by coqmktop *) diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index ee511edbbc..875cf2ec0f 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -14,3 +14,9 @@ val init_toplevel : string list -> unit val start : unit -> unit + + +(* For other toploops *) +val toploop_init : (string list -> string list) ref +val toploop_run : (unit -> unit) ref + diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 11f00d6e54..695fd3b82e 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -211,7 +211,8 @@ let file_of_name name = let suffix = get_ml_object_suffix name in let fail s = errorlabstrm "Mltop.load_object" - (str"File not found on loadpath : " ++ str s) in + (str"File not found on loadpath : " ++ str s ++ str"\n" ++ + str"Loadpath: " ++ str(String.concat ":" !coq_mlpath_copy)) in if is_native then let name = match suffix with | Some ((".cmo"|".cma") as suffix) -> @@ -290,6 +291,8 @@ let load_ml_object mname fname= add_known_module mname; init_ml_object mname +let load_ml_object_raw fname = dir_ml_load (file_of_name fname) + (* Summary of declared ML Modules *) (* List and not String.Set because order is important: most recent first. *) diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli index 196c0bf94b..a4ba732d26 100644 --- a/toplevel/mltop.mli +++ b/toplevel/mltop.mli @@ -54,6 +54,7 @@ val add_rec_path : unix_path:string -> coq_root:Names.DirPath.t -> implicit:bool val add_known_module : string -> unit val module_is_known : string -> bool val load_ml_object : string -> string -> unit +val load_ml_object_raw : string -> unit (** {5 Initialization functions} *) diff --git a/toplevel/search.ml b/toplevel/search.ml index 37403504db..016b9f22b5 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 c06a64be17..a69a8db79c 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/toplevel.mllib b/toplevel/toplevel.mllib index a5519d5860..d22524e5ca 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -15,7 +15,6 @@ Mltop Vernacentries Whelp Vernac -Ide_slave Usage Coqloop Coqinit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 2e97b74d66..b1ed564d81 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 |