aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore1
-rw-r--r--INSTALL.md14
-rw-r--r--Makefile2
-rw-r--r--src/Makefile866
-rw-r--r--src/Makefile.local2
-rw-r--r--src/Misc.v26
-rw-r--r--src/SMT_terms.v2
-rw-r--r--src/State.v10
-rw-r--r--src/bva/BVList.v8
-rw-r--r--src/bva/Bva_checker.v32
-rw-r--r--src/cnf/Cnf.v10
-rwxr-xr-xsrc/configure.sh4
-rw-r--r--src/lia/Lia.v47
-rw-r--r--src/trace/coqInterface.ml4
-rw-r--r--src/trace/coqInterface.mli3
-rw-r--r--src/trace/smtCommands.ml2
16 files changed, 946 insertions, 87 deletions
diff --git a/.gitignore b/.gitignore
index 1c3eaea..a83f570 100644
--- a/.gitignore
+++ b/.gitignore
@@ -24,7 +24,6 @@ setup.log
.nia.cache
# targets of coq_makefile:
-src/Makefile
src/Makefile.conf
src/g_smtcoq.ml
diff --git a/INSTALL.md b/INSTALL.md
index 0667a05..3a16700 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -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
diff --git a/Makefile b/Makefile
index 5e3b013..c31aa9b 100644
--- a/Makefile
+++ b/Makefile
@@ -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:
diff --git a/src/Makefile.local b/src/Makefile.local
index 1985ef7..ab84471 100644
--- a/src/Makefile.local
+++ b/src/Makefile.local
@@ -23,7 +23,7 @@ clean::
cd ../unit-tests; make clean
cleanall::
- rm -f ../3rdparty/alt-ergo/smtlib2_lex.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_parse.mli .lia.cache Makefile.conf lfsc/lfscLexer.ml lfsc/lfscParser.ml lfsc/lfscParser.mli smtlib2/sExprLexer.ml smtlib2/sExprParser.ml smtlib2/sExprParser.mli verit/veritLexer.ml verit/veritParser.ml verit/veritParser.mli Makefile
+ rm -f ../3rdparty/alt-ergo/smtlib2_lex.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_parse.mli .lia.cache Makefile.conf lfsc/lfscLexer.ml lfsc/lfscParser.ml lfsc/lfscParser.mli smtlib2/sExprLexer.ml smtlib2/sExprParser.ml smtlib2/sExprParser.mli verit/veritLexer.ml verit/veritParser.ml verit/veritParser.mli
diff --git a/src/Misc.v b/src/Misc.v
index 82cc2c9..9a4a589 100644
--- a/src/Misc.v
+++ b/src/Misc.v
@@ -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 *)
@@ -87,20 +89,20 @@ Qed.
Lemma not_0_ltb : forall x, x <> 0 <-> 0 < x = true.
Proof.
intros x;rewrite ltb_spec, to_Z_0;assert (W:=to_Z_bounded x);split.
- intros Hd;assert ([|x|] <> 0)%Z;[ | omega].
+ intros Hd;assert ([|x|] <> 0)%Z;[ | lia].
intros Heq;elim Hd;apply to_Z_inj;trivial.
intros Hlt Heq;elimtype False.
- assert ([|x|] = 0)%Z;[ rewrite Heq, to_Z_0;trivial | omega].
+ assert ([|x|] = 0)%Z;[ rewrite Heq, to_Z_0;trivial | lia].
Qed.
Lemma ltb_0 : forall x, ~ (x < 0 = true).
Proof.
- intros x;rewrite ltb_spec, to_Z_0;destruct (to_Z_bounded x);omega.
+ intros x;rewrite ltb_spec, to_Z_0;destruct (to_Z_bounded x);lia.
Qed.
Lemma not_ltb_refl : forall i, ~(i < i = true).
Proof.
- intros;rewrite ltb_spec;omega.
+ intros;rewrite ltb_spec;lia.
Qed.
Lemma ltb_trans : forall x y z, x < y = true -> y < z = true -> x < z = true.
@@ -112,7 +114,7 @@ Lemma leb_ltb_eqb : forall x y, ((x <= y) = (x < y) || (x == y)).
Proof.
intros.
apply eq_true_iff_eq.
- rewrite leb_spec, orb_true_iff, ltb_spec, eqb_spec, <- to_Z_eq;omega.
+ rewrite leb_spec, orb_true_iff, ltb_spec, eqb_spec, <- to_Z_eq;lia.
Qed.
Lemma leb_ltb_trans : forall x y z, x <= y = true -> y < z = true -> x < z = true.
@@ -123,7 +125,7 @@ Qed.
Lemma to_Z_add_1 : forall x y, x < y = true -> [|x+1|] = ([|x|] + 1)%Z.
Proof.
intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y);
- rewrite ltb_spec;intros;rewrite add_spec, to_Z_1, Z.mod_small;omega.
+ rewrite ltb_spec;intros;rewrite add_spec, to_Z_1, Z.mod_small;lia.
Qed.
Lemma to_Z_add_1_wB : forall x, ([|x|] < wB - 1)%Z -> [|x + 1|] = ([|x|] + 1)%Z.
@@ -133,7 +135,7 @@ Qed.
Lemma leb_not_gtb : forall n m, m <= n = true -> ~(n < m = true).
Proof.
- intros n m; rewrite ltb_spec, leb_spec;omega.
+ intros n m; rewrite ltb_spec, leb_spec;lia.
Qed.
Lemma leb_negb_gtb : forall x y, x <= y = negb (y < x).
@@ -141,7 +143,7 @@ Proof.
intros x y;apply Bool.eq_true_iff_eq;split;intros.
apply Bool.eq_true_not_negb;apply leb_not_gtb;trivial.
rewrite Bool.negb_true_iff, <- Bool.not_true_iff_false in H.
- rewrite leb_spec; rewrite ltb_spec in H;omega.
+ rewrite leb_spec; rewrite ltb_spec in H;lia.
Qed.
Lemma ltb_negb_geb : forall x y, x < y = negb (y <= x).
@@ -152,7 +154,7 @@ Qed.
Lemma to_Z_sub_gt : forall x y, y <= x = true -> [|x - y|] = ([|x|] - [|y|])%Z.
Proof.
intros x y;assert (W:= to_Z_bounded x);assert (W0:= to_Z_bounded y);
- rewrite leb_spec;intros;rewrite sub_spec, Zmod_small;omega.
+ rewrite leb_spec;intros;rewrite sub_spec, Zmod_small;lia.
Qed.
Lemma to_Z_sub_1 : forall x y, y < x = true -> ([| x - 1|] = [|x|] - 1)%Z.
@@ -247,15 +249,15 @@ Proof.
assert (W1 : [|n|] <> 0%Z) by (intros Heq;apply n0;apply to_Z_inj;trivial).
assert (W2 := to_Z_bounded n);clear n0.
assert (W3 : [|n-1|] = ([|n|] - 1)%Z).
- rewrite sub_spec, to_Z_1, Zmod_small;trivial;omega.
+ rewrite sub_spec, to_Z_1, Zmod_small;trivial;lia.
assert (H1 : n = (n-1)+1).
apply to_Z_inj;rewrite add_spec, W3.
- rewrite Zmod_small;rewrite to_Z_1; omega.
+ rewrite Zmod_small;rewrite to_Z_1; lia.
case_eq ((n-1) < digits); intro l.
rewrite ltb_spec in l.
rewrite H1, <- !bit_half, H; trivial; rewrite ltb_spec; trivial.
assert ((digits <= n) = true).
- rewrite <- Bool.not_true_iff_false, ltb_spec in l; rewrite leb_spec;omega.
+ rewrite <- Bool.not_true_iff_false, ltb_spec in l; rewrite leb_spec;lia.
rewrite !bit_M;trivial.
Qed.
diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index 8c4ffa6..085c5f6 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 d8b1114..8b899f1 100644
--- a/src/State.v
+++ b/src/State.v
@@ -10,7 +10,7 @@
(**************************************************************************)
-Require Import List Bool Int63 Psatz Ring63 PArray Omega Misc Ring.
+Require Import List Bool Int63 Psatz Ring63 PArray Misc Ring.
(* Require Import AxiomesInt. *)
@@ -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).
@@ -674,8 +674,8 @@ Module S.
rewrite foldi_lt_r.
apply C.resolve_correct; [ apply Hv | ring_simplify (i + 1 - 1); exact Hc ].
rewrite ltb_spec, to_Z_add_1_wB, to_Z_1.
- rewrite leb_spec, to_Z_1 in Hi1; generalize (to_Z_bounded i); omega.
- rewrite ltb_spec in Hi2; generalize (to_Z_bounded (length r)); omega.
+ rewrite leb_spec, to_Z_1 in Hi1; generalize (to_Z_bounded i); lia.
+ rewrite ltb_spec in Hi2; generalize (to_Z_bounded (length r)); lia.
Qed.
(* Weakening *)
diff --git a/src/bva/BVList.v b/src/bva/BVList.v
index 025bbd2..4c28ece 100644
--- a/src/bva/BVList.v
+++ b/src/bva/BVList.v
@@ -589,7 +589,7 @@ Definition ult_list (x y: list bool) :=
(ult_list_big_endian (List.rev x) (List.rev y)).
-Fixpoint slt_list_big_endian (x y: list bool) :=
+Definition slt_list_big_endian (x y: list bool) :=
match x, y with
| nil, _ => false
| _ , nil => false
@@ -2103,7 +2103,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.
@@ -2117,8 +2117,8 @@ Lemma prop_mult_bool_step: forall k' a b res k,
length (mult_bool_step a b res k k') = (length res)%nat.
Proof. intro k'.
induction k'.
- - intros. simpl. rewrite prop_mult_bool_step_k_h_len. simpl. omega.
- - intros. simpl. rewrite IHk'. rewrite prop_mult_bool_step_k_h_len. simpl; omega.
+ - intros. simpl. rewrite prop_mult_bool_step_k_h_len. simpl. lia.
+ - intros. simpl. rewrite IHk'. rewrite prop_mult_bool_step_k_h_len. simpl; lia.
Qed.
Lemma and_with_bool_len: forall a b, length (and_with_bool a (nth 0 b false)) = length a.
diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v
index 55c002f..24917a8 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 d98c3d6..db6e689 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 0246799..f172e22 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 8b91225..b139d3e 100644
--- a/src/trace/coqInterface.ml
+++ b/src/trace/coqInterface.ml
@@ -153,8 +153,6 @@ let error s = CErrors.user_err (Pp.str s)
let anomaly s = CErrors.anomaly (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
@@ -165,7 +163,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 453bce1..f4fff30 100644
--- a/src/trace/coqInterface.mli
+++ b/src/trace/coqInterface.mli
@@ -100,10 +100,9 @@ type constr_expr = Constrexpr.constr_expr
val error : string -> 'a
val anomaly : 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 2108da4..27ba80c 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -681,7 +681,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
generated by cgit (git 2.34.1) at 2024-05-08 03:30:24 +0000