diff options
-rw-r--r-- | .gitignore | 1 | ||||
-rw-r--r-- | INSTALL.md | 14 | ||||
-rw-r--r-- | Makefile | 2 | ||||
-rw-r--r-- | src/Makefile | 866 | ||||
-rw-r--r-- | src/Misc.v | 2 | ||||
-rw-r--r-- | src/SMT_terms.v | 2 | ||||
-rw-r--r-- | src/State.v | 4 | ||||
-rw-r--r-- | src/bva/Bva_checker.v | 32 | ||||
-rw-r--r-- | src/cnf/Cnf.v | 10 | ||||
-rwxr-xr-x | src/configure.sh | 4 | ||||
-rw-r--r-- | src/lia/Lia.v | 47 | ||||
-rw-r--r-- | src/trace/coqInterface.ml | 4 | ||||
-rw-r--r-- | src/trace/coqInterface.mli | 3 | ||||
-rw-r--r-- | src/trace/smtCommands.ml | 2 |
14 files changed, 926 insertions, 67 deletions
@@ -24,7 +24,6 @@ setup.log .nia.cache # targets of coq_makefile: -src/Makefile src/Makefile.conf src/g_smtcoq.ml @@ -73,12 +73,12 @@ Then follow the instructions of the previous section. ### Requirements -You need to have OCaml version >= 4.09.0 and Coq version 8.11.*. +You need to have OCaml version >= 4.11.1 and Coq version 8.12.*. > **Warning**: The version of Coq that you plan to use must have been compiled > with the same version of OCaml that you are going to use to compile > SMTCoq. In particular this means you want a version of Coq that was compiled -> with OCaml version >= 4.08. +> with OCaml version >= 4.11.1. ### Install opam @@ -103,24 +103,24 @@ eval `opam config env` ### Install OCaml -Now you can install an OCaml compiler (we recommend 4.10.0): +Now you can install an OCaml compiler (we recommend 4.11.1): ```bash -opam switch create ocaml-base-compiler.4.10.0 +opam switch create ocaml-base-compiler.4.11.1 ``` ### Install Coq -After OCaml is installed, you can install Coq-8.11.2 through opam. +After OCaml is installed, you can install Coq-8.12.1 through opam. ```bash -opam install coq.8.11.2 +opam install coq.8.12.1 ``` If you also want to install CoqIDE at the same time you can do ```bash -opam install coq.8.11.2 coqide.8.11.2 +opam install coq.8.12.1 coqide.8.12.1 ``` but you might need to install some extra packages and libraries for your system @@ -1,5 +1,5 @@ all: - cd src && ./configure.sh && $(MAKE) + cd src && $(MAKE) install: all cd src && $(MAKE) install diff --git a/src/Makefile b/src/Makefile new file mode 100644 index 0000000..5653389 --- /dev/null +++ b/src/Makefile @@ -0,0 +1,866 @@ +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # Copyright INRIA, CNRS and contributors ## +## <O___,, # (see version control and CREDITS file for authors & dates) ## +## \VV/ ############################################################### +## // # This file is distributed under the terms of the ## +## # GNU Lesser General Public License Version 2.1 ## +## # (see LICENSE file for the text of the license) ## +########################################################################## +## GNUMakefile for Coq 8.12.2 + +# For debugging purposes (must stay here, don't move below) +INITIAL_VARS := $(.VARIABLES) +# To implement recursion we save the name of the main Makefile +SELF := $(lastword $(MAKEFILE_LIST)) +PARENT := $(firstword $(MAKEFILE_LIST)) + +# This file is generated by coq_makefile and contains many variable +# definitions, like the list of .v files or the path to Coq +include Makefile.conf + +# Put in place old names +VFILES := $(COQMF_VFILES) +MLIFILES := $(COQMF_MLIFILES) +MLFILES := $(COQMF_MLFILES) +MLGFILES := $(COQMF_MLGFILES) +MLPACKFILES := $(COQMF_MLPACKFILES) +MLLIBFILES := $(COQMF_MLLIBFILES) +CMDLINE_VFILES := $(COQMF_CMDLINE_VFILES) +INSTALLCOQDOCROOT := $(COQMF_INSTALLCOQDOCROOT) +OTHERFLAGS := $(COQMF_OTHERFLAGS) +COQ_SRC_SUBDIRS := $(COQMF_COQ_SRC_SUBDIRS) +OCAMLLIBS := $(COQMF_OCAMLLIBS) +SRC_SUBDIRS := $(COQMF_SRC_SUBDIRS) +COQLIBS := $(COQMF_COQLIBS) +COQLIBS_NOML := $(COQMF_COQLIBS_NOML) +CMDLINE_COQLIBS := $(COQMF_CMDLINE_COQLIBS) +LOCAL := $(COQMF_LOCAL) +COQLIB := $(COQMF_COQLIB) +DOCDIR := $(COQMF_DOCDIR) +OCAMLFIND := $(COQMF_OCAMLFIND) +CAMLFLAGS := $(COQMF_CAMLFLAGS) +HASNATDYNLINK := $(COQMF_HASNATDYNLINK) +OCAMLWARN := $(COQMF_WARN) + +Makefile.conf: _CoqProject + coq_makefile -f _CoqProject -o Makefile + +# This file can be created by the user to hook into double colon rules or +# add any other Makefile code he may need +-include Makefile.local + +# Parameters ################################################################## +# +# Parameters are make variable assignments. +# They can be passed to (each call to) make on the command line. +# They can also be put in Makefile.local once and for all. +# For retro-compatibility reasons they can be put in the _CoqProject, but this +# practice is discouraged since _CoqProject better not contain make specific +# code (be nice to user interfaces). + +# Print shell commands (set to non empty) +VERBOSE ?= + +# Time the Coq process (set to non empty), and how (see default value) +TIMED?= +TIMECMD?= +# Use command time on linux, gtime on Mac OS +TIMEFMT?="$@ (real: %e, user: %U, sys: %S, mem: %M ko)" +ifneq (,$(TIMED)) +ifeq (0,$(shell command time -f "" true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=command time -f $(TIMEFMT) +else +ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=gtime -f $(TIMEFMT) +else +STDTIME?=command time +endif +endif +else +STDTIME?=command time -f $(TIMEFMT) +endif + +ifneq (,$(COQBIN)) +# add an ending / +COQBIN:=$(COQBIN)/ +endif + +# Coq binaries +COQC ?= "$(COQBIN)coqc" +COQTOP ?= "$(COQBIN)coqtop" +COQCHK ?= "$(COQBIN)coqchk" +COQDEP ?= "$(COQBIN)coqdep" +COQDOC ?= "$(COQBIN)coqdoc" +COQPP ?= "$(COQBIN)coqpp" +COQMKFILE ?= "$(COQBIN)coq_makefile" +OCAMLLIBDEP ?= "$(COQBIN)ocamllibdep" + +# Timing scripts +COQMAKE_ONE_TIME_FILE ?= "$(COQLIB)/tools/make-one-time-file.py" +COQMAKE_BOTH_TIME_FILES ?= "$(COQLIB)/tools/make-both-time-files.py" +COQMAKE_BOTH_SINGLE_TIMING_FILES ?= "$(COQLIB)/tools/make-both-single-timing-files.py" +BEFORE ?= +AFTER ?= + +# FIXME this should be generated by Coq (modules already linked by Coq) +CAMLDONTLINK=num,str,unix,dynlink,threads + +# OCaml binaries +CAMLC ?= "$(OCAMLFIND)" ocamlc -c +CAMLOPTC ?= "$(OCAMLFIND)" opt -c +CAMLLINK ?= "$(OCAMLFIND)" ocamlc -linkpkg -dontlink $(CAMLDONTLINK) +CAMLOPTLINK ?= "$(OCAMLFIND)" opt -linkpkg -dontlink $(CAMLDONTLINK) +CAMLDOC ?= "$(OCAMLFIND)" ocamldoc +CAMLDEP ?= "$(OCAMLFIND)" ocamldep -slash -ml-synonym .mlpack + +# DESTDIR is prepended to all installation paths +DESTDIR ?= + +# Debug builds, typically -g to OCaml, -debug to Coq. +CAMLDEBUG ?= +COQDEBUG ?= + +# Extra packages to be linked in (as in findlib -package) +CAMLPKGS ?= + +# Option for making timing files +TIMING?= +# Option for changing sorting of timing output file +TIMING_SORT_BY ?= auto +# Option for changing the fuzz parameter on the output file +TIMING_FUZZ ?= 0 +# Option for changing whether to use real or user time for timing tables +TIMING_REAL?= +# Option for including the memory column(s) +TIMING_INCLUDE_MEM?= +# Option for sorting by the memory column +TIMING_SORT_BY_MEM?= +# Output file names for timed builds +TIME_OF_BUILD_FILE ?= time-of-build.log +TIME_OF_BUILD_BEFORE_FILE ?= time-of-build-before.log +TIME_OF_BUILD_AFTER_FILE ?= time-of-build-after.log +TIME_OF_PRETTY_BUILD_FILE ?= time-of-build-pretty.log +TIME_OF_PRETTY_BOTH_BUILD_FILE ?= time-of-build-both.log +TIME_OF_PRETTY_BUILD_EXTRA_FILES ?= - # also output to the command line + +TGTS ?= + +########## End of parameters ################################################## +# What follows may be relevant to you only if you need to +# extend this Makefile. If so, look for 'Extension point' here and +# put in Makefile.local double colon rules accordingly. +# E.g. to perform some work after the all target completes you can write +# +# post-all:: +# echo "All done!" +# +# in Makefile.local +# +############################################################################### + + + + +# Flags ####################################################################### +# +# We define a bunch of variables combining the parameters. +# To add additional flags to coq, coqchk or coqdoc, set the +# {COQ,COQCHK,COQDOC}EXTRAFLAGS variable to whatever you want to add. +# To overwrite the default choice and set your own flags entirely, set the +# {COQ,COQCHK,COQDOC}FLAGS variable. + +SHOW := $(if $(VERBOSE),@true "",@echo "") +HIDE := $(if $(VERBOSE),,@) + +TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) + +OPT?= + +# The DYNOBJ and DYNLIB variables are used by "coqdep -dyndep var" in .v.d +ifeq '$(OPT)' '-byte' +USEBYTE:=true +DYNOBJ:=.cma +DYNLIB:=.cma +else +USEBYTE:= +DYNOBJ:=.cmxs +DYNLIB:=.cmxs +endif + +# these variables are meant to be overridden if you want to add *extra* flags +COQEXTRAFLAGS?= +COQCHKEXTRAFLAGS?= +COQDOCEXTRAFLAGS?= + +# these flags do NOT contain the libraries, to make them easier to overwrite +COQFLAGS?=-q $(OTHERFLAGS) $(COQEXTRAFLAGS) +COQCHKFLAGS?=-silent -o $(COQCHKEXTRAFLAGS) +COQDOCFLAGS?=-interpolate -utf8 $(COQDOCEXTRAFLAGS) + +COQDOCLIBS?=$(COQLIBS_NOML) + +# The version of Coq being run and the version of coq_makefile that +# generated this makefile +COQ_VERSION:=$(shell $(COQC) --print-version | cut -d " " -f 1) +COQMAKEFILE_VERSION:=8.12.2 + +COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)") + +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) +# ocamldoc fails with unknown argument otherwise +CAMLDOCFLAGS:=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) +CAMLFLAGS+=$(OCAMLWARN) + +ifneq (,$(TIMING)) +TIMING_ARG=-time +ifeq (after,$(TIMING)) +TIMING_EXT=after-timing +else +ifeq (before,$(TIMING)) +TIMING_EXT=before-timing +else +TIMING_EXT=timing +endif +endif +else +TIMING_ARG= +endif + +# Retro compatibility (DESTDIR is standard on Unix, DSTROOT is not) +ifdef DSTROOT +DESTDIR := $(DSTROOT) +endif + +concat_path = $(if $(1),$(1)/$(if $(COQMF_WINDRIVE),$(subst $(COQMF_WINDRIVE),/,$(2)),$(2)),$(2)) + +COQLIBINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/user-contrib) +COQDOCINSTALL = $(call concat_path,$(DESTDIR),$(DOCDIR)/user-contrib) +COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop) + +# Files ####################################################################### +# +# We here define a bunch of variables about the files being part of the +# Coq project in order to ease the writing of build target and build rules + +VDFILE := .Makefile.d + +ALLSRCFILES := \ + $(MLGFILES) \ + $(MLFILES) \ + $(MLPACKFILES) \ + $(MLLIBFILES) \ + $(MLIFILES) + +# helpers +vo_to_obj = $(addsuffix .o,\ + $(filter-out Warning: Error:,\ + $(shell $(COQTOP) -q -noinit -batch -quiet -print-mod-uid $(1)))) +strip_dotslash = $(patsubst ./%,%,$(1)) + +# without this we get undefined variables in the expansion for the +# targets of the [deprecated,use-mllib-or-mlpack] rule +with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1))) + +VO = vo +VOS = vos + +VOFILES = $(VFILES:.v=.$(VO)) +GLOBFILES = $(VFILES:.v=.glob) +HTMLFILES = $(VFILES:.v=.html) +GHTMLFILES = $(VFILES:.v=.g.html) +BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) +TEXFILES = $(VFILES:.v=.tex) +GTEXFILES = $(VFILES:.v=.g.tex) +CMOFILES = \ + $(MLGFILES:.mlg=.cmo) \ + $(MLFILES:.ml=.cmo) \ + $(MLPACKFILES:.mlpack=.cmo) +CMXFILES = $(CMOFILES:.cmo=.cmx) +OFILES = $(CMXFILES:.cmx=.o) +CMAFILES = $(MLLIBFILES:.mllib=.cma) $(MLPACKFILES:.mlpack=.cma) +CMXAFILES = $(CMAFILES:.cma=.cmxa) +CMIFILES = \ + $(CMOFILES:.cmo=.cmi) \ + $(MLIFILES:.mli=.cmi) +# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just +# a .mlg file +CMXSFILES = \ + $(MLPACKFILES:.mlpack=.cmxs) \ + $(CMXAFILES:.cmxa=.cmxs) \ + $(if $(MLPACKFILES)$(CMXAFILES),,\ + $(MLGFILES:.mlg=.cmxs) $(MLFILES:.ml=.cmxs)) + +# files that are packed into a plugin (no extension) +PACKEDFILES = \ + $(call strip_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES)),$(call with_undef,$(lib)))) +# files that are archived into a .cma (mllib) +LIBEDFILES = \ + $(call strip_dotslash, \ + $(foreach lib, \ + $(call strip_dotslash, \ + $(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES)),$(call with_undef,$(lib)))) +CMIFILESTOINSTALL = $(filter-out $(addsuffix .cmi,$(PACKEDFILES)),$(CMIFILES)) +CMOFILESTOINSTALL = $(filter-out $(addsuffix .cmo,$(PACKEDFILES)),$(CMOFILES)) +OBJFILES = $(call vo_to_obj,$(VOFILES)) +ALLNATIVEFILES = \ + $(OBJFILES:.o=.cmi) \ + $(OBJFILES:.o=.cmx) \ + $(OBJFILES:.o=.cmxs) +# trick: wildcard filters out non-existing files, so that `install` doesn't show +# warnings and `clean` doesn't pass to rm a list of files that is too long for +# the shell. +NATIVEFILES = $(wildcard $(ALLNATIVEFILES)) +FILESTOINSTALL = \ + $(VOFILES) \ + $(VFILES) \ + $(GLOBFILES) \ + $(NATIVEFILES) \ + $(CMIFILESTOINSTALL) +BYTEFILESTOINSTALL = \ + $(CMOFILESTOINSTALL) \ + $(CMAFILES) +ifeq '$(HASNATDYNLINK)' 'true' +DO_NATDYNLINK = yes +FILESTOINSTALL += $(CMXSFILES) $(CMXAFILES) $(CMOFILESTOINSTALL:.cmo=.cmx) +else +DO_NATDYNLINK = +endif + +ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE) + +# Compilation targets ######################################################### + +all: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all +.PHONY: all + +all.timing.diff: + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" pre-all + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" real-all.timing.diff TIME_OF_PRETTY_BUILD_EXTRA_FILES="" + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" post-all +.PHONY: all.timing.diff + +ifeq (0,$(TIMING_REAL)) +TIMING_REAL_ARG := +TIMING_USER_ARG := --user +else +ifeq (1,$(TIMING_REAL)) +TIMING_REAL_ARG := --real +TIMING_USER_ARG := +else +TIMING_REAL_ARG := +TIMING_USER_ARG := +endif +endif + +ifeq (0,$(TIMING_INCLUDE_MEM)) +TIMING_INCLUDE_MEM_ARG := --no-include-mem +else +TIMING_INCLUDE_MEM_ARG := +endif + +ifeq (1,$(TIMING_SORT_BY_MEM)) +TIMING_SORT_BY_MEM_ARG := --sort-by-mem +else +TIMING_SORT_BY_MEM_ARG := +endif + +make-pretty-timed-before:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_BEFORE_FILE) +make-pretty-timed-after:: TIME_OF_BUILD_FILE=$(TIME_OF_BUILD_AFTER_FILE) +make-pretty-timed make-pretty-timed-before make-pretty-timed-after:: + $(HIDE)rm -f pretty-timed-success.ok + $(HIDE)($(MAKE) --no-print-directory -f "$(PARENT)" $(TGTS) TIMED=1 2>&1 && touch pretty-timed-success.ok) | tee -a $(TIME_OF_BUILD_FILE) + $(HIDE)rm pretty-timed-success.ok # must not be -f; must fail if the touch failed +print-pretty-timed:: + $(HIDE)$(COQMAKE_ONE_TIME_FILE) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +print-pretty-timed-diff:: + $(HIDE)$(COQMAKE_BOTH_TIME_FILES) --sort-by=$(TIMING_SORT_BY) $(TIMING_INCLUDE_MEM_ARG) $(TIMING_SORT_BY_MEM_ARG) $(TIMING_REAL_ARG) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +ifeq (,$(BEFORE)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' + $(HIDE)false +else +ifeq (,$(AFTER)) +print-pretty-single-time-diff:: + @echo 'Error: Usage: $(MAKE) print-pretty-single-time-diff AFTER=path/to/file.v.after-timing BEFORE=path/to/file.v.before-timing' + $(HIDE)false +else +print-pretty-single-time-diff:: + $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --fuzz=$(TIMING_FUZZ) --sort-by=$(TIMING_SORT_BY) $(TIMING_USER_ARG) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES) +endif +endif +pretty-timed: + $(HIDE)$(MAKE) --no-print-directory -f "$(PARENT)" make-pretty-timed + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-timed +.PHONY: pretty-timed make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff + +# Extension points for actions to be performed before/after the all target +pre-all:: + @# Extension point + $(HIDE)if [ "$(COQMAKEFILE_VERSION)" != "$(COQ_VERSION)" ]; then\ + echo "W: This Makefile was generated by Coq $(COQMAKEFILE_VERSION)";\ + echo "W: while the current Coq version is $(COQ_VERSION)";\ + fi +.PHONY: pre-all + +post-all:: + @# Extension point +.PHONY: post-all + +real-all: $(VOFILES) $(if $(USEBYTE),bytefiles,optfiles) +.PHONY: real-all + +real-all.timing.diff: $(VOFILES:.vo=.v.timing.diff) +.PHONY: real-all.timing.diff + +bytefiles: $(CMOFILES) $(CMAFILES) +.PHONY: bytefiles + +optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) +.PHONY: optfiles + +# FIXME, see Ralf's bugreport +# quick is deprecated, now renamed vio +vio: $(VOFILES:.vo=.vio) +.PHONY: vio +quick: vio + $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") +.PHONY: quick + +vio2vo: + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ + -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) +.PHONY: vio2vo + +# quick2vo is undocumented +quick2vo: + $(HIDE)make -j $(J) vio + $(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \ + viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \ + if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \ + done); \ + echo "VIO2VO: $$VIOFILES"; \ + if [ -n "$$VIOFILES" ]; then \ + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -schedule-vio2vo $(J) $$VIOFILES; \ + fi +.PHONY: quick2vo + +checkproofs: + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) \ + -schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio) +.PHONY: checkproofs + +vos: $(VOFILES:%.vo=%.vos) +.PHONY: vos + +vok: $(VOFILES:%.vo=%.vok) +.PHONY: vok + +validate: $(VOFILES) + $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^ +.PHONY: validate + +only: $(TGTS) +.PHONY: only + +# Documentation targets ####################################################### + +html: $(GLOBFILES) $(VFILES) + $(SHOW)'COQDOC -d html $(GAL)' + $(HIDE)mkdir -p html + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -html $(GAL) $(COQDOCLIBS) -d html $(VFILES) + +mlihtml: $(MLIFILES:.mli=.cmi) + $(SHOW)'CAMLDOC -d $@' + $(HIDE)mkdir $@ || rm -rf $@/* + $(HIDE)$(CAMLDOC) -html \ + -d $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) + +all-mli.tex: $(MLIFILES:.mli=.cmi) + $(SHOW)'CAMLDOC -latex $@' + $(HIDE)$(CAMLDOC) -latex \ + -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) + +all.ps: $(VFILES) + $(SHOW)'COQDOC -ps $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort $(VFILES)` + +all.pdf: $(VFILES) + $(SHOW)'COQDOC -pdf $(GAL)' + $(HIDE)$(COQDOC) \ + -toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \ + -o $@ `$(COQDEP) -sort $(VFILES)` + +# FIXME: not quite right, since the output name is different +gallinahtml: GAL=-g +gallinahtml: html + +all-gal.ps: GAL=-g +all-gal.ps: all.ps + +all-gal.pdf: GAL=-g +all-gal.pdf: all.pdf + +# ? +beautify: $(BEAUTYFILES) + for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done + @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: beautify + +# Installation targets ######################################################## +# +# There rules can be extended in Makefile.local +# Extensions can't assume when they run. + +install: + $(HIDE)code=0; for f in $(FILESTOINSTALL); do\ + if ! [ -f "$$f" ]; then >&2 echo $$f does not exist; code=1; fi \ + done; exit $$code + $(HIDE)for f in $(FILESTOINSTALL); do\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ + echo SKIP "$$f" since it has no logical path;\ + else\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ + fi;\ + done + $(HIDE)$(MAKE) install-extra -f "$(SELF)" +install-extra:: + @# Extension point +.PHONY: install install-extra + +install-byte: + $(HIDE)for f in $(BYTEFILESTOINSTALL); do\ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`";\ + if [ "$$?" != "0" -o -z "$$df" ]; then\ + echo SKIP "$$f" since it has no logical path;\ + else\ + install -d "$(COQLIBINSTALL)/$$df" &&\ + install -m 0644 "$$f" "$(COQLIBINSTALL)/$$df" &&\ + echo INSTALL "$$f" "$(COQLIBINSTALL)/$$df";\ + fi;\ + done + +install-doc:: html mlihtml + @# Extension point + $(HIDE)install -d "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(HIDE)for i in html/*; do \ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + install -m 0644 "$$i" "$$dest";\ + echo INSTALL "$$i" "$$dest";\ + done + $(HIDE)install -d \ + "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE)for i in mlihtml/*; do \ + dest="$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/$$i";\ + install -m 0644 "$$i" "$$dest";\ + echo INSTALL "$$i" "$$dest";\ + done +.PHONY: install-doc + +uninstall:: + @# Extension point + $(HIDE)for f in $(FILESTOINSTALL); do \ + df="`$(COQMKFILE) -destination-of "$$f" $(COQLIBS)`" &&\ + instf="$(COQLIBINSTALL)/$$df/`basename $$f`" &&\ + rm -f "$$instf" &&\ + echo RM "$$instf" &&\ + (rmdir "$(call concat_path,,$(COQLIBINSTALL)/$$df/)" 2>/dev/null || true); \ + done +.PHONY: uninstall + +uninstall-doc:: + @# Extension point + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/html" + $(SHOW)'RM $(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml' + $(HIDE)rm -rf "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/mlihtml" + $(HIDE) rmdir "$(COQDOCINSTALL)/$(INSTALLCOQDOCROOT)/" || true +.PHONY: uninstall-doc + +# Cleaning #################################################################### +# +# There rules can be extended in Makefile.local +# Extensions can't assume when they run. + +clean:: + @# Extension point + $(SHOW)'CLEAN' + $(HIDE)rm -f $(CMOFILES) + $(HIDE)rm -f $(CMIFILES) + $(HIDE)rm -f $(CMAFILES) + $(HIDE)rm -f $(CMOFILES:.cmo=.cmx) + $(HIDE)rm -f $(CMXAFILES) + $(HIDE)rm -f $(CMXSFILES) + $(HIDE)rm -f $(CMOFILES:.cmo=.o) + $(HIDE)rm -f $(CMXAFILES:.cmxa=.a) + $(HIDE)rm -f $(MLGFILES:.mlg=.ml) + $(HIDE)rm -f $(ALLDFILES) + $(HIDE)rm -f $(NATIVEFILES) + $(HIDE)find . -name .coq-native -type d -empty -delete + $(HIDE)rm -f $(VOFILES) + $(HIDE)rm -f $(VOFILES:.vo=.vio) + $(HIDE)rm -f $(VOFILES:.vo=.vos) + $(HIDE)rm -f $(VOFILES:.vo=.vok) + $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) + $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex + $(HIDE)rm -f $(VFILES:.v=.glob) + $(HIDE)rm -f $(VFILES:.v=.tex) + $(HIDE)rm -f $(VFILES:.v=.g.tex) + $(HIDE)rm -f pretty-timed-success.ok + $(HIDE)rm -rf html mlihtml +.PHONY: clean + +cleanall:: clean + @# Extension point + $(SHOW)'CLEAN *.aux *.timing' + $(HIDE)rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux) + $(HIDE)rm -f $(TIME_OF_BUILD_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.before-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.after-timing) + $(HIDE)rm -f $(VOFILES:.vo=.v.timing.diff) + $(HIDE)rm -f .lia.cache .nia.cache +.PHONY: cleanall + +archclean:: + @# Extension point + $(SHOW)'CLEAN *.cmx *.o' + $(HIDE)rm -f $(NATIVEFILES) + $(HIDE)rm -f $(CMOFILES:%.cmo=%.cmx) +.PHONY: archclean + + +# Compilation rules ########################################################### + +$(MLIFILES:.mli=.cmi): %.cmi: %.mli + $(SHOW)'CAMLC -c $<' + $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< + +$(MLGFILES:.mlg=.ml): %.ml: %.mlg + $(SHOW)'COQPP $<' + $(HIDE)$(COQPP) $< + +# Stupid hack around a deficient syntax: we cannot concatenate two expansions +$(filter %.cmo, $(MLFILES:.ml=.cmo) $(MLGFILES:.mlg=.cmo)): %.cmo: %.ml + $(SHOW)'CAMLC -c $<' + $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $< + +# Same hack +$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml + $(SHOW)'CAMLOPT -c $(FOR_PACK) $<' + $(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $< + + +$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa + $(SHOW)'CAMLOPT -shared -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -linkall -shared -o $@ $< + +$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + +$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^ + + +$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa + $(SHOW)'CAMLOPT -shared -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -shared -linkall -o $@ $< + +$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx + $(SHOW)'CAMLOPT -a -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $< + +$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack + $(SHOW)'CAMLC -a -o $@' + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^ + +$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack + $(SHOW)'CAMLC -pack -o $@' + $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ + +$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack + $(SHOW)'CAMLOPT -pack -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^ + +# This rule is for _CoqProject with no .mllib nor .mlpack +$(filter-out $(MLLIBFILES:.mllib=.cmxs) $(MLPACKFILES:.mlpack=.cmxs) $(addsuffix .cmxs,$(PACKEDFILES)) $(addsuffix .cmxs,$(LIBEDFILES)),$(MLFILES:.ml=.cmxs) $(MLGFILES:.mlg=.cmxs)): %.cmxs: %.cmx + $(SHOW)'[deprecated,use-mllib-or-mlpack] CAMLOPT -shared -o $@' + $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \ + -shared -o $@ $< + +ifneq (,$(TIMING)) +TIMING_EXTRA = > $<.$(TIMING_EXT) +else +TIMING_EXTRA = +endif + +$(VOFILES): %.vo: %.v + $(SHOW)COQC $< + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(TIMING_ARG) $(COQFLAGS) $(COQLIBS) $< $(TIMING_EXTRA) + +# FIXME ?merge with .vo / .vio ? +$(GLOBFILES): %.glob: %.v + $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(VFILES:.v=.vio): %.vio: %.v + $(SHOW)COQC -vio $< + $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(VFILES:.v=.vos): %.vos: %.v + $(SHOW)COQC -vos $< + $(HIDE)$(TIMER) $(COQC) -vos $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(VFILES:.v=.vok): %.vok: %.v + $(SHOW)COQC -vok $< + $(HIDE)$(TIMER) $(COQC) -vok $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + +$(addsuffix .timing.diff,$(VFILES)): %.timing.diff : %.before-timing %.after-timing + $(SHOW)PYTHON TIMING-DIFF $*.{before,after}-timing + $(HIDE)$(MAKE) --no-print-directory -f "$(SELF)" print-pretty-single-time-diff BEFORE=$*.before-timing AFTER=$*.after-timing TIME_OF_PRETTY_BUILD_FILE="$@" + +$(BEAUTYFILES): %.v.beautified: %.v + $(SHOW)'BEAUTIFY $<' + $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $< + +$(TEXFILES): %.tex: %.v + $(SHOW)'COQDOC -latex $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ + +$(GTEXFILES): %.g.tex: %.v + $(SHOW)'COQDOC -latex -g $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@ + +$(HTMLFILES): %.html: %.v %.glob + $(SHOW)'COQDOC -html $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html $< -o $@ + +$(GHTMLFILES): %.g.html: %.v %.glob + $(SHOW)'COQDOC -html -g $<' + $(HIDE)$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@ + +# Dependency files ############################################################ + +ifndef MAKECMDGOALS + -include $(ALLDFILES) +else + ifneq ($(filter-out archclean clean cleanall printenv make-pretty-timed make-pretty-timed-before make-pretty-timed-after print-pretty-timed print-pretty-timed-diff print-pretty-single-time-diff,$(MAKECMDGOALS)),) + -include $(ALLDFILES) + endif +endif + +.SECONDARY: $(ALLDFILES) + +redir_if_ok = > "$@" || ( RV=$$?; rm -f "$@"; exit $$RV ) + +GENMLFILES:=$(MLGFILES:.mlg=.ml) +$(addsuffix .d,$(ALLSRCFILES)): $(GENMLFILES) + +$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLGFILES)): %.mlg.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml + $(SHOW)'CAMLDEP $<' + $(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) + +$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack + $(SHOW)'OCAMLLIBDEP $<' + $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok) + +# If this makefile is created using a _CoqProject we have coqdep get +# options from it. This avoids argument length limits for pathological +# projects. Note that extra options might be on the command line. +VDFILE_FLAGS:=$(if _CoqProject,-f _CoqProject,) $(CMDLINE_COQLIBS) $(CMDLINE_VFILES) + +$(VDFILE): $(VFILES) + $(SHOW)'COQDEP VFILES' + $(HIDE)$(COQDEP) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok) + +# Misc ######################################################################## + +byte: + $(HIDE)$(MAKE) all "OPT:=-byte" -f "$(SELF)" +.PHONY: byte + +opt: + $(HIDE)$(MAKE) all "OPT:=-opt" -f "$(SELF)" +.PHONY: opt + +# This is deprecated. To extend this makefile use +# extension points and Makefile.local +printenv:: + $(warning printenv is deprecated) + $(warning write extensions in Makefile.local or include Makefile.conf) + @echo 'LOCAL = $(LOCAL)' + @echo 'COQLIB = $(COQLIB)' + @echo 'DOCDIR = $(DOCDIR)' + @echo 'OCAMLFIND = $(OCAMLFIND)' + @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' + @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' + @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' + @echo 'OCAMLFIND = $(OCAMLFIND)' + @echo 'PP = $(PP)' + @echo 'COQFLAGS = $(COQFLAGS)' + @echo 'COQLIB = $(COQLIBS)' + @echo 'COQLIBINSTALL = $(COQLIBINSTALL)' + @echo 'COQDOCINSTALL = $(COQDOCINSTALL)' +.PHONY: printenv + +# Generate a .merlin file. If you need to append directives to this +# file you can extend the merlin-hook target in Makefile.local +.merlin: + $(SHOW)'FILL .merlin' + $(HIDE)echo 'FLG $(COQMF_CAMLFLAGS)' > .merlin + $(HIDE)echo 'B $(COQLIB)' >> .merlin + $(HIDE)echo 'S $(COQLIB)' >> .merlin + $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ + echo 'B $(COQLIB)$(d)' >> .merlin;) + $(HIDE)$(foreach d,$(COQ_SRC_SUBDIRS), \ + echo 'S $(COQLIB)$(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'B $(d)' >> .merlin;) + $(HIDE)$(foreach d,$(SRC_SUBDIRS), echo 'S $(d)' >> .merlin;) + $(HIDE)$(MAKE) merlin-hook -f "$(SELF)" +.PHONY: merlin + +merlin-hook:: + @# Extension point +.PHONY: merlin-hook + +# prints all variables +debug: + $(foreach v,\ + $(sort $(filter-out $(INITIAL_VARS) INITIAL_VARS,\ + $(.VARIABLES))),\ + $(info $(v) = $($(v)))) +.PHONY: debug + +.DEFAULT_GOAL := all + +# Local Variables: +# mode: makefile-gmake +# End: @@ -14,6 +14,8 @@ Require Import Bool List PArray Int63 Ring63 ZArith Psatz. Local Open Scope int63_scope. Local Open Scope array_scope. +Global Notation "[| x |]" := (φ x). + (** Lemmas about Bool *) diff --git a/src/SMT_terms.v b/src/SMT_terms.v index bf72333..f536bd6 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -105,7 +105,7 @@ Module Form. t_b.[i <- interp_aux (get t_b) (t_form.[i])]) 0 (length t_form) (make (length t_form) true). - Fixpoint lt_form i h {struct h} := + Definition lt_form i h := match h with | Fatom _ | Ftrue | Ffalse => true | Fnot2 _ l => Lit.blit l < i diff --git a/src/State.v b/src/State.v index 16868b7..ae69f37 100644 --- a/src/State.v +++ b/src/State.v @@ -239,7 +239,7 @@ Proof. rewrite <- eqb_spec;trivial. rewrite <- not_true_iff_false in H, H0. unfold is_true in *;rewrite ltb_spec in H |- *;rewrite eqb_spec in H0. - assert ([|x|] <> [|y|]) by (intros Heq;apply H0, to_Z_inj;trivial);omega. + assert ([|x|] <> [|y|]) by (intros Heq;apply H0, to_Z_inj;trivial);lia. Qed. @@ -358,7 +358,7 @@ Module C. intros rho resolve_correct Hc1;simpl in Hc1. induction c2;simpl;try discriminate. generalize (compare_spec' l1 a);destruct (l1 ?= a);intros;subst;simpl. - simpl in Hc1;destruct (Lit.interp rho a);simpl in *;auto. + simpl in Hc1;destruct (Lit.interp rho l1);simpl in *;auto. generalize (Lit.lxor_neg l1 a);destruct (l1 lxor a == 1);intros. rewrite or_correct. rewrite H1, Lit.interp_neg in Hc1;trivial;destruct (Lit.interp rho a). diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v index 72347e9..a7743b2 100644 --- a/src/bva/Bva_checker.v +++ b/src/bva/Bva_checker.v @@ -1305,7 +1305,7 @@ Proof. intros a bs. induction bs as [ | b ys IHys]. - intros. simpl in H. cut (i = n). intro Hn. rewrite Hn in H1. - contradict H1. omega. omega. + contradict H1. lia. lia. - intros. simpl in H0. case_eq (Lit.is_pos b). intros Heq0. rewrite Heq0 in H0. case_eq (t_form .[ Lit.blit b] ). intros i1 Heq1. rewrite Heq1 in H0. @@ -1336,7 +1336,7 @@ Proof. intros a bs. cut ((S k - S i)%nat = (k - i)%nat). intro ISki. specialize (@IHys Hd). now rewrite ISki in IHys. - now simpl. omega. + now simpl. lia. rewrite Hd. cut ((i0 - i0 = 0)%nat). intro Hi0. rewrite Hi0. simpl. @@ -1404,13 +1404,13 @@ Proof. intros a bs. now apply Nat.eqb_eq in Hif2. now apply Nat.eqb_eq in Hif1. - omega. + lia. destruct H1. specialize (@le_le_S_eq i i0). intros H11. specialize (@H11 H1). destruct H11. left. split. exact H5. exact H3. right. exact H5. - omega. + lia. intro H3. rewrite H3 in H0. now contradict H0. intros n0 Hn. rewrite Hn in H0. now contradict H0. intros n0 Hn. rewrite Hn in H0. now contradict H0. @@ -1451,7 +1451,7 @@ Proof. intros. cut ( (0 <= i0 < Datatypes.length bs)%nat). intro Hc3. specialize (@Hp Hc3). now rewrite Hc in Hp. - omega. omega. omega. + lia. lia. lia. Qed. @@ -1488,7 +1488,7 @@ Proof. intros a. cut ((0 < S (Datatypes.length xs))%nat). intro HS. specialize (@H2 HS). rewrite H2; apply f_equal. apply IHxs. intros. apply (@nth_eq0 i a b xs ys). - apply H. simpl. omega. omega. + apply H. simpl. lia. lia. Qed. Lemma is_even_0: is_even 0 = true. @@ -1632,7 +1632,7 @@ Proof. case (t_form .[ Lit.blit b]) in Hc; try now contradict Hc. case a in Hc; try now contradict Hc. exact Hc. case a in Hc; try now contradict Hc. exact Hc. - simpl in Hlen. omega. + simpl in Hlen. lia. Qed. Lemma prop_check_bbc2: forall l bs, check_bbc l bs = true -> @@ -2876,7 +2876,7 @@ Proof. intros bs1 bs2 bsres. specialize (IHbsres bs1 bs2 (n-1)%nat). simpl in H0. assert (length bs1 = (n-1)%nat). - { omega. } + { lia. } cut ( (BO_BVand (N.of_nat n - 1)) = (BO_BVand (N.of_nat (n - 1)))). @@ -2885,7 +2885,7 @@ Proof. intros bs1 bs2 bsres. rewrite H2. intros. specialize (IHbsres H H1). - simpl. rewrite IHbsres. omega. + simpl. rewrite IHbsres. lia. simpl. cut ((N.of_nat n - 1)%N = (N.of_nat (n - 1))). @@ -3003,7 +3003,7 @@ Proof. intros bs1 bs2 bsres. specialize (IHbsres bs1 bs2 (n-1)%nat). simpl in H0. assert (length bs1 = (n-1)%nat). - { omega. } + { lia. } cut ( (BO_BVor (N.of_nat n - 1)) = (BO_BVor (N.of_nat (n - 1)))). @@ -3012,7 +3012,7 @@ Proof. intros bs1 bs2 bsres. rewrite H2. intros. specialize (IHbsres H H1). - simpl. rewrite IHbsres. omega. + simpl. rewrite IHbsres. lia. simpl. cut ((N.of_nat n - 1)%N = (N.of_nat (n - 1))). @@ -3128,7 +3128,7 @@ Proof. intros bs1 bs2 bsres. specialize (IHbsres bs1 bs2 (n-1)%nat). simpl in H0. assert (length bs1 = (n-1)%nat). - { omega. } + { lia. } cut ( (BO_BVxor (N.of_nat n - 1)) = (BO_BVxor (N.of_nat (n - 1)))). @@ -3137,7 +3137,7 @@ Proof. intros bs1 bs2 bsres. rewrite H2. intros. specialize (IHbsres H H1). - simpl. rewrite IHbsres. omega. + simpl. rewrite IHbsres. lia. simpl. cut ((N.of_nat n - 1)%N = (N.of_nat (n - 1))). @@ -6501,7 +6501,7 @@ Proof. intro a. induction a as [ | xa xsa IHa ]. - intros. simpl. easy. - intros. - case b in *. simpl. rewrite IHa. simpl. omega. + case b in *. simpl. rewrite IHa. simpl. lia. simpl. case (k - 1 <? 0)%Z; simpl; now rewrite IHa. Qed. @@ -6509,9 +6509,9 @@ Lemma prop_mult_step3: forall k' a b res k, length (mult_step a b res k k') = (length res)%nat. Proof. intro k'. induction k'. - - intros. simpl. rewrite prop_mult_step_k_h_len. simpl. omega. + - intros. simpl. rewrite prop_mult_step_k_h_len. simpl. lia. - intros. simpl. - rewrite IHk'. rewrite prop_mult_step_k_h_len. simpl; omega. + rewrite IHk'. rewrite prop_mult_step_k_h_len. simpl; lia. Qed. Lemma prop_and_with_bit2: forall bs1 b, length (and_with_bit bs1 b) = length bs1. diff --git a/src/cnf/Cnf.v b/src/cnf/Cnf.v index 14e7bb9..c036bc8 100644 --- a/src/cnf/Cnf.v +++ b/src/cnf/Cnf.v @@ -35,10 +35,10 @@ Lemma get_or_of_imp : forall args i, Proof. unfold or_of_imp; intros args i H; case_eq (0 < PArray.length args). intro Heq; rewrite get_amapi. - replace (i == PArray.length args - 1) with false; auto; symmetry; rewrite eqb_false_spec; intro; subst i; unfold is_true in H; rewrite ltb_spec, (to_Z_sub_1 _ _ Heq) in H; omega. - rewrite ltb_spec; unfold is_true in H; rewrite ltb_spec, (to_Z_sub_1 _ _ Heq) in H; omega. + replace (i == PArray.length args - 1) with false; auto; symmetry; rewrite eqb_false_spec; intro; subst i; unfold is_true in H; rewrite ltb_spec, (to_Z_sub_1 _ _ Heq) in H; lia. + rewrite ltb_spec; unfold is_true in H; rewrite ltb_spec, (to_Z_sub_1 _ _ Heq) in H; lia. rewrite ltb_negb_geb; case_eq (PArray.length args <= 0); try discriminate; intros Heq _; assert (H1: PArray.length args = 0). - apply to_Z_inj; rewrite leb_spec in Heq; destruct (to_Z_bounded (PArray.length args)) as [H1 _]; change [|0|] with 0%Z in *; omega. + apply to_Z_inj; rewrite leb_spec in Heq; destruct (to_Z_bounded (PArray.length args)) as [H1 _]; change [|0|] with 0%Z in *; lia. rewrite !get_outofbound. rewrite default_amapi, H1; auto. rewrite H1; case_eq (i < 0); auto; intro H2; eelim ltb_0; eassumption. @@ -50,7 +50,7 @@ Lemma get_or_of_imp2 : forall args i, 0 < PArray.length args -> Proof. unfold or_of_imp; intros args i Heq Hi; rewrite get_amapi; subst i. rewrite Int63.eqb_refl; auto. - rewrite ltb_spec, (to_Z_sub_1 _ _ Heq); omega. + rewrite ltb_spec, (to_Z_sub_1 _ _ Heq); lia. Qed. Lemma afold_right_impb p a : @@ -497,7 +497,7 @@ Section CHECKER. exists (a.[i]);split;trivial. assert (H1: 0 < PArray.length a) by (apply (leb_ltb_trans _ i _); auto; apply leb_0); rewrite Int63.eqb_spec in Heq'; rewrite <- (get_or_of_imp2 H1 Heq'); apply to_list_In; rewrite length_or_of_imp; auto. exists (Lit.neg (a.[i]));rewrite Lit.interp_neg, Heq2;split;trivial. - assert (H1: i < PArray.length a - 1 = true) by (rewrite ltb_spec, (to_Z_sub_1 _ _ Hlt); rewrite eqb_false_spec in Heq'; assert (H1: [|i|] <> ([|PArray.length a|] - 1)%Z) by (intro H1; apply Heq', to_Z_inj; rewrite (to_Z_sub_1 _ _ Hlt); auto); rewrite ltb_spec in Hlt; omega); rewrite <- (get_or_of_imp H1); apply to_list_In; rewrite length_or_of_imp; auto. + assert (H1: i < PArray.length a - 1 = true) by (rewrite ltb_spec, (to_Z_sub_1 _ _ Hlt); rewrite eqb_false_spec in Heq'; assert (H1: [|i|] <> ([|PArray.length a|] - 1)%Z) by (intro H1; apply Heq', to_Z_inj; rewrite (to_Z_sub_1 _ _ Hlt); auto); rewrite ltb_spec in Hlt; lia); rewrite <- (get_or_of_imp H1); apply to_list_In; rewrite length_or_of_imp; auto. Qed. End CHECKER. diff --git a/src/configure.sh b/src/configure.sh deleted file mode 100755 index 7b0c264..0000000 --- a/src/configure.sh +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/sh - -coq_makefile -f _CoqProject -o Makefile -sed -i 's/^CAMLDONTLINK=unix,str$/CAMLDONTLINK=num,str,unix,dynlink,threads/' Makefile diff --git a/src/lia/Lia.v b/src/lia/Lia.v index f6e6520..4f5d9ef 100644 --- a/src/lia/Lia.v +++ b/src/lia/Lia.v @@ -13,7 +13,7 @@ Require Import Bool List Int63 Ring63 PArray ZArith. Require Import Misc State SMT_terms Euf. -Require Import RingMicromega ZMicromega Tauto Psatz. +Require Import RingMicromega ZMicromega Coq.micromega.Tauto Psatz. Local Open Scope array_scope. Local Open Scope int63_scope. @@ -532,15 +532,15 @@ Section certif. induction lvm;simpl;try discriminate. intros pvm Heq1 Heq. assert (1 < pvm)%positive. - rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;omega. + rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;lia. assert (Datatypes.length lvm = nat_of_P (Pos.pred pvm) - 1)%nat. rewrite Ppred_minus, Pminus_minus;trivial. - change (nat_of_P 1) with 1%nat ;try omega. + change (nat_of_P 1) with 1%nat ;try lia. revert Heq1. destruct (Atom.reflect_eqb h a);subst. - intros Heq1;inversion Heq1;clear Heq1;subst;omega. + intros Heq1;inversion Heq1;clear Heq1;subst;lia. intros Heq1;apply IHlvm in Heq1;trivial. - apply lt_trans with (1:= Heq1);omega. + apply lt_trans with (1:= Heq1);lia. Qed. Lemma build_pexpr_atom_aux_correct_z : @@ -578,10 +578,10 @@ Section certif. induction lvm;simpl;try discriminate. intros pvm p Heq1 Heq. assert (1 < pvm)%positive. - rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;omega. + rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;lia. assert (Datatypes.length lvm = nat_of_P (Pos.pred pvm) - 1)%nat. rewrite Ppred_minus, Pminus_minus;trivial. - change (nat_of_P 1) with 1%nat ;try omega. + change (nat_of_P 1) with 1%nat ;try lia. revert Heq1. destruct (Atom.reflect_eqb h a);subst. intros Heq1;inversion Heq1;clear Heq1;subst. @@ -589,8 +589,7 @@ Section certif. assert (1 < nat_of_P pvm)%nat by (rewrite Plt_lt in H;trivial). assert (W:=nat_of_P_pos (Pos.pred pvm)). assert (nat_of_P (pvm - Pos.pred pvm) - 1 = 0)%nat. - rewrite Pminus_minus;try omega. - apply Plt_lt;omega. + rewrite Pminus_minus;lia. rewrite H4;simpl. destruct (check_aux_interp_aux _ _ _ wf_t_atom _ _ H1) as (z,Hz). rewrite Hz;trivial. @@ -600,31 +599,31 @@ Section certif. assert (W1:= W);rewrite <- Plt_lt in W. rewrite !Pminus_minus;trivial. assert (W2:=nat_of_P_pos (Pos.pred pvm)). - omega. + lia. rewrite Plt_lt. - apply lt_trans with (1:= W1);omega. + apply lt_trans with (1:= W1);lia. rewrite H3;simpl;apply IHlvm;trivial. intros _ Heq;inversion Heq;clear Heq;subst;unfold wf_vmap; simpl;intros (Hwf1, Hwf2);repeat split;simpl. - rewrite Psucc_S; assert (W:= nat_of_P_pos pvm);omega. + rewrite Psucc_S; assert (W:= nat_of_P_pos pvm);lia. rewrite Hh;trivial. - rewrite Psucc_S;omega. + rewrite Psucc_S;lia. intros p Hlt; assert (nat_of_P (Pos.succ pvm - p) - 1 = S (nat_of_P (pvm - p) - 1))%nat. assert (W1:= Hlt);rewrite <- Plt_lt in W1. rewrite !Pminus_minus;trivial. - rewrite Psucc_S;omega. - rewrite Plt_lt, Psucc_S;omega. + rewrite Psucc_S;lia. + rewrite Plt_lt, Psucc_S;lia. rewrite H;trivial. unfold is_true;rewrite <- Zlt_is_lt_bool. - rewrite Zpos_succ_morphism;omega. + rewrite Zpos_succ_morphism;lia. destruct (check_aux_interp_aux _ _ _ wf_t_atom _ _ Hh) as (z,Hz). rewrite Hz;unfold interp_vmap;simpl. assert (nat_of_P (Pos.succ pvm - pvm) = 1%nat). rewrite Pplus_one_succ_l, Pminus_minus, Pplus_plus. - change (nat_of_P 1) with 1%nat;omega. + change (nat_of_P 1) with 1%nat;lia. rewrite Plt_lt, Pplus_plus. - change (nat_of_P 1) with 1%nat;omega. + change (nat_of_P 1) with 1%nat;lia. rewrite H;simpl;rewrite Hz;trivial. Qed. @@ -898,7 +897,7 @@ Transparent build_z_atom. apply leb_0. intros h vm vm' pe Hh. assert (W:=to_Z_bounded h);rewrite to_Z_0 in Hh. - elimtype False;omega. + elimtype False;lia. intros i cont Hpos Hlen Hrec. intros h vm vm' pe;unfold is_true;rewrite <-ltb_spec;intros. rewrite t_interp_wf;trivial. @@ -1150,14 +1149,14 @@ Qed. (* Fatom *) case_eq (build_formula vm h); try discriminate; intros [vm0 f] Heq H1 H2; inversion H1; subst vm0; subst bf; apply build_formula_correct; auto. (* Ftrue *) - intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [omega| ]; do 4 split; auto. + intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [lia| ]; do 4 split; auto. (* Ffalse *) - intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [omega| ]; do 3 (split; auto with smtcoq_core); discriminate. + intros H H1; inversion H; subst vm'; subst bf; split; auto; split; [lia| ]; do 3 (split; auto with smtcoq_core); discriminate. (* Fnot2 *) case_eq (build_var vm (Lit.blit l)); try discriminate; intros [vm0 f] Heq H H1; inversion H; subst vm0; subst bf; destruct (Hbv _ _ _ _ Heq H1) as [H2 [H3 [H4 [H5 H6]]]]; do 3 (split; auto); case_eq (Lit.is_pos l); [apply build_not2_pos_correct|apply build_not2_neg_correct]; auto. (* Fand *) simpl; unfold afold_left; rewrite !length_amap; case_eq (length l == 0); [ rewrite Int63.eqb_spec | rewrite eqb_false_spec, not_0_ltb ]; intro Hl. - intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [omega| ]; do 3 (split; auto with smtcoq_core). + intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [lia| ]; do 3 (split; auto with smtcoq_core). revert vm' bf; rewrite !get_amap by exact Hl; set (a := foldi _ _ _ _); set (b := foldi _ _ _ _); pattern (length l), a, b; subst a b; apply foldi_ind2. rewrite ltb_spec, to_Z_0 in Hl; rewrite leb_spec, to_Z_1; lia. intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto); unfold Lit.interp; rewrite Heq2; auto; simpl; split. @@ -1170,7 +1169,7 @@ Qed. simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; rewrite get_amap by exact H1; case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[ i]))); try rewrite andb_true_r; try rewrite andb_false_r; try (intros; split; auto with smtcoq_core); try discriminate; intros [H20 H21]; auto with smtcoq_core. (* For *) simpl; unfold afold_left; rewrite !length_amap; case_eq (length l == 0); [ rewrite Int63.eqb_spec | rewrite eqb_false_spec, not_0_ltb ]; intro Hl. - intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [omega| ]; do 3 (split; auto with smtcoq_core); discriminate. + intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [lia| ]; do 3 (split; auto with smtcoq_core); discriminate. revert vm' bf; rewrite !get_amap by exact Hl; set (a := foldi _ _ _ _); set (b := foldi _ _ _ _); pattern (length l), a, b; subst a b; apply foldi_ind2. rewrite ltb_spec, to_Z_0 in Hl; rewrite leb_spec, to_Z_1; lia. intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ 0]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ 0])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split. @@ -1183,7 +1182,7 @@ Qed. simpl; rewrite (interp_bformula_le _ _ H12 _ H8) in H9; rewrite <- H9; rewrite get_amap by exact H1; case_eq (Lit.is_pos (l .[ i])); intro Heq2; simpl; rewrite <- H14; unfold Lit.interp; rewrite Heq2; split; case (Var.interp rho (Lit.blit (l .[ i]))); try rewrite orb_false_r; try rewrite orb_true_r; auto with smtcoq_core; try (intros [H20|H20]; auto with smtcoq_core; discriminate); right; intro H20; discriminate. (* Fimp *) simpl; unfold afold_right; rewrite !length_amap; case_eq (length l == 0); [ rewrite Int63.eqb_spec | rewrite eqb_false_spec, not_0_ltb ]; intro Hl. - intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [omega| ]; do 3 (split; auto with smtcoq_core). + intro H; inversion H; subst vm'; subst bf; simpl; intro H1; split; auto with smtcoq_core; split; [lia| ]; do 3 (split; auto with smtcoq_core). revert vm' bf; rewrite !get_amap by (apply minus_1_lt; rewrite eqb_false_spec, not_0_ltb; exact Hl); set (a := foldi _ _ _ _); set (b := foldi _ _ _ _); pattern (length l), a, b; subst a b; apply foldi_ind2. rewrite ltb_spec, to_Z_0 in Hl; rewrite leb_spec, to_Z_1; lia. intros vm' bf; case_eq (build_var vm (Lit.blit (l .[ length l - 1]))); try discriminate; intros [vm0 f] Heq; case_eq (Lit.is_pos (l .[ length l - 1])); intros Heq2 H1 H2; inversion H1; subst vm'; subst bf; destruct (Hbv _ _ _ _ Heq H2) as [H10 [H11 [H12 [H13 H14]]]]; do 4 (split; auto with smtcoq_core); unfold Lit.interp; rewrite Heq2; auto with smtcoq_core; simpl; split. diff --git a/src/trace/coqInterface.ml b/src/trace/coqInterface.ml index 5aa1087..f11563c 100644 --- a/src/trace/coqInterface.ml +++ b/src/trace/coqInterface.ml @@ -184,8 +184,6 @@ type constr_expr = Constrexpr.constr_expr let error s = CErrors.user_err (Pp.str s) let warning n s = CWarnings.create ~name:n ~category:"SMTCoq plugin" Pp.str s -let extern_constr c = Constrextern.extern_constr true Environ.empty_env Evd.empty (EConstr.of_constr c) - let destruct_rel_decl r = Context.Rel.Declaration.get_name r, Context.Rel.Declaration.get_type r @@ -196,7 +194,7 @@ let ppconstr_lsimpleconstr = Ppconstr.lsimpleconstr let constrextern_extern_constr c = let env = Global.env () in - Constrextern.extern_constr false env (Evd.from_env env) (EConstr.of_constr c) + Constrextern.extern_constr ~inctx:false env (Evd.from_env env) (EConstr.of_constr c) let get_rel_dec_name = function | Context.Rel.Declaration.LocalAssum (n, _) | Context.Rel.Declaration.LocalDef (n, _, _) -> diff --git a/src/trace/coqInterface.mli b/src/trace/coqInterface.mli index 0b0914a..f450f6d 100644 --- a/src/trace/coqInterface.mli +++ b/src/trace/coqInterface.mli @@ -110,10 +110,9 @@ val set_evars_tac : constr -> tactic type constr_expr = Constrexpr.constr_expr val error : string -> 'a val warning : string -> string -> unit -val extern_constr : constr -> constr_expr val destruct_rel_decl : (constr, types) Context.Rel.Declaration.pt -> name * types val interp_constr : Environ.env -> Evd.evar_map -> constr_expr -> constr -val ppconstr_lsimpleconstr : Notation_gram.tolerability +val ppconstr_lsimpleconstr : Constrexpr.entry_relative_level val constrextern_extern_constr : constr -> constr_expr val get_rel_dec_name : (constr, types) Context.Rel.Declaration.pt -> name val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml index e655a9d..fba59e1 100644 --- a/src/trace/smtCommands.ml +++ b/src/trace/smtCommands.ml @@ -689,7 +689,7 @@ let gen_rel_name = let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma = let warn () = - CoqInterface.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr Environ.empty_env Evd.empty (CoqInterface.extern_constr clemma)))); + CoqInterface.warning "Lemma" ("Discarding the following lemma (unsupported): "^(SmtMisc.string_coq_constr clemma)); None in |