diff options
78 files changed, 580 insertions, 592 deletions
diff --git a/.dir-locals.el b/.dir-locals.el deleted file mode 100644 index e32ce14a4..000000000 --- a/.dir-locals.el +++ /dev/null @@ -1,37 +0,0 @@ -;; EMACS CONFIGURATION FOR COQ DEVELOPPERS This configuration will be -;; executed for each opened file under coq root directory. -((nil - . ((eval - . (progn - ;; coq root directory (ending with slash) - (let ((coq-root-directory (when buffer-file-name - (locate-dominating-file - buffer-file-name - ".dir-locals.el"))) - (coq-project-find-file - (and (boundp 'coq-project-find-file) coq-project-find-file))) - ;; coq tags file and coq debugger executable - (set (make-local-variable 'tags-file-name) - (concat coq-root-directory "TAGS")) - (setq camldebug-command-name (concat coq-root-directory - "dev/ocamldebug-coq")) - - ;; Setting the compilation directory to coq root. This is - ;; mutually exclusive with the setting of default-directory - ;; below. Also setting the path for next error. - (unless coq-project-find-file - (set (make-local-variable 'compile-command) - (concat "make -C " coq-root-directory)) - (set (make-local-variable 'compilation-search-path) - (cons coq-root-directory nil))) - - ;; Set default directory to coq root ONLY IF variable - ;; coq-project-find-file is non nil. This should remain a - ;; user preference and not be set by default. This setting - ;; is redundant with compile-command above as M-x compile - ;; always CD's to default directory. To enable it add this - ;; to your emacs config: (setq coq-project-find-file t) - (when coq-project-find-file - (setq default-directory coq-root-directory)))) - )) - )) diff --git a/.gitignore b/.gitignore index 1e7f982a5..b857b754a 100644 --- a/.gitignore +++ b/.gitignore @@ -55,7 +55,7 @@ config/Makefile config/coq_config.ml config/Info-*.plist dev/ocamldebug-coq -dev/camlp4.dbg +dev/camlp5.dbg plugins/micromega/csdpcert plugins/micromega/.micromega.ml.generated kernel/byterun/dllcoqrun.so @@ -266,7 +266,7 @@ cacheclean: find theories plugins test-suite -name '.*.aux' -delete cleanconfig: - rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp4.dbg config/Info-*.plist + rm -f config/Makefile config/coq_config.ml myocamlbuild_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist distclean: clean cleanconfig cacheclean timingclean diff --git a/Makefile.build b/Makefile.build index f0dd46b0f..39d177a13 100644 --- a/Makefile.build +++ b/Makefile.build @@ -196,7 +196,7 @@ COQOPTS=$(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile LOCALINCLUDES=$(addprefix -I ,$(SRCDIRS)) -MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) +MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP5LIB) OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) OCAMLOPT := $(OCAMLFIND) opt $(CAMLFLAGS) @@ -240,8 +240,8 @@ endef # Camlp5 settings -CAMLP4DEPS:=grammar/grammar.cma -CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) +CAMLP5DEPS:=grammar/grammar.cma +CAMLP5USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) @@ -345,14 +345,14 @@ grammar/vernacextend.cmo : $(GRAMBASEDEPS) grammar/tacextend.cmo \ ## Ocaml compiler with the right options and -I for grammar GRAMC := $(OCAMLFIND) ocamlc $(CAMLFLAGS) $(CAMLDEBUG) $(USERFLAGS) \ - -I $(MYCAMLP4LIB) -I grammar + -I $(MYCAMLP5LIB) -I grammar ## Specific rules for grammar.cma grammar/grammar.cma : $(GRAMCMO) $(SHOW)'Testing $@' @touch grammar/test.mlp - $(HIDE)$(GRAMC) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) $^ -impl' -impl grammar/test.mlp -o grammar/test + $(HIDE)$(GRAMC) -pp '$(CAMLP5O) -I $(MYCAMLP5LIB) $^ -impl' -impl grammar/test.mlp -o grammar/test @rm -f grammar/test.* grammar/test $(SHOW)'OCAMLC -a $@' $(HIDE)$(GRAMC) $^ -linkall -a -o $@ @@ -361,7 +361,7 @@ grammar/grammar.cma : $(GRAMCMO) COMPATCMO:= GRAMP4USE:=$(COMPATCMO) pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) -GRAMPP:=$(CAMLP4O) -I $(MYCAMLP4LIB) $(GRAMP4USE) $(CAMLP4COMPAT) -impl +GRAMPP:=$(CAMLP5O) -I $(MYCAMLP5LIB) $(GRAMP4USE) $(CAMLP5COMPAT) -impl ## Rules for standard .mlp and .mli files in grammar/ @@ -406,17 +406,16 @@ $(COQTOPEXE): $(COQTOPBYTE) cp $< $@ endif -# Are "-cclib lcoqrun -dllib -lcoqrun" necessary? +# VMBYTEFLAGS will either contain -custom of the right -dllpath for the VM $(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP) $(SHOW)'COQMKTOP -o $@' $(HIDE)$(OCAMLC) -linkall -linkpkg -I toplevel \ - -I kernel/byterun -dllpath $(abspath kernel/byterun) -cclib -lcoqrun -dllib -lcoqrun \ + -I kernel/byterun/ -cclib -lcoqrun $(VMBYTEFLAGS) \ $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \ $(LINKCMO) $(BYTEFLAGS) \ $(COQTOP_BYTE_MLTOP) toplevel/coqtop_bin.ml -o $@ -# coqc - +# For coqc COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo $(COQC): $(call bestobj, $(COQCCMO)) @@ -684,10 +683,10 @@ plugins/%.cmx: plugins/%.ml $(SHOW)'OCAMLLEX $<' $(HIDE)$(OCAMLLEX) -o $@ "$*.mll" -%.ml: %.ml4 $(CAMLP4DEPS) +%.ml: %.ml4 $(CAMLP5DEPS) $(SHOW)'CAMLP5O $<' - $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) \ - $(CAMLP4DEPS) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@ + $(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) \ + $(CAMLP5DEPS) $(CAMLP5USE) $(CAMLP5COMPAT) -impl $< -o $@ ########################################################################### diff --git a/Makefile.ci b/Makefile.ci index 334827a93..80fbd7bbe 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -1,5 +1,4 @@ -CI_TARGETS=ci-all \ - ci-bignums \ +CI_TARGETS=ci-bignums \ ci-color \ ci-compcert \ ci-coq-dpdgraph \ @@ -23,7 +22,7 @@ CI_TARGETS=ci-all \ ci-unimath \ ci-vst -.PHONY: $(CI_TARGETS) +.PHONY: ci-all $(CI_TARGETS) ci-color: ci-bignums @@ -37,6 +36,8 @@ ci-formal-topology: ci-corn $(CI_TARGETS): ci-%: +./dev/ci/ci-wrapper.sh $* +ci-all: $(CI_TARGETS) + # For emacs: # Local Variables: # mode: makefile diff --git a/Makefile.dev b/Makefile.dev index db83be369..d35ad7501 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -18,9 +18,9 @@ DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo devel: printers -printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp4.dbg +printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp5.dbg -dev/camlp4.dbg: +dev/camlp5.dbg: echo "load_printer gramlib.cma" > $@ ############ diff --git a/Makefile.ide b/Makefile.ide index 09eef1f6b..4846f5e60 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -106,9 +106,9 @@ $(COQIDEBYTE): $(LINKIDE) $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \ lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^ -ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here - $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ +ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp5deps here + $(SHOW)'CAMLP5O $<' + $(HIDE)$(CAMLP5O) -I $(MYCAMLP5LIB) $(PR_O) $(CAMLP5USE) -D$(IDEINT) -impl $< -o $@ ide/%.cmi: ide/%.mli diff --git a/checker/include b/checker/include index 09bf2826c..da0346359 100644 --- a/checker/include +++ b/checker/include @@ -13,7 +13,6 @@ #directory "kernel";; #directory "checker";; #directory "+threads";; -#directory "+camlp4";; #directory "+camlp5";; #load "unix.cma";; diff --git a/config/coq_config.mli b/config/coq_config.mli index e2d9d0d01..5f9ebdc1a 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -28,11 +28,10 @@ val ocamllex : string val camlbin : string (* base directory of OCaml binaries *) val camllib : string (* for Dynlink *) -val camlp4 : string (* exact name of camlp4: either "camlp4" ou "camlp5" *) -val camlp4o : string (* name of the camlp4o/camlp5o executable *) -val camlp4bin : string (* base directory for Camlp4/5 binaries *) -val camlp4lib : string (* where is the library of Camlp4 *) -val camlp4compat : string (* compatibility argument to camlp4/5 *) +val camlp5o : string (* name of the camlp5o executable *) +val camlp5bin : string (* base directory for camlp5 binaries *) +val camlp5lib : string (* where is the library of camlp5 *) +val camlp5compat : string (* compatibility argument to camlp5 *) val coqideincl : string (* arguments for building coqide (e.g. lablgtk) *) val cflags : string (* arguments passed to gcc *) diff --git a/configure.ml b/configure.ml index 06a7dd822..9992e03b8 100644 --- a/configure.ml +++ b/configure.ml @@ -193,7 +193,7 @@ let select_command msg candidates = in search candidates (** As per bug #4828, ocamlfind on Windows/Cygwin barfs if you pass it - a quoted path to camlpXo via -pp. So we only quote camlpXo on not + a quoted path to camlp5o via -pp. So we only quote camlp5o on not Windows, and warn on Windows if the path contains spaces *) let contains_suspicious_characters str = List.fold_left (fun b ch -> String.contains str ch || b) false [' '; '\t'] @@ -487,7 +487,7 @@ let camlbin, caml_version, camllib, findlib_version = then reset_caml_top camlexec (camlbin / "ocaml") in camlbin, caml_version, camllib, findlib_version -let camlp4compat = "-loc loc" +let camlp5compat = "-loc loc" (** Caml version as a list of string, e.g. ["4";"00";"1"] *) @@ -570,9 +570,9 @@ let caml_flags = let coq_caml_flags = coq_warn_error -(** * CamlpX configuration *) +(** * Camlp5 configuration *) -(* Convention: we use camldir as a prioritary location for camlpX, if given *) +(* Convention: we use camldir as a prioritary location for camlp5, if given *) (* i.e., in the case of camlp5, we search for a copy of camlp5o which *) (* answers the right camlp5 lib dir *) @@ -588,7 +588,7 @@ let which_camlp5o_for camlp5lib = if fst (tryrun camlp5o ["-where"]) = camlp5lib then camlp5o else die ("Error: cannot find Camlp5 binaries corresponding to Camlp5 library " ^ camlp5lib) -let which_camlpX base = +let which_camlp5 base = let file = Filename.concat camlbin base in if is_executable file then file else which base @@ -609,7 +609,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with in die msg | None -> try - let camlp5o = which_camlpX "camlp5o" in + let camlp5o = which_camlp5 "camlp5o" in let dir,_ = tryrun camlp5o ["-where"] in dir, camlp5o with Not_found -> @@ -623,15 +623,14 @@ let check_camlp5_version camlp5o = printf "You have Camlp5 %s. Good!\n" version; version | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n" -let config_camlpX () = +let config_camlp5 () = let camlp5mod = "gramlib" in let camlp5libdir, camlp5o = check_camlp5 (camlp5mod^".cma") in let camlp5_version = check_camlp5_version camlp5o in - "camlp5", "Camlp5", camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version + camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version -let camlpX, capitalized_camlpX, camlpXo, - camlpXbindir, fullcamlpXlibdir, - camlpXmod, camlpX_version = config_camlpX () +let camlp5o, camlp5bindir, fullcamlp5libdir, + camlp5mod, camlp5_version = config_camlp5 () let shorten_camllib s = if starts_with s (camllib^"/") then @@ -639,7 +638,7 @@ let shorten_camllib s = "+" ^ String.sub s l (String.length s - l) else s -let camlpXlibdir = shorten_camllib fullcamlpXlibdir +let camlp5libdir = shorten_camllib fullcamlp5libdir (** * Native compiler *) @@ -649,8 +648,8 @@ let msg_byteonly () = let msg_no_ocamlopt () = printf "Cannot find the OCaml native-code compiler.\n"; msg_byteonly () -let msg_no_camlpX_cmxa () = - printf "Cannot find the native-code library of %s.\n" camlpX; msg_byteonly () +let msg_no_camlp5_cmxa () = + printf "Cannot find the native-code library of camlp5.\n"; msg_byteonly () let msg_no_dynlink_cmxa () = printf "Cannot find native-code dynlink library.\n"; msg_byteonly (); @@ -662,8 +661,8 @@ let check_native () = let () = if !Prefs.byteonly then raise Not_found in let version, _ = tryrun camlexec.find ["opt";"-version"] in if version = "" then let () = msg_no_ocamlopt () in raise Not_found - else if not (Sys.file_exists (fullcamlpXlibdir/camlpXmod^".cmxa")) - then let () = msg_no_camlpX_cmxa () in raise Not_found + else if not (Sys.file_exists (fullcamlp5libdir/camlp5mod^".cmxa")) + then let () = msg_no_camlp5_cmxa () in raise Not_found else if fst (tryrun camlexec.find ["query";"dynlink"]) = "" then let () = msg_no_dynlink_cmxa () in raise Not_found else @@ -1015,9 +1014,9 @@ let print_summary () = pr " OCaml binaries in : %s\n" (esc camlbin); pr " OCaml library in : %s\n" (esc camllib); pr " OCaml flambda flags : %s\n" (String.concat " " !Prefs.flambda_flags); - pr " %s version : %s\n" capitalized_camlpX camlpX_version; - pr " %s binaries in : %s\n" capitalized_camlpX (esc camlpXbindir); - pr " %s library in : %s\n" capitalized_camlpX (esc camlpXlibdir); + pr " Camlp5 version : %s\n" camlp5_version; + pr " Camlp5 binaries in : %s\n" (esc camlp5bindir); + pr " Camlp5 library in : %s\n" (esc camlp5libdir); if best_compiler = "opt" then pr " Native dynamic link support : %B\n" hasnatdynlink; if coqide <> "no" then @@ -1057,7 +1056,7 @@ let write_dbg_wrapper f = pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure #\n\n"; pr "export COQTOP=%S\n" coqtop; pr "OCAMLDEBUG=%S\n" (camlbin^"/ocamldebug"); - pr "CAMLP4LIB=%S\n\n" camlpXlibdir; + pr "CAMLP5LIB=%S\n\n" camlp5libdir; pr ". $COQTOP/dev/ocamldebug-coq.run\n"; close_out o; Unix.chmod f 0o555 @@ -1095,11 +1094,10 @@ let write_configml f = pr_s "ocamllex" camlexec.lex; pr_s "camlbin" camlbin; pr_s "camllib" camllib; - pr_s "camlp4" camlpX; - pr_s "camlp4o" camlpXo; - pr_s "camlp4bin" camlpXbindir; - pr_s "camlp4lib" camlpXlibdir; - pr_s "camlp4compat" camlp4compat; + pr_s "camlp5o" camlp5o; + pr_s "camlp5bin" camlp5bindir; + pr_s "camlp5lib" camlp5libdir; + pr_s "camlp5compat" camlp5compat; pr_s "cflags" cflags; pr_s "caml_flags" caml_flags; pr_s "best" best_compiler; @@ -1220,12 +1218,11 @@ let write_makefile f = pr "CAMLDEBUGOPT=%s\n\n" coq_debug_flag; pr "# Compilation profile flag\n"; pr "CAMLTIMEPROF=%s\n\n" coq_profile_flag; - pr "# Camlp4 : flavor, binaries, libraries ...\n"; - pr "# NB : avoid using CAMLP4LIB (conflict under Windows)\n"; - pr "CAMLP4=%s\n" camlpX; - pr "CAMLP4O=%s\n" (win_aware_quote_executable camlpXo); - pr "CAMLP4COMPAT=%s\n" camlp4compat; - pr "MYCAMLP4LIB=%S\n\n" camlpXlibdir; + pr "# Camlp5 : flavor, binaries, libraries ...\n"; + pr "# NB : avoid using CAMLP5LIB (conflict under Windows)\n"; + pr "CAMLP5O=%s\n" (win_aware_quote_executable camlp5o); + pr "CAMLP5COMPAT=%s\n" camlp5compat; + pr "MYCAMLP5LIB=%S\n\n" camlp5libdir; pr "# Your architecture\n"; pr "# Can be obtain by UNIX command arch\n"; pr "ARCH=%s\n" arch; diff --git a/dev/README b/dev/README index 6b83579de..453f85f0d 100644 --- a/dev/README +++ b/dev/README @@ -40,7 +40,11 @@ Documentation of ML interfaces using ocamldoc (directory ocamldoc/html) Other development tools (directory tools) ----------------------- +coqdev.el: helper customizations for everyday Coq development, eg + making `compile' work in subdirectories + objects.el: various development utilities at emacs level + anomaly-traces-parser.el: a .emacs-ready elisp snippet to parse location of Anomaly backtraces and jump to them conveniently from the Emacs *compilation* output. diff --git a/dev/base_include b/dev/base_include index 8b8afbd44..350ccaa10 100644 --- a/dev/base_include +++ b/dev/base_include @@ -19,7 +19,6 @@ #directory "stm";; #directory "vernac";; -#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *) #directory "+camlp5";; (* Gramext is found in top_printers.ml *) #use "top_printers.ml";; diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index c46767821..d8cde39f8 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -794,8 +794,8 @@ function make_ocaml { # TODO: this might not work if PREFIX contains spaces sed -i "s|^PREFIX=.*|PREFIX=$PREFIXOCAML|" config/Makefile - # We don't want to mess up Coq's dirctory structure so put the OCaml library in a separate folder - # If we refer to the make variable ${PREFIX} below, camlp4 ends up having a wrong path: + # We don't want to mess up Coq's directory structure so put the OCaml library in a separate folder + # If we refer to the make variable ${PREFIX} below, camlp5 ends up having the wrong path: # D:\bin\coq64_buildtest_abs_ocaml4\bin>ocamlc -where => D:/bin/coq64_buildtest_abs_ocaml4/libocaml # D:\bin\coq64_buildtest_abs_ocaml4\bin>camlp4 -where => ${PREFIX}/libocaml\camlp4 # So we put an explicit path in there diff --git a/dev/core.dbg b/dev/core.dbg index 00a4355a4..57c136900 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -1,4 +1,4 @@ -source camlp4.dbg +source camlp5.dbg load_printer threads.cma load_printer str.cma load_printer clib.cma diff --git a/dev/doc/build-system.dev.txt b/dev/doc/build-system.dev.txt index f3fc13e96..abba13428 100644 --- a/dev/doc/build-system.dev.txt +++ b/dev/doc/build-system.dev.txt @@ -46,7 +46,7 @@ see build-system.txt . .ml4 files ---------- -.ml4 are converted to .ml by camlp4. By default, they are produced +.ml4 are converted to .ml by camlp5. By default, they are produced in the binary ast format understood by ocamlc/ocamlopt/ocamldep. Pros: - faster than parsing clear-text source file. diff --git a/dev/doc/build-system.txt b/dev/doc/build-system.txt index 873adc1b2..1c4fd2eba 100644 --- a/dev/doc/build-system.txt +++ b/dev/doc/build-system.txt @@ -88,7 +88,7 @@ bootstrapped. The dependencies of a file FOO are in FOO.d . This enables partial recalculation of dependencies (only the dependencies of changed files are recomputed). -If you add a dependency to a Coq camlp4 extension (grammar.cma or +If you add a dependency to a Coq camlp5 extension (grammar.cma or q_constr.cmo), then see sections ".ml4 files" and "new files". Cleaning Targets @@ -127,7 +127,7 @@ of a grammar extension via a line of the form: The use of (*i camlp4use: ... i*) to mention uses of standard extension such as IFDEF has also been discontinued, the Makefile now -always calls camlp4 with pa_macros.cmo and a few others by default. +always calls camlp5 with pa_macros.cmo and a few others by default. For debugging a Coq grammar extension, it could be interesting to use the READABLE_ML4=1 option, otherwise the generated .ml are diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt index 2dbd132da..b3d49b7e5 100644 --- a/dev/doc/coq-src-description.txt +++ b/dev/doc/coq-src-description.txt @@ -25,7 +25,7 @@ intf : grammar : - Camlp4 syntax extensions. The file grammar/grammar.cma is used + Camlp5 syntax extensions. The file grammar/grammar.cma is used to pre-process .ml4 files containing EXTEND constructions, either TACTIC EXTEND, ARGUMENTS EXTEND or VERNAC ... EXTEND. This grammar.cma incorporates many files from other directories diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run index 3cbccab44..f3e60edea 100644 --- a/dev/ocamldebug-coq.run +++ b/dev/ocamldebug-coq.run @@ -3,19 +3,19 @@ # Wrapper around ocamldebug for Coq # This file is to be launched via the generated script ocamldebug-coq, -# which will set the env variables $OCAMLDEBUG, $CAMLP4LIB, $COQTOP +# which will set the env variables $OCAMLDEBUG, $CAMLP5LIB, $COQTOP # Anyway, just in case someone tries to use this script directly, # here are some reasonable default values [ -z "$OCAMLDEBUG" ] && OCAMLDEBUG=ocamldebug -[ -z "$CAMLP4LIB" ] && CAMLP4LIB=+camlp5 +[ -z "$CAMLP5LIB" ] && CAMLP5LIB=+camlp5 [ -z "$COQTOP" -a -d "$PWD/kernel" ] && COQTOP=$PWD [ -z "$COQTOP" -a -d "$PWD/../kernel" ] && COQTOP=`dirname $PWD` export CAML_LD_LIBRARY_PATH=$COQTOP/kernel/byterun:$CAML_LD_LIBRARY_PATH exec $OCAMLDEBUG \ - -I $CAMLP4LIB -I +threads \ + -I $CAMLP5LIB -I +threads \ -I $COQTOP \ -I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \ -I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \ diff --git a/dev/tools/anomaly-traces-parser.el b/dev/tools/anomaly-traces-parser.el deleted file mode 100644 index 68f54266f..000000000 --- a/dev/tools/anomaly-traces-parser.el +++ /dev/null @@ -1,28 +0,0 @@ -;; This Elisp snippet adds a regexp parser for the format of Anomaly -;; backtraces (coqc -bt ...), to the error parser of the Compilation -;; mode (C-c C-c: "Compile command: ..."). Once the -;; coq-change-error-alist-for-backtraces function has run, file -;; locations in traces are recognized and can be jumped from easily -;; from the *compilation* buffer. - -;; You can just copy everything below to your .emacs and this will be -;; enabled from any compilation command launched from an OCaml file. - -(defun coq-change-error-alist-for-backtraces () - "Hook to change the compilation-error-regexp-alist variable, to - search the coq backtraces for error locations" - (interactive) - (add-to-list - 'compilation-error-regexp-alist-alist - '(coq-backtrace - "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\ - lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\ - \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)" - 2 (3 . 4) (5 . 6))) - (add-to-list 'compilation-error-regexp-alist 'coq-backtrace)) - -;; this Anomaly parser should be available when one is hacking -;; on the *OCaml* code of Coq (adding bugs), so we enable it -;; through the OCaml mode hooks. -(add-hook 'caml-mode-hook 'coq-change-error-alist-for-backtraces) -(add-hook 'tuareg-mode-hook 'coq-change-error-alist-for-backtraces) diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el new file mode 100644 index 000000000..8c55be283 --- /dev/null +++ b/dev/tools/coqdev.el @@ -0,0 +1,106 @@ +;;; coqdev.el --- Emacs helpers for Coq development -*- lexical-binding:t -*- + +;; Copyright (C) 2018 The Coq Development Team + +;; Maintainer: coqdev@inria.fr + +;;; Commentary: + +;; Helpers to set compilation commands, proof general variables, etc +;; for Coq development + +;; You can disable individual features without editing this file by +;; using `remove-hook', for instance +;; (remove-hook 'hack-local-variables-hook #'coqdev-setup-compile-command) + +;;; Installation: + +;; To use this, with coqdev.el located at /path/to/coqdev.el, add the +;; following to your init: + +;; (add-to-list 'load-path "/path/to/coqdev/") +;; (require 'coqdev) + +;; If you load this file from a git repository, checking out an old +;; commit will make it disappear and cause errors for your Emacs +;; startup. To ignore those errors use (require 'coqdev nil t). If you +;; check out a malicious commit Emacs startup would allow it to run +;; arbitrary code, to avoid this you can copy coqdev.el to any +;; location and adjust the load path accordingly (of course if you run +;; ./configure to compile Coq it is already too late). + +;;; Code: + +(defun coqdev-default-directory () + "Return the Coq repository containing `default-directory'." + (let ((dir (locate-dominating-file default-directory "META.coq"))) + (when dir (expand-file-name dir)))) + +(defun coqdev-setup-compile-command () + "Setup `compile-command' for Coq development." + (let ((dir (coqdev-default-directory))) + (when dir (setq-local compile-command (concat "make -C " (shell-quote-argument dir)))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-compile-command) + +(defvar camldebug-command-name) ; from camldebug.el (caml package) +(defvar ocamldebug-command-name) ; from ocamldebug.el (tuareg package) +(defun coqdev-setup-camldebug () + "Setup ocamldebug for Coq development. + +Specifically `camldebug-command-name' and `ocamldebug-command-name'." + (let ((dir (coqdev-default-directory))) + (when dir + (setq-local camldebug-command-name + (concat dir "dev/ocamldebug-coq")) + (setq-local ocamldebug-command-name + (concat dir "dev/ocamldebug-coq"))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-camldebug) + +(defun coqdev-setup-tags () + "Setup `tags-file-name' for Coq development." + (let ((dir (coqdev-default-directory))) + (when dir (setq-local tags-file-name (concat dir "TAGS"))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-tags) + +(defvar coq-prog-args) +(defvar coq-prog-name) + +;; Lets us detect whether there are file local variables +;; even though PG sets it with `setq' when there's a _Coqproject. +;; Also makes sense generally, so might make it into PG someday. +(make-variable-buffer-local 'coq-prog-args) +(setq-default coq-prog-args nil) + +(defun coqdev-setup-proofgeneral () + "Setup Proofgeneral variables for Coq development. + +Note that this function is executed before _Coqproject is read if it exists." + (let ((dir (coqdev-default-directory))) + (when dir + (unless coq-prog-args + (setq coq-prog-args + `("-coqlib" ,dir "-R" ,(concat dir "plugins") + "Coq" "-R" ,(concat dir "theories") + "Coq"))) + (setq-local coq-prog-name (concat dir "bin/coqtop"))))) +(add-hook 'hack-local-variables-hook #'coqdev-setup-proofgeneral) + +;; This Elisp snippet adds a regexp parser for the format of Anomaly +;; backtraces (coqc -bt ...), to the error parser of the Compilation +;; mode (C-c C-c: "Compile command: ..."). File locations in traces +;; are recognized and can be jumped from easily in the *compilation* +;; buffer. +(defvar compilation-error-regexp-alist-alist) +(defvar compilation-error-regexp-alist) +(with-eval-after-load 'compile + (add-to-list + 'compilation-error-regexp-alist-alist + '(coq-backtrace + "^ *\\(?:raise\\|frame\\) @ file \\(\"?\\)\\([^,\" \n\t<>]+\\)\\1,\ + lines? \\([0-9]+\\)-?\\([0-9]+\\)?\\(?:$\\|,\ + \\(?: characters? \\([0-9]+\\)-?\\([0-9]+\\)?:?\\)?\\)" + 2 (3 . 4) (5 . 6))) + (add-to-list 'compilation-error-regexp-alist 'coq-backtrace)) + +(provide 'coqdev) +;;; coqdev ends here diff --git a/dev/top_printers.ml b/dev/top_printers.ml index af38ce4b8..f99e2593d 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -485,7 +485,7 @@ let in_current_context f c = let (evmap,sign) = Pfedit.get_current_context () in f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*) -(* We expand the result of preprocessing to be independent of camlp4 +(* We expand the result of preprocessing to be independent of camlp5 VERNAC COMMAND EXTEND PrintPureConstr | [ "PrintPureConstr" constr(c) ] -> [ in_current_context print_pure_constr c ] diff --git a/ide/minilib.ml b/ide/minilib.ml index 2b278fac6..572222c06 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -20,7 +20,7 @@ type level = [ | `FATAL ] (** Some excerpt of Util and similar files to avoid loading the whole - module and its dependencies (and hence Compat and Camlp4) *) + module and its dependencies (and hence Compat and Camlp5) *) let debug = ref false diff --git a/ide/minilib.mli b/ide/minilib.mli index c96e59b22..4f5fbe7db 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -7,7 +7,7 @@ (***********************************************************************) (** Some excerpts of Util and similar files to avoid depending on them - and hence on Compat and Camlp4 *) + and hence on Compat and Camlp5 *) val print_list : (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a list -> unit diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 9febc6449..6d91c3ec9 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -45,6 +45,55 @@ type reloc_table = (tag * int) array type annot_switch = {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} +let rec eq_structured_constant c1 c2 = match c1, c2 with +| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2 +| Const_sorts _, _ -> false +| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 +| Const_ind _, _ -> false +| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2 +| Const_proj _, _ -> false +| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 +| Const_b0 _, _ -> false +| Const_bn (t1, a1), Const_bn (t2, a2) -> + Int.equal t1 t2 && CArray.equal eq_structured_constant a1 a2 +| Const_bn _, _ -> false +| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 +| Const_univ_level _ , _ -> false +| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2 +| Const_type _ , _ -> false + +let rec hash_structured_constant c = + let open Hashset.Combine in + match c with + | Const_sorts s -> combinesmall 1 (Sorts.hash s) + | Const_ind i -> combinesmall 2 (ind_hash i) + | Const_proj p -> combinesmall 3 (Constant.hash p) + | Const_b0 t -> combinesmall 4 (Int.hash t) + | Const_bn (t, a) -> + let fold h c = combine h (hash_structured_constant c) in + let h = Array.fold_left fold 0 a in + combinesmall 5 (combine (Int.hash t) h) + | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l) + | Const_type u -> combinesmall 7 (Univ.Universe.hash u) + +let eq_annot_switch asw1 asw2 = + let eq_ci ci1 ci2 = + eq_ind ci1.ci_ind ci2.ci_ind && + Int.equal ci1.ci_npar ci2.ci_npar && + CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls + in + let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in + eq_ci asw1.ci asw2.ci && + CArray.equal eq_rlc asw1.rtbl asw2.rtbl && + (asw1.tailcall : bool) == asw2.tailcall + +let hash_annot_switch asw = + let open Hashset.Combine in + let h1 = Constr.case_info_hash asw.ci in + let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in + let h3 = if asw.tailcall then 1 else 0 in + combine3 h1 h2 h3 + module Label = struct type t = int diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 5d37a5840..bf2e462e8 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -41,6 +41,12 @@ type reloc_table = (tag * int) array type annot_switch = {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} +val eq_structured_constant : structured_constant -> structured_constant -> bool +val hash_structured_constant : structured_constant -> int + +val eq_annot_switch : annot_switch -> annot_switch -> bool +val hash_annot_switch : annot_switch -> int + module Label : sig type t = int diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index eeea19c12..856b0b465 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -10,18 +10,51 @@ machine, Oct 2004 *) (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) +open Names open Term open Cbytecodes open Copcodes open Mod_subst +type emitcodes = String.t + +external tcode_of_code : Bytes.t -> int -> Vmvalues.tcode = "coq_tcode_of_code" + (* Relocation information *) type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant | Reloc_getglobal of Names.Constant.t -type patch = reloc_info * int +let eq_reloc_info r1 r2 = match r1, r2 with +| Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2 +| Reloc_annot _, _ -> false +| Reloc_const c1, Reloc_const c2 -> eq_structured_constant c1 c2 +| Reloc_const _, _ -> false +| Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2 +| Reloc_getglobal _, _ -> false + +let hash_reloc_info r = + let open Hashset.Combine in + match r with + | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw) + | Reloc_const c -> combinesmall 2 (hash_structured_constant c) + | Reloc_getglobal c -> combinesmall 3 (Constant.hash c) + +module RelocTable = Hashtbl.Make(struct + type t = reloc_info + let equal = eq_reloc_info + let hash = hash_reloc_info +end) + +(** We use arrays for on-disk representation. On 32-bit machines, this means we + can only have a maximum amount of about 4.10^6 relocations, which seems + quite a lot, but potentially reachable if e.g. compiling big proofs. This + would prevent VM computing with these terms on 32-bit architectures. Maybe + we should use a more robust data structure? *) +type patches = { + reloc_infos : (reloc_info * int array) array; +} let patch_char4 buff pos c1 c2 c3 c4 = Bytes.unsafe_set buff pos c1; @@ -29,40 +62,48 @@ let patch_char4 buff pos c1 c2 c3 c4 = Bytes.unsafe_set buff (pos + 2) c3; Bytes.unsafe_set buff (pos + 3) c4 -let patch buff (pos, n) = +let patch1 buff pos n = patch_char4 buff pos (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8)) (Char.unsafe_chr (n asr 16)) (Char.unsafe_chr (n asr 24)) -(* val patch_int : emitcodes -> ((\*pos*\)int * int) list -> emitcodes *) -let patch_int buff patches = +let patch_int buff reloc = (* copy code *before* patching because of nested evaluations: the code we are patching might be called (and thus "concurrently" patched) and results in wrong results. Side-effects... *) let buff = Bytes.of_string buff in - let () = List.iter (fun p -> patch buff p) patches in - (* Note: we follow the apporach suggested by Gabriel Scherer in - PR#136 here, and use unsafe as we own buff. + let iter (reloc, npos) = Array.iter (fun pos -> patch1 buff pos reloc) npos in + let () = CArray.iter iter reloc in + buff - The crux of the question that avoids defining emitcodes just as a - Byte.t is the call to hcons in to_memory below. Even if disabling - this optimization has no visible time impact, test data shows - that the optimization is indeed triggered quite often so we - choose ugliness over altering the semantics. - - Handle with care. - *) - Bytes.unsafe_to_string buff +let patch buff pl f = + (** Order seems important here? *) + let reloc = CArray.map (fun (r, pos) -> (f r, pos)) pl.reloc_infos in + let buff = patch_int buff reloc in + tcode_of_code buff (Bytes.length buff) (* Buffering of bytecode *) -let out_buffer = ref(Bytes.create 1024) -and out_position = ref 0 +type label_definition = + Label_defined of int + | Label_undefined of (int * int) list -let out_word b1 b2 b3 b4 = - let p = !out_position in - if p >= Bytes.length !out_buffer then begin - let len = Bytes.length !out_buffer in +type env = { + mutable out_buffer : Bytes.t; + mutable out_position : int; + mutable label_table : label_definition array; + (* le ieme element de la table = Label_defined n signifie que l'on a + deja rencontrer le label i et qu'il est a l'offset n. + = Label_undefined l signifie que l'on a + pas encore rencontrer ce label, le premier entier indique ou est l'entier + a patcher dans la string, le deuxieme son origine *) + reloc_info : int list RelocTable.t; +} + +let out_word env b1 b2 b3 b4 = + let p = env.out_position in + if p >= Bytes.length env.out_buffer then begin + let len = Bytes.length env.out_buffer in let new_len = if len <= Sys.max_string_length / 2 then 2 * len @@ -71,260 +112,240 @@ let out_word b1 b2 b3 b4 = then invalid_arg "String.create" (* Pas la bonne exception .... *) else Sys.max_string_length in let new_buffer = Bytes.create new_len in - Bytes.blit !out_buffer 0 new_buffer 0 len; - out_buffer := new_buffer + Bytes.blit env.out_buffer 0 new_buffer 0 len; + env.out_buffer <- new_buffer end; - patch_char4 !out_buffer p (Char.unsafe_chr b1) + patch_char4 env.out_buffer p (Char.unsafe_chr b1) (Char.unsafe_chr b2) (Char.unsafe_chr b3) (Char.unsafe_chr b4); - out_position := p + 4 + env.out_position <- p + 4 -let out opcode = - out_word opcode 0 0 0 +let out env opcode = + out_word env opcode 0 0 0 -let out_int n = - out_word n (n asr 8) (n asr 16) (n asr 24) +let out_int env n = + out_word env n (n asr 8) (n asr 16) (n asr 24) (* Handling of local labels and backpatching *) -type label_definition = - Label_defined of int - | Label_undefined of (int * int) list - -let label_table = ref ([| |] : label_definition array) -(* le ieme element de la table = Label_defined n signifie que l'on a - deja rencontrer le label i et qu'il est a l'offset n. - = Label_undefined l signifie que l'on a - pas encore rencontrer ce label, le premier entier indique ou est l'entier - a patcher dans la string, le deuxieme son origine *) - -let extend_label_table needed = - let new_size = ref(Array.length !label_table) in +let extend_label_table env needed = + let new_size = ref(Array.length env.label_table) in while needed >= !new_size do new_size := 2 * !new_size done; let new_table = Array.make !new_size (Label_undefined []) in - Array.blit !label_table 0 new_table 0 (Array.length !label_table); - label_table := new_table - -let backpatch (pos, orig) = - let displ = (!out_position - orig) asr 2 in - Bytes.set !out_buffer pos @@ Char.unsafe_chr displ; - Bytes.set !out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8); - Bytes.set !out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16); - Bytes.set !out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24) - -let define_label lbl = - if lbl >= Array.length !label_table then extend_label_table lbl; - match (!label_table).(lbl) with + Array.blit env.label_table 0 new_table 0 (Array.length env.label_table); + env.label_table <- new_table + +let backpatch env (pos, orig) = + let displ = (env.out_position - orig) asr 2 in + Bytes.set env.out_buffer pos @@ Char.unsafe_chr displ; + Bytes.set env.out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8); + Bytes.set env.out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16); + Bytes.set env.out_buffer (pos+3) @@ Char.unsafe_chr (displ asr 24) + +let define_label env lbl = + if lbl >= Array.length env.label_table then extend_label_table env lbl; + match (env.label_table).(lbl) with Label_defined _ -> raise(Failure "CEmitcode.define_label") | Label_undefined patchlist -> - List.iter backpatch patchlist; - (!label_table).(lbl) <- Label_defined !out_position + List.iter (fun p -> backpatch env p) patchlist; + (env.label_table).(lbl) <- Label_defined env.out_position -let out_label_with_orig orig lbl = - if lbl >= Array.length !label_table then extend_label_table lbl; - match (!label_table).(lbl) with +let out_label_with_orig env orig lbl = + if lbl >= Array.length env.label_table then extend_label_table env lbl; + match (env.label_table).(lbl) with Label_defined def -> - out_int((def - orig) asr 2) + out_int env ((def - orig) asr 2) | Label_undefined patchlist -> (* spiwack: patchlist is supposed to be non-empty all the time thus I commented that out. If there is no problem I suggest removing it for next release (cur: 8.1) *) (*if patchlist = [] then *) - (!label_table).(lbl) <- - Label_undefined((!out_position, orig) :: patchlist); - out_int 0 + (env.label_table).(lbl) <- + Label_undefined((env.out_position, orig) :: patchlist); + out_int env 0 -let out_label l = out_label_with_orig !out_position l +let out_label env l = out_label_with_orig env env.out_position l (* Relocation information *) -let reloc_info = ref ([] : (reloc_info * int) list) +let enter env info = + let pos = env.out_position in + let old = try RelocTable.find env.reloc_info info with Not_found -> [] in + RelocTable.replace env.reloc_info info (pos :: old) -let enter info = - reloc_info := (info, !out_position) :: !reloc_info +let slot_for_const env c = + enter env (Reloc_const c); + out_int env 0 -let slot_for_const c = - enter (Reloc_const c); - out_int 0 +let slot_for_annot env a = + enter env (Reloc_annot a); + out_int env 0 -let slot_for_annot a = - enter (Reloc_annot a); - out_int 0 - -let slot_for_getglobal p = - enter (Reloc_getglobal p); - out_int 0 +let slot_for_getglobal env p = + enter env (Reloc_getglobal p); + out_int env 0 (* Emission of one instruction *) -let emit_instr = function - | Klabel lbl -> define_label lbl +let emit_instr env = function + | Klabel lbl -> define_label env lbl | Kacc n -> - if n < 8 then out(opACC0 + n) else (out opACC; out_int n) + if n < 8 then out env(opACC0 + n) else (out env opACC; out_int env n) | Kenvacc n -> if n >= 1 && n <= 4 - then out(opENVACC1 + n - 1) - else (out opENVACC; out_int n) + then out env(opENVACC1 + n - 1) + else (out env opENVACC; out_int env n) | Koffsetclosure ofs -> if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2 - then out (opOFFSETCLOSURE0 + ofs / 2) - else (out opOFFSETCLOSURE; out_int ofs) + then out env (opOFFSETCLOSURE0 + ofs / 2) + else (out env opOFFSETCLOSURE; out_int env ofs) | Kpush -> - out opPUSH + out env opPUSH | Kpop n -> - out opPOP; out_int n + out env opPOP; out_int env n | Kpush_retaddr lbl -> - out opPUSH_RETADDR; out_label lbl + out env opPUSH_RETADDR; out_label env lbl | Kapply n -> - if n < 4 then out(opAPPLY1 + n - 1) else (out opAPPLY; out_int n) + if n < 4 then out env(opAPPLY1 + n - 1) else (out env opAPPLY; out_int env n) | Kappterm(n, sz) -> - if n < 4 then (out(opAPPTERM1 + n - 1); out_int sz) - else (out opAPPTERM; out_int n; out_int sz) + if n < 4 then (out env(opAPPTERM1 + n - 1); out_int env sz) + else (out env opAPPTERM; out_int env n; out_int env sz) | Kreturn n -> - out opRETURN; out_int n + out env opRETURN; out_int env n | Kjump -> - out opRETURN; out_int 0 + out env opRETURN; out_int env 0 | Krestart -> - out opRESTART + out env opRESTART | Kgrab n -> - out opGRAB; out_int n + out env opGRAB; out_int env n | Kgrabrec(rec_arg) -> - out opGRABREC; out_int rec_arg + out env opGRABREC; out_int env rec_arg | Kclosure(lbl, n) -> - out opCLOSURE; out_int n; out_label lbl + out env opCLOSURE; out_int env n; out_label env lbl | Kclosurerec(nfv,init,lbl_types,lbl_bodies) -> - out opCLOSUREREC;out_int (Array.length lbl_bodies); - out_int nfv; out_int init; - let org = !out_position in - Array.iter (out_label_with_orig org) lbl_types; - let org = !out_position in - Array.iter (out_label_with_orig org) lbl_bodies + out env opCLOSUREREC;out_int env (Array.length lbl_bodies); + out_int env nfv; out_int env init; + let org = env.out_position in + Array.iter (out_label_with_orig env org) lbl_types; + let org = env.out_position in + Array.iter (out_label_with_orig env org) lbl_bodies | Kclosurecofix(nfv,init,lbl_types,lbl_bodies) -> - out opCLOSURECOFIX;out_int (Array.length lbl_bodies); - out_int nfv; out_int init; - let org = !out_position in - Array.iter (out_label_with_orig org) lbl_types; - let org = !out_position in - Array.iter (out_label_with_orig org) lbl_bodies + out env opCLOSURECOFIX;out_int env (Array.length lbl_bodies); + out_int env nfv; out_int env init; + let org = env.out_position in + Array.iter (out_label_with_orig env org) lbl_types; + let org = env.out_position in + Array.iter (out_label_with_orig env org) lbl_bodies | Kgetglobal q -> - out opGETGLOBAL; slot_for_getglobal q + out env opGETGLOBAL; slot_for_getglobal env q | Kconst (Const_b0 i) -> if i >= 0 && i <= 3 - then out (opCONST0 + i) - else (out opCONSTINT; out_int i) + then out env (opCONST0 + i) + else (out env opCONSTINT; out_int env i) | Kconst c -> - out opGETGLOBAL; slot_for_const c + out env opGETGLOBAL; slot_for_const env c | Kmakeblock(n, t) -> if Int.equal n 0 then invalid_arg "emit_instr : block size = 0" - else if n < 4 then (out(opMAKEBLOCK1 + n - 1); out_int t) - else (out opMAKEBLOCK; out_int n; out_int t) + else if n < 4 then (out env(opMAKEBLOCK1 + n - 1); out_int env t) + else (out env opMAKEBLOCK; out_int env n; out_int env t) | Kmakeprod -> - out opMAKEPROD + out env opMAKEPROD | Kmakeswitchblock(typlbl,swlbl,annot,sz) -> - out opMAKESWITCHBLOCK; - out_label typlbl; out_label swlbl; - slot_for_annot annot;out_int sz + out env opMAKESWITCHBLOCK; + out_label env typlbl; out_label env swlbl; + slot_for_annot env annot;out_int env sz | Kswitch (tbl_const, tbl_block) -> let lenb = Array.length tbl_block in let lenc = Array.length tbl_const in assert (lenb < 0x100 && lenc < 0x1000000); - out opSWITCH; - out_word lenc (lenc asr 8) (lenc asr 16) (lenb); -(* out_int (Array.length tbl_const + (Array.length tbl_block lsl 23)); *) - let org = !out_position in - Array.iter (out_label_with_orig org) tbl_const; - Array.iter (out_label_with_orig org) tbl_block + out env opSWITCH; + out_word env lenc (lenc asr 8) (lenc asr 16) (lenb); +(* out_int env (Array.length tbl_const + (Array.length tbl_block lsl 23)); *) + let org = env.out_position in + Array.iter (out_label_with_orig env org) tbl_const; + Array.iter (out_label_with_orig env org) tbl_block | Kpushfields n -> - out opPUSHFIELDS;out_int n + out env opPUSHFIELDS;out_int env n | Kfield n -> - if n <= 1 then out (opGETFIELD0+n) - else (out opGETFIELD;out_int n) + if n <= 1 then out env (opGETFIELD0+n) + else (out env opGETFIELD;out_int env n) | Ksetfield n -> - if n <= 1 then out (opSETFIELD0+n) - else (out opSETFIELD;out_int n) + if n <= 1 then out env (opSETFIELD0+n) + else (out env opSETFIELD;out_int env n) | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr" - | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p) - | Kensurestackcapacity size -> out opENSURESTACKCAPACITY; out_int size + | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_const env (Const_proj p) + | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size (* spiwack *) - | Kbranch lbl -> out opBRANCH; out_label lbl - | Kaddint31 -> out opADDINT31 - | Kaddcint31 -> out opADDCINT31 - | Kaddcarrycint31 -> out opADDCARRYCINT31 - | Ksubint31 -> out opSUBINT31 - | Ksubcint31 -> out opSUBCINT31 - | Ksubcarrycint31 -> out opSUBCARRYCINT31 - | Kmulint31 -> out opMULINT31 - | Kmulcint31 -> out opMULCINT31 - | Kdiv21int31 -> out opDIV21INT31 - | Kdivint31 -> out opDIVINT31 - | Kaddmuldivint31 -> out opADDMULDIVINT31 - | Kcompareint31 -> out opCOMPAREINT31 - | Khead0int31 -> out opHEAD0INT31 - | Ktail0int31 -> out opTAIL0INT31 - | Kisconst lbl -> out opISCONST; out_label lbl - | Kareconst(n,lbl) -> out opARECONST; out_int n; out_label lbl - | Kcompint31 -> out opCOMPINT31 - | Kdecompint31 -> out opDECOMPINT31 - | Klorint31 -> out opORINT31 - | Klandint31 -> out opANDINT31 - | Klxorint31 -> out opXORINT31 + | Kbranch lbl -> out env opBRANCH; out_label env lbl + | Kaddint31 -> out env opADDINT31 + | Kaddcint31 -> out env opADDCINT31 + | Kaddcarrycint31 -> out env opADDCARRYCINT31 + | Ksubint31 -> out env opSUBINT31 + | Ksubcint31 -> out env opSUBCINT31 + | Ksubcarrycint31 -> out env opSUBCARRYCINT31 + | Kmulint31 -> out env opMULINT31 + | Kmulcint31 -> out env opMULCINT31 + | Kdiv21int31 -> out env opDIV21INT31 + | Kdivint31 -> out env opDIVINT31 + | Kaddmuldivint31 -> out env opADDMULDIVINT31 + | Kcompareint31 -> out env opCOMPAREINT31 + | Khead0int31 -> out env opHEAD0INT31 + | Ktail0int31 -> out env opTAIL0INT31 + | Kisconst lbl -> out env opISCONST; out_label env lbl + | Kareconst(n,lbl) -> out env opARECONST; out_int env n; out_label env lbl + | Kcompint31 -> out env opCOMPINT31 + | Kdecompint31 -> out env opDECOMPINT31 + | Klorint31 -> out env opORINT31 + | Klandint31 -> out env opANDINT31 + | Klxorint31 -> out env opXORINT31 (*/spiwack *) | Kstop -> - out opSTOP + out env opSTOP (* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *) -let rec emit insns remaining = match insns with +let rec emit env insns remaining = match insns with | [] -> (match remaining with [] -> () - | (first::rest) -> emit first rest) + | (first::rest) -> emit env first rest) (* Peephole optimizations *) | Kpush :: Kacc n :: c -> - if n < 8 then out(opPUSHACC0 + n) else (out opPUSHACC; out_int n); - emit c remaining + if n < 8 then out env(opPUSHACC0 + n) else (out env opPUSHACC; out_int env n); + emit env c remaining | Kpush :: Kenvacc n :: c -> if n >= 1 && n <= 4 - then out(opPUSHENVACC1 + n - 1) - else (out opPUSHENVACC; out_int n); - emit c remaining + then out env(opPUSHENVACC1 + n - 1) + else (out env opPUSHENVACC; out_int env n); + emit env c remaining | Kpush :: Koffsetclosure ofs :: c -> if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2 - then out(opPUSHOFFSETCLOSURE0 + ofs / 2) - else (out opPUSHOFFSETCLOSURE; out_int ofs); - emit c remaining + then out env(opPUSHOFFSETCLOSURE0 + ofs / 2) + else (out env opPUSHOFFSETCLOSURE; out_int env ofs); + emit env c remaining | Kpush :: Kgetglobal id :: c -> - out opPUSHGETGLOBAL; slot_for_getglobal id; emit c remaining + out env opPUSHGETGLOBAL; slot_for_getglobal env id; emit env c remaining | Kpush :: Kconst (Const_b0 i) :: c -> if i >= 0 && i <= 3 - then out (opPUSHCONST0 + i) - else (out opPUSHCONSTINT; out_int i); - emit c remaining + then out env (opPUSHCONST0 + i) + else (out env opPUSHCONSTINT; out_int env i); + emit env c remaining | Kpush :: Kconst const :: c -> - out opPUSHGETGLOBAL; slot_for_const const; - emit c remaining + out env opPUSHGETGLOBAL; slot_for_const env const; + emit env c remaining | Kpop n :: Kjump :: c -> - out opRETURN; out_int n; emit c remaining + out env opRETURN; out_int env n; emit env c remaining | Ksequence(c1,c2)::c -> - emit c1 (c2::c::remaining) + emit env c1 (c2::c::remaining) (* Default case *) | instr :: c -> - emit_instr instr; emit c remaining + emit_instr env instr; emit env c remaining (* Initialization *) -let init () = - out_position := 0; - label_table := Array.make 16 (Label_undefined []); - reloc_info := [] - -type emitcodes = String.t - -let length = String.length - -type to_patch = emitcodes * (patch list) * fv +type to_patch = emitcodes * patches * fv (* Substitution *) let rec subst_strcst s sc = @@ -334,17 +355,21 @@ let rec subst_strcst s sc = | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) -let subst_patch s (ri,pos) = +let subst_reloc s ri = match ri with | Reloc_annot a -> let (kn,i) = a.ci.ci_ind in let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in - (Reloc_annot {a with ci = ci},pos) - | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos) - | Reloc_getglobal kn -> (Reloc_getglobal (subst_constant s kn), pos) + Reloc_annot {a with ci = ci} + | Reloc_const sc -> Reloc_const (subst_strcst s sc) + | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn) + +let subst_patches subst p = + let infos = CArray.map (fun (r, pos) -> (subst_reloc subst r, pos)) p.reloc_infos in + { reloc_infos = infos; } let subst_to_patch s (code,pl,fv) = - code,List.rev_map (subst_patch s) pl,fv + code, subst_patches s pl, fv type body_code = | BCdefined of to_patch @@ -381,16 +406,23 @@ let repr_body_code = function | PBCconstant -> (None, BCconstant) let to_memory (init_code, fun_code, fv) = - init(); - emit init_code []; - emit fun_code []; + let env = { + out_buffer = Bytes.create 1024; + out_position = 0; + label_table = Array.make 16 (Label_undefined []); + reloc_info = RelocTable.create 91; + } in + emit env init_code []; + emit env fun_code []; (** Later uses of this string are all purely functional *) - let code = Bytes.sub_string !out_buffer 0 !out_position in + let code = Bytes.sub_string env.out_buffer 0 env.out_position in let code = CString.hcons code in - let reloc = List.rev !reloc_info in + let fold reloc npos accu = (reloc, Array.of_list npos) :: accu in + let reloc = RelocTable.fold fold env.reloc_info [] in + let reloc = { reloc_infos = CArray.of_list reloc } in Array.iter (fun lbl -> (match lbl with Label_defined _ -> assert true | Label_undefined patchlist -> - assert (patchlist = []))) !label_table; + assert (patchlist = []))) env.label_table; (code, reloc, fv) diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index fee45aafd..03920dc1a 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -6,20 +6,12 @@ type reloc_info = | Reloc_const of structured_constant | Reloc_getglobal of Constant.t -type patch = reloc_info * int - -(* A virer *) -val subst_patch : Mod_subst.substitution -> patch -> patch - +type patches type emitcodes -val length : emitcodes -> int - -val patch_int : emitcodes -> ((*pos*)int * int) list -> emitcodes - -type to_patch = emitcodes * (patch list) * fv +val patch : emitcodes -> patches -> (reloc_info -> int) -> Vmvalues.tcode -val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch +type to_patch = emitcodes * patches * fv type body_code = | BCdefined of to_patch diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index bbd284bc1..55430a9d8 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -14,7 +14,6 @@ open Util open Names -open Constr open Vmvalues open Cemitcodes open Cbytecodes @@ -25,7 +24,6 @@ open Cbytegen module NamedDecl = Context.Named.Declaration module RelDecl = Context.Rel.Declaration -external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code" external eval_tcode : tcode -> values array -> values = "coq_eval_tcode" (*******************) @@ -56,61 +54,12 @@ let set_global v = (* table pour les structured_constant et les annotations des switchs *) -let rec eq_structured_constant c1 c2 = match c1, c2 with -| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2 -| Const_sorts _, _ -> false -| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 -| Const_ind _, _ -> false -| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2 -| Const_proj _, _ -> false -| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 -| Const_b0 _, _ -> false -| Const_bn (t1, a1), Const_bn (t2, a2) -> - Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2 -| Const_bn _, _ -> false -| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 -| Const_univ_level _ , _ -> false -| Const_type u1, Const_type u2 -> Univ.Universe.equal u1 u2 -| Const_type _ , _ -> false - -let rec hash_structured_constant c = - let open Hashset.Combine in - match c with - | Const_sorts s -> combinesmall 1 (Sorts.hash s) - | Const_ind i -> combinesmall 2 (ind_hash i) - | Const_proj p -> combinesmall 3 (Constant.hash p) - | Const_b0 t -> combinesmall 4 (Int.hash t) - | Const_bn (t, a) -> - let fold h c = combine h (hash_structured_constant c) in - let h = Array.fold_left fold 0 a in - combinesmall 5 (combine (Int.hash t) h) - | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l) - | Const_type u -> combinesmall 7 (Univ.Universe.hash u) - module SConstTable = Hashtbl.Make (struct type t = structured_constant let equal = eq_structured_constant let hash = hash_structured_constant end) -let eq_annot_switch asw1 asw2 = - let eq_ci ci1 ci2 = - eq_ind ci1.ci_ind ci2.ci_ind && - Int.equal ci1.ci_npar ci2.ci_npar && - Array.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls - in - let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in - eq_ci asw1.ci asw2.ci && - Array.equal eq_rlc asw1.rtbl asw2.rtbl && - (asw1.tailcall : bool) == asw2.tailcall - -let hash_annot_switch asw = - let open Hashset.Combine in - let h1 = Constr.case_info_hash asw.ci in - let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in - let h3 = if asw.tailcall then 1 else 0 in - combine3 h1 h2 h3 - module AnnotTable = Hashtbl.Make (struct type t = annot_switch let equal = eq_annot_switch @@ -205,15 +154,13 @@ and slot_for_fv env fv = assert false and eval_to_patch env (buff,pl,fv) = - let patch = function - | Reloc_annot a, pos -> (pos, slot_for_annot a) - | Reloc_const sc, pos -> (pos, slot_for_str_cst sc) - | Reloc_getglobal kn, pos -> (pos, slot_for_getglobal env kn) + let slots = function + | Reloc_annot a -> slot_for_annot a + | Reloc_const sc -> slot_for_str_cst sc + | Reloc_getglobal kn -> slot_for_getglobal env kn in - let patches = List.map_left patch pl in - let buff = patch_int buff patches in + let tc = patch buff pl slots in let vm_env = Array.map (slot_for_fv env) fv in - let tc = tcode_of_code buff (length buff) in eval_tcode tc vm_env and val_of_constr env c = diff --git a/lib/envars.ml b/lib/envars.ml index 8ebf84057..9b66c1f71 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -155,23 +155,21 @@ let exe s = s ^ Coq_config.exec_extension let ocamlfind () = Coq_config.ocamlfind -(** {2 Camlp4 paths} *) +(** {2 Camlp5 paths} *) -let guess_camlp4bin () = which (user_path ()) (exe Coq_config.camlp4) +let guess_camlp5bin () = which (user_path ()) (exe "camlp5") -let camlp4bin () = - if !Flags.boot then Coq_config.camlp4bin else - try guess_camlp4bin () +let camlp5bin () = + if !Flags.boot then Coq_config.camlp5bin else + try guess_camlp5bin () with Not_found -> - Coq_config.camlp4bin + Coq_config.camlp5bin -let camlp4 () = camlp4bin () / exe Coq_config.camlp4 - -let camlp4lib () = +let camlp5lib () = if !Flags.boot then - Coq_config.camlp4lib + Coq_config.camlp5lib else - let ex, res = CUnix.run_command (ocamlfind () ^ " query " ^ Coq_config.camlp4) in + let ex, res = CUnix.run_command (ocamlfind () ^ " query camlp5") in match ex with | Unix.WEXITED 0 -> String.strip res | _ -> "/dev/null" @@ -206,11 +204,10 @@ let print_config ?(prefix_var_name="") f coq_src_subdirs = fprintf f "%sCOQLIB=%s/\n" prefix_var_name (coqlib ()); fprintf f "%sDOCDIR=%s/\n" prefix_var_name (docdir ()); fprintf f "%sOCAMLFIND=%s\n" prefix_var_name (ocamlfind ()); - fprintf f "%sCAMLP4=%s\n" prefix_var_name Coq_config.camlp4; - fprintf f "%sCAMLP4O=%s\n" prefix_var_name Coq_config.camlp4o; - fprintf f "%sCAMLP4BIN=%s/\n" prefix_var_name (camlp4bin ()); - fprintf f "%sCAMLP4LIB=%s\n" prefix_var_name (camlp4lib ()); - fprintf f "%sCAMLP4OPTIONS=%s\n" prefix_var_name Coq_config.camlp4compat; + fprintf f "%sCAMLP5O=%s\n" prefix_var_name Coq_config.camlp5o; + fprintf f "%sCAMLP5BIN=%s/\n" prefix_var_name (camlp5bin ()); + fprintf f "%sCAMLP5LIB=%s\n" prefix_var_name (camlp5lib ()); + fprintf f "%sCAMLP5OPTIONS=%s\n" prefix_var_name Coq_config.camlp5compat; fprintf f "%sCAMLFLAGS=%s\n" prefix_var_name Coq_config.caml_flags; fprintf f "%sHASNATDYNLINK=%s\n" prefix_var_name (if Coq_config.has_natdynlink then "true" else "false"); diff --git a/lib/envars.mli b/lib/envars.mli index 09f2b4ca1..1ccd1feff 100644 --- a/lib/envars.mli +++ b/lib/envars.mli @@ -56,14 +56,11 @@ val coqpath : string list (** [camlfind ()] is the path to the ocamlfind binary. *) val ocamlfind : unit -> string -(** [camlp4bin ()] is the path to the camlp4 binary. *) -val camlp4bin : unit -> string +(** [camlp5bin ()] is the path to the camlp5 binary. *) +val camlp5bin : unit -> string -(** [camlp4lib ()] is the path to the camlp4 library. *) -val camlp4lib : unit -> string - -(** [camlp4 ()] is the camlp4 utility. *) -val camlp4 : unit -> string +(** [camlp5lib ()] is the path to the camlp5 library. *) +val camlp5lib : unit -> string (** Coq tries to honor the XDG Base Directory Specification to access the user's configuration files. diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 9c2766187..ea6266dd4 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -21,11 +21,11 @@ open Names a reference to the current level (to be translated into "SELF" on the left border and into "constr LEVEL n" elsewhere), to the level below (to be translated into "NEXT") or to an below wrt associativity (to be - translated in camlp4 into "constr" without level) or to another level + translated in camlp5 into "constr" without level) or to another level (to be translated into "constr LEVEL n") The boolean is true if the entry was existing _and_ empty; this to - circumvent a weakness of camlp4/camlp5 whose undo mechanism is not the + circumvent a weakness of camlp5 whose undo mechanism is not the converse of the extension mechanism *) let constr_level = string_of_int @@ -144,11 +144,11 @@ let find_position accu forpat assoc level = (**************************************************************************) (* - * --- Note on the mapping of grammar productions to camlp4 actions --- + * --- Note on the mapping of grammar productions to camlp5 actions --- * * Translation of environments: a production * [ nt1(x1) ... nti(xi) ] -> act(x1..xi) - * is written (with camlp4 conventions): + * is written (with camlp5 conventions): * (fun vi -> .... (fun v1 -> act(v1 .. vi) )..) * where v1..vi are the values generated by non-terminals nt1..nti. * Since the actions are executed by substituting an environment, @@ -172,8 +172,8 @@ let find_position accu forpat assoc level = (**********************************************************************) (* Binding constr entry keys to entries *) -(* Camlp4 levels do not treat NonA: use RightA with a NEXT on the left *) -let camlp4_assoc = function +(* Camlp5 levels do not treat NonA: use RightA with a NEXT on the left *) +let camlp5_assoc = function | Some NonA | Some RightA -> RightA | None | Some LeftA -> LeftA @@ -205,7 +205,7 @@ let adjust_level assoc from = function (* If NonA on the left-hand side, adopt the current assoc ?? *) | (NumLevel n,BorderProd (Left,Some NonA)) -> None (* If the expected assoc is the current one, set to SELF *) - | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp4_assoc assoc) -> + | (NumLevel n,BorderProd (Left,Some a)) when assoc_eq a (camlp5_assoc assoc) -> None (* Otherwise, force the level, n or n-1, according to expected assoc *) | (NumLevel n,BorderProd (Left,Some a)) -> diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 8e0469275..1e3869818 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Mapping of grammar productions to camlp4 actions *) +(** Mapping of grammar productions to camlp5 actions *) (** This is the part specific to Coq-level Notation and Tactic Notation. For the ML-level tactic and vernac extensions, see Egramml. *) diff --git a/parsing/egramml.mli b/parsing/egramml.mli index 7414773d3..74dd95a20 100644 --- a/parsing/egramml.mli +++ b/parsing/egramml.mli @@ -8,7 +8,7 @@ open Vernacexpr -(** Mapping of grammar productions to camlp4 actions. *) +(** Mapping of grammar productions to camlp5 actions. *) (** This is the part specific to vernac extensions. For the Coq-level Notation and Tactic Notation, see Egramcoq. *) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3244b0ff2..d42b5f622 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -17,7 +17,7 @@ open Vernacexpr open Decl_kinds open Declarations open Misctypes -open Tok (* necessary for camlp4 *) +open Tok (* necessary for camlp5 *) open Pcoq open Pcoq.Prim @@ -827,7 +827,7 @@ GEXTEND Gram command: [ [ IDENT "Comments"; l = LIST0 comment -> VernacComments l - (* Hack! Should be in grammar_ext, but camlp4 factorize badly *) + (* Hack! Should be in grammar_ext, but camlp5 factorizes badly *) | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":"; expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200"; info = hint_info -> diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index c934d38a2..54e7949ae 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -202,7 +202,7 @@ end = struct end -let camlp4_verbosity silent f x = +let camlp5_verbosity silent f x = let a = !warning_verbose in warning_verbose := silent; f x; @@ -274,7 +274,7 @@ type ext_kind = (** The list of extensions *) -let camlp4_state = ref [] +let camlp5_state = ref [] (** Deletion *) @@ -299,13 +299,13 @@ let grammar_delete e reinit (pos,rls) = let grammar_extend e reinit ext = let ext = of_coq_extend_statement ext in let undo () = grammar_delete e reinit ext in - let redo () = camlp4_verbosity false (uncurry (G.extend e)) ext in - camlp4_state := ByEXTEND (undo, redo) :: !camlp4_state; + let redo () = camlp5_verbosity false (uncurry (G.extend e)) ext in + camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () let grammar_extend_sync e reinit ext = - camlp4_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp4_state; - camlp4_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext) + camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state; + camlp5_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext) (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -315,20 +315,20 @@ module Gram = include G let extend e = curry - (fun ext -> - camlp4_state := - (ByEXTEND ((fun () -> grammar_delete e None ext), - (fun () -> uncurry (G.extend e) ext))) - :: !camlp4_state; - uncurry (G.extend e) ext) + (fun ext -> + camlp5_state := + (ByEXTEND ((fun () -> grammar_delete e None ext), + (fun () -> uncurry (G.extend e) ext))) + :: !camlp5_state; + uncurry (G.extend e) ext) let delete_rule e pil = (* spiwack: if you use load an ML module which contains GDELETE_RULE - in a section, God kills a kitty. As it would corrupt remove_grammars. + in a section, God kills a kitty. As it would corrupt remove_grammars. There does not seem to be a good way to undo a delete rule. As deleting - takes fewer arguments than extending. The production rule isn't returned - by delete_rule. If we could retrieve the necessary information, then - ByEXTEND provides just the framework we need to allow this in section. - I'm not entirely sure it makes sense, but at least it would be more correct. + takes fewer arguments than extending. The production rule isn't returned + by delete_rule. If we could retrieve the necessary information, then + ByEXTEND provides just the framework we need to allow this in section. + I'm not entirely sure it makes sense, but at least it would be more correct. *) G.delete_rule e pil end @@ -340,18 +340,18 @@ module Gram = let rec remove_grammars n = if n>0 then - (match !camlp4_state with + (match !camlp5_state with | [] -> anomaly ~label:"Pcoq.remove_grammars" (Pp.str "too many rules to remove.") | ByGrammar (ExtendRule (g, reinit, ext)) :: t -> grammar_delete g reinit (of_coq_extend_statement ext); - camlp4_state := t; + camlp5_state := t; remove_grammars (n-1) | ByEXTEND (undo,redo)::t -> undo(); - camlp4_state := t; + camlp5_state := t; remove_grammars n; redo(); - camlp4_state := ByEXTEND (undo,redo) :: !camlp4_state) + camlp5_state := ByEXTEND (undo,redo) :: !camlp5_state) let make_rule r = [None, None, r] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 756d9487d..75378d2c6 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -124,7 +124,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e | | Egrammar.make_constr_prod_item V - Gramext.g_symbol list which is sent to camlp4 + Gramext.g_symbol list which is sent to camlp5 For user level tactic notations, dynamic addition of new rules is also done in several steps: @@ -161,9 +161,9 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e *) -(** Temporarily activate camlp4 verbosity *) +(** Temporarily activate camlp5 verbosity *) -val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit +val camlp5_verbosity : bool -> ('a -> unit) -> 'a -> unit (** Parse a string *) diff --git a/parsing/tok.ml b/parsing/tok.ml index 0917e8d6d..fafad2779 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -60,7 +60,7 @@ let match_keyword kwd = function | KEYWORD kwd' when kwd = kwd' -> true | _ -> false -(* Needed to fix Camlp4 signature. +(* Needed to fix Camlp5 signature. Cannot use Pp because of silly Tox -> Compat -> Pp dependency *) let print ppf tok = Format.pp_print_string ppf (to_string tok) diff --git a/parsing/tok.mli b/parsing/tok.mli index 59a79dcd2..162310e2a 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -22,7 +22,7 @@ type t = val equal : t -> t -> bool val extract_string : t -> string val to_string : t -> string -(* Needed to fit Camlp4 signature *) +(* Needed to fit Camlp5 signature *) val print : Format.formatter -> t -> unit val match_keyword : string -> t -> bool (** for camlp5 *) diff --git a/plugins/.dir-locals.el b/plugins/.dir-locals.el deleted file mode 100644 index 4e8830f6c..000000000 --- a/plugins/.dir-locals.el +++ /dev/null @@ -1,4 +0,0 @@ -((coq-mode . ((eval . (let ((default-directory (locate-dominating-file - buffer-file-name ".dir-locals.el"))) - (setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq")) - (setq-local coq-prog-name (expand-file-name "../bin/coqtop"))))))) diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4 index 23b91507c..896bb91f1 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin DECLARE PLUGIN "btauto_plugin" diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4 index 6ed4672ce..0d677ac7a 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin open Cctac open Stdarg diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 index df701ed80..72057cd9b 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.ml4 @@ -8,8 +8,6 @@ open Stdarg -(*i camlp4deps: "grammar/grammar.cma" i*) - DECLARE PLUGIN "derive_plugin" let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 24c70bccf..4b6de58bd 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Pcoq.Prim DECLARE PLUGIN "extraction_plugin" diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index b81010c7b..3c6ab47e9 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) open Ltac_plugin open Formula diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 index 682673e8d..16dd4c886 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin open FourierR diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 4b828a702..ac7a2f284 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -5,7 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) open Ltac_plugin open Util open Pp diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 2769802cf..7d2c4d082 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Util open Locus open Misctypes diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index bb01aca55..4c6d3c2d3 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Pp open Genarg open Stdarg diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 3e3965b94..286f9d95d 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Pp open Genarg open Stdarg diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 90a44708f..f74d24db0 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Pp open Genarg open Stdarg diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index ed2d9da63..014433ac4 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Class_tactics open Stdarg open Tacarg diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4 index 549436902..f705778fc 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.ml4 @@ -12,8 +12,6 @@ (* by Eduardo Gimenez *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Eqdecide DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index cc7ce339b..9ef819569 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - DECLARE PLUGIN "ltac_plugin" open Util @@ -17,7 +15,7 @@ open Tacexpr open Misctypes open Genarg open Genredexpr -open Tok (* necessary for camlp4 *) +open Tok (* necessary for camlp5 *) open Names open Pcoq diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index f6cc3833a..e251b1049 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -6,11 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - (* Syntax for the subtac terms and types. - Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) + Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) open Libnames open Constrexpr diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index ea1808a25..2459a09bc 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - (* Syntax for rewriting with strategies *) open Names diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 index 9864ffeb6..7a75662be 100644 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ b/plugins/ltac/profile_ltac_tactics.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - (** Ltac profiling entrypoints *) open Profile_ltac diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4 index b15dd7ae6..9f1d83f96 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.ml4 @@ -14,8 +14,6 @@ (* *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin open Stdarg open Tacarg diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index 01c3d7940..272d4a20f 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin DECLARE PLUGIN "nsatz_plugin" diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 735af6bab..f7b153a13 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -13,8 +13,6 @@ (* *) (**************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - DECLARE PLUGIN "omega_plugin" diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index f7ebd3204..40897d62f 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin open Names open Misctypes diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 5fd9c9419..5b77d08de 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -6,8 +6,6 @@ *************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - DECLARE PLUGIN "romega_plugin" diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4 index bfa1e5f39..1bfcdc2fb 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.ml4 @@ -7,8 +7,6 @@ (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin DECLARE PLUGIN "rtauto_plugin" diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index a7d6d5bb2..b34d12952 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin open Pp open Util diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 7cdf05117..d25ecee06 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -745,7 +745,7 @@ let discharge_hyp (id', (id, mode)) gl = let cl' = Vars.subst_var id (pf_concl gl) in match pf_get_hyp gl id, mode with | NamedDecl.LocalAssum (_, t), _ | NamedDecl.LocalDef (_, _, t), "(" -> - Proofview.V82.of_tactic (Tactics.apply_type (EConstr.of_constr (mkProd (Name id', t, cl'))) + Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false (EConstr.of_constr (mkProd (Name id', t, cl'))) [EConstr.of_constr (mkVar id)]) gl | NamedDecl.LocalDef (_, v, t), _ -> Proofview.V82.of_tactic @@ -1179,7 +1179,7 @@ let pf_interp_gen_aux ist gl to_ind ((oclr, occ), t) = false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl else CErrors.user_err ?loc:(loc_of_cpattern t) (str "generalized term didn't match") -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type x xs) +let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) let genclrtac cl cs clr = let tclmyORELSE tac1 tac2 gl = diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 4e0b44a44..5782a7621 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -28,7 +28,7 @@ module RelDecl = Context.Rel.Declaration (** The "case" and "elim" tactic *) -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type x xs) +let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) (* TASSI: given the type of an elimination principle, it finds the higher order * argument (index), it computes it's arity and the arity of the eliminator and diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 6032ed2af..11ebe4337 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -382,7 +382,7 @@ let is_construct_ref sigma c r = EConstr.isConstruct sigma c && eq_gr (ConstructRef (fst(EConstr.destConstruct sigma c))) r let is_ind_ref sigma c r = EConstr.isInd sigma c && eq_gr (IndRef (fst(EConstr.destInd sigma c))) r -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type x xs) +let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) let rwcltac cl rdx dir sr gl = let n, r_n,_, ucst = pf_abs_evars gl sr in diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 6c325cce4..b3be31b7b 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -41,7 +41,7 @@ module RelDecl = Context.Rel.Declaration (* They require guessing the view hints and the number of *) (* implicits, respectively, which we do by brute force. *) -let apply_type x xs = Proofview.V82.of_tactic (apply_type x xs) +let apply_type x xs = Proofview.V82.of_tactic (apply_type ~typecheck:false x xs) let new_tac = Proofview.V82.of_tactic diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 5e43c8374..6514b186e 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -122,7 +122,7 @@ let endclausestac id_map clseq gl_id cl0 gl = if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else CErrors.user_err (Pp.str "tampering with discharged assumptions of \"in\" tactical") -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type x xs) +let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) let tclCLAUSES ist tac (gens, clseq) gl = if clseq = InGoal || clseq = InSeqGoal then tac gl else diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index d6dbad7a9..7d0584a00 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -12,9 +12,6 @@ * we thus save the lexer to restore it at the end of the file *) let frozen_lexer = CLexer.get_keyword_state () ;; -(*i camlp4use: "pa_extend.cmo" i*) -(*i camlp4deps: "grammar/grammar.cma" i*) - open Ltac_plugin open Names open Pp diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 754e88139..18ecbf8ed 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -451,17 +451,15 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl = then Anonymous, None, None else - match Option.map detype p with - | None -> Anonymous, None, None - | Some p -> - let nl,typ = it_destRLambda_or_LetIn_names k p in - let n,typ = match DAst.get typ with - | GLambda (x,_,t,c) -> x, c - | _ -> Anonymous, typ in - let aliastyp = - if List.for_all (Name.equal Anonymous) nl then None - else Some (Loc.tag (indsp,nl)) in - n, aliastyp, Some typ + let p = detype p in + let nl,typ = it_destRLambda_or_LetIn_names k p in + let n,typ = match DAst.get typ with + | GLambda (x,_,t,c) -> x, c + | _ -> Anonymous, typ in + let aliastyp = + if List.for_all (Name.equal Anonymous) nl then None + else Some (Loc.tag (indsp,nl)) in + n, aliastyp, Some typ in let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in let tag = @@ -650,7 +648,7 @@ and detype_r d flags avoid env sigma t = (is_nondep_branch sigma) avoid (ci.ci_ind,ci.ci_pp_info.style, ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags) - (Some p) c bl + p c bl | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index a0a8276c5..a4097237f 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -159,34 +159,21 @@ and infer_vect infos variances v = let infer_term cv_pb env variances c = let open CClosure in - let reds = RedFlags.red_add_transparent betaiotazeta Names.full_transparent_state in - let infos = create_clos_infos reds env in + let infos = create_clos_infos all env in infer_fterm cv_pb infos variances (CClosure.inject c) [] -let infer_arity_constructor env variances arcn is_arity params = - let numchecked = ref 0 in - let numparams = Context.Rel.nhyps params in - let basic_check env variances tp = - let variances = - if !numchecked >= numparams then - infer_term CUMUL env variances tp - else - variances - in - numchecked := !numchecked + 1; variances - in +let infer_arity_constructor is_arity env variances arcn = let infer_typ typ (env,variances) = match typ with | Context.Rel.Declaration.LocalAssum (_, typ') -> - (Environ.push_rel typ env, basic_check env variances typ') + (Environ.push_rel typ env, infer_term CUMUL env variances typ') | Context.Rel.Declaration.LocalDef _ -> assert false in - let arcn' = Term.it_mkProd_or_LetIn arcn params in - let typs, codom = Reduction.dest_prod env arcn' in + let typs, codom = Reduction.dest_prod env arcn in let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j} i is irrelevant, j is invariant. *) - if not is_arity then basic_check env variances codom else variances + if not is_arity then infer_term CUMUL env variances codom else variances let infer_inductive env mie = let open Entries in @@ -205,15 +192,12 @@ let infer_inductive env mie = Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances) LMap.empty uarray in + let env, _ = Typeops.infer_local_decls env params in let variances = List.fold_left (fun variances entry -> - let _, params = Typeops.infer_local_decls env params in - let variances = infer_arity_constructor - env variances entry.mind_entry_arity true params + let variances = infer_arity_constructor true + env variances entry.mind_entry_arity in - List.fold_left - (fun variances cons -> - infer_arity_constructor - env variances cons false params) + List.fold_left (infer_arity_constructor false env) variances entry.mind_entry_lc) variances entries diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9fded04db..d5160fc9a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2157,11 +2157,11 @@ let keep hyps = and [a1..an:A1..An(a1..an-1)] such that the goal is [G(a1..an)], this generalizes [hyps |- goal] into [hyps |- T] *) -let apply_type newcl args = +let apply_type ~typecheck newcl args = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in - Refine.refine ~typecheck:false begin fun sigma -> + Refine.refine ~typecheck begin fun sigma -> let newcl = nf_betaiota env sigma newcl (* As in former Logic.refine *) in let (sigma, ev) = Evarutil.new_evar env sigma ~principal:true ~store newcl in @@ -2893,7 +2893,7 @@ let generalize_dep ?(with_let=false) c = let args = Context.Named.to_instance mkVar to_quantify_rev in tclTHENLIST [ Proofview.Unsafe.tclEVARS evd; - apply_type cl'' (if Option.is_empty body then c::args else args); + apply_type ~typecheck:false cl'' (if Option.is_empty body then c::args else args); clear (List.rev tothin')] end @@ -2907,7 +2907,7 @@ let generalize_gen_let lconstr = Proofview.Goal.enter begin fun gl -> let (evd, _) = Typing.type_of env evd newcl in let map ((_, c, b),_) = if Option.is_empty b then Some c else None in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd) - (apply_type newcl (List.map_filter map lconstr)) + (apply_type ~typecheck:false newcl (List.map_filter map lconstr)) end let new_generalize_gen_let lconstr = @@ -4282,7 +4282,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ (if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn) (Tacticals.New.tclTHENLIST [ (* Generalize dependent hyps (but not args) *) - if deps = [] then Proofview.tclUNIT () else apply_type tmpcl deps_cstr; + if deps = [] then Proofview.tclUNIT () else apply_type ~typecheck:false tmpcl deps_cstr; (* side-conditions in elim (resp case) schemes come last (resp first) *) induct_tac elim; Tacticals.New.tclMAP expand_hyp toclear; diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 83fc655f1..ca8e0f20c 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -185,7 +185,7 @@ val revert : Id.t list -> unit Proofview.tactic (** {6 Resolution tactics. } *) -val apply_type : constr -> constr list -> unit Proofview.tactic +val apply_type : typecheck:bool -> constr -> constr list -> unit Proofview.tactic val bring_hyps : named_context -> unit Proofview.tactic val apply : constr -> unit Proofview.tactic diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index 1fb3abfe4..e05762477 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -124,3 +124,13 @@ Inductive Mut1 A := with Mut2 A := | Base2 : Type -> Mut2 A | Node2 : Mut1 A -> Mut2 A. + +(* If we don't reduce T while inferring cumulativity for the + constructor we will see a Rel and believe i is irrelevant. *) +Inductive withparams@{i j} (T:=Type@{i}:Type@{j}) := mkwithparams : T -> withparams. + +Definition withparams_co@{i i' j|i < i', i' < j} : withparams@{i j} -> withparams@{i' j} + := fun x => x. + +Fail Definition withparams_not_irr@{i i' j|i' < i, i' < j} : withparams@{i j} -> withparams@{i' j} + := fun x => x. diff --git a/theories/.dir-locals.el b/theories/.dir-locals.el deleted file mode 100644 index 4e8830f6c..000000000 --- a/theories/.dir-locals.el +++ /dev/null @@ -1,4 +0,0 @@ -((coq-mode . ((eval . (let ((default-directory (locate-dominating-file - buffer-file-name ".dir-locals.el"))) - (setq-local coq-prog-args `("-coqlib" ,(expand-file-name "..") "-R" ,(expand-file-name ".") "Coq")) - (setq-local coq-prog-name (expand-file-name "../bin/coqtop"))))))) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 23212ef84..727fd3ec3 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -34,11 +34,10 @@ LOCAL := $(COQMF_LOCAL) COQLIB := $(COQMF_COQLIB) DOCDIR := $(COQMF_DOCDIR) OCAMLFIND := $(COQMF_OCAMLFIND) -CAMLP4 := $(COQMF_CAMLP4) -CAMLP4O := $(COQMF_CAMLP4O) -CAMLP4BIN := $(COQMF_CAMLP4BIN) -CAMLP4LIB := $(COQMF_CAMLP4LIB) -CAMLP4OPTIONS := $(COQMF_CAMLP4OPTIONS) +CAMLP5O := $(COQMF_CAMLP5O) +CAMLP5BIN := $(COQMF_CAMLP5BIN) +CAMLP5LIB := $(COQMF_CAMLP5LIB) +CAMLP5OPTIONS := $(COQMF_CAMLP5OPTIONS) CAMLFLAGS := $(COQMF_CAMLFLAGS) HASNATDYNLINK := $(COQMF_HASNATDYNLINK) @@ -179,24 +178,20 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") -CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) +CAMLFLAGS+=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP5LIB) # ocamldoc fails with unknown argument otherwise CAMLDOCFLAGS=$(filter-out -annot, $(filter-out -bin-annot, $(CAMLFLAGS))) # FIXME This should be generated by Coq GRAMMARS:=grammar.cma -ifeq ($(CAMLP4),camlp5) -CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo -else -CAMLP4EXTEND= -endif +CAMLP5EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib 2> /dev/null) ifeq (,$(CAMLLIB)) PP=$(error "Cannot find the 'ocamlfind' binary used to build Coq ($(OCAMLFIND)). Pre-compiled binary packages of Coq do not support compiling plugins this way. Please download the sources of Coq and run the Windows build script.") else -PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' +PP:=-pp '$(CAMLP5O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP5EXTEND) $(GRAMMARS) $(CAMLP5OPTIONS) -impl' endif ifneq (,$(TIMING)) @@ -752,11 +747,10 @@ printenv:: @echo 'COQLIB = $(COQLIB)' @echo 'DOCDIR = $(DOCDIR)' @echo 'OCAMLFIND = $(OCAMLFIND)' - @echo 'CAMLP4 = $(CAMLP4)' - @echo 'CAMLP4O = $(CAMLP4O)' - @echo 'CAMLP4BIN = $(CAMLP4BIN)' - @echo 'CAMLP4LIB = $(CAMLP4LIB)' - @echo 'CAMLP4OPTIONS = $(CAMLP4OPTIONS)' + @echo 'CAMLP5O = $(CAMLP5O)' + @echo 'CAMLP5BIN = $(CAMLP5BIN)' + @echo 'CAMLP5LIB = $(CAMLP5LIB)' + @echo 'CAMLP5OPTIONS = $(CAMLP5OPTIONS)' @echo 'HASNATDYNLINK = $(HASNATDYNLINK)' @echo 'SRC_SUBDIRS = $(SRC_SUBDIRS)' @echo 'COQ_SRC_SUBDIRS = $(COQ_SRC_SUBDIRS)' diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 1bb9e0da1..3be357598 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -606,8 +606,8 @@ let distribute a ll = List.map (fun l -> a @ l) ll t;sep;t;...;t;sep;t;...;t;sep;t;LIST1(t,sep) *) let expand_list_rule typ tkl x n p ll = - let camlp4_message_name = Some (add_suffix x ("_"^string_of_int n)) in - let main = GramConstrNonTerminal (ETConstr typ, camlp4_message_name) in + let camlp5_message_name = Some (add_suffix x ("_"^string_of_int n)) in + let main = GramConstrNonTerminal (ETConstr typ, camlp5_message_name) in let tks = List.map (fun x -> GramConstrTerminal x) tkl in let rec aux i hds ll = if i < p then aux (i+1) (main :: tks @ hds) ll diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index b3049f1b7..e064b570e 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -51,7 +51,7 @@ val add_syntax_extension : val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr -> bool -> Flags.compat_version option -> unit -(** Print the Camlp4 state of a grammar *) +(** Print the Camlp5 state of a grammar *) val pr_grammar : string -> Pp.t |