diff options
58 files changed, 515 insertions, 296 deletions
diff --git a/API/API.mli b/API/API.mli index c5a1743f7e..8f46a58321 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2394,7 +2394,7 @@ sig and case_expr = constr_expr * Names.Name.t Loc.located option * cases_pattern_expr option and branch_expr = - (cases_pattern_expr list Loc.located list * constr_expr) Loc.located + (cases_pattern_expr list list * constr_expr) Loc.located and binder_expr = Names.Name.t Loc.located list * binder_kind * constr_expr @@ -3853,10 +3853,9 @@ sig type matching_result = { m_sub : bound_ident_map * Ltac_pretype.patvar_map; m_ctx : EConstr.constr } - val match_subterm_gen : Environ.env -> Evd.evar_map -> - bool -> - binding_bound_vars * Pattern.constr_pattern -> EConstr.constr -> - matching_result IStream.t + val match_subterm : Environ.env -> Evd.evar_map -> + binding_bound_vars * Pattern.constr_pattern -> EConstr.constr -> + matching_result IStream.t val matches : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Ltac_pretype.patvar_map end @@ -4347,6 +4346,7 @@ sig | Later : [ `thunk ] delay val print_universes : bool ref val print_evar_arguments : bool ref + val print_allow_match_default_clause : bool ref val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.Set.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g val subst_glob_constr : Mod_subst.substitution -> Glob_term.glob_constr -> Glob_term.glob_constr val set_detype_anonymous : (?loc:Loc.t -> int -> Names.Id.t) -> unit @@ -12,6 +12,16 @@ Notations opened rather than to the latest notations defined independently of whether they are in an opened scope or not. +Specification language + +- When printing clauses of a "match", clauses with same right-hand + side are factorized and the last most factorized clause with no + variables, if it exists, is turned into a default clause. + Use "Unset Printing Allow Default Clause" do deactivate printing + of a default clause. + Use "Unset Printing Factorizable Match Patterns" to deactivate + factorization of clauses with same right-hand side. + Tactics - On Linux, "native_compute" calls can be profiled using the "perf" @@ -233,7 +233,7 @@ package "API" ( description = "Coq API" version = "8.7" - requires = "coq.stm" + requires = "coq.intf, coq.stm" directory = "API" archive(byte) = "API.cma" diff --git a/config/coq_config.mli b/config/coq_config.mli index 40661f4284..1666df0bde 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -76,4 +76,5 @@ val wwwbugtracker : string val wwwstdlib : string val localwwwrefman : string -val no_native_compiler : bool +val bytecode_compiler : bool +val native_compiler : bool diff --git a/configure.ml b/configure.ml index 2292913d50..06aa5e7666 100644 --- a/configure.ml +++ b/configure.ml @@ -277,6 +277,7 @@ module Prefs = struct let debug = ref true let profile = ref false let annotate = ref false + let bytecodecompiler = ref true let nativecompiler = ref (not (os_type_win32 || os_type_cygwin)) let coqwebsite = ref "http://coq.inria.fr/" let force_caml_version = ref false @@ -343,6 +344,8 @@ let args_options = Arg.align [ " Add profiling information in the Coq executables"; "-annotate", Arg.Set Prefs.annotate, " Dumps ml annotation files while compiling Coq"; + "-bytecode-compiler", arg_bool Prefs.bytecodecompiler, + "(yes|no) Enable Coq's bytecode reduction machine (VM)"; "-native-compiler", arg_bool Prefs.nativecompiler, "(yes|no) Compilation to native code for conversion and normalization"; "-coqwebsite", Arg.Set_string Prefs.coqwebsite, @@ -1031,9 +1034,9 @@ let print_summary () = pr " Documentation : %s\n" (if withdoc then "All" else "None"); pr " Web browser : %s\n" browser; - pr " Coq web site : %s\n\n" !Prefs.coqwebsite; - if not !Prefs.nativecompiler then - pr " Native compiler for conversion and normalization disabled\n\n"; + pr " Coq web site : %s\n" !Prefs.coqwebsite; + pr " Bytecode VM enabled : %B\n" !Prefs.bytecodecompiler; + pr " Native Compiler enabled : %B\n\n" !Prefs.nativecompiler; if !Prefs.local then pr " Local build, no installation...\n" else @@ -1128,7 +1131,8 @@ let write_configml f = pr_s "wwwrefman" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/refman/"); pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/"); pr_s "localwwwrefman" ("file:/" ^ docdir ^ "/html/refman"); - pr_b "no_native_compiler" (not !Prefs.nativecompiler); + pr_b "bytecode_compiler" !Prefs.bytecodecompiler; + pr_b "native_compiler" !Prefs.nativecompiler; let core_src_dirs = [ "config"; "dev"; "kernel"; "library"; "engine"; "pretyping"; "interp"; "parsing"; "proofs"; diff --git a/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh b/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh new file mode 100644 index 0000000000..6741cf26fb --- /dev/null +++ b/dev/ci/user-overlays/06169-Zimmi48-clean-up-deprecated-options.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6169" ] || [ "$TRAVIS_BRANCH" = "clean-up/deprecated-options" ]; then + ltac2_CI_BRANCH=master + ltac2_CI_GITURL=https://github.com/Zimmi48/ltac2 +fi diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 5c519e46e3..a1950d136e 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -550,6 +550,60 @@ the same way as the {\Coq} kernel handles them. This tells if the printing matching mode is on or off. The default is on. +\subsubsection{Factorization of clauses with same right-hand side} +\label{SetPrintingFactorizableMatchPatterns} +\optindex{Printing Factorizable Match Patterns} + +When several patterns share the same right-hand side, it is +additionally possible to share the clauses using disjunctive patterns. +Assuming that the printing matching mode is on, whether {\Coq}'s +printer shall try to do this kind of factorization is governed by the +following commands: + +\begin{quote} +{\tt Set Printing Factorizable Match Patterns.} +\end{quote} +This tells {\Coq}'s printer to try to use disjunctive patterns. This is the default +behavior. + +\begin{quote} +{\tt Unset Printing Factorizable Match Patterns.} +\end{quote} +This tells {\Coq}'s printer not to try to use disjunctive patterns. + +\begin{quote} +{\tt Test Printing Factorizable Match Patterns.} +\end{quote} +This tells if the factorization of clauses with same right-hand side is +on or off. + +\subsubsection{Use of a default clause} +\label{SetPrintingAllowDefaultClause} +\optindex{Printing Allow Default Clause} + +When several patterns share the same right-hand side which do not +depend on the arguments of the patterns, yet an extra factorization is +possible: the disjunction of patterns can be replaced with a ``{\tt + \_}'' default clause. Assuming that the printing matching mode and +the factorization mode are on, whether {\Coq}'s printer shall try to +use a default clause is governed by the following commands: + +\begin{quote} +{\tt Set Printing Allow Default Clause.} +\end{quote} +This tells {\Coq}'s printer to use a default clause when relevant. This is the default +behavior. + +\begin{quote} +{\tt Unset Printing Allow Default Clause.} +\end{quote} +This tells {\Coq}'s printer not to use a default clause. + +\begin{quote} +{\tt Test Printing Allow Default Clause.} +\end{quote} +This tells if the use of a default clause is allowed. + \subsubsection{Printing of wildcard pattern \optindex{Printing Wildcard}} diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 7034c56081..8d82460a72 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -198,8 +198,6 @@ is understood as {\cpattern} {\tt =>} {\tacexpr}\\ & $|$ & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} {\tt =>} {\tacexpr}\\ -& $|$ & {\tt appcontext} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} - {\tt =>} {\tacexpr}\\ & $|$ & {\tt \_ =>} {\tacexpr}\\ \\ {\it test} & ::= & @@ -876,21 +874,6 @@ Goal True. f (3+4). \end{coq_example} -\item \index{appcontext@\texttt{appcontext}!in pattern} - \optindex{Tactic Compat Context} -For historical reasons, {\tt context} used to consider $n$-ary applications -such as {\tt (f 1 2)} as a whole, and not as a sequence of unary -applications {\tt ((f 1) 2)}. Hence {\tt context [f ?x]} would fail -to find a matching subterm in {\tt (f 1 2)}: if the pattern was a partial -application, the matched subterms would have necessarily been -applications with exactly the same number of arguments. -As a workaround, one could use the following variant of {\tt context}: -\begin{quote} -{\tt appcontext} {\ident} {\tt [} {\cpattern} {\tt ]} -\end{quote} -This syntax is now deprecated, as {\tt context} behaves as intended. The former -behavior can be retrieved with the {\tt Tactic Compat Context} flag. - \end{Variants} \subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}\label{ltac-match-goal} diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 8b78a91b5b..7cc8de85d2 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -188,7 +188,7 @@ and case_expr_eq (e1, n1, p1) (e2, n2, p2) = Option.equal cases_pattern_expr_eq p1 p2 and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) = - List.equal (eq_located (List.equal cases_pattern_expr_eq)) p1 p2 && + List.equal (List.equal cases_pattern_expr_eq) p1 p2 && constr_expr_eq e1 e2 and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) = @@ -260,7 +260,6 @@ let local_binders_loc bll = match bll with (* Legacy functions *) let down_located f (_l, x) = f x -let located_fold_left f x (_l, y) = f x y let is_constructor id = try Globnames.isConstructRef @@ -292,8 +291,7 @@ let ids_of_pattern = let ids_of_pattern_list = List.fold_left - (located_fold_left - (List.fold_left (cases_pattern_fold_names Id.Set.add))) + (List.fold_left (cases_pattern_fold_names Id.Set.add)) Id.Set.empty let ids_of_cases_indtype p = @@ -571,7 +569,7 @@ let expand_binders ?loc mkC bl c = let c = CAst.make ?loc @@ CCases (LetPatternStyle, None, [(e,None,None)], - [(Loc.tag ?loc:loc1 ([(loc1,[p])], c))]) + [(Loc.tag ?loc:loc1 ([[p]], c))]) in (ni :: env, mkC ?loc ([id],Default Explicit,ty) c) in diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bc8debd02d..1330b3741e 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -852,7 +852,7 @@ let rec extern inctx scopes vars r = ) x)) tml in - let eqns = List.map (extern_eqn inctx scopes vars) eqns in + let eqns = List.map (extern_eqn inctx scopes vars) (factorize_eqns eqns) in CCases (sty,rtntypopt',tml,eqns) | GLetTuple (nal,(na,typopt),tm,b) -> @@ -966,9 +966,9 @@ and extern_local_binder scopes vars = function let (assums,ids,l) = extern_local_binder scopes vars l in (assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l) -and extern_eqn inctx scopes vars (loc,(ids,pl,c)) = - Loc.tag ?loc ([loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], - extern inctx scopes vars c) +and extern_eqn inctx scopes vars (loc,(ids,pll,c)) = + let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in + Loc.tag ?loc (pll,extern inctx scopes vars c) and extern_notation (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 977146b2fe..74ae321202 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -958,8 +958,11 @@ let rec has_duplicate = function | [] -> None | x::l -> if Id.List.mem x l then (Some x) else has_duplicate l +let loc_of_multiple_pattern pl = + Loc.merge_opt (cases_pattern_expr_loc (List.hd pl)) (cases_pattern_expr_loc (List.last pl)) + let loc_of_lhs lhs = - Loc.merge_opt (fst (List.hd lhs)) (fst (List.last lhs)) + Loc.merge_opt (loc_of_multiple_pattern (List.hd lhs)) (loc_of_multiple_pattern (List.last lhs)) let check_linearity lhs ids = match has_duplicate ids with @@ -1873,8 +1876,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = intern_local_binder_aux intern ntnvars env bind (* Expands a multiple pattern into a disjunction of multiple patterns *) - and intern_multiple_pattern env n (loc,pl) = + and intern_multiple_pattern env n pl = let idsl_pll = List.map (intern_cases_pattern globalenv (None,env.scopes) empty_alias) pl in + let loc = loc_of_multiple_pattern pl in check_number_of_pattern loc n pl; product_of_cases_patterns empty_alias idsl_pll diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index e0d2d7bf48..8bcdbcc0ef 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -104,7 +104,7 @@ and case_expr = constr_expr (* expression that is being matched * cases_pattern_expr option (* in-clause *) and branch_expr = - (cases_pattern_expr list Loc.located list * constr_expr) Loc.located + (cases_pattern_expr list list * constr_expr) Loc.located and binder_expr = Name.t Loc.located list * binder_kind * constr_expr diff --git a/intf/glob_term.ml b/intf/glob_term.ml index 72c91db6a0..f311d33b8a 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -93,6 +93,14 @@ type fix_recursion_order = [ `any ] fix_recursion_order_g type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr +type 'a disjunctive_cases_clause_g = (Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) Loc.located +type 'a disjunctive_cases_clauses_g = 'a disjunctive_cases_clause_g list +type 'a cases_pattern_disjunction_g = 'a cases_pattern_g list + +type disjunctive_cases_clause = [ `any ] disjunctive_cases_clause_g +type disjunctive_cases_clauses = [ `any ] disjunctive_cases_clauses_g +type cases_pattern_disjunction = [ `any ] cases_pattern_disjunction_g + type 'a extended_glob_local_binder_r = | GLocalAssum of Name.t * binding_kind * 'a glob_constr_g | GLocalDef of Name.t * binding_kind * 'a glob_constr_g * 'a glob_constr_g option diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index a62a079da9..9f9102f7d2 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -154,7 +154,7 @@ let warn_no_native_compiler = (* Wrapper for [native_conv] above *) let native_conv cv_pb sigma env t1 t2 = - if Coq_config.no_native_compiler then begin + if not Coq_config.native_compiler then begin warn_no_native_compiler (); vm_conv cv_pb env t1 t2 end diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 0e41bfc3c4..5150ad4113 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -858,7 +858,7 @@ let export ?except senv dir = } in let ast, symbols = - if !Flags.native_compiler then + if !Flags.output_native_objects then Nativelibrary.dump_library mp dir senv.env str else [], Nativecode.empty_symbols in diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 578a893718..3ef297b1f4 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -204,4 +204,4 @@ let vm_conv cv_pb env t1 t2 = let univs = (univs, checked_universes) in let _ = vm_conv_gen cv_pb env univs t1 t2 in () -let _ = Reduction.set_vm_conv vm_conv +let _ = if Coq_config.bytecode_compiler then Reduction.set_vm_conv vm_conv diff --git a/lib/flags.ml b/lib/flags.ml index 9631da633d..644f66d02b 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -161,12 +161,11 @@ let set_inline_level = (:=) inline_level let get_inline_level () = !inline_level (* Native code compilation for conversion and normalization *) -let native_compiler = ref false +let output_native_objects = ref false (* Print the mod uid associated to a vo file by the native compiler *) let print_mod_uid = ref false -let tactic_context_compat = ref false let profile_ltac = ref false let profile_ltac_cutoff = ref 2.0 diff --git a/lib/flags.mli b/lib/flags.mli index 1b1e264f0c..000862b2c6 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -127,16 +127,12 @@ val set_inline_level : int -> unit val get_inline_level : unit -> int val default_inline_level : int -(** Native code compilation for conversion and normalization *) -val native_compiler : bool ref +(** When producing vo objects, also compile the native-code version *) +val output_native_objects : bool ref (** Print the mod uid associated to a vo file by the native compiler *) val print_mod_uid : bool ref -val tactic_context_compat : bool ref -(** Set to [true] to trigger the compatibility bugged context matching (old - context vs. appcontext) is set. *) - val profile_ltac : bool ref val profile_ltac_cutoff : float ref @@ -208,6 +208,7 @@ let string_of_ppcmds c = let pr_comma () = str "," ++ spc () let pr_semicolon () = str ";" ++ spc () let pr_bar () = str "|" ++ spc () +let pr_spcbar () = str " |" ++ spc () let pr_arg pr x = spc () ++ pr x let pr_non_empty_arg pr x = let pp = pr x in if ismt pp then mt () else spc () ++ pr x let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x diff --git a/lib/pp.mli b/lib/pp.mli index 2d11cad86e..d9be1c5ce9 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -120,6 +120,9 @@ val pr_semicolon : unit -> t val pr_bar : unit -> t (** Well-spaced pipe bar. *) +val pr_spcbar : unit -> t +(** Pipe bar with space before and after. *) + val pr_arg : ('a -> t) -> 'a -> t (** Adds a space in front of its argument. *) diff --git a/library/library.ml b/library/library.ml index 88470d121b..868e26684d 100644 --- a/library/library.ml +++ b/library/library.ml @@ -170,7 +170,7 @@ let register_loaded_library m = let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in let f = prefix ^ "cmo" in let f = Dynlink.adapt_filename f in - if not Coq_config.no_native_compiler then + if Coq_config.native_compiler then Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function @@ -738,7 +738,7 @@ let save_library_to ?todo dir f otab = System.marshal_out_segment f' ch (opaque_table : seg_proofs); close_out ch; (* Writing native code files *) - if !Flags.native_compiler then + if !Flags.output_native_objects then let fn = Filename.dirname f'^"/"^Nativecode.mod_uid_of_dirpath dir in if not (Nativelib.compile_library dir ast fn) then user_err Pp.(str "Could not compile the library to native code.") diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 0cf96d487b..db68a75e09 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -267,17 +267,17 @@ GEXTEND Gram | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)]) + CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([[p]], c2)]) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)]) + CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([[p]], c2)]) | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([(Loc.tag ~loc:!@loc [p])], c2)]) + CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([[p]], c2)]) | "if"; c=operconstr LEVEL "200"; po = return_type; "then"; b1=operconstr LEVEL "200"; "else"; b2=operconstr LEVEL "200" -> @@ -362,7 +362,7 @@ GEXTEND Gram [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ] ; mult_pattern: - [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> (Loc.tag ~loc:!@loc pl) ] ] + [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> pl ] ] ; eqn: [ [ pll = LIST1 mult_pattern SEP "|"; diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 8bf6e48fdb..5a9248d478 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -183,7 +183,9 @@ let with_full_print f a = and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in let old_rawprint = !Flags.raw_print in let old_printuniverses = !Constrextern.print_universes in + let old_printallowmatchdefaultclause = !Detyping.print_allow_match_default_clause in Constrextern.print_universes := true; + Detyping.print_allow_match_default_clause := false; Flags.raw_print := true; Impargs.make_implicit_args false; Impargs.make_strict_implicit_args false; @@ -197,6 +199,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; + Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; Dumpglob.continue (); res with @@ -206,6 +209,7 @@ let with_full_print f a = Impargs.make_contextual_implicit_args old_contextual_implicit_args; Flags.raw_print := old_rawprint; Constrextern.print_universes := old_printuniverses; + Detyping.print_allow_match_default_clause := old_printallowmatchdefaultclause; Dumpglob.continue (); raise reraise diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 8b9eb39837..ebf6e450b1 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -78,11 +78,6 @@ let test_bracket_ident = let hint = G_proofs.hint -let warn_deprecated_appcontext = - CWarnings.create ~name:"deprecated-appcontext" ~category:"deprecated" - (fun () -> strbrk "appcontext is deprecated and will be removed " ++ - strbrk "in a future version") - GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint tactic_mode constr_may_eval constr_eval toplevel_selector @@ -242,12 +237,7 @@ GEXTEND Gram match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; "["; pc = Constr.lconstr_pattern; "]" -> - let mode = not (!Flags.tactic_context_compat) in - Subterm (mode, oid, pc) - | IDENT "appcontext"; oid = OPT Constr.ident; - "["; pc = Constr.lconstr_pattern; "]" -> - warn_deprecated_appcontext ~loc:!@loc (); - Subterm (true,oid, pc) + Subterm (oid, pc) | pc = Constr.lconstr_pattern -> Term pc ] ] ; match_hyps: diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 6aa2f6f898..e5ff473568 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -526,11 +526,9 @@ let pr_goal_selector ~toplevel s = let pr_match_pattern pr_pat = function | Term a -> pr_pat a - | Subterm (b,None,a) -> - (** ppedrot: we don't make difference between [appcontext] and [context] - anymore, and the interpretation is governed by a flag instead. *) + | Subterm (None,a) -> keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]" - | Subterm (b,Some id,a) -> + | Subterm (Some id,a) -> keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]" let pr_match_hyps pr_pat = function diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 9ae8bfe65b..5225420dc4 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -408,7 +408,7 @@ let print_results_filter ~cutoff ~filter = let results = SM.fold (fun _ -> merge_roots ~disjoint:true) !data (empty_treenode root) in let results = merge_roots results Local.(CList.last !stack) in - Feedback.msg_notice (to_string ~cutoff ~filter results) + Feedback.msg_info (to_string ~cutoff ~filter results) ;; let print_results ~cutoff = diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 index 2b1106ee21..f095660638 100644 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.ml4 @@ -13,7 +13,7 @@ open Profile_ltac open Stdarg -DECLARE PLUGIN "profile_ltac_plugin" +DECLARE PLUGIN "ltac_plugin" let tclSET_PROFILING b = Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> set_profiling b)) @@ -22,7 +22,7 @@ TACTIC EXTEND start_ltac_profiling | [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ] END -TACTIC EXTEND stop_profiling +TACTIC EXTEND stop_ltac_profiling | [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] END diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 9bd3efc6b7..ccd555b615 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -81,7 +81,7 @@ type 'a with_bindings_arg = clear_flag * 'a with_bindings (* Type of patterns *) type 'a match_pattern = | Term of 'a - | Subterm of bool * Id.t option * 'a + | Subterm of Id.t option * 'a (* Type of hypotheses for a Match Context rule *) type 'a match_context_hyps = diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index b16b0a7bae..ebffde441d 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -428,9 +428,9 @@ let intern_hyp_location ist ((occs,id),hl) = (* Reads a pattern *) let intern_pattern ist ?(as_type=false) ltacvars = function - | Subterm (b,ido,pc) -> + | Subterm (ido,pc) -> let (metas,pc) = intern_constr_pattern ist ~as_type:false ~ltacvars pc in - ido, metas, Subterm (b,ido,pc) + ido, metas, Subterm (ido,pc) | Term pc -> let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in None, metas, Term pc diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 9e47db1c34..ded902a8fb 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -890,7 +890,7 @@ let interp_intro_pattern_naming_option ist env sigma = function let interp_or_and_intro_pattern_option ist env sigma = function | None -> sigma, None | Some (ArgVar (loc,id)) -> - (match coerce_to_intro_pattern env sigma (Id.Map.find id ist.lfun) with + (match interp_intro_pattern_var loc ist env sigma id with | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l) | _ -> user_err ?loc (str "Cannot coerce to a disjunctive/conjunctive pattern.")) @@ -1040,7 +1040,7 @@ let eval_pattern lfun ist env sigma (bvars,(glob,_),pat as c) = (bvars,instantiate_pattern env sigma lfun pat) let read_pattern lfun ist env sigma = function - | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c) + | Subterm (ido,c) -> Subterm (ido,eval_pattern lfun ist env sigma c) | Term c -> Term (eval_pattern lfun ist env sigma c) (* Reads the hypotheses of a Match Context rule *) diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 918d1faebe..79bf3685e2 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -121,7 +121,7 @@ let subst_raw_may_eval subst = function | ConstrTerm c -> ConstrTerm (subst_glob_constr subst c) let subst_match_pattern subst = function - | Subterm (b,ido,pc) -> Subterm (b,ido,(subst_glob_constr_or_pattern subst pc)) + | Subterm (ido,pc) -> Subterm (ido,(subst_glob_constr_or_pattern subst pc)) | Term pc -> Term (subst_glob_constr_or_pattern subst pc) let rec subst_match_goal_hyps subst = function diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 89b78e5907..e87951dd7f 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -237,7 +237,7 @@ module PatternMatching (E:StaticEnvironment) = struct return lhs with Constr_matching.PatternMatchingFailure -> fail end - | Subterm (with_app_context,id_ctxt,p) -> + | Subterm (id_ctxt,p) -> let rec map s (e, info) = { stream = fun k ctx -> match IStream.peek s with @@ -252,7 +252,7 @@ module PatternMatching (E:StaticEnvironment) = struct | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx) } in - map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error + map (Constr_matching.match_subterm E.env E.sigma p term) imatching_error (** [rule_match_term term rule] matches the term [term] with the diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 047ca509be..8493dbdbb5 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1159,6 +1159,7 @@ let pf_interp_gen_aux ist gl to_ind ((oclr, occ), t) = let (c, ucst), cl = try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr cl) pat occ 1 with NoMatch -> redex_of_pattern env pat, (EConstr.Unsafe.to_constr cl) in + let gl = pf_merge_uc ucst gl in let c = EConstr.of_constr c in let cl = EConstr.of_constr cl in let clr = interp_clr sigma (oclr, (tag_of_cpattern t, c)) in diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 3efb7b9147..4f530a0aec 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -74,7 +74,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;; let no_ct = None, None and no_rt = None in let aliasvar = function - | [_, [{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id) + | [[{ CAst.v = CPatAlias (_, id); loc }]] -> Some (loc,Name id) | _ -> None in let mk_cnotype mp = aliasvar mp, None in let mk_ctype mp t = aliasvar mp, Some t in @@ -86,14 +86,14 @@ let mk_pat c (na, t) = (c, na, t) in GEXTEND Gram GLOBAL: binder_constr; ssr_rtype: [[ "return"; t = operconstr LEVEL "100" -> mk_rtype t ]]; - ssr_mpat: [[ p = pattern -> [Loc.tag ~loc:!@loc [p]] ]]; + ssr_mpat: [[ p = pattern -> [[p]] ]]; ssr_dpat: [ [ mp = ssr_mpat; "in"; t = pattern; rt = ssr_rtype -> mp, mk_ctype mp t, rt | mp = ssr_mpat; rt = ssr_rtype -> mp, mk_cnotype mp, rt | mp = ssr_mpat -> mp, no_ct, no_rt ] ]; ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen ~loc:!@loc dp c ]]; - ssr_elsepat: [[ "else" -> [Loc.tag ~loc:!@loc [CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; + ssr_elsepat: [[ "else" -> [[CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; ssr_else: [[ mp = ssr_elsepat; c = lconstr -> Loc.tag ~loc:!@loc (mp, c) ]]; binder_constr: [ [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index e63a05b781..d6dbad7a95 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1228,7 +1228,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in sigma, [pat] in match pattern with - | None -> do_subst env0 concl0 concl0 1 + | None -> do_subst env0 concl0 concl0 1, Evd.empty_evar_universe_context | Some (sigma, (T rp | In_T rp)) -> let rp = fs sigma rp in let ise = create_evar_defs sigma in @@ -1236,8 +1236,8 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let rp = mk_upat_for env0 sigma0 (ise, rp) all_ok in let find_T, end_T = mk_tpattern_matcher ?raise_NoMatch sigma0 occ rp in let concl = find_T env0 concl0 1 ~k:do_subst in - let _ = end_T () in - concl + let _, _, (_, us, _) = end_T () in + concl, us | Some (sigma, (X_In_T (hole, p) | In_X_In_T (hole, p))) -> let p = fs sigma p in let occ = match pattern with Some (_, X_In_T _) -> occ | _ -> noindex in @@ -1252,8 +1252,8 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma, e_body = pop_evar p_sigma ex p in fs p_sigma (find_X env (fs sigma p) h ~k:(fun env _ -> do_subst env e_body))) in - let _ = end_X () in let _ = end_T () in - concl + let _ = end_X () in let _, _, (_, us, _) = end_T () in + concl, us | Some (sigma, E_In_X_In_T (e, hole, p)) -> let p, e = fs sigma p, fs sigma e in let ex = ex_value hole in @@ -1268,8 +1268,9 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let sigma, e_body = pop_evar p_sigma ex p in fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h -> find_E env e_body h ~k:do_subst))) in - let _ = end_E () in let _ = end_X () in let _ = end_T () in - concl + let _,_,(_,us,_) = end_E () in + let _ = end_X () in let _ = end_T () in + concl, us | Some (sigma, E_As_X_In_T (e, hole, p)) -> let p, e = fs sigma p, fs sigma e in let ex = ex_value hole in @@ -1287,8 +1288,8 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let e_sigma = unify_HO env sigma (EConstr.of_constr e_body) (EConstr.of_constr e) in let e_body = fs e_sigma e in do_subst env e_body e_body h))) in - let _ = end_X () in let _ = end_TE () in - concl + let _ = end_X () in let _,_,(_,us,_) = end_TE () in + concl, us ;; let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) = @@ -1306,12 +1307,14 @@ let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h = let find_R, conclude = let r = ref None in (fun env c _ h' -> - do_once r (fun () -> c, Evd.empty_evar_universe_context); + do_once r (fun () -> c); if do_make_rel then mkRel (h'+h-1) else c), - (fun _ -> if !r = None then redex_of_pattern env pat else assert_done r) in - let cl = eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in + (fun _ -> if !r = None then fst(redex_of_pattern env pat) + else assert_done r) in + let cl, us = + eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in let e = conclude cl in - e, cl + (e, us), cl ;; (* clenup interface for external use *) @@ -1319,6 +1322,10 @@ let mk_tpattern ?p_origin env sigma0 sigma_t f dir c = mk_tpattern ?p_origin env sigma0 sigma_t f dir c ;; +let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = + fst (eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst) +;; + let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = let p = EConstr.Unsafe.to_constr p in let concl = EConstr.Unsafe.to_constr concl in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 4f3669a2b9..1207c967b5 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1566,11 +1566,9 @@ substituer après par les initiaux *) (* builds the matrix of equations testing that each eqn has n patterns * and linearizing the _ patterns. - * Syntactic correctness has already been done in astterm *) + * Syntactic correctness has already been done in constrintern *) let matx_of_eqns env eqns = - let build_eqn (loc,(ids,lpat,rhs)) = - let initial_lpat,initial_rhs = lpat,rhs in - let initial_rhs = rhs in + let build_eqn (loc,(ids,initial_lpat,initial_rhs)) = let avoid = ids_of_named_context_val (named_context_val env) in let avoid = List.fold_left (fun accu id -> Id.Set.add id accu) avoid ids in let rhs = diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 478ba73fd5..ec7c3077fb 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -206,7 +206,7 @@ let merge_binding sigma allow_bound_rels ctx n cT subst = in constrain sigma n c subst -let matches_core env sigma allow_partial_app allow_bound_rels +let matches_core env sigma allow_bound_rels (binding_vars,pat) c = let open EConstr in let convref ref c = @@ -260,7 +260,7 @@ let matches_core env sigma allow_partial_app allow_bound_rels | PApp (PApp (h, a1), a2), _ -> sorec ctx env subst (PApp(h,Array.append a1 a2)) t - | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app -> + | PApp (PMeta meta,args1), App (c2,args2) -> (let diff = Array.length args2 - Array.length args1 in if diff >= 0 then let args21, args22 = Array.chop diff args2 in @@ -373,14 +373,14 @@ let matches_core env sigma allow_partial_app allow_bound_rels in sorec [] env (Id.Map.empty, Id.Map.empty) pat c -let matches_core_closed env sigma allow_partial_app pat c = - let names, subst = matches_core env sigma allow_partial_app false pat c in +let matches_core_closed env sigma pat c = + let names, subst = matches_core env sigma false pat c in (names, Id.Map.map snd subst) -let extended_matches env sigma = matches_core env sigma true true +let extended_matches env sigma = matches_core env sigma true let matches env sigma pat c = - snd (matches_core_closed env sigma true (Id.Set.empty,pat) c) + snd (matches_core_closed env sigma (Id.Set.empty,pat) c) let special_meta = (-1) @@ -405,9 +405,9 @@ let matches_head env sigma pat c = matches env sigma pat head (* Tells if it is an authorized occurrence and if the instance is closed *) -let authorized_occ env sigma partial_app closed pat c mk_ctx = +let authorized_occ env sigma closed pat c mk_ctx = try - let subst = matches_core_closed env sigma partial_app pat c in + let subst = matches_core_closed env sigma pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst) then (fun next -> next ()) else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next) @@ -416,10 +416,10 @@ let authorized_occ env sigma partial_app closed pat c mk_ctx = let subargs env v = Array.map_to_list (fun c -> (env, c)) v (* Tries to match a subterm of [c] with [pat] *) -let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = +let sub_match ?(closed=true) env sigma pat c = let open EConstr in let rec aux env c mk_ctx next = - let here = authorized_occ env sigma partial_app closed pat c mk_ctx in + let here = authorized_occ env sigma closed pat c mk_ctx in let next () = match EConstr.kind sigma c with | Cast (c1,k,c2) -> let next_mk_ctx = function @@ -449,34 +449,12 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let env' = EConstr.push_rel (LocalDef (x,c1,t)) env in try_aux [(env, c1); (env', c2)] next_mk_ctx next | App (c1,lc) -> - let topdown = true in - if partial_app then - if topdown then - let lc1 = Array.sub lc 0 (Array.length lc - 1) in - let app = mkApp (c1,lc1) in - let mk_ctx = function - | [app';c] -> mk_ctx (mkApp (app',[|c|])) - | _ -> assert false in - try_aux [(env, app); (env, Array.last lc)] mk_ctx next - else - let rec aux2 app args next = - match args with - | [] -> - let mk_ctx le = - mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - let sub = (env, c1) :: subargs env lc in - try_aux sub mk_ctx next - | arg :: args -> - let app = mkApp (app,[|arg|]) in - let next () = aux2 app args next in - let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in - aux env app mk_ctx next in - aux2 c1 (Array.to_list lc) next - else - let mk_ctx le = - mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in - let sub = (env, c1) :: subargs env lc in - try_aux sub mk_ctx next + let lc1 = Array.sub lc 0 (Array.length lc - 1) in + let app = mkApp (c1,lc1) in + let mk_ctx = function + | [app';c] -> mk_ctx (mkApp (app',[|c|])) + | _ -> assert false in + try_aux [(env, app); (env, Array.last lc)] mk_ctx next | Case (ci,hd,c1,lc) -> let next_mk_ctx = function | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) @@ -499,14 +477,11 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let sub = subargs env types @ subargs env bodies in try_aux sub next_mk_ctx next | Proj (p,c') -> - let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in - if partial_app then - try - let term = Retyping.expand_projection env sigma p c' [] in - aux env term mk_ctx next - with Retyping.RetypeError _ -> next () - else - try_aux [env, c'] next_mk_ctx next + begin try + let term = Retyping.expand_projection env sigma p c' [] in + aux env term mk_ctx next + with Retyping.RetypeError _ -> next () + end | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> next () in @@ -527,13 +502,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = let result () = aux env c (fun x -> x) lempty in IStream.thunk result -let match_subterm env sigma pat c = sub_match env sigma (Id.Set.empty,pat) c - -let match_appsubterm env sigma pat c = - sub_match ~partial_app:true env sigma (Id.Set.empty,pat) c - -let match_subterm_gen env sigma app pat c = - sub_match ~partial_app:app env sigma pat c +let match_subterm env sigma pat c = sub_match env sigma pat c let is_matching env sigma pat c = try let _ = matches env sigma pat c in true @@ -545,5 +514,5 @@ let is_matching_head env sigma pat c = let is_matching_appsubterm ?(closed=true) env sigma pat c = let pat = (Id.Set.empty,pat) in - let results = sub_match ~partial_app:true ~closed env sigma pat c in + let results = sub_match ~closed env sigma pat c in not (IStream.is_empty results) diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 60e1c34a15..e4d9ff9e1e 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -61,18 +61,10 @@ type matching_result = { m_sub : bound_ident_map * patvar_map; m_ctx : EConstr.t } -(** [match_subterm n pat c] returns the substitution and the context - corresponding to each **closed** subterm of [c] matching [pat]. *) -val match_subterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t - -(** [match_appsubterm pat c] returns the substitution and the context +(** [match_subterm pat c] returns the substitution and the context corresponding to each **closed** subterm of [c] matching [pat], considering application contexts as well. *) -val match_appsubterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t - -(** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *) -val match_subterm_gen : env -> Evd.evar_map -> - bool (** true = with app context *) -> +val match_subterm : env -> Evd.evar_map -> binding_bound_vars * constr_pattern -> constr -> matching_result IStream.t diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 6527ba9355..23993243f4 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -252,6 +252,89 @@ let lookup_index_as_renamed env sigma t n = in lookup n 1 t (**********************************************************************) +(* Factorization of match patterns *) + +let print_factorize_match_patterns = ref true + +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "factorization of \"match\" patterns in printing"; + optkey = ["Printing";"Factorizable";"Match";"Patterns"]; + optread = (fun () -> !print_factorize_match_patterns); + optwrite = (fun b -> print_factorize_match_patterns := b) } + +let print_allow_match_default_clause = ref true + +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "possible use of \"match\" default pattern in printing"; + optkey = ["Printing";"Allow";"Match";"Default";"Clause"]; + optread = (fun () -> !print_allow_match_default_clause); + optwrite = (fun b -> print_allow_match_default_clause := b) } + +let rec join_eqns (ids,rhs as x) patll = function + | (loc,(ids',patl',rhs') as eqn')::rest -> + if not !Flags.raw_print && !print_factorize_match_patterns && + List.eq_set Id.equal ids ids' && glob_constr_eq rhs rhs' + then + join_eqns x (patl'::patll) rest + else + let eqn,rest = join_eqns x patll rest in + eqn, eqn'::rest + | [] -> + patll, [] + +let number_of_patterns (_gloc,(_ids,patll,_rhs)) = List.length patll + +let is_default_candidate (_gloc,(ids,_patll,_rhs) ) = ids = [] + +let rec move_more_factorized_default_candidate_to_end eqn n = function + | eqn' :: eqns -> + let set,get = set_temporary_memory () in + if is_default_candidate eqn' && set (number_of_patterns eqn') >= n then + let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn' (get ()) eqns in + if isbest then false, dft, eqns else false, dft, eqn' :: eqns + else + let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn n eqns in + isbest, dft, eqn' :: eqns + | [] -> true, Some eqn, [] + +let rec select_default_clause = function + | eqn :: eqns -> + let set,get = set_temporary_memory () in + if is_default_candidate eqn && set (number_of_patterns eqn) > 1 then + let isbest, dft, eqns = move_more_factorized_default_candidate_to_end eqn (get ()) eqns in + if isbest then dft, eqns else dft, eqn :: eqns + else + let dft, eqns = select_default_clause eqns in dft, eqn :: eqns + | [] -> None, [] + +let factorize_eqns eqns = + let rec aux found = function + | (loc,(ids,patl,rhs))::rest -> + let patll,rest = join_eqns (ids,rhs) [patl] rest in + aux ((loc,(ids,patll,rhs))::found) rest + | [] -> + found in + let eqns = aux [] (List.rev eqns) in + let mk_anon patl = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl in + if not !Flags.raw_print && !print_allow_match_default_clause && eqns <> [] then + match select_default_clause eqns with + (* At least two clauses and the last one is disjunctive with no variables *) + | Some (gloc,([],patl::_::_,rhs)), (_::_ as eqns) -> eqns@[gloc,([],[mk_anon patl],rhs)] + (* Only one clause which is disjunctive with no variables: we keep at least one constructor *) + (* so that it is not interpreted as a dummy "match" *) + | Some (gloc,([],patl::patl'::_,rhs)), [] -> [gloc,([],[patl;mk_anon patl'],rhs)] + | Some (_,((_::_,_,_ | _,([]|[_]),_))), _ -> assert false + | None, eqns -> eqns + else + eqns + +(**********************************************************************) (* Fragile algorithm to reverse pattern-matching compilation *) let update_name sigma na ((_,(e,_)),c) = @@ -284,13 +367,12 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c = let rec build_tree na isgoal e sigma ci cl = let mkpat n rhs pl = DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in let cnl = ci.ci_pp_info.cstr_tags in - let cna = ci.ci_cstr_nargs in List.flatten (List.init (Array.length cl) - (fun i -> contract_branch isgoal e sigma (cnl.(i),cna.(i),mkpat i,cl.(i)))) + (fun i -> contract_branch isgoal e sigma (cnl.(i),mkpat i,cl.(i)))) and align_tree nal isgoal (e,c as rhs) sigma = match nal with - | [] -> [[],rhs] + | [] -> [Id.Set.empty,[],rhs] | na::nal -> match EConstr.kind sigma c with | Case (ci,p,c,cl) when @@ -300,19 +382,20 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with computable sigma p (List.length ci.ci_pp_info.ind_tags) (* FIXME: can do better *) -> let clauses = build_tree na isgoal e sigma ci cl in List.flatten - (List.map (fun (pat,rhs) -> + (List.map (fun (ids,pat,rhs) -> let lines = align_tree nal isgoal rhs sigma in - List.map (fun (hd,rest) -> pat::hd,rest) lines) + List.map (fun (ids',hd,rest) -> Id.Set.fold Id.Set.add ids ids',pat::hd,rest) lines) clauses) | _ -> - let pat = DAst.make @@ PatVar(update_name sigma na rhs) in - let mat = align_tree nal isgoal rhs sigma in - List.map (fun (hd,rest) -> pat::hd,rest) mat + let na = update_name sigma na rhs in + let pat = DAst.make @@ PatVar na in + let mat = align_tree nal isgoal rhs sigma in + List.map (fun (ids,hd,rest) -> Nameops.Name.fold_right Id.Set.add na ids,pat::hd,rest) mat -and contract_branch isgoal e sigma (cdn,can,mkpat,b) = - let nal,rhs = decomp_branch cdn [] isgoal e sigma b in +and contract_branch isgoal e sigma (cdn,mkpat,rhs) = + let nal,rhs = decomp_branch cdn [] isgoal e sigma rhs in let mat = align_tree nal isgoal rhs sigma in - List.map (fun (hd,rhs) -> (mkpat rhs hd,rhs)) mat + List.map (fun (ids,hd,rhs) -> ids,mkpat rhs hd,rhs) mat (**********************************************************************) (* Transform internal representation of pattern-matching into list of *) @@ -648,7 +731,7 @@ and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl = try if !Flags.raw_print || not (reverse_matching ()) then raise Exit; let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in - List.map (fun (pat,((avoid,env),c)) -> Loc.tag ([],[pat],detype d flags avoid env sigma c)) + List.map (fun (ids,pat,((avoid,env),c)) -> Loc.tag (Id.Set.elements ids,[pat],detype d flags avoid env sigma c)) mat with e when CErrors.noncritical e -> Array.to_list diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index cb1c0d8d4b..f150cb1956 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -26,10 +26,20 @@ val print_universes : bool ref (** If true, prints full local context of evars *) val print_evar_arguments : bool ref +(** If true, contract branches with same r.h.s. and same matching + variables in a disjunctive pattern *) +val print_factorize_match_patterns : bool ref + +(** If true and the last non unique clause of a "match" is a + variable-free disjunctive pattern, turn it into a catch-call case *) +val print_allow_match_default_clause : bool ref + val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern val subst_glob_constr : substitution -> glob_constr -> glob_constr +val factorize_eqns : 'a cases_clauses_g -> 'a disjunctive_cases_clauses_g + (** [detype isgoal avoid ctx c] turns a closed [c], into a glob_constr de Bruijn indexes are turned to bound names, avoiding names in [avoid] [isgoal] tells if naming must avoid global-level synonyms as intro does diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index dafe8cb269..79e0afa72b 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -436,11 +436,11 @@ let stop_profiler m_pid = match profiler_platform() with "Unix (Linux)" -> stop_profiler_linux m_pid | _ -> () - + let native_norm env sigma c ty = let c = EConstr.Unsafe.to_constr c in let ty = EConstr.Unsafe.to_constr ty in - if Coq_config.no_native_compiler then + if not Coq_config.native_compiler then user_err Pp.(str "Native_compute reduction has been disabled at configure time.") else let penv = Environ.pre_env env in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index d9994c4733..ac88468545 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -294,12 +294,12 @@ sig val append_app : 'a array -> 'a t -> 'a t val decomp : 'a t -> ('a * 'a t) option val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t) - val equal : ('a * int -> 'a * int -> bool) -> (('a, 'a) pfixpoint * int -> ('a, 'a) pfixpoint * int -> bool) - -> 'a t -> 'a t -> (int * int) option + val equal : ('a -> 'a -> bool) -> (('a, 'a) pfixpoint -> ('a, 'a) pfixpoint -> bool) + -> 'a t -> 'a t -> bool val compare_shape : 'a t -> 'a t -> bool val map : ('a -> 'a) -> 'a t -> 'a t val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> - constr t -> constr t -> 'a * int * int + constr t -> constr t -> 'a val append_app_list : 'a list -> 'a t -> 'a t val strip_app : 'a t -> 'a t * 'a t val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option @@ -397,44 +397,37 @@ struct else (l.(j), sk) let equal f f_fix sk1 sk2 = - let equal_cst_member x lft1 y lft2 = + let equal_cst_member x y = match x, y with | Cst_const (c1,u1), Cst_const (c2, u2) -> - Constant.equal c1 c2 && Univ.Instance.equal u1 u2 + Constant.equal c1 c2 && Univ.Instance.equal u1 u2 | Cst_proj p1, Cst_proj p2 -> - Constant.equal (Projection.constant p1) (Projection.constant p2) + Constant.equal (Projection.constant p1) (Projection.constant p2) | _, _ -> false in - let rec equal_rec sk1 lft1 sk2 lft2 = + let rec equal_rec sk1 sk2 = match sk1,sk2 with - | [],[] -> Some (lft1,lft2) + | [],[] -> true | App a1 :: s1, App a2 :: s2 -> - let t1,s1' = decomp_node_last a1 s1 in - let t2,s2' = decomp_node_last a2 s2 in - if f (t1,lft1) (t2,lft2) then equal_rec s1' lft1 s2' lft2 else None + let t1,s1' = decomp_node_last a1 s1 in + let t2,s2' = decomp_node_last a2 s2 in + (f t1 t2) && (equal_rec s1' s2') | Case (_,t1,a1,_) :: s1, Case (_,t2,a2,_) :: s2 -> - if f (t1,lft1) (t2,lft2) && CArray.equal (fun x y -> f (x,lft1) (y,lft2)) a1 a2 - then equal_rec s1 lft1 s2 lft2 - else None + f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2 | (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) -> - if Int.equal n1 n2 && Int.equal m1 m2 - && Constant.equal (Projection.constant p) (Projection.constant p2) - then equal_rec s1 lft1 s2 lft2 - else None + Int.equal n1 n2 && Int.equal m1 m2 + && Constant.equal (Projection.constant p) (Projection.constant p2) + && equal_rec s1 s2 | Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' -> - if f_fix (f1,lft1) (f2,lft2) then - match equal_rec (List.rev s1) lft1 (List.rev s2) lft2 with - | None -> None - | Some (lft1',lft2') -> equal_rec s1' lft1' s2' lft2' - else None + f_fix f1 f2 + && equal_rec (List.rev s1) (List.rev s2) + && equal_rec s1' s2' | Cst (c1,curr1,remains1,params1,_)::s1', Cst (c2,curr2,remains2,params2,_)::s2' -> - if equal_cst_member c1 lft1 c2 lft2 then - match equal_rec (List.rev params1) lft1 (List.rev params2) lft2 with - | Some (lft1',lft2') -> equal_rec s1' lft1' s2' lft2' - | None -> None - else None - | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> None - in equal_rec (List.rev sk1) 0 (List.rev sk2) 0 + equal_cst_member c1 c2 + && equal_rec (List.rev params1) (List.rev params2) + && equal_rec s1' s2' + | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> false + in equal_rec (List.rev sk1) (List.rev sk2) let compare_shape stk1 stk2 = let rec compare_rec bal stk1 stk2 = @@ -455,34 +448,26 @@ struct exception IncompatibleFold2 let fold2 f o sk1 sk2 = - let rec aux o lft1 sk1 lft2 sk2 = - let fold_array = - Array.fold_left2 (fun a x y -> f a (Vars.lift lft1 x) (Vars.lift lft2 y)) - in + let rec aux o sk1 sk2 = match sk1,sk2 with - | [], [] -> o,lft1,lft2 + | [], [] -> o | App n1 :: q1, App n2 :: q2 -> - let t1,l1 = decomp_node_last n1 q1 in - let t2,l2 = decomp_node_last n2 q2 in - aux (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2)) - lft1 l1 lft2 l2 + let t1,l1 = decomp_node_last n1 q1 in + let t2,l2 = decomp_node_last n2 q2 in + aux (f o t1 t2) l1 l2 | Case (_,t1,a1,_) :: q1, Case (_,t2,a2,_) :: q2 -> - aux (fold_array - (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2)) - a1 a2) lft1 q1 lft2 q2 + aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2 | Proj (n1,m1,p1,_) :: q1, Proj (n2,m2,p2,_) :: q2 -> - aux o lft1 q1 lft2 q2 + aux o q1 q2 | Fix ((_,(_,a1,b1)),s1,_) :: q1, Fix ((_,(_,a2,b2)),s2,_) :: q2 -> - let (o',lft1',lft2') = aux (fold_array (fold_array o b1 b2) a1 a2) - lft1 (List.rev s1) lft2 (List.rev s2) in - aux o' lft1' q1 lft2' q2 + let o' = aux (Array.fold_left2 f (Array.fold_left2 f o b1 b2) a1 a2) (List.rev s1) (List.rev s2) in + aux o' q1 q2 | Cst (cst1,_,_,params1,_) :: q1, Cst (cst2,_,_,params2,_) :: q2 -> - let (o',lft1',lft2') = - aux o lft1 (List.rev params1) lft2 (List.rev params2) - in aux o' lft1' q1 lft2' q2 + let o' = aux o (List.rev params1) (List.rev params2) in + aux o' q1 q2 | (((App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> - raise IncompatibleFold2 - in aux o 0 (List.rev sk1) 0 (List.rev sk2) + raise IncompatibleFold2 + in aux o (List.rev sk1) (List.rev sk2) let rec map f x = List.map (function | (Proj (_,_,_,_)) as e -> e @@ -535,12 +520,12 @@ struct let list_of_app_stack s = let rec aux = function | App (i,a,j) :: s -> - let (k,(args',s')) = aux s in - let a' = Array.map (Vars.lift k) (Array.sub a i (j - i + 1)) in - k,(Array.fold_right (fun x y -> x::y) a' args', s') - | s -> (0,([],s)) in - let (lft,(out,s')) = aux s in - let init = match s' with [] when Int.equal lft 0 -> true | _ -> false in + let (args',s') = aux s in + let a' = Array.sub a i (j - i + 1) in + (Array.fold_right (fun x y -> x::y) a' args', s') + | s -> ([],s) in + let (out,s') = aux s in + let init = match s' with [] -> true | _ -> false in Option.init init out let assign s p c = @@ -845,11 +830,9 @@ let _ = Goptions.declare_bool_option { } let equal_stacks sigma (x, l) (y, l') = - let f_equal (x,lft1) (y,lft2) = eq_constr sigma (Vars.lift lft1 x) (Vars.lift lft2 y) in - let eq_fix (a,b) (c,d) = f_equal (mkFix a, b) (mkFix c, d) in - match Stack.equal f_equal eq_fix l l' with - | None -> false - | Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2) + let f_equal x y = eq_constr sigma x y in + let eq_fix a b = f_equal (mkFix a) (mkFix b) in + Stack.equal f_equal eq_fix l l' && f_equal x y let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let open Context.Named.Declaration in diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 7e12d263aa..a277864c92 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -100,7 +100,7 @@ module Stack : sig @return the result and the lifts to apply on the terms @raise IncompatibleFold2 when [sk1] and [sk2] have incompatible shapes *) val fold2 : ('a -> constr -> constr -> 'a) -> 'a -> - constr t -> constr t -> 'a * int * int + constr t -> constr t -> 'a val map : ('a -> 'a) -> 'a t -> 'a t val append_app_list : 'a list -> 'a t -> 'a t diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 08329391d5..30674fee27 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1077,13 +1077,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e in try let opt' = {opt with with_types = false} in - let (substn,_,_) = Reductionops.Stack.fold2 + let substn = Reductionops.Stack.fold2 (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u)) (evd,ms,es) us2 us in - let (substn,_,_) = Reductionops.Stack.fold2 + let substn = Reductionops.Stack.fold2 (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u)) substn params1 params in - let (substn,_,_) = Reductionops.Stack.fold2 (fun s u1 u2 -> unirec_rec curenvnb pb opt' s u1 u2) substn ts ts1 in + let substn = Reductionops.Stack.fold2 (fun s u1 u2 -> unirec_rec curenvnb pb opt' s u1 u2) substn ts ts1 in let app = mkApp (c, Array.rev_of_list ks) in (* let substn = unirec_rec curenvnb pb b false substn t cN in *) unirec_rec curenvnb pb opt' substn c1 app diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b5b8987e33..e395bdbc63 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -365,4 +365,4 @@ let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 = Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> Vconv.vm_conv_gen pb) ~catch_incon:true ~pb env sigma t1 t2 -let _ = Reductionops.set_vm_infer_conv vm_infer_conv +let _ = if Coq_config.bytecode_compiler then Reductionops.set_vm_infer_conv vm_infer_conv diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 2abbc389fa..51735bc9e1 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -286,7 +286,7 @@ let tag_var = tag Tag.variable pr_reference r, latom | CPatOr pl -> - hov 0 (prlist_with_sep pr_bar (pr_patt spc (lpator,L)) pl), lpator + hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator | CPatNotation ("( _ )",([p],[]),[]) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom @@ -311,11 +311,10 @@ let tag_var = tag Tag.variable let pr_patt = pr_patt mt let pr_eqn pr (loc,(pl,rhs)) = - let pl = List.map snd pl in spc() ++ hov 4 (pr_with_comments ?loc (str "| " ++ - hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl + hov 0 (prlist_with_sep pr_spcbar (prlist_with_sep sep_v (pr_patt ltop)) pl ++ str " =>") ++ pr_sep_com spc (pr ltop) rhs)) @@ -402,7 +401,7 @@ let tag_var = tag Tag.variable | { v = CProdN ([],c) } -> extract_prod_binders c | { loc; v = CProdN ([[_,Name id],bk,t], - { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([_,[p]],b))])} ) } + { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} ) } when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) -> let bl,c = extract_prod_binders b in CLocalPattern (loc, (p,None)) :: bl, c @@ -418,7 +417,7 @@ let tag_var = tag Tag.variable | CLambdaN ([],c) -> extract_lam_binders c | CLambdaN ([[_,Name id],bk,t], - { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([_,[p]],b))])} ) + { v = CCases (LetPatternStyle,None, [{ v = CRef (Ident (_,id'),None)},None,None],[(_,([[p]],b))])} ) when Id.equal id id' && not (Id.Set.mem id (free_vars_of_constr_expr b)) -> let bl,c = extract_lam_binders b in CLocalPattern (ce.loc,(p,None)) :: bl, c @@ -650,7 +649,7 @@ let tag_var = tag Tag.variable hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"), latom ) - | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([(loc,[p])],b))]) -> + | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([[p]],b))]) -> return ( hv 0 ( keyword "let" ++ spc () ++ str"'" ++ diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 6052ba3672..9a5d4e154e 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -25,8 +25,11 @@ open Misctypes (* call by value normalisation function using the virtual machine *) let cbv_vm env sigma c = - let ctyp = Retyping.get_type_of env sigma c in - Vnorm.cbv_vm env sigma c ctyp + if Coq_config.bytecode_compiler then + let ctyp = Retyping.get_type_of env sigma c in + Vnorm.cbv_vm env sigma c ctyp + else + compute env sigma c let warn_native_compute_disabled = CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler" @@ -34,12 +37,12 @@ let warn_native_compute_disabled = strbrk "native_compute disabled at configure time; falling back to vm_compute.") let cbv_native env sigma c = - if Coq_config.no_native_compiler then - (warn_native_compute_disabled (); - cbv_vm env sigma c) - else + if Coq_config.native_compiler then let ctyp = Retyping.get_type_of env sigma c in Nativenorm.native_norm env sigma c ctyp + else + (warn_native_compute_disabled (); + cbv_vm env sigma c) let whd_cbn flags env sigma t = let (state,_) = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 839090903e..508040ec18 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -59,28 +59,6 @@ let typ_of env sigma c = open Goptions -(* Option for 8.2 compatibility *) -let dependent_propositions_elimination = ref true - -let use_dependent_propositions_elimination () = - !dependent_propositions_elimination - -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "dependent-propositions-elimination tactic"; - optkey = ["Dependent";"Propositions";"Elimination"]; - optread = (fun () -> !dependent_propositions_elimination) ; - optwrite = (fun b -> dependent_propositions_elimination := b) } - -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "trigger bugged context matching compatibility"; - optkey = ["Tactic";"Compat";"Context"]; - optread = (fun () -> !Flags.tactic_context_compat) ; - optwrite = (fun b -> Flags.tactic_context_compat := b) } - let apply_solve_class_goals = ref false let _ = @@ -4149,8 +4127,7 @@ let guess_elim isrec dep s hyp0 gl = let env = Tacmach.New.pf_env gl in let sigma = Tacmach.New.project gl in let u = EInstance.kind (Tacmach.New.project gl) u in - if use_dependent_propositions_elimination () && dep = Some true - then + if dep then let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in let ind = EConstr.of_constr ind in (sigma, ind) @@ -4182,11 +4159,10 @@ let find_induction_type isrec elim hyp0 gl = match elim with | None -> let sort = Tacticals.New.elimination_sort_of_goal gl in - let _, (elimc,elimt),_ = - guess_elim isrec None sort hyp0 gl in - let scheme = compute_elim_sig sigma ~elimc elimt in - (* We drop the scheme waiting to know if it is dependent *) - scheme, ElimOver (isrec,hyp0) + let _, (elimc,elimt),_ = guess_elim isrec false sort hyp0 gl in + let scheme = compute_elim_sig sigma ~elimc elimt in + (* We drop the scheme waiting to know if it is dependent *) + scheme, ElimOver (isrec,hyp0) | Some e -> let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in let scheme = compute_elim_sig sigma ~elimc elimt in @@ -4217,7 +4193,7 @@ let get_eliminator elim dep s gl = | ElimUsing (elim,indsign) -> Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign | ElimOver (isrec,id) -> - let evd, (elimc,elimt),_ as elims = guess_elim isrec (Some dep) s id gl in + let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in let _, (l, s) = compute_elim_signature elims id in let branchlengthes = List.map (fun d -> assert (RelDecl.is_local_assum d); pi1 (decompose_prod_letin (Tacmach.New.project gl) (RelDecl.get_type d))) (List.rev s.branches) diff --git a/test-suite/bugs/closed/6378.v b/test-suite/bugs/closed/6378.v new file mode 100644 index 0000000000..d0ef090d08 --- /dev/null +++ b/test-suite/bugs/closed/6378.v @@ -0,0 +1,4 @@ +Goal True. + start ltac profiling. + stop ltac profiling. +Abort. diff --git a/test-suite/bugs/closed/gh6384.v b/test-suite/bugs/closed/gh6384.v new file mode 100644 index 0000000000..cec84642fb --- /dev/null +++ b/test-suite/bugs/closed/gh6384.v @@ -0,0 +1,5 @@ +Theorem test (A:Prop) : A \/ A -> A. + Fail intro H; destruct H as H. + (* Error: Disjunctive/conjunctive introduction pattern expected. *) + Fail intros H; destruct H as H. +Abort. diff --git a/test-suite/bugs/closed/gh6385.v b/test-suite/bugs/closed/gh6385.v new file mode 100644 index 0000000000..3bbb664f4f --- /dev/null +++ b/test-suite/bugs/closed/gh6385.v @@ -0,0 +1,5 @@ +Theorem test (A:Prop) : A \/ A -> A. + Fail let H := idtac in intros H; destruct H as H'. + (* Disjunctive/conjunctive introduction pattern expected. *) + Fail let H' := idtac in intros H; destruct H as H'. +Abort. diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 97fa8e2542..419dcadb4c 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -95,8 +95,7 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl x : nat n, n0 := match x + 0 with - | 0 => 0 - | S _ => 0 + | 0 | S _ => 0 end : nat e, e0 := match x + 0 as y return (y = y) with @@ -104,8 +103,7 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl | S n => eq_refl end : x + 0 = x + 0 n1, n2 := match x with - | 0 => 0 - | S _ => 0 + | 0 | S _ => 0 end : nat e1, e2 := match x return (x = x) with | 0 => eq_refl @@ -126,3 +124,48 @@ fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl end : p = p /\ p = p ============================ eq_refl = eq_refl +fun x : comparison => match x with + | Eq => 1 + | _ => 0 + end + : comparison -> nat +fun x : comparison => match x with + | Eq => 1 + | Lt => 0 + | Gt => 0 + end + : comparison -> nat +fun x : comparison => match x with + | Eq => 1 + | Lt | Gt => 0 + end + : comparison -> nat +fun x : comparison => +match x return nat with +| Eq => S O +| Lt => O +| Gt => O +end + : forall _ : comparison, nat +fun x : K => match x with + | a3 | a4 => 3 + | _ => 2 + end + : K -> nat +fun x : K => match x with + | a1 | a2 => 4 + | a3 => 3 + | _ => 2 + end + : K -> nat +fun x : K => match x with + | a1 | a2 => 4 + | a4 => 3 + | _ => 2 + end + : K -> nat +fun x : K => match x with + | a1 | a3 | a4 => 3 + | _ => 2 + end + : K -> nat diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 17fee3303d..caf3b28701 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -1,5 +1,7 @@ (* Cases with let-in in constructors types *) +Unset Printing Allow Match Default Clause. + Inductive t : Set := k : let x := t in x -> x. @@ -184,3 +186,33 @@ let p := fresh "p" in |- eq_refl ?p = _ => pose (match eq_refl p in _ = z return p=p /\ z=z with eq_refl => conj eq_refl eq_refl end) end. Show. + +Set Printing Allow Match Default Clause. + +(***************************************************) +(* Testing strategy for factorizing cases branches *) + +(* Factorization + default clause *) +Check fun x => match x with Eq => 1 | _ => 0 end. + +(* No factorization *) +Unset Printing Factorizable Match Patterns. +Check fun x => match x with Eq => 1 | _ => 0 end. +Set Printing Factorizable Match Patterns. + +(* Factorization but no default clause *) +Unset Printing Allow Match Default Clause. +Check fun x => match x with Eq => 1 | _ => 0 end. +Set Printing Allow Match Default Clause. + +(* No factorization in printing all mode *) +Set Printing All. +Check fun x => match x with Eq => 1 | _ => 0 end. +Unset Printing All. + +(* Several clauses *) +Inductive K := a1|a2|a3|a4|a5|a6. +Check fun x => match x with a3 | a4 => 3 | _ => 2 end. +Check fun x => match x with a3 => 3 | a2 | a1 => 4 | _ => 2 end. +Check fun x => match x with a4 => 3 | a2 | a1 => 4 | _ => 2 end. +Check fun x => match x with a3 | a4 | a1 => 3 | _ => 2 end. diff --git a/test-suite/output/InvalidDisjunctiveIntro.out b/test-suite/output/InvalidDisjunctiveIntro.out new file mode 100644 index 0000000000..25a306b458 --- /dev/null +++ b/test-suite/output/InvalidDisjunctiveIntro.out @@ -0,0 +1,16 @@ +The command has indeed failed with message: +Cannot coerce to a disjunctive/conjunctive pattern. +The command has indeed failed with message: +Disjunctive/conjunctive introduction pattern expected. +The command has indeed failed with message: +Cannot coerce to a disjunctive/conjunctive pattern. +The command has indeed failed with message: +Cannot coerce to a disjunctive/conjunctive pattern. +The command has indeed failed with message: +Ltac variable H is bound to <tactic closure> which cannot be coerced to +an introduction pattern. +The command has indeed failed with message: +Disjunctive/conjunctive introduction pattern expected. +The command has indeed failed with message: +Ltac variable H' is bound to <tactic closure> which cannot be coerced to +an introduction pattern. diff --git a/test-suite/output/InvalidDisjunctiveIntro.v b/test-suite/output/InvalidDisjunctiveIntro.v new file mode 100644 index 0000000000..4febdf0344 --- /dev/null +++ b/test-suite/output/InvalidDisjunctiveIntro.v @@ -0,0 +1,18 @@ +Theorem test (A:Prop) : A \/ A -> A. + Fail intros H; destruct H as H. + (* Cannot coerce to a disjunctive/conjunctive pattern. *) + Fail intro H; destruct H as H. + (* Disjunctive/conjunctive introduction pattern expected. *) + Fail let H := fresh in intro H; destruct H as H. + (* Cannot coerce to a disjunctive/conjunctive pattern. *) + Fail let H := fresh in intros H; destruct H as H. + (* Cannot coerce to a disjunctive/conjunctive pattern. *) + Fail let H := idtac in intros H; destruct H as H. + (* Ltac variable H is bound to <tactic closure> which cannot be +coerced to an introduction pattern. *) + Fail let H := idtac in intros H; destruct H as H'. + (* Disjunctive/conjunctive introduction pattern expected. *) + Fail let H' := idtac in intros H; destruct H as H'. +(* Ltac variable H' is bound to <tactic closure> which cannot +be coerced to an introduction pattern. *) +Abort. diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index a1028bda0c..121a369a94 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -37,6 +37,17 @@ let' f (x y : nat) (a := 0) (z : nat) (_ : bool) := x + y + z + 1 in f 0 1 2 λ (f : nat -> nat) (x : nat), f(x) + S(x) : (nat -> nat) -> nat -> nat Notation plus2 n := (S(S(n))) +λ n : list(nat), match n with + | 1 :: nil => 0 + | _ => 2 + end + : list(nat) -> nat +λ n : list(nat), +match n with +| 1 :: nil => 0 +| nil | 0 :: _ | 1 :: _ :: _ | plus2 _ :: _ => 2 +end + : list(nat) -> nat λ n : list(nat), match n with | nil => 2 diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 4c3eaa0c7b..531398bb0b 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -79,6 +79,13 @@ Notation plus2 n := (S (S n)). (* plus2 was not correctly printed in the two following tests in 8.3pl1 *) Print plus2. Check fun n => match n with list1 => 0 | _ => 2 end. +Unset Printing Allow Match Default Clause. +Check fun n => match n with list1 => 0 | _ => 2 end. +Unset Printing Factorizable Match Patterns. +Check fun n => match n with list1 => 0 | _ => 2 end. +Set Printing Allow Match Default Clause. +Set Printing Factorizable Match Patterns. + End A. (* This one is not fully satisfactory because binders in the same type diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 2fa9f0ab4d..437b7b0ac2 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -727,9 +727,9 @@ let parse_args arglist = |"-noinit"|"-nois" -> load_init := false |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true |"-native-compiler" -> - if Coq_config.no_native_compiler then + if not Coq_config.native_compiler then warning "Native compilation was disabled at configure time." - else Flags.native_compiler := true + else Flags.output_native_objects := true |"-output-context" -> output_context := true |"-profile-ltac" -> Flags.profile_ltac := true |"-q" -> Coqinit.no_load_rc () |