From c215c4429a85a6d73cc1a33041258cacbe4de199 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 16 Dec 2008 13:56:19 +0000 Subject: Take advantage of natdynlink when available: almost all contribs become loadable plugins - Any contrib foo leads to contrib/foo/foo_plugin.cmxs (and .cma for bytecode). - Features that were available without any Require are now loaded systematically when launching coqtop (see Coqtop.load_initial_plugins): extraction, jprover, cc, ground, dp, recdef, xml - The other plugins are loaded when a corresponding Require is done: quote, ring, field, setoid_ring, omega, romega, micromega, fourier - I experienced a crash (segfault) while turning subtac into a plugin, so this one stays statically linked into coqtop for now - When the ocaml version doesn't support natdynlink, or if "-natdynlink no" is explicitely given to configure, coqtop is statically linked with all of the above code as usual. Some messages [Ignore ML file Foo_plugin] may appear. - How should coqdep handle a "Declare ML Module "foo"" if foo is an archive and not a ml file ? For now, we suppose that the foo.{cmxs,cma} are at the same location as the .v during the build, but can be moved later in any place of the ml loadpath. This is clearly an experimentation. Feedback most welcome... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11687 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile | 4 +- Makefile.build | 176 +++++++------- Makefile.common | 61 +++-- configure | 12 +- contrib/field/LegacyField.v | 1 + contrib/fourier/Fourier.v | 10 +- contrib/micromega/Psatz.v | 1 + contrib/micromega/QMicromega.v | 1 + contrib/micromega/RMicromega.v | 1 + contrib/micromega/ZMicromega.v | 1 + contrib/omega/Omega.v | 1 + contrib/omega/OmegaPlugin.v | 11 + contrib/quote/Quote.v | 87 +++++++ contrib/quote/g_quote.ml4 | 18 ++ contrib/quote/quote.ml | 491 ++++++++++++++++++++++++++++++++++++++++ contrib/ring/LegacyRing.v | 1 + contrib/ring/Quote.v | 85 ------- contrib/ring/Setoid_ring.v | 3 +- contrib/ring/g_quote.ml4 | 18 -- contrib/ring/quote.ml | 491 ---------------------------------------- contrib/ring/ring.ml | 2 +- contrib/romega/ROmega.v | 2 + contrib/rtauto/Rtauto.v | 2 + contrib/setoid_ring/Ring_base.v | 3 +- contrib/setoid_ring/Ring_tac.v | 3 +- theories/Reals/Rlogic.v | 2 +- tools/coqdep.ml | 15 +- toplevel/coqtop.ml | 17 +- toplevel/mltop.ml4 | 20 +- 29 files changed, 817 insertions(+), 723 deletions(-) create mode 100644 contrib/omega/OmegaPlugin.v create mode 100644 contrib/quote/Quote.v create mode 100644 contrib/quote/g_quote.ml4 create mode 100644 contrib/quote/quote.ml delete mode 100644 contrib/ring/Quote.v delete mode 100644 contrib/ring/g_quote.ml4 delete mode 100644 contrib/ring/quote.ml diff --git a/Makefile b/Makefile index c8b885902c..0eaf689dd8 100644 --- a/Makefile +++ b/Makefile @@ -118,7 +118,7 @@ else stage1 $(STAGE1_TARGETS): always $(call stage-template,1) -CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.dep.ps %.dot +CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot ifdef CM_STAGE1 $(CAML_OBJECT_PATTERNS): always $(call stage-template,1) @@ -189,7 +189,7 @@ archclean: clean-ide cleantheories rm -f $(COQTOPEXE) $(COQMKTOP) $(COQC) $(CHICKEN) rm -f $(COQTOPOPT) $(COQMKTOPOPT) $(COQCOPT) $(CHICKENOPT) rm -f bin/coq-parser.opt$(EXE) bin/coq-interface.opt$(EXE) - find . -name '*.cmx' -or -name '*.cmxa' -or -name '*.[soa]' -or -name '*.so' | xargs rm -f + find . -name '*.cmx' -or -name '*.cmxs' -or -name '*.cmxa' -or -name '*.[soa]' -or -name '*.so' | xargs rm -f rm -f $(TOOLS) $(CSDPCERT) clean-ide: diff --git a/Makefile.build b/Makefile.build index bba84709bd..61d4944835 100644 --- a/Makefile.build +++ b/Makefile.build @@ -67,6 +67,7 @@ LOCALINCLUDES=-I config -I tools -I tools/coqdoc \ -I proofs -I tactics -I pretyping \ -I interp -I toplevel -I parsing -I ide/utils -I ide \ -I contrib/omega -I contrib/romega -I contrib/micromega \ + -I contrib/quote \ -I contrib/ring -I contrib/dp -I contrib/setoid_ring \ -I contrib/xml -I contrib/extraction \ -I contrib/interface -I contrib/fourier \ @@ -168,12 +169,14 @@ coqbinaries:: ${COQBINARIES} ${CSDPCERT} coq: coqlib tools coqbinaries -coqlib:: theories contrib +coqlib:: initplugins theories contrib -coqlight: theories-light tools coqbinaries +coqlight: initplugins theories-light tools coqbinaries states:: states/initial.coq +initplugins: $(INITPLUGINSOPT) $(INITPLUGINS) + $(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ @@ -193,12 +196,12 @@ CHKOPTFLAGS:=$(CHKLIBS) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) $(CHICKENOPT): checker/check.cmxa checker/main.ml $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ unix.cmxa gramlib.cmxa checker/check.cmxa checker/main.ml + $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ unix.cmxa gramlib.cmxa $^ $(STRIP) $@ $(CHICKENBYTE): checker/check.cma checker/main.ml $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ unix.cma gramlib.cma checker/check.cma checker/main.ml + $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ unix.cma gramlib.cma $^ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE) @@ -207,13 +210,11 @@ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN) $(COQMKTOPBYTE): $(COQMKTOPCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma \ - $(COQMKTOPCMO) $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $^ $(OSDEPLIBS) $(COQMKTOPOPT): $(COQMKTOPCMX) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa \ - $(COQMKTOPCMX) $(OSDEPLIBS) + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa $^ $(OSDEPLIBS) $(STRIP) $@ $(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP) @@ -258,108 +259,109 @@ hightactics: $(HIGHTACTICS) # target for libraries lib/lib.cma: $(LIBREP) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(LIBREP) - lib/lib.cmxa: $(LIBREP:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(LIBREP:.cmo=.cmx) kernel/kernel.cma: $(KERNEL) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(KERNEL) - kernel/kernel.cmxa: $(KERNEL:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(KERNEL:.cmo=.cmx) - -checker/check.cma: $(MCHECKER) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -a -o $@ $(MCHECKER) - -checker/check.cmxa: $(MCHECKER:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -a -o $@ $(MCHECKER:.cmo=.cmx) library/library.cma: $(LIBRARY) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(LIBRARY) - library/library.cmxa: $(LIBRARY:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(LIBRARY:.cmo=.cmx) pretyping/pretyping.cma: $(PRETYPING) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(PRETYPING) - pretyping/pretyping.cmxa: $(PRETYPING:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(PRETYPING:.cmo=.cmx) interp/interp.cma: $(INTERP) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(INTERP) - interp/interp.cmxa: $(INTERP:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(INTERP:.cmo=.cmx) parsing/parsing.cma: $(PARSING) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(PARSING) - parsing/parsing.cmxa: $(PARSING:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(PARSING:.cmo=.cmx) proofs/proofs.cma: $(PROOFS) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(PROOFS) - proofs/proofs.cmxa: $(PROOFS:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(PROOFS:.cmo=.cmx) tactics/tactics.cma: $(TACTICS) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(TACTICS) - tactics/tactics.cmxa: $(TACTICS:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(TACTICS:.cmo=.cmx) toplevel/toplevel.cma: $(TOPLEVEL) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(TOPLEVEL) - toplevel/toplevel.cmxa: $(TOPLEVEL:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(TOPLEVEL:.cmo=.cmx) parsing/highparsing.cma: $(HIGHPARSING) - $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(HIGHPARSING) - parsing/highparsing.cmxa: $(HIGHPARSING:.cmo=.cmx) - $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHPARSING:.cmo=.cmx) tactics/hightactics.cma: $(HIGHTACTICS) +tactics/hightactics.cmxa: $(HIGHTACTICS:.cmo=.cmx) + +contrib/contrib.cma: $(CONTRIBSTATIC) +contrib/contrib.cmxa: $(CONTRIBSTATIC:.cmo=.cmx) + +$(OMEGACMA): $(OMEGACMO) +$(OMEGACMA:.cma=.cmxa): $(OMEGACMO:.cmo=.cmx) + +$(ROMEGACMA): $(ROMEGACMO) +$(ROMEGACMA:.cma=.cmxa): $(ROMEGACMO:.cmo=.cmx) + +$(MICROMEGACMA): $(MICROMEGACMO) +$(MICROMEGACMA:.cma=.cmxa): $(MICROMEGACMO:.cmo=.cmx) + +$(QUOTACMA): $(QUOTECMO) +$(QUOTECMA:.cma=.cmxa): $(QUOTECMO:.cmo=.cmx) + +$(RINGCMA): $(RINGCMO) +$(RINGCMA:.cma=.cmxa): $(RINGCMO:.cmo=.cmx) + +$(NEWRINGCMA): $(NEWRINGCMO) +$(NEWRINGCMA:.cma=.cmxa): $(NEWRINGCMO:.cmo=.cmx) + +$(FIELDCMA): $(FIELDCMO) +$(FIELDCMA:.cma=.cmxa): $(FIELDCMO:.cmo=.cmx) + +$(XMLCMA): $(XMLCMO) +$(XMLCMA:.cma=.cmxa): $(XMLCMO:.cmo=.cmx) + +$(FOURIERCMA): $(FOURIERCMO) +$(FOURIERCMA:.cma=.cmxa): $(FOURIERCMO:.cmo=.cmx) + +$(EXTRACTIONCMA): $(EXTRACTIONCMO) +$(EXTRACTIONCMA:.cma=.cmxa): $(EXTRACTIONCMO:.cmo=.cmx) + +$(RTAUTOCMA): $(RTAUTOCMO) +$(RTAUTOCMA:.cma=.cmxa): $(RTAUTOCMO:.cmo=.cmx) + +$(JPROVERCMA): $(JPROVERCMO) +$(JPROVERCMA:.cma=.cmxa): $(JPROVERCMO:.cmo=.cmx) + +$(FOCMA): $(FOCMO) +$(FOCMA:.cma=.cmxa): $(FOCMO:.cmo=.cmx) + +$(CCCMA): $(CCCMO) +$(CCCMA:.cma=.cmxa): $(CCCMO:.cmo=.cmx) + +$(DPCMA): $(DPCMO) +$(DPCMA:.cma=.cmxa): $(DPCMO:.cmo=.cmx) + +$(FUNINDCMA): $(FUNINDCMO) +$(FUNINDCMA:.cma=.cmxa): $(FUNINDCMO:.cmo=.cmx) + +$(SUBTACCMA): $(SUBTACCMO) +$(SUBTACCMA:.cma=.cmxa): $(SUBTACCMO:.cmo=.cmx) + +%.cma: $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(HIGHTACTICS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $^ -tactics/hightactics.cmxa: $(HIGHTACTICS:.cmo=.cmx) +%.cmxa: $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(HIGHTACTICS:.cmo=.cmx) + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $^ -contrib/contrib.cma: $(CONTRIB) +# For the checker, different flags may be used + +checker/check.cma: $(MCHECKER) $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(CONTRIB) + $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -a -o $@ $^ -contrib/contrib.cmxa: $(CONTRIB:.cmo=.cmx) +checker/check.cmxa: $(MCHECKER:.cmo=.cmx) $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(CONTRIB:.cmo=.cmx) + $(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -a -o $@ $^ ########################################################################### # Csdp to micromega special targets @@ -368,12 +370,12 @@ contrib/contrib.cmxa: $(CONTRIB:.cmo=.cmx) ifeq ($(BEST),opt) contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMX) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa -o $@ $(CSDPCERTCMX) + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) nums.cmxa -o $@ $^ $(STRIP) $@ else contrib/micromega/csdpcert$(EXE): $(CSDPCERTCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma -o $@ $(CSDPCERTCMO) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) nums.cma -o $@ $^ endif ########################################################################### @@ -421,11 +423,11 @@ ide/%.cmx: ide/%.ml | ide/%.ml.d ide/ide.cma: $(COQIDECMO) $(SHOW)'OCAMLC -a -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $(COQIDECMO) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -a -o $@ $^ ide/ide.cmxa: $(COQIDECMO:.cmo=.cmx) $(SHOW)'OCAMLOPT -a -o $@' - $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $(COQIDECMO:.cmo=.cmx) + $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -a -o $@ $^ # install targets @@ -551,7 +553,7 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \ # contribs (interface not included) ########################################################################### -contrib: $(CONTRIBVO) $(CONTRIBCMO) +contrib: $(CONTRIBVO) omega: $(OMEGAVO) $(OMEGACMO) $(ROMEGAVO) $(ROMEGACMO) micromega: $(MICROMEGAVO) $(MICROMEGACMO) $(CSDPCERT) ring: $(RINGVO) $(RINGCMO) @@ -575,7 +577,7 @@ states/initial.coq: states/MakeInitial.v $(INITVO) $(VO_TOOLS_STRICT) | states/M $(SHOW)'BUILD $@' $(HIDE)$(BOOTCOQTOP) -batch -notop -silent -nois -load-vernac-source states/MakeInitial.v -outputstate states/initial.coq -theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY) +theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY) $(SHOW)'COQC -nois $<' $(HIDE)rm -f theories/Init/$*.glob $(HIDE)$(BOOTCOQTOP) -nois -compile theories/Init/$* @@ -593,27 +595,27 @@ tools:: $(TOOLS) $(DEBUGPRINTERS) $(COQDEP): $(COQDEPCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQDEPCMO) $(OSDEPLIBS) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $^ $(OSDEPLIBS) $(GALLINA): $(GALLINACMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(GALLINACMO) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $^ -$(COQMAKEFILE): tools/coq_makefile.cmo config/coq_config.cmo +$(COQMAKEFILE): config/coq_config.cmo tools/coq_makefile.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma $^ $(COQTEX): tools/coq-tex.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma tools/coq-tex.cmo + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma $^ $(COQWC): tools/coqwc.cmo $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ tools/coqwc.cmo + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $^ $(COQDOC): $(COQDOCCMO) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $(COQDOCCMO) + $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $^ ########################################################################### # Installation @@ -730,7 +732,7 @@ dev/printers.cma: $(PRINTERSCMO) $(HIDE)$(OCAMLC) $(BYTEFLAGS) gramlib.cma $(PRINTERSCMO) -o test-printer @rm -f test-printer $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(PRINTERSCMO) -linkall -a -o $@ + $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ parsing/grammar.cma: $(GRAMMARCMO) $(SHOW)'Testing $@' diff --git a/Makefile.common b/Makefile.common index 4ca7e2e45b..63740d086a 100644 --- a/Makefile.common +++ b/Makefile.common @@ -234,33 +234,42 @@ HIGHTACTICS:=\ tactics/extratactics.cmo tactics/eauto.cmo tactics/class_tactics.cmo \ tactics/tauto.cmo tactics/eqdecide.cmo +OMEGACMA:=contrib/omega/omega_plugin.cma OMEGACMO:=\ contrib/omega/omega.cmo contrib/omega/coq_omega.cmo \ contrib/omega/g_omega.cmo +ROMEGACMA:=contrib/romega/romega_plugin.cma ROMEGACMO:=\ contrib/romega/const_omega.cmo \ contrib/romega/refl_omega.cmo contrib/romega/g_romega.cmo +MICROMEGACMA:=contrib/micromega/micromega_plugin.cma MICROMEGACMO:=\ contrib/micromega/mutils.cmo \ contrib/micromega/micromega.cmo contrib/micromega/mfourier.cmo \ contrib/micromega/certificate.cmo \ contrib/micromega/coq_micromega.cmo contrib/micromega/g_micromega.cmo +QUOTECMA:=contrib/quote/quote_plugin.cma +QUOTECMO:=\ + contrib/quote/quote.cmo contrib/quote/g_quote.cmo + +RINGCMA:=contrib/ring/ring_plugin.cma RINGCMO:=\ - contrib/ring/quote.cmo contrib/ring/g_quote.cmo \ contrib/ring/ring.cmo contrib/ring/g_ring.cmo -NEWRINGCMO:=\ - contrib/setoid_ring/newring.cmo +NEWRINGCMA:=contrib/setoid_ring/newring_plugin.cma +NEWRINGCMO:=contrib/setoid_ring/newring.cmo +DPCMA:=contrib/dp/dp_plugin.cma DPCMO:=contrib/dp/dp_why.cmo contrib/dp/dp_zenon.cmo \ contrib/dp/dp.cmo contrib/dp/dp_gappa.cmo contrib/dp/g_dp.cmo -FIELDCMO:=\ - contrib/field/field.cmo +FIELDCMO:=contrib/field/field.cmo +FIELDCMA:=contrib/field/field_plugin.cma +XMLCMA:=contrib/xml/xml_plugin.cma XMLCMO:=\ contrib/xml/unshare.cmo contrib/xml/xml.cmo contrib/xml/acic.cmo \ contrib/xml/doubleTypeInference.cmo \ @@ -270,10 +279,12 @@ XMLCMO:=\ contrib/xml/xmlentries.cmo contrib/xml/cic2Xml.cmo \ contrib/xml/dumptree.cmo +FOURIERCMA:=contrib/fourier/fourier_plugin.cma FOURIERCMO:=\ contrib/fourier/fourier.cmo contrib/fourier/fourierR.cmo \ contrib/fourier/g_fourier.cmo +EXTRACTIONCMA:=contrib/extraction/extraction_plugin.cma EXTRACTIONCMO:=\ contrib/extraction/table.cmo\ contrib/extraction/mlutil.cmo\ @@ -286,12 +297,14 @@ EXTRACTIONCMO:=\ contrib/extraction/extract_env.cmo \ contrib/extraction/g_extraction.cmo +JPROVERCMA:=contrib/jprover/jprover_plugin.cma JPROVERCMO:=\ contrib/jprover/opname.cmo \ contrib/jprover/jterm.cmo contrib/jprover/jlogic.cmo \ contrib/jprover/jtunify.cmo contrib/jprover/jall.cmo \ contrib/jprover/jprover.cmo +FUNINDCMA:=contrib/funind/recdef_plugin.cma FUNINDCMO:=\ contrib/funind/indfun_common.cmo contrib/funind/rawtermops.cmo \ contrib/funind/recdef.cmo \ @@ -301,15 +314,18 @@ FUNINDCMO:=\ contrib/funind/invfun.cmo contrib/funind/indfun.cmo \ contrib/funind/merge.cmo contrib/funind/g_indfun.cmo +FOCMA:=contrib/firstorder/ground_plugin.cma FOCMO:=\ contrib/firstorder/formula.cmo contrib/firstorder/unify.cmo \ contrib/firstorder/sequent.cmo contrib/firstorder/rules.cmo \ contrib/firstorder/instances.cmo contrib/firstorder/ground.cmo \ contrib/firstorder/g_ground.cmo +CCCMA:=contrib/cc/cc_plugin.cma CCCMO:=contrib/cc/ccalgo.cmo contrib/cc/ccproof.cmo contrib/cc/cctac.cmo \ contrib/cc/g_congruence.cmo +SUBTACCMA:=contrib/subtac/subtac_plugin.cma SUBTACCMO:=contrib/subtac/subtac_utils.cmo contrib/subtac/eterm.cmo \ contrib/subtac/g_eterm.cmo \ contrib/subtac/subtac_errors.cmo contrib/subtac/subtac_coercion.cmo \ @@ -319,14 +335,28 @@ SUBTACCMO:=contrib/subtac/subtac_utils.cmo contrib/subtac/eterm.cmo \ contrib/subtac/subtac.cmo contrib/subtac/g_subtac.cmo \ contrib/subtac/equations.cmo +RTAUTOCMA:=contrib/rtauto/rtauto_plugin.cma RTAUTOCMO:=contrib/rtauto/proof_search.cmo contrib/rtauto/refl_tauto.cmo \ contrib/rtauto/g_rtauto.cmo -CONTRIB:=$(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \ - $(RINGCMO) $(NEWRINGCMO) $(DPCMO) $(FIELDCMO) \ - $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ - $(CCCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \ - $(FUNINDCMO) +CONTRIBSTATIC:=\ + $(OMEGACMO) $(ROMEGACMO) $(MICROMEGACMO) \ + $(QUOTECMO) $(RINGCMO) $(NEWRINGCMO) $(DPCMO) $(FIELDCMO) \ + $(FOURIERCMO) $(EXTRACTIONCMO) $(JPROVERCMO) $(XMLCMO) \ + $(CCCMO) $(FOCMO) $(SUBTACCMO) $(RTAUTOCMO) \ + $(FUNINDCMO) + +ifeq ($(HASNATDYNLINK),true) + CONTRIBSTATIC:=$(SUBTACCMO) + INITPLUGINS:=$(EXTRACTIONCMA) $(JPROVERCMA) $(FOCMA) $(CCCMA) $(DPCMA) \ + $(XMLCMA) $(FUNINDCMA) #$(SUBTACCMA) + INITPLUGINSOPT:=$(INITPLUGINS:.cma=.cmxs) + ifeq ($(BEST),opt) + INITPLUGINSBEST:=$(INITPLUGINSOPT) + else + INITPLUGINSBEST:=$(INITPLUGINS) + endif +endif CMA:=$(CLIBS) $(CAMLP4OBJS) CMXA:=$(CMA:.cma=.cmxa) @@ -346,7 +376,7 @@ LINKCMX:=$(LINKCMOCMXA:.cmo=.cmx) # objects known by the toplevel of Coq OBJSCMO:=$(CONFIG) $(LIBREP) $(KERNEL) $(LIBRARY) $(PRETYPING) $(INTERP) \ $(PROOFS) $(PARSING) $(TACTICS) $(TOPLEVEL) $(HIGHPARSING) \ - $(HIGHTACTICS) $(CONTRIB) + $(HIGHTACTICS) $(CONTRIBSTATIC) COQIDECMO:=ide/utils/okey.cmo ide/utils/config_file.cmo \ ide/utils/configwin_keys.cmo ide/utils/configwin_types.cmo \ @@ -753,7 +783,7 @@ THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO) ## Contribs OMEGAVO:=$(addprefix contrib/omega/, \ - PreOmega.vo OmegaLemmas.vo Omega.vo ) + PreOmega.vo OmegaLemmas.vo OmegaPlugin.vo Omega.vo ) ROMEGAVO:=$(addprefix contrib/romega/, \ ReflOmegaCore.vo ROmega.vo ) @@ -767,12 +797,15 @@ MICROMEGAVO:=$(addprefix contrib/micromega/, \ QMicromega.vo RMicromega.vo \ Tauto.vo ) +QUOTEVO:=$(addprefix contrib/quote/, \ + Quote.vo ) + RINGVO:=$(addprefix contrib/ring/, \ LegacyArithRing.vo Ring_normalize.vo \ LegacyRing_theory.vo LegacyRing.vo \ LegacyNArithRing.vo \ LegacyZArithRing.vo Ring_abstract.vo \ - Quote.vo Setoid_ring_normalize.vo \ + Setoid_ring_normalize.vo \ Setoid_ring.vo Setoid_ring_theory.vo ) FIELDVO:=$(addprefix contrib/field/, \ @@ -811,7 +844,7 @@ RTAUTOVO:=$(addprefix contrib/rtauto/, \ CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \ $(XMLVO) $(FOURIERVO) $(JPROVERVO) $(CCVO) $(FUNINDVO) \ - $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO) + $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO) VFILES:= $(ALLVO:.vo=.v) diff --git a/configure b/configure index a64f561481..b9e6f9ea8f 100755 --- a/configure +++ b/configure @@ -59,6 +59,8 @@ usage () { printf "\tSpecifies the architecture\n" echo "-opt" printf "\tSpecifies whether or not to generate optimized executables\n" + echo "-natdynlink (yes|no)" + printf "\tSpecifies whether or not to use dynamic loading of native code\n" echo "-fsets (all|basic)" echo "-reals (all|basic)" printf "\tSpecifies whether or not to compile full FSets/Reals library\n" @@ -104,6 +106,7 @@ coq_profile_flag= coq_annotate_flag= best_compiler=opt cflags="-fno-defer-pop -Wall -Wno-unused" +natdynlink=yes gcc_exec=gcc ar_exec=ar @@ -186,6 +189,11 @@ while : ; do -opt|--opt) bytecamlc=ocamlc.opt camlp4oexec=camlp4o # can't add .opt since dyn load'll be required nativecamlc=ocamlopt.opt;; + -natdynlink|--natdynlink) case "$2" in + yes) natdynlink=yes;; + *) natdynlink=no + esac + shift;; -fsets|--fsets) case "$2" in yes|all) fsets=all;; *) fsets=basic @@ -212,7 +220,7 @@ while : ; do esac shift;; -with-geoproof|--with-geoproof) - case $2 in + case "$2" in yes) with_geoproof=true;; no) with_geoproof=false;; esac @@ -442,7 +450,7 @@ if [ "$coq_debug_flag" = "-g" ]; then fi # Native dynlink -if test -f `"$CAMLC" -where`/dynlink.cmxa; then +if [ "$natdynlink" = "yes" -a -f `"$CAMLC" -where`/dynlink.cmxa ]; then HASNATDYNLINK=true else HASNATDYNLINK=false diff --git a/contrib/field/LegacyField.v b/contrib/field/LegacyField.v index ee1ddd477b..efa53b4e9d 100644 --- a/contrib/field/LegacyField.v +++ b/contrib/field/LegacyField.v @@ -11,5 +11,6 @@ Require Export LegacyField_Compl. Require Export LegacyField_Theory. Require Export LegacyField_Tactic. +Declare ML Module "field_plugin". (* Command declarations are moved to the ML side *) diff --git a/contrib/fourier/Fourier.v b/contrib/fourier/Fourier.v index ac1592beea..07b2973a4a 100644 --- a/contrib/fourier/Fourier.v +++ b/contrib/fourier/Fourier.v @@ -10,15 +10,11 @@ (* "Fourier's method to solve linear inequations/equations systems.".*) -Declare ML Module "quote". -Declare ML Module "ring". -Declare ML Module "fourier". -Declare ML Module "fourierR". -Declare ML Module "field". - -Require Export Fourier_util. +Require Export LegacyRing. Require Export LegacyField. Require Export DiscrR. +Require Export Fourier_util. +Declare ML Module "fourier_plugin". Ltac fourier := abstract (fourierz; field; discrR). diff --git a/contrib/micromega/Psatz.v b/contrib/micromega/Psatz.v index b2dd99100c..a3be562077 100644 --- a/contrib/micromega/Psatz.v +++ b/contrib/micromega/Psatz.v @@ -22,6 +22,7 @@ Require Import Raxioms. Require Export RingMicromega. Require Import VarMap. Require Tauto. +Declare ML Module "micromega_plugin". Ltac xpsatz dom d := let tac := lazymatch dom with diff --git a/contrib/micromega/QMicromega.v b/contrib/micromega/QMicromega.v index c054f218aa..f02209459f 100644 --- a/contrib/micromega/QMicromega.v +++ b/contrib/micromega/QMicromega.v @@ -17,6 +17,7 @@ Require Import RingMicromega. Require Import Refl. Require Import QArith. Require Import Qfield. +Declare ML Module "micromega_plugin". Lemma Qsor : SOR 0 1 Qplus Qmult Qminus Qopp Qeq Qle Qlt. Proof. diff --git a/contrib/micromega/RMicromega.v b/contrib/micromega/RMicromega.v index 7c6969c2f2..70786a0571 100644 --- a/contrib/micromega/RMicromega.v +++ b/contrib/micromega/RMicromega.v @@ -17,6 +17,7 @@ Require Import RingMicromega. Require Import Refl. Require Import Raxioms RIneq Rpow_def DiscrR. Require Setoid. +Declare ML Module "micromega_plugin". Definition Rsrt : ring_theory R0 R1 Rplus Rmult Rminus Ropp (@eq R). Proof. diff --git a/contrib/micromega/ZMicromega.v b/contrib/micromega/ZMicromega.v index 0855925a3d..1da3228a98 100644 --- a/contrib/micromega/ZMicromega.v +++ b/contrib/micromega/ZMicromega.v @@ -19,6 +19,7 @@ Require Import Refl. Require Import ZArith. Require Import List. Require Import Bool. +Declare ML Module "micromega_plugin". Ltac flatten_bool := repeat match goal with diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v index 3b427162e8..30b9457183 100644 --- a/contrib/omega/Omega.v +++ b/contrib/omega/Omega.v @@ -19,6 +19,7 @@ Require Export ZArith_base. Require Export OmegaLemmas. Require Export PreOmega. +Declare ML Module "omega_plugin". Hint Resolve Zle_refl Zplus_comm Zplus_assoc Zmult_comm Zmult_assoc Zplus_0_l Zplus_0_r Zmult_1_l Zplus_opp_l Zplus_opp_r Zmult_plus_distr_l diff --git a/contrib/omega/OmegaPlugin.v b/contrib/omega/OmegaPlugin.v new file mode 100644 index 0000000000..21535f0d3b --- /dev/null +++ b/contrib/omega/OmegaPlugin.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* bool + index_eq_prop: (n,m:index)(index_eq n m)=true -> n=m + index_lt : index -> bool + varmap : Type -> Type. + varmap_find : (A:Type)A -> index -> (varmap A) -> A. + + The first arg. of varmap_find is the default value to take + if the object is not found in the varmap. + + index_lt defines a total well-founded order, but we don't prove that. + +***********************************************************************) + +Set Implicit Arguments. +Unset Boxed Definitions. + +Section variables_map. + +Variable A : Type. + +Inductive varmap : Type := + | Empty_vm : varmap + | Node_vm : A -> varmap -> varmap -> varmap. + +Inductive index : Set := + | Left_idx : index -> index + | Right_idx : index -> index + | End_idx : index. + +Fixpoint varmap_find (default_value:A) (i:index) (v:varmap) {struct v} : A := + match i, v with + | End_idx, Node_vm x _ _ => x + | Right_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v2 + | Left_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v1 + | _, _ => default_value + end. + +Fixpoint index_eq (n m:index) {struct m} : bool := + match n, m with + | End_idx, End_idx => true + | Left_idx n', Left_idx m' => index_eq n' m' + | Right_idx n', Right_idx m' => index_eq n' m' + | _, _ => false + end. + +Fixpoint index_lt (n m:index) {struct m} : bool := + match n, m with + | End_idx, Left_idx _ => true + | End_idx, Right_idx _ => true + | Left_idx n', Right_idx m' => true + | Right_idx n', Right_idx m' => index_lt n' m' + | Left_idx n', Left_idx m' => index_lt n' m' + | _, _ => false + end. + +Lemma index_eq_prop : forall n m:index, index_eq n m = true -> n = m. + simple induction n; simple induction m; simpl in |- *; intros. + rewrite (H i0 H1); reflexivity. + discriminate. + discriminate. + discriminate. + rewrite (H i0 H1); reflexivity. + discriminate. + discriminate. + discriminate. + reflexivity. +Qed. + +End variables_map. + +Unset Implicit Arguments. diff --git a/contrib/quote/g_quote.ml4 b/contrib/quote/g_quote.ml4 new file mode 100644 index 0000000000..808cbbf274 --- /dev/null +++ b/contrib/quote/g_quote.ml4 @@ -0,0 +1,18 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* [ quote f [] ] +| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ] +END diff --git a/contrib/quote/quote.ml b/contrib/quote/quote.ml new file mode 100644 index 0000000000..9141dc2f52 --- /dev/null +++ b/contrib/quote/quote.ml @@ -0,0 +1,491 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (varmap A L) -> A}. + + Then, the tactic \texttt{Quote f} will replace an + expression \texttt{e} of type \texttt{A} by \texttt{(f vm t)} + such that \texttt{e} and \texttt{(f vm t)} are convertible. + + The problem is then inverting the function f. + + The tactic works when: + + \begin{itemize} + \item L is a simple inductive datatype. The constructors of L may + have one of the three following forms: + + \begin{enumerate} + \item ordinary recursive constructors like: \verb|Cplus : L -> L -> L| + \item variable leaf like: \verb|Cvar : index -> L| + \item constant leaf like \verb|Cconst : A -> L| + \end{enumerate} + + The definition of \texttt{L} must contain at most one variable + leaf and at most one constant leaf. + + When there are both a variable leaf and a constant leaf, there is + an ambiguity on inversion. The term t can be either the + interpretation of \texttt{(Cconst t)} or the interpretation of + (\texttt{Cvar}~$i$) in a variables map containing the binding $i + \rightarrow$~\texttt{t}. How to discriminate between these + choices ? + + To solve the dilemma, one gives to \texttt{Quote} a list of + \emph{constant constructors}: a term will be considered as a + constant if it is either a constant constructor of the + application of a constant constructor to constants. For example + the list \verb+[S, O]+ defines the closed natural + numbers. \texttt{(S (S O))} is a constant when \texttt{(S x)} is + not. + + The definition of constants vary for each application of the + tactic, so it can even be different for two applications of + \texttt{Quote} with the same function. + + \item \texttt{f} is a quite simple fixpoint on + \texttt{L}. In particular, \texttt{f} must verify: + +\begin{verbatim} + (f (Cvar i)) = (varmap_find vm default_value i) +\end{verbatim} +\begin{verbatim} + (f (Cconst c)) = c +\end{verbatim} + + where \texttt{index} and \texttt{varmap\_find} are those defined + the \texttt{Quote} module. \emph{The tactic won't work with + user's own variables map !!} It is mandatory to use the + variables map defined in module \texttt{Quote}. + + \end{itemize} + + The method to proceed is then clear: + + \begin{itemize} + \item Start with an empty hashtable of "registed leafs" + that map constr to integers and a "variable counter" equal to 0. + \item Try to match the term with every right hand side of the + definition of f. + + If there is one match, returns the correponding left hand + side and call yourself recursively to get the arguments of this + left hand side. + + If there is no match, we are at a leaf. That is the + interpretation of either a variable or a constant. + + If it is a constant, return \texttt{Cconst} applied to that + constant. + + If not, it is a variable. Look in the hashtable + if this leaf has been already encountered. If not, increment + the variables counter and add an entry to the hashtable; then + return \texttt{(Cvar !variables\_counter)} + \end{itemize} +*) + + +(*i*) +open Pp +open Util +open Names +open Term +open Pattern +open Matching +open Tacmach +open Tactics +open Proof_trees +open Tacexpr +(*i*) + +(*s First, we need to access some Coq constants + We do that lazily, because this code can be linked before + the constants are loaded in the environment *) + +let constant dir s = Coqlib.gen_constant "Quote" ("quote"::dir) s + +let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm") +let coq_Node_vm = lazy (constant ["Quote"] "Node_vm") +let coq_varmap_find = lazy (constant ["Quote"] "varmap_find") +let coq_Right_idx = lazy (constant ["Quote"] "Right_idx") +let coq_Left_idx = lazy (constant ["Quote"] "Left_idx") +let coq_End_idx = lazy (constant ["Quote"] "End_idx") + +(*s Then comes the stuff to decompose the body of interpetation function + and pre-compute the inversion data. + +For a function like: + +\begin{verbatim} + Fixpoint interp[vm:(varmap Prop); f:form] := + Cases f of + | (f_and f1 f1 f2) => (interp f1)/\(interp f2) + | (f_or f1 f1 f2) => (interp f1)\/(interp f2) + | (f_var i) => (varmap_find Prop default_v i vm) + | (f_const c) => c +\end{verbatim} + +With the constant constructors \texttt{C1}, \dots, \texttt{Cn}, the +corresponding scheme will be: + +\begin{verbatim} + {normal_lhs_rhs = + [ "(f_and ?1 ?2)", "?1 /\ ?2"; + "(f_or ?1 ?2)", " ?1 \/ ?2";]; + return_type = "Prop"; + constants = Some [C1,...Cn]; + variable_lhs = Some "(f_var ?1)"; + constant_lhs = Some "(f_const ?1)" + } +\end{verbatim} + +If there is no constructor for variables in the type \texttt{form}, +then [variable_lhs] is [None]. Idem for constants and +[constant_lhs]. Both cannot be equal to [None]. + +The metas in the RHS must correspond to those in the LHS (one cannot +exchange ?1 and ?2 in the example above) + +*) + +module ConstrSet = Set.Make( + struct + type t = constr + let compare = (Pervasives.compare : t->t->int) + end) + +type inversion_scheme = { + normal_lhs_rhs : (constr * constr_pattern) list; + variable_lhs : constr option; + return_type : constr; + constants : ConstrSet.t; + constant_lhs : constr option } + +(*s [compute_ivs gl f cs] computes the inversion scheme associated to + [f:constr] with constants list [cs:constr list] in the context of + goal [gl]. This function uses the auxiliary functions + [i_can't_do_that], [decomp_term], [compute_lhs] and [compute_rhs]. *) + +let i_can't_do_that () = error "Quote: not a simple fixpoint" + +let decomp_term c = kind_of_term (strip_outer_cast c) + +(*s [compute_lhs typ i nargsi] builds the term \texttt{(C ?nargsi ... + ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive + type [typ] *) + +let coerce_meta_out id = + let s = string_of_id id in + int_of_string (String.sub s 1 (String.length s - 1)) +let coerce_meta_in n = + id_of_string ("M" ^ string_of_int n) + +let compute_lhs typ i nargsi = + match kind_of_term typ with + | Ind(sp,0) -> + let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in + mkApp (mkConstruct ((sp,0),i+1), argsi) + | _ -> i_can't_do_that () + +(*s This function builds the pattern from the RHS. Recursive calls are + replaced by meta-variables ?i corresponding to those in the LHS *) + +let compute_rhs bodyi index_of_f = + let rec aux c = + match kind_of_term c with + | App (j, args) when j = mkRel (index_of_f) (* recursive call *) -> + let i = destRel (array_last args) in + PMeta (Some (coerce_meta_in i)) + | App (f,args) -> + PApp (pattern_of_constr f, Array.map aux args) + | Cast (c,_,_) -> aux c + | _ -> pattern_of_constr c + in + aux bodyi + +(*s Now the function [compute_ivs] itself *) + +let compute_ivs gl f cs = + let cst = try destConst f with _ -> i_can't_do_that () in + let body = Environ.constant_value (Global.env()) cst in + match decomp_term body with + | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) -> + let (args3, body3) = decompose_lam body2 in + let nargs3 = List.length args3 in + begin match decomp_term body3 with + | Case(_,p,c,lci) -> (*

Case c of c1 ... cn end *) + let n_lhs_rhs = ref [] + and v_lhs = ref (None : constr option) + and c_lhs = ref (None : constr option) in + Array.iteri + (fun i ci -> + let argsi, bodyi = decompose_lam ci in + let nargsi = List.length argsi in + (* REL (narg3 + nargsi + 1) is f *) + (* REL nargsi+1 to REL nargsi + nargs3 are arguments of f *) + (* REL 1 to REL nargsi are argsi (reverse order) *) + (* First we test if the RHS is the RHS for constants *) + if bodyi = mkRel 1 then + c_lhs := Some (compute_lhs (snd (List.hd args3)) + i nargsi) + (* Then we test if the RHS is the RHS for variables *) + else begin match decompose_app bodyi with + | vmf, [_; _; a3; a4 ] + when isRel a3 & isRel a4 & + pf_conv_x gl vmf + (Lazy.force coq_varmap_find)-> + v_lhs := Some (compute_lhs + (snd (List.hd args3)) + i nargsi) + (* Third case: this is a normal LHS-RHS *) + | _ -> + n_lhs_rhs := + (compute_lhs (snd (List.hd args3)) i nargsi, + compute_rhs bodyi (nargs3 + nargsi + 1)) + :: !n_lhs_rhs + end) + lci; + + if !c_lhs = None & !v_lhs = None then i_can't_do_that (); + + (* The Cases predicate is a lambda; we assume no dependency *) + let p = match kind_of_term p with + | Lambda (_,_,p) -> Termops.pop p + | _ -> p + in + + { normal_lhs_rhs = List.rev !n_lhs_rhs; + variable_lhs = !v_lhs; + return_type = p; + constants = List.fold_right ConstrSet.add cs ConstrSet.empty; + constant_lhs = !c_lhs } + + | _ -> i_can't_do_that () + end + |_ -> i_can't_do_that () + +(* TODO for that function: +\begin{itemize} +\item handle the case where the return type is an argument of the + function +\item handle the case of simple mutual inductive (for example terms + and lists of terms) formulas with the corresponding mutual + recursvive interpretation functions. +\end{itemize} +*) + +(*s Stuff to build variables map, currently implemented as complete +binary search trees (see file \texttt{Quote.v}) *) + +(* First the function to distinghish between constants (closed terms) + and variables (open terms) *) + +let rec closed_under cset t = + (ConstrSet.mem t cset) or + (match (kind_of_term t) with + | Cast(c,_,_) -> closed_under cset c + | App(f,l) -> closed_under cset f && array_for_all (closed_under cset) l + | _ -> false) + +(*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete + binary search tree containing the [ci], that is: + +\begin{verbatim} + c1 + / \ + c2 c3 + / \ + c4 c5 +\end{verbatim} + +The second argument is a constr (the common type of the [ci]) +*) + +let btree_of_array a ty = + let size_of_a = Array.length a in + let semi_size_of_a = size_of_a lsr 1 in + let node = Lazy.force coq_Node_vm + and empty = mkApp (Lazy.force coq_Empty_vm, [| ty |]) in + let rec aux n = + if n > size_of_a + then empty + else if n > semi_size_of_a + then mkApp (node, [| ty; a.(n-1); empty; empty |]) + else mkApp (node, [| ty; a.(n-1); aux (2*n); aux (2*n+1) |]) + in + aux 1 + +(*s [btree_of_array] and [path_of_int] verify the following invariant:\\ + {\tt (varmap\_find A dv }[(path_of_int n)] [(btree_of_array a ty)] + = [a.(n)]\\ + [n] must be [> 0] *) + +let path_of_int n = + (* returns the list of digits of n in reverse order with + initial 1 removed *) + let rec digits_of_int n = + if n=1 then [] + else (n mod 2 = 1)::(digits_of_int (n lsr 1)) + in + List.fold_right + (fun b c -> mkApp ((if b then Lazy.force coq_Right_idx + else Lazy.force coq_Left_idx), + [| c |])) + (List.rev (digits_of_int n)) + (Lazy.force coq_End_idx) + +(*s The tactic works with a list of subterms sharing the same + variables map. We need to sort terms in order to avoid than + strange things happen during replacement of terms by their + 'abstract' counterparties. *) + +(* [subterm t t'] tests if constr [t'] occurs in [t] *) +(* This function does not descend under binders (lambda and Cases) *) + +let rec subterm gl (t : constr) (t' : constr) = + (pf_conv_x gl t t') or + (match (kind_of_term t) with + | App (f,args) -> array_exists (fun t -> subterm gl t t') args + | Cast(t,_,_) -> (subterm gl t t') + | _ -> false) + +(*s We want to sort the list according to reverse subterm order. *) +(* Since it's a partial order the algoritm of Sort.list won't work !! *) + +let rec sort_subterm gl l = + let rec insert c = function + | [] -> [c] + | (h::t as l) when c = h -> l (* Avoid doing the same work twice *) + | h::t -> if subterm gl c h then c::h::t else h::(insert c t) + in + match l with + | [] -> [] + | h::t -> insert h (sort_subterm gl t) + +(*s Now we are able to do the inversion itself. + We destructurate the term and use an imperative hashtable + to store leafs that are already encountered. + The type of arguments is:\\ + [ivs : inversion_scheme]\\ + [lc: constr list]\\ + [gl: goal sigma]\\ *) + +let quote_terms ivs lc gl = + Coqlib.check_required_library ["Coq";"quote";"Quote"]; + let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in + let varlist = ref ([] : constr list) in (* list of variables *) + let counter = ref 1 in (* number of variables created + 1 *) + let rec aux c = + let rec auxl l = + match l with + | (lhs, rhs)::tail -> + begin try + let s1 = matches rhs c in + let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux c_i)) s1 + in + Termops.subst_meta s2 lhs + with PatternMatchingFailure -> auxl tail + end + | [] -> + begin match ivs.variable_lhs with + | None -> + begin match ivs.constant_lhs with + | Some c_lhs -> Termops.subst_meta [1, c] c_lhs + | None -> anomaly "invalid inversion scheme for quote" + end + | Some var_lhs -> + begin match ivs.constant_lhs with + | Some c_lhs when closed_under ivs.constants c -> + Termops.subst_meta [1, c] c_lhs + | _ -> + begin + try Hashtbl.find varhash c + with Not_found -> + let newvar = + Termops.subst_meta [1, (path_of_int !counter)] + var_lhs in + begin + incr counter; + varlist := c :: !varlist; + Hashtbl.add varhash c newvar; + newvar + end + end + end + end + in + auxl ivs.normal_lhs_rhs + in + let lp = List.map aux lc in + (lp, (btree_of_array (Array.of_list (List.rev !varlist)) + ivs.return_type )) + +(*s actually we could "quote" a list of terms instead of the + conclusion of current goal. Ring for example needs that, but Ring doesn't + uses Quote yet. *) + +let quote f lid gl = + let f = pf_global gl f in + let cl = List.map (pf_global gl) lid in + let ivs = compute_ivs gl f cl in + let (p, vm) = match quote_terms ivs [(pf_concl gl)] gl with + | [p], vm -> (p,vm) + | _ -> assert false + in + match ivs.variable_lhs with + | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl + | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl + +(*i + +Just testing ... + +#use "include.ml";; +open Quote;; + +let r = raw_constr_of_string;; + +let ivs = { + normal_lhs_rhs = + [ r "(f_and ?1 ?2)", r "?1/\?2"; + r "(f_not ?1)", r "~?1"]; + variable_lhs = Some (r "(f_atom ?1)"); + return_type = r "Prop"; + constants = ConstrSet.empty; + constant_lhs = (r "nat") +};; + +let t1 = r "True/\(True /\ ~False)";; +let t2 = r "True/\~~False";; + +quote_term ivs () t1;; +quote_term ivs () t2;; + +let ivs2 = + normal_lhs_rhs = + [ r "(f_and ?1 ?2)", r "?1/\?2"; + r "(f_not ?1)", r "~?1" + r "True", r "f_true"]; + variable_lhs = Some (r "(f_atom ?1)"); + return_type = r "Prop"; + constants = ConstrSet.empty; + constant_lhs = (r "nat") + +i*) diff --git a/contrib/ring/LegacyRing.v b/contrib/ring/LegacyRing.v index ed1da9c56e..4ae85baf37 100644 --- a/contrib/ring/LegacyRing.v +++ b/contrib/ring/LegacyRing.v @@ -13,6 +13,7 @@ Require Export LegacyRing_theory. Require Export Quote. Require Export Ring_normalize. Require Export Ring_abstract. +Declare ML Module "ring_plugin". (* As an example, we provide an instantation for bool. *) (* Other instatiations are given in ArithRing and ZArithRing in the diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v deleted file mode 100644 index 9a11a70b9c..0000000000 --- a/contrib/ring/Quote.v +++ /dev/null @@ -1,85 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* bool - index_eq_prop: (n,m:index)(index_eq n m)=true -> n=m - index_lt : index -> bool - varmap : Type -> Type. - varmap_find : (A:Type)A -> index -> (varmap A) -> A. - - The first arg. of varmap_find is the default value to take - if the object is not found in the varmap. - - index_lt defines a total well-founded order, but we don't prove that. - -***********************************************************************) - -Set Implicit Arguments. -Unset Boxed Definitions. - -Section variables_map. - -Variable A : Type. - -Inductive varmap : Type := - | Empty_vm : varmap - | Node_vm : A -> varmap -> varmap -> varmap. - -Inductive index : Set := - | Left_idx : index -> index - | Right_idx : index -> index - | End_idx : index. - -Fixpoint varmap_find (default_value:A) (i:index) (v:varmap) {struct v} : A := - match i, v with - | End_idx, Node_vm x _ _ => x - | Right_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v2 - | Left_idx i1, Node_vm x v1 v2 => varmap_find default_value i1 v1 - | _, _ => default_value - end. - -Fixpoint index_eq (n m:index) {struct m} : bool := - match n, m with - | End_idx, End_idx => true - | Left_idx n', Left_idx m' => index_eq n' m' - | Right_idx n', Right_idx m' => index_eq n' m' - | _, _ => false - end. - -Fixpoint index_lt (n m:index) {struct m} : bool := - match n, m with - | End_idx, Left_idx _ => true - | End_idx, Right_idx _ => true - | Left_idx n', Right_idx m' => true - | Right_idx n', Right_idx m' => index_lt n' m' - | Left_idx n', Left_idx m' => index_lt n' m' - | _, _ => false - end. - -Lemma index_eq_prop : forall n m:index, index_eq n m = true -> n = m. - simple induction n; simple induction m; simpl in |- *; intros. - rewrite (H i0 H1); reflexivity. - discriminate. - discriminate. - discriminate. - rewrite (H i0 H1); reflexivity. - discriminate. - discriminate. - discriminate. - reflexivity. -Qed. - -End variables_map. - -Unset Implicit Arguments. diff --git a/contrib/ring/Setoid_ring.v b/contrib/ring/Setoid_ring.v index b5cd6b1d0c..93b9bc7cf5 100644 --- a/contrib/ring/Setoid_ring.v +++ b/contrib/ring/Setoid_ring.v @@ -10,4 +10,5 @@ Require Export Setoid_ring_theory. Require Export Quote. -Require Export Setoid_ring_normalize. \ No newline at end of file +Require Export Setoid_ring_normalize. +Declare ML Module "ring_plugin". diff --git a/contrib/ring/g_quote.ml4 b/contrib/ring/g_quote.ml4 deleted file mode 100644 index 808cbbf274..0000000000 --- a/contrib/ring/g_quote.ml4 +++ /dev/null @@ -1,18 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* [ quote f [] ] -| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ] -END diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml deleted file mode 100644 index 3b13283e13..0000000000 --- a/contrib/ring/quote.ml +++ /dev/null @@ -1,491 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* (varmap A L) -> A}. - - Then, the tactic \texttt{Quote f} will replace an - expression \texttt{e} of type \texttt{A} by \texttt{(f vm t)} - such that \texttt{e} and \texttt{(f vm t)} are convertible. - - The problem is then inverting the function f. - - The tactic works when: - - \begin{itemize} - \item L is a simple inductive datatype. The constructors of L may - have one of the three following forms: - - \begin{enumerate} - \item ordinary recursive constructors like: \verb|Cplus : L -> L -> L| - \item variable leaf like: \verb|Cvar : index -> L| - \item constant leaf like \verb|Cconst : A -> L| - \end{enumerate} - - The definition of \texttt{L} must contain at most one variable - leaf and at most one constant leaf. - - When there are both a variable leaf and a constant leaf, there is - an ambiguity on inversion. The term t can be either the - interpretation of \texttt{(Cconst t)} or the interpretation of - (\texttt{Cvar}~$i$) in a variables map containing the binding $i - \rightarrow$~\texttt{t}. How to discriminate between these - choices ? - - To solve the dilemma, one gives to \texttt{Quote} a list of - \emph{constant constructors}: a term will be considered as a - constant if it is either a constant constructor of the - application of a constant constructor to constants. For example - the list \verb+[S, O]+ defines the closed natural - numbers. \texttt{(S (S O))} is a constant when \texttt{(S x)} is - not. - - The definition of constants vary for each application of the - tactic, so it can even be different for two applications of - \texttt{Quote} with the same function. - - \item \texttt{f} is a quite simple fixpoint on - \texttt{L}. In particular, \texttt{f} must verify: - -\begin{verbatim} - (f (Cvar i)) = (varmap_find vm default_value i) -\end{verbatim} -\begin{verbatim} - (f (Cconst c)) = c -\end{verbatim} - - where \texttt{index} and \texttt{varmap\_find} are those defined - the \texttt{Quote} module. \emph{The tactic won't work with - user's own variables map !!} It is mandatory to use the - variables map defined in module \texttt{Quote}. - - \end{itemize} - - The method to proceed is then clear: - - \begin{itemize} - \item Start with an empty hashtable of "registed leafs" - that map constr to integers and a "variable counter" equal to 0. - \item Try to match the term with every right hand side of the - definition of f. - - If there is one match, returns the correponding left hand - side and call yourself recursively to get the arguments of this - left hand side. - - If there is no match, we are at a leaf. That is the - interpretation of either a variable or a constant. - - If it is a constant, return \texttt{Cconst} applied to that - constant. - - If not, it is a variable. Look in the hashtable - if this leaf has been already encountered. If not, increment - the variables counter and add an entry to the hashtable; then - return \texttt{(Cvar !variables\_counter)} - \end{itemize} -*) - - -(*i*) -open Pp -open Util -open Names -open Term -open Pattern -open Matching -open Tacmach -open Tactics -open Proof_trees -open Tacexpr -(*i*) - -(*s First, we need to access some Coq constants - We do that lazily, because this code can be linked before - the constants are loaded in the environment *) - -let constant dir s = Coqlib.gen_constant "Quote" ("ring"::dir) s - -let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm") -let coq_Node_vm = lazy (constant ["Quote"] "Node_vm") -let coq_varmap_find = lazy (constant ["Quote"] "varmap_find") -let coq_Right_idx = lazy (constant ["Quote"] "Right_idx") -let coq_Left_idx = lazy (constant ["Quote"] "Left_idx") -let coq_End_idx = lazy (constant ["Quote"] "End_idx") - -(*s Then comes the stuff to decompose the body of interpetation function - and pre-compute the inversion data. - -For a function like: - -\begin{verbatim} - Fixpoint interp[vm:(varmap Prop); f:form] := - Cases f of - | (f_and f1 f1 f2) => (interp f1)/\(interp f2) - | (f_or f1 f1 f2) => (interp f1)\/(interp f2) - | (f_var i) => (varmap_find Prop default_v i vm) - | (f_const c) => c -\end{verbatim} - -With the constant constructors \texttt{C1}, \dots, \texttt{Cn}, the -corresponding scheme will be: - -\begin{verbatim} - {normal_lhs_rhs = - [ "(f_and ?1 ?2)", "?1 /\ ?2"; - "(f_or ?1 ?2)", " ?1 \/ ?2";]; - return_type = "Prop"; - constants = Some [C1,...Cn]; - variable_lhs = Some "(f_var ?1)"; - constant_lhs = Some "(f_const ?1)" - } -\end{verbatim} - -If there is no constructor for variables in the type \texttt{form}, -then [variable_lhs] is [None]. Idem for constants and -[constant_lhs]. Both cannot be equal to [None]. - -The metas in the RHS must correspond to those in the LHS (one cannot -exchange ?1 and ?2 in the example above) - -*) - -module ConstrSet = Set.Make( - struct - type t = constr - let compare = (Pervasives.compare : t->t->int) - end) - -type inversion_scheme = { - normal_lhs_rhs : (constr * constr_pattern) list; - variable_lhs : constr option; - return_type : constr; - constants : ConstrSet.t; - constant_lhs : constr option } - -(*s [compute_ivs gl f cs] computes the inversion scheme associated to - [f:constr] with constants list [cs:constr list] in the context of - goal [gl]. This function uses the auxiliary functions - [i_can't_do_that], [decomp_term], [compute_lhs] and [compute_rhs]. *) - -let i_can't_do_that () = error "Quote: not a simple fixpoint" - -let decomp_term c = kind_of_term (strip_outer_cast c) - -(*s [compute_lhs typ i nargsi] builds the term \texttt{(C ?nargsi ... - ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive - type [typ] *) - -let coerce_meta_out id = - let s = string_of_id id in - int_of_string (String.sub s 1 (String.length s - 1)) -let coerce_meta_in n = - id_of_string ("M" ^ string_of_int n) - -let compute_lhs typ i nargsi = - match kind_of_term typ with - | Ind(sp,0) -> - let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in - mkApp (mkConstruct ((sp,0),i+1), argsi) - | _ -> i_can't_do_that () - -(*s This function builds the pattern from the RHS. Recursive calls are - replaced by meta-variables ?i corresponding to those in the LHS *) - -let compute_rhs bodyi index_of_f = - let rec aux c = - match kind_of_term c with - | App (j, args) when j = mkRel (index_of_f) (* recursive call *) -> - let i = destRel (array_last args) in - PMeta (Some (coerce_meta_in i)) - | App (f,args) -> - PApp (pattern_of_constr f, Array.map aux args) - | Cast (c,_,_) -> aux c - | _ -> pattern_of_constr c - in - aux bodyi - -(*s Now the function [compute_ivs] itself *) - -let compute_ivs gl f cs = - let cst = try destConst f with _ -> i_can't_do_that () in - let body = Environ.constant_value (Global.env()) cst in - match decomp_term body with - | Fix(([| len |], 0), ([| name |], [| typ |], [| body2 |])) -> - let (args3, body3) = decompose_lam body2 in - let nargs3 = List.length args3 in - begin match decomp_term body3 with - | Case(_,p,c,lci) -> (*

Case c of c1 ... cn end *) - let n_lhs_rhs = ref [] - and v_lhs = ref (None : constr option) - and c_lhs = ref (None : constr option) in - Array.iteri - (fun i ci -> - let argsi, bodyi = decompose_lam ci in - let nargsi = List.length argsi in - (* REL (narg3 + nargsi + 1) is f *) - (* REL nargsi+1 to REL nargsi + nargs3 are arguments of f *) - (* REL 1 to REL nargsi are argsi (reverse order) *) - (* First we test if the RHS is the RHS for constants *) - if bodyi = mkRel 1 then - c_lhs := Some (compute_lhs (snd (List.hd args3)) - i nargsi) - (* Then we test if the RHS is the RHS for variables *) - else begin match decompose_app bodyi with - | vmf, [_; _; a3; a4 ] - when isRel a3 & isRel a4 & - pf_conv_x gl vmf - (Lazy.force coq_varmap_find)-> - v_lhs := Some (compute_lhs - (snd (List.hd args3)) - i nargsi) - (* Third case: this is a normal LHS-RHS *) - | _ -> - n_lhs_rhs := - (compute_lhs (snd (List.hd args3)) i nargsi, - compute_rhs bodyi (nargs3 + nargsi + 1)) - :: !n_lhs_rhs - end) - lci; - - if !c_lhs = None & !v_lhs = None then i_can't_do_that (); - - (* The Cases predicate is a lambda; we assume no dependency *) - let p = match kind_of_term p with - | Lambda (_,_,p) -> Termops.pop p - | _ -> p - in - - { normal_lhs_rhs = List.rev !n_lhs_rhs; - variable_lhs = !v_lhs; - return_type = p; - constants = List.fold_right ConstrSet.add cs ConstrSet.empty; - constant_lhs = !c_lhs } - - | _ -> i_can't_do_that () - end - |_ -> i_can't_do_that () - -(* TODO for that function: -\begin{itemize} -\item handle the case where the return type is an argument of the - function -\item handle the case of simple mutual inductive (for example terms - and lists of terms) formulas with the corresponding mutual - recursvive interpretation functions. -\end{itemize} -*) - -(*s Stuff to build variables map, currently implemented as complete -binary search trees (see file \texttt{Quote.v}) *) - -(* First the function to distinghish between constants (closed terms) - and variables (open terms) *) - -let rec closed_under cset t = - (ConstrSet.mem t cset) or - (match (kind_of_term t) with - | Cast(c,_,_) -> closed_under cset c - | App(f,l) -> closed_under cset f && array_for_all (closed_under cset) l - | _ -> false) - -(*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete - binary search tree containing the [ci], that is: - -\begin{verbatim} - c1 - / \ - c2 c3 - / \ - c4 c5 -\end{verbatim} - -The second argument is a constr (the common type of the [ci]) -*) - -let btree_of_array a ty = - let size_of_a = Array.length a in - let semi_size_of_a = size_of_a lsr 1 in - let node = Lazy.force coq_Node_vm - and empty = mkApp (Lazy.force coq_Empty_vm, [| ty |]) in - let rec aux n = - if n > size_of_a - then empty - else if n > semi_size_of_a - then mkApp (node, [| ty; a.(n-1); empty; empty |]) - else mkApp (node, [| ty; a.(n-1); aux (2*n); aux (2*n+1) |]) - in - aux 1 - -(*s [btree_of_array] and [path_of_int] verify the following invariant:\\ - {\tt (varmap\_find A dv }[(path_of_int n)] [(btree_of_array a ty)] - = [a.(n)]\\ - [n] must be [> 0] *) - -let path_of_int n = - (* returns the list of digits of n in reverse order with - initial 1 removed *) - let rec digits_of_int n = - if n=1 then [] - else (n mod 2 = 1)::(digits_of_int (n lsr 1)) - in - List.fold_right - (fun b c -> mkApp ((if b then Lazy.force coq_Right_idx - else Lazy.force coq_Left_idx), - [| c |])) - (List.rev (digits_of_int n)) - (Lazy.force coq_End_idx) - -(*s The tactic works with a list of subterms sharing the same - variables map. We need to sort terms in order to avoid than - strange things happen during replacement of terms by their - 'abstract' counterparties. *) - -(* [subterm t t'] tests if constr [t'] occurs in [t] *) -(* This function does not descend under binders (lambda and Cases) *) - -let rec subterm gl (t : constr) (t' : constr) = - (pf_conv_x gl t t') or - (match (kind_of_term t) with - | App (f,args) -> array_exists (fun t -> subterm gl t t') args - | Cast(t,_,_) -> (subterm gl t t') - | _ -> false) - -(*s We want to sort the list according to reverse subterm order. *) -(* Since it's a partial order the algoritm of Sort.list won't work !! *) - -let rec sort_subterm gl l = - let rec insert c = function - | [] -> [c] - | (h::t as l) when c = h -> l (* Avoid doing the same work twice *) - | h::t -> if subterm gl c h then c::h::t else h::(insert c t) - in - match l with - | [] -> [] - | h::t -> insert h (sort_subterm gl t) - -(*s Now we are able to do the inversion itself. - We destructurate the term and use an imperative hashtable - to store leafs that are already encountered. - The type of arguments is:\\ - [ivs : inversion_scheme]\\ - [lc: constr list]\\ - [gl: goal sigma]\\ *) - -let quote_terms ivs lc gl = - Coqlib.check_required_library ["Coq";"ring";"Quote"]; - let varhash = (Hashtbl.create 17 : (constr, constr) Hashtbl.t) in - let varlist = ref ([] : constr list) in (* list of variables *) - let counter = ref 1 in (* number of variables created + 1 *) - let rec aux c = - let rec auxl l = - match l with - | (lhs, rhs)::tail -> - begin try - let s1 = matches rhs c in - let s2 = List.map (fun (i,c_i) -> (coerce_meta_out i,aux c_i)) s1 - in - Termops.subst_meta s2 lhs - with PatternMatchingFailure -> auxl tail - end - | [] -> - begin match ivs.variable_lhs with - | None -> - begin match ivs.constant_lhs with - | Some c_lhs -> Termops.subst_meta [1, c] c_lhs - | None -> anomaly "invalid inversion scheme for quote" - end - | Some var_lhs -> - begin match ivs.constant_lhs with - | Some c_lhs when closed_under ivs.constants c -> - Termops.subst_meta [1, c] c_lhs - | _ -> - begin - try Hashtbl.find varhash c - with Not_found -> - let newvar = - Termops.subst_meta [1, (path_of_int !counter)] - var_lhs in - begin - incr counter; - varlist := c :: !varlist; - Hashtbl.add varhash c newvar; - newvar - end - end - end - end - in - auxl ivs.normal_lhs_rhs - in - let lp = List.map aux lc in - (lp, (btree_of_array (Array.of_list (List.rev !varlist)) - ivs.return_type )) - -(*s actually we could "quote" a list of terms instead of the - conclusion of current goal. Ring for example needs that, but Ring doesn't - uses Quote yet. *) - -let quote f lid gl = - let f = pf_global gl f in - let cl = List.map (pf_global gl) lid in - let ivs = compute_ivs gl f cl in - let (p, vm) = match quote_terms ivs [(pf_concl gl)] gl with - | [p], vm -> (p,vm) - | _ -> assert false - in - match ivs.variable_lhs with - | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast gl - | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast gl - -(*i - -Just testing ... - -#use "include.ml";; -open Quote;; - -let r = raw_constr_of_string;; - -let ivs = { - normal_lhs_rhs = - [ r "(f_and ?1 ?2)", r "?1/\?2"; - r "(f_not ?1)", r "~?1"]; - variable_lhs = Some (r "(f_atom ?1)"); - return_type = r "Prop"; - constants = ConstrSet.empty; - constant_lhs = (r "nat") -};; - -let t1 = r "True/\(True /\ ~False)";; -let t2 = r "True/\~~False";; - -quote_term ivs () t1;; -quote_term ivs () t2;; - -let ivs2 = - normal_lhs_rhs = - [ r "(f_and ?1 ?2)", r "?1/\?2"; - r "(f_not ?1)", r "~?1" - r "True", r "f_true"]; - variable_lhs = Some (r "(f_atom ?1)"); - return_type = r "Prop"; - constants = ConstrSet.empty; - constant_lhs = (r "nat") - -i*) diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index 92f74d1d94..bb6aaea7de 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -752,7 +752,7 @@ let constants_to_unfold = "Coq.ring.Ring_normalize.interp_vl"; "Coq.ring.Ring_abstract.interp_acs"; "Coq.ring.Ring_abstract.interp_sacs"; - "Coq.ring.Quote.varmap_find"; + "Coq.quote.Quote.varmap_find"; (* anciennement des Local devenus Definition *) "Coq.ring.Ring_normalize.ics_aux"; "Coq.ring.Ring_normalize.ivl_aux"; diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v index 4281cc5736..3ddb6bed12 100644 --- a/contrib/romega/ROmega.v +++ b/contrib/romega/ROmega.v @@ -10,3 +10,5 @@ Require Import ReflOmegaCore. Require Export Setoid. Require Export PreOmega. Require Export ZArith_base. +Require Import OmegaPlugin. +Declare ML Module "romega_plugin". \ No newline at end of file diff --git a/contrib/rtauto/Rtauto.v b/contrib/rtauto/Rtauto.v index 342c03dbac..4b95097e2f 100644 --- a/contrib/rtauto/Rtauto.v +++ b/contrib/rtauto/Rtauto.v @@ -14,6 +14,8 @@ Require Export Bintree. Require Import Bool. Unset Boxed Definitions. +Declare ML Module "rtauto_plugin". + Ltac caseq t := generalize (refl_equal t); pattern t at -1; case t. Ltac clean:=try (simpl;congruence). diff --git a/contrib/setoid_ring/Ring_base.v b/contrib/setoid_ring/Ring_base.v index 95b037e3b6..fd9dd8d0d3 100644 --- a/contrib/setoid_ring/Ring_base.v +++ b/contrib/setoid_ring/Ring_base.v @@ -10,7 +10,8 @@ ring tactic. Abstract rings need more theory, depending on ZArith_base. *) -Declare ML Module "newring". +Require Import Quote. +Declare ML Module "newring_plugin". Require Export Ring_theory. Require Export Ring_tac. Require Import InitialRing. diff --git a/contrib/setoid_ring/Ring_tac.v b/contrib/setoid_ring/Ring_tac.v index 46d106d37a..2ff3322380 100644 --- a/contrib/setoid_ring/Ring_tac.v +++ b/contrib/setoid_ring/Ring_tac.v @@ -4,7 +4,8 @@ Require Import BinPos. Require Import Ring_polynom. Require Import BinList. Require Import InitialRing. -Declare ML Module "newring". +Require Import Quote. +Declare ML Module "newring_plugin". (* adds a definition id' on the normal form of t and an hypothesis id diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v index 8aadf8f5dd..e535a55683 100644 --- a/theories/Reals/Rlogic.v +++ b/theories/Reals/Rlogic.v @@ -177,7 +177,7 @@ assert (Z: Un_cv (fun N : nat => sum_f_R0 g N) ((1/2)^n)). split; intros H; simpl; unfold g; - destruct (eq_nat_dec 0 n); try reflexivity. + destruct (eq_nat_dec 0 n) as [t|f]; try reflexivity. elim f; auto with *. elimtype False; omega. destruct IHa as [IHa0 IHa1]. diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 529ca0ba54..3d93c8a908 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -246,11 +246,22 @@ let traite_fichier_Coq verbose f = try let mldir = Hashtbl.find mlKnown s in let filename = file_name ([String.uncapitalize s],mldir) in - if Coq_config.has_natdynlink then + if Coq_config.has_natdynlink then printf " %s.cmo %s.cmxs" filename filename else printf " %s.cmo" filename - with Not_found -> () + with Not_found -> + (** The .cmxs we want to load dynamically may come + from a .cmxa, that has no corresponding .ml file. + Idem with bytecode .cma. What dependency should + we produce then ? For the moment, we suppose the + .cmxs and .cma are at the same location. *) + let mldir = Some (Filename.dirname f) in + let filename = file_name ([String.uncapitalize s],mldir) in + if Coq_config.has_natdynlink then + printf " %s.cma %s.cmxs" filename filename + else + printf " %s.cma" filename end) sl | Load str -> diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index b2589d42f0..fa8fca66f5 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -78,7 +78,21 @@ let set_include d p = let p = dirpath_of_string p in check_coq_overwriting p; push_include (d,p) let set_rec_include d p = let p = dirpath_of_string p in check_coq_overwriting p; push_rec_include(d,p) - + +let load_initial_plugins () = + (** Order matters ! For instance ground_plugin needs cc_plugin *) + let initial_plugins = + [ "extraction_plugin"; + "jprover_plugin"; + "cc_plugin"; + "ground_plugin"; + "dp_plugin"; + "recdef_plugin"; + (*"subtac_plugin";*) + "xml_plugin"; + ] in + if Mltop.has_dynlink then Mltop.declare_ml_modules initial_plugins + let load_vernacular_list = ref ([] : (string * bool) list) let add_load_vernacular verb s = load_vernacular_list := ((make_suffix s ".v"),verb) :: !load_vernacular_list @@ -340,6 +354,7 @@ let init is_ide = if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then Option.iter Declaremods.start_library !toplevel_name; init_library_roots (); + load_initial_plugins (); load_vernac_obj (); require (); load_rcfile(); diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 57c1464286..611567af98 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -289,18 +289,20 @@ let cache_ml_module_object (_,{mnames=mnames}) = (fun name -> let mname = mod_of_name name in if not (module_is_known mname) then - let fname = file_of_name mname in - begin - try - if_verbose + if has_dynlink then + let fname = file_of_name mname in + try + if_verbose msg (str"[Loading ML file " ++ str fname ++ str" ..."); load_object mname fname; - if_verbose msgnl (str"done]") - with e -> - if_verbose msgnl (str"failed]"); + if_verbose msgnl (str"done]"); + add_loaded_module mname + with e -> + if_verbose msgnl (str"failed]"); raise e - end; - add_loaded_module mname) + else + if_verbose + msgnl (str"[Ignoring ML file " ++ str mname ++ str "]")) mnames let export_ml_module_object x = Some x -- cgit v1.2.3