diff options
72 files changed, 830 insertions, 514 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/indtypes.ml b/checker/indtypes.ml index 50e65ef587..f6c510ee1c 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -531,10 +531,11 @@ let check_positivity env_ar mind params nrecp inds = Array.mapi (fun j t -> (Mrec(mind,j),t)) (Rtree.mk_rec_calls ntypes) in let lra_ind = List.rev (Array.to_list rc) in let lparams = rel_context_length params in + let ra_env = + List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in + let env_ar_par = push_rel_context params env_ar in let check_one i mip = - let ra_env = - List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in - let ienv = (env_ar, 1+lparams, ntypes, ra_env) in + let ienv = (env_ar_par, 1+lparams, ntypes, ra_env) in check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc in let irecargs = Array.mapi check_one inds in 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/cArray.ml b/clib/cArray.ml index 9644834381..c3a693ff16 100644 --- a/clib/cArray.ml +++ b/clib/cArray.ml @@ -35,6 +35,8 @@ sig val fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a val fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c + val fold_right3 : + ('a -> 'b -> 'c -> 'd -> 'd) -> 'a array -> 'b array -> 'c array -> 'd -> 'd val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val fold_left3 : @@ -252,6 +254,16 @@ let fold_left2_i f a v1 v2 = if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2_i"; fold a 0 +let fold_right3 f v1 v2 v3 a = + let lv1 = Array.length v1 in + let rec fold a n = + if n=0 then a + else + let k = n-1 in + fold (f (uget v1 k) (uget v2 k) (uget v3 k) a) k in + if Array.length v2 <> lv1 || Array.length v3 <> lv1 then invalid_arg "Array.fold_right3"; + fold a lv1 + let fold_left3 f a v1 v2 v3 = let lv1 = Array.length v1 in let rec fold a n = diff --git a/clib/cArray.mli b/clib/cArray.mli index e65a56d15e..21479d2b45 100644 --- a/clib/cArray.mli +++ b/clib/cArray.mli @@ -58,6 +58,8 @@ sig val fold_left_i : (int -> 'a -> 'b -> 'a) -> 'a -> 'b array -> 'a val fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a array -> 'b array -> 'c -> 'c + val fold_right3 : + ('a -> 'b -> 'c -> 'd -> 'd) -> 'a array -> 'b array -> 'c array -> 'd -> 'd val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b array -> 'c array -> 'a val fold_left3 : 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/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/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/environ.ml b/kernel/environ.ml index 3b7e3ae544..f61dd0c101 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -350,9 +350,6 @@ let map_universes f env = { env with env_stratification = { s with env_universes = f s.env_universes } } -let set_universes env u = - { env with env_stratification = { env.env_stratification with env_universes = u } } - let add_constraints c env = if Univ.Constraint.is_empty c then env else map_universes (UGraph.merge_constraints c) env @@ -405,19 +402,12 @@ let add_constant_key kn cb linkinfo env = let add_constant kn cb env = add_constant_key kn cb no_link_info env -let constraints_of cb u = - match cb.const_universes with - | Monomorphic_const _ -> Univ.Constraint.empty - | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx - (* constant_type gives the type of a constant *) let constant_type env (kn,u) = let cb = lookup_constant kn env in - match cb.const_universes with - | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty - | Polymorphic_const _ctx -> - let csts = constraints_of cb u in - (subst_instance_constr u cb.const_type, csts) + let uctx = Declareops.constant_polymorphic_context cb in + let csts = Univ.AUContext.instantiate u uctx in + (subst_instance_constr u cb.const_type, csts) type const_evaluation_result = NoBody | Opaque @@ -425,20 +415,24 @@ exception NotEvaluableConst of const_evaluation_result let constant_value_and_type env (kn, u) = let cb = lookup_constant kn env in - if Declareops.constant_is_polymorphic cb then - let cst = constraints_of cb u in - let b' = match cb.const_body with - | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body)) - | OpaqueDef _ -> None - | Undef _ -> None - in - b', subst_instance_constr u cb.const_type, cst - else - let b' = match cb.const_body with - | Def l_body -> Some (Mod_subst.force_constr l_body) - | OpaqueDef _ -> None - | Undef _ -> None - in b', cb.const_type, Univ.Constraint.empty + let uctx = Declareops.constant_polymorphic_context cb in + let cst = Univ.AUContext.instantiate u uctx in + let b' = match cb.const_body with + | Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body)) + | OpaqueDef _ -> None + | Undef _ -> None + in + b', subst_instance_constr u cb.const_type, cst + +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 @@ -447,9 +441,7 @@ let constant_value_and_type env (kn, u) = (* constant_type gives the type of a constant *) let constant_type_in env (kn,u) = let cb = lookup_constant kn env in - if Declareops.constant_is_polymorphic cb then - subst_instance_constr u cb.const_type - else cb.const_type + subst_instance_constr u cb.const_type let constant_value_in env (kn,u) = let cb = lookup_constant kn env in @@ -694,6 +686,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..c285f907fc 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -155,11 +155,6 @@ val named_body : variable -> env -> constr option val fold_named_context : (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a -val set_universes : env -> UGraph.t -> env -(** This is used to update universes during a proof for the sake of - evar map-unaware functions, eg [Typing] calling - [Typeops.check_hyps_inclusion]. *) - (** Recurrence on [named_context] starting from younger decl *) val fold_named_context_reverse : ('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a @@ -211,6 +206,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 +321,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/reduction.ml b/kernel/reduction.ml index 18697d07e5..5515ff9767 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -68,7 +68,7 @@ type lft_constr_stack_elt = Zlapp of (lift * fconstr) array | Zlproj of Projection.Repr.t * lift | Zlfix of (lift * fconstr) * lft_constr_stack - | Zlcase of case_info * lift * fconstr * fconstr array + | Zlcase of case_info * lift * constr * constr array * fconstr subs and lft_constr_stack = lft_constr_stack_elt list let rec zlapp v = function @@ -102,7 +102,7 @@ let pure_stack lfts stk = let (lfx,pa) = pure_rec l a in (l, Zlfix((lfx,fx),pa)::pstk) | (ZcaseT(ci,p,br,e),(l,pstk)) -> - (l,Zlcase(ci,l,mk_clos e p,Array.map (mk_clos e) br)::pstk)) + (l,Zlcase(ci,l,p,br,e)::pstk)) in snd (pure_rec lfts stk) @@ -288,31 +288,13 @@ let conv_table_key infos k1 k2 cuniv = | RelKey n, RelKey n' when Int.equal n n' -> cuniv | _ -> raise NotConvertible -let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = - let rec cmp_rec pstk1 pstk2 cuniv = - match (pstk1,pstk2) with - | (z1::s1, z2::s2) -> - let cu1 = cmp_rec s1 s2 cuniv in - (match (z1,z2) with - | (Zlapp a1,Zlapp a2) -> - Array.fold_right2 f a1 a2 cu1 - | (Zlproj (c1,_l1),Zlproj (c2,_l2)) -> - if not (Projection.Repr.equal c1 c2) then - raise NotConvertible - else cu1 - | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> - let cu2 = f fx1 fx2 cu1 in - cmp_rec a1 a2 cu2 - | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) -> - if not (fmind ci1.ci_ind ci2.ci_ind) then - raise NotConvertible; - let cu2 = f (l1,p1) (l2,p2) cu1 in - Array.fold_right2 (fun c1 c2 -> f (l1,c1) (l2,c2)) br1 br2 cu2 - | _ -> assert false) - | _ -> cuniv in - if compare_stack_shape stk1 stk2 then - cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv - else raise NotConvertible +exception IrregularPatternShape + +let rec skip_pattern n c = + if Int.equal n 0 then c + else match kind c with + | Lambda (_, _, c) -> skip_pattern (pred n) c + | _ -> raise IrregularPatternShape type conv_tab = { cnv_inf : clos_infos; @@ -611,10 +593,31 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | FProd _ | FEvar _), _ -> raise NotConvertible and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = - compare_stacks - (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv) - (eq_ind) - lft1 stk1 lft2 stk2 cuniv + let f (l1, t1) (l2, t2) cuniv = ccnv CONV l2r infos l1 l2 t1 t2 cuniv in + let rec cmp_rec pstk1 pstk2 cuniv = + match (pstk1,pstk2) with + | (z1::s1, z2::s2) -> + let cu1 = cmp_rec s1 s2 cuniv in + (match (z1,z2) with + | (Zlapp a1,Zlapp a2) -> + Array.fold_right2 f a1 a2 cu1 + | (Zlproj (c1,_l1),Zlproj (c2,_l2)) -> + if not (Projection.Repr.equal c1 c2) then + raise NotConvertible + else cu1 + | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> + let cu2 = f fx1 fx2 cu1 in + cmp_rec a1 a2 cu2 + | (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) -> + if not (eq_ind ci1.ci_ind ci2.ci_ind) then + raise NotConvertible; + let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in + convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2 + | _ -> assert false) + | _ -> cuniv in + if compare_stack_shape stk1 stk2 then + cmp_rec (pure_stack lft1 stk1) (pure_stack lft2 stk2) cuniv + else raise NotConvertible and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = let lv1 = Array.length v1 in @@ -629,6 +632,22 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv = fold 0 cuniv else raise NotConvertible +and convert_branches l2r infos ci e1 e2 lft1 lft2 br1 br2 cuniv = + (** Skip comparison of the pattern types. We know that the two terms are + living in a common type, thus this check is useless. *) + let fold n c1 c2 cuniv = match skip_pattern n c1, skip_pattern n c2 with + | (c1, c2) -> + let lft1 = el_liftn n lft1 in + let lft2 = el_liftn n lft2 in + let e1 = subs_liftn n e1 in + let e2 = subs_liftn n e2 in + ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv + | exception IrregularPatternShape -> + (** Might happen due to a shape invariant that is not enforced *) + ccnv CONV l2r infos lft1 lft2 (mk_clos e1 c1) (mk_clos e2 c2) cuniv + in + Array.fold_right3 fold ci.ci_cstr_nargs br1 br2 cuniv + let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 = let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in let infos = create_clos_infos ~evars reds env in 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/kernel/typeops.ml b/kernel/typeops.ml index 1bb2d3c79c..c8fd83c8a9 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -91,7 +91,8 @@ let type_of_variable env id = (* Checks if a context of variables can be instantiated by the variables of the current env. Order does not have to be checked assuming that all names are distinct *) -let check_hyps_inclusion env f c sign = +let check_hyps_inclusion env ?evars f c sign = + let conv env a b = conv env ?evars a b in Context.Named.fold_outside (fun d1 () -> let open Context.Named.Declaration in diff --git a/kernel/typeops.mli b/kernel/typeops.mli index d24002065b..4193324136 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -116,4 +116,5 @@ val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t (** {6 Miscellaneous. } *) (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit +val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) -> + ('a -> constr) -> 'a -> Constr.named_context -> unit 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 5828494454..2a046a3e65 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -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/arguments_renaming.mli b/pretyping/arguments_renaming.mli index 6a776dc961..6d1b6eefd4 100644 --- a/pretyping/arguments_renaming.mli +++ b/pretyping/arguments_renaming.mli @@ -17,6 +17,8 @@ val rename_arguments : bool -> GlobRef.t -> Name.t list -> unit (** [Not_found] is raised if no names are defined for [r] *) val arguments_names : GlobRef.t -> Name.t list +val rename_type : types -> GlobRef.t -> types + val rename_type_of_constant : env -> pconstant -> types val rename_type_of_inductive : env -> pinductive -> types val rename_type_of_constructor : env -> pconstructor -> types 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/pretyping/typing.ml b/pretyping/typing.ml index dc3f042431..b5729d7574 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -218,9 +218,6 @@ let judge_of_cast env sigma cj k tj = sigma, { uj_val = mkCast (cj.uj_val, k, expected_type); uj_type = expected_type } -let enrich_env env sigma = - set_universes env @@ Evd.universes sigma - let check_fix env sigma pfix = let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in let (idx, (ids, cs, ts)) = pfix in @@ -277,6 +274,38 @@ let judge_of_letin env name defj typj j = { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ; uj_type = subst1 defj.uj_val j.uj_type } +let check_hyps_inclusion env sigma f x hyps = + let evars = Evarutil.safe_evar_value sigma, Evd.universes sigma in + let f x = EConstr.Unsafe.to_constr (f x) in + Typeops.check_hyps_inclusion env ~evars f x hyps + +let type_of_constant env sigma (c,u) = + let open Declarations in + let cb = Environ.lookup_constant c env in + let () = check_hyps_inclusion env sigma mkConstU (c,u) cb.const_hyps in + let u = EInstance.kind sigma u in + let ty, csts = Environ.constant_type env (c,u) in + let sigma = Evd.add_constraints sigma csts in + sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstRef c))) + +let type_of_inductive env sigma (ind,u) = + let open Declarations in + let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in + let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in + let u = EInstance.kind sigma u in + let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in + let sigma = Evd.add_constraints sigma csts in + sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.IndRef ind))) + +let type_of_constructor env sigma ((ind,_ as ctor),u) = + let open Declarations in + let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in + let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in + let u = EInstance.kind sigma u in + let ty, csts = Inductive.constrained_type_of_constructor (ctor,u) specif in + let sigma = Evd.add_constraints sigma csts in + sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor))) + (* cstr must be in n.f. w.r.t. evars and execute returns a judgement where both the term and type are in n.f. *) let rec execute env sigma cstr = @@ -297,17 +326,17 @@ let rec execute env sigma cstr = | Var id -> sigma, judge_of_variable env id - | Const (c, u) -> - let u = EInstance.kind sigma u in - sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constant env (c, u))) + | Const c -> + let sigma, ty = type_of_constant env sigma c in + sigma, make_judge cstr ty - | Ind (ind, u) -> - let u = EInstance.kind sigma u in - sigma, make_judge cstr (EConstr.of_constr (rename_type_of_inductive env (ind, u))) + | Ind ind -> + let sigma, ty = type_of_inductive env sigma ind in + sigma, make_judge cstr ty - | Construct (cstruct, u) -> - let u = EInstance.kind sigma u in - sigma, make_judge cstr (EConstr.of_constr (rename_type_of_constructor env (cstruct, u))) + | Construct ctor -> + let sigma, ty = type_of_constructor env sigma ctor in + sigma, make_judge cstr ty | Case (ci,p,c,lf) -> let sigma, cj = execute env sigma c in @@ -391,7 +420,6 @@ and execute_recdef env sigma (names,lar,vdef) = and execute_array env = Array.fold_left_map (execute env) let check env sigma c t = - let env = enrich_env env sigma in let sigma, j = execute env sigma c in match Evarconv.cumul env sigma j.uj_type t with | None -> @@ -401,14 +429,12 @@ let check env sigma c t = (* Type of a constr *) let unsafe_type_of env sigma c = - let env = enrich_env env sigma in let sigma, j = execute env sigma c in j.uj_type (* Sort of a type *) let sort_of env sigma c = - let env = enrich_env env sigma in let sigma, j = execute env sigma c in let sigma, a = type_judgment env sigma j in sigma, a.utj_type @@ -416,7 +442,6 @@ let sort_of env sigma c = (* Try to solve the existential variables by typing *) let type_of ?(refresh=false) env sigma c = - let env = enrich_env env sigma in let sigma, j = execute env sigma c in (* side-effect on evdref *) if refresh then @@ -424,7 +449,6 @@ let type_of ?(refresh=false) env sigma c = else sigma, j.uj_type let solve_evars env sigma c = - let env = enrich_env env sigma in let sigma, j = execute env sigma c in (* side-effect on evdref *) sigma, nf_evar sigma j.uj_val 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..5cead11a5c 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 @@ -4100,12 +4097,15 @@ let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info = let guess_elim isrec dep s hyp0 gl = let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in let (mind, u), _ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in - let evd, elimc = - if isrec && not (is_nonrec mind) then find_ind_eliminator mind s gl + let env = Tacmach.New.pf_env gl in + let sigma = Tacmach.New.project gl in + let sigma, elimc = + if isrec && not (is_nonrec mind) + then + let gr = lookup_eliminator mind s in + Evd.fresh_global env sigma gr else - let env = Tacmach.New.pf_env gl in - let sigma = Tacmach.New.project gl in - let u = EInstance.kind (Tacmach.New.project gl) u in + let u = EInstance.kind sigma u in if dep then let (sigma, ind) = build_case_analysis_scheme env sigma (mind, u) true s in let ind = EConstr.of_constr ind in @@ -4115,8 +4115,8 @@ let guess_elim isrec dep s hyp0 gl = let ind = EConstr.of_constr ind in (sigma, ind) in - let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in - evd, ((elimc, NoBindings), elimt), mkIndU (mind, u) + let elimt = Typing.unsafe_type_of env sigma elimc in + sigma, ((elimc, NoBindings), elimt), mkIndU (mind, u) let given_elim hyp0 (elimc,lbind as e) gl = let sigma = Tacmach.New.project gl in @@ -4884,179 +4884,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/coqchk/bug_8655.v b/test-suite/coqchk/bug_8655.v new file mode 100644 index 0000000000..06d08b2082 --- /dev/null +++ b/test-suite/coqchk/bug_8655.v @@ -0,0 +1 @@ +Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2). 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/success/Inductive.v b/test-suite/success/Inductive.v index f07c0191f1..c2130995fc 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -1,7 +1,5 @@ (* Test des definitions inductives imbriquees *) -Require Import List. - Inductive X : Set := cons1 : list X -> X. 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 |