diff options
72 files changed, 1143 insertions, 600 deletions
@@ -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. @@ -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 @@ -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 @@ -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 @@ -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 Binary files differnew file mode 100644 index 00000000..94ce897d --- /dev/null +++ b/ide/coq.ico @@ -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 () = |