Addition of a "Combined Scheme" vernacular command for building the conjunction of mutual inductions principles.

e.g: Combined Scheme mutind from tree_ind, forest_ind gives a conclusion (forall t : tree, P t) /\ (forall f : forest, P0 f).


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

4 files changed, 58 insertions, 0 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index ff5b3bd3b..756ae31b6 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -656,6 +656,58 @@ let build_scheme lnamedepindsort =
   let _ = List.fold_right2 declare listdecl lrecnames [] in
   if_verbose ppnl (recursive_message Fixpoint lrecnames)
 
+let rec get_concl n t = 
+  if n = 0 then t
+  else
+    match kind_of_term t with
+	Prod (_,_,t) -> get_concl (pred n) t
+      | _ -> raise (Invalid_argument "get_concl")
+
+let cut_last l = 
+  let rec aux acc = function
+      hd :: [] -> List.rev acc, hd
+    | hd :: tl -> aux (hd :: acc) tl
+    | [] -> raise (Invalid_argument "cut_last")
+  in aux [] l
+	
+let build_combined_scheme name schemes =
+  let env = Global.env () in
+  let defs = 
+    List.map (fun x -> 
+		let refe = Ident x in
+		let qualid = qualid_of_reference refe in
+		let cst = Nametab.locate_constant (snd qualid) in
+		  qualid, cst, Typeops.type_of_constant env cst)
+      schemes
+  in
+  let (qid, c, t) = List.hd defs in
+  let nargs = 
+    let (_, arity, _) = destProd t in
+      nb_prod arity
+  in
+  let prods = nb_prod t - nargs in
+  let defs, (qid, c, t) = cut_last defs in
+  let (args, concl) = decompose_prod_n prods t in
+  let concls = List.map (fun (_, cst, t) -> cst, get_concl prods t) defs in
+  let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in
+  let relargs = rel_vect 0 prods in
+  let concl_typ, concl_bod = 
+    List.fold_right
+      (fun (cst, x) (acct, accb) -> 
+	 mkApp (coqand, [| x; acct |]),
+	 mkApp (coqconj, [| x; acct; mkApp(mkConst cst, relargs); accb |])) 
+      concls (concl, mkApp (mkConst c, relargs))
+  in
+  let ctx = List.map (fun (x, y) -> x, None, y) args in
+  let typ = it_mkProd_wo_LetIn concl_typ ctx in
+  let body = it_mkLambda_or_LetIn concl_bod ctx in
+  let ce = { const_entry_body = body;
+             const_entry_type = Some typ;
+             const_entry_opaque = false;
+	     const_entry_boxed = Options.boxed_definitions() } in
+  let _ = declare_constant (snd name) (DefinitionEntry ce, IsDefinition Scheme) in
+    if_verbose ppnl (recursive_message Fixpoint [snd name])
+
 (* 4| Goal declaration *)
 
 let start_proof id kind c hook =
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 7c3d51946..c4ef92447 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -50,6 +50,8 @@ val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit
 
 val build_scheme : (identifier located * bool * reference * rawsort) list -> unit
 
+val build_combined_scheme : identifier located -> identifier located list -> unit
+
 val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr
 
 val start_proof : identifier -> goal_kind -> constr ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index db30d7b95..44e7cbad7 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -359,6 +359,8 @@ let vernac_cofixpoint = build_corecursive
 
 let vernac_scheme = build_scheme
 
+let vernac_combined_scheme = build_combined_scheme
+
 (**********************)
 (* Modules            *)
 
@@ -1135,6 +1137,7 @@ let interp c = match c with
   | VernacFixpoint (l,b) -> vernac_fixpoint l b
   | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b
   | VernacScheme l -> vernac_scheme l
+  | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
 
   (* Modules *)
   | VernacDeclareModule (export,(_,id),bl,mtyo) -> 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index a87221c75..ffde10192 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -199,6 +199,7 @@ type vernac_expr =
   | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool
   | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool
   | VernacScheme of (lident * bool * lreference * sort_expr) list
+  | VernacCombinedScheme of lident * lident list
 
   (* Gallina extensions *)
   | VernacRecord of bool (* = Record or Structure *)