diff options
| -rw-r--r-- | .gitignore | 8 | ||||
| -rw-r--r-- | .merlin | 2 | ||||
| -rw-r--r-- | .travis.yml | 1 | ||||
| -rw-r--r-- | Makefile.ci | 7 | ||||
| -rw-r--r-- | Makefile.common | 16 | ||||
| -rw-r--r-- | Makefile.dev | 7 | ||||
| -rwxr-xr-x | configure | 2 | ||||
| -rw-r--r-- | dev/Makefile.oug | 74 | ||||
| -rw-r--r-- | dev/base_include | 4 | ||||
| -rw-r--r-- | dev/ci/ci-common.sh | 46 | ||||
| -rwxr-xr-x | dev/ci/ci-compcert.sh | 5 | ||||
| -rwxr-xr-x | dev/ci/ci-coquelicot.sh | 21 | ||||
| -rwxr-xr-x | dev/ci/ci-fiat-crypto.sh | 5 | ||||
| -rwxr-xr-x | dev/ci/ci-flocq.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-geocoq.sh | 8 | ||||
| -rwxr-xr-x | dev/ci/ci-hott.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-iris-coq.sh | 24 | ||||
| -rwxr-xr-x | dev/ci/ci-math-classes.sh | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-math-comp.sh | 10 | ||||
| -rwxr-xr-x | dev/ci/ci-metacoq.sh | 4 | ||||
| -rwxr-xr-x | dev/ci/ci-tlc.sh | 2 | ||||
| -rwxr-xr-x | dev/ci/ci-unimath.sh | 15 | ||||
| -rw-r--r-- | dev/core.dbg | 1 | ||||
| -rw-r--r-- | dev/doc/changes.txt | 18 | ||||
| -rw-r--r-- | dev/ocamldebug-coq.run | 4 | ||||
| -rw-r--r-- | dev/top_printers.ml | 2 | ||||
| -rw-r--r-- | engine/proofview.ml | 29 | ||||
| -rw-r--r-- | engine/proofview.mli | 1 | ||||
| -rw-r--r-- | interp/constrintern.ml | 3 | ||||
| -rw-r--r-- | interp/notation.ml | 14 | ||||
| -rw-r--r-- | interp/ppextend.ml | 6 | ||||
| -rw-r--r-- | interp/ppextend.mli | 3 | ||||
| -rw-r--r-- | interp/topconstr.ml | 11 | ||||
| -rw-r--r-- | kernel/cbytecodes.ml | 2 | ||||
| -rw-r--r-- | kernel/fast_typeops.ml | 464 | ||||
| -rw-r--r-- | kernel/fast_typeops.mli | 24 | ||||
| -rw-r--r-- | kernel/kernel.mllib | 1 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 1 | ||||
| -rw-r--r-- | kernel/typeops.ml | 561 | ||||
| -rw-r--r-- | kernel/typeops.mli | 18 | ||||
| -rw-r--r-- | lib/pp.ml | 15 | ||||
| -rw-r--r-- | lib/pp.mli | 5 | ||||
| -rw-r--r-- | lib/unicode.ml | 24 | ||||
| -rw-r--r-- | plugins/btauto/g_btauto.ml4 | 2 | ||||
| -rw-r--r-- | plugins/cc/ccalgo.ml | 2 | ||||
| -rw-r--r-- | plugins/cc/g_congruence.ml4 | 1 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 1 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 1 | ||||
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 1 | ||||
| -rw-r--r-- | plugins/decl_mode/ppdecl_proof.ml | 1 | ||||
| -rw-r--r-- | plugins/extraction/common.ml | 16 | ||||
| -rw-r--r-- | plugins/extraction/common.mli | 2 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.ml | 3 | ||||
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/g_extraction.ml4 | 1 | ||||
| -rw-r--r-- | plugins/extraction/ocaml.ml | 89 | ||||
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 1 | ||||
| -rw-r--r-- | plugins/firstorder/ground.ml | 1 | ||||
| -rw-r--r-- | plugins/fourier/g_fourier.ml4 | 1 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 1 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 8 | ||||
| -rw-r--r-- | plugins/ltac/Ltac.v (renamed from ltac/tauto.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/coretactics.ml4 (renamed from ltac/coretactics.ml4) | 0 | ||||
| -rw-r--r-- | plugins/ltac/evar_tactics.ml (renamed from ltac/evar_tactics.ml) | 0 | ||||
| -rw-r--r-- | plugins/ltac/evar_tactics.mli (renamed from ltac/evar_tactics.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/extraargs.ml4 (renamed from ltac/extraargs.ml4) | 0 | ||||
| -rw-r--r-- | plugins/ltac/extraargs.mli (renamed from ltac/extraargs.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.ml4 (renamed from ltac/extratactics.ml4) | 0 | ||||
| -rw-r--r-- | plugins/ltac/extratactics.mli (renamed from ltac/extratactics.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/g_auto.ml4 (renamed from ltac/g_auto.ml4) | 0 | ||||
| -rw-r--r-- | plugins/ltac/g_class.ml4 (renamed from ltac/g_class.ml4) | 0 | ||||
| -rw-r--r-- | plugins/ltac/g_eqdecide.ml4 (renamed from ltac/g_eqdecide.ml4) | 0 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 (renamed from ltac/g_ltac.ml4) | 0 | ||||
| -rw-r--r-- | plugins/ltac/g_obligations.ml4 (renamed from ltac/g_obligations.ml4) | 0 | ||||
| -rw-r--r-- | plugins/ltac/g_rewrite.ml4 (renamed from ltac/g_rewrite.ml4) | 0 | ||||
| -rw-r--r-- | plugins/ltac/g_tactic.ml4 (renamed from ltac/g_tactic.ml4) | 0 | ||||
| -rw-r--r-- | plugins/ltac/ltac_plugin.mlpack (renamed from ltac/ltac.mllib) | 0 | ||||
| -rw-r--r-- | plugins/ltac/pltac.ml (renamed from ltac/pltac.ml) | 0 | ||||
| -rw-r--r-- | plugins/ltac/pltac.mli (renamed from ltac/pltac.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.ml (renamed from ltac/pptactic.ml) | 9 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.mli (renamed from ltac/pptactic.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/pptacticsig.mli (renamed from ltac/pptacticsig.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/profile_ltac.ml (renamed from ltac/profile_ltac.ml) | 0 | ||||
| -rw-r--r-- | plugins/ltac/profile_ltac.mli (renamed from ltac/profile_ltac.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/profile_ltac_tactics.ml4 (renamed from ltac/profile_ltac_tactics.ml4) | 0 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml (renamed from ltac/rewrite.ml) | 0 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.mli (renamed from ltac/rewrite.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tacarg.ml (renamed from ltac/tacarg.ml) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tacarg.mli (renamed from ltac/tacarg.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.ml (renamed from ltac/taccoerce.ml) | 0 | ||||
| -rw-r--r-- | plugins/ltac/taccoerce.mli (renamed from ltac/taccoerce.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.ml (renamed from ltac/tacentries.ml) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.mli (renamed from ltac/tacentries.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tacenv.ml (renamed from ltac/tacenv.ml) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tacenv.mli (renamed from ltac/tacenv.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tacexpr.mli (renamed from ltac/tacexpr.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tacintern.ml (renamed from ltac/tacintern.ml) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tacintern.mli (renamed from ltac/tacintern.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml (renamed from ltac/tacinterp.ml) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.mli (renamed from ltac/tacinterp.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tacsubst.ml (renamed from ltac/tacsubst.ml) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tacsubst.mli (renamed from ltac/tacsubst.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tactic_debug.ml (renamed from ltac/tactic_debug.ml) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tactic_debug.mli (renamed from ltac/tactic_debug.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tactic_matching.ml (renamed from ltac/tactic_matching.ml) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tactic_matching.mli (renamed from ltac/tactic_matching.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tactic_option.ml (renamed from ltac/tactic_option.ml) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tactic_option.mli (renamed from ltac/tactic_option.mli) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tauto.ml (renamed from ltac/tauto.ml) | 0 | ||||
| -rw-r--r-- | plugins/ltac/tauto.mli | 0 | ||||
| -rw-r--r-- | plugins/ltac/vo.itarget | 1 | ||||
| -rw-r--r-- | plugins/micromega/g_micromega.ml4 | 1 | ||||
| -rw-r--r-- | plugins/nsatz/g_nsatz.ml4 | 4 | ||||
| -rw-r--r-- | plugins/omega/g_omega.ml4 | 1 | ||||
| -rw-r--r-- | plugins/quote/g_quote.ml4 | 1 | ||||
| -rw-r--r-- | plugins/romega/g_romega.ml4 | 1 | ||||
| -rw-r--r-- | plugins/rtauto/g_rtauto.ml4 | 2 | ||||
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 1 | ||||
| -rw-r--r-- | plugins/setoid_ring/g_newring.ml4 | 1 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 1 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 1 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 6 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 7 | ||||
| -rw-r--r-- | stm/stm.ml | 285 | ||||
| -rw-r--r-- | stm/stm.mli | 7 | ||||
| -rw-r--r-- | stm/stm.mllib | 1 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 13 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 1 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3612.v | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3649.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4121.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4527.v | 1 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4533.v | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4544.v | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5346.v | 29 | ||||
| -rw-r--r-- | test-suite/output/Search.out | 114 | ||||
| -rw-r--r-- | test-suite/output/SearchHead.out | 42 | ||||
| -rw-r--r-- | test-suite/output/SearchPattern.out | 84 | ||||
| -rw-r--r-- | theories/Init/Notations.v | 3 | ||||
| -rw-r--r-- | tools/coq_makefile.ml | 6 | ||||
| -rw-r--r-- | tools/coqmktop.ml | 1 | ||||
| -rw-r--r-- | tools/gallina-db.el | 2 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/toplevel.mllib | 16 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 6 | ||||
| -rw-r--r-- | vernac/assumptions.ml (renamed from toplevel/assumptions.ml) | 0 | ||||
| -rw-r--r-- | vernac/assumptions.mli (renamed from toplevel/assumptions.mli) | 0 | ||||
| -rw-r--r-- | vernac/auto_ind_decl.ml (renamed from toplevel/auto_ind_decl.ml) | 0 | ||||
| -rw-r--r-- | vernac/auto_ind_decl.mli (renamed from toplevel/auto_ind_decl.mli) | 0 | ||||
| -rw-r--r-- | vernac/class.ml (renamed from toplevel/class.ml) | 0 | ||||
| -rw-r--r-- | vernac/class.mli (renamed from toplevel/class.mli) | 0 | ||||
| -rw-r--r-- | vernac/classes.ml (renamed from toplevel/classes.ml) | 0 | ||||
| -rw-r--r-- | vernac/classes.mli (renamed from toplevel/classes.mli) | 0 | ||||
| -rw-r--r-- | vernac/command.ml (renamed from toplevel/command.ml) | 0 | ||||
| -rw-r--r-- | vernac/command.mli (renamed from toplevel/command.mli) | 0 | ||||
| -rw-r--r-- | vernac/discharge.ml (renamed from toplevel/discharge.ml) | 0 | ||||
| -rw-r--r-- | vernac/discharge.mli (renamed from toplevel/discharge.mli) | 0 | ||||
| -rw-r--r-- | vernac/doc.tex (renamed from toplevel/doc.tex) | 0 | ||||
| -rw-r--r-- | vernac/explainErr.ml (renamed from toplevel/explainErr.ml) | 0 | ||||
| -rw-r--r-- | vernac/explainErr.mli (renamed from toplevel/explainErr.mli) | 0 | ||||
| -rw-r--r-- | vernac/himsg.ml (renamed from toplevel/himsg.ml) | 0 | ||||
| -rw-r--r-- | vernac/himsg.mli (renamed from toplevel/himsg.mli) | 0 | ||||
| -rw-r--r-- | vernac/ind_tables.ml (renamed from toplevel/ind_tables.ml) | 0 | ||||
| -rw-r--r-- | vernac/ind_tables.mli (renamed from toplevel/ind_tables.mli) | 0 | ||||
| -rw-r--r-- | vernac/indschemes.ml (renamed from toplevel/indschemes.ml) | 0 | ||||
| -rw-r--r-- | vernac/indschemes.mli (renamed from toplevel/indschemes.mli) | 0 | ||||
| -rw-r--r-- | vernac/lemmas.ml (renamed from stm/lemmas.ml) | 0 | ||||
| -rw-r--r-- | vernac/lemmas.mli (renamed from stm/lemmas.mli) | 0 | ||||
| -rw-r--r-- | vernac/locality.ml (renamed from toplevel/locality.ml) | 0 | ||||
| -rw-r--r-- | vernac/locality.mli (renamed from toplevel/locality.mli) | 0 | ||||
| -rw-r--r-- | vernac/metasyntax.ml (renamed from toplevel/metasyntax.ml) | 249 | ||||
| -rw-r--r-- | vernac/metasyntax.mli (renamed from toplevel/metasyntax.mli) | 0 | ||||
| -rw-r--r-- | vernac/mltop.ml (renamed from toplevel/mltop.ml) | 0 | ||||
| -rw-r--r-- | vernac/mltop.mli (renamed from toplevel/mltop.mli) | 0 | ||||
| -rw-r--r-- | vernac/obligations.ml (renamed from toplevel/obligations.ml) | 6 | ||||
| -rw-r--r-- | vernac/obligations.mli (renamed from toplevel/obligations.mli) | 6 | ||||
| -rw-r--r-- | vernac/record.ml (renamed from toplevel/record.ml) | 3 | ||||
| -rw-r--r-- | vernac/record.mli (renamed from toplevel/record.mli) | 0 | ||||
| -rw-r--r-- | vernac/search.ml (renamed from toplevel/search.ml) | 66 | ||||
| -rw-r--r-- | vernac/search.mli (renamed from toplevel/search.mli) | 8 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 17 | ||||
| -rw-r--r-- | vernac/vernacentries.ml (renamed from toplevel/vernacentries.ml) | 85 | ||||
| -rw-r--r-- | vernac/vernacentries.mli (renamed from toplevel/vernacentries.mli) | 0 | ||||
| -rw-r--r-- | vernac/vernacinterp.ml (renamed from toplevel/vernacinterp.ml) | 0 | ||||
| -rw-r--r-- | vernac/vernacinterp.mli (renamed from toplevel/vernacinterp.mli) | 0 |
186 files changed, 1217 insertions, 1499 deletions
diff --git a/.gitignore b/.gitignore index 7434f62127..35cdf9b4e8 100644 --- a/.gitignore +++ b/.gitignore @@ -122,10 +122,10 @@ g_*.ml ide/project_file.ml parsing/compat.ml parsing/cLexer.ml -ltac/coretactics.ml -ltac/extratactics.ml -ltac/extraargs.ml -ltac/profile_ltac_tactics.ml +plugins/ltac/coretactics.ml +plugins/ltac/extratactics.ml +plugins/ltac/extraargs.ml +plugins/ltac/profile_ltac_tactics.ml ide/coqide_main.ml plugins/ssrmatching/ssrmatching.ml @@ -34,6 +34,8 @@ S stm B stm S toplevel B toplevel +S vernac +B vernac S tools B tools diff --git a/.travis.yml b/.travis.yml index 188e446007..de16f2d0b4 100644 --- a/.travis.yml +++ b/.travis.yml @@ -36,6 +36,7 @@ env: - TEST_TARGET="ci-math-classes" - TEST_TARGET="ci-math-comp" - TEST_TARGET="ci-sf" + - TEST_TARGET="ci-unimath" # Not ready yet for 8.7 # - TEST_TARGET="ci-metacoq" # - TEST_TARGET="ci-tlc" diff --git a/Makefile.ci b/Makefile.ci index 040144e6e8..e4b5832f60 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -1,6 +1,7 @@ -CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \ - ci-color ci-math-classes ci-tlc ci-fiat-crypto \ - ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq +CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \ + ci-color ci-math-classes ci-tlc ci-fiat-crypto \ + ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \ + ci-unimath .PHONY: $(CI_TARGETS) diff --git a/Makefile.common b/Makefile.common index 49fe1fd939..df705034e7 100644 --- a/Makefile.common +++ b/Makefile.common @@ -53,16 +53,16 @@ INSTALLSH:=./install.sh MKDIR:=install -d CORESRCDIRS:=\ - config lib kernel kernel/byterun library \ - proofs tactics pretyping interp stm \ - toplevel parsing printing intf engine ltac + config lib kernel intf kernel/byterun library \ + engine pretyping interp proofs parsing printing \ + tactics vernac stm toplevel PLUGINDIRS:=\ omega romega micromega quote \ setoid_ring extraction fourier \ cc funind firstorder derive \ rtauto nsatz syntax decl_mode btauto \ - ssrmatching + ssrmatching ltac SRCDIRS:=\ $(CORESRCDIRS) \ @@ -77,14 +77,13 @@ BYTERUN:=$(addprefix kernel/byterun/, \ coq_fix_code.o coq_memory.o coq_values.o coq_interp.o ) # LINK ORDER: -# Beware that highparsing.cma should appear before ltac.cma # respecting this order is useful for developers that want to load or link # the libraries directly CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ - parsing/parsing.cma printing/printing.cma tactics/tactics.cma \ - stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma + parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ + stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma @@ -120,6 +119,7 @@ OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \ string_syntax_plugin.cmo ) DECLMODECMO:=plugins/decl_mode/decl_mode_plugin.cmo DERIVECMO:=plugins/derive/derive_plugin.cmo +LTACCMO:=plugins/ltac/ltac_plugin.cmo SSRMATCHINGCMO:=plugins/ssrmatching/ssrmatching_plugin.cmo PLUGINSCMO:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \ @@ -127,7 +127,7 @@ PLUGINSCMO:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) $(DECLMODECMO) \ $(FOURIERCMO) $(EXTRACTIONCMO) \ $(CCCMO) $(FOCMO) $(RTAUTOCMO) $(BTAUTOCMO) \ $(FUNINDCMO) $(NSATZCMO) $(NATSYNTAXCMO) $(OTHERSYNTAXCMO) \ - $(DERIVECMO) $(SSRMATCHINGCMO) + $(DERIVECMO) $(SSRMATCHINGCMO) $(LTACCMO) ifeq ($(HASNATDYNLINK)-$(BEST),false-opt) STATICPLUGINS:=$(PLUGINSCMO) diff --git a/Makefile.dev b/Makefile.dev index 8c1812da18..ea6b8b9194 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -121,10 +121,9 @@ pretyping: pretyping/pretyping.cma highparsing: parsing/highparsing.cma stm: stm/stm.cma toplevel: toplevel/toplevel.cma -ltac: ltac/ltac.cma .PHONY: lib kernel byterun library proofs tactics interp parsing pretyping -.PHONY: engine highparsing stm toplevel ltac +.PHONY: engine highparsing stm toplevel ###################### ### 3) theories files @@ -183,6 +182,7 @@ RTAUTOVO:=$(filter plugins/rtauto/%, $(PLUGINSVO)) EXTRACTIONVO:=$(filter plugins/extraction/%, $(PLUGINSVO)) CCVO:= DERIVEVO:=$(filter plugins/derive/%, $(PLUGINSVO)) +LTACVO:=$(filter plugins/ltac/%, $(PLUGINSVO)) omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO) micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) @@ -194,9 +194,10 @@ funind: $(FUNINDCMO) $(FUNINDVO) cc: $(CCVO) $(CCCMO) rtauto: $(RTAUTOVO) $(RTAUTOCMO) btauto: $(BTAUTOVO) $(BTAUTOCMO) +ltac: $(LTACVO) $(LTACCMO) .PHONY: omega micromega setoid_ring nsatz extraction -.PHONY: fourier funind cc rtauto btauto +.PHONY: fourier funind cc rtauto btauto ltac ################################# ### Misc other development rules @@ -26,7 +26,7 @@ done ## We check that $cmd is ok before the real exec $cmd -`$cmd -version > /dev/null 2>&1` && exec $cmd $script "$@" +`$cmd -version > /dev/null 2>&1` && exec $cmd -w "-3" $script "$@" ## If we're still here, something is wrong with $cmd diff --git a/dev/Makefile.oug b/dev/Makefile.oug deleted file mode 100644 index ee69ea80df..0000000000 --- a/dev/Makefile.oug +++ /dev/null @@ -1,74 +0,0 @@ -####################################################################### -# v # The Coq Proof Assistant / The Coq Development Team # -# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay # -# \VV/ ############################################################# -# // # This file is distributed under the terms of the # -# # GNU Lesser General Public License Version 2.1 # -####################################################################### - - -#### Source Code Analysis via Oug #### -#### Cf http://home.gna.org/oug #### - - -# To be used from top dir : make -f dev/Makefile.oug ... - -include Makefile.build - -# Oug location: in the path by default, native version - -OUG:=oug.x - -# NB: coq should have been compiled with the same ocaml version as oug - -# NOTA: it seems we obtain more useless elements reported when _not_ -# providing the .mli files, and also when giving a precise start point. -# TO BE INVESTIGATED - -ml_of_cma = $(patsubst %.cmo,%.ml,$(filter %.cmo,$(shell cat $(1:.cma=.mllib.d)))) -local_ml_of_cma = $(filter $(dir $(1))%,$(call ml_of_cma,$(1))) -mli_of_ml = $(foreach ml,$(1),$(wildcard $(ml)i)) - -# Analysis of coqtop, without plugins - -COREML:=config/coq_config.ml $(call ml_of_cma, $(CORECMA)) -COREMLI:=$(call mli_of_ml,$(COREML)) - -core.oug: - $(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(COREML) - -core.useless: core.oug - $(OUG) --load-data $< --no-reduce --print-loc --roots "<Coqtop.start>" --useless-elements $@ - -core_intf.oug: - $(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(COREML) $(COREMLI) - -core_intf.useless: core_intf.oug - $(OUG) --load-data $< --no-reduce --print-loc --roots "<Coqtop.start>" --useless-elements $@ - -# Analysis of coqchk, considering only files in the checker/ subdir - -CHECKERML:=$(call local_ml_of_cma,checker/check.cma) -CHECKERMLI:=$(call mli_of_ml,$(CHECKERML)) - -## BUG: in oug, include dirs have reversed priority compared with ocaml, cannot use CHKLIBS -MYCHKINCL:=$(MLINCLUDES) -I checker - -checker.oug: - $(OUG) --dump-data $@ -rectypes $(MYCHKINCL) $(CHECKERML) #$(CHECKERMLI) - -checker.useless: checker.oug - $(OUG) --load-data $< --no-reduce --print-loc --roots "<Checker.start>" --useless-elements $@ - -# Analysis of extraction - -EXTRACTIONML:=$(call local_ml_of_cma,$(EXTRACTIONCMA)) -EXTRACTIONMLI:=$(call mli_of_ml,$(EXTRACTIONMLI)) - -extraction.oug: - $(OUG) --dump-data $@ -rectypes $(MLINCLUDES) $(EXTRACTIONML) #$(EXTRACTIONMLI) - -extraction.useless: extraction.oug - $(OUG) --load-data $< --no-reduce --print-loc --useless-elements $@ - -# More to come ...
\ No newline at end of file diff --git a/dev/base_include b/dev/base_include index 0abcefc38e..242405ae29 100644 --- a/dev/base_include +++ b/dev/base_include @@ -17,7 +17,7 @@ #directory "grammar";; #directory "intf";; #directory "stm";; -#directory "ltac";; +#directory "vernac";; #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) #directory "+camlp5";; (* Gramext is found in top_printers.ml *) @@ -195,7 +195,7 @@ let qid = Libnames.qualid_of_string;; (* parsing of terms *) let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;; -let parse_tac = Pcoq.parse_string Pltac.tactic;; +let parse_tac = Pcoq.parse_string Ltac_plugin.Pltac.tactic;; let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;; (* build a term of type glob_constr without type-checking or resolution of diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 2a6601e045..412da626fd 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -2,5 +2,51 @@ set -xe +# Coq's tools need an ending slash :S, we should fix them. +export COQBIN=`pwd`/bin/ export PATH=`pwd`/bin:$PATH + ls `pwd`/bin + +# Maybe we should just use Ruby... +mathcomp_CI_BRANCH=master +mathcomp_CI_GITURL=https://github.com/math-comp/math-comp.git + +# git_checkout branch +git_checkout() +{ + local _BRANCH=${1} + local _URL=${2} + local _DEST=${3} + + echo "Checking out ${_DEST}" + git clone --depth 1 -b ${_BRANCH} ${_URL} ${_DEST} + ( cd ${3} && echo "${_DEST}: `git log -1 --format='%s | %H | %cd | %aN'`" ) +} + +checkout_mathcomp() +{ + git_checkout ${mathcomp_CI_BRANCH} ${mathcomp_CI_GITURL} ${1} +} + +# this installs just the ssreflect library of math-comp +install_ssreflect() +{ + echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r' + + checkout_mathcomp math-comp + ( cd math-comp/mathcomp && \ + sed -i.bak '/ssrtest/d' Make && \ + sed -i.bak '/odd_order/d' Make && \ + sed -i.bak '/all\/all.v/d' Make && \ + sed -i.bak '/character/d' Make && \ + sed -i.bak '/real_closed/d' Make && \ + sed -i.bak '/solvable/d' Make && \ + sed -i.bak '/field/d' Make && \ + sed -i.bak '/fingroup/d' Make && \ + sed -i.bak '/algebra/d' Make && \ + make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all && make install ) + + echo -en 'travis_fold:end:ssr.install\\r' + +} diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh index d4023c9165..ec09389f8e 100755 --- a/dev/ci/ci-compcert.sh +++ b/dev/ci/ci-compcert.sh @@ -3,8 +3,11 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh +CompCert_CI_BRANCH=master +CompCert_CI_GITURL=https://github.com/AbsInt/CompCert.git + opam install -j ${NJOBS} -y menhir -git clone --depth 3 -b coq-8.6 https://github.com/maximedenes/CompCert.git +git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} CompCert # Patch to avoid the upper version limit ( cd CompCert && sed -i.bak 's/8.6)/8.6|trunk)/' configure && ./configure x86_32-linux && make -j ${NJOBS} ) diff --git a/dev/ci/ci-coquelicot.sh b/dev/ci/ci-coquelicot.sh index 4a23e51be6..94bd5e468f 100755 --- a/dev/ci/ci-coquelicot.sh +++ b/dev/ci/ci-coquelicot.sh @@ -4,26 +4,9 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://github.com/math-comp/math-comp.git - -# coquelicot just needs mathcomp -( cd math-comp/mathcomp && \ - sed -i.bak '/ssrtest/d' Make && \ - sed -i.bak '/odd_order/d' Make && \ - sed -i.bak '/all\/all.v/d' Make && \ - sed -i.bak '/character/d' Make && \ - sed -i.bak '/real_closed/d' Make && \ - sed -i.bak '/solvable/d' Make && \ - sed -i.bak '/field/d' Make && \ - sed -i.bak '/fingroup/d' Make && \ - sed -i.bak '/algebra/d' Make && \ - make -j ${NJOBS} && make install ) - -# Setup ssr -# echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc -# echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc +install_ssreflect # Setup coquelicot -git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git +git_checkout master https://scm.gforge.inria.fr/anonscm/git/coquelicot/coquelicot.git coquelicot ( cd coquelicot && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat-crypto.sh index c594f83603..c669195ddd 100755 --- a/dev/ci/ci-fiat-crypto.sh +++ b/dev/ci/ci-fiat-crypto.sh @@ -4,9 +4,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://github.com/mit-plv/fiat-crypto.git +git_checkout master https://github.com/mit-plv/fiat-crypto.git fiat-crypto ( cd fiat-crypto && make -j ${NJOBS} ) - -# ( cd corn && make -j ${NJOBS} ) - diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh index b9cf649a1a..345924e40a 100755 --- a/dev/ci/ci-flocq.sh +++ b/dev/ci/ci-flocq.sh @@ -4,6 +4,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git +git_checkout master https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git flocq ( cd flocq && ./autogen.sh && ./configure && ./remake -j${NJOBS} ) diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh index 7b5811dc4a..ce870e52b5 100755 --- a/dev/ci/ci-geocoq.sh +++ b/dev/ci/ci-geocoq.sh @@ -7,6 +7,10 @@ source ${ci_dir}/ci-common.sh GeoCoq_CI_BRANCH=master GeoCoq_CI_GITURL=https://github.com/GeoCoq/GeoCoq.git -git clone --depth 1 -b ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} +git_checkout ${GeoCoq_CI_BRANCH} ${GeoCoq_CI_GITURL} GeoCoq -( cd GeoCoq && ./configure.sh && make -j ${NJOBS} ) +( cd GeoCoq && \ + ./configure.sh && \ + sed -i.bak '/Ch16_coordinates_with_functions\.v/d' Make && \ + coq_makefile -f Make -o Makefile && \ + make -j ${NJOBS} ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 8f82ba9f21..0c07564c02 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 -b mz-8.6 https://github.com/ejgallego/HoTT.git +git_checkout mz-8.7 https://github.com/ejgallego/HoTT.git HoTT ( cd HoTT && ./autogen.sh && ./configure && make -j ${NJOBS} ) diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index e97e2c19e3..c21af976f4 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -4,32 +4,14 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -# XXX: Refactor into install-ssreflect -git clone --depth 1 https://github.com/math-comp/math-comp.git - -# coquelicot just needs mathcomp -( cd math-comp/mathcomp && \ - sed -i.bak '/ssrtest/d' Make && \ - sed -i.bak '/odd_order/d' Make && \ - sed -i.bak '/all\/all.v/d' Make && \ - sed -i.bak '/character/d' Make && \ - sed -i.bak '/real_closed/d' Make && \ - sed -i.bak '/solvable/d' Make && \ - sed -i.bak '/field/d' Make && \ - sed -i.bak '/fingroup/d' Make && \ - sed -i.bak '/algebra/d' Make && \ - make -j ${NJOBS} && make install ) - -# Setup ssr = This doesn't work as coq_makefile will pass -q to coqc :S :S -# echo "Add ML Path \"`pwd`/math-comp/mathcomp/\"." > ${HOME}/.coqrc -# echo "Add LoadPath \"`pwd`/math-comp/mathcomp/\" as mathcomp." >> ${HOME}/.coqrc +install_ssreflect # Setup stdpp -git clone --depth 1 https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git +git_checkout master https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp.git coq-stdpp ( cd coq-stdpp && make -j ${NJOBS} && make install ) # Setup Iris -git clone --depth 1 https://gitlab.mpi-sws.org/FP/iris-coq.git +git_checkout master https://gitlab.mpi-sws.org/FP/iris-coq.git iris-coq ( cd iris-coq && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math-classes.sh index 9127c18951..4450dc0710 100755 --- a/dev/ci/ci-math-classes.sh +++ b/dev/ci/ci-math-classes.sh @@ -4,9 +4,9 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 1 -b v8.6 https://github.com/math-classes/math-classes.git +git_checkout v8.6 https://github.com/math-classes/math-classes.git math-classes ( cd math-classes && make -j ${NJOBS} && make install ) -git clone --depth 1 -b v8.6 https://github.com/c-corn/corn.git +git_checkout v8.6 https://github.com/c-corn/corn.git corn ( cd corn && make -j ${NJOBS} ) diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-math-comp.sh index b833792419..2eb150cb52 100755 --- a/dev/ci/ci-math-comp.sh +++ b/dev/ci/ci-math-comp.sh @@ -4,10 +4,10 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone --depth 3 https://github.com/math-comp/math-comp.git +checkout_mathcomp math-comp # odd_order takes too much time for travis. -( cd math-comp/mathcomp && \ - sed -i.bak '/PFsection/d' Make && \ - sed -i.bak '/stripped_odd_order_theorem/d' Make && \ - make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all ) +( cd math-comp/mathcomp && \ + sed -i.bak '/PFsection/d' Make && \ + sed -i.bak '/stripped_odd_order_theorem/d' Make && \ + make Makefile.coq && make -f Makefile.coq -j ${NJOBS} all ) diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh index 9a9bd3648b..91a33695b0 100755 --- a/dev/ci/ci-metacoq.sh +++ b/dev/ci/ci-metacoq.sh @@ -6,11 +6,11 @@ source ${ci_dir}/ci-common.sh # MetaCoq + UniCoq -git clone --depth 1 https://github.com/unicoq/unicoq.git +git_checkout master https://github.com/unicoq/unicoq.git unicoq ( cd unicoq && coq_makefile -f Make -o Makefile && make -j ${NJOBS} && make install ) -git clone --depth 1 https://github.com/MetaCoq/MetaCoq.git +git_checkout master https://github.com/MetaCoq/MetaCoq.git MetaCoq ( cd MetaCoq && coq_makefile -f _CoqProject -o Makefile && make -j ${NJOBS} ) diff --git a/dev/ci/ci-tlc.sh b/dev/ci/ci-tlc.sh index 2161a11461..b946324924 100755 --- a/dev/ci/ci-tlc.sh +++ b/dev/ci/ci-tlc.sh @@ -3,6 +3,6 @@ ci_dir="$(dirname "$0")" source ${ci_dir}/ci-common.sh -git clone https://gforge.inria.fr/git/tlc/tlc.git +git_checkout master https://gforge.inria.fr/git/tlc/tlc.git tlc ( cd tlc && make -j ${NJOBS} ) diff --git a/dev/ci/ci-unimath.sh b/dev/ci/ci-unimath.sh new file mode 100755 index 0000000000..15e619acbb --- /dev/null +++ b/dev/ci/ci-unimath.sh @@ -0,0 +1,15 @@ +#!/bin/bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +UniMath_CI_BRANCH=master +UniMath_CI_GITURL=https://github.com/UniMath/UniMath.git + +git_checkout ${UniMath_CI_BRANCH} ${UniMath_CI_GITURL} UniMath + +( cd UniMath && \ + sed -i.bak '/Folds/d' Makefile && \ + sed -i.bak '/HomologicalAlgebra/d' Makefile && \ + make -j ${NJOBS} BUILD_COQ=no ) + diff --git a/dev/core.dbg b/dev/core.dbg index 38b9b29463..698db63d23 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -12,6 +12,7 @@ load_printer proofs.cma load_printer parsing.cma load_printer printing.cma load_printer tactics.cma +load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma load_printer highparsing.cma diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index f54f3fcc8e..8d2d055908 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -40,6 +40,24 @@ important things: - Some printing functions were moved from Pptactic to Pputils - A part of Tacexpr has been moved to Tactypes +The folder itself has been turned into a plugin. This does not change much, +but because it is a packed plugin, it may wreak havoc for third-party plugins +depending on any module defined in the ltac/ directory. Namely, even if +everything looks OK at compile time, a plugin can fail to load at link time +because it mistakenly looks for a module Foo instead of Ltac_plugin.Foo, with +an error of the form: + +Error: while loading myplugin.cmxs, no implementation available for Foo. + +In particular, most EXTEND macros will trigger this problem even if they +seemingly do not use any Ltac module, as their expansion do. + +The solution is simple, and consists in adding a statement "open Ltac_plugin" +in each file using a Ltac module, before such a module is actually called. An +alternative solution would be to fully qualify Ltac modules, e.g. turning any +call to Tacinterp into Ltac_plugin.Tacinterp. Note that this solution does not +work for EXTEND macros though. + ** Error handling ** - All error functions now take an optional parameter `?loc:Loc.t`. For diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 46caca8d6f..3850c05fd9 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -20,7 +20,7 @@ exec $OCAMLDEBUG \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar \ -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ -I $COQTOP/library -I $COQTOP/engine \ - -I $COQTOP/pretyping -I $COQTOP/parsing \ + -I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \ -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \ -I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \ -I $COQTOP/plugins/cc -I $COQTOP/plugins/dp \ @@ -32,6 +32,6 @@ exec $OCAMLDEBUG \ -I $COQTOP/plugins/ring -I $COQTOP/plugins/romega \ -I $COQTOP/plugins/rtauto -I $COQTOP/plugins/setoid_ring \ -I $COQTOP/plugins/subtac -I $COQTOP/plugins/syntax \ - -I $COQTOP/plugins/xml \ + -I $COQTOP/plugins/xml -I $COQTOP/plugins/ltac \ -I $COQTOP/ide \ "$@" diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 4fcad88202..dc354b130b 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -234,7 +234,7 @@ let ppenvwithcst e = pp 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 pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x)) let ppobj obj = Format.print_string (Libobject.object_tag obj) diff --git a/engine/proofview.ml b/engine/proofview.ml index 2fbabb7492..721389af4f 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -453,6 +453,25 @@ let iter_goal i = Solution.get >>= fun evd -> Comb.set CList.(undefined evd (flatten (rev subgoals))) +(** List iter but allocates a list of results *) +let map_goal i = + let rev = List.rev in (* hem... Proof masks List... *) + let open Proof in + Comb.get >>= fun initial -> + Proof.List.fold_left begin fun (acc, subgoals as cur) goal -> + Solution.get >>= fun step -> + match Evarutil.advance step goal with + | None -> return cur + | Some goal -> + Comb.set [goal] >> + i goal >>= fun res -> + Proof.map (fun comb -> comb :: subgoals) Comb.get >>= fun x -> + return (res :: acc, x) + end ([],[]) initial >>= fun (results_rev, subgoals) -> + Solution.get >>= fun evd -> + Comb.set CList.(undefined evd (flatten (rev subgoals))) >> + return (rev results_rev) + (** A variant of [Monad.List.fold_left2] where the first list is the list of focused goals. The argument tactic is executed in a focus comprising only of the current goal, a goal which has been solved @@ -585,7 +604,15 @@ let tclINDEPENDENT tac = let tac = InfoL.tag (Info.DBranch) tac in InfoL.tag (Info.Dispatch) (iter_goal (fun _ -> tac)) - +let tclINDEPENDENTL tac = + let open Proof in + Pv.get >>= fun initial -> + match initial.comb with + | [] -> tclUNIT [] + | [_] -> tac >>= fun x -> return [x] + | _ -> + let tac = InfoL.tag (Info.DBranch) tac in + InfoL.tag (Info.Dispatch) (map_goal (fun _ -> tac)) (** {7 Goal manipulation} *) diff --git a/engine/proofview.mli b/engine/proofview.mli index 90be2f90ab..294b03dca2 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -292,6 +292,7 @@ val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tact independent of backtracking in another. It is equivalent to [tclEXTEND [] tac []]. *) val tclINDEPENDENT : unit tactic -> unit tactic +val tclINDEPENDENTL: 'a tactic -> 'a list tactic (** {7 Goal manipulation} *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c102d8e117..3ed8733df5 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1591,7 +1591,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = let idl_tmp = Array.map (fun ((loc,id),bl,ty,_) -> let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in - let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> assert false) rbl in + let rbl = List.map (function BDRawDef a -> a | BDPattern _ -> + Loc.raise ~loc (Stream.Error "pattern with quote not allowed after cofix")) rbl in (List.rev rbl, intern_type env' ty,env')) dl in let idl = Array.map2 (fun (_,_,_,bd) (b,c,env') -> diff --git a/interp/notation.ml b/interp/notation.ml index 948d624a27..66d3c91859 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -927,19 +927,19 @@ let locate_notation prglob ntn scope = match ntns with | [] -> str "Unknown notation" | _ -> - t (str "Notation " ++ - tab () ++ str "Scope " ++ tab () ++ fnl () ++ + str "Notation" ++ fnl () ++ prlist (fun (ntn,l) -> let scope = find_default ntn scopes in prlist (fun (sc,r,(_,df)) -> hov 0 ( - pr_notation_info prglob df r ++ tbrk (1,2) ++ - (if String.equal sc default_scope then mt () else (str ": " ++ str sc)) ++ - tbrk (1,2) ++ - (if Option.equal String.equal (Some sc) scope then str "(default interpretation)" else mt ()) + pr_notation_info prglob df r ++ + (if String.equal sc default_scope then mt () + else (spc () ++ str ": " ++ str sc)) ++ + (if Option.equal String.equal (Some sc) scope + then spc () ++ str "(default interpretation)" else mt ()) ++ fnl ())) - l) ntns) + l) ntns let collect_notation_in_scope scope sc known = assert (not (String.equal scope default_scope)); diff --git a/interp/ppextend.ml b/interp/ppextend.ml index 37bbe0ce87..87ca253253 100644 --- a/interp/ppextend.ml +++ b/interp/ppextend.ml @@ -23,12 +23,9 @@ type ppbox = | PpHOVB of int | PpHVB of int | PpVB of int - | PpTB type ppcut = | PpBrk of int * int - | PpTbrk of int * int - | PpTab | PpFnl let ppcmd_of_box = function @@ -36,13 +33,10 @@ let ppcmd_of_box = function | PpHOVB n -> hov n | PpHVB n -> hv n | PpVB n -> v n - | PpTB -> t let ppcmd_of_cut = function - | PpTab -> tab () | PpFnl -> fnl () | PpBrk(n1,n2) -> brk(n1,n2) - | PpTbrk(n1,n2) -> tbrk(n1,n2) type unparsing = | UnpMetaVar of int * parenRelation diff --git a/interp/ppextend.mli b/interp/ppextend.mli index de7a42eee5..09dc369437 100644 --- a/interp/ppextend.mli +++ b/interp/ppextend.mli @@ -23,12 +23,9 @@ type ppbox = | PpHOVB of int | PpHVB of int | PpVB of int - | PpTB type ppcut = | PpBrk of int * int - | PpTbrk of int * int - | PpTab | PpFnl val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 407cec0842..fd57b70ca9 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -60,6 +60,9 @@ let rec cases_pattern_fold_names f a = function | CPatPrim _ | CPatAtom _ -> a | CPatCast _ -> assert false +let ids_of_pattern = + cases_pattern_fold_names Id.Set.add Id.Set.empty + let ids_of_pattern_list = List.fold_left (Loc.located_fold_left @@ -173,7 +176,8 @@ let split_at_annot bl na = (List.rev ans, LocalRawAssum (r, k, t) :: rest) end | LocalRawDef _ as x :: rest -> aux (x :: acc) rest - | LocalPattern _ :: rest -> assert false + | LocalPattern (loc,_,_) :: rest -> + Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix") | [] -> user_err ~loc (str "No parameter named " ++ Nameops.pr_id id ++ str".") @@ -196,8 +200,9 @@ let map_local_binders f g e bl = (map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl) | LocalRawDef((loc,na),ty) -> (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) - | LocalPattern _ -> - assert false in + | LocalPattern (loc,pat,t) -> + let ids = ids_of_pattern pat in + (Id.Set.fold g ids e, LocalPattern (loc,pat,Option.map (f e) t)::bl) in let (e,rbl) = List.fold_left h (e,[]) bl in (e, List.rev rbl) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 810c346990..94ca4c72dd 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -299,7 +299,7 @@ and pp_bytecodes c = | Ksequence (l1, l2) :: c -> pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c | i :: c -> - tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c + pp_instr i ++ fnl () ++ pp_bytecodes c (*spiwack: moved this type in this file because I needed it for retroknowledge which can't depend from cbytegen *) diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml deleted file mode 100644 index dce4e93076..0000000000 --- a/kernel/fast_typeops.ml +++ /dev/null @@ -1,464 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open CErrors -open Util -open Names -open Univ -open Term -open Vars -open Declarations -open Environ -open Reduction -open Inductive -open Type_errors - -module RelDecl = Context.Rel.Declaration -module NamedDecl = Context.Named.Declaration - -let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y - -let conv_leq_vecti env v1 v2 = - Array.fold_left2_i - (fun i _ t1 t2 -> - try conv_leq false env t1 t2 - with NotConvertible -> raise (NotConvertibleVect i)) - () - v1 - v2 - -let check_constraints cst env = - if Environ.check_constraints cst env then () - else error_unsatisfied_constraints env cst - -(* This should be a type (a priori without intention to be an assumption) *) -let type_judgment env c t = - match kind_of_term(whd_all env t) with - | Sort s -> {utj_val = c; utj_type = s } - | _ -> error_not_type env (make_judge c t) - -let check_type env c t = - match kind_of_term(whd_all env t) with - | Sort s -> s - | _ -> error_not_type env (make_judge c t) - -(* This should be a type intended to be assumed. The error message is *) -(* not as useful as for [type_judgment]. *) -let assumption_of_judgment env t ty = - try let _ = check_type env t ty in t - with TypeError _ -> - error_assumption env (make_judge t ty) - -(************************************************) -(* Incremental typing rules: builds a typing judgment given the *) -(* judgments for the subterms. *) - -(*s Type of sorts *) - -(* Prop and Set *) - -let judge_of_prop = mkSort type1_sort - -let judge_of_prop_contents _ = judge_of_prop - -(* Type of Type(i). *) - -let judge_of_type u = - let uu = Universe.super u in - mkType uu - -(*s Type of a de Bruijn index. *) - -let judge_of_relative env n = - try - env |> lookup_rel n |> RelDecl.get_type |> lift n - with Not_found -> - error_unbound_rel env n - -(* Type of variables *) -let judge_of_variable env id = - try named_type id env - with Not_found -> - error_unbound_var env id - -(* Management of context of variables. *) - -(* Checks if a context of variables can be instantiated by the - variables of the current env *) -(* TODO: check order? *) -let check_hyps_inclusion env f c sign = - Context.Named.fold_outside - (fun decl () -> - let id = NamedDecl.get_id decl in - let ty1 = NamedDecl.get_type decl in - try - let ty2 = named_type id env in - if not (eq_constr ty2 ty1) then raise Exit - with Not_found | Exit -> - error_reference_variables env id (f c)) - sign - ~init:() - -(* Instantiation of terms on real arguments. *) - -(* Make a type polymorphic if an arity *) - -(* Type of constants *) - - -let type_of_constant_knowing_parameters_arity env t paramtyps = - match t with - | RegularArity t -> t - | TemplateArity (sign,ar) -> - let ctx = List.rev sign in - let ctx,s = instantiate_universes env ctx ar paramtyps in - mkArity (List.rev ctx,s) - -let type_of_constant_knowing_parameters env cst paramtyps = - let ty, cu = constant_type env cst in - type_of_constant_knowing_parameters_arity env ty paramtyps, cu - -let judge_of_constant_knowing_parameters env (kn,u as cst) args = - let cb = lookup_constant kn env in - let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in - let ty, cu = type_of_constant_knowing_parameters env cst args in - let () = check_constraints cu env in - ty - -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] - -(* Type of a lambda-abstraction. *) - -(* [judge_of_abstraction env name var j] implements the rule - - env, name:typ |- j.uj_val:j.uj_type env, |- (name:typ)j.uj_type : s - ----------------------------------------------------------------------- - env |- [name:typ]j.uj_val : (name:typ)j.uj_type - - Since all products are defined in the Calculus of Inductive Constructions - and no upper constraint exists on the sort $s$, we don't need to compute $s$ -*) - -let judge_of_abstraction env name var ty = - mkProd (name, var, ty) - -(* Type of an application. *) - -let make_judgev c t = - Array.map2 make_judge c t - -let judge_of_apply env func funt argsv argstv = - let len = Array.length argsv in - let rec apply_rec i typ = - if Int.equal i len then typ - else - (match kind_of_term (whd_all env typ) with - | Prod (_,c1,c2) -> - let arg = argsv.(i) and argt = argstv.(i) in - (try - let () = conv_leq false env argt c1 in - apply_rec (i+1) (subst1 arg c2) - with NotConvertible -> - error_cant_apply_bad_type env - (i+1,c1,argt) - (make_judge func funt) - (make_judgev argsv argstv)) - - | _ -> - error_cant_apply_not_functional env - (make_judge func funt) - (make_judgev argsv argstv)) - in apply_rec 0 funt - -(* Type of product *) - -let sort_of_product env domsort rangsort = - match (domsort, rangsort) with - (* Product rule (s,Prop,Prop) *) - | (_, Prop Null) -> rangsort - (* Product rule (Prop/Set,Set,Set) *) - | (Prop _, Prop Pos) -> rangsort - (* Product rule (Type,Set,?) *) - | (Type u1, Prop Pos) -> - if is_impredicative_set env then - (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) - rangsort - else - (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) - Type (Universe.sup Universe.type0 u1) - (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2) - (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Null, Type _) -> rangsort - (* Product rule (Type_i,Type_i,Type_i) *) - | (Type u1, Type u2) -> Type (Universe.sup u1 u2) - -(* [judge_of_product env name (typ1,s1) (typ2,s2)] implements the rule - - env |- typ1:s1 env, name:typ1 |- typ2 : s2 - ------------------------------------------------------------------------- - s' >= (s1,s2), env |- (name:typ)j.uj_val : s' - - where j.uj_type is convertible to a sort s2 -*) -let judge_of_product env name s1 s2 = - let s = sort_of_product env s1 s2 in - mkSort s - -(* Type of a type cast *) - -(* [judge_of_cast env (c,typ1) (typ2,s)] implements the rule - - env |- c:typ1 env |- typ2:s env |- typ1 <= typ2 - --------------------------------------------------------------------- - env |- c:typ2 -*) - -let judge_of_cast env c ct k expected_type = - try - match k with - | VMcast -> - vm_conv CUMUL env ct expected_type - | DEFAULTcast -> - default_conv ~l2r:false CUMUL env ct expected_type - | REVERTcast -> - default_conv ~l2r:true CUMUL env ct expected_type - | NATIVEcast -> - let sigma = Nativelambda.empty_evars in - Nativeconv.native_conv CUMUL sigma env ct expected_type - with NotConvertible -> - error_actual_type env (make_judge c ct) expected_type - -(* Inductive types. *) - -(* The type is parametric over the uniform parameters whose conclusion - is in Type; to enforce the internal constraints between the - parameters and the instances of Type occurring in the type of the - constructors, we use the level variables _statically_ assigned to - the conclusions of the parameters as mediators: e.g. if a parameter - has conclusion Type(alpha), static constraints of the form alpha<=v - exist between alpha and the Type's occurring in the constructor - types; when the parameters is finally instantiated by a term of - conclusion Type(u), then the constraints u<=alpha is computed in - the App case of execute; from this constraints, the expected - dynamic constraints of the form u<=v are enforced *) - -let judge_of_inductive_knowing_parameters env (ind,u as indu) args = - let (mib,mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters - env (spec,u) args - in - check_constraints cst env; - t - -let judge_of_inductive env (ind,u as indu) = - let (mib,mip) = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in - check_constraints cst env; - t - -(* Constructors. *) - -let judge_of_constructor env (c,u as cu) = - let _ = - let ((kn,_),_) = c in - let mib = lookup_mind kn env in - check_hyps_inclusion env mkConstructU cu mib.mind_hyps in - let specif = lookup_mind_specif env (inductive_of_constructor c) in - let t,cst = constrained_type_of_constructor cu specif in - let () = check_constraints cst env in - t - -(* Case. *) - -let check_branch_types env (ind,u) c ct lft explft = - try conv_leq_vecti env lft explft - with - NotConvertibleVect i -> - error_ill_formed_branch env c ((ind,i+1),u) lft.(i) explft.(i) - | Invalid_argument _ -> - error_number_branches env (make_judge c ct) (Array.length explft) - -let judge_of_case env ci p pt c ct lf lft = - let (pind, _ as indspec) = - try find_rectype env ct - with Not_found -> error_case_not_inductive env (make_judge c ct) in - let _ = check_case_info env pind ci in - let (bty,rslty) = - type_case_branches env indspec (make_judge p pt) c in - let () = check_branch_types env pind c ct lft bty in - rslty - -let judge_of_projection env p c ct = - let pb = lookup_projection p env in - let (ind,u), args = - try find_rectype env ct - with Not_found -> error_case_not_inductive env (make_judge c ct) - in - assert(eq_mind pb.proj_ind (fst ind)); - let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in - substl (c :: List.rev args) ty - - -(* Fixpoints. *) - -(* Checks the type of a general (co)fixpoint, i.e. without checking *) -(* the specific guard condition. *) - -let type_fixpoint env lna lar vdef vdeft = - let lt = Array.length vdeft in - assert (Int.equal (Array.length lar) lt); - try - conv_leq_vecti env vdeft (Array.map (fun ty -> lift lt ty) lar) - with NotConvertibleVect i -> - error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar - -(************************************************************************) -(************************************************************************) - -(* The typing machine. *) - (* ATTENTION : faudra faire le typage du contexte des Const, - Ind et Constructsi un jour cela devient des constructions - arbitraires et non plus des variables *) -let rec execute env cstr = - let open Context.Rel.Declaration in - match kind_of_term cstr with - (* Atomic terms *) - | Sort (Prop c) -> - judge_of_prop_contents c - - | Sort (Type u) -> - judge_of_type u - - | Rel n -> - judge_of_relative env n - - | Var id -> - judge_of_variable env id - - | Const c -> - judge_of_constant env c - - | Proj (p, c) -> - let ct = execute env c in - judge_of_projection env p c ct - - (* Lambda calculus operators *) - | App (f,args) -> - let argst = execute_array env args in - let ft = - match kind_of_term f with - | Ind ind when Environ.template_polymorphic_pind ind env -> - (* Template sort-polymorphism of inductive types *) - let args = Array.map (fun t -> lazy t) argst in - judge_of_inductive_knowing_parameters env ind args - | Const cst when Environ.template_polymorphic_pconstant cst env -> - (* Template sort-polymorphism of constants *) - let args = Array.map (fun t -> lazy t) argst in - judge_of_constant_knowing_parameters env cst args - | _ -> - (* Full or no sort-polymorphism *) - execute env f - in - - judge_of_apply env f ft args argst - - | Lambda (name,c1,c2) -> - let _ = execute_is_type env c1 in - let env1 = push_rel (LocalAssum (name,c1)) env in - let c2t = execute env1 c2 in - judge_of_abstraction env name c1 c2t - - | Prod (name,c1,c2) -> - let vars = execute_is_type env c1 in - let env1 = push_rel (LocalAssum (name,c1)) env in - let vars' = execute_is_type env1 c2 in - judge_of_product env name vars vars' - - | LetIn (name,c1,c2,c3) -> - let c1t = execute env c1 in - let _c2s = execute_is_type env c2 in - let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in - let env1 = push_rel (LocalDef (name,c1,c2)) env in - let c3t = execute env1 c3 in - subst1 c1 c3t - - | Cast (c,k,t) -> - let ct = execute env c in - let _ts = execute_type env t in - let _ = judge_of_cast env c ct k t in - t - - (* Inductive types *) - | Ind ind -> - judge_of_inductive env ind - - | Construct c -> - judge_of_constructor env c - - | Case (ci,p,c,lf) -> - let ct = execute env c in - let pt = execute env p in - let lft = execute_array env lf in - judge_of_case env ci p pt c ct lf lft - - | Fix ((vn,i as vni),recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in - let fix = (vni,recdef') in - check_fix env fix; fix_ty - - | CoFix (i,recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in - let cofix = (i,recdef') in - check_cofix env cofix; fix_ty - - (* Partial proofs: unsupported by the kernel *) - | Meta _ -> - anomaly (Pp.str "the kernel does not support metavariables") - - | Evar _ -> - anomaly (Pp.str "the kernel does not support existential variables") - -and execute_is_type env constr = - let t = execute env constr in - check_type env constr t - -and execute_type env constr = - let t = execute env constr in - type_judgment env constr t - -and execute_recdef env (names,lar,vdef) i = - let lart = execute_array env lar in - let lara = Array.map2 (assumption_of_judgment env) lar lart in - let env1 = push_rec_types (names,lara,vdef) env in - let vdeft = execute_array env1 vdef in - let () = type_fixpoint env1 names lara vdef vdeft in - (lara.(i),(names,lara,vdef)) - -and execute_array env = Array.map (execute env) - -(* Derived functions *) -let infer env constr = - let t = execute env constr in - make_judge constr t - -let infer = - if Flags.profile then - let infer_key = Profile.declare_profile "Fast_infer" in - Profile.profile2 infer_key (fun b c -> infer b c) - else (fun b c -> infer b c) - -let infer_type env constr = - execute_type env constr - -let infer_v env cv = - let jv = execute_array env cv in - make_judgev cv jv diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli deleted file mode 100644 index 41cff607e7..0000000000 --- a/kernel/fast_typeops.mli +++ /dev/null @@ -1,24 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Term -open Environ -open Declarations - -(** {6 Typing functions (not yet tagged as safe) } - - They return unsafe judgments that are "in context" of a set of - (local) universe variables (the ones that appear in the term) - and associated constraints. In case of polymorphic definitions, - these variables and constraints will be generalized. - *) - - -val infer : env -> constr -> unsafe_judgment -val infer_v : env -> constr array -> unsafe_judgment array -val infer_type : env -> types -> unsafe_type_judgment diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 15f213ce9c..4c540a6d73 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -32,7 +32,6 @@ Type_errors Modops Inductive Typeops -Fast_typeops Indtypes Cooking Term_typing diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index d8774944e4..3a0d1a2a5e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -20,7 +20,6 @@ open Declarations open Environ open Entries open Typeops -open Fast_typeops module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 24018ab31a..7d9a2aac09 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -14,11 +14,9 @@ open Term open Vars open Declarations open Environ -open Entries open Reduction open Inductive open Type_errors -open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -38,61 +36,46 @@ let check_constraints cst env = if Environ.check_constraints cst env then () else error_unsatisfied_constraints env cst -(* This should be a type (a priori without intension to be an assumption) *) -let type_judgment env j = - match kind_of_term(whd_all env j.uj_type) with - | Sort s -> {utj_val = j.uj_val; utj_type = s } - | _ -> error_not_type env j +(* This should be a type (a priori without intention to be an assumption) *) +let check_type env c t = + match kind_of_term(whd_all env t) with + | Sort s -> s + | _ -> error_not_type env (make_judge c t) -(* This should be a type intended to be assumed. The error message is *) -(* not as useful as for [type_judgment]. *) -let assumption_of_judgment env j = - try (type_judgment env j).utj_val +(* This should be a type intended to be assumed. The error message is + not as useful as for [type_judgment]. *) +let check_assumption env t ty = + try let _ = check_type env t ty in t with TypeError _ -> - error_assumption env j + error_assumption env (make_judge t ty) (************************************************) -(* Incremental typing rules: builds a typing judgement given the *) -(* judgements for the subterms. *) +(* Incremental typing rules: builds a typing judgment given the *) +(* judgments for the subterms. *) (*s Type of sorts *) (* Prop and Set *) -let judge_of_prop = - { uj_val = mkProp; - uj_type = mkSort type1_sort } - -let judge_of_set = - { uj_val = mkSet; - uj_type = mkSort type1_sort } - -let judge_of_prop_contents = function - | Null -> judge_of_prop - | Pos -> judge_of_set +let type1 = mkSort type1_sort (* Type of Type(i). *) -let judge_of_type u = +let type_of_type u = let uu = Universe.super u in - { uj_val = mkType u; - uj_type = mkType uu } + mkType uu (*s Type of a de Bruijn index. *) -let judge_of_relative env n = +let type_of_relative env n = try - let typ = RelDecl.get_type (lookup_rel n env) in - { uj_val = mkRel n; - uj_type = lift n typ } + env |> lookup_rel n |> RelDecl.get_type |> lift n with Not_found -> error_unbound_rel env n (* Type of variables *) -let judge_of_variable env id = - try - let ty = named_type id env in - make_judge (mkVar id) ty +let type_of_variable env id = + try named_type id env with Not_found -> error_unbound_var env id @@ -101,7 +84,7 @@ let judge_of_variable env id = (* Checks if a context of variables can be instantiated by the variables of the current env. Order does not have to be checked assuming that all names are distinct *) -let check_hyps_inclusion env c sign = +let check_hyps_inclusion env f c sign = Context.Named.fold_outside (fun d1 () -> let open Context.Named.Declaration in @@ -117,7 +100,7 @@ let check_hyps_inclusion env c sign = | LocalDef _, LocalAssum _ -> raise NotConvertible | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1); with Not_found | NotConvertible | Option.Heterogeneous -> - error_reference_variables env id c) + error_reference_variables env id (f c)) sign ~init:() @@ -125,35 +108,9 @@ let check_hyps_inclusion env c sign = (* Make a type polymorphic if an arity *) -let extract_level env p = - let _,c = dest_prod_assum env p in - match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None - -let extract_context_levels env l = - let fold l = function - | LocalAssum (_,p) -> extract_level env p :: l - | LocalDef _ -> l - in - List.fold_left fold [] l - -let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = - let params, ccl = dest_prod_assum env t in - match kind_of_term ccl with - | Sort (Type u) -> - let ind, l = decompose_app (whd_all env c) in - if isInd ind && List.is_empty l then - let mis = lookup_mind_specif env (fst (destInd ind)) in - let nparams = Inductive.inductive_params mis in - let paramsl = CList.lastn nparams params in - let param_ccls = extract_context_levels env paramsl in - let s = { template_param_levels = param_ccls; template_level = u} in - TemplateArity (params,s) - else RegularArity t - | _ -> - RegularArity t - (* Type of constants *) + let type_of_constant_type_knowing_parameters env t paramtyps = match t with | RegularArity t -> t @@ -162,49 +119,28 @@ let type_of_constant_type_knowing_parameters env t paramtyps = let ctx,s = instantiate_universes env ctx ar paramtyps in mkArity (List.rev ctx,s) -let type_of_constant_knowing_parameters env cst paramtyps = - let cb = lookup_constant (fst cst) env in - let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in +let type_of_constant_knowing_parameters env (kn,u as cst) args = + let cb = lookup_constant kn env in + let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty, cu = constant_type env cst in - type_of_constant_type_knowing_parameters env ty paramtyps, cu + let ty = type_of_constant_type_knowing_parameters env ty args in + let () = check_constraints cu env in + ty -let type_of_constant_knowing_parameters_in env cst paramtyps = - let cb = lookup_constant (fst cst) env in - let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in +let type_of_constant_knowing_parameters_in env (kn,u as cst) args = + let cb = lookup_constant kn env in + let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty = constant_type_in env cst in - type_of_constant_type_knowing_parameters env ty paramtyps - -let type_of_constant_type env t = - type_of_constant_type_knowing_parameters env t [||] + type_of_constant_type_knowing_parameters env ty args let type_of_constant env cst = type_of_constant_knowing_parameters env cst [||] let type_of_constant_in env cst = - let cb = lookup_constant (fst cst) env in - let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in - let ar = constant_type_in env cst in - type_of_constant_type_knowing_parameters env ar [||] - -let judge_of_constant_knowing_parameters env (kn,u as cst) args = - let c = mkConstU cst in - let ty, cu = type_of_constant_knowing_parameters env cst args in - let () = check_constraints cu env in - make_judge c ty - -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] - -let type_of_projection env (p,u) = - let cst = Projection.constant p in - let cb = lookup_constant cst env in - match cb.const_proj with - | Some pb -> - if cb.const_polymorphic then - Vars.subst_instance_constr u pb.proj_type - else pb.proj_type - | None -> raise (Invalid_argument "type_of_projection: not a projection") + type_of_constant_knowing_parameters_in env cst [||] +let type_of_constant_type env t = + type_of_constant_type_knowing_parameters env t [||] (* Type of a lambda-abstraction. *) @@ -218,40 +154,36 @@ let type_of_projection env (p,u) = and no upper constraint exists on the sort $s$, we don't need to compute $s$ *) -let judge_of_abstraction env name var j = - { uj_val = mkLambda (name, var.utj_val, j.uj_val); - uj_type = mkProd (name, var.utj_val, j.uj_type) } - -(* Type of let-in. *) - -let judge_of_letin env name defj typj j = - { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ; - uj_type = subst1 defj.uj_val j.uj_type } +let type_of_abstraction env name var ty = + mkProd (name, var, ty) (* Type of an application. *) -let judge_of_apply env funj argjv = - let rec apply_rec n typ = function - | [] -> - { uj_val = mkApp (j_val funj, Array.map j_val argjv); - uj_type = typ } - | hj::restjl -> - (match kind_of_term (whd_all env typ) with - | Prod (_,c1,c2) -> - (try - let () = conv_leq false env hj.uj_type c1 in - apply_rec (n+1) (subst1 hj.uj_val c2) restjl - with NotConvertible -> - error_cant_apply_bad_type env - (n,c1, hj.uj_type) - funj argjv) - - | _ -> - error_cant_apply_not_functional env funj argjv) - in - apply_rec 1 - funj.uj_type - (Array.to_list argjv) +let make_judgev c t = + Array.map2 make_judge c t + +let type_of_apply env func funt argsv argstv = + let len = Array.length argsv in + let rec apply_rec i typ = + if Int.equal i len then typ + else + (match kind_of_term (whd_all env typ) with + | Prod (_,c1,c2) -> + let arg = argsv.(i) and argt = argstv.(i) in + (try + let () = conv_leq false env argt c1 in + apply_rec (i+1) (subst1 arg c2) + with NotConvertible -> + error_cant_apply_bad_type env + (i+1,c1,argt) + (make_judge func funt) + (make_judgev argsv argstv)) + + | _ -> + error_cant_apply_not_functional env + (make_judge func funt) + (make_judgev argsv argstv)) + in apply_rec 0 funt (* Type of product *) @@ -284,10 +216,9 @@ let sort_of_product env domsort rangsort = where j.uj_type is convertible to a sort s2 *) -let judge_of_product env name t1 t2 = - let s = sort_of_product env t1.utj_type t2.utj_type in - { uj_val = mkProd (name, t1.utj_val, t2.utj_val); - uj_type = mkSort s } +let type_of_product env name s1 s2 = + let s = sort_of_product env s1 s2 in + mkSort s (* Type of a type cast *) @@ -298,29 +229,20 @@ let judge_of_product env name t1 t2 = env |- c:typ2 *) -let judge_of_cast env cj k tj = - let expected_type = tj.utj_val in +let check_cast env c ct k expected_type = try - let c, cst = - match k with - | VMcast -> - mkCast (cj.uj_val, k, expected_type), - Reduction.vm_conv CUMUL env cj.uj_type expected_type - | DEFAULTcast -> - mkCast (cj.uj_val, k, expected_type), - default_conv ~l2r:false CUMUL env cj.uj_type expected_type - | REVERTcast -> - cj.uj_val, - default_conv ~l2r:true CUMUL env cj.uj_type expected_type - | NATIVEcast -> - let sigma = Nativelambda.empty_evars in - mkCast (cj.uj_val, k, expected_type), - Nativeconv.native_conv CUMUL sigma env cj.uj_type expected_type - in - { uj_val = c; - uj_type = expected_type } + match k with + | VMcast -> + vm_conv CUMUL env ct expected_type + | DEFAULTcast -> + default_conv ~l2r:false CUMUL env ct expected_type + | REVERTcast -> + default_conv ~l2r:true CUMUL env ct expected_type + | NATIVEcast -> + let sigma = Nativelambda.empty_evars in + Nativeconv.native_conv CUMUL sigma env ct expected_type with NotConvertible -> - error_actual_type env cj expected_type + error_actual_type env (make_judge c ct) expected_type (* Inductive types. *) @@ -336,83 +258,78 @@ let judge_of_cast env cj k tj = the App case of execute; from this constraints, the expected dynamic constraints of the form u<=v are enforced *) -let judge_of_inductive_knowing_parameters env (ind,u as indu) args = - let c = mkIndU indu in +let type_of_inductive_knowing_parameters env (ind,u as indu) args = let (mib,mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env c mib.mind_hyps; + check_hyps_inclusion env mkIndU indu mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters env (spec,u) args in - check_constraints cst env; - make_judge c t + check_constraints cst env; + t -let judge_of_inductive env (ind,u as indu) = - let c = mkIndU indu in - let (mib,mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env c mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive env (spec,u) in - check_constraints cst env; - (make_judge c t) +let type_of_inductive env (ind,u as indu) = + let (mib,mip) = lookup_mind_specif env ind in + check_hyps_inclusion env mkIndU indu mib.mind_hyps; + let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in + check_constraints cst env; + t (* Constructors. *) -let judge_of_constructor env (c,u as cu) = - let constr = mkConstructU cu in - let _ = +let type_of_constructor env (c,u as cu) = + let () = let ((kn,_),_) = c in let mib = lookup_mind kn env in - check_hyps_inclusion env constr mib.mind_hyps in + check_hyps_inclusion env mkConstructU cu mib.mind_hyps + in let specif = lookup_mind_specif env (inductive_of_constructor c) in let t,cst = constrained_type_of_constructor cu specif in let () = check_constraints cst env in - (make_judge constr t) + t (* Case. *) -let check_branch_types env (ind,u) cj (lfj,explft) = - try conv_leq_vecti env (Array.map j_type lfj) explft +let check_branch_types env (ind,u) c ct lft explft = + try conv_leq_vecti env lft explft with NotConvertibleVect i -> - error_ill_formed_branch env cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i) + error_ill_formed_branch env c ((ind,i+1),u) lft.(i) explft.(i) | Invalid_argument _ -> - error_number_branches env cj (Array.length explft) + error_number_branches env (make_judge c ct) (Array.length explft) -let judge_of_case env ci pj cj lfj = +let type_of_case env ci p pt c ct lf lft = let (pind, _ as indspec) = - try find_rectype env cj.uj_type - with Not_found -> error_case_not_inductive env cj in + try find_rectype env ct + with Not_found -> error_case_not_inductive env (make_judge c ct) in let () = check_case_info env pind ci in let (bty,rslty) = - type_case_branches env indspec pj cj.uj_val in - let () = check_branch_types env pind cj (lfj,bty) in - ({ uj_val = mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, - Array.map j_val lfj); - uj_type = rslty }) + type_case_branches env indspec (make_judge p pt) c in + let () = check_branch_types env pind c ct lft bty in + rslty -let judge_of_projection env p cj = +let type_of_projection env p c ct = let pb = lookup_projection p env in let (ind,u), args = - try find_rectype env cj.uj_type - with Not_found -> error_case_not_inductive env cj + try find_rectype env ct + with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(eq_mind pb.proj_ind (fst ind)); - let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in - let ty = substl (cj.uj_val :: List.rev args) ty in - {uj_val = mkProj (p,cj.uj_val); - uj_type = ty} + assert(eq_mind pb.proj_ind (fst ind)); + let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in + substl (c :: List.rev args) ty + (* Fixpoints. *) (* Checks the type of a general (co)fixpoint, i.e. without checking *) (* the specific guard condition. *) -let type_fixpoint env lna lar vdefj = - let lt = Array.length vdefj in +let check_fixpoint env lna lar vdef vdeft = + let lt = Array.length vdeft in assert (Int.equal (Array.length lar) lt); try - conv_leq_vecti env (Array.map j_type vdefj) (Array.map (fun ty -> lift lt ty) lar) + conv_leq_vecti env vdeft (Array.map (fun ty -> lift lt ty) lar) with NotConvertibleVect i -> - error_ill_typed_rec_body env i lna vdefj lar + error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar (************************************************************************) (************************************************************************) @@ -422,95 +339,96 @@ let type_fixpoint env lna lar vdefj = Ind et Constructsi un jour cela devient des constructions arbitraires et non plus des variables *) let rec execute env cstr = + let open Context.Rel.Declaration in match kind_of_term cstr with (* Atomic terms *) | Sort (Prop c) -> - judge_of_prop_contents c + type1 | Sort (Type u) -> - judge_of_type u + type_of_type u | Rel n -> - judge_of_relative env n + type_of_relative env n | Var id -> - judge_of_variable env id + type_of_variable env id | Const c -> - judge_of_constant env c + type_of_constant env c | Proj (p, c) -> - let cj = execute env c in - judge_of_projection env p cj + let ct = execute env c in + type_of_projection env p c ct (* Lambda calculus operators *) | App (f,args) -> - let jl = execute_array env args in - let j = + let argst = execute_array env args in + let ft = match kind_of_term f with - | Ind ind when Environ.template_polymorphic_pind ind env -> - (* Sort-polymorphism of inductive types *) - let args = Array.map (fun j -> lazy j.uj_type) jl in - judge_of_inductive_knowing_parameters env ind args - | Const cst when Environ.template_polymorphic_pconstant cst env -> - (* Sort-polymorphism of constant *) - let args = Array.map (fun j -> lazy j.uj_type) jl in - judge_of_constant_knowing_parameters env cst args - | _ -> - (* No sort-polymorphism *) - execute env f + | Ind ind when Environ.template_polymorphic_pind ind env -> + (* Template sort-polymorphism of inductive types *) + let args = Array.map (fun t -> lazy t) argst in + type_of_inductive_knowing_parameters env ind args + | Const cst when Environ.template_polymorphic_pconstant cst env -> + (* Template sort-polymorphism of constants *) + let args = Array.map (fun t -> lazy t) argst in + type_of_constant_knowing_parameters env cst args + | _ -> + (* Full or no sort-polymorphism *) + execute env f in - judge_of_apply env j jl + + type_of_apply env f ft args argst | Lambda (name,c1,c2) -> - let varj = execute_type env c1 in - let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in - let j' = execute env1 c2 in - judge_of_abstraction env name varj j' + let _ = execute_is_type env c1 in + let env1 = push_rel (LocalAssum (name,c1)) env in + let c2t = execute env1 c2 in + type_of_abstraction env name c1 c2t | Prod (name,c1,c2) -> - let varj = execute_type env c1 in - let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in - let varj' = execute_type env1 c2 in - judge_of_product env name varj varj' + let vars = execute_is_type env c1 in + let env1 = push_rel (LocalAssum (name,c1)) env in + let vars' = execute_is_type env1 c2 in + type_of_product env name vars vars' | LetIn (name,c1,c2,c3) -> - let j1 = execute env c1 in - let j2 = execute_type env c2 in - let _ = judge_of_cast env j1 DEFAULTcast j2 in - let env1 = push_rel (LocalDef (name,j1.uj_val,j2.utj_val)) env in - let j' = execute env1 c3 in - judge_of_letin env name j1 j2 j' + let c1t = execute env c1 in + let _c2s = execute_is_type env c2 in + let () = check_cast env c1 c1t DEFAULTcast c2 in + let env1 = push_rel (LocalDef (name,c1,c2)) env in + let c3t = execute env1 c3 in + subst1 c1 c3t | Cast (c,k,t) -> - let cj = execute env c in - let tj = execute_type env t in - judge_of_cast env cj k tj + let ct = execute env c in + let _ts = (check_type env t (execute env t)) in + let () = check_cast env c ct k t in + t (* Inductive types *) | Ind ind -> - judge_of_inductive env ind + type_of_inductive env ind | Construct c -> - judge_of_constructor env c + type_of_constructor env c | Case (ci,p,c,lf) -> - let cj = execute env c in - let pj = execute env p in - let lfj = execute_array env lf in - judge_of_case env ci pj cj lfj + let ct = execute env c in + let pt = execute env p in + let lft = execute_array env lf in + type_of_case env ci p pt c ct lf lft | Fix ((vn,i as vni),recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let fix = (vni,recdef') in - check_fix env fix; - make_judge (mkFix fix) fix_ty + check_fix env fix; fix_ty | CoFix (i,recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let cofix = (i,recdef') in - check_cofix env cofix; - (make_judge (mkCoFix cofix) fix_ty) + check_cofix env cofix; fix_ty (* Partial proofs: unsupported by the kernel *) | Meta _ -> @@ -519,53 +437,158 @@ let rec execute env cstr = | Evar _ -> anomaly (Pp.str "the kernel does not support existential variables") -and execute_type env constr = - let j = execute env constr in - type_judgment env j +and execute_is_type env constr = + let t = execute env constr in + check_type env constr t and execute_recdef env (names,lar,vdef) i = - let larj = execute_array env lar in - let lara = Array.map (assumption_of_judgment env) larj in + let lart = execute_array env lar in + let lara = Array.map2 (check_assumption env) lar lart in let env1 = push_rec_types (names,lara,vdef) env in - let vdefj = execute_array env1 vdef in - let vdefv = Array.map j_val vdefj in - let () = type_fixpoint env1 names lara vdefj in - (lara.(i),(names,lara,vdefv)) + let vdeft = execute_array env1 vdef in + let () = check_fixpoint env1 names lara vdef vdeft in + (lara.(i),(names,lara,vdef)) and execute_array env = Array.map (execute env) (* Derived functions *) let infer env constr = - let j = execute env constr in - assert (eq_constr j.uj_val constr); - j + let t = execute env constr in + make_judge constr t + +let infer = + if Flags.profile then + let infer_key = Profile.declare_profile "Fast_infer" in + Profile.profile2 infer_key (fun b c -> infer b c) + else (fun b c -> infer b c) + +let assumption_of_judgment env {uj_val=c; uj_type=t} = + check_assumption env c t -(* let infer_key = Profile.declare_profile "infer" *) -(* let infer = Profile.profile2 infer_key infer *) +let type_judgment env {uj_val=c; uj_type=t} = + let s = check_type env c t in + {utj_val = c; utj_type = s } let infer_type env constr = - let j = execute_type env constr in - j + let t = execute env constr in + let s = check_type env constr t in + {utj_val = constr; utj_type = s} let infer_v env cv = let jv = execute_array env cv in - jv + make_judgev cv jv (* Typing of several terms. *) let infer_local_decl env id = function - | LocalDefEntry c -> - let j = infer env c in - LocalDef (Name id, j.uj_val, j.uj_type) - | LocalAssumEntry c -> - let j = infer env c in - LocalAssum (Name id, assumption_of_judgment env j) + | Entries.LocalDefEntry c -> + let t = execute env c in + RelDecl.LocalDef (Name id, c, t) + | Entries.LocalAssumEntry c -> + let t = execute env c in + RelDecl.LocalAssum (Name id, check_assumption env c t) let infer_local_decls env decls = let rec inferec env = function | (id, d) :: l -> let (env, l) = inferec env l in let d = infer_local_decl env id d in - (push_rel d env, Context.Rel.add d l) - | [] -> (env, Context.Rel.empty) in + (push_rel d env, Context.Rel.add d l) + | [] -> (env, Context.Rel.empty) + in inferec env decls + +let judge_of_prop = make_judge mkProp type1 +let judge_of_set = make_judge mkSet type1 +let judge_of_type u = make_judge (mkType u) (type_of_type u) + +let judge_of_prop_contents = function + | Null -> judge_of_prop + | Pos -> judge_of_set + +let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k) + +let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x) + +let judge_of_constant env cst = make_judge (mkConstU cst) (type_of_constant env cst) +let judge_of_constant_knowing_parameters env cst args = + make_judge (mkConstU cst) (type_of_constant_knowing_parameters env cst args) + +let judge_of_projection env p cj = + make_judge (mkProj (p,cj.uj_val)) (type_of_projection env p cj.uj_val cj.uj_type) + +let dest_judgev v = + Array.map j_val v, Array.map j_type v + +let judge_of_apply env funj argjv = + let args, argtys = dest_judgev argjv in + make_judge (mkApp (funj.uj_val, args)) (type_of_apply env funj.uj_val funj.uj_type args argtys) + +let judge_of_abstraction env x varj bodyj = + make_judge (mkLambda (x, varj.utj_val, bodyj.uj_val)) + (type_of_abstraction env x varj.utj_val bodyj.uj_type) + +let judge_of_product env x varj outj = + make_judge (mkProd (x, varj.utj_val, outj.utj_val)) + (mkSort (sort_of_product env varj.utj_type outj.utj_type)) + +let judge_of_letin env name defj typj j = + make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val)) + (subst1 defj.uj_val j.uj_type) + +let judge_of_cast env cj k tj = + let () = check_cast env cj.uj_val cj.uj_type k tj.utj_val in + let c = match k with | REVERTcast -> cj.uj_val | _ -> mkCast (cj.uj_val, k, tj.utj_val) in + make_judge c tj.utj_val + +let judge_of_inductive env indu = + make_judge (mkIndU indu) (type_of_inductive env indu) + +let judge_of_constructor env cu = + make_judge (mkConstructU cu) (type_of_constructor env cu) + +let judge_of_case env ci pj cj lfj = + let lf, lft = dest_judgev lfj in + make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) + (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) + +let type_of_projection_constant env (p,u) = + let cst = Projection.constant p in + let cb = lookup_constant cst env in + match cb.const_proj with + | Some pb -> + if cb.const_polymorphic then + Vars.subst_instance_constr u pb.proj_type + else pb.proj_type + | None -> raise (Invalid_argument "type_of_projection: not a projection") + +(* Instantiation of terms on real arguments. *) + +(* Make a type polymorphic if an arity *) + +let extract_level env p = + let _,c = dest_prod_assum env p in + match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None + +let extract_context_levels env l = + let fold l = function + | RelDecl.LocalAssum (_,p) -> extract_level env p :: l + | RelDecl.LocalDef _ -> l + in + List.fold_left fold [] l + +let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = + let params, ccl = dest_prod_assum env t in + match kind_of_term ccl with + | Sort (Type u) -> + let ind, l = decompose_app (whd_all env c) in + if isInd ind && List.is_empty l then + let mis = lookup_mind_specif env (fst (destInd ind)) in + let nparams = Inductive.inductive_params mis in + let paramsl = CList.lastn nparams params in + let param_ccls = extract_context_levels env paramsl in + let s = { template_param_levels = param_ccls; template_level = u} in + TemplateArity (params,s) + else RegularArity t + | _ -> + RegularArity t diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 81fd1427d0..007acae604 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -15,7 +15,7 @@ open Declarations (** {6 Typing functions (not yet tagged as safe) } - They return unsafe judgments that are "in context" of a set of + They return unsafe judgments that are "in context" of a set of (local) universe variables (the ones that appear in the term) and associated constraints. In case of polymorphic definitions, these variables and constraints will be generalized. @@ -91,9 +91,6 @@ val judge_of_cast : val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment -(* val judge_of_inductive_knowing_parameters : *) -(* env -> inductive -> unsafe_judgment array -> unsafe_judgment *) - val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) @@ -101,24 +98,15 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -(** Typecheck general fixpoint (not checking guard conditions) *) -val type_fixpoint : env -> Name.t array -> types array - -> unsafe_judgment array -> unit - -val type_of_constant : env -> pconstant -> types constrained - val type_of_constant_type : env -> constant_type -> types -val type_of_projection : env -> Names.projection puniverses -> types +val type_of_projection_constant : env -> Names.projection puniverses -> types val type_of_constant_in : env -> pconstant -> types val type_of_constant_type_knowing_parameters : env -> constant_type -> types Lazy.t array -> types -val type_of_constant_knowing_parameters : - env -> pconstant -> types Lazy.t array -> types constrained - val type_of_constant_knowing_parameters_in : env -> pconstant -> types Lazy.t array -> types @@ -127,4 +115,4 @@ val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> constant_type (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> constr -> Context.Named.t -> unit +val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit @@ -72,8 +72,6 @@ open Pp_control this block is small enough to fit on a single line \item[hovbox:] Horizontal or Vertical block: breaks lead to new line only when necessary to print the content of the block - \item[tbox:] Tabulation block: go to tabulation marks and no line breaking - (except if no mark yet on the reste of the line) \end{description} *) @@ -82,7 +80,6 @@ type block_type = | Pp_vbox of int | Pp_hvbox of int | Pp_hovbox of int - | Pp_tbox type str_token = | Str_def of string @@ -92,14 +89,11 @@ type 'a ppcmd_token = | Ppcmd_print of 'a | Ppcmd_box of block_type * ('a ppcmd_token Glue.t) | Ppcmd_print_break of int * int - | Ppcmd_set_tab - | Ppcmd_print_tbreak of int * int | Ppcmd_white_space of int | Ppcmd_force_newline | Ppcmd_print_if_broken | Ppcmd_open_box of block_type | Ppcmd_close_box - | Ppcmd_close_tbox | Ppcmd_comment of string list | Ppcmd_open_tag of Tag.t | Ppcmd_close_tag @@ -161,8 +155,6 @@ let utf8_length s = let str s = Glue.atom(Ppcmd_print (Str_def s)) let stras (i, s) = Glue.atom(Ppcmd_print (Str_len (s, i))) let brk (a,b) = Glue.atom(Ppcmd_print_break (a,b)) -let tbrk (a,b) = Glue.atom(Ppcmd_print_tbreak (a,b)) -let tab () = Glue.atom(Ppcmd_set_tab) let fnl () = Glue.atom(Ppcmd_force_newline) let pifb () = Glue.atom(Ppcmd_print_if_broken) let ws n = Glue.atom(Ppcmd_white_space n) @@ -212,16 +204,13 @@ let h n s = Glue.atom(Ppcmd_box(Pp_hbox n,s)) let v n s = Glue.atom(Ppcmd_box(Pp_vbox n,s)) let hv n s = Glue.atom(Ppcmd_box(Pp_hvbox n,s)) let hov n s = Glue.atom(Ppcmd_box(Pp_hovbox n,s)) -let t s = Glue.atom(Ppcmd_box(Pp_tbox,s)) (* Opening and closing of boxes *) let hb n = Glue.atom(Ppcmd_open_box(Pp_hbox n)) let vb n = Glue.atom(Ppcmd_open_box(Pp_vbox n)) let hvb n = Glue.atom(Ppcmd_open_box(Pp_hvbox n)) let hovb n = Glue.atom(Ppcmd_open_box(Pp_hovbox n)) -let tb () = Glue.atom(Ppcmd_open_box Pp_tbox) let close () = Glue.atom(Ppcmd_close_box) -let tclose () = Glue.atom(Ppcmd_close_tbox) (* Opening and closed of tags *) let open_tag t = Glue.atom(Ppcmd_open_tag t) @@ -263,7 +252,6 @@ let pp_dirs ?pp_tag ft = | Pp_vbox n -> Format.pp_open_vbox ft n | Pp_hvbox n -> Format.pp_open_hvbox ft n | Pp_hovbox n -> Format.pp_open_hovbox ft n - | Pp_tbox -> Format.pp_open_tbox ft () in let rec pp_cmd = function | Ppcmd_print tok -> @@ -280,11 +268,8 @@ let pp_dirs ?pp_tag ft = Format.pp_close_box ft () | Ppcmd_open_box bty -> pp_open_box bty | Ppcmd_close_box -> Format.pp_close_box ft () - | Ppcmd_close_tbox -> Format.pp_close_tbox ft () | Ppcmd_white_space n -> Format.pp_print_break ft n 0 | Ppcmd_print_break(m,n) -> Format.pp_print_break ft m n - | Ppcmd_set_tab -> Format.pp_set_tab ft () - | Ppcmd_print_tbreak(m,n) -> Format.pp_print_tbreak ft m n | Ppcmd_force_newline -> Format.pp_force_newline ft () | Ppcmd_print_if_broken -> Format.pp_print_if_newline ft () | Ppcmd_comment coms -> List.iter (pr_com ft) coms diff --git a/lib/pp.mli b/lib/pp.mli index 8342a983de..f17908262c 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -15,8 +15,6 @@ type std_ppcmds val str : string -> std_ppcmds val stras : int * string -> std_ppcmds val brk : int * int -> std_ppcmds -val tbrk : int * int -> std_ppcmds -val tab : unit -> std_ppcmds val fnl : unit -> std_ppcmds val pifb : unit -> std_ppcmds val ws : int -> std_ppcmds @@ -58,7 +56,6 @@ val h : int -> std_ppcmds -> std_ppcmds val v : int -> std_ppcmds -> std_ppcmds val hv : int -> std_ppcmds -> std_ppcmds val hov : int -> std_ppcmds -> std_ppcmds -val t : std_ppcmds -> std_ppcmds (** {6 Opening and closing of boxes} *) @@ -66,9 +63,7 @@ val hb : int -> std_ppcmds val vb : int -> std_ppcmds val hvb : int -> std_ppcmds val hovb : int -> std_ppcmds -val tb : unit -> std_ppcmds val close : unit -> std_ppcmds -val tclose : unit -> std_ppcmds (** {6 Opening and closing of tags} *) diff --git a/lib/unicode.ml b/lib/unicode.ml index ced5e258c2..959ccaf73c 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -124,27 +124,11 @@ exception End_of_input let utf8_of_unicode n = if n < 128 then String.make 1 (Char.chr n) - else if n < 2048 then - let s = String.make 2 (Char.chr (128 + n mod 64)) in - begin - s.[0] <- Char.chr (192 + n / 64); - s - end - else if n < 65536 then - let s = String.make 3 (Char.chr (128 + n mod 64)) in - begin - s.[1] <- Char.chr (128 + (n / 64) mod 64); - s.[0] <- Char.chr (224 + n / 4096); - s - end else - let s = String.make 4 (Char.chr (128 + n mod 64)) in - begin - s.[2] <- Char.chr (128 + (n / 64) mod 64); - s.[1] <- Char.chr (128 + (n / 4096) mod 64); - s.[0] <- Char.chr (240 + n / 262144); - s - end + let (m,s) = if n < 2048 then (2,192) else if n < 65536 then (3,224) else (4,240) in + String.init m (fun i -> + let j = (n lsr ((m - 1 - i) * 6)) land 63 in + Char.chr (j + if i = 0 then s else 128)) (* If [s] is some UTF-8 encoded string and [i] is a position of some UTF-8 character within [s] diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4 index f3e2c99f4c..2980274487 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin + DECLARE PLUGIN "btauto_plugin" TACTIC EXTEND btauto diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index bc53b113df..7347c3c2cd 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -444,7 +444,7 @@ and applist_projection c l = let p = Projection.make (fst c) false in (match l with | [] -> (* Expand the projection *) - let ty,_ = Typeops.type_of_constant (Global.env ()) c in + let ty = Typeops.type_of_constant_in (Global.env ()) c in (* FIXME constraints *) let pb = Environ.lookup_projection p (Global.env()) in let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 6f6811334d..7e76854b16 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -8,6 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open Cctac open Stdarg diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index f68c01b18b..2b63ed6d6e 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ltac_plugin open CErrors open Util open Names diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index e19dc86c45..deb2ede1d5 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ltac_plugin open CErrors open Util open Pp diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index 18a35c6cfb..a71d20f0dc 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -10,6 +10,7 @@ DECLARE PLUGIN "decl_mode_plugin" +open Ltac_plugin open Compat open Pp open Decl_expr diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 59a0bb5a2d..f5de638ed2 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ltac_plugin open CErrors open Pp open Decl_expr diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 9446cf667c..de97ba97c3 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -308,15 +308,16 @@ end module DupMap = Map.Make(DupOrd) -let add_duplicate, check_duplicate = +let add_duplicate, get_duplicate = let index = ref 0 and dups = ref DupMap.empty in register_cleanup (fun () -> index := 0; dups := DupMap.empty); let add mp l = incr index; let ren = "Coq__" ^ string_of_int !index in dups := DupMap.add (mp,l) ren !dups - and check mp l = DupMap.find (mp, l) !dups - in (add,check) + and get mp l = + try Some (DupMap.find (mp, l) !dups) with Not_found -> None + in (add,get) type reset_kind = AllButExternal | Everything @@ -510,10 +511,11 @@ let pp_duplicate k' prefix mp rls olab = (* Here rls=s::rls', we search the label for s inside mp *) List.tl rls, get_nth_label_mp (mp_length mp - mp_length prefix) mp in - try dottify (check_duplicate prefix lbl :: rls') - with Not_found -> - assert (get_phase () == Pre); (* otherwise it's too late *) - add_duplicate prefix lbl; dottify rls + match get_duplicate prefix lbl with + | Some ren -> dottify (ren :: rls') + | None -> + assert (get_phase () == Pre); (* otherwise it's too late *) + add_duplicate prefix lbl; dottify rls let fstlev_ks k = function | [] -> assert false diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 2f5601964e..b8e95afb38 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -62,7 +62,7 @@ val top_visible_mp : unit -> module_path val push_visible : module_path -> module_path list -> unit val pop_visible : unit -> unit -val check_duplicate : module_path -> Label.t -> string +val get_duplicate : module_path -> Label.t -> string option type reset_kind = AllButExternal | Everything diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 52f22ee603..e019bb3c2a 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -507,8 +507,7 @@ let print_structure_to_file (fn,si,mo) dry struc = in (* First, a dry run, for computing objects to rename or duplicate *) set_phase Pre; - let devnull = formatter true None in - pp_with devnull (d.pp_struct struc); + ignore (d.pp_struct struc); let opened = opened_libraries () in (* Print the implementation *) let cout = if dry then None else Option.map open_out fn in diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index a980a43f53..2b19c2805f 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -258,7 +258,7 @@ let rec extract_type env db j c args = | Const (kn,u as c) -> let r = ConstRef kn in let cb = lookup_constant kn env in - let typ,_ = Typeops.type_of_constant env c in + let typ = Typeops.type_of_constant_in env c in (match flag_of_type env typ with | (Logic,_) -> assert false (* Cf. logical cases above *) | (Info, TypeScheme) -> diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index e1d6bb4a84..3ed959cf2c 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -12,6 +12,7 @@ DECLARE PLUGIN "extraction_plugin" (* ML names *) +open Ltac_plugin open Genarg open Stdarg open Pcoq.Prim diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 1c29a9bc24..d89bf95ee8 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -555,24 +555,6 @@ let pp_decl = function | Dfix (rv,defs,typs) -> pp_Dfix (rv,defs,typs) -let pp_alias_decl ren = function - | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } - | Dtype (r, l, _) -> - let name = pp_global Type r in - let l = rename_tvars keywords l in - let ids = pp_parameters l in - hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ - str (ren^".") ++ name) - | Dterm (r, a, t) -> - let name = pp_global Term r in - hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) - | Dfix (rv, _, _) -> - prvecti (fun i r -> if is_inline_custom r then mt () else - let name = pp_global Term r in - hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++ - fnl ()) - rv - let pp_spec = function | Sval (r,_) when is_inline_custom r -> mt () | Stype (r,_,_) when is_inline_custom r -> mt () @@ -597,42 +579,32 @@ let pp_spec = function in hov 2 (str "type " ++ ids ++ name ++ def) -let pp_alias_spec ren = function - | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } - | Stype (r,l,_) -> - let name = pp_global Type r in - let l = rename_tvars keywords l in - let ids = pp_parameters l in - hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ - str (ren^".") ++ name) - | Sval _ -> assert false - let rec pp_specif = function | (_,Spec (Sval _ as s)) -> pp_spec s | (l,Spec s) -> - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in + (match Common.get_duplicate (top_visible_mp ()) l with + | None -> pp_spec s + | Some ren -> hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++ fnl () ++ str "end" ++ fnl () ++ - pp_alias_spec ren s - with Not_found -> pp_spec s) + str ("include module type of struct include "^ren^" end")) | (l,Smodule mt) -> let def = pp_module_type [] mt in - let def' = pp_module_type [] mt in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++ - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in - fnl () ++ hov 1 (str ("module "^ren^" :") ++ fnl () ++ def') - with Not_found -> Pp.mt ()) + (match Common.get_duplicate (top_visible_mp ()) l with + | None -> Pp.mt () + | Some ren -> + fnl () ++ + hov 1 (str ("module "^ren^" :") ++ spc () ++ + str "module type of struct include " ++ name ++ str " end")) | (l,Smodtype mt) -> let def = pp_module_type [] mt in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++ - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in - fnl () ++ str ("module type "^ren^" = ") ++ name - with Not_found -> Pp.mt ()) + (match Common.get_duplicate (top_visible_mp ()) l with + | None -> Pp.mt () + | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name) and pp_module_type params = function | MTident kn -> @@ -653,8 +625,10 @@ and pp_module_type params = function let l = List.rev l in pop_visible (); str "sig" ++ fnl () ++ - v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ - fnl () ++ str "end" + (if List.is_empty l then mt () + else + v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ()) + ++ str "end" | MTwith(mt,ML_With_type(idl,vl,typ)) -> let ids = pp_parameters (rename_tvars keywords vl) in let mp_mt = msid_of_mt mt in @@ -681,12 +655,11 @@ let is_short = function MEident _ | MEapply _ -> true | _ -> false let rec pp_structure_elem = function | (l,SEdecl d) -> - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in + (match Common.get_duplicate (top_visible_mp ()) l with + | None -> pp_decl d + | Some ren -> hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++ - fnl () ++ str "end" ++ fnl () ++ - pp_alias_decl ren d - with Not_found -> pp_decl d) + fnl () ++ str "end" ++ fnl () ++ str ("include "^ren)) | (l,SEmodule m) -> let typ = (* virtual printing of the type, in order to have a correct mli later*) @@ -699,18 +672,16 @@ let rec pp_structure_elem = function hov 1 (str "module " ++ name ++ typ ++ str " =" ++ (if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++ - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in - fnl () ++ str ("module "^ren^" = ") ++ name - with Not_found -> mt ()) + (match Common.get_duplicate (top_visible_mp ()) l with + | Some ren -> fnl () ++ str ("module "^ren^" = ") ++ name + | None -> mt ()) | (l,SEmodtype m) -> let def = pp_module_type [] m in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++ - (try - let ren = Common.check_duplicate (top_visible_mp ()) l in - fnl () ++ str ("module type "^ren^" = ") ++ name - with Not_found -> mt ()) + (match Common.get_duplicate (top_visible_mp ()) l with + | None -> mt () + | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name) and pp_module_expr params = function | MEident mp -> pp_modname mp @@ -732,8 +703,10 @@ and pp_module_expr params = function let l = List.rev l in pop_visible (); str "struct" ++ fnl () ++ - v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ - fnl () ++ str "end" + (if List.is_empty l then mt () + else + v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ()) + ++ str "end" let rec prlist_sep_nonempty sep f = function | [] -> mt () diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 260e86ad67..e28d6aa626 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -8,6 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open Formula open Sequent open Ground diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 628af4e719..d6cd7e2a08 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ltac_plugin open Formula open Sequent open Rules diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 index 7c665ae7b5..1960fa8355 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.ml4 @@ -8,6 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open FourierR DECLARE PLUGIN "fourier_plugin" diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 6603a95a84..368b23be30 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open Compat open Util open Term diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index c8b4e48337..70333b063d 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ltac_plugin open Tacexpr open Declarations open CErrors diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 54066edfb8..e00fa528ad 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -78,8 +78,10 @@ let def_of_const t = let type_of_const t = match (kind_of_term t) with - Const sp -> Typeops.type_of_constant (Global.env()) sp - |_ -> assert false + | Const sp -> + (* FIXME discarding universe constraints *) + Typeops.type_of_constant_in (Global.env()) sp + |_ -> assert false let constr_of_global x = fst (Universes.unsafe_constr_of_global x) @@ -1422,7 +1424,7 @@ let start_equation (f:global_reference) (term_f:global_reference) (cont_tactic:Id.t list -> tactic) g = let ids = pf_ids_of_hyps g in let terminate_constr = constr_of_global term_f in - let nargs = nb_prod (fst (type_of_const terminate_constr)) (*FIXME*) in + let nargs = nb_prod (type_of_const terminate_constr) in let x = n_x_id ids nargs in observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [ h_intros x; diff --git a/ltac/tauto.mli b/plugins/ltac/Ltac.v index e69de29bb2..e69de29bb2 100644 --- a/ltac/tauto.mli +++ b/plugins/ltac/Ltac.v diff --git a/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 28ff6df838..28ff6df838 100644 --- a/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 diff --git a/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index c5b26e6d56..c5b26e6d56 100644 --- a/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml diff --git a/ltac/evar_tactics.mli b/plugins/ltac/evar_tactics.mli index e67540c055..e67540c055 100644 --- a/ltac/evar_tactics.mli +++ b/plugins/ltac/evar_tactics.mli diff --git a/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 53b726432c..53b726432c 100644 --- a/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 diff --git a/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index b12187e18a..b12187e18a 100644 --- a/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli diff --git a/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 1223f6eb4b..1223f6eb4b 100644 --- a/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 diff --git a/ltac/extratactics.mli b/plugins/ltac/extratactics.mli index 18334dafe7..18334dafe7 100644 --- a/ltac/extratactics.mli +++ b/plugins/ltac/extratactics.mli diff --git a/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 4ec42c676f..4ec42c676f 100644 --- a/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 diff --git a/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index a28132a4b0..a28132a4b0 100644 --- a/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 diff --git a/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4 index 905653281c..905653281c 100644 --- a/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.ml4 diff --git a/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 54229bb2ae..54229bb2ae 100644 --- a/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 diff --git a/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index d286a58708..d286a58708 100644 --- a/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 diff --git a/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index b1c4f58eb8..b1c4f58eb8 100644 --- a/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 diff --git a/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 685c07c9a8..685c07c9a8 100644 --- a/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 diff --git a/ltac/ltac.mllib b/plugins/ltac/ltac_plugin.mlpack index af1c7149da..af1c7149da 100644 --- a/ltac/ltac.mllib +++ b/plugins/ltac/ltac_plugin.mlpack diff --git a/ltac/pltac.ml b/plugins/ltac/pltac.ml index 1d21118ae8..1d21118ae8 100644 --- a/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml diff --git a/ltac/pltac.mli b/plugins/ltac/pltac.mli index 810e1ec39a..810e1ec39a 100644 --- a/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli diff --git a/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index b1a6fa63d6..fccee6e40a 100644 --- a/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1243,11 +1243,10 @@ let declare_extra_genarg_pprule wit (f : 'a raw_extra_genarg_printer) (g : 'b glob_extra_genarg_printer) (h : 'c extra_genarg_printer) = - let s = match wit with - | ExtraArg s -> ArgT.repr s - | _ -> error - "Can declare a pretty-printing rule only for extra argument types." - in + begin match wit with + | ExtraArg s -> () + | _ -> error "Can declare a pretty-printing rule only for extra argument types." + end; let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in let g x = let env = Global.env () in diff --git a/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 86e3ea5484..86e3ea5484 100644 --- a/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli diff --git a/ltac/pptacticsig.mli b/plugins/ltac/pptacticsig.mli index 74ddd377ad..74ddd377ad 100644 --- a/ltac/pptacticsig.mli +++ b/plugins/ltac/pptacticsig.mli diff --git a/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 2514ededb0..2514ededb0 100644 --- a/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml diff --git a/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli index e5e2e41975..e5e2e41975 100644 --- a/ltac/profile_ltac.mli +++ b/plugins/ltac/profile_ltac.mli diff --git a/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 index 8cb76d81c5..8cb76d81c5 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.ml4 diff --git a/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3c5a109c0d..3c5a109c0d 100644 --- a/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml diff --git a/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 35c4483513..35c4483513 100644 --- a/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli diff --git a/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index 42552c4846..42552c4846 100644 --- a/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml diff --git a/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index bfa423db20..bfa423db20 100644 --- a/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli diff --git a/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index df38a42cb9..df38a42cb9 100644 --- a/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml diff --git a/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 0b67f8726e..0b67f8726e 100644 --- a/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli diff --git a/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 2e2b55be74..2e2b55be74 100644 --- a/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml diff --git a/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 969c118fb5..969c118fb5 100644 --- a/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli diff --git a/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index e3c2b4ad51..e3c2b4ad51 100644 --- a/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml diff --git a/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 94e14223aa..94e14223aa 100644 --- a/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli diff --git a/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 9c25a16457..9c25a16457 100644 --- a/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli diff --git a/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 4b5d87fc3c..4b5d87fc3c 100644 --- a/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml diff --git a/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 71ca354fa1..71ca354fa1 100644 --- a/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli diff --git a/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index fda9142eda..fda9142eda 100644 --- a/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml diff --git a/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 6f64981eff..6f64981eff 100644 --- a/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli diff --git a/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index b09bdda65c..b09bdda65c 100644 --- a/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml diff --git a/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli index c1bf272579..c1bf272579 100644 --- a/ltac/tacsubst.mli +++ b/plugins/ltac/tacsubst.mli diff --git a/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 5cbddc7f64..5cbddc7f64 100644 --- a/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml diff --git a/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 520fb41eff..520fb41eff 100644 --- a/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli diff --git a/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index ef45ee47e1..ef45ee47e1 100644 --- a/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml diff --git a/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli index 090207bcc3..090207bcc3 100644 --- a/ltac/tactic_matching.mli +++ b/plugins/ltac/tactic_matching.mli diff --git a/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml index a5ba3b8371..a5ba3b8371 100644 --- a/ltac/tactic_option.ml +++ b/plugins/ltac/tactic_option.ml diff --git a/ltac/tactic_option.mli b/plugins/ltac/tactic_option.mli index ed759a76db..ed759a76db 100644 --- a/ltac/tactic_option.mli +++ b/plugins/ltac/tactic_option.mli diff --git a/ltac/tauto.ml b/plugins/ltac/tauto.ml index 756958c2f0..756958c2f0 100644 --- a/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml diff --git a/plugins/ltac/tauto.mli b/plugins/ltac/tauto.mli new file mode 100644 index 0000000000..e69de29bb2 --- /dev/null +++ b/plugins/ltac/tauto.mli diff --git a/plugins/ltac/vo.itarget b/plugins/ltac/vo.itarget new file mode 100644 index 0000000000..a28fb770be --- /dev/null +++ b/plugins/ltac/vo.itarget @@ -0,0 +1 @@ +Ltac.vo diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index 79020ed037..ccb6daa116 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -16,6 +16,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open Stdarg open Tacarg diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index 5f906a8dad..195dec3627 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -1,5 +1,3 @@ -DECLARE PLUGIN "nsatz_plugin" - (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) @@ -10,6 +8,8 @@ DECLARE PLUGIN "nsatz_plugin" (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin + DECLARE PLUGIN "nsatz_plugin" TACTIC EXTEND nsatz_compute diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 27115abecc..6b711a1761 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -17,6 +17,7 @@ DECLARE PLUGIN "omega_plugin" +open Ltac_plugin open Names open Coq_omega open Stdarg diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index e7e6ecef98..f2c021f595 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -8,6 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open Names open Misctypes open Tacexpr diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 2f38688d1f..9a54ad7789 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -10,6 +10,7 @@ DECLARE PLUGIN "romega_plugin" +open Ltac_plugin open Names open Refl_omega open Stdarg diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index d27b04834e..7e58ef9a3e 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin + DECLARE PLUGIN "rtauto_plugin" TACTIC EXTEND rtauto diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 367a133330..35d6768c13 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -8,6 +8,7 @@ module Search = Explore.Make(Proof_search) +open Ltac_plugin open CErrors open Util open Term diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 0987c44ae2..707ff79a6c 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -8,6 +8,7 @@ (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open Pp open Util open Libnames diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 657efe175b..59f23a6379 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Ltac_plugin open Pp open CErrors open Util diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index fc988a2c5f..f4f6efa4a6 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -15,6 +15,7 @@ let frozen_lexer = CLexer.freeze () ;; (*i camlp4use: "pa_extend.cmo" i*) (*i camlp4deps: "grammar/grammar.cma" i*) +open Ltac_plugin open Names open Pp open Pcoq diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 29f57144a9..ac6d775e34 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -24,14 +24,14 @@ open Context.Rel.Declaration let type_of_inductive env (ind,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - Typeops.check_hyps_inclusion env (mkInd ind) mib.mind_hyps; + Typeops.check_hyps_inclusion env mkInd ind mib.mind_hyps; Inductive.type_of_inductive env (specif,u) (* Return type as quoted by the user *) let type_of_constructor env (cstr,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Typeops.check_hyps_inclusion env (mkConstruct cstr) mib.mind_hyps; + Typeops.check_hyps_inclusion env mkConstruct cstr mib.mind_hyps; Inductive.type_of_constructor (cstr,u) specif (* Return constructor types in user form *) @@ -615,7 +615,7 @@ let type_of_projection_knowing_arg env sigma p c ty = raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type") in let (_,u), pars = dest_ind_family pars in - substl (c :: List.rev pars) (Typeops.type_of_projection env (p,u)) + substl (c :: List.rev pars) (Typeops.type_of_projection_constant env (p,u)) (***********************************************) (* Guard condition *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index a2ee622215..120cde5e55 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -317,7 +317,10 @@ let constrain_variables init uctx = let cstrs = UState.constrain_variables levels uctx in Univ.ContextSet.add_constraints cstrs (UState.context_set uctx) -let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = +type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context + +let close_proof ~keep_body_ucst_separate ?feedback_id ~now + (fpl : closed_proof_output Future.computation) = let { pid; section_vars; strength; proof; terminator; universe_binders } = cur_pstate () in let poly = pi2 strength (* Polymorphic *) in @@ -395,8 +398,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl = universes = (universes, binders) }, fun pr_ending -> CEphemeron.get terminator pr_ending -type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context - let return_proof ?(allow_partial=false) () = let { pid; proof; strength = (_,poly,_) } = cur_pstate () in if allow_partial then begin diff --git a/stm/stm.ml b/stm/stm.ml index 6f34c8dbc3..e698d1c72e 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -24,11 +24,13 @@ open Ppvernac open Vernac_classifier open Feedback +let execution_error state_id loc msg = + feedback ~id:(State state_id) + (Message (Error, Some loc, pp_to_richpp msg)) + module Hooks = struct let process_error, process_error_hook = Hook.make () -let interp, interp_hook = Hook.make () -let with_fail, with_fail_hook = Hook.make () let state_computed, state_computed_hook = Hook.make ~default:(fun state_id ~in_cache -> @@ -48,10 +50,6 @@ let parse_error, parse_error_hook = Hook.make ~default:(fun id loc msg -> feedback ~id (Message(Error, Some loc, pp_to_richpp msg))) () -let execution_error, execution_error_hook = Hook.make - ~default:(fun state_id loc msg -> - feedback ~id:(State state_id) (Message(Error, Some loc, pp_to_richpp msg))) () - let unreachable_state, unreachable_state_hook = Hook.make ~default:(fun _ _ -> ()) () @@ -105,26 +103,6 @@ let may_pierce_opaque = function | { expr = VernacExtend (("ExtractionInductive",_), _) } -> true | _ -> false -(* Wrapper for Vernacentries.interp to set the feedback id *) -let vernac_interp ?proof id ?route { verbose; loc; expr } = - let rec internal_command = function - | VernacResetName _ | VernacResetInitial | VernacBack _ - | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ - | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true - | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> internal_command e - | _ -> false in - if internal_command expr then begin - prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) - end else begin - set_id_for_feedback ?route (State id); - Aux_file.record_in_aux_set_at loc; - prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); - try Hooks.(call interp ?verbosely:(Some verbose) ?proof (loc, expr)) - with e -> - let e = CErrors.push e in - iraise Hooks.(call_process_error_once e) - end - (* Wrapper for Vernac.parse_sentence to set the feedback id *) let indentation_of_string s = let len = String.length s in @@ -860,7 +838,7 @@ end = struct (* {{{ *) | None -> let loc = Option.default Loc.ghost (Loc.get_loc info) in let (e, info) = Hooks.(call_process_error_once (e, info)) in - Hooks.(call execution_error id loc (iprint (e, info))); + execution_error id loc (iprint (e, info)); (e, Stateid.add info ~valid id) let same_env { system = s1 } { system = s2 } = @@ -910,6 +888,126 @@ end = struct (* {{{ *) end (* }}} *) +(* indentation code for Show Script, initially contributed + * by D. de Rauglaudre. Should be moved away. + *) + +module ShowScript = struct + +let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) = + (* ng1 : number of goals remaining at the current level (before cmd) + ngl1 : stack of previous levels with their remaining goals + ng : number of goals after the execution of cmd + beginend : special indentation stack for { } *) + let ngprev = List.fold_left (+) ng1 ngl1 in + let new_ngl = + if ng > ngprev then + (* We've branched *) + (ng - ngprev + 1, ng1 - 1 :: ngl1) + else if ng < ngprev then + (* A subgoal have been solved. Let's compute the new current level + by discarding all levels with 0 remaining goals. *) + let rec loop = function + | (0, ng2::ngl2) -> loop (ng2,ngl2) + | p -> p + in loop (ng1-1, ngl1) + else + (* Standard case, same goal number as before *) + (ng1, ngl1) + in + (* When a subgoal have been solved, separate this block by an empty line *) + let new_nl = (ng < ngprev) + in + (* Indentation depth *) + let ind = List.length ngl1 + in + (* Some special handling of bullets and { }, to get a nicer display *) + let pred n = max 0 (n-1) in + let ind, nl, new_beginend = match cmd with + | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend + | VernacEndSubproof -> List.hd beginend, false, List.tl beginend + | VernacBullet _ -> pred ind, nl, beginend + | _ -> ind, nl, beginend + in + let pp = + (if nl then fnl () else mt ()) ++ + (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)) + in + (new_ngl, new_nl, new_beginend, pp :: ppl) + +let get_script prf = + let branch, test = + match prf with + | None -> VCS.Branch.master, fun _ -> true + | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in + let rec find acc id = + if Stateid.equal id Stateid.initial || + Stateid.equal id Stateid.dummy then acc else + let view = VCS.visit id in + match view.step with + | `Fork((_,_,_,ns), _) when test ns -> acc + | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof + | `Sideff (`Ast (x,_)) -> + find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next + | `Sideff (`Id id) -> find acc id + | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *) + find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next + | `Cmd _ -> find acc view.next + | `Alias (id,_) -> find acc id + | `Fork _ -> find acc view.next + in + find [] (VCS.get_branch_pos branch) + +let show_script ?proof () = + try + let prf = + try match proof with + | None -> Some (Pfedit.get_current_proof_name ()) + | Some (p,_) -> Some (p.Proof_global.id) + with Proof_global.NoCurrentProof -> None + in + let cmds = get_script prf in + let _,_,_,indented_cmds = + List.fold_left indent_script_item ((1,[]),false,[],[]) cmds + in + let indented_cmds = List.rev (indented_cmds) in + msg_notice (v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds)) + with Vcs_aux.Expired -> () + +end + +(* Wrapper for Vernacentries.interp to set the feedback id *) +(* It is currently called 19 times, this number should be certainly + reduced... *) +let stm_vernac_interp ?proof id ?route { verbose; loc; expr } = + (* The Stm will gain the capability to interpret commmads affecting + the whole document state, such as backtrack, etc... so we start + to design the stm command interpreter now *) + set_id_for_feedback ?route (State id); + Aux_file.record_in_aux_set_at loc; + (* We need to check if a command should be filtered from + * vernac_entries, as it cannot handle it. This should go away in + * future refactorings. + *) + let rec is_filtered_command = function + | VernacResetName _ | VernacResetInitial | VernacBack _ + | VernacBackTo _ | VernacRestart | VernacUndo _ | VernacUndoTo _ + | VernacBacktrack _ | VernacAbortAll | VernacAbort _ -> true + | VernacTime (_,e) | VernacTimeout (_,e) | VernacRedirect (_,(_,e)) -> is_filtered_command e + | _ -> false + in + let aux_interp cmd = + if is_filtered_command cmd then + prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr)) + else match cmd with + | VernacShow ShowScript -> ShowScript.show_script () + | expr -> + prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr)); + try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr) + with e -> + let e = CErrors.push e in + iraise Hooks.(call_process_error_once e) + in aux_interp expr (****************************** CRUFT *****************************************) (******************************************************************************) @@ -1287,7 +1385,7 @@ end = struct (* {{{ *) let info = Stateid.add ~valid:start Exninfo.null start in let e = (RemoteException (strbrk s), info) in t_assign (`Exn e); - Hooks.(call execution_error start Loc.ghost (strbrk s)); + execution_error start Loc.ghost (strbrk s); feedback (InProgress ~-1) let build_proof_here ~drop_pt (id,valid) loc eop = @@ -1321,7 +1419,7 @@ end = struct (* {{{ *) Proof_global.close_future_proof stop (Future.from_val ~fix_exn p) in let terminator = (* The one sent by master is an InvalidKey *) Lemmas.(standard_proof_terminator [] (mk_hook (fun _ _ -> ()))) in - vernac_interp stop + stm_vernac_interp stop ~proof:(pobject, terminator) { verbose = false; loc; indentation = 0; strlen = 0; expr = (VernacEndProof (Proved (Opaque None,None))) }) in @@ -1463,7 +1561,7 @@ end = struct (* {{{ *) (* We jump at the beginning since the kernel handles side effects by also * looking at the ones that happen to be present in the current env *) Reach.known_state ~cache:`No start; - vernac_interp stop ~proof + stm_vernac_interp stop ~proof { verbose = false; loc; indentation = 0; strlen = 0; expr = (VernacEndProof (Proved (Opaque None,None))) }; `OK proof @@ -1714,7 +1812,7 @@ end = struct (* {{{ *) else begin let (i, ast) = r_ast in Proof_global.simple_with_current_proof (fun _ p -> Proof.focus focus_cond () i p); - vernac_interp r_state_fb ast; + stm_vernac_interp r_state_fb ast; let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in match Evd.(evar_body (find sigma r_goal)) with | Evd.Evar_empty -> RespNoProgress @@ -1750,7 +1848,7 @@ end = struct (* {{{ *) | VernacTime (_,e) | VernacRedirect (_,(_,e)) -> find true fail e | VernacFail e -> find time true e | _ -> e, time, fail in find false false e in - Hooks.call Hooks.with_fail fail (fun () -> + Vernacentries.with_fail fail (fun () -> (if time then System.with_time false else (fun x -> x)) (fun () -> ignore(TaskQueue.with_n_workers nworkers (fun queue -> Proof_global.with_current_proof (fun _ p -> @@ -1843,7 +1941,7 @@ end = struct (* {{{ *) VCS.print (); Reach.known_state ~cache:`No r_where; try - vernac_interp r_for { r_what with verbose = true }; + stm_vernac_interp r_for { r_what with verbose = true }; feedback ~id:(State r_for) Processed with e when CErrors.noncritical e -> let e = CErrors.push e in @@ -2052,7 +2150,7 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.with_current_proof (fun _ p -> feedback ~id:(State id) Feedback.AddedAxiom; fst (Pfedit.solve Vernacexpr.SelectAll None tac p), ()); - Option.iter (fun expr -> vernac_interp id { + Option.iter (fun expr -> stm_vernac_interp id { verbose = true; loc = Loc.ghost; expr; indentation = 0; strlen = 0 }) recovery_command @@ -2131,24 +2229,24 @@ let known_state ?(redefine_qed=false) ~cache id = resilient_tactic id cblock (fun () -> reach view.next; Hooks.(call tactic_being_run true); - vernac_interp id x; + stm_vernac_interp id x; Hooks.(call tactic_being_run false)); if eff then update_global_env () ), (if eff then `Yes else cache), true | `Cmd { cast = x; ceff = eff } -> (fun () -> resilient_command reach view.next; - vernac_interp id x; + stm_vernac_interp id x; if eff then update_global_env () ), (if eff then `Yes else cache), true | `Fork ((x,_,_,_), None) -> (fun () -> resilient_command reach view.next; - vernac_interp id x; + stm_vernac_interp id x; wall_clock_last_fork := Unix.gettimeofday () ), `Yes, true | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *) reach ~cache:`Shallow prev; reach view.next; - (try vernac_interp id x; + (try stm_vernac_interp id x; with e when CErrors.noncritical e -> let (e, info) = CErrors.push e in let info = Stateid.add info ~valid:prev id in @@ -2198,14 +2296,14 @@ let known_state ?(redefine_qed=false) ~cache id = Proof_global.close_future_proof ~feedback_id:id fp in if not delegate then ignore(Future.compute fp); reach view.next; - vernac_interp id ~proof x; + stm_vernac_interp id ~proof x; feedback ~id:(State id) Incomplete | { VCS.kind = `Master }, _ -> assert false end; Proof_global.discard_all () ), (if redefine_qed then `No else `Yes), true | `Sync (name, _, `Immediate) -> (fun () -> - reach eop; vernac_interp id x; Proof_global.discard_all () + reach eop; stm_vernac_interp id x; Proof_global.discard_all () ), `Yes, true | `Sync (name, pua, reason) -> (fun () -> log_processing_sync id name reason; @@ -2226,7 +2324,7 @@ let known_state ?(redefine_qed=false) ~cache id = if keep != VtKeepAsAxiom then reach view.next; let wall_clock2 = Unix.gettimeofday () in - vernac_interp id ?proof x; + stm_vernac_interp id ?proof x; let wall_clock3 = Unix.gettimeofday () in Aux_file.record_in_aux_at x.loc "proof_check_time" (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2)); @@ -2242,7 +2340,7 @@ let known_state ?(redefine_qed=false) ~cache id = in aux (collect_proof keep (view.next, x) brname brinfo eop) | `Sideff (`Ast (x,_)) -> (fun () -> - reach view.next; vernac_interp id x; update_global_env () + reach view.next; stm_vernac_interp id x; update_global_env () ), cache, true | `Sideff (`Id origin) -> (fun () -> reach view.next; @@ -2430,7 +2528,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty " classified as: " ^ string_of_vernac_classification c); match c with (* PG stuff *) - | VtStm(VtPG,false), VtNow -> vernac_interp Stateid.dummy x; `Ok + | VtStm(VtPG,false), VtNow -> stm_vernac_interp Stateid.dummy x; `Ok | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater") (* Joining various parts of the document *) | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok @@ -2474,13 +2572,13 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty (* Query *) | VtQuery (false,(report_id,route)), VtNow when tty = true -> finish (); - (try Future.purify (vernac_interp report_id ~route) + (try Future.purify (stm_vernac_interp report_id ~route) {x with verbose = true } with e when CErrors.noncritical e -> let e = CErrors.push e in iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok | VtQuery (false,(report_id,route)), VtNow -> - (try vernac_interp report_id ~route x + (try stm_vernac_interp report_id ~route x with e -> let e = CErrors.push e in iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok @@ -2553,7 +2651,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty (* Side effect on all branches *) | VtUnknown, _ when expr = VernacToplevelControl Drop -> - vernac_interp (VCS.get_branch_pos head) x; `Ok + stm_vernac_interp (VCS.get_branch_pos head) x; `Ok | VtSideff l, w -> let in_proof = not (VCS.Branch.equal head VCS.Branch.master) in @@ -2579,7 +2677,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty VCS.checkout VCS.Branch.master; let mid = VCS.get_branch_pos VCS.Branch.master in Reach.known_state ~cache:(interactive ()) mid; - vernac_interp id x; + stm_vernac_interp id x; (* Vernac x may or may not start a proof *) if not in_proof && Proof_global.there_are_pending_proofs () then begin @@ -2609,7 +2707,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty begin match expr with | VernacStm (PGLast _) -> if not (VCS.Branch.equal head VCS.Branch.master) then - vernac_interp Stateid.dummy + stm_vernac_interp Stateid.dummy { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0; expr = VernacShow (ShowGoal OpenSubgoals) } | _ -> () @@ -2856,102 +2954,13 @@ let proofname b = match VCS.get_branch b with let get_all_proof_names () = List.map unmangle (List.map_filter proofname (VCS.branches ())) -let get_current_proof_name () = - Option.map unmangle (proofname (VCS.current_branch ())) - -let get_script prf = - let branch, test = - match prf with - | None -> VCS.Branch.master, fun _ -> true - | Some name -> VCS.current_branch (),fun nl -> nl=[] || List.mem name nl in - let rec find acc id = - if Stateid.equal id Stateid.initial || - Stateid.equal id Stateid.dummy then acc else - let view = VCS.visit id in - match view.step with - | `Fork((_,_,_,ns), _) when test ns -> acc - | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof - | `Sideff (`Ast (x,_)) -> - find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next - | `Sideff (`Id id) -> find acc id - | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *) - find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next - | `Cmd _ -> find acc view.next - | `Alias (id,_) -> find acc id - | `Fork _ -> find acc view.next - in - find [] (VCS.get_branch_pos branch) - -(* indentation code for Show Script, initially contributed - by D. de Rauglaudre *) - -let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) = - (* ng1 : number of goals remaining at the current level (before cmd) - ngl1 : stack of previous levels with their remaining goals - ng : number of goals after the execution of cmd - beginend : special indentation stack for { } *) - let ngprev = List.fold_left (+) ng1 ngl1 in - let new_ngl = - if ng > ngprev then - (* We've branched *) - (ng - ngprev + 1, ng1 - 1 :: ngl1) - else if ng < ngprev then - (* A subgoal have been solved. Let's compute the new current level - by discarding all levels with 0 remaining goals. *) - let rec loop = function - | (0, ng2::ngl2) -> loop (ng2,ngl2) - | p -> p - in loop (ng1-1, ngl1) - else - (* Standard case, same goal number as before *) - (ng1, ngl1) - in - (* When a subgoal have been solved, separate this block by an empty line *) - let new_nl = (ng < ngprev) - in - (* Indentation depth *) - let ind = List.length ngl1 - in - (* Some special handling of bullets and { }, to get a nicer display *) - let pred n = max 0 (n-1) in - let ind, nl, new_beginend = match cmd with - | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend - | VernacEndSubproof -> List.hd beginend, false, List.tl beginend - | VernacBullet _ -> pred ind, nl, beginend - | _ -> ind, nl, beginend - in - let pp = - (if nl then fnl () else mt ()) ++ - (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd)) - in - (new_ngl, new_nl, new_beginend, pp :: ppl) - -let show_script ?proof () = - try - let prf = - try match proof with - | None -> Some (Pfedit.get_current_proof_name ()) - | Some (p,_) -> Some (p.Proof_global.id) - with Proof_global.NoCurrentProof -> None - in - let cmds = get_script prf in - let _,_,_,indented_cmds = - List.fold_left indent_script_item ((1,[]),false,[],[]) cmds - in - let indented_cmds = List.rev (indented_cmds) in - msg_notice (v 0 (prlist_with_sep fnl (fun x -> x) indented_cmds)) - with Vcs_aux.Expired -> () - (* Export hooks *) let state_computed_hook = Hooks.state_computed_hook let state_ready_hook = Hooks.state_ready_hook let parse_error_hook = Hooks.parse_error_hook -let execution_error_hook = Hooks.execution_error_hook let forward_feedback_hook = Hooks.forward_feedback_hook let process_error_hook = Hooks.process_error_hook -let interp_hook = Hooks.interp_hook -let with_fail_hook = Hooks.with_fail_hook let unreachable_state_hook = Hooks.unreachable_state_hook -let get_fix_exn () = !State.fix_exn_ref +let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref) let tactic_being_run_hook = Hooks.tactic_being_run_hook (* vim:set foldmethod=marker: *) diff --git a/stm/stm.mli b/stm/stm.mli index b8a2a38596..0f0a3c4e13 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -184,7 +184,6 @@ val register_proof_block_delimiter : val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t val parse_error_hook : (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t -val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t (* ready means that master has it at hand *) val state_ready_hook : (Stateid.t -> unit) Hook.t @@ -213,12 +212,6 @@ val interp : bool -> vernac_expr located -> unit (* Queries for backward compatibility *) val current_proof_depth : unit -> int val get_all_proof_names : unit -> Id.t list -val get_current_proof_name : unit -> Id.t option -val show_script : ?proof:Proof_global.closed_proof -> unit -> unit (* Hooks to be set by other Coq components in order to break file cycles *) val process_error_hook : Future.fix_exn Hook.t -val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof -> - Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t -val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t -val get_fix_exn : unit -> (Exninfo.iexn -> Exninfo.iexn) diff --git a/stm/stm.mllib b/stm/stm.mllib index 939ee187ae..4b254e8113 100644 --- a/stm/stm.mllib +++ b/stm/stm.mllib @@ -4,7 +4,6 @@ Vcs TQueue WorkerPool Vernac_classifier -Lemmas CoqworkmgrApi AsyncTaskQueue Stm diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 93c04e373c..c5562b326c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -368,6 +368,16 @@ module New = struct catch_failerror e <*> t2 end end + + let tclORELSE0L t1 t2 = + tclINDEPENDENTL begin + tclORELSE + t1 + begin fun e -> + catch_failerror e <*> t2 + end + end + let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2 @@ -419,6 +429,9 @@ module New = struct let tclTRY t = tclORELSE0 t (tclUNIT ()) + + let tclTRYb t = + tclORELSE0L (t <*> tclUNIT true) (tclUNIT false) let tclIFTHENELSE t1 t2 t3 = tclINDEPENDENT begin diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 18cf03c51d..7aacc52f33 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -209,6 +209,7 @@ module New : sig val tclMAP : ('a -> unit tactic) -> 'a list -> unit tactic val tclTRY : unit tactic -> unit tactic + val tclTRYb : unit tactic -> bool list tactic val tclFIRST : unit tactic list -> unit tactic val tclIFTHENELSE : unit tactic -> unit tactic -> unit tactic -> unit tactic val tclIFTHENSVELSE : unit tactic -> unit tactic array -> unit tactic -> unit tactic diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v index a547685070..4b4f81dbce 100644 --- a/test-suite/bugs/closed/3612.v +++ b/test-suite/bugs/closed/3612.v @@ -38,8 +38,11 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P) (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2), p = q. +Declare ML Module "ltac_plugin". Declare ML Module "coretactics". +Set Default Proof Mode "Classic". + Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x)) (xx : @paths (@sigT A (fun x0 : A => B x0)) x x), @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v index fc4c171e2c..8687eaab00 100644 --- a/test-suite/bugs/closed/3649.v +++ b/test-suite/bugs/closed/3649.v @@ -2,7 +2,9 @@ (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *) (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0 coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *) +Declare ML Module "ltac_plugin". Declare ML Module "coretactics". +Set Default Proof Mode "Classic". Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). Reserved Notation "x = y" (at level 70, no associativity). Delimit Scope type_scope with type. diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v index d34a2b8b1b..816bc845fd 100644 --- a/test-suite/bugs/closed/4121.v +++ b/test-suite/bugs/closed/4121.v @@ -4,6 +4,8 @@ Unset Strict Universe Declaration. (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0 coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *) +Declare ML Module "ltac_plugin". + Set Universe Polymorphism. Class Contr_internal (A : Type) := BuildContr { center : A }. Arguments center A {_}. @@ -13,4 +15,4 @@ Definition contr_paths_contr0 {A} `{Contr A} : Contr A := {| center := center A Instance contr_paths_contr1 {A} `{Contr A} : Contr A := {| center := center A |}. Check @contr_paths_contr0@{i}. Check @contr_paths_contr1@{i}. (* Error: Universe instance should have length 2 *) -(** It should have length 1, just like contr_paths_contr0 *)
\ No newline at end of file +(** It should have length 1, just like contr_paths_contr0 *) diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index 08628377f0..c6fcc24b6b 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -5,6 +5,7 @@ then from 269 lines to 255 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) +Declare ML Module "ltac_plugin". Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v index ae17fb145d..64c7fd8eb1 100644 --- a/test-suite/bugs/closed/4533.v +++ b/test-suite/bugs/closed/4533.v @@ -5,6 +5,7 @@ then from 285 lines to 271 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) +Declare ML Module "ltac_plugin". Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. @@ -223,4 +224,4 @@ v = _) r, | [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good" | [ |- ?G ] => fail 1 "bad" G end. - Fail rewrite concat_p_pp.
\ No newline at end of file + Fail rewrite concat_p_pp. diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index da140c9318..64dd8c304f 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -2,6 +2,7 @@ (* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *) (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0 coqtop version 8.5 (January 2016) *) +Declare ML Module "ltac_plugin". Inductive False := . Axiom proof_admitted : False. Tactic Notation "admit" := case proof_admitted. @@ -1004,4 +1005,4 @@ Proof. Fail Timeout 1 Time rewrite !loops_functor_group. (* 0.004 s in 8.5rc1, 8.677 s in 8.5 *) Timeout 1 do 3 rewrite loops_functor_group. -Abort.
\ No newline at end of file +Abort. diff --git a/test-suite/bugs/closed/5346.v b/test-suite/bugs/closed/5346.v new file mode 100644 index 0000000000..0118c18704 --- /dev/null +++ b/test-suite/bugs/closed/5346.v @@ -0,0 +1,29 @@ +Inductive comp : Type -> Type := +| Ret {T} : forall (v:T), comp T +| Bind {T T'} : forall (p: comp T') (p': T' -> comp T), comp T. + +Notation "'do' x .. y <- p1 ; p2" := + (Bind p1 (fun x => .. (fun y => p2) ..)) + (at level 60, right associativity, + x binder, y binder). + +Definition Fst1 A B (p: comp (A*B)) : comp A := + do '(a, b) <- p; + Ret a. + +Definition Fst2 A B (p: comp (A*B)) : comp A := + match tt with + | _ => Bind p (fun '(a, b) => Ret a) + end. + +Definition Fst3 A B (p: comp (A*B)) : comp A := + match tt with + | _ => do a <- p; + Ret (fst a) + end. + +Definition Fst A B (p: comp (A * B)) : comp A := + match tt with + | _ => do '(a, b) <- p; + Ret a + end. diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index c17b285bc9..81fda176ec 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -1,108 +1,108 @@ le_n: forall n : nat, n <= n +le_0_n: forall n : nat, 0 <= n le_S: forall n m : nat, n <= m -> n <= S m +le_n_S: forall n m : nat, n <= m -> S n <= S m +le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m +le_S_n: forall n m : nat, S n <= S m -> n <= m +min_l: forall n m : nat, n <= m -> Nat.min n m = n +max_r: forall n m : nat, n <= m -> Nat.max n m = m +min_r: forall n m : nat, m <= n -> Nat.min n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n le_ind: forall (n : nat) (P : nat -> Prop), P n -> (forall m : nat, n <= m -> P m -> P (S m)) -> forall n0 : nat, n <= n0 -> P n0 -le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m -le_S_n: forall n m : nat, S n <= S m -> n <= m -le_0_n: forall n : nat, 0 <= n -le_n_S: forall n m : nat, n <= m -> S n <= S m -max_l: forall n m : nat, m <= n -> Nat.max n m = n -max_r: forall n m : nat, n <= m -> Nat.max n m = m -min_l: forall n m : nat, n <= m -> Nat.min n m = n -min_r: forall n m : nat, m <= n -> Nat.min n m = m -true: bool false: bool -bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b -bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b -bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b -andb: bool -> bool -> bool -orb: bool -> bool -> bool -implb: bool -> bool -> bool -xorb: bool -> bool -> bool +true: bool +is_true: bool -> Prop negb: bool -> bool -andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true -andb_true_intro: - forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true eq_true: bool -> Prop -eq_true_rect: - forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b -eq_true_ind: - forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b +implb: bool -> bool -> bool +orb: bool -> bool -> bool +andb: bool -> bool -> bool +xorb: bool -> bool -> bool +Nat.even: nat -> bool +Nat.odd: nat -> bool +BoolSpec: Prop -> Prop -> bool -> Prop +Nat.eqb: nat -> nat -> bool +Nat.testbit: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool +Nat.leb: nat -> nat -> bool +Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b +bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b eq_true_rec: forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b -is_true: bool -> Prop -eq_true_ind_r: - forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true -eq_true_rec_r: - forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true +eq_true_ind: + forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b eq_true_rect_r: forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true -BoolSpec: Prop -> Prop -> bool -> Prop +eq_true_rec_r: + forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true +eq_true_rect: + forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b +bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b +eq_true_ind_r: + forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true +andb_true_intro: + forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true BoolSpec_ind: forall (P Q : Prop) (P0 : bool -> Prop), (P -> P0 true) -> (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b -Nat.eqb: nat -> nat -> bool -Nat.leb: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool -Nat.even: nat -> bool -Nat.odd: nat -> bool -Nat.testbit: nat -> nat -> bool -Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat bool_choice: forall (S : Set) (R1 R2 : S -> Prop), (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} -eq_S: forall x y : nat, x = y -> S x = S y -f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y -f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +mult_n_O: forall n : nat, 0 = n * 0 +plus_O_n: forall n : nat, 0 + n = n +plus_n_O: forall n : nat, n = n + 0 +n_Sn: forall n : nat, n <> S n pred_Sn: forall n : nat, n = Nat.pred (S n) +O_S: forall n : nat, 0 <> S n +f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +eq_S: forall x y : nat, x = y -> S x = S y eq_add_S: forall n m : nat, S n = S m -> n = m +min_r: forall n m : nat, m <= n -> Nat.min n m = m +min_l: forall n m : nat, n <= m -> Nat.min n m = n +max_r: forall n m : nat, n <= m -> Nat.max n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n +plus_Sn_m: forall n m : nat, S n + m = S (n + m) +plus_n_Sm: forall n m : nat, S (n + m) = n + S m +f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y not_eq_S: forall n m : nat, n <> m -> S n <> S m -O_S: forall n : nat, 0 <> S n -n_Sn: forall n : nat, n <> S n +mult_n_Sm: forall n m : nat, n * m + n = n * S m f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 +f_equal2_mult: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 f_equal2_nat: forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat), x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2 -plus_n_O: forall n : nat, n = n + 0 -plus_O_n: forall n : nat, 0 + n = n -plus_n_Sm: forall n m : nat, S (n + m) = n + S m -plus_Sn_m: forall n m : nat, S n + m = S (n + m) -f_equal2_mult: - forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 -mult_n_O: forall n : nat, 0 = n * 0 -mult_n_Sm: forall n m : nat, n * m + n = n * S m -max_l: forall n m : nat, m <= n -> Nat.max n m = n -max_r: forall n m : nat, n <= m -> Nat.max n m = m -min_l: forall n m : nat, n <= m -> Nat.min n m = n -min_r: forall n m : nat, m <= n -> Nat.min n m = m -andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true andb_true_intro: forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true bool_choice: forall (S : Set) (R1 R2 : S -> Prop), (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} -andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true andb_true_intro: forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true -h': newdef n <> n +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true h: n <> newdef n h': newdef n <> n h: n <> newdef n +h': newdef n <> n h: n <> newdef n h: n <> newdef n -h': ~ P n h: P n h': ~ P n h: P n h': ~ P n h: P n +h': ~ P n h: P n h: P n diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out index 0d5924ec61..7038eac22c 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/SearchHead.out @@ -1,39 +1,39 @@ le_n: forall n : nat, n <= n +le_0_n: forall n : nat, 0 <= n le_S: forall n m : nat, n <= m -> n <= S m le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m -le_S_n: forall n m : nat, S n <= S m -> n <= m -le_0_n: forall n : nat, 0 <= n le_n_S: forall n m : nat, n <= m -> S n <= S m -true: bool +le_S_n: forall n m : nat, S n <= S m -> n <= m false: bool -andb: bool -> bool -> bool -orb: bool -> bool -> bool +true: bool +negb: bool -> bool implb: bool -> bool -> bool +orb: bool -> bool -> bool +andb: bool -> bool -> bool xorb: bool -> bool -> bool -negb: bool -> bool -Nat.eqb: nat -> nat -> bool -Nat.leb: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool Nat.even: nat -> bool Nat.odd: nat -> bool +Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool -eq_S: forall x y : nat, x = y -> S x = S y -f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +Nat.eqb: nat -> nat -> bool +mult_n_O: forall n : nat, 0 = n * 0 +plus_O_n: forall n : nat, 0 + n = n +plus_n_O: forall n : nat, n = n + 0 pred_Sn: forall n : nat, n = Nat.pred (S n) +f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y eq_add_S: forall n m : nat, S n = S m -> n = m -f_equal2_plus: - forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 -plus_n_O: forall n : nat, n = n + 0 -plus_O_n: forall n : nat, 0 + n = n +eq_S: forall x y : nat, x = y -> S x = S y +max_r: forall n m : nat, n <= m -> Nat.max n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n +min_r: forall n m : nat, m <= n -> Nat.min n m = m +min_l: forall n m : nat, n <= m -> Nat.min n m = n plus_n_Sm: forall n m : nat, S (n + m) = n + S m plus_Sn_m: forall n m : nat, S n + m = S (n + m) +mult_n_Sm: forall n m : nat, n * m + n = n * S m +f_equal2_plus: + forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 f_equal2_mult: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 -mult_n_O: forall n : nat, 0 = n * 0 -mult_n_Sm: forall n m : nat, n * m + n = n * S m -max_l: forall n m : nat, m <= n -> Nat.max n m = n -max_r: forall n m : nat, n <= m -> Nat.max n m = m -min_l: forall n m : nat, n <= m -> Nat.min n m = n -min_r: forall n m : nat, m <= n -> Nat.min n m = m h: newdef n h: P n diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index f3c12effca..45ff5e73b6 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -1,77 +1,77 @@ -true: bool false: bool -andb: bool -> bool -> bool -orb: bool -> bool -> bool +true: bool +negb: bool -> bool implb: bool -> bool -> bool +orb: bool -> bool -> bool +andb: bool -> bool -> bool xorb: bool -> bool -> bool -negb: bool -> bool -Nat.eqb: nat -> nat -> bool -Nat.leb: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool Nat.even: nat -> bool Nat.odd: nat -> bool +Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool -O: nat -S: nat -> nat -length: forall A : Type, list A -> nat +Nat.eqb: nat -> nat -> bool +Nat.two: nat Nat.zero: nat Nat.one: nat -Nat.two: nat -Nat.succ: nat -> nat +O: nat +Nat.double: nat -> nat +Nat.sqrt: nat -> nat +Nat.div2: nat -> nat +Nat.log2: nat -> nat Nat.pred: nat -> nat +Nat.square: nat -> nat +S: nat -> nat +Nat.succ: nat -> nat +Nat.ldiff: nat -> nat -> nat Nat.add: nat -> nat -> nat -Nat.double: nat -> nat +Nat.lor: nat -> nat -> nat +Nat.lxor: nat -> nat -> nat +Nat.land: nat -> nat -> nat Nat.mul: nat -> nat -> nat Nat.sub: nat -> nat -> nat Nat.max: nat -> nat -> nat -Nat.min: nat -> nat -> nat -Nat.pow: nat -> nat -> nat Nat.div: nat -> nat -> nat +Nat.pow: nat -> nat -> nat +Nat.min: nat -> nat -> nat Nat.modulo: nat -> nat -> nat Nat.gcd: nat -> nat -> nat -Nat.square: nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat -Nat.sqrt: nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat -Nat.log2: nat -> nat -Nat.div2: nat -> nat +length: forall A : Type, list A -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat -Nat.land: nat -> nat -> nat -Nat.lor: nat -> nat -> nat +Nat.div2: nat -> nat +Nat.sqrt: nat -> nat +Nat.log2: nat -> nat +Nat.double: nat -> nat +Nat.pred: nat -> nat +Nat.square: nat -> nat +Nat.succ: nat -> nat +S: nat -> nat Nat.ldiff: nat -> nat -> nat +Nat.pow: nat -> nat -> nat +Nat.land: nat -> nat -> nat Nat.lxor: nat -> nat -> nat -S: nat -> nat -Nat.succ: nat -> nat -Nat.pred: nat -> nat -Nat.add: nat -> nat -> nat -Nat.double: nat -> nat +Nat.div: nat -> nat -> nat Nat.mul: nat -> nat -> nat -Nat.sub: nat -> nat -> nat -Nat.max: nat -> nat -> nat Nat.min: nat -> nat -> nat -Nat.pow: nat -> nat -> nat -Nat.div: nat -> nat -> nat Nat.modulo: nat -> nat -> nat +Nat.sub: nat -> nat -> nat +Nat.lor: nat -> nat -> nat Nat.gcd: nat -> nat -> nat -Nat.square: nat -> nat -Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat -Nat.sqrt: nat -> nat +Nat.max: nat -> nat -> nat +Nat.add: nat -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat -Nat.log2: nat -> nat -Nat.div2: nat -> nat +Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat -Nat.land: nat -> nat -> nat -Nat.lor: nat -> nat -> nat -Nat.ldiff: nat -> nat -> nat -Nat.lxor: nat -> nat -> nat mult_n_Sm: forall n m : nat, n * m + n = n * S m -identity_refl: forall (A : Type) (a : A), identity a a iff_refl: forall A : Prop, A <-> A +le_n: forall n : nat, n <= n +identity_refl: forall (A : Type) (a : A), identity a a eq_refl: forall (A : Type) (x : A), x = x Nat.divmod: nat -> nat -> nat -> nat -> nat * nat -le_n: forall n : nat, n <= n -pair: forall A B : Type, A -> B -> A * B conj: forall A B : Prop, A -> B -> A /\ B +pair: forall A B : Type, A -> B -> A * B Nat.divmod: nat -> nat -> nat -> nat -> nat * nat h: n <> newdef n h: n <> newdef n diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 48fbe0793c..edcd53005e 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -88,9 +88,12 @@ Open Scope type_scope. (** ML Tactic Notations *) +Declare ML Module "ltac_plugin". Declare ML Module "coretactics". Declare ML Module "extratactics". Declare ML Module "g_auto". Declare ML Module "g_class". Declare ML Module "g_eqdecide". Declare ML Module "g_rewrite". + +Global Set Default Proof Mode "Classic". diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index b7dd5f2a14..4842a89151 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -50,9 +50,9 @@ let section s = let lib_dirs = ["kernel"; "lib"; "library"; "parsing"; "pretyping"; "interp"; "printing"; "intf"; - "proofs"; "tactics"; "tools"; "ltacprof"; - "toplevel"; "stm"; "grammar"; "config"; - "ltac"; "engine"] + "proofs"; "tactics"; "tools"; + "vernac"; "stm"; "toplevel"; "grammar"; "config"; + "engine"] let usage () = diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index eaf938e8ce..645b3665e0 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -75,6 +75,7 @@ let std_includes basedir = let rebase d = match basedir with None -> d | Some base -> base / d in ["-I"; rebase "."; "-I"; rebase "lib"; + "-I"; rebase "vernac"; (* For Mltop *) "-I"; rebase "toplevel"; "-I"; rebase "kernel/byterun"; "-I"; Envars.camlp4lib () ] @ diff --git a/tools/gallina-db.el b/tools/gallina-db.el index baabebb13a..9664f69f8b 100644 --- a/tools/gallina-db.el +++ b/tools/gallina-db.el @@ -163,7 +163,7 @@ for DB structure." (defun coq-sort-menu-entries (menu) (sort menu - '(lambda (x y) (string< + (lambda (x y) (string< (downcase (elt x 0)) (downcase (elt y 0)))))) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index d9f8ed8815..cc1c44fe31 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -603,8 +603,6 @@ let init_toplevel arglist = init_gc (); Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) Lib.init(); - (* Default Proofb Mode starts with an alternative default. *) - Goptions.set_string_option_value ["Default";"Proof";"Mode"] "Classic"; begin try let extras = parse_args arglist in diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib index d689223639..10bf486476 100644 --- a/toplevel/toplevel.mllib +++ b/toplevel/toplevel.mllib @@ -1,19 +1,3 @@ -Himsg -ExplainErr -Class -Locality -Metasyntax -Auto_ind_decl -Search -Indschemes -Obligations -Command -Classes -Record -Assumptions -Vernacinterp -Mltop -Vernacentries Vernac Usage Coqloop diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 0e72a044c1..f914f83b9b 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -105,7 +105,7 @@ let verbose_phrase verbch loc = match verbch with | Some ch -> let len = snd loc - fst loc in - let s = String.create len in + let s = Bytes.create len in seek_in ch (fst loc); really_input ch s 0 len; Feedback.msg_notice (str s) @@ -162,7 +162,7 @@ let pr_new_syntax po loc chan_beautify ocom = let pp_cmd_header loc com = let shorten s = try (String.sub s 0 30)^"..." with _ -> s in let noblank s = - for i = 0 to String.length s - 1 do + for i = 0 to Bytes.length s - 1 do match s.[i] with | ' ' | '\n' | '\t' | '\r' -> s.[i] <- '~' | _ -> () @@ -343,7 +343,7 @@ let compile verbosely f = let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in Library.save_library_raw lfdv sum lib univs proofs -let compile v f = +let compile v f = ignore(CoqworkmgrApi.get 1); compile v f; CoqworkmgrApi.giveback 1 diff --git a/toplevel/assumptions.ml b/vernac/assumptions.ml index 8865cd6469..8865cd6469 100644 --- a/toplevel/assumptions.ml +++ b/vernac/assumptions.ml diff --git a/toplevel/assumptions.mli b/vernac/assumptions.mli index 0726757839..0726757839 100644 --- a/toplevel/assumptions.mli +++ b/vernac/assumptions.mli diff --git a/toplevel/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 594f2e9449..594f2e9449 100644 --- a/toplevel/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml diff --git a/toplevel/auto_ind_decl.mli b/vernac/auto_ind_decl.mli index 60232ba8f4..60232ba8f4 100644 --- a/toplevel/auto_ind_decl.mli +++ b/vernac/auto_ind_decl.mli diff --git a/toplevel/class.ml b/vernac/class.ml index 0dc7990143..0dc7990143 100644 --- a/toplevel/class.ml +++ b/vernac/class.ml diff --git a/toplevel/class.mli b/vernac/class.mli index 5f9ae28f62..5f9ae28f62 100644 --- a/toplevel/class.mli +++ b/vernac/class.mli diff --git a/toplevel/classes.ml b/vernac/classes.ml index 6512f3defa..6512f3defa 100644 --- a/toplevel/classes.ml +++ b/vernac/classes.ml diff --git a/toplevel/classes.mli b/vernac/classes.mli index d2cb788eae..d2cb788eae 100644 --- a/toplevel/classes.mli +++ b/vernac/classes.mli diff --git a/toplevel/command.ml b/vernac/command.ml index 049f58aa26..049f58aa26 100644 --- a/toplevel/command.ml +++ b/vernac/command.ml diff --git a/toplevel/command.mli b/vernac/command.mli index 616afb91f0..616afb91f0 100644 --- a/toplevel/command.mli +++ b/vernac/command.mli diff --git a/toplevel/discharge.ml b/vernac/discharge.ml index e24d5e74fb..e24d5e74fb 100644 --- a/toplevel/discharge.ml +++ b/vernac/discharge.ml diff --git a/toplevel/discharge.mli b/vernac/discharge.mli index 18d1b67766..18d1b67766 100644 --- a/toplevel/discharge.mli +++ b/vernac/discharge.mli diff --git a/toplevel/doc.tex b/vernac/doc.tex index f2550fda11..f2550fda11 100644 --- a/toplevel/doc.tex +++ b/vernac/doc.tex diff --git a/toplevel/explainErr.ml b/vernac/explainErr.ml index 17897460c0..17897460c0 100644 --- a/toplevel/explainErr.ml +++ b/vernac/explainErr.ml diff --git a/toplevel/explainErr.mli b/vernac/explainErr.mli index a67c887af3..a67c887af3 100644 --- a/toplevel/explainErr.mli +++ b/vernac/explainErr.mli diff --git a/toplevel/himsg.ml b/vernac/himsg.ml index 6cff805fc2..6cff805fc2 100644 --- a/toplevel/himsg.ml +++ b/vernac/himsg.ml diff --git a/toplevel/himsg.mli b/vernac/himsg.mli index ced54fd279..ced54fd279 100644 --- a/toplevel/himsg.mli +++ b/vernac/himsg.mli diff --git a/toplevel/ind_tables.ml b/vernac/ind_tables.ml index 85d0b6194c..85d0b6194c 100644 --- a/toplevel/ind_tables.ml +++ b/vernac/ind_tables.ml diff --git a/toplevel/ind_tables.mli b/vernac/ind_tables.mli index 20f30d6d16..20f30d6d16 100644 --- a/toplevel/ind_tables.mli +++ b/vernac/ind_tables.mli diff --git a/toplevel/indschemes.ml b/vernac/indschemes.ml index f7e3f0d954..f7e3f0d954 100644 --- a/toplevel/indschemes.ml +++ b/vernac/indschemes.ml diff --git a/toplevel/indschemes.mli b/vernac/indschemes.mli index e5d79fd514..e5d79fd514 100644 --- a/toplevel/indschemes.mli +++ b/vernac/indschemes.mli diff --git a/stm/lemmas.ml b/vernac/lemmas.ml index 55f33be399..55f33be399 100644 --- a/stm/lemmas.ml +++ b/vernac/lemmas.ml diff --git a/stm/lemmas.mli b/vernac/lemmas.mli index 39c089be9f..39c089be9f 100644 --- a/stm/lemmas.mli +++ b/vernac/lemmas.mli diff --git a/toplevel/locality.ml b/vernac/locality.ml index 03640676e6..03640676e6 100644 --- a/toplevel/locality.ml +++ b/vernac/locality.ml diff --git a/toplevel/locality.mli b/vernac/locality.mli index 2ec392eefc..2ec392eefc 100644 --- a/toplevel/locality.mli +++ b/vernac/locality.mli diff --git a/toplevel/metasyntax.ml b/vernac/metasyntax.ml index f28ef3f650..0aaf6afd7e 100644 --- a/toplevel/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -20,10 +20,8 @@ open Extend open Libobject open Constrintern open Vernacexpr -open Pcoq open Libnames open Tok -open Egramcoq open Notation open Nameops @@ -46,7 +44,7 @@ let add_token_obj s = Lib.add_anonymous_leaf (inToken s) let entry_buf = Buffer.create 64 -type any_entry = AnyEntry : 'a Gram.entry -> any_entry +type any_entry = AnyEntry : 'a Pcoq.Gram.entry -> any_entry let grammars : any_entry list String.Map.t ref = ref String.Map.empty @@ -56,7 +54,7 @@ let register_grammar name grams = let pr_entry e = let () = Buffer.clear entry_buf in let ft = Format.formatter_of_buffer entry_buf in - let () = Gram.entry_print ft e in + let () = Pcoq.Gram.entry_print ft e in str (Buffer.contents entry_buf) let pr_registered_grammar name = @@ -65,7 +63,7 @@ let pr_registered_grammar name = | None -> error "Unknown or unprintable grammar entry." | Some entries -> let pr_one (AnyEntry e) = - str "Entry " ++ str (Gram.Entry.name e) ++ str " is" ++ fnl () ++ + str "Entry " ++ str (Pcoq.Gram.Entry.name e) ++ str " is" ++ fnl () ++ pr_entry e in prlist pr_one entries @@ -738,52 +736,74 @@ let inSyntaxExtension : syntax_extension_obj -> obj = (* Interpreting user-provided modifiers *) -let interp_modifiers modl = - let onlyparsing = ref false in - let onlyprinting = ref false in - let compat = ref None in - let rec interp assoc level etyps format extra = function - | [] -> - (assoc,level,etyps,!onlyparsing,!onlyprinting,!compat,format,extra) +(* XXX: We could move this to the parser itself *) +module NotationMods = struct + +type notation_modifier = { + assoc : gram_assoc option; + level : int option; + etyps : (Id.t * simple_constr_prod_entry_key) list; + + (* common to syn_data below *) + only_parsing : bool; + only_printing : bool; + compat : compat_version option; + format : string Loc.located option; + extra : (string * string) list; +} + +let default = { + assoc = None; + level = None; + etyps = []; + only_parsing = false; + only_printing = false; + compat = None; + format = None; + extra = []; +} + +end + +let interp_modifiers modl = let open NotationMods in + let rec interp acc = function + | [] -> acc | SetEntryType (s,typ) :: l -> let id = Id.of_string s in - if Id.List.mem_assoc id etyps then + if Id.List.mem_assoc id acc.etyps then user_err ~hdr:"Metasyntax.interp_modifiers" (str s ++ str " is already assigned to an entry or constr level."); - interp assoc level ((id,typ)::etyps) format extra l + interp { acc with etyps = (id,typ) :: acc.etyps; } l | SetItemLevel ([],n) :: l -> - interp assoc level etyps format extra l + interp acc l | SetItemLevel (s::idl,n) :: l -> let id = Id.of_string s in - if Id.List.mem_assoc id etyps then + if Id.List.mem_assoc id acc.etyps then user_err ~hdr:"Metasyntax.interp_modifiers" (str s ++ str " is already assigned to an entry or constr level."); let typ = ETConstr (n,()) in - interp assoc level ((id,typ)::etyps) format extra (SetItemLevel (idl,n)::l) + interp { acc with etyps = (id,typ)::acc.etyps; } (SetItemLevel (idl,n)::l) | SetLevel n :: l -> - if not (Option.is_empty level) then error "A level is given more than once."; - interp assoc (Some n) etyps format extra l + + interp { acc with level = Some n; } l | SetAssoc a :: l -> - if not (Option.is_empty assoc) then error"An associativity is given more than once."; - interp (Some a) level etyps format extra l - | SetOnlyParsing :: l -> - onlyparsing := true; - interp assoc level etyps format extra l + if not (Option.is_empty acc.assoc) then error "An associativity is given more than once."; + interp { acc with assoc = Some a; } l + | SetOnlyParsing :: l -> + interp { acc with only_parsing = true; } l | SetOnlyPrinting :: l -> - onlyprinting := true; - interp assoc level etyps format extra l + interp { acc with only_printing = true; } l | SetCompatVersion v :: l -> - compat := Some v; - interp assoc level etyps format extra l + interp { acc with compat = Some v; } l | SetFormat ("text",s) :: l -> - if not (Option.is_empty format) then error "A format is given more than once."; - interp assoc level etyps (Some s) extra l + if not (Option.is_empty acc.format) then error "A format is given more than once."; + interp { acc with format = Some s; } l | SetFormat (k,(_,s)) :: l -> - interp assoc level etyps format ((k,s) :: extra) l - in interp None None [] None [] modl + interp { acc with extra = (k,s)::acc.extra; } l + in interp default modl let check_infix_modifiers modifiers = - let (_, _, t, _, _, _, _, _) = interp_modifiers modifiers in + let t = (interp_modifiers modifiers).NotationMods.etyps in if not (List.is_empty t) then error "Explicit entry level or type unexpected in infix notation." @@ -990,18 +1010,59 @@ let remove_curly_brackets l = | x :: l -> x :: aux false l in aux true l +module SynData = struct + + (* XXX: Document *) + type syn_data = { + + (* Notation name and location *) + info : notation * notation_location; + + (* Fields coming from the vernac-level modifiers *) + only_parsing : bool; + only_printing : bool; + compat : compat_version option; + format : string Loc.located option; + extra : (string * string) list; + + (* XXX: Callback to printing, must remove *) + msgs : ((std_ppcmds -> unit) * std_ppcmds) list; + + (* Fields for internalization *) + recvars : (Id.t * Id.t) list; + mainvars : Id.List.elt list; + intern_typs : notation_var_internalization_type list; + + (* Notation data for parsing *) + + level : int; + syntax_data : (Id.t * (production_level, production_position) constr_entry_key_gen) list * (* typs *) + symbol list; (* symbols *) + not_data : notation * (* notation *) + (int * parenRelation) list * (* precedence *) + bool; (* needs_squash *) + } + +end + let compute_syntax_data df modifiers = - let (assoc,n,etyps,onlyparse,onlyprint,compat,fmt,extra) = interp_modifiers modifiers in - let assoc = match assoc with None -> (* default *) Some NonA | a -> a in + let open SynData in + let open NotationMods in + let mods = interp_modifiers modifiers in + let assoc = Option.append mods.assoc (Some NonA) in let toks = split_notation_string df in - let (recvars,mainvars,symbols) = analyze_notation_tokens toks in - let _ = check_useless_entry_types recvars mainvars etyps in + let recvars,mainvars,symbols = analyze_notation_tokens toks in + let _ = check_useless_entry_types recvars mainvars mods.etyps in + + (* Notations for interp and grammar *) let ntn_for_interp = make_notation_key symbols in let symbols' = remove_curly_brackets symbols in - let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in let ntn_for_grammar = make_notation_key symbols' in check_rule_productivity symbols'; - let msgs,n = find_precedence n etyps symbols' in + + (* Misc *) + let need_squash = not (List.equal Notation.symbol_eq symbols symbols') in + let msgs,n = find_precedence mods.level mods.etyps symbols' in let innerlevel = NumLevel 200 in let typs = find_symbols @@ -1010,25 +1071,44 @@ let compute_syntax_data df modifiers = (NumLevel n,BorderProd(Right,assoc)) symbols' in (* To globalize... *) - let etyps = join_auxiliary_recursive_types recvars etyps in + let etyps = join_auxiliary_recursive_types recvars mods.etyps in let sy_typs = List.map (set_entry_type etyps) typs in - let prec = (n,List.map (assoc_of_type n) sy_typs) in + let prec = List.map (assoc_of_type n) sy_typs in let i_typs = set_internalization_type sy_typs in - let sy_data = (n,sy_typs,symbols',fmt) in - let sy_fulldata = (i_typs,ntn_for_grammar,prec,need_squash,sy_data) in + let sy_data = (sy_typs,symbols') in + let sy_fulldata = (ntn_for_grammar,prec,need_squash) in let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in - let i_data = (onlyparse,onlyprint,compat,recvars,mainvars,(ntn_for_interp,df')) in + let i_data = ntn_for_interp, df' in + (* Return relevant data for interpretation and for parsing/printing *) - (msgs,i_data,i_typs,sy_fulldata,extra) + { info = i_data; + + only_parsing = mods.only_parsing; + only_printing = mods.only_printing; + compat = mods.compat; + format = mods.format; + extra = mods.extra; + + msgs; + + recvars; + mainvars; + intern_typs = i_typs; + + level = n; + syntax_data = sy_data; + not_data = sy_fulldata; + } let compute_pure_syntax_data df mods = - let (msgs,(onlyparse,onlyprint,_,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in + let open SynData in + let sd = compute_syntax_data df mods in let msgs = - if onlyparse then + if sd.only_parsing then (Feedback.msg_warning ?loc:None, - strbrk "The only parsing modifier has no effect in Reserved Notation.")::msgs - else msgs in - msgs, sy_data, extra, onlyprint + strbrk "The only parsing modifier has no effect in Reserved Notation.")::sd.msgs + else sd.msgs in + { sd with msgs } (**********************************************************************) (* Registration of notations interpretation *) @@ -1091,7 +1171,7 @@ let with_lib_stk_protection f x = let with_syntax_protection f x = with_lib_stk_protection - (with_grammar_rule_protection + (Pcoq.with_grammar_rule_protection (with_notation_protection f)) x (**********************************************************************) @@ -1145,10 +1225,10 @@ let recover_notation_syntax rawntn = (**********************************************************************) (* Main entry point for building parsing and printing rules *) -let make_pa_rule i_typs (n,typs,symbols,_) ntn onlyprint = +let make_pa_rule i_typs level (typs,symbols) ntn onlyprint = let assoc = recompute_assoc typs in let prod = make_production typs symbols in - { notgram_level = n; + { notgram_level = level; notgram_assoc = assoc; notgram_notation = ntn; notgram_prods = prod; @@ -1156,21 +1236,23 @@ let make_pa_rule i_typs (n,typs,symbols,_) ntn onlyprint = notgram_onlyprinting = onlyprint; } -let make_pp_rule (n,typs,symbols,fmt) = +let make_pp_rule level (typs,symbols) fmt = match fmt with - | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)] - | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt) - -let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint compat = - let pa_rule = make_pa_rule i_typs sy_data ntn onlyprint in - let pp_rule = make_pp_rule sy_data in + | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols level)] + | Some fmt -> hunks_of_format (level, List.split typs) (symbols, parse_format fmt) + +(* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *) +let make_syntax_rules (sd : SynData.syn_data) = let open SynData in + let ntn, prec, need_squash = sd.not_data in + let pa_rule = make_pa_rule sd.intern_typs sd.level sd.syntax_data ntn sd.only_printing in + let pp_rule = make_pp_rule sd.level sd.syntax_data sd.format in let sy = { - synext_level = prec; + synext_level = (sd.level, prec); synext_notation = ntn; - synext_notgram = pa_rule; + synext_notgram = pa_rule; synext_unparsing = pp_rule; - synext_extra = extra; - synext_compat = compat; + synext_extra = sd.extra; + synext_compat = sd.compat; } in (* By construction, the rule for "{ _ }" is declared, but we need to redeclare it because the file where it is declared needs not be open @@ -1185,39 +1267,39 @@ let to_map l = List.fold_left fold Id.Map.empty l let add_notation_in_scope local df c mods scope = - let (msgs,i_data,i_typs,sy_data,extra) = compute_syntax_data df mods in + let open SynData in + let sd = compute_syntax_data df mods in (* Prepare the interpretation *) - let (onlyparse, onlyprint, compat, recvars,mainvars, df') = i_data in (* Prepare the parsing and printing rules *) - let sy_rules = make_syntax_rules sy_data extra onlyprint compat in - let i_vars = make_internalization_vars recvars mainvars i_typs in + let sy_rules = make_syntax_rules sd in + let i_vars = make_internalization_vars sd.recvars sd.mainvars sd.intern_typs in let nenv = { ninterp_var_type = to_map i_vars; - ninterp_rec_vars = to_map recvars; + ninterp_rec_vars = to_map sd.recvars; } in let (acvars, ac, reversible) = interp_notation_constr nenv c in - let interp = make_interpretation_vars recvars acvars in + let interp = make_interpretation_vars sd.recvars acvars in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in - let onlyparse = is_not_printable onlyparse (not reversible) ac in + let onlyparse = is_not_printable sd.only_parsing (not reversible) ac in let notation = { notobj_local = local; notobj_scope = scope; notobj_interp = (List.map_filter map i_vars, ac); (** Order is important here! *) notobj_onlyparse = onlyparse; - notobj_onlyprint = onlyprint; - notobj_compat = compat; - notobj_notation = df'; + notobj_onlyprint = sd.only_printing; + notobj_compat = sd.compat; + notobj_notation = sd.info; } in (* Ready to change the global state *) - Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs; + Flags.if_verbose (List.iter (fun (f,x) -> f x)) sd.msgs; Lib.add_anonymous_leaf (inSyntaxExtension (local, sy_rules)); Lib.add_anonymous_leaf (inNotation notation); - df' + sd.info let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat = let dfs = split_notation_string df in - let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in + let recvars,mainvars,symbs = analyze_notation_tokens dfs in (* Recover types of variables and pa/pp rules; redeclare them if needed *) let i_typs, onlyprint = if not (is_numeral symbs) then begin let i_typs,sy_rules,onlyprint' = recover_notation_syntax (make_notation_key symbs) in @@ -1227,8 +1309,8 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) i_typs, onlyprint end else [], false in (* Declare interpretation *) - let path = (Lib.library_dp(),Lib.current_dirpath true) in - let df' = (make_notation_key symbs,(path,df)) in + let path = (Lib.library_dp(), Lib.current_dirpath true) in + let df' = (make_notation_key symbs, (path,df)) in let i_vars = make_internalization_vars recvars mainvars i_typs in let nenv = { ninterp_var_type = to_map i_vars; @@ -1253,10 +1335,10 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env) (* Notations without interpretation (Reserved Notation) *) -let add_syntax_extension local ((loc,df),mods) = - let msgs, sy_data, extra, onlyprint = compute_pure_syntax_data df mods in - let sy_rules = make_syntax_rules sy_data extra onlyprint None in - Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs; +let add_syntax_extension local ((loc,df),mods) = let open SynData in + let psd = compute_pure_syntax_data df mods in + let sy_rules = make_syntax_rules {psd with compat = None} in + Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs; Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules)) (* Notations with only interpretation *) @@ -1385,4 +1467,3 @@ let add_syntactic_definition ident (vars,c) local onlyparse = | p -> p in Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat) - diff --git a/toplevel/metasyntax.mli b/vernac/metasyntax.mli index 57c1204022..57c1204022 100644 --- a/toplevel/metasyntax.mli +++ b/vernac/metasyntax.mli diff --git a/toplevel/mltop.ml b/vernac/mltop.ml index 2396cf04a4..2396cf04a4 100644 --- a/toplevel/mltop.ml +++ b/vernac/mltop.ml diff --git a/toplevel/mltop.mli b/vernac/mltop.mli index 6633cb9372..6633cb9372 100644 --- a/toplevel/mltop.mli +++ b/vernac/mltop.mli diff --git a/toplevel/obligations.ml b/vernac/obligations.ml index 9ada043171..6f3921903b 100644 --- a/toplevel/obligations.ml +++ b/vernac/obligations.ml @@ -25,6 +25,8 @@ module NamedDecl = Context.Named.Declaration let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false) let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false) +let get_fix_exn, stm_get_fix_exn = Hook.make () + let succfix (depth, fixrels) = (succ depth, List.map succ fixrels) @@ -485,7 +487,7 @@ let declare_definition prg = let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None) (Evd.evar_universe_context_subst prg.prg_ctx) in let opaque = prg.prg_opaque in - let fix_exn = Stm.get_fix_exn () in + let fix_exn = Hook.get get_fix_exn () in let pl, ctx = Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) in let ce = @@ -566,7 +568,7 @@ let declare_mutual_definition l = in (* Declare the recursive definitions *) let ctx = Evd.evar_context_universe_context first.prg_ctx in - let fix_exn = Stm.get_fix_exn () in + let fix_exn = Hook.get get_fix_exn () in let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx) fixnames fixdecls fixtypes fiximps in (* Declare notations *) diff --git a/toplevel/obligations.mli b/vernac/obligations.mli index 80b6891447..11366fe91b 100644 --- a/toplevel/obligations.mli +++ b/vernac/obligations.mli @@ -24,6 +24,12 @@ val declare_definition_ref : Safe_typing.private_constants Entries.definition_entry -> Impargs.manual_implicits -> global_reference Lemmas.declaration_hook -> global_reference) ref +(* This is a hack to make it possible for Obligations to craft a Qed + * behind the scenes. The fix_exn the Stm attaches to the Future proof + * is not available here, so we provide a side channel to get it *) +val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t + + val check_evars : env -> evar_map -> unit val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t diff --git a/toplevel/record.ml b/vernac/record.ml index d5faafaf89..b494430c28 100644 --- a/toplevel/record.ml +++ b/vernac/record.ml @@ -110,7 +110,8 @@ let typecheck_params_and_fields def id pl t ps nots fs = List.iter (function LocalRawDef (b, _) -> error default_binder_kind b | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls - | LocalPattern _ -> assert false) ps + | LocalPattern (loc,_,_) -> + Loc.raise ~loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps in let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in let t', template = match t with diff --git a/toplevel/record.mli b/vernac/record.mli index c50e577860..c50e577860 100644 --- a/toplevel/record.mli +++ b/vernac/record.mli diff --git a/toplevel/search.ml b/vernac/search.ml index d319b24199..e1b56b1319 100644 --- a/toplevel/search.ml +++ b/vernac/search.ml @@ -107,6 +107,72 @@ let generic_search glnumopt fn = | Some glnum -> iter_hypothesis glnum fn); iter_declarations fn +(** This module defines a preference on constrs in the form of a + [compare] function (preferred constr must be big for this + functions, so preferences such as small constr must use a reversed + order). This priority will be used to order search results and + propose first results which are more likely to be relevant to the + query, this is why the type [t] contains the other elements + required of a search. *) +module ConstrPriority = struct + + (* The priority is memoised here. Because of the very localised use + of this module, it is not worth it making a convenient interface. *) + type t = + Globnames.global_reference * Environ.env * Constr.t * priority + and priority = int + + module ConstrSet = CSet.Make(Constr) + + (** A measure of the size of a term *) + let rec size t = + Constr.fold (fun s t -> 1 + s + size t) 0 t + + (** Set of the "symbols" (definitions, inductives, constructors) + which appear in a term. *) + let rec symbols acc t = + let open Constr in + match kind t with + | Const _ | Ind _ | Construct _ -> ConstrSet.add t acc + | _ -> Constr.fold symbols acc t + + (** The number of distinct "symbols" (see {!symbols}) which appear + in a term. *) + let num_symbols t = + ConstrSet.(cardinal (symbols empty t)) + + let priority t : priority = + -(3*(num_symbols t) + size t) + + let compare (_,_,_,p1) (_,_,_,p2) = + compare p1 p2 +end + +module PriorityQueue = Heap.Functional(ConstrPriority) + +let rec iter_priority_queue q fn = + (* use an option to make the function tail recursive. Will be + obsoleted with Ocaml 4.02 with the [match … with | exception …] + syntax. *) + let next = begin + try Some (PriorityQueue.maximum q) + with Heap.EmptyHeap -> None + end in + match next with + | Some (gref,env,t,_) -> + fn gref env t; + iter_priority_queue (PriorityQueue.remove q) fn + | None -> () + +let prioritize_search seq fn = + let acc = ref PriorityQueue.empty in + let iter gref env t = + let p = ConstrPriority.priority t in + acc := PriorityQueue.add (gref,env,t,p) !acc + in + let () = seq iter in + iter_priority_queue !acc fn + (** Filters *) (** This function tries to see whether the conclusion matches a pattern. *) diff --git a/toplevel/search.mli b/vernac/search.mli index ba3d48efcc..c9167c485d 100644 --- a/toplevel/search.mli +++ b/vernac/search.mli @@ -74,3 +74,11 @@ val interface_search : ?glnum:int -> (search_constraint * bool) list -> val generic_search : int option -> display_function -> unit (** This function iterates over all hypothesis of the goal numbered [glnum] (if present) and all known declarations. *) + +(** {6 Search function modifiers} *) + +val prioritize_search : (display_function -> unit) -> display_function -> unit +(** [prioritize_search iter] iterates over the values of [iter] (seen + as a sequence of declarations), in a relevance order. This requires to + perform the entire iteration of [iter] before starting streaming. So + [prioritize_search] should not be used for low-latency streaming. *) diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib new file mode 100644 index 0000000000..94ef54f70f --- /dev/null +++ b/vernac/vernac.mllib @@ -0,0 +1,17 @@ +Lemmas +Himsg +ExplainErr +Class +Locality +Metasyntax +Auto_ind_decl +Search +Indschemes +Obligations +Command +Classes +Record +Assumptions +Vernacinterp +Mltop +Vernacentries diff --git a/toplevel/vernacentries.ml b/vernac/vernacentries.ml index a2f2ded327..8b7d654572 100644 --- a/toplevel/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -165,7 +165,7 @@ let show_match id = let print_path_entry p = let dir = pr_dirpath (Loadpath.logical p) in let path = str (Loadpath.physical p) in - (dir ++ str " " ++ tbrk (0, 0) ++ path) + Pp.hov 2 (dir ++ spc () ++ path) let print_loadpath dir = let l = Loadpath.get_load_paths () in @@ -175,9 +175,8 @@ let print_loadpath dir = let filter p = is_dirpath_prefix_of dir (Loadpath.logical p) in List.filter filter l in - Pp.t (str "Logical Path: " ++ - tab () ++ str "Physical path:" ++ fnl () ++ - prlist_with_sep fnl print_path_entry l) + str "Logical Path / Physical path:" ++ fnl () ++ + prlist_with_sep fnl print_path_entry l let print_modules () = let opened = Library.opened_libraries () @@ -515,11 +514,8 @@ let vernac_start_proof locality p kind l lettop = let qed_display_script = ref true let vernac_end_proof ?proof = function - | Admitted -> save_proof ?proof Admitted - | Proved (_,_) as e -> - if is_verbose () && !qed_display_script && !Flags.coqtop_ui then - Stm.show_script ?proof (); - save_proof ?proof e + | Admitted -> save_proof ?proof Admitted + | Proved (_,_) as e -> save_proof ?proof e (* A stupid macro that should be replaced by ``Exact c. Save.'' all along the theories [??] *) @@ -1787,13 +1783,13 @@ let vernac_search s gopt r = in match s with | SearchPattern c -> - Search.search_pattern gopt (get_pattern c) r pr_search + (Search.search_pattern gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchRewrite c -> - Search.search_rewrite gopt (get_pattern c) r pr_search + (Search.search_rewrite gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchHead c -> - Search.search_by_head gopt (get_pattern c) r pr_search + (Search.search_by_head gopt (get_pattern c) r |> Search.prioritize_search) pr_search | SearchAbout sl -> - Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r pr_search + (Search.search_about gopt (List.map (on_snd (interp_search_about_item env)) sl) r |> Search.prioritize_search) pr_search let vernac_locate = let open Feedback in function | LocateAny (AN qid) -> msg_notice (print_located_qualid qid) @@ -1868,6 +1864,7 @@ let vernac_bullet (bullet:Proof_global.Bullet.t) = Proof_global.Bullet.put p bullet) let vernac_show = let open Feedback in function + | ShowScript -> assert false (* Only the stm knows the script *) | ShowGoal goalref -> let info = match goalref with | OpenSubgoals -> pr_open_subgoals () @@ -1882,7 +1879,6 @@ let vernac_show = let open Feedback in function Constrextern.with_implicits msg_notice (pr_nth_open_subgoal n) | ShowProof -> show_proof () | ShowNode -> show_node () - | ShowScript -> Stm.show_script () | ShowExistentials -> show_top_evars () | ShowUniverses -> show_universes () | ShowTree -> show_prooftree () @@ -1909,6 +1905,12 @@ let vernac_check_guard () = exception End_of_input +(* XXX: This won't properly set the proof mode, as of today, it is + controlled by the STM. Thus, we would need access information from + the classifier. The proper fix is to move it to the STM, however, + the way the proof mode is set there makes the task non trivial + without a considerable amount of refactoring. + *) let vernac_load interp fname = let interp x = let proof_mode = Proof_global.get_default_proof_mode_name () in @@ -1936,16 +1938,45 @@ let vernac_load interp fname = let interp ?proof ~loc locality poly c = prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); match c with - (* Done later in this file *) + (* The below vernac are candidates for removal from the main type + and to be put into a new doc_command datatype: *) + | VernacLoad _ -> assert false + + (* Done later in this file *) | VernacFail _ -> assert false | VernacTime _ -> assert false | VernacRedirect _ -> assert false | VernacTimeout _ -> assert false | VernacStm _ -> assert false + (* The STM should handle that, but LOAD bypasses the STM... *) + | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command") + | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command") + | VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command") + | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command") + | VernacBacktrack _ -> CErrors.user_err (str "Backtrack cannot be used through the Load command") + + (* Toplevel control *) + | VernacToplevelControl e -> raise e + + (* Resetting *) + | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm") + | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm") + | VernacBack _ -> anomaly (str "VernacBack not handled by Stm") + | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm") + + (* Horrible Hack that should die. *) | VernacError e -> raise e + (* This one is possible to handle here *) + | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") + + (* Handled elsewhere *) + | VernacProgram _ + | VernacPolymorphic _ + | VernacLocal _ -> assert false + (* Syntax *) | VernacSyntaxExtension (local,sl) -> vernac_syntax_extension locality local sl @@ -2017,12 +2048,6 @@ let interp ?proof ~loc locality poly c = | VernacWriteState s -> vernac_write_state s | VernacRestoreState s -> vernac_restore_state s - (* Resetting *) - | VernacResetName _ -> anomaly (str "VernacResetName not handled by Stm") - | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm") - | VernacBack _ -> anomaly (str "VernacBack not handled by Stm") - | VernacBackTo _ -> anomaly (str "VernacBackTo not handled by Stm") - (* Commands *) | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb locality dbname b | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints locality dbnames ids @@ -2054,14 +2079,6 @@ let interp ?proof ~loc locality poly c = | VernacRegister (id, r) -> vernac_register id r | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n") - (* The STM should handle that, but LOAD bypasses the STM... *) - | VernacAbort id -> CErrors.user_err (str "Abort cannot be used through the Load command") - | VernacAbortAll -> CErrors.user_err (str "AbortAll cannot be used through the Load command") - | VernacRestart -> CErrors.user_err (str "Restart cannot be used through the Load command") - | VernacUndo _ -> CErrors.user_err (str "Undo cannot be used through the Load command") - | VernacUndoTo _ -> CErrors.user_err (str "UndoTo cannot be used through the Load command") - | VernacBacktrack _ -> CErrors.user_err (str "Backtrack cannot be used through the Load command") - (* Proof management *) | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false | VernacFocus n -> vernac_focus n @@ -2084,17 +2101,10 @@ let interp ?proof ~loc locality poly c = Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:yes"; vernac_set_end_tac tac; vernac_set_used_variables l | VernacProofMode mn -> Proof_global.set_proof_mode mn - (* Toplevel control *) - | VernacToplevelControl e -> raise e (* Extensions *) | VernacExtend (opn,args) -> Vernacinterp.call ?locality (opn,args) - (* Handled elsewhere *) - | VernacProgram _ - | VernacPolymorphic _ - | VernacLocal _ -> assert false - (* Vernaculars that take a locality flag *) let check_vernac_supports_locality c l = match l, c with @@ -2253,6 +2263,3 @@ let interp ?(verbosely=true) ?proof (loc,c) = in if verbosely then Flags.verbosely (aux false) c else aux false c - -let () = Hook.set Stm.interp_hook interp -let () = Hook.set Stm.with_fail_hook with_fail diff --git a/toplevel/vernacentries.mli b/vernac/vernacentries.mli index 7cdc8dd064..7cdc8dd064 100644 --- a/toplevel/vernacentries.mli +++ b/vernac/vernacentries.mli diff --git a/toplevel/vernacinterp.ml b/vernac/vernacinterp.ml index f26ef460dd..f26ef460dd 100644 --- a/toplevel/vernacinterp.ml +++ b/vernac/vernacinterp.ml diff --git a/toplevel/vernacinterp.mli b/vernac/vernacinterp.mli index 5149b5416d..5149b5416d 100644 --- a/toplevel/vernacinterp.mli +++ b/vernac/vernacinterp.mli |