correction of bug #1220

adding a "using" optional argument to Function.


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

3 files changed, 82 insertions, 36 deletions

diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 9a8d52eb7c..b234ce1f23 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -129,8 +129,8 @@ let functional_induction with_clean c princl pat =
 
 type annot = 
     Struct of identifier 
-  | Wf of Topconstr.constr_expr * identifier option
-  | Mes of Topconstr.constr_expr * identifier option
+  | Wf of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list
+  | Mes of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list
 
 
 type newfixpoint_expr =
@@ -360,7 +360,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
     tcc_lemma_ref is_mes  rec_arg_num rec_arg_type relation
 
 
-let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
+let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg using_lemmas args ret_type body
     pre_hook 
     =  
   let type_of_f = Command.generalize_constr_expr ret_type args in 
@@ -414,9 +414,10 @@ let register_wf ?(is_mes=false) fname wf_rel_expr wf_arg args ret_type body
     rec_arg_num
     eq
     hook
+    using_lemmas
 
     
-let register_mes fname wf_mes_expr wf_arg args ret_type body = 
+let register_mes fname wf_mes_expr wf_arg using_lemmas args ret_type body = 
   let wf_arg_type,wf_arg = 
     match wf_arg with 
       | None -> 
@@ -455,14 +456,15 @@ let register_mes fname wf_mes_expr wf_arg args ret_type body =
   let wf_rel_from_mes = 
     Topconstr.mkAppC(Topconstr.mkRefC  ltof,[wf_arg_type;fun_from_mes])
   in
-  register_wf ~is_mes:true fname wf_rel_from_mes (Some wf_arg) args ret_type body
+  register_wf ~is_mes:true fname wf_rel_from_mes (Some wf_arg) 
+    using_lemmas args ret_type body
 	  
 
 let do_generate_principle register_built interactive_proof fixpoint_exprl  = 
   let recdefs = build_newrecursive fixpoint_exprl in 
   let _is_struct = 
     match fixpoint_exprl with 
-      | [((name,Some (Wf (wf_rel,wf_x)),args,types,body))] -> 
+      | [((name,Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> 
 	  let pre_hook = 
 	    generate_principle 
 	      true
@@ -472,9 +474,10 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	      true
 	      false
 	  in 
-	  if register_built then register_wf name wf_rel wf_x args types body pre_hook;
+	  if register_built 
+	  then register_wf name wf_rel wf_x using_lemmas args types body pre_hook;
 	  false
-      | [((name,Some (Mes (wf_mes,wf_x)),args,types,body))] -> 
+      | [((name,Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> 
 	  let pre_hook = 
 	    generate_principle 
 	      true
@@ -484,7 +487,8 @@ let do_generate_principle register_built interactive_proof fixpoint_exprl  =
 	      true
 	      false
 	  in 
-	  if register_built then register_mes name wf_mes wf_x args types body pre_hook;
+	  if register_built 
+	  then register_mes name wf_mes wf_x using_lemmas args types body pre_hook;
 	  false
       | _ -> 
 	  let fix_names = 
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4
index d0be12288a..6476340a60 100644
--- a/contrib/funind/indfun_main.ml4
+++ b/contrib/funind/indfun_main.ml4
@@ -103,10 +103,28 @@ TACTIC EXTEND snewfunind
 END
 
 
+let pr_constr_coma_sequence prc _ _ = Util.prlist_with_sep Util.pr_coma prc
+
+ARGUMENT EXTEND constr_coma_sequence'
+  TYPED AS constr_list
+  PRINTED BY pr_constr_coma_sequence
+| [ constr(c) "," constr_coma_sequence'(l) ] -> [ c::l ]
+| [ constr(c) ] -> [ [c] ]
+END
+
+let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
+
+ARGUMENT EXTEND auto_using'
+  TYPED AS constr_list
+  PRINTED BY pr_auto_using
+| [ "using" constr_coma_sequence'(l) ] -> [ l ]
+| [ ] -> [ [] ]
+END
+
 VERNAC ARGUMENT EXTEND rec_annotation2
   [ "{"  "struct" ident(id)  "}"] -> [ Struct id ]
-| [ "{" "wf" constr(r) ident_opt(id) "}" ] -> [ Wf(r,id) ]
-| [ "{" "measure" constr(r) ident_opt(id) "}" ] -> [ Mes(r,id) ] 
+| [ "{" "wf" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Wf(r,id,l) ]
+| [ "{" "measure" constr(r) ident_opt(id) auto_using'(l) "}" ] -> [ Mes(r,id,l) ] 
 END
 
 
@@ -131,8 +149,8 @@ VERNAC ARGUMENT EXTEND rec_definition2
      let check_exists_args an =
        try 
 	 let id = match an with 
-	   | Struct id -> id | Wf(_,Some id) -> id | Mes(_,Some id) -> id 
-	   | Wf(_,None) | Mes(_,None) -> failwith "check_exists_args" 
+	   | Struct id -> id | Wf(_,Some id,_) -> id | Mes(_,Some id,_) -> id 
+	   | Wf(_,None,_) | Mes(_,None,_) -> failwith "check_exists_args" 
 	 in 
 	 (try ignore(Util.list_index (Name id) names - 1); annot
 	  with Not_found ->  Util.user_err_loc
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 7404722370..731ded8dc5 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -763,7 +763,7 @@ let whole_start is_mes func input_type relation rec_arg_num  : tactic =
 	   )
 	     g 
 	)
-	tclUSER_if_not_mes
+	tclUSER_if_not_mes 
 	g 
   end
 
@@ -771,7 +771,7 @@ let whole_start is_mes func input_type relation rec_arg_num  : tactic =
 let get_current_subgoals_types () = 
   let pts =  get_pftreestate () in 
   let _,subs = extract_open_pftreestate pts in 
-  List.map snd subs 
+  List.map snd (List.sort (fun (x,_) (y,_) -> x -y )subs )
 
 
 let build_and_l l = 
@@ -837,7 +837,7 @@ let prove_with_tcc lemma _ : tactic =
       
 	     
 
-let open_new_goal ref goal_name (gls_type,decompose_and_tac,nb_goal)   = 
+let open_new_goal using_lemmas ref goal_name (gls_type,decompose_and_tac,nb_goal)   = 
   let current_proof_name = get_current_proof_name () in
   let name = match goal_name with 
     | Some s -> s 
@@ -866,8 +866,28 @@ let open_new_goal ref goal_name (gls_type,decompose_and_tac,nb_goal)   =
     sign
     gls_type 
     hook ;
-  by (decompose_and_tac);
-  if Options.is_verbose () then (pp (Printer.pr_open_subgoals()))
+  by (
+    fun g -> 
+      tclTHEN 
+	(decompose_and_tac)
+	(tclORELSE 
+	(tclFIRST 
+	   (List.map
+	      (fun c -> 
+		 tclTHENSEQ
+		   [intros; 
+		    h_apply (interp_constr Evd.empty (Global.env()) c,Rawterm.NoBindings); 
+		    tclCOMPLETE Auto.default_auto
+		   ]
+	      )
+	      using_lemmas)
+	) tclIDTAC)
+	g);
+  try
+    by tclIDTAC; (* raises UserError _ if the proof is complete *)
+    if Options.is_verbose () then (pp (Printer.pr_open_subgoals()))
+  with UserError _ -> 
+    defined ()
   
     
 let com_terminate 
@@ -878,7 +898,7 @@ let com_terminate
     input_type
     relation 
     rec_arg_num
-    thm_name hook =
+    thm_name using_lemmas hook =
   let (evmap, env) = Command.get_current_context() in
   start_proof thm_name
     (Global, Proof Lemma) (Environ.named_context_val env)
@@ -887,7 +907,7 @@ let com_terminate
 				       input_type relation rec_arg_num ));
   try 
     let new_goal_type = build_new_goal_type () in 
-    open_new_goal tcc_lemma_ref
+    open_new_goal using_lemmas tcc_lemma_ref
       (Some tcc_lemma_name)
       (new_goal_type)
   with Failure "empty list of subgoals!" -> 
@@ -969,9 +989,9 @@ let start_equation (f:global_reference) (term_f:global_reference)
   in
   tclTHENLIST [
     h_intros x;
-    unfold_constr f;
-    simplest_case (mkApp (terminate_constr, Array.of_list (List.map mkVar x)));
-    cont_tactic x] g
+    observe_tac "unfold_constr f" (unfold_constr f);
+    observe_tac "simplest_case" (simplest_case (mkApp (terminate_constr, Array.of_list (List.map mkVar x))));
+    observe_tac "prove_eq" (cont_tactic x)] g
 ;;
 
 let base_leaf_eq func eqs f_id g =
@@ -1095,8 +1115,8 @@ let rec prove_eq  (termine:constr) (f:constr)(functional:global_reference)
 	     _,[] -> 
 	       tclTHENS(mkCaseEq a)(* (simplest_case a) *)
 	  	 (List.map
-		    (mk_intros_and_continue true
-		       (prove_eq  termine f functional) eqs)
+		    (fun expr -> observe_tac "mk_intros_and_continue" (mk_intros_and_continue true
+		       (prove_eq  termine f functional) eqs expr))
 		    (Array.to_list l))
 	   | _,_::_ ->
                	(match find_call_occs f expr with
@@ -1119,13 +1139,13 @@ let rec prove_eq  (termine:constr) (f:constr)(functional:global_reference)
 
 let (com_eqn : identifier ->
        global_reference -> global_reference -> global_reference
-	 -> constr_expr -> unit) =
-  fun eq_name functional_ref f_ref terminate_ref eq ->
+	 -> constr -> unit) =
+  fun eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
     let (evmap, env) = Command.get_current_context() in
-    let eq_constr = interp_constr evmap env eq in
     let f_constr = (constr_of_reference f_ref) in
+    let equation_lemma_type = subst1 f_constr equation_lemma_type in
     (start_proof eq_name (Global, Proof Lemma)
-       (Environ.named_context_val env) eq_constr (fun _ _ -> ());
+       (Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
      by
        (start_equation f_ref terminate_ref
 	  (fun x ->
@@ -1145,17 +1165,18 @@ let (com_eqn : identifier ->
 
 
 let recursive_definition is_mes function_name type_of_f r rec_arg_num eq 
-    generate_induction_principle : unit =
+    generate_induction_principle using_lemmas : unit =
   let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
-  let env = push_rel (Name function_name,None,function_type) (Global.env()) in
-  let res_vars,eq' = decompose_prod (interp_constr Evd.empty env eq) in 
+  let env = push_named (function_name,None,function_type) (Global.env()) in
+  let equation_lemma_type = interp_constr Evd.empty env eq in 
+  let res_vars,eq' = decompose_prod equation_lemma_type in 
   let res = 
 (*     Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
 (*     Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *)
 (*     Pp.msgnl (str "eq' := " ++ str (string_of_int rec_arg_num)); *)
     match kind_of_term eq' with 
       | App(e,[|_;_;eq_fix|]) -> 
-	  mkLambda (Name function_name,function_type,compose_lam res_vars eq_fix)
+	  mkLambda (Name function_name,function_type,subst_var function_name (compose_lam res_vars  eq_fix))
       | _ -> failwith "Recursive Definition (res not eq)"
   in
   let pre_rec_args,function_type_before_rec_arg = decompose_prod_n (rec_arg_num - 1) function_type in 
@@ -1180,9 +1201,11 @@ let recursive_definition is_mes function_name type_of_f r rec_arg_num eq
     let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
 (*     message "start second proof"; *)
     begin 
-      try com_eqn equation_id functional_ref f_ref term_ref eq
+      try com_eqn equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type)
       with e -> 
 	begin 
+	  if Tacinterp.get_debug () <> Tactic_debug.DebugOff
+	  then anomalylabstrm "" (str "Cannot create equation Lemma " ++ Cerrors.explain_exn e);
 	  ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ());
 	  anomaly "Cannot create equation Lemma"
 	end
@@ -1208,6 +1231,7 @@ let recursive_definition is_mes function_name type_of_f r rec_arg_num eq
       rec_arg_type
       relation rec_arg_num
       term_id
+      using_lemmas
       hook 
   with e -> 
     begin
@@ -1228,10 +1252,10 @@ VERNAC COMMAND EXTEND RecursiveDefinition
 	| None -> 1
 	| Some n -> n 
     in
-    recursive_definition false f type_of_f r rec_arg_num eq (fun _ _ _ _ _  _ _ _ -> ())]
+    recursive_definition false f type_of_f r rec_arg_num eq (fun _ _ _ _ _  _ _ _ -> ()) []]
 | [ "Recursive" "Definition" ident(f) constr(type_of_f) constr(r) constr(wf)
      "[" ne_constr_list(proof) "]" constr(eq) ] ->
-  [ ignore(proof);ignore(wf);recursive_definition false f type_of_f r 1 eq  (fun  _ _  _ _ _ _ _ _ -> ())]
+  [ ignore(proof);ignore(wf);recursive_definition false f type_of_f r 1 eq  (fun  _ _  _ _ _ _ _ _ -> ()) []]
 END