Added support for definition of fixpoints using tactics.

Fixed some bugs in -beautify and robustness of {struct} clause.

Note: I tried to make the Automatic Introduction mode on by default
for version >= 8.3 but it is to complicated to adapt even in the
standard library.



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

3 files changed, 58 insertions, 88 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 669d1f2aec..393125e29e 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -10,6 +10,7 @@
 
 (* $Id$ *)
 
+open Pp
 open Pcoq
 open Constr
 open Prim
@@ -43,21 +44,11 @@ let binders_of_lidents l =
     LocalRawAssum ([loc, Name id], Default Rawterm.Explicit,
 		  CHole (loc, Some (Evd.BinderType (Name id))))) l
 
-let rec index_and_rec_order_of_annot loc bl ann =
-  match names_of_local_assums bl,ann with
-    | [loc,Name id], (None, r) -> Some (loc, id), r
-    | lids, (Some (loc, n), ro) ->
-        if List.exists (fun (_, x) -> x = Name n) lids then
-	  Some (loc, n), ro
-        else user_err_loc(loc,"index_of_annot", Pp.str"No such fix variable.")
-    | _, (None, r) -> None, r
-
 let mk_fixb (id,bl,ann,body,(loc,tyc)) =
-  let n,ro = index_and_rec_order_of_annot (fst id) bl ann in
   let ty = match tyc with
       Some ty -> ty
     | None -> CHole (loc, None) in
-  (id,(n,ro),bl,ty,body)
+  (id,ann,bl,ty,body)
 
 let mk_cofixb (id,bl,ann,body,(loc,tyc)) =
   let _ = Option.map (fun (aloc,_) ->
@@ -308,7 +299,8 @@ GEXTEND Gram
   ;
   fix_decl:
     [ [ id=identref; bl=binders_let_fixannot; ty=type_cstr; ":=";
-        c=operconstr LEVEL "200" -> (id,fst bl,snd bl,c,ty) ] ]
+        c=operconstr LEVEL "200" ->
+          (id,fst bl,snd bl,c,ty) ] ]
   ;
   match_constr:
     [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with";
@@ -402,8 +394,7 @@ GEXTEND Gram
     [ [ id=impl_ident; assum=binder_assum; bl = binders_let_fixannot ->
 	(assum (loc, Name id) :: fst bl), snd bl
     | f = fixannot -> [], f
-    | b = binder_let; bl = binders_let_fixannot ->
-	b @ fst bl, snd bl
+    | b = binder_let; bl = binders_let_fixannot -> b @ fst bl, snd bl
     | -> [], (None, CStructRec)
     ] ]
   ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 56946ef27c..54cf671ccb 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -129,8 +129,8 @@ GEXTEND Gram
     [ [ thm = thm_token; id = identref; bl = binders_let; ":"; c = lconstr;
         l = LIST0
           [ "with"; id = identref; bl = binders_let; ":"; c = lconstr ->
-            (Some id,(bl,c)) ] ->
-          VernacStartTheoremProof (thm,(Some id,(bl,c))::l, false, no_hook)
+            (Some id,(bl,c,None)) ] ->
+          VernacStartTheoremProof (thm,(Some id,(bl,c,None))::l, false, no_hook)
       | stre = assumption_token; nl = inline; bl = assum_list ->
 	  VernacAssumption (stre, nl, bl)
       | stre = assumptions_token; nl = inline; bl = assum_list ->
@@ -275,29 +275,12 @@ GEXTEND Gram
     [ [ id = identref;
 	bl = binders_let_fixannot;
         ty = type_cstr;
-	":="; def = lconstr; ntn = decl_notation ->
-	  let bl, annot = bl in
-          let names = names_of_local_assums bl in
-          let ni =
-            match fst annot with
-                Some (loc, id) ->
-                  (if List.exists (fun (_, id') -> Name id = id') names then
-		    Some (loc, id)
-		    else Util.user_err_loc
-                      (loc,"Fixpoint",
-                       str "No argument named " ++ Nameops.pr_id id ++ str"."))
-              | None ->
-		  (* If there is only one argument, it is the recursive one,
-		     otherwise, we search the recursive index later *)
-		  match names with
-		    | [(loc, Name na)] -> Some (loc, na)
-		    | _ -> None
-	  in
-	  ((id,(ni,snd annot),bl,ty,def),ntn) ] ]
+	def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
+	  let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ]
   ;
   corec_definition:
-    [ [ id = identref; bl = binders_let; ty = type_cstr; ":=";
-        def = lconstr; ntn = decl_notation ->
+    [ [ id = identref; bl = binders_let; ty = type_cstr; 
+        def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
           ((id,bl,ty,def),ntn) ] ]
   ;
   type_cstr:
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 1902711599..4f31607aa2 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -302,6 +302,28 @@ let pr_binders_arg =
 let pr_and_type_binders_arg bl =
   pr_binders_arg bl
 
+let names_of_binder = function
+  | LocalRawAssum (nal,_,_) -> nal
+  | LocalRawDef (_,_) -> []
+
+let pr_guard_annot bl (n,ro) =
+  match n with
+  | None -> mt ()
+  | Some (loc, id) ->
+      match (ro : Topconstr.recursion_order_expr) with
+      | CStructRec ->
+          let ids = List.flatten (List.map names_of_binder bl) in
+	  if List.length ids > 1 then
+	    spc() ++ str "{struct " ++ pr_id id ++ str"}"
+	  else mt()
+      | CWfRec c ->
+	  spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++
+	  pr_id id ++ str"}"
+      | CMeasureRec (m,r) ->
+	  spc() ++ str "{measure " ++ pr_lconstr_expr m ++ spc() ++
+	  pr_id id ++ (match r with None -> mt() | Some r -> str" on " ++
+	    pr_lconstr_expr r) ++ str"}"
+
 let pr_onescheme (idop,schem) =
   match schem with
   | InductionScheme (dep,ind,s) ->
@@ -409,6 +431,14 @@ let pr_paren_reln_or_extern = function
   | Some pprim,Prec p -> qs pprim ++ spc() ++ str":" ++ spc() ++ int p
   | _ -> mt()
 
+let pr_statement head (id,(bl,c,guard)) =
+  assert (id<>None);
+  hov 0
+    (head ++ pr_lident (Option.get id) ++ spc() ++
+    (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
+    pr_opt (pr_guard_annot bl) guard ++
+    str":" ++ pr_spc_lconstr c)
+
 (**************************************)
 (* Pretty printer for vernac commands *)
 (**************************************)
@@ -567,11 +597,6 @@ let rec pr_vernac = function
         | Some cc -> str" :=" ++ spc() ++ cc))
 
   | VernacStartTheoremProof (ki,l,_,_) ->
-      let pr_statement head (id,(bl,c)) =
-        hov 0
-          (head ++ pr_opt pr_lident id ++ spc() ++
-              (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
-              str":" ++ pr_spc_lconstr c) in
       hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++
              prlist (pr_statement (spc () ++ str "with")) (List.tl l))
 
@@ -605,75 +630,46 @@ let rec pr_vernac = function
 	    spc() ++
 	    pr_record_decl b c fs in
       let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
-	let kw =
-	  str (match k with Record -> "Record" | Structure -> "Structure"
-		 | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
-		 | Class b -> if b then "Definitional Class" else "Class")
-	in
-	  hov 0 (
-	    kw ++ spc() ++
-	      (if i then str"Infer" else str"") ++
-              (if coe then str" > " else str" ") ++ pr_lident id ++
+	hov 0 (
+	    str key ++ spc() ++
+	      (if i then str"Infer " else str"") ++
+              (if coe then str"> " else str"") ++ pr_lident id ++
               pr_and_type_binders_arg indpar ++ spc() ++
 	      Option.cata (fun s -> str":" ++ spc() ++ pr_lconstr_expr s) (mt()) s ++
 	      str" :=") ++ pr_constructor_list k lc ++
 	    prlist (pr_decl_notation pr_constr) ntn
       in
-      hov 1 (pr_oneind (if (Decl_kinds.recursivity_flag_of_kind f) then "Inductive" else "CoInductive") (List.hd l))
-      ++
+      let key =
+        let (_,_,_,k,_),_ = List.hd l in
+	match k with Record -> "Record" | Structure -> "Structure"
+	  | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+	  | Class b -> if b then "Definitional Class" else "Class" in
+      hov 1 (pr_oneind key (List.hd l)) ++
       (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
 
 
   | VernacFixpoint (recs,b) ->
-      let name_of_binder = function
-        | LocalRawAssum (nal,_,_) -> nal
-        | LocalRawDef (_,_) -> [] in
       let pr_onerec = function
-        | ((loc,id),(n,ro),bl,type_,def),ntn ->
-            let (bl',def,type_) =
-              if Flags.do_beautify() then extract_def_binders def type_
-              else ([],def,type_) in
-            let bl = bl @ bl' in
-            let ids = List.flatten (List.map name_of_binder bl) in
-            let annot =
-	      match n with
-		| None -> mt ()
-		| Some (loc, id) ->
-		    match (ro : Topconstr.recursion_order_expr) with
-			CStructRec ->
-			  if List.length ids > 1 then
-			    spc() ++ str "{struct " ++ pr_id id ++ str"}"
-			  else mt()
-		      | CWfRec c ->
-			  spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++
-			    pr_id id ++ str"}"
-		      | CMeasureRec (m,r) ->
-			  spc() ++ str "{measure " ++ pr_lconstr_expr m ++ spc() ++
-			    pr_id id ++ (match r with None -> mt() | Some r -> str" on " ++
-			    pr_lconstr_expr r) ++ str"}"
-	    in
+        | ((loc,id),ro,bl,type_,def),ntn ->
+            let annot = pr_guard_annot bl ro in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
-            ++ str" :=" ++ brk(1,1) ++ pr_lconstr def ++
+            ++ pr_opt (fun def -> str" :=" ++ brk(1,2) ++ pr_lconstr def) def ++
 	    prlist (pr_decl_notation pr_constr) ntn
       in
       let start = if b then "Boxed Fixpoint" else "Fixpoint" in
-      hov 1 (str start ++ spc() ++
-        prlist_with_sep (fun _ -> fnl() ++ fnl() ++ str"with ") pr_onerec recs)
+      hov 0 (str start ++ spc() ++
+        prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onerec recs)
 
   | VernacCoFixpoint (corecs,b) ->
       let pr_onecorec (((loc,id),bl,c,def),ntn) =
-        let (bl',def,c) =
-              if Flags.do_beautify() then extract_def_binders def c
-              else ([],def,c) in
-        let bl = bl @ bl' in
         pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
         spc() ++ pr_lconstr_expr c ++
-        str" :=" ++ brk(1,1) ++ pr_lconstr def  ++
+        pr_opt (fun def -> str" :=" ++ brk(1,2) ++ pr_lconstr def) def ++
 	prlist (pr_decl_notation pr_constr) ntn
       in
       let start = if b then "Boxed CoFixpoint" else "CoFixpoint" in
-      hov 1 (str start ++ spc() ++
+      hov 0 (str start ++ spc() ++
       prlist_with_sep (fun _ -> fnl() ++ str"with ") pr_onecorec corecs)
   | VernacScheme l ->
       hov 2 (str"Scheme" ++ spc() ++