diff options
69 files changed, 780 insertions, 476 deletions
diff --git a/.gitignore b/.gitignore index 709e87cc9c..f9e43a0eb7 100644 --- a/.gitignore +++ b/.gitignore @@ -139,7 +139,7 @@ plugins/ltac/coretactics.ml plugins/ltac/extratactics.ml plugins/ltac/extraargs.ml plugins/ltac/profile_ltac_tactics.ml -ide/coqide_main.ml +ide/coqide_os_specific.ml plugins/ssrmatching/ssrmatching.ml plugins/ssr/ssrparser.ml plugins/ssr/ssrvernac.ml @@ -78,7 +78,6 @@ LEXFILES := $(call find, '*.mll') YACCFILES := $(call find, '*.mly') export MLLIBFILES := $(call find, '*.mllib') export MLPACKFILES := $(call find, '*.mlpack') -export ML4FILES := $(call find, '*.ml4') export MLGFILES := $(call find, '*.mlg') export CFILES := $(call findindir, 'kernel/byterun', '*.c') @@ -94,19 +93,14 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated -GENML4FILES:= $(ML4FILES:.ml4=.ml) GENMLGFILES:= $(MLGFILES:.mlg=.ml) -export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) kernel/copcodes.ml +export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) $(GENMLGFILES) ide/coqide_os_specific.ml kernel/copcodes.ml export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) -# NB: all files in $(GENFILES) can be created initially, while -# .ml files in $(GENML4FILES) might need some intermediate building. -# That's why we keep $(GENML4FILES) out of $(GENFILES) - ## More complex file lists -export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES) $(GENMLGFILES), $(EXISTINGML)) +export MLSTATICFILES := $(filter-out $(GENMLFILES), $(EXISTINGML)) export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) include Makefile.common @@ -194,7 +188,7 @@ META.coq: META.coq.in # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean timingclean alienclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide mlgclean depclean cleanconfig distclean voclean timingclean alienclean clean: objclean cruftclean depclean docclean camldevfilesclean @@ -202,7 +196,7 @@ cleankeepvo: indepclean clean-ide optclean cruftclean depclean docclean objclean: archclean indepclean -cruftclean: ml4clean +cruftclean: mlgclean find . \( -name '*~' -o -name '*.annot' \) -exec rm -f {} + rm -f gmon.out core @@ -252,8 +246,8 @@ clean-ide: rm -f ide/utf8_convert.ml rm -rf $(COQIDEAPP) -ml4clean: - rm -f $(GENML4FILES) $(GENMLGFILES) +mlgclean: + rm -f $(GENMLGFILES) depclean: find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} + @@ -286,7 +280,7 @@ KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO)) EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa') -KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \ +KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(MLPACKFILES:.mlpack=.ml) \ $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ $(MLIFILES:.mli=.cmi) \ @@ -308,7 +302,7 @@ include Makefile.ci .PHONY: tags printenv tags: - echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \ + echo $(filter-out checker/%, $(MLIFILES)) $(filter-out checker/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ etags --language=none\ "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ @@ -317,12 +311,12 @@ tags: "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ "--regex=/module[ \t]+\([^ \t]+\)/\1/" - echo $(ML4FILES) | sort -r | xargs \ + echo $(MLGFILES) | sort -r | xargs \ etags --append --language=none\ "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" checker-tags: - echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(ML4FILES) | sort -r | xargs \ + echo $(filter-out kernel/%, $(MLIFILES)) $(filter-out kernel/%, $(MLSTATICFILES)) $(MLGFILES) | sort -r | xargs \ etags --language=none\ "--regex=/let[ \t]+\([^ \t]+\)/\1/" \ "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \ @@ -331,7 +325,7 @@ checker-tags: "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \ "--regex=/val[ \t]+\([^ \t]+\)/\1/" \ "--regex=/module[ \t]+\([^ \t]+\)/\1/" - echo $(ML4FILES) | sort -r | xargs \ + echo $(MLGFILES) | sort -r | xargs \ etags --append --language=none\ "--regex=/[ \t]*\([^: \t]+\)[ \t]*:/\1/" diff --git a/Makefile.build b/Makefile.build index 08863014ea..fb84a131c7 100644 --- a/Makefile.build +++ b/Makefile.build @@ -86,7 +86,7 @@ byte: coqbyte coqide-byte pluginsbyte printers # This list of ml files used to be in the main Makefile, we moved it here # to avoid exhausting the variable env in Win32 -MLFILES := $(MLSTATICFILES) $(GENMLFILES) $(ML4FILES:.ml4=.ml) +MLFILES := $(MLSTATICFILES) $(GENMLFILES) include Makefile.common include Makefile.vofiles @@ -148,7 +148,7 @@ endif # This include below will lauch the build of all .d. # The - at front is for disabling warnings about currently missing ones. # For creating the missing .d, make will recursively build things like -# coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d). +# coqdep_boot (for the .v.d files) or coqpp (for .mlg -> .ml -> .ml.d). VDFILE := .vfiles MLDFILE := .mlfiles @@ -166,7 +166,7 @@ DEPENDENCIES := \ # of include, and they will then be automatically deleted, leading to an # infinite loop. -.SECONDARY: $(DEPENDENCIES) $(GENFILES) $(ML4FILES:.ml4=.ml) +.SECONDARY: $(DEPENDENCIES) $(GENFILES) $(MLGFILES:.mlg=.ml) ########################################################################### # Compilation options @@ -259,6 +259,7 @@ CAMLP5DEPS:=grammar/grammar.cma CAMLP5USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) +# XXX unused but should be used for mlp files # Main packages linked by Coq. SYSMOD:=-package num,str,unix,dynlink,threads @@ -768,11 +769,6 @@ kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50 $(SHOW)'OCAMLYACC $<' $(HIDE)$(OCAMLYACC) --strict "$*.mly" -%.ml: %.ml4 $(CAMLP5DEPS) $(COQPP) - $(SHOW)'CAMLP5O $<' - $(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) \ - $(CAMLP5DEPS) $(CAMLP5USE) $(CAMLP5COMPAT) -impl $< -o $@ - %.ml: %.mlg $(COQPP) $(SHOW)'COQPP $<' $(HIDE)$(COQPP) $< @@ -782,7 +778,7 @@ kernel/%.cmx: COND_OPTFLAGS+=-w +a-4-44-50 ########################################################################### # Ocamldep is now used directly again (thanks to -ml-synonym in OCaml >= 3.12) -OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack +OCAMLDEP = $(OCAMLFIND) ocamldep -slash -ml-synonym .mlpack MAINMLFILES := $(filter-out checker/% plugins/%, $(MLFILES) $(MLIFILES)) MAINMLLIBFILES := $(filter-out checker/% plugins/%, $(MLLIBFILES) $(MLPACKFILES)) diff --git a/Makefile.ide b/Makefile.ide index 6c069a1e50..39af1f8545 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -49,8 +49,8 @@ IDETOPEXE=bin/coqidetop$(EXE) IDETOP=bin/coqidetop.opt$(EXE) IDETOPBYTE=bin/coqidetop.byte$(EXE) -LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_main.mli ide/coqide_main.ml -LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_main.mli ide/coqide_main.ml +LINKIDE:=$(IDEDEPS) $(IDECDEPS) $(IDECMA) ide/coqide_os_specific.cmo ide/coqide_main.mli ide/coqide_main.ml +LINKIDEOPT:=$(IDEOPTCDEPS) $(patsubst %.cma,%.cmxa,$(IDEDEPS:.cmo=.cmx)) $(IDECMA:.cma=.cmxa) ide/coqide_os_specific.cmx ide/coqide_main.mli ide/coqide_main.ml IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map @@ -110,10 +110,10 @@ $(COQIDEBYTE): $(LINKIDE) $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ \ -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS) $(IDECDEPSFLAGS) $^ -ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp5deps here - $(SHOW)'CAMLP5O $<' - $(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) $(CAMLP5USE) -D$(IDEINT) -impl $< -o $@ - +ide/coqide_os_specific.ml: ide/coqide_$(IDEINT).ml.in config/Makefile + @rm -f $@ + cp $< $@ + @chmod -w $@ ide/%.cmi: ide/%.mli $(SHOW)'OCAMLC $<' diff --git a/checker/inductive.ml b/checker/inductive.ml index 5e34f04f51..269a98cb0e 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -388,7 +388,7 @@ let type_case_branches env (pind,largs) (p,pj) c = let check_case_info env indsp ci = let mib, mip as spec = lookup_mind_specif env indsp in if - not (eq_ind_chk indsp ci.ci_ind) || + not (mind_equiv env indsp ci.ci_ind) || (mib.mind_nparams <> ci.ci_npar) || (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) || (mip.mind_consnrealargs <> ci.ci_cstr_nargs) || diff --git a/checker/reduction.ml b/checker/reduction.ml index 58a3f4e410..1158152f63 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -192,10 +192,7 @@ let convert_constructors | Monomorphic_ind _ | Polymorphic_ind _ -> convert_universes univs u1 u2 | Cumulative_ind cumi -> let num_cnstr_args = - let nparamsctxt = - mind.mind_nparams + mind.mind_packets.(ind).mind_nrealargs - in - nparamsctxt + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1) + mind.mind_nparams + mind.mind_packets.(ind).mind_consnrealargs.(cns - 1) in if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then convert_universes univs u1 u2 diff --git a/clib/cMap.ml b/clib/cMap.ml index 040dede0a2..e4ce6c7c02 100644 --- a/clib/cMap.ml +++ b/clib/cMap.ml @@ -35,6 +35,7 @@ sig val fold_left : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b val height : 'a t -> int + val filter_range : (key -> int) -> 'a t -> 'a t module Smart : sig val map : ('a -> 'a) -> 'a t -> 'a t @@ -62,6 +63,7 @@ sig val fold_left : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b val height : 'a map -> int + val filter_range : (M.t -> int) -> 'a map -> 'a map module Smart : sig val map : ('a -> 'a) -> 'a map -> 'a map @@ -85,8 +87,11 @@ struct if this happens, we can still implement a less clever version of [domain]. *) - type 'a map = 'a Map.Make(M).t - type set = Set.Make(M).t + module F = Map.Make(M) + type 'a map = 'a F.t + + module S = Set.Make(M) + type set = S.t type 'a _map = | MEmpty @@ -164,6 +169,23 @@ struct | MEmpty -> 0 | MNode (_, _, _, _, h) -> h + (* Filter based on a range *) + let filter_range in_range m = + let rec aux m = function + | MEmpty -> m + | MNode (l, k, v, r, _) -> + let vr = in_range k in + (* the range is below the current value *) + if vr < 0 then aux m (map_prj l) + (* the range is above the current value *) + else if vr > 0 then aux m (map_prj r) + (* The current value is in the range *) + else + let m = aux m (map_prj l) in + let m = aux m (map_prj r) in + F.add k v m + in aux F.empty (map_prj m) + module Smart = struct diff --git a/clib/cMap.mli b/clib/cMap.mli index f5496239f6..ca6ddb2f4e 100644 --- a/clib/cMap.mli +++ b/clib/cMap.mli @@ -60,6 +60,12 @@ sig val height : 'a t -> int (** An indication of the logarithmic size of a map *) + val filter_range : (key -> int) -> 'a t -> 'a t + (** [find_range in_range m] Given a comparison function [in_range x], + that tests if [x] is below, above, or inside a given range + [filter_range] returns the submap of [m] whose keys are in + range. Note that [in_range] has to define a continouous range. *) + module Smart : sig val map : ('a -> 'a) -> 'a t -> 'a t diff --git a/clib/hMap.ml b/clib/hMap.ml index 33cb6d0131..9c80398e4d 100644 --- a/clib/hMap.ml +++ b/clib/hMap.ml @@ -398,6 +398,10 @@ struct let height s = Int.Map.height s + (* Not as efficient as the original version *) + let filter_range f s = + filter (fun x _ -> f x = 0) s + module Unsafe = struct let map f s = diff --git a/default.nix b/default.nix index 9a7afbe89e..7c8113c9ab 100644 --- a/default.nix +++ b/default.nix @@ -23,8 +23,8 @@ { pkgs ? (import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/06613c189eebf4d6167d2d010a59cf38b43b6ff4.tar.gz"; - sha256 = "13grhy3cvdwr7wql1rm5d7zsfpvp44cyjhiain4zs70r90q3swdg"; + url = "https://github.com/NixOS/nixpkgs/archive/69522a0acf8e840e8b6ac0a9752a034ab74eb3c0.tar.gz"; + sha256 = "12k80gd4lkw9h9y1szvmh0jmh055g3b6wnphmx4ab1qdwlfaylnx"; }) {}) , ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06 , buildIde ? true @@ -33,6 +33,7 @@ , shell ? false # We don't use lib.inNixShell because that would also apply # when in a nix-shell of some package depending on this one. +, coq-version ? "8.10-git" }: with pkgs; @@ -101,7 +102,20 @@ stdenv.mkDerivation rec { installCheckTarget = [ "check" ]; - passthru = { inherit ocamlPackages; }; + passthru = { + inherit coq-version ocamlPackages; + dontFilter = true; # Useful to use mkCoqPackages from <nixpkgs> + }; + + setupHook = writeText "setupHook.sh" " + addCoqPath () { + if test -d \"$1/lib/coq/${coq-version}/user-contrib\"; then + export COQPATH=\"$COQPATH\${COQPATH:+:}$1/lib/coq/${coq-version}/user-contrib/\" + fi + } + + addEnvHooks \"$targetOffset\" addCoqPath + "; meta = { description = "Coq proof assistant"; @@ -113,6 +127,7 @@ stdenv.mkDerivation rec { ''; homepage = http://coq.inria.fr; license = licenses.lgpl21; + platforms = platforms.unix; }; } diff --git a/dev/ci/user-overlays/08844-split-tactics.sh b/dev/ci/user-overlays/08844-split-tactics.sh new file mode 100644 index 0000000000..8ad8cba243 --- /dev/null +++ b/dev/ci/user-overlays/08844-split-tactics.sh @@ -0,0 +1,12 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "8844" ] || [ "$CI_BRANCH" = "split-tactics" ]; then + Equations_CI_REF=split-tactics + Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + ltac2_CI_REF=split-tactics + ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2 + + fiat_parsers_CI_REF=split-tactics + fiat_parsers_CI_GITURL=https://github.com/SkySkimmer/fiat +fi diff --git a/dev/doc/proof-engine.md b/dev/doc/proof-engine.md index 8f96ac223f..774552237a 100644 --- a/dev/doc/proof-engine.md +++ b/dev/doc/proof-engine.md @@ -42,8 +42,8 @@ goal holes thanks to the `Refine` module, and in particular to the `Refine.refine` primitive. ```ocaml -val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic -(** In [refine typecheck t], [t] is a term with holes under some +val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit tactic +(** In [refine ~typecheck t], [t] is a term with holes under some [evar_map] context. The term [t] is used as a partial solution for the current goal (refine is a goal-dependent tactic), the new holes created by [t] become the new subgoals. Exceptions @@ -51,12 +51,11 @@ val refine : typecheck:bool -> Constr.t Sigma.run -> unit tactic tactic failures. If [typecheck] is [true] [t] is type-checked beforehand. *) ``` -In a first approximation, we can think of `'a Sigma.run` as -`evar_map -> 'a * evar_map`. What the function does is first evaluate the -`Constr.t Sigma.run` argument in the current proof state, and then use the -resulting term as a filler for the proof under focus. All evars that have been -created by the invocation of this thunk are then turned into new goals added in -the order of their creation. +What the function does is first evaluate the `t` argument in the +current proof state, and then use the resulting term as a filler for +the proof under focus. All evars that have been created by the +invocation of this thunk are then turned into new goals added in the +order of their creation. To see how we can use it, let us have a look at an idealized example, the `cut` tactic. Assuming `X` is a type, `cut X` fills the current goal `[Γ ⊢ _ : A]` @@ -66,8 +65,7 @@ two new holes `[e1, e2]` are added to the goal state in this order. ```ocaml let cut c = - let open Sigma in - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> (** In this block, we focus on one goal at a time indicated by gl *) let env = Proofview.Goal.env gl in (** Get the context of the goal, essentially [Γ] *) @@ -80,25 +78,22 @@ let cut c = let t = mkArrow c (Vars.lift 1 concl) in (** Build [X -> A]. Note the lifting of [A] due to being on the right hand side of the arrow. *) - Refine.refine { run = begin fun sigma -> + Refine.refine begin fun sigma -> (** All evars generated by this block will be added as goals *) - let Sigma (f, sigma, p) = Evarutil.new_evar env sigma t in + let sigma, f = Evarutil.new_evar env sigma t in (** Generate ?e1 : [Γ ⊢ _ : X -> A], add it to sigma, and return the term [f := Γ ⊢ ?e1{Γ} : X -> A] with the updated sigma. The identity substitution for [Γ] is extracted from the [env] argument, so that one must be careful to pass the correct context here in order for the resulting term to be well-typed. The [p] return value is a proof term used to enforce sigma monotonicity. *) - let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c in + let sigma, x = Evarutil.new_evar env sigma c in (** Generate ?e2 : [Γ ⊢ _ : X] in sigma and return [x := Γ ⊢ ?e2{Γ} : X]. *) let r = mkLetIn (Name id, x, c, mkApp (Vars.lift 1 r, [|mkRel 1|])) in (** Build [r := Γ ⊢ let id : X := ?e2{Γ} in ?e1{Γ} id : A] *) - Sigma (r, sigma, p +> q) - (** Fills the current hole with [r]. The [p +> q] thingy ensures - monotonicity of sigma. *) - end } - end } + end + end ``` The `Evarutil.new_evar` function is the preferred way to generate evars in diff --git a/dev/tools/change-header b/dev/tools/change-header index 61cc866602..687c02f4f1 100755 --- a/dev/tools/change-header +++ b/dev/tools/change-header @@ -22,7 +22,7 @@ lineb='(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)' modified=0 kept=0 -for i in `find . -name \*.mli -o -name \*.ml -o -name \*.ml4 -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do +for i in `find . -name \*.mli -o -name \*.ml -o -name \*.mlg -o -name \*.mll -o -name \*.mly -o -name \*.mlp -o -name \*.v`; do headline=`head -n 1 $i` if `echo $headline | grep "(\* -\*- .* \*)" > /dev/null`; then # Has emacs header diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 835d6dcaa6..cc5d9d6205 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -678,7 +678,7 @@ form*. There are several ways (or strategies) to apply the reduction rules. Among them, we have to mention the *head reduction* which will play an important role (see Chapter :ref:`tactics`). Any term :math:`t` can be written as :math:`λ x_1 :T_1 . … λ x_k :T_k . (t_0~t_1 … t_n )` where :math:`t_0` is not an -application. We say then that :math:`t~0` is the *head of* :math:`t`. If we assume +application. We say then that :math:`t_0` is the *head of* :math:`t`. If we assume that :math:`t_0` is :math:`λ x:T. u_0` then one step of β-head reduction of :math:`t` is: .. math:: @@ -771,8 +771,8 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is \odd&:&\nat → \Prop \end{array}\right]} {\left[\begin{array}{rcl} \evenO &:& \even~0\\ - \evenS &:& \forall n, \odd~n -> \even~(\kw{S}~n)\\ - \oddS &:& \forall n, \even~n -> \odd~(\kw{S}~n) + \evenS &:& \forall n, \odd~n → \even~(\kw{S}~n)\\ + \oddS &:& \forall n, \even~n → \odd~(\kw{S}~n) \end{array}\right]} which corresponds to the result of the |Coq| declaration: diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 3385b78958..cfc4bea85f 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -99,6 +99,14 @@ let isFix sigma c = match kind sigma c with Fix _ -> true | _ -> false let isCoFix sigma c = match kind sigma c with CoFix _ -> true | _ -> false let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false + +let rec isType sigma c = match kind sigma c with + | Sort s -> (match ESorts.kind sigma s with + | Sorts.Type _ -> true + | _ -> false ) + | Cast (c,_,_) -> isType sigma c + | _ -> false + let isVarId sigma id c = match kind sigma c with Var id' -> Id.equal id id' | _ -> false let isRelN sigma n c = diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 1edc0ee12b..6532e08e9d 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -157,6 +157,8 @@ val isCoFix : Evd.evar_map -> t -> bool val isCase : Evd.evar_map -> t -> bool val isProj : Evd.evar_map -> t -> bool +val isType : Evd.evar_map -> constr -> bool + type arity = rel_context * ESorts.t val destArity : Evd.evar_map -> types -> arity val isArity : Evd.evar_map -> t -> bool diff --git a/engine/evd.ml b/engine/evd.ml index 3a77a2b440..b3848e1b5b 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -483,6 +483,8 @@ let is_typeclass_evar evd evk = let flags = evd.evar_flags in Evar.Set.mem evk flags.typeclass_evars +let get_obligation_evars evd = evd.evar_flags.obligation_evars + let set_obligation_evar evd evk = let flags = evd.evar_flags in let evar_flags = { flags with obligation_evars = Evar.Set.add evk flags.obligation_evars } in diff --git a/engine/evd.mli b/engine/evd.mli index b0e3c2b869..be54bebcd7 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -262,6 +262,9 @@ val get_typeclass_evars : evar_map -> Evar.Set.t val is_typeclass_evar : evar_map -> Evar.t -> bool (** Is the evar declared resolvable for typeclass resolution *) +val get_obligation_evars : evar_map -> Evar.Set.t +(** The set of obligation evars *) + val set_obligation_evar : evar_map -> Evar.t -> evar_map (** Declare an evar as an obligation *) diff --git a/engine/termops.ml b/engine/termops.ml index f720e5195d..52880846f8 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -366,12 +366,18 @@ let pr_evar_map_gen with_univs pr_evars env sigma = else str "TYPECLASSES:" ++ brk (0, 1) ++ prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl () + and obligations = + let evars = Evd.get_obligation_evars sigma in + if Evar.Set.is_empty evars then mt () + else + str "OBLIGATIONS:" ++ brk (0, 1) ++ + prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl () and metas = if List.is_empty (Evd.meta_list sigma) then mt () else str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma in - evs ++ svs ++ cstrs ++ typeclasses ++ metas + evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas let pr_evar_list env sigma l = let open Evd in @@ -1173,7 +1179,7 @@ let isGlobalRef sigma c = | Const _ | Ind _ | Construct _ | Var _ -> true | _ -> false -let is_template_polymorphic env sigma f = +let is_template_polymorphic_ind env sigma f = match EConstr.kind sigma f with | Ind (ind, u) -> if not (EConstr.EInstance.is_empty u) then false diff --git a/engine/termops.mli b/engine/termops.mli index 1054fbbc5e..07c9541f25 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -282,7 +282,7 @@ val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool val isGlobalRef : Evd.evar_map -> constr -> bool -val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool +val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool val is_Prop : Evd.evar_map -> constr -> bool val is_Set : Evd.evar_map -> constr -> bool diff --git a/ide/coqide_QUARTZ.ml.in b/ide/coqide_QUARTZ.ml.in new file mode 100644 index 0000000000..a08bac5772 --- /dev/null +++ b/ide/coqide_QUARTZ.ml.in @@ -0,0 +1,37 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +let osx = GosxApplication.osxapplication () + +let () = + let _ = osx#connect#ns_application_open_file + ~callback:(fun x -> Coqide.do_load x; true) + in + let _ = osx#connect#ns_application_block_termination + ~callback:Coqide.forbid_quit + in + let _ = osx#connect#ns_application_will_terminate + ~callback:Coqide.close_and_quit + in () + +let init () = + let () = GtkosxApplication.Application.set_menu_bar osx#as_osxapplication + (GtkMenu.MenuShell.cast + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget) + in + let () = GtkosxApplication.Application.insert_app_menu_item + osx#as_osxapplication + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1 + in + let () = GtkosxApplication.Application.set_help_menu osx#as_osxapplication + (Some (GtkMenu.MenuItem.cast + (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget)) + in + osx#ready () diff --git a/ide/coqide_WIN32.ml.in b/ide/coqide_WIN32.ml.in new file mode 100644 index 0000000000..8c4649fc39 --- /dev/null +++ b/ide/coqide_WIN32.ml.in @@ -0,0 +1,50 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* On win32, we add the directory of coqide to the PATH at launch-time + (this used to be done in a .bat script). *) + +let set_win32_path () = + Unix.putenv "PATH" + (Filename.dirname Sys.executable_name ^ ";" ^ + (try Sys.getenv "PATH" with _ -> "")) + +(* On win32, since coqide is now console-free, we re-route stdout/stderr + to avoid Sys_error if someone writes to them. We write to a pipe which + is never read (by default) or to a temp log file (when in debug mode). +*) + +let reroute_stdout_stderr () = + (* We anticipate a bit the argument parsing and look for -debug *) + let debug = List.mem "-debug" (Array.to_list Sys.argv) in + Minilib.debug := debug; + let out_descr = + if debug then + let (name,chan) = Filename.open_temp_file "coqide_" ".log" in + Coqide.logfile := Some name; + Unix.descr_of_out_channel chan + else + snd (Unix.pipe ()) + in + Unix.set_close_on_exec out_descr; + Unix.dup2 out_descr Unix.stdout; + Unix.dup2 out_descr Unix.stderr + +(* We also provide specific kill and interrupt functions. *) + +external win32_kill : int -> unit = "win32_kill" +external win32_interrupt : int -> unit = "win32_interrupt" +let () = + Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; + set_win32_path (); + Coq.interrupter := win32_interrupt; + reroute_stdout_stderr () + +let init () = () diff --git a/ide/coqide_X11.ml.in b/ide/coqide_X11.ml.in new file mode 100644 index 0000000000..6a5784eac3 --- /dev/null +++ b/ide/coqide_X11.ml.in @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +let init () = () diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml index 3a92e1bc91..91e8be875a 100644 --- a/ide/coqide_main.ml4 +++ b/ide/coqide_main.ml @@ -49,88 +49,6 @@ let catch_gtk_messages () = let () = catch_gtk_messages () - - -(** System-dependent settings *) - -let os_specific_init () = () - -(** Win32 *) - -IFDEF WIN32 THEN - -(* On win32, we add the directory of coqide to the PATH at launch-time - (this used to be done in a .bat script). *) - -let set_win32_path () = - Unix.putenv "PATH" - (Filename.dirname Sys.executable_name ^ ";" ^ - (try Sys.getenv "PATH" with _ -> "")) - -(* On win32, since coqide is now console-free, we re-route stdout/stderr - to avoid Sys_error if someone writes to them. We write to a pipe which - is never read (by default) or to a temp log file (when in debug mode). -*) - -let reroute_stdout_stderr () = - (* We anticipate a bit the argument parsing and look for -debug *) - let debug = List.mem "-debug" (Array.to_list Sys.argv) in - Minilib.debug := debug; - let out_descr = - if debug then - let (name,chan) = Filename.open_temp_file "coqide_" ".log" in - Coqide.logfile := Some name; - Unix.descr_of_out_channel chan - else - snd (Unix.pipe ()) - in - Unix.set_close_on_exec out_descr; - Unix.dup2 out_descr Unix.stdout; - Unix.dup2 out_descr Unix.stderr - -(* We also provide specific kill and interrupt functions. *) - -external win32_kill : int -> unit = "win32_kill" -external win32_interrupt : int -> unit = "win32_interrupt" -let () = - Coq.gio_channel_of_descr_socket := Glib.Io.channel_of_descr_socket; - set_win32_path (); - Coq.interrupter := win32_interrupt; - reroute_stdout_stderr () -END - -(** MacOSX *) - -IFDEF QUARTZ THEN -let osx = GosxApplication.osxapplication () - -let () = - let _ = osx#connect#ns_application_open_file - ~callback:(fun x -> Coqide.do_load x; true) - in - let _ = osx#connect#ns_application_block_termination - ~callback:Coqide.forbid_quit - in - let _ = osx#connect#ns_application_will_terminate - ~callback:Coqide.close_and_quit - in () - -let os_specific_init () = - let () = GtkosxApplication.Application.set_menu_bar osx#as_osxapplication - (GtkMenu.MenuShell.cast - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget) - in - let () = GtkosxApplication.Application.insert_app_menu_item - osx#as_osxapplication - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1 - in - let () = GtkosxApplication.Application.set_help_menu osx#as_osxapplication - (Some (GtkMenu.MenuItem.cast - (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget)) - in - osx#ready () -END - let load_prefs () = try Preferences.load_pref () with e -> Ideutils.flash_info @@ -145,7 +63,7 @@ let () = Coq.check_connection args; Coqide.sup_args := args; Coqide.main files; - os_specific_init (); + Coqide_os_specific.init (); try GMain.main (); failwith "Gtk loop ended" diff --git a/ide/coqide_os_specific.mli b/ide/coqide_os_specific.mli new file mode 100644 index 0000000000..ebd09099f0 --- /dev/null +++ b/ide/coqide_os_specific.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val init : unit -> unit @@ -33,9 +33,9 @@ (libraries coqide-server.protocol coqide-server.core lablgtk2.sourceview2)) (rule - (targets coqide_main.ml) - (deps (:ml4-file coqide_main.ml4)) - (action (run coqmlp5 -loc loc -impl %{ml4-file} -o %{targets}))) + (targets coqide_os_specific.ml) + (deps (:in-file coqide_X11.ml.in)) ; TODO support others + (action (run cp %{in-file} %{targets}))) (executable (name coqide_main) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 601099c6ff..838ef40545 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -480,6 +480,9 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (make_pat_notation ?loc ntn (l,ll) l2') key) end | SynDefRule kn -> + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> let qid = Nametab.shortest_qualid_of_syndef ?loc vars kn in let l1 = List.rev_map (fun (c,(subentry,(scopt,scl))) -> @@ -493,7 +496,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) |None -> raise No_match in assert (List.is_empty substlist); - mkPat ?loc qid (List.rev_append l1 l2') + insert_pat_coercion ?loc coercion (mkPat ?loc qid (List.rev_append l1 l2')) and extern_notation_pattern allscopes vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> @@ -1131,12 +1134,15 @@ and extern_notation (custom,scopes as allscopes) vars t = function binderlists in insert_coercion coercion (insert_delimiters (make_notation loc ntn (l,ll,bl,bll)) key)) | SynDefRule kn -> + match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> let l = List.map (fun (c,(subentry,(scopt,scl))) -> extern true (subentry,(scopt,scl@snd scopes)) vars c, None) terms in let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in - CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in + insert_coercion coercion (CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l)) in if List.is_empty args then e else let args = fill_arg_scopes args argsscopes allscopes in diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c03a5fee90..02db8f6aab 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -737,7 +737,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in try let gc = intern nenv c in - Id.Map.add id (gc, Some c) map + Id.Map.add id (gc, None) map with Nametab.GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = @@ -2051,15 +2051,22 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let (ltacvars, ntnvars) = lvar in (* Preventively declare notation variables in ltac as non-bindings *) Id.Map.iter (fun x (used_as_binder,_,_) -> used_as_binder := false) ntnvars; - let ntnvars = Id.Map.domain ntnvars in let extra = ltacvars.ltac_extra in + (* We inform ltac that the interning vars and the notation vars are bound *) + (* but we could instead rely on the "intern_sign" *) let lvars = Id.Set.union ltacvars.ltac_bound ltacvars.ltac_vars in - let lvars = Id.Set.union lvars ntnvars in + let lvars = Id.Set.union lvars (Id.Map.domain ntnvars) in let ltacvars = Id.Set.union lvars env.ids in + (* Propagating enough information for mutual interning with tac-in-term *) + let intern_sign = { + Genintern.intern_ids = env.ids; + Genintern.notation_variable_status = ntnvars + } in let ist = { Genintern.genv = globalenv; ltacvars; extra; + intern_sign; } in let (_, glb) = Genintern.generic_intern ist gen in Some glb @@ -2344,16 +2351,23 @@ let intern_constr_pattern env sigma ?(as_type=false) ?(ltacvars=empty_ltac_sign) ~pattern_mode:true ~ltacvars env sigma c in pattern_of_glob_constr c +let intern_core kind env sigma ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) + { Genintern.intern_ids = ids; Genintern.notation_variable_status = vl } c = + let tmp_scope = scope_of_type_kind sigma kind in + let impls = empty_internalization_env in + internalize env {ids; unb = false; tmp_scope; scopes = []; impls} + pattern_mode (ltacvars, vl) c + let interp_notation_constr env ?(impls=empty_internalization_env) nenv a = + let ids = extract_ids env in (* [vl] is intended to remember the scope of the free variables of [a] *) let vl = Id.Map.map (fun typ -> (ref false, ref None, typ)) nenv.ninterp_var_type in let impls = Id.Map.fold (fun id _ impls -> Id.Map.remove id impls) nenv.ninterp_var_type impls in - let c = internalize (Global.env()) {ids = extract_ids env; unb = false; - tmp_scope = None; scopes = []; impls = impls} + let c = internalize env {ids; unb = false; tmp_scope = None; scopes = []; impls} false (empty_ltac_sign, vl) a in + (* Splits variables into those that are binding, bound, or both *) (* Translate and check that [c] has all its free variables bound in [vars] *) let a, reversible = notation_constr_of_glob_constr nenv c in - (* Splits variables into those that are binding, bound, or both *) (* binding and bound *) let out_scope = function None -> None,[] | Some (a,l) -> a,l in let unused = match reversible with NonInjective ids -> ids | _ -> [] in diff --git a/interp/constrintern.mli b/interp/constrintern.mli index dd0944cc48..147a903fe2 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -185,6 +185,13 @@ val interp_notation_constr : env -> ?impls:internalization_env -> notation_interp_env -> constr_expr -> (bool * subscopes) Id.Map.t * notation_constr * reversibility_status +(** Idem but to glob_constr (weaker check of binders) *) + +val intern_core : typing_constraint -> + env -> evar_map -> ?pattern_mode:bool -> ?ltacvars:ltac_sign -> + Genintern.intern_variable_status -> constr_expr -> + glob_constr + (** Globalization options *) val parsing_explicit : bool ref diff --git a/interp/genintern.ml b/interp/genintern.ml index d9a0db040a..1b736b7977 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -14,16 +14,31 @@ open Genarg module Store = Store.Make () +type intern_variable_status = { + intern_ids : Id.Set.t; + notation_variable_status : + (bool ref * Notation_term.subscopes option ref * + Notation_term.notation_var_internalization_type) + Id.Map.t +} + type glob_sign = { ltacvars : Id.Set.t; genv : Environ.env; extra : Store.t; + intern_sign : intern_variable_status; +} + +let empty_intern_sign = { + intern_ids = Id.Set.empty; + notation_variable_status = Id.Map.empty; } let empty_glob_sign env = { ltacvars = Id.Set.empty; genv = env; extra = Store.empty; + intern_sign = empty_intern_sign; } (** In globalize tactics, we need to keep the initial [constr_expr] to recompute diff --git a/interp/genintern.mli b/interp/genintern.mli index f4f064bcac..4100f39029 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -14,10 +14,19 @@ open Genarg module Store : Store.S +type intern_variable_status = { + intern_ids : Id.Set.t; + notation_variable_status : + (bool ref * Notation_term.subscopes option ref * + Notation_term.notation_var_internalization_type) + Id.Map.t +} + type glob_sign = { ltacvars : Id.Set.t; genv : Environ.env; extra : Store.t; + intern_sign : intern_variable_status; } val empty_glob_sign : Environ.env -> glob_sign diff --git a/interp/interp.mllib b/interp/interp.mllib index 3668455aeb..aa20bda705 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -3,8 +3,8 @@ Genredexpr Redops Tactypes Stdarg -Genintern Notation_term +Genintern Notation_ops Notation Syntax_def diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index c558689595..95546a83e1 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -21,6 +21,8 @@ (* This file implements a lazy reduction for the Calculus of Inductive Constructions *) +[@@@ocaml.warning "+4"] + open CErrors open Util open Pp @@ -255,7 +257,7 @@ open Context.Named.Declaration let assoc_defined id env = match Environ.lookup_named id env with | LocalDef (_, c, _) -> c -| _ -> raise Not_found +| LocalAssum _ -> raise Not_found (**********************************************************************) (* Lazy reduction: the one used in kernel operations *) @@ -310,7 +312,7 @@ and fterm = let fterm_of v = v.term let set_norm v = v.norm <- Norm -let is_val v = match v.norm with Norm -> true | _ -> false +let is_val v = match v.norm with Norm -> true | Cstr | Whnf | Red -> false let mk_atom c = {norm=Norm;term=FAtom c} let mk_red f = {norm=Red;term=f} @@ -359,20 +361,21 @@ let append_stack v s = if Int.equal (Array.length v) 0 then s else match s with | Zapp l :: s -> Zapp (Array.append v l) :: s - | _ -> Zapp v :: s + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> + Zapp v :: s (* Collapse the shifts in the stack *) let zshift n s = match (n,s) with (0,_) -> s | (_,Zshift(k)::s) -> Zshift(n+k)::s - | _ -> Zshift(n)::s + | (_,(ZcaseT _ | Zproj _ | Zfix _ | Zapp _ | Zupdate _) :: _) | _,[] -> Zshift(n)::s let rec stack_args_size = function | Zapp v :: s -> Array.length v + stack_args_size s | Zshift(_)::s -> stack_args_size s | Zupdate(_)::s -> stack_args_size s - | _ -> 0 + | (ZcaseT _ | Zproj _ | Zfix _) :: _ | [] -> 0 (* When used as an argument stack (only Zapp can appear) *) let rec decomp_stack = function @@ -382,12 +385,12 @@ let rec decomp_stack = function | 1 -> Some (v.(0), s) | _ -> Some (v.(0), (Zapp (Array.sub v 1 (Array.length v - 1)) :: s))) - | _ -> None + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> None let array_of_stack s = let rec stackrec = function | [] -> [] | Zapp args :: s -> args :: (stackrec s) - | _ -> assert false + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ -> assert false in Array.concat (stackrec s) let rec stack_assign s p c = match s with | Zapp args :: s -> @@ -398,7 +401,7 @@ let rec stack_assign s p c = match s with (let nargs = Array.copy args in nargs.(p) <- c; Zapp nargs :: s) - | _ -> s + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> s let rec stack_tail p s = if Int.equal p 0 then s else match s with @@ -406,13 +409,13 @@ let rec stack_tail p s = let q = Array.length args in if p >= q then stack_tail (p-q) s else Zapp (Array.sub args p (q-p)) :: s - | _ -> failwith "stack_tail" + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> failwith "stack_tail" let rec stack_nth s p = match s with | Zapp args :: s -> let q = Array.length args in if p >= q then stack_nth s (p-q) else args.(p) - | _ -> raise Not_found + | (ZcaseT _ | Zproj _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] -> raise Not_found (* Lifting. Preserves sharing (useful only for cell with norm=Red). lft_fconstr always create a new cell, while lift_fconstr avoids it @@ -426,7 +429,7 @@ let rec lft_fconstr n ft = | FCoFix(cfx,e) -> {norm=Cstr; term=FCoFix(cfx,subs_shft(n,e))} | FLIFT(k,m) -> lft_fconstr (n+k) m | FLOCKED -> assert false - | FFlex _ | FAtom _ | FApp _ | FProj _ | FCaseT _ | FProd _ + | FFlex (RelKey _) | FAtom _ | FApp _ | FProj _ | FCaseT _ | FProd _ | FLetIn _ | FEvar _ | FCLOS _ -> {norm=ft.norm; term=FLIFT(n,ft)} let lift_fconstr k f = if Int.equal k 0 then f else lft_fconstr k f @@ -451,13 +454,14 @@ let compact_stack head stk = (** The stack contains [Zupdate] marks only if in sharing mode *) let _ = update ~share:true m h'.norm h'.term in strip_rec depth s - | stk -> zshift depth stk in + | ((ZcaseT _ | Zproj _ | Zfix _ | Zapp _) :: _ | []) as stk -> zshift depth stk + in strip_rec 0 stk (* Put an update mark in the stack, only if needed *) let zupdate info m s = let share = info.i_cache.i_share in - if share && begin match m.norm with Red -> true | _ -> false end + if share && begin match m.norm with Red -> true | Norm | Whnf | Cstr -> false end then let s' = compact_stack m s in let _ = m.term <- FLOCKED in @@ -469,12 +473,12 @@ let mk_lambda env t = FLambda(List.length rvars, List.rev rvars, t', env) let destFLambda clos_fun t = - match t.term with - FLambda(_,[(na,ty)],b,e) -> (na,clos_fun e ty,clos_fun (subs_lift e) b) - | FLambda(n,(na,ty)::tys,b,e) -> - (na,clos_fun e ty,{norm=Cstr;term=FLambda(n-1,tys,b,subs_lift e)}) - | _ -> assert false - (* t must be a FLambda and binding list cannot be empty *) + match [@ocaml.warning "-4"] t.term with + | FLambda(_,[(na,ty)],b,e) -> (na,clos_fun e ty,clos_fun (subs_lift e) b) + | FLambda(n,(na,ty)::tys,b,e) -> + (na,clos_fun e ty,{norm=Cstr;term=FLambda(n-1,tys,b,subs_lift e)}) + | _ -> assert false +(* t must be a FLambda and binding list cannot be empty *) (* Optimization: do not enclose variables in a closure. Makes variable access much faster *) @@ -602,7 +606,7 @@ let rec to_constr lfts v = subst_constr subs t | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*) -and subst_constr subst c = match Constr.kind c with +and subst_constr subst c = match [@ocaml.warning "-4"] Constr.kind c with | Rel i -> begin match expand_rel i subst with | Inl (k, lazy v) -> Vars.lift k v @@ -664,15 +668,17 @@ let strip_update_shift_app_red head stk = | Zupdate(m)::s -> (** The stack contains [Zupdate] marks only if in sharing mode *) strip_rec rstk (update ~share:true m h.norm h.term) depth s - | stk -> (depth,List.rev rstk, stk) in + | ((ZcaseT _ | Zproj _ | Zfix _) :: _ | []) as stk -> + (depth,List.rev rstk, stk) + in strip_rec [] head 0 stk let strip_update_shift_app head stack = - assert (match head.norm with Red -> false | _ -> true); + assert (match head.norm with Red -> false | Norm | Cstr | Whnf -> true); strip_update_shift_app_red head stack let get_nth_arg head n stk = - assert (match head.norm with Red -> false | _ -> true); + assert (match head.norm with Red -> false | Norm | Cstr | Whnf -> true); let rec strip_rec rstk h n = function | Zshift(k) as e :: s -> strip_rec (e::rstk) (lift_fconstr k h) n s @@ -690,14 +696,13 @@ let get_nth_arg head n stk = | Zupdate(m)::s -> (** The stack contains [Zupdate] mark only if in sharing mode *) strip_rec rstk (update ~share:true m h.norm h.term) n s - | s -> (None, List.rev rstk @ s) in + | ((ZcaseT _ | Zproj _ | Zfix _) :: _ | []) as s -> (None, List.rev rstk @ s) in strip_rec [] head n stk (* Beta reduction: look for an applied argument in the stack. Since the encountered update marks are removed, h must be a whnf *) -let rec get_args n tys f e stk = - match stk with - Zupdate r :: s -> +let rec get_args n tys f e = function + | Zupdate r :: s -> (** The stack contains [Zupdate] mark only if in sharing mode *) let _hd = update ~share:true r Cstr (FLambda(n,tys,f,e)) in get_args n tys f e s @@ -713,7 +718,8 @@ let rec get_args n tys f e stk = else (* more lambdas *) let etys = List.skipn na tys in get_args (n-na) etys f (subs_cons(l,e)) s - | _ -> (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk) + | ((ZcaseT _ | Zproj _ | Zfix _) :: _ | []) as stk -> + (Inr {norm=Cstr;term=FLambda(n,tys,f,e)}, stk) (* Eta expansion: add a reference to implicit surrounding lambda at end of stack *) let rec eta_expand_stack = function @@ -725,19 +731,17 @@ let rec eta_expand_stack = function (* Iota reduction: extract the arguments to be passed to the Case branches *) -let rec reloc_rargs_rec depth stk = - match stk with - Zapp args :: s -> - Zapp (lift_fconstr_vect depth args) :: reloc_rargs_rec depth s - | Zshift(k)::s -> if Int.equal k depth then s else reloc_rargs_rec (depth-k) s - | _ -> stk +let rec reloc_rargs_rec depth = function + | Zapp args :: s -> + Zapp (lift_fconstr_vect depth args) :: reloc_rargs_rec depth s + | Zshift(k)::s -> if Int.equal k depth then s else reloc_rargs_rec (depth-k) s + | ((ZcaseT _ | Zproj _ | Zfix _ | Zupdate _) :: _ | []) as stk -> stk let reloc_rargs depth stk = if Int.equal depth 0 then stk else reloc_rargs_rec depth stk -let rec try_drop_parameters depth n argstk = - match argstk with - Zapp args::s -> +let rec try_drop_parameters depth n = function + | Zapp args::s -> let q = Array.length args in if n > q then try_drop_parameters depth (n-q) s else if Int.equal n q then reloc_rargs depth s @@ -748,7 +752,7 @@ let rec try_drop_parameters depth n argstk = | [] -> if Int.equal n 0 then [] else raise Not_found - | _ -> assert false + | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _) :: _ -> assert false (* strip_update_shift_app only produces Zapp and Zshift items *) let drop_parameters depth n argstk = @@ -788,13 +792,12 @@ let eta_expand_ind_stack env ind m s (f, s') = argss, [Zapp hstack] | None -> raise Not_found (* disallow eta-exp for non-primitive records *) -let rec project_nth_arg n argstk = - match argstk with +let rec project_nth_arg n = function | Zapp args :: s -> let q = Array.length args in if n >= q then project_nth_arg (n - q) s else (* n < q *) args.(n) - | _ -> assert false + | (ZcaseT _ | Zproj _ | Zfix _ | Zupdate _ | Zshift _) :: _ | [] -> assert false (* After drop_parameters we have a purely applicative stack *) @@ -809,7 +812,7 @@ let rec project_nth_arg n argstk = (* does not deal with FLIFT *) let contract_fix_vect fix = let (thisbody, make_body, env, nfix) = - match fix with + match [@ocaml.warning "-4"] fix with | FFix (((reci,i),(_,_,bds as rdcl)),env) -> (bds.(i), (fun j -> { norm = Cstr; term = FFix (((reci,j),rdcl),env) }), @@ -900,7 +903,7 @@ let rec knr info tab m stk = let use_match = red_set info.i_flags fMATCH in let use_fix = red_set info.i_flags fFIX in if use_match || use_fix then - (match strip_update_shift_app m stk with + (match [@ocaml.warning "-4"] strip_update_shift_app m stk with | (depth, args, ZcaseT(ci,_,br,e)::s) when use_match -> assert (ci.ci_npar>=0); let rargs = drop_parameters depth ci.ci_npar args in @@ -918,17 +921,17 @@ let rec knr info tab m stk = else (m,stk) | FCoFix _ when red_set info.i_flags fCOFIX -> (match strip_update_shift_app m stk with - (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> + | (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in knit info tab fxe fxbd (args@stk') - | (_,args,s) -> (m,args@s)) + | (_,args, ((Zapp _ | Zfix _ | Zshift _ | Zupdate _) :: _ | [] as s)) -> (m,args@s)) | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA -> knit info tab (subs_cons([|v|],e)) bd stk | FEvar(ev,env) -> (match info.i_cache.i_sigma ev with Some c -> knit info tab env c stk | None -> (m,stk)) - | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FApp _ | FProj _ + | FLOCKED | FRel _ | FAtom _ | FFlex (RelKey _ | ConstKey _ | VarKey _) | FInd _ | FApp _ | FProj _ | FFix _ | FCoFix _ | FCaseT _ | FLambda _ | FProd _ | FLetIn _ | FLIFT _ | FCLOS _ -> (m, stk) @@ -1057,4 +1060,4 @@ let unfold_reference info tab key = if red_set info.i_flags (fVAR i) then ref_value_cache info tab key else None - | _ -> ref_value_cache info tab key + | RelKey _ -> ref_value_cache info tab key diff --git a/kernel/environ.ml b/kernel/environ.ml index 3b7e3ae544..e341412294 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -440,6 +440,16 @@ let constant_value_and_type env (kn, u) = | Undef _ -> None in b', cb.const_type, Univ.Constraint.empty +let body_of_constant_body env cb = + let otab = opaque_tables env in + match cb.const_body with + | Undef _ -> + None + | Def c -> + Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb) + | OpaqueDef o -> + Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb) + (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) @@ -694,6 +704,22 @@ let is_polymorphic env r = | IndRef ind -> polymorphic_ind ind env | ConstructRef cstr -> polymorphic_ind (inductive_of_constructor cstr) env +let is_template_polymorphic env r = + let open Names.GlobRef in + match r with + | VarRef _id -> false + | ConstRef _c -> false + | IndRef ind -> template_polymorphic_ind ind env + | ConstructRef cstr -> template_polymorphic_ind (inductive_of_constructor cstr) env + +let is_type_in_type env r = + let open Names.GlobRef in + match r with + | VarRef _id -> false + | ConstRef c -> type_in_type_constant c env + | IndRef ind -> type_in_type_ind ind env + | ConstructRef cstr -> type_in_type_ind (inductive_of_constructor cstr) env + (*spiwack: the following functions assemble the pieces of the retroknowledge note that the "consistent" register function is available in the module Safetyping, Environ only synchronizes the proactive and the reactive parts*) diff --git a/kernel/environ.mli b/kernel/environ.mli index 43bfe7c2fb..0255581749 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -211,6 +211,12 @@ val constant_value_and_type : env -> Constant.t puniverses -> polymorphic *) val constant_context : env -> Constant.t -> Univ.AUContext.t +(** Returns the body of the constant if it has any, and the polymorphic context + it lives in. For monomorphic constant, the latter is empty, and for + polymorphic constants, the term contains De Bruijn universe variables that + need to be instantiated. *) +val body_of_constant_body : env -> constant_body -> (Constr.constr * Univ.AUContext.t) option + (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) @@ -320,6 +326,8 @@ val apply_to_hyp : named_context_val -> variable -> val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declaration) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val val is_polymorphic : env -> Names.GlobRef.t -> bool +val is_template_polymorphic : env -> GlobRef.t -> bool +val is_type_in_type : env -> GlobRef.t -> bool open Retroknowledge (** functions manipulating the retroknowledge diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 12f9592ab7..779e05ee0c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -194,6 +194,10 @@ let set_engagement c senv = let set_typing_flags c senv = { senv with env = Environ.set_typing_flags c senv.env } +let set_share_reduction b senv = + let flags = Environ.typing_flags senv.env in + set_typing_flags { flags with share_reduction = b } senv + (** Check that the engagement [c] expected by a library matches the current (initial) one *) let check_engagement env expected_impredicative_set = @@ -1190,7 +1194,7 @@ loaded by side-effect once and for all (like it is done in OCaml). Would this be correct with respect to undo's and stuff ? *) -let set_strategy e k l = { e with env = +let set_strategy k l e = { e with env = (Environ.set_oracle e.env (Conv_oracle.set_strategy (Environ.oracle e.env) k l)) } diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 26fa91adbd..443b5cfd73 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -137,6 +137,7 @@ val add_constraints : (** Setting the type theory flavor *) val set_engagement : Declarations.engagement -> safe_transformer0 val set_typing_flags : Declarations.typing_flags -> safe_transformer0 +val set_share_reduction : bool -> safe_transformer0 (** {6 Interactive module functions } *) @@ -217,4 +218,4 @@ val register : val register_inline : Constant.t -> safe_transformer0 val set_strategy : - safe_environment -> Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_environment + Names.Constant.t Names.tableKey -> Conv_oracle.level -> safe_transformer0 diff --git a/library/global.ml b/library/global.ml index 3781ff3230..bfea6d3dea 100644 --- a/library/global.ml +++ b/library/global.ml @@ -128,19 +128,7 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) let opaque_tables () = Environ.opaque_tables (env ()) -let instantiate cb c = - let open Declarations in - match cb.const_universes with - | Monomorphic_const _ -> c, Univ.AUContext.empty - | Polymorphic_const ctx -> c, ctx - -let body_of_constant_body cb = - let open Declarations in - let otab = opaque_tables () in - match cb.const_body with - | Undef _ -> None - | Def c -> Some (instantiate cb (Mod_subst.force_constr c)) - | OpaqueDef o -> Some (instantiate cb (Opaqueproof.force_proof otab o)) +let body_of_constant_body ce = body_of_constant_body (env ()) ce let body_of_constant cst = body_of_constant_body (lookup_constant cst) @@ -165,8 +153,6 @@ let import c u d = globalize (Safe_typing.import c u d) let env_of_context hyps = reset_with_named_context hyps (env()) -open Globnames - let constr_of_global_in_context = Typeops.constr_of_global_in_context let type_of_global_in_context = Typeops.type_of_global_in_context @@ -175,21 +161,9 @@ let universes_of_global gr = let is_polymorphic r = Environ.is_polymorphic (env()) r -let is_template_polymorphic r = - let env = env() in - match r with - | VarRef id -> false - | ConstRef c -> false - | IndRef ind -> Environ.template_polymorphic_ind ind env - | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env - -let is_type_in_type r = - let env = env() in - match r with - | VarRef id -> false - | ConstRef c -> Environ.type_in_type_constant c env - | IndRef ind -> Environ.type_in_type_ind ind env - | ConstructRef cstr -> Environ.type_in_type_ind (inductive_of_constructor cstr) env +let is_template_polymorphic r = is_template_polymorphic (env ()) r + +let is_type_in_type r = is_type_in_type (env ()) r let current_modpath () = Safe_typing.current_modpath (safe_env ()) @@ -208,11 +182,7 @@ let register field value = let register_inline c = globalize0 (Safe_typing.register_inline c) let set_strategy k l = - GlobalSafeEnv.set_safe_env (Safe_typing.set_strategy (safe_env ()) k l) - -let set_reduction_sharing b = - let env = safe_env () in - let flags = Environ.typing_flags (Safe_typing.env_of_safe_env env) in - let flags = { flags with Declarations.share_reduction = b } in - let env = Safe_typing.set_typing_flags flags env in - GlobalSafeEnv.set_safe_env env + globalize0 (Safe_typing.set_strategy k l) + +let set_share_reduction b = + globalize0 (Safe_typing.set_share_reduction b) diff --git a/library/global.mli b/library/global.mli index 42a8005a4f..762a3f006d 100644 --- a/library/global.mli +++ b/library/global.mli @@ -150,7 +150,9 @@ val register_inline : Constant.t -> unit val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit -val set_reduction_sharing : bool -> unit +(** {6 Conversion settings } *) + +val set_share_reduction : bool -> unit (* Modifies the global state, registering new universes *) diff --git a/library/libobject.ml b/library/libobject.ml index ea19fbb90b..43934304c2 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -71,7 +71,7 @@ type dynamic_object_declaration = { let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t let cache_tab = - (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) + (Hashtbl.create 223 : (string,dynamic_object_declaration) Hashtbl.t) let declare_object_full odecl = let na = odecl.object_name in diff --git a/library/nametab.ml b/library/nametab.ml index 06ace373c3..029d850504 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -74,6 +74,8 @@ module type NAMETREE = sig val user_name : qualid -> t -> user_name val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid val find_prefixes : qualid -> t -> elt list + (** Matches a prefix of [qualid], useful for completion *) + val match_prefixes : qualid -> t -> elt list end module Make (U : UserName) (E : EqualityType) : NAMETREE @@ -259,9 +261,19 @@ let find_prefixes qid tab = search_prefixes (Id.Map.find id tab) (DirPath.repr dir) with Not_found -> [] -end - +let match_prefixes = + let cprefix x y = CString.(compare x (sub y 0 (min (length x) (length y)))) in + fun qid tab -> + try + let (dir,id) = repr_qualid qid in + let id_prefix = cprefix Id.(to_string id) in + let matches = Id.Map.filter_range (fun x -> id_prefix Id.(to_string x)) tab in + let matches = Id.Map.mapi (fun _key tab -> search_prefixes tab (DirPath.repr dir)) matches in + (* Coq's flatten is "magical", so this is not so bad perf-wise *) + CList.flatten @@ Id.Map.(fold (fun _ r l -> r :: l) matches []) + with Not_found -> [] +end (* Global name tables *************************************************) @@ -447,6 +459,10 @@ let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab let locate_extended_all_modtype qid = MPTab.find_prefixes qid !the_modtypetab +(* Completion *) +let completion_canditates qualid = + ExtRefTab.match_prefixes qualid !the_ccitab + (* Derived functions *) let locate_constant qid = diff --git a/library/nametab.mli b/library/nametab.mli index 1c3322bfb1..1e479b200b 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -118,6 +118,12 @@ val locate_extended_all : qualid -> extended_global_reference list val locate_extended_all_dir : qualid -> global_dir_reference list val locate_extended_all_modtype : qualid -> ModPath.t list +(** Experimental completion support, API is _unstable_ *) +val completion_canditates : qualid -> extended_global_reference list +(** [completion_canditates qualid] will return the list of global + references that have [qualid] as a prefix. UI usually will want to + compose this with [shortest_qualid_of_global] *) + (** Mapping a full path to a global reference *) val global_of_path : full_path -> GlobRef.t @@ -211,6 +217,7 @@ module type NAMETREE = sig val user_name : qualid -> t -> user_name val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid val find_prefixes : qualid -> t -> elt list + val match_prefixes : qualid -> t -> elt list end module Make (U : UserName) (E : EqualityType) : diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index b660865e8b..05a65e4cd8 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -855,9 +855,9 @@ END TACTIC EXTEND transparent_abstract | [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } | [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } + Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } END (* ********************************************************************* *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index fcbcfae115..5e2a9af7e5 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -44,6 +44,7 @@ type glob_sign = Genintern.glob_sign = { (* ltac variables and the subset of vars introduced by Intro/Let/... *) genv : Environ.env; extra : Genintern.Store.t; + intern_sign : Genintern.intern_variable_status; } let make_empty_glob_sign () = Genintern.empty_glob_sign (Global.env ()) @@ -209,7 +210,7 @@ let intern_binding_name ist x = and if a term w/o ltac vars, check the name is indeed quantified *) x -let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c = +let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra; intern_sign} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in let ltacvars = { @@ -218,7 +219,7 @@ let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} c = ltac_extra = extra; } in let c' = - warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env Evd.(from_env env)) c + warn (Constrintern.intern_core scope ~pattern_mode ~ltacvars env Evd.(from_env env) intern_sign) c in (c',if !strict_check then None else Some c) diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index a9f2d76e30..178f6af71d 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -21,6 +21,7 @@ type glob_sign = Genintern.glob_sign = { ltacvars : Id.Set.t; genv : Environ.env; extra : Genintern.Store.t; + intern_sign : Genintern.intern_variable_status; } val make_empty_glob_sign : unit -> glob_sign diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 528d7de549..2a046a3e65 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -686,7 +686,7 @@ let interp_may_eval f ist env sigma = function | ConstrContext ({loc;v=s},c) -> (try let (sigma,ic) = f ist env sigma c in - let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in + let ctxt = try_interp_ltac_var coerce_to_constr_context ist (Some (env, sigma)) (make ?loc s) in let ctxt = EConstr.Unsafe.to_constr ctxt in let ic = EConstr.Unsafe.to_constr ic in let c = subst_meta [Constr_matching.special_meta,ic] ctxt in @@ -1078,7 +1078,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with push_trace(None,call) ist >>= fun trace -> Profile_ltac.do_profile "eval_tactic:TacAbstract" trace (catch_error_tac trace begin - Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT + Proofview.Goal.enter begin fun gl -> Abstract.tclABSTRACT (Option.map (interp_ident ist (pf_env gl) (project gl)) ido) (interp_tactic ist t) end end) | TacThen (t1,t) -> diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index e15c00f7dc..e21c2fda85 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -104,6 +104,7 @@ let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env ev Evar_kinds.qm_name=na; }) in let evd, v = Evarutil.new_evar env !evdref ~src c in + let evd = Evd.set_obligation_evar evd (fst (destEvar evd v)) in evdref := evd; v diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index dd38ec6f64..96213af9c6 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -83,7 +83,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) (** Refresh the types of evars under template polymorphic references *) let rec refresh_term_evars ~onevars ~top t = match EConstr.kind !evdref t with - | App (f, args) when is_template_polymorphic env !evdref f -> + | App (f, args) when Termops.is_template_polymorphic_ind env !evdref f -> let pos = get_polymorphic_positions !evdref f in refresh_polymorphic_positions args pos; t | App (f, args) when top && isEvar !evdref f -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 55817f1b76..cba1533da5 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -457,6 +457,15 @@ let pretype_sort ?loc sigma = function let new_type_evar env sigma loc = new_type_evar env sigma ~src:(Loc.tag ?loc Evar_kinds.InternalHole) +let mark_obligation_evar sigma k evc = + if Flags.is_program_mode () then + match k with + | Evar_kinds.QuestionMark _ + | Evar_kinds.ImplicitArg (_, _, false) -> + Evd.set_obligation_evar sigma (fst (destEvar sigma evc)) + | _ -> sigma + else sigma + (* [pretype tycon env sigma lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [sigma] and *) (* the type constraint tycon *) @@ -510,15 +519,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma | Some ty -> sigma, ty | None -> new_type_evar env sigma loc in let sigma, uj_val = new_evar env sigma ~src:(loc,k) ~naming ty in - let sigma = - if Flags.is_program_mode () then - match k with - | Evar_kinds.QuestionMark _ - | Evar_kinds.ImplicitArg (_, _, false) -> - Evd.set_obligation_evar sigma (fst (destEvar sigma uj_val)) - | _ -> sigma - else sigma - in + let sigma = mark_obligation_evar sigma k uj_val in sigma, { uj_val; uj_type = ty } | GHole (k, _naming, Some arg) -> @@ -691,7 +692,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma let sigma, resj = match EConstr.kind sigma resj.uj_val with | App (f,args) -> - if is_template_polymorphic !!env sigma f then + if Termops.is_template_polymorphic_ind !!env sigma f then (* Special case for inductive type applications that must be refreshed right away. *) let c = mkApp (f, args) in @@ -1039,6 +1040,7 @@ and pretype_type k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get | None -> let sigma, s = new_sort_variable univ_flexible_alg sigma in let sigma, utj_val = new_evar env sigma ~src:(loc, knd) ~naming (mkSort s) in + let sigma = mark_obligation_evar sigma knd utj_val in sigma, { utj_val; utj_type = s}) | _ -> let sigma, j = pretype k0 resolve_tc empty_tycon env sigma c in diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 7e43c5e41d..62ad296ecb 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -130,7 +130,7 @@ let retype ?(polyprop=true) sigma = subst1 b (type_of (push_rel (LocalDef (name,b,c1)) env) c2) | Fix ((_,i),(_,tys,_)) -> tys.(i) | CoFix (i,(_,tys,_)) -> tys.(i) - | App(f,args) when is_template_polymorphic env sigma f -> + | App(f,args) when Termops.is_template_polymorphic_ind env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in strip_outer_cast sigma (subst_type env sigma t (Array.to_list args)) | App(f,args) -> @@ -156,7 +156,7 @@ let retype ?(polyprop=true) sigma = let dom = sort_of env t in let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in Typeops.sort_of_product env dom rang - | App(f,args) when is_template_polymorphic env sigma f -> + | App(f,args) when Termops.is_template_polymorphic_ind env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in sort_of_atomic_type env sigma t args | App(f,args) -> sort_of_atomic_type env sigma (type_of env f) args @@ -190,14 +190,14 @@ let get_sort_family_of ?(truncation_style=false) ?(polyprop=true) env sigma t = let s2 = sort_family_of (push_rel (LocalAssum (name,t)) env) c2 in if not (is_impredicative_set env) && s2 == InSet && sort_family_of env t == InType then InType else s2 - | App(f,args) when is_template_polymorphic env sigma f -> + | App(f,args) when Termops.is_template_polymorphic_ind env sigma f -> if truncation_style then InType else let t = type_of_global_reference_knowing_parameters env f args in Sorts.family (sort_of_atomic_type env sigma t args) | App(f,args) -> Sorts.family (sort_of_atomic_type env sigma (type_of env f) args) | Lambda _ | Fix _ | Construct _ -> retype_error NotAType - | Ind _ when truncation_style && is_template_polymorphic env sigma t -> InType + | Ind _ when truncation_style && Termops.is_template_polymorphic_ind env sigma t -> InType | _ -> Sorts.family (decomp_sort env sigma (type_of env t)) in sort_family_of env t diff --git a/proofs/clenv.ml b/proofs/clenv.ml index d01338fa95..b7ccd647b5 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -603,12 +603,20 @@ let make_evar_clause env sigma ?len t = in (** FIXME: do the renaming online *) let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in - let rec clrec (sigma, holes) n t = + let rec clrec (sigma, holes) inst n t = if n = 0 then (sigma, holes, t) else match EConstr.kind sigma t with - | Cast (t, _, _) -> clrec (sigma, holes) n t + | Cast (t, _, _) -> clrec (sigma, holes) inst n t | Prod (na, t1, t2) -> - let (sigma, ev) = new_evar env sigma ~typeclass_candidate:false t1 in + (** Share the evar instances as we are living in the same context *) + let inst, ctx, args, subst = match inst with + | None -> + (** Dummy type *) + let ctx, _, args, subst = push_rel_context_to_named_context env sigma mkProp in + Some (ctx, args, subst), ctx, args, subst + | Some (ctx, args, subst) -> inst, ctx, args, subst + in + let (sigma, ev) = new_evar_instance ~typeclass_candidate:false ctx sigma (csubst_subst subst t1) args in let dep = not (noccurn sigma 1 t2) in let hole = { hole_evar = ev; @@ -618,11 +626,11 @@ let make_evar_clause env sigma ?len t = hole_name = na; } in let t2 = if dep then subst1 ev t2 else t2 in - clrec (sigma, hole :: holes) (pred n) t2 - | LetIn (na, b, _, t) -> clrec (sigma, holes) n (subst1 b t) + clrec (sigma, hole :: holes) inst (pred n) t2 + | LetIn (na, b, _, t) -> clrec (sigma, holes) inst n (subst1 b t) | _ -> (sigma, holes, t) in - let (sigma, holes, t) = clrec (sigma, []) bound t in + let (sigma, holes, t) = clrec (sigma, []) None bound t in let holes = List.rev holes in let clause = { cl_concl = t; cl_holes = holes } in (sigma, clause) diff --git a/proofs/logic.ml b/proofs/logic.ml index b8612cd2c0..4d5711c195 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -384,7 +384,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env sigma (EConstr.of_constr f) then + if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f) then let ty = (* Template polymorphism of definitions and inductive types *) let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in @@ -447,7 +447,7 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env sigma (EConstr.of_constr f) + if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f) then let l' = meta_free_prefix sigma l in (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f) diff --git a/stm/stm.ml b/stm/stm.ml index 19915b1600..b731678f6d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2028,7 +2028,7 @@ end = struct (* {{{ *) str"g=" ++ int (Evar.repr gid) ++ spc () ++ str"t=" ++ (Printer.pr_constr_env env sigma pt) ++ spc () ++ str"uc=" ++ Termops.pr_evar_universe_context uc)); - (if abstract then Tactics.tclABSTRACT None else (fun x -> x)) + (if abstract then Abstract.tclABSTRACT None else (fun x -> x)) (V82.tactic (Refiner.tclPUSHEVARUNIVCONTEXT uc) <*> Tactics.exact_no_check (EConstr.of_constr pt)) | None -> diff --git a/tactics/abstract.ml b/tactics/abstract.ml new file mode 100644 index 0000000000..2b4d9a7adf --- /dev/null +++ b/tactics/abstract.ml @@ -0,0 +1,195 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +module CVars = Vars + +open Util +open Names +open Termops +open EConstr +open Decl_kinds +open Evarutil + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + +(* tactical to save as name a subproof such that the generalisation of + the current goal, abstracted with respect to the local signature, + is solved by tac *) + +(** d1 is the section variable in the global context, d2 in the goal context *) +let interpretable_as_section_decl env evd d1 d2 = + let open Context.Named.Declaration in + let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env !sigma c1 c2 with + | None -> false + | Some cstr -> + try ignore (Evd.add_universe_constraints !sigma cstr); true + with UState.UniversesDiffer -> false + in + match d2, d1 with + | LocalDef _, LocalAssum _ -> false + | LocalDef (_,b1,t1), LocalDef (_,b2,t2) -> + e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2 + | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type d2) + +let rec decompose len c t accu = + let open Constr in + let open Context.Rel.Declaration in + if len = 0 then (c, t, accu) + else match kind c, kind t with + | Lambda (na, u, c), Prod (_, _, t) -> + decompose (pred len) c t (LocalAssum (na, u) :: accu) + | LetIn (na, b, u, c), LetIn (_, _, _, t) -> + decompose (pred len) c t (LocalDef (na, b, u) :: accu) + | _ -> assert false + +let rec shrink ctx sign c t accu = + let open Constr in + let open CVars in + match ctx, sign with + | [], [] -> (c, t, accu) + | p :: ctx, decl :: sign -> + if noccurn 1 c && noccurn 1 t then + let c = subst1 mkProp c in + let t = subst1 mkProp t in + shrink ctx sign c t accu + else + let c = Term.mkLambda_or_LetIn p c in + let t = Term.mkProd_or_LetIn p t in + let accu = if RelDecl.is_local_assum p + then mkVar (NamedDecl.get_id decl) :: accu + else accu + in + shrink ctx sign c t accu +| _ -> assert false + +let shrink_entry sign const = + let open Entries in + let typ = match const.const_entry_type with + | None -> assert false + | Some t -> t + in + (** The body has been forced by the call to [build_constant_by_tactic] *) + let () = assert (Future.is_over const.const_entry_body) in + let ((body, uctx), eff) = Future.force const.const_entry_body in + let (body, typ, ctx) = decompose (List.length sign) body typ [] in + let (body, typ, args) = shrink ctx sign body typ [] in + let const = { const with + const_entry_body = Future.from_val ((body, uctx), eff); + const_entry_type = Some typ; + } in + (const, args) + +let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = + let open Tacticals.New in + let open Tacmach.New in + let open Proofview.Notations in + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let current_sign = Global.named_context_val () + and global_sign = Proofview.Goal.hyps gl in + let evdref = ref sigma in + let sign,secsign = + List.fold_right + (fun d (s1,s2) -> + let id = NamedDecl.get_id d in + if mem_named_context_val id current_sign && + interpretable_as_section_decl env evdref (lookup_named_val id current_sign) d + then (s1,push_named_context_val d s2) + else (Context.Named.add d s1,s2)) + global_sign (Context.Named.empty, Environ.empty_named_context_val) in + let id = Namegen.next_global_ident_away id (pf_ids_set_of_hyps gl) in + let concl = match goal_type with + | None -> Proofview.Goal.concl gl + | Some ty -> ty in + let concl = it_mkNamedProd_or_LetIn concl sign in + let concl = + try flush_and_check_evars !evdref concl + with Uninstantiated_evar _ -> + CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials.") in + + let evd, ctx, concl = + (* FIXME: should be done only if the tactic succeeds *) + let evd = Evd.minimize_universes !evdref in + let ctx = Evd.universe_context_set evd in + evd, ctx, Evarutil.nf_evars_universes evd concl + in + let concl = EConstr.of_constr concl in + let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in + let ectx = Evd.evar_universe_context evd in + let (const, safe, ectx) = + try Pfedit.build_constant_by_tactic ~goal_kind:gk id ectx secsign concl solve_tac + with Logic_monad.TacticFailure e as src -> + (* if the tactic [tac] fails, it reports a [TacticFailure e], + which is an error irrelevant to the proof system (in fact it + means that [e] comes from [tac] failing to yield enough + success). Hence it reraises [e]. *) + let (_, info) = CErrors.push src in + iraise (e, info) + in + let const, args = shrink_entry sign const in + let args = List.map EConstr.of_constr args in + let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in + let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in + let cst () = + (** do not compute the implicit arguments, it may be costly *) + let () = Impargs.make_implicit_args false in + (** ppedrot: seems legit to have abstracted subproofs as local*) + Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl + in + let cst = Impargs.with_implicit_protection cst () in + let inst = match const.Entries.const_entry_universes with + | Entries.Monomorphic_const_entry _ -> EInstance.empty + | Entries.Polymorphic_const_entry ctx -> + (** We mimick what the kernel does, that is ensuring that no additional + constraints appear in the body of polymorphic constants. Ideally this + should be enforced statically. *) + let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in + let () = assert (Univ.ContextSet.is_empty body_uctx) in + EInstance.make (Univ.UContext.instance ctx) + in + let lem = mkConstU (cst, inst) in + let evd = Evd.set_universe_context evd ectx in + let open Safe_typing in + let eff = private_con_of_con (Global.safe_env ()) cst in + let effs = concat_private eff + Entries.(snd (Future.force const.const_entry_body)) in + let solve = + Proofview.tclEFFECTS effs <*> + tacK lem args + in + let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) tac + end + +let abstract_subproof ~opaque id gk tac = + cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> Tactics.exact_no_check (applist (lem, args))) + +let anon_id = Id.of_string "anonymous" + +let name_op_to_name name_op object_kind suffix = + let open Proof_global in + let default_gk = (Global, false, object_kind) in + let name, gk = match Proof_global.V82.get_current_initial_conclusions () with + | (id, (_, gk)) -> Some id, gk + | exception NoCurrentProof -> None, default_gk + in + match name_op with + | Some s -> s, gk + | None -> + let name = Option.default anon_id name in + Nameops.add_suffix name suffix, gk + +let tclABSTRACT ?(opaque=true) name_op tac = + let s, gk = if opaque + then name_op_to_name name_op (Proof Theorem) "_subproof" + else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in + abstract_subproof ~opaque s gk tac diff --git a/tactics/abstract.mli b/tactics/abstract.mli new file mode 100644 index 0000000000..7fb671fbf8 --- /dev/null +++ b/tactics/abstract.mli @@ -0,0 +1,16 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open EConstr + +val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic + +val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a6a104ccca..25f9bc5576 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -module CVars = Vars - open Pp open CErrors open Util @@ -36,7 +34,6 @@ open Refiner open Tacticals open Hipattern open Coqlib -open Decl_kinds open Evarutil open Indrec open Pretype_errors @@ -4884,179 +4881,6 @@ let transitivity t = transitivity_gen (Some t) let intros_transitivity n = Tacticals.New.tclTHEN intros (transitivity_gen n) -(* tactical to save as name a subproof such that the generalisation of - the current goal, abstracted with respect to the local signature, - is solved by tac *) - -(** d1 is the section variable in the global context, d2 in the goal context *) -let interpretable_as_section_decl env evd d1 d2 = - let open Context.Named.Declaration in - let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env !sigma c1 c2 with - | None -> false - | Some cstr -> - try ignore (Evd.add_universe_constraints !sigma cstr); true - with UniversesDiffer -> false - in - match d2, d1 with - | LocalDef _, LocalAssum _ -> false - | LocalDef (_,b1,t1), LocalDef (_,b2,t2) -> - e_eq_constr_univs evd b1 b2 && e_eq_constr_univs evd t1 t2 - | LocalAssum (_,t1), d2 -> e_eq_constr_univs evd t1 (NamedDecl.get_type d2) - -let rec decompose len c t accu = - let open Context.Rel.Declaration in - if len = 0 then (c, t, accu) - else match Constr.kind c, Constr.kind t with - | Lambda (na, u, c), Prod (_, _, t) -> - decompose (pred len) c t (LocalAssum (na, u) :: accu) - | LetIn (na, b, u, c), LetIn (_, _, _, t) -> - decompose (pred len) c t (LocalDef (na, b, u) :: accu) - | _ -> assert false - -let rec shrink ctx sign c t accu = - let open Constr in - let open CVars in - match ctx, sign with - | [], [] -> (c, t, accu) - | p :: ctx, decl :: sign -> - if noccurn 1 c && noccurn 1 t then - let c = subst1 mkProp c in - let t = subst1 mkProp t in - shrink ctx sign c t accu - else - let c = Term.mkLambda_or_LetIn p c in - let t = Term.mkProd_or_LetIn p t in - let accu = if RelDecl.is_local_assum p - then mkVar (NamedDecl.get_id decl) :: accu - else accu - in - shrink ctx sign c t accu -| _ -> assert false - -let shrink_entry sign const = - let open Entries in - let typ = match const.const_entry_type with - | None -> assert false - | Some t -> t - in - (** The body has been forced by the call to [build_constant_by_tactic] *) - let () = assert (Future.is_over const.const_entry_body) in - let ((body, uctx), eff) = Future.force const.const_entry_body in - let (body, typ, ctx) = decompose (List.length sign) body typ [] in - let (body, typ, args) = shrink ctx sign body typ [] in - let const = { const with - const_entry_body = Future.from_val ((body, uctx), eff); - const_entry_type = Some typ; - } in - (const, args) - -let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = - let open Tacticals.New in - let open Tacmach.New in - let open Proofview.Notations in - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let current_sign = Global.named_context_val () - and global_sign = Proofview.Goal.hyps gl in - let evdref = ref sigma in - let sign,secsign = - List.fold_right - (fun d (s1,s2) -> - let id = NamedDecl.get_id d in - if mem_named_context_val id current_sign && - interpretable_as_section_decl env evdref (lookup_named_val id current_sign) d - then (s1,push_named_context_val d s2) - else (Context.Named.add d s1,s2)) - global_sign (Context.Named.empty, empty_named_context_val) in - let id = next_global_ident_away id (pf_ids_set_of_hyps gl) in - let concl = match goal_type with - | None -> Proofview.Goal.concl gl - | Some ty -> ty in - let concl = it_mkNamedProd_or_LetIn concl sign in - let concl = - try flush_and_check_evars !evdref concl - with Uninstantiated_evar _ -> - error "\"abstract\" cannot handle existentials." in - - let evd, ctx, concl = - (* FIXME: should be done only if the tactic succeeds *) - let evd = Evd.minimize_universes !evdref in - let ctx = Evd.universe_context_set evd in - evd, ctx, Evarutil.nf_evars_universes evd concl - in - let concl = EConstr.of_constr concl in - let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in - let ectx = Evd.evar_universe_context evd in - let (const, safe, ectx) = - try Pfedit.build_constant_by_tactic ~goal_kind:gk id ectx secsign concl solve_tac - with Logic_monad.TacticFailure e as src -> - (* if the tactic [tac] fails, it reports a [TacticFailure e], - which is an error irrelevant to the proof system (in fact it - means that [e] comes from [tac] failing to yield enough - success). Hence it reraises [e]. *) - let (_, info) = CErrors.push src in - iraise (e, info) - in - let const, args = shrink_entry sign const in - let args = List.map EConstr.of_constr args in - let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in - let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in - let cst () = - (** do not compute the implicit arguments, it may be costly *) - let () = Impargs.make_implicit_args false in - (** ppedrot: seems legit to have abstracted subproofs as local*) - Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl - in - let cst = Impargs.with_implicit_protection cst () in - let inst = match const.Entries.const_entry_universes with - | Entries.Monomorphic_const_entry _ -> EInstance.empty - | Entries.Polymorphic_const_entry ctx -> - (** We mimick what the kernel does, that is ensuring that no additional - constraints appear in the body of polymorphic constants. Ideally this - should be enforced statically. *) - let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in - let () = assert (Univ.ContextSet.is_empty body_uctx) in - EInstance.make (Univ.UContext.instance ctx) - in - let lem = mkConstU (cst, inst) in - let evd = Evd.set_universe_context evd ectx in - let open Safe_typing in - let eff = private_con_of_con (Global.safe_env ()) cst in - let effs = concat_private eff - Entries.(snd (Future.force const.const_entry_body)) in - let solve = - Proofview.tclEFFECTS effs <*> - tacK lem args - in - let tac = if not safe then Proofview.mark_as_unsafe <*> solve else solve in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) tac - end - -let abstract_subproof ~opaque id gk tac = - cache_term_by_tactic_then ~opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args))) - -let anon_id = Id.of_string "anonymous" - -let name_op_to_name name_op object_kind suffix = - let open Proof_global in - let default_gk = (Global, false, object_kind) in - let name, gk = match Proof_global.V82.get_current_initial_conclusions () with - | (id, (_, gk)) -> Some id, gk - | exception NoCurrentProof -> None, default_gk - in - match name_op with - | Some s -> s, gk - | None -> - let name = Option.default anon_id name in - add_suffix name suffix, gk - -let tclABSTRACT ?(opaque=true) name_op tac = - let s, gk = if opaque - then name_op_to_name name_op (Proof Theorem) "_subproof" - else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in - abstract_subproof ~opaque s gk tac - let constr_eq ~strict x y = let fail = Tacticals.New.tclFAIL 0 (str "Not equal") in let fail_universes = Tacticals.New.tclFAIL 0 (str "Not equal (due to universes)") in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 24c12ffd82..7efadb2c28 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -418,10 +418,6 @@ val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic -val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic - -val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic - val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> unit Proofview.tactic val specialize_eqs : Id.t -> unit Proofview.tactic diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index f54ad86a3f..5afec74fae 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -7,6 +7,7 @@ Ind_tables Eqschemes Elimschemes Tactics +Abstract Elim Equality Contradiction diff --git a/test-suite/bugs/closed/bug_3468.v b/test-suite/bugs/closed/bug_3468.v new file mode 100644 index 0000000000..6ff394bca6 --- /dev/null +++ b/test-suite/bugs/closed/bug_3468.v @@ -0,0 +1,29 @@ +(* Checking that unrelated terms requiring some scope do not affect + the interpretation of tactic-in-term. The "Check" was failing with: + The term "Set" has type "Type" while it is expected to have type + "nat". *) + +Notation bar2 a b := (let __ := ltac:(exact I) in (a + b)%type) (only parsing). +Check bar2 (Set + Set) Set. + +(* Taking into account scopes in notations containing tactic-in-term *) + +Declare Scope foo_scope. +Delimit Scope foo_scope with foo. +Notation "x ~~" := (x) (at level 0, only parsing) : foo_scope. +Notation bar x := (x%foo) (only parsing). +Notation baz x := ltac:(exact x%foo) (only parsing). +Check bar (O ~~). +Check baz (O ~~). (* Was failing *) + +(* This was reported as bug #8706 *) + +Declare Scope my_scope. +Notation "@ a" := a%nat (at level 100, only parsing) : my_scope. +Delimit Scope my_scope with my. + +Notation "& b" := ltac:(exact (b)%my) (at level 100, only parsing): my_scope. +Definition test := (& (@4))%my. + +(* Check inconsistent scopes *) +Fail Notation bar3 a := (let __ := ltac:(exact a%nat) in a%bool) (only parsing). diff --git a/test-suite/bugs/closed/bug_8755.v b/test-suite/bugs/closed/bug_8755.v new file mode 100644 index 0000000000..cd5aee4fa0 --- /dev/null +++ b/test-suite/bugs/closed/bug_8755.v @@ -0,0 +1,6 @@ + +Lemma f : Type. +Fail let i := ident:(i) in +let t := context i [Type] in +idtac. +Abort. diff --git a/test-suite/coqchk/bug_8876.v b/test-suite/coqchk/bug_8876.v new file mode 100644 index 0000000000..2d20511a04 --- /dev/null +++ b/test-suite/coqchk/bug_8876.v @@ -0,0 +1,19 @@ +(* -*- coq-prog-args: ("-noinit"); -*- *) +Require Import Coq.Init.Notations. + +Notation "x -> y" := (forall _ : x, y). + +Inductive eq {A:Type} (a:A) : A -> Prop := eq_refl : eq a a. + +Set Universe Polymorphism. +Set Polymorphic Inductive Cumulativity. +Set Printing Universes. + +(* Constructors for an inductive with indices *) +Module WithIndex. + Inductive foo@{i} : (Prop -> Prop) -> Prop := mkfoo: foo (fun x => x). + + Monomorphic Universes i j. + Monomorphic Constraint i < j. + Definition bar : eq mkfoo@{i} mkfoo@{j} := eq_refl _. +End WithIndex. diff --git a/test-suite/coqchk/bug_8881.v b/test-suite/coqchk/bug_8881.v new file mode 100644 index 0000000000..dfc209b318 --- /dev/null +++ b/test-suite/coqchk/bug_8881.v @@ -0,0 +1,23 @@ + +(* Check use of equivalence on inductive types (bug #1242) *) + +Module Type ASIG. + Inductive t : Set := a | b : t. + Definition f := fun x => match x with a => true | b => false end. +End ASIG. + +Module Type BSIG. + Declare Module A : ASIG. + Definition f := fun x => match x with A.a => true | A.b => false end. +End BSIG. + +Module C (A : ASIG) (B : BSIG with Module A:=A). + + (* Check equivalence is considered in "case_info" *) + Lemma test : forall x, A.f x = B.f x. + Proof. + intro x. unfold B.f, A.f. + destruct x; reflexivity. + Qed. + +End C. diff --git a/test-suite/misc/poly-capture-global-univs/.gitignore b/test-suite/misc/poly-capture-global-univs/.gitignore index f5a6d22b8e..2a6a6bc68d 100644 --- a/test-suite/misc/poly-capture-global-univs/.gitignore +++ b/test-suite/misc/poly-capture-global-univs/.gitignore @@ -1 +1,2 @@ /Makefile* +/src/evil.ml diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index cef7d1a702..46784d1897 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -1,5 +1,7 @@ [< 0 > + < 1 > * < 2 >] : nat +[< b > + < b > * < 2 >] + : nat [<< # 0 >>] : option nat [1 {f 1}] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 9738ce5a5e..6bdbf1bed5 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -10,6 +10,10 @@ Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4). Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10). Check [ < 0 > + < 1 > * < 2 >]. +Axiom a : nat. +Notation b := a. +Check [ < b > + < a > * < 2 >]. + Declare Custom Entry anotherconstr. Notation "[ x ]" := x (x custom myconstr at level 6). diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index cea8af3f05..fe8ef1f0e0 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -178,7 +178,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let sigma, h_e_term = Evarutil.new_evar env sigma ~src:(Loc.tag @@ Evar_kinds.QuestionMark { Evar_kinds.default_question_mark with Evar_kinds.qm_obligation=Evar_kinds.Define false; - }) wf_proof in + }) wf_proof in + let sigma = Evd.set_obligation_evar sigma (fst (destEvar sigma h_e_term)) in sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |]) in let sigma, def = Typing.solve_evars env sigma def in diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 844caf5a3e..ad6ca3a84e 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -391,11 +391,10 @@ let explain_unexpected_type env sigma actual_type expected_type = str "where" ++ spc () ++ prexp ++ str " was expected." let explain_not_product env sigma c = - let c = EConstr.to_constr sigma c in - let pr = pr_lconstr_env env sigma c in + let pr = pr_econstr_env env sigma c in str "The type of this term is a product" ++ spc () ++ str "while it is expected to be" ++ - (if Constr.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." + (if EConstr.isType sigma c then str " a sort" else (brk(1,1) ++ pr)) ++ str "." (* TODO: use the names *) (* (co)fixpoints *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index fbf552e649..5c1384fba7 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -37,13 +37,11 @@ let succfix (depth, fixrels) = let check_evars env evm = Evar.Map.iter - (fun key evi -> - let (loc,k) = evar_source key evm in - match k with - | Evar_kinds.QuestionMark _ - | Evar_kinds.ImplicitArg (_,_,false) -> () - | _ -> - Pretype_errors.error_unsolvable_implicit ?loc env evm key None) + (fun key evi -> + if Evd.is_obligation_evar evm key then () + else + let (loc,k) = evar_source key evm in + Pretype_errors.error_unsolvable_implicit ?loc env evm key None) (Evd.undefined_map evm) type oblinfo = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1190d73258..5eace14cbf 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1536,7 +1536,7 @@ let _ = optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction); - optwrite = (fun b -> Global.set_reduction_sharing b) } + optwrite = Global.set_share_reduction } let _ = declare_bool_option |