- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses

- New tactic "pose proof" that generalizes "assert (id:=p)" with intro patterns
- TacTrueCut and TacForward merged into new TacAssert bound to Tactics.forward


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

3 files changed, 81 insertions, 41 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index f27191e2ec..f7c05c7786 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -68,6 +68,24 @@ let lpar_id_colon =
               | _ -> raise Stream.Failure)
         | _ -> raise Stream.Failure)
 
+let guess_lpar_ipat s strm =
+  match Stream.npeek 1 strm with
+    | [("","(")] ->
+        (match Stream.npeek 2 strm with
+          | [_; ("",("("|"["))] -> ()
+          | [_; ("IDENT",_)] ->
+              (match Stream.npeek 3 strm with
+                | [_; _; ("", s')] when s = s' -> ()
+                | _ -> raise Stream.Failure)
+          | _ -> raise Stream.Failure)
+    | _ -> raise Stream.Failure
+
+let guess_lpar_coloneq =
+  Gram.Entry.of_parser "guess_lpar_coloneq" (guess_lpar_ipat ":=")
+
+let guess_lpar_colon =
+  Gram.Entry.of_parser "guess_lpar_colon" (guess_lpar_ipat ":")
+
 open Constr
 open Prim
 open Tactic
@@ -261,6 +279,9 @@ GEXTEND Gram
   with_names:
     [ [ "as"; ipat = simple_intropattern -> Some ipat | -> None ] ]
   ;
+  by_tactic:
+    [ [ "by"; tac = tactic -> tac | -> TacId "" ] ]
+  ;
   simple_tactic:
     [ [ 
       (* Basic tactics *)
@@ -293,22 +314,30 @@ GEXTEND Gram
       | "cofix"; id = ident; "with"; fd = LIST1 fixdecl ->
 	  TacMutualCofix (id,List.map mk_cofix_tac fd)
 
-      | IDENT "cut"; c = constr -> TacCut c
-      | IDENT "assert"; id = lpar_id_colon; t = lconstr; ")" ->
-          TacTrueCut (Names.Name id,t)
-      | IDENT "assert"; id = lpar_id_coloneq; b = lconstr; ")" ->
-          TacForward (false,Names.Name id,b)
-      | IDENT "assert"; c = constr -> TacTrueCut (Names.Anonymous,c)
       | IDENT "pose"; id = lpar_id_coloneq; b = lconstr; ")" ->
-	  TacForward (true,Names.Name id,b)
-      | IDENT "pose"; b = constr -> TacForward (true,Names.Anonymous,b)
-      | IDENT "generalize"; lc = LIST1 constr -> TacGeneralize lc
-      | IDENT "generalize"; IDENT "dependent"; c = constr ->
-          TacGeneralizeDep c
-      | IDENT "set"; id = lpar_id_coloneq; c = lconstr; ")";
-          p = clause -> TacLetTac (Names.Name id,c,p)
+	  TacLetTac (Names.Name id,b,nowhere)
+      | IDENT "pose"; b = constr ->
+	  TacLetTac (Names.Anonymous,b,nowhere)
+      | IDENT "set"; id = lpar_id_coloneq; c = lconstr; ")"; p = clause ->
+	  TacLetTac (Names.Name id,c,p)
       | IDENT "set"; c = constr; p = clause ->
           TacLetTac (Names.Anonymous,c,p)
+
+      (* Begin compatibility *)
+      | IDENT "assert"; id = lpar_id_coloneq; c = lconstr; ")" -> 
+	  TacAssert (None,Some (IntroIdentifier id),c)
+      | IDENT "assert"; id = lpar_id_colon; c = lconstr; ")"; tac=by_tactic -> 
+	  TacAssert (Some tac,Some (IntroIdentifier id),c)
+      (* End compatibility *)
+
+      | IDENT "assert"; c = constr; ipat = with_names; tac = by_tactic ->
+	  TacAssert (Some tac,ipat,c)
+      | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = with_names ->
+	  TacAssert (None,ipat,c)
+
+      | IDENT "cut"; c = constr -> TacCut c
+      | IDENT "generalize"; lc = LIST1 constr -> TacGeneralize lc
+      | IDENT "generalize"; IDENT "dependent"; c = constr -> TacGeneralizeDep c
     (*  | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")"; "in";
 	  hid = hypident ->
 	    let (id,(hloc,_)) = hid in
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 46caf88b82..c1eef07dcb 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -366,6 +366,30 @@ let pr_with_names = function
   | None -> mt ()
   | Some ipat -> spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
 
+let pr_pose prlc prc na c = match na with
+  | Anonymous -> spc() ++ prc c
+  | Name id -> spc() ++ surround (pr_id id ++ str " :=" ++ spc() ++ prlc c)
+
+let pr_assertion _prlc prc ipat c = match ipat with
+(* Use this "optimisation" or use only the general case ?
+  | Some (IntroIdentifier id) ->
+      spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
+*)
+  | ipat ->
+      spc() ++ prc c ++ pr_with_names ipat
+
+let pr_assumption prlc prc ipat c = match ipat with
+(* Use this "optimisation" or use only the general case ?
+  | Some (IntroIdentifier id) ->
+      spc() ++ surround (pr_intro_pattern ipat ++ str " :" ++ spc() ++ prlc c)
+*)
+  | ipat ->
+      spc() ++ prc c ++ pr_with_names ipat
+
+let pr_by_tactic prt = function
+  | TacId "" -> mt ()
+  | tac -> spc() ++ str "by " ++ prt tac
+
 let pr_occs pp = function
     [] -> pp
   | nl -> hov 1 (pp ++ spc() ++ str"at " ++
@@ -577,7 +601,6 @@ let pr_fix_tac env (id,n,c) =
 let pr_cofix_tac env (id,c) =
   hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg env c ++ str")") in
 
-
   (* Printing tactics as arguments *)
 let rec pr_atom0 env = function
   | TacIntroPattern [] -> str "intros"
@@ -632,34 +655,23 @@ and pr_atom1 env = function
       hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
              str"with " ++ prlist_with_sep spc (pr_cofix_tac env) l)
   | TacCut c -> hov 1 (str "cut" ++ pr_constrarg env c)
-  | TacTrueCut (Anonymous,c) -> 
-      hov 1 (str "assert" ++ pr_constrarg env c)
-  | TacTrueCut (Name id,c) -> 
-      hov 1 (str "assert" ++ spc () ++
-             hov 1 (str"(" ++ pr_id id ++ str " :" ++
-                    pr_lconstrarg env c ++ str")"))
-  | TacForward (false,na,c) ->
-      hov 1 (str "assert" ++ spc () ++
-             hov 1 (str"(" ++ pr_name na ++ str " :=" ++
-                    pr_lconstrarg env c ++ str")"))
-  | TacForward (true,Anonymous,c) ->
-      hov 1 (str "pose" ++ pr_constrarg env c)
-  | TacForward (true,Name id,c) ->
-      hov 1 (str "pose" ++ spc() ++
-             hov 1 (str"(" ++ pr_id id ++ str " :=" ++
-                    pr_lconstrarg env c ++ str")"))
+  | TacAssert (Some tac,ipat,c) -> 
+      hov 1 (str "assert" ++ 
+             pr_assumption (pr_lconstr env) (pr_constr env) ipat c ++ 
+             pr_by_tactic (pr_tac_level env ltop) tac)
+  | TacAssert (None,ipat,c) -> 
+      hov 1 (str "pose proof" ++
+             pr_assertion (pr_lconstr env) (pr_constr env) ipat c)
   | TacGeneralize l ->
       hov 1 (str "generalize" ++ spc () ++
              prlist_with_sep spc (pr_constr env) l)
   | TacGeneralizeDep c ->
       hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
              pr_constrarg env c)
-  | TacLetTac (Anonymous,c,cl) ->
-      hov 1 (str "set" ++ pr_constrarg env c) ++ pr_clauses pr_ident cl
-  | TacLetTac (Name id,c,cl) ->
-      hov 1 (str "set" ++ spc () ++
-             hov 1 (str"(" ++ pr_id id ++ str " :=" ++
-                    pr_lconstrarg env c ++ str")") ++
+  | TacLetTac (na,c,cl) when cl = nowhere ->
+      hov 1 (str "pose" ++ pr_pose (pr_lconstr env) (pr_constr env) na c)
+  | TacLetTac (na,c,cl) ->
+      hov 1 (str "set" ++ pr_pose (pr_lconstr env) (pr_constr env) na c ++
              pr_clauses pr_ident cl)
 (*  | TacInstantiate (n,c,ConclLocation ()) ->
       hov 1 (str "instantiate" ++ spc() ++
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index f8172ac6e1..659f64c7b6 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -297,11 +297,10 @@ let rec mlexpr_of_atomic_tactic = function
 
   | Tacexpr.TacCut c ->
       <:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
-  | Tacexpr.TacTrueCut (na,c) ->
-      let na = mlexpr_of_name na in
-      <:expr< Tacexpr.TacTrueCut $na$ $mlexpr_of_constr c$ >>
-  | Tacexpr.TacForward (b,na,c) ->
-      <:expr< Tacexpr.TacForward $mlexpr_of_bool b$ $mlexpr_of_name na$ $mlexpr_of_constr c$ >>
+  | Tacexpr.TacAssert (t,ipat,c) ->
+      let ipat = mlexpr_of_option mlexpr_of_intro_pattern ipat in
+      <:expr< Tacexpr.TacAssert $mlexpr_of_option mlexpr_of_tactic t$ $ipat$ 
+	      $mlexpr_of_constr c$ >>
   | Tacexpr.TacGeneralize cl ->
       <:expr< Tacexpr.TacGeneralize $mlexpr_of_list mlexpr_of_constr cl$ >>
   | Tacexpr.TacGeneralizeDep c ->