diff options
129 files changed, 2099 insertions, 1865 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 324889ec90..512a9c99eb 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -24,6 +24,7 @@ /.travis.yml @coq/ci-maintainers /.gitlab-ci.yml @coq/ci-maintainers /Makefile.ci @coq/ci-maintainers +/dev/ci/nix @coq/nix-maintainers /dev/ci/user-overlays/*.sh @ghost # Trick to avoid getting review requests diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 89b9e6de30..1c5c8efc19 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -9,7 +9,7 @@ stages: variables: # Format: $IMAGE-V$DATE [Cache is not used as of today but kept here # for reference] - CACHEKEY: "bionic_coq-V2018-11-07-V1" + CACHEKEY: "bionic_coq-V2018-10-30-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" @@ -414,6 +414,9 @@ ci-formal-topology: ci-geocoq: <<: *ci-template-flambda +ci-coqhammer: + <<: *ci-template + ci-hott: <<: *ci-template @@ -429,6 +432,9 @@ ci-math-comp: ci-mtac2: <<: *ci-template +ci-paramcoq: + <<: *ci-template + ci-pidetop: <<: *ci-template diff --git a/CHANGES.md b/CHANGES.md index 91763ba35c..c830bc7a1c 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -52,6 +52,9 @@ Vernacular commands - `Combined Scheme` can now work when inductive schemes are generated in sort `Type`. It used to be limited to sort `Prop`. +- Binders for an `Instance` now act more like binders for a `Theorem`. + Names may not be repeated, and may not overlap with section variable names. + Tools - The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values: @@ -172,8 +175,9 @@ Standard Library - Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`, and `int31` are no longer available merely by `Require`ing the files - that define the inductives. You must `Import` `Coq.Strings.String`, - `Coq.Strings.Ascii`, `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`, + that define the inductives. You must `Import` `Coq.Strings.String.StringSyntax` + (after `Require` `Coq.Strings.String`), `Coq.Strings.Ascii.AsciiSyntax` (after + `Require` `Coq.Strings.Ascii`), `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`, `Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and `Coq.Numbers.Cyclic.Int31.Int31`, respectively, to be able to use these notations. Note that passing `-compat 8.8` or issuing @@ -39,7 +39,7 @@ WHAT DO YOU NEED ? - Findlib (version >= 1.4.1) (available at http://projects.camlcity.org/projects/findlib.html) - - Camlp5 (version >= 7.06) + - Camlp5 (version >= 7.03) (available at https://camlp5.github.io/) - GNU Make version 3.81 or later diff --git a/Makefile.checker b/Makefile.checker index a0f0778d49..7440c767e6 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -59,8 +59,7 @@ checker/check.cmxa: checker/check.mllib $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) -CHECKMLFILES:=$(filter checker/%, $(MLFILES) $(MLIFILES)) \ - $(filter dev/checker_%, $(MLFILES) $(MLIFILES)) +CHECKMLFILES:=$(filter checker/%, $(MLFILES) $(MLIFILES)) $(CHECKMLDFILE).d: $(filter checker/%, $(MLFILES) $(MLIFILES)) $(SHOW)'OCAMLDEP checker/MLFILES checker/MLIFILES' @@ -82,14 +81,6 @@ checker/%.cmx: checker/%.ml $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(CHKLIBS) $(OPTFLAGS) -c $< -dev/checker_%.cmo: dev/checker_%.ml - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -I dev/ -c $< - -dev/checker_%.cmi: dev/checker_%.mli - $(SHOW)'OCAMLC $<' - $(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -I dev/ -c $< - # For emacs: # Local Variables: # mode: makefile diff --git a/Makefile.ci b/Makefile.ci index 8234da0869..e8fea11bdb 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -29,12 +29,14 @@ CI_TARGETS= \ ci-flocq \ ci-formal-topology \ ci-geocoq \ + ci-coqhammer \ ci-hott \ ci-iris-lambda-rust \ ci-ltac2 \ ci-math-classes \ ci-math-comp \ ci-mtac2 \ + ci-paramcoq \ ci-pidetop \ ci-plugin-tutorial \ ci-quickchick \ diff --git a/Makefile.dev b/Makefile.dev index 54710b6690..9659f602d7 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -17,7 +17,7 @@ .PHONY: devel printers -DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo +DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo devel: printers printers: $(CORECMA) $(DEBUGPRINTERS) diff --git a/Makefile.dune b/Makefile.dune index d201d1783a..2293c69c38 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -42,9 +42,9 @@ check: voboot COQTOP_FILES=ide/idetop.bc ide/coqide_main.bc checker/coqchk.bc PLUGIN_FILES=$(wildcard plugins/*/*.mlpack) -PRINTER_FILES=dev/top_printers.cma dev/checker_printers.cma +PRINTER_FILES=dev/top_printers.cma QUICKBYTE_TARGETS=$(COQTOP_FILES) $(PLUGIN_FILES:.mlpack=.cma) $(PRINTER_FILES) topbin/coqtop_byte_bin.bc -QUICKOPT_TARGETS=$(COQTOP_FILES:.bc=.exe) $(PLUGIN_FILES:.mlpack=.cmxa) $(PRINTER_FILES:.cma=.cmxa) topbin/coqtop_bin.exe +QUICKOPT_TARGETS=$(COQTOP_FILES:.bc=.exe) $(PLUGIN_FILES:.mlpack=.cmxs) $(PRINTER_FILES:.cma=.cmxa) topbin/coqtop_bin.exe quickbyte: voboot dune build $(DUNEOPT) $(QUICKBYTE_TARGETS) @@ -53,7 +53,7 @@ quickopt: voboot dune build $(DUNEOPT) $(QUICKOPT_TARGETS) test-suite: voboot - dune $(DUNEOPT) runtest + dune runtest $(DUNEOPT) release: voboot dune build $(DUNEOPT) -p coq diff --git a/checker/values.ml b/checker/values.ml index 8f6b24ec26..e21acd8179 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -122,8 +122,7 @@ let v_cstrs = let v_variance = v_enum "variance" 3 let v_instance = Annot ("instance", Array v_level) -let v_context = v_tuple "universe_context" [|v_instance;v_cstrs|] -let v_abs_context = v_context (* only for clarity *) +let v_abs_context = v_tuple "abstract_universe_context" [|Array v_name; v_cstrs|] let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|] let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|] diff --git a/clib/cUnix.ml b/clib/cUnix.ml index 6b42e3041d..eedd878f93 100644 --- a/clib/cUnix.ml +++ b/clib/cUnix.ml @@ -74,10 +74,6 @@ let canonical_path_name p = let make_suffix name suffix = if Filename.check_suffix name suffix then name else (name ^ suffix) -let get_extension f = - let pos = try String.rindex f '.' with Not_found -> String.length f in - String.sub f pos (String.length f - pos) - let correct_path f dir = if Filename.is_relative f then Filename.concat dir f else f diff --git a/clib/cUnix.mli b/clib/cUnix.mli index 1b185345be..896ccd4ea7 100644 --- a/clib/cUnix.mli +++ b/clib/cUnix.mli @@ -38,10 +38,6 @@ val path_to_list : string -> string list [file] does not already end with [suf]. *) val make_suffix : string -> string -> string -(** Return the extension of a file, i.e. its smaller suffix starting - with "." if any, or "" otherwise. *) -val get_extension : string -> string - val file_readable_p : string -> bool (** {6 Executing commands } *) diff --git a/configure.ml b/configure.ml index 14c1f38a95..47f7633ae8 100644 --- a/configure.ml +++ b/configure.ml @@ -709,9 +709,9 @@ let check_camlp5_version camlp5o = let version_line, _ = run ~err:StdOut camlp5o ["-v"] in let version = List.nth (string_split ' ' version_line) 2 in match numeric_prefix_list version with - | major::minor::_ when s2i major > 7 || (s2i major, s2i minor) >= (7,6) -> + | major::minor::_ when s2i major > 6 || (s2i major, s2i minor) >= (6,6) -> cprintf "You have Camlp5 %s. Good!" version; version - | _ -> die "Error: unsupported Camlp5 (version < 7.06 or unrecognized).\n" + | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n" let config_camlp5 () = let camlp5mod = "gramlib" in @@ -1211,10 +1211,9 @@ let write_configml f = pr_b "bytecode_compiler" !prefs.bytecodecompiler; pr_b "native_compiler" !prefs.nativecompiler; - let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library"; + let core_src_dirs = [ "config"; "lib"; "clib"; "kernel"; "library"; "engine"; "pretyping"; "interp"; "parsing"; "proofs"; - "tactics"; "toplevel"; "printing"; - "grammar"; "ide"; "stm"; "vernac" ] in + "tactics"; "toplevel"; "printing"; "ide"; "stm"; "vernac" ] in let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ " \"" ^ core_src_subdir ^ "\";\n") "" core_src_dirs in @@ -22,7 +22,7 @@ depends: [ "ocaml" { >= "4.05.0" } "dune" { build & >= "1.4.0" } "num" - "camlp5" { >= "7.06" } + "camlp5" { >= "7.03" } ] build-env: [ diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 7cecff9d75..ba3b9bcbbf 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -357,15 +357,15 @@ let print_body fmt r = print_binders r.vernac_toks print_atts_right r.vernac_atts let rec print_sig fmt = function -| [] -> fprintf fmt "@[Vernacentries.TyNil@]" +| [] -> fprintf fmt "@[Vernacextend.TyNil@]" | ExtTerminal s :: rem -> - fprintf fmt "@[Vernacentries.TyTerminal (\"%s\", %a)@]" s print_sig rem + fprintf fmt "@[Vernacextend.TyTerminal (\"%s\", %a)@]" s print_sig rem | ExtNonTerminal (symb, _) :: rem -> - fprintf fmt "@[Vernacentries.TyNonTerminal (%a, %a)@]" + fprintf fmt "@[Vernacextend.TyNonTerminal (%a, %a)@]" print_symbol symb print_sig rem let print_rule fmt r = - fprintf fmt "Vernacentries.TyML (%b, %a, %a, %a)" + fprintf fmt "Vernacextend.TyML (%b, %a, %a, %a)" r.vernac_depr print_sig r.vernac_toks print_body r print_rule_classifier r let print_rules fmt rules = @@ -386,7 +386,7 @@ let print_entry fmt = function let print_ast fmt ext = let pr fmt () = - fprintf fmt "Vernacentries.vernac_extend ~command:\"%s\" %a ?entry:%a %a" + fprintf fmt "Vernacextend.vernac_extend ~command:\"%s\" %a ?entry:%a %a" ext.vernacext_name print_classifier ext.vernacext_class print_entry ext.vernacext_entry print_rules ext.vernacext_rules in @@ -481,8 +481,8 @@ let print_rules fmt (name, rules) = factorization of parsing rules. It allows to recognize rules of the form [ entry(x) ] -> [ x ] so as not to generate a proxy entry and reuse the same entry directly. *) - fprintf fmt "@[Vernacentries.Arg_alias (%s)@]" e - | _ -> fprintf fmt "@[Vernacentries.Arg_rules (%a)@]" pr rules + fprintf fmt "@[Vernacextend.Arg_alias (%s)@]" e + | _ -> fprintf fmt "@[Vernacextend.Arg_rules (%a)@]" pr rules let print_printer fmt = function | None -> fprintf fmt "@[fun _ -> Pp.str \"missing printer\"@]" @@ -491,9 +491,9 @@ let print_printer fmt = function let print_ast fmt arg = let name = arg.vernacargext_name in let pr fmt () = - fprintf fmt "Vernacentries.vernac_argument_extend ~name:%a @[{@\n\ - Vernacentries.arg_parsing = %a;@\n\ - Vernacentries.arg_printer = %a;@\n}@]" + fprintf fmt "Vernacextend.vernac_argument_extend ~name:%a @[{@\n\ + Vernacextend.arg_parsing = %a;@\n\ + Vernacextend.arg_printer = %a;@\n}@]" print_string name print_rules (name, arg.vernacargext_rules) print_printer arg.vernacargext_printer in diff --git a/dev/base_include b/dev/base_include index 67a7e87d78..0e12b57b36 100644 --- a/dev/base_include +++ b/dev/base_include @@ -176,7 +176,7 @@ open Mltop open Record open Coqloop open Vernacentries -open Vernacinterp +open Vernacextend open Vernac (* Various utilities *) diff --git a/dev/checker.dbg b/dev/checker.dbg deleted file mode 100644 index b5b7f0e6d3..0000000000 --- a/dev/checker.dbg +++ /dev/null @@ -1,7 +0,0 @@ -load_printer threads.cma -load_printer str.cma -load_printer clib.cma -load_printer dynlink.cma -load_printer config.cma -load_printer lib.cma -load_printer check.cma diff --git a/dev/checker_db b/dev/checker_db deleted file mode 100644 index fcb6f679ed..0000000000 --- a/dev/checker_db +++ /dev/null @@ -1,5 +0,0 @@ -source checker.dbg - -load_printer checker_printers.cmo - -source checker_printers.dbg diff --git a/dev/checker_dune_db b/dev/checker_dune_db deleted file mode 100644 index cdb6a4b809..0000000000 --- a/dev/checker_dune_db +++ /dev/null @@ -1,5 +0,0 @@ -source checker_dune.dbg - -load_printer checker_printers.cma - -source checker_printers.dbg diff --git a/dev/checker_printers.dbg b/dev/checker_printers.dbg deleted file mode 100644 index 9ebbd74834..0000000000 --- a/dev/checker_printers.dbg +++ /dev/null @@ -1,35 +0,0 @@ -install_printer Checker_printers.pP - -install_printer Checker_printers.ppfuture - -install_printer Checker_printers.ppid -install_printer Checker_printers.pplab -install_printer Checker_printers.ppmbid -install_printer Checker_printers.ppdir -install_printer Checker_printers.ppmp -install_printer Checker_printers.ppcon -install_printer Checker_printers.ppproj -install_printer Checker_printers.ppkn -install_printer Checker_printers.ppmind -install_printer Checker_printers.ppind - -install_printer Checker_printers.ppbigint - -install_printer Checker_printers.ppintset -install_printer Checker_printers.ppidset - -install_printer Checker_printers.ppidmapgen - -install_printer Checker_printers.ppididmap - -install_printer Checker_printers.ppuni -install_printer Checker_printers.ppuni_level -install_printer Checker_printers.ppuniverse_set -install_printer Checker_printers.ppuniverse_instance -install_printer Checker_printers.ppauniverse_context -install_printer Checker_printers.ppuniverse_context -install_printer Checker_printers.ppconstraints -install_printer Checker_printers.ppuniverse_context_future -install_printer Checker_printers.ppuniverses - -install_printer Checker_printers.pploc diff --git a/dev/checker_printers.ml b/dev/checker_printers.ml deleted file mode 100644 index 4f89bbd34e..0000000000 --- a/dev/checker_printers.ml +++ /dev/null @@ -1,69 +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 Pp -open Names -open Univ - -let pp x = Pp.pp_with Format.std_formatter x - -(** Future printer *) - -let ppfuture kx = pp (Future.print (fun _ -> str "_") kx) - -(* name printers *) -let ppid id = pp (Id.print id) -let pplab l = pp (Label.print l) -let ppmbid mbid = pp (str (MBId.debug_to_string mbid)) -let ppdir dir = pp (DirPath.print dir) -let ppmp mp = pp(str (ModPath.debug_to_string mp)) -let ppcon con = pp(Constant.debug_print con) -let ppproj con = pp(Constant.debug_print (Projection.constant con)) -let ppkn kn = pp(str (KerName.to_string kn)) -let ppmind kn = pp(MutInd.debug_print kn) -let ppind (kn,i) = pp(MutInd.debug_print kn ++ str"," ++int i) - -(* term printers *) -let ppbigint n = pp (str (Bigint.to_string n));; - -let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]" -let ppintset l = pp (prset int (Int.Set.elements l)) -let ppidset l = pp (prset Id.print (Id.Set.elements l)) - -let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]" - -let pridmap pr l = - let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in - prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l []) -let ppidmap pr l = pp (pridmap pr l) - -let pridmapgen l = - let dom = Id.Set.elements (Id.Map.domain l) in - if dom = [] then str "[]" else - str "[domain= " ++ hov 0 (prlist_with_sep spc Id.print dom) ++ str "]" -let ppidmapgen l = pp (pridmapgen l) - -let prididmap = pridmap (fun _ -> Id.print) -let ppididmap = ppidmap (fun _ -> Id.print) - -let pP s = pp (hov 0 s) - -(* proof printers *) -let ppuni u = pp(Universe.pr u) -let ppuni_level u = pp (Level.pr u) - -let ppuniverse_context l = pp (pr_universe_context Level.pr l) -let ppconstraints c = pp (pr_constraints Level.pr c) -let ppuniverse_context_future c = - let ctx = Future.force c in - ppuniverse_context ctx - -let pploc x = let (l,r) = Loc.unloc x in - print_string"(";print_int l;print_string",";print_int r;print_string")" diff --git a/dev/checker_printers.mli b/dev/checker_printers.mli deleted file mode 100644 index 8be9b87257..0000000000 --- a/dev/checker_printers.mli +++ /dev/null @@ -1,50 +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) *) -(************************************************************************) - -(** Printers for the ocaml toplevel. *) - -val pp : Pp.t -> unit -val pP : Pp.t -> unit (* with surrounding box *) - -val ppfuture : 'a Future.computation -> unit - -val ppid : Names.Id.t -> unit -val pplab : Names.Label.t -> unit -val ppmbid : Names.MBId.t -> unit -val ppdir : Names.DirPath.t -> unit -val ppmp : Names.ModPath.t -> unit -val ppcon : Names.Constant.t -> unit -val ppproj : Names.Projection.t -> unit -val ppkn : Names.KerName.t -> unit -val ppmind : Names.MutInd.t -> unit -val ppind : Names.inductive -> unit - -val ppbigint : Bigint.bigint -> unit - -val ppintset : Int.Set.t -> unit -val ppidset : Names.Id.Set.t -> unit - -val pridmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> Pp.t -val ppidmap : (Names.Id.Map.key -> 'a -> Pp.t) -> 'a Names.Id.Map.t -> unit - -val pridmapgen : 'a Names.Id.Map.t -> Pp.t -val ppidmapgen : 'a Names.Id.Map.t -> unit - -val prididmap : Names.Id.t Names.Id.Map.t -> Pp.t -val ppididmap : Names.Id.t Names.Id.Map.t -> unit - -(* Universes *) -val ppuni : Univ.Universe.t -> unit -val ppuni_level : Univ.Level.t -> unit (* raw *) -val ppuniverse_context : Univ.UContext.t -> unit -val ppconstraints : Univ.Constraint.t -> unit -val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit - -val pploc : Loc.t -> unit diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 50d4d21637..3137576207 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -70,6 +70,13 @@ : "${HoTT_CI_ARCHIVEURL:=${HoTT_CI_GITURL}/archive}" ######################################################################## +# CoqHammer +######################################################################## +: "${coqhammer_CI_REF:=master}" +: "${coqhammer_CI_GITURL:=https://github.com/lukaszcz/coqhammer}" +: "${coqhammer_CI_ARCHIVEURL:=${coqhammer_CI_GITURL}/archive}" + +######################################################################## # Ltac2 ######################################################################## : "${ltac2_CI_REF:=master}" @@ -255,3 +262,10 @@ : "${aactactics_CI_REF:=master}" : "${aactactics_CI_GITURL:=https://github.com/coq-community/aac-tactics}" : "${aactactics_CI_ARCHIVEURL:=${aactactics_CI_GITURL}/archive}" + +######################################################################## +# paramcoq +######################################################################## +: "${paramcoq_CI_REF:=master}" +: "${paramcoq_CI_GITURL:=https://github.com/coq-community/paramcoq}" +: "${paramcoq_CI_ARCHIVEURL:=${paramcoq_CI_GITURL}/archive}" diff --git a/dev/ci/ci-coqhammer.sh b/dev/ci/ci-coqhammer.sh new file mode 100755 index 0000000000..4384e6c828 --- /dev/null +++ b/dev/ci/ci-coqhammer.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download coqhammer + +( cd "${CI_BUILD_DIR}/coqhammer" && make ) diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 7eeeb09372..c8e6fe690f 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")" git_download HoTT -( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh && ./configure && make && make validate ) +( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh -skip-submodules && ./configure && make && make validate ) diff --git a/dev/ci/ci-paramcoq.sh b/dev/ci/ci-paramcoq.sh new file mode 100755 index 0000000000..c641af2abb --- /dev/null +++ b/dev/ci/ci-paramcoq.sh @@ -0,0 +1,8 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +. "${ci_dir}/ci-common.sh" + +git_download paramcoq + +( cd "${CI_BUILD_DIR}/paramcoq" && make && make install ) diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index 0439d566fd..4ddb582414 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-11-07-V1" +# CACHEKEY: "bionic_coq-V2018-10-30-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -41,7 +41,7 @@ ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.4.0 ounit.2.0.8 odoc.1.3.0" \ CI_OPAM="menhir.20180530 elpi.1.1.0 ocamlgraph.1.8.8" # BASE switch; CI_OPAM contains Coq's CI dependencies. -ENV CAMLP5_VER="7.06" \ +ENV CAMLP5_VER="7.03" \ COQIDE_OPAM="lablgtk.2.18.5 conf-gtksourceview.2" # base switch diff --git a/dev/ci/nix/CoLoR.nix b/dev/ci/nix/CoLoR.nix new file mode 100644 index 0000000000..4c5cfd83da --- /dev/null +++ b/dev/ci/nix/CoLoR.nix @@ -0,0 +1,5 @@ +{ bignums }: + +{ + buildInputs = [ bignums ]; +} diff --git a/dev/ci/nix/CompCert.nix b/dev/ci/nix/CompCert.nix new file mode 100644 index 0000000000..db1721e5f5 --- /dev/null +++ b/dev/ci/nix/CompCert.nix @@ -0,0 +1,7 @@ +{ ocamlPackages }: + +{ + buildInputs = with ocamlPackages; [ ocaml findlib menhir ]; + configure = "./configure -ignore-coq-version x86_64-linux"; + make = "make all check-proof"; +} diff --git a/dev/ci/nix/Corn.nix b/dev/ci/nix/Corn.nix new file mode 100644 index 0000000000..18c7750279 --- /dev/null +++ b/dev/ci/nix/Corn.nix @@ -0,0 +1,5 @@ +{ bignums, math-classes }: + +{ + buildInputs = [ bignums math-classes ]; +} diff --git a/dev/ci/nix/Elpi.nix b/dev/ci/nix/Elpi.nix new file mode 100644 index 0000000000..0a6ed20295 --- /dev/null +++ b/dev/ci/nix/Elpi.nix @@ -0,0 +1,4 @@ +{ ocamlPackages }: +{ + buildInputs = with ocamlPackages; [ ocaml findlib elpi ]; +} diff --git a/dev/ci/nix/GeoCoq.nix b/dev/ci/nix/GeoCoq.nix new file mode 100644 index 0000000000..a86fb2c44a --- /dev/null +++ b/dev/ci/nix/GeoCoq.nix @@ -0,0 +1,5 @@ +{ mathcomp }: +{ + buildInputs = [ mathcomp ]; + configure = "./configure.sh"; +} diff --git a/dev/ci/nix/HoTT.nix b/dev/ci/nix/HoTT.nix new file mode 100644 index 0000000000..dea0aeeb55 --- /dev/null +++ b/dev/ci/nix/HoTT.nix @@ -0,0 +1,6 @@ +{ autoconf, automake }: +{ + buildInputs = [ autoconf automake ]; + configure = "./autogen.sh && ./configure"; + make = "make all validate"; +} diff --git a/dev/ci/nix/VST.nix b/dev/ci/nix/VST.nix new file mode 100644 index 0000000000..3e2629a0b6 --- /dev/null +++ b/dev/ci/nix/VST.nix @@ -0,0 +1,6 @@ +{}: + +rec { + make = "make IGNORECOQVERSION=true"; + clean = "${make} clean"; +} diff --git a/dev/ci/nix/bedrock2.nix b/dev/ci/nix/bedrock2.nix new file mode 100644 index 0000000000..552d9297e2 --- /dev/null +++ b/dev/ci/nix/bedrock2.nix @@ -0,0 +1,5 @@ +{}: +{ + configure = "git submodule update --init --recursive"; + clean = "(cd deps/bbv && make clean); (cd deps/riscv-coq && make clean); (cd compiler && make clean); (cd bedrock2 && make clean)"; +} diff --git a/dev/ci/nix/bignums.nix b/dev/ci/nix/bignums.nix new file mode 100644 index 0000000000..1d931c858e --- /dev/null +++ b/dev/ci/nix/bignums.nix @@ -0,0 +1,5 @@ +{ ocamlPackages }: + +{ + buildInputs = with ocamlPackages; [ ocaml findlib camlp5 ]; +} diff --git a/dev/ci/nix/coq.nix b/dev/ci/nix/coq.nix new file mode 100644 index 0000000000..ecd280e58d --- /dev/null +++ b/dev/ci/nix/coq.nix @@ -0,0 +1,9 @@ +{ stdenv, callPackage, branch, wd }: + +let coq = callPackage wd { buildDoc = false; doInstallCheck = false; coq-version = "8.9"; }; in + +coq.overrideAttrs (o: { + name = "coq-local-${branch}"; + src = fetchGit "${wd}"; + enableParallelBuilding = true; +}) diff --git a/dev/ci/nix/coq_dpdgraph.nix b/dev/ci/nix/coq_dpdgraph.nix new file mode 100644 index 0000000000..611e2fcca5 --- /dev/null +++ b/dev/ci/nix/coq_dpdgraph.nix @@ -0,0 +1,7 @@ +{ autoconf, ocamlPackages }: + +{ + buildInputs = [ autoconf ] ++ (with ocamlPackages; [ ocaml findlib camlp5 ocamlgraph ]); + configure = "autoconf && ./configure"; + make = "make all test-suite"; +} diff --git a/dev/ci/nix/cross_crypto.nix b/dev/ci/nix/cross_crypto.nix new file mode 100644 index 0000000000..98f74f9474 --- /dev/null +++ b/dev/ci/nix/cross_crypto.nix @@ -0,0 +1,5 @@ +{}: +{ + configure = "git submodule update --init --recursive"; + clean = "make cleanall"; +} diff --git a/dev/ci/nix/default.nix b/dev/ci/nix/default.nix new file mode 100644 index 0000000000..4acfae48e4 --- /dev/null +++ b/dev/ci/nix/default.nix @@ -0,0 +1,72 @@ +{ pkgs ? import <nixpkgs> {} +, branch +, wd +, project ? "xyz" +, bn ? "release" +}: + +with pkgs; + +# Coq from this directory +let coq = callPackage ./coq.nix { inherit branch wd; }; in + +# Third-party libraries, built with this Coq +let coqPackages = mkCoqPackages coq; in +let mathcomp = coqPackages.mathcomp.overrideAttrs (o: { + name = "coq-git-mathcomp-git"; + src = fetchTarball https://github.com/math-comp/math-comp/archive/master.tar.gz; + }); in +let bignums = coqPackages.bignums.overrideAttrs (o: + if bn == "release" then {} else + if bn == "master" then { src = fetchTarball https://github.com/coq/bignums/archive/master.tar.gz; } else + { src = fetchTarball bn; } + ); in +let coqprime = coqPackages.coqprime.override { inherit coq bignums; }; in +let math-classes = + (coqPackages.math-classes.override { inherit coq bignums; }) + .overrideAttrs (o: { + src = fetchTarball "https://github.com/coq-community/math-classes/archive/master.tar.gz"; + }); in + +let unicoq = callPackage ./unicoq.nix { inherit coq; }; in + +let callPackage = newScope { inherit coq mathcomp bignums coqprime math-classes unicoq; }; in + +# Environments for building CI libraries with this Coq +let projects = { + bedrock2 = callPackage ./bedrock2.nix {}; + bignums = callPackage ./bignums.nix {}; + CoLoR = callPackage ./CoLoR.nix {}; + CompCert = callPackage ./CompCert.nix {}; + coq_dpdgraph = callPackage ./coq_dpdgraph.nix {}; + Corn = callPackage ./Corn.nix {}; + cross_crypto = callPackage ./cross_crypto.nix {}; + Elpi = callPackage ./Elpi.nix {}; + fiat_crypto = callPackage ./fiat_crypto.nix {}; + fiat_crypto_legacy = callPackage ./fiat_crypto_legacy.nix {}; + flocq = callPackage ./flocq.nix {}; + GeoCoq = callPackage ./GeoCoq.nix {}; + HoTT = callPackage ./HoTT.nix {}; + math_classes = callPackage ./math_classes.nix {}; + mathcomp = {}; + mtac2 = callPackage ./mtac2.nix {}; + oddorder = callPackage ./oddorder.nix {}; + VST = callPackage ./VST.nix {}; +}; in + +if !builtins.hasAttr project projects +then throw "Unknown project “${project}”; choose from: ${pkgs.lib.concatStringsSep ", " (builtins.attrNames projects)}." +else + +let prj = projects."${project}"; in + +stdenv.mkDerivation { + name = "shell-for-${project}-in-${branch}"; + + buildInputs = [ coq ] ++ (prj.buildInputs or []); + + configure = prj.configure or "true"; + make = prj.make or "make"; + clean = prj.clean or "make clean"; + +} diff --git a/dev/ci/nix/fiat_crypto.nix b/dev/ci/nix/fiat_crypto.nix new file mode 100644 index 0000000000..7b37e6e8e4 --- /dev/null +++ b/dev/ci/nix/fiat_crypto.nix @@ -0,0 +1,6 @@ +{ coqprime }: +{ + buildInputs = [ coqprime ]; + configure = "git submodule update --init --recursive && ulimit -s 32768"; + make = "make new-pipeline c-files"; +} diff --git a/dev/ci/nix/fiat_crypto_legacy.nix b/dev/ci/nix/fiat_crypto_legacy.nix new file mode 100644 index 0000000000..3248665579 --- /dev/null +++ b/dev/ci/nix/fiat_crypto_legacy.nix @@ -0,0 +1,6 @@ +{}: + +{ + configure = "./etc/ci/remove_autogenerated.sh"; + make = "make print-old-pipeline-lite old-pipeline-lite lite-display"; +} diff --git a/dev/ci/nix/flocq.nix b/dev/ci/nix/flocq.nix new file mode 100644 index 0000000000..e153043557 --- /dev/null +++ b/dev/ci/nix/flocq.nix @@ -0,0 +1,7 @@ +{ autoconf, automake }: + +{ + buildInputs = [ autoconf automake ]; + configure = "./autogen.sh && ./configure"; + make = "./remake"; +} diff --git a/dev/ci/nix/math_classes.nix b/dev/ci/nix/math_classes.nix new file mode 100644 index 0000000000..b0fa2fe795 --- /dev/null +++ b/dev/ci/nix/math_classes.nix @@ -0,0 +1,6 @@ +{ bignums }: + +{ + buildInputs = [ bignums ]; + configure = "./configure.sh"; +} diff --git a/dev/ci/nix/mtac2.nix b/dev/ci/nix/mtac2.nix new file mode 100644 index 0000000000..9a2353c5cf --- /dev/null +++ b/dev/ci/nix/mtac2.nix @@ -0,0 +1,5 @@ +{ coq, unicoq }: +{ + buildInputs = [ unicoq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 ]); + configure = "./configure.sh"; +} diff --git a/dev/ci/nix/oddorder.nix b/dev/ci/nix/oddorder.nix new file mode 100644 index 0000000000..3b8fdbab51 --- /dev/null +++ b/dev/ci/nix/oddorder.nix @@ -0,0 +1,4 @@ +{ mathcomp }: +{ + buildInputs = [ mathcomp ]; +} diff --git a/dev/ci/nix/shell b/dev/ci/nix/shell new file mode 100755 index 0000000000..2e4462ed40 --- /dev/null +++ b/dev/ci/nix/shell @@ -0,0 +1,20 @@ +#!/usr/bin/env sh + +## This file should be run from the root of the Coq source tree + +BRANCH=$(git rev-parse --abbrev-ref HEAD) +echo "Branch: $BRANCH in $PWD" + +if [ "$#" -ne 1 ]; then + PROJECT="" +else + PROJECT="--argstr project $1" +fi + +if [ "$BN" ]; then + BN="--argstr bn ${BN}" +else + BN="" +fi + +nix-shell ./dev/ci/nix/ --show-trace --argstr wd $PWD --argstr branch $BRANCH $PROJECT $BN diff --git a/dev/ci/nix/unicoq.nix b/dev/ci/nix/unicoq.nix new file mode 100644 index 0000000000..f10afd5680 --- /dev/null +++ b/dev/ci/nix/unicoq.nix @@ -0,0 +1,14 @@ +{ stdenv, fetchzip, coq }: + +stdenv.mkDerivation { + name = "coq${coq.coq-version}-unicoq-0.0-git"; + src = fetchzip { + url = "https://github.com/vbgl/unicoq/archive/8b33e37700e92bfd404bf8bf9fe03f1be8928d97.tar.gz"; + sha256 = "0s4z0wjxlp56ccgzxgk04z7skw90rdnz39v730ffkgrjl38rr9il"; + }; + + buildInputs = [ coq ] ++ (with coq.ocamlPackages; [ ocaml findlib camlp5 num ]); + + configurePhase = "coq_makefile -f Make -o Makefile"; + installFlags = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; +} diff --git a/dev/ci/user-overlays/08601-name-abstract-univ-context.sh b/dev/ci/user-overlays/08601-name-abstract-univ-context.sh new file mode 100644 index 0000000000..9d723dc7f2 --- /dev/null +++ b/dev/ci/user-overlays/08601-name-abstract-univ-context.sh @@ -0,0 +1,11 @@ +_OVERLAY_BRANCH=name-abstract-univ-context + +if [ "$CI_PULL_REQUEST" = "8601" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + Elpi_CI_REF="$_OVERLAY_BRANCH" + Elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi + + Equations_CI_REF="$_OVERLAY_BRANCH" + Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + +fi diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index 000f21c254..318562338d 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -6,19 +6,21 @@ This document describes how patches, submitted as pull requests (PRs) on the ## Code owners -The [CODEOWNERS](../../.github/CODEOWNERS) file describes, for each part of the -system, two owners. One is the principal maintainer of the component, the other -is the secondary maintainer. +The [CODEOWNERS](../../.github/CODEOWNERS) file defines owners for each part of +the code. Sometime there is one principal maintainer and one or several +secondary maintainer(s). Sometimes, it is a team of code owners and all of its +members act as principal maintainers for the component. When a PR is submitted, GitHub will automatically ask the principal -maintainer for a review. If the PR touches several parts, all the -corresponding principal maintainers will be asked for a review. +maintainer (or the code owner team) for a review. If the PR touches several +parts, all the corresponding owners will be asked for a review. Maintainers are never assigned as reviewer on their own PRs. -If a principal maintainer submits a PR that changes the component they own, they -must assign the secondary maintainer as reviewer. They should also do it if they -know they are not available to do the review. +If a principal maintainer submits a PR or is a co-author of a PR that is +submitted and this PR changes the component they own, they must request a +review from a secondary maintainer. They can also delegate the review if they +know they are not available to do it. ## Reviewing @@ -35,17 +37,29 @@ When maintainers receive a review request, they are expected to: REVIEWERS(*) have approved the PR, the assignee is expected to follow the merging process described below. -In all cases, maintainers can delegate reviews to the other maintainer of the -same component, except if it would lead to a maintainer reviewing their own -patch. +When a PR received lots of comments or if the PR has not been opened for long +and the assignee thinks that some other developers might want to comment, +it is recommended that they announce their intention to merge and wait a full +working day (or more if deemed useful) before the actual merge, as a sort of +last call for comments. + +In all cases, maintainers can delegate reviews to the other maintainers, +except if it would lead to a maintainer reviewing their own patch. A maintainer is expected to be reasonably reactive, but no specific timeframe is given for reviewing. +When none of the maintainers have commented nor self-assigned a PR in a delay +of five working days, any maintainer of another component who feels comfortable +reviewing the PR can assign it to themselves. To prevent misunderstandings, +maintainers should not hesitate to announce in advance when they shall be +unavailable for more than five working days. + (*) In case a component is touched in a trivial way (adding/removing one file in a `Makefile`, etc), or by applying a systematic refactoring process (global renaming for instance) that has been reviewed globally, the assignee can -say in a comment they think a review is not required and proceed with the merge. +say in a comment they think a review is not required from every code owner and +proceed with the merge. ### Breaking changes @@ -54,7 +68,8 @@ those external projects should have been prepared (cf. the relevant sub-section in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested with these fixes thanks to ["overlays"](../ci/user-overlays/README.md). -Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) file. +Moreover the PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) or +the [`dev/doc/changes.md`](changes.md) file. If overlays are missing, ask the author to prepare them and label the PR with the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label. @@ -78,9 +93,9 @@ put the approriate label. Otherwise, they are expected to merge the PR using the When CI has a few failures which look spurious, restarting the corresponding jobs is a good way of ensuring this was indeed the case. -To restart a job on Travis, you should connect using your GitHub account; -being part of the Coq organization on GitHub should give you the permission -to do so. +To restart a job on Travis or on AppVeyor, you should connect using your GitHub +account; being part of the Coq organization on GitHub should give you the +permission to do so. To restart a job on GitLab CI, you should sign into GitLab (this can be done using a GitHub account); if you are part of the [Coq organization on GitLab](https://gitlab.com/coq), you should see a "Retry" @@ -93,9 +108,10 @@ When the PR has conflicts, the assignee can either: In both cases, CI should be run again. -In some rare cases (e.g. the conflicts are in the `CHANGES.md` file), it is ok to fix +In some rare cases (e.g. the conflicts are in the `CHANGES.md` file and the PR +is not a candidate for backporting), it is ok to fix the conflicts in the merge commit (following the same steps as below), and push -to `master` directly. Don't use the GitHub interface to fix these conflicts. +to `master` directly. DON'T USE the GitHub interface to fix these conflicts. To merge the PR proceed in the following way ``` diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 0aeb30c4e8..c5ea88aaf6 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -81,7 +81,7 @@ or ``` dune exec dev/dune-dbg checker -(ocd) source checker_dune_db +(ocd) source dune_db ``` for the checker. Unfortunately, dependency handling here is not fully @@ -3,18 +3,9 @@ (public_name coq.top_printers) (synopsis "Coq's Debug Printers") (wrapped false) - (modules :standard \ checker_printers) + (modules :standard) (libraries coq.toplevel coq.plugins.ltac)) -(library - (name checker_printers) - (public_name coq.checker_printers) - (synopsis "Coq's Debug Printers [for the Checker]") - (wrapped false) - (flags :standard -open Checklib) - (modules checker_printers) - (libraries coq.checklib)) - (rule (targets dune-dbg) (deps dune-dbg.in diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in index 464e026400..3f3df23fe1 100755 --- a/dev/dune-dbg.in +++ b/dev/dune-dbg.in @@ -2,10 +2,12 @@ # Run in a proper install dune env. case $1 in -checker) - ocamldebug `ocamlfind query -recursive -i-format coq.checker_printers` -I +threads -I dev _build/default/checker/main.bc - ;; -*) - ocamldebug `ocamlfind query -recursive -i-format coq.top_printers` -I +threads -I dev _build/default/topbin/coqtop_byte_bin.bc - ;; + checker) + exe=_build/default/checker/main.bc + ;; + *) + exe=_build/default/topbin/coqtop_byte_bin.bc + ;; esac + +ocamldebug $(ocamlfind query -recursive -i-format coq.top_printers) -I +threads -I dev $exe diff --git a/dev/top_printers.ml b/dev/top_printers.ml index fd08f9ffe8..f94e9acb72 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -509,41 +509,23 @@ VERNAC COMMAND EXTEND PrintConstr END *) -open Genarg -open Stdarg -open Egramml - let _ = - try - Vernacinterp.vinterp_add false ("PrintConstr", 0) - (function - [c] when genarg_tag c = unquote (topwit wit_constr) && true -> - let c = out_gen (rawwit wit_constr) c in - (fun ~atts ~st -> in_current_context econstr_display c; st) - | _ -> failwith "Vernac extension: cannot occur") - with - e -> pp (CErrors.print e) -let _ = - extend_vernac_command_grammar ("PrintConstr", 0) None - [GramTerminal "PrintConstr"; - GramNonTerminal - (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))] + let open Vernacextend in + let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in + let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in + let cmd_fn c ~atts ~st = in_current_context econstr_display c; st in + let cmd_class _ = Vernacexpr.(VtQuery,VtNow) in + let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in + Vernacextend.vernac_extend ~command:"PrintConstr" [cmd] let _ = - try - Vernacinterp.vinterp_add false ("PrintPureConstr", 0) - (function - [c] when genarg_tag c = unquote (topwit wit_constr) && true -> - let c = out_gen (rawwit wit_constr) c in - (fun ~atts ~st -> in_current_context print_pure_econstr c; st) - | _ -> failwith "Vernac extension: cannot occur") - with - e -> pp (CErrors.print e) -let _ = - extend_vernac_command_grammar ("PrintPureConstr", 0) None - [GramTerminal "PrintPureConstr"; - GramNonTerminal - (Loc.tag (rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr))] + let open Vernacextend in + let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in + let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in + let cmd_fn c ~atts ~st = in_current_context print_pure_econstr c; st in + let cmd_class _ = Vernacexpr.(VtQuery,VtNow) in + let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in + Vernacextend.vernac_extend ~command:"PrintPureConstr" [cmd] (* Setting printer of unbound global reference *) open Names diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 8b13789179..b58148ffff 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -1 +1,77 @@ - +plugins/btauto/Algebra.v +plugins/btauto/Btauto.v +plugins/btauto/Reflect.v +plugins/derive/Derive.v +plugins/extraction/ExtrHaskellBasic.v +plugins/extraction/ExtrHaskellNatInt.v +plugins/extraction/ExtrHaskellNatInteger.v +plugins/extraction/ExtrHaskellNatNum.v +plugins/extraction/ExtrHaskellString.v +plugins/extraction/ExtrHaskellZInt.v +plugins/extraction/ExtrHaskellZInteger.v +plugins/extraction/ExtrHaskellZNum.v +plugins/extraction/ExtrOcamlBasic.v +plugins/extraction/ExtrOcamlBigIntConv.v +plugins/extraction/ExtrOcamlIntConv.v +plugins/extraction/ExtrOcamlNatBigInt.v +plugins/extraction/ExtrOcamlNatInt.v +plugins/extraction/ExtrOcamlString.v +plugins/extraction/ExtrOcamlZBigInt.v +plugins/extraction/ExtrOcamlZInt.v +plugins/extraction/Extraction.v +plugins/funind/FunInd.v +plugins/funind/Recdef.v +plugins/ltac/Ltac.v +plugins/micromega/Env.v +plugins/micromega/EnvRing.v +plugins/micromega/Fourier.v +plugins/micromega/Fourier_util.v +plugins/micromega/Lia.v +plugins/micromega/Lqa.v +plugins/micromega/Lra.v +plugins/micromega/MExtraction.v +plugins/micromega/OrderedRing.v +plugins/micromega/Psatz.v +plugins/micromega/QMicromega.v +plugins/micromega/RMicromega.v +plugins/micromega/Refl.v +plugins/micromega/RingMicromega.v +plugins/micromega/Tauto.v +plugins/micromega/VarMap.v +plugins/micromega/ZCoeff.v +plugins/micromega/ZMicromega.v +plugins/nsatz/Nsatz.v +plugins/omega/Omega.v +plugins/omega/OmegaLemmas.v +plugins/omega/OmegaPlugin.v +plugins/omega/OmegaTactic.v +plugins/omega/PreOmega.v +plugins/quote/Quote.v +plugins/romega/ROmega.v +plugins/romega/ReflOmegaCore.v +plugins/rtauto/Bintree.v +plugins/rtauto/Rtauto.v +plugins/setoid_ring/Algebra_syntax.v +plugins/setoid_ring/ArithRing.v +plugins/setoid_ring/BinList.v +plugins/setoid_ring/Cring.v +plugins/setoid_ring/Field.v +plugins/setoid_ring/Field_tac.v +plugins/setoid_ring/Field_theory.v +plugins/setoid_ring/InitialRing.v +plugins/setoid_ring/Integral_domain.v +plugins/setoid_ring/NArithRing.v +plugins/setoid_ring/Ncring.v +plugins/setoid_ring/Ncring_initial.v +plugins/setoid_ring/Ncring_polynom.v +plugins/setoid_ring/Ncring_tac.v +plugins/setoid_ring/RealField.v +plugins/setoid_ring/Ring.v +plugins/setoid_ring/Ring_base.v +plugins/setoid_ring/Ring_polynom.v +plugins/setoid_ring/Ring_tac.v +plugins/setoid_ring/Ring_theory.v +plugins/setoid_ring/Rings_Q.v +plugins/setoid_ring/Rings_R.v +plugins/setoid_ring/Rings_Z.v +plugins/setoid_ring/ZArithRing.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index e8f6decfbf..64164cc56f 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -588,6 +588,17 @@ through the <tt>Require Import</tt> command.</p> theories/Program/Combinators.v </dd> + <dt> <b>SSReflect</b>: + Base libraries for the SSReflect proof language and the + small scale reflection formalization technique + </dt> + <dd> + plugins/ssrmatching/ssrmatching.v + plugins/ssr/ssreflect.v + plugins/ssr/ssrbool.v + plugins/ssr/ssrfun.v + </dd> + <dt> <b>Unicode</b>: Unicode-based notations </dt> diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index 43802efa0a..bea6f24098 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -8,35 +8,32 @@ HIDDEN=$2 cp -f $FILE.template tmp echo -n "Building file index-list.prehtml... " -#LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Vectors Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings" -LIBDIRS=`find theories/* -type d ! -name .coq-native | sed -e "s:^theories/::"` +LIBDIRS=`find theories/* plugins/* -type d ! -name .coq-native` for k in $LIBDIRS; do - i=theories/$k - d=`basename $i` - ls $i | grep -q \.v'$' + d=`basename $k` + ls $k | grep -q \.v'$' if [ $? = 0 ]; then - for j in $i/*.v; do + for j in $k/*.v; do b=`basename $j .v` rm -f tmp2 - grep -q theories/$k/$b.v tmp + grep -q $k/$b.v tmp a=$? - grep -q theories/$k/$b.v $HIDDEN + grep -q $k/$b.v $HIDDEN h=$? if [ $a = 0 ]; then if [ $h = 0 ]; then - echo Error: $FILE and $HIDDEN both mention theories/$k/$b.v; exit 1 + echo Error: $FILE and $HIDDEN both mention $k/$b.v; exit 1 else - p=`echo $k | sed 's:/:.:g'` - sed -e "s:theories/$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2 + p=`echo $k | sed 's:^[^/]*/::' | sed 's:/:.:g'` + sed -e "s:$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2 mv -f tmp2 tmp fi else if [ $h = 0 ]; then - echo Error: theories/$k/$b.v is missing in the template file - exit 1 + echo Warning: $k/$b.v will be hidden from the index else - echo Error: none of $FILE and $HIDDEN mention theories/$k/$b.v + echo Error: none of $FILE and $HIDDEN mention $k/$b.v exit 1 fi diff --git a/engine/evd.ml b/engine/evd.ml index b3848e1b5b..6345046431 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -891,6 +891,9 @@ let make_flexible_variable evd ~algebraic u = { evd with universes = UState.make_flexible_variable evd.universes ~algebraic u } +let make_nonalgebraic_variable evd u = + { evd with universes = UState.make_nonalgebraic_variable evd.universes u } + (****************************************) (* Operations on constants *) (****************************************) diff --git a/engine/evd.mli b/engine/evd.mli index be54bebcd7..0a8d1f3287 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -561,6 +561,9 @@ val universe_rigidity : evar_map -> Univ.Level.t -> rigid val make_flexible_variable : evar_map -> algebraic:bool -> Univ.Level.t -> evar_map (** See [UState.make_flexible_variable] *) +val make_nonalgebraic_variable : evar_map -> Univ.Level.t -> evar_map +(** See [UState.make_nonalgebraic_variable]. *) + val is_sort_variable : evar_map -> Sorts.t -> Univ.Level.t option (** [is_sort_variable evm s] returns [Some u] or [None] if [s] is not a local sort variable declared in [evm] *) diff --git a/engine/uState.ml b/engine/uState.ml index aa7ec63a6f..5747ae2ad4 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -101,13 +101,21 @@ let context ctx = Univ.ContextSet.to_context ctx.uctx_local let const_univ_entry ~poly uctx = let open Entries in - if poly then Polymorphic_const_entry (context uctx) + if poly then + let (binders, _) = uctx.uctx_names in + let uctx = context uctx in + let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in + Polymorphic_const_entry (nas, uctx) else Monomorphic_const_entry (context_set uctx) (* does not support cumulativity since you need more info *) let ind_univ_entry ~poly uctx = let open Entries in - if poly then Polymorphic_ind_entry (context uctx) + if poly then + let (binders, _) = uctx.uctx_names in + let uctx = context uctx in + let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in + Polymorphic_ind_entry (nas, uctx) else Monomorphic_ind_entry (context_set uctx) let of_context_set ctx = { empty with uctx_local = ctx } @@ -140,7 +148,25 @@ let of_binders b = in { ctx with uctx_names = b, rmap } -let universe_binders ctx = fst ctx.uctx_names +let invent_name (named,cnt) u = + let rec aux i = + let na = Id.of_string ("u"^(string_of_int i)) in + if Id.Map.mem na named then aux (i+1) + else Id.Map.add na u named, i+1 + in + aux cnt + +let universe_binders ctx = + let open Univ in + let named, rev = ctx.uctx_names in + let named, _ = LSet.fold (fun u named -> + match LMap.find u rev with + | exception Not_found -> (* not sure if possible *) invent_name named u + | { uname = None } -> invent_name named u + | { uname = Some _ } -> named) + (ContextSet.levels ctx.uctx_local) (named, 0) + in + named let instantiate_variable l b v = try v := Univ.LMap.set l (Some b) !v @@ -394,8 +420,11 @@ let check_univ_decl ~poly uctx decl = let ctx = let names = decl.univdecl_instance in let extensible = decl.univdecl_extensible_instance in - if poly - then Entries.Polymorphic_const_entry (universe_context ~names ~extensible uctx) + if poly then + let (binders, _) = uctx.uctx_names in + let uctx = universe_context ~names ~extensible uctx in + let nas = UnivNames.compute_instance_binders (Univ.UContext.instance uctx) binders in + Entries.Polymorphic_const_entry (nas, uctx) else let () = check_universe_context_set ~names ~extensible uctx in Entries.Monomorphic_const_entry uctx.uctx_local @@ -566,6 +595,9 @@ let make_flexible_variable ctx ~algebraic u = {ctx with uctx_univ_variables = uvars'; uctx_univ_algebraic = avars'} +let make_nonalgebraic_variable ctx u = + { ctx with uctx_univ_algebraic = Univ.LSet.remove u ctx.uctx_univ_algebraic } + let make_flexible_nonalgebraic ctx = {ctx with uctx_univ_algebraic = Univ.LSet.empty} diff --git a/engine/uState.mli b/engine/uState.mli index 8053a7bf83..ad0cd5c1bb 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -126,9 +126,15 @@ val add_global_univ : t -> Univ.Level.t -> t Turn the variable [l] flexible, and algebraic if [algebraic] is true and [l] can be. That is if there are no strict upper constraints on [l] and and it does not appear in the instance of any non-algebraic - universe. Otherwise the variable is just made flexible. *) + universe. Otherwise the variable is just made flexible. + + If [l] is already algebraic it will remain so even with [algebraic:false]. *) val make_flexible_variable : t -> algebraic:bool -> Univ.Level.t -> t +val make_nonalgebraic_variable : t -> Univ.Level.t -> t +(** Make the level non algebraic. Undefined behaviour on + already-defined algebraics. *) + (** Turn all undefined flexible algebraic variables into simply flexible ones. Can be used in case the variables might appear in universe instances (typically for polymorphic program obligations). *) diff --git a/engine/univNames.ml b/engine/univNames.ml index a71f9c5736..ad91d31f87 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -36,69 +36,28 @@ type universe_binders = Univ.Level.t Names.Id.Map.t let empty_binders = Id.Map.empty -let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders" - -let universe_binders_of_global ref : Id.t list = - try - let l = GlobRef.Map.find ref !universe_binders_table in l - with Not_found -> [] - -let cache_ubinder (_,(ref,l)) = - universe_binders_table := GlobRef.Map.add ref l !universe_binders_table - -let subst_ubinder (subst,(ref,l as orig)) = - let ref' = fst (Globnames.subst_global subst ref) in - if ref == ref' then orig else ref', l +let universe_binders_of_global ref : Name.t array = + try AUContext.names (Environ.universes_of_global (Global.env ()) ref) + with Not_found -> [||] let name_universe lvl = (** Best-effort naming from the string representation of the level. This is completely hackish and should be solved in upper layers instead. *) Id.of_string_soft (Level.to_string lvl) -let discharge_ubinder (_,(ref,l)) = - (** Expand polymorphic binders with the section context *) - let info = Lib.section_segment_of_reference ref in - let sec_inst = Array.to_list (Instance.to_array (info.Lib.abstr_subst)) in - let map lvl = match Level.name lvl with - | None -> (* Having Prop/Set/Var as section universes makes no sense *) - assert false - | Some na -> - try - let qid = Nametab.shortest_qualid_of_universe na in - snd (Libnames.repr_qualid qid) - with Not_found -> name_universe lvl - in - let l = List.map map sec_inst @ l in - Some (ref, l) - -let ubinder_obj : GlobRef.t * Id.t list -> Libobject.obj = - let open Libobject in - declare_object { (default_object "universe binder") with - cache_function = cache_ubinder; - load_function = (fun _ x -> cache_ubinder x); - classify_function = (fun x -> Substitute x); - subst_function = subst_ubinder; - discharge_function = discharge_ubinder; - rebuild_function = (fun x -> x); } - -let register_universe_binders ref ubinders = - (** TODO: change the API to register a [Name.t list] instead. This is the last - part of the code that depends on the internal representation of names in - abstract contexts, but removing it requires quite a rework of the - callers. *) - let univs = AUContext.instance (Environ.universes_of_global (Global.env()) ref) in +let compute_instance_binders inst ubinders = let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in let map lvl = - try LMap.find lvl revmap - with Not_found -> name_universe lvl + try Name (LMap.find lvl revmap) + with Not_found -> Name (name_universe lvl) in - let ubinders = Array.map_to_list map (Instance.to_array univs) in - if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders)) + Array.map map (Instance.to_array inst) type univ_name_list = Names.lname list let universe_binders_with_opt_names ref names = let orig = universe_binders_of_global ref in + let orig = Array.to_list orig in let udecl = match names with | None -> orig | Some udecl -> @@ -106,11 +65,14 @@ let universe_binders_with_opt_names ref names = List.map2 (fun orig {CAst.v = na} -> match na with | Anonymous -> orig - | Name id -> id) orig udecl + | Name id -> Name id) orig udecl with Invalid_argument _ -> let len = List.length orig in CErrors.user_err ~hdr:"universe_binders_with_opt_names" Pp.(str "Universe instance should have length " ++ int len) in - let fold i acc na = Names.Id.Map.add na (Level.var i) acc in + let fold i acc na = match na with + | Name id -> Names.Id.Map.add id (Level.var i) acc + | Anonymous -> acc + in List.fold_left_i fold 0 empty_binders udecl diff --git a/engine/univNames.mli b/engine/univNames.mli index bd4062ade4..dc669f45d6 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -19,7 +19,7 @@ type universe_binders = Univ.Level.t Names.Id.Map.t val empty_binders : universe_binders -val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit +val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t array type univ_name_list = Names.lname list diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index b882d2164f..715b8cd23f 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -75,9 +75,9 @@ let is_ident x = function let make_extend loc self cl = match cl with | [[ExtNonTerminal (Uentry e, Some id)], act] when is_ident id act -> (** Special handling of identity arguments by not redeclaring an entry *) - <:expr< Vernacentries.Arg_alias $lid:e$ >> + <:expr< Vernacextend.Arg_alias $lid:e$ >> | _ -> - <:expr< Vernacentries.Arg_rules $mlexpr_of_list (make_rule loc self) (List.rev cl)$ >> + <:expr< Vernacextend.Arg_rules $mlexpr_of_list (make_rule loc self) (List.rev cl)$ >> let warning_deprecated prefix s = function | None -> () @@ -144,9 +144,9 @@ let declare_vernac_argument loc s pr cl = let pr_rules = match pr with | None -> <:expr< fun _ -> Pp.str $str:"[No printer for "^s^"]"$ >> | Some pr -> <:expr< $lid:pr$ >> in - declare_arg loc s <:expr< Vernacentries.vernac_argument_extend ~{ name = $se$ } { - Vernacentries.arg_printer = $pr_rules$; - Vernacentries.arg_parsing = $make_extend loc s cl$ + declare_arg loc s <:expr< Vernacextend.vernac_argument_extend ~{ name = $se$ } { + Vernacextend.arg_printer = $pr_rules$; + Vernacextend.arg_parsing = $make_extend loc s cl$ } >> open Pcaml diff --git a/grammar/dune b/grammar/dune index f03fe07607..78df2826d6 100644 --- a/grammar/dune +++ b/grammar/dune @@ -1,8 +1,7 @@ (library - (name grammar) + (name grammar5) (synopsis "Coq Camlp5 Grammar Extensions for Plugins") (public_name coq.grammar) - (wrapped false) (flags (:standard -w -58)) (libraries camlp5)) @@ -14,7 +13,7 @@ (rule (targets coqp5) - (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar.cmxa} -o coqp5))) + (action (run mkcamlp5.opt pa_o.cmx pa_op.cmx pr_dump.cmx pa_extend.cmx q_MLast.cmx pa_macro.cmx pr_o.cmx %{dep:grammar5.cmxa} -o coqp5))) (install (section bin) diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp index 3c401e827e..d44eeef670 100644 --- a/grammar/vernacextend.mlp +++ b/grammar/vernacextend.mlp @@ -25,24 +25,24 @@ type rule = { } let rec mlexpr_of_clause = function -| [] -> <:expr< Vernacentries.TyNil >> -| ExtTerminal s :: cl -> <:expr< Vernacentries.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >> +| [] -> <:expr< Vernacextend.TyNil >> +| ExtTerminal s :: cl -> <:expr< Vernacextend.TyTerminal ($str:s$, $mlexpr_of_clause cl$) >> | ExtNonTerminal (g, id) :: cl -> - <:expr< Vernacentries.TyNonTerminal ($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >> + <:expr< Vernacextend.TyNonTerminal ($mlexpr_of_symbol g$, $mlexpr_of_clause cl$) >> let make_rule r = let ty = mlexpr_of_clause r.r_patt in let cmd = binders_of_tokens r.r_branch r.r_patt in let make_classifier c = binders_of_tokens c r.r_patt in let classif = mlexpr_of_option make_classifier r.r_class in - <:expr< Vernacentries.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >> + <:expr< Vernacextend.TyML ($mlexpr_of_bool r.r_depr$, $ty$, $cmd$, $classif$) >> let declare_command loc s c nt cl = let se = mlexpr_of_string s in let c = mlexpr_of_option (fun x -> x) c in let rules = mlexpr_of_list make_rule cl in declare_str_items loc - [ <:str_item< Vernacentries.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ] + [ <:str_item< Vernacextend.vernac_extend ?{ classifier = $c$ } ~{ command = $se$ } ?{ entry = $nt$ } $rules$ >> ] open Pcaml diff --git a/interp/declare.ml b/interp/declare.ml index 7a32018c0e..a9bfe8cabb 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -219,7 +219,7 @@ let cache_variable ((sp,_),o) = let (body, uctx), () = Future.force de.const_entry_body in let poly, univs = match de.const_entry_universes with | Monomorphic_const_entry uctx -> false, uctx - | Polymorphic_const_entry uctx -> true, Univ.ContextSet.of_context uctx + | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx in let univs = Univ.ContextSet.union uctx univs in (** We must declare the universe constraints before type-checking the @@ -339,7 +339,7 @@ let infer_inductive_subtyping mind_ent = match mind_ent.mind_entry_universes with | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> mind_ent - | Cumulative_ind_entry cumi -> + | Cumulative_ind_entry (_, cumi) -> begin let env = Global.env () in (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *) @@ -366,14 +366,14 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter | Monomorphic_ind_entry _ -> (** Global constraints already defined through the inductive *) Monomorphic_const_entry Univ.ContextSet.empty - | Polymorphic_ind_entry ctx -> - Polymorphic_const_entry ctx - | Cumulative_ind_entry ctx -> - Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx) + | Polymorphic_ind_entry (nas, ctx) -> + Polymorphic_const_entry (nas, ctx) + | Cumulative_ind_entry (nas, ctx) -> + Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context ctx) in let term, types = match univs with | Monomorphic_const_entry _ -> term, types - | Polymorphic_const_entry ctx -> + | Polymorphic_const_entry (_, ctx) -> let u = Univ.UContext.instance ctx in Vars.subst_instance_constr u term, Vars.subst_instance_constr u types in @@ -473,36 +473,33 @@ type universe_source = type universe_name_decl = universe_source * (Id.t * Nametab.universe_id) list let check_exists sp = - let depth = sections_depth () in - let sp = Libnames.make_path (pop_dirpath_n depth (dirpath sp)) (basename sp) in if Nametab.exists_universe sp then alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists") else () -let qualify_univ i sp src id = - let open Libnames in +let qualify_univ i dp src id = match src with | BoundUniv | UnqualifiedUniv -> - let sp = dirpath sp in - i, make_path sp id + i, Libnames.make_path dp id | QualifiedUniv l -> - let sp = dirpath sp in - let sp = DirPath.repr sp in - Nametab.map_visibility succ i, make_path (DirPath.make (l::sp)) id + let dp = DirPath.repr dp in + Nametab.map_visibility succ i, Libnames.make_path (DirPath.make (l::dp)) id -let do_univ_name ~check i sp src (id,univ) = - let i, sp = qualify_univ i sp src id in +let do_univ_name ~check i dp src (id,univ) = + let i, sp = qualify_univ i dp src id in if check then check_exists sp; Nametab.push_universe i sp univ let cache_univ_names ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:true (Nametab.Until 1) sp src) univs + let depth = sections_depth () in + let dp = pop_dirpath_n depth (dirpath sp) in + List.iter (do_univ_name ~check:true (Nametab.Until 1) dp src) univs let load_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Until i) sp src) univs + List.iter (do_univ_name ~check:false (Nametab.Until i) (dirpath sp) src) univs let open_univ_names i ((sp, _), (src, univs)) = - List.iter (do_univ_name ~check:false (Nametab.Exactly i) sp src) univs + List.iter (do_univ_name ~check:false (Nametab.Exactly i) (dirpath sp) src) univs let discharge_univ_names = function | _, (BoundUniv, _) -> None @@ -520,12 +517,12 @@ let input_univ_names : universe_name_decl -> Libobject.obj = let declare_univ_binders gr pl = if Global.is_polymorphic gr then - UnivNames.register_universe_binders gr pl + () else let l = match gr with | ConstRef c -> Label.to_id @@ Constant.label c | IndRef (c, _) -> Label.to_id @@ MutInd.label c - | VarRef id -> id + | VarRef id -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on variable " ++ Id.print id ++ str".") | ConstructRef _ -> anomaly ~label:"declare_univ_binders" Pp.(str "declare_univ_binders on an constructor reference") diff --git a/interp/discharge.ml b/interp/discharge.ml index 21b2e85e8f..eeda5a6867 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -79,13 +79,15 @@ let process_inductive info modlist mib = | Monomorphic_ind ctx -> Univ.empty_level_subst, Monomorphic_ind_entry ctx | Polymorphic_ind auctx -> let subst, auctx = Lib.discharge_abstract_universe_context info auctx in + let nas = Univ.AUContext.names auctx in let auctx = Univ.AUContext.repr auctx in - subst, Polymorphic_ind_entry auctx + subst, Polymorphic_ind_entry (nas, auctx) | Cumulative_ind cumi -> let auctx = Univ.ACumulativityInfo.univ_context cumi in let subst, auctx = Lib.discharge_abstract_universe_context info auctx in + let nas = Univ.AUContext.names auctx in let auctx = Univ.AUContext.repr auctx in - subst, Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context auctx) + subst, Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context auctx) in let discharge c = Vars.subst_univs_level_constr subst (expmod_constr modlist c) in let inds = diff --git a/interp/modintern.ml b/interp/modintern.ml index 51e27299e3..60056dfd90 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -107,8 +107,8 @@ let transl_with_decl env base kind = function let c, ectx = interp_constr env sigma c in let poly = lookup_polymorphism env base kind fqid in begin match UState.check_univ_decl ~poly ectx udecl with - | Entries.Polymorphic_const_entry ctx -> - let inst, ctx = Univ.abstract_universes ctx in + | Entries.Polymorphic_const_entry (nas, ctx) -> + let inst, ctx = Univ.abstract_universes nas ctx in let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in let c = EConstr.to_constr sigma c in WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty diff --git a/kernel/entries.ml b/kernel/entries.ml index c5bcd74072..58bb782f15 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -30,8 +30,8 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1]; type inductive_universes = | Monomorphic_ind_entry of Univ.ContextSet.t - | Polymorphic_ind_entry of Univ.UContext.t - | Cumulative_ind_entry of Univ.CumulativityInfo.t + | Polymorphic_ind_entry of Name.t array * Univ.UContext.t + | Cumulative_ind_entry of Name.t array * Univ.CumulativityInfo.t type one_inductive_entry = { mind_entry_typename : Id.t; @@ -60,7 +60,7 @@ type 'a const_entry_body = 'a proof_output Future.computation type constant_universes_entry = | Monomorphic_const_entry of Univ.ContextSet.t - | Polymorphic_const_entry of Univ.UContext.t + | Polymorphic_const_entry of Name.t array * Univ.UContext.t type 'a in_constant_universes_entry = 'a * constant_universes_entry diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 0346026aa4..20c90bc05a 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -268,8 +268,8 @@ let typecheck_inductive env mie = let env' = match mie.mind_entry_universes with | Monomorphic_ind_entry ctx -> push_context_set ctx env - | Polymorphic_ind_entry ctx -> push_context ctx env - | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env + | Polymorphic_ind_entry (_, ctx) -> push_context ctx env + | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env in let env_params = check_context env' mie.mind_entry_params in let paramsctxt = mie.mind_entry_params in @@ -407,7 +407,7 @@ let typecheck_inductive env mie = match mie.mind_entry_universes with | Monomorphic_ind_entry _ -> () | Polymorphic_ind_entry _ -> () - | Cumulative_ind_entry cumi -> check_subtyping cumi paramsctxt env_arities inds + | Cumulative_ind_entry (_, cumi) -> check_subtyping cumi paramsctxt env_arities inds in (env_arities, env_ar_par, paramsctxt, inds) (************************************************************************) @@ -851,12 +851,12 @@ let compute_projections (kn, i as ind) mib = let abstract_inductive_universes iu = match iu with | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx) - | Polymorphic_ind_entry ctx -> - let (inst, auctx) = Univ.abstract_universes ctx in + | Polymorphic_ind_entry (nas, ctx) -> + let (inst, auctx) = Univ.abstract_universes nas ctx in let inst = Univ.make_instance_subst inst in (inst, Polymorphic_ind auctx) - | Cumulative_ind_entry cumi -> - let (inst, acumi) = Univ.abstract_cumulativity_info cumi in + | Cumulative_ind_entry (nas, cumi) -> + let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in let inst = Univ.make_instance_subst inst in (inst, Cumulative_ind acumi) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 8b11851bbb..df10398b2f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -682,7 +682,7 @@ let constant_entry_of_side_effect cb u = | Monomorphic_const uctx -> Monomorphic_const_entry uctx | Polymorphic_const auctx -> - Polymorphic_const_entry (Univ.AUContext.repr auctx) + Polymorphic_const_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx) in let pt = match cb.const_body, u with diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index fb1b3e236c..35fa871b4e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -68,8 +68,8 @@ let feedback_completion_typecheck = let abstract_constant_universes = function | Monomorphic_const_entry uctx -> Univ.empty_level_subst, Monomorphic_const uctx - | Polymorphic_const_entry uctx -> - let sbst, auctx = Univ.abstract_universes uctx in + | Polymorphic_const_entry (nas, uctx) -> + let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in sbst, Polymorphic_const auctx @@ -78,7 +78,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = | ParameterEntry (ctx,(t,uctx),nl) -> let env = match uctx with | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env - | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env + | Polymorphic_const_entry (_, uctx) -> push_context ~strict:false uctx env in let j = infer env t in let usubst, univs = abstract_constant_universes uctx in @@ -150,7 +150,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let ctx = Univ.ContextSet.union univs ctx in let env = push_context_set ~strict:true ctx env in env, Univ.empty_level_subst, Monomorphic_const ctx - | Polymorphic_const_entry uctx -> + | Polymorphic_const_entry (nas, uctx) -> (** Ensure not to generate internal constraints in polymorphic mode. The only way for this to happen would be that either the body contained deferred universes, or that it contains monomorphic @@ -160,7 +160,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = i.e. [trust] is always [Pure]. *) let () = assert (Univ.ContextSet.is_empty ctx) in let env = push_context ~strict:false uctx env in - let sbst, auctx = Univ.abstract_universes uctx in + let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in env, sbst, Polymorphic_const auctx in diff --git a/kernel/univ.ml b/kernel/univ.ml index d09b54e7ec..0edf750997 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -937,17 +937,30 @@ let hcons_universe_context = UContext.hcons module AUContext = struct - include UContext + type t = Names.Name.t array constrained let repr (inst, cst) = - (Array.mapi (fun i _l -> Level.var i) inst, cst) + (Array.init (Array.length inst) (fun i -> Level.var i), cst) - let pr f ?variance ctx = pr f ?variance (repr ctx) + let pr f ?variance ctx = UContext.pr f ?variance (repr ctx) let instantiate inst (u, cst) = assert (Array.length u = Array.length inst); subst_instance_constraints inst cst + let names (nas, _) = nas + + let hcons (univs, cst) = + (Array.map Names.Name.hcons univs, hcons_constraints cst) + + let empty = ([||], Constraint.empty) + + let is_empty (nas, cst) = Array.is_empty nas && Constraint.is_empty cst + + let union (nas, cst) (nas', cst') = (Array.append nas nas', Constraint.union cst cst') + + let size (nas, _) = Array.length nas + end let hcons_abstract_universe_context = AUContext.hcons @@ -993,7 +1006,22 @@ end let hcons_cumulativity_info = CumulativityInfo.hcons -module ACumulativityInfo = CumulativityInfo +module ACumulativityInfo = +struct + type t = AUContext.t * Variance.t array + + let pr prl (univs, variance) = + AUContext.pr prl ~variance univs + + let hcons (univs, variance) = (* should variance be hconsed? *) + (AUContext.hcons univs, variance) + + let univ_context (univs, _subtypcst) = univs + let variance (_univs, variance) = variance + + let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts + let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts +end let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons @@ -1145,19 +1173,20 @@ let make_inverse_instance_subst i = LMap.empty arr let make_abstract_instance (ctx, _) = - Array.mapi (fun i _l -> Level.var i) ctx + Array.init (Array.length ctx) (fun i -> Level.var i) -let abstract_universes ctx = +let abstract_universes nas ctx = let instance = UContext.instance ctx in + let () = assert (Int.equal (Array.length nas) (Instance.length instance)) in let subst = make_instance_subst instance in let cstrs = subst_univs_level_constraints subst (UContext.constraints ctx) in - let ctx = UContext.make (instance, cstrs) in + let ctx = (nas, cstrs) in instance, ctx -let abstract_cumulativity_info (univs, variance) = - let subst, univs = abstract_universes univs in +let abstract_cumulativity_info nas (univs, variance) = + let subst, univs = abstract_universes nas univs in subst, (univs, variance) let rec compact_univ s vars i u = diff --git a/kernel/univ.mli b/kernel/univ.mli index 7ac8247ca4..de7b334ae4 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -336,9 +336,6 @@ sig val empty : t val is_empty : t -> bool - (** Don't use. *) - val instance : t -> Instance.t - val size : t -> int (** Keeps the order of the instances *) @@ -347,6 +344,9 @@ sig val instantiate : Instance.t -> t -> Constraint.t (** Generate the set of instantiated Constraint.t **) + val names : t -> Names.Name.t array + (** Return the names of the bound universe variables *) + end (** Universe info for cumulative inductive types: A context of @@ -466,8 +466,8 @@ val make_instance_subst : Instance.t -> universe_level_subst val make_inverse_instance_subst : Instance.t -> universe_level_subst -val abstract_universes : UContext.t -> Instance.t * AUContext.t -val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativityInfo.t +val abstract_universes : Names.Name.t array -> UContext.t -> Instance.t * AUContext.t +val abstract_cumulativity_info : Names.Name.t array -> CumulativityInfo.t -> Instance.t * ACumulativityInfo.t (** TODO: move universe abstraction out of the kernel *) val make_abstract_instance : AUContext.t -> Instance.t diff --git a/lib/coqProject_file.ml b/lib/coqProject_file.ml index d0b01453a0..7395654022 100644 --- a/lib/coqProject_file.ml +++ b/lib/coqProject_file.ml @@ -220,7 +220,7 @@ let process_cmd_line orig_dir proj args = let f = CUnix.correct_path f orig_dir in let proj = if exists_dir f then { proj with subdirs = proj.subdirs @ [sourced f] } - else match CUnix.get_extension f with + else match Filename.extension f with | ".v" -> { proj with v_files = proj.v_files @ [sourced f] } | ".ml" -> { proj with ml_files = proj.ml_files @ [sourced f] } diff --git a/lib/system.ml b/lib/system.ml index eec007dcab..a9db95318f 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -83,7 +83,9 @@ let file_exists_respecting_case path f = let rec aux f = let bf = Filename.basename f in let df = Filename.dirname f in - (String.equal df "." || aux df) + (* When [df] is the same as [f], it means that the root of the file system + has been reached. There is no point in looking further up. *) + (String.equal df "." || String.equal f df || aux df) && exists_in_dir_respecting_case (Filename.concat path df) bf in (!trust_file_cache || Sys.file_exists (Filename.concat path f)) && aux f diff --git a/library/goptions.ml b/library/goptions.ml index dcbc46ab72..154b863fa1 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -73,7 +73,7 @@ module MakeTable = let _ = if String.List.mem_assoc nick !A.table then - user_err Pp.(str "Sorry, this table name is already used.") + user_err Pp.(str "Sorry, this table name (" ++ str nick ++ str ") is already used.") module MySet = Set.Make (struct type t = A.t let compare = A.compare end) @@ -216,11 +216,11 @@ let get_option key = OptionMap.find key !value_tab let check_key key = try let _ = get_option key in - user_err Pp.(str "Sorry, this option name is already used.") + user_err Pp.(str "Sorry, this option name ("++ str (nickname key) ++ str ") is already used.") with Not_found -> if String.List.mem_assoc (nickname key) !string_table || String.List.mem_assoc (nickname key) !ref_table - then user_err Pp.(str "Sorry, this option name is already used.") + then user_err Pp.(str "Sorry, this option name (" ++ str (nickname key) ++ str ") is already used.") open Libobject diff --git a/library/lib.ml b/library/lib.ml index 690a4fd53d..9c13cdafdb 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -479,7 +479,24 @@ let instance_from_variable_context = let named_of_variable_context = List.map fst - + +let name_instance inst = + (** FIXME: this should probably be done at an upper level, by storing the + name information in the section data structure. *) + let map lvl = match Univ.Level.name lvl with + | None -> (* Having Prop/Set/Var as section universes makes no sense *) + assert false + | Some na -> + try + let qid = Nametab.shortest_qualid_of_universe na in + Name (Libnames.qualid_basename qid) + with Not_found -> + (** Best-effort naming from the string representation of the level. + See univNames.ml for a similar hack. *) + Name (Id.of_string_soft (Univ.Level.to_string lvl)) + in + Array.map map (Univ.Instance.to_array inst) + let add_section_replacement f g poly hyps = match !sectab with | [] -> () @@ -488,7 +505,8 @@ let add_section_replacement f g poly hyps = let sechyps,ctx = extract_hyps (vars,hyps) in let ctx = Univ.ContextSet.to_context ctx in let inst = Univ.UContext.instance ctx in - let subst, ctx = Univ.abstract_universes ctx in + let nas = name_instance inst in + let subst, ctx = Univ.abstract_universes nas ctx in let args = instance_from_variable_context (List.rev sechyps) in let info = { abstr_ctx = sechyps; diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index fbdadbc0f2..eb3e633892 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -83,9 +83,13 @@ module type S = *) type 'a entry = 'a Entry.e + type internal_entry = Tok.t Gramext.g_entry + type symbol = Tok.t Gramext.g_symbol + type action = Gramext.g_action type coq_parsable val coq_parsable : ?file:Loc.source -> char Stream.t -> coq_parsable + val action : 'a -> action val entry_create : string -> 'a entry val entry_parse : 'a entry -> coq_parsable -> 'a @@ -96,6 +100,9 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct include Grammar.GMake(CLexer) type 'a entry = 'a Entry.e + type internal_entry = Tok.t Gramext.g_entry + type symbol = Tok.t Gramext.g_symbol + type action = Gramext.g_action type coq_parsable = parsable * CLexer.lexer_state ref @@ -106,6 +113,7 @@ end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e = struct state := CLexer.get_lexer_state (); (a,state) + let action = Gramext.action let entry_create = Entry.create let entry_parse e (p,state) = @@ -158,9 +166,16 @@ let of_coq_position = function | Extend.Level s -> Gramext.Level s module Symbols : sig - val stoken : Tok.t -> ('s, string) G.ty_symbol - val slist0sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol - val slist1sep : ('s, 'a) G.ty_symbol -> ('s, 'b) G.ty_symbol -> ('s, 'a list) G.ty_symbol + val stoken : Tok.t -> G.symbol + val sself : G.symbol + val snext : G.symbol + val slist0 : G.symbol -> G.symbol + val slist0sep : G.symbol * G.symbol -> G.symbol + val slist1 : G.symbol -> G.symbol + val slist1sep : G.symbol * G.symbol -> G.symbol + val sopt : G.symbol -> G.symbol + val snterml : G.internal_entry * string -> G.symbol + val snterm : G.internal_entry -> G.symbol end = struct let stoken tok = @@ -175,10 +190,19 @@ end = struct | Tok.BULLET s -> "BULLET", s | Tok.EOI -> "EOI", "" in - G.s_token pattern + Gramext.Stoken pattern + + let slist0sep (x, y) = Gramext.Slist0sep (x, y, false) + let slist1sep (x, y) = Gramext.Slist1sep (x, y, false) + + let snterml (x, y) = Gramext.Snterml (x, y) + let snterm x = Gramext.Snterm x + let sself = Gramext.Sself + let snext = Gramext.Snext + let slist0 x = Gramext.Slist0 x + let slist1 x = Gramext.Slist1 x + let sopt x = Gramext.Sopt x - let slist0sep x y = G.s_list0sep x y false - let slist1sep x y = G.s_list1sep x y false end let camlp5_verbosity silent f x = @@ -200,41 +224,40 @@ let camlp5_verbosity silent f x = (** Binding general entry keys to symbol *) -type ('s, 'a, 'r) casted_rule = Casted : ('s, 'b, 'r) G.ty_rule * ('a -> 'b) -> ('s, 'a, 'r) casted_rule - -let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> (s, a) G.ty_symbol = function -| Atoken t -> Symbols.stoken t -| Alist1 s -> G.s_list1 (symbol_of_prod_entry_key s) -| Alist1sep (s,sep) -> - Symbols.slist1sep (symbol_of_prod_entry_key s) (symbol_of_prod_entry_key sep) -| Alist0 s -> G.s_list0 (symbol_of_prod_entry_key s) -| Alist0sep (s,sep) -> - Symbols.slist0sep (symbol_of_prod_entry_key s) (symbol_of_prod_entry_key sep) -| Aopt s -> G.s_opt (symbol_of_prod_entry_key s) -| Aself -> G.s_self -| Anext -> G.s_next -| Aentry e -> G.s_nterm e -| Aentryl (e, n) -> G.s_nterml e n -| Arules rs -> G.s_rules (List.map symbol_of_rules rs) - -and symbol_of_rule : type s a r. (s, a, Loc.t -> r) Extend.rule -> (s, a, Ploc.t -> r) casted_rule = function -| Stop -> Casted (G.r_stop, fun act loc -> act (!@loc)) -| Next (r, s) -> - let Casted (r, cast) = symbol_of_rule r in - Casted (G.r_next r (symbol_of_prod_entry_key s), (fun act x -> cast (act x))) - -and symbol_of_rules : type a. a Extend.rules -> a G.ty_production = function +let rec of_coq_action : type a r. (r, a, Loc.t -> r) Extend.rule -> a -> G.action = function +| Stop -> fun f -> G.action (fun loc -> f (!@ loc)) +| Next (r, _) -> fun f -> G.action (fun x -> of_coq_action r (f x)) + +let rec symbol_of_prod_entry_key : type s a. (s, a) symbol -> _ = function + | Atoken t -> Symbols.stoken t + | Alist1 s -> Symbols.slist1 (symbol_of_prod_entry_key s) + | Alist1sep (s,sep) -> + Symbols.slist1sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep) + | Alist0 s -> Symbols.slist0 (symbol_of_prod_entry_key s) + | Alist0sep (s,sep) -> + Symbols.slist0sep (symbol_of_prod_entry_key s, symbol_of_prod_entry_key sep) + | Aopt s -> Symbols.sopt (symbol_of_prod_entry_key s) + | Aself -> Symbols.sself + | Anext -> Symbols.snext + | Aentry e -> + Symbols.snterm (G.Entry.obj e) + | Aentryl (e, n) -> + Symbols.snterml (G.Entry.obj e, n) + | Arules rs -> + Gramext.srules (List.map symbol_of_rules rs) + +and symbol_of_rule : type s a r. (s, a, r) Extend.rule -> _ = function +| Stop -> fun accu -> accu +| Next (r, s) -> fun accu -> symbol_of_rule r (symbol_of_prod_entry_key s :: accu) + +and symbol_of_rules : type a. a Extend.rules -> _ = function | Rules (r, act) -> - let Casted (symb, cast) = symbol_of_rule r.norec_rule in - G.production (symb, cast act) - -(** FIXME: This is a hack around a deficient camlp5 API *) -type 'a any_production = AnyProduction : ('a, 'f, Ploc.t -> 'a) G.ty_rule * 'f -> 'a any_production + let symb = symbol_of_rule r.norec_rule [] in + let act = of_coq_action r.norec_rule act in + (symb, act) -let of_coq_production_rule : type a. a Extend.production_rule -> a any_production = function -| Rule (toks, act) -> - let Casted (symb, cast) = symbol_of_rule toks in - AnyProduction (symb, cast act) +let of_coq_production_rule : type a. a Extend.production_rule -> _ = function +| Rule (toks, act) -> (symbol_of_rule toks [], of_coq_action toks act) let of_coq_single_extend_statement (lvl, assoc, rule) = (lvl, Option.map of_coq_assoc assoc, List.map of_coq_production_rule rule) @@ -242,13 +265,6 @@ let of_coq_single_extend_statement (lvl, assoc, rule) = let of_coq_extend_statement (pos, st) = (Option.map of_coq_position pos, List.map of_coq_single_extend_statement st) -let fix_extend_statement (pos, st) = - let fix_single_extend_statement (lvl, assoc, rules) = - let fix_production_rule (AnyProduction (s, act)) = G.production (s, act) in - (lvl, assoc, List.map fix_production_rule rules) - in - (pos, List.map fix_single_extend_statement st) - (** Type of reinitialization data *) type gram_reinit = gram_assoc * gram_position @@ -275,22 +291,6 @@ let camlp5_entries = ref EntryDataMap.empty let grammar_delete e reinit (pos,rls) = List.iter (fun (n,ass,lev) -> - List.iter (fun (AnyProduction (pil,_)) -> G.safe_delete_rule e pil) (List.rev lev)) - (List.rev rls); - match reinit with - | Some (a,ext) -> - let a = of_coq_assoc a in - let ext = of_coq_position ext in - let lev = match pos with - | Some (Gramext.Level n) -> n - | _ -> assert false - in - (G.safe_extend e) (Some ext) [Some lev,Some a,[]] - | None -> () - -let unsafe_grammar_delete e reinit (pos,rls) = - List.iter - (fun (n,ass,lev) -> List.iter (fun (pil,_) -> G.delete_rule e pil) (List.rev lev)) (List.rev rls); match reinit with @@ -309,15 +309,13 @@ let unsafe_grammar_delete e reinit (pos,rls) = let grammar_extend e reinit ext = let ext = of_coq_extend_statement ext in let undo () = grammar_delete e reinit ext in - let ext = fix_extend_statement ext in - let redo () = camlp5_verbosity false (uncurry (G.safe_extend e)) ext in + let redo () = camlp5_verbosity false (uncurry (G.extend e)) ext in camlp5_state := ByEXTEND (undo, redo) :: !camlp5_state; redo () let grammar_extend_sync e reinit ext = camlp5_state := ByGrammar (ExtendRule (e, reinit, ext)) :: !camlp5_state; - let ext = fix_extend_statement (of_coq_extend_statement ext) in - camlp5_verbosity false (uncurry (G.safe_extend e)) ext + camlp5_verbosity false (uncurry (G.extend e)) (of_coq_extend_statement ext) (** The apparent parser of Coq; encapsulate G to keep track of the extensions. *) @@ -329,7 +327,7 @@ module Gram = curry (fun ext -> camlp5_state := - (ByEXTEND ((fun () -> unsafe_grammar_delete e None ext), + (ByEXTEND ((fun () -> grammar_delete e None ext), (fun () -> uncurry (G.extend e) ext))) :: !camlp5_state; uncurry (G.extend e) ext) @@ -382,16 +380,16 @@ let make_rule r = [None, None, r] let eoi_entry en = let e = Entry.create ((Gram.Entry.name en) ^ "_eoi") in - let symbs = G.r_next (G.r_next G.r_stop (G.s_nterm en)) (Symbols.stoken Tok.EOI) in - let act = fun _ x loc -> x in - Gram.safe_extend e None (make_rule [G.production (symbs, act)]); + let symbs = [Symbols.snterm (Gram.Entry.obj en); Symbols.stoken Tok.EOI] in + let act = Gram.action (fun _ x loc -> x) in + uncurry (Gram.extend e) (None, make_rule [symbs, act]); e let map_entry f en = let e = Entry.create ((Gram.Entry.name en) ^ "_map") in - let symbs = G.r_next G.r_stop (G.s_nterm en) in - let act = fun x loc -> f x in - Gram.safe_extend e None (make_rule [G.production (symbs, act)]); + let symbs = [Symbols.snterm (Gram.Entry.obj en)] in + let act = Gram.action (fun x loc -> f x) in + uncurry (Gram.extend e) (None, make_rule [symbs, act]); e (* Parse a string, does NOT check if the entire string was read @@ -518,10 +516,10 @@ module Module = end let epsilon_value f e = - let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in - let ext = [None, None, [r]] in + let r = Rule (Next (Stop, e), fun x _ -> f x) in + let ext = of_coq_extend_statement (None, [None, None, [r]]) in let entry = Gram.entry_create "epsilon" in - let () = G.safe_extend entry None ext in + let () = uncurry (G.extend entry) ext in try Some (parse_string entry "") with _ -> None (** Synchronized grammar extensions *) diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index f26ec0f401..a6f432b5bd 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -333,9 +333,6 @@ let get_representative uf i= let get_constructors uf i= uf.map.(i).constructors -let find_pac uf i pac = - PacMap.find pac (get_constructors uf i) - let rec find_oldest_pac uf i pac= try PacMap.find pac (get_constructors uf i) with Not_found -> diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 4ebc6a135a..d52e83dc31 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -145,8 +145,6 @@ val tail_pac : pa_constructor -> pa_constructor val find : forest -> int -> int -val find_pac : forest -> int -> pa_constructor -> int - val find_oldest_pac : forest -> int -> pa_constructor -> int val term : forest -> int -> term diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index b9274cf6b8..1128a78093 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -89,8 +89,6 @@ END { -let fail_solver=tclFAIL 0 (Pp.str "GTauto failed") - let gen_ground_tac flag taco ids bases = let backup= !qflag in Proofview.tclOR begin diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index b0c4785d7a..832a98b7f8 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -21,7 +21,6 @@ open Termops open Formula open Sequent open Globnames -open Locus module NamedDecl = Context.Named.Declaration @@ -56,10 +55,6 @@ let wrap n b continue seq = continue seq2 end -let basename_of_global=function - VarRef id->id - | _->assert false - let clear_global=function VarRef id-> clear [id] | _->tclIDTAC @@ -230,19 +225,3 @@ let ll_forall_tac prod backtrack id continue seq= backtrack (* rules for instantiation with unification moved to instances.ml *) - -(* special for compatibility with old Intuition *) - -let constant str = Coqlib.lib_ref str - -let defined_connectives = lazy - [AllOccurrences, EvalConstRef (destConstRef (constant "core.not.type")); - AllOccurrences, EvalConstRef (destConstRef (constant "core.iff.type"))] - -let normalize_evaluables= - Proofview.Goal.enter begin fun gl -> - unfold_in_concl (Lazy.force defined_connectives) <*> - tclMAP - (fun id -> unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)) - (pf_ids_of_hyps gl) - end diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli index 924c26790c..97bc992b26 100644 --- a/plugins/firstorder/rules.mli +++ b/plugins/firstorder/rules.mli @@ -22,8 +22,6 @@ type 'a with_backtracking = tactic -> 'a val wrap : int -> bool -> seqtac -val basename_of_global: GlobRef.t -> Id.t - val clear_global: GlobRef.t -> tactic val axiom_tac : constr -> Sequent.t -> tactic @@ -51,5 +49,3 @@ val forall_tac : seqtac with_backtracking val left_exists_tac : pinductive -> lseqtac with_backtracking val ll_forall_tac : types -> lseqtac with_backtracking - -val normalize_evaluables : tactic diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 28a9542167..cd2ea3ef88 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -27,10 +27,6 @@ let array_get_start a = (Array.length a - 1) (fun i -> a.(i)) -let id_of_name = function - Name id -> id - | _ -> raise Not_found - let locate qid = Nametab.locate qid let locate_ind ref = @@ -105,15 +101,6 @@ let const_of_id id = CErrors.user_err ~hdr:"IndFun.const_of_id" (str "cannot find " ++ Id.print id) -let def_of_const t = - match Constr.kind t with - Const sp -> - (try (match Environ.constant_opt_value_in (Global.env()) sp with - | Some c -> c - | _ -> assert false) - with Not_found -> assert false) - |_ -> assert false - [@@@ocaml.warning "-3"] let coq_constant s = UnivGen.constr_of_monomorphic_global @@ diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 1b4c1248a5..0c8f40c5cf 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -18,8 +18,6 @@ val get_name : Id.t list -> ?default:string -> Name.t -> Name.t val array_get_start : 'a array -> 'a array -val id_of_name : Name.t -> Id.t - val locate_ind : Libnames.qualid -> inductive val locate_constant : Libnames.qualid -> Constant.t val locate_with_msg : @@ -38,7 +36,6 @@ val chop_rlambda_n : int -> Glob_term.glob_constr -> val chop_rprod_n : int -> Glob_term.glob_constr -> (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr -val def_of_const : Constr.t -> Constr.t val eq : EConstr.constr Lazy.t val refl_equal : EConstr.constr Lazy.t val const_of_id: Id.t -> GlobRef.t(* constantyes *) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 0f88734caf..1b212334ce 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -700,7 +700,7 @@ type ('b, 'c) argument_interp = (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp type ('a, 'b, 'c) tactic_argument = { - arg_parsing : 'a Vernacentries.argument_rule; + arg_parsing : 'a Vernacextend.argument_rule; arg_tag : 'c Val.tag option; arg_intern : ('a, 'b) argument_intern; arg_subst : 'b argument_subst; @@ -751,10 +751,10 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) = in let () = register_interp0 wit (interp_fun name arg tag) in let entry = match arg.arg_parsing with - | Vernacentries.Arg_alias e -> + | Vernacextend.Arg_alias e -> let () = Pcoq.register_grammar wit e in e - | Vernacentries.Arg_rules rules -> + | Vernacextend.Arg_rules rules -> let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in e diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index c93d6251e0..79f9e093fb 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -128,7 +128,7 @@ type ('b, 'c) argument_interp = (Geninterp.interp_sign -> Proof_type.goal Evd.sigma -> 'b -> Evd.evar_map * 'c) -> ('b, 'c) argument_interp type ('a, 'b, 'c) tactic_argument = { - arg_parsing : 'a Vernacentries.argument_rule; + arg_parsing : 'a Vernacextend.argument_rule; arg_tag : 'c Geninterp.Val.tag option; arg_intern : ('a, 'b) argument_intern; arg_subst : 'b argument_subst; diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 4626378db6..9173e23b89 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -88,20 +88,9 @@ let subst_reference subst = (*CSC: subst_global_reference is used "only" for RefArgType, that propagates to the syntactic non-terminals "global", used in commands such as Print. It is also used for non-evaluable references. *) -open Pp -open Printer let subst_global_reference subst = - let subst_global ref = - let ref',t' = subst_global subst ref in - if not (is_global ref' t') then - (let sigma, env = Pfedit.get_current_context () in - Feedback.msg_warning (strbrk "The reference " ++ pr_global ref ++ str " is not " ++ - str " expanded to \"" ++ pr_lconstr_env env sigma t' ++ str "\", but to " ++ - pr_global ref')); - ref' - in - subst_or_var (subst_located subst_global) + subst_or_var (subst_located (subst_global_reference subst)) let subst_evaluable subst = let subst_eval_ref = subst_evaluable_reference subst in diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index 0865f75ec5..a618fc781f 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -10,264 +10,266 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **) + Require Bool. Require Import ssreflect ssrfun. -(******************************************************************************) -(* A theory of boolean predicates and operators. A large part of this file is *) -(* concerned with boolean reflection. *) -(* Definitions and notations: *) -(* is_true b == the coercion of b : bool to Prop (:= b = true). *) -(* This is just input and displayed as `b''. *) -(* reflect P b == the reflection inductive predicate, asserting *) -(* that the logical proposition P : prop with the *) -(* formula b : bool. Lemmas asserting reflect P b *) -(* are often referred to as "views". *) -(* iffP, appP, sameP, rwP :: lemmas for direct manipulation of reflection *) -(* views: iffP is used to prove reflection from *) -(* logical equivalence, appP to compose views, and *) -(* sameP and rwP to perform boolean and setoid *) -(* rewriting. *) -(* elimT :: coercion reflect >-> Funclass, which allows the *) -(* direct application of `reflect' views to *) -(* boolean assertions. *) -(* decidable P <-> P is effectively decidable (:= {P} + {~ P}. *) -(* contra, contraL, ... :: contraposition lemmas. *) -(* altP my_viewP :: natural alternative for reflection; given *) -(* lemma myviewP: reflect my_Prop my_formula, *) -(* have [myP | not_myP] := altP my_viewP. *) -(* generates two subgoals, in which my_formula has *) -(* been replaced by true and false, resp., with *) -(* new assumptions myP : my_Prop and *) -(* not_myP: ~~ my_formula. *) -(* Caveat: my_formula must be an APPLICATION, not *) -(* a variable, constant, let-in, etc. (due to the *) -(* poor behaviour of dependent index matching). *) -(* boolP my_formula :: boolean disjunction, equivalent to *) -(* altP (idP my_formula) but circumventing the *) -(* dependent index capture issue; destructing *) -(* boolP my_formula generates two subgoals with *) -(* assumtions my_formula and ~~ myformula. As *) -(* with altP, my_formula must be an application. *) -(* \unless C, P <-> we can assume property P when a something that *) -(* holds under condition C (such as C itself). *) -(* := forall G : Prop, (C -> G) -> (P -> G) -> G. *) -(* This is just C \/ P or rather its impredicative *) -(* encoding, whose usage better fits the above *) -(* description: given a lemma UCP whose conclusion *) -(* is \unless C, P we can assume P by writing: *) -(* wlog hP: / P by apply/UCP; (prove C -> goal). *) -(* or even apply: UCP id _ => hP if the goal is C. *) -(* classically P <-> we can assume P when proving is_true b. *) -(* := forall b : bool, (P -> b) -> b. *) -(* This is equivalent to ~ (~ P) when P : Prop. *) -(* implies P Q == wrapper variant type that coerces to P -> Q and *) -(* can be used as a P -> Q view unambigously. *) -(* Useful to avoid spurious insertion of <-> views *) -(* when Q is a conjunction of foralls, as in Lemma *) -(* all_and2 below; conversely, avoids confusion in *) -(* apply views for impredicative properties, such *) -(* as \unless C, P. Also supports contrapositives. *) -(* a && b == the boolean conjunction of a and b. *) -(* a || b == the boolean disjunction of a and b. *) -(* a ==> b == the boolean implication of b by a. *) -(* ~~ a == the boolean negation of a. *) -(* a (+) b == the boolean exclusive or (or sum) of a and b. *) -(* [ /\ P1 , P2 & P3 ] == multiway logical conjunction, up to 5 terms. *) -(* [ \/ P1 , P2 | P3 ] == multiway logical disjunction, up to 4 terms. *) -(* [&& a, b, c & d] == iterated, right associative boolean conjunction *) -(* with arbitrary arity. *) -(* [|| a, b, c | d] == iterated, right associative boolean disjunction *) -(* with arbitrary arity. *) -(* [==> a, b, c => d] == iterated, right associative boolean implication *) -(* with arbitrary arity. *) -(* and3P, ... == specific reflection lemmas for iterated *) -(* connectives. *) -(* andTb, orbAC, ... == systematic names for boolean connective *) -(* properties (see suffix conventions below). *) -(* prop_congr == a tactic to move a boolean equality from *) -(* its coerced form in Prop to the equality *) -(* in bool. *) -(* bool_congr == resolution tactic for blindly weeding out *) -(* like terms from boolean equalities (can fail). *) -(* This file provides a theory of boolean predicates and relations: *) -(* pred T == the type of bool predicates (:= T -> bool). *) -(* simpl_pred T == the type of simplifying bool predicates, using *) -(* the simpl_fun from ssrfun.v. *) -(* rel T == the type of bool relations. *) -(* := T -> pred T or T -> T -> bool. *) -(* simpl_rel T == type of simplifying relations. *) -(* predType == the generic predicate interface, supported for *) -(* for lists and sets. *) -(* pred_class == a coercion class for the predType projection to *) -(* pred; declaring a coercion to pred_class is an *) -(* alternative way of equipping a type with a *) -(* predType structure, which interoperates better *) -(* with coercion subtyping. This is used, e.g., *) -(* for finite sets, so that finite groups inherit *) -(* the membership operation by coercing to sets. *) -(* If P is a predicate the proposition "x satisfies P" can be written *) -(* applicatively as (P x), or using an explicit connective as (x \in P); in *) -(* the latter case we say that P is a "collective" predicate. We use A, B *) -(* rather than P, Q for collective predicates: *) -(* x \in A == x satisfies the (collective) predicate A. *) -(* x \notin A == x doesn't satisfy the (collective) predicate A. *) -(* The pred T type can be used as a generic predicate type for either kind, *) -(* but the two kinds of predicates should not be confused. When a "generic" *) -(* pred T value of one type needs to be passed as the other the following *) -(* conversions should be used explicitly: *) -(* SimplPred P == a (simplifying) applicative equivalent of P. *) -(* mem A == an applicative equivalent of A: *) -(* mem A x simplifies to x \in A. *) -(* Alternatively one can use the syntax for explicit simplifying predicates *) -(* and relations (in the following x is bound in E): *) -(* [pred x | E] == simplifying (see ssrfun) predicate x => E. *) -(* [pred x : T | E] == predicate x => E, with a cast on the argument. *) -(* [pred : T | P] == constant predicate P on type T. *) -(* [pred x | E1 & E2] == [pred x | E1 && E2]; an x : T cast is allowed. *) -(* [pred x in A] == [pred x | x in A]. *) -(* [pred x in A | E] == [pred x | x in A & E]. *) -(* [pred x in A | E1 & E2] == [pred x in A | E1 && E2]. *) -(* [predU A & B] == union of two collective predicates A and B. *) -(* [predI A & B] == intersection of collective predicates A and B. *) -(* [predD A & B] == difference of collective predicates A and B. *) -(* [predC A] == complement of the collective predicate A. *) -(* [preim f of A] == preimage under f of the collective predicate A. *) -(* predU P Q, ... == union, etc of applicative predicates. *) -(* pred0 == the empty predicate. *) -(* predT == the total (always true) predicate. *) -(* if T : predArgType, then T coerces to predT. *) -(* {: T} == T cast to predArgType (e.g., {: bool * nat}) *) -(* In the following, x and y are bound in E: *) -(* [rel x y | E] == simplifying relation x, y => E. *) -(* [rel x y : T | E] == simplifying relation with arguments cast. *) -(* [rel x y in A & B | E] == [rel x y | [&& x \in A, y \in B & E]]. *) -(* [rel x y in A & B] == [rel x y | (x \in A) && (y \in B)]. *) -(* [rel x y in A | E] == [rel x y in A & A | E]. *) -(* [rel x y in A] == [rel x y in A & A]. *) -(* relU R S == union of relations R and S. *) -(* Explicit values of type pred T (i.e., lamdba terms) should always be used *) -(* applicatively, while values of collection types implementing the predType *) -(* interface, such as sequences or sets should always be used as collective *) -(* predicates. Defined constants and functions of type pred T or simpl_pred T *) -(* as well as the explicit simpl_pred T values described below, can generally *) -(* be used either way. Note however that x \in A will not auto-simplify when *) -(* A is an explicit simpl_pred T value; the generic simplification rule inE *) -(* must be used (when A : pred T, the unfold_in rule can be used). Constants *) -(* of type pred T with an explicit simpl_pred value do not auto-simplify when *) -(* used applicatively, but can still be expanded with inE. This behavior can *) -(* be controlled as follows: *) -(* Let A : collective_pred T := [pred x | ... ]. *) -(* The collective_pred T type is just an alias for pred T, but this cast *) -(* stops rewrite inE from expanding the definition of A, thus treating A *) -(* into an abstract collection (unfold_in or in_collective can be used to *) -(* expand manually). *) -(* Let A : applicative_pred T := [pred x | ...]. *) -(* This cast causes inE to turn x \in A into the applicative A x form; *) -(* A will then have to unfolded explicitly with the /A rule. This will *) -(* also apply to any definition that reduces to A (e.g., Let B := A). *) -(* Canonical A_app_pred := ApplicativePred A. *) -(* This declaration, given after definition of A, similarly causes inE to *) -(* turn x \in A into A x, but in addition allows the app_predE rule to *) -(* turn A x back into x \in A; it can be used for any definition of type *) -(* pred T, which makes it especially useful for ambivalent predicates *) -(* as the relational transitive closure connect, that are used in both *) -(* applicative and collective styles. *) -(* Purely for aesthetics, we provide a subtype of collective predicates: *) -(* qualifier q T == a pred T pretty-printing wrapper. An A : qualifier q T *) -(* coerces to pred_class and thus behaves as a collective *) -(* predicate, but x \in A and x \notin A are displayed as: *) -(* x \is A and x \isn't A when q = 0, *) -(* x \is a A and x \isn't a A when q = 1, *) -(* x \is an A and x \isn't an A when q = 2, respectively. *) -(* [qualify x | P] := Qualifier 0 (fun x => P), constructor for the above. *) -(* [qualify x : T | P], [qualify a x | P], [qualify an X | P], etc. *) -(* variants of the above with type constraints and different *) -(* values of q. *) -(* We provide an internal interface to support attaching properties (such as *) -(* being multiplicative) to predicates: *) -(* pred_key p == phantom type that will serve as a support for properties *) -(* to be attached to p : pred_class; instances should be *) -(* created with Fact/Qed so as to be opaque. *) -(* KeyedPred k_p == an instance of the interface structure that attaches *) -(* (k_p : pred_key P) to P; the structure projection is a *) -(* coercion to pred_class. *) -(* KeyedQualifier k_q == an instance of the interface structure that attaches *) -(* (k_q : pred_key q) to (q : qualifier n T). *) -(* DefaultPredKey p == a default value for pred_key p; the vernacular command *) -(* Import DefaultKeying attaches this key to all predicates *) -(* that are not explicitly keyed. *) -(* Keys can be used to attach properties to predicates, qualifiers and *) -(* generic nouns in a way that allows them to be used transparently. The key *) -(* projection of a predicate property structure such as unsignedPred should *) -(* be a pred_key, not a pred, and corresponding lemmas will have the form *) -(* Lemma rpredN R S (oppS : @opprPred R S) (kS : keyed_pred oppS) : *) -(* {mono -%R: x / x \in kS}. *) -(* Because x \in kS will be displayed as x \in S (or x \is S, etc), the *) -(* canonical instance of opprPred will not normally be exposed (it will also *) -(* be erased by /= simplification). In addition each predicate structure *) -(* should have a DefaultPredKey Canonical instance that simply issues the *) -(* property as a proof obligation (which can be caught by the Prop-irrelevant *) -(* feature of the ssreflect plugin). *) -(* Some properties of predicates and relations: *) -(* A =i B <-> A and B are extensionally equivalent. *) -(* {subset A <= B} <-> A is a (collective) subpredicate of B. *) -(* subpred P Q <-> P is an (applicative) subpredicate or Q. *) -(* subrel R S <-> R is a subrelation of S. *) -(* In the following R is in rel T: *) -(* reflexive R <-> R is reflexive. *) -(* irreflexive R <-> R is irreflexive. *) -(* symmetric R <-> R (in rel T) is symmetric (equation). *) -(* pre_symmetric R <-> R is symmetric (implication). *) -(* antisymmetric R <-> R is antisymmetric. *) -(* total R <-> R is total. *) -(* transitive R <-> R is transitive. *) -(* left_transitive R <-> R is a congruence on its left hand side. *) -(* right_transitive R <-> R is a congruence on its right hand side. *) -(* equivalence_rel R <-> R is an equivalence relation. *) -(* Localization of (Prop) predicates; if P1 is convertible to forall x, Qx, *) -(* P2 to forall x y, Qxy and P3 to forall x y z, Qxyz : *) -(* {for y, P1} <-> Qx{y / x}. *) -(* {in A, P1} <-> forall x, x \in A -> Qx. *) -(* {in A1 & A2, P2} <-> forall x y, x \in A1 -> y \in A2 -> Qxy. *) -(* {in A &, P2} <-> forall x y, x \in A -> y \in A -> Qxy. *) -(* {in A1 & A2 & A3, Q3} <-> forall x y z, *) -(* x \in A1 -> y \in A2 -> z \in A3 -> Qxyz. *) -(* {in A1 & A2 &, Q3} == {in A1 & A2 & A2, Q3}. *) -(* {in A1 && A3, Q3} == {in A1 & A1 & A3, Q3}. *) -(* {in A &&, Q3} == {in A & A & A, Q3}. *) -(* {in A, bijective f} == f has a right inverse in A. *) -(* {on C, P1} == forall x, (f x) \in C -> Qx *) -(* when P1 is also convertible to Pf f. *) -(* {on C &, P2} == forall x y, f x \in C -> f y \in C -> Qxy *) -(* when P2 is also convertible to Pf f. *) -(* {on C, P1' & g} == forall x, (f x) \in cd -> Qx *) -(* when P1' is convertible to Pf f *) -(* and P1' g is convertible to forall x, Qx. *) -(* {on C, bijective f} == f has a right inverse on C. *) -(* This file extends the lemma name suffix conventions of ssrfun as follows: *) -(* A -- associativity, as in andbA : associative andb. *) -(* AC -- right commutativity. *) -(* ACA -- self-interchange (inner commutativity), e.g., *) -(* orbACA : (a || b) || (c || d) = (a || c) || (b || d). *) -(* b -- a boolean argument, as in andbb : idempotent andb. *) -(* C -- commutativity, as in andbC : commutative andb, *) -(* or predicate complement, as in predC. *) -(* CA -- left commutativity. *) -(* D -- predicate difference, as in predD. *) -(* E -- elimination, as in negbFE : ~~ b = false -> b. *) -(* F or f -- boolean false, as in andbF : b && false = false. *) -(* I -- left/right injectivity, as in addbI : right_injective addb, *) -(* or predicate intersection, as in predI. *) -(* l -- a left-hand operation, as andb_orl : left_distributive andb orb. *) -(* N or n -- boolean negation, as in andbN : a && (~~ a) = false. *) -(* P -- a characteristic property, often a reflection lemma, as in *) -(* andP : reflect (a /\ b) (a && b). *) -(* r -- a right-hand operation, as orb_andr : rightt_distributive orb andb. *) -(* T or t -- boolean truth, as in andbT: right_id true andb. *) -(* U -- predicate union, as in predU. *) -(* W -- weakening, as in in1W : {in D, forall x, P} -> forall x, P. *) -(******************************************************************************) +(** + A theory of boolean predicates and operators. A large part of this file is + concerned with boolean reflection. + Definitions and notations: + is_true b == the coercion of b : bool to Prop (:= b = true). + This is just input and displayed as `b''. + reflect P b == the reflection inductive predicate, asserting + that the logical proposition P : prop with the + formula b : bool. Lemmas asserting reflect P b + are often referred to as "views". + iffP, appP, sameP, rwP :: lemmas for direct manipulation of reflection + views: iffP is used to prove reflection from + logical equivalence, appP to compose views, and + sameP and rwP to perform boolean and setoid + rewriting. + elimT :: coercion reflect >-> Funclass, which allows the + direct application of `reflect' views to + boolean assertions. + decidable P <-> P is effectively decidable (:= {P} + {~ P}. + contra, contraL, ... :: contraposition lemmas. + altP my_viewP :: natural alternative for reflection; given + lemma myviewP: reflect my_Prop my_formula, + have #[#myP | not_myP#]# := altP my_viewP. + generates two subgoals, in which my_formula has + been replaced by true and false, resp., with + new assumptions myP : my_Prop and + not_myP: ~~ my_formula. + Caveat: my_formula must be an APPLICATION, not + a variable, constant, let-in, etc. (due to the + poor behaviour of dependent index matching). + boolP my_formula :: boolean disjunction, equivalent to + altP (idP my_formula) but circumventing the + dependent index capture issue; destructing + boolP my_formula generates two subgoals with + assumtions my_formula and ~~ myformula. As + with altP, my_formula must be an application. + \unless C, P <-> we can assume property P when a something that + holds under condition C (such as C itself). + := forall G : Prop, (C -> G) -> (P -> G) -> G. + This is just C \/ P or rather its impredicative + encoding, whose usage better fits the above + description: given a lemma UCP whose conclusion + is \unless C, P we can assume P by writing: + wlog hP: / P by apply/UCP; (prove C -> goal). + or even apply: UCP id _ => hP if the goal is C. + classically P <-> we can assume P when proving is_true b. + := forall b : bool, (P -> b) -> b. + This is equivalent to ~ (~ P) when P : Prop. + implies P Q == wrapper variant type that coerces to P -> Q and + can be used as a P -> Q view unambigously. + Useful to avoid spurious insertion of <-> views + when Q is a conjunction of foralls, as in Lemma + all_and2 below; conversely, avoids confusion in + apply views for impredicative properties, such + as \unless C, P. Also supports contrapositives. + a && b == the boolean conjunction of a and b. + a || b == the boolean disjunction of a and b. + a ==> b == the boolean implication of b by a. + ~~ a == the boolean negation of a. + a (+) b == the boolean exclusive or (or sum) of a and b. + #[# /\ P1 , P2 & P3 #]# == multiway logical conjunction, up to 5 terms. + #[# \/ P1 , P2 | P3 #]# == multiway logical disjunction, up to 4 terms. + #[#&& a, b, c & d#]# == iterated, right associative boolean conjunction + with arbitrary arity. + #[#|| a, b, c | d#]# == iterated, right associative boolean disjunction + with arbitrary arity. + #[#==> a, b, c => d#]# == iterated, right associative boolean implication + with arbitrary arity. + and3P, ... == specific reflection lemmas for iterated + connectives. + andTb, orbAC, ... == systematic names for boolean connective + properties (see suffix conventions below). + prop_congr == a tactic to move a boolean equality from + its coerced form in Prop to the equality + in bool. + bool_congr == resolution tactic for blindly weeding out + like terms from boolean equalities (can fail). + This file provides a theory of boolean predicates and relations: + pred T == the type of bool predicates (:= T -> bool). + simpl_pred T == the type of simplifying bool predicates, using + the simpl_fun from ssrfun.v. + rel T == the type of bool relations. + := T -> pred T or T -> T -> bool. + simpl_rel T == type of simplifying relations. + predType == the generic predicate interface, supported for + for lists and sets. + pred_class == a coercion class for the predType projection to + pred; declaring a coercion to pred_class is an + alternative way of equipping a type with a + predType structure, which interoperates better + with coercion subtyping. This is used, e.g., + for finite sets, so that finite groups inherit + the membership operation by coercing to sets. + If P is a predicate the proposition "x satisfies P" can be written + applicatively as (P x), or using an explicit connective as (x \in P); in + the latter case we say that P is a "collective" predicate. We use A, B + rather than P, Q for collective predicates: + x \in A == x satisfies the (collective) predicate A. + x \notin A == x doesn't satisfy the (collective) predicate A. + The pred T type can be used as a generic predicate type for either kind, + but the two kinds of predicates should not be confused. When a "generic" + pred T value of one type needs to be passed as the other the following + conversions should be used explicitly: + SimplPred P == a (simplifying) applicative equivalent of P. + mem A == an applicative equivalent of A: + mem A x simplifies to x \in A. + Alternatively one can use the syntax for explicit simplifying predicates + and relations (in the following x is bound in E): + #[#pred x | E#]# == simplifying (see ssrfun) predicate x => E. + #[#pred x : T | E#]# == predicate x => E, with a cast on the argument. + #[#pred : T | P#]# == constant predicate P on type T. + #[#pred x | E1 & E2#]# == #[#pred x | E1 && E2#]#; an x : T cast is allowed. + #[#pred x in A#]# == #[#pred x | x in A#]#. + #[#pred x in A | E#]# == #[#pred x | x in A & E#]#. + #[#pred x in A | E1 & E2#]# == #[#pred x in A | E1 && E2#]#. + #[#predU A & B#]# == union of two collective predicates A and B. + #[#predI A & B#]# == intersection of collective predicates A and B. + #[#predD A & B#]# == difference of collective predicates A and B. + #[#predC A#]# == complement of the collective predicate A. + #[#preim f of A#]# == preimage under f of the collective predicate A. + predU P Q, ... == union, etc of applicative predicates. + pred0 == the empty predicate. + predT == the total (always true) predicate. + if T : predArgType, then T coerces to predT. + {: T} == T cast to predArgType (e.g., {: bool * nat}) + In the following, x and y are bound in E: + #[#rel x y | E#]# == simplifying relation x, y => E. + #[#rel x y : T | E#]# == simplifying relation with arguments cast. + #[#rel x y in A & B | E#]# == #[#rel x y | #[#&& x \in A, y \in B & E#]# #]#. + #[#rel x y in A & B#]# == #[#rel x y | (x \in A) && (y \in B) #]#. + #[#rel x y in A | E#]# == #[#rel x y in A & A | E#]#. + #[#rel x y in A#]# == #[#rel x y in A & A#]#. + relU R S == union of relations R and S. + Explicit values of type pred T (i.e., lamdba terms) should always be used + applicatively, while values of collection types implementing the predType + interface, such as sequences or sets should always be used as collective + predicates. Defined constants and functions of type pred T or simpl_pred T + as well as the explicit simpl_pred T values described below, can generally + be used either way. Note however that x \in A will not auto-simplify when + A is an explicit simpl_pred T value; the generic simplification rule inE + must be used (when A : pred T, the unfold_in rule can be used). Constants + of type pred T with an explicit simpl_pred value do not auto-simplify when + used applicatively, but can still be expanded with inE. This behavior can + be controlled as follows: + Let A : collective_pred T := #[#pred x | ... #]#. + The collective_pred T type is just an alias for pred T, but this cast + stops rewrite inE from expanding the definition of A, thus treating A + into an abstract collection (unfold_in or in_collective can be used to + expand manually). + Let A : applicative_pred T := #[#pred x | ... #]#. + This cast causes inE to turn x \in A into the applicative A x form; + A will then have to unfolded explicitly with the /A rule. This will + also apply to any definition that reduces to A (e.g., Let B := A). + Canonical A_app_pred := ApplicativePred A. + This declaration, given after definition of A, similarly causes inE to + turn x \in A into A x, but in addition allows the app_predE rule to + turn A x back into x \in A; it can be used for any definition of type + pred T, which makes it especially useful for ambivalent predicates + as the relational transitive closure connect, that are used in both + applicative and collective styles. + Purely for aesthetics, we provide a subtype of collective predicates: + qualifier q T == a pred T pretty-printing wrapper. An A : qualifier q T + coerces to pred_class and thus behaves as a collective + predicate, but x \in A and x \notin A are displayed as: + x \is A and x \isn't A when q = 0, + x \is a A and x \isn't a A when q = 1, + x \is an A and x \isn't an A when q = 2, respectively. + #[#qualify x | P#]# := Qualifier 0 (fun x => P), constructor for the above. + #[#qualify x : T | P#]#, #[#qualify a x | P#]#, #[#qualify an X | P#]#, etc. + variants of the above with type constraints and different + values of q. + We provide an internal interface to support attaching properties (such as + being multiplicative) to predicates: + pred_key p == phantom type that will serve as a support for properties + to be attached to p : pred_class; instances should be + created with Fact/Qed so as to be opaque. + KeyedPred k_p == an instance of the interface structure that attaches + (k_p : pred_key P) to P; the structure projection is a + coercion to pred_class. + KeyedQualifier k_q == an instance of the interface structure that attaches + (k_q : pred_key q) to (q : qualifier n T). + DefaultPredKey p == a default value for pred_key p; the vernacular command + Import DefaultKeying attaches this key to all predicates + that are not explicitly keyed. + Keys can be used to attach properties to predicates, qualifiers and + generic nouns in a way that allows them to be used transparently. The key + projection of a predicate property structure such as unsignedPred should + be a pred_key, not a pred, and corresponding lemmas will have the form + Lemma rpredN R S (oppS : @opprPred R S) (kS : keyed_pred oppS) : + {mono -%%R: x / x \in kS}. + Because x \in kS will be displayed as x \in S (or x \is S, etc), the + canonical instance of opprPred will not normally be exposed (it will also + be erased by /= simplification). In addition each predicate structure + should have a DefaultPredKey Canonical instance that simply issues the + property as a proof obligation (which can be caught by the Prop-irrelevant + feature of the ssreflect plugin). + Some properties of predicates and relations: + A =i B <-> A and B are extensionally equivalent. + {subset A <= B} <-> A is a (collective) subpredicate of B. + subpred P Q <-> P is an (applicative) subpredicate or Q. + subrel R S <-> R is a subrelation of S. + In the following R is in rel T: + reflexive R <-> R is reflexive. + irreflexive R <-> R is irreflexive. + symmetric R <-> R (in rel T) is symmetric (equation). + pre_symmetric R <-> R is symmetric (implication). + antisymmetric R <-> R is antisymmetric. + total R <-> R is total. + transitive R <-> R is transitive. + left_transitive R <-> R is a congruence on its left hand side. + right_transitive R <-> R is a congruence on its right hand side. + equivalence_rel R <-> R is an equivalence relation. + Localization of (Prop) predicates; if P1 is convertible to forall x, Qx, + P2 to forall x y, Qxy and P3 to forall x y z, Qxyz : + {for y, P1} <-> Qx{y / x}. + {in A, P1} <-> forall x, x \in A -> Qx. + {in A1 & A2, P2} <-> forall x y, x \in A1 -> y \in A2 -> Qxy. + {in A &, P2} <-> forall x y, x \in A -> y \in A -> Qxy. + {in A1 & A2 & A3, Q3} <-> forall x y z, + x \in A1 -> y \in A2 -> z \in A3 -> Qxyz. + {in A1 & A2 &, Q3} == {in A1 & A2 & A2, Q3}. + {in A1 && A3, Q3} == {in A1 & A1 & A3, Q3}. + {in A &&, Q3} == {in A & A & A, Q3}. + {in A, bijective f} == f has a right inverse in A. + {on C, P1} == forall x, (f x) \in C -> Qx + when P1 is also convertible to Pf f. + {on C &, P2} == forall x y, f x \in C -> f y \in C -> Qxy + when P2 is also convertible to Pf f. + {on C, P1' & g} == forall x, (f x) \in cd -> Qx + when P1' is convertible to Pf f + and P1' g is convertible to forall x, Qx. + {on C, bijective f} == f has a right inverse on C. + This file extends the lemma name suffix conventions of ssrfun as follows: + A -- associativity, as in andbA : associative andb. + AC -- right commutativity. + ACA -- self-interchange (inner commutativity), e.g., + orbACA : (a || b) || (c || d) = (a || c) || (b || d). + b -- a boolean argument, as in andbb : idempotent andb. + C -- commutativity, as in andbC : commutative andb, + or predicate complement, as in predC. + CA -- left commutativity. + D -- predicate difference, as in predD. + E -- elimination, as in negbFE : ~~ b = false -> b. + F or f -- boolean false, as in andbF : b && false = false. + I -- left/right injectivity, as in addbI : right_injective addb, + or predicate intersection, as in predI. + l -- a left-hand operation, as andb_orl : left_distributive andb orb. + N or n -- boolean negation, as in andbN : a && (~~ a) = false. + P -- a characteristic property, often a reflection lemma, as in + andP : reflect (a /\ b) (a && b). + r -- a right-hand operation, as orb_andr : rightt_distributive orb andb. + T or t -- boolean truth, as in andbT: right_id true andb. + U -- predicate union, as in predU. + W -- weakening, as in in1W : {in D, forall x, P} -> forall x, P. **) + Set Implicit Arguments. Unset Strict Implicit. @@ -288,23 +290,24 @@ Reserved Notation "x \notin A" Reserved Notation "p1 =i p2" (at level 70, format "'[hv' p1 '/ ' =i p2 ']'", no associativity). -(* We introduce a number of n-ary "list-style" notations that share a common *) -(* format, namely *) -(* [op arg1, arg2, ... last_separator last_arg] *) -(* This usually denotes a right-associative applications of op, e.g., *) -(* [&& a, b, c & d] denotes a && (b && (c && d)) *) -(* The last_separator must be a non-operator token. Here we use &, | or =>; *) -(* our default is &, but we try to match the intended meaning of op. The *) -(* separator is a workaround for limitations of the parsing engine; the same *) -(* limitations mean the separator cannot be omitted even when last_arg can. *) -(* The Notation declarations are complicated by the separate treatment for *) -(* some fixed arities (binary for bool operators, and all arities for Prop *) -(* operators). *) -(* We also use the square brackets in comprehension-style notations *) -(* [type var separator expr] *) -(* where "type" is the type of the comprehension (e.g., pred) and "separator" *) -(* is | or => . It is important that in other notations a leading square *) -(* bracket [ is always followed by an operator symbol or a fixed identifier. *) +(** + We introduce a number of n-ary "list-style" notations that share a common + format, namely + #[#op arg1, arg2, ... last_separator last_arg#]# + This usually denotes a right-associative applications of op, e.g., + #[#&& a, b, c & d#]# denotes a && (b && (c && d)) + The last_separator must be a non-operator token. Here we use &, | or =>; + our default is &, but we try to match the intended meaning of op. The + separator is a workaround for limitations of the parsing engine; the same + limitations mean the separator cannot be omitted even when last_arg can. + The Notation declarations are complicated by the separate treatment for + some fixed arities (binary for bool operators, and all arities for Prop + operators). + We also use the square brackets in comprehension-style notations + #[#type var separator expr#]# + where "type" is the type of the comprehension (e.g., pred) and "separator" + is | or => . It is important that in other notations a leading square + bracket #[# is always followed by an operator symbol or a fixed identifier. **) Reserved Notation "[ /\ P1 & P2 ]" (at level 0, only parsing). Reserved Notation "[ /\ P1 , P2 & P3 ]" (at level 0, format @@ -344,19 +347,19 @@ Reserved Notation "[ 'rel' x y => E ]" (at level 0, x, y at level 8, format Reserved Notation "[ 'rel' x y : T => E ]" (at level 0, x, y at level 8, format "'[hv' [ 'rel' x y : T => '/ ' E ] ']'"). -(* Shorter delimiter *) +(** Shorter delimiter **) Delimit Scope bool_scope with B. Open Scope bool_scope. -(* An alternative to xorb that behaves somewhat better wrt simplification. *) +(** An alternative to xorb that behaves somewhat better wrt simplification. **) Definition addb b := if b then negb else id. -(* Notation for && and || is declared in Init.Datatypes. *) +(** Notation for && and || is declared in Init.Datatypes. **) Notation "~~ b" := (negb b) : bool_scope. Notation "b ==> c" := (implb b c) : bool_scope. Notation "b1 (+) b2" := (addb b1 b2) : bool_scope. -(* Constant is_true b := b = true is defined in Init.Datatypes. *) +(** Constant is_true b := b = true is defined in Init.Datatypes. **) Coercion is_true : bool >-> Sortclass. (* Prop *) Lemma prop_congr : forall b b' : bool, b = b' -> b = b' :> Prop. @@ -364,21 +367,22 @@ Proof. by move=> b b' ->. Qed. Ltac prop_congr := apply: prop_congr. -(* Lemmas for trivial. *) +(** Lemmas for trivial. **) Lemma is_true_true : true. Proof. by []. Qed. Lemma not_false_is_true : ~ false. Proof. by []. Qed. Lemma is_true_locked_true : locked true. Proof. by unlock. Qed. Hint Resolve is_true_true not_false_is_true is_true_locked_true. -(* Shorter names. *) +(** Shorter names. **) Definition isT := is_true_true. Definition notF := not_false_is_true. -(* Negation lemmas. *) +(** Negation lemmas. **) -(* We generally take NEGATION as the standard form of a false condition: *) -(* negative boolean hypotheses should be of the form ~~ b, rather than ~ b or *) -(* b = false, as much as possible. *) +(** + We generally take NEGATION as the standard form of a false condition: + negative boolean hypotheses should be of the form ~~ b, rather than ~ b or + b = false, as much as possible. **) Lemma negbT b : b = false -> ~~ b. Proof. by case: b. Qed. Lemma negbTE b : ~~ b -> b = false. Proof. by case: b. Qed. @@ -426,8 +430,9 @@ Proof. by move/contra=> notb_notc /notb_notc/negbTE. Qed. Lemma contraFF (c b : bool) : (c -> b) -> b = false -> c = false. Proof. by move/contraFN=> bF_notc /bF_notc/negbTE. Qed. -(* Coercion of sum-style datatypes into bool, which makes it possible *) -(* to use ssr's boolean if rather than Coq's "generic" if. *) +(** + Coercion of sum-style datatypes into bool, which makes it possible + to use ssr's boolean if rather than Coq's "generic" if. **) Coercion isSome T (u : option T) := if u is Some _ then true else false. @@ -441,16 +446,17 @@ Prenex Implicits isSome is_inl is_left is_inleft. Definition decidable P := {P} + {~ P}. -(* Lemmas for ifs with large conditions, which allow reasoning about the *) -(* condition without repeating it inside the proof (the latter IS *) -(* preferable when the condition is short). *) -(* Usage : *) -(* if the goal contains (if cond then ...) = ... *) -(* case: ifP => Hcond. *) -(* generates two subgoal, with the assumption Hcond : cond = true/false *) -(* Rewrite if_same eliminates redundant ifs *) -(* Rewrite (fun_if f) moves a function f inside an if *) -(* Rewrite if_arg moves an argument inside a function-valued if *) +(** + Lemmas for ifs with large conditions, which allow reasoning about the + condition without repeating it inside the proof (the latter IS + preferable when the condition is short). + Usage : + if the goal contains (if cond then ...) = ... + case: ifP => Hcond. + generates two subgoal, with the assumption Hcond : cond = true/false + Rewrite if_same eliminates redundant ifs + Rewrite (fun_if f) moves a function f inside an if + Rewrite if_arg moves an argument inside a function-valued if **) Section BoolIf. @@ -483,13 +489,13 @@ Lemma if_arg (fT fF : A -> B) : (if b then fT else fF) x = if b then fT x else fF x. Proof. by case b. Qed. -(* Turning a boolean "if" form into an application. *) +(** Turning a boolean "if" form into an application. **) Definition if_expr := if b then vT else vF. Lemma ifE : (if b then vT else vF) = if_expr. Proof. by []. Qed. End BoolIf. -(* Core (internal) reflection lemmas, used for the three kinds of views. *) +(** Core (internal) reflection lemmas, used for the three kinds of views. **) Section ReflectCore. @@ -517,7 +523,7 @@ Proof. by case Hb => [? _ H ? | ? H _]; case: H. Qed. End ReflectCore. -(* Internal negated reflection lemmas *) +(** Internal negated reflection lemmas **) Section ReflectNegCore. Variables (P Q : Prop) (b c : bool). @@ -537,7 +543,7 @@ Proof. by rewrite -if_neg; apply: xorPif. Qed. End ReflectNegCore. -(* User-oriented reflection lemmas *) +(** User-oriented reflection lemmas **) Section Reflect. Variables (P Q : Prop) (b b' c : bool). @@ -584,7 +590,7 @@ Lemma rwP : P <-> b. Proof. by split; [apply: introT | apply: elimT]. Qed. Lemma rwP2 : reflect Q b -> (P <-> Q). Proof. by move=> Qb; split=> ?; [apply: appP | apply: elimT; case: Qb]. Qed. -(* Predicate family to reflect excluded middle in bool. *) +(** Predicate family to reflect excluded middle in bool. **) Variant alt_spec : bool -> Type := | AltTrue of P : alt_spec true | AltFalse of ~~ b : alt_spec false. @@ -600,7 +606,7 @@ Hint View for apply/ introTF|3 introNTF|3 introTFn|3 elimT|2 elimTn|2 elimN|2. Hint View for apply// equivPif|3 xorPif|3 equivPifn|3 xorPifn|3. -(* Allow the direct application of a reflection lemma to a boolean assertion. *) +(** Allow the direct application of a reflection lemma to a boolean assertion. **) Coercion elimT : reflect >-> Funclass. Variant implies P Q := Implies of P -> Q. @@ -611,7 +617,7 @@ Coercion impliesP : implies >-> Funclass. Hint View for move/ impliesPn|2 impliesP|2. Hint View for apply/ impliesPn|2 impliesP|2. -(* Impredicative or, which can emulate a classical not-implies. *) +(** Impredicative or, which can emulate a classical not-implies. **) Definition unless condition property : Prop := forall goal : Prop, (condition -> goal) -> (property -> goal) -> goal. @@ -637,8 +643,9 @@ Proof. by split; apply=> [hC|hP]; [apply/unlessL/unlessL | apply/unlessR]. Qed. Lemma unless_contra b C : implies (~~ b -> C) (\unless C, b). Proof. by split; case: b => [_ | hC]; [apply/unlessR | apply/unlessL/hC]. Qed. -(* Classical reasoning becomes directly accessible for any bool subgoal. *) -(* Note that we cannot use "unless" here for lack of universe polymorphism. *) +(** + Classical reasoning becomes directly accessible for any bool subgoal. + Note that we cannot use "unless" here for lack of universe polymorphism. **) Definition classically P : Prop := forall b : bool, (P -> b) -> b. Lemma classicP (P : Prop) : classically P <-> ~ ~ P. @@ -669,11 +676,12 @@ move=> iPQ []// notPQ; apply/notPQ=> /iPQ-cQ. by case: notF; apply: cQ => hQ; apply: notPQ. Qed. -(* List notations for wider connectives; the Prop connectives have a fixed *) -(* width so as to avoid iterated destruction (we go up to width 5 for /\, and *) -(* width 4 for or). The bool connectives have arbitrary widths, but denote *) -(* expressions that associate to the RIGHT. This is consistent with the right *) -(* associativity of list expressions and thus more convenient in most proofs. *) +(** + List notations for wider connectives; the Prop connectives have a fixed + width so as to avoid iterated destruction (we go up to width 5 for /\, and + width 4 for or). The bool connectives have arbitrary widths, but denote + expressions that associate to the RIGHT. This is consistent with the right + associativity of list expressions and thus more convenient in most proofs. **) Inductive and3 (P1 P2 P3 : Prop) : Prop := And3 of P1 & P2 & P3. @@ -822,7 +830,7 @@ Arguments implyP [b1 b2]. Prenex Implicits idP idPn negP negPn negPf. Prenex Implicits andP and3P and4P and5P orP or3P or4P nandP norP implyP. -(* Shorter, more systematic names for the boolean connectives laws. *) +(** Shorter, more systematic names for the boolean connectives laws. **) Lemma andTb : left_id true andb. Proof. by []. Qed. Lemma andFb : left_zero false andb. Proof. by []. Qed. @@ -880,14 +888,14 @@ Proof. by case: a; case: b. Qed. Lemma negb_or (a b : bool) : ~~ (a || b) = ~~ a && ~~ b. Proof. by case: a; case: b. Qed. -(* Pseudo-cancellation -- i.e, absorbtion *) +(** Pseudo-cancellation -- i.e, absorbtion **) Lemma andbK a b : a && b || a = a. Proof. by case: a; case: b. Qed. Lemma andKb a b : a || b && a = a. Proof. by case: a; case: b. Qed. Lemma orbK a b : (a || b) && a = a. Proof. by case: a; case: b. Qed. Lemma orKb a b : a && (b || a) = a. Proof. by case: a; case: b. Qed. -(* Imply *) +(** Imply **) Lemma implybT b : b ==> true. Proof. by case: b. Qed. Lemma implybF b : (b ==> false) = ~~ b. Proof. by case: b. Qed. @@ -917,7 +925,7 @@ Proof. by case: a; case: b => // ->. Qed. Lemma implyb_id2l (a b c : bool) : (a -> b = c) -> (a ==> b) = (a ==> c). Proof. by case: a; case: b; case: c => // ->. Qed. -(* Addition (xor) *) +(** Addition (xor) **) Lemma addFb : left_id false addb. Proof. by []. Qed. Lemma addbF : right_id false addb. Proof. by case. Qed. @@ -946,9 +954,10 @@ Lemma addbP a b : reflect (~~ a = b) (a (+) b). Proof. by case: a; case: b; constructor. Qed. Arguments addbP [a b]. -(* Resolution tactic for blindly weeding out common terms from boolean *) -(* equalities. When faced with a goal of the form (andb/orb/addb b1 b2) = b3 *) -(* they will try to locate b1 in b3 and remove it. This can fail! *) +(** + Resolution tactic for blindly weeding out common terms from boolean + equalities. When faced with a goal of the form (andb/orb/addb b1 b2) = b3 + they will try to locate b1 in b3 and remove it. This can fail! **) Ltac bool_congr := match goal with @@ -963,100 +972,101 @@ Ltac bool_congr := | |- (~~ ?X1 = ?X2) => congr 1 negb end. -(******************************************************************************) -(* Predicates, i.e., packaged functions to bool. *) -(* - pred T, the basic type for predicates over a type T, is simply an alias *) -(* for T -> bool. *) -(* We actually distinguish two kinds of predicates, which we call applicative *) -(* and collective, based on the syntax used to test them at some x in T: *) -(* - For an applicative predicate P, one uses prefix syntax: *) -(* P x *) -(* Also, most operations on applicative predicates use prefix syntax as *) -(* well (e.g., predI P Q). *) -(* - For a collective predicate A, one uses infix syntax: *) -(* x \in A *) -(* and all operations on collective predicates use infix syntax as well *) -(* (e.g., [predI A & B]). *) -(* There are only two kinds of applicative predicates: *) -(* - pred T, the alias for T -> bool mentioned above *) -(* - simpl_pred T, an alias for simpl_fun T bool with a coercion to pred T *) -(* that auto-simplifies on application (see ssrfun). *) -(* On the other hand, the set of collective predicate types is open-ended via *) -(* - predType T, a Structure that can be used to put Canonical collective *) -(* predicate interpretation on other types, such as lists, tuples, *) -(* finite sets, etc. *) -(* Indeed, we define such interpretations for applicative predicate types, *) -(* which can therefore also be used with the infix syntax, e.g., *) -(* x \in predI P Q *) -(* Moreover these infix forms are convertible to their prefix counterpart *) -(* (e.g., predI P Q x which in turn simplifies to P x && Q x). The converse *) -(* is not true, however; collective predicate types cannot, in general, be *) -(* general, be used applicatively, because of the "uniform inheritance" *) -(* restriction on implicit coercions. *) -(* However, we do define an explicit generic coercion *) -(* - mem : forall (pT : predType), pT -> mem_pred T *) -(* where mem_pred T is a variant of simpl_pred T that preserves the infix *) -(* syntax, i.e., mem A x auto-simplifies to x \in A. *) -(* Indeed, the infix "collective" operators are notation for a prefix *) -(* operator with arguments of type mem_pred T or pred T, applied to coerced *) -(* collective predicates, e.g., *) -(* Notation "x \in A" := (in_mem x (mem A)). *) -(* This prevents the variability in the predicate type from interfering with *) -(* the application of generic lemmas. Moreover this also makes it much easier *) -(* to define generic lemmas, because the simplest type -- pred T -- can be *) -(* used as the type of generic collective predicates, provided one takes care *) -(* not to use it applicatively; this avoids the burden of having to declare a *) -(* different predicate type for each predicate parameter of each section or *) -(* lemma. *) -(* This trick is made possible by the fact that the constructor of the *) -(* mem_pred T type aligns the unification process, forcing a generic *) -(* "collective" predicate A : pred T to unify with the actual collective B, *) -(* which mem has coerced to pred T via an internal, hidden implicit coercion, *) -(* supplied by the predType structure for B. Users should take care not to *) -(* inadvertently "strip" (mem B) down to the coerced B, since this will *) -(* expose the internal coercion: Coq will display a term B x that cannot be *) -(* typed as such. The topredE lemma can be used to restore the x \in B *) -(* syntax in this case. While -topredE can conversely be used to change *) -(* x \in P into P x, it is safer to use the inE and memE lemmas instead, as *) -(* they do not run the risk of exposing internal coercions. As a consequence *) -(* it is better to explicitly cast a generic applicative pred T to simpl_pred *) -(* using the SimplPred constructor, when it is used as a collective predicate *) -(* (see, e.g., Lemma eq_big in bigop). *) -(* We also sometimes "instantiate" the predType structure by defining a *) -(* coercion to the sort of the predPredType structure. This works better for *) -(* types such as {set T} that have subtypes that coerce to them, since the *) -(* same coercion will be inserted by the application of mem. It also lets us *) -(* turn any Type aT : predArgType into the total predicate over that type, *) -(* i.e., fun _: aT => true. This allows us to write, e.g., #|'I_n| for the *) -(* cardinal of the (finite) type of integers less than n. *) -(* Collective predicates have a specific extensional equality, *) -(* - A =i B, *) -(* while applicative predicates use the extensional equality of functions, *) -(* - P =1 Q *) -(* The two forms are convertible, however. *) -(* We lift boolean operations to predicates, defining: *) -(* - predU (union), predI (intersection), predC (complement), *) -(* predD (difference), and preim (preimage, i.e., composition) *) -(* For each operation we define three forms, typically: *) -(* - predU : pred T -> pred T -> simpl_pred T *) -(* - [predU A & B], a Notation for predU (mem A) (mem B) *) -(* - xpredU, a Notation for the lambda-expression inside predU, *) -(* which is mostly useful as an argument of =1, since it exposes the head *) -(* head constant of the expression to the ssreflect matching algorithm. *) -(* The syntax for the preimage of a collective predicate A is *) -(* - [preim f of A] *) -(* Finally, the generic syntax for defining a simpl_pred T is *) -(* - [pred x : T | P(x)], [pred x | P(x)], [pred x in A | P(x)], etc. *) -(* We also support boolean relations, but only the applicative form, with *) -(* types *) -(* - rel T, an alias for T -> pred T *) -(* - simpl_rel T, an auto-simplifying version, and syntax *) -(* [rel x y | P(x,y)], [rel x y in A & B | P(x,y)], etc. *) -(* The notation [rel of fA] can be used to coerce a function returning a *) -(* collective predicate to one returning pred T. *) -(* Finally, note that there is specific support for ambivalent predicates *) -(* that can work in either style, as per this file's head descriptor. *) -(******************************************************************************) + +(** + Predicates, i.e., packaged functions to bool. + - pred T, the basic type for predicates over a type T, is simply an alias + for T -> bool. + We actually distinguish two kinds of predicates, which we call applicative + and collective, based on the syntax used to test them at some x in T: + - For an applicative predicate P, one uses prefix syntax: + P x + Also, most operations on applicative predicates use prefix syntax as + well (e.g., predI P Q). + - For a collective predicate A, one uses infix syntax: + x \in A + and all operations on collective predicates use infix syntax as well + (e.g., #[#predI A & B#]#). + There are only two kinds of applicative predicates: + - pred T, the alias for T -> bool mentioned above + - simpl_pred T, an alias for simpl_fun T bool with a coercion to pred T + that auto-simplifies on application (see ssrfun). + On the other hand, the set of collective predicate types is open-ended via + - predType T, a Structure that can be used to put Canonical collective + predicate interpretation on other types, such as lists, tuples, + finite sets, etc. + Indeed, we define such interpretations for applicative predicate types, + which can therefore also be used with the infix syntax, e.g., + x \in predI P Q + Moreover these infix forms are convertible to their prefix counterpart + (e.g., predI P Q x which in turn simplifies to P x && Q x). The converse + is not true, however; collective predicate types cannot, in general, be + general, be used applicatively, because of the "uniform inheritance" + restriction on implicit coercions. + However, we do define an explicit generic coercion + - mem : forall (pT : predType), pT -> mem_pred T + where mem_pred T is a variant of simpl_pred T that preserves the infix + syntax, i.e., mem A x auto-simplifies to x \in A. + Indeed, the infix "collective" operators are notation for a prefix + operator with arguments of type mem_pred T or pred T, applied to coerced + collective predicates, e.g., + Notation "x \in A" := (in_mem x (mem A)). + This prevents the variability in the predicate type from interfering with + the application of generic lemmas. Moreover this also makes it much easier + to define generic lemmas, because the simplest type -- pred T -- can be + used as the type of generic collective predicates, provided one takes care + not to use it applicatively; this avoids the burden of having to declare a + different predicate type for each predicate parameter of each section or + lemma. + This trick is made possible by the fact that the constructor of the + mem_pred T type aligns the unification process, forcing a generic + "collective" predicate A : pred T to unify with the actual collective B, + which mem has coerced to pred T via an internal, hidden implicit coercion, + supplied by the predType structure for B. Users should take care not to + inadvertently "strip" (mem B) down to the coerced B, since this will + expose the internal coercion: Coq will display a term B x that cannot be + typed as such. The topredE lemma can be used to restore the x \in B + syntax in this case. While -topredE can conversely be used to change + x \in P into P x, it is safer to use the inE and memE lemmas instead, as + they do not run the risk of exposing internal coercions. As a consequence + it is better to explicitly cast a generic applicative pred T to simpl_pred + using the SimplPred constructor, when it is used as a collective predicate + (see, e.g., Lemma eq_big in bigop). + We also sometimes "instantiate" the predType structure by defining a + coercion to the sort of the predPredType structure. This works better for + types such as {set T} that have subtypes that coerce to them, since the + same coercion will be inserted by the application of mem. It also lets us + turn any Type aT : predArgType into the total predicate over that type, + i.e., fun _: aT => true. This allows us to write, e.g., ##|'I_n| for the + cardinal of the (finite) type of integers less than n. + Collective predicates have a specific extensional equality, + - A =i B, + while applicative predicates use the extensional equality of functions, + - P =1 Q + The two forms are convertible, however. + We lift boolean operations to predicates, defining: + - predU (union), predI (intersection), predC (complement), + predD (difference), and preim (preimage, i.e., composition) + For each operation we define three forms, typically: + - predU : pred T -> pred T -> simpl_pred T + - #[#predU A & B#]#, a Notation for predU (mem A) (mem B) + - xpredU, a Notation for the lambda-expression inside predU, + which is mostly useful as an argument of =1, since it exposes the head + head constant of the expression to the ssreflect matching algorithm. + The syntax for the preimage of a collective predicate A is + - #[#preim f of A#]# + Finally, the generic syntax for defining a simpl_pred T is + - #[#pred x : T | P(x) #]#, #[#pred x | P(x) #]#, #[#pred x in A | P(x) #]#, etc. + We also support boolean relations, but only the applicative form, with + types + - rel T, an alias for T -> pred T + - simpl_rel T, an auto-simplifying version, and syntax + #[#rel x y | P(x,y) #]#, #[#rel x y in A & B | P(x,y) #]#, etc. + The notation #[#rel of fA#]# can be used to coerce a function returning a + collective predicate to one returning pred T. + Finally, note that there is specific support for ambivalent predicates + that can work in either style, as per this file's head descriptor. **) + Definition pred T := T -> bool. @@ -1094,8 +1104,9 @@ Coercion applicative_pred_of_simpl (p : simpl_pred) : applicative_pred := fun_of_simpl p. Coercion collective_pred_of_simpl (p : simpl_pred) : collective_pred := fun x => (let: SimplFun f := p in fun _ => f x) x. -(* Note: applicative_of_simpl is convertible to pred_of_simpl, while *) -(* collective_of_simpl is not. *) +(** + Note: applicative_of_simpl is convertible to pred_of_simpl, while + collective_of_simpl is not. **) Definition pred0 := SimplPred xpred0. Definition predT := SimplPred xpredT. @@ -1166,19 +1177,21 @@ Notation "[ 'rel' x y : T | E ]" := (SimplRel (fun x y : T => E%B)) Notation "[ 'predType' 'of' T ]" := (@clone_pred _ T _ id _ _ id) (at level 0, format "[ 'predType' 'of' T ]") : form_scope. -(* This redundant coercion lets us "inherit" the simpl_predType canonical *) -(* instance by declaring a coercion to simpl_pred. This hack is the only way *) -(* to put a predType structure on a predArgType. We use simpl_pred rather *) -(* than pred to ensure that /= removes the identity coercion. Note that the *) -(* coercion will never be used directly for simpl_pred, since the canonical *) -(* instance should always be resolved. *) +(** + This redundant coercion lets us "inherit" the simpl_predType canonical + instance by declaring a coercion to simpl_pred. This hack is the only way + to put a predType structure on a predArgType. We use simpl_pred rather + than pred to ensure that /= removes the identity coercion. Note that the + coercion will never be used directly for simpl_pred, since the canonical + instance should always be resolved. **) Notation pred_class := (pred_sort (predPredType _)). Coercion sort_of_simpl_pred T (p : simpl_pred T) : pred_class := p : pred T. -(* This lets us use some types as a synonym for their universal predicate. *) -(* Unfortunately, this won't work for existing types like bool, unless we *) -(* redefine bool, true, false and all bool ops. *) +(** + This lets us use some types as a synonym for their universal predicate. + Unfortunately, this won't work for existing types like bool, unless we + redefine bool, true, false and all bool ops. **) Definition predArgType := Type. Bind Scope type_scope with predArgType. Identity Coercion sort_of_predArgType : predArgType >-> Sortclass. @@ -1187,8 +1200,9 @@ Coercion pred_of_argType (T : predArgType) : simpl_pred T := predT. Notation "{ : T }" := (T%type : predArgType) (at level 0, format "{ : T }") : type_scope. -(* These must be defined outside a Section because "cooking" kills the *) -(* nosimpl tag. *) +(** + These must be defined outside a Section because "cooking" kills the + nosimpl tag. **) Definition mem T (pT : predType T) : pT -> mem_pred T := nosimpl (let: @PredType _ _ _ (exist _ mem _) := pT return pT -> _ in mem). @@ -1254,12 +1268,13 @@ Section simpl_mem. Variables (T : Type) (pT : predType T). Implicit Types (x : T) (p : pred T) (sp : simpl_pred T) (pp : pT). -(* Bespoke structures that provide fine-grained control over matching the *) -(* various forms of the \in predicate; note in particular the different forms *) -(* of hoisting that are used. We had to work around several bugs in the *) -(* implementation of unification, notably improper expansion of telescope *) -(* projections and overwriting of a variable assignment by a later *) -(* unification (probably due to conversion cache cross-talk). *) +(** + Bespoke structures that provide fine-grained control over matching the + various forms of the \in predicate; note in particular the different forms + of hoisting that are used. We had to work around several bugs in the + implementation of unification, notably improper expansion of telescope + projections and overwriting of a variable assignment by a later + unification (probably due to conversion cache cross-talk). **) Structure manifest_applicative_pred p := ManifestApplicativePred { manifest_applicative_pred_value :> pred T; _ : manifest_applicative_pred_value = p @@ -1305,10 +1320,11 @@ Lemma in_simpl x p (msp : manifest_simpl_pred p) : in_mem x (Mem [eta fun_of_simpl (msp : simpl_pred T)]) = p x. Proof. by case: msp => _ /= ->. Qed. -(* Because of the explicit eta expansion in the left-hand side, this lemma *) -(* should only be used in a right-to-left direction. The 8.3 hack allowing *) -(* partial right-to-left use does not work with the improved expansion *) -(* heuristics in 8.4. *) +(** + Because of the explicit eta expansion in the left-hand side, this lemma + should only be used in a right-to-left direction. The 8.3 hack allowing + partial right-to-left use does not work with the improved expansion + heuristics in 8.4. **) Lemma unfold_in x p : (x \in ([eta p] : pred T)) = p x. Proof. by []. Qed. @@ -1327,7 +1343,7 @@ Proof. by rewrite -mem_topred. Qed. End simpl_mem. -(* Qualifiers and keyed predicates. *) +(** Qualifiers and keyed predicates. **) Variant qualifier (q : nat) T := Qualifier of predPredType T. @@ -1371,7 +1387,7 @@ Notation "[ 'qualify' 'an' x | P ]" := (Qualifier 2 (fun x => P%B)) Notation "[ 'qualify' 'an' x : T | P ]" := (Qualifier 2 (fun x : T => P%B)) (at level 0, x at level 99, only parsing) : form_scope. -(* Keyed predicates: support for property-bearing predicate interfaces. *) +(** Keyed predicates: support for property-bearing predicate interfaces. **) Section KeyPred. @@ -1388,13 +1404,14 @@ Definition KeyedPred := @PackKeyedPred k p (frefl _). Variable k_p : keyed_pred k. Lemma keyed_predE : k_p =i p. Proof. by case: k_p. Qed. -(* Instances that strip the mem cast; the first one has "pred_of_mem" as its *) -(* projection head value, while the second has "pred_of_simpl". The latter *) -(* has the side benefit of preempting accidental misdeclarations. *) -(* Note: pred_of_mem is the registered mem >-> pred_class coercion, while *) -(* simpl_of_mem; pred_of_simpl is the mem >-> pred >=> Funclass coercion. We *) -(* must write down the coercions explicitly as the Canonical head constant *) -(* computation does not strip casts !! *) +(** + Instances that strip the mem cast; the first one has "pred_of_mem" as its + projection head value, while the second has "pred_of_simpl". The latter + has the side benefit of preempting accidental misdeclarations. + Note: pred_of_mem is the registered mem >-> pred_class coercion, while + simpl_of_mem; pred_of_simpl is the mem >-> pred >=> Funclass coercion. We + must write down the coercions explicitly as the Canonical head constant + computation does not strip casts !! **) Canonical keyed_mem := @PackKeyedPred k (pred_of_mem (mem k_p)) keyed_predE. Canonical keyed_mem_simpl := @@ -1434,7 +1451,7 @@ Canonical default_keyed_qualifier T n (q : qualifier n T) := End DefaultKeying. -(* Skolemizing with conditions. *) +(** Skolemizing with conditions. **) Lemma all_tag_cond_dep I T (C : pred I) U : (forall x, T x) -> (forall x, C x -> {y : T x & U x y}) -> @@ -1461,8 +1478,9 @@ Proof. by move=> y0; apply: all_sig_cond_dep. Qed. Section RelationProperties. -(* Caveat: reflexive should not be used to state lemmas, as auto and trivial *) -(* will not expand the constant. *) +(** + Caveat: reflexive should not be used to state lemmas, as auto and trivial + will not expand the constant. **) Variable T : Type. @@ -1496,8 +1514,9 @@ Proof. by move=> x y /sym_left_transitive Rxy z; rewrite !(symR z) Rxy. Qed. End PER. -(* We define the equivalence property with prenex quantification so that it *) -(* can be localized using the {in ..., ..} form defined below. *) +(** + We define the equivalence property with prenex quantification so that it + can be localized using the {in ..., ..} form defined below. **) Definition equivalence_rel := forall x y z, R z z * (R x y -> R x z = R y z). @@ -1512,7 +1531,7 @@ End RelationProperties. Lemma rev_trans T (R : rel T) : transitive R -> transitive (fun x y => R y x). Proof. by move=> trR x y z Ryx Rzy; apply: trR Rzy Ryx. Qed. -(* Property localization *) +(** Property localization **) Local Notation "{ 'all1' P }" := (forall x, P x : Prop) (at level 0). Local Notation "{ 'all2' P }" := (forall x y, P x y : Prop) (at level 0). @@ -1626,11 +1645,12 @@ Notation "{ 'on' cd , 'bijective' f }" := (bijective_on (mem cd) f) (at level 0, f at level 8, format "{ 'on' cd , 'bijective' f }") : type_scope. -(* Weakening and monotonicity lemmas for localized predicates. *) -(* Note that using these lemmas in backward reasoning will force expansion of *) -(* the predicate definition, as Coq needs to expose the quantifier to apply *) -(* these lemmas. We define a few specialized variants to avoid this for some *) -(* of the ssrfun predicates. *) +(** + Weakening and monotonicity lemmas for localized predicates. + Note that using these lemmas in backward reasoning will force expansion of + the predicate definition, as Coq needs to expose the quantifier to apply + these lemmas. We define a few specialized variants to avoid this for some + of the ssrfun predicates. **) Section LocalGlobal. diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index e43cab094b..01af67912a 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -10,50 +10,53 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **) + Require Import Bool. (* For bool_scope delimiter 'bool'. *) Require Import ssrmatching. Declare ML Module "ssreflect_plugin". -(******************************************************************************) -(* This file is the Gallina part of the ssreflect plugin implementation. *) -(* Files that use the ssreflect plugin should always Require ssreflect and *) -(* either Import ssreflect or Import ssreflect.SsrSyntax. *) -(* Part of the contents of this file is technical and will only interest *) -(* advanced developers; in addition the following are defined: *) -(* [the str of v by f] == the Canonical s : str such that f s = v. *) -(* [the str of v] == the Canonical s : str that coerces to v. *) -(* argumentType c == the T such that c : forall x : T, P x. *) -(* returnType c == the R such that c : T -> R. *) -(* {type of c for s} == P s where c : forall x : T, P x. *) -(* phantom T v == singleton type with inhabitant Phantom T v. *) -(* phant T == singleton type with inhabitant Phant v. *) -(* =^~ r == the converse of rewriting rule r (e.g., in a *) -(* rewrite multirule). *) -(* unkeyed t == t, but treated as an unkeyed matching pattern by *) -(* the ssreflect matching algorithm. *) -(* nosimpl t == t, but on the right-hand side of Definition C := *) -(* nosimpl disables expansion of C by /=. *) -(* locked t == t, but locked t is not convertible to t. *) -(* locked_with k t == t, but not convertible to t or locked_with k' t *) -(* unless k = k' (with k : unit). Coq type-checking *) -(* will be much more efficient if locked_with with a *) -(* bespoke k is used for sealed definitions. *) -(* unlockable v == interface for sealed constant definitions of v. *) -(* Unlockable def == the unlockable that registers def : C = v. *) -(* [unlockable of C] == a clone for C of the canonical unlockable for the *) -(* definition of C (e.g., if it uses locked_with). *) -(* [unlockable fun C] == [unlockable of C] with the expansion forced to be *) -(* an explicit lambda expression. *) -(* -> The usage pattern for ADT operations is: *) -(* Definition foo_def x1 .. xn := big_foo_expression. *) -(* Fact foo_key : unit. Proof. by []. Qed. *) -(* Definition foo := locked_with foo_key foo_def. *) -(* Canonical foo_unlockable := [unlockable fun foo]. *) -(* This minimizes the comparison overhead for foo, while still allowing *) -(* rewrite unlock to expose big_foo_expression. *) -(* More information about these definitions and their use can be found in the *) -(* ssreflect manual, and in specific comments below. *) -(******************************************************************************) + +(** + This file is the Gallina part of the ssreflect plugin implementation. + Files that use the ssreflect plugin should always Require ssreflect and + either Import ssreflect or Import ssreflect.SsrSyntax. + Part of the contents of this file is technical and will only interest + advanced developers; in addition the following are defined: + #[#the str of v by f#]# == the Canonical s : str such that f s = v. + #[#the str of v#]# == the Canonical s : str that coerces to v. + argumentType c == the T such that c : forall x : T, P x. + returnType c == the R such that c : T -> R. + {type of c for s} == P s where c : forall x : T, P x. + phantom T v == singleton type with inhabitant Phantom T v. + phant T == singleton type with inhabitant Phant v. + =^~ r == the converse of rewriting rule r (e.g., in a + rewrite multirule). + unkeyed t == t, but treated as an unkeyed matching pattern by + the ssreflect matching algorithm. + nosimpl t == t, but on the right-hand side of Definition C := + nosimpl disables expansion of C by /=. + locked t == t, but locked t is not convertible to t. + locked_with k t == t, but not convertible to t or locked_with k' t + unless k = k' (with k : unit). Coq type-checking + will be much more efficient if locked_with with a + bespoke k is used for sealed definitions. + unlockable v == interface for sealed constant definitions of v. + Unlockable def == the unlockable that registers def : C = v. + #[#unlockable of C#]# == a clone for C of the canonical unlockable for the + definition of C (e.g., if it uses locked_with). + #[#unlockable fun C#]# == #[#unlockable of C#]# with the expansion forced to be + an explicit lambda expression. + -> The usage pattern for ADT operations is: + Definition foo_def x1 .. xn := big_foo_expression. + Fact foo_key : unit. Proof. by #[# #]#. Qed. + Definition foo := locked_with foo_key foo_def. + Canonical foo_unlockable := #[#unlockable fun foo#]#. + This minimizes the comparison overhead for foo, while still allowing + rewrite unlock to expose big_foo_expression. + More information about these definitions and their use can be found in the + ssreflect manual, and in specific comments below. **) + Set Implicit Arguments. @@ -62,15 +65,16 @@ Unset Printing Implicit Defensive. Module SsrSyntax. -(* Declare Ssr keywords: 'is' 'of' '//' '/=' and '//='. We also declare the *) -(* parsing level 8, as a workaround for a notation grammar factoring problem. *) -(* Arguments of application-style notations (at level 10) should be declared *) -(* at level 8 rather than 9 or the camlp5 grammar will not factor properly. *) +(** + Declare Ssr keywords: 'is' 'of' '//' '/=' and '//='. We also declare the + parsing level 8, as a workaround for a notation grammar factoring problem. + Arguments of application-style notations (at level 10) should be declared + at level 8 rather than 9 or the camlp5 grammar will not factor properly. **) Reserved Notation "(* x 'is' y 'of' z 'isn't' // /= //= *)" (at level 8). Reserved Notation "(* 69 *)" (at level 69). -(* Non ambiguous keyword to check if the SsrSyntax module is imported *) +(** Non ambiguous keyword to check if the SsrSyntax module is imported **) Reserved Notation "(* Use to test if 'SsrSyntax_is_Imported' *)" (at level 8). Reserved Notation "<hidden n >" (at level 200). @@ -81,10 +85,11 @@ End SsrSyntax. Export SsrMatchingSyntax. Export SsrSyntax. -(* Make the general "if" into a notation, so that we can override it below. *) -(* The notations are "only parsing" because the Coq decompiler will not *) -(* recognize the expansion of the boolean if; using the default printer *) -(* avoids a spurrious trailing %GEN_IF. *) +(** + Make the general "if" into a notation, so that we can override it below. + The notations are "only parsing" because the Coq decompiler will not + recognize the expansion of the boolean if; using the default printer + avoids a spurrious trailing %%GEN_IF. **) Declare Scope general_if_scope. Delimit Scope general_if_scope with GEN_IF. @@ -102,7 +107,7 @@ Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" := (at level 200, c, t, v1, v2 at level 200, x ident, only parsing) : general_if_scope. -(* Force boolean interpretation of simple if expressions. *) +(** Force boolean interpretation of simple if expressions. **) Declare Scope boolean_if_scope. Delimit Scope boolean_if_scope with BOOL_IF. @@ -118,38 +123,41 @@ Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" := Open Scope boolean_if_scope. -(* To allow a wider variety of notations without reserving a large number of *) -(* of identifiers, the ssreflect library systematically uses "forms" to *) -(* enclose complex mixfix syntax. A "form" is simply a mixfix expression *) -(* enclosed in square brackets and introduced by a keyword: *) -(* [keyword ... ] *) -(* Because the keyword follows a bracket it does not need to be reserved. *) -(* Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq *) -(* Lists library) should be loaded before ssreflect so that their notations *) -(* do not mask all ssreflect forms. *) +(** + To allow a wider variety of notations without reserving a large number of + of identifiers, the ssreflect library systematically uses "forms" to + enclose complex mixfix syntax. A "form" is simply a mixfix expression + enclosed in square brackets and introduced by a keyword: + #[#keyword ... #]# + Because the keyword follows a bracket it does not need to be reserved. + Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq + Lists library) should be loaded before ssreflect so that their notations + do not mask all ssreflect forms. **) Declare Scope form_scope. Delimit Scope form_scope with FORM. Open Scope form_scope. -(* Allow overloading of the cast (x : T) syntax, put whitespace around the *) -(* ":" symbol to avoid lexical clashes (and for consistency with the parsing *) -(* precedence of the notation, which binds less tightly than application), *) -(* and put printing boxes that print the type of a long definition on a *) -(* separate line rather than force-fit it at the right margin. *) +(** + Allow overloading of the cast (x : T) syntax, put whitespace around the + ":" symbol to avoid lexical clashes (and for consistency with the parsing + precedence of the notation, which binds less tightly than application), + and put printing boxes that print the type of a long definition on a + separate line rather than force-fit it at the right margin. **) Notation "x : T" := (x : T) (at level 100, right associativity, format "'[hv' x '/ ' : T ']'") : core_scope. -(* Allow the casual use of notations like nat * nat for explicit Type *) -(* declarations. Note that (nat * nat : Type) is NOT equivalent to *) -(* (nat * nat)%type, whose inferred type is legacy type "Set". *) +(** + Allow the casual use of notations like nat * nat for explicit Type + declarations. Note that (nat * nat : Type) is NOT equivalent to + (nat * nat)%%type, whose inferred type is legacy type "Set". **) Notation "T : 'Type'" := (T%type : Type) (at level 100, only parsing) : core_scope. -(* Allow similarly Prop annotation for, e.g., rewrite multirules. *) +(** Allow similarly Prop annotation for, e.g., rewrite multirules. **) Notation "P : 'Prop'" := (P%type : Prop) (at level 100, only parsing) : core_scope. -(* Constants for abstract: and [: name ] intro pattern *) +(** Constants for abstract: and #[#: name #]# intro pattern **) Definition abstract_lock := unit. Definition abstract_key := tt. @@ -163,31 +171,32 @@ Register abstract_lock as plugins.ssreflect.abstract_lock. Register abstract_key as plugins.ssreflect.abstract_key. Register abstract as plugins.ssreflect.abstract. -(* Constants for tactic-views *) +(** Constants for tactic-views **) Inductive external_view : Type := tactic_view of Type. -(* Syntax for referring to canonical structures: *) -(* [the struct_type of proj_val by proj_fun] *) -(* This form denotes the Canonical instance s of the Structure type *) -(* struct_type whose proj_fun projection is proj_val, i.e., such that *) -(* proj_fun s = proj_val. *) -(* Typically proj_fun will be A record field accessors of struct_type, but *) -(* this need not be the case; it can be, for instance, a field of a record *) -(* type to which struct_type coerces; proj_val will likewise be coerced to *) -(* the return type of proj_fun. In all but the simplest cases, proj_fun *) -(* should be eta-expanded to allow for the insertion of implicit arguments. *) -(* In the common case where proj_fun itself is a coercion, the "by" part *) -(* can be omitted entirely; in this case it is inferred by casting s to the *) -(* inferred type of proj_val. Obviously the latter can be fixed by using an *) -(* explicit cast on proj_val, and it is highly recommended to do so when the *) -(* return type intended for proj_fun is "Type", as the type inferred for *) -(* proj_val may vary because of sort polymorphism (it could be Set or Prop). *) -(* Note when using the [the _ of _] form to generate a substructure from a *) -(* telescopes-style canonical hierarchy (implementing inheritance with *) -(* coercions), one should always project or coerce the value to the BASE *) -(* structure, because Coq will only find a Canonical derived structure for *) -(* the Canonical base structure -- not for a base structure that is specific *) -(* to proj_value. *) +(** + Syntax for referring to canonical structures: + #[#the struct_type of proj_val by proj_fun#]# + This form denotes the Canonical instance s of the Structure type + struct_type whose proj_fun projection is proj_val, i.e., such that + proj_fun s = proj_val. + Typically proj_fun will be A record field accessors of struct_type, but + this need not be the case; it can be, for instance, a field of a record + type to which struct_type coerces; proj_val will likewise be coerced to + the return type of proj_fun. In all but the simplest cases, proj_fun + should be eta-expanded to allow for the insertion of implicit arguments. + In the common case where proj_fun itself is a coercion, the "by" part + can be omitted entirely; in this case it is inferred by casting s to the + inferred type of proj_val. Obviously the latter can be fixed by using an + explicit cast on proj_val, and it is highly recommended to do so when the + return type intended for proj_fun is "Type", as the type inferred for + proj_val may vary because of sort polymorphism (it could be Set or Prop). + Note when using the #[#the _ of _ #]# form to generate a substructure from a + telescopes-style canonical hierarchy (implementing inheritance with + coercions), one should always project or coerce the value to the BASE + structure, because Coq will only find a Canonical derived structure for + the Canonical base structure -- not for a base structure that is specific + to proj_value. **) Module TheCanonical. @@ -210,11 +219,12 @@ Notation "[ 'the' sT 'of' v 'by' f ]" := Notation "[ 'the' sT 'of' v ]" := (get ((fun s : sT => Put v (*coerce*)s s) _)) (at level 0, only parsing) : form_scope. -(* The following are "format only" versions of the above notations. Since Coq *) -(* doesn't provide this facility, we fake it by splitting the "the" keyword. *) -(* We need to do this to prevent the formatter from being be thrown off by *) -(* application collapsing, coercion insertion and beta reduction in the right *) -(* hand side of the notations above. *) +(** + The following are "format only" versions of the above notations. Since Coq + doesn't provide this facility, we fake it by splitting the "the" keyword. + We need to do this to prevent the formatter from being be thrown off by + application collapsing, coercion insertion and beta reduction in the right + hand side of the notations above. **) Notation "[ 'th' 'e' sT 'of' v 'by' f ]" := (@get_by _ sT f v _ _) (at level 0, format "[ 'th' 'e' sT 'of' v 'by' f ]") : form_scope. @@ -222,37 +232,39 @@ Notation "[ 'th' 'e' sT 'of' v 'by' f ]" := (@get_by _ sT f v _ _) Notation "[ 'th' 'e' sT 'of' v ]" := (@get _ sT v _ _) (at level 0, format "[ 'th' 'e' sT 'of' v ]") : form_scope. -(* We would like to recognize -Notation "[ 'th' 'e' sT 'of' v : 'Type' ]" := (@get Type sT v _ _) - (at level 0, format "[ 'th' 'e' sT 'of' v : 'Type' ]") : form_scope. -*) - -(* Helper notation for canonical structure inheritance support. *) -(* This is a workaround for the poor interaction between delta reduction and *) -(* canonical projections in Coq's unification algorithm, by which transparent *) -(* definitions hide canonical instances, i.e., in *) -(* Canonical a_type_struct := @Struct a_type ... *) -(* Definition my_type := a_type. *) -(* my_type doesn't effectively inherit the struct structure from a_type. Our *) -(* solution is to redeclare the instance as follows *) -(* Canonical my_type_struct := Eval hnf in [struct of my_type]. *) -(* The special notation [str of _] must be defined for each Strucure "str" *) -(* with constructor "Str", typically as follows *) -(* Definition clone_str s := *) -(* let: Str _ x y ... z := s return {type of Str for s} -> str in *) -(* fun k => k _ x y ... z. *) -(* Notation "[ 'str' 'of' T 'for' s ]" := (@clone_str s (@Str T)) *) -(* (at level 0, format "[ 'str' 'of' T 'for' s ]") : form_scope. *) -(* Notation "[ 'str' 'of' T ]" := (repack_str (fun x => @Str T x)) *) -(* (at level 0, format "[ 'str' 'of' T ]") : form_scope. *) -(* The notation for the match return predicate is defined below; the eta *) -(* expansion in the second form serves both to distinguish it from the first *) -(* and to avoid the delta reduction problem. *) -(* There are several variations on the notation and the definition of the *) -(* the "clone" function, for telescopes, mixin classes, and join (multiple *) -(* inheritance) classes. We describe a different idiom for clones in ssrfun; *) -(* it uses phantom types (see below) and static unification; see fintype and *) -(* ssralg for examples. *) +(** + We would like to recognize +Notation " #[# 'th' 'e' sT 'of' v : 'Type' #]#" := (@get Type sT v _ _) + (at level 0, format " #[# 'th' 'e' sT 'of' v : 'Type' #]#") : form_scope. + **) + +(** + Helper notation for canonical structure inheritance support. + This is a workaround for the poor interaction between delta reduction and + canonical projections in Coq's unification algorithm, by which transparent + definitions hide canonical instances, i.e., in + Canonical a_type_struct := @Struct a_type ... + Definition my_type := a_type. + my_type doesn't effectively inherit the struct structure from a_type. Our + solution is to redeclare the instance as follows + Canonical my_type_struct := Eval hnf in #[#struct of my_type#]#. + The special notation #[#str of _ #]# must be defined for each Strucure "str" + with constructor "Str", typically as follows + Definition clone_str s := + let: Str _ x y ... z := s return {type of Str for s} -> str in + fun k => k _ x y ... z. + Notation " #[# 'str' 'of' T 'for' s #]#" := (@clone_str s (@Str T)) + (at level 0, format " #[# 'str' 'of' T 'for' s #]#") : form_scope. + Notation " #[# 'str' 'of' T #]#" := (repack_str (fun x => @Str T x)) + (at level 0, format " #[# 'str' 'of' T #]#") : form_scope. + The notation for the match return predicate is defined below; the eta + expansion in the second form serves both to distinguish it from the first + and to avoid the delta reduction problem. + There are several variations on the notation and the definition of the + the "clone" function, for telescopes, mixin classes, and join (multiple + inheritance) classes. We describe a different idiom for clones in ssrfun; + it uses phantom types (see below) and static unification; see fintype and + ssralg for examples. **) Definition argumentType T P & forall x : T, P x := T. Definition dependentReturnType T P & forall x : T, P x := P. @@ -261,81 +273,84 @@ Definition returnType aT rT & aT -> rT := rT. Notation "{ 'type' 'of' c 'for' s }" := (dependentReturnType c s) (at level 0, format "{ 'type' 'of' c 'for' s }") : type_scope. -(* A generic "phantom" type (actually, a unit type with a phantom parameter). *) -(* This type can be used for type definitions that require some Structure *) -(* on one of their parameters, to allow Coq to infer said structure so it *) -(* does not have to be supplied explicitly or via the "[the _ of _]" notation *) -(* (the latter interacts poorly with other Notation). *) -(* The definition of a (co)inductive type with a parameter p : p_type, that *) -(* needs to use the operations of a structure *) -(* Structure p_str : Type := p_Str {p_repr :> p_type; p_op : p_repr -> ...} *) -(* should be given as *) -(* Inductive indt_type (p : p_str) := Indt ... . *) -(* Definition indt_of (p : p_str) & phantom p_type p := indt_type p. *) -(* Notation "{ 'indt' p }" := (indt_of (Phantom p)). *) -(* Definition indt p x y ... z : {indt p} := @Indt p x y ... z. *) -(* Notation "[ 'indt' x y ... z ]" := (indt x y ... z). *) -(* That is, the concrete type and its constructor should be shadowed by *) -(* definitions that use a phantom argument to infer and display the true *) -(* value of p (in practice, the "indt" constructor often performs additional *) -(* functions, like "locking" the representation -- see below). *) -(* We also define a simpler version ("phant" / "Phant") of phantom for the *) -(* common case where p_type is Type. *) +(** + A generic "phantom" type (actually, a unit type with a phantom parameter). + This type can be used for type definitions that require some Structure + on one of their parameters, to allow Coq to infer said structure so it + does not have to be supplied explicitly or via the " #[#the _ of _ #]#" notation + (the latter interacts poorly with other Notation). + The definition of a (co)inductive type with a parameter p : p_type, that + needs to use the operations of a structure + Structure p_str : Type := p_Str {p_repr :> p_type; p_op : p_repr -> ...} + should be given as + Inductive indt_type (p : p_str) := Indt ... . + Definition indt_of (p : p_str) & phantom p_type p := indt_type p. + Notation "{ 'indt' p }" := (indt_of (Phantom p)). + Definition indt p x y ... z : {indt p} := @Indt p x y ... z. + Notation " #[# 'indt' x y ... z #]#" := (indt x y ... z). + That is, the concrete type and its constructor should be shadowed by + definitions that use a phantom argument to infer and display the true + value of p (in practice, the "indt" constructor often performs additional + functions, like "locking" the representation -- see below). + We also define a simpler version ("phant" / "Phant") of phantom for the + common case where p_type is Type. **) Variant phantom T (p : T) := Phantom. Arguments phantom : clear implicits. Arguments Phantom : clear implicits. Variant phant (p : Type) := Phant. -(* Internal tagging used by the implementation of the ssreflect elim. *) +(** Internal tagging used by the implementation of the ssreflect elim. **) Definition protect_term (A : Type) (x : A) : A := x. Register protect_term as plugins.ssreflect.protect_term. -(* The ssreflect idiom for a non-keyed pattern: *) -(* - unkeyed t wiil match any subterm that unifies with t, regardless of *) -(* whether it displays the same head symbol as t. *) -(* - unkeyed t a b will match any application of a term f unifying with t, *) -(* to two arguments unifying with with a and b, repectively, regardless of *) -(* apparent head symbols. *) -(* - unkeyed x where x is a variable will match any subterm with the same *) -(* type as x (when x would raise the 'indeterminate pattern' error). *) +(** + The ssreflect idiom for a non-keyed pattern: + - unkeyed t wiil match any subterm that unifies with t, regardless of + whether it displays the same head symbol as t. + - unkeyed t a b will match any application of a term f unifying with t, + to two arguments unifying with with a and b, repectively, regardless of + apparent head symbols. + - unkeyed x where x is a variable will match any subterm with the same + type as x (when x would raise the 'indeterminate pattern' error). **) Notation unkeyed x := (let flex := x in flex). -(* Ssreflect converse rewrite rule rule idiom. *) +(** Ssreflect converse rewrite rule rule idiom. **) Definition ssr_converse R (r : R) := (Logic.I, r). Notation "=^~ r" := (ssr_converse r) (at level 100) : form_scope. -(* Term tagging (user-level). *) -(* The ssreflect library uses four strengths of term tagging to restrict *) -(* convertibility during type checking: *) -(* nosimpl t simplifies to t EXCEPT in a definition; more precisely, given *) -(* Definition foo := nosimpl bar, foo (or foo t') will NOT be expanded by *) -(* the /= and //= switches unless it is in a forcing context (e.g., in *) -(* match foo t' with ... end, foo t' will be reduced if this allows the *) -(* match to be reduced). Note that nosimpl bar is simply notation for a *) -(* a term that beta-iota reduces to bar; hence rewrite /foo will replace *) -(* foo by bar, and rewrite -/foo will replace bar by foo. *) -(* CAVEAT: nosimpl should not be used inside a Section, because the end of *) -(* section "cooking" removes the iota redex. *) -(* locked t is provably equal to t, but is not convertible to t; 'locked' *) -(* provides support for selective rewriting, via the lock t : t = locked t *) -(* Lemma, and the ssreflect unlock tactic. *) -(* locked_with k t is equal but not convertible to t, much like locked t, *) -(* but supports explicit tagging with a value k : unit. This is used to *) -(* mitigate a flaw in the term comparison heuristic of the Coq kernel, *) -(* which treats all terms of the form locked t as equal and conpares their *) -(* arguments recursively, leading to an exponential blowup of comparison. *) -(* For this reason locked_with should be used rather than locked when *) -(* defining ADT operations. The unlock tactic does not support locked_with *) -(* but the unlock rewrite rule does, via the unlockable interface. *) -(* we also use Module Type ascription to create truly opaque constants, *) -(* because simple expansion of constants to reveal an unreducible term *) -(* doubles the time complexity of a negative comparison. Such opaque *) -(* constants can be expanded generically with the unlock rewrite rule. *) -(* See the definition of card and subset in fintype for examples of this. *) +(** + Term tagging (user-level). + The ssreflect library uses four strengths of term tagging to restrict + convertibility during type checking: + nosimpl t simplifies to t EXCEPT in a definition; more precisely, given + Definition foo := nosimpl bar, foo (or foo t') will NOT be expanded by + the /= and //= switches unless it is in a forcing context (e.g., in + match foo t' with ... end, foo t' will be reduced if this allows the + match to be reduced). Note that nosimpl bar is simply notation for a + a term that beta-iota reduces to bar; hence rewrite /foo will replace + foo by bar, and rewrite -/foo will replace bar by foo. + CAVEAT: nosimpl should not be used inside a Section, because the end of + section "cooking" removes the iota redex. + locked t is provably equal to t, but is not convertible to t; 'locked' + provides support for selective rewriting, via the lock t : t = locked t + Lemma, and the ssreflect unlock tactic. + locked_with k t is equal but not convertible to t, much like locked t, + but supports explicit tagging with a value k : unit. This is used to + mitigate a flaw in the term comparison heuristic of the Coq kernel, + which treats all terms of the form locked t as equal and conpares their + arguments recursively, leading to an exponential blowup of comparison. + For this reason locked_with should be used rather than locked when + defining ADT operations. The unlock tactic does not support locked_with + but the unlock rewrite rule does, via the unlockable interface. + we also use Module Type ascription to create truly opaque constants, + because simple expansion of constants to reveal an unreducible term + doubles the time complexity of a negative comparison. Such opaque + constants can be expanded generically with the unlock rewrite rule. + See the definition of card and subset in fintype for examples of this. **) Notation nosimpl t := (let: tt := tt in t). @@ -347,11 +362,11 @@ Register locked as plugins.ssreflect.locked. Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed. -(* Needed for locked predicates, in particular for eqType's. *) +(** Needed for locked predicates, in particular for eqType's. **) Lemma not_locked_false_eq_true : locked false <> true. Proof. unlock; discriminate. Qed. -(* The basic closing tactic "done". *) +(** The basic closing tactic "done". **) Ltac done := trivial; hnf; intros; solve [ do ![solve [trivial | apply: sym_equal; trivial] @@ -359,7 +374,7 @@ Ltac done := | case not_locked_false_eq_true; assumption | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. -(* Quicker done tactic not including split, syntax: /0/ *) +(** Quicker done tactic not including split, syntax: /0/ **) Ltac ssrdone0 := trivial; hnf; intros; solve [ do ![solve [trivial | apply: sym_equal; trivial] @@ -367,7 +382,7 @@ Ltac ssrdone0 := | case not_locked_false_eq_true; assumption | match goal with H : ~ _ |- _ => solve [case H; trivial] end ]. -(* To unlock opaque constants. *) +(** To unlock opaque constants. **) Structure unlockable T v := Unlockable {unlocked : T; _ : unlocked = v}. Lemma unlock T x C : @unlocked T x C = x. Proof. by case: C. Qed. @@ -377,25 +392,26 @@ Notation "[ 'unlockable' 'of' C ]" := (@Unlockable _ _ C (unlock _)) Notation "[ 'unlockable' 'fun' C ]" := (@Unlockable _ (fun _ => _) C (unlock _)) (at level 0, format "[ 'unlockable' 'fun' C ]") : form_scope. -(* Generic keyed constant locking. *) +(** Generic keyed constant locking. **) -(* The argument order ensures that k is always compared before T. *) +(** The argument order ensures that k is always compared before T. **) Definition locked_with k := let: tt := k in fun T x => x : T. -(* This can be used as a cheap alternative to cloning the unlockable instance *) -(* below, but with caution as unkeyed matching can be expensive. *) +(** + This can be used as a cheap alternative to cloning the unlockable instance + below, but with caution as unkeyed matching can be expensive. **) Lemma locked_withE T k x : unkeyed (locked_with k x) = x :> T. Proof. by case: k. Qed. -(* Intensionaly, this instance will not apply to locked u. *) +(** Intensionaly, this instance will not apply to locked u. **) Canonical locked_with_unlockable T k x := @Unlockable T x (locked_with k x) (locked_withE k x). -(* More accurate variant of unlock, and safer alternative to locked_withE. *) +(** More accurate variant of unlock, and safer alternative to locked_withE. **) Lemma unlock_with T k x : unlocked (locked_with_unlockable k x) = x :> T. Proof. exact: unlock. Qed. -(* The internal lemmas for the have tactics. *) +(** The internal lemmas for the have tactics. **) Definition ssr_have Plemma Pgoal (step : Plemma) rest : Pgoal := rest step. Arguments ssr_have Plemma [Pgoal]. @@ -416,7 +432,7 @@ Arguments ssr_wlog Plemma [Pgoal]. Register ssr_suff as plugins.ssreflect.ssr_suff. Register ssr_wlog as plugins.ssreflect.ssr_wlog. -(* Internal N-ary congruence lemmas for the congr tactic. *) +(** Internal N-ary congruence lemmas for the congr tactic. **) Fixpoint nary_congruence_statement (n : nat) : (forall B, (B -> B -> Prop) -> Prop) -> Prop := @@ -443,7 +459,7 @@ Arguments ssr_congr_arrow : clear implicits. Register nary_congruence as plugins.ssreflect.nary_congruence. Register ssr_congr_arrow as plugins.ssreflect.ssr_congr_arrow. -(* View lemmas that don't use reflection. *) +(** View lemmas that don't use reflection. **) Section ApplyIff. @@ -461,14 +477,15 @@ End ApplyIff. Hint View for move/ iffLRn|2 iffRLn|2 iffLR|2 iffRL|2. Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2. -(* To focus non-ssreflect tactics on a subterm, eg vm_compute. *) -(* Usage: *) -(* elim/abstract_context: (pattern) => G defG. *) -(* vm_compute; rewrite {}defG {G}. *) -(* Note that vm_cast are not stored in the proof term *) -(* for reductions occuring in the context, hence *) -(* set here := pattern; vm_compute in (value of here) *) -(* blows up at Qed time. *) +(** + To focus non-ssreflect tactics on a subterm, eg vm_compute. + Usage: + elim/abstract_context: (pattern) => G defG. + vm_compute; rewrite {}defG {G}. + Note that vm_cast are not stored in the proof term + for reductions occuring in the context, hence + set here := pattern; vm_compute in (value of here) + blows up at Qed time. **) Lemma abstract_context T (P : T -> Type) x : (forall Q, Q = P -> Q x) -> P x. Proof. by move=> /(_ P); apply. Qed. diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index 99ff943e61..e2c0ed7c8b 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -10,207 +10,210 @@ (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **) + Require Import ssreflect. -(******************************************************************************) -(* This file contains the basic definitions and notations for working with *) -(* functions. The definitions provide for: *) -(* *) -(* - Pair projections: *) -(* p.1 == first element of a pair *) -(* p.2 == second element of a pair *) -(* These notations also apply to p : P /\ Q, via an and >-> pair coercion. *) -(* *) -(* - Simplifying functions, beta-reduced by /= and simpl: *) -(* [fun : T => E] == constant function from type T that returns E *) -(* [fun x => E] == unary function *) -(* [fun x : T => E] == unary function with explicit domain type *) -(* [fun x y => E] == binary function *) -(* [fun x y : T => E] == binary function with common domain type *) -(* [fun (x : T) y => E] \ *) -(* [fun (x : xT) (y : yT) => E] | == binary function with (some) explicit, *) -(* [fun x (y : T) => E] / independent domain types for each argument *) -(* *) -(* - Partial functions using option type: *) -(* oapp f d ox == if ox is Some x returns f x, d otherwise *) -(* odflt d ox == if ox is Some x returns x, d otherwise *) -(* obind f ox == if ox is Some x returns f x, None otherwise *) -(* omap f ox == if ox is Some x returns Some (f x), None otherwise *) -(* *) -(* - Singleton types: *) -(* all_equal_to x0 == x0 is the only value in its type, so any such value *) -(* can be rewritten to x0. *) -(* *) -(* - A generic wrapper type: *) -(* wrapped T == the inductive type with values Wrap x for x : T. *) -(* unwrap w == the projection of w : wrapped T on T. *) -(* wrap x == the canonical injection of x : T into wrapped T; it is *) -(* equivalent to Wrap x, but is declared as a (default) *) -(* Canonical Structure, which lets the Coq HO unification *) -(* automatically expand x into unwrap (wrap x). The delta *) -(* reduction of wrap x to Wrap can be exploited to *) -(* introduce controlled nondeterminism in Canonical *) -(* Structure inference, as in the implementation of *) -(* the mxdirect predicate in matrix.v. *) -(* *) -(* - Sigma types: *) -(* tag w == the i of w : {i : I & T i}. *) -(* tagged w == the T i component of w : {i : I & T i}. *) -(* Tagged T x == the {i : I & T i} with component x : T i. *) -(* tag2 w == the i of w : {i : I & T i & U i}. *) -(* tagged2 w == the T i component of w : {i : I & T i & U i}. *) -(* tagged2' w == the U i component of w : {i : I & T i & U i}. *) -(* Tagged2 T U x y == the {i : I & T i} with components x : T i and y : U i. *) -(* sval u == the x of u : {x : T | P x}. *) -(* s2val u == the x of u : {x : T | P x & Q x}. *) -(* The properties of sval u, s2val u are given by lemmas svalP, s2valP, and *) -(* s2valP'. We provide coercions sigT2 >-> sigT and sig2 >-> sig >-> sigT. *) -(* A suite of lemmas (all_sig, ...) let us skolemize sig, sig2, sigT, sigT2 *) -(* and pair, e.g., *) -(* have /all_sig[f fP] (x : T): {y : U | P y} by ... *) -(* yields an f : T -> U such that fP : forall x, P (f x). *) -(* - Identity functions: *) -(* id == NOTATION for the explicit identity function fun x => x. *) -(* @id T == notation for the explicit identity at type T. *) -(* idfun == an expression with a head constant, convertible to id; *) -(* idfun x simplifies to x. *) -(* @idfun T == the expression above, specialized to type T. *) -(* phant_id x y == the function type phantom _ x -> phantom _ y. *) -(* *** In addition to their casual use in functional programming, identity *) -(* functions are often used to trigger static unification as part of the *) -(* construction of dependent Records and Structures. For example, if we need *) -(* a structure sT over a type T, we take as arguments T, sT, and a "dummy" *) -(* function T -> sort sT: *) -(* Definition foo T sT & T -> sort sT := ... *) -(* We can avoid specifying sT directly by calling foo (@id T), or specify *) -(* the call completely while still ensuring the consistency of T and sT, by *) -(* calling @foo T sT idfun. The phant_id type allows us to extend this trick *) -(* to non-Type canonical projections. It also allows us to sidestep *) -(* dependent type constraints when building explicit records, e.g., given *) -(* Record r := R {x; y : T(x)}. *) -(* if we need to build an r from a given y0 while inferring some x0, such *) -(* that y0 : T(x0), we pose *) -(* Definition mk_r .. y .. (x := ...) y' & phant_id y y' := R x y'. *) -(* Calling @mk_r .. y0 .. id will cause Coq to use y' := y0, while checking *) -(* the dependent type constraint y0 : T(x0). *) -(* *) -(* - Extensional equality for functions and relations (i.e. functions of two *) -(* arguments): *) -(* f1 =1 f2 == f1 x is equal to f2 x for all x. *) -(* f1 =1 f2 :> A == ... and f2 is explicitly typed. *) -(* f1 =2 f2 == f1 x y is equal to f2 x y for all x y. *) -(* f1 =2 f2 :> A == ... and f2 is explicitly typed. *) -(* *) -(* - Composition for total and partial functions: *) -(* f^~ y == function f with second argument specialised to y, *) -(* i.e., fun x => f x y *) -(* CAVEAT: conditional (non-maximal) implicit arguments *) -(* of f are NOT inserted in this context *) -(* @^~ x == application at x, i.e., fun f => f x *) -(* [eta f] == the explicit eta-expansion of f, i.e., fun x => f x *) -(* CAVEAT: conditional (non-maximal) implicit arguments *) -(* of f are NOT inserted in this context. *) -(* fun=> v := the constant function fun _ => v. *) -(* f1 \o f2 == composition of f1 and f2. *) -(* Note: (f1 \o f2) x simplifies to f1 (f2 x). *) -(* f1 \; f2 == categorical composition of f1 and f2. This expands to *) -(* to f2 \o f1 and (f1 \; f2) x simplifies to f2 (f1 x). *) -(* pcomp f1 f2 == composition of partial functions f1 and f2. *) -(* *) -(* *) -(* - Properties of functions: *) -(* injective f <-> f is injective. *) -(* cancel f g <-> g is a left inverse of f / f is a right inverse of g. *) -(* pcancel f g <-> g is a left inverse of f where g is partial. *) -(* ocancel f g <-> g is a left inverse of f where f is partial. *) -(* bijective f <-> f is bijective (has a left and right inverse). *) -(* involutive f <-> f is involutive. *) -(* *) -(* - Properties for operations. *) -(* left_id e op <-> e is a left identity for op (e op x = x). *) -(* right_id e op <-> e is a right identity for op (x op e = x). *) -(* left_inverse e inv op <-> inv is a left inverse for op wrt identity e, *) -(* i.e., (inv x) op x = e. *) -(* right_inverse e inv op <-> inv is a right inverse for op wrt identity e *) -(* i.e., x op (i x) = e. *) -(* self_inverse e op <-> each x is its own op-inverse (x op x = e). *) -(* idempotent op <-> op is idempotent for op (x op x = x). *) -(* associative op <-> op is associative, i.e., *) -(* x op (y op z) = (x op y) op z. *) -(* commutative op <-> op is commutative (x op y = y op x). *) -(* left_commutative op <-> op is left commutative, i.e., *) -(* x op (y op z) = y op (x op z). *) -(* right_commutative op <-> op is right commutative, i.e., *) -(* (x op y) op z = (x op z) op y. *) -(* left_zero z op <-> z is a left zero for op (z op x = z). *) -(* right_zero z op <-> z is a right zero for op (x op z = z). *) -(* left_distributive op1 op2 <-> op1 distributes over op2 to the left: *) -(* (x op2 y) op1 z = (x op1 z) op2 (y op1 z). *) -(* right_distributive op1 op2 <-> op distributes over add to the right: *) -(* x op1 (y op2 z) = (x op1 z) op2 (x op1 z). *) -(* interchange op1 op2 <-> op1 and op2 satisfy an interchange law: *) -(* (x op2 y) op1 (z op2 t) = (x op1 z) op2 (y op1 t). *) -(* Note that interchange op op is a commutativity property. *) -(* left_injective op <-> op is injective in its left argument: *) -(* x op y = z op y -> x = z. *) -(* right_injective op <-> op is injective in its right argument: *) -(* x op y = x op z -> y = z. *) -(* left_loop inv op <-> op, inv obey the inverse loop left axiom: *) -(* (inv x) op (x op y) = y for all x, y, i.e., *) -(* op (inv x) is always a left inverse of op x *) -(* rev_left_loop inv op <-> op, inv obey the inverse loop reverse left *) -(* axiom: x op ((inv x) op y) = y, for all x, y. *) -(* right_loop inv op <-> op, inv obey the inverse loop right axiom: *) -(* (x op y) op (inv y) = x for all x, y. *) -(* rev_right_loop inv op <-> op, inv obey the inverse loop reverse right *) -(* axiom: (x op y) op (inv y) = x for all x, y. *) -(* Note that familiar "cancellation" identities like x + y - y = x or *) -(* x - y + y = x are respectively instances of right_loop and rev_right_loop *) -(* The corresponding lemmas will use the K and NK/VK suffixes, respectively. *) -(* *) -(* - Morphisms for functions and relations: *) -(* {morph f : x / a >-> r} <-> f is a morphism with respect to functions *) -(* (fun x => a) and (fun x => r); if r == R[x], *) -(* this states that f a = R[f x] for all x. *) -(* {morph f : x / a} <-> f is a morphism with respect to the *) -(* function expression (fun x => a). This is *) -(* shorthand for {morph f : x / a >-> a}; note *) -(* that the two instances of a are often *) -(* interpreted at different types. *) -(* {morph f : x y / a >-> r} <-> f is a morphism with respect to functions *) -(* (fun x y => a) and (fun x y => r). *) -(* {morph f : x y / a} <-> f is a morphism with respect to the *) -(* function expression (fun x y => a). *) -(* {homo f : x / a >-> r} <-> f is a homomorphism with respect to the *) -(* predicates (fun x => a) and (fun x => r); *) -(* if r == R[x], this states that a -> R[f x] *) -(* for all x. *) -(* {homo f : x / a} <-> f is a homomorphism with respect to the *) -(* predicate expression (fun x => a). *) -(* {homo f : x y / a >-> r} <-> f is a homomorphism with respect to the *) -(* relations (fun x y => a) and (fun x y => r). *) -(* {homo f : x y / a} <-> f is a homomorphism with respect to the *) -(* relation expression (fun x y => a). *) -(* {mono f : x / a >-> r} <-> f is monotone with respect to projectors *) -(* (fun x => a) and (fun x => r); if r == R[x], *) -(* this states that R[f x] = a for all x. *) -(* {mono f : x / a} <-> f is monotone with respect to the projector *) -(* expression (fun x => a). *) -(* {mono f : x y / a >-> r} <-> f is monotone with respect to relators *) -(* (fun x y => a) and (fun x y => r). *) -(* {mono f : x y / a} <-> f is monotone with respect to the relator *) -(* expression (fun x y => a). *) -(* *) -(* The file also contains some basic lemmas for the above concepts. *) -(* Lemmas relative to cancellation laws use some abbreviated suffixes: *) -(* K - a cancellation rule like esymK : cancel (@esym T x y) (@esym T y x). *) -(* LR - a lemma moving an operation from the left hand side of a relation to *) -(* the right hand side, like canLR: cancel g f -> x = g y -> f x = y. *) -(* RL - a lemma moving an operation from the right to the left, e.g., canRL. *) -(* Beware that the LR and RL orientations refer to an "apply" (back chaining) *) -(* usage; when using the same lemmas with "have" or "move" (forward chaining) *) -(* the directions will be reversed!. *) -(******************************************************************************) + +(** + This file contains the basic definitions and notations for working with + functions. The definitions provide for: + + - Pair projections: + p.1 == first element of a pair + p.2 == second element of a pair + These notations also apply to p : P /\ Q, via an and >-> pair coercion. + + - Simplifying functions, beta-reduced by /= and simpl: + #[#fun : T => E#]# == constant function from type T that returns E + #[#fun x => E#]# == unary function + #[#fun x : T => E#]# == unary function with explicit domain type + #[#fun x y => E#]# == binary function + #[#fun x y : T => E#]# == binary function with common domain type + #[#fun (x : T) y => E#]# \ + #[#fun (x : xT) (y : yT) => E#]# | == binary function with (some) explicit, + #[#fun x (y : T) => E#]# / independent domain types for each argument + + - Partial functions using option type: + oapp f d ox == if ox is Some x returns f x, d otherwise + odflt d ox == if ox is Some x returns x, d otherwise + obind f ox == if ox is Some x returns f x, None otherwise + omap f ox == if ox is Some x returns Some (f x), None otherwise + + - Singleton types: + all_equal_to x0 == x0 is the only value in its type, so any such value + can be rewritten to x0. + + - A generic wrapper type: + wrapped T == the inductive type with values Wrap x for x : T. + unwrap w == the projection of w : wrapped T on T. + wrap x == the canonical injection of x : T into wrapped T; it is + equivalent to Wrap x, but is declared as a (default) + Canonical Structure, which lets the Coq HO unification + automatically expand x into unwrap (wrap x). The delta + reduction of wrap x to Wrap can be exploited to + introduce controlled nondeterminism in Canonical + Structure inference, as in the implementation of + the mxdirect predicate in matrix.v. + + - Sigma types: + tag w == the i of w : {i : I & T i}. + tagged w == the T i component of w : {i : I & T i}. + Tagged T x == the {i : I & T i} with component x : T i. + tag2 w == the i of w : {i : I & T i & U i}. + tagged2 w == the T i component of w : {i : I & T i & U i}. + tagged2' w == the U i component of w : {i : I & T i & U i}. + Tagged2 T U x y == the {i : I & T i} with components x : T i and y : U i. + sval u == the x of u : {x : T | P x}. + s2val u == the x of u : {x : T | P x & Q x}. + The properties of sval u, s2val u are given by lemmas svalP, s2valP, and + s2valP'. We provide coercions sigT2 >-> sigT and sig2 >-> sig >-> sigT. + A suite of lemmas (all_sig, ...) let us skolemize sig, sig2, sigT, sigT2 + and pair, e.g., + have /all_sig#[#f fP#]# (x : T): {y : U | P y} by ... + yields an f : T -> U such that fP : forall x, P (f x). + - Identity functions: + id == NOTATION for the explicit identity function fun x => x. + @id T == notation for the explicit identity at type T. + idfun == an expression with a head constant, convertible to id; + idfun x simplifies to x. + @idfun T == the expression above, specialized to type T. + phant_id x y == the function type phantom _ x -> phantom _ y. + *** In addition to their casual use in functional programming, identity + functions are often used to trigger static unification as part of the + construction of dependent Records and Structures. For example, if we need + a structure sT over a type T, we take as arguments T, sT, and a "dummy" + function T -> sort sT: + Definition foo T sT & T -> sort sT := ... + We can avoid specifying sT directly by calling foo (@id T), or specify + the call completely while still ensuring the consistency of T and sT, by + calling @foo T sT idfun. The phant_id type allows us to extend this trick + to non-Type canonical projections. It also allows us to sidestep + dependent type constraints when building explicit records, e.g., given + Record r := R {x; y : T(x)}. + if we need to build an r from a given y0 while inferring some x0, such + that y0 : T(x0), we pose + Definition mk_r .. y .. (x := ...) y' & phant_id y y' := R x y'. + Calling @mk_r .. y0 .. id will cause Coq to use y' := y0, while checking + the dependent type constraint y0 : T(x0). + + - Extensional equality for functions and relations (i.e. functions of two + arguments): + f1 =1 f2 == f1 x is equal to f2 x for all x. + f1 =1 f2 :> A == ... and f2 is explicitly typed. + f1 =2 f2 == f1 x y is equal to f2 x y for all x y. + f1 =2 f2 :> A == ... and f2 is explicitly typed. + + - Composition for total and partial functions: + f^~ y == function f with second argument specialised to y, + i.e., fun x => f x y + CAVEAT: conditional (non-maximal) implicit arguments + of f are NOT inserted in this context + @^~ x == application at x, i.e., fun f => f x + #[#eta f#]# == the explicit eta-expansion of f, i.e., fun x => f x + CAVEAT: conditional (non-maximal) implicit arguments + of f are NOT inserted in this context. + fun=> v := the constant function fun _ => v. + f1 \o f2 == composition of f1 and f2. + Note: (f1 \o f2) x simplifies to f1 (f2 x). + f1 \; f2 == categorical composition of f1 and f2. This expands to + to f2 \o f1 and (f1 \; f2) x simplifies to f2 (f1 x). + pcomp f1 f2 == composition of partial functions f1 and f2. + + + - Properties of functions: + injective f <-> f is injective. + cancel f g <-> g is a left inverse of f / f is a right inverse of g. + pcancel f g <-> g is a left inverse of f where g is partial. + ocancel f g <-> g is a left inverse of f where f is partial. + bijective f <-> f is bijective (has a left and right inverse). + involutive f <-> f is involutive. + + - Properties for operations. + left_id e op <-> e is a left identity for op (e op x = x). + right_id e op <-> e is a right identity for op (x op e = x). + left_inverse e inv op <-> inv is a left inverse for op wrt identity e, + i.e., (inv x) op x = e. + right_inverse e inv op <-> inv is a right inverse for op wrt identity e + i.e., x op (i x) = e. + self_inverse e op <-> each x is its own op-inverse (x op x = e). + idempotent op <-> op is idempotent for op (x op x = x). + associative op <-> op is associative, i.e., + x op (y op z) = (x op y) op z. + commutative op <-> op is commutative (x op y = y op x). + left_commutative op <-> op is left commutative, i.e., + x op (y op z) = y op (x op z). + right_commutative op <-> op is right commutative, i.e., + (x op y) op z = (x op z) op y. + left_zero z op <-> z is a left zero for op (z op x = z). + right_zero z op <-> z is a right zero for op (x op z = z). + left_distributive op1 op2 <-> op1 distributes over op2 to the left: + (x op2 y) op1 z = (x op1 z) op2 (y op1 z). + right_distributive op1 op2 <-> op distributes over add to the right: + x op1 (y op2 z) = (x op1 z) op2 (x op1 z). + interchange op1 op2 <-> op1 and op2 satisfy an interchange law: + (x op2 y) op1 (z op2 t) = (x op1 z) op2 (y op1 t). + Note that interchange op op is a commutativity property. + left_injective op <-> op is injective in its left argument: + x op y = z op y -> x = z. + right_injective op <-> op is injective in its right argument: + x op y = x op z -> y = z. + left_loop inv op <-> op, inv obey the inverse loop left axiom: + (inv x) op (x op y) = y for all x, y, i.e., + op (inv x) is always a left inverse of op x + rev_left_loop inv op <-> op, inv obey the inverse loop reverse left + axiom: x op ((inv x) op y) = y, for all x, y. + right_loop inv op <-> op, inv obey the inverse loop right axiom: + (x op y) op (inv y) = x for all x, y. + rev_right_loop inv op <-> op, inv obey the inverse loop reverse right + axiom: (x op y) op (inv y) = x for all x, y. + Note that familiar "cancellation" identities like x + y - y = x or + x - y + y = x are respectively instances of right_loop and rev_right_loop + The corresponding lemmas will use the K and NK/VK suffixes, respectively. + + - Morphisms for functions and relations: + {morph f : x / a >-> r} <-> f is a morphism with respect to functions + (fun x => a) and (fun x => r); if r == R#[#x#]#, + this states that f a = R#[#f x#]# for all x. + {morph f : x / a} <-> f is a morphism with respect to the + function expression (fun x => a). This is + shorthand for {morph f : x / a >-> a}; note + that the two instances of a are often + interpreted at different types. + {morph f : x y / a >-> r} <-> f is a morphism with respect to functions + (fun x y => a) and (fun x y => r). + {morph f : x y / a} <-> f is a morphism with respect to the + function expression (fun x y => a). + {homo f : x / a >-> r} <-> f is a homomorphism with respect to the + predicates (fun x => a) and (fun x => r); + if r == R#[#x#]#, this states that a -> R#[#f x#]# + for all x. + {homo f : x / a} <-> f is a homomorphism with respect to the + predicate expression (fun x => a). + {homo f : x y / a >-> r} <-> f is a homomorphism with respect to the + relations (fun x y => a) and (fun x y => r). + {homo f : x y / a} <-> f is a homomorphism with respect to the + relation expression (fun x y => a). + {mono f : x / a >-> r} <-> f is monotone with respect to projectors + (fun x => a) and (fun x => r); if r == R#[#x#]#, + this states that R#[#f x#]# = a for all x. + {mono f : x / a} <-> f is monotone with respect to the projector + expression (fun x => a). + {mono f : x y / a >-> r} <-> f is monotone with respect to relators + (fun x y => a) and (fun x y => r). + {mono f : x y / a} <-> f is monotone with respect to the relator + expression (fun x y => a). + + The file also contains some basic lemmas for the above concepts. + Lemmas relative to cancellation laws use some abbreviated suffixes: + K - a cancellation rule like esymK : cancel (@esym T x y) (@esym T y x). + LR - a lemma moving an operation from the left hand side of a relation to + the right hand side, like canLR: cancel g f -> x = g y -> f x = y. + RL - a lemma moving an operation from the right to the left, e.g., canRL. + Beware that the LR and RL orientations refer to an "apply" (back chaining) + usage; when using the same lemmas with "have" or "move" (forward chaining) + the directions will be reversed!. **) + Set Implicit Arguments. Unset Strict Implicit. @@ -220,7 +223,7 @@ Declare Scope fun_scope. Delimit Scope fun_scope with FUN. Open Scope fun_scope. -(* Notations for argument transpose *) +(** Notations for argument transpose **) Notation "f ^~ y" := (fun x => f x y) (at level 10, y at level 8, no associativity, format "f ^~ y") : fun_scope. Notation "@^~ x" := (fun f => f x) @@ -230,7 +233,7 @@ Declare Scope pair_scope. Delimit Scope pair_scope with PAIR. Open Scope pair_scope. -(* Notations for pair/conjunction projections *) +(** Notations for pair/conjunction projections **) Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1") : pair_scope. Notation "p .2" := (snd p) @@ -241,8 +244,9 @@ Coercion pair_of_and P Q (PandQ : P /\ Q) := (proj1 PandQ, proj2 PandQ). Definition all_pair I T U (w : forall i : I, T i * U i) := (fun i => (w i).1, fun i => (w i).2). -(* Complements on the option type constructor, used below to *) -(* encode partial functions. *) +(** + Complements on the option type constructor, used below to + encode partial functions. **) Module Option. @@ -262,7 +266,7 @@ Notation obind := Option.bind. Notation omap := Option.map. Notation some := (@Some _) (only parsing). -(* Shorthand for some basic equality lemmas. *) +(** Shorthand for some basic equality lemmas. **) Notation erefl := refl_equal. Notation ecast i T e x := (let: erefl in _ = i := e return T in x). @@ -271,31 +275,32 @@ Definition nesym := sym_not_eq. Definition etrans := trans_eq. Definition congr1 := f_equal. Definition congr2 := f_equal2. -(* Force at least one implicit when used as a view. *) +(** Force at least one implicit when used as a view. **) Prenex Implicits esym nesym. -(* A predicate for singleton types. *) +(** A predicate for singleton types. **) Definition all_equal_to T (x0 : T) := forall x, unkeyed x = x0. Lemma unitE : all_equal_to tt. Proof. by case. Qed. -(* A generic wrapper type *) +(** A generic wrapper type **) Structure wrapped T := Wrap {unwrap : T}. Canonical wrap T x := @Wrap T x. Prenex Implicits unwrap wrap Wrap. -(* Syntax for defining auxiliary recursive function. *) -(* Usage: *) -(* Section FooDefinition. *) -(* Variables (g1 : T1) (g2 : T2). (globals) *) -(* Fixoint foo_auxiliary (a3 : T3) ... := *) -(* body, using [rec e3, ...] for recursive calls *) -(* where "[ 'rec' a3 , a4 , ... ]" := foo_auxiliary. *) -(* Definition foo x y .. := [rec e1, ...]. *) -(* + proofs about foo *) -(* End FooDefinition. *) +(** + Syntax for defining auxiliary recursive function. + Usage: + Section FooDefinition. + Variables (g1 : T1) (g2 : T2). (globals) + Fixoint foo_auxiliary (a3 : T3) ... := + body, using #[#rec e3, ... #]# for recursive calls + where " #[# 'rec' a3 , a4 , ... #]#" := foo_auxiliary. + Definition foo x y .. := #[#rec e1, ... #]#. + + proofs about foo + End FooDefinition. **) Reserved Notation "[ 'rec' a0 ]" (at level 0, format "[ 'rec' a0 ]"). @@ -321,8 +326,9 @@ Reserved Notation "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]" (at level 0, format "[ 'rec' a0 , a1 , a2 , a3 , a4 , a5 , a6 , a7 , a8 , a9 ]"). -(* Definitions and notation for explicit functions with simplification, *) -(* i.e., which simpl and /= beta expand (this is complementary to nosimpl). *) +(** + Definitions and notation for explicit functions with simplification, + i.e., which simpl and /= beta expand (this is complementary to nosimpl). **) Section SimplFun. @@ -364,11 +370,12 @@ Notation "[ 'fun' ( x : xT ) ( y : yT ) => E ]" := (fun x : xT => [fun y : yT => E]) (at level 0, x ident, y ident, only parsing) : fun_scope. -(* For delta functions in eqtype.v. *) +(** For delta functions in eqtype.v. **) Definition SimplFunDelta aT rT (f : aT -> aT -> rT) := [fun z => f z z]. -(* Extensional equality, for unary and binary functions, including syntactic *) -(* sugar. *) +(** + Extensional equality, for unary and binary functions, including syntactic + sugar. **) Section ExtensionalEquality. @@ -441,7 +448,7 @@ Notation "@ 'idfun' T " := (@id_head T explicit_id_key) Definition phant_id T1 T2 v1 v2 := phantom T1 v1 -> phantom T2 v2. -(* Strong sigma types. *) +(** Strong sigma types. **) Section Tag. @@ -475,9 +482,9 @@ Lemma all_tag2 I T U V : {f : forall i, T i & forall i, U i (f i) & forall i, V i (f i)}. Proof. by case/all_tag=> f /all_pair[]; exists f. Qed. -(* Refinement types. *) +(** Refinement types. **) -(* Prenex Implicits and renaming. *) +(** Prenex Implicits and renaming. **) Notation sval := (@proj1_sig _ _). Notation "@ 'sval'" := (@proj1_sig) (at level 10, format "@ 'sval'"). @@ -516,16 +523,16 @@ Section Morphism. Variables (aT rT sT : Type) (f : aT -> rT). -(* Morphism property for unary and binary functions *) +(** Morphism property for unary and binary functions **) Definition morphism_1 aF rF := forall x, f (aF x) = rF (f x). Definition morphism_2 aOp rOp := forall x y, f (aOp x y) = rOp (f x) (f y). -(* Homomorphism property for unary and binary relations *) +(** Homomorphism property for unary and binary relations **) Definition homomorphism_1 (aP rP : _ -> Prop) := forall x, aP x -> rP (f x). Definition homomorphism_2 (aR rR : _ -> _ -> Prop) := forall x y, aR x y -> rR (f x) (f y). -(* Stability property for unary and binary relations *) +(** Stability property for unary and binary relations **) Definition monomorphism_1 (aP rP : _ -> sT) := forall x, rP (f x) = aP x. Definition monomorphism_2 (aR rR : _ -> _ -> sT) := forall x y, rR (f x) (f y) = aR x y. @@ -602,16 +609,18 @@ Notation "{ 'mono' f : x y /~ a }" := (at level 0, f at level 99, x ident, y ident, format "{ 'mono' f : x y /~ a }") : type_scope. -(* In an intuitionistic setting, we have two degrees of injectivity. The *) -(* weaker one gives only simplification, and the strong one provides a left *) -(* inverse (we show in `fintype' that they coincide for finite types). *) -(* We also define an intermediate version where the left inverse is only a *) -(* partial function. *) +(** + In an intuitionistic setting, we have two degrees of injectivity. The + weaker one gives only simplification, and the strong one provides a left + inverse (we show in `fintype' that they coincide for finite types). + We also define an intermediate version where the left inverse is only a + partial function. **) Section Injections. -(* rT must come first so we can use @ to mitigate the Coq 1st order *) -(* unification bug (e..g., Coq can't infer rT from a "cancel" lemma). *) +(** + rT must come first so we can use @ to mitigate the Coq 1st order + unification bug (e..g., Coq can't infer rT from a "cancel" lemma). **) Variables (rT aT : Type) (f : aT -> rT). Definition injective := forall x1 x2, f x1 = f x2 -> x1 = x2. @@ -641,10 +650,10 @@ End Injections. Lemma Some_inj {T} : injective (@Some T). Proof. by move=> x y []. Qed. -(* Force implicits to use as a view. *) +(** Force implicits to use as a view. **) Prenex Implicits Some_inj. -(* cancellation lemmas for dependent type casts. *) +(** cancellation lemmas for dependent type casts. **) Lemma esymK T x y : cancel (@esym T x y) (@esym T y x). Proof. by case: y /. Qed. diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml index 776d2a2229..d90b7d754c 100644 --- a/plugins/syntax/r_syntax.ml +++ b/plugins/syntax/r_syntax.ml @@ -34,10 +34,8 @@ let is_gr c gr = match DAst.get c with | _ -> false let positive_modpath = MPfile (make_dir binnums) -let positive_path = make_path binnums "positive" let positive_kn = MutInd.make2 positive_modpath (Label.make "positive") -let glob_positive = IndRef (positive_kn,0) let path_of_xI = ((positive_kn,0),1) let path_of_xO = ((positive_kn,0),2) let path_of_xH = ((positive_kn,0),3) @@ -71,9 +69,7 @@ let rec bignat_of_pos c = match DAst.get c with (* Parsing Z via scopes *) (**********************************************************************) -let z_path = make_path binnums "Z" let z_kn = MutInd.make2 positive_modpath (Label.make "Z") -let glob_z = IndRef (z_kn,0) let path_of_ZERO = ((z_kn,0),1) let path_of_POS = ((z_kn,0),2) let path_of_NEG = ((z_kn,0),3) diff --git a/vernac/vernacinterp.mli b/plugins/syntax/r_syntax.mli index 0fc02c6915..7c3ee60040 100644 --- a/vernac/vernacinterp.mli +++ b/plugins/syntax/r_syntax.mli @@ -7,15 +7,3 @@ (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************) - -(** Interpretation of extended vernac phrases. *) - -type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t - -type plugin_args = Genarg.raw_generic_argument list - -val vinterp_init : unit -> unit -val vinterp_add : bool -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit -val overwriting_vinterp_add : Vernacexpr.extend_name -> plugin_args vernac_command -> unit - -val call : Vernacexpr.extend_name -> plugin_args -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 96213af9c6..4692fe0057 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -66,9 +66,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) if not onlyalg then refresh_sort status ~direction s else t | UnivFlexible alg -> - if onlyalg && alg then - (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t) - else t)) + (if alg then + evdref := Evd.make_nonalgebraic_variable !evdref l); + t)) | Set when refreshset && not direction -> (* Cannot make a universe "lower" than "Set", only refreshing when we want higher universes. *) diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index 422a05c19a..9762d0f1d9 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -188,7 +188,7 @@ let infer_inductive env mie = match mie.mind_entry_universes with | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ as univs -> univs - | Cumulative_ind_entry cumi -> + | Cumulative_ind_entry (nas, cumi) -> let uctx = CumulativityInfo.univ_context cumi in let uarray = Instance.to_array @@ UContext.instance uctx in let env = Environ.push_context uctx env in @@ -207,6 +207,6 @@ let infer_inductive env mie = entries in let variances = Array.map (fun u -> LMap.find u variances) uarray in - Cumulative_ind_entry (CumulativityInfo.make (uctx, variances)) + Cumulative_ind_entry (nas, CumulativityInfo.make (uctx, variances)) in { mie with mind_entry_universes = univs } diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index c93487d377..4db86817c9 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -189,7 +189,7 @@ let classify_vernac e = | VernacWriteState _ -> VtSideff [], VtNow (* Plugins should classify their commands *) | VernacExtend (s,l) -> - try Vernacentries.get_vernac_classifier s l + try Vernacextend.get_vernac_classifier s l with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in let rec static_control_classifier = function diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 2b4d9a7adf..3c262de910 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -148,7 +148,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let cst = Impargs.with_implicit_protection cst () in let inst = match const.Entries.const_entry_universes with | Entries.Monomorphic_const_entry _ -> EInstance.empty - | Entries.Polymorphic_const_entry ctx -> + | Entries.Polymorphic_const_entry (_, ctx) -> (** We mimick what the kernel does, that is ensuring that no additional constraints appear in the body of polymorphic constants. Ideally this should be enforced statically. *) diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index b81967c781..a53e3bf20d 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -118,15 +118,12 @@ let compute_name internal id = | InternalTacticRequest -> Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name -let define internal id c p univs = +let define internal id c poly univs = let fd = declare_constant ~internal in let id = compute_name internal id in let ctx = UState.minimize univs in let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in - let univs = - if p then Polymorphic_const_entry (UState.context ctx) - else Monomorphic_const_entry (UState.context_set ctx) - in + let univs = UState.const_univ_entry ~poly ctx in let entry = { const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5cead11a5c..1646906daa 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1062,6 +1062,12 @@ let intros_replacing ids = (Tacticals.New.tclMAP (fun (id,pos) -> intro_move (Some id) pos) posl) end +(* The standard for implementing Automatic Introduction *) +let auto_intros_tac ids = + Tacticals.New.tclMAP (function + | Name id -> intro_mustbe_force id + | Anonymous -> intro) (List.rev ids) + (* User-level introduction tactics *) let lookup_hypothesis_as_renamed env sigma ccl = function diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 7efadb2c28..b298524ff8 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -70,6 +70,9 @@ val intros_using : Id.t list -> unit Proofview.tactic val intros_replacing : Id.t list -> unit Proofview.tactic val intros_possibly_replacing : Id.t list -> unit Proofview.tactic +(** [auto_intros_tac names] handles Automatic Introduction of binders *) +val auto_intros_tac : Names.Name.t list -> unit Proofview.tactic + val intros : unit Proofview.tactic (** [depth_of_quantified_hypothesis b h g] returns the index of [h] in diff --git a/test-suite/bugs/closed/bug_4771.v b/test-suite/bugs/closed/bug_4771.v new file mode 100644 index 0000000000..e25e5a1be5 --- /dev/null +++ b/test-suite/bugs/closed/bug_4771.v @@ -0,0 +1,21 @@ +(* The following code used to trigger an anomaly in functor substitutions *) + +Module Type Foo. + +Parameter Inline t : nat. + +End Foo. + +Module F(X : Foo). + +Tactic Notation "foo" ref(x) := idtac. + +Ltac g := foo X.t. + +End F. + +Module N. +Definition t := 0 + 0. +End N. + +Module K := F(N). diff --git a/test-suite/bugs/closed/bug_8224.v b/test-suite/bugs/closed/bug_8224.v new file mode 100644 index 0000000000..42dd47d48c --- /dev/null +++ b/test-suite/bugs/closed/bug_8224.v @@ -0,0 +1,9 @@ +(* Checking that terms are evar-free before being grounded *) + +(* This used to raise an anomaly in 8.9 beta *) + +Fail Fixpoint restrict f n := + match n with + | O => nil + | S n => cons (f n) (restrict f n) + end. diff --git a/test-suite/bugs/closed/bug_8791.v b/test-suite/bugs/closed/bug_8791.v new file mode 100644 index 0000000000..9be1936cdf --- /dev/null +++ b/test-suite/bugs/closed/bug_8791.v @@ -0,0 +1,9 @@ +Class Inhabited (A : Type) : Type := populate { inhabitant : A }. + +Definition A := 42. + +Instance foo (A: Type): Inhabited (list A). +Check A. +Abort. + +Fail Instance foo (A : nat) (A : Type) : Inhabited nat. diff --git a/test-suite/bugs/closed/bug_8908.v b/test-suite/bugs/closed/bug_8908.v new file mode 100644 index 0000000000..9c85839b75 --- /dev/null +++ b/test-suite/bugs/closed/bug_8908.v @@ -0,0 +1,8 @@ +Record foo : Type := + { fooA : Type; fooB : Type }. +Definition id {A : Type} (a : A) := a. +Definition untypable : Type. + unshelve refine (let X := _ in let Y : _ := ltac:(let ty := type of X in exact ty) in id Y). + exact foo. + constructor. exact unit. exact unit. +Defined. diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml index 6d8ce7c5d7..047f4cd080 100644 --- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml +++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml @@ -15,7 +15,7 @@ let evil t f = let tc = mkConst tc in let fe = Declare.definition_entry - ~univs:(Polymorphic_const_entry (UContext.make (Instance.of_array [|u|],Constraint.empty))) + ~univs:(Polymorphic_const_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty))) ~types:(Term.mkArrow tc tu) (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1)) in diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 49c292c501..d63b6dbfce 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -79,8 +79,9 @@ mono The command has indeed failed with message: Universe u already exists. Monomorphic bobmorane = -let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff - : Type@{max(tt.u,ff.u)} +let tt := Type@{UnivBinders.32} in +let ff := Type@{UnivBinders.34} in tt -> ff + : Type@{max(UnivBinders.31,UnivBinders.33)} bobmorane is not universe polymorphic The command has indeed failed with message: @@ -150,6 +151,11 @@ Polymorphic NonCumulative Inductive insecind@{u k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{u k} For inseccstr: Argument scope is [type_scope] +Polymorphic insec2@{u} = Prop + : Type@{Set+1} +(* u |= *) + +insec2 is universe polymorphic Polymorphic inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) @@ -171,26 +177,26 @@ inmod@{u} -> Type@{v} (* u v |= *) Applied.infunct is universe polymorphic -axfoo@{i UnivBinders.55 UnivBinders.56} : -Type@{UnivBinders.55} -> Type@{i} -(* i UnivBinders.55 UnivBinders.56 |= *) +axfoo@{i UnivBinders.56 UnivBinders.57} : +Type@{UnivBinders.56} -> Type@{i} +(* i UnivBinders.56 UnivBinders.57 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo -axbar@{i UnivBinders.55 UnivBinders.56} : -Type@{UnivBinders.56} -> Type@{i} -(* i UnivBinders.55 UnivBinders.56 |= *) +axbar@{i UnivBinders.56 UnivBinders.57} : +Type@{UnivBinders.57} -> Type@{i} +(* i UnivBinders.56 UnivBinders.57 |= *) axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axbar -axfoo' : Type@{UnivBinders.58} -> Type@{axbar'.i} +axfoo' : Type@{axbar'.u0} -> Type@{axbar'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant UnivBinders.axfoo' -axbar' : Type@{UnivBinders.58} -> Type@{axbar'.i} +axbar' : Type@{axbar'.u0} -> Type@{axbar'.i} axbar' is not universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index 56474a0723..582a5e969a 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -1,4 +1,5 @@ -(* coq-prog-args: ("-top" "UnivBinders") *) +(* -*- coq-prog-args: ("-top" "UnivBinders"); -*- *) + Set Universe Polymorphism. Set Printing Universes. (* Unset Strict Universe Declaration. *) @@ -73,19 +74,10 @@ Module SecLet. (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *) Unset Strict Universe Declaration. Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *) - Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *) + Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* names disappear into space *) Definition bobmorane := tt -> ff. End foo. - Print bobmorane. (* - bobmorane@{UnivBinders.15 UnivBinders.16 ff.u ff.v} = - let tt := Type@{UnivBinders.16} in let ff := Type@{ff.v} in tt -> ff - : Type@{max(UnivBinders.15,ff.u)} - (* UnivBinders.15 UnivBinders.16 ff.u ff.v |= UnivBinders.16 < UnivBinders.15 - ff.v < ff.u - *) - - bobmorane is universe polymorphic - *) + Print bobmorane. End SecLet. (* fun x x => foo is nonsense with local binders *) @@ -130,6 +122,12 @@ End SomeSec. Print insec. Print insecind. +Section SomeSec2. + Universe u. + Definition insec2@{} := Prop. +End SomeSec2. +Print insec2. + Module SomeMod. Definition inmod@{u} := Type@{u}. Print inmod. diff --git a/test-suite/success/unidecls.v b/test-suite/success/unidecls.v index 7c298c98b6..1bc565cbb5 100644 --- a/test-suite/success/unidecls.v +++ b/test-suite/success/unidecls.v @@ -1,4 +1,4 @@ -(* coq-prog-args: ("-top" "unidecls") *) +(* -*- coq-prog-args: ("-top" "unidecls"); -*- *) Set Printing Universes. Module decls. @@ -46,12 +46,12 @@ Universe secfoo. Section Foo'. Fail Universe secfoo. Universe secfoo2. - Check Type@{Foo'.secfoo2}. + Fail Check Type@{Foo'.secfoo2}. + Check Type@{secfoo2}. Constraint secfoo2 < a. End Foo'. Check Type@{secfoo2}. -Fail Check Type@{Foo'.secfoo2}. Fail Check eq_refl : Type@{secfoo2} = Type@{a}. (** Below, u and v are global, fixed universes *) diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v index 950cd8242b..0aab64e4c4 100644 --- a/theories/Compat/Coq88.v +++ b/theories/Compat/Coq88.v @@ -15,11 +15,10 @@ Require Export Coq.Compat.Coq89. [Require]. So we make all of the relevant notations accessible in compatibility mode. *) Require Coq.Strings.Ascii Coq.Strings.String. +Export String.StringSyntax Ascii.AsciiSyntax. Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef. Require Coq.Reals.Rdefinitions. Require Coq.Numbers.Cyclic.Int31.Int31. -Declare ML Module "string_syntax_plugin". -Declare ML Module "ascii_syntax_plugin". Declare ML Module "r_syntax_plugin". Declare ML Module "int31_syntax_plugin". Numeral Notation BinNums.Z BinIntDef.Z.of_int BinIntDef.Z.to_int : Z_scope. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index d1168694b2..b7c1eaa788 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -23,7 +23,7 @@ Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool). Register Ascii as plugins.syntax.Ascii. Declare Scope char_scope. -Declare ML Module "ascii_syntax_plugin". +Module Export AsciiSyntax. Declare ML Module "ascii_syntax_plugin". End AsciiSyntax. Delimit Scope char_scope with char. Bind Scope char_scope with ascii. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index f6cc8c99ed..a09d518892 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -25,7 +25,7 @@ Inductive string : Set := | String : ascii -> string -> string. Declare Scope string_scope. -Declare ML Module "string_syntax_plugin". +Module Export StringSyntax. Declare ML Module "string_syntax_plugin". End StringSyntax. Delimit Scope string_scope with string. Bind Scope string_scope with string. Local Open Scope string_scope. diff --git a/vernac/classes.ml b/vernac/classes.ml index f4b0015851..b0dba2485a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -146,7 +146,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); instance_hook k pri global imps ?hook (ConstRef cst); id -let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype = +let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype = let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in if program_mode then let hook _ _ vis gr = @@ -189,10 +189,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id in ignore (Pfedit.by init_refine) else if Flags.is_auto_intros () then - ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro)); + ignore (Pfedit.by (Tactics.auto_intros_tac ids)); (match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) () -let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props len = +let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = let props = match props with | Some (true, { CAst.v = CRecord fs }) -> @@ -275,7 +275,7 @@ let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~pro if not (Evd.has_undefined sigma) && not (Option.is_empty term) then declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype else if program_mode || refine || Option.is_empty term then - declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype + declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype else CErrors.user_err Pp.(str "Unsolved obligations remaining."); id @@ -341,7 +341,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~ do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id else do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode - cty k u ctx ctx' pri decl imps subst id props len + cty k u ctx ctx' pri decl imps subst id props let named_of_rel_context l = let open Vars in @@ -370,25 +370,24 @@ let context poly l = user_err Pp.(str "Anonymous variables not allowed in contexts.") in let univs = - let uctx = Evd.universe_context_set sigma in match ctx with | [] -> assert false - | [_] -> - if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context uctx) - else Monomorphic_const_entry uctx + | [_] -> Evd.const_univ_entry ~poly sigma | _::_::_ -> + (** TODO: explain this little belly dance *) if Lib.sections_are_opened () then begin + let uctx = Evd.universe_context_set sigma in Declare.declare_universe_context poly uctx; - if poly then Polymorphic_const_entry Univ.UContext.empty + if poly then Polymorphic_const_entry ([||], Univ.UContext.empty) else Monomorphic_const_entry Univ.ContextSet.empty end - else if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context uctx) + else if poly then + Evd.const_univ_entry ~poly sigma else begin + let uctx = Evd.universe_context_set sigma in Declare.declare_universe_context poly uctx; Monomorphic_const_entry Univ.ContextSet.empty end diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index e990f0cd15..8707121306 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -47,7 +47,7 @@ match local with | Discharge when Lib.sections_are_opened () -> let ctx = match ctx with | Monomorphic_const_entry ctx -> ctx - | Polymorphic_const_entry ctx -> Univ.ContextSet.of_context ctx + | Polymorphic_const_entry (_, ctx) -> Univ.ContextSet.of_context ctx in let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in let _ = declare_variable ident decl in @@ -79,7 +79,7 @@ match local with let () = if do_instance then Typeclasses.declare_instance None false gr in let () = if is_coe then Class.try_add_new_coercion gr ~local p in let inst = match ctx with - | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx + | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx | Monomorphic_const_entry _ -> Univ.Instance.empty in (gr,inst,Lib.is_modtype_strict ()) diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 138696e3a7..a9c499b192 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -99,7 +99,7 @@ let check_mutuality env evd isfix fixl = let names = List.map fst fixl in let preorder = List.map (fun (id,def) -> - (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' (EConstr.of_constr def)) names)) + (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env evd id' def) names)) fixl in let po = partial_order Id.equal preorder in match List.filter (function (_,Inr _) -> true | _ -> false) po with @@ -227,25 +227,28 @@ let interp_recursive ~program_mode ~cofix fixl notations = (* Instantiate evars and check all are resolved *) let sigma = solve_unif_constraints_with_heuristics env_rec sigma in let sigma = Evd.minimize_universes sigma in - (* XXX: We still have evars here in Program *) - let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr ~abort_on_undefined_evars:false sigma) c) fixdefs in - let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in (* Build the fix declaration block *) (env,rec_sign,decl,sigma), (fixnames,fixdefs,fixtypes), List.combine3 fixctxs fiximps fixannots let check_recursive isfix env evd (fixnames,fixdefs,_) = - check_evars_are_solved env evd (Evd.from_env env); if List.for_all Option.has_some fixdefs then begin let fixdefs = List.map Option.get fixdefs in check_mutuality env evd isfix (List.combine fixnames fixdefs) end +let ground_fixpoint env evd (fixnames,fixdefs,fixtypes) = + check_evars_are_solved env evd (Evd.from_env env); + let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr evd) c) fixdefs in + let fixtypes = List.map EConstr.(to_constr evd) fixtypes in + Evd.evar_universe_context evd, (fixnames,fixdefs,fixtypes) + let interp_fixpoint ~cofix l ntns = let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l ntns in check_recursive true env evd fix; - (fix,pl,Evd.evar_universe_context evd,info) + let uctx,fix = ground_fixpoint env evd fix in + (fix,pl,uctx,info) let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns = if List.exists Option.is_empty fixdefs then diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index b1a9c8a5a3..f4569ed3e2 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -51,7 +51,7 @@ val interp_recursive : (* env / signature / univs / evar_map *) (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) * (* names / defs / types *) - (Id.t list * Constr.constr option list * Constr.types list) * + (Id.t list * EConstr.constr option list * EConstr.types list) * (* ctx per mutual def / implicits / struct annotations *) (EConstr.rel_context * Impargs.manual_explicitation list * int option) list diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 5ff3032ec4..f405c4d5a9 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -450,10 +450,10 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not in let univs = match uctx with - | Polymorphic_const_entry uctx -> + | Polymorphic_const_entry (nas, uctx) -> if cum then - Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context uctx) - else Polymorphic_ind_entry uctx + Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context uctx) + else Polymorphic_ind_entry (nas, uctx) | Monomorphic_const_entry uctx -> Monomorphic_ind_entry uctx in @@ -535,11 +535,11 @@ let declare_mutual_inductive_with_eliminations mie pl impls = let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in let (_, kn), prim = declare_mind mie in let mind = Global.mind_of_delta_kn kn in + Declare.declare_univ_binders (IndRef (mind,0)) pl; List.iteri (fun i (indimpls, constrimpls) -> let ind = (mind,i) in let gr = IndRef ind in maybe_declare_manual_implicits false gr indimpls; - Declare.declare_univ_binders gr pl; List.iteri (fun j impls -> maybe_declare_manual_implicits false diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 3d3d825bd0..ebedfb1e0d 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -1,3 +1,13 @@ +(************************************************************************) +(* * 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 Pp open CErrors open Util @@ -204,7 +214,6 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = (** FIXME: include locality *) let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in let gr = ConstRef c in - let () = UnivNames.register_universe_binders gr (Evd.universe_binders sigma) in if Impargs.is_implicit_args () || not (List.is_empty impls) then Impargs.declare_manual_implicits false gr [impls] in @@ -252,10 +261,10 @@ let do_program_recursive local poly fixkind fixl ntns = let collect_evars id def typ imps = (* Generalize by the recursive prototypes *) let def = - EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign) + EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) and typ = (* Worrying... *) - EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign) + EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = @@ -269,6 +278,9 @@ let do_program_recursive local poly fixkind fixl ntns = let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in let () = if not cofix then begin let possible_indexes = List.map ComFixpoint.compute_possible_guardness_evidences info in + (* XXX: are we allowed to have evars here? *) + let fixtypes = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixtypes in + let fixdefs = List.map (EConstr.to_constr ~abort_on_undefined_evars:false evd) fixdefs in let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), Array.of_list fixtypes, Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs) diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 35fb18e292..2fe03a8ec5 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -43,9 +43,11 @@ let declare_definition ident (local, p, k) ce pl imps hook = | Discharge | Local | Global -> let local = get_locality ident ~kind:"definition" local in let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in - ConstRef kn in + let gr = ConstRef kn in + let () = Declare.declare_univ_binders gr pl in + gr + in let () = maybe_declare_manual_implicits false gr imps in - let () = Declare.declare_univ_binders gr pl in let () = definition_message ident in Lemmas.call_hook fix_exn hook local gr; gr diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 8aa459729c..3b041b7065 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -197,10 +197,11 @@ let save ?export_seff id const uctx do_guard (locality,poly,kind) hook = let () = if should_suggest then Proof_using.suggest_constant (Global.env ()) kn in - ConstRef kn + let gr = ConstRef kn in + Declare.declare_univ_binders gr (UState.universe_binders uctx); + gr in definition_message id; - Declare.declare_univ_binders r (UState.universe_binders uctx); call_hook (fun exn -> exn) hook locality r with e when CErrors.noncritical e -> let e = CErrors.push e in @@ -228,7 +229,7 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_, | Discharge -> let impl = false in (* copy values from Vernacentries *) let univs = match univs with - | Polymorphic_const_entry univs -> + | Polymorphic_const_entry (_, univs) -> (* What is going on here? *) Univ.ContextSet.of_context univs | Monomorphic_const_entry univs -> univs @@ -368,10 +369,7 @@ let rec_tac_initializer finite guard thms snl = | _ -> assert false let start_proof_with_initialization kind sigma decl recguard thms snl hook = - let intro_tac (_, (_, (ids, _))) = - Tacticals.New.tclMAP (function - | Name id -> Tactics.intro_mustbe_force id - | Anonymous -> Tactics.intro) (List.rev ids) in + let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in let init_tac,guard = match recguard with | Some (finite,guard,init_tac) -> let rec_tac = rec_tac_initializer finite guard thms snl in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 97ed43c5f4..c2805674e4 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -667,7 +667,7 @@ let declare_obligation prg obl body ty uctx = if not opaque then add_hint (Locality.make_section_locality None) prg constant; definition_message obl.obl_name; let body = match uctx with - | Polymorphic_const_entry uctx -> + | Polymorphic_const_entry (_, uctx) -> Some (DefinedObl (constant, Univ.UContext.instance uctx)) | Monomorphic_const_entry _ -> Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) @@ -1004,10 +1004,7 @@ and solve_obligation_by_tac prg obls i tac = solve_by_tac obl.obl_name (evar_of_obligation obl) tac (pi2 prg.prg_kind) (Evd.evar_universe_context evd) in - let uctx = if pi2 prg.prg_kind - then Polymorphic_const_entry (UState.context ctx) - else Monomorphic_const_entry (UState.context_set ctx) - in + let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in let prg = {prg with prg_ctx = ctx} in let def, obl' = declare_obligation prg obl t ty uctx in obls.(i) <- obl'; diff --git a/vernac/record.ml b/vernac/record.ml index 7a4c38e972..ac84003266 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -277,12 +277,12 @@ let warn_non_primitive_record = strbrk" could not be defined as a primitive record"))) (* We build projections *) -let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields = +let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in let u = match ctx with - | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx + | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx | Monomorphic_const_entry ctx -> Univ.Instance.empty in let paramdecls = Inductive.inductive_paramdecls (mib, u) in @@ -324,7 +324,6 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u (** Already defined by declare_mind silently *) let kn = Projection.Repr.constant p in Declare.definition_message fid; - UnivNames.register_universe_binders (ConstRef kn) ubinders; kn, mkProj (Projection.make p false,mkRel 1) else let ccl = subst_projection fid subst ti in @@ -360,7 +359,6 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u applist (mkConstU (kn,u),proj_args) in Declare.definition_message fid; - UnivNames.register_universe_binders (ConstRef kn) ubinders; kn, constr_fip with Type_errors.TypeError (ctx,te) -> raise (NotDefinable (BadTypedProj (fid,ctx,te))) @@ -389,10 +387,10 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St match univs with | Monomorphic_ind_entry ctx -> false, Monomorphic_const_entry Univ.ContextSet.empty - | Polymorphic_ind_entry ctx -> - true, Polymorphic_const_entry ctx - | Cumulative_ind_entry cumi -> - true, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi) + | Polymorphic_ind_entry (nas, ctx) -> + true, Polymorphic_const_entry (nas, ctx) + | Cumulative_ind_entry (nas, cumi) -> + true, Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context cumi) in let binder_name = match name with @@ -443,7 +441,7 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St let map i (_, _, _, fieldimpls, fields, is_coe, coers) = let rsp = (kn, i) in (* This is ind path of idstruc *) let cstr = (rsp, 1) in - let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers ubinders fieldimpls fields in + let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in let build = ConstructRef cstr in let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in @@ -480,7 +478,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari (DefinitionEntry class_entry, IsDefinition Definition) in let inst, univs = match univs with - | Polymorphic_const_entry uctx -> Univ.UContext.instance uctx, univs + | Polymorphic_const_entry (_, uctx) -> Univ.UContext.instance uctx, univs | Monomorphic_const_entry _ -> Univ.Instance.empty, Monomorphic_const_entry Univ.ContextSet.empty in let cstu = (cst, inst) in @@ -496,9 +494,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari in let cref = ConstRef cst in Impargs.declare_manual_implicits false cref [paramimpls]; - UnivNames.register_universe_binders cref ubinders; Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; - UnivNames.register_universe_binders (ConstRef proj_cst) ubinders; Classes.set_typeclass_transparency (EvalConstRef cst) false false; let sub = match List.hd coers with | Some b -> Some ((if b then Backward else Forward), List.hd priorities) @@ -508,11 +504,11 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari | _ -> let univs = match univs with - | Polymorphic_const_entry univs -> + | Polymorphic_const_entry (nas, univs) -> if cum then - Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs) + Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs) else - Polymorphic_ind_entry univs + Polymorphic_ind_entry (nas, univs) | Monomorphic_const_entry univs -> Monomorphic_ind_entry univs in @@ -541,8 +537,8 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari in let univs, ctx_context, fields = match univs with - | Polymorphic_const_entry univs -> - let usubst, auctx = Univ.abstract_universes univs in + | Polymorphic_const_entry (nas, univs) -> + let usubst, auctx = Univ.abstract_universes nas univs in let usubst = Univ.make_instance_subst usubst in let map c = Vars.subst_univs_level_constr usubst c in let fields = Context.Rel.map map fields in @@ -682,11 +678,11 @@ let definition_structure udecl kind ~template cum poly finite records = let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in let univs = match univs with - | Polymorphic_const_entry univs -> + | Polymorphic_const_entry (nas, univs) -> if cum then - Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs) + Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs) else - Polymorphic_ind_entry univs + Polymorphic_ind_entry (nas, univs) | Monomorphic_const_entry univs -> Monomorphic_ind_entry univs in diff --git a/vernac/record.mli b/vernac/record.mli index 953d5ec3b6..04984030f7 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -20,7 +20,6 @@ val declare_projections : ?kind:Decl_kinds.definition_object_kind -> Id.t -> bool list -> - UnivNames.universe_binders -> Impargs.manual_implicits list -> Constr.rel_context -> (Name.t * bool) list * Constant.t option list diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 30fae756e9..ce93a8baaf 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -8,7 +8,7 @@ Himsg ExplainErr Locality Egramml -Vernacinterp +Vernacextend Ppvernac Proof_using Lemmas diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 74423d482e..1fab35b650 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -30,7 +30,6 @@ open Constrexpr open Redexpr open Lemmas open Locality -open Vernacinterp open Attributes module NamedDecl = Context.Named.Declaration @@ -2268,7 +2267,7 @@ let interp ?proof ~atts ~st c = (* Extensions *) | VernacExtend (opn,args) -> (* XXX: Here we are returning the state! :) *) - let _st : Vernacstate.t = Vernacinterp.call ~atts opn args ~st in + let _st : Vernacstate.t = Vernacextend.call ~atts opn args ~st in () (** A global default timeout, controlled by option "Set Default Timeout n". @@ -2400,147 +2399,3 @@ let interp ?verbosely ?proof ~st cmd = let exn = CErrors.push exn in Vernacstate.invalidate_cache (); iraise exn - -(** VERNAC EXTEND registering *) - -open Genarg -open Extend - -type classifier = Genarg.raw_generic_argument list -> vernac_classification - -type (_, _) ty_sig = -| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig -| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig -| TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig - -type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml - -let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND") - -let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function -| TyNil -> fun f args -> - begin match args with - | [] -> f - | _ :: _ -> type_error () - end -| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args -| TyNonTerminal (tu, ty) -> fun f args -> - begin match args with - | [] -> type_error () - | Genarg.GenArg (Rawwit tag, v) :: args -> - match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with - | None -> type_error () - | Some Refl -> untype_classifier ty (f v) args - end - -(** Stupid GADTs forces us to duplicate the definition just for typing *) -let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function -| TyNil -> fun f args -> - begin match args with - | [] -> f - | _ :: _ -> type_error () - end -| TyTerminal (_, ty) -> fun f args -> untype_command ty f args -| TyNonTerminal (tu, ty) -> fun f args -> - begin match args with - | [] -> type_error () - | Genarg.GenArg (Rawwit tag, v) :: args -> - match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with - | None -> type_error () - | Some Refl -> untype_command ty (f v) args - end - -let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol = function -| TUlist1 l -> Alist1 (untype_user_symbol l) -| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s)) -| TUlist0 l -> Alist0 (untype_user_symbol l) -| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s)) -| TUopt o -> Aopt (untype_user_symbol o) -| TUentry a -> Aentry (Pcoq.genarg_grammar (ExtraArg a)) -| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (ExtraArg a), string_of_int i) - -let rec untype_grammar : type r s. (r, s) ty_sig -> vernac_expr Egramml.grammar_prod_item list = function -| TyNil -> [] -| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty -| TyNonTerminal (tu, ty) -> - let t = rawwit (Egramml.proj_symbol tu) in - let symb = untype_user_symbol tu in - Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty - -let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol - -let classifiers : classifier array String.Map.t ref = ref String.Map.empty - -let get_vernac_classifier (name, i) args = - (String.Map.find name !classifiers).(i) args - -let declare_vernac_classifier name f = - classifiers := String.Map.add name f !classifiers - -let vernac_extend ~command ?classifier ?entry ext = - let get_classifier (TyML (_, ty, _, cl)) = match cl with - | Some cl -> untype_classifier ty cl - | None -> - match classifier with - | Some cl -> fun _ -> cl command - | None -> - let e = match entry with - | None -> "COMMAND" - | Some e -> Pcoq.Gram.Entry.name e - in - let msg = Printf.sprintf "\ - Vernac entry \"%s\" misses a classifier. \ - A classifier is a function that returns an expression \ - of type vernac_classification (see Vernacexpr). You can: \n\ - - Use '... EXTEND %s CLASSIFIED AS QUERY ...' if the \ - new vernacular command does not alter the system state;\n\ - - Use '... EXTEND %s CLASSIFIED AS SIDEFF ...' if the \ - new vernacular command alters the system state but not the \ - parser nor it starts a proof or ends one;\n\ - - Use '... EXTEND %s CLASSIFIED BY f ...' to specify \ - a global function f. The function f will be called passing\ - \"%s\" as the only argument;\n\ - - Add a specific classifier in each clause using the syntax:\n\ - '[...] => [ f ] -> [...]'.\n\ - Specific classifiers have precedence over global \ - classifiers. Only one classifier is called." - command e e e command - in - CErrors.user_err (Pp.strbrk msg) - in - let cl = Array.map_of_list get_classifier ext in - let iter i (TyML (depr, ty, f, _)) = - let f = untype_command ty f in - let r = untype_grammar ty in - let () = vinterp_add depr (command, i) f in - Egramml.extend_vernac_command_grammar (command, i) entry r - in - let () = declare_vernac_classifier command cl in - List.iteri iter ext - -(** VERNAC ARGUMENT EXTEND registering *) - -type 'a argument_rule = -| Arg_alias of 'a Pcoq.Entry.t -| Arg_rules of 'a Extend.production_rule list - -type 'a vernac_argument = { - arg_printer : 'a -> Pp.t; - arg_parsing : 'a argument_rule; -} - -let vernac_argument_extend ~name arg = - let wit = Genarg.create_arg name in - let entry = match arg.arg_parsing with - | Arg_alias e -> - let () = Pcoq.register_grammar wit e in - e - | Arg_rules rules -> - let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in - let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in - e - in - let pr = arg.arg_printer in - let pr x = Genprint.PrinterBasic (fun () -> pr x) in - let () = Genprint.register_vernac_print0 wit pr in - (wit, entry) diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 8ccd121b8f..8d8d7cfcf0 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -36,50 +36,3 @@ val command_focus : unit Proof.focus_kind val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t - -(** {5 VERNAC EXTEND} *) - -type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification - -type (_, _) ty_sig = -| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig -| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig -| TyNonTerminal : - ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> - ('a -> 'r, 'a -> 's) ty_sig - -type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml - -(** Wrapper to dynamically extend vernacular commands. *) -val vernac_extend : - command:string -> - ?classifier:(string -> Vernacexpr.vernac_classification) -> - ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t -> - ty_ml list -> unit - -(** {5 VERNAC ARGUMENT EXTEND} *) - -type 'a argument_rule = -| Arg_alias of 'a Pcoq.Entry.t - (** This is used because CAMLP5 parser can be dumb about rule factorization, - which sometimes requires two entries to be the same. *) -| Arg_rules of 'a Extend.production_rule list - (** There is a discrepancy here as we use directly extension rules and thus - entries instead of ty_user_symbol and thus arguments as roots. *) - -type 'a vernac_argument = { - arg_printer : 'a -> Pp.t; - arg_parsing : 'a argument_rule; -} - -val vernac_argument_extend : name:string -> 'a vernac_argument -> - ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t - -(** {5 STM classifiers} *) - -val get_vernac_classifier : - Vernacexpr.extend_name -> classifier - -(** Low-level API, not for casual user. *) -val declare_vernac_classifier : - string -> classifier array -> unit diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml new file mode 100644 index 0000000000..5fba586298 --- /dev/null +++ b/vernac/vernacextend.ml @@ -0,0 +1,211 @@ +(************************************************************************) +(* * 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 Util +open Pp +open CErrors + +type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t + +type plugin_args = Genarg.raw_generic_argument list + +(* Table of vernac entries *) +let vernac_tab = + (Hashtbl.create 211 : + (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t) + +let vinterp_add depr s f = + try + Hashtbl.add vernac_tab s (depr, f) + with Failure _ -> + user_err ~hdr:"vinterp_add" + (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.") + +let vinterp_map s = + try + Hashtbl.find vernac_tab s + with Failure _ | Not_found -> + user_err ~hdr:"Vernac Interpreter" + (str"Cannot find vernac command " ++ str (fst s) ++ str".") + +let warn_deprecated_command = + let open CWarnings in + create ~name:"deprecated-command" ~category:"deprecated" + (fun pr -> str "Deprecated vernacular command: " ++ pr) + +(* Interpretation of a vernac command *) + +let call opn converted_args ~atts ~st = + let phase = ref "Looking up command" in + try + let depr, callback = vinterp_map opn in + let () = if depr then + let rules = Egramml.get_extend_vernac_rule opn in + let pr_gram = function + | Egramml.GramTerminal s -> str s + | Egramml.GramNonTerminal _ -> str "_" + in + let pr = pr_sequence pr_gram rules in + warn_deprecated_command pr; + in + phase := "Checking arguments"; + let hunk = callback converted_args in + phase := "Executing command"; + hunk ~atts ~st + with + | reraise -> + let reraise = CErrors.push reraise in + if !Flags.debug then + Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); + iraise reraise + +(** VERNAC EXTEND registering *) + +type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification + +type (_, _) ty_sig = +| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig +| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig +| TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig + +type ty_ml = TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml + +let type_error () = CErrors.anomaly (Pp.str "Ill-typed VERNAC EXTEND") + +let rec untype_classifier : type r s. (r, s) ty_sig -> s -> classifier = function +| TyNil -> fun f args -> + begin match args with + | [] -> f + | _ :: _ -> type_error () + end +| TyTerminal (_, ty) -> fun f args -> untype_classifier ty f args +| TyNonTerminal (tu, ty) -> fun f args -> + let open Genarg in + begin match args with + | [] -> type_error () + | GenArg (Rawwit tag, v) :: args -> + match Genarg.genarg_type_eq tag (Egramml.proj_symbol tu) with + | None -> type_error () + | Some Refl -> untype_classifier ty (f v) args + end + +(** Stupid GADTs forces us to duplicate the definition just for typing *) +let rec untype_command : type r s. (r, s) ty_sig -> r -> plugin_args vernac_command = function +| TyNil -> fun f args -> + begin match args with + | [] -> f + | _ :: _ -> type_error () + end +| TyTerminal (_, ty) -> fun f args -> untype_command ty f args +| TyNonTerminal (tu, ty) -> fun f args -> + let open Genarg in + begin match args with + | [] -> type_error () + | GenArg (Rawwit tag, v) :: args -> + match genarg_type_eq tag (Egramml.proj_symbol tu) with + | None -> type_error () + | Some Refl -> untype_command ty (f v) args + end + +let rec untype_user_symbol : type s a b c. (a, b, c) Extend.ty_user_symbol -> (s, a) Extend.symbol = + let open Extend in function +| TUlist1 l -> Alist1 (untype_user_symbol l) +| TUlist1sep (l, s) -> Alist1sep (untype_user_symbol l, Atoken (CLexer.terminal s)) +| TUlist0 l -> Alist0 (untype_user_symbol l) +| TUlist0sep (l, s) -> Alist0sep (untype_user_symbol l, Atoken (CLexer.terminal s)) +| TUopt o -> Aopt (untype_user_symbol o) +| TUentry a -> Aentry (Pcoq.genarg_grammar (Genarg.ExtraArg a)) +| TUentryl (a, i) -> Aentryl (Pcoq.genarg_grammar (Genarg.ExtraArg a), string_of_int i) + +let rec untype_grammar : type r s. (r, s) ty_sig -> Vernacexpr.vernac_expr Egramml.grammar_prod_item list = function +| TyNil -> [] +| TyTerminal (tok, ty) -> Egramml.GramTerminal tok :: untype_grammar ty +| TyNonTerminal (tu, ty) -> + let t = Genarg.rawwit (Egramml.proj_symbol tu) in + let symb = untype_user_symbol tu in + Egramml.GramNonTerminal (Loc.tag (t, symb)) :: untype_grammar ty + +let _ = untype_classifier, untype_command, untype_grammar, untype_user_symbol + +let classifiers : classifier array String.Map.t ref = ref String.Map.empty + +let get_vernac_classifier (name, i) args = + (String.Map.find name !classifiers).(i) args + +let declare_vernac_classifier name f = + classifiers := String.Map.add name f !classifiers + +let vernac_extend ~command ?classifier ?entry ext = + let get_classifier (TyML (_, ty, _, cl)) = match cl with + | Some cl -> untype_classifier ty cl + | None -> + match classifier with + | Some cl -> fun _ -> cl command + | None -> + let e = match entry with + | None -> "COMMAND" + | Some e -> Pcoq.Gram.Entry.name e + in + let msg = Printf.sprintf "\ + Vernac entry \"%s\" misses a classifier. \ + A classifier is a function that returns an expression \ + of type vernac_classification (see Vernacexpr). You can: \n\ + - Use '... EXTEND %s CLASSIFIED AS QUERY ...' if the \ + new vernacular command does not alter the system state;\n\ + - Use '... EXTEND %s CLASSIFIED AS SIDEFF ...' if the \ + new vernacular command alters the system state but not the \ + parser nor it starts a proof or ends one;\n\ + - Use '... EXTEND %s CLASSIFIED BY f ...' to specify \ + a global function f. The function f will be called passing\ + \"%s\" as the only argument;\n\ + - Add a specific classifier in each clause using the syntax:\n\ + '[...] => [ f ] -> [...]'.\n\ + Specific classifiers have precedence over global \ + classifiers. Only one classifier is called." + command e e e command + in + CErrors.user_err (Pp.strbrk msg) + in + let cl = Array.map_of_list get_classifier ext in + let iter i (TyML (depr, ty, f, _)) = + let f = untype_command ty f in + let r = untype_grammar ty in + let () = vinterp_add depr (command, i) f in + Egramml.extend_vernac_command_grammar (command, i) entry r + in + let () = declare_vernac_classifier command cl in + List.iteri iter ext + +(** VERNAC ARGUMENT EXTEND registering *) + +type 'a argument_rule = +| Arg_alias of 'a Pcoq.Entry.t +| Arg_rules of 'a Extend.production_rule list + +type 'a vernac_argument = { + arg_printer : 'a -> Pp.t; + arg_parsing : 'a argument_rule; +} + +let vernac_argument_extend ~name arg = + let wit = Genarg.create_arg name in + let entry = match arg.arg_parsing with + | Arg_alias e -> + let () = Pcoq.register_grammar wit e in + e + | Arg_rules rules -> + let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in + let () = Pcoq.grammar_extend e None (None, [(None, None, rules)]) in + e + in + let pr = arg.arg_printer in + let pr x = Genprint.PrinterBasic (fun () -> pr x) in + let () = Genprint.register_vernac_print0 wit pr in + (wit, entry) diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli new file mode 100644 index 0000000000..bb94f3a6a9 --- /dev/null +++ b/vernac/vernacextend.mli @@ -0,0 +1,60 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +(** Interpretation of extended vernac phrases. *) + +type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t + +type plugin_args = Genarg.raw_generic_argument list + +val call : Vernacexpr.extend_name -> plugin_args -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t + +(** {5 VERNAC EXTEND} *) + +type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification + +type (_, _) ty_sig = +| TyNil : (atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig +| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig +| TyNonTerminal : + ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> + ('a -> 'r, 'a -> 's) ty_sig + +type ty_ml = TyML : bool (** deprecated *) * ('r, 's) ty_sig * 'r * 's option -> ty_ml + +(** Wrapper to dynamically extend vernacular commands. *) +val vernac_extend : + command:string -> + ?classifier:(string -> Vernacexpr.vernac_classification) -> + ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t -> + ty_ml list -> unit + +(** {5 VERNAC ARGUMENT EXTEND} *) + +type 'a argument_rule = +| Arg_alias of 'a Pcoq.Entry.t + (** This is used because CAMLP5 parser can be dumb about rule factorization, + which sometimes requires two entries to be the same. *) +| Arg_rules of 'a Extend.production_rule list + (** There is a discrepancy here as we use directly extension rules and thus + entries instead of ty_user_symbol and thus arguments as roots. *) + +type 'a vernac_argument = { + arg_printer : 'a -> Pp.t; + arg_parsing : 'a argument_rule; +} + +val vernac_argument_extend : name:string -> 'a vernac_argument -> + ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t + +(** {5 STM classifiers} *) + +val get_vernac_classifier : + Vernacexpr.extend_name -> classifier diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml deleted file mode 100644 index eb4282705e..0000000000 --- a/vernac/vernacinterp.ml +++ /dev/null @@ -1,77 +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 Util -open Pp -open CErrors - -type 'a vernac_command = 'a -> atts:Vernacexpr.vernac_flags -> st:Vernacstate.t -> Vernacstate.t - -type plugin_args = Genarg.raw_generic_argument list - -(* Table of vernac entries *) -let vernac_tab = - (Hashtbl.create 211 : - (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t) - -let vinterp_add depr s f = - try - Hashtbl.add vernac_tab s (depr, f) - with Failure _ -> - user_err ~hdr:"vinterp_add" - (str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.") - -let overwriting_vinterp_add s f = - begin - try - let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s - with Not_found -> () - end; - Hashtbl.add vernac_tab s (false, f) - -let vinterp_map s = - try - Hashtbl.find vernac_tab s - with Failure _ | Not_found -> - user_err ~hdr:"Vernac Interpreter" - (str"Cannot find vernac command " ++ str (fst s) ++ str".") - -let vinterp_init () = Hashtbl.clear vernac_tab - -let warn_deprecated_command = - let open CWarnings in - create ~name:"deprecated-command" ~category:"deprecated" - (fun pr -> str "Deprecated vernacular command: " ++ pr) - -(* Interpretation of a vernac command *) - -let call opn converted_args ~atts ~st = - let phase = ref "Looking up command" in - try - let depr, callback = vinterp_map opn in - let () = if depr then - let rules = Egramml.get_extend_vernac_rule opn in - let pr_gram = function - | Egramml.GramTerminal s -> str s - | Egramml.GramNonTerminal _ -> str "_" - in - let pr = pr_sequence pr_gram rules in - warn_deprecated_command pr; - in - phase := "Checking arguments"; - let hunk = callback converted_args in - phase := "Executing command"; - hunk ~atts ~st - with - | reraise -> - let reraise = CErrors.push reraise in - if !Flags.debug then - Feedback.msg_debug (str"Vernac Interpreter " ++ str !phase); - iraise reraise |