aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore2
-rw-r--r--INSTALL.md15
-rw-r--r--ci/manifest-sources-8.111
-rw-r--r--examples/Example.v2
-rw-r--r--src/Makefile153
-rw-r--r--src/Makefile.local4
-rw-r--r--src/Misc.v2
-rw-r--r--src/PropToBool.v4
-rw-r--r--src/SMT_terms.v2
-rw-r--r--src/State.v6
-rw-r--r--src/_CoqProject2
-rw-r--r--src/bva/Bva_checker.v32
-rw-r--r--src/cnf/Cnf.v10
-rw-r--r--src/lia/Lia.v47
-rw-r--r--src/trace/coqInterface.ml47
-rw-r--r--src/trace/coqInterface.mli9
-rw-r--r--src/trace/smtCommands.ml2
-rw-r--r--unit-tests/Makefile2
18 files changed, 202 insertions, 140 deletions
diff --git a/.gitignore b/.gitignore
index 0f92c0b..a83f570 100644
--- a/.gitignore
+++ b/.gitignore
@@ -17,6 +17,8 @@ setup.log
*.v.d
*.aux
*.vo
+*.vok
+*.vos
*.d
.lia.cache
.nia.cache
diff --git a/INSTALL.md b/INSTALL.md
index 2b83320..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.08 and < 4.10 and Coq version 8.10.*.
+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.09.0):
+Now you can install an OCaml compiler (we recommend 4.11.1):
```bash
-opam switch create ocaml-base-compiler.4.09.0
+opam switch create ocaml-base-compiler.4.11.1
```
### Install Coq
-After OCaml is installed, you can install Coq-8.10.2 through opam.
+After OCaml is installed, you can install Coq-8.12.1 through opam.
```bash
-opam install coq.8.10.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.10.2 coqide.8.10.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
@@ -132,6 +132,7 @@ but you might need to install some extra packages and libraries for your system
Compile and install SMTCoq by using the following commands in the src directory.
```bash
+./configure.sh
make
make install
```
diff --git a/ci/manifest-sources-8.11 b/ci/manifest-sources-8.11
index 043c626..b93f959 100644
--- a/ci/manifest-sources-8.11
+++ b/ci/manifest-sources-8.11
@@ -27,6 +27,7 @@ tasks:
cd smtcoq
git checkout coq-8.11
cd src
+ ./configure.sh
make
make install
cd ../..
diff --git a/examples/Example.v b/examples/Example.v
index b405206..cd53212 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -11,7 +11,7 @@
(* [Require Import SMTCoq.SMTCoq.] loads the SMTCoq library.
- If you are using native-coq instead of Coq 8.10, replace it with:
+ If you are using native-coq instead of Coq 8.11, replace it with:
Require Import SMTCoq.
*)
diff --git a/src/Makefile b/src/Makefile
index 5d24b0c..5653389 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -1,10 +1,13 @@
-###############################################################################
-## v # The Coq Proof Assistant ##
-## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
-## \VV/ # ##
-## // # ##
-###############################################################################
-## GNUMakefile for Coq 8.10.2
+##########################################################################
+## # 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)
@@ -51,7 +54,7 @@ Makefile.conf: _CoqProject
#
# 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 an for all.
+# 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).
@@ -63,12 +66,12 @@ VERBOSE ?=
TIMED?=
TIMECMD?=
# Use command time on linux, gtime on Mac OS
-TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)"
+TIMEFMT?="$@ (real: %e, user: %U, sys: %S, mem: %M ko)"
ifneq (,$(TIMED))
-ifeq (0,$(shell command time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+ifeq (0,$(shell command time -f "" true >/dev/null 2>/dev/null; echo $$?))
STDTIME?=command time -f $(TIMEFMT)
else
-ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?))
+ifeq (0,$(shell gtime -f "" true >/dev/null 2>/dev/null; echo $$?))
STDTIME?=gtime -f $(TIMEFMT)
else
STDTIME?=command time
@@ -78,6 +81,11 @@ else
STDTIME?=command time -f $(TIMEFMT)
endif
+ifneq (,$(COQBIN))
+# add an ending /
+COQBIN:=$(COQBIN)/
+endif
+
# Coq binaries
COQC ?= "$(COQBIN)coqc"
COQTOP ?= "$(COQBIN)coqtop"
@@ -86,6 +94,7 @@ 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"
@@ -95,7 +104,7 @@ BEFORE ?=
AFTER ?=
# FIXME this should be generated by Coq (modules already linked by Coq)
-CAMLDONTLINK=unix,str
+CAMLDONTLINK=num,str,unix,dynlink,threads
# OCaml binaries
CAMLC ?= "$(OCAMLFIND)" ocamlc -c
@@ -119,6 +128,14 @@ CAMLPKGS ?=
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
@@ -186,7 +203,7 @@ 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.10.2
+COQMAKEFILE_VERSION:=8.12.2
COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)/$(d)")
@@ -226,7 +243,7 @@ COQTOPINSTALL = $(call concat_path,$(DESTDIR),$(COQLIB)/toploop)
# 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 := .coqdeps
+VDFILE := .Makefile.d
ALLSRCFILES := \
$(MLGFILES) \
@@ -246,6 +263,7 @@ strip_dotslash = $(patsubst ./%,%,$(1))
with_undef = $(if $(filter-out undefined, $(origin $(1))),$($(1)))
VO = vo
+VOS = vos
VOFILES = $(VFILES:.v=.$(VO))
GLOBFILES = $(VFILES:.v=.glob)
@@ -266,7 +284,7 @@ CMIFILES = \
$(CMOFILES:.cmo=.cmi) \
$(MLIFILES:.mli=.cmi)
# the /if/ is because old _CoqProject did not list a .ml(pack|lib) but just
-# a .ml4 file
+# a .mlg file
CMXSFILES = \
$(MLPACKFILES:.mlpack=.cmxs) \
$(CMXAFILES:.cmxa=.cmxs) \
@@ -312,7 +330,7 @@ else
DO_NATDYNLINK =
endif
-ALLDFILES = $(addsuffix .d,$(ALLSRCFILES) $(VDFILE))
+ALLDFILES = $(addsuffix .d,$(ALLSRCFILES)) $(VDFILE)
# Compilation targets #########################################################
@@ -328,6 +346,31 @@ all.timing.diff:
$(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::
@@ -335,9 +378,9 @@ make-pretty-timed make-pretty-timed-before make-pretty-timed-after::
$(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) $(TIME_OF_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+ $(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) $(TIME_OF_BUILD_AFTER_FILE) $(TIME_OF_BUILD_BEFORE_FILE) $(TIME_OF_PRETTY_BOTH_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+ $(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'
@@ -349,7 +392,7 @@ print-pretty-single-time-diff::
$(HIDE)false
else
print-pretty-single-time-diff::
- $(HIDE)$(COQMAKE_BOTH_SINGLE_TIMING_FILES) --sort-by=$(TIMING_SORT_BY) $(AFTER) $(BEFORE) $(TIME_OF_PRETTY_BUILD_FILE) $(TIME_OF_PRETTY_BUILD_EXTRA_FILES)
+ $(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:
@@ -383,7 +426,11 @@ optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
.PHONY: optfiles
# FIXME, see Ralf's bugreport
-quick: $(VOFILES:.vo=.vio)
+# 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:
@@ -391,8 +438,9 @@ vio2vo:
-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
.PHONY: vio2vo
+# quick2vo is undocumented
quick2vo:
- $(HIDE)make -j $(J) quick
+ $(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; \
@@ -408,6 +456,12 @@ checkproofs:
-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
@@ -438,13 +492,13 @@ all.ps: $(VFILES)
$(SHOW)'COQDOC -ps $(GAL)'
$(HIDE)$(COQDOC) \
-toc $(COQDOCFLAGS) -ps $(GAL) $(COQDOCLIBS) \
- -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+ -o $@ `$(COQDEP) -sort $(VFILES)`
all.pdf: $(VFILES)
$(SHOW)'COQDOC -pdf $(GAL)'
$(HIDE)$(COQDOC) \
-toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \
- -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+ -o $@ `$(COQDEP) -sort $(VFILES)`
# FIXME: not quite right, since the output name is different
gallinahtml: GAL=-g
@@ -558,6 +612,8 @@ clean::
$(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)
@@ -576,6 +632,7 @@ cleanall:: clean
$(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::
@@ -590,7 +647,7 @@ archclean::
$(MLIFILES:.mli=.cmi): %.cmi: %.mli
$(SHOW)'CAMLC -c $<'
- $(HIDE)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
+ $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
$(MLGFILES:.mlg=.ml): %.ml: %.mlg
$(SHOW)'COQPP $<'
@@ -599,53 +656,53 @@ $(MLGFILES:.mlg=.ml): %.ml: %.mlg
# 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)$(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
+ $(HIDE)$(TIMER) $(CAMLC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $<
# Same hack
$(filter %.cmx, $(MLFILES:.ml=.cmx) $(MLGFILES:.mlg=.cmx)): %.cmx: %.ml
$(SHOW)'CAMLOPT -c $(FOR_PACK) $<'
- $(HIDE)$(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $<
+ $(HIDE)$(TIMER) $(CAMLOPTC) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) $(FOR_PACK) $<
$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
$(SHOW)'CAMLOPT -shared -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+ $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
-linkall -shared -o $@ $<
$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib
$(SHOW)'CAMLC -a -o $@'
- $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+ $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib
$(SHOW)'CAMLOPT -a -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+ $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $^
$(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmxa
$(SHOW)'CAMLOPT -shared -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+ $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
-shared -linkall -o $@ $<
$(MLPACKFILES:.mlpack=.cmxa): %.cmxa: %.cmx
$(SHOW)'CAMLOPT -a -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $<
+ $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -a -o $@ $<
$(MLPACKFILES:.mlpack=.cma): %.cma: %.cmo | %.mlpack
$(SHOW)'CAMLC -a -o $@'
- $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
+ $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) -a -o $@ $^
$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack
$(SHOW)'CAMLC -pack -o $@'
- $(HIDE)$(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
+ $(HIDE)$(TIMER) $(CAMLLINK) $(CAMLDEBUG) $(CAMLFLAGS) -pack -o $@ $^
$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
$(SHOW)'CAMLOPT -pack -o $@'
- $(HIDE)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) -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)$(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
+ $(HIDE)$(TIMER) $(CAMLOPTLINK) $(CAMLDEBUG) $(CAMLFLAGS) $(CAMLPKGS) \
-shared -o $@ $<
ifneq (,$(TIMING))
@@ -663,11 +720,19 @@ $(GLOBFILES): %.glob: %.v
$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
$(VFILES:.v=.vio): %.vio: %.v
- $(SHOW)COQC -quick $<
- $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $<
+ $(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 $<
+ $(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
@@ -720,21 +785,21 @@ $(addsuffix .d,$(MLFILES)): %.ml.d: %.ml
$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" $(redir_if_ok)
$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib
- $(SHOW)'COQDEP $<'
- $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
+ $(SHOW)'OCAMLLIBDEP $<'
+ $(HIDE)$(OCAMLLIBDEP) -c $(OCAMLLIBS) "$<" $(redir_if_ok)
$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
- $(SHOW)'COQDEP $<'
- $(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" $(redir_if_ok)
+ $(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).d: $(VFILES)
+$(VDFILE): $(VFILES)
$(SHOW)'COQDEP VFILES'
- $(HIDE)$(COQDEP) -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
+ $(HIDE)$(COQDEP) -vos -dyndep var $(VDFILE_FLAGS) $(redir_if_ok)
# Misc ########################################################################
diff --git a/src/Makefile.local b/src/Makefile.local
index 913f948..ab84471 100644
--- a/src/Makefile.local
+++ b/src/Makefile.local
@@ -29,6 +29,10 @@ cleanall::
CAMLLEX = $(CAMLBIN)ocamllex
CAMLYACC = $(CAMLBIN)ocamlyacc
+CAMLPKGS += -package num
+
+merlin-hook::
+ $(HIDE)echo 'PKG num' >> .merlin
%.ml : %.mll
$(CAMLLEX) $<
diff --git a/src/Misc.v b/src/Misc.v
index b3a0fc4..5ea1d14 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 *)
diff --git a/src/PropToBool.v b/src/PropToBool.v
index bdbfc8c..d71c81c 100644
--- a/src/PropToBool.v
+++ b/src/PropToBool.v
@@ -243,7 +243,7 @@ Ltac prop2bool_hyps Hs :=
Section Test.
Variable A : Type.
- Hypothesis basic : forall (l1 l2:list A), length (l1++l2) = length l1 + length l2.
+ Hypothesis basic : forall (l1 l2:list A), length (l1++l2) = (length l1 + length l2)%nat.
Hypothesis no_eq : forall (z1 z2:Z), (z1 < z2)%Z.
Hypothesis uninterpreted_type : forall (a:A), a = a.
Hypothesis bool_eq : forall (b:bool), negb (negb b) = b.
@@ -318,7 +318,7 @@ End MultipleCompDec.
polymorphism will be removed before *)
Section Poly.
Hypothesis basic : forall (A:Type) (l1 l2:list A),
- length (l1++l2) = length l1 + length l2.
+ length (l1++l2) = (length l1 + length l2)%nat.
Hypothesis uninterpreted_type : forall (A:Type) (a:A), a = a.
Goal True.
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 fb1c42f..4e133c6 100644
--- a/src/State.v
+++ b/src/State.v
@@ -10,7 +10,7 @@
(**************************************************************************)
-Require Import List Bool Int63 Psatz Ring63 PArray Omega Misc.
+Require Import List Bool Int63 Psatz Ring63 PArray Omega 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).
diff --git a/src/_CoqProject b/src/_CoqProject
index 2a883c8..9ac5799 100644
--- a/src/_CoqProject
+++ b/src/_CoqProject
@@ -9,6 +9,8 @@
########################################################################
## To generate the Makefile: ##
## coq_makefile -f Make -o Makefile ##
+## sed -i 's/^CAMLDONTLINK=unix,str$/CAMLDONTLINK=num,str,unix,dynlink,threads/' Makefile ##
+## WARNING: DO NOT FORGET THE SECOND LINE (see PR#62) ##
########################################################################
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/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 9b2c72c..f33f091 100644
--- a/src/trace/coqInterface.ml
+++ b/src/trace/coqInterface.ml
@@ -10,9 +10,6 @@
(**************************************************************************)
-open Entries
-
-
(* Constr generation and manipulation *)
type id = Names.variable
let mkId = Names.Id.of_string
@@ -50,47 +47,39 @@ let pr_constr_env env = Printer.pr_constr_env env Evd.empty
let pr_constr = pr_constr_env Environ.empty_env
-let mkUConst : Constr.t -> Safe_typing.private_constants Entries.definition_entry = fun c ->
+let mkUConst : Constr.t -> Evd.side_effects Declare.proof_entry = fun c ->
let env = Global.env () in
let evd = Evd.from_env env in
let evd, ty = Typing.type_of env evd (EConstr.of_constr c) in
- { Entries.const_entry_body = Future.from_val ((c, Univ.ContextSet.empty),
- Safe_typing.empty_private_constants);
- const_entry_secctx = None;
- const_entry_feedback = None;
- const_entry_type = Some (EConstr.Unsafe.to_constr ty); (* Cannot contain evars since it comes from a Constr.t *)
- const_entry_universes = Evd.univ_entry ~poly:false evd;
- const_entry_opaque = false;
- const_entry_inline_code = false }
+ Declare.definition_entry
+ ~opaque:false
+ ~inline:false
+ ~types:(EConstr.Unsafe.to_constr ty) (* Cannot contain evars since it comes from a Constr.t *)
+ ~univs:(Evd.univ_entry ~poly:false evd)
+ c
let mkTConst c noc ty =
let env = Global.env () in
let evd = Evd.from_env env in
let evd, _ = Typing.type_of env evd (EConstr.of_constr noc) in
- { const_entry_body = Future.from_val ((c, Univ.ContextSet.empty),
- Safe_typing.empty_private_constants);
- const_entry_secctx = None;
- const_entry_feedback = None;
- const_entry_type = Some ty;
- const_entry_universes = Evd.univ_entry ~poly:false evd;
- const_entry_opaque = false;
- const_entry_inline_code = false }
+ Declare.definition_entry
+ ~opaque:false
+ ~inline:false
+ ~types:ty
+ ~univs:(Evd.univ_entry ~poly:false evd)
+ c
(* TODO : Set -> Type *)
let declare_new_type t =
- let _ = ComAssumption.declare_assumption ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_entry Univ.ContextSet.empty) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make t) in
+ let _ = ComAssumption.declare_variable false ~kind:Decls.Definitional Constr.mkSet [] Glob_term.Explicit (CAst.make t) in
Constr.mkVar t
let declare_new_variable v constr_t =
- let env = Global.env () in
- let evd = Evd.from_env env in
- let evd, _ = Typing.type_of env evd (EConstr.of_constr constr_t) in
- let _ = ComAssumption.declare_assumption ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.univ_entry ~poly:false evd) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make v) in
+ let _ = ComAssumption.declare_variable false ~kind:Decls.Definitional constr_t [] Glob_term.Explicit (CAst.make v) in
Constr.mkVar v
let declare_constant n c =
- Declare.declare_constant n (DefinitionEntry c, Decl_kinds.IsDefinition Decl_kinds.Definition)
-
+ Declare.declare_constant ~name:n ~kind:(Decls.IsDefinition Decls.Definition) (Declare.DefinitionEntry c)
type cast_kind = Constr.cast_kind
@@ -163,8 +152,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
@@ -175,7 +162,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 0536ef1..af34d87 100644
--- a/src/trace/coqInterface.mli
+++ b/src/trace/coqInterface.mli
@@ -43,11 +43,11 @@ val mkArrow : types -> types -> constr
val pr_constr_env : Environ.env -> constr -> Pp.t
val pr_constr : constr -> Pp.t
-val mkUConst : constr -> Safe_typing.private_constants Entries.definition_entry
-val mkTConst : constr -> constr -> types -> Safe_typing.private_constants Entries.definition_entry
+val mkUConst : constr -> Evd.side_effects Declare.proof_entry
+val mkTConst : constr -> constr -> types -> Evd.side_effects Declare.proof_entry
val declare_new_type : id -> types
val declare_new_variable : id -> types -> constr
-val declare_constant : id -> Safe_typing.private_constants Entries.definition_entry -> Names.Constant.t
+val declare_constant : id -> Evd.side_effects Declare.proof_entry -> Names.Constant.t
type cast_kind
val vmcast : cast_kind
@@ -99,10 +99,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 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
diff --git a/unit-tests/Makefile b/unit-tests/Makefile
index b042078..bd271b3 100644
--- a/unit-tests/Makefile
+++ b/unit-tests/Makefile
@@ -53,4 +53,4 @@ clean: cleanvo
cleanvo:
- rm -rf *~ *.vo *.glob *.vio .*.aux .lia.cache
+ rm -rf *~ *.vo *.glob *.vio .*.aux .lia.cache *.vok *.vos
generated by cgit (git 2.34.1) at 2024-05-18 11:18:55 +0000