summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-19 13:13:14 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-19 13:13:14 +0100
commita0a94c1340a63cdb824507b973393882666ba52a (patch)
tree73aa4eb32cbd176379bc91b21c184e2a6882bfe3
parentcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (diff)
Imported Upstream version 8.2-1+dfsgupstream/8.2-1+dfsg
-rw-r--r--CHANGES7
-rw-r--r--INSTALL34
-rw-r--r--INSTALL.macosx5
-rw-r--r--KNOWN-BUGS20
-rw-r--r--Makefile.build72
-rw-r--r--Makefile.common15
-rw-r--r--README17
-rw-r--r--README.win22
-rw-r--r--checker/check_stat.ml4
-rw-r--r--checker/checker.ml4
-rw-r--r--checker/declarations.ml74
-rw-r--r--checker/declarations.mli5
-rw-r--r--checker/environ.ml3
-rw-r--r--checker/environ.mli18
-rw-r--r--checker/include176
-rw-r--r--checker/mod_checking.ml9
-rw-r--r--checker/modops.ml1
-rw-r--r--checker/safe_typing.ml6
-rw-r--r--checker/term.ml45
-rw-r--r--checker/term.mli7
-rw-r--r--checker/typeops.ml15
-rw-r--r--checker/validate.ml200
-rw-r--r--config/Makefile.template1
-rwxr-xr-xconfigure54
-rw-r--r--contrib/extraction/extraction.ml6
-rw-r--r--contrib/firstorder/unify.ml6
-rw-r--r--contrib/funind/functional_principles_proofs.ml16
-rw-r--r--contrib/interface/showproof.ml2
-rw-r--r--contrib/subtac/subtac_cases.ml11
-rw-r--r--contrib/subtac/subtac_obligations.ml2
-rw-r--r--contrib/xml/cic2acic.ml6
-rw-r--r--contrib/xml/doubleTypeInference.ml8
-rw-r--r--dev/base_include1
-rw-r--r--ide/coq.icobin0 -> 11326 bytes
-rwxr-xr-xinstall.sh6
-rw-r--r--interp/notation.ml6
-rw-r--r--kernel/closure.ml34
-rw-r--r--kernel/closure.mli11
-rw-r--r--kernel/reduction.ml40
-rw-r--r--kernel/reduction.mli19
-rw-r--r--lib/envars.ml5
-rw-r--r--lib/util.ml35
-rw-r--r--lib/util.mli17
-rw-r--r--library/declaremods.ml3
-rw-r--r--library/libnames.ml22
-rw-r--r--library/library.ml4
-rw-r--r--man/coqchk.186
-rw-r--r--pretyping/cases.ml12
-rw-r--r--pretyping/cbv.ml12
-rw-r--r--pretyping/cbv.mli4
-rw-r--r--pretyping/classops.ml4
-rw-r--r--pretyping/clenv.ml8
-rw-r--r--pretyping/evarconv.ml35
-rw-r--r--pretyping/evarutil.ml26
-rw-r--r--pretyping/indrec.ml6
-rw-r--r--pretyping/reductionops.ml232
-rw-r--r--pretyping/reductionops.mli27
-rw-r--r--pretyping/retyping.ml6
-rw-r--r--pretyping/tacred.ml63
-rw-r--r--pretyping/unification.ml31
-rw-r--r--proofs/logic.ml8
-rw-r--r--proofs/refiner.ml4
-rw-r--r--proofs/tacmach.ml4
-rw-r--r--tactics/class_tactics.ml48
-rw-r--r--tactics/decl_proof_instr.ml6
-rw-r--r--tactics/equality.ml6
-rw-r--r--tactics/leminv.ml5
-rw-r--r--tactics/tactics.ml9
-rw-r--r--test-suite/complexity/unification.v51
-rw-r--r--theories/Numbers/Cyclic/Int31/Cyclic31.v9
-rw-r--r--theories/Reals/RIneq.v4
-rw-r--r--tools/coq_makefile.ml43
72 files changed, 1143 insertions, 600 deletions
diff --git a/CHANGES b/CHANGES
index 035579cd..494575fa 100644
--- a/CHANGES
+++ b/CHANGES
@@ -489,9 +489,10 @@ Miscellaneous
"Test Printing Let for ref" and "Test Printing If for ref".
- An overhauled build system (new Makefiles); see dev/doc/build-system.txt.
- Add -browser option to configure script.
-- Build a shared library for the C part of Coq, and use it by default.
- Bytecode executables are now pure. The behaviour is configurable with
- the -coqrunbyteflags configure option.
+- Build a shared library for the C part of Coq, and use it by default on
+ non-(Windows or MacOS) systems. Bytecode executables are now pure. The
+ behaviour is configurable with -coqrunbyteflags, -coqtoolsbyteflags and
+ -custom configure options.
- Complexity tests can be skipped by setting the environment variable
COQTEST_SKIPCOMPLEXITY.
diff --git a/INSTALL b/INSTALL
index 626417d6..47d2cb2e 100644
--- a/INSTALL
+++ b/INSTALL
@@ -71,10 +71,12 @@ WHAT DO YOU NEED ?
- a C compiler
- - for Coqide, the Lablgtk development files, and the GTK libraries, see INSTALL.ide for more details
+ - for Coqide, the Lablgtk development files, and the GTK
+ libraries, see INSTALL.ide for more details
- By FTP, Coq comes as a single compressed tar-file. You have
- probably already decompressed it if you are reading this document.
+ Coq sources distribution comes as a single compressed tar-file. You
+ have probably already decompressed it if you are reading this
+ document.
QUICK INSTALLATION PROCEDURE.
@@ -99,21 +101,18 @@ INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
bigger), you will also need the "ocamlopt" (or its native code version
"ocamlopt.opt") command.
-2- Check that you have Camlp4 installed on your
- computer and that the command "camlp4" lies in a directory which
- is present in your $PATH environment variable path.
- (You need Camlp4 in both bytecode and native versions if
- your platform supports it).
-
- Note: in the latest ocaml distributions, camlp4 comes with ocaml so
- you do not have to check this point anymore.
+2- If you are using OCaml version >= 3.10.0, check that you have
+ Camlp5 installed on your computer and that the command "camlp5"
+ lies in a directory which is present in your $PATH environment
+ variable path. (You need Camlp5 in both bytecode and native
+ versions if your platform supports it).
3- The uncompression and un-tarring of the distribution file gave birth
to a directory named "coq-8.xx". You can rename this directory and put
it wherever you want. Just keep in mind that you will need some spare
- space during the compilation (reckon on about 50 Mb of disk space
+ space during the compilation (reckon on about 250 Mb of disk space
for the whole system in native-code compilation). Once installed, the
- binaries take about 14 Mb, and the library about 9 Mb.
+ binaries take about 65 Mb, and the library about 60 Mb.
4- First you need to configure the system. It is done automatically with
the command:
@@ -313,12 +312,9 @@ MOVING BINARIES OR LIBRARY.
Error: Can't find file initial.coq on loadpath
If you really have (or want) to move the binaries or the library, then
- you have to indicate their new places to Coq, using the options -bindir (for
- the binaries directory) and -libdir (for the standard library directory) :
-
- coqtop -bindir <new directory> -libdir <new directory>
+ you have to indicate where Coq will find the libraries:
- See also next section.
+ coqtop -coqlib <directory>
DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
@@ -344,6 +340,6 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
where <path> is the directory where the dllcoqrun.so is installed;
- (not recommended) compile bytecode executables with a custom OCaml
runtime by using:
- ./configure -coqrunbyteflags -custom ...
+ ./configure -custom ...
be aware that stripping executables generated this way, or performing
other executable-specific operations, will make them useless.
diff --git a/INSTALL.macosx b/INSTALL.macosx
index 121a3e0b..fc33351a 100644
--- a/INSTALL.macosx
+++ b/INSTALL.macosx
@@ -16,5 +16,6 @@ team. To use the MacOS X package,:
can be used from a Terminal window: the interactive toplevel is
named coqtop and the compiler is coqc.
-If you have any trouble with this installation, please contact:
-coq-bugs@pauillac.inria.fr.
+If you have any trouble with this installation, please consider using
+our bug tracking system to report bug (see
+http://logical.saclay.inria.fr/coq-bugs).
diff --git a/KNOWN-BUGS b/KNOWN-BUGS
deleted file mode 100644
index 774d181c..00000000
--- a/KNOWN-BUGS
+++ /dev/null
@@ -1,20 +0,0 @@
- THIS IS A LIST OF KNOWN BUGS OF COQ V7.0
-
-- Realizer and Program/Program_all are not available
-
-- Local definitions in Record/Structure are not allowed
-
-- Alias of pattern with dependent types are not supported
-
-- Tokens with both symbols and letters are not supported
-
-- No consistency check is done when requiring a module (that is, a
- module can be compiled with logical name Mycontrib.Arith.Plus but
- required with name HisContrib.Zarith.Plus).
-
-- The syntax "Specialize num ident" is temporarily not accepted
- outside "Tactic Definition". Syntax "Specialize ident" is OK.
-
-- New Induction fails for mutual inductive elimination
-
-- Elim fails with eliminators not imported \ No newline at end of file
diff --git a/Makefile.build b/Makefile.build
index 0d0125ca..19f13f15 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -6,7 +6,7 @@
# # GNU Lesser General Public License Version 2.1 #
#######################################################################
-# $Id: Makefile.build 11858 2009-01-26 13:27:23Z notin $
+# $Id: Makefile.build 11935 2009-02-17 16:14:07Z notin $
# Makefile for Coq
@@ -197,7 +197,7 @@ $(CHICKENOPT): checker/check.cmxa checker/main.ml
$(CHICKENBYTE): checker/check.cma checker/main.ml
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^
+ $(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^
$(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE)
@@ -501,11 +501,13 @@ install-pcoq-manpages:
# tests
###########################################################################
+VALIDOPTS=-silent -o -m
+
validate:: $(BESTCHICKEN) $(ALLVO)
$(SHOW)'COQCHK <theories & contrib>'
- $(HIDE)$(BESTCHICKEN) -boot -o -m $(ALLMODS)
+ $(HIDE)$(BESTCHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
-check:: world
+check:: world validate
cd test-suite; \
env COQBIN=../bin COQLIB=.. ./check -$(BEST) | tee check.log
if grep -F 'Error!' test-suite/check.log ; then false; fi
@@ -590,29 +592,71 @@ printers: $(DEBUGPRINTERS)
tools:: $(TOOLS) $(DEBUGPRINTERS)
+ifeq ($(BEST),opt)
+$(COQDEP): $(COQDEPCMX)
+ $(SHOW)'OCAMLOPT -o $@'
+ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa $^ $(OSDEPLIBS)
+ $(STRIP) $@
+else
$(COQDEP): $(COQDEPCMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ $(OSDEPLIBS)
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ $(OSDEPLIBS)
+endif
+ifeq ($(BEST),opt)
+$(GALLINA): $(GALLINACMX)
+ $(SHOW)'OCAMLOPT -o $@'
+ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ $(GALLINACMX)
+ $(STRIP) $@
+else
$(GALLINA): $(GALLINACMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ $(GALLINACMO)
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(GALLINACMO)
+endif
+ifeq ($(BEST),opt)
+$(COQMAKEFILE): tools/coq_makefile.cmx config/coq_config.cmx
+ $(SHOW)'OCAMLOPT -o $@'
+ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa config/coq_config.cmx tools/coq_makefile.cmx
+ $(STRIP) $@
+else
$(COQMAKEFILE): tools/coq_makefile.cmo config/coq_config.cmo
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma config/coq_config.cmo tools/coq_makefile.cmo
+endif
+ifeq ($(BEST),opt)
+$(COQTEX): tools/coq-tex.cmx
+ $(SHOW)'OCAMLOPT -o $@'
+ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa tools/coq-tex.cmx
+ $(STRIP) $@
+else
$(COQTEX): tools/coq-tex.cmo
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma tools/coq-tex.cmo
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma tools/coq-tex.cmo
+endif
+ifeq ($(BEST),opt)
+$(COQWC): tools/coqwc.cmx
+ $(SHOW)'OCAMLOPT -o $@'
+ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ tools/coqwc.cmx
+ $(STRIP) $@
+else
$(COQWC): tools/coqwc.cmo
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ tools/coqwc.cmo
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ tools/coqwc.cmo
+endif
+ifeq ($(BEST),opt)
+$(COQDOC): $(COQDOCCMX)
+ $(SHOW)'OCAMLOPT -o $@'
+ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa $(COQDOCCMX)
+ $(STRIP) $@
+else
$(COQDOC): $(COQDOCCMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $(COQDOCCMO)
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ str.cma unix.cma $(COQDOCCMO)
+endif
###########################################################################
# Installation
@@ -639,13 +683,13 @@ install-binaries:: install-$(BEST) install-tools
install-byte::
$(MKDIR) $(FULLBINDIR)
- $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(FULLBINDIR)
- cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE)
+ $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(CHICKEN) $(FULLBINDIR)
+ cd $(FULLBINDIR); ln -sf coqtop.byte$(EXE) coqtop$(EXE); ln -sf coqchk.byte$(EXE) coqchk$(EXE)
install-opt::
$(MKDIR) $(FULLBINDIR)
- $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(FULLBINDIR)
- cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE)
+ $(INSTALLBIN) $(COQMKTOP) $(COQC) $(COQTOPBYTE) $(COQTOPOPT) $(CHICKEN) $(CHICKENOPT) $(FULLBINDIR)
+ cd $(FULLBINDIR); ln -sf coqtop.opt$(EXE) coqtop$(EXE); ln -sf coqchk.opt$(EXE) coqchk$(EXE)
install-tools::
$(MKDIR) $(FULLBINDIR)
diff --git a/Makefile.common b/Makefile.common
index 1889afc8..15faace0 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -66,8 +66,7 @@ COQTEX:=bin/coq-tex$(EXE)
COQWC:=bin/coqwc$(EXE)
COQDOC:=bin/coqdoc$(EXE)
-TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) \
- $(COQWC) $(COQDOC)
+TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC)
###########################################################################
# Documentation
@@ -404,11 +403,15 @@ CSDPCERTCMX:= $(CSDPCERTCMO:.cmo=.cmx)
DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma
COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep.cmo
+COQDEPCMX:=$(COQDEPCMO:.cmo=.cmx)
+
GALLINACMO:=tools/gallina_lexer.cmo tools/gallina.cmo
+GALLINACMX:=$(GALLINACMO:.cmo=.cmx)
+
COQDOCCMO:=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \
tools/coqdoc/index.cmo tools/coqdoc/output.cmo \
tools/coqdoc/pretty.cmo tools/coqdoc/main.cmo
-
+COQDOCCMX:=$(COQDOCCMO:.cmo=.cmx)
# checker
@@ -418,15 +421,15 @@ MCHECKER:=\
lib/flags.cmo lib/util.cmo lib/option.cmo lib/hashcons.cmo \
lib/system.cmo lib/envars.cmo \
lib/predicate.cmo lib/rtree.cmo \
- kernel/names.cmo kernel/univ.cmo \
- kernel/esubst.cmo checker/term.cmo \
+ kernel/names.cmo kernel/univ.cmo kernel/esubst.cmo \
+ checker/validate.cmo \
+ checker/term.cmo \
checker/declarations.cmo checker/environ.cmo \
checker/closure.cmo checker/reduction.cmo \
checker/type_errors.cmo \
checker/modops.cmo \
checker/inductive.cmo checker/typeops.cmo \
checker/indtypes.cmo checker/subtyping.cmo checker/mod_checking.cmo \
- checker/validate.cmo \
checker/safe_typing.cmo checker/check.cmo \
checker/check_stat.cmo checker/checker.cmo
diff --git a/README b/README
index 86783630..5cf88c1d 100644
--- a/README
+++ b/README
@@ -11,9 +11,8 @@ INSTALLATION.
DOCUMENTATION.
==============
- The documentation of Coq V8.2 is available by anonymous ftp (see below),
- in a directory doc/. It is also available on Coq web site at
- http://coq.inria.fr/doc-eng.html.
+ The documentation of Coq V8.2 is available online from the Coq web
+ site (see http://coq.inria.fr)
CHANGES.
@@ -27,10 +26,10 @@ CHANGES.
AVAILABILITY.
=============
- Coq is available by anonymous FTP on ftp.inria.fr:
+ Coq is available as a precompiled package from the major linux
+ distributions. It is also available for Windows and Mac OS systems
+ from the Coq web site (see http://coq.inria.fr).
- host: ftp.inria.fr (192.93.2.54)
- directory: INRIA/LogiCal/coq/
THE COQ CLUB.
=============
@@ -68,11 +67,7 @@ BUGS REPORT.
Send your bug reports by filling a form at
- http://coq.inria.fr/bin/coq-bugs
-
- or by E-mail to
-
- coq-bugs@coq.inria.fr
+ http://logical.saclay.inria.fr/coq-bugs
To be effective, bug reports should mention the Caml version used
to compile and run Coq, the Coq version (coqtop -v), the configuration
diff --git a/README.win b/README.win
index af1df482..da1a456c 100644
--- a/README.win
+++ b/README.win
@@ -1,7 +1,7 @@
THE COQ V8.2 SYSTEM
===================
- This file contains remarks specific to the windows port of Coq.
+ This file contains remarks specific to the Windows port of Coq.
INSTALLATION.
=============
@@ -16,12 +16,19 @@ default).
COMPILATION.
============
- If you want to install coq, you had better transfer the precompiled
+ If you want to install Coq, you had better transfer the precompiled
distribution. If you really need to recompile under Windows, here
are some indications:
- 1- Install ocaml for Windows (MinGW port), preferably version 3.09.3.
+ 1- Install OCaml for Windows (MinGW port), preferably version 3.11.0.
See: http://caml.inria.fr
+
+ If you choose OCaml 3.11.0, you also need to install FlexDLL.
+ See: http://alain.frisch.fr/flexdll.html
+
+ As shell script really dislikes space character within file
+ names, we strongly advise you to install OCaml to a path not
+ containing spaces, like 'C:\OCaml'
2- Install a shell environment with at least:
- a C compiler (gcc),
@@ -31,19 +38,22 @@ COMPILATION.
(official packages are made using Cygwin) See:
http://www.cygwin.com
- 3- In order to compile Coqide, you will need the LablGTK library
+ 3- If using OCaml version >= 3.10.0, you have to install Camlp5.
+ See http://pauillac.inria.fr/~ddr/camlp5/
+
+ 4- In order to compile Coqide, you will need the LablGTK library
See: http://wwwfun.kurims.kyoto-u.ac.jp/soft/olabl/lablgtk.html
You also need to install the GTK libraries for Windows (see the
installation instruction for LablGTK)
- 4- In a shell window, type successively
+ 5- In a shell window, type successively
./configure
make world
make install
- 5- Though not nescessary, you can find useful:
+ 6- Though not nescessary, you can find useful:
- Windows version of (X)Emacs: it is a powerful environment for
developpers with coloured syntax, modes for compilation and debug,
and many more. It is free. See: http://www.gnu.org/software.
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 96366594..6ea153a3 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -55,7 +55,7 @@ let print_context env =
env_stratification=
{env_universes=univ; env_engagement=engt}} = env in
msgnl(hov 0
- (str"CONTEXT SUMMARY" ++ fnl() ++
+ (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
str"===============" ++ fnl() ++ fnl() ++
str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++
str "* " ++ hov 0 (pr_ax csts) ++
@@ -65,5 +65,3 @@ let print_context env =
let stats () =
print_context (Safe_typing.get_env());
print_memory_stat ()
-
-let _ = at_exit stats
diff --git a/checker/checker.ml b/checker/checker.ml
index 3d928933..70e2eb97 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -256,7 +256,7 @@ let rec explain_exn = function
| Not_found ->
hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report ())
| Failure s ->
- hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report ())
+ hov 0 (str "Failure: " ++ str s ++ report ())
| Invalid_argument s ->
hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report ())
| Sys.Break ->
@@ -385,4 +385,4 @@ let run () =
flush_all();
exit 1)
-let start () = init(); run(); exit 0
+let start () = init(); run(); Check_stat.stats(); exit 0
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 2cf3854a..c6a7b4b4 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -1,6 +1,7 @@
open Util
open Names
open Term
+open Validate
(* Bytecode *)
type values
@@ -11,17 +12,22 @@ type action
type retroknowledge
type engagement = ImpredicativeSet
+let val_eng = val_enum "eng" 1
type polymorphic_arity = {
poly_param_levels : Univ.universe option list;
poly_level : Univ.universe;
}
+let val_pol_arity =
+ val_tuple"polyorphic_arity"[|val_list(val_opt val_univ);val_univ|]
type constant_type =
| NonPolymorphicType of constr
| PolymorphicArity of rel_context * polymorphic_arity
+let val_cst_type =
+ val_sum "constant_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|]
type substitution_domain =
@@ -29,6 +35,9 @@ type substitution_domain =
| MBI of mod_bound_id
| MPI of module_path
+let val_subst_dom =
+ val_sum "substitution_domain" 0 [|[|val_uid|];[|val_uid|];[|val_mp|]|]
+
module Umap = Map.Make(struct
type t = substitution_domain
let compare = Pervasives.compare
@@ -39,6 +48,13 @@ type resolver
type substitution = (module_path * resolver option) Umap.t
type 'a subst_fun = substitution -> 'a -> 'a
+let val_res = val_opt no_val
+
+let val_subst =
+ val_map ~name:"substitution"
+ val_subst_dom (val_tuple "substition range" [|val_mp;val_res|])
+
+
let fold_subst fs fb fp =
Umap.fold
(fun k (mp,_) acc ->
@@ -360,6 +376,11 @@ let force_constr = force subst_mps
type constr_substituted = constr substituted
+let val_cstr_subst =
+ val_ref
+ (val_sum "constr_substituted" 0
+ [|[|val_constr|];[|val_subst;val_constr|]|])
+
let subst_constr_subst = subst_substituted
type constant_body = {
@@ -372,6 +393,11 @@ type constant_body = {
const_opaque : bool;
const_inline : bool}
+let val_cb = val_tuple "constant_body"
+ [|val_nctxt;val_opt val_cstr_subst; val_cst_type;no_val;val_cstrs;
+ val_bool; val_bool |]
+
+
let subst_rel_declaration sub (id,copt,t as x) =
let copt' = Option.smartmap (subst_mps sub) copt in
let t' = subst_mps sub t in
@@ -383,6 +409,8 @@ type recarg =
| Norec
| Mrec of int
| Imbr of inductive
+let val_recarg = val_sum "recarg" 1 (* Norec *)
+ [|[|val_int|] (* Mrec *);[|val_ind|] (* Imbr *)|]
let subst_recarg sub r = match r with
| Norec | Mrec _ -> r
@@ -390,6 +418,12 @@ let subst_recarg sub r = match r with
if kn==kn' then r else Imbr (kn',i)
type wf_paths = recarg Rtree.t
+let val_wfp = val_rec_sum "wf_paths" 0
+ (fun val_wfp ->
+ [|[|val_int;val_int|]; (* Rtree.Param *)
+ [|val_recarg;val_array val_wfp|]; (* Rtree.Node *)
+ [|val_int;val_array val_wfp|] (* Rtree.Rec *)
+ |])
let mk_norec = Rtree.mk_node Norec [||]
@@ -417,10 +451,14 @@ type monomorphic_inductive_arity = {
mind_user_arity : constr;
mind_sort : sorts;
}
+let val_mono_ind_arity =
+ val_tuple"monomorphic_inductive_arity"[|val_constr;val_sort|]
type inductive_arity =
| Monomorphic of monomorphic_inductive_arity
| Polymorphic of polymorphic_arity
+let val_ind_arity = val_sum "inductive_arity" 0
+ [|[|val_mono_ind_arity|];[|val_pol_arity|]|]
type one_inductive_body = {
@@ -471,6 +509,12 @@ type one_inductive_body = {
mind_reloc_tbl : reloc_table;
}
+let val_one_ind = val_tuple "one_inductive_body"
+ [|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr;
+ val_int; val_list val_sortfam;val_array val_constr;val_array val_int;
+ val_wfp; val_int; val_int; no_val|]
+
+
type mutual_inductive_body = {
(* The component of the mutual inductive block *)
@@ -503,6 +547,10 @@ type mutual_inductive_body = {
(* Source of the inductive block when aliased in a module *)
mind_equiv : kernel_name option
}
+let val_ind_pack = val_tuple "mutual_inductive_body"
+ [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt;
+ val_int; val_int; val_rctxt;val_cstrs;val_opt val_kn|]
+
let subst_arity sub = function
| NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
@@ -558,6 +606,8 @@ let subst_mind sub mib =
(* Modules *)
+(* Whenever you change these types, please do update the validation
+ functions below *)
type structure_field_body =
| SFBconst of constant_body
| SFBmind of mutual_inductive_body
@@ -592,6 +642,30 @@ and module_type_body =
typ_strength : module_path option;
typ_alias : substitution}
+(* the validation functions: *)
+let rec val_sfb o = val_sum "struct_field_body" 0
+ [|[|val_cb|]; (* SFBconst *)
+ [|val_ind_pack|]; (* SFBmind *)
+ [|val_module|]; (* SFBmodule *)
+ [|val_mp;val_opt val_seb;val_opt val_cstrs|]; (* SFBalias *)
+ [|val_modtype|] (* SFBmodtype *)
+ |] o
+and val_sb o = val_list (val_tuple"label*sfb"[|val_id;val_sfb|]) o
+and val_seb o = val_sum "struct_expr_body" 0
+ [|[|val_mp|]; (* SEBident *)
+ [|val_uid;val_modtype;val_seb|]; (* SEBfunctor *)
+ [|val_uid;val_sb|]; (* SEBstruct *)
+ [|val_seb;val_seb;val_cstrs|]; (* SEBapply *)
+ [|val_seb;val_with|] (* SEBwith *)
+ |] o
+and val_with o = val_sum "with_declaration_body" 0
+ [|[|val_list val_id;val_mp;val_cstrs|];
+ [|val_list val_id;val_cb|]|] o
+and val_module o = val_tuple "module_body"
+ [|val_opt val_seb;val_opt val_seb;val_cstrs;val_subst;no_val|] o
+and val_modtype o = val_tuple "module_type_body"
+ [|val_seb;val_opt val_mp;val_subst|] o
+
let rec subst_with_body sub = function
| With_module_body(id,mp,typ_opt,cst) ->
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 78bf2053..d71e625f 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -212,3 +212,8 @@ val join_alias : substitution -> substitution -> substitution
val update_subst_alias : substitution -> substitution -> substitution
val update_subst : substitution -> substitution -> substitution
val subst_key : substitution -> substitution -> substitution
+
+(* Validation *)
+val val_eng : Obj.t -> unit
+val val_module : Obj.t -> unit
+val val_modtype : Obj.t -> unit
diff --git a/checker/environ.ml b/checker/environ.ml
index 58f08bdd..4bdbeee6 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -201,6 +201,3 @@ let lookup_module mp env =
let lookup_modtype ln env =
MPmap.find ln env.env_globals.env_modtypes
-
-let lookup_alias mp env =
- MPmap.find mp env.env_globals.env_alias
diff --git a/checker/environ.mli b/checker/environ.mli
index a3f531dd..1541bf0d 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -1,6 +1,8 @@
open Names
open Term
+(* Environments *)
+
type globals = {
env_constants : Declarations.constant_body Cmap.t;
env_inductives : Declarations.mutual_inductive_body KNmap.t;
@@ -20,26 +22,33 @@ type env = {
env_imports : Digest.t MPmap.t;
}
val empty_env : env
+
+(* Engagement *)
val engagement : env -> Declarations.engagement option
-val universes : env -> Univ.universes
-val named_context : env -> named_context
-val rel_context : env -> rel_context
val set_engagement : Declarations.engagement -> env -> env
+(* Digests *)
val add_digest : env -> dir_path -> Digest.t -> env
val lookup_digest : env -> dir_path -> Digest.t
+(* de Bruijn variables *)
+val rel_context : env -> rel_context
val lookup_rel : int -> env -> rel_declaration
val push_rel : rel_declaration -> env -> env
val push_rel_context : rel_context -> env -> env
val push_rec_types : name array * constr array * 'a -> env -> env
+(* Named variables *)
+val named_context : env -> named_context
val push_named : named_declaration -> env -> env
val lookup_named : identifier -> env -> named_declaration
val named_type : identifier -> env -> constr
+(* Universes *)
+val universes : env -> Univ.universes
val add_constraints : Univ.constraints -> env -> env
+(* Constants *)
val lookup_constant : constant -> env -> Declarations.constant_body
val add_constant : constant -> Declarations.constant_body -> env -> env
val constant_type : env -> constant -> Declarations.constant_type
@@ -49,6 +58,7 @@ val constant_value : env -> constant -> constr
val constant_opt_value : env -> constant -> constr option
val evaluable_constant : constant -> env -> bool
+(* Inductives *)
val lookup_mind :
mutual_inductive -> env -> Declarations.mutual_inductive_body
val scrape_mind : env -> mutual_inductive -> mutual_inductive
@@ -56,6 +66,7 @@ val add_mind :
mutual_inductive -> Declarations.mutual_inductive_body -> env -> env
val mind_equiv : env -> inductive -> inductive -> bool
+(* Modules *)
val add_modtype :
module_path -> Declarations.module_type_body -> env -> env
val shallow_add_module :
@@ -64,4 +75,3 @@ val register_alias : module_path -> module_path -> env -> env
val scrape_alias : module_path -> env -> module_path
val lookup_module : module_path -> env -> Declarations.module_body
val lookup_modtype : module_path -> env -> Declarations.module_type_body
-val lookup_alias : module_path -> env -> module_path
diff --git a/checker/include b/checker/include
new file mode 100644
index 00000000..331eb45c
--- /dev/null
+++ b/checker/include
@@ -0,0 +1,176 @@
+(* -*-tuareg-*- *)
+
+(* Caml script to include for debugging the checker.
+ Usage: from the checker/ directory launch ocaml toplevel and then
+ type #use"include";;
+ This command loads the relevent modules, defines some pretty
+ printers, and provides functions to interactively check modules
+ (mainly run_l and norec).
+ *)
+
+#cd ".."
+#directory "lib";;
+#directory "kernel";;
+#directory "checker";;
+
+#load "unix.cma";;
+#load "str.cma";;
+#load "gramlib.cma";;
+#load "check.cma";;
+
+open Typeops;;
+open Check;;
+
+
+open Pp;;
+open Util;;
+open Names;;
+open Term;;
+open Environ;;
+open Declarations;;
+open Mod_checking;;
+
+let pr_id id = str(string_of_id id)
+let pr_na = function Name id -> pr_id id | _ -> str"_";;
+let prdp dp = pp(str(string_of_dirpath dp));;
+(*
+let prc c = pp(Himsg.pr_lconstr_env (Check.get_env()) c);;
+let prcs cs = prc (Declarations.force cs);;
+let pru u = pp(str(Univ.string_of_universe u));;*)
+let pru u = pp(Univ.pr_uni u);;
+let prlab l = pp(str(string_of_label l));;
+let prid id = pp(pr_id id);;
+let prcon c = pp(Indtypes.prcon c);;
+let prkn kn = pp(Indtypes.prkn kn);;
+
+
+let prus g = pp(Univ.pr_universes g);;
+
+let prcstrs c =
+ let g = Univ.merge_constraints c Univ.initial_universes in
+ pp(Univ.pr_universes g);;
+(*let prcstrs c = pp(Univ.pr_constraints c);; *)
+(*
+let prenvu e =
+ let u = universes e in
+ let pu =
+ str "UNIVERSES:"++fnl()++str" "++hov 0 (Univ.pr_universes u) ++fnl() in
+ pp pu;;
+
+let prenv e =
+ let ctx1 = named_context e in
+ let ctx2 = rel_context e in
+ let pe =
+ hov 1 (str"[" ++
+ prlist_with_sep spc (fun (na,_,_) -> pr_id na) (List.rev ctx1)++
+ str"]") ++ spc() ++
+ hov 1 (str"[" ++
+ prlist_with_sep spc (fun (na,_,_) -> pr_na na) (List.rev ctx2)++
+ str"]") in
+ pp pe;;
+*)
+
+let prsub s =
+ let string_of_mp mp =
+ let s = string_of_mp mp in
+ (match mp with MPself _ -> "#self."|MPbound _ -> "#bound."|_->"")^s in
+ pp (hv 0
+ (fold_subst
+ (fun msid mp strm ->
+ str "S " ++ str (debug_string_of_msid msid) ++ str " |-> " ++
+ str (string_of_mp mp) ++ fnl() ++ strm)
+ (fun mbid mp strm ->
+ str"B " ++ str (debug_string_of_mbid mbid) ++ str " |-> " ++
+ str (string_of_mp mp) ++ fnl() ++ strm)
+ (fun mp1 mp strm ->
+ str"P " ++ str (string_of_mp mp1) ++ str " |-> " ++
+ str (string_of_mp mp) ++ fnl() ++ strm) s (mt())))
+;;
+
+#install_printer prid;;
+#install_printer prcon;;
+#install_printer prlab;;
+#install_printer prdp;;
+#install_printer prkn;;
+#install_printer pru;;
+(*
+#install_printer prc;;
+#install_printer prcs;;
+*)
+#install_printer prcstrs;;
+(*#install_printer prus;;*)
+(*#install_printer prenv;;*)
+(*#install_printer prenvu;;*)
+#install_printer prsub;;
+
+Checker.init();;
+Flags.make_silent false;;
+Flags.debug := true;;
+Sys.catch_break true;;
+
+let module_of_file f =
+ let (_,mb,_,_) = Obj.magic ((intern_from_file f).library_compiled) in
+ (mb:module_body)
+;;
+let mod_access m fld =
+ match m.mod_expr with
+ Some(SEBstruct(msid,l)) -> List.assoc fld l
+ | _ -> failwith "bad structure type"
+;;
+
+let parse_dp s =
+ make_dirpath(List.map id_of_string (List.rev (Str.split(Str.regexp"\\.") s)))
+;;
+let parse_sp s =
+ let l = List.rev (Str.split(Str.regexp"\\.") s) in
+ {dirpath=List.tl l; basename=List.hd l};;
+let parse_kn s =
+ let l = List.rev (Str.split(Str.regexp"\\.") s) in
+ let dp = make_dirpath(List.map id_of_string(List.tl l)) in
+ make_kn(MPfile dp) empty_dirpath (label_of_id (id_of_string (List.hd l)))
+;;
+let parse_con s =
+ let l = List.rev (Str.split(Str.regexp"\\.") s) in
+ let dp = make_dirpath(List.map id_of_string(List.tl l)) in
+ make_con(MPfile dp) empty_dirpath (label_of_id (id_of_string (List.hd l)))
+;;
+let get_mod dp =
+ lookup_module dp (Safe_typing.get_env())
+;;
+let get_mod_type dp =
+ lookup_modtype dp (Safe_typing.get_env())
+;;
+let get_cst kn =
+ lookup_constant kn (Safe_typing.get_env())
+;;
+
+let read_mod s f =
+ let lib = intern_from_file (parse_dp s,f) in
+ ((Obj.magic lib.library_compiled):
+ dir_path *
+ module_body *
+ (dir_path * Digest.t) list *
+ engagement option);;
+
+let deref_mod md s =
+ let (Some (SEBstruct(msid,l))) = md.mod_expr in
+ List.assoc (label_of_id(id_of_string s)) l
+;;
+
+let expln f x =
+ try f x
+ with UserError(_,strm) as e ->
+ msgnl strm; raise e
+
+let admit_l l =
+ let l = List.map parse_sp l in
+ Check.recheck_library ~admit:l ~check:l;;
+let run_l l =
+ Check.recheck_library ~admit:[] ~check:(List.map parse_sp l);;
+let norec q =
+ Check.recheck_library ~norec:[parse_sp q] ~admit:[] ~check:[];;
+
+(*
+admit_l["Bool";"OrderedType";"DecidableType"];;
+run_l["FSetInterface"];;
+*)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index af5e4f46..9e7a2336 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -130,6 +130,12 @@ let check_definition_sub env cb1 cb2 =
Reduction.conv env c1 c2
| _ -> ())
+let lookup_modtype mp env =
+ try Environ.lookup_modtype mp env
+ with Not_found ->
+ failwith ("Unknown module type: "^string_of_mp mp)
+
+
let rec check_with env mtb with_decl =
match with_decl with
| With_definition_body _ ->
@@ -308,7 +314,8 @@ and check_structure_field (s,env) mp lab = function
and check_modexpr env mse = match mse with
| SEBident mp ->
- let mtb = lookup_modtype mp env in
+ let mp = scrape_alias mp env in
+ let mtb = lookup_modtype mp env in
mtb.typ_alias
| SEBfunctor (arg_id, mtb, body) ->
check_module_type env mtb;
diff --git a/checker/modops.ml b/checker/modops.ml
index 27ea4d55..498bd775 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -125,6 +125,7 @@ let strengthen_mind env mp l mib = match mib.mind_equiv with
let rec eval_struct env = function
| SEBident mp ->
begin
+ let mp = scrape_alias mp env in
let mtb =lookup_modtype mp env in
match mtb.typ_expr,mtb.typ_strength with
mtb,None -> eval_struct env mtb
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index d5779923..9e886837 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -106,6 +106,10 @@ type compiled_library =
(dir_path * Digest.t) list *
engagement option
+open Validate
+let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|])
+let val_vo = val_tuple "vo" [|val_dp;val_module;val_deps;val_eng|]
+
(* This function should append a certificate to the .vo file.
The digest must be part of the certicate to rule out attackers
that could change the .vo file between the time it was read and
@@ -116,7 +120,7 @@ let stamp_library file digest = ()
(* When the module is checked, digests do not need to match, but a
warning is issued in case of mismatch *)
let import file (dp,mb,depends,engmt as vo) digest =
- Validate.val_vo (Obj.repr vo);
+ Validate.apply !Flags.debug val_vo vo;
Flags.if_verbose msgnl (str "*** vo structure validated ***");
let env = !genv in
check_imports msg_warning dp env depends;
diff --git a/checker/term.ml b/checker/term.ml
index 45568a59..f245d155 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -15,6 +15,7 @@ open Pp
open Names
open Univ
open Esubst
+open Validate
(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
@@ -35,6 +36,10 @@ type case_info =
ci_cstr_nargs : int array; (* number of real args of each constructor *)
ci_pp_info : case_printing (* not interpreted by the kernel *)
}
+let val_ci =
+ let val_cstyle = val_enum "case_style" 5 in
+ let val_cprint = val_tuple "case_printing" [|val_int;val_cstyle|] in
+ val_tuple "case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
(* Sorts. *)
@@ -51,6 +56,9 @@ let family_of_sort = function
| Prop Pos -> InSet
| Type _ -> InType
+let val_sort = val_sum "sort" 0 [|[|val_enum "cnt" 2|];[|val_univ|]|]
+let val_sortfam = val_enum "sorts_family" 3
+
(********************************************************************)
(* Constructions as implemented *)
(********************************************************************)
@@ -65,7 +73,16 @@ type 'constr pfixpoint =
type 'constr pcofixpoint =
int * 'constr prec_declaration
+let val_evar f = val_tuple "pexistential" [|val_int;val_array f|]
+let val_prec f =
+ val_tuple "prec_declaration"[|val_array val_name; val_array f; val_array f|]
+let val_fix f =
+ val_tuple"pfixpoint"
+ [|val_tuple"fix2"[|val_array val_int;val_int|];val_prec f|]
+let val_cofix f = val_tuple"pcofixpoint"[|val_int;val_prec f|]
+
type cast_kind = VMcast | DEFAULTcast
+let val_cast = val_enum "cast_kind" 2
(*s*******************************************************************)
(* The type of constructions *)
@@ -88,11 +105,31 @@ type constr =
| Fix of constr pfixpoint
| CoFix of constr pcofixpoint
+let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [|
+ [|val_int|]; (* Rel *)
+ [|val_id|]; (* Var *)
+ [|val_int|]; (* Meta *)
+ [|val_evar val_constr|]; (* Evar *)
+ [|val_sort|]; (* Sort *)
+ [|val_constr;val_cast;val_constr|]; (* Cast *)
+ [|val_name;val_constr;val_constr|]; (* Prod *)
+ [|val_name;val_constr;val_constr|]; (* Lambda *)
+ [|val_name;val_constr;val_constr;val_constr|]; (* LetIn *)
+ [|val_constr;val_array val_constr|]; (* App *)
+ [|val_kn|]; (* Const *)
+ [|val_ind|]; (* Ind *)
+ [|val_cstr|]; (* Construct *)
+ [|val_ci;val_constr;val_constr;val_array val_constr|]; (* Case *)
+ [|val_fix val_constr|]; (* Fix *)
+ [|val_cofix val_constr|] (* CoFix *)
+|])
+
type existential = constr pexistential
type rec_declaration = constr prec_declaration
type fixpoint = constr pfixpoint
type cofixpoint = constr pcofixpoint
+
let rec strip_outer_cast c = match c with
| Cast (c,_,_) -> strip_outer_cast c
| _ -> c
@@ -275,6 +312,13 @@ let subst1 lam = substl [lam]
(* Type of assumptions and contexts *)
(***************************************************************************)
+let val_ndecl =
+ val_tuple"named_declaration"[|val_id;val_opt val_constr;val_constr|]
+let val_rdecl =
+ val_tuple"rel_declaration"[|val_name;val_opt val_constr;val_constr|]
+let val_nctxt = val_list val_ndecl
+let val_rctxt = val_list val_rdecl
+
type named_declaration = identifier * constr option * constr
type rel_declaration = name * constr option * constr
@@ -395,6 +439,7 @@ let decompose_prod_n_assum n =
(***************************)
type arity = rel_context * sorts
+let val_arity = val_tuple"arity"[|val_rctxt;val_constr|]
let mkArity (sign,s) = it_mkProd_or_LetIn (Sort s) sign
diff --git a/checker/term.mli b/checker/term.mli
index 30a2c03a..1367e581 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -109,3 +109,10 @@ val destArity : constr -> arity
val isArity : constr -> bool
val compare_constr : (constr -> constr -> bool) -> constr -> constr -> bool
val eq_constr : constr -> constr -> bool
+
+(* Validation *)
+val val_sortfam : Obj.t -> unit
+val val_sort : Obj.t -> unit
+val val_constr : Obj.t -> unit
+val val_rctxt : Obj.t -> unit
+val val_nctxt : Obj.t -> unit
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 1af8b2ce..1832ebec 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -140,7 +140,10 @@ let type_of_constant env cst =
let judge_of_constant_knowing_parameters env cst paramstyp =
let c = Const cst in
- let cb = lookup_constant cst env in
+ let cb =
+ try lookup_constant cst env
+ with Not_found ->
+ failwith ("Cannot find constant: "^string_of_con cst) in
let _ = check_args env c cb.const_hyps in
type_of_constant_knowing_parameters env cb.const_type paramstyp
@@ -222,7 +225,10 @@ let judge_of_cast env (c,cj) k tj =
let judge_of_inductive_knowing_parameters env ind (paramstyp:constr array) =
let c = Ind ind in
- let (mib,mip) = lookup_mind_specif env ind in
+ let (mib,mip) =
+ try lookup_mind_specif env ind
+ with Not_found ->
+ failwith ("Cannot find inductive: "^string_of_kn (fst ind)) in
check_args env c mib.mind_hyps;
type_of_inductive_knowing_parameters env mip paramstyp
@@ -235,7 +241,10 @@ let judge_of_constructor env c =
let constr = Construct c in
let _ =
let ((kn,_),_) = c in
- let mib = lookup_mind kn env in
+ let mib =
+ try lookup_mind kn env
+ with Not_found ->
+ failwith ("Cannot find inductive: "^string_of_kn (fst (fst c))) in
check_args env constr mib.mind_hyps in
let specif = lookup_mind_specif env (inductive_of_constructor c) in
type_of_constructor c specif
diff --git a/checker/validate.ml b/checker/validate.ml
index 86e51b7b..804bf7df 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -6,19 +6,19 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: term.ml 10098 2007-08-27 11:41:08Z herbelin $ *)
+(* $Id$ *)
(* This module defines validation functions to ensure an imported
value (using input_value) has the correct structure. *)
let rec pr_obj_rec o =
if Obj.is_int o then
- Format.print_string ("INT:"^string_of_int(Obj.magic o))
+ Format.print_int(Obj.magic o)
else if Obj.is_block o then
let t = Obj.tag o in
if t > Obj.no_scan_tag then
if t = Obj.string_tag then
- Format.print_string ("STR:"^Obj.magic o)
+ Format.print_string ("\""^String.escaped(Obj.magic o)^"\"")
else
Format.print_string "?"
else
@@ -36,7 +36,20 @@ let rec pr_obj_rec o =
let pr_obj o = pr_obj_rec o; Format.print_newline()
(**************************************************************************)
-(* Low-level validators *)
+(* Obj low-level validators *)
+
+exception ValidObjError of string * Obj.t
+let fail o s = raise (ValidObjError(s,o))
+
+let apply debug f x =
+ let o = Obj.repr x in
+ try f o
+ with ValidObjError(msg,obj) ->
+ if debug then begin
+ print_endline ("Validation failed: "^msg);
+ pr_obj obj
+ end;
+ failwith "validation failed"
(* data not validated *)
let no_val (o:Obj.t) = ()
@@ -44,26 +57,24 @@ let no_val (o:Obj.t) = ()
(* Check that object o is a block with tag t *)
let val_tag t o =
if Obj.is_block o && Obj.tag o = t then ()
- else failwith ("tag "^string_of_int t)
+ else fail o ("expected tag "^string_of_int t)
-let val_obj s o =
+let val_block s o =
if Obj.is_block o then
(if Obj.tag o > Obj.no_scan_tag then
- failwith (s^". Not a normal tag"))
- else failwith (s^". Not a block")
+ fail o (s^": found no scan tag"))
+ else fail o (s^": expected block obj")
(* Check that an object is a tuple (or a record). v is an array of
validation functions for each field. Its size corresponds to the
expected size of the object. *)
let val_tuple s v o =
let n = Array.length v in
- val_obj ("tuple: "^s) o;
+ val_block ("tuple: "^s) o;
if Obj.size o = n then
Array.iteri (fun i f -> f (Obj.field o i)) v
else
- (pr_obj o;
- failwith
- ("tuple:" ^s^" size found:"^string_of_int (Obj.size o)))
+ fail o ("tuple:" ^s^" size found:"^string_of_int (Obj.size o))
(* Check that the object is either a constant constructor of tag < cc,
or a constructed variant. each element of vv is an array of
@@ -73,15 +84,16 @@ let val_tuple s v o =
i-th non-constant constructor. *)
let val_sum s cc vv o =
if Obj.is_block o then
- (val_obj ("sum: "^s) o;
+ (val_block s o;
let n = Array.length vv in
let i = Obj.tag o in
- if i < n then val_tuple (s^"("^string_of_int i^")") vv.(i) o
- else failwith ("bad tag in sum ("^s^"): "^string_of_int i))
+ if i < n then val_tuple (s^"(tag "^string_of_int i^")") vv.(i) o
+ else fail o ("bad tag in (sum type) "^s^": max is "^string_of_int i))
else if Obj.is_int o then
let (n:int) = Obj.magic o in
- (if n<0 || n>=cc then failwith ("bad constant constructor ("^s^")"))
- else failwith ("not a sum ("^s^")")
+ (if n<0 || n>=cc then
+ fail o (s^": bad constant constructor "^string_of_int n))
+ else fail o ("not a sum ("^s^")")
let val_enum s n = val_sum s n [||]
@@ -89,177 +101,79 @@ let val_enum s n = val_sum s n [||]
let rec val_rec_sum s cc f o =
val_sum s cc (f (val_rec_sum s cc f)) o
+let rec val_rectype f o =
+ f (val_rectype f) o
+
(**************************************************************************)
(* Builtin types *)
(* Check the o is an array of values satisfying f. *)
-let val_array f o =
- val_obj "array" o;
+let val_array ?(name="array") f o =
+ val_block name o;
for i = 0 to Obj.size o - 1 do
(f (Obj.field o i):unit)
done
(* Integer validator *)
let val_int o =
- if not (Obj.is_int o) then failwith "expected an int"
+ if not (Obj.is_int o) then fail o "expected an int"
(* String validator *)
-let val_str s = val_tag Obj.string_tag s
+let val_str o =
+ try val_tag Obj.string_tag o
+ with Failure _ -> fail o "expected a string"
(* Booleans *)
let val_bool = val_enum "bool" 2
(* Option type *)
-let val_opt f = val_sum "option" 1 [|[|f|]|]
+let val_opt ?(name="option") f = val_sum name 1 [|[|f|]|]
(* Lists *)
-let val_list f =
- val_rec_sum "list" 1 (fun vlist -> [|[|f;vlist|]|])
+let val_list ?(name="list") f =
+ val_rec_sum name 1 (fun vlist -> [|[|f;vlist|]|])
(* Reference *)
-let val_ref f = val_tuple "ref" [|f|]
+let val_ref ?(name="ref") f = val_tuple name [|f|]
(**************************************************************************)
(* Standard library types *)
(* Sets *)
-let val_set f =
- val_rec_sum "set" 1 (fun vset -> [|[|vset;f;vset;val_int|]|])
+let val_set ?(name="Set.t") f =
+ val_rec_sum name 1 (fun vset -> [|[|vset;f;vset;val_int|]|])
(* Maps *)
-let rec val_map fk fv =
- val_rec_sum "map" 1 (fun vmap -> [|[|vmap;fk;fv;vmap;val_int|]|])
+let rec val_map ?(name="Map.t") fk fv =
+ val_rec_sum name 1 (fun vmap -> [|[|vmap;fk;fv;vmap;val_int|]|])
(**************************************************************************)
(* Coq types *)
+(* names *)
let val_id = val_str
-let val_dp = val_list val_id
+let val_dp = val_list ~name:"dirpath" val_id
let val_name = val_sum "name" 1 [|[|val_id|]|]
-let val_uid = val_tuple "uid" [|val_int;val_str;val_dp|]
+let val_uid = val_tuple "uniq_ident" [|val_int;val_str;val_dp|]
let val_mp =
- val_rec_sum "mp" 0
+ val_rec_sum "module_path" 0
(fun vmp -> [|[|val_dp|];[|val_uid|];[|val_uid|];[|vmp;val_id|]|])
-let val_kn = val_tuple "kn" [|val_mp;val_dp;val_id|]
-
-let val_ind = val_tuple "ind"[|val_kn;val_int|]
-let val_cstr = val_tuple "cstr"[|val_ind;val_int|]
-
-let val_ci =
- let val_cstyle = val_enum "case_style" 5 in
- let val_cprint = val_tuple "case_printing" [|val_int;val_cstyle|] in
- val_tuple "case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
+let val_kn = val_tuple "kernel_name" [|val_mp;val_dp;val_id|]
+let val_ind = val_tuple "inductive"[|val_kn;val_int|]
+let val_cstr = val_tuple "constructor"[|val_ind;val_int|]
+(* univ *)
let val_level = val_sum "level" 1 [|[|val_dp;val_int|]|]
let val_univ = val_sum "univ" 0
[|[|val_level|];[|val_list val_level;val_list val_level|]|]
let val_cstrs =
- val_set (val_tuple"univ_cstr"[|val_level;val_enum "order" 3;val_level|])
-
-let val_cast = val_enum "cast_kind" 2
-let val_sort = val_sum "sort" 0 [|[|val_enum "cnt" 2|];[|val_univ|]|]
-let val_sortfam = val_enum "sort_family" 3
-
-let val_evar f = val_tuple "evar" [|val_int;val_array f|]
-
-let val_prec f =
- val_tuple "prec"[|val_array val_name; val_array f; val_array f|]
-let val_fix f =
- val_tuple"fix1"[|val_tuple"fix2"[|val_array val_int;val_int|];val_prec f|]
-let val_cofix f = val_tuple"cofix"[|val_int;val_prec f|]
-
-
-let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [|
- [|val_int|]; (* Rel *)
- [|val_id|]; (* Var *)
- [|val_int|]; (* Meta *)
- [|val_evar val_constr|]; (* Evar *)
- [|val_sort|]; (* Sort *)
- [|val_constr;val_cast;val_constr|]; (* Cast *)
- [|val_name;val_constr;val_constr|]; (* Prod *)
- [|val_name;val_constr;val_constr|]; (* Lambda *)
- [|val_name;val_constr;val_constr;val_constr|]; (* LetIn *)
- [|val_constr;val_array val_constr|]; (* App *)
- [|val_kn|]; (* Const *)
- [|val_ind|]; (* Ind *)
- [|val_cstr|]; (* Construct *)
- [|val_ci;val_constr;val_constr;val_array val_constr|]; (* Case *)
- [|val_fix val_constr|]; (* Fix *)
- [|val_cofix val_constr|] (* CoFix *)
-|])
-
-
-let val_ndecl = val_tuple"ndecl"[|val_id;val_opt val_constr;val_constr|]
-let val_rdecl = val_tuple"rdecl"[|val_name;val_opt val_constr;val_constr|]
-let val_nctxt = val_list val_ndecl
-let val_rctxt = val_list val_rdecl
-
-let val_arity = val_tuple"arity"[|val_rctxt;val_constr|]
-
-let val_eng = val_enum "eng" 1
-
-let val_pol_arity = val_tuple"pol_arity"[|val_list(val_opt val_univ);val_univ|]
-let val_cst_type =
- val_sum "cst_type" 0 [|[|val_constr|];[|val_rctxt;val_pol_arity|]|]
-
-let val_subst_dom =
- val_sum "subst_dom" 0 [|[|val_uid|];[|val_uid|];[|val_mp|]|]
-
-
-let val_res = val_opt no_val
-
-let val_subst =
- val_map val_subst_dom (val_tuple "subst range" [|val_mp;val_res|])
-
-let val_cstr_subst =
- val_ref (val_sum "cstr_subst" 0 [|[|val_constr|];[|val_subst;val_constr|]|])
-
-let val_cb = val_tuple "cb"
- [|val_nctxt;val_opt val_cstr_subst; val_cst_type;no_val;val_cstrs;
- val_bool; val_bool |]
-
-let val_recarg = val_sum "recarg" 1 [|[|val_int|];[|val_ind|]|]
-
-let val_wfp = val_rec_sum "wf_paths" 0
- (fun val_wfp ->
- [|[|val_int;val_int|];[|val_recarg;val_array val_wfp|];
- [|val_int;val_array val_wfp|]|])
-
-let val_mono_ind_arity = val_tuple"mono_ind_arity"[|val_constr;val_sort|]
-let val_ind_arity = val_sum "ind_arity" 0
- [|[|val_mono_ind_arity|];[|val_pol_arity|]|]
-
-let val_one_ind = val_tuple "one_ind"
- [|val_id;val_rctxt;val_ind_arity;val_array val_id;val_array val_constr;
- val_int; val_list val_sortfam;val_array val_constr;val_array val_int;
- val_wfp; val_int; val_int; no_val|]
-
-let val_ind_pack = val_tuple "ind_pack"
- [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt;
- val_int; val_int; val_rctxt;val_cstrs;val_opt val_kn|]
-
-let rec val_sfb o = val_sum "sfb" 0
- [|[|val_cb|];[|val_ind_pack|];[|val_mod|];
- [|val_mp;val_opt val_cstrs|];[|val_modty|]|] o
-and val_sb o = val_list (val_tuple"sb"[|val_id;val_sfb|]) o
-and val_seb o = val_sum "seb" 0
- [|[|val_mp|];[|val_uid;val_modty;val_seb|];[|val_uid;val_sb|];
- [|val_seb;val_seb;val_cstrs|];[|val_seb;val_with|]|] o
-and val_with o = val_sum "with" 0
- [|[|val_list val_id;val_mp;val_cstrs|];
- [|val_list val_id;val_cb|]|] o
-and val_mod o = val_tuple "module_body"
- [|val_opt val_seb;val_opt val_seb;val_cstrs;val_subst;no_val|] o
-and val_modty o = val_tuple "module_type_body"
- [|val_seb;val_opt val_mp;val_subst|] o
-
-let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|])
-
-let val_vo = val_tuple "vo" [|val_dp;val_mod;val_deps;val_eng|]
+ val_set ~name:"Univ.constraints"
+ (val_tuple "univ_constraint"
+ [|val_level;val_enum "order_request" 3;val_level|])
diff --git a/config/Makefile.template b/config/Makefile.template
index 35e2a2d7..6f9fac3c 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -23,6 +23,7 @@ LOCAL=LOCALINSTALLATION
# Bytecode link flags for VM ("-custom" or "-dllib -lcoqrun")
COQRUNBYTEFLAGS=XCOQRUNBYTEFLAGS
+COQTOOLSBYTEFLAGS=XCOQTOOLSBYTEFLAGS
BUILDLDPATH=
# Paths for true installation
diff --git a/configure b/configure
index 14ff9950..c8508f52 100755
--- a/configure
+++ b/configure
@@ -6,9 +6,9 @@
#
##################################
-VERSION=8.2rc2
-VOMAGIC=08193
-STATEMAGIC=19764
+VERSION=8.2
+VOMAGIC=08200
+STATEMAGIC=58200
DATE=`LANG=C date +"%B %Y"`
# Create the bin/ directory if non-existent
@@ -36,7 +36,11 @@ usage () {
echo "-local"
printf "\tSet installation directory to the current source tree\n"
echo "-coqrunbyteflags"
- printf "\tSet link flags for VM-dependent bytecode\n"
+ printf "\tSet link flags for VM-dependent bytecode (coqtop)\n"
+ echo "-coqtoolsbyteflags"
+ printf "\tSet link flags for VM-independant bytecode (coqdep, coqdoc, ...)\n"
+ echo "-custom"
+ printf "\tGenerate all bytecode executables with -custom (not recommended)\n"
echo "-src"
printf "\tSpecifies the source directory\n"
echo "-bindir"
@@ -111,6 +115,8 @@ ranlib_exec=ranlib
local=false
coqrunbyteflags_spec=no
+coqtoolsbyteflags_spec=no
+custom_spec=no
src_spec=no
prefix_spec=no
bindir_spec=no
@@ -147,6 +153,11 @@ while : ; do
-coqrunbyteflags|--coqrunbyteflags) coqrunbyteflags_spec=yes
coqrunbyteflags="$2"
shift;;
+ -coqtoolsbyteflags|--coqtoolsbyteflags) coqtoolsbyteflags_spec=yes
+ coqtoolsbyteflags="$2"
+ shift;;
+ -custom|--custom) custom_spec=yes
+ shift;;
-src|--src) src_spec=yes
COQSRC="$2"
shift;;
@@ -388,7 +399,7 @@ fi
# Under Windows, OCaml only understands Windows filenames (C:\...)
case $ARCH in
- win32) CAMLBIN=`cygpath -w ${CAMLBIN}`;;
+ win32) CAMLBIN=`cygpath -m ${CAMLBIN}`;;
esac
# this fixes a camlp4 bug under FreeBSD
@@ -668,7 +679,7 @@ esac
# OCaml only understand Windows filenames (C:\...)
case $ARCH in
- win32) COQTOP=`cygpath -w ${COQTOP}`
+ win32) COQTOP=`cygpath -m ${COQTOP}`
esac
case $ARCH in
@@ -774,12 +785,25 @@ case $coqdocdir_spec/$prefix_spec/$local in
esac;;
esac
+# Determine if we enable -custom by default (Windows and MacOS)
+CUSTOM_OS=no
+if [ "$ARCH" = "win32" ] || [ "`uname -s`" = "Darwin" ]; then
+ CUSTOM_OS=yes
+fi
+
BUILDLDPATH="# you might want to set CAML_LD_LIBRARY_PATH by hand!"
-case $coqrunbyteflags_spec/$local in
- yes/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
- */true) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $COQTOP/kernel/byterun";;
- *) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath $LIBDIR"
- BUILDLDPATH="export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun";;
+case $coqrunbyteflags_spec/$local/$custom_spec/$CUSTOM_OS in
+ yes/*/*/*) COQRUNBYTEFLAGS="$coqrunbyteflags";;
+ */*/yes/*|*/*/*/yes) COQRUNBYTEFLAGS="-custom";;
+ */true/*/*) COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$COQTOP'/kernel/byterun";;
+ *)
+ COQRUNBYTEFLAGS="-dllib -lcoqrun -dllpath '$LIBDIR'"
+ BUILDLDPATH="export CAML_LD_LIBRARY_PATH='$COQTOP'/kernel/byterun";;
+esac
+case $coqtoolsbyteflags_spec/$custom_spec/$CUSTOM_OS in
+ yes/*/*) COQTOOLSBYTEFLAGS="$coqtoolsbyteflags";;
+ */yes/*|*/*/yes) COQTOOLSBYTEFLAGS="-custom";;
+ *) COQTOOLSBYTEFLAGS="";;
esac
# case $emacs_spec in
@@ -803,6 +827,7 @@ if test ! -z "$OS" ; then
echo " Operating system : $OS"
fi
echo " Coq VM bytecode link flags : $COQRUNBYTEFLAGS"
+echo " Coq tools bytecode link flags : $COQTOOLSBYTEFLAGS"
echo " OS dependent libraries : $OSDEPLIBS"
echo " Objective-Caml/Camlp4 version : $CAMLVERSION"
echo " Objective-Caml/Camlp4 binaries in : $CAMLBIN"
@@ -858,7 +883,7 @@ case $ARCH in
win32)
ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
- ESCSRCDIR=`cygpath -d $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
+ ESCSRCDIR=`cygpath -m $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
ESCCAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
@@ -870,6 +895,7 @@ case $ARCH in
ESCCAMLP4LIB=`echo $CAMLP4LIB |sed -e 's|\\\|\\\\\\\|g'`
ESCLABLGTKINCLUDES=`echo $LABLGTKINCLUDES |sed -e 's|\\\|\\\\\\\|g'`
ESCCOQRUNBYTEFLAGS=`echo $COQRUNBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
+ ESCCOQTOOLSBYTEFLAGS=`echo $COQTOOLSBYTEFLAGS |sed -e 's|\\\|\\\\\\\|g'`
ESCBUILDLDPATH=`echo $BUILDLDPATH |sed -e 's|\\\|\\\\\\\|g'`
;;
*)
@@ -887,6 +913,7 @@ case $ARCH in
ESCCAMLP4LIB="$CAMLP4LIB"
ESCLABLGTKINCLUDES="$LABLGTKINCLUDES"
ESCCOQRUNBYTEFLAGS="$COQRUNBYTEFLAGS"
+ ESCCOQTOOLSBYTEFLAGS="$COQTOOLSBYTEFLAGS"
;;
esac
@@ -947,6 +974,7 @@ rm -f "$COQSRC/config/Makefile"
sed -e "s|LOCALINSTALLATION|$local|" \
-e "s|XCOQRUNBYTEFLAGS|$ESCCOQRUNBYTEFLAGS|" \
+ -e "s|XCOQTOOLSBYTEFLAGS|$ESCCOQTOOLSBYTEFLAGS|" \
-e "s|COQSRCDIRECTORY|$COQSRC|" \
-e "s|COQVERSION|$VERSION|" \
-e "s|BINDIRDIRECTORY|$ESCBINDIR|" \
@@ -1040,4 +1068,4 @@ echo
echo "*Warning* To compile the system for a new architecture"
echo " don't forget to do a 'make archclean' before './configure'."
-# $Id: configure 11858 2009-01-26 13:27:23Z notin $
+# $Id: configure 11934 2009-02-17 15:58:54Z notin $
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index fa006c1c..2cf457c6 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extraction.ml 11459 2008-10-16 16:29:07Z letouzey $ i*)
+(*i $Id: extraction.ml 11897 2009-02-09 19:28:02Z barras $ i*)
(*i*)
open Util
@@ -177,7 +177,7 @@ let parse_ind_args si args relmax =
let rec extract_type env db j c args =
- match kind_of_term (whd_betaiotazeta c) with
+ match kind_of_term (whd_betaiotazeta Evd.empty c) with
| App (d, args') ->
(* We just accumulate the arguments. *)
extract_type env db j d (Array.to_list args' @ args)
@@ -285,7 +285,7 @@ and extract_type_app env db (r,s) args =
and extract_type_scheme env db c p =
if p=0 then extract_type env db 0 c []
else
- let c = whd_betaiotazeta c in
+ let c = whd_betaiotazeta Evd.empty c in
match kind_of_term c with
| Lambda (n,t,d) ->
extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
diff --git a/contrib/firstorder/unify.ml b/contrib/firstorder/unify.ml
index 1dd13cbe..27c06f54 100644
--- a/contrib/firstorder/unify.ml
+++ b/contrib/firstorder/unify.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: unify.ml 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: unify.ml 11897 2009-02-09 19:28:02Z barras $ i*)
open Util
open Formula
@@ -42,8 +42,8 @@ let unif t1 t2=
Queue.add (t1,t2) bige;
try while true do
let t1,t2=Queue.take bige in
- let nt1=head_reduce (whd_betaiotazeta t1)
- and nt2=head_reduce (whd_betaiotazeta t2) in
+ let nt1=head_reduce (whd_betaiotazeta Evd.empty t1)
+ and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in
match (kind_of_term nt1),(kind_of_term nt2) with
Meta i,Meta j->
if i<>j then
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 9f3e412a..b13bea9d 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -252,7 +252,8 @@ let change_eq env sigma hyp_id (context:Sign.rel_context) x t end_of_type =
(new_end_of_type,0,witness_fun)
context
in
- let new_type_of_hyp = Reductionops.nf_betaiota new_type_of_hyp in
+ let new_type_of_hyp =
+ Reductionops.nf_betaiota Evd.empty new_type_of_hyp in
let new_ctxt,new_end_of_type =
Sign.decompose_prod_n_assum ctxt_size new_type_of_hyp
in
@@ -708,7 +709,8 @@ let build_proof
| Const _ ->
do_finalize dyn_infos g
| Lambda _ ->
- let new_term = Reductionops.nf_beta dyn_infos.info in
+ let new_term =
+ Reductionops.nf_beta Evd.empty dyn_infos.info in
build_proof do_finalize {dyn_infos with info = new_term}
g
| LetIn _ ->
@@ -1056,7 +1058,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
let bodies_with_all_params =
Array.map
(fun body ->
- Reductionops.nf_betaiota
+ Reductionops.nf_betaiota Evd.empty
(applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
List.rev_map var_of_decl princ_params))
)
@@ -1093,12 +1095,12 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
let body_with_param,num =
let body = get_body fnames.(i) in
let body_with_full_params =
- Reductionops.nf_betaiota (
+ Reductionops.nf_betaiota Evd.empty (
applist(body,List.rev_map var_of_decl full_params))
in
match kind_of_term body_with_full_params with
| Fix((_,num),(_,_,bs)) ->
- Reductionops.nf_betaiota
+ Reductionops.nf_betaiota Evd.empty
(
(applist
(substl
@@ -1174,7 +1176,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
nb_rec_hyps = -100;
rec_hyps = [];
info =
- Reductionops.nf_betaiota
+ Reductionops.nf_betaiota Evd.empty
(applist(fix_body,List.rev_map mkVar args_id));
eq_hyps = []
}
@@ -1236,7 +1238,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
nb_rec_hyps = -100;
rec_hyps = [];
info =
- Reductionops.nf_betaiota
+ Reductionops.nf_betaiota Evd.empty
(applist(fbody_with_full_params,
(List.rev_map var_of_decl princ_params)@
(List.rev_map mkVar args_id)
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index cf861642..2ab62763 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1361,7 +1361,7 @@ and natural_cutintro ig lh g gs arg ltree =
{ihsg=No_subgoals_hyp;isgintro=""}
(List.nth ltree 0))]
]
-and whd_betadeltaiota x = whd_betaiotaevar (Global.env()) Evd.empty x
+and whd_betadeltaiota x = whd_betaiota Evd.empty x
and type_of_ast s c = type_of (Global.env()) Evd.empty (constr_of_ast c)
and prod_head t =
match (kind_of_term (strip_outer_cast t)) with
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 094226ff..1d213db9 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -7,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_cases.ml 11576 2008-11-10 19:13:15Z msozeau $ *)
+(* $Id: subtac_cases.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Cases
open Util
@@ -822,7 +822,7 @@ let infer_predicate loc env isevars typs cstrs indf =
(* Empiric normalization: p may depend in a irrelevant way on args of the*)
(* cstr as in [c:{_:Alpha & Beta}] match c with (existS a b)=>(a,b) end *)
let typs =
- Array.map (local_strong (whd_betaevar empty_env (Evd.evars_of !isevars))) typs
+ Array.map (local_strong whd_beta (Evd.evars_of !isevars)) typs
in
let eqns = array_map2 prepare_unif_pb typs cstrs in
(* First strategy: no dependencies at all *)
@@ -1042,9 +1042,10 @@ let find_predicate loc env isevars p typs cstrs current
match p with
| Some p -> abstract_predicate env (Evd.evars_of !isevars) indf current tms p
| None -> infer_predicate loc env isevars typs cstrs indf in
- let typ = whd_beta (applist (pred, realargs)) in
+ let typ = whd_beta (Evd.evars_of !isevars) (applist (pred, realargs)) in
if dep then
- (pred, whd_beta (applist (typ, [current])), new_Type ())
+ (pred, whd_beta (Evd.evars_of !isevars) (applist (typ, [current])),
+ new_Type ())
else
(pred, typ, new_Type ())
@@ -1246,7 +1247,7 @@ and match_current pb tomatch =
find_predicate pb.caseloc pb.env pb.isevars
pb.pred brtyps cstrs current indt pb.tomatch in
let ci = make_case_info pb.env mind pb.casestyle in
- let case = mkCase (ci,nf_betaiota pred,current,brvals) in
+ let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in
let inst = List.map mkRel deps in
{ uj_val = applist (case, inst);
uj_type = substl inst typ }
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index cc1e2dde..d2e831ef 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -282,7 +282,7 @@ let declare_obligation obl body =
print_message (Subtac_utils.definition_message obl.obl_name);
{ obl with obl_body = Some (mkConst constant) }
-let red = Reductionops.nf_betaiota
+let red = Reductionops.nf_betaiota Evd.empty
let init_prog_info n b t deps fixkind notations obls impls kind hook =
let obls' =
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index c62db00b..13e5e6d5 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -245,9 +245,9 @@ let typeur sigma metamap =
let Inductiveops.IndType(_,realargs) =
try Inductiveops.find_rectype env sigma (type_of env c)
with Not_found -> Util.anomaly "type_of: Bad recursive type" in
- let t = Reductionops.whd_beta (T.applist (p, realargs)) in
+ let t = Reductionops.whd_beta sigma (T.applist (p, realargs)) in
(match Term.kind_of_term (DoubleTypeInference.whd_betadeltaiotacprop env sigma (type_of env t)) with
- | T.Prod _ -> Reductionops.whd_beta (T.applist (t, [c]))
+ | T.Prod _ -> Reductionops.whd_beta sigma (T.applist (t, [c]))
| _ -> t)
| T.Lambda (name,c1,c2) ->
T.mkProd (name, c1, type_of (Environ.push_rel (name,None,c1) env) c2)
@@ -390,7 +390,7 @@ Pp.ppnl (Pp.(++) (Pp.str "BUG: this subterm was not visited during the double-ty
(* We need to refresh the universes because we are doing *)
(* type inference on an already inferred type. *)
{D.synthesized =
- Reductionops.nf_beta
+ Reductionops.nf_beta evar_map
(CPropRetyping.get_type_of env evar_map
(Termops.refresh_universes tt)) ;
D.expected = None}
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index de8c540c..17d1d5da 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -163,7 +163,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
| hj::restjl ->
match T.kind_of_term (Reduction.whd_betadeltaiota env typ) with
T.Prod (_,c1,c2) ->
- (Some (Reductionops.nf_beta c1)) ::
+ (Some (Reductionops.nf_beta sigma c1)) ::
(aux (T.subst1 hj c2) restjl)
| _ -> assert false
in
@@ -183,7 +183,7 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
| Some ety ->
match T.kind_of_term (Reduction.whd_betadeltaiota env ety) with
T.Prod (_,_,expected_target_type) ->
- Some (Reductionops.nf_beta expected_target_type)
+ Some (Reductionops.nf_beta sigma expected_target_type)
| _ -> assert false
in
let j' = execute env1 sigma c2 expectedc2type in
@@ -214,14 +214,14 @@ let double_type_of env sigma cstr expectedty subterms_to_types =
Typeops.judge_of_letin env name j1 j2 j3
| T.Cast (c,k,t) ->
- let cj = execute env sigma c (Some (Reductionops.nf_beta t)) in
+ let cj = execute env sigma c (Some (Reductionops.nf_beta sigma t)) in
let tj = execute env sigma t None in
let tj = type_judgment env sigma tj in
let j, _ = Typeops.judge_of_cast env cj k tj in
j
in
let synthesized = E.j_type judgement in
- let synthesized' = Reductionops.nf_beta synthesized in
+ let synthesized' = Reductionops.nf_beta sigma synthesized in
let types,res =
match expectedty with
None ->
diff --git a/dev/base_include b/dev/base_include
index 0b7a0b67..d4366843 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -128,7 +128,6 @@ open Hipattern
open Inv
open Leminv
open Refine
-open Setoid_replace
open Tacinterp
open Tacticals
open Tactics
diff --git a/ide/coq.ico b/ide/coq.ico
new file mode 100644
index 00000000..94ce897d
--- /dev/null
+++ b/ide/coq.ico
Binary files differ
diff --git a/install.sh b/install.sh
index 0719ca77..277222f5 100755
--- a/install.sh
+++ b/install.sh
@@ -1,13 +1,13 @@
#! /bin/sh
-dest=$1
+dest="$1"
shift
for f; do
bn=`basename $f`
dn=`dirname $f`
- install -d $dest/$dn
- install -m 644 $f $dest/$dn/$bn
+ install -d "$dest/$dn"
+ install -m 644 $f "$dest/$dn/$bn"
done
diff --git a/interp/notation.ml b/interp/notation.ml
index fcb2b6f5..776fff79 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: notation.ml 11512 2008-10-27 12:28:36Z herbelin $ *)
+(* $Id: notation.ml 11897 2009-02-09 19:28:02Z barras $ *)
(*i*)
open Util
@@ -422,7 +422,7 @@ let find_class_scope cl =
Gmap.find cl !class_scope_map
let find_class t =
- let t, _ = decompose_app (Reductionops.whd_betaiotazeta t) in
+ let t, _ = decompose_app (Reductionops.whd_betaiotazeta Evd.empty t) in
match kind_of_term t with
| Var id -> CL_SECVAR id
| Const sp -> CL_CONST sp
@@ -435,7 +435,7 @@ let find_class t =
(* Special scopes associated to arguments of a global reference *)
let rec compute_arguments_scope t =
- match kind_of_term (Reductionops.whd_betaiotazeta t) with
+ match kind_of_term (Reductionops.whd_betaiotazeta Evd.empty t) with
| Prod (_,t,u) ->
let sc =
try Some (find_class_scope (find_class t)) with Not_found -> None in
diff --git a/kernel/closure.ml b/kernel/closure.ml
index b85be204..a184c128 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: closure.ml 10819 2008-04-20 18:14:44Z msozeau $ *)
+(* $Id: closure.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Util
open Pp
@@ -28,7 +28,8 @@ let iota = ref 0
let prune = ref 0
let reset () =
- beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; prune := 0
+ beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; evar := 0;
+ prune := 0
let stop() =
msgnl (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++
@@ -83,7 +84,6 @@ module RedFlags = (struct
r_delta : bool;
r_const : transparent_state;
r_zeta : bool;
- r_evar : bool;
r_iota : bool }
type red_kind = BETA | DELTA | IOTA | ZETA
@@ -99,7 +99,6 @@ module RedFlags = (struct
r_delta = false;
r_const = all_opaque;
r_zeta = false;
- r_evar = false;
r_iota = false }
let red_add red = function
@@ -201,6 +200,7 @@ type 'a infos = {
i_flags : reds;
i_repr : 'a infos -> constr -> 'a;
i_env : env;
+ i_sigma : existential -> constr option;
i_rels : int * (int * constr) list;
i_vars : (identifier * constr) list;
i_tab : (table_key, 'a) Hashtbl.t }
@@ -227,6 +227,9 @@ let ref_value_cache info ref =
| NotEvaluableConst _ (* Const *)
-> None
+let evar_value info ev =
+ info.i_sigma ev
+
let defined_vars flags env =
(* if red_local_const (snd flags) then*)
Sign.fold_named_context
@@ -259,10 +262,11 @@ let rec mind_equiv env (kn1,i1) (kn2,i2) =
let mind_equiv_infos info = mind_equiv info.i_env
-let create mk_cl flgs env =
+let create mk_cl flgs env evars =
{ i_flags = flgs;
i_repr = mk_cl;
i_env = env;
+ i_sigma = evars;
i_rels = defined_rels flgs env;
i_vars = defined_vars flgs env;
i_tab = Hashtbl.create 17 }
@@ -314,7 +318,7 @@ and fterm =
| FLambda of int * (name * constr) list * constr * fconstr subs
| FProd of name * fconstr * fconstr
| FLetIn of name * fconstr * fconstr * constr * fconstr subs
- | FEvar of existential_key * fconstr array
+ | FEvar of existential * fconstr subs
| FLIFT of int * fconstr
| FCLOS of constr * fconstr subs
| FLOCKED
@@ -581,8 +585,8 @@ let mk_clos_deep clos_fun env t =
| LetIn (n,b,t,c) ->
{ norm = Red;
term = FLetIn (n, clos_fun env b, clos_fun env t, c, env) }
- | Evar(ev,args) ->
- { norm = Whnf; term = FEvar(ev,Array.map (clos_fun env) args) }
+ | Evar ev ->
+ { norm = Red; term = FEvar(ev,env) }
(* A better mk_clos? *)
let mk_clos2 = mk_clos_deep mk_clos
@@ -632,7 +636,8 @@ let rec to_constr constr_fun lfts v =
mkLetIn (n, constr_fun lfts b,
constr_fun lfts t,
constr_fun (el_lift lfts) fc)
- | FEvar (ev,args) -> mkEvar(ev,Array.map (constr_fun lfts) args)
+ | FEvar ((ev,args),env) ->
+ mkEvar(ev,Array.map (fun a -> constr_fun lfts (mk_clos2 env a)) args)
| FLIFT (k,a) -> to_constr constr_fun (el_shft k lfts) a
| FCLOS (t,env) ->
let fr = mk_clos2 env t in
@@ -891,6 +896,10 @@ let rec knr info m stk =
| (_,args,s) -> (m,args@s))
| FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
knit info (subs_cons([|v|],e)) bd stk
+ | FEvar(ev,env) ->
+ (match evar_value info ev with
+ Some c -> knit info env c stk
+ | None -> (m,stk))
| _ -> (m,stk)
(* Computes the weak head normal form of a term *)
@@ -959,7 +968,8 @@ and norm_head info m =
let fbds =
Array.map (mk_clos (subs_liftn (Array.length na) e)) bds in
mkFix(n,(na, Array.map (kl info) ftys, Array.map (kl info) fbds))
- | FEvar(i,args) -> mkEvar(i, Array.map (kl info) args)
+ | FEvar((i,args),env) ->
+ mkEvar(i, Array.map (fun a -> kl info (mk_clos env a)) args)
| t -> term_of_fconstr m
(* Initialization and then normalization *)
@@ -982,7 +992,7 @@ let whd_stack infos m stk =
(* cache of constants: the body is computed only when needed. *)
type clos_infos = fconstr infos
-let create_clos_infos flgs env =
- create (fun _ -> inject) flgs env
+let create_clos_infos ?(evars=fun _ -> None) flgs env =
+ create (fun _ -> inject) flgs env evars
let unfold_reference = ref_value_cache
diff --git a/kernel/closure.mli b/kernel/closure.mli
index c814baad..a80f7a62 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: closure.mli 10652 2008-03-10 21:52:06Z herbelin $ i*)
+(*i $Id: closure.mli 11897 2009-02-09 19:28:02Z barras $ i*)
(*i*)
open Pp
@@ -85,7 +85,9 @@ type table_key = id_key
type 'a infos
val ref_value_cache: 'a infos -> table_key -> 'a option
val info_flags: 'a infos -> reds
-val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos
+val create: ('a infos -> constr -> 'a) -> reds -> env ->
+ (existential -> constr option) -> 'a infos
+val evar_value : 'a infos -> existential -> constr option
(************************************************************************)
(*s Lazy reduction. *)
@@ -111,7 +113,7 @@ type fterm =
| FLambda of int * (name * constr) list * constr * fconstr subs
| FProd of name * fconstr * fconstr
| FLetIn of name * fconstr * fconstr * constr * fconstr subs
- | FEvar of existential_key * fconstr array
+ | FEvar of existential * fconstr subs
| FLIFT of int * fconstr
| FCLOS of constr * fconstr subs
| FLOCKED
@@ -156,7 +158,8 @@ val destFLambda :
(* Global and local constant cache *)
type clos_infos
-val create_clos_infos : reds -> env -> clos_infos
+val create_clos_infos :
+ ?evars:(existential->constr option) -> reds -> env -> clos_infos
(* Reduction function *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 43ef3a98..76b32463 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: reduction.ml 10930 2008-05-15 10:50:32Z barras $ *)
+(* $Id: reduction.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Util
open Names
@@ -248,10 +248,12 @@ and eqappr cv_pb infos (lft1,st1) (lft2,st2) cuniv =
then convert_stacks infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
| _ -> raise NotConvertible)
- | (FEvar (ev1,args1), FEvar (ev2,args2)) ->
+ | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) ->
if ev1=ev2 then
let u1 = convert_stacks infos lft1 lft2 v1 v2 cuniv in
- convert_vect infos el1 el2 args1 args2 u1
+ convert_vect infos el1 el2
+ (Array.map (mk_clos env1) args1)
+ (Array.map (mk_clos env2) args2) u1
else raise NotConvertible
(* 2 index known to be bound to no constant *)
@@ -382,29 +384,29 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv =
fold 0 cuniv
else raise NotConvertible
-let clos_fconv trans cv_pb env t1 t2 =
- let infos = trans, create_clos_infos betaiotazeta env in
+let clos_fconv trans cv_pb evars env t1 t2 =
+ let infos = trans, create_clos_infos ~evars betaiotazeta env in
ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty
-let trans_fconv reds cv_pb env t1 t2 =
+let trans_fconv reds cv_pb evars env t1 t2 =
if eq_constr t1 t2 then Constraint.empty
- else clos_fconv reds cv_pb env t1 t2
+ else clos_fconv reds cv_pb evars env t1 t2
-let trans_conv_cmp conv reds = trans_fconv reds conv
-let trans_conv reds = trans_fconv reds CONV
-let trans_conv_leq reds = trans_fconv reds CUMUL
+let trans_conv_cmp conv reds = trans_fconv reds conv (fun _->None)
+let trans_conv ?(evars=fun _->None) reds = trans_fconv reds CONV evars
+let trans_conv_leq ?(evars=fun _->None) reds = trans_fconv reds CUMUL evars
let fconv = trans_fconv (Idpred.full, Cpred.full)
-let conv_cmp = fconv
-let conv = fconv CONV
-let conv_leq = fconv CUMUL
+let conv_cmp cv_pb = fconv cv_pb (fun _->None)
+let conv ?(evars=fun _->None) = fconv CONV evars
+let conv_leq ?(evars=fun _->None) = fconv CUMUL evars
-let conv_leq_vecti env v1 v2 =
+let conv_leq_vecti ?(evars=fun _->None) env v1 v2 =
array_fold_left2_i
(fun i c t1 t2 ->
let c' =
- try conv_leq env t1 t2
+ try conv_leq ~evars env t1 t2
with NotConvertible -> raise (NotConvertibleVect i) in
Constraint.union c c')
Constraint.empty
@@ -413,17 +415,17 @@ let conv_leq_vecti env v1 v2 =
(* option for conversion *)
-let vm_conv = ref fconv
+let vm_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None))
let set_vm_conv f = vm_conv := f
let vm_conv cv_pb env t1 t2 =
try
!vm_conv cv_pb env t1 t2
with Not_found | Invalid_argument _ ->
(* If compilation fails, fall-back to closure conversion *)
- fconv cv_pb env t1 t2
+ fconv cv_pb (fun _->None) env t1 t2
-let default_conv = ref fconv
+let default_conv = ref (fun cv_pb -> fconv cv_pb (fun _->None))
let set_default_conv f = default_conv := f
@@ -432,7 +434,7 @@ let default_conv cv_pb env t1 t2 =
!default_conv cv_pb env t1 t2
with Not_found | Invalid_argument _ ->
(* If compilation fails, fall-back to closure conversion *)
- fconv cv_pb env t1 t2
+ fconv cv_pb (fun _->None) env t1 t2
let default_conv_leq = default_conv CUMUL
(*
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 3b9eb315..d8658d43 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: reduction.mli 10840 2008-04-23 21:29:34Z herbelin $ i*)
+(*i $Id: reduction.mli 11897 2009-02-09 19:28:02Z barras $ i*)
(*i*)
open Term
@@ -40,15 +40,18 @@ val conv_sort : sorts conversion_function
val conv_sort_leq : sorts conversion_function
val trans_conv_cmp : conv_pb -> constr trans_conversion_function
-
-val trans_conv : constr trans_conversion_function
-val trans_conv_leq : types trans_conversion_function
+val trans_conv :
+ ?evars:(existential->constr option) -> constr trans_conversion_function
+val trans_conv_leq :
+ ?evars:(existential->constr option) -> types trans_conversion_function
val conv_cmp : conv_pb -> constr conversion_function
-
-val conv : constr conversion_function
-val conv_leq : types conversion_function
-val conv_leq_vecti : types array conversion_function
+val conv :
+ ?evars:(existential->constr option) -> constr conversion_function
+val conv_leq :
+ ?evars:(existential->constr option) -> types conversion_function
+val conv_leq_vecti :
+ ?evars:(existential->constr option) -> types array conversion_function
(* option for conversion *)
val set_vm_conv : (conv_pb -> types conversion_function) -> unit
diff --git a/lib/envars.ml b/lib/envars.ml
index 5887adcd..d700ffe1 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -21,8 +21,9 @@ let guess_coqlib () =
else
let coqbin = System.canonical_path_name (Filename.dirname Sys.executable_name) in
let prefix = Filename.dirname coqbin in
- let coqlib = if Coq_config.local then prefix else
- List.fold_left Filename.concat prefix ["lib";"coq"] in
+ let rpath = if Coq_config.local then [] else
+ (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
+ let coqlib = List.fold_left Filename.concat prefix rpath in
if Sys.file_exists (Filename.concat coqlib file) then coqlib else
Util.error "cannot guess a path for Coq libraries; please use -coqlib option"
diff --git a/lib/util.ml b/lib/util.ml
index a73a5558..a8a99c0b 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(* $Id: util.ml 11845 2009-01-22 18:55:08Z letouzey $ *)
+(* $Id: util.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
@@ -1354,6 +1354,39 @@ let pr_located pr (loc,x) =
let surround p = hov 1 (str"(" ++ p ++ str")")
+(*s Memoization *)
+
+let memo1_eq eq f =
+ let m = ref None in
+ fun x ->
+ match !m with
+ Some(x',y') when eq x x' -> y'
+ | _ -> let y = f x in m := Some(x,y); y
+
+let memo1_1 f = memo1_eq (==) f
+let memo1_2 f =
+ let f' =
+ memo1_eq (fun (x,y) (x',y') -> x==x' && y==y') (fun (x,y) -> f x y) in
+ (fun x y -> f'(x,y))
+
+(* Memorizes the last n distinct calls to f. Since there is no hash,
+ Efficient only for small n. *)
+let memon_eq eq n f =
+ let cache = ref [] in (* the cache: a stack *)
+ let m = ref 0 in (* usage of the cache *)
+ let rec find x = function
+ | (x',y')::l when eq x x' -> y', l (* cell is moved to the top *)
+ | [] -> (* we assume n>0, so creating one memo cell is OK *)
+ incr m; (f x, [])
+ | [_] when !m>=n -> f x,[] (* cache is full: dispose of last cell *)
+ | p::l (* not(eq x (fst p)) *) -> let (y,l') = find x l in (y, p::l')
+ in
+ (fun x ->
+ let (y,l) = find x !cache in
+ cache := (x,y)::l;
+ y)
+
+
(*s Size of ocaml values. *)
module Size = struct
diff --git a/lib/util.mli b/lib/util.mli
index 3cd934e7..5432eb98 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
-(*i $Id: util.mli 11769 2009-01-08 17:59:22Z glondu $ i*)
+(*i $Id: util.mli 11897 2009-02-09 19:28:02Z barras $ i*)
(*i*)
open Pp
@@ -298,6 +298,21 @@ val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
val surround : std_ppcmds -> std_ppcmds
+(*s Memoization. *)
+
+(* General comments on memoization:
+ - cache is created whenever the function is supplied (because of
+ ML's polymorphic value restriction).
+ - cache is never flushed (unless the memoized fun is GC'd)
+ *)
+(* One cell memory: memorizes only the last call *)
+val memo1_1 : ('a -> 'b) -> ('a -> 'b)
+val memo1_2 : ('a -> 'b -> 'c) -> ('a -> 'b -> 'c)
+(* with custom equality (used to deal with various arities) *)
+val memo1_eq : ('a -> 'a -> bool) -> ('a -> 'b) -> ('a -> 'b)
+
+(* Memorizes the last [n] distinct calls. Efficient only for small [n]. *)
+val memon_eq : ('a -> 'a -> bool) -> int -> ('a -> 'b) -> ('a -> 'b)
(*s Size of an ocaml value (in words, bytes and kilobytes). *)
diff --git a/library/declaremods.ml b/library/declaremods.ml
index de1893c7..3026143b 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declaremods.ml 11703 2008-12-18 15:54:41Z soubiran $ i*)
+(*i $Id: declaremods.ml 11898 2009-02-10 10:52:45Z soubiran $ i*)
open Pp
open Util
open Names
@@ -628,6 +628,7 @@ let rec get_modtype_substobjs env = function
| MSEwith (mty, With_Definition _) -> get_modtype_substobjs env mty
| MSEwith (mty, With_Module (idl,mp)) ->
let substobjs = get_modtype_substobjs env mty in
+ let mp = Environ.scrape_alias mp env in
let modobjs = MPmap.find mp !modtab_substobjs in
replace_module_object idl substobjs modobjs mp
| MSEapply (mexpr, MSEident mp) ->
diff --git a/library/libnames.ml b/library/libnames.ml
index 3f226179..89a77128 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: libnames.ml 11750 2009-01-05 20:47:34Z herbelin $ i*)
+(*i $Id: libnames.ml 11878 2009-02-03 12:48:18Z soubiran $ i*)
open Pp
open Util
@@ -199,11 +199,23 @@ let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id)
let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id)
let decode_kn kn =
+ let rec dir_of_mp = function
+ | MPfile dir -> repr_dirpath dir
+ | MPbound mbid ->
+ let _,_,dp = repr_mbid mbid in
+ let id = id_of_mbid mbid in
+ id::(repr_dirpath dp)
+ | MPself msid ->
+ let _,_,dp = repr_msid msid in
+ let id = id_of_msid msid in
+ id::(repr_dirpath dp)
+ | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp)
+ in
let mp,sec_dir,l = repr_kn kn in
- match mp,(repr_dirpath sec_dir) with
- MPfile dir,[] -> (dir,id_of_label l)
- | _ , [] -> anomaly "MPfile expected!"
- | _ -> anomaly "Section part should be empty!"
+ if (repr_dirpath sec_dir) = [] then
+ (make_dirpath (dir_of_mp mp)),id_of_label l
+ else
+ anomaly "Section part should be empty!"
let decode_con kn =
let mp,sec_dir,l = repr_con kn in
diff --git a/library/library.ml b/library/library.ml
index 9f3478f0..0e1342f0 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: library.ml 11801 2009-01-18 20:11:41Z herbelin $ *)
+(* $Id: library.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -629,6 +629,8 @@ let error_recursively_dependent_library dir =
strbrk " to save current library because" ++
strbrk " it already depends on a library of this name.")
+(* Security weakness: file might have been changed on disk between
+ writing the content and computing the checksum... *)
let save_library_to dir f =
let cenv, seg = Declaremods.end_library dir in
let md = {
diff --git a/man/coqchk.1 b/man/coqchk.1
new file mode 100644
index 00000000..b0a9c6ab
--- /dev/null
+++ b/man/coqchk.1
@@ -0,0 +1,86 @@
+.TH COQ 1 "February 9, 2009"
+
+.SH NAME
+coqchk \- The Coq Proof Assistant compiled libraries verifier
+
+
+.SH SYNOPSIS
+.B coqchk
+[
+.B options
+]
+.I files-or-modules
+
+
+.SH DESCRIPTION
+
+.B coqchk
+is the standalone checker of compiled libraries (.vo files produced by
+coqc) for the Coq Proof Assistant. See the Reference Manual for more
+information. It returns with exit code 0 if all the requested tasks
+succeeded. A non-zero return code means that something went wrong: some
+library was not found, corrupted content, type-checking failure, etc.
+
+.IR files-or-modules \&
+is a list of modules to be checked. Modules can be referred to either
+by a filename (without the .vo suffix) or by their (possibly
+qualified) module name.
+
+.SH OPTIONS
+
+.TP
+.BI \-I \ dir, \ \-\-include \ dir
+add directory
+.I dir
+in the include path
+
+.TP
+.BI \-R \ dir\ coqdir
+recursively map physical
+.I dir
+to logical
+.I coqdir
+
+.TP
+.BI \-where
+print Coq's standard library location and exit
+
+.TP
+.BI \-silent
+makes coqchk less verbose.
+
+.TP
+.BI \-admit \ file-or-module
+tag the specified module and all its dependencies as trusted, and will
+not be rechecked, unless explicitely requested by other options.
+
+.TP
+.BI \-norec \ file-or-module
+specifies that the given module shall be verified without requesting
+to check its dependencies
+
+.TP
+.BI \-m,\ \-\-memory
+displays a summary of the memory used by the checker
+
+.TP
+.BI \-o,\ \-\-output\-context
+displays a summary of the logical content that have been
+verified: assumptions and usage of impredicativity
+
+.TP
+.BI \-impredicative\-set
+allows the checker to verify libraries that have been compiled with
+this flag.
+
+.SH SEE ALSO
+
+.BR coqtop (1),
+.BR coqc (1),
+.BR coq_makefile (1),
+.BR coqdep (1).
+.br
+.I
+The Coq Reference Manual.
+.I
+The Coq web site: http://coq.inria.fr
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 52b73535..a4880f5e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cases.ml 11708 2008-12-20 10:50:20Z msozeau $ *)
+(* $Id: cases.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Util
open Names
@@ -981,7 +981,8 @@ let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl =
let copti = if depna<>Anonymous then Some (build_dependent_constructor cs) else None in
(* The substituends argsi, copti are all defined in gamma, x1...xn *)
(* We need _parallel_ bindings to get gamma, x1...xn, tms |- ccl'' *)
- let ccl'' = whd_betaiota (subst_predicate (argsi, copti) ccl' tms) in
+ let ccl'' =
+ whd_betaiota Evd.empty (subst_predicate (argsi, copti) ccl' tms) in
(* We adjust ccl st: gamma, x1..xn, x1..xn, tms |- ccl'' *)
let ccl''' = liftn_predicate n (n+1) ccl'' tms in
(* We finally get gamma,x1..xn |- [X1,x1:=R1,x1]..[Xn,xn:=Rn,xn]pred'''*)
@@ -989,7 +990,8 @@ let specialize_predicate newtomatchs (names,(depna,_)) cs tms ccl =
let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms =
let pred= abstract_predicate env (evars_of !evdref) indf current dep tms p in
- (pred, whd_betaiota (applist (pred, realargs@[current])), new_Type ())
+ (pred, whd_betaiota (evars_of !evdref)
+ (applist (pred, realargs@[current])), new_Type ())
let adjust_predicate_from_tomatch ((_,oldtyp),_,(nadep,_)) typ pb =
match typ, oldtyp with
@@ -1211,7 +1213,7 @@ and match_current pb tomatch =
find_predicate pb.caseloc pb.env pb.evdref
pb.pred current indt (names,dep) pb.tomatch in
let ci = make_case_info pb.env mind pb.casestyle in
- let case = mkCase (ci,nf_betaiota pred,current,brvals) in
+ let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in
let inst = List.map mkRel deps in
{ uj_val = applist (case, inst);
uj_type = substl inst typ }
@@ -1454,8 +1456,8 @@ let adjust_to_extended_env_and_remove_deps env extenv subst t =
*)
let abstract_tycon loc env evdref subst _tycon extenv t =
- let t = nf_betaiota t in (* it helps in some cases to remove K-redex... *)
let sigma = evars_of !evdref in
+ let t = nf_betaiota sigma t in (* it helps in some cases to remove K-redex *)
let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv subst t in
(* We traverse the type T of the original problem Xi looking for subterms
that match the non-constructor part of the constraints (this part
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 2a01e901..f4c612a5 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cbv.ml 8802 2006-05-10 20:47:28Z barras $ *)
+(* $Id: cbv.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Util
open Pp
@@ -218,6 +218,11 @@ let rec norm_head info env t stack =
cbv_norm_term info env' c) in
(VAL(0,normt), stack) (* Considérer une coupure commutative ? *)
+ | Evar ev ->
+ (match evar_value info ev with
+ Some c -> norm_head info env c stack
+ | None -> (VAL(0, t), stack))
+
(* non-neutral cases *)
| Lambda _ ->
let ctxt,b = decompose_lam t in
@@ -227,7 +232,7 @@ let rec norm_head info env t stack =
| Construct c -> (CONSTR(c, [||]), stack)
(* neutral cases *)
- | (Sort _ | Meta _ | Ind _|Evar _) -> (VAL(0, t), stack)
+ | (Sort _ | Meta _ | Ind _) -> (VAL(0, t), stack)
| Prod (x,t,c) ->
(VAL(0, mkProd (x, cbv_norm_term info env t,
cbv_norm_term info (subs_lift env) c)),
@@ -353,8 +358,9 @@ let cbv_norm infos constr =
type cbv_infos = cbv_value infos
(* constant bodies are normalized at the first expansion *)
-let create_cbv_infos flgs env =
+let create_cbv_infos flgs env sigma =
create
(fun old_info c -> cbv_stack_term old_info TOP (ESID 0) c)
flgs
env
+ (Reductionops.safe_evar_value sigma)
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 8c969e2c..9ab15886 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: cbv.mli 8799 2006-05-09 21:15:07Z barras $ i*)
+(*i $Id: cbv.mli 11897 2009-02-09 19:28:02Z barras $ i*)
(*i*)
open Names
@@ -22,7 +22,7 @@ open Esubst
(* Entry point for cbv normalization of a constr *)
type cbv_infos
-val create_cbv_infos : RedFlags.reds -> env -> cbv_infos
+val create_cbv_infos : RedFlags.reds -> env -> Evd.evar_map -> cbv_infos
val cbv_norm : cbv_infos -> constr -> constr
(************************************************************************)
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 398da529..27418b4d 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: classops.ml 11343 2008-09-01 20:55:13Z herbelin $ *)
+(* $Id: classops.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Util
open Pp
@@ -143,7 +143,7 @@ let coercion_params coe_info = coe_info.coe_param
(* find_class_type : env -> evar_map -> constr -> cl_typ * int *)
let find_class_type env sigma t =
- let t', args = Reductionops.whd_betaiotazetaevar_stack env sigma t in
+ let t', args = Reductionops.whd_betaiotazeta_stack sigma t in
match kind_of_term t' with
| Var id -> CL_SECVAR id, args
| Const sp -> CL_CONST sp, args
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 8dfec2be..51952f4f 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: clenv.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: clenv.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -254,7 +254,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
{ clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl =
- if isMeta (fst (whd_stack clenv.templtyp.rebus)) then
+ if isMeta (fst (whd_stack (evars_of clenv.evd) clenv.templtyp.rebus)) then
clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) (pf_concl gl)
(clenv_unify_meta_types ~flags:flags clenv)
else
@@ -402,7 +402,7 @@ let error_already_defined b =
(str "Position " ++ int n ++ str" already defined.")
let clenv_unify_binding_type clenv c t u =
- if isMeta (fst (whd_stack u)) then
+ if isMeta (fst (whd_stack (evars_of clenv.evd) u)) then
(* Not enough information to know if some subtyping is needed *)
CoerceToType, clenv, c
else
@@ -416,7 +416,7 @@ let clenv_unify_binding_type clenv c t u =
let clenv_assign_binding clenv k (sigma,c) =
let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
- let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in
+ let c_typ = nf_betaiota (evars_of clenv'.evd) (clenv_get_type_of clenv' c) in
let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in
{ clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd }
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 58369811..4c5ebe3e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evarconv.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
+(* $Id: evarconv.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -62,7 +62,7 @@ let evar_apprec env evd stack c =
in aux (c, append_stack_list stack empty_stack)
let apprec_nohdbeta env evd c =
- match kind_of_term (fst (Reductionops.whd_stack c)) with
+ match kind_of_term (fst (Reductionops.whd_stack (evars_of evd) c)) with
| (Case _ | Fix _) -> applist (evar_apprec env evd [] c)
| _ -> c
@@ -164,18 +164,25 @@ let rec evar_conv_x env evd pbty term1 term2 =
(* Maybe convertible but since reducing can erase evars which [evar_apprec]
could have found, we do it only if the terms are free of evar.
Note: incomplete heuristic... *)
- if is_ground_term evd term1 && is_ground_term evd term2
- && is_ground_env evd env
- then (evd, is_fconv pbty env (evars_of evd) term1 term2)
- else
- let term1 = apprec_nohdbeta env evd term1 in
- let term2 = apprec_nohdbeta env evd term2 in
- if is_undefined_evar evd term1 then
- solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2)
- else if is_undefined_evar evd term2 then
- solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1)
- else
- evar_eqappr_x env evd pbty (decompose_app term1) (decompose_app term2)
+ let ground_test =
+ if is_ground_term evd term1 && is_ground_term evd term2 then
+ if is_fconv pbty env (evars_of evd) term1 term2 then
+ Some true
+ else if is_ground_env evd env then Some false
+ else None
+ else None in
+ match ground_test with
+ Some b -> (evd,b)
+ | None ->
+ let term1 = apprec_nohdbeta env evd term1 in
+ let term2 = apprec_nohdbeta env evd term2 in
+ if is_undefined_evar evd term1 then
+ solve_simple_eqn evar_conv_x env evd (pbty,destEvar term1,term2)
+ else if is_undefined_evar evd term2 then
+ solve_simple_eqn evar_conv_x env evd (pbty,destEvar term2,term1)
+ else
+ evar_eqappr_x env evd pbty
+ (decompose_app term1) (decompose_app term2)
and evar_eqappr_x env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(* Evar must be undefined since we have whd_ised *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b418f996..c0c0b941 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: evarutil.ml 11819 2009-01-20 20:04:50Z herbelin $ *)
+(* $Id: evarutil.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Util
open Pp
@@ -119,7 +119,7 @@ let evars_to_metas sigma (emap, c) =
let emap = nf_evars emap in
let sigma',emap' = push_dependent_evars sigma emap in
let change_exist evar =
- let ty = nf_betaiota (nf_evar emap (existential_type emap evar)) in
+ let ty = nf_betaiota emap (existential_type emap evar) in
let n = new_meta() in
mkCast (mkMeta n, DEFAULTcast, ty) in
let rec replace c =
@@ -906,7 +906,7 @@ let rec invert_definition env evd (evk,argsv as ev) rhs =
map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
imitate envk t in
- let rhs = whd_beta rhs (* heuristic *) in
+ let rhs = whd_beta (evars_of evd) rhs (* heuristic *) in
let body = imitate (env,0) rhs in
(!evdref,body)
@@ -959,9 +959,19 @@ and evar_define env (evk,_ as ev) rhs evd =
(* Auxiliary functions for the conversion algorithms modulo evars
*)
-let has_undefined_evars evd t =
- try let _ = local_strong (whd_ise (evars_of evd)) t in false
- with Uninstantiated_evar _ -> true
+let has_undefined_evars evd t =
+ let evm = evars_of evd in
+ let rec has_ev t =
+ match kind_of_term t with
+ Evar (ev,args) ->
+ (match evar_body (Evd.find evm ev) with
+ | Evar_defined c ->
+ has_ev c; Array.iter has_ev args
+ | Evar_empty ->
+ raise NotInstantiatedEvar)
+ | _ -> iter_constr has_ev t in
+ try let _ = has_ev t in false
+ with (Not_found | NotInstantiatedEvar) -> true
let is_ground_term evd t =
not (has_undefined_evars evd t)
@@ -972,6 +982,9 @@ let is_ground_env evd env =
| _ -> true in
List.for_all is_ground_decl (rel_context env) &&
List.for_all is_ground_decl (named_context env)
+(* Memoization is safe since evar_map and environ are applicative
+ structures *)
+let is_ground_env = memo1_2 is_ground_env
let head_evar =
let rec hrec c = match kind_of_term c with
@@ -1012,6 +1025,7 @@ let is_unification_pattern_evar env (_,args) l t =
l
else
(* Probably strong restrictions coming from t being evar-closed *)
+ let t = expand_vars_in_term env t in
let fv_rels = free_rels t in
let fv_ids = global_vars env t in
List.filter (fun c ->
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index d3123eb6..88a0c2a6 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: indrec.ml 11735 2009-01-02 17:22:31Z herbelin $ *)
+(* $Id: indrec.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -229,7 +229,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
| None ->
lambda_name env
(n,t,process_constr (push_rel d env) (i+1)
- (whd_beta (applist (lift 1 f, [(mkRel 1)])))
+ (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1)])))
(cprest,rest))
| Some(_,f_0) ->
let nF = lift (i+1+decF) f_0 in
@@ -237,7 +237,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
let arg = process_pos env' nF (lift 1 t) in
lambda_name env
(n,t,process_constr env' (i+1)
- (whd_beta (applist (lift 1 f, [(mkRel 1); arg])))
+ (whd_beta Evd.empty (applist (lift 1 f, [(mkRel 1); arg])))
(cprest,rest)))
| (n,Some c,t as d)::cprest, rest ->
mkLetIn
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a1603d69..33928f67 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: reductionops.ml 11796 2009-01-18 13:41:39Z herbelin $ *)
+(* $Id: reductionops.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -114,31 +114,41 @@ type state = constr * constr stack
type contextual_reduction_function = env -> evar_map -> constr -> constr
type reduction_function = contextual_reduction_function
-type local_reduction_function = constr -> constr
+type local_reduction_function = evar_map -> constr -> constr
type contextual_stack_reduction_function =
env -> evar_map -> constr -> constr * constr list
type stack_reduction_function = contextual_stack_reduction_function
-type local_stack_reduction_function = constr -> constr * constr list
+type local_stack_reduction_function =
+ evar_map -> constr -> constr * constr list
type contextual_state_reduction_function =
env -> evar_map -> state -> state
type state_reduction_function = contextual_state_reduction_function
-type local_state_reduction_function = state -> state
+type local_state_reduction_function = evar_map -> state -> state
(*************************************)
(*** Reduction Functions Operators ***)
(*************************************)
-let rec whd_state (x, stack as s) =
+let safe_evar_value sigma ev =
+ try Some (Evd.existential_value sigma ev)
+ with NotInstantiatedEvar | Not_found -> None
+
+let rec whd_state sigma (x, stack as s) =
match kind_of_term x with
- | App (f,cl) -> whd_state (f, append_stack cl stack)
- | Cast (c,_,_) -> whd_state (c, stack)
+ | App (f,cl) -> whd_state sigma (f, append_stack cl stack)
+ | Cast (c,_,_) -> whd_state sigma (c, stack)
+ | Evar ev ->
+ (match safe_evar_value sigma ev with
+ Some c -> whd_state sigma (c,stack)
+ | _ -> s)
| _ -> s
let appterm_of_stack (f,s) = (f,list_of_stack s)
-let whd_stack x = appterm_of_stack (whd_state (x, empty_stack))
+let whd_stack sigma x =
+ appterm_of_stack (whd_state sigma (x, empty_stack))
let whd_castapp_stack = whd_stack
let stack_reduction_of_reduction red_fun env sigma s =
@@ -150,14 +160,14 @@ let strong whdfun env sigma t =
map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in
strongrec env t
-let local_strong whdfun =
- let rec strongrec t = map_constr strongrec (whdfun t) in
+let local_strong whdfun sigma =
+ let rec strongrec t = map_constr strongrec (whdfun sigma t) in
strongrec
-let rec strong_prodspine redfun c =
- let x = redfun c in
+let rec strong_prodspine redfun sigma c =
+ let x = redfun sigma c in
match kind_of_term x with
- | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun b)
+ | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b)
| _ -> x
(*************************************)
@@ -171,7 +181,6 @@ module type RedFlagsSig = sig
type flags
type flag
val fbeta : flag
- val fevar : flag
val fdelta : flag
val feta : flag
val fiota : flag
@@ -179,7 +188,6 @@ module type RedFlagsSig = sig
val mkflags : flag list -> flags
val red_beta : flags -> bool
val red_delta : flags -> bool
- val red_evar : flags -> bool
val red_eta : flags -> bool
val red_iota : flags -> bool
val red_zeta : flags -> bool
@@ -211,14 +219,12 @@ module RedFlags = (struct
type flags = int
let fbeta = 1
let fdelta = 2
- let fevar = 4
let feta = 8
let fiota = 16
let fzeta = 32
let mkflags = List.fold_left (lor) 0
let red_beta f = f land fbeta <> 0
let red_delta f = f land fdelta <> 0
- let red_evar f = f land fevar <> 0
let red_eta f = f land feta <> 0
let red_iota f = f land fiota <> 0
let red_zeta f = f land fzeta <> 0
@@ -229,20 +235,16 @@ open RedFlags
(* Local *)
let beta = mkflags [fbeta]
let eta = mkflags [feta]
-let evar = mkflags [fevar]
-let betaevar = mkflags [fevar; fbeta]
let betaiota = mkflags [fiota; fbeta]
let betaiotazeta = mkflags [fiota; fbeta;fzeta]
-let betaiotazetaevar = mkflags [fiota; fbeta;fzeta;fevar]
(* Contextual *)
-let delta = mkflags [fdelta;fevar]
-let betadelta = mkflags [fbeta;fdelta;fzeta;fevar]
-let betadeltaeta = mkflags [fbeta;fdelta;fzeta;fevar;feta]
-let betadeltaiota = mkflags [fbeta;fdelta;fzeta;fevar;fiota]
-let betadeltaiota_nolet = mkflags [fbeta;fdelta;fevar;fiota]
-let betadeltaiotaeta = mkflags [fbeta;fdelta;fzeta;fevar;fiota;feta]
-let betaiotaevar = mkflags [fbeta;fiota;fevar]
+let delta = mkflags [fdelta]
+let betadelta = mkflags [fbeta;fdelta;fzeta]
+let betadeltaeta = mkflags [fbeta;fdelta;fzeta;feta]
+let betadeltaiota = mkflags [fbeta;fdelta;fzeta;fiota]
+let betadeltaiota_nolet = mkflags [fbeta;fdelta;fiota]
+let betadeltaiotaeta = mkflags [fbeta;fdelta;fzeta;fiota;feta]
let betaetalet = mkflags [fbeta;feta;fzeta]
let betalet = mkflags [fbeta;fzeta]
@@ -303,11 +305,11 @@ let fix_recarg ((recindices,bodynum),_) stack =
type fix_reduction_result = NotReducible | Reduced of state
-let reduce_fix whdfun fix stack =
+let reduce_fix whdfun sigma fix stack =
match fix_recarg fix stack with
| None -> NotReducible
| Some (recargnum,recarg) ->
- let (recarg'hd,_ as recarg') = whdfun (recarg, empty_stack) in
+ let (recarg'hd,_ as recarg') = whdfun sigma (recarg, empty_stack) in
let stack' = stack_assign stack recargnum (app_stack recarg') in
(match kind_of_term recarg'hd with
| Construct _ -> Reduced (contract_fix fix, stack')
@@ -333,8 +335,8 @@ let rec whd_state_gen flags env sigma =
(match lookup_named id env with
| (_,Some body,_) -> whrec (body, stack)
| _ -> s)
- | Evar ev when red_evar flags ->
- (match existential_opt_value sigma ev with
+ | Evar ev ->
+ (match safe_evar_value sigma ev with
| Some body -> whrec (body, stack)
| None -> s)
| Const const when red_delta flags ->
@@ -375,7 +377,7 @@ let rec whd_state_gen flags env sigma =
(mkCase (ci, p, app_stack (c,cargs), lf), stack)
| Fix fix when red_iota flags ->
- (match reduce_fix whrec fix stack with
+ (match reduce_fix (fun _ -> whrec) sigma fix stack with
| Reduced s' -> whrec s'
| NotReducible -> s)
@@ -383,7 +385,7 @@ let rec whd_state_gen flags env sigma =
in
whrec
-let local_whd_state_gen flags =
+let local_whd_state_gen flags sigma =
let rec whrec (x, stack as s) =
match kind_of_term x with
| LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack
@@ -418,105 +420,91 @@ let local_whd_state_gen flags =
(mkCase (ci, p, app_stack (c,cargs), lf), stack)
| Fix fix when red_iota flags ->
- (match reduce_fix whrec fix stack with
+ (match reduce_fix (fun _ ->whrec) sigma fix stack with
| Reduced s' -> whrec s'
| NotReducible -> s)
+ | Evar ev ->
+ (match safe_evar_value sigma ev with
+ Some c -> whrec (c,stack)
+ | None -> s)
+
| x -> s
in
whrec
+let stack_red_of_state_red f sigma x =
+ appterm_of_stack (f sigma (x, empty_stack))
+
+let red_of_state_red f sigma x =
+ app_stack (f sigma (x,empty_stack))
+
(* 1. Beta Reduction Functions *)
let whd_beta_state = local_whd_state_gen beta
-let whd_beta_stack x = appterm_of_stack (whd_beta_state (x, empty_stack))
-let whd_beta x = app_stack (whd_beta_state (x,empty_stack))
+let whd_beta_stack = stack_red_of_state_red whd_beta_state
+let whd_beta = red_of_state_red whd_beta_state
(* Nouveau ! *)
let whd_betaetalet_state = local_whd_state_gen betaetalet
-let whd_betaetalet_stack x =
- appterm_of_stack (whd_betaetalet_state (x, empty_stack))
-let whd_betaetalet x = app_stack (whd_betaetalet_state (x,empty_stack))
+let whd_betaetalet_stack = stack_red_of_state_red whd_betaetalet_state
+let whd_betaetalet = red_of_state_red whd_betaetalet_state
let whd_betalet_state = local_whd_state_gen betalet
-let whd_betalet_stack x = appterm_of_stack (whd_betalet_state (x, empty_stack))
-let whd_betalet x = app_stack (whd_betalet_state (x,empty_stack))
+let whd_betalet_stack = stack_red_of_state_red whd_betalet_state
+let whd_betalet = red_of_state_red whd_betalet_state
(* 2. Delta Reduction Functions *)
let whd_delta_state e = whd_state_gen delta e
-let whd_delta_stack env sigma x =
- appterm_of_stack (whd_delta_state env sigma (x, empty_stack))
-let whd_delta env sigma c =
- app_stack (whd_delta_state env sigma (c, empty_stack))
+let whd_delta_stack env = stack_red_of_state_red (whd_delta_state env)
+let whd_delta env = red_of_state_red (whd_delta_state env)
let whd_betadelta_state e = whd_state_gen betadelta e
-let whd_betadelta_stack env sigma x =
- appterm_of_stack (whd_betadelta_state env sigma (x, empty_stack))
-let whd_betadelta env sigma c =
- app_stack (whd_betadelta_state env sigma (c, empty_stack))
-
-let whd_betaevar_state e = whd_state_gen betaevar e
-let whd_betaevar_stack env sigma c =
- appterm_of_stack (whd_betaevar_state env sigma (c, empty_stack))
-let whd_betaevar env sigma c =
- app_stack (whd_betaevar_state env sigma (c, empty_stack))
+let whd_betadelta_stack env =
+ stack_red_of_state_red (whd_betadelta_state env)
+let whd_betadelta env =
+ red_of_state_red (whd_betadelta_state env)
let whd_betadeltaeta_state e = whd_state_gen betadeltaeta e
-let whd_betadeltaeta_stack env sigma x =
- appterm_of_stack (whd_betadeltaeta_state env sigma (x, empty_stack))
-let whd_betadeltaeta env sigma x =
- app_stack (whd_betadeltaeta_state env sigma (x, empty_stack))
+let whd_betadeltaeta_stack env =
+ stack_red_of_state_red (whd_betadeltaeta_state env)
+let whd_betadeltaeta env =
+ red_of_state_red (whd_betadeltaeta_state env)
(* 3. Iota reduction Functions *)
let whd_betaiota_state = local_whd_state_gen betaiota
-let whd_betaiota_stack x =
- appterm_of_stack (whd_betaiota_state (x, empty_stack))
-let whd_betaiota x =
- app_stack (whd_betaiota_state (x, empty_stack))
+let whd_betaiota_stack = stack_red_of_state_red whd_betaiota_state
+let whd_betaiota = red_of_state_red whd_betaiota_state
let whd_betaiotazeta_state = local_whd_state_gen betaiotazeta
-let whd_betaiotazeta_stack x =
- appterm_of_stack (whd_betaiotazeta_state (x, empty_stack))
-let whd_betaiotazeta x =
- app_stack (whd_betaiotazeta_state (x, empty_stack))
-
-let whd_betaiotazetaevar_state = whd_state_gen betaiotazetaevar
-let whd_betaiotazetaevar_stack env sigma x =
- appterm_of_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack))
-let whd_betaiotazetaevar env sigma x =
- app_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack))
-
-let whd_betaiotaevar_state e = whd_state_gen betaiotaevar e
-let whd_betaiotaevar_stack env sigma x =
- appterm_of_stack (whd_betaiotaevar_state env sigma (x, empty_stack))
-let whd_betaiotaevar env sigma x =
- app_stack (whd_betaiotaevar_state env sigma (x, empty_stack))
+let whd_betaiotazeta_stack = stack_red_of_state_red whd_betaiotazeta_state
+let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state
let whd_betadeltaiota_state e = whd_state_gen betadeltaiota e
-let whd_betadeltaiota_stack env sigma x =
- appterm_of_stack (whd_betadeltaiota_state env sigma (x, empty_stack))
-let whd_betadeltaiota env sigma x =
- app_stack (whd_betadeltaiota_state env sigma (x, empty_stack))
+let whd_betadeltaiota_stack env =
+ stack_red_of_state_red (whd_betadeltaiota_state env)
+let whd_betadeltaiota env =
+ red_of_state_red (whd_betadeltaiota_state env)
let whd_betadeltaiotaeta_state e = whd_state_gen betadeltaiotaeta e
-let whd_betadeltaiotaeta_stack env sigma x =
- appterm_of_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack))
-let whd_betadeltaiotaeta env sigma x =
- app_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack))
+let whd_betadeltaiotaeta_stack env =
+ stack_red_of_state_red (whd_betadeltaiotaeta_state env)
+let whd_betadeltaiotaeta env =
+ red_of_state_red (whd_betadeltaiotaeta_state env)
let whd_betadeltaiota_nolet_state e = whd_state_gen betadeltaiota_nolet e
-let whd_betadeltaiota_nolet_stack env sigma x =
- appterm_of_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack))
-let whd_betadeltaiota_nolet env sigma x =
- app_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack))
+let whd_betadeltaiota_nolet_stack env =
+ stack_red_of_state_red (whd_betadeltaiota_nolet_state env)
+let whd_betadeltaiota_nolet env =
+ red_of_state_red (whd_betadeltaiota_nolet_state env)
(* 3. Eta reduction Functions *)
-let whd_eta c = app_stack (local_whd_state_gen eta (c,empty_stack))
+let whd_eta c = app_stack (local_whd_state_gen eta Evd.empty (c,empty_stack))
(****************************************************************************)
(* Reduction Functions *)
@@ -526,24 +514,25 @@ let whd_eta c = app_stack (local_whd_state_gen eta (c,empty_stack))
let rec whd_evar sigma c =
match kind_of_term c with
| Evar ev ->
- let d =
- try Some (Evd.existential_value sigma ev)
- with NotInstantiatedEvar | Not_found -> None in
- (match d with Some c -> whd_evar sigma c | None -> c)
+ (match safe_evar_value sigma ev with
+ Some c -> whd_evar sigma c
+ | None -> c)
| Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c
| _ -> collapse_appl c
-let nf_evar sigma =
- local_strong (whd_evar sigma)
+let nf_evar =
+ local_strong whd_evar
(* lazy reduction functions. The infos must be created for each term *)
(* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add
a [nf_evar] here *)
let clos_norm_flags flgs env sigma t =
- norm_val (create_clos_infos flgs env) (inject (nf_evar sigma t))
+ norm_val
+ (create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
+ (inject t)
-let nf_beta = clos_norm_flags Closure.beta empty_env Evd.empty
-let nf_betaiota = clos_norm_flags Closure.betaiota empty_env Evd.empty
+let nf_beta = clos_norm_flags Closure.beta empty_env
+let nf_betaiota = clos_norm_flags Closure.betaiota empty_env
let nf_betadeltaiota env sigma =
clos_norm_flags Closure.betadeltaiota env sigma
@@ -553,7 +542,7 @@ let nf_betadeltaiota env sigma =
du type checking :
(fun x => x + x) M
*)
-let rec whd_betaiotaevar_preserving_vm_cast env sigma t =
+let rec whd_betaiota_preserving_vm_cast env sigma t =
let rec stacklam_var subst t stack =
match (decomp_stack stack,kind_of_term t) with
| Some (h,stacktl), Lambda (_,_,c) ->
@@ -568,7 +557,7 @@ let rec whd_betaiotaevar_preserving_vm_cast env sigma t =
and whrec (x, stack as s) =
match kind_of_term x with
| Evar ev ->
- (match existential_opt_value sigma ev with
+ (match safe_evar_value sigma ev with
| Some body -> whrec (body, stack)
| None -> s)
| Cast (c,VMcast,t) ->
@@ -594,12 +583,14 @@ let rec whd_betaiotaevar_preserving_vm_cast env sigma t =
in
app_stack (whrec (t,empty_stack))
-let nf_betaiotaevar_preserving_vm_cast =
- strong whd_betaiotaevar_preserving_vm_cast
+let nf_betaiota_preserving_vm_cast =
+ strong whd_betaiota_preserving_vm_cast
(* lazy weak head reduction functions *)
let whd_flags flgs env sigma t =
- whd_val (create_clos_infos flgs env) (inject (nf_evar sigma t))
+ whd_val
+ (create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
+ (inject t)
(********************************************************************)
(* Conversion *)
@@ -627,23 +618,9 @@ let pb_equal = function
let sort_cmp = sort_cmp
-
-let nf_red_env sigma env =
- let nf_decl = function
- (x,Some t,ty) -> (x,Some (nf_evar sigma t),ty)
- | d -> d in
- let sign = named_context env in
- let ctxt = rel_context env in
- let env = reset_context env in
- let env = Sign.fold_named_context
- (fun d env -> push_named (nf_decl d) env) ~init:env sign in
- Sign.fold_rel_context
- (fun d env -> push_rel (nf_decl d) env) ~init:env ctxt
-
-
-let test_conversion f env sigma x y =
+let test_conversion (f:?evars:'a->'b) env sigma x y =
try let _ =
- f (nf_red_env sigma env) (nf_evar sigma x) (nf_evar sigma y) in true
+ f ~evars:(safe_evar_value sigma) env x y in true
with NotConvertible -> false
let is_conv env sigma = test_conversion Reduction.conv env sigma
@@ -729,7 +706,8 @@ let plain_instance s c =
*)
let instance s c =
- (* if s = [] then c else *) local_strong whd_betaiota (plain_instance s c)
+ (* if s = [] then c else *)
+ local_strong whd_betaiota Evd.empty (plain_instance s c)
(* pseudo-reduction rule:
* [hnf_prod_app env s (Prod(_,B)) N --> B[N]
@@ -830,7 +808,7 @@ let is_sort env sigma arity =
let whd_betaiota_deltazeta_for_iota_state env sigma s =
let rec whrec s =
- let (t, stack as s) = whd_betaiota_state s in
+ let (t, stack as s) = whd_betaiota_state sigma s in
match kind_of_term t with
| Case (ci,p,d,lf) ->
let (cr,crargs) = whd_betadeltaiota_stack env sigma d in
@@ -840,7 +818,7 @@ let whd_betaiota_deltazeta_for_iota_state env sigma s =
else
s
| Fix fix ->
- (match reduce_fix (whd_betadeltaiota_state env sigma) fix stack with
+ (match reduce_fix (whd_betadeltaiota_state env) sigma fix stack with
| Reduced s -> whrec s
| NotReducible -> s)
| _ -> s
@@ -882,7 +860,7 @@ let whd_programs_stack env sigma =
else
(mkCase (ci, p, app_stack(c,cargs), lf), stack)
| Fix fix ->
- (match reduce_fix whrec fix stack with
+ (match reduce_fix (fun _ ->whrec) sigma fix stack with
| Reduced s' -> whrec s'
| NotReducible -> s)
| _ -> s
@@ -952,7 +930,7 @@ let meta_reducible_instance evd b =
| Some (g,(_,s)) -> (mv,(g.rebus,s))::l
| None -> l) [] fm in
let rec irec u =
- let u = whd_betaiota u in
+ let u = whd_betaiota Evd.empty u in
match kind_of_term u with
| Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) ->
let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index c026d9fe..8b3657c7 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: reductionops.mli 11343 2008-09-01 20:55:13Z herbelin $ i*)
+(*i $Id: reductionops.mli 11897 2009-02-09 19:28:02Z barras $ i*)
(*i*)
open Names
@@ -54,17 +54,18 @@ type state = constr * constr stack
type contextual_reduction_function = env -> evar_map -> constr -> constr
type reduction_function = contextual_reduction_function
-type local_reduction_function = constr -> constr
+type local_reduction_function = evar_map -> constr -> constr
type contextual_stack_reduction_function =
env -> evar_map -> constr -> constr * constr list
type stack_reduction_function = contextual_stack_reduction_function
-type local_stack_reduction_function = constr -> constr * constr list
+type local_stack_reduction_function =
+ evar_map -> constr -> constr * constr list
type contextual_state_reduction_function =
env -> evar_map -> state -> state
type state_reduction_function = contextual_state_reduction_function
-type local_state_reduction_function = state -> state
+type local_state_reduction_function = evar_map -> state -> state
(* Removes cast and put into applicative form *)
val whd_stack : local_stack_reduction_function
@@ -92,13 +93,12 @@ val nf_betaiota : local_reduction_function
val nf_betadeltaiota : reduction_function
val nf_evar : evar_map -> constr -> constr
-val nf_betaiotaevar_preserving_vm_cast : reduction_function
+val nf_betaiota_preserving_vm_cast : reduction_function
(* Lazy strategy, weak head reduction *)
val whd_evar : evar_map -> constr -> constr
val whd_beta : local_reduction_function
val whd_betaiota : local_reduction_function
val whd_betaiotazeta : local_reduction_function
-val whd_betaiotazetaevar : contextual_reduction_function
val whd_betadeltaiota : contextual_reduction_function
val whd_betadeltaiota_nolet : contextual_reduction_function
val whd_betaetalet : local_reduction_function
@@ -106,7 +106,7 @@ val whd_betalet : local_reduction_function
val whd_beta_stack : local_stack_reduction_function
val whd_betaiota_stack : local_stack_reduction_function
-val whd_betaiotazetaevar_stack : contextual_stack_reduction_function
+val whd_betaiotazeta_stack : local_stack_reduction_function
val whd_betadeltaiota_stack : contextual_stack_reduction_function
val whd_betadeltaiota_nolet_stack : contextual_stack_reduction_function
val whd_betaetalet_stack : local_stack_reduction_function
@@ -114,7 +114,7 @@ val whd_betalet_stack : local_stack_reduction_function
val whd_beta_state : local_state_reduction_function
val whd_betaiota_state : local_state_reduction_function
-val whd_betaiotazetaevar_state : contextual_state_reduction_function
+val whd_betaiotazeta_state : local_state_reduction_function
val whd_betadeltaiota_state : contextual_state_reduction_function
val whd_betadeltaiota_nolet_state : contextual_state_reduction_function
val whd_betaetalet_state : local_state_reduction_function
@@ -128,12 +128,6 @@ val whd_delta : reduction_function
val whd_betadelta_stack : stack_reduction_function
val whd_betadelta_state : state_reduction_function
val whd_betadelta : reduction_function
-val whd_betaevar_stack : stack_reduction_function
-val whd_betaevar_state : state_reduction_function
-val whd_betaevar : reduction_function
-val whd_betaiotaevar_stack : stack_reduction_function
-val whd_betaiotaevar_state : state_reduction_function
-val whd_betaiotaevar : reduction_function
val whd_betadeltaeta_stack : stack_reduction_function
val whd_betadeltaeta_state : state_reduction_function
val whd_betadeltaeta : reduction_function
@@ -143,8 +137,9 @@ val whd_betadeltaiotaeta : reduction_function
val whd_eta : constr -> constr
+(* Various reduction functions *)
-
+val safe_evar_value : evar_map -> existential -> constr option
val beta_applist : constr * constr list -> constr
@@ -187,7 +182,7 @@ val whd_programs : reduction_function
type fix_reduction_result = NotReducible | Reduced of state
val fix_recarg : fixpoint -> constr stack -> (int * constr) option
-val reduce_fix : local_state_reduction_function -> fixpoint
+val reduce_fix : local_state_reduction_function -> evar_map -> fixpoint
-> constr stack -> fix_reduction_result
(*s Querying the kernel conversion oracle: opaque/transparent constants *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 2465bd1e..19e46a47 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: retyping.ml 11778 2009-01-13 13:17:39Z msozeau $ *)
+(* $Id: retyping.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Util
open Term
@@ -62,9 +62,9 @@ let retype sigma metamap =
let Inductiveops.IndType(_,realargs) =
try Inductiveops.find_rectype env sigma (type_of env c)
with Not_found -> anomaly "type_of: Bad recursive type" in
- let t = whd_beta (applist (p, realargs)) in
+ let t = whd_beta sigma (applist (p, realargs)) in
(match kind_of_term (whd_betadeltaiota env sigma (type_of env t)) with
- | Prod _ -> whd_beta (applist (t, [c]))
+ | Prod _ -> whd_beta sigma (applist (t, [c]))
| _ -> t)
| Lambda (name,c1,c2) ->
mkProd (name, c1, type_of (push_rel (name,None,c1) env) c2)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 88a6f499..740b2ca8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacred.ml 11654 2008-12-03 18:39:40Z barras $ *)
+(* $Id: tacred.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -204,7 +204,7 @@ let invert_name labs l na0 env sigma ref = function
| None -> None
| Some c ->
let labs',ccl = decompose_lam c in
- let _, l' = whd_betalet_stack ccl in
+ let _, l' = whd_betalet_stack sigma ccl in
let labs' = List.map snd labs' in
if labs' = labs & l = l' then Some (minfxargs,ref)
else None
@@ -234,7 +234,7 @@ let compute_consteval_direct sigma env ref =
let compute_consteval_mutual_fix sigma env ref =
let rec srec env minarg labs ref c =
- let c',l = whd_betalet_stack c in
+ let c',l = whd_betalet_stack sigma c in
let nargs = List.length l in
match kind_of_term c' with
| Lambda (na,t,g) when l=[] ->
@@ -378,7 +378,7 @@ let solve_arity_problem env sigma fxminargs c =
let evm = ref sigma in
let set_fix i = evm := Evd.define !evm i (mkVar vfx) in
let rec check strict c =
- let c' = whd_betaiotazeta c in
+ let c' = whd_betaiotazeta sigma c in
let (h,rcargs) = decompose_app c' in
match kind_of_term h with
Evar(i,_) when Intmap.mem i fxminargs && not (Evd.is_defined !evm i) ->
@@ -418,14 +418,14 @@ let substl_checking_arity env subst c =
-let contract_fix_use_function env f
+let contract_fix_use_function env sigma f
((recindices,bodynum),(_names,_types,bodies as typedbodies)) =
let nbodies = Array.length recindices in
let make_Fi j = (mkFix((recindices,j),typedbodies), f j) in
let lbodies = list_tabulate make_Fi nbodies in
- substl_checking_arity env (List.rev lbodies) (nf_beta bodies.(bodynum))
+ substl_checking_arity env (List.rev lbodies) (nf_beta sigma bodies.(bodynum))
-let reduce_fix_use_function env f whfun fix stack =
+let reduce_fix_use_function env sigma f whfun fix stack =
match fix_recarg fix stack with
| None -> NotReducible
| Some (recargnum,recarg) ->
@@ -438,17 +438,18 @@ let reduce_fix_use_function env f whfun fix stack =
let stack' = stack_assign stack recargnum (app_stack recarg') in
(match kind_of_term recarg'hd with
| Construct _ ->
- Reduced (contract_fix_use_function env f fix,stack')
+ Reduced (contract_fix_use_function env sigma f fix,stack')
| _ -> NotReducible)
-let contract_cofix_use_function env f
+let contract_cofix_use_function env sigma f
(bodynum,(_names,_,bodies as typedbodies)) =
let nbodies = Array.length bodies in
let make_Fi j = (mkCoFix(j,typedbodies), f j) in
let subbodies = list_tabulate make_Fi nbodies in
- substl_checking_arity env (List.rev subbodies) (nf_beta bodies.(bodynum))
+ substl_checking_arity env (List.rev subbodies)
+ (nf_beta sigma bodies.(bodynum))
-let reduce_mind_case_use_function func env mia =
+let reduce_mind_case_use_function func env sigma mia =
match kind_of_term mia.mconstr with
| Construct(ind_sp,i) ->
let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in
@@ -476,11 +477,11 @@ let reduce_mind_case_use_function func env mia =
else
fun _ -> None in
let cofix_def =
- contract_cofix_use_function env build_cofix_name cofix in
+ contract_cofix_use_function env sigma build_cofix_name cofix in
mkCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
| _ -> assert false
-let special_red_case sigma env whfun (ci, p, c, lf) =
+let special_red_case env sigma whfun (ci, p, c, lf) =
let rec redrec s =
let (constr, cargs) = whfun s in
if isEvalRef env constr then
@@ -489,7 +490,7 @@ let special_red_case sigma env whfun (ci, p, c, lf) =
| None -> raise Redelimination
| Some gvalue ->
if reducible_mind_case gvalue then
- reduce_mind_case_use_function constr env
+ reduce_mind_case_use_function constr env sigma
{mP=p; mconstr=gvalue; mcargs=list_of_stack cargs;
mci=ci; mlf=lf}
else
@@ -514,15 +515,15 @@ let rec red_elim_const env sigma ref largs =
let c = reference_value sigma env ref in
let c', lrest = whd_betadelta_state env sigma (c,largs) in
let whfun = whd_simpl_state env sigma in
- (special_red_case sigma env whfun (destCase c'), lrest)
+ (special_red_case env sigma whfun (destCase c'), lrest)
| EliminationFix (min,minfxargs,infos) when stack_args_size largs >=min ->
let c = reference_value sigma env ref in
let d, lrest = whd_betadelta_state env sigma (c,largs) in
let f = make_elim_fun ([|Some (minfxargs,ref)|],infos) largs in
let whfun = whd_construct_state env sigma in
- (match reduce_fix_use_function env f whfun (destFix d) lrest with
+ (match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
| NotReducible -> raise Redelimination
- | Reduced (c,rest) -> (nf_beta c, rest))
+ | Reduced (c,rest) -> (nf_beta sigma c, rest))
| EliminationMutualFix (min,refgoal,refinfos)
when stack_args_size largs >= min ->
let rec descend ref args =
@@ -530,15 +531,15 @@ let rec red_elim_const env sigma ref largs =
if ref = refgoal then
(c,args)
else
- let c', lrest = whd_betalet_state (c,args) in
+ let c', lrest = whd_betalet_state sigma (c,args) in
descend (destEvalRef c') lrest in
let (_, midargs as s) = descend ref largs in
let d, lrest = whd_betadelta_state env sigma s in
let f = make_elim_fun refinfos midargs in
let whfun = whd_construct_state env sigma in
- (match reduce_fix_use_function env f whfun (destFix d) lrest with
+ (match reduce_fix_use_function env sigma f whfun (destFix d) lrest with
| NotReducible -> raise Redelimination
- | Reduced (c,rest) -> (nf_beta c, rest))
+ | Reduced (c,rest) -> (nf_beta sigma c, rest))
| _ -> raise Redelimination
(* reduce to whd normal form or to an applied constant that does not hide
@@ -556,11 +557,11 @@ and whd_simpl_state env sigma s =
| Cast (c,_,_) -> redrec (c, stack)
| Case (ci,p,c,lf) ->
(try
- redrec (special_red_case sigma env redrec (ci,p,c,lf), stack)
+ redrec (special_red_case env sigma redrec (ci,p,c,lf), stack)
with
Redelimination -> s)
| Fix fix ->
- (try match reduce_fix (whd_construct_state env sigma) fix stack with
+ (try match reduce_fix (whd_construct_state env) sigma fix stack with
| Reduced s' -> redrec s'
| NotReducible -> s
with Redelimination -> s)
@@ -660,7 +661,7 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c =
| Cast (c,_,_) -> redrec (c, stack)
| Case (ci,p,d,lf) ->
(try
- redrec (special_red_case sigma env whd_all (ci,p,d,lf), stack)
+ redrec (special_red_case env sigma whd_all (ci,p,d,lf), stack)
with Redelimination ->
s)
| Fix fix ->
@@ -795,7 +796,7 @@ let unfoldoccs env sigma ((nowhere_except_in,locs as plocs),name) c =
error ((string_of_evaluable_ref env name)^" does not occur.");
let rest = List.filter (fun o -> o >= nbocc) locs in
if rest <> [] then error_invalid_occurrence rest;
- nf_betaiota uc
+ nf_betaiota sigma uc
(* Unfold reduction tactic: *)
let unfoldn loccname env sigma c =
@@ -824,10 +825,10 @@ let fold_commands cl env sigma c =
(* call by value reduction functions *)
let cbv_norm_flags flags env sigma t =
- cbv_norm (create_cbv_infos flags env) (nf_evar sigma t)
+ cbv_norm (create_cbv_infos flags env sigma) t
-let cbv_beta = cbv_norm_flags beta empty_env Evd.empty
-let cbv_betaiota = cbv_norm_flags betaiota empty_env Evd.empty
+let cbv_beta = cbv_norm_flags beta empty_env
+let cbv_betaiota = cbv_norm_flags betaiota empty_env
let cbv_betadeltaiota env sigma = cbv_norm_flags betadeltaiota env sigma
let compute = cbv_betadeltaiota
@@ -899,11 +900,11 @@ let one_step_reduce env sigma c =
| Cast (c,_,_) -> redrec (c,stack)
| Case (ci,p,c,lf) ->
(try
- (special_red_case sigma env (whd_simpl_state env sigma)
+ (special_red_case env sigma (whd_simpl_state env sigma)
(ci,p,c,lf), stack)
with Redelimination -> raise NotStepReducible)
| Fix fix ->
- (match reduce_fix (whd_construct_state env sigma) fix stack with
+ (match reduce_fix (whd_construct_state env) sigma fix stack with
| Reduced s' -> s'
| NotReducible -> raise NotStepReducible)
| _ when isEvalRef env x ->
@@ -932,7 +933,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
else
(* lazily reduces to match the head of [t] with the expected [ref] *)
let rec elimrec env t l =
- let c, _ = Reductionops.whd_stack t in
+ let c, _ = Reductionops.whd_stack sigma t in
match kind_of_term c with
| Prod (n,ty,t') ->
if allow_product then
@@ -948,7 +949,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
else raise Not_found
with Not_found ->
try
- let t' = nf_betaiota (one_step_reduce env sigma t) in
+ let t' = nf_betaiota sigma (one_step_reduce env sigma t) in
elimrec env t' l
with NotStepReducible ->
errorlabstrm ""
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 981a5605..fb29196c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: unification.ml 11819 2009-01-20 20:04:50Z herbelin $ *)
+(* $Id: unification.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -268,21 +268,25 @@ let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
| Some true ->
(match expand_key curenv cf1 with
| Some c ->
- unirec_rec curenvnb pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN
+ unirec_rec curenvnb pb b substn
+ (whd_betaiotazeta sigma (mkApp(c,l1))) cN
| None ->
(match expand_key curenv cf2 with
| Some c ->
- unirec_rec curenvnb pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
+ unirec_rec curenvnb pb b substn cM
+ (whd_betaiotazeta sigma (mkApp(c,l2)))
| None ->
error_cannot_unify curenv sigma (cM,cN)))
| Some false ->
(match expand_key curenv cf2 with
| Some c ->
- unirec_rec curenvnb pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
+ unirec_rec curenvnb pb b substn cM
+ (whd_betaiotazeta sigma (mkApp(c,l2)))
| None ->
(match expand_key curenv cf1 with
| Some c ->
- unirec_rec curenvnb pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN
+ unirec_rec curenvnb pb b substn
+ (whd_betaiotazeta sigma (mkApp(c,l1))) cN
| None ->
error_cannot_unify curenv sigma (cM,cN)))
else
@@ -489,7 +493,7 @@ let unify_to_type env evd flags c u =
let sigma = evars_of evd in
let c = refresh_universes c in
let t = get_type_of_with_meta env sigma (metas_of evd) c in
- let t = Tacred.hnf_constr env sigma (nf_betaiota (nf_meta evd t)) in
+ let t = Tacred.hnf_constr env sigma (nf_betaiota sigma (nf_meta evd t)) in
let u = Tacred.hnf_constr env sigma u in
try unify_0 env sigma Cumul flags t u
with e when precatchable_exception e -> ([],[])
@@ -613,11 +617,12 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
types of metavars are unifiable with the types of their instances *)
let check_types env evd flags subst m n =
- if isEvar (fst (whd_stack m)) or isEvar (fst (whd_stack n)) then
+ let sigma = evars_of evd in
+ if isEvar (fst (whd_stack sigma m)) or isEvar (fst (whd_stack sigma n)) then
unify_0_with_initial_metas subst true env (evars_of evd) topconv
flags
- (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) m)
- (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) n)
+ (Retyping.get_type_of_with_meta env sigma (metas_of evd) m)
+ (Retyping.get_type_of_with_meta env sigma (metas_of evd) n)
else
subst
@@ -738,8 +743,8 @@ let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
w_merge env false flags ([p,pred,(ConvUpToEta 0,TypeProcessed)],[]) evd'
let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
- let c1, oplist1 = whd_stack ty1 in
- let c2, oplist2 = whd_stack ty2 in
+ let c1, oplist1 = whd_stack (evars_of evd) ty1 in
+ let c2, oplist2 = whd_stack (evars_of evd) ty2 in
match kind_of_term c1, kind_of_term c2 with
| Meta p1, _ ->
(* Find the predicate *)
@@ -777,8 +782,8 @@ let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
Meta(1) had meta-variables in it. *)
let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
let cv_pb = of_conv_pb cv_pb in
- let hd1,l1 = whd_stack ty1 in
- let hd2,l2 = whd_stack ty2 in
+ let hd1,l1 = whd_stack (evars_of evd) ty1 in
+ let hd2,l2 = whd_stack (evars_of evd) ty2 in
match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
(* Pattern case *)
| (Meta _, true, Lambda _, _ | Lambda _, _, Meta _, true)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a04216cb..3e758eb6 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: logic.ml 11796 2009-01-18 13:41:39Z herbelin $ *)
+(* $Id: logic.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -336,7 +336,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
*)
match kind_of_term trm with
| Meta _ ->
- let conclty = nf_betaiota conclty in
+ let conclty = nf_betaiota sigma conclty in
if !check && occur_meta conclty then
raise (RefinerError (MetaInType conclty));
(mk_goal hyps conclty)::goalacc, conclty
@@ -390,7 +390,7 @@ and mk_hdgoals sigma goal goalacc trm =
match kind_of_term trm with
| Cast (c,_, ty) when isMeta c ->
check_typability env sigma ty;
- (mk_goal hyps (nf_betaiota ty))::goalacc,ty
+ (mk_goal hyps (nf_betaiota sigma ty))::goalacc,ty
| Cast (t,_, ty) ->
check_typability env sigma ty;
@@ -502,7 +502,7 @@ let prim_refiner r sigma goal =
raise (RefinerError IntroNeedsProduct))
| Cut (b,replace,id,t) ->
- let sg1 = mk_goal sign (nf_betaiota t) in
+ let sg1 = mk_goal sign (nf_betaiota sigma t) in
let sign,cl,sigma =
if replace then
let nexthyp = get_hyp_after id (named_context_of_val sign) in
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index a9a1f51d..7ce256bf 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: refiner.ml 11865 2009-01-28 17:34:30Z herbelin $ *)
+(* $Id: refiner.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -763,7 +763,7 @@ let extract_pftreestate pts =
else
str "Attempt to save a proof with existential variables still non-instantiated");
let env = Global.env_of_context pts.tpf.goal.evar_hyps in
- nf_betaiotaevar_preserving_vm_cast env pts.tpfsigma pfterm
+ nf_betaiota_preserving_vm_cast env pts.tpfsigma pfterm
(* strong whd_betaiotaevar env pts.tpfsigma pfterm *)
(***
local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index bf194d47..6c4f7b5e 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacmach.ml 11639 2008-11-27 17:48:32Z barras $ *)
+(* $Id: tacmach.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -99,7 +99,7 @@ let pf_whd_betadeltaiota_stack = pf_reduce whd_betadeltaiota_stack
let pf_hnf_constr = pf_reduce hnf_constr
let pf_red_product = pf_reduce red_product
let pf_nf = pf_reduce nf
-let pf_nf_betaiota = pf_reduce (fun _ _ -> nf_betaiota)
+let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota)
let pf_compute = pf_reduce compute
let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds)
let pf_type_of = pf_reduce type_of
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index e609fb77..6a425984 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -9,7 +9,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: class_tactics.ml4 11823 2009-01-21 15:32:37Z msozeau $ *)
+(* $Id: class_tactics.ml4 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -650,14 +650,14 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
| Prod (na, ty, b), obj :: cstrs ->
if dependent (mkRel 1) b then
let (b, arg, evars) = aux (Environ.push_rel (na, None, ty) env) b cstrs in
- let ty = Reductionops.nf_betaiota ty in
+ let ty = Reductionops.nf_betaiota (Evd.evars_of !isevars) ty in
let pred = mkLambda (na, ty, b) in
let liftarg = mkLambda (na, ty, arg) in
let arg' = mkApp (Lazy.force forall_relation, [| ty ; pred ; liftarg |]) in
mkProd(na, ty, b), arg', (ty, None) :: evars
else
let (b', arg, evars) = aux env (subst1 mkProp b) cstrs in
- let ty = Reductionops.nf_betaiota ty in
+ let ty = Reductionops.nf_betaiota(Evd.evars_of !isevars) ty in
let relty = mk_relty ty obj in
let newarg = mkApp (Lazy.force respectful, [| ty ; b' ; relty ; arg |]) in
mkProd(na, ty, b), newarg, (ty, Some relty) :: evars
@@ -665,7 +665,7 @@ let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.
| _, [] ->
(match finalcstr with
None ->
- let t = Reductionops.nf_betaiota ty in
+ let t = Reductionops.nf_betaiota(Evd.evars_of !isevars) ty in
let rel = mk_relty t None in
t, rel, [t, Some rel]
| Some codom -> let (t, rel) = Lazy.force codom in
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 839a494a..2d0395a3 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: decl_proof_instr.ml 11671 2008-12-12 12:43:03Z herbelin $ *)
+(* $Id: decl_proof_instr.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Util
open Pp
@@ -1093,7 +1093,7 @@ let thesis_for obj typ per_info env=
((Printer.pr_constr_env env obj) ++ spc () ++
str "cannot give an induction hypothesis (wrong parameters).") in
let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
- compose_prod rc (whd_beta hd2)
+ compose_prod rc (whd_beta Evd.empty hd2)
let rec build_product_dep pat_info per_info args body gls =
match args with
@@ -1225,7 +1225,7 @@ let hrec_for fix_id per_info gls obj_id =
try List.for_all2 eq_constr params per_info.per_params with
Invalid_argument _ -> false end;
let hd2 = applist (mkVar fix_id,args@[obj]) in
- compose_lam rc (whd_beta hd2)
+ compose_lam rc (whd_beta gls.sigma hd2)
let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
match tree, objs with
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ba18430a..baebee07 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: equality.ml 11800 2009-01-18 18:34:15Z msozeau $ *)
+(* $Id: equality.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -120,7 +120,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs ((c,l) : open_constr with_
let sigma, c' = c in
let sigma = Evd.merge sigma (project gl) in
let ctype = get_type_of env sigma c' in
- let rels, t = decompose_prod (whd_betaiotazeta ctype) in
+ let rels, t = decompose_prod (whd_betaiotazeta sigma ctype) in
match match_with_equality_type t with
| Some (hdcncl,args) -> (* Fast path: direct leibniz rewrite *)
let lft2rgt = adjust_rewriting_direction args lft2rgt in
@@ -737,7 +737,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
else
error "Cannot solve an unification problem."
else
- let (a,p_i_minus_1) = match whd_beta_stack p_i with
+ let (a,p_i_minus_1) = match whd_beta_stack (evars_of !evdref) p_i with
| (_sigS,[a;p]) -> (a,p)
| _ -> anomaly "sig_clausal_form: should be a sigma type" in
let ev = Evarutil.e_new_evar evdref env a in
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 5acc5197..e798f59a 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: leminv.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: leminv.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -237,7 +237,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
meta_types
in
let invProof =
- it_mkNamedLambda_or_LetIn (local_strong (whd_meta mvb) pfterm) ownSign
+ it_mkNamedLambda_or_LetIn
+ (local_strong (fun _ -> whd_meta mvb) Evd.empty pfterm) ownSign
in
invProof
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5af5c0d5..2c567034 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tactics.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
+(* $Id: tactics.ml 11897 2009-02-09 19:28:02Z barras $ *)
open Pp
open Util
@@ -759,7 +759,7 @@ let general_apply with_delta with_destruct with_evars (c,lbind) gl0 =
let concl_nprod = nb_prod (pf_concl gl0) in
let evm, c = c in
let rec try_main_apply c gl =
- let thm_ty0 = nf_betaiota (pf_type_of gl c) in
+ let thm_ty0 = nf_betaiota (project gl) (pf_type_of gl c) in
let try_apply thm_ty nprod =
let n = nb_prod thm_ty - nprod in
if n<0 then error "Applied theorem has not enough premisses.";
@@ -850,7 +850,7 @@ let progress_with_clause flags innerclause clause =
with Failure _ -> error "Unable to unify."
let apply_in_once_main flags innerclause (d,lbind) gl =
- let thm = nf_betaiota (pf_type_of gl d) in
+ let thm = nf_betaiota gl.sigma (pf_type_of gl d) in
let rec aux clause =
try progress_with_clause flags innerclause clause
with err ->
@@ -985,7 +985,8 @@ let specialize mopt (c,lbind) g =
else
let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
let clause = clenv_unify_meta_types clause in
- let (thd,tstack) = whd_stack (clenv_value clause) in
+ let (thd,tstack) =
+ whd_stack (evars_of clause.evd) (clenv_value clause) in
let nargs = List.length tstack in
let tstack = match mopt with
| Some m ->
diff --git a/test-suite/complexity/unification.v b/test-suite/complexity/unification.v
new file mode 100644
index 00000000..0e1ec00d
--- /dev/null
+++ b/test-suite/complexity/unification.v
@@ -0,0 +1,51 @@
+(* Test parsing/interpretation/pretyping on a large example *)
+(* Expected time < 0.10s *)
+
+(* Complexity of unification used to be exponential in the number of nested
+ constants, as pointed out by Georges Gonthier and Nicolas Tabareau (a.o.)
+
+ The problem is that unification of id^n+1(0) and id^n+1(1) proceeds as:
+ - try not unfold the outermost id by trying to unify its arguments:
+ 1st rec. call on id^n(0) id^n(1), which fails
+ - Coq then tries to unfold id^n+1(k) which produces id^n(k)
+ - 2nd rec. call on id^n(0) id^n(1), which also fails
+ Complexity is thus at least exponential.
+
+ This is fixed (in the ground case), by the fact that when we try to
+ unify two ground terms (ie. without unsolved evars), we call kernel
+ conversion and if this fails, then the terms are not unifiable.
+ Hopefully, kernel conversion is not exponential on cases like the one
+ below thanks to sharing (as long as unfolding the fonction does not
+ use its argument under a binder).
+
+ There are probably still many cases where unification goes astray.
+ *)
+
+
+Definition id (n:nat) := n.
+Goal
+ (id (id (id (id
+ (id (id (id (id
+ (id (id (id (id
+ (id (id (id (id
+ (id (id (id (id
+ 0
+ ))))
+ ))))
+ ))))
+ ))))
+ ))))
+ =
+ (id (id (id (id
+ (id (id (id (id
+ (id (id (id (id
+ (id (id (id (id
+ (id (id (id (id
+ 1
+ ))))
+ ))))
+ ))))
+ ))))
+ ))))
+.
+Time try refine (refl_equal _).
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 4d655eac..6da1c6ec 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Cyclic31.v 11034 2008-06-02 08:15:34Z thery $ i*)
+(*i $Id: Cyclic31.v 11907 2009-02-10 23:54:28Z letouzey $ i*)
(** * Int31 numbers defines indeed a cyclic structure : Z/(2^31)Z *)
@@ -1637,7 +1637,12 @@ Section Int31_Spec.
apply Zplus_eq_compat.
ring.
assert ((2*[|y|]) mod wB = 2*[|y|] - wB).
- admit.
+ clear - H. symmetry. apply Zmod_unique with 1; [ | ring ].
+ generalize (phi_lowerbound _ H) (phi_bounded y).
+ set (wB' := 2^Z_of_nat (pred size)).
+ replace wB with (2*wB'); [ omega | ].
+ unfold wB'. rewrite <- Zpower_Zsucc, <- inj_S by (auto with zarith).
+ f_equal.
rewrite H1.
replace wB with (2^(Z_of_nat n)*2^(31-Z_of_nat n)) by
(rewrite <- Zpower_exp; auto with zarith; f_equal; unfold size; ring).
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 19bdeccd..c07b86a6 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: RIneq.v 10762 2008-04-06 16:57:31Z herbelin $ i*)
+(*i $Id: RIneq.v 11887 2009-02-06 19:57:33Z herbelin $ i*)
(*********************************************************)
(** * Basic lemmas for the classical real numbers *)
@@ -1200,7 +1200,7 @@ Hint Resolve Rmult_le_compat: real.
Lemma Rmult_ge_compat :
forall r1 r2 r3 r4,
- 0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4.
+ r2 >= 0 -> r4 >= 0 -> r1 >= r2 -> r3 >= r4 -> r1 * r3 >= r2 * r4.
Proof. auto with real rorders. Qed.
Lemma Rmult_gt_0_lt_compat :
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 3fbf71dd..98457261 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: coq_makefile.ml4 11771 2009-01-09 18:00:56Z notin $ *)
+(* $Id: coq_makefile.ml4 11883 2009-02-06 09:54:52Z herbelin $ *)
(* créer un Makefile pour un développement Coq automatiquement *)
@@ -248,6 +248,7 @@ let implicit () =
print "%.cmxs: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n";
print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
+ print "%.cmxs: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<\n\n";
print "%.ml.d: %.ml\n";
print "\t$(CAMLBIN)ocamldep -slash $(COQSRCLIBS) $(PP) \"$<\" > \"$@\"\n\n"
and v_rule () =