diff options
78 files changed, 1233 insertions, 824 deletions
diff --git a/CHANGES.md b/CHANGES.md index bcdb951a94..4f75bfe0b2 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -49,6 +49,9 @@ Notations - New command `String Notation` to register string syntax for custom inductive types. +- Various bugs have been fixed (e.g. PR #9214 on removing spurious + parentheses on abbreviations shortening a strict prefix of an application). + Plugins - The quote plugin (https://coq.inria.fr/distrib/V8.8.1/refman/proof-engine/detailed-tactic-examples.html#quote) @@ -161,12 +164,24 @@ Misc SSReflect - New intro patterns: - - temporary introduction: => + - - block introduction: => [^ prefix ] [^~ suffix ] - - fast introduction: => > - - tactics as views: => /ltac:mytac + - temporary introduction: `=> +` + - block introduction: `=> [^ prefix ] [^~ suffix ]` + - fast introduction: `=> >` + - tactics as views: `=> /ltac:mytac` + - replace hypothesis: `=> {}H` See the reference manual for the actual documentation. +- Clear discipline made consistent across the entire proof language. + Whenever a clear switch `{x..}` comes immediately before an existing proof + context entry (used as a view, as a rewrite rule or as name for a new + context entry) then such entry is cleared too. + + E.g. The following sentences are elaborated as follows (when H is an existing + proof context entry): + - `=> {x..} H` -> `=> {x..H} H` + - `=> {x..} /H` -> `=> /v {x..H}` + - `rewrite {x..} H` -> `rewrite E {x..H}` + Changes from 8.8.2 to 8.9+beta1 =============================== @@ -82,7 +82,8 @@ export MLPACKFILES := $(call find, '*.mlpack') export MLGFILES := $(call find, '*.mlg') export CFILES := $(call findindir, 'kernel/byterun', '*.c') -MERLININFILES := $(call find, '.merlin.in') +# NB our find wrapper ignores the test suite +MERLININFILES := $(call find, '.merlin.in') test-suite/unit-tests/.merlin.in export MERLINFILES := $(MERLININFILES:.in=) # NB: The lists of currently existing .ml and .mli files will change diff --git a/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh new file mode 100644 index 0000000000..ebd1b524da --- /dev/null +++ b/dev/ci/user-overlays/09263-maximedenes-parsing-state.sh @@ -0,0 +1,12 @@ +if [ "$CI_PULL_REQUEST" = "9263" ] || [ "$CI_BRANCH" = "parsing-state" ]; then + + mtac2_CI_REF=proof-mode + mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2 + + ltac2_CI_REF=proof-mode + ltac2_CI_GITURL=https://github.com/maximedenes/ltac2 + + equations_CI_REF=proof-mode + equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations + +fi diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index b1c111685b..d05b6c8eef 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -4,37 +4,20 @@ - [ ] Create a new issue to track the release process where you can copy-paste the present checklist. -- [ ] Change the version name to the next major version and the magic numbers - (see [#7008](https://github.com/coq/coq/pull/7008/files)). -- [ ] Update the compatibility infrastructure, which consists of doing - the following steps. Note that all but the final step can be - performed automatically by - [`dev/tools/update-compat.py`](/dev/tools/update-compat.py) so - long as you have already updated `coq_version` in - [`configure.ml`](/configure.ml). - + [ ] Add a file `theories/Compat/CoqXX.v` which contains just the header - from [`dev/header.ml`](/dev/header.ml) - + [ ] Add the line `Require Export Coq.Compat.CoqXX.` at the top of - `theories/Compat/CoqYY.v`, where Y.Y is the version prior to X.X. - + [ ] Delete the file `theories/Compat/CoqWW.v`, where W.W is three versions - prior to X.X. - + [ ] Update - [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template) - with the deleted/added files. - + [ ] Remove any notations in the standard library which have `compat "W.W"`. - + [ ] Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by - bumping all the version numbers by one, and update the interpretations - of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and - [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg). - + [ ] Update the files - [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v), - [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v), - and - [`test-suite/success/CompatOldFlag.v`](/test-suite/success/CompatOldFlag.v) - by bumping all version numbers by 1. - + [ ] Decide what to do about all test-suite files which mention `-compat - W.W` or `Coq.Comapt.CoqWW` (which is no longer valid, since we only - keep compatibility against the two previous versions) +- [ ] Change the version name to the next major version and the magic + numbers (see [#7008](https://github.com/coq/coq/pull/7008/files)). + + Additionally, in the same commit, update the compatibility + infrastructure, which consists of invoking + [`dev/tools/update-compat.py`](../tools/update-compat.py) with the + `--master` flag. + + Note that the `update-compat.py` script must be run twice: once + *immediately after* branching with the `--master` flag (which sets + up Coq to support four `-compat` flag arguments), *in the same + commit* as the one that updates `coq_version` in + [`configure.ml`](../../configure.ml), and once again later on before + the next branch point with the `--release` flag (see next section). - [ ] Put the corresponding alpha tag using `git tag -s`. The `VX.X+alpha` tag marks the first commit to be in `master` and not in the branch of the previous version. @@ -43,6 +26,19 @@ release date) and put this information in the milestone (using the description and due date fields). +## Anytime after the previous version is branched off master ## + +- [ ] Update the compatibility infrastructure to the next release, + which consists of invoking + [`dev/tools/update-compat.py`](../tools/update-compat.py) with the + `--release` flag; this sets up Coq to support three `-compat` flag + arguments. To ensure that CI passes, you will have to decide what + to do about all test-suite files which mention `-compat U.U` or + `Coq.Comapt.CoqUU` (which is no longer valid, since we only keep + compatibility against the two previous versions on releases), and + you may have to prepare overlays for projects using the + compatibility flags. + ## About one month before the beta ## - [ ] Create the `X.X.0` milestone and set its due date. diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index 14094553a2..bde00a2f0d 100755 --- a/dev/tools/update-compat.py +++ b/dev/tools/update-compat.py @@ -1,6 +1,60 @@ #!/usr/bin/env python from __future__ import with_statement -import os, re, sys +import os, re, sys, subprocess + +# When passed `--release`, this script sets up Coq to support three +# `-compat` flag arguments. If executed manually, this would consist +# of doing the following steps: +# +# - Delete the file `theories/Compat/CoqUU.v`, where U.U is four +# versions prior to the new version X.X. After this, there +# should be exactly three `theories/Compat/CoqNN.v` files. +# - Update +# [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template) +# with the deleted file. +# - Remove any notations in the standard library which have `compat "U.U"`. +# - Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by +# bumping all the version numbers by one, and update the interpretations +# of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and +# [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg). +# +# - Remove the file +# [`test-suite/success/CompatOldOldFlag.v`](/test-suite/success/CompatOldOldFlag.v). +# - Update +# [`test-suite/tools/update-compat/run.sh`](/test-suite/tools/update-compat/run.sh) +# to ensure that it passes `--release` to the `update-compat.py` +# script. + +# When passed the `--master` flag, this script sets up Coq to support +# four `-compat` flag arguments. If executed manually, this would +# consist of doing the following steps: +# +# - Add a file `theories/Compat/CoqXX.v` which contains just the header +# from [`dev/header.ml`](/dev/header.ml) +# - Add the line `Require Export Coq.Compat.CoqXX.` at the top of +# `theories/Compat/CoqYY.v`, where Y.Y is the version prior to X.X. +# - Update +# [`doc/stdlib/index-list.html.template`](/doc/stdlib/index-list.html.template) +# with the added file. +# - Update the type `compat_version` in [`lib/flags.ml`](/lib/flags.ml) by +# bumping all the version numbers by one, and update the interpretations +# of those flags in [`toplevel/coqargs.ml`](/toplevel/coqargs.ml) and +# [`vernac/g_vernac.mlg`](/vernac/g_vernac.mlg). +# - Update the files +# [`test-suite/success/CompatCurrentFlag.v`](/test-suite/success/CompatCurrentFlag.v), +# [`test-suite/success/CompatPreviousFlag.v`](/test-suite/success/CompatPreviousFlag.v), +# and +# [`test-suite/success/CompatOldFlag.v`](/test-suite/success/CompatOldFlag.v) +# by bumping all version numbers by 1. Re-create the file +# [`test-suite/success/CompatOldOldFlag.v`](/test-suite/success/CompatOldOldFlag.v) +# with its version numbers also bumped by 1 (file should have +# been removed before branching; see above). +# - Update +# [`test-suite/tools/update-compat/run.sh`](/test-suite/tools/update-compat/run.sh) +# to ensure that it passes `--master` to the `update-compat.py` +# script. + + # Obtain the absolute path of the script being run. By assuming that # the script lives in dev/tools/, and basing all calls on the path of @@ -11,6 +65,8 @@ ROOT_PATH = os.path.realpath(os.path.join(SCRIPT_PATH, '..', '..')) CONFIGURE_PATH = os.path.join(ROOT_PATH, 'configure.ml') HEADER_PATH = os.path.join(ROOT_PATH, 'dev', 'header.ml') DEFAULT_NUMBER_OF_OLD_VERSIONS = 2 +RELEASE_NUMBER_OF_OLD_VERSIONS = 2 +MASTER_NUMBER_OF_OLD_VERSIONS = 3 EXTRA_HEADER = '\n(** Compatibility file for making Coq act similar to Coq v%s *)\n' FLAGS_MLI_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.mli') FLAGS_ML_PATH = os.path.join(ROOT_PATH, 'lib', 'flags.ml') @@ -18,6 +74,7 @@ COQARGS_ML_PATH = os.path.join(ROOT_PATH, 'toplevel', 'coqargs.ml') G_VERNAC_PATH = os.path.join(ROOT_PATH, 'vernac', 'g_vernac.mlg') DOC_INDEX_PATH = os.path.join(ROOT_PATH, 'doc', 'stdlib', 'index-list.html.template') BUG_4798_PATH = os.path.join(ROOT_PATH, 'test-suite', 'bugs', 'closed', 'bug_4798.v') +TEST_SUITE_RUN_PATH = os.path.join(ROOT_PATH, 'test-suite', 'tools', 'update-compat', 'run.sh') TEST_SUITE_PATHS = tuple(os.path.join(ROOT_PATH, 'test-suite', 'success', i) for i in ('CompatOldOldFlag.v', 'CompatOldFlag.v', 'CompatPreviousFlag.v', 'CompatCurrentFlag.v')) TEST_SUITE_DESCRIPTIONS = ('current-minus-three', 'current-minus-two', 'current-minus-one', 'current') @@ -30,6 +87,29 @@ def get_header(): HEADER = get_header() +def break_or_continue(): + msg = 'Press ENTER to continue, or Ctrl+C to break...' + try: + raw_input(msg) + except NameError: # we must be running python3 + input(msg) + +def maybe_git_add(local_path, suggest_add=True, **args): + if args['git_add']: + print("Running 'git add %s'..." % local_path) + retc = subprocess.call(['git', 'add', local_path], cwd=ROOT_PATH) + if retc is not None and retc != 0: + print('!!! Process returned code %d' % retc) + elif suggest_add: + print(r"!!! Don't forget to 'git add %s'!" % local_path) + +def maybe_git_rm(local_path, **args): + if args['git_add']: + print("Running 'git rm %s'..." % local_path) + retc = subprocess.call(['git', 'rm', local_path], cwd=ROOT_PATH) + if retc is not None and retc != 0: + print('!!! Process returned code %d' % retc) + def get_version(cur_version=None): if cur_version is not None: return cur_version with open(CONFIGURE_PATH, 'r') as f: @@ -72,11 +152,47 @@ def get_known_versions(): def get_new_versions(known_versions, **args): if args['cur_version'] in known_versions: assert(known_versions[-1] == args['cur_version']) - assert(len(known_versions) == args['number_of_compat_versions']) - return known_versions + known_versions = known_versions[:-1] assert(len(known_versions) >= args['number_of_old_versions']) return tuple(list(known_versions[-args['number_of_old_versions']:]) + [args['cur_version']]) +def print_diff(olds, news, numch=30): + for ch in range(min(len(olds), len(news))): + if olds[ch] != news[ch]: + print('Character %d differs:\nOld: %s\nNew: %s' % (ch, repr(olds[ch:][:numch]), repr(news[ch:][numch]))) + return + ch = min(len(olds), len(news)) + assert(len(olds) != len(news)) + print('Strings are different lengths:\nOld tail: %s\nNew tail: %s' % (repr(olds[ch:]), repr(news[ch:]))) + +def update_shebang_to_match(contents, new_contents, path): + contents_lines = contents.split('\n') + new_contents_lines = new_contents.split('\n') + if not (contents_lines[0].startswith('#!/') and contents_lines[0].endswith('bash')): + raise Exception('Unrecognized #! line in existing %s: %s' % (os.path.relpath(path, ROOT_PATH), repr(contents_lines[0]))) + if not (new_contents_lines[0].startswith('#!/') and new_contents_lines[0].endswith('bash')): + raise Exception('Unrecognized #! line in new %s: %s' % (os.path.relpath(path, ROOT_PATH), repr(new_contents_lines[0]))) + new_contents_lines[0] = contents_lines[0] + return '\n'.join(new_contents_lines) + +def update_if_changed(contents, new_contents, path, exn_string='%s changed!', suggest_add=False, pass_through_shebang=False, assert_unchanged=False, **args): + if contents is not None and pass_through_shebang: + new_contents = update_shebang_to_match(contents, new_contents, path) + if contents is None or contents != new_contents: + if not assert_unchanged: + print('Updating %s...' % os.path.relpath(path, ROOT_PATH)) + with open(path, 'w') as f: + f.write(new_contents) + maybe_git_add(os.path.relpath(path, ROOT_PATH), suggest_add=suggest_add, **args) + else: + if contents is not None: + print('Unexpected change:\nOld contents:\n%s\n\nNew contents:\n%s\n' % (contents, new_contents)) + print_diff(contents, new_contents) + raise Exception(exn_string % os.path.relpath(path, ROOT_PATH)) + +def update_file(new_contents, path, **args): + update_if_changed(None, new_contents, path, **args) + def update_compat_files(old_versions, new_versions, assert_unchanged=False, **args): for v in old_versions: if v not in new_versions: @@ -85,6 +201,7 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar print('Removing %s...' % compat_file) compat_path = os.path.join(ROOT_PATH, compat_file) os.rename(compat_path, compat_path + '.bak') + maybe_git_rm(compat_file, **args) else: raise Exception('%s exists!' % compat_file) for v, next_v in zip(new_versions, list(new_versions[1:]) + [None]): @@ -95,12 +212,7 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar contents = HEADER + (EXTRA_HEADER % v) if next_v is not None: contents += '\nRequire Export Coq.Compat.%s.\n' % version_name_to_compat_name(next_v, ext='') - if not assert_unchanged: - with open(compat_path, 'w') as f: - f.write(contents) - print(r"Don't forget to 'git add %s'!" % compat_file) - else: - raise Exception('%s does not exist!' % compat_file) + update_file(contents, compat_path, exn_string='%s does not exist!', assert_unchanged=assert_unchanged, **args) else: # print('Checking %s...' % compat_file) with open(compat_path, 'r') as f: @@ -116,12 +228,7 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar if not contents.startswith(header + '\n'): contents = contents.replace(header, header + '\n') contents = contents.replace(header, '%s\n%s' % (header, line)) - if not assert_unchanged: - print('Updating %s...' % compat_file) - with open(compat_path, 'w') as f: - f.write(contents) - else: - raise Exception('Compat file %s is missing line %s' % (compat_file, line)) + update_file(contents, compat_path, exn_string=('Compat file %%s is missing line %s' % line), assert_unchanged=assert_unchanged, **args) def update_compat_versions_type_line(new_versions, contents, relpath): compat_version_string = ' | '.join(['V%s_%s' % tuple(v.split('.')) for v in new_versions[:-1]] + ['Current']) @@ -173,11 +280,18 @@ def update_add_compat_require(new_versions, contents, relpath): return new_contents def update_parse_compat_version(new_versions, contents, relpath, **args): - line_count = args['number_of_compat_versions']+2 # 1 for the first line, 1 for the invalid flags + line_count = 3 # 1 for the first line, 1 for the invalid flags, and 1 for Current first_line = 'let parse_compat_version = let open Flags in function' - old_function_lines = contents[contents.index(first_line):].split('\n')[:line_count] - if re.match(r'^ \| \([0-9 "\.\|]*\) as s ->$', old_function_lines[-1]) is None: - raise Exception('Could not recognize line %d of parse_compat_version in %s as a list of invalid versions' % (line_count, relpath)) + split_contents = contents[contents.index(first_line):].split('\n') + while True: + cur_line = split_contents[:line_count][-1] + if re.match(r'^ \| \([0-9 "\.\|]*\) as s ->$', cur_line) is not None: + break + elif re.match(r'^ \| "[0-9\.]*" -> V[0-9_]*$', cur_line) is not None: + line_count += 1 + else: + raise Exception('Could not recognize line %d of parse_compat_version in %s as a list of invalid versions (line was %s)' % (line_count, relpath, repr(cur_line))) + old_function_lines = split_contents[:line_count] all_versions = re.findall(r'"([0-9\.]+)"', ''.join(old_function_lines)) invalid_versions = tuple(i for i in all_versions if i not in new_versions) new_function_lines = [first_line] @@ -197,15 +311,6 @@ def check_no_old_versions(old_versions, new_versions, contents, relpath): if V in contents: raise Exception('Unreplaced usage of %s remaining in %s' % (V, relpath)) -def update_if_changed(contents, new_contents, path, assert_unchanged=False, **args): - if contents != new_contents: - if not assert_unchanged: - print('Updating %s...' % os.path.relpath(path, ROOT_PATH)) - with open(path, 'w') as f: - f.write(new_contents) - else: - raise Exception('%s changed!' % os.path.relpath(path, ROOT_PATH)) - def update_flags_mli(old_versions, new_versions, **args): with open(FLAGS_MLI_PATH, 'r') as f: contents = f.read() new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH)) @@ -242,17 +347,20 @@ def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TES assert(len(new_versions) == len(test_suite_paths)) assert(len(new_versions) == len(test_suite_descriptions)) for i, (v, path, descr) in enumerate(zip(new_versions, test_suite_paths, test_suite_descriptions)): - if not os.path.exists(path): - raise Exception('Could not find existing file %s' % os.path.relpath(path, ROOT_PATH)) + contents = None + suggest_add = False + if os.path.exists(path): + with open(path, 'r') as f: contents = f.read() + else: + suggest_add = True if '%s' in descr: descr = descr % v - with open(path, 'r') as f: contents = f.read() lines = ['(* -*- coq-prog-args: ("-compat" "%s") -*- *)' % v, '(** Check that the %s compatibility flag actually requires the relevant modules. *)' % descr] for imp_v in reversed(new_versions[i:]): lines.append('Import Coq.Compat.%s.' % version_name_to_compat_name(imp_v, ext='')) lines.append('') new_contents = '\n'.join(lines) - update_if_changed(contents, new_contents, path, **args) + update_if_changed(contents, new_contents, path, suggest_add=suggest_add, **args) def update_doc_index(new_versions, **args): with open(DOC_INDEX_PATH, 'r') as f: contents = f.read() @@ -264,6 +372,20 @@ def update_doc_index(new_versions, **args): new_contents = new_contents.replace(firstline, '\n'.join([firstline] + extra_lines)) update_if_changed(contents, new_contents, DOC_INDEX_PATH, **args) +def update_test_suite_run(**args): + with open(TEST_SUITE_RUN_PATH, 'r') as f: contents = f.read() + new_contents = r'''#!/usr/bin/env bash + +# allow running this script from any directory by basing things on where the script lives +SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )" + +# we assume that the script lives in test-suite/tools/update-compat/, +# and that update-compat.py lives in dev/tools/ +cd "${SCRIPT_DIR}/../../.." +dev/tools/update-compat.py --assert-unchanged %s || exit $? +''' % ' '.join([('--master' if args['master'] else ''), ('--release' if args['release'] else '')]).strip() + update_if_changed(contents, new_contents, TEST_SUITE_RUN_PATH, pass_through_shebang=True, **args) + def update_bug_4789(new_versions, **args): # we always update this compat notation to oldest # currently-supported compat version, which should never be the @@ -305,11 +427,26 @@ def parse_args(argv): args = { 'assert_unchanged': False, 'cur_version': None, - 'number_of_old_versions': DEFAULT_NUMBER_OF_OLD_VERSIONS + 'number_of_old_versions': None, + 'master': False, + 'release': False, + 'git_add': False, } + if '--master' not in argv and '--release' not in argv: + print(r'''WARNING: You should pass either --release (sometime before branching) + or --master (right after branching and updating the version number in version.ml)''') + if '--assert-unchanged' not in args: break_or_continue() for arg in argv[1:]: if arg == '--assert-unchanged': args['assert_unchanged'] = True + elif arg == '--git-add': + args['git_add'] = True + elif arg == '--master': + args['master'] = True + if args['number_of_old_versions'] is None: args['number_of_old_versions'] = MASTER_NUMBER_OF_OLD_VERSIONS + elif arg == '--release': + args['release'] = True + if args['number_of_old_versions'] is None: args['number_of_old_versions'] = RELEASE_NUMBER_OF_OLD_VERSIONS elif arg.startswith('--cur-version='): args['cur_version'] = arg[len('--cur-version='):] assert(len(args['cur_version'].split('.')) == 2) @@ -317,10 +454,11 @@ def parse_args(argv): elif arg.startswith('--number-of-old-versions='): args['number_of_old_versions'] = int(arg[len('--number-of-old-versions='):]) else: - print('USAGE: %s [--assert-unchanged] [--cur-version=NN.NN] [--number-of-old-versions=NN]' % argv[0]) + print('USAGE: %s [--assert-unchanged] [--cur-version=NN.NN] [--number-of-old-versions=NN] [--git-add]' % argv[0]) print('') print('ERROR: Unrecognized argument: %s' % arg) sys.exit(1) + if args['number_of_old_versions'] is None: args['number_of_old_versions'] = DEFAULT_NUMBER_OF_OLD_VERSIONS return args if __name__ == '__main__': @@ -335,6 +473,7 @@ if __name__ == '__main__': update_compat_files(known_versions, new_versions, **args) update_flags(known_versions, new_versions, **args) update_test_suite(new_versions, **args) + update_test_suite_run(**args) update_doc_index(new_versions, **args) update_bug_4789(new_versions, **args) update_compat_notations(known_versions, new_versions, **args) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index d0e44cd212..50a56f1d51 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -234,7 +234,8 @@ Primitive Projections extended the Calculus of Inductive Constructions with a new binary term constructor `r.(p)` representing a primitive projection `p` applied to a record object `r` (i.e., primitive projections are always applied). - Even if the record type has parameters, these do not appear at + Even if the record type has parameters, these do not appear + in the internal representation of applications of the projection, considerably reducing the sizes of terms when manipulating parameterized records and type checking time. On the user level, primitive projections can be used as a replacement diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 3629b5c5ec..442077616f 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -41,32 +41,36 @@ mode but it can also be used in toplevel definitions as shown below. .. note:: - - The infix tacticals “… \|\| …”, “… + …”, and “… ; …” are associative. + - The infix tacticals ``… || …`` , ``… + …`` , and ``… ; …`` are associative. - - In :token:`tacarg`, there is an overlap between qualid as a direct tactic - argument and :token:`qualid` as a particular case of term. The resolution is - done by first looking for a reference of the tactic language and if - it fails, for a reference to a term. To force the resolution as a - reference of the tactic language, use the form :g:`ltac:(@qualid)`. To - force the resolution as a reference to a term, use the syntax - :g:`(@qualid)`. + .. example:: - - As shown by the figure, tactical ``\|\|`` binds more than the prefix - tacticals try, repeat, do and abstract which themselves bind more - than the postfix tactical “… ;[ … ]” which binds more than “… ; …”. + If you want that :n:`@tactic__2; @tactic__3` be fully run on the first + subgoal generated by :n:`@tactic__1`, before running on the other + subgoals, then you should not write + :n:`@tactic__1; (@tactic__2; @tactic__3)` but rather + :n:`@tactic__1; [> @tactic__2; @tactic__3 .. ]`. - For instance + - In :token:`tacarg`, there is an overlap between :token:`qualid` as a + direct tactic argument and :token:`qualid` as a particular case of + :token:`term`. The resolution is done by first looking for a reference + of the tactic language and if it fails, for a reference to a term. + To force the resolution as a reference of the tactic language, use the + form :n:`ltac:(@qualid)`. To force the resolution as a reference to a + term, use the syntax :n:`(@qualid)`. - .. coqtop:: in + - As shown by the figure, tactical ``… || …`` binds more than the prefix + tacticals :tacn:`try`, :tacn:`repeat`, :tacn:`do` and :tacn:`abstract` + which themselves bind more than the postfix tactical ``… ;[ … ]`` + which binds at the same level as ``… ; …`` . - try repeat tac1 || tac2; tac3; [tac31 | ... | tac3n]; tac4. + .. example:: - is understood as + :n:`try repeat @tactic__1 || @tactic__2; @tactic__3; [ {+| @tactic } ]; @tactic__4` - .. coqtop:: in + is understood as: - try (repeat (tac1 || tac2)); - ((tac3; [tac31 | ... | tac3n]); tac4). + :n:`((try (repeat (@tactic__1 || @tactic__2)); @tactic__3); [ {+| @tactic } ]); @tactic__4` .. productionlist:: coq expr : `expr` ; `expr` diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 92bd4dbd1d..483dbd311d 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1445,6 +1445,16 @@ section constant. If tactic is ``move`` or ``case`` and an equation :token:`ident` is given, then clear (step 3) for :token:`d_item` is suppressed (see section :ref:`generation_of_equations_ssr`). +Intro patterns (see section :ref:`introduction_ssr`) +and the ``rewrite`` tactic (see section :ref:`rewriting_ssr`) +let one place a :token:`clear_switch` in the middle of other items +(namely identifiers, views and rewrite rules). This can trigger the +addition of proof context items to the ones being explicitly +cleared, and in turn this can result in clear errors (e.g. if the +context item automatically added occurs in the goal). The +relevant sections describe ways to avoid the unintended clear of +context items. + Matching for apply and exact ```````````````````````````` @@ -1572,6 +1582,9 @@ The :token:`i_pattern`\s can be seen as a variant of *intro patterns* (see :tacn:`intros`:) each performs an introduction operation, i.e., pops some variables or assumptions from the goal. +Simplification items +````````````````````` + An :token:`s_item` can simplify the set of subgoals or the subgoals themselves: + ``//`` removes all the “trivial” subgoals that can be resolved by the @@ -1583,18 +1596,32 @@ An :token:`s_item` can simplify the set of subgoals or the subgoals themselves: ``/= //``, i.e., ``simpl; try done``. -When an :token:`s_item` bears a :token:`clear_switch`, then the +When an :token:`s_item` immediately precedes a :token:`clear_switch`, then the :token:`clear_switch` is executed *after* the :token:`s_item`, e.g., ``{IHn}//`` will solve some subgoals, possibly using the fact ``IHn``, and will erase ``IHn`` from the context of the remaining subgoals. +Views +````` + The first entry in the :token:`i_view` grammar rule, :n:`/@term`, represents a view (see section :ref:`views_and_reflection_ssr`). It interprets the top of the stack with the view :token:`term`. -It is equivalent to ``move/term``. The optional flag ``{}`` can -be used to signal that the :token:`term`, when it is a context entry, -has to be cleared. +It is equivalent to :n:`move/@term`. + +A :token:`clear_switch` that immediately precedes an :token:`i_view` +is complemented with the name of the view if an only if the :token:`i_view` +is a simple proof context entry [#10]_. +E.g. ``{}/v`` is equivalent to ``/v{v}``. +This behavior can be avoided by separating the :token:`clear_switch` +from the :token:`i_view` with the ``-`` intro pattern or by putting +parentheses around the view. + +A :token:`clear_switch` that immediately precedes an :token:`i_view` +is executed after the view application. + + If the next :token:`i_item` is a view, then the view is applied to the assumption in top position once all the previous :token:`i_item` have been performed. @@ -1608,6 +1635,9 @@ Notations can be used to name tactics, for example:: lets one write just ``/myop`` in the intro pattern. Note the scope annotation: views are interpreted opening the ``ssripat`` scope. +Intro patterns +`````````````` + |SSR| supports the following :token:`i_pattern`\s: :token:`ident` @@ -1615,6 +1645,13 @@ annotation: views are interpreted opening the ``ssripat`` scope. a new constant, fact, or defined constant :token:`ident`, respectively. Note that defined constants cannot be introduced when δ-expansion is required to expose the top variable or assumption. + A :token:`clear_switch` (even an empty one) immediately preceding an + :token:`ident` is complemented with that :token:`ident` if and only if + the identifier is a simple proof context entry [#10]_. + As a consequence by prefixing the + :token:`ident` with ``{}`` one can *replace* a context entry. + This behavior can be avoided by separating the :token:`clear_switch` + from the :token:`ident` with the ``-`` intro pattern. ``>`` pops every variable occurring in the rest of the stack. Type class instances are popped even if they don't occur @@ -1708,6 +1745,9 @@ annotation: views are interpreted opening the ``ssripat`` scope. Note that |SSR| does not support the syntax ``(ipat, …, ipat)`` for destructing intro-patterns. +Clear switch +```````````` + Clears are deferred until the end of the intro pattern. .. example:: @@ -1730,6 +1770,9 @@ is performed behind the scenes. Facts mentioned in a clear switch must be valid names in the proof context (excluding the section context). +Branching and destructuring +``````````````````````````` + The rules for interpreting branching and destructing :token:`i_pattern` are motivated by the fact that it would be pointless to have a branching pattern if tactic is a ``move``, and in most of the remaining cases @@ -1754,6 +1797,9 @@ interpretation, e.g.: are all equivalent. +Block introduction +`````````````````` + |SSR| supports the following :token:`i_block`\s: :n:`[^ @ident ]` @@ -3030,13 +3076,22 @@ operation should be performed: pattern. In its simplest form, it is a regular term. If no explicit redex switch is present the rewrite pattern to be matched is inferred from the :token:`r_item`. -+ This optional term, or the :token:`r_item`, may be preceded by an occurrence - switch (see section :ref:`selectors_ssr`) or a clear item - (see section :ref:`discharge_ssr`), - these two possibilities being exclusive. An occurrence switch selects ++ This optional term, or the :token:`r_item`, may be preceded by an + :token:`occ_switch` (see section :ref:`selectors_ssr`) or a + :token:`clear_switch` (see section :ref:`discharge_ssr`), + these two possibilities being exclusive. + + An occurrence switch selects the occurrences of the rewrite pattern which should be affected by the rewrite operation. + A clear switch, even an empty one, is performed *after* the + :token:`r_item` is actually processed and is complemented with the name of + the rewrite rule if an only if it is a simple proof context entry [#10]_. + As a consequence one can + write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately + afterwards. + This behavior can be avoided by putting parentheses around the rewrite rule. An :token:`r_item` can be: @@ -3291,10 +3346,6 @@ the rewrite tactic. The effect of the tactic on the initial goal is to rewrite this lemma at the second occurrence of the first matching ``x + y + 0`` of the explicit rewrite redex ``_ + y + 0``. -An empty occurrence switch ``{}`` is not interpreted as a valid occurrence -switch. It has the effect of clearing the :token:`r_item` (when it is the name -of a context entry). - Occurrence selection and repetition ``````````````````````````````````` @@ -5520,3 +5571,5 @@ Settings in the metatheory .. [#9] The current state of the proof shall be displayed by the Show Proof command of |Coq| proof mode. +.. [#10] A simple proof context entry is a naked identifier (i.e. not between + parentheses) designating a context entry that is not a section variable. diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 51f94d7e5a..c33df52038 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -618,5 +618,6 @@ through the <tt>Require Import</tt> command.</p> theories/Compat/Coq87.v theories/Compat/Coq88.v theories/Compat/Coq89.v + theories/Compat/Coq810.v </dd> </dl> diff --git a/ide/fake_ide.ml b/ide/fake_ide.ml index 8b0c736f50..4e26cb6095 100644 --- a/ide/fake_ide.ml +++ b/ide/fake_ide.ml @@ -241,6 +241,9 @@ let eval_print l coq = | [ Tok(_,"ADD"); Top [Tok(_,name)]; Tok(_,phrase) ] -> let eid, tip = add_sentence ~name phrase in after_add (base_eval_call (add ((phrase,eid),(tip,true))) coq) + | [ Tok(_,"FAILADD"); Tok(_,phrase) ] -> + let eid, tip = add_sentence phrase in + after_fail coq (base_eval_call ~fail:false (add ((phrase,eid),(tip,true))) coq) | [ Tok(_,"GOALS"); ] -> eval_call (goals ()) coq | [ Tok(_,"FAILGOALS"); ] -> @@ -267,7 +270,8 @@ let eval_print l coq = prerr_endline "Quitting fake_ide"; exit 0 | Tok("#[^\n]*",_) :: _ -> () - | _ -> error "syntax error" + | Tok(s,_) :: _ -> error ("syntax error at " ^ s) + | _ -> error ("syntax error") let grammar = let open Parser in @@ -275,6 +279,7 @@ let grammar = let eat_phrase = eat_balanced '{' in Alt [ Seq [Item (eat_rex "ADD"); Opt (Item eat_id); Item eat_phrase] + ; Seq [Item (eat_rex "FAILADD"); Item eat_phrase] ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id] ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase] ; Seq [Item (eat_rex "WAIT")] diff --git a/ide/idetop.ml b/ide/idetop.ml index 716a942d5c..205f4455a3 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -64,11 +64,19 @@ let is_known_option cmd = match Vernacprop.under_control cmd with (** Check whether a command is forbidden in the IDE *) -let ide_cmd_checks ~id {CAst.loc;v=ast} = - let user_error s = CErrors.user_err ?loc ~hdr:"IDE" (str s) in - let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in +let ide_cmd_checks ~last_valid {CAst.loc;v=ast} = + let user_error s = + try CErrors.user_err ?loc ~hdr:"IDE" (str s) + with e -> + let (e, info) = CErrors.push e in + let info = Stateid.add info ~valid:last_valid Stateid.dummy in + Exninfo.raise ~info e + in if is_debug ast then - user_error "Debug mode not available in the IDE"; + user_error "Debug mode not available in the IDE" + +let ide_cmd_warns ~id {CAst.loc;v=ast} = + let warn msg = Feedback.(feedback ~id (Message (Warning, loc, strbrk msg))) in if is_known_option ast then warn "Set this option from the IDE menu instead"; if is_navigation_vernac ast || is_undo ast then @@ -83,11 +91,15 @@ let set_doc doc = ide_doc := Some doc let add ((s,eid),(sid,verbose)) = let doc = get_doc () in let pa = Pcoq.Parsable.make (Stream.of_string s) in - let loc_ast = Stm.parse_sentence ~doc sid pa in + match Stm.parse_sentence ~doc sid ~entry:Pvernac.main_entry pa with + | None -> assert false (* s is not an empty string *) + | Some (loc, ast) -> + let loc_ast = CAst.make ~loc ast in + ide_cmd_checks ~last_valid:sid loc_ast; let doc, newid, rc = Stm.add ~doc ~ontop:sid verbose loc_ast in set_doc doc; let rc = match rc with `NewTip -> CSig.Inl () | `Unfocus id -> CSig.Inr id in - ide_cmd_checks ~id:newid loc_ast; + ide_cmd_warns ~id:newid loc_ast; (* TODO: the "" parameter is a leftover of the times the protocol * used to include stderr/stdout output. * @@ -121,10 +133,10 @@ let query (route, (s,id)) = let annotate phrase = let doc = get_doc () in - let {CAst.loc;v=ast} = - let pa = Pcoq.Parsable.make (Stream.of_string phrase) in - Stm.parse_sentence ~doc (Stm.get_current_state ~doc) pa - in + let pa = Pcoq.Parsable.make (Stream.of_string phrase) in + match Stm.parse_sentence ~doc (Stm.get_current_state ~doc) ~entry:Pvernac.main_entry pa with + | None -> Richpp.richpp_of_pp 78 (Pp.mt ()) + | Some (_, ast) -> (* XXX: Width should be a parameter of annotate... *) Richpp.richpp_of_pp 78 (Ppvernac.pr_vernac ast) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 444ac5ab6d..13078840ef 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -625,8 +625,13 @@ let explicitize inctx impl (cf,f) args = CApp ((ip,f),args1@args2) | None -> let args = exprec 1 (args,impl) in - if List.is_empty args then f.CAst.v else CApp ((None, f), args) - in + if List.is_empty args then f.CAst.v else + match f.CAst.v with + | CApp (g,args') -> + (* may happen with notations for a prefix of an n-ary + application *) + CApp (g,args'@args) + | _ -> CApp ((None, f), args) in try expl () with Expl -> let f',us = match f with { CAst.v = CRef (f,us) } -> f,us | _ -> assert false in diff --git a/lib/flags.ml b/lib/flags.ml index ae4d337ded..55bfa3cbde 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -66,7 +66,7 @@ let we_are_parsing = ref false (* Current means no particular compatibility consideration. For correct comparisons, this constructor should remain the last one. *) -type compat_version = V8_7 | V8_8 | Current +type compat_version = V8_7 | V8_8 | V8_9 | Current let compat_version = ref Current @@ -77,6 +77,9 @@ let version_compare v1 v2 = match v1, v2 with | V8_8, V8_8 -> 0 | V8_8, _ -> -1 | _, V8_8 -> 1 + | V8_9, V8_9 -> 0 + | V8_9, _ -> -1 + | _, V8_9 -> 1 | Current, Current -> 0 let version_strictly_greater v = version_compare !compat_version v > 0 @@ -85,6 +88,7 @@ let version_less_or_equal v = not (version_strictly_greater v) let pr_version = function | V8_7 -> "8.7" | V8_8 -> "8.8" + | V8_9 -> "8.9" | Current -> "current" (* Translate *) diff --git a/lib/flags.mli b/lib/flags.mli index d883cf1e30..7336b9beaf 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -58,7 +58,7 @@ val we_are_parsing : bool ref (* Set Printing All flag. For some reason it is a global flag *) val raw_print : bool ref -type compat_version = V8_7 | V8_8 | Current +type compat_version = V8_7 | V8_8 | V8_9 | Current val compat_version : compat_version ref val version_compare : compat_version -> compat_version -> int val version_strictly_greater : compat_version -> bool diff --git a/lib/stateid.ml b/lib/stateid.ml index 5485c4bf19..8f45f3605d 100644 --- a/lib/stateid.ml +++ b/lib/stateid.ml @@ -27,6 +27,8 @@ let get exn = Exninfo.get exn state_id_info let equal = Int.equal let compare = Int.compare +let print id = Pp.int id + module Self = struct type t = int let compare = compare diff --git a/lib/stateid.mli b/lib/stateid.mli index 5d4b71a354..f6ce7ddc40 100644 --- a/lib/stateid.mli +++ b/lib/stateid.mli @@ -20,6 +20,7 @@ val initial : t val dummy : t val fresh : unit -> t val to_string : t -> string +val print : t -> Pp.t val of_int : int -> t val to_int : t -> int diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 19ae97da77..759e60fbca 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -439,7 +439,6 @@ module Module = let module_expr = Entry.create "module_expr" let module_type = Entry.create "module_type" end - let epsilon_value f e = let r = G.production (G.r_next G.r_stop (symbol_of_prod_entry_key e), (fun x _ -> f x)) in let ext = [None, None, [r]] in diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 352857d4cd..3203a25b46 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -41,6 +41,16 @@ end - static rules explicitly defined in files g_*.ml4 - static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and VERNAC EXTEND (see e.g. file extratactics.ml4) + + Note that parsing a Coq document is in essence stateful: the parser + needs to recognize commands that start proofs and use a different + parsing entry point for them. + + We thus provide two different interfaces: the "raw" parsing + interface, in the style of camlp5, which provides more flexibility, + and a more specialize "parse_vernac" one, which will indeed adjust + the state as needed. + *) (** Dynamic extension of rules @@ -269,3 +279,7 @@ type any_entry = AnyEntry : 'a Entry.t -> any_entry val register_grammars_by_name : string -> any_entry list -> unit val find_grammars_by_name : string -> any_entry list + +(** Parsing state handling *) +val freeze : marshallable:bool -> frozen_t +val unfreeze : frozen_t -> unit diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index df4b647642..0cdf8fb5d8 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -18,7 +18,7 @@ DECLARE PLUGIN "derive_plugin" { -let classify_derive_command _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) +let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]),VtLater) } diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg index 8f0440a2a4..c4f8843e51 100644 --- a/plugins/funind/g_indfun.mlg +++ b/plugins/funind/g_indfun.mlg @@ -186,7 +186,7 @@ VERNAC COMMAND EXTEND Function (Vernacexpr.(VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)))) with | Vernacextend.VtSideff ids, _ when hard -> - Vernacextend.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) + Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater) | x -> x } -> { do_generate_principle false (List.map snd recsl) } END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index d9b19c1ae6..4c24f51b1e 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -58,15 +58,8 @@ let new_entry name = let toplevel_selector = new_entry "vernac:toplevel_selector" let tacdef_body = new_entry "tactic:tacdef_body" -(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for - proof editing and changes nothing else). Then sets it as the default proof mode. *) -let _ = - let mode = { - Proof_global.name = "Classic"; - set = (fun () -> Pvernac.set_command_entry tactic_mode); - reset = (fun () -> Pvernac.(set_command_entry noedit_mode)); - } in - Proof_global.register_proof_mode mode +(* Registers [tactic_mode] as a parser for proof editing *) +let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode (* Hack to parse "[ id" without dropping [ *) let test_bracket_ident = diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg index 1ea6ff84d4..cdee012a82 100644 --- a/plugins/ltac/g_obligations.mlg +++ b/plugins/ltac/g_obligations.mlg @@ -83,7 +83,7 @@ open Obligations let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac -let classify_obbl _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) +let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater) } diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 31fb1c9abf..db8d1b20d8 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -285,13 +285,13 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF add_morphism_infer atts m n; } | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater } + => { VtStartProof(GuaranteesOpacity,[n]), VtLater } -> { add_morphism atts [] m s n; } | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater } + => { VtStartProof(GuaranteesOpacity,[n]), VtLater } -> { add_morphism atts binders m s n; } diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index dd2c2d0ba4..9ce9250a43 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -67,7 +67,7 @@ type ssrview = ast_closure_term list type id_block = Prefix of Id.t | SuffixId of Id.t | SuffixNum of int (* Only [One] forces an introduction, possibly reducing the goal. *) -type anon_iter = +type anon_kind = | One of string option (* name hint *) | Drop | All @@ -76,25 +76,23 @@ type anon_iter = type ssripat = | IPatNoop | IPatId of Id.t - | IPatAnon of anon_iter (* inaccessible name *) -(* TODO | IPatClearMark *) - | IPatDispatch of bool (* ssr exception: accept a dispatch on the empty list even when there are subgoals *) * ssripatss_or_block (* (..|..) *) - | IPatCase of (* ipats_mod option * *) ssripatss_or_block (* this is not equivalent to /case /[..|..] if there are already multiple goals *) + | IPatAnon of anon_kind (* inaccessible name *) + | IPatDispatch of ssripatss_or_block (* (..|..) *) + | IPatCase of ssripatss_or_block (* [..|..] *) | IPatInj of ssripatss | IPatRewrite of (*occurrence option * rewrite_pattern **) ssrocc * ssrdir - | IPatView of bool * ssrview (* {}/view (true if the clear is present) *) + | IPatView of ssrview (* /view *) | IPatClear of ssrclear (* {H1 H2} *) | IPatSimpl of ssrsimpl | IPatAbstractVars of Id.t list | IPatFastNondep - | IPatEqGen of unit Proofview.tactic (* internal use: generation of eqn *) and ssripats = ssripat list and ssripatss = ssripats list and ssripatss_or_block = | Block of id_block | Regular of ssripats list -type ssrhpats = ((ssrclear * ssripats) * ssripats) * ssripats +type ssrhpats = ((ssrclear option * ssripats) * ssripats) * ssripats type ssrhpats_wtransp = bool * ssrhpats (* tac => inpats *) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 311d912efd..c3b9bde9b8 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -66,7 +66,7 @@ let check_hyp_exists hyps (SsrHyp(_, id)) = try ignore(Context.Named.lookup id hyps) with Not_found -> errorstrm Pp.(str"No assumption is named " ++ Id.print id) -let test_hypname_exists hyps id = +let test_hyp_exists hyps (SsrHyp(_, id)) = try ignore(Context.Named.lookup id hyps); true with Not_found -> false diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 51116ccd75..e642b5e788 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -29,7 +29,7 @@ val allocc : ssrocc val hyp_id : ssrhyp -> Id.t val hyps_ids : ssrhyps -> Id.t list val check_hyp_exists : ('a, 'b) Context.Named.pt -> ssrhyp -> unit -val test_hypname_exists : ('a, 'b) Context.Named.pt -> Id.t -> bool +val test_hyp_exists : ('a, 'b) Context.Named.pt -> ssrhyp -> bool val check_hyps_uniq : Id.t list -> ssrhyps -> unit val not_section_id : Id.t -> bool val hyp_err : ?loc:Loc.t -> string -> Id.t -> 'a diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 257ecd2a85..8c1363020a 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -94,17 +94,23 @@ let basecuttac name c gl = let introstac ipats = Proofview.V82.of_tactic (tclIPAT ipats) let havetac ist - (transp,((((clr, pats), binders), simpl), (((fk, _), t), hint))) + (transp,((((clr, orig_pats), binders), simpl), (((fk, _), t), hint))) suff namefst gl = let concl = pf_concl gl in + let pats = tclCompileIPats orig_pats in + let binders = tclCompileIPats binders in + let simpl = tclCompileIPats simpl in let skols, pats = - List.partition (function IPatAbstractVars _ -> true | _ -> false) pats in + List.partition (function IOpAbstractVars _ -> true | _ -> false) pats in let itac_mkabs = introstac skols in - let itac_c = introstac (IPatClear clr :: pats) in + let itac_c, clr = + match clr with + | None -> introstac pats, [] + | Some clr -> introstac (tclCompileIPats (IPatClear clr :: orig_pats)), clr in let itac, id, clr = introstac pats, Tacticals.tclIDTAC, old_cleartac clr in let binderstac n = - let rec aux = function 0 -> [] | n -> IPatAnon (One None) :: aux (n-1) in + let rec aux = function 0 -> [] | n -> IOpInaccessible None :: aux (n-1) in Tacticals.tclTHEN (if binders <> [] then introstac (aux n) else Tacticals.tclIDTAC) (introstac binders) in let simpltac = introstac simpl in @@ -160,7 +166,7 @@ let havetac ist gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c | FwdHave, false, false -> let skols = List.flatten (List.map (function - | IPatAbstractVars ids -> ids + | IOpAbstractVars ids -> ids | _ -> assert false) skols) in let skols_args = List.map (fun id -> Ssripats.Internal.examine_abstract (EConstr.mkVar id) gl) skols in @@ -203,10 +209,12 @@ let destProd_or_LetIn sigma c = | _ -> raise DestKO let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = + let clr0 = Option.default [] clr0 in + let pats = tclCompileIPats pats in let mkabs gen = abs_wgen false (fun x -> x) gen in let mkclr gen clrs = clr_of_wgen gen clrs in let mkpats = function - | _, Some ((x, _), _) -> fun pats -> IPatId (hoi_id x) :: pats + | _, Some ((x, _), _) -> fun pats -> IOpId (hoi_id x) :: pats | _ -> fun x -> x in let ct = match Ssrcommon.ssrterm_of_ast_closure_term ct with | (a, (b, Some ct)) -> @@ -265,7 +273,7 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = if gens = [] then errorstrm(str"gen have requires some generalizations"); let clear0 = old_cleartac clr0 in let id, name_general_hyp, cleanup, pats = match id, pats with - | None, (IPatId id as ip)::pats -> Some id, tacipat [ip], clear0, pats + | None, (IOpId id as ip)::pats -> Some id, tacipat [ip], clear0, pats | None, _ -> None, Tacticals.tclIDTAC, clear0, pats | Some (Some id),_ -> Some id, introid id, clear0, pats | Some _,_ -> @@ -289,6 +297,10 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl = (** The "suffice" tactic *) let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) = + let clr = Option.default [] clr in + let pats = tclCompileIPats pats in + let binders = tclCompileIPats binders in + let simpl = tclCompileIPats simpl in let htac = Tacticals.tclTHEN (introstac pats) (hinttac ist true hint) in let c = match Ssrcommon.ssrterm_of_ast_closure_term c with | (a, (b, Some ct)) -> diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli index 8a05e25504..35e89dbcea 100644 --- a/plugins/ssr/ssrfwd.mli +++ b/plugins/ssr/ssrfwd.mli @@ -22,7 +22,7 @@ val ssrposetac : Id.t * (ssrfwdfmt * ast_closure_term) -> v82tac val havetac : ist -> bool * - ((((Ssrast.ssrclear * Ssrast.ssripat list) * Ssrast.ssripats) * + ((((Ssrast.ssrclear option * Ssrast.ssripat list) * Ssrast.ssripats) * Ssrast.ssripats) * (((Ssrast.ssrfwdkind * 'a) * ast_closure_term) * (bool * Tacinterp.Value.t option list))) -> @@ -35,7 +35,7 @@ val basecuttac : val wlogtac : Ltac_plugin.Tacinterp.interp_sign -> - ((Ssrast.ssrhyps * Ssrast.ssripats) * 'a) * 'b -> + ((Ssrast.ssrclear option * Ssrast.ssripats) * 'a) * 'b -> (Ssrast.ssrhyps * ((Ssrast.ssrhyp_or_id * string) * Ssrmatching_plugin.Ssrmatching.cpattern option) @@ -50,7 +50,7 @@ val wlogtac : val sufftac : Ssrast.ist -> - (((Ssrast.ssrhyps * Ssrast.ssripats) * Ssrast.ssripat list) * + (((Ssrast.ssrclear option * Ssrast.ssripats) * Ssrast.ssripat list) * Ssrast.ssripat list) * (('a * ast_closure_term) * diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index ce81d83661..a8dfd69240 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -19,14 +19,78 @@ open Proofview.Notations open Ssrast +type ssriop = + | IOpId of Names.Id.t + | IOpDrop + | IOpTemporay + | IOpInaccessible of string option + | IOpInaccessibleAll + | IOpAbstractVars of Names.Id.t list + | IOpFastNondep + + | IOpInj of ssriops list + + | IOpDispatchBlock of id_block + | IOpDispatchBranches of ssriops list + + | IOpCaseBlock of id_block + | IOpCaseBranches of ssriops list + + | IOpRewrite of ssrocc * ssrdir + | IOpView of ssrclear option * ssrview (* extra clears to be performed *) + + | IOpClear of ssrclear * ssrhyp option (* must clear, may clear *) + | IOpSimpl of ssrsimpl + + | IOpEqGen of unit Proofview.tactic (* generation of eqn *) + + | IOpNoop + +and ssriops = ssriop list + +let rec pr_ipatop = function + | IOpId id -> Names.Id.print id + | IOpDrop -> Pp.str "_" + | IOpTemporay -> Pp.str "+" + | IOpInaccessible None -> Pp.str "?" + | IOpInaccessible (Some s) -> Pp.str ("?«"^s^"»") + | IOpInaccessibleAll -> Pp.str "*" + | IOpAbstractVars l -> Pp.str ("[:"^String.concat " " (List.map Names.Id.to_string l)^"]") + | IOpFastNondep -> Pp.str ">" + + | IOpInj l -> Pp.(str "[=" ++ ppl l ++ str "]") + + | IOpDispatchBlock b -> Pp.(str"(" ++ Ssrprinters.pr_block b ++ str")") + | IOpDispatchBranches l -> Pp.(str "(" ++ ppl l ++ str ")") + + | IOpCaseBlock b -> Pp.(str"[" ++ Ssrprinters.pr_block b ++ str"]") + | IOpCaseBranches l -> Pp.(str "[" ++ ppl l ++ str "]") + + | IOpRewrite (occ,dir) -> Pp.(Ssrprinters.(pr_occ occ ++ pr_dir dir)) + | IOpView (None,vs) -> Pp.(prlist_with_sep mt (fun c -> str "/" ++ Ssrprinters.pr_ast_closure_term c) vs) + | IOpView (Some cl,vs) -> Pp.(Ssrprinters.pr_clear Pp.spc cl ++ prlist_with_sep mt (fun c -> str "/" ++ Ssrprinters.pr_ast_closure_term c) vs) + + | IOpClear (clmust,clmay) -> + Pp.(Ssrprinters.pr_clear spc clmust ++ + match clmay with + | Some cl -> str "(try " ++ Ssrprinters.pr_clear spc [cl] ++ str")" + | None -> mt ()) + | IOpSimpl s -> Ssrprinters.pr_simpl s + + | IOpEqGen _ -> Pp.str "E:" + | IOpNoop -> Pp.str"-" +and ppl x = Pp.(prlist_with_sep (fun () -> str"|") (prlist_with_sep spc pr_ipatop)) x + + module IpatMachine : sig (* the => tactical. ?eqtac is a tactic to be eventually run * after the first [..] block. first_case_is_dispatch is the * ssr exception to elim: and case: *) val main : ?eqtac:unit tactic -> first_case_is_dispatch:bool -> - ssripats -> unit tactic + ssriops -> unit tactic + val tclCompileIPats : ssripats -> ssriops val tclSEED_SUBGOALS : Names.Name.t list array -> unit tactic -> unit tactic @@ -53,7 +117,7 @@ module State : sig val isNSEED_CONSUME : (Names.Name.t list option -> unit tactic) -> unit tactic (* Some data may expire *) - val isTICK : ssripat -> unit tactic + val isTICK : ssriop -> unit tactic val isPRINT : Proofview.Goal.t -> Pp.t @@ -149,7 +213,7 @@ let isNSEED_CONSUME k = k x) let isTICK = function - | IPatSimpl _ | IPatClear _ -> tclUNIT () + | IOpSimpl _ | IOpClear _ -> tclUNIT () | _ -> tclGET (fun s -> tclSET { s with name_seed = None }) end (* }}} *************************************************************** *) @@ -238,6 +302,13 @@ let tacCHECK_HYPS_EXIST hyps = Goal.enter begin fun gl -> tclUNIT () end +let tacFILTER_HYP_EXIST hyps k = Goal.enter begin fun gl -> + let ctx = Goal.hyps gl in + k (Option.bind hyps (fun h -> + if Ssrcommon.test_hyp_exists ctx h && + Ssrcommon.(not_section_id (hyp_id h)) then Some h else None)) +end + (** [=> []] *****************************************************************) (* calls t1 then t2 on each subgoal passing to t2 the index of the current @@ -286,13 +357,13 @@ let tac_intro_seed interp_ipats fix = Goal.enter begin fun gl -> | Prefix id -> Id.to_string id ^ "?" | SuffixNum n -> "?" ^ string_of_int n | SuffixId id -> "?" ^ Id.to_string id in - IPatAnon (One (Some s)) + IOpInaccessible (Some s) | Name id -> let s = match fix with | Prefix fix -> Id.to_string fix ^ Id.to_string id | SuffixNum n -> Id.to_string id ^ string_of_int n | SuffixId fix -> Id.to_string id ^ Id.to_string fix in - IPatId (Id.of_string s)) seeds in + IOpId (Id.of_string s)) seeds in interp_ipats ipats end end @@ -342,7 +413,7 @@ let tclMK_ABSTRACT_VARS ids = (* Debugging *) let tclLOG p t = tclUNIT () >>= begin fun () -> - Ssrprinters.ppdebug (lazy Pp.(str "exec: " ++ Ssrprinters.pr_ipat p)); + Ssrprinters.ppdebug (lazy Pp.(str "exec: " ++ pr_ipatop p)); tclUNIT () end <*> Goal.enter begin fun g -> @@ -362,58 +433,74 @@ let tclLOG p t = let notTAC = tclUNIT false +let duplicate_clear = + CWarnings.create ~name:"duplicate-clear" ~category:"ssr" + (fun id -> Pp.(str "Duplicate clear of " ++ Id.print id)) + (* returns true if it was a tactic (eg /ltac:tactic) *) let rec ipat_tac1 ipat : bool tactic = match ipat with - | IPatView (clear_if_id,l) -> + | IOpView (glued_clear,l) -> + let clear_if_id, extra_clear = + match glued_clear with + | None -> false, [] + | Some x -> true, List.map Ssrcommon.hyp_id x in Ssrview.tclIPAT_VIEWS ~views:l ~clear_if_id - ~conclusion:(fun ~to_clear:clr -> intro_clear clr) + ~conclusion:(fun ~to_clear:clr -> + let inter = CList.intersect Id.equal clr extra_clear in + List.iter duplicate_clear inter; + let cl = CList.union Id.equal clr extra_clear in + intro_clear cl) - | IPatDispatch(true, Regular [[]]) -> - notTAC - | IPatDispatch(_, Regular ipatss) -> + | IOpDispatchBranches ipatss -> tclDISPATCH (List.map ipat_tac ipatss) <*> notTAC - | IPatDispatch(_,Block id_block) -> + | IOpDispatchBlock id_block -> tac_intro_seed ipat_tac id_block <*> notTAC - - | IPatId id -> Ssrcommon.tclINTRO_ID id <*> notTAC - | IPatFastNondep -> intro_anon_deps <*> notTAC - - | IPatCase (Block id_block) -> + | IOpCaseBlock id_block -> Ssrcommon.tclWITHTOP tac_case <*> tac_intro_seed ipat_tac id_block <*> notTAC - | IPatCase (Regular ipatss) -> + | IOpCaseBranches ipatss -> tclIORPAT (Ssrcommon.tclWITHTOP tac_case) ipatss <*> notTAC - | IPatInj ipatss -> + + | IOpId id -> Ssrcommon.tclINTRO_ID id <*> notTAC + | IOpFastNondep -> intro_anon_deps <*> notTAC + | IOpDrop -> intro_drop <*> notTAC + | IOpInaccessible seed -> Ssrcommon.tclINTRO_ANON ?seed () <*> notTAC + | IOpInaccessibleAll -> intro_anon_all <*> notTAC + | IOpTemporay -> intro_anon_temp <*> notTAC + + | IOpSimpl Nop -> assert false + + | IOpInj ipatss -> tclIORPAT (Ssrcommon.tclWITHTOP (fun t -> V82.tactic ~nf_evars:false (Ssrelim.perform_injection t))) ipatss <*> notTAC - | IPatAnon Drop -> intro_drop <*> notTAC - | IPatAnon (One seed) -> Ssrcommon.tclINTRO_ANON ?seed () <*> notTAC - | IPatAnon All -> intro_anon_all <*> notTAC - | IPatAnon Temporary -> intro_anon_temp <*> notTAC - - | IPatNoop -> notTAC - | IPatSimpl Nop -> notTAC - - | IPatClear ids -> - tacCHECK_HYPS_EXIST ids <*> - intro_clear (List.map Ssrcommon.hyp_id ids) <*> + | IOpClear (must,may) -> + tacCHECK_HYPS_EXIST must <*> + tacFILTER_HYP_EXIST may (fun may -> + let must = List.map Ssrcommon.hyp_id must in + let cl = Option.fold_left (fun cls (SsrHyp(_,id)) -> + if CList.mem_f Id.equal id cls then begin + duplicate_clear id; + cls + end else id :: cls) must may in + intro_clear cl) <*> notTAC - | IPatSimpl x -> + | IOpSimpl x -> V82.tactic ~nf_evars:false (Ssrequality.simpltac x) <*> notTAC - | IPatRewrite (occ,dir) -> + | IOpRewrite (occ,dir) -> Ssrcommon.tclWITHTOP (fun x -> V82.tactic ~nf_evars:false (Ssrequality.ipat_rewrite occ dir x)) <*> notTAC - | IPatAbstractVars ids -> tclMK_ABSTRACT_VARS ids <*> notTAC + | IOpAbstractVars ids -> tclMK_ABSTRACT_VARS ids <*> notTAC - | IPatEqGen t -> t <*> notTAC + | IOpEqGen t -> t <*> notTAC + | IOpNoop -> notTAC and ipat_tac pl : unit tactic = match pl with @@ -433,51 +520,88 @@ and tclIORPAT tac = function | p -> Tacticals.New.tclTHENS tac (List.map ipat_tac p) and ssr_exception is_on = function - | Some (IPatCase l) when is_on -> Some (IPatDispatch(true, l)) + | Some (IOpCaseBranches [[]]) when is_on -> Some IOpNoop + | Some (IOpCaseBranches l) when is_on -> + Some (IOpDispatchBranches l) + | Some (IOpCaseBlock s) when is_on -> + Some (IOpDispatchBlock s) | x -> x and option_to_list = function None -> [] | Some x -> [x] and split_at_first_case ipats = let rec loop acc = function - | (IPatSimpl _ | IPatClear _) as x :: rest -> loop (x :: acc) rest - | (IPatCase _ | IPatDispatch _) as x :: xs -> CList.rev acc, Some x, xs + | (IOpSimpl _ | IOpClear _) as x :: rest -> loop (x :: acc) rest + | (IOpCaseBlock _ | IOpCaseBranches _ + | IOpDispatchBlock _ | IOpDispatchBranches _) as x :: xs -> + CList.rev acc, Some x, xs | pats -> CList.rev acc, None, pats in loop [] ipats ;; (* Simple pass doing {x}/v -> /v{x} *) -let elaborate_ipats l = +let tclCompileIPats l = let rec elab = function + + | (IPatClear cl) :: (IPatView v) :: rest -> + (IOpView(Some cl,v)) :: elab rest + | (IPatClear cl) :: (IPatId id) :: rest -> + (IOpClear (cl,Some (SsrHyp(None,id)))) :: IOpId id :: elab rest + + (* boring code *) | [] -> [] - | (IPatClear _ as p1) :: (IPatView _ as p2) :: rest -> p2 :: p1 :: elab rest - | IPatDispatch(s, Regular p) :: rest -> IPatDispatch (s, Regular (List.map elab p)) :: elab rest - | IPatCase (Regular p) :: rest -> IPatCase (Regular (List.map elab p)) :: elab rest - | IPatInj p :: rest -> IPatInj (List.map elab p) :: elab rest - | (IPatEqGen _ | IPatId _ | IPatSimpl _ | IPatClear _ | IPatFastNondep | - IPatAnon _ | IPatView _ | IPatNoop | IPatRewrite _ | - IPatAbstractVars _ | IPatDispatch(_, Block _) | IPatCase(Block _)) as x :: rest -> x :: elab rest - in - elab l -let main ?eqtac ~first_case_is_dispatch ipats = - let ipats = elaborate_ipats ipats in - let ip_before, case, ip_after = split_at_first_case ipats in + | IPatId id :: rest -> IOpId id :: elab rest + | IPatAnon (One hint) ::rest -> IOpInaccessible hint :: elab rest + | IPatAnon Drop :: rest -> IOpDrop :: elab rest + | IPatAnon All :: rest -> IOpInaccessibleAll :: elab rest + | IPatAnon Temporary :: rest -> IOpTemporay :: elab rest + | IPatAbstractVars vs :: rest -> IOpAbstractVars vs :: elab rest + | IPatFastNondep :: rest -> IOpFastNondep :: elab rest + + | IPatInj pats :: rest -> IOpInj (List.map elab pats) :: elab rest + | IPatRewrite(occ,dir) :: rest -> IOpRewrite(occ,dir) :: elab rest + | IPatView vs :: rest -> IOpView (None,vs) :: elab rest + | IPatSimpl s :: rest -> IOpSimpl s :: elab rest + | IPatClear cl :: rest -> IOpClear (cl,None) :: elab rest + + | IPatCase (Block seed) :: rest -> IOpCaseBlock seed :: elab rest + | IPatCase (Regular bs) :: rest -> IOpCaseBranches (List.map elab bs) :: elab rest + | IPatDispatch (Block seed) :: rest -> IOpDispatchBlock seed :: elab rest + | IPatDispatch (Regular bs) :: rest -> IOpDispatchBranches (List.map elab bs) :: elab rest + | IPatNoop :: rest -> IOpNoop :: elab rest + + in + elab l +;; +let tclCompileIPats l = + Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats input: " ++ + prlist_with_sep spc Ssrprinters.pr_ipat l)); + let ops = tclCompileIPats l in + Ssrprinters.ppdebug (lazy Pp.(str "tclCompileIPats output: " ++ + prlist_with_sep spc pr_ipatop ops)); + ops + +let main ?eqtac ~first_case_is_dispatch iops = + let ip_before, case, ip_after = split_at_first_case iops in let case = ssr_exception first_case_is_dispatch case in let case = option_to_list case in - let eqtac = option_to_list (Option.map (fun x -> IPatEqGen x) eqtac) in - Ssrcommon.tcl0G ~default:() (ipat_tac (ip_before @ case @ eqtac @ ip_after) <*> intro_end) + let eqtac = option_to_list (Option.map (fun x -> IOpEqGen x) eqtac) in + let ipats = ip_before @ case @ eqtac @ ip_after in + Ssrcommon.tcl0G ~default:() (ipat_tac ipats <*> intro_end) end (* }}} *) let tclIPAT_EQ eqtac ip = Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); - IpatMachine.main ~eqtac ~first_case_is_dispatch:true ip + IpatMachine.(main ~eqtac ~first_case_is_dispatch:true (tclCompileIPats ip)) let tclIPATssr ip = Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); - IpatMachine.main ~first_case_is_dispatch:true ip + IpatMachine.(main ~first_case_is_dispatch:true (tclCompileIPats ip)) + +let tclCompileIPats = IpatMachine.tclCompileIPats (* Common code to handle generalization lists along with the defective case *) let with_defective maintac deps clr = Goal.enter begin fun g -> @@ -721,12 +845,12 @@ let eqmovetac _ gen = ;; let rec eqmoveipats eqpat = function - | (IPatSimpl _ | IPatClear _ as ipat) :: ipats -> + | (IOpSimpl _ | IOpClear _ as ipat) :: ipats -> ipat :: eqmoveipats eqpat ipats - | (IPatAnon All :: _ | []) as ipats -> - IPatAnon (One None) :: eqpat :: ipats + | (IOpInaccessibleAll :: _ | []) as ipats -> + IOpInaccessible None :: eqpat @ ipats | ipat :: ipats -> - ipat :: eqpat :: ipats + ipat :: eqpat @ ipats let ssrsmovetac = Goal.enter begin fun g -> let sigma, concl = Goal.(sigma g, concl g) in @@ -736,7 +860,6 @@ let ssrsmovetac = Goal.enter begin fun g -> end let tclIPAT ip = - Ssrprinters.ppdebug (lazy Pp.(str "ipat@run: " ++ Ssrprinters.pr_ipats ip)); IpatMachine.main ~first_case_is_dispatch:false ip let ssrmovetac = function @@ -748,17 +871,17 @@ let ssrmovetac = function gentac <*> tclLAST_GEN ~to_ind:false lastgen (tacVIEW_THEN_GRAB view ~conclusion) <*> - tclIPAT (IPatClear clr :: ipats) + tclIPAT (IOpClear (clr,None) :: IpatMachine.tclCompileIPats ipats) | _::_ as view, (_, ({ gens = []; clr }, ipats)) -> - tclIPAT (IPatView (false,view) :: IPatClear clr :: ipats) + tclIPAT (IOpView (None,view) :: IOpClear (clr,None) :: IpatMachine.tclCompileIPats ipats) | _, (Some pat, (dgens, ipats)) -> let dgentac = with_dgens dgens eqmovetac in - dgentac <*> tclIPAT (eqmoveipats pat ipats) + dgentac <*> tclIPAT (eqmoveipats (IpatMachine.tclCompileIPats [pat]) (IpatMachine.tclCompileIPats ipats)) | _, (_, ({ gens = (_ :: _ as gens); dgens = []; clr}, ipats)) -> let gentac = V82.tactic ~nf_evars:false (Ssrcommon.genstac (gens, clr)) in - gentac <*> tclIPAT ipats + gentac <*> tclIPAT (IpatMachine.tclCompileIPats ipats) | _, (_, ({ clr }, ipats)) -> - Tacticals.New.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT ipats] + Tacticals.New.tclTHENLIST [ssrsmovetac; Tactics.clear (List.map Ssrcommon.hyp_id clr); tclIPAT (IpatMachine.tclCompileIPats ipats)] (** [abstract: absvar gens] **************************************************) let rec is_Evar_or_CastedMeta sigma x = diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli index 89cba4be71..893061b154 100644 --- a/plugins/ssr/ssripats.mli +++ b/plugins/ssr/ssripats.mli @@ -19,8 +19,44 @@ open Ssrast +(* Atomic operations for the IPat machine. Use this if you are "patching" an + * ipat written by the user, since patching it at he AST level and then + * compiling it may have tricky effects, eg adding a clear in front of a view + * also has the effect of disposing the view (the compilation phase takes care + * of this, by using the compiled ipats you can be more precise *) +type ssriop = + | IOpId of Names.Id.t + | IOpDrop + | IOpTemporay + | IOpInaccessible of string option + | IOpInaccessibleAll + | IOpAbstractVars of Names.Id.t list + | IOpFastNondep + + | IOpInj of ssriops list + + | IOpDispatchBlock of id_block + | IOpDispatchBranches of ssriops list + + | IOpCaseBlock of id_block + | IOpCaseBranches of ssriops list + + | IOpRewrite of ssrocc * ssrdir + | IOpView of ssrclear option * ssrview (* extra clears to be performed *) + + | IOpClear of ssrclear * ssrhyp option + | IOpSimpl of ssrsimpl + + | IOpEqGen of unit Proofview.tactic (* generation of eqn *) + + | IOpNoop + +and ssriops = ssriop list + +val tclCompileIPats : ssripats -> ssriops + (* The => tactical *) -val tclIPAT : ssripats -> unit Proofview.tactic +val tclIPAT : ssriops -> unit Proofview.tactic (* As above but with the SSR exception: first case is dispatch *) val tclIPATssr : ssripats -> unit Proofview.tactic diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 76726009ac..3fb21e5ef6 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -635,11 +635,10 @@ let rec map_ipat map_id map_ssrhyp map_ast_closure_term = function | IPatClear clr -> IPatClear (List.map map_ssrhyp clr) | IPatCase (Regular iorpat) -> IPatCase (Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)) | IPatCase (Block(hat)) -> IPatCase (Block(map_block map_id hat)) - | IPatDispatch (s, Regular iorpat) -> IPatDispatch (s, Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)) - | IPatDispatch (s, Block (hat)) -> IPatDispatch (s, Block(map_block map_id hat)) + | IPatDispatch (Regular iorpat) -> IPatDispatch (Regular (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat)) + | IPatDispatch (Block (hat)) -> IPatDispatch (Block(map_block map_id hat)) | IPatInj iorpat -> IPatInj (List.map (List.map (map_ipat map_id map_ssrhyp map_ast_closure_term)) iorpat) - | IPatView (clr,v) -> IPatView (clr,List.map map_ast_closure_term v) - | IPatEqGen _ -> assert false (*internal usage only *) + | IPatView v -> IPatView (List.map map_ast_closure_term v) and map_block map_id = function | Prefix id -> Prefix (map_id id) | SuffixId id -> SuffixId (map_id id) @@ -715,22 +714,22 @@ let interp_ipat ist gl = if not (ltacvar id) then hyp :: hyps else add_intro_pattern_hyps CAst.(make ?loc (interp_introid ist gl id)) hyps in let clr' = List.fold_right add_hyps clr [] in - check_hyps_uniq [] clr'; IPatClear clr' + check_hyps_uniq [] clr'; + IPatClear clr' | IPatCase(Regular iorpat) -> IPatCase(Regular(List.map (List.map interp) iorpat)) | IPatCase(Block(hat)) -> IPatCase(Block(interp_block hat)) - | IPatDispatch(s,Regular iorpat) -> - IPatDispatch(s,Regular (List.map (List.map interp) iorpat)) - | IPatDispatch(s,Block(hat)) -> IPatDispatch(s,Block(interp_block hat)) + | IPatDispatch(Regular iorpat) -> + IPatDispatch(Regular (List.map (List.map interp) iorpat)) + | IPatDispatch(Block(hat)) -> IPatDispatch(Block(interp_block hat)) | IPatInj iorpat -> IPatInj (List.map (List.map interp) iorpat) | IPatAbstractVars l -> IPatAbstractVars (List.map get_intro_id (List.map (interp_introid ist gl) l)) - | IPatView (clr,l) -> IPatView (clr,List.map (fun x -> snd(interp_ast_closure_term ist + | IPatView l -> IPatView (List.map (fun x -> snd(interp_ast_closure_term ist gl x)) l) | (IPatSimpl _ | IPatAnon _ | IPatRewrite _ | IPatNoop | IPatFastNondep) as x -> x - | IPatEqGen _ -> assert false (*internal usage only *) in interp @@ -765,10 +764,6 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats } | Some [], _ -> CErrors.user_err ~loc (str"occ_switch expected") | None, occ -> [IPatRewrite (occ, R2L)] | Some clr, _ -> [IPatClear clr; IPatRewrite (allocc, R2L)] } - | [ ssrdocc(occ) ssrfwdview(v) ] -> { match occ with - | Some [], _ -> [IPatView (true,v)] - | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl;IPatView (false,v)] - | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") } | [ ssrdocc(occ) ] -> { match occ with | Some cl, _ -> check_hyps_uniq [] cl; [IPatClear cl] | _ -> CErrors.user_err ~loc (str"Only identifiers are allowed here") } @@ -786,7 +781,7 @@ ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats } | [ "-/" integer(n) "/=" ] -> { [IPatNoop;IPatSimpl(SimplCut (n,~-1))] } | [ "-/" integer(n) "/" integer (m) "=" ] -> { [IPatNoop;IPatSimpl(SimplCut(n,m))] } - | [ ssrfwdview(v) ] -> { [IPatView (false,v)] } + | [ ssrfwdview(v) ] -> { [IPatView v] } | [ "[" ":" ident_list(idl) "]" ] -> { [IPatAbstractVars idl] } | [ "[:" ident_list(idl) "]" ] -> { [IPatAbstractVars idl] } END @@ -875,11 +870,12 @@ ARGUMENT EXTEND ssripats_ne TYPED AS ssripat PRINTED BY { pr_ssripats } let check_ssrhpats loc w_binders ipats = let err_loc s = CErrors.user_err ~loc ~hdr:"ssreflect" s in let clr, ipats = + let opt_app = function None -> fun l -> Some l + | Some l1 -> fun l2 -> Some (l1 @ l2) in let rec aux clr = function - | IPatClear cl :: tl -> aux (clr @ cl) tl -(* | IPatSimpl (cl, sim) :: tl -> clr @ cl, IPatSimpl ([], sim) :: tl *) + | IPatClear cl :: tl -> aux (opt_app clr cl) tl | tl -> clr, tl - in aux [] ipats in + in aux None ipats in let simpl, ipats = match List.rev ipats with | IPatSimpl _ as s :: tl -> [s], List.rev tl @@ -903,27 +899,29 @@ let check_ssrhpats loc w_binders ipats = in loop [] ipats in ((clr, ipat), binders), simpl +let pr_clear_opt sep = function None -> mt () | Some x -> pr_clear sep x + let pr_hpats (((clr, ipat), binders), simpl) = - pr_clear mt clr ++ pr_ipats ipat ++ pr_ipats binders ++ pr_ipats simpl + pr_clear_opt mt clr ++ pr_ipats ipat ++ pr_ipats binders ++ pr_ipats simpl let pr_ssrhpats _ _ _ = pr_hpats let pr_ssrhpats_wtransp _ _ _ (_, x) = pr_hpats x } -ARGUMENT EXTEND ssrhpats TYPED AS (((ssrclear * ssripat) * ssripat) * ssripat) +ARGUMENT EXTEND ssrhpats TYPED AS (((ssrclear option * ssripat) * ssripat) * ssripat) PRINTED BY { pr_ssrhpats } | [ ssripats(i) ] -> { check_ssrhpats loc true i } END ARGUMENT EXTEND ssrhpats_wtransp - TYPED AS (bool * (((ssrclear * ssripats) * ssripats) * ssripats)) + TYPED AS (bool * (((ssrclear option * ssripats) * ssripats) * ssripats)) PRINTED BY { pr_ssrhpats_wtransp } | [ ssripats(i) ] -> { false,check_ssrhpats loc true i } | [ ssripats(i) "@" ssripats(j) ] -> { true,check_ssrhpats loc true (i @ j) } END ARGUMENT EXTEND ssrhpats_nobs -TYPED AS (((ssrclear * ssripats) * ssripats) * ssripats) PRINTED BY { pr_ssrhpats } +TYPED AS (((ssrclear option * ssripats) * ssripats) * ssripats) PRINTED BY { pr_ssrhpats } | [ ssripats(i) ] -> { check_ssrhpats loc false i } END @@ -2051,7 +2049,7 @@ END (* We just add a numeric version that clears the n top assumptions. *) TACTIC EXTEND ssrclear - | [ "clear" natural(n) ] -> { tclIPAT (List.init n (fun _ -> IPatAnon Drop)) } + | [ "clear" natural(n) ] -> { tclIPAT (List.init n (fun _ -> IOpDrop)) } END (** The "move" tactic *) @@ -2090,10 +2088,10 @@ let movearg_of_parsed_movearg (v,(eq,(dg,ip))) = TACTIC EXTEND ssrmove | [ "move" ssrmovearg(arg) ssrrpat(pat) ] -> - { ssrmovetac (movearg_of_parsed_movearg arg) <*> tclIPAT [pat] } + { ssrmovetac (movearg_of_parsed_movearg arg) <*> tclIPAT (tclCompileIPats [pat]) } | [ "move" ssrmovearg(arg) ssrclauses(clauses) ] -> { tclCLAUSES (ssrmovetac (movearg_of_parsed_movearg arg)) clauses } -| [ "move" ssrrpat(pat) ] -> { tclIPAT [pat] } +| [ "move" ssrrpat(pat) ] -> { tclIPAT (tclCompileIPats [pat]) } | [ "move" ] -> { ssrsmovetac } END @@ -2632,7 +2630,11 @@ END { -let augment_preclr clr1 (((clr0, x),y),z) = (((clr1 @ clr0, x),y),z) +let augment_preclr clr1 (((clr0, x),y),z) = + let cl = match clr0 with + | None -> if clr1 = [] then None else Some clr1 + | Some clr0 -> Some (clr1 @ clr0) in + (((cl, x),y),z) } diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index 898e03b00e..38f5b7d107 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -74,7 +74,7 @@ let pr_occ = function | None -> str "{}" let pr_clear_ne clr = str "{" ++ pr_hyps clr ++ str "}" -let pr_clear sep clr = if clr = [] then mt () else sep () ++ pr_clear_ne clr +let pr_clear sep clr = sep () ++ pr_clear_ne clr let pr_dir = function L2R -> str "->" | R2L -> str "<-" @@ -102,20 +102,18 @@ let rec pr_ipat p = | IPatClear clr -> pr_clear mt clr | IPatCase (Regular iorpat) -> hov 1 (str "[" ++ pr_iorpat iorpat ++ str "]") | IPatCase (Block m) -> hov 1 (str"[" ++ pr_block m ++ str"]") - | IPatDispatch(_,Regular iorpat) -> hov 1 (str "(" ++ pr_iorpat iorpat ++ str ")") - | IPatDispatch (_,Block m) -> hov 1 (str"(" ++ pr_block m ++ str")") + | IPatDispatch(Regular iorpat) -> hov 1 (str "(" ++ pr_iorpat iorpat ++ str ")") + | IPatDispatch (Block m) -> hov 1 (str"(" ++ pr_block m ++ str")") | IPatInj iorpat -> hov 1 (str "[=" ++ pr_iorpat iorpat ++ str "]") | IPatRewrite (occ, dir) -> pr_occ occ ++ pr_dir dir | IPatAnon All -> str "*" | IPatAnon Drop -> str "_" | IPatAnon (One _) -> str "?" - | IPatView (false,v) -> pr_view2 v - | IPatView (true,v) -> str"{}" ++ pr_view2 v + | IPatView v -> pr_view2 v | IPatAnon Temporary -> str "+" | IPatNoop -> str "-" | IPatAbstractVars l -> str "[:" ++ pr_list spc Id.print l ++ str "]" | IPatFastNondep -> str">" - | IPatEqGen _ -> str "<tac>" and pr_ipats ipats = pr_list spc pr_ipat ipats and pr_iorpat iorpat = pr_list pr_bar pr_ipats iorpat and pr_block = function (Prefix id) -> str"^" ++ Id.print id diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 31c360ad6d..5f20ac2705 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -43,6 +43,7 @@ val pr_view2 : ast_closure_term list -> Pp.t val pr_ipat : ssripat -> Pp.t val pr_ipats : ssripats -> Pp.t val pr_iorpat : ssripatss -> Pp.t +val pr_block : id_block -> Pp.t val pr_hyp : ssrhyp -> Pp.t val pr_hyps : ssrhyps -> Pp.t diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index 4816027296..2794696017 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -142,7 +142,7 @@ let intern_constr_expr { Genintern.genv; ltacvars = vars } sigma ce = To allow for t being a notation, like "Notation foo x := ltac:(foo x)", we need to internalize t. *) -let is_tac_in_term ?extra_scope { body; glob_env; interp_env } = +let is_tac_in_term ?extra_scope { annotation; body; glob_env; interp_env } = Goal.(enter_one ~__LOC__ begin fun goal -> let genv = env goal in let sigma = sigma goal in @@ -161,7 +161,7 @@ let is_tac_in_term ?extra_scope { body; glob_env; interp_env } = | Glob_term.GHole (_,_, Some x) when Genarg.has_type x (Genarg.glbwit Tacarg.wit_tactic) -> tclUNIT (`Tac (Genarg.out_gen (Genarg.glbwit Tacarg.wit_tactic) x)) - | _ -> tclUNIT (`Term (interp_env, g)) + | _ -> tclUNIT (`Term (annotation, interp_env, g)) end) (* To inject a constr into a glob_constr we use an Ltac variable *) @@ -207,7 +207,7 @@ let tclKeepOpenConstr (_env, sigma, t) = Unsafe.tclEVARS sigma <*> tclUNIT t let tclADD_CLEAR_IF_ID (env, ist, t) x = Ssrprinters.ppdebug (lazy Pp.(str"tclADD_CLEAR_IF_ID: " ++ Printer.pr_econstr_env env ist t)); - let hd, _ = EConstr.decompose_app ist t in + let hd, args = EConstr.decompose_app ist t in match EConstr.kind ist hd with | Constr.Var id when Ssrcommon.not_section_id id -> tclUNIT (x, [id]) | _ -> tclUNIT (x,[]) @@ -280,8 +280,9 @@ let interp_view ~clear_if_id ist v p = else tclKeepOpenConstr ot >>= tclPAIR [] (* we store in the state (v top), then (v1 (v2 top))... *) -let pile_up_view ~clear_if_id (ist, v) = +let pile_up_view ~clear_if_id (annotation, ist, v) = let ist = Ssrcommon.option_assert_get ist (Pp.str"not a term") in + let clear_if_id = clear_if_id && annotation <> `Parens in State.vsPUSH (fun p -> interp_view ~clear_if_id ist v p) let finalize_view s0 ?(simple_types=true) p = diff --git a/printing/prettyp.ml b/printing/prettyp.ml index c417ef8a66..408bd5f60b 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -267,7 +267,6 @@ let print_name_infos ref = print_ref true ref None; blankline] else [] in - print_polymorphism ref @ print_type_in_type ref @ print_primitive ref @ type_info_for_implicit @ @@ -838,6 +837,7 @@ let print_about_any ?loc env sigma k udecl = Dumpglob.add_glob ?loc ref; pr_infos_list (print_ref false ref udecl :: blankline :: + print_polymorphism ref @ print_name_infos ref @ (if Pp.ismt rb then [] else [rb]) @ print_opacity ref @ diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 4cc73f419e..9ee9e7ae2c 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -22,51 +22,6 @@ open Names module NamedDecl = Context.Named.Declaration -(*** Proof Modes ***) - -(* Type of proof modes : - - A function [set] to set it *from standard mode* - - A function [reset] to reset the *standard mode* from it *) -type proof_mode_name = string -type proof_mode = { - name : proof_mode_name ; - set : unit -> unit ; - reset : unit -> unit -} - -let proof_modes = Hashtbl.create 6 -let find_proof_mode n = - try Hashtbl.find proof_modes n - with Not_found -> - CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n)) - -let register_proof_mode ({name = n} as m) = - Hashtbl.add proof_modes n (CEphemeron.create m) - -(* initial mode: standard mode *) -let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) } -let _ = register_proof_mode standard - -(* Default proof mode, to be set at the beginning of proofs. *) -let default_proof_mode = ref (find_proof_mode "No") - -let get_default_proof_mode_name () = - (CEphemeron.default !default_proof_mode standard).name - -let proof_mode_opt_name = ["Default";"Proof";"Mode"] -let () = - Goptions.(declare_string_option { - optdepr = false; - optname = "default proof mode" ; - optkey = proof_mode_opt_name ; - optread = begin fun () -> - (CEphemeron.default !default_proof_mode standard).name - end; - optwrite = begin fun n -> - default_proof_mode := find_proof_mode n - end - }) - (*** Proof Global Environment ***) (* Extra info on proofs. *) @@ -95,7 +50,6 @@ type pstate = { endline_tactic : Genarg.glob_generic_argument option; section_vars : Constr.named_context option; proof : Proof.t; - mode : proof_mode CEphemeron.key; universe_decl: UState.universe_decl; strength : Decl_kinds.goal_kind; } @@ -109,23 +63,8 @@ let apply_terminator f = f to be resumed when the current proof is closed or aborted. *) let pstates = ref ([] : pstate list) -(* Current proof_mode, for bookkeeping *) -let current_proof_mode = ref !default_proof_mode - -(* combinators for proof modes *) -let update_proof_mode () = - match !pstates with - | { mode = m } :: _ -> - CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); - current_proof_mode := m; - CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ()) - | _ -> - CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); - current_proof_mode := find_proof_mode "No" - (* combinators for the current_proof lists *) -let push a l = l := a::!l; - update_proof_mode () +let push a l = l := a::!l exception NoSuchProof let () = CErrors.register_handler begin function @@ -221,25 +160,8 @@ let discard {CAst.loc;v=id} = let discard_current () = if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates - let discard_all () = pstates := [] -(* [set_proof_mode] sets the proof mode to be used after it's called. It is - typically called by the Proof Mode command. *) -let set_proof_mode m id = - pstates := List.map - (fun ps -> if pf_name_eq id ps then { ps with mode = m } else ps) - !pstates; - update_proof_mode () - -let set_proof_mode mn = - set_proof_mode (find_proof_mode mn) (get_current_proof_name ()) - -let activate_proof_mode mode = - CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ()) -let disactivate_current_proof_mode () = - CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()) - (** [start_proof sigma id pl str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this @@ -254,9 +176,8 @@ let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator proof = Proof.start ~name ~poly:(pi2 kind) sigma goals; endline_tactic = None; section_vars = None; - mode = find_proof_mode "No"; - universe_decl = pl; - strength = kind } in + strength = kind; + universe_decl = pl } in push initial_state pstates let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator = @@ -265,9 +186,8 @@ let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals termina proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals; endline_tactic = None; section_vars = None; - mode = find_proof_mode "No"; - universe_decl = pl; - strength = kind } in + strength = kind; + universe_decl = pl } in push initial_state pstates let get_used_variables () = (cur_pstate ()).section_vars @@ -478,7 +398,7 @@ end let freeze ~marshallable = if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.") else !pstates -let unfreeze s = pstates := s; update_proof_mode () +let unfreeze s = pstates := s let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof let copy_terminators ~src ~tgt = assert(List.length src = List.length tgt); diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index e762f3b7dc..40920f51a3 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -13,7 +13,6 @@ environment. *) type t - val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit @@ -139,47 +138,3 @@ val freeze : marshallable:bool -> t val unfreeze : t -> unit val proof_of_state : t -> Proof.t val copy_terminators : src:t -> tgt:t -> t - - -(**********************************************************) -(* Proof Mode API *) -(* The current Proof Mode API is deprecated and a new one *) -(* will be (hopefully) defined in 8.8 *) -(**********************************************************) - -(** Type of proof modes : - - A name - - A function [set] to set it *from standard mode* - - A function [reset] to reset the *standard mode* from it - -*) -type proof_mode_name = string -type proof_mode = { - name : proof_mode_name ; - set : unit -> unit ; - reset : unit -> unit -} - -(** Registers a new proof mode which can then be adressed by name - in [set_default_proof_mode]. - One mode is already registered - the standard mode - named "No", - It corresponds to Coq default setting are they are set when coqtop starts. *) -val register_proof_mode : proof_mode -> unit -(* Can't make this deprecated due to limitations of camlp5 *) -(* [@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] *) - -val proof_mode_opt_name : string list - -val get_default_proof_mode_name : unit -> proof_mode_name -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] - -(** [set_proof_mode] sets the proof mode to be used after it's called. It is - typically called by the Proof Mode command. *) -val set_proof_mode : proof_mode_name -> unit -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] - -val activate_proof_mode : proof_mode_name -> unit -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] - -val disactivate_current_proof_mode : unit -> unit -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] diff --git a/stm/stm.ml b/stm/stm.ml index 8ed7f2c866..dfe5581ed5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -126,8 +126,6 @@ type aast = { } let pr_ast { expr; indentation } = Pp.(int indentation ++ str " " ++ Ppvernac.pr_vernac expr) -let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] - (* Commands piercing opaque *) let may_pierce_opaque = function | VernacPrint _ @@ -146,13 +144,13 @@ let update_global_env () = module Vcs_ = Vcs.Make(Stateid.Self) type future_proof = Proof_global.closed_proof_output Future.computation -type proof_mode = string + type depth = int type branch_type = [ `Master - | `Proof of proof_mode * depth + | `Proof of depth | `Edit of - proof_mode * Stateid.t * Stateid.t * Vernacextend.vernac_qed_type * Vcs_.Branch.t ] + Stateid.t * Stateid.t * Vernacextend.vernac_qed_type * Vcs_.Branch.t ] (* TODO 8.7 : split commands and tactics, since this type is too messy now *) type cmd_t = { ctac : bool; (* is a tactic *) @@ -203,10 +201,10 @@ let summary_pstate = Evarutil.meta_counter_summary_tag, Obligations.program_tcc_summary_tag type cached_state = - | Empty - | Error of Exninfo.iexn - | Valid of Vernacstate.t - + | EmptyState + | ParsingState of Vernacstate.Parser.state + | FullState of Vernacstate.t + | ErrorState of Vernacstate.Parser.state option * Exninfo.iexn type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info type backup = { mine : branch; others : branch list } @@ -214,10 +212,16 @@ type 'vcs state_info = { (* TODO: Make this record private to VCS *) mutable n_reached : int; (* debug cache: how many times was computed *) mutable n_goals : int; (* open goals: indentation *) mutable state : cached_state; (* state value *) + mutable proof_mode : Pvernac.proof_mode option; mutable vcs_backup : 'vcs option * backup option; } -let default_info () = - { n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None } +let default_info proof_mode = + { + n_reached = 0; n_goals = 0; + state = EmptyState; + proof_mode; + vcs_backup = (None,None); + } module DynBlockData : Dyn.S = Dyn.Make () @@ -256,15 +260,15 @@ end = struct (* {{{ *) List.fold_left max 0 (CList.map_filter (function - | { Vcs_.kind = `Proof (_,n) } -> Some n + | { Vcs_.kind = `Proof n } -> Some n | { Vcs_.kind = `Edit _ } -> Some 1 | _ -> None) (List.map (Vcs_.get_branch vcs) (Vcs_.branches vcs))) let find_proof_at_depth vcs pl = try List.find (function - | _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl - | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth.") + | _, { Vcs_.kind = `Proof n } -> Int.equal n pl + | _, { Vcs_.kind = `Edit _ } -> anomaly(Pp.str "find_proof_at_depth") | _ -> false) (List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs)) with Not_found -> failwith "find_proof_at_depth" @@ -326,7 +330,7 @@ module VCS : sig type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t - val init : stm_doc_type -> id -> doc + val init : stm_doc_type -> id -> Vernacstate.Parser.state -> doc (* val get_type : unit -> stm_doc_type *) val set_ldir : Names.DirPath.t -> unit val get_ldir : unit -> Names.DirPath.t @@ -339,7 +343,7 @@ module VCS : sig val branches : unit -> Branch.t list val get_branch : Branch.t -> branch_type branch_info val get_branch_pos : Branch.t -> id - val new_node : ?id:Stateid.t -> unit -> id + val new_node : ?id:Stateid.t -> Pvernac.proof_mode option -> unit -> id val merge : id -> ours:transaction -> ?into:Branch.t -> Branch.t -> unit val rewrite_merge : id -> ours:transaction -> at:id -> Branch.t -> unit val delete_branch : Branch.t -> unit @@ -356,6 +360,10 @@ module VCS : sig val goals : id -> int -> unit val set_state : id -> cached_state -> unit val get_state : id -> cached_state + val set_parsing_state : id -> Vernacstate.Parser.state -> unit + val get_parsing_state : id -> Vernacstate.Parser.state option + val get_proof_mode : id -> Pvernac.proof_mode option + val set_proof_mode : id -> Pvernac.proof_mode option -> unit (* cuts from start -> stop, raising Expired if some nodes are not there *) val slice : block_start:id -> block_stop:id -> vcs @@ -369,7 +377,8 @@ module VCS : sig val proof_nesting : unit -> int val checkout_shallowest_proof_branch : unit -> unit - val propagate_sideff : action:seff_t -> unit + val propagate_sideff : action:seff_t -> Stateid.t list + val propagate_qed : unit -> unit val gc : unit -> unit @@ -411,11 +420,11 @@ end = struct (* {{{ *) | Qed { qast } -> Pp.string_of_ppcmds (pr_ast qast) in let is_green id = match get_info vcs id with - | Some { state = Valid _ } -> true + | Some { state = FullState _ } -> true | _ -> false in let is_red id = match get_info vcs id with - | Some { state = Error _ } -> true + | Some { state = ErrorState _ } -> true | _ -> false in let head = current_branch vcs in let heads = @@ -517,10 +526,11 @@ end = struct (* {{{ *) let doc_type = ref (Interactive (TopLogical (Names.DirPath.make []))) let ldir = ref Names.DirPath.empty - let init dt id = + let init dt id ps = doc_type := dt; vcs := empty id; - vcs := set_info !vcs id (default_info ()); + let info = { (default_info None) with state = ParsingState ps } in + vcs := set_info !vcs id info; dummy_doc let set_ldir ld = @@ -545,9 +555,9 @@ end = struct (* {{{ *) let branches () = branches !vcs let get_branch head = get_branch !vcs head let get_branch_pos head = (get_branch head).pos - let new_node ?(id=Stateid.fresh ()) () = + let new_node ?(id=Stateid.fresh ()) proof_mode () = assert(Vcs_.get_info !vcs id = None); - vcs := set_info !vcs id (default_info ()); + vcs := set_info !vcs id (default_info proof_mode); id let merge id ~ours ?into branch = vcs := merge !vcs id ~ours ~theirs:Noop ?into branch @@ -569,9 +579,39 @@ end = struct (* {{{ *) | Some x -> x | None -> raise Vcs_aux.Expired let set_state id s = - (get_info id).state <- s; - if async_proofs_is_master !cur_opt then Hooks.(call state_ready ~doc:dummy_doc (* XXX should be taken in input *) id) + let info = get_info id in + info.state <- s; + let is_full_state_valid = match s with + | FullState _ -> true + | EmptyState | ErrorState _ | ParsingState _ -> false + in + if async_proofs_is_master !cur_opt && is_full_state_valid then + Hooks.(call state_ready ~doc:dummy_doc (* XXX should be taken in input *) id) + let get_state id = (get_info id).state + + let get_parsing_state id = + stm_pperr_endline (fun () -> str "retrieve parsing state state " ++ str (Stateid.to_string id) ++ str " }}}"); + match (get_info id).state with + | FullState s -> Some s.Vernacstate.parsing + | ParsingState s -> Some s + | ErrorState (s,_) -> s + | EmptyState -> None + + let set_parsing_state id ps = + let info = get_info id in + let new_state = + match info.state with + | FullState s -> assert false + | ParsingState s -> assert false + | ErrorState _ -> assert false + | EmptyState -> ParsingState ps + in + info.state <- new_state + + let get_proof_mode id = (get_info id).proof_mode + let set_proof_mode id pm = (get_info id).proof_mode <- pm + let reached id = let info = get_info id in info.n_reached <- info.n_reached + 1 @@ -582,28 +622,33 @@ end = struct (* {{{ *) let checkout_shallowest_proof_branch () = if List.mem edit_branch (Vcs_.branches !vcs) then begin - checkout edit_branch; - match get_branch edit_branch with - | { kind = `Edit (mode, _,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"] - | _ -> assert false + checkout edit_branch end else let pl = proof_nesting () in try - let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with - | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in - checkout branch; - stm_prerr_endline (fun () -> "mode:" ^ mode); - Proof_global.activate_proof_mode mode [@ocaml.warning "-3"] + let branch = fst @@ Vcs_aux.find_proof_at_depth !vcs pl in + checkout branch with Failure _ -> - checkout Branch.master; - Proof_global.disactivate_current_proof_mode () [@ocaml.warning "-3"] + checkout Branch.master (* copies the transaction on every open branch *) let propagate_sideff ~action = + List.map (fun b -> + checkout b; + let proof_mode = get_proof_mode @@ get_branch_pos b in + let id = new_node proof_mode () in + merge id ~ours:(Sideff action) ~into:b Branch.master; + id) + (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ())) + + let propagate_qed () = List.iter (fun b -> checkout b; - let id = new_node () in - merge id ~ours:(Sideff action) ~into:b Branch.master) + let proof_mode = get_proof_mode @@ get_branch_pos b in + let id = new_node proof_mode () in + let parsing = Option.get @@ get_parsing_state (get_branch_pos b) in + merge id ~ours:(Sideff CherryPickEnv) ~into:b Branch.master; + set_parsing_state id parsing) (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ())) let visit id = Vcs_aux.visit !vcs id @@ -625,10 +670,12 @@ end = struct (* {{{ *) let slice ~block_start ~block_stop = let l = nodes_in_slice ~block_start ~block_stop in let copy_info v id = + let info = get_info id in Vcs_.set_info v id - { (get_info id) with state = Empty; vcs_backup = None,None } in + { info with state = EmptyState; + vcs_backup = None,None } in let make_shallow = function - | Valid st -> Valid (Vernacstate.make_shallow st) + | FullState st -> FullState (Vernacstate.make_shallow st) | x -> x in let copy_info_w_state v id = @@ -651,12 +698,14 @@ end = struct (* {{{ *) let v = copy_info v id in v) l v in (* Stm should have reached the beginning of proof *) - assert (match (get_info block_start).state with Valid _ -> true | _ -> false); + assert (match get_state block_start + with FullState _ -> true | _ -> false); (* We put in the new dag the most recent state known to master *) let rec fill id = - match (get_info id).state with - | Empty | Error _ -> fill (Vcs_aux.visit v id).next - | Valid _ -> copy_info_w_state v id in + match get_state id with + | EmptyState | ErrorState _ | ParsingState _ -> fill (Vcs_aux.visit v id).next + | FullState _ -> copy_info_w_state v id + in let v = fill block_stop in (* We put in the new dag the first state (since Qed shall run on it, * see check_task_aux) *) @@ -753,13 +802,12 @@ end = struct (* {{{ *) end (* }}} *) let state_of_id ~doc id = - try match (VCS.get_info id).state with - | Valid s -> `Valid (Some s) - | Error (e,_) -> `Error e - | Empty -> `Valid None + try match VCS.get_state id with + | FullState s -> `Valid (Some s) + | ErrorState (_,(e,_)) -> `Error e + | EmptyState | ParsingState _ -> `Valid None with VCS.Expired -> `Expired - (****** A cache: fills in the nodes of the VCS document with their value ******) module State : sig @@ -782,6 +830,7 @@ module State : sig val fix_exn_ref : (Exninfo.iexn -> Exninfo.iexn) ref val install_cached : Stateid.t -> unit + (* val install_parsing_state : Stateid.t -> unit *) val is_cached : ?cache:bool -> Stateid.t -> bool val is_cached_and_valid : ?cache:bool -> Stateid.t -> bool @@ -804,10 +853,6 @@ module State : sig val register_root_state : unit -> unit val restore_root_state : unit -> unit - (* Only for internal use to catch problems in parse_sentence, should - be removed in the state handling refactoring. *) - val cur_id : Stateid.t ref - val purify : ('a -> 'b) -> 'a -> 'b end = struct (* {{{ *) @@ -824,6 +869,8 @@ end = struct (* {{{ *) Vernacstate.unfreeze_interp_state st.vernac_state; cur_id := st.id + let invalidate_cur_state () = cur_id := Stateid.dummy + type proof_part = Proof_global.t * int * (* Evarutil.meta_counter_summary_tag *) @@ -842,49 +889,58 @@ end = struct (* {{{ *) Summary.project_from_summary st Util.(pi3 summary_pstate) let cache_state ~marshallable id = - VCS.set_state id (Valid (Vernacstate.freeze_interp_state ~marshallable)) + VCS.set_state id (FullState (Vernacstate.freeze_interp_state ~marshallable)) - let freeze_invalid id iexn = VCS.set_state id (Error iexn) + let freeze_invalid id iexn = + let ps = VCS.get_parsing_state id in + VCS.set_state id (ErrorState (ps,iexn)) let is_cached ?(cache=false) id only_valid = if Stateid.equal id !cur_id then try match VCS.get_info id with - | { state = Empty } when cache -> cache_state ~marshallable:false id; true + | ({ state = EmptyState } | { state = ParsingState _ }) when cache -> cache_state ~marshallable:false id; true | _ -> true with VCS.Expired -> false else - try match VCS.get_info id with - | { state = Empty } -> false - | { state = Valid _ } -> true - | { state = Error _ } -> not only_valid + try match VCS.get_state id with + | EmptyState | ParsingState _ -> false + | FullState _ -> true + | ErrorState _ -> not only_valid with VCS.Expired -> false let is_cached_and_valid ?cache id = is_cached ?cache id true let is_cached ?cache id = is_cached ?cache id false let install_cached id = - match VCS.get_info id with - | { state = Valid s } -> + match VCS.get_state id with + | FullState s -> Vernacstate.unfreeze_interp_state s; cur_id := id - | { state = Error ie } -> + | ErrorState (_,ie) -> Exninfo.iraise ie - | _ -> - (* coqc has a 1 slot cache and only for valid states *) - if not (VCS.is_interactive ()) && Stateid.equal id !cur_id then () - else anomaly Pp.(str "installing a non cached state.") + | EmptyState | ParsingState _ -> + (* coqc has a 1 slot cache and only for valid states *) + if (VCS.is_interactive ()) || not (Stateid.equal id !cur_id) then + anomaly Pp.(str "installing a non cached state.") + + (* + let install_parsing_state id = + if not (Stateid.equal id !cur_id) then begin + Vernacstate.Parser.install @@ VCS.get_parsing_state id + end + *) let get_cached id = - try match VCS.get_info id with - | { state = Valid s } -> s + try match VCS.get_state id with + | FullState s -> s | _ -> anomaly Pp.(str "not a cached state.") with VCS.Expired -> anomaly Pp.(str "not a cached state (expired).") let assign id what = let open Vernacstate in - if VCS.get_state id <> Empty then () else + if VCS.get_state id <> EmptyState then () else try match what with | `Full s -> let s = @@ -896,7 +952,7 @@ end = struct (* {{{ *) ~src:(get_cached prev).proof ~tgt:s.proof } else s with VCS.Expired -> s in - VCS.set_state id (Valid s) + VCS.set_state id (FullState s) | `ProofOnly(ontop,(pstate,c1,c2,c3)) -> if is_cached_and_valid ontop then let s = get_cached ontop in @@ -912,7 +968,7 @@ end = struct (* {{{ *) st end } in - VCS.set_state id (Valid s) + VCS.set_state id (FullState s) with VCS.Expired -> () let exn_on id ~valid (e, info) = @@ -958,7 +1014,7 @@ end = struct (* {{{ *) with e -> let (e, info) = CErrors.push e in let good_id = !cur_id in - cur_id := Stateid.dummy; + invalidate_cur_state (); VCS.reached id; let ie = match Stateid.get info, safe_id with @@ -1130,7 +1186,7 @@ module Backtrack : sig val branches_of : Stateid.t -> backup (* Returns the state that the command should backtract to *) - val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t * vernac_when + val undo_vernac_classifier : vernac_control -> doc:doc -> Stateid.t val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option end = struct (* {{{ *) @@ -1205,30 +1261,30 @@ end = struct (* {{{ *) try match Vernacprop.under_control v with | VernacResetInitial -> - Stateid.initial, VtNow + Stateid.initial | VernacResetName {CAst.v=name} -> - let id = VCS.get_branch_pos (VCS.current_branch ()) in + let id = VCS.cur_tip () in (try let oid = fold_until (fun b (id,_,label,_,_) -> if b then `Stop id else `Cont (List.mem name label)) false id in - oid, VtNow + oid with Not_found -> - id, VtNow) + id) | VernacBack n -> - let id = VCS.get_branch_pos (VCS.current_branch ()) in + let id = VCS.cur_tip () in let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in - oid, VtNow + oid | VernacUndo n -> - let id = VCS.get_branch_pos (VCS.current_branch ()) in + let id = VCS.cur_tip () in let oid = fold_until back_tactic n id in - oid, VtLater + oid | VernacUndoTo _ | VernacRestart as e -> let m = match e with VernacUndoTo m -> m | _ -> 0 in - let id = VCS.get_branch_pos (VCS.current_branch ()) in + let id = VCS.cur_tip () in let vcs = match (VCS.get_info id).vcs_backup with | None, _ -> anomaly Pp.(str"Backtrack: tip with no vcs_backup.") @@ -1241,15 +1297,15 @@ end = struct (* {{{ *) 0 id in let oid = fold_until (fun n (id,_,_,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in - oid, VtLater + oid | VernacAbortAll -> - let id = VCS.get_branch_pos (VCS.current_branch ()) in + let id = VCS.cur_tip () in let oid = fold_until (fun () (id,vcs,_,_,_) -> match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ()) () id in - oid, VtLater + oid | VernacBackTo id -> - Stateid.of_int id, VtNow + Stateid.of_int id | _ -> anomaly Pp.(str "incorrect VtMeta classification") with | Not_found -> @@ -2331,8 +2387,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = (Proofview.Goal.goal gl) goals_to_admit then Proofview.give_up else Proofview.tclUNIT () end in - match (VCS.get_info base_state).state with - | Valid { Vernacstate.proof } -> + match VCS.get_state base_state with + | FullState { Vernacstate.proof } -> Proof_global.unfreeze proof; Proof_global.with_current_proof (fun _ p -> feedback ~id:id Feedback.AddedAxiom; @@ -2469,7 +2525,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = VCS.create_proof_task_box nodes ~qed:id ~block_start; begin match brinfo, qed.fproof with | { VCS.kind = `Edit _ }, None -> assert false - | { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) -> + | { VCS.kind = `Edit (_,_, okeep, _) }, Some (ofp, cancel) -> assert(redefine_qed = true); if okeep <> keep then msg_warning(strbrk("The command closing the proof changed. " @@ -2655,7 +2711,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = (* We must reset the whole state before creating a document! *) State.restore_root_state (); - let doc = VCS.init doc_type Stateid.initial in + let doc = VCS.init doc_type Stateid.initial (Vernacstate.Parser.init ()) in (* Set load path; important, this has to happen before we declare the library below as [Declaremods/Library] will infer the module @@ -2723,16 +2779,8 @@ let observe ~doc id = let finish ~doc = let head = VCS.current_branch () in - let doc =observe ~doc (VCS.get_branch_pos head) in - VCS.print (); - (* EJGA: Setting here the proof state looks really wrong, and it - hides true bugs cf bug #5363. Also, what happens with observe? *) - (* Some commands may by side effect change the proof mode *) - (match VCS.get_branch head with - | { VCS.kind = `Edit (mode,_,_,_,_) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"] - | { VCS.kind = `Proof (mode, _) } -> Proof_global.activate_proof_mode mode [@ocaml.warning "-3"] - | _ -> () - ); doc + let doc = observe ~doc (VCS.get_branch_pos head) in + VCS.print (); doc let wait ~doc = let doc = observe ~doc (VCS.get_branch_pos VCS.Branch.master) in @@ -2809,12 +2857,14 @@ let merge_proof_branch ~valid ?id qast keep brname = match brinfo with | { VCS.kind = `Proof _ } -> VCS.checkout VCS.Branch.master; - let id = VCS.new_node ?id () in + let id = VCS.new_node ?id None () in + let parsing = Option.get @@ VCS.get_parsing_state (VCS.cur_tip ()) in VCS.merge id ~ours:(Qed (qed None)) brname; + VCS.set_parsing_state id parsing; VCS.delete_branch brname; - VCS.propagate_sideff ~action:CherryPickEnv; + VCS.propagate_qed (); `Ok - | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } -> + | { VCS.kind = `Edit (qed_id, master_id, _,_) } -> let ofp = match VCS.visit qed_id with | { step = `Qed ({ fproof }, _) } -> fproof @@ -2846,25 +2896,32 @@ let snapshot_vio ~doc ldir long_f_dot_vo = let reset_task_queue = Slaves.reset_task_queue (* Document building *) -let process_back_meta_command ~newtip ~head oid aast w = - let id = VCS.new_node ~id:newtip () in - let { mine; others } = Backtrack.branches_of oid in + +(* We process a meta command found in the document *) +let process_back_meta_command ~newtip ~head oid aast = let valid = VCS.get_branch_pos head in + let old_parsing = Option.get @@ VCS.get_parsing_state oid in + + (* Merge in and discard all the branches currently open that were not open in `oid` *) + let { mine; others } = Backtrack.branches_of oid in List.iter (fun branch -> if not (List.mem_assoc branch (mine::others)) then ignore(merge_proof_branch ~valid aast VtDrop branch)) (VCS.branches ()); + + (* We add a node on top of every branch, to represent state aliasing *) VCS.checkout_shallowest_proof_branch (); let head = VCS.current_branch () in List.iter (fun b -> - if not(VCS.Branch.equal b head) then begin - VCS.checkout b; - VCS.commit (VCS.new_node ()) (Alias (oid,aast)); - end) + VCS.checkout b; + let id = if (VCS.Branch.equal b head) then Some newtip else None in + let proof_mode = VCS.get_proof_mode @@ VCS.cur_tip () in + let id = VCS.new_node ?id proof_mode () in + VCS.commit id (Alias (oid,aast)); + VCS.set_parsing_state id old_parsing) (VCS.branches ()); VCS.checkout_shallowest_proof_branch (); - VCS.commit id (Alias (oid,aast)); - Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok + Backtrack.record (); `Ok let get_allow_nested_proofs = Goptions.declare_bool_option_and_ref @@ -2873,6 +2930,7 @@ let get_allow_nested_proofs = ~key:Vernac_classifier.stm_allow_nested_proofs_option_name ~value:false +(** [process_transaction] adds a node in the document *) let process_transaction ~doc ?(newtip=Stateid.fresh ()) ({ verbose; loc; expr } as x) c = stm_pperr_endline (fun () -> str "{{{ processing: " ++ pr_ast x); @@ -2880,18 +2938,21 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) try let head = VCS.current_branch () in VCS.checkout head; + let head_parsing = + Option.get @@ VCS.(get_parsing_state (get_branch_pos head)) in + let proof_mode = VCS.(get_proof_mode (get_branch_pos head)) in let rc = begin stm_prerr_endline (fun () -> " classified as: " ^ Vernac_classifier.string_of_vernac_classification c); match c with (* Meta *) | VtMeta, _ -> - let id, w = Backtrack.undo_vernac_classifier expr ~doc in - process_back_meta_command ~newtip ~head id x w + let id = Backtrack.undo_vernac_classifier expr ~doc in + process_back_meta_command ~newtip ~head id x (* Query *) | VtQuery, w -> - let id = VCS.new_node ~id:newtip () in + let id = VCS.new_node ~id:newtip proof_mode () in let queue = if VCS.is_vio_doc () && VCS.((get_branch head).kind = `Master) && @@ -2899,10 +2960,11 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) then `SkipQueue else `MainQueue in VCS.commit id (mkTransCmd x [] false queue); - Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok + VCS.set_parsing_state id head_parsing; + Backtrack.record (); assert (w == VtLater); `Ok (* Proof *) - | VtStartProof (mode, guarantee, names), w -> + | VtStartProof (guarantee, names), w -> if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on." @@ -2912,39 +2974,22 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) |> Exninfo.iraise else - let id = VCS.new_node ~id:newtip () in + let proof_mode = Some (Vernacentries.get_default_proof_mode ()) in + let id = VCS.new_node ~id:newtip proof_mode () in let bname = VCS.mk_branch_name x in VCS.checkout VCS.Branch.master; if VCS.Branch.equal head VCS.Branch.master then begin VCS.commit id (Fork (x, bname, guarantee, names)); - VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1)) + VCS.branch bname (`Proof (VCS.proof_nesting () + 1)) end else begin - VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1)); + VCS.branch bname (`Proof (VCS.proof_nesting () + 1)); VCS.merge id ~ours:(Fork (x, bname, guarantee, names)) head end; - Proof_global.activate_proof_mode mode [@ocaml.warning "-3"]; - Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok - | VtProofMode _, VtLater -> - anomaly(str"VtProofMode must be executed VtNow.") - | VtProofMode mode, VtNow -> - let id = VCS.new_node ~id:newtip () in - VCS.commit id (mkTransCmd x [] false `MainQueue); - List.iter - (fun bn -> match VCS.get_branch bn with - | { VCS.root; kind = `Master; pos } -> () - | { VCS.root; kind = `Proof(_,d); pos } -> - VCS.delete_branch bn; - VCS.branch ~root ~pos bn (`Proof(mode,d)) - | { VCS.root; kind = `Edit(_,f,q,k,ob); pos } -> - VCS.delete_branch bn; - VCS.branch ~root ~pos bn (`Edit(mode,f,q,k,ob))) - (VCS.branches ()); - VCS.checkout_shallowest_proof_branch (); - Backtrack.record (); - ignore(finish ~doc:dummy_doc); - `Ok + VCS.set_parsing_state id head_parsing; + Backtrack.record (); assert (w == VtLater); `Ok + | VtProofStep { parallel; proof_block_detection = cblock }, w -> - let id = VCS.new_node ~id:newtip () in + let id = VCS.new_node ~id:newtip proof_mode () in let queue = match parallel with | `Yes(solve,abstract) -> `TacQueue (solve, abstract, ref false) @@ -2954,21 +2999,25 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) If/when and UI will make something useful with this piece of info, detection should occur here. detect_proof_block id cblock; *) - Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok + VCS.set_parsing_state id head_parsing; + Backtrack.record (); assert (w == VtLater); `Ok + | VtQed keep, w -> let valid = VCS.get_branch_pos head in - let rc = merge_proof_branch ~valid ~id:newtip x keep head in + let rc = + merge_proof_branch ~valid ~id:newtip x keep head in VCS.checkout_shallowest_proof_branch (); - Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); + Backtrack.record (); assert (w == VtLater); rc (* Side effect in a (still open) proof is replayed on all branches*) | VtSideff l, w -> - let id = VCS.new_node ~id:newtip () in - begin match (VCS.get_branch head).VCS.kind with - | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue); - | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue); - | `Proof _ -> + let id = VCS.new_node ~id:newtip proof_mode () in + let new_ids = + match (VCS.get_branch head).VCS.kind with + | `Edit _ -> VCS.commit id (mkTransCmd x l true `MainQueue); [] + | `Master -> VCS.commit id (mkTransCmd x l false `MainQueue); [] + | `Proof _ -> VCS.checkout VCS.Branch.master; VCS.commit id (mkTransCmd x l true `MainQueue); (* We can't replay a Definition since universes may be differently @@ -2976,10 +3025,27 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) let action = match Vernacprop.under_control x.expr with | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv | _ -> ReplayCommand x in - VCS.propagate_sideff ~action; - end; + VCS.propagate_sideff ~action + in VCS.checkout_shallowest_proof_branch (); - Backtrack.record (); if w == VtNow then ignore(finish ~doc:dummy_doc); `Ok + Backtrack.record (); + let parsing_state = + begin match w with + | VtNow -> + (* We need to execute to get the new parsing state *) + ignore(finish ~doc:dummy_doc); + let parsing = Vernacstate.Parser.cur_state () in + (* If execution has not been put in cache, we need to save the parsing state *) + if (VCS.get_info id).state == EmptyState then VCS.set_parsing_state id parsing; + parsing + | VtLater -> VCS.set_parsing_state id head_parsing; head_parsing + end + in + (* We save the parsing state on non-master branches *) + List.iter (fun id -> + if (VCS.get_info id).state == EmptyState then + VCS.set_parsing_state id parsing_state) new_ids; + `Ok (* Unknown: we execute it, check for open goals and propagate sideeff *) | VtUnknown, VtNow -> @@ -2991,7 +3057,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) |> State.exn_on ~valid:Stateid.dummy Stateid.dummy |> Exninfo.iraise else - let id = VCS.new_node ~id:newtip () in + let id = VCS.new_node ~id:newtip proof_mode () in let head_id = VCS.get_branch_pos head in let _st : unit = Reach.known_state ~doc ~cache:true head_id in (* ensure it is ok *) let step () = @@ -3009,9 +3075,8 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VernacInstance (_,_ , None, _) -> GuaranteesOpacity | _ -> Doesn'tGuaranteeOpacity in VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[])); - let proof_mode = default_proof_mode () in - VCS.branch bname (`Proof (proof_mode, VCS.proof_nesting () + 1)); - Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"]; + VCS.set_proof_mode id (Some (Vernacentries.get_default_proof_mode ())); + VCS.branch bname (`Proof (VCS.proof_nesting () + 1)); end else begin begin match (VCS.get_branch head).VCS.kind with | `Edit _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); @@ -3019,7 +3084,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | `Proof _ -> VCS.commit id (mkTransCmd x [] in_proof `MainQueue); (* We hope it can be replayed, but we can't really know *) - VCS.propagate_sideff ~action:(ReplayCommand x); + ignore(VCS.propagate_sideff ~action:(ReplayCommand x)); end; VCS.checkout_shallowest_proof_branch (); end in @@ -3028,6 +3093,17 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) | VtUnknown, VtLater -> anomaly(str"classifier: VtUnknown must imply VtNow.") + + | VtProofMode pm, VtNow -> + let proof_mode = Pvernac.lookup_proof_mode pm in + let id = VCS.new_node ~id:newtip proof_mode () in + VCS.commit id (mkTransCmd x [] false `MainQueue); + VCS.set_parsing_state id head_parsing; + Backtrack.record (); `Ok + + | VtProofMode _, VtLater -> + anomaly(str"classifier: VtProofMode must imply VtNow.") + end in let pr_rc rc = match rc with | `Ok -> Pp.(seq [str "newtip ("; str (Stateid.to_string (VCS.cur_tip ())); str ")"]) @@ -3051,45 +3127,10 @@ let get_ast ~doc id = let stop_worker n = Slaves.cancel_worker n -(* We must parse on top of a state id, it should be something like: - - - get parsing information for that state. - - feed the parsable / parser with the right parsing information. - - call the parser - - Now, the invariant in ensured by the callers, but this is a bit - problematic. -*) -exception End_of_input - -let parse_sentence ~doc sid pa = - (* XXX: Should this restore the previous state? - Using reach here to try to really get to the - proper state makes the error resilience code fail *) - (* Reach.known_state ~cache:`Yes sid; *) - let cur_tip = VCS.cur_tip () in - let real_tip = !State.cur_id in - if not (Stateid.equal sid cur_tip) then - user_err ~hdr:"Stm.parse_sentence" - (str "Currently, the parsing api only supports parsing at the tip of the document." ++ fnl () ++ - str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++ - str " but the current tip is: " ++ str (Stateid.to_string cur_tip)) ; - if not (Stateid.equal sid real_tip) && !Flags.debug && !stm_debug then - Feedback.msg_debug - (str "Warning, the real tip doesn't match the current tip." ++ - str "You wanted to parse at: " ++ str (Stateid.to_string sid) ++ - str " but the real tip is: " ++ str (Stateid.to_string real_tip) ++ fnl () ++ - str "This is usually due to use of Stm.observe to evaluate a state different than the tip. " ++ - str "All is good if not parsing changes occur between the two states, however if they do, a problem might occur."); - Flags.with_option Flags.we_are_parsing (fun () -> - try - match Pcoq.Entry.parse Pvernac.main_entry pa with - | None -> raise End_of_input - | Some (loc, cmd) -> CAst.make ~loc cmd - with e when CErrors.noncritical e -> - let (e, info) = CErrors.push e in - Exninfo.iraise (e, info)) - () +let parse_sentence ~doc sid ~entry pa = + let ps = Option.get @@ VCS.get_parsing_state sid in + let proof_mode = VCS.get_proof_mode sid in + Vernacstate.Parser.parse ps (entry proof_mode) pa (* You may need to know the len + indentation of previous command to compute * the indentation of the current one. @@ -3153,20 +3194,20 @@ let query ~doc ~at ~route s = State.purify (fun s -> if Stateid.equal at Stateid.dummy then ignore(finish ~doc:dummy_doc) else Reach.known_state ~doc ~cache:true at; - try - while true do - let { CAst.loc; v=ast } = parse_sentence ~doc at s in - let indentation, strlen = compute_indentation ?loc at in - let st = State.get_cached at in - let aast = { verbose = true; indentation; strlen; loc; expr = ast } in - ignore(stm_vernac_interp ~route at st aast) - done; - with - | End_of_input -> () - | exn -> - let iexn = CErrors.push exn in - Exninfo.iraise iexn - ) + let rec loop () = + match parse_sentence ~doc at ~entry:Pvernac.main_entry s with + | None -> () + | Some (loc, ast) -> + let indentation, strlen = compute_indentation ~loc at in + let st = State.get_cached at in + let aast = { + verbose = true; indentation; strlen; + loc = Some loc; expr = ast } in + ignore(stm_vernac_interp ~route at st aast); + loop () + in + loop () + ) s let edit_at ~doc id = @@ -3204,21 +3245,21 @@ let edit_at ~doc id = | { step = `Sideff (ReplayCommand _,id) } -> id | { step = `Sideff _ } -> tip | { next } -> master_for_br root next in - let reopen_branch start at_id mode qed_id tip old_branch = + let reopen_branch start at_id qed_id tip old_branch = let master_id, cancel_switch, keep = (* Hum, this should be the real start_id in the cluster and not next *) match VCS.visit qed_id with | { step = `Qed ({ fproof = Some (_,cs); keep },_) } -> start, cs, keep | _ -> anomaly (str "ProofTask not ending with Qed.") in VCS.branch ~root:master_id ~pos:id - VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch)); + VCS.edit_branch (`Edit (qed_id, master_id, keep, old_branch)); VCS.delete_boxes_of id; cancel_switch := true; Reach.known_state ~doc ~cache:(VCS.is_interactive ()) id; VCS.checkout_shallowest_proof_branch (); `Focus { stop = qed_id; start = master_id; tip } in let no_edit = function - | `Edit (pm, _,_,_,_) -> `Proof(pm,1) + | `Edit (_,_,_,_) -> `Proof 1 | x -> x in let backto id bn = List.iter VCS.delete_branch (VCS.branches ()); @@ -3244,17 +3285,17 @@ let edit_at ~doc id = let focused = List.exists ((=) VCS.edit_branch) (VCS.branches ()) in let branch_info = match snd (VCS.get_info id).vcs_backup with - | Some{ mine = bn, { VCS.kind = `Proof(m,_) }} -> Some(m,bn) - | Some{ mine = _, { VCS.kind = `Edit(m,_,_,_,bn) }} -> Some (m,bn) + | Some{ mine = bn, { VCS.kind = `Proof _ }} -> Some bn + | Some{ mine = _, { VCS.kind = `Edit(_,_,_,bn) }} -> Some bn | _ -> None in match focused, VCS.proof_task_box_of id, branch_info with | _, Some _, None -> assert false - | false, Some { qed = qed_id ; lemma = start }, Some(mode,bn) -> + | false, Some { qed = qed_id ; lemma = start }, Some bn -> let tip = VCS.cur_tip () in if has_failed qed_id && is_pure qed_id && not !cur_opt.async_proofs_never_reopen_branch - then reopen_branch start id mode qed_id tip bn + then reopen_branch start id qed_id tip bn else backto id (Some bn) - | true, Some { qed = qed_id }, Some(mode,bn) -> + | true, Some { qed = qed_id }, Some bn -> if on_cur_branch id then begin assert false end else if is_ancestor_of_cur_branch id then begin @@ -3273,7 +3314,7 @@ let edit_at ~doc id = end else begin anomaly(str"Cannot leave an `Edit branch open.") end - | false, None, Some(_,bn) -> backto id (Some bn) + | false, None, Some bn -> backto id (Some bn) | false, None, None -> backto id None in VCS.print (); diff --git a/stm/stm.mli b/stm/stm.mli index b6071fa56b..821ab59a43 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -93,16 +93,17 @@ val init_core : unit -> unit (** [new_doc opt] Creates a new document with options [opt] *) val new_doc : stm_init_options -> doc * Stateid.t -(** [parse_sentence sid pa] Reads a sentence from [pa] with parsing - state [sid] Returns [End_of_input] if the stream ends *) -val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Parsable.t -> - Vernacexpr.vernac_control CAst.t +(** [parse_sentence sid entry pa] Reads a sentence from [pa] with parsing state + [sid] and non terminal [entry]. [entry] receives in input the current proof + mode. [sid] should be associated with a valid parsing state (which may not + be the case if an error was raised at parsing time). *) +val parse_sentence : + doc:doc -> Stateid.t -> + entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.Parsable.t -> 'a (* Reminder: A parsable [pa] is constructed using [Pcoq.Parsable.t stream], where [stream : char Stream.t]. *) -exception End_of_input - (* [add ~ontop ?newtip verbose cmd] adds a new command [cmd] ontop of the state [ontop]. The [ontop] parameter just asserts that the GUI is on diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 09f531ce13..710ddb5571 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -15,8 +15,6 @@ open CAst open Vernacextend open Vernacexpr -let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] - let string_of_parallel = function | `Yes (solve,abs) -> "par" ^ if solve then "solve" else "" ^ if abs then "abs" else "" @@ -32,9 +30,9 @@ let string_of_vernac_type = function | VtProofStep { parallel; proof_block_detection } -> "ProofStep " ^ string_of_parallel parallel ^ Option.default "" proof_block_detection - | VtProofMode s -> "ProofMode " ^ s | VtQuery -> "Query" | VtMeta -> "Meta " + | VtProofMode _ -> "Proof Mode" let string_of_vernac_when = function | VtLater -> "Later" @@ -57,7 +55,7 @@ let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"] let options_affecting_stm_scheduling = [ Attributes.universe_polymorphism_option_name; stm_allow_nested_proofs_option_name; - Proof_global.proof_mode_opt_name; + Vernacentries.proof_mode_opt_name; ] let classify_vernac e = @@ -97,15 +95,15 @@ let classify_vernac e = | VernacSetOption (_, ["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) -> - VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater + VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i), VtLater | VernacDefinition (_,({v=i},_),ProveBody _) -> let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof(default_proof_mode (),guarantee, idents_of_name i), VtLater + VtStartProof(guarantee, idents_of_name i), VtLater | VernacStartTheoremProof (_,l) -> let ids = List.map (fun (({v=i}, _), _) -> i) l in let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in - VtStartProof (default_proof_mode (),guarantee,ids), VtLater + VtStartProof (guarantee,ids), VtLater | VernacFixpoint (discharge,l) -> let guarantee = if discharge = Decl_kinds.DoDischarge || poly then Doesn'tGuaranteeOpacity @@ -115,7 +113,7 @@ let classify_vernac e = List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof - then VtStartProof (default_proof_mode (),guarantee,ids), VtLater + then VtStartProof (guarantee,ids), VtLater else VtSideff ids, VtLater | VernacCoFixpoint (discharge,l) -> let guarantee = @@ -126,7 +124,7 @@ let classify_vernac e = List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof - then VtStartProof (default_proof_mode (),guarantee,ids), VtLater + then VtStartProof (guarantee,ids), VtLater else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> @@ -184,8 +182,8 @@ let classify_vernac e = | VernacSyntacticDefinition _ | VernacRequire _ | VernacImport _ | VernacInclude _ | VernacDeclareMLModule _ - | VernacContext _ (* TASSI: unsure *) - | VernacProofMode _ -> VtSideff [], VtNow + | VernacContext _ (* TASSI: unsure *) -> VtSideff [], VtNow + | VernacProofMode pm -> VtProofMode pm, VtNow (* These are ambiguous *) | VernacInstance _ -> VtUnknown, VtNow (* Stm will install a new classifier to handle these *) @@ -211,10 +209,10 @@ let classify_vernac e = | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match static_control_classifier e with | ( VtQuery | VtProofStep _ | VtSideff _ - | VtProofMode _ | VtMeta), _ as x -> x + | VtMeta), _ as x -> x | VtQed _, _ -> VtProofStep { parallel = `No; proof_block_detection = None }, - VtNow - | (VtStartProof _ | VtUnknown), _ -> VtQuery, VtLater) + VtLater + | (VtStartProof _ | VtUnknown | VtProofMode _), _ -> VtQuery, VtLater) in static_control_classifier e diff --git a/test-suite/ide/debug_ltac.fake b/test-suite/ide/debug_ltac.fake new file mode 100644 index 0000000000..aa68fad39e --- /dev/null +++ b/test-suite/ide/debug_ltac.fake @@ -0,0 +1,2 @@ +FAILADD { Debug On. } +ADD { Set Debug On. } diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 583ea0cb43..ba4bc070c6 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -52,7 +52,6 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] @@ -92,7 +91,6 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -myplus is not universe polymorphic Arguments are renamed to Z, t, n, m Argument Z is implicit and maximally inserted Argument scopes are [type_scope _ nat_scope nat_scope] diff --git a/test-suite/output/Binder.out b/test-suite/output/Binder.out index 6e27837b26..34558e9a6b 100644 --- a/test-suite/output/Binder.out +++ b/test-suite/output/Binder.out @@ -1,12 +1,8 @@ foo = fun '(x, y) => x + y : nat * nat -> nat - -foo is not universe polymorphic forall '(a, b), a /\ b : Prop foo = λ '(x, y), x + y : nat * nat → nat - -foo is not universe polymorphic ∀ '(a, b), a ∧ b : Prop diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index efcc299e82..cb835ab48d 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -7,7 +7,6 @@ fix F (t : t) : P t := : forall P : t -> Type, (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t -t_rect is not universe polymorphic Argument scopes are [function_scope function_scope _] = fun d : TT => match d with | {| f3 := b |} => b @@ -27,7 +26,6 @@ match Nat.eq_dec x y with end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y -proj is not universe polymorphic Argument scopes are [nat_scope nat_scope function_scope _ _] foo = fix foo (A : Type) (l : list A) {struct l} : option A := @@ -38,7 +36,6 @@ fix foo (A : Type) (l : list A) {struct l} : option A := end : forall A : Type, list A -> option A -foo is not universe polymorphic Argument scopes are [type_scope list_scope] uncast = fun (A : Type) (x : I A) => match x with @@ -46,12 +43,9 @@ fun (A : Type) (x : I A) => match x with end : forall A : Type, I A -> A -uncast is not universe polymorphic Argument scopes are [type_scope _] foo' = if A 0 then true else false : bool - -foo' is not universe polymorphic f = fun H : B => match H with @@ -62,8 +56,6 @@ match H with else fun _ : P false => Logic.I) x end : B -> True - -f is not universe polymorphic The command has indeed failed with message: Non exhaustive pattern-matching: no clause found for pattern gadtTy _ _ @@ -86,19 +78,14 @@ The constructor D (in type J) expects 3 arguments. lem1 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k - -lem1 is not universe polymorphic lem2 = fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl : forall k : bool, k = k -lem2 is not universe polymorphic Argument scope is [bool_scope] lem3 = fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl : forall k : nat * nat, k = k - -lem3 is not universe polymorphic 1 subgoal x : nat diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 0b0f501f9a..3b65003c29 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,7 +5,6 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -d2 is not universe polymorphic Arguments x, x0 are implicit Argument scopes are [nat_scope nat_scope _] map id (1 :: nil) diff --git a/test-suite/output/Load.out b/test-suite/output/Load.out index ebbd5d422b..0904d5540b 100644 --- a/test-suite/output/Load.out +++ b/test-suite/output/Load.out @@ -1,10 +1,6 @@ f = 2 : nat - -f is not universe polymorphic u = I : True - -u is not universe polymorphic The command has indeed failed with message: Files processed by Load cannot leave open proofs. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 71d92482d0..015dac2512 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -232,7 +232,6 @@ fun l : list nat => match l with end : list nat -> list nat -foo is not universe polymorphic Argument scope is [list_scope] Notation "'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope @@ -263,9 +262,5 @@ myfoo01 tt : list (list nat) amatch = mmatch 0 (with 0 => 1| 1 => 2 end) : unit - -amatch is not universe polymorphic alist = [0; 1; 2] : list nat - -alist is not universe polymorphic diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 94016e170b..72d5a9253a 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -45,5 +45,9 @@ fun x : nat => (x.-1)%pred : Prop ## : Prop +myAnd1 True True + : Prop +r 2 3 + : Prop Notation Cn := Foo.FooCn Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 309115848f..90babf9c55 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -165,6 +165,22 @@ Check ##. End H. +(* Fixing bugs reported by G. Gonthier in #9207 *) + +Module I. + +Definition myAnd A B := A /\ B. +Notation myAnd1 A := (myAnd A). +Check myAnd1 True True. + +Set Warnings "-auto-template". + +Record Pnat := {inPnat :> nat -> Prop}. +Axiom r : nat -> Pnat. +Check r 2 3. + +End I. + (* Fixing a bug reported by G. Gonthier in #9207 *) Module J. diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index bdbc5a5960..8a6d94c732 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -1,29 +1,20 @@ swap = fun '(x, y) => (y, x) : A * B -> B * A - -swap is not universe polymorphic fun '(x, y) => (y, x) : A * B -> B * A forall '(x, y), swap (x, y) = (y, x) : Prop proj_informative = fun '(exist _ x _) => x : A : {x : A | P x} -> A - -proj_informative is not universe polymorphic foo = fun '(Bar n b tt p) => if b then n + p else n - p : Foo -> nat - -foo is not universe polymorphic baz = fun '(Bar n1 _ tt p1) '(Bar _ _ tt _) => n1 + p1 : Foo -> Foo -> nat - -baz is not universe polymorphic swap = fun (A B : Type) '(x, y) => (y, x) : forall A B : Type, A * B -> B * A -swap is not universe polymorphic Arguments A, B are implicit and maximally inserted Argument scopes are [type_scope type_scope _] fun (A B : Type) '(x, y) => swap (x, y) = (y, x) @@ -42,8 +33,6 @@ both_z = fun pat : nat * nat => let '(n, p) as x := pat return (F x) in (Z n, Z p) : F (n, p) : forall pat : nat * nat, F pat - -both_z is not universe polymorphic fun '(x, y) '(z, t) => swap (x, y) = (z, t) : A * B -> B * A -> Prop forall '(x, y) '(z, t), swap (x, y) = (z, t) @@ -53,7 +42,6 @@ fun (pat : nat) '(x, y) => x + y = pat f = fun x : nat => x + x : nat -> nat -f is not universe polymorphic Argument scope is [nat_scope] fun x : nat => x + x : nat -> nat diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index da1fca7134..ab4172711e 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -46,7 +46,6 @@ fix add (n m : nat) {struct n} : nat := end : nat -> nat -> nat -Nat.add is not universe polymorphic Argument scopes are [nat_scope nat_scope] Nat.add : nat -> nat -> nat @@ -86,7 +85,6 @@ Argument x is implicit and maximally inserted Expands to: Constant PrintInfos.bar *** [ bar : foo ] -bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out index c7e6ef950e..9366113c0c 100644 --- a/test-suite/output/StringSyntax.out +++ b/test-suite/output/StringSyntax.out @@ -433,7 +433,6 @@ end P "167" -> P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b -byte_rect is not universe polymorphic Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] byte_rec = fun P : byte -> Set => byte_rect P @@ -608,7 +607,6 @@ fun P : byte -> Set => byte_rect P P "167" -> P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b -byte_rec is not universe polymorphic Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] byte_ind = fun (P : byte -> Prop) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") @@ -1045,7 +1043,6 @@ end P "167" -> P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b -byte_ind is not universe polymorphic Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] "000" : byte diff --git a/test-suite/output/TranspModtype.out b/test-suite/output/TranspModtype.out index 67b65d4b81..f94ed64234 100644 --- a/test-suite/output/TranspModtype.out +++ b/test-suite/output/TranspModtype.out @@ -1,15 +1,7 @@ TrM.A = M.A : Set - -TrM.A is not universe polymorphic OpM.A = M.A : Set - -OpM.A is not universe polymorphic TrM.B = M.B : Set - -TrM.B is not universe polymorphic *** [ OpM.B : Set ] - -OpM.B is not universe polymorphic diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 0bd6ade690..a960fe3441 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -9,7 +9,6 @@ fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p : forall A : Type@{u}, PWrap@{u} A -> A (* u |= *) -punwrap is universe polymorphic Argument scopes are [type_scope _] Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } @@ -20,33 +19,26 @@ fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap : forall A : Type@{u}, RWrap@{u} A -> A (* u |= *) -runwrap is universe polymorphic Argument scopes are [type_scope _] Wrap@{u} = fun A : Type@{u} => A : Type@{u} -> Type@{u} (* u |= *) -Wrap is universe polymorphic Argument scope is [type_scope] wrap@{u} = fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap : forall A : Type@{u}, Wrap@{u} A -> A (* u |= *) -wrap is universe polymorphic Arguments A, Wrap are implicit and maximally inserted Argument scopes are [type_scope _] bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) - -bar is universe polymorphic foo@{u UnivBinders.17 v} = Type@{UnivBinders.17} -> Type@{v} -> Type@{u} : Type@{max(u+1,UnivBinders.17+1,v+1)} (* u UnivBinders.17 v |= *) - -foo is universe polymorphic Type@{i} -> Type@{j} : Type@{max(i+1,j+1)} (* {j i} |= *) @@ -56,8 +48,6 @@ Type@{i} -> Type@{j} mono = Type@{mono.u} : Type@{mono.u+1} (* {mono.u} |= *) - -mono is not universe polymorphic mono : Type@{mono.u+1} Type@{mono.u} @@ -78,22 +68,16 @@ bobmorane = let tt := Type@{UnivBinders.32} in let ff := Type@{UnivBinders.34} in tt -> ff : Type@{max(UnivBinders.31,UnivBinders.33)} - -bobmorane is not universe polymorphic The command has indeed failed with message: Universe u already bound. foo@{E M N} = Type@{M} -> Type@{N} -> Type@{E} : Type@{max(E+1,M+1,N+1)} (* E M N |= *) - -foo is universe polymorphic foo@{u UnivBinders.17 v} = Type@{UnivBinders.17} -> Type@{v} -> Type@{u} : Type@{max(u+1,UnivBinders.17+1,v+1)} (* u UnivBinders.17 v |= *) - -foo is universe polymorphic Inductive Empty@{E} : Type@{E} := Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } @@ -119,26 +103,18 @@ bind_univs.mono = Type@{bind_univs.mono.u} : Type@{bind_univs.mono.u+1} (* {bind_univs.mono.u} |= *) - -bind_univs.mono is not universe polymorphic bind_univs.poly@{u} = Type@{u} : Type@{u+1} (* u |= *) - -bind_univs.poly is universe polymorphic insec@{v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* v |= *) - -insec is universe polymorphic Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} For inseccstr: Argument scope is [type_scope] insec@{u v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) - -insec is universe polymorphic Inductive insecind@{u k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{u k} @@ -146,29 +122,19 @@ For inseccstr: Argument scope is [type_scope] insec2@{u} = Prop : Type@{Set+1} (* u |= *) - -insec2 is universe polymorphic inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) - -inmod is universe polymorphic SomeMod.inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) - -SomeMod.inmod is universe polymorphic inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) - -inmod is universe polymorphic Applied.infunct@{u v} = inmod@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) - -Applied.infunct is universe polymorphic axfoo@{i UnivBinders.56 UnivBinders.57} : Type@{UnivBinders.56} -> Type@{i} (* i UnivBinders.56 UnivBinders.57 |= *) diff --git a/test-suite/output/goal_output.out b/test-suite/output/goal_output.out index 20568f742a..773533a8d3 100644 --- a/test-suite/output/goal_output.out +++ b/test-suite/output/goal_output.out @@ -1,11 +1,7 @@ Nat.t = nat : Set - -Nat.t is not universe polymorphic Nat.t = nat : Set - -Nat.t is not universe polymorphic 1 subgoal ============================ diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index f545ca679c..f7ffd1959a 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -4,8 +4,6 @@ fun e : option L => match e with | None => None end : option L -> option L - -P is not universe polymorphic fun n : nat => let y : T n := A n in ?t ?x : T n : forall n : nat, T n where diff --git a/test-suite/ssr/ipat_replace.v b/test-suite/ssr/ipat_replace.v new file mode 100644 index 0000000000..528f33f30d --- /dev/null +++ b/test-suite/ssr/ipat_replace.v @@ -0,0 +1,17 @@ +Require Import ssreflect. + +Lemma test : True. +Proof. +have H : True. + by []. +have {}H : True. + by apply: H. +by apply: H. +Qed. + +Lemma test2 (H : True) : False -> False -> False. +Proof. +move=> {}W. +move=> {}H. +by apply: H. +Qed. diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v index 5650dba236..81469d79c3 100644 --- a/test-suite/success/CompatCurrentFlag.v +++ b/test-suite/success/CompatCurrentFlag.v @@ -1,3 +1,3 @@ -(* -*- coq-prog-args: ("-compat" "8.9") -*- *) +(* -*- coq-prog-args: ("-compat" "8.10") -*- *) (** Check that the current compatibility flag actually requires the relevant modules. *) -Import Coq.Compat.Coq89. +Import Coq.Compat.Coq810. diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v index 37d50ee67d..afeb57f9f2 100644 --- a/test-suite/success/CompatOldFlag.v +++ b/test-suite/success/CompatOldFlag.v @@ -1,5 +1,5 @@ -(* -*- coq-prog-args: ("-compat" "8.7") -*- *) +(* -*- coq-prog-args: ("-compat" "8.8") -*- *) (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq810. Import Coq.Compat.Coq89. Import Coq.Compat.Coq88. -Import Coq.Compat.Coq87. diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v new file mode 100644 index 0000000000..1f62635f50 --- /dev/null +++ b/test-suite/success/CompatOldOldFlag.v @@ -0,0 +1,6 @@ +(* -*- coq-prog-args: ("-compat" "8.7") -*- *) +(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq810. +Import Coq.Compat.Coq89. +Import Coq.Compat.Coq88. +Import Coq.Compat.Coq87. diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v index 9981388381..c8f75915c8 100644 --- a/test-suite/success/CompatPreviousFlag.v +++ b/test-suite/success/CompatPreviousFlag.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-compat" "8.8") -*- *) +(* -*- coq-prog-args: ("-compat" "8.9") -*- *) (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *) +Import Coq.Compat.Coq810. Import Coq.Compat.Coq89. -Import Coq.Compat.Coq88. diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh index 02a2348450..61273c4f37 100755 --- a/test-suite/tools/update-compat/run.sh +++ b/test-suite/tools/update-compat/run.sh @@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )" # we assume that the script lives in test-suite/tools/update-compat/, # and that update-compat.py lives in dev/tools/ cd "${SCRIPT_DIR}/../../.." -dev/tools/update-compat.py --assert-unchanged --cur-version=8.9 || exit $? +dev/tools/update-compat.py --assert-unchanged --master || exit $? diff --git a/theories/Compat/Coq810.v b/theories/Compat/Coq810.v new file mode 100644 index 0000000000..f10201661e --- /dev/null +++ b/theories/Compat/Coq810.v @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Compatibility file for making Coq act similar to Coq v8.10 *) diff --git a/theories/Compat/Coq89.v b/theories/Compat/Coq89.v index decb5c7519..05d63d9a47 100644 --- a/theories/Compat/Coq89.v +++ b/theories/Compat/Coq89.v @@ -11,5 +11,7 @@ (** Compatibility file for making Coq act similar to Coq v8.9 *) Local Set Warnings "-deprecated". +Require Export Coq.Compat.Coq810. + Unset Private Polymorphic Universes. Set Refine Instance Mode. diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 0a32879764..eaa050bdce 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -165,7 +165,8 @@ let add_compat_require opts v = match v with | Flags.V8_7 -> add_vo_require opts "Coq.Compat.Coq87" None (Some false) | Flags.V8_8 -> add_vo_require opts "Coq.Compat.Coq88" None (Some false) - | Flags.Current -> add_vo_require opts "Coq.Compat.Coq89" None (Some false) + | Flags.V8_9 -> add_vo_require opts "Coq.Compat.Coq89" None (Some false) + | Flags.Current -> add_vo_require opts "Coq.Compat.Coq810" None (Some false) let set_batch_mode opts = (* XXX: This should be in the argument record *) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index e58b9ccac7..cdbe444e5b 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -243,7 +243,7 @@ let set_prompt prompt = let parse_to_dot = let rec dot st = match Stream.next st with | Tok.KEYWORD ("."|"...") -> () - | Tok.EOI -> raise Stm.End_of_input + | Tok.EOI -> () | _ -> dot st in Pcoq.Entry.of_parser "Coqtoplevel.dot" dot @@ -257,12 +257,12 @@ let rec discard_to_dot () = Pcoq.Entry.parse parse_to_dot top_buffer.tokens with | Gramlib.Plexing.Error _ | CLexer.Error.E _ -> discard_to_dot () - | Stm.End_of_input -> raise Stm.End_of_input | e when CErrors.noncritical e -> () let read_sentence ~state input = (* XXX: careful with ignoring the state Eugene!*) - try G_toplevel.parse_toplevel input + let open Vernac.State in + try Stm.parse_sentence ~doc:state.doc state.sid ~entry:G_toplevel.vernac_toplevel input with reraise -> let reraise = CErrors.push reraise in discard_to_dot (); @@ -366,7 +366,6 @@ let top_goal_print ~doc c oldp newp = let msg = CErrors.iprint (e, info) in TopErr.print_error_for_buffer ?loc Feedback.Error msg top_buffer -(* Careful to keep this loop tail-rec *) let rec vernac_loop ~state = let open CAst in let open Vernac.State in @@ -379,26 +378,30 @@ let rec vernac_loop ~state = try let input = top_buffer.tokens in match read_sentence ~state input with - | {v=VernacBacktrack(bid,_,_)} -> + | Some { v = VernacBacktrack(bid,_,_) } -> let bid = Stateid.of_int bid in let doc, res = Stm.edit_at ~doc:state.doc bid in assert (res = `NewTip); let state = { state with doc; sid = bid } in vernac_loop ~state - | {v=VernacQuit} -> + | Some { v = VernacQuit } -> exit 0 - | {v=VernacDrop} -> + + | Some { v = VernacDrop } -> if Mltop.is_ocaml_top() then (drop_last_doc := Some state; state) else (Feedback.msg_warning (str "There is no ML toplevel."); vernac_loop ~state) - | {v=VernacControl c; loc} -> + + | Some { v = VernacControl c; loc } -> let nstate = Vernac.process_expr ~state (make ?loc c) in top_goal_print ~doc:state.doc c state.proof nstate.proof; vernac_loop ~state:nstate + + | None -> + top_stderr (fnl ()); exit 0 + with - | Stm.End_of_input -> - top_stderr (fnl ()); exit 0 (* Exception printing should be done by the feedback listener, however this is not yet ready so we rely on the exception for now. *) diff --git a/toplevel/g_toplevel.mlg b/toplevel/g_toplevel.mlg index 5aba3d6b0b..7f1cca277e 100644 --- a/toplevel/g_toplevel.mlg +++ b/toplevel/g_toplevel.mlg @@ -21,7 +21,7 @@ type vernac_toplevel = | VernacControl of vernac_control module Toplevel_ : sig - val vernac_toplevel : vernac_toplevel CAst.t Entry.t + val vernac_toplevel : vernac_toplevel CAst.t option Entry.t end = struct let gec_vernac s = Entry.create ("toplevel:" ^ s) let vernac_toplevel = gec_vernac "vernac_toplevel" @@ -34,14 +34,14 @@ open Toplevel_ GRAMMAR EXTEND Gram GLOBAL: vernac_toplevel; vernac_toplevel: FIRST - [ [ IDENT "Drop"; "." -> { CAst.make VernacDrop } - | IDENT "Quit"; "." -> { CAst.make VernacQuit } + [ [ IDENT "Drop"; "." -> { Some (CAst.make VernacDrop) } + | IDENT "Quit"; "." -> { Some (CAst.make VernacQuit) } | IDENT "Backtrack"; n = natural ; m = natural ; p = natural; "." -> - { CAst.make (VernacBacktrack (n,m,p)) } - | cmd = Pvernac.main_entry -> + { Some (CAst.make (VernacBacktrack (n,m,p))) } + | cmd = Pvernac.Vernac_.main_entry -> { match cmd with - | None -> raise Stm.End_of_input - | Some (loc,c) -> CAst.make ~loc (VernacControl c) } + | None -> None + | Some (loc,c) -> Some (CAst.make ~loc (VernacControl c)) } ] ] ; @@ -49,6 +49,8 @@ END { -let parse_toplevel pa = Pcoq.Entry.parse vernac_toplevel pa +let vernac_toplevel pm = + Pvernac.Unsafe.set_tactic_entry pm; + vernac_toplevel } diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index d8465aac27..45ca658857 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -68,10 +68,8 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = if ntip <> `NewTip then anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!"); - (* Due to bug #5363 we cannot use observe here as we should, - it otherwise reveals bugs *) - (* Stm.observe nsid; *) - let ndoc = if check then Stm.finish ~doc else doc in + (* Force the command *) + let ndoc = if check then Stm.observe ~doc nsid else doc in let new_proof = Proof_global.give_me_the_proof_opt () in { state with doc = ndoc; sid = nsid; proof = new_proof; } with reraise -> @@ -92,51 +90,37 @@ let load_vernac_core ~echo ~check ~interactive ~state file = let in_echo = if echo then Some (open_utf8_file_in file) else None in let input_cleanup () = close_in in_chan; Option.iter close_in in_echo in - let in_pa = Pcoq.Parsable.make ~file:(Loc.InFile file) (Stream.of_channel in_chan) in - let rstate = ref state in - (* For beautify, list of parsed sids *) - let rids = ref [] in + let in_pa = + Pcoq.Parsable.make ~file:(Loc.InFile file) (Stream.of_channel in_chan) in let open State in - try - (* we go out of the following infinite loop when a End_of_input is - * raised, which means that we raised the end of the file being loaded *) - while true do - let { CAst.loc; _ } as ast = - Stm.parse_sentence ~doc:!rstate.doc !rstate.sid in_pa - (* If an error in parsing occurs, we propagate the exception - so the caller of load_vernac will take care of it. However, - in the future it could be possible that we want to handle - all the errors as feedback events, thus in this case we - should relay the exception here for convenience. A - possibility is shown below, however we may want to refactor - this code: - - try Stm.parse_sentence !rsid in_pa - with - | any when not is_end_of_input any -> - let (e, info) = CErrors.push any in - let loc = Loc.get_loc info in - let msg = CErrors.iprint (e, info) in - Feedback.msg_error ?loc msg; - iraise (e, info) - *) - in - (* Printing of vernacs *) - Option.iter (vernac_echo ?loc) in_echo; - - checknav_simple ast; - let state = Flags.silently (interp_vernac ~check ~interactive ~state:!rstate) ast in - rids := state.sid :: !rids; - rstate := state; - done; - input_cleanup (); - !rstate, !rids, Pcoq.Parsable.comment_state in_pa + + (* ids = For beautify, list of parsed sids *) + let rec loop state ids = + match + Stm.parse_sentence + ~doc:state.doc ~entry:Pvernac.main_entry state.sid in_pa + with + | None -> + input_cleanup (); + state, ids, Pcoq.Parsable.comment_state in_pa + | Some (loc, ast) -> + let ast = CAst.make ~loc ast in + + (* Printing of AST for -compile-verbose *) + Option.iter (vernac_echo ~loc) in_echo; + + checknav_simple ast; + + let state = + Flags.silently (interp_vernac ~check ~interactive ~state) ast in + + loop state (state.sid :: ids) + in + try loop state [] with any -> (* whatever the exception *) let (e, info) = CErrors.push any in input_cleanup (); - match e with - | Stm.End_of_input -> !rstate, !rids, Pcoq.Parsable.comment_state in_pa - | reraise -> iraise (e, info) + iraise (e, info) let process_expr ~state loc_ast = checknav_deep loc_ast; diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 3bc4aecdb1..79adefdcf7 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -61,7 +61,8 @@ let make_bullet s = | _ -> assert false let parse_compat_version = let open Flags in function - | "8.9" -> Current + | "8.10" -> Current + | "8.9" -> V8_9 | "8.8" -> V8_8 | "8.7" -> V8_7 | ("8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 8f155adb8a..0dfbba0e83 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -340,7 +340,7 @@ let start_proof id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c | None -> standard_proof_terminator ?hook compute_guard | Some terminator -> terminator ?hook compute_guard in - let sign = + let sign = match sign with | Some sign -> sign | None -> initialize_named_context_for_proof () diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index a647b2ef73..0e46df2320 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -12,6 +12,27 @@ open Pcoq let uvernac = create_universe "vernac" +type proof_mode = string + +(* Tactic parsing modes *) +let register_proof_mode, find_proof_mode, lookup_proof_mode = + let proof_mode : (string, Vernacexpr.vernac_expr Entry.t) Hashtbl.t = + Hashtbl.create 19 in + let register_proof_mode ename e = Hashtbl.add proof_mode ename e; ename in + let find_proof_mode ename = + try Hashtbl.find proof_mode ename + with Not_found -> + CErrors.anomaly Pp.(str "proof mode not found: " ++ str ename) in + let lookup_proof_mode name = + if Hashtbl.mem proof_mode name then Some name + else None + in + register_proof_mode, find_proof_mode, lookup_proof_mode + +let proof_mode_to_string name = name + +let command_entry_ref = ref None + module Vernac_ = struct let gec_vernac s = Entry.create ("vernac:" ^ s) @@ -39,17 +60,24 @@ module Vernac_ = ] in Pcoq.grammar_extend main_entry None (None, [None, None, rule]) - let command_entry_ref = ref noedit_mode + let select_tactic_entry spec = + match spec with + | None -> noedit_mode + | Some ename -> find_proof_mode ename + let command_entry = Pcoq.Entry.of_parser "command_entry" - (fun strm -> Pcoq.Entry.parse_token_stream !command_entry_ref strm) + (fun strm -> Pcoq.Entry.parse_token_stream (select_tactic_entry !command_entry_ref) strm) end -let main_entry = Vernac_.main_entry +module Unsafe = struct + let set_tactic_entry oname = command_entry_ref := oname +end -let set_command_entry e = Vernac_.command_entry_ref := e -let get_command_entry () = !Vernac_.command_entry_ref +let main_entry proof_mode = + Unsafe.set_tactic_entry proof_mode; + Vernac_.main_entry let () = register_grammar Genredexpr.wit_red_expr (Vernac_.red_expr); diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index b2f8f71462..fa251281dc 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -14,6 +14,8 @@ open Vernacexpr val uvernac : gram_universe +type proof_mode + module Vernac_ : sig val gallina : vernac_expr Entry.t @@ -24,13 +26,31 @@ module Vernac_ : val rec_definition : (fixpoint_expr * decl_notation list) Entry.t val noedit_mode : vernac_expr Entry.t val command_entry : vernac_expr Entry.t + val main_entry : (Loc.t * vernac_control) option Entry.t val red_expr : raw_red_expr Entry.t val hint_info : Hints.hint_info_expr Entry.t end +(* To be removed when the parser is made functional wrt the tactic + * non terminal *) +module Unsafe : sig + (* To let third party grammar entries reuse Vernac_ and + * do something with the proof mode *) + val set_tactic_entry : proof_mode option -> unit +end + (** The main entry: reads an optional vernac command *) -val main_entry : (Loc.t * vernac_control) option Entry.t +val main_entry : proof_mode option -> (Loc.t * vernac_control) option Entry.t + +(** Grammar entry for tactics: proof mode(s). + By default Coq's grammar has an empty entry (non-terminal) for + tactics. A plugin can register its non-terminal by providing a name + and a grammar entry. + + For example the Ltac plugin register the "Classic" grammar + entry for parsing its tactics. + *) -(** Handling of the proof mode entry *) -val get_command_entry : unit -> vernac_expr Entry.t -val set_command_entry : vernac_expr Entry.t -> unit +val register_proof_mode : string -> Vernacexpr.vernac_expr Entry.t -> proof_mode +val lookup_proof_mode : string -> proof_mode option +val proof_mode_to_string : proof_mode -> string diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 26859cd2cf..996fe320f9 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -489,6 +489,28 @@ let vernac_notation ~module_local = let vernac_custom_entry ~module_local s = Metasyntax.declare_custom_entry module_local s +(* Default proof mode, to be set at the beginning of proofs for + programs that cannot be statically classified. *) +let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode) +let get_default_proof_mode () = !default_proof_mode + +let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode +let set_default_proof_mode_opt name = + default_proof_mode := + match Pvernac.lookup_proof_mode name with + | Some pm -> pm + | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name)) + +let proof_mode_opt_name = ["Default";"Proof";"Mode"] +let () = + Goptions.declare_string_option Goptions.{ + optdepr = false; + optname = "default proof mode" ; + optkey = proof_mode_opt_name; + optread = get_default_proof_mode_opt; + optwrite = set_default_proof_mode_opt; + } + (***********) (* Gallina *) @@ -2115,13 +2137,9 @@ exception End_of_input let vernac_load interp fname = if Proof_global.there_are_pending_proofs () then CErrors.user_err Pp.(str "Load is not supported inside proofs."); - let interp x = - let proof_mode = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] in - Proof_global.activate_proof_mode proof_mode [@ocaml.warning "-3"]; - interp x in - let parse_sentence = Flags.with_option Flags.we_are_parsing + let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing (fun po -> - match Pcoq.Entry.parse Pvernac.main_entry po with + match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with | Some x -> x | None -> raise End_of_input) in let fname = @@ -2132,7 +2150,15 @@ let vernac_load interp fname = let in_chan = open_utf8_file_in longfname in Pcoq.Parsable.make ~file:(Loc.InFile longfname) (Stream.of_channel in_chan) in begin - try while true do interp (snd (parse_sentence input)) done + try while true do + let proof_mode = + if Proof_global.there_are_pending_proofs () then + Some (get_default_proof_mode ()) + else + None + in + interp (snd (parse_sentence proof_mode input)); + done with End_of_input -> () end; (* If Load left a proof open, we fail too. *) @@ -2312,8 +2338,7 @@ let interp ?proof ~atts ~st c = Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings); Option.iter vernac_set_end_tac tac; Option.iter vernac_set_used_variables using - | VernacProofMode mn -> unsupported_attributes atts; - Proof_global.set_proof_mode mn [@ocaml.warning "-3"] + | VernacProofMode mn -> unsupported_attributes atts; () (* Extensions *) | VernacExtend (opn,args) -> diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 8d8d7cfcf0..4fbd3849b0 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -10,6 +10,11 @@ val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit +(** Default proof mode set by `start_proof` *) +val get_default_proof_mode : unit -> Pvernac.proof_mode + +val proof_mode_opt_name : string list + (** Vernacular entries *) val vernac_require : Libnames.qualid option -> bool option -> Libnames.qualid list -> unit diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index 05687afd8b..f5cf3401d0 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -29,15 +29,15 @@ type vernac_type = parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; proof_block_detection : proof_block_name option } - (* To be removed *) - | VtProofMode of string (* Queries are commands assumed to be "pure", that is to say, they don't modify the interpretation state. *) | VtQuery + (* Commands that change the current proof mode *) + | VtProofMode of string (* To be removed *) | VtMeta | VtUnknown -and vernac_start = string * opacity_guarantee * Names.Id.t list +and vernac_start = opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 0d43eb1ee8..118907c31b 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -45,15 +45,15 @@ type vernac_type = parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ]; proof_block_detection : proof_block_name option } - (* To be removed *) - | VtProofMode of string (* Queries are commands assumed to be "pure", that is to say, they don't modify the interpretation state. *) | VtQuery + (* Commands that change the current proof mode *) + | VtProofMode of string (* To be removed *) | VtMeta | VtUnknown -and vernac_start = string * opacity_guarantee * Names.Id.t list +and vernac_start = opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 61540024ef..c691dc8559 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -8,10 +8,30 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +module Parser = struct + + type state = Pcoq.frozen_t + + let init () = Pcoq.freeze ~marshallable:false + + let cur_state () = Pcoq.freeze ~marshallable:false + + let parse ps entry pa = + Pcoq.unfreeze ps; + Flags.with_option Flags.we_are_parsing (fun () -> + try Pcoq.Entry.parse entry pa + with e when CErrors.noncritical e -> + let (e, info) = CErrors.push e in + Exninfo.iraise (e, info)) + () + +end + type t = { - system : States.state; (* summary + libstack *) - proof : Proof_global.t; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) + parsing: Parser.state; + system : States.state; (* summary + libstack *) + proof : Proof_global.t; (* proof state *) + shallow : bool; (* is the state trimmed down (libstack) *) } let s_cache = ref None @@ -37,11 +57,13 @@ let freeze_interp_state ~marshallable = { system = update_cache s_cache (States.freeze ~marshallable); proof = update_cache s_proof (Proof_global.freeze ~marshallable); shallow = false; + parsing = Parser.cur_state (); } -let unfreeze_interp_state { system; proof } = +let unfreeze_interp_state { system; proof; parsing } = do_if_not_cached s_cache States.unfreeze system; - do_if_not_cached s_proof Proof_global.unfreeze proof + do_if_not_cached s_proof Proof_global.unfreeze proof; + Pcoq.unfreeze parsing let make_shallow st = let lib = States.lib_of_state st.system in diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index ed20cb935a..581c23386a 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -8,10 +8,21 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +module Parser : sig + type state + + val init : unit -> state + val cur_state : unit -> state + + val parse : state -> 'a Pcoq.Entry.t -> Pcoq.Parsable.t -> 'a + +end + type t = { - system : States.state; (* summary + libstack *) - proof : Proof_global.t; (* proof state *) - shallow : bool (* is the state trimmed down (libstack) *) + parsing: Parser.state; + system : States.state; (* summary + libstack *) + proof : Proof_global.t; (* proof state *) + shallow : bool; (* is the state trimmed down (libstack) *) } val freeze_interp_state : marshallable:bool -> t |