diff options
| author |  Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
| commit | d2c5c5e616a6e118291fe1ce9965c731adac03a8 (patch) | |
| tree | 7b000ad50dcc45ff1c63768a983cded1e23a07ca | |
| parent | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (diff) | |
Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg
62 files changed, 910 insertions, 508 deletions
@@ -1,3 +1,34 @@ +Changes from V8.4pl2 to V8.4pl3 +=============================== + +Ide_slave XML interface + +- 20120712, 20130419 : Invalidated protocol versions +- From 20130419 extra datastructure : union + (Inl "" = <union val="in_l"><string></string></union>, + Inr _ = <union val="in_r">...) +- 20130419~1 : new toplevel entry : message, not send by coptop v8.4 and not + handle by coqide v8.4. A message has a level and a content (of string). + Message levels are Debug of string, Info, Notice, Warning and Error. +- 20130425 : + * new toplevel entry : feedback, once again not send by coqtop v8.4 and not + handle by coqide v8.4. A feedback gives the id of the sentence it provides info + about and a content. Feedback contents are Processed, AddedAxiom and + GlobRef of Util.loc * string * string * string * string + * <call val="interp"> must provide an attribute id of type int. It is OK in + coqtop v8.4 to alwais send <call val="interp" id="0"> + +Bug fixes + +- Solved bugs: + #2230 #2837 #2846 #2987 #3003 #3001 #3013 #3023 #3025 #3036 #3118 #3169 + #(3150, 3151, 3152, 3153) +- Fixing a significant efficiency leak in the code of the field tactic. +- Fix caching of local hint database in typeclasses eauto which could + miss some hypotheses. +- Fix automatic solving of obligation in program, which was not trying + to solve obligations that had no undefined dependencies left. + Changes from V8.4pl1 to V8.4pl2 =============================== @@ -28,7 +28,7 @@ AVAILABILITY. ============= Coq is available at http://coq.inria.fr, or, for older versions at - ftp://ftp.inria.fr/INRIA/LogiCal/coq. + ftp://ftp.inria.fr/INRIA/Projects/LogiCal/coq. THE COQ CLUB. @@ -8,11 +8,11 @@ <tools/coq_tex.{native,byte}> : use_str <tools/coq_makefile.{native,byte}> : use_str, use_unix <tools/coqdoc/main.{native,byte}> : use_str -<ide/coqide_main.{native,byte}> : use_str, use_unix, thread, ide +<ide/coqide_main.{native,byte}> : use_str, use_unix, thread, ide, use_camlpX <checker/main.{native,byte}> : use_str, use_unix, use_dynlink, use_camlpX <plugins/micromega/csdpcert.{native,byte}> : use_nums, use_unix <tools/mkwinapp.{native,byte}> : use_unix -<tools/fake_ide.{native,byte}> : use_unix +<tools/fake_ide.{native,byte}> : use_unix, use_camlpX ## tags for ide @@ -6,7 +6,7 @@ # ################################## -VERSION=8.4pl2 +VERSION=8.4pl3 VOMAGIC=08400 STATEMAGIC=58400 DATE=`LC_ALL=C LANG=C date +"%B %Y"` @@ -332,10 +332,11 @@ fi MAKE=`which ${makecmd:-make}` if [ "$MAKE" != "" ]; then - MAKEVERSION=`$MAKE -v | head -1 | cut -d" " -f3` + # Beware of the final \r in Win32 + MAKEVERSION=`"$MAKE" -v | head -1 | tr -d "\r" | cut -d" " -f3` MAKEVERSIONMAJOR=`echo $MAKEVERSION | cut -d. -f1` MAKEVERSIONMINOR=`echo $MAKEVERSION | cut -d. -f2` - if [ "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then + if [ "$MAKEVERSIONMAJOR" -gt 3 -o "$MAKEVERSIONMAJOR" -eq 3 -a "$MAKEVERSIONMINOR" -ge 81 ]; then echo "You have GNU Make $MAKEVERSION. Good!" else OK="no" @@ -521,16 +522,23 @@ case $usecamlp5 in echo "Configuration script failed!" exit 1 fi - elif [ -f "${CAMLLIB}/camlp5/${CAMLP4MOD}.cma" ]; then - CAMLP4LIB=+camlp5 - FULLCAMLP4LIB=${CAMLLIB}/camlp5 - elif [ -f "${CAMLLIB}/site-lib/${CAMLP4MOD}.cma" ]; then + else + # Beware of the final \r in Win32 + camlp5dir="$(camlp5 -where | tr -d '\r')" + if [ "$camlp5dir" != "" ]; then + CAMLP4LIB=$camlp5dir + FULLCAMLP4LIB=$camlp5dir + elif [ -f "${CAMLLIB}/camlp5/${CAMLP4MOD}.cma" ]; then + CAMLP4LIB=+camlp5 + FULLCAMLP4LIB=${CAMLLIB}/camlp5 + elif [ -f "${CAMLLIB}/site-lib/${CAMLP4MOD}.cma" ]; then CAMLP4LIB=+site-lib/camlp5 FULLCAMLP4LIB=${CAMLLIB}/site-lib/camlp5 - else - echo "No Camlp5 installation found. Looking for Camlp4 instead..." - usecamlp5=no - fi + else + echo "No Camlp5 installation found. Looking for Camlp4 instead..." + usecamlp5=no + fi + fi esac # If we're (still...) going to use Camlp5, let's check its version @@ -623,7 +631,9 @@ if [ "$coqide_spec" = "yes" -a "$COQIDE" = "no" ]; then else case $lablgtkdir_spec in no) - if lablgtkdirtmp=$(ocamlfind query lablgtk2 2> /dev/null); then + # Beware of the final \r in Win32 + lablgtkdirtmp="$(ocamlfind query lablgtk2 2> /dev/null | tr -d '\r')" + if [ "$lablgtkdirtmp" != "" ]; then if [ -f "$lablgtkdirtmp/glib.cmi" -a -f "$lablgtkdirtmp/glib.mli" ]; then lablgtkdirfoundmsg="LabelGtk2 found by ocamlfind" lablgtkdir=$lablgtkdirtmp @@ -632,7 +642,7 @@ else echo "Headers missings in Lablgtk2 found by ocamlfind (glib.cmi/glib.mli not found)." fi fi - if [ "$lablgtkdir" = "" -a -f "${CAMLLIB}/lablgtk2/glib.mli" -a -f "${CAMLLIB}/glib.mli" ]; then + if [ "$lablgtkdir" = "" -a -f "${CAMLLIB}/lablgtk2/glib.cmi" -a -f "${CAMLLIB}/lablgtk2/glib.mli" ]; then lablgtkdirfoundmsg="LablGtk2 found in ocaml lib directory" lablgtkdir=${CAMLLIB}/lablgtk2 LABLGTKLIB=+lablgtk2 # Pour le message utilisateur @@ -887,7 +897,7 @@ case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM_OS in */true/*/*) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$COQTOP'/kernel/byterun";; *) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$LIBDIR'" - BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun";; + BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun:$CAML_LD_LIBRARY_PATH";; esac case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";; diff --git a/ide/command_windows.ml b/ide/command_windows.ml index 470bd5b4..d496e9fd 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -84,10 +84,6 @@ object(self) ~packing:hbox#pack () in - let on_activate c () = - if List.mem combo#entry#text Coq_commands.state_preserving then c () - else prerr_endline "Not a state preserving command" - in let entry = GEdit.entry ~packing:(hbox#pack ~expand:true) () in entry#misc#set_can_default true; let r_bin = @@ -103,6 +99,10 @@ object(self) result#misc#modify_base [`NORMAL, `COLOR clr]; result#misc#set_can_focus true; (* false causes problems for selection *) result#set_editable false; + let on_activate c () = + if List.mem combo#entry#text Coq_commands.state_preserving then c () + else result#buffer#set_text "Error: Not a state preserving command" + in let callback () = let com = combo#entry#text in let phrase = @@ -111,7 +111,7 @@ object(self) in try result#buffer#set_text - (match Coq.interp !coqtop ~raw:true phrase with + (match Coq.interp !coqtop ~raw:true 0 phrase with | Interface.Fail (l,str) -> ("Error while interpreting "^phrase^":\n"^str) | Interface.Good results -> @@ -270,13 +270,13 @@ let eval_call coqtop (c:'a Ide_intf.call) = let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in (Ide_intf.to_answer xml c : 'a Interface.value) -let interp coqtop ?(raw=false) ?(verbose=true) s = - eval_call coqtop (Ide_intf.interp (raw,verbose,s)) +let interp coqtop ?(raw=false) ?(verbose=true) i s = + eval_call coqtop (Ide_intf.interp (i,raw,verbose,s)) let rewind coqtop i = eval_call coqtop (Ide_intf.rewind i) let inloadpath coqtop s = eval_call coqtop (Ide_intf.inloadpath s) let mkcases coqtop s = eval_call coqtop (Ide_intf.mkcases s) -let status coqtop = eval_call coqtop Ide_intf.status -let hints coqtop = eval_call coqtop Ide_intf.hints +let status coqtop = eval_call coqtop (Ide_intf.status ()) +let hints coqtop = eval_call coqtop (Ide_intf.hints ()) module PrintOpt = struct @@ -308,8 +308,8 @@ end let goals coqtop = let () = PrintOpt.enforce_hack coqtop in - eval_call coqtop Ide_intf.goals + eval_call coqtop (Ide_intf.goals ()) let evars coqtop = let () = PrintOpt.enforce_hack coqtop in - eval_call coqtop Ide_intf.evars + eval_call coqtop (Ide_intf.evars ()) diff --git a/ide/coq.mli b/ide/coq.mli index f25268ef..0f40c61e 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -47,7 +47,7 @@ val interrupter : (int -> unit) ref (** * Calls to Coqtop, cf [Ide_intf] for more details *) val interp : - coqtop -> ?raw:bool -> ?verbose:bool -> string -> string Interface.value + coqtop -> ?raw:bool -> ?verbose:bool -> int -> string -> string Interface.value val rewind : coqtop -> int -> int Interface.value val status : coqtop -> Interface.status Interface.value val goals : coqtop -> Interface.goals option Interface.value diff --git a/ide/coqide.ml b/ide/coqide.ml index 94be8318..76094abe 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -868,11 +868,9 @@ object(self) prerr_endline "Send_to_coq starting now"; (* It's important here to work with [ct] and not [!mycoqtop], otherwise we could miss a restart of coqtop and continue sending it orders. *) - match Coq.interp ct ~verbose phrase with + match Coq.interp ct ~verbose 0 phrase with | Interface.Fail (l,str) -> sync display_error (l,str); None | Interface.Good msg -> sync display_output msg; Some Safe - (* TODO: Restore someday the access to Decl_mode.get_damon_flag, - and also detect the use of admit, and then return Unsafe *) with | End_of_file -> (* Coqtop has died, let's trigger a reset_initial. *) raise RestartCoqtop @@ -890,9 +888,10 @@ object(self) end in try - match Coq.interp !mycoqtop ~raw:true ~verbose:false phrase with + match Coq.interp !mycoqtop ~raw:true ~verbose:false 0 phrase with | Interface.Fail (_, err) -> sync display_error err - | Interface.Good msg -> sync self#insert_message msg + | Interface.Good msg -> + sync self#insert_message msg with | End_of_file -> raise RestartCoqtop | e -> sync display_error (Printexc.to_string e) @@ -1256,7 +1255,7 @@ object(self) | Interface.Good true -> () | Interface.Good false -> let cmd = Printf.sprintf "Add LoadPath \"%s\". " dir in - match Coq.interp ct cmd with + match Coq.interp ct 0 cmd with | Interface.Fail (l,str) -> self#set_message ("Couln't add loadpath:\n"^str) | Interface.Good _ -> () diff --git a/interp/topconstr.ml b/interp/topconstr.ml index b02a67ea..dff8844d 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -1075,7 +1075,7 @@ let fold_constr_expr_with_binders g f n acc = function fold_local_binders g f n' (fold_local_binders g f n acc t lb) c lb) l acc | CCoFix (loc,_,_) -> - Pp.warning "Capture check in multiple binders not done"; acc + Pp.msg_warn "Capture check in multiple binders not done"; acc let free_vars_of_constr_expr c = let rec aux bdvars l = function diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index da34d81e..dc2220c1 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cbytecodes.mli 15714 2012-08-08 18:54:37Z herbelin $ *) +(* $Id$ *) open Names open Term diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index 565c31ae..179e4820 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: csymtable.mli 15714 2012-08-08 18:54:37Z herbelin $ *) +(* $Id$ *) open Names open Term diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 0dd2cd69..9ca838fc 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -42,7 +42,7 @@ type inductive_error = | SameNamesTypes of identifier | SameNamesConstructors of identifier | SameNamesOverlap of identifier list - | NotAnArity of identifier + | NotAnArity of env * constr | BadEntry | LargeNonPropInductiveNotInType @@ -254,7 +254,10 @@ let typecheck_inductive env mie = let ind_min_levels = inductive_levels arities inds in let inds, cst = array_fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst -> - let sign, s = dest_arity env full_arity in + let sign, s = + try dest_arity env full_arity + with NotArity -> raise (InductiveError (NotAnArity (env, full_arity))) + in let status,cst = match s with | Type u when ar_level <> None (* Explicitly polymorphic *) && no_upper_constraints u cst -> diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 4d71a81d..077a2b4f 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -28,7 +28,7 @@ type inductive_error = | SameNamesTypes of identifier | SameNamesConstructors of identifier | SameNamesOverlap of identifier list - | NotAnArity of identifier + | NotAnArity of env * constr | BadEntry | LargeNonPropInductiveNotInType diff --git a/kernel/univ.ml b/kernel/univ.ml index 028eaeb4..e8c1fed9 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -161,7 +161,7 @@ let type0_univ = Atom UniverseLevel.Set let is_type0_univ = function | Atom UniverseLevel.Set -> true - | Max ([UniverseLevel.Set], []) -> warning "Non canonical Set"; true + | Max ([UniverseLevel.Set], []) -> msg_warn "Non canonical Set"; true | u -> false let is_univ_variable = function @@ -341,6 +341,7 @@ let msgnl x = msgnl_with !std_ft x let msgerr x = msg_with !err_ft x let msgerrnl x = msgnl_with !err_ft x let msg_warning x = msg_warning_with !err_ft x +let msg_warn x = msg_warning (str x) (* Same specific display in emacs as warning, but without the "Warning:" *) let msg_debug x = msgnl (emacs_quote x) @@ -116,6 +116,7 @@ val msgnl : std_ppcmds -> unit val msgerr : std_ppcmds -> unit val msgerrnl : std_ppcmds -> unit val msg_warning : std_ppcmds -> unit +val msg_warn : string -> unit (** Same specific display in emacs as warning, but without the "Warning:" **) val msg_debug : std_ppcmds -> unit diff --git a/library/library.ml b/library/library.ml index c857fc86..8620c0a5 100644 --- a/library/library.ml +++ b/library/library.ml @@ -656,7 +656,7 @@ let save_library_to dir f = System.marshal_out ch table; close_out ch with reraise -> - warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise reraise + msg_warn ("Removed file "^f'); close_out ch; Sys.remove f'; raise reraise (************************************************************************) (*s Display the memory use of a library. *) diff --git a/myocamlbuild.ml b/myocamlbuild.ml index 7a214bcd..5b873fce 100644 --- a/myocamlbuild.ml +++ b/myocamlbuild.ml @@ -76,13 +76,15 @@ end let use_camlp5 = (Coq_config.camlp4 = "camlp5") +let camlp4lib = if w32 then w32lib^"ocaml/camlp5" else Coq_config.camlp4lib + let camlp4args = if use_camlp5 then [A "pa_extend.cmo";A "q_MLast.cmo";A "pa_macro.cmo"] else [] let ocaml = A Coq_config.ocaml let camlp4o = S ((A Coq_config.camlp4o) :: camlp4args) -let camlp4incl = S[A"-I"; A Coq_config.camlp4lib] +let camlp4incl = S[A"-I"; A camlp4lib] let camlp4compat = Sh Coq_config.camlp4compat let opt = (Coq_config.best = "opt") let ide = Coq_config.has_coqide @@ -301,7 +303,7 @@ let extra_rules () = begin mlp_cmo "tools/compat5b"; end; - ocaml_lib ~extern:true ~dir:Coq_config.camlp4lib ~tag_name:"use_camlpX" + ocaml_lib ~extern:true ~dir:camlp4lib ~tag_name:"use_camlpX" ~byte:true ~native:true (if use_camlp5 then "gramlib" else "camlp4lib"); (** Special case of toplevel/mltop.ml4: @@ -322,7 +324,7 @@ let extra_rules () = begin Cmd (S [!Options.ocamlc; A"-c"; A"-pp"; Quote (S [camlp4o; T(tags_of_pathname ml4 ++ "p4mod"); A"-DByte";A"-DHasDynlink";camlp4compat;A"-impl"]); - A"-rectypes"; camlp4incl; incl ml4; A"-impl"; P ml4])); + A"-rectypes"; A"-impl"; P ml4])); (** All caml files are compiled with -rectypes and +camlp4/5 and ide files need +lablgtk2 *) diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index caea30b2..c8e67f4d 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -656,7 +656,7 @@ let strip s = let terminal s = let s = strip s in - if s = "" then failwith "empty token"; + if s = "" then Util.error "empty token."; if is_ident_not_keyword s then IDENT s else if is_number s then INT s else KEYWORD s diff --git a/parsing/printer.ml b/parsing/printer.ml index 29ebe4fa..a5bd30b1 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -571,7 +571,7 @@ let pr_prim_rule = function (str"fix " ++ pr_id f ++ str"/" ++ int n) | FixRule (f,n,others,j) -> - if j<>0 then warning "Unsupported printing of \"fix\""; + if j<>0 then msg_warn "Unsupported printing of \"fix\""; let rec print_mut = function | (f,n,ar)::oth -> pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth @@ -583,7 +583,7 @@ let pr_prim_rule = function (str"cofix " ++ pr_id f) | Cofix (f,others,j) -> - if j<>0 then warning "Unsupported printing of \"fix\""; + if j<>0 then msg_warn "Unsupported printing of \"fix\""; let rec print_mut = function | (f,ar)::oth -> (pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth) diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 4f4f2039..7b746396 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -248,11 +248,11 @@ Fixpoint interpret3 t fv {struct t}: R := End nsatz1. Ltac equality_to_goal H x y:= - let h := fresh "nH" in (* eliminate trivial hypotheses, but it takes time!: + let h := fresh "nH" in (assert (h:equality x y); [solve [cring] | clear H; clear h]) - || *) (try generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H) + || *) try (generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H) . Ltac equalities_to_goal := diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v index 8ac952c0..013fd0ef 100644 --- a/plugins/setoid_ring/Field_tac.v +++ b/plugins/setoid_ring/Field_tac.v @@ -201,7 +201,8 @@ Ltac fold_field_cond req := Ltac simpl_PCond FLD := let req := get_FldEq FLD in let lemma := get_CondLemma FLD in - try apply lemma; + try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; + clear lock_def lock); protect_fv "field_cond"; fold_field_cond req; try exact I. @@ -209,7 +210,8 @@ Ltac simpl_PCond FLD := Ltac simpl_PCond_BEURK FLD := let req := get_FldEq FLD in let lemma := get_CondLemma FLD in - apply lemma; + try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; + clear lock_def lock); protect_fv "field_cond"; fold_field_cond req. diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index bc05c252..1989e9b3 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1507,13 +1507,15 @@ Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) := | cons a l1 => Fcons a (Fapp l1 m) end. -Lemma fcons_correct : forall l l1, - PCond l (Fapp l1 nil) -> PCond l l1. -induction l1; simpl; intros. - trivial. - elim PCond_fcons_inv with (1 := H); intros. - destruct l1; auto. -Qed. + Lemma fcons_correct : forall l l1, + (forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1. + Proof. + intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1. + induction l1; simpl; intros. + trivial. + elim PCond_fcons_inv with (1 := H); intros. + destruct l1; trivial. split; trivial. apply IHl1; trivial. + Qed. End Fcons_impl. diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index d8f46098..7a4916fa 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -559,14 +559,18 @@ and solve_prg_obligations prg ?oblset tac = let obls, rem = prg.prg_obligations in let rem = ref rem in let obls' = Array.copy obls in + let set = ref Intset.empty in let p = match oblset with | None -> (fun _ -> true) - | Some s -> (fun i -> Intset.mem i s) + | Some s -> set := s; + (fun i -> Intset.mem i !set) in let _ = Array.iteri (fun i x -> - if p i && solve_obligation_by_tac prg obls' i tac then - decr rem) + if p i && solve_obligation_by_tac prg obls' i tac then + let deps = dependencies obls i in + (set := Intset.union !set deps; + decr rem)) obls' in update_obls prg obls' !rem diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index a14eda60..165bf83d 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -23,7 +23,7 @@ let get_module_path_of_full_path path = (function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules with [] -> - Pp.warning ("Modules not supported: reference to "^ + Pp.msg_warn ("Modules not supported: reference to "^ Libnames.string_of_path path^" will be wrong"); dirpath | [modul] -> modul diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 867aac71..59ade01e 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -433,46 +433,46 @@ let kind_of_constant kn = | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration" | DK.IsAssumption DK.Logical -> "AXIOM","Axiom" | DK.IsAssumption DK.Conjectural -> - Pp.warning "Conjecture not supported in dtd (used Declaration instead)"; + Pp.msg_warn "Conjecture not supported in dtd (used Declaration instead)"; "AXIOM","Declaration" | DK.IsDefinition DK.Definition -> "DEFINITION","Definition" | DK.IsDefinition DK.Example -> - Pp.warning "Example not supported in dtd (used Definition instead)"; + Pp.msg_warn "Example not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Coercion -> - Pp.warning "Coercion not supported in dtd (used Definition instead)"; + Pp.msg_warn "Coercion not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.SubClass -> - Pp.warning "SubClass not supported in dtd (used Definition instead)"; + Pp.msg_warn "SubClass not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.CanonicalStructure -> - Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)"; + Pp.msg_warn "CanonicalStructure not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Fixpoint -> - Pp.warning "Fixpoint not supported in dtd (used Definition instead)"; + Pp.msg_warn "Fixpoint not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.CoFixpoint -> - Pp.warning "CoFixpoint not supported in dtd (used Definition instead)"; + Pp.msg_warn "CoFixpoint not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Scheme -> - Pp.warning "Scheme not supported in dtd (used Definition instead)"; + Pp.msg_warn "Scheme not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.StructureComponent -> - Pp.warning "StructureComponent not supported in dtd (used Definition instead)"; + Pp.msg_warn "StructureComponent not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.IdentityCoercion -> - Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)"; + Pp.msg_warn "IdentityCoercion not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Instance -> - Pp.warning "Instance not supported in dtd (used Definition instead)"; + Pp.msg_warn "Instance not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsDefinition DK.Method -> - Pp.warning "Method not supported in dtd (used Definition instead)"; + Pp.msg_warn "Method not supported in dtd (used Definition instead)"; "DEFINITION","Definition" | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) -> "THEOREM",DK.string_of_theorem_kind thm | DK.IsProof _ -> - Pp.warning "Unsupported theorem kind (used Theorem instead)"; + Pp.msg_warn "Unsupported theorem kind (used Theorem instead)"; "THEOREM",DK.string_of_theorem_kind DK.Theorem ;; diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index a145508a..92378837 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -56,12 +56,14 @@ let section_segment_of_reference = function | _ -> [] let discharge_rename_args = function - | _, (ReqGlobal (c, names), _) -> - let c' = pop_global_reference c in - let vars = section_segment_of_reference c in - let var_names = List.map (fun (id, _,_,_) -> Name id) vars in - let names' = List.map (fun l -> var_names @ l) names in - Some (ReqGlobal (c', names), (c', names')) + | _, (ReqGlobal (c, names), _ as req) -> + (try + let vars = section_segment_of_reference c in + let c' = pop_global_reference c in + let var_names = List.map (fun (id, _,_,_) -> Name id) vars in + let names' = List.map (fun l -> var_names @ l) names in + Some (ReqGlobal (c', names), (c', names')) + with Not_found -> Some req) | _ -> None let rebuild_rename_args x = x diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 0166b64c..1065aec9 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -300,7 +300,7 @@ let it_destRLambda_or_LetIn_names n c = let a = GVar (dl,x) in aux (n-1) (Name x :: nal) (match c with - | GApp (loc,p,l) -> GApp (loc,c,l@[a]) + | GApp (loc,p,l) -> GApp (loc,p,l@[a]) | _ -> (GApp (dl,c,[a]))) in aux n [] c @@ -481,7 +481,7 @@ and share_names isgoal n l avoid env c t = share_names isgoal (n-1) ((Name id,Explicit,None,t')::l) avoid env appc c' (* If built with the f/n notation: we renounce to share names *) | _ -> - if n>0 then warning "Detyping.detype: cannot factorize fix enough"; + if n>0 then msg_warn "Detyping.detype: cannot factorize fix enough"; let c = detype isgoal avoid env c in let t = detype isgoal avoid env t in (List.rev l,c,t) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0eed1949..f0019448 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -197,6 +197,18 @@ let rec evar_conv_x ts env evd pbty term1 term2 = and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) = + + let eta env evd onleft term l term' l' = + assert (l = []); + let (na,c,body) = destLambda term in + let c = nf_evar evd c in + let env' = push_rel (na,None,c) env in + let appr1 = evar_apprec ts env' evd [] body in + let appr2 = (lift 1 term', List.map (lift 1) l' @ [mkRel 1]) in + if onleft then evar_eqappr_x ts env' evd CONV appr1 appr2 + else evar_eqappr_x ts env' evd CONV appr2 appr1 + in + (* Evar must be undefined since we have flushed evars *) match (flex_kind_of_term term1 l1, flex_kind_of_term term2 l2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> @@ -382,6 +394,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) solve_simple_eqn (evar_conv_x ts) env evd (position_problem true pbty,ev1,t2) | None -> + if isLambda term2 then + eta env evd false term2 l2 term1 l1 + else (* Postpone the use of an heuristic *) add_conv_pb (pbty,env,applist appr1,applist appr2) evd, true) @@ -396,6 +411,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) solve_simple_eqn (evar_conv_x ts) env evd (position_problem false pbty,ev2,t1) | None -> + if isLambda term1 then + eta env evd true term1 l1 term2 l2 + else (* Postpone the use of an heuristic *) add_conv_pb (pbty,env,applist appr1,applist appr2) evd, true) @@ -408,7 +426,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) match eval_flexible_term ts env flex1 with | Some v1 -> evar_eqappr_x ts env i pbty (evar_apprec ts env i l1 v1) appr2 - | None -> (i,false) + | None -> + if isLambda term2 then + eta env i false term2 l2 term1 l1 + else + (i,false) in ise_try evd [f3; f4] @@ -420,28 +442,20 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) match eval_flexible_term ts env flex2 with | Some v2 -> evar_eqappr_x ts env i pbty appr1 (evar_apprec ts env i l2 v2) - | None -> (i,false) + | None -> + if isLambda term1 then + eta env i true term1 l1 term2 l2 + else + (i,false) in ise_try evd [f3; f4] (* Eta-expansion *) | Rigid c1, _ when isLambda c1 -> - assert (l1 = []); - let (na,c1,c'1) = destLambda c1 in - let c = nf_evar evd c1 in - let env' = push_rel (na,None,c) env in - let appr1 = evar_apprec ts env' evd [] c'1 in - let appr2 = (lift 1 term2, List.map (lift 1) l2 @ [mkRel 1]) in - evar_eqappr_x ts env' evd CONV appr1 appr2 + eta env evd true term1 l1 term2 l2 | _, Rigid c2 when isLambda c2 -> - assert (l2 = []); - let (na,c2,c'2) = destLambda c2 in - let c = nf_evar evd c2 in - let env' = push_rel (na,None,c) env in - let appr1 = (lift 1 term1, List.map (lift 1) l1 @ [mkRel 1]) in - let appr2 = evar_apprec ts env' evd [] c'2 in - evar_eqappr_x ts env' evd CONV appr1 appr2 + eta env evd false term2 l2 term1 l1 | Rigid c1, Rigid c2 -> begin match kind_of_term c1, kind_of_term c2 with @@ -582,15 +596,21 @@ let choose_less_dependent_instance evk evd term args = if subst' = [] then evd, false else Evd.define evk (mkVar (fst (List.hd subst'))) evd, true -let apply_on_subterm f c t = +let apply_on_subterm evdref f c t = let rec applyrec (k,c as kc) t = (* By using eq_constr, we make an approximation, for instance, we *) (* could also be interested in finding a term u convertible to t *) (* such that c occurs in u *) if eq_constr c t then f k else - map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c)) - applyrec kc t + match kind_of_term t with + | Evar (evk,args) when Evd.is_undefined !evdref evk -> + let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in + let g (_,b,_) a = if b = None then applyrec kc a else a in + mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args))) + | _ -> + map_constr_with_binders_left_to_right (fun d (k,c) -> (k+1,lift 1 c)) + applyrec kc t in applyrec (0,c) t @@ -598,7 +618,8 @@ let filter_possible_projections c ty ctxt args = let fv1 = free_rels c in let fv2 = collect_vars c in let tyvars = collect_vars ty in - List.map2 (fun (id,_,_) a -> + List.map2 (fun (id,b,_) a -> + b <> None || a == c || (* Here we make an approximation, for instance, we could also be *) (* interested in finding a term u convertible to c such that a occurs *) @@ -670,7 +691,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = evdref := evd; evsref := (fst (destEvar ev),evty)::!evsref; ev in - set_holes evdref (apply_on_subterm set_var c rhs) subst + set_holes evdref (apply_on_subterm evdref set_var c rhs) subst | [] -> rhs in let subst = make_subst (ctxt,args,argoccs) in diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 89ca95cb..d99b8c9f 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -178,12 +178,15 @@ let matches_core convert allow_partial_app allow_bound_rels pat c = | PApp (PApp (h, a1), a2), _ -> sorec stk subst (PApp(h,Array.append a1 a2)) t - | PApp (PMeta (Some n),args1), App (c2,args2) when allow_partial_app -> + | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app -> let p = Array.length args2 - Array.length args1 in if p>=0 then let args21, args22 = array_chop p args2 in let c = mkApp(c2,args21) in - let subst = merge_binding allow_bound_rels stk n c subst in + let subst = + match meta with + | None -> subst + | Some n -> merge_binding allow_bound_rels stk n c subst in array_fold_left2 (sorec stk) subst args1 args22 else raise PatternMatchingFailure diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 3b679fce..3f6acfcb 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -17,6 +17,19 @@ open Typeops open Declarations open Termops +let get_type_from_constraints env sigma t = + if isEvar (fst (decompose_app t)) then + match + list_map_filter (fun (pbty,env,t1,t2) -> + if is_fconv Reduction.CONV env sigma t t1 then Some t2 + else if is_fconv Reduction.CONV env sigma t t2 then Some t1 + else None) + (snd (Evd.extract_all_conv_pbs sigma)) + with + | t::l -> t + | _ -> raise Not_found + else raise Not_found + let rec subst_type env sigma typ = function | [] -> typ | h::rest -> @@ -58,7 +71,12 @@ let retype ?(polyprop=true) sigma = | Construct cstr -> type_of_constructor env cstr | Case (_,p,c,lf) -> let Inductiveops.IndType(_,realargs) = - try Inductiveops.find_rectype env sigma (type_of env c) + let t = type_of env c in + try Inductiveops.find_rectype env sigma t + with Not_found -> + try + let t = get_type_from_constraints env sigma t in + Inductiveops.find_rectype env sigma t with Not_found -> anomaly "type_of: Bad recursive type" in let t = whd_beta sigma (applist (p, realargs)) in (match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with diff --git a/pretyping/unification.ml b/pretyping/unification.ml index df5eff6a..fd045690 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -386,9 +386,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag | Meta k, _ when not (dependent cM cN) (* helps early trying alternatives *) -> if wt && flags.check_applied_meta_types then - (let tyM = Typing.meta_type sigma k in - let tyN = get_type_of curenv sigma cN in - check_compatibility curenv substn tyM tyN); + (try + let tyM = Typing.meta_type sigma k in + let tyN = get_type_of curenv sigma cN in + check_compatibility curenv substn tyM tyN + with Anomaly _ (* Hack *) -> + (* Renounce, maybe metas/evars prevents typing *) ()); (* Here we check that [cN] does not contain any local variables *) if nb = 0 then sigma,(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst @@ -400,9 +403,12 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag | _, Meta k when not (dependent cN cM) (* helps early trying alternatives *) -> if wt && flags.check_applied_meta_types then - (let tyM = get_type_of curenv sigma cM in - let tyN = Typing.meta_type sigma k in - check_compatibility curenv substn tyM tyN); + (try + let tyM = get_type_of curenv sigma cM in + let tyN = Typing.meta_type sigma k in + check_compatibility curenv substn tyM tyN + with Anomaly _ (* Hack *) -> + (* Renounce, maybe metas/evars prevents typing *) ()); (* Here we check that [cM] does not contain any local variables *) if nb = 0 then (sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst) diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index d5750cfa..9d1d081e 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -22,8 +22,10 @@ open Libobject open Summary (* call by value normalisation function using the virtual machine *) -let cbv_vm env _ c = - let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in +let cbv_vm env sigma c = + let ctyp = Retyping.get_type_of env sigma c in + if Termops.occur_meta_or_existential c then + error "vm_compute does not support existential variables."; Vnorm.cbv_vm env c ctyp diff --git a/scripts/coqc.ml b/scripts/coqc.ml index dbd73bbb..968bd0da 100644 --- a/scripts/coqc.ml +++ b/scripts/coqc.ml @@ -120,7 +120,7 @@ let parse_args () = parse (cfiles,args) rem | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () - | ("-outputstate"|"-inputstate"|"-is" + | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir" |"-load-vernac-source"|"-l"|"-load-vernac-object" |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib" as o) :: rem -> diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index d05ae680..3a980ef9 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -276,7 +276,7 @@ let make_hints g st only_classes sign = (PathEmpty, []) sign in Hint_db.add_list hintlist (Hint_db.empty st true) -let autogoal_hints_cache : (Environ.named_context_val * hint_db) option ref = ref None +let autogoal_hints_cache : (bool * Environ.named_context_val * hint_db) option ref = ref None let freeze () = !autogoal_hints_cache let unfreeze v = autogoal_hints_cache := v let init () = autogoal_hints_cache := None @@ -293,9 +293,11 @@ let make_autogoal_hints = fun only_classes ?(st=full_transparent_state) g -> let sign = pf_filtered_hyps g in match freeze () with - | Some (sign', hints) when Environ.eq_named_context_val sign sign' -> hints + | Some (onlyc, sign', hints) + when onlyc = only_classes && + Environ.eq_named_context_val sign sign' -> hints | _ -> let hints = make_hints g st only_classes (Environ.named_context_of_val sign) in - unfreeze (Some (sign, hints)); hints + unfreeze (Some (only_classes, sign, hints)); hints let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac = { skft = fun sk fk {it = gl,hints; sigma=s} -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 1c5e4b2f..0385063f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -236,15 +236,27 @@ let register_general_rewrite_clause = (:=) general_rewrite_clause let is_applied_rewrite_relation = ref (fun _ _ _ _ -> None) let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation +(* Do we have a JMeq instance on twice the same domains ? *) + +let jmeq_same_dom gl = function + | None -> true (* already checked in Hipattern.find_eq_data_decompose *) + | Some t -> + let rels, t = decompose_prod_assum t in + let env = Environ.push_rel_context rels (pf_env gl) in + match decompose_app t with + | _, [dom1; _; dom2;_] -> is_conv env (project gl) dom1 dom2 + | _ -> false + (* find_elim determines which elimination principle is necessary to eliminate lbeq on sort_of_gl. *) -let find_elim hdcncl lft2rgt dep cls args gl = - let inccl = (cls = None) in - if (eq_constr hdcncl (constr_of_reference (Coqlib.glob_eq)) || - eq_constr hdcncl (constr_of_reference (Coqlib.glob_jmeq)) && - pf_conv_x gl (List.nth args 0) (List.nth args 2)) && not dep - || Flags.version_less_or_equal Flags.V8_2 +let find_elim hdcncl lft2rgt dep cls ot gl = + let inccl = not (Option.has_some cls) in + let hdcncl_is u = eq_constr hdcncl (constr_of_reference u) in + if (hdcncl_is (Coqlib.glob_eq) || + hdcncl_is (Coqlib.glob_jmeq) && jmeq_same_dom gl ot) + && not dep + || Flags.version_less_or_equal Flags.V8_2 then match kind_of_term hdcncl with | Ind ind_sp -> @@ -295,7 +307,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars frze let isatomic = isProd (whd_zeta hdcncl) in let dep_fun = if isatomic then dependent else dependent_no_evar in let dep = dep_proof_ok && dep_fun c (type_of_clause gl cls) in - let elim = find_elim hdcncl lft2rgt dep cls (snd (decompose_app t)) gl in + let elim = find_elim hdcncl lft2rgt dep cls (Some t) gl in general_elim_clause with_evars frzevars tac cls sigma c t l (match lft2rgt with None -> false | Some b -> b) {elimindex = None; elimbody = (elim,NoBindings)} gl @@ -1208,7 +1220,7 @@ let swapEquandsInConcl gls = let bareRevSubstInConcl lbeq body (t,e1,e2) gls = (* find substitution scheme *) - let eq_elim = find_elim lbeq.eq (Some false) false None [e1;e2] gls in + let eq_elim = find_elim lbeq.eq (Some false) false None None gls in (* build substitution predicate *) let p = lambda_create (pf_env gls) (t,body) in (* apply substitution scheme *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 7479ee9a..c2eaa327 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -227,7 +227,7 @@ let add_tactic s t = let overwriting_add_tactic s t = if Hashtbl.mem tac_tab s then begin Hashtbl.remove tac_tab s; - warning ("Overwriting definition of tactic "^s) + msg_warn ("Overwriting definition of tactic "^s) end; Hashtbl.add tac_tab s t @@ -265,7 +265,7 @@ let lookup_genarg id = try Gmap.find id !extragenargtab with Not_found -> let msg = "No interpretation function found for entry " ^ id in - warning msg; + msg_warn msg; let f = (fun _ _ -> failwith msg), (fun _ _ _ -> failwith msg), (fun _ a -> a) in add_interp_genarg id f; f diff --git a/test-suite/Makefile b/test-suite/Makefile index cd5886f8..ae1562c7 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -46,6 +46,7 @@ SHOW := $(if $(VERBOSE),@true,@echo) HIDE := $(if $(VERBOSE),,@) REDIR := $(if $(VERBOSE),,> /dev/null 2>&1) +bogomips := ifneq (,$(wildcard /proc/cpuinfo)) sedbogo := -e "s/bogomips.*: \([0-9]*\).*/\1/p" # i386, ppc sedbogo += -e "s/Cpu0Bogo.*: \([0-9]*\).*/\1/p" # sparc diff --git a/test-suite/bugs/closed/3003.v b/test-suite/bugs/closed/3003.v new file mode 100644 index 00000000..2f8bcdae --- /dev/null +++ b/test-suite/bugs/closed/3003.v @@ -0,0 +1,12 @@ +(* This used to raise an anomaly in 8.4 and trunk up to 17 April 2013 *) + +Set Implicit Arguments. + +Inductive path (V : Type) (E : V -> V -> Type) (s : V) : V -> Type := + | NoEdges : path E s s + | AddEdge : forall d d' : V, path E s d -> E d d' -> path E s d'. +Inductive G_Vertex := G_v0 | G_v1. +Inductive G_Edge : G_Vertex -> G_Vertex -> Set := G_e : G_Edge G_v0 G_v1. +Goal forall x1 : G_Edge G_v1 G_v1, @AddEdge _ G_Edge G_v1 _ _ (NoEdges _ _) x1 = NoEdges _ _. +intro x1. +try destruct x1. (* now raises a typing error *) diff --git a/test-suite/bugs/closed/3023.v b/test-suite/bugs/closed/3023.v new file mode 100644 index 00000000..ed489511 --- /dev/null +++ b/test-suite/bugs/closed/3023.v @@ -0,0 +1,31 @@ +(* Checking use of eta on Flexible/Rigid and SemiFlexible/Rigid unif problems *) + +Set Implicit Arguments. +Generalizable All Variables. + +Record Category {obj : Type} := + { + Morphism : obj -> obj -> Type; + + Identity : forall x, Morphism x x; + Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'; + LeftIdentity : forall a b (f : Morphism a b), Compose (Identity b) f = f + }. + + +Section DiscreteAdjoints. + Let C := {| + Morphism := (fun X Y : Type => X -> Y); + Identity := (fun X : Type => (fun x : X => x)); + Compose := (fun _ _ _ f g => (fun x => f (g x))); + LeftIdentity := (fun X Y p => @eq_refl _ p : (fun x : X => p x) = p) + |}. + Variable ObjectFunctor : C = C. + + Goal True. + Proof. + subst C. + revert ObjectFunctor. + intro ObjectFunctor. + simpl in ObjectFunctor. + revert ObjectFunctor. (* Used to failed in 8.4 up to 16 April 2013 *) diff --git a/test-suite/bugs/closed/shouldsucceed/2230.v b/test-suite/bugs/closed/shouldsucceed/2230.v new file mode 100644 index 00000000..5076fb2b --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2230.v @@ -0,0 +1,6 @@ +Goal forall f, f 1 1 -> True. +intros. +match goal with + | [ H : _ ?a |- _ ] => idtac +end. +Abort. diff --git a/test-suite/bugs/closed/shouldsucceed/2837.v b/test-suite/bugs/closed/shouldsucceed/2837.v new file mode 100644 index 00000000..5d984463 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2837.v @@ -0,0 +1,15 @@ +Require Import JMeq. + +Axiom test : forall n m : nat, JMeq n m. + +Goal forall n m : nat, JMeq n m. + +(* I) with no intros nor variable hints, this should produce a regular error + instead of Uncaught exception Failure("nth"). *) +Fail rewrite test. + +(* II) with intros but indication of variables, still an error *) +Fail (intros; rewrite test). + +(* III) a working variant: *) +intros; rewrite (test n m).
\ No newline at end of file diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index e443115c..17c80d13 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,7 +1,9 @@ The command has indeed failed with message: => Error: To rename arguments the "rename" flag must be specified. +Argument A renamed to B. The command has indeed failed with message: => Error: To rename arguments the "rename" flag must be specified. +Argument A renamed to T. @eq_refl : forall (B : Type) (y : B), y = y eq_refl @@ -106,3 +108,6 @@ The command has indeed failed with message: => Error: Argument z cannot be declared implicit. The command has indeed failed with message: => Error: Extra argument y. +The command has indeed failed with message: +=> Error: To rename arguments the "rename" flag must be specified. +Argument A renamed to R. diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v index b133e733..e68fbd69 100644 --- a/test-suite/output/Arguments_renaming.v +++ b/test-suite/output/Arguments_renaming.v @@ -50,5 +50,5 @@ Fail Arguments eq_refl {F}, [F]. Fail Arguments eq_refl {F F}, [F] F. Fail Arguments eq {F} x [z]. Fail Arguments eq {F} x z y. - +Fail Arguments eq {R} s t. diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v index 9a6ed71a..c29e5297 100644 --- a/test-suite/success/Case19.v +++ b/test-suite/success/Case19.v @@ -6,3 +6,14 @@ Variable T : Type. Variable x : nat*nat. Check let (_, _) := x in sigT (fun _ : T => nat). + +(* This used to raise an anomaly in V8.4, up to pl2 *) + +Goal {x: nat & x=x}. +Fail exists (fun x => + match + projT2 (projT2 x) as e in (_ = y) + return _ = existT _ (projT1 x) (existT _ y e) + with + | eq_refl => eq_refl + end). diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v index 89d3eebc..dc18496f 100644 --- a/theories/Logic/ConstructiveEpsilon.v +++ b/theories/Logic/ConstructiveEpsilon.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ConstructiveEpsilon.v 15714 2012-08-08 18:54:37Z herbelin $ i*) +(*i $Id: ConstructiveEpsilon.v 12112 2009-04-28 15:47:34Z herbelin $ i*) (** This provides with a proof of the constructive form of definite and indefinite descriptions for Sigma^0_1-formulas (hereafter called diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 90cdd12d..8a5f0695 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -157,9 +157,10 @@ let declare_dependencies () = (List.rev !vAccu) let usage () = - eprintf - "[ usage: coqdep [-w] [-I dir] [-R dir coqdir] [-coqlib dir] [-c] [-i] [-D] <filename>+ ]\n"; - flush stderr; + eprintf " usage: coqdep [-w] [-c] [-D] [-I dir] [-R dir coqdir] <filename>+\n"; + eprintf " extra options:\n"; + eprintf " -coqlib dir : set the coq standard library directory\n"; + eprintf " -exclude-dir f : skip subdirectories named f during -R search\n"; exit 1 let rec parse = function @@ -177,9 +178,11 @@ let rec parse = function | "-R" :: r :: "-as" :: [] -> usage () | "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll | "-R" :: ([] | [_]) -> usage () - | "-coqlib" :: (r :: ll) -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll + | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll + | "-exclude-dir" :: [] -> usage () + | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll | "-coqlib" :: [] -> usage () - | "-suffix" :: (s :: ll) -> suffixe := s ; parse ll + | "-suffix" :: s :: ll -> suffixe := s ; parse ll | "-suffix" :: [] -> usage () | "-slash" :: ll -> option_slash := true; parse ll | ("-h"|"--help"|"-help") :: _ -> usage () diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 19aba41d..15fcdc60 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -26,7 +26,7 @@ let rec parse = function (* To solve conflict (e.g. same filename in kernel and checker) we allow to state an explicit order *) add_dir add_known r []; - norecdir_list:=r::!norecdir_list; + norec_dirs:=r::!norec_dirs; parse ll | f :: ll -> treat_file None f; parse ll | [] -> () diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 4977a94c..2b316b0c 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -26,7 +26,8 @@ let option_slash = ref false let option_natdynlk = ref true let option_mldep = ref None -let norecdir_list = ref ([]:string list) +let norec_dirs = ref ([] : string list) +let norec_dirnames = ref ["CVS"; "_darcs"] let suffixe = ref ".vo" @@ -439,14 +440,17 @@ let rec add_directory recur add_file phys_dir log_dir = try while true do let f = readdir dirh in - (* we avoid . .. and all hidden files and subdirs (e.g. .svn, _darcs) *) - if f.[0] <> '.' && f.[0] <> '_' then + (* we avoid all files and subdirs starting by '.' (e.g. .svn), + plus CVS and _darcs and any subdirs given via -exclude-dirs *) + if f.[0] <> '.' then let phys_f = if phys_dir = "." then f else phys_dir//f in match try (stat phys_f).st_kind with _ -> S_BLK with | S_DIR when recur -> - if List.mem phys_f !norecdir_list then () - else - add_directory recur add_file phys_f (log_dir@[f]) + if List.mem f !norec_dirnames then () + else + if List.mem phys_f !norec_dirs then () + else + add_directory recur add_file phys_f (log_dir@[f]) | S_REG -> add_file phys_dir log_dir f | _ -> () done diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli index afc171cb..d9ca3ca8 100644 --- a/tools/coqdep_common.mli +++ b/tools/coqdep_common.mli @@ -11,7 +11,8 @@ val option_noglob : bool ref val option_slash : bool ref val option_natdynlk : bool ref val option_mldep : string option ref -val norecdir_list : string list ref +val norec_dirs : string list ref +val norec_dirnames : string list ref val suffixe : string ref type dir = string option val ( // ) : string -> string -> string diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml index 22a36ede..7b688212 100644 --- a/tools/fake_ide.ml +++ b/tools/fake_ide.ml @@ -26,15 +26,15 @@ let eval_call (call:'a Ide_intf.call) = match res with Interface.Fail _ -> exit 1 | _ -> () let commands = - [ "INTERPRAWSILENT", (fun s -> eval_call (Ide_intf.interp (true,false,s))); - "INTERPRAW", (fun s -> eval_call (Ide_intf.interp (true,true,s))); - "INTERPSILENT", (fun s -> eval_call (Ide_intf.interp (false,false,s))); - "INTERP", (fun s -> eval_call (Ide_intf.interp (false,true,s))); + [ "INTERPRAWSILENT", (fun s -> eval_call (Ide_intf.interp (0,true,false,s))); + "INTERPRAW", (fun s -> eval_call (Ide_intf.interp (0,true,true,s))); + "INTERPSILENT", (fun s -> eval_call (Ide_intf.interp (0,false,false,s))); + "INTERP", (fun s -> eval_call (Ide_intf.interp (0,false,true,s))); "REWIND", (fun s -> eval_call (Ide_intf.rewind (int_of_string s))); - "GOALS", (fun _ -> eval_call Ide_intf.goals); - "HINTS", (fun _ -> eval_call Ide_intf.hints); - "GETOPTIONS", (fun _ -> eval_call Ide_intf.get_options); - "STATUS", (fun _ -> eval_call Ide_intf.status); + "GOALS", (fun _ -> eval_call (Ide_intf.goals ())); + "HINTS", (fun _ -> eval_call (Ide_intf.hints ())); + "GETOPTIONS", (fun _ -> eval_call (Ide_intf.get_options ())); + "STATUS", (fun _ -> eval_call (Ide_intf.status ())); "INLOADPATH", (fun s -> eval_call (Ide_intf.inloadpath s)); "MKCASES", (fun s -> eval_call (Ide_intf.mkcases s)); "#", (fun _ -> raise Comment); diff --git a/toplevel/class.ml b/toplevel/class.ml index 52d507a1..7e7dfd17 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -255,7 +255,7 @@ let add_new_coercion_core coef stre source target isid = in check_source (Some cls); if not (uniform_cond (llp-ind) lvs) then - warning (Pp.string_of_ppcmds (explain_coercion_error coef NotUniform)); + msg_warn (Pp.string_of_ppcmds (explain_coercion_error coef NotUniform)); let clt = try get_target tg ind diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 8f954573..85c2ca6e 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -140,6 +140,6 @@ let get_compat_version = function | "8.3" -> Flags.V8_3 | "8.2" -> Flags.V8_2 | ("8.1" | "8.0") as s -> - warning ("Compatibility with version "^s^" not supported."); + msg_warn ("Compatibility with version "^s^" not supported."); Flags.V8_2 | s -> Util.error ("Unknown compatibility version \""^s^"\".") diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index f550df16..2ef8bd2b 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -851,8 +851,8 @@ let error_same_names_overlap idl = str "names:" ++ spc () ++ prlist_with_sep pr_comma pr_id idl ++ str "." -let error_not_an_arity id = - str "The type of" ++ spc () ++ pr_id id ++ spc () ++ str "is not an arity." +let error_not_an_arity env c = + str "The type" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ str "is not an arity." let error_bad_entry () = str "Bad inductive definition." @@ -888,7 +888,7 @@ let explain_inductive_error = function | SameNamesTypes id -> error_same_names_types id | SameNamesConstructors id -> error_same_names_constructors id | SameNamesOverlap idl -> error_same_names_overlap idl - | NotAnArity id -> error_not_an_arity id + | NotAnArity (env, c) -> error_not_an_arity env c | BadEntry -> error_bad_entry () | LargeNonPropInductiveNotInType -> error_large_non_prop_inductive_not_in_type () diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml index 6937eeb8..46b75339 100644 --- a/toplevel/ide_intf.ml +++ b/toplevel/ide_intf.ml @@ -10,7 +10,7 @@ (** WARNING: TO BE UPDATED WHEN MODIFIED! *) -let protocol_version = "20120710" +let protocol_version = "20130425~2" (** * Interface of calls to Coq by CoqIde *) @@ -22,76 +22,143 @@ type xml = Xml_parser.xml (** We use phantom types and GADT to protect ourselves against wild casts *) type 'a call = - | Interp of raw * verbose * string - | Rewind of int - | Goal - | Evars - | Hints - | Status - | Search of search_flags - | GetOptions - | SetOptions of (option_name * option_value) list - | InLoadPath of string - | MkCases of string - | Quit - | About - -(** The structure that coqtop should implement *) - -type handler = { - interp : raw * verbose * string -> string; - rewind : int -> int; - goals : unit -> goals option; - evars : unit -> evar list option; - hints : unit -> (hint list * hint) option; - status : unit -> status; - search : search_flags -> string coq_object list; - get_options : unit -> (option_name * option_state) list; - set_options : (option_name * option_value) list -> unit; - inloadpath : string -> bool; - mkcases : string -> string list list; - quit : unit -> unit; - about : unit -> coq_info; - handle_exn : exn -> location * string; -} + | Interp of interp_sty + | Rewind of rewind_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 + | InLoadPath of inloadpath_sty + | MkCases of mkcases_sty + | Quit of quit_sty + | About of about_sty + +type unknown (** The actual calls *) -let interp (r,b,s) : string call = Interp (r,b,s) -let rewind i : int call = Rewind i -let goals : goals option call = Goal -let evars : evar list option call = Evars -let hints : (hint list * hint) option call = Hints -let status : status call = Status -let search flags : string coq_object list call = Search flags -let get_options : (option_name * option_state) list call = GetOptions -let set_options l : unit call = SetOptions l -let inloadpath s : bool call = InLoadPath s -let mkcases s : string list list call = MkCases s -let quit : unit call = Quit +let interp x : interp_rty call = Interp x +let rewind x : rewind_rty call = Rewind 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 inloadpath x : inloadpath_rty call = InLoadPath 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 (** * Coq answers to CoqIde *) -let abstract_eval_call handler c = +let abstract_eval_call handler (c : 'a call) = + let mkGood x : 'a value = Good (Obj.magic x) in try - let res = match c with - | Interp (r,b,s) -> Obj.magic (handler.interp (r,b,s) : string) - | Rewind i -> Obj.magic (handler.rewind i : int) - | Goal -> Obj.magic (handler.goals () : goals option) - | Evars -> Obj.magic (handler.evars () : evar list option) - | Hints -> Obj.magic (handler.hints () : (hint list * hint) option) - | Status -> Obj.magic (handler.status () : status) - | Search flags -> Obj.magic (handler.search flags : string coq_object list) - | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list) - | SetOptions opts -> Obj.magic (handler.set_options opts : unit) - | InLoadPath s -> Obj.magic (handler.inloadpath s : bool) - | MkCases s -> Obj.magic (handler.mkcases s : string list list) - | Quit -> Obj.magic (handler.quit () : unit) - | About -> Obj.magic (handler.about () : coq_info) - in Good res + match c with + | Interp x -> mkGood (handler.interp x) + | Rewind x -> mkGood (handler.rewind 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) + | InLoadPath x -> mkGood (handler.inloadpath x) + | MkCases x -> mkGood (handler.mkcases x) + | Quit x -> mkGood (handler.quit x) + | About x -> mkGood (handler.about x) with any -> - let (l, str) = handler.handle_exn any in - Fail (l,str) + Fail (handler.handle_exn any) + +(* To read and typecheck the answers we give a description of the types, + and a way to statically check that the reified version is in sync *) +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 goals_t : goals val_t + val evar_t : evar val_t + val state_t : status val_t + val coq_info_t : coq_info val_t + val option_state_t : option_state val_t + val option_t : 'a val_t -> 'a option val_t + val list_t : 'a val_t -> 'a list val_t + val coq_object_t : 'a val_t -> 'a coq_object 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) Util.union val_t + + type value_type = private + | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info + | Option of value_type + | List of value_type + | Coq_object of value_type + | Pair of value_type * value_type + | Union of value_type * value_type + + val check : 'a val_t -> value_type + +end = struct + + type value_type = + | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info + | Option of value_type + | List of value_type + | Coq_object of value_type + | Pair of value_type * value_type + | Union of value_type * value_type + + type 'a val_t = value_type + let check x = x + + let unit_t = Unit + let string_t = String + let int_t = Int + let bool_t = Bool + let goals_t = Goals + let evar_t = Evar + let state_t = State + let coq_info_t = Coq_info + let option_state_t = Option_state + let option_t x = Option x + let list_t x = List x + let coq_object_t x = Coq_object x + let pair_t x y = Pair (x, y) + let union_t x y = Union (x, y) + +end + +open ReifType + +(* For every (call : 'a call), we build the reification of 'a. + * In OCaml 4 we could use GATDs to do that I guess *) +let expected_answer_type call : value_type = + let hint = list_t (pair_t string_t string_t) in + let hints = pair_t (list_t hint) hint in + let options = pair_t (list_t string_t) option_state_t in + let objs = coq_object_t string_t in + match call with + | Interp _ -> check (string_t : interp_rty val_t) + | Rewind _ -> check (int_t : rewind_rty val_t) + | Goal _ -> check (option_t goals_t : goals_rty val_t) + | Evars _ -> check (option_t (list_t evar_t) : evars_rty val_t) + | Hints _ -> check (option_t hints : hints_rty val_t) + | Status _ -> check (state_t : status_rty val_t) + | Search _ -> check (list_t objs : search_rty val_t) + | GetOptions _ -> check (list_t options : get_options_rty val_t) + | SetOptions _ -> check (unit_t : set_options_rty val_t) + | InLoadPath _ -> check (bool_t : inloadpath_rty val_t) + | MkCases _ -> check (list_t (list_t string_t) : mkcases_rty val_t) + | Quit _ -> check (unit_t : quit_rty val_t) + | About _ -> check (coq_info_t : about_rty val_t) (** * XML data marshalling *) @@ -113,10 +180,6 @@ let do_match constr t mf = match constr with else raise Marshal_error | _ -> raise Marshal_error -let pcdata = function -| PCData s -> s -| _ -> raise Marshal_error - let singleton = function | [x] -> x | _ -> raise Marshal_error @@ -132,56 +195,68 @@ let bool_arg tag b = if b then [tag, ""] else [] let of_unit () = Element ("unit", [], []) -let to_unit = function +let to_unit : xml -> unit = function | Element ("unit", [], []) -> () | _ -> raise Marshal_error -let of_bool b = +let of_bool (b : bool) : xml = if b then constructor "bool" "true" [] else constructor "bool" "false" [] -let to_bool xml = do_match xml "bool" +let to_bool xml : bool = do_match xml "bool" (fun s _ -> match s with | "true" -> true | "false" -> false | _ -> raise Marshal_error) -let of_list f l = +let of_list (f : 'a -> xml) (l : 'a list) = Element ("list", [], List.map f l) -let to_list f = function +let to_list (f : xml -> 'a) : xml -> 'a list = function | Element ("list", [], l) -> List.map f l | _ -> raise Marshal_error -let of_option f = function +let of_option (f : 'a -> xml) : 'a option -> xml = function | None -> Element ("option", ["val", "none"], []) | Some x -> Element ("option", ["val", "some"], [f x]) -let to_option f = function +let to_option (f : xml -> 'a) : xml -> 'a option = function | Element ("option", ["val", "none"], []) -> None | Element ("option", ["val", "some"], [x]) -> Some (f x) | _ -> raise Marshal_error -let of_string s = Element ("string", [], [PCData s]) +let of_string (s : string) : xml = Element ("string", [], [PCData s]) -let to_string = function +let to_string : xml -> string = function | Element ("string", [], l) -> raw_string l | _ -> raise Marshal_error -let of_int i = Element ("int", [], [PCData (string_of_int i)]) +let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)]) -let to_int = function +let to_int : xml -> int = function | Element ("int", [], [PCData s]) -> (try int_of_string s with Failure _ -> raise Marshal_error) | _ -> raise Marshal_error -let of_pair f g (x, y) = Element ("pair", [], [f x; g y]) +let of_pair (f : 'a -> xml) (g : 'b -> xml) : 'a * 'b -> xml = + function (x,y) -> Element ("pair", [], [f x; g y]) -let to_pair f g = function +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) Util.union -> xml = +function +| Util.Inl x -> Element ("union", ["val","in_l"], [f x]) +| Util.Inr x -> Element ("union", ["val","in_r"], [g x]) + +let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) Util.union= +function +| Element ("union", ["val","in_l"], [x]) -> Util.Inl (f x) +| Element ("union", ["val","in_r"], [x]) -> Util.Inr (g x) +| _ -> raise Marshal_error + (** More elaborate types *) let of_option_value = function @@ -275,7 +350,7 @@ let to_value f = function let loc_s = int_of_string (List.assoc "loc_s" attrs) in let loc_e = int_of_string (List.assoc "loc_e" attrs) in Some (loc_s, loc_e) - with e when e <> Sys.Break -> None + with Not_found | Failure _ -> None in let msg = raw_string l in Fail (loc, msg) @@ -283,23 +358,24 @@ let to_value f = function | _ -> raise Marshal_error let of_call = function -| Interp (raw, vrb, cmd) -> +| Interp (id,raw, vrb, cmd) -> let flags = (bool_arg "raw" raw) @ (bool_arg "verbose" vrb) in - Element ("call", ("val", "interp") :: flags, [PCData cmd]) + Element ("call", ("val", "interp") :: ("id", string_of_int id) :: flags, + [PCData cmd]) | Rewind n -> Element ("call", ("val", "rewind") :: ["steps", string_of_int n], []) -| Goal -> +| Goal () -> Element ("call", ["val", "goal"], []) -| Evars -> +| Evars () -> Element ("call", ["val", "evars"], []) -| Hints -> +| Hints () -> Element ("call", ["val", "hints"], []) -| Status -> +| Status () -> Element ("call", ["val", "status"], []) | Search flags -> let args = List.map (of_pair of_search_constraint of_bool) flags in Element ("call", ["val", "search"], args) -| GetOptions -> +| GetOptions () -> Element ("call", ["val", "getoptions"], []) | SetOptions opts -> let args = List.map (of_pair (of_list of_string) of_option_value) opts in @@ -308,37 +384,40 @@ let of_call = function Element ("call", ["val", "inloadpath"], [PCData file]) | MkCases ind -> Element ("call", ["val", "mkcases"], [PCData ind]) -| Quit -> +| Quit () -> Element ("call", ["val", "quit"], []) -| About -> +| About () -> Element ("call", ["val", "about"], []) let to_call = function | Element ("call", attrs, l) -> let ans = massoc "val" attrs in begin match ans with - | "interp" -> - let raw = List.mem_assoc "raw" attrs in - let vrb = List.mem_assoc "verbose" attrs in - Interp (raw, vrb, raw_string l) + | "interp" -> begin + try + let id = List.assoc "id" attrs in + let raw = List.mem_assoc "raw" attrs in + let vrb = List.mem_assoc "verbose" attrs in + Interp (int_of_string id, raw, vrb, raw_string l) + with Not_found -> raise Marshal_error end | "rewind" -> let steps = int_of_string (massoc "steps" attrs) in Rewind steps - | "goal" -> Goal - | "evars" -> Evars - | "status" -> Status + | "goal" -> Goal () + | "evars" -> Evars () + | "status" -> Status () | "search" -> let args = List.map (to_pair to_search_constraint to_bool) l in Search args - | "getoptions" -> GetOptions + | "getoptions" -> GetOptions () | "setoptions" -> let args = List.map (to_pair (to_list to_string) to_option_value) l in SetOptions args | "inloadpath" -> InLoadPath (raw_string l) | "mkcases" -> MkCases (raw_string l) - | "hints" -> Hints - | "quit" -> Quit - | "about" -> About + | "hints" -> Hints () + | "quit" -> Quit () + | "about" -> About () | _ -> raise Marshal_error end | _ -> raise Marshal_error @@ -419,181 +498,216 @@ let to_coq_info = function } | _ -> 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 xml = do_match xml "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 in + Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[]) + +let to_loc xml = match xml with +| Element ("loc", l,[]) -> + (try + let start = List.assoc "start" l in + let stop = List.assoc "stop" l in + (int_of_string start, int_of_string stop) + with Not_found | Invalid_argument _ -> raise Marshal_error) +| _ -> raise Marshal_error + +let to_feedback_content xml = do_match xml "feedback_content" + (fun s args -> match s with + | "addedaxiom" -> AddedAxiom + | "processed" -> Processed + | "globref" -> + (match args with + | [loc; filepath; modpath; ident; ty] -> + GlobRef(to_loc loc, to_string filepath, to_string modpath, + to_string ident, to_string ty) + | _ -> raise Marshal_error) + | _ -> raise Marshal_error) + +let of_feedback_content = function +| AddedAxiom -> constructor "feedback_content" "addedaxiom" [] +| Processed -> constructor "feedback_content" "processed" [] +| 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 + ] + +let of_feedback msg = + let content = of_feedback_content msg.content in + Element ("feedback", ["id",string_of_int msg.edit_id], [content]) + +let to_feedback xml = match xml with +| Element ("feedback", ["id",id], [content]) -> + { edit_id = int_of_string id; + content = to_feedback_content content } +| _ -> raise Marshal_error + +let is_feedback = function +| Element ("feedback", _, _) -> true +| _ -> false + (** Conversions between ['a value] and xml answers When decoding an xml answer, we dynamically check that it is compatible with the original call. For that we now rely on the fact that all sub-fonctions [to_xxx : xml -> xxx] check that the current xml element - is "xxx", and raise [Marshal_error] if anything goes wrong. -*) - -type value_type = - | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info - | Option of value_type - | List of value_type - | Coq_object of value_type - | Pair of value_type * value_type - -let hint = List (Pair (String, String)) -let option_name = List String - -let expected_answer_type = function - | Interp _ -> String - | Rewind _ -> Int - | Goal -> Option Goals - | Evars -> Option (List Evar) - | Hints -> Option (Pair (List hint, hint)) - | Status -> State - | Search _ -> List (Coq_object String) - | GetOptions -> List (Pair (option_name, Option_state)) - | SetOptions _ -> Unit - | InLoadPath _ -> Bool - | MkCases _ -> List (List String) - | Quit -> Unit - | About -> Coq_info + is "xxx", and raise [Marshal_error] if anything goes wrong. *) let of_answer (q : 'a call) (r : 'a value) : 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 - | 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)) + | 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 + | 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)) in of_value (convert (expected_answer_type q)) r let to_answer xml (c : 'a call) : 'a value = 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 - | 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)) + | 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 + | 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)) in to_value (convert (expected_answer_type c)) xml (** * Debug printing *) +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 rec pr_setoptions opts = - let map (key, v) = - let key = String.concat " " key in - key ^ " := " ^ (pr_option_value v) - in - String.concat "; " (List.map map opts) - -let pr_getoptions opts = - let map (key, s) = - let key = String.concat " " key in - Printf.sprintf "%s: sync := %b; depr := %b; name := %s; value := %s\n" - key s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value) - in - "\n" ^ String.concat "" (List.map map opts) + | 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 Util.Inl x -> pr1 x | Util.Inr x -> pr2 x let pr_call = function - | Interp (r,b,s) -> + | Interp (id,r,b,s) -> let raw = if r then "RAW" else "" in let verb = if b then "" else "SILENT" in - "INTERP"^raw^verb^" ["^s^"]" + "INTERP"^raw^verb^" "^string_of_int id^" ["^s^"]" | Rewind i -> "REWIND "^(string_of_int i) - | Goal -> "GOALS" - | Evars -> "EVARS" - | Hints -> "HINTS" - | Status -> "STATUS" + | Goal _ -> "GOALS" + | Evars _ -> "EVARS" + | Hints _ -> "HINTS" + | Status _ -> "STATUS" | Search _ -> "SEARCH" - | GetOptions -> "GETOPTIONS" - | SetOptions l -> "SETOPTIONS" ^ " [" ^ pr_setoptions l ^ "]" + | GetOptions _ -> "GETOPTIONS" + | SetOptions l -> "SETOPTIONS" ^ " [" ^ + String.concat ";" + (List.map (pr_pair (pr_list pr_string) pr_option_value) l) ^ "]" | InLoadPath s -> "INLOADPATH "^s | MkCases s -> "MKCASES "^s - | Quit -> "QUIT" - | About -> "ABOUT" - + | Quit _ -> "QUIT" + | About _ -> "ABOUT" let pr_value_gen pr = function | Good v -> "GOOD " ^ pr v | Fail (_,str) -> "FAIL ["^str^"]" - -let pr_value v = pr_value_gen (fun _ -> "") v - -let pr_string s = "["^s^"]" -let pr_bool b = if b then "true" else "false" - -let pr_status s = - 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_mkcases l = - let l = List.map (String.concat " ") l in - "[" ^ String.concat " | " l ^ "]" - -let pr_goals_aux g = - 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_goals = function -| None -> "No proof in progress." -| Some g -> pr_goals_aux g - -let pr_evar ev = "[" ^ ev.evar_info ^ "]" - -let pr_evars = function -| None -> "No proof in progress." -| Some evars -> String.concat " " (List.map pr_evar evars) - +let pr_value v = pr_value_gen (fun _ -> "FIXME") v let pr_full_value call value = - match call with - | Interp _ -> pr_value_gen pr_string (Obj.magic value : string value) - | Rewind i -> pr_value_gen string_of_int (Obj.magic value : int value) - | Goal -> pr_value_gen pr_goals (Obj.magic value : goals option value) - | Evars -> pr_value_gen pr_evars (Obj.magic value : evar list option value) - | Hints -> pr_value value - | Status -> pr_value_gen pr_status (Obj.magic value : status value) - | Search _ -> pr_value value - | GetOptions -> pr_value_gen pr_getoptions (Obj.magic value : (option_name * option_state) list value) - | SetOptions _ -> pr_value value - | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value) - | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value) - | Quit -> pr_value value - | About -> pr_value value - + let rec pr = 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 + | Coq_info -> Obj.magic pr_coq_info + | Goals -> Obj.magic pr_goal + | Evar -> Obj.magic pr_evar + | List t -> Obj.magic (pr_list (pr t)) + | Option t -> Obj.magic (pr_option (pr t)) + | Coq_object t -> Obj.magic pr_coq_object + | Pair (t1,t2) -> Obj.magic (pr_pair (pr t1) (pr t2)) + | Union (t1,t2) -> Obj.magic (pr_union (pr t1) (pr t2)) + in + pr_value_gen (pr (expected_answer_type call)) value diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli index 7d0685b1..aa3f91bf 100644 --- a/toplevel/ide_intf.mli +++ b/toplevel/ide_intf.mli @@ -14,78 +14,20 @@ type xml = Xml_parser.xml type 'a call -(** Running a command (given as a string). - - The 1st flag indicates whether to use "raw" mode - (less sanity checks, no impact on the undo stack). - Suitable e.g. for queries, or for the Set/Unset - of display options that coqide performs all the time. - - The 2nd flag controls the verbosity. - - The returned string contains the messages produced - by this command, but not the updated goals (they are - to be fetch by a separated [current_goals]). *) -val interp : raw * verbose * string -> string call - -(** Backtracking by at least a certain number of phrases. - No finished proofs will be re-opened. Instead, - we continue backtracking until before these proofs, - and answer the amount of extra backtracking performed. - Backtracking by more than the number of phrases already - interpreted successfully (and not yet undone) will fail. *) -val rewind : int -> int call - -(** Fetching the list of current goals. Return [None] if no proof is in - progress, [Some gl] otherwise. *) -val goals : goals option call - -(** Retrieving the tactics applicable to the current goal. [None] if there is - no proof in progress. *) -val hints : (hint list * hint) option call - -(** The status, for instance "Ready in SomeSection, proving Foo" *) -val status : status call - -(** Is a directory part of Coq's loadpath ? *) -val inloadpath : string -> bool call - -(** Create a "match" template for a given inductive type. - For each branch of the match, we list the constructor name - followed by enough pattern variables. *) -val mkcases : string -> string list list call - -(** Retrieve the list of unintantiated evars in the current proof. [None] if no - proof is in progress. *) -val evars : evar list option call - -(** Retrieve the list of options of the current toplevel, together with their - state. *) -val get_options : (option_name * option_state) list call - -(** Set the options to the given value. Warning: this is not atomic, so whenever - the call fails, the option state can be messed up... This is the caller duty - to check that everything is correct. *) -val set_options : (option_name * option_value) list -> unit call - -(** Quit gracefully the interpreter. *) -val quit : unit call - -(** The structure that coqtop should implement *) - -type handler = { - interp : raw * verbose * string -> string; - rewind : int -> int; - goals : unit -> goals option; - evars : unit -> evar list option; - hints : unit -> (hint list * hint) option; - status : unit -> status; - search : search_flags -> string coq_object list; - get_options : unit -> (option_name * option_state) list; - set_options : (option_name * option_value) list -> unit; - inloadpath : string -> bool; - mkcases : string -> string list list; - quit : unit -> unit; - about : unit -> coq_info; - handle_exn : exn -> location * string; -} +type unknown + +val interp : interp_sty -> interp_rty call +val rewind : rewind_sty -> rewind_rty call +val goals : goals_sty -> goals_rty call +val hints : hints_sty -> hints_rty call +val status : status_sty -> status_rty call +val inloadpath : inloadpath_sty -> inloadpath_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 abstract_eval_call : handler -> 'a call -> 'a value @@ -97,11 +39,18 @@ val protocol_version : string 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_value : ('a -> xml) -> 'a value -> xml -val to_value : (xml -> 'a) -> xml -> 'a value -val of_call : 'a call -> xml -val to_call : xml -> 'a call +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 : xml -> 'a call -> 'a value diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 6e9a0ee0..019f8a69 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -112,7 +112,7 @@ let coqide_cmd_checks (loc,ast) = (** Interpretation (cf. [Ide_intf.interp]) *) -let interp (raw,verbosely,s) = +let interp (id,raw,verbosely,s) = let pa = Pcoq.Gram.parsable (Stream.of_string s) in let loc_ast = Vernac.parse_sentence (pa,None) in if not raw then coqide_cmd_checks loc_ast; @@ -371,7 +371,7 @@ let eval_call c = (* Here we do send an acknowledgement message to prove everything went OK. *) let dummy = Interface.Good () in - let xml_answer = Ide_intf.of_answer Ide_intf.quit dummy in + let xml_answer = Ide_intf.of_answer (Ide_intf.quit ()) dummy in let () = Xml_utils.print_xml !orig_stdout xml_answer in let () = flush !orig_stdout in let () = pr_debug "Exiting gracefully." in @@ -392,20 +392,20 @@ let eval_call c = r in let handler = { - Ide_intf.interp = interruptible interp; - Ide_intf.rewind = interruptible Backtrack.back; - Ide_intf.goals = interruptible goals; - Ide_intf.evars = interruptible evars; - Ide_intf.hints = interruptible hints; - Ide_intf.status = interruptible status; - Ide_intf.search = interruptible search; - Ide_intf.inloadpath = interruptible inloadpath; - Ide_intf.get_options = interruptible get_options; - Ide_intf.set_options = interruptible set_options; - Ide_intf.mkcases = interruptible Vernacentries.make_cases; - Ide_intf.quit = (fun () -> raise Quit); - Ide_intf.about = interruptible about; - Ide_intf.handle_exn = handle_exn; } + Interface.interp = interruptible interp; + Interface.rewind = interruptible Backtrack.back; + Interface.goals = interruptible goals; + Interface.evars = interruptible evars; + Interface.hints = interruptible hints; + Interface.status = interruptible status; + Interface.search = interruptible search; + Interface.inloadpath = interruptible inloadpath; + Interface.get_options = interruptible get_options; + Interface.set_options = interruptible set_options; + Interface.mkcases = interruptible Vernacentries.make_cases; + Interface.quit = (fun () -> raise Quit); + Interface.about = interruptible about; + Interface.handle_exn = handle_exn; } in (* If the messages of last command are still there, we remove them *) ignore (read_stdout ()); diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index e30404e1..c8292937 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -271,7 +271,7 @@ let declare_congr_scheme ind = then ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind) else - warning "Cannot build congruence scheme because eq is not found" + msg_warn "Cannot build congruence scheme because eq is not found" end let declare_sym_scheme ind = diff --git a/toplevel/interface.mli b/toplevel/interface.mli index 7b4312a3..f2a22f22 100644 --- a/toplevel/interface.mli +++ b/toplevel/interface.mli @@ -86,8 +86,8 @@ type search_constraint = the flag should be negated. *) type search_flags = (search_constraint * bool) list -(** A named object in Coq. [coq_object_qualid] is the shortest path defined for - the user. [coq_object_prefix] is the missing part to recover the fully +(** A named object in Coq. [coq_object_qualid] is the shortest path defined for + 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 = { @@ -103,10 +103,129 @@ type coq_info = { compile_date : string; } -(** * Coq answers to CoqIde *) +(** 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 feedback_content = + | AddedAxiom + | Processed + | GlobRef of (int*int) * string * string * string * string + +type feedback = { + edit_id : edit_id; + content : feedback_content; +} + +(** Calls result *) type location = (int * int) option (* start and end of the error *) type 'a value = | Good of 'a | Fail of (location * string) + +(* Request/Reply message protocol between Coq and CoqIde *) + +(** Running a command (given as its id and its text). + "raw" mode (less sanity checks, no impact on the undo stack) + is suitable for queries, or for the Set/Unset + of display options that coqide performs all the time. + The returned string contains the messages produced + but not the updated goals (they are + to be fetch by a separated [current_goals]). *) +type interp_sty = edit_id * raw * verbose * string +type interp_rty = string + +(** Backtracking by at least a certain number of phrases. + No finished proofs will be re-opened. Instead, + we continue backtracking until before these proofs, + and answer the amount of extra backtracking performed. + Backtracking by more than the number of phrases already + interpreted successfully (and not yet undone) will fail. *) +type rewind_sty = int +type rewind_rty = int + +(** Fetching the list of current goals. Return [None] if no proof is in + progress, [Some gl] otherwise. *) +type goals_sty = unit +type goals_rty = goals option + +(** Retrieve the list of unintantiated evars in the current proof. [None] if no + proof is in progress. *) +type evars_sty = unit +type evars_rty = evar list option + +(** Retrieving the tactics applicable to the current goal. [None] if there is + no proof in progress. *) +type hints_sty = unit +type hints_rty = (hint list * hint) option + +(** The status, for instance "Ready in SomeSection, proving Foo" *) +type status_sty = unit +type status_rty = status + +(** Search for objects satisfying the given search flags. *) +type search_sty = search_flags +type search_rty = string coq_object list + +(** Retrieve the list of options of the current toplevel *) +type get_options_sty = unit +type get_options_rty = (option_name * option_state) list + +(** Set the options to the given value. Warning: this is not atomic, so whenever + the call fails, the option state can be messed up... This is the caller duty + to check that everything is correct. *) +type set_options_sty = (option_name * option_value) list +type set_options_rty = unit + +(** Is a directory part of Coq's loadpath ? *) +type inloadpath_sty = string +type inloadpath_rty = bool + +(** Create a "match" template for a given inductive type. + For each branch of the match, we list the constructor name + followed by enough pattern variables. *) +type mkcases_sty = string +type mkcases_rty = string list list + +(** Quit gracefully the interpreter. *) +type quit_sty = unit +type quit_rty = unit + +type about_sty = unit +type about_rty = coq_info + +type handle_exn_rty = location * string +type handle_exn_sty = exn + +type handler = { + interp : interp_sty -> interp_rty; + rewind : rewind_sty -> rewind_rty; + goals : goals_sty -> goals_rty; + evars : evars_sty -> evars_rty; + hints : hints_sty -> hints_rty; + status : status_sty -> status_rty; + search : search_sty -> search_rty; + get_options : get_options_sty -> get_options_rty; + set_options : set_options_sty -> set_options_rty; + inloadpath : inloadpath_sty -> inloadpath_rty; + mkcases : mkcases_sty -> mkcases_rty; + quit : quit_sty -> quit_rty; + about : about_sty -> about_rty; + handle_exn : handle_exn_sty -> handle_exn_rty; +} + diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 006dc5ec..7653bfc4 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -851,7 +851,7 @@ let check_rule_productivity l = error "A recursive notation must start with at least one symbol." let is_not_printable = function - | AVar _ -> warning "This notation will not be used for printing as it is bound to a \nsingle variable"; true + | AVar _ -> msg_warn "This notation will not be used for printing as it is bound to a \nsingle variable"; true | _ -> false let find_precedence lev etyps symbols = @@ -909,7 +909,7 @@ let remove_curly_brackets l = (match next' with | Terminal "}" as t2 :: l'' as l1 -> if l <> l0 or l' <> l1 then - warning "Skipping spaces inside curly brackets"; + msg_warn "Skipping spaces inside curly brackets"; if deb & l'' = [] then [t1;x;t2] else begin check_curly_brackets_notation_exists (); x :: aux false l'' diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index f08308d3..b6639c06 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -117,7 +117,7 @@ let dir_ml_load s = let dir_ml_use s = match !load with | WithTop t -> t.use_file s - | _ -> warning "Cannot access the ML compiler" + | _ -> msg_warn "Cannot access the ML compiler" (* Adds a path to the ML paths *) let add_ml_dir s = diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 75efe139..e7db8fac 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -801,7 +801,7 @@ let vernac_chdir = function | Some path -> begin try Sys.chdir (System.expand_path_macros path) - with Sys_error str -> warning ("Cd failed: " ^ str) + with Sys_error str -> msg_warn ("Cd failed: " ^ str) end; if_verbose message (Sys.getcwd()) @@ -883,6 +883,12 @@ let vernac_declare_arguments local r l nargs flags = | x, _ -> x in List.map (fun ns -> List.map name_anons (List.combine ns inf_names)) l in let names_decl = List.map (List.map (fun (id, _,_,_,_) -> id)) l in + let renamed_arg = ref None in + let set_renamed a b = + if !renamed_arg = None && a <> b then renamed_arg := Some(b,a) in + let pr_renamed_arg () = match !renamed_arg with None -> "" + | Some (o,n) -> + "\nArgument "^string_of_id o ^" renamed to "^string_of_id n^"." in let some_renaming_specified = try Arguments_renaming.arguments_names sr <> names_decl with Not_found -> false in @@ -894,15 +900,19 @@ let vernac_declare_arguments local r l nargs flags = | (Name x, _,_, true, _), Anonymous -> error ("Argument "^string_of_id x^" cannot be declared implicit.") | (Name iid, _,_, true, max), Name id -> + set_renamed iid id; b || iid <> id, Some (ExplByName id, max, false) - | (Name iid, _,_, _, _), Name id -> b || iid <> id, None + | (Name iid, _,_, _, _), Name id -> + set_renamed iid id; + b || iid <> id, None | _ -> b, None) sr (List.combine il inf_names) in sr || sr', Util.list_map_filter (fun x -> x) impl) some_renaming_specified l in if some_renaming_specified then if not (List.mem `Rename flags) then - error "To rename arguments the \"rename\" flag must be specified." + error ("To rename arguments the \"rename\" flag must be specified." + ^ pr_renamed_arg ()) else Arguments_renaming.rename_arguments local sr names_decl; (* All other infos are in the first item of l *) let l = List.hd l in |