diff options
78 files changed, 581 insertions, 545 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8b43d975a..b47494d3a 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -40,6 +40,11 @@ before_script: - if [ ! "(" -d .opamcache ")" ]; then mv ~/.opam .opamcache; else mv ~/.opam ~/.opam-old; fi - ln -s $(readlink -f .opamcache) ~/.opam + # the default repo in this docker image is a local directory + # at the time of 4aaeb8abf it lagged behind the official + # repository such that camlp5 7.01 was not available + - opam repository set-url default https://opam.ocaml.org + - opam update - opam switch ${COMPILER} - eval $(opam config env) - opam config list diff --git a/.travis.yml b/.travis.yml index 3cd7fdf5e..9c7ad553f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -37,34 +37,33 @@ env: - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" - TEST_TARGET="validate" TW="travis_wait" - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait" - - TEST_TARGET="ci-bignums" - - TEST_TARGET="ci-color" - - TEST_TARGET="ci-compcert" + - TEST_TARGET="ci-bignums TIMED=1" + - TEST_TARGET="ci-color TIMED=1" + - TEST_TARGET="ci-compcert TIMED=1" - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph" - - TEST_TARGET="ci-coquelicot" - - TEST_TARGET="ci-geocoq" - - TEST_TARGET="ci-fiat-crypto" - - TEST_TARGET="ci-fiat-parsers" - - TEST_TARGET="ci-flocq" - - TEST_TARGET="ci-formal-topology" - - TEST_TARGET="ci-hott" - - TEST_TARGET="ci-iris-coq" - - TEST_TARGET="ci-math-classes" - - TEST_TARGET="ci-math-comp" - - TEST_TARGET="ci-sf" - - TEST_TARGET="ci-unimath" - - TEST_TARGET="ci-vst" + - TEST_TARGET="ci-coquelicot TIMED=1" + - TEST_TARGET="ci-geocoq TIMED=1" + - TEST_TARGET="ci-fiat-crypto TIMED=1" + - TEST_TARGET="ci-fiat-parsers TIMED=1" + - TEST_TARGET="ci-flocq TIMED=1" + - TEST_TARGET="ci-formal-topology TIMED=1" + - TEST_TARGET="ci-hott TIMED=1" + - TEST_TARGET="ci-iris-coq TIMED=1" + - TEST_TARGET="ci-math-classes TIMED=1" + - TEST_TARGET="ci-math-comp TIMED=1" + - TEST_TARGET="ci-sf TIMED=1" + - TEST_TARGET="ci-unimath TIMED=1" + - TEST_TARGET="ci-vst TIMED=1" # Not ready yet for 8.7 - # - TEST_TARGET="ci-cpdt" - # - TEST_TARGET="ci-metacoq" - # - TEST_TARGET="ci-tlc" + # - TEST_TARGET="ci-cpdt TIMED=1" + # - TEST_TARGET="ci-metacoq TIMED=1" + # - TEST_TARGET="ci-tlc TIMED=1" matrix: allow_failures: - env: TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph" - - env: TEST_TARGET="ci-geocoq" - - env: TEST_TARGET="ci-fiat-parsers" + - env: TEST_TARGET="ci-geocoq TIMED=1" include: # Full Coq test-suite with two compilers diff --git a/API/API.mli b/API/API.mli index b00862535..3ae8ac64c 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1185,8 +1185,6 @@ sig | RegularArity of 'a | TemplateArity of 'b - type constant_type = (Constr.types, Context.Rel.t * template_arity) declaration_arity - type constant_universes = | Monomorphic_const of Univ.universe_context | Polymorphic_const of Univ.abstract_universe_context @@ -1208,7 +1206,7 @@ sig type constant_body = { const_hyps : Context.Named.t; const_body : constant_def; - const_type : constant_type; + const_type : Term.types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; const_proj : projection_body option; @@ -1345,6 +1343,9 @@ sig type inline = int option type 'a proof_output = Constr.t Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation + type constant_universes_entry = + | Monomorphic_const_entry of Univ.universe_context + | Polymorphic_const_entry of Univ.universe_context type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) @@ -1352,8 +1353,7 @@ sig (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : Constr.types option; - const_entry_polymorphic : bool; - const_entry_universes : Univ.UContext.t; + const_entry_universes : constant_universes_entry; const_entry_opaque : bool; const_entry_inline_code : bool } type parameter_entry = Context.Named.t option * bool * Constr.types Univ.in_universe_context * inline @@ -1584,7 +1584,6 @@ end module Typeops : sig val infer_type : Environ.env -> Term.types -> Environ.unsafe_type_judgment - val type_of_constant_type : Environ.env -> Declarations.constant_type -> Term.types val type_of_constant_in : Environ.env -> Term.pconstant -> Term.types end @@ -4626,6 +4625,7 @@ sig val get_current_proof_name : unit -> Names.Id.t [@@ocaml.deprecated "use Proof_global.get_current_proof_name"] + val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types end module Clenv : @@ -5401,6 +5401,8 @@ sig val pp_hints_path : hints_path -> Pp.t val glob_hints_path : Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen + val run_hint : hint -> + ((raw_hint * Clenv.clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic val typeclasses_db : hint_db_name val add_hints_init : (unit -> unit) -> unit val create_hint_db : bool -> hint_db_name -> Names.transparent_state -> bool -> unit @@ -42,9 +42,9 @@ # to communicate between make sub-calls (in Win32, 8kb max per env variable, # 32kb total) -# !! Before using FIND_VCS_CLAUSE, please read how you should in the !! -# !! FIND_VCS_CLAUSE section of dev/doc/build-system.dev.txt !! -FIND_VCS_CLAUSE:='(' \ +# !! Before using FIND_SKIP_DIRS, please read how you should in the !! +# !! FIND_SKIP_DIRS section of dev/doc/build-system.dev.txt !! +FIND_SKIP_DIRS:='(' \ -name '{arch}' -o \ -name '.svn' -o \ -name '_darcs' -o \ @@ -55,25 +55,23 @@ FIND_VCS_CLAUSE:='(' \ -name '_build' -o \ -name '_build_ci' -o \ -name 'coq-makefile' -o \ - -name '.opamcache' \ + -name '.opamcache' -o \ + -name '.coq-native' \ ')' -prune -o define find - $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -print | sed 's|^\./||') + $(shell find . $(FIND_SKIP_DIRS) '(' -name $(1) ')' -print | sed 's|^\./||') endef define findindir - $(shell find $(1) $(FIND_VCS_CLAUSE) '(' -name $(2) ')' -print | sed 's|^\./||') -endef - -define findx - $(shell find . $(FIND_VCS_CLAUSE) '(' -name $(1) ')' -exec $(2) {} \; | sed 's|^\./||') + $(shell find $(1) $(FIND_SKIP_DIRS) '(' -name $(2) ')' -print | sed 's|^\./||') endef ## Files in the source tree LEXFILES := $(call find, '*.mll') -export MLLIBFILES := $(call find, '*.mllib') $(call find, '*.mlpack') +export MLLIBFILES := $(call find, '*.mllib') +export MLPACKFILES := $(call find, '*.mlpack') export ML4FILES := $(call find, '*.ml4') export CFILES := $(call findindir, 'kernel/byterun', '*.c') @@ -97,11 +95,7 @@ export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) ## More complex file lists -define diff - $(strip $(foreach f, $(1), $(if $(filter $(f),$(2)),,$f))) -endef - -export MLSTATICFILES := $(call diff, $(EXISTINGML), $(GENMLFILES) $(GENML4FILES)) +export MLSTATICFILES := $(filter-out $(GENMLFILES) $(GENML4FILES), $(EXISTINGML)) export MLIFILES := $(sort $(GENMLIFILES) $(EXISTINGMLI)) include Makefile.common @@ -139,6 +133,36 @@ Then, you may want to consider whether you want to restore the autosaves) #run. endif +# Check that every compiled file around has a known source file. +# This should help preventing weird compilation failures caused by leftover +# compiled files after deleting or moving some source files. + +ifndef ACCEPT_ALIEN_VO +EXISTINGVO:=$(call find, '*.vo') +KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) +ALIENVO:=$(filter-out $(KNOWNVO),$(EXISTINGVO)) +ifdef ALIENVO +$(error Leftover compiled Coq files without known sources: $(ALIENVO); \ +remove them first, for instance via 'make voclean' \ +(or skip this check via 'make ACCEPT_ALIEN_VO=1')) +endif +endif + +ifndef ACCEPT_ALIEN_OBJ +EXISTINGOBJS:=$(call find, '*.cm[oxia]' -o -name '*.cmxa') +KNOWNML:=$(EXISTINGML) $(GENMLFILES) $(GENML4FILES) $(MLPACKFILES:.mlpack=.ml) \ + $(patsubst %.mlp,%.ml,$(wildcard grammar/*.mlp)) +KNOWNOBJS:=$(KNOWNML:.ml=.cmo) $(KNOWNML:.ml=.cmx) $(KNOWNML:.ml=.cmi) \ + $(MLIFILES:.mli=.cmi) \ + $(MLLIBFILES:.mllib=.cma) $(MLLIBFILES:.mllib=.cmxa) grammar/grammar.cma +ALIENOBJS:=$(filter-out $(KNOWNOBJS),$(EXISTINGOBJS)) +ifdef ALIENOBJS +$(error Leftover compiled OCaml files without known sources: $(ALIENOBJS); \ +remove them first, for instance via 'make clean' \ +(or skip this check via 'make ACCEPT_ALIEN_OBJ=1')) +endif +endif + # Apart from clean and tags, everything will be done in a sub-call to make # on Makefile.build. This way, we avoid doing here the -include of .d : # since they trigger some compilations, we do not want them for a mere clean. @@ -218,7 +242,7 @@ archclean: clean-ide optclean voclean optclean: rm -f $(COQTOPEXE) $(COQMKTOP) $(CHICKEN) rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT) - find . -name '*.cmx' -o -name '*.cmxs' -o -name '*.cmxa' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f + find . -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f clean-ide: rm -f $(COQIDECMO) $(COQIDECMX) $(COQIDECMO:.cmo=.cmi) $(COQIDEBYTE) $(COQIDE) @@ -231,7 +255,7 @@ ml4clean: rm -f $(GENML4FILES) depclean: - find . $(FIND_VCS_CLAUSE) '(' -name '*.d' ')' -print | xargs rm -f + find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -print | xargs rm -f cacheclean: find theories plugins test-suite -name '.*.aux' -delete diff --git a/Makefile.build b/Makefile.build index e3316df91..7961092fa 100644 --- a/Makefile.build +++ b/Makefile.build @@ -151,7 +151,7 @@ endif # coqdep_boot (for the .v.d files) or grammar.cma (for .ml4 -> .ml -> .ml.d). DEPENDENCIES := \ - $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(CFILES) $(VFILES)) + $(addsuffix .d, $(MLFILES) $(MLIFILES) $(MLLIBFILES) $(MLPACKFILES) $(CFILES) $(VFILES)) -include $(DEPENDENCIES) diff --git a/Makefile.ci b/Makefile.ci index c8bc09fdc..1b09905cc 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -24,4 +24,9 @@ CI_TARGETS=ci-all \ # Generic rule, we use make to easy travis integraton with mixed rules $(CI_TARGETS): ci-%: - +./dev/ci/ci-$*.sh + rm -f ci-$*.ok + +(./dev/ci/ci-$*.sh 2>&1 && touch ci-$*.ok) | tee time-of-build.log + echo 'Aggregating timing log...' && echo -en 'travis_fold:start:coq.test.timing\\r' + python ./tools/make-one-time-file.py time-of-build.log + echo -en 'travis_fold:end:coq.test.timing\\r' + rm ci-$*.ok # must not be -f; we're checking to see that it exists diff --git a/checker/cic.mli b/checker/cic.mli index 14fa7c774..59dd5bc4d 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -182,8 +182,6 @@ type ('a, 'b) declaration_arity = | RegularArity of 'a | TemplateArity of 'b -type constant_type = (constr, rel_context * template_arity) declaration_arity - (** Inlining level of parameters at functor applications. This is ignored by the checker. *) @@ -226,7 +224,7 @@ type typing_flags = { type constant_body = { const_hyps : section_context; (** New: younger hyp at top *) const_body : constant_def; - const_type : constant_type; + const_type : constr; const_body_code : to_patch_substituted; const_universes : constant_universes; const_proj : projection_body option; diff --git a/checker/declarations.ml b/checker/declarations.ml index 2eefe4781..093d999a3 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -515,12 +515,6 @@ let subst_rel_declaration sub = let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) -let subst_template_cst_arity sub (ctx,s as arity) = - let ctx' = subst_rel_context sub ctx in - if ctx==ctx' then arity else (ctx',s) - -let subst_arity sub s = subst_decl_arity subst_mps subst_template_cst_arity sub s - let constant_is_polymorphic cb = match cb.const_universes with | Monomorphic_const _ -> false @@ -531,7 +525,7 @@ let constant_is_polymorphic cb = let subst_const_body sub cb = { cb with const_body = subst_constant_def sub cb.const_body; - const_type = subst_arity sub cb.const_type } + const_type = subst_mps sub cb.const_type } let subst_regular_ind_arity sub s = diff --git a/checker/environ.ml b/checker/environ.ml index d3f393c65..a0818012c 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -124,12 +124,6 @@ let constraints_of cb u = | Monomorphic_const _ -> Univ.Constraint.empty | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx -let map_regular_arity f = function - | RegularArity a as ar -> - let a' = f a in - if a' == a then ar else RegularArity a' - | TemplateArity _ -> assert false - (* constant_type gives the type of a constant *) let constant_type env (kn,u) = let cb = lookup_constant kn env in @@ -137,7 +131,7 @@ let constant_type env (kn,u) = | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty | Polymorphic_const ctx -> let csts = constraints_of cb u in - (map_regular_arity (subst_instance_constr u) cb.const_type, csts) + (subst_instance_constr u cb.const_type, csts) exception NotEvaluableConst of const_evaluation_result diff --git a/checker/environ.mli b/checker/environ.mli index 754c295d2..8e8d0fd49 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -46,7 +46,7 @@ val check_constraints : Univ.constraints -> env -> bool (* Constants *) val lookup_constant : constant -> env -> Cic.constant_body val add_constant : constant -> Cic.constant_body -> env -> env -val constant_type : env -> constant puniverses -> constant_type Univ.constrained +val constant_type : env -> constant puniverses -> constr Univ.constrained type const_evaluation_result = NoBody | Opaque | IsProj exception NotEvaluableConst of const_evaluation_result val constant_value : env -> constant puniverses -> constr diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 4948f6008..b6816dd48 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -35,15 +35,11 @@ let check_constant_declaration env kn cb = push_context ~strict:false ctx env in let envty, ty = - match cb.const_type with - RegularArity ty -> - let ty', cu = refresh_arity ty in - let envty = push_context_set cu env' in - let _ = infer_type envty ty' in envty, ty - | TemplateArity(ctxt,par) -> - let _ = check_ctxt env' ctxt in - check_polymorphic_arity env' ctxt par; - env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt + let ty = cb.const_type in + let ty', cu = refresh_arity ty in + let envty = push_context_set cu env' in + let _ = infer_type envty ty' in + envty, ty in let () = match body_of_constant cb with diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 3097c3a0b..68a467bea 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -294,8 +294,8 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let cb1 = subst_const_body subst1 cb1 in let cb2 = subst_const_body subst2 cb2 in (*Start by checking types*) - let typ1 = Typeops.type_of_constant_type env cb1.const_type in - let typ2 = Typeops.type_of_constant_type env cb2.const_type in + let typ1 = cb1.const_type in + let typ2 = cb2.const_type in check_type env typ1 typ2; (* Now we check the bodies: - A transparent constant can only be implemented by a compatible diff --git a/checker/typeops.ml b/checker/typeops.ml index f2cbfec7d..9f39d588a 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -69,35 +69,16 @@ let judge_of_relative env n = (* Type of constants *) - -let type_of_constant_type_knowing_parameters env t paramtyps = - match t with - | RegularArity t -> t - | TemplateArity (sign,ar) -> - let ctx = List.rev sign in - let ctx,s = instantiate_universes env ctx ar paramtyps in - mkArity (List.rev ctx,s) - -let type_of_constant_knowing_parameters env cst paramtyps = - let ty, cu = constant_type env cst in - type_of_constant_type_knowing_parameters env ty paramtyps, cu - -let type_of_constant_type env t = - type_of_constant_type_knowing_parameters env t [||] - -let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp = +let judge_of_constant env (kn,u as cst) = let _cb = try lookup_constant kn env with Not_found -> failwith ("Cannot find constant: "^Constant.to_string kn) in - let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in + let ty, cu = constant_type env cst in let () = check_constraints cu env in ty -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] - (* Type of an application. *) let judge_of_apply env (f,funj) argjv = @@ -276,8 +257,6 @@ let rec execute env cstr = match f with | Ind ind -> judge_of_inductive_knowing_parameters env ind jl - | Const cst -> - judge_of_constant_knowing_parameters env cst jl | _ -> (* No template polymorphism *) execute env f diff --git a/checker/typeops.mli b/checker/typeops.mli index 2be461b05..d9f2915a3 100644 --- a/checker/typeops.mli +++ b/checker/typeops.mli @@ -18,6 +18,3 @@ val infer_type : env -> constr -> sorts val check_ctxt : env -> rel_context -> env val check_polymorphic_arity : env -> rel_context -> template_arity -> unit - -val type_of_constant_type : env -> constant_type -> constr - diff --git a/checker/values.ml b/checker/values.ml index e13430e98..c95c3f1b2 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 67309b04a86b247431fd3e580ecbb50d checker/cic.mli +MD5 c802f941f368bedd96e931cda0559d67 checker/cic.mli *) @@ -201,9 +201,6 @@ let v_engagement = v_impredicative_set let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] -let v_cst_type = - v_sum "constant_type" 0 [|[|v_constr|]; [|v_pair v_rctxt v_pol_arity|]|] - let v_cst_def = v_sum "constant_def" 0 [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] @@ -222,7 +219,7 @@ let v_const_univs = v_sum "constant_universes" 0 [|[|v_context|]; [|v_abs_contex let v_cb = v_tuple "constant_body" [|v_section_ctxt; v_cst_def; - v_cst_type; + v_constr; Any; v_const_univs; Opt v_projbody; diff --git a/dev/base_include b/dev/base_include index bfbf6bb5d..79ecd73e0 100644 --- a/dev/base_include +++ b/dev/base_include @@ -194,8 +194,8 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;; let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; +let parse_tac = API.Pcoq.parse_string Ltac_plugin.Pltac.tactic;; (* build a term of type glob_constr without type-checking or resolution of implicit syntax *) diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 656030543..4b3b44875 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -85,8 +85,8 @@ ######################################################################## # fiat_parsers ######################################################################## -: ${fiat_parsers_CI_BRANCH:=trunk__API} -: ${fiat_parsers_CI_GITURL:=https://github.com/matejkosik/fiat.git} +: ${fiat_parsers_CI_BRANCH:=master} +: ${fiat_parsers_CI_GITURL:=https://github.com/mit-plv/fiat.git} ######################################################################## # fiat_crypto diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 693135a4c..1bf6e9a87 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -7,4 +7,4 @@ HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR} -( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make ) +( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} ) diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index fefcb0937..f3fc13e96 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -74,25 +74,25 @@ The Makefile is separated in several files : - Makefile.doc : specific rules for compiling the documentation. -FIND_VCS_CLAUSE +FIND_SKIP_DIRS --------------- -The recommended style of using FIND_VCS_CLAUSE is for example +The recommended style of using FIND_SKIP_DIRS is for example - find . $(FIND_VCS_CLAUSE) '(' -name '*.example' ')' -print - find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -or -name '*.foo' ')' -print + find . $(FIND_SKIP_DIRS) '(' -name '*.example' ')' -print + find . $(FIND_SKIP_DIRS) '(' -name '*.example' -or -name '*.foo' ')' -print 1) The parentheses even in the one-criteria case is so that if one adds other conditions, e.g. change the first example to the second - find . $(FIND_VCS_CLAUSE) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print + find . $(FIND_SKIP_DIRS) '(' -name '*.example' -and -not -name '*.bak.example' ')' -print one is not tempted to write - find . $(FIND_VCS_CLAUSE) -name '*.example' -and -not -name '*.bak.example' -print + find . $(FIND_SKIP_DIRS) -name '*.example' -and -not -name '*.bak.example' -print -because this will not necessarily work as expected; $(FIND_VCS_CLAUSE) +because this will not necessarily work as expected; $(FIND_SKIP_DIRS) ends with an -or, and how it combines with what comes later depends on operator precedence and all that. Much safer to override it with parentheses. @@ -105,13 +105,13 @@ As to the -print at the end, yes it is necessary. Here's why. You are used to write: find . -name '*.example' and it works fine. But the following will not: - find . $(FIND_VCS_CLAUSE) -name '*.example' -it will also list things directly matched by FIND_VCS_CLAUSE + find . $(FIND_SKIP_DIRS) -name '*.example' +it will also list things directly matched by FIND_SKIP_DIRS (directories we want to prune, in which we don't want to find anything). C'est subtil... Il y a effectivement un -print implicite ร la fin, qui fait que la commande habituelle sans print fonctionne bien, mais dรจs que l'on introduit d'autres commandes dans le lot (le --prune de FIND_VCS_CLAUSE), รงa se corse ร cause d'histoires de +-prune de FIND_SKIP_DIRS), รงa se corse ร cause d'histoires de parenthรจses du -print implicite par rapport au parenthรฉsage dans la forme recommandรฉe d'utilisation: diff --git a/dev/doc/naming-conventions.tex b/dev/doc/naming-conventions.tex index 349164948..337b9226d 100644 --- a/dev/doc/naming-conventions.tex +++ b/dev/doc/naming-conventions.tex @@ -267,7 +267,7 @@ If the conclusion is in the other way than listed below, add suffix {forall x y:D, op (op' x y) = op' x (op y)} \itemrule{Idempotency of binary operator {\op} on domain {\D}}{Dop\_idempotent} -{forall x:D, op x n = x} +{forall x:D, op x x = x} \itemrule{Idempotency of unary operator {\op} on domain {\D}}{Dop\_idempotent} {forall x:D, op (op x) = op x} diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex index 7ffe25225..b93ca2957 100644 --- a/doc/refman/AsyncProofs.tex +++ b/doc/refman/AsyncProofs.tex @@ -6,7 +6,7 @@ This chapter explains how proofs can be asynchronously processed by Coq. This feature improves the reactivity of the system when used in interactive -mode via CoqIDE. In addition to that, it allows Coq to take advantage of +mode via CoqIDE. In addition, it allows Coq to take advantage of parallel hardware when used as a batch compiler by decoupling the checking of statements and definitions from the construction and checking of proofs objects. @@ -22,7 +22,12 @@ For example, in interactive mode, some errors coming from the kernel of Coq are signaled late. The type of errors belonging to this category are universe inconsistencies. -Last, at the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously. +At the time of writing, only opaque proofs (ending with \texttt{Qed} or \texttt{Admitted}) can be processed asynchronously. + +Finally, asynchronous processing is disabled when running CoqIDE in Windows. The +current implementation of the feature is not stable on Windows. It can be +enabled, as described below at \ref{interactivecaveats}, though doing so is not +recommended. \section{Proof annotations} @@ -112,6 +117,7 @@ the kernel to check all the proof objects, one has to click the button with the gears. Only then are all the universe constraints checked. \subsubsection{Caveats} +\label{interactivecaveats} The number of worker processes can be increased by passing CoqIDE the \texttt{-async-proofs-j $n$} flag. Note that the memory consumption @@ -120,7 +126,8 @@ the master process. Also note that increasing the number of workers may reduce the reactivity of the master process to user commands. To disable this feature, one can pass the \texttt{-async-proofs off} flag to -CoqIDE. +CoqIDE. Conversely, on Windows, where the feature is disabled by default, +pass the \texttt{-async-proofs on} flag to enable it. Proofs that are known to take little time to process are not delegated to a worker process. The threshold can be configure with \texttt{-async-proofs-delegation-threshold}. Default is 0.03 seconds. diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 48f82f2d9..48048b7a0 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -591,5 +591,6 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/AdmitAxiom.v theories/Compat/Coq85.v theories/Compat/Coq86.v + theories/Compat/Coq87.v </dd> </dl> diff --git a/engine/termops.ml b/engine/termops.ml index 1aba2bbdd..cf7c0cc20 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1145,9 +1145,6 @@ let is_template_polymorphic env sigma f = | Ind (ind, u) -> if not (EConstr.EInstance.is_empty u) then false else Environ.template_polymorphic_ind ind env - | Const (cst, u) -> - if not (EConstr.EInstance.is_empty u) then false - else Environ.template_polymorphic_constant cst env | _ -> false let base_sort_cmp pb s0 s1 = diff --git a/engine/universes.ml b/engine/universes.ml index 08461a218..719af43ed 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -419,7 +419,7 @@ let type_of_reference env r = | VarRef id -> Environ.named_type id env, ContextSet.empty | ConstRef c -> let cb = Environ.lookup_constant c env in - let ty = Typeops.type_of_constant_type env cb.const_type in + let ty = cb.const_type in begin match cb.const_universes with | Monomorphic_const _ -> ty, ContextSet.empty diff --git a/ide/coq.ml b/ide/coq.ml index 8ecdf9caa..0fe831ab3 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -366,7 +366,14 @@ let bind_self_as f = (** This launches a fresh handle from its command line arguments. *) let spawn_handle args respawner feedback_processor = let prog = coqtop_path () in - let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: "on" :: "-ideslave" :: args) in + let async_default = + (* disable async processing by default in Windows *) + if List.mem Sys.os_type ["Win32"; "Cygwin"] then + "off" + else + "on" + in + let args = Array.of_list ("--xml_format=Ppcmds" :: "-async-proofs" :: async_default :: "-ideslave" :: args) in let env = match !Flags.ideslave_coqtop_flags with | None -> None diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f360fb192..c9fc3aa4f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -664,11 +664,11 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt -> let a,letins = snd (Option.get binderopt) in let e = make_letins letins (aux subst' infos c') in - let (loc,(na,bk,t)) = a in + let (_loc,(na,bk,t)) = a in CAst.make ?loc @@ GProd (na,bk,t,e) | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt -> let a,letins = snd (Option.get binderopt) in - let (loc,(na,bk,t)) = a in + let (_loc,(na,bk,t)) = a in CAst.make ?loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c')) (* Two special cases to keep binder name synchronous with BinderType *) | NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c') diff --git a/interp/declare.ml b/interp/declare.ml index 154793a32..70f422b51 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -63,8 +63,12 @@ let cache_variable ((sp,_),o) = impl, true, poly, ctx | SectionLocalDef (de) -> let univs = Global.push_named_def (id,de) in + let poly = match de.const_entry_universes with + | Monomorphic_const_entry _ -> false + | Polymorphic_const_entry _ -> true + in Explicit, de.const_entry_opaque, - de.const_entry_polymorphic, univs in + poly, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id impl poly ctx; Dischargedhypsmap.set_discharged_hyps sp []; @@ -98,14 +102,12 @@ let declare_variable id obj = (** Declaration of constants and parameters *) type constant_obj = { - cst_decl : global_declaration; + cst_decl : global_declaration option; + (** [None] when the declaration is a side-effect and has already been defined + in the global environment. *) cst_hyps : Dischargedhypsmap.discharged_hyps; cst_kind : logical_kind; cst_locl : bool; - mutable cst_exported : Safe_typing.exported_private_constant list; - (* mutable: to avoid change the libobject API, since cache_function - * does not return an updated object *) - mutable cst_was_seff : bool } type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind @@ -145,16 +147,15 @@ let cache_constant ((sp,kn), obj) = let id = basename sp in let _,dir,_ = repr_kn kn in let kn' = - if obj.cst_was_seff then begin - obj.cst_was_seff <- false; + match obj.cst_decl with + | None -> if Global.exists_objlabel (Label.of_id (basename sp)) then constant_of_kn kn else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp) ++ str".") - end else + | Some decl -> let () = check_exists sp in - let kn', exported = Global.add_constant dir id obj.cst_decl in - obj.cst_exported <- exported; - kn' in + Global.add_constant dir id decl + in assert (eq_constant kn' (constant_of_kn kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); let cst = Global.lookup_constant kn' in @@ -175,26 +176,20 @@ let discharge_constant ((sp, kn), obj) = let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in let abstract = (named_of_variable_context hyps, subst, uctx) in let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in - Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } + Some { obj with cst_hyps = new_hyps; cst_decl = Some new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = - ConstantEntry - (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) - let dummy_constant cst = { - cst_decl = dummy_constant_entry; + cst_decl = None; cst_hyps = []; cst_kind = cst.cst_kind; cst_locl = cst.cst_locl; - cst_exported = []; - cst_was_seff = cst.cst_was_seff; } let classify_constant cst = Substitute (dummy_constant cst) -let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) = - declare_object_full { (default_object "CONSTANT") with +let (inConstant : constant_obj -> obj) = + declare_object { (default_object "CONSTANT") with cache_function = cache_constant; load_function = load_constant; open_function = open_constant; @@ -205,31 +200,14 @@ let (inConstant, outConstant : (constant_obj -> obj) * (obj -> constant_obj)) = let declare_scheme = ref (fun _ _ -> assert false) let set_declare_scheme f = declare_scheme := f +let update_tables c = + declare_constant_implicits c; + Heads.declare_head (EvalConstRef c); + Notation.declare_ref_arguments_scope (ConstRef c) + let declare_constant_common id cst = - let update_tables c = -(* Printf.eprintf "tables: %s\n%!" (Names.Constant.to_string c); *) - declare_constant_implicits c; - Heads.declare_head (EvalConstRef c); - Notation.declare_ref_arguments_scope (ConstRef c) in let o = inConstant cst in let _, kn as oname = add_leaf id o in - List.iter (fun (c,ce,role) -> - (* handling of private_constants just exported *) - let o = inConstant { - cst_decl = ConstantEntry (false, ce); - cst_hyps = [] ; - cst_kind = IsProof Theorem; - cst_locl = false; - cst_exported = []; - cst_was_seff = true; } in - let id = Label.to_id (pi3 (Constant.repr3 c)) in - ignore(add_leaf id o); - update_tables c; - let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in - match role with - | Safe_typing.Subproof -> () - | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|]) - (outConstant o).cst_exported; pull_to_head oname; let c = Global.constant_of_delta_kn kn in update_tables c; @@ -237,34 +215,58 @@ let declare_constant_common id cst = let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body = + let univs = + if poly then Polymorphic_const_entry univs + else Monomorphic_const_entry univs + in { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff); const_entry_secctx = None; const_entry_type = types; - const_entry_polymorphic = poly; const_entry_universes = univs; const_entry_opaque = opaque; const_entry_feedback = None; const_entry_inline_code = inline} let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = - let export = (* We deal with side effects *) + let is_poly de = match de.const_entry_universes with + | Monomorphic_const_entry _ -> false + | Polymorphic_const_entry _ -> true + in + let in_section = Lib.sections_are_opened () in + let export, decl = (* We deal with side effects *) match cd with | DefinitionEntry de when export_seff || not de.const_entry_opaque || - de.const_entry_polymorphic -> - let bo = de.const_entry_body in - let _, seff = Future.force bo in - Safe_typing.empty_private_constants <> seff - | _ -> false + is_poly de -> + (** This globally defines the side-effects in the environment. We mark + exported constants as being side-effect not to redeclare them at + caching time. *) + let cd, export = Global.export_private_constants ~in_section cd in + export, ConstantEntry (PureEntry, cd) + | _ -> [], ConstantEntry (EffectEntry, cd) + in + let iter_eff (c, role) = + let o = inConstant { + cst_decl = None; + cst_hyps = [] ; + cst_kind = IsProof Theorem; + cst_locl = false; + } in + let id = Label.to_id (pi3 (Constant.repr3 c)) in + ignore(add_leaf id o); + update_tables c; + let () = if_xml (Hook.get f_xml_declare_constant) (InternalTacticRequest, c) in + match role with + | Safe_typing.Subproof -> () + | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|] in + let () = List.iter iter_eff export in let cst = { - cst_decl = ConstantEntry (export,cd); + cst_decl = Some decl; cst_hyps = [] ; cst_kind = kind; cst_locl = local; - cst_exported = []; - cst_was_seff = false; } in let kn = declare_constant_common id cst in let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in diff --git a/interp/impargs.ml b/interp/impargs.ml index b7125fc85..d8241c044 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -414,7 +414,7 @@ let compute_semi_auto_implicits env f manual t = let compute_constant_implicits flags manual cst = let env = Global.env () in let cb = Environ.lookup_constant cst env in - let ty = Typeops.type_of_constant_type env cb.const_type in + let ty = cb.const_type in let impls = compute_semi_auto_implicits env flags manual ty in impls diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 95822fac6..80d41847c 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -18,7 +18,6 @@ open Util open Names open Term open Declarations -open Environ open Univ module NamedDecl = Context.Named.Declaration @@ -151,9 +150,14 @@ let abstract_constant_body = type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool -type result = - constant_def * constant_type * projection_body option * - constant_universes * inline * Context.Named.t option +type result = { + cook_body : constant_def; + cook_type : types; + cook_proj : projection_body option; + cook_universes : constant_universes; + cook_inline : inline; + cook_context : Context.Named.t option; +} let on_body ml hy f = function | Undef _ as x -> x @@ -162,11 +166,6 @@ let on_body ml hy f = function OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:f { Opaqueproof.modlist = ml; abstract = hy } o) -let constr_of_def otab = function - | Undef _ -> assert false - | Def cs -> Mod_subst.force_constr cs - | OpaqueDef lc -> Opaqueproof.force_proof otab lc - let expmod_constr_subst cache modlist subst c = let c = expmod_constr cache modlist c in Vars.subst_univs_level_constr subst c @@ -215,17 +214,7 @@ let cook_constant ~hcons env { from = cb; info } = List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl'))) hyps) hyps ~init:cb.const_hyps in - let typ = match cb.const_type with - | RegularArity t -> - let typ = - abstract_constant_type (expmod t) hyps in - RegularArity typ - | TemplateArity (ctx,s) -> - let t = mkArity (ctx,Type s.template_level) in - let typ = abstract_constant_type (expmod t) hyps in - let j = make_judge (constr_of_def (opaque_tables env) body) typ in - Typeops.make_polymorphic_if_constant_for_ind env j - in + let typ = abstract_constant_type (expmod cb.const_type) hyps in let projection pb = let c' = abstract_constant_body (expmod pb.proj_body) hyps in let etab = abstract_constant_body (expmod (fst pb.proj_eta)) hyps in @@ -239,9 +228,6 @@ let cook_constant ~hcons env { from = cb; info } = | _ -> assert false with Not_found -> (((pb.proj_ind,0),Univ.Instance.empty), 0) in - let typ = (* By invariant, a regular arity *) - match typ with RegularArity t -> t | TemplateArity _ -> assert false - in let ctx, ty' = decompose_prod_n (n' + pb.proj_npars + 1) typ in { proj_ind = mind; proj_npars = pb.proj_npars + n'; proj_arg = pb.proj_arg; proj_eta = etab, etat; @@ -254,9 +240,14 @@ let cook_constant ~hcons env { from = cb; info } = | Polymorphic_const auctx -> Polymorphic_const (AUContext.union abs_ctx auctx) in - (body, typ, Option.map projection cb.const_proj, - univs, cb.const_inline_code, - Some const_hyps) + { + cook_body = body; + cook_type = typ; + cook_proj = Option.map projection cb.const_proj; + cook_universes = univs; + cook_inline = cb.const_inline_code; + cook_context = Some const_hyps; + } (* let cook_constant_key = Profile.declare_profile "cook_constant" *) (* let cook_constant = Profile.profile2 cook_constant_key cook_constant *) diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 79a028d76..6d1b776c0 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -16,9 +16,14 @@ type recipe = { from : constant_body; info : Opaqueproof.cooking_info } type inline = bool -type result = - constant_def * constant_type * projection_body option * - constant_universes * inline * Context.Named.t option +type result = { + cook_body : constant_def; + cook_type : types; + cook_proj : projection_body option; + cook_universes : constant_universes; + cook_inline : inline; + cook_context : Context.Named.t option; +} val cook_constant : hcons:bool -> env -> recipe -> result val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr diff --git a/kernel/declarations.ml b/kernel/declarations.ml index f35438dfc..9697b0b8b 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -36,8 +36,6 @@ type ('a, 'b) declaration_arity = | RegularArity of 'a | TemplateArity of 'b -type constant_type = (types, Context.Rel.t * template_arity) declaration_arity - (** Inlining level of parameters at functor applications. None means no inlining *) @@ -83,7 +81,7 @@ type typing_flags = { type constant_body = { const_hyps : Context.Named.t; (** New: younger hyp at top *) const_body : constant_def; - const_type : constant_type; + const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; const_proj : projection_body option; diff --git a/kernel/declareops.ml b/kernel/declareops.ml index efce21982..85dd1e66d 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -69,10 +69,6 @@ let subst_rel_declaration sub = let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) -let subst_template_cst_arity sub (ctx,s as arity) = - let ctx' = subst_rel_context sub ctx in - if ctx==ctx' then arity else (ctx',s) - let subst_const_type sub arity = if is_empty_subst sub then arity else subst_mps sub arity @@ -94,7 +90,7 @@ let subst_const_body sub cb = if is_empty_subst sub then cb else let body' = subst_const_def sub cb.const_body in - let type' = subst_decl_arity subst_const_type subst_template_cst_arity sub cb.const_type in + let type' = subst_const_type sub cb.const_type in let proj' = Option.smartmap (subst_const_proj sub) cb.const_proj in if body' == cb.const_body && type' == cb.const_type && proj' == cb.const_proj then cb @@ -120,14 +116,6 @@ let hcons_rel_decl = let hcons_rel_context l = List.smartmap hcons_rel_decl l -let hcons_regular_const_arity t = Term.hcons_constr t - -let hcons_template_const_arity (ctx, ar) = - (hcons_rel_context ctx, hcons_template_arity ar) - -let hcons_const_type = - map_decl_arity hcons_regular_const_arity hcons_template_const_arity - let hcons_const_def = function | Undef inl -> Undef inl | Def l_constr -> @@ -145,7 +133,7 @@ let hcons_const_universes cbu = let hcons_const_body cb = { cb with const_body = hcons_const_def cb.const_body; - const_type = hcons_const_type cb.const_type; + const_type = Term.hcons_constr cb.const_type; const_universes = hcons_const_universes cb.const_universes } (** {6 Inductive types } *) diff --git a/kernel/entries.ml b/kernel/entries.ml index 3fa25c142..a1ccbdbc1 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -64,6 +64,10 @@ type mutual_inductive_entry = { type 'a proof_output = constr Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation +type constant_universes_entry = + | Monomorphic_const_entry of Univ.universe_context + | Polymorphic_const_entry of Univ.universe_context + type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) @@ -71,8 +75,7 @@ type 'a definition_entry = { (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; - const_entry_polymorphic : bool; - const_entry_universes : Univ.universe_context; + const_entry_universes : constant_universes_entry; const_entry_opaque : bool; const_entry_inline_code : bool } diff --git a/kernel/environ.ml b/kernel/environ.ml index b01b65200..d2c737ab0 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -232,12 +232,6 @@ let constraints_of cb u = | Monomorphic_const _ -> Univ.Constraint.empty | Polymorphic_const ctx -> Univ.AUContext.instantiate u ctx -let map_regular_arity f = function - | RegularArity a as ar -> - let a' = f a in - if a' == a then ar else RegularArity a' - | TemplateArity _ -> assert false - (* constant_type gives the type of a constant *) let constant_type env (kn,u) = let cb = lookup_constant kn env in @@ -245,7 +239,7 @@ let constant_type env (kn,u) = | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty | Polymorphic_const ctx -> let csts = constraints_of cb u in - (map_regular_arity (subst_instance_constr u) cb.const_type, csts) + (subst_instance_constr u cb.const_type, csts) let constant_context env kn = let cb = lookup_constant kn env in @@ -287,7 +281,7 @@ let constant_value_and_type env (kn, u) = | OpaqueDef _ -> None | Undef _ -> None in - b', map_regular_arity (subst_instance_constr u) cb.const_type, cst + 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) @@ -303,7 +297,7 @@ let constant_value_and_type env (kn, u) = let constant_type_in env (kn,u) = let cb = lookup_constant kn env in if Declareops.constant_is_polymorphic cb then - map_regular_arity (subst_instance_constr u) cb.const_type + subst_instance_constr u cb.const_type else cb.const_type let constant_value_in env (kn,u) = @@ -337,15 +331,6 @@ let polymorphic_pconstant (cst,u) env = let type_in_type_constant cst env = not (lookup_constant cst env).const_typing_flags.check_universes -let template_polymorphic_constant cst env = - match (lookup_constant cst env).const_type with - | TemplateArity _ -> true - | RegularArity _ -> false - -let template_polymorphic_pconstant (cst,u) env = - if not (Univ.Instance.is_empty u) then false - else template_polymorphic_constant cst env - let lookup_projection cst env = match (lookup_constant (Projection.constant cst) env).const_proj with | Some pb -> pb diff --git a/kernel/environ.mli b/kernel/environ.mli index cd7a9d279..377c61de2 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -139,10 +139,6 @@ val polymorphic_constant : constant -> env -> bool val polymorphic_pconstant : pconstant -> env -> bool val type_in_type_constant : constant -> env -> bool -(** Old-style polymorphism *) -val template_polymorphic_constant : constant -> env -> bool -val template_polymorphic_pconstant : pconstant -> env -> bool - (** {6 ... } *) (** [constant_value env c] raises [NotEvaluableConst Opaque] if [c] is opaque and [NotEvaluableConst NoBody] if it has no @@ -153,11 +149,11 @@ type const_evaluation_result = NoBody | Opaque | IsProj exception NotEvaluableConst of const_evaluation_result val constant_value : env -> constant puniverses -> constr constrained -val constant_type : env -> constant puniverses -> constant_type constrained +val constant_type : env -> constant puniverses -> types constrained val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option val constant_value_and_type : env -> constant puniverses -> - constr option * constant_type * Univ.constraints + constr option * types * Univ.constraints (** The universe context associated to the constant, empty if not polymorphic *) val constant_context : env -> constant -> Univ.abstract_universe_context @@ -166,7 +162,7 @@ val constant_context : env -> constant -> Univ.abstract_universe_context already contains the constraints corresponding to the constant application. *) val constant_value_in : env -> constant puniverses -> constr -val constant_type_in : env -> constant puniverses -> constant_type +val constant_type_in : env -> constant puniverses -> types val constant_opt_value_in : env -> constant puniverses -> constr option (** {6 Primitive projections} *) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index c7f3e5c51..0888ccc10 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -83,7 +83,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let c',cst = match cb.const_body with | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in - let typ = Typeops.type_of_constant_type env' cb.const_type in + let typ = cb.const_type in let cst' = Reduction.infer_conv_leq env' (Environ.universes env') j.uj_type typ in j.uj_val, cst' @@ -103,7 +103,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv = let cst = match cb.const_body with | Undef _ | OpaqueDef _ -> let j = Typeops.infer env' c in - let typ = Typeops.type_of_constant_type env' cb.const_type in + let typ = cb.const_type in let cst' = Reduction.infer_conv_leq env' (Environ.universes env') j.uj_type typ in cst' diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ed4c7d57a..04051f2e2 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -382,12 +382,13 @@ let safe_push_named d env = let push_named_def (id,de) senv = - let c,typ,univs = - match Term_typing.translate_local_def senv.revstruct senv.env id de with - | c, typ, Monomorphic_const ctx -> c, typ, ctx - | _, _, Polymorphic_const _ -> assert false + let open Entries in + let trust = Term_typing.SideEffects senv.revstruct in + let c,typ,univs = Term_typing.translate_local_def trust senv.env id de in + let poly = match de.Entries.const_entry_universes with + | Monomorphic_const_entry _ -> false + | Polymorphic_const_entry _ -> true in - let poly = de.Entries.const_entry_polymorphic in let univs = Univ.ContextSet.of_context univs in let c, univs = match c with | Def c -> Mod_subst.force_constr c, univs @@ -492,12 +493,16 @@ let add_field ((l,sfb) as field) gn senv = let update_resolver f senv = { senv with modresolver = f senv.modresolver } (** Insertion of constants and parameters in environment *) +type 'a effect_entry = +| EffectEntry : private_constants effect_entry +| PureEntry : unit effect_entry + type global_declaration = - | ConstantEntry of bool * private_constants Entries.constant_entry + | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration | GlobalRecipe of Cooking.recipe type exported_private_constant = - constant * private_constants Entries.constant_entry * private_constant_role + constant * private_constant_role let add_constant_aux no_section senv (kn, cb) = let l = pi3 (Constant.repr3 kn) in @@ -521,30 +526,29 @@ let add_constant_aux no_section senv (kn, cb) = in senv'' +let export_private_constants ~in_section ce senv = + let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in + let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in + let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in + let no_section = not in_section in + let senv = List.fold_left (add_constant_aux no_section) senv bodies in + (ce, exported), senv + let add_constant dir l decl senv = let kn = make_con senv.modpath dir l in let no_section = DirPath.is_empty dir in - let seff_to_export, decl = - match decl with - | ConstantEntry (true, ce) -> - let exports, ce = - Term_typing.export_side_effects senv.revstruct senv.env ce in - exports, ConstantEntry (false, ce) - | _ -> [], decl - in - let senv = - List.fold_left (add_constant_aux no_section) senv - (List.map (fun (kn,cb,_,_) -> kn, cb) seff_to_export) in let senv = let cb = match decl with - | ConstantEntry (export_seff,ce) -> - Term_typing.translate_constant senv.revstruct senv.env kn ce + | ConstantEntry (EffectEntry, ce) -> + Term_typing.translate_constant (Term_typing.SideEffects senv.revstruct) senv.env kn ce + | ConstantEntry (PureEntry, ce) -> + Term_typing.translate_constant Term_typing.Pure senv.env kn ce | GlobalRecipe r -> let cb = Term_typing.translate_recipe senv.env kn r in if no_section then Declareops.hcons_const_body cb else cb in add_constant_aux no_section senv (kn, cb) in - (kn, List.map (fun (kn,_,ce,r) -> kn, ce, r) seff_to_export), senv + kn, senv (** Insertion of inductive types *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 5bb8ceb1a..752fdd793 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -67,7 +67,7 @@ val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output val inline_private_constants_in_constr : Environ.env -> Constr.constr -> private_constants -> Constr.constr val inline_private_constants_in_definition_entry : - Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry + Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry val universes_of_private : private_constants -> Univ.universe_context_set list @@ -94,19 +94,26 @@ val push_named_def : (** Insertion of global axioms or definitions *) +type 'a effect_entry = +| EffectEntry : private_constants effect_entry +| PureEntry : unit effect_entry + type global_declaration = - (* bool: export private constants *) - | ConstantEntry of bool * private_constants Entries.constant_entry + | ConstantEntry : 'a effect_entry * 'a Entries.constant_entry -> global_declaration | GlobalRecipe of Cooking.recipe type exported_private_constant = - constant * private_constants Entries.constant_entry * private_constant_role + constant * private_constant_role + +val export_private_constants : in_section:bool -> + private_constants Entries.constant_entry -> + (unit Entries.constant_entry * exported_private_constant list) safe_transformer (** returns the main constant plus a list of auxiliary constants (empty unless one requires the side effects to be exported) *) val add_constant : DirPath.t -> Label.t -> global_declaration -> - (constant * exported_private_constant list) safe_transformer + constant safe_transformer (** Adding an inductive type *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index bd82dd465..b311165f1 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -313,8 +313,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = error (PolymorphicStatusExpected false) in (* Now check types *) - let typ1 = Typeops.type_of_constant_type env cb1.const_type in - let typ2 = Typeops.type_of_constant_type env cb2.const_type in + let typ1 = cb1.const_type in + let typ2 = cb2.const_type in let cst = check_type poly cst env typ1 typ2 in (* Now we check the bodies: - A transparent constant can only be implemented by a compatible diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index cf82d54ec..3f42c348f 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -21,7 +21,6 @@ open Environ open Entries open Typeops -module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (* Insertion of constants and parameters in environment. *) @@ -77,6 +76,10 @@ end type side_effects = SideEffects.t +type _ trust = +| Pure : unit trust +| SideEffects : structure_body -> side_effects trust + let uniq_seff_rev = SideEffects.repr let uniq_seff l = List.rev (SideEffects.repr l) @@ -124,7 +127,7 @@ let inline_side_effects env body ctx side_eff = match cb.const_universes with | Monomorphic_const cnstctx -> (** Abstract over the term at the top of the proof *) - let ty = Typeops.type_of_constant_type env cb.const_type in + let ty = cb.const_type in let subst = Cmap_env.add c (Inr var) subst in let univs = Univ.ContextSet.of_context cnstctx in let ctx = Univ.ContextSet.union ctx univs in @@ -232,7 +235,7 @@ let abstract_constant_universes abstract uctx = let sbst, auctx = Univ.abstract_universes uctx in sbst, Polymorphic_const auctx -let infer_declaration ~trust env kn dcl = +let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context ~strict:(not poly) uctx env in @@ -243,7 +246,14 @@ let infer_declaration ~trust env kn dcl = in let c = Typeops.assumption_of_judgment env j in let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in - Undef nl, RegularArity t, None, univs, false, ctx + { + Cooking.cook_body = Undef nl; + cook_type = t; + cook_proj = None; + cook_universes = univs; + cook_inline = false; + cook_context = ctx; + } (** Definition [c] is opaque (Qed), non polymorphic and with a specified type, so we delay the typing and hash consing of its body. @@ -251,52 +261,69 @@ let infer_declaration ~trust env kn dcl = delay even in the polymorphic case. *) | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; - const_entry_polymorphic = false} as c) -> - let env = push_context ~strict:true c.const_entry_universes env in + const_entry_universes = Monomorphic_const_entry univs } as c) -> + let env = push_context ~strict:true univs env in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let tyj = infer_type env typ in let proofterm = Future.chain ~pure:true body (fun ((body,uctx),side_eff) -> - let body, uctx, signatures = - inline_side_effects env body uctx side_eff in - let valid_signatures = check_signatures trust signatures in - let env = push_context_set uctx env in - let j = + let j, uctx = match trust with + | Pure -> + let env = push_context_set uctx env in + let j = infer env body in + let _ = judge_of_cast env j DEFAULTcast tyj in + j, uctx + | SideEffects mb -> + let (body, uctx, signatures) = inline_side_effects env body uctx side_eff in + let valid_signatures = check_signatures mb signatures in + let env = push_context_set uctx env in let body,env,ectx = skip_trusted_seff valid_signatures body env in let j = infer env body in - unzip ectx j in - let _ = judge_of_cast env j DEFAULTcast tyj in + let j = unzip ectx j in + let _ = judge_of_cast env j DEFAULTcast tyj in + j, uctx + in let c = hcons_constr j.uj_val in feedback_completion_typecheck feedback_id; c, uctx) in let def = OpaqueDef (Opaqueproof.create proofterm) in - def, RegularArity typ, None, - (Monomorphic_const c.const_entry_universes), - c.const_entry_inline_code, c.const_entry_secctx + { + Cooking.cook_body = def; + cook_type = typ; + cook_proj = None; + cook_universes = Monomorphic_const univs; + cook_inline = c.const_entry_inline_code; + cook_context = c.const_entry_secctx; + } (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> let { const_entry_type = typ; const_entry_opaque = opaque } = c in let { const_entry_body = body; const_entry_feedback = feedback_id } = c in let (body, ctx), side_eff = Future.join body in - let univsctx = Univ.ContextSet.of_context c.const_entry_universes in - let body, ctx, _ = inline_side_effects env body - (Univ.ContextSet.union univsctx ctx) side_eff in - let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in - let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in + let poly, univs = match c.const_entry_universes with + | Monomorphic_const_entry univs -> false, univs + | Polymorphic_const_entry univs -> true, univs + in + let univsctx = Univ.ContextSet.of_context univs in + let ctx = Univ.ContextSet.union univsctx ctx in + let body, ctx, _ = match trust with + | Pure -> body, ctx, [] + | SideEffects _ -> inline_side_effects env body ctx side_eff + in + let env = push_context_set ~strict:(not poly) ctx env in + let abstract = poly && not (Option.is_empty kn) in let usubst, univs = abstract_constant_universes abstract (Univ.ContextSet.to_context ctx) in let j = infer env body in let typ = match typ with | None -> - if not c.const_entry_polymorphic then (* Old-style polymorphism *) - make_polymorphic_if_constant_for_ind env j - else RegularArity (Vars.subst_univs_level_constr usubst j.uj_type) + Vars.subst_univs_level_constr usubst j.uj_type | Some t -> let tj = infer_type env t in let _ = judge_of_cast env j DEFAULTcast tj in - RegularArity (Vars.subst_univs_level_constr usubst t) + Vars.subst_univs_level_constr usubst t in let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in let def = @@ -304,7 +331,14 @@ let infer_declaration ~trust env kn dcl = else Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; - def, typ, None, univs, c.const_entry_inline_code, c.const_entry_secctx + { + Cooking.cook_body = def; + cook_type = typ; + cook_proj = None; + cook_universes = univs; + cook_inline = c.const_entry_inline_code; + cook_context = c.const_entry_secctx; + } | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} -> let mib, _ = Inductive.lookup_mind_specif env (ind,0) in @@ -324,16 +358,14 @@ let infer_declaration ~trust env kn dcl = Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi) in let term, typ = pb.proj_eta in - Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb, - univs, false, None - -let global_vars_set_constant_type env = function - | RegularArity t -> global_vars_set env t - | TemplateArity (ctx,_) -> - Context.Rel.fold_outside - (RelDecl.fold_constr - (fun t c -> Id.Set.union (global_vars_set env t) c)) - ctx ~init:Id.Set.empty + { + Cooking.cook_body = Def (Mod_subst.from_val (hcons_constr term)); + cook_type = typ; + cook_proj = Some pb; + cook_universes = univs; + cook_inline = false; + cook_context = None; + } let record_aux env s_ty s_bo suggested_expr = let in_ty = keep_hyps env s_ty in @@ -349,7 +381,9 @@ let record_aux env s_ty s_bo suggested_expr = let suggest_proof_using = ref (fun _ _ _ _ _ -> "") let set_suggest_proof_using f = suggest_proof_using := f -let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = +let build_constant_declaration kn env result = + let open Cooking in + let typ = result.cook_type in let check declared inferred = let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in @@ -376,11 +410,12 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = (* We try to postpone the computation of used section variables *) let hyps, def = let context_ids = List.map NamedDecl.get_id (named_context env) in - match ctx with + let def = result.cook_body in + match result.cook_context with | None when not (List.is_empty context_ids) -> (* No declared section vars, and non-empty section context: we must look at the body NOW, if any *) - let ids_typ = global_vars_set_constant_type env typ in + let ids_typ = global_vars_set env typ in let ids_def = match def with | Undef _ -> Idset.empty | Def cs -> global_vars_set env (Mod_subst.force_constr cs) @@ -408,20 +443,21 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = match def with | Undef _ as x -> x (* nothing to check *) | Def cs as x -> - let ids_typ = global_vars_set_constant_type env typ in + let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env (Mod_subst.force_constr cs) in let inferred = keep_hyps env (Idset.union ids_typ ids_def) in check declared inferred; x | OpaqueDef lc -> (* In this case we can postpone the check *) OpaqueDef (Opaqueproof.iter_direct_opaque (fun c -> - let ids_typ = global_vars_set_constant_type env typ in + let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env c in let inferred = keep_hyps env (Idset.union ids_typ ids_def) in check declared inferred) lc) in + let univs = result.cook_universes in let tps = let res = - match proj with + match result.cook_proj with | None -> compile_constant_body env univs def | Some pb -> (* The compilation of primitive projections is a bit tricky, because @@ -434,10 +470,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = { const_hyps = hyps; const_body = def; const_type = typ; - const_proj = proj; + const_proj = result.cook_proj; const_body_code = None; const_universes = univs; - const_inline_code = inline_code; + const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env; } in @@ -448,10 +484,10 @@ let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) = { const_hyps = hyps; const_body = def; const_type = typ; - const_proj = proj; + const_proj = result.cook_proj; const_body_code = tps; const_universes = univs; - const_inline_code = inline_code; + const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } (*s Global and local constant declaration. *) @@ -461,11 +497,12 @@ let translate_constant mb env kn ce = (infer_declaration ~trust:mb env (Some kn) ce) let constant_entry_of_side_effect cb u = - let poly, univs = + let univs = match cb.const_universes with - | Monomorphic_const ctx -> false, ctx + | Monomorphic_const uctx -> + Monomorphic_const_entry uctx | Polymorphic_const auctx -> - true, Univ.AUContext.repr auctx + Polymorphic_const_entry (Univ.AUContext.repr auctx) in let pt = match cb.const_body, u with @@ -473,12 +510,10 @@ let constant_entry_of_side_effect cb u = | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty | _ -> assert false in DefinitionEntry { - const_entry_body = Future.from_val (pt, empty_seff); + const_entry_body = Future.from_val (pt, ()); const_entry_secctx = None; const_entry_feedback = None; - const_entry_type = - (match cb.const_type with RegularArity t -> Some t | _ -> None); - const_entry_polymorphic = poly; + const_entry_type = Some cb.const_type; const_entry_universes = univs; const_entry_opaque = Declareops.is_opaque cb; const_entry_inline_code = cb.const_inline_code } @@ -497,17 +532,18 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effects constant_entry * side_effect_role + constant * constant_body * side_effect_role let export_side_effects mb env ce = match ce with - | ParameterEntry _ | ProjectionEntry _ -> [], ce + | ParameterEntry e -> [], ParameterEntry e + | ProjectionEntry e -> [], ProjectionEntry e | DefinitionEntry c -> let { const_entry_body = body } = c in let _, eff = Future.force body in let ce = DefinitionEntry { c with const_entry_body = Future.chain ~pure:true body - (fun (b_ctx, _) -> b_ctx, empty_seff) } in + (fun (b_ctx, _) -> b_ctx, ()) } in let not_exists (c,_,_,_) = try ignore(Environ.lookup_constant c env); false with Not_found -> true in @@ -547,8 +583,8 @@ let export_side_effects mb env ce = let env, cbs = List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> let ce = constant_entry_of_side_effect ocb u in - let cb = translate_constant mb env kn ce in - (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) + let cb = translate_constant Pure env kn ce in + (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,r) :: cbs)) (env,[]) cbs in translate_seff sl rest (cbs @ acc) env | Some sl, cbs :: rest -> @@ -556,7 +592,7 @@ let export_side_effects mb env ce = let cbs = List.map turn_direct cbs in let env = List.fold_left push_seff env cbs in let ecbs = List.map (fun (kn,cb,u,r) -> - kn, cb, constant_entry_of_side_effect cb u, r) cbs in + kn, cb, r) cbs in translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env in translate_seff trusted seff [] env @@ -575,11 +611,11 @@ let translate_recipe env kn r = build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) let translate_local_def mb env id centry = - let def,typ,proj,univs,inline_code,ctx = - infer_declaration ~trust:mb env None (DefinitionEntry centry) in - let typ = type_of_constant_type env typ in - if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin - match def with + let open Cooking in + let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in + let typ = decl.cook_type in + if Option.is_empty decl.cook_context && !Flags.compilation_mode = Flags.BuildVo then begin + match decl.cook_body with | Undef _ -> () | Def _ -> () | OpaqueDef lc -> @@ -592,7 +628,11 @@ let translate_local_def mb env id centry = env ids_def ids_typ context_ids in record_aux env ids_typ ids_def expr end; - def, typ, univs + let univs = match decl.cook_universes with + | Monomorphic_const ctx -> ctx + | Polymorphic_const _ -> assert false + in + decl.cook_body, typ, univs (* Insertion of inductive types. *) @@ -602,7 +642,7 @@ let inline_entry_side_effects env ce = { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body (fun ((body, ctx), side_eff) -> let body, ctx',_ = inline_side_effects env body ctx side_eff in - (body, ctx'), empty_seff); + (body, ctx'), ()); } let inline_side_effects env body side_eff = diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 77d126074..24153343e 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -14,8 +14,12 @@ open Entries type side_effects -val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> - constant_def * types * constant_universes +type _ trust = +| Pure : unit trust +| SideEffects : structure_body -> side_effects trust + +val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry -> + constant_def * types * Univ.universe_context val translate_local_assum : env -> types -> types @@ -26,7 +30,7 @@ val inline_side_effects : env -> constr -> side_effects -> constr redexes. *) val inline_entry_side_effects : - env -> side_effects definition_entry -> side_effects definition_entry + env -> side_effects definition_entry -> unit definition_entry (** Same as {!inline_side_effects} but applied to entries. Only modifies the {!Entries.const_entry_body} field. It is meant to get a term out of a not yet type checked proof. *) @@ -43,7 +47,7 @@ val uniq_seff : side_effects -> side_effect list val equal_eff : side_effect -> side_effect -> bool val translate_constant : - structure_body -> env -> constant -> side_effects constant_entry -> + 'a trust -> env -> constant -> 'a constant_entry -> constant_body type side_effect_role = @@ -51,7 +55,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effects constant_entry * side_effect_role + constant * constant_body * side_effect_role (* Given a constant entry containing side effects it exports them (either * by re-checking them or trusting them). Returns the constant bodies to @@ -59,10 +63,7 @@ type exported_side_effect = * needs to be translated as usual after this step. *) val export_side_effects : structure_body -> env -> side_effects constant_entry -> - exported_side_effect list * side_effects constant_entry - -val constant_entry_of_side_effect : - constant_body -> seff_env -> side_effects constant_entry + exported_side_effect list * unit constant_entry val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body @@ -71,8 +72,8 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:structure_body -> env -> constant option -> - side_effects constant_entry -> Cooking.result +val infer_declaration : trust:'a trust -> env -> constant option -> + 'a constant_entry -> Cooking.result val build_constant_declaration : constant -> env -> Cooking.result -> constant_body diff --git a/kernel/typeops.ml b/kernel/typeops.ml index b814deb6e..044877e82 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -111,36 +111,17 @@ let check_hyps_inclusion env f c sign = (* Type of constants *) -let type_of_constant_type_knowing_parameters env t paramtyps = - match t with - | RegularArity t -> t - | TemplateArity (sign,ar) -> - let ctx = List.rev sign in - let ctx,s = instantiate_universes env ctx ar paramtyps in - mkArity (List.rev ctx,s) - -let type_of_constant_knowing_parameters env (kn,u as cst) args = +let type_of_constant env (kn,u as cst) = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty, cu = constant_type env cst in - let ty = type_of_constant_type_knowing_parameters env ty args in let () = check_constraints cu env in ty -let type_of_constant_knowing_parameters_in env (kn,u as cst) args = +let type_of_constant_in env (kn,u as cst) = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in - let ty = constant_type_in env cst in - type_of_constant_type_knowing_parameters env ty args - -let type_of_constant env cst = - type_of_constant_knowing_parameters env cst [||] - -let type_of_constant_in env cst = - type_of_constant_knowing_parameters_in env cst [||] - -let type_of_constant_type env t = - type_of_constant_type_knowing_parameters env t [||] + constant_type_in env cst (* Type of a lambda-abstraction. *) @@ -369,9 +350,6 @@ let rec execute env cstr = | Ind ind when Environ.template_polymorphic_pind ind env -> let args = Array.map (fun t -> lazy t) argst in type_of_inductive_knowing_parameters env ind args - | Const cst when Environ.template_polymorphic_pconstant cst env -> - let args = Array.map (fun t -> lazy t) argst in - type_of_constant_knowing_parameters env cst args | _ -> (* No template polymorphism *) execute env f @@ -509,8 +487,6 @@ let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k) let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x) let judge_of_constant env cst = make_judge (mkConstU cst) (type_of_constant env cst) -let judge_of_constant_knowing_parameters env cst args = - make_judge (mkConstU cst) (type_of_constant_knowing_parameters env cst args) let judge_of_projection env p cj = make_judge (mkProj (p,cj.uj_val)) (type_of_projection env p cj.uj_val cj.uj_type) @@ -559,34 +535,3 @@ let type_of_projection_constant env (p,u) = Vars.subst_instance_constr u pb.proj_type else pb.proj_type | None -> raise (Invalid_argument "type_of_projection: not a projection") - -(* Instantiation of terms on real arguments. *) - -(* Make a type polymorphic if an arity *) - -let extract_level env p = - let _,c = dest_prod_assum env p in - match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None - -let extract_context_levels env l = - let fold l = function - | RelDecl.LocalAssum (_,p) -> extract_level env p :: l - | RelDecl.LocalDef _ -> l - in - List.fold_left fold [] l - -let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = - let params, ccl = dest_prod_assum env t in - match kind_of_term ccl with - | Sort (Type u) -> - let ind, l = decompose_app (whd_all env c) in - if isInd ind && List.is_empty l then - let mis = lookup_mind_specif env (fst (destInd ind)) in - let nparams = Inductive.inductive_params mis in - let paramsl = CList.lastn nparams params in - let param_ccls = extract_context_levels env paramsl in - let s = { template_param_levels = param_ccls; template_level = u} in - TemplateArity (params,s) - else RegularArity t - | _ -> - RegularArity t diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 24521070e..a8f7fba9a 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -11,7 +11,6 @@ open Univ open Term open Environ open Entries -open Declarations (** {6 Typing functions (not yet tagged as safe) } @@ -53,9 +52,6 @@ val judge_of_variable : env -> variable -> unsafe_judgment val judge_of_constant : env -> pconstant -> unsafe_judgment -val judge_of_constant_knowing_parameters : - env -> pconstant -> types Lazy.t array -> unsafe_judgment - (** {6 type of an applied projection } *) val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment @@ -98,21 +94,9 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -val type_of_constant_type : env -> constant_type -> types - val type_of_projection_constant : env -> Names.projection puniverses -> types val type_of_constant_in : env -> pconstant -> types -val type_of_constant_type_knowing_parameters : - env -> constant_type -> types Lazy.t array -> types - -val type_of_constant_knowing_parameters_in : - env -> pconstant -> types Lazy.t array -> types - -(** Make a type polymorphic if an arity *) -val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> - constant_type - (** Check that hyps are included in env and fails with error otherwise *) val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit diff --git a/lib/flags.ml b/lib/flags.ml index 5d9d9dcf5..0bce22f58 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -106,7 +106,7 @@ let we_are_parsing = ref false (* Current means no particular compatibility consideration. For correct comparisons, this constructor should remain the last one. *) -type compat_version = VOld | V8_5 | V8_6 | Current +type compat_version = VOld | V8_5 | V8_6 | V8_7 | Current let compat_version = ref Current @@ -120,6 +120,9 @@ let version_compare v1 v2 = match v1, v2 with | V8_6, V8_6 -> 0 | V8_6, _ -> -1 | _, V8_6 -> 1 + | V8_7, V8_7 -> 0 + | V8_7, _ -> -1 + | _, V8_7 -> 1 | Current, Current -> 0 let version_strictly_greater v = version_compare !compat_version v > 0 @@ -129,6 +132,7 @@ let pr_version = function | VOld -> "old" | V8_5 -> "8.5" | V8_6 -> "8.6" + | V8_7 -> "8.7" | Current -> "current" (* Translate *) diff --git a/lib/flags.mli b/lib/flags.mli index e63f1ec26..eb4c37a54 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -77,7 +77,7 @@ val raw_print : bool ref (* Univ print flag, never set anywere. Maybe should belong to Univ? *) val univ_print : bool ref -type compat_version = VOld | V8_5 | V8_6 | Current +type compat_version = VOld | V8_5 | V8_6 | V8_7 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool diff --git a/lib/profile.ml b/lib/profile.ml index b66916185..0bc226a45 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -85,6 +85,9 @@ let init_alloc = ref 0.0 let reset_profile () = List.iter reset_record !prof_table let init_profile () = + (* We test Flags.profile as a way to support declaring profiled + functions in plugins *) + if !prof_table <> [] || Flags.profile then begin let outside = create_record () in stack := [outside]; last_alloc := get_alloc (); @@ -92,6 +95,7 @@ let init_profile () = init_time := get_time (); outside.tottime <- - !init_time; outside.owntime <- - !init_time + end let ajoute n o = o.owntime <- o.owntime + n.owntime; @@ -317,15 +321,15 @@ let adjust_time ov_bc ov_ad e = owntime = e.owntime - int_of_float (ad_imm +. bc_imm) } let close_profile print = - let dw = spent_alloc () in - let t = get_time () in - match !stack with - | [outside] -> - outside.tottime <- outside.tottime + t; - outside.owntime <- outside.owntime + t; - ajoute_ownalloc outside dw; - ajoute_totalloc outside dw; - if !prof_table <> [] then begin + if !prof_table <> [] then begin + let dw = spent_alloc () in + let t = get_time () in + match !stack with + | [outside] -> + outside.tottime <- outside.tottime + t; + outside.owntime <- outside.owntime + t; + ajoute_ownalloc outside dw; + ajoute_totalloc outside dw; let ov_bc = time_overhead_B_C () (* B+C overhead *) in let ov_ad = time_overhead_A_D () (* A+D overhead *) in let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in @@ -346,8 +350,8 @@ let close_profile print = in if print then format_profile updated_data; init_profile () - end - | _ -> failwith "Inconsistency" + | _ -> failwith "Inconsistency" + end let print_profile () = close_profile true @@ -358,9 +362,6 @@ let declare_profile name = prof_table := (name,e)::!prof_table; e -(* Default initialization, may be overridden *) -let _ = init_profile () - (******************************) (* Entry points for profiling *) let profile1 e f a = diff --git a/library/global.ml b/library/global.ml index 5b17855dc..963c97741 100644 --- a/library/global.ml +++ b/library/global.ml @@ -86,6 +86,7 @@ let push_context b c = globalize0 (Safe_typing.push_context b c) let set_engagement c = globalize0 (Safe_typing.set_engagement c) let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c) +let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) @@ -198,8 +199,7 @@ let type_of_global_in_context env r = | ConstRef c -> let cb = Environ.lookup_constant c env in let univs = Declareops.constant_polymorphic_context cb in - let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in - Typeops.type_of_constant_type env cb.Declarations.const_type, univs + cb.Declarations.const_type, univs | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let univs = Declareops.inductive_polymorphic_context mib in @@ -254,7 +254,7 @@ let is_template_polymorphic r = let env = env() in match r with | VarRef id -> false - | ConstRef c -> Environ.template_polymorphic_constant c env + | ConstRef c -> false | IndRef ind -> Environ.template_polymorphic_ind ind env | ConstructRef cstr -> Environ.template_polymorphic_ind (inductive_of_constructor cstr) env diff --git a/library/global.mli b/library/global.mli index 48bcfa989..c777691d1 100644 --- a/library/global.mli +++ b/library/global.mli @@ -34,9 +34,12 @@ val set_typing_flags : Declarations.typing_flags -> unit val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit val push_named_def : (Id.t * Safe_typing.private_constants Entries.definition_entry) -> Univ.universe_context_set +val export_private_constants : in_section:bool -> + Safe_typing.private_constants Entries.constant_entry -> + unit Entries.constant_entry * Safe_typing.exported_private_constant list + val add_constant : - DirPath.t -> Id.t -> Safe_typing.global_declaration -> - constant * Safe_typing.exported_private_constant list + DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant val add_mind : DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 39826d744..89c2a0ae3 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -132,7 +132,7 @@ let rec add_labels mp = function exception Impossible let check_arity env cb = - let t = Typeops.type_of_constant_type env cb.const_type in + let t = cb.const_type in if Reduction.is_arity env t then raise Impossible let check_fix env cb i = diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 3661faada..661842790 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -518,7 +518,7 @@ and mlt_env env r = match r with match lookup_typedef kn cb with | Some _ as o -> o | None -> - let typ = Typeops.type_of_constant_type env cb.const_type + let typ = cb.const_type (* FIXME not sure if we should instantiate univs here *) in match flag_of_type env typ with | Info,TypeScheme -> @@ -543,7 +543,7 @@ let record_constant_type env kn opt_typ = | Some schema -> schema | None -> let typ = match opt_typ with - | None -> Typeops.type_of_constant_type env cb.const_type + | None -> cb.const_type | Some typ -> typ in let mlt = extract_type env [] 1 typ [] in @@ -969,7 +969,7 @@ let extract_fixpoint env vkn (fi,ti,ci) = let extract_constant env kn cb = let r = ConstRef kn in - let typ = Typeops.type_of_constant_type env cb.const_type in + let typ = cb.const_type in let warn_info () = if not (is_custom r) then add_info_axiom r in let warn_log () = if not (constant_has_body cb) then add_log_axiom r in @@ -1025,7 +1025,7 @@ let extract_constant env kn cb = let extract_constant_spec env kn cb = let r = ConstRef kn in - let typ = Typeops.type_of_constant_type env cb.const_type in + let typ = cb.const_type in try match flag_of_type env typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index f1bcde2f3..a4c2bcd88 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -120,7 +120,6 @@ let rec mgu = function mgu (a, a'); mgu (b, b') | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' -> List.iter mgu (List.combine l l') - | (Tdummy _, _ | _, Tdummy _) when lang() == Haskell -> () | Tdummy _, Tdummy _ -> () | Tvar i, Tvar j when Int.equal i j -> () | Tvar' i, Tvar' j when Int.equal i j -> () @@ -1052,6 +1051,7 @@ let rec simpl o = function | MLmagic(MLcase(typ,e,br)) -> let br' = Array.map (fun (ids,p,c) -> (ids,p,MLmagic c)) br in simpl o (MLcase(typ,e,br')) + | MLmagic(MLdummy _ as e) when lang () == Haskell -> e | MLmagic(MLexn _ as e) -> e | a -> ast_map (simpl o) a diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 863c9dc8d..89537ad3f 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -857,7 +857,7 @@ let make_graph (f_ref:global_reference) = with_full_print (fun () -> (Constrextern.extern_constr false env sigma body, Constrextern.extern_type false env sigma - ((*FIXME*) Typeops.type_of_constant_type env c_body.const_type) + ((*FIXME*) c_body.const_type) ) ) () diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 9f4829761..ef0fb8ea6 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -34,12 +34,6 @@ let get_polymorphic_positions sigma f = (match oib.mind_arity with | RegularArity _ -> assert false | TemplateArity templ -> templ.template_param_levels) - | Const (cst, u) -> - let cb = Global.lookup_constant cst in - (match cb.const_type with - | RegularArity _ -> assert false - | TemplateArity (_, templ) -> - templ.template_param_levels) | _ -> assert false let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index e0f9bfcb7..079524f34 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -192,11 +192,6 @@ let retype ?(polyprop=true) sigma = EConstr.of_constr (try Inductive.type_of_inductive_knowing_parameters ~polyprop env (mip, u) argtyps with Reduction.NotArity -> retype_error NotAnArity) - | Const (cst, u) -> - let u = EInstance.kind sigma u in - EConstr.of_constr (try Typeops.type_of_constant_knowing_parameters_in env (cst, u) argtyps - with Reduction.NotArity -> retype_error NotAnArity) - | Var id -> type_of_var env id | Construct (cstr, u) -> let u = EInstance.kind sigma u in EConstr.of_constr (type_of_constructor env (cstr, u)) @@ -220,7 +215,7 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = | Const (cst, u) -> let t = constant_type_in env (cst, EInstance.kind sigma u) in (* TODO *) - sigma, EConstr.of_constr (Typeops.type_of_constant_type_knowing_parameters env t [||]) + sigma, EConstr.of_constr t | Var id -> sigma, type_of_var env id | Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u)) | _ -> assert false diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 1bb003575..1f35fa19a 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -35,11 +35,6 @@ let meta_type evd mv = let ty = Evd.map_fl EConstr.of_constr ty in meta_instance evd ty -let constant_type_knowing_parameters env sigma (cst, u) jl = - let u = Unsafe.to_instance u in - let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in - EConstr.of_constr (type_of_constant_knowing_parameters_in env (cst, u) paramstyp) - let inductive_type_knowing_parameters env sigma (ind,u) jl = let u = Unsafe.to_instance u in let mspec = lookup_mind_specif env ind in @@ -315,9 +310,6 @@ let rec execute env evdref cstr = | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env -> make_judge f (inductive_type_knowing_parameters env !evdref (ind, u) jl) - | Const (cst, u) when EInstance.is_empty u && Environ.template_polymorphic_constant cst env -> - make_judge f - (constant_type_knowing_parameters env !evdref (cst, u) jl) | _ -> (* No template polymorphism *) execute env evdref f diff --git a/printing/prettyp.ml b/printing/prettyp.ml index e0ebe99db..09859157c 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -501,9 +501,6 @@ let print_body env evd = function let print_typed_body env evd (val_0,typ) = (print_body env evd val_0 ++ fnl () ++ str " : " ++ pr_ltype_env env evd typ) -let ungeneralized_type_of_constant_type t = - Typeops.type_of_constant_type (Global.env ()) t - let print_instance sigma cb = if Declareops.constant_is_polymorphic cb then let univs = Declareops.constant_polymorphic_context cb in @@ -515,17 +512,13 @@ let print_instance sigma cb = let print_constant with_values sep sp = let cb = Global.lookup_constant sp in let val_0 = Global.body_of_constant_body cb in - let typ = match cb.const_type with - | RegularArity t as x -> - begin match cb.const_universes with - | Monomorphic_const _ -> x + let typ = + match cb.const_universes with + | Monomorphic_const _ -> cb.const_type | Polymorphic_const univs -> let inst = Univ.AUContext.instance univs in - RegularArity (Vars.subst_instance_constr inst t) - end - | TemplateArity _ as x -> x + Vars.subst_instance_constr inst cb.const_type in - let typ = ungeneralized_type_of_constant_type typ in let univs = let otab = Global.opaque_tables () in match cb.const_body with @@ -698,7 +691,7 @@ let print_full_pure_context () = | "CONSTANT" -> let con = Global.constant_of_delta_kn kn in let cb = Global.lookup_constant con in - let typ = ungeneralized_type_of_constant_type cb.const_type in + let typ = cb.const_type in hov 0 ( match cb.const_body with | Undef _ -> diff --git a/printing/printmod.ml b/printing/printmod.ml index 5c7dcdc10..219eafda4 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -323,7 +323,7 @@ let print_body is_impl env mp (l,body) = str " :" ++ spc () ++ hov 0 (Printer.pr_ltype_env env sigma (Vars.subst_instance_constr u - (Typeops.type_of_constant_type env cb.const_type))) ++ + cb.const_type)) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index a949c8e91..193788558 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -157,10 +157,9 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce else { ce with const_entry_body = Future.chain ~pure:true ce.const_entry_body - (fun (pt, _) -> pt, Safe_typing.empty_private_constants) } in - let (cb, ctx), se = Future.force ce.const_entry_body in + (fun (pt, _) -> pt, ()) } in + let (cb, ctx), () = Future.force ce.const_entry_body in let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in - assert(Safe_typing.empty_private_constants = se); cb, status, Evd.evar_universe_context univs' let refine_by_tactic env sigma ty tac = diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 52d6787d4..2ade797f6 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -378,6 +378,10 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now let t = EConstr.Unsafe.to_constr t in let univstyp, body = make_body t p in let univs, typ = Future.force univstyp in + let univs = + if poly then Entries.Polymorphic_const_entry univs + else Entries.Monomorphic_const_entry univs + in { Entries. const_entry_body = body; const_entry_secctx = section_vars; @@ -386,7 +390,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now const_entry_inline_code = false; const_entry_opaque = true; const_entry_universes = univs; - const_entry_polymorphic = poly}) + }) fpl initial_goals in let binders = Option.map (fun names -> fst (Evd.universe_context ~names (Evd.from_ctx universes))) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 72e57a85b..5337565d3 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1143,7 +1143,7 @@ module Search = struct let res = if j = 0 then tclUNIT () else tclDISPATCH - (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j)))) + (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j')))) in let finish nestedshelf sigma = let filter ev = diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 0407c1e36..7f087ea01 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -123,14 +123,18 @@ let define internal id c p univs = let ctx = Evd.normalize_evar_universe_context univs in let c = Vars.subst_univs_fn_constr (Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in + let univs = Evd.evar_context_universe_context ctx in + let univs = + if p then Polymorphic_const_entry univs + else Monomorphic_const_entry univs + in let entry = { const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), Safe_typing.empty_private_constants); const_entry_secctx = None; const_entry_type = None; - const_entry_polymorphic = p; - const_entry_universes = Evd.evar_context_universe_context ctx; + const_entry_universes = univs; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8a95ad177..cb905e749 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5004,8 +5004,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = in let cst = Impargs.with_implicit_protection cst () in let lem = - if const.Entries.const_entry_polymorphic then - let uctx = Univ.ContextSet.of_context const.Entries.const_entry_universes in + match const.Entries.const_entry_universes with + | Entries.Polymorphic_const_entry uctx -> + let uctx = Univ.ContextSet.of_context uctx in (** Hack: the kernel may generate definitions whose universe variables are not the same as requested in the entry because of constraints delayed in the body, even in polymorphic mode. We mimick what it does for now @@ -5014,7 +5015,8 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let uctx = Univ.ContextSet.to_context (Univ.ContextSet.union uctx body_uctx) in let u = Univ.UContext.instance uctx in mkConstU (cst, EInstance.make u) - else mkConst cst + | Entries.Monomorphic_const_entry _ -> + mkConst cst in let evd = Evd.set_universe_context evd ectx in let open Safe_typing in diff --git a/test-suite/bugs/closed/4844.v b/test-suite/bugs/closed/4844.v new file mode 100644 index 000000000..f140939cc --- /dev/null +++ b/test-suite/bugs/closed/4844.v @@ -0,0 +1,47 @@ + +(* Bug report 4844 (and 4824): + The Haskell extraction was erroneously considering [Any] and + [()] as convertible ([Tunknown] an [Tdummy] internally). *) + +(* A value with inner logical parts. + Its extracted type will be [Sum () ()]. *) + +Definition semilogic : True + True := inl I. + +(* Higher-order record, whose projection [ST] isn't expressible + as an Haskell (or OCaml) type. Hence [ST] is extracted as the + unknown type [Any] in Haskell. *) + +Record SomeType := { ST : Type }. + +Definition SomeTrue := {| ST := True |}. + +(* A first version of the issue: + [abstrSum] is extracted as [Sum Any Any], so an unsafeCoerce + is required to cast [semilogic] into [abstrSum SomeTrue]. *) + +Definition abstrSum (t : SomeType) := ((ST t) + (ST t))%type. + +Definition semilogic' : abstrSum SomeTrue := semilogic. + +(* A deeper version of the issue. + In the previous example, the extraction could have reduced + [abstrSum SomeTrue] into [True+True], solving the issue. + It might do so in future versions. But if we put an inductive + in the way, a reduction isn't helpful. *) + +Inductive box (t : SomeType) := Box : ST t + ST t -> box t. + +Definition boxed_semilogic : box SomeTrue := + Box SomeTrue semilogic. + +Require Extraction. +Extraction Language Haskell. +Recursive Extraction semilogic' boxed_semilogic. +(* Warning! To fully check that this bug is still closed, + you should run ghc on the extracted code: + +Extraction "bug4844.hs" semilogic' boxed_semilogic. +ghc bug4844.hs + +*) diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out index 73369ab71..8b38fe0ff 100644 --- a/test-suite/output/TypeclassDebug.out +++ b/test-suite/output/TypeclassDebug.out @@ -1,18 +1,18 @@ Debug: 1: looking for foo without backtracking Debug: 1.1: simple apply H on foo, 1 subgoal(s) -Debug: 1.1-2 : foo -Debug: 1.1-2: looking for foo without backtracking -Debug: 1.1-2.1: simple apply H on foo, 1 subgoal(s) -Debug: 1.1-2.1-2 : foo -Debug: 1.1-2.1-2: looking for foo without backtracking -Debug: 1.1-2.1-2.1: simple apply H on foo, 1 subgoal(s) -Debug: 1.1-2.1-2.1-2 : foo -Debug: 1.1-2.1-2.1-2: looking for foo without backtracking -Debug: 1.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s) -Debug: 1.1-2.1-2.1-2.1-2 : foo -Debug: 1.1-2.1-2.1-2.1-2: looking for foo without backtracking -Debug: 1.1-2.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s) -Debug: 1.1-2.1-2.1-2.1-2.1-2 : foo +Debug: 1.1-1 : foo +Debug: 1.1-1: looking for foo without backtracking +Debug: 1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1 : foo +Debug: 1.1-1.1-1: looking for foo without backtracking +Debug: 1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1.1-1 : foo +Debug: 1.1-1.1-1.1-1: looking for foo without backtracking +Debug: 1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1.1-1.1-1 : foo +Debug: 1.1-1.1-1.1-1.1-1: looking for foo without backtracking +Debug: 1.1-1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s) +Debug: 1.1-1.1-1.1-1.1-1.1-1 : foo The command has indeed failed with message: Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed. Tactic failure: Proof search reached its limit. diff --git a/theories/Compat/Coq86.v b/theories/Compat/Coq86.v index f46460886..34061ddd6 100644 --- a/theories/Compat/Coq86.v +++ b/theories/Compat/Coq86.v @@ -7,5 +7,7 @@ (************************************************************************) (** Compatibility file for making Coq act similar to Coq v8.6 *) +Require Export Coq.Compat.Coq87. + Require Export Coq.extraction.Extraction. Require Export Coq.funind.FunInd. diff --git a/theories/Compat/Coq87.v b/theories/Compat/Coq87.v new file mode 100644 index 000000000..61e911678 --- /dev/null +++ b/theories/Compat/Coq87.v @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Compatibility file for making Coq act similar to Coq v8.7 *) diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index b1c0fdaa2..3e7664929 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -654,19 +654,19 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Lemma xelements_bits_lt_1 : forall p p0 q m v, List.In (p0,v) (xelements m (append p (xO q))) -> E.bits_lt p0 p. - Proof. + Proof using. intros. generalize (xelements_complete _ _ _ _ H); clear H; intros. - revert p0 q m v H. + revert p0 H. induction p; destruct p0; simpl; intros; eauto; try discriminate. Qed. Lemma xelements_bits_lt_2 : forall p p0 q m v, List.In (p0,v) (xelements m (append p (xI q))) -> E.bits_lt p p0. - Proof. + Proof using. intros. generalize (xelements_complete _ _ _ _ H); clear H; intros. - revert p0 q m v H. + revert p0 H. induction p; destruct p0; simpl; intros; eauto; try discriminate. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index ce49877e4..967b68d36 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -602,6 +602,14 @@ Proof. apply div_mod; order. Qed. +Lemma mod_div: forall a b, b~=0 -> + a mod b / b == 0. +Proof. + intros a b Hb. + rewrite div_small_iff by assumption. + auto using mod_always_pos. +Qed. + (** A last inequality: *) Theorem div_mul_le: diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index ca6197002..a9077127e 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -650,6 +650,14 @@ Proof. apply div_mod; order. Qed. +Lemma mod_div: forall a b, b~=0 -> + a mod b / b == 0. +Proof. + intros a b Hb. + rewrite div_small_iff by assumption. + auto using mod_bound_or. +Qed. + (** A last inequality: *) Theorem div_mul_le: diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index 46c36015d..bbb8ad5ae 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -622,6 +622,14 @@ Proof. apply quot_rem; order. Qed. +Lemma rem_quot: forall a b, b~=0 -> + a rem b รท b == 0. +Proof. + intros a b Hb. + rewrite quot_small_iff by assumption. + auto using rem_bound_abs. +Qed. + (** A last inequality: *) Theorem quot_mul_le: diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 55fc90f21..fa1ddf56f 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -508,6 +508,13 @@ Qed. (** Unfortunately, the previous result isn't always true on negative numbers. For instance: 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) *) +Lemma Zmod_div : forall a b, a mod b / b = 0. +Proof. + intros a b. + zero_or_not b. + auto using Z.mod_div. +Qed. + (** A last inequality: *) Theorem Zdiv_mult_le: diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index f61416dde..326ef5471 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -127,7 +127,8 @@ let init_ocaml_path () = List.iter add_subdir Coq_config.all_src_dirs let get_compat_version ?(allow_old = true) = function - | "8.7" -> Flags.Current + | "8.8" -> Flags.Current + | "8.7" -> Flags.V8_7 | "8.6" -> Flags.V8_6 | "8.5" -> Flags.V8_5 | ("8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 08c235023..515552fe7 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -209,6 +209,7 @@ let add_compat_require v = match v with | Flags.V8_5 -> add_require "Coq.Compat.Coq85" | Flags.V8_6 -> add_require "Coq.Compat.Coq86" + | Flags.V8_7 -> add_require "Coq.Compat.Coq87" | Flags.VOld | Flags.Current -> () let compile_list = ref ([] : (bool * string) list) @@ -613,6 +614,7 @@ let parse_args arglist = with any -> fatal_error any let init_toplevel arglist = + Profile.init_profile (); init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) let init_feeder = Feedback.add_feeder coqtop_init_feed in diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 86bbf46a3..6711b14da 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -311,10 +311,7 @@ let traverse current t = (** Hopefully bullet-proof function to recover the type of a constant. It just ignores all the universe stuff. There are many issues that can arise when considering terms out of any valid environment, so use with caution. *) -let type_of_constant cb = match cb.Declarations.const_type with -| Declarations.RegularArity ty -> ty -| Declarations.TemplateArity (ctx, arity) -> - Term.mkArity (ctx, Sorts.sort_of_univ arity.Declarations.template_level) +let type_of_constant cb = cb.Declarations.const_type let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t = let (idts, knst) = st in diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 3d97a767c..6ea8bc7f2 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -109,13 +109,17 @@ let _ = let define id internal ctx c t = let f = declare_constant ~internal in + let _, univs = Evd.universe_context ctx in + let univs = + if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs + else Monomorphic_const_entry univs + in let kn = f id (DefinitionEntry { const_entry_body = c; const_entry_secctx = None; const_entry_type = t; - const_entry_polymorphic = Flags.is_universe_polymorphism (); - const_entry_universes = snd (Evd.universe_context ctx); + const_entry_universes = univs; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None; diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 10d3317f8..28aeaa725 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -636,12 +636,12 @@ let declare_obligation prg obl body ty uctx = shrink_body body ty else [], body, ty, [||] in let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in + let univs = if poly then Polymorphic_const_entry uctx else Monomorphic_const_entry uctx in let ce = { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body; const_entry_secctx = None; const_entry_type = ty; - const_entry_polymorphic = poly; - const_entry_universes = uctx; + const_entry_universes = univs; const_entry_opaque = opaque; const_entry_inline_code = false; const_entry_feedback = None; @@ -818,8 +818,7 @@ let solve_by_tac name evi t poly ctx = id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps concl (Tacticals.New.tclCOMPLETE t) in let env = Global.env () in let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in - let body, eff = Future.force entry.const_entry_body in - assert(Safe_typing.empty_private_constants = eff); + let body, () = Future.force entry.const_entry_body in let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard (Global.env ()) (fst body); (fst body), entry.const_entry_type, Evd.evar_universe_context ctx' @@ -836,8 +835,7 @@ let obligation_terminator name num guard hook auto pf = let env = Global.env () in let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in let ty = entry.Entries.const_entry_type in - let (body, cstr), eff = Future.force entry.Entries.const_entry_body in - assert(Safe_typing.empty_private_constants = eff); + let (body, cstr), () = Future.force entry.Entries.const_entry_body in let sigma = Evd.from_ctx (fst uctx) in let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in Inductiveops.control_only_guard (Global.env ()) body; diff --git a/vernac/record.ml b/vernac/record.ml index 63ca22786..a2e443e5f 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -322,13 +322,16 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in try + let univs = + if poly then Polymorphic_const_entry ctx + else Monomorphic_const_entry ctx + in let entry = { const_entry_body = Future.from_val (Safe_typing.mk_pure_proof proj); const_entry_secctx = None; const_entry_type = Some projtyp; - const_entry_polymorphic = poly; - const_entry_universes = ctx; + const_entry_universes = univs; const_entry_opaque = false; const_entry_inline_code = false; const_entry_feedback = None } in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index c75ccf8de..959df89f6 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -257,7 +257,7 @@ let print_namespace ns = in let print_constant k body = (* FIXME: universes *) - let t = Typeops.type_of_constant_type (Global.env ()) body.Declarations.const_type in + let t = body.Declarations.const_type in print_kn k ++ str":" ++ spc() ++ Printer.pr_type t in let matches mp = match match_modulepath ns mp with |