diff options
60 files changed, 869 insertions, 797 deletions
diff --git a/.gitignore b/.gitignore index 538124b8e5..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 diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index bb1aa81a73..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-22-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/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 41e1d1a937..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-22-V1" +# 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.3.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/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 f89a5dfca0..06281d6287 100644 --- a/ide/wg_Command.ml +++ b/ide/wg_Command.ml @@ -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/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/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/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/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/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/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 = |