Detection des paramettres pour les Functions bien fondees

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

4 files changed, 161 insertions, 23 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 0bcf19dc6..ab411cf11 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -1379,7 +1379,7 @@ let is_valid_hypothesis predicates_name =
 	| _ -> false 
   in
   is_valid_hypothesis 
-
+(*
 let fresh_id avoid na = 
   let id =  
     match na with 
@@ -1591,13 +1591,160 @@ let prove_principle_for_gen
 	 arg_tac;
 	 start_tac
 	] g
+*)
 
-
-
-
-
-
-
+let prove_principle_for_gen
+    (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes
+    rec_arg_num rec_arg_type relation gl = 
+  let princ_type = pf_concl gl in 
+  let princ_info = compute_elim_sig princ_type in 
+  let fresh_id = 
+    let avoid = ref (pf_ids_of_hyps gl) in 
+    fun na -> 
+      let new_id = 
+	  match na with 
+	    | Name id -> fresh_id !avoid (string_of_id id) 
+	    | Anonymous -> fresh_id !avoid "H" 
+      in
+      avoid := new_id :: !avoid;
+      Name new_id
+  in
+  let fresh_decl (na,b,t) = (fresh_id na,b,t) in
+  let princ_info : elim_scheme = 
+    { princ_info with 
+	params = List.map fresh_decl princ_info.params;
+	predicates = List.map fresh_decl princ_info.predicates; 
+	branches = List.map fresh_decl princ_info.branches; 
+	args = List.map fresh_decl princ_info.args
+    }
+  in
+  let wf_tac = 
+    if is_mes 
+    then 
+      (fun b -> Recdef.tclUSER_if_not_mes b None)
+    else fun _ -> prove_with_tcc tcc_lemma_ref []
+  in
+  let real_rec_arg_num = rec_arg_num - princ_info.nparams in 
+  let npost_rec_arg = princ_info.nargs - real_rec_arg_num + 1 in 
+  let (post_rec_arg,pre_rec_arg) = 
+    Util.list_chop npost_rec_arg princ_info.args
+  in
+  let rec_arg_id = 
+    match post_rec_arg with 
+      | (Name id,_,_)::_ -> id 
+      | _ -> assert false 
+  in
+  let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in 
+  let relation = substl subst_constrs relation in 
+  let input_type = substl subst_constrs rec_arg_type in 
+  let wf_thm_id = Nameops.out_name (fresh_id (Name (id_of_string "wf_R"))) in 
+  let acc_rec_arg_id = 
+    Nameops.out_name (fresh_id (Name (id_of_string ("Acc_"^(string_of_id rec_arg_id)))))
+  in 
+  let revert l = 
+    tclTHEN (h_generalize (List.map mkVar l)) (clear l) 
+  in
+  let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in 
+  let prove_rec_arg_acc g = 
+      (observe_tac "prove_rec_arg_acc" 
+	 (tclCOMPLETE
+	    (tclTHEN
+	       (forward 
+		  (Some ((fun g -> observe_tac "prove wf" (tclCOMPLETE (wf_tac is_mes)) g)))
+		  (Genarg.IntroIdentifier wf_thm_id)
+		  (mkApp (delayed_force well_founded,[|input_type;relation|])))
+	       (
+		 observe_tac 
+		   "apply wf_thm" 
+		   (h_apply ((mkApp(mkVar wf_thm_id,
+				    [|mkVar rec_arg_id |])),Rawterm.NoBindings)
+		   )
+	       )
+	    )
+	 )
+      )
+      g
+  in
+  let args_ids = List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.args in
+  tclTHENSEQ
+    [ 
+      h_intros 
+	(List.rev_map (fun (na,_,_) -> Nameops.out_name na) 
+	   (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params)
+	);
+      observe_tac "" (forward
+	 (Some (prove_rec_arg_acc))
+	 (Genarg.IntroIdentifier acc_rec_arg_id)
+ 	 (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
+      );
+      observe_tac "reverting" (revert (List.rev (acc_rec_arg_id::args_ids)));
+      observe_tac "h_fix" (h_fix (Some fix_id) (real_rec_arg_num + 1)); 
+      h_intros (List.rev (acc_rec_arg_id::args_ids));
+      Equality.rewriteLR (mkConst eq_ref);
+      observe_tac "finish" (fun gl' -> 
+	 let body = 
+	   let _,args = destApp (pf_concl gl') in 
+	   array_last args
+	 in
+	 let body_info rec_hyps = 
+	   {
+	     nb_rec_hyps = List.length rec_hyps;
+	     rec_hyps = rec_hyps;
+	     eq_hyps = [];
+	     info = body
+	   }
+	 in 
+	 let acc_inv = 
+	   lazy (
+	     mkApp (
+	       delayed_force acc_inv_id,
+	       [|input_type;relation;mkVar rec_arg_id|]
+	     )
+	   )
+	 in
+	 let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar  acc_rec_arg_id|])) in
+	 let predicates_names = 
+	   List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.predicates
+	 in
+	 let pte_info = 
+	   { proving_tac =
+	       (fun eqs -> 
+		  observe_tac "new_prove_with_tcc" 
+		    (new_prove_with_tcc 
+		       is_mes acc_inv fix_id tcc_lemma_ref (List.map mkVar eqs)
+		    )
+	       );
+	     is_valid = is_valid_hypothesis predicates_names
+	   }
+	 in
+	 let ptes_info : pte_info Idmap.t = 
+	   List.fold_left
+	     (fun map pte_id -> 
+		Idmap.add pte_id 
+		  pte_info			       
+		  map
+	     )
+	     Idmap.empty
+	     predicates_names
+	 in
+	 let make_proof rec_hyps = 
+	   build_proof 
+	     false 
+	     [f_ref]
+	     ptes_info
+	     (body_info rec_hyps)
+	 in
+	 observe_tac "instanciate_hyps_with_args" 
+	   (instanciate_hyps_with_args 
+	      make_proof
+	      (List.map (fun (na,_,_) -> Nameops.out_name na) princ_info.branches)
+	      (List.rev args_ids)
+	   )
+	   gl'
+      )
+			   
+    ]
+    gl    
 
 
 
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 43d14f521..c7f100c36 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -271,7 +271,7 @@ let derive_inversion fix_names =
   with _ -> ()
 
 let generate_principle 
-    is_general do_built fix_rec_l recdefs  interactive_proof parametrize 
+    is_general do_built fix_rec_l recdefs  interactive_proof 
     (continue_proof : int -> Names.constant array -> Term.constr array -> int -> 
       Tacmach.tactic) : unit =
   let names = List.map (function (name,_,_,_,_) -> name) fix_rec_l in
@@ -280,7 +280,7 @@ let generate_principle
   let funs_types =  List.map (function (_,_,_,types,_) -> types) fix_rec_l in
   try 
     (* We then register the Inductive graphs of the functions  *)
-    Rawterm_to_relation.build_inductive parametrize names funs_args funs_types recdefs;
+    Rawterm_to_relation.build_inductive names funs_args funs_types recdefs;
     if do_built 
     then
       begin
@@ -472,7 +472,6 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	      fixpoint_exprl 
 	      recdefs
 	      true
-	      false
 	  in 
 	  if register_built 
 	  then register_wf name rec_impls wf_rel wf_x using_lemmas args types body pre_hook;
@@ -485,11 +484,10 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	      fixpoint_exprl 
 	      recdefs
 	      true
-	      false
 	  in 
 	  if register_built 
 	  then register_mes name rec_impls wf_mes wf_x using_lemmas args types body pre_hook;
-	  false
+	  true
       | _ -> 
 	  let fix_names = 
 	    List.map (function (name,_,_,_,_) -> name) fixpoint_exprl 
@@ -538,7 +536,6 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	    fixpoint_exprl
 	    recdefs 
 	    interactive_proof
-	    true
 	    (Functional_principles_proofs.prove_princ_for_struct interactive_proof);
 	  if register_built then derive_inversion fix_names;
 	  true;
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 5f09b3590..aca84f062 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1075,7 +1075,7 @@ let rec rebuild_return_type rt =
 
 
 let do_build_inductive 
-    parametrize funnames (funsargs: (Names.name * rawconstr * bool) list list)  
+    funnames (funsargs: (Names.name * rawconstr * bool) list list)  
     returned_types 
     (rtl:rawconstr list) =
   let _time1 = System.get_time () in
@@ -1133,12 +1133,7 @@ let do_build_inductive
   in
   let rel_constructors = Array.mapi rel_constructors resa in
   (* Computing the set of parameters if asked *)
-  let rels_params = 
-    if parametrize 
-    then
-      compute_params_name relnames_as_set funsargs  rel_constructors 
-    else []
-  in
+  let rels_params = compute_params_name relnames_as_set funsargs  rel_constructors in
   let nrel_params = List.length rels_params in
   let rel_constructors = (* Taking into account the parameters in constructors *)
     Array.map (List.map 
@@ -1248,9 +1243,9 @@ let do_build_inductive
 
 
 
-let build_inductive parametrize funnames funsargs returned_types rtl = 
+let build_inductive funnames funsargs returned_types rtl = 
   try 
-    do_build_inductive  parametrize funnames funsargs returned_types rtl
+    do_build_inductive funnames funsargs returned_types rtl
   with e -> raise (Building_graph e)
       
 
diff --git a/contrib/funind/rawterm_to_relation.mli b/contrib/funind/rawterm_to_relation.mli
index 33d1cacc7..0075fb0a0 100644
--- a/contrib/funind/rawterm_to_relation.mli
+++ b/contrib/funind/rawterm_to_relation.mli
@@ -8,7 +8,6 @@
 *)
 
 val build_inductive :
-  bool -> (* if true try to detect parameter. Always use it as true except for debug *)
   Names.identifier list -> (* The list of function name *)
   (Names.name*Rawterm.rawconstr*bool) list list -> (* The list of function args *)
   Topconstr.constr_expr list -> (* The list of function returned type *)