diff options
42 files changed, 764 insertions, 770 deletions
diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix index 8736c0f9b8..e7a0ba4f6c 100644 --- a/dev/nixpkgs.nix +++ b/dev/nixpkgs.nix @@ -1,4 +1,4 @@ import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/31c38894c90429c9554eab1b416e59e3b6e054df.tar.gz"; - sha256 = "1fv14rj5zslzm14ak4lvwqix94gm18h28376h4hsmrqqpnfqwsdw"; + url = "https://github.com/NixOS/nixpkgs/archive/4cd2cb43fb3a87f48c1e10bb65aee99d8f24cb9d.tar.gz"; + sha256 = "1d6rmq67kdg5gmk94wx2774qw89nvbhy6g1f2lms3c9ph37hways"; }) diff --git a/doc/changelog/02-specification-language/10985-about-arguments.rst b/doc/changelog/02-specification-language/10985-about-arguments.rst new file mode 100644 index 0000000000..1e05b0b0fe --- /dev/null +++ b/doc/changelog/02-specification-language/10985-about-arguments.rst @@ -0,0 +1,5 @@ +- The output of the :cmd:`Print` and :cmd:`About` commands has + changed. Arguments meta-data is now displayed as the corresponding + :cmd:`Arguments <Arguments (implicits)>` command instead of the + human-targeted prose used in previous Coq versions. (`#10985 + <https://github.com/coq/coq/pull/10985>`_, by Gaëtan Gilbert). diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index f477bf239d..f50cf9340c 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1927,9 +1927,11 @@ Renaming implicit arguments This command is used to redefine the names of implicit arguments. -With the assert flag, ``Arguments`` can be used to assert that a given -object has the expected number of arguments and that these arguments -are named as expected. +.. cmd:: Arguments @qualid {* @name} : assert + :name: Arguments (assert) + + This command is used to assert that a given object has the expected + number of arguments and that these arguments are named as expected. .. example:: (continued) diff --git a/plugins/micromega/DeclConstant.v b/plugins/micromega/DeclConstant.v index 0288728504..7ad5e313e3 100644 --- a/plugins/micromega/DeclConstant.v +++ b/plugins/micromega/DeclConstant.v @@ -51,7 +51,7 @@ Instance GT_APP2 {T1 T2 T3: Type} (F : T1 -> T2 -> T3) GT A1 -> GT A2 -> GT (F A1 A2). Defined. -Require Import ZArith. +Require Import QArith_base. Instance DO : DeclaredConstant O := {}. Instance DS : DeclaredConstant S := {}. @@ -64,6 +64,4 @@ Instance DZneg: DeclaredConstant Zneg := {}. Instance DZpow_pos : DeclaredConstant Z.pow_pos := {}. Instance DZpow : DeclaredConstant Z.pow := {}. -Require Import QArith. - Instance DQ : DeclaredConstant Qmake := {}. diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v index 3351c7ef8a..55a93eade7 100644 --- a/plugins/micromega/Lia.v +++ b/plugins/micromega/Lia.v @@ -15,7 +15,7 @@ (************************************************************************) Require Import ZMicromega. -Require Import ZArith. +Require Import ZArith_base. Require Import RingMicromega. Require Import VarMap. Require Import DeclConstant. diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v index 3651b54ed8..6c1852acbf 100644 --- a/plugins/micromega/RMicromega.v +++ b/plugins/micromega/RMicromega.v @@ -22,6 +22,7 @@ Require Import QArith. Require Import Qfield. Require Import Qreals. Require Import DeclConstant. +Require Import Lia. Require Setoid. (*Declare ML Module "micromega_plugin".*) @@ -192,7 +193,7 @@ Proof. destruct z ; try congruence. compute. congruence. compute. congruence. - generalize (Zle_0_nat n). auto with zarith. + generalize (Zle_0_nat n). auto using Z.le_ge. Qed. Definition CInvR0 (r : Rcst) := Qeq_bool (Q_of_Rcst r) (0 # 1). @@ -333,7 +334,7 @@ Proof. apply Qeq_bool_eq in C2. rewrite C2. simpl. - rewrite Qpower0 by auto with zarith. + rewrite Qpower0 by lia. apply Q2R_0. + rewrite Q2RpowerRZ. rewrite IHc. @@ -341,7 +342,7 @@ Proof. rewrite andb_false_iff in C. destruct C. simpl. apply Z.ltb_ge in H. - auto with zarith. + lia. left ; apply Qeq_bool_neq; auto. + simpl. rewrite <- IHc. diff --git a/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v index f93fe021f9..6db62e8401 100644 --- a/plugins/micromega/VarMap.v +++ b/plugins/micromega/VarMap.v @@ -15,7 +15,7 @@ (* *) (************************************************************************) -Require Import ZArith. +Require Import ZArith_base. Require Import Coq.Arith.Max. Require Import List. Set Implicit Arguments. diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v index 26970faf0c..08f3f39204 100644 --- a/plugins/micromega/ZCoeff.v +++ b/plugins/micromega/ZCoeff.v @@ -12,9 +12,10 @@ Require Import OrderedRing. Require Import RingMicromega. -Require Import ZArith. +Require Import ZArith_base. Require Import InitialRing. Require Import Setoid. +Require Import ZArithRing. Import OrderedRingSyntax. diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v index c160e11467..d709fdda14 100644 --- a/plugins/micromega/ZMicromega.v +++ b/plugins/micromega/ZMicromega.v @@ -21,7 +21,8 @@ Require Import RingMicromega. Require FSetPositive FSetEqProperties. Require Import ZCoeff. Require Import Refl. -Require Import ZArith. +Require Import ZArith_base. +Require Import ZArithRing. Require PreOmega. (*Declare ML Module "micromega_plugin".*) Local Open Scope Z_scope. diff --git a/printing/printing.mllib b/printing/printing.mllib index deb52ad270..5b5b6590a4 100644 --- a/printing/printing.mllib +++ b/printing/printing.mllib @@ -4,4 +4,3 @@ Ppconstr Proof_diffs Printer Printmod -Prettyp diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index 3c1e27ba9d..6704337f80 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -1,14 +1,14 @@ Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.sub _%nat_scope _%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 Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.sub _%nat_scope / _%nat_scope : simpl nomatch The reduction tactics unfold Nat.sub when applied to 1 argument but avoid exposing match constructs Nat.sub is transparent @@ -16,7 +16,7 @@ Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.sub !_%nat_scope / _%nat_scope : simpl nomatch The reduction tactics unfold Nat.sub when the 1st argument evaluates to a constructor and when applied to 1 argument but avoid exposing match constructs @@ -25,7 +25,7 @@ Expands to: Constant Coq.Init.Nat.sub Nat.sub : nat -> nat -> nat Nat.sub is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.sub !_%nat_scope !_%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 -Argument scopes are [nat_scope nat_scope] +Arguments Nat.sub !_%nat_scope !_%nat_scope The reduction tactics unfold Nat.sub when the 1st and 2nd arguments evaluate to a constructor Nat.sub is transparent @@ -43,37 +43,34 @@ forall D1 C1 : Type, (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2 pf is not universe polymorphic -Arguments D2, C2 are implicit -Arguments D1, C1 are implicit and maximally inserted -Argument scopes are [foo_scope type_scope _ _ _ _ _] +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 A, B, C are implicit and maximally inserted -Argument scopes are [type_scope type_scope type_scope _ _ _] +Arguments fcomp {A%type_scope} {B%type_scope} {C%type_scope} _ _ _ / The reduction tactics unfold fcomp when applied to 6 arguments fcomp is transparent Expands to: Constant Arguments.fcomp volatile : nat -> nat volatile is not universe polymorphic -Argument scope is [nat_scope] +Arguments volatile / _%nat_scope The reduction tactics always unfold volatile volatile is transparent Expands to: Constant Arguments.volatile f : T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Argument scopes are [_ _ nat_scope _ nat_scope] +Arguments f _ _ _%nat_scope _ _%nat_scope f is transparent Expands to: Constant Arguments.S1.S2.f f : T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Argument scopes are [_ _ nat_scope _ nat_scope] +Arguments f _ _ !_%nat_scope !_ !_%nat_scope The reduction tactics unfold f when the 3rd, 4th and 5th arguments evaluate to a constructor f is transparent @@ -81,8 +78,7 @@ Expands to: Constant Arguments.S1.S2.f f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic -Argument T2 is implicit -Argument scopes are [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 @@ -90,8 +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 T1, T2 are implicit -Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope] +Arguments f [T1%type_scope] [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 @@ -103,6 +98,7 @@ Expands to: Constant Arguments.f f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat f is not universe polymorphic +Arguments f _ _ _ _ !_ !_ !_ The reduction tactics unfold f when the 5th, 6th and 7th arguments evaluate to a constructor f is transparent @@ -118,7 +114,7 @@ Extra arguments: _, _. volatilematch : nat -> nat volatilematch is not universe polymorphic -Argument scope is [nat_scope] +Arguments volatilematch / _%nat_scope : simpl nomatch The reduction tactics always unfold volatilematch but avoid exposing match constructs volatilematch is transparent diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out index 69ba329ff1..7b25fd40f8 100644 --- a/test-suite/output/ArgumentsScope.out +++ b/test-suite/output/ArgumentsScope.out @@ -1,29 +1,29 @@ a : bool -> bool a is not universe polymorphic -Argument scope is [bool_scope] +Arguments a _%bool_scope Expands to: Variable a b : bool -> bool b is not universe polymorphic -Argument scope is [bool_scope] +Arguments b _%bool_scope Expands to: Variable b negb'' : bool -> bool negb'' is not universe polymorphic -Argument scope is [bool_scope] +Arguments negb'' _%bool_scope negb'' is transparent Expands to: Constant ArgumentsScope.A.B.negb'' negb' : bool -> bool negb' is not universe polymorphic -Argument scope is [bool_scope] +Arguments negb' _%bool_scope negb' is transparent Expands to: Constant ArgumentsScope.A.negb' negb : bool -> bool negb is not universe polymorphic -Argument scope is [bool_scope] +Arguments negb _%bool_scope negb is transparent Expands to: Constant Coq.Init.Datatypes.negb a : bool -> bool diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 65c902202d..53d5624f6f 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -13,36 +13,21 @@ where ?y : [ |- nat] Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x -For eq_refl: Arguments are renamed to B, y -For eq: Argument A is implicit and maximally inserted -For eq_refl, when applied to no arguments: - Arguments B, y are implicit and maximally inserted -For eq_refl, when applied to 1 argument: - Argument B is implicit -For eq: Argument scopes are [type_scope _ _] -For eq_refl: Argument scopes are [type_scope _] +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 are renamed to B, y -When applied to no arguments: - Arguments B, y are implicit and maximally inserted -When applied to 1 argument: - Argument B is implicit -Argument scopes are [type_scope _] +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 -For myrefl: Arguments are renamed to C, x, _ -For myrefl: Argument C is implicit and maximally inserted -For myEq: Argument scopes are [type_scope _ _] -For myrefl: Argument scopes are [type_scope _ _] +Arguments myEq _%type_scope +Arguments myrefl {C%type_scope} x : rename myrefl : forall (B : Type) (x : A), B -> myEq B x x myrefl is not universe polymorphic -Arguments are renamed to C, x, _ -Argument C is implicit and maximally inserted -Argument scopes are [type_scope _ _] +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 := @@ -52,15 +37,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments are renamed to Z, t, n, m -Argument Z is implicit and maximally inserted -Argument scopes are [type_scope _ nat_scope nat_scope] +Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename myplus : 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] +Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename The reduction tactics unfold myplus when the 2nd and 3rd arguments evaluate to a constructor myplus is transparent @@ -70,16 +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 -For myrefl: Arguments are renamed to A, C, x, _ -For myrefl: Argument C is implicit and maximally inserted -For myEq: Argument scopes are [type_scope type_scope _ _] -For myrefl: Argument scopes are [type_scope type_scope _ _] +Arguments myEq _%type_scope _%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 are renamed to A, C, x, _ -Argument C is implicit and maximally inserted -Argument scopes are [type_scope type_scope _ _] +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 @@ -91,15 +68,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat := end : forall T : Type, T -> nat -> nat -> nat -Arguments are renamed to Z, t, n, m -Argument Z is implicit and maximally inserted -Argument scopes are [type_scope _ nat_scope nat_scope] +Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename myplus : 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] +Arguments myplus {Z%type_scope} !t !n%nat_scope 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 cb835ab48d..7489b8987e 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 -Argument scopes are [function_scope function_scope _] +Arguments t_rect _%function_scope _%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 -Argument scopes are [nat_scope nat_scope function_scope _ _] +Arguments proj _%nat_scope _%nat_scope _%function_scope foo = fix foo (A : Type) (l : list A) {struct l} : option A := match l with @@ -36,14 +36,14 @@ fix foo (A : Type) (l : list A) {struct l} : option A := end : forall A : Type, list A -> option A -Argument scopes are [type_scope list_scope] +Arguments foo _%type_scope _%list_scope uncast = fun (A : Type) (x : I A) => match x with | x0 <: _ => x0 end : forall A : Type, I A -> A -Argument scopes are [type_scope _] +Arguments uncast _%type_scope foo' = if A 0 then true else false : bool f = @@ -82,7 +82,7 @@ lem2 = fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl : forall k : bool, k = k -Argument scope is [bool_scope] +Arguments lem2 _%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 diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out index 3b65003c29..d65d2a8f55 100644 --- a/test-suite/output/Implicit.out +++ b/test-suite/output/Implicit.out @@ -5,8 +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 x, x0 are implicit -Argument scopes are [nat_scope nat_scope _] +Arguments d2 [x%nat_scope] [x0%nat_scope] map id (1 :: nil) : list nat map id' (1 :: nil) diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out index af202ea01c..8ff571ae55 100644 --- a/test-suite/output/Inductive.out +++ b/test-suite/output/Inductive.out @@ -3,5 +3,5 @@ Last occurrence of "list'" must have "A" as 1st argument in "A -> list' A -> list' (A * A)%type". Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x -For foo: Argument scopes are [type_scope _] -For Foo: Argument scopes are [type_scope _] +Arguments foo _%type_scope +Arguments Foo _%type_scope diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index c17c63e724..ce058a6d34 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,11 +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} -For sig2: Argument A is implicit -For exist2: Argument A is implicit -For sig2: Argument scopes are [type_scope type_scope type_scope] -For exist2: Argument scopes are [type_scope function_scope function_scope _ _ - _] +Arguments sig2 [A%type_scope] _%type_scope _%type_scope +Arguments exist2 [A%type_scope] _%function_scope _%function_scope exists x : nat, x = x : Prop fun b : bool => if b then b else b diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index d32cf67e28..abada44da7 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -230,7 +230,7 @@ fun l : list nat => match l with end : list nat -> list nat -Argument scope is [list_scope] +Arguments foo _%list_scope Notation "'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope (default interpretation) diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out index 8a6d94c732..2952b6d94b 100644 --- a/test-suite/output/PatternsInBinders.out +++ b/test-suite/output/PatternsInBinders.out @@ -15,8 +15,7 @@ swap = fun (A B : Type) '(x, y) => (y, x) : forall A B : Type, A * B -> B * A -Arguments A, B are implicit and maximally inserted -Argument scopes are [type_scope type_scope _] +Arguments swap {A%type_scope} {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) @@ -42,6 +41,6 @@ fun (pat : nat) '(x, y) => x + y = pat f = fun x : nat => x + x : nat -> nat -Argument scope is [nat_scope] +Arguments f _%nat_scope fun x : nat => x + x : nat -> nat diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out index e788977fb7..7d0d81a3e8 100644 --- a/test-suite/output/PrintInfos.out +++ b/test-suite/output/PrintInfos.out @@ -1,36 +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 -Argument A is implicit -Argument scopes are [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} -For sigT: Argument A is implicit -For existT: Argument A is implicit -For sigT: Argument scopes are [type_scope type_scope] -For existT: Argument scopes are [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 -For eq: Argument A is implicit and maximally inserted -For eq_refl, when applied to no arguments: - Arguments A, x are implicit and maximally inserted -For eq_refl, when applied to 1 argument: - Argument A is implicit -For eq: Argument scopes are [type_scope _ _] -For eq_refl: Argument scopes are [type_scope _] +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 -When applied to no arguments: - Arguments A, x are implicit and maximally inserted -When applied to 1 argument: - Argument A is implicit -Argument scopes are [type_scope _] +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 @@ -46,11 +34,11 @@ fix add (n m : nat) {struct n} : nat := end : nat -> nat -> nat -Argument scopes are [nat_scope nat_scope] +Arguments Nat.add _%nat_scope _%nat_scope Nat.add : nat -> nat -> nat Nat.add is not universe polymorphic -Argument scopes are [nat_scope nat_scope] +Arguments Nat.add _%nat_scope _%nat_scope Nat.add is transparent Expands to: Constant Coq.Init.Nat.add Nat.add : nat -> nat -> nat @@ -58,17 +46,15 @@ Nat.add : nat -> nat -> nat plus_n_O : forall n : nat, n = n + 0 plus_n_O is not universe polymorphic -Argument scope is [nat_scope] +Arguments plus_n_O _%nat_scope plus_n_O is opaque 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 -For le_S: Argument m is implicit -For le_S: Argument n is implicit and maximally inserted -For le: Argument scopes are [nat_scope nat_scope] -For le_n: Argument scope is [nat_scope] -For le_S: Argument scopes are [nat_scope nat_scope _] +Arguments le _%nat_scope _%nat_scope +Arguments le_n _%nat_scope +Arguments le_S {n%nat_scope} [m%nat_scope] comparison : Set comparison is not universe polymorphic @@ -81,26 +67,21 @@ bar is not universe polymorphic Expanded type for implicit arguments bar : forall x : nat, x = 0 -Argument x is implicit and maximally inserted +Arguments bar {x} Expands to: Constant PrintInfos.bar *** [ bar : foo ] Expanded type for implicit arguments bar : forall x : nat, x = 0 -Argument x is implicit and maximally inserted +Arguments bar {x} Module Coq.Init.Peano 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 -For eq: Argument A is implicit and maximally inserted -For eq_refl, when applied to no arguments: - Arguments A, x are implicit and maximally inserted -For eq_refl, when applied to 1 argument: - Argument A is implicit and maximally inserted -For eq: Argument scopes are [type_scope _ _] -For eq_refl: Argument scopes are [type_scope _] +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/StringSyntax.out b/test-suite/output/StringSyntax.out index 9366113c0c..e9cf4282dc 100644 --- a/test-suite/output/StringSyntax.out +++ b/test-suite/output/StringSyntax.out @@ -433,7 +433,7 @@ 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 -Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +Arguments byte_rect _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope byte_rec = fun P : byte -> Set => byte_rect P : forall P : byte -> Set, @@ -607,7 +607,7 @@ 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 -Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +Arguments byte_rec _%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 "?") (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") @@ -1043,7 +1043,7 @@ 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 -Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope] +Arguments byte_ind _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope "000" : byte "a" diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index d48d8b900f..298a0789c4 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -4,37 +4,36 @@ Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A } (* u |= *) PWrap has primitive projections with eta conversion. -For PWrap: Argument scope is [type_scope] -For pwrap: Argument scopes are [type_scope _] +Arguments PWrap _%type_scope +Arguments pwrap _%type_scope punwrap@{u} = fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p : forall A : Type@{u}, PWrap@{u} A -> A (* u |= *) -Argument scopes are [type_scope _] +Arguments punwrap _%type_scope Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A } (* u |= *) -For RWrap: Argument scope is [type_scope] -For rwrap: Argument scopes are [type_scope _] +Arguments RWrap _%type_scope +Arguments rwrap _%type_scope runwrap@{u} = fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap : forall A : Type@{u}, RWrap@{u} A -> A (* u |= *) -Argument scopes are [type_scope _] +Arguments runwrap _%type_scope Wrap@{u} = fun A : Type@{u} => A : Type@{u} -> Type@{u} (* u |= *) -Argument scope is [type_scope] +Arguments Wrap _%type_scope wrap@{u} = fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap : forall A : Type@{u}, Wrap@{u} A -> A (* u |= *) -Arguments A, Wrap are implicit and maximally inserted -Argument scopes are [type_scope _] +Arguments wrap {A%type_scope} {Wrap} bar@{u} = nat : Wrap@{u} Set (* u |= Set < u *) @@ -87,13 +86,13 @@ Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A } (* E |= *) PWrap has primitive projections with eta conversion. -For PWrap: Argument scope is [type_scope] -For pwrap: Argument scopes are [type_scope _] +Arguments PWrap _%type_scope +Arguments pwrap _%type_scope punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A (* K |= *) punwrap is universe polymorphic -Argument scopes are [type_scope _] +Arguments punwrap _%type_scope punwrap is transparent Expands to: Constant UnivBinders.punwrap The command has indeed failed with message: @@ -118,7 +117,7 @@ Inductive insecind@{k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{k} (* k |= *) -For inseccstr: Argument scope is [type_scope] +Arguments inseccstr _%type_scope insec@{u v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) @@ -126,7 +125,7 @@ Inductive insecind@{u k} : Type@{k+1} := inseccstr : Type@{k} -> insecind@{u k} (* u k |= *) -For inseccstr: Argument scope is [type_scope] +Arguments inseccstr _%type_scope insec2@{u} = Prop : Type@{Set+1} (* u |= *) @@ -148,24 +147,24 @@ Type@{UnivBinders.59} -> Type@{i} (* i UnivBinders.59 UnivBinders.60 |= *) axfoo is universe polymorphic -Argument scope is [type_scope] +Arguments axfoo _%type_scope Expands to: Constant UnivBinders.axfoo axbar@{i UnivBinders.59 UnivBinders.60} : Type@{UnivBinders.60} -> Type@{i} (* i UnivBinders.59 UnivBinders.60 |= *) axbar is universe polymorphic -Argument scope is [type_scope] +Arguments axbar _%type_scope Expands to: Constant UnivBinders.axbar axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i} axfoo' is not universe polymorphic -Argument scope is [type_scope] +Arguments axfoo' _%type_scope Expands to: Constant UnivBinders.axfoo' axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i} axbar' is not universe polymorphic -Argument scope is [type_scope] +Arguments axbar' _%type_scope Expands to: Constant UnivBinders.axbar' The command has indeed failed with message: When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block). diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 72c496d56d..febf4fa1be 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -15,6 +15,7 @@ Require Export DoubleType. Require Import Lia. Require Import Zpow_facts. Require Import Zgcd_alt. +Require ZArith. Import Znumtheory. Register bool as kernel.ind_bool. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 54d35cded2..4239943d03 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Export ZArith. +Require Export ZArith_base. Require Export ZArithRing. Require Export Morphisms Setoid Bool. diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index 8d68038582..35f113e226 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -9,6 +9,7 @@ (************************************************************************) Require Import QArith. +Import Zdiv. Lemma Qopp_lt_compat: forall p q : Q, p < q -> - q < - p. Proof. @@ -38,7 +39,7 @@ Proof. intros z. unfold Qceiling. simpl. -rewrite Zdiv_1_r. +rewrite Z.div_1_r. apply Z.opp_involutive. Qed. @@ -50,8 +51,7 @@ unfold Qle. simpl. replace (n*1)%Z with n by ring. rewrite Z.mul_comm. -apply Z_mult_div_ge. -auto with *. +now apply Z.mul_div_le. Qed. Hint Resolve Qfloor_le : qarith. diff --git a/theories/Structures/OrderedTypeEx.v b/theories/Structures/OrderedTypeEx.v index cc216b21f8..e889150d92 100644 --- a/theories/Structures/OrderedTypeEx.v +++ b/theories/Structures/OrderedTypeEx.v @@ -9,7 +9,7 @@ (************************************************************************) Require Import OrderedType. -Require Import ZArith. +Require Import ZArith_base. Require Import PeanoNat. Require Import Ascii String. Require Import NArith Ndec. diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v index 056e67db83..4896301aa7 100644 --- a/theories/ZArith/Zdigits.v +++ b/theories/ZArith/Zdigits.v @@ -15,11 +15,11 @@ Require Import Bvector. Require Import ZArith. Require Export Zpower. -Require Import Omega. +Require Import Lia. (** The evaluation of boolean vector is done both in binary and two's complement. The computed number belongs to Z. - We hence use Omega to perform computations in Z. + We hence use lia to perform computations in Z. Moreover, we use functions [2^n] where [n] is a natural number (here the vector length). *) @@ -155,10 +155,10 @@ Section Z_BRIC_A_BRAC. forall (n:nat) (bv:Bvector n), (binary_value n bv >= 0)%Z. Proof. induction bv as [| a n v IHbv]; cbn. - omega. + lia. - destruct a; destruct (binary_value n v); simpl; auto. - auto with zarith. + destruct a; destruct (binary_value n v); auto. + discriminate. Qed. Lemma two_compl_value_Sn : @@ -203,7 +203,7 @@ Section Z_BRIC_A_BRAC. auto. destruct p; auto. - simpl; intros; omega. + simpl; intros; lia. intro H; elim H; trivial. Qed. @@ -214,11 +214,11 @@ Section Z_BRIC_A_BRAC. (z < two_power_nat (S n))%Z -> (Z.div2 z < two_power_nat n)%Z. Proof. intros. - enough (2 * Z.div2 z < 2 * two_power_nat n)%Z by omega. + enough (2 * Z.div2 z < 2 * two_power_nat n)%Z by lia. rewrite <- two_power_nat_S. destruct (Zeven.Zeven_odd_dec z) as [Heven|Hodd]; intros. rewrite <- Zeven.Zeven_div2; auto. - generalize (Zeven.Zodd_div2 z Hodd); omega. + generalize (Zeven.Zodd_div2 z Hodd); lia. Qed. Lemma Z_to_two_compl_Sn_z : @@ -253,9 +253,9 @@ Section Z_BRIC_A_BRAC. intros n z; rewrite (two_power_nat_S n). generalize (Zmod2_twice z). destruct (Zeven.Zeven_odd_dec z) as [H| H]. - rewrite (Zeven_bit_value z H); intros; omega. + rewrite (Zeven_bit_value z H); intros; lia. - rewrite (Zodd_bit_value z H); intros; omega. + rewrite (Zodd_bit_value z H); intros; lia. Qed. Lemma Zlt_two_power_nat_S : @@ -265,9 +265,9 @@ Section Z_BRIC_A_BRAC. intros n z; rewrite (two_power_nat_S n). generalize (Zmod2_twice z). destruct (Zeven.Zeven_odd_dec z) as [H| H]. - rewrite (Zeven_bit_value z H); intros; omega. + rewrite (Zeven_bit_value z H); intros; lia. - rewrite (Zodd_bit_value z H); intros; omega. + rewrite (Zodd_bit_value z H); intros; lia. Qed. End Z_BRIC_A_BRAC. @@ -309,7 +309,7 @@ Section COHERENT_VALUE. (z < two_power_nat n)%Z -> binary_value n (Z_to_binary n z) = z. Proof. induction n as [| n IHn]. - unfold two_power_nat, shift_nat; simpl; intros; omega. + unfold two_power_nat, shift_nat; simpl; intros; lia. intros; rewrite Z_to_binary_Sn_z. rewrite binary_value_Sn. @@ -328,13 +328,13 @@ Section COHERENT_VALUE. Proof. induction n as [| n IHn]. unfold two_power_nat, shift_nat; simpl; intros. - assert (z = (-1)%Z \/ z = 0%Z). omega. + assert (z = (-1)%Z \/ z = 0%Z). lia. intuition; subst z; trivial. intros; rewrite Z_to_two_compl_Sn_z. rewrite two_compl_value_Sn. rewrite IHn. - generalize (Zmod2_twice z); omega. + generalize (Zmod2_twice z); lia. apply Zge_minus_two_power_nat_S; auto. diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v index 0cc137ef5d..da2df40572 100644 --- a/theories/ZArith/Zgcd_alt.v +++ b/theories/ZArith/Zgcd_alt.v @@ -25,7 +25,7 @@ Require Import ZArith_base. Require Import ZArithRing. Require Import Zdiv. Require Import Znumtheory. -Require Import Omega. +Require Import Lia. Open Scope Z_scope. @@ -76,8 +76,7 @@ Open Scope Z_scope. Z.abs a < Z.of_nat n -> Zis_gcd a b (Zgcdn n a b). Proof. induction n. - simpl; intros. - exfalso; generalize (Z.abs_nonneg a); omega. + intros; lia. destruct a; intros; simpl; [ generalize (Zis_gcd_0_abs b); intuition | | ]; unfold Z.modulo; @@ -85,8 +84,7 @@ Open Scope Z_scope. destruct (Z.div_eucl b (Zpos p)) as (q,r); intros (H0,H1); rewrite Nat2Z.inj_succ in H; simpl Z.abs in H; - (assert (H2: Z.abs r < Z.of_nat n) by - (rewrite Z.abs_eq; auto with zarith)); + (assert (H2: Z.abs r < Z.of_nat n) by lia); assert (IH:=IHn r (Zpos p) H2); clear IHn; simpl in IH |- *; rewrite H0. @@ -108,15 +106,11 @@ Open Scope Z_scope. Lemma fibonacci_pos : forall n, 0 <= fibonacci n. Proof. enough (forall N n, (n<N)%nat -> 0<=fibonacci n) by eauto. - induction N. - inversion 1. + induction N. intros; lia. + intros [ | [ | n ] ]. 1-2: simpl; lia. intros. - destruct n. - simpl; auto with zarith. - destruct n. - simpl; auto with zarith. change (0 <= fibonacci (S n) + fibonacci n). - generalize (IHN n) (IHN (S n)); omega. + generalize (IHN n) (IHN (S n)); lia. Qed. Lemma fibonacci_incr : @@ -129,7 +123,7 @@ Open Scope Z_scope. destruct m. simpl; auto with zarith. change (fibonacci (S m) <= fibonacci (S m)+fibonacci m). - generalize (fibonacci_pos m); omega. + generalize (fibonacci_pos m); lia. Qed. (** 3) We prove that fibonacci numbers are indeed worst-case: @@ -144,8 +138,8 @@ Open Scope Z_scope. fibonacci (S (S n)) <= b. Proof. induction n. - intros [|a|a]; intros; simpl; omega. - intros [|a|a] b (Ha,Ha'); [simpl; omega | | easy ]. + intros [|a|a]; intros; simpl; lia. + intros [|a|a] b (Ha,Ha'); [simpl; lia | | easy ]. remember (S n) as m. rewrite Heqm at 2. simpl Zgcdn. unfold Z.modulo; generalize (Z_div_mod b (Zpos a) eq_refl). @@ -161,20 +155,13 @@ Open Scope Z_scope. apply Zis_gcd_sym. apply Zis_gcd_for_euclid2; auto. apply Zis_gcd_sym; auto. - + split; auto. - rewrite EQ. - apply Z.add_le_mono; auto. - apply Z.le_trans with (Zpos a * 1); auto. - now rewrite Z.mul_1_r. - apply Z.mul_le_mono_nonneg_l; auto with zarith. - change 1 with (Z.succ 0). apply Z.le_succ_l. - destruct q; auto with zarith. - assert (Zpos a * Zneg p < 0) by now compute. omega. + + split. auto. + destruct q. lia. 1-2: nia. - (* r = 0 *) clear IHn EQ Hr'; intros _. subst r; simpl; rewrite Heqm. destruct n. - + simpl. omega. + + simpl. lia. + now destruct 1. Qed. @@ -184,7 +171,7 @@ Open Scope Z_scope. 0 < a < b -> a < fibonacci (S n) -> Zis_gcd a b (Zgcdn n a b). Proof. - destruct a; [ destruct 1; exfalso; omega | | destruct 1; discriminate]. + destruct a. 1,3 : intros; lia. cut (forall k n b, k = (S (Pos.to_nat p) - n)%nat -> 0 < Zpos p < b -> Zpos p < fibonacci (S n) -> @@ -192,22 +179,17 @@ Open Scope Z_scope. destruct 2; eauto. clear n; induction k. intros. - assert (Pos.to_nat p < n)%nat by omega. apply Zgcdn_linear_bound. - simpl. - generalize (inj_le _ _ H2). - rewrite Nat2Z.inj_succ. - rewrite positive_nat_Z; auto. - omega. + lia. intros. generalize (Zgcdn_worst_is_fibonacci n (Zpos p) b H0); intros. assert (Zis_gcd (Zpos p) b (Zgcdn (S n) (Zpos p) b)). apply IHk; auto. - omega. + lia. replace (fibonacci (S (S n))) with (fibonacci (S n)+fibonacci n) by auto. - generalize (fibonacci_pos n); omega. + generalize (fibonacci_pos n); lia. replace (Zgcdn n (Zpos p) b) with (Zgcdn (S n) (Zpos p) b); auto. - generalize (H2 H3); clear H2 H3; omega. + generalize (H2 H3); clear H2 H3; lia. Qed. (** 4) The proposed bound leads to a fibonacci number that is big enough. *) @@ -215,7 +197,7 @@ Open Scope Z_scope. Lemma Zgcd_bound_fibonacci : forall a, 0 < a -> a < fibonacci (Zgcd_bound a). Proof. - destruct a; [omega| | intro H; discriminate]. + destruct a; [lia| | intro H; discriminate]. intros _. induction p; [ | | compute; auto ]; simpl Zgcd_bound in *; @@ -224,10 +206,10 @@ Open Scope Z_scope. assert (n <> O) by (unfold n; destruct p; simpl; auto). destruct n as [ |m]; [elim H; auto| ]. - generalize (fibonacci_pos m); rewrite Pos2Z.inj_xI; omega. + generalize (fibonacci_pos m); rewrite Pos2Z.inj_xI; lia. destruct n as [ |m]; [elim H; auto| ]. - generalize (fibonacci_pos m); rewrite Pos2Z.inj_xO; omega. + generalize (fibonacci_pos m); rewrite Pos2Z.inj_xO; lia. Qed. (* 5) the end: we glue everything together and take care of @@ -265,10 +247,10 @@ Open Scope Z_scope. Z.le_elim H1. + apply Zgcdn_ok_before_fibonacci; auto. apply Z.lt_le_trans with (fibonacci (S m)); - [ omega | apply fibonacci_incr; auto]. + [ lia | apply fibonacci_incr; auto]. + subst r; simpl. - destruct m as [ |m]; [exfalso; omega| ]. - destruct n as [ |n]; [exfalso; omega| ]. + destruct m as [ |m]; [ lia | ]. + destruct n as [ |n]; [ lia | ]. simpl; apply Zis_gcd_sym; apply Zis_gcd_0. Qed. @@ -277,7 +259,7 @@ Open Scope Z_scope. Proof. destruct a. - simpl; intros. - destruct n; [exfalso; omega | ]. + destruct n; [ lia | ]. simpl; generalize (Zis_gcd_0_abs b); intuition. - apply Zgcdn_is_gcd_pos. - rewrite <- Zgcd_bound_opp, <- Zgcdn_opp. diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index e65eb7cdc7..a669429ffa 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import ZArith_base ZArithRing Omega Zcomplements Zdiv Znumtheory. +Require Import ZArith_base ZArithRing Lia Zcomplements Zdiv Znumtheory. Require Export Zpower. Local Open Scope Z_scope. @@ -49,7 +49,7 @@ Proof. intros. now apply Z.pow_le_mono_r. Qed. Theorem Zpower_lt_monotone a b c : 1 < a -> 0 <= b < c -> a^b < a^c. -Proof. intros. apply Z.pow_lt_mono_r; auto with zarith. Qed. +Proof. intros. apply Z.pow_lt_mono_r; lia. Qed. Theorem Zpower_gt_1 x y : 1 < x -> 0 < y -> 1 < x^y. Proof. apply Z.pow_gt_1. Qed. @@ -87,10 +87,10 @@ Proof. assert (Hn := Nat2Z.is_nonneg n). destruct p; simpl Pos.size_nat. - specialize IHn with p. - rewrite Pos2Z.inj_xI, Nat2Z.inj_succ, Z.pow_succ_r; omega. + rewrite Nat2Z.inj_succ, Z.pow_succ_r; lia. - specialize IHn with p. - rewrite Pos2Z.inj_xO, Nat2Z.inj_succ, Z.pow_succ_r; omega. - - split; auto with zarith. + rewrite Nat2Z.inj_succ, Z.pow_succ_r; lia. + - split. lia. intros _. apply Z.pow_gt_1. easy. now rewrite Nat2Z.inj_succ, Z.lt_succ_r. Qed. @@ -103,8 +103,8 @@ Proof. intros Hn; destruct (Z.le_gt_cases 0 q) as [H1|H1]. - pattern q; apply natlike_ind; trivial. clear q H1. intros q Hq Rec. rewrite !Z.pow_succ_r; trivial. - rewrite Z.mul_mod_idemp_l; auto with zarith. - rewrite Z.mul_mod, Rec, <- Z.mul_mod; auto with zarith. + rewrite Z.mul_mod_idemp_l by lia. + rewrite Z.mul_mod, Rec, <- Z.mul_mod by lia. reflexivity. - rewrite !Z.pow_neg_r; auto with zarith. Qed. @@ -163,7 +163,7 @@ Qed. Lemma Zpower_divide p q : 0 < q -> (p | p ^ q). Proof. exists (p^(q - 1)). - rewrite Z.mul_comm, <- Z.pow_succ_r; f_equal; auto with zarith. + rewrite Z.mul_comm, <- Z.pow_succ_r by lia; f_equal; lia. Qed. Theorem rel_prime_Zpower_r i p q : @@ -190,7 +190,7 @@ Proof. - simpl; intros. assert (2<=p) by (apply prime_ge_2; auto). assert (p<=1) by (apply Z.divide_pos_le; auto with zarith). - omega. + lia. - intros n Hn Rec. rewrite Z.pow_succ_r by trivial. intros. assert (2<=p) by (apply prime_ge_2; auto). @@ -213,11 +213,11 @@ Proof. exists 1; rewrite Z.pow_1_r; apply prime_power_prime with n; auto. case not_prime_divide with (2 := Hpr); auto. intros p1 ((Hp1, Hpq1),(q1,->)). - assert (Hq1 : 0 < q1) by (apply Z.mul_lt_mono_pos_r with p1; auto with zarith). - destruct (IH p1) with p n as (r1,Hr1); auto with zarith. + assert (Hq1 : 0 < q1) by (apply Z.mul_lt_mono_pos_r with p1; lia). + destruct (IH p1) with p n as (r1,Hr1). 3-4: assumption. 1-2: lia. transitivity (q1 * p1); trivial. exists q1; auto with zarith. - destruct (IH q1) with p n as (r2,Hr2); auto with zarith. - split; auto with zarith. + destruct (IH q1) with p n as (r2,Hr2). 3-4: assumption. 2: lia. + split. lia. rewrite <- (Z.mul_1_r q1) at 1. apply Z.mul_lt_mono_pos_l; auto with zarith. transitivity (q1 * p1); trivial. exists p1; auto with zarith. diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index fea7db7921..b3e7fff7d6 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -63,6 +63,7 @@ Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Z.quot_1_r Z.rem_1_r Ltac zero_or_not a := destruct (Z.eq_decidable a 0) as [->|?]; [rewrite ?Zquot_0_l, ?Zrem_0_l, ?Zquot_0_r, ?Zrem_0_r; + try lia; auto with zarith|]. Lemma Z_rem_same a : Z.rem a a = 0. @@ -100,7 +101,6 @@ Proof. zero_or_not b. now apply Z.rem_opp_opp. Qed. Theorem Zrem_sgn a b : 0 <= Z.sgn (Z.rem a b) * Z.sgn a. Proof. zero_or_not b. - - apply Z.square_nonneg. - zero_or_not (Z.rem a b). rewrite Z.rem_sign_nz; trivial. apply Z.square_nonneg. Qed. @@ -203,18 +203,18 @@ Qed. (* Division of positive numbers is positive. *) Lemma Z_quot_pos a b : 0 <= a -> 0 <= b -> 0 <= a÷b. -Proof. intros. zero_or_not b. apply Z.quot_pos; auto with zarith. Qed. +Proof. intros. zero_or_not b. apply Z.quot_pos; lia. Qed. (** As soon as the divisor is greater or equal than 2, the division is strictly decreasing. *) Lemma Z_quot_lt a b : 0 < a -> 2 <= b -> a÷b < a. -Proof. intros. apply Z.quot_lt; auto with zarith. Qed. +Proof. intros. apply Z.quot_lt; lia. Qed. (** [<=] is compatible with a positive division. *) Lemma Z_quot_monotone a b c : 0<=c -> a<=b -> a÷c <= b÷c. -Proof. intros. zero_or_not c. apply Z.quot_le_mono; auto with zarith. Qed. +Proof. intros. zero_or_not c. apply Z.quot_le_mono; lia. Qed. (** With our choice of division, rounding of (a÷b) is always done toward 0: *) @@ -228,12 +228,12 @@ Proof. intros. zero_or_not b. apply Z.mul_quot_ge; auto with zarith. Qed. iff the modulo is zero. *) Lemma Z_quot_exact_full a b : a = b*(a÷b) <-> Z.rem a b = 0. -Proof. intros. zero_or_not b. intuition. apply Z.quot_exact; auto. Qed. +Proof. intros. zero_or_not b. apply Z.quot_exact; auto. Qed. (** A modulo cannot grow beyond its starting point. *) Theorem Zrem_le a b : 0 <= a -> 0 <= b -> Z.rem a b <= a. -Proof. intros. zero_or_not b. apply Z.rem_le; auto with zarith. Qed. +Proof. intros. zero_or_not b. apply Z.rem_le; lia. Qed. (** Some additional inequalities about Zdiv. *) @@ -357,7 +357,7 @@ Qed. Theorem Zquot_mult_le: forall a b c, 0<=a -> 0<=b -> 0<=c -> c*(a÷b) <= (c*a)÷b. -Proof. intros. zero_or_not b. apply Z.quot_mul_le; auto with zarith. Qed. +Proof. intros. zero_or_not b. apply Z.quot_mul_le; lia. Qed. (** Z.rem is related to divisibility (see more in Znumtheory) *) @@ -376,7 +376,7 @@ Lemma Zquot2_odd_remainder : forall a, Proof. intros [ |p|p]. simpl. left. simpl. auto with zarith. - left. destruct p; simpl; auto with zarith. + left. destruct p; simpl; lia. right. destruct p; simpl; split; now auto with zarith. Qed. @@ -414,10 +414,10 @@ Theorem Zquotrem_Zdiv_eucl_pos : forall a b:Z, 0 <= a -> 0 < b -> Proof. intros. apply Zdiv_mod_unique with b. - apply Zrem_lt_pos; auto with zarith. - rewrite Z.abs_eq; auto with *; apply Z_mod_lt; auto with *. - rewrite <- Z_div_mod_eq; auto with *. - symmetry; apply Z.quot_rem; auto with *. + apply Zrem_lt_pos; lia. + rewrite Z.abs_eq by lia. apply Z_mod_lt; lia. + rewrite <- Z_div_mod_eq by lia. + symmetry; apply Z.quot_rem; lia. Qed. Theorem Zquot_Zdiv_pos : forall a b, 0 <= a -> 0 <= b -> diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v index 853ec951ae..ca04bb4c8f 100644 --- a/theories/ZArith/Zwf.v +++ b/theories/ZArith/Zwf.v @@ -10,7 +10,7 @@ Require Import ZArith_base. Require Export Wf_nat. -Require Import Omega. +Require Import Lia. Local Open Scope Z_scope. (** Well-founded relations on Z. *) @@ -39,20 +39,19 @@ Section wf_proof. clear a; simple induction n; intros. (** n= 0 *) case H; intros. - case (lt_n_O (f a)); auto. + lia. apply Acc_intro; unfold Zwf; intros. - assert False; omega || contradiction. + lia. (** inductive case *) case H0; clear H0; intro; auto. apply Acc_intro; intros. apply H. unfold Zwf in H1. - case (Z.le_gt_cases c y); intro; auto with zarith. + case (Z.le_gt_cases c y); intro. 2: lia. left. - red in H0. apply lt_le_trans with (f a); auto with arith. unfold f. - apply Zabs2Nat.inj_lt; omega. + lia. apply (H (S (f a))); auto. Qed. @@ -83,9 +82,7 @@ Section wf_proof_up. Proof. apply well_founded_lt_compat with (f := f). unfold Zwf_up, f. - intros. - apply Zabs2Nat.inj_lt; try (apply Z.le_0_sub; intuition). - now apply Z.sub_lt_mono_l. + lia. Qed. End wf_proof_up. diff --git a/toplevel/coqc.ml b/toplevel/coqc.ml index 642dc94ab2..98206fb341 100644 --- a/toplevel/coqc.ml +++ b/toplevel/coqc.ml @@ -53,11 +53,7 @@ let coqc_main copts ~opts = if opts.Coqargs.post.Coqargs.output_context then begin let sigma, env = let e = Global.env () in Evd.from_env e, e in - let library_accessor = Library.indirect_accessor in - let mod_ops = { Printmod.import_module = Declaremods.import_module - ; process_module_binding = Declaremods.process_module_binding - } in - Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context ~mod_ops ~library_accessor env) sigma) ++ fnl ()) + Feedback.msg_notice Pp.(Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ()) end; CProfile.print_profile () diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml new file mode 100644 index 0000000000..737e0427ec --- /dev/null +++ b/vernac/comArguments.ml @@ -0,0 +1,306 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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) *) +(************************************************************************) + +open CAst +open Util +open Names +open Vernacexpr + +let smart_global r = + let gr = Smartlocate.smart_global r in + Dumpglob.add_glob ?loc:r.loc gr; + gr + +let cache_bidi_hints (_name, (gr, ohint)) = + match ohint with + | None -> Pretyping.clear_bidirectionality_hint gr + | Some nargs -> Pretyping.add_bidirectionality_hint gr nargs + +let load_bidi_hints _ r = + cache_bidi_hints r + +let subst_bidi_hints (subst, (gr, ohint as orig)) = + let gr' = Globnames.subst_global_reference subst gr in + if gr == gr' then orig else (gr', ohint) + +let discharge_bidi_hints (_name, (gr, ohint)) = + if Globnames.isVarRef gr && Lib.is_in_section gr then None + else + let vars = Lib.variable_section_segment_of_reference gr in + let n = List.length vars in + Some (gr, Option.map ((+) n) ohint) + +let inBidiHints = + let open Libobject in + declare_object { (default_object "BIDIRECTIONALITY-HINTS" ) with + load_function = load_bidi_hints; + cache_function = cache_bidi_hints; + classify_function = (fun o -> Substitute o); + subst_function = subst_bidi_hints; + discharge_function = discharge_bidi_hints; + } + + +let warn_arguments_assert = + CWarnings.create ~name:"arguments-assert" ~category:"vernacular" + Pp.(fun sr -> + strbrk "This command is just asserting the names of arguments of " ++ + Printer.pr_global sr ++ strbrk". If this is what you want add " ++ + strbrk "': assert' to silence the warning. If you want " ++ + strbrk "to clear implicit arguments add ': clear implicits'. " ++ + strbrk "If you want to clear notation scopes add ': clear scopes'") + +(* [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 env = Global.env () in + let sigma = Evd.from_env env in + let assert_flag = List.mem `Assert flags in + let rename_flag = List.mem `Rename flags in + let clear_scopes_flag = List.mem `ClearScopes flags in + let extra_scopes_flag = List.mem `ExtraScopes flags in + let clear_implicits_flag = List.mem `ClearImplicits flags in + let default_implicits_flag = List.mem `DefaultImplicits flags in + let never_unfold_flag = List.mem `ReductionNeverUnfold flags in + let nomatch_flag = List.mem `ReductionDontExposeCase flags in + let clear_bidi_hint = List.mem `ClearBidiHint flags in + + let err_incompat x y = + CErrors.user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in + + if assert_flag && rename_flag then + err_incompat "assert" "rename"; + if clear_scopes_flag && extra_scopes_flag then + err_incompat "clear scopes" "extra scopes"; + if clear_implicits_flag && default_implicits_flag then + err_incompat "clear implicits" "default implicits"; + + let sr = smart_global reference in + let inf_names = + let ty, _ = Typeops.type_of_global_in_context env sr in + Impargs.compute_implicits_names env sigma (EConstr.of_constr ty) + in + let prev_names = + try Arguments_renaming.arguments_names sr with Not_found -> inf_names + in + let num_args = List.length inf_names in + assert (Int.equal num_args (List.length prev_names)); + + let names_of args = List.map (fun a -> a.name) args in + + (* Checks *) + + let err_extra_args names = + CErrors.user_err ~hdr:"vernac_declare_arguments" + Pp.(strbrk "Extra arguments: " ++ + prlist_with_sep pr_comma Name.print names ++ str ".") + in + let err_missing_args names = + CErrors.user_err ~hdr:"vernac_declare_arguments" + Pp.(strbrk "The following arguments are not declared: " ++ + prlist_with_sep pr_comma Name.print names ++ str ".") + in + + let rec check_extra_args extra_args = + match extra_args with + | [] -> () + | { notation_scope = None } :: _ -> + CErrors.user_err Pp.(str"Extra arguments should specify a scope.") + | { notation_scope = Some _ } :: args -> check_extra_args args + in + + let args, scopes = + let scopes = List.map (fun { notation_scope = s } -> s) args in + if List.length args > num_args then + let args, extra_args = List.chop num_args args in + if extra_scopes_flag then + (check_extra_args extra_args; (args, scopes)) + else err_extra_args (names_of extra_args) + else args, scopes + in + + if Option.cata (fun n -> n > num_args) false nargs_for_red then + CErrors.user_err Pp.(str "The \"/\" modifier should be put before any extra scope."); + + if Option.cata (fun n -> n > num_args) false nargs_before_bidi then + CErrors.user_err Pp.(str "The \"&\" modifier should be put before any extra scope."); + + let scopes_specified = List.exists Option.has_some scopes in + + if scopes_specified && clear_scopes_flag then + CErrors.user_err Pp.(str "The \"clear scopes\" flag is incompatible with scope annotations."); + + let names = List.map (fun { name } -> name) args in + let names = names :: List.map (List.map fst) more_implicits in + + let rename_flag_required = ref false in + let example_renaming = ref None in + let save_example_renaming renaming = + rename_flag_required := !rename_flag_required + || not (Name.equal (fst renaming) Anonymous); + if Option.is_empty !example_renaming then + example_renaming := Some renaming + in + + let rec names_union names1 names2 = + match names1, names2 with + | [], [] -> [] + | _ :: _, [] -> names1 + | [], _ :: _ -> names2 + | (Name _ as name) :: names1, Anonymous :: names2 + | Anonymous :: names1, (Name _ as name) :: names2 -> + name :: names_union names1 names2 + | name1 :: names1, name2 :: names2 -> + if Name.equal name1 name2 then + name1 :: names_union names1 names2 + else CErrors.user_err Pp.(str "Argument lists should agree on the names they provide.") + in + + let names = List.fold_left names_union [] names in + + let rec rename prev_names names = + match prev_names, names with + | [], [] -> [] + | [], _ :: _ -> err_extra_args names + | _ :: _, [] when assert_flag -> + (* Error messages are expressed in terms of original names, not + renamed ones. *) + err_missing_args (List.lastn (List.length prev_names) inf_names) + | _ :: _, [] -> prev_names + | prev :: prev_names, Anonymous :: names -> + prev :: rename prev_names names + | prev :: prev_names, (Name id as name) :: names -> + if not (Name.equal prev name) then save_example_renaming (prev,name); + name :: rename prev_names names + in + + let names = rename prev_names names in + let renaming_specified = Option.has_some !example_renaming in + + if !rename_flag_required && not rename_flag then begin + let msg = let open Pp in + match !example_renaming with + | None -> + strbrk "To rename arguments the \"rename\" flag must be specified." + | Some (o,n) -> + strbrk "Flag \"rename\" expected to rename " ++ Name.print o ++ + strbrk " into " ++ Name.print n ++ str "." + in CErrors.user_err ~hdr:"vernac_declare_arguments" msg + end; + + let duplicate_names = + List.duplicates Name.equal (List.filter ((!=) Anonymous) names) + in + if not (List.is_empty duplicate_names) then begin + CErrors.user_err Pp.(strbrk "Some argument names are duplicated: " ++ + prlist_with_sep pr_comma Name.print duplicate_names) + end; + + let implicits = + List.map (fun { name; implicit_status = i } -> (name,i)) args + in + let implicits = implicits :: more_implicits in + + let implicits = List.map (List.map snd) implicits in + let implicits_specified = match implicits with + | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l + | _ -> true in + + if implicits_specified && clear_implicits_flag then + CErrors.user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations"); + + if implicits_specified && default_implicits_flag then + CErrors.user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations"); + + let rargs = + Util.List.map_filter (function (n, true) -> Some n | _ -> None) + (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 args) + in + + let red_behavior = + let open Reductionops.ReductionBehaviour in + match never_unfold_flag, nomatch_flag, rargs, nargs_for_red with + | true, false, [], None -> Some NeverUnfold + | true, true, _, _ -> err_incompat "simpl never" "simpl nomatch" + | true, _, _::_, _ -> err_incompat "simpl never" "!" + | true, _, _, Some _ -> err_incompat "simpl never" "/" + | false, false, [], None -> None + | false, false, _, _ -> Some (UnfoldWhen { nargs = nargs_for_red; + recargs = rargs; + }) + | false, true, _, _ -> Some (UnfoldWhenNoMatch { nargs = nargs_for_red; + recargs = rargs; + }) + in + + + let red_modifiers_specified = Option.has_some red_behavior in + + let bidi_hint_specified = Option.has_some nargs_before_bidi in + + if bidi_hint_specified && clear_bidi_hint then + err_incompat "clear bidirectionality hint" "&"; + + + (* Actions *) + + if renaming_specified then begin + Arguments_renaming.rename_arguments section_local sr names + end; + + if scopes_specified || clear_scopes_flag then begin + let scopes = List.map (Option.map (fun {loc;v=k} -> + try ignore (Notation.find_scope k); k + with CErrors.UserError _ -> + Notation.find_delimiters_scope ?loc k)) scopes + in + Notation.declare_arguments_scope section_local (smart_global reference) scopes + end; + + if implicits_specified || clear_implicits_flag then + Impargs.set_implicits section_local (smart_global reference) implicits; + + if default_implicits_flag then + Impargs.declare_implicits section_local (smart_global reference); + + if red_modifiers_specified then begin + match sr with + | GlobRef.ConstRef _ -> + Reductionops.ReductionBehaviour.set + ~local:section_local sr (Option.get red_behavior) + + | _ -> + CErrors.user_err + Pp.(strbrk "Modifiers of the behavior of the simpl tactic "++ + strbrk "are relevant for constants only.") + end; + + if bidi_hint_specified then begin + let n = Option.get nargs_before_bidi in + if section_local then + Pretyping.add_bidirectionality_hint sr n + else + Lib.add_anonymous_leaf (inBidiHints (sr, Some n)) + end; + + if clear_bidi_hint then begin + if section_local then + Pretyping.clear_bidirectionality_hint sr + else + Lib.add_anonymous_leaf (inBidiHints (sr, None)) + end; + + if not (renaming_specified || + implicits_specified || + scopes_specified || + red_modifiers_specified || + bidi_hint_specified) && (List.is_empty flags) then + warn_arguments_assert sr diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli new file mode 100644 index 0000000000..f78e01a11f --- /dev/null +++ b/vernac/comArguments.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) +(* <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) *) +(************************************************************************) + +val vernac_arguments + : section_local:bool + -> 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/declaremods.ml b/vernac/declaremods.ml index c7b68d18c2..65cd4cd6a4 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -1068,3 +1068,9 @@ let debug_print_modtab _ = in let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in hov 0 modules + + +let mod_ops = { + Printmod.import_module = import_module; + process_module_binding = process_module_binding; +} diff --git a/vernac/declaremods.mli b/vernac/declaremods.mli index ae84704656..23f25bc597 100644 --- a/vernac/declaremods.mli +++ b/vernac/declaremods.mli @@ -126,3 +126,5 @@ val debug_print_modtab : unit -> Pp.t val process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit + +val mod_ops : Printmod.mod_ops diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index f91983d31c..3dbf7afb78 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1082,8 +1082,13 @@ let string_of_definition_object_kind = let open Decls in function 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 - | _, _, [] -> mt() + | _, 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; notation_scope = s; implicit_status = imp } :: tl -> diff --git a/printing/prettyp.ml b/vernac/prettyp.ml index c995887f31..5ebc89892c 100644 --- a/printing/prettyp.ml +++ b/vernac/prettyp.ml @@ -17,7 +17,6 @@ open CErrors open Util open CAst open Names -open Nameops open Termops open Declarations open Environ @@ -30,25 +29,27 @@ open Printer open Printmod open Context.Rel.Declaration -(* module RelDecl = Context.Rel.Declaration *) +module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration type object_pr = { print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; - print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; + print_module : bool -> ModPath.t -> Pp.t; + print_modtype : ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; - print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } -let gallina_print_module = print_module -let gallina_print_modtype = print_modtype +let gallina_print_module = print_module ~mod_ops:Declaremods.mod_ops +let gallina_print_modtype = print_modtype ~mod_ops:Declaremods.mod_ops + + (**************) (** Utilities *) @@ -94,7 +95,7 @@ let print_ref reduce ref udecl = else mt () in let priv = None in (* We deliberately don't print private univs in About. *) - hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ + hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ Printer.pr_abstract_universe_ctx sigma ?variance univs ?priv) (********************************) @@ -123,25 +124,20 @@ let print_impargs_list prefix l = List.flatten (List.map (fun (cond,imps) -> match cond with | None -> - List.map (fun pp -> add_colon prefix ++ pp) - (print_one_impargs_list imps) + List.map (fun pp -> add_colon prefix ++ pp) + (print_one_impargs_list imps) | Some (n1,n2) -> [v 2 (prlist_with_sep cut (fun x -> x) - [(if ismt prefix then str "When" else prefix ++ str ", when") ++ - str " applied to " ++ - (if Int.equal n1 n2 then int_or_no n2 else - if Int.equal n1 0 then str "no more than " ++ int n2 - else int n1 ++ str " to " ++ int_or_no n2) ++ - str (String.plural n2 " argument") ++ str ":"; + [(if ismt prefix then str "When" else prefix ++ str ", when") ++ + str " applied to " ++ + (if Int.equal n1 n2 then int_or_no n2 else + if Int.equal n1 0 then str "no more than " ++ int n2 + else int n1 ++ str " to " ++ int_or_no n2) ++ + str (String.plural n2 " argument") ++ str ":"; v 0 (prlist_with_sep cut (fun x -> x) - (if List.exists is_status_implicit imps - then print_one_impargs_list imps - else [str "No implicit arguments"]))])]) l) - -let print_renames_list prefix l = - if List.is_empty l then [] else - [add_colon prefix ++ str "Arguments are renamed to " ++ - hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))] + (if List.exists is_status_implicit imps + then print_one_impargs_list imps + else [str "No implicit arguments"]))])]) l) let need_expansion impl ref = let typ, _ = Typeops.type_of_global_in_context (Global.env ()) ref in @@ -163,19 +159,6 @@ let print_impargs ref = else [str "No implicit arguments"])) (*********************) -(** Printing Scopes *) - -let print_argument_scopes prefix = function - | [Some sc] -> - [add_colon prefix ++ str"Argument scope is [" ++ str sc ++ str"]"] - | l when not (List.for_all Option.is_empty l) -> - [add_colon prefix ++ hov 2 (str"Argument scopes are" ++ spc() ++ - str "[" ++ - pr_sequence (function Some sc -> str sc | None -> str "_") l ++ - str "]")] - | _ -> [] - -(*********************) (** Printing Opacity *) type opacity = @@ -191,8 +174,8 @@ let opacity env = let cb = Environ.lookup_constant cst env in (match cb.const_body with | Undef _ | Primitive _ -> None - | OpaqueDef _ -> Some FullyOpaque - | Def _ -> Some + | OpaqueDef _ -> Some FullyOpaque + | Def _ -> Some (TransparentMaybeOpacified (Conv_oracle.get_strategy (Environ.oracle env) (ConstKey cst)))) | _ -> None @@ -254,19 +237,91 @@ let print_primitive_record recflag mipv = function | FakeRecord | NotRecord -> [] let print_primitive ref = - match ref with + match ref with | GlobRef.IndRef ind -> let mib,_ = Global.lookup_inductive ind in print_primitive_record mib.mind_finite mib.mind_packets mib.mind_record | _ -> [] -let print_name_infos ref = - let impls = implicits_of_global ref in +let needs_extra_scopes ref scopes = + let open Constr in + let rec aux env t = function + | [] -> false + | _::scopes -> match kind (Reduction.whd_all env t) with + | Prod (na,dom,codom) -> aux (push_rel (RelDecl.LocalAssum (na,dom)) env) codom scopes + | _ -> true + in + let env = Global.env() in + let ty, _ctx = Typeops.type_of_global_in_context env ref in + aux env ty scopes + +let implicit_kind_of_status = function + | None -> Anonymous, NotImplicit + | Some (id,_,(maximal,_)) -> Name id, if maximal then MaximallyImplicit else Implicit + +let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} = + name = Anonymous && not recarg_like && notation_scope = None && implicit_status = NotImplicit + +let rec main_implicits i renames recargs scopes impls = + if renames = [] && recargs = [] && scopes = [] && impls = [] then [] + else + let recarg_like, recargs = match recargs with + | j :: recargs when i = j -> true, recargs + | _ -> false, recargs + in + let (name, implicit_status) = + match renames, impls with + | _, (Some _ as i) :: _ -> implicit_kind_of_status i + | name::_, _ -> (name,NotImplicit) + | [], (None::_ | []) -> (Anonymous, NotImplicit) + in + let notation_scope = match scopes with + | scope :: _ -> Option.map CAst.make scope + | [] -> None + in + let status = {Vernacexpr.implicit_status; name; recarg_like; notation_scope} in + let tl = function [] -> [] | _::tl -> tl in + (* recargs is special -> tl handled above *) + let rest = main_implicits (i+1) (tl renames) recargs (tl scopes) (tl impls) in + if is_dummy status && rest = [] + then [] (* we may have a trail of dummies due to eg "clear scopes" *) + else status :: rest + +let print_arguments ref = + let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in + let flags, recargs, nargs_for_red = + let open Reductionops.ReductionBehaviour in + match get ref with + | None -> [], [], None + | Some NeverUnfold -> [`ReductionNeverUnfold], [], None + | Some (UnfoldWhen { nargs; recargs }) -> [], recargs, nargs + | Some (UnfoldWhenNoMatch { nargs; recargs }) -> [`ReductionDontExposeCase], recargs, nargs + in + let flags, renames = match Arguments_renaming.arguments_names ref with + | exception Not_found -> flags, [] + | [] -> flags, [] + | renames -> `Rename::flags, renames + in let scopes = Notation.find_arguments_scope ref in - let renames = - try Arguments_renaming.arguments_names ref with Not_found -> [] in + let flags = if needs_extra_scopes ref scopes then `ExtraScopes::flags else flags in + let impls = Impargs.extract_impargs_data (Impargs.implicits_of_global ref) in + let impls, moreimpls = match impls with + | (_, impls) :: rest -> impls, rest + | [] -> assert false + in + 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 [] + 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))] + +let print_name_infos ref = let type_info_for_implicit = - if need_expansion (select_impargs_size 0 impls) ref then + if need_expansion (select_impargs_size 0 (implicits_of_global ref)) ref then (* Need to reduce since implicits are computed with products flattened *) [str "Expanded type for implicit arguments"; print_ref true ref None; blankline] @@ -275,42 +330,15 @@ let print_name_infos ref = print_type_in_type ref @ print_primitive ref @ type_info_for_implicit @ - print_renames_list (mt()) renames @ - print_impargs_list (mt()) impls @ - print_argument_scopes (mt()) scopes @ + print_arguments ref @ print_if_is_coercion ref -let print_id_args_data test pr id l = - if List.exists test l then - pr (str "For " ++ Id.print id) l - else - [] - -let print_args_data_of_inductive_ids get test pr sp mipv = - List.flatten (Array.to_list (Array.mapi - (fun i mip -> - print_id_args_data test pr mip.mind_typename (get (GlobRef.IndRef (sp,i))) @ - List.flatten (Array.to_list (Array.mapi - (fun j idc -> - print_id_args_data test pr idc (get (GlobRef.ConstructRef ((sp,i),j+1)))) - mip.mind_consnames))) - mipv)) - -let print_inductive_implicit_args = - print_args_data_of_inductive_ids - implicits_of_global (fun l -> not (List.is_empty (positions_of_implicits l))) - print_impargs_list - -let print_inductive_renames = - print_args_data_of_inductive_ids - (fun r -> - try Arguments_renaming.arguments_names r with Not_found -> []) - ((!=) Anonymous) - print_renames_list - -let print_inductive_argument_scopes = - print_args_data_of_inductive_ids - Notation.find_arguments_scope (Option.has_some) print_argument_scopes +let print_inductive_args sp mipv = + let flatmapi f v = List.flatten (Array.to_list (Array.mapi f v)) in + flatmapi + (fun i mip -> print_arguments (GlobRef.IndRef (sp,i)) @ + flatmapi (fun j _ -> print_arguments (GlobRef.ConstructRef ((sp,i),j+1))) + mip.mind_consnames) mipv let print_bidi_hints gr = match Pretyping.get_bidirectionality_hint gr with @@ -367,10 +395,10 @@ let locate_any_name qid = let pr_located_qualid = function | Term ref -> let ref_str = let open GlobRef in match ref with - ConstRef _ -> "Constant" - | IndRef _ -> "Inductive" - | ConstructRef _ -> "Constructor" - | VarRef _ -> "Variable" in + ConstRef _ -> "Constant" + | IndRef _ -> "Inductive" + | ConstructRef _ -> "Constructor" + | VarRef _ -> "Variable" in str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref) | Syntactic kn -> str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn) @@ -470,19 +498,19 @@ let print_located_qualid name flags qid = in match located with | [] -> - let (dir,id) = repr_qualid qid in - if DirPath.is_empty dir then - str "No " ++ str name ++ str " of basename" ++ spc () ++ Id.print id - else - str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid + let (dir,id) = repr_qualid qid in + if DirPath.is_empty dir then + str "No " ++ str name ++ str " of basename" ++ spc () ++ Id.print id + else + str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid | l -> - prlist_with_sep fnl - (fun (o,oqid) -> - hov 2 (pr_located_qualid o ++ - (if not (qualid_eq oqid qid) then - spc() ++ str "(shorter name to refer to it in current context is " + prlist_with_sep fnl + (fun (o,oqid) -> + hov 2 (pr_located_qualid o ++ + (if not (qualid_eq oqid qid) then + spc() ++ str "(shorter name to refer to it in current context is " ++ pr_qualid oqid ++ str")" - else mt ()) ++ + else mt ()) ++ display_alias o)) l let print_located_term ref = print_located_qualid "term" LocTerm ref @@ -509,8 +537,8 @@ let print_named_def env sigma name body typ = let pbody = if Constr.isCast body then surround pbody else pbody in (str "*** [" ++ str name ++ str " " ++ hov 0 (str ":=" ++ brk (1,2) ++ pbody ++ spc () ++ - str ":" ++ brk (1,2) ++ ptyp) ++ - str "]") + str ":" ++ brk (1,2) ++ ptyp) ++ + str "]") let print_named_assum env sigma name typ = str "*** [" ++ str name ++ str " : " ++ pr_ltype_env env sigma typ ++ str "]" @@ -536,9 +564,7 @@ let gallina_print_inductive sp udecl = pr_mutual_inductive_body env sp mib udecl ++ with_line_skip (print_primitive_record mib.mind_finite mipv mib.mind_record @ - print_inductive_renames sp mipv @ - print_inductive_implicit_args sp mipv @ - print_inductive_argument_scopes sp mipv) + print_inductive_args sp mipv) let print_named_decl env sigma id = gallina_print_named_decl env sigma (Global.lookup_named id) ++ fnl () @@ -561,9 +587,9 @@ let print_instance sigma cb = pr_universe_instance sigma inst else mt() -let print_constant indirect_accessor with_values sep sp udecl = +let print_constant with_values sep sp udecl = let cb = Global.lookup_constant sp in - let val_0 = Global.body_of_constant_body indirect_accessor cb in + let val_0 = Global.body_of_constant_body Library.indirect_accessor cb in let typ = cb.const_type in let univs = let open Univ in @@ -571,7 +597,7 @@ let print_constant indirect_accessor with_values sep sp udecl = match cb.const_body with | Undef _ | Def _ | Primitive _ -> cb.const_universes | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints indirect_accessor otab o in + let body_uctxs = Opaqueproof.force_constraints Library.indirect_accessor otab o in match cb.const_universes with | Monomorphic ctx -> Monomorphic (ContextSet.union body_uctxs ctx) @@ -588,21 +614,21 @@ let print_constant indirect_accessor with_values sep sp udecl = hov 0 ( match val_0 with | None -> - str"*** [ " ++ - print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ - str" ]" ++ + str"*** [ " ++ + print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ + str" ]" ++ Printer.pr_universes sigma univs | Some (c, priv, ctx) -> let priv = match priv with | Opaqueproof.PrivateMonomorphic () -> None | Opaqueproof.PrivatePolymorphic (_, ctx) -> Some ctx in - print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ - (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ + print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ + (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ Printer.pr_universes sigma univs ?priv) -let gallina_print_constant_with_infos indirect_accessor sp udecl = - print_constant indirect_accessor true " = " sp udecl ++ +let gallina_print_constant_with_infos sp udecl = + print_constant true " = " sp udecl ++ with_line_skip (print_name_infos (GlobRef.ConstRef sp)) let gallina_print_syntactic_def env kn = @@ -618,38 +644,38 @@ let gallina_print_syntactic_def env kn = Constrextern.without_specific_symbols [Notation.SynDefRule kn] (pr_glob_constr_env env) c) -let gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values ((sp,kn as oname),lobj) = +let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) = let sep = if with_values then " = " else " : " in match lobj with | AtomicObject o -> let tag = object_tag o in begin match (oname,tag) with | (_,"VARIABLE") -> - (* Outside sections, VARIABLES still exist but only with universes + (* Outside sections, VARIABLES still exist but only with universes constraints *) (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None) | (_,"CONSTANT") -> - Some (print_constant indirect_accessor with_values sep (Constant.make1 kn) None) + Some (print_constant with_values sep (Constant.make1 kn) None) | (_,"INDUCTIVE") -> Some (gallina_print_inductive (MutInd.make1 kn) None) | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"| - "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None + "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None (* To deal with forgotten cases... *) | (_,s) -> None end | ModuleObject _ -> let (mp,l) = KerName.repr kn in - Some (print_module ~mod_ops with_values (MPdot (mp,l))) + Some (print_module with_values ~mod_ops:Declaremods.mod_ops (MPdot (mp,l))) | ModuleTypeObject _ -> let (mp,l) = KerName.repr kn in - Some (print_modtype ~mod_ops (MPdot (mp,l))) + Some (print_modtype ~mod_ops:Declaremods.mod_ops (MPdot (mp,l))) | _ -> None -let gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values ent = +let gallina_print_library_entry env sigma with_values ent = let pr_name (sp,_) = Id.print (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> - gallina_print_leaf_entry ~mod_ops indirect_accessor env sigma with_values (oname,lobj) + gallina_print_leaf_entry env sigma with_values (oname,lobj) | (oname,Lib.OpenedSection (dir,_)) -> Some (str " >>>>>>> Section " ++ pr_name oname) | (_,Lib.CompilingLibrary { Nametab.obj_dir; _ }) -> @@ -657,10 +683,10 @@ let gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values | (oname,Lib.OpenedModule _) -> Some (str " >>>>>>> Module " ++ pr_name oname) -let gallina_print_context ~mod_ops indirect_accessor env sigma with_values = +let gallina_print_context env sigma with_values = let rec prec n = function | h::rest when Option.is_empty n || Option.get n > 0 -> - (match gallina_print_library_entry ~mod_ops indirect_accessor env sigma with_values h with + (match gallina_print_library_entry env sigma with_values h with | None -> prec n rest | Some pp -> prec (Option.map ((+) (-1)) n) rest ++ pp ++ fnl ()) | _ -> mt () @@ -698,8 +724,8 @@ let print_syntactic_def x = !object_pr.print_syntactic_def x let print_module x = !object_pr.print_module x let print_modtype x = !object_pr.print_modtype x let print_named_decl x = !object_pr.print_named_decl x -let print_library_entry ~mod_ops x = !object_pr.print_library_entry ~mod_ops x -let print_context ~mod_ops x = !object_pr.print_context ~mod_ops x +let print_library_entry x = !object_pr.print_library_entry x +let print_context x = !object_pr.print_context x let print_typed_value_in_env x = !object_pr.print_typed_value_in_env x let print_eval x = !object_pr.print_eval x @@ -720,30 +746,32 @@ let print_safe_judgment env sigma j = (*********************) (* *) -let print_full_context ~mod_ops indirect_accessor env sigma = - print_context ~mod_ops indirect_accessor env sigma true None (Lib.contents ()) -let print_full_context_typ ~mod_ops indirect_accessor env sigma = - print_context ~mod_ops indirect_accessor env sigma false None (Lib.contents ()) +let print_full_context env sigma = + print_context env sigma true None (Lib.contents ()) +let print_full_context_typ env sigma = + print_context env sigma false None (Lib.contents ()) -let print_full_pure_context ~mod_ops ~library_accessor env sigma = +let print_full_pure_context env sigma = let rec prec = function | ((_,kn),Lib.Leaf AtomicObject lobj)::rest -> let pp = match object_tag lobj with | "CONSTANT" -> - let con = Global.constant_of_delta_kn kn in - let cb = Global.lookup_constant con in - let typ = cb.const_type in - hov 0 ( - match cb.const_body with - | Undef _ -> - str "Parameter " ++ + let con = Global.constant_of_delta_kn kn in + let cb = Global.lookup_constant con in + let typ = cb.const_type in + hov 0 ( + match cb.const_body with + | Undef _ -> + str "Parameter " ++ print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ - | OpaqueDef lc -> - str "Theorem " ++ print_basename con ++ cut () ++ + | OpaqueDef lc -> + str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof library_accessor (Global.opaque_tables ()) lc)) + str "Proof " ++ pr_lconstr_env env sigma + (fst (Opaqueproof.force_proof Library.indirect_accessor + (Global.opaque_tables ()) lc)) | Def c -> - str "Definition " ++ print_basename con ++ cut () ++ + str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ pr_lconstr_env env sigma (Mod_subst.force_constr c) | Primitive _ -> @@ -751,20 +779,20 @@ let print_full_pure_context ~mod_ops ~library_accessor env sigma = print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ) ++ str "." ++ fnl () ++ fnl () | "INDUCTIVE" -> - let mind = Global.mind_of_delta_kn kn in - let mib = Global.lookup_mind mind in + let mind = Global.mind_of_delta_kn kn in + let mib = Global.lookup_mind mind in pr_mutual_inductive_body (Global.env()) mind mib None ++ - str "." ++ fnl () ++ fnl () + str "." ++ fnl () ++ fnl () | _ -> mt () in prec rest ++ pp | ((_,kn),Lib.Leaf ModuleObject _)::rest -> (* TODO: make it reparsable *) let (mp,l) = KerName.repr kn in - prec rest ++ print_module ~mod_ops true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + prec rest ++ print_module true (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | ((_,kn),Lib.Leaf ModuleTypeObject _)::rest -> (* TODO: make it reparsable *) let (mp,l) = KerName.repr kn in - prec rest ++ print_modtype ~mod_ops (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () + prec rest ++ print_modtype (MPdot (mp,l)) ++ str "." ++ fnl () ++ fnl () | _::rest -> prec rest | _ -> mt () in prec (Lib.contents ()) @@ -789,11 +817,11 @@ let read_sec_context qid = let cxt = Lib.contents () in List.rev (get_cxt [] cxt) -let print_sec_context ~mod_ops indirect_accessor env sigma sec = - print_context ~mod_ops indirect_accessor env sigma true None (read_sec_context sec) +let print_sec_context env sigma sec = + print_context env sigma true None (read_sec_context sec) -let print_sec_context_typ ~mod_ops indirect_accessor env sigma sec = - print_context ~mod_ops indirect_accessor env sigma false None (read_sec_context sec) +let print_sec_context_typ env sigma sec = + print_context env sigma false None (read_sec_context sec) let maybe_error_reject_univ_decl na udecl = let open GlobRef in @@ -803,19 +831,19 @@ let maybe_error_reject_univ_decl na udecl = (* TODO Print na somehow *) user_err ~hdr:"reject_univ_decl" (str "This object does not support universe names.") -let print_any_name ~mod_ops indirect_accessor env sigma na udecl = +let print_any_name env sigma na udecl = maybe_error_reject_univ_decl na udecl; let open GlobRef in match na with - | Term (ConstRef sp) -> print_constant_with_infos indirect_accessor sp udecl + | Term (ConstRef sp) -> print_constant_with_infos sp udecl | Term (IndRef (sp,_)) -> print_inductive sp udecl | Term (ConstructRef ((sp,_),_)) -> print_inductive sp udecl | Term (VarRef sp) -> print_section_variable env sigma sp | Syntactic kn -> print_syntactic_def env kn | Dir (Nametab.GlobDirRef.DirModule Nametab.{ obj_dir; obj_mp; _ } ) -> - print_module ~mod_ops (printable_body obj_dir) obj_mp + print_module (printable_body obj_dir) obj_mp | Dir _ -> mt () - | ModuleType mp -> print_modtype ~mod_ops mp + | ModuleType mp -> print_modtype mp | Other (obj, info) -> info.print obj | Undefined qid -> try (* Var locale de but, pas var de section... donc pas d'implicits *) @@ -827,23 +855,23 @@ let print_any_name ~mod_ops indirect_accessor env sigma na udecl = user_err ~hdr:"print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.") -let print_name ~mod_ops indirect_accessor env sigma na udecl = +let print_name env sigma na udecl = match na with | {loc; v=Constrexpr.ByNotation (ntn,sc)} -> - print_any_name ~mod_ops indirect_accessor env sigma + print_any_name env sigma (Term (Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc)) udecl | {loc; v=Constrexpr.AN ref} -> - print_any_name ~mod_ops indirect_accessor env sigma (locate_any_name ref) udecl + print_any_name env sigma (locate_any_name ref) udecl -let print_opaque_name indirect_accessor env sigma qid = +let print_opaque_name env sigma qid = let open GlobRef in match Nametab.global qid with | ConstRef cst -> let cb = Global.lookup_constant cst in if Declareops.constant_has_body cb then - print_constant_with_infos indirect_accessor cst None + print_constant_with_infos cst None else user_err Pp.(str "Not a defined constant.") | IndRef (sp,_) -> @@ -865,9 +893,9 @@ let print_about_any ?loc env sigma k udecl = 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 @ + print_name_infos ref @ + (if Pp.ismt rb then [] else [rb]) @ + print_opacity ref @ print_bidi_hints ref @ [hov 0 (str "Expands to: " ++ pr_located_qualid k)]) | Syntactic kn -> @@ -891,8 +919,8 @@ let print_about env sigma na udecl = print_about_any ?loc env sigma (locate_any_name ref) udecl (* for debug *) -let inspect ~mod_ops indirect_accessor env sigma depth = - print_context ~mod_ops indirect_accessor env sigma false (Some depth) (Lib.contents ()) +let inspect env sigma depth = + print_context env sigma false (Some depth) (Lib.contents ()) (*************************************************************************) (* Pretty-printing functions coming from classops.ml *) @@ -938,7 +966,7 @@ let print_path_between cls clt = with Not_found -> user_err ~hdr:"index_cl_of_id" (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt - ++ str ".") + ++ str ".") in print_path ((i,j),p) diff --git a/printing/prettyp.mli b/vernac/prettyp.mli index c8b361d95b..dc4280f286 100644 --- a/printing/prettyp.mli +++ b/vernac/prettyp.mli @@ -19,48 +19,31 @@ val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref val print_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map + : env + -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t val print_library_entry - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map - -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option -val print_full_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t -val print_full_context_typ - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> Pp.t - -val print_full_pure_context - : mod_ops:Printmod.mod_ops - -> library_accessor:Opaqueproof.indirect_accessor - -> env + : env -> Evd.evar_map - -> Pp.t + -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option +val print_full_context : env -> Evd.evar_map -> Pp.t +val print_full_context_typ : env -> Evd.evar_map -> Pp.t + +val print_full_pure_context : env -> Evd.evar_map -> Pp.t -val print_sec_context - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t -val print_sec_context_typ - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map -> qualid Constrexpr.or_by_notation - -> UnivNames.univ_name_list option -> Pp.t -val print_opaque_name - : Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> qualid -> Pp.t +val print_name : env -> Evd.evar_map + -> qualid Constrexpr.or_by_notation + -> UnivNames.univ_name_list option + -> Pp.t +val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t @@ -77,10 +60,7 @@ val print_typeclasses : unit -> Pp.t val print_instances : GlobRef.t -> Pp.t val print_all_instances : unit -> Pp.t -val inspect - : mod_ops:Printmod.mod_ops - -> Opaqueproof.indirect_accessor - -> env -> Evd.evar_map -> int -> Pp.t +val inspect : env -> Evd.evar_map -> int -> Pp.t (** {5 Locate} *) @@ -113,14 +93,14 @@ val print_located_other : string -> qualid -> Pp.t type object_pr = { print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; - print_constant_with_infos : Opaqueproof.indirect_accessor -> Constant.t -> UnivNames.univ_name_list option -> Pp.t; + print_constant_with_infos : Constant.t -> UnivNames.univ_name_list option -> Pp.t; print_section_variable : env -> Evd.evar_map -> variable -> Pp.t; print_syntactic_def : env -> KerName.t -> Pp.t; - print_module : mod_ops:Printmod.mod_ops -> bool -> ModPath.t -> Pp.t; - print_modtype : mod_ops:Printmod.mod_ops -> ModPath.t -> Pp.t; + print_module : bool -> ModPath.t -> Pp.t; + print_modtype : ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; - print_context : mod_ops:Printmod.mod_ops -> Opaqueproof.indirect_accessor -> env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; + print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; + print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 956b56e256..5226c2ba65 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -19,6 +19,7 @@ DeclareObl Canonical RecLemmas Library +Prettyp Lemmas Class Auto_ind_decl @@ -38,6 +39,7 @@ Assumptions Mltop Topfmt Loadpath +ComArguments Vernacentries Vernacstate Vernacinterp diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 684d8a3d90..edff80af00 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -15,7 +15,6 @@ open CErrors open CAst open Util open Names -open Nameops open Tacmach open Constrintern open Prettyp @@ -176,7 +175,7 @@ let print_module qid = let globdir = Nametab.locate_dir qid in match globdir with DirModule Nametab.{ obj_dir; obj_mp; _ } -> - Printmod.print_module (Printmod.printable_body obj_dir) obj_mp + Printmod.print_module ~mod_ops:Declaremods.mod_ops (Printmod.printable_body obj_dir) obj_mp | _ -> raise Not_found with Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) @@ -184,12 +183,12 @@ let print_module qid = let print_modtype qid = try let kn = Nametab.locate_modtype qid in - Printmod.print_modtype kn + Printmod.print_modtype ~mod_ops:Declaremods.mod_ops kn with Not_found -> (* Is there a module of this name ? If yes we display its type *) try let mp = Nametab.locate_module qid in - Printmod.print_module false mp + Printmod.print_module ~mod_ops:Declaremods.mod_ops false mp with Not_found -> user_err (str"Unknown Module Type or Module " ++ pr_qualid qid) @@ -448,9 +447,6 @@ let vernac_bind_scope ~module_local sc cll = let vernac_open_close_scope ~section_local (b,s) = Notation.open_close_scope (section_local,b,s) -let vernac_arguments_scope ~section_local r scl = - Notation.declare_arguments_scope section_local (smart_global r) scl - let vernac_infix ~atts = let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in Metasyntax.add_infix ~local:module_local deprecation (Global.env()) @@ -655,7 +651,7 @@ let vernac_record ~template udecl cum k poly finite records = let cumulative = should_treat_as_cumulative cum poly in let map ((coe, id), binders, sort, nameopt, cfs) = let const = match nameopt with - | None -> add_prefix "Build_" id.v + | None -> Nameops.add_prefix "Build_" id.v | Some lid -> let () = Dumpglob.dump_definition lid false "constr" in lid.v @@ -1213,292 +1209,6 @@ let vernac_syntactic_definition ~atts lid x compat = Dumpglob.dump_definition lid false "syndef"; Metasyntax.add_syntactic_definition ~local:module_local deprecation (Global.env()) lid.v x compat -let cache_bidi_hints (_name, (gr, ohint)) = - match ohint with - | None -> Pretyping.clear_bidirectionality_hint gr - | Some nargs -> Pretyping.add_bidirectionality_hint gr nargs - -let load_bidi_hints _ r = - cache_bidi_hints r - -let subst_bidi_hints (subst, (gr, ohint as orig)) = - let gr' = subst_global_reference subst gr in - if gr == gr' then orig else (gr', ohint) - -let discharge_bidi_hints (_name, (gr, ohint)) = - if isVarRef gr && Lib.is_in_section gr then None - else - let vars = Lib.variable_section_segment_of_reference gr in - let n = List.length vars in - Some (gr, Option.map ((+) n) ohint) - -let inBidiHints = - let open Libobject in - declare_object { (default_object "BIDIRECTIONALITY-HINTS" ) with - load_function = load_bidi_hints; - cache_function = cache_bidi_hints; - classify_function = (fun o -> Substitute o); - subst_function = subst_bidi_hints; - discharge_function = discharge_bidi_hints; - } - - -let warn_arguments_assert = - CWarnings.create ~name:"arguments-assert" ~category:"vernacular" - (fun sr -> - strbrk "This command is just asserting the names of arguments of " ++ - pr_global sr ++ strbrk". If this is what you want add " ++ - strbrk "': assert' to silence the warning. If you want " ++ - strbrk "to clear implicit arguments add ': clear implicits'. " ++ - strbrk "If you want to clear notation scopes add ': clear scopes'") - -(* [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 env = Global.env () in - let sigma = Evd.from_env env in - let assert_flag = List.mem `Assert flags in - let rename_flag = List.mem `Rename flags in - let clear_scopes_flag = List.mem `ClearScopes flags in - let extra_scopes_flag = List.mem `ExtraScopes flags in - let clear_implicits_flag = List.mem `ClearImplicits flags in - let default_implicits_flag = List.mem `DefaultImplicits flags in - let never_unfold_flag = List.mem `ReductionNeverUnfold flags in - let nomatch_flag = List.mem `ReductionDontExposeCase flags in - let clear_bidi_hint = List.mem `ClearBidiHint flags in - - let err_incompat x y = - user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in - - if assert_flag && rename_flag then - err_incompat "assert" "rename"; - if clear_scopes_flag && extra_scopes_flag then - err_incompat "clear scopes" "extra scopes"; - if clear_implicits_flag && default_implicits_flag then - err_incompat "clear implicits" "default implicits"; - - let sr = smart_global reference in - let inf_names = - let ty, _ = Typeops.type_of_global_in_context env sr in - Impargs.compute_implicits_names env sigma (EConstr.of_constr ty) - in - let prev_names = - try Arguments_renaming.arguments_names sr with Not_found -> inf_names - in - let num_args = List.length inf_names in - assert (Int.equal num_args (List.length prev_names)); - - let names_of args = List.map (fun a -> a.name) args in - - (* Checks *) - - let err_extra_args names = - user_err ~hdr:"vernac_declare_arguments" - (strbrk "Extra arguments: " ++ - prlist_with_sep pr_comma Name.print names ++ str ".") - in - let err_missing_args names = - user_err ~hdr:"vernac_declare_arguments" - (strbrk "The following arguments are not declared: " ++ - prlist_with_sep pr_comma Name.print names ++ str ".") - in - - let rec check_extra_args extra_args = - match extra_args with - | [] -> () - | { notation_scope = None } :: _ -> - user_err Pp.(str"Extra arguments should specify a scope.") - | { notation_scope = Some _ } :: args -> check_extra_args args - in - - let args, scopes = - let scopes = List.map (fun { notation_scope = s } -> s) args in - if List.length args > num_args then - let args, extra_args = List.chop num_args args in - if extra_scopes_flag then - (check_extra_args extra_args; (args, scopes)) - else err_extra_args (names_of extra_args) - else args, scopes - in - - if Option.cata (fun n -> n > num_args) false nargs_for_red then - user_err Pp.(str "The \"/\" modifier should be put before any extra scope."); - - if Option.cata (fun n -> n > num_args) false nargs_before_bidi then - user_err Pp.(str "The \"&\" modifier should be put before any extra scope."); - - let scopes_specified = List.exists Option.has_some scopes in - - if scopes_specified && clear_scopes_flag then - user_err Pp.(str "The \"clear scopes\" flag is incompatible with scope annotations."); - - let names = List.map (fun { name } -> name) args in - let names = names :: List.map (List.map fst) more_implicits in - - let rename_flag_required = ref false in - let example_renaming = ref None in - let save_example_renaming renaming = - rename_flag_required := !rename_flag_required - || not (Name.equal (fst renaming) Anonymous); - if Option.is_empty !example_renaming then - example_renaming := Some renaming - in - - let rec names_union names1 names2 = - match names1, names2 with - | [], [] -> [] - | _ :: _, [] -> names1 - | [], _ :: _ -> names2 - | (Name _ as name) :: names1, Anonymous :: names2 - | Anonymous :: names1, (Name _ as name) :: names2 -> - name :: names_union names1 names2 - | name1 :: names1, name2 :: names2 -> - if Name.equal name1 name2 then - name1 :: names_union names1 names2 - else user_err Pp.(str "Argument lists should agree on the names they provide.") - in - - let names = List.fold_left names_union [] names in - - let rec rename prev_names names = - match prev_names, names with - | [], [] -> [] - | [], _ :: _ -> err_extra_args names - | _ :: _, [] when assert_flag -> - (* Error messages are expressed in terms of original names, not - renamed ones. *) - err_missing_args (List.lastn (List.length prev_names) inf_names) - | _ :: _, [] -> prev_names - | prev :: prev_names, Anonymous :: names -> - prev :: rename prev_names names - | prev :: prev_names, (Name id as name) :: names -> - if not (Name.equal prev name) then save_example_renaming (prev,name); - name :: rename prev_names names - in - - let names = rename prev_names names in - let renaming_specified = Option.has_some !example_renaming in - - if !rename_flag_required && not rename_flag then begin - let msg = - match !example_renaming with - | None -> - strbrk "To rename arguments the \"rename\" flag must be specified." - | Some (o,n) -> - strbrk "Flag \"rename\" expected to rename " ++ Name.print o ++ - strbrk " into " ++ Name.print n ++ str "." - in user_err ~hdr:"vernac_declare_arguments" msg - end; - - let duplicate_names = - List.duplicates Name.equal (List.filter ((!=) Anonymous) names) - in - if not (List.is_empty duplicate_names) then begin - let duplicates = prlist_with_sep pr_comma Name.print duplicate_names in - user_err (strbrk "Some argument names are duplicated: " ++ duplicates) - end; - - let implicits = - List.map (fun { name; implicit_status = i } -> (name,i)) args - in - let implicits = implicits :: more_implicits in - - let implicits = List.map (List.map snd) implicits in - let implicits_specified = match implicits with - | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l - | _ -> true in - - if implicits_specified && clear_implicits_flag then - user_err Pp.(str "The \"clear implicits\" flag is incompatible with implicit annotations"); - - if implicits_specified && default_implicits_flag then - user_err Pp.(str "The \"default implicits\" flag is incompatible with implicit annotations"); - - let rargs = - Util.List.map_filter (function (n, true) -> Some n | _ -> None) - (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 args) - in - - let red_behavior = - let open Reductionops.ReductionBehaviour in - match never_unfold_flag, nomatch_flag, rargs, nargs_for_red with - | true, false, [], None -> Some NeverUnfold - | true, true, _, _ -> err_incompat "simpl never" "simpl nomatch" - | true, _, _::_, _ -> err_incompat "simpl never" "!" - | true, _, _, Some _ -> err_incompat "simpl never" "/" - | false, false, [], None -> None - | false, false, _, _ -> Some (UnfoldWhen { nargs = nargs_for_red; - recargs = rargs; - }) - | false, true, _, _ -> Some (UnfoldWhenNoMatch { nargs = nargs_for_red; - recargs = rargs; - }) - in - - - let red_modifiers_specified = Option.has_some red_behavior in - - let bidi_hint_specified = Option.has_some nargs_before_bidi in - - if bidi_hint_specified && clear_bidi_hint then - err_incompat "clear bidirectionality hint" "&"; - - - (* Actions *) - - if renaming_specified then begin - Arguments_renaming.rename_arguments section_local sr names - end; - - if scopes_specified || clear_scopes_flag then begin - let scopes = List.map (Option.map (fun {loc;v=k} -> - try ignore (Notation.find_scope k); k - with UserError _ -> - Notation.find_delimiters_scope ?loc k)) scopes - in - vernac_arguments_scope ~section_local reference scopes - end; - - if implicits_specified || clear_implicits_flag then - Impargs.set_implicits section_local (smart_global reference) implicits; - - if default_implicits_flag then - Impargs.declare_implicits section_local (smart_global reference); - - if red_modifiers_specified then begin - match sr with - | GlobRef.ConstRef _ as c -> - Reductionops.ReductionBehaviour.set - ~local:section_local c (Option.get red_behavior) - - | _ -> user_err - (strbrk "Modifiers of the behavior of the simpl tactic "++ - strbrk "are relevant for constants only.") - end; - - if bidi_hint_specified then begin - let n = Option.get nargs_before_bidi in - if section_local then - Pretyping.add_bidirectionality_hint sr n - else - Lib.add_anonymous_leaf (inBidiHints (sr, Some n)) - end; - - if clear_bidi_hint then begin - if section_local then - Pretyping.clear_bidirectionality_hint sr - else - Lib.add_anonymous_leaf (inBidiHints (sr, None)) - end; - - if not (renaming_specified || - implicits_specified || - scopes_specified || - red_modifiers_specified || - bidi_hint_specified) && (List.is_empty flags) then - warn_arguments_assert sr - let default_env () = { Notation_term.ninterp_var_type = Id.Map.empty; ninterp_rec_vars = Id.Map.empty; @@ -1962,29 +1672,26 @@ let print_about_hyp_globs ~pstate ?loc ref_or_by_not udecl glopt = print_about env sigma ref_or_by_not udecl let vernac_print ~pstate ~atts = - let mod_ops = { Printmod.import_module = Declaremods.import_module - ; process_module_binding = Declaremods.process_module_binding - } in let sigma, env = get_current_or_global_context ~pstate in function | PrintTypingFlags -> pr_typing_flags (Environ.typing_flags (Global.env ())) | PrintTables -> print_tables () - | PrintFullContext-> print_full_context_typ ~mod_ops Library.indirect_accessor env sigma - | PrintSectionContext qid -> print_sec_context_typ ~mod_ops Library.indirect_accessor env sigma qid - | PrintInspect n -> inspect ~mod_ops Library.indirect_accessor env sigma n + | PrintFullContext-> print_full_context_typ env sigma + | PrintSectionContext qid -> print_sec_context_typ env sigma qid + | PrintInspect n -> inspect env sigma n | PrintGrammar ent -> Metasyntax.pr_grammar ent | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir | PrintModules -> print_modules () - | PrintModule qid -> print_module ~mod_ops qid - | PrintModuleType qid -> print_modtype ~mod_ops qid + | PrintModule qid -> print_module qid + | PrintModuleType qid -> print_modtype qid | PrintNamespace ns -> print_namespace ~pstate ns | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () | PrintDebugGC -> Mltop.print_gc () | PrintName (qid,udecl) -> dump_global qid; - print_name ~mod_ops Library.indirect_accessor env sigma qid udecl + print_name env sigma qid udecl | PrintGraph -> Prettyp.print_graph () | PrintClasses -> Prettyp.print_classes() | PrintTypeClasses -> Prettyp.print_typeclasses() @@ -2453,7 +2160,8 @@ let translate_vernac ~atts v = let open Vernacextend in match v with VtDefault(fun () -> vernac_syntactic_definition ~atts id c b) | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) -> VtDefault(fun () -> - with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags)) + with_section_locality ~atts + (ComArguments.vernac_arguments qid args more_implicits nargs bidi flags)) | VernacReserve bl -> VtDefault(fun () -> unsupported_attributes atts; diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index b712d7e264..564c55670d 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -257,6 +257,17 @@ type vernac_argument_status = { implicit_status : Impargs.implicit_kind; } +type arguments_modifier = + [ `Assert + | `ClearBidiHint + | `ClearImplicits + | `ClearScopes + | `DefaultImplicits + | `ExtraScopes + | `ReductionDontExposeCase + | `ReductionNeverUnfold + | `Rename ] + type extend_name = (* Name of the vernac entry where the tactic is defined, typically found after the VERNAC EXTEND statement in the source. *) @@ -365,16 +376,16 @@ type nonrec vernac_expr = | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * qualid list | VernacHints of string list * Hints.hints_expr - | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * + | VernacSyntacticDefinition of + lident * (Id.t list * constr_expr) * onlyparsing_flag - | VernacArguments of qualid or_by_notation * + | VernacArguments of + qualid or_by_notation * vernac_argument_status list (* Main arguments status list *) * - (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) * + (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 *) * - [ `ReductionDontExposeCase | `ReductionNeverUnfold | `Rename | - `ExtraScopes | `Assert | `ClearImplicits | `ClearScopes | `ClearBidiHint | - `DefaultImplicits ] list + arguments_modifier list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list) |