Added a function to rebuild an elim scheme from elim_scheme_info. Will

use it for elim principle type generation from merged graphs.


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

3 files changed, 83 insertions, 2 deletions

diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index adec67e36f..ec456aae6f 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -9,7 +9,8 @@
 (* Merging of induction principles. *)
 
 (*i $Id: i*)
-
+open Libnames
+open Tactics
 open Indfun_common
 open Util
 open Topconstr
@@ -17,6 +18,7 @@ open Vernacexpr
 open Pp
 open Names
 open Term
+open Termops 
 open Declarations
 open Environ
 open Rawterm
@@ -26,6 +28,8 @@ open Rawtermops
 
 (** {2 Useful operations on constr and rawconstr} *)
 
+let rec popn i c = if i<=0 then c else pop (popn (i-1) c)
+
 (** Substitutions in constr *)
 let compare_constr_nosub t1 t2 =
   if compare_constr (fun _ _ -> false) t1 t2 
@@ -949,8 +953,67 @@ let merge (id1:identifier) (id2:identifier) (args1:identifier array)
   merge_inductive finfo1.graph_ind finfo2.graph_ind lnk1 lnk2 id
 
 
+let remove_last_arg c =
+  let (x,y) = decompose_prod c in
+  let xnolast = List.rev (List.tl (List.rev x)) in
+  compose_prod xnolast y
+
+let rec remove_n_fst_list n l = if n=0 then l else remove_n_fst_list (n-1) (List.tl l)
+let remove_n_last_list n l = List.rev (remove_n_fst_list n (List.rev l))
+
+let remove_last_n_arg n c =
+  let (x,y) = decompose_prod c in
+  let xnolast = remove_n_last_list n x in
+  compose_prod xnolast y
+
+(* [funify_branches relinfo nfuns branch] returns the branch [branch]
+   of the relinfo [relinfo] modified to fit in a functional principle.
+   Things to do: 
+    - remove indargs from rel applications
+    - replace *variables only* corresponding to function (recursive)
+      results by the actual function application. *)
+let funify_branches relinfo nfuns branch = 
+  let mut_induct, induct = 
+    match relinfo.indref with
+      | None -> assert false
+      | Some (IndRef ((mutual_ind,i) as ind)) -> mutual_ind,ind
+      | _ -> assert false in
+  let is_dom c =
+    match kind_of_term c with
+      | Ind((u,_)) | Construct((u,_),_) -> u = mut_induct
+      | _ -> false in
+  let _dom_i c =
+    assert (is_dom c);
+    match kind_of_term c with
+      | Ind((u,i)) | Construct((u,_),i) -> i
+      | _ -> assert false in
+  let _is_pred c shift = 
+    match kind_of_term c with
+      | Rel i -> let reali = i-shift in (reali>=0 && reali<relinfo.nbranches)
+      | _ -> false in
+  (* FIXME: *)
+  (Anonymous,Some mkProp,mkProp)
+  
 
-
+let relprinctype_to_funprinctype relprinctype nfuns =
+  let relinfo = compute_elim_sig relprinctype in
+  assert (not relinfo.farg_in_concl);
+  assert (relinfo.indarg_in_concl);
+  (* first remove indarg and indarg_in_concl *)
+  let relinfo_noindarg = { relinfo with
+    indarg_in_concl = false; indarg = None;
+    concl = remove_last_arg (pop relinfo.concl); } in
+  (* the nfuns last induction arguments are functional ones: remove them *)
+  let relinfo_argsok = { relinfo_noindarg with
+    nargs = relinfo_noindarg.nargs - nfuns;
+    (* args is in reverse order, so remove fst *)
+    args = remove_n_fst_list nfuns relinfo_noindarg.args;
+    concl = popn nfuns relinfo_noindarg.concl
+  } in
+  let new_branches = 
+    List.map (funify_branches relinfo_argsok nfuns) relinfo_argsok.branches in
+  let relinfo_branches = { relinfo_argsok with branches = new_branches } in
+  relinfo_branches
 
 (* @article{ bundy93rippling,
     author = "Alan Bundy and Andrew Stevens and Frank van Harmelen and Andrew Ireland and Alan Smaill",
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b021f5e469..e8192c177e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1909,6 +1909,23 @@ let exchange_hd_app subst_hd t =
   let hd,args= decompose_app t in mkApp (subst_hd,Array.of_list args)
 
 
+
+(* [rebuild_elimtype_from_scheme scheme] rebuilds the type of an
+   eliminator from its [scheme_info]. The idea is to build variants of
+   eliminator by modifying there scheme_info, then rebuild the
+   eliminator type, then prove it (with tactics). *)
+let rebuild_elimtype_from_scheme (scheme:elim_scheme): types =
+  let hiconcl = 
+    match scheme.indarg with
+      | None -> scheme.concl
+      | Some x -> mkProd_or_LetIn x scheme.concl in
+  let xihiconcl = it_mkProd_or_LetIn hiconcl scheme.args in
+  let brconcl = it_mkProd_or_LetIn xihiconcl scheme.branches in
+  let predconcl = it_mkProd_or_LetIn brconcl scheme.predicates in
+  let paramconcl = it_mkProd_or_LetIn predconcl scheme.params in
+  paramconcl
+
+
 exception NoLastArg
 exception NoLastArgCcl
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 3a3bf6de51..c723c2b9a3 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -232,6 +232,7 @@ type elim_scheme = {
 
 
 val compute_elim_sig : ?elimc: constr with_ebindings -> types -> elim_scheme
+val rebuild_elimtype_from_scheme: elim_scheme -> types
 
 val general_elim  : evars_flag ->
   constr with_ebindings -> constr with_ebindings -> ?allow_K:bool -> tactic