diff options
84 files changed, 995 insertions, 889 deletions
diff --git a/.gitignore b/.gitignore index f741135211..709e87cc9c 100644 --- a/.gitignore +++ b/.gitignore @@ -55,7 +55,6 @@ config/coq_config.ml config/coq_config.py config/Info-*.plist dev/ocamldebug-coq -dev/camlp5.dbg plugins/micromega/csdpcert plugins/micromega/.micromega.ml.generated kernel/byterun/dllcoqrun.so @@ -68,6 +67,7 @@ time-of-build-after.log .csdp.cache test-suite/.lia.cache test-suite/.nra.cache +test-suite/.nia.cache test-suite/trace test-suite/misc/universes/all_stdlib.v test-suite/misc/universes/universes.txt @@ -165,8 +165,6 @@ checker/esubst.mli user-contrib .*.sw* .#* -test-suite/.lia.cache -test-suite/.nra.cache plugins/ssr/ssrparser.ml plugins/ssr/ssrvernac.ml diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1669145d9b..01931fd7ef 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-10-04-V1" + CACHEKEY: "bionic_coq-V2018-10-23-V1" IMAGE: "$CI_REGISTRY_IMAGE:$CACHEKEY" # By default, jobs run in the base switch; override to select another switch OPAM_SWITCH: "base" diff --git a/CHANGES.md b/CHANGES.md index 865e1eeb95..ada68f97d5 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -241,6 +241,8 @@ Standard Library - There are now conversions between `string` and `positive`, `Z`, `nat`, and `N` in binary, octal, and hex. +- Added `ByteVector` type that can convert to and from [string]. + Display diffs between proof steps - `coqtop` and `coqide` can now highlight the differences between proof steps diff --git a/META.coq.in b/META.coq.in index 1ccde1338f..16928587cb 100644 --- a/META.coq.in +++ b/META.coq.in @@ -25,6 +25,8 @@ package "config" ( directory = "config" + archive(byte) = "config.cma" + archive(native) = "config.cmxa" ) package "clib" ( @@ -261,7 +261,7 @@ cacheclean: find theories plugins test-suite -name '.*.aux' -exec rm -f {} + cleanconfig: - rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist + rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist distclean: clean cleanconfig cacheclean timingclean diff --git a/Makefile.build b/Makefile.build index 77fcfc0abf..08863014ea 100644 --- a/Makefile.build +++ b/Makefile.build @@ -441,7 +441,7 @@ $(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(COQTOP_BYTE) $(LINKCMO) $(BYTEFLAGS) $(COQTOP_BYTE) -o $@ # For coqc -COQCCMO:=clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo +COQCCMO:=config/config.cma clib/clib.cma lib/lib.cma toplevel/usage.cmo tools/coqc.cmo $(COQC): $(call bestobj, $(COQCCMO)) $(SHOW)'OCAMLBEST -o $@' @@ -502,7 +502,7 @@ $(OCAMLLIBDEPBYTE): tools/ocamllibdep.cmo # The full coqdep (unused by this build, but distributed by make install) -COQDEPCMO:=clib/clib.cma lib/lib.cma tools/coqdep_lexer.cmo \ +COQDEPCMO:=config/config.cma clib/clib.cma lib/lib.cma tools/coqdep_lexer.cmo \ tools/coqdep_common.cmo tools/coqdep.cmo $(COQDEP): $(call bestobj, $(COQDEPCMO)) @@ -513,7 +513,7 @@ $(COQDEPBYTE): $(COQDEPCMO) $(SHOW)'OCAMLC -o $@' $(HIDE)$(call ocamlbyte, $(SYSMOD)) -COQMAKEFILECMO:=clib/clib.cma lib/lib.cma tools/coq_makefile.cmo +COQMAKEFILECMO:=config/config.cma clib/clib.cma lib/lib.cma tools/coq_makefile.cmo $(COQMAKEFILE): $(call bestobj,$(COQMAKEFILECMO)) $(SHOW)'OCAMLBEST -o $@' @@ -539,7 +539,7 @@ $(COQWCBYTE): tools/coqwc.cmo $(SHOW)'OCAMLC -o $@' $(HIDE)$(call ocamlbyte, -package str) -COQDOCCMO:=clib/clib.cma lib/lib.cma $(addprefix tools/coqdoc/, \ +COQDOCCMO:=config/config.cma clib/clib.cma lib/lib.cma $(addprefix tools/coqdoc/, \ cdglobals.cmo alpha.cmo index.cmo tokens.cmo output.cmo cpretty.cmo main.cmo ) $(COQDOC): $(call bestobj, $(COQDOCCMO)) @@ -550,7 +550,7 @@ $(COQDOCBYTE): $(COQDOCCMO) $(SHOW)'OCAMLC -o $@' $(HIDE)$(call ocamlbyte, -package str,unix) -COQWORKMGRCMO:=clib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo +COQWORKMGRCMO:=config/config.cma clib/clib.cma lib/lib.cma stm/spawned.cmo stm/coqworkmgrApi.cmo tools/coqworkmgr.cmo $(COQWORKMGR): $(call bestobj, $(COQWORKMGRCMO)) $(SHOW)'OCAMLBEST -o $@' @@ -563,7 +563,7 @@ $(COQWORKMGRBYTE): $(COQWORKMGRCMO) # fake_ide : for debugging or test-suite purpose, a fake ide simulating # a connection to coqidetop -FAKEIDECMO:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo ide/fake_ide.cmo +FAKEIDECMO:=config/config.cma clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma ide/document.cmo ide/fake_ide.cmo $(FAKEIDE): $(call bestobj, $(FAKEIDECMO)) | $(IDETOP) $(SHOW)'OCAMLBEST -o $@' diff --git a/Makefile.checker b/Makefile.checker index 6c19a1a42b..e6b1541efa 100644 --- a/Makefile.checker +++ b/Makefile.checker @@ -49,7 +49,7 @@ checker/names.ml: kernel/names.ml sed -i.bak '1i(* AUTOGENERATED FILE: DO NOT EDIT *)\n\n\n\n\n\n\n\n' $@ && rm $@.bak ifeq ($(BEST),opt) -$(CHICKEN): checker/check.cmxa checker/main.mli checker/main.ml +$(CHICKEN): config/config.cmxa checker/check.cmxa checker/main.mli checker/main.ml $(SHOW)'OCAMLOPT -o $@' $(HIDE)$(OCAMLOPT) -linkpkg $(SYSMOD) $(CHKLIBS) $(OPTFLAGS) $(LINKMETADATA) -o $@ $^ $(STRIP_HIDE) $@ @@ -59,7 +59,7 @@ $(CHICKEN): $(CHICKENBYTE) cp $< $@ endif -$(CHICKENBYTE): checker/check.cma checker/main.mli checker/main.ml +$(CHICKENBYTE): config/config.cma checker/check.cma checker/main.mli checker/main.ml $(SHOW)'OCAMLC -o $@' $(HIDE)$(OCAMLC) -linkpkg $(SYSMOD) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -o $@ $^ diff --git a/Makefile.common b/Makefile.common index f90919a4bc..f2a11ee4b4 100644 --- a/Makefile.common +++ b/Makefile.common @@ -117,7 +117,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ # respecting this order is useful for developers that want to load or link # the libraries directly -CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ +CORECMA:=config/config.cma clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \ engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \ parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ stm/stm.cma toplevel/toplevel.cma diff --git a/Makefile.dev b/Makefile.dev index 6a2a1b2101..54710b6690 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -20,10 +20,7 @@ DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/checker_printers.cmo devel: printers -printers: $(CORECMA) $(DEBUGPRINTERS) dev/camlp5.dbg - -dev/camlp5.dbg: - echo "load_printer gramlib.cma" > $@ +printers: $(CORECMA) $(DEBUGPRINTERS) ############ # revision diff --git a/Makefile.ide b/Makefile.ide index cb55960203..6c069a1e50 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -43,7 +43,7 @@ IDESRCDIRS:= $(CORESRCDIRS) ide ide/protocol COQIDEFLAGS=$(addprefix -I , $(IDESRCDIRS)) $(COQIDEINCLUDES) -IDEDEPS:=clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma +IDEDEPS:=config/config.cma clib/clib.cma lib/lib.cma ide/protocol/ideprotocol.cma IDECMA:=ide/ide.cma IDETOPEXE=bin/coqidetop$(EXE) IDETOP=bin/coqidetop.opt$(EXE) diff --git a/checker/check.mllib b/checker/check.mllib index 139fa765b4..173ad1e325 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,5 +1,3 @@ -Coq_config - Analyze Hook Terminal diff --git a/checker/closure.ml b/checker/closure.ml index 5706011607..138499b0e6 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -121,9 +121,6 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA] * abstractions, storing a representation (of type 'a) of the body of * this constant or abstraction. * * i_tab is the cache table of the results - * * i_repr is the function to get the representation from the current - * state of the cache and the body of the constant. The result - * is stored in the table. * * i_rels = (4,[(1,c);(3,d)]) means there are 4 free rel variables * and only those with index 1 and 3 have bodies which are c and d resp. * @@ -156,33 +153,6 @@ end module KeyTable = Hashtbl.Make(KeyHash) -type 'a infos = { - i_flags : reds; - i_repr : 'a infos -> constr -> 'a; - i_env : env; - i_rels : int * (int * constr) list; - i_tab : 'a KeyTable.t } - -let ref_value_cache info ref = - try - Some (KeyTable.find info.i_tab ref) - with Not_found -> - try - let body = - match ref with - | RelKey n -> - let (s,l) = info.i_rels in lift n (Int.List.assoc (s-n) l) - | VarKey id -> raise Not_found - | ConstKey cst -> constant_value info.i_env cst - in - let v = info.i_repr info body in - KeyTable.add info.i_tab ref v; - Some v - with - | Not_found (* List.assoc *) - | NotEvaluableConst _ (* Const *) - -> None - let defined_rels flags env = (* if red_local_const (snd flags) then*) fold_rel_context @@ -193,16 +163,6 @@ let defined_rels flags env = (rel_context env) ~init:(0,[]) (* else (0,[])*) -let mind_equiv_infos info = mind_equiv info.i_env - -let create mk_cl flgs env = - { i_flags = flgs; - i_repr = mk_cl; - i_env = env; - i_rels = defined_rels flgs env; - i_tab = KeyTable.create 17 } - - (**********************************************************************) (* Lazy reduction: the one used in kernel operations *) @@ -255,6 +215,12 @@ and fterm = | FCLOS of constr * fconstr subs | FLOCKED +type clos_infos = { + i_flags : reds; + i_env : env; + i_rels : int * (int * constr) list; + i_tab : fconstr KeyTable.t } + let fterm_of v = v.term let set_norm v = v.norm <- Norm @@ -372,6 +338,30 @@ let mk_clos e t = let mk_clos_vect env v = Array.map (mk_clos env) v +let inject = mk_clos (subs_id 0) + +let ref_value_cache info ref = + try + Some (KeyTable.find info.i_tab ref) + with Not_found -> + try + let body = + match ref with + | RelKey n -> + let (s,l) = info.i_rels in lift n (Int.List.assoc (s-n) l) + | VarKey id -> raise Not_found + | ConstKey cst -> constant_value info.i_env cst + in + let v = inject body in + KeyTable.add info.i_tab ref v; + Some v + with + | Not_found (* List.assoc *) + | NotEvaluableConst _ (* Const *) + -> None + +let mind_equiv_infos info = mind_equiv info.i_env + (* Translate the head constructor of t from constr to fconstr. This function is parameterized by the function to apply on the direct subterms. @@ -783,21 +773,19 @@ let kh info v stk = fapp_stack(kni info v stk) let whd_val info v = with_stats (lazy (term_of_fconstr (kh info v []))) -let inject = mk_clos (subs_id 0) - let whd_stack infos m stk = let k = kni infos m stk in let _ = fapp_stack k in (* to unlock Zupdates! *) k -(* cache of constants: the body is computed only when needed. *) -type clos_infos = fconstr infos - let infos_env x = x.i_env let infos_flags x = x.i_flags let oracle_of_infos x = x.i_env.env_conv_oracle let create_clos_infos flgs env = - create (fun _ -> inject) flgs env + { i_flags = flgs; + i_env = env; + i_rels = defined_rels flgs env; + i_tab = KeyTable.create 17 } let unfold_reference = ref_value_cache diff --git a/checker/closure.mli b/checker/closure.mli index cec785699d..4c6643754b 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -61,10 +61,6 @@ val betadeltaiotanolet : reds type table_key = Constant.t puniverses tableKey -type 'a infos -val ref_value_cache: 'a infos -> table_key -> 'a option -val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos - (************************************************************************) (*s Lazy reduction. *) diff --git a/checker/reduction.ml b/checker/reduction.ml index d36c0ef2c9..58a3f4e410 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -280,17 +280,26 @@ let get_strategy { var_opacity; cst_opacity } = function with Not_found -> default_level) | RelKey _ -> Expand +let dep_order l2r k1 k2 = match k1, k2 with +| RelKey _, RelKey _ -> l2r +| RelKey _, (VarKey _ | ConstKey _) -> true +| VarKey _, RelKey _ -> false +| VarKey _, VarKey _ -> l2r +| VarKey _, ConstKey _ -> true +| ConstKey _, (RelKey _ | VarKey _) -> false +| ConstKey _, ConstKey _ -> l2r + let oracle_order infos l2r k1 k2 = let o = Closure.oracle_of_infos infos in match get_strategy o k1, get_strategy o k2 with - | Expand, Expand -> l2r + | Expand, Expand -> dep_order l2r k1 k2 | Expand, (Opaque | Level _) -> true | (Opaque | Level _), Expand -> false - | Opaque, Opaque -> l2r + | Opaque, Opaque -> dep_order l2r k1 k2 | Level _, Opaque -> true | Opaque, Level _ -> false | Level n1, Level n2 -> - if Int.equal n1 n2 then l2r + if Int.equal n1 n2 then dep_order l2r k1 k2 else n1 < n2 let eq_table_key univ = diff --git a/config/config.mllib b/config/config.mllib new file mode 100644 index 0000000000..ce3ddfca69 --- /dev/null +++ b/config/config.mllib @@ -0,0 +1 @@ +Coq_config @@ -1,18 +1,28 @@ -opam-version: "1.2" +synopsis: "The Coq Proof Assistant" +description: """ +Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. Typical +applications include the certification of properties of programming +languages (e.g. the CompCert compiler certification project, or the +Bedrock verified low-level programming library), the formalization of +mathematics (e.g. the full formalization of the Feit-Thompson theorem +or homotopy type theory) and teaching. +""" +opam-version: "2.0" maintainer: "The Coq development team <coqdev@inria.fr>" authors: "The Coq development team, INRIA, CNRS, and contributors." homepage: "https://coq.inria.fr/" bug-reports: "https://github.com/coq/coq/issues" -dev-repo: "https://github.com/coq/coq.git" +dev-repo: "git+https://github.com/coq/coq.git" license: "LGPL-2.1" -available: [ ocaml-version >= "4.05.0" ] - depends: [ - "dune" { build & >= "1.2.0" } - "ocamlfind" { build } + "ocaml" { >= "4.05.0" } + "dune" { build & >= "1.4.0" } "num" - "camlp5" { >= "7.03" } + "camlp5" { >= "7.03" } ] build-env: [ diff --git a/coqide-server.opam b/coqide-server.opam index 546ce75dbd..ed6f3d98d8 100644 --- a/coqide-server.opam +++ b/coqide-server.opam @@ -1,15 +1,25 @@ -opam-version: "1.2" +synopsis: "The Coq Proof Assistant" +description: """ +Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +This package provides the `coqidetop` language server, an +implementation of Coq's [XML protocol](https://github.com/coq/coq/blob/master/dev/doc/xml-protocol.md) +which allows clients, such as CoqIDE, to interact with Coq in a +structured way. +""" +opam-version: "2.0" maintainer: "The Coq development team <coqdev@inria.fr>" authors: "The Coq development team, INRIA, CNRS, and contributors." homepage: "https://coq.inria.fr/" bug-reports: "https://github.com/coq/coq/issues" -dev-repo: "https://github.com/coq/coq.git" +dev-repo: "git+https://github.com/coq/coq.git" license: "LGPL-2.1" -available: [ocaml-version >= "4.05.0"] - depends: [ - "dune" { build & >= "1.2.0" } + "dune" { build & >= "1.4.0" } "coq" ] diff --git a/coqide.opam b/coqide.opam index 17fb5dbbe2..314943a881 100644 --- a/coqide.opam +++ b/coqide.opam @@ -1,16 +1,23 @@ -opam-version: "1.2" +synopsis: "The Coq Proof Assistant" +description: """ +Coq is a formal proof management system. It provides +a formal language to write mathematical definitions, executable +algorithms and theorems together with an environment for +semi-interactive development of machine-checked proofs. + +This package provides the CoqIDE, a graphical user interface for the +development of interactive proofs. +""" +opam-version: "2.0" maintainer: "The Coq development team <coqdev@inria.fr>" authors: "The Coq development team, INRIA, CNRS, and contributors." homepage: "https://coq.inria.fr/" bug-reports: "https://github.com/coq/coq/issues" -dev-repo: "https://github.com/coq/coq.git" +dev-repo: "git+https://github.com/coq/coq.git" license: "LGPL-2.1" -available: [ocaml-version >= "4.05.0"] - depends: [ - "dune" { build & >= "1.2.0" } - "coq" + "dune" { build & >= "1.4.0" } "coqide-server" "conf-gtksourceview" "lablgtk" { >= "2.18.5" } diff --git a/default.nix b/default.nix index 61f434efe6..9a7afbe89e 100644 --- a/default.nix +++ b/default.nix @@ -23,8 +23,8 @@ { pkgs ? (import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/4c95508641fe780efe41885366e03339b95d04fb.tar.gz"; - sha256 = "1wjspwhzdb6d1kz4khd9l0fivxdk2nq3qvj93pql235sb7909ygx"; + url = "https://github.com/NixOS/nixpkgs/archive/06613c189eebf4d6167d2d010a59cf38b43b6ff4.tar.gz"; + sha256 = "13grhy3cvdwr7wql1rm5d7zsfpvp44cyjhiain4zs70r90q3swdg"; }) {}) , ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06 , buildIde ? true @@ -47,7 +47,7 @@ stdenv.mkDerivation rec { python2 time # coq-makefile timing tools dune ] - ++ (with ocamlPackages; [ ocaml findlib camlp5_strict num ]) + ++ (with ocamlPackages; [ ocaml findlib camlp5 num ]) ++ optional buildIde ocamlPackages.lablgtk ++ optionals buildDoc [ # Sphinx doc dependencies diff --git a/dev/base_db b/dev/base_db index e18ac534ac..155e9591e0 100644 --- a/dev/base_db +++ b/dev/base_db @@ -1,4 +1,5 @@ source core.dbg +load_printer ltac_plugin.cmo load_printer top_printers.cmo install_printer Top_printers.ppid install_printer Top_printers.ppsp diff --git a/dev/checker.dbg b/dev/checker.dbg index b2323b6175..b5b7f0e6d3 100644 --- a/dev/checker.dbg +++ b/dev/checker.dbg @@ -2,5 +2,6 @@ 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 index 327e636c57..fcb6f679ed 100644 --- a/dev/checker_db +++ b/dev/checker_db @@ -2,38 +2,4 @@ source checker.dbg load_printer checker_printers.cmo -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 +source checker_printers.dbg diff --git a/dev/checker_dune_db b/dev/checker_dune_db new file mode 100644 index 0000000000..cdb6a4b809 --- /dev/null +++ b/dev/checker_dune_db @@ -0,0 +1,5 @@ +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 new file mode 100644 index 0000000000..9ebbd74834 --- /dev/null +++ b/dev/checker_printers.dbg @@ -0,0 +1,35 @@ +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/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile index f257c62dd3..098c950b32 100644 --- a/dev/ci/docker/bionic_coq/Dockerfile +++ b/dev/ci/docker/bionic_coq/Dockerfile @@ -1,4 +1,4 @@ -# CACHEKEY: "bionic_coq-V2018-10-04-V2" +# CACHEKEY: "bionic_coq-V2018-10-23-V1" # ^^ Update when modifying this file. FROM ubuntu:bionic @@ -37,7 +37,7 @@ ENV COMPILER="4.05.0" # Common OPAM packages. # `num` does not have a version number as the right version to install varies # with the compiler version. -ENV BASE_OPAM="num ocamlfind.1.8.0 dune.1.2.1 ounit.2.0.8 odoc.1.2.0" \ +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. @@ -56,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \ ENV COMPILER_EDGE="4.07.0" \ CAMLP5_VER_EDGE="7.06" \ COQIDE_OPAM_EDGE="lablgtk.2.18.6 conf-gtksourceview.2" \ - BASE_OPAM_EDGE="dune-release.0.3.0" + BASE_OPAM_EDGE="dune-release.1.1.0" RUN opam switch create $COMPILER_EDGE && eval $(opam env) && \ opam install $BASE_OPAM $BASE_OPAM_EDGE camlp5.$CAMLP5_VER_EDGE $COQIDE_OPAM_EDGE diff --git a/dev/core.dbg b/dev/core.dbg index 972ba701e4..f676b643e4 100644 --- a/dev/core.dbg +++ b/dev/core.dbg @@ -1,6 +1,7 @@ -source camlp5.dbg load_printer threads.cma load_printer str.cma +load_printer gramlib.cma +load_printer config.cma load_printer clib.cma load_printer dynlink.cma load_printer lib.cma @@ -16,4 +17,3 @@ load_printer tactics.cma load_printer vernac.cma load_printer stm.cma load_printer toplevel.cma -load_printer ltac_plugin.cmo diff --git a/dev/core_dune.dbg b/dev/core_dune.dbg new file mode 100644 index 0000000000..cf9c5bd39a --- /dev/null +++ b/dev/core_dune.dbg @@ -0,0 +1,20 @@ +load_printer threads.cma +load_printer str.cma +load_printer gramlib.cma +load_printer config.cma +load_printer clib.cma +load_printer dynlink.cma +load_printer lib.cma +load_printer byterun.cma +load_printer kernel.cma +load_printer library.cma +load_printer engine.cma +load_printer pretyping.cma +load_printer interp.cma +load_printer proofs.cma +load_printer parsing.cma +load_printer printing.cma +load_printer tactics.cma +load_printer vernac.cma +load_printer stm.cma +load_printer toplevel.cma @@ -1,88 +1,6 @@ source core.dbg + +load_printer ltac_plugin.cmo load_printer top_printers.cmo -install_printer Top_printers.pP -install_printer Top_printers.ppfuture -install_printer Top_printers.ppid -install_printer Top_printers.pplab -install_printer Top_printers.ppmbid -install_printer Top_printers.ppdir -install_printer Top_printers.ppmp -install_printer Top_printers.ppcon -install_printer Top_printers.ppproj -install_printer Top_printers.ppkn -install_printer Top_printers.ppmind -install_printer Top_printers.ppind -install_printer Top_printers.ppsp -install_printer Top_printers.ppqualid -install_printer Top_printers.ppclindex -install_printer Top_printers.ppscheme -install_printer Top_printers.ppwf_paths -install_printer Top_printers.ppevar -install_printer Top_printers.ppconstr -install_printer Top_printers.ppsconstr -install_printer Top_printers.ppeconstr -install_printer Top_printers.ppconstr_expr -install_printer Top_printers.ppglob_constr -install_printer Top_printers.pppattern -install_printer Top_printers.ppfconstr -install_printer Top_printers.ppbigint -install_printer Top_printers.ppintset -install_printer Top_printers.ppidset -install_printer Top_printers.ppidmapgen -install_printer Top_printers.ppididmap -install_printer Top_printers.ppconstrunderbindersidmap -install_printer Top_printers.ppevarsubst -install_printer Top_printers.ppunbound_ltac_var_map -install_printer Top_printers.ppclosure -install_printer Top_printers.ppclosedglobconstr -install_printer Top_printers.ppclosedglobconstridmap -install_printer Top_printers.ppglobal -install_printer Top_printers.ppconst -install_printer Top_printers.ppvar -install_printer Top_printers.ppj -install_printer Top_printers.ppsubst -install_printer Top_printers.ppdelta -install_printer Top_printers.pp_idpred -install_printer Top_printers.pp_cpred -install_printer Top_printers.pp_transparent_state -install_printer Top_printers.pp_stack_t -install_printer Top_printers.pp_cst_stack_t -install_printer Top_printers.pp_state_t -install_printer Top_printers.ppmetas -install_printer Top_printers.ppevm -install_printer Top_printers.ppexistentialset -install_printer Top_printers.ppexistentialfilter -install_printer Top_printers.ppclenv -install_printer Top_printers.ppgoalgoal -install_printer Top_printers.ppgoal -install_printer Top_printers.pphintdb -install_printer Top_printers.ppproofview -install_printer Top_printers.ppopenconstr -install_printer Top_printers.pproof -install_printer Top_printers.ppuni -install_printer Top_printers.ppuni_level -install_printer Top_printers.ppuniverse_set -install_printer Top_printers.ppuniverse_instance -install_printer Top_printers.ppuniverse_context -install_printer Top_printers.ppuniverse_context_set -install_printer Top_printers.ppuniverse_subst -install_printer Top_printers.ppuniverse_opt_subst -install_printer Top_printers.ppuniverse_level_subst -install_printer Top_printers.ppevar_universe_context -install_printer Top_printers.ppconstraints -install_printer Top_printers.ppuniverseconstraints -install_printer Top_printers.ppuniverse_context_future -install_printer Top_printers.ppcumulativity_info -install_printer Top_printers.ppabstract_cumulativity_info -install_printer Top_printers.ppuniverses -install_printer Top_printers.ppnamedcontextval -install_printer Top_printers.ppenv -install_printer Top_printers.pptac -install_printer Top_printers.ppobj -install_printer Top_printers.pploc -install_printer Top_printers.pp_argument_type -install_printer Top_printers.pp_generic_argument -install_printer Top_printers.ppgenarginfo -install_printer Top_printers.ppgenargargt -install_printer Top_printers.ppist +source top_printers.dbg diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 91ab57f1e9..0aeb30c4e8 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -68,6 +68,27 @@ Note that you must invoke the `#rectypes;;` toplevel flag in order to use Coq libraries. The provided `.ocamlinit` file does this automatically. +## ocamldebug + +You can use `ocamldebug` with Dune; after a build, do: + +``` +dune exec dev/dune-dbg +(ocd) source dune_db +``` + +or + +``` +dune exec dev/dune-dbg checker +(ocd) source checker_dune_db +``` + +for the checker. Unfortunately, dependency handling here is not fully +refined, so you need to build enough of Coq once to use this target +[it will then correctly compute the deps and rebuild if you call the +script again] This will be fixed in the future. + ## Compositionality, developer and release modes. By default [in "developer mode"], Dune will compose all the packages diff --git a/dev/dune b/dev/dune new file mode 100644 index 0000000000..fd6c8cf32c --- /dev/null +++ b/dev/dune @@ -0,0 +1,25 @@ +(library + (name top_printers) + (public_name coq.top_printers) + (synopsis "Coq's Debug Printers") + (wrapped false) + (modules :standard \ checker_printers) + (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 + ../checker/main.bc + ../topbin/coqtop_byte_bin.bc + ; This is not enough as the call to `ocamlfind` will fail :/ + top_printers.cma) + (action (copy dune-dbg.in dune-dbg))) diff --git a/dev/dune-dbg.in b/dev/dune-dbg.in new file mode 100755 index 0000000000..464e026400 --- /dev/null +++ b/dev/dune-dbg.in @@ -0,0 +1,11 @@ +#!/usr/bin/env bash + +# 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 + ;; +esac diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all index 93b807d5e3..f45f6de529 100644 --- a/dev/dune-workspace.all +++ b/dev/dune-workspace.all @@ -1,4 +1,4 @@ -(lang dune 1.2) +(lang dune 1.4) ; Add custom flags here. Default developer profile is `dev` (context (opam (switch 4.05.0))) diff --git a/dev/dune_db b/dev/dune_db new file mode 100644 index 0000000000..f920f7c75c --- /dev/null +++ b/dev/dune_db @@ -0,0 +1,6 @@ +source core_dune.dbg + +load_printer ltac_plugin.cma +load_printer top_printers.cma + +source top_printers.dbg diff --git a/dev/top_printers.dbg b/dev/top_printers.dbg new file mode 100644 index 0000000000..eab88c7290 --- /dev/null +++ b/dev/top_printers.dbg @@ -0,0 +1,85 @@ +install_printer Top_printers.pP +install_printer Top_printers.ppfuture +install_printer Top_printers.ppid +install_printer Top_printers.pplab +install_printer Top_printers.ppmbid +install_printer Top_printers.ppdir +install_printer Top_printers.ppmp +install_printer Top_printers.ppcon +install_printer Top_printers.ppproj +install_printer Top_printers.ppkn +install_printer Top_printers.ppmind +install_printer Top_printers.ppind +install_printer Top_printers.ppsp +install_printer Top_printers.ppqualid +install_printer Top_printers.ppclindex +install_printer Top_printers.ppscheme +install_printer Top_printers.ppwf_paths +install_printer Top_printers.ppevar +install_printer Top_printers.ppconstr +install_printer Top_printers.ppsconstr +install_printer Top_printers.ppeconstr +install_printer Top_printers.ppconstr_expr +install_printer Top_printers.ppglob_constr +install_printer Top_printers.pppattern +install_printer Top_printers.ppfconstr +install_printer Top_printers.ppbigint +install_printer Top_printers.ppintset +install_printer Top_printers.ppidset +install_printer Top_printers.ppidmapgen +install_printer Top_printers.ppididmap +install_printer Top_printers.ppconstrunderbindersidmap +install_printer Top_printers.ppevarsubst +install_printer Top_printers.ppunbound_ltac_var_map +install_printer Top_printers.ppclosure +install_printer Top_printers.ppclosedglobconstr +install_printer Top_printers.ppclosedglobconstridmap +install_printer Top_printers.ppglobal +install_printer Top_printers.ppconst +install_printer Top_printers.ppvar +install_printer Top_printers.ppj +install_printer Top_printers.ppsubst +install_printer Top_printers.ppdelta +install_printer Top_printers.pp_idpred +install_printer Top_printers.pp_cpred +install_printer Top_printers.pp_transparent_state +install_printer Top_printers.pp_stack_t +install_printer Top_printers.pp_cst_stack_t +install_printer Top_printers.pp_state_t +install_printer Top_printers.ppmetas +install_printer Top_printers.ppevm +install_printer Top_printers.ppexistentialset +install_printer Top_printers.ppexistentialfilter +install_printer Top_printers.ppclenv +install_printer Top_printers.ppgoalgoal +install_printer Top_printers.ppgoal +install_printer Top_printers.pphintdb +install_printer Top_printers.ppproofview +install_printer Top_printers.ppopenconstr +install_printer Top_printers.pproof +install_printer Top_printers.ppuni +install_printer Top_printers.ppuni_level +install_printer Top_printers.ppuniverse_set +install_printer Top_printers.ppuniverse_instance +install_printer Top_printers.ppuniverse_context +install_printer Top_printers.ppuniverse_context_set +install_printer Top_printers.ppuniverse_subst +install_printer Top_printers.ppuniverse_opt_subst +install_printer Top_printers.ppuniverse_level_subst +install_printer Top_printers.ppevar_universe_context +install_printer Top_printers.ppconstraints +install_printer Top_printers.ppuniverseconstraints +install_printer Top_printers.ppuniverse_context_future +install_printer Top_printers.ppcumulativity_info +install_printer Top_printers.ppabstract_cumulativity_info +install_printer Top_printers.ppuniverses +install_printer Top_printers.ppnamedcontextval +install_printer Top_printers.ppenv +install_printer Top_printers.pptac +install_printer Top_printers.ppobj +install_printer Top_printers.pploc +install_printer Top_printers.pp_argument_type +install_printer Top_printers.pp_generic_argument +install_printer Top_printers.ppgenarginfo +install_printer Top_printers.ppgenargargt +install_printer Top_printers.ppist diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index ffdc4f3ec6..57f1174d59 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -120,7 +120,7 @@ G. Dowek, allowed hierarchical developments of mathematical theories. This high-level language was called the *Mathematical Vernacular*. Furthermore, an interactive *Theorem Prover* permitted the incremental construction of proof trees in a top-down manner, subgoaling recursively -and backtracking from dead-alleys. The theorem prover executed tactics +and backtracking from dead-ends. The theorem prover executed tactics written in CAML, in the LCF fashion. A basic set of tactics was predefined, which the user could extend by his own specific tactics. This system (Version 4.10) was released in 1989. Then, the system was diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 381f8bb661..835d6dcaa6 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -533,10 +533,10 @@ Convertibility Let us write :math:`E[Γ] ⊢ t \triangleright u` for the contextual closure of the relation :math:`t` reduces to :math:`u` in the global environment :math:`E` and local context :math:`Γ` with one of the previous -reductions β, ι, δ or ζ. +reductions β, δ, ι or ζ. We say that two terms :math:`t_1` and :math:`t_2` are -*βιδζη-convertible*, or simply *convertible*, or *equivalent*, in the +*βδιζη-convertible*, or simply *convertible*, or *equivalent*, in the global environment :math:`E` and local context :math:`Γ` iff there exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index c802f44ac1..741f9fe5b0 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -144,8 +144,9 @@ list of assertion commands is given in :ref:`Assertions`. The command the proof is a subset of the declared one. The set of declared variables is closed under type dependency. For - example if ``T`` is variable and a is a variable of type ``T``, the commands - ``Proof using a`` and ``Proof using T a`` are actually equivalent. + example, if ``T`` is a variable and ``a`` is a variable of type + ``T``, then the commands ``Proof using a`` and ``Proof using T a`` + are equivalent. .. cmdv:: Proof using {+ @ident } with @tactic diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 52609546d5..3ca0ffe678 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -916,11 +916,8 @@ but also folds ``x`` in the goal. .. coqtop:: reset From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - .. coqtop:: all undo + .. coqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. set z := 3 in Hx. @@ -929,6 +926,10 @@ If the localization also mentions the goal, then the result is the following one .. example:: + .. coqtop:: reset + + From Coq Require Import ssreflect. + .. coqtop:: all Lemma test x t (Hx : x = 3) : x + t = 4. @@ -2485,8 +2486,7 @@ destruction of existential assumptions like in the tactic: .. coqtop:: all Lemma test : True. - have [x Px]: exists x : nat, x > 0. - Focus 2. + have [x Px]: exists x : nat, x > 0; last first. An alternative use of the ``have`` tactic is to provide the explicit proof term for the intermediate lemma, using tactics of the form: @@ -2564,8 +2564,7 @@ copying the goal itself. .. coqtop:: all Lemma test : True. - have suff H : 2 + 2 = 3. - Focus 2. + have suff H : 2 + 2 = 3; last first. Note that H is introduced in the second goal. @@ -2852,8 +2851,7 @@ pattern will be used to process its instance. .. coqtop:: all Lemma simple n (ngt0 : 0 < n ) : P n. - gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0). - Focus 2. + gen have ltnV, /andP[nge0 neq0] : n ngt0 / (0 <= n) && (n != 0); last first. .. _advanced_generalization_ssr: @@ -3556,6 +3554,7 @@ corresponding new goals will be generated. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. + Set Warnings "-notation-overridden". .. coqtop:: all @@ -3756,9 +3755,10 @@ which the function is supplied: :name: congr This tactic: -+ checks that the goal is a Leibniz equality -+ matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints. -+ generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. + + + checks that the goal is a Leibniz equality; + + matches both sides of this equality with “term applied to some arguments”, inferring the right number of arguments from the goal and the type of term. This may expand some definitions or fixpoints; + + generates the subgoals corresponding to pairwise equalities of the arguments present in the goal. The goal can be a non dependent product ``P -> Q``. In that case, the system asserts the equation ``P = Q``, uses it to solve the goal, and @@ -4918,7 +4918,7 @@ which produces the converse implication. In both cases, the two first Prop arguments are implicit. If ``term`` is an instance of the ``reflect`` predicate, then ``A`` will be one -of the defined view hints for the ``reflec``t predicate, which are by +of the defined view hints for the ``reflect`` predicate, which are by default the ones present in the file ``ssrbool.v``. These hints are not only used for choosing the appropriate direction of the translation, but they also allow complex transformation, involving negations. @@ -4933,9 +4933,9 @@ but they also allow complex transformation, involving negations. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: in + .. coqtop:: all - Lemma introN : forall (P : Prop) (b : bool), reflect P b -> ~ P -> ~~b. + Check introN. .. coqtop:: all @@ -4945,12 +4945,11 @@ but they also allow complex transformation, involving negations. In fact this last script does not exactly use the hint ``introN``, but the more general hint: - .. coqtop:: in + .. coqtop:: all - Lemma introNTF : forall (P : Prop) (b c : bool), - reflect P b -> (if c then ~ P else P) -> ~~ b = c. + Check introNTF. - The lemma ` `introN`` is an instantiation of introNF using c := true. + The lemma ``introN`` is an instantiation of ``introNF`` using ``c := true``. Note that views, being part of :token:`i_pattern`, can be used to interpret assertions too. For example the following script asserts ``a && b`` but diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 4cbf75b715..e8f6decfbf 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -502,6 +502,7 @@ through the <tt>Require Import</tt> command.</p> theories/Strings/BinaryString.v theories/Strings/HexString.v theories/Strings/OctalString.v + theories/Strings/ByteVector.v </dd> <dt> <b>Reals</b>: @@ -38,4 +38,5 @@ ; Use summary.log as the target (alias (name runtest) + (package coqide-server) (deps test-suite/summary.log)) diff --git a/dune-project b/dune-project index 607e5a68a5..85238c70c5 100644 --- a/dune-project +++ b/dune-project @@ -1,3 +1,3 @@ -(lang dune 1.2) +(lang dune 1.4) (name coq) diff --git a/engine/namegen.ml b/engine/namegen.ml index 7ce759a3fb..db72dc8ec3 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -21,7 +21,6 @@ open Constr open Environ open EConstr open Vars -open Nametab open Nameops open Libnames open Globnames @@ -82,14 +81,14 @@ let is_imported_ref = function let is_global id = try - let ref = locate (qualid_of_ident id) in + let ref = Nametab.locate (qualid_of_ident id) in not (is_imported_ref ref) with Not_found -> false let is_constructor id = try - match locate (qualid_of_ident id) with + match Nametab.locate (qualid_of_ident id) with | ConstructRef _ -> true | _ -> false with Not_found -> @@ -116,7 +115,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *) | Cast (c,_,_) | App (c,_) -> hdrec c | Proj (kn,_) -> Some (Label.to_id (Constant.label (Projection.constant kn))) | Const _ | Ind _ | Construct _ | Var _ as c -> - Some (basename_of_global (global_of_constr c)) + Some (Nametab.basename_of_global (global_of_constr c)) | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> Some (match lna.(i) with Name id -> id | _ -> assert false) | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None @@ -148,8 +147,8 @@ let hdchar env sigma c = | Cast (c,_,_) | App (c,_) -> hdrec k c | Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn))) | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn)) - | Ind (x,_) -> (try lowercase_first_char (basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") - | Construct (x,_) -> (try lowercase_first_char (basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") | Var id -> lowercase_first_char id | Sort s -> sort_hdchar (ESorts.kind sigma s) | Rel n -> @@ -267,7 +266,7 @@ let visible_ids sigma (nenv, c) = begin try let gseen = GlobRef.Set_env.add g gseen in - let short = shortest_qualid_of_global Id.Set.empty g in + let short = Nametab.shortest_qualid_of_global Id.Set.empty g in let dir, id = repr_qualid short in let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in accu := (gseen, vseen, ids) diff --git a/engine/termops.ml b/engine/termops.ml index ee0c3d210e..e1f5fb0d7f 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -816,26 +816,11 @@ let map_constr_with_full_binders_user_view sigma g f = each binder traversal; it is not recursive *) let fold_constr_with_full_binders sigma g f n acc c = - let open RelDecl in - match EConstr.kind sigma c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> acc - | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c - | Lambda (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g (LocalDef (na, b, t)) n) (f n (f n acc b) t) c - | App (c,l) -> Array.fold_left (f n) (f n acc c) l - | Proj (p,c) -> f n acc c - | Evar (_,l) -> Array.fold_left (f n) acc l - | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl - | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + let open EConstr in + let f l acc c = f l acc (of_constr c) in + let g d l = g (of_rel_decl d) l in + let c = Unsafe.to_constr (whd_evar sigma c) in + Constr.fold_with_full_binders g f n acc c let fold_constr_with_binders sigma g f n acc c = fold_constr_with_full_binders sigma (fun _ x -> g x) f n acc c diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml index 8eddfb3149..06281d6287 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -98,7 +98,7 @@ object(self) ~packing:(vbox#pack ~fill:true ~expand:true) () in let result = Wg_MessageView.message_view () in router#register_route route_id result; - r_bin#add (result :> GObj.widget); + r_bin#add_with_viewport (result :> GObj.widget); views <- (frame#coerce, result, combo#entry) :: views; let cb clr = result#misc#modify_base [`NORMAL, `NAME clr] in let _ = background_color#connect#changed ~callback:cb in @@ -152,9 +152,9 @@ object(self) method show = frame#show; let cur_page = notebook#get_nth_page notebook#current_page in - let _, _, e = - List.find (fun (p,_,_) -> p#get_oid == cur_page#get_oid) views in - e#misc#grab_focus () + match List.find (fun (p,_,_) -> p#get_oid == cur_page#get_oid) views with + | (_, _, e) -> e#misc#grab_focus () + | exception Not_found -> () method hide = frame#hide diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 98e1f6dd36..601099c6ff 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -26,7 +26,6 @@ open Notation_ops open Glob_term open Glob_ops open Pattern -open Nametab open Notation open Detyping open Decl_kinds @@ -213,7 +212,7 @@ let is_record indsp = with Not_found -> false let encode_record r = - let indsp = global_inductive r in + let indsp = Nametab.global_inductive r in if not (is_record indsp) then user_err ?loc:r.CAst.loc ~hdr:"encode_record" (str "This type is not a structure type."); @@ -279,7 +278,7 @@ let extern_evar n l = CEvar (n,l) may be inaccurate *) let default_extern_reference ?loc vars r = - shortest_qualid_of_global ?loc vars r + Nametab.shortest_qualid_of_global ?loc vars r let my_extern_reference = ref default_extern_reference @@ -481,7 +480,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (make_pat_notation ?loc ntn (l,ll) l2') key) end | SynDefRule kn -> - let qid = shortest_qualid_of_syndef ?loc vars kn in + let qid = Nametab.shortest_qualid_of_syndef ?loc vars kn in let l1 = List.rev_map (fun (c,(subentry,(scopt,scl))) -> extern_cases_pattern_in_scope (subentry,(scopt,scl@scopes)) vars c) @@ -1136,7 +1135,7 @@ and extern_notation (custom,scopes as allscopes) vars t = function List.map (fun (c,(subentry,(scopt,scl))) -> extern true (subentry,(scopt,scl@snd scopes)) vars c, None) terms in - let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in + let a = CRef (Nametab.shortest_qualid_of_syndef ?loc vars kn,None) in CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in if List.is_empty args then e else diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d7497d4e8e..6b22261a15 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -28,7 +28,6 @@ open Constrexpr open Constrexpr_ops open Notation_term open Notation_ops -open Nametab open Notation open Inductiveops open Decl_kinds @@ -633,7 +632,7 @@ let terms_of_binders bl = | PatVar (Name id) -> CRef (qualid_of_ident id, None) | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> - let qid = qualid_of_path ?loc (path_of_global (ConstructRef c)) in + let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in @@ -721,7 +720,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = try let gc = intern nenv c in Id.Map.add id (gc, Some c) map - with GlobalizationError _ -> map + with Nametab.GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in @@ -986,7 +985,7 @@ let intern_extended_global_of_qualid qid = let intern_reference qid = let r = try intern_extended_global_of_qualid qid - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid in Smartlocate.global_of_extended_global r @@ -1058,11 +1057,11 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qi (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then (gvar (loc,qualid_basename qid) us, [], [], []), args - else error_global_not_found qid + else Nametab.error_global_not_found qid else let r,projapp,args2 = try intern_qualid qid intern env ntnvars us args - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid in let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 @@ -1312,7 +1311,7 @@ let sort_fields ~complete loc fields completer = (* the reference constructor of the record *) let base_constructor = let global_record_id = ConstructRef record.Recordops.s_CONST in - try shortest_qualid_of_global ?loc Id.Set.empty global_record_id + try Nametab.shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in let () = check_duplicate loc fields in @@ -1493,7 +1492,7 @@ let drop_notations_pattern looked_for genv = in let rec drop_syndef top scopes qid pats = try - match locate_extended qid with + match Nametab.locate_extended qid with | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with @@ -1550,7 +1549,7 @@ let drop_notations_pattern looked_for genv = | None -> raise (InternalizationError (loc,NotAConstructor head)) end | CPatCstr (qid, Some expl_pl, pl) -> - let g = try locate qid + let g = try Nametab.locate qid with Not_found -> raise (InternalizationError (loc,NotAConstructor qid)) in if expl_pl == [] then diff --git a/interp/declare.ml b/interp/declare.ml index 07a0066ea8..7a32018c0e 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -60,14 +60,7 @@ let open_constant i ((sp,kn), obj) = if obj.cst_locl then () else let con = Global.constant_of_delta_kn kn in - Nametab.push (Nametab.Exactly i) sp (ConstRef con); - match (Global.lookup_constant con).const_body with - | (Def _ | Undef _) -> () - | OpaqueDef lc -> - match Opaqueproof.get_constraints (Global.opaque_tables ()) lc with - | Some f when Future.is_val f -> - Global.push_context_set false (Future.force f) - | _ -> () + Nametab.push (Nametab.Exactly i) sp (ConstRef con) let exists_name id = variable_exists id || Global.exists_objlabel (Label.of_id id) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ab57176643..7a525f84a5 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -892,7 +892,9 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) | GVar id' -> (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), sigma - | _ -> anomaly (str "A term which can be a binder has to be a variable.") + | t -> + (* The term is a non-variable pattern *) + raise No_match with Not_found -> (* The matching against a term allowing to find the instance has not been found yet *) (* If it will be a different name, we shall unfortunately fail *) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index e3d490a1ad..b73d238c22 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -15,7 +15,6 @@ open Names open Libnames open Libobject open Lib -open Nametab open Notation_term (* Syntactic definitions. *) @@ -38,7 +37,7 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = let is_alias_of_already_visible_name sp = function | _,NRef ref -> - let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in + let (dir,id) = repr_qualid (Nametab.shortest_qualid_of_global Id.Set.empty ref) in DirPath.is_empty dir && Id.equal id (basename sp) | _ -> false @@ -83,11 +82,11 @@ let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac) let declare_syntactic_definition local id onlyparse pat = let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in () -let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn) +let pr_syndef kn = pr_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) let pr_compat_warning (kn, def, v) = let pp_def = match def with - | [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r + | [], NRef r -> spc () ++ str "is" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r | _ -> strbrk " is a compatibility notation" in pr_syndef kn ++ pp_def diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 819a66c190..c558689595 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -224,11 +224,6 @@ let unfold_red kn = * abstractions, storing a representation (of type 'a) of the body of * this constant or abstraction. * * i_tab is the cache table of the results - * * i_repr is the function to get the representation from the current - * state of the cache and the body of the constant. The result - * is stored in the table. - * * i_rels is the array of free rel variables together with their optional - * body * * ref_value_cache searchs in the tab, otherwise uses i_repr to * compute the result and store it in the table. If the constant can't @@ -256,74 +251,12 @@ end module KeyTable = Hashtbl.Make(IdKeyHash) -let eq_table_key = IdKeyHash.equal - -type 'a infos_tab = 'a KeyTable.t - -type 'a infos_cache = { - i_repr : 'a infos -> 'a infos_tab -> constr -> 'a; - i_env : env; - i_sigma : existential -> constr option; - i_rels : (Constr.rel_declaration * lazy_val) Range.t; - i_share : bool; -} - -and 'a infos = { - i_flags : reds; - i_cache : 'a infos_cache } - -let info_flags info = info.i_flags -let info_env info = info.i_cache.i_env - open Context.Named.Declaration let assoc_defined id env = match Environ.lookup_named id env with | LocalDef (_, c, _) -> c | _ -> raise Not_found -let ref_value_cache ({i_cache = cache;_} as infos) tab ref = - try - Some (KeyTable.find tab ref) - with Not_found -> - try - let body = - match ref with - | RelKey n -> - let open! Context.Rel.Declaration in - let i = n - 1 in - let (d, _) = - try Range.get cache.i_rels i - with Invalid_argument _ -> raise Not_found - in - begin match d with - | LocalAssum _ -> raise Not_found - | LocalDef (_, t, _) -> lift n t - end - | VarKey id -> assoc_defined id cache.i_env - | ConstKey cst -> constant_value_in cache.i_env cst - in - let v = cache.i_repr infos tab body in - KeyTable.add tab ref v; - Some v - with - | Not_found (* List.assoc *) - | NotEvaluableConst _ (* Const *) - -> None - -let evar_value cache ev = - cache.i_sigma ev - -let create ~repr ~share flgs env evars = - let cache = - { i_repr = repr; - i_env = env; - i_sigma = evars; - i_rels = env.env_rel_context.env_rel_map; - i_share = share; - } - in { i_flags = flgs; i_cache = cache } - - (**********************************************************************) (* Lazy reduction: the one used in kernel operations *) @@ -391,6 +324,23 @@ let update ~share v1 no t = v1) else {norm=no;term=t} +(** Reduction cache *) + +type infos_cache = { + i_env : env; + i_sigma : existential -> constr option; + i_share : bool; +} + +type clos_infos = { + i_flags : reds; + i_cache : infos_cache } + +type clos_tab = fconstr KeyTable.t + +let info_flags info = info.i_flags +let info_env info = info.i_cache.i_env + (**********************************************************************) (* The type of (machine) stacks (= lambda-bar-calculus' contexts) *) @@ -539,6 +489,8 @@ let mk_clos e t = | (CoFix _|Lambda _|Fix _|Prod _|Evar _|App _|Case _|Cast _|LetIn _|Proj _) -> {norm = Red; term = FCLOS(t,e)} +let inject c = mk_clos (subs_id 0) c + (** Hand-unrolling of the map function to bypass the call to the generic array allocation *) let mk_clos_vect env v = match v with @@ -550,6 +502,35 @@ let mk_clos_vect env v = match v with [|mk_clos env v0; mk_clos env v1; mk_clos env v2; mk_clos env v3|] | v -> Array.Fun1.map mk_clos env v +let ref_value_cache ({ i_cache = cache; _ }) tab ref = + try + Some (KeyTable.find tab ref) + with Not_found -> + try + let body = + match ref with + | RelKey n -> + let open! Context.Rel.Declaration in + let i = n - 1 in + let (d, _) = + try Range.get cache.i_env.env_rel_context.env_rel_map i + with Invalid_argument _ -> raise Not_found + in + begin match d with + | LocalAssum _ -> raise Not_found + | LocalDef (_, t, _) -> lift n t + end + | VarKey id -> assoc_defined id cache.i_env + | ConstKey cst -> constant_value_in cache.i_env cst + in + let v = inject body in + KeyTable.add tab ref v; + Some v + with + | Not_found (* List.assoc *) + | NotEvaluableConst _ (* Const *) + -> None + (* The inverse of mk_clos: move back to constr *) let rec to_constr lfts v = match v.term with @@ -944,7 +925,7 @@ let rec knr info tab m stk = | FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA -> knit info tab (subs_cons([|v|],e)) bd stk | FEvar(ev,env) -> - (match evar_value info.i_cache ev with + (match info.i_cache.i_sigma ev with Some c -> knit info tab env c stk | None -> (m,stk)) | FLOCKED | FRel _ | FAtom _ | FFlex _ | FInd _ | FApp _ | FProj _ @@ -1040,8 +1021,6 @@ let whd_val info tab v = let norm_val info tab v = with_stats (lazy (kl info tab v)) -let inject c = mk_clos (subs_id 0) c - let whd_stack infos tab m stk = match m.norm with | Whnf | Norm -> (** No need to perform [kni] nor to unlock updates because @@ -1052,19 +1031,19 @@ let whd_stack infos tab m stk = match m.norm with let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *) k -(* cache of constants: the body is computed only when needed. *) -type clos_infos = fconstr infos - let create_clos_infos ?(evars=fun _ -> None) flgs env = let share = (Environ.typing_flags env).Declarations.share_reduction in - create ~share ~repr:(fun _ _ c -> inject c) flgs env evars + let cache = { + i_env = env; + i_sigma = evars; + i_share = share; + } in + { i_flags = flgs; i_cache = cache } let create_tab () = KeyTable.create 17 let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env -let env_of_infos infos = infos.i_cache.i_env - let infos_with_reds infos reds = { infos with i_flags = reds } diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 2a018d172a..1ee4bccc25 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -98,25 +98,7 @@ val unfold_red : evaluable_global_reference -> reds (***********************************************************************) type table_key = Constant.t Univ.puniverses tableKey -type 'a infos_cache -type 'a infos_tab -type 'a infos = { - i_flags : reds; - i_cache : 'a infos_cache } - -val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option -val create: - repr:('a infos -> 'a infos_tab -> constr -> 'a) -> - share:bool -> - reds -> - env -> - (existential -> constr option) -> - 'a infos -val create_tab : unit -> 'a infos_tab -val evar_value : 'a infos_cache -> existential -> constr option - -val info_env : 'a infos -> env -val info_flags: 'a infos -> reds +module KeyTable : Hashtbl.S with type key = table_key (*********************************************************************** s Lazy reduction. *) @@ -173,7 +155,6 @@ val stack_tail : int -> stack -> stack val stack_nth : stack -> int -> fconstr val zip_term : (fconstr -> constr) -> constr -> stack -> constr val eta_expand_stack : stack -> stack -val unfold_projection : 'a infos -> Projection.t -> stack_member option (** To lazy reduce a constr, create a [clos_infos] with [create_clos_infos], inject the term to reduce with [inject]; then use @@ -193,27 +174,32 @@ val destFLambda : (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr (** Global and local constant cache *) -type clos_infos = fconstr infos +type clos_infos +type clos_tab val create_clos_infos : ?evars:(existential->constr option) -> reds -> env -> clos_infos val oracle_of_infos : clos_infos -> Conv_oracle.oracle -val env_of_infos : 'a infos -> env +val create_tab : unit -> clos_tab + +val info_env : clos_infos -> env +val info_flags: clos_infos -> reds +val unfold_projection : clos_infos -> Projection.t -> stack_member option val infos_with_reds : clos_infos -> reds -> clos_infos (** Reduction function *) (** [norm_val] is for strong normalization *) -val norm_val : clos_infos -> fconstr infos_tab -> fconstr -> constr +val norm_val : clos_infos -> clos_tab -> fconstr -> constr (** [whd_val] is for weak head normalization *) -val whd_val : clos_infos -> fconstr infos_tab -> fconstr -> constr +val whd_val : clos_infos -> clos_tab -> fconstr -> constr (** [whd_stack] performs weak head normalization in a given stack. It stops whenever a reduction is blocked. *) val whd_stack : - clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack + clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack (** [eta_expand_ind_stack env ind c s t] computes stacks correspoding to the conversion of the eta expansion of t, considered as an inhabitant @@ -230,9 +216,7 @@ val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> (** Conversion auxiliary functions to do step by step normalisation *) (** [unfold_reference] unfolds references in a [fconstr] *) -val unfold_reference : clos_infos -> fconstr infos_tab -> table_key -> fconstr option - -val eq_table_key : table_key -> table_key -> bool +val unfold_reference : clos_infos -> clos_tab -> table_key -> fconstr option (*********************************************************************** i This is for lazy debug *) @@ -243,9 +227,9 @@ val lift_fconstr_vect : int -> fconstr array -> fconstr array val mk_clos : fconstr subs -> constr -> fconstr val mk_clos_vect : fconstr subs -> constr array -> fconstr array -val kni: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack -val knr: clos_infos -> fconstr infos_tab -> fconstr -> stack -> fconstr * stack -val kl : clos_infos -> fconstr infos_tab -> fconstr -> constr +val kni: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack +val knr: clos_infos -> clos_tab -> fconstr -> stack -> fconstr * stack +val kl : clos_infos -> clos_tab -> fconstr -> constr val to_constr : lift -> fconstr -> constr diff --git a/kernel/constr.ml b/kernel/constr.ml index b490aa5092..d7f35da10d 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -452,6 +452,27 @@ let fold f acc c = match kind c with | CoFix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl +let fold_with_full_binders g f n acc c = + let open Context.Rel.Declaration in + match kind c with + | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc + | Cast (c,_, t) -> f n (f n acc c) t + | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c + | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c + | App (c,l) -> Array.fold_left (f n) (f n acc c) l + | Proj (_,c) -> f n acc c + | Evar (_,l) -> Array.fold_left (f n) acc l + | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl + | Fix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + | CoFix (_,(lna,tl,bl)) -> + let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in + let fd = Array.map2 (fun t b -> (t,b)) tl bl in + Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + (* [iter f c] iters [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *) diff --git a/kernel/constr.mli b/kernel/constr.mli index c012f04260..8753c20eac 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -470,6 +470,10 @@ val map_return_predicate_with_full_binders : ((constr, constr) Context.Rel.Decla val fold : ('a -> constr -> 'a) -> 'a -> constr -> 'a +val fold_with_full_binders : + (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> + 'a -> 'b -> constr -> 'b + (** [map f c] maps [f] on the immediate subterms of [c]; it is not recursive and the order with which subterms are processed is not specified *) diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index c74f2ab318..ac78064235 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -83,18 +83,27 @@ let fold_strategy f { var_opacity; cst_opacity; _ } accu = let get_transp_state { var_trstate; cst_trstate; _ } = (var_trstate, cst_trstate) +let dep_order l2r k1 k2 = match k1, k2 with +| RelKey _, RelKey _ -> l2r +| RelKey _, (VarKey _ | ConstKey _) -> true +| VarKey _, RelKey _ -> false +| VarKey _, VarKey _ -> l2r +| VarKey _, ConstKey _ -> true +| ConstKey _, (RelKey _ | VarKey _) -> false +| ConstKey _, ConstKey _ -> l2r + (* Unfold the first constant only if it is "more transparent" than the second one. In case of tie, use the recommended default. *) let oracle_order f o l2r k1 k2 = match get_strategy o f k1, get_strategy o f k2 with - | Expand, Expand -> l2r + | Expand, Expand -> dep_order l2r k1 k2 | Expand, (Opaque | Level _) -> true | (Opaque | Level _), Expand -> false - | Opaque, Opaque -> l2r + | Opaque, Opaque -> dep_order l2r k1 k2 | Level _, Opaque -> true | Opaque, Level _ -> false | Level n1, Level n2 -> - if Int.equal n1 n2 then l2r + if Int.equal n1 n2 then dep_order l2r k1 k2 else n1 < n2 let get_strategy o = get_strategy o (fun x -> x) diff --git a/kernel/environ.mli b/kernel/environ.mli index 3d653bcfe0..43bfe7c2fb 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -156,6 +156,9 @@ val fold_named_context : (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a val set_universes : env -> UGraph.t -> env +(** This is used to update universes during a proof for the sake of + evar map-unaware functions, eg [Typing] calling + [Typeops.check_hyps_inclusion]. *) (** Recurrence on [named_context] starting from younger decl *) val fold_named_context_reverse : diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 00576476ab..18697d07e5 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -316,8 +316,8 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = type conv_tab = { cnv_inf : clos_infos; - lft_tab : fconstr infos_tab; - rgt_tab : fconstr infos_tab; + lft_tab : clos_tab; + rgt_tab : clos_tab; } (** Invariant: for any tl ∈ lft_tab and tr ∈ rgt_tab, there is no mutable memory location contained both in tl and in tr. *) @@ -346,7 +346,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | (Sort s1, Sort s2) -> if not (is_empty_stack v1 && is_empty_stack v2) then anomaly (Pp.str "conversion was given ill-typed terms (Sort)."); - sort_cmp_universes (env_of_infos infos.cnv_inf) cv_pb s1 s2 cuniv + sort_cmp_universes (info_env infos.cnv_inf) cv_pb s1 s2 cuniv | (Meta n, Meta m) -> if Int.equal n m then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 625b7e5073..12f9592ab7 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -216,15 +216,55 @@ let get_opaque_body env cbo = (Opaqueproof.force_proof (Environ.opaque_tables env) opaque, Opaqueproof.force_constraints (Environ.opaque_tables env) opaque) -type private_constants = Term_typing.side_effects +type side_effect = { + from_env : Declarations.structure_body CEphemeron.key; + eff : Entries.side_eff list; +} -let empty_private_constants = Term_typing.empty_seff -let add_private = Term_typing.add_seff -let concat_private = Term_typing.concat_seff -let mk_pure_proof = Term_typing.mk_pure_proof -let inline_private_constants_in_constr = Term_typing.inline_side_effects -let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects -let side_effects_of_private_constants = Term_typing.uniq_seff +module SideEffects : +sig + type t + val repr : t -> side_effect list + val empty : t + val add : side_effect -> t -> t + val concat : t -> t -> t +end = +struct + +module SeffOrd = struct +open Entries +type t = side_effect +let compare e1 e2 = + let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in + List.compare cmp e1.eff e2.eff +end + +module SeffSet = Set.Make(SeffOrd) + +type t = { seff : side_effect list; elts : SeffSet.t } +(** Invariant: [seff] is a permutation of the elements of [elts] *) + +let repr eff = eff.seff +let empty = { seff = []; elts = SeffSet.empty } +let add x es = + if SeffSet.mem x es.elts then es + else { seff = x :: es.seff; elts = SeffSet.add x es.elts } +let concat xes yes = + List.fold_right add xes.seff yes + +end + +type private_constants = SideEffects.t + +let side_effects_of_private_constants l = + let ans = List.rev (SideEffects.repr l) in + List.map_append (fun { eff; _ } -> eff) ans + +let empty_private_constants = SideEffects.empty +let add_private mb eff effs = + let from_env = CEphemeron.create mb in + SideEffects.add { eff; from_env } effs +let concat_private = SideEffects.concat let make_eff env cst r = let open Entries in @@ -257,7 +297,7 @@ let universes_of_private eff = | Monomorphic_const ctx -> ctx :: acc | Polymorphic_const _ -> acc in - List.fold_left fold [] (Term_typing.uniq_seff eff) + List.fold_left fold [] (side_effects_of_private_constants eff) let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env @@ -507,8 +547,218 @@ let add_constant_aux ~in_section senv (kn, cb) = in senv'' +let mk_pure_proof c = (c, Univ.ContextSet.empty), SideEffects.empty + +let inline_side_effects env body side_eff = + let open Entries in + let open Constr in + (** First step: remove the constants that are still in the environment *) + let filter { eff = se; from_env = mb } = + let map e = (e.seff_constant, e.seff_body, e.seff_env) in + let cbl = List.map map se in + let not_exists (c,_,_) = + try ignore(Environ.lookup_constant c env); false + with Not_found -> true in + let cbl = List.filter not_exists cbl in + (cbl, mb) + in + (* CAVEAT: we assure that most recent effects come first *) + let side_eff = List.map filter (SideEffects.repr side_eff) in + let sigs = List.rev_map (fun (cbl, mb) -> mb, List.length cbl) side_eff in + let side_eff = List.fold_left (fun accu (cbl, _) -> cbl @ accu) [] side_eff in + let side_eff = List.rev side_eff in + (** Most recent side-effects first in side_eff *) + if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs) + else + (** Second step: compute the lifts and substitutions to apply *) + let cname c = Name (Label.to_id (Constant.label c)) in + let fold (subst, var, ctx, args) (c, cb, b) = + let (b, opaque) = match cb.const_body, b with + | Def b, _ -> (Mod_subst.force_constr b, false) + | OpaqueDef _, `Opaque (b,_) -> (b, true) + | _ -> assert false + in + match cb.const_universes with + | Monomorphic_const univs -> + (** Abstract over the term at the top of the proof *) + let ty = cb.const_type in + let subst = Cmap_env.add c (Inr var) subst in + let ctx = Univ.ContextSet.union ctx univs in + (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) + | Polymorphic_const _auctx -> + (** Inline the term to emulate universe polymorphism *) + let subst = Cmap_env.add c (Inl b) subst in + (subst, var, ctx, args) + in + let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, Univ.ContextSet.empty, []) side_eff in + (** Third step: inline the definitions *) + let rec subst_const i k t = match Constr.kind t with + | Const (c, u) -> + let data = try Some (Cmap_env.find c subst) with Not_found -> None in + begin match data with + | None -> t + | Some (Inl b) -> + (** [b] is closed but may refer to other constants *) + subst_const i k (Vars.subst_instance_constr u b) + | Some (Inr n) -> + mkRel (k + n - i) + end + | Rel n -> + (** Lift free rel variables *) + if n <= k then t + else mkRel (n + len - i - 1) + | _ -> Constr.map_with_binders ((+) 1) (fun k t -> subst_const i k t) k t + in + let map_args i (na, b, ty, opaque) = + (** Both the type and the body may mention other constants *) + let ty = subst_const (len - i - 1) 0 ty in + let b = subst_const (len - i - 1) 0 b in + (na, b, ty, opaque) + in + let args = List.mapi map_args args in + let body = subst_const 0 0 body in + let fold_arg (na, b, ty, opaque) accu = + if opaque then mkApp (mkLambda (na, ty, accu), [|b|]) + else mkLetIn (na, b, ty, accu) + in + let body = List.fold_right fold_arg args body in + (body, ctx, sigs) + +let inline_private_constants_in_definition_entry env ce = + let open Entries in + { ce with + const_entry_body = Future.chain + ce.const_entry_body (fun ((body, ctx), side_eff) -> + let body, ctx',_ = inline_side_effects env body side_eff in + let ctx' = Univ.ContextSet.union ctx ctx' in + (body, ctx'), ()); + } + +let inline_private_constants_in_constr env body side_eff = + pi1 (inline_side_effects env body side_eff) + +let rec is_nth_suffix n l suf = + if Int.equal n 0 then l == suf + else match l with + | [] -> false + | _ :: l -> is_nth_suffix (pred n) l suf + +(* Given the list of signatures of side effects, checks if they match. + * I.e. if they are ordered descendants of the current revstruct. + Returns the number of effects that can be trusted. *) +let check_signatures curmb sl = + let is_direct_ancestor accu (mb, how_many) = + match accu with + | None -> None + | Some (n, curmb) -> + try + let mb = CEphemeron.get mb in + if is_nth_suffix how_many mb curmb + then Some (n + how_many, mb) + else None + with CEphemeron.InvalidKey -> None in + let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in + match sl with + | None -> 0 + | Some (n, _) -> n + + +let constant_entry_of_side_effect cb u = + let open Entries in + let univs = + match cb.const_universes with + | Monomorphic_const uctx -> + Monomorphic_const_entry uctx + | Polymorphic_const auctx -> + Polymorphic_const_entry (Univ.AUContext.repr auctx) + in + let pt = + match cb.const_body, u with + | OpaqueDef _, `Opaque (b, c) -> b, c + | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty + | _ -> assert false in + DefinitionEntry { + const_entry_body = Future.from_val (pt, ()); + const_entry_secctx = None; + const_entry_feedback = None; + const_entry_type = Some cb.const_type; + const_entry_universes = univs; + const_entry_opaque = Declareops.is_opaque cb; + const_entry_inline_code = cb.const_inline_code } + +let turn_direct orig = + let open Entries in + let cb = orig.seff_body in + if Declareops.is_opaque cb then + let p = match orig.seff_env with + | `Opaque (b, c) -> (b, c) + | _ -> assert false + in + let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in + let cb = { cb with const_body } in + { orig with seff_body = cb } + else orig + +let export_eff eff = + let open Entries in + (eff.seff_constant, eff.seff_body, eff.seff_role) + +let export_side_effects mb env c = + let open Entries in + let body = c.const_entry_body in + let _, eff = Future.force body in + let ce = { c with + Entries.const_entry_body = Future.chain body + (fun (b_ctx, _) -> b_ctx, ()) } in + let not_exists e = + try ignore(Environ.lookup_constant e.seff_constant env); false + with Not_found -> true in + let aux (acc,sl) { eff = se; from_env = mb } = + let cbl = List.filter not_exists se in + if List.is_empty cbl then acc, sl + else cbl :: acc, (mb,List.length cbl) :: sl in + let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in + let trusted = check_signatures mb signatures in + let push_seff env eff = + let { seff_constant = kn; seff_body = cb ; _ } = eff in + let env = Environ.add_constant kn cb env in + match cb.const_universes with + | Polymorphic_const _ -> env + | Monomorphic_const ctx -> + let ctx = match eff.seff_env with + | `Nothing -> ctx + | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx + in + Environ.push_context_set ~strict:true ctx env + in + let rec translate_seff sl seff acc env = + match seff with + | [] -> List.rev acc, ce + | cbs :: rest -> + if Int.equal sl 0 then + let env, cbs = + List.fold_left (fun (env,cbs) eff -> + let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in + let ce = constant_entry_of_side_effect ocb u in + let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in + let eff = { eff with + seff_body = cb; + seff_env = `Nothing; + } in + (push_seff env eff, export_eff eff :: cbs)) + (env,[]) cbs in + translate_seff 0 rest (cbs @ acc) env + else + let cbs_len = List.length cbs in + let cbs = List.map turn_direct cbs in + let env = List.fold_left push_seff env cbs in + let ecbs = List.map export_eff cbs in + translate_seff (sl - cbs_len) rest (ecbs @ acc) env + in + translate_seff trusted seff [] env + let export_private_constants ~in_section ce senv = - let exported, ce = Term_typing.export_side_effects senv.revstruct senv.env ce in + let exported, ce = export_side_effects senv.revstruct senv.env ce in let bodies = List.map (fun (kn, cb, _) -> (kn, cb)) exported in let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in @@ -520,7 +770,12 @@ let add_constant ~in_section l decl senv = let cb = match decl with | ConstantEntry (EffectEntry, ce) -> - Term_typing.translate_constant (Term_typing.SideEffects senv.revstruct) senv.env kn ce + let handle env body eff = + let body, uctx, signatures = inline_side_effects env body eff in + let trusted = check_signatures senv.revstruct signatures in + body, uctx, trusted + in + Term_typing.translate_constant (Term_typing.SideEffects handle) senv.env kn ce | ConstantEntry (PureEntry, ce) -> Term_typing.translate_constant Term_typing.Pure senv.env kn ce | GlobalRecipe r -> diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 5ccc23eefc..fb1b3e236c 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -27,159 +27,12 @@ module NamedDecl = Context.Named.Declaration (* Insertion of constants and parameters in environment. *) -type side_effect = { - from_env : Declarations.structure_body CEphemeron.key; - eff : side_eff list; -} - -module SideEffects : -sig - type t - val repr : t -> side_effect list - val empty : t - val add : side_effect -> t -> t - val concat : t -> t -> t -end = -struct - -module SeffOrd = struct -type t = side_effect -let compare e1 e2 = - let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in - List.compare cmp e1.eff e2.eff -end - -module SeffSet = Set.Make(SeffOrd) - -type t = { seff : side_effect list; elts : SeffSet.t } -(** Invariant: [seff] is a permutation of the elements of [elts] *) - -let repr eff = eff.seff -let empty = { seff = []; elts = SeffSet.empty } -let add x es = - if SeffSet.mem x es.elts then es - else { seff = x :: es.seff; elts = SeffSet.add x es.elts } -let concat xes yes = - List.fold_right add xes.seff yes - -end - -type side_effects = SideEffects.t +type 'a effect_handler = + env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) type _ trust = | Pure : unit trust -| SideEffects : structure_body -> side_effects trust - -let uniq_seff_rev = SideEffects.repr -let uniq_seff l = - let ans = List.rev (SideEffects.repr l) in - List.map_append (fun { eff ; _ } -> eff) ans - -let empty_seff = SideEffects.empty -let add_seff mb eff effs = - let from_env = CEphemeron.create mb in - SideEffects.add { eff; from_env } effs -let concat_seff = SideEffects.concat - -let mk_pure_proof c = (c, Univ.ContextSet.empty), empty_seff - -let inline_side_effects env body ctx side_eff = - (** First step: remove the constants that are still in the environment *) - let filter { eff = se; from_env = mb } = - let map e = (e.seff_constant, e.seff_body, e.seff_env) in - let cbl = List.map map se in - let not_exists (c,_,_) = - try ignore(Environ.lookup_constant c env); false - with Not_found -> true in - let cbl = List.filter not_exists cbl in - (cbl, mb) - in - (* CAVEAT: we assure that most recent effects come first *) - let side_eff = List.map filter (uniq_seff_rev side_eff) in - let sigs = List.rev_map (fun (cbl, mb) -> mb, List.length cbl) side_eff in - let side_eff = List.fold_left (fun accu (cbl, _) -> cbl @ accu) [] side_eff in - let side_eff = List.rev side_eff in - (** Most recent side-effects first in side_eff *) - if List.is_empty side_eff then (body, ctx, sigs) - else - (** Second step: compute the lifts and substitutions to apply *) - let cname c = Name (Label.to_id (Constant.label c)) in - let fold (subst, var, ctx, args) (c, cb, b) = - let (b, opaque) = match cb.const_body, b with - | Def b, _ -> (Mod_subst.force_constr b, false) - | OpaqueDef _, `Opaque (b,_) -> (b, true) - | _ -> assert false - in - match cb.const_universes with - | Monomorphic_const univs -> - (** Abstract over the term at the top of the proof *) - let ty = cb.const_type in - let subst = Cmap_env.add c (Inr var) subst in - let ctx = Univ.ContextSet.union ctx univs in - (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) - | Polymorphic_const _auctx -> - (** Inline the term to emulate universe polymorphism *) - let subst = Cmap_env.add c (Inl b) subst in - (subst, var, ctx, args) - in - let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, ctx, []) side_eff in - (** Third step: inline the definitions *) - let rec subst_const i k t = match Constr.kind t with - | Const (c, u) -> - let data = try Some (Cmap_env.find c subst) with Not_found -> None in - begin match data with - | None -> t - | Some (Inl b) -> - (** [b] is closed but may refer to other constants *) - subst_const i k (Vars.subst_instance_constr u b) - | Some (Inr n) -> - mkRel (k + n - i) - end - | Rel n -> - (** Lift free rel variables *) - if n <= k then t - else mkRel (n + len - i - 1) - | _ -> Constr.map_with_binders ((+) 1) (fun k t -> subst_const i k t) k t - in - let map_args i (na, b, ty, opaque) = - (** Both the type and the body may mention other constants *) - let ty = subst_const (len - i - 1) 0 ty in - let b = subst_const (len - i - 1) 0 b in - (na, b, ty, opaque) - in - let args = List.mapi map_args args in - let body = subst_const 0 0 body in - let fold_arg (na, b, ty, opaque) accu = - if opaque then mkApp (mkLambda (na, ty, accu), [|b|]) - else mkLetIn (na, b, ty, accu) - in - let body = List.fold_right fold_arg args body in - (body, ctx, sigs) - -let rec is_nth_suffix n l suf = - if Int.equal n 0 then l == suf - else match l with - | [] -> false - | _ :: l -> is_nth_suffix (pred n) l suf - -(* Given the list of signatures of side effects, checks if they match. - * I.e. if they are ordered descendants of the current revstruct. - Returns the number of effects that can be trusted. *) -let check_signatures curmb sl = - let is_direct_ancestor accu (mb, how_many) = - match accu with - | None -> None - | Some (n, curmb) -> - try - let mb = CEphemeron.get mb in - if is_nth_suffix how_many mb curmb - then Some (n + how_many, mb) - else None - with CEphemeron.InvalidKey -> None in - let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in - match sl with - | None -> 0 - | Some (n, _) -> n +| SideEffects : 'a effect_handler -> 'a trust let skip_trusted_seff sl b e = let rec aux sl b e acc = @@ -259,9 +112,9 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let j = infer env body in let _ = judge_of_cast env j DEFAULTcast tyj in j, uctx - | SideEffects mb -> - let (body, uctx, signatures) = inline_side_effects env body uctx side_eff in - let valid_signatures = check_signatures mb signatures in + | SideEffects handle -> + let (body, uctx', valid_signatures) = handle env body side_eff in + let uctx = Univ.ContextSet.union uctx uctx' in let env = push_context_set uctx env in let body,env,ectx = skip_trusted_seff valid_signatures body env in let j = infer env body in @@ -286,9 +139,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let { const_entry_type = typ; const_entry_opaque = opaque ; _ } = c in let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in let (body, ctx), side_eff = Future.join body in - let body, ctx, _ = match trust with - | Pure -> body, ctx, [] - | SideEffects _ -> inline_side_effects env body ctx side_eff + let body, ctx = match trust with + | Pure -> body, ctx + | SideEffects handle -> + let body, ctx', _ = handle env body side_eff in + body, Univ.ContextSet.union ctx ctx' in let env, usubst, univs = match c.const_entry_universes with | Monomorphic_const_entry univs -> @@ -431,101 +286,6 @@ let translate_constant mb env kn ce = build_constant_declaration kn env (infer_declaration ~trust:mb env ce) -let constant_entry_of_side_effect cb u = - let univs = - match cb.const_universes with - | Monomorphic_const uctx -> - Monomorphic_const_entry uctx - | Polymorphic_const auctx -> - Polymorphic_const_entry (Univ.AUContext.repr auctx) - in - let pt = - match cb.const_body, u with - | OpaqueDef _, `Opaque (b, c) -> b, c - | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty - | _ -> assert false in - DefinitionEntry { - const_entry_body = Future.from_val (pt, ()); - const_entry_secctx = None; - const_entry_feedback = None; - const_entry_type = Some cb.const_type; - const_entry_universes = univs; - const_entry_opaque = Declareops.is_opaque cb; - const_entry_inline_code = cb.const_inline_code } -;; - -let turn_direct orig = - let cb = orig.seff_body in - if Declareops.is_opaque cb then - let p = match orig.seff_env with - | `Opaque (b, c) -> (b, c) - | _ -> assert false - in - let const_body = OpaqueDef (Opaqueproof.create (Future.from_val p)) in - let cb = { cb with const_body } in - { orig with seff_body = cb } - else orig - -type exported_side_effect = - Constant.t * constant_body * side_effect_role - -let export_eff eff = - (eff.seff_constant, eff.seff_body, eff.seff_role) - -let export_side_effects mb env c = - let { const_entry_body = body; _ } = c in - let _, eff = Future.force body in - let ce = { c with - const_entry_body = Future.chain body - (fun (b_ctx, _) -> b_ctx, ()) } in - let not_exists e = - try ignore(Environ.lookup_constant e.seff_constant env); false - with Not_found -> true in - let aux (acc,sl) { eff = se; from_env = mb } = - let cbl = List.filter not_exists se in - if List.is_empty cbl then acc, sl - else cbl :: acc, (mb,List.length cbl) :: sl in - let seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in - let trusted = check_signatures mb signatures in - let push_seff env eff = - let { seff_constant = kn; seff_body = cb ; _ } = eff in - let env = Environ.add_constant kn cb env in - match cb.const_universes with - | Polymorphic_const _ -> env - | Monomorphic_const ctx -> - let ctx = match eff.seff_env with - | `Nothing -> ctx - | `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx - in - Environ.push_context_set ~strict:true ctx env - in - let rec translate_seff sl seff acc env = - match seff with - | [] -> List.rev acc, ce - | cbs :: rest -> - if Int.equal sl 0 then - let env, cbs = - List.fold_left (fun (env,cbs) eff -> - let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in - let ce = constant_entry_of_side_effect ocb u in - let cb = translate_constant Pure env kn ce in - let eff = { eff with - seff_body = cb; - seff_env = `Nothing; - } in - (push_seff env eff, export_eff eff :: cbs)) - (env,[]) cbs in - translate_seff 0 rest (cbs @ acc) env - else - let cbs_len = List.length cbs in - let cbs = List.map turn_direct cbs in - let env = List.fold_left push_seff env cbs in - let ecbs = List.map export_eff cbs in - translate_seff (sl - cbs_len) rest (ecbs @ acc) env - in - translate_seff trusted seff [] env -;; - let translate_local_assum env t = let j = infer env t in let t = Typeops.assumption_of_judgment env j in @@ -578,13 +338,3 @@ let translate_local_def env _id centry = (* Insertion of inductive types. *) let translate_mind env kn mie = Indtypes.check_inductive env kn mie - -let inline_entry_side_effects env ce = { ce with - const_entry_body = Future.chain - ce.const_entry_body (fun ((body, ctx), side_eff) -> - let body, ctx',_ = inline_side_effects env body ctx side_eff in - (body, ctx'), ()); -} - -let inline_side_effects env body side_eff = - pi1 (inline_side_effects env body Univ.ContextSet.empty side_eff) diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index ab25090b00..faf434c142 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -14,53 +14,27 @@ open Environ open Declarations open Entries -type side_effects +(** Handlers are used to manage side-effects. The ['a] type stands for the type + of side-effects, and it is parametric because they are only defined later + on. Handlers inline the provided side-effects into the term, and return + the set of additional global constraints that need to be added for the term + to be well typed. *) +type 'a effect_handler = + env -> Constr.t -> 'a -> (Constr.t * Univ.ContextSet.t * int) type _ trust = | Pure : unit trust -| SideEffects : structure_body -> side_effects trust +| SideEffects : 'a effect_handler -> 'a trust val translate_local_def : env -> Id.t -> section_def_entry -> constr * types val translate_local_assum : env -> types -> types -val mk_pure_proof : constr -> side_effects proof_output - -val inline_side_effects : env -> constr -> side_effects -> constr -(** Returns the term where side effects have been turned into let-ins or beta - redexes. *) - -val inline_entry_side_effects : - env -> side_effects definition_entry -> unit definition_entry -(** Same as {!inline_side_effects} but applied to entries. Only modifies the - {!Entries.const_entry_body} field. It is meant to get a term out of a not - yet type checked proof. *) - -val empty_seff : side_effects -val add_seff : Declarations.structure_body -> Entries.side_eff list -> side_effects -> side_effects -val concat_seff : side_effects -> side_effects -> side_effects -(** [concat_seff e1 e2] adds the side-effects of [e1] to [e2], i.e. effects in - [e1] must be more recent than those of [e2]. *) -val uniq_seff : side_effects -> side_eff list -(** Return the list of individual side-effects in the order of their - creation. *) - val translate_constant : 'a trust -> env -> Constant.t -> 'a constant_entry -> constant_body -type exported_side_effect = - Constant.t * constant_body * side_effect_role - -(* Given a constant entry containing side effects it exports them (either - * by re-checking them or trusting them). Returns the constant bodies to - * be pushed in the safe_env by safe typing. The main constant entry - * needs to be translated as usual after this step. *) -val export_side_effects : - structure_body -> env -> side_effects definition_entry -> - exported_side_effect list * unit definition_entry - val translate_mind : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body diff --git a/lib/lib.mllib b/lib/lib.mllib index 41b3622a99..206b2504db 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -1,5 +1,3 @@ -Coq_config - Hook Flags Control diff --git a/library/coqlib.ml b/library/coqlib.ml index 677515981a..a044a9a395 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -14,7 +14,6 @@ open Pp open Names open Libnames open Globnames -open Nametab let make_dir l = DirPath.make (List.rev_map Id.of_string l) @@ -79,7 +78,7 @@ let register_ref s c = (* Generic functions to find Coq objects *) let has_suffix_in_dirs dirs ref = - let dir = dirpath (path_of_global ref) in + let dir = dirpath (Nametab.path_of_global ref) in List.exists (fun d -> is_dirpath_prefix_of d dir) dirs let gen_reference_in_modules locstr dirs s = diff --git a/man/coq-interface.1 b/man/coq-interface.1 deleted file mode 100644 index ee013d952e..0000000000 --- a/man/coq-interface.1 +++ /dev/null @@ -1,37 +0,0 @@ -.TH COQ 1 "April 25, 2001" - -.SH NAME -coq\-interface \- Customized Coq toplevel to make user interfaces - - -.SH SYNOPSIS -.B coq-interface -[ -.B options -] - -.SH DESCRIPTION - -.B coq-interface -is a Coq customized toplevel system for Coq containing some modules -useful for the graphical interface. This program is not for the casual -user. - -.SH OPTIONS - -.TP -.B \-h -Help. Will give you the complete list of options accepted by -coq-interface (the same as coqtop). - -.SH SEE ALSO - -.BR coqc (1), -.BR coqdep (1), -.BR coqtop (1), -.BR coq\-parser (1). -.br -.I -The Coq Reference Manual. -.I -The Coq web site: http://coq.inria.fr diff --git a/man/coq-parser.1 b/man/coq-parser.1 deleted file mode 100644 index 23dc820193..0000000000 --- a/man/coq-parser.1 +++ /dev/null @@ -1,30 +0,0 @@ -.TH COQ 1 "April 25, 2001" - -.SH NAME -coq\-parser \- Coq parser - - -.SH SYNOPSIS -.B coq\-parser -[ -.B options -] - -.SH DESCRIPTION - -.B parser -is a program reading Coq proof developments and outputing them in the -structured format given in the INRIA technical report RT154. This -program is not for the casual user. - -.SH SEE ALSO - -.BR coq\-interface (1), -.BR coqc (1), -.BR coqtop (1), -.BR coqdep (1). -.br -.I -The Coq Reference Manual. -.I -The Coq web site: http://coq.inria.fr diff --git a/man/dune b/man/dune new file mode 100644 index 0000000000..359e780545 --- /dev/null +++ b/man/dune @@ -0,0 +1,10 @@ +(install + (section man) + (package coq) + (files coqc.1 coqtop.1 coqtop.byte.1 coqtop.opt.1 coqchk.1 coqdep.1 coqdoc.1 coq_makefile.1 coq-tex.1 coqwc.1)) + +(install + (section man) + (package coqide) + (files coqide.1)) + diff --git a/parsing/dune b/parsing/dune index b70612a52b..f931321358 100644 --- a/parsing/dune +++ b/parsing/dune @@ -5,11 +5,6 @@ (libraries proofs)) (rule - (targets cLexer.ml) - (deps (:ml4-file cLexer.ml4)) - (action (run camlp5o -loc loc -impl %{ml4-file} -o %{targets}))) - -(rule (targets g_prim.ml) (deps (:mlg-file g_prim.mlg)) (action (run coqpp %{mlg-file}))) diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 1f2c722b34..a88285c9ee 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -115,7 +115,6 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } = (* Summary and Object declaration *) -open Nametab open Libobject type ltac_entry = { @@ -153,19 +152,19 @@ let tac_deprecation kn = let load_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> - let () = if not local then push_tactic (Until i) sp kn in + let () = if not local then push_tactic (Nametab.Until i) sp kn in add ~deprecation kn b t | Some kn0 -> replace kn0 kn t let open_md i ((sp, kn), (local, id, b, t, deprecation)) = match id with | None -> - let () = if not local then push_tactic (Exactly i) sp kn in + let () = if not local then push_tactic (Nametab.Exactly i) sp kn in add ~deprecation kn b t | Some kn0 -> replace kn0 kn t let cache_md ((sp, kn), (local, id ,b, t, deprecation)) = match id with | None -> - let () = push_tactic (Until 1) sp kn in + let () = push_tactic (Nametab.Until 1) sp kn in add ~deprecation kn b t | Some kn0 -> replace kn0 kn t diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 5501cf92a5..55412c74bb 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -19,7 +19,6 @@ open Util open Names open Libnames open Globnames -open Nametab open Smartlocate open Constrexpr open Termops @@ -98,7 +97,7 @@ let intern_global_reference ist qid = ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) else try ArgArg (qid.CAst.loc,locate_global_with_alias qid) - with Not_found -> error_global_not_found qid + with Not_found -> Nametab.error_global_not_found qid let intern_ltac_variable ist qid = if qualid_is_ident qid && find_var (qualid_basename qid) ist then @@ -150,7 +149,7 @@ let intern_isolated_tactic_reference strict ist qid = try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid)) with Not_found -> (* Reference not found *) - error_global_not_found qid + Nametab.error_global_not_found qid (* Internalize an applied tactic reference *) @@ -169,7 +168,7 @@ let intern_applied_tactic_reference ist qid = try intern_applied_global_tactic_reference qid with Not_found -> (* Reference not found *) - error_global_not_found qid + Nametab.error_global_not_found qid (* Intern a reference parsed in a non-tactic entry *) @@ -190,7 +189,7 @@ let intern_non_tactic_reference strict ist qid = TacGeneric ipat else (* Reference not found *) - error_global_not_found qid + Nametab.error_global_not_found qid let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x @@ -302,7 +301,7 @@ let intern_evaluable_global_reference ist qid = try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid) with Not_found -> if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid) - else error_global_not_found qid + else Nametab.error_global_not_found qid let intern_evaluable_reference_or_by_notation ist = function | {v=AN r} -> intern_evaluable_global_reference ist r @@ -377,7 +376,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = subterm matched when a pattern *) let r = match r with | {v=AN r} -> r - | {loc} -> (qualid_of_path ?loc (path_of_global (smart_global r))) in + | {loc} -> (qualid_of_path ?loc (Nametab.path_of_global (smart_global r))) in let sign = { Constrintern.ltac_vars = ist.ltacvars; ltac_bound = Id.Set.empty; diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index f90e889678..b60b77595b 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -23,7 +23,6 @@ open Names open Nameops open Libnames open Globnames -open Nametab open Refiner open Tacmach.New open Tactic_debug @@ -358,7 +357,7 @@ let interp_reference ist env sigma = function with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> error_global_not_found (qualid_of_ident ?loc id) + with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -374,14 +373,14 @@ let interp_evaluable ist env sigma = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> error_global_not_found (qualid_of_ident ?loc id) + | _ -> Nametab.error_global_not_found (qualid_of_ident ?loc id) end | ArgArg (r,None) -> r | ArgVar {loc;v=id} -> try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try try_interp_evaluable env (loc, id) - with Not_found -> error_global_not_found (qualid_of_ident ?loc id) + with Not_found -> Nametab.error_global_not_found (qualid_of_ident ?loc id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -640,7 +639,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id) with Not_found -> - error_global_not_found (qualid_of_ident ?loc id)) + Nametab.error_global_not_found (qualid_of_ident ?loc id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 265909980b..5061aeff88 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -134,7 +134,12 @@ let mkSTACK = function | STACK(0,v0,stk0), stk -> STACK(0,v0,stack_concat stk0 stk) | v,stk -> STACK(0,v,stk) -type cbv_infos = { tab : cbv_value infos_tab; infos : cbv_value infos; sigma : Evd.evar_map } +type cbv_infos = { + env : Environ.env; + tab : cbv_value KeyTable.t; + reds : RedFlags.reds; + sigma : Evd.evar_map +} (* Change: zeta reduction cannot be avoided in CBV *) @@ -260,8 +265,8 @@ let rec norm_head info env t stack = | Proj (p, c) -> let p' = - if red_set (info_flags info.infos) (fCONST (Projection.constant p)) - && red_set (info_flags info.infos) fBETA + if red_set info.reds (fCONST (Projection.constant p)) + && red_set info.reds fBETA then Projection.unfold p else p in @@ -280,16 +285,16 @@ let rec norm_head info env t stack = | Var id -> norm_head_ref 0 info env stack (VarKey id) | Const sp -> - Reductionops.reduction_effect_hook (env_of_infos info.infos) info.sigma + Reductionops.reduction_effect_hook info.env info.sigma (fst sp) (lazy (reify_stack t stack)); norm_head_ref 0 info env stack (ConstKey sp) | LetIn (_, b, _, c) -> (* zeta means letin are contracted; delta without zeta means we *) (* allow bindings but leave let's in place *) - if red_set (info_flags info.infos) fZETA then + if red_set info.reds fZETA then (* New rule: for Cbv, Delta does not apply to locally bound variables - or red_set (info_flags info.infos) fDELTA + or red_set info.reds fDELTA *) let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in norm_head info env' c stack @@ -297,7 +302,7 @@ let rec norm_head info env t stack = (CBN(t,env), stack) (* Should we consider a commutative cut ? *) | Evar ev -> - (match evar_value info.infos.i_cache ev with + (match Reductionops.safe_evar_value info.sigma ev with Some c -> norm_head info env c stack | None -> let e, xs = ev in @@ -317,8 +322,8 @@ let rec norm_head info env t stack = | Prod _ -> (CBN(t,env), stack) and norm_head_ref k info env stack normt = - if red_set_ref (info_flags info.infos) normt then - match ref_value_cache info.infos info.tab normt with + if red_set_ref info.reds normt then + match cbv_value_cache info normt with | Some body -> if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); strip_appl (shift_value k body) stack @@ -343,7 +348,7 @@ and cbv_stack_term info stack env t = and cbv_stack_value info env = function (* a lambda meets an application -> BETA *) | (LAM (nlams,ctxt,b,env), APP (args, stk)) - when red_set (info_flags info.infos) fBETA -> + when red_set info.reds fBETA -> let nargs = Array.length args in if nargs == nlams then cbv_stack_term info stk (subs_cons(args,env)) b @@ -357,31 +362,31 @@ and cbv_stack_value info env = function (* a Fix applied enough -> IOTA *) | (FIXP(fix,env,[||]), stk) - when fixp_reducible (info_flags info.infos) fix stk -> + when fixp_reducible info.reds fix stk -> let (envf,redfix) = contract_fixp env fix in cbv_stack_term info stk envf redfix (* constructor guard satisfied or Cofix in a Case -> IOTA *) | (COFIXP(cofix,env,[||]), stk) - when cofixp_reducible (info_flags info.infos) cofix stk-> + when cofixp_reducible info.reds cofix stk-> let (envf,redfix) = contract_cofixp env cofix in cbv_stack_term info stk envf redfix (* constructor in a Case -> IOTA *) | (CONSTR(((sp,n),u),[||]), APP(args,CASE(_,br,ci,env,stk))) - when red_set (info_flags info.infos) fMATCH -> + when red_set info.reds fMATCH -> let cargs = Array.sub args ci.ci_npar (Array.length args - ci.ci_npar) in cbv_stack_term info (stack_app cargs stk) env br.(n-1) (* constructor of arity 0 in a Case -> IOTA *) | (CONSTR(((_,n),u),[||]), CASE(_,br,_,env,stk)) - when red_set (info_flags info.infos) fMATCH -> + when red_set info.reds fMATCH -> cbv_stack_term info stk env br.(n-1) (* constructor in a Projection -> IOTA *) | (CONSTR(((sp,n),u),[||]), APP(args,PROJ(p,stk))) - when red_set (info_flags info.infos) fMATCH && Projection.unfolded p -> + when red_set info.reds fMATCH && Projection.unfolded p -> let arg = args.(Projection.npars p + Projection.arg p) in cbv_stack_value info env (strip_appl arg stk) @@ -393,6 +398,29 @@ and cbv_stack_value info env = function (* definitely a value *) | (head,stk) -> mkSTACK(head, stk) +and cbv_value_cache info ref = match KeyTable.find info.tab ref with +| v -> Some v +| exception Not_found -> + try + let body = match ref with + | RelKey n -> + let open Context.Rel.Declaration in + begin match Environ.lookup_rel n info.env with + | LocalDef (_, c, _) -> lift n c + | LocalAssum _ -> raise Not_found + end + | VarKey id -> + let open Context.Named.Declaration in + begin match Environ.lookup_named id info.env with + | LocalDef (_, c, _) -> c + | LocalAssum _ -> raise Not_found + end + | ConstKey cst -> Environ.constant_value_in info.env cst + in + let v = cbv_stack_term info TOP (subs_id 0) body in + let () = KeyTable.add info.tab ref v in + Some v + with Not_found | Environ.NotEvaluableConst _ -> None (* When we are sure t will never produce a redex with its stack, we * normalize (even under binders) the applied terms and we build the @@ -453,11 +481,5 @@ let cbv_norm infos constr = EConstr.of_constr (with_stats (lazy (cbv_norm_term infos (subs_id 0) constr))) (* constant bodies are normalized at the first expansion *) -let create_cbv_infos flgs env sigma = - let infos = create - ~share:true (** Not used by cbv *) - ~repr:(fun old_info tab c -> cbv_stack_term { tab; infos = old_info; sigma } TOP (subs_id 0) c) - flgs - env - (Reductionops.safe_evar_value sigma) in - { tab = CClosure.create_tab (); infos; sigma } +let create_cbv_infos reds env sigma = + { tab = KeyTable.create 91; reds; env; sigma } diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 543eea59c1..2c2a8fe49e 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -15,7 +15,6 @@ open Names open Constr open Libnames open Globnames -open Nametab open Libobject open Mod_subst @@ -228,14 +227,14 @@ let string_of_class = function | CL_FUN -> "Funclass" | CL_SORT -> "Sortclass" | CL_CONST sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp)) | CL_PROJ sp -> let sp = Projection.Repr.constant sp in - string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (ConstRef sp)) | CL_IND sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (IndRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (IndRef sp)) | CL_SECVAR sp -> - string_of_qualid (shortest_qualid_of_global Id.Set.empty (VarRef sp)) + string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty (VarRef sp)) let pr_class x = str (string_of_class x) @@ -520,7 +519,7 @@ module CoercionPrinting = let compare = GlobRef.Ordered.compare let encode = coercion_of_reference let subst = subst_coe_typ - let printer x = pr_global_env Id.Set.empty x + let printer x = Nametab.pr_global_env Id.Set.empty x let key = ["Printing";"Coercion"] let title = "Explicitly printed coercions: " let member_message x b = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 592057ab41..072ac9deed 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -25,7 +25,6 @@ open Termops open Namegen open Libnames open Globnames -open Nametab open Mod_subst open Decl_kinds open Context.Named.Declaration @@ -58,7 +57,7 @@ let add_name_opt na b t (nenv, env) = (* Tools for printing of Cases *) let encode_inductive r = - let indsp = global_inductive r in + let indsp = Nametab.global_inductive r in let constr_lengths = constructors_nrealargs indsp in (indsp,constr_lengths) @@ -97,7 +96,7 @@ module PrintingInductiveMake = let compare = ind_ord let encode = Test.encode let subst subst obj = subst_ind subst obj - let printer ind = pr_global_env Id.Set.empty (IndRef ind) + let printer ind = Nametab.pr_global_env Id.Set.empty (IndRef ind) let key = ["Printing";Test.field] let title = Test.title let member_message x = Test.member_message (printer x) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index e49ba75b3f..89f64d328a 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -29,7 +29,6 @@ open Inductive open Inductiveops open Environ open Reductionops -open Nametab open Context.Rel.Declaration type dep_flag = bool @@ -618,6 +617,6 @@ let lookup_eliminator ind_sp s = user_err ~hdr:"default_elim" (strbrk "Cannot find the elimination combinator " ++ Id.print id ++ strbrk ", the elimination of the inductive definition " ++ - pr_global_env Id.Set.empty (IndRef ind_sp) ++ + Nametab.pr_global_env Id.Set.empty (IndRef ind_sp) ++ strbrk " on sort " ++ Termops.pr_sort_family s ++ strbrk " is probably not allowed.") diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index f8dc5ba4d6..5d74b59b27 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -20,7 +20,6 @@ open Util open Pp open Names open Globnames -open Nametab open Constr open Libobject open Mod_subst @@ -330,7 +329,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) let error_not_structure ref description = user_err ~hdr:"object_declare" (str"Could not declare a canonical structure " ++ - (Id.print (basename_of_global ref) ++ str"." ++ spc() ++ + (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++ description)) let check_and_decompose_canonical_structure ref = diff --git a/printing/printer.ml b/printing/printer.ml index 990bdaad7d..3cf995a005 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -15,7 +15,6 @@ open Names open Constr open Environ open Globnames -open Nametab open Evd open Refiner open Constrextern @@ -242,7 +241,7 @@ let pr_abstract_cumulativity_info sigma cumi = (**********************************************************************) (* Global references *) -let pr_global_env = pr_global_env +let pr_global_env = Nametab.pr_global_env let pr_global = pr_global_env Id.Set.empty let pr_universe_instance evd inst = diff --git a/test-suite/bugs/closed/bug_8785.v b/test-suite/bugs/closed/bug_8785.v new file mode 100644 index 0000000000..b10569499e --- /dev/null +++ b/test-suite/bugs/closed/bug_8785.v @@ -0,0 +1,44 @@ +Universe u v w. +Inductive invertible {X:Type@{u}} {Y:Type} (f:X->Y) : Prop := . + +Inductive FiniteT : Type -> Prop := + | add_finite: forall T:Type@{v}, FiniteT T -> FiniteT (option T) + | bij_finite: forall (X:Type@{w}) (Y:Type) (f:X->Y), FiniteT X -> + invertible f -> FiniteT Y. + +Set Printing Universes. + +Axiom a : False. +(* +Constraint v <= u. +Constraint v <= w. +*) +Lemma finite_subtype: forall (X:Type) (P:X->Prop), + FiniteT X -> (forall x:X, P x \/ ~ P x) -> + FiniteT {x:X | P x}. +Proof. +intros. +induction H. + +destruct (H0 None). +elim a. + +pose (g := fun (x:{x:T | P (Some x)}) => + match x return {x:option T | P x} with + | exist _ x0 i => exist (fun x:option T => P x) (Some x0) i + end). +apply bij_finite with _ g. +apply IHFiniteT. +intro; apply H0. +elim a. + +pose (g := fun (x:{x:X | P (f x)}) => + match x with + | exist _ x0 i => exist (fun x:Y => P x) (f x0) i + end). +apply bij_finite with _ g. +apply IHFiniteT. +intro; apply H0. +elim a. + +Qed. diff --git a/test-suite/bugs/closed/bug_8794.v b/test-suite/bugs/closed/bug_8794.v new file mode 100644 index 0000000000..5ff0b30260 --- /dev/null +++ b/test-suite/bugs/closed/bug_8794.v @@ -0,0 +1,11 @@ +(* This used to raise an anomaly in 8.8 *) + +Inductive T := Tau (t : T). + +Notation idT t := (match t with Tau t => Tau t end). + +Lemma match_itree : forall (t : T), t = idT t. +Proof. destruct t; auto. Qed. + +Lemma what (k : unit -> T) : k tt = k tt. +Proof. rewrite match_itree. Abort. diff --git a/theories/Strings/ByteVector.v b/theories/Strings/ByteVector.v new file mode 100644 index 0000000000..16f26002d2 --- /dev/null +++ b/theories/Strings/ByteVector.v @@ -0,0 +1,56 @@ +(************************************************************************) +(* * 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) *) +(************************************************************************) + +Require Import Ascii Basics Bvector Psatz String Vector. +Export VectorNotations. +Open Scope program_scope. +Open Scope string_scope. + +Definition ByteVector := Vector.t ascii. + +Definition ByteNil : ByteVector 0 := Vector.nil ascii. + +Definition little_endian_to_string {n : nat} (v : ByteVector n) : string := + fold_right String v "". + +Definition to_string {n : nat} : ByteVector n -> string := + little_endian_to_string ∘ rev. + +Fixpoint little_endian_of_string (s : string) : ByteVector (length s) := + match s with + | "" => ByteNil + | String b s' => b :: little_endian_of_string s' + end. + +Definition of_string (s : string) : ByteVector (length s) := + rev (little_endian_of_string s). + +Fixpoint to_Bvector {n : nat} (v : ByteVector n) : Bvector (n * 8) := + match v with + | [] => [] + | Ascii b0 b1 b2 b3 b4 b5 b6 b7::v' => + b0::b1::b2::b3::b4::b5::b6::b7::to_Bvector v' + end. + +Fixpoint of_Bvector {n : nat} : Bvector (n * 8) -> ByteVector n := + match n with + | 0 => fun _ => [] + | S n' => + fun v => + let (b0, v1) := uncons v in + let (b1, v2) := uncons v1 in + let (b2, v3) := uncons v2 in + let (b3, v4) := uncons v3 in + let (b4, v5) := uncons v4 in + let (b5, v6) := uncons v5 in + let (b6, v7) := uncons v6 in + let (b7, v8) := uncons v7 in + Ascii b0 b1 b2 b3 b4 b5 b6 b7::of_Bvector v8 + end. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index 390ca78c0e..4a2bddf35c 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -132,6 +132,9 @@ replace v (Fin.of_nat_lt H). Definition tl {A} := @caseS _ (fun n v => t A n) (fun h n t => t). Global Arguments tl {A} {n} v. +(** Destruct a non empty vector *) +Definition uncons {A} {n : nat} (v : t A (S n)) : A * t A n := (hd v, tl v). + (** Remove last element of a non-empty vector *) Definition shiftout {A} := @rectS _ (fun n _ => t A n) (fun a => []) (fun h _ _ H => h :: H). diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 15c0278f47..6beac2032d 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -162,27 +162,6 @@ let label_of = function | ConstructRef ((kn,_),_) -> MutInd.label kn | VarRef id -> Label.of_id id -let fold_constr_with_full_binders g f n acc c = - let open Context.Rel.Declaration in - match Constr.kind c with - | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc - | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c - | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c - | App (c,l) -> Array.fold_left (f n) (f n acc c) l - | Proj (p,c) -> f n acc c - | Evar (_,l) -> Array.fold_left (f n) acc l - | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl - | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - let rec traverse current ctx accu t = match Constr.kind t with | Var id -> let body () = id |> Global.lookup_named |> NamedDecl.get_value in @@ -205,10 +184,10 @@ let rec traverse current ctx accu t = match Constr.kind t with traverse_object ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn) | _ -> - fold_constr_with_full_binders + Constr.fold_with_full_binders Context.Rel.add (traverse current) ctx accu t end -| _ -> fold_constr_with_full_binders +| _ -> Constr.fold_with_full_binders Context.Rel.add (traverse current) ctx accu t and traverse_object ?inhabits (curr, data, ax2ty) body obj = diff --git a/vernac/class.ml b/vernac/class.ml index 62efc72f1f..ab43d5c8ff 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -21,7 +21,6 @@ open Environ open Classops open Declare open Globnames -open Nametab open Decl_kinds let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL @@ -310,7 +309,7 @@ let add_coercion_hook poly local ref = | Global -> false in let () = try_add_new_coercion ref ~local poly in - let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in + let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in Flags.if_verbose Feedback.msg_info msg let add_coercion_hook poly = Lemmas.mk_hook (add_coercion_hook poly) diff --git a/vernac/classes.ml b/vernac/classes.ml index ca0387fd1b..84ffb84206 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -12,7 +12,6 @@ module CVars = Vars open Names open EConstr -open Nametab open CErrors open Util open Typeclasses_errors @@ -67,7 +66,7 @@ let intern_info {hint_priority;hint_pattern} = (** TODO: add subinstances *) let existing_instance glob g info = - let c = global g in + let c = Nametab.global g in let info = Option.default Hints.empty_hint_info info in let info = intern_info info in let instance, _ = Typeops.type_of_global_in_context (Global.env ()) c in diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 7b28895814..885a22b209 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -22,7 +22,6 @@ open Nameops open Constrexpr open Constrexpr_ops open Constrintern -open Nametab open Impargs open Reductionops open Indtypes @@ -575,6 +574,6 @@ let do_mutual_inductive ~template udecl indl cum poly prv ~uniform finite = (* Declare the possible notations of inductive types *) List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns; (* Declare the coercions *) - List.iter (fun qid -> Class.try_add_new_coercion (locate qid) ~local:false poly) coes; + List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false poly) coes; (* If positivity is assumed declares itself as unsafe. *) if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else () diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 8d691eb3b2..d8cd429e6e 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -33,7 +33,6 @@ open Globnames open Goptions open Nameops open Termops -open Nametab open Smartlocate open Vernacexpr open Ind_tables @@ -369,7 +368,7 @@ requested | InSet -> recs ^ "_nodep" | InType -> recs ^ "t_nodep") ) in - let newid = add_suffix (basename_of_global (IndRef ind)) suffix in + let newid = add_suffix (Nametab.basename_of_global (IndRef ind)) suffix in let newref = CAst.make newid in ((newref,isdep,ind,z)::l1),l2 in diff --git a/vernac/search.ml b/vernac/search.ml index 23e53ce673..1fac28358a 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -18,7 +18,6 @@ open Environ open Pattern open Libnames open Globnames -open Nametab module NamedDecl = Context.Named.Declaration @@ -192,7 +191,7 @@ let rec head_filter pat ref env sigma typ = | _ -> false let full_name_of_reference ref = - let (dir,id) = repr_path (path_of_global ref) in + let (dir,id) = repr_path (Nametab.path_of_global ref) in DirPath.to_string dir ^ "." ^ Id.to_string id (** Whether a reference is blacklisted *) @@ -204,14 +203,14 @@ let blacklist_filter_aux () = List.for_all is_not_bl l let module_filter (mods, outside) ref env typ = - let sp = path_of_global ref in + let sp = Nametab.path_of_global ref in let sl = dirpath sp in let is_outside md = not (is_dirpath_prefix_of md sl) in let is_inside md = is_dirpath_prefix_of md sl in if outside then List.for_all is_outside mods else List.is_empty mods || List.exists is_inside mods -let name_of_reference ref = Id.to_string (basename_of_global ref) +let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref) let search_about_filter query gr env typ = match query with | GlobSearchSubPattern pat -> |