Modification of VernacScheme to handle a new scheme: Equality (equality in

boolean, will be added later) and update so everything is fine with the new
syntax. 

New Type:

type scheme =
  | InductionScheme of bool * lreference * sort_expr
  | EqualityScheme of lreference
...
  | VernacScheme of (lident * scheme) list



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

6 files changed, 51 insertions, 18 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 2abdcaa19c..c16b5215ac 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1934,11 +1934,13 @@ let rec xlate_vernac =
 	  (CT_cofix_rec_list (strip_mutcorec lm, List.map strip_mutcorec lmi))
    | VernacScheme [] -> xlate_error "induction scheme"
    | VernacScheme (lm :: lmi) ->
-      let strip_ind ((_,id), depstr, inde, sort) =
+      let strip_ind = function
+      | ((_,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) in
+	     xlate_sort sort)
+      | ((_,id), 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 73e366c931..94e39621e9 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -280,13 +280,14 @@ GEXTEND Gram
   ;
   (* Inductive schemes *)
   scheme:
-    [ [ id = identref; ":="; dep = dep_scheme; "for"; ind = global;
-        IDENT "Sort"; s = sort ->
-          (id,dep,ind,s) ] ]
-  ;
-  dep_scheme:
-    [ [ IDENT "Induction" -> true
-      | IDENT "Minimality" -> false ] ]
+    [ [ id = identref; ":="; kind = scheme_kind  -> (id,kind) ] ]
+  ;
+  scheme_kind:
+    [ [ IDENT "Induction"; "for"; ind = global;
+          IDENT "Sort"; s = sort-> InductionScheme(true,ind,s)
+      | IDENT "Minimality"; "for"; ind = global;
+          IDENT "Sort"; s = sort-> InductionScheme(false,ind,s)
+      | IDENT "Equality"; "for" ; ind = global -> EqualityScheme(ind)  ] ]
   ;
   (* Various Binders *)
 (*
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 62af97b439..f12f730610 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -279,11 +279,17 @@ let pr_binders_arg =
 let pr_and_type_binders_arg bl =
   pr_binders_arg bl
 
-let pr_onescheme (id,dep,ind,s) =
-  hov 0 (pr_lident id ++ str" :=") ++ 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)
+let pr_onescheme (id,schem) =
+  match schem with 
+  | InductionScheme (dep,ind,s) ->
+    hov 0 (pr_lident id ++ str" :=") ++ 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() ++
+    hov 0 (str"Equality for")
+    ++ spc() ++ pr_reference ind
 
 let begin_of_inductive = function
     [] -> 0
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 6fd56536b9..6c4fe20571 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -648,8 +648,15 @@ let build_corecursive l b =
   interp_recursive IsCoFixpoint fixl b
 
 (* 3d| Schemes *)
-
-let build_scheme lnamedepindsort = 
+let rec split_scheme = function
+  | [] -> [],[]
+  | (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)
+    )
+
+let build_induction_scheme lnamedepindsort = 
   let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
   and sigma = Evd.empty
   and env0 = Global.env() in
@@ -675,6 +682,19 @@ let build_scheme lnamedepindsort =
   let _ = List.fold_right2 declare listdecl lrecnames [] in
   if_verbose ppnl (recursive_message Fixpoint lrecnames)
 
+let build_scheme l = 
+  let ischeme,escheme = split_scheme l in
+    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 *)
+      in Pp.msgnl (print_constr (mkInd ind))
+    ) escheme
+  )
+
 let rec get_concl n t = 
   if n = 0 then t
   else
diff --git a/toplevel/command.mli b/toplevel/command.mli
index cf05f691bf..4bda8a362c 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 * bool * reference * rawsort) list -> unit
+val build_scheme : (identifier located * scheme ) list -> unit
 
 val build_combined_scheme : identifier located -> identifier located list -> unit
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 9714ffd6c9..efdb710c2a 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -168,6 +168,10 @@ type proof_end =
   | Admitted
   | Proved of opacity_flag * (lident * theorem_kind option) option
 
+type scheme =
+  | InductionScheme of bool * lreference * sort_expr
+  | EqualityScheme of lreference
+
 type vernac_expr =
   (* Control *)
   | VernacList of located_vernac_expr list
@@ -199,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 * bool * lreference * sort_expr) list
+  | VernacScheme of (lident * scheme) list
   | VernacCombinedScheme of lident * lident list
 
   (* Gallina extensions *)