diff options
69 files changed, 628 insertions, 475 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 20dac57a77..e56693eac2 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -268,7 +268,7 @@ ci-color: <<: *ci-template variables: <<: *ci-template-vars - EXTRA_PACKAGES: "$TIMING_PACKAGES subversion" + EXTRA_PACKAGES: "$TIMING_PACKAGES" ci-compcert: <<: *ci-template diff --git a/API/API.mli b/API/API.mli index b79be8f7dd..6251bc18b8 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1293,65 +1293,6 @@ sig type to_patch_substituted end -module Decl_kinds : -sig - type polymorphic = bool - type cumulative_inductive_flag = bool - type recursivity_kind = - | Finite - | CoFinite - | BiFinite - - type discharge = - | DoDischarge - | NoDischarge - - type locality = - | Discharge - | Local - | Global - - type definition_object_kind = - | Definition - | Coercion - | SubClass - | CanonicalStructure - | Example - | Fixpoint - | CoFixpoint - | Scheme - | StructureComponent - | IdentityCoercion - | Instance - | Method - | Let - type theorem_kind = - | Theorem - | Lemma - | Fact - | Remark - | Property - | Proposition - | Corollary - type goal_object_kind = - | DefinitionBody of definition_object_kind - | Proof of theorem_kind - type goal_kind = locality * polymorphic * goal_object_kind - type assumption_object_kind = - | Definitional - | Logical - | Conjectural - type logical_kind = - | IsAssumption of assumption_object_kind - | IsDefinition of definition_object_kind - | IsProof of theorem_kind - type binding_kind = - | Explicit - | Implicit - type private_flag = bool - type definition_kind = locality * polymorphic * definition_object_kind -end - module Retroknowledge : sig type action @@ -1501,10 +1442,15 @@ sig type record_body = (Id.t * Constant.t array * projection_body array) option + type recursivity_kind = + | Finite + | CoFinite + | BiFinite + type mutual_inductive_body = { mind_packets : one_inductive_body array; mind_record : record_body option; - mind_finite : Decl_kinds.recursivity_kind; + mind_finite : recursivity_kind; mind_ntypes : int; mind_hyps : Context.Named.t; mind_nparams : int; @@ -1578,7 +1524,7 @@ sig (** Some (Some id): primitive record with id the binder name of the record in projections. Some None: non-primitive record *) - mind_entry_finite : Decl_kinds.recursivity_kind; + mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; mind_entry_universes : inductive_universes; @@ -2210,6 +2156,66 @@ sig | SubEvar of Evar.t end +module Decl_kinds : +sig + type polymorphic = bool + type cumulative_inductive_flag = bool + type recursivity_kind = Declarations.recursivity_kind = + | Finite + | CoFinite + | BiFinite + [@@ocaml.deprecated "Please use [Declarations.recursivity_kind"] + + type discharge = + | DoDischarge + | NoDischarge + + type locality = + | Discharge + | Local + | Global + + type definition_object_kind = + | Definition + | Coercion + | SubClass + | CanonicalStructure + | Example + | Fixpoint + | CoFixpoint + | Scheme + | StructureComponent + | IdentityCoercion + | Instance + | Method + | Let + type theorem_kind = + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary + type goal_object_kind = + | DefinitionBody of definition_object_kind + | Proof of theorem_kind + type goal_kind = locality * polymorphic * goal_object_kind + type assumption_object_kind = + | Definitional + | Logical + | Conjectural + type logical_kind = + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_kind + type binding_kind = + | Explicit + | Implicit + type private_flag = bool + type definition_kind = locality * polymorphic * definition_object_kind +end + module Glob_term : sig type 'a cases_pattern_r = @@ -3999,7 +4005,7 @@ sig type instance_flag = bool option type coercion_flag = bool - type inductive_flag = Decl_kinds.recursivity_kind + type inductive_flag = Declarations.recursivity_kind type lname = Names.Name.t Loc.located type lident = Names.Id.t Loc.located type opacity_flag = @@ -4964,8 +4970,6 @@ sig val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool - val pf_is_matching : Goal.goal Evd.sigma -> Pattern.constr_pattern -> EConstr.constr -> bool - val pf_hyps_types : Goal.goal Evd.sigma -> (Names.Id.t * EConstr.types) list val pr_gls : Goal.goal Evd.sigma -> Pp.t @@ -5247,16 +5251,20 @@ end module Genprint : sig - type printer_with_level = + type 'a with_level = { default_already_surrounded : Notation_term.tolerability; default_ensure_surrounded : Notation_term.tolerability; - printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t } + printer : 'a } type printer_result = - | PrinterBasic of (unit -> Pp.t) - | PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) - | PrinterNeedsContextAndLevel of printer_with_level - type 'a printer = 'a -> Pp.t - type 'a top_printer = 'a -> printer_result +| PrinterBasic of (unit -> Pp.t) +| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level + type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t + type top_printer_result = + | TopPrinterBasic of (unit -> Pp.t) + | TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) + | TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level + type 'a printer = 'a -> printer_result + type 'a top_printer = 'a -> top_printer_result val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw printer -> 'glb printer -> 'top top_printer -> unit val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> @@ -6066,7 +6074,7 @@ sig val do_mutual_inductive : (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> - Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> unit + Decl_kinds.private_flag -> Declarations.recursivity_kind -> unit val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option -> Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> @@ -6092,7 +6100,7 @@ sig structured_inductive_expr -> Vernacexpr.decl_notation list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> - Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> + Decl_kinds.private_flag -> Declarations.recursivity_kind -> Entries.mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list val declare_mutual_inductive_with_eliminations : @@ -7,6 +7,10 @@ Notations right (e.g. "( x ; .. ; y ; z )") now supported. - Notations with a specific level for the leftmost nonterminal, when printing-only, are supported. +- When several notations are available for the same expression, + priority is given to latest notations defined in the scopes being + opened rather than to the latest notations defined independently of + whether they are in an opened scope or not. Tactics @@ -43,7 +43,7 @@ WHAT DO YOU NEED ? - a C compiler - for Coqide, the Lablgtk development files, and the GTK libraries - incuding gtksourceview, see INSTALL.ide for more details + including gtksourceview, see INSTALL.ide for more details Opam (https://opam.ocaml.org/) is recommended to install ocaml and the corresponding packages. @@ -30,7 +30,7 @@ package "lib" ( directory = "lib" - requires = "coq.config" + requires = "str, unix, threads, coq.config" archive(byte) = "clib.cma" archive(byte) += "lib.cma" @@ -65,7 +65,7 @@ package "kernel" ( directory = "kernel" - requires = "coq.lib, coq.vm" + requires = "dynlink, coq.lib, coq.vm" archive(byte) = "kernel.cma" archive(native) = "kernel.cmxa" @@ -168,7 +168,7 @@ package "parsing" ( description = "Coq Parsing Engine" version = "8.7" - requires = "coq.proofs" + requires = "camlp5.gramlib, coq.proofs" directory = "parsing" archive(byte) = "parsing.cma" @@ -139,19 +139,10 @@ endif # This should help preventing weird compilation failures caused by leftover # compiled files after deleting or moving some source files. -ifeq (,$(findstring clean,$(MAKECMDGOALS))) # Skip this for 'make clean' and alii -ifndef ACCEPT_ALIEN_VO EXISTINGVO:=$(call find, '*.vo') KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO)) -ifdef ALIENVO -$(error Leftover compiled Coq files without known sources: $(ALIENVO); \ -remove them first, for instance via 'make voclean' \ -(or skip this check via 'make ACCEPT_ALIEN_VO=1')) -endif -endif -ifndef ACCEPT_ALIEN_OBJ EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa') KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \ $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) @@ -159,9 +150,20 @@ KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ $(MLIFILES:.mli=.cmi) \ $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS)) + +ifeq (,$(findstring clean,$(MAKECMDGOALS))) # Skip this for 'make clean' and alii +ifndef ACCEPT_ALIEN_VO +ifdef ALIENVO +$(error Leftover compiled Coq files without known sources: $(ALIENVO); \ +remove them first, for instance via 'make voclean' or 'make alienclean' \ +(or skip this check via 'make ACCEPT_ALIEN_VO=1')) +endif +endif + +ifndef ACCEPT_ALIEN_OBJ ifdef ALIENOBJS $(error Leftover compiled OCaml files without known sources: $(ALIENOBJS); \ -remove them first, for instance via 'make clean' \ +remove them first, for instance via 'make clean' or 'make alienclean' \ (or skip this check via 'make ACCEPT_ALIEN_OBJ=1')) endif endif @@ -196,7 +198,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean devdocclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean devdocclean alienclean clean: objclean cruftclean depclean docclean devdocclean @@ -282,6 +284,9 @@ devdocclean: rm -f $(OCAMLDOCDIR)/ocamldoc.sty $(OCAMLDOCDIR)/coq.tex rm -f $(OCAMLDOCDIR)/html/*.html +alienclean: + rm -f $(ALIENOBJS) $(ALIENVO) + ########################################################################### # Continuous Intregration Tests ########################################################################### diff --git a/checker/check.ml b/checker/check.ml index 44105aa72f..82341ad9b2 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -129,8 +129,6 @@ type logical_path = DirPath.t let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list) -let get_load_paths () = fst !load_paths - (* Hints to partially detects if two paths refer to the same repertory *) let rec remove_path_dot p = let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *) @@ -227,13 +225,8 @@ let locate_absolute_library dir = let locate_qualified_library qid = try - let loadpath = - (* Search library in loadpath *) - if qid.dirpath=[] then get_load_paths () - else - (* we assume qid is an absolute dirpath *) - load_paths_of_dir_path (dir_of_path qid) - in + (* we assume qid is an absolute dirpath *) + let loadpath = load_paths_of_dir_path (dir_of_path qid) in if loadpath = [] then raise LibUnmappedDir; let name = qid.basename^".vo" in let path, file = System.where_in_path loadpath name in diff --git a/checker/checker.ml b/checker/checker.ml index b2433ee364..fee31b6675 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -96,17 +96,13 @@ let add_rec_path ~unix_path ~coq_root = (* By the option -include -I or -R of the command line *) let includes = ref [] -let push_include (s, alias) = includes := (s,alias,false) :: !includes -let push_rec_include (s, alias) = includes := (s,alias,true) :: !includes +let push_include (s, alias) = includes := (s,alias) :: !includes let set_default_include d = push_include (d, Check.default_root_prefix) let set_include d p = let p = dirpath_of_string p in push_include (d,p) -let set_rec_include d p = - let p = dirpath_of_string p in - push_rec_include(d,p) (* Initializes the LoadPath *) let init_load_path () = @@ -132,8 +128,7 @@ let init_load_path () = add_path ~unix_path:"." ~coq_root:Check.default_root_prefix; (* additional loadpath, given with -I -include -R options *) List.iter - (fun (unix_path, coq_root, reci) -> - if reci then add_rec_path ~unix_path ~coq_root else add_path ~unix_path ~coq_root) + (fun (unix_path, coq_root) -> add_rec_path ~unix_path ~coq_root) (List.rev !includes); includes := [] @@ -179,7 +174,9 @@ let print_usage_channel co command = output_string co command; output_string co "coqchk options are:\n"; output_string co -" -R dir coqdir map physical dir to logical coqdir\ +" -Q dir coqdir map physical dir to logical coqdir\ +\n -R dir coqdir synonymous for -Q\ +\n\ \n\ \n -admit module load module and dependencies without checking\ \n -norec module check module but admit dependencies without checking\ @@ -311,6 +308,9 @@ let explain_exn = function report ()) | e -> CErrors.print e (* for anomalies and other uncaught exceptions *) +let deprecated flag = + Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag)) + let parse_args argv = let rec parse = function | [] -> () @@ -324,12 +324,15 @@ let parse_args argv = Flags.coqlib_spec := true; parse rem - | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem + | ("-I"|"-include") :: d :: "-as" :: p :: rem -> deprecated "-I"; set_include d p; parse rem | ("-I"|"-include") :: d :: "-as" :: [] -> usage () - | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem + | ("-I"|"-include") :: d :: rem -> deprecated "-I"; set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem + | "-Q" :: d :: p :: rem -> set_include d p;parse rem + | "-Q" :: ([] | [_]) -> usage () + + | "-R" :: d :: p :: rem -> set_include d p;parse rem | "-R" :: ([] | [_]) -> usage () | "-debug" :: rem -> set_debug (); parse rem diff --git a/checker/closure.ml b/checker/closure.ml index 7982ffa7a5..3a56bba015 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -279,7 +279,6 @@ and fterm = | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) | FLambda of int * (Name.t * constr) list * constr * fconstr subs | FProd of Name.t * fconstr * fconstr @@ -306,7 +305,6 @@ let update v1 (no,t) = type stack_member = | Zapp of fconstr array - | Zcase of case_info * fconstr * fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs | Zproj of int * int * projection | Zfix of fconstr * stack @@ -456,13 +454,10 @@ let rec to_constr constr_fun lfts v = | FFlex (ConstKey op) -> Const op | FInd op -> Ind op | FConstruct op -> Construct op - | FCase (ci,p,c,ve) -> - Case (ci, constr_fun lfts p, - constr_fun lfts c, - Array.map (constr_fun lfts) ve) - | FCaseT (ci,p,c,ve,e) -> (* TODO: enable sharing, cf FCLOS below ? *) - to_constr constr_fun lfts - {norm=Red;term=FCase(ci,mk_clos2 e p,c,mk_clos_vect e ve)} + | FCaseT (ci,p,c,ve,e) -> + let fp = mk_clos2 e p in + let fve = mk_clos_vect e ve in + Case (ci, constr_fun lfts fp, constr_fun lfts c, Array.map (constr_fun lfts) fve) | FFix ((op,(lna,tys,bds)),e) -> let n = Array.length bds in let ftys = Array.map (mk_clos e) tys in @@ -532,9 +527,6 @@ let rec zip m stk = match stk with | [] -> m | Zapp args :: s -> zip {norm=neutr m.norm; term=FApp(m, args)} s - | Zcase(ci,p,br)::s -> - let t = FCase(ci, p, m, br) in - zip {norm=neutr m.norm; term=t} s | ZcaseT(ci,p,br,e)::s -> let t = FCaseT(ci, p, m, br, e) in zip {norm=neutr m.norm; term=t} s @@ -616,7 +608,7 @@ let rec get_args n tys f e stk = (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *) let rec eta_expand_stack = function - | (Zapp _ | Zfix _ | Zcase _ | ZcaseT _ | Zproj _ + | (Zapp _ | Zfix _ | ZcaseT _ | Zproj _ | Zshift _ | Zupdate _ as e) :: s -> e :: eta_expand_stack s | [] -> @@ -720,7 +712,6 @@ let rec knh info m stk = | FCLOS(t,e) -> knht info e t (zupdate m stk) | FLOCKED -> assert false | FApp(a,b) -> knh info a (append_stack b (zupdate m stk)) - | FCase(ci,p,t,br) -> knh info t (Zcase(ci,p,br)::zupdate m stk) | FCaseT(ci,p,t,br,env) -> knh info t (ZcaseT(ci,p,br,env)::zupdate m stk) | FFix(((ri,n),(_,_,_)),_) -> (match get_nth_arg m ri.(n) stk with @@ -778,10 +769,6 @@ let rec knr info m stk = | None -> (set_norm m; (m,stk))) | FConstruct((ind,c),u) when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with - (depth, args, Zcase(ci,_,br)::s) -> - assert (ci.ci_npar>=0); - let rargs = drop_parameters depth ci.ci_npar args in - kni info br.(c-1) (rargs@s) | (depth, args, ZcaseT(ci,_,br,env)::s) -> assert (ci.ci_npar>=0); let rargs = drop_parameters depth ci.ci_npar args in @@ -798,7 +785,7 @@ let rec knr info m stk = | (_,args,s) -> (m,args@s)) | FCoFix _ when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with - (_, args, (((Zcase _|ZcaseT _)::_) as stk')) -> + (_, args, (((ZcaseT _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in knit info fxe fxbd (args@stk') | (_,args,s) -> (m,args@s)) diff --git a/checker/closure.mli b/checker/closure.mli index 957cc4adb4..02d8b22fae 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -98,7 +98,6 @@ type fterm = | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) | FLambda of int * (Name.t * constr) list * constr * fconstr subs | FProd of Name.t * fconstr * fconstr @@ -115,7 +114,6 @@ type fterm = type stack_member = | Zapp of fconstr array - | Zcase of case_info * fconstr * fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs | Zproj of int * int * projection | Zfix of fconstr * stack diff --git a/checker/reduction.ml b/checker/reduction.ml index 6d8783d7e5..9b8eac04cd 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -42,8 +42,8 @@ let compare_stack_shape stk1 stk2 = | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2 | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 - | ((Zcase(c1,_,_)|ZcaseT(c1,_,_,_))::s1, - (Zcase(c2,_,_)|ZcaseT(c2,_,_,_))::s2) -> + | ((ZcaseT(c1,_,_,_))::s1, + (ZcaseT(c2,_,_,_))::s2) -> bal=0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> bal=0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 @@ -78,8 +78,7 @@ let pure_stack lfts stk = (l, Zlfix((lfx,fx),pa)::pstk) | (ZcaseT(ci,p,br,env),(l,pstk)) -> (l,Zlcase(ci,l,mk_clos env p,mk_clos_vect env br)::pstk) - | (Zcase(ci,p,br),(l,pstk)) -> - (l,Zlcase(ci,l,p,br)::pstk)) in + ) in snd (pure_rec lfts stk) (****************************************************************************) @@ -243,7 +242,6 @@ let rec no_arg_available = function | Zshift _ :: stk -> no_arg_available stk | Zapp v :: stk -> Array.length v = 0 && no_arg_available stk | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -256,7 +254,6 @@ let rec no_nth_arg_available n = function if n >= k then no_nth_arg_available (n-k) stk else false | Zproj _ :: _ -> true - | Zcase _ :: _ -> true | ZcaseT _ :: _ -> true | Zfix _ :: _ -> true @@ -266,13 +263,12 @@ let rec no_case_available = function | Zshift _ :: stk -> no_case_available stk | Zapp _ :: stk -> no_case_available stk | Zproj (_,_,_) :: _ -> false - | Zcase _ :: _ -> false | ZcaseT _ :: _ -> false | Zfix _ :: _ -> true let in_whnf (t,stk) = match fterm_of t with - | (FLetIn _ | FCase _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false + | (FLetIn _ | FCaseT _ | FApp _ | FCLOS _ | FLIFT _ | FCast _) -> false | FLambda _ -> no_arg_available stk | FConstruct _ -> no_case_available stk | FCoFix _ -> no_case_available stk @@ -504,8 +500,8 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = else raise NotConvertible (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *) - | ( (FLetIn _, _) | (FCase _,_) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) - | (_, FLetIn _) | (_,FCase _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) + | ( (FLetIn _, _) | (FCaseT _,_) | (FApp _,_) | (FCLOS _,_) | (FLIFT _,_) + | (_, FLetIn _) | (_,FCaseT _) | (_,FApp _) | (_,FCLOS _) | (_,FLIFT _) | (FLOCKED,_) | (_,FLOCKED) ) -> assert false (* In all other cases, terms are not convertible *) diff --git a/configure.ml b/configure.ml index e14eeac7b8..c7d25bfc80 100644 --- a/configure.ml +++ b/configure.ml @@ -686,7 +686,7 @@ let operating_system, osdeplibs = let check_for_numlib () = if caml_version_nums >= [4;6;0] then - let numlib,_ = tryrun "ocamlfind" ["query";"num"] in + let numlib,_ = tryrun camlexec.find ["query";"num"] in match numlib with | "" -> die "Num library not installed, required for OCaml 4.06 or later" @@ -727,11 +727,11 @@ let get_lablgtkdir () = else "", msg | None -> let msg = OCamlFind in - let d1,_ = tryrun "ocamlfind" ["query";"lablgtk2.sourceview2"] in + let d1,_ = tryrun camlexec.find ["query";"lablgtk2.sourceview2"] in if d1 <> "" && check_lablgtkdir msg d1 then d1, msg else (* In debian wheezy, ocamlfind knows only of lablgtk2 *) - let d2,_ = tryrun "ocamlfind" ["query";"lablgtk2"] in + let d2,_ = tryrun camlexec.find ["query";"lablgtk2"] in if d2 <> "" && d2 <> d1 && check_lablgtkdir msg d2 then d2, msg else let msg = Stdlib in @@ -757,7 +757,7 @@ let check_lablgtk_version src dir = match src with if ans then printf "Warning: could not check the version of lablgtk2.\n"; (ans, "an unknown version") | OCamlFind -> - let v, _ = tryrun "ocamlfind" ["query"; "-format"; "%v"; "lablgtk2"] in + let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in try let vi = List.map s2i (numeric_prefix_list v) in ([2; 16] <= vi, v) @@ -814,7 +814,7 @@ let coqide_flags () = if !lablgtkdir <> "" then lablgtkincludes := sprintf "-I %S" !lablgtkdir; match coqide, arch with | "opt", "Darwin" when !Prefs.macintegration -> - let osxdir,_ = tryrun "ocamlfind" ["query";"lablgtkosx"] in + let osxdir,_ = tryrun camlexec.find ["query";"lablgtkosx"] in if osxdir <> "" then begin lablgtkincludes := sprintf "%s -I %S" !lablgtkincludes osxdir; idearchflags := "lablgtkosx.cma"; diff --git a/default.nix b/default.nix index 86f86ff99b..3dd24bac4d 100644 --- a/default.nix +++ b/default.nix @@ -42,15 +42,21 @@ stdenv.mkDerivation rec { # CoqIDE dependencies ocamlPackages.lablgtk - ] else []) ++ (if doCheck then [ + ] else []) ++ (if doCheck then # Test-suite dependencies + let inherit (stdenv.lib) versionAtLeast optional; in + /* ncurses is required to build an OCaml REPL */ + optional (!versionAtLeast ocaml.version "4.07") ncurses + ++ [ python rsync which ] else []) ++ (if lib.inNixShell then [ ocamlPackages.merlin + ocamlPackages.ocpIndent + ocamlPackages.ocp-index ] else []); src = diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 168a34e6e4..232b8a56e4 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -115,7 +115,8 @@ ######################################################################## # CoLoR ######################################################################## -: ${Color_CI_SVNURL:=https://scm.gforge.inria.fr/anonscm/svn/color/trunk/color} +: ${CoLoR_CI_BRANCH:=master} +: ${CoLoR_CI_GITURL:=https://github.com/fblanqui/color.git} ######################################################################## # SF diff --git a/dev/ci/ci-color.sh b/dev/ci/ci-color.sh index 309050057c..c3ae7552a9 100755 --- a/dev/ci/ci-color.sh +++ b/dev/ci/ci-color.sh @@ -3,33 +3,11 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -Color_CI_DIR=${CI_BUILD_DIR}/color +CoLoR_CI_DIR=${CI_BUILD_DIR}/color # Setup Bignums - source ${ci_dir}/ci-bignums.sh -# Compiles CoLoR - -svn checkout ${Color_CI_SVNURL} ${Color_CI_DIR} - -sed -i -e "s/From Coq Require Import BigN/From Bignums Require Import BigN/" ${Color_CI_DIR}/Util/*/*.v -sed -i -e "s/From Coq Require Export BigN/From Bignums Require Export BigN/" ${Color_CI_DIR}/Util/*/*.v -sed -i -e "s/From Coq Require Import BigZ/From Bignums Require Import BigZ/" ${Color_CI_DIR}/Util/*/*.v -sed -i -e "s/From Coq Require Export BigZ/From Bignums Require Export BigZ/" ${Color_CI_DIR}/Util/*/*.v - -# Adapt to PR #220 (FunInd not loaded in Prelude anymore) -sed -i -e "15i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/basis/ordered_set.v -sed -i -e "8i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/equational_extension.v -sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/more_list_extention.v -sed -i -e "6i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/examples/cime_trace/ring_extention.v -sed -i -e "27i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/dickson.v -sed -i -e "26i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_permut.v -sed -i -e "23i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_set.v -sed -i -e "25i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/list_sort.v -sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Coccinelle/list_extensions/more_list.v -sed -i -e "21i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/List/ListUtil.v -sed -i -e "17i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Multiset/MultisetOrder.v -sed -i -e "13i From Coq Require Import FunInd." ${Color_CI_DIR}/Util/Set/SetUtil.v - -( cd ${Color_CI_DIR} && make ) +# Compile CoLoR +git_checkout ${CoLoR_CI_BRANCH} ${CoLoR_CI_GITURL} ${CoLoR_CI_DIR} +( cd ${CoLoR_CI_DIR} && make ) diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index fc3cef3426..7bf2c7427d 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -8,4 +8,5 @@ CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert opam install -j ${NJOBS} -y menhir git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR} -( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) +#( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof ) +( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make ) diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh index 4865be31ec..ed40036012 100755 --- a/dev/ci/ci-ltac2.sh +++ b/dev/ci/ci-ltac2.sh @@ -3,7 +3,7 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -ltac2_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph +ltac2_CI_DIR=${CI_BUILD_DIR}/ltac2 git_checkout ${ltac2_CI_BRANCH} ${ltac2_CI_GITURL} ${ltac2_CI_DIR} diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh index 217540cc19..4e8c7e145e 100755 --- a/dev/ci/ci-sf.sh +++ b/dev/ci/ci-sf.sh @@ -3,13 +3,10 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -# XXX: Needs fixing to properly set the build directory. -wget ${sf_lf_CI_TARURL} -wget ${sf_plf_CI_TARURL} -wget ${sf_vfa_CI_TARURL} -tar xvfz lf.tgz -tar xvfz plf.tgz -tar xvfz vfa.tgz +mkdir -p ${CI_BUILD_DIR} && cd ${CI_BUILD_DIR} +wget -qO- ${sf_lf_CI_TARURL} | tar xvz +wget -qO- ${sf_plf_CI_TARURL} | tar xvz +wget -qO- ${sf_vfa_CI_TARURL} | tar xvz sed -i.bak '1i From Coq Require Extraction.' lf/Extraction.v sed -i.bak '1i From Coq Require Extraction.' vfa/Extract.v diff --git a/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh b/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh new file mode 100644 index 0000000000..cdca8e525a --- /dev/null +++ b/dev/ci/user-overlays/06158-herbelin-master+fix-pr6158-ltac-value-printer.sh @@ -0,0 +1,4 @@ +if [ "$TRAVIS_PULL_REQUEST" = "6158" ] || [ "$TRAVIS_BRANCH" = "master+some-fix-ltac-printing+refined-printers" ]; then + ltac2_CI_BRANCH=master+fix-pr6158-ltac-value-printer + ltac2_CI_GITURL=https://github.com/herbelin/ltac2.git +fi diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh index bc6ee31916..4c4dbe1e97 100755 --- a/dev/tools/backport-pr.sh +++ b/dev/tools/backport-pr.sh @@ -1,6 +1,6 @@ #!/usr/bin/env bash -# Usage: git-backport <PR number> +# Usage: dev/tools/backport-pr.sh <PR number> set -e diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh index f770004a5c..0c4a79bfd3 100755 --- a/dev/tools/merge-pr.sh +++ b/dev/tools/merge-pr.sh @@ -1,4 +1,6 @@ -#!/bin/sh -e +#!/usr/bin/env bash + +set -e # This script depends (at least) on git and jq. # It should be used like this: dev/tools/merge-pr.sh /PR number/ @@ -15,12 +17,12 @@ API=https://api.github.com/repos/coq/coq BASE_BRANCH=`curl -s $API/pulls/$PR | jq -r '.base.label'` -COMMIT=`git rev-parse $REMOTE/pr/$PR` +COMMIT=`git rev-parse FETCH_HEAD` STATUS=`curl -s $API/commits/$COMMIT/status | jq -r '.state'` if [ $BASE_BRANCH != "coq:$CURRENT_LOCAL_BRANCH" ]; then echo "Wrong base branch" - read -p "Bypass? [y/n] " -n 1 -r + read -p "Bypass? [y/N] " -n 1 -r echo if [[ ! $REPLY =~ ^[Yy]$ ]] then @@ -30,7 +32,7 @@ fi; if [ $STATUS != "success" ]; then echo "CI status is \"$STATUS\"" - read -p "Bypass? [y/n] " -n 1 -r + read -p "Bypass? [y/N] " -n 1 -r echo if [[ ! $REPLY =~ ^[Yy]$ ]] then @@ -38,7 +40,7 @@ if [ $STATUS != "success" ]; then fi fi; -git merge -S --no-ff $REMOTE/pr/$PR -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e +git merge -S --no-ff FETCH_HEAD -m "Merge PR #$PR: `curl -s $API/pulls/$PR | jq -r '.title'`" -e # TODO: improve this check if [[ `git diff $REMOTE/$CURRENT_LOCAL_BRANCH dev/ci` ]]; then diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index b4d9f60ebc..04a8a25c12 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -331,9 +331,12 @@ code, it cannot be guaranteed that the produced compiled libraries are correct. {\tt coqchk} is a standalone verifier, and thus it cannot be tainted by such malicious code. -Command-line options {\tt -I}, {\tt -R}, {\tt -where} and +Command-line options {\tt -Q}, {\tt -R}, {\tt -where} and {\tt -impredicative-set} are supported by {\tt coqchk} and have the -same meaning as for {\tt coqtop}. Extra options are: +same meaning as for {\tt coqtop}. As there is no notion of relative paths in +object files {\tt -Q} and {\tt -R} have exactly the same meaning. + +Extra options are: \begin{description} \item[{\tt -norec} {\em module}]\ % diff --git a/engine/evd.ml b/engine/evd.ml index d57ae89ddf..45d2a8b084 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -401,7 +401,7 @@ let rename evk id (evtoid, idtoev) = | None -> (EvMap.add evk id evtoid, Id.Map.add id evk idtoev) | Some id' -> if Id.Map.mem id idtoev then anomaly (str "Evar name already in use."); - (EvMap.update evk id evtoid (* overwrite old name *), Id.Map.add id evk (Id.Map.remove id' idtoev)) + (EvMap.set evk id evtoid (* overwrite old name *), Id.Map.add id evk (Id.Map.remove id' idtoev)) let reassign_name_defined evk evk' (evtoid, idtoev as names) = let id = try Some (EvMap.find evk evtoid) with Not_found -> None in diff --git a/engine/uState.ml b/engine/uState.ml index 57e61bb827..6566ad989c 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -135,7 +135,7 @@ let of_binders b = let universe_binders ctx = fst ctx.uctx_names let instantiate_variable l b v = - try v := Univ.LMap.update l (Some b) !v + try v := Univ.LMap.set l (Some b) !v with Not_found -> assert false exception UniversesDiffer diff --git a/engine/universes.ml b/engine/universes.ml index 93696b4ca8..0250295fdf 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -491,7 +491,7 @@ module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap) let add_list_map u t map = try let l = LMap.find u map in - LMap.update u (t :: l) map + LMap.set u (t :: l) map with Not_found -> LMap.add u [t] map @@ -584,7 +584,7 @@ let normalize_univ_variable_subst subst = let find l = Univ.LMap.find l !subst in let update l b = assert (match Universe.level b with Some l' -> not (Level.equal l l') | None -> true); - try subst := Univ.LMap.update l b !subst; b with Not_found -> assert false in + try subst := Univ.LMap.set l b !subst; b with Not_found -> assert false in normalize_univ_variable ~find ~update let normalize_universe_opt_subst subst = diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index f6f46710c2..a561ea3703 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -82,7 +82,7 @@ let make_clause_classifier cg s { r_patt = pt; r_class = c; } = "classifiers. Only one classifier is called.") ^ "\n"); (make_patt pt, ploc_vala None, - <:expr< fun loc -> (Vernacexpr.VtUnknown, Vernacexpr.VtNow) >>) + <:expr< fun () -> ( CErrors.anomaly (Pp.str "No classification given for command " ^ s ) ) >>) let make_fun_clauses loc s l = let map c = diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e1df24f717..bc8debd02d 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -383,7 +383,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = try if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_pattern scopes vars pat - (uninterp_cases_pattern_notations pat) + (uninterp_cases_pattern_notations scopes pat) with No_match -> lift (fun ?loc -> function | PatVar (Name id) -> CPatAtom (Some (Ident (loc,id))) @@ -514,7 +514,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = try if !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_ind_pattern scopes vars ind args - (uninterp_ind_pattern_notations ind) + (uninterp_ind_pattern_notations scopes ind) with No_match -> let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in @@ -734,7 +734,7 @@ let rec extern inctx scopes vars r = try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation scopes vars r'' (uninterp_notations r'') + extern_notation scopes vars r'' (uninterp_notations scopes r'') with No_match -> lift (fun ?loc -> function | GRef (ref,us) -> extern_global (select_stronger_impargs (implicits_of_global ref)) diff --git a/interp/notation.ml b/interp/notation.ml index f36294f732..94ce2a6c8d 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -526,15 +526,38 @@ let interp_notation ?loc ntn local_scopes = user_err ?loc (str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".") -let uninterp_notations c = - List.map_append (fun key -> keymap_find key !notations_key_table) - (glob_constr_keys c) - -let uninterp_cases_pattern_notations c = - keymap_find (cases_pattern_key c) !notations_key_table - -let uninterp_ind_pattern_notations ind = - keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table +let sort_notations scopes l = + let extract_scope l = function + | Scope sc -> List.partitioni (fun _i x -> + match x with + | NotationRule (Some sc',_),_,_ -> String.equal sc sc' + | _ -> false) l + | SingleNotation ntn -> List.partitioni (fun _i x -> + match x with + | NotationRule (None,ntn'),_,_ -> String.equal ntn ntn' + | _ -> false) l in + let rec aux l scopes = + if l == [] then [] (* shortcut *) else + match scopes with + | sc :: scopes -> let ntn_in_sc,l = extract_scope l sc in ntn_in_sc @ aux l scopes + | [] -> l in + aux l scopes + +let uninterp_notations scopes c = + let scopes = make_current_scopes scopes in + let keys = glob_constr_keys c in + let maps = List.map_append (fun key -> keymap_find key !notations_key_table) keys in + sort_notations scopes maps + +let uninterp_cases_pattern_notations scopes c = + let scopes = make_current_scopes scopes in + let maps = keymap_find (cases_pattern_key c) !notations_key_table in + sort_notations scopes maps + +let uninterp_ind_pattern_notations scopes ind = + let scopes = make_current_scopes scopes in + let maps = keymap_find (RefKey (canonical_gr (IndRef ind))) !notations_key_table in + sort_notations scopes maps let availability_of_notation (ntn_scope,ntn) scopes = let f scope = diff --git a/interp/notation.mli b/interp/notation.mli index 2066d346fe..7d055571c8 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -124,9 +124,9 @@ val interp_notation : ?loc:Loc.t -> notation -> local_scopes -> type notation_rule = interp_rule * interpretation * int option (** Return the possible notations for a given term *) -val uninterp_notations : 'a glob_constr_g -> notation_rule list -val uninterp_cases_pattern_notations : 'a cases_pattern_g -> notation_rule list -val uninterp_ind_pattern_notations : inductive -> notation_rule list +val uninterp_notations : local_scopes -> 'a glob_constr_g -> notation_rule list +val uninterp_cases_pattern_notations : local_scopes -> 'a cases_pattern_g -> notation_rule list +val uninterp_ind_pattern_notations : local_scopes -> inductive -> notation_rule list (** Test if a notation is available in the scopes context [scopes]; if available, the result is not None; the first diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml index 1dea6d9e98..b0c1f66613 100644 --- a/intf/decl_kinds.ml +++ b/intf/decl_kinds.ml @@ -75,7 +75,8 @@ type logical_kind = (** Recursive power of type declarations *) -type recursivity_kind = +type recursivity_kind = Declarations.recursivity_kind = | Finite (** = inductive *) | CoFinite (** = coinductive *) | BiFinite (** = non-recursive, like in "Record" definitions *) +[@@ocaml.deprecated "Please use [Declarations.recursivity_kind"] diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 5c9141fd6f..c7a9db1cbc 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -145,7 +145,7 @@ type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *) type export_flag = bool (* true = Export; false = Import *) -type inductive_flag = Decl_kinds.recursivity_kind +type inductive_flag = Declarations.recursivity_kind type onlyparsing_flag = Flags.compat_version option (* Some v = Parse only; None = Print also. If v<>Current, it contains the name of the coq version @@ -482,18 +482,39 @@ and vernac_argument_status = { implicit_status : vernac_implicit_status; } -(* A vernac classifier has to tell if a command: - vernac_when: has to be executed now (alters the parser) or later - vernac_type: if it is starts, ends, continues a proof or +(* A vernac classifier provides information about the exectuion of a + command: + + - vernac_when: encodes if the vernac may alter the parser [thus + forcing immediate execution], or if indeed it is pure and parsing + can continue without its execution. + + - vernac_type: if it is starts, ends, continues a proof or alters the global state or is a control command like BackTo or is - a query like Check *) + a query like Check. + + The classification works on the assumption that we have 3 states: + parsing, execution (global enviroment, etc...), and proof + state. For example, commands that only alter the proof state are + considered safe to delegate to a worker. + +*) type vernac_type = + (* Start of a proof *) | VtStartProof of vernac_start + (* Command altering the global state, bad for parallel + processing. *) | VtSideff of vernac_sideff_type + (* End of a proof *) | VtQed of vernac_qed_type + (* A proof step *) | VtProofStep of proof_step + (* To be removed *) | VtProofMode of string + (* Queries are commands assumed to be "pure", that is to say, they + don't modify the interpretation state. *) | VtQuery of vernac_part_of_script * Feedback.route_id + (* To be removed *) | VtMeta | VtUnknown and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index d5312c5006..7f4b85fd05 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -172,13 +172,18 @@ type abstract_inductive_universes = | Polymorphic_ind of Univ.AUContext.t | Cumulative_ind of Univ.ACumulativityInfo.t +type recursivity_kind = + | Finite (** = inductive *) + | CoFinite (** = coinductive *) + | BiFinite (** = non-recursive, like in "Record" definitions *) + type mutual_inductive_body = { mind_packets : one_inductive_body array; (** The component of the mutual inductive block *) mind_record : record_body option; (** The record information *) - mind_finite : Decl_kinds.recursivity_kind; (** Whether the type is inductive or coinductive *) + mind_finite : recursivity_kind; (** Whether the type is inductive or coinductive *) mind_ntypes : int; (** Number of types in the block *) diff --git a/kernel/entries.ml b/kernel/entries.ml index c44a17df2a..ca79de404d 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -51,7 +51,7 @@ type mutual_inductive_entry = { (** Some (Some id): primitive record with id the binder name of the record in projections. Some None: non-primitive record *) - mind_entry_finite : Decl_kinds.recursivity_kind; + mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; mind_entry_universes : inductive_universes; diff --git a/lib/cMap.ml b/lib/cMap.ml index 0ecb40209c..b4c4aedd0e 100644 --- a/lib/cMap.ml +++ b/lib/cMap.ml @@ -26,7 +26,7 @@ sig include CSig.MapS module Set : CSig.SetS with type elt = key val get : key -> 'a t -> 'a - val update : key -> 'a -> 'a t -> 'a t + val set : key -> 'a -> 'a t -> 'a t val modify : key -> (key -> 'a -> 'a) -> 'a t -> 'a t val domain : 'a t -> Set.t val bind : (key -> 'a) -> Set.t -> 'a t @@ -50,7 +50,7 @@ end module MapExt (M : Map.OrderedType) : sig type 'a map = 'a Map.Make(M).t - val update : M.t -> 'a -> 'a map -> 'a map + val set : M.t -> 'a -> 'a map -> 'a map val modify : M.t -> (M.t -> 'a -> 'a) -> 'a map -> 'a map val domain : 'a map -> Set.Make(M).t val bind : (M.t -> 'a) -> Set.Make(M).t -> 'a map @@ -93,19 +93,19 @@ struct let set_prj : set -> _set = Obj.magic let set_inj : _set -> set = Obj.magic - let rec update k v (s : 'a map) : 'a map = match map_prj s with + let rec set k v (s : 'a map) : 'a map = match map_prj s with | MEmpty -> raise Not_found | MNode (l, k', v', r, h) -> let c = M.compare k k' in if c < 0 then - let l' = update k v l in + let l' = set k v l in if l == l' then s else map_inj (MNode (l', k', v', r, h)) else if c = 0 then if v' == v then s else map_inj (MNode (l, k', v, r, h)) else - let r' = update k v r in + let r' = set k v r in if r == r' then s else map_inj (MNode (l, k', v', r', h)) diff --git a/lib/cMap.mli b/lib/cMap.mli index f65036139b..5e65bd200a 100644 --- a/lib/cMap.mli +++ b/lib/cMap.mli @@ -34,7 +34,7 @@ sig val get : key -> 'a t -> 'a (** Same as {!find} but fails an assertion instead of raising [Not_found] *) - val update : key -> 'a -> 'a t -> 'a t + val set : key -> 'a -> 'a t -> 'a t (** Same as [add], but expects the key to be present, and thus faster. @raise Not_found when the key is unbound in the map. *) diff --git a/lib/cSig.mli b/lib/cSig.mli index 6910cbbf03..32e9d2af0c 100644 --- a/lib/cSig.mli +++ b/lib/cSig.mli @@ -56,6 +56,12 @@ sig val is_empty: 'a t -> bool val mem: key -> 'a t -> bool val add: key -> 'a -> 'a t -> 'a t + (* when Coq requires OCaml 4.06 or later, can add: + + val update : key -> ('a option -> 'a option) -> 'a t -> 'a t + + allowing Coq to use OCaml's "update" + *) val singleton: key -> 'a -> 'a t val remove: key -> 'a t -> 'a t val merge: diff --git a/lib/hMap.ml b/lib/hMap.ml index c69efdb711..37079af783 100644 --- a/lib/hMap.ml +++ b/lib/hMap.ml @@ -47,7 +47,7 @@ struct try let m = Int.Map.find h s in let m = Set.add x m in - Int.Map.update h m s + Int.Map.set h m s with Not_found -> let m = Set.singleton x in Int.Map.add h m s @@ -65,7 +65,7 @@ struct if Set.is_empty m then Int.Map.remove h s else - Int.Map.update h m s + Int.Map.set h m s with Not_found -> s let height s = Int.Map.height s @@ -135,7 +135,7 @@ struct let s' = Int.Map.find h accu in let si = Set.filter (fun e -> not (Set.mem e s)) s' in if Set.is_empty si then Int.Map.remove h accu - else Int.Map.update h si accu + else Int.Map.set h si accu with Not_found -> accu in Int.Map.fold fold s2 s1 @@ -242,11 +242,19 @@ struct try let m = Int.Map.find h s in let m = Map.add k x m in - Int.Map.update h m s + Int.Map.set h m s with Not_found -> let m = Map.singleton k x in Int.Map.add h m s + (* when Coq requires OCaml 4.06 or later, the module type + CSig.MapS may include the signature of OCaml's "update", + requiring an implementation here, which could be just: + + let update k f s = assert false (* not implemented *) + + *) + let singleton k x = let h = M.hash k in Int.Map.singleton h (Map.singleton k x) @@ -259,7 +267,7 @@ struct if Map.is_empty m then Int.Map.remove h s else - Int.Map.update h m s + Int.Map.set h m s with Not_found -> s let merge f s1 s2 = @@ -359,7 +367,7 @@ struct let h = M.hash k in let m = Int.Map.find h s in let m = Map.modify k f m in - Int.Map.update h m s + Int.Map.set h m s let bind f s = let fb m = Map.bind f m in @@ -367,11 +375,11 @@ struct let domain s = Int.Map.map Map.domain s - let update k x s = + let set k x s = let h = M.hash k in let m = Int.Map.find h s in - let m = Map.update k x m in - Int.Map.update h m s + let m = Map.set k x m in + Int.Map.set h m s let smartmap f s = let fs m = Map.smartmap f m in diff --git a/man/coqchk.1 b/man/coqchk.1 index a00914eab8..f9241c0d47 100644 --- a/man/coqchk.1 +++ b/man/coqchk.1 @@ -34,13 +34,17 @@ add directory in the include path .TP -.BI \-R \ dir\ coqdir -recursively map physical +.BI \-Q \ dir\ coqdir +map physical .I dir to logical .I coqdir .TP +.BI \-R \ dir\ coqdir +synonymous for -Q + +.TP .BI \-silent makes coqchk less verbose. diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b0a76137b7..766adfc63a 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -141,7 +141,7 @@ let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; let lt = function () -> (coq_init_constant "lt") -let le = function () -> (coq_init_constant "le") +let le = function () -> (Coqlib.gen_reference_in_modules "RecursiveDefinition" Coqlib.init_modules "le") let ex = function () -> (coq_init_constant "ex") let nat = function () -> (coq_init_constant "nat") let iter_ref () = @@ -857,9 +857,13 @@ let rec prove_le g = Proofview.V82.of_tactic (apply (delayed_force le_n)); begin try - let matching_fun = - pf_is_matching g - (Pattern.PApp(Pattern.PRef (Globnames.global_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in + let matching_fun c = match EConstr.kind sigma c with + | App (c, [| x0 ; _ |]) -> + EConstr.isVar sigma x0 && + Id.equal (destVar sigma x0) (destVar sigma x) && + is_global sigma (le ()) c + | _ -> false + in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in let y = diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 34fea6175b..8b9eb39837 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -471,7 +471,7 @@ END VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => - [ VtUnknown, VtNow ] -> + [ VtSideff [], VtNow ] -> [ fun ~atts ~st -> let open Vernacinterp in let n = Option.default 0 n in Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e; diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index d707512457..6aa2f6f898 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -84,6 +84,24 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +type 'a raw_extra_genarg_printer_with_level = + (constr_expr -> Pp.t) -> + (constr_expr -> Pp.t) -> + (tolerability -> raw_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a glob_extra_genarg_printer_with_level = + (glob_constr_and_expr -> Pp.t) -> + (glob_constr_and_expr -> Pp.t) -> + (tolerability -> glob_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a extra_genarg_printer_with_level = + (EConstr.constr -> Pp.t) -> + (EConstr.constr -> Pp.t) -> + (tolerability -> Val.t -> Pp.t) -> + tolerability -> 'a -> Pp.t + let string_of_genarg_arg (ArgumentType arg) = let rec aux : type a b c. (a, b, c) genarg_type -> string = function | ListArg t -> aux t ^ "_list" @@ -127,9 +145,9 @@ let string_of_genarg_arg (ArgumentType arg) = | Some Refl -> let open Genprint in match generic_top_print (in_gen (Topwit wit) x) with - | PrinterBasic pr -> pr () - | PrinterNeedsContext pr -> pr (Global.env()) Evd.empty - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + | TopPrinterBasic pr -> pr () + | TopPrinterNeedsContext pr -> pr (Global.env()) Evd.empty + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> printer (Global.env()) Evd.empty default_ensure_surrounded end | _ -> default @@ -723,8 +741,10 @@ let pr_goal_selector ~toplevel s = | TacIntroPattern (ev,[]) as t -> pr_atom0 t | TacIntroPattern (ev,(_::_ as p)) -> - hov 1 (primitive (if ev then "eintros" else "intros") ++ spc () ++ - prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p) + hov 1 (primitive (if ev then "eintros" else "intros") ++ + (match p with + | [_,Misctypes.IntroForthcoming false] -> mt () + | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)) | TacApply (a,ev,cb,inhyp) -> hov 1 ( (if a then mt() else primitive "simple ") ++ @@ -1192,42 +1212,77 @@ let declare_extra_genarg_pprule wit | ExtraArg s -> () | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") end; - let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + let f x = + Genprint.PrinterBasic (fun () -> + f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in let g x = + Genprint.PrinterBasic (fun () -> let env = Global.env () in - g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x + g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x) in let h x = - Genprint.PrinterNeedsContext (fun env sigma -> + Genprint.TopPrinterNeedsContext (fun env sigma -> h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x) in Genprint.register_print0 wit f g h +let declare_extra_genarg_pprule_with_level wit + (f : 'a raw_extra_genarg_printer_with_level) + (g : 'b glob_extra_genarg_printer_with_level) + (h : 'c extra_genarg_printer_with_level) default_surrounded default_non_surrounded = + begin match wit with + | ExtraArg s -> () + | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") + end; + let open Genprint in + let f x = + PrinterNeedsLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun n -> + f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level n x) } in + let g x = + let env = Global.env () in + PrinterNeedsLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun n -> + g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) n x) } + in + let h x = + TopPrinterNeedsContextAndLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun env sigma n -> + h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") n x) } + in + Genprint.register_print0 wit f g h + let declare_extra_vernac_genarg_pprule wit f = - let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + let f x = Genprint.PrinterBasic (fun () -> f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in Genprint.register_vernac_print0 wit f (** Registering *) -let pr_intro_pattern_env p = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_intro_pattern_env p = Genprint.TopPrinterNeedsContext (fun env sigma -> let print_constr c = let (sigma, c) = c env sigma in pr_econstr_env env sigma c in Miscprint.pr_intro_pattern print_constr p) -let pr_red_expr_env r = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_red_expr_env r = Genprint.TopPrinterNeedsContext (fun env sigma -> pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma, pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r) -let pr_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, bl = bl env sigma in Miscprint.pr_bindings (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) -let pr_with_bindings_env bl = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_with_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, bl = bl env sigma in pr_with_bindings (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) -let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma -> +let pr_destruction_arg_env c = Genprint.TopPrinterNeedsContext (fun env sigma -> let sigma, c = match c with | clear_flag,ElimOnConstr g -> let sigma,c = g env sigma in sigma,(clear_flag,ElimOnConstr c) | clear_flag,ElimOnAnonHyp n as x -> sigma, x @@ -1236,12 +1291,16 @@ let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma -> (pr_econstr_env env sigma) (pr_leconstr_env env sigma) c) let make_constr_printer f c = - Genprint.PrinterNeedsContextAndLevel { + Genprint.TopPrinterNeedsContextAndLevel { Genprint.default_already_surrounded = Ppconstr.ltop; Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr; Genprint.printer = (fun env sigma n -> f env sigma n c)} let lift f a = Genprint.PrinterBasic (fun () -> f a) +let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a) + +let register_basic_print0 wit f g h = + Genprint.register_print0 wit (lift f) (lift g) (lift_top h) let pr_glob_constr_pptac c = @@ -1255,80 +1314,81 @@ let pr_lglob_constr_pptac c = let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in - Genprint.register_print0 wit_int_or_var - (pr_or_var int) (pr_or_var int) (lift int); - Genprint.register_print0 wit_ref - pr_reference (pr_or_var (pr_located pr_global)) (lift pr_global); - Genprint.register_print0 wit_ident - pr_id pr_id (lift pr_id); - Genprint.register_print0 wit_var - (pr_located pr_id) (pr_located pr_id) (lift pr_id); - Genprint.register_print0 + let open Genprint in + register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; + register_basic_print0 wit_ref + pr_reference (pr_or_var (pr_located pr_global)) pr_global; + register_basic_print0 wit_ident pr_id pr_id pr_id; + register_basic_print0 wit_var (pr_located pr_id) (pr_located pr_id) pr_id; + register_print0 wit_intro_pattern - (Miscprint.pr_intro_pattern pr_constr_expr) - (Miscprint.pr_intro_pattern (fun (c, _) -> pr_glob_constr_pptac c)) + (lift (Miscprint.pr_intro_pattern pr_constr_expr)) + (lift (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac c))) pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl - (pr_clauses (Some true) pr_lident) - (pr_clauses (Some true) pr_lident) - (fun c -> Genprint.PrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) + (lift (pr_clauses (Some true) pr_lident)) + (lift (pr_clauses (Some true) pr_lident)) + (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) ; Genprint.register_print0 wit_constr - Ppconstr.pr_constr_expr - (fun (c, _) -> pr_glob_constr_pptac c) + (lift Ppconstr.pr_lconstr_expr) + (lift (fun (c, _) -> pr_lglob_constr_pptac c)) (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_uconstr - Ppconstr.pr_constr_expr - (fun (c, _) -> pr_glob_constr_pptac c) + (lift Ppconstr.pr_constr_expr) + (lift (fun (c,_) -> pr_glob_constr_pptac c)) (make_constr_printer Printer.pr_closed_glob_n_env) ; Genprint.register_print0 wit_open_constr - Ppconstr.pr_constr_expr - (fun (c, _) -> pr_glob_constr_pptac c) + (lift Ppconstr.pr_constr_expr) + (lift (fun (c, _) -> pr_glob_constr_pptac c)) (make_constr_printer Printer.pr_econstr_n_env) ; - Genprint.register_print0 wit_red_expr - (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) - (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac)) + Genprint.register_print0 + wit_red_expr + (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))) + (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac))) pr_red_expr_env ; - Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift pr_quantified_hypothesis); - Genprint.register_print0 wit_bindings - (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) - (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_basic_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; + register_print0 wit_bindings + (lift (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)) + (lift (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_bindings_env ; - Genprint.register_print0 wit_constr_with_bindings - (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_print0 wit_constr_with_bindings + (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr)) + (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_with_bindings_env ; - Genprint.register_print0 wit_open_constr_with_bindings - (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_print0 wit_open_constr_with_bindings + (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr)) + (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_with_bindings_env ; - Genprint.register_print0 Tacarg.wit_destruction_arg - (pr_destruction_arg pr_constr_expr pr_lconstr_expr) - (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)) + register_print0 Tacarg.wit_destruction_arg + (lift (pr_destruction_arg pr_constr_expr pr_lconstr_expr)) + (lift (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) pr_destruction_arg_env ; - Genprint.register_print0 Stdarg.wit_int int int (lift int); - Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool (lift pr_bool); - Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit (lift pr_unit); - Genprint.register_print0 Stdarg.wit_pre_ident str str (lift str); - Genprint.register_print0 Stdarg.wit_string qstring qstring (lift qstring) + register_basic_print0 Stdarg.wit_int int int int; + register_basic_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; + register_basic_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; + register_basic_print0 Stdarg.wit_pre_ident str str str; + register_basic_print0 Stdarg.wit_string qstring qstring qstring let () = - let printer _ _ prtac = prtac (0, E) in - declare_extra_genarg_pprule wit_tactic printer printer printer + let printer _ _ prtac = prtac in + declare_extra_genarg_pprule_with_level wit_tactic printer printer printer + ltop (0,E) let () = - let pr_unit _ _ _ () = str "()" in - let printer _ _ prtac = prtac (0, E) in - declare_extra_genarg_pprule wit_ltac printer printer pr_unit + let pr_unit _ _ _ _ () = str "()" in + let printer _ _ prtac = prtac in + declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit + ltop (0,E) diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 5ecfaf590c..bda5774abf 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -40,12 +40,37 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +type 'a raw_extra_genarg_printer_with_level = + (constr_expr -> Pp.t) -> + (constr_expr -> Pp.t) -> + (tolerability -> raw_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a glob_extra_genarg_printer_with_level = + (glob_constr_and_expr -> Pp.t) -> + (glob_constr_and_expr -> Pp.t) -> + (tolerability -> glob_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a extra_genarg_printer_with_level = + (EConstr.constr -> Pp.t) -> + (EConstr.constr -> Pp.t) -> + (tolerability -> Val.t -> Pp.t) -> + tolerability -> 'a -> Pp.t + val declare_extra_genarg_pprule : ('a, 'b, 'c) genarg_type -> 'a raw_extra_genarg_printer -> 'b glob_extra_genarg_printer -> 'c extra_genarg_printer -> unit +val declare_extra_genarg_pprule_with_level : + ('a, 'b, 'c) genarg_type -> + 'a raw_extra_genarg_printer_with_level -> + 'b glob_extra_genarg_printer_with_level -> + 'c extra_genarg_printer_with_level -> + (* surroounded *) tolerability -> (* non-surroounded *) tolerability -> unit + val declare_extra_vernac_genarg_pprule : ('a, 'b, 'c) genarg_type -> 'a raw_extra_genarg_printer -> unit diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index c03a867326..9ae112d371 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -33,7 +33,7 @@ let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_bin let () = register_val0 wit None in let () = Genprint.register_val_print0 (base_val_typ wit) (fun c -> - Genprint.PrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in + Genprint.TopPrinterNeedsContext (fun env sigma -> Printer.pr_constr_under_binders_env env sigma c)) in wit (** All the types considered here are base types *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 14b79d73ed..e0d7eca5f8 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -128,7 +128,7 @@ let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = let wit = Genarg.create_arg "tacvalue" in let () = register_val0 wit None in let () = Genprint.register_val_print0 (base_val_typ wit) - (fun _ -> Genprint.PrinterBasic (fun () -> str "<tactic closure>")) in + (fun _ -> Genprint.TopPrinterBasic (fun () -> str "<tactic closure>")) in wit let of_tacvalue v = in_gen (topwit wit_tacvalue) v @@ -242,9 +242,9 @@ let pr_value env v = | None -> str "a value of type" ++ spc () ++ pr_argument_type v in let open Genprint in match generic_val_print v with - | PrinterBasic pr -> pr () - | PrinterNeedsContext pr -> pr_with_env pr - | PrinterNeedsContextAndLevel { default_already_surrounded; printer } -> + | TopPrinterBasic pr -> pr () + | TopPrinterNeedsContext pr -> pr_with_env pr + | TopPrinterNeedsContextAndLevel { default_already_surrounded; printer } -> pr_with_env (fun env sigma -> printer env sigma default_already_surrounded) let pr_closure env ist body = @@ -821,9 +821,9 @@ let message_of_value v = Ftactic.enter begin fun gl -> Ftactic.return (pr (pf_env gl) (project gl)) end in let open Genprint in match generic_val_print v with - | PrinterBasic pr -> Ftactic.return (pr ()) - | PrinterNeedsContext pr -> pr_with_env pr - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + | TopPrinterBasic pr -> Ftactic.return (pr ()) + | TopPrinterNeedsContext pr -> pr_with_env pr + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> pr_with_env (fun env sigma -> printer env sigma default_ensure_surrounded) let interp_message_token ist = function @@ -1353,8 +1353,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = begin let open Genprint in match generic_val_print v with - | PrinterBasic _ -> call_debug None - | PrinterNeedsContext _ | PrinterNeedsContextAndLevel _ -> + | TopPrinterBasic _ -> call_debug None + | TopPrinterNeedsContext _ | TopPrinterNeedsContextAndLevel _ -> Proofview.Goal.enter (fun gl -> call_debug (Some (pf_env gl,project gl))) end <*> if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 49ccb468c1..387a525141 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -149,7 +149,7 @@ let open_in f = match read_key_elem inch with | None -> () | Some (key,elem) -> - Table.add htbl key elem ; + Table.replace htbl key elem ; xload () in try (* Locking of the (whole) file while reading *) @@ -195,7 +195,7 @@ let add t k e = else let fd = descr_of_out_channel outch in begin - Table.add tbl k e ; + Table.replace tbl k e ; do_under_lock Write fd (fun _ -> Marshal.to_channel outch (k,e) [Marshal.No_sharing] ; diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 20ef65c884..478ba73fd5 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -13,7 +13,6 @@ open Util open Names open Globnames open Termops -open Reductionops open Term open EConstr open Vars @@ -207,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 convert allow_partial_app allow_bound_rels +let matches_core env sigma allow_partial_app allow_bound_rels (binding_vars,pat) c = let open EConstr in let convref ref c = @@ -216,11 +215,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | ConstRef c, Const (c',_) -> Constant.equal c c' | IndRef i, Ind (i', _) -> Names.eq_ind i i' | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' - | _, _ -> - (if convert then - let sigma,c' = Evd.fresh_global env sigma ref in - is_conv env sigma (EConstr.of_constr c') c - else false) + | _, _ -> false in let rec sorec ctx env subst p t = let cT = strip_outer_cast sigma t in @@ -378,14 +373,14 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels in sorec [] env (Id.Map.empty, Id.Map.empty) pat c -let matches_core_closed env sigma convert allow_partial_app pat c = - let names, subst = matches_core env sigma convert allow_partial_app false pat c in +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 (names, Id.Map.map snd subst) -let extended_matches env sigma = matches_core env sigma false true true +let extended_matches env sigma = matches_core env sigma true true let matches env sigma pat c = - snd (matches_core_closed env sigma false true (Id.Set.empty,pat) c) + snd (matches_core_closed env sigma true (Id.Set.empty,pat) c) let special_meta = (-1) @@ -412,7 +407,7 @@ let matches_head env sigma pat c = (* 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 = try - let subst = matches_core_closed env sigma false partial_app pat c in + let subst = matches_core_closed env sigma partial_app 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) @@ -552,10 +547,3 @@ 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 not (IStream.is_empty results) - -let matches_conv env sigma p c = - snd (matches_core_closed env sigma true false (Id.Set.empty,p) c) - -let is_matching_conv env sigma pat n = - try let _ = matches_conv env sigma pat n in true - with PatternMatchingFailure -> false diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 780ccc23d1..60e1c34a15 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -55,12 +55,6 @@ val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool prefix of it matches against [pat] *) val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool -(** [matches_conv env sigma] matches up to conversion in environment - [(env,sigma)] when constants in pattern are concerned; it raises - [PatternMatchingFailure] if not matchable; bindings are given in - increasing order based on the numbers given in the pattern *) -val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map - (** The type of subterm matching results: a substitution + a context (whose hole is denoted here with [special_meta]) *) type matching_result = @@ -85,8 +79,3 @@ val match_subterm_gen : env -> Evd.evar_map -> (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches against [pat] taking partial subterms into consideration *) val is_matching_appsubterm : ?closed:bool -> env -> Evd.evar_map -> constr_pattern -> constr -> bool - -(** [is_matching_conv env sigma pat c] tells if [c] matches against [pat] - up to conversion for constants in patterns *) -val is_matching_conv : - env -> Evd.evar_map -> constr_pattern -> constr -> bool diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 18e0c31dd6..e5776d2eca 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -310,8 +310,6 @@ let ise_stack2 no_app env evd f sk1 sk2 = | Success i' -> ise_stack2 true i' q1 q2 | UnifFailure _ as x -> fail x else fail (UnifFailure (i,NotSameHead)) - | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ - | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false | Stack.App _ :: _, Stack.App _ :: _ -> if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else begin match ise_app_stack2 env f i sk1 sk2 with @@ -344,8 +342,6 @@ let exact_ise_stack2 env evd f sk1 sk2 = if Constant.equal (Projection.constant p1) (Projection.constant p2) then ise_stack2 i q1 q2 else (UnifFailure (i, NotSameHead)) - | Stack.Update _ :: _, _ | Stack.Shift _ :: _, _ - | _, Stack.Update _ :: _ | _, Stack.Shift _ :: _ -> assert false | Stack.App _ :: _, Stack.App _ :: _ -> begin match ise_app_stack2 env f i sk1 sk2 with |_,(UnifFailure _ as x) -> x @@ -457,7 +453,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in let out2 = whd_nored_state evd - (Stack.zip evd (term', sk' @ [Stack.Shift 1]), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), + (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), Cst_stack.empty in if onleft then evar_eqappr_x ts env' evd CONV out1 out2 else evar_eqappr_x ts env' evd CONV out2 out1 diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index ba0502ca45..2f8e5b9643 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -284,8 +284,6 @@ sig | Proj of int * int * projection * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list exception IncompatibleFold2 @@ -343,8 +341,6 @@ struct | Proj of int * int * projection * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list let rec pr_member pr_c member = @@ -367,8 +363,6 @@ struct ++ pr_comma () ++ prlist_with_sep pr_semicolon int remains ++ pr_comma () ++ pr pr_c params ++ str ")" - | Shift i -> str "ZShift(" ++ int i ++ str ")" - | Update t -> str "ZUpdate(" ++ pr_c t ++ str ")" and pr pr_c l = let open Pp in prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l @@ -414,9 +408,6 @@ struct let rec equal_rec sk1 lft1 sk2 lft2 = match sk1,sk2 with | [],[] -> Some (lft1,lft2) - | (Update _ :: _, _ | _, Update _ :: _) -> assert false - | Shift k :: s1, _ -> equal_rec s1 (lft1+k) sk2 lft2 - | _, Shift k :: s2 -> equal_rec sk1 lft1 s2 (lft2+k) | App a1 :: s1, App a2 :: s2 -> let t1,s1' = decomp_node_last a1 s1 in let t2,s2' = decomp_node_last a2 s2 in @@ -449,8 +440,6 @@ struct let rec compare_rec bal stk1 stk2 = match (stk1,stk2) with ([],[]) -> Int.equal bal 0 - | ((Update _|Shift _)::s1, _) -> compare_rec bal s1 stk2 - | (_, (Update _|Shift _)::s2) -> compare_rec bal stk1 s2 | (App (i,_,j)::s1, _) -> compare_rec (bal + j + 1 - i) s1 stk2 | (_, App (i,_,j)::s2) -> compare_rec (bal - j - 1 + i) stk1 s2 | (Case(c1,_,_,_)::s1, Case(c2,_,_,_)::s2) -> @@ -472,8 +461,6 @@ struct in match sk1,sk2 with | [], [] -> o,lft1,lft2 - | Shift n :: q1, _ -> aux o (lft1+n) q1 lft2 sk2 - | _, Shift n :: q2 -> aux o lft1 sk1 (lft2+n) q2 | App n1 :: q1, App n2 :: q2 -> let t1,l1 = decomp_node_last n1 q1 in let t2,l2 = decomp_node_last n2 q2 in @@ -493,13 +480,12 @@ struct let (o',lft1',lft2') = aux o lft1 (List.rev params1) lft2 (List.rev params2) in aux o' lft1' q1 lft2' q2 - | (((Update _|App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> + | (((App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> raise IncompatibleFold2 in aux o 0 (List.rev sk1) 0 (List.rev sk2) let rec map f x = List.map (function - | Update _ -> assert false - | (Proj (_,_,_,_) | Shift _) as e -> e + | (Proj (_,_,_,_)) as e -> e | App (i,a,j) -> let le = j - i + 1 in App (0,Array.map f (Array.sub a i le), le-1) @@ -516,18 +502,15 @@ struct let rec args_size = function | App (i,_,j)::s -> j + 1 - i + args_size s - | Shift(_)::s -> args_size s - | Update(_)::s -> args_size s | (Case _|Fix _|Proj _|Cst _)::_ | [] -> 0 let strip_app s = let rec aux out = function - | ( App _ | Shift _ as e) :: s -> aux (e :: out) s + | ( App _ as e) :: s -> aux (e :: out) s | s -> List.rev out,s in aux [] s let strip_n_app n s = let rec aux n out = function - | Shift k as e :: s -> aux n (e :: out) s | App (i,a,j) as e :: s -> let nb = j - i + 1 in if n >= nb then @@ -555,8 +538,6 @@ struct 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') - | Shift n :: s -> - let (k,(args',s')) = aux s in (k+n,(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 @@ -568,20 +549,18 @@ struct | None -> assert false let tail n0 s0 = - let rec aux lft n s = - let out s = if Int.equal lft 0 then s else Shift lft :: s in - if Int.equal n 0 then out s else + let rec aux n s = + if Int.equal n 0 then s else match s with | App (i,a,j) :: s -> let nb = j - i + 1 in if n >= nb then - aux lft (n - nb) s + aux (n - nb) s else let p = i+n in if j >= p then App(p,a,j)::s else s - | Shift k :: s' -> aux (lft+k) n s' | _ -> raise (Invalid_argument "Reductionops.Stack.tail") - in aux 0 n0 s0 + in aux n0 s0 let nth s p = match strip_n_app p s with @@ -627,11 +606,9 @@ struct zip (best_state sigma (constr_of_cst_member cst (params @ (append_app [|f|] s))) cst_l) | f, (Cst (cst,_,_,params,_)::s) -> zip (constr_of_cst_member cst (params @ (append_app [|f|] s))) - | f, (Shift n::s) -> zip (lift n f, s) | f, (Proj (n,m,p,cst_l)::s) when refold -> zip (best_state sigma (mkProj (p,f),s) cst_l) | f, (Proj (n,m,p,_)::s) -> zip (mkProj (p,f),s) - | _, (Update _::_) -> assert false in zip s @@ -1074,7 +1051,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = (arg, Stack.Cst (const,next,remains',s' @ (Stack.append_app [|x'|] bef),cst_l) :: s''') end - |_, (Stack.App _|Stack.Update _|Stack.Shift _)::_ -> assert false + |_, (Stack.App _)::_ -> assert false |_, _ -> fold () else fold () @@ -1155,7 +1132,7 @@ let local_whd_state_gen flags sigma = |args, (Stack.Fix (f,s',cst)::s'') when use_fix -> let x' = Stack.zip sigma (x,args) in whrec (contract_fix sigma f, s' @ (Stack.append_app [|x'|] s'')) - |_, (Stack.App _|Stack.Update _|Stack.Shift _|Stack.Cst _)::_ -> assert false + |_, (Stack.App _|Stack.Cst _)::_ -> assert false |_, _ -> s else s @@ -1685,7 +1662,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = if isConstruct sigma t_o then whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'') else s,csts' - |_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts' + |_, ((Stack.App _|Stack.Cst _) :: _|[]) -> s,csts' in whrec csts s let find_conclusion env sigma = diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index db0c29aeff..34fdbe8583 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -82,8 +82,6 @@ module Stack : sig | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *) * 'a t * Cst_stack.t - | Shift of int - | Update of 'a and 'a t = 'a member list val pr : ('a -> Pp.t) -> 'a t -> Pp.t @@ -107,7 +105,7 @@ module Stack : sig val append_app_list : 'a list -> 'a t -> 'a t (** if [strip_app s] = [(a,b)], then [s = a @ b] and [b] does not - start by App or Shift *) + start by App *) val strip_app : 'a t -> 'a t * 'a t (** @return (the nth first elements, the (n+1)th element, the remaining stack) *) val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option diff --git a/printing/genprint.ml b/printing/genprint.ml index 776a212b5c..37a94fe219 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -16,21 +16,27 @@ open Geninterp (* Printing generic values *) -type printer_with_level = +type 'a with_level = { default_already_surrounded : Notation_term.tolerability; default_ensure_surrounded : Notation_term.tolerability; - printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t } + printer : 'a } type printer_result = | PrinterBasic of (unit -> Pp.t) -| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) -| PrinterNeedsContextAndLevel of printer_with_level +| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level -type 'a printer = 'a -> Pp.t +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t -type 'a top_printer = 'a -> printer_result +type top_printer_result = +| TopPrinterBasic of (unit -> Pp.t) +| TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) +| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level -module ValMap = ValTMap (struct type 'a t = 'a -> printer_result end) +type 'a printer = 'a -> printer_result + +type 'a top_printer = 'a -> top_printer_result + +module ValMap = ValTMap (struct type 'a t = 'a -> top_printer_result end) let print0_val_map = ref ValMap.empty @@ -48,32 +54,32 @@ let register_val_print0 s pr = print0_val_map := ValMap.add s pr !print0_val_map let combine_dont_needs pr_pair pr1 = function - | PrinterBasic pr2 -> - PrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ())) - | PrinterNeedsContext pr2 -> - PrinterNeedsContext (fun env sigma -> + | TopPrinterBasic pr2 -> + TopPrinterBasic (fun () -> pr_pair (pr1 ()) (pr2 ())) + | TopPrinterNeedsContext pr2 -> + TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 ()) (pr2 env sigma)) - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> - PrinterNeedsContext (fun env sigma -> + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 ()) (printer env sigma default_ensure_surrounded)) let combine_needs pr_pair pr1 = function - | PrinterBasic pr2 -> - PrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ())) - | PrinterNeedsContext pr2 -> - PrinterNeedsContext (fun env sigma -> + | TopPrinterBasic pr2 -> + TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 ())) + | TopPrinterNeedsContext pr2 -> + TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (pr2 env sigma)) - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> - PrinterNeedsContext (fun env sigma -> + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + TopPrinterNeedsContext (fun env sigma -> pr_pair (pr1 env sigma) (printer env sigma default_ensure_surrounded)) let combine pr_pair pr1 v2 = match pr1 with - | PrinterBasic pr1 -> + | TopPrinterBasic pr1 -> combine_dont_needs pr_pair pr1 (generic_val_print v2) - | PrinterNeedsContext pr1 -> + | TopPrinterNeedsContext pr1 -> combine_needs pr_pair pr1 (generic_val_print v2) - | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> combine_needs pr_pair (fun env sigma -> printer env sigma default_ensure_surrounded) (generic_val_print v2) @@ -81,14 +87,14 @@ let _ = let pr_cons a b = Pp.(a ++ spc () ++ b) in register_val_print0 Val.typ_list (function - | [] -> PrinterBasic mt + | [] -> TopPrinterBasic mt | a::l -> List.fold_left (combine pr_cons) (generic_val_print a) l) let _ = register_val_print0 Val.typ_opt (function - | None -> PrinterBasic Pp.mt + | None -> TopPrinterBasic Pp.mt | Some v -> generic_val_print v) let _ = @@ -99,9 +105,9 @@ let _ = (* Printing generic arguments *) type ('raw, 'glb, 'top) genprinter = { - raw : 'raw printer; - glb : 'glb printer; - top : 'top -> printer_result; + raw : 'raw -> printer_result; + glb : 'glb -> printer_result; + top : 'top -> top_printer_result; } module PrintObj = @@ -112,9 +118,9 @@ struct | ExtraArg tag -> let name = ArgT.repr tag in let printer = { - raw = (fun _ -> str "<genarg:" ++ str name ++ str ">"); - glb = (fun _ -> str "<genarg:" ++ str name ++ str ">"); - top = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">")); + raw = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">")); + glb = (fun _ -> PrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">")); + top = (fun _ -> TopPrinterBasic (fun () -> str "<genarg:" ++ str name ++ str ">")); } in Some printer | _ -> assert false diff --git a/printing/genprint.mli b/printing/genprint.mli index 2da9bbc36b..baa60fcb2e 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -10,19 +10,25 @@ open Genarg -type printer_with_level = +type 'a with_level = { default_already_surrounded : Notation_term.tolerability; default_ensure_surrounded : Notation_term.tolerability; - printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t } + printer : 'a } type printer_result = | PrinterBasic of (unit -> Pp.t) -| PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) -| PrinterNeedsContextAndLevel of printer_with_level +| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level -type 'a printer = 'a -> Pp.t +type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t -type 'a top_printer = 'a -> printer_result +type top_printer_result = +| TopPrinterBasic of (unit -> Pp.t) +| TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) +| TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level + +type 'a printer = 'a -> printer_result + +type 'a top_printer = 'a -> top_printer_result val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw printer (** Printer for raw level generic arguments. *) @@ -34,7 +40,7 @@ val top_print : ('raw, 'glb, 'top) genarg_type -> 'top top_printer (** Printer for top level generic arguments. *) val register_print0 : ('raw, 'glb, 'top) genarg_type -> - 'raw printer -> 'glb printer -> ('top -> printer_result) -> unit + 'raw printer -> 'glb printer -> 'top top_printer -> unit val register_val_print0 : 'top Geninterp.Val.typ -> 'top top_printer -> unit val register_vernac_print0 : ('raw, 'glb, 'top) genarg_type -> diff --git a/printing/pputils.ml b/printing/pputils.ml index 12d5338ade..a544b47623 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -130,7 +130,10 @@ let rec pr_raw_generic env (GenArg (Rawwit wit, x)) = let q = in_gen (rawwit wit2) q in hov_if_not_empty 0 (pr_sequence (pr_raw_generic env) [p; q]) | ExtraArg s -> - Genprint.generic_raw_print (in_gen (rawwit wit) x) + let open Genprint in + match generic_raw_print (in_gen (rawwit wit) x) with + | PrinterBasic pp -> pp () + | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded let rec pr_glb_generic env (GenArg (Glbwit wit, x)) = @@ -152,4 +155,7 @@ let rec pr_glb_generic env (GenArg (Glbwit wit, x)) = let ans = pr_sequence (pr_glb_generic env) [p; q] in hov_if_not_empty 0 ans | ExtraArg s -> - Genprint.generic_glb_print (in_gen (glbwit wit) x) + let open Genprint in + match generic_glb_print (in_gen (glbwit wit) x) with + | PrinterBasic pp -> pp () + | PrinterNeedsLevel { default_ensure_surrounded; printer } -> printer default_ensure_surrounded diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a8ec4d8ca3..cab8d7b52a 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -102,9 +102,6 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls -let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p c -let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c - (********************************************) (* Definition of the most primitive tactics *) (********************************************) @@ -223,8 +220,6 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_all gl (pf_get_type_of gl t) - let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t - let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index d9496d2b4f..e0fb8fbc5d 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -12,9 +12,7 @@ open Environ open EConstr open Proof_type open Redexpr -open Pattern open Locus -open Ltac_pretype (** Operations for handling terms under a local typing context. *) @@ -79,10 +77,6 @@ val pf_const_value : goal sigma -> pconstant -> constr val pf_conv_x : goal sigma -> constr -> constr -> bool val pf_conv_x_leq : goal sigma -> constr -> constr -> bool -val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map -val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool - - (** {6 The most primitive tactics. } *) val refiner : rule -> tactic @@ -138,8 +132,6 @@ module New : sig val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr val pf_compute : 'a Proofview.Goal.t -> constr -> constr - val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr end diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 1ca572a36c..c5ae27a110 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -185,12 +185,12 @@ let rec classify_vernac e = (* These commands alter the parser *) | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ - | VernacSyntaxExtension _ + | VernacSyntaxExtension _ | VernacSyntacticDefinition _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ | VernacContext _ (* TASSI: unsure *) - | VernacProofMode _ + | VernacProofMode _ -> VtSideff [], VtNow (* These are ambiguous *) | VernacInstance _ -> VtUnknown, VtNow (* Stm will install a new classifier to handle these *) @@ -201,7 +201,7 @@ let rec classify_vernac e = (* What are these? *) | VernacToplevelControl _ | VernacRestoreState _ - | VernacWriteState _ -> VtUnknown, VtNow + | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> try List.assoc s !classifiers l () diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 8e851375a6..2c8ca19722 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -39,7 +39,6 @@ type testing_function = Evd.evar_map -> EConstr.constr -> bool let mkmeta n = Nameops.make_ident "X" (Some n) let meta1 = mkmeta 1 let meta2 = mkmeta 2 -let meta3 = mkmeta 3 let op2bool = function Some _ -> true | None -> false @@ -460,22 +459,6 @@ let find_this_eq_data_decompose gl eqn = user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in (lbeq,u,eq_args) -let match_eq_nf gls eqn (ref, hetero) = - let n = if hetero then 4 else 3 in - let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in - let pat = mkPattern (mkGAppRef ref args) in - match Id.Map.bindings (pf_matches gls pat eqn) with - | [(m1,t);(m2,x);(m3,y)] -> - assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3); - (t,pf_whd_all gls x,pf_whd_all gls y) - | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms.") - -let dest_nf_eq gls eqn = - try - snd (first_match (match_eq_nf gls eqn) equalities) - with PatternMatchingFailure -> - user_err Pp.(str "Not an equality.") - (*** Sigma-types *) let match_sigma env sigma ex = diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 8ff6fe95c6..237ed42d55 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -144,9 +144,6 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool [t,u,T] and a boolean telling if equality is on the left side *) val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr -(** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) -val dest_nf_eq : 'a Proofview.Goal.t -> constr -> (constr * constr * constr) - (** Match a negation *) val is_matching_not : Environ.env -> evar_map -> constr -> bool val is_matching_imp_False : Environ.env -> evar_map -> constr -> bool diff --git a/tactics/inv.ml b/tactics/inv.ml index 46b10bf33e..cb0bbfd0e7 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -334,6 +334,16 @@ let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id If it can discriminate then the goal is proved, if not tries to use it as a rewrite rule. It erases the clause which is given as input *) +let dest_nf_eq env sigma t = match EConstr.kind sigma t with +| App (r, [| t; x; y |]) -> + let open Reductionops in + let lazy eq = Coqlib.coq_eq_ref in + if EConstr.is_global sigma eq r then + (t, whd_all env sigma x, whd_all env sigma y) + else user_err Pp.(str "Not an equality.") +| _ -> + user_err Pp.(str "Not an equality.") + let projectAndApply as_mode thin avoid id eqname names depids = let subst_hyp l2r id = tclTHEN (tclTRY(rewriteInConcl l2r (EConstr.mkVar id))) @@ -344,7 +354,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = let sigma = project gl in (** We only look at the type of hypothesis "id" *) let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in - let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in + let (t,t1,t2) = dest_nf_eq (pf_env gl) sigma hyp in match (EConstr.kind sigma t1, EConstr.kind sigma t2) with | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1 | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2 diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 7bcd7b041c..2f0ee765db 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -64,7 +64,7 @@ The command has indeed failed with message: Cannot find where the recursive pattern starts. The command has indeed failed with message: Both ends of the recursive pattern are the same. -SUM (nat * nat) nat +(nat * nat + nat)%type : Set FST (0; 1) : Z @@ -72,7 +72,7 @@ Nil : forall A : Type, list A NIL : list nat : list nat -(false && I 3)%bool /\ I 6 +(false && I 3)%bool /\ (I 6)%bool : Prop [|1, 2, 3; 4, 5, 6|] : Z * Z * Z * (Z * Z * Z) diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index fe6c05c39e..413812ee19 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -30,7 +30,7 @@ Check (decomp (true,true) as t, u in (t,u)). Section A. -Notation "! A" := (forall _:nat, A) (at level 60). +Notation "! A" := (forall _:nat, A) (at level 60) : type_scope. Check ! (0=0). Check forall n, n=0. @@ -194,9 +194,9 @@ Open Scope nat_scope. Coercion is_true := fun b => b=true. Coercion of_nat n := match n with 0 => true | _ => false end. -Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10). +Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10) : bool_scope. -Check (false && I 3)%bool /\ I 6. +Check (false && I 3)%bool /\ (I 6)%bool. (**********************************************************************) (* Check notations with several recursive patterns *) diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index f57cc163d0..a1028bda0c 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -41,7 +41,7 @@ Notation plus2 n := (S(S(n))) match n with | nil => 2 | 0 :: _ => 2 -| list1 => 0 +| 1 :: nil => 0 | 1 :: _ :: _ => 2 | plus2 _ :: _ => 2 end diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 9ca180c9df..4c3eaa0c7b 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -70,6 +70,7 @@ Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2. (* Note: does not work for pattern *) Module A. Notation "f ( x )" := (f x) (at level 10, format "f ( x )"). +Open Scope nat_scope. Check fun f x => f x + S x. Open Scope list_scope. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 6ef75dd135..1b57252752 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -128,3 +128,13 @@ return (1, 2, 3, 4) : nat *(1.2) : nat +[{0; 0}] + : list (list nat) +[{1; 2; 3}; + {4; 5; 6}; + {7; 8; 9}] + : list (list nat) +amatch = mmatch 0 (with 0 => 1| 1 => 2 end) + : unit +alist = [0; 1; 2] + : list nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 8c7bbe5917..a8d6c97fbd 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -59,7 +59,7 @@ Check fun f => CURRYINVLEFT (x:nat) (y:bool), f. (* Notations with variables bound both as a term and as a binder *) (* This is #4592 *) -Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)). +Notation "{# x | P }" := (ex2 (fun y => x = y) (fun x => P)) : type_scope. Check forall n:nat, {# n | 1 > n}. Parameter foo : forall {T}(x : T)(P : T -> Prop), Prop. @@ -183,9 +183,13 @@ Check letpair x [1] = {0}; return (1,2,3,4). (* Test spacing in #5569 *) +Section S1. +Variable plus : nat -> nat -> nat. +Infix "+" := plus. Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut) (at level 0, xR at level 39, format "{ { xL | xR // xcut } }"). Check 1+1+1. +End S1. (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). @@ -193,7 +197,59 @@ Check !!! (x y:nat), True. (* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) -Notation "* x" := (id x) (only printing, at level 15, format "* x"). -Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). +Section S2. +Notation "* x" := (id x) (only printing, at level 15, format "* x") : nat_scope. +Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y") : nat_scope. Check (((id 1) + 2) + 3). Check (id (1 + 2)). +End S2. + +(* Test printing of notations guided by scope *) + +Module A. + +Delimit Scope line_scope with line. +Notation "{ }" := nil (format "{ }") : line_scope. +Notation "{ x }" := (cons x nil) : line_scope. +Notation "{ x ; y ; .. ; z }" := (cons x (cons y .. (cons z nil) ..)) : line_scope. +Notation "[ ]" := nil (format "[ ]") : matx_scope. +Notation "[ l ]" := (cons l%line nil) : matx_scope. +Notation "[ l ; l' ; .. ; l'' ]" := (cons l%line (cons l'%line .. (cons l''%line nil) ..)) + (format "[ '[v' l ; '/' l' ; '/' .. ; '/' l'' ']' ]") : matx_scope. + +Open Scope matx_scope. +Check [[0;0]]. +Check [[1;2;3];[4;5;6];[7;8;9]]. + +End A. + +(* Example by Beta Ziliani *) + +Require Import Lists.List. + +Module B. + +Import ListNotations. + +Delimit Scope pattern_scope with pattern. +Delimit Scope patterns_scope with patterns. + +Notation "a => b" := (a, b) (at level 201) : pattern_scope. +Notation "'with' p1 | .. | pn 'end'" := + ((cons p1%pattern (.. (cons pn%pattern nil) ..))) + (at level 91, p1 at level 210, pn at level 210) : patterns_scope. + +Definition mymatch (n:nat) (l : list (nat * nat)) := tt. +Arguments mymatch _ _%patterns. +Notation "'mmatch' n ls" := (mymatch n ls) (at level 0). + +Close Scope patterns_scope. +Close Scope pattern_scope. + +Definition amatch := mmatch 0 with 0 => 1 | 1 => 2 end. +Print amatch. (* Good: amatch = mmatch 0 (with 0 => 1| 1 => 2 end) *) + +Definition alist := [0;1;2]. +Print alist. + +End B. diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index c5d58ec1ec..eb9f571022 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,7 +1,7 @@ The command has indeed failed with message: Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := - symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize + symmetry in x, y; auto with z; auto; intros; clearbody x; generalize dependent z The command has indeed failed with message: In nested Ltac calls to "g1" and "refine (uconstr)", last call failed. @@ -32,7 +32,7 @@ nat 0 0 Ltac foo := - let x := intros ** in + let x := intros in let y := intros -> in let v := constr:(nil) in let w := () in diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 87783350a2..7fd9429081 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -172,7 +172,7 @@ COQDOCFLAGS?=-interpolate -utf8 $(COQLIBS_NOML) # The version of Coq being run and the version of coq_makefile that # generated this makefile -COQ_VERSION:=$(shell $(COQC) --print-version | cut -d ' ' -f 1) +COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") diff --git a/vernac/command.mli b/vernac/command.mli index a1f916c782..c7342e6da9 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -82,7 +82,7 @@ type one_inductive_impls = val interp_mutual_inductive : structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> + polymorphic -> private_flag -> Declarations.recursivity_kind -> mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list (** Registering a mutual inductive definition together with its @@ -96,7 +96,7 @@ val declare_mutual_inductive_with_eliminations : val do_mutual_inductive : (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag -> - polymorphic -> private_flag -> Decl_kinds.recursivity_kind -> unit + polymorphic -> private_flag -> Declarations.recursivity_kind -> unit (** {6 Fixpoints and cofixpoints} *) diff --git a/vernac/record.mli b/vernac/record.mli index 9fdd5e1c46..e632e7bbff 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -15,7 +15,7 @@ val primitive_flag : bool ref val definition_structure : inductive_kind * Decl_kinds.cumulative_inductive_flag * Decl_kinds.polymorphic * - Decl_kinds.recursivity_kind * ident_decl with_coercion * local_binder_expr list * + Declarations.recursivity_kind * ident_decl with_coercion * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option -> global_reference |