New Arguments vernacular

The new vernacular "Arguments" attaches to constants the extra-logical
piece of information regarding implicit arguments, notation scopes and
the behaviour of the simpl tactic. The About vernacular is extended to
print the new extra logical data for simpl.

Examples:

Arguments foo {A B}%type f [T] x.
  (* declares A B and T as implicit arguments, A B maximally inserted.
     declares type_scope on A and B *)

Arguments foo {A%type b%nat} p%myscope q.
  (* declares A and b as maximally inserted implicit arguments.
     declares type_scope on A, nat_scope on b and the scope delimited by
     myscope on p *)

Arguments foo (A B)%type c d.
  (* declares A and b in type_scope, but not as implicit arguments. *)

Arguments foo A B c.
  (* leaves implicit arguments and scopes declared for foo untouched *)

Arguments foo A B c : clear implicits
  (* equivalente too Implicit Arguments foo [] *)

Arguments foo A B c : clear scopes
  (* equivalente too Arguments Scope foo [_ _ _] *)

Arguments foo A B c : clear scopes, clear implicits
Arguments foo A B c : clear implicits, clear scopes
Arguments foo A B c : clear scopes and implicits
Arguments foo A B c : clear implicits and scopes
  (* equivalente too Arguments Scope foo [_ _ _]. Implcit Arguments foo [] *)

Arguments foo A B c : default implicits.
  (* equivalent to Implicit Arguments foo. *)

Arguments foo {A B} x , A [B] x.
  (* equivalent to Implicit Arguments foo [[A] [B]] [B]. *)

Arguments foo a !b c !d.
  (* foo is unfolded by simpl if b and d evaluate to a constructor *)

Arguments foo a b c / d.
  (* foo is unfolded by simpl if applied to 3 arguments *)

Arguments foo a !b c / d.
  (* foo is unfolded by simpl if applied to 3 arguments and if b
     evaluates to a constructor *)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14717 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 93 insertions, 0 deletions

diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
new file mode 100644
index 000000000..139f9e992
--- /dev/null
+++ b/test-suite/output/Arguments.out
@@ -0,0 +1,93 @@
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus avoiding to expose match constructs
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus when applied to 1 argument
+  avoiding to expose match constructs
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus
+  when the 1st argument evaluates to a constructor and
+  when applied to 1 argument avoiding to expose match constructs
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus
+  when the 1st and 2nd arguments evaluate to a constructor and
+  when applied to 2 arguments 
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+minus : nat -> nat -> nat
+
+Argument scopes are [nat_scope nat_scope]
+The simpl tactic unfolds minus
+  when the 1st and 2nd arguments evaluate to a constructor 
+minus is transparent
+Expands to: Constant Coq.Init.Peano.minus
+pf :
+forall D1 C1 : Type,
+(D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
+
+Arguments D2, C2 are implicit
+Arguments D1, C1 are implicit and maximally inserted
+Argument scopes are [foo_scope type_scope _ _ _ _ _]
+The simpl tactic never unfolds pf
+pf is transparent
+Expands to: Constant Top.pf
+fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
+
+Arguments A, B, C are implicit and maximally inserted
+Argument scopes are [type_scope type_scope type_scope _ _ _]
+The simpl tactic unfolds fcomp when applied to 6 arguments 
+fcomp is transparent
+Expands to: Constant Top.fcomp
+volatile : nat -> nat
+
+Argument scope is [nat_scope]
+The simpl tactic always unfolds volatile
+volatile is transparent
+Expands to: Constant Top.volatile
+f : T1 -> T2 -> nat -> unit -> nat -> nat
+
+Argument scopes are [_ _ nat_scope _ nat_scope]
+f is transparent
+Expands to: Constant Top.S1.S2.f
+f : T1 -> T2 -> nat -> unit -> nat -> nat
+
+Argument scopes are [_ _ nat_scope _ nat_scope]
+The simpl tactic unfolds f
+  when the 3rd, 4th and 5th arguments evaluate to a constructor 
+f is transparent
+Expands to: Constant Top.S1.S2.f
+f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+
+Argument T2 is implicit
+Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
+The simpl tactic unfolds f
+  when the 4th, 5th and 6th arguments evaluate to a constructor 
+f is transparent
+Expands to: Constant Top.S1.f
+f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+
+Arguments T1, T2 are implicit
+Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
+The simpl tactic unfolds f
+  when the 5th, 6th and 7th arguments evaluate to a constructor 
+f is transparent
+Expands to: Constant Top.f
+f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
+
+The simpl tactic unfolds f
+  when the 5th, 6th and 7th arguments evaluate to a constructor 
+f is transparent
+Expands to: Constant Top.f