diff options
108 files changed, 1059 insertions, 2915 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index eb2797101..192a2b181 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -137,8 +137,7 @@ /plugins/derive/ @aspiwack # Secondary maintainer @ppedrot -/plugins/extraction/ @letouzey -# Secondary maintainer @maximedenes +/plugins/extraction/ @maximedenes /plugins/firstorder/ @PierreCorbineau # Secondary maintainer @herbelin @@ -159,10 +158,6 @@ /plugins/nsatz/ @thery # Secondary maintainer @ppedrot -/plugins/omega/ @letouzey - -/plugins/romega/ @letouzey - /plugins/setoid_ring/ @amahboubi # Secondary maintainer @bgregoir @@ -219,44 +214,34 @@ ########## Standard library ########## -/theories/Arith/ @letouzey -# Secondary maintainer @herbelin +/theories/Arith/ @herbelin -/theories/Bool/ @letouzey -# Secondary maintainer @herbelin +/theories/Bool/ @herbelin /theories/Classes/ @mattam82 # Secondary maintainer @herbelin -/theories/FSets/ @letouzey -# Secondary maintainer @herbelin +/theories/FSets/ @herbelin -/theories/Init/ @letouzey -# Secondary maintainer @ppedrot +/theories/Init/ @ppedrot -/theories/Lists/ @letouzey -# Secondary maintainer @ppedrot +/theories/Lists/ @ppedrot /theories/Logic/ @herbelin # Secondary maintainer @ppedrot -/theories/MSets/ @letouzey -# Secondary maintainer @herbelin +/theories/MSets/ @herbelin -/theories/NArith/ @letouzey -# Secondary maintainer @herbelin +/theories/NArith/ @herbelin -/theories/Numbers/ @letouzey -# Secondary maintainer @herbelin +/theories/Numbers/ @herbelin -/theories/PArith/ @letouzey -# Secondary maintainer @herbelin +/theories/PArith/ @herbelin /theories/Program/ @mattam82 # Secondary maintainer @herbelin -/theories/QArith/ @letouzey -# Secondary maintainer @herbelin +/theories/QArith/ @herbelin /theories/Reals/ @silene # Secondary maintainer @ppedrot @@ -267,26 +252,19 @@ /theories/Setoids/ @mattam82 # Secondary maintainer @ppedrot -/theories/Sets/ @letouzey -# Secondary maintainer @herbelin +/theories/Sets/ @herbelin -/theories/Sorting/ @letouzey -# Secondary maintainer @herbelin +/theories/Sorting/ @herbelin -/theories/Strings/ @letouzey -# Secondary maintainer @herbelin +/theories/Strings/ @herbelin -/theories/Structures/ @letouzey -# Secondary maintainer @herbelin +/theories/Structures/ @herbelin -/theories/Unicode/ @letouzey -# Secondary maintainer @herbelin +/theories/Unicode/ @herbelin -/theories/Wellfounded/ @letouzey -# Secondary maintainer @mattam82 +/theories/Wellfounded/ @mattam82 -/theories/ZArith/ @letouzey -# Secondary maintainer @herbelin +/theories/ZArith/ @herbelin /theories/Compat/ @JasonGross # Secondary maintainer @Zimmi48 @@ -331,14 +309,11 @@ ########## Build system ########## -/Makefile* @letouzey -# Secondary maintainer @gares +/Makefile* @gares -/configure* @letouzey -# Secondary maintainer @ejgallego +/configure* @ejgallego /META.coq @ejgallego -# Secondary maintainer @letouzey /dev/build/windows @MSoegtropIMC # Secondary maintainer @maximedenes diff --git a/.gitignore b/.gitignore index 1eee3f94f..466f4c1a7 100644 --- a/.gitignore +++ b/.gitignore @@ -120,7 +120,6 @@ dev/ocamlweb-doc/lex.ml ide/coq_lex.ml ide/config_lexer.ml ide/utf8_convert.ml -tools/gallina_lexer.ml tools/coqwc.ml tools/coqdep_lexer.ml tools/ocamllibdep.ml diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 8469d6119..11614bc38 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -45,6 +45,9 @@ before_script: - opam list - opam config list +after_script: + - echo "The build completed normally (not a runner failure)." + ################ GITLAB CACHING ###################### # - use artifacts between jobs # ###################################################### @@ -233,6 +236,35 @@ windows32: variables: ARCH: "32" +pkg:nix: + image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git + stage: test + variables: + # By default we use coq.cachix.org as an extra substituter but this can be overridden + EXTRA_SUBSTITUTERS: https://coq.cachix.org + EXTRA_PUBLIC_KEYS: coq.cachix.org-1:Jgt0DwGAUo+wpxCM52k2V+E0hLoOzFPzvg94F65agtI= + # The following variables should not be overridden + GIT_STRATEGY: none + CACHIX_PUBLIC_KEY: cachix.cachix.org-1:eWNHQldwUO7G2VkjpnjDbWwy4KQ/HNxht7H4SSoMckM= + NIXOS_PUBLIC_KEY: cache.nixos.org-1:6NCHdD59X431o0gWypbMrAURkbJ16ZPMQFGspcDShjY= + + dependencies: [] # We don't need to download build artifacts + before_script: [] # We don't want to use the shared 'before_script' + script: + # Use current worktree as tmpdir to allow exporting artifacts in case of failure + - export TMPDIR=$PWD + # Install Cachix as documented at https://github.com/cachix/cachix + - nix-env -if https://github.com/cachix/cachix/tarball/master --substituters https://cachix.cachix.org --trusted-public-keys "$CACHIX_PUBLIC_KEY" + # We build an expression rather than a direct URL to not be dependent on + # the URL location; we are forced to put the public key of cache.nixos.org + # because there is no --extra-trusted-public-key option. + - nix-build -E "import (fetchTarball $CI_PROJECT_URL/-/archive/$CI_COMMIT_SHA.tar.gz) {}" -K --extra-substituters "$EXTRA_SUBSTITUTERS" --trusted-public-keys "$NIXOS_PUBLIC_KEY $EXTRA_PUBLIC_KEYS" | if [ ! -z "$CACHIX_SIGNING_KEY" ]; then cachix push coq; fi + artifacts: + name: "$CI_JOB_NAME.logs" + when: on_failure + paths: + - nix-build-coq.drv-0/*/test-suite/logs + warnings:base: <<: *warnings-template diff --git a/.travis.yml b/.travis.yml index 627334690..42c41249d 100644 --- a/.travis.yml +++ b/.travis.yml @@ -67,9 +67,6 @@ matrix: - TEST_TARGET="validate" COMPILER="${COMPILER_BE}+flambda" CAMLP5_VER="${CAMLP5_VER_BE}" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" FINDLIB_VER="${FINDLIB_VER_BE}" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-bignums" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-color" - if: NOT (type = pull_request) env: @@ -85,9 +82,6 @@ matrix: - TEST_TARGET="ci-equations" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-fcsl-pcm" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-fiat-parsers" - if: NOT (type = pull_request) env: @@ -100,9 +94,6 @@ matrix: - TEST_TARGET="ci-ltac2" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-math-classes" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-mtac2" - if: NOT (type = pull_request) env: @@ -45,6 +45,16 @@ Tools COQFLAGS is now entirely separate from COQLIBS, so in custom Makefiles $(COQFLAGS) should be replaced by $(COQFLAGS) $(COQLIBS). +- Removed the gallina utility (extracts specification from Coq vernacular files). + If you would like to maintain this tool externally, please contact us. + +- Removed the Emacs modes distributed with Coq. You are advised to + use Proof-General <https://proofgeneral.github.io/> (and optionally + Company-Coq <https://github.com/cpitclaudel/company-coq>) instead. + If your use case is not covered by these alternative Emacs modes, + please open an issue. We can help set up external maintenance as part + of Proof-General, or independently as part of coq-community. + Vernacular Commands - Removed deprecated commands Arguments Scope and Implicit Arguments @@ -156,7 +156,10 @@ endif MAKE_OPTS := --warn-undefined-variable --no-builtin-rules -submake: alienclean +bin: + mkdir bin + +submake: alienclean | bin $(MAKE) $(MAKE_OPTS) -f Makefile.build $(MAKECMDGOALS) noconfig: @@ -214,7 +217,7 @@ archclean: clean-ide optclean voclean rm -f $(ALLSTDLIB).* optclean: - rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBIN) + rm -f $(COQTOPEXE) $(CHICKEN) $(TOPBINOPT) rm -f $(TOOLS) $(PRIVATEBINARIES) $(CSDPCERT) find . -name '*.cmx' -o -name '*.cmx[as]' -o -name '*.[soa]' -o -name '*.so' | xargs rm -f diff --git a/Makefile.build b/Makefile.build index c8ab85765..cd145ae64 100644 --- a/Makefile.build +++ b/Makefile.build @@ -212,9 +212,17 @@ DEPFLAGS=$(LOCALINCLUDES)$(if $(filter plugins/%,$@),, -I ide -I ide/protocol) ifeq ($(shell which codesign > /dev/null 2>&1 && echo $(ARCH)),Darwin) LINKMETADATA=$(if $(filter $(PRIVATEBINARIES),$@),,-ccopt "-sectcreate __TEXT __info_plist config/Info-$(notdir $@).plist") CODESIGN=$(if $(filter $(PRIVATEBINARIES),$@),true,codesign -s -) +CODESIGN_HIDE=$(CODESIGN) else LINKMETADATA= CODESIGN=true +CODESIGN_HIDE=$(HIDE)true +endif + +ifeq ($(STRIP),true) +STRIP_HIDE=$(HIDE)true +else +STRIP_HIDE=$(STRIP) endif # Best OCaml compiler, used in a generic way @@ -400,12 +408,12 @@ grammar/%.cmi: grammar/%.mli .PHONY: coqbinaries coqbyte -coqbinaries: $(TOPBIN) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) +coqbinaries: $(TOPBINOPT) $(COQTOPEXE) $(CHICKEN) $(CSDPCERT) $(FAKEIDE) coqbyte: $(TOPBYTE) $(CHICKENBYTE) # Special rule for coqtop, we imitate `ocamlopt` can delete the target # to avoid #7666 -$(COQTOPEXE): $(TOPBIN:.opt=.$(BEST)) +$(COQTOPEXE): $(TOPBINOPT:.opt=.$(BEST)) rm -f $@ && cp $< $@ bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN) @@ -413,8 +421,8 @@ bin/%.opt$(EXE): topbin/%_bin.ml $(LINKCMX) $(LIBCOQRUN) $(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) \ $(SYSMOD) -package camlp5.gramlib \ $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@ - $(STRIP) $@ - $(CODESIGN) $@ + $(STRIP_HIDE) $@ + $(CODESIGN_HIDE) $@ bin/%.byte$(EXE): topbin/%_bin.ml $(LINKCMO) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' @@ -507,14 +515,6 @@ $(COQDEPBYTE): $(COQDEPCMO) $(SHOW)'OCAMLC -o $@' $(HIDE)$(call ocamlbyte, $(SYSMOD)) -$(GALLINA): $(call bestobj, tools/gallina_lexer.cmo tools/gallina.cmo) - $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,) - -$(GALLINABYTE): tools/gallina_lexer.cmo tools/gallina.cmo - $(SHOW)'OCAMLC -o $@' - $(HIDE)$(call ocamlbyte,) - COQMAKEFILECMO:=clib/clib.cma lib/lib.cma tools/coq_makefile.cmo $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO)) diff --git a/Makefile.checker b/Makefile.checker index 0ec565d61..6c19a1a42 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -52,8 +52,8 @@ ifeq ($(BEST),opt) $(CHICKEN): checker/check.cmxa checker/main.mli checker/main.ml $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^ - $(STRIP) $@ - $(CODESIGN) $@ + $(STRIP_HIDE) $@ + $(CODESIGN_HIDE) $@ else $(CHICKEN): $(CHICKENBYTE) cp $< $@ diff --git a/Makefile.common b/Makefile.common index 94b965a7f..96d0d2ed8 100644 --- a/Makefile.common +++ b/Makefile.common @@ -14,8 +14,8 @@ # Executables ########################################################################### -TOPBIN:=$(addsuffix .opt$(EXE), $(addprefix bin/, coqtop coqproofworker coqtacticworker coqqueryworker)) -TOPBYTE:=$(TOPBIN:.opt$(EXE)=.byte$(EXE)) +TOPBINOPT:=$(addsuffix .opt$(EXE), $(addprefix bin/, coqtop coqproofworker coqtacticworker coqqueryworker)) +TOPBYTE:=$(TOPBINOPT:.opt$(EXE)=.byte$(EXE)) COQTOPEXE:=bin/coqtop$(EXE) COQTOPBYTE:=bin/coqtop.byte$(EXE) @@ -24,8 +24,6 @@ COQDEP:=bin/coqdep$(EXE) COQDEPBYTE:=bin/coqdep.byte$(EXE) COQMAKEFILE:=bin/coq_makefile$(EXE) COQMAKEFILEBYTE:=bin/coq_makefile.byte$(EXE) -GALLINA:=bin/gallina$(EXE) -GALLINABYTE:=bin/gallina.byte$(EXE) COQTEX:=bin/coq-tex$(EXE) COQTEXBYTE:=bin/coq-tex.byte$(EXE) COQWC:=bin/coqwc$(EXE) @@ -41,7 +39,7 @@ COQTIME_FILE_MAKER:=tools/TimeFileMaker.py COQMAKE_BOTH_TIME_FILES:=tools/make-both-time-files.py COQMAKE_BOTH_SINGLE_TIMING_FILES:=tools/make-both-single-timing-files.py -TOOLS:=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ +TOOLS:=$(COQDEP) $(COQMAKEFILE) $(COQTEX) $(COQWC) $(COQDOC) $(COQC)\ $(COQWORKMGR) TOOLS_HELPERS:=tools/CoqMakefile.in $(COQMAKE_ONE_TIME_FILE) $(COQTIME_FILE_MAKER)\ $(COQMAKE_BOTH_TIME_FILES) $(COQMAKE_BOTH_SINGLE_TIMING_FILES) diff --git a/Makefile.ide b/Makefile.ide index 6bb0f62f3..cb5596020 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -99,7 +99,7 @@ $(COQIDE): $(LINKIDEOPT) $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \ -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS:.cma=.cmxa) $^ - $(STRIP) $@ + $(STRIP_HIDE) $@ else $(COQIDE): $(COQIDEBYTE) cp $< $@ @@ -149,8 +149,8 @@ $(IDETOP): ide/idetop.ml $(LINKCMX) $(LIBCOQRUN) $(IDETOPCMX) $(HIDE)$(OCAMLOPT) -linkall -linkpkg $(MLINCLUDES) -I ide -I ide/protocol/ \ $(SYSMOD) -package camlp5.gramlib \ $(LINKCMX) $(IDETOPCMX) $(OPTFLAGS) $(LINKMETADATA) $< -o $@ - $(STRIP) $@ - $(CODESIGN) $@ + $(STRIP_HIDE) $@ + $(CODESIGN_HIDE) $@ $(IDETOPBYTE): ide/idetop.ml $(LINKCMO) $(LIBCOQRUN) $(IDETOPCMA) $(SHOW)'COQMKTOP -o $@' @@ -229,7 +229,7 @@ $(COQIDEINAPP): ide/macos_prehook.cmx $(LINKIDEOPT) | $(COQIDEAPP)/Contents $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ \ -linkpkg -package str,unix,dynlink,threads,lablgtk2.sourceview2 $(IDEFLAGS:.cma=.cmxa) $^ - $(STRIP) $@ + $(STRIP_HIDE) $@ $(COQIDEAPP)/Contents/Resources/share: $(COQIDEAPP)/Contents $(MKDIR) $@/coq/ @@ -275,7 +275,7 @@ $(COQIDEAPP)/Contents/Resources:$(COQIDEAPP)/Contents/Resources/etc $(COQIDEAPP) $(INSTALLLIB) ide/MacOS/*.icns $@ $(COQIDEAPP):$(COQIDEAPP)/Contents/Resources - $(CODESIGN) $@ + $(CODESIGN_HIDE) $@ ########################################################################### # CoqIde for Windows special targets diff --git a/Makefile.install b/Makefile.install index 010e35d42..be6fe5493 100644 --- a/Makefile.install +++ b/Makefile.install @@ -43,7 +43,6 @@ FULLCOQLIB=$(COQLIBINSTALL:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLCONFIGDIR=$(CONFIGDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLDATADIR=$(DATADIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLMANDIR=$(MANDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) -FULLEMACSLIB=$(EMACSLIB:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLCOQDOCDIR=$(COQDOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) FULLDOCDIR=$(DOCDIR:"$(OLDROOT)%="$(COQINSTALLPREFIX)%) else @@ -52,14 +51,13 @@ FULLCOQLIB=$(COQLIBINSTALL) FULLCONFIGDIR=$(CONFIGDIR) FULLDATADIR=$(DATADIR) FULLMANDIR=$(MANDIR) -FULLEMACSLIB=$(EMACSLIB) FULLCOQDOCDIR=$(COQDOCDIR) FULLDOCDIR=$(DOCDIR) endif .PHONY: install-coq install-binaries install-byte install-opt .PHONY: install-tools install-library install-devfiles install-merlin -.PHONY: install-coq-info install-coq-manpages install-emacs install-latex +.PHONY: install-coq-info install-coq-manpages install-latex .PHONY: install-meta install-coq: install-binaries install-library install-coq-info install-devfiles @@ -70,7 +68,7 @@ endif install-binaries: install-tools $(MKDIR) $(FULLBINDIR) - $(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBIN) $(FULLBINDIR) + $(INSTALLBIN) $(COQC) $(CHICKEN) $(COQTOPEXE) $(TOPBINOPT) $(FULLBINDIR) install-byte: install-coqide-byte $(MKDIR) $(FULLBINDIR) @@ -136,9 +134,9 @@ endif rm -f $(FULLCOQLIB)/revision -$(INSTALLLIB) revision $(FULLCOQLIB) -install-coq-info: install-coq-manpages install-emacs install-latex +install-coq-info: install-coq-manpages install-latex -MANPAGES:=man/coq-tex.1 man/coqdep.1 man/gallina.1 \ +MANPAGES:=man/coq-tex.1 man/coqdep.1 \ man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \ man/coqwc.1 man/coqdoc.1 man/coqide.1 \ man/coq_makefile.1 man/coqchk.1 @@ -147,10 +145,6 @@ install-coq-manpages: $(MKDIR) $(FULLMANDIR)/man1 $(INSTALLLIB) $(MANPAGES) $(FULLMANDIR)/man1 -install-emacs: - $(MKDIR) $(FULLEMACSLIB) - $(INSTALLLIB) tools/gallina-db.el tools/coq-font-lock.el tools/gallina-syntax.el tools/gallina.el tools/inferior-coq.el $(FULLEMACSLIB) - # command to update TeX' kpathsea database #UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null diff --git a/checker/indtypes.ml b/checker/indtypes.ml index bcb71fe55..8f11e01c3 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -221,7 +221,7 @@ let allowed_sorts issmall isunit s = -let compute_elim_sorts env_ar params mib arity lc = +let compute_elim_sorts env_ar params arity lc = let inst = extended_rel_list 0 params in let env_params = push_rel_context params env_ar in let lc = Array.map @@ -239,7 +239,7 @@ let compute_elim_sorts env_ar params mib arity lc = allowed_sorts small unit s -let typecheck_one_inductive env params mib mip = +let typecheck_one_inductive env params mip = (* mind_typename and mind_consnames not checked *) (* mind_reloc_tbl, mind_nb_constant, mind_nb_args not checked (VM) *) (* mind_arity_ctxt, mind_arity, mind_nrealargs DONE (typecheck_arity) *) @@ -256,7 +256,7 @@ let typecheck_one_inductive env params mib mip = Array.iter2 check_cons_args mip.mind_nf_lc mip.mind_consnrealdecls; (* mind_kelim: checked by positivity criterion ? *) let sorts = - compute_elim_sorts env params mib mip.mind_arity mip.mind_nf_lc in + compute_elim_sorts env params mip.mind_arity mip.mind_nf_lc in let reject_sort s = not (List.mem_f family_equal s sorts) in if List.exists reject_sort mip.mind_kelim then failwith "elimination not allowed"; @@ -355,7 +355,7 @@ let lambda_implicit_lift n a = (* This removes global parameters of the inductive types in lc (for nested inductive types only ) *) -let abstract_mind_lc env ntyps npars lc = +let abstract_mind_lc ntyps npars lc = if npars = 0 then lc else @@ -448,7 +448,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc let auxntyp = mib.mind_ntypes in if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n)); (* The nested inductive type with parameters removed *) - let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in + let auxlcvect = abstract_mind_lc auxntyp auxnpar mip.mind_nf_lc in (* Extends the environment with a variable corresponding to the inductive def *) let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),lpar) in @@ -625,7 +625,7 @@ let check_inductive env kn mib = (* - check arities *) let env_ar = typecheck_arity env0 params mib.mind_packets in (* - check constructor types *) - Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets; + Array.iter (typecheck_one_inductive env_ar params) mib.mind_packets; (* check the inferred subtyping relation *) let () = match mib.mind_universes with diff --git a/checker/inductive.ml b/checker/inductive.ml index b1edec556..d15380643 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -797,7 +797,7 @@ let rec subterm_specif renv stack t = | Lambda (x,a,b) -> assert (l=[]); - let spec,stack' = extract_stack renv a stack in + let spec,stack' = extract_stack stack in subterm_specif (push_var renv (x,a,spec)) stack' b (* Metas and evars are considered OK *) @@ -813,7 +813,7 @@ and stack_element_specif = function |SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h |SArg x -> x -and extract_stack renv a = function +and extract_stack = function | [] -> Lazy.from_val Not_subterm , [] | h::t -> stack_element_specif h, t @@ -845,7 +845,7 @@ let error_illegal_rec_call renv fx (arg_renv,arg) = let error_partial_apply renv fx = raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx)) -let filter_stack_domain env ci p stack = +let filter_stack_domain env p stack = let absctx, ar = dest_lam_assum env p in (* Optimization: if the predicate is not dependent, no restriction is needed and we avoid building the recargs tree. *) @@ -925,7 +925,7 @@ let check_one_fix renv recpos trees def = let case_spec = branches_specif renv (lazy_subterm_specif renv [] c_0) ci in let stack' = push_stack_closures renv l stack in - let stack' = filter_stack_domain renv.env ci p stack' in + let stack' = filter_stack_domain renv.env p stack' in Array.iteri (fun k br' -> let stack_br = push_stack_args case_spec.(k) stack' in check_rec_call renv stack_br br') lrest @@ -968,7 +968,7 @@ let check_one_fix renv recpos trees def = | Lambda (x,a,b) -> assert (l = []); check_rec_call renv [] a ; - let spec, stack' = extract_stack renv a stack in + let spec, stack' = extract_stack stack in check_rec_call (push_var renv (x,a,spec)) stack' b | Prod (x,a,b) -> diff --git a/checker/modops.ml b/checker/modops.ml index c7ad0977a..b92d7bbf1 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -80,7 +80,7 @@ and add_module mb env = let add_module_type mp mtb env = add_module (module_body_of_type mp mtb) env -let strengthen_const mp_from l cb resolver = +let strengthen_const mp_from l cb = match cb.const_body with | Def _ -> cb | _ -> @@ -104,34 +104,34 @@ and strengthen_body : 'a. (_ -> 'a) -> _ -> _ -> 'a generic_module_body -> 'a ge match mb.mod_type with | MoreFunctor _ -> mb | NoFunctor sign -> - let resolve_out,sign_out = strengthen_sig mp_from sign mp_to mb.mod_delta + let resolve_out,sign_out = strengthen_sig mp_from sign mp_to in { mb with mod_expr = mk_expr mp_to; mod_type = NoFunctor sign_out; mod_delta = resolve_out } -and strengthen_sig mp_from sign mp_to resolver = +and strengthen_sig mp_from sign mp_to = match sign with | [] -> empty_delta_resolver,[] | (l,SFBconst cb) :: rest -> - let item' = l,SFBconst (strengthen_const mp_from l cb resolver) in - let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in + let item' = l,SFBconst (strengthen_const mp_from l cb) in + let resolve_out,rest' = strengthen_sig mp_from rest mp_to in resolve_out,item'::rest' | (_,SFBmind _ as item):: rest -> - let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in + let resolve_out,rest' = strengthen_sig mp_from rest mp_to in resolve_out,item::rest' | (l,SFBmodule mb) :: rest -> let mp_from' = MPdot (mp_from,l) in let mp_to' = MPdot(mp_to,l) in let mb_out = strengthen_mod mp_from' mp_to' mb in let item' = l,SFBmodule (mb_out) in - let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in + let resolve_out,rest' = strengthen_sig mp_from rest mp_to in resolve_out (*add_delta_resolver resolve_out mb.mod_delta*), - item':: rest' - | (l,SFBmodtype mty as item) :: rest -> - let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in - resolve_out,item::rest' + item':: rest' + | (_,SFBmodtype _ as item) :: rest -> + let resolve_out,rest' = strengthen_sig mp_from rest mp_to in + resolve_out,item::rest' let strengthen mtb mp = strengthen_body ignore mtb.mod_mp mp mtb diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 6d0d6f6c6..3f7f84470 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -217,7 +217,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= let _ = Array.map2_i check_cons_types mib1.mind_packets mib2.mind_packets in () -let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = +let check_constant env l info1 cb2 spec2 subst1 subst2 = let error () = error_not_match l spec2 in let check_conv f = check_conv_error error f in let check_type env t1 t2 = check_conv conv_leq env t1 t2 in @@ -281,7 +281,7 @@ and check_signatures env mp1 sig1 sig2 subst1 subst2 = let check_one_body (l,spec2) = match spec2 with | SFBconst cb2 -> - check_constant env mp1 l (get_obj mp1 map1 l) + check_constant env l (get_obj mp1 map1 l) cb2 spec2 subst1 subst2 | SFBmind mib2 -> check_inductive env mp1 l (get_obj mp1 map1 l) diff --git a/configure.ml b/configure.ml index c13c5e107..194f47c49 100644 --- a/configure.ml +++ b/configure.ml @@ -18,7 +18,7 @@ let vo_magic = 8891 let state_magic = 58891 let distributed_exec = ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt"; - "coqc";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"] + "coqc";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"coqwc";"csdpcert";"coqdep"] let verbose = ref false (* for debugging this script *) @@ -235,12 +235,6 @@ let get_date () = let short_date, full_date = get_date () - -(** Create the bin/ directory if non-existent *) - -let _ = if not (dir_exists "bin") then Unix.mkdir "bin" 0o755 - - (** * Command-line parsing *) type ide = Opt | Byte | No @@ -256,7 +250,6 @@ type preferences = { datadir : string option; mandir : string option; docdir : string option; - emacslib : string option; coqdocdir : string option; ocamlfindcmd : string option; lablgtkdir : string option; @@ -294,7 +287,6 @@ let default = { datadir = None; mandir = None; docdir = None; - emacslib = None; coqdocdir = None; ocamlfindcmd = None; lablgtkdir = None; @@ -392,8 +384,6 @@ let args_options = Arg.align [ "<dir> Where to install man files"; "-docdir", arg_string_option (fun p docdir -> { p with docdir }), "<dir> Where to install doc files"; - "-emacslib", arg_string_option (fun p emacslib -> { p with emacslib }), - "<dir> Where to install emacs files"; "-coqdocdir", arg_string_option (fun p coqdocdir -> { p with coqdocdir }), "<dir> Where to install Coqdoc style files"; "-ocamlfind", arg_string_option (fun p ocamlfindcmd -> { p with ocamlfindcmd }), @@ -1014,8 +1004,6 @@ let install = [ Relative "man", Relative "share/man", Relative "man"; "DOCDIR", "the Coq documentation", !prefs.docdir, Relative "doc", Relative "share/doc/coq", Relative "doc"; - "EMACSLIB", "the Coq Emacs mode", !prefs.emacslib, - Relative "emacs", Relative "share/emacs/site-lisp", Relative "tools"; "COQDOCDIR", "the Coqdoc LaTeX files", !prefs.coqdocdir, Relative "latex", Relative "share/texmf/tex/latex/misc", Relative "tools/coqdoc"; ] diff --git a/default.nix b/default.nix index a2645f4fc..d9317bcca 100644 --- a/default.nix +++ b/default.nix @@ -9,23 +9,30 @@ # nix-shell supports the --arg option (see Nix doc) that allows you for # instance to do this: -# $ nix-shell --arg ocamlPackages "(import <nixpkgs> {}).ocamlPackages_latest" --arg buildIde false +# $ nix-shell --arg ocamlPackages "(import <nixpkgs> {}).ocaml-ng.ocamlPackages_4_05" --arg buildIde false # You can also compile Coq and "install" it by running: # $ make clean # (only needed if you have left-over compilation files) # $ nix-build # at the root of the Coq repository. # nix-build also supports the --arg option, so you will be able to do: -# $ nix-build --arg doCheck false +# $ nix-build --arg doInstallCheck false # if you want to speed up things by not running the test-suite. # Once the build is finished, you will find, in the current directory, # a symlink to where Coq was installed. -{ pkgs ? (import <nixpkgs> {}) +{ pkgs ? + (import (fetchTarball { + url = "https://github.com/NixOS/nixpkgs/archive/060a98e9f4ad879492e48d63e887b0b6db26299e.tar.gz"; + sha256 = "1lzvp3md0hf6kp2bvc6dbzh40navlyd51qlns9wbkz6lqk3lgf6j"; + }) {}) , ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06 , buildIde ? true , buildDoc ? true -, doCheck ? true +, doInstallCheck ? true +, shell ? false + # We don't use lib.inNixShell because that would also apply + # when in a nix-shell of some package depending on this one. }: with pkgs; @@ -36,64 +43,64 @@ stdenv.mkDerivation rec { name = "coq"; buildInputs = [ - - # Coq dependencies hostname - ] ++ (with ocamlPackages; [ - ocaml - findlib - camlp5_strict - num - - ]) ++ (if buildIde then [ - - # CoqIDE dependencies - ocamlPackages.lablgtk - - ] else []) ++ (if buildDoc then [ - + python2 time # coq-makefile timing tools + ] + ++ (with ocamlPackages; [ ocaml findlib camlp5_strict num ]) + ++ optional buildIde ocamlPackages.lablgtk + ++ optionals buildDoc [ # Sphinx doc dependencies pkgconfig (python3.withPackages (ps: [ ps.sphinx ps.sphinx_rtd_theme ps.pexpect ps.beautifulsoup4 ps.antlr4-python3-runtime ps.sphinxcontrib-bibtex ])) - antlr4 - - ] else []) ++ (if doCheck then - + antlr4 + ] + ++ optionals doInstallCheck ( # Test-suite dependencies # ncurses is required to build an OCaml REPL optional (!versionAtLeast ocaml.version "4.07") ncurses - ++ [ - python - rsync - which - ocamlPackages.ounit - - ] else []) ++ (if lib.inNixShell then [ - ocamlPackages.merlin - ocamlPackages.ocp-indent - ocamlPackages.ocp-index - - # Dependencies of the merging script - jq - curl - git - gnupg - - ] else []); + ++ [ ocamlPackages.ounit rsync which ] + ) + ++ optionals shell ( + [ jq curl git gnupg ] # Dependencies of the merging script + ++ (with ocamlPackages; [ merlin ocp-indent ocp-index ]) # Dev tools + ); src = - if lib.inNixShell then null + if shell then null else with builtins; filterSource - (path: _: !elem (baseNameOf path) [".git" "result" "bin"]) ./.; + (path: _: + !elem (baseNameOf path) [".git" "result" "bin" "_build_ci"]) ./.; prefixKey = "-prefix "; - buildFlags = [ "world" ] ++ optional buildDoc "doc-html"; + buildFlags = [ "world" "byte" ] ++ optional buildDoc "doc-html"; + + installTargets = + [ "install" "install-byte" ] ++ optional buildDoc "install-doc-html"; + + inherit doInstallCheck; + + preInstallCheck = '' + patchShebangs tools/ + patchShebangs test-suite/ + ''; + + installCheckTarget = [ "check" ]; - installTargets = [ "install" ] ++ optional buildDoc "install-doc-html"; + passthru = { inherit ocamlPackages; }; - inherit doCheck; + meta = { + description = "Coq proof assistant"; + longDescription = '' + Coq is a formal proof management system. It provides a formal language + to write mathematical definitions, executable algorithms and theorems + together with an environment for semi-interactive development of + machine-checked proofs. + ''; + homepage = http://coq.inria.fr; + license = licenses.lgpl21; + }; } diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 85df249d3..a68cd0933 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -69,7 +69,7 @@ git_checkout() if [ ! -d .git ] ; then git clone "${_DEPTH[@]}" "${_URL}" . ; fi && \ echo "Checking out ${_DEST}" && \ git fetch "${_URL}" "${_BRANCH}" && \ - git checkout "${_COMMIT}" && \ + git -c advice.detachedHead=false checkout "${_COMMIT}" && \ echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" ) } diff --git a/dev/ci/user-overlays/07746-cleanup-unused-various.sh b/dev/ci/user-overlays/07746-cleanup-unused-various.sh new file mode 100644 index 000000000..8688b0d53 --- /dev/null +++ b/dev/ci/user-overlays/07746-cleanup-unused-various.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "7746" ] || [ "$CI_BRANCH" = "cleanup-unused-various" ]; then + Equations_CI_BRANCH="adapt-unused" + Equations_CI_GITURL="https://github.com/SkySkimmer/Coq-Equations.git" +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 4177513a1..6d5023405 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -95,19 +95,73 @@ Primitive number parsers ### Transitioning away from Camlp5 -In an effort to reduce dependency on Camlp5, the use of Camlp5 GEXTEND macro -is discouraged. Most plugin writers do not need this low-level interface, but -for those who do, the transition path is somewhat straightforward. To convert -a ml4 file containing only standard OCaml with GEXTEND statements, the following -should be enough: -- replace its "ml4" extension with "mlg" -- replace GEXTEND with GRAMMAR EXTEND -- wrap every occurrence of OCaml code into braces { } +In an effort to reduce dependency on camlp5, the use of several grammar macros +is discouraged. Coq is now shipped with its own preprocessor, called coqpp, +which serves the same purpose as camlp5. + +To perform the transition to coqpp macros, one first needs to change the +extension of a macro file from `.ml4` to `.mlg`. Not all camlp5 macros are +handled yet. + +Due to parsing constraints, the syntax of the macros is slightly different, but +updating the source code is mostly a matter of straightforward +search-and-replace. The main differences are summarized below. + +#### OCaml code + +Every piece of toplevel OCaml code needs to be wrapped into braces. For instance, code of the form ``` let myval = 0 +``` +should be turned into +``` +{ +let myval = 0 +} +``` + +#### TACTIC EXTEND + +Steps to perform: +- replace the brackets enclosing OCaml code in actions with braces +- if not there yet, add a leading `|̀ to the first rule + +For instance, code of the form: +``` +TACTIC EXTEND my_tac + [ "tac1" int_or_var(i) tactic(t) ] -> [ mytac1 ist i t ] +| [ "tac2" tactic(t) ] -> [ mytac2 t ] +END +``` +should be turned into +``` +TACTIC EXTEND my_tac +| [ "tac1" int_or_var(i) tactic(t) ] -> { mytac1 ist i t } +| [ "tac2" tactic(t) ] -> { mytac2 t } +END +``` + +#### VERNAC EXTEND + +Not handled yet. + +#### ARGUMENT EXTEND + +Not handled yet. + +#### GEXTEND +Most plugin writers do not need this low-level interface, but for the sake of +completeness we document it. + +Steps to perform are: +- replace GEXTEND with GRAMMAR EXTEND +- wrap every occurrence of OCaml code in actions into braces { } + +For instance, code of the form +``` GEXTEND Gram GLOBAL: my_entry; @@ -119,10 +173,6 @@ END ``` should be turned into ``` -{ -let myval = 0 -} - GRAMMAR EXTEND Gram GLOBAL: my_entry; @@ -133,9 +183,12 @@ my_entry: END ``` -Currently mlg files can only contain GRAMMAR EXTEND statements. They do not -support TACTIC, VERNAC nor ARGUMENT EXTEND. In case you have a file containing -both kinds at the same time, it is recommended splitting it in two. +Caveats: +- No `GLOBAL` entries mean that they are all local, while camlp5 special-cases + this as a shorthand for all global entries. Solution: always define a `GLOBAL` + section. +- No complex patterns allowed in token naming. Solution: match on it inside the + OCaml quotation. ## Changes between Coq 8.7 and Coq 8.8 diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index b35571e9c..48671c03b 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -10,9 +10,9 @@ versions of Proof General. A somewhat out-of-date description of the async state machine is [documented here](https://github.com/ejgallego/jscoq/blob/master/etc/notes/coq-notes.md). -OCaml types for the protocol can be found in the [`ide/interface.mli` file](/ide/interface.mli). +OCaml types for the protocol can be found in the [`ide/protocol/interface.ml` file](/ide/protocol/interface.ml). -Changes to the XML protocol are documented as part of [`dev/doc/changes.txt`](/dev/doc/changes.txt). +Changes to the XML protocol are documented as part of [`dev/doc/changes.md`](/dev/doc/changes.md). * [Commands](#commands) - [About](#command-about) diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index f6bab0267..b01a4ef0f 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -721,67 +721,68 @@ called the *context of parameters*. Furthermore, we must have that each :math:`T` in :math:`(t:T)∈Γ_I` can be written as: :math:`∀Γ_P,∀Γ_{\mathit{Arr}(t)}, S` where :math:`Γ_{\mathit{Arr}(t)}` is called the *Arity* of the inductive type t and :math:`S` is called the sort of the inductive type t (not to be confused with :math:`\Sort` which is the set of sorts). -** Examples** The declaration for parameterized lists is: - -.. math:: - \ind{1}{[\List:\Set→\Set]}{\left[\begin{array}{rcl} - \Nil & : & \forall A:\Set,\List~A \\ - \cons & : & \forall A:\Set, A→ \List~A→ \List~A - \end{array} - \right]} - -which corresponds to the result of the |Coq| declaration: .. example:: - .. coqtop:: in - - Inductive list (A:Set) : Set := - | nil : list A - | cons : A -> list A -> list A. + The declaration for parameterized lists is: -The declaration for a mutual inductive definition of tree and forest -is: + .. math:: + \ind{1}{[\List:\Set→\Set]}{\left[\begin{array}{rcl} + \Nil & : & \forall A:\Set,\List~A \\ + \cons & : & \forall A:\Set, A→ \List~A→ \List~A + \end{array} + \right]} -.. math:: - \ind{~}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} - {\left[\begin{array}{rcl} - \node &:& \forest → \tree\\ - \emptyf &:& \forest\\ - \consf &:& \tree → \forest → \forest\\ - \end{array}\right]} + which corresponds to the result of the |Coq| declaration: -which corresponds to the result of the |Coq| declaration: + .. coqtop:: in + + Inductive list (A:Set) : Set := + | nil : list A + | cons : A -> list A -> list A. .. example:: - .. coqtop:: in + The declaration for a mutual inductive definition of tree and forest + is: - Inductive tree : Set := - | node : forest -> tree - with forest : Set := - | emptyf : forest - | consf : tree -> forest -> forest. + .. math:: + \ind{~}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} + {\left[\begin{array}{rcl} + \node &:& \forest → \tree\\ + \emptyf &:& \forest\\ + \consf &:& \tree → \forest → \forest\\ + \end{array}\right]} -The declaration for a mutual inductive definition of even and odd is: + which corresponds to the result of the |Coq| declaration: -.. math:: - \ind{1}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ - \odd&:&\nat → \Prop \end{array}\right]} - {\left[\begin{array}{rcl} - \evenO &:& \even~0\\ - \evenS &:& \forall n, \odd~n -> \even~(\kw{S}~n)\\ - \oddS &:& \forall n, \even~n -> \odd~(\kw{S}~n) - \end{array}\right]} + .. coqtop:: in -which corresponds to the result of the |Coq| declaration: + Inductive tree : Set := + | node : forest -> tree + with forest : Set := + | emptyf : forest + | consf : tree -> forest -> forest. .. example:: - .. coqtop:: in + The declaration for a mutual inductive definition of even and odd is: + + .. math:: + \ind{1}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ + \odd&:&\nat → \Prop \end{array}\right]} + {\left[\begin{array}{rcl} + \evenO &:& \even~0\\ + \evenS &:& \forall n, \odd~n -> \even~(\kw{S}~n)\\ + \oddS &:& \forall n, \even~n -> \odd~(\kw{S}~n) + \end{array}\right]} + + which corresponds to the result of the |Coq| declaration: - Inductive even : nat -> prop := - | even_O : even 0 - | even_S : forall n, odd n -> even (S n) - with odd : nat -> prop := - | odd_S : forall n, even n -> odd (S n). + .. coqtop:: in + + Inductive even : nat -> prop := + | even_O : even 0 + | even_S : forall n, odd n -> even (S n) + with odd : nat -> prop := + | odd_S : forall n, even n -> odd (S n). @@ -838,8 +839,8 @@ rules, we need a few definitions: Arity of a given sort +++++++++++++++++++++ -A type :math:`T` is an *arity of sort s* if it converts to the sort s or to a -product :math:`∀ x:T,U` with :math:`U` an arity of sort s. +A type :math:`T` is an *arity of sort* :math:`s` if it converts to the sort :math:`s` or to a +product :math:`∀ x:T,U` with :math:`U` an arity of sort :math:`s`. .. example:: @@ -850,7 +851,7 @@ product :math:`∀ x:T,U` with :math:`U` an arity of sort s. Arity +++++ A type :math:`T` is an *arity* if there is a :math:`s∈ \Sort` such that :math:`T` is an arity of -sort s. +sort :math:`s`. .. example:: @@ -921,29 +922,29 @@ condition* for a constant :math:`X` in the following cases: For instance, if one considers the following variant of a tree type branching over the natural numbers: - .. coqtop:: in + .. coqtop:: in - Inductive nattree (A:Type) : Type := - | leaf : nattree A - | node : A -> (nat -> nattree A) -> nattree A. - End TreeExample. - - Then every instantiated constructor of ``nattree A`` satisfies the nested positivity - condition for ``nattree``: + Inductive nattree (A:Type) : Type := + | leaf : nattree A + | node : A -> (nat -> nattree A) -> nattree A. + End TreeExample. + + Then every instantiated constructor of ``nattree A`` satisfies the nested positivity + condition for ``nattree``: - + Type ``nattree A`` of constructor ``leaf`` satisfies the positivity condition for - ``nattree`` because ``nattree`` does not appear in any (real) arguments of the - type of that constructor (primarily because ``nattree`` does not have any (real) - arguments) ... (bullet 1) + + Type ``nattree A`` of constructor ``leaf`` satisfies the positivity condition for + ``nattree`` because ``nattree`` does not appear in any (real) arguments of the + type of that constructor (primarily because ``nattree`` does not have any (real) + arguments) ... (bullet 1) - + Type ``A → (nat → nattree A) → nattree A`` of constructor ``node`` satisfies the - positivity condition for ``nattree`` because: + + Type ``A → (nat → nattree A) → nattree A`` of constructor ``node`` satisfies the + positivity condition for ``nattree`` because: - - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 3) + - ``nattree`` occurs only strictly positively in ``A`` ... (bullet 3) - - ``nattree`` occurs only strictly positively in ``nat → nattree A`` ... (bullet 3 + 2) + - ``nattree`` occurs only strictly positively in ``nat → nattree A`` ... (bullet 3 + 2) - - ``nattree`` satisfies the positivity condition for ``nattree A`` ... (bullet 1) + - ``nattree`` satisfies the positivity condition for ``nattree A`` ... (bullet 1) .. _Correctness-rules: @@ -978,35 +979,33 @@ provided that the following side conditions hold: One can remark that there is a constraint between the sort of the arity of the inductive type and the sort of the type of its constructors which will always be satisfied for the impredicative -sortProp but may fail to define inductive definition on sort Set and +sort :math:`\Prop` but may fail to define inductive definition on sort :math:`\Set` and generate constraints between universes for inductive definitions in the Type hierarchy. -**Examples**. It is well known that the existential quantifier can be encoded as an -inductive definition. The following declaration introduces the second- -order existential quantifier :math:`∃ X.P(X)`. - .. example:: + It is well known that the existential quantifier can be encoded as an + inductive definition. The following declaration introduces the second- + order existential quantifier :math:`∃ X.P(X)`. + .. coqtop:: in - + Inductive exProp (P:Prop->Prop) : Prop := | exP_intro : forall X:Prop, P X -> exProp P. -The same definition on Set is not allowed and fails: + The same definition on :math:`\Set` is not allowed and fails: -.. example:: .. coqtop:: all Fail Inductive exSet (P:Set->Prop) : Set := exS_intro : forall X:Set, P X -> exSet P. -It is possible to declare the same inductive definition in the -universe Type. The exType inductive definition has type -:math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT_intro}` -has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`. + It is possible to declare the same inductive definition in the + universe :math:`\Type`. The :g:`exType` inductive definition has type + :math:`(\Type(i)→\Prop)→\Type(j)` with the constraint that the parameter :math:`X` of :math:`\kw{exT_intro}` + has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`. -.. example:: .. coqtop:: all Inductive exType (P:Type->Prop) : Type := @@ -1019,9 +1018,9 @@ has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`. Template polymorphism +++++++++++++++++++++ -Inductive types declared in Type are polymorphic over their arguments -in Type. If :math:`A` is an arity of some sort and s is a sort, we write :math:`A_{/s}` -for the arity obtained from :math:`A` by replacing its sort with s. +Inductive types declared in :math:`\Type` are polymorphic over their arguments +in :math:`\Type`. If :math:`A` is an arity of some sort and math:`s` is a sort, we write :math:`A_{/s}` +for the arity obtained from :math:`A` by replacing its sort with :math:`s`. Especially, if :math:`A` is well-typed in some global environment and local context, then :math:`A_{/s}` is typable by typability of all products in the Calculus of Inductive Constructions. The following typing rule is @@ -1382,7 +1381,7 @@ this type. [I:Prop|I→ s] A *singleton definition* has only one constructor and all the -arguments of this constructor have type Prop. In that case, there is a +arguments of this constructor have type :math:`\Prop`. In that case, there is a canonical way to interpret the informative extraction on an object in that type, such that the elimination on any sort :math:`s` is legal. Typical examples are the conjunction of non-informative propositions and the @@ -1421,45 +1420,45 @@ corresponding to the :math:`c:C` constructor. We write :math:`\{c\}^P` for :math:`\{c:C\}^P` with :math:`C` the type of :math:`c`. -**Example.** -The following term in concrete syntax:: +.. example:: + The following term in concrete syntax:: - match t as l return P' with - | nil _ => t1 - | cons _ hd tl => t2 - end + match t as l return P' with + | nil _ => t1 + | cons _ hd tl => t2 + end -can be represented in abstract syntax as + can be represented in abstract syntax as -.. math:: - \case(t,P,f 1 | f 2 ) + .. math:: + \case(t,P,f 1 | f 2 ) -where + where -.. math:: - \begin{eqnarray*} - P & = & \lambda~l~.~P^\prime\\ - f_1 & = & t_1\\ - f_2 & = & \lambda~(hd:\nat)~.~\lambda~(tl:\List~\nat)~.~t_2 - \end{eqnarray*} + .. math:: + \begin{eqnarray*} + P & = & \lambda~l~.~P^\prime\\ + f_1 & = & t_1\\ + f_2 & = & \lambda~(hd:\nat)~.~\lambda~(tl:\List~\nat)~.~t_2 + \end{eqnarray*} -According to the definition: + According to the definition: -.. math:: - \{(\kw{nil}~\nat)\}^P ≡ \{(\kw{nil}~\nat) : (\List~\nat)\}^P ≡ (P~(\kw{nil}~\nat)) + .. math:: + \{(\kw{nil}~\nat)\}^P ≡ \{(\kw{nil}~\nat) : (\List~\nat)\}^P ≡ (P~(\kw{nil}~\nat)) -.. math:: - - \begin{array}{rl} - \{(\kw{cons}~\nat)\}^P & ≡\{(\kw{cons}~\nat) : (\nat→\List~\nat→\List~\nat)\}^P \\ - & ≡∀ n:\nat, \{(\kw{cons}~\nat~n) : \List~\nat→\List~\nat)\}^P \\ - & ≡∀ n:\nat, ∀ l:\List~\nat, \{(\kw{cons}~\nat~n~l) : \List~\nat)\}^P \\ - & ≡∀ n:\nat, ∀ l:\List~\nat,(P~(\kw{cons}~\nat~n~l)). - \end{array} + .. math:: + + \begin{array}{rl} + \{(\kw{cons}~\nat)\}^P & ≡\{(\kw{cons}~\nat) : (\nat→\List~\nat→\List~\nat)\}^P \\ + & ≡∀ n:\nat, \{(\kw{cons}~\nat~n) : \List~\nat→\List~\nat)\}^P \\ + & ≡∀ n:\nat, ∀ l:\List~\nat, \{(\kw{cons}~\nat~n~l) : \List~\nat)\}^P \\ + & ≡∀ n:\nat, ∀ l:\List~\nat,(P~(\kw{cons}~\nat~n~l)). + \end{array} -Given some :math:`P` then :math:`\{(\kw{nil}~\nat)\}^P` represents the expected type of :math:`f_1` , -and :math:`\{(\kw{cons}~\nat)\}^P` represents the expected type of :math:`f_2`. + Given some :math:`P` then :math:`\{(\kw{nil}~\nat)\}^P` represents the expected type of :math:`f_1` , + and :math:`\{(\kw{cons}~\nat)\}^P` represents the expected type of :math:`f_2`. .. _Typing-rule: @@ -1819,7 +1818,7 @@ while it will type-check, if one uses instead the `coqtop` ``-impredicative-set`` option.. The major change in the theory concerns the rule for product formation -in the sort Set, which is extended to a domain in any sort: +in the sort :math:`\Set`, which is extended to a domain in any sort: .. inference:: ProdImp @@ -1832,11 +1831,11 @@ in the sort Set, which is extended to a domain in any sort: This extension has consequences on the inductive definitions which are allowed. In the impredicative system, one can build so-called *large inductive definitions* like the example of second-order existential -quantifier (exSet). +quantifier (:g:`exSet`). There should be restrictions on the eliminations which can be performed on such definitions. The eliminations rules in the -impredicative system for sort Set become: +impredicative system for sort :math:`\Set` become: diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 5dba92429..bdaa2aa1a 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -950,71 +950,10 @@ There are options to produce the |Coq| parts in smaller font, italic, between horizontal rules, etc. See the man page of ``coq-tex`` for more details. -|Coq| and GNU Emacs ------------------------ - - -The |Coq| Emacs mode -~~~~~~~~~~~~~~~~~~~~~~~~~ - -|Coq| comes with a Major mode for GNU Emacs, ``gallina.el``. This mode -provides syntax highlighting and also a rudimentary indentation -facility in the style of the ``Caml`` GNU Emacs mode. - -Add the following lines to your ``.emacs`` file: - -:: - - (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) - (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) - - -The |Coq| major mode is triggered by visiting a file with extension ``.v``, -or manually with the command ``M-x coq-mode``. It gives you the correct -syntax table for the |Coq| language, and also a rudimentary indentation -facility: - - -+ pressing ``Tab`` at the beginning of a line indents the line like the - line above; -+ extra tabulations increase the indentation level (by 2 spaces by default); -+ ``M-Tab`` decreases the indentation level. - - -An inferior mode to run |Coq| under Emacs, by Marco Maggesi, is also -included in the distribution, in file ``inferior-coq.el``. Instructions to -use it are contained in this file. - - -Proof-General -~~~~~~~~~~~~~ - -Proof-General is a generic interface for proof assistants based on -Emacs. The main idea is that the |Coq| commands you are editing are sent -to a |Coq| toplevel running behind Emacs and the answers of the system -automatically inserted into other Emacs buffers. Thus you don’t need -to copy-paste the |Coq| material from your files to the |Coq| toplevel or -conversely from the |Coq| toplevel to some files. - -Proof-General is developed and distributed independently of the system -|Coq|. It is freely available at `<https://proofgeneral.github.io/>`_. - - -Module specification --------------------- - -Given a |Coq| vernacular file, the gallina filter extracts its -specification (inductive types declarations, definitions, type of -lemmas and theorems), removing the proofs parts of the file. The |Coq| -file ``file.v`` gives birth to the specification file ``file.g`` (where -the suffix ``.g`` stands for |Gallina|). - -See the man page of ``gallina`` for more details and options. - Man pages --------- -There are man pages for the commands ``coqdep``, ``gallina`` and ``coq-tex``. Man +There are man pages for the commands ``coqdep`` and ``coq-tex``. Man pages are installed at installation time (see installation instructions in file ``INSTALL``, step 6). diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 0c044f20d..b77bf55d8 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -495,12 +495,12 @@ let e_new_type_evar env evdref ?src ?filter ?naming ?principal ?hypnaming rigid evdref := evd; c -let new_Type ?(rigid=Evd.univ_flexible) env evd = +let new_Type ?(rigid=Evd.univ_flexible) evd = let open EConstr in let (evd, s) = new_sort_variable rigid evd in (evd, mkSort s) -let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = +let e_new_Type ?(rigid=Evd.univ_flexible) evdref = let evd', s = new_sort_variable rigid !evdref in evdref := evd'; EConstr.mkSort s diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 135aa73fc..0ad323ac4 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -63,7 +63,7 @@ val new_type_evar : env -> evar_map -> rigid -> evar_map * (constr * Sorts.t) -val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr +val new_Type : ?rigid:rigid -> evar_map -> evar_map * constr (** Polymorphic constants *) @@ -287,7 +287,7 @@ val e_new_type_evar : env -> evar_map ref -> ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t [@@ocaml.deprecated "Use [Evarutil.new_type_evar]"] -val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr +val e_new_Type : ?rigid:rigid -> evar_map ref -> constr [@@ocaml.deprecated "Use [Evarutil.new_Type]"] val e_new_global : evar_map ref -> GlobRef.t -> constr diff --git a/engine/evd.ml b/engine/evd.ml index 761ae7983..d1c7fef73 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -805,8 +805,8 @@ let make_flexible_variable evd ~algebraic u = (* Operations on constants *) (****************************************) -let fresh_sort_in_family ?loc ?(rigid=univ_flexible) env evd s = - with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family env s) +let fresh_sort_in_family ?loc ?(rigid=univ_flexible) evd s = + with_context_set ?loc rigid evd (UnivGen.fresh_sort_in_family s) let fresh_constant_instance ?loc env evd c = with_context_set ?loc univ_flexible evd (UnivGen.fresh_constant_instance env c) @@ -820,8 +820,6 @@ let fresh_constructor_instance ?loc env evd c = let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr = with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr) -let whd_sort_variable evd t = t - let is_sort_variable evd s = UState.is_sort_variable evd.universes s let is_flexible_level evd l = diff --git a/engine/evd.mli b/engine/evd.mli index d638bb2d3..db2bd4eed 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -340,8 +340,6 @@ val shelve_on_future_goals : Evar.t list -> future_goals -> future_goals Evar maps also keep track of the universe constraints defined at a given point. This section defines the relevant manipulation functions. *) -val whd_sort_variable : evar_map -> econstr -> econstr - exception UniversesDiffer val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map @@ -598,7 +596,7 @@ val update_sigma_env : evar_map -> env -> evar_map (** Polymorphic universes *) -val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> env -> evar_map -> Sorts.family -> evar_map * Sorts.t +val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> evar_map -> Sorts.family -> evar_map * Sorts.t val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> Constant.t -> evar_map * pconstant val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor diff --git a/engine/uState.ml b/engine/uState.ml index 81ab3dd66..0791e4c27 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -583,7 +583,7 @@ let refresh_constraints univs (ctx, cstrs) = in ((ctx, cstrs'), univs') let normalize_variables uctx = - let normalized_variables, undef, def, subst = + let normalized_variables, def, subst = UnivSubst.normalize_univ_variables uctx.uctx_univ_variables in let ctx_local = subst_univs_context_with_def def (Univ.make_subst subst) uctx.uctx_local in diff --git a/engine/univGen.ml b/engine/univGen.ml index 796a1bcc1..b07d4848f 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -215,7 +215,7 @@ let type_of_reference env r = let type_of_global t = type_of_reference (Global.env ()) t -let fresh_sort_in_family env = function +let fresh_sort_in_family = function | InProp -> Sorts.prop, ContextSet.empty | InSet -> Sorts.set, ContextSet.empty | InType -> @@ -223,7 +223,7 @@ let fresh_sort_in_family env = function Type (Univ.Universe.make u), ContextSet.singleton u let new_sort_in_family sf = - fst (fresh_sort_in_family (Global.env ()) sf) + fst (fresh_sort_in_family sf) let extend_context (a, ctx) (ctx') = (a, ContextSet.union ctx ctx') diff --git a/engine/univGen.mli b/engine/univGen.mli index 8169dbda4..439424934 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -39,7 +39,7 @@ val fresh_instance_from_context : AUContext.t -> val fresh_instance_from : AUContext.t -> Instance.t option -> Instance.t in_universe_context_set -val fresh_sort_in_family : env -> Sorts.family -> +val fresh_sort_in_family : Sorts.family -> Sorts.t in_universe_context_set val fresh_constant_instance : env -> Constant.t -> pconstant in_universe_context_set diff --git a/engine/univSubst.ml b/engine/univSubst.ml index 6a433d9fb..2f59a3fa8 100644 --- a/engine/univSubst.ml +++ b/engine/univSubst.ml @@ -162,13 +162,13 @@ let subst_opt_univs_constr s = let normalize_univ_variables ctx = let ctx = normalize_opt_subst ctx in - let undef, def, subst = - Univ.LMap.fold (fun u v (undef, def, subst) -> + let def, subst = + Univ.LMap.fold (fun u v (def, subst) -> match v with - | None -> (Univ.LSet.add u undef, def, subst) - | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst)) - ctx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty) - in ctx, undef, def, subst + | None -> (def, subst) + | Some b -> (Univ.LSet.add u def, Univ.LMap.add u b subst)) + ctx (Univ.LSet.empty, Univ.LMap.empty) + in ctx, def, subst let pr_universe_body = function | None -> mt () diff --git a/engine/univSubst.mli b/engine/univSubst.mli index 26e8d1db9..e76d25333 100644 --- a/engine/univSubst.mli +++ b/engine/univSubst.mli @@ -23,7 +23,7 @@ val make_opt_subst : universe_opt_subst -> universe_subst_fn val subst_opt_univs_constr : universe_opt_subst -> constr -> constr val normalize_univ_variables : universe_opt_subst -> - universe_opt_subst * LSet.t * LSet.t * universe_subst + universe_opt_subst * LSet.t * universe_subst val normalize_univ_variable : find:(Level.t -> Universe.t) -> diff --git a/engine/universes.mli b/engine/universes.mli index 29673de1e..ad937471e 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -86,7 +86,7 @@ val fresh_instance_from : AUContext.t -> Instance.t option -> Instance.t in_universe_context_set [@@ocaml.deprecated "Use [UnivGen.fresh_instance_from]"] -val fresh_sort_in_family : env -> Sorts.family -> +val fresh_sort_in_family : Sorts.family -> Sorts.t in_universe_context_set [@@ocaml.deprecated "Use [UnivGen.fresh_sort_in_family]"] @@ -154,7 +154,7 @@ val subst_opt_univs_constr : universe_opt_subst -> constr -> constr [@@ocaml.deprecated "Use [UnivSubst.subst_opt_univs_constr]"] val normalize_univ_variables : universe_opt_subst -> - universe_opt_subst * LSet.t * LSet.t * universe_subst + universe_opt_subst * LSet.t * universe_subst [@@ocaml.deprecated "Use [UnivSubst.normalize_univ_variables]"] val normalize_univ_variable : diff --git a/grammar/coqpp_ast.mli b/grammar/coqpp_ast.mli index 245e530ae..39b4d2ab3 100644 --- a/grammar/coqpp_ast.mli +++ b/grammar/coqpp_ast.mli @@ -13,14 +13,22 @@ type loc = { type code = { code : string } +type user_symbol = +| Ulist1 of user_symbol +| Ulist1sep of user_symbol * string +| Ulist0 of user_symbol +| Ulist0sep of user_symbol * string +| Uopt of user_symbol +| Uentry of string +| Uentryl of string * int + type token_data = | TokNone | TokName of string -| TokNameSep of string * string type ext_token = | ExtTerminal of string -| ExtNonTerminal of string * token_data +| ExtNonTerminal of user_symbol * token_data type tactic_rule = { tac_toks : ext_token list; @@ -70,11 +78,18 @@ type grammar_ext = { gramext_entries : grammar_entry list; } +type tactic_ext = { + tacext_name : string; + tacext_level : int option; + tacext_rules : tactic_rule list; +} + type node = | Code of code | Comment of string +| DeclarePlugin of string | GramExt of grammar_ext | VernacExt -| TacticExt of string * tactic_rule list +| TacticExt of tactic_ext type t = node list diff --git a/grammar/coqpp_lex.mll b/grammar/coqpp_lex.mll index f35766b16..6c6562c20 100644 --- a/grammar/coqpp_lex.mll +++ b/grammar/coqpp_lex.mll @@ -83,6 +83,7 @@ let alphanum = ['_' 'a'-'z' 'A'-'Z' '0'-'9' '\''] let ident = letterlike alphanum* let qualid = ident ('.' ident)* let space = [' ' '\t' '\r'] +let number = [ '0'-'9' ] rule extend = parse | "(*" { start_comment (); comment lexbuf } @@ -92,6 +93,8 @@ rule extend = parse | "TACTIC" { TACTIC } | "EXTEND" { EXTEND } | "END" { END } +| "DECLARE" { DECLARE } +| "PLUGIN" { PLUGIN } (** Camlp5 specific keywords *) | "GLOBAL" { GLOBAL } | "FIRST" { FIRST } @@ -105,6 +108,7 @@ rule extend = parse (** Standard *) | ident { IDENT (Lexing.lexeme lexbuf) } | qualid { QUALID (Lexing.lexeme lexbuf) } +| number { INT (int_of_string (Lexing.lexeme lexbuf)) } | space { extend lexbuf } | '\"' { string lexbuf } | '\n' { newline lexbuf; extend lexbuf } diff --git a/grammar/coqpp_main.ml b/grammar/coqpp_main.ml index 23a5104e2..e76a1e9ed 100644 --- a/grammar/coqpp_main.ml +++ b/grammar/coqpp_main.ml @@ -55,6 +55,8 @@ let string_split s = in if len == 0 then [] else split 0 +let plugin_name = "__coq_plugin_name" + module GramExt : sig @@ -82,42 +84,42 @@ let get_local_entries ext = in uniquize StringSet.empty local -let print_local chan ext = +let print_local fmt ext = let locals = get_local_entries ext in match locals with | [] -> () | e :: locals -> - let mk_e chan e = fprintf chan "%s.Entry.create \"%s\"" ext.gramext_name e in - let () = fprintf chan "@[<hv 2>let %s =@ @[%a@]@]@ " e mk_e e in - let iter e = fprintf chan "@[<hv 2>and %s =@ @[%a@]@]@ " e mk_e e in + let mk_e fmt e = fprintf fmt "%s.Entry.create \"%s\"" ext.gramext_name e in + let () = fprintf fmt "@[<hv 2>let %s =@ @[%a@]@]@ " e mk_e e in + let iter e = fprintf fmt "@[<hv 2>and %s =@ @[%a@]@]@ " e mk_e e in let () = List.iter iter locals in - fprintf chan "in@ " + fprintf fmt "in@ " -let print_string chan s = fprintf chan "\"%s\"" s +let print_string fmt s = fprintf fmt "\"%s\"" s -let print_list chan pr l = - let rec prl chan = function +let print_list fmt pr l = + let rec prl fmt = function | [] -> () - | [x] -> fprintf chan "%a" pr x - | x :: l -> fprintf chan "%a;@ %a" pr x prl l + | [x] -> fprintf fmt "%a" pr x + | x :: l -> fprintf fmt "%a;@ %a" pr x prl l in - fprintf chan "@[<hv>[%a]@]" prl l + fprintf fmt "@[<hv>[%a]@]" prl l -let print_opt chan pr = function -| None -> fprintf chan "None" -| Some x -> fprintf chan "Some@ (%a)" pr x +let print_opt fmt pr = function +| None -> fprintf fmt "None" +| Some x -> fprintf fmt "Some@ (%a)" pr x -let print_position chan pos = match pos with -| First -> fprintf chan "Extend.First" -| Last -> fprintf chan "Extend.Last" -| Before s -> fprintf chan "Extend.Before@ \"%s\"" s -| After s -> fprintf chan "Extend.After@ \"%s\"" s -| Level s -> fprintf chan "Extend.Level@ \"%s\"" s +let print_position fmt pos = match pos with +| First -> fprintf fmt "Extend.First" +| Last -> fprintf fmt "Extend.Last" +| Before s -> fprintf fmt "Extend.Before@ \"%s\"" s +| After s -> fprintf fmt "Extend.After@ \"%s\"" s +| Level s -> fprintf fmt "Extend.Level@ \"%s\"" s -let print_assoc chan = function -| LeftA -> fprintf chan "Extend.LeftA" -| RightA -> fprintf chan "Extend.RightA" -| NonA -> fprintf chan "Extend.NonA" +let print_assoc fmt = function +| LeftA -> fprintf fmt "Extend.LeftA" +| RightA -> fprintf fmt "Extend.RightA" +| NonA -> fprintf fmt "Extend.NonA" type symb = | SymbToken of string * string option @@ -171,111 +173,166 @@ let rec parse_tokens = function and parse_token tkn = parse_tokens [tkn] -let print_fun chan (vars, body) = +let print_fun fmt (vars, body) = let vars = List.rev vars in let iter = function - | None -> fprintf chan "_@ " - | Some id -> fprintf chan "%s@ " id + | None -> fprintf fmt "_@ " + | Some id -> fprintf fmt "%s@ " id in - let () = fprintf chan "fun@ " in + let () = fprintf fmt "fun@ " in let () = List.iter iter vars in (** FIXME: use Coq locations in the macros *) - let () = fprintf chan "loc ->@ @[%s@]" body.code in + let () = fprintf fmt "loc ->@ @[%s@]" body.code in () (** Meta-program instead of calling Tok.of_pattern here because otherwise violates value restriction *) -let print_tok chan = function -| "", s -> fprintf chan "Tok.KEYWORD %a" print_string s -| "IDENT", s -> fprintf chan "Tok.IDENT %a" print_string s -| "PATTERNIDENT", s -> fprintf chan "Tok.PATTERNIDENT %a" print_string s -| "FIELD", s -> fprintf chan "Tok.FIELD %a" print_string s -| "INT", s -> fprintf chan "Tok.INT %a" print_string s -| "STRING", s -> fprintf chan "Tok.STRING %a" print_string s -| "LEFTQMARK", _ -> fprintf chan "Tok.LEFTQMARK" -| "BULLET", s -> fprintf chan "Tok.BULLET %a" print_string s -| "EOI", _ -> fprintf chan "Tok.EOI" +let print_tok fmt = function +| "", s -> fprintf fmt "Tok.KEYWORD %a" print_string s +| "IDENT", s -> fprintf fmt "Tok.IDENT %a" print_string s +| "PATTERNIDENT", s -> fprintf fmt "Tok.PATTERNIDENT %a" print_string s +| "FIELD", s -> fprintf fmt "Tok.FIELD %a" print_string s +| "INT", s -> fprintf fmt "Tok.INT %a" print_string s +| "STRING", s -> fprintf fmt "Tok.STRING %a" print_string s +| "LEFTQMARK", _ -> fprintf fmt "Tok.LEFTQMARK" +| "BULLET", s -> fprintf fmt "Tok.BULLET %a" print_string s +| "EOI", _ -> fprintf fmt "Tok.EOI" | _ -> failwith "Tok.of_pattern: not a constructor" -let rec print_prod chan p = +let rec print_prod fmt p = let (vars, tkns) = List.split p.gprod_symbs in let f = (vars, p.gprod_body) in let tkn = List.rev_map parse_tokens tkns in - fprintf chan "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun f + fprintf fmt "@[Extend.Rule@ (@[%a@],@ @[(%a)@])@]" print_symbols tkn print_fun f -and print_symbols chan = function -| [] -> fprintf chan "Extend.Stop" +and print_symbols fmt = function +| [] -> fprintf fmt "Extend.Stop" | tkn :: tkns -> - fprintf chan "Extend.Next @[(%a,@ %a)@]" print_symbols tkns print_symbol tkn + fprintf fmt "Extend.Next @[(%a,@ %a)@]" print_symbols tkns print_symbol tkn -and print_symbol chan tkn = match tkn with +and print_symbol fmt tkn = match tkn with | SymbToken (t, s) -> let s = match s with None -> "" | Some s -> s in - fprintf chan "(Extend.Atoken (%a))" print_tok (t, s) + fprintf fmt "(Extend.Atoken (%a))" print_tok (t, s) | SymbEntry (e, None) -> - fprintf chan "(Extend.Aentry %s)" e + fprintf fmt "(Extend.Aentry %s)" e | SymbEntry (e, Some l) -> - fprintf chan "(Extend.Aentryl (%s, %a))" e print_string l + fprintf fmt "(Extend.Aentryl (%s, %a))" e print_string l | SymbSelf -> - fprintf chan "Extend.Aself" + fprintf fmt "Extend.Aself" | SymbNext -> - fprintf chan "Extend.Anext" + fprintf fmt "Extend.Anext" | SymbList0 (s, None) -> - fprintf chan "(Extend.Alist0 %a)" print_symbol s + fprintf fmt "(Extend.Alist0 %a)" print_symbol s | SymbList0 (s, Some sep) -> - fprintf chan "(Extend.Alist0sep (%a, %a))" print_symbol s print_symbol sep + fprintf fmt "(Extend.Alist0sep (%a, %a))" print_symbol s print_symbol sep | SymbList1 (s, None) -> - fprintf chan "(Extend.Alist1 %a)" print_symbol s + fprintf fmt "(Extend.Alist1 %a)" print_symbol s | SymbList1 (s, Some sep) -> - fprintf chan "(Extend.Alist1sep (%a, %a))" print_symbol s print_symbol sep + fprintf fmt "(Extend.Alist1sep (%a, %a))" print_symbol s print_symbol sep | SymbOpt s -> - fprintf chan "(Extend.Aopt %a)" print_symbol s + fprintf fmt "(Extend.Aopt %a)" print_symbol s | SymbRules rules -> - let pr chan (r, body) = + let pr fmt (r, body) = let (vars, tkn) = List.split r in let tkn = List.rev tkn in - fprintf chan "Extend.Rules @[({ Extend.norec_rule = %a },@ (%a))@]" print_symbols tkn print_fun (vars, body) + fprintf fmt "Extend.Rules @[({ Extend.norec_rule = %a },@ (%a))@]" print_symbols tkn print_fun (vars, body) in - let pr chan rules = print_list chan pr rules in - fprintf chan "(Extend.Arules %a)" pr (List.rev rules) - -let print_rule chan r = - let pr_lvl chan lvl = print_opt chan print_string lvl in - let pr_asc chan asc = print_opt chan print_assoc asc in - let pr_prd chan prd = print_list chan print_prod prd in - fprintf chan "@[(%a,@ %a,@ %a)@]" pr_lvl r.grule_label pr_asc r.grule_assoc pr_prd (List.rev r.grule_prods) - -let print_entry chan gram e = - let print_position_opt chan pos = print_opt chan print_position pos in - let print_rules chan rules = print_list chan print_rule rules in - fprintf chan "let () =@ @[%s.safe_extend@ %s@ @[(%a, %a)@]@]@ in@ " + let pr fmt rules = print_list fmt pr rules in + fprintf fmt "(Extend.Arules %a)" pr (List.rev rules) + +let print_rule fmt r = + let pr_lvl fmt lvl = print_opt fmt print_string lvl in + let pr_asc fmt asc = print_opt fmt print_assoc asc in + let pr_prd fmt prd = print_list fmt print_prod prd in + fprintf fmt "@[(%a,@ %a,@ %a)@]" pr_lvl r.grule_label pr_asc r.grule_assoc pr_prd (List.rev r.grule_prods) + +let print_entry fmt gram e = + let print_position_opt fmt pos = print_opt fmt print_position pos in + let print_rules fmt rules = print_list fmt print_rule rules in + fprintf fmt "let () =@ @[%s.gram_extend@ %s@ @[(%a, %a)@]@]@ in@ " gram e.gentry_name print_position_opt e.gentry_pos print_rules e.gentry_rules -let print_ast chan ext = - let () = fprintf chan "let _ = @[" in - let () = fprintf chan "@[<v>%a@]" print_local ext in - let () = List.iter (fun e -> print_entry chan ext.gramext_name e) ext.gramext_entries in - let () = fprintf chan "()@]\n" in +let print_ast fmt ext = + let () = fprintf fmt "let _ = @[" in + let () = fprintf fmt "@[<v>%a@]" print_local ext in + let () = List.iter (fun e -> print_entry fmt ext.gramext_name e) ext.gramext_entries in + let () = fprintf fmt "()@]@\n" in () end -let pr_ast chan = function -| Code s -> fprintf chan "%s@\n" s.code -| Comment s -> fprintf chan "%s@\n" s -| GramExt gram -> fprintf chan "%a@\n" GramExt.print_ast gram -| VernacExt -> fprintf chan "VERNACEXT@\n" -| TacticExt (id, rules) -> - let pr_tok = function - | ExtTerminal s -> Printf.sprintf "%s" s - | ExtNonTerminal (s, _) -> Printf.sprintf "%s" s - in - let pr_tacrule r = - let toks = String.concat " " (List.map pr_tok r.tac_toks) in - Printf.sprintf "[%s] -> {%s}" toks r.tac_body.code +module TacticExt : +sig + +val print_ast : Format.formatter -> tactic_ext -> unit + +end = +struct + +let rec print_symbol fmt = function +| Ulist1 s -> + fprintf fmt "@[Extend.TUlist1 (%a)@]" print_symbol s +| Ulist1sep (s, sep) -> + fprintf fmt "@[Extend.TUlist1sep (%a, \"%s\")@]" print_symbol s sep +| Ulist0 s -> + fprintf fmt "@[Extend.TUlist0 (%a)@]" print_symbol s +| Ulist0sep (s, sep) -> + fprintf fmt "@[Extend.TUlist0sep (%a, \"%s\")@]" print_symbol s sep +| Uopt s -> + fprintf fmt "@[Extend.TUopt (%a)@]" print_symbol s +| Uentry e -> + fprintf fmt "@[Extend.TUentry (Genarg.get_arg_tag wit_%s)@]" e +| Uentryl (e, l) -> + assert (e = "tactic"); + fprintf fmt "@[Extend.TUentryl (Genarg.get_arg_tag wit_%s, %i)@]" e l + +let rec print_clause fmt = function +| [] -> fprintf fmt "@[TyNil@]" +| ExtTerminal s :: cl -> fprintf fmt "@[TyIdent (\"%s\", %a)@]" s print_clause cl +| ExtNonTerminal (g, TokNone) :: cl -> + fprintf fmt "@[TyAnonArg (%a, %a)@]" + print_symbol g print_clause cl +| ExtNonTerminal (g, TokName id) :: cl -> + fprintf fmt "@[TyArg (%a, \"%s\", %a)@]" + print_symbol g id print_clause cl + +let rec print_binders fmt = function +| [] -> fprintf fmt "ist@ " +| (ExtTerminal _ | ExtNonTerminal (_, TokNone)) :: rem -> print_binders fmt rem +| (ExtNonTerminal (_, TokName id)) :: rem -> + fprintf fmt "%s@ %a" id print_binders rem + +let print_rule fmt r = + fprintf fmt "@[TyML (%a, @[fun %a -> %s@])@]" + print_clause r.tac_toks print_binders r.tac_toks r.tac_body.code + +let rec print_rules fmt = function +| [] -> () +| [r] -> fprintf fmt "(%a)@\n" print_rule r +| r :: rem -> fprintf fmt "(%a);@\n%a" print_rule r print_rules rem + +let print_rules fmt rules = + fprintf fmt "Tacentries.([@[<v>%a@]])" print_rules rules + +let print_ast fmt ext = + let pr fmt () = + let level = match ext.tacext_level with None -> 0 | Some i -> i in + fprintf fmt "Tacentries.tactic_extend %s \"%s\" ~level:%i %a" + plugin_name ext.tacext_name level print_rules ext.tacext_rules in - let rules = String.concat ", " (List.map pr_tacrule rules) in - fprintf chan "TACTICEXT (%s, [%s])@\n" id rules + let () = fprintf fmt "let () = @[%a@]\n" pr () in + () + +end + +let pr_ast fmt = function +| Code s -> fprintf fmt "%s@\n" s.code +| Comment s -> fprintf fmt "%s@\n" s +| DeclarePlugin name -> fprintf fmt "let %s = \"%s\"@\n" plugin_name name +| GramExt gram -> fprintf fmt "%a@\n" GramExt.print_ast gram +| VernacExt -> fprintf fmt "VERNACEXT@\n" +| TacticExt tac -> fprintf fmt "%a@\n" TacticExt.print_ast tac let () = let () = diff --git a/grammar/coqpp_parse.mly b/grammar/coqpp_parse.mly index aa22d2717..baafd633c 100644 --- a/grammar/coqpp_parse.mly +++ b/grammar/coqpp_parse.mly @@ -10,13 +10,59 @@ open Coqpp_ast +let starts s pat = + let len = String.length s in + let patlen = String.length pat in + if patlen <= len && String.sub s 0 patlen = pat then + Some (String.sub s patlen (len - patlen)) + else None + +let ends s pat = + let len = String.length s in + let patlen = String.length pat in + if patlen <= len && String.sub s (len - patlen) patlen = pat then + Some (String.sub s 0 (len - patlen)) + else None + +let between s pat1 pat2 = match starts s pat1 with +| None -> None +| Some s -> ends s pat2 + +let without_sep k sep r = + if sep <> "" then raise Parsing.Parse_error else k r + +let parse_user_entry s sep = + let table = [ + "ne_", "_list", without_sep (fun r -> Ulist1 r); + "ne_", "_list_sep", (fun sep r -> Ulist1sep (r, sep)); + "", "_list", without_sep (fun r -> Ulist0 r); + "", "_list_sep", (fun sep r -> Ulist0sep (r, sep)); + "", "_opt", without_sep (fun r -> Uopt r); + ] in + let rec parse s sep = function + | [] -> + let () = without_sep ignore sep () in + begin match starts s "tactic" with + | Some ("0"|"1"|"2"|"3"|"4"|"5") -> Uentryl ("tactic", int_of_string s) + | Some _ | None -> Uentry s + end + | (pat1, pat2, k) :: rem -> + match between s pat1 pat2 with + | None -> parse s sep rem + | Some s -> + let r = parse s "" table in + k sep r + in + parse s sep table + %} %token <Coqpp_ast.code> CODE %token <string> COMMENT %token <string> IDENT QUALID %token <string> STRING -%token VERNAC TACTIC GRAMMAR EXTEND END +%token <int> INT +%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN %token LBRACKET RBRACKET PIPE ARROW COMMA EQUAL %token LPAREN RPAREN COLON SEMICOLON %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA @@ -42,11 +88,16 @@ nodes: node: | CODE { Code $1 } | COMMENT { Comment $1 } +| declare_plugin { $1 } | grammar_extend { $1 } | vernac_extend { $1 } | tactic_extend { $1 } ; +declare_plugin: +| DECLARE PLUGIN STRING { DeclarePlugin $3 } +; + grammar_extend: | GRAMMAR EXTEND qualid_or_ident globals gram_entries END { GramExt { gramext_name = $3; gramext_globals = $4; gramext_entries = $5 } } @@ -57,7 +108,13 @@ vernac_extend: ; tactic_extend: -| TACTIC EXTEND IDENT tactic_rules END { TacticExt ($3, $4) } +| TACTIC EXTEND IDENT tactic_level tactic_rules END + { TacticExt { tacext_name = $3; tacext_level = $4; tacext_rules = $5 } } +; + +tactic_level: +| { None } +| LEVEL INT { Some $2 } ; tactic_rules: @@ -77,9 +134,18 @@ ext_tokens: ext_token: | STRING { ExtTerminal $1 } -| IDENT { ExtNonTerminal ($1, TokNone) } -| IDENT LPAREN IDENT RPAREN { ExtNonTerminal ($1, TokName $3) } -| IDENT LPAREN IDENT COMMA STRING RPAREN { ExtNonTerminal ($1, TokNameSep ($3, $5)) } +| IDENT { + let e = parse_user_entry $1 "" in + ExtNonTerminal (e, TokNone) + } +| IDENT LPAREN IDENT RPAREN { + let e = parse_user_entry $1 "" in + ExtNonTerminal (e, TokName $3) + } +| IDENT LPAREN IDENT COMMA STRING RPAREN { + let e = parse_user_entry $1 $5 in + ExtNonTerminal (e, TokName $3) +} ; qualid_or_ident: diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 525be6432..cea0bed59 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -15,11 +15,6 @@ open Argextend let plugin_name = <:expr< __coq_plugin_name >> -let mlexpr_of_ident id = - (** Workaround for badly-designed generic arguments lacking a closure *) - let id = "$" ^ id in - <:expr< Names.Id.of_string_soft $str:id$ >> - let rec mlexpr_of_symbol = function | Ulist1 s -> <:expr< Extend.TUlist1 $mlexpr_of_symbol s$ >> | Ulist1sep (s,sep) -> <:expr< Extend.TUlist1sep $mlexpr_of_symbol s$ $str:sep$ >> @@ -38,9 +33,9 @@ let rec mlexpr_of_clause = function | [] -> <:expr< TyNil >> | ExtTerminal s :: cl -> <:expr< TyIdent($str:s$, $mlexpr_of_clause cl$) >> | ExtNonTerminal(g,None) :: cl -> - <:expr< TyAnonArg(Loc.tag($mlexpr_of_symbol g$), $mlexpr_of_clause cl$) >> + <:expr< TyAnonArg($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >> | ExtNonTerminal(g,Some id) :: cl -> - <:expr< TyArg(Loc.tag($mlexpr_of_symbol g$, $mlexpr_of_ident id$), $mlexpr_of_clause cl$) >> + <:expr< TyArg($mlexpr_of_symbol g$, $mlexpr_of_string id$, $mlexpr_of_clause cl$) >> let rec binders_of_clause e = function | [] -> <:expr< fun ist -> $e$ >> diff --git a/ide/idetop.ml b/ide/idetop.ml index 7abbf239b..6fb004061 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -151,7 +151,7 @@ let hyp_next_tac sigma env decl = ("inversion clear "^id_s), ("inversion_clear "^id_s^".") ] -let concl_next_tac sigma concl = +let concl_next_tac = let expand s = (s,s^".") in List.map expand ([ "intro"; @@ -230,10 +230,9 @@ let hints () = | [] -> None | g :: _ -> let env = Goal.V82.env sigma g in - let hint_goal = concl_next_tac sigma g in let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in - Some (hint_hyps, hint_goal) + Some (hint_hyps, concl_next_tac) with Proof_global.NoCurrentProof -> None diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 521a7d890..094609b96 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -204,7 +204,7 @@ let lift_univs cb subst auctx0 = let auctx' = Univ.subst_univs_level_abstract_universe_context (Univ.make_instance_subst subst) auctx in subst, (Polymorphic_const (AUContext.union auctx0 auctx')) -let cook_constant ~hcons env { from = cb; info } = +let cook_constant ~hcons { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in let cache = RefTable.create 13 in let abstract, usubst, abs_ctx = abstract in diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 4c254d2ea..6ebe691b8 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -10,7 +10,6 @@ open Constr open Declarations -open Environ (** {6 Cooking the constants. } *) @@ -26,7 +25,7 @@ type result = { cook_context : Constr.named_context option; } -val cook_constant : hcons:bool -> env -> recipe -> result +val cook_constant : hcons:bool -> recipe -> result val cook_constr : Opaqueproof.cooking_info -> constr -> constr (** {6 Utility functions used in module [Discharge]. } *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 61b71df31..5d45c2c1a 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -120,16 +120,6 @@ let mind_check_names mie = (* Typing the arities and constructor types *) -(* An inductive definition is a "unit" if it has only one constructor - and that all arguments expected by this constructor are - logical, this is the case for equality, conjunction of logical properties -*) -let is_unit constrsinfos = - match constrsinfos with (* One info = One constructor *) - | [level] -> is_type0m_univ level - | [] -> (* type without constructors *) true - | _ -> false - let infos_and_sort env t = let rec aux env t max = let t = whd_all env t in @@ -174,10 +164,9 @@ let infer_constructor_packet env_ar_par params lc = let lc'' = Array.map (fun j -> Term.it_mkProd_or_LetIn j.utj_val params) jlc in (* compute the max of the sorts of the products of the constructors types *) let levels = List.map (infos_and_sort env_ar_par) lc in - let isunit = is_unit levels in let min = if Array.length jlc > 1 then Universe.type0 else Universe.type0m in let level = List.fold_left (fun max l -> Universe.sup max l) min levels in - (lc'', (isunit, level)) + (lc'', level) (* If indices matter *) let cumulate_arity_large_levels env sign = @@ -354,7 +343,7 @@ let typecheck_inductive env mie = (* Compute/check the sorts of the inductive types *) let inds = - Array.map (fun ((id,full_arity,sign,expltype,def_level,inf_level),cn,lc,(is_unit,clev)) -> + Array.map (fun ((id,full_arity,sign,expltype,def_level,inf_level),cn,lc,clev) -> let infu = (** Inferred level, with parameters and constructors. *) match inf_level with diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 584c1af03..88b00600e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -785,7 +785,7 @@ let rec subterm_specif renv stack t = | Lambda (x,a,b) -> let () = assert (List.is_empty l) in - let spec,stack' = extract_stack renv a stack in + let spec,stack' = extract_stack stack in subterm_specif (push_var renv (x,a,spec)) stack' b (* Metas and evars are considered OK *) @@ -817,7 +817,7 @@ and stack_element_specif = function |SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h |SArg x -> x -and extract_stack renv a = function +and extract_stack = function | [] -> Lazy.from_val Not_subterm , [] | h::t -> stack_element_specif h, t @@ -848,7 +848,7 @@ let error_illegal_rec_call renv fx (arg_renv,arg) = let error_partial_apply renv fx = raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx)) -let filter_stack_domain env ci p stack = +let filter_stack_domain env p stack = let absctx, ar = dest_lam_assum env p in (* Optimization: if the predicate is not dependent, no restriction is needed and we avoid building the recargs tree. *) @@ -933,7 +933,7 @@ let check_one_fix renv recpos trees def = let case_spec = branches_specif renv (lazy_subterm_specif renv [] c_0) ci in let stack' = push_stack_closures renv l stack in - let stack' = filter_stack_domain renv.env ci p stack' in + let stack' = filter_stack_domain renv.env p stack' in Array.iteri (fun k br' -> let stack_br = push_stack_args case_spec.(k) stack' in check_rec_call renv stack_br br') lrest @@ -976,7 +976,7 @@ let check_one_fix renv recpos trees def = | Lambda (x,a,b) -> let () = assert (List.is_empty l) in check_rec_call renv [] a ; - let spec, stack' = extract_stack renv a stack in + let spec, stack' = extract_stack stack in check_rec_call (push_var renv (x,a,spec)) stack' b | Prod (x,a,b) -> diff --git a/kernel/modops.ml b/kernel/modops.ml index 02bab581a..98a997311 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -265,7 +265,7 @@ let subst_structure subst = subst_structure subst do_delta_codom (* spiwack: here comes the function which takes care of importing the retroknowledge declared in the library *) (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) -let add_retroknowledge mp = +let add_retroknowledge = let perform rkaction env = match rkaction with | Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) -> Environ.register env f e @@ -309,7 +309,7 @@ and add_module mb linkinfo env = let env = Environ.shallow_add_module mb env in match mb.mod_type with |NoFunctor struc -> - add_retroknowledge mp mb.mod_retroknowledge + add_retroknowledge mb.mod_retroknowledge (add_structure mp struc mb.mod_delta linkinfo env) |MoreFunctor _ -> env diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 1748e98a4..39f7de942 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1649,15 +1649,15 @@ let pp_mllam fmt l = and pp_letrec fmt defs = let len = Array.length defs in - let pp_one_rec i (fn, argsn, body) = + let pp_one_rec (fn, argsn, body) = Format.fprintf fmt "%a%a =@\n %a" pp_lname fn pp_ldecls argsn pp_mllam body in Format.fprintf fmt "@[let rec "; - pp_one_rec 0 defs.(0); + pp_one_rec defs.(0); for i = 1 to len - 1 do Format.fprintf fmt "@\nand "; - pp_one_rec i defs.(i) + pp_one_rec defs.(i) done; and pp_blam fmt l = @@ -1941,7 +1941,7 @@ let is_code_loaded ~interactive name = let param_name = Name (Id.of_string "params") let arg_name = Name (Id.of_string "arg") -let compile_mind prefix ~interactive mb mind stack = +let compile_mind mb mind stack = let u = Declareops.inductive_polymorphic_context mb in (** Generate data for every block *) let f i stack ob = @@ -2020,7 +2020,7 @@ let compile_mind_deps env prefix ~interactive then init else let comp_stack = - compile_mind prefix ~interactive mib mind comp_stack + compile_mind mib mind comp_stack in let name = if interactive then LinkedInteractive prefix @@ -2092,9 +2092,9 @@ let compile_constant_field env prefix con acc cb = in gl@acc -let compile_mind_field prefix mp l acc mb = +let compile_mind_field mp l acc mb = let mind = MutInd.make2 mp l in - compile_mind prefix ~interactive:false mb mind acc + compile_mind mb mind acc let mk_open s = Gopen s diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 684983a87..96efa7faa 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -67,7 +67,7 @@ val register_native_file : string -> unit val compile_constant_field : env -> string -> Constant.t -> global list -> constant_body -> global list -val compile_mind_field : string -> ModPath.t -> Label.t -> +val compile_mind_field : ModPath.t -> Label.t -> global list -> mutual_inductive_body -> global list val mk_conv_code : env -> evars -> string -> constr -> constr -> linkable_code diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 8bff43632..edce9367f 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -37,7 +37,7 @@ and translate_field prefix mp env acc (l,x) = let id = mb.mind_packets.(0).mind_typename in let msg = Printf.sprintf "Compiling inductive %s..." (Id.to_string id) in Feedback.msg_debug (Pp.str msg)); - compile_mind_field prefix mp l acc mb + compile_mind_field mp l acc mb | SFBmodule md -> let mp = md.mod_mp in (if !Flags.debug then diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 1e58f5c24..74042f9e0 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -224,7 +224,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 cst -let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = +let check_constant cst env l info1 cb2 spec2 subst1 subst2 = let error why = error_signature_mismatch l spec2 why in let check_conv cst poly f = check_conv_error error cst poly f in let check_type poly cst env t1 t2 = @@ -292,7 +292,7 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= let check_one_body cst (l,spec2) = match spec2 with | SFBconst cb2 -> - check_constant cst env mp1 l (get_obj mp1 map1 l) + check_constant cst env l (get_obj mp1 map1 l) cb2 spec2 subst1 subst2 | SFBmind mib2 -> check_inductive cst env mp1 l (get_obj mp1 map1 l) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index bad449731..1f7ee145a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -378,7 +378,7 @@ let build_constant_declaration kn env result = str "Proof using " ++ declared_vars ++ fnl () ++ str "to" ++ fnl () ++ str "Proof using " ++ inferred_vars) in - let sort evn l = + let sort l = List.filter (fun decl -> let id = NamedDecl.get_id decl in List.exists (NamedDecl.get_id %> Names.Id.equal id) l) @@ -411,7 +411,7 @@ let build_constant_declaration kn env result = [], def (* Empty section context: no need to check *) | Some declared -> (* We use the declared set and chain a check of correctness *) - sort env declared, + sort declared, match def with | Undef _ as x -> x (* nothing to check *) | Def cs as x -> @@ -554,7 +554,7 @@ let translate_recipe env kn r = be useless. It is detected by the dirpath of the constant being empty. *) let (_, dir, _) = Constant.repr3 kn in let hcons = DirPath.is_empty dir in - build_constant_declaration kn env (Cooking.cook_constant ~hcons env r) + build_constant_declaration kn env (Cooking.cook_constant ~hcons r) let translate_local_def env id centry = let open Cooking in diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index fda25a0a6..0cf989e49 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -120,7 +120,7 @@ let uniquize_flags_rev flags = (** [normalize_flags] removes redundant warnings. Unknown warnings are kept because they may be declared in a plugin that will be linked later. *) -let normalize_flags ~silent warnings = +let normalize_flags warnings = let warnings = cut_before_all_rev warnings in uniquize_flags_rev warnings @@ -130,7 +130,7 @@ let normalize_flags_string s = if is_none_keyword s then s else let flags = flags_of_string s in - let flags = normalize_flags ~silent:false flags in + let flags = normalize_flags flags in string_of_flags flags let parse_warnings items = @@ -146,7 +146,7 @@ let parse_flags s = else begin Flags.make_warn true; let flags = flags_of_string s in - let flags = normalize_flags ~silent:true flags in + let flags = normalize_flags flags in parse_warnings flags; string_of_flags flags end diff --git a/lib/util.ml b/lib/util.ml index 7d7d380b2..38d73d345 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -38,8 +38,8 @@ let is_blank = function module Empty = struct - type t - let abort (x : t) = assert false + type t = { abort : 'a. 'a } + let abort (x : t) = x.abort end (* Strings *) diff --git a/library/libobject.ml b/library/libobject.ml index c5cd01525..79a3fed1b 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -98,7 +98,7 @@ let declare_object_full odecl = declare_object_full odecl (* this function describes how the cache, load, open, and export functions are triggered. *) -let apply_dyn_fun deflt f lobj = +let apply_dyn_fun f lobj = let tag = object_tag lobj in let dodecl = try Hashtbl.find cache_tab tag @@ -107,24 +107,24 @@ let apply_dyn_fun deflt f lobj = f dodecl let cache_object ((_,lobj) as node) = - apply_dyn_fun () (fun d -> d.dyn_cache_function node) lobj + apply_dyn_fun (fun d -> d.dyn_cache_function node) lobj let load_object i ((_,lobj) as node) = - apply_dyn_fun () (fun d -> d.dyn_load_function i node) lobj + apply_dyn_fun (fun d -> d.dyn_load_function i node) lobj let open_object i ((_,lobj) as node) = - apply_dyn_fun () (fun d -> d.dyn_open_function i node) lobj + apply_dyn_fun (fun d -> d.dyn_open_function i node) lobj let subst_object ((_,lobj) as node) = - apply_dyn_fun lobj (fun d -> d.dyn_subst_function node) lobj + apply_dyn_fun (fun d -> d.dyn_subst_function node) lobj let classify_object lobj = - apply_dyn_fun Dispose (fun d -> d.dyn_classify_function lobj) lobj + apply_dyn_fun (fun d -> d.dyn_classify_function lobj) lobj let discharge_object ((_,lobj) as node) = - apply_dyn_fun None (fun d -> d.dyn_discharge_function node) lobj + apply_dyn_fun (fun d -> d.dyn_discharge_function node) lobj let rebuild_object lobj = - apply_dyn_fun lobj (fun d -> d.dyn_rebuild_function lobj) lobj + apply_dyn_fun (fun d -> d.dyn_rebuild_function lobj) lobj let dump = Dyn.dump diff --git a/library/library.ml b/library/library.ml index 400f3dcf1..0ff82d7cc 100644 --- a/library/library.ml +++ b/library/library.ml @@ -167,7 +167,7 @@ let opened_libraries () = !libraries_imports_list let register_loaded_library m = let libname = m.libsum_name in - let link m = + let link () = let dirname = Filename.dirname (library_full_filename libname) in let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in let f = prefix ^ "cmo" in @@ -176,7 +176,7 @@ let register_loaded_library m = Nativelib.link_library ~prefix ~dirname ~basename:f in let rec aux = function - | [] -> link m; [libname] + | [] -> link (); [libname] | m'::_ as l when DirPath.equal m' libname -> l | m'::l' -> m' :: aux l' in libraries_loaded_list := aux !libraries_loaded_list; @@ -288,16 +288,15 @@ let locate_absolute_library dir = try let name = Id.to_string base ^ ext in let _, file = System.where_in_path ~warn:false loadpath name in - [file] - with Not_found -> [] in - match find ".vo" @ find ".vio" with - | [] -> raise LibNotFound - | [file] -> file - | [vo;vi] when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + Some file + with Not_found -> None in + match find ".vo", find ".vio" with + | None, None -> raise LibNotFound + | Some file, None | None, Some file -> file + | Some vo, Some vi when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> warn_several_object_files (vi, vo); vi - | [vo;vi] -> vo - | _ -> assert false + | Some vo, Some _ -> vo let locate_qualified_library ?root ?(warn = true) qid = (* Search library in loadpath *) @@ -309,18 +308,17 @@ let locate_qualified_library ?root ?(warn = true) qid = let name = Id.to_string base ^ ext in let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in - [lpath, file] - with Not_found -> [] in + Some (lpath, file) + with Not_found -> None in let lpath, file = - match find ".vo" @ find ".vio" with - | [] -> raise LibNotFound - | [lpath, file] -> lpath, file - | [lpath_vo, vo; lpath_vi, vi] + match find ".vo", find ".vio" with + | None, None -> raise LibNotFound + | Some res, None | None, Some res -> res + | Some (_, vo), Some (_, vi as resvi) when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> warn_several_object_files (vi, vo); - lpath_vi, vi - | [lpath_vo, vo; _ ] -> lpath_vo, vo - | _ -> assert false + resvi + | Some resvo, Some _ -> resvo in let dir = add_dirpath_suffix (String.List.assoc lpath loadpath) base in (* Look if loaded *) diff --git a/man/gallina.1 b/man/gallina.1 deleted file mode 100644 index f8879c457..000000000 --- a/man/gallina.1 +++ /dev/null @@ -1,74 +0,0 @@ -.TH COQ 1 "29 March 1995" "Coq tools" - -.SH NAME -gallina \- extracts specification from Coq vernacular files - -.SH SYNOPSIS -.B gallina -[ -.BI \- -] -[ -.BI \-stdout -] -[ -.BI \-nocomments -] -.I file ... - -.SH DESCRIPTION - -.B gallina -takes Coq files as arguments and builds the corresponding -specification files. -The Coq file -.IR foo.v \& -gives bearth to the specification file -.IR foo.g. \& -The suffix '.g' stands for Gallina. - -For that purpose, gallina removes all commands that follow a -"Theorem", "Lemma", "Fact", "Remark" or "Goal" statement until it -reaches a command "Abort.", "Qed.", "Defined." or "Proof -<...>.". It also removes every "Hint", "Syntax", -"Immediate" or "Transparent" command. - -Files without the .v suffix are ignored. - - -.SH OPTIONS - -.TP -.BI \-stdout -Prints the result on standard output. -.TP -.BI \- -Coq source is taken on standard input. The result is printed on -standard output. -.TP -.BI \-nocomments -Comments are removed in the *.g file. - -.SH NOTES - -Nested comments are correctly handled. In particular, every command -"Qed." or "Abort." in a comment is not taken into account. - - -.SH BUGS - -Please report any bug to -.B coq@pauillac.inria.fr - - - - - - - - - - - - - diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 171276a70..997ea78e6 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -336,7 +336,7 @@ module Gram = I'm not entirely sure it makes sense, but at least it would be more correct. *) G.delete_rule e pil - let safe_extend e ext = grammar_extend e None ext + let gram_extend e ext = grammar_extend e None ext end (** Remove extensions diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 48604e188..154de1221 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -80,7 +80,7 @@ module type S = (* Get comment parsing information from the Lexer *) val comment_state : coq_parsable -> ((int * int) * string) list - val safe_extend : 'a entry -> 'a Extend.extend_statement -> unit + val gram_extend : 'a entry -> 'a Extend.extend_statement -> unit (* Apparently not used *) val srules' : production_rule list -> symbol diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.mlg index 3ae0f45cb..312ef1e55 100644 --- a/plugins/btauto/g_btauto.ml4 +++ b/plugins/btauto/g_btauto.mlg @@ -8,11 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin +} + DECLARE PLUGIN "btauto_plugin" TACTIC EXTEND btauto -| [ "btauto" ] -> [ Refl_btauto.Btauto.tac ] +| [ "btauto" ] -> { Refl_btauto.Btauto.tac } END diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.mlg index fb013ac13..685059294 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.mlg @@ -8,22 +8,26 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin open Cctac open Stdarg +} + DECLARE PLUGIN "cc_plugin" (* Tactic registration *) TACTIC EXTEND cc - [ "congruence" ] -> [ congruence_tac 1000 [] ] - |[ "congruence" integer(n) ] -> [ congruence_tac n [] ] - |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ] +| [ "congruence" ] -> { congruence_tac 1000 [] } +| [ "congruence" integer(n) ] -> { congruence_tac n [] } +| [ "congruence" "with" ne_constr_list(l) ] -> { congruence_tac 1000 l } |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> - [ congruence_tac n l ] + { congruence_tac n l } END TACTIC EXTEND f_equal - [ "f_equal" ] -> [ f_equal ] +| [ "f_equal" ] -> { f_equal } END diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.mlg index 44560ac18..703e29f96 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.mlg @@ -8,11 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin open FourierR +} + DECLARE PLUGIN "fourier_plugin" TACTIC EXTEND fourier - [ "fourierz" ] -> [ fourier () ] +| [ "fourierz" ] -> { fourier () } END diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 31496513a..b2a528a1f 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -322,8 +322,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) try let f = funs.(i) in - let env = Global.env () in - let type_sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd InType in + let type_sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd InType in let new_sorts = match sorts with | None -> Array.make (Array.length funs) (type_sort) @@ -344,7 +343,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) (* let id_of_f = Label.to_id (con_label f) in *) let register_with_sort fam_sort = let evd' = Evd.from_env (Global.env ()) in - let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in + let evd',s = Evd.fresh_sort_in_family evd' fam_sort in let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in @@ -354,7 +353,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) Evd.const_univ_entry ~poly evd' in let ce = Declare.definition_entry ~univs value in - ignore( + ignore( Declare.declare_constant name (DefinitionEntry ce, @@ -508,8 +507,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_ let i = ref (-1) in let sorts = List.rev_map (fun (_,x) -> - Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd x - ) + Evarutil.evd_comb1 Evd.fresh_sort_in_family evd x + ) fas in (* We create the first priciple by tactic *) diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.mlg index 61525cb49..6388906f5 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.mlg @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Util open Locus open Tactypes @@ -18,147 +20,153 @@ open Tacarg open Names open Logic +let wit_hyp = wit_var + +} + DECLARE PLUGIN "ltac_plugin" (** Basic tactics *) TACTIC EXTEND reflexivity - [ "reflexivity" ] -> [ Tactics.intros_reflexivity ] +| [ "reflexivity" ] -> { Tactics.intros_reflexivity } END TACTIC EXTEND exact - [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ] +| [ "exact" casted_constr(c) ] -> { Tactics.exact_no_check c } END TACTIC EXTEND assumption - [ "assumption" ] -> [ Tactics.assumption ] +| [ "assumption" ] -> { Tactics.assumption } END TACTIC EXTEND etransitivity - [ "etransitivity" ] -> [ Tactics.intros_transitivity None ] +| [ "etransitivity" ] -> { Tactics.intros_transitivity None } END TACTIC EXTEND cut - [ "cut" constr(c) ] -> [ Tactics.cut c ] +| [ "cut" constr(c) ] -> { Tactics.cut c } END TACTIC EXTEND exact_no_check - [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ] +| [ "exact_no_check" constr(c) ] -> { Tactics.exact_no_check c } END TACTIC EXTEND vm_cast_no_check - [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ] +| [ "vm_cast_no_check" constr(c) ] -> { Tactics.vm_cast_no_check c } END TACTIC EXTEND native_cast_no_check - [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ] +| [ "native_cast_no_check" constr(c) ] -> { Tactics.native_cast_no_check c } END TACTIC EXTEND casetype - [ "casetype" constr(c) ] -> [ Tactics.case_type c ] +| [ "casetype" constr(c) ] -> { Tactics.case_type c } END TACTIC EXTEND elimtype - [ "elimtype" constr(c) ] -> [ Tactics.elim_type c ] +| [ "elimtype" constr(c) ] -> { Tactics.elim_type c } END TACTIC EXTEND lapply - [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ] +| [ "lapply" constr(c) ] -> { Tactics.cut_and_apply c } END TACTIC EXTEND transitivity - [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some c) ] +| [ "transitivity" constr(c) ] -> { Tactics.intros_transitivity (Some c) } END (** Left *) TACTIC EXTEND left - [ "left" ] -> [ Tactics.left_with_bindings false NoBindings ] +| [ "left" ] -> { Tactics.left_with_bindings false NoBindings } END TACTIC EXTEND eleft - [ "eleft" ] -> [ Tactics.left_with_bindings true NoBindings ] +| [ "eleft" ] -> { Tactics.left_with_bindings true NoBindings } END TACTIC EXTEND left_with - [ "left" "with" bindings(bl) ] -> [ +| [ "left" "with" bindings(bl) ] -> { Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.left_with_bindings false bl) - ] + } END TACTIC EXTEND eleft_with - [ "eleft" "with" bindings(bl) ] -> [ +| [ "eleft" "with" bindings(bl) ] -> { Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.left_with_bindings true bl) - ] + } END (** Right *) TACTIC EXTEND right - [ "right" ] -> [ Tactics.right_with_bindings false NoBindings ] +| [ "right" ] -> { Tactics.right_with_bindings false NoBindings } END TACTIC EXTEND eright - [ "eright" ] -> [ Tactics.right_with_bindings true NoBindings ] +| [ "eright" ] -> { Tactics.right_with_bindings true NoBindings } END TACTIC EXTEND right_with - [ "right" "with" bindings(bl) ] -> [ +| [ "right" "with" bindings(bl) ] -> { Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.right_with_bindings false bl) - ] + } END TACTIC EXTEND eright_with - [ "eright" "with" bindings(bl) ] -> [ +| [ "eright" "with" bindings(bl) ] -> { Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.right_with_bindings true bl) - ] + } END (** Constructor *) TACTIC EXTEND constructor - [ "constructor" ] -> [ Tactics.any_constructor false None ] -| [ "constructor" int_or_var(i) ] -> [ +| [ "constructor" ] -> { Tactics.any_constructor false None } +| [ "constructor" int_or_var(i) ] -> { Tactics.constructor_tac false None i NoBindings - ] -| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> [ + } +| [ "constructor" int_or_var(i) "with" bindings(bl) ] -> { let tac bl = Tactics.constructor_tac false None i bl in Tacticals.New.tclDELAYEDWITHHOLES false bl tac - ] + } END TACTIC EXTEND econstructor - [ "econstructor" ] -> [ Tactics.any_constructor true None ] -| [ "econstructor" int_or_var(i) ] -> [ +| [ "econstructor" ] -> { Tactics.any_constructor true None } +| [ "econstructor" int_or_var(i) ] -> { Tactics.constructor_tac true None i NoBindings - ] -| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> [ + } +| [ "econstructor" int_or_var(i) "with" bindings(bl) ] -> { let tac bl = Tactics.constructor_tac true None i bl in Tacticals.New.tclDELAYEDWITHHOLES true bl tac - ] + } END (** Specialize *) TACTIC EXTEND specialize - [ "specialize" constr_with_bindings(c) ] -> [ +| [ "specialize" constr_with_bindings(c) ] -> { Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c None) - ] -| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> [ + } +| [ "specialize" constr_with_bindings(c) "as" intropattern(ipat) ] -> { Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> Tactics.specialize c (Some ipat)) - ] + } END TACTIC EXTEND symmetry - [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ] +| [ "symmetry" ] -> { Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} } END TACTIC EXTEND symmetry_in -| [ "symmetry" "in" in_clause(cl) ] -> [ Tactics.intros_symmetry cl ] +| [ "symmetry" "in" in_clause(cl) ] -> { Tactics.intros_symmetry cl } END (** Split *) +{ + let rec delayed_list = function | [] -> fun _ sigma -> (sigma, []) | x :: l -> @@ -167,147 +175,159 @@ let rec delayed_list = function let (sigma, l) = delayed_list l env sigma in (sigma, x :: l) +} + TACTIC EXTEND split - [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ] +| [ "split" ] -> { Tactics.split_with_bindings false [NoBindings] } END TACTIC EXTEND esplit - [ "esplit" ] -> [ Tactics.split_with_bindings true [NoBindings] ] +| [ "esplit" ] -> { Tactics.split_with_bindings true [NoBindings] } END TACTIC EXTEND split_with - [ "split" "with" bindings(bl) ] -> [ +| [ "split" "with" bindings(bl) ] -> { Tacticals.New.tclDELAYEDWITHHOLES false bl (fun bl -> Tactics.split_with_bindings false [bl]) - ] + } END TACTIC EXTEND esplit_with - [ "esplit" "with" bindings(bl) ] -> [ +| [ "esplit" "with" bindings(bl) ] -> { Tacticals.New.tclDELAYEDWITHHOLES true bl (fun bl -> Tactics.split_with_bindings true [bl]) - ] + } END TACTIC EXTEND exists - [ "exists" ] -> [ Tactics.split_with_bindings false [NoBindings] ] -| [ "exists" ne_bindings_list_sep(bll, ",") ] -> [ +| [ "exists" ] -> { Tactics.split_with_bindings false [NoBindings] } +| [ "exists" ne_bindings_list_sep(bll, ",") ] -> { Tacticals.New.tclDELAYEDWITHHOLES false (delayed_list bll) (fun bll -> Tactics.split_with_bindings false bll) - ] + } END TACTIC EXTEND eexists - [ "eexists" ] -> [ Tactics.split_with_bindings true [NoBindings] ] -| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> [ +| [ "eexists" ] -> { Tactics.split_with_bindings true [NoBindings] } +| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> { Tacticals.New.tclDELAYEDWITHHOLES true (delayed_list bll) (fun bll -> Tactics.split_with_bindings true bll) - ] + } END (** Intro *) TACTIC EXTEND intros_until - [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ] +| [ "intros" "until" quantified_hypothesis(h) ] -> { Tactics.intros_until h } END TACTIC EXTEND intro -| [ "intro" ] -> [ Tactics.intro_move None MoveLast ] -| [ "intro" ident(id) ] -> [ Tactics.intro_move (Some id) MoveLast ] -| [ "intro" ident(id) "at" "top" ] -> [ Tactics.intro_move (Some id) MoveFirst ] -| [ "intro" ident(id) "at" "bottom" ] -> [ Tactics.intro_move (Some id) MoveLast ] -| [ "intro" ident(id) "after" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveAfter h) ] -| [ "intro" ident(id) "before" hyp(h) ] -> [ Tactics.intro_move (Some id) (MoveBefore h) ] -| [ "intro" "at" "top" ] -> [ Tactics.intro_move None MoveFirst ] -| [ "intro" "at" "bottom" ] -> [ Tactics.intro_move None MoveLast ] -| [ "intro" "after" hyp(h) ] -> [ Tactics.intro_move None (MoveAfter h) ] -| [ "intro" "before" hyp(h) ] -> [ Tactics.intro_move None (MoveBefore h) ] +| [ "intro" ] -> { Tactics.intro_move None MoveLast } +| [ "intro" ident(id) ] -> { Tactics.intro_move (Some id) MoveLast } +| [ "intro" ident(id) "at" "top" ] -> { Tactics.intro_move (Some id) MoveFirst } +| [ "intro" ident(id) "at" "bottom" ] -> { Tactics.intro_move (Some id) MoveLast } +| [ "intro" ident(id) "after" hyp(h) ] -> { Tactics.intro_move (Some id) (MoveAfter h) } +| [ "intro" ident(id) "before" hyp(h) ] -> { Tactics.intro_move (Some id) (MoveBefore h) } +| [ "intro" "at" "top" ] -> { Tactics.intro_move None MoveFirst } +| [ "intro" "at" "bottom" ] -> { Tactics.intro_move None MoveLast } +| [ "intro" "after" hyp(h) ] -> { Tactics.intro_move None (MoveAfter h) } +| [ "intro" "before" hyp(h) ] -> { Tactics.intro_move None (MoveBefore h) } END (** Move *) TACTIC EXTEND move - [ "move" hyp(id) "at" "top" ] -> [ Tactics.move_hyp id MoveFirst ] -| [ "move" hyp(id) "at" "bottom" ] -> [ Tactics.move_hyp id MoveLast ] -| [ "move" hyp(id) "after" hyp(h) ] -> [ Tactics.move_hyp id (MoveAfter h) ] -| [ "move" hyp(id) "before" hyp(h) ] -> [ Tactics.move_hyp id (MoveBefore h) ] +| [ "move" hyp(id) "at" "top" ] -> { Tactics.move_hyp id MoveFirst } +| [ "move" hyp(id) "at" "bottom" ] -> { Tactics.move_hyp id MoveLast } +| [ "move" hyp(id) "after" hyp(h) ] -> { Tactics.move_hyp id (MoveAfter h) } +| [ "move" hyp(id) "before" hyp(h) ] -> { Tactics.move_hyp id (MoveBefore h) } END (** Rename *) TACTIC EXTEND rename -| [ "rename" ne_rename_list_sep(ids, ",") ] -> [ Tactics.rename_hyp ids ] +| [ "rename" ne_rename_list_sep(ids, ",") ] -> { Tactics.rename_hyp ids } END (** Revert *) TACTIC EXTEND revert - [ "revert" ne_hyp_list(hl) ] -> [ Tactics.revert hl ] +| [ "revert" ne_hyp_list(hl) ] -> { Tactics.revert hl } END (** Simple induction / destruct *) +{ + let simple_induct h = Tacticals.New.tclTHEN (Tactics.intros_until h) (Tacticals.New.onLastHyp Tactics.simplest_elim) +} + TACTIC EXTEND simple_induction - [ "simple" "induction" quantified_hypothesis(h) ] -> [ simple_induct h ] +| [ "simple" "induction" quantified_hypothesis(h) ] -> { simple_induct h } END +{ + let simple_destruct h = Tacticals.New.tclTHEN (Tactics.intros_until h) (Tacticals.New.onLastHyp Tactics.simplest_case) +} + TACTIC EXTEND simple_destruct - [ "simple" "destruct" quantified_hypothesis(h) ] -> [ simple_destruct h ] +| [ "simple" "destruct" quantified_hypothesis(h) ] -> { simple_destruct h } END (** Double induction *) TACTIC EXTEND double_induction - [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] -> - [ Elim.h_double_induction h1 h2 ] +| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] -> + { Elim.h_double_induction h1 h2 } END (* Admit *) TACTIC EXTEND admit - [ "admit" ] -> [ Proofview.give_up ] +|[ "admit" ] -> { Proofview.give_up } END (* Fix *) TACTIC EXTEND fix - [ "fix" ident(id) natural(n) ] -> [ Tactics.fix id n ] +| [ "fix" ident(id) natural(n) ] -> { Tactics.fix id n } END (* Cofix *) TACTIC EXTEND cofix - [ "cofix" ident(id) ] -> [ Tactics.cofix id ] +| [ "cofix" ident(id) ] -> { Tactics.cofix id } END (* Clear *) TACTIC EXTEND clear - [ "clear" hyp_list(ids) ] -> [ +| [ "clear" hyp_list(ids) ] -> { if List.is_empty ids then Tactics.keep [] else Tactics.clear ids - ] -| [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ] + } +| [ "clear" "-" ne_hyp_list(ids) ] -> { Tactics.keep ids } END (* Clearbody *) TACTIC EXTEND clearbody - [ "clearbody" ne_hyp_list(ids) ] -> [ Tactics.clear_body ids ] +| [ "clearbody" ne_hyp_list(ids) ] -> { Tactics.clear_body ids } END (* Generalize dependent *) TACTIC EXTEND generalize_dependent - [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ] +| [ "generalize" "dependent" constr(c) ] -> { Tactics.generalize_dep c } END (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) +{ + open Tacexpr let initial_atomic () = @@ -364,3 +384,5 @@ let initial_tacticals () = ] let () = Mltop.declare_cache_obj initial_tacticals "ltac_plugin" + +} diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 660e29ca8..f24ab2bdd 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -293,7 +293,7 @@ open Vars let constr_flags () = { Pretyping.use_typeclasses = true; - Pretyping.solve_unification_constraints = true; + Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics (); Pretyping.use_hook = Pfedit.solve_by_implicit_tactic (); Pretyping.fail_evar = false; Pretyping.expand_evars = true } diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.mlg index 2251a6620..e57afe3e3 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.mlg @@ -14,15 +14,19 @@ (* by Eduardo Gimenez *) (************************************************************************) +{ + open Eqdecide open Stdarg +} + DECLARE PLUGIN "ltac_plugin" TACTIC EXTEND decide_equality -| [ "decide" "equality" ] -> [ decideEqualityGoal ] +| [ "decide" "equality" ] -> { decideEqualityGoal } END TACTIC EXTEND compare -| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ] +| [ "compare" constr(c1) constr(c2) ] -> { compare c1 c2 } END diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 09179dad3..4357689ee 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -115,7 +115,7 @@ let string_of_genarg_arg (ArgumentType arg) = let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) - let has_type (Val.Dyn (tag, x)) t = match Val.eq tag t with + let has_type (Val.Dyn (tag, _)) t = match Val.eq tag t with | None -> false | Some _ -> true @@ -188,7 +188,7 @@ let string_of_genarg_arg (ArgumentType arg) = | AN v -> f v | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc) - let pr_located pr (loc,x) = pr x + let pr_located pr (_,x) = pr x let pr_evaluable_reference = function | EvalVarRef id -> pr_id id @@ -240,7 +240,7 @@ let string_of_genarg_arg (ArgumentType arg) = in pr_sequence (fun x -> x) l - let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l = + let pr_extend_gen pr_gen _ { mltac_name = s; mltac_index = i } l = let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++ str "@" ++ int i @@ -260,7 +260,7 @@ let string_of_genarg_arg (ArgumentType arg) = | Extend.Uentry tag -> let ArgT.Any tag = tag in ArgT.repr tag - | Extend.Uentryl (tkn, lvl) -> "tactic" ^ string_of_int lvl + | Extend.Uentryl (_, lvl) -> "tactic" ^ string_of_int lvl let pr_alias_key key = try @@ -288,7 +288,7 @@ let string_of_genarg_arg (ArgumentType arg) = let p = pr_tacarg_using_rule pr_gen prods in if pp.pptac_level > lev then surround p else p with Not_found -> - let pr arg = str "_" in + let pr _ = str "_" in KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)" let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.tag arg)) @@ -341,14 +341,14 @@ let string_of_genarg_arg (ArgumentType arg) = pr_any_arg pr symb arg | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")" - let pr_raw_extend_rec prc prlc prtac prpat = + let pr_raw_extend_rec prtac = pr_extend_gen (pr_farg prtac) - let pr_glob_extend_rec prc prlc prtac prpat = + let pr_glob_extend_rec prtac = pr_extend_gen (pr_farg prtac) - let pr_raw_alias prc prlc prtac prpat lev key args = + let pr_raw_alias prtac lev key args = pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args - let pr_glob_alias prc prlc prtac prpat lev key args = + let pr_glob_alias prtac lev key args = pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args (**********************************************************************) @@ -743,7 +743,7 @@ let pr_goal_selector ~toplevel s = (* Main tactic printer *) and pr_atom1 a = tag_atom a (match a with (* Basic tactics *) - | TacIntroPattern (ev,[]) as t -> + | TacIntroPattern (_,[]) as t -> pr_atom0 t | TacIntroPattern (ev,(_::_ as p)) -> hov 1 (primitive (if ev then "eintros" else "intros") ++ @@ -1054,7 +1054,7 @@ let pr_goal_selector ~toplevel s = primitive "fresh" ++ pr_fresh_ids l, latom | TacArg(_,TacGeneric arg) -> pr.pr_generic arg, latom - | TacArg(_,TacCall(loc,(f,[]))) -> + | TacArg(_,TacCall(_,(f,[]))) -> pr.pr_reference f, latom | TacArg(_,TacCall(loc,(f,l))) -> pr_with_comments ?loc (hov 1 ( @@ -1112,8 +1112,8 @@ let pr_goal_selector ~toplevel s = pr_reference = pr_qualid; pr_name = pr_lident; pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg); - pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; - pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; + pr_extend = pr_raw_extend_rec pr_raw_tactic_level; + pr_alias = pr_raw_alias pr_raw_tactic_level; } in make_pr_tac pr raw_printers @@ -1142,12 +1142,8 @@ let pr_goal_selector ~toplevel s = pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant); pr_name = pr_lident; pr_generic = (fun arg -> Pputils.pr_glb_generic (Global.env ()) arg); - pr_extend = pr_glob_extend_rec - (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) - prtac (pr_pat_and_constr_expr (pr_glob_constr_env env)); - pr_alias = pr_glob_alias - (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) - prtac (pr_pat_and_constr_expr (pr_glob_constr_env env)); + pr_extend = pr_glob_extend_rec prtac; + pr_alias = pr_glob_alias prtac; } in make_pr_tac pr glob_printers @@ -1168,8 +1164,8 @@ let pr_goal_selector ~toplevel s = | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty - let pr_atomic_tactic_level env sigma n t = - let prtac n (t:atomic_tactic_expr) = + let pr_atomic_tactic_level env sigma t = + let prtac (t:atomic_tactic_expr) = let pr = { pr_tactic = (fun _ _ -> str "<tactic>"); pr_constr = (fun c -> pr_econstr_env env sigma c); @@ -1188,18 +1184,15 @@ let pr_goal_selector ~toplevel s = in pr_atom pr strip_prod_binders_constr tag_atomic_tactic_expr t in - prtac n t + prtac t let pr_raw_generic = Pputils.pr_raw_generic let pr_glb_generic = Pputils.pr_glb_generic - let pr_raw_extend env = pr_raw_extend_rec - pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr + let pr_raw_extend _ = pr_raw_extend_rec pr_raw_tactic_level - let pr_glob_extend env = pr_glob_extend_rec - (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) - (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env)) + let pr_glob_extend env = pr_glob_extend_rec (pr_glob_tactic_level env) let pr_alias pr lev key args = pr_alias_gen (fun _ arg -> pr arg) lev key args @@ -1207,14 +1200,14 @@ let pr_goal_selector ~toplevel s = let pr_extend pr lev ml args = pr_extend_gen pr lev ml args - let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma ltop c + let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma c let declare_extra_genarg_pprule wit (f : 'a raw_extra_genarg_printer) (g : 'b glob_extra_genarg_printer) (h : 'c extra_genarg_printer) = begin match wit with - | ExtraArg s -> () + | ExtraArg _ -> () | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") end; let f x = diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 01c52c413..9f8cd2fc4 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -409,7 +409,7 @@ module TypeGlobal = struct let inverse env (evd,cstrs) car rel = - let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in + let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible evd in app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |] end diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 84baea964..026c00b84 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -165,8 +165,7 @@ let coerce_var_to_ident fresh env sigma v = (* Interprets, if possible, a constr to an identifier which may not be fresh but suitable to be given to the fresh tactic. Works for vars, constants, inductive, constructors and sorts. *) -let coerce_to_ident_not_fresh env sigma v = -let g = sigma in +let coerce_to_ident_not_fresh sigma v = let id_of_name = function | Name.Anonymous -> Id.of_string "x" | Name.Name x -> x in @@ -183,9 +182,9 @@ let id_of_name = function | Some c -> match EConstr.kind sigma c with | Var id -> id - | Meta m -> id_of_name (Evd.meta_name g m) + | Meta m -> id_of_name (Evd.meta_name sigma m) | Evar (kn,_) -> - begin match Evd.evar_ident kn g with + begin match Evd.evar_ident kn sigma with | None -> fail () | Some id -> id end @@ -208,7 +207,7 @@ let id_of_name = function | _ -> fail() -let coerce_to_intro_pattern env sigma v = +let coerce_to_intro_pattern sigma v = if has_type v (topwit wit_intro_pattern) then (out_gen (topwit wit_intro_pattern) v).CAst.v else if has_type v (topwit wit_var) then @@ -221,8 +220,8 @@ let coerce_to_intro_pattern env sigma v = IntroNaming (IntroIdentifier (destVar sigma c)) | _ -> raise (CannotCoerceTo "an introduction pattern") -let coerce_to_intro_pattern_naming env sigma v = - match coerce_to_intro_pattern env sigma v with +let coerce_to_intro_pattern_naming sigma v = + match coerce_to_intro_pattern sigma v with | IntroNaming pat -> pat | _ -> raise (CannotCoerceTo "a naming introduction pattern") @@ -255,7 +254,7 @@ let coerce_to_constr env v = (try [], constr_of_id env id with Not_found -> fail ()) else fail () -let coerce_to_uconstr env v = +let coerce_to_uconstr v = if has_type v (topwit wit_uconstr) then out_gen (topwit wit_uconstr) v else @@ -299,11 +298,11 @@ let coerce_to_constr_list env v = List.map map l | None -> raise (CannotCoerceTo "a term list") -let coerce_to_intro_pattern_list ?loc env sigma v = +let coerce_to_intro_pattern_list ?loc sigma v = match Value.to_list v with | None -> raise (CannotCoerceTo "an intro pattern list") | Some l -> - let map v = CAst.make ?loc @@ coerce_to_intro_pattern env sigma v in + let map v = CAst.make ?loc @@ coerce_to_intro_pattern sigma v in List.map map l let coerce_to_hyp env sigma v = @@ -328,7 +327,7 @@ let coerce_to_hyp_list env sigma v = | None -> raise (CannotCoerceTo "a variable list") (* Interprets a qualified name *) -let coerce_to_reference env sigma v = +let coerce_to_reference sigma v = match Value.to_constr v with | Some c -> begin @@ -356,7 +355,7 @@ let coerce_to_quantified_hypothesis sigma v = (* Quantified named or numbered hypothesis or hypothesis in context *) (* (as in Inversion) *) -let coerce_to_decl_or_quant_hyp env sigma v = +let coerce_to_decl_or_quant_hyp sigma v = if has_type v (topwit wit_int) then AnonHyp (out_gen (topwit wit_int) v) else diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 56f881684..d2ae92f6c 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -51,12 +51,12 @@ val coerce_to_constr_context : Value.t -> constr val coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Id.t -val coerce_to_ident_not_fresh : Environ.env -> Evd.evar_map -> Value.t -> Id.t +val coerce_to_ident_not_fresh : Evd.evar_map -> Value.t -> Id.t -val coerce_to_intro_pattern : Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr +val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr val coerce_to_intro_pattern_naming : - Environ.env -> Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr + Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr val coerce_to_hint_base : Value.t -> string @@ -64,7 +64,7 @@ val coerce_to_int : Value.t -> int val coerce_to_constr : Environ.env -> Value.t -> Ltac_pretype.constr_under_binders -val coerce_to_uconstr : Environ.env -> Value.t -> Ltac_pretype.closed_glob_constr +val coerce_to_uconstr : Value.t -> Ltac_pretype.closed_glob_constr val coerce_to_closed_constr : Environ.env -> Value.t -> constr @@ -74,17 +74,17 @@ val coerce_to_evaluable_ref : val coerce_to_constr_list : Environ.env -> Value.t -> constr list val coerce_to_intro_pattern_list : - ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns + ?loc:Loc.t -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t val coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Id.t list -val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> GlobRef.t +val coerce_to_reference : Evd.evar_map -> Value.t -> GlobRef.t val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypothesis -val coerce_to_decl_or_quant_hyp : Environ.env -> Evd.evar_map -> Value.t -> quantified_hypothesis +val coerce_to_decl_or_quant_hyp : Evd.evar_map -> Value.t -> quantified_hypothesis val coerce_to_int_or_var_list : Value.t -> int Locus.or_var list diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 876e6f320..fac464a62 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -554,13 +554,18 @@ let () = ] in register_grammars_by_name "tactic" entries +let get_identifier id = + (** Workaround for badly-designed generic arguments lacking a closure *) + Names.Id.of_string_soft ("$" ^ id) + + type _ ty_sig = | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig | TyIdent : string * 'r ty_sig -> 'r ty_sig | TyArg : - (('a, 'b, 'c) Extend.ty_user_symbol * Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig | TyAnonArg : - ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml @@ -578,10 +583,11 @@ let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol fun sign -> match sign with | TyNil -> [] | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig' - | TyArg ((loc,(a,id)),sig') -> - TacNonTerm (loc,(untype_user_symbol a,Some id)) :: clause_of_sign sig' - | TyAnonArg ((loc,a),sig') -> - TacNonTerm (loc,(untype_user_symbol a,None)) :: clause_of_sign sig' + | TyArg (a, id, sig') -> + let id = get_identifier id in + TacNonTerm (None,(untype_user_symbol a,Some id)) :: clause_of_sign sig' + | TyAnonArg (a, sig') -> + TacNonTerm (None,(untype_user_symbol a,None)) :: clause_of_sign sig' let clause_of_ty_ml = function | TyML (t,_) -> clause_of_sign t @@ -604,7 +610,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i | _ :: _ -> assert false end | TyIdent (s, sig') -> eval_sign sig' tac - | TyArg ((_loc,(a,id)), sig') -> + | TyArg (a, _, sig') -> let f = eval_sign sig' in begin fun tac vals ist -> match vals with | [] -> assert false @@ -612,7 +618,7 @@ let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.i let v' = Taccoerce.Value.cast (topwit (prj a)) v in f (tac v') vals ist end tac - | TyAnonArg ((_loc,a), sig') -> eval_sign sig' tac + | TyAnonArg (a, sig') -> eval_sign sig' tac let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function | TyML (t,tac) -> eval_sign t tac @@ -624,14 +630,14 @@ let is_constr_entry = function let rec only_constr : type a. a ty_sig -> bool = function | TyNil -> true | TyIdent(_,_) -> false -| TyArg((_,(u,_)),s) -> if is_constr_entry u then only_constr s else false -| TyAnonArg((_,u),s) -> if is_constr_entry u then only_constr s else false +| TyArg (u, _, s) -> if is_constr_entry u then only_constr s else false +| TyAnonArg (u, s) -> if is_constr_entry u then only_constr s else false let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function | TyNil -> [] | TyIdent (_,s) -> mk_sign_vars s -| TyArg((_,(_,name)),s) -> Name name :: mk_sign_vars s -| TyAnonArg((_,_),s) -> Anonymous :: mk_sign_vars s +| TyArg (_, name, s) -> Name (get_identifier name) :: mk_sign_vars s +| TyAnonArg (_, s) -> Anonymous :: mk_sign_vars s let dummy_id = Id.of_string "_" diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 2bfbbe2e1..9bba9ba71 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -72,9 +72,9 @@ type _ ty_sig = | TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig | TyIdent : string * 'r ty_sig -> 'r ty_sig | TyArg : - (('a, 'b, 'c) Extend.ty_user_symbol * Names.Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * string * 'r ty_sig -> ('c -> 'r) ty_sig | TyAnonArg : - ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig + ('a, 'b, 'c) Extend.ty_user_symbol * 'r ty_sig -> 'r ty_sig type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 9d1cc1643..d9ac96d89 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -312,11 +312,11 @@ let interp_name ist env sigma = function | Name id -> Name (interp_ident ist env sigma id) let interp_intro_pattern_var loc ist env sigma id = - try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (make ?loc id) + try try_interp_ltac_var (coerce_to_intro_pattern sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> IntroNaming (IntroIdentifier id) let interp_intro_pattern_naming_var loc ist env sigma id = - try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (make ?loc id) + try try_interp_ltac_var (coerce_to_intro_pattern_naming sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> IntroIdentifier id let interp_int ist ({loc;v=id} as locid) = @@ -357,7 +357,7 @@ let interp_hyp_list ist env sigma l = let interp_reference ist env sigma = function | ArgArg (_,r) -> r | ArgVar {loc;v=id} -> - try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (make ?loc id) + try try_interp_ltac_var (coerce_to_reference sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) @@ -451,7 +451,7 @@ let default_fresh_id = Id.of_string "H" let interp_fresh_id ist env sigma l = let extract_ident ist env sigma id = - try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma) + try try_interp_ltac_var (coerce_to_ident_not_fresh sigma) ist (Some (env,sigma)) (make id) with Not_found -> id in let ids = List.map_filter (function ArgVar {v=id} -> Some id | _ -> None) l in @@ -474,7 +474,7 @@ let interp_fresh_id ist env sigma l = (* Extract the uconstr list from lfun *) let extract_ltac_constr_context ist env sigma = let add_uconstr id v map = - try Id.Map.add id (coerce_to_uconstr env v) map + try Id.Map.add id (coerce_to_uconstr v) map with CannotCoerceTo _ -> map in let add_constr id v map = @@ -799,7 +799,7 @@ and interp_or_and_intro_pattern ist env sigma = function and interp_intro_pattern_list_as_list ist env sigma = function | [{loc;v=IntroNaming (IntroIdentifier id)}] as l -> - (try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun) + (try sigma, coerce_to_intro_pattern_list ?loc sigma (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> List.fold_left_map (interp_intro_pattern ist env) sigma l) | l -> List.fold_left_map (interp_intro_pattern ist env) sigma l @@ -842,7 +842,7 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function | AnonHyp n -> AnonHyp n | NamedHyp id -> try try_interp_ltac_var - (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (make id) + (coerce_to_decl_or_quant_hyp sigma) ist (Some (env,sigma)) (make id) with Not_found -> NamedHyp id let interp_binding ist env sigma {loc;v=(b,c)} = diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.mlg index 81140a46a..21f0414e9 100644 --- a/plugins/micromega/g_micromega.ml4 +++ b/plugins/micromega/g_micromega.mlg @@ -16,70 +16,74 @@ (* *) (************************************************************************) +{ + open Ltac_plugin open Stdarg open Tacarg +} + DECLARE PLUGIN "micromega_plugin" TACTIC EXTEND RED -| [ "myred" ] -> [ Tactics.red_in_concl ] +| [ "myred" ] -> { Tactics.red_in_concl } END TACTIC EXTEND PsatzZ -| [ "psatz_Z" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_Z i +| [ "psatz_Z" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Z i (Tacinterp.tactic_of_value ist t)) - ] -| [ "psatz_Z" tactic(t)] -> [ (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) ] + } +| [ "psatz_Z" tactic(t)] -> { (Coq_micromega.psatz_Z (-1)) (Tacinterp.tactic_of_value ist t) } END TACTIC EXTEND Lia -[ "xlia" tactic(t) ] -> [ (Coq_micromega.xlia (Tacinterp.tactic_of_value ist t)) ] +| [ "xlia" tactic(t) ] -> { (Coq_micromega.xlia (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND Nia -[ "xnlia" tactic(t) ] -> [ (Coq_micromega.xnlia (Tacinterp.tactic_of_value ist t)) ] +| [ "xnlia" tactic(t) ] -> { (Coq_micromega.xnlia (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND NRA -[ "xnra" tactic(t) ] -> [ (Coq_micromega.nra (Tacinterp.tactic_of_value ist t))] +| [ "xnra" tactic(t) ] -> { (Coq_micromega.nra (Tacinterp.tactic_of_value ist t))} END TACTIC EXTEND NQA -[ "xnqa" tactic(t) ] -> [ (Coq_micromega.nqa (Tacinterp.tactic_of_value ist t))] +| [ "xnqa" tactic(t) ] -> { (Coq_micromega.nqa (Tacinterp.tactic_of_value ist t))} END TACTIC EXTEND Sos_Z -| [ "sos_Z" tactic(t) ] -> [ (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) ] +| [ "sos_Z" tactic(t) ] -> { (Coq_micromega.sos_Z (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND Sos_Q -| [ "sos_Q" tactic(t) ] -> [ (Coq_micromega.sos_Q (Tacinterp.tactic_of_value ist t)) ] +| [ "sos_Q" tactic(t) ] -> { (Coq_micromega.sos_Q (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND Sos_R -| [ "sos_R" tactic(t) ] -> [ (Coq_micromega.sos_R (Tacinterp.tactic_of_value ist t)) ] +| [ "sos_R" tactic(t) ] -> { (Coq_micromega.sos_R (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND LRA_Q -[ "lra_Q" tactic(t) ] -> [ (Coq_micromega.lra_Q (Tacinterp.tactic_of_value ist t)) ] +| [ "lra_Q" tactic(t) ] -> { (Coq_micromega.lra_Q (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND LRA_R -[ "lra_R" tactic(t) ] -> [ (Coq_micromega.lra_R (Tacinterp.tactic_of_value ist t)) ] +| [ "lra_R" tactic(t) ] -> { (Coq_micromega.lra_R (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND PsatzR -| [ "psatz_R" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) ] -| [ "psatz_R" tactic(t) ] -> [ (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) ] +| [ "psatz_R" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_R i (Tacinterp.tactic_of_value ist t)) } +| [ "psatz_R" tactic(t) ] -> { (Coq_micromega.psatz_R (-1) (Tacinterp.tactic_of_value ist t)) } END TACTIC EXTEND PsatzQ -| [ "psatz_Q" int_or_var(i) tactic(t) ] -> [ (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) ] -| [ "psatz_Q" tactic(t) ] -> [ (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) ] +| [ "psatz_Q" int_or_var(i) tactic(t) ] -> { (Coq_micromega.psatz_Q i (Tacinterp.tactic_of_value ist t)) } +| [ "psatz_Q" tactic(t) ] -> { (Coq_micromega.psatz_Q (-1) (Tacinterp.tactic_of_value ist t)) } END diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.mlg index 4ac49adb9..16ff512e8 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.mlg @@ -8,11 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin open Stdarg +} + DECLARE PLUGIN "nsatz_plugin" TACTIC EXTEND nsatz_compute -| [ "nsatz_compute" constr(lt) ] -> [ Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) ] +| [ "nsatz_compute" constr(lt) ] -> { Nsatz.nsatz_compute (EConstr.Unsafe.to_constr lt) } END diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 6f4138828..e14c4e2ec 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -38,15 +38,9 @@ open OmegaSolver (* Added by JCF, 09/03/98 *) -let elim_id id = - Proofview.Goal.enter begin fun gl -> - simplest_elim (mkVar id) - end -let resolve_id id = Proofview.Goal.enter begin fun gl -> - apply (mkVar id) -end +let elim_id id = simplest_elim (mkVar id) -let timing timer_name f arg = f arg +let resolve_id id = apply (mkVar id) let display_time_flag = ref false let display_system_flag = ref false diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.mlg index 170b937c9..c3d063cff 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.mlg @@ -18,6 +18,8 @@ DECLARE PLUGIN "omega_plugin" +{ + open Ltac_plugin open Names open Coq_omega @@ -43,14 +45,15 @@ let omega_tactic l = (Tacticals.New.tclREPEAT (Tacticals.New.tclTHENLIST tacs)) (omega_solver) +} TACTIC EXTEND omega -| [ "omega" ] -> [ omega_tactic [] ] +| [ "omega" ] -> { omega_tactic [] } END TACTIC EXTEND omega' | [ "omega" "with" ne_ident_list(l) ] -> - [ omega_tactic (List.map Names.Id.to_string l) ] -| [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ] + { omega_tactic (List.map Names.Id.to_string l) } +| [ "omega" "with" "*" ] -> { omega_tactic ["nat";"positive";"N";"Z"] } END diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.mlg index 09209dc22..749903c3a 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.mlg @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin open Names open Tacexpr @@ -16,8 +18,12 @@ open Quote open Stdarg open Tacarg +} + DECLARE PLUGIN "quote_plugin" +{ + let cont = Id.of_string "cont" let x = Id.of_string "x" @@ -27,12 +33,14 @@ let make_cont (k : Val.t) (c : EConstr.t) = let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac)) +} + TACTIC EXTEND quote - [ "quote" ident(f) ] -> [ quote f [] ] -| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ] +| [ "quote" ident(f) ] -> { quote f [] } +| [ "quote" ident(f) "[" ne_ident_list(lc) "]"] -> { quote f lc } | [ "quote" ident(f) "in" constr(c) "using" tactic(k) ] -> - [ gen_quote (make_cont k) c f [] ] + { gen_quote (make_cont k) c f [] } | [ "quote" ident(f) "[" ne_ident_list(lc) "]" "in" constr(c) "using" tactic(k) ] -> - [ gen_quote (make_cont k) c f lc ] + { gen_quote (make_cont k) c f lc } END diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.mlg index 5b77d08de..c1ce30027 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.mlg @@ -9,6 +9,8 @@ DECLARE PLUGIN "romega_plugin" +{ + open Ltac_plugin open Names open Refl_omega @@ -39,13 +41,15 @@ let romega_tactic unsafe l = (Tactics.intros) (total_reflexive_omega_tactic unsafe)) +} + TACTIC EXTEND romega -| [ "romega" ] -> [ romega_tactic false [] ] -| [ "unsafe_romega" ] -> [ romega_tactic true [] ] +| [ "romega" ] -> { romega_tactic false [] } +| [ "unsafe_romega" ] -> { romega_tactic true [] } END TACTIC EXTEND romega' | [ "romega" "with" ne_ident_list(l) ] -> - [ romega_tactic false (List.map Names.Id.to_string l) ] -| [ "romega" "with" "*" ] -> [ romega_tactic false ["nat";"positive";"N";"Z"] ] + { romega_tactic false (List.map Names.Id.to_string l) } +| [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] } END diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.mlg index aa6757634..9c9fdcfa2 100644 --- a/plugins/rtauto/g_rtauto.ml4 +++ b/plugins/rtauto/g_rtauto.mlg @@ -8,12 +8,15 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ open Ltac_plugin +} + DECLARE PLUGIN "rtauto_plugin" TACTIC EXTEND rtauto - [ "rtauto" ] -> [ Proofview.V82.tactic (Refl_tauto.rtauto_tac) ] +| [ "rtauto" ] -> { Proofview.V82.tactic (Refl_tauto.rtauto_tac) } END diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 93ca9dc5e..2d72b9db6 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1699,7 +1699,8 @@ let abstract_tycon ?loc env evdref subst tycon extenv t = let ty = get_type_of env !evdref t in Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in - let ty = lift (-k) (aux x ty) in + let dummy_subst = List.init k (fun _ -> mkProp) in + let ty = substl dummy_subst (aux x ty) in let depvl = free_rels !evdref ty in let inst = List.map_i diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index ba193da60..4dfa789ba 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -112,7 +112,7 @@ let fix_kind_eq f k1 k2 = match k1, k2 with let eq (i1, o1) (i2, o2) = Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2 in - Int.equal i1 i2 && Array.equal eq a1 a1 + Int.equal i1 i2 && Array.equal eq a1 a2 | GCoFix i1, GCoFix i2 -> Int.equal i1 i2 | (GFix _ | GCoFix _), _ -> false @@ -452,7 +452,7 @@ let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function else r | GProd (na,bk,t,c) -> let na',l' = update_subst na l in - GProd (na,bk,rename_glob_vars l t,rename_glob_vars l' c) + GProd (na',bk,rename_glob_vars l t,rename_glob_vars l' c) | GLambda (na,bk,t,c) -> let na',l' = update_subst na l in GLambda (na',bk,rename_glob_vars l t,rename_glob_vars l' c) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 4ab932723..551cc67b6 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -86,7 +86,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = if not (Sorts.List.mem kind (elim_sorts specif)) then raise (RecursionSchemeError - (NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family env kind), pind))) + (NotAllowedCaseAnalysis (false, fst (UnivGen.fresh_sort_in_family kind), pind))) in let ndepar = mip.mind_nrealdecls + 1 in @@ -136,7 +136,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = mkLambda_string "f" t (add_branch (push_rel (LocalAssum (Anonymous, t)) env) (k+1)) in - let (sigma, s) = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env sigma kind in + let (sigma, s) = Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg sigma kind in let typP = make_arity env' sigma dep indf s in let typP = EConstr.Unsafe.to_constr typP in let c = @@ -455,7 +455,7 @@ let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = | ((indi,u),_,_,dep,kinds)::rest -> let indf = make_ind_family ((indi,u), Context.Rel.to_extended_list mkRel i lnamesparrec) in let s = - Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env) + Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg) evdref kinds in let typP = make_arity env !evdref dep indf s in @@ -550,8 +550,7 @@ let check_arities env listdepkind = let kelim = elim_sorts (mibi,mipi) in if not (Sorts.List.mem kind kelim) then raise (RecursionSchemeError - (NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family env - kind),(mind,u)))) + (NotAllowedCaseAnalysis (true, fst (UnivGen.fresh_sort_in_family kind),(mind,u)))) else if Int.List.mem ni ln then raise (RecursionSchemeError (NotMutualInScheme (mind,mind))) else ni::ln) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index a66ecaaac..ca2702d74 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -138,7 +138,7 @@ let is_correct_arity env sigma c pj ind specif params = then error () else sigma | Evar (ev,_), [] -> - let sigma, s = Evd.fresh_sort_in_family env sigma (max_sort allowed_sorts) in + let sigma, s = Evd.fresh_sort_in_family sigma (max_sort allowed_sorts) in let sigma = Evd.define ev (mkSort s) sigma in sigma | _, (LocalDef _ as d)::ar' -> diff --git a/printing/pputils.ml b/printing/pputils.ml index c6b8d5022..59e5f68f2 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -68,7 +68,7 @@ let pr_short_red_flag pr r = let pr_red_flag pr r = try pr_short_red_flag pr r - with complexRedFlags -> + with ComplexRedFlag -> (if r.rBeta then pr_arg str "beta" else mt ()) ++ (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else (if r.rMatch then pr_arg str "match" else mt ()) ++ diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 7b7973224..e02b5ab95 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -85,6 +85,9 @@ val solve : ?with_end_tac:unit Proofview.tactic -> val by : unit Proofview.tactic -> bool +(** Option telling if unification heuristics should be used. *) +val use_unification_heuristics : unit -> bool + (** [instantiate_nth_evar_com n c] instantiate the [n]th undefined existential variable of the current focused proof by [c] or raises a UserError if no proof is focused or if there is no such [n]th diff --git a/shell.nix b/shell.nix new file mode 100644 index 000000000..3201c5050 --- /dev/null +++ b/shell.nix @@ -0,0 +1,4 @@ +# Some developers don't want a pinned nix-shell by default. +# If you want to use the pin nix-shell or a more sophisticated set of arguments: +# $ nix-shell default.nix --arg shell true +import ./default.nix { pkgs = import <nixpkgs> {}; shell = true; } diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 70f73df5c..3b69d9922 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -44,7 +44,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = mib.mind_nparams_rec else mib.mind_nparams in - let sigma, sort = Evd.fresh_sort_in_family env sigma sort in + let sigma, sort = Evd.fresh_sort_in_family sigma sort in let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in let sigma = Evd.minimize_universes sigma in (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index ad5239116..ea5ff4a6c 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -397,7 +397,7 @@ let build_l2r_rew_scheme dep env ind kind = rel_vect (nrealargs+4) nrealargs; rel_vect 1 nrealargs; [|mkRel 1|]]) in - let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in + let s, ctx' = UnivGen.fresh_sort_in_family kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in let ci = make_case_info (Global.env()) ind RegularStyle in @@ -500,7 +500,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in let realsign_ind_P n aP = name_context env ((LocalAssum (Name varH,aP))::realsign_P n) in - let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in + let s, ctx' = UnivGen.fresh_sort_in_family kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in let ci = make_case_info (Global.env()) ind RegularStyle in @@ -578,7 +578,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = let applied_ind = build_dependent_inductive indu specif in let realsign_ind = name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in - let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in + let s, ctx' = UnivGen.fresh_sort_in_family kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in let ci = make_case_info (Global.env()) ind RegularStyle in diff --git a/tactics/inv.ml b/tactics/inv.ml index e467eacd9..43786c8e1 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -94,7 +94,7 @@ let make_inv_predicate env evd indf realargs id status concl = | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*) | None -> let sort = get_sort_family_of env !evd concl in - let sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd sort in + let sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd sort in let p = make_arity env !evd true indf sort in let evd',(p,ptyp) = Unification.abstract_list_all env !evd p concl (realargs@[mkVar id]) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 10937322e..caf4c1eca 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -251,7 +251,7 @@ let add_inversion_lemma_exn ~poly na com comsort bool tac = let env = Global.env () in let sigma = Evd.from_env env in let sigma, c = Constrintern.interp_type_evars env sigma com in - let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid env sigma comsort in + let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in try add_inversion_lemma ~poly na env sigma c sort bool tac with diff --git a/test-suite/bugs/closed/5719.v b/test-suite/bugs/closed/5719.v new file mode 100644 index 000000000..0fad5f54e --- /dev/null +++ b/test-suite/bugs/closed/5719.v @@ -0,0 +1,9 @@ +Axiom cons_data_one : + forall (Aone : unit -> Set) (i : unit) (a : Aone i), nat. +Axiom P : nat -> Prop. +Axiom children_data_rect3 : forall {Aone : unit -> Set} + (cons_one_case : forall (i : unit) (b : Aone i), + nat -> nat -> P (cons_data_one Aone i b)), + P 0. +Fail Definition decide_children_equality IH := children_data_rect3 + (fun _ '(existT _ _ _) => match IH with tt => _ end). diff --git a/test-suite/bugs/closed/8004.v b/test-suite/bugs/closed/8004.v new file mode 100644 index 000000000..818639997 --- /dev/null +++ b/test-suite/bugs/closed/8004.v @@ -0,0 +1,47 @@ +Require Export Coq.Program.Tactics Coq.Classes.SetoidTactics Coq.Classes.CMorphisms . + +Set Universe Polymorphism. + +Delimit Scope category_theory_scope with category_theory. +Open Scope category_theory_scope. + +Infix "∧" := prod (at level 80, right associativity) : category_theory_scope. + +Class Setoid A := { + equiv : crelation A; + setoid_equiv :> Equivalence equiv +}. + +Notation "f ≈ g" := (equiv f g) (at level 79) : category_theory_scope. + +Open Scope list_scope. + +Generalizable All Variables. + +Fixpoint list_equiv `{Setoid A} (xs ys : list A) : Type := + match xs, ys with + | nil, nil => True + | x :: xs, y :: ys => x ≈ y ∧ list_equiv xs ys + | _, _ => False + end. + +Axiom proof_admitted : False. +Tactic Notation "admit" := abstract case proof_admitted. + +Program Instance list_equivalence `{Setoid A} : Equivalence list_equiv. +Next Obligation. + repeat intro. + induction x; simpl; split; auto. + reflexivity. +Qed. +Next Obligation. + repeat intro. + generalize dependent y. + induction x, y; simpl; intros; auto. + destruct X; split. + now symmetry. + intuition. +Qed. +Next Obligation. +admit. +Defined. diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected index 975e359b7..159e64551 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/001-correct-diff-sorting-order/time-of-build-both.log.expected @@ -1,6 +1,6 @@ After | File Name | Before || Change | % Change ---------------------------------------------------------------------------------------------- -19m16.05s | Total | 21m25.28s || -2m09.23s | -10.05% +19m16.04s | Total | 21m25.27s || -2m09.23s | -10.05% ---------------------------------------------------------------------------------------------- 4m01.34s | Specific/X25519/C64/ladderstep | 4m59.49s || -0m58.15s | -19.41% 2m48.52s | Specific/solinas32_2e255m765_13limbs/femul | 3m12.95s || -0m24.42s | -12.66% diff --git a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected index fdd5ec21d..b9739ddb1 100644 --- a/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected +++ b/test-suite/coq-makefile/timing/precomputed-time-tests/002-single-file-sorting/time-of-build-pretty.log.expected @@ -1,6 +1,6 @@ Time | File Name ---------------------------------------------------------- -19m16.05s | Total +19m16.04s | Total ---------------------------------------------------------- 4m01.34s | Specific/X25519/C64/ladderstep 3m09.62s | Specific/NISTP256/AMD64/femul diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 8e60d3932..8b6822a4e 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -65,20 +65,20 @@ VERBOSE ?= # Time the Coq process (set to non empty), and how (see default value) TIMED?= TIMECMD?= -# Use /usr/bin/env time on linux, gtime on Mac OS +# Use command time on linux, gtime on Mac OS TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" ifneq (,$(TIMED)) -ifeq (0,$(shell /usr/bin/env time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) -STDTIME?=/usr/bin/env time -f $(TIMEFMT) +ifeq (0,$(shell command time -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) +STDTIME?=command time -f $(TIMEFMT) else ifeq (0,$(shell gtime -f $(TIMEFMT) true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=gtime -f $(TIMEFMT) else -STDTIME?=time +STDTIME?=command time endif endif else -STDTIME?=/usr/bin/env time -f $(TIMEFMT) +STDTIME?=command time -f $(TIMEFMT) endif # Coq binaries @@ -86,7 +86,6 @@ COQC ?= "$(COQBIN)coqc" COQTOP ?= "$(COQBIN)coqtop" COQCHK ?= "$(COQBIN)coqchk" COQDEP ?= "$(COQBIN)coqdep" -GALLINA ?= "$(COQBIN)gallina" COQDOC ?= "$(COQBIN)coqdoc" COQMKFILE ?= "$(COQBIN)coq_makefile" @@ -256,7 +255,6 @@ VO = vo VOFILES = $(VFILES:.v=.$(VO)) GLOBFILES = $(VFILES:.v=.glob) -GFILES = $(VFILES:.v=.g) HTMLFILES = $(VFILES:.v=.html) GHTMLFILES = $(VFILES:.v=.g.html) BEAUTYFILES = $(addsuffix .beautified,$(VFILES)) @@ -442,8 +440,6 @@ all-mli.tex: $(MLIFILES:.mli=.cmi) $(HIDE)$(CAMLDOC) -latex \ -o $@ -m A $(CAMLDEBUG) $(CAMLDOCFLAGS) $(MLIFILES) -gallina: $(GFILES) - all.ps: $(VFILES) $(SHOW)'COQDOC -ps $(GAL)' $(HIDE)$(COQDOC) \ @@ -564,7 +560,6 @@ clean:: $(HIDE)find . -name .coq-native -type d -empty -delete $(HIDE)rm -f $(VOFILES) $(HIDE)rm -f $(VOFILES:.vo=.vio) - $(HIDE)rm -f $(GFILES) $(HIDE)rm -f $(BEAUTYFILES) $(VFILES:=.old) $(HIDE)rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob all-mli.tex $(HIDE)rm -f $(VFILES:.v=.glob) @@ -683,10 +678,6 @@ $(BEAUTYFILES): %.v.beautified: %.v $(SHOW)'BEAUTIFY $<' $(HIDE)$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) -beautify $< -$(GFILES): %.g: %.v - $(SHOW)'GALLINA $<' - $(HIDE)$(GALLINA) $< - $(TEXFILES): %.tex: %.v $(SHOW)'COQDOC -latex $<' $(HIDE)$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@ diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py index 0d24332f1..b16888c7e 100644 --- a/tools/TimeFileMaker.py +++ b/tools/TimeFileMaker.py @@ -1,6 +1,9 @@ -#!/usr/bin/env python from __future__ import with_statement +from __future__ import division +from __future__ import unicode_literals +from __future__ import print_function import os, sys, re +from io import open # This script parses the output of `make TIMED=1` into a dictionary # mapping names of compiled files to the number of minutes and seconds @@ -8,7 +11,7 @@ import os, sys, re STRIP_REG = re.compile('^(coq/|contrib/|)(?:theories/|src/)?') STRIP_REP = r'\1' -INFINITY = '\xe2\x88\x9e' +INFINITY = '\u221e' def parse_args(argv, USAGE, HELP_STRING): sort_by = 'auto' @@ -27,7 +30,7 @@ def parse_args(argv, USAGE, HELP_STRING): def reformat_time_string(time): seconds, milliseconds = time.split('.') seconds = int(seconds) - minutes, seconds = int(seconds / 60), seconds % 60 + minutes, seconds = divmod(seconds, 60) return '%dm%02d.%ss' % (minutes, seconds, milliseconds) def get_times(file_name): @@ -40,7 +43,7 @@ def get_times(file_name): if file_name == '-': lines = sys.stdin.read() else: - with open(file_name, 'r') as f: + with open(file_name, 'r', encoding="utf-8") as f: lines = f.read() reg = re.compile(r'^([^\s]+) \([^\)]*?user: ([0-9\.]+)[^\)]*?\)\s*$', re.MULTILINE) times = reg.findall(lines) @@ -60,7 +63,7 @@ def get_single_file_times(file_name): if file_name == '-': lines = sys.stdin.read() else: - with open(file_name, 'r') as f: + with open(file_name, 'r', encoding="utf-8") as f: lines = f.read() reg = re.compile(r'^Chars ([0-9]+) - ([0-9]+) ([^ ]+) ([0-9\.]+) secs (.*)$', re.MULTILINE) times = reg.findall(lines) @@ -101,7 +104,7 @@ def from_seconds(seconds, signed=False): ''' sign = ('-' if seconds < 0 else '+') if signed else '' seconds = abs(seconds) - minutes = int(seconds) / 60 + minutes = int(seconds) // 60 seconds -= minutes * 60 full_seconds = int(seconds) partial_seconds = int(100 * (seconds - full_seconds)) @@ -112,7 +115,8 @@ def sum_times(times, signed=False): Takes the values of an output from get_times, parses the time strings, and returns their sum, in the same string format. ''' - return from_seconds(sum(map(to_seconds, times)), signed=signed) + # sort the times before summing because floating point addition is not associative + return from_seconds(sum(sorted(map(to_seconds, times))), signed=signed) def format_percentage(num, signed=True): sign = ('-' if num < 0 else '+') if signed else '' @@ -153,8 +157,8 @@ def make_diff_table_string(left_times_dict, right_times_dict, # set the widths of each of the columns by the longest thing to go in that column left_sum = sum_times(left_times_dict.values()) right_sum = sum_times(right_times_dict.values()) - left_sum_float = sum(map(to_seconds, left_times_dict.values())) - right_sum_float = sum(map(to_seconds, right_times_dict.values())) + left_sum_float = sum(sorted(map(to_seconds, left_times_dict.values()))) + right_sum_float = sum(sorted(map(to_seconds, right_times_dict.values()))) diff_sum = from_seconds(left_sum_float - right_sum_float, signed=True) percent_diff_sum = (format_percentage((left_sum_float - right_sum_float) / right_sum_float) if right_sum_float > 0 else 'N/A') @@ -203,8 +207,12 @@ def make_table_string(times_dict, def print_or_write_table(table, files): if len(files) == 0 or '-' in files: - print(table) + try: + binary_stdout = sys.stdout.buffer + except AttributeError: + binary_stdout = sys.stdout + print(table.encode("utf-8"), file=binary_stdout) for file_name in files: if file_name != '-': - with open(file_name, 'w') as f: + with open(file_name, 'w', encoding="utf-8") as f: f.write(table) diff --git a/tools/coq-font-lock.el b/tools/coq-font-lock.el deleted file mode 100644 index 068e64002..000000000 --- a/tools/coq-font-lock.el +++ /dev/null @@ -1,137 +0,0 @@ -;; coq-font-lock.el --- Coq syntax highlighting for Emacs - compatibilty code -;; Pierre Courtieu, may 2009 -;; -;; Authors: Pierre Courtieu -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> - -;; This is copy paste from ProofGeneral by David Aspinall -;; <David.Aspinall@ed.ac.uk>. ProofGeneral is under GPL and Copyright -;; (C) LFCS Edinburgh. - - -;;; Commentary: -;; This file contains the code necessary to coq-syntax.el and -;; coq-db.el from ProofGeneral. It is also pocked from ProofGeneral. - - -;;; History: -;; First created from ProofGeneral may 28th 2009 - - -;;; Code: - -(setq coq-version-is-V8-1 t) -(defun coq-build-regexp-list-from-db (db &optional filter) - "Take a keyword database DB and return the list of regexps for font-lock. -If non-nil Optional argument FILTER is a function applying to each line of DB. -For each line if FILTER returns nil, then the keyword is not added to the -regexp. See `coq-syntax-db' for DB structure." - (let ((l db) (res ())) - (while l - (let* ((hd (car l)) (tl (cdr l)) ; hd is the first infos list - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing - (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string - ) - ;; TODO delete doublons - (when (and e5 (or (not filter) (funcall filter hd))) - (setq res (nconc res (list e5)))) ; careful: nconc destructive! - (setq l tl))) - res - )) -(defun filter-state-preserving (l) - ; checkdoc-params: (l) - "Not documented." - (not (nth 3 l))) ; fourth argument is nil --> state preserving command - -(defun filter-state-changing (l) - ; checkdoc-params: (l) - "Not documented." - (nth 3 l)) ; fourth argument is nil --> state preserving command - -;; Generic font-lock - -(defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)" - "A regular expression for parsing identifiers.") - -;; For font-lock, we treat ,-separated identifiers as one identifier -;; and refontify commata using \{proof-zap-commas}. - -(defun proof-anchor-regexp (e) - "Anchor (\\`) and group the regexp E." - (concat "\\`\\(" e "\\)")) - -(defun proof-ids (proof-id &optional sepregexp) - "Generate a regular expression for separated lists of identifiers PROOF-ID. -Default is comma separated, or SEPREGEXP if set." - (concat proof-id "\\(\\s-*" (or sepregexp ",") "\\s-*" - proof-id "\\)*")) - -(defun proof-ids-to-regexp (l) - "Maps a non-empty list of tokens `L' to a regexp matching any element." - (if (featurep 'xemacs) - (mapconcat (lambda (s) (concat "\\_<" s "\\_>")) l "\\|") ;; old version - (concat "\\_<\\(?:" (mapconcat 'identity l "\\|") "\\)\\_>"))) - -;; TODO: get rid of this list. Does 'default work widely enough -;; by now? -(defconst pg-defface-window-systems - '(x ;; bog standard - mswindows ;; Windows - w32 ;; Windows - gtk ;; gtk emacs (obsolete?) - mac ;; used by Aquamacs - carbon ;; used by Carbon XEmacs - ns ;; NeXTstep Emacs (Emacs.app) - x-toolkit) ;; possible catch all (but probably not) - "A list of possible values for variable `window-system'. -If you are on a window system and your value of variable -`window-system' is not listed here, you may not get the correct -syntax colouring behaviour.") - -(defmacro proof-face-specs (bl bd ow) - "Return a spec for `defface' with BL for light bg, BD for dark, OW o/w." - `(append - (apply 'append - (mapcar - (lambda (ty) (list - (list (list (list 'type ty) '(class color) - (list 'background 'light)) - (quote ,bl)) - (list (list (list 'type ty) '(class color) - (list 'background 'dark)) - (quote ,bd)))) - pg-defface-window-systems)) - (list (list t (quote ,ow))))) - -;;A new face for tactics -(defface coq-solve-tactics-face - (proof-face-specs - (:foreground "forestgreen" t) ; for bright backgrounds - (:foreground "forestgreen" t) ; for dark backgrounds - ()) ; for black and white - "Face for names of closing tactics in proof scripts." - :group 'proof-faces) - -;;A new face for tactics which fail when they don't kill the current goal -(defface coq-solve-tactics-face - (proof-face-specs - (:foreground "red" t) ; for bright backgrounds - (:foreground "red" t) ; for dark backgrounds - ()) ; for black and white - "Face for names of closing tactics in proof scripts." - :group 'proof-faces) - - -(defconst coq-solve-tactics-face 'coq-solve-tactics-face - "Expression that evaluates to a face. -Required so that 'proof-solve-tactics-face is a proper facename") - -(defconst proof-tactics-name-face 'coq-solve-tactics-face) -(defconst proof-tacticals-name-face 'coq-solve-tactics-face) - -(provide 'coq-font-lock) -;;; coq-font-lock.el ends here diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 6f11ee397..ad489da82 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -218,7 +218,7 @@ let windrive s = else "" ;; -let generate_conf_coq_config oc args = +let generate_conf_coq_config oc = section oc "Coq configuration."; let src_dirs = Coq_config.all_src_dirs in Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; @@ -282,7 +282,7 @@ let generate_conf oc project args = fprintf oc "# %s\n\n" (String.concat " " (List.map quote args)); generate_conf_files oc project; generate_conf_includes oc project; - generate_conf_coq_config oc args; + generate_conf_coq_config oc; generate_conf_defs oc project; generate_conf_doc oc project; generate_conf_extra_target oc project.extra_targets; diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index df493fdf7..885324aa0 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -77,7 +77,7 @@ let add_ref m loc m' sp id ty = let find m l = Hashtbl.find reftable (m, l) -let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t) +let find_string s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t) (* Coq modules *) diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 5cd301389..7c9aad67f 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -41,7 +41,7 @@ type index_entry = val find : coq_module -> loc -> index_entry (* Find what data is referred to by some string in some coq module *) -val find_string : coq_module -> string -> index_entry +val find_string : string -> index_entry val add_module : coq_module -> unit diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index d25227002..c640167ac 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -431,7 +431,7 @@ module Latex = struct else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then try - let tag = Index.find_string (get_module false) s in + let tag = Index.find_string s in reference (translate s) tag with _ -> Tokens.output_tagged_ident_string s else Tokens.output_tagged_ident_string s @@ -706,7 +706,7 @@ module Html = struct else if is_keyword s then printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s) else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then - try reference (translate s) (Index.find_string (get_module false) s) + try reference (translate s) (Index.find_string s) with Not_found -> Tokens.output_tagged_ident_string s else Tokens.output_tagged_ident_string s diff --git a/tools/gallina-db.el b/tools/gallina-db.el deleted file mode 100644 index 9664f69f8..000000000 --- a/tools/gallina-db.el +++ /dev/null @@ -1,240 +0,0 @@ -;;; gallina-db.el --- coq keywords database utility functions -;; -;; Author: Pierre Courtieu <courtieu@lri.fr> -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; - -;;; We store all information on keywords (tactics or command) in big -;; tables (ex: `coq-tactics-db') From there we get: menus including -;; "smart" commands, completions for command coq-insert-... -;; abbrev tables and font-lock keyword - -;;; real value defined below - -;;; Commentary: -;; - -;;; Code: - -;(require 'proof-config) ; for proof-face-specs, a macro -;(require 'holes) - -(defconst coq-syntax-db nil - "Documentation-only variable, for coq keyword databases. -Each element of a keyword database contains the definition of a \"form\", of the -form: - -(MENUNAME ABBREV INSERT STATECH KWREG INSERT-FUN HIDE) - -MENUNAME is the name of form (or form variant) as it should appear in menus or -completion lists. - -ABBREV is the abbreviation for completion via \\[expand-abbrev]. - -INSERT is the complete text of the form, which may contain holes denoted by -\"#\" or \"@{xxx}\". - -If non-nil the optional STATECH specifies that the command is not state -preserving for coq. - -If non-nil the optional KWREG is the regexp to colorize correponding to the -keyword. ex: \"simple\\\\s-+destruct\" (\\\\s-+ meaning \"one or more spaces\"). -*WARNING*: A regexp longer than another one should be put FIRST. For example: - - (\"Module Type\" ... ... t \"Module\\s-+Type\") - (\"Module\" ... ... t \"Module\") - -Is ok because the longer regexp is recognized first. - -If non-nil the optional INSERT-FUN is the function to be called when inserting -the form (instead of inserting INSERT, except when using \\[expand-abbrev]). This -allows writing functions asking for more information to assist the user. - -If non-nil the optional HIDE specifies that this form should not appear in the -menu but only in interactive completions. - -Example of what could be in your emacs init file: - -(defvar coq-user-tactics-db - '( - (\"mytac\" \"mt\" \"mytac # #\" t \"mytac\") - (\"myassert by\" \"massb\" \"myassert ( # : # ) by #\" t \"assert\") - )) - -Explanation of the first line: the tactic menu entry mytac, abbreviated by mt, -will insert \"mytac # #\" where #s are holes to fill, and \"mytac\" becomes a -new keyword to colorize." ) - -(defun coq-insert-from-db (db prompt) - "Ask for a keyword, with completion on keyword database DB and insert. -Insert corresponding string with holes at point. If an insertion function is -present for the keyword, call it instead. see `coq-syntax-db' for DB -structure." - (let* ((tac (completing-read (concat prompt " (tab for completion) : ") - db nil nil)) - (infos (cddr (assoc tac db))) - (s (car infos)) ; completion to insert - (f (car-safe (cdr-safe (cdr-safe (cdr infos))))) ; insertion function - (pt (point))) - (if f (funcall f) ; call f if present - (insert (or s tac)) ; insert completion and indent otherwise - (holes-replace-string-by-holes-backward-jump pt) - (indent-according-to-mode)))) - - - -(defun coq-build-regexp-list-from-db (db &optional filter) - "Take a keyword database DB and return the list of regexps for font-lock. -If non-nil Optional argument FILTER is a function applying to each line of DB. -For each line if FILTER returns nil, then the keyword is not added to the -regexp. See `coq-syntax-db' for DB structure." - (let ((l db) (res ())) - (while l - (let* ((hd (car l)) (tl (cdr l)) ; hd is the first infos list - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing - (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string - ) - ;; TODO delete doublons - (when (and e5 (or (not filter) (funcall filter hd))) - (setq res (nconc res (list e5)))) ; careful: nconc destructive! - (setq l tl))) - res - )) - -;; Computes the max length of strings in a list -(defun max-length-db (db) - "Return the length of the longest first element (menu label) of DB. -See `coq-syntax-db' for DB structure." - (let ((l db) (res 0)) - (while l - (let ((lgth (length (car (car l))))) - (setq res (max lgth res)) - (setq l (cdr l)))) - res)) - - - -(defun coq-build-menu-from-db-internal (db lgth menuwidth) - "Take a keyword database DB and return one insertion submenu. -Argument LGTH is the max size of the submenu. Argument MENUWIDTH is the width -of the largest line in the menu (without abbrev and shortcut specifications). -Used by `coq-build-menu-from-db', which you should probably use instead. See -`coq-syntax-db' for DB structure." - (let ((l db) (res ()) (size lgth) - (keybind-abbrev (substitute-command-keys " \\[expand-abbrev]"))) - (while (and l (> size 0)) - (let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4 - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing - (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string - (e6 (car-safe tl5)) ; e6 = function for smart insertion - (e7 (car-safe (cdr-safe tl5))) ; e7 = if non-nil : hide in menu - (entry-with (max (- menuwidth (length e1)) 0)) - (spaces (make-string entry-with ? )) - ;;(restofmenu (coq-build-menu-from-db-internal tl (- size 1) menuwidth)) - ) - (when (not e7) ;; if not hidden - (let ((menu-entry - (vector - ;; menu entry label - (concat e1 (if (not e2) "" (concat spaces "(" e2 keybind-abbrev ")"))) - ;;insertion function if present otherwise insert completion - (if e6 e6 `(holes-insert-and-expand ,e3)) - t))) - (setq res (nconc res (list menu-entry)))));; append *in place* - (setq l tl) - (setq size (- size 1)))) - res)) - - -(defun coq-build-title-menu (db size) - "Build a title for the first submenu of DB, of size SIZE. -Return the string made of the first and the SIZE nth first element of DB, -separated by \"...\". Used by `coq-build-menu-from-db'. See `coq-syntax-db' -for DB structure." - (concat (car-safe (car-safe db)) - " ... " - (car-safe (car-safe (nthcdr (- size 1) db))))) - -(defun coq-sort-menu-entries (menu) - (sort menu - (lambda (x y) (string< - (downcase (elt x 0)) - (downcase (elt y 0)))))) - -(defun coq-build-menu-from-db (db &optional size) - "Take a keyword database DB and return a list of insertion menus for them. -Submenus contain SIZE entries (default 30). See `coq-syntax-db' for DB -structure." - ;; sort is destructive for the list, so copy list before sorting - (let* ((l (coq-sort-menu-entries (copy-list db))) (res ()) - (wdth (+ 2 (max-length-db db))) - (sz (or size 30)) (lgth (length l))) - (while l - (if (<= lgth sz) - (setq res ;; careful: nconc destructive! - (nconc res (list (cons - (coq-build-title-menu l lgth) - (coq-build-menu-from-db-internal l lgth wdth))))) - (setq res ; careful: nconc destructive! - (nconc res (list (cons - (coq-build-title-menu l sz) - (coq-build-menu-from-db-internal l sz wdth)))))) - (setq l (nthcdr sz l)) - (setq lgth (length l))) - res)) - -(defun coq-build-abbrev-table-from-db (db) - "Take a keyword database DB and return an abbrev table. -See `coq-syntax-db' for DB structure." - (let ((l db) (res ())) - (while l - (let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4 - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - ) - ;; careful: nconc destructive! - (when e2 - (setq res (nconc res (list `(,e2 ,e3 holes-abbrev-complete))))) - (setq l tl))) - res)) - - -(defun filter-state-preserving (l) - ; checkdoc-params: (l) - "Not documented." - (not (nth 3 l))) ; fourth argument is nil --> state preserving command - -(defun filter-state-changing (l) - ; checkdoc-params: (l) - "Not documented." - (nth 3 l)) ; fourth argument is nil --> state preserving command - -(defconst coq-solve-tactics-face 'coq-solve-tactics-face - "Expression that evaluates to a face. -Required so that 'proof-solve-tactics-face is a proper facename") - - -;;A new face for tactics which fail when they don't kill the current goal -(defface coq-solve-tactics-face - '((t (:background "red"))) - "Face for names of closing tactics in proof scripts." - :group 'proof-faces) - - - - - -(provide 'gallina-db) - -;;; gallina-db.el ends here - -;** Local Variables: *** -;** fill-column: 80 *** -;** End: *** diff --git a/tools/gallina-syntax.el b/tools/gallina-syntax.el deleted file mode 100644 index 7c59fb6ae..000000000 --- a/tools/gallina-syntax.el +++ /dev/null @@ -1,979 +0,0 @@ -;; gallina-syntax.el Font lock expressions for Coq -;; Copyright (C) 1997-2007 LFCS Edinburgh. -;; Authors: Thomas Kleymann, Healfdene Goguen, Pierre Courtieu -;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; Maintainer: Pierre Courtieu <courtieu@lri.fr> - -;; gallina-syntax.el,v 9.9 2008/07/21 15:14:58 pier Exp - -;(require 'proof-syntax) -;(require 'proof-utils) ; proof-locate-executable -(require 'gallina-db) - - - - ;;; keyword databases - - -(defcustom coq-user-tactics-db nil - "User defined tactic information. See `coq-syntax-db' for - syntax. It is not necessary to add your own tactics here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your tactics will be colorized by font-lock - - 2 your tactics will be added to the menu and to completion when - calling \\[coq-insert-tactic] - - 3 you may define an abbreviation for your tactic." - - :type '(repeat sexp) - :group 'coq) - - -(defcustom coq-user-commands-db nil - "User defined command information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - -(defcustom coq-user-tacticals-db nil - "User defined tactical information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - -(defcustom coq-user-solve-tactics-db nil - "User defined closing tactics. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - - - -(defcustom coq-user-reserved-db nil - "User defined reserved keywords information. See `coq-syntax-db' for - syntax. It is not necessary to add your own commands here (it is not - needed by the synchronizing/backtracking system). You may however do - so for the following reasons: - - 1 your commands will be colorized by font-lock - - 2 your commands will be added to the menu and to completion when - calling \\[coq-insert-command] - - 3 you may define an abbreviation for your command." - - :type '(repeat sexp) - :group 'coq) - - - -(defvar coq-tactics-db - (append - coq-user-tactics-db - '( - ("absurd " "abs" "absurd " t "absurd") - ("apply" "ap" "apply " t "apply") - ("assert by" "assb" "assert ( # : # ) by #" t "assert") - ("assert" "ass" "assert ( # : # )" t) - ;; ("assumption" "as" "assumption" t "assumption") - ("auto with arith" "awa" "auto with arith" t) - ("auto with" "aw" "auto with @{db}" t) - ("auto" "a" "auto" t "auto") - ("autorewrite with in using" "arwiu" "autorewrite with @{db,db...} in @{hyp} using @{tac}" t) - ("autorewrite with in" "arwi" "autorewrite with @{db,db...} in @{hyp}" t) - ("autorewrite with using" "arwu" "autorewrite with @{db,db...} using @{tac}" t) - ("autorewrite with" "ar" "autorewrite with @{db,db...}" t "autorewrite") - ("case" "c" "case " t "case") - ("cbv" "cbv" "cbv beta [#] delta iota zeta" t "cbv") - ("change in" "chi" "change # in #" t) - ("change with in" "chwi" "change # with # in #" t) - ("change with" "chw" "change # with" t) - ("change" "ch" "change " t "change") - ("clear" "cl" "clear" t "clear") - ("clearbody" "cl" "clearbody" t "clearbody") - ("cofix" "cof" "cofix" t "cofix") - ("coinduction" "coind" "coinduction" t "coinduction") - ("compare" "cmpa" "compare # #" t "compare") - ("compute" "cmpu" "compute" t "compute") - ;; ("congruence" "cong" "congruence" t "congruence") - ("constructor" "cons" "constructor" t "constructor") - ;; ("contradiction" "contr" "contradiction" t "contradiction") - ("cut" "cut" "cut" t "cut") - ("cutrewrite" "cutr" "cutrewrite -> # = #" t "cutrewrite") - ;; ("decide equality" "deg" "decide equality" t "decide\\s-+equality") - ("decompose record" "decr" "decompose record #" t "decompose\\s-+record") - ("decompose sum" "decs" "decompose sum #" t "decompose\\s-+sum") - ("decompose" "dec" "decompose [#] #" t "decompose") - ("dependent inversion" "depinv" "dependent inversion" t "dependent\\s-+inversion") - ("dependent inversion with" "depinvw" "dependent inversion # with #" t) - ("dependent inversion_clear" "depinvc" "dependent inversion_clear" t "dependent\\s-+inversion_clear") - ("dependent inversion_clear with" "depinvw" "dependent inversion_clear # with #" t) - ("dependent rewrite ->" "depr" "dependent rewrite -> @{id}" t "dependent\\s-+rewrite") - ("dependent rewrite <-" "depr<" "dependent rewrite <- @{id}" t) - ("destruct as" "desa" "destruct # as #" t) - ("destruct using" "desu" "destruct # using #" t) - ("destruct" "des" "destruct " t "destruct") - ;; ("discriminate" "dis" "discriminate" t "discriminate") - ("discrR" "discrR" "discrR" t "discrR") - ("double induction" "dind" "double induction # #" t "double\\s-+induction") - ("eapply" "eap" "eapply #" t "eapply") - ("eauto with arith" "eawa" "eauto with arith" t) - ("eauto with" "eaw" "eauto with @{db}" t) - ("eauto" "ea" "eauto" t "eauto") - ("econstructor" "econs" "econstructor" t "econstructor") - ("eexists" "eex" "eexists" t "eexists") - ("eleft" "eleft" "eleft" t "eleft") - ("elim using" "elu" "elim # using #" t) - ("elim" "e" "elim #" t "elim") - ("elimtype" "elt" "elimtype" "elimtype") - ("eright" "erig" "eright" "eright") - ("esplit" "esp" "esplit" t "esplit") - ;; ("exact" "exa" "exact" t "exact") - ("exists" "ex" "exists #" t "exists") - ;; ("fail" "fa" "fail" nil) - ;; ("field" "field" "field" t "field") - ("firstorder" "fsto" "firstorder" t "firstorder") - ("firstorder with" "fsto" "firstorder with #" t) - ("firstorder with using" "fsto" "firstorder # with #" t) - ("fold" "fold" "fold #" t "fold") - ;; ("fourier" "four" "fourier" t "fourier") - ("functional induction" "fi" "functional induction @{f} @{args}" t "functional\\s-+induction") - ("generalize dependent" "gd" "generalize dependent #" t "generalize\\s-+dependent") - ("generalize" "g" "generalize #" t "generalize") - ("hnf" "hnf" "hnf" t "hnf") - ("idtac" "id" "idtac" nil "idtac") ; also in tacticals with abbrev id - ("idtac \"" "id\"" "idtac \"#\"") ; also in tacticals - ("induction" "ind" "induction #" t "induction") - ("induction using" "indu" "induction # using #" t) - ("injection" "inj" "injection #" t "injection") - ("instantiate" "inst" "instantiate" t "instantiate") - ("intro" "i" "intro" t "intro") - ("intro after" "ia" "intro # after #" t) - ("intros" "is" "intros #" t "intros") - ("intros! (guess names)" nil "intros #" nil nil coq-insert-intros) - ("intros until" "isu" "intros until #" t) - ("intuition" "intu" "intuition #" t "intuition") - ("inversion" "inv" "inversion #" t "inversion") - ("inversion in" "invi" "inversion # in #" t) - ("inversion using" "invu" "inversion # using #" t) - ("inversion using in" "invui" "inversion # using # in #" t) - ("inversion_clear" "invcl" "inversion_clear" t "inversion_clear") - ("lapply" "lap" "lapply" t "lapply") - ("lazy" "lazy" "lazy beta [#] delta iota zeta" t "lazy") - ("left" "left" "left" t "left") - ("linear" "lin" "linear" t "linear") - ("load" "load" "load" t "load") - ("move after" "mov" "move # after #" t "move") - ("omega" "o" "omega" t "omega") - ("pattern" "pat" "pattern" t "pattern") - ("pattern(s)" "pats" "pattern # , #" t) - ("pattern at" "pata" "pattern # at #" t) - ("pose" "po" "pose ( # := # )" t "pose") - ("prolog" "prol" "prolog" t "prolog") - ("quote" "quote" "quote" t "quote") - ("quote []" "quote2" "quote # [#]" t) - ("red" "red" "red" t "red") - ("refine" "ref" "refine" t "refine") - ;; ("reflexivity" "refl" "reflexivity #" t "reflexivity") - ("rename into" "ren" "rename # into #" t "rename") - ("replace with" "rep" "replace # with #" t "replace") - ("replace with in" "repi" "replace # with # in #" t) - ("rewrite <- in" "ri<" "rewrite <- # in #" t) - ("rewrite <-" "r<" "rewrite <- #" t) - ("rewrite in" "ri" "rewrite # in #" t) - ("rewrite" "r" "rewrite #" t "rewrite") - ("right" "rig" "right" t "right") - ;; ("ring" "ring" "ring #" t "ring") - ("set in * |-" "seth" "set ( # := #) in * |-" t) - ("set in *" "set*" "set ( # := #) in *" t) - ("set in |- *" "setg" "set ( # := #) in |- *" t) - ("set in" "seti" "set ( # := #) in #" t) - ("set" "set" "set ( # := #)" t "set") - ("setoid_replace with" "strep2" "setoid_replace # with #" t "setoid_replace") - ("setoid replace with" "strep" "setoid replace # with #" t "setoid\\s-+replace") - ("setoid_rewrite" "strew" "setoid_rewrite #" t "setoid_rewrite") - ("setoid rewrite" "strew" "setoid rewrite #" t "setoid\\s-+rewrite") - ("simpl" "s" "simpl" t "simpl") - ("simpl" "sa" "simpl # at #" t) - ("simple destruct" "sdes" "simple destruct" t "simple\\s-+destruct") - ("simple inversion" "sinv" "simple inversion" t "simple\\s-+inversion") - ("simple induction" "sind" "simple induction" t "simple\\s-+induction") - ("simplify_eq" "simeq" "simplify_eq @{hyp}" t "simplify_eq") - ("specialize" "spec" "specialize" t "specialize") - ("split" "sp" "split" t "split") - ("split_Rabs" "spra" "splitRabs" t "split_Rabs") - ("split_Rmult" "sprm" "splitRmult" t "split_Rmult") - ("stepl" "stl" "stepl #" t "stepl") - ("stepl by" "stlb" "stepl # by #" t) - ("stepr" "str" "stepr #" t "stepr") - ("stepr by" "strb" "stepr # by #" t) - ("subst" "su" "subst #" t "subst") - ("symmetry" "sy" "symmetry" t "symmetry") - ("symmetry in" "syi" "symmetry in #" t) - ;; ("tauto" "ta" "tauto" t "tauto") - ("transitivity" "trans" "transitivity #" t "transitivity") - ("trivial" "t" "trivial" t "trivial") - ("trivial with" "tw" "trivial with @{db}" t) - ("unfold" "u" "unfold #" t "unfold") - ("unfold(s)" "us" "unfold # , #" t) - ("unfold in" "unfi" "unfold # in #" t) - ("unfold at" "unfa" "unfold # at #" t) - )) - "Coq tactics information list. See `coq-syntax-db' for syntax. " - ) - -(defvar coq-solve-tactics-db - (append - coq-user-solve-tactics-db - '( - ("assumption" "as" "assumption" t "assumption") - ("by" "by" "by #" t "by") - ("congruence" "cong" "congruence" t "congruence") - ("contradiction" "contr" "contradiction" t "contradiction") - ("decide equality" "deg" "decide equality" t "decide\\s-+equality") - ("discriminate" "dis" "discriminate" t "discriminate") - ("exact" "exa" "exact" t "exact") - ("fourier" "four" "fourier" t "fourier") - ("fail" "fa" "fail" nil) - ("field" "field" "field" t "field") - ("omega" "o" "omega" t "omega") - ("reflexivity" "refl" "reflexivity #" t "reflexivity") - ("ring" "ring" "ring #" t "ring") - ("solve" nil "solve [ # | # ]" nil "solve") - ("tauto" "ta" "tauto" t "tauto") - )) - "Coq tactic(al)s that solve a subgoal." - ) - - -(defvar coq-tacticals-db - (append - coq-user-tacticals-db - '( - ("info" nil "info #" nil "info") - ("first" nil "first [ # | # ]" nil "first") - ("abstract" nil "abstract @{tac} using @{name}." nil "abstract") - ("do" nil "do @{num} @{tac}" nil "do") - ("idtac" nil "idtac") ; also in tactics - ; ("idtac \"" nil "idtac \"#\"") ; also in tactics - ("fail" "fa" "fail" nil "fail") - ; ("fail \"" "fa\"" "fail" nil) ; - ; ("orelse" nil "orelse #" t "orelse") - ("repeat" nil "repeat #" nil "repeat") - ("try" nil "try #" nil "try") - ("progress" nil "progress #" nil "progress") - ("|" nil "[ # | # ]" nil) - ("||" nil "# || #" nil) - )) - "Coq tacticals information list. See `coq-syntax-db' for syntax.") - - - - -(defvar coq-decl-db - '( - ("Axiom" "ax" "Axiom # : #" t "Axiom") - ("Hint Constructors" "hc" "Hint Constructors # : #." t "Hint\\s-+Constructors") - ("Hint Extern" "he" "Hint Extern @{cost} @{pat} => @{tac} : @{db}." t "Hint\\s-+Extern") - ("Hint Immediate" "hi" "Hint Immediate # : @{db}." t "Hint\\s-+Immediate") - ("Hint Resolve" "hr" "Hint Resolve # : @{db}." t "Hint\\s-+Resolve") - ("Hint Rewrite ->" "hrw" "Hint Rewrite -> @{t1,t2...} using @{tac} : @{db}." t "Hint\\s-+Rewrite") - ("Hint Rewrite <-" "hrw" "Hint Rewrite <- @{t1,t2...} using @{tac} : @{db}." t ) - ("Hint Unfold" "hu" "Hint Unfold # : #." t "Hint\\s-+Unfold") - ("Hypothesis" "hyp" "Hypothesis #: #" t "Hypothesis") - ("Hypotheses" "hyp" "Hypotheses #: #" t "Hypotheses") - ("Parameter" "par" "Parameter #: #" t "Parameter") - ("Parameters" "par" "Parameter #: #" t "Parameters") - ("Conjecture" "conj" "Conjecture #: #." t "Conjecture") - ("Variable" "v" "Variable #: #." t "Variable") - ("Variables" "vs" "Variables # , #: #." t "Variables") - ("Coercion" "coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." t "Coercion") - ) - "Coq declaration keywords information list. See `coq-syntax-db' for syntax." - ) - -(defvar coq-defn-db - '( - ("CoFixpoint" "cfix" "CoFixpoint # (#:#) : # :=\n#." t "CoFixpoint") - ("CoInductive" "coindv" "CoInductive # : # :=\n|# : #." t "CoInductive") - ("Declare Module : :=" "dm" "Declare Module # : # := #." t "Declare\\s-+Module") - ("Declare Module <: :=" "dm2" "Declare Module # <: # := #." t);; careful - ("Declare Module Import : :=" "dmi" "Declare Module # : # := #." t) - ("Declare Module Import <: :=" "dmi2" "Declare Module # <: # := #." t);; careful - ("Declare Module Export : :=" "dme" "Declare Module # : # := #." t) - ("Declare Module Export <: :=" "dme2" "Declare Module # <: # := #." t);; careful - ("Definition" "def" "Definition #:# := #." t "Definition");; careful - ("Definition (2 args)" "def2" "Definition # (# : #) (# : #):# := #." t) - ("Definition (3 args)" "def3" "Definition # (# : #) (# : #) (# : #):# := #." t) - ("Definition (4 args)" "def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." t) - ("Program Definition" "pdef" "Program Definition #:# := #." t "Program\\s-+Definition");; careful ? - ("Program Definition (2 args)" "pdef2" "Program Definition # (# : #) (# : #):# := #." t) - ("Program Definition (3 args)" "pdef3" "Program Definition # (# : #) (# : #) (# : #):# := #." t) - ("Program Definition (4 args)" "pdef4" "Program Definition # (# : #) (# : #) (# : #) (# : #):# := #." t) - ("Derive Inversion" nil "Derive Inversion @{id} with # Sort #." t "Derive\\s-+Inversion") - ("Derive Dependent Inversion" nil "Derive Dependent Inversion @{id} with # Sort #." t "Derive\\s-+Dependent\\s-+Inversion") - ("Derive Inversion_clear" nil "Derive Inversion_clear @{id} with # Sort #." t) - ("Fixpoint" "fix" "Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Fixpoint") - ("Program Fixpoint" "pfix" "Program Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t "Program\\s-+Fixpoint") - ("Program Fixpoint measure" "pfixm" "Program Fixpoint # (#:#) {measure @{arg} @{f}} : # :=\n#." t) - ("Program Fixpoint wf" "pfixwf" "Program Fixpoint # (#:#) {wf @{arg} @{f}} : # :=\n#." t) - ("Function" "func" "Function # (#:#) {struct @{arg}} : # :=\n#." t "Function") - ("Function measure" "funcm" "Function # (#:#) {measure @{f} @{arg}} : # :=\n#." t) - ("Function wf" "func wf" "Function # (#:#) {wf @{R} @{arg}} : # :=\n#." t) - ("Functional Scheme with" "fsw" "Functional Scheme @{name} := Induction for @{fun} with @{mutfuns}." t ) - ("Functional Scheme" "fs" "Functional Scheme @{name} := Induction for @{fun}." t "Functional\\s-+Scheme") - ("Inductive" "indv" "Inductive # : # := # : #." t "Inductive") - ("Inductive (2 args)" "indv2" "Inductive # : # :=\n| # : #\n| # : #." t ) - ("Inductive (3 args)" "indv3" "Inductive # : # :=\n| # : #\n| # : #\n| # : #." t ) - ("Inductive (4 args)" "indv4" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Inductive (5 args)" "indv5" "Inductive # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Variant" "indv" "Variant # : # := # : #." t "Variant") - ("Variant (2 args)" "indv2" "Variant # : # :=\n| # : #\n| # : #." t ) - ("Variant (3 args)" "indv3" "Variant # : # :=\n| # : #\n| # : #\n| # : #." t ) - ("Variant (4 args)" "indv4" "Variant # : # :=\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Variant (5 args)" "indv5" "Variant # : # :=\n| # : #\n| # : #\n| # : #\n| # : #\n| # : #." t ) - ("Let" "Let" "Let # : # := #." t "Let") - ("Ltac" "ltac" "Ltac # := #" t "Ltac") - ("Module :=" "mo" "Module # : # := #." t ) ; careful - ("Module <: :=" "mo2" "Module # <: # := #." t ) ; careful - ("Module Import :=" "moi" "Module Import # : # := #." t ) ; careful - ("Module Import <: :=" "moi2" "Module Import # <: # := #." t ) ; careful - ("Module Export :=" "moe" "Module Export # : # := #." t ) ; careful - ("Module Export <: :=" "moe2" "Module Export# <: # := #." t ) ; careful - ("Record" "rec" "Record # : # := {\n# : #;\n# : # }" t "Record") - ("Scheme" "sc" "Scheme @{name} := #." t "Scheme") - ("Scheme Induction" "sci" "Scheme @{name} := Induction for # Sort #." t) - ("Scheme Minimality" "scm" "Scheme @{name} := Minimality for # Sort #." t) - ("Structure" "str" "Structure # : # := {\n# : #;\n# : # }" t "Structure") - ) - "Coq definition keywords information list. See `coq-syntax-db' for syntax. " - ) - -;; modules and section are indented like goal starters -(defvar coq-goal-starters-db - '( - ("Add Morphism" "addmor" "Add Morphism @{f} : @{id}" t "Add\\s-+Morphism") - ("Chapter" "chp" "Chapter # : #." t "Chapter") - ("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary") - ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t) - ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t) - ("Definition goal" "defg" "Definition #:#.\n#\nQed." t);; careful - ("Fact" "fct" "Fact # : #." t "Fact") - ("Goal" nil "Goal #." t "Goal") - ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma") - ("Program Lemma" "pl" "Program Lemma # : #.\nProof.\n#\nQed." t "Program\\s-+Lemma") - ("Module! (interactive)" nil "Module # : #.\n#\nEnd #." nil nil coq-insert-section-or-module) - ("Module Type" "mti" "Module Type #.\n#\nEnd #." t "Module\\s-+Type") ; careful - ("Module :" "moi" "Module # : #.\n#\nEnd #." t "Module") ; careful - ("Module <:" "moi2" "Module # <: #.\n#\nEnd #." t ) ; careful - ("Remark" "rk" "Remark # : #.\n#\nQed." t "Remark") - ("Section" "sec" "Section #." t "Section") - ("Theorem" "th" "Theorem # : #.\n#\nQed." t "Theorem") - ("Program Theorem" "pth" "Program Theorem # : #.\nProof.\n#\nQed." t "Program\\s-+Theorem") - ("Obligation" "obl" "Obligation #.\n#\nQed." t "Obligation") - ("Next Obligation" "nobl" "Next Obligation.\n#\nQed." t "Next Obligation") - ) - "Coq goal starters keywords information list. See `coq-syntax-db' for syntax. " - ) - -;; command that are not declarations, definition or goal starters -(defvar coq-other-commands-db - '( - ;; ("Abort" nil "Abort." t "Abort" nil nil);don't appear in menu - ("About" nil "About #." nil "About") - ("Add" nil "Add #." nil "Add" nil t) - ("Add Abstract Ring" nil "Add Abstract Ring #." t "Add\\s-+Abstract\\s-+Ring") - ("Add Abstract Semi Ring" nil "Add Abstract Semi Ring #." t "Add\\s-+Abstract\\s-+Semi\\s-+Ring") - ("Add Field" nil "Add Field #." t "Add\\s-+Field") - ("Add LoadPath" nil "Add LoadPath #." nil "Add\\s-+LoadPath") - ("Add ML Path" nil "Add ML Path #." nil "Add\\s-+ML\\s-+Path") - ("Add Morphism" nil "Add Morphism #." t "Add\\s-+Morphism") - ("Add Printing" nil "Add Printing #." t "Add\\s-+Printing") - ("Add Printing Constructor" nil "Add Printing Constructor #." t "Add\\s-+Printing\\s-+Constructor") - ("Add Printing If" nil "Add Printing If #." t "Add\\s-+Printing\\s-+If") - ("Add Printing Let" nil "Add Printing Let #." t "Add\\s-+Printing\\s-+Let") - ("Add Printing Record" nil "Add Printing Record #." t "Add\\s-+Printing\\s-+Record") - ("Add Rec LoadPath" nil "Add Rec LoadPath #." nil "Add\\s-+Rec\\s-+LoadPath") - ("Add Rec ML Path" nil "Add Rec ML Path #." nil "Add\\s-+Rec\\s-+ML\\s-+Path") - ("Add Ring" nil "Add Ring #." t "Add\\s-+Ring") - ("Add Semi Ring" nil "Add Semi Ring #." t "Add\\s-+Semi\\s-+Ring") - ("Add Setoid" nil "Add Setoid #." t "Add\\s-+Setoid") - ("Admit Obligations" "oblsadmit" "Admit Obligations." nil "Admit\\s-+Obligations") - ("Bind Scope" "bndsc" "Bind Scope @{scope} with @{type}" t "Bind\\s-+Scope") - ("Canonical Structure" nil "Canonical Structure #." t "Canonical\\s-+Structure") - ("Cd" nil "Cd #." nil "Cd") - ("Check" nil "Check" nil "Check") - ("Close Local Scope" "cllsc" "Close Local Scope #" t "Close\\s-+Local\\s-+Scope") - ("Close Scope" "clsc" "Close Scope #" t "Close\\s-+Scope") - ("Comments" nil "Comments #." nil "Comments") - ("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t "Delimit\\s-+Scope" ) - ("Eval" nil "Eval #." nil "Eval") - ("Export" nil "Export #." t "Export") - ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." nil "Extract\\s-+Constant") - ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} => \"@{id}\"." nil "Extract\\s-+Inlined\\s-+Constant") - ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\" [\"@{id}\" \"@{id...}\"]." nil "Extract") - ("Extraction" "extr" "Extraction @{id}." nil "Extraction") - ("Extraction (in a file)" "extrf" "Extraction \"@{file}\" @{id}." nil) - ("Extraction Inline" nil "Extraction Inline #." t "Extraction\\s-+Inline") - ("Extraction NoInline" nil "Extraction NoInline #." t "Extraction\\s-+NoInline") - ("Extraction Language" "extrlang" "Extraction Language #." t "Extraction\\s-+Language") - ("Extraction Library" "extrl" "Extraction Library @{id}." nil "Extraction\\s-+Library") - ("Focus" nil "Focus #." nil "Focus") - ("Identity Coercion" nil "Identity Coercion #." t "Identity\\s-+Coercion") - ("Implicit Arguments Off" nil "Implicit Arguments Off." t "Implicit\\s-+Arguments\\s-+Off") - ("Implicit Arguments On" nil "Implicit Arguments On." t "Implicit\\s-+Arguments\\s-+On") - ("Implicit Arguments" nil "Implicit Arguments # [#]." t "Implicit\\s-+Arguments") - ("Import" nil "Import #." t "Import") - ("Infix" "inf" "Infix \"#\" := # (at level #) : @{scope}." t "Infix") - ("Inspect" nil "Inspect #." nil "Inspect") - ("Locate" nil "Locate" nil "Locate") - ("Locate File" nil "Locate File \"#\"." nil "Locate\\s-+File") - ("Locate Library" nil "Locate Library #." nil "Locate\\s-+Library") - ("Notation (assoc)" "notas" "Notation \"#\" := # (at level #, # associativity)." t) - ("Notation (at assoc)" "notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." t) - ("Notation (at at scope)" "notasc" "Notation \"#\" := # (at level #, # at level #) : @{scope}." t) - ("Notation (at at)" "nota" "Notation \"#\" := # (at level #, # at level #)." t) - ("Notation (only parsing)" "notsp" "Notation # := # (only parsing)." t) - ("Notation Local (only parsing)" "notslp" "Notation Local # := # (only parsing)." t) - ("Notation Local" "notsl" "Notation Local # := #." t "Notation\\s-+Local") - ("Notation (simple)" "nots" "Notation # := #." t "Notation") - ("Opaque" nil "Opaque #." nil "Opaque") - ("Obligations Tactic" nil "Obligations Tactic := #." t "Obligations\\s-+Tactic") - ("Open Local Scope" "oplsc" "Open Local Scope #" t "Open\\s-+Local\\s-+Scope") - ("Open Scope" "opsc" "Open Scope #" t "Open\\s-+Scope") - ("Print Coercions" nil "Print Coercions." nil "Print\\s-+Coercions") - ("Print Hint" nil "Print Hint." nil "Print\\s-+Hint" coq-PrintHint) - ("Print" "p" "Print #." nil "Print") - ("Qed" nil "Qed." nil "Qed") - ("Pwd" nil "Pwd." nil "Pwd") - ("Recursive Extraction" "recextr" "Recursive Extraction @{id}." nil "Recursive\\s-+Extraction") - ("Recursive Extraction Library" "recextrl" "Recursive Extraction Library @{id}." nil "Recursive\\s-+Extraction\\s-+Library") - ("Recursive Extraction Module" "recextrm" "Recursive Extraction Module @{id}." nil "Recursive\\s-+Extraction\\s-+Module") - ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") - ("Remove LoadPath" nil "Remove LoadPath" nil "Remove\\s-+LoadPath") - ("Remove Printing If" nil "Remove Printing If #." t "Remove\\s-+Printing\\s-+If") - ("Remove Printing Let" nil "Remove Printing Let #." t "Remove\\s-+Printing\\s-+Let") - ("Require Export" nil "Require Export #." t "Require\\s-+Export") - ("Require Import" nil "Require Import #." t "Require\\s-+Import") - ("Require" nil "Require #." t "Require") - ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation") - ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline") - ("Search" nil "Search #" nil "Search") - ("SearchAbout" nil "SearchAbout #" nil "SearchAbout") - ("SearchPattern" nil "SearchPattern #" nil "SearchPattern") - ("SearchRewrite" nil "SearchRewrite #" nil "SearchRewrite") - ("Set Extraction AutoInline" nil "Set Extraction AutoInline" t "Set\\s-+Extraction\\s-+AutoInline") - ("Set Extraction Optimize" nil "Set Extraction Optimize" t "Set\\s-+Extraction\\s-+Optimize") - ("Set Implicit Arguments" nil "Set Implicit Arguments" t "Set\\s-+Implicit\\s-+Arguments") - ("Set Strict Implicit" nil "Set Strict Implicit" t "Set\\s-+Strict\\s-+Implicit") - ("Set Printing Synth" nil "Set Printing Synth" t "Set\\s-+Printing\\s-+Synth") - ("Set Printing Wildcard" nil "Set Printing Wildcard" t "Set\\s-+Printing\\s-+Wildcard") - ("Set Printing All" "sprall" "Set Printing All" t "Set\\s-+Printing\\s-+All") - ("Set Printing Records" nil "Set Printing Records" t "Set\\s-+Printing\\s-+Records") - ("Set Hyps Limit" nil "Set Hyps Limit #." nil "Set\\s-+Hyps\\s-+Limit") - ("Set Printing Coercions" nil "Set Printing Coercions." t "Set\\s-+Printing\\s-+Coercions") - ("Set Printing Notations" "sprn" "Set Printing Notations" t "Set\\s-+Printing\\s-+Notations") - ("Set Undo" nil "Set Undo #." nil "Set\\s-+Undo") - ("Show" nil "Show #." nil "Show") - ("Solve Obligations" "oblssolve" "Solve Obligations using #." nil "Solve\\s-+Obligations") - ("Test" nil "Test" nil "Test" nil t) - ("Test Printing Depth" nil "Test Printing Depth." nil "Test\\s-+Printing\\s-+Depth") - ("Test Printing If" nil "Test Printing If #." nil "Test\\s-+Printing\\s-+If") - ("Test Printing Let" nil "Test Printing Let #." nil "Test\\s-+Printing\\s-+Let") - ("Test Printing Synth" nil "Test Printing Synth." nil "Test\\s-+Printing\\s-+Synth") - ("Test Printing Width" nil "Test Printing Width." nil "Test\\s-+Printing\\s-+Width") - ("Test Printing Wildcard" nil "Test Printing Wildcard." nil "Test\\s-+Printing\\s-+Wildcard") - ("Transparent" nil "Transparent #." nil "Transparent") - ("Unfocus" nil "Unfocus." nil "Unfocus") - ("Unset Extraction AutoInline" nil "Unset Extraction AutoInline" t "Unset\\s-+Extraction\\s-+AutoInline") - ("Unset Extraction Optimize" nil "Unset Extraction Optimize" t "Unset\\s-+Extraction\\s-+Optimize") - ("Unset Implicit Arguments" nil "Unset Implicit Arguments" t "Unset\\s-+Implicit\\s-+Arguments") - ("Unset Strict Implicit" nil "Unset Strict Implicit" t "Unset\\s-+Strict\\s-+Implicit") - ("Unset Printing Synth" nil "Unset Printing Synth" t "Unset\\s-+Printing\\s-+Synth") - ("Unset Printing Wildcard" nil "Unset Printing Wildcard" t "Unset\\s-+Printing\\s-+Wildcard") - ("Unset Hyps Limit" nil "Unset Hyps Limit" nil "Unset\\s-+Hyps\\s-+Limit") - ("Unset Printing All" "unsprall" "Unset Printing All" nil "Unset\\s-+Printing\\s-+All") - ("Unset Printing Coercion" nil "Unset Printing Coercion #." t "Unset\\s-+Printing\\s-+Coercion") - ("Unset Printing Coercions" nil "Unset Printing Coercions." nil "Unset\\s-+Printing\\s-+Coercions") - ("Unset Printing Notations" "unsprn" "Unset Printing Notations" nil "Unset\\s-+Printing\\s-+Notations") - ("Unset Undo" nil "Unset Undo." nil "Unset\\s-+Undo") - ; ("print" "pr" "print #" "print") - ) - "Command that are not declarations, definition or goal starters." - ) - -(defvar coq-commands-db - (append coq-decl-db coq-defn-db coq-goal-starters-db - coq-other-commands-db coq-user-commands-db) - "Coq all commands keywords information list. See `coq-syntax-db' for syntax. " - ) - - -(defvar coq-terms-db - '( - ("fun (1 args)" "f" "fun #:# => #" nil "fun") - ("fun (2 args)" "f2" "fun (#:#) (#:#) => #") - ("fun (3 args)" "f3" "fun (#:#) (#:#) (#:#) => #") - ("fun (4 args)" "f4" "fun (#:#) (#:#) (#:#) (#:#) => #") - ("forall" "fo" "forall #:#,#" nil "forall") - ("forall (2 args)" "fo2" "forall (#:#) (#:#), #") - ("forall (3 args)" "fo3" "forall (#:#) (#:#) (#:#), #") - ("forall (4 args)" "fo4" "forall (#:#) (#:#) (#:#) (#:#), #") - ("if" "if" "if # then # else #" nil "if") - ("let in" "li" "let # := # in #" nil "let") - ("match! (from type)" nil "" nil "match" coq-insert-match) - ("match with" "m" "match # with\n| # => #\nend") - ("match with 2" "m2" "match # with\n| # => #\n| # => #\nend") - ("match with 3" "m3" "match # with\n| # => #\n| # => #\n| # => #\nend") - ("match with 4" "m4" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\nend") - ("match with 5" "m5" "match # with\n| # => #\n| # => #\n| # => #\n| # => #\n| # => #\nend") - ) - "Coq terms keywords information list. See `coq-syntax-db' for syntax. " - ) - - - - - - - - ;;; Goals (and module/sections) starters detection - - -;; ----- keywords for font-lock. - -;; FIXME da: this one function breaks the nice configuration of Proof General: -;; would like to have proof-goal-regexp instead. -;; Unfortunately Coq allows "Definition" and friends to perhaps have a goal, -;; so it appears more difficult than just a proof-goal-regexp setting. -;; Future improvement may simply to be allow a function value for -;; proof-goal-regexp. - -;; FIXME Pierre: the right way IMHO here would be to set a span -;; property 'goalcommand when coq prompt says it (if the name of -;; current proof has changed). - -;; excerpt of Jacek Chrzaszcz, implementer of the module system: sorry -;; for the french: -;;*) suivant les suggestions de Chritine, pas de mode preuve dans un type de -;; module (donc pas de Definition truc:machin. Lemma, Theorem ... ) -;; -;; *) la commande Module M [ ( : | <: ) MTYP ] [ := MEXPR ] est valable -;; uniquement hors d'un MT -;; - si :=MEXPR est absent, elle demarre un nouveau module interactif -;; - si :=MEXPR est present, elle definit un module -;; (la fonction vernac_define_module dans toplevel/vernacentries) -;; -;; *) la nouvelle commande Declare Module M [ ( : | <: ) MTYP ] [ := MEXPR ] -;; est valable uniquement dans un MT -;; - si :=MEXPR absent, :MTYP absent, elle demarre un nouveau module -;; interactif -;; - si (:=MEXPR absent, :MTYP present) -;; ou (:=MEXPR present, :MTYP absent) -;; elle declare un module. -;; (la fonction vernac_declare_module dans toplevel/vernacentries) - -(defun coq-count-match (regexp strg) - "Count the number of (maximum, non overlapping) matching substring - of STRG matching REGEXP. Empty match are counted once." - (let ((nbmatch 0) (str strg)) - (while (and (proof-string-match regexp str) (not (string-equal str ""))) - (incf nbmatch) - (if (= (match-end 0) 0) (setq str (substring str 1)) - (setq str (substring str (match-end 0))))) - nbmatch)) - -;; This function is used for amalgamating a proof into a single -;; goal-save region (proof-goal-command-p used in -;; proof-done-advancing-save in generic/proof-script.el) for coq < -;; 8.0. It is the test when looking backward the start of the proof. -;; It is NOT used for coq > v8.1 -;; (coq-find-and-forget in gallina.el uses state numbers, proof numbers and -;; lemma names given in the prompt) - -;; compatibility with v8.0, will delete it some day -(defun coq-goal-command-str-v80-p (str) - "See `coq-goal-command-p'." - (let* ((match (coq-count-match "\\<match\\>" str)) - (with (coq-count-match "\\<with\\>" str)) - (letwith (+ (coq-count-match "\\<let\\>" str) (- with match))) - (affect (coq-count-match ":=" str))) - - (and (proof-string-match coq-goal-command-regexp str) - (not ; - (and - (proof-string-match "\\`\\(Local\\|Definition\\|Lemma\\|Module\\)\\>" str) - (not (= letwith affect)))) - (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str)) - ) - ) - ) - -;; Module and or section openings are detected syntactically. Module -;; *openings* are difficult to detect because there can be Module -;; ...with X := ... . So we need to count :='s to detect real openings. - -;; TODO: have opened section/chapter in the prompt too, and get rid of -;; syntactical tests everywhere -(defun coq-module-opening-p (str) - "Decide whether STR is a module or section opening or not. -Used by `coq-goal-command-p'" - (let* ((match (coq-count-match "\\<match\\>" str)) - (with (coq-count-match "\\<with\\>" str)) - (letwith (+ (coq-count-match "\\<let\\>" str) (- with match))) - (affect (coq-count-match ":=" str))) - (and (proof-string-match "\\`\\(Module\\)\\>" str) - (= letwith affect)) - )) - -(defun coq-section-command-p (str) - (proof-string-match "\\`\\(Section\\|Chapter\\)\\>" str)) - - -(defun coq-goal-command-str-v81-p (str) - "Decide syntactically whether STR is a goal start or not. Use - `coq-goal-command-p-v81' on a span instead if possible." - (coq-goal-command-str-v80-p str) - ) - -;; This is the function that tests if a SPAN is a goal start. All it -;; has to do is look at the 'goalcmd attribute of the span. -;; It also looks if this is not a module start. - -;; TODO: have also attributes 'modulecmd and 'sectioncmd. This needs -;; something in the coq prompt telling the name of all opened modules -;; (like for open goals), and use it to set goalcmd --> no more need -;; to look at Modules and section (actually indentation will still -;; need it) -(defun coq-goal-command-p-v81 (span) - "see `coq-goal-command-p'" - (or (span-property span 'goalcmd) - ;; module and section starts are detected here - (let ((str (or (span-property span 'cmd) ""))) - (or (coq-section-command-p str) - (coq-module-opening-p str)) - ))) - -;; In coq > 8.1 This is used only for indentation. -(defun coq-goal-command-str-p (str) - "Decide whether argument is a goal or not. Use - `coq-goal-command-p' on a span instead if posible." - (cond - (coq-version-is-V8-1 (coq-goal-command-str-v81-p str)) - (coq-version-is-V8-0 (coq-goal-command-str-v80-p str)) - (t (coq-goal-command-str-v80-p str));; this is temporary - )) - -;; This is used for backtracking -(defun coq-goal-command-p (span) - "Decide whether argument is a goal or not." - (cond - (coq-version-is-V8-1 (coq-goal-command-p-v81 span)) - (coq-version-is-V8-0 (coq-goal-command-str-v80-p (span-property span 'cmd))) - (t (coq-goal-command-str-v80-p (span-property span 'cmd)));; this is temporary - )) - -(defvar coq-keywords-save-strict - '("Defined" - "Qed" - "End" - "Admitted" - "Abort" - )) - -(defvar coq-keywords-save - (append coq-keywords-save-strict '("Proof")) - ) - -(defun coq-save-command-p (span str) - "Decide whether argument is a Save command or not" - (or (proof-string-match coq-save-command-regexp-strict str) - (and (proof-string-match "\\`Proof\\>" str) - (not (proof-string-match "Proof\\s-*\\(\\.\\|\\<with\\>\\)" str))) - ) - ) - - -(defvar coq-keywords-kill-goal - '("Abort")) - -;; Following regexps are all state changing -(defvar coq-keywords-state-changing-misc-commands - (coq-build-regexp-list-from-db coq-commands-db 'filter-state-changing)) - -(defvar coq-keywords-goal - (coq-build-regexp-list-from-db coq-goal-starters-db)) - -(defvar coq-keywords-decl - (coq-build-regexp-list-from-db coq-decl-db)) - -(defvar coq-keywords-defn - (coq-build-regexp-list-from-db coq-defn-db)) - - -(defvar coq-keywords-state-changing-commands - (append - coq-keywords-state-changing-misc-commands - coq-keywords-decl ; all state changing - coq-keywords-defn ; idem - coq-keywords-goal)) ; idem - - -;; -(defvar coq-keywords-state-preserving-commands - (coq-build-regexp-list-from-db coq-commands-db 'filter-state-preserving)) - -;; concat this is faster that redoing coq-build-regexp-list-from-db on -;; whole commands-db -(defvar coq-keywords-commands - (append coq-keywords-state-changing-commands - coq-keywords-state-preserving-commands) - "All commands keyword.") - -(defvar coq-solve-tactics - (coq-build-regexp-list-from-db coq-solve-tactics-db) - "Keywords for closing tactic(al)s.") - -(defvar coq-tacticals - (coq-build-regexp-list-from-db coq-tacticals-db) - "Keywords for tacticals in a Coq script.") - - - ;; From JF Monin: -(defvar coq-reserved - (append - coq-user-reserved-db - '( - "False" "True" "after" "as" "cofix" "fix" "forall" "fun" "match" - "return" "struct" "else" "end" "if" "in" "into" "let" "then" - "using" "with" "beta" "delta" "iota" "zeta" "after" "until" - "at" "Sort" "Time")) - "Reserved keywords of Coq.") - - -(defvar coq-state-changing-tactics - (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-changing)) - -(defvar coq-state-preserving-tactics - (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-preserving)) - - -(defvar coq-tactics - (append coq-state-changing-tactics coq-state-preserving-tactics)) - -(defvar coq-retractable-instruct - (append coq-state-changing-tactics coq-keywords-state-changing-commands)) - -(defvar coq-non-retractable-instruct - (append coq-state-preserving-tactics - coq-keywords-state-preserving-commands)) - -(defvar coq-keywords - (append coq-keywords-goal coq-keywords-save coq-keywords-decl - coq-keywords-defn coq-keywords-commands) - "All keywords in a Coq script.") - - - -(defvar coq-symbols - '("|" - "||" - ":" - ";" - "," - "(" - ")" - "[" - "]" - "{" - "}" - ":=" - "=>" - "->" - ".") - "Punctuation Symbols used by Coq.") - -;; ----- regular expressions -(defvar coq-error-regexp "^\\(Error:\\|Discarding pattern\\|Syntax error:\\|System Error:\\|User Error:\\|User error:\\|Anomaly[:.]\\|Toplevel input[,]\\)" - "A regexp indicating that the Coq process has identified an error.") - -(defvar coq-id proof-id) -(defvar coq-id-shy "\\(?:\\w\\(?:\\w\\|\\s_\\)*\\)") - -(defvar coq-ids (proof-ids coq-id " ")) - -(defun coq-first-abstr-regexp (paren end) - (concat paren "\\s-*\\(" coq-ids "\\)\\s-*" end)) - -(defcustom coq-variable-highlight-enable t - "Activates partial bound variable highlighting" - :type 'boolean - :group 'coq) - - -(defvar coq-font-lock-terms - (if coq-variable-highlight-enable - (list - ;; lambda binders - (list (coq-first-abstr-regexp "\\<fun\\>" "\\(?:=>\\|:\\)") 1 'font-lock-variable-name-face) - ;; forall binder - (list (coq-first-abstr-regexp "\\<forall\\>" "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face) - ; (list "\\<forall\\>" - ; (list 0 font-lock-type-face) - ; (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil - ; (list 0 font-lock-variable-name-face))) - ;; parenthesized binders - (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face) - )) - "*Font-lock table for Coq terms.") - - - -;; According to Coq, "Definition" is both a declaration and a goal. -;; It is understood here as being a goal. This is important for -;; recognizing global identifiers, see coq-global-p. -(defconst coq-save-command-regexp-strict - (proof-anchor-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict) - "\\)"))) -(defconst coq-save-command-regexp - (proof-anchor-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save) - "\\)"))) -(defconst coq-save-with-hole-regexp - (concat "\\(Time\\s-+\\|\\)\\(" (proof-ids-to-regexp coq-keywords-save-strict) - "\\)\\s-+\\(" coq-id "\\)\\s-*\\.")) - -(defconst coq-goal-command-regexp - (proof-anchor-regexp (proof-ids-to-regexp coq-keywords-goal))) - -(defconst coq-goal-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-goal) - "\\)\\s-+\\(" coq-id "\\)\\s-*:?")) - -(defconst coq-decl-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-decl) - "\\)\\s-+\\(" coq-ids "\\)\\s-*:")) - -;; (defconst coq-decl-with-hole-regexp -;; (if coq-variable-highlight-enable coq-decl-with-hole-regexp-1 'nil)) - -(defconst coq-defn-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp coq-keywords-defn) - "\\)\\s-+\\(" coq-id "\\)")) - -;; must match: -;; "with f x y :" (followed by = or not) -;; "with f x y (z:" (not followed by =) -;; BUT NOT: -;; "with f ... (x:=" -;; "match ... with .. => " -(defconst coq-with-with-hole-regexp - (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^=(.]*:\\|[^(]*(\\s-*" - coq-id "\\s-*:[^=]\\)")) -;; marche aussi a peu pres -;; (concat "\\(with\\)\\s-+\\(" coq-id "\\)\\s-*\\([^(.]*:\\|.*)[^(.]*:=\\)")) -;;"\\<Prop\\>\\|\\<Set\\>\\|\\<Type\\>" -(defvar coq-font-lock-keywords-1 - (append - coq-font-lock-terms - (list - (cons (proof-ids-to-regexp coq-solve-tactics) 'coq-solve-tactics-face) - (cons (proof-ids-to-regexp coq-keywords) 'font-lock-keyword-face) - (cons (proof-ids-to-regexp coq-reserved) 'font-lock-type-face) - (cons (proof-ids-to-regexp coq-tactics ) 'proof-tactics-name-face) - (cons (proof-ids-to-regexp coq-tacticals) 'proof-tacticals-name-face) - (cons (proof-ids-to-regexp (list "Set" "Type" "Prop")) 'font-lock-type-face) - (cons "============================" 'font-lock-keyword-face) - (cons "Subtree proved!" 'font-lock-keyword-face) - (cons "subgoal [0-9]+ is:" 'font-lock-keyword-face) - (list "^\\([^ \n]+\\) \\(is defined\\)" - (list 2 'font-lock-keyword-face t) - (list 1 'font-lock-function-name-face t)) - - (list coq-goal-with-hole-regexp 2 'font-lock-function-name-face)) - (if coq-variable-highlight-enable (list (list coq-decl-with-hole-regexp 2 'font-lock-variable-name-face))) - (list - (list coq-defn-with-hole-regexp 2 'font-lock-function-name-face) - (list coq-with-with-hole-regexp 2 'font-lock-function-name-face) - (list coq-save-with-hole-regexp 2 'font-lock-function-name-face) - ;; Remove spurious variable and function faces on commas. - '(proof-zap-commas)))) - -(defvar coq-font-lock-keywords coq-font-lock-keywords-1) - -(defun coq-init-syntax-table () - "Set appropriate values for syntax table in current buffer." - - (modify-syntax-entry ?\$ ".") - (modify-syntax-entry ?\/ ".") - (modify-syntax-entry ?\\ ".") - (modify-syntax-entry ?+ ".") - (modify-syntax-entry ?- ".") - (modify-syntax-entry ?= ".") - (modify-syntax-entry ?% ".") - (modify-syntax-entry ?< ".") - (modify-syntax-entry ?> ".") - (modify-syntax-entry ?\& ".") - (modify-syntax-entry ?_ "_") - (modify-syntax-entry ?\' "_") - (modify-syntax-entry ?\| ".") - -;; should maybe be "_" but it makes coq-find-and-forget (in gallina.el) bug - (modify-syntax-entry ?\. ".") - - (condition-case nil - ;; Try to use Emacs-21's nested comments. - (modify-syntax-entry ?\* ". 23n") - ;; Revert to non-nested comments if that failed. - (error (modify-syntax-entry ?\* ". 23"))) - (modify-syntax-entry ?\( "()1") - (modify-syntax-entry ?\) ")(4")) - - -(defconst coq-generic-expression - (mapcar (lambda (kw) - (list (capitalize kw) - (concat "\\<" kw "\\>" "\\s-+\\(\\w+\\)\\W" ) - 1)) - (append coq-keywords-decl coq-keywords-defn coq-keywords-goal))) - -(provide 'gallina-syntax) - ;;; gallina-syntax.el ends here - -; Local Variables: *** -; indent-tabs-mode: nil *** -; End: *** diff --git a/tools/gallina.el b/tools/gallina.el deleted file mode 100644 index cbc13118a..000000000 --- a/tools/gallina.el +++ /dev/null @@ -1,142 +0,0 @@ -;; gallina.el --- Coq mode editing commands for Emacs -;; -;; Jean-Christophe Filliatre, march 1995 -;; Shamelessly copied from caml.el, Xavier Leroy, july 1993. -;; -;; modified by Marco Maggesi <maggesi@math.unifi.it> for gallina-inferior - -; compatibility code for proofgeneral files -(require 'coq-font-lock) -; ProofGeneral files. remember to remove coq version tests in -; gallina-syntax.el -(require 'gallina-syntax) - -(defvar coq-mode-map nil - "Keymap used in Coq mode.") -(if coq-mode-map - () - (setq coq-mode-map (make-sparse-keymap)) - (define-key coq-mode-map "\t" 'coq-indent-command) - (define-key coq-mode-map "\M-\t" 'coq-unindent-command) - (define-key coq-mode-map "\C-c\C-c" 'compile) -) - -(defvar coq-mode-syntax-table nil - "Syntax table in use in Coq mode buffers.") -(if coq-mode-syntax-table - () - (setq coq-mode-syntax-table (make-syntax-table)) - ; ( is first character of comment start - (modify-syntax-entry ?\( "()1" coq-mode-syntax-table) - ; * is second character of comment start, - ; and first character of comment end - (modify-syntax-entry ?* ". 23" coq-mode-syntax-table) - ; ) is last character of comment end - (modify-syntax-entry ?\) ")(4" coq-mode-syntax-table) - ; quote is a string-like delimiter (for character literals) - (modify-syntax-entry ?' "\"" coq-mode-syntax-table) - ; quote is part of words - (modify-syntax-entry ?' "w" coq-mode-syntax-table) -) - -(defvar coq-mode-indentation 2 - "*Indentation for each extra tab in Coq mode.") - -(defun coq-mode-variables () - (set-syntax-table coq-mode-syntax-table) - (make-local-variable 'paragraph-start) - (setq paragraph-start (concat "^$\\|" page-delimiter)) - (make-local-variable 'paragraph-separate) - (setq paragraph-separate paragraph-start) - (make-local-variable 'paragraph-ignore-fill-prefix) - (setq paragraph-ignore-fill-prefix t) - (make-local-variable 'require-final-newline) - (setq require-final-newline t) - (make-local-variable 'comment-start) - (setq comment-start "(* ") - (make-local-variable 'comment-end) - (setq comment-end " *)") - (make-local-variable 'comment-column) - (setq comment-column 40) - (make-local-variable 'comment-start-skip) - (setq comment-start-skip "(\\*+ *") - (make-local-variable 'parse-sexp-ignore-comments) - (setq parse-sexp-ignore-comments nil) - (make-local-variable 'indent-line-function) - (setq indent-line-function 'coq-indent-command) - (make-local-variable 'font-lock-keywords) - (setq font-lock-defaults '(coq-font-lock-keywords-1))) - -;;; The major mode - -(defun coq-mode () - "Major mode for editing Coq code. -Tab at the beginning of a line indents this line like the line above. -Extra tabs increase the indentation level. -\\{coq-mode-map} -The variable coq-mode-indentation indicates how many spaces are -inserted for each indentation level." - (interactive) - (kill-all-local-variables) - (setq major-mode 'coq-mode) - (setq mode-name "coq") - (use-local-map coq-mode-map) - (coq-mode-variables) - (run-hooks 'coq-mode-hook)) - -;;; Indentation stuff - -(defun coq-in-indentation () - "Tests whether all characters between beginning of line and point -are blanks." - (save-excursion - (skip-chars-backward " \t") - (bolp))) - -(defun coq-indent-command () - "Indent the current line in Coq mode. -When the point is at the beginning of an empty line, indent this line like -the line above. -When the point is at the beginning of an indented line -\(i.e. all characters between beginning of line and point are blanks\), -increase the indentation by one level. -The indentation size is given by the variable coq-mode-indentation. -In all other cases, insert a tabulation (using insert-tab)." - (interactive) - (let* ((begline - (save-excursion - (beginning-of-line) - (point))) - (current-offset - (- (point) begline)) - (previous-indentation - (save-excursion - (if (eq (forward-line -1) 0) (current-indentation) 0)))) - (cond ((and (bolp) - (looking-at "[ \t]*$") - (> previous-indentation 0)) - (indent-to previous-indentation)) - ((coq-in-indentation) - (indent-to (+ current-offset coq-mode-indentation))) - (t - (insert-tab))))) - -(defun coq-unindent-command () - "Decrease indentation by one level in Coq mode. -Works only if the point is at the beginning of an indented line -\(i.e. all characters between beginning of line and point are blanks\). -Does nothing otherwise." - (interactive) - (let* ((begline - (save-excursion - (beginning-of-line) - (point))) - (current-offset - (- (point) begline))) - (if (and (>= current-offset coq-mode-indentation) - (coq-in-indentation)) - (backward-delete-char-untabify coq-mode-indentation)))) - -;;; gallina.el ends here - -(provide 'gallina) diff --git a/tools/gallina.ml b/tools/gallina.ml deleted file mode 100644 index c7ff76bec..000000000 --- a/tools/gallina.ml +++ /dev/null @@ -1,63 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Gallina_lexer - -let vfiles = ref ([] : string list) - -let option_moins = ref false - -let option_stdout = ref false - -let traite_fichier f = - try - let chan_in = open_in (f^".v") in - let buf = Lexing.from_channel chan_in in - if not !option_stdout then chan_out := open_out (f ^ ".g"); - try - while true do Gallina_lexer.action buf done - with Fin_fichier -> begin - flush !chan_out; - close_in chan_in; - if not !option_stdout then close_out !chan_out - end - with Sys_error _ -> - () - -let traite_stdin () = - try - let buf = Lexing.from_channel stdin in - try - while true do Gallina_lexer.action buf done - with Fin_fichier -> - flush !chan_out - with Sys_error _ -> - () - -let _ = - let lg_command = Array.length Sys.argv in - if lg_command < 2 then begin - output_string stderr "Usage: gallina [-] [-stdout] file1 file2 ...\n"; - flush stderr; - exit 1 - end; - let treat = function - | "-" -> option_moins := true - | "-stdout" -> option_stdout := true - | "-nocomments" -> comments := false - | f -> - if Filename.check_suffix f ".v" then - vfiles := (Filename.chop_suffix f ".v") :: !vfiles - in - Array.iter treat Sys.argv; - if !option_moins then - traite_stdin () - else - List.iter traite_fichier !vfiles diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll deleted file mode 100644 index 1a594aebb..000000000 --- a/tools/gallina_lexer.mll +++ /dev/null @@ -1,126 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -{ - - let chan_out = ref stdout - - let comment_depth = ref 0 - let cRcpt = ref 0 - let comments = ref true - let print s = output_string !chan_out s - - exception Fin_fichier - -} - -let space = [' ' '\t' '\n' '\r'] -let enddot = '.' (' ' | '\t' | '\n' | '\r' | eof) - -rule action = parse - | "Theorem" space { print "Theorem "; body lexbuf; - cRcpt := 1; action lexbuf } - | "Lemma" space { print "Lemma "; body lexbuf; - cRcpt := 1; action lexbuf } - | "Fact" space { print "Fact "; body lexbuf; - cRcpt := 1; action lexbuf } - | "Remark" space { print "Remark "; body lexbuf; - cRcpt := 1; action lexbuf } - | "Goal" space { print "Goal "; body lexbuf; - cRcpt := 1; action lexbuf } - | "Correctness" space { print "Correctness "; body_pgm lexbuf; - cRcpt := 1; action lexbuf } - | "Definition" space { print "Definition "; body_def lexbuf; - cRcpt := 1; action lexbuf } - | "Hint" space { skip_until_point lexbuf ; action lexbuf } - | "Hints" space { skip_until_point lexbuf ; action lexbuf } - | "Transparent" space { skip_until_point lexbuf ; action lexbuf } - | "Immediate" space { skip_until_point lexbuf ; action lexbuf } - | "Syntax" space { skip_until_point lexbuf ; action lexbuf } - | "(*" { (if !comments then print "(*"); - comment_depth := 1; - comment lexbuf; - cRcpt := 0; action lexbuf } - | [' ' '\t']* '\n' { if !cRcpt < 2 then print "\n"; - cRcpt := !cRcpt+1; action lexbuf} - | eof { (raise Fin_fichier : unit)} - | _ { print (Lexing.lexeme lexbuf); cRcpt := 0; action lexbuf } - -and comment = parse - | "(*" { (if !comments then print "(*"); - comment_depth := succ !comment_depth; comment lexbuf } - | "*)" { (if !comments then print "*)"); - comment_depth := pred !comment_depth; - if !comment_depth > 0 then comment lexbuf } - | "*)" [' ''\t']*'\n' { (if !comments then print (Lexing.lexeme lexbuf)); - comment_depth := pred !comment_depth; - if !comment_depth > 0 then comment lexbuf } - | eof { raise Fin_fichier } - | _ { (if !comments then print (Lexing.lexeme lexbuf)); - comment lexbuf } - -and skip_comment = parse - | "(*" { comment_depth := succ !comment_depth; skip_comment lexbuf } - | "*)" { comment_depth := pred !comment_depth; - if !comment_depth > 0 then skip_comment lexbuf } - | eof { raise Fin_fichier } - | _ { skip_comment lexbuf } - -and body_def = parse - | [^'.']* ":=" { print (Lexing.lexeme lexbuf); () } - | _ { print (Lexing.lexeme lexbuf); body lexbuf } - -and body = parse - | enddot { print ".\n"; skip_proof lexbuf } - | ":=" { print ".\n"; skip_proof lexbuf } - | "(*" { print "(*"; comment_depth := 1; - comment lexbuf; body lexbuf } - | eof { raise Fin_fichier } - | _ { print (Lexing.lexeme lexbuf); body lexbuf } - -and body_pgm = parse - | enddot { print ".\n"; skip_proof lexbuf } - | "(*" { print "(*"; comment_depth := 1; - comment lexbuf; body_pgm lexbuf } - | eof { raise Fin_fichier } - | _ { print (Lexing.lexeme lexbuf); body_pgm lexbuf } - -and skip_until_point = parse - | '.' '\n' { () } - | enddot { end_of_line lexbuf } - | "(*" { comment_depth := 1; - skip_comment lexbuf; skip_until_point lexbuf } - | eof { raise Fin_fichier } - | _ { skip_until_point lexbuf } - -and end_of_line = parse - | [' ' '\t' ]* { end_of_line lexbuf } - | '\n' { () } - | eof { raise Fin_fichier } - | _ { print (Lexing.lexeme lexbuf) } - -and skip_proof = parse - | "Save" space - { skip_until_point lexbuf } - | "Qed." { end_of_line lexbuf } - | "Qed" space - { skip_until_point lexbuf } - | "Defined." { end_of_line lexbuf } - | "Defined" space - { skip_until_point lexbuf } - | "Abort." { end_of_line lexbuf } - | "Abort" space - { skip_until_point lexbuf } - | "Proof" space { skip_until_point lexbuf } - | "Proof" [' ' '\t']* '.' { skip_proof lexbuf } - | "(*" { comment_depth := 1; - skip_comment lexbuf; skip_proof lexbuf } - | eof { raise Fin_fichier } - | _ { skip_proof lexbuf } diff --git a/tools/inferior-coq.el b/tools/inferior-coq.el deleted file mode 100644 index 453bd1391..000000000 --- a/tools/inferior-coq.el +++ /dev/null @@ -1,324 +0,0 @@ -;;; inferior-coq.el --- Run an inferior Coq process. -;;; -;;; Copyright (C) Marco Maggesi <maggesi@math.unifi.it> -;;; Time-stamp: "2002-02-28 12:15:04 maggesi" - - -;; Emacs Lisp Archive Entry -;; Filename: inferior-coq.el -;; Version: 1.0 -;; Keywords: process coq -;; Author: Marco Maggesi <maggesi@math.unifi.it> -;; Maintainer: Marco Maggesi <maggesi@math.unifi.it> -;; Description: Run an inferior Coq process. -;; URL: http://www.math.unifi.it/~maggesi/ -;; Compatibility: Emacs20, Emacs21, XEmacs21 - -;; This is free software; you can redistribute it and/or modify it under -;; the terms of the GNU General Public License as published by the Free -;; Software Foundation; either version 2, or (at your option) any later -;; version. -;; -;; This is distributed in the hope that it will be useful, but WITHOUT -;; ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or -;; FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -;; for more details. -;; -;; You should have received a copy of the GNU General Public License -;; along with GNU Emacs; see the file COPYING. If not, write to the -;; Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, -;; MA 02111-1307, USA. - -;;; Commentary: - -;; Coq is a proof assistant (http://coq.inria.fr/). This code run an -;; inferior Coq process and defines functions to send bits of code -;; from other buffers to the inferior process. This is a -;; customisation of comint-mode (see comint.el). For a more complex -;; and full featured Coq interface under Emacs look at Proof General -;; (http://zermelo.dcs.ed.ac.uk/~proofgen/). -;; -;; Written by Marco Maggesi <maggesi@math.unifi.it> with code heavly -;; borrowed from emacs cmuscheme.el -;; -;; Please send me bug reports, bug fixes, and extensions, so that I can -;; merge them into the master source. - -;;; Installation: - -;; You need to have gallina.el already installed (it comes with the -;; standard Coq distribution) in order to use this code. Put this -;; file somewhere in you load-path and add the following lines in your -;; "~/.emacs": -;; -;; (setq auto-mode-alist (cons '("\\.v$" . coq-mode) auto-mode-alist)) -;; (autoload 'coq-mode "gallina" "Major mode for editing Coq vernacular." t) -;; (autoload 'run-coq "inferior-coq" "Run an inferior Coq process." t) -;; (autoload 'run-coq-other-window "inferior-coq" -;; "Run an inferior Coq process in a new window." t) -;; (autoload 'run-coq-other-frame "inferior-coq" -;; "Run an inferior Coq process in a new frame." t) - -;;; Usage: - -;; Call `M-x "run-coq'. -;; -;; Functions and key bindings (Learn more keys with `C-c C-h' or `C-h m'): -;; C-return ('M-x coq-send-line) send the current line. -;; C-c C-r (`M-x coq-send-region') send the current region. -;; C-c C-a (`M-x coq-send-abort') send the command "Abort". -;; C-c C-t (`M-x coq-send-restart') send the command "Restart". -;; C-c C-s (`M-x coq-send-show') send the command "Show". -;; C-c C-u (`M-x coq-send-undo') send the command "Undo". -;; C-c C-v (`M-x coq-check-region') run command "Check" on region. -;; C-c . (`M-x coq-come-here') Restart and send until current point. - -;;; Change Log: - -;; From -0.0 to 1.0 brought into existence. - - -(require 'gallina) -(require 'comint) - -(setq coq-program-name "coqtop") - -(defgroup inferior-coq nil - "Run a coq process in a buffer." - :group 'coq) - -(defcustom inferior-coq-mode-hook nil - "*Hook for customising inferior-coq mode." - :type 'hook - :group 'coq) - -(defvar inferior-coq-mode-map - (let ((m (make-sparse-keymap))) - (define-key m "\C-c\C-r" 'coq-send-region) - (define-key m "\C-c\C-a" 'coq-send-abort) - (define-key m "\C-c\C-t" 'coq-send-restart) - (define-key m "\C-c\C-s" 'coq-send-show) - (define-key m "\C-c\C-u" 'coq-send-undo) - (define-key m "\C-c\C-v" 'coq-check-region) - m)) - -;; Install the process communication commands in the coq-mode keymap. -(define-key coq-mode-map [(control return)] 'coq-send-line) -(define-key coq-mode-map "\C-c\C-r" 'coq-send-region) -(define-key coq-mode-map "\C-c\C-a" 'coq-send-abort) -(define-key coq-mode-map "\C-c\C-t" 'coq-send-restart) -(define-key coq-mode-map "\C-c\C-s" 'coq-send-show) -(define-key coq-mode-map "\C-c\C-u" 'coq-send-undo) -(define-key coq-mode-map "\C-c\C-v" 'coq-check-region) -(define-key coq-mode-map "\C-c." 'coq-come-here) - -(defvar coq-buffer) - -(define-derived-mode inferior-coq-mode comint-mode "Inferior Coq" - "\ -Major mode for interacting with an inferior Coq process. - -The following commands are available: -\\{inferior-coq-mode-map} - -A Coq process can be fired up with M-x run-coq. - -Customisation: Entry to this mode runs the hooks on comint-mode-hook -and inferior-coq-mode-hook (in that order). - -You can send text to the inferior Coq process from other buffers -containing Coq source. - -Functions and key bindings (Learn more keys with `C-c C-h'): - C-return ('M-x coq-send-line) send the current line. - C-c C-r (`M-x coq-send-region') send the current region. - C-c C-a (`M-x coq-send-abort') send the command \"Abort\". - C-c C-t (`M-x coq-send-restart') send the command \"Restart\". - C-c C-s (`M-x coq-send-show') send the command \"Show\". - C-c C-u (`M-x coq-send-undo') send the command \"Undo\". - C-c C-v (`M-x coq-check-region') run command \"Check\" on region. - C-c . (`M-x coq-come-here') Restart and send until current point. -" - ;; Customise in inferior-coq-mode-hook - (setq comint-prompt-regexp "^[^<]* < *") - (coq-mode-variables) - (setq mode-line-process '(":%s")) - (setq comint-input-filter (function coq-input-filter)) - (setq comint-get-old-input (function coq-get-old-input))) - -(defcustom inferior-coq-filter-regexp "\\`\\s *\\S ?\\S ?\\s *\\'" - "*Input matching this regexp are not saved on the history list. -Defaults to a regexp ignoring all inputs of 0, 1, or 2 letters." - :type 'regexp - :group 'inferior-coq) - -(defun coq-input-filter (str) - "Don't save anything matching `inferior-coq-filter-regexp'." - (not (string-match inferior-coq-filter-regexp str))) - -(defun coq-get-old-input () - "Snarf the sexp ending at point." - (save-excursion - (let ((end (point))) - (backward-sexp) - (buffer-substring (point) end)))) - -(defun coq-args-to-list (string) - (let ((where (string-match "[ \t]" string))) - (cond ((null where) (list string)) - ((not (= where 0)) - (cons (substring string 0 where) - (coq-args-to-list (substring string (+ 1 where) - (length string))))) - (t (let ((pos (string-match "[^ \t]" string))) - (if (null pos) - nil - (coq-args-to-list (substring string pos - (length string))))))))) - -;;;###autoload -(defun run-coq (cmd) - "Run an inferior Coq process, input and output via buffer *coq*. -If there is a process already running in `*coq*', switch to that buffer. -With argument, allows you to edit the command line (default is value -of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' -\(after the `comint-mode-hook' is run). -\(Type \\[describe-mode] in the process buffer for a list of commands.)" - - (interactive (list (if current-prefix-arg - (read-string "Run Coq: " coq-program-name) - coq-program-name))) - (if (not (comint-check-proc "*coq*")) - (let ((cmdlist (coq-args-to-list cmd))) - (set-buffer (apply 'make-comint "coq" (car cmdlist) - nil (cdr cmdlist))) - (inferior-coq-mode))) - (setq coq-program-name cmd) - (setq coq-buffer "*coq*") - (switch-to-buffer "*coq*")) -;;;###autoload (add-hook 'same-window-buffer-names "*coq*") - -;;;###autoload -(defun run-coq-other-window (cmd) - "Run an inferior Coq process, input and output via buffer *coq*. -If there is a process already running in `*coq*', switch to that buffer. -With argument, allows you to edit the command line (default is value -of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' -\(after the `comint-mode-hook' is run). -\(Type \\[describe-mode] in the process buffer for a list of commands.)" - - (interactive (list (if current-prefix-arg - (read-string "Run Coq: " coq-program-name) - coq-program-name))) - (if (not (comint-check-proc "*coq*")) - (let ((cmdlist (coq-args-to-list cmd))) - (set-buffer (apply 'make-comint "coq" (car cmdlist) - nil (cdr cmdlist))) - (inferior-coq-mode))) - (setq coq-program-name cmd) - (setq coq-buffer "*coq*") - (pop-to-buffer "*coq*")) -;;;###autoload (add-hook 'same-window-buffer-names "*coq*") - -(defun run-coq-other-frame (cmd) - "Run an inferior Coq process, input and output via buffer *coq*. -If there is a process already running in `*coq*', switch to that buffer. -With argument, allows you to edit the command line (default is value -of `coq-program-name'). Runs the hooks `inferior-coq-mode-hook' -\(after the `comint-mode-hook' is run). -\(Type \\[describe-mode] in the process buffer for a list of commands.)" - - (interactive (list (if current-prefix-arg - (read-string "Run Coq: " coq-program-name) - coq-program-name))) - (if (not (comint-check-proc "*coq*")) - (let ((cmdlist (coq-args-to-list cmd))) - (set-buffer (apply 'make-comint "coq" (car cmdlist) - nil (cdr cmdlist))) - (inferior-coq-mode))) - (setq coq-program-name cmd) - (setq coq-buffer "*coq*") - (switch-to-buffer-other-frame "*coq*")) - -(defun switch-to-coq (eob-p) - "Switch to the coq process buffer. -With argument, position cursor at end of buffer." - (interactive "P") - (if (get-buffer coq-buffer) - (pop-to-buffer coq-buffer) - (error "No current process buffer. See variable `coq-buffer'")) - (cond (eob-p - (push-mark) - (goto-char (point-max))))) - -(defun coq-send-region (start end) - "Send the current region to the inferior Coq process." - (interactive "r") - (comint-send-region (coq-proc) start end) - (comint-send-string (coq-proc) "\n")) - -(defun coq-send-line () - "Send the current line to the Coq process." - (interactive) - (save-excursion - (end-of-line) - (let ((end (point))) - (beginning-of-line) - (coq-send-region (point) end))) - (forward-line 1)) - -(defun coq-send-abort () - "Send the command \"Abort.\" to the inferior Coq process." - (interactive) - (comint-send-string (coq-proc) "Abort.\n")) - -(defun coq-send-restart () - "Send the command \"Restart.\" to the inferior Coq process." - (interactive) - (comint-send-string (coq-proc) "Restart.\n")) - -(defun coq-send-undo () - "Reset coq to the initial state and send the region between the - beginning of file and the point." - (interactive) - (comint-send-string (coq-proc) "Undo.\n")) - -(defun coq-check-region (start end) - "Run the commmand \"Check\" on the current region." - (interactive "r") - (comint-proc-query (coq-proc) - (concat "Check " - (buffer-substring start end) - ".\n"))) - -(defun coq-send-show () - "Send the command \"Show.\" to the inferior Coq process." - (interactive) - (comint-send-string (coq-proc) "Show.\n")) - -(defun coq-come-here () - "Reset coq to the initial state and send the region between the - beginning of file and the point." - (interactive) - (comint-send-string (coq-proc) "Reset Initial.\n") - (coq-send-region 1 (point))) - -(defvar coq-buffer nil "*The current coq process buffer.") - -(defun coq-proc () - "Return the current coq process. See variable `coq-buffer'." - (let ((proc (get-buffer-process (if (eq major-mode 'inferior-coq-mode) - (current-buffer) - coq-buffer)))) - (or proc - (error "No current process. See variable `coq-buffer'")))) - -(defcustom inferior-coq-load-hook nil - "This hook is run when inferior-coq is loaded in. -This is a good place to put keybindings." - :type 'hook - :group 'inferior-coq) - -(run-hooks 'inferior-coq-load-hook) - -(provide 'inferior-coq) diff --git a/tools/make-both-single-timing-files.py b/tools/make-both-single-timing-files.py index c6af2ff1f..32c52c7a1 100755 --- a/tools/make-both-single-timing-files.py +++ b/tools/make-both-single-timing-files.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python2 +#!/usr/bin/env python import sys from TimeFileMaker import * diff --git a/tools/make-both-time-files.py b/tools/make-both-time-files.py index 643429679..f730a8d6b 100755 --- a/tools/make-both-time-files.py +++ b/tools/make-both-time-files.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python2 +#!/usr/bin/env python import sys from TimeFileMaker import * diff --git a/tools/make-one-time-file.py b/tools/make-one-time-file.py index c9905249e..e66136df9 100755 --- a/tools/make-one-time-file.py +++ b/tools/make-one-time-file.py @@ -1,4 +1,4 @@ -#!/usr/bin/env python2 +#!/usr/bin/env python import sys from TimeFileMaker import * |