diff options
45 files changed, 335 insertions, 1247 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index d9136ee24b..bac6ccd823 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -168,8 +168,6 @@ /plugins/syntax/ @ppedrot # Secondary maintainer @maximedenes -/plugins/quote/ @herbelin - /plugins/rtauto/ @PierreCorbineau # Secondary maintainer @herbelin diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 693a0b6bf0..0115ac9eff 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-08-27-V2" + CACHEKEY: "bionic_coq-V2018-09-05-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -275,7 +275,7 @@ doc:refman: dependencies: - build:base -doc:ml-api: +doc:ml-api:ocamldoc: stage: test dependencies: - build:edge @@ -287,6 +287,19 @@ doc:ml-api: paths: - dev/ocamldoc +doc:ml-api:odoc: + <<: *dune-template + stage: test + dependencies: + - build:egde:dune:dev + variables: + OPAM_SWITCH: edge + DUNE_TARGET: apidoc + artifacts: + name: "$CI_JOB_NAME" + paths: + - _build/default/_doc/ + test-suite:base: <<: *test-suite-template dependencies: @@ -1,3 +1,13 @@ +Changes beyond 8.9 +================== + +Plugins + +- The quote plugin (https://coq.inria.fr/distrib/V8.8.1/refman/proof-engine/detailed-tactic-examples.html#quote) + was removed. If some users are interested in maintaining this plugin + externally, the Coq development team can provide assistance for extracting + the plugin and setting up a new repository. + Changes from 8.8.2 to 8.9+beta1 =============================== @@ -50,8 +50,6 @@ plugins/nsatz developed by Loïc Pottier (INRIA-Marelle, 2009-2011) plugins/omega developed by Pierre Crégut (France Telecom R&D, 1996) -plugins/quote - developed by Patrick Loiseleur (LRI, 1997-1999) plugins/romega developed by Pierre Crégut (France Telecom R&D, 2001-2004) plugins/rtauto diff --git a/META.coq.in b/META.coq.in index e942267ad7..a7bf08ec49 100644 --- a/META.coq.in +++ b/META.coq.in @@ -325,24 +325,12 @@ package "plugins" ( archive(native) = "micromega_plugin.cmx" ) - package "quote" ( - - description = "Coq quote plugin" - version = "8.10" - - requires = "coq.plugins.ltac" - directory = "quote" - - archive(byte) = "quote_plugin.cmo" - archive(native) = "quote_plugin.cmx" - ) - package "newring" ( description = "Coq newring plugin" version = "8.10" - requires = "coq.plugins.quote" + requires = "" directory = "setoid_ring" archive(byte) = "newring_plugin.cmo" diff --git a/Makefile.common b/Makefile.common index 09457ced7b..69dea1d284 100644 --- a/Makefile.common +++ b/Makefile.common @@ -95,7 +95,7 @@ CORESRCDIRS:=\ tactics vernac stm toplevel PLUGINDIRS:=\ - omega romega micromega quote \ + omega romega micromega \ setoid_ring extraction \ cc funind firstorder derive \ rtauto nsatz syntax btauto \ @@ -131,7 +131,6 @@ GRAMMARCMA:=grammar/grammar.cma OMEGACMO:=plugins/omega/omega_plugin.cmo ROMEGACMO:=plugins/romega/romega_plugin.cmo MICROMEGACMO:=plugins/micromega/micromega_plugin.cmo -QUOTECMO:=plugins/quote/quote_plugin.cmo RINGCMO:=plugins/setoid_ring/newring_plugin.cmo NSATZCMO:=plugins/nsatz/nsatz_plugin.cmo EXTRACTIONCMO:=plugins/extraction/extraction_plugin.cmo @@ -152,7 +151,7 @@ SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo SSRCMO:=plugins/ssr/ssreflect_plugin.cmo PLUGINSCMO:=$(LTACCMO) $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \ - $(QUOTECMO) $(RINGCMO) \ + $(RINGCMO) \ $(EXTRACTIONCMO) \ $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \ $(FUNINDCMO) $(NSATZCMO) $(SYNTAXCMO) \ diff --git a/Makefile.dev b/Makefile.dev index 7fc1076a8f..2a7e61126a 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -171,7 +171,6 @@ noreal: unicode logic arith bool zarith qarith lists sets fsets \ OMEGAVO:=$(filter plugins/omega/%, $(PLUGINSVO)) ROMEGAVO:=$(filter plugins/romega/%, $(PLUGINSVO)) MICROMEGAVO:=$(filter plugins/micromega/%, $(PLUGINSVO)) -QUOTEVO:=$(filter plugins/quote/%, $(PLUGINSVO)) RINGVO:=$(filter plugins/setoid_ring/%, $(PLUGINSVO)) NSATZVO:=$(filter plugins/nsatz/%, $(PLUGINSVO)) FUNINDVO:=$(filter plugins/funind/%, $(PLUGINSVO)) diff --git a/Makefile.dune b/Makefile.dune index f90f555557..e04982650f 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -13,6 +13,7 @@ help: @echo " - states: build a minimal functional coqtop" @echo " - world: build all binaries and libraries" @echo " - release: build Coq in release mode" + @echo " - apidoc: build ML API documentation" @echo " - clean: remove build directory and autogenerated files" @echo " - help: show this message" @@ -29,6 +30,12 @@ world: voboot release: voboot dune build $(DUNEOPT) -p coq +apidoc: + # Ugly workaround for https://github.com/ocaml/odoc/issues/148 + mv checker/dune checker/dune.disabled || true + dune build $(DUNEOPT) @doc + mv checker/dune.disabled checker/dune || true + clean: dune clean diff --git a/dev/ci/README.md b/dev/ci/README.md index 95892ebe0a..3a179a9431 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -157,7 +157,7 @@ Currently available artifacts are: https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_install_ci/?job=build:base Additionally, an experimental Dune build is provided: - https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune + https://gitlab.com/coq/coq/-/jobs/artifacts/master/browse/_build/?job=build:edge:dune:dev - the Coq documentation, built in the `doc:*` jobs. When submitting a documentation PR, this can help reviewers checking the rendered result: @@ -167,7 +167,10 @@ Currently available artifacts are: + Coq's Standard Library Documentation [master branch] https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/html/stdlib/index.html?job=doc:refman + Coq's ML API Documentation [master branch] - https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/dev/ocamldoc/html/index.html?job=doc:ml-api + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/dev/ocamldoc/html/index.html?job=doc:ml-api:ocamldoc + + The dune job also provides its own API documentation using the newer `odoc` tool: + https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_build/default/_doc/_html/index.html?job=doc:ml-api:odoc ### GitLab and Windows diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 7a649591dd..8b26294d8f 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-08-27-V2" +# CACHEKEY: "bionic_coq-V2018-09-05-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -45,12 +45,13 @@ RUN opam switch -y -j $NJOBS "${COMPILER}+32bit" && eval $(opam config env) && \ # EDGE switch ENV COMPILER_EDGE="4.07.0" \ CAMLP5_VER_EDGE="7.06" \ - COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" + COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ + BASE_OPAM_EDGE="odoc.1.2.0 dune-release.0.3.0" RUN opam switch -y -j $NJOBS $COMPILER_EDGE && eval $(opam config env) && \ - opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE + opam install -j $NJOBS $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE # EDGE+flambda switch, we install CI_OPAM as to be able to use # `ci-template-flambda` with everything. RUN opam switch -y -j $NJOBS "${COMPILER_EDGE}+flambda" && eval $(opam config env) && \ - opam install -j $NJOBS $BASE_OPAM camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM + opam install -j $NJOBS $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE $CI_OPAM diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 98190b05b5..47cfeb98d7 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -2,7 +2,6 @@ open Format open Term open Constr open Names -open Cbytecodes open Cemitcodes open Vmvalues diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 35f45e2e0e..ac0f0f8ea6 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -605,7 +605,7 @@ Subtyping rules At the moment, we did not take into account one rule between universes which says that any term in a universe of index i is also a term in -the universe of index i+1 (this is the *cumulativity* rule of|Cic|). +the universe of index i+1 (this is the *cumulativity* rule of |Cic|). This property extends the equivalence relation of convertibility into a *subtyping* relation inductively defined by: @@ -640,7 +640,7 @@ a *subtyping* relation inductively defined by: respectively then .. math:: - E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t~w_1' … w_m' + E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t'~w_1' … w_m' (notice that :math:`t` and :math:`t'` are both fully applied, i.e., they have a sort as a type) if diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 72dd79d930..bd16b70d02 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -417,218 +417,8 @@ the optional tactic of the ``Hint Rewrite`` command. Qed. -.. _quote: - -quote ------ - -The tactic ``quote`` allows using Barendregt’s so-called 2-level approach -without writing any ML code. Suppose you have a language ``L`` of -'abstract terms' and a type ``A`` of 'concrete terms' and a function ``f : L -> A``. -If ``L`` is a simple inductive datatype and ``f`` a simple fixpoint, -``quote f`` will replace the head of current goal by a convertible term of -the form ``(f t)``. ``L`` must have a constructor of type: ``A -> L``. - -Here is an example: - -.. coqtop:: in reset - - Require Import Quote. - -.. coqtop:: all - - Parameters A B C : Prop. - -.. coqtop:: all - - Inductive formula : Type := - | f_and : formula -> formula -> formula (* binary constructor *) - | f_or : formula -> formula -> formula - | f_not : formula -> formula (* unary constructor *) - | f_true : formula (* 0-ary constructor *) - | f_const : Prop -> formula (* constructor for constants *). - -.. coqtop:: all - - Fixpoint interp_f (f:formula) : Prop := - match f with - | f_and f1 f2 => interp_f f1 /\ interp_f f2 - | f_or f1 f2 => interp_f f1 \/ interp_f f2 - | f_not f1 => ~ interp_f f1 - | f_true => True - | f_const c => c - end. - -.. coqtop:: all - - Goal A /\ (A \/ True) /\ ~ B /\ (A <-> A). - -.. coqtop:: all - - quote interp_f. - -The algorithm to perform this inversion is: try to match the term with -right-hand sides expression of ``f``. If there is a match, apply the -corresponding left-hand side and call yourself recursively on sub- -terms. If there is no match, we are at a leaf: return the -corresponding constructor (here ``f_const``) applied to the term. - -When ``quote`` is not able to perform inversion properly, it will error out with -:exn:`quote: not a simple fixpoint`. - - -Introducing variables map -~~~~~~~~~~~~~~~~~~~~~~~~~ - -The normal use of quote is to make proofs by reflection: one defines a -function ``simplify : formula -> formula`` and proves a theorem -``simplify_ok: (f:formula)(interp_f (simplify f)) -> (interp_f f)``. Then, -one can simplify formulas by doing: - -.. coqtop:: in - - quote interp_f. - apply simplify_ok. - compute. - -But there is a problem with leafs: in the example above one cannot -write a function that implements, for example, the logical -simplifications :math:`A \wedge A \rightarrow A` or :math:`A \wedge -\lnot A \rightarrow \mathrm{False}`. This is because ``Prop`` is -impredicative. - -It is better to use that type of formulas: - -.. coqtop:: in reset - - Require Import Quote. - -.. coqtop:: in - - Parameters A B C : Prop. - -.. coqtop:: all - - Inductive formula : Set := - | f_and : formula -> formula -> formula - | f_or : formula -> formula -> formula - | f_not : formula -> formula - | f_true : formula - | f_atom : index -> formula. - -``index`` is defined in module ``Quote``. Equality on that type is -decidable so we are able to simplify :math:`A \wedge A` into :math:`A` -at the abstract level. - -When there are variables, there are bindings, and ``quote`` also -provides a type ``(varmap A)`` of bindings from index to any set -``A``, and a function ``varmap_find`` to search in such maps. The -interpretation function also has another argument, a variables map: - -.. coqtop:: all - - Fixpoint interp_f (vm:varmap Prop) (f:formula) {struct f} : Prop := - match f with - | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2 - | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2 - | f_not f1 => ~ interp_f vm f1 - | f_true => True - | f_atom i => varmap_find True i vm - end. - -``quote`` handles this second case properly: - -.. coqtop:: all - - Goal A /\ (B \/ A) /\ (A \/ ~ B). - -.. coqtop:: all - - quote interp_f. - -It builds ``vm`` and ``t`` such that ``(f vm t)`` is convertible with the -conclusion of current goal. - - -Combining variables and constants -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -One can have both variables and constants in abstracts terms; for -example, this is the case for the :tacn:`ring` tactic. Then one must provide to -``quote`` a list of *constructors of constants*. For example, if the list -is ``[O S]`` then closed natural numbers will be considered as constants -and other terms as variables. - -.. coqtop:: in reset - - Require Import Quote. - -.. coqtop:: in - - Parameters A B C : Prop. - -.. coqtop:: in - - Inductive formula : Type := - | f_and : formula -> formula -> formula - | f_or : formula -> formula -> formula - | f_not : formula -> formula - | f_true : formula - | f_const : Prop -> formula (* constructor for constants *) - | f_atom : index -> formula. - -.. coqtop:: in - - Fixpoint interp_f (vm:varmap Prop) (f:formula) {struct f} : Prop := - match f with - | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2 - | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2 - | f_not f1 => ~ interp_f vm f1 - | f_true => True - | f_const c => c - | f_atom i => varmap_find True i vm - end. - -.. coqtop:: in - - Goal A /\ (A \/ True) /\ ~ B /\ (C <-> C). - -.. coqtop:: all - - quote interp_f [ A B ]. - - -.. coqtop:: all - - Undo. - -.. coqtop:: all - - quote interp_f [ B C iff ]. - -.. warning:: - Since functional inversion is undecidable in the general case, - don’t expect miracles from it! - -.. tacv:: quote @ident in @term using @tactic - - ``tactic`` must be a functional tactic (starting with ``fun x =>``) and - will be called with the quoted version of term according to ``ident``. - -.. tacv:: quote @ident [{+ @ident}] in @term using @tactic - - Same as above, but will use the additional ``ident`` list to chose - which subterms are constants (see above). - -.. seealso:: - Comments from the source file ``plugins/quote/quote.ml`` - -.. seealso:: - The :tacn:`ring` tactic. - - Using the tactic language ---------------------------- +------------------------- About the cardinality of the set of natural numbers diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 62a482096c..fb121c82ec 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4217,26 +4217,6 @@ available after a ``Require Import FunInd``. functional inversion, this variant allows choosing which :n:`@qualid` is inverted. -.. tacn:: quote @ident - :name: quote - -This kind of inversion has nothing to do with the tactic :tacn:`inversion` -above. This tactic does :g:`change (@ident t)`, where `t` is a term built in -order to ensure the convertibility. In other words, it does inversion of the -function :n:`@ident`. This function must be a fixpoint on a simple recursive -datatype: see :ref:`quote` for the full details. - - -.. exn:: quote: not a simple fixpoint. - - Happens when quote is not able to perform inversion properly. - - -.. tacv:: quote @ident {* @ident} - - All terms that are built only with :n:`{* @ident}` will be considered by quote - as constants rather than variables. - Classical tactics ----------------- diff --git a/interp/declare.ml b/interp/declare.ml index a82e6b35a6..22e6cf9d1c 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -39,7 +39,6 @@ type constant_obj = { 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; } @@ -94,28 +93,20 @@ let cache_constant ((sp,kn), obj) = Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn)); let cst = Global.lookup_constant kn' in add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps; - Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; add_constant_kind (Constant.make1 kn) obj.cst_kind -let discharged_hyps kn sechyps = - let (_,dir,_) = KerName.repr kn in - let args = Array.to_list (instance_from_variable_context sechyps) in - List.rev_map (Libnames.make_path dir) args - let discharge_constant ((sp, kn), obj) = let con = Constant.make1 kn in let from = Global.lookup_constant con in let modlist = replacement_context () in let { abstr_ctx = hyps; abstr_subst = subst; abstr_uctx = uctx } = section_segment_of_constant con in - 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 = Some new_decl; } + Some { obj with cst_decl = Some new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant cst = { cst_decl = None; - cst_hyps = []; cst_kind = cst.cst_kind; cst_locl = cst.cst_locl; } @@ -142,7 +133,6 @@ let update_tables c = let register_side_effect (c, role) = let o = inConstant { cst_decl = None; - cst_hyps = [] ; cst_kind = IsProof Theorem; cst_locl = false; } in @@ -194,7 +184,6 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e let () = List.iter register_side_effect export in let cst = { cst_decl = Some decl; - cst_hyps = [] ; cst_kind = kind; cst_locl = local; } in @@ -255,7 +244,6 @@ let cache_variable ((sp,_),o) = 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 []; add_variable_data id (p,opaq,ctx,poly,mk) let discharge_variable (_,o) = match o with @@ -311,15 +299,15 @@ let inductive_names sp kn mie = ([], 0) mie.mind_entry_inds in names -let load_inductive i ((sp,kn),(_,mie)) = +let load_inductive i ((sp,kn),mie) = let names = inductive_names sp kn mie in List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until i) sp ref ) names -let open_inductive i ((sp,kn),(_,mie)) = +let open_inductive i ((sp,kn),mie) = let names = inductive_names sp kn mie in List.iter (fun (sp, ref) -> Nametab.push (Nametab.Exactly i) sp ref) names -let cache_inductive ((sp,kn),(dhyps,mie)) = +let cache_inductive ((sp,kn),mie) = let names = inductive_names sp kn mie in List.iter check_exists (List.map fst names); let id = basename sp in @@ -328,17 +316,14 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = assert (MutInd.equal kn' (MutInd.make1 kn)); let mind = Global.lookup_mind kn' in add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps; - Dischargedhypsmap.set_discharged_hyps sp dhyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names -let discharge_inductive ((sp,kn),(dhyps,mie)) = +let discharge_inductive ((sp,kn),mie) = let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in let repl = replacement_context () in let info = section_segment_of_mutual_inductive mind in - let sechyps = info.Lib.abstr_ctx in - Some (discharged_hyps kn sechyps, - Discharge.process_inductive info repl mie) + Some (Discharge.process_inductive info repl mie) let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; @@ -349,30 +334,28 @@ let dummy_one_inductive_entry mie = { } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_inductive_entry (_,m) = ([],{ +let dummy_inductive_entry m = { mind_entry_params = []; mind_entry_record = None; mind_entry_finite = Declarations.BiFinite; mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty; mind_entry_private = None; -}) +} (* reinfer subtyping constraints for inductive after section is dischared. *) -let infer_inductive_subtyping (pth, mind_ent) = +let infer_inductive_subtyping mind_ent = match mind_ent.mind_entry_universes with | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> - (pth, mind_ent) + mind_ent | Cumulative_ind_entry cumi -> begin let env = Global.env () in (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) - (pth, InferCumulativity.infer_inductive env mind_ent) + InferCumulativity.infer_inductive env mind_ent end -type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry - -let inInductive : inductive_obj -> obj = +let inInductive : mutual_inductive_entry -> obj = declare_object {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; @@ -426,7 +409,7 @@ let declare_mind mie = let id = match mie.mind_entry_inds with | ind::_ -> ind.mind_entry_typename | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in - let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in + let (sp,kn as oname) = add_leaf id (inInductive mie) in let mind = Global.mind_of_delta_kn kn in let isprim = declare_projections mie.mind_entry_universes mind in declare_mib_implicits mind; diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 9a1224aab2..ed3bd866a4 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -15,78 +15,7 @@ (* This file defines the type of bytecode instructions *) open Names -open Constr - -type tag = int - -let accu_tag = 0 - -let type_atom_tag = 2 -let max_atom_tag = 2 -let proj_tag = 3 -let fix_app_tag = 4 -let switch_tag = 5 -let cofix_tag = 6 -let cofix_evaluated_tag = 7 - -(* It would be great if OCaml exported this value, - So fixme if this happens in a new version of OCaml *) -let last_variant_tag = 245 - -type structured_constant = - | Const_sort of Sorts.t - | Const_ind of inductive - | Const_b0 of tag - | Const_bn of tag * structured_constant array - | Const_univ_level of Univ.Level.t - -type reloc_table = (tag * int) array - -type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} - -let rec eq_structured_constant c1 c2 = match c1, c2 with -| Const_sort s1, Const_sort s2 -> Sorts.equal s1 s2 -| Const_sort _, _ -> false -| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 -| Const_ind _, _ -> false -| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 -| Const_b0 _, _ -> false -| Const_bn (t1, a1), Const_bn (t2, a2) -> - Int.equal t1 t2 && CArray.equal eq_structured_constant a1 a2 -| Const_bn _, _ -> false -| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 -| Const_univ_level _ , _ -> false - -let rec hash_structured_constant c = - let open Hashset.Combine in - match c with - | Const_sort s -> combinesmall 1 (Sorts.hash s) - | Const_ind i -> combinesmall 2 (ind_hash i) - | Const_b0 t -> combinesmall 3 (Int.hash t) - | Const_bn (t, a) -> - let fold h c = combine h (hash_structured_constant c) in - let h = Array.fold_left fold 0 a in - combinesmall 4 (combine (Int.hash t) h) - | Const_univ_level l -> combinesmall 5 (Univ.Level.hash l) - -let eq_annot_switch asw1 asw2 = - let eq_ci ci1 ci2 = - eq_ind ci1.ci_ind ci2.ci_ind && - Int.equal ci1.ci_npar ci2.ci_npar && - CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls - in - let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in - eq_ci asw1.ci asw2.ci && - CArray.equal eq_rlc asw1.rtbl asw2.rtbl && - (asw1.tailcall : bool) == asw2.tailcall - -let hash_annot_switch asw = - let open Hashset.Combine in - let h1 = Constr.case_info_hash asw.ci in - let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in - let h3 = if asw.tailcall then 1 else 0 in - combine3 h1 h2 h3 +open Vmvalues module Label = struct @@ -232,21 +161,6 @@ type comp_env = { open Pp open Util -let pp_sort s = - let open Sorts in - match s with - | Prop -> str "Prop" - | Set -> str "Set" - | Type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}" - -let rec pp_struct_const = function - | Const_sort s -> pp_sort s - | Const_ind (mind, i) -> MutInd.print mind ++ str"#" ++ int i - | Const_b0 i -> int i - | Const_bn (i,t) -> - int i ++ surround (prvect_with_sep pr_comma pp_struct_const t) - | Const_univ_level l -> Univ.Level.pr l - let pp_lbl lbl = str "L" ++ int lbl let pp_fv_elem = function diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index f17a1e657e..9c04c166a2 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -11,41 +11,7 @@ (* $Id$ *) open Names -open Constr - -type tag = int - -val accu_tag : tag - -val type_atom_tag : tag -val max_atom_tag : tag -val proj_tag : tag -val fix_app_tag : tag -val switch_tag : tag -val cofix_tag : tag -val cofix_evaluated_tag : tag - -val last_variant_tag : tag - -type structured_constant = - | Const_sort of Sorts.t - | Const_ind of inductive - | Const_b0 of tag - | Const_bn of tag * structured_constant array - | Const_univ_level of Univ.Level.t - -val pp_struct_const : structured_constant -> Pp.t - -type reloc_table = (tag * int) array - -type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} - -val eq_structured_constant : structured_constant -> structured_constant -> bool -val hash_structured_constant : structured_constant -> int - -val eq_annot_switch : annot_switch -> annot_switch -> bool -val hash_annot_switch : annot_switch -> int +open Vmvalues module Label : sig diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index e336ea922d..5362f9a814 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -14,6 +14,7 @@ open Util open Names +open Vmvalues open Cbytecodes open Cemitcodes open Cinstr @@ -395,17 +396,17 @@ let init_fun_code () = fun_code := [] (* If [tag] hits the OCaml limitation for non constant constructors, we switch to another representation for the remaining constructors: -[last_variant_tag|tag - last_variant_tag|args] +[last_variant_tag|tag - Obj.last_non_constant_constructor_tag|args] -We subtract last_variant_tag for efficiency of match interpretation. +We subtract Obj.last_non_constant_constructor_tag for efficiency of match interpretation. *) let nest_block tag arity cont = - Kconst (Const_b0 (tag - last_variant_tag)) :: - Kmakeblock(arity+1, last_variant_tag) :: cont + Kconst (Const_b0 (tag - Obj.last_non_constant_constructor_tag)) :: + Kmakeblock(arity+1, Obj.last_non_constant_constructor_tag) :: cont let code_makeblock ~stack_size ~arity ~tag cont = - if tag < last_variant_tag then + if tag < Obj.last_non_constant_constructor_tag then Kmakeblock(arity, tag) :: cont else begin set_max_stack_size (stack_size + 1); @@ -490,7 +491,9 @@ let rec compile_lam env cenv lam sz cont = match lam with | Lrel(_, i) -> pos_rel i cenv sz :: cont - | Lval v -> compile_structured_constant cenv v sz cont + | Lint i -> compile_structured_constant cenv (Const_b0 i) sz cont + + | Lval v -> compile_structured_constant cenv (Const_val v) sz cont | Lproj (p,arg) -> compile_lam env cenv arg sz (Kproj p :: cont) @@ -634,9 +637,9 @@ let rec compile_lam env cenv lam sz cont = let lbl_consts = Array.make oib.mind_nb_constant Label.no in let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *) let nconst = Array.length branches.constant_branches in - let nblock = min nallblock (last_variant_tag + 1) in + let nblock = min nallblock (Obj.last_non_constant_constructor_tag + 1) in let lbl_blocks = Array.make nblock Label.no in - let neblock = max 0 (nallblock - last_variant_tag) in + let neblock = max 0 (nallblock - Obj.last_non_constant_constructor_tag) in let lbl_eblocks = Array.make neblock Label.no in let branch1, cont = make_branch cont in (* Compilation of the return type *) @@ -662,7 +665,7 @@ let rec compile_lam env cenv lam sz cont = let lbl_b, code_b = label_code ( Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in - lbl_blocks.(last_variant_tag) <- lbl_b; + lbl_blocks.(Obj.last_non_constant_constructor_tag) <- lbl_b; c := code_b end; @@ -684,7 +687,7 @@ let rec compile_lam env cenv lam sz cont = compile_lam env (push_param arity sz_b cenv) body (sz_b+arity) (add_pop arity (branch::!c)) in let code_b = - if tag < last_variant_tag then begin + if tag < Obj.last_non_constant_constructor_tag then begin set_max_stack_size (sz_b + arity); Kpushfields arity :: code_b end @@ -694,8 +697,8 @@ let rec compile_lam env cenv lam sz cont = end in let lbl_b, code_b = label_code code_b in - if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b - else lbl_eblocks.(tag - last_variant_tag) <- lbl_b; + if tag < Obj.last_non_constant_constructor_tag then lbl_blocks.(tag) <- lbl_b + else lbl_eblocks.(tag - Obj.last_non_constant_constructor_tag) <- lbl_b; c := code_b done; diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index ca24f9b689..50f5607e31 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -14,6 +14,7 @@ open Names open Constr +open Vmvalues open Cbytecodes open Copcodes open Mod_subst @@ -357,10 +358,9 @@ let rec emit env insns remaining = match insns with type to_patch = emitcodes * patches * fv (* Substitution *) -let rec subst_strcst s sc = +let subst_strcst s sc = match sc with - | Const_sort _ | Const_b0 _ | Const_univ_level _ -> sc - | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) + | Const_sort _ | Const_b0 _ | Const_univ_level _ | Const_val _ -> sc | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) let subst_reloc s ri = diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 9009926bdb..39ddf4a047 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -1,4 +1,5 @@ open Names +open Vmvalues open Cbytecodes type reloc_info = diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli index 171ca38830..dca1757b7d 100644 --- a/kernel/cinstr.mli +++ b/kernel/cinstr.mli @@ -9,6 +9,7 @@ (************************************************************************) open Names open Constr +open Vmvalues open Cbytecodes (** This file defines the lambda code for the bytecode compiler. It has been @@ -33,10 +34,11 @@ and lambda = | Lfix of (int array * int) * fix_decl | Lcofix of int * fix_decl (* must be in eta-expanded form *) | Lmakeblock of int * lambda array - | Lval of structured_constant + | Lval of structured_values | Lsort of Sorts.t | Lind of pinductive | Lproj of Projection.Repr.t * lambda + | Lint of int | Luint of uint (* Cofixpoints have to be in eta-expanded form for their call-by-need evaluation diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 75cf6b747d..31dede6f5d 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -4,6 +4,7 @@ open Esubst open Term open Constr open Declarations +open Vmvalues open Cbytecodes open Cinstr open Environ @@ -115,6 +116,8 @@ let rec pp_lam lam = hov 1 (str "(proj " ++ Projection.Repr.print p ++ str "(" ++ pp_lam arg ++ str ")") + | Lint i -> + Pp.(str "(int:" ++ int i ++ str ")") | Luint _ -> str "(uint)" @@ -150,7 +153,7 @@ let shift subst = subs_shft (1, subst) let rec map_lam_with_binders g f n lam = match lam with - | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> lam + | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ -> lam | Levar (evk, args) -> let args' = Array.Smart.map (f n) args in if args == args' then lam else Levar (evk, args') @@ -349,7 +352,7 @@ let rec occurrence k kind lam = if n = k then if kind then false else raise Not_found else kind - | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> kind + | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Lint _ -> kind | Levar (_, args) -> occurrence_args k kind args | Lprod(dom, codom) -> @@ -419,7 +422,7 @@ let rec remove_let subst lam = exception TooLargeInductive of Pp.t let max_nb_const = 0x1000000 -let max_nb_block = 0x1000000 + last_variant_tag - 1 +let max_nb_block = 0x1000000 + Obj.last_non_constant_constructor_tag - 1 let str_max_constructors = Format.sprintf @@ -436,23 +439,22 @@ let check_compilable ib = let is_value lc = match lc with - | Lval _ -> true + | Lval _ | Lint _ -> true | _ -> false let get_value lc = match lc with | Lval v -> v + | Lint i -> val_of_int i | _ -> raise Not_found -let mkConst_b0 n = Lval (Cbytecodes.Const_b0 n) - let make_args start _end = Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i)) (* Translation of constructors *) let expand_constructor tag nparams arity = let ids = Array.make (nparams + arity) Anonymous in - if arity = 0 then mkLlam ids (mkConst_b0 tag) + if arity = 0 then mkLlam ids (Lint tag) else let args = make_args arity 1 in Llam(ids, Lmakeblock (tag, args)) @@ -463,15 +465,15 @@ let makeblock tag nparams arity args = mkLapp (expand_constructor tag nparams arity) args else (* The constructor is fully applied *) - if arity = 0 then mkConst_b0 tag + if arity = 0 then Lint tag else if Array.for_all is_value args then - if tag < last_variant_tag then - Lval(Cbytecodes.Const_bn(tag, Array.map get_value args)) + if tag < Obj.last_non_constant_constructor_tag then + Lval(val_of_block tag (Array.map get_value args)) else let args = Array.map get_value args in - let args = Array.append [|Cbytecodes.Const_b0 (tag - last_variant_tag) |] args in - Lval(Cbytecodes.Const_bn(last_variant_tag, args)) + let args = Array.append [| val_of_int (tag - Obj.last_non_constant_constructor_tag) |] args in + Lval(val_of_block Obj.last_non_constant_constructor_tag args) else Lmakeblock(tag, args) @@ -835,10 +837,11 @@ let dynamic_int31_compilation fc args = if not fc then raise Not_found else Luint (UintDigits args) +let d0 = Lint 0 +let d1 = Lint 1 + (* We are relying here on the tags of digits constructors *) let digits_from_uint i = - let d0 = mkConst_b0 0 in - let d1 = mkConst_b0 1 in let digits = Array.make 31 d0 in for k = 0 to 30 do if Int.equal ((Uint31.to_int i lsr k) land 1) 1 then diff --git a/kernel/constr.mli b/kernel/constr.mli index 9cc044316b..ea38dabd5c 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -285,8 +285,8 @@ val destMeta : constr -> metavariable (** Destructs a variable *) val destVar : constr -> Id.t -(** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether - [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *) +(** Destructs a sort. [is_Prop] recognizes the sort [Prop], whether + [isprop] recognizes both [Prop] and [Set]. *) val destSort : constr -> Sorts.t (** Destructs a casted term *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 1d49550442..61fcb4832a 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -164,7 +164,7 @@ type one_inductive_body = { mind_nb_args : int; (** number of no constant constructor *) - mind_reloc_tbl : Cbytecodes.reloc_table; + mind_reloc_tbl : Vmvalues.reloc_table; } type abstract_inductive_universes = diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 07a02f6ef5..a18c5d1e20 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -10,13 +10,13 @@ Constr Vars Term Mod_subst +Vmvalues Cbytecodes Copcodes Cemitcodes Opaqueproof Declarations Entries -Vmvalues Nativevalues CPrimitives Declareops diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 9c6ef64b50..3fd40a7f42 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -12,7 +12,7 @@ open Names open Constr open Environ -(** Type errors. {% \label{%}typeerrors{% }%} *) +(** Type errors. {% \label{typeerrors} %} *) (*i Rem: NotEnoughAbstractionInFixBody should only occur with "/i" Fix notation i*) diff --git a/kernel/vm.ml b/kernel/vm.ml index d7eedc226c..9917e94a35 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Cbytecodes open Vmvalues external set_drawinstr : unit -> unit = "coq_set_drawinstr" diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index d6d9312938..8edd49f77f 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -9,8 +9,8 @@ (************************************************************************) open Names open Sorts -open Cbytecodes open Univ +open Constr (*******************************************) (* Initalization of the abstract machine ***) @@ -25,11 +25,124 @@ let _ = init_vm () (* Abstract data types and utility functions **********) (******************************************************) +(* The representation of values relies on this assertion *) +let _ = assert (Int.equal Obj.first_non_constant_constructor_tag 0) + (* Values of the abstract machine *) type values +type structured_values = values let val_of_obj v = ((Obj.obj v):values) let crazy_val = (val_of_obj (Obj.repr 0)) +type tag = int + +let accu_tag = 0 + +let type_atom_tag = 2 +let max_atom_tag = 2 +let proj_tag = 3 +let fix_app_tag = 4 +let switch_tag = 5 +let cofix_tag = 6 +let cofix_evaluated_tag = 7 + +(** Structured constants are constants whose construction is done once. Their +occurrences share the same value modulo kernel name substitutions (for functor +application). Structured values have the additional property that no +substitution will need to be performed, so their runtime value can directly be +shared without reallocating a more structured representation. *) +type structured_constant = + | Const_sort of Sorts.t + | Const_ind of inductive + | Const_b0 of tag + | Const_univ_level of Univ.Level.t + | Const_val of structured_values + +type reloc_table = (tag * int) array + +type annot_switch = + {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} + +let rec eq_structured_values v1 v2 = + v1 == v2 || + let o1 = Obj.repr v1 in + let o2 = Obj.repr v2 in + if Obj.is_int o1 && Obj.is_int o2 then o1 == o2 + else + let t1 = Obj.tag o1 in + let t2 = Obj.tag o2 in + if Int.equal t1 t2 && + Int.equal (Obj.size o1) (Obj.size o2) + then begin + assert (t1 <= Obj.last_non_constant_constructor_tag && + t2 <= Obj.last_non_constant_constructor_tag); + let i = ref 0 in + while (!i < Obj.size o1 && eq_structured_values + (Obj.magic (Obj.field o1 !i) : structured_values) + (Obj.magic (Obj.field o2 !i) : structured_values)) do + incr i + done; + !i >= Obj.size o1 + end + else false + +let hash_structured_values (v : structured_values) = + (* We may want a better hash function here *) + Hashtbl.hash v + +let eq_structured_constant c1 c2 = match c1, c2 with +| Const_sort s1, Const_sort s2 -> Sorts.equal s1 s2 +| Const_sort _, _ -> false +| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 +| Const_ind _, _ -> false +| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 +| Const_b0 _, _ -> false +| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 +| Const_univ_level _ , _ -> false +| Const_val v1, Const_val v2 -> eq_structured_values v1 v2 +| Const_val v1, _ -> false + +let hash_structured_constant c = + let open Hashset.Combine in + match c with + | Const_sort s -> combinesmall 1 (Sorts.hash s) + | Const_ind i -> combinesmall 2 (ind_hash i) + | Const_b0 t -> combinesmall 3 (Int.hash t) + | Const_univ_level l -> combinesmall 4 (Univ.Level.hash l) + | Const_val v -> combinesmall 5 (hash_structured_values v) + +let eq_annot_switch asw1 asw2 = + let eq_ci ci1 ci2 = + eq_ind ci1.ci_ind ci2.ci_ind && + Int.equal ci1.ci_npar ci2.ci_npar && + CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls + in + let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in + eq_ci asw1.ci asw2.ci && + CArray.equal eq_rlc asw1.rtbl asw2.rtbl && + (asw1.tailcall : bool) == asw2.tailcall + +let hash_annot_switch asw = + let open Hashset.Combine in + let h1 = Constr.case_info_hash asw.ci in + let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in + let h3 = if asw.tailcall then 1 else 0 in + combine3 h1 h2 h3 + +let pp_sort s = + let open Sorts in + match s with + | Prop -> Pp.str "Prop" + | Set -> Pp.str "Set" + | Type u -> Pp.(str "Type@{" ++ Univ.pr_uni u ++ str "}") + +let pp_struct_const = function + | Const_sort s -> pp_sort s + | Const_ind (mind, i) -> Pp.(MutInd.print mind ++ str"#" ++ int i) + | Const_b0 i -> Pp.int i + | Const_univ_level l -> Univ.Level.pr l + | Const_val _ -> Pp.str "(value)" + (* Abstract data *) type vprod type vfun @@ -293,19 +406,21 @@ let obj_of_atom : atom -> Obj.t = res (* obj_of_str_const : structured_constant -> Obj.t *) -let rec obj_of_str_const str = +let obj_of_str_const str = match str with | Const_sort s -> obj_of_atom (Asort s) | Const_ind ind -> obj_of_atom (Aind ind) | Const_b0 tag -> Obj.repr tag - | Const_bn(tag, args) -> - let len = Array.length args in - let res = Obj.new_block tag len in - for i = 0 to len - 1 do - Obj.set_field res i (obj_of_str_const args.(i)) - done; - res | Const_univ_level l -> Obj.repr (Vuniv_level l) + | Const_val v -> Obj.repr v + +let val_of_block tag (args : structured_values array) = + let nargs = Array.length args in + let r = Obj.new_block tag nargs in + for i = 0 to nargs - 1 do + Obj.set_field r i (Obj.repr args.(i)) + done; + (Obj.magic r : structured_values) let val_of_obj o = ((Obj.obj o) : values) @@ -313,6 +428,8 @@ let val_of_str_const str = val_of_obj (obj_of_str_const str) let val_of_atom a = val_of_obj (obj_of_atom a) +let val_of_int i = (Obj.magic i : values) + let atom_of_proj kn v = let r = Obj.new_block proj_tag 2 in Obj.set_field r 0 (Obj.repr kn); @@ -514,10 +631,10 @@ let branch_arg k (tag,arity) = if Int.equal arity 0 then ((Obj.magic tag):values) else let b, ofs = - if tag < last_variant_tag then Obj.new_block tag arity, 0 + if tag < Obj.last_non_constant_constructor_tag then Obj.new_block tag arity, 0 else - let b = Obj.new_block last_variant_tag (arity+1) in - Obj.set_field b 0 (Obj.repr (tag-last_variant_tag)); + let b = Obj.new_block Obj.last_non_constant_constructor_tag (arity+1) in + Obj.set_field b 0 (Obj.repr (tag-Obj.last_non_constant_constructor_tag)); b,1 in for i = ofs to ofs + arity - 1 do Obj.set_field b i (Obj.repr (val_of_rel (k+i))) diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 6eedcf1d37..ae1d416ed5 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -9,11 +9,12 @@ (************************************************************************) open Names -open Cbytecodes +open Constr (** Values *) type values +type structured_values type vm_env type vm_global type vprod @@ -25,6 +26,38 @@ type arguments type vstack = values array type to_update +type tag = int + +val accu_tag : tag + +val type_atom_tag : tag +val max_atom_tag : tag +val proj_tag : tag +val fix_app_tag : tag +val switch_tag : tag +val cofix_tag : tag +val cofix_evaluated_tag : tag + +type structured_constant = + | Const_sort of Sorts.t + | Const_ind of inductive + | Const_b0 of tag + | Const_univ_level of Univ.Level.t + | Const_val of structured_values + +val pp_struct_const : structured_constant -> Pp.t + +type reloc_table = (tag * int) array + +type annot_switch = + {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} + +val eq_structured_constant : structured_constant -> structured_constant -> bool +val hash_structured_constant : structured_constant -> int + +val eq_annot_switch : annot_switch -> annot_switch -> bool +val hash_annot_switch : annot_switch -> int + val fun_val : vfun -> values val fix_val : vfix -> values val cofix_upd_val : to_update -> values @@ -110,6 +143,8 @@ val val_of_constant : Constant.t -> values val val_of_evar : Evar.t -> values val val_of_proj : Projection.Repr.t -> values -> values val val_of_atom : atom -> values +val val_of_int : int -> structured_values +val val_of_block : tag -> structured_values array -> structured_values external val_of_annot_switch : annot_switch -> values = "%identity" external val_of_proj_name : Projection.Repr.t -> values = "%identity" @@ -158,4 +193,4 @@ val bfield : vblock -> int -> values (** Switch *) val check_switch : vswitch -> vswitch -> bool -val branch_arg : int -> Cbytecodes.tag * int -> values +val branch_arg : int -> tag * int -> values diff --git a/lib/genarg.mli b/lib/genarg.mli index bb85f99e3c..52db3df088 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -13,7 +13,7 @@ (** The route of a generic argument, from parsing to evaluation. In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. -{% \begin{%}verbatim{% }%} +{% \begin{verbatim} %} parsing in_raw out_raw char stream ---> raw_object ---> raw_object generic_argument -------+ encapsulation decaps| @@ -36,7 +36,7 @@ In the following diagram, "object" can be tactic_expr, constr, tactic_arg, etc. | V effective use -{% \end{%}verbatim{% }%} +{% \end{verbatim} %} To distinguish between the uninterpreted, globalized and interpreted worlds, we annotate the type [generic_argument] by a diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml deleted file mode 100644 index abcdb93a27..0000000000 --- a/library/dischargedhypsmap.ml +++ /dev/null @@ -1,21 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Libnames - -type discharged_hyps = full_path list - -let discharged_hyps_map = Summary.ref Spmap.empty ~name:"discharged_hypothesis" - -let set_discharged_hyps sp hyps = - discharged_hyps_map := Spmap.add sp hyps !discharged_hyps_map - -let get_discharged_hyps sp = - try Spmap.find sp !discharged_hyps_map with Not_found -> [] diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli deleted file mode 100644 index c70677225b..0000000000 --- a/library/dischargedhypsmap.mli +++ /dev/null @@ -1,19 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Libnames - -type discharged_hyps = full_path list - -(** Discharged hypothesis. Here we store the discharged hypothesis of each - constant or inductive type declaration. *) - -val set_discharged_hyps : full_path -> discharged_hyps -> unit -val get_discharged_hyps : full_path -> discharged_hyps diff --git a/library/library.mllib b/library/library.mllib index 9cacaba4a7..8f694f4a31 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -11,7 +11,6 @@ Loadpath Library States Kindops -Dischargedhypsmap Goptions Decls Keys diff --git a/plugins/quote/Quote.v b/plugins/quote/Quote.v deleted file mode 100644 index 2d3d9170c1..0000000000 --- a/plugins/quote/Quote.v +++ /dev/null @@ -1,86 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -Declare ML Module "quote_plugin". - -(*********************************************************************** - The "abstract" type index is defined to represent variables. - - index : Set - index_eq : index -> bool - index_eq_prop: (n,m:index)(index_eq n m)=true -> n=m - index_lt : index -> bool - varmap : Type -> Type. - varmap_find : (A:Type)A -> index -> (varmap A) -> A. - - The first arg. of varmap_find is the default value to take - if the object is not found in the varmap. - - index_lt defines a total well-founded order, but we don't prove that. - -***********************************************************************) - -Set Implicit Arguments. - -Section variables_map. - -Variable A : Type. - -Inductive varmap : Type := - | Empty_vm : varmap - | Node_vm : A -> varmap -> varmap -> varmap. - -Inductive index : Set := - | Left_idx : index -> index - | Right_idx : index -> index - | End_idx : index. - -Fixpoint varmap_find (default_value:A) (i:index) (v:varmap) {struct v} : A := - match i, v with - | End_idx, Node_vm x _ _ => x - | Right_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v2 - | Left_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v1 - | _, _ => default_value - end. - -Fixpoint index_eq (n m:index) {struct m} : bool := - match n, m with - | End_idx, End_idx => true - | Left_idx n', Left_idx m' => index_eq n' m' - | Right_idx n', Right_idx m' => index_eq n' m' - | _, _ => false - end. - -Fixpoint index_lt (n m:index) {struct m} : bool := - match n, m with - | End_idx, Left_idx _ => true - | End_idx, Right_idx _ => true - | Left_idx n', Right_idx m' => true - | Right_idx n', Right_idx m' => index_lt n' m' - | Left_idx n', Left_idx m' => index_lt n' m' - | _, _ => false - end. - -Lemma index_eq_prop : forall n m:index, index_eq n m = true -> n = m. - simple induction n; simple induction m; simpl; intros. - rewrite (H i0 H1); reflexivity. - discriminate. - discriminate. - discriminate. - rewrite (H i0 H1); reflexivity. - discriminate. - discriminate. - discriminate. - reflexivity. -Qed. - -End variables_map. - -Unset Implicit Arguments. diff --git a/plugins/quote/g_quote.mlg b/plugins/quote/g_quote.mlg deleted file mode 100644 index 749903c3ad..0000000000 --- a/plugins/quote/g_quote.mlg +++ /dev/null @@ -1,46 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -{ - -open Ltac_plugin -open Names -open Tacexpr -open Geninterp -open Quote -open Stdarg -open Tacarg - -} - -DECLARE PLUGIN "quote_plugin" - -{ - -let cont = Id.of_string "cont" -let x = Id.of_string "x" - -let make_cont (k : Val.t) (c : EConstr.t) = - let c = Tacinterp.Value.of_constr c in - let tac = TacCall (Loc.tag (Locus.ArgVar CAst.(make cont), [Reference (Locus.ArgVar CAst.(make x))])) in - let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in - Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac)) - -} - -TACTIC EXTEND quote -| [ "quote" ident(f) ] -> { quote f [] } -| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> { quote f lc } -| [ "quote" ident(f) "in" constr(c) "using" tactic(k) ] -> - { gen_quote (make_cont k) c f [] } -| [ "quote" ident(f) "[" ne_ident_list(lc) "]" - "in" constr(c) "using" tactic(k) ] -> - { gen_quote (make_cont k) c f lc } -END diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml deleted file mode 100644 index 7464b42dc5..0000000000 --- a/plugins/quote/quote.ml +++ /dev/null @@ -1,540 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -(* The `Quote' tactic *) - -(* The basic idea is to automatize the inversion of interpretation functions - in 2-level approach - - Examples are given in \texttt{theories/DEMOS/DemoQuote.v} - - Suppose you have a langage \texttt{L} of 'abstract terms' - and a type \texttt{A} of 'concrete terms' - and a function \texttt{f : L -> (varmap A L) -> A}. - - Then, the tactic \texttt{quote f} will replace an - expression \texttt{e} of type \texttt{A} by \texttt{(f vm t)} - such that \texttt{e} and \texttt{(f vm t)} are convertible. - - The problem is then inverting the function \texttt{f}. - - The tactic works when: - - \begin{itemize} - \item L is a simple inductive datatype. The constructors of L may - have one of the three following forms: - - \begin{enumerate} - \item ordinary recursive constructors like: \verb|Cplus : L -> L -> L| - \item variable leaf like: \verb|Cvar : index -> L| - \item constant leaf like \verb|Cconst : A -> L| - \end{enumerate} - - The definition of \texttt{L} must contain at most one variable - leaf and at most one constant leaf. - - When there are both a variable leaf and a constant leaf, there is - an ambiguity on inversion. The term t can be either the - interpretation of \texttt{(Cconst t)} or the interpretation of - (\texttt{Cvar}~$i$) in a variable map containing the binding $i - \rightarrow$~\texttt{t}. How to discriminate between these - choices? - - To solve the dilemma, one gives to \texttt{quote} a list of - \emph{constant constructors}: a term will be considered as a - constant if it is either a constant constructor or the - application of a constant constructor to constants. For example - the list \verb+[S, O]+ defines the closed natural - numbers. \texttt{(S (S O))} is a constant when \texttt{(S x)} is - not. - - The definition of constants vary for each application of the - tactic, so it can even be different for two applications of - \texttt{quote} with the same function. - - \item \texttt{f} is a quite simple fixpoint on - \texttt{L}. In particular, \texttt{f} must verify: - -\begin{verbatim} - (f (Cvar i)) = (varmap_find vm default_value i) -\end{verbatim} -\begin{verbatim} - (f (Cconst c)) = c -\end{verbatim} - - where \texttt{index} and \texttt{varmap\_find} are those defined - the \texttt{Quote} module. \emph{The tactic won't work with - user's own variables map!!} It is mandatory to use the - variable map defined in module \texttt{Quote}. - - \end{itemize} - - The method to proceed is then clear: - - \begin{itemize} - \item Start with an empty hashtable of "registed leafs" - that maps constr to integers and a "variable counter" equal to 0. - \item Try to match the term with every right hand side of the - definition of \texttt{f}. - - If there is one match, returns the correponding left hand - side and call yourself recursively to get the arguments of this - left hand side. - - If there is no match, we are at a leaf. That is the - interpretation of either a variable or a constant. - - If it is a constant, return \texttt{Cconst} applied to that - constant. - - If not, it is a variable. Look in the hashtable - if this leaf has been already encountered. If not, increment - the variable counter and add an entry to the hashtable; then - return \texttt{(Cvar !variables\_counter)} - \end{itemize} -*) - - -(*i*) -open CErrors -open Util -open Names -open Constr -open EConstr -open Pattern -open Patternops -open Constr_matching -open Tacmach -open Proofview.Notations -(*i*) - -(*s First, we need to access some Coq constants - We do that lazily, because this code can be linked before - the constants are loaded in the environment *) - -let constant dir s = - EConstr.of_constr @@ UnivGen.constr_of_global @@ - Coqlib.coq_reference "Quote" ("quote"::dir) s - -let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm") -let coq_Node_vm = lazy (constant ["Quote"] "Node_vm") -let coq_varmap_find = lazy (constant ["Quote"] "varmap_find") -let coq_Right_idx = lazy (constant ["Quote"] "Right_idx") -let coq_Left_idx = lazy (constant ["Quote"] "Left_idx") -let coq_End_idx = lazy (constant ["Quote"] "End_idx") - -(*s Then comes the stuff to decompose the body of interpetation function - and pre-compute the inversion data. - -For a function like: - -\begin{verbatim} - Fixpoint interp (vm:varmap Prop) (f:form) := - match f with - | f_and f1 f1 f2 => (interp f1) /\ (interp f2) - | f_or f1 f1 f2 => (interp f1) \/ (interp f2) - | f_var i => varmap_find Prop default_v i vm - | f_const c => c - end. -\end{verbatim} - -With the constant constructors \texttt{C1}, \dots, \texttt{Cn}, the -corresponding scheme will be: - -\begin{verbatim} - {normal_lhs_rhs = - [ "(f_and ?1 ?2)", "?1 /\ ?2"; - "(f_or ?1 ?2)", " ?1 \/ ?2";]; - return_type = "Prop"; - constants = Some [C1,...Cn]; - variable_lhs = Some "(f_var ?1)"; - constant_lhs = Some "(f_const ?1)" - } -\end{verbatim} - -If there is no constructor for variables in the type \texttt{form}, -then [variable_lhs] is [None]. Idem for constants and -[constant_lhs]. Both cannot be equal to [None]. - -The metas in the RHS must correspond to those in the LHS (one cannot -exchange ?1 and ?2 in the example above) - -*) - -module ConstrSet = Set.Make(Constr) - -type inversion_scheme = { - normal_lhs_rhs : (constr * constr_pattern) list; - variable_lhs : constr option; - return_type : constr; - constants : ConstrSet.t; - constant_lhs : constr option } - -(*s [compute_ivs gl f cs] computes the inversion scheme associated to - [f:constr] with constants list [cs:constr list] in the context of - goal [gl]. This function uses the auxiliary functions - [i_can't_do_that], [decomp_term], [compute_lhs] and [compute_rhs]. *) - -let i_can't_do_that () = user_err Pp.(str "Quote: not a simple fixpoint") - -let decomp_term sigma c = EConstr.kind sigma (Termops.strip_outer_cast sigma c) - -(*s [compute_lhs typ i nargsi] builds the term \texttt{(C ?nargsi ... - ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive - type [typ] *) - -let coerce_meta_out id = - let s = Id.to_string id in - int_of_string (String.sub s 1 (String.length s - 1)) -let coerce_meta_in n = - Id.of_string ("M" ^ string_of_int n) - -let compute_lhs sigma typ i nargsi = - match EConstr.kind sigma typ with - | Ind((sp,0),u) -> - let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in - mkApp (mkConstructU (((sp,0),i+1),u), argsi) - | _ -> i_can't_do_that () - -(*s This function builds the pattern from the RHS. Recursive calls are - replaced by meta-variables ?i corresponding to those in the LHS *) - -let compute_rhs env sigma bodyi index_of_f = - let rec aux c = - match EConstr.kind sigma c with - | App (j, args) when isRel sigma j && Int.equal (destRel sigma j) index_of_f (* recursive call *) -> - let i = destRel sigma (Array.last args) in - PMeta (Some (coerce_meta_in i)) - | App (f,args) -> - PApp (pattern_of_constr env sigma (EConstr.to_constr sigma f), Array.map aux args) - | Cast (c,_,_) -> aux c - | _ -> pattern_of_constr env sigma (EConstr.to_constr sigma c) - in - aux bodyi - -(*s Now the function [compute_ivs] itself *) - -let compute_ivs f cs gl = - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let (cst, u) = try destConst sigma f with DestKO -> i_can't_do_that () in - let u = EInstance.kind sigma u in - let body = Environ.constant_value_in (Global.env()) (cst, u) in - let body = EConstr.of_constr body in - match decomp_term sigma body with - | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) -> - let (args3, body3) = decompose_lam sigma body2 in - let nargs3 = List.length args3 in - let is_conv = Reductionops.is_conv env sigma in - begin match decomp_term sigma body3 with - | Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *) - let n_lhs_rhs = ref [] - and v_lhs = ref (None : constr option) - and c_lhs = ref (None : constr option) in - Array.iteri - (fun i ci -> - let argsi, bodyi = decompose_lam sigma ci in - let nargsi = List.length argsi in - (* REL (narg3 + nargsi + 1) is f *) - (* REL nargsi+1 to REL nargsi + nargs3 are arguments of f *) - (* REL 1 to REL nargsi are argsi (reverse order) *) - (* First we test if the RHS is the RHS for constants *) - if isRel sigma bodyi && Int.equal (destRel sigma bodyi) 1 then - c_lhs := Some (compute_lhs sigma (snd (List.hd args3)) - i nargsi) - (* Then we test if the RHS is the RHS for variables *) - else begin match decompose_app sigma bodyi with - | vmf, [_; _; a3; a4 ] - when isRel sigma a3 && isRel sigma a4 && is_conv vmf - (Lazy.force coq_varmap_find) -> - v_lhs := Some (compute_lhs sigma - (snd (List.hd args3)) - i nargsi) - (* Third case: this is a normal LHS-RHS *) - | _ -> - n_lhs_rhs := - (compute_lhs sigma (snd (List.hd args3)) i nargsi, - compute_rhs env sigma bodyi (nargs3 + nargsi + 1)) - :: !n_lhs_rhs - end) - lci; - - if Option.is_empty !c_lhs && Option.is_empty !v_lhs then i_can't_do_that (); - - (* The Cases predicate is a lambda; we assume no dependency *) - let p = match EConstr.kind sigma p with - | Lambda (_,_,p) -> Termops.pop p - | _ -> p - in - - { normal_lhs_rhs = List.rev !n_lhs_rhs; - variable_lhs = !v_lhs; - return_type = p; - constants = List.fold_right ConstrSet.add cs ConstrSet.empty; - constant_lhs = !c_lhs } - - | _ -> i_can't_do_that () - end - |_ -> i_can't_do_that () - -(* TODO for that function: -\begin{itemize} -\item handle the case where the return type is an argument of the - function -\item handle the case of simple mutual inductive (for example terms - and lists of terms) formulas with the corresponding mutual - recursvive interpretation functions. -\end{itemize} -*) - -(*s Stuff to build variables map, currently implemented as complete -binary search trees (see file \texttt{Quote.v}) *) - -(* First the function to distinghish between constants (closed terms) - and variables (open terms) *) - -let rec closed_under sigma cset t = - (ConstrSet.mem (EConstr.Unsafe.to_constr t) cset) || - (match EConstr.kind sigma t with - | Cast(c,_,_) -> closed_under sigma cset c - | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l - | _ -> false) - -(*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete - binary search tree containing the [ci], that is: - -\begin{verbatim} - c1 - / \ - c2 c3 - / \ - c4 c5 -\end{verbatim} - -The second argument is a constr (the common type of the [ci]) -*) - -let btree_of_array a ty = - let size_of_a = Array.length a in - let semi_size_of_a = size_of_a lsr 1 in - let node = Lazy.force coq_Node_vm - and empty = mkApp (Lazy.force coq_Empty_vm, [| ty |]) in - let rec aux n = - if n > size_of_a - then empty - else if n > semi_size_of_a - then mkApp (node, [| ty; a.(n-1); empty; empty |]) - else mkApp (node, [| ty; a.(n-1); aux (2*n); aux (2*n+1) |]) - in - aux 1 - -(*s [btree_of_array] and [path_of_int] verify the following invariant:\\ - {\tt (varmap\_find A dv }[(path_of_int n)] [(btree_of_array a ty)] - = [a.(n)]\\ - [n] must be [> 0] *) - -let path_of_int n = - (* returns the list of digits of n in reverse order with - initial 1 removed *) - let rec digits_of_int n = - if Int.equal n 1 then [] - else (Int.equal (n mod 2) 1)::(digits_of_int (n lsr 1)) - in - List.fold_right - (fun b c -> mkApp ((if b then Lazy.force coq_Right_idx - else Lazy.force coq_Left_idx), - [| c |])) - (List.rev (digits_of_int n)) - (Lazy.force coq_End_idx) - -(*s The tactic works with a list of subterms sharing the same - variables map. We need to sort terms in order to avoid than - strange things happen during replacement of terms by their - 'abstract' counterparties. *) - -(* [subterm t t'] tests if constr [t'] occurs in [t] *) -(* This function does not descend under binders (lambda and Cases) *) - -let rec subterm gl (t : constr) (t' : constr) = - (pf_conv_x gl t t') || - (match EConstr.kind (project gl) t with - | App (f,args) -> Array.exists (fun t -> subterm gl t t') args - | Cast(t,_,_) -> (subterm gl t t') - | _ -> false) - -(*s We want to sort the list according to reverse subterm order. *) -(* Since it's a partial order the algoritm of Sort.list won't work !! *) - -let rec sort_subterm gl l = - let sigma = project gl in - let rec insert c = function - | [] -> [c] - | (h::t as l) when EConstr.eq_constr sigma c h -> l (* Avoid doing the same work twice *) - | h::t -> if subterm gl c h then c::h::t else h::(insert c t) - in - match l with - | [] -> [] - | h::t -> insert h (sort_subterm gl t) - -module Constrhash = Hashtbl.Make(Constr) - -let subst_meta subst c = - let subst = List.map (fun (i, c) -> i, EConstr.Unsafe.to_constr c) subst in - EConstr.of_constr (Termops.subst_meta subst (EConstr.Unsafe.to_constr c)) - -(*s Now we are able to do the inversion itself. - We destructurate the term and use an imperative hashtable - to store leafs that are already encountered. - The type of arguments is:\\ - [ivs : inversion_scheme]\\ - [lc: constr list]\\ - [gl: goal sigma]\\ *) -let quote_terms env sigma ivs lc = - Coqlib.check_required_library ["Coq";"quote";"Quote"]; - let varhash = (Constrhash.create 17 : constr Constrhash.t) in - let varlist = ref ([] : constr list) in (* list of variables *) - let counter = ref 1 in (* number of variables created + 1 *) - let rec aux c = - let rec auxl l = - match l with - | (lhs, rhs)::tail -> - begin try - let s1 = Id.Map.bindings (matches env sigma rhs c) in - let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux c_i)) s1 - in - subst_meta s2 lhs - with PatternMatchingFailure -> auxl tail - end - | [] -> - begin match ivs.variable_lhs with - | None -> - begin match ivs.constant_lhs with - | Some c_lhs -> subst_meta [1, c] c_lhs - | None -> anomaly (Pp.str "invalid inversion scheme for quote.") - end - | Some var_lhs -> - begin match ivs.constant_lhs with - | Some c_lhs when closed_under sigma ivs.constants c -> - subst_meta [1, c] c_lhs - | _ -> - begin - try Constrhash.find varhash (EConstr.Unsafe.to_constr c) - with Not_found -> - let newvar = - subst_meta [1, (path_of_int !counter)] - var_lhs in - begin - incr counter; - varlist := c :: !varlist; - Constrhash.add varhash (EConstr.Unsafe.to_constr c) newvar; - newvar - end - end - end - end - in - auxl ivs.normal_lhs_rhs - in - let lp = List.map aux lc in - (lp, (btree_of_array (Array.of_list (List.rev !varlist)) - ivs.return_type )) - -(*s actually we could "quote" a list of terms instead of a single - term. Ring for example needs that, but Ring doesn't use Quote - yet. *) - -let pf_constrs_of_globals l = - let rec aux l acc = - match l with - [] -> Proofview.tclUNIT (List.rev acc) - | hd :: tl -> - Tacticals.New.pf_constr_of_global hd >>= fun g -> aux tl (g :: acc) - in aux l [] - -let quote f lid = - Proofview.Goal.enter begin fun gl -> - let fg = Tacmach.New.pf_global f gl in - let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in - Tacticals.New.pf_constr_of_global fg >>= fun f -> - pf_constrs_of_globals clg >>= fun cl -> - Proofview.Goal.nf_enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let ivs = compute_ivs f (List.map (EConstr.to_constr sigma) cl) gl in - let concl = Proofview.Goal.concl gl in - let quoted_terms = quote_terms env sigma ivs [concl] in - let (p, vm) = match quoted_terms with - | [p], vm -> (p,vm) - | _ -> assert false - in - match ivs.variable_lhs with - | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast - | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast - end - end - -let gen_quote cont c f lid = - Proofview.Goal.enter begin fun gl -> - let fg = Tacmach.New.pf_global f gl in - let clg = List.map (fun id -> Tacmach.New.pf_global id gl) lid in - Tacticals.New.pf_constr_of_global fg >>= fun f -> - pf_constrs_of_globals clg >>= fun cl -> - Proofview.Goal.nf_enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.New.project gl in - let cl = List.map (EConstr.to_constr sigma) cl in - let ivs = compute_ivs f cl gl in - let quoted_terms = quote_terms env sigma ivs [c] in - let (p, vm) = match quoted_terms with - | [p], vm -> (p,vm) - | _ -> assert false - in - match ivs.variable_lhs with - | None -> cont (mkApp (f, [| p |])) - | Some _ -> cont (mkApp (f, [| vm; p |])) - end - end - -(*i - -Just testing ... - -#use "include.ml";; -open Quote;; - -let r = glob_constr_of_string;; - -let ivs = { - normal_lhs_rhs = - [ r "(f_and ?1 ?2)", r "?1/\?2"; - r "(f_not ?1)", r "~?1"]; - variable_lhs = Some (r "(f_atom ?1)"); - return_type = r "Prop"; - constants = ConstrSet.empty; - constant_lhs = (r "nat") -};; - -let t1 = r "True/\(True /\ ~False)";; -let t2 = r "True/\~~False";; - -quote_term ivs () t1;; -quote_term ivs () t2;; - -let ivs2 = - normal_lhs_rhs = - [ r "(f_and ?1 ?2)", r "?1/\?2"; - r "(f_not ?1)", r "~?1" - r "True", r "f_true"]; - variable_lhs = Some (r "(f_atom ?1)"); - return_type = r "Prop"; - constants = ConstrSet.empty; - constant_lhs = (r "nat") - -i*) diff --git a/plugins/quote/quote_plugin.mlpack b/plugins/quote/quote_plugin.mlpack deleted file mode 100644 index 2e9be09d8d..0000000000 --- a/plugins/quote/quote_plugin.mlpack +++ /dev/null @@ -1,2 +0,0 @@ -Quote -G_quote diff --git a/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v index a9b4d9d6f4..920b13ef49 100644 --- a/plugins/setoid_ring/Ring_base.v +++ b/plugins/setoid_ring/Ring_base.v @@ -12,7 +12,6 @@ ring tactic. Abstract rings need more theory, depending on ZArith_base. *) -Require Import Quote. Declare ML Module "newring_plugin". Require Export Ring_theory. Require Export Ring_tac. diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index e8efb362e2..26fef99bb2 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -15,7 +15,6 @@ Require Import Ring_polynom. Require Import BinList. Require Export ListTactics. Require Import InitialRing. -Require Import Quote. Declare ML Module "newring_plugin". diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index e6065dda87..bf38c30a1f 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -23,7 +23,7 @@ type reduction_tactic_error = exception ReductionTacticError of reduction_tactic_error -(** {6 Reduction functions associated to tactics. {% \label{%}tacred{% }%} } *) +(** {6 Reduction functions associated to tactics. } *) (** Evaluable global reference *) diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 266e94b34d..c30c4f0932 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -161,9 +161,9 @@ and nf_whd env sigma whd typ = | Vconstr_block b -> let tag = btag b in let (tag,ofs) = - if tag = Cbytecodes.last_variant_tag then + if tag = Obj.last_non_constant_constructor_tag then match whd_val (bfield b 0) with - | Vconstr_const tag -> (tag+Cbytecodes.last_variant_tag, 1) + | Vconstr_const tag -> (tag+Obj.last_non_constant_constructor_tag, 1) | _ -> assert false else (tag, 0) in let capp,ctyp = construct_of_constr_block env tag typ in @@ -278,7 +278,7 @@ and nf_stk ?from:(from=0) env sigma c t stk = in let branchs = Array.mapi mkbranch bsw in let tcase = build_case_type p realargs c in - let ci = sw.sw_annot.Cbytecodes.ci in + let ci = sw.sw_annot.Vmvalues.ci in nf_stk env sigma (mkCase(ci, p, c, branchs)) tcase stk | Zproj p :: stk -> assert (from = 0) ; diff --git a/test-suite/Makefile b/test-suite/Makefile index 080aeff85b..93ce519350 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -196,10 +196,7 @@ PRINT_LOGS:=APPVEYOR endif #APPVEYOR report: summary.log - $(HIDE)bash save-logs.sh - $(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo "travis_fold:start:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo "travis_fold:end:coq.logs.$$(echo '{}' | sed s,/,.,g)"' ';'; fi - $(HIDE)if [ -n "${PRINT_LOGS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec 'bash' '-c' 'echo {}' ';' -exec cat '{}' ';' -exec 'bash' '-c' 'echo' ';'; fi - $(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi + $(HIDE)bash report.sh ####################################################################### # Regression (and progression) tests diff --git a/test-suite/output/Quote.v b/test-suite/output/Quote.v deleted file mode 100644 index 2c373d5052..0000000000 --- a/test-suite/output/Quote.v +++ /dev/null @@ -1,36 +0,0 @@ -Require Import Quote. - -Parameter A B : Prop. - -Inductive formula : Type := - | f_and : formula -> formula -> formula - | f_or : formula -> formula -> formula - | f_not : formula -> formula - | f_true : formula - | f_atom : index -> formula - | f_const : Prop -> formula. - -Fixpoint interp_f (vm: - varmap Prop) (f:formula) {struct f} : Prop := - match f with - | f_and f1 f2 => interp_f vm f1 /\ interp_f vm f2 - | f_or f1 f2 => interp_f vm f1 \/ interp_f vm f2 - | f_not f1 => ~ interp_f vm f1 - | f_true => True - | f_atom i => varmap_find True i vm - | f_const c => c - end. - -Goal A \/ B -> A /\ (B \/ A) /\ (A \/ ~ B). -intro H. -match goal with - | H : ?a \/ ?b |- _ => quote interp_f in a using (fun x => idtac x; change (x \/ b) in H) -end. -match goal with - |- ?g => quote interp_f [ A ] in g using (fun x => idtac x) -end. -quote interp_f. -Show. -simpl; quote interp_f [ A ]. -Show. -Admitted. diff --git a/test-suite/report.sh b/test-suite/report.sh new file mode 100755 index 0000000000..05f39b4b02 --- /dev/null +++ b/test-suite/report.sh @@ -0,0 +1,55 @@ +#!/usr/bin/env bash + +# save failed logs to logs/, then print failure information +# returns failure code if any failed logs exist + +# save step + +SAVEDIR="logs" + +# reset for local builds +rm -rf "$SAVEDIR" +mkdir "$SAVEDIR" + +# keep this synced with test-suite/Makefile +FAILMARK="==========> FAILURE <==========" + +FAILED=$(mktemp /tmp/coq-check-XXXXXX) +find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" + +rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR" +cp summary.log "$SAVEDIR"/ + +# cleanup +rm "$FAILED" + +# print info +if [ -n "$TRAVIS" ] || [ -n "$PRINT_LOGS" ]; then + find logs/ -name '*.log' -not -name 'summary.log' -print0 | while IFS= read -r -d '' file; do + if [ -n "$TRAVIS" ]; then + # ${foo////.} replaces every / by . in $foo + printf 'travis_fold:start:coq.logs.%s\n' "${file////.}"; + else printf '%s\n' "$file" + fi + + cat "$file" + + if [ -n "$TRAVIS" ]; then + # ${foo////.} replaces every / by . in $foo + printf 'travis_fold:end:coq.logs.%s\n' "${file////.}"; + else printf '\n' + fi + done +fi + +if grep -q -F 'Error!' summary.log ; then + echo FAILURES; + grep -F 'Error!' summary.log; + if [ -z "$TRAVIS" ] && [ -z "$PRINT_LOGS" ]; then + echo 'To print details of failed tests, rerun with environment variable PRINT_LOGS=1' + echo 'eg "make report PRINT_LOGS=1" from the test suite directory"' + echo 'See README.md in the test suite directory for more information.' + fi + false +else echo NO FAILURES; +fi diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh deleted file mode 100755 index 9b8fff09f8..0000000000 --- a/test-suite/save-logs.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/usr/bin/env bash - -SAVEDIR="logs" - -# reset for local builds -rm -rf "$SAVEDIR" -mkdir "$SAVEDIR" - -# keep this synced with test-suite/Makefile -FAILMARK="==========> FAILURE <==========" - -FAILED=$(mktemp /tmp/coq-check-XXXXXX) -find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED" - -rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR" -cp summary.log "$SAVEDIR"/ - -# cleanup -rm "$FAILED" |