diff options
Diffstat (limited to 'src/versions')
| -rw-r--r-- | src/versions/standard/Array/PArray_standard.v | 2 | ||||
| -rw-r--r-- | src/versions/standard/Make | 23 | ||||
| -rw-r--r-- | src/versions/standard/Makefile | 202 | ||||
| -rw-r--r-- | src/versions/standard/g_smtcoq_standard.ml4 | 62 | ||||
| -rw-r--r-- | src/versions/standard/smtcoq_plugin_standard.ml4 | 8 | ||||
| -rw-r--r-- | src/versions/standard/smtcoq_plugin_standard.mlpack | 34 | ||||
| -rw-r--r-- | src/versions/standard/structures.ml | 11 |
7 files changed, 245 insertions, 97 deletions
diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v index 2cc8366..4bf5e7a 100644 --- a/src/versions/standard/Array/PArray_standard.v +++ b/src/versions/standard/Array/PArray_standard.v @@ -80,8 +80,6 @@ Notation "t '.[' i '<-' a ']'" := (set t i a) (at level 50) : array_scope. Local Open Scope array_scope. -Set Vm Optimize. - Definition max_array_length := 4194302%int31. (** Axioms *) diff --git a/src/versions/standard/Make b/src/versions/standard/Make index 3834ee0..7c4497e 100644 --- a/src/versions/standard/Make +++ b/src/versions/standard/Make @@ -9,6 +9,8 @@ ######################################################################## ## To generate the Makefile: ## ## coq_makefile -f Make -o Makefile ## +## Suppress the "Makefile" target ## + ## Change the "all" target into: ## ## all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES) ## ## Change the "install-natdynlink" target: change CMXSFILES into CMXS and add the same thing for CMXA. ## @@ -21,6 +23,7 @@ -R . SMTCoq +-I . -I cnf -I euf -I lia @@ -32,19 +35,16 @@ -I versions/standard/Int63 -I versions/standard/Array --custom "cd ../unit-tests; make" "" "test" --custom "cd ../unit-tests; make zchaff" "" "ztest" --custom "cd ../unit-tests; make verit" "" "vtest" +-I $(COQBIN)../plugins/micromega --custom "$(CAMLLEX) $<" "%.mll" "%.ml" --custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli" --custom "" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml" "ml" +# -extra "test" "" "cd ../unit-tests; make" "" +# -extra "ztest" "" "cd ../unit-tests; make zchaff" +# -extra "vtest" "" "cd ../unit-tests; make verit" --custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/standard/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx" "$(CMXA)" --custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)" +-extra "%.ml" "%.mll" "$(CAMLLEX) $<" +-extra "%.ml %.mli" "%.mly" "$(CAMLYACC) $<" +-extra-phony "smtcoq_plugin.mlpack.d" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml" "" -CMXA = smtcoq.cmxa -CMXS = smtcoq_plugin.cmxs CAMLLEX = $(CAMLBIN)ocamllex CAMLYACC = $(CAMLBIN)ocamlyacc @@ -107,4 +107,5 @@ SMT_terms.v State.v Trace.v -smtcoq_plugin.ml4 +g_smtcoq.ml4 +smtcoq_plugin.mlpack diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile index 43946bf..9fda4ea 100644 --- a/src/versions/standard/Makefile +++ b/src/versions/standard/Makefile @@ -2,7 +2,7 @@ ## v # The Coq Proof Assistant ## ## <O___,, # INRIA - CNRS - LIX - LRI - PPS ## ## \VV/ # ## -## // # Makefile automagically generated by coq_makefile V8.5pl2 ## +## // # Makefile automagically generated by coq_makefile V8.6.1 ## ############################################################################# # WARNING @@ -25,6 +25,11 @@ # TIMED if non empty, use the default time command as TIMECMD; # ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc; # DSTROOT to specify a prefix to install path. +# VERBOSE to disable the short display of compilation rules. + +VERBOSE?= +SHOW := $(if $(VERBOSE),@true "",@echo "") +HIDE := $(if $(VERBOSE),,@) # Here is a hack to make $(eval $(shell works: define donewline @@ -34,8 +39,8 @@ endef includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; }))) $(call includecmdwithout@,$(COQBIN)coqtop -config) -TIMED= -TIMECMD= +TIMED?= +TIMECMD?= STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)" TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) @@ -49,7 +54,8 @@ vo_to_obj = $(addsuffix .o,\ # # ########################## -OCAMLLIBS?=-I "cnf"\ +OCAMLLIBS?=-I "."\ + -I "cnf"\ -I "euf"\ -I "lia"\ -I "smtlib2"\ @@ -58,9 +64,11 @@ OCAMLLIBS?=-I "cnf"\ -I "zchaff"\ -I "versions/standard"\ -I "versions/standard/Int63"\ - -I "versions/standard/Array" + -I "versions/standard/Array"\ + -I "$(COQBIN)../plugins/micromega" COQLIBS?=\ -R "." SMTCoq\ + -I "."\ -I "cnf"\ -I "euf"\ -I "lia"\ @@ -70,7 +78,8 @@ COQLIBS?=\ -I "zchaff"\ -I "versions/standard"\ -I "versions/standard/Int63"\ - -I "versions/standard/Array" + -I "versions/standard/Array"\ + -I "$(COQBIN)../plugins/micromega" COQCHKLIBS?=\ -R "." SMTCoq COQDOCLIBS?=\ @@ -82,8 +91,6 @@ COQDOCLIBS?=\ # # ########################## -CMXA=smtcoq.cmxa -CMXS=smtcoq_plugin.cmxs CAMLLEX=$(CAMLBIN)ocamllex CAMLYACC=$(CAMLBIN)ocamlyacc @@ -109,10 +116,13 @@ COQSRCLIBS?=-I "$(COQLIB)kernel" \ -I "$(COQLIB)proofs" \ -I "$(COQLIB)tactics" \ -I "$(COQLIB)tools" \ +-I "$(COQLIB)ltacprof" \ -I "$(COQLIB)toplevel" \ -I "$(COQLIB)stm" \ -I "$(COQLIB)grammar" \ -I "$(COQLIB)config" \ +-I "$(COQLIB)ltac" \ +-I "$(COQLIB)engine" \ \ -I "$(COQLIB)/plugins/btauto" \ -I "$(COQLIB)/plugins/cc" \ @@ -122,6 +132,7 @@ COQSRCLIBS?=-I "$(COQLIB)kernel" \ -I "$(COQLIB)/plugins/firstorder" \ -I "$(COQLIB)/plugins/fourier" \ -I "$(COQLIB)/plugins/funind" \ + -I "$(COQLIB)/plugins/ltac" \ -I "$(COQLIB)/plugins/micromega" \ -I "$(COQLIB)/plugins/nsatz" \ -I "$(COQLIB)/plugins/omega" \ @@ -129,21 +140,24 @@ COQSRCLIBS?=-I "$(COQLIB)kernel" \ -I "$(COQLIB)/plugins/romega" \ -I "$(COQLIB)/plugins/rtauto" \ -I "$(COQLIB)/plugins/setoid_ring" \ + -I "$(COQLIB)/plugins/ssrmatching" \ -I "$(COQLIB)/plugins/syntax" \ -I "$(COQLIB)/plugins/xml" ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) -CAMLC?=$(OCAMLC) -c -rectypes -thread -CAMLOPTC?=$(OCAMLOPT) -c -rectypes -thread -CAMLLINK?=$(OCAMLC) -rectypes -thread -CAMLOPTLINK?=$(OCAMLOPT) -rectypes -thread +CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread +CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread +CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread +CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread +CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack +CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib) GRAMMARS?=grammar.cma ifeq ($(CAMLP4),camlp5) -CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma +CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo else -CAMLP4EXTEND=threads.cma +CAMLP4EXTEND= endif -PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)threads/ $(COQSRCLIBS) compat5.cmo \ +PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \ $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' ################## @@ -207,7 +221,7 @@ GHTMLFILES:=$(VFILES:.v=.g.html) OBJFILES=$(call vo_to_obj,$(VOFILES)) ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs) NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f)) -ML4FILES:=smtcoq_plugin.ml4 +ML4FILES:=g_smtcoq.ml4 ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) -include $(addsuffix .d,$(ML4FILES)) @@ -254,6 +268,18 @@ endif .SECONDARY: $(addsuffix .d,$(MLFILES)) +MLPACKFILES:=smtcoq_plugin.mlpack + +ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),) +-include $(addsuffix .d,$(MLPACKFILES)) +else +ifeq ($(MAKECMDGOALS),) +-include $(addsuffix .d,$(MLPACKFILES)) +endif +endif + +.SECONDARY: $(addsuffix .d,$(MLPACKFILES)) + MLIFILES:=trace/smtAtom.mli\ trace/smtForm.mli\ smtlib2/smtlib2_parse.mli\ @@ -270,7 +296,7 @@ endif .SECONDARY: $(addsuffix .d,$(MLIFILES)) -ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo) +ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo) $(MLPACKFILES:.mlpack=.cmo) CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES)) CMXFILES=$(CMOFILES:.cmo=.cmx) OFILES=$(CMXFILES:.cmx=.o) @@ -288,14 +314,14 @@ endif # # ####################################### -all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES) +all: $(VOFILES) $(CMOFILES) $(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) mlihtml: $(MLIFILES:.mli=.cmi) mkdir $@ || rm -rf $@/* - $(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli) + $(OCAMLFIND) ocamldoc -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli) all-mli.tex: $(MLIFILES:.mli=.cmi) - $(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli) + $(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli) quick: $(VOFILES:.vo=.vio) @@ -333,7 +359,7 @@ beautify: $(VFILES:=.beautified) @echo 'Do not do "make clean" until you are sure that everything went well!' @echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/' -.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo +.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo smtcoq_plugin.mlpack.d ################### # # @@ -341,28 +367,27 @@ beautify: $(VFILES:=.beautified) # # ################### -test: - cd ../unit-tests; make - -ztest: - cd ../unit-tests; make zchaff - -vtest: - cd ../unit-tests; make verit - %.ml: %.mll $(CAMLLEX) $< %.ml %.mli: %.mly $(CAMLYACC) $< -ml: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml +smtcoq_plugin.mlpack.d: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml + +##################################### +# # +# Ad-hoc implicit rules for mlpack. # +# # +##################################### -$(CMXA): versions/standard/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx - $(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^ +$(addsuffix .cmx,$(filter $(basename $(MLFILES)),$(smtcoq_plugin_MLPACK_DEPENDENCIES))): %.cmx: %.ml + $(SHOW)'CAMLOPT -c -for-pack Smtcoq_plugin $<' + $(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack Smtcoq_plugin $< -$(CMXS): $(CMXA) - $(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^ +$(addsuffix .cmx,$(filter $(basename $(ML4FILES)),$(smtcoq_plugin_MLPACK_DEPENDENCIES))): %.cmx: %.ml4 + $(SHOW)'CAMLOPT -c -pp -for-pack Smtcoq_plugin $<' + $(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack Smtcoq_plugin $(PP) -impl $< #################### # # @@ -380,11 +405,7 @@ userinstall: +$(MAKE) USERINSTALL=true install install-natdynlink: - cd "." && for i in $(CMXS); do \ - install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i`"; \ - install -m 0755 $$i "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i; \ - done - cd "." && for i in $(CMXA); do \ + cd "." && for i in $(CMXSFILES); do \ install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i`"; \ install -m 0755 $$i "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i; \ done @@ -394,7 +415,7 @@ install-toploop: $(MLLIBFILES:.mllib=.cmxs) install -m 0755 $? "$(DSTROOT)"$(COQTOPINSTALL)/ install:$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink) - cd "." && for i in $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMXFILES) $(CMIFILES) $(CMAFILES); do \ + cd "." && for i in $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES); do \ install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i`"; \ install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i; \ done @@ -426,21 +447,26 @@ uninstall: uninstall_me.sh .merlin: @echo 'FLG -rectypes' > .merlin - @echo "B $(COQLIB) kernel" >> .merlin - @echo "B $(COQLIB) lib" >> .merlin - @echo "B $(COQLIB) library" >> .merlin - @echo "B $(COQLIB) parsing" >> .merlin - @echo "B $(COQLIB) pretyping" >> .merlin - @echo "B $(COQLIB) interp" >> .merlin - @echo "B $(COQLIB) printing" >> .merlin - @echo "B $(COQLIB) intf" >> .merlin - @echo "B $(COQLIB) proofs" >> .merlin - @echo "B $(COQLIB) tactics" >> .merlin - @echo "B $(COQLIB) tools" >> .merlin - @echo "B $(COQLIB) toplevel" >> .merlin - @echo "B $(COQLIB) stm" >> .merlin - @echo "B $(COQLIB) grammar" >> .merlin - @echo "B $(COQLIB) config" >> .merlin + @echo "B $(COQLIB)kernel" >> .merlin + @echo "B $(COQLIB)lib" >> .merlin + @echo "B $(COQLIB)library" >> .merlin + @echo "B $(COQLIB)parsing" >> .merlin + @echo "B $(COQLIB)pretyping" >> .merlin + @echo "B $(COQLIB)interp" >> .merlin + @echo "B $(COQLIB)printing" >> .merlin + @echo "B $(COQLIB)intf" >> .merlin + @echo "B $(COQLIB)proofs" >> .merlin + @echo "B $(COQLIB)tactics" >> .merlin + @echo "B $(COQLIB)tools" >> .merlin + @echo "B $(COQLIB)ltacprof" >> .merlin + @echo "B $(COQLIB)toplevel" >> .merlin + @echo "B $(COQLIB)stm" >> .merlin + @echo "B $(COQLIB)grammar" >> .merlin + @echo "B $(COQLIB)config" >> .merlin + @echo "B $(COQLIB)ltac" >> .merlin + @echo "B $(COQLIB)engine" >> .merlin + @echo "B /home/artemis/Recherche/Github/smtcoq/smtcoq/src/versions/standard" >> .merlin + @echo "S /home/artemis/Recherche/Github/smtcoq/smtcoq/src/versions/standard" >> .merlin @echo "B cnf" >> .merlin @echo "S cnf" >> .merlin @echo "B euf" >> .merlin @@ -461,6 +487,8 @@ uninstall: uninstall_me.sh @echo "S versions/standard/Int63" >> .merlin @echo "B versions/standard/Array" >> .merlin @echo "S versions/standard/Array" >> .merlin + @echo "B $(COQBIN)../plugins/micromega" >> .merlin + @echo "S $(COQBIN)../plugins/micromega" >> .merlin clean:: rm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES) @@ -471,30 +499,23 @@ clean:: rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old) rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex - rm -rf html mlihtml uninstall_me.sh - - rm -rf test - - rm -rf ztest - - rm -rf vtest - - rm -rf ml - - rm -rf $(CMXA) - - rm -rf $(CMXS) - - rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtcoq.a cleanall:: clean - rm -f $(patsubst %.v,.%.aux,$(VFILES)) + rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) archclean:: rm -f *.cmx *.o printenv: @"$(COQBIN)coqtop" -config - @echo 'CAMLC = $(CAMLC)' - @echo 'CAMLOPTC = $(CAMLOPTC)' + @echo 'OCAMLFIND = $(OCAMLFIND)' @echo 'PP = $(PP)' @echo 'COQFLAGS = $(COQFLAGS)' @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' + ################### # # # Implicit rules. # @@ -502,34 +523,60 @@ printenv: ################### $(MLIFILES:.mli=.cmi): %.cmi: %.mli - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $< + $(SHOW)'CAMLC -c $<' + $(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $< $(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli - $(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) $(ML4FILES:.ml4=.cmo): %.cmo: %.ml4 - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< + $(SHOW)'CAMLC -pp -c $<' + $(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< $(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4 - $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< + $(SHOW)'CAMLOPT -pp -c $<' + $(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $< $(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4 - $(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + $(SHOW)'CAMLDEP -pp $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) $(MLFILES:.ml=.cmo): %.cmo: %.ml - $(CAMLC) $(ZDEBUG) $(ZFLAGS) $< + $(SHOW)'CAMLC -c $<' + $(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $< $(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml - $(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $< + $(SHOW)'CAMLOPT -c $<' + $(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $< $(addsuffix .d,$(MLFILES)): %.ml.d: %.ml - $(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + +$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx + $(SHOW)'CAMLOPT -shared -o $@' + $(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $< $(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa - $(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $< + $(SHOW)'CAMLOPT -shared -o $@' + $(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $< + +$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack + $(SHOW)'CAMLC -pack -o $@' + $(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^ + +$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack + $(SHOW)'CAMLOPT -pack -o $@' + $(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^ + +$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack + $(SHOW)'COQDEP $<' + $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) $(VOFILES): %.vo: %.v - $(COQC) $(COQDEBUG) $(COQFLAGS) $< + $(SHOW)COQC $< + $(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $< $(GLOBFILES): %.glob: %.v $(COQC) $(COQDEBUG) $(COQFLAGS) $< @@ -553,7 +600,8 @@ $(GHTMLFILES): %.g.html: %.v %.glob $(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ $(addsuffix .d,$(VFILES)): %.v.d: %.v - $(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) + $(SHOW)'COQDEP $<' + $(HIDE)$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} ) $(addsuffix .beautified,$(VFILES)): %.v.beautified: $(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v diff --git a/src/versions/standard/g_smtcoq_standard.ml4 b/src/versions/standard/g_smtcoq_standard.ml4 new file mode 100644 index 0000000..ab097a1 --- /dev/null +++ b/src/versions/standard/g_smtcoq_standard.ml4 @@ -0,0 +1,62 @@ +(**************************************************************************) +(* *) +(* SMTCoq *) +(* Copyright (C) 2011 - 2016 *) +(* *) +(* Michaël Armand *) +(* Benjamin Grégoire *) +(* Chantal Keller *) +(* *) +(* Inria - École Polytechnique - Université Paris-Sud *) +(* *) +(* This file is distributed under the terms of the CeCILL-C licence *) +(* *) +(**************************************************************************) + + +DECLARE PLUGIN "smtcoq_plugin" + +open Genarg +open Stdarg +open Constrarg + +VERNAC COMMAND EXTEND Vernac_zchaff CLASSIFIED AS QUERY +| [ "Parse_certif_zchaff" + ident(dimacs) ident(trace) string(fdimacs) string(fproof) ] -> + [ + Zchaff.parse_certif dimacs trace fdimacs fproof + ] +| [ "Zchaff_Checker" string(fdimacs) string(fproof) ] -> + [ + Zchaff.checker fdimacs fproof + ] +| [ "Zchaff_Theorem" ident(name) string(fdimacs) string(fproof) ] -> + [ + Zchaff.theorem name fdimacs fproof + ] +END + +VERNAC COMMAND EXTEND Vernac_verit CLASSIFIED AS QUERY +| [ "Parse_certif_verit" + ident(t_i) ident(t_func) ident(t_atom) ident(t_form) ident(root) ident(used_roots) ident(trace) string(fsmt) string(fproof) ] -> + [ + Verit.parse_certif t_i t_func t_atom t_form root used_roots trace fsmt fproof + ] +| [ "Verit_Checker" string(fsmt) string(fproof) ] -> + [ + Verit.checker fsmt fproof + ] +| [ "Verit_Theorem" ident(name) string(fsmt) string(fproof) ] -> + [ + Verit.theorem name fsmt fproof + ] +END + + +TACTIC EXTEND Tactic_zchaff +| [ "zchaff" ] -> [ Zchaff.tactic () ] +END + +TACTIC EXTEND Tactic_verit +| [ "verit" ] -> [ Verit.tactic () ] +END diff --git a/src/versions/standard/smtcoq_plugin_standard.ml4 b/src/versions/standard/smtcoq_plugin_standard.ml4 index 6ae3545..ab097a1 100644 --- a/src/versions/standard/smtcoq_plugin_standard.ml4 +++ b/src/versions/standard/smtcoq_plugin_standard.ml4 @@ -16,7 +16,11 @@ DECLARE PLUGIN "smtcoq_plugin" -VERNAC COMMAND EXTEND Vernac_zchaff +open Genarg +open Stdarg +open Constrarg + +VERNAC COMMAND EXTEND Vernac_zchaff CLASSIFIED AS QUERY | [ "Parse_certif_zchaff" ident(dimacs) ident(trace) string(fdimacs) string(fproof) ] -> [ @@ -32,7 +36,7 @@ VERNAC COMMAND EXTEND Vernac_zchaff ] END -VERNAC COMMAND EXTEND Vernac_verit +VERNAC COMMAND EXTEND Vernac_verit CLASSIFIED AS QUERY | [ "Parse_certif_verit" ident(t_i) ident(t_func) ident(t_atom) ident(t_form) ident(root) ident(used_roots) ident(trace) string(fsmt) string(fproof) ] -> [ diff --git a/src/versions/standard/smtcoq_plugin_standard.mlpack b/src/versions/standard/smtcoq_plugin_standard.mlpack new file mode 100644 index 0000000..3ab358b --- /dev/null +++ b/src/versions/standard/smtcoq_plugin_standard.mlpack @@ -0,0 +1,34 @@ +Structures + +SmtMisc +CoqTerms +SmtForm +SmtCertif +SmtTrace +SmtCnf +SatAtom +SmtAtom + +SatParser +ZchaffParser +CnfParser +Zchaff + +Smtlib2_util +Smtlib2_ast +Smtlib2_parse +Smtlib2_lex + +Lia + +VeritSyntax +VeritParser +VeritLexer + +Smtlib2_genConstr + +SmtCommands + +Verit + +G_smtcoq diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml index 19104fe..45a8ca4 100644 --- a/src/versions/standard/structures.ml +++ b/src/versions/standard/structures.ml @@ -111,7 +111,7 @@ let mkTConst c noc ty = const_entry_opaque = false; const_entry_inline_code = false } -let error = Errors.error +let error = CErrors.error let coqtype = Future.from_val Term.mkSet @@ -138,14 +138,15 @@ let lift = Vars.lift let tclTHEN = Tacticals.New.tclTHEN let tclTHENLAST = Tacticals.New.tclTHENLAST let assert_before = Tactics.assert_before -let vm_cast_no_check t = Proofview.V82.tactic (Tactics.vm_cast_no_check t) +let vm_cast_no_check t = Tactics.vm_cast_no_check t +(* let vm_cast_no_check t = Proofview.V82.tactic (Tactics.vm_cast_no_check t) *) let mk_tactic tac = - Proofview.Goal.nf_enter (fun gl -> + Proofview.Goal.nf_enter {enter = (fun gl -> let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in + let sigma = Tacmach.New.project gl in let t = Proofview.Goal.concl gl in tac env sigma t - ) + )} let set_evars_tac noc = mk_tactic ( fun env sigma _ -> |