Modification of the Scheme command.

Now you can forget to provide the name of the scheme, it will be
built automatically depending of the sorts involved.

e.g. Scheme Induction for nat Sort Set.
will build nat_rec



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

6 files changed, 69 insertions, 13 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index af68c7cf91..fdaa2c5964 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1940,12 +1940,17 @@ let rec xlate_vernac =
    | VernacScheme [] -> xlate_error "induction scheme"
    | VernacScheme (lm :: lmi) ->
       let strip_ind = function
-      | ((_,id), InductionScheme (depstr, inde, sort)) ->
+      | (Some (_,id), InductionScheme (depstr, inde, sort)) ->
            CT_scheme_spec
             (xlate_ident id, xlate_dep depstr, 
 	    CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde),
 	     xlate_sort sort)
-      | ((_,id), EqualityScheme _) -> xlate_error "TODO: Scheme Equality" in
+      | (None, InductionScheme (depstr, inde, sort)) ->
+           CT_scheme_spec
+            (xlate_ident (id_of_string ""), xlate_dep depstr,
+            CT_coerce_ID_to_FORMULA (loc_qualid_to_ct_ID inde),
+             xlate_sort sort)
+      | (_, EqualityScheme _) -> xlate_error "TODO: Scheme Equality" in
         CT_ind_scheme
 	  (CT_scheme_spec_list (strip_ind lm, List.map strip_ind lmi))
    | VernacCombinedScheme _ -> xlate_error "TODO: Combined Scheme"
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index c61dfbf63d..b7cde536f7 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -285,7 +285,8 @@ GEXTEND Gram
   ;
   (* Inductive schemes *)
   scheme:
-    [ [ id = identref; ":="; kind = scheme_kind  -> (id,kind) ] ]
+    [ [ kind = scheme_kind -> (None,kind)
+      | id = identref; ":="; kind = scheme_kind -> (Some id,kind) ] ]
   ;
   scheme_kind:
     [ [ IDENT "Induction"; "for"; ind = global;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index d44e225b50..4bb7d27520 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -279,15 +279,21 @@ let pr_binders_arg =
 let pr_and_type_binders_arg bl =
   pr_binders_arg bl
 
-let pr_onescheme (id,schem) =
+let pr_onescheme (idop,schem) =
   match schem with 
   | InductionScheme (dep,ind,s) ->
-    hov 0 (pr_lident id ++ str" :=") ++ spc() ++
+    (match idop with
+      | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
+      | None -> spc ()
+    ) ++
     hov 0 ((if dep then str"Induction for" else str"Minimality for")
     ++ spc() ++ pr_reference ind) ++ spc() ++ 
     hov 0 (str"Sort" ++ spc() ++ pr_rawsort s)
   | EqualityScheme ind -> 
-    hov 0 (pr_lident id ++ str" :=") ++ spc() ++
+    (match idop with
+      | Some id -> hov 0 (pr_lident id ++ str" :=") ++ spc()
+      | None -> spc()
+    ) ++
     hov 0 (str"Equality for")
     ++ spc() ++ pr_reference ind
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d634957ca9..1b8c537b4b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -671,13 +671,54 @@ let build_corecursive l b =
   interp_recursive IsCoFixpoint fixl b
 
 (* 3d| Schemes *)
-let rec split_scheme = function
+let rec split_scheme l = 
+ let env = Global.env() in
+ match l with
   | [] -> [],[]
-  | (id,t)::q -> let l1,l2 = split_scheme q in 
+  | (Some id,t)::q -> let l1,l2 = split_scheme q in 
     ( match t with
       | InductionScheme (x,y,z) -> ((id,x,y,z)::l1),l2
-      | EqualityScheme  x -> l1,((id,x)::l2)
+      | EqualityScheme  x -> l1,(x::l2)
     )
+(*
+ if no name has been provided, we build one from the types of the ind
+requested 
+*)
+  | (None,t)::q ->
+       let l1,l2 = split_scheme q in
+    ( match t with
+      | InductionScheme (x,y,z) ->
+             let ind = mkInd (Nametab.global_inductive y) in
+             let sort_of_ind = family_of_sort (Typing.sort_of env Evd.empty ind)
+in
+             let z' = family_of_sort (interp_sort z) in
+             let suffix = (
+                match sort_of_ind with
+                | InProp ->
+                    if x then (match z' with
+                       | InProp -> "_ind_nodep"
+                       | InSet -> "_rec_nodep"
+                       | InType -> "_rect_nodep")
+                    else ( match z' with
+                       | InProp -> "_ind"
+                       | InSet -> "_rec"
+                       | InType -> "_rect" )
+                | _ ->
+                    if x then (match z' with
+                       | InProp -> "_ind"
+                       | InSet -> "_rec"
+                       | InType -> "_rect" )
+                    else (match z' with
+                       | InProp -> "_ind_nodep"
+                       | InSet  -> "_rec_nodep"
+                       | InType -> "_rect_nodep")
+                ) in
+            let newid = (string_of_id (Pcoq.coerce_global_to_id y))^suffix in
+            let newref = (dummy_loc,id_of_string newid) in
+          ((newref,x,y,z)::l1),l2
+      | EqualityScheme  x -> l1,(x::l2)
+    )
+
 
 let build_induction_scheme lnamedepindsort = 
   let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
@@ -707,13 +748,16 @@ let build_induction_scheme lnamedepindsort =
 
 let build_scheme l = 
   let ischeme,escheme = split_scheme l in
+(* we want 1 kind of scheme at a time so we check if the user
+tried to declare different schemes at once *)
     if (ischeme <> []) && (escheme <> []) 
     then
       error "Do not declare equality and induction scheme at the same time."
     else (
       if ischeme <> [] then build_induction_scheme ischeme;
-    List.iter ( fun (_,eq)-> let ind = Nametab.global_inductive eq
-(* vsiles :This will be replace with the boolean when it will be commited *)
+      List.iter ( fun indname ->
+        let ind = Nametab.global_inductive indname
+(* vsiles :This will be replace with the boolean eq when it will be commited *)
       in Pp.msgnl (print_constr (mkInd ind))
     ) escheme
   )
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 4bda8a362c..3f7e502850 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -52,7 +52,7 @@ val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit
 
 val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit
 
-val build_scheme : (identifier located * scheme ) list -> unit
+val build_scheme : (identifier located option * scheme ) list -> unit
 
 val build_combined_scheme : identifier located -> identifier located list -> unit
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index efdb710c2a..c1a8625bce 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -203,7 +203,7 @@ type vernac_expr =
   | VernacInductive of inductive_flag * (inductive_expr * decl_notation) list
   | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool
   | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool
-  | VernacScheme of (lident * scheme) list
+  | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
 
   (* Gallina extensions *)