+functional inversion now takes the function to invert as an optional argument.

+ Code cleaning un Function code 


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

10 files changed, 137 insertions, 41 deletions

diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 14dfbdffc..7977d4e0f 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -16,10 +16,7 @@ open Indfun_common
 open Libnames
 
 let msgnl = Pp.msgnl
-
-let do_observe () = 
-  Tacinterp.get_debug () <> Tactic_debug.DebugOff  
-
+  
 
 let observe strm =
   if do_observe ()
@@ -751,10 +748,6 @@ let build_proof
      (build_proof_aux do_finalize dyn_infos) g
   and build_proof_args do_finalize dyn_infos (* f_args'  args *) :tactic =
     fun g ->
-(*      if Tacinterp.get_debug () <> Tactic_debug.DebugOff  *)
-(*      then msgnl (str "build_proof_args with "  ++  *)
-(* 		   pr_lconstr_env (pf_env g) f_args' *)
-(* 		); *)
       let (f_args',args) = dyn_infos.info in 
       let tac : tactic =
 	fun g -> 
diff --git a/contrib/funind/functional_principles_proofs.mli b/contrib/funind/functional_principles_proofs.mli
index 35da5d507..62eb528e0 100644
--- a/contrib/funind/functional_principles_proofs.mli
+++ b/contrib/funind/functional_principles_proofs.mli
@@ -16,5 +16,4 @@ val prove_principle_for_gen :
   Tacmach.tactic
 
 
-val is_pte  : rel_declaration -> bool 
-val do_observe : unit -> bool 
+(* val is_pte  : rel_declaration -> bool  *)
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 8e6ff7c2f..f83eae8d3 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -32,8 +32,9 @@ let pr_elim_scheme el =
   msg ++ fnl () ++ str "concl := " ++ pr_lconstr_env env el.concl
 
 
-let observe s = if Functional_principles_proofs.do_observe () 
-then Pp.msgnl s 
+let observe s = 
+  if do_observe () 
+  then Pp.msgnl s 
 
 
 let pr_elim_scheme el = 
@@ -49,8 +50,9 @@ let pr_elim_scheme el =
   msg ++ fnl () ++ str "concl := " ++ pr_lconstr_env env el.concl
 
 
-let observe s = if Functional_principles_proofs.do_observe () 
-then Pp.msgnl s 
+let observe s = 
+  if do_observe () 
+  then Pp.msgnl s 
 
 (* 
    Transform an inductive induction principle into 
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 3830cdb21..dffc81209 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -238,6 +238,19 @@ let prepare_body (name,annot,args,types,body) rt =
   (fun_args,rt')
 
 
+let derive_inversion fix_names = 
+  try
+    Invfun.derive_correctness 
+      Functional_principles_types.make_scheme
+      functional_induction 
+	  (List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names)
+      (*i The next call to mk_rel_id is valid since we have just construct the graph 
+	Ensures by : register_built
+	i*) 
+      (List.map (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id))) fix_names)
+  with e -> 
+    msg_warning (str "Cannot define correction of function and graph" ++ Cerrors.explain_exn e)
+	  
 let generate_principle 
     do_built fix_rec_l recdefs  interactive_proof parametrize 
     (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) : unit =
@@ -358,7 +371,7 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
 	(generate_correction_proof_wf f_ref tcc_lemma_ref is_mes
 	   functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
 	);
-      Command.save_named true
+      derive_inversion [fname]
     with e -> 
       (* No proof done *) 
       ()
@@ -486,23 +499,8 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	    interactive_proof
 	    true
 	    (Functional_principles_proofs.prove_princ_for_struct interactive_proof);
-	  if register_built 
-	  then
-	    begin
-	      try 
-		Invfun.derive_correctness 
-		  Functional_principles_types.make_scheme
-		  functional_induction 
-		  (List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names)
-		  (*i The next call to mk_rel_id is valid since we have just construct the graph 
-		    Ensures by : register_built
-		    i*) 
-		  (List.map (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id))) fix_names)
-	      with e -> 
-		msg_warning (str "Cannot define correction of function and graph" ++ Cerrors.explain_exn e)
-	    end;
+	  if register_built then derive_inversion  fix_names;
 	  true;
-		  
   in
   ()
 
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 71840de9e..f41aac205 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -442,3 +442,25 @@ let add_Function f =
   update_Function finfos
 
 let pr_table () = pr_table !function_table
+(*********************************)
+(* Debuging *)
+let function_debug = ref false 
+open Goptions
+
+let function_debug_sig =
+  {
+    optsync = false;
+    optname = "Function debug";
+    optkey =  PrimaryTable("Function_debug");
+    optread = (fun () -> !function_debug);
+    optwrite = (fun b -> function_debug := b)
+  }
+
+let _ = declare_bool_option function_debug_sig
+
+
+let do_observe () = 
+  !function_debug = true
+      
+      
+    
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
index e3e49603f..00e1ce8d9 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -100,3 +100,6 @@ val update_Function : function_info -> unit
 val pr_info : function_info -> Pp.std_ppcmds
 val pr_table : unit -> Pp.std_ppcmds
 
+
+val function_debug : bool ref 
+val do_observe : unit -> bool
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index d45941540..00b5f28ca 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -49,7 +49,7 @@ END
 
 
 TACTIC EXTEND newfuninv
-   [ "functional" "inversion"  quantified_hypothesis(hyp) reference(fname) ] -> 
+   [ "functional" "inversion"  quantified_hypothesis(hyp) reference_opt(fname) ] -> 
      [
        Invfun.invfun hyp fname
      ]
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 7dd3bc112..084ec7e01 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -66,10 +66,6 @@ let pr_elim_scheme el =
 (* The local debuging mechanism *)
 let msgnl = Pp.msgnl
 
-let do_observe () = 
-  Tacinterp.get_debug () <> Tactic_debug.DebugOff  
-
-
 let observe strm =
   if do_observe ()
   then Pp.msgnl strm
@@ -580,6 +576,14 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	tclTHENSEQ[
 	  tclMAP h_intro ids;
 	  Equality.rewriteLR (mkConst eq_lemma);
+	  (* Don't forget to $\zeta$ normlize the term since the principles have been $\zeta$-normalized *)
+	  h_reduce 
+	    (Rawterm.Cbv
+	       {Rawterm.all_flags 
+		with Rawterm.rDelta = false; 		 
+	       }) 
+	    onConcl
+	  ;
 	  h_generalize (List.map mkVar ids);
 	  thin ids
 	]
@@ -933,3 +937,43 @@ let invfun qhyp f  =
   with 
     | Not_found ->  error "No graph found" 
     | Failure "out_some"  -> error "Cannot use equivalence with graph!"
+
+
+let invfun qhyp f g = 
+  match f with 
+    | Some f -> invfun qhyp f g
+    | None -> 
+	Tactics.try_intros_until 
+	  (fun hid g -> 
+	     let hyp_typ = pf_type_of g (mkVar hid)  in 
+	     match kind_of_term hyp_typ with 
+	       | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ()) -> 
+		   begin
+		     let f1,_ = decompose_app args.(1) in 
+		     try 
+		       if not (isConst f1) then failwith "";
+		       let finfos = find_Function_infos (destConst f1) in 
+		       let f_correct = mkConst(out_some finfos.correctness_lemma) 
+		       and kn = fst finfos.graph_ind
+		       in
+		       functional_inversion kn hid f1 f_correct g
+		     with | Failure "" | Failure "out_some" | Not_found -> 
+		       try 
+			 let f2,_ = decompose_app args.(2) in 
+			 if not (isConst f2) then failwith "";
+			 let finfos = find_Function_infos (destConst f2) in 
+			 let f_correct = mkConst(out_some finfos.correctness_lemma) 
+			 and kn = fst finfos.graph_ind
+			 in
+			 functional_inversion kn hid  f2 f_correct g
+		       with
+			 | Failure "" -> 
+			     errorlabstrm "" (Ppconstr.pr_id hid ++ str " must contain at leat one function")
+			 | Failure "out_some"  ->  
+			     error "Cannot use equivalence with graph for any side of equality"
+			 | Not_found -> error "No graph found for any side of equality" 
+		   end
+	       | _ -> errorlabstrm "" (Ppconstr.pr_id hid ++ str " must be an equality ")
+	  )
+	  qhyp
+	  g
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index ba60f49ed..dbf2f9441 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -9,11 +9,11 @@ open Util
 open Rawtermops
 
 let observe strm =  
-  if Tacinterp.get_debug () <> Tactic_debug.DebugOff  
+  if do_observe ()
   then Pp.msgnl strm 
   else ()
 let observennl strm =  
-  if Tacinterp.get_debug () <> Tactic_debug.DebugOff  
+  if do_observe ()
   then Pp.msg strm 
   else ()
 
@@ -416,6 +416,40 @@ let add_pat_variables pat typ env : Environ.env =
 
 
 
+
+let rec pattern_to_term_and_type env typ  = function
+  | PatVar(loc,Anonymous) -> assert false
+  | PatVar(loc,Name id) ->
+	mkRVar id
+  | PatCstr(loc,constr,patternl,_) ->
+      let cst_narg =
+	Inductiveops.mis_constructor_nargs_env
+	  (Global.env ())
+	  constr
+      in
+      let Inductiveops.IndType(indf,indargs) = 
+	try Inductiveops.find_rectype env Evd.empty typ
+	with Not_found -> assert false 
+      in
+      let constructors = Inductiveops.get_constructors env indf in 
+      let constructor  = List.find (fun cs -> cs.Inductiveops.cs_cstr = constr) (Array.to_list constructors) in 
+      let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in 
+      let _,cstl = Inductiveops.dest_ind_family indf in 
+      let csta = Array.of_list cstl in 
+      let implicit_args =
+	Array.to_list
+	  (Array.init
+	     (cst_narg - List.length patternl)
+	     (fun i -> Detyping.detype false [] (Termops.names_of_rel_context env) csta.(i))
+	  )
+      in
+      let patl_as_term =
+	List.map2 (pattern_to_term_and_type env)  (List.rev cs_args_types)  patternl
+      in
+      mkRApp(mkRRef(Libnames.ConstructRef constr),
+	     implicit_args@patl_as_term
+	    )
+
 (* [build_entry_lc funnames avoid rt] construct the list (in fact a build_entry_return) 
    of constructors corresponding to [rt] when replacing calls to [funnames] by calls to the 
    corresponding graphs. 
@@ -689,7 +723,7 @@ and build_entry_lc_from_case env funname make_discr
 	  List.map 
 	    (build_entry_lc_from_case_term
 	       env types
-	       funname (make_discr (List.map fst el))
+	       funname (make_discr (* (List.map fst el) *))
 	       []  brl 
 	       case_resl.to_avoid) 
 	    case_resl.result 
@@ -799,7 +833,8 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 			     List.for_all (fun x -> x) unif) patterns_to_prevent
 	   then 
 	     let i = List.length patterns_to_prevent in 
-	     [(Prod Anonymous,make_discr i  )]
+	     let pats_as_constr = List.map2 (pattern_to_term_and_type new_env) types patl in
+	     [(Prod Anonymous,make_discr pats_as_constr i  )]
 	   else 
 	     []
 	  )
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index 204249f1d..14805cf49 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -321,7 +321,7 @@ let rec alpha_rt excluded rt =
 	     List.map (alpha_rt excluded) args
 	    )
   in 
-  if Tacinterp.get_debug () <> Tactic_debug.DebugOff  && false 
+  if Indfun_common.do_observe ()  && false 
   then
     Pp.msgnl (str "debug: alpha_rt(" ++ str "[" ++
 	      prlist_with_sep (fun _ -> str";") Ppconstr.pr_id excluded ++