diff options
91 files changed, 1392 insertions, 790 deletions
diff --git a/.gitignore b/.gitignore index 4acd9930e3..bea12162c4 100644 --- a/.gitignore +++ b/.gitignore @@ -52,9 +52,9 @@ dev/ocamldebug-coq plugins/micromega/csdpcert kernel/byterun/dllcoqrun.so coqdoc.sty -csdp.cache -test-suite/lia.cache -test-suite/nra.cache +.csdp.cache +test-suite/.lia.cache +test-suite/.nra.cache test-suite/trace test-suite/misc/universes/all_stdlib.v test-suite/misc/universes/universes.txt @@ -68,7 +68,7 @@ doc/faq/axioms.eps_t doc/faq/axioms.pdf doc/faq/axioms.pdf_t doc/faq/axioms.png -doc/refman/csdp.cache +doc/refman/.csdp.cache doc/refman/trace doc/refman/Reference-Manual.pdf doc/refman/Reference-Manual.ps @@ -135,7 +135,7 @@ kernel/copcodes.ml tools/tolink.ml theories/Numbers/Natural/BigN/NMake_gen.v ide/index_urls.txt -lia.cache +.lia.cache checker/names.ml checker/names.mli checker/esubst.ml @@ -111,6 +111,7 @@ Changes from V8.5pl2 to V8.5pl3 =============================== Critical bugfix + - #4876: Guard checker incompleteness when using primitive projections Other bugfixes @@ -119,7 +120,50 @@ Other bugfixes - #4673: regression in setoid_rewrite, unfolding let-ins for type unification. - #4754: Regression in setoid_rewrite, allow postponed unification problems to remain. - #4769: Anomaly with universe polymorphic schemes defined inside sections. -- #3886: Program: duplicate obligations of mutual fixpoints +- #3886: Program: duplicate obligations of mutual fixpoints. +- #4994: Documentation typo. +- #5008: Use the "md5" command on OpenBSD. +- #5007: Do not assume the "TERM" environment variable is always set. +- #4606: Output a break before a list only if there was an empty line. +- #5001: metas not cleaned properly in clenv_refine_in. +- #2336: incorrect glob data for module symbols (bug #2336). +- #4832: Remove extraneous dot in error message. +- Anomaly in printing a unification error message. +- #4947: Options which take string arguments are not backwards compatible. +- #4156: micromega cache files are now hidden files. +- #4871: interrupting par:abstract kills coqtop. +- #5043: [Admitted] lemmas pick up section variables. +- Fix name of internal refine ("simple refine"). +- #5062: probably a typo in Strict Proofs mode. +- #5065: Anomaly: Not a proof by induction. +- Restore native compiler optimizations, they were disabled since 8.5! +- #5077: failure on typing a fixpoint with evars in its type. +- Fix recursive notation bug. +- #5095: non relevant too strict test in let-in abstraction. +- Ensuring that the evar name is preserved by "rename". +- #4887: confusion between using and with in documentation of firstorder. +- Bug in subst with let-ins. +- #4762: eauto weaker than auto. +- Remove if_then_else (was buggy). Use tryif instead. +- #4970: confusion between special "{" and non special "{{" in notations. +- #4529: primitive projections unfolding. +- #4416: Incorrect "Error: Incorrect number of goals". +- #4863: abstract in typeclass hint fails. +- #5123: unshelve can impact typeclass resolution +- Fix a collision about the meta-variable ".." in recursive notations. +- Fix printing of info_auto. +- #3209: Not_found due to an occur-check cycle. +- #5097: status of evars refined by "clear" in ltac: closed wrt evars. +- #5150: Missing dependency of the test-suite subsystems in prerequisite. +- Fix a bug in error printing of unif constraints +- #3941: Do not stop propagation of signals when Coq is busy. +- #4822: Incorrect assertion in cbn. +- #3479 parsing of "{" and "}" when a keyword starts with "{" or "}". +- #5127: Memory corruption with the VM. +- #5102: bullets parsing broken by calls to parse_entry. + +Various documentation improvements + Changes from V8.5pl1 to V8.5pl2 =============================== diff --git a/Makefile.doc b/Makefile.doc index aa6e478a80..cdd9852e87 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -124,7 +124,7 @@ endif (cd `dirname $<`; $(DVIPS) -q -o `basename $@` `basename $<`) %.png: %.fig - $(FIG2DEV) -m 2 -L png $< $@ + $(FIG2DEV) -L png -m 2 $< $@ %.pdf: %.fig $(FIG2DEV) -L pdftex $< $@ diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index fcee79e07e..79a0c6312a 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -2,6 +2,11 @@ = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= +** Parsing ** + +Pcoq.parsable now takes an extra optional filename argument so as to +bind locations to a file name when relevant. + ** Files ** To avoid clashes with OCaml's compiler libs, the following files were renamed: @@ -251,6 +256,12 @@ define_evar_* mostly used internally in the unification engine. - `Tacexpr.TacDynamic(Loc.dummy_loc, Pretyping.constr_in c)` --> `Tacinterp.Value.of_constr c` +** Search API ** + +The main search functions now take a function iterating over the +results. This allows for clients to use streaming or more economic +printing. + ========================================= = CHANGES BETWEEN COQ V8.4 AND COQ V8.5 = ========================================= diff --git a/dev/top_printers.ml b/dev/top_printers.ml index e34385e5c3..a3d5cf5c12 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -215,7 +215,6 @@ let ppuniverse_subst l = pp (Univ.pr_universe_subst l) let ppuniverse_opt_subst l = pp (Universes.pr_universe_opt_subst l) let ppuniverse_level_subst l = pp (Univ.pr_universe_level_subst l) let ppevar_universe_context l = pp (Evd.pr_evar_universe_context l) -let ppconstraints_map c = pp (Universes.pr_constraints_map c) let ppconstraints c = pp (pr_constraints Level.pr c) let ppuniverseconstraints c = pp (Universes.Constraints.pr c) let ppuniverse_context_future c = diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 2da12c8d69..dd45feebc6 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3489,7 +3489,7 @@ hints of the database named {\tt core}. Uses the hint databases $\ident_1$ \dots\ $\ident_n$ in addition to the database {\tt core}. See Section~\ref{Hints-databases} for the list of pre-defined databases and the way to create or extend a - database. This option can be combined with the previous one. + database. \item {\tt auto with *} @@ -3503,9 +3503,17 @@ hints of the database named {\tt core}. $lemma_i$ is an inductive type, it is the collection of its constructors which is added as hints. -\item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ with \ident$_1$ {\ldots} \ident$_n$ +\item {\tt info\_auto} - This combines the effects of the {\tt using} and {\tt with} options. + Behaves like {\tt auto} but shows the tactics it uses to solve the goal. + This variant is very useful for getting a better understanding of automation, + or to know what lemmas/assumptions were used. + +\item {\tt \zeroone{info\_}auto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + + This is the most general form, combining the various options. \item {\tt trivial}\tacindex{trivial} @@ -3517,6 +3525,14 @@ hints of the database named {\tt core}. \item \texttt{trivial with *} +\item \texttt{trivial using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ + +\item {\tt info\_trivial} + +\item {\tt \zeroone{info\_}trivial} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + \end{Variants} \Rem {\tt auto} either solves completely the goal or else leaves it @@ -3530,8 +3546,8 @@ intact. \texttt{auto} and \texttt{trivial} never fail. This tactic generalizes {\tt auto}. While {\tt auto} does not try resolution hints which would leave existential variables in the goal, -{\tt eauto} does try them (informally speaking, it uses {\tt eapply} -where {\tt auto} uses {\tt apply}). +{\tt eauto} does try them (informally speaking, it uses +{\tt simple eapply} where {\tt auto} uses {\tt simple apply}). As a consequence, {\tt eauto} can solve such a goal: \begin{coq_eval} @@ -3546,8 +3562,17 @@ eauto. Abort. \end{coq_eval} -Note that {\tt ex\_intro} should be declared as an -hint. +Note that {\tt ex\_intro} should be declared as a hint. + +\begin{Variants} + +\item {\tt \zeroone{info\_}eauto \zeroone{\num}} \zeroone{{\tt using} \nterm{lemma}$_1$ + {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$} \zeroone{{\tt with} + \ident$_1$ {\ldots} \ident$_n$} + + The various options for eauto are the same as for auto. + +\end{Variants} \SeeAlso Section~\ref{Hints-databases} @@ -3701,11 +3726,12 @@ The {\hintdef} is one of the following expressions: the number of subgoals generated by {\tt simple apply {\term}}. %{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false - % Is it really needed? - %% In case the inferred type of \term\ does not start with a product - %% the tactic added in the hint list is {\tt exact {\term}}. In case - %% this type can however be reduced to a type starting with a product, - %% the tactic {\tt apply {\term}} is also stored in the hints list. + In case the inferred type of \term\ does not start with a product + the tactic added in the hint list is {\tt exact {\term}}. +% Actually, a slightly restricted version is used (no conversion on the head symbol) + In case + this type can however be reduced to a type starting with a product, + the tactic {\tt simple apply {\term}} is also stored in the hints list. If the inferred type of \term\ contains a dependent quantification on a variable which occurs only in the premisses of the type and not @@ -3735,6 +3761,17 @@ The {\hintdef} is one of the following expressions: Adds each \texttt{Resolve} {\term$_i$}. + \item {\tt Resolve -> \term} + + Adds the left-to-right implication of an equivalence as a hint + (informally the hint will be used as {\tt apply <- \term}, + although as mentionned before, the tactic actually used is + a restricted version of apply). + + \item {\tt Resolve <- \term} + + Adds the right-to-left implication of an equivalence as a hint. + \end{Variants} \item \texttt{Immediate {\term}} diff --git a/engine/evarutil.ml b/engine/evarutil.ml index e45e7dc496..df170c8ddc 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -678,6 +678,28 @@ let gather_dependent_evars evm l = (* /spiwack *) +(** [advance sigma g] returns [Some g'] if [g'] is undefined and is + the current avatar of [g] (for instance [g] was changed by [clear] + into [g']). It returns [None] if [g] has been (partially) + solved. *) +(* spiwack: [advance] is probably performance critical, and the good + behaviour of its definition may depend sensitively to the actual + definition of [Evd.find]. Currently, [Evd.find] starts looking for + a value in the heap of undefined variable, which is small. Hence in + the most common case, where [advance] is applied to an unsolved + goal ([advance] is used to figure if a side effect has modified the + goal) it terminates quickly. *) +let rec advance sigma evk = + let evi = Evd.find sigma evk in + match evi.evar_body with + | Evar_empty -> Some evk + | Evar_defined v -> + if Option.default false (Store.get evi.evar_extra cleared) then + let (evk,_) = Term.destEvar v in + advance sigma evk + else + None + (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. This is roughly a combination of the previous functions and diff --git a/engine/evarutil.mli b/engine/evarutil.mli index c0c81442d5..7fdc7aac78 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -110,6 +110,12 @@ val is_ground_env : evar_map -> env -> bool its (partial) definition. *) val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.Map.t +(** [advance sigma g] returns [Some g'] if [g'] is undefined and is + the current avatar of [g] (for instance [g] was changed by [clear] + into [g']). It returns [None] if [g] has been (partially) + solved. *) +val advance : evar_map -> evar -> evar option + (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. This is roughly a combination of the previous functions and diff --git a/engine/evd.ml b/engine/evd.ml index 6ba8a51120..aa91fc5222 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -641,6 +641,7 @@ let set_universe_context evd uctx' = { evd with universes = uctx' } let add_conv_pb ?(tail=false) pb d = + (** MS: we have duplicates here, why? *) if tail then {d with conv_pbs = d.conv_pbs @ [pb]} else {d with conv_pbs = pb::d.conv_pbs} @@ -1411,6 +1412,16 @@ let print_env_short env = let pr_evar_constraints pbs = let pr_evconstr (pbty, env, t1, t2) = + let env = + (** We currently allow evar instances to refer to anonymous de + Bruijn indices, so we protect the error printing code in this + case by giving names to every de Bruijn variable in the + rel_context of the conversion problem. MS: we should rather + stop depending on anonymous variables, they can be used to + indicate independency. Also, this depends on a strategy for + naming/renaming. *) + Namegen.make_all_name_different env + in print_env_short env ++ spc () ++ str "|-" ++ spc () ++ print_constr_env env t1 ++ spc () ++ str (match pbty with diff --git a/engine/proofview.ml b/engine/proofview.ml index 85a52fdcaf..855235d2b0 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -152,33 +152,9 @@ let focus i j sp = let (new_comb, context) = focus_sublist i j sp.comb in ( { sp with comb = new_comb } , context ) - -(** [advance sigma g] returns [Some g'] if [g'] is undefined and is - the current avatar of [g] (for instance [g] was changed by [clear] - into [g']). It returns [None] if [g] has been (partially) - solved. *) -(* spiwack: [advance] is probably performance critical, and the good - behaviour of its definition may depend sensitively to the actual - definition of [Evd.find]. Currently, [Evd.find] starts looking for - a value in the heap of undefined variable, which is small. Hence in - the most common case, where [advance] is applied to an unsolved - goal ([advance] is used to figure if a side effect has modified the - goal) it terminates quickly. *) -let rec advance sigma g = - let open Evd in - let evi = Evd.find sigma g in - match evi.evar_body with - | Evar_empty -> Some g - | Evar_defined v -> - if Option.default false (Store.get evi.evar_extra Evarutil.cleared) then - let (e,_) = Term.destEvar v in - advance sigma e - else - None - (** [undefined defs l] is the list of goals in [l] which are still unsolved (after advancing cleared goals). *) -let undefined defs l = CList.map_filter (advance defs) l +let undefined defs l = CList.map_filter (Evarutil.advance defs) l (** Unfocuses a proofview with respect to a context. *) let unfocus c sp = @@ -465,7 +441,7 @@ let iter_goal i = Comb.get >>= fun initial -> Proof.List.fold_left begin fun (subgoals as cur) goal -> Solution.get >>= fun step -> - match advance step goal with + match Evarutil.advance step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -489,7 +465,7 @@ let fold_left2_goal i s l = in Proof.List.fold_left2 err begin fun ((r,subgoals) as cur) goal a -> Solution.get >>= fun step -> - match advance step goal with + match Evarutil.advance step goal with | None -> return cur | Some goal -> Comb.set [goal] >> @@ -533,7 +509,7 @@ let tclDISPATCHGEN0 join tacs = let open Proof in Pv.get >>= function | { comb=[goal] ; solution } -> - begin match advance solution goal with + begin match Evarutil.advance solution goal with | None -> tclUNIT (join []) | Some _ -> Proof.map (fun res -> join [res]) tac end @@ -965,7 +941,7 @@ module Unsafe = struct let mark_as_goal evd content = mark_in_evm ~goal:true evd content - let advance = advance + let advance = Evarutil.advance let mark_as_unresolvable p gl = { p with solution = mark_in_evm ~goal:false p.solution gl } @@ -1130,7 +1106,7 @@ module Goal = struct Pv.get >>= fun step -> let sigma = step.solution in let map goal = - match advance sigma goal with + match Evarutil.advance sigma goal with | None -> None (** ppedrot: Is this check really necessary? *) | Some goal -> let gl = @@ -1144,7 +1120,7 @@ module Goal = struct let unsolved { self=self } = tclEVARMAP >>= fun sigma -> - tclUNIT (not (Option.is_empty (advance sigma self))) + tclUNIT (not (Option.is_empty (Evarutil.advance sigma self))) (* compatibility *) let goal { self=self } = self diff --git a/interp/constrextern.ml b/interp/constrextern.ml index afc1c4caf8..dd8a48b85e 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -149,17 +149,8 @@ let extern_evar loc n l = CEvar (loc,n,l) For instance, in the debugger the tables of global references may be inaccurate *) -let safe_shortest_qualid_of_global vars r = - try shortest_qualid_of_global vars r - with Not_found -> - match r with - | VarRef v -> make_qualid DirPath.empty v - | ConstRef c -> make_qualid DirPath.empty Names.(Label.to_id (con_label c)) - | IndRef (i,_) | ConstructRef ((i,_),_) -> - make_qualid DirPath.empty Names.(Label.to_id (mind_label i)) - let default_extern_reference loc vars r = - Qualid (loc,safe_shortest_qualid_of_global vars r) + Qualid (loc,shortest_qualid_of_global vars r) let my_extern_reference = ref default_extern_reference diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 29e33d349b..d5feafbf91 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -57,7 +57,7 @@ void init_arity () { arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]= arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]= arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]= - arity[BRANCH]=arity[ISCONST]= 1; + arity[BRANCH]=arity[ISCONST]=arity[ENSURESTACKCAPACITY]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= arity[ARECONST]=arity[PROJ]=2; @@ -79,7 +79,7 @@ void * coq_stat_alloc (asize_t sz) value coq_makeaccu (value i) { code_t q; - code_t res = coq_stat_alloc(8); + code_t res = coq_stat_alloc(2 * sizeof(opcode_t)); q = res; *q++ = VALINSTR(MAKEACCU); *q = (opcode_t)Int_val(i); @@ -91,13 +91,13 @@ value coq_pushpop (value i) { int n; n = Int_val(i); if (n == 0) { - res = coq_stat_alloc(4); + res = coq_stat_alloc(sizeof(opcode_t)); *res = VALINSTR(STOP); return (value)res; } else { code_t q; - res = coq_stat_alloc(12); + res = coq_stat_alloc(3 * sizeof(opcode_t)); q = res; *q++ = VALINSTR(POP); *q++ = (opcode_t)n; diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index 8c5ab0ecbd..d92e85fdf8 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -14,6 +14,8 @@ /* Nota: this list of instructions is parsed to produce derived files */ /* coq_jumptbl.h and copcodes.ml. Instructions should be uppercase */ /* and alone on lines starting by two spaces. */ +/* If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c */ +/* with the arity of the instruction and maybe coq_tcode_of_code. */ enum instructions { ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC, @@ -37,6 +39,7 @@ enum instructions { GETFIELD0, GETFIELD1, GETFIELD, SETFIELD0, SETFIELD1, SETFIELD, PROJ, + ENSURESTACKCAPACITY, CONST0, CONST1, CONST2, CONST3, CONSTINT, PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT, ACCUMULATE, diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index df5fdce755..792a311fcf 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -76,6 +76,14 @@ sp is a local copy of the global variable extern_sp. */ # define print_lint(i) #endif +#define CHECK_STACK(num_args) { \ +if (sp - num_args < coq_stack_threshold) { \ + coq_sp = sp; \ + realloc_coq_stack(num_args + Coq_stack_threshold / sizeof(value)); \ + sp = coq_sp; \ + } \ +} + /* GC interface */ #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; } #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; } @@ -198,6 +206,9 @@ value coq_interprete sp = coq_sp; pc = coq_pc; accu = coq_accu; + + CHECK_STACK(0); + #ifdef THREADED_CODE goto *(void *)(coq_jumptbl_base + *pc++); /* Jump to the first instruction */ #else @@ -354,7 +365,7 @@ value coq_interprete coq_extra_args = *pc - 1; pc = Code_val(accu); coq_env = accu; - goto check_stacks; + goto check_stack; } Instruct(APPLY1) { value arg1 = sp[0]; @@ -371,7 +382,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args = 0; - goto check_stacks; + goto check_stack; } Instruct(APPLY2) { value arg1 = sp[0]; @@ -386,7 +397,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args = 1; - goto check_stacks; + goto check_stack; } Instruct(APPLY3) { value arg1 = sp[0]; @@ -403,17 +414,13 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args = 2; - goto check_stacks; + goto check_stack; } /* Stack checks */ - check_stacks: - print_instr("check_stacks"); - if (sp < coq_stack_threshold) { - coq_sp = sp; - realloc_coq_stack(Coq_stack_threshold); - sp = coq_sp; - } + check_stack: + print_instr("check_stack"); + CHECK_STACK(0); /* We also check for signals */ if (caml_signals_are_pending) { /* If there's a Ctrl-C, we reset the vm */ @@ -422,6 +429,16 @@ value coq_interprete } Next; + Instruct(ENSURESTACKCAPACITY) { + print_instr("ENSURESTACKCAPACITY"); + int size = *pc++; + /* CHECK_STACK may trigger here a useless allocation because of the + threshold, but check_stack: often does it anyway, so we prefer to + factorize the code. */ + CHECK_STACK(size); + Next; + } + Instruct(APPTERM) { int nargs = *pc++; int slotsize = *pc; @@ -436,7 +453,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args += nargs - 1; - goto check_stacks; + goto check_stack; } Instruct(APPTERM1) { value arg1 = sp[0]; @@ -445,7 +462,7 @@ value coq_interprete sp[0] = arg1; pc = Code_val(accu); coq_env = accu; - goto check_stacks; + goto check_stack; } Instruct(APPTERM2) { value arg1 = sp[0]; @@ -458,7 +475,7 @@ value coq_interprete print_lint(accu); coq_env = accu; coq_extra_args += 1; - goto check_stacks; + goto check_stack; } Instruct(APPTERM3) { value arg1 = sp[0]; @@ -472,7 +489,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args += 2; - goto check_stacks; + goto check_stack; } Instruct(RETURN) { @@ -503,6 +520,7 @@ value coq_interprete int num_args = Wosize_val(coq_env) - 2; int i; print_instr("RESTART"); + CHECK_STACK(num_args); sp -= num_args; for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2); coq_env = Field(coq_env, 1); @@ -539,6 +557,7 @@ value coq_interprete pc++;/* On saute le Restart */ } else { if (coq_extra_args < rec_pos) { + /* Partial application */ mlsize_t num_args, i; num_args = 1 + coq_extra_args; /* arg1 + extra args */ Alloc_small(accu, num_args + 2, Closure_tag); @@ -553,10 +572,10 @@ value coq_interprete } else { /* The recursif argument is an accumulator */ mlsize_t num_args, i; - /* Construction of partially applied PF */ + /* Construction of fixpoint applied to its [rec_pos-1] first arguments */ Alloc_small(accu, rec_pos + 2, Closure_tag); - Field(accu, 1) = coq_env; - for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; + Field(accu, 1) = coq_env; // We store the fixpoint in the first field + for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; // Storing args Code_val(accu) = pc; sp += rec_pos; *--sp = accu; @@ -862,29 +881,7 @@ value coq_interprete sp++; Next; } - - /* *sp = accu; - * Netoyage des cofix * - size = Wosize_val(accu); - for (i = 2; i < size; i++) { - accu = Field(*sp, i); - if (IS_EVALUATED_COFIX(accu)) { - size_aux = Wosize_val(accu); - *--sp = accu; - Alloc_small(accu, size_aux, Accu_tag); - for(j = 0; j < size_aux; j++) Field(accu, j) = Field(*sp, j); - *sp = accu; - Alloc_small(accu, 1, ATOM_COFIX_TAG); - Field(accu, 0) = Field(Field(*sp, 1), 0); - caml_modify(&Field(*sp, 1), accu); - accu = *sp; sp++; - caml_modify(&Field(*sp, i), accu); - } - } - sp++; - Next; - } */ - + Instruct(SETFIELD){ print_instr("SETFIELD"); caml_modify(&Field(accu, *pc),*sp); @@ -978,28 +975,31 @@ value coq_interprete } Instruct(MAKESWITCHBLOCK) { print_instr("MAKESWITCHBLOCK"); - *--sp = accu; - accu = Field(accu,1); + *--sp = accu; // Save matched block on stack + accu = Field(accu,1); // Save atom to accu register switch (Tag_val(accu)) { - case ATOM_COFIX_TAG: + case ATOM_COFIX_TAG: // We are forcing a cofix { mlsize_t i, nargs; print_instr("COFIX_TAG"); sp-=2; pc++; + // Push the return address sp[0] = (value) (pc + *pc); sp[1] = coq_env; - coq_env = Field(accu,0); - accu = sp[2]; - sp[2] = Val_long(coq_extra_args); - nargs = Wosize_val(accu) - 2; + coq_env = Field(accu,0); // Pointer to suspension + accu = sp[2]; // Save accumulator to accu register + sp[2] = Val_long(coq_extra_args); // Push number of args for return + nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom) + // Push arguments to stack + CHECK_STACK(nargs+1); sp -= nargs; - for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); - *--sp = accu; + for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); + *--sp = accu; // Last argument is the pointer to the suspension print_lint(nargs); coq_extra_args = nargs; - pc = Code_val(coq_env); - goto check_stacks; + pc = Code_val(coq_env); // Trigger evaluation + goto check_stack; } case ATOM_COFIXEVALUATED_TAG: { @@ -1024,7 +1024,7 @@ value coq_interprete annot = *pc++; sz = *pc++; *--sp=Field(coq_global_data, annot); - /* On sauve la pile */ + /* We save the stack */ if (sz == 0) accu = Atom(0); else { Alloc_small(accu, sz, Default_tag); @@ -1035,17 +1035,17 @@ value coq_interprete } } *--sp = accu; - /* On cree le zipper switch */ + /* We create the switch zipper */ Alloc_small(accu, 5, Default_tag); Field(accu, 0) = (value)typlbl; Field(accu, 1) = (value)swlbl; Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; Field(accu, 4) = coq_env; sp++;sp[0] = accu; - /* On cree l'atome */ + /* We create the atom */ Alloc_small(accu, 2, ATOM_SWITCH_TAG); Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0]; sp++;sp[0] = accu; - /* On cree l'accumulateur */ + /* We create the accumulator */ Alloc_small(accu, 2, Accu_tag); Code_val(accu) = accumulate; Field(accu,1) = *sp++; @@ -1457,26 +1457,32 @@ value coq_push_val(value v) { value coq_push_arguments(value args) { int nargs,i; + value * sp = coq_sp; nargs = Wosize_val(args) - 2; + CHECK_STACK(nargs); coq_sp -= nargs; print_instr("push_args");print_int(nargs); for(i = 0; i < nargs; i++) coq_sp[i] = Field(args, i+2); return Val_unit; } -value coq_push_vstack(value stk) { +value coq_push_vstack(value stk, value max_stack_size) { int len,i; + value * sp = coq_sp; len = Wosize_val(stk); + CHECK_STACK(len); coq_sp -= len; print_instr("push_vstack");print_int(len); for(i = 0; i < len; i++) coq_sp[i] = Field(stk,i); + sp = coq_sp; + CHECK_STACK(uint32_of_value(max_stack_size)); return Val_unit; } value coq_interprete_ml(value tcode, value a, value e, value ea) { print_instr("coq_interprete"); return coq_interprete((code_t)tcode, a, e, Long_val(ea)); - print_instr("end coq_interprete"); + print_instr("end coq_interprete"); } value coq_eval_tcode (value tcode, value e) { diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index c9bcdc32ff..45cfae509d 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -130,6 +130,7 @@ value init_coq_vm(value unit) /* ML */ return Val_unit;; } +/* [required_space] is a size in words */ void realloc_coq_stack(asize_t required_space) { asize_t size; diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 8d4de523a1..810c346990 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -43,7 +43,7 @@ type structured_constant = type reloc_table = (tag * int) array type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool} + {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} module Label = struct @@ -87,6 +87,7 @@ type instruction = | Ksequence of bytecodes * bytecodes | Kproj of int * Constant.t (* index of the projected argument, name of projection *) + | Kensurestackcapacity of int (* spiwack: instructions concerning integers *) | Kbranch of Label.t (* jump to label *) | Kaddint31 (* adds the int31 in the accu @@ -264,6 +265,8 @@ let rec pp_instr i = | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p + | Kensurestackcapacity size -> str "growstack " ++ int size + | Kaddint31 -> str "addint31" | Kaddcint31 -> str "addcint31" | Kaddcarrycint31 -> str "addcarrycint31" diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 5f1f09d00c..b8de7619cf 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -39,7 +39,7 @@ val pp_struct_const : structured_constant -> Pp.std_ppcmds type reloc_table = (tag * int) array type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool} + {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} module Label : sig @@ -84,6 +84,7 @@ type instruction = | Ksequence of bytecodes * bytecodes | Kproj of int * Constant.t (** index of the projected argument, name of projection *) + | Kensurestackcapacity of int (** spiwack: instructions concerning integers *) | Kbranch of Label.t (** jump to label, is it needed ? *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 008955d804..b1fc0c85de 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -91,6 +91,11 @@ open Pre_env (* In Cfxe_t accumulators, we need to store [fcofixi] for testing *) (* conversion of cofixpoints (which is intentional). *) +module Config = struct + let stack_threshold = 256 (* see byterun/coq_memory.h *) + let stack_safety_margin = 15 +end + type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t let empty_fv = { size= 0; fv_rev = []; fv_fwd = FvMap.empty } @@ -112,6 +117,26 @@ let empty_comp_env ?(univs=0) ()= in_env = ref empty_fv } +(* Maximal stack size reached during the current function body. Used to + reallocate the stack if we lack space. *) +let max_stack_size = ref 0 + +let set_max_stack_size stack_size = + if stack_size > !max_stack_size then + max_stack_size := stack_size + +let ensure_stack_capacity f x = + let old = !max_stack_size in + max_stack_size := 0; + let code = f x in + let used_safe = + !max_stack_size + Config.stack_safety_margin + in + max_stack_size := old; + if used_safe > Config.stack_threshold then + Kensurestackcapacity used_safe :: code + else code + (*i Creation functions for comp_env *) let rec add_param n sz l = @@ -370,14 +395,28 @@ let const_bn tag args = else Const_bn(last_variant_tag, Array.append [|Const_b0 (tag - last_variant_tag) |] args) - -let code_makeblock arity tag cont = +(* +If [tag] hits the OCaml limitation for non constant constructors, we switch to +another representation for the remaining constructors: +[last_variant_tag|tag - last_variant_tag|args] + +We subtract last_variant_tag for efficiency of match interpretation. + *) + +let nest_block tag arity cont = + Kconst (Const_b0 (tag - last_variant_tag)) :: + Kmakeblock(arity+1, last_variant_tag) :: cont + +let code_makeblock ~stack_size ~arity ~tag cont = if tag < last_variant_tag then Kmakeblock(arity, tag) :: cont - else - Kpush :: Kconst (Const_b0 (tag - last_variant_tag)) :: - Kmakeblock(arity+1, last_variant_tag) :: cont + else begin + set_max_stack_size (stack_size + 1); + Kpush :: nest_block tag arity cont + end +(* [code_construct] compiles an abstracted constructor dropping parameters and + updates [fun_code] *) (* Inv : nparam + arity > 0 *) let code_construct tag nparams arity cont = let f_cont = @@ -386,11 +425,11 @@ let code_construct tag nparams arity cont = [Kconst (Const_b0 tag); Kreturn 0] else if tag < last_variant_tag then [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0] - else - [Kconst (Const_b0 (tag - last_variant_tag)); - Kmakeblock(arity+1, last_variant_tag); Kreturn 0]) + else + nest_block tag arity [Kreturn 0]) in let lbl = Label.create() in + (* No need to grow the stack here, as the function does not push stuff. *) fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)]; Kclosure(lbl,0) :: cont @@ -506,6 +545,7 @@ let comp_args comp_expr reloc args sz cont = done; !c +(* Precondition: args not empty *) let comp_app comp_fun comp_arg reloc f args sz cont = let nargs = Array.length args in match is_tailcall cont with @@ -535,11 +575,12 @@ let compile_fv_elem reloc fv sz cont = let rec compile_fv reloc l sz cont = match l with | [] -> cont - | [fvn] -> compile_fv_elem reloc fvn sz cont + | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem reloc fvn sz cont | fvn :: tl -> compile_fv_elem reloc fvn sz (Kpush :: compile_fv reloc tl (sz + 1) cont) + (* Compiling constants *) let rec get_alias env kn = @@ -554,6 +595,7 @@ let rec get_alias env kn = (* sz is the size of the local stack *) let rec compile_constr reloc c sz cont = + set_max_stack_size sz; match kind_of_term c with | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta" | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar" @@ -602,6 +644,7 @@ let rec compile_constr reloc c sz cont = compile_str_cst reloc (Bstrconst (Const_sorts (Type uglob))) sz cont else let compile_get_univ reloc idx sz cont = + set_max_stack_size sz; compile_fv_elem reloc (FVuniv_var idx) sz cont in comp_app compile_str_cst compile_get_univ reloc @@ -621,7 +664,8 @@ let rec compile_constr reloc c sz cont = let r_fun = comp_env_fun arity in let lbl_fun = Label.create() in let cont_fun = - compile_constr r_fun body arity [Kreturn arity] in + ensure_stack_capacity (compile_constr r_fun body arity) [Kreturn arity] + in fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)]; let fv = fv r_fun in compile_fv reloc fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) @@ -641,9 +685,10 @@ let rec compile_constr reloc c sz cont = (* Compilation des types *) let env_type = comp_env_fix_type rfv in for i = 0 to ndef - 1 do - let lbl,fcode = - label_code - (compile_constr env_type type_bodies.(i) 0 [Kstop]) in + let fcode = + ensure_stack_capacity (compile_constr env_type type_bodies.(i) 0) [Kstop] + in + let lbl,fcode = label_code fcode in lbl_types.(i) <- lbl; fun_code := [Ksequence(fcode,!fun_code)] done; @@ -653,7 +698,8 @@ let rec compile_constr reloc c sz cont = let arity = List.length params in let env_body = comp_env_fix ndef i arity rfv in let cont1 = - compile_constr env_body body arity [Kreturn arity] in + ensure_stack_capacity (compile_constr env_body body arity) [Kreturn arity] + in let lbl = Label.create () in lbl_bodies.(i) <- lbl; let fcode = add_grabrec rec_args.(i) arity lbl cont1 in @@ -671,9 +717,10 @@ let rec compile_constr reloc c sz cont = let rfv = ref empty_fv in let env_type = comp_env_cofix_type ndef rfv in for i = 0 to ndef - 1 do - let lbl,fcode = - label_code - (compile_constr env_type type_bodies.(i) 0 [Kstop]) in + let fcode = + ensure_stack_capacity (compile_constr env_type type_bodies.(i) 0) [Kstop] + in + let lbl,fcode = label_code fcode in lbl_types.(i) <- lbl; fun_code := [Ksequence(fcode,!fun_code)] done; @@ -683,14 +730,17 @@ let rec compile_constr reloc c sz cont = let arity = List.length params in let env_body = comp_env_cofix ndef arity rfv in let lbl = Label.create () in - let cont1 = - compile_constr env_body body (arity+1) (cont_cofix arity) in - let cont2 = - add_grab (arity+1) lbl cont1 in + let comp arity = + (* 4 stack slots are needed to update the cofix when forced *) + set_max_stack_size (arity + 4); + compile_constr env_body body (arity+1) (cont_cofix arity) + in + let cont = ensure_stack_capacity comp arity in lbl_bodies.(i) <- lbl; - fun_code := [Ksequence(cont2,!fun_code)]; + fun_code := [Ksequence(add_grab (arity+1) lbl cont,!fun_code)]; done; let fv = !rfv in + set_max_stack_size (sz + fv.size + ndef + 2); compile_fv reloc fv.fv_rev sz (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont) @@ -708,9 +758,11 @@ let rec compile_constr reloc c sz cont = let lbl_eblocks = Array.make neblock Label.no in let branch1,cont = make_branch cont in (* Compiling return type *) - let lbl_typ,fcode = - label_code (compile_constr reloc t sz [Kpop sz; Kstop]) - in fun_code := [Ksequence(fcode,!fun_code)]; + let fcode = + ensure_stack_capacity (compile_constr reloc t sz) [Kpop sz; Kstop] + in + let lbl_typ,fcode = label_code fcode in + fun_code := [Ksequence(fcode,!fun_code)]; (* Compiling branches *) let lbl_sw = Label.create () in let sz_b,branch,is_tailcall = @@ -720,14 +772,9 @@ let rec compile_constr reloc c sz cont = sz, branch1, true | _ -> sz+3, Kjump, false in - let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in - (* Compiling branch for accumulators *) - let lbl_accu, code_accu = - label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch::cont) - in - lbl_blocks.(0) <- lbl_accu; - let c = ref code_accu in - (* perform the extra match if needed (to many block constructors) *) + + let c = ref cont in + (* Perform the extra match if needed (too many block constructors) *) if neblock <> 0 then begin let lbl_b, code_b = label_code ( @@ -757,14 +804,34 @@ let rec compile_constr reloc c sz cont = compile_constr reloc branchs.(i) (sz_b+arity) (Kappterm(arity,sz_appterm) :: !c) in let code_b = - if tag < last_variant_tag then Kpushfields arity :: code_b - else Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b in + if tag < last_variant_tag then begin + set_max_stack_size (sz_b + arity); + Kpushfields arity :: code_b + end + else begin + set_max_stack_size (sz_b + arity + 1); + Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b + end + in let lbl_b,code_b = label_code code_b in if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b else lbl_eblocks.(tag - last_variant_tag) <- lbl_b; c := code_b done; - c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c; + + let annot = + {ci = ci; rtbl = tbl; tailcall = is_tailcall; + max_stack_size = !max_stack_size - sz} + in + + (* Compiling branch for accumulators *) + let lbl_accu, code_accu = + set_max_stack_size (sz+3); + label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch :: !c) + in + lbl_blocks.(0) <- lbl_accu; + + c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: code_accu; let code_sw = match branch1 with (* spiwack : branch1 can't be a lbl anymore it's a Branch instead @@ -781,12 +848,14 @@ let rec compile_constr reloc c sz cont = code_sw) and compile_str_cst reloc sc sz cont = + set_max_stack_size sz; match sc with | Bconstr c -> compile_constr reloc c sz cont | Bstrconst sc -> Kconst sc :: cont | Bmakeblock(tag,args) -> - let nargs = Array.length args in - comp_args compile_str_cst reloc args sz (code_makeblock nargs tag cont) + let arity = Array.length args in + let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in + comp_args compile_str_cst reloc args sz cont | Bconstruct_app(tag,nparams,arity,args) -> if Int.equal (Array.length args) 0 then code_construct tag nparams arity cont @@ -800,6 +869,7 @@ and compile_str_cst reloc sc sz cont = (* spiwack : compilation of constants with their arguments. Makes a special treatment with 31-bit integer addition *) and compile_get_global reloc (kn,u) sz cont = + set_max_stack_size sz; let kn = get_alias !global_env kn in if Univ.Instance.is_empty u then Kgetglobal kn :: cont @@ -808,11 +878,13 @@ and compile_get_global reloc (kn,u) sz cont = compile_universe reloc () (Univ.Instance.to_array u) sz cont and compile_universe reloc uni sz cont = + set_max_stack_size sz; match Univ.Level.var_index uni with | None -> Kconst (Const_univ_level uni) :: cont | Some idx -> pos_universe_var idx reloc sz :: cont and compile_const reloc kn u args sz cont = + set_max_stack_size sz; let nargs = Array.length args in (* spiwack: checks if there is a specific way to compile the constant if there is not, Not_found is raised, and the function @@ -874,7 +946,7 @@ let compile fail_on_error ?universes:(universes=0) env c = let reloc, init_code = if Int.equal universes 0 then let reloc = empty_comp_env () in - reloc, compile_constr reloc c 0 cont + reloc, ensure_stack_capacity (compile_constr reloc c 0) cont else (* We are going to generate a lambda, but merge the universe closure * with the function closure if it exists. @@ -891,11 +963,16 @@ let compile fail_on_error ?universes:(universes=0) env c = let r_fun = comp_env_fun ~univs:universes arity in let lbl_fun = Label.create () in let cont_fun = - compile_constr r_fun body full_arity [Kreturn full_arity] + ensure_stack_capacity (compile_constr r_fun body full_arity) + [Kreturn full_arity] in fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)]; let fv = fv r_fun in - reloc, compile_fv reloc fv.fv_rev 0 (Kclosure(lbl_fun,fv.size) :: cont) + let init_code = + ensure_stack_capacity (compile_fv reloc fv.fv_rev 0) + (Kclosure(lbl_fun,fv.size) :: cont) + in + reloc, init_code in let fv = List.rev (!(reloc.in_env).fv_rev) in (if !Flags.dump_bytecode then diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index d779a81ff6..ad7a41a347 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -234,6 +234,7 @@ let emit_instr = function else (out opSETFIELD;out_int n) | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr" | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p) + | Kensurestackcapacity size -> out opENSURESTACKCAPACITY; out_int size (* spiwack *) | Kbranch lbl -> out opBRANCH; out_label lbl | Kaddint31 -> out opADDINT31 diff --git a/kernel/make-opcodes b/kernel/make-opcodes index c8f573c682..e1371b3d0c 100644 --- a/kernel/make-opcodes +++ b/kernel/make-opcodes @@ -1,2 +1,3 @@ $1=="enum" {n=0; next; } - {for (i = 1; i <= NF; i++) {printf("let op%s = %d\n", $i, n++);}} + {printf("(* THIS FILE IS GENERATED. DON'T EDIT. *)\n\n"); + for (i = 1; i <= NF; i++) {printf("let op%s = %d\n", $i, n++);}} diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 894f5296a8..74d956bef0 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -77,6 +77,7 @@ and conv_whd env pb k whd1 whd2 cu = | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> conv_atom env pb k a1 stk1 a2 stk2 cu | Vfun _, _ | _, Vfun _ -> + (* on the fly eta expansion *) conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ diff --git a/kernel/vm.ml b/kernel/vm.ml index eb992ef892..53483a2220 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -170,7 +170,7 @@ type whd = external push_ra : tcode -> unit = "coq_push_ra" external push_val : values -> unit = "coq_push_val" external push_arguments : arguments -> unit = "coq_push_arguments" -external push_vstack : vstack -> unit = "coq_push_vstack" +external push_vstack : vstack -> int -> unit = "coq_push_vstack" (* interpreteur *) @@ -206,7 +206,9 @@ let apply_varray vf varray = else begin push_ra stop; - push_vstack varray; + (* The fun code of [vf] will make sure we have enough stack, so we put 0 + here. *) + push_vstack varray 0; interprete (fun_code vf) vf (Obj.magic vf) (n - 1) end @@ -560,7 +562,9 @@ let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl let case_info sw = sw.sw_annot.ci let type_of_switch sw = - push_vstack sw.sw_stk; + (* The fun code of types will make sure we have enough stack, so we put 0 + here. *) + push_vstack sw.sw_stk 0; interprete sw.sw_type_code crazy_val sw.sw_env 0 let branch_arg k (tag,arity) = @@ -580,9 +584,10 @@ let branch_arg k (tag,arity) = let apply_switch sw arg = let tc = sw.sw_annot.tailcall in if tc then - (push_ra stop;push_vstack sw.sw_stk) + (push_ra stop;push_vstack sw.sw_stk sw.sw_annot.max_stack_size) else - (push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk))); + (push_vstack sw.sw_stk sw.sw_annot.max_stack_size; + push_ra (popstop_code (Array.length sw.sw_stk))); interprete sw.sw_code arg sw.sw_env 0 let branch_of_switch k sw = diff --git a/lib/flags.ml b/lib/flags.ml index 65873e5214..0e2f7e5a62 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -70,7 +70,7 @@ let priority_of_string = function | "high" -> High | _ -> raise (Invalid_argument "priority_of_string") type tac_error_filter = [ `None | `Only of string list | `All ] -let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "curly" ]) +let async_proofs_tac_error_resilience = ref (`Only [ "curly" ]) let async_proofs_cmd_error_resilience = ref true let async_proofs_is_worker () = @@ -139,8 +139,6 @@ let pr_version = function (* Translate *) let beautify = ref false -let make_beautify f = beautify := f -let do_beautify () = !beautify let beautify_file = ref false (* Silent / Verbose *) diff --git a/lib/flags.mli b/lib/flags.mli index 9dc0c9c048..897602641c 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -70,8 +70,6 @@ val version_less_or_equal : compat_version -> bool val pr_version : compat_version -> string val beautify : bool ref -val make_beautify : bool -> unit -val do_beautify : unit -> bool val beautify_file : bool ref val make_silent : bool -> unit diff --git a/lib/stateid.ml b/lib/stateid.ml index 500581a39e..ae25735c5f 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -22,7 +22,7 @@ let to_int id = id let newer_than id1 id2 = id1 > id2 let state_id_info : (t * t) Exninfo.t = Exninfo.make () -let add exn ?(valid = initial) id = +let add exn ~valid id = Exninfo.add exn state_id_info (valid, id) let get exn = Exninfo.get exn state_id_info diff --git a/lib/stateid.mli b/lib/stateid.mli index cd8fddf0ce..1d87a343b3 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -26,9 +26,8 @@ val newer_than : t -> t -> bool (* Attaches to an exception the concerned state id, plus an optional * state id that is a valid state id before the error. - * Backtracking to the valid id is safe. - * The initial_state_id is assumed to be safe. *) -val add : Exninfo.info -> ?valid:t -> t -> Exninfo.info + * Backtracking to the valid id is safe. *) +val add : Exninfo.info -> valid:t -> t -> Exninfo.info val get : Exninfo.info -> (t * t) option type ('a,'b) request = { diff --git a/lib/unicode.ml b/lib/unicode.ml index dc852d9819..ced5e258c2 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -8,9 +8,7 @@ (** Unicode utilities *) -type status = Letter | IdentPart | Symbol - -exception Unsupported +type status = Letter | IdentPart | Symbol | Unknown (* The following table stores classes of Unicode characters that are used by the lexer. There are 3 different classes so 2 bits are @@ -29,6 +27,7 @@ let mask i = function | Letter -> 1 lsl ((i land 7) lsl 1) (* 01 *) | IdentPart -> 2 lsl ((i land 7) lsl 1) (* 10 *) | Symbol -> 3 lsl ((i land 7) lsl 1) (* 11 *) + | Unknown -> 0 lsl ((i land 7) lsl 1) (* 00 *) (* Helper to reset 2 bits in a word. *) let reset_mask i = @@ -55,7 +54,7 @@ let lookup x = if v = 1 then Letter else if v = 2 then IdentPart else if v = 3 then Symbol - else raise Unsupported + else Unknown (* [classify] discriminates between 3 different kinds of symbols based on the standard unicode classification (extracted from @@ -215,7 +214,6 @@ let ident_refutation s = |x -> x with | End_of_input -> Some (true,"The empty string is not an identifier.") - | Unsupported -> Some (true,s^": unsupported character in utf8 sequence.") | Invalid_argument _ -> Some (true,s^": invalid utf8 sequence.") let lowercase_unicode = diff --git a/lib/unicode.mli b/lib/unicode.mli index 1f8bd44eee..2609e1968f 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -8,22 +8,16 @@ (** Unicode utilities *) -type status = Letter | IdentPart | Symbol +type status = Letter | IdentPart | Symbol | Unknown -(** This exception is raised when UTF-8 the input string contains unsupported UTF-8 characters. *) -exception Unsupported - -(** Classify a unicode char into 3 classes. - @raise Unsupported if the input string contains unsupported UTF-8 characters. *) +(** Classify a unicode char into 3 classes or unknown. *) val classify : int -> status (** Return [None] if a given string can be used as a (Coq) identifier. - Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity. - @raise Unsupported if the input string contains unsupported UTF-8 characters. *) + Return [Some (b,s)] otherwise, where [s] is an explanation and [b] is severity. *) val ident_refutation : string -> (bool * string) option (** First char of a string, converted to lowercase - @raise Unsupported if the input string contains unsupported UTF-8 characters. @raise Assert_failure if the input string is empty. *) val lowercase_first_char : string -> string diff --git a/library/declare.ml b/library/declare.ml index c5b83c11a0..c9992fff3b 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -491,8 +491,10 @@ let do_universe poly l = type constraint_decl = polymorphic * Univ.constraints let cache_constraints (na, (p, c)) = - let ctx = Univ.ContextSet.add_constraints c Univ.ContextSet.empty in - cache_universe_context (p,ctx) + let ctx = + Univ.ContextSet.add_constraints c + Univ.ContextSet.empty (* No declared universes here, just constraints *) + in cache_universe_context (p,ctx) let discharge_constraints (_, (p, c as a)) = if p then None else Some a diff --git a/library/universes.ml b/library/universes.ml index db95607f18..112b20a4c4 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -702,12 +702,45 @@ let pr_universe_body = function let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body -exception Found of Level.t +let compare_constraint_type d d' = + match d, d' with + | Eq, Eq -> 0 + | Eq, _ -> -1 + | _, Eq -> 1 + | Le, Le -> 0 + | Le, _ -> -1 + | _, Le -> 1 + | Lt, Lt -> 0 + +type lowermap = constraint_type LMap.t + +let lower_union = + let merge k a b = + match a, b with + | Some _, None -> a + | None, Some _ -> b + | None, None -> None + | Some l, Some r -> + if compare_constraint_type l r >= 0 then a + else b + in LMap.merge merge + +let lower_add l c m = + try let c' = LMap.find l m in + if compare_constraint_type c c' > 0 then + LMap.add l c m + else m + with Not_found -> LMap.add l c m + +let lower_of_list l = + List.fold_left (fun acc (d,l) -> LMap.add l d acc) LMap.empty l + +exception Found of Level.t * lowermap let find_inst insts v = - try LMap.iter (fun k (enf,alg,v') -> - if not alg && enf && Universe.equal v' v then raise (Found k)) + try LMap.iter (fun k (enf,alg,v',lower) -> + if not alg && enf && Universe.equal v' v then raise (Found (k, lower))) insts; raise Not_found - with Found l -> l + with Found (f,l) -> (f,l) let compute_lbound left = (** The universe variable was not fixed yet. @@ -726,27 +759,33 @@ let compute_lbound left = else None)) None left -let instantiate_with_lbound u lbound alg enforce (ctx, us, algs, insts, cstrs) = +let instantiate_with_lbound u lbound lower alg enforce (ctx, us, algs, insts, cstrs) = if enforce then let inst = Universe.make u in let cstrs' = enforce_leq lbound inst cstrs in (ctx, us, LSet.remove u algs, - LMap.add u (enforce,alg,lbound) insts, cstrs'), (enforce, alg, inst) + LMap.add u (enforce,alg,lbound,lower) insts, cstrs'), + (enforce, alg, inst, lower) else (* Actually instantiate *) (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs, - LMap.add u (enforce,alg,lbound) insts, cstrs), (enforce, alg, lbound) + LMap.add u (enforce,alg,lbound,lower) insts, cstrs), + (enforce, alg, lbound, lower) type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t let pr_constraints_map cmap = LMap.fold (fun l cstrs acc -> Level.pr l ++ str " => " ++ - prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ fnl () - ++ acc) + prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ + fnl () ++ acc) cmap (mt ()) let remove_alg l (ctx, us, algs, insts, cstrs) = (ctx, us, LSet.remove l algs, insts, cstrs) + +let remove_lower u lower = + let levels = Universe.levels u in + LSet.fold (fun l acc -> LMap.remove l acc) levels lower let minimize_univ_variables ctx us algs left right cstrs = let left, lbounds = @@ -756,22 +795,50 @@ let minimize_univ_variables ctx us algs left right cstrs = let lbounds' = match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with | None -> lbounds - | Some lbound -> LMap.add r (true, false, lbound) lbounds + | Some lbound -> LMap.add r (true, false, lbound, lower_of_list lower) + lbounds in (Univ.LMap.remove r left, lbounds')) left (left, Univ.LMap.empty) in let rec instance (ctx', us, algs, insts, cstrs as acc) u = - let acc, left = - try let l = LMap.find u left in - List.fold_left - (fun (acc, left') (d, l) -> - let acc', (enf,alg,l') = aux acc l in - let l' = - if enf then Universe.make l - else l' - in acc', (d, l') :: left') - (acc, []) l - with Not_found -> acc, [] + let acc, left, lower = + try + let l = LMap.find u left in + let acc, left, newlow, lower = + List.fold_left + (fun (acc, left', newlow, lower') (d, l) -> + let acc', (enf,alg,l',lower) = aux acc l in + let l' = + if enf then Universe.make l + else l' + in acc', (d, l') :: left', + lower_add l d newlow, lower_union lower lower') + (acc, [], LMap.empty, LMap.empty) l + in + let not_lower (d,l) = + (* We're checking if (d,l) is already implied by the lower + constraints on some level u. If it represents l < u (d is Lt + or d is Le and i > 0, the i < 0 case is impossible due to + invariants of Univ), and the lower constraints only have l <= + u then it is not implied. *) + Univ.Universe.exists + (fun (l,i) -> + let d = + if i == 0 then d + else match d with + | Le -> Lt + | d -> d + in + try let d' = LMap.find l lower in + (* If d is stronger than the already implied lower + * constraints we must keep it. *) + compare_constraint_type d d' > 0 + with Not_found -> + (** No constraint existing on l *) true) l + in + let left = List.uniquize (List.filter not_lower left) in + (acc, left, LMap.union newlow lower) + with Not_found -> acc, [], LMap.empty and right = try Some (LMap.find u right) with Not_found -> None @@ -779,31 +846,33 @@ let minimize_univ_variables ctx us algs left right cstrs = let instantiate_lbound lbound = let alg = LSet.mem u algs in if alg then - (* u is algebraic: we instantiate it with it's lower bound, if any, + (* u is algebraic: we instantiate it with its lower bound, if any, or enforce the constraints if it is bounded from the top. *) - instantiate_with_lbound u lbound true false acc + let lower = remove_lower lbound lower in + instantiate_with_lbound u lbound lower true false acc else (* u is non algebraic *) match Universe.level lbound with | Some l -> (* The lowerbound is directly a level *) (* u is not algebraic but has no upper bounds, we instantiate it with its lower bound if it is a different level, otherwise we keep it. *) + let lower = LMap.remove l lower in if not (Level.equal l u) then (* Should check that u does not have upper constraints that are not already in right *) let acc' = remove_alg l acc in - instantiate_with_lbound u lbound false false acc' - else acc, (true, false, lbound) - | None -> - try - (* if right <> None then raise Not_found; *) - (* Another universe represents the same lower bound, - we can share them with no harm. *) - let can = find_inst insts lbound in - instantiate_with_lbound u (Universe.make can) false false acc + instantiate_with_lbound u lbound lower false false acc' + else acc, (true, false, lbound, lower) + | None -> + try + (* Another universe represents the same lower bound, + we can share them with no harm. *) + let can, lower = find_inst insts lbound in + let lower = LMap.remove can lower in + instantiate_with_lbound u (Universe.make can) lower false false acc with Not_found -> (* We set u as the canonical universe representing lbound *) - instantiate_with_lbound u lbound false true acc + instantiate_with_lbound u lbound lower false true acc in let acc' acc = match right with @@ -812,7 +881,7 @@ let minimize_univ_variables ctx us algs left right cstrs = let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in if List.is_empty dangling then acc else - let ((ctx', us, algs, insts, cstrs), (enf,_,inst as b)) = acc in + let ((ctx', us, algs, insts, cstrs), (enf,_,inst,lower as b)) = acc in let cstrs' = List.fold_left (fun cstrs (d, r) -> if d == Univ.Le then enforce_leq inst (Universe.make r) cstrs @@ -824,15 +893,15 @@ let minimize_univ_variables ctx us algs left right cstrs = in (ctx', us, algs, insts, cstrs'), b in - if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u)) + if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u, lower)) else let lbound = compute_lbound left in match lbound with | None -> (* Nothing to do *) - acc' (acc, (true, false, Universe.make u)) + acc' (acc, (true, false, Universe.make u, lower)) | Some lbound -> try acc' (instantiate_lbound lbound) - with Failure _ -> acc' (acc, (true, false, Universe.make u)) + with Failure _ -> acc' (acc, (true, false, Universe.make u, lower)) and aux (ctx', us, algs, seen, cstrs as acc) u = try acc, LMap.find u seen with Not_found -> instance acc u diff --git a/library/universes.mli b/library/universes.mli index a5740ec49f..d3a271b8d0 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -232,40 +232,6 @@ val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_s val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds -(* For tracing *) - -type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t - -val pr_constraints_map : constraints_map -> Pp.std_ppcmds - -val choose_canonical : universe_set -> (Level.t -> bool) (* flexibles *) -> universe_set -> universe_set -> - universe_level * (universe_set * universe_set * universe_set) - -val compute_lbound : (constraint_type * Univ.universe) list -> universe option - -val instantiate_with_lbound : - Univ.LMap.key -> - Univ.universe -> - bool -> - bool -> - Univ.LSet.t * Univ.universe option Univ.LMap.t * - Univ.LSet.t * - (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints -> - (Univ.LSet.t * Univ.universe option Univ.LMap.t * - Univ.LSet.t * - (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints) * - (bool * bool * Univ.universe) - -val minimize_univ_variables : - Univ.LSet.t -> - Univ.universe option Univ.LMap.t -> - Univ.LSet.t -> - constraints_map -> constraints_map -> - Univ.constraints -> - Univ.LSet.t * Univ.universe option Univ.LMap.t * - Univ.LSet.t * - (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints - (** {6 Support for old-style sort-polymorphism } *) val solve_constraints_system : universe option array -> universe array -> universe array -> diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index d6ba670d83..d0318fb5f6 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -263,8 +263,10 @@ let add_rewrite_hint bases ort t lcsr = let ctx = let ctx = UState.context_set ctx in if poly then ctx - else (Declare.declare_universe_context false ctx; - Univ.ContextSet.empty) + else (** This is a global universe context that shouldn't be + refreshed at every use of the hint, declare it globally. *) + (Declare.declare_universe_context false ctx; + Univ.ContextSet.empty) in Constrexpr_ops.constr_loc ce, (c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t in let eqs = List.map f lcsr in @@ -353,7 +355,7 @@ let refine_tac ist simple c = let expected_type = Pretyping.OfType concl in let c = Pretyping.type_uconstr ~flags ~expected_type ist c in let update = { run = fun sigma -> c.delayed env sigma } in - let refine = Refine.refine ~unsafe:false update in + let refine = Refine.refine ~unsafe:true update in if simple then refine else refine <*> Tactics.New.reduce_after_refine <*> diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 08e67a0c2f..52208979c4 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -875,6 +875,9 @@ let rec message_of_value v = Ftactic.return (pr_closed_glob_env (pf_env gl) (project gl) c) end } + else if has_type v (topwit wit_var) then + let id = out_gen (topwit wit_var) v in + Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (pr_id id) end } else match Value.to_list v with | Some l -> Ftactic.List.map message_of_value l >>= fun l -> diff --git a/parsing/cLexer.ml4 b/parsing/cLexer.ml4 index 181c4b7fd8..79771f3f66 100644 --- a/parsing/cLexer.ml4 +++ b/parsing/cLexer.ml4 @@ -69,6 +69,15 @@ let ttree_remove ttree str = in remove ttree 0 +let ttree_elements ttree = + let rec elts tt accu = + let accu = match tt.node with + | None -> accu + | Some s -> CString.Set.add s accu + in + CharMap.fold (fun _ tt accu -> elts tt accu) tt.branch accu + in + elts ttree CString.Set.empty (* Errors occurring while lexing (explained as "Lexer error: ...") *) @@ -101,14 +110,6 @@ module Error = struct end open Error -let current_file = ref "" - -let get_current_file () = - !current_file - -let set_current_file ~fname = - current_file := fname - let err loc str = Loc.raise (Compat.to_coqloc loc) (Error.E str) let bad_token str = raise (Error.E (Bad_token str)) @@ -120,11 +121,6 @@ type token_kind = | AsciiChar | EmptyStream -let error_unsupported_unicode_character loc n unicode cs = - let bp = Stream.count cs in - let loc = set_loc_pos loc bp (bp+n) in - err loc (UnsupportedUnicode unicode) - let error_utf8 loc cs = let bp = Stream.count cs in Stream.junk cs; (* consume the char to avoid read it and fail again *) @@ -174,14 +170,12 @@ let lookup_utf8_tail loc c cs = (Char.code c3 land 0x3F) lsl 6 + (Char.code c4 land 0x3F) | _ -> error_utf8 loc cs in - try Unicode.classify unicode, n - with Unicode.Unsupported -> - njunk n cs; error_unsupported_unicode_character loc n unicode cs + Utf8Token (Unicode.classify unicode, n) let lookup_utf8 loc cs = match Stream.peek cs with | Some ('\x00'..'\x7F') -> AsciiChar - | Some ('\x80'..'\xFF' as c) -> Utf8Token (lookup_utf8_tail loc c cs) + | Some ('\x80'..'\xFF' as c) -> lookup_utf8_tail loc c cs | None -> EmptyStream let unlocated f x = f x @@ -199,17 +193,6 @@ let check_keyword str = in loop_symb (Stream.of_string str) -let warn_unparsable_keyword = - CWarnings.create ~name:"unparsable-keyword" ~category:"parsing" - (fun (s,unicode) -> - strbrk (Printf.sprintf "Token '%s' contains unicode character 0x%x \ - which will not be parsable." s unicode)) - -let check_keyword_to_add s = - try check_keyword s - with Error.E (UnsupportedUnicode unicode) -> - warn_unparsable_keyword (s,unicode) - let check_ident str = let rec loop_id intail = parser | [< ' ('a'..'z' | 'A'..'Z' | '_'); s >] -> @@ -240,13 +223,15 @@ let is_keyword s = let add_keyword str = if not (is_keyword str) then begin - check_keyword_to_add str; + check_keyword str; token_tree := ttree_add !token_tree str end let remove_keyword str = token_tree := ttree_remove !token_tree str +let keywords () = ttree_elements !token_tree + (* Freeze and unfreeze the state of the lexer *) type frozen_t = ttree @@ -270,6 +255,12 @@ let get_buff len = String.sub !buff 0 len (* The classical lexer: idents, numbers, quoted strings, comments *) +let warn_unrecognized_unicode = + CWarnings.create ~name:"unrecognized-unicode" ~category:"parsing" + (fun (u,id) -> + strbrk (Printf.sprintf "Not considering unicode character \"%s\" of unknown \ + lexical status as part of identifier \"%s\"." u id)) + let rec ident_tail loc len = parser | [< ' ('a'..'z' | 'A'..'Z' | '0'..'9' | ''' | '_' as c); s >] -> ident_tail loc (store len c) s @@ -277,6 +268,10 @@ let rec ident_tail loc len = parser match lookup_utf8 loc s with | Utf8Token ((Unicode.IdentPart | Unicode.Letter), n) -> ident_tail loc (nstore n len s) s + | Utf8Token (Unicode.Unknown, n) -> + let id = get_buff len in + let u = String.concat "" (List.map (String.make 1) (Stream.npeek n s)) in + warn_unrecognized_unicode ~loc:!@loc (u,id); len | _ -> len let rec number len = parser @@ -334,6 +329,9 @@ let rec string loc ~comm_level bp len = parser (* Hook for exporting comment into xml theory files *) let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore () +(* To associate locations to a file name *) +let current_file = ref None + (* Utilities for comments in beautify *) let comment_begin = ref None let comm_loc bp = match !comment_begin with @@ -354,16 +352,20 @@ let rec split_comments comacc acc pos = function let extract_comments pos = split_comments [] [] pos !comments -type comments_state = int option * string * bool * ((int * int) * string) list -let restore_comments_state (o,s,b,c) = +(* The state of the lexer visible from outside *) +type lexer_state = int option * string * bool * ((int * int) * string) list * string option + +let init_lexer_state f = (None,"",true,[],f) +let set_lexer_state (o,s,b,c,f) = comment_begin := o; Buffer.clear current_comment; Buffer.add_string current_comment s; between_commands := b; - comments := c -let default_comments_state = (None,"",true,[]) -let comments_state () = - let s = (!comment_begin, Buffer.contents current_comment, !between_commands, !comments) in - restore_comments_state default_comments_state; s + comments := c; + current_file := f +let release_lexer_state () = + (!comment_begin, Buffer.contents current_comment, !between_commands, !comments, !current_file) +let drop_lexer_state () = + set_lexer_state (init_lexer_state None) let real_push_char c = Buffer.add_char current_comment c @@ -391,7 +393,7 @@ let comment_stop ep = if !Flags.xml_export && Buffer.length current_comment > 0 && (!between_commands || not(null_comment current_s)) then Hook.get f_xml_output_comment current_s; - (if Flags.do_beautify() && Buffer.length current_comment > 0 && + (if !Flags.beautify && Buffer.length current_comment > 0 && (!between_commands || not(null_comment current_s)) then let bp = match !comment_begin with Some bp -> bp @@ -408,7 +410,7 @@ let comment_stop ep = (* Does not unescape!!! *) let rec comm_string loc bp = parser - | [< ''"' >] ep -> push_string "\""; loc + | [< ''"' >] -> push_string "\""; loc | [< ''\\'; loc = (parser [< ' ('"' | '\\' as c) >] -> let () = match c with @@ -438,7 +440,7 @@ let rec comment loc bp = parser bp2 let loc = (* In beautify mode, the lexing differs between strings in comments and regular strings (e.g. escaping). It seems wrong. *) - if Flags.do_beautify() then (push_string"\""; comm_string loc bp2 s) + if !Flags.beautify then (push_string"\""; comm_string loc bp2 s) else fst (string loc ~comm_level:(Some 0) bp2 0 s) in comment loc bp s @@ -511,20 +513,19 @@ let process_chars loc bp c cs = let loc = set_loc_pos loc bp ep' in err loc Undefined_token -let token_of_special c s = match c with - | '.' -> FIELD s - | _ -> assert false +(* Parse what follows a dot *) -(* Parse what follows a dot / a dollar *) - -let parse_after_special loc c bp = +let parse_after_dot loc c bp = parser - | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail loc (store 0 d) >] -> - token_of_special c (get_buff len) + | [< ' ('a'..'z' | 'A'..'Z' | '_' as d); len = ident_tail loc (store 0 d); s >] -> + let field = get_buff len in + (try find_keyword loc ("."^field) s with Not_found -> FIELD field) | [< s >] -> match lookup_utf8 loc s with | Utf8Token (Unicode.Letter, n) -> - token_of_special c (get_buff (ident_tail loc (nstore n 0 s) s)) + let len = ident_tail loc (nstore n 0 s) s in + let field = get_buff len in + (try find_keyword loc ("."^field) s with Not_found -> FIELD field) | AsciiChar | Utf8Token _ | EmptyStream -> fst (process_chars loc bp c s) (* Parse what follows a question mark *) @@ -552,7 +553,7 @@ let rec next_token loc = parser bp comm_loc bp; push_char c; next_token (bump_loc_line loc ep) s | [< '' ' | '\t' | '\r' as c; s >] -> comm_loc bp; push_char c; next_token loc s - | [< ''.' as c; t = parse_after_special loc c bp; s >] ep -> + | [< ''.' as c; t = parse_after_dot loc c bp; s >] ep -> comment_stop bp; (* We enforce that "." should either be part of a larger keyword, for instance ".(", or followed by a blank or eof. *) @@ -572,7 +573,7 @@ let rec next_token loc = parser bp comment_stop bp; between_commands := new_between_commands; t | [< ''?'; s >] ep -> let t = parse_after_qmark loc bp s in - comment_stop bp; (t, set_loc_pos loc ep bp) + comment_stop bp; (t, set_loc_pos loc bp ep) | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail loc (store 0 c); s >] ep -> let id = get_buff len in @@ -592,6 +593,12 @@ let rec next_token loc = parser bp let loc = comment loc bp s in next_token loc s | [< t = process_chars loc bp c >] -> comment_stop bp; t >] -> t + | [< ' ('{' | '}' as c); s >] ep -> + let t,new_between_commands = + if !between_commands then (KEYWORD (String.make 1 c), set_loc_pos loc bp ep), true + else process_chars loc bp c s, false + in + comment_stop bp; between_commands := new_between_commands; t | [< s >] -> match lookup_utf8 loc s with | Utf8Token (Unicode.Letter, n) -> @@ -600,11 +607,9 @@ let rec next_token loc = parser bp let ep = Stream.count s in comment_stop bp; (try find_keyword loc id s with Not_found -> IDENT id), set_loc_pos loc bp ep - | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart), _) -> + | AsciiChar | Utf8Token ((Unicode.Symbol | Unicode.IdentPart | Unicode.Unknown), _) -> let t = process_chars loc bp (Stream.next s) s in - let new_between_commands = match t with - (KEYWORD ("{"|"}"),_) -> !between_commands | _ -> false in - comment_stop bp; between_commands := new_between_commands; t + comment_stop bp; t | EmptyStream -> comment_stop bp; (EOI, set_loc_pos loc bp (bp+1)) @@ -626,12 +631,6 @@ let loct_func loct i = let loct_add loct i loc = Hashtbl.add loct i loc -let current_location_table = ref (loct_create ()) - -type location_table = (int, Compat.CompatLoc.t) Hashtbl.t -let location_table () = !current_location_table -let restore_location_table t = current_location_table := t - (** {6 The lexer of Coq} *) (** Note: removing a token. @@ -669,7 +668,6 @@ let func cs = cur_loc := Compat.after loc; loct_add loct i loc; Some tok) in - current_location_table := loct; (ts, loct_func loct) let lexer = { @@ -706,7 +704,6 @@ end let mk () = let loct = loct_create () in let cur_loc = ref (Compat.make_loc !current_file 1 0 0 0) in - current_location_table := loct; let rec self init_loc (* FIXME *) = parser i [< (tok, loc) = next_token !cur_loc; s >] -> diff --git a/parsing/cLexer.mli b/parsing/cLexer.mli index 3ad49eb74a..e0fdf8cb55 100644 --- a/parsing/cLexer.mli +++ b/parsing/cLexer.mli @@ -9,22 +9,7 @@ val add_keyword : string -> unit val remove_keyword : string -> unit val is_keyword : string -> bool - -(* val location_function : int -> Loc.t *) - -(** for coqdoc *) -type location_table -val location_table : unit -> location_table -val restore_location_table : location_table -> unit - - -(** [get_current_file fname] returns the filename used in locations emitted by - the lexer *) -val get_current_file : unit -> string - -(** [set_current_file fname] sets the filename used in locations emitted by the - lexer *) -val set_current_file : fname:string -> unit +val keywords : unit -> CString.Set.t val check_ident : string -> unit val is_ident : string -> bool diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index ecf515111c..befa0d01ba 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -10,6 +10,10 @@ (** Locations *) +let file_loc_of_file = function +| None -> "" +| Some f -> f + IFDEF CAMLP5 THEN module CompatLoc = struct @@ -29,7 +33,7 @@ let to_coqloc loc = Loc.line_nb_last = Ploc.line_nb_last loc; Loc.bol_pos_last = Ploc.bol_pos_last loc; } -let make_loc fname line_nb bol_pos bp ep = Ploc.make_loc fname line_nb bol_pos (bp, ep) "" +let make_loc fname line_nb bol_pos bp ep = Ploc.make_loc (file_loc_of_file fname) line_nb bol_pos (bp, ep) "" (* Update a loc without allocating an intermediate pair *) let set_loc_pos loc bp ep = @@ -80,7 +84,7 @@ let to_coqloc loc = Loc.bol_pos_last = CompatLoc.stop_bol loc; } let make_loc fname line_nb bol_pos start stop = - CompatLoc.of_tuple (fname, line_nb, bol_pos, start, line_nb, bol_pos, stop, false) + CompatLoc.of_tuple (file_loc_of_file fname, line_nb, bol_pos, start, line_nb, bol_pos, stop, false) open CompatLoc @@ -97,7 +101,7 @@ let bump_loc_line_last loc bol_pos = stop_line loc + 1, bol_pos, stop_off loc, is_ghost loc) let set_loc_file loc fname = - of_tuple (fname, start_line loc, start_bol loc, start_off loc, + of_tuple (file_loc_of_file fname, start_line loc, start_bol loc, start_off loc, stop_line loc, stop_bol loc, stop_off loc, is_ghost loc) let after loc = @@ -138,20 +142,22 @@ module type LexerSig = sig exception E of t val to_string : t -> string end - type comments_state - val default_comments_state : comments_state - val comments_state : unit -> comments_state - val restore_comments_state : comments_state -> unit + type lexer_state + val init_lexer_state : string option -> lexer_state + val set_lexer_state : lexer_state -> unit + val release_lexer_state : unit -> lexer_state + val drop_lexer_state : unit -> unit end ELSE module type LexerSig = sig include Camlp4.Sig.Lexer with module Loc = CompatLoc and type Token.t = Tok.t - type comments_state - val default_comments_state : comments_state - val comments_state : unit -> comments_state - val restore_comments_state : comments_state -> unit + type lexer_state + val init_lexer_state : string option -> lexer_state + val set_lexer_state : lexer_state -> unit + val release_lexer_state : unit -> lexer_state + val drop_lexer_state : unit -> unit end END @@ -172,7 +178,7 @@ module type GrammarSig = sig type extend_statment = Gramext.position option * single_extend_statment list type coq_parsable - val parsable : char Stream.t -> coq_parsable + val parsable : ?file:string -> char Stream.t -> coq_parsable val action : 'a -> action val entry_create : string -> 'a entry val entry_parse : 'a entry -> coq_parsable -> 'a @@ -193,32 +199,34 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct string option * Gramext.g_assoc option * production_rule list type extend_statment = Gramext.position option * single_extend_statment list - type coq_parsable = parsable * L.comments_state ref - let parsable c = - let state = ref L.default_comments_state in (parsable c, state) + type coq_parsable = parsable * L.lexer_state ref + let parsable ?file c = + let state = ref (L.init_lexer_state file) in + L.set_lexer_state !state; + let a = parsable c in + state := L.release_lexer_state (); + (a,state) let action = Gramext.action let entry_create = Entry.create let entry_parse e (p,state) = - L.restore_comments_state !state; + L.set_lexer_state !state; try let c = Entry.parse e p in - state := L.comments_state (); - L.restore_comments_state L.default_comments_state; + state := L.release_lexer_state (); c with Exc_located (loc,e) -> - L.restore_comments_state L.default_comments_state; + L.drop_lexer_state (); let loc' = Loc.get_loc (Exninfo.info e) in let loc = match loc' with None -> to_coqloc loc | Some loc -> loc in Loc.raise loc e let with_parsable (p,state) f x = - L.restore_comments_state !state; + L.set_lexer_state !state; try let a = f x in - state := L.comments_state (); - L.restore_comments_state L.default_comments_state; + state := L.release_lexer_state (); a with e -> - L.restore_comments_state L.default_comments_state; + L.drop_lexer_state (); raise e let entry_print ft x = Entry.print ft x @@ -234,7 +242,7 @@ module type GrammarSig = sig type 'a entry = 'a Entry.t type action = Action.t type coq_parsable - val parsable : char Stream.t -> coq_parsable + val parsable : ?file:string -> char Stream.t -> coq_parsable val action : 'a -> action val entry_create : string -> 'a entry val entry_parse : 'a entry -> coq_parsable -> 'a @@ -249,31 +257,28 @@ module GrammarMake (L:LexerSig) : GrammarSig = struct include Camlp4.Struct.Grammar.Static.Make (L) type 'a entry = 'a Entry.t type action = Action.t - type comments_state = int option * string * bool * ((int * int) * string) list - type coq_parsable = char Stream.t * L.comments_state ref - let parsable s = let state = ref L.default_comments_state in (s, state) + type coq_parsable = char Stream.t * L.lexer_state ref + let parsable ?file s = let state = ref (L.init_lexer_state file) in (s, state) let action = Action.mk let entry_create = Entry.mk let entry_parse e (s,state) = - L.restore_comments_state !state; + L.set_lexer_state !state; try let c = parse e (*FIXME*)CompatLoc.ghost s in - state := L.comments_state (); - L.restore_comments_state L.default_comments_state; + state := L.release_lexer_state (); c with Exc_located (loc,e) -> - L.restore_comments_state L.default_comments_state; - raise_coq_loc loc e + L.drop_lexer_state (); + raise_coq_loc loc e;; let with_parsable (p,state) f x = - L.restore_comments_state !state; + L.set_lexer_state !state; try let a = f x in - state := L.comments_state (); - L.restore_comments_state L.default_comments_state; + state := L.release_lexer_state (); a with e -> - L.restore_comments_state L.default_comments_state; - raise e + L.drop_lexer_state (); + Pervasives.raise e;; let entry_print ft x = Entry.print ft x let srules' = srules (entry_create "dummy") end diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index 8874afef33..e43c47d050 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -142,7 +142,8 @@ let rec json_expr env = function ("what", json_str "fix:item"); ("name", json_id fi); ("body", json_function env' ti) - ]) (Array.map2 (fun a b -> a,b) ids' defs))) + ]) (Array.map2 (fun a b -> a,b) ids' defs))); + ("for", json_int i); ] | MLexn s -> json_dict [ ("what", json_str "expr:exception"); diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 62f3071151..fa84e4ddf3 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1538,7 +1538,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num begin if do_observe () then Feedback.msg_debug (str "Cannot create equation Lemma " ++ CErrors.print e) - else anomaly (Pp.str "Cannot create equation Lemma") + else CErrors.errorlabstrm "Cannot create equation Lemma" + (str "Cannot create equation lemma." ++ spc () ++ + str "This may be because the function is nested-recursive.") ; true end diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index a34fa4cae7..41eb5826b0 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -908,9 +908,47 @@ let glob_ssrterm gs = function fst x, Some c | ct -> ct +(* This piece of code asserts the following notations are reserved *) +(* Reserved Notation "( a 'in' b )" (at level 0). *) +(* Reserved Notation "( a 'as' b )" (at level 0). *) +(* Reserved Notation "( a 'in' b 'in' c )" (at level 0). *) +(* Reserved Notation "( a 'as' b 'in' c )" (at level 0). *) +let glob_cpattern gs p = + pp(lazy(str"globbing pattern: " ++ pr_term p)); + let glob x = snd (glob_ssrterm gs (mk_lterm x)) in + let encode k s l = + let name = Name (id_of_string ("_ssrpat_" ^ s)) in + k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None) in + let bind_in t1 t2 = + let d = dummy_loc in let n = Name (destCVar t1) in + fst (glob (mkCCast d (mkCHole d) (mkCLambda d n (mkCHole d) t2))) in + let check_var t2 = if not (isCVar t2) then + loc_error (constr_loc t2) "Only identifiers are allowed here" in + match p with + | _, (_, None) as x -> x + | k, (v, Some t) as orig -> + if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else + match t with + | CNotation(_, "( _ in _ )", ([t1; t2], [], [])) -> + (try match glob t1, glob t2 with + | (r1, None), (r2, None) -> encode k "In" [r1;r2] + | (r1, Some _), (r2, Some _) when isCVar t1 -> + encode k "In" [r1; r2; bind_in t1 t2] + | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] + | _ -> CErrors.anomaly (str"where are we?") + with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) + | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) -> + check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] + | CNotation(_, "( _ as _ )", ([t1; t2], [], [])) -> + encode k "As" [fst (glob t1); fst (glob t2)] + | CNotation(_, "( _ as _ in _ )", ([t1; t2; t3], [], [])) -> + check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] + | _ -> glob_ssrterm gs orig +;; + let glob_rpattern s p = match p with - | T t -> T (glob_ssrterm s t) + | T t -> T (glob_cpattern s t) | In_T t -> In_T (glob_ssrterm s t) | X_In_T(x,t) -> X_In_T (x,glob_ssrterm s t) | In_X_In_T(x,t) -> In_X_In_T (x,glob_ssrterm s t) @@ -995,44 +1033,6 @@ let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with | _ -> ' ' let ssrtermkind = Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind -(* This piece of code asserts the following notations are reserved *) -(* Reserved Notation "( a 'in' b )" (at level 0). *) -(* Reserved Notation "( a 'as' b )" (at level 0). *) -(* Reserved Notation "( a 'in' b 'in' c )" (at level 0). *) -(* Reserved Notation "( a 'as' b 'in' c )" (at level 0). *) -let glob_cpattern gs p = - pp(lazy(str"globbing pattern: " ++ pr_term p)); - let glob x = snd (glob_ssrterm gs (mk_lterm x)) in - let encode k s l = - let name = Name (id_of_string ("_ssrpat_" ^ s)) in - k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None) in - let bind_in t1 t2 = - let d = dummy_loc in let n = Name (destCVar t1) in - fst (glob (mkCCast d (mkCHole d) (mkCLambda d n (mkCHole d) t2))) in - let check_var t2 = if not (isCVar t2) then - loc_error (constr_loc t2) "Only identifiers are allowed here" in - match p with - | _, (_, None) as x -> x - | k, (v, Some t) as orig -> - if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else - match t with - | CNotation(_, "( _ in _ )", ([t1; t2], [], [])) -> - (try match glob t1, glob t2 with - | (r1, None), (r2, None) -> encode k "In" [r1;r2] - | (r1, Some _), (r2, Some _) when isCVar t1 -> - encode k "In" [r1; r2; bind_in t1 t2] - | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] - | _ -> CErrors.anomaly (str"where are we?") - with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) - | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) -> - check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] - | CNotation(_, "( _ as _ )", ([t1; t2], [], [])) -> - encode k "As" [fst (glob t1); fst (glob t2)] - | CNotation(_, "( _ as _ in _ )", ([t1; t2; t3], [], [])) -> - check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] - | _ -> glob_ssrterm gs orig -;; - let interp_ssrterm _ gl t = Tacmach.project gl, t ARGUMENT EXTEND cpattern diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 0ac34b7186..5c9ce2624c 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -62,13 +62,14 @@ let error_wrong_numarg_constructor_loc loc env c n = let error_wrong_numarg_inductive_loc loc env c n = raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargInductive(c,n)) -let rec list_try_compile f = function - | [a] -> f a - | [] -> anomaly (str "try_find_f") +let list_try_compile f l = + let rec aux errors = function + | [] -> if errors = [] then anomaly (str "try_find_f") else raise (List.last errors) | h::t -> try f h - with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ -> - list_try_compile f t + with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e -> + aux (e::errors) t in + aux [] l let force_name = let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b7e0535dad..28600ad153 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -97,19 +97,19 @@ let position_problem l2r = function | CONV -> None | CUMUL -> Some l2r -let occur_rigidly ev evd t = +let occur_rigidly (evk,_ as ev) evd t = let rec aux t = match kind_of_term (whd_evar evd t) with | App (f, c) -> if aux f then Array.exists aux c else false | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true | Proj (p, c) -> not (aux c) - | Evar (ev',_) -> if Evar.equal ev ev' then raise Occur else false + | Evar (evk',_) -> if Evar.equal evk evk' then raise Occur else false | Cast (p, _, _) -> aux p | Lambda _ | LetIn _ -> false | Const _ -> false | Prod (_, b, t) -> ignore(aux b || aux t); true | Rel _ | Var _ -> false - | Case _ -> false + | Case (_,_,c,_) -> if eq_constr (mkEvar ev) c then raise Occur else false in try ignore(aux t); false with Occur -> true (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose @@ -478,7 +478,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [eta;(* Postpone the use of an heuristic *) (fun i -> - if not (occur_rigidly (fst ev) i tR) then + if not (occur_rigidly ev i tR) then let i,tF = if isRel tR || isVar tR then (* Optimization so as to generate candidates *) @@ -1147,7 +1147,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in Success (solve_refl ~can_drop:true f env evd (position_problem true pbty) evk1 args1 args2) - | Evar ev1, Evar ev2 -> + | Evar ev1, Evar ev2 when app_empty -> Success (solve_evar_evar ~force:true (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd (position_problem true pbty) ev1 ev2) @@ -1175,9 +1175,14 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = (* Some head evar have been instantiated, or unknown kind of problem *) evar_conv_x ts env evd pbty t1 t2 +let error_cannot_unify env evd pb ?reason t1 t2 = + Pretype_errors.error_cannot_unify_loc + (loc_of_conv_pb evd pb) env + evd ?reason (t1, t2) + let check_problems_are_solved env evd = match snd (extract_all_conv_pbs evd) with - | (pbty,env,t1,t2)::_ -> Pretype_errors.error_cannot_unify env evd (t1, t2) + | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2 | _ -> () let max_undefined_with_candidates evd = @@ -1246,17 +1251,15 @@ let consider_remaining_unif_problems env aux evd pbs progress (pb :: stuck) end | UnifFailure (evd,reason) -> - Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) - env evd ~reason (t1, t2)) + error_cannot_unify env evd pb ~reason t1 t2) | _ -> if progress then aux evd stuck false [] else match stuck with | [] -> (* We're finished *) evd | (pbty,env,t1,t2 as pb) :: _ -> - (* There remains stuck problems *) - Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb) - env evd (t1, t2) + (* There remains stuck problems *) + error_cannot_unify env evd pb t1 t2 in let (evd,pbs) = extract_all_conv_pbs evd in let heuristic_solved_evd = aux evd pbs false [] in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index a97e248aee..f1526faccc 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -613,7 +613,13 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si * substitution u1..uq. *) +exception MorePreciseOccurCheckNeeeded + let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = + if Evd.is_defined evd evk1 then + (* Some circularity somewhere (see e.g. #3209) *) + raise MorePreciseOccurCheckNeeeded; + let (evk1,args1) = destEvar (whd_evar evd (mkEvar (evk1,args1))) in let evi1 = Evd.find_undefined evd evk1 in let env1,rel_sign = env_rel_context_chop k env in let sign1 = evar_hyps evi1 in @@ -1553,6 +1559,8 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = postpone_non_unique_projection env evd pbty ev sols rhs | NotEnoughInformationEvarEvar t -> add_conv_oriented_pb (pbty,env,mkEvar ev,t) evd + | MorePreciseOccurCheckNeeeded -> + add_conv_oriented_pb (pbty,env,mkEvar ev,rhs) evd | NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e -> raise e | OccurCheckIn (evd,rhs) -> @@ -1591,8 +1599,6 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = * ass. *) -(* This criterion relies on the fact that we postpone only problems of the form: -?x [?x1 ... ?xn] = t or the symmetric case. *) let status_changed lev (pbty,_,t1,t2) = (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) || (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 48bf9149d0..6afa55862f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -249,17 +249,24 @@ type inference_flags = { expand_evars : bool } -let frozen_holes (sigma, sigma') = - (); fun ev -> Evar.Map.mem ev (Evd.undefined_map sigma) - -let pending_holes (sigma, sigma') = - let fold evk _ accu = - if not (Evd.mem sigma evk) then Evar.Set.add evk accu else accu - in - Evd.fold_undefined fold sigma' Evar.Set.empty +(* Compute the set of still-undefined initial evars up to restriction + (e.g. clearing) and the set of yet-unsolved evars freshly created + in the extension [sigma'] of [sigma] (excluding the restrictions of + the undefined evars of [sigma] to be freshly created evars of + [sigma']). Otherwise said, we partition the undefined evars of + [sigma'] into those already in [sigma] or deriving from an evar in + [sigma] by restriction, and the evars properly created in [sigma'] *) + +let frozen_and_pending_holes (sigma, sigma') = + let add_derivative_of evk evi acc = + match advance sigma' evk with None -> acc | Some evk' -> Evar.Set.add evk' acc in + let frozen = Evd.fold_undefined add_derivative_of sigma Evar.Set.empty in + let fold evk _ accu = if not (Evar.Set.mem evk frozen) then Evar.Set.add evk accu else accu in + let pending = Evd.fold_undefined fold sigma' Evar.Set.empty in + (frozen,pending) let apply_typeclasses env evdref frozen fail_evar = - let filter_frozen = frozen in + let filter_frozen evk = Evar.Set.mem evk frozen in evdref := Typeclasses.resolve_typeclasses ~filter:(if Flags.is_program_mode () then (fun evk evi -> Typeclasses.no_goals_or_obligations evk evi && not (filter_frozen evk)) @@ -327,8 +334,7 @@ let check_evars_are_solved env current_sigma frozen pending = (* Try typeclasses, hooks, unification heuristics ... *) let solve_remaining_evars flags env current_sigma pending = - let frozen = frozen_holes pending in - let pending = pending_holes pending in + let frozen,pending = frozen_and_pending_holes pending in let evdref = ref current_sigma in if flags.use_typeclasses then apply_typeclasses env evdref frozen false; if Option.has_some flags.use_hook then @@ -338,8 +344,7 @@ let solve_remaining_evars flags env current_sigma pending = !evdref let check_evars_are_solved env current_sigma pending = - let frozen = frozen_holes pending in - let pending = pending_holes pending in + let frozen,pending = frozen_and_pending_holes pending in check_evars_are_solved env current_sigma frozen pending let process_inference_flags flags env initial_sigma (sigma,c) = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 531b615539..e0a81cfbb9 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1269,7 +1269,8 @@ let solve_simple_evar_eqn ts env evd ev rhs = match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with | UnifFailure (evd,reason) -> error_cannot_unify env evd ~reason (mkEvar ev,rhs); - | Success evd -> evd + | Success evd -> + Evarconv.consider_remaining_unif_problems env evd (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index c94650f1ee..aa94fb7be3 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -129,7 +129,7 @@ end) = struct str "`" ++ str hd ++ c ++ str tl let pr_com_at n = - if Flags.do_beautify() && not (Int.equal n 0) then comment (CLexer.extract_comments n) + if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n) else mt() let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp) diff --git a/printing/pputils.ml b/printing/pputils.ml index 57a1d957e0..50ce56fb02 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -9,7 +9,7 @@ open Pp let pr_located pr (loc, x) = - if Flags.do_beautify () && loc <> Loc.ghost then + if !Flags.beautify && loc <> Loc.ghost then let (b, e) = Loc.unloc loc in (* Side-effect: order matters *) let before = Pp.comment (CLexer.extract_comments b) in diff --git a/printing/printer.ml b/printing/printer.ml index 6d54a5b3d5..608bca62ac 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -424,7 +424,16 @@ let pr_evgl_sign sigma evi = (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") in let pc = pr_lconstr_env env sigma evi.evar_concl in - hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++ spc () ++ warn) + let candidates = + match evi.evar_body, evi.evar_candidates with + | Evar_empty, Some l -> + spc () ++ str "= {" ++ + prlist_with_sep (fun () -> str "|") (pr_lconstr_env env sigma) l ++ str "}" + | _ -> + mt () + in + hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++ + candidates ++ spc () ++ warn) (* Print an existential variable *) @@ -471,7 +480,7 @@ let default_pr_subgoal n sigma = let pr_internal_existential_key ev = str (string_of_existential ev) -let print_evar_constraints gl sigma cstrs = +let print_evar_constraints gl sigma = let pr_env = match gl with | None -> fun e' -> pr_context_of e' sigma @@ -487,6 +496,14 @@ let print_evar_constraints gl sigma cstrs = let pr_evconstr (pbty,env,t1,t2) = let t1 = Evarutil.nf_evar sigma t1 and t2 = Evarutil.nf_evar sigma t2 in + let env = + (** We currently allow evar instances to refer to anonymous de Bruijn + indices, so we protect the error printing code in this case by giving + names to every de Bruijn variable in the rel_context of the conversion + problem. MS: we should rather stop depending on anonymous variables, they + can be used to indicate independency. Also, this depends on a strategy for + naming/renaming *) + Namegen.make_all_name_different env in str" " ++ hov 2 (pr_env env ++ pr_lconstr_env env sigma t1 ++ spc () ++ str (match pbty with @@ -494,7 +511,23 @@ let print_evar_constraints gl sigma cstrs = | Reduction.CUMUL -> "<=") ++ spc () ++ pr_lconstr_env env sigma t2) in - prlist_with_sep fnl pr_evconstr cstrs + let pr_candidate ev evi (candidates,acc) = + if Option.has_some evi.evar_candidates then + (succ candidates, acc ++ pr_evar sigma (ev,evi) ++ fnl ()) + else (candidates, acc) + in + let constraints = + let _, cstrs = Evd.extract_all_conv_pbs sigma in + if List.is_empty cstrs then mt () + else fnl () ++ str (String.plural (List.length cstrs) "unification constraint") + ++ str":" ++ fnl () ++ hov 0 (prlist_with_sep fnl pr_evconstr cstrs) + in + let candidates, ppcandidates = Evd.fold_undefined pr_candidate sigma (0,mt ()) in + constraints ++ + if candidates > 0 then + fnl () ++ str (String.plural candidates "existential") ++ + str" with candidates:" ++ fnl () ++ hov 0 ppcandidates + else mt () let should_print_dependent_evars = ref true @@ -509,12 +542,7 @@ let _ = optwrite = (fun v -> should_print_dependent_evars := v) } let print_dependent_evars gl sigma seeds = - let constraints = - let _, cstrs = Evd.extract_all_conv_pbs sigma in - if List.is_empty cstrs then mt () - else fnl () ++ str (String.plural (List.length cstrs) "unification constraint") - ++ str":" ++ fnl () ++ hov 0 (print_evar_constraints gl sigma cstrs) - in + let constraints = print_evar_constraints gl sigma in let evars () = if !should_print_dependent_evars then let evars = Evarutil.gather_dependent_evars sigma seeds in diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml index ce12185cba..8162fc3bb5 100644 --- a/stm/proofBlockDelimiter.ml +++ b/stm/proofBlockDelimiter.ml @@ -83,7 +83,7 @@ let static_bullet ({ entry_point; prev_node } as view) = if node.indentation > base then `Cont node else match node.ast with | Vernacexpr.VernacBullet b' when b = b' -> - `Found { stop = entry_point.id; start = prev.id; + `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = of_bullet_val b } | _ -> `Stop) entry_point | _ -> assert false @@ -108,7 +108,7 @@ let static_curly_brace ({ entry_point; prev_node } as view) = crawl view (fun (nesting,prev) node -> match node.ast with | Vernacexpr.VernacSubproof _ when nesting = 0 -> - `Found { stop = entry_point.id; start = prev.id; + `Found { block_stop = entry_point.id; block_start = prev.id; dynamic_switch = node.id; carry_on_data = unit_val } | Vernacexpr.VernacSubproof _ -> `Cont (nesting - 1,node) @@ -135,7 +135,7 @@ let static_par { entry_point; prev_node } = match prev_node entry_point with | None -> None | Some { id = pid } -> - Some { stop = entry_point.id; start = pid; + Some { block_stop = entry_point.id; block_start = pid; dynamic_switch = pid; carry_on_data = unit_val } let dynamic_par { dynamic_switch = id } = @@ -162,7 +162,7 @@ let static_indent ({ entry_point; prev_node } as view) = crawl view ~init:(Some last_tac) (fun prev node -> if node.indentation >= last_tac.indentation then `Cont node else - `Found { stop = entry_point.id; start = node.id; + `Found { block_stop = entry_point.id; block_start = node.id; dynamic_switch = node.id; carry_on_data = of_vernac_expr_val entry_point.ast } ) last_tac diff --git a/stm/stm.ml b/stm/stm.ml index bb4f5f72f3..e387e6322f 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -256,8 +256,8 @@ and pt = { (* TODO: inline records in OCaml 4.03 *) qed : Stateid.t; } and static_block_declaration = { - start : Stateid.t; - stop : Stateid.t; + block_start : Stateid.t; + block_stop : Stateid.t; dynamic_switch : Stateid.t; carry_on_data : DynBlockData.t; } @@ -362,10 +362,10 @@ module VCS : sig val get_state : id -> cached_state (* cuts from start -> stop, raising Expired if some nodes are not there *) - val slice : start:id -> stop:id -> vcs - val nodes_in_slice : start:id -> stop:id -> Stateid.t list + val slice : block_start:id -> block_stop:id -> vcs + val nodes_in_slice : block_start:id -> block_stop:id -> Stateid.t list - val create_proof_task_box : id list -> qed:id -> start:id -> unit + val create_proof_task_box : id list -> qed:id -> block_start:id -> unit val create_proof_block : static_block_declaration -> string -> unit val box_of : id -> box list val delete_boxes_of : id -> unit @@ -582,20 +582,20 @@ end = struct (* {{{ *) let visit id = Vcs_aux.visit !vcs id - let nodes_in_slice ~start ~stop = + let nodes_in_slice ~block_start ~block_stop = let rec aux id = - if Stateid.equal id start then [] else + if Stateid.equal id block_start then [] else match visit id with | { next = n; step = `Cmd x } -> (id,Cmd x) :: aux n | { next = n; step = `Alias x } -> (id,Alias x) :: aux n | { next = n; step = `Sideff (`Ast (x,_)) } -> (id,Sideff (Some x)) :: aux n - | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string start ^ - " to "^Stateid.to_string stop)) - in aux stop + | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string block_start ^ + " to "^Stateid.to_string block_stop)) + in aux block_stop - let slice ~start ~stop = - let l = nodes_in_slice ~start ~stop in + let slice ~block_start ~block_stop = + let l = nodes_in_slice ~block_start ~block_stop in let copy_info v id = Vcs_.set_info v id { (get_info id) with state = Empty; vcs_backup = None,None } in @@ -611,27 +611,27 @@ end = struct (* {{{ *) (Stateid.Set.elements (Vcs_.Dag.Property.having_it p)) (Vcs_.Dag.Property.data p)) v props in - let v = Vcs_.empty start in - let v = copy_info v start in + let v = Vcs_.empty block_start in + let v = copy_info v block_start in let v = List.fold_right (fun (id,tr) v -> let v = Vcs_.commit v id tr in let v = copy_info v id in v) l v in (* Stm should have reached the beginning of proof *) - assert (match (get_info start).state with Valid _ -> true | _ -> false); + assert (match (get_info block_start).state with Valid _ -> true | _ -> false); (* We put in the new dag the most recent state known to master *) let rec fill id = match (get_info id).state with | Empty | Error _ -> fill (Vcs_aux.visit v id).next | Valid _ -> copy_info_w_state v id in - let v = fill stop in + let v = fill block_stop in (* We put in the new dag the first state (since Qed shall run on it, * see check_task_aux) *) - let v = copy_info_w_state v start in + let v = copy_info_w_state v block_start in copy_proof_blockes v - let nodes_in_slice ~start ~stop = - List.rev (List.map fst (nodes_in_slice ~start ~stop)) + let nodes_in_slice ~block_start ~block_stop = + List.rev (List.map fst (nodes_in_slice ~block_start ~block_stop)) let topo_invariant l = let all = List.fold_right Stateid.Set.add l Stateid.Set.empty in @@ -642,11 +642,11 @@ end = struct (* {{{ *) List.for_all (fun s -> Stateid.Set.(subset s all || subset all s)) sets) l - let create_proof_task_box l ~qed ~start:lemma = + let create_proof_task_box l ~qed ~block_start:lemma = if not (topo_invariant l) then anomaly (str "overlapping boxes"); vcs := create_property !vcs l (ProofTask { qed; lemma }) - let create_proof_block ({ start; stop} as decl) name = - let l = nodes_in_slice ~start ~stop in + let create_proof_block ({ block_start; block_stop} as decl) name = + let l = nodes_in_slice ~block_start ~block_stop in if not (topo_invariant l) then anomaly (str "overlapping boxes"); vcs := create_property !vcs l (ProofBlock (decl, name)) let box_of id = List.map Dag.Property.data (property_of !vcs id) @@ -746,7 +746,7 @@ module State : sig val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool - val exn_on : Stateid.t -> ?valid:Stateid.t -> iexn -> iexn + val exn_on : Stateid.t -> valid:Stateid.t -> iexn -> iexn (* to send states across worker/master *) type frozen_state val get_cached : Stateid.t -> frozen_state @@ -854,14 +854,14 @@ end = struct (* {{{ *) VCS.set_state id (Valid s) with VCS.Expired -> () - let exn_on id ?valid (e, info) = + let exn_on id ~valid (e, info) = match Stateid.get info with | Some _ -> (e, info) | None -> let loc = Option.default Loc.ghost (Loc.get_loc info) in let (e, info) = Hooks.(call_process_error_once (e, info)) in Hooks.(call execution_error id loc (iprint (e, info))); - (e, Stateid.add info ?valid id) + (e, Stateid.add info ~valid id) let same_env { system = s1 } { system = s2 } = let s1 = States.summary_of_state s1 in @@ -1139,7 +1139,7 @@ let detect_proof_block id name = let static, _ = List.assoc name !proof_block_delimiters in begin match static { prev_node; entry_point } with | None -> () - | Some ({ start; stop } as decl) -> + | Some ({ block_start; block_stop } as decl) -> VCS.create_proof_block decl name end with Not_found -> @@ -1251,7 +1251,7 @@ end = struct (* {{{ *) try Some (ReqBuildProof ({ Stateid.exn_info = t_exn_info; stop = t_stop; - document = VCS.slice ~start:t_start ~stop:t_stop; + document = VCS.slice ~block_start:t_start ~block_stop:t_stop; loc = t_loc; uuid = t_uuid; name = t_name }, t_drop, t_states)) @@ -1401,7 +1401,7 @@ and Slaves : sig (* (eventually) remote calls *) val build_proof : loc:Loc.t -> drop_pt:bool -> - exn_info:(Stateid.t * Stateid.t) -> start:Stateid.t -> stop:Stateid.t -> + exn_info:(Stateid.t * Stateid.t) -> block_start:Stateid.t -> block_stop:Stateid.t -> name:string -> future_proof * cancel_switch (* blocking function that waits for the task queue to be empty *) @@ -1560,7 +1560,7 @@ end = struct (* {{{ *) BuildProof { t_states = s2 } -> overlap_rel s1 s2 | _ -> 0) - let build_proof ~loc ~drop_pt ~exn_info ~start ~stop ~name:pname = + let build_proof ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name:pname = let id, valid as t_exn_info = exn_info in let cancel_switch = ref false in if TaskQueue.n_workers (Option.get !queue) = 0 then @@ -1569,21 +1569,21 @@ end = struct (* {{{ *) Future.create_delegate ~blocking:true ~name:pname (State.exn_on id ~valid) in let t_uuid = Future.uuid f in let task = ProofTask.(BuildProof { - t_exn_info; t_start = start; t_stop = stop; t_drop = drop_pt; + t_exn_info; t_start = block_start; t_stop = block_stop; t_drop = drop_pt; t_assign = assign; t_loc = loc; t_uuid; t_name = pname; - t_states = VCS.nodes_in_slice ~start ~stop }) in + t_states = VCS.nodes_in_slice ~block_start ~block_stop }) in TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch); f, cancel_switch end else - ProofTask.build_proof_here ~drop_pt t_exn_info loc stop, cancel_switch + ProofTask.build_proof_here ~drop_pt t_exn_info loc block_stop, cancel_switch else let f, t_assign = Future.create_delegate ~name:pname (State.exn_on id ~valid) in let t_uuid = Future.uuid f in feedback (InProgress 1); let task = ProofTask.(BuildProof { - t_exn_info; t_start = start; t_stop = stop; t_assign; t_drop = drop_pt; + t_exn_info; t_start = block_start; t_stop = block_stop; t_assign; t_drop = drop_pt; t_loc = loc; t_uuid; t_name = pname; - t_states = VCS.nodes_in_slice ~start ~stop }) in + t_states = VCS.nodes_in_slice ~block_start ~block_stop }) in TaskQueue.enqueue_task (Option.get !queue) (task,cancel_switch); f, cancel_switch @@ -1665,7 +1665,7 @@ end = struct (* {{{ *) r_state_fb = t_state_fb; r_document = if age <> `Fresh then None - else Some (VCS.slice ~start:t_state ~stop:t_state); + else Some (VCS.slice ~block_start:t_state ~block_stop:t_state); r_ast = t_ast; r_goal = t_goal; r_name = t_name } @@ -1823,7 +1823,7 @@ end = struct (* {{{ *) try Some { r_where = t_where; r_for = t_for; - r_doc = VCS.slice ~start:t_where ~stop:t_where; + r_doc = VCS.slice ~block_start:t_where ~block_stop:t_where; r_what = t_what } with VCS.Expired -> None @@ -2026,7 +2026,7 @@ let known_state ?(redefine_qed=false) ~cache id = let boxes = VCS.box_of id in let valid_boxes = CList.map_filter (function - | ProofBlock ({ stop } as decl, name) when Stateid.equal stop id -> + | ProofBlock ({ block_stop } as decl, name) when Stateid.equal block_stop id -> Some (decl, name) | _ -> None) boxes in assert(List.length valid_boxes < 2); @@ -2156,12 +2156,12 @@ let known_state ?(redefine_qed=false) ~cache id = ), `Yes, true | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) -> let rec aux = function - | `ASync (start, pua, nodes, name, delegate) -> (fun () -> + | `ASync (block_start, pua, nodes, name, delegate) -> (fun () -> assert(keep == VtKeep || keep == VtKeepAsAxiom); let drop_pt = keep == VtKeepAsAxiom in - let stop, exn_info, loc = eop, (id, eop), x.loc in + let block_stop, exn_info, loc = eop, (id, eop), x.loc in log_processing_async id name; - VCS.create_proof_task_box nodes ~qed:id ~start; + VCS.create_proof_task_box nodes ~qed:id ~block_start; begin match brinfo, qed.fproof with | { VCS.kind = `Edit _ }, None -> assert false | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> @@ -2175,7 +2175,7 @@ let known_state ?(redefine_qed=false) ~cache id = ^"the proof's statement to avoid that.")); let fp, cancel = Slaves.build_proof - ~loc ~drop_pt ~exn_info ~start ~stop ~name in + ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name in Future.replace ofp fp; qed.fproof <- Some (fp, cancel); (* We don't generate a new state, but we still need @@ -2183,14 +2183,14 @@ let known_state ?(redefine_qed=false) ~cache id = State.install_cached id | { VCS.kind = `Proof _ }, Some _ -> assert false | { VCS.kind = `Proof _ }, None -> - reach ~cache:`Shallow start; + reach ~cache:`Shallow block_start; let fp, cancel = if delegate then Slaves.build_proof - ~loc ~drop_pt ~exn_info ~start ~stop ~name + ~loc ~drop_pt ~exn_info ~block_start ~block_stop ~name else ProofTask.build_proof_here - ~drop_pt exn_info loc stop, ref false + ~drop_pt exn_info loc block_stop, ref false in qed.fproof <- Some (fp, cancel); let proof = @@ -2354,7 +2354,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) = msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e); exit 1 -let merge_proof_branch ?valid ?id qast keep brname = +let merge_proof_branch ~valid ?id qast keep brname = let brinfo = VCS.get_branch brname in let qed fproof = { qast; keep; brname; brinfo; fproof } in match brinfo with @@ -2377,7 +2377,7 @@ let merge_proof_branch ?valid ?id qast keep brname = VCS.checkout VCS.Branch.master; `Unfocus qed_id | { VCS.kind = `Master } -> - iraise (State.exn_on ?valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null)) + iraise (State.exn_on ~valid Stateid.dummy (Proof_global.NoCurrentProof, Exninfo.null)) (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) @@ -2446,9 +2446,10 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty | VtStm (VtBack oid, true), w -> let id = VCS.new_node ~id:newtip () in let { mine; others } = Backtrack.branches_of oid in + let valid = VCS.get_branch_pos head in List.iter (fun branch -> if not (List.mem_assoc branch (mine::others)) then - ignore(merge_proof_branch x VtDrop branch)) + ignore(merge_proof_branch ~valid x VtDrop branch)) (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); let head = VCS.current_branch () in @@ -2543,8 +2544,8 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty detect_proof_block id cblock; *) Backtrack.record (); if w == VtNow then finish (); `Ok | VtQed keep, w -> - let valid = if tty then Some(VCS.get_branch_pos head) else None in - let rc = merge_proof_branch ?valid ~id:newtip x keep head in + let valid = VCS.get_branch_pos head in + let rc = merge_proof_branch ~valid ~id:newtip x keep head in VCS.checkout_shallowest_proof_branch (); Backtrack.record (); if w == VtNow then finish (); rc diff --git a/stm/stm.mli b/stm/stm.mli index 37ec1f0a13..b8a2a38596 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -139,8 +139,8 @@ module QueryTask : AsyncTaskQueue.Task module DynBlockData : Dyn.S type static_block_declaration = { - start : Stateid.t; - stop : Stateid.t; + block_start : Stateid.t; + block_stop : Stateid.t; dynamic_switch : Stateid.t; carry_on_data : DynBlockData.t; } diff --git a/tactics/auto.ml b/tactics/auto.ml index a6dc64b4e4..6c5ecac943 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -260,31 +260,25 @@ let pr_info_atom (d,pp) = let pr_info_trace = function | (Info,_,{contents=(d,Some pp)::l}) -> - prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l) - | _ -> mt () + Feedback.msg_info (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l)) + | _ -> () let pr_info_nop = function - | (Info,_,_) -> str "idtac." - | _ -> mt () + | (Info,_,_) -> Feedback.msg_info (str "idtac.") + | _ -> () let pr_dbg_header = function - | (Off,_,_) -> mt () - | (Debug,0,_) -> str "(* debug trivial: *)" - | (Debug,_,_) -> str "(* debug auto: *)" - | (Info,0,_) -> str "(* info trivial: *)" - | (Info,_,_) -> str "(* info auto: *)" + | (Off,_,_) -> () + | (Debug,0,_) -> Feedback.msg_debug (str "(* debug trivial: *)") + | (Debug,_,_) -> Feedback.msg_debug (str "(* debug auto: *)") + | (Info,0,_) -> Feedback.msg_info (str "(* info trivial: *)") + | (Info,_,_) -> Feedback.msg_info (str "(* info auto: *)") let tclTRY_dbg d tac = - let (level, _, _) = d in let delay f = Proofview.tclUNIT () >>= fun () -> f () in - let tac = match level with - | Off -> tac - | Debug | Info -> delay (fun () -> Feedback.msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d); tac) - in - let after = match level with - | Info -> delay (fun () -> Feedback.msg_debug (pr_info_nop d); Proofview.tclUNIT ()) - | Off | Debug -> Proofview.tclUNIT () - in + let tac = delay (fun () -> pr_dbg_header d; tac) >>= + fun () -> pr_info_trace d; Proofview.tclUNIT () in + let after = delay (fun () -> pr_info_nop d; Proofview.tclUNIT ()) in Tacticals.New.tclORELSE0 tac after (**************************************************************************) diff --git a/tactics/eauto.ml b/tactics/eauto.ml index c6d2448679..5ca68cbe96 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -346,13 +346,13 @@ let mk_eauto_dbg d = else Off let pr_info_nop = function - | Info -> Feedback.msg_debug (str "idtac.") + | Info -> Feedback.msg_info (str "idtac.") | _ -> () let pr_dbg_header = function | Off -> () | Debug -> Feedback.msg_debug (str "(* debug eauto: *)") - | Info -> Feedback.msg_debug (str "(* info eauto: *)") + | Info -> Feedback.msg_info (str "(* info eauto: *)") let pr_info dbg s = if dbg != Info then () @@ -363,7 +363,7 @@ let pr_info dbg s = | State sp -> let mindepth = loop sp in let indent = String.make (mindepth - sp.depth) ' ' in - Feedback.msg_debug (str indent ++ Lazy.force s.last_tactic ++ str "."); + Feedback.msg_info (str indent ++ Lazy.force s.last_tactic ++ str "."); mindepth in ignore (loop s) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 893f33f1a8..d2e5d8525d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4975,7 +4975,7 @@ module New = struct let reduce_after_refine = reduce (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]}) - {onhyps=Some []; concl_occs=AllOccurrences } + {onhyps=None; concl_occs=AllOccurrences } let refine ?unsafe c = Refine.refine ?unsafe c <*> diff --git a/test-suite/Makefile b/test-suite/Makefile index b32071e802..c10cd4ed44 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -88,6 +88,9 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \ # All subsystems SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk +PREREQUISITELOG = prerequisite/admit.v.log \ + prerequisite/make_local.v.log prerequisite/make_notation.v.log + ####################################################################### # Phony targets ####################################################################### @@ -102,7 +105,7 @@ run: $(SUBSYSTEMS) bugs: $(BUGS) clean: - rm -f trace lia.cache + rm -f trace .lia.cache $(SHOW) "RM <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log>" $(HIDE)find . \( \ -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' \ @@ -226,7 +229,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v +$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \ @@ -257,7 +260,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v +$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -271,7 +274,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v fi; \ } > "$@" -$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out +$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -330,7 +333,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out rm $$tmpexpected; \ } > "$@" -$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v +$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -348,7 +351,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v # the .v file with exactly two digits after the dot. The reference for # time is a 6120 bogomips cpu. ifneq (,$(bogomips)) -$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v +$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ @@ -379,7 +382,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v endif # Ideal-features tests -$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v +$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ echo $(call log_intro,$<); \ diff --git a/test-suite/bugs/closed/3209.v b/test-suite/bugs/closed/3209.v new file mode 100644 index 0000000000..855058b011 --- /dev/null +++ b/test-suite/bugs/closed/3209.v @@ -0,0 +1,75 @@ +(* Avoiding some occur-check *) + +(* 1. Original example *) + +Inductive eqT {A} (x : A) : A -> Type := + reflT : eqT x x. +Definition Bi_inv (A B : Type) (f : (A -> B)) := + sigT (fun (g : B -> A) => + sigT (fun (h : B -> A) => + sigT (fun (α : forall b : B, eqT (f (g b)) b) => + forall a : A, eqT (h (f a)) a))). +Definition TEquiv (A B : Type) := sigT (fun (f : A -> B) => Bi_inv _ _ f). + +Axiom UA : forall (A B : Type), TEquiv (TEquiv A B) (eqT A B). +Definition idtoeqv {A B} (e : eqT A B) : TEquiv A B := + sigT_rect (fun _ => TEquiv A B) + (fun (f : TEquiv A B -> eqT A B) H => + sigT_rect _ (* (fun _ => TEquiv A B) *) + (fun g _ => g e) + H) + (UA A B). + +(* 2. Alternative example by Guillaume *) + +Inductive foo (A : Prop) : Prop := Foo : foo A. +Axiom bar : forall (A : Prop) (P : foo A -> Prop), (A -> P (Foo A)) -> Prop. + +(* This used to fail with a Not_found, we fail more graciously but a + heuristic could be implemented, e.g. in some smart occur-check + function, to find a solution of then form ?P := fun _ => ?P' *) + +Fail Check (fun e : ?[T] => bar ?[A] ?[P] (fun g : ?[A'] => g e)). + +(* This works and tells which solution we could have inferred *) + +Check (fun e : ?[T] => bar ?[A] (fun _ => ?[P]) (fun g : ?[A'] => g e)). + +(* For the record, here is the trace in the failing example: + +In (fun e : ?T => bar ?[A] ?[P] (fun g : ?A' => g e)), we have the existential variables + +e:?T |- ?A : Prop +e:?T |- ?P : foo ?A -> Prop +e:?T |- ?A' : Type + +with constraints + +?A' == ?A +?A' == ?T -> ?P (Foo ?A) + +To type (g e), unification first defines + +?A := forall x:?B, ?P'{e:=e,x:=x} +with ?T <= ?B +and ?P'@{e:=e,x:=e} <= ?P@{e:=e} (Foo (forall x:?B, ?P'{e:=e,x:=x})) + +Then, since ?P'@{e:=e,x:=e} may use "e" in two different ways, it is +not a pattern and we define a new + +e:?T x:?B|- ?P'' : foo (?B' -> ?P''') -> Prop + +for some ?B' and ?P''', together with + +?P'@{e,x} := ?P''{e:=e,x:=e} (Foo (?B -> ?P') +?P@{e} := ?P''{e:=e,x:=e} + +Moreover, ?B' and ?P''' have to satisfy + +?B'@{e:=e,x:=e} == ?B@{e:=e} +?P'''@{e:=e,x:=e} == ?P'@{e:=e,x:=x} + +and this leads to define ?P' which was the initial existential +variable to define. +*) + diff --git a/test-suite/bugs/closed/3495.v b/test-suite/bugs/closed/3495.v new file mode 100644 index 0000000000..102a2aba0d --- /dev/null +++ b/test-suite/bugs/closed/3495.v @@ -0,0 +1,18 @@ +Require Import RelationClasses. + +Axiom R : Prop -> Prop -> Prop. +Declare Instance : Reflexive R. + +Class bar := { x : False }. +Record foo := { a : Prop ; b : bar }. + +Definition default_foo (a0 : Prop) `{b : bar} : foo := {| a := a0 ; b := b |}. + +Goal exists k, R k True. +Proof. +eexists. +evar (b : bar). +let e := match goal with |- R ?e _ => constr:(e) end in +unify e (a (default_foo True)). +subst b. +reflexivity. diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index 4ca6fe78cd..08628377f0 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -249,10 +249,10 @@ Section Reflective_Subuniverse. exact H. Defined. - Definition inO_paths@{i j} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : + Definition inO_paths@{i} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : S) : In@{Ou Oa i} O (x=y). Proof. - simple refine (inO_to_O_retract@{i j} _ _ _); intro u. + simple refine (inO_to_O_retract@{i} _ _ _); intro u. - assert (p : (fun _ : O (x=y) => x) == (fun _=> y)). { @@ -264,4 +264,4 @@ S) : In@{Ou Oa i} O (x=y). hnf. rewrite O_indpaths_beta; reflexivity. Qed. - Check inO_paths@{Type Type}. + Check inO_paths@{Type}. diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index 048f31ce3d..da140c9318 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -652,7 +652,7 @@ Defined. Definition ReflectiveSubuniverse := Modality. - Definition O_reflector := O_reflector. + Definition O_reflector@{u a i} := O_reflector@{u a i}. Definition In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), Type2le@{i a} -> Type2le@{i a} @@ -660,7 +660,7 @@ Defined. Definition O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), In@{u a i} O (O_reflector@{u a i} O T) := O_inO@{u a i}. - Definition to := to. + Definition to@{u a i} := to@{u a i}. Definition inO_equiv_inO@{u a i j k} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j}) (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v index ac0653492a..a6ebda61cf 100644 --- a/test-suite/bugs/closed/4733.v +++ b/test-suite/bugs/closed/4733.v @@ -25,16 +25,16 @@ Check [ _ ]%list : list _. Check [ _ ]%vector : Vector.t _ _. Check [ _ ; _ ]%list : list _. Check [ _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ]%mylist : mylist _. Check [ _ ; _ ; _ ]%list : list _. Check [ _ ; _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ]%mylist : mylist _. Check [ _ ; _ ; _ ; _ ]%list : list _. Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope. -(* Now these all work, but not so in 8.4. If we get the ability to remove notations, and the above fails can be removed, this section can also just be removed. *) +(* Now these all work, but not so in 8.4. If we get the ability to remove notations, this section can also just be removed. *) Check [ ]%mylist : mylist _. Check [ ]%list : list _. Check []%vector : Vector.t _ _. diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v deleted file mode 100644 index ae8ed0e6e8..0000000000 --- a/test-suite/bugs/closed/4763.v +++ /dev/null @@ -1,13 +0,0 @@ -Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses. -Coercion is_true : bool >-> Sortclass. -Global Instance: Transitive leb. -Admitted. - -Goal forall x y z, leb x y -> leb y z -> True. - intros ??? H H'. - lazymatch goal with - | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ] - => pose proof (transitivity H H' : is_true (R x z)) - end. - exact I. -Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v index 14af2d91df..c3c97d3f59 100644 --- a/test-suite/bugs/closed/4785.v +++ b/test-suite/bugs/closed/4785.v @@ -21,7 +21,7 @@ Delimit Scope mylist_scope with mylist. Bind Scope mylist_scope with mylist. Arguments mynil {_}, _. Arguments mycons {_} _ _. -Notation " [] " := mynil : mylist_scope. +Notation " [] " := mynil (compat "8.5") : mylist_scope. Notation " [ ] " := mynil (format "[ ]") : mylist_scope. Notation " [ x ] " := (mycons x nil) : mylist_scope. Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v new file mode 100644 index 0000000000..9d65840acd --- /dev/null +++ b/test-suite/bugs/closed/4785_compat_85.v @@ -0,0 +1,46 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.5") -*- *) +Require Coq.Lists.List Coq.Vectors.Vector. +Require Coq.Compat.Coq85. + +Module A. +Import Coq.Lists.List Coq.Vectors.Vector. +Import ListNotations. +Check [ ]%list : list _. +Import VectorNotations ListNotations. +Delimit Scope vector_scope with vector. +Check [ ]%vector : Vector.t _ _. +Check []%vector : Vector.t _ _. +Check [ ]%list : list _. +Fail Check []%list : list _. + +Goal True. + idtac; [ ]. (* Note that vector notations break the [ | .. | ] syntax of Ltac *) +Abort. + +Inductive mylist A := mynil | mycons (x : A) (xs : mylist A). +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Arguments mynil {_}, _. +Arguments mycons {_} _ _. +Notation " [] " := mynil (compat "8.5") : mylist_scope. +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x nil) : mylist_scope. +Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. + +Import Coq.Compat.Coq85. +Locate Module VectorNotations. +Import VectorDef.VectorNotations. + +Check []%vector : Vector.t _ _. +Check []%mylist : mylist _. +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +End A. + +Module B. +Import Coq.Compat.Coq85. + +Goal True. + idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *) +Abort. +End B. diff --git a/test-suite/bugs/closed/4955.v b/test-suite/bugs/closed/4955.v new file mode 100644 index 0000000000..dce1f764c3 --- /dev/null +++ b/test-suite/bugs/closed/4955.v @@ -0,0 +1,98 @@ +(* An example involving a first-order unification triggering a cyclic constraint *) + +Module A. +Notation "{ x : A | P }" := (sigT (fun x:A => P)). +Notation "( x ; y )" := (existT _ x y) : fibration_scope. +Open Scope fibration_scope. +Notation "p @ q" := (eq_trans p q) (at level 20). +Notation "p ^" := (eq_sym p) (at level 3). +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) +: P y := + match p with eq_refl => u end. +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only +parsing). +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with eq_refl => eq_refl end. +Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y): p # (f +x) = f y + := match p with eq_refl => eq_refl end. +Axiom transport_compose + : forall {A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f +x)), + transport (fun x => P (f x)) p z = transport P (ap f p) z. +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope object_scope with object. +Record PreCategory := { object :> Type ; morphism : object -> object -> Type }. +Delimit Scope functor_scope with functor. +Record Functor (C D : PreCategory) := + { object_of :> C -> D; + morphism_of : forall s d, morphism C s d -> morphism D (object_of s) +(object_of d) }. +Arguments object_of {C%category D%category} f%functor c%object : rename, simpl +nomatch. +Arguments morphism_of [C%category] [D%category] f%functor [s%object d%object] +m%morphism : rename, simpl nomatch. +Section path_functor. + Variable C : PreCategory. + Variable D : PreCategory. + + Local Notation path_functor'_T F G + := { HO : object_of F = object_of G + | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) +(GO d)) + HO + (morphism_of F) + = morphism_of G } + (only parsing). + Definition path_functor'_sig_inv (F G : Functor C D) : F = G -> +path_functor'_T F G + := fun H' + => (ap object_of H'; + (transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H'). + +End path_functor. +End A. + +(* A variant of it with more axioms *) + +Module B. +Notation "{ x : A | P }" := (sigT (fun x:A => P)). +Notation "( x ; y )" := (existT _ x y). +Notation "p @ q" := (eq_trans p q) (at level 20). +Notation "p ^" := (eq_sym p) (at level 3). +Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y. +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only +parsing). +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with eq_refl => eq_refl end. +Axiom apD : forall {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y), p # (f +x) = f y. +Axiom transport_compose + : forall {A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f +x)), + transport (fun x => P (f x)) p z = transport P (ap f p) z. +Record PreCategory := { object :> Type ; morphism : object -> object -> Type }. +Record Functor (C D : PreCategory) := + { object_of :> C -> D; + morphism_of : forall s d, morphism C s d -> morphism D (object_of s) +(object_of d) }. +Arguments object_of {C D} f c : rename, simpl nomatch. +Arguments morphism_of [C] [D] f [s d] m : rename, simpl nomatch. +Section path_functor. + Variable C D : PreCategory. + Local Notation path_functor'_T F G + := { HO : object_of F = object_of G + | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) +(GO d)) + HO + (morphism_of F) + = morphism_of G }. + Definition path_functor'_sig_inv (F G : Functor C D) : F = G -> +path_functor'_T F G + := fun H' + => (ap object_of H'; + (transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H'). + +End path_functor. +End B. diff --git a/test-suite/bugs/closed/5097.v b/test-suite/bugs/closed/5097.v new file mode 100644 index 0000000000..37b239cf61 --- /dev/null +++ b/test-suite/bugs/closed/5097.v @@ -0,0 +1,7 @@ +(* Tracing existing evars along the weakening rule ("clear") *) +Goal forall y, exists x, x=0->x=y. +intros. +eexists ?[x]. +intros. +let x:=constr:(ltac:(clear y; exact 0)) in idtac x. +Abort. diff --git a/test-suite/bugs/closed/5127.v b/test-suite/bugs/closed/5127.v new file mode 100644 index 0000000000..831e8fb507 --- /dev/null +++ b/test-suite/bugs/closed/5127.v @@ -0,0 +1,15 @@ +Fixpoint arrow (n: nat) := + match n with + | S n => bool -> arrow n + | O => bool + end. + +Fixpoint apply (n : nat) : arrow n -> bool := + match n return arrow n -> bool with + | S n => fun f => apply _ (f true) + | O => fun x => x + end. + +Axiom f : arrow 10000. +Definition v : bool := Eval compute in apply _ f. +Definition w : bool := Eval vm_compute in v. diff --git a/test-suite/bugs/closed/5145.v b/test-suite/bugs/closed/5145.v new file mode 100644 index 0000000000..0533d21e0c --- /dev/null +++ b/test-suite/bugs/closed/5145.v @@ -0,0 +1,10 @@ +Class instructions := + { + W : Type; + ldi : nat -> W + }. + +Fail Definition foo := + let y2 := ldi 0 in + let '(CF, _) := (true, 0) in + y2. diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v index 3ca5c095f5..4530548b8f 100644 --- a/test-suite/bugs/opened/4803.v +++ b/test-suite/bugs/opened/4803.v @@ -25,10 +25,24 @@ Check [ _ ]%list : list _. Check [ _ ]%vector : Vector.t _ _. Check [ _ ; _ ]%list : list _. Check [ _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser; it should be added to Compat/Coq84.v *) +Check [ _ ; _ ]%mylist : mylist _. Check [ _ ; _ ; _ ]%list : list _. Check [ _ ; _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ]%mylist : mylist _. Check [ _ ; _ ; _ ; _ ]%list : list _. Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. + +(** Now check that we can add and then remove notations from the parser *) +(* We should be able to stick some vernacular here to remove [] from the parser *) +Fail Remove Notation "[]". +Goal True. + (* This should not be a syntax error; before moving this file to closed, uncomment this line. *) + (* idtac; []. *) + constructor. +Qed. + +Check { _ : _ & _ }. +Reserved Infix "&" (at level 0). +Fail Remove Infix "&". +(* Check { _ : _ & _ }. *) diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 2b828d382a..8ce6f9795c 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -56,3 +56,19 @@ match H with else fun _ : P false => Logic.I) x end : B -> True +The command has indeed failed with message: +Non exhaustive pattern-matching: no clause found for pattern +gadtTy _ _ +The command has indeed failed with message: +In environment +texpDenote : forall t : type, texp t -> typeDenote t +t : type +e : texp t +t1 : type +t2 : type +t0 : type +b : tbinop t1 t2 t0 +e1 : texp t1 +e2 : texp t2 +The term "0" has type "nat" while it is expected to have type + "typeDenote t0". diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 3c2eaf42c9..4074896420 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -77,3 +77,32 @@ destruct b as [|] ; exact Logic.I. Defined. Print f. + +(* Was enhancement request #5142 (error message reported on the most + general return clause heuristic) *) + +Inductive gadt : Type -> Type := +| gadtNat : nat -> gadt nat +| gadtTy : forall T, T -> gadt T. + +Fail Definition gadt_id T (x: gadt T) : gadt T := + match x with + | gadtNat n => gadtNat n + end. + +(* A variant of #5142 (see Satrajit Roy's example on coq-club (Oct 17, 2016)) *) + +Inductive type:Set:=Nat. +Inductive tbinop:type->type->type->Set:= TPlus : tbinop Nat Nat Nat. +Inductive texp:type->Set:= + |TNConst:nat->texp Nat + |TBinop:forall t1 t2 t, tbinop t1 t2 t->texp t1->texp t2->texp t. +Definition typeDenote(t:type):Set:= match t with Nat => nat end. + +(* We expect a failure on TBinop *) +Fail Fixpoint texpDenote t (e:texp t):typeDenote t:= + match e with + | TNConst n => n + | TBinop t1 t2 _ b e1 e2 => O + end. + diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index 5541ccf57b..ad60aeccce 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -60,3 +60,27 @@ exist (Q x) y conj : nat -> nat {1, 2} : nat -> Prop +a# + : Set +a# + : Set +a≡ + : Set +a≡ + : Set +.≡ + : Set +.≡ + : Set +.a# + : Set +.a# + : Set +.a≡ + : Set +.a≡ + : Set +.α + : Set +.α + : Set diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 1d8278c088..ceb29d1b9e 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -116,3 +116,32 @@ Check %j. Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) .. (a = v))). Check ({1, 2}). + +(**********************************************************************) +(* Check notations of the form ".a", ".a≡", "a≡" *) +(* Only "a#", "a≡" and ".≡" were working properly for parsing. The *) +(* other ones were working only for printing. *) + +Notation "a#" := nat. +Check nat. +Check a#. + +Notation "a≡" := nat. +Check nat. +Check a≡. + +Notation ".≡" := nat. +Check nat. +Check .≡. + +Notation ".a#" := nat. +Check nat. +Check .a#. + +Notation ".a≡" := nat. +Check nat. +Check .a≡. + +Notation ".α" := nat. +Check nat. +Check .α. diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index 1eb7eca8f1..f3c12effca 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -40,7 +40,6 @@ Nat.land: nat -> nat -> nat Nat.lor: nat -> nat -> nat Nat.ldiff: nat -> nat -> nat Nat.lxor: nat -> nat -> nat - S: nat -> nat Nat.succ: nat -> nat Nat.pred: nat -> nat @@ -74,7 +73,6 @@ le_n: forall n : nat, n <= n pair: forall A B : Type, A -> B -> A * B conj: forall A B : Prop, A -> B -> A /\ B Nat.divmod: nat -> nat -> nat -> nat -> nat * nat - h: n <> newdef n h: n <> newdef n h: P n diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index f4254e4e2f..a7bde5ea3f 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -26,3 +26,8 @@ The command has indeed failed with message: In nested Ltac calls to "h" and "injection (destruction_arg)", last call failed. Error: No primitive equality found. +Hx +nat +nat +0 +0 diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v index dfa60eeda0..76c37625aa 100644 --- a/test-suite/output/ltac.v +++ b/test-suite/output/ltac.v @@ -43,3 +43,17 @@ Goal True -> False. Fail h I. intro H. Fail h H. + +(* Check printing of the "var" argument "Hx" *) +Ltac m H := idtac H; exact H. +Goal True. +let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac. + +(* Check consistency of interpretation scopes (#4398) *) + +Goal nat*(0*0=0) -> nat*(0*0=0). intro. +match goal with H: ?x*?y |- _ => idtac x end. +match goal with |- ?x*?y => idtac x end. +match goal with H: context [?x*?y] |- _ => idtac x end. +match goal with |- context [?x*?y] => idtac x end. +Abort. diff --git a/test-suite/output/qualification.out b/test-suite/output/qualification.out new file mode 100644 index 0000000000..9300c3f546 --- /dev/null +++ b/test-suite/output/qualification.out @@ -0,0 +1,3 @@ +File "stdin", line 19, characters 0-7: +Error: Signature components for label test do not match: expected type +"Top.M2.t = Top.M2.M.t" but found type "Top.M2.t = Top.M2.t". diff --git a/test-suite/output/qualification.v b/test-suite/output/qualification.v new file mode 100644 index 0000000000..d39097e2dd --- /dev/null +++ b/test-suite/output/qualification.v @@ -0,0 +1,19 @@ +Module Type T1. + Parameter t : Type. +End T1. + +Module Type T2. + Declare Module M : T1. + Parameter t : Type. + Parameter test : t = M.t. +End T2. + +Module M1 <: T1. + Definition t : Type := bool. +End M1. + +Module M2 <: T2. + Module M := M1. + Definition t : Type := nat. + Lemma test : t = t. Proof. reflexivity. Qed. +End M2. diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out index d152052ba3..ae84603622 100644 --- a/test-suite/output/unifconstraints.out +++ b/test-suite/output/unifconstraints.out @@ -8,11 +8,7 @@ subgoal 2 is: forall n : nat, ?Goal n -> ?Goal (S n) subgoal 3 is: nat -unification constraints: - ?Goal ?Goal2 <= - True /\ True /\ True \/ - veeryyyyyyyyyyyyloooooooooooooonggidentifier = - veeryyyyyyyyyyyyloooooooooooooonggidentifier +unification constraint: ?Goal ?Goal2 <= True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = @@ -28,11 +24,7 @@ subgoal 2 is: forall n0 : nat, ?Goal@{n:=n; m:=m} n0 -> ?Goal@{n:=n; m:=m} (S n0) subgoal 3 is: nat -unification constraints: - ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <= - True /\ True /\ True \/ - veeryyyyyyyyyyyyloooooooooooooonggidentifier = - veeryyyyyyyyyyyyloooooooooooooonggidentifier +unification constraint: ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <= True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = @@ -48,12 +40,7 @@ subgoal 2 is: forall n0 : nat, ?Goal1@{m:=m} n0 -> ?Goal1@{m:=m} (S n0) subgoal 3 is: nat -unification constraints: - - n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <= - True /\ True /\ True \/ - veeryyyyyyyyyyyyloooooooooooooonggidentifier = - veeryyyyyyyyyyyyloooooooooooooonggidentifier +unification constraint: n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <= True /\ True /\ True \/ @@ -70,12 +57,7 @@ subgoal 2 is: forall n0 : nat, ?Goal0@{m:=m} n0 -> ?Goal0@{m:=m} (S n0) subgoal 3 is: nat -unification constraints: - - n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <= - True /\ True /\ True \/ - veeryyyyyyyyyyyyloooooooooooooonggidentifier = - veeryyyyyyyyyyyyloooooooooooooonggidentifier +unification constraint: n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <= True /\ True /\ True \/ diff --git a/test-suite/success/CaseInClause.v b/test-suite/success/CaseInClause.v index 599b9566cb..6424fe92dd 100644 --- a/test-suite/success/CaseInClause.v +++ b/test-suite/success/CaseInClause.v @@ -24,3 +24,6 @@ Theorem foo : forall (n m : nat) (pf : n = m), (* Check redundant clause is removed *) Inductive I : nat * nat -> Type := C : I (0,0). Check fun x : I (1,1) => match x in I (y,z) return y = z with C => eq_refl end. + +(* An example of non-local inference of the type of an impossible case *) +Check (fun y n (x:Vector.t nat (S n)) => match x with a::_ => a | _ => y end) 2. diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 2f7c62972a..07bbb60c40 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -58,7 +58,7 @@ Check (fun x:nat*nat => match x with R x y => (x,y) end). (* Check multi-tokens recursive notations *) -Local Notation "[ a # ; .. # ; b ]" := (a + .. (b + 0) ..). +Local Notation "[ a # ; .. # ; b ]" := (a + .. (b + 0) ..). Check [ 0 ]. Check [ 0 # ; 1 ]. @@ -110,3 +110,21 @@ Goal True -> True. intros H. exact H. Qed. (* Check absence of collision on ".." in nested notations with ".." *) Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)). + +(* Check that vector notations do not break Ltac [] (bugs #4785, #4733) *) +Require Import Coq.Vectors.VectorDef. +Import VectorNotations. +Goal True. idtac; []. (* important for test: no space here *) constructor. Qed. + +(* Check parsing of { and } is not affected by notations #3479 *) +Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10). +Goal True. +{{ exact I. }} +Qed. +Check |- {{ 0 }} 0. + +(* Check parsing of { and } is not affected by notations #3479 *) +Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10). +Goal True. +{{ exact I. }} +Qed. diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 5eecdc64cc..a3e23f91c9 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -74,12 +74,6 @@ Coercion sig_of_sigT : sigT >-> sig. Coercion sigT2_of_sig2 : sig2 >-> sigT2. Coercion sig2_of_sigT2 : sigT2 >-> sig2. -(** As per bug #4733 (https://coq.inria.fr/bugs/show_bug.cgi?id=4733), we want the user to be able to create custom list-like notatoins that work in both 8.4 and 8.5. This is necessary. These should become compat 8.4 notations in the relevant files, but these modify the parser (bug #4798), so this cannot happen until that bug is fixed. *) -Require Coq.Lists.List. -Require Coq.Vectors.VectorDef. -Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) : list_scope. -Notation "[ x ; .. ; y ]" := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope. - (** In 8.4, the statement of admitted lemmas did not depend on the section variables. *) Unset Keep Admitted Variables. diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index 74b416aae7..4007536442 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -27,21 +27,3 @@ Global Set Refolding Reduction. Global Set Typeclasses Legacy Resolution. Global Set Typeclasses Limit Intros. Global Unset Typeclasses Filtered Unification. - -(** In Coq 8.5, [] meant Vector, and [ ] meant list. Restore this - behavior, to allow user-defined [] to not override vector - notations. See https://coq.inria.fr/bugs/show_bug.cgi?id=4785. *) - -Require Coq.Lists.List. -Require Coq.Vectors.VectorDef. -Module Export Coq. -Module Export Vectors. -Module VectorDef. -Export Coq.Vectors.VectorDef. -Module VectorNotations. -Export Coq.Vectors.VectorDef.VectorNotations. -Notation "[]" := (VectorDef.nil _) : vector_scope. -End VectorNotations. -End VectorDef. -End Vectors. -End Coq. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index fc94d7e254..bf21ffb47b 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -27,6 +27,7 @@ Module ListNotations. Notation "[ ]" := nil (format "[ ]") : list_scope. Notation "[ x ]" := (cons x nil) : list_scope. Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) : list_scope. +Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) (compat "8.4") : list_scope. End ListNotations. Import ListNotations. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index f49b340758..1f8b76cb62 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -295,11 +295,12 @@ End VECTORLIST. Module VectorNotations. Delimit Scope vector_scope with vector. Notation "[ ]" := [] (format "[ ]") : vector_scope. +Notation "[]" := [] (compat "8.5") : vector_scope. Notation "h :: t" := (h :: t) (at level 60, right associativity) : vector_scope. Notation "[ x ]" := (x :: []) : vector_scope. -Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope -. +Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope. +Notation "[ x ; .. ; y ]" := (cons _ x _ .. (cons _ y _ (nil _)) ..) (compat "8.4") : vector_scope. Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope. Open Scope vector_scope. End VectorNotations. diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 71e1f9593d..f0f8f18641 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -34,7 +34,7 @@ let resize_buffer ibuf = ibuf.str <- nstr (* Delete all irrelevant lines of the input buffer. Keep the last line - in the buffer (useful when there are several commands on the same line. *) + in the buffer (useful when there are several commands on the same line). *) let resynch_buffer ibuf = match ibuf.bols with @@ -299,7 +299,7 @@ let do_vernac () = resynch_buffer top_buffer; try let input = (top_buffer.tokens, None) in - Vernac.eval_expr input (read_sentence input) + Vernac.process_expr top_buffer.tokens (read_sentence input) with | End_of_input | CErrors.Quit -> top_stderr (fnl ()); raise CErrors.Quit @@ -308,7 +308,6 @@ let do_vernac () = else Feedback.msg_error (str"There is no ML toplevel.") | any -> let any = CErrors.push any in - Format.set_formatter_out_channel stdout; let msg = print_toplevel_error any ++ fnl () in pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft msg; Format.pp_print_flush !Pp_control.std_ft () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7a67e0951f..5ae1c36ed8 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -168,7 +168,7 @@ let load_vernacular () = List.iter (fun (s,b) -> let s = Loadpath.locate_file s in - if Flags.do_beautify () then + if !Flags.beautify then with_option beautify_file (Vernac.load_vernac b) s else Vernac.load_vernac b s) @@ -219,7 +219,7 @@ let add_compile verbose s = compile_list := (verbose,s) :: !compile_list let compile_file (v,f) = - if Flags.do_beautify () then + if !Flags.beautify then with_option beautify_file (Vernac.compile v) f else Vernac.compile v f @@ -228,11 +228,9 @@ let compile_files () = if !compile_list == [] then () else let init_state = States.freeze ~marshallable:`No in - let coqdoc_init_state = CLexer.location_table () in Feedback.(add_feeder debug_feeder); List.iter (fun vf -> States.unfreeze init_state; - CLexer.restore_location_table coqdoc_init_state; compile_file vf) (List.rev !compile_list) @@ -538,7 +536,7 @@ let parse_args arglist = Flags.async_proofs_never_reopen_branch := true; |"-batch" -> set_batch_mode () |"-test-mode" -> test_mode := true - |"-beautify" -> make_beautify true + |"-beautify" -> beautify := true |"-boot" -> boot := true; no_load_rc () |"-bt" -> Backtrace.record_backtrace true |"-color" -> set_color (next ()) @@ -550,7 +548,7 @@ let parse_args arglist = |"-ideslave" -> set_ideslave () |"-impredicative-set" -> set_impredicative_set () |"-indices-matter" -> Indtypes.enforce_indices_matter () - |"-just-parsing" -> Vernac.just_parsing := true + |"-just-parsing" -> warning "-just-parsing option has been removed in 8.6" |"-m"|"--memory" -> memory_stat := true |"-noinit"|"-nois" -> load_init := false |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 6ee695bc24..f98505c362 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -516,7 +516,8 @@ let explain_cant_find_case_type env sigma c = let c = Evarutil.nf_evar sigma c in let env = make_all_name_different env in let pe = pr_lconstr_env env sigma c in - str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe ++ str "." + str "Cannot infer the return type of pattern-matching on" ++ ws 1 ++ + pe ++ str "." let explain_occur_check env sigma ev rhs = let rhs = Evarutil.nf_evar sigma rhs in @@ -755,7 +756,7 @@ let pr_constraints printenv env sigma evars cstrs = let evs = prlist (fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++ - str " : " ++ pr_lconstr_env env' sigma evi.evar_concl) l + str " : " ++ pr_lconstr_env env' sigma evi.evar_concl ++ fnl ()) l in h 0 (pe ++ evs ++ pr_evar_constraints cstrs) else diff --git a/toplevel/search.ml b/toplevel/search.ml index 921308f78a..ff3c7a4f42 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -29,17 +29,6 @@ query, separated by a newline. This type of output is useful for editors (like emacs), to generate a list of completion candidates without having to parse thorugh the types of all symbols. *) -let search_output_name_only = ref false - -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "output-name-only search"; - optkey = ["Search";"Output";"Name";"Only"]; - optread = (fun () -> !search_output_name_only); - optwrite = (:=) search_output_name_only } - type glob_search_about_item = | GlobSearchSubPattern of constr_pattern | GlobSearchString of string @@ -118,18 +107,6 @@ let generic_search glnumopt fn = | Some glnum -> iter_hypothesis glnum fn); iter_declarations fn -(** Standard display *) -let plain_display accu ref env c = - let pr = pr_global ref in - if !search_output_name_only then - accu := pr :: !accu - else begin - let pc = pr_lconstr_env env Evd.empty c in - accu := hov 2 (pr ++ str":" ++ spc () ++ pc) :: !accu - end - -let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l) - (** Filters *) (** This function tries to see whether the conclusion matches a pattern. *) @@ -181,8 +158,7 @@ let search_about_filter query gr env typ = match query with (** SearchPattern *) -let search_pattern gopt pat mods = - let ans = ref [] in +let search_pattern gopt pat mods pr_search = let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && @@ -190,10 +166,9 @@ let search_pattern gopt pat mods = blacklist_filter ref env typ in let iter ref env typ = - if filter ref env typ then plain_display ans ref env typ + if filter ref env typ then pr_search ref env typ in - let () = generic_search gopt iter in - format_display !ans + generic_search gopt iter (** SearchRewrite *) @@ -205,10 +180,9 @@ let rewrite_pat1 pat = let rewrite_pat2 pat = PApp (PRef eq, [| PMeta None; PMeta None; pat |]) -let search_rewrite gopt pat mods = +let search_rewrite gopt pat mods pr_search = let pat1 = rewrite_pat1 pat in let pat2 = rewrite_pat2 pat in - let ans = ref [] in let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && @@ -217,15 +191,13 @@ let search_rewrite gopt pat mods = blacklist_filter ref env typ in let iter ref env typ = - if filter ref env typ then plain_display ans ref env typ + if filter ref env typ then pr_search ref env typ in - let () = generic_search gopt iter in - format_display !ans + generic_search gopt iter (** Search *) -let search_by_head gopt pat mods = - let ans = ref [] in +let search_by_head gopt pat mods pr_search = let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && @@ -233,15 +205,13 @@ let search_by_head gopt pat mods = blacklist_filter ref env typ in let iter ref env typ = - if filter ref env typ then plain_display ans ref env typ + if filter ref env typ then pr_search ref env typ in - let () = generic_search gopt iter in - format_display !ans + generic_search gopt iter (** SearchAbout *) -let search_about gopt items mods = - let ans = ref [] in +let search_about gopt items mods pr_search = let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = let eqb b1 b2 = if b1 then b2 else not b2 in @@ -251,10 +221,9 @@ let search_about gopt items mods = blacklist_filter ref env typ in let iter ref env typ = - if filter ref env typ then plain_display ans ref env typ + if filter ref env typ then pr_search ref env typ in - let () = generic_search gopt iter in - format_display !ans + generic_search gopt iter type search_constraint = | Name_Pattern of Str.regexp diff --git a/toplevel/search.mli b/toplevel/search.mli index 9f209a17e7..ba3d48efcc 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -39,11 +39,14 @@ val search_about_filter : glob_search_about_item -> filter_function goal and the global environment for things matching [pattern] and satisfying module exclude/include clauses of [modinout]. *) -val search_by_head : int option -> constr_pattern -> DirPath.t list * bool -> std_ppcmds -val search_rewrite : int option -> constr_pattern -> DirPath.t list * bool -> std_ppcmds -val search_pattern : int option -> constr_pattern -> DirPath.t list * bool -> std_ppcmds +val search_by_head : int option -> constr_pattern -> DirPath.t list * bool + -> display_function -> unit +val search_rewrite : int option -> constr_pattern -> DirPath.t list * bool + -> display_function -> unit +val search_pattern : int option -> constr_pattern -> DirPath.t list * bool + -> display_function -> unit val search_about : int option -> (bool * glob_search_about_item) list - -> DirPath.t list * bool -> std_ppcmds + -> DirPath.t list * bool -> display_function -> unit type search_constraint = (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index b8e44db9a7..b453dbc469 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -18,6 +18,8 @@ open Vernacexpr Use the module Coqtoplevel, which catches these exceptions (the exceptions are explained only at the toplevel). *) +let user_error loc s = CErrors.user_err_loc (loc,"_",str s) + (* Navigation commands are allowed in a coqtop session but not in a .v file *) let rec is_navigation_vernac = function @@ -42,6 +44,14 @@ let is_reset = function | VernacResetInitial | VernacResetName _ -> true | _ -> false +let checknav_simple loc cmd = + if is_navigation_vernac cmd && not (is_reset cmd) then + user_error loc "Navigation commands forbidden in files." + +let checknav_deep loc ast = + if is_deep_navigation_vernac ast then + user_error loc "Navigation commands forbidden in nested commands." + (* When doing Load on a file, two behaviors are possible: - either the history stack is grown by only one command, @@ -70,8 +80,6 @@ let disable_drop = function | Drop -> CErrors.error "Drop is forbidden." | e -> e -let user_error loc s = CErrors.user_err_loc (loc,"_",str s) - (* Opening and closing a channel. Open it twice when verbose: the first channel is used to read the commands, and the second one to print them. Note: we could use only one thanks to seek_in, but seeking on and on in @@ -81,7 +89,7 @@ let open_file_twice_if verbosely longfname = let in_chan = open_utf8_file_in longfname in let verb_ch = if verbosely then Some (open_utf8_file_in longfname) else None in - let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in + let po = Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in (in_chan, longfname, (po, verb_ch)) let close_input in_chan (_,verb) = @@ -114,48 +122,39 @@ let parse_sentence = Flags.with_option Flags.we_are_parsing (* vernac parses the given stream, executes interpfun on the syntax tree it * parses, and is verbose on "primitives" commands if verbosely is true *) -let just_parsing = ref false let chan_beautify = ref stdout let beautify_suffix = ".beautified" -let set_formatter_translator() = - let ch = !chan_beautify in +let set_formatter_translator ch = let out s b e = output ch s b e in Format.set_formatter_output_functions out (fun () -> flush ch); Format.set_max_boxes max_int -let pr_new_syntax_in_context loc ocom = +let pr_new_syntax_in_context loc chan_beautify ocom = let loc = Loc.unloc loc in - if !beautify_file then set_formatter_translator(); + if !beautify_file then set_formatter_translator chan_beautify; let fs = States.freeze ~marshallable:`No in - (* Side-effect: order matters *) - let before = comment (CLexer.extract_comments (fst loc)) in - let com = match ocom with - | Some com -> Ppvernac.pr_vernac com - | None -> mt() in - let after = comment (CLexer.extract_comments (snd loc)) in - if !beautify_file then - Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after)) - else - Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); - States.unfreeze fs; - Format.set_formatter_out_channel stdout - -let pr_new_syntax (po,_) loc ocom = - (* Reinstall the context of parsing which includes the bindings of comments to locations *) - Pcoq.Gram.with_parsable po (pr_new_syntax_in_context loc) ocom - -let save_translator_coqdoc () = - (* translator state *) - let ch = !chan_beautify in - (* end translator state *) - let coqdocstate = CLexer.location_table () in - ch,coqdocstate + (* The content of this is not supposed to fail, but if ever *) + try + (* Side-effect: order matters *) + let before = comment (CLexer.extract_comments (fst loc)) in + let com = match ocom with + | Some com -> Ppvernac.pr_vernac com + | None -> mt() in + let after = comment (CLexer.extract_comments (snd loc)) in + if !beautify_file then + Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after)) + else + Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); + States.unfreeze fs; + Format.set_formatter_out_channel stdout + with any -> + States.unfreeze fs; + Format.set_formatter_out_channel stdout -let restore_translator_coqdoc (ch,coqdocstate) = - if !Flags.beautify_file then close_out !chan_beautify; - chan_beautify := ch; - CLexer.restore_location_table coqdocstate +let pr_new_syntax po loc chan_beautify ocom = + (* Reinstall the context of parsing which includes the bindings of comments to locations *) + Pcoq.Gram.with_parsable po (pr_new_syntax_in_context chan_beautify loc) ocom (* For coqtop -time, we display the position in the file, and a glimpse of the executed command *) @@ -185,72 +184,52 @@ let print_cmd_header loc com = Pp.pp_with !Pp_control.std_ft (pp_cmd_header loc com); Format.pp_print_flush !Pp_control.std_ft () -let rec vernac_com input checknav (loc,com) = +let rec interp_vernac po chan_beautify checknav (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let f = Loadpath.locate_file fname in - let st = save_translator_coqdoc () in - let old_lexer_file = CLexer.get_current_file () in - CLexer.set_current_file f; - if !Flags.beautify_file then - begin - chan_beautify := open_out (f^beautify_suffix); - end; - begin - try - Flags.silently (read_vernac_file verbosely) f; - restore_translator_coqdoc st; - CLexer.set_current_file old_lexer_file; - with reraise -> - let reraise = CErrors.push reraise in - restore_translator_coqdoc st; - CLexer.set_current_file old_lexer_file; - iraise reraise - end - - | v when !just_parsing -> () + load_vernac verbosely f | v -> Stm.interp (Flags.is_verbose()) (loc,v) in try checknav loc com; - if do_beautify () then pr_new_syntax input loc (Some com); + if !beautify then pr_new_syntax po chan_beautify loc (Some com); (* XXX: This is not 100% correct if called from an IDE context *) if !Flags.time then print_cmd_header loc com; let com = if !Flags.time then VernacTime (loc,com) else com in interp com with reraise -> let (reraise, info) = CErrors.push reraise in - Format.set_formatter_out_channel stdout; let loc' = Option.default Loc.ghost (Loc.get_loc info) in if Loc.is_ghost loc' then iraise (reraise, Loc.add_loc info loc) else iraise (reraise, info) -and read_vernac_file verbosely s = - let checknav loc cmd = - if is_navigation_vernac cmd && not (is_reset cmd) then - user_error loc "Navigation commands forbidden in files" - in - let (in_chan, fname, input) = open_file_twice_if verbosely s in +(* Load a vernac file. CErrors are annotated with file and location *) +and load_vernac verbosely file = + let chan_beautify = + if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout in + let (in_chan, fname, input) = open_file_twice_if verbosely file in try (* we go out of the following infinite loop when a End_of_input is * raised, which means that we raised the end of the file being loaded *) while true do - let loc_ast = parse_sentence input in + let loc_ast = Flags.silently parse_sentence input in CWarnings.set_current_loc (fst loc_ast); - vernac_com input checknav loc_ast; + Flags.silently (interp_vernac (fst input) chan_beautify checknav_simple) loc_ast; done with any -> (* whatever the exception *) let (e, info) = CErrors.push any in - Format.set_formatter_out_channel stdout; close_input in_chan input; (* we must close the file first *) match e with | End_of_input -> - if do_beautify () then - pr_new_syntax input (Loc.make_loc (max_int,max_int)) None + if !beautify then + pr_new_syntax (fst input) chan_beautify (Loc.make_loc (max_int,max_int)) None; + if !Flags.beautify_file then close_out chan_beautify; | reraise -> + if !Flags.beautify_file then close_out chan_beautify; iraise (disable_drop e, info) (** [eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit] @@ -260,32 +239,12 @@ and read_vernac_file verbosely s = of a new state label). An example of state-preserving command is one coming from the query panel of Coqide. *) -let checknav loc ast = - if is_deep_navigation_vernac ast then - user_error loc "Navigation commands forbidden in nested commands" - -let eval_expr input loc_ast = vernac_com input checknav loc_ast +let process_expr po loc_ast = interp_vernac po stdout checknav_deep loc_ast (* XML output hooks *) let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore () -(* Load a vernac file. CErrors are annotated with file and location *) -let load_vernac verb file = - chan_beautify := - if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout; - let old_lexer_file = CLexer.get_current_file () in - try - CLexer.set_current_file file; - Flags.silently (read_vernac_file verb) file; - if !Flags.beautify_file then close_out !chan_beautify; - CLexer.set_current_file old_lexer_file; - with any -> - let (e, info) = CErrors.push any in - if !Flags.beautify_file then close_out !chan_beautify; - CLexer.set_current_file old_lexer_file; - iraise (disable_drop e, info) - let warn_file_no_extension = CWarnings.create ~name:"file-no-extension" ~category:"filesystem" (fun (f,ext) -> diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli index 2fd86ddc22..0d9f5871a3 100644 --- a/toplevel/vernac.mli +++ b/toplevel/vernac.mli @@ -14,14 +14,11 @@ val parse_sentence : Pcoq.Gram.coq_parsable * in_channel option -> Loc.t * Vernacexpr.vernac_expr -(** Reads and executes vernac commands from a stream. - The boolean [just_parsing] disables interpretation of commands. *) +(** Reads and executes vernac commands from a stream. *) exception End_of_input -val just_parsing : bool ref - -val eval_expr : Pcoq.Gram.coq_parsable * in_channel option -> Loc.t * Vernacexpr.vernac_expr -> unit +val process_expr : Pcoq.Gram.coq_parsable -> Loc.t * Vernacexpr.vernac_expr -> unit (** Set XML hooks *) val xml_start_library : (unit -> unit) Hook.t diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8a2caa446a..4de1d95959 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1738,6 +1738,28 @@ let interp_search_about_item env = errorlabstrm "interp_search_about_item" (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component") +(* 05f22a5d6d5b8e3e80f1a37321708ce401834430 introduced the + `search_output_name_only` option to avoid excessive printing when + searching. + + The motivation was to make search usable for IDE completion, + however, it is still too slow due to the non-indexed nature of the + underlying search mechanism. + + In the future we should deprecate the option and provide a fast, + indexed name-searching interface. +*) +let search_output_name_only = ref false + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "output-name-only search"; + optkey = ["Search";"Output";"Name";"Only"]; + optread = (fun () -> !search_output_name_only); + optwrite = (:=) search_output_name_only } + let vernac_search s gopt r = let r = interp_search_restriction r in let env,gopt = @@ -1749,16 +1771,25 @@ let vernac_search s gopt r = | Some g -> snd (Pfedit.get_goal_context g) , Some g in let get_pattern c = snd (intern_constr_pattern env c) in - let open Feedback in + let pr_search ref env c = + let pr = pr_global ref in + let pp = if !search_output_name_only + then pr + else begin + let pc = pr_lconstr_env env Evd.empty c in + hov 2 (pr ++ str":" ++ spc () ++ pc) + end + in Feedback.msg_notice pp + in match s with | SearchPattern c -> - msg_notice (Search.search_pattern gopt (get_pattern c) r) + Search.search_pattern gopt (get_pattern c) r pr_search | SearchRewrite c -> - msg_notice (Search.search_rewrite gopt (get_pattern c) r) + Search.search_rewrite gopt (get_pattern c) r pr_search | SearchHead c -> - msg_notice (Search.search_by_head gopt (get_pattern c) r) + Search.search_by_head gopt (get_pattern c) r pr_search | SearchAbout sl -> - msg_notice (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r) + Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r pr_search let vernac_locate = let open Feedback in function | LocateAny (AN qid) -> msg_notice (print_located_qualid qid) @@ -1886,7 +1917,7 @@ let vernac_load interp fname = let input = let longfname = Loadpath.locate_file fname in let in_chan = open_utf8_file_in longfname in - Pcoq.Gram.parsable (Stream.of_channel in_chan) in + Pcoq.Gram.parsable ~file:longfname (Stream.of_channel in_chan) in try while true do interp (snd (parse_sentence input)) done with End_of_input -> () |