From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- .gitattributes | 5 + .mailmap | 89 +++++ CHANGES | 134 +++++++- INSTALL | 10 +- INSTALL.doc | 28 +- INSTALL.ide | 2 +- Makefile | 3 +- Makefile.build | 22 +- Makefile.common | 13 +- Makefile.doc | 26 +- README.doc | 0 checker/analyze.ml | 350 ++++++++++++++++++++ checker/analyze.mli | 35 ++ checker/check.ml | 53 ++- checker/check.mllib | 4 +- checker/check_stat.ml | 18 +- checker/checker.ml | 34 +- checker/cic.mli | 21 +- checker/closure.ml | 11 +- checker/closure.mli | 4 +- checker/declarations.ml | 19 +- checker/declarations.mli | 5 +- checker/environ.ml | 48 ++- checker/environ.mli | 8 +- checker/indtypes.ml | 12 +- checker/inductive.ml | 92 +++--- checker/mod_checking.ml | 22 +- checker/modops.ml | 7 +- checker/print.ml | 2 +- checker/reduction.ml | 15 +- checker/safe_typing.ml | 30 +- checker/safe_typing.mli | 4 +- checker/term.ml | 2 +- checker/typeops.ml | 2 +- checker/univ.ml | 87 +++-- checker/univ.mli | 20 +- checker/values.ml | 26 +- checker/votour.ml | 140 +++++++- configure.ml | 46 +-- dev/TODO | 22 ++ dev/base_include | 2 + dev/doc/README-V1-V5 | 293 ++++++++++++++++ dev/doc/univpoly.txt | 50 ++- dev/doc/versions-history.tex | 109 ++++-- dev/make-installer-win32.sh | 4 +- dev/make-installer-win64.sh | 28 ++ dev/nsis/coq.nsi | 4 +- dev/printers.mllib | 6 +- dev/top_printers.ml | 5 + dev/v8-syntax/memo-v8.tex | 2 +- dev/vm_printers.ml | 10 +- doc/stdlib/Library.tex | 0 doc/stdlib/index-list.html.template | 10 +- grammar/grammar.mllib | 5 +- grammar/tacextend.ml4 | 12 +- grammar/vernacextend.ml4 | 2 + ide/config_lexer.mll | 2 +- ide/coq-ssreflect.lang | 1 + ide/coq.lang | 363 ++++++++++---------- ide/coq.mli | 6 +- ide/coqOps.ml | 11 +- ide/coqide.ml | 12 +- ide/ide_slave.ml | 18 +- ide/ideutils.ml | 2 +- ide/interface.mli | 1 + ide/preferences.ml | 33 +- ide/session.ml | 20 +- ide/utf8_convert.mll | 2 +- ide/wg_ProofView.ml | 23 +- ide/wg_ScriptView.ml | 2 +- ide/xmlprotocol.ml | 4 + interp/constrintern.ml | 21 +- interp/constrintern.mli | 10 +- interp/coqlib.ml | 11 +- interp/implicit_quantifiers.ml | 16 +- interp/implicit_quantifiers.mli | 6 +- interp/modintern.ml | 2 +- interp/notation.ml | 41 ++- interp/notation.mli | 1 + interp/syntax_def.ml | 2 +- intf/misctypes.mli | 4 +- intf/tacexpr.mli | 10 +- intf/vernacexpr.mli | 48 ++- kernel/byterun/coq_fix_code.c | 2 +- kernel/byterun/coq_gc.h | 13 +- kernel/byterun/coq_instruct.h | 1 + kernel/byterun/coq_interp.c | 79 ++++- kernel/byterun/coq_memory.c | 16 - kernel/byterun/coq_values.c | 1 - kernel/byterun/coq_values.h | 19 +- kernel/cbytecodes.ml | 251 ++++++++------ kernel/cbytecodes.mli | 71 ++-- kernel/cbytegen.ml | 266 +++++++++++---- kernel/cbytegen.mli | 10 +- kernel/cemitcodes.ml | 35 +- kernel/cemitcodes.mli | 4 +- kernel/constr.ml | 54 ++- kernel/constr.mli | 20 +- kernel/conv_oracle.ml | 15 +- kernel/csymtable.ml | 44 ++- kernel/declarations.mli | 21 +- kernel/declareops.ml | 18 +- kernel/declareops.mli | 12 +- kernel/entries.mli | 25 +- kernel/environ.ml | 59 ++-- kernel/environ.mli | 13 +- kernel/fast_typeops.ml | 8 +- kernel/indtypes.ml | 109 +++--- kernel/indtypes.mli | 2 +- kernel/inductive.ml | 105 +++--- kernel/mod_subst.ml | 2 +- kernel/mod_subst.mli | 5 +- kernel/mod_typing.ml | 119 +++++-- kernel/mod_typing.mli | 13 +- kernel/modops.ml | 12 +- kernel/modops.mli | 3 - kernel/names.ml | 36 +- kernel/names.mli | 4 + kernel/nativecode.ml | 32 +- kernel/nativecode.mli | 26 +- kernel/nativeconv.ml | 136 ++++---- kernel/nativeconv.mli | 4 + kernel/nativelambda.ml | 38 +-- kernel/nativelambda.mli | 2 +- kernel/nativelib.ml | 28 +- kernel/nativelibrary.ml | 4 +- kernel/nativelibrary.mli | 2 +- kernel/nativevalues.ml | 2 +- kernel/opaqueproof.ml | 5 +- kernel/pre_env.ml | 6 +- kernel/pre_env.mli | 3 +- kernel/reduction.ml | 58 +--- kernel/reduction.mli | 27 +- kernel/safe_typing.ml | 278 ++++++++++------ kernel/safe_typing.mli | 61 +++- kernel/sorts.ml | 10 +- kernel/subtyping.ml | 13 +- kernel/term.ml | 28 +- kernel/term.mli | 31 +- kernel/term_typing.ml | 302 ++++++++++++++--- kernel/term_typing.mli | 41 ++- kernel/typeops.ml | 26 +- kernel/univ.ml | 235 +++++++------ kernel/univ.mli | 21 +- kernel/vars.ml | 4 +- kernel/vars.mli | 2 +- kernel/vconv.ml | 191 ++++------- kernel/vconv.mli | 10 +- kernel/vm.ml | 305 +++++++++-------- kernel/vm.mli | 25 +- lib/aux_file.ml | 2 + lib/aux_file.mli | 4 + lib/cThread.ml | 14 +- lib/clib.mllib | 1 + lib/dyn.ml | 9 +- lib/errors.ml | 27 +- lib/errors.mli | 10 + lib/flags.ml | 12 +- lib/flags.mli | 13 +- lib/future.ml | 20 +- lib/future.mli | 7 +- lib/pp.ml | 77 +++-- lib/pp.mli | 5 +- lib/pp_control.ml | 11 +- lib/ppstyle.ml | 149 +++++++++ lib/ppstyle.mli | 70 ++++ lib/richpp.mli | 2 +- lib/spawn.ml | 44 ++- lib/system.ml | 79 +++-- lib/system.mli | 10 +- lib/terminal.ml | 7 +- lib/terminal.mli | 3 + lib/util.ml | 11 + lib/util.mli | 3 + lib/xml_lexer.mll | 17 +- lib/xml_parser.mli | 16 +- lib/xml_printer.ml | 2 + library/assumptions.ml | 225 ------------- library/assumptions.mli | 41 --- library/declare.ml | 261 +++++++-------- library/declare.mli | 23 +- library/declaremods.ml | 18 +- library/declaremods.mli | 2 +- library/global.ml | 14 +- library/global.mli | 15 +- library/goptions.ml | 25 +- library/goptions.mli | 2 + library/heads.ml | 5 +- library/impargs.ml | 9 +- library/impargs.mli | 4 +- library/lib.ml | 52 ++- library/lib.mli | 3 +- library/libobject.ml | 16 +- library/library.ml | 185 +++++------ library/library.mli | 17 +- library/library.mllib | 1 - library/loadpath.ml | 8 +- library/loadpath.mli | 7 +- library/nameops.ml | 5 + library/nameops.mli | 2 +- library/nametab.ml | 3 +- library/states.ml | 18 +- library/universes.ml | 221 +++++++++---- library/universes.mli | 19 ++ man/coqide.1 | 20 +- man/coqtop.1 | 19 +- parsing/g_constr.ml4 | 44 ++- parsing/g_proofs.ml4 | 12 +- parsing/g_tactic.ml4 | 66 ++-- parsing/g_vernac.ml4 | 115 ++++--- parsing/g_xml.ml4 | 290 ---------------- parsing/lexer.ml4 | 2 +- parsing/pcoq.ml4 | 10 +- plugins/btauto/Algebra.v | 2 +- plugins/cc/ccalgo.ml | 20 +- plugins/cc/ccalgo.mli | 2 +- plugins/cc/cctac.ml | 49 ++- plugins/decl_mode/decl_proof_instr.ml | 42 ++- plugins/derive/derive.ml | 4 +- plugins/extraction/CHANGES | 6 +- plugins/extraction/ExtrHaskellNatInt.v | 13 + plugins/extraction/ExtrHaskellNatInteger.v | 13 + plugins/extraction/ExtrHaskellNatNum.v | 35 ++ plugins/extraction/ExtrHaskellString.v | 38 +++ plugins/extraction/ExtrHaskellZInt.v | 24 ++ plugins/extraction/ExtrHaskellZInteger.v | 23 ++ plugins/extraction/ExtrHaskellZNum.v | 21 ++ plugins/extraction/extraction.ml | 3 +- plugins/extraction/mlutil.ml | 14 +- plugins/extraction/vo.itarget | 9 +- plugins/firstorder/instances.ml | 4 +- plugins/firstorder/sequent.ml | 7 +- plugins/funind/functional_principles_proofs.ml | 24 +- plugins/funind/functional_principles_types.ml | 68 ++-- plugins/funind/functional_principles_types.mli | 10 +- plugins/funind/g_indfun.ml4 | 244 -------------- plugins/funind/glob_term_to_relation.ml | 99 +++--- plugins/funind/glob_termops.mli | 4 +- plugins/funind/indfun.ml | 75 ++--- plugins/funind/indfun_common.ml | 13 +- plugins/funind/indfun_common.mli | 4 +- plugins/funind/invfun.ml | 26 +- plugins/funind/merge.ml | 8 +- plugins/funind/recdef.ml | 32 +- plugins/micromega/mfourier.ml | 2 +- plugins/omega/coq_omega.ml | 10 +- plugins/romega/refl_omega.ml | 8 +- plugins/setoid_ring/newring.ml4 | 13 +- pretyping/cases.ml | 70 ++-- pretyping/classops.mli | 4 +- pretyping/coercion.ml | 28 +- pretyping/constr_matching.ml | 192 +++++------ pretyping/constr_matching.mli | 9 +- pretyping/detyping.ml | 9 +- pretyping/evarconv.ml | 20 +- pretyping/evarsolve.ml | 111 +++++-- pretyping/evarutil.ml | 37 ++- pretyping/evarutil.mli | 7 + pretyping/evd.ml | 331 +++++++++++++------ pretyping/evd.mli | 57 ++-- pretyping/glob_ops.ml | 111 +++++-- pretyping/glob_ops.mli | 1 + pretyping/inductiveops.ml | 12 +- pretyping/inductiveops.mli | 2 + pretyping/miscops.ml | 2 +- pretyping/namegen.ml | 1 + pretyping/nativenorm.ml | 46 +-- pretyping/nativenorm.mli | 6 +- pretyping/patternops.ml | 4 +- pretyping/pretyping.ml | 168 ++++++---- pretyping/pretyping.mli | 28 +- pretyping/pretyping.mllib | 2 +- pretyping/recordops.ml | 2 +- pretyping/reductionops.ml | 26 +- pretyping/reductionops.mli | 18 +- pretyping/retyping.ml | 13 +- pretyping/tacred.ml | 8 +- pretyping/termops.ml | 17 +- pretyping/termops.mli | 4 + pretyping/typeclasses.ml | 2 +- pretyping/typing.ml | 13 +- pretyping/typing.mli | 9 +- pretyping/unification.ml | 13 +- pretyping/vnorm.ml | 106 ++++-- pretyping/vnorm.mli | 2 +- printing/ppconstr.ml | 14 +- printing/ppstyle.ml | 149 --------- printing/ppstyle.mli | 70 ---- printing/pptactic.ml | 9 +- printing/ppvernac.ml | 61 ++-- printing/prettyp.ml | 68 ++-- printing/printer.ml | 99 +++++- printing/printer.mli | 22 +- printing/printing.mllib | 1 - printing/printmod.ml | 58 ++-- proofs/clenv.ml | 2 +- proofs/clenvtac.ml | 4 +- proofs/evar_refiner.ml | 5 +- proofs/logic.ml | 32 +- proofs/logic_monad.ml | 133 ++++---- proofs/logic_monad.mli | 9 +- proofs/pfedit.ml | 22 +- proofs/pfedit.mli | 11 +- proofs/proof.ml | 21 +- proofs/proof.mli | 4 + proofs/proof_global.ml | 102 ++++-- proofs/proof_global.mli | 22 +- proofs/proof_using.ml | 172 +++++----- proofs/proof_using.mli | 15 +- proofs/proofview.ml | 51 ++- proofs/proofview.mli | 2 +- proofs/redexpr.ml | 20 +- proofs/refiner.ml | 18 +- proofs/tacmach.ml | 4 + proofs/tacmach.mli | 6 +- proofs/tactic_debug.ml | 23 +- stm/lemmas.ml | 67 ++-- stm/lemmas.mli | 3 +- stm/spawned.ml | 19 +- stm/spawned.mli | 2 +- stm/stm.ml | 191 +++++++---- stm/stm.mli | 17 +- stm/tQueue.ml | 20 ++ stm/tQueue.mli | 3 + stm/texmacspp.ml | 24 +- stm/vernac_classifier.ml | 24 +- stm/vio_checking.ml | 8 +- tactics/auto.ml | 54 ++- tactics/auto.mli | 9 +- tactics/autorewrite.ml | 15 +- tactics/class_tactics.ml | 67 ++-- tactics/contradiction.ml | 6 +- tactics/eauto.ml4 | 78 +++-- tactics/elim.ml | 4 +- tactics/elimschemes.ml | 26 +- tactics/eqdecide.ml | 46 ++- tactics/eqschemes.ml | 27 +- tactics/eqschemes.mli | 4 +- tactics/equality.ml | 143 ++++++-- tactics/equality.mli | 2 +- tactics/extratactics.ml4 | 27 +- tactics/hints.ml | 292 ++++++++++------ tactics/hints.mli | 39 ++- tactics/hipattern.ml4 | 2 +- tactics/inv.ml | 6 +- tactics/leminv.ml | 7 +- tactics/rewrite.ml | 350 +++++++++++--------- tactics/rewrite.mli | 5 +- tactics/tacenv.ml | 46 ++- tactics/tacenv.mli | 16 + tactics/tacintern.ml | 29 +- tactics/tacinterp.ml | 53 +-- tactics/tactic_matching.mli | 4 +- tactics/tacticals.ml | 26 +- tactics/tactics.ml | 377 +++++++++++++-------- tactics/tactics.mli | 1 + tactics/tauto.ml4 | 4 +- tactics/term_dnet.ml | 4 +- test-suite/Makefile | 12 +- test-suite/bugs/closed/2016.v | 62 ++++ test-suite/bugs/closed/2243.v | 9 + test-suite/bugs/closed/2584.v | 89 +++++ test-suite/bugs/closed/3267.v | 11 + test-suite/bugs/closed/3309.v | 334 ------------------- test-suite/bugs/closed/3314.v | 8 +- test-suite/bugs/closed/3330.v | 1 + test-suite/bugs/closed/3352.v | 1 + test-suite/bugs/closed/3386.v | 1 + test-suite/bugs/closed/3387.v | 1 + test-suite/bugs/closed/3446.v | 51 +++ test-suite/bugs/closed/3461.v | 5 + test-suite/bugs/closed/3509.v | 6 + test-suite/bugs/closed/3510.v | 5 + test-suite/bugs/closed/3539.v | 4 +- test-suite/bugs/closed/3559.v | 1 + test-suite/bugs/closed/3566.v | 1 + test-suite/bugs/closed/3593.v | 10 + test-suite/bugs/closed/3666.v | 1 + test-suite/bugs/closed/3685.v | 75 +++++ test-suite/bugs/closed/3690.v | 1 + test-suite/bugs/closed/3736.v | 8 + test-suite/bugs/closed/3743.v | 11 + test-suite/bugs/closed/3777.v | 17 + test-suite/bugs/closed/3779.v | 12 + test-suite/bugs/closed/3808.v | 1 + test-suite/bugs/closed/3819.v | 9 + test-suite/bugs/closed/3821.v | 1 + test-suite/bugs/closed/3922.v | 3 +- test-suite/bugs/closed/3948.v | 24 ++ test-suite/bugs/closed/3956.v | 143 ++++++++ test-suite/bugs/closed/3974.v | 7 + test-suite/bugs/closed/3975.v | 8 + test-suite/bugs/closed/4034.v | 25 ++ test-suite/bugs/closed/4057.v | 210 ++++++++++++ test-suite/bugs/closed/4069.v | 51 +++ test-suite/bugs/closed/4089.v | 3 +- test-suite/bugs/closed/4116.v | 383 +++++++++++++++++++++ test-suite/bugs/closed/4121.v | 1 + test-suite/bugs/closed/4151.v | 403 +++++++++++++++++++++++ test-suite/bugs/closed/4161.v | 27 ++ test-suite/bugs/closed/4191.v | 5 + test-suite/bugs/closed/4198.v | 37 +++ test-suite/bugs/closed/4203.v | 19 ++ test-suite/bugs/closed/4205.v | 8 + test-suite/bugs/closed/4216.v | 20 ++ test-suite/bugs/closed/4217.v | 6 + test-suite/bugs/closed/4221.v | 9 + test-suite/bugs/closed/4232.v | 20 ++ test-suite/bugs/closed/4234.v | 7 + test-suite/bugs/closed/4240.v | 12 + test-suite/bugs/closed/4251.v | 17 + test-suite/bugs/closed/4254.v | 13 + test-suite/bugs/closed/4272.v | 12 + test-suite/bugs/closed/4276.v | 11 + test-suite/bugs/closed/4280.v | 24 ++ test-suite/bugs/closed/4283.v | 8 + test-suite/bugs/closed/4287.v | 125 +++++++ test-suite/bugs/closed/4294.v | 31 ++ test-suite/bugs/closed/4298.v | 7 + test-suite/bugs/closed/4299.v | 12 + test-suite/bugs/closed/4301.v | 13 + test-suite/bugs/closed/4305.v | 17 + test-suite/bugs/closed/4316.v | 3 + test-suite/bugs/closed/4318.v | 2 + test-suite/bugs/closed/4325.v | 5 + test-suite/bugs/closed/4328.v | 6 + test-suite/bugs/closed/4346.v | 2 + test-suite/bugs/closed/4347.v | 17 + test-suite/bugs/closed/4354.v | 11 + test-suite/bugs/closed/4366.v | 15 + test-suite/bugs/closed/4372.v | 20 ++ test-suite/bugs/closed/4375.v | 106 ++++++ test-suite/bugs/closed/4390.v | 37 +++ test-suite/bugs/closed/4394.v | 19 ++ test-suite/bugs/closed/4397.v | 3 + test-suite/bugs/closed/HoTT_coq_007.v | 1 + test-suite/bugs/closed/HoTT_coq_014.v | 6 +- test-suite/bugs/closed/HoTT_coq_036.v | 1 + test-suite/bugs/closed/HoTT_coq_053.v | 2 +- test-suite/bugs/closed/HoTT_coq_062.v | 1 + test-suite/bugs/closed/HoTT_coq_093.v | 3 +- test-suite/bugs/closed/HoTT_coq_108.v | 2 +- test-suite/bugs/closed/HoTT_coq_120.v | 138 ++++++++ test-suite/bugs/opened/3045.v | 30 -- test-suite/bugs/opened/3326.v | 18 - test-suite/bugs/opened/3461.v | 5 - test-suite/bugs/opened/3509.v | 19 -- test-suite/bugs/opened/3510.v | 35 -- test-suite/bugs/opened/3562.v | 2 - test-suite/bugs/opened/3593.v | 10 - test-suite/bugs/opened/3657.v | 33 -- test-suite/bugs/opened/3670.v | 19 -- test-suite/bugs/opened/3675.v | 20 -- test-suite/bugs/opened/3685.v | 75 ----- test-suite/bugs/opened/3754.v | 1 + test-suite/bugs/opened/3788.v | 5 - test-suite/bugs/opened/3808.v | 2 - test-suite/bugs/opened/3819.v | 11 - test-suite/bugs/opened/4214.v | 5 + test-suite/bugs/opened/HoTT_coq_120.v | 137 -------- test-suite/coqchk/primproj.v | 2 + test-suite/failure/guard-cofix.v | 2 +- test-suite/ide/bug4246.fake | 14 + test-suite/ide/bug4249.fake | 16 + test-suite/ide/reopen.fake | 21 ++ test-suite/ide/univ.fake | 14 + test-suite/interactive/4289.v | 14 + test-suite/interactive/ParalITP_smallproofs.v | 0 test-suite/kernel/vm-univ.v | 145 ++++++++ test-suite/output/Inductive.out | 3 + test-suite/output/Inductive.v | 3 + test-suite/output/Notations.out | 4 +- test-suite/output/PrintAssumptions.out | 7 +- test-suite/output/PrintAssumptions.v | 16 + test-suite/output/PrintModule.out | 4 + test-suite/output/PrintModule.v | 34 ++ test-suite/output/inference.out | 4 +- test-suite/output/ltac.out | 2 + test-suite/output/ltac.v | 17 + test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v | 0 test-suite/success/Hints.v | 44 +++ test-suite/success/apply.v | 47 ++- test-suite/success/auto.v | 2 +- test-suite/success/extraction_polyprop.v | 11 + test-suite/success/intros.v | 36 ++ test-suite/success/ltac.v | 19 ++ test-suite/success/namedunivs.v | 2 + test-suite/success/polymorphism.v | 30 ++ test-suite/success/primitiveproj.v | 7 + test-suite/success/proof_using.v | 76 +++++ test-suite/success/record_syntax.v | 47 +++ test-suite/success/sideff.v | 12 + test-suite/success/simpl.v | 7 + test-suite/success/specialize.v | 20 +- test-suite/success/univnames.v | 26 ++ theories/Arith/intro.tex | 55 ---- theories/Bool/intro.tex | 16 - theories/Classes/CMorphisms.v | 8 +- theories/Classes/RelationClasses.v | 5 + theories/Compat/Coq84.v | 77 +++++ theories/Compat/Coq85.v | 9 + theories/Compat/vo.itarget | 2 + theories/Lists/List.v | 20 +- theories/Lists/intro.tex | 20 -- theories/Logic/WeakFan.v | 11 +- theories/Logic/intro.tex | 8 - theories/NArith/intro.tex | 5 - theories/Numbers/Cyclic/Int31/Int31.v | 2 +- theories/Numbers/NaryFunctions.v | 2 +- theories/PArith/intro.tex | 4 - theories/Program/Syntax.v | 7 - theories/Program/Tactics.v | 2 +- theories/Reals/intro.tex | 4 - theories/Relations/intro.tex | 23 -- theories/Setoids/intro.tex | 1 - theories/Sets/intro.tex | 24 -- theories/Sorting/intro.tex | 1 - theories/Vectors/Fin.v | 32 +- theories/Vectors/VectorSpec.v | 45 +-- theories/Wellfounded/intro.tex | 4 - theories/ZArith/intro.tex | 6 - theories/theories.itarget | 1 + tools/README.coq-tex | 13 - tools/README.emacs | 0 tools/coq-sl.sty | 0 tools/coq_makefile.ml | 23 +- tools/coq_tex.ml | 203 ++++++------ tools/coqc.ml | 15 +- tools/coqdep.ml | 64 ++-- tools/coqdep_boot.ml | 6 +- tools/coqdep_common.ml | 155 ++++++--- tools/coqdep_common.mli | 10 +- tools/coqdep_lexer.mli | 3 +- tools/coqdep_lexer.mll | 16 +- tools/coqdoc/cpretty.mll | 1 + tools/coqdoc/main.ml | 8 +- tools/coqdoc/output.ml | 7 +- tools/coqwc.mll | 4 +- tools/fake_ide.ml | 6 +- tools/gallina.ml | 5 +- toplevel/assumptions.ml | 230 +++++++++++++ toplevel/assumptions.mli | 32 ++ toplevel/auto_ind_decl.ml | 123 +++---- toplevel/auto_ind_decl.mli | 1 + toplevel/cerrors.ml | 17 +- toplevel/cerrors.mli | 2 +- toplevel/class.ml | 13 +- toplevel/classes.ml | 23 +- toplevel/command.ml | 328 +++++++++++------- toplevel/command.mli | 40 ++- toplevel/coqinit.ml | 5 +- toplevel/coqloop.ml | 2 +- toplevel/coqtop.ml | 125 ++++--- toplevel/coqtop.mli | 2 +- toplevel/discharge.ml | 4 +- toplevel/himsg.ml | 22 +- toplevel/ind_tables.ml | 60 ++-- toplevel/ind_tables.mli | 19 +- toplevel/indschemes.ml | 52 +-- toplevel/locality.ml | 5 +- toplevel/metasyntax.ml | 41 ++- toplevel/metasyntax.mli | 1 + toplevel/mltop.ml | 13 +- toplevel/obligations.ml | 221 +++++++------ toplevel/obligations.mli | 4 +- toplevel/record.ml | 122 ++++--- toplevel/record.mli | 2 +- toplevel/search.ml | 8 +- toplevel/toplevel.mllib | 1 + toplevel/usage.ml | 21 +- toplevel/vernac.ml | 77 ++--- toplevel/vernacentries.ml | 287 ++++++++-------- toplevel/vernacentries.mli | 3 + 573 files changed, 13485 insertions(+), 7706 deletions(-) create mode 100644 .gitattributes create mode 100644 .mailmap mode change 100755 => 100644 README.doc create mode 100644 checker/analyze.ml create mode 100644 checker/analyze.mli create mode 100644 dev/TODO create mode 100644 dev/doc/README-V1-V5 create mode 100755 dev/make-installer-win64.sh mode change 100755 => 100644 doc/stdlib/Library.tex create mode 100644 lib/ppstyle.ml create mode 100644 lib/ppstyle.mli delete mode 100644 library/assumptions.ml delete mode 100644 library/assumptions.mli delete mode 100644 parsing/g_xml.ml4 create mode 100644 plugins/extraction/ExtrHaskellNatInt.v create mode 100644 plugins/extraction/ExtrHaskellNatInteger.v create mode 100644 plugins/extraction/ExtrHaskellNatNum.v create mode 100644 plugins/extraction/ExtrHaskellString.v create mode 100644 plugins/extraction/ExtrHaskellZInt.v create mode 100644 plugins/extraction/ExtrHaskellZInteger.v create mode 100644 plugins/extraction/ExtrHaskellZNum.v delete mode 100644 printing/ppstyle.ml delete mode 100644 printing/ppstyle.mli create mode 100644 test-suite/bugs/closed/2016.v create mode 100644 test-suite/bugs/closed/2243.v create mode 100644 test-suite/bugs/closed/2584.v delete mode 100644 test-suite/bugs/closed/3309.v create mode 100644 test-suite/bugs/closed/3446.v create mode 100644 test-suite/bugs/closed/3461.v create mode 100644 test-suite/bugs/closed/3509.v create mode 100644 test-suite/bugs/closed/3510.v create mode 100644 test-suite/bugs/closed/3593.v create mode 100644 test-suite/bugs/closed/3685.v create mode 100644 test-suite/bugs/closed/3736.v create mode 100644 test-suite/bugs/closed/3743.v create mode 100644 test-suite/bugs/closed/3777.v create mode 100644 test-suite/bugs/closed/3779.v create mode 100644 test-suite/bugs/closed/3819.v create mode 100644 test-suite/bugs/closed/3948.v create mode 100644 test-suite/bugs/closed/3956.v create mode 100644 test-suite/bugs/closed/3974.v create mode 100644 test-suite/bugs/closed/3975.v create mode 100644 test-suite/bugs/closed/4034.v create mode 100644 test-suite/bugs/closed/4057.v create mode 100644 test-suite/bugs/closed/4069.v create mode 100644 test-suite/bugs/closed/4116.v create mode 100644 test-suite/bugs/closed/4151.v create mode 100644 test-suite/bugs/closed/4161.v create mode 100644 test-suite/bugs/closed/4191.v create mode 100644 test-suite/bugs/closed/4198.v create mode 100644 test-suite/bugs/closed/4203.v create mode 100644 test-suite/bugs/closed/4205.v create mode 100644 test-suite/bugs/closed/4216.v create mode 100644 test-suite/bugs/closed/4217.v create mode 100644 test-suite/bugs/closed/4221.v create mode 100644 test-suite/bugs/closed/4232.v create mode 100644 test-suite/bugs/closed/4234.v create mode 100644 test-suite/bugs/closed/4240.v create mode 100644 test-suite/bugs/closed/4251.v create mode 100644 test-suite/bugs/closed/4254.v create mode 100644 test-suite/bugs/closed/4272.v create mode 100644 test-suite/bugs/closed/4276.v create mode 100644 test-suite/bugs/closed/4280.v create mode 100644 test-suite/bugs/closed/4283.v create mode 100644 test-suite/bugs/closed/4287.v create mode 100644 test-suite/bugs/closed/4294.v create mode 100644 test-suite/bugs/closed/4298.v create mode 100644 test-suite/bugs/closed/4299.v create mode 100644 test-suite/bugs/closed/4301.v create mode 100644 test-suite/bugs/closed/4305.v create mode 100644 test-suite/bugs/closed/4316.v create mode 100644 test-suite/bugs/closed/4318.v create mode 100644 test-suite/bugs/closed/4325.v create mode 100644 test-suite/bugs/closed/4328.v create mode 100644 test-suite/bugs/closed/4346.v create mode 100644 test-suite/bugs/closed/4347.v create mode 100644 test-suite/bugs/closed/4354.v create mode 100644 test-suite/bugs/closed/4366.v create mode 100644 test-suite/bugs/closed/4372.v create mode 100644 test-suite/bugs/closed/4375.v create mode 100644 test-suite/bugs/closed/4390.v create mode 100644 test-suite/bugs/closed/4394.v create mode 100644 test-suite/bugs/closed/4397.v create mode 100644 test-suite/bugs/closed/HoTT_coq_120.v delete mode 100644 test-suite/bugs/opened/3045.v delete mode 100644 test-suite/bugs/opened/3326.v delete mode 100644 test-suite/bugs/opened/3461.v delete mode 100644 test-suite/bugs/opened/3509.v delete mode 100644 test-suite/bugs/opened/3510.v delete mode 100644 test-suite/bugs/opened/3562.v delete mode 100644 test-suite/bugs/opened/3593.v delete mode 100644 test-suite/bugs/opened/3657.v delete mode 100644 test-suite/bugs/opened/3670.v delete mode 100644 test-suite/bugs/opened/3675.v delete mode 100644 test-suite/bugs/opened/3685.v delete mode 100644 test-suite/bugs/opened/3788.v delete mode 100644 test-suite/bugs/opened/3808.v delete mode 100644 test-suite/bugs/opened/3819.v create mode 100644 test-suite/bugs/opened/4214.v delete mode 100644 test-suite/bugs/opened/HoTT_coq_120.v create mode 100644 test-suite/coqchk/primproj.v create mode 100644 test-suite/ide/bug4246.fake create mode 100644 test-suite/ide/bug4249.fake create mode 100644 test-suite/ide/reopen.fake create mode 100644 test-suite/ide/univ.fake create mode 100644 test-suite/interactive/4289.v mode change 100755 => 100644 test-suite/interactive/ParalITP_smallproofs.v create mode 100644 test-suite/kernel/vm-univ.v create mode 100644 test-suite/output/Inductive.out create mode 100644 test-suite/output/Inductive.v create mode 100644 test-suite/output/PrintModule.out create mode 100644 test-suite/output/PrintModule.v create mode 100644 test-suite/output/ltac.out create mode 100644 test-suite/output/ltac.v mode change 100755 => 100644 test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v create mode 100644 test-suite/success/extraction_polyprop.v create mode 100644 test-suite/success/record_syntax.v create mode 100644 test-suite/success/sideff.v create mode 100644 test-suite/success/univnames.v delete mode 100755 theories/Arith/intro.tex delete mode 100644 theories/Bool/intro.tex create mode 100644 theories/Compat/Coq84.v create mode 100644 theories/Compat/Coq85.v create mode 100644 theories/Compat/vo.itarget delete mode 100755 theories/Lists/intro.tex delete mode 100755 theories/Logic/intro.tex delete mode 100644 theories/NArith/intro.tex delete mode 100644 theories/PArith/intro.tex delete mode 100644 theories/Reals/intro.tex delete mode 100755 theories/Relations/intro.tex delete mode 100644 theories/Setoids/intro.tex delete mode 100755 theories/Sets/intro.tex delete mode 100644 theories/Sorting/intro.tex delete mode 100755 theories/Wellfounded/intro.tex delete mode 100755 theories/ZArith/intro.tex delete mode 100755 tools/README.coq-tex mode change 100755 => 100644 tools/README.emacs mode change 100755 => 100644 tools/coq-sl.sty create mode 100644 toplevel/assumptions.ml create mode 100644 toplevel/assumptions.mli diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 00000000..6af0a106 --- /dev/null +++ b/.gitattributes @@ -0,0 +1,5 @@ +.dir-locals.el export-ignore +.gitattributes export-ignore +.gitignore export-ignore +.mailmap export-ignore +TODO export-ignore diff --git a/.mailmap b/.mailmap new file mode 100644 index 00000000..13c71558 --- /dev/null +++ b/.mailmap @@ -0,0 +1,89 @@ +## Coq contributors +## +## This file allows joining the different accounts of a same person. +## Cf for instance: git shortlog -nse. More details via: man git shortlog +## +## To avoid spam issues, we use by default a pseudo-email +## for all persons that haven't made commits with real emails +## +## If you're mentionned here and want to update your information, +## either amend this file and commit it, or contact the coqdev list + +Jim Apple jbapple +Bruno Barras barras +Bruno Barras barras-local +Yves Bertot bertot +Frédéric Besson fbesson +Pierre Boutillier pboutill +Pierre Boutillier Pierre +Pierre Boutillier Pierre Boutillier +Xavier Clerc xclerc +Xavier Clerc xclerc +Pierre Corbineau corbinea +Judicaël Courant courant +Pierre Courtieu courtieu +David Delahaye delahaye +Maxime Dénès mdenes +Daniel De Rauglaudre ddr +Olivier Desmettre desmettr +Damien Doligez doligez +Jean-Christophe Filliâtre filliatr +Jean-Christophe Filliâtre Jean-Christophe Filliatre +Julien Forest jforest +Julien Forest forest +Julien Forest jforest +Julien Forest jforest +Stéphane Glondu glondu +Stéphane Glondu Stephane Glondu +Benjamin Grégoire Benjamin Gregoire +Benjamin Grégoire bgregoir +Benjamin Grégoire gregoire +Jason Gross Jason Gross +Jason Gross Jason Gross +Vincent Gross vgross +Huang Guan-Shieng huang +Hugo Herbelin herbelin +Tom Hutchinson thutchin +Cezary Kaliszyk cek +Florent Kirchner fkirchne +Florent Kirchner kirchner +Marc Lasson mlasson +Pierre Letouzey letouzey +Assia Mahboubi amahboub +Evgeny Makarov emakarov +Gregory Malecha Gregory Malecha +Lionel Elie Mamane lmamane +Claude Marché marche +Micaela Mayero mayero +Guillaume Melquiond gmelquio +Alexandre Miquel miquel +Benjamin Monate monate +Julien Narboux jnarboux +Julien Narboux narboux +Jean-Marc Notin notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty +Jean-Marc Notin notin +Russel O'Connor roconnor +Christine Paulin cpaulin +Christine Paulin mohring +Pierre-Marie Pédrot ppedrot +Loïc Pottier pottier +Matthias Puech puech +Yann Régis-Gianas regisgia +Clément Renard clrenard +Claudio Sacerdoti Coen sacerdot +Vincent Siles vsiles +Elie Soubiran soubiran +Matthieu Sozeau msozeau +Matthieu Sozeau Matthieu Sozeau +Arnaud Spiwack aspiwack +Enrico Tassi gareuselesinge +Enrico Tassi Enrico Tassi +Enrico Tassi Enrico Tassi +Laurent Théry thery +Benjamin Werner werner + +# Anonymous accounts + +anonymous < > coq +anonymous < > (no author) <(no author)@85f007b7-540e-0410-9357-904b9bb8a0f7> +anonymous < > serpyc diff --git a/CHANGES b/CHANGES index 57bb9f19..7b50dfae 100644 --- a/CHANGES +++ b/CHANGES @@ -1,3 +1,108 @@ +Changes from V8.5beta2 to V8.5beta3 +=================================== + +Vernacular commands + +- New command "Redirect" to redirect the output of a command to a file. +- New command "Undelimit Scope" to remove the delimiter of a scope. +- New option "Strict Universe Declaration", set by default. It enforces the + declaration of all polymorphic universes appearing in a definition when + introducing it. +- New command "Show id" to show goal named id. + +Tactics + +- New flag "Regular Subst Tactic" which fixes "subst" in situations where + it failed to substitute all substitutable equations or failed to simplify + cycles, or accidentally unfolded local definitions (flag is off by default). +- New flag "Loose Hint Behavior" to handle hints loaded but not imported in a + special way. It accepts three distinct flags: + * "Lax", which is the default one, sets the old behavior, i.e. a non-imported + hint behaves the same as an imported one. + * "Warn" outputs a warning when a non-imported hint is used. Note that this is + an over-approximation, because a hint may be triggered by an eauto run that + will eventually fail and backtrack. + * "Strict" changes the behavior of an unloaded hint to the one of the fail + tactic, allowing to emulate the hopefully future import-scoped hint mechanism. +- New compatibility flag "Universal Lemma Under Conjunction" which + let tactics working under conjunctions apply sublemmas of the form + "forall A, ... -> A". +- New compatibility flag "Bracketing Last Introduction Pattern" which can be + set so that the last disjunctive-conjunctive introduction pattern given to + "intros" automatically complete the introduction of its subcomponents, as the + the disjunctive-conjunctive introduction patterns in non-terminal position + already do. +- Importing Program no longer overrides the "exists" tactic (potential source + of incompatibilities). +- Hints costs are now correctly taken into account (potential source of + incompatibilities). +- Documented the Hint Cut command that allows control of the + proof-search during typeclass resolution (see reference manual). + +API + +- Some functions from pretyping/typing.ml and their derivatives were potential + source of evarmap leaks, as they dropped their resulting evarmap. The + situation was clarified by renaming them according to a unsafe_* scheme. Their + sound variant is likewise renamed to their old name. The following renamings + were made. + * Typing.type_of -> unsafe_type_of + * Typing.e_type_of -> type_of + * A new e_type_of function that matches the e_ prefix policy + * Tacmach.pf_type_of -> pf_unsafe_type_of + * A new safe pf_type_of function. + All uses of unsafe_* functions should be eventually eliminated. + +Tools + +- Added an option -w to control the output of coqtop warnings. +- Configure now takes an optional -native-compiler (yes|no) flag replacing + -no-native-compiler. The new flag is set to no by default under Windows. +- Flag -no-native-compiler was removed and became the default for coqc. If + precompilation of files for native conversion test is desired, use + -native-compiler. +- The -compile command-line option now takes the full path of the considered + file, including the ".v" extension, and outputs a warning if such an extension + is lacking. +- The -require and -load-vernac-object command-line options now take a logical + path of a given library rather than a physical path, thus they behave like + Require [Import] path. + +Changes from V8.5beta1 to V8.5beta2 +=================================== + +Logic + +- The VM now supports inductive types with up to 8388851 non-constant + constructors and up to 8388607 constant ones. + +Tactics + +- A script using the admit tactic can no longer be concluded by either + Qed or Defined. In the first case, Admitted can be used instead. In + the second case, a subproof should be used. +- The easy tactic and the now tactical now have a more predictable + behavior, but they might now discharge some previously unsolved goals. + +Extraction + +- Definitions extracted to Haskell GHC should no longer randomly + segfault when some Coq types cannot be represented by Haskell types. +- Definitions can now be extracted to Json for post-processing. + +Tools + +- Option -I -as has been removed, and option -R -as has been + deprecated. In both cases, option -R can be used instead. +- coq_makefile now generates double-colon rules for rules such as clean. + +API + +- The interface of [change] has changed to take a [change_arg], which + can be built from a [constr] using [make_change_arg]. +- [pattern_of_constr] now returns a triplet including the cleaned-up + [evar_map], removing the evars that were turned into metas. + Changes from V8.4 to V8.5beta1 ============================== @@ -84,12 +189,13 @@ Specification Language break user notations using "$(", fixable by inserting a space or rewriting the notation). - Constructors in pattern-matching patterns now respect the same rules - regarding implicit arguments than in applicative position. The old + regarding implicit arguments as in applicative position. The old behavior can be recovered by the command "Set Asymmetric - Patterns". As a side effect, Much more notations can be used in - patterns. Considering that the pattern language is rich enough like - that, definitions are now always forbidden in patterns. (source of - incompatibilities for definitions that delta-reduce to a constructor) + Patterns". As a side effect, notations for constructors explicitly + mentioning non-implicit parameters can now be used in patterns. + Considering that the pattern language is already rich enough, binding + local definitions is however now forbidden in patterns (source of + incompatibilities for local definitions that delta-reduce to a constructor). - Type inference algorithm now granting opacity of constants. This might also affect behavior of tactics (source of incompatibilities, solvable by re-declaring transparent constants which were set opaque). @@ -110,10 +216,12 @@ Tactics during the execution of c, it can backtrack and try b instead of a. * New tactical (once a) removes all the backtracking points from a (i.e. it selects the first success of a). - * Tactic "constructor" is now fully backtracking, thus deprecating - the need of the undocumented "constructor " syntax which is - now equivalent to "[> once (constructor; tac) ..]". (potential - source of rare incompatibilities). + * Tactic "constructor" is now fully backtracking. In case of + incompatibilities (e.g. combinatoric explosion), the former + behavior of "constructor" can be retrieved by using instead + "[> once constructor ..]". Thanks to backtracking, undocumented + "constructor " syntax is now equivalent to + "[> once (constructor; tac) ..]". * New "multimatch" variant of "match" tactic which backtracks to new branches in case of a later failure. The "match" tactic is equivalent to "once multimatch". @@ -279,6 +387,10 @@ Tactics trace anymore. Use "Info 1 auto" instead. The same goes for "info_trivial". On the other hand "info_eauto" still works fine, while "Info 1 eauto" prints a trivial trace. +- When using a lemma of the prototypical form "forall A, {a:A & P a}", + "apply" and "apply in" do not instantiate anymore "A" with the + current goal and use "a" as the proof, as they were sometimes doing, + now considering that it is a too powerful decision. Program @@ -342,7 +454,7 @@ Interfaces - Many CoqIDE windows, including the query one, are now detachable to improve usability on multi screen work stations. -- Coqtop outputs highlighted syntax. Colors can be configured thanks +- Coqtop/coqc outputs highlighted syntax. Colors can be configured thanks to the COQ_COLORS environment variable, and their current state can be displayed with the -list-tags command line option. @@ -2076,7 +2188,7 @@ Changes from V7.3.1 to V7.4 Symbolic notations - Introduction of a notion of scope gathering notations in a consistent set; - a notation sets has been developped for nat, Z and R (undocumented) + a notation sets has been developed for nat, Z and R (undocumented) - New command "Notation" for declaring notations simultaneously for parsing and printing (see chap 10 of the reference manual) - Declarations with only implicit arguments now handled (e.g. the diff --git a/INSTALL b/INSTALL index 955e605c..83c1b9f3 100644 --- a/INSTALL +++ b/INSTALL @@ -55,10 +55,12 @@ QUICK INSTALLATION PROCEDURE. INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= -1- Check that you have the Objective Caml compiler version 3.12.1 (or later) - installed on your computer and that "ocamlc" (or its native code version - "ocamlc.opt") lie in a directory which is present in your $PATH environment - variable. +1- Check that you have the Objective Caml compiler installed on your + computer and that "ocamlc" (or, better, its native code version + "ocamlc.opt") lies in a directory which is present in your $PATH + environment variable. At the time of writing this sentence, all + versions of Objective Caml later or equal to 3.12.1 are + supported to the exception of Objective Caml 4.02.0. To get Coq in native-code, (it runs 4 to 10 times faster than bytecode, but it takes more time to get compiled and the binary is diff --git a/INSTALL.doc b/INSTALL.doc index 96918b49..76588005 100644 --- a/INSTALL.doc +++ b/INSTALL.doc @@ -1,7 +1,7 @@ The Coq documentation ===================== -The Coq documentation includes +The Coq documentation includes - A Reference Manual - A Tutorial @@ -15,31 +15,25 @@ html files are generated. Prerequisite ------------ -To produce the PostScript documents, the following tools -are needed: +To produce all the documents, the following tools are needed: - latex (latex2e) + - pdflatex - dvips - bibtex - makeindex - - pngtopnm and pnmtops (for the Reference Manual and the FAQ) - -To produce the PDF documents, the following tools are needed: - - - pdflatex - - bibtex - -To produce the html documents, the following tools are needed: - - - hevea (e.g. 1.07 works) + - fig2dev + - convert + - hevea + - hacha Under Debian based operating systems (Debian, Ubuntu, ...) a working set of packages for compiling the documentation for Coq is: texlive texlive-latex-extra texlive-math-extra texlive-fonts-extra - texlive-lang-french texlive-humanities texlive-pictures latex-xcolor - hevea netpbm + texlive-humanities texlive-pictures latex-xcolor hevea transfig + imagemagick Compilation @@ -52,7 +46,7 @@ To produce all documentation about Coq, just run: Alternatively, you can use some specific targets: - make doc-ps + make doc-ps to produce all PostScript documents make doc-pdf @@ -74,7 +68,7 @@ Alternatively, you can use some specific targets: to produce all formats of the FAQ make stdlib - to produce all formats of the Coq standard library + to produce all formats of the Coq standard library Installation diff --git a/INSTALL.ide b/INSTALL.ide index 13e741e3..6e41b2d0 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -119,5 +119,5 @@ TROUBLESHOOTING rid of the problem is to edit by hand your coqiderc (either /home//.config/coq/coqiderc under Linux, or C:\Documents and Settings\\.config\coq\coqiderc under Windows) - and replace any occurence of MOD4 by MOD1. + and replace any occurrence of MOD4 by MOD1. diff --git a/Makefile b/Makefile index 554718bc..bb51e3dd 100644 --- a/Makefile +++ b/Makefile @@ -202,7 +202,8 @@ docclean: rm -f doc/stdlib/index-list.html doc/stdlib/index-body.html \ doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \ doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex - rm -f doc/*/*.ps doc/*/*.pdf + rm -f doc/*/*.ps doc/*/*.pdf doc/*/*.eps doc/*/*.pdf_t doc/*/*.eps_t + rm -f doc/faq/axioms.png rm -rf doc/refman/html doc/stdlib/html doc/faq/html doc/tutorial/tutorial.v.html rm -f doc/refman/euclid.ml doc/refman/euclid.mli rm -f doc/refman/heapsort.ml doc/refman/heapsort.mli diff --git a/Makefile.build b/Makefile.build index 018471b6..0455a247 100644 --- a/Makefile.build +++ b/Makefile.build @@ -69,7 +69,7 @@ TIMED= # non-empty will activate a default time command TIMECMD= # if you prefer a specific time command instead of $(STDTIME) # e.g. "'time -p'" - +CAMLFLAGS:=${CAMLFLAGS} -w -3 # NB: if you want to collect compilation timings of .v and import them # in a spreadsheet, I suggest something like: # make TIMED=1 2> timings.csv @@ -81,7 +81,7 @@ TIMECMD= # if you prefer a specific time command instead of $(STDTIME) STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) -COQOPTS=$(COQ_XML) $(VM) +COQOPTS=$(COQ_XML) $(VM) $(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile # The SHOW and HIDE variables control whether make will echo complete commands @@ -101,7 +101,7 @@ BYTEFLAGS=-thread $(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=-thread $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils -ifeq ($(shell which codesign > /dev/null && echo $(ARCH)),Darwin) +ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin) LINKMETADATA=-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist" CODESIGN:=codesign -s - else @@ -282,11 +282,11 @@ $(COQC): $(patsubst %.cma,%$(BESTLIB),$(COQCCMO:.cmo=$(BESTOBJ))) # For the checker, different flags may be used -checker/check.cma: | checker/check.mllib.d +checker/check.cma: | md5chk checker/check.mllib.d $(SHOW)'OCAMLC -a -o $@' $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -a -o $@ $^ -checker/check.cmxa: | checker/check.mllib.d +checker/check.cmxa: | md5chk checker/check.mllib.d $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $^ @@ -479,7 +479,7 @@ md5chk: VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m -validate: $(CHICKEN) md5chk | $(ALLVO) +validate: $(CHICKEN) | $(ALLVO) $(SHOW)'COQCHK ' $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS) @@ -524,6 +524,7 @@ hightactics: tactics/hightactics.cma .PHONY: init theories theories-light .PHONY: logic arith bool narith zarith qarith lists strings sets .PHONY: fsets relations wellfounded reals setoids sorting numbers noreal +.PHONY: msets mmaps compat init: $(INITVO) @@ -551,6 +552,9 @@ classes: $(CLASSESVO) program: $(PROGRAMVO) structures: $(STRUCTURESVO) vectors: $(VECTORSVO) +msets: $(MSETSVO) +mmaps: $(MMAPSVO) +compat: $(COMPATVO) noreal: unicode logic arith bool zarith qarith lists sets fsets \ relations wellfounded setoids sorting @@ -584,7 +588,7 @@ pluginsbyte: $(PLUGINS) theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d $(SHOW)'COQC -noinit $<' $(HIDE)rm -f theories/Init/$*.glob - $(HIDE)$(BOOTCOQC) theories/Init/$* -noinit -R theories Coq + $(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq theories/Numbers/Natural/BigN/NMake_gen.v: theories/Numbers/Natural/BigN/NMake_gen.ml $(OCAML) $< $(TOTARGET) @@ -654,7 +658,7 @@ $(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) # votour: a small vo explorer (based on the checker) -bin/votour: lib/cObj$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml +bin/votour: lib/cObj$(BESTOBJ) checker/analyze$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml $(SHOW)'OCAMLBEST -o $@' $(HIDE)$(call bestocaml, -I checker,) @@ -1035,7 +1039,7 @@ plugins/%_mod.ml: plugins/%.mllib %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d $(SHOW)'COQC $<' $(HIDE)rm -f $*.glob - $(HIDE)$(BOOTCOQC) $* + $(HIDE)$(BOOTCOQC) $< ifdef VALIDATE $(SHOW)'COQCHK $(call vo_to_mod,$@)' $(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ diff --git a/Makefile.common b/Makefile.common index 07df8bb1..92a48cd6 100644 --- a/Makefile.common +++ b/Makefile.common @@ -109,7 +109,11 @@ LATEX:=latex BIBTEX:=BIBINPUTS=.: bibtex -min-crossrefs=10 MAKEINDEX:=makeindex PDFLATEX:=pdflatex +DVIPS:=dvips +FIG2DEV:=fig2dev +CONVERT:=convert HEVEA:=hevea +HACHA:=hacha HEVEAOPTS:=-fix -exec xxdate.exe HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea HTMLSTYLE:=simple @@ -127,13 +131,14 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-decl.v.tex RefMan-pro.v.tex RefMan-sch.v.tex \ Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \ Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ - Setoid.v.tex Classes.v.tex AsyncProofs.v.tex Universes.v.tex \ + Setoid.v.tex Classes.v.tex Universes.v.tex \ Misc.v.tex) REFMANTEXFILES:=$(addprefix doc/refman/, \ headers.sty Reference-Manual.tex \ RefMan-pre.tex RefMan-int.tex RefMan-com.tex \ - RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex ) \ + RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex \ + AsyncProofs.tex ) \ $(REFMANCOQTEXFILES) \ REFMANEPSFILES:=doc/refman/coqide.eps doc/refman/coqide-queries.eps @@ -297,6 +302,7 @@ SETOIDSVO:=$(call cat_vo_itarget, theories/Setoids) UNICODEVO:=$(call cat_vo_itarget, theories/Unicode) CLASSESVO:=$(call cat_vo_itarget, theories/Classes) PROGRAMVO:=$(call cat_vo_itarget, theories/Program) +COMPATVO:=$(call cat_vo_itarget, theories/Compat) THEORIESVO:=\ $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) \ @@ -306,7 +312,8 @@ THEORIESVO:=\ $(PARITHVO) $(NARITHVO) $(ZARITHVO) \ $(SETSVO) $(FSETSVO) $(MSETSVO) $(MMAPSVO) \ $(REALSVO) $(SORTINGVO) $(QARITHVO) \ - $(NUMBERSVO) $(STRUCTURESVO) $(VECTORSVO) + $(NUMBERSVO) $(STRUCTURESVO) $(VECTORSVO) \ + $(COMPATVO) THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(UNICODEVO) $(ARITHVO) diff --git a/Makefile.doc b/Makefile.doc index 1f350935..b7251ce5 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -58,7 +58,21 @@ else endif %.ps: %.dvi - (cd `dirname $<`; dvips -q -o `basename $@` `basename $<`) + (cd `dirname $<`; $(DVIPS) -q -o `basename $@` `basename $<`) + +%.png: %.fig + $(FIG2DEV) -m 2 -L png $< $@ + +%.pdf: %.fig + $(FIG2DEV) -L pdftex $< $@ + $(FIG2DEV) -L pdftex_t -p `basename $@` $< $@_t + +%.eps: %.fig + $(FIG2DEV) -L pstex $< $@ + $(FIG2DEV) -L pstex_t -p `basename $@` $< $@_t + +%.eps: %.png + $(CONVERT) $< $@ ###################################################################### # Macros for filtering outputs @@ -107,7 +121,7 @@ doc/refman/Reference-Manual.dvi: $(REFMANFILES) doc/refman/Reference-Manual.tex $(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\ ../tools/show_latex_messages -no-overfull Reference-Manual.log) -doc/refman/Reference-Manual.pdf: doc/refman/Reference-Manual.dvi +doc/refman/Reference-Manual.pdf: doc/refman/Reference-Manual.dvi $(REFMANPNGFILES) (cd doc/refman;\ $(PDFLATEX) -interaction=batchmode Reference-Manual.tex;\ ../tools/show_latex_messages -no-overfull Reference-Manual.log) @@ -133,7 +147,7 @@ refman-html-dir: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \ - rm -rf doc/refman/html $(MKDIR) doc/refman/html $(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html - (cd doc/refman/html; hacha -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html) + (cd doc/refman/html; $(HACHA) -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html) $(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html -$(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html @@ -173,7 +187,7 @@ doc/tutorial/Tutorial.v.html: $(DOCCOMMON) doc/tutorial/Tutorial.v.tex # FAQ ###################################################################### -doc/faq/FAQ.v.dvi: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.tex +doc/faq/FAQ.v.dvi: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.tex doc/faq/axioms.eps (cd doc/faq;\ $(LATEX) -interaction=batchmode FAQ.v;\ $(BIBTEX) -terse FAQ.v;\ @@ -181,12 +195,12 @@ doc/faq/FAQ.v.dvi: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.tex $(LATEX) -interaction=batchmode FAQ.v > /dev/null;\ ../tools/show_latex_messages FAQ.v.log) -doc/faq/FAQ.v.pdf: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.dvi doc/faq/axioms.png +doc/faq/FAQ.v.pdf: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.dvi doc/faq/axioms.pdf (cd doc/faq;\ $(PDFLATEX) -interaction=batchmode FAQ.v.tex;\ ../tools/show_latex_messages FAQ.v.log) -doc/faq/FAQ.v.html: doc/faq/FAQ.v.dvi # to ensure FAQ.v.bbl +doc/faq/FAQ.v.html: doc/faq/FAQ.v.dvi doc/faq/axioms.png # to ensure FAQ.v.bbl (cd doc/faq; ($(HEVEA) $(HEVEAOPTS) FAQ.v.tex $(HEVEAFAQFILTER))) doc/faq/html/index.html: doc/faq/FAQ.v.html diff --git a/README.doc b/README.doc old mode 100755 new mode 100644 diff --git a/checker/analyze.ml b/checker/analyze.ml new file mode 100644 index 00000000..c48b8301 --- /dev/null +++ b/checker/analyze.ml @@ -0,0 +1,350 @@ +(** Headers *) + +let prefix_small_block = 0x80 +let prefix_small_int = 0x40 +let prefix_small_string = 0x20 + +let code_int8 = 0x00 +let code_int16 = 0x01 +let code_int32 = 0x02 +let code_int64 = 0x03 +let code_shared8 = 0x04 +let code_shared16 = 0x05 +let code_shared32 = 0x06 +let code_double_array32_little = 0x07 +let code_block32 = 0x08 +let code_string8 = 0x09 +let code_string32 = 0x0A +let code_double_big = 0x0B +let code_double_little = 0x0C +let code_double_array8_big = 0x0D +let code_double_array8_little = 0x0E +let code_double_array32_big = 0x0F +let code_codepointer = 0x10 +let code_infixpointer = 0x11 +let code_custom = 0x12 +let code_block64 = 0x13 + +type code_descr = +| CODE_INT8 +| CODE_INT16 +| CODE_INT32 +| CODE_INT64 +| CODE_SHARED8 +| CODE_SHARED16 +| CODE_SHARED32 +| CODE_DOUBLE_ARRAY32_LITTLE +| CODE_BLOCK32 +| CODE_STRING8 +| CODE_STRING32 +| CODE_DOUBLE_BIG +| CODE_DOUBLE_LITTLE +| CODE_DOUBLE_ARRAY8_BIG +| CODE_DOUBLE_ARRAY8_LITTLE +| CODE_DOUBLE_ARRAY32_BIG +| CODE_CODEPOINTER +| CODE_INFIXPOINTER +| CODE_CUSTOM +| CODE_BLOCK64 + +let code_max = 0x13 + +let magic_number = "\132\149\166\190" + +(** Memory reification *) + +type repr = +| RInt of int +| RBlock of (int * int) (* tag × len *) +| RString of string +| RPointer of int +| RCode of int + +type data = +| Int of int (* value *) +| Ptr of int (* pointer *) +| Atm of int (* tag *) +| Fun of int (* address *) + +type obj = +| Struct of int * data array (* tag × data *) +| String of string + +module type Input = +sig + type t + val input_byte : t -> int + val input_binary_int : t -> int +end + +module type S = +sig + type input + val parse : input -> (data * obj array) +end + +module Make(M : Input) = +struct + +open M + +type input = M.t + +let current_offset = ref 0 + +let input_byte chan = + let () = incr current_offset in + input_byte chan + +let input_binary_int chan = + let () = current_offset := !current_offset + 4 in + input_binary_int chan + +let input_char chan = Char.chr (input_byte chan) + +let parse_header chan = + let () = current_offset := 0 in + let magic = String.create 4 in + let () = for i = 0 to 3 do magic.[i] <- input_char chan done in + let length = input_binary_int chan in + let objects = input_binary_int chan in + let size32 = input_binary_int chan in + let size64 = input_binary_int chan in + (magic, length, size32, size64, objects) + +let input_int8s chan = + let i = input_byte chan in + if i land 0x80 = 0 + then i + else i lor ((-1) lsl 8) + +let input_int8u = input_byte + +let input_int16s chan = + let i = input_byte chan in + let j = input_byte chan in + let ans = (i lsl 8) lor j in + if i land 0x80 = 0 + then ans + else ans lor ((-1) lsl 16) + +let input_int16u chan = + let i = input_byte chan in + let j = input_byte chan in + (i lsl 8) lor j + +let input_int32s chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let ans = (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l in + if i land 0x80 = 0 + then ans + else ans lor ((-1) lsl 31) + +let input_int32u chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l + +let input_int64s chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let m = input_byte chan in + let n = input_byte chan in + let o = input_byte chan in + let p = input_byte chan in + let ans = + (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor + (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor p + in + if i land 0x80 = 0 + then ans + else ans lor ((-1) lsl 63) + +let input_int64u chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let m = input_byte chan in + let n = input_byte chan in + let o = input_byte chan in + let p = input_byte chan in + (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor + (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor p + +let input_header32 chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let tag = l in + let len = (i lsl 14) lor (j lsl 6) lor (k lsr 2) in + (tag, len) + +let input_header64 chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let m = input_byte chan in + let n = input_byte chan in + let o = input_byte chan in + let p = input_byte chan in + let tag = p in + let len = + (i lsl 46) lor (j lsl 38) lor (k lsl 30) lor (l lsl 22) lor + (m lsl 14) lor (n lsl 6) lor (o lsr 2) + in + (tag, len) + +let input_string len chan = + let ans = String.create len in + for i = 0 to pred len do + ans.[i] <- input_char chan; + done; + ans + +let parse_object chan = + let data = input_byte chan in + if prefix_small_block <= data then + let tag = data land 0x0F in + let len = (data lsr 4) land 0x07 in + RBlock (tag, len) + else if prefix_small_int <= data then + RInt (data land 0x3F) + else if prefix_small_string <= data then + let len = data land 0x1F in + RString (input_string len chan) + else if data > code_max then + assert false + else match (Obj.magic data) with + | CODE_INT8 -> + RInt (input_int8s chan) + | CODE_INT16 -> + RInt (input_int16s chan) + | CODE_INT32 -> + RInt (input_int32s chan) + | CODE_INT64 -> + RInt (input_int64s chan) + | CODE_SHARED8 -> + RPointer (input_int8u chan) + | CODE_SHARED16 -> + RPointer (input_int16u chan) + | CODE_SHARED32 -> + RPointer (input_int32u chan) + | CODE_BLOCK32 -> + RBlock (input_header32 chan) + | CODE_BLOCK64 -> + RBlock (input_header64 chan) + | CODE_STRING8 -> + let len = input_int8u chan in + RString (input_string len chan) + | CODE_STRING32 -> + let len = input_int32u chan in + RString (input_string len chan) + | CODE_CODEPOINTER -> + let addr = input_int32u chan in + for i = 0 to 15 do ignore (input_byte chan); done; + RCode addr + | CODE_DOUBLE_ARRAY32_LITTLE + | CODE_DOUBLE_BIG + | CODE_DOUBLE_LITTLE + | CODE_DOUBLE_ARRAY8_BIG + | CODE_DOUBLE_ARRAY8_LITTLE + | CODE_DOUBLE_ARRAY32_BIG + | CODE_INFIXPOINTER + | CODE_CUSTOM -> + Printf.eprintf "Unhandled code %04x\n%!" data; assert false + +let parse chan = + let (magic, len, _, _, size) = parse_header chan in + let () = assert (magic = magic_number) in + let memory = Array.make size (Struct ((-1), [||])) in + let current_object = ref 0 in + let fill_obj = function + | RPointer n -> + let data = Ptr (!current_object - n) in + data, None + | RInt n -> + let data = Int n in + data, None + | RString s -> + let data = Ptr !current_object in + let () = memory.(!current_object) <- String s in + let () = incr current_object in + data, None + | RBlock (tag, 0) -> + (* Atoms are never shared *) + let data = Atm tag in + data, None + | RBlock (tag, len) -> + let data = Ptr !current_object in + let nblock = Array.make len (Atm (-1)) in + let () = memory.(!current_object) <- Struct (tag, nblock) in + let () = incr current_object in + data, Some nblock + | RCode addr -> + let data = Fun addr in + data, None + in + + let rec fill block off accu = + if Array.length block = off then + match accu with + | [] -> () + | (block, off) :: accu -> fill block off accu + else + let data, nobj = fill_obj (parse_object chan) in + let () = block.(off) <- data in + let block, off, accu = match nobj with + | None -> block, succ off, accu + | Some nblock -> nblock, 0, ((block, succ off) :: accu) + in + fill block off accu + in + let ans = [|Atm (-1)|] in + let () = fill ans 0 [] in + (ans.(0), memory) + +end + +module IChannel = +struct + type t = in_channel + let input_byte = Pervasives.input_byte + let input_binary_int = Pervasives.input_binary_int +end + +module IString = +struct + type t = (string * int ref) + + let input_byte (s, off) = + let ans = Char.code (s.[!off]) in + let () = incr off in + ans + + let input_binary_int chan = + let i = input_byte chan in + let j = input_byte chan in + let k = input_byte chan in + let l = input_byte chan in + let ans = (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l in + if i land 0x80 = 0 + then ans + else ans lor ((-1) lsl 31) + +end + +module PChannel = Make(IChannel) +module PString = Make(IString) + +let parse_channel = PChannel.parse +let parse_string s = PString.parse (s, ref 0) diff --git a/checker/analyze.mli b/checker/analyze.mli new file mode 100644 index 00000000..42efcf01 --- /dev/null +++ b/checker/analyze.mli @@ -0,0 +1,35 @@ +type data = +| Int of int +| Ptr of int +| Atm of int (* tag *) +| Fun of int (* address *) + +type obj = +| Struct of int * data array (* tag × data *) +| String of string + +val parse_channel : in_channel -> (data * obj array) +val parse_string : string -> (data * obj array) + +(** {6 Functorized version} *) + +module type Input = +sig + type t + val input_byte : t -> int + (** Input a single byte *) + val input_binary_int : t -> int + (** Input a big-endian 31-bits signed integer *) +end +(** Type of inputs *) + +module type S = +sig + type input + val parse : input -> (data * obj array) + (** Return the entry point and the reification of the memory out of a + marshalled structure. *) +end + +module Make (M : Input) : S with type input = M.t +(** Functorized version of the previous code. *) diff --git a/checker/check.ml b/checker/check.ml index 3e22c4b1..21c8f1c5 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -46,7 +46,7 @@ type library_t = { library_opaques : Cic.opaque_table; library_deps : Cic.library_deps; library_digest : Cic.vodigest; - library_extra_univs : Univ.constraints } + library_extra_univs : Univ.ContextSet.t } module LibraryOrdered = struct @@ -97,7 +97,7 @@ let access_opaque_univ_table dp i = let t = LibraryMap.find dp !opaque_univ_tables in assert (i < Array.length t); Future.force t.(i) - with Not_found -> Univ.empty_constraint + with Not_found -> Univ.ContextSet.empty let _ = Declarations.indirect_opaque_access := access_opaque_table @@ -271,32 +271,22 @@ let try_locate_qualified_library qid = | LibNotFound -> error_lib_not_found qid (************************************************************************) -(*s Low-level interning/externing of libraries to files *) +(*s Low-level interning of libraries from files *) -(*s Loading from disk to cache (preparation phase) *) - -let raw_intern_library = - snd (System.raw_extern_intern Coq_config.vo_magic_number) - -let with_magic_number_check f a = - try f a - with System.Bad_magic_number fname -> - errorlabstrm "with_magic_number_check" - (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++ - spc () ++ str"It is corrupted" ++ spc () ++ - str"or was compiled with another version of Coq.") +let raw_intern_library f = + System.raw_intern_state Coq_config.vo_magic_number f (************************************************************************) (* Internalise libraries *) open Cic -let mk_library md f table digest cst = { - library_name = md.md_name; +let mk_library sd md f table digest cst = { + library_name = sd.md_name; library_filename = f; library_compiled = md.md_compiled; library_opaques = table; - library_deps = md.md_deps; + library_deps = sd.md_deps; library_digest = digest; library_extra_univs = cst } @@ -310,10 +300,11 @@ let depgraph = ref LibraryMap.empty let intern_from_file (dir, f) = Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush (); - let (md,table,opaque_csts,digest) = + let (sd,md,table,opaque_csts,digest) = try - let ch = with_magic_number_check raw_intern_library f in - let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in + let ch = System.with_magic_number_check raw_intern_library f in + let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in + let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in let (discharging:'a option), _, _ = System.marshal_in_segment f ch in let (tasks:'a option), _, _ = System.marshal_in_segment f ch in @@ -325,9 +316,9 @@ let intern_from_file (dir, f) = if not (String.equal (Digest.channel ch pos) checksum) then errorlabstrm "intern_from_file" (str "Checksum mismatch"); let () = close_in ch in - if dir <> md.md_name then + if dir <> sd.md_name then errorlabstrm "intern_from_file" - (name_clash_message dir md.md_name f); + (name_clash_message dir sd.md_name f); if tasks <> None || discharging <> None then errorlabstrm "intern_from_file" (str "The file "++str f++str " contains unfinished tasks"); @@ -340,25 +331,25 @@ let intern_from_file (dir, f) = Validate.validate !Flags.debug Values.v_univopaques opaque_csts; end; (* Verification of the unmarshalled values *) + Validate.validate !Flags.debug Values.v_libsum sd; Validate.validate !Flags.debug Values.v_lib md; Validate.validate !Flags.debug Values.v_opaques table; Flags.if_verbose ppnl (str" done]"); pp_flush (); let digest = if opaque_csts <> None then Cic.Dviovo (digest,udg) else (Cic.Dvo digest) in - md,table,opaque_csts,digest + sd,md,table,opaque_csts,digest with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in - depgraph := LibraryMap.add md.md_name md.md_deps !depgraph; - opaque_tables := LibraryMap.add md.md_name table !opaque_tables; + depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph; + opaque_tables := LibraryMap.add sd.md_name table !opaque_tables; Option.iter (fun (opaque_csts,_,_) -> opaque_univ_tables := - LibraryMap.add md.md_name opaque_csts !opaque_univ_tables) + LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables) opaque_csts; let extra_cst = - Option.default Univ.empty_constraint - (Option.map (fun (_,cs,_) -> - Univ.ContextSet.constraints cs) opaque_csts) in - mk_library md f table digest extra_cst + Option.default Univ.ContextSet.empty + (Option.map (fun (_,cs,_) -> cs) opaque_csts) in + mk_library sd md f table digest extra_cst let get_deps (dir, f) = try LibraryMap.find dir !depgraph diff --git a/checker/check.mllib b/checker/check.mllib index 22df3756..49ca6bf0 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,6 +1,7 @@ Coq_config Hook +Terminal Canary Hashset Hashcons @@ -23,13 +24,14 @@ Pp Segmenttree Unicodetable Unicode -Errors CObj CList CString CArray CStack Util +Ppstyle +Errors Ephemeron Future CUnix diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 05a2a1b9..d041f1b7 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -23,11 +23,17 @@ let print_memory_stat () = let output_context = ref false -let pr_engt = function - Some ImpredicativeSet -> - str "Theory: Set is impredicative" - | None -> - str "Theory: Set is predicative" +let pr_engagement (impr_set,type_in_type) = + begin + match impr_set with + | ImpredicativeSet -> str "Theory: Set is impredicative" + | PredicativeSet -> str "Theory: Set is predicative" + end ++ + begin + match type_in_type with + | StratifiedType -> str "Theory: Stratified type hierarchy" + | TypeInType -> str "Theory: Type is of type Type" + end let cst_filter f csts = Cmap_env.fold @@ -54,7 +60,7 @@ let print_context env = ppnl(hov 0 (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++ str"===============" ++ fnl() ++ fnl() ++ - str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++ + str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_ax csts) ++ fnl())); pp_flush() end diff --git a/checker/checker.ml b/checker/checker.ml index 9a1007ac..d5d9b9e3 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -67,13 +67,13 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = Check.add_load_path (dir,coq_dirpath) end else - msg_warning (str ("Cannot open " ^ dir)) + msg_warning (str "Cannot open " ++ str dir) let convert_string d = try Id.of_string d with Errors.UserError _ -> if_verbose msg_warning - (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)")); + (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit let add_rec_path ~unix_path ~coq_root = @@ -90,7 +90,7 @@ let add_rec_path ~unix_path ~coq_root = List.iter Check.add_load_path dirs; Check.add_load_path (unix_path, coq_root) else - msg_warning (str ("Cannot open " ^ unix_path)) + msg_warning (str "Cannot open " ++ str unix_path) (* By the option -include -I or -R of the command line *) let includes = ref [] @@ -138,10 +138,11 @@ let init_load_path () = let set_debug () = Flags.debug := true -let engagement = ref None -let set_engagement c = engagement := Some c -let engage () = - match !engagement with Some c -> Safe_typing.set_engagement c | None -> () +let impredicative_set = ref Cic.PredicativeSet +let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet +let type_in_type = ref Cic.StratifiedType +let set_type_in_type () = type_in_type := Cic.TypeInType +let engage () = Safe_typing.set_engagement (!impredicative_set,!type_in_type) let admit_list = ref ([] : section_path list) @@ -194,6 +195,7 @@ let print_usage_channel co command = \n -silent disable trace of constants being checked\ \n\ \n -impredicative-set set sort Set impredicative\ +\n -type-in-type collapse type hierarchy\ \n\ \n -h, --help print this list of options\ \n" @@ -221,7 +223,7 @@ let print_loc loc = else let loc = Loc.unloc loc in (int (fst loc) ++ str"-" ++ int (snd loc)) -let guill s = "\""^s^"\"" +let guill s = str "\"" ++ str s ++ str "\"" let where s = if !Flags.debug then (str"in " ++ str s ++ str":" ++ spc ()) else (mt ()) @@ -232,7 +234,7 @@ let rec explain_exn = function | Stream.Error txt -> hov 0 (str "Syntax error: " ++ str txt) | Sys_error msg -> - hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report() ) + hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ guill msg ++ report() ) | UserError(s,pps) -> hov 1 (str "User error: " ++ where s ++ pps) | Out_of_memory -> @@ -241,14 +243,14 @@ let rec explain_exn = function hov 0 (str "Stack overflow") | Match_failure(filename,pos1,pos2) -> hov 1 (anomaly_string () ++ str "Match failure in file " ++ - str (guill filename) ++ str " at line " ++ int pos1 ++ + guill filename ++ str " at line " ++ int pos1 ++ str " character " ++ int pos2 ++ report ()) | Not_found -> hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ()) | Failure s -> hov 0 (str "Failure: " ++ str s ++ report ()) | Invalid_argument s -> - hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ()) + hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ guill s ++ report ()) | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.") | Univ.UniverseInconsistency (o,u,v) -> @@ -294,7 +296,7 @@ let rec explain_exn = function Format.printf "@\n====== universes ====@\n"; Pp.pp (Univ.pr_universes (ctx.Environ.env_stratification.Environ.env_universes)); - str("\nCantApplyBadType at argument " ^ string_of_int n) + str "\nCantApplyBadType at argument " ++ int n | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" | IllFormedRecBody _ -> str"IllFormedRecBody" | IllTypedRecBody _ -> str"IllTypedRecBody" @@ -309,7 +311,7 @@ let rec explain_exn = function hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++ (if s = "" then mt () else - (str ("(file \"" ^ s ^ "\", line ") ++ int b ++ + (str "(file \"" ++ str s ++ str "\", line " ++ int b ++ str ", characters " ++ int e ++ str "-" ++ int (e+6) ++ str ")")) ++ report ()) @@ -319,11 +321,13 @@ let parse_args argv = let rec parse = function | [] -> () | "-impredicative-set" :: rem -> - set_engagement Cic.ImpredicativeSet; parse rem + set_impredicative_set (); parse rem + | "-type-in-type" :: rem -> + set_type_in_type (); parse rem | "-coqlib" :: s :: rem -> if not (exists_dir s) then - fatal_error (str ("Directory '"^s^"' does not exist")) false; + fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false; Flags.coqlib := s; Flags.coqlib_spec := true; parse rem diff --git a/checker/cic.mli b/checker/cic.mli index 90a0e9fe..bd75111a 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -102,7 +102,7 @@ type constr = | Case of case_info * constr * constr * constr array | Fix of constr pfixpoint | CoFix of constr pcofixpoint - | Proj of constant * constr + | Proj of projection * constr type existential = constr pexistential type rec_declaration = constr prec_declaration @@ -165,7 +165,10 @@ type action (** Engagements *) -type engagement = ImpredicativeSet +type set_predicativity = ImpredicativeSet | PredicativeSet +type type_hierarchy = TypeInType | StratifiedType + +type engagement = set_predicativity * type_hierarchy (** {6 Representation of constants (Definition/Axiom) } *) @@ -377,7 +380,7 @@ and module_body = (** algebraic type, kept if it's relevant for extraction *) mod_type_alg : module_expression option; (** set of all constraints in the module *) - mod_constraints : Univ.constraints; + mod_constraints : Univ.ContextSet.t; (** quotiented set of equivalent constants and inductive names *) mod_delta : delta_resolver; mod_retroknowledge : action list } @@ -407,7 +410,7 @@ type compiled_library = { comp_name : compilation_unit_name; comp_mod : module_body; comp_deps : library_deps; - comp_enga : engagement option; + comp_enga : engagement; comp_natsymbs : nativecode_symb_array } @@ -417,12 +420,16 @@ type compiled_library = { type library_objects -type library_disk = { +type summary_disk = { md_name : compilation_unit_name; + md_imports : compilation_unit_name array; + md_deps : library_deps; +} + +type library_disk = { md_compiled : compiled_library; md_objects : library_objects; - md_deps : library_deps; - md_imports : compilation_unit_name array } +} type opaque_table = constr Future.computation array type univ_table = diff --git a/checker/closure.ml b/checker/closure.ml index 356b683f..c6cc2185 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -276,7 +276,7 @@ and fterm = | FInd of pinductive | FConstruct of pconstructor | FApp of fconstr * fconstr array - | FProj of constant * fconstr + | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCase of case_info * fconstr * fconstr * fconstr array @@ -308,7 +308,7 @@ type stack_member = | Zapp of fconstr array | Zcase of case_info * fconstr * fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * constant + | Zproj of int * int * projection | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr @@ -678,8 +678,9 @@ let eta_expand_ind_stack env ind m s (f, s') = let (depth, args, s) = strip_update_shift_app m s in (** Try to drop the params, might fail on partially applied constructors. *) let argss = try_drop_parameters depth pars args in - let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *) - term = FProj (p, right) }) projs in + let hstack = + Array.map (fun p -> { norm = Red; (* right can't be a constructor though *) + term = FProj (Projection.make p false, right) }) projs in argss, [Zapp hstack] | _ -> raise Not_found (* disallow eta-exp for non-primitive records *) @@ -738,7 +739,7 @@ let rec knh info m stk = | FCast(t,_,_) -> knh info t stk | FProj (p,c) -> - if red_set info.i_flags (fCONST p) then + if red_set info.i_flags (fCONST (Projection.constant p)) then (let pb = lookup_projection p (info.i_env) in knh info c (Zproj (pb.proj_npars, pb.proj_arg, p) :: zupdate m stk)) diff --git a/checker/closure.mli b/checker/closure.mli index e6b39250..376e9fef 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -95,7 +95,7 @@ type fterm = | FInd of pinductive | FConstruct of pconstructor | FApp of fconstr * fconstr array - | FProj of constant * fconstr + | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCase of case_info * fconstr * fconstr * fconstr array @@ -117,7 +117,7 @@ type stack_member = | Zapp of fconstr array | Zcase of case_info * fconstr * fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * constant + | Zproj of int * int * projection | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr diff --git a/checker/declarations.ml b/checker/declarations.ml index 8d913475..32d1713a 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -206,14 +206,15 @@ let rec map_kn f f' c = let func = map_kn f f' in match c with | Const (kn, u) -> (try snd (f' kn u) with No_subst -> c) - | Proj (kn,t) -> - let kn' = - try fst (f' kn Univ.Instance.empty) - with No_subst -> kn + | Proj (p,t) -> + let p' = + Projection.map (fun kn -> + try fst (f' kn Univ.Instance.empty) + with No_subst -> kn) p in let t' = func t in - if kn' == kn && t' == t then c - else Proj (kn', t') + if p' == p && t' == t then c + else Proj (p', t') | Ind ((kn,i),u) -> let kn' = f kn in if kn'==kn then c else Ind ((kn',i),u) @@ -425,7 +426,7 @@ let subst_lazy_constr sub = function let indirect_opaque_access = ref ((fun dp i -> assert false) : DirPath.t -> int -> constr) let indirect_opaque_univ_access = - ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.constraints) + ref ((fun dp i -> assert false) : DirPath.t -> int -> Univ.ContextSet.t) let force_lazy_constr = function | Indirect (l,dp,i) -> @@ -434,7 +435,7 @@ let force_lazy_constr = function let force_lazy_constr_univs = function | OpaqueDef (Indirect (l,dp,i)) -> !indirect_opaque_univ_access dp i - | _ -> Univ.empty_constraint + | _ -> Univ.ContextSet.empty let subst_constant_def sub = function | Undef inl -> Undef inl @@ -456,6 +457,8 @@ let is_opaque cb = match cb.const_body with | OpaqueDef _ -> true | Def _ | Undef _ -> false +let opaque_univ_context cb = force_lazy_constr_univs cb.const_body + let subst_rel_declaration sub (id,copt,t as x) = let copt' = Option.smartmap (subst_mps sub) copt in let t' = subst_mps sub t in diff --git a/checker/declarations.mli b/checker/declarations.mli index 3c6db6ab..456df836 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -2,17 +2,18 @@ open Names open Cic val force_constr : constr_substituted -> constr -val force_lazy_constr_univs : Cic.constant_def -> Univ.constraints +val force_lazy_constr_univs : Cic.constant_def -> Univ.ContextSet.t val from_val : constr -> constr_substituted val indirect_opaque_access : (DirPath.t -> int -> constr) ref -val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.constraints) ref +val indirect_opaque_univ_access : (DirPath.t -> int -> Univ.ContextSet.t) ref (** Constant_body *) val body_of_constant : constant_body -> constr option val constant_has_body : constant_body -> bool val is_opaque : constant_body -> bool +val opaque_univ_context : constant_body -> Univ.ContextSet.t (* Mutual inductives *) diff --git a/checker/environ.ml b/checker/environ.ml index 710ebc71..f8f5c29b 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -14,7 +14,7 @@ type globals = { type stratification = { env_universes : Univ.universes; - env_engagement : engagement option + env_engagement : engagement } type env = { @@ -33,19 +33,28 @@ let empty_env = { env_rel_context = []; env_stratification = { env_universes = Univ.initial_universes; - env_engagement = None}; + env_engagement = (PredicativeSet,StratifiedType)}; env_imports = MPmap.empty } let engagement env = env.env_stratification.env_engagement let universes env = env.env_stratification.env_universes let rel_context env = env.env_rel_context -let set_engagement c env = - match env.env_stratification.env_engagement with - | Some c' -> if c=c' then env else error "Incompatible engagement" - | None -> - { env with env_stratification = - { env.env_stratification with env_engagement = Some c } } +let set_engagement (impr_set,type_in_type as c) env = + let expected_impr_set,expected_type_in_type = + env.env_stratification.env_engagement in + begin + match impr_set,expected_impr_set with + | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement" + | _ -> () + end; + begin + match type_in_type,expected_type_in_type with + | StratifiedType, TypeInType -> error "Incompatible engagement" + | _ -> () + end; + { env with env_stratification = + { env.env_stratification with env_engagement = c } } (* Digests *) @@ -75,13 +84,20 @@ let push_rec_types (lna,typarray,_) env = Array.fold_left (fun e assum -> push_rel assum e) env ctxt (* Universe constraints *) -let add_constraints c env = - if c == Univ.Constraint.empty then - env - else - let s = env.env_stratification in +let map_universes f env = + let s = env.env_stratification in { env with env_stratification = - { s with env_universes = Univ.merge_constraints c s.env_universes } } + { s with env_universes = f s.env_universes } } + +let add_constraints c env = + if c == Univ.Constraint.empty then env + else map_universes (Univ.merge_constraints c) env + +let push_context ?(strict=false) ctx env = + map_universes (Univ.merge_context strict ctx) env + +let push_context_set ?(strict=false) ctx env = + map_universes (Univ.merge_context_set strict ctx) env let check_constraints cst env = Univ.check_constraints cst env.env_stratification.env_universes @@ -147,8 +163,8 @@ let evaluable_constant cst env = let is_projection cst env = not (Option.is_empty (lookup_constant cst env).const_proj) -let lookup_projection cst env = - match (lookup_constant cst env).const_proj with +let lookup_projection p env = + match (lookup_constant (Projection.constant p) env).const_proj with | Some pb -> pb | None -> anomaly ("lookup_projection: constant is not a projection") diff --git a/checker/environ.mli b/checker/environ.mli index d3448b12..87f143d1 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -11,7 +11,7 @@ type globals = { env_modtypes : module_type_body MPmap.t} type stratification = { env_universes : Univ.universes; - env_engagement : engagement option; + env_engagement : engagement; } type env = { env_globals : globals; @@ -22,7 +22,7 @@ type env = { val empty_env : env (* Engagement *) -val engagement : env -> Cic.engagement option +val engagement : env -> Cic.engagement val set_engagement : Cic.engagement -> env -> env (* Digests *) @@ -39,6 +39,8 @@ val push_rec_types : name array * constr array * 'a -> env -> env (* Universes *) val universes : env -> Univ.universes val add_constraints : Univ.constraints -> env -> env +val push_context : ?strict:bool -> Univ.universe_context -> env -> env +val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env val check_constraints : Univ.constraints -> env -> bool (* Constants *) @@ -51,7 +53,7 @@ val constant_value : env -> constant puniverses -> constr val evaluable_constant : constant -> env -> bool val is_projection : constant -> env -> bool -val lookup_projection : constant -> env -> projection_body +val lookup_projection : projection -> env -> projection_body (* Inductives *) val mind_equiv : env -> inductive -> inductive -> bool diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 050c33e6..f02f03dc 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -176,7 +176,7 @@ let typecheck_arity env params inds = (* Allowed eliminations *) let check_predicativity env s small level = - match s, engagement env with + match s, fst (engagement env) with Type u, _ -> (* let u' = fresh_local_univ () in *) (* let cst = *) @@ -184,7 +184,7 @@ let check_predicativity env s small level = (* (universes env) in *) if not (Univ.check_leq (universes env) level u) then failwith "impredicative Type inductive type" - | Prop Pos, Some ImpredicativeSet -> () + | Prop Pos, ImpredicativeSet -> () | Prop Pos, _ -> if not small then failwith "impredicative Set inductive type" | Prop Null,_ -> () @@ -269,7 +269,7 @@ type ill_formed_ind = | LocalNonPos of int | LocalNotEnoughArgs of int | LocalNotConstructor - | LocalNonPar of int * int + | LocalNonPar of int * int * int exception IllFormedInd of ill_formed_ind @@ -291,9 +291,9 @@ let explain_ind_err ntyp env0 nbpar c err = | LocalNotConstructor -> raise (InductiveError (NotConstructor (env,c',Rel (ntyp+nbpar)))) - | LocalNonPar (n,l) -> + | LocalNonPar (n,i,l) -> raise (InductiveError - (NonPar (env,c',n,Rel (nbpar-n+1), Rel (l+nbpar)))) + (NonPar (env,c',n,Rel i,Rel (l+nbpar)))) let failwith_non_pos n ntypes c = for k = n to n + ntypes - 1 do @@ -323,7 +323,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = | _::hyps -> match whd_betadeltaiota env lpar.(k) with | Rel w when w = index -> check (k-1) (index+1) hyps - | _ -> raise (IllFormedInd (LocalNonPar (k+1,l))) + | _ -> raise (IllFormedInd (LocalNonPar (k+1,index,l))) in check (nparams-1) (n-nhyps) hyps; if not (Array.for_all (noccur_between n ntypes) largs') then failwith_non_pos_vect n ntypes largs' diff --git a/checker/inductive.ml b/checker/inductive.ml index 59d1a645..21b80f32 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -103,13 +103,12 @@ let instantiate_params full t u args sign = let full_inductive_instantiate mib u params sign = let dummy = Prop Null in - let t = mkArity (sign,dummy) in + let t = mkArity (subst_instance_context u sign,dummy) in fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) -let full_constructor_instantiate ((mind,_),u,(mib,_),params) = - let inst_ind = constructor_instantiate mind u mib in - (fun t -> - instantiate_params true (inst_ind t) u params mib.mind_params_ctxt) +let full_constructor_instantiate ((mind,_),u,(mib,_),params) t = + let inst_ind = constructor_instantiate mind u mib t in + instantiate_params true inst_ind u params mib.mind_params_ctxt (************************************************************************) (************************************************************************) @@ -142,53 +141,60 @@ let sort_as_univ = function | Prop Null -> Univ.type0m_univ | Prop Pos -> Univ.type0_univ +(* cons_subst add the mapping [u |-> su] in subst if [u] is not *) +(* in the domain or add [u |-> sup x su] if [u] is already mapped *) +(* to [x]. *) let cons_subst u su subst = - Univ.LMap.add u su subst - -let actualize_decl_level env lev t = - let sign,s = dest_arity env t in - mkArity (sign,lev) - -let polymorphism_on_non_applied_parameters = false + try + Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst + with Not_found -> Univ.LMap.add u su subst + +(* remember_subst updates the mapping [u |-> x] by [u |-> sup x u] *) +(* if it is presents and returns the substitution unchanged if not.*) +let remember_subst u subst = + try + let su = Universe.make u in + Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst + with Not_found -> subst (* Bind expected levels of parameters to actual levels *) (* Propagate the new levels in the signature *) -let rec make_subst env = function - | (_,Some _,_ as t)::sign, exp, args -> - let ctx,subst = make_subst env (sign, exp, args) in - t::ctx, subst - | d::sign, None::exp, args -> - let args = match args with _::args -> args | [] -> [] in - let ctx,subst = make_subst env (sign, exp, args) in - d::ctx, subst - | d::sign, Some u::exp, a::args -> - (* We recover the level of the argument, but we don't change the *) - (* level in the corresponding type in the arity; this level in the *) - (* arity is a global level which, at typing time, will be enforce *) - (* to be greater than the level of the argument; this is probably *) - (* a useless extra constraint *) - let s = sort_as_univ (snd (dest_arity env a)) in - let ctx,subst = make_subst env (sign, exp, args) in - d::ctx, cons_subst u s subst - | (na,None,t as d)::sign, Some u::exp, [] -> - (* No more argument here: we instantiate the type with a fresh level *) - (* which is first propagated to the corresponding premise in the arity *) - (* (actualize_decl_level), then to the conclusion of the arity (via *) - (* the substitution) *) - let ctx,subst = make_subst env (sign, exp, []) in - d::ctx, subst - | sign, [], _ -> - (* Uniform parameters are exhausted *) - sign,Univ.LMap.empty - | [], _, _ -> - assert false - +let rec make_subst env = + let rec make subst = function + | (_,Some _,_)::sign, exp, args -> + make subst (sign, exp, args) + | d::sign, None::exp, args -> + let args = match args with _::args -> args | [] -> [] in + make subst (sign, exp, args) + | d::sign, Some u::exp, a::args -> + (* We recover the level of the argument, but we don't change the *) + (* level in the corresponding type in the arity; this level in the *) + (* arity is a global level which, at typing time, will be enforce *) + (* to be greater than the level of the argument; this is probably *) + (* a useless extra constraint *) + let s = sort_as_univ (snd (dest_arity env a)) in + make (cons_subst u s subst) (sign, exp, args) + | (na,None,t)::sign, Some u::exp, [] -> + (* No more argument here: we add the remaining universes to the *) + (* substitution (when [u] is distinct from all other universes in the *) + (* template, it is identity substitution otherwise (ie. when u is *) + (* already in the domain of the substitution) [remember_subst] will *) + (* update its image [x] by [sup x u] in order not to forget the *) + (* dependency in [u] that remains to be fullfilled. *) + make (remember_subst u subst) (sign, exp, []) + | sign, [], _ -> + (* Uniform parameters are exhausted *) + subst + | [], _, _ -> + assert false + in + make Univ.LMap.empty exception SingletonInductiveBecomesProp of Id.t let instantiate_universes env ctx ar argsorts = let args = Array.to_list argsorts in - let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in + let subst = make_subst env (ctx,ar.template_param_levels,args) in let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 998e23c6..3ea5ed0d 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -18,19 +18,27 @@ let refresh_arity ar = let ctxt, hd = decompose_prod_assum ar in match hd with Sort (Type u) when not (Univ.is_univ_variable u) -> - let u' = Univ.Universe.make (Univ.Level.make empty_dirpath 1) in - mkArity (ctxt,Prop Null), - Univ.enforce_leq u u' Univ.empty_constraint - | _ -> ar, Univ.empty_constraint + let ul = Univ.Level.make empty_dirpath 1 in + let u' = Univ.Universe.make ul in + let cst = Univ.enforce_leq u u' Univ.empty_constraint in + let ctx = Univ.ContextSet.make (Univ.LSet.singleton ul) cst in + mkArity (ctxt,Prop Null), ctx + | _ -> ar, Univ.ContextSet.empty let check_constant_declaration env kn cb = Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn); pp_flush (); - let env' = add_constraints (Univ.UContext.constraints cb.const_universes) env in + let env' = + if cb.const_polymorphic then + let inst = Univ.make_abstract_instance cb.const_universes in + let ctx = Univ.UContext.make (inst, Univ.UContext.constraints cb.const_universes) in + push_context ~strict:false ctx env + else push_context ~strict:true cb.const_universes env + in let envty, ty = match cb.const_type with RegularArity ty -> let ty', cu = refresh_arity ty in - let envty = add_constraints cu env' 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 @@ -69,7 +77,7 @@ let mk_mtb mp sign delta = mod_expr = Abstract; mod_type = sign; mod_type_alg = None; - mod_constraints = Univ.Constraint.empty; + mod_constraints = Univ.ContextSet.empty; mod_delta = delta; mod_retroknowledge = []; } diff --git a/checker/modops.ml b/checker/modops.ml index 8ccf118d..7f07f8bf 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -83,12 +83,13 @@ let strengthen_const mp_from l cb resolver = | Def _ -> cb | _ -> let con = Constant.make2 mp_from l in - (* let con = constant_of_delta resolver con in*) let u = - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + if cb.const_polymorphic then + Univ.make_abstract_instance cb.const_universes else Univ.Instance.empty in - { cb with const_body = Def (Declarations.from_val (Const (con,u))) } + { cb with + const_body = Def (Declarations.from_val (Const (con,u))) } let rec strengthen_mod mp_from mp_to mb = if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb diff --git a/checker/print.ml b/checker/print.ml index 1cc48ff7..7624fd32 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -100,7 +100,7 @@ let print_pure_constr csr = done in print_string"{"; print_fix (); print_string"}" | Proj (p, c) -> - print_string "Proj("; sp_con_display p; print_string ","; + print_string "Proj("; sp_con_display (Projection.constant p); print_string ","; box_display c; print_string ")" and box_display c = open_hovbox 1; term_display c; close_box() diff --git a/checker/reduction.ml b/checker/reduction.ml index 28fdb130..384d883e 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -52,7 +52,7 @@ let compare_stack_shape stk1 stk2 = type lft_constr_stack_elt = Zlapp of (lift * fconstr) array - | Zlproj of Names.constant * lift + | Zlproj of Names.projection * lift | Zlfix of (lift * fconstr) * lft_constr_stack | Zlcase of case_info * lift * fconstr * fconstr array and lft_constr_stack = lft_constr_stack_elt list @@ -137,7 +137,9 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 = | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> f fx1 fx2; cmp_rec a1 a2 | (Zlproj (c1,l1),Zlproj (c2,l2)) -> - if not (Names.eq_con_chk c1 c2) then + if not (Names.eq_con_chk + (Names.Projection.constant c1) + (Names.Projection.constant c2)) then raise NotConvertible | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) -> if not (fmind ci1.ci_ind ci2.ci_ind) then @@ -156,7 +158,7 @@ type conv_pb = | CONV | CUMUL -let sort_cmp univ pb s0 s1 = +let sort_cmp env univ pb s0 s1 = match (s0,s1) with | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible @@ -165,14 +167,15 @@ let sort_cmp univ pb s0 s1 = CUMUL -> () | _ -> raise NotConvertible) | (Type u1, Type u2) -> - if not + if snd (engagement env) == StratifiedType + && not (match pb with | CONV -> Univ.check_eq univ u1 u2 | CUMUL -> Univ.check_leq univ u1 u2) then begin if !Flags.debug then begin let op = match pb with CONV -> "=" | CUMUL -> "<=" in - Printf.eprintf "cort_cmp: %s\n%!" Pp.(string_of_ppcmds + Printf.eprintf "sort_cmp: %s\n%!" Pp.(string_of_ppcmds (str"Error: " ++ Univ.pr_uni u1 ++ str op ++ Univ.pr_uni u2 ++ str ":" ++ cut() ++ Univ.pr_universes univ)) end; @@ -259,7 +262,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (match a1, a2 with | (Sort s1, Sort s2) -> assert (is_empty_stack v1 && is_empty_stack v2); - sort_cmp univ cv_pb s1 s2 + sort_cmp (infos_env infos) univ cv_pb s1 s2 | (Meta n, Meta m) -> if n=m then convert_stacks univ infos lft1 lft2 v1 v2 diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 810d6e0b..81a3cc03 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -27,18 +27,26 @@ let set_engagement c = (* full_add_module adds module with universes and constraints *) let full_add_module dp mb univs digest = let env = !genv in - let env = add_constraints mb.mod_constraints env in - let env = add_constraints univs env in + let env = push_context_set ~strict:true mb.mod_constraints env in + let env = push_context_set ~strict:true univs env in let env = Modops.add_module mb env in genv := add_digest env dp digest -(* Check that the engagement expected by a library matches the initial one *) -let check_engagement env c = - match engagement env, c with - | Some ImpredicativeSet, Some ImpredicativeSet -> () - | _, None -> () - | _, Some ImpredicativeSet -> - error "Needs option -impredicative-set" +(* Check that the engagement expected by a library extends the initial one *) +let check_engagement env (expected_impredicative_set,expected_type_in_type) = + let impredicative_set,type_in_type = Environ.engagement env in + begin + match impredicative_set, expected_impredicative_set with + | PredicativeSet, ImpredicativeSet -> + Errors.error "Needs option -impredicative-set." + | _ -> () + end; + begin + match type_in_type, expected_type_in_type with + | StratifiedType, TypeInType -> + Errors.error "Needs option -type-in-type." + | _ -> () + end (* Libraries = Compiled modules *) @@ -75,8 +83,8 @@ let import file clib univs digest = check_engagement env clib.comp_enga; let mb = clib.comp_mod in Mod_checking.check_module - (add_constraints univs - (add_constraints mb.mod_constraints env)) mb.mod_mp mb; + (push_context_set ~strict:true univs + (push_context_set ~strict:true mb.mod_constraints env)) mb.mod_mp mb; stamp_library file digest; full_add_module clib.comp_name mb univs digest diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli index e16e64e6..892a8d2c 100644 --- a/checker/safe_typing.mli +++ b/checker/safe_typing.mli @@ -15,6 +15,6 @@ val get_env : unit -> env val set_engagement : engagement -> unit val import : - CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit + CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit val unsafe_import : - CUnix.physical_path -> compiled_library -> Univ.constraints -> Cic.vodigest -> unit + CUnix.physical_path -> compiled_library -> Univ.ContextSet.t -> Cic.vodigest -> unit diff --git a/checker/term.ml b/checker/term.ml index 93540276..430be495 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -392,7 +392,7 @@ let compare_constr f t1 t2 = Array.equal f tl1 tl2 && Array.equal f bl1 bl2 | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2 - | Proj (p1,c1), Proj(p2,c2) -> eq_con_chk p1 p2 && f c1 c2 + | Proj (p1,c1), Proj(p2,c2) -> Projection.equal p1 p2 && f c1 c2 | _ -> false let rec eq_constr m n = diff --git a/checker/typeops.ml b/checker/typeops.ml index 9bc4b269..21819992 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -128,7 +128,7 @@ let sort_of_product env domsort rangsort = | (Prop _, Prop Pos) -> rangsort (* Product rule (Type,Set,?) *) | (Type u1, Prop Pos) -> - if engagement env = Some ImpredicativeSet then + if fst (engagement env) = ImpredicativeSet then (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) rangsort else diff --git a/checker/univ.ml b/checker/univ.ml index 3bcb3bc9..648e4781 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -244,7 +244,8 @@ module Level = struct let set = make Set let prop = make Prop - + let var i = make (Var i) + let is_small x = match data x with | Level _ -> false @@ -281,8 +282,8 @@ module Level = struct end (** Level sets and maps *) -module LSet = Set.Make (Level) -module LMap = Map.Make (Level) +module LMap = HMap.Make (Level) +module LSet = LMap.Set type 'a universe_map = 'a LMap.t @@ -559,20 +560,26 @@ let repr g u = in repr_rec u -(* [safe_repr] also search for the canonical representative, but - if the graph doesn't contain the searched universe, we add it. *) - -let safe_repr g u = - let rec safe_repr_rec u = - match UMap.find u g with - | Equiv v -> safe_repr_rec v - | Canonical arc -> arc - in - try g, safe_repr_rec u - with Not_found -> - let can = terminal u in - enter_arc can g, can +let get_set_arc g = repr g Level.set +exception AlreadyDeclared + +let add_universe vlev strict g = + try + let _arcv = UMap.find vlev g in + raise AlreadyDeclared + with Not_found -> + let v = terminal vlev in + let arc = + let arc = get_set_arc g in + if strict then + { arc with lt=vlev::arc.lt} + else + { arc with le=vlev::arc.le} + in + let g = enter_arc arc g in + enter_arc v g + (* reprleq : canonical_arc -> canonical_arc list *) (* All canonical arcv such that arcu<=arcv with arcv#arcu *) let reprleq g arcu = @@ -739,8 +746,8 @@ let is_lt g arcu arcv = (** First, checks on universe levels *) let check_equal g u v = - let g, arcu = safe_repr g u in - let _, arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in arcu == arcv let check_eq_level g u v = u == v || check_equal g u v @@ -749,8 +756,8 @@ let is_set_arc u = Level.is_set u.univ let is_prop_arc u = Level.is_prop u.univ let check_smaller g strict u v = - let g, arcu = safe_repr g u in - let g, arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in if strict then is_lt g arcu arcv else @@ -900,8 +907,8 @@ let error_inconsistency o u v = (* enforc_univ_eq u v will force u=v if possible, will fail otherwise *) let enforce_univ_eq u v g = - let g,arcu = safe_repr g u in - let g,arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in match fast_compare g arcu arcv with | FastEQ -> g | FastLT -> error_inconsistency Eq v u @@ -916,8 +923,8 @@ let enforce_univ_eq u v g = (* enforce_univ_leq : Level.t -> Level.t -> unit *) (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *) let enforce_univ_leq u v g = - let g,arcu = safe_repr g u in - let g,arcv = safe_repr g v in + let arcu = repr g u in + let arcv = repr g v in if is_leq g arcu arcv then g else match fast_compare g arcv arcu with @@ -928,8 +935,8 @@ let enforce_univ_leq u v g = (* enforce_univ_lt u v will force u g | FastLE -> fst (setlt g arcu arcv) @@ -941,7 +948,10 @@ let enforce_univ_lt u v g = | FastLE | FastLT -> error_inconsistency Lt u v (* Prop = Set is forbidden here. *) -let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty +let initial_universes = + let g = enter_arc (terminal Level.set) UMap.empty in + let g = enter_arc (terminal Level.prop) g in + enforce_univ_lt Level.prop Level.set g (* Constraints and sets of constraints. *) @@ -970,7 +980,7 @@ module Constraint = Set.Make(UConstraintOrd) let empty_constraint = Constraint.empty let merge_constraints c g = Constraint.fold enforce_constraint c g - + type constraints = Constraint.t (** A value with universe constraints. *) @@ -1146,7 +1156,7 @@ struct (** Universe contexts (variables as a list) *) let empty = (Instance.empty, Constraint.empty) - + let make x = x let instance (univs, cst) = univs let constraints (univs, cst) = cst end @@ -1158,6 +1168,8 @@ struct type t = LSet.t constrained let empty = LSet.empty, Constraint.empty let constraints (_, cst) = cst + let levels (ctx, _) = ctx + let make ctx cst = (ctx, cst) end type universe_context_set = ContextSet.t @@ -1207,6 +1219,9 @@ let subst_instance_constraints s csts = (fun c csts -> Constraint.add (subst_instance_constraint s c) csts) csts Constraint.empty +let make_abstract_instance (ctx, _) = + Array.mapi (fun i l -> Level.var i) ctx + (** Substitute instance inst for ctx in csts *) let instantiate_univ_context (ctx, csts) = (ctx, subst_instance_constraints ctx csts) @@ -1238,6 +1253,20 @@ let subst_univs_universe fn ul = List.fold_left (fun acc u -> Universe.merge_univs acc (Universe.Huniv.tip u)) substs nosubst +let merge_context strict ctx g = + let g = Array.fold_left + (* Be lenient, module typing reintroduces universes and + constraints due to includes *) + (fun g v -> try add_universe v strict g with AlreadyDeclared -> g) + g (UContext.instance ctx) + in merge_constraints (UContext.constraints ctx) g + +let merge_context_set strict ctx g = + let g = LSet.fold + (fun v g -> try add_universe v strict g with AlreadyDeclared -> g) + (ContextSet.levels ctx) g + in merge_constraints (ContextSet.constraints ctx) g + (** Pretty-printing *) let pr_arc = function diff --git a/checker/univ.mli b/checker/univ.mli index 742ef91a..02c1bbdb 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -74,6 +74,13 @@ val check_eq : universe check_function (** The initial graph of universes: Prop < Set *) val initial_universes : universes +(** Adds a universe to the graph, ensuring it is >= or > Set. + @raises AlreadyDeclared if the level is already declared in the graph. *) + +exception AlreadyDeclared + +val add_universe : universe_level -> bool -> universes -> universes + (** {6 Constraints. } *) type constraint_type = Lt | Le | Eq @@ -117,14 +124,14 @@ type univ_inconsistency = constraint_type * universe * universe exception UniverseInconsistency of univ_inconsistency val merge_constraints : constraints -> universes -> universes - + val check_constraints : constraints -> universes -> bool (** {6 Support for universe polymorphism } *) (** Polymorphic maps from universe levels to 'a *) module LMap : Map.S with type key = universe_level - +module LSet : CSig.SetS with type elt = universe_level type 'a universe_map = 'a LMap.t (** {6 Substitution} *) @@ -177,7 +184,7 @@ sig type t val empty : t - + val make : universe_instance constrained -> t val instance : t -> Instance.t val constraints : t -> constraints @@ -186,6 +193,7 @@ end module ContextSet : sig type t + val make : LSet.t -> constraints -> t val empty : t val constraints : t -> constraints end @@ -193,6 +201,9 @@ module ContextSet : type universe_context = UContext.t type universe_context_set = ContextSet.t +val merge_context : bool -> universe_context -> universes -> universes +val merge_context_set : bool -> universe_context_set -> universes -> universes + val empty_level_subst : universe_level_subst val is_empty_level_subst : universe_level_subst -> bool @@ -219,6 +230,9 @@ val subst_instance_constraints : universe_instance -> constraints -> constraints val instantiate_univ_context : universe_context -> universe_context val instantiate_univ_constraints : universe_instance -> universe_context -> constraints +(** Build the relative instance corresponding to the context *) +val make_abstract_instance : universe_context -> universe_instance + (** {6 Pretty-printing of universes. } *) val pr_universes : universes -> Pp.std_ppcmds diff --git a/checker/values.ml b/checker/values.ml index cf93466b..34de511c 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 0a174243f8b06535c9eecbbe8d339fe1 checker/cic.mli +MD5 76312d06933f47498a1981a6261c9f75 checker/cic.mli *) @@ -126,6 +126,7 @@ let v_caseinfo = v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|] let v_cast = v_enum "cast_kind" 4 +let v_proj = v_tuple "projection" [|v_cst; v_bool|] let rec v_constr = Sum ("constr",0,[| @@ -145,7 +146,7 @@ let rec v_constr = [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *) [|v_fix|]; (* Fix *) [|v_cofix|]; (* CoFix *) - [|v_cst;v_constr|] (* Proj *) + [|v_proj;v_constr|] (* Proj *) |]) and v_prec = Tuple ("prec_declaration", @@ -192,7 +193,9 @@ let v_lazy_constr = (** kernel/declarations *) -let v_engagement = v_enum "eng" 1 +let v_impredicative_set = v_enum "impr-set" 2 +let v_type_in_type = v_enum "type-in-type" 2 +let v_engagement = v_tuple "eng" [|v_impredicative_set; v_type_in_type|] let v_pol_arity = v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|] @@ -205,8 +208,10 @@ let v_cst_def = [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|] let v_projbody = - v_tuple "projection_body" [|v_cst;Int;Int;v_constr;v_tuple "proj_eta" [|v_constr;v_constr|]; - v_constr|] + v_tuple "projection_body" + [|v_cst;Int;Int;v_constr; + v_tuple "proj_eta" [|v_constr;v_constr|]; + v_constr|] let v_cb = v_tuple "constant_body" [|v_section_ctxt; @@ -302,17 +307,17 @@ and v_impl = and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *) and v_module = Tuple ("module_body", - [|v_mp;v_impl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|]) + [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) and v_modtype = Tuple ("module_type_body", - [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|]) + [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|]) (** kernel/safe_typing *) let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |]) let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|]) let v_compiled_lib = - v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|] + v_tuple "compiled" [|v_dp;v_module;v_deps;v_engagement;Any|] (** Library objects *) @@ -350,8 +355,11 @@ let v_stm_seg = v_pair v_tasks v_counters (** Toplevel structures in a vo (see Cic.mli) *) +let v_libsum = + Tuple ("summary", [|v_dp;Array v_dp;v_deps|]) + let v_lib = - Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|]) + Tuple ("library",[|v_compiled_lib;v_libraryobjs|]) let v_opaques = Array (v_computation v_constr) let v_univopaques = diff --git a/checker/votour.ml b/checker/votour.ml index 7c954d6f..4aecb28f 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -21,32 +21,91 @@ sig type obj val input : in_channel -> obj val repr : obj -> obj repr - val size : int list -> int + val size : obj -> int end -module Repr : S = +module ReprObj : S = struct - type obj = Obj.t + type obj = Obj.t * int list let input chan = let obj = input_value chan in let () = CObj.register_shared_size obj in - obj + (obj, []) - let repr obj = + let repr (obj, pos) = if Obj.is_block obj then let tag = Obj.tag obj in if tag = Obj.string_tag then STRING (Obj.magic obj) else if tag < Obj.no_scan_tag then - let data = Obj.dup obj in - let () = Obj.set_tag data 0 in + let init i = (Obj.field obj i, i :: pos) in + let data = Array.init (Obj.size obj) init in BLOCK (tag, Obj.magic data) else OTHER else INT (Obj.magic obj) - let size p = CObj.shared_size_of_pos p + let size (_, p) = CObj.shared_size_of_pos p +end + +module ReprMem : S = +struct + open Analyze + + type obj = data + + let memory = ref [||] + let sizes = ref [||] + (** size, in words *) + + let ws = Sys.word_size / 8 + + let rec init_size seen = function + | Int _ | Atm _ | Fun _ -> 0 + | Ptr p -> + if seen.(p) then 0 + else + let () = seen.(p) <- true in + match (!memory).(p) with + | Struct (tag, os) -> + let fold accu o = accu + 1 + init_size seen o in + let size = Array.fold_left fold 1 os in + let () = (!sizes).(p) <- size in + size + | String s -> + let size = 2 + (String.length s / ws) in + let () = (!sizes).(p) <- size in + size + + let size = function + | Int _ | Atm _ | Fun _ -> 0 + | Ptr p -> (!sizes).(p) + + let repr = function + | Int i -> INT i + | Atm t -> BLOCK (t, [||]) + | Fun _ -> OTHER + | Ptr p -> + match (!memory).(p) with + | Struct (tag, os) -> BLOCK (tag, os) + | String s -> STRING s + + let input ch = + let obj, mem = parse_channel ch in + let () = memory := mem in + let () = sizes := Array.make (Array.length mem) (-1) in + let seen = Array.make (Array.length mem) false in + let _ = init_size seen obj in + obj + end +module Visit (Repr : S) : +sig + val init : unit -> unit + val visit : Values.value -> Repr.obj -> int list -> unit +end = +struct + (** Name of a value *) let rec get_name ?(extra=false) = function @@ -92,7 +151,7 @@ let rec get_details v o = match v, Repr.repr o with let node_info (v,o,p) = get_name ~extra:true v ^ get_details v o ^ - " (size "^ string_of_int (Repr.size p)^"w)" + " (size "^ string_of_int (Repr.size o)^"w)" (** Children of a block : type, object, position. For lists, we collect all elements of the list at once *) @@ -201,14 +260,49 @@ let rec visit v o pos = | Failure "forbidden" -> let info = pop () in visit info.typ info.obj info.pos | Failure _ | Invalid_argument _ -> visit v o pos +end + (** Loading the vo *) +type header = { + magic : string; + (** Magic number of the marshaller *) + length : int; + (** Size on disk in bytes *) + size32 : int; + (** Size in words when loaded on 32-bit systems *) + size64 : int; + (** Size in words when loaded on 64-bit systems *) + objects : int; + (** Number of blocks defined in the marshalled structure *) +} + +let dummy_header = { + magic = "\000\000\000\000"; + length = 0; + size32 = 0; + size64 = 0; + objects = 0; +} + +let parse_header chan = + let magic = String.create 4 in + let () = for i = 0 to 3 do magic.[i] <- input_char chan done in + let length = input_binary_int chan in + let objects = input_binary_int chan in + let size32 = input_binary_int chan in + let size64 = input_binary_int chan in + { magic; length; size32; size64; objects } + type segment = { name : string; mutable pos : int; typ : Values.value; + mutable header : header; } +let make_seg name typ = { name; typ; pos = 0; header = dummy_header } + let visit_vo f = Printf.printf "\nWelcome to votour !\n"; Printf.printf "Enjoy your guided tour of a Coq .vo or .vi file\n"; @@ -216,12 +310,19 @@ let visit_vo f = Printf.printf "At prompt, enters the -th child, u goes up 1 level, x exits\n\n%!"; let segments = [| - {name="library"; pos=0; typ=Values.v_lib}; - {name="univ constraints of opaque proofs"; pos=0;typ=Values.v_univopaques}; - {name="discharging info"; pos=0; typ=Opt Any}; - {name="STM tasks"; pos=0; typ=Opt Values.v_stm_seg}; - {name="opaque proofs"; pos=0; typ=Values.v_opaques}; + make_seg "summary" Values.v_libsum; + make_seg "library" Values.v_lib; + make_seg "univ constraints of opaque proofs" Values.v_univopaques; + make_seg "discharging info" (Opt Any); + make_seg "STM tasks" (Opt Values.v_stm_seg); + make_seg "opaque proofs" Values.v_opaques; |] in + let repr = + if Sys.word_size = 64 then (module ReprMem : S) else (module ReprObj : S) + (** On 32-bit machines, representation may exceed the max size of arrays *) + in + let module Repr = (val repr : S) in + let module Visit = Visit(Repr) in while true do let ch = open_in_bin f in let magic = input_binary_int ch in @@ -229,21 +330,24 @@ let visit_vo f = for i=0 to Array.length segments - 1 do let pos = input_binary_int ch in segments.(i).pos <- pos_in ch; + let header = parse_header ch in + segments.(i).header <- header; seek_in ch pos; ignore(Digest.input ch); done; Printf.printf "The file has %d segments, choose the one to visit:\n" (Array.length segments); - Array.iteri (fun i { name; pos } -> - Printf.printf " %d: %s, starting at byte %d\n" i name pos) + Array.iteri (fun i { name; pos; header } -> + let size = if Sys.word_size = 64 then header.size64 else header.size32 in + Printf.printf " %d: %s, starting at byte %d (size %iw)\n" i name pos size) segments; Printf.printf "# %!"; let l = read_line () in let seg = int_of_string l in seek_in ch segments.(seg).pos; let o = Repr.input ch in - let () = init () in - visit segments.(seg).typ o [] + let () = Visit.init () in + Visit.visit segments.(seg).typ o [] done let main = diff --git a/configure.ml b/configure.ml index bbe43520..51033c3d 100644 --- a/configure.ml +++ b/configure.ml @@ -11,11 +11,11 @@ #load "str.cma" open Printf -let coq_version = "8.5beta2" -let coq_macos_version = "8.4.92" (** "[...] should be a string comprised of +let coq_version = "8.5beta3" +let coq_macos_version = "8.4.93" (** "[...] should be a string comprised of three non-negative, period-separed integers [...]" *) -let vo_magic = 8591 -let state_magic = 58501 +let vo_magic = 8493 +let state_magic = 58503 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr"; "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"] @@ -252,7 +252,7 @@ module Prefs = struct let profile = ref false let annotate = ref false let makecmd = ref "make" - let nativecompiler = ref true + let nativecompiler = ref (not (os_type_win32 || os_type_cygwin)) let coqwebsite = ref "http://coq.inria.fr/" let force_caml_version = ref false end @@ -331,12 +331,12 @@ let args_options = Arg.align [ " Dumps ml annotation files while compiling Coq"; "-makecmd", Arg.Set_string Prefs.makecmd, " Name of GNU Make command"; - "-no-native-compiler", Arg.Clear Prefs.nativecompiler, - " No compilation to native code for conversion and normalization"; + "-native-compiler", arg_bool Prefs.nativecompiler, + "(yes|no) Compilation to native code for conversion and normalization"; "-coqwebsite", Arg.Set_string Prefs.coqwebsite, " URL of the coq website"; - "-force-caml-version", arg_bool Prefs.force_caml_version, - " Force OCaml version"; + "-force-caml-version", Arg.Set Prefs.force_caml_version, + "Force OCaml version"; ] let parse_args () = @@ -396,8 +396,7 @@ let coq_annotate_flag = then if program_in_path "ocamlmerlin" then "-bin-annot" else "-dtypes" else "" -let cflags = "-Wall -Wno-unused" - +let cflags = "-Wall -Wno-unused -g -O2" (** * Architecture *) @@ -477,7 +476,10 @@ let camlbin, caml_version, camllib = rebase_camlexec dir camlexec; Filename.dirname camlexec.byte, camlexec.byte | None -> - try let camlc = which camlexec.byte in Filename.dirname camlc, camlc + try let camlc = which camlexec.byte in + let dir = Filename.dirname camlc in + if not arch_win32 then rebase_camlexec dir camlexec; (* win32: TOCHECK *) + dir, camlc with Not_found -> die (sprintf "Error: cannot find '%s' in your path!\n" camlexec.byte ^ "Please adjust your path or use the -camldir option of ./configure") @@ -514,7 +516,12 @@ let caml_version_nums = let check_caml_version () = if caml_version_nums >= [3;12;1] then - printf "You have OCaml %s. Good!\n" caml_version + if caml_version_nums = [4;2;0] && not !Prefs.force_caml_version then + die ("Your version of OCaml is 4.02.0 which suffers from a bug inducing\n" ^ + "very slow compilation times. If you still want to use it, use \n" ^ + "option -force-caml-version.\n") + else + printf "You have OCaml %s. Good!\n" caml_version else let () = printf "Your version of OCaml is %s.\n" caml_version in if !Prefs.force_caml_version then @@ -839,12 +846,6 @@ let md5sum = if arch = "Darwin" then "md5 -q" else "md5sum" -(** * md5sum command *) - -let md5sum = - if arch = "Darwin" then "md5 -q" else "md5sum" - - (** * Documentation : do we have latex, hevea, ... *) let check_doc () = @@ -856,6 +857,9 @@ let check_doc () = if not !Prefs.withdoc then raise Not_found; if not (program_in_path "latex") then err "latex"; if not (program_in_path "hevea") then err "hevea"; + if not (program_in_path "hacha") then err "hacha"; + if not (program_in_path "fig2dev") then err "fig2dev"; + if not (program_in_path "convert") then err "convert"; true with Not_found -> false @@ -1200,7 +1204,9 @@ let write_makefile f = pr "# Defining REVISION\n"; pr "CHECKEDOUT=%s\n\n" vcs; pr "# Option to control compilation and installation of the documentation\n"; - pr "WITHDOC=%s\n" (if withdoc then "all" else "no"); + pr "WITHDOC=%s\n\n" (if withdoc then "all" else "no"); + pr "# Option to produce precompiled files for native_compute\n"; + pr "NATIVECOMPUTE=%s\n" (if !Prefs.nativecompiler then "-native-compiler" else ""); close_out o; Unix.chmod f 0o444 diff --git a/dev/TODO b/dev/TODO new file mode 100644 index 00000000..e62ee6e5 --- /dev/null +++ b/dev/TODO @@ -0,0 +1,22 @@ + + o options de la ligne de commande + - reporter les options de l'ancien script coqtop sur le nouveau coqtop.ml + + o arguments implicites + - les calculer une fois pour toutes à la déclaration (dans Declare) + et stocker cette information dans le in_variable, in_constant, etc. + + o Environnements compilés (type Environ.compiled_env) + - pas de timestamp mais plutôt un checksum avec Digest (mais comment ?) + + o Efficacité + - utiliser DOPL plutôt que DOPN (sauf pour Case) + - batch mode => pas de undo, ni de reset + - conversion : déplier la constante la plus récente + - un cache pour type_of_const, type_of_inductive, type_of_constructor, + lookup_mind_specif + + o Toplevel + - parsing de la ligne de commande : utiliser Arg ??? + + diff --git a/dev/base_include b/dev/base_include index de63c557..dac1f609 100644 --- a/dev/base_include +++ b/dev/base_include @@ -86,6 +86,7 @@ open Cbv open Classops open Clenv open Clenvtac +open Constr_matching open Glob_term open Glob_ops open Coercion @@ -147,6 +148,7 @@ open Tactic_debug open Decl_proof_instr open Decl_mode +open Hints open Auto open Autorewrite open Contradiction diff --git a/dev/doc/README-V1-V5 b/dev/doc/README-V1-V5 new file mode 100644 index 00000000..2ca62e3d --- /dev/null +++ b/dev/doc/README-V1-V5 @@ -0,0 +1,293 @@ + + Notes on the prehistory of Coq + +This archive contains the sources of the CONSTR ancestor of the Coq proof +assistant. CONSTR, then Coq, was designed and implemented in the Formel team, +joint between the INRIA Rocquencourt laboratory and the Ecole Normale Supérieure +of Paris, from 1984 onwards. + +Version 1 + +This software is a prototype type-checker for a higher-order logical formalism +known as the Theory of Constructions, presented in his PhD thesis by +Thierry Coquand, with influences from Girard's system F and de Bruijn's Automath. +The metamathematical analysis of the system is the +PhD work of Thierry Coquand. The software is mostly the work of Gérard Huet. +Most of the mathematical examples verified with the software are due +to Thierry Coquand. + +The programming language of the CONSTR software (as it was called at the time) +is a version of ML issued from the Edinburgh LCF system and running on +a LISP backend. The main improvements from the original LCF ML are that ML +is compiled rather than interpreted (Gérard Huet building on the original +translator by Lockwood Morris), and that it is enriched by recursively +defined types (work of Guy Cousineau). This ancestor of CAML was used +and improved by Larry Paulson for his implementation of Cambridge LCF. + +Software developments of this prototype occurred from late 1983 to early 1985. + +Version 1.10 was frozen on December 22nd 1984. It is the version used for the +examples in Thierry Coquand's thesis, defended on January 31st 1985. +There was a unique binding operator, used both for universal quantification +(dependent product) at the level of types and functional abstraction (lambda) +at the level of terms/proofs, in the manner of Automath. Substitution +(lambda reduction) was implemented using de Bruijn's indexes. + +Version 1.11 was frozen on February 19th, 1985. It is the version used for the +examples in the paper: +Th. Coquand, G. Huet. Constructions: A Higher Order Proof System for Mechanizing +Mathematics. Invited paper, EUROCAL85, April 1985, Linz, Austria. Springer Verlag +LNCS 203, pp. 151-184. + +Christine Paulin joined the team at this point, for her DEA research internship. +In her DEA memoir (August 1985) she presents developments for the lambo function +computing the minimal m such that f(m) is greater than n, for f an increasing +integer function, a challenge for constructive mathematics. She also encoded +the majority voting algorithm of Boyer and Moore. + +Version 2 + +The formal system, now renamed as the "Calculus of Constructions", was presented +with a proof of consistency and comparisons with proof systems of Per +Martin Löf, Girard, and the Automath family of N. de Bruijn, in the paper: +T. Coquand and G. Huet. The Calculus of Constructions. +Submitted on June 30th 1985, accepted on December 5th, 1985, +Information and Computation. Preprint as Rapport de Recherche Inria n°530, +Mai 1986. Final version in Information and Computation 76,2/3, Feb. 88. + +An abstraction of the software design, in the form of an abstract machine +for proof checking, and a fuller sequence of mathematical developments was +presented in: +Th. Coquand, G. Huet. Concepts Mathématiques et Informatiques Formalisés dans le Calcul des Constructions. Invited paper, European Logic Colloquium, Orsay, +July 1985. Preprint as Rapport de recherche INRIA n°463, Dec. 85. +Published in Logic Colloquium 1985, North-Holland, 1987. + +Version 2.8 was frozen on December 16th, 1985, and served for developing +the exemples in the above papers. + +This calculus was then enriched in version 2.9 with a cumulative hierarchy of +universes. Universe levels were initially explicit natural numbers. +Another improvement was the possibility of automatic synthesis of implicit +type arguments, relieving the user of tedious redundant declarations. + +Christine Paulin wrote an article "Algorithm development in the Calculus of +Constructions", preprint as Rapport de recherche INRIA n°497, March 86. +Final version in Proceedings Symposium on Logic in Computer Science, Cambridge, +MA, 1986 (IEEE Computer Society Press). Besides lambo and majority, +she presents quicksort and a text formatting algorithm. + +Version 2.13 of the calculus of constructions with universes was frozen +on June 25th, 1986. + +A synthetic presentation of type theory along constructive lines with ML +algorithms was given by Gérard Huet in his May 1986 CMU course notes +"Formal Structures for Computation and Deduction". Its chapter +"Induction and Recursion in the Theory of Constructions" was presented +as an invited paper at the Joint Conference on Theory and Practice of Software +Development TAPSOFT’87 at Pise in March 1987, and published as +"Induction Principles Formalized in the Calculus of Constructions" in +Programming of Future Generation Computers, Ed. K. Fuchi and M. Nivat, +North-Holland, 1988. + +Version 3 + +This version saw the beginning of proof automation, with a search algorithm +inspired from PROLOG and the applicative logic programming programs +of the course notes "Formal structures for computation and deduction". +The search algorithm was implemented in ML by Thierry Coquand. +The proof system could thus be used in two modes: proof verification and +proof synthesis, with tactics such as "AUTO". + +The implementation language was now called CAML, for "categorical abstract +machine language". It used as backend the LLM3 virtual machine of Le Lisp +by Jérôme Chailloux. The main developers of CAML were Michel Mauny, +Ascander Suarez and Pierre Weis. + +V3.1 was started in the summer of 1986, V3.2 was frozen at the end of November +1986. V3.4 was developed in the first half of 1987. + +Thierry Coquand held a post-doctoral position in Cambrige University in 1986-87, +where he developed a variant implementation in SML, with which he wrote +some developments on fixpoints in Scott's domains. + +Version 4 + +This version saw the beginning of program extraction from proofs, with +two varieties of the type Prop of propositions, indicating constructive intent. +The proof extraction algorithms were implemented by Christine Paulin-Mohring. + +V4.1 was frozen on July 24th, 1987. It had a first identified library of +mathematical developments (directory exemples), with libraries Logic +(containing impredicative encodings of intuitionistic logic and algebraic +primitives for booleans, natural numbers and list), Peano developing second-order +Peano arithmetic, Arith defining addition, multiplication, euclidean division +and factorial. Typical developments were the Knaster-Tarski theorem +and Newman's lemma from rewriting theory. + +V4.2 was a joint development of a team consisting of Thierry Coquand, Gérard +Huet and Christine Paulin-Mohring. A file V4.2.log records the log of changes. +It was frozen on September 1987 as the last version implemented in CAML 2.3, +and V4.3 followed on CAML 2.5, a more stable development system. + +V4.3 saw the first top-level of the system. Instead of evaluating explicit +quotations, the user could develop his mathematics in a high-level language +called the mathematical vernacular (following Automath terminology). +The user could develop files in the vernacular notation (with .v extension) +which were now separate from the ml sources of the implementation. +Gilles Dowek joined the team to develop the vernacular language as his +DEA internship research. + +A notion of sticky constant was introduced, in order to keep names of lemmas +when local hypotheses of proofs were discharged. This gave a notion +of global mathematical environment with local sections. + +Another significant practical change was that the system, originally developped +on the VAX central computer of our lab, was transferred on SUN personal +workstations, allowing a level of distributed development. +The extraction algorithm was modified, with three annotations Pos, Null and +Typ decorating the sorts Prop and Type. + +Version 4.3 was frozen at the end of November 1987, and was distributed to an +early community of users (among those were Hugo Herbelin and Loic Colson). + +V4.4 saw the first version of (encoded) inductive types. +Now natural numbers could be defined as: +Inductive NAT : Prop = O : NAT | Succ : NAT->NAT. +These inductive types were encoded impredicatively in the calculus, +using a subsystem "rec" due to Christine Paulin. +V4.4 was frozen on March 6th 1988. + +Version 4.5 was the first one to support inductive types and program extraction. +Its banner was "Calcul des Constructions avec Realisations et Synthese". +The vernacular language was enriched to accommodate extraction commands. + +The verification engine design was presented as: +G. Huet. The Constructive Engine. Version 4.5. Invited Conference, 2nd European +Symposium on Programming, Nancy, March 88. +The final paper, describing the V4.9 implementation, appeared in: +A perspective in Theoretical Computer Science, Commemorative Volume in memory +of Gift Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989. + +Version 4.5 was demonstrated in June 1988 at the YoP Institute on Logical +Foundations of Functional Programming organized by Gérard Huet at Austin, Texas. + +Version 4.6 was started during summer 1988. Its main improvement was the +complete rehaul of the proof synthesis engine by Thierry Coquand, with +a tree structure of goals. + +Its source code was communicated to Randy Pollack on September 2nd 1988. +It evolved progressively into LEGO, proof system for Luo's formalism +of Extended Calculus of Constructions. + +The discharge tactic was modified by G. Huet to allow for inter-dependencies +in discharged lemmas. Christine Paulin improved the inductive definition scheme +in order to accommodate predicates of any arity. + +Version 4.7 was started on September 6th, 1988. + +This version starts exploiting the CAML notion of module in order to improve the +modularity of the implementation. Now the term verifier is identified as +a proper module Machine, which the structure of its internal data structures +being hidden and thus accessible only through the legitimate operations. +This machine (the constructive engine) was the trusted core of the +implementation. The proof synthesis mechanism was a separate proof term +generator. Once a complete proof term was synthesized with the help of tactics, +it was entirely re-checked by the engine. Thus there was no need to certify +the tactics, and the system took advantage of this fact by having tactics ignore +the universe levels, universe consistency check being relegated to the final +type-checking pass. This induced a certain puzzlement of early users who saw +their successful proof search ended with QED, followed by silence, followed by +a failure message of universe inconsistency rejection... + +The set of examples comprise set theory experiments by Hugo Herbelin, +and notably the Schroeder-Bernstein theorem. + +Version 4.8, started on October 8th, 1988, saw a major re-implementation of the +abstract syntax type constr, separating variables of the formalism and +metavariables denoting incomplete terms managed by the search mechanism. +A notion of level (with three values TYPE, OBJECT and PROOF) is made explicit +and a type judgement clarifies the constructions, whose implementation is now +fully explicit. Structural equality is speeded up by using pointer equality, +yielding spectacular improvements. Thierry Coquand adapts the proof synthesis +to the new representation, and simplifies pattern matching to 1st order +predicate calculus matching, with important performance gain. + +A new representation of the universe hierarchy is then defined by G. Huet. +Universe levels are now implemented implicitly, through a hidden graph +of abstract levels constrained with an order relation. +Checking acyclicity of the graph insures well-foundedness of the ordering, +and thus consistency. This was documented in a memo +"Adding Type:Type to the Calculus of Constructions" which was never published. + +The development version is released as a stable 4.8 at the end of 1988. + +Version 4.9 is released on March 1st 1989, with the new "elastic" +universe hierarchy. + +The spring 89 saw the first attempt at documenting the system usage, +with a number of papers describing the formalism: +- Metamathematical Investigations of a Calculus of Constructions, by +Thierry Coquand (INRIA Research Report N°1088, Sept. 1989, published in +Logic and Computer Science, ed. P.G. Odifreddi, Academic Press, 1990) +- Inductive definitions in the Calculus of Constructions, by +Christine Paulin-Mohring, +- Extracting Fomega's programs from proofs in the Calculus of Constructions, by +Christine Paulin-Mohring (published in POPL'89) +- The Constructive Engine, by Gérard Huet +as well as a number of user guides: +- A short user's guide for the Constructions Version 4.10, by Gérard Huet +- A Vernacular Syllabus, by Gilles Dowek. +- The Tactics Theorem Prover, User's guide, Version 4.10, by Thierry Coquand. + +Stable V4.10, released on May 1st, 1989, was then a mature system, +distributed with CAML V2.6. + +In the mean time, Thierry Coquand and Christine Paulin-Mohring +had been investigating how to add native inductive types to the +Calculus of Constructions, in the manner of Per Martin-Löf's Intuitionistic +Type Theory. The impredicative encoding had already been presented in: +F. Pfenning and C. Paulin-Mohring. Inductively defined types in the Calculus +of Constructions. Preprint technical report CMU-CS-89-209, final version in +Proceedings of Mathematical Foundations of Programming Semantics, +volume 442, Lecture Notes in Computer Science. Springer-Verlag, 1990. +An extension of the calculus with primitive inductive types appeared in: +Th. Coquand and C. Paulin-Mohring. Inductively defined types. +In P. Martin-Löf and G. Mints, editors, Proceedings of Colog'88, volume 417, +Lecture Notes in Computer Science. Springer-Verlag, 1990. + +This lead to the Calculus of Inductive Constructions, logical formalism +implemented in Versions 5 upward of the system, and documented in: +C. Paulin-Mohring. Inductive Definitions in the System Coq - Rules and +Properties. In M. Bezem and J.-F. Groote, editors, Proceedings of the conference +Typed Lambda Calculi and Applications, volume 664, Lecture Notes in Computer +Science, 1993. + +The last version of CONSTR is Version 4.11, which was last distributed +in Spring 1990. It was demonstrated at the first workshop of the European +Basic Research Action Logical Frameworks In Sophia Antipolis in May 1990. + +At the end of 1989, Version 5.1 was started, and renamed as the system Coq +for the Calculus of Inductive Constructions. It was then ported to the new +stand-alone implementation of ML called Caml-light. + +In 1990 many changes occurred. Thierry Coquand left for Chalmers University +in Göteborg. Christine Paulin-Mohring took a CNRS researcher position +at the LIP laboratory of Ecole Normale Supérieure de Lyon. Project Formel +was terminated, and gave rise to two teams: Cristal at INRIA-Roquencourt, +that continued developments in functional programming with Caml-light then +Ocaml, and Coq, continuing the type theory research, with a joint team +headed by Gérard Huet at INRIA-Rocquencourt and Christine Paulin-Mohring +at the LIP laboratory of CNRS-ENS Lyon. + +Chetan Murthy joined the team in 1991 and became the main software architect +of Version 5. He completely rehauled the implementation for efficiency. +Versions 5.6 and 5.8 were major distributed versions, with complete +documentation and a library of users' developements. The use of the RCS +revision control system, and systematic ChangeLog files, allow a more +precise tracking of the software developments. + +Developments from Version 6 upwards are documented in the credits section of +Coq's Reference Manual. + +September 2015 +Thierry Coquand, Gérard Huet and Christine Paulin-Mohring. diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt index 4c89af01..6a69c579 100644 --- a/dev/doc/univpoly.txt +++ b/dev/doc/univpoly.txt @@ -1,5 +1,5 @@ -Notes on universe polymorphism and primitive projections, M. Sozeau - WIP -========================================================================= +Notes on universe polymorphism and primitive projections, M. Sozeau +=================================================================== The new implementation of universe polymorphism and primitive projections introduces a few changes to the API of Coq. First and @@ -46,15 +46,16 @@ universes and constraints to the global universe context when it is put in the environment. No other universes than the global ones and the declared local ones are needed to check a declaration, hence the kernel does not produce any constraints anymore, apart from module -subtyping.... There are hance two conversion functions now: check_conv -and infer_conv: the former just checks the definition in the current env +subtyping.... There are hence two conversion functions now: [check_conv] +and [infer_conv]: the former just checks the definition in the current env (in which we usually push_universe_context of the associated context), -and infer_conv which produces constraints that were not implied by the +and [infer_conv] which produces constraints that were not implied by the ambient constraints. Ideally, that one could be put out of the kernel, -but again, module subtyping needs it. +but currently module subtyping needs it. Inference of universes is now done during refinement, and the evar_map -carries the incrementally built universe context. [Evd.conversion] is a +carries the incrementally built universe context, starting from the +global universe constraints (see [Evd.from_env]). [Evd.conversion] is a wrapper around [infer_conv] that will do the bookkeeping for you, it uses [evar_conv_x]. There is a universe substitution being built incrementally according to the constraints, so one should normalize at @@ -72,7 +73,7 @@ val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> ta Is the way to make a constr out of a global reference in the new API. If they constr is polymorphic, it will add the necessary constraints to the evar_map. Even if a constr is not polymorphic, we have to take care -of keeping track of it's universes. Typically, using: +of keeping track of its universes. Typically, using: mkApp (coq_id_function, [| A; a |]) @@ -81,11 +82,11 @@ show that A's type is in cumululativity relation with id's type argument, incurring a universe constraint. To do this, one can simply call Typing.resolve_evars env evdref c which will do some infer_conv to produce the right constraints and put them in the evar_map. Of course in -some cases you might now from an invariant that no new constraint would +some cases you might know from an invariant that no new constraint would be produced and get rid of it. Anyway the kernel will tell you if you forgot some. As a temporary way out, [Universes.constr_of_global] allows -you to make a constr from any non-polymorphic constant, but it might -forget constraints. +you to make a constr from any non-polymorphic constant, but it will fail +on polymorphic ones. Other than that, unification (w_unify and evarconv) now take account of universes and produce only well-typed evar_maps. @@ -157,6 +158,30 @@ this is the only solution I found. In the case of global_references only, it's just a matter of using [Evd.fresh_global] / [pf_constr_of_global] to let the system take care of universes. + +The universe graph +================== + +To accomodate universe polymorphic definitions, the graph structure in +kernel/univ.ml was modified. The new API forces every universe to be +declared before it is mentionned in any constraint. This forces to +declare every universe to be >= Set or > Set. Every universe variable +introduced during elaboration is >= Set. Every _global_ universe is now +declared explicitly > Set, _after_ typechecking the definition. In +polymorphic definitions Type@{i} ranges over Set and any other universe +j. However, at instantiation time for polymorphic references, one can +try to instantiate a universe parameter with Prop as well, if the +instantiated constraints allow it. The graph invariants ensure that +no universe i can be set lower than Set, so the chain of universes +always bottoms down at Prop < Set. + +Modules +======= + +One has to think of universes in modules as being globally declared, so +when including a module (type) which declares a type i (e.g. through a +parameter), we get back a copy of i and not some fresh universe. + Projections =========== @@ -208,8 +233,7 @@ constants left (the most common case). E.g. Ring with Set Universe Polymorphism and Set Primitive Projections work (at least it did at some point, I didn't recheck yet). -- [native_compute] is untested: it should deal with primitive -projections right but not universes. +- [native_compute] works with universes and projections. Incompatibilities diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex index 9892a441..1b1d3500 100644 --- a/dev/doc/versions-history.tex +++ b/dev/doc/versions-history.tex @@ -10,55 +10,76 @@ \begin{center} \begin{huge} -An history of Coq versions +A history of Coq versions \end{huge} \end{center} \bigskip \centerline{\large 1984-1989: The Calculus of Constructions} + +\bigskip +\centerline{\large (see README.V1-V5 for details)} \mbox{}\\ \mbox{}\\ \begin{tabular}{l|l|l} version & date & comments \\ \hline -CoC V1.10& mention of dates from 6 December & implementation language is Caml\\ - & 1984 to 13 February 1985 \\ -CoC V1.11& mention of dates from 6 December\\ - & 1984 to 19 February 1985\\ +CONSTR V1.10& mention of dates from 6 December & \feature{type-checker for Coquand's Calculus }\\ + & 1984 to 13 February 1985 & \feature{of Constructions}, implementation \\ + & frozen 22 December 1984 & language is a predecessor of CAML\\ + +CONSTR V1.11& mention of dates from 6 December\\ + & 1984 to 19 February 1985 (freeze date) &\\ + +CoC V2.8& dated 16 December 1985 (freeze date)\\ -CoC V2.13& dated 16 December 1985\\ +CoC V2.9& & \feature{cumulative hierarchy of universes}\\ -CoC V2.13& dated 25 June 1986\\ +CoC V2.13& dated 25 June 1986 (freeze date)\\ -CoC V3.1& dated 20 November 1986 & \feature{auto}\\ +CoC V3.1& started summer 1986 & \feature{AUTO tactic}\\ + & dated 20 November 1986 & implementation language now named CAML\\ CoC V3.2& dated 27 November 1986\\ -CoC V3.3 and V3.4& dated 1 January 1987 & creation of a directory for examples\\ +CoC V3.3& dated 1 January 1987 & creation of a directory for examples\\ -CoC V4.1& dated 24 July 1987\\ +CoC V3.4& dated 1 January 1987 & \feature{lambda and product distinguished in the syntax}\\ + +CoC V4.1& dated 24 July 1987 (freeze date)\\ CoC V4.2& dated 10 September 1987\\ -CoC V4.3& dated 15 September 1987\\ +CoC V4.3& dated 15 September 1987 & \feature{mathematical vernacular toplevel}\\ + & frozen November 1987 & \feature{section mechanism}\\ + & & \feature{logical vs computational content (sorte Spec)}\\ + & & \feature{LCF engine}\\ + +CoC V4.4& dated 27 January 1988 & \feature{impredicatively encoded inductive types}\\ + & frozen March 1988\\ -CoC V4.4& dated 27 January 1988\\ +CoC V4.5 and V4.5.5& dated 15 March 1988 & \feature{program extraction}\\ + & demonstrated in June 1988\\ -CoC V4.5 and V4.5.5& dated 15 March 1988\\ +CoC V4.6& dated 1 September 1988 & start of LEGO fork\\ -CoC V4.6 and V4.7& dated 1 September 1988\\ +CoC V4.7& started 6 September 1988 \\ -CoC V4.8& dated 1 December 1988\\ +CoC V4.8& dated 1 December 1988 (release time) & \feature{floating universes}\\ -CoC V4.8.5& dated 1 February 1989\\ +CoC V4.8.5& dated 1 February 1989 & \\ -CoC V4.9& dated 1 March 1989\\ +CoC V4.9& dated 1 March 1989 (release date)\\ -CoC V4.10 and 4.10.1& dated 1 May 1989 & first public release - in English\\ +CoC V4.10 and 4.10.1& dated 1 May 1989 & released with documentation in English\\ \end{tabular} \bigskip + +\noindent Note: CoC above stands as an abbreviation for {\em Calculus of + Constructions}, official name of the system. +\bigskip \bigskip \newpage @@ -80,7 +101,7 @@ Coq V5.2 & log dated 4 October 1990 & internal use \\ Coq V5.3 & log dated 12 October 1990 & internal use \\ -Coq V5.4 & headers dated 24 October 1990 & internal use, \feature{extraction} (version 1) [3-12-90]\\ +Coq V5.4 & headers dated 24 October 1990 & internal use, new \feature{extraction} (version 1) [3-12-90]\\ Coq V5.5 & started 6 December 1990 & internal use \\ @@ -265,7 +286,17 @@ Coq V7.3.1& released 5 October 2002 & \feature{module system} [2-8-2002]\\ & & \feature{pattern-matching compilation} (version 2) [13-6-2002]\\ Coq V7.4& released 6 February 2003 & \feature{notation}, \feature{scopes} [13-10-2002]\\ +\end{tabular} +\medskip +\bigskip + +\centerline{V- New concrete syntax} +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +version & date & comments \\ +\hline Coq V8.0& released 21 April 2004 & \feature{new concrete syntax}, \feature{Set predicative}, \feature{CoqIDE} [from 4-2-2003]\\ Coq V8.0pl1& released 18 July 2004\\ @@ -307,6 +338,46 @@ Coq V8.2 & released 17 February 2009 & \feature{type classes} [10-12-2007], \fea & & a first package released on February 11 was incomplete\\ +Coq V8.2pl1& released 4 July 2009 & \\ +Coq V8.2pl2& released 29 June 2010 & \\ +\end{tabular} + +\medskip +\bigskip + +\newpage +\mbox{}\\ +\mbox{}\\ +\begin{tabular}{l|l|l} +Coq V8.3 beta & released 16 February 2010 & \feature{MSets library} [13-10-2009] \\ +Coq V8.3 & released 14 October 2010 & \feature{nsatz} [3-6-2010] \\ +Coq V8.3pl1& released 23 December 2010 & \\ +Coq V8.3pl2& released 19 April 2011 & \\ +Coq V8.3pl3& released 19 December 2011 & \\ +Coq V8.3pl3& released 26 March 2012 & \\ +Coq V8.3pl5& released 28 September 2012 & \\ +Coq V8.4 beta & released 27 December 2011 & \feature{modular arithmetic library} [2010-2012]\\ +&& \feature{vector library} [10-12-2010]\\ +&& \feature{structured scripts} [22-4-2010]\\ +&& \feature{eta-conversion} [20-9-2010]\\ +&& \feature{new proof engine available} [10-12-2010]\\ +Coq V8.4 beta2 & released 21 May 2012 & \\ +Coq V8.4 & released 12 August 2012 &\\ +Coq V8.4pl1& released 22 December 2012 & \\ +Coq V8.4pl2& released 4 April 2013 & \\ +Coq V8.4pl3& released 21 December 2013 & \\ +Coq V8.4pl4& released 24 April 2014 & \\ +Coq V8.4pl5& released 22 October 2014 & \\ +Coq V8.4pl6& released 9 April 2015 & \\ + +Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation to OCaml} [22-1-2013]\\ +&& \feature{asynchonous evaluation} [8-8-2013]\\ +&& \feature{new proof engine deployed} [2-11-2013]\\ +&& \feature{universe polymorphism} [6-5-2014]\\ +&& \feature{primitive projections} [6-5-2014]\\ + +Coq V8.5 beta2 & released 22 April 2015 & \feature{MMaps library} [4-3-2015]\\ + \end{tabular} \medskip diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh index ec7cd577..d405e66c 100755 --- a/dev/make-installer-win32.sh +++ b/dev/make-installer-win32.sh @@ -1,11 +1,13 @@ #!/bin/sh +set -e + NSIS="$BASE/NSIS/makensis" ZIP=_make.zip URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download -[ -e config/Makefile ] || ./configure -prefix ./ -with-doc no +[ -e config/Makefile ] || ./configure -debug -prefix ./ -with-doc no make -j2 if [ ! -e bin/make.exe ]; then wget -O $ZIP $URL1 && 7z x $ZIP "bin/*" diff --git a/dev/make-installer-win64.sh b/dev/make-installer-win64.sh new file mode 100755 index 00000000..2f765c1a --- /dev/null +++ b/dev/make-installer-win64.sh @@ -0,0 +1,28 @@ +#!/bin/sh + +set -e + +NSIS="$BASE/NSIS/makensis" +ZIP=_make.zip +URL1=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-bin.zip/download +URL2=http://sourceforge.net/projects/gnuwin32/files/make/3.81/make-3.81-dep.zip/download + +[ -e config/Makefile ] || ./configure -debug -prefix ./ -with-doc no +make -j2 coqide +mkdir -p bin32 +cp bin/* bin32/ +make clean +make archclean +( . ${BASE}_64/environ && ./configure -debug -prefix ./ -with-doc no && make -j2 && make ide/coqidetop.cmxs ) +cp bin32/coqide* bin/ +if [ ! -e bin/make.exe ]; then + wget -O $ZIP $URL1 && 7z x $ZIP "bin/*" + wget -O $ZIP $URL2 && 7z x $ZIP "bin/*" + rm -rf $ZIP +fi +VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2` +cd dev/nsis +"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" coq.nsi +echo Installer: +ls -h $PWD/*exe +cd ../.. diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi index 5b421e49..67649051 100755 --- a/dev/nsis/coq.nsi +++ b/dev/nsis/coq.nsi @@ -95,8 +95,8 @@ Section "Coq" Sec1 File /r ${COQ_SRC_PATH}\theories\*.vo File /r ${COQ_SRC_PATH}\theories\*.v File /r ${COQ_SRC_PATH}\theories\*.glob - File /r ${COQ_SRC_PATH}\theories\*.cmi - File /r ${COQ_SRC_PATH}\theories\*.cmxs + ; File /r ${COQ_SRC_PATH}\theories\*.cmi + ; File /r ${COQ_SRC_PATH}\theories\*.cmxs SetOutPath "$INSTDIR\lib\plugins" File /r ${COQ_SRC_PATH}\plugins\*.vo File /r ${COQ_SRC_PATH}\plugins\*.v diff --git a/dev/printers.mllib b/dev/printers.mllib index 2f78c2e9..07b48ed5 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -27,13 +27,14 @@ Pp Segmenttree Unicodetable Unicode -Errors CObj CList CString CArray CStack Util +Ppstyle +Errors Bigint Dyn CUnix @@ -109,7 +110,6 @@ Loadpath Goptions Decls Heads -Assumptions Keys Locusops Miscops @@ -154,7 +154,6 @@ Tok Lexer Ppextend Pputils -Ppstyle Ppannotation Stdarg Constrarg @@ -204,6 +203,7 @@ Hints Himsg Cerrors Locality +Assumptions Vernacinterp Dischargedhypsmap Discharge diff --git a/dev/top_printers.ml b/dev/top_printers.ml index f969f013..f9f2e1b0 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -229,6 +229,11 @@ let ppenv e = pp (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]") +let ppenvwithcst e = pp + (str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++ + str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++ + str "{" ++ Cmap_env.fold (fun a _ s -> pr_con a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}") + let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x)) let ppobj obj = Format.print_string (Libobject.object_tag obj) diff --git a/dev/v8-syntax/memo-v8.tex b/dev/v8-syntax/memo-v8.tex index 8d116de2..ae4b569b 100644 --- a/dev/v8-syntax/memo-v8.tex +++ b/dev/v8-syntax/memo-v8.tex @@ -253,7 +253,7 @@ became \TERM{context}. Syntax is unified with subterm matching. \subsection{Occurrences} To avoid ambiguity between a numeric literal and the optionnal -occurence numbers of this term, the occurence numbers are put after +occurrence numbers of this term, the occurrence numbers are put after the term itself. This applies to tactic \TERM{pattern} and also \TERM{unfold} \begin{transbox} diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 4578a3b3..1c501df8 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -13,7 +13,7 @@ let ppripos (ri,pos) = ("annot : MutInd("^(string_of_mind sp)^","^(string_of_int i)^")\n") | Reloc_const _ -> print_string "structured constant\n" - | Reloc_getglobal (kn,_) -> + | Reloc_getglobal kn -> print_string ("getglob "^(string_of_con kn)^"\n")); print_flush () @@ -30,7 +30,7 @@ let ppsort = function let print_idkey idk = match idk with - | ConstKey (sp,_) -> + | ConstKey sp -> print_string "Cons("; print_string (string_of_con sp); print_string ")" @@ -49,6 +49,7 @@ let rec ppzipper z = close_box() | Zfix _ -> print_string "Zfix" | Zswitch _ -> print_string "Zswitch" + | Zproj _ -> print_string "Zproj" and ppstack s = open_hovbox 0; @@ -60,8 +61,8 @@ and ppstack s = and ppatom a = match a with | Aid idk -> print_idkey idk - | Aiddef(idk,_) -> print_string "&";print_idkey idk - | Aind((sp,i),_) -> print_string "Ind("; + | Atype u -> print_string "Type(...)" + | Aind(sp,i) -> print_string "Ind("; print_string (string_of_mind sp); print_string ","; print_int i; print_string ")" @@ -78,6 +79,7 @@ and ppwhd whd = | Vatom_stk(a,s) -> open_hbox();ppatom a;close_box(); print_string"@";ppstack s + | Vuniv_level lvl -> Pp.pp (Univ.Level.pr lvl) and ppvblock b = open_hbox(); diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex old mode 100755 new mode 100644 diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 024e1341..866193ff 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -591,7 +591,7 @@ through the Require Import command.

Program: - Support for dependently-typed programming. + Support for dependently-typed programming
theories/Program/Basics.v @@ -612,4 +612,12 @@ through the Require Import command.

theories/Unicode/Utf8_core.v theories/Unicode/Utf8.v
+ +
Compat: + Compatibility wrappers for previous versions of Coq +
+
+ theories/Compat/Coq84.v + theories/Compat/Coq85.v +
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 0b168377..60ea0df0 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -1,6 +1,7 @@ Coq_config Hook +Terminal Canary Hashset Hashcons @@ -19,12 +20,14 @@ Serialize Stateid Feedback Pp -Errors + CList CString CArray CStack Util +Ppstyle +Errors Bigint Predicate Segmenttree diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 0421ad7c..66f82fcd 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "tools/compat5b.cmo" i*) +(** Implementation of the TACTIC EXTEND macro. *) + open Util open Pp open Names @@ -172,17 +174,17 @@ let is_constr_gram = function | Aentry ("constr", "constr") -> true | _ -> false -let make_vars len = - (** We choose names unlikely to be written by a human, even though that - does not matter at all. *) - List.init len (fun i -> Some (Id.of_string (Printf.sprintf "_%i" i))) +let make_var = function + | GramNonTerminal(loc',_,_,Some p) -> Some p + | GramNonTerminal(loc',_,_,None) -> Some (Id.of_string "_") + | _ -> assert false let declare_tactic loc s c cl = match cl with | [(GramTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem -> (** The extension is only made of a name followed by constr entries: we do not add any grammar nor printing rule and add it as a true Ltac definition. *) let patt = make_patt rem in - let vars = make_vars (List.length rem) in + let vars = List.map make_var rem in let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in let entry = mlexpr_of_string s in let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 9db89308..03061d8b 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "tools/compat5b.cmo" i*) +(** Implementation of the VERNAC EXTEND macro. *) + open Pp open Util open Q_util diff --git a/ide/config_lexer.mll b/ide/config_lexer.mll index 87cc6d06..36715356 100644 --- a/ide/config_lexer.mll +++ b/ide/config_lexer.mll @@ -17,7 +17,7 @@ let space = [' ' '\010' '\013' '\009' '\012'] let char = ['A'-'Z' 'a'-'z' '_' '0'-'9'] -let ident = char+ +let ident = (char | '.')+ let ignore = space | ('#' [^ '\n']*) rule prefs m = parse diff --git a/ide/coq-ssreflect.lang b/ide/coq-ssreflect.lang index 4c488ae8..7cfc1670 100644 --- a/ide/coq-ssreflect.lang +++ b/ide/coq-ssreflect.lang @@ -190,6 +190,7 @@ Eval Load Undo + Restart Goal Print Save diff --git a/ide/coq.lang b/ide/coq.lang index 65150d6a..e25eedbc 100644 --- a/ide/coq.lang +++ b/ide/coq.lang @@ -5,7 +5,7 @@ \(\* \*\) - +