aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.github/workflows/ci.yml91
-rw-r--r--README.md8
-rw-r--r--azure-pipelines.yml116
-rwxr-xr-xdev/ci/azure-build.sh1
-rw-r--r--dev/ci/user-overlays/13537-ppedrot-lazy-subst-kernel.sh5
-rw-r--r--doc/sphinx/changes.rst19
-rw-r--r--doc/tools/coqrst/coqdomain.py29
-rw-r--r--interp/constrintern.ml681
-rw-r--r--kernel/cClosure.ml21
-rw-r--r--kernel/esubst.ml309
-rw-r--r--kernel/esubst.mli49
-rw-r--r--kernel/nativelambda.ml2
-rw-r--r--kernel/typeops.ml2
-rw-r--r--kernel/vmlambda.ml2
-rw-r--r--pretyping/cases.ml25
-rw-r--r--pretyping/cases.mli12
-rw-r--r--pretyping/cbv.ml21
-rw-r--r--pretyping/inductiveops.ml8
-rw-r--r--pretyping/inductiveops.mli4
-rw-r--r--test-suite/output/Cases.out52
-rw-r--r--test-suite/output/Cases.v30
-rw-r--r--test-suite/output/RecordFieldErrors.out2
-rw-r--r--test-suite/output/RecordFieldErrors.v2
-rw-r--r--test-suite/success/Case22.v13
-rw-r--r--test-suite/success/Cases.v57
-rw-r--r--vernac/himsg.ml38
26 files changed, 922 insertions, 677 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
new file mode 100644
index 0000000000..f5527192e0
--- /dev/null
+++ b/.github/workflows/ci.yml
@@ -0,0 +1,91 @@
+name: GitHub CI
+
+on: [push, pull_request]
+
+jobs:
+ Windows:
+ runs-on: windows-latest
+
+ steps:
+ - uses: actions/checkout@v2
+
+ - name: Set up Cygwin
+ uses: egor-tensin/setup-cygwin@v1
+ with:
+ packages: rsync patch diffutils make unzip m4 findutils time wget curl git mingw64-x86_64-binutils mingw64-x86_64-gcc-core mingw64-x86_64-gcc-g++ mingw64-x86_64-pkg-config mingw64-x86_64-windows_default_manifest mingw64-x86_64-headers mingw64-x86_64-runtime mingw64-x86_64-pthreads mingw64-x86_64-zlib mingw64-x86_64-gmp python3
+
+ - name: Create home dir
+ run: |
+ C:\tools\cygwin\bin\bash.exe --login -c 'env'
+
+ - name: Install opam
+ run: |
+ C:\tools\cygwin\bin\bash.exe dev\ci\azure-opam.sh
+
+ - name: Build Coq
+ run: |
+ C:\tools\cygwin\bin\bash.exe dev\ci\azure-build.sh
+
+ macOS:
+ runs-on: macOS-10.15
+
+ steps:
+ - uses: actions/checkout@v2
+
+ - name: Install system dependencies
+ run: |
+ brew install gnu-time opam gtksourceview3 adwaita-icon-theme
+ pip3 install macpack
+
+ - name: Install OCaml dependencies
+ run: |
+ export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig
+ opam init -a -j "$NJOBS" --compiler=ocaml-base-compiler.$COMPILER
+ opam switch set ocaml-base-compiler.$COMPILER
+ eval $(opam env)
+ opam update
+ opam install -j "$NJOBS" ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.10
+ opam list
+ env:
+ COMPILER: "4.11.1"
+ FINDLIB_VER: ".1.8.1"
+ OPAMYES: "true"
+ MACOSX_DEPLOYMENT_TARGET: "10.11"
+ NJOBS: "2"
+
+ - name: Build Coq
+ run: |
+ eval $(opam env)
+ ./configure -prefix "$(pwd)/_install_ci" -warn-error yes -native-compiler no -coqide opt
+ make -j "$NJOBS" byte
+ make -j "$NJOBS"
+ env:
+ MACOSX_DEPLOYMENT_TARGET: "10.11"
+ NJOBS: "2"
+
+ - name: Run Coq Test Suite
+ run: |
+ eval $(opam env)
+ export OCAMLPATH=$(pwd):"$OCAMLPATH"
+ make -j "$NJOBS" test-suite PRINT_LOGS=1
+ env:
+ NJOBS: "2"
+
+ - name: Install Coq
+ run: |
+ make install
+
+ - name: Create the dmg bundle
+ run: |
+ eval $(opam env)
+ export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig
+ export OUTDIR="$(pwd)/_install_ci"
+ ./dev/build/osx/make-macos-dmg.sh
+ env:
+ MACOSX_DEPLOYMENT_TARGET: "10.11"
+ NJOBS: "2"
+
+ - uses: actions/upload-artifact@v2
+ with:
+ name: coq-macOS-installer
+ path: _build/*.dmg
diff --git a/README.md b/README.md
index a5be6e22b8..743bcf128a 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,7 @@
# Coq
-[![GitLab][gitlab-badge]][gitlab-link]
-[![Azure Pipelines][azure-badge]][azure-link]
+[![GitLab CI][gitlab-badge]][gitlab-link]
+[![GitHub CI][action-badge]][action-link]
[![Zulip][zulip-badge]][zulip-link]
[![Discourse][discourse-badge]][discourse-link]
[![DOI][doi-badge]][doi-link]
@@ -9,8 +9,8 @@
[gitlab-badge]: https://gitlab.com/coq/coq/badges/master/pipeline.svg
[gitlab-link]: https://gitlab.com/coq/coq/commits/master
-[azure-badge]: https://dev.azure.com/coq/coq/_apis/build/status/coq.coq?branchName=master
-[azure-link]: https://dev.azure.com/coq/coq/_build/latest?definitionId=1?branchName=master
+[action-badge]: https://github.com/coq/coq/workflows/GitHub%20CI/badge.svg?branch=master
+[action-link]: https://github.com/coq/coq/actions?query=workflow:"GitHub%20CI"
[discourse-badge]: https://img.shields.io/badge/Discourse-forum-informational.svg
[discourse-link]: https://coq.discourse.group/
diff --git a/azure-pipelines.yml b/azure-pipelines.yml
deleted file mode 100644
index 11f225bdb6..0000000000
--- a/azure-pipelines.yml
+++ /dev/null
@@ -1,116 +0,0 @@
-
-# NB: image names can be found at
-# https://docs.microsoft.com/en-us/azure/devops/pipelines/agents/hosted
-
-variables:
- NJOBS: "2"
-
-jobs:
-- job: Windows
- pool:
- vmImage: 'vs2017-win2016'
-
- # Equivalent to allow_failure: true
- # continueOnError: true
-
- steps:
- - checkout: self
- fetchDepth: 10
-
- # cygwin package list not checked for minimality
- - script: |
- powershell -Command "(New-Object Net.WebClient).DownloadFile('http://www.cygwin.com/setup-x86_64.exe', 'setup-x86_64.exe')"
- SET CYGROOT=C:\cygwin64
- SET CYGCACHE=%CYGROOT%\var\cache\setup
- setup-x86_64.exe -qnNdO -R %CYGROOT% -l %CYGCACHE% -s %CYGMIRROR% -P rsync -P patch -P diffutils -P make -P unzip -P m4 -P findutils -P time -P wget -P curl -P git -P mingw64-x86_64-binutils,mingw64-x86_64-gcc-core,mingw64-x86_64-gcc-g++,mingw64-x86_64-pkg-config,mingw64-x86_64-windows_default_manifest -P mingw64-x86_64-headers,mingw64-x86_64-runtime,mingw64-x86_64-pthreads,mingw64-x86_64-zlib,mingw64-x86_64-gmp -P python3
-
- SET TARGET_ARCH=x86_64-w64-mingw32
- SET CD_MFMT=%cd:\=/%
- SET RESULT_INSTALLDIR_CFMT=%CD_MFMT:C:/=/cygdrive/c/%
- C:\cygwin64\bin\bash -l %cd%\dev\build\windows\configure_profile.sh
- displayName: 'Install cygwin'
- env:
- CYGMIRROR: "http://mirror.cs.vt.edu/pub/cygwin/cygwin"
-
- - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-opam.sh
- displayName: 'Install opam'
-
- - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-build.sh
- displayName: 'Build Coq'
-
- # We are hitting a bug where Dune is rebuilding Coq to run the
- # test-suite, also it seems to time out, so we just build for now
- #
- # - script: C:\cygwin64\bin\bash -l %cd%\dev\ci\azure-test.sh
- # displayName: 'Test Coq'
-
- - publish: _build/log
- artifact: Dune Build Log
- condition: always()
-
-- job: macOS
- pool:
- vmImage: 'macOS-10.14'
-
- variables:
- MACOSX_DEPLOYMENT_TARGET: '10.11'
-
- steps:
-
- - checkout: self
- fetchDepth: 10
-
- - script: |
- set -e
- brew install gnu-time opam gtksourceview3 adwaita-icon-theme
- pip3 install macpack
- displayName: 'Install system dependencies'
-
- - script: |
- set -e
- export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig
- opam init -a -j "$NJOBS" --compiler=ocaml-base-compiler.$COMPILER
- opam switch set ocaml-base-compiler.$COMPILER
- eval $(opam env)
- opam update
- opam install -j "$NJOBS" ocamlfind${FINDLIB_VER} ounit lablgtk3-sourceview3 zarith.1.10
- opam list
- displayName: 'Install OCaml dependencies'
- env:
- COMPILER: "4.11.1"
- FINDLIB_VER: ".1.8.1"
- OPAMYES: "true"
-
- - script: |
- set -e
-
- eval $(opam env)
- ./configure -prefix '$(Build.BinariesDirectory)' -warn-error yes -native-compiler no -coqide opt
- make -j "$NJOBS" byte
- make -j "$NJOBS"
- displayName: 'Build Coq'
-
- - script: |
- eval $(opam env)
- export OCAMLPATH=$(pwd):"$OCAMLPATH"
- make -j "$NJOBS" test-suite PRINT_LOGS=1
- displayName: 'Run Coq Test Suite'
-
- - script: |
- make install
- displayName: 'Install Coq'
-
- - script: |
- set -e
- eval $(opam env)
- export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig
- ./dev/build/osx/make-macos-dmg.sh
- mv _build/*.dmg "$(Build.ArtifactStagingDirectory)/"
- displayName: 'Create the dmg bundle'
- env:
- OUTDIR: '$(Build.BinariesDirectory)'
-
- - task: PublishBuildArtifacts@1
- inputs:
- pathtoPublish: '$(Build.ArtifactStagingDirectory)'
- artifactName: coq-macOS-installer
diff --git a/dev/ci/azure-build.sh b/dev/ci/azure-build.sh
index 494651c5bf..1b02cd45ed 100755
--- a/dev/ci/azure-build.sh
+++ b/dev/ci/azure-build.sh
@@ -4,4 +4,5 @@ set -e -x
cd $(dirname $0)/../..
+eval $(opam env)
dune build coq.install coqide-server.install
diff --git a/dev/ci/user-overlays/13537-ppedrot-lazy-subst-kernel.sh b/dev/ci/user-overlays/13537-ppedrot-lazy-subst-kernel.sh
new file mode 100644
index 0000000000..aa686ea619
--- /dev/null
+++ b/dev/ci/user-overlays/13537-ppedrot-lazy-subst-kernel.sh
@@ -0,0 +1,5 @@
+if [ "$CI_PULL_REQUEST" = "13537" ] || [ "$CI_BRANCH" = "lazy-subst-kernel" ]; then
+
+ overlay mtac2 https://github.com/ppedrot/Mtac2 lazy-subst-kernel
+
+fi
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 8fb03879e8..726a6309d4 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -2017,6 +2017,25 @@ Changes in 8.12.1
fixes `#12332 <https://github.com/coq/coq/issues/12332>`_,
by Théo Zimmermann and Jim Fehrle).
+Changes in 8.12.2
+~~~~~~~~~~~~~~~~~
+
+**Notations**
+
+- **Fixed:**
+ 8.12 regression causing notations mentioning a coercion to be ignored
+ (`#13436 <https://github.com/coq/coq/pull/13436>`_,
+ fixes `#13432 <https://github.com/coq/coq/issues/13432>`_,
+ by Hugo Herbelin).
+
+**Tactics**
+
+- **Fixed:**
+ 8.12 regression: incomplete inference of implicit arguments in :tacn:`exists`
+ (`#13468 <https://github.com/coq/coq/pull/13468>`_,
+ fixes `#13456 <https://github.com/coq/coq/issues/13456>`_,
+ by Hugo Herbelin).
+
Version 8.11
------------
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 56464851ba..8f642df8fd 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -99,6 +99,11 @@ def make_math_node(latex, docname, nowrap):
node['number'] = None
return node
+# To support any character in tacn, ... names.
+# see https://github.com/coq/coq/pull/13564
+def make_id(tag):
+ return tag.replace(" ", "-")
+
class CoqObject(ObjectDescription):
"""A generic Coq object for Sphinx; all Coq objects are subclasses of this.
@@ -200,7 +205,7 @@ class CoqObject(ObjectDescription):
names_in_subdomain[name] = (self.env.docname, self.objtype, target_id)
def _target_id(self, name):
- return make_target(self.objtype, nodes.make_id(name))
+ return make_target(self.objtype, make_id(name))
def _add_target(self, signode, name):
"""Register a link target ‘name’, pointing to signode."""
@@ -210,6 +215,16 @@ class CoqObject(ObjectDescription):
signode['names'].append(name)
signode['first'] = (not self.names)
self._record_name(name, targetid, signode)
+ else:
+ # todo: make the following a real error or warning
+ # todo: then maybe the above "if" is not needed
+ names_in_subdomain = self.subdomain_data()
+ if name in names_in_subdomain:
+ try:
+ print("Duplicate", self.subdomain, "name: ", name)
+ except UnicodeEncodeError: # in CI
+ print("*** UnicodeEncodeError")
+ # self._warn_if_duplicate_name(names_in_subdomain, name, signode)
return targetid
def _add_index_entry(self, name, target):
@@ -322,7 +337,7 @@ class VernacObject(NotationObject):
annotation = "Command"
def _name_from_signature(self, signature):
- m = re.match(r"[a-zA-Z ]+", signature)
+ m = re.match(r"[a-zA-Z0-9_ ]+", signature)
return m.group(0).strip() if m else None
class VernacVariantObject(VernacObject):
@@ -505,7 +520,7 @@ class ProductionObject(CoqObject):
pass
def _target_id(self, name):
- return 'grammar-token-{}'.format(nodes.make_id(name[1]))
+ return make_id('grammar-token-{}'.format(name[1]))
def _record_name(self, name, targetid, signode):
env = self.state.document.settings.env
@@ -533,7 +548,7 @@ class ProductionObject(CoqObject):
row = nodes.container(classes=['prodn-row'])
entry = nodes.container(classes=['prodn-cell-nonterminal'])
if lhs != "":
- target_name = 'grammar-token-' + nodes.make_id(lhs)
+ target_name = make_id('grammar-token-' + lhs)
target = nodes.target('', '', ids=[target_name], names=[target_name])
# putting prodn-target on the target node won't appear in the tex file
inline = nodes.inline(classes=['prodn-target'])
@@ -862,7 +877,7 @@ class InferenceDirective(Directive):
docname = self.state.document.settings.env.docname
math_node = make_math_node(latex, docname, nowrap=False)
- tid = nodes.make_id(title)
+ tid = make_id(title)
target = nodes.target('', '', ids=['inference-' + tid])
self.state.document.note_explicit_target(target)
@@ -1182,7 +1197,7 @@ def GrammarProductionRole(typ, rawtext, text, lineno, inliner, options={}, conte
"""
#pylint: disable=dangerous-default-value, unused-argument
env = inliner.document.settings.env
- targetid = nodes.make_id('grammar-token-{}'.format(text))
+ targetid = make_id('grammar-token-{}'.format(text))
target = nodes.target('', '', ids=[targetid])
inliner.document.note_explicit_target(target)
code = nodes.literal(rawtext, text, role=typ.lower())
@@ -1221,7 +1236,7 @@ def GlossaryDefRole(typ, rawtext, text, lineno, inliner, options={}, content=[])
msg = MSG.format(term, env.doc2path(std[key][0]))
inliner.document.reporter.warning(msg, line=lineno)
- targetid = nodes.make_id('term-{}'.format(term))
+ targetid = make_id('term-{}'.format(term))
std[key] = (env.docname, targetid)
target = nodes.target('', '', ids=[targetid], names=[term])
inliner.document.note_explicit_target(target)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index cf2f333596..e3a4d1b169 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -90,18 +90,6 @@ let for_grammar f x =
a
(**********************************************************************)
-(* Locating reference, possibly via an abbreviation *)
-
-let locate_reference qid =
- Smartlocate.global_of_extended_global (Nametab.locate_extended qid)
-
-let is_global id =
- try
- let _ = locate_reference (qualid_of_ident id) in true
- with Not_found ->
- false
-
-(**********************************************************************)
(* Internalization errors *)
type internalization_error =
@@ -112,8 +100,7 @@ type internalization_error =
| NonLinearPattern of Id.t
| BadPatternsNumber of int * int
| NotAProjection of qualid
- | NotAProjectionOf of qualid * qualid
- | ProjectionsOfDifferentRecords of qualid * qualid
+ | ProjectionsOfDifferentRecords of Recordops.struc_typ * Recordops.struc_typ
exception InternalizationError of internalization_error
@@ -139,13 +126,16 @@ let explain_bad_patterns_number n1 n2 =
str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++
str " but found " ++ int n2
+let inductive_of_record record =
+ let inductive = GlobRef.IndRef (inductive_of_constructor record.Recordops.s_CONST) in
+ Nametab.shortest_qualid_of_global Id.Set.empty inductive
+
let explain_field_not_a_projection field_id =
pr_qualid field_id ++ str ": Not a projection"
-let explain_field_not_a_projection_of field_id inductive_id =
- pr_qualid field_id ++ str ": Not a projection of inductive " ++ pr_qualid inductive_id
-
-let explain_projections_of_diff_records inductive1_id inductive2_id =
+let explain_projections_of_diff_records record1 record2 =
+ let inductive1_id = inductive_of_record record1 in
+ let inductive2_id = inductive_of_record record2 in
str "This record contains fields of both " ++ pr_qualid inductive1_id ++
str " and " ++ pr_qualid inductive2_id
@@ -158,8 +148,6 @@ let explain_internalization_error e =
| NonLinearPattern id -> explain_non_linear_pattern id
| BadPatternsNumber (n1,n2) -> explain_bad_patterns_number n1 n2
| NotAProjection field_id -> explain_field_not_a_projection field_id
- | NotAProjectionOf (field_id, inductive_id) ->
- explain_field_not_a_projection_of field_id inductive_id
| ProjectionsOfDifferentRecords (inductive1_id, inductive2_id) ->
explain_projections_of_diff_records inductive1_id inductive2_id
in pp ++ str "."
@@ -277,9 +265,9 @@ type pattern_intern_env = {
(* Remembering the parsing scope of variables in notations *)
let make_current_scope tmp scopes = match tmp, scopes with
-| Some tmp_scope, (sc :: _) when String.equal sc tmp_scope -> scopes
-| Some tmp_scope, scopes -> tmp_scope :: scopes
-| None, scopes -> scopes
+ | Some tmp_scope, (sc :: _) when String.equal sc tmp_scope -> scopes
+ | Some tmp_scope, scopes -> tmp_scope :: scopes
+ | None, scopes -> scopes
let pr_scope_stack = function
| [] -> str "the empty scope stack"
@@ -736,9 +724,9 @@ let set_type ty1 ty2 =
user_err ?loc:t2.CAst.loc Pp.(str "Unexpected type constraint in notation already providing a type constraint.")
let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renaming,env) na ty =
- match na with
- | Anonymous -> (renaming,env), None, Anonymous, Explicit, set_type ty None
- | Name id ->
+ match na with
+ | Anonymous -> (renaming,env), None, Anonymous, Explicit, set_type ty None
+ | Name id ->
let store,get = set_temporary_memory () in
let test_kind = test_kind_tolerant in
try
@@ -778,10 +766,10 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam
(renaming',env), None, Name id', Explicit, set_type ty None
type binder_action =
-| AddLetIn of lname * constr_expr * constr_expr option
-| AddTermIter of (constr_expr * subscopes) Names.Id.Map.t
-| AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *)
-| AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *)
+ | AddLetIn of lname * constr_expr * constr_expr option
+ | AddTermIter of (constr_expr * subscopes) Names.Id.Map.t
+ | AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *)
+ | AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *)
let dmap_with_loc f n =
CAst.map_with_loc (fun ?loc c -> f ?loc (DAst.get_thunk c)) n
@@ -1063,35 +1051,35 @@ let string_of_ty = function
| Variable -> "var"
let gvar (loc, id) us = match us with
-| None | Some [] -> DAst.make ?loc @@ GVar id
-| Some _ ->
- user_err ?loc (str "Variable " ++ Id.print id ++
- str " cannot have a universe instance")
+ | None | Some [] -> DAst.make ?loc @@ GVar id
+ | Some _ ->
+ user_err ?loc (str "Variable " ++ Id.print id ++
+ str " cannot have a universe instance")
let intern_var env (ltacvars,ntnvars) namedctx loc id us =
(* Is [id] a notation variable *)
if Id.Map.mem id ntnvars then
begin
if not (Id.Map.mem id env.impls) then set_var_scope ?loc id true (env.tmp_scope,env.scopes) ntnvars;
- gvar (loc,id) us, [], []
+ gvar (loc,id) us
end
else
(* Is [id] registered with implicit arguments *)
try
- let ty,impls,argsc,uid = Id.Map.find id env.impls in
+ let ty,_,_,uid = Id.Map.find id env.impls in
let tys = string_of_ty ty in
Dumpglob.dump_reference ?loc "<>" uid tys;
- gvar (loc,id) us, make_implicits_list impls, argsc
+ gvar (loc,id) us
with Not_found ->
(* Is [id] bound in current term or is an ltac var bound to constr *)
if Id.Set.mem id env.ids || Id.Set.mem id ltacvars.ltac_vars
then
- gvar (loc,id) us, [], []
+ gvar (loc,id) us
else if Id.equal id ldots_var
(* Is [id] the special variable for recursive notations? *)
then if Id.Map.is_empty ntnvars
then error_ldots_var ?loc
- else gvar (loc,id) us, [], []
+ else gvar (loc,id) us
else if Id.Set.mem id ltacvars.ltac_bound then
(* Is [id] bound to a free name in ltac (this is an ltac error message) *)
user_err ?loc ~hdr:"intern_var"
@@ -1103,32 +1091,73 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us =
(* [id] a section variable *)
(* Redundant: could be done in intern_qualid *)
let ref = GlobRef.VarRef id in
- let impls = implicits_of_global ref in
- let scopes = find_arguments_scope ref in
Dumpglob.dump_secvar ?loc id; (* this raises Not_found when not a section variable *)
(* Someday we should stop relying on Dumglob raising exceptions *)
- DAst.make ?loc @@ GRef (ref, us), impls, scopes
+ DAst.make ?loc @@ GRef (ref, us)
with e when CErrors.noncritical e ->
(* [id] a goal variable *)
- gvar (loc,id) us, [], []
+ gvar (loc,id) us
+
+(**********************************************************************)
+(* Locating reference, possibly via an abbreviation *)
+
+let locate_reference qid =
+ Smartlocate.global_of_extended_global (Nametab.locate_extended qid)
+
+let is_global id =
+ try
+ let _ = locate_reference (qualid_of_ident id) in true
+ with Not_found ->
+ false
-let find_appl_head_data c =
+let dump_extended_global loc = function
+ | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob ?loc ref
+ | SynDef sp -> Dumpglob.add_glob_kn ?loc sp
+
+let intern_extended_global_of_qualid qid =
+ let r = Nametab.locate_extended qid in dump_extended_global qid.CAst.loc r; r
+
+let intern_reference qid =
+ let r =
+ try intern_extended_global_of_qualid qid
+ with Not_found as exn ->
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info qid
+ in
+ Smartlocate.global_of_extended_global r
+
+let intern_projection qid =
+ try
+ let gr = Smartlocate.global_of_extended_global (intern_extended_global_of_qualid qid) in
+ (gr, Recordops.find_projection gr)
+ with Not_found ->
+ Loc.raise ?loc:qid.loc (InternalizationError (NotAProjection qid))
+
+(**********************************************************************)
+(* Interpreting references *)
+
+let find_appl_head_data env (_,ntnvars) c =
match DAst.get c with
+ | GVar id when not (Id.Map.mem id ntnvars) ->
+ (try
+ let _,impls,argsc,_ = Id.Map.find id env.impls in
+ make_implicits_list impls, argsc
+ with Not_found -> [], [])
| GRef (ref,_) ->
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
- c, impls, scopes
+ impls, scopes
| GApp (r, l) ->
begin match DAst.get r with
| GRef (ref,_) ->
let n = List.length l in
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
- c, (if n = 0 then [] else List.map (drop_first_implicits n) impls),
- List.skipn_at_least n scopes
- | _ -> c,[],[]
+ (if n = 0 then [] else List.map (drop_first_implicits n) impls),
+ List.skipn_at_least n scopes
+ | _ -> [],[]
end
- | _ -> c,[],[]
+ | _ -> [],[]
let error_not_enough_arguments ?loc =
user_err ?loc (str "Abbreviation is not applied enough.")
@@ -1142,22 +1171,6 @@ let check_no_explicitation l =
| (_, Some {loc}) :: _ ->
user_err ?loc (str"Unexpected explicitation of the argument of an abbreviation.")
-let dump_extended_global loc = function
- | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob ?loc ref
- | SynDef sp -> Dumpglob.add_glob_kn ?loc sp
-
-let intern_extended_global_of_qualid qid =
- let r = Nametab.locate_extended qid in dump_extended_global qid.CAst.loc r; r
-
-let intern_reference qid =
- let r =
- try intern_extended_global_of_qualid qid
- with Not_found as exn ->
- let _, info = Exninfo.capture exn in
- Nametab.error_global_not_found ~info qid
- in
- Smartlocate.global_of_extended_global r
-
let glob_sort_of_level (level: glob_level) : glob_sort =
match level with
| UAnonymous {rigid} -> UAnonymous {rigid}
@@ -1230,6 +1243,37 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
in
c, None, args2
+let intern_qualid_for_pattern test_global intern_not qid pats =
+ match intern_extended_global_of_qualid qid with
+ | TrueGlobal g ->
+ test_global g;
+ (g, false, Some [], pats)
+ | SynDef kn ->
+ let filter (vars,a) =
+ match a with
+ | NRef g ->
+ (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
+ test_global g;
+ let () = assert (List.is_empty vars) in
+ Some (g, Some [], pats)
+ | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *)
+ test_global g;
+ let () = assert (List.is_empty vars) in
+ Some (g, None, pats)
+ | NApp (NRef g,args) ->
+ (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
+ test_global g;
+ let nvars = List.length vars in
+ if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc;
+ let pats1,pats2 = List.chop nvars pats in
+ let subst = split_by_type_pat vars (pats1,[]) in
+ let args = List.map (intern_not subst) args in
+ Some (g, Some args, pats2)
+ | _ -> None in
+ match Syntax_def.search_filtered_syntactic_definition filter kn with
+ | Some (g, pats1, pats2) -> (g, true, pats1, pats2)
+ | None -> raise Not_found
+
let warn_nonprimitive_projection =
CWarnings.create ~name:"nonprimitive-projection-syntax" ~category:"syntax" ~default:CWarnings.Disabled
Pp.(fun f -> pr_qualid f ++ str " used as a primitive projection but is not one.")
@@ -1256,35 +1300,34 @@ let intern_applied_reference ~isproj intern env namedctx (_, ntnvars as lvar) us
let loc = qid.CAst.loc in
let us = intern_instance ~local_univs:env.local_univs us in
if qualid_is_ident qid then
- try
- let res = intern_var env lvar namedctx loc (qualid_basename qid) us in
- check_applied_projection isproj None qid;
- res, args
- with Not_found ->
- try
- let r, realref, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
- check_applied_projection isproj realref qid;
- find_appl_head_data r, args2
- with Not_found as exn ->
- (* Extra allowance for non globalizing functions *)
- if !interning_grammar || env.unb then
- (* check_applied_projection ?? *)
- (gvar (loc,qualid_basename qid) us, [], []), args
- else
- let _, info = Exninfo.capture exn in
- Nametab.error_global_not_found ~info qid
+ try
+ let res = intern_var env lvar namedctx loc (qualid_basename qid) us in
+ check_applied_projection isproj None qid;
+ res, args
+ with Not_found ->
+ try
+ let res, realref, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in
+ check_applied_projection isproj realref qid;
+ res, args2
+ with Not_found as exn ->
+ (* Extra allowance for non globalizing functions *)
+ if !interning_grammar || env.unb then
+ (* check_applied_projection ?? *)
+ gvar (loc,qualid_basename qid) us, args
+ else
+ let _, info = Exninfo.capture exn in
+ Nametab.error_global_not_found ~info qid
else
- let r,realref,args2 =
- try intern_qualid qid intern env ntnvars us args
- with Not_found as exn ->
+ try
+ let res, realref, args2 = intern_qualid qid intern env ntnvars us args in
+ check_applied_projection isproj realref qid;
+ res, args2
+ with Not_found as exn ->
let _, info = Exninfo.capture exn in
Nametab.error_global_not_found ~info qid
- in
- check_applied_projection isproj realref qid;
- find_appl_head_data r, args2
let interp_reference vars r =
- let (r,_,_),_ =
+ let r,_ =
intern_applied_reference ~isproj:None (fun _ -> error_not_enough_arguments ?loc:None)
{ids = Id.Set.empty; unb = false;
local_univs = { bound=Id.Map.empty; unb_univs = false };(* <- doesn't matter here *)
@@ -1297,17 +1340,18 @@ let interp_reference vars r =
(**********************************************************************)
(** {5 Cases } *)
-(** Private internalization patterns *)
+(** Intermediate type common to the patterns of the "in" and of the
+ "with" clause of "match" *)
+
type 'a raw_cases_pattern_expr_r =
| RCPatAlias of 'a raw_cases_pattern_expr * lname
- | RCPatCstr of GlobRef.t
- * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
- (** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *)
+ | RCPatCstr of GlobRef.t * 'a raw_cases_pattern_expr list
| RCPatAtom of (lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
| RCPatOr of 'a raw_cases_pattern_expr list
and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t
(** {6 Elementary bricks } *)
+
let apply_scope_env env = function
| [] -> {env with tmp_scope = None}, []
| sc::scl -> {env with tmp_scope = sc}, scl
@@ -1320,22 +1364,19 @@ let rec simple_adjust_scopes n scopes =
| [] -> None :: simple_adjust_scopes (n-1) []
| sc::scopes -> sc :: simple_adjust_scopes (n-1) scopes
-let find_remaining_scopes pl1 pl2 ref =
- let impls_st = implicits_of_global ref in
- let len_pl1 = List.length pl1 in
- let len_pl2 = List.length pl2 in
- let impl_list = if Int.equal len_pl1 0
- then select_impargs_size len_pl2 impls_st
- else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in
- let allscs = find_arguments_scope ref in
- let scope_list = List.skipn_at_least len_pl1 allscs in
- let rec aux = function
- |[],l -> l
- |_,[] -> []
- |h::t,_::tt when is_status_implicit h -> aux (t,tt)
- |_::t,h::tt -> h :: aux (t,tt)
- in ((try List.firstn len_pl1 allscs with Failure _ -> simple_adjust_scopes len_pl1 allscs),
- simple_adjust_scopes len_pl2 (aux (impl_list,scope_list)))
+let rec adjust_to_up l l' default =
+ match l, l' with
+ | l, [] -> []
+ | [], l -> l
+ | true::l, l' -> default :: adjust_to_up l l' default
+ | false::l, y::l' -> y :: adjust_to_up l l' default
+
+let rec adjust_to_down l l' default =
+ match l, l' with
+ | [], l -> []
+ | true::l, l' -> adjust_to_down l l' default
+ | false::l, [] -> default :: adjust_to_down l [] default
+ | false::l, y::l' -> y :: adjust_to_down l l' default
(* @return the first variable that occurs twice in a pattern
@@ -1378,85 +1419,16 @@ let check_or_pat_variables loc ids idsl =
Id.print (List.hd ids'').v ++ strbrk " is not bound in all patterns).")
| [] -> ()
-(** Use only when params were NOT asked to the user.
- @return if letin are included *)
-let check_constructor_length env loc cstr len_pl pl0 =
- let n = len_pl + List.length pl0 in
- if Int.equal n (Inductiveops.constructor_nallargs env cstr) then false else
- (Int.equal n (Inductiveops.constructor_nalldecls env cstr) ||
- (error_wrong_numarg_constructor ?loc env cstr
- (Inductiveops.constructor_nrealargs env cstr)))
-
-open Declarations
-
-(* Similar to Cases.adjust_local_defs but on RCPat *)
-let insert_local_defs_in_pattern (ind,j) l =
- let (mib,mip) = Global.lookup_inductive ind in
- if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then
- (* Optimisation *) l
- else
- let (ctx, _) = mip.mind_nf_lc.(j-1) in
- let decls = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in
- let rec aux decls args =
- match decls, args with
- | Context.Rel.Declaration.LocalDef _ :: decls, args -> (DAst.make @@ RCPatAtom None) :: aux decls args
- | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *)
- | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args
- | _ -> assert false in
- aux decls l
-
-let add_local_defs_and_check_length loc env g pl args =
- let open GlobRef in
- match g with
- | ConstructRef cstr ->
- (* We consider that no variables corresponding to local binders
- have been given in the "explicit" arguments, which come from a
- "@C args" notation or from a custom user notation *)
- let pl' = insert_local_defs_in_pattern cstr pl in
- let maxargs = Inductiveops.constructor_nalldecls env cstr in
- if List.length pl' + List.length args > maxargs then
- error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr);
- (* Two possibilities: either the args are given with explicit
- variables for local definitions, then we give the explicit args
- extended with local defs, so that there is nothing more to be
- added later on; or the args are not enough to have all arguments,
- which a priori means local defs to add in the [args] part, so we
- postpone the insertion of local defs in the explicit args *)
- (* Note: further checks done later by check_constructor_length *)
- if List.length pl' + List.length args = maxargs then pl' else pl
- | _ -> pl
-
-let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 =
- let impl_list = if Int.equal len_pl1 0
- then select_impargs_size (List.length pl2) impls_st
- else List.skipn_at_least len_pl1 (select_stronger_impargs impls_st) in
- let remaining_args = List.fold_left (fun i x -> if is_status_implicit x then i else succ i) in
- let rec aux i = function
- |[],l -> let args_len = List.length l + List.length impl_list + len_pl1 in
- ((if Int.equal args_len nargs then false
- else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
- ,l)
- |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp
- then let (b,out) = aux i (q,[]) in (b,(DAst.make @@ RCPatAtom None)::out)
- else fail (remaining_args (len_pl1+i) il)
- |imp::q,(hh::tt as l) -> if is_status_implicit imp
- then let (b,out) = aux i (q,l) in (b,(DAst.make @@ RCPatAtom None)::out)
- else let (b,out) = aux (succ i) (q,tt) in (b,hh::out)
- in aux 0 (impl_list,pl2)
-
-let add_implicits_check_constructor_length env loc c len_pl1 pl2 =
- let nargs = Inductiveops.constructor_nallargs env c in
- let nargs' = Inductiveops.constructor_nalldecls env c in
- let impls_st = implicits_of_global (GlobRef.ConstructRef c) in
- add_implicits_check_length (error_wrong_numarg_constructor ?loc env c)
- nargs nargs' impls_st len_pl1 pl2
-
-let add_implicits_check_ind_length env loc c len_pl1 pl2 =
- let nallargs = inductive_nallargs env c in
- let nalldecls = inductive_nalldecls env c in
- let impls_st = implicits_of_global (GlobRef.IndRef c) in
- add_implicits_check_length (error_wrong_numarg_inductive ?loc env c)
- nallargs nalldecls impls_st len_pl1 pl2
+let check_has_letin ?loc g expanded nargs nimps tags =
+ let expected_ndecls = List.length tags - nimps in
+ let expected_nassums = List.count (fun x -> not x) tags - nimps in
+ if nargs = expected_nassums then false
+ else if nargs = expected_ndecls then true else
+ let env = Global.env() in
+ match g with
+ | GlobRef.ConstructRef cstr -> error_wrong_numarg_constructor ?loc env ~cstr ~expanded ~nargs ~expected_nassums ~expected_ndecls
+ | GlobRef.IndRef ind -> error_wrong_numarg_inductive ?loc env ~ind ~expanded ~nargs ~expected_nassums ~expected_ndecls
+ | _ -> assert false
(** Do not raise NotEnoughArguments thanks to preconditions*)
let chop_params_pattern loc ind args with_letin =
@@ -1470,9 +1442,9 @@ let chop_params_pattern loc ind args with_letin =
| PatVar _ | PatCstr(_,_,_) -> error_parameter_not_implicit ?loc:c.CAst.loc) params;
args
-let find_constructor loc add_params ref =
+let find_constructor_head ?loc ref =
let open GlobRef in
- let (ind,_ as cstr) = match ref with
+ match ref with
| ConstructRef cstr -> cstr
| IndRef _ ->
let error = str "There is an inductive name deep in a \"in\" clause." in
@@ -1480,17 +1452,12 @@ let find_constructor loc add_params ref =
| ConstRef _ | VarRef _ ->
let error = str "This reference is not a constructor." in
user_err ?loc ~hdr:"find_constructor" error
- in
- cstr, match add_params with
- | Some nb_args ->
- let env = Global.env () in
- let nb =
- if Int.equal nb_args (Inductiveops.constructor_nrealdecls env cstr)
- then Inductiveops.inductive_nparamdecls env ind
- else Inductiveops.inductive_nparams env ind
- in
- List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)])
- | None -> []
+
+let find_inductive_head ?loc ref =
+ let open GlobRef in
+ match ref with
+ | IndRef ind -> ind
+ | _ -> error_bad_inductive_type ?loc ()
let find_pattern_variable qid =
if qualid_is_ident qid then qualid_basename qid
@@ -1505,10 +1472,6 @@ let check_duplicate ?loc fields =
user_err ?loc (str "This record defines several times the field " ++
pr_qualid r ++ str ".")
-let inductive_of_record loc record =
- let inductive = GlobRef.IndRef (inductive_of_constructor record.Recordops.s_CONST) in
- Nametab.shortest_qualid_of_global ?loc Id.Set.empty inductive
-
(** [sort_fields ~complete loc fields completer] expects a list
[fields] of field assignments [f = e1; g = e2; ...], where [f, g]
are fields of a record and [e1] are "values" (either terms, when
@@ -1526,16 +1489,7 @@ let sort_fields ~complete loc fields completer =
match fields with
| [] -> None
| (first_field_ref, _):: _ ->
- let (first_field_glob_ref, record) =
- try
- let gr = locate_reference first_field_ref in
- Dumpglob.add_glob ?loc:first_field_ref.CAst.loc gr;
- (gr, Recordops.find_projection gr)
- with Not_found as exn ->
- let _, info = Exninfo.capture exn in
- let info = Option.cata (Loc.add_loc info) info loc in
- Exninfo.iraise (InternalizationError(NotAProjection first_field_ref), info)
- in
+ let (first_field_glob_ref, record) = intern_projection first_field_ref in
(* the number of parameters *)
let nparams = record.Recordops.s_EXPECTEDPARAM in
(* the reference constructor of the record *)
@@ -1554,25 +1508,14 @@ let sort_fields ~complete loc fields completer =
let rec index_fields fields remaining_projs acc =
match fields with
| (field_ref, field_value) :: fields ->
- let field_glob_ref = try locate_reference field_ref
- with Not_found ->
- user_err ?loc:field_ref.CAst.loc ~hdr:"intern"
- (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in
+ let field_glob_ref,this_field_record = intern_projection field_ref in
let remaining_projs, (field_index, _, regular) =
let the_proj = function
| (idx, Some glob_id, _) -> GlobRef.equal field_glob_ref (GlobRef.ConstRef glob_id)
| (idx, None, _) -> false in
try CList.extract_first the_proj remaining_projs
with Not_found ->
- let floc = field_ref.CAst.loc in
- let this_field_record =
- try Recordops.find_projection field_glob_ref
- with Not_found ->
- let inductive_ref = inductive_of_record floc record in
- Loc.raise ?loc:floc (InternalizationError(NotAProjectionOf (field_ref, inductive_ref))) in
- let ind1 = inductive_of_record floc record in
- let ind2 = inductive_of_record floc this_field_record in
- Loc.raise ?loc (InternalizationError(ProjectionsOfDifferentRecords (ind1, ind2)))
+ Loc.raise ?loc (InternalizationError(ProjectionsOfDifferentRecords (record, this_field_record)))
in
if not regular && complete then
(* "regular" is false when the field is defined
@@ -1625,8 +1568,8 @@ let merge_aliases aliases {loc;v=na} =
{ alias_ids; alias_map; }
let alias_of als = match als.alias_ids with
-| [] -> Anonymous
-| {v=id} :: _ -> Name id
+ | [] -> Anonymous
+ | {v=id} :: _ -> Name id
(** {6 Expanding notations }
@@ -1652,29 +1595,33 @@ let product_of_cases_patterns aliases idspl =
let rec subst_pat_iterator y t = DAst.(map (function
| RCPatAtom id as p ->
begin match id with Some ({v=x},_) when Id.equal x y -> DAst.get t | _ -> p end
- | RCPatCstr (id,l1,l2) ->
- RCPatCstr (id,List.map (subst_pat_iterator y t) l1,
- List.map (subst_pat_iterator y t) l2)
+ | RCPatCstr (id,l) ->
+ RCPatCstr (id,List.map (subst_pat_iterator y t) l)
| RCPatAlias (p,a) -> RCPatAlias (subst_pat_iterator y t p,a)
| RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl)))
let is_non_zero c = match c with
-| { CAst.v = CPrim (Number p) } -> not (NumTok.Signed.is_zero p)
-| _ -> false
+ | { CAst.v = CPrim (Number p) } -> not (NumTok.Signed.is_zero p)
+ | _ -> false
let is_non_zero_pat c = match c with
-| { CAst.v = CPatPrim (Number p) } -> not (NumTok.Signed.is_zero p)
-| _ -> false
+ | { CAst.v = CPatPrim (Number p) } -> not (NumTok.Signed.is_zero p)
+ | _ -> false
let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref
~depr:false
~key:["Asymmetric";"Patterns"]
~value:false
+type global_reference_test = {
+ for_ind : bool;
+ test_kind : ?loc:Loc.t -> GlobRef.t -> unit
+}
+
let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
(* At toplevel, Constructors and Inductives are accepted, in recursive calls
only constructor are allowed *)
- let ensure_kind test_kind ?loc g =
+ let ensure_kind {test_kind} ?loc g =
try test_kind ?loc g
with Not_found ->
error_invalid_pattern_notation ?loc ()
@@ -1682,60 +1629,47 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
(* [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
let rec rcp_of_glob scopes x = DAst.(map (function
| GVar id -> RCPatAtom (Some (CAst.make ?loc:x.loc id,scopes))
- | GHole (_,_,_) -> RCPatAtom (None)
- | GRef (g,_) -> RCPatCstr (g,[],[])
+ | GHole (_,_,_) -> RCPatAtom None
+ | GRef (g,_) -> RCPatCstr (g, [])
| GApp (r, l) ->
begin match DAst.get r with
| GRef (g,_) ->
let allscs = find_arguments_scope g in
- let allscs = simple_adjust_scopes (List.length l) allscs in (* TO CHECK *)
- RCPatCstr (g, List.map2 (fun sc a -> rcp_of_glob (sc,snd scopes) a) allscs l,[])
+ let allscs = simple_adjust_scopes (List.length l) allscs in
+ RCPatCstr (g, List.map2 (fun sc a -> rcp_of_glob (sc,snd scopes) a) allscs l)
| _ ->
CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr.")
end
| _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x
in
- let rec drop_syndef test_kind ?loc scopes qid pats =
+ let make_pars ?loc g =
+ let env = Global.env () in
+ let n = match g with
+ | GlobRef.ConstructRef (ind,_) -> Inductiveops.inductive_nparams env ind
+ | _ -> 0 in
+ List.make n (DAst.make ?loc @@ RCPatAtom None)
+ in
+ let rec drop_syndef {test_kind} ?loc scopes qid add_par_if_no_ntn_with_par no_impl pats =
try
- if qualid_is_ident qid && Option.cata (Id.Set.mem (qualid_basename qid)) false env.pat_ids then
+ if qualid_is_ident qid && Option.cata (Id.Set.mem (qualid_basename qid)) false env.pat_ids && List.is_empty pats then
raise Not_found;
- match Nametab.locate_extended qid with
- | SynDef sp ->
- let filter (vars,a) =
- try match a with
- | NRef g ->
- (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
- test_kind ?loc g;
- let () = assert (List.is_empty vars) in
- let (_,argscs) = find_remaining_scopes [] pats g in
- Some (g, [], List.map2 (in_pat_sc scopes) argscs pats)
- | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr deactivates implicit arguments *)
- test_kind ?loc g;
- let () = assert (List.is_empty vars) in
- let (_,argscs) = find_remaining_scopes [] pats g in
- Some (g, List.map2 (in_pat_sc scopes) argscs pats, [])
- | NApp (NRef g,args) ->
- (* Convention: do not deactivate implicit arguments and scopes for further arguments *)
- test_kind ?loc g;
- let nvars = List.length vars in
- if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc;
- let pats1,pats2 = List.chop nvars pats in
- let subst = split_by_type_pat vars (pats1,[]) in
- let idspl1 = List.map (in_not test_kind_inner qid.loc scopes subst []) args in
- let (_,argscs) = find_remaining_scopes pats1 pats2 g in
- Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2)
- | _ -> raise Not_found
- with Not_found -> None in
- Syntax_def.search_filtered_syntactic_definition filter sp
- | TrueGlobal g ->
- test_kind ?loc g;
- Dumpglob.add_glob ?loc:qid.loc g;
- let (_,argscs) = find_remaining_scopes [] pats g in
- Some (g,[],List.map2 (in_pat_sc scopes) argscs pats)
+ let intern_not subst pat = in_not test_kind_inner qid.loc scopes subst [] pat in
+ let g, expanded, ntnpats, pats = intern_qualid_for_pattern (test_kind ?loc) intern_not qid pats in
+ match ntnpats with
+ | None ->
+ (* deactivate implicit *)
+ let ntnpats = if add_par_if_no_ntn_with_par then make_pars ?loc g else [] in
+ Some (g, in_patargs ?loc scopes g expanded true ntnpats pats)
+ | Some ntnpats ->
+ let ntnpats = if add_par_if_no_ntn_with_par && ntnpats = [] then make_pars ?loc g else ntnpats in
+ Some (g, in_patargs ?loc scopes g expanded no_impl ntnpats pats)
with Not_found -> None
- and in_pat test_kind scopes pt =
+ and in_pat ({for_ind} as test_kind) scopes pt =
let open CAst in
let loc = pt.loc in
+ (* The two policies implied by asymmetric pattern mode *)
+ let add_par_if_no_ntn_with_par = get_asymmetric_patterns () && not for_ind in
+ let no_impl = get_asymmetric_patterns () && not for_ind in
match pt.v with
| CPatAlias (p, id) -> DAst.make ?loc @@ RCPatAlias (in_pat test_kind scopes p, id)
| CPatRecord l ->
@@ -1744,36 +1678,22 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
begin match sorted_fields with
| None -> DAst.make ?loc @@ RCPatAtom None
| Some (n, head, pl) ->
- let pl =
- let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in
- List.rev_append pars pl
- in
- let (_,argscs) = find_remaining_scopes [] pl head in
- let pats = List.map2 (in_pat_sc scopes) argscs pl in
- DAst.make ?loc @@ RCPatCstr(head, pats, [])
+ let pars = make_pars ?loc head in
+ let pats = in_patargs ?loc scopes head true true pars pl in
+ DAst.make ?loc @@ RCPatCstr(head, pats)
end
| CPatCstr (head, None, pl) ->
begin
- match drop_syndef test_kind ?loc scopes head pl with
- | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c)
- | None -> Loc.raise ?loc (InternalizationError (NotAConstructor head))
+ match drop_syndef test_kind ?loc scopes head add_par_if_no_ntn_with_par no_impl pl with
+ | Some (g,pl) -> DAst.make ?loc @@ RCPatCstr(g, pl)
+ | None -> Loc.raise ?loc (InternalizationError (NotAConstructor head))
end
| CPatCstr (qid, Some expl_pl, pl) ->
- let g =
- try Nametab.locate qid
- with Not_found as exn ->
- let _, info = Exninfo.capture exn in
- let info = Option.cata (Loc.add_loc info) info loc in
- Exninfo.iraise (InternalizationError (NotAConstructor qid), info)
- in
- if expl_pl == [] then
- (* Convention: (@r) deactivates all further implicit arguments and scopes *)
- DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat test_kind_inner scopes) pl, [])
- else
- (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *)
- (* but not scopes in expl_pl *)
- let (argscs1,_) = find_remaining_scopes expl_pl pl g in
- DAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat test_kind_inner scopes) pl, [])
+ begin
+ match drop_syndef test_kind ?loc scopes qid false true (expl_pl@pl) with
+ | Some (g,pl) -> DAst.make ?loc @@ RCPatCstr (g, pl)
+ | None -> Loc.raise ?loc (InternalizationError (NotAConstructor qid))
+ end
| CPatNotation (_,(InConstrEntry,"- _"),([a],[]),[]) when is_non_zero_pat a ->
let p = match a.CAst.v with CPatPrim (Number (_, p)) -> p | _ -> assert false in
let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind test_kind_inner) (Number (SMinus,p)) scopes in
@@ -1789,20 +1709,20 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
| CPatDelimiters (key, e) ->
in_pat test_kind (None,find_delimiters_scope ?loc key::snd scopes) e
| CPatPrim p ->
- let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc test_kind_inner p scopes in
+ let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc test_kind_inner.test_kind p scopes in
rcp_of_glob scopes pat
| CPatAtom (Some id) ->
begin
- match drop_syndef test_kind ?loc scopes id [] with
- | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c)
- | None -> DAst.make ?loc @@ RCPatAtom (Some ((make ?loc @@ find_pattern_variable id),scopes))
+ match drop_syndef test_kind ?loc scopes id add_par_if_no_ntn_with_par no_impl [] with
+ | Some (g, pl) -> DAst.make ?loc @@ RCPatCstr (g, pl)
+ | None -> DAst.make ?loc @@ RCPatAtom (Some ((make ?loc @@ find_pattern_variable id),scopes))
end
| CPatAtom None -> DAst.make ?loc @@ RCPatAtom None
| CPatOr pl -> DAst.make ?loc @@ RCPatOr (List.map (in_pat test_kind scopes) pl)
| CPatCast (_,_) ->
(* We raise an error if the pattern contains a cast, due to
current restrictions on casts in patterns. Cast in patterns
- are supported only in local binders and only at top level.
+ are supported only in local binders and only at for_ind level.
The only reason they are in the [cases_pattern_expr] type
is that the parser needs to factor the "c : t" notation
with user defined notations. In the long term, we will try to
@@ -1812,7 +1732,46 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
duplicating the levels of the [pattern] rule. *)
CErrors.user_err ?loc (Pp.strbrk "Casts are not supported in this pattern.")
and in_pat_sc scopes x = in_pat test_kind_inner (x,snd scopes)
- and in_not (test_kind:?loc:Loc.t->'a->'b) loc scopes (subst,substlist as fullsubst) args = function
+ and in_patargs ?loc scopes
+ gr (* head of the pattern *)
+ expanded (* tell if comes from a notation (for error reporting) *)
+ no_impl (* tell if implicit are not expected (for asymmetric patterns, or @, or {| |} *)
+ ntnpats (* prefix of patterns obtained by expansion of notations or parameter insertion *)
+ pats (* user given patterns *)
+ =
+ let default = DAst.make ?loc @@ RCPatAtom None in
+ let npats = List.length pats in
+ let n = List.length ntnpats in
+ let ntnpats_with_letin, tags =
+ let tags = match gr with
+ | GlobRef.ConstructRef cstr -> constructor_alltags (Global.env()) cstr
+ | GlobRef.IndRef ind -> inductive_alltags (Global.env()) ind
+ | _ -> assert false in
+ let ntnpats_with_letin = adjust_to_up tags ntnpats default in
+ ntnpats_with_letin, List.skipn (List.length ntnpats_with_letin) tags in
+ let imps =
+ let imps =
+ if no_impl then [] else
+ let impls_st = implicits_of_global gr in
+ if Int.equal n 0 then select_impargs_size npats impls_st
+ else List.skipn_at_least n (select_stronger_impargs impls_st) in
+ adjust_to_down tags imps None in
+ let subscopes = adjust_to_down tags (List.skipn_at_least n (find_arguments_scope gr)) None in
+ let has_letin = check_has_letin ?loc gr expanded npats (List.count is_status_implicit imps) tags in
+ let rec aux imps subscopes tags pats =
+ match imps, subscopes, tags, pats with
+ | _, _, true::tags, p::pats when has_letin ->
+ in_pat_sc scopes None p :: aux imps subscopes tags pats
+ | _, _, true::tags, _ ->
+ default :: aux imps subscopes tags pats
+ | imp::imps, sc::subscopes, false::tags, _ when is_status_implicit imp ->
+ default :: aux imps subscopes tags pats
+ | imp::imps, sc::subscopes, false::tags, p::pats ->
+ in_pat_sc scopes sc p :: aux imps subscopes tags pats
+ | _, _, [], [] -> []
+ | _ -> assert false in
+ ntnpats_with_letin @ aux imps subscopes tags pats
+ and in_not test_kind loc scopes (subst,substlist as fullsubst) args = function
| NVar id ->
let () = assert (List.is_empty args) in
begin
@@ -1827,22 +1786,15 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
end
| NRef g ->
ensure_kind test_kind ?loc g;
- let (_,argscs) = find_remaining_scopes [] args g in
- DAst.make ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
- | NApp (NRef g,pl) ->
+ DAst.make ?loc @@ RCPatCstr (g, in_patargs ?loc scopes g true false [] args)
+ | NApp (NRef g,ntnpl) ->
ensure_kind test_kind ?loc g;
- let (argscs1,argscs2) = find_remaining_scopes pl args g in
- let pl = List.map2 (fun x -> in_not test_kind_inner loc (x,snd scopes) fullsubst []) argscs1 pl in
- let pl = add_local_defs_and_check_length loc genv g pl args in
- let args = List.map2 (fun x -> in_pat test_kind_inner (x,snd scopes)) argscs2 args in
- let pat =
- if List.length pl = 0 then
- (* Convention: if notation is @f, encoded as NApp(Nref g,[]), then
- implicit arguments are not inherited *)
- RCPatCstr (g, pl @ args, [])
- else
- RCPatCstr (g, pl, args) in
- DAst.make ?loc @@ pat
+ let ntnpl = List.map (in_not test_kind_inner loc scopes fullsubst []) ntnpl in
+ let no_impl =
+ (* Convention: if notation is @f, encoded as NApp(Nref g,[]), then
+ implicit arguments are not inherited *)
+ ntnpl = [] in
+ DAst.make ?loc @@ RCPatCstr (g, in_patargs ?loc scopes g true no_impl ntnpl args)
| NList (x,y,iter,terminator,revert) ->
if not (List.is_empty args) then user_err ?loc
(strbrk "Application of arguments to a recursive notation not supported in patterns.");
@@ -1875,23 +1827,14 @@ let rec intern_pat genv ntnvars aliases pat =
| RCPatAlias (p, id) ->
let aliases' = merge_aliases aliases id in
intern_pat genv ntnvars aliases' p
- | RCPatCstr (head, expl_pl, pl) ->
- if get_asymmetric_patterns () then
- let len = if List.is_empty expl_pl then Some (List.length pl) else None in
- let c,idslpl1 = find_constructor loc len head in
- let with_letin =
- check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
- intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl)
- else
- let c,idslpl1 = find_constructor loc None head in
- let with_letin, pl2 =
- add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
- intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
+ | RCPatCstr (head, pl) ->
+ let c = find_constructor_head ?loc head in
+ intern_cstr_with_all_args loc c true [] pl
| RCPatAtom (Some ({loc;v=id},scopes)) ->
let aliases = merge_aliases aliases (make ?loc @@ Name id) in
set_var_scope ?loc id false scopes ntnvars;
(aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)]) (* TO CHECK: aura-t-on id? *)
- | RCPatAtom (None) ->
+ | RCPatAtom None ->
let { alias_ids = ids; alias_map = asubst; } = aliases in
(ids, [asubst, DAst.make ?loc @@ PatVar (alias_of aliases)])
| RCPatOr pl ->
@@ -1903,8 +1846,9 @@ let rec intern_pat genv ntnvars aliases pat =
(ids,List.flatten pl')
let intern_cases_pattern test_kind genv ntnvars env aliases pat =
+ let test = {for_ind=false;test_kind} in
intern_pat genv ntnvars aliases
- (drop_notations_pattern (test_kind,test_kind) genv env pat)
+ (drop_notations_pattern (test,test) genv env pat)
let _ =
intern_cases_pattern_fwd :=
@@ -1924,21 +1868,21 @@ let intern_ind_pattern genv ntnvars env pat =
raise Not_found in
let no_not =
try
- drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat
+ let test_top = {for_ind=true;test_kind=test_kind_top} in
+ let test_inner = {for_ind=false;test_kind=test_kind_inner} in
+ drop_notations_pattern (test_top,test_inner) genv env pat
with InternalizationError (NotAConstructor _) as exn ->
let _, info = Exninfo.capture exn in
error_bad_inductive_type ~info ()
in
let loc = no_not.CAst.loc in
match DAst.get no_not with
- | RCPatCstr (head, expl_pl, pl) ->
- let c = (function GlobRef.IndRef ind -> ind | _ -> error_bad_inductive_type ?loc ()) head in
- let with_letin, pl2 = add_implicits_check_ind_length genv loc c
- (List.length expl_pl) pl in
- let idslpl = List.map (intern_pat genv ntnvars empty_alias) (expl_pl@pl2) in
- (with_letin,
+ | RCPatCstr (head, pl) ->
+ let ind = find_inductive_head ?loc head in
+ let idslpl = List.map (intern_pat genv ntnvars empty_alias) pl in
+ (true,
match product_of_cases_patterns empty_alias idslpl with
- | ids,[asubst,pl] -> (c,ids,asubst,chop_params_pattern loc c pl with_letin)
+ | ids,[asubst,pl] -> (ind,ids,asubst,chop_params_pattern loc ind pl true)
| _ -> error_bad_inductive_type ?loc ())
| x -> error_bad_inductive_type ?loc ()
@@ -1999,17 +1943,22 @@ let extract_explicit_arg imps args =
(Id.Map.add id (loc, a) eargs, rargs)
in aux args
+let extract_regular_arguments args =
+ List.map_filter (function
+ | (a,Some pos) -> user_err ?loc:pos.loc (str "Unexpected explicit argument.")
+ | (a,None) -> Some a) args
+
(**********************************************************************)
(* Main loop *)
let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
let rec intern env = CAst.with_loc_val (fun ?loc -> function
| CRef (ref,us) ->
- let (c,imp,subscopes),_ =
+ let c,_ =
intern_applied_reference ~isproj:None intern env (Environ.named_context_val globalenv)
lvar us [] ref
in
- apply_impargs c env imp subscopes [] loc
+ apply_impargs env loc c []
| CFix ({ CAst.loc = locid; v = iddef}, dl) ->
let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in
@@ -2108,8 +2057,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
| CNotation (_,(InConstrEntry,"( _ )"),([a],[],[],[])) -> intern env a
| CNotation (_,ntn,args) ->
let c = intern_notation intern env ntnvars loc ntn args in
- let x, impl, scopes = find_appl_head_data c in
- apply_impargs x env impl scopes [] loc
+ apply_impargs env loc c []
| CGeneralization (b,a,c) ->
intern_generalization intern env ntnvars loc b a c
| CPrim p ->
@@ -2118,12 +2066,13 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
intern {env with tmp_scope = None;
scopes = find_delimiters_scope ?loc key :: env.scopes} e
| CAppExpl ((isproj,ref,us), args) ->
- let (f,_,args_scopes),args =
+ let f,args =
let args = List.map (fun a -> (a,None)) args in
intern_applied_reference ~isproj intern env (Environ.named_context_val globalenv)
lvar us args ref
in
check_not_notation_variable f ntnvars;
+ let _,args_scopes = find_appl_head_data env lvar f in
(* Rem: GApp(_,f,[]) stands for @f *)
if args = [] then DAst.make ?loc @@ GApp (f,[]) else
smart_gapp f loc (intern_args env args_scopes (List.map fst args))
@@ -2135,22 +2084,21 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
isproj',f,args'@args
(* Don't compact "(f args') args" to resolve implicits separately *)
| _ -> isproj,f,args in
- let (c,impargs,args_scopes),args =
- match f.CAst.v with
+ (match f.CAst.v with
| CRef (ref,us) ->
- intern_applied_reference ~isproj intern env
- (Environ.named_context_val globalenv) lvar us args ref
+ let f, args = intern_applied_reference ~isproj intern env
+ (Environ.named_context_val globalenv) lvar us args ref in
+ apply_impargs env loc f args
| CNotation (_,ntn,ntnargs) ->
assert (Option.is_empty isproj);
let c = intern_notation intern env ntnvars loc ntn ntnargs in
- find_appl_head_data c, args
+ apply_impargs env loc c args
| _ ->
- assert (Option.is_empty isproj);
- let f = intern_no_implicit env f in
- let f, _, args_scopes = find_appl_head_data f in
- (f,[],args_scopes), args
- in
- apply_impargs c env impargs args_scopes args loc
+ assert (Option.is_empty isproj);
+ let f = intern_no_implicit env f in
+ let _, args_scopes = find_appl_head_data env lvar f in
+ let args = extract_regular_arguments args in
+ smart_gapp f loc (intern_args env args_scopes args))
| CRecord fs ->
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
@@ -2445,10 +2393,11 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
intern_args env subscopes rargs
in aux 1 l subscopes eargs rargs
- and apply_impargs c env imp subscopes l loc =
- let imp = select_impargs_size (List.length (List.filter (fun (_,x) -> x == None) l)) imp in
- let l = intern_impargs c env imp subscopes l in
- smart_gapp c loc l
+ and apply_impargs env loc c args =
+ let impl, subscopes = find_appl_head_data env lvar c in
+ let imp = select_impargs_size (List.length (List.filter (fun (_,x) -> x == None) args)) impl in
+ let args = intern_impargs c env imp subscopes args in
+ smart_gapp c loc args
and smart_gapp f loc = function
| [] -> f
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index c9326615dc..d2256720c4 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -759,6 +759,10 @@ let get_nth_arg head n stk =
| ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as s -> (None, List.rev rstk @ s) in
strip_rec [] head n stk
+let rec subs_consn v i n s =
+ if Int.equal i n then s
+ else subs_consn v (i + 1) n (subs_cons v.(i) s)
+
(* Beta reduction: look for an applied argument in the stack.
Since the encountered update marks are removed, h must be a whnf *)
let rec get_args n tys f e = function
@@ -770,14 +774,13 @@ let rec get_args n tys f e = function
get_args n tys f (subs_shft (k,e)) s
| Zapp l :: s ->
let na = Array.length l in
- if n == na then (Inl (subs_cons(l,e)),s)
+ if n == na then (Inl (subs_consn l 0 na e), s)
else if n < na then (* more arguments *)
- let args = Array.sub l 0 n in
let eargs = Array.sub l n (na-n) in
- (Inl (subs_cons(args,e)), Zapp eargs :: s)
+ (Inl (subs_consn l 0 n e), Zapp eargs :: s)
else (* more lambdas *)
let etys = List.skipn na tys in
- get_args (n-na) etys f (subs_cons(l,e)) s
+ get_args (n-na) etys f (subs_consn l 0 na e) s
| ((ZcaseT _ | Zproj _ | Zfix _ | Zprimitive _) :: _ | []) as stk ->
(Inr {mark=mark Cstr Unknown;term=FLambda(n,tys,f,e)}, stk)
@@ -931,7 +934,11 @@ let contract_fix_vect fix =
env, Array.length bds)
| _ -> assert false
in
- (subs_cons(Array.init nfix make_body, env), thisbody)
+ let rec mk_subs env i =
+ if Int.equal i nfix then env
+ else mk_subs (subs_cons (make_body i) env) (i + 1)
+ in
+ (mk_subs env 0, thisbody)
let unfold_projection info p =
if red_projection info.i_flags p
@@ -1367,7 +1374,7 @@ let rec knr info tab m stk =
knit info tab fxe fxbd (args@stk')
| (_,args, ((Zapp _ | Zfix _ | Zshift _ | Zupdate _ | Zprimitive _) :: _ | [] as s)) -> (m,args@s))
| FLetIn (_,v,_,bd,e) when red_set info.i_flags fZETA ->
- knit info tab (subs_cons([|v|],e)) bd stk
+ knit info tab (subs_cons v e) bd stk
| FEvar(ev,env) ->
(match info.i_cache.i_sigma ev with
Some c -> knit info tab env c stk
@@ -1417,7 +1424,7 @@ and case_inversion info tab ci (univs,args) v =
let env = info_env info in
let ind = ci.ci_ind in
let params, indices = Array.chop ci.ci_npar args in
- let psubst = subs_cons (params, subs_id 0) in
+ let psubst = subs_consn params 0 ci.ci_npar (subs_id 0) in
let mib = Environ.lookup_mind (fst ind) env in
let mip = mib.mind_packets.(snd ind) in
(* indtyping enforces 1 ctor with no letins in the context *)
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 3e8502b988..afd8e3ef67 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -60,127 +60,188 @@ let rec is_lift_id = function
(* Substitutions *)
(*********************)
-(* (bounded) explicit substitutions of type 'a *)
-type 'a subs =
- | ESID of int (* ESID(n) = %n END bounded identity *)
- | CONS of 'a array * 'a subs
- (* CONS([|t1..tn|],S) =
- (S.t1...tn) parallel substitution
- beware of the order *)
- | SHIFT of int * 'a subs (* SHIFT(n,S) = (^n o S) terms in S are relocated *)
- (* with n vars *)
- | LIFT of int * 'a subs (* LIFT(n,S) = (%n S) stands for ((^n o S).n...1) *)
-
-(* operations of subs: collapses constructors when possible.
- * Needn't be recursive if we always use these functions
- *)
-
-let subs_id i = ESID i
-
-let subs_cons(x,s) = if Int.equal (Array.length x) 0 then s else CONS(x,s)
-
-let subs_liftn n = function
- | ESID p -> ESID (p+n) (* bounded identity lifted extends by p *)
- | LIFT (p,lenv) -> LIFT (p+n, lenv)
- | lenv -> LIFT (n,lenv)
-
-let subs_lift a = subs_liftn 1 a
-let subs_liftn n a = if Int.equal n 0 then a else subs_liftn n a
-
-let subs_shft = function
- | (0, s) -> s
- | (n, SHIFT (k,s1)) -> SHIFT (k+n, s1)
- | (n, s) -> SHIFT (n,s)
-let subs_shft s = if Int.equal (fst s) 0 then snd s else subs_shft s
-
-let subs_shift_cons = function
- (0, s, t) -> CONS(t,s)
-| (k, SHIFT(n,s1), t) -> CONS(t,SHIFT(k+n, s1))
-| (k, s, t) -> CONS(t,SHIFT(k, s));;
-
-(* Tests whether a substitution is equal to the identity *)
-let rec is_subs_id = function
- ESID _ -> true
- | LIFT(_,s) -> is_subs_id s
- | SHIFT(0,s) -> is_subs_id s
- | CONS(x,s) -> Int.equal (Array.length x) 0 && is_subs_id s
- | _ -> false
-
-(* Expands de Bruijn k in the explicit substitution subs
- * lams accumulates de shifts to perform when retrieving the i-th value
- * the rules used are the following:
- *
- * [id]k --> k
- * [S.t]1 --> t
- * [S.t]k --> [S](k-1) if k > 1
- * [^n o S] k --> [^n]([S]k)
- * [(%n S)] k --> k if k <= n
- * [(%n S)] k --> [^n]([S](k-n))
- *
- * the result is (Inr (k+lams,p)) when the variable is just relocated
- * where p is None if the variable points inside subs and Some(k) if the
- * variable points k bindings beyond subs.
- *)
-let rec exp_rel lams k subs =
- match subs with
- | CONS (def,_) when k <= Array.length def
- -> Inl(lams,def.(Array.length def - k))
- | CONS (v,l) -> exp_rel lams (k - Array.length v) l
- | LIFT (n,_) when k<=n -> Inr(lams+k,None)
- | LIFT (n,l) -> exp_rel (n+lams) (k-n) l
- | SHIFT (n,s) -> exp_rel (n+lams) k s
- | ESID n when k<=n -> Inr(lams+k,None)
- | ESID n -> Inr(lams+k,Some (k-n))
-
-let expand_rel k subs = exp_rel 0 k subs
-
-let rec subs_map f = function
-| ESID _ as s -> s
-| CONS (x, s) -> CONS (Array.map f x, subs_map f s)
-| SHIFT (n, s) -> SHIFT (n, subs_map f s)
-| LIFT (n, s) -> LIFT (n, subs_map f s)
-
-let rec lift_subst mk_cl s1 s2 = match s1 with
-| ELID -> subs_map (fun c -> mk_cl ELID c) s2
-| ELSHFT(s, k) -> subs_shft(k, lift_subst mk_cl s s2)
-| ELLFT (k, s) ->
- match s2 with
- | CONS(x,s') ->
- CONS(CArray.Fun1.map mk_cl s1 x, lift_subst mk_cl s1 s')
- | ESID n -> lift_subst mk_cl s (ESID (n + k))
- | SHIFT(k',s') ->
- if k<k'
- then subs_shft(k, lift_subst mk_cl s (subs_shft(k'-k, s')))
- else subs_shft(k', lift_subst mk_cl (el_liftn (k-k') s) s')
- | LIFT(k',s') ->
- if k<k'
- then subs_liftn k (lift_subst mk_cl s (subs_liftn (k'-k) s'))
- else subs_liftn k' (lift_subst mk_cl (el_liftn (k-k') s) s')
-
-let rec comp mk_cl s1 s2 =
- match (s1, s2) with
- | _, ESID _ -> s1
- | ESID _, _ -> s2
- | SHIFT(k,s), _ -> subs_shft(k, comp mk_cl s s2)
- | _, CONS(x,s') ->
- CONS(Array.Fun1.map (fun s t -> mk_cl(s,t)) s1 x, comp mk_cl s1 s')
- | CONS(x,s), SHIFT(k,s') ->
- let lg = Array.length x in
- if k == lg then comp mk_cl s s'
- else if k > lg then comp mk_cl s (SHIFT(k-lg, s'))
- else comp mk_cl (CONS(Array.sub x 0 (lg-k), s)) s'
- | CONS(x,s), LIFT(k,s') ->
- let lg = Array.length x in
- if k == lg then CONS(x, comp mk_cl s s')
- else if k > lg then CONS(x, comp mk_cl s (LIFT(k-lg, s')))
- else
- CONS(Array.sub x (lg-k) k,
- comp mk_cl (CONS(Array.sub x 0 (lg-k),s)) s')
- | LIFT(k,s), SHIFT(k',s') ->
- if k<k'
- then subs_shft(k, comp mk_cl s (subs_shft(k'-k, s')))
- else subs_shft(k', comp mk_cl (subs_liftn (k-k') s) s')
- | LIFT(k,s), LIFT(k',s') ->
- if k<k'
- then subs_liftn k (comp mk_cl s (subs_liftn (k'-k) s'))
- else subs_liftn k' (comp mk_cl (subs_liftn (k-k') s) s')
+(* Variant of skewed lists enriched w.r.t. a monoid. See the Range module.
+
+ In addition to the indexed data, every node contains a monoid element, in our
+ case, integers. It corresponds to the number of partial shifts to apply when
+ reaching this subtree. The total shift is obtained by summing all the partial
+ shifts encountered in the tree traversal. For efficiency, we also cache the
+ sum of partial shifts of the whole subtree as the last argument of the [Node]
+ constructor.
+
+ A more intuitive but inefficient representation of this data structure would
+ be a list of terms interspeded with shifts, as in
+
+ type 'a subst = NIL | CONS of 'a or_var * 'a subst | SHIFT of 'a subst
+
+ On this inefficient representation, the typing rules would be:
+
+ · ⊢ NIL : ·
+ Γ ⊢ σ : Δ and Γ ⊢ t : A{σ} implies Γ ⊢ CONS (t, σ) : Δ, A
+ Γ ⊢ σ : Δ implies Γ, A ⊢ SHIFT σ : Δ
+
+ The efficient representation is isomorphic to this naive variant, except that
+ shifts are grouped together, and we use skewed lists instead of lists.
+
+*)
+
+type shf = int
+let cmp n m = n + m
+let idn = 0
+
+type 'a or_var = Arg of 'a | Var of int
+
+type 'a tree =
+| Leaf of shf * 'a or_var
+| Node of shf * 'a or_var * 'a tree * 'a tree * shf
+(*
+ Invariants:
+ - All trees are complete.
+ - Define get_shift inductively as [get_shift (Leaf (w, _)) := w] and
+ [get_shift (Node (w, _, t1, t2, _)) := w + t1 + t2] then for every tree
+ of the form Node (_, _, t1, t2, sub), we must have
+ sub = get_shift t1 + get_shift t2.
+
+ In the naive semantics:
+
+ Leaf (w, x) := SHIFT^w (CONS (x, NIL))
+ Node (w, x, t1, t2, _) := SHIFT^w (CONS (x, t1 @ t2))
+
+*)
+
+type 'a subs = Nil of shf * int | Cons of int * 'a tree * 'a subs
+(*
+ In the naive semantics mentioned above, we have the following.
+
+ Nil (w, n) stands for SHIFT^w (ID n) where ID n is a compact form of identity
+ substitution, defined inductively as
+
+ ID 0 := NIL
+ ID (S n) := CONS (Var 1, SHIFT (ID n))
+
+ Cons (h, t, s) stands for (t @ s) and h is the total number of values in the
+ tree t. In particular, it is always of the form 2^n - 1 for some n.
+*)
+
+(* Returns the number of shifts contained in the whole tree. *)
+let eval = function
+| Leaf (w, _) -> w
+| Node (w1, _, _, _, w2) -> cmp w1 w2
+
+let leaf x = Leaf (idn, x)
+let node x t1 t2 = Node (idn, x, t1, t2, cmp (eval t1) (eval t2))
+
+let rec tree_get h w t i = match t with
+| Leaf (w', x) ->
+ let w = cmp w w' in
+ if i = 0 then w, Inl x else assert false
+| Node (w', x, t1, t2, _) ->
+ let w = cmp w w' in
+ if i = 0 then w, Inl x
+ else
+ let h = h / 2 in
+ if i <= h then tree_get h w t1 (i - 1)
+ else tree_get h (cmp w (eval t1)) t2 (i - h - 1)
+
+let rec get w l i = match l with
+| Nil (w', n) ->
+ let w = cmp w w' in
+ if i < n then w, Inl (Var (i + 1))
+ else n + w, Inr (i - n) (* FIXME: double check *)
+| Cons (h, t, rem) ->
+ if i < h then tree_get h w t i else get (cmp (eval t) w) rem (i - h)
+
+let get l i = get idn l i
+
+let tree_write w = function
+| Leaf (w', x) -> Leaf (cmp w w', x)
+| Node (w', x, t1, t2, wt) -> Node (cmp w w', x, t1, t2, wt)
+
+let write w l = match l with
+| Nil (w', n) -> Nil (cmp w w', n)
+| Cons (h, t, rem) -> Cons (h, tree_write w t, rem)
+
+let cons x l = match l with
+| Cons (h1, t1, Cons (h2, t2, rem)) ->
+ if Int.equal h1 h2 then Cons (1 + h1 + h2, node x t1 t2, rem)
+ else Cons (1, leaf x, l)
+| _ -> Cons (1, leaf x, l)
+
+let expand_rel n s =
+ let k, v = get s (n - 1) in
+ match v with
+ | Inl (Arg v) -> Inl (k, v)
+ | Inl (Var i) -> Inr (k + i, None)
+ | Inr i -> Inr (k + i + 1, Some (i + 1))
+
+let is_subs_id = function
+| Nil (w, _) -> Int.equal w 0
+| Cons (_, _, _) -> false
+
+let subs_cons v s = cons (Arg v) s
+
+let rec push_vars i s =
+ if Int.equal i 0 then s
+ else push_vars (pred i) (cons (Var i) s)
+
+let subs_liftn n s =
+ if Int.equal n 0 then s
+ else match s with
+ | Nil (0, m) -> Nil (0, m + n) (* Preserve identity substitutions *)
+ | Nil _ | Cons _ ->
+ let s = write n s in
+ push_vars n s
+
+let subs_lift s = match s with
+| Nil (0, m) -> Nil (0, m + 1) (* Preserve identity substitutions *)
+| Nil _ | Cons _ ->
+ cons (Var 1) (write 1 s)
+
+let subs_id n = Nil (0, n)
+
+let subs_shft (n, s) = write n s
+
+(* pop is the n-ary tailrec variant of a function whose typing rules would be
+ given as follows. Assume Γ ⊢ e : Δ, A, then
+ - Γ := Ξ, A, Ω for some Ξ and Ω with |Ω| := fst (pop e)
+ - Ξ ⊢ snd (pop e) : Δ
+*)
+let rec pop n i e =
+ if Int.equal n 0 then i, e
+ else match e with
+ | ELID -> i, e
+ | ELLFT (k, e) ->
+ if k <= n then pop (n - k) i e
+ else i, ELLFT (k - n, e)
+ | ELSHFT (e, k) -> pop n (i + k) e
+
+let apply mk e = function
+| Var i -> Var (reloc_rel i e)
+| Arg v -> Arg (mk e v)
+
+let rec tree_map mk e = function
+| Leaf (w, x) ->
+ let (n, e) = pop w 0 e in
+ Leaf (w + n, apply mk e x), e
+| Node (w, x, t1, t2, _) ->
+ let (n, e) = pop w 0 e in
+ let x = apply mk e x in
+ let t1, e = tree_map mk e t1 in
+ let t2, e = tree_map mk e t2 in
+ Node (w + n, x, t1, t2, cmp (eval t1) (eval t2)), e
+
+let rec lift_id e n = match e with
+| ELID -> Nil (0, n)
+| ELSHFT (e, k) -> write k (lift_id e n)
+| ELLFT (k, e) ->
+ if k <= n then subs_liftn k (lift_id e (n - k))
+ else assert false
+
+let rec lift_subst mk e s = match s with
+| Nil (w, m) ->
+ let (n, e) = pop w 0 e in
+ write (w + n) (lift_id e m)
+| Cons (h, t, rem) ->
+ let t, e = tree_map mk e t in
+ let rem = lift_subst mk e rem in
+ Cons (h, t, rem)
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index 4239e42adc..8ff29ab07a 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -11,28 +11,38 @@
(** Explicit substitutions *)
(** {6 Explicit substitutions } *)
-(** Explicit substitutions of type ['a].
- - ESID(n) = %n END bounded identity
- - CONS([|t1..tn|],S) = (S.t1...tn) parallel substitution
- (beware of the order: indice 1 is substituted by tn)
- - SHIFT(n,S) = (^n o S) terms in S are relocated with n vars
- - LIFT(n,S) = (%n S) stands for ((^n o S).n...1)
- (corresponds to S crossing n binders) *)
-type 'a subs = private
- | ESID of int
- | CONS of 'a array * 'a subs
- | SHIFT of int * 'a subs
- | LIFT of int * 'a subs
+(** Explicit substitutions for some type of terms ['a].
+
+ Assuming terms enjoy a notion of typability Γ ⊢ t : A, where Γ is a
+ telescope and A a type, substitutions can be typed as Γ ⊢ σ : Δ, where
+ as a first approximation σ is a list of terms u₁; ...; uₙ s.t.
+ Δ := (x₁ : A₁), ..., (xₙ : Aₙ) and Γ ⊢ uᵢ : Aᵢ{u₁...uᵢ₋₁} for all 1 ≤ i ≤ n.
+
+ Substitutions can be applied to terms as follows, and furthermore
+ if Γ ⊢ σ : Δ and Δ ⊢ t : A, then Γ ⊢ t{σ} : A{σ}.
+
+ We make the typing rules explicit below, but we omit the explicit De Bruijn
+ fidgetting and leave relocations implicit in terms and types.
+
+*)
+type 'a subs
(** Derived constructors granting basic invariants *)
+
+(** Assuming |Γ| = n, Γ ⊢ subs_id n : Γ *)
val subs_id : int -> 'a subs
-val subs_cons: 'a array * 'a subs -> 'a subs
+
+(** Assuming Γ ⊢ σ : Δ and Γ ⊢ t : A{σ}, then Γ ⊢ subs_cons t σ : Δ, A *)
+val subs_cons: 'a -> 'a subs -> 'a subs
+
+(** Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ subs_shft (n, σ) : Δ *)
val subs_shft: int * 'a subs -> 'a subs
+
+(** Unary variant of {!subst_liftn}. *)
val subs_lift: 'a subs -> 'a subs
-val subs_liftn: int -> 'a subs -> 'a subs
-(** [subs_shift_cons(k,s,[|t1..tn|])] builds (^k s).t1..tn *)
-val subs_shift_cons: int * 'a subs * 'a array -> 'a subs
+(** Assuming Γ ⊢ σ : Δ and |Ξ| = n, then Γ, Ξ ⊢ subs_liftn n σ : Δ, Ξ *)
+val subs_liftn: int -> 'a subs -> 'a subs
(** [expand_rel k subs] expands de Bruijn [k] in the explicit substitution
[subs]. The result is either (Inl(lams,v)) when the variable is
@@ -51,7 +61,6 @@ val is_subs_id: 'a subs -> bool
mk_clos is used when a closure has to be created, i.e. when
s1 is applied on an element of s2.
*)
-val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
(** {6 Compact representation } *)
(** Compact representation of explicit relocations
@@ -60,6 +69,10 @@ val comp : ('a subs * 'a -> 'a) -> 'a subs -> 'a subs -> 'a subs
Invariant ensured by the private flag: no lift contains two consecutive
[ELSHFT] nor two consecutive [ELLFT].
+
+ Relocations are a particular kind of substitutions that only contain
+ variables. In particular, [el_*] enjoys the same typing rules as the
+ equivalent substitution function [subs_*].
*)
type lift = private
| ELID
@@ -77,5 +90,7 @@ val is_lift_id : lift -> bool
substitution equivalent to applying el then s. Argument
mk_clos is used when a closure has to be created, i.e. when
el is applied on an element of s.
+
+ That is, if Γ ⊢ e : Δ and Δ ⊢ σ : Ξ, then Γ ⊢ lift_subst mk e σ : Ξ.
*)
val lift_subst : (lift -> 'a -> 'b) -> lift -> 'a subs -> 'b subs
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 18f16f427d..b27c53ef0f 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -102,7 +102,7 @@ let decompose_Llam_Llet lam =
let subst_id = subs_id 0
let lift = subs_lift
let liftn = subs_liftn
-let cons v subst = subs_cons([|v|], subst)
+let cons v subst = subs_cons v subst
let shift subst = subs_shft (1, subst)
(* Linked code location utilities *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 85e24f87b7..802a32b0e7 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -198,7 +198,7 @@ let type_of_apply env func funt argsv argstv =
let argt = argstv.(i) in
let c1 = term_of_fconstr c1 in
begin match conv_leq false env argt c1 with
- | () -> apply_rec (i+1) (mk_clos (Esubst.subs_cons ([| inject arg |], e)) c2)
+ | () -> apply_rec (i+1) (mk_clos (Esubst.subs_cons (inject arg) e) c2)
| exception NotConvertible ->
error_cant_apply_bad_type env
(i+1,c1,argt)
diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml
index 9cca204e8c..390fa58883 100644
--- a/kernel/vmlambda.ml
+++ b/kernel/vmlambda.ml
@@ -179,7 +179,7 @@ let decompose_Llam lam =
let subst_id = subs_id 0
let lift = subs_lift
let liftn = subs_liftn
-let cons v subst = subs_cons([|v|], subst)
+let cons v subst = subs_cons v subst
let shift subst = subs_shft (1, subst)
(* A generic map function *)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a793e217d4..d2859b1b4e 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -46,8 +46,10 @@ module NamedDecl = Context.Named.Declaration
type pattern_matching_error =
| BadPattern of constructor * constr
| BadConstructor of constructor * inductive
- | WrongNumargConstructor of constructor * int
- | WrongNumargInductive of inductive * int
+ | WrongNumargConstructor of
+ {cstr:constructor; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int}
+ | WrongNumargInductive of
+ {ind:inductive; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int}
| UnusedClause of cases_pattern list
| NonExhaustive of cases_pattern list
| CannotInferPredicate of (constr * types) array
@@ -65,11 +67,13 @@ let error_bad_constructor ?loc env cstr ind =
raise_pattern_matching_error ?loc
(env, Evd.empty, BadConstructor (cstr,ind))
-let error_wrong_numarg_constructor ?loc env c n =
- raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargConstructor(c,n))
+let error_wrong_numarg_constructor ?loc env ~cstr ~expanded ~nargs ~expected_nassums ~expected_ndecls =
+ raise_pattern_matching_error ?loc (env, Evd.empty,
+ WrongNumargConstructor {cstr; expanded; nargs; expected_nassums; expected_ndecls})
-let error_wrong_numarg_inductive ?loc env c n =
- raise_pattern_matching_error ?loc (env, Evd.empty, WrongNumargInductive(c,n))
+let error_wrong_numarg_inductive ?loc env ~ind ~expanded ~nargs ~expected_nassums ~expected_ndecls =
+ raise_pattern_matching_error ?loc (env, Evd.empty,
+ WrongNumargInductive {ind; expanded; nargs; expected_nassums; expected_ndecls})
let list_try_compile f l =
let rec aux errors = function
@@ -519,13 +523,18 @@ let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with
(* Check the constructor has the right number of args *)
let ci = cstrs.(i-1) in
let nb_args_constr = ci.cs_nargs in
- if Int.equal (List.length args) nb_args_constr then pat
+ let nargs = List.length args in
+ if Int.equal nargs nb_args_constr then pat
else
try
let args' = adjust_local_defs ?loc (args, List.rev ci.cs_args)
in DAst.make ?loc @@ PatCstr (cstr, args', alias)
with NotAdjustable ->
- error_wrong_numarg_constructor ?loc env cstr nb_args_constr
+ let nlet = List.count (function LocalDef _ -> true | _ -> false) ci.cs_args in
+ (* In practice, this is already checked at interning *)
+ error_wrong_numarg_constructor ?loc env ~cstr
+ (* as if not expanded: *) ~expanded:false ~nargs ~expected_nassums:nb_args_constr
+ ~expected_ndecls:(nb_args_constr + nlet)
else
(* Try to insert a coercion *)
try
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 9a986bc14c..ade1fbf3d3 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -23,17 +23,21 @@ open Evardefine
type pattern_matching_error =
| BadPattern of constructor * constr
| BadConstructor of constructor * inductive
- | WrongNumargConstructor of constructor * int
- | WrongNumargInductive of inductive * int
+ | WrongNumargConstructor of
+ {cstr:constructor; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int}
+ | WrongNumargInductive of
+ {ind:inductive; expanded:bool; nargs:int; expected_nassums:int; expected_ndecls:int}
| UnusedClause of cases_pattern list
| NonExhaustive of cases_pattern list
| CannotInferPredicate of (constr * types) array
exception PatternMatchingError of env * evar_map * pattern_matching_error
-val error_wrong_numarg_constructor : ?loc:Loc.t -> env -> constructor -> int -> 'a
+val error_wrong_numarg_constructor :
+ ?loc:Loc.t -> env -> cstr:constructor -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a
-val error_wrong_numarg_inductive : ?loc:Loc.t -> env -> inductive -> int -> 'a
+val error_wrong_numarg_inductive :
+ ?loc:Loc.t -> env -> ind:inductive -> expanded:bool -> nargs:int -> expected_nassums:int -> expected_ndecls:int -> 'a
val irrefutable : env -> cases_pattern -> bool
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 2661000a39..bada2c3a60 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -111,15 +111,20 @@ let shift_value n v =
* (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1}))
* -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti)
*)
+
+let rec mk_fix_subs make_body n env i =
+ if Int.equal i n then env
+ else mk_fix_subs make_body n (subs_cons (make_body i) env) (i + 1)
+
let contract_fixp env ((reci,i),(_,_,bds as bodies)) =
let make_body j = FIXP(((reci,j),bodies), env, [||]) in
let n = Array.length bds in
- subs_cons(Array.init n make_body, env), bds.(i)
+ mk_fix_subs make_body n env 0, bds.(i)
let contract_cofixp env (i,(_,_,bds as bodies)) =
let make_body j = COFIXP((j,bodies), env, [||]) in
let n = Array.length bds in
- subs_cons(Array.init n make_body, env), bds.(i)
+ mk_fix_subs make_body n env 0, bds.(i)
let make_constr_ref n k t =
match k with
@@ -401,6 +406,10 @@ let rec strip_app = function
| APP (args,st) -> APP (args,strip_app st)
| s -> TOP
+let rec subs_consn v i n s =
+ if Int.equal i n then s
+ else subs_consn v (i + 1) n (subs_cons v.(i) s)
+
(* The main recursive functions
*
* Go under applications and cases/projections (pushed in the stack),
@@ -456,7 +465,7 @@ let rec norm_head info env t stack =
(* New rule: for Cbv, Delta does not apply to locally bound variables
or red_set info.reds fDELTA
*)
- let env' = subs_cons ([|cbv_stack_term info TOP env b|],env) in
+ let env' = subs_cons (cbv_stack_term info TOP env b) env in
norm_head info env' c stack
else
(CBN(t,env), stack) (* Should we consider a commutative cut ? *)
@@ -526,14 +535,14 @@ and cbv_stack_value info env = function
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
+ cbv_stack_term info stk (subs_consn args 0 nargs env) b
else if nlams < nargs then
- let env' = subs_cons(Array.sub args 0 nlams, env) in
+ let env' = subs_consn args 0 nlams env in
let eargs = Array.sub args nlams (nargs-nlams) in
cbv_stack_term info (APP(eargs,stk)) env' b
else
let ctxt' = List.skipn nargs ctxt in
- LAM(nlams-nargs,ctxt', b, subs_cons(args,env))
+ LAM(nlams-nargs,ctxt', b, subs_consn args 0 nargs env)
(* a Fix applied enough -> IOTA *)
| (FIXP(fix,env,[||]), stk)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 23145b1629..bd875cf68b 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -245,6 +245,14 @@ let inductive_alldecls env (ind,u) =
let inductive_alldecls_env env (ind,u) = inductive_alldecls env (ind,u)
[@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"]
+let inductive_alltags env ind =
+ let (mib,mip) = Inductive.lookup_mind_specif env ind in
+ Context.Rel.to_tags mip.mind_arity_ctxt
+
+let constructor_alltags env (ind,j) =
+ let (mib,mip) = Inductive.lookup_mind_specif env ind in
+ Context.Rel.to_tags (fst mip.mind_nf_lc.(j-1))
+
let constructor_has_local_defs env (indsp,j) =
let (mib,mip) = Inductive.lookup_mind_specif env indsp in
let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 1e2bba9f73..3705d39280 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -138,6 +138,10 @@ val constructor_nrealdecls : env -> constructor -> int
val constructor_nrealdecls_env : env -> constructor -> int
[@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"]
+(** @return tags of all decls: true = assumption, false = letin *)
+val inductive_alltags : env -> inductive -> bool list
+val constructor_alltags : env -> constructor -> bool list
+
(** Is there local defs in params or args ? *)
val constructor_has_local_defs : env -> constructor -> bool
val inductive_has_local_defs : env -> inductive -> bool
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 01564e7f25..984ac4e527 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -74,7 +74,9 @@ fun '{{n, m, p}} => n + m + p
fun '(D n m p q) => n + m + p + q
: J -> nat
The command has indeed failed with message:
-The constructor D (in type J) expects 3 arguments.
+Once notations are expanded, the resulting constructor D (in type J) is
+expected to be applied to no arguments while it is actually applied to
+1 argument.
lem1 =
fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
: forall k : nat * nat, k = k
@@ -181,3 +183,51 @@ end
File "stdin", line 253, characters 4-5:
Warning: Unused variable B catches more than one case.
[unused-pattern-matching-variable,pattern-matching]
+The command has indeed failed with message:
+Application of arguments to a recursive notation not supported in patterns.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 3 arguments.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 1 argument.
+The command has indeed failed with message:
+The constructor D' (in type J') is expected to be applied to 4 arguments (or
+6 arguments when including variables for local definitions) while it is
+actually applied to 5 arguments.
+fun x : J' bool (true, true) =>
+match x with
+| D' _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e
+end
+ : J' bool (true, true) -> {x0 : nat & x0 = x0}
+fun x : J' bool (true, true) =>
+match x with
+| @D' _ _ _ _ n _ p _ => n + p
+end
+ : J' bool (true, true) -> nat
+The command has indeed failed with message:
+Application of arguments to a recursive notation not supported in patterns.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 3 arguments.
+The command has indeed failed with message:
+The constructor cons (in type list) is expected to be applied to 2 arguments
+while it is actually applied to 1 argument.
+The command has indeed failed with message:
+The constructor D' (in type J') is expected to be applied to 3 arguments (or
+4 arguments when including variables for local definitions) while it is
+actually applied to 2 arguments.
+The command has indeed failed with message:
+The constructor D' (in type J') is expected to be applied to 3 arguments (or
+4 arguments when including variables for local definitions) while it is
+actually applied to 5 arguments.
+fun x : J' bool (true, true) =>
+match x with
+| @D' _ _ _ _ _ m _ e => existT (fun x0 : nat => x0 = x0) m e
+end
+ : J' bool (true, true) -> {x0 : nat & x0 = x0}
+fun x : J' bool (true, true) =>
+match x with
+| @D' _ _ _ _ n _ p _ => (n, p)
+end
+ : J' bool (true, true) -> nat * nat
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 2d8a8b359c..0cb3ac3ddc 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -254,3 +254,33 @@ Definition bar (f : foo) :=
end.
End Wish12762.
+
+Module ConstructorArgumentsNumber.
+
+Arguments cons {A} _ _.
+
+Inductive J' A {B} (C:=(A*B)%type) (c:C) := D' : forall n {m}, let p := n+m in m=m -> J' A c.
+
+Unset Asymmetric Patterns.
+
+Fail Check fun x => match x with (y,z) w => y+z+w end.
+Fail Check fun x => match x with cons y z w => 0 | nil => 0 end.
+Fail Check fun x => match x with cons y => 0 | nil => 0 end.
+
+(* Missing a let-in to be in let-in mode *)
+Fail Check fun x => match x with D' _ _ n p e => 0 end.
+Check fun x : J' bool (true,true) => match x with D' _ _ n e => existT (fun x => eq x x) _ e end.
+Check fun x : J' bool (true,true) => match x with D' _ _ _ n p e => n+p end.
+
+Set Asymmetric Patterns.
+
+Fail Check fun x => match x with (y,z) w => y+z+w end.
+Fail Check fun x => match x with cons y z w => 0 | nil => 0 end.
+Fail Check fun x => match x with cons y => 0 | nil => 0 end.
+
+Fail Check fun x => match x with D' n _ => 0 end.
+Fail Check fun x => match x with D' n m p e _ => 0 end.
+Check fun x : J' bool (true,true) => match x with D' n m e => existT (fun x => eq x x) m e end.
+Check fun x : J' bool (true,true) => match x with D' n m p e => (n,p) end.
+
+End ConstructorArgumentsNumber.
diff --git a/test-suite/output/RecordFieldErrors.out b/test-suite/output/RecordFieldErrors.out
index 5b67f632c9..b80345108e 100644
--- a/test-suite/output/RecordFieldErrors.out
+++ b/test-suite/output/RecordFieldErrors.out
@@ -11,4 +11,4 @@ This record defines several times the field foo.
The command has indeed failed with message:
This record defines several times the field unit.
The command has indeed failed with message:
-unit: Not a projection of inductive t.
+unit: Not a projection.
diff --git a/test-suite/output/RecordFieldErrors.v b/test-suite/output/RecordFieldErrors.v
index 27aa07822b..ff817c31aa 100644
--- a/test-suite/output/RecordFieldErrors.v
+++ b/test-suite/output/RecordFieldErrors.v
@@ -35,4 +35,4 @@ acceptable and seems an unlikely mistake. *)
Fail Check {| foo := tt;
unit := tt |}.
-(* unit: Not a projection of inductive t. *)
+(* unit: Not a projection. *)
diff --git a/test-suite/success/Case22.v b/test-suite/success/Case22.v
index 465b3eb8c0..90c1b308f2 100644
--- a/test-suite/success/Case22.v
+++ b/test-suite/success/Case22.v
@@ -89,3 +89,16 @@ Check fun x:Ind bool nat =>
match x in Ind _ X Y Z return Z with
| y => (true,0)
end.
+
+(* A check that multi-implicit arguments work *)
+
+Check fun x : {True}+{False} => match x with left _ _ => 0 | right _ _ => 1 end.
+Check fun x : {True}+{False} => match x with left _ => 0 | right _ => 1 end.
+
+(* Check that Asymmetric Patterns does not apply to the in clause *)
+
+Inductive expr {A} : A -> Type := intro : forall {n:nat} (a:A), n=n -> expr a.
+Check fun (x:expr true) => match x in expr n return n=n with intro _ _ => eq_refl end.
+Set Asymmetric Patterns.
+Check fun (x:expr true) => match x in expr n return n=n with intro _ a _ => eq_refl a end.
+Unset Asymmetric Patterns.
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 232ac17cbf..e678fc7882 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1882,3 +1882,60 @@ Check match O in nat return nat with O => O | _ => O end.
(* Checking that aliases are substituted in the correct order *)
Check match eq_refl (1,0) in _ = (y as z, y' as z) return z = z with eq_refl => eq_refl end : 0=0.
+
+(* Checking use of argument scopes *)
+
+Module Intern.
+
+Inductive I (A:Type) := C : nat -> let a:=0 in bool -> list bool -> bool -> I A.
+
+Close Scope nat_scope.
+Notation "0" := true : bool_scope.
+Notation "0" := nil : list_scope.
+Notation C' := @C (only parsing).
+Notation C'' := C (only parsing).
+Notation C''' := (C _ 0) (only parsing).
+
+Set Asymmetric Patterns.
+
+Check fun x => match x with C 0 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C 0 _ 0 0 0 => O | _ => O end. (* was not supported *)
+
+Check fun x => match x with C' 0 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C' _ 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C' 0 _ 0 0 0 => O | _ => O end. (* was not supported *)
+Check fun x => match x with C' _ _ 0 0 0 => O | _ => O end. (* was pre 8.5 bug *)
+
+Check fun x => match x with C'' 0 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C'' _ 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C'' 0 _ 0 0 0 => O | _ => O end. (* was not supported *)
+Check fun x => match x with C'' _ _ 0 0 0 => O | _ => O end. (* was pre 8.5 bug *)
+
+Check fun x => match x with C''' 0 0 0 => O | _ => O end. (* 8.5 regression *)
+Check fun x => match x with C''' _ 0 0 0 => O | _ => O end. (* was not supported *)
+
+Unset Asymmetric Patterns.
+Arguments C {A} _ {x} _ _.
+
+Check fun x => match x with C 0 0 0 => O | _ => O end. (* was ok *)
+Check fun x => match x with C 0 _ 0 0 => O | _ => O end. (* was wrong scope on last argument with let-in *)
+
+Check fun x => match x with C' _ 0 _ 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with C' _ 0 _ 0 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with C'' _ 0 0 => O | _ => O end. (* was ok *)
+Check fun x => match x with C'' _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with C''' 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with C''' _ 0 0 => O | _ => O end. (* works by miscount compensating *)
+
+Check fun x => match x with (@C _ 0) _ 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with (@C _ 0) _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with @C _ 0 _ 0 0 => O | _ => O end. (* was ok *)
+Check fun x => match x with @C _ 0 _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+Check fun x => match x with (@C) _ O _ 0 0 => O | _ => O end. (* was wrong scope *)
+Check fun x => match x with (@C) _ O _ _ 0 0 => O | _ => O end. (* was wrong scope *)
+
+End Intern.
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index d35e13c4ef..bff0359782 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1325,14 +1325,28 @@ let decline_string n s =
else if Int.equal n 1 then str "1 " ++ str s
else (int n ++ str " " ++ str s ++ str "s")
-let explain_wrong_numarg_constructor env cstr n =
- str "The constructor " ++ pr_constructor env cstr ++
- str " (in type " ++ pr_inductive env (inductive_of_constructor cstr) ++
- str ") expects " ++ decline_string n "argument" ++ str "."
-
-let explain_wrong_numarg_inductive env ind n =
- str "The inductive type " ++ pr_inductive env ind ++
- str " expects " ++ decline_string n "argument" ++ str "."
+let explain_wrong_numarg_pattern expanded nargs expected_nassums expected_ndecls pp =
+ (if expanded then
+ strbrk "Once notations are expanded, the resulting "
+ else
+ strbrk "The ") ++ pp ++
+ strbrk " is expected to be applied to " ++ decline_string expected_nassums "argument" ++
+ (if expected_nassums = expected_ndecls then mt () else
+ strbrk " (or " ++ decline_string expected_ndecls "argument" ++
+ strbrk " when including variables for local definitions)") ++
+ strbrk " while it is actually applied to " ++
+ decline_string nargs "argument" ++ str "."
+
+let explain_wrong_numarg_constructor env cstr expanded nargs expected_nassums expected_ndecls =
+ let pp =
+ strbrk "constructor " ++ pr_constructor env cstr ++
+ strbrk " (in type " ++ pr_inductive env (inductive_of_constructor cstr) ++
+ strbrk ")" in
+ explain_wrong_numarg_pattern expanded nargs expected_nassums expected_ndecls pp
+
+let explain_wrong_numarg_inductive env ind expanded nargs expected_nassums expected_ndecls =
+ let pp = strbrk "inductive type " ++ pr_inductive env ind in
+ explain_wrong_numarg_pattern expanded nargs expected_nassums expected_ndecls pp
let explain_unused_clause env pats =
str "Pattern \"" ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats) ++ strbrk "\" is redundant in this clause."
@@ -1357,10 +1371,10 @@ let explain_pattern_matching_error env sigma = function
explain_bad_pattern env sigma c t
| BadConstructor (c,ind) ->
explain_bad_constructor env c ind
- | WrongNumargConstructor (c,n) ->
- explain_wrong_numarg_constructor env c n
- | WrongNumargInductive (c,n) ->
- explain_wrong_numarg_inductive env c n
+ | WrongNumargConstructor {cstr; expanded; nargs; expected_nassums; expected_ndecls} ->
+ explain_wrong_numarg_constructor env cstr expanded nargs expected_nassums expected_ndecls
+ | WrongNumargInductive {ind; expanded; nargs; expected_nassums; expected_ndecls} ->
+ explain_wrong_numarg_inductive env ind expanded nargs expected_nassums expected_ndecls
| UnusedClause tms ->
explain_unused_clause env tms
| NonExhaustive tms ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 04:34:12 +0000