diff options
25 files changed, 235 insertions, 143 deletions
diff --git a/configure.ml b/configure.ml index 60ba8b1101..d4521a7872 100644 --- a/configure.ml +++ b/configure.ml @@ -919,16 +919,16 @@ let datadir,datadirsuffix = let (_,_,d,s) = select "DATADIR" in d,s let cflags_dflt = "-Wall -Wno-unused -g -O2 -fexcess-precision=standard" -let cflags_sse2 = ["-msse2"; "-mfpmath=sse"] +let cflags_sse2 = "-msse2 -mfpmath=sse" let cflags, sse2_math = let _, slurp = (* Test SSE2_MATH support <https://stackoverflow.com/a/45667927> *) - tryrun "cc" (["-march=native"; "-dM"; "-E"] - @ cflags_sse2 - @ [coqtop/"kernel/byterun/coq_interp.h"] (* any file *)) in + tryrun camlexec.find + ["ocamlc"; "-ccopt"; cflags_dflt ^ " -march=native -dM -E " ^ cflags_sse2; + "-c"; coqtop/"dev/header.c"] in (* any file *) if List.exists (fun line -> starts_with line "#define __SSE2_MATH__ 1") slurp - then (cflags_dflt ^ " " ^ String.concat " " cflags_sse2, true) + then (cflags_dflt ^ " " ^ cflags_sse2, true) else (cflags_dflt, false) (** Test at configure time that no harmful double rounding seems to diff --git a/dev/tools/update-compat.py b/dev/tools/update-compat.py index c7bb36b6d3..7312c2a5af 100755 --- a/dev/tools/update-compat.py +++ b/dev/tools/update-compat.py @@ -1,6 +1,8 @@ -#!/usr/bin/env python2 +#!/usr/bin/env python3 from __future__ import with_statement +from __future__ import print_function import os, re, sys, subprocess +from io import open # When passed `--release`, this script sets up Coq to support three # `-compat` flag arguments. If executed manually, this would consist @@ -84,17 +86,25 @@ BUG_HEADER = r"""(* DO NOT MODIFY THIS FILE DIRECTLY *) (* It is autogenerated by %s. *) """ % os.path.relpath(os.path.realpath(__file__), ROOT_PATH) +def get_file_lines(file_name): + with open(file_name, 'rb') as f: + lines = f.readlines() + return [line.decode('utf-8') for line in lines] + +def get_file(file_name): + return ''.join(get_file_lines(file_name)) + def get_header(): - with open(HEADER_PATH, 'r') as f: return f.read() + return get_file(HEADER_PATH) 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 fatal_error(msg): + if hasattr(sys.stderr, 'buffer'): + sys.stderr.buffer.write(msg.encode("utf-8")) + else: + sys.stderr.write(msg.encode("utf-8")) + sys.exit(1) def maybe_git_add(local_path, suggest_add=True, **args): if args['git_add']: @@ -114,11 +124,10 @@ def maybe_git_rm(local_path, **args): def get_version(cur_version=None): if cur_version is not None: return cur_version - with open(CONFIGURE_PATH, 'r') as f: - for line in f.readlines(): - found = re.findall(r'let coq_version = "([0-9]+\.[0-9]+)', line) - if len(found) > 0: - return found[0] + for line in get_file_lines(CONFIGURE_PATH): + found = re.findall(r'let coq_version = "([0-9]+\.[0-9]+)', line) + if len(found) > 0: + return found[0] raise Exception("No line 'let coq_version = \"X.X' found in %s" % os.path.relpath(CONFIGURE_PATH, ROOT_PATH)) def compat_name_to_version_name(compat_file_name): @@ -132,8 +141,7 @@ def version_name_to_compat_name(v, ext='.v'): # returns (lines of compat files, lines of not compat files def get_doc_index_lines(): - with open(DOC_INDEX_PATH, 'r') as f: - lines = f.readlines() + lines = get_file_lines(DOC_INDEX_PATH) return (tuple(line for line in lines if 'theories/Compat/Coq' in line), tuple(line for line in lines if 'theories/Compat/Coq' not in line)) @@ -183,7 +191,7 @@ def update_if_changed(contents, new_contents, path, exn_string='%s changed!', su 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: + with open(path, 'w', encoding='utf-8') as f: f.write(new_contents) maybe_git_add(os.path.relpath(path, ROOT_PATH), suggest_add=suggest_add, **args) else: @@ -226,8 +234,7 @@ def update_compat_files(old_versions, new_versions, assert_unchanged=False, **ar 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: - contents = f.read() + contents = get_file(compat_path) header = HEADER + (EXTRA_HEADER % v) if not contents.startswith(HEADER): raise Exception("Invalid header in %s; does not match %s" % (compat_file, os.path.relpath(HEADER_PATH, ROOT_PATH))) @@ -323,13 +330,13 @@ def check_no_old_versions(old_versions, new_versions, contents, relpath): raise Exception('Unreplaced usage of %s remaining in %s' % (V, relpath)) def update_flags_mli(old_versions, new_versions, **args): - with open(FLAGS_MLI_PATH, 'r') as f: contents = f.read() + contents = get_file(FLAGS_MLI_PATH) new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH)) check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(FLAGS_MLI_PATH, ROOT_PATH)) update_if_changed(contents, new_contents, FLAGS_MLI_PATH, **args) def update_flags_ml(old_versions, new_versions, **args): - with open(FLAGS_ML_PATH, 'r') as f: contents = f.read() + contents = get_file(FLAGS_ML_PATH) new_contents = update_compat_versions_type_line(new_versions, contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH)) new_contents = update_version_compare(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH)) new_contents = update_pr_version(new_versions, new_contents, os.path.relpath(FLAGS_ML_PATH, ROOT_PATH)) @@ -337,13 +344,13 @@ def update_flags_ml(old_versions, new_versions, **args): update_if_changed(contents, new_contents, FLAGS_ML_PATH, **args) def update_coqargs_ml(old_versions, new_versions, **args): - with open(COQARGS_ML_PATH, 'r') as f: contents = f.read() + contents = get_file(COQARGS_ML_PATH) new_contents = update_add_compat_require(new_versions, contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH)) check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(COQARGS_ML_PATH, ROOT_PATH)) update_if_changed(contents, new_contents, COQARGS_ML_PATH, **args) def update_g_vernac(old_versions, new_versions, **args): - with open(G_VERNAC_PATH, 'r') as f: contents = f.read() + contents = get_file(G_VERNAC_PATH) new_contents = update_parse_compat_version(new_versions, contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH), **args) check_no_old_versions(old_versions, new_versions, new_contents, os.path.relpath(G_VERNAC_PATH, ROOT_PATH)) update_if_changed(contents, new_contents, G_VERNAC_PATH, **args) @@ -361,7 +368,7 @@ def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TES contents = None suggest_add = False if os.path.exists(path): - with open(path, 'r') as f: contents = f.read() + contents = get_file(path) else: suggest_add = True if '%s' in descr: descr = descr % v @@ -376,7 +383,7 @@ def update_test_suite(new_versions, assert_unchanged=False, test_suite_paths=TES remove_if_exists(path, assert_unchanged=assert_unchanged, **args) def update_doc_index(new_versions, **args): - with open(DOC_INDEX_PATH, 'r') as f: contents = f.read() + contents = get_file(DOC_INDEX_PATH) firstline = ' theories/Compat/AdmitAxiom.v' new_contents = ''.join(DOC_INDEX_LINES) if firstline not in new_contents: @@ -386,7 +393,7 @@ def update_doc_index(new_versions, **args): 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() + contents = get_file(TEST_SUITE_RUN_PATH) new_contents = r'''#!/usr/bin/env bash # allow running this script from any directory by basing things on where the script lives @@ -410,7 +417,7 @@ def update_compat_notations(old_versions, new_versions, **args): for root, dirs, files in os.walk(os.path.join(ROOT_PATH, 'theories')): for fname in files: if not fname.endswith('.v'): continue - with open(os.path.join(root, fname), 'r') as f: contents = f.read() + contents = get_file(os.path.join(root, fname)) new_contents = update_compat_notations_in(old_versions, new_versions, contents) update_if_changed(contents, new_contents, os.path.join(root, fname), **args) @@ -435,9 +442,8 @@ def parse_args(argv): 'git_add': False, } if '--master' not in argv and '--release' not in argv: - print(r'''WARNING: You should pass either --release (sometime before branching) + fatal_error(r'''ERROR: 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 diff --git a/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst b/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst new file mode 100644 index 0000000000..5c3936073a --- /dev/null +++ b/doc/changelog/03-notations/11090-master+refactoring-application-printing.rst @@ -0,0 +1 @@ +- Fixed #11033: regression in not printing coercions to which is also associated a notation (`#11090 <https://github.com/coq/coq/pull/11090>`_, by Hugo Herbelin). diff --git a/doc/plugin_tutorial/README.md b/doc/plugin_tutorial/README.md index 6d142a9af8..e0cedb0487 100644 --- a/doc/plugin_tutorial/README.md +++ b/doc/plugin_tutorial/README.md @@ -3,13 +3,21 @@ How to write plugins in Coq # Working environment In addition to installing OCaml and Coq, it can help to install several tools for development. - - ## Merlin + + ## Tuareg and Merlin These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html) ```shell opam install merlin # prints instructions for vim and emacs +opam install tuareg # syntax highlighting for OCaml +opam user-setup install # automatically configures editors for merlin +``` + + Adding this line to your .emacs helps Tuareg recognize the .mlg extension: + +```shell +(add-to-list 'auto-mode-alist '("\\.mlg$" . tuareg-mode) t) ``` ## This tutorial @@ -23,7 +31,7 @@ make # build # tuto0 : basics of project organization - package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject` + package an mlg file in a plugin, organize a `Makefile`, `_CoqProject` - Example of syntax to add a new toplevel command - Example of function call to print a simple message - Example of function call to print a simple warning diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 62d4aa704f..4f903d5776 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3281,11 +3281,13 @@ the conversion in hypotheses :n:`{+ @ident}`. defined transparent constant or local definition (see :ref:`gallina-definitions` and :ref:`vernac-controlling-the-reduction-strategies`). The tactic - :tacn:`unfold` applies the :math:`\delta` rule to each occurrence of - the constant to which :n:`@qualid` refers in the current goal and - then replaces it with its :math:`\beta`:math:`\iota`-normal form. + :tacn:`unfold` applies the :math:`\delta` rule to each occurrence + of the constant to which :n:`@qualid` refers in the current goal + and then replaces it with its :math:`\beta\iota\zeta`-normal form. + Use the general reduction tactics if you want to avoid this final + reduction, for instance :n:`cbv delta [@qualid]`. - .. exn:: @qualid does not denote an evaluable constant. + .. exn:: Cannot coerce @qualid to an evaluable reference. This error is frequent when trying to unfold something that has defined as an inductive type (or constructor) and not as a diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0c247e2660..c85f4f2cf7 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -721,15 +721,27 @@ let extern_possible_prim_token (custom,scopes) r = | None -> raise No_match | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) -let extern_possible extern r = - try Some (extern r) with No_match -> None - -let extern_optimal extern r r' = - let c = extern_possible extern r in - let c' = if r==r' then None else extern_possible extern r' in - match c,c' with - | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n - | _ -> raise No_match +let filter_fully_applied r l = + let nargs = match DAst.get r with + | GApp (f,args) -> List.length args + | _ -> assert false in + List.filter (fun (keyrule,pat,n as _rule) -> n = Some nargs) l + +let extern_optimal extern extern_fully_applied r r' = + if r==r' then + (* No coercion: we look for a notation for r or a partial application of it *) + extern r + else + (* A coercion is removed: we prefer in order: + - a notation w/o a delimiter for the expression w/o coercions (or a partial application of it), if any + - a notation for the fully-applied expression with coercions, if any + - a notation with a delimiter for the expression w/o coercions (or a partial applied of it), if any *) + try + let c' = extern r' in + match c' with + | { CAst.v = CDelimiters _} -> (try extern_fully_applied r with No_match -> c') + | _ -> c' + with No_match -> extern_fully_applied r (* Helper function for safe and optimal printing of primitive tokens *) (* such as those for Int63 *) @@ -798,13 +810,15 @@ let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_optimal (extern_possible_prim_token scopes) r r' + let extern_fun = extern_possible_prim_token scopes in + extern_optimal extern_fun extern_fun r r' with No_match -> try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; extern_optimal (fun r -> extern_notation scopes vars r (uninterp_notations r)) + (fun r -> extern_notation scopes vars r (filter_fully_applied r (uninterp_notations r))) r r'' with No_match -> let loc = r'.CAst.loc in diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v index 376410658a..f6b192c226 100644 --- a/plugins/ssr/ssrbool.v +++ b/plugins/ssr/ssrbool.v @@ -290,7 +290,7 @@ Require Import ssreflect ssrfun. r -- a right-hand operation, as orb_andr : rightt_distributive orb andb. T or t -- boolean truth, as in andbT: right_id true andb. U -- predicate union, as in predU. - W -- weakening, as in in1W : {in D, forall x, P} -> forall x, P. **) + W -- weakening, as in in1W : (forall x, P) -> {in D, forall x, P}. **) Set Implicit Arguments. diff --git a/test-suite/bugs/closed/bug_11161.v b/test-suite/bugs/closed/bug_11161.v new file mode 100644 index 0000000000..22a075e096 --- /dev/null +++ b/test-suite/bugs/closed/bug_11161.v @@ -0,0 +1,10 @@ +(* Ensure that evars are properly normalized in the instance path. + Problems with this can cause eg #11161. *) + +Class Foo (n:nat) := {x : bool}. + +Instance bar n : Foo n. Admitted. + +Instance bar' n : Foo n. split. abstract exact true. Qed. + +Instance bar'' n : Foo n. split. abstract exact true. Defined. diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 6704337f80..f889da4e98 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -1,7 +1,7 @@ Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Arguments Nat.sub _%nat_scope _%nat_scope : simpl nomatch +Arguments Nat.sub (_ _)%nat_scope : simpl nomatch The reduction tactics unfold Nat.sub but avoid exposing match constructs Nat.sub is transparent Expands to: Constant Coq.Init.Nat.sub @@ -25,7 +25,7 @@ Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Arguments Nat.sub !_%nat_scope !_%nat_scope / +Arguments Nat.sub (!_ !_)%nat_scope / The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor and when applied to 2 arguments Nat.sub is transparent @@ -33,7 +33,7 @@ Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Arguments Nat.sub !_%nat_scope !_%nat_scope +Arguments Nat.sub (!_ !_)%nat_scope The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor Nat.sub is transparent @@ -43,14 +43,14 @@ forall D1 C1 : Type, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 pf is not universe polymorphic -Arguments pf {D1%foo_scope} {C1%type_scope} _ [D2] [C2] : simpl never +Arguments pf {D1}%foo_scope {C1}%type_scope _ [D2 C2] : simpl never The reduction tactics never unfold pf pf is transparent Expands to: Constant Arguments.pf fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C fcomp is not universe polymorphic -Arguments fcomp {A%type_scope} {B%type_scope} {C%type_scope} _ _ _ / +Arguments fcomp {A B C}%type_scope _ _ _ / The reduction tactics unfold fcomp when applied to 6 arguments fcomp is transparent Expands to: Constant Arguments.fcomp @@ -78,7 +78,7 @@ Expands to: Constant Arguments.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Arguments f [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope +Arguments f [T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope The reduction tactics unfold f when the 4th, 5th and 6th arguments evaluate to a constructor f is transparent @@ -86,7 +86,7 @@ Expands to: Constant Arguments.S1.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Arguments f [T1%type_scope] [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope +Arguments f [T1 T2]%type_scope _ _ !_%nat_scope !_ !_%nat_scope The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 53d5624f6f..5093e785de 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -13,21 +13,21 @@ where ?y : [ |- nat] Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -Arguments eq {A%type_scope} -Arguments eq_refl {B%type_scope} {y}, [B] _ +Arguments eq {A}%type_scope +Arguments eq_refl {B}%type_scope {y}, [B] _ eq_refl : forall (A : Type) (x : A), x = x eq_refl is not universe polymorphic -Arguments eq_refl {B%type_scope} {y}, [B] _ +Arguments eq_refl {B}%type_scope {y}, [B] _ Expands to: Constructor Coq.Init.Logic.eq_refl Inductive myEq (B : Type) (x : A) : A -> Prop := myrefl : B -> myEq B x x Arguments myEq _%type_scope -Arguments myrefl {C%type_scope} x : rename +Arguments myrefl {C}%type_scope x : rename myrefl : forall (B : Type) (x : A), B -> myEq B x x myrefl is not universe polymorphic -Arguments myrefl {C%type_scope} x : rename +Arguments myrefl {C}%type_scope x : rename Expands to: Constructor Arguments_renaming.Test1.myrefl myplus = fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := @@ -37,11 +37,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename myplus : forall T : Type, T -> nat -> nat -> nat myplus is not universe polymorphic -Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent @@ -51,12 +51,12 @@ Expands to: Constant Arguments_renaming.Test1.myplus Inductive myEq (A B : Type) (x : A) : A -> Prop := myrefl : B -> myEq A B x x -Arguments myEq _%type_scope _%type_scope -Arguments myrefl A%type_scope {C%type_scope} x : rename +Arguments myEq (_ _)%type_scope +Arguments myrefl A%type_scope {C}%type_scope x : rename myrefl : forall (A B : Type) (x : A), B -> myEq A B x x myrefl is not universe polymorphic -Arguments myrefl A%type_scope {C%type_scope} x : rename +Arguments myrefl A%type_scope {C}%type_scope x : rename Expands to: Constructor Arguments_renaming.myrefl myrefl : forall (A C : Type) (x : A), C -> myEq A C x x @@ -68,11 +68,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename myplus : forall T : Type, T -> nat -> nat -> nat myplus is not universe polymorphic -Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename +Arguments myplus {Z}%type_scope !t (!n m)%nat_scope : rename The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out index 7489b8987e..e84ac85aa8 100644 --- a/test-suite/output/Cases.out +++ b/test-suite/output/Cases.out @@ -7,7 +7,7 @@ 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 -Arguments t_rect _%function_scope _%function_scope +Arguments t_rect (_ _)%function_scope = fun d : TT => match d with | {| f3 := b |} => b end @@ -26,7 +26,7 @@ match Nat.eq_dec x y with end : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y -Arguments proj _%nat_scope _%nat_scope _%function_scope +Arguments proj (_ _)%nat_scope _%function_scope foo = fix foo (A : Type) (l : list A) {struct l} : option A := match l with diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index d65d2a8f55..5f22eb5d7c 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,7 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I d2 = fun x : nat => d1 (y:=x) : forall x x0 : nat, x0 = x -> x0 = x -Arguments d2 [x%nat_scope] [x0%nat_scope] +Arguments d2 [x x0]%nat_scope map id (1 :: nil) : list nat map id' (1 :: nil) diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index ce058a6d34..da255e86cd 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,8 +1,8 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} -Arguments sig2 [A%type_scope] _%type_scope _%type_scope -Arguments exist2 [A%type_scope] _%function_scope _%function_scope +Arguments sig2 [A]%type_scope (_ _)%type_scope +Arguments exist2 [A]%type_scope (_ _)%function_scope exists x : nat, x = x : Prop fun b : bool => if b then b else b diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index ba4ac5a8f9..32120a9674 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -59,3 +59,5 @@ where |- Type] (pat, p0, p cannot be used) fun '{| |} => true : R -> bool +b = a + : Prop diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 4b9d0abd95..d3433949d1 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -140,3 +140,17 @@ Record R := { n : nat }. Check fun '{|n:=x|} => true. End EmptyRecordSyntax. + +Module L. + +(* Testing regression #11053 *) + +Section Test. +Variables (A B : Type) (a : A) (b : B). +Variable c : A -> B. +Coercion c : A >-> B. +Notation COERCION := (c). +Check b = a. +End Test. + +End L. diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 2952b6d94b..4f09f00c56 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -15,7 +15,7 @@ swap = fun (A B : Type) '(x, y) => (y, x) : forall A B : Type, A * B -> B * A -Arguments swap {A%type_scope} {B%type_scope} +Arguments swap {A B}%type_scope fun (A B : Type) '(x, y) => swap (x, y) = (y, x) : forall A B : Type, A * B -> Prop forall (A B : Type) '(x, y), swap (x, y) = (y, x) diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index 7d0d81a3e8..71d162c314 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,24 +1,24 @@ existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} existT is template universe polymorphic on sigT.u0 sigT.u1 -Arguments existT [A%type_scope] _%function_scope +Arguments existT [A]%type_scope _%function_scope Expands to: Constructor Coq.Init.Specif.existT Inductive sigT (A : Type) (P : A -> Type) : Type := existT : forall x : A, P x -> {x : A & P x} -Arguments sigT [A%type_scope] _%type_scope -Arguments existT [A%type_scope] _%function_scope +Arguments sigT [A]%type_scope _%type_scope +Arguments existT [A]%type_scope _%function_scope existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x} Argument A is implicit Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -Arguments eq {A%type_scope} -Arguments eq_refl {A%type_scope} {x}, [A] _ +Arguments eq {A}%type_scope +Arguments eq_refl {A}%type_scope {x}, [A] _ eq_refl : forall (A : Type) (x : A), x = x eq_refl is not universe polymorphic -Arguments eq_refl {A%type_scope} {x}, [A] _ +Arguments eq_refl {A}%type_scope {x}, [A] _ Expands to: Constructor Coq.Init.Logic.eq_refl eq_refl : forall (A : Type) (x : A), x = x @@ -34,11 +34,11 @@ fix add (n m : nat) {struct n} : nat := end : nat -> nat -> nat -Arguments Nat.add _%nat_scope _%nat_scope +Arguments Nat.add (_ _)%nat_scope Nat.add : nat -> nat -> nat Nat.add is not universe polymorphic -Arguments Nat.add _%nat_scope _%nat_scope +Arguments Nat.add (_ _)%nat_scope Nat.add is transparent Expands to: Constant Coq.Init.Nat.add Nat.add : nat -> nat -> nat @@ -52,9 +52,9 @@ Expands to: Constant Coq.Init.Peano.plus_n_O Inductive le (n : nat) : nat -> Prop := le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m -Arguments le _%nat_scope _%nat_scope +Arguments le (_ _)%nat_scope Arguments le_n _%nat_scope -Arguments le_S {n%nat_scope} [m%nat_scope] +Arguments le_S {n}%nat_scope [m]%nat_scope comparison : Set comparison is not universe polymorphic @@ -80,8 +80,8 @@ Notation sym_eq := eq_sym Expands to: Notation Coq.Init.Logic.sym_eq Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -Arguments eq {A%type_scope} -Arguments eq_refl {A%type_scope} {x}, {A} _ +Arguments eq {A}%type_scope +Arguments eq_refl {A}%type_scope {x}, {A} _ n:nat Hypothesis of the goal context. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 298a0789c4..525ca48bee 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -33,7 +33,7 @@ fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap : forall A : Type@{u}, Wrap@{u} A -> A (* u |= *) -Arguments wrap {A%type_scope} {Wrap} +Arguments wrap {A}%type_scope {Wrap} bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml index 737e0427ec..15077298aa 100644 --- a/vernac/comArguments.ml +++ b/vernac/comArguments.ml @@ -60,7 +60,7 @@ let warn_arguments_assert = (* [nargs_for_red] is the number of arguments required to trigger reduction, [args] is the main list of arguments statuses, [more_implicits] is a list of extra lists of implicit statuses *) -let vernac_arguments ~section_local reference args more_implicits nargs_for_red nargs_before_bidi flags = +let vernac_arguments ~section_local reference args more_implicits flags = let env = Global.env () in let sigma = Evd.from_env env in let assert_flag = List.mem `Assert flags in @@ -83,6 +83,23 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red if clear_implicits_flag && default_implicits_flag then err_incompat "clear implicits" "default implicits"; + let args, nargs_for_red, nargs_before_bidi, _i = + List.fold_left (fun (args,red,bidi,i) arg -> + match arg with + | RealArg arg -> (arg::args,red,bidi,i+1) + | VolatileArg -> + if Option.has_some red + then CErrors.user_err Pp.(str "The \"/\" modifier may only occur once."); + (args,Some i,bidi,i) + | BidiArg -> + if Option.has_some bidi + then CErrors.user_err Pp.(str "The \"&\" modifier may only occur once."); + (args,red,Some i,i)) + ([],None,None,0) + args + in + let args = List.rev args in + let sr = smart_global reference in let inf_names = let ty, _ = Typeops.type_of_global_in_context env sr in diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli index f78e01a11f..71effddf67 100644 --- a/vernac/comArguments.mli +++ b/vernac/comArguments.mli @@ -13,7 +13,5 @@ val vernac_arguments -> Libnames.qualid Constrexpr.or_by_notation -> Vernacexpr.vernac_argument_status list -> (Names.Name.t * Impargs.implicit_kind) list list - -> int option - -> int option -> Vernacexpr.arguments_modifier list -> unit diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 0515e88a15..5b97e06b2b 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -781,25 +781,8 @@ GRAMMAR EXTEND Gram ]; mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> { l } ] -> { let mods = match mods with None -> [] | Some l -> List.flatten l in - let slash_position = ref None in - let ampersand_position = ref None in - let rec parse_args i = function - | [] -> [] - | `Id x :: args -> x :: parse_args (i+1) args - | `Slash :: args -> - if Option.is_empty !slash_position then - (slash_position := Some i; parse_args i args) - else - user_err Pp.(str "The \"/\" modifier can occur only once") - | `Ampersand :: args -> - if Option.is_empty !ampersand_position then - (ampersand_position := Some i; parse_args i args) - else - user_err Pp.(str "The \"&\" modifier can occur only once") - in - let args = parse_args 0 (List.flatten args) in let more_implicits = Option.default [] more_implicits in - VernacArguments (qid, args, more_implicits, !slash_position, !ampersand_position, mods) } + VernacArguments (qid, List.flatten args, more_implicits, mods) } | IDENT "Implicit"; "Type"; bl = reserv_list -> { VernacReserve bl } @@ -843,17 +826,17 @@ GRAMMAR EXTEND Gram argument_spec_block: [ [ item = argument_spec -> { let name, recarg_like, notation_scope = item in - [`Id { name=name; recarg_like=recarg_like; + [RealArg { name=name; recarg_like=recarg_like; notation_scope=notation_scope; implicit_status = NotImplicit}] } - | "/" -> { [`Slash] } - | "&" -> { [`Ampersand] } + | "/" -> { [VolatileArg] } + | "&" -> { [BidiArg] } | "("; items = LIST1 argument_spec; ")"; sc = OPT scope_delimiter -> { let f x = match sc, x with | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; + RealArg { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; implicit_status = NotImplicit}) items } | "["; items = LIST1 argument_spec; "]"; sc = OPT scope_delimiter -> @@ -861,7 +844,7 @@ GRAMMAR EXTEND Gram | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; + RealArg { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; implicit_status = Implicit}) items } | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope_delimiter -> @@ -869,7 +852,7 @@ GRAMMAR EXTEND Gram | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> - `Id { name=name; recarg_like=recarg_like; + RealArg { name=name; recarg_like=recarg_like; notation_scope=f notation_scope; implicit_status = MaximallyImplicit}) items } ] diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 3dbf7afb78..080629ede2 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1068,39 +1068,52 @@ let string_of_definition_object_kind = let open Decls in function | Some Flags.Current -> [SetOnlyParsing] | Some v -> [SetCompatVersion v])) ) - | VernacArguments (q, args, more_implicits, nargs, nargs_before_bidi, mods) -> + | VernacArguments (q, args, more_implicits, mods) -> return ( hov 2 ( keyword "Arguments" ++ spc() ++ pr_smart_global q ++ let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in let pr_if b x = if b then x else str "" in - let pr_br imp x = match imp with - | Impargs.Implicit -> str "[" ++ x ++ str "]" - | Impargs.MaximallyImplicit -> str "{" ++ x ++ str "}" - | Impargs.NotImplicit -> x in - let rec print_arguments n nbidi l = - match n, nbidi, l with - | Some 0, _, l -> spc () ++ str"/" ++ print_arguments None nbidi l - | _, Some 0, l -> spc () ++ str"&" ++ print_arguments n None l - | None, None, [] -> mt() - | _, _, [] -> - let dummy = {name=Anonymous; recarg_like=false; - notation_scope=None; implicit_status=Impargs.NotImplicit} - in - print_arguments n nbidi [dummy] - | n, nbidi, { name = id; recarg_like = k; + let pr_one_arg (x,k) = pr_if k (str"!") ++ Name.print x in + let pr_br imp force x = + let left,right = + match imp with + | Impargs.Implicit -> str "[", str "]" + | Impargs.MaximallyImplicit -> str "{", str "}" + | Impargs.NotImplicit -> if force then str"(",str")" else mt(),mt() + in + left ++ x ++ right + in + let get_arguments_like s imp tl = + if s = None && imp = Impargs.NotImplicit then [], tl + else + let rec fold extra = function + | RealArg arg :: tl when + Option.equal (fun a b -> String.equal a.CAst.v b.CAst.v) arg.notation_scope s + && arg.implicit_status = imp -> + fold ((arg.name,arg.recarg_like) :: extra) tl + | args -> List.rev extra, args + in + fold [] tl + in + let rec print_arguments = function + | [] -> mt() + | VolatileArg :: l -> spc () ++ str"/" ++ print_arguments l + | BidiArg :: l -> spc () ++ str"&" ++ print_arguments l + | RealArg { name = id; recarg_like = k; notation_scope = s; implicit_status = imp } :: tl -> - spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++ - print_arguments (Option.map pred n) (Option.map pred nbidi) tl + let extra, tl = get_arguments_like s imp tl in + spc() ++ pr_br imp (extra<>[]) (prlist_with_sep spc pr_one_arg ((id,k)::extra)) ++ + pr_s s ++ print_arguments tl in let rec print_implicits = function | [] -> mt () | (name, impl) :: rest -> - spc() ++ pr_br impl (Name.print name) ++ print_implicits rest + spc() ++ pr_br impl false (Name.print name) ++ print_implicits rest in - print_arguments nargs nargs_before_bidi args ++ + print_arguments args ++ if not (List.is_empty more_implicits) then prlist (fun l -> str"," ++ print_implicits l) more_implicits else (mt ()) ++ diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index 5ebc89892c..ea49cae9db 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -259,6 +259,13 @@ let implicit_kind_of_status = function | None -> Anonymous, NotImplicit | Some (id,_,(maximal,_)) -> Name id, if maximal then MaximallyImplicit else Implicit +let dummy = { + Vernacexpr.implicit_status = NotImplicit; + name = Anonymous; + recarg_like = false; + notation_scope = None; +} + let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} = name = Anonymous && not recarg_like && notation_scope = None && implicit_status = NotImplicit @@ -287,6 +294,20 @@ let rec main_implicits i renames recargs scopes impls = then [] (* we may have a trail of dummies due to eg "clear scopes" *) else status :: rest +let rec insert_fake_args volatile bidi impls = + let open Vernacexpr in + match volatile, bidi with + | Some 0, _ -> VolatileArg :: insert_fake_args None bidi impls + | _, Some 0 -> BidiArg :: insert_fake_args volatile None impls + | None, None -> List.map (fun a -> RealArg a) impls + | _, _ -> + let hd, tl = match impls with + | impl :: impls -> impl, impls + | [] -> dummy, [] + in + let f = Option.map pred in + RealArg hd :: insert_fake_args (f volatile) (f bidi) tl + let print_arguments ref = let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in let flags, recargs, nargs_for_red = @@ -312,12 +333,13 @@ let print_arguments ref = let impls = main_implicits 0 renames recargs scopes impls in let moreimpls = List.map (fun (_,i) -> List.map implicit_kind_of_status i) moreimpls in let bidi = Pretyping.get_bidirectionality_hint ref in - if impls = [] && moreimpls = [] && nargs_for_red = None && bidi = None && flags = [] then [] + let impls = insert_fake_args nargs_for_red bidi impls in + if impls = [] && moreimpls = [] && flags = [] then [] else let open Constrexpr in let open Vernacexpr in [Ppvernac.pr_vernac_expr - (VernacArguments (CAst.make (AN qid), impls, moreimpls, nargs_for_red, bidi, flags))] + (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags))] let print_name_infos ref = let type_info_for_implicit = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f56cc00c3b..535aceed15 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2167,10 +2167,10 @@ let translate_vernac ~atts v = let open Vernacextend in match v with vernac_hints ~atts dbnames hints) | VernacSyntacticDefinition (id,c,b) -> VtDefault(fun () -> vernac_syntactic_definition ~atts id c b) - | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) -> + | VernacArguments (qid, args, more_implicits, flags) -> VtDefault(fun () -> with_section_locality ~atts - (ComArguments.vernac_arguments qid args more_implicits nargs bidi flags)) + (ComArguments.vernac_arguments qid args more_implicits flags)) | VernacReserve bl -> VtDefault(fun () -> unsupported_attributes atts; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 564c55670d..ce96d9265c 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -250,13 +250,17 @@ type vernac_cumulative = VernacCumulative | VernacNonCumulative (** {6 The type of vernacular expressions} *) -type vernac_argument_status = { +type vernac_one_argument_status = { name : Name.t; recarg_like : bool; notation_scope : string CAst.t option; implicit_status : Impargs.implicit_kind; } +type vernac_argument_status = + | VolatileArg | BidiArg + | RealArg of vernac_one_argument_status + type arguments_modifier = [ `Assert | `ClearBidiHint @@ -383,8 +387,6 @@ type nonrec vernac_expr = qualid or_by_notation * vernac_argument_status list (* Main arguments status list *) * (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) * - int option (* Number of args to trigger reduction *) * - int option (* Number of args before bidirectional typing *) * arguments_modifier list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option |