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

3 files changed, 134 insertions, 7 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 78e01afd9..422da8544 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -581,10 +581,59 @@ GEXTEND Gram
 
       | IDENT "Existing"; IDENT "Class"; is = global -> VernacDeclareClass is
 
+      (* Arguments *)
+      | IDENT "Arguments"; qid = smart_global; 
+        impl = LIST1 [ l = LIST0
+        [ item = argument_spec ->
+            let id, r, s = item in [`Id (id,r,s,false,false)]
+        | "/" -> [`Slash]
+        | "("; items = LIST1 argument_spec; ")"; sc = OPT scope ->
+            let f x = match sc, x with
+            | None, x -> x | x, None -> Option.map (fun y -> loc, y) x
+            | Some _, Some _ -> error "scope declared twice" in
+            List.map (fun (id,r,s) -> `Id(id,r,f s,false,false)) items
+        | "["; items = LIST1 argument_spec; "]"; sc = OPT scope ->
+            let f x = match sc, x with
+            | None, x -> x | x, None -> Option.map (fun y -> loc, y) x
+            | Some _, Some _ -> error "scope declared twice" in
+            List.map (fun (id,r,s) -> `Id(id,r,f s,true,false)) items
+        | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope ->
+            let f x = match sc, x with
+            | None, x -> x | x, None -> Option.map (fun y -> loc, y) x
+            | Some _, Some _ -> error "scope declared twice" in
+            List.map (fun (id,r,s) -> `Id(id,r,f s,true,true)) items
+        ] -> l ] SEP ",";
+        mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> l ] ->
+         let mods = match mods with None -> [] | Some l -> List.flatten l in
+         let impl = List.map List.flatten impl in
+         let rec aux n (narg, impl) = function
+           | `Id x :: tl -> aux (n+1) (narg, impl@[x]) tl
+           | `Slash :: tl -> aux (n+1) (n, impl) tl
+           | [] -> narg, impl in
+         let nargs, impl = List.split (List.map (aux 0 (-1, [])) impl) in
+         let nargs, rest = List.hd nargs, List.tl nargs in
+         if List.exists ((<>) nargs) rest then
+           error "All arguments lists must have the same length";
+         let err_incompat x y =
+           error ("Options \""^x^"\" and \""^y^"\" are incompatible") in
+         if nargs > 0 && List.mem `SimplNeverUnfold mods then
+           err_incompat "simpl never" "/";
+         if List.mem `SimplNeverUnfold mods &&
+            List.mem `SimplDontExposeCase mods then
+           err_incompat "simpl never" "simpl nomatch";
+         VernacArguments (use_section_locality(), qid, impl, nargs, mods)
+
+     (* moved there so that camlp5 factors it with the previous rule *)
+     | IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
+       "["; scl = LIST0 [ "_" -> None | sc = IDENT -> Some sc ]; "]" ->
+         warning "Arguments Scope is deprecated; use Arguments instead";
+	 VernacArgumentsScope (use_section_locality (),qid,scl)
+
       (* Implicit *)
       | IDENT "Implicit"; IDENT "Arguments"; qid = smart_global;
 	   pos = LIST0 [ "["; l = LIST0 implicit_name; "]" ->
 	     List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] ->
+	   warning "Implicit Arguments is deprecated; use Arguments instead";
 	   VernacDeclareImplicits (use_section_locality (),qid,pos)
 
       | IDENT "Implicit"; "Type"; bl = reserv_list ->
@@ -601,12 +650,32 @@ GEXTEND Gram
 		  idl = LIST1 identref -> Some idl ] ->
 	     VernacGeneralizable (use_non_locality (), gen) ] ]
   ;
+  arguments_modifier:
+    [ [ IDENT "simpl"; IDENT "nomatch" -> [`SimplDontExposeCase]
+      | IDENT "simpl"; IDENT "never" -> [`SimplNeverUnfold]
+      | IDENT "default"; IDENT "implicits" -> [`DefaultImplicits]
+      | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits]
+      | IDENT "clear"; IDENT "scopes" -> [`ClearScopes]
+      | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" ->
+          [`ClearImplicits; `ClearScopes]
+      | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" ->
+          [`ClearImplicits; `ClearScopes]
+      ] ]
+  ;
   implicit_name:
     [ [ "!"; id = ident -> (id, false, true)
     | id = ident -> (id,false,false)
     | "["; "!"; id = ident; "]" -> (id,true,true)
     | "["; id = ident; "]" -> (id,true, false) ] ]
   ;
+  scope:
+    [ [ "%"; key = IDENT -> key ] ]
+  ;
+  argument_spec: [
+       [ b = OPT "!"; id = name ; s = OPT scope ->
+       snd id, b <> None, Option.map (fun x -> loc, x) s
+    ]
+  ];
   strategy_level:
     [ [ IDENT "expand" -> Conv_oracle.Expand
       | IDENT "opaque" -> Conv_oracle.Opaque
@@ -901,10 +970,6 @@ GEXTEND Gram
      | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with";
        refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl)
 
-     | IDENT "Arguments"; IDENT "Scope"; qid = smart_global;
-       "["; scl = LIST0 opt_scope; "]" ->
-	 VernacArgumentsScope (use_section_locality (),qid,scl)
-
      | IDENT "Infix"; local = obsolete_locality;
 	 op = ne_lstring; ":="; p = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
@@ -970,9 +1035,6 @@ GEXTEND Gram
       | IDENT "closed"; IDENT "binder" -> ETBinder false
     ] ]
   ;
-  opt_scope:
-    [ [ "_" -> None | sc = IDENT -> Some sc ] ]
-  ;
   production_item:
     [ [ s = ne_string -> TacTerm s
       | nt = IDENT;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 6254d345f..4e73b3793 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -835,6 +835,31 @@ let rec pr_vernac = function
 	prlist_with_sep spc (fun imps ->
 	  str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
 	  impls)
+  | VernacArguments (local, q, impl, nargs, mods) ->
+      hov 2 (pr_section_locality local ++ str"Arguments" ++ spc() ++
+        pr_smart_global q ++
+      let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in
+      let pr_if b x = if b then x else str "" in
+      let pr_br imp max x = match imp, max with
+        | true, false -> str "[" ++ x ++ str "]"
+        | true, true -> str "{" ++ x ++ str "}"
+        | _ -> x in
+      let rec aux n l =
+        match n, l with
+        | 0, l -> spc () ++ str"/" ++ aux ~-1 l
+        | _, [] -> mt()
+        | n, (id,k,s,imp,max) :: tl ->
+            spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
+            aux (n-1) tl in
+      prlist_with_sep (fun () -> str", ") (aux nargs) impl ++
+      if mods <> [] then str" : " else str"" ++
+      prlist_with_sep (fun () -> str", " ++ spc()) (function
+        | `SimplDontExposeCase -> str "simpl nomatch"
+        | `SimplNeverUnfold -> str "simpl never"
+        | `DefaultImplicits -> str "default implicits"
+        | `ClearImplicits -> str "clear implicits"
+        | `ClearScopes -> str "clear scopes")
+        mods)
   | VernacReserve bl ->
       let n = List.length (List.flatten (List.map fst bl)) in
       hov 2 (str"Implicit Type" ++
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 06d148ec6..741f9201e 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -151,6 +151,45 @@ let print_argument_scopes prefix = function
       str "]")]
   | _  -> []
 
+(*****************************)
+(** Printing simpl behaviour *)
+
+let print_simpl_behaviour ref =
+  match Tacred.get_simpl_behaviour ref with
+  | None -> []
+  | Some (recargs, nargs, flags) ->
+     let never = List.mem `SimplNeverUnfold flags in
+     let nomatch = List.mem `SimplDontExposeCase flags in
+     let pp_nomatch = spc() ++ if nomatch then
+       str "avoiding to expose match constructs" else str"" in
+     let pp_recargs = spc() ++ str "when the " ++
+       let rec aux = function
+         | [] -> mt()
+         | [x] -> str (ordinal (x+1))
+         | [x;y] -> str (ordinal (x+1)) ++ str " and " ++ str (ordinal (y+1))
+         | x::tl -> str (ordinal (x+1)) ++ str ", " ++ aux tl in
+       aux recargs ++ str (plural (List.length recargs) " argument") ++
+       str (plural (if List.length recargs >= 2 then 1 else 2) " evaluate") ++
+       str " to a constructor" in
+     let pp_nargs =
+       spc() ++ str "when applied to " ++ int nargs ++
+       str (plural nargs " argument") in
+     [hov 2 (str "The simpl tactic " ++
+     match recargs, nargs, never with
+     | _,_, true -> str "never unfolds " ++ pr_global ref
+     | [], 0, _ -> str "always unfolds " ++ pr_global ref
+     | _::_, n, _ when n < 0 ->
+        str "unfolds " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
+     | _::_, n, _ when n > List.fold_left max 0 recargs ->
+        str "unfolds " ++ pr_global ref ++ pp_recargs ++
+        str " and" ++ pp_nargs ++ pp_nomatch
+     | _::_, _, _ ->
+        str "unfolds " ++ pr_global ref ++ pp_recargs ++ pp_nomatch
+     | [], n, _ when n > 0 ->
+        str "unfolds " ++ pr_global ref ++ pp_nargs ++ pp_nomatch
+     | _ -> str "unfolds " ++ pr_global ref ++ pp_nomatch )]
+;;
+
 (*********************)
 (** Printing Opacity *)
 
@@ -625,6 +664,7 @@ let print_about_any k =
       pr_infos_list
        ([print_ref false ref; blankline] @
 	print_name_infos ref @
+	print_simpl_behaviour ref @
 	print_opacity ref @
 	[hov 0 (str "Expands to: " ++ pr_located_qualid k)])
   | Syntactic kn ->