Julien:

+ Compatibility with new induction
+ Induction principle for general recursion preparation still continuing
+ Cleaning dead code ...


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

1 files changed, 242 insertions, 12 deletions

diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index 43977de320..b07a587d14 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -48,13 +48,15 @@ open Genarg
 let h_intros l = 
   tclMAP h_intro l
 
+let do_observe_tac s tac g =
+  let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in
+ try let v = tac g in msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); v
+ with e ->
+   msgnl (str "observation "++str s++str " raised exception " ++ 	Cerrors.explain_exn e ++ str "on goal " ++ goal ); raise e;;
+
+
 let observe_tac s tac g = tac g
 
-(* let observe_tac s tac g = *)
-(*   let goal = begin try (Printer.pr_goal (sig_it g)) with _ -> assert false end in  *)
-(*  try let v = tac g in msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); v *)
-(*  with e -> *)
-(*    msgnl (str "observation "++str s++str " raised an exception on goal " ++ goal ); raise e;; *)
 
 let hyp_ids = List.map id_of_string
     ["x";"v";"k";"def";"p";"h";"n";"h'"; "anonymous"; "teq"; "rec_res";
@@ -282,7 +284,7 @@ let list_rewrite (rev:bool) (eqs: constr list) =
        (fun eq i -> tclORELSE (rewriteLR eq) i)
        (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
 
-let base_leaf (func:global_reference) eqs expr =
+let base_leaf_terminate (func:global_reference) eqs expr =
 (*  let _ = msgnl (str "entering base_leaf") in *)
   (fun g ->
      let ids = pf_ids_of_hyps g in
@@ -454,12 +456,13 @@ let rec introduce_all_values is_mes acc_inv func context_fn
     )
  
 	   
-let rec_leaf is_mes acc_inv hrec (func:global_reference) eqs expr =
+let rec_leaf_terminate is_mes acc_inv hrec (func:global_reference) eqs expr =
   match find_call_occs (mkVar (get_f (constr_of_reference func))) expr with
   | context_fn, args ->
       observe_tac "introduce_all_values" 
 	(introduce_all_values is_mes acc_inv func context_fn eqs  hrec args  [] [])
 
+(* 
 let rec proveterminate is_mes acc_inv (hrec:identifier)  
   (f_constr:constr) (func:global_reference) (eqs:constr list) (expr:constr)  =
 try
@@ -500,6 +503,54 @@ try
 with e -> 
   msgerrnl(str "failure in proveterminate"); 
   raise e
+*)
+let proveterminate is_mes acc_inv (hrec:identifier)  
+  (f_constr:constr) (func:global_reference) base_leaf rec_leaf = 
+  let rec proveterminate (eqs:constr list) (expr:constr)  =
+    try
+      (*  let _ = msgnl (str "entering proveterminate") in *)
+      let v =
+	match (kind_of_term expr) with
+	    Case (_, t, a, l) -> 
+	      (match find_call_occs f_constr a with
+		   _,[] ->
+      		     tclTHENS 
+		       (fun g ->
+			  (* let _ = msgnl(str "entering mkCaseEq") in *)
+			  let v = (mkCaseEq a) g in 
+			  (* let _ = msgnl (str "exiting mkCaseEq") in *)
+			  v
+		       )
+   	               (List.map 
+			  (mk_intros_and_continue true proveterminate eqs)
+			  (Array.to_list l)
+		       )
+		 | _, _::_ -> 
+		     (
+		       match find_call_occs  f_constr expr with
+	     		   _,[] -> observe_tac "base_leaf" (base_leaf func eqs expr)
+			 | _, _:: _ -> 
+			     observe_tac "rec_leaf" 
+			       (rec_leaf is_mes acc_inv hrec  func eqs expr)
+		     )
+	      )
+	  | _ ->  (match find_call_occs  f_constr expr with
+	     	       _,[] -> 
+			 (try 
+			    observe_tac "base_leaf" (base_leaf func eqs expr)
+			  with e -> 
+			    (msgerrnl (str "failure in base case");raise e ))
+		     | _, _::_ -> 
+			 observe_tac "rec_leaf" 
+			   (rec_leaf is_mes acc_inv hrec  func eqs expr)
+		  ) in
+      (*  let _ = msgnl(str "exiting proveterminate") in *)
+      v
+    with e -> 
+      msgerrnl(str "failure in proveterminate"); 
+      raise e
+  in 
+  proveterminate 
 
 let hyp_terminates func = 
   let a_arrow_b = arg_type (constr_of_reference func) in 
@@ -668,6 +719,8 @@ let whole_start is_mes func input_type relation rec_arg_num  : tactic =
 	      hrec
 	      (mkVar f_id)
 	      func
+	      base_leaf_terminate 
+	      rec_leaf_terminate
 	      []
 	      expr
 	   )
@@ -935,7 +988,7 @@ let (com_eqn : identifier ->
      Command.save_named true);;
 
 
-let recursive_definition is_mes f type_of_f r  rec_arg_num eq =
+let recursive_definition is_mes f type_of_f r rec_arg_num eq generate_induction_principle =
   let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
   let env = push_rel (Name f,None,function_type) (Global.env()) in
   let res_vars,eq' = decompose_prod (interp_constr Evd.empty env eq) in 
@@ -969,11 +1022,185 @@ let recursive_definition is_mes f type_of_f r  rec_arg_num eq =
     let f_ref = declare_f f (IsProof Lemma) arg_types term_ref in
 (*     let _ = message "start second proof" in *)
     com_eqn equation_id functional_ref f_ref term_ref eq;
-      ()
+    let eq_ref = Nametab.locate (make_short_qualid equation_id ) in
+    generate_induction_principle
+      functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation;
+    ()
+
   in
-  com_terminate is_mes functional_ref rec_arg_type relation  rec_arg_num term_id  hook 
+  com_terminate is_mes functional_ref rec_arg_type relation rec_arg_num term_id  hook 
 ;;
 
+
+
+(* let observe_tac = do_observe_tac  *)
+
+let base_leaf_princ eq_cst functional_ref eqs expr = 
+  tclTHENSEQ 
+    [rewriteLR (mkConst eq_cst);
+     list_rewrite true eqs;
+     gen_eauto(* default_eauto *) false (false,5) [] (Some [])
+    ]
+
+
+
+let finalize_rec_leaf_princ_with is_mes hrec acc_inv br = 
+  tclTHENSEQ [
+    Eauto.e_resolve_constr (mkVar br);
+    tclFIRST
+      [
+	e_assumption;
+	reflexivity;
+	tclTHEN (apply (mkVar hrec))
+	  (tclTHENS
+	     (* (try *) (observe_tac "applying inversion" (apply (Lazy.force acc_inv))) 
+(* 	      with e -> Pp.msgnl (Printer.pr_lconstr (Lazy.force acc_inv));raise e *)
+(* 	     ) *)
+	     [ h_assumption
+	     ;
+	       (fun g ->
+	       tclUSER
+		 is_mes
+		 (Some (hrec::(retrieve_acc_var g)))
+		 g
+	       )
+	     ]
+	  );
+	(fun g -> tclIDTAC_MESSAGE (str "here" ++ Printer.pr_goal (sig_it g)) g)
+      ]
+  ]
+    
+let rec_leaf_princ
+    eq_cst
+    branches_names 
+    is_mes
+    acc_inv
+    hrec
+    (functional_ref:global_reference) 
+    eqs
+    expr
+    = 
+  
+  tclTHENSEQ 
+    [ rewriteLR (mkConst eq_cst);
+      list_rewrite true eqs;
+      tclFIRST 
+	(List.map (finalize_rec_leaf_princ_with is_mes hrec acc_inv) branches_names)
+    ]
+
+
+let fresh_id avoid na = 
+  let id =  
+    match na with 
+      | Name id -> id 
+      | Anonymous -> h_id 
+  in 
+  next_global_ident_away true id avoid
+
+
+
+let prove_principle is_mes functional_ref 
+    eq_ref rec_arg_num rec_arg_type nb_args relation = 
+(*  f_ref eq_ref rec_arg_num rec_arg_type nb_args relation *)
+  let eq_cst =   
+    match eq_ref with 
+	ConstRef sp -> sp 
+      | _ -> assert false 
+  in
+  fun g -> 
+    let type_of_goal = pf_concl g in 
+    let goal_ids = pf_ids_of_hyps g in 
+    let goal_elim_infos = compute_elim_sig  (mkRel 0,Rawterm.NoBindings) type_of_goal in 
+    let params_names,ids = List.fold_left 
+      (fun (params_names,avoid) (na,_,_) -> 
+	 let new_id = fresh_id avoid na in 
+	 (new_id::params_names,new_id::avoid)
+      )
+      ([],goal_ids)
+      goal_elim_infos.params
+    in
+    let predicates_names,ids = 
+      List.fold_left 
+	(fun (predicates_names,avoid) (na,_,_) -> 
+	   let new_id = fresh_id avoid na in 
+	   (new_id::predicates_names,new_id::avoid)
+	)
+	([],ids)
+	goal_elim_infos.predicates
+    in
+    let branches_names,ids = 
+      List.fold_left 
+	(fun (branches_names,avoid) (na,_,_) -> 
+	   let new_id = fresh_id avoid na in 
+	   (new_id::branches_names,new_id::avoid)
+	)
+	([],ids)
+	goal_elim_infos.branches
+    in
+    let to_intro = params_names@predicates_names@branches_names in 
+    let nparams = List.length params_names in 
+    let rec_arg_num = rec_arg_num - nparams in 
+    begin 
+      tclTHEN 
+	(h_intros to_intro)
+	(observe_tac (string_of_int (rec_arg_num)) 
+	   (fun g -> 
+	      let ids = ids_of_named_context (pf_hyps g) in
+	      let func_body = (def_of_const (constr_of_reference functional_ref)) in
+(* 	      let _ = Pp.msgnl (Printer.pr_lconstr func_body) in  *)
+	      let (f_name, _, body1) = destLambda func_body in
+	      let f_id =
+		match f_name with
+		  | Name f_id -> next_global_ident_away true f_id ids
+		  | Anonymous -> assert false 
+	      in
+	      let n_names_types,_ = decompose_lam body1 in 
+	      let n_ids,ids = 
+		List.fold_left 
+		  (fun (n_ids,ids) (n_name,_) -> 
+		     match n_name with 
+		       | Name id -> 
+			   let n_id = next_global_ident_away true id ids in 
+			   n_id::n_ids,n_id::ids
+		       | _ -> assert false
+		  )
+		  ([],(f_id::ids))
+		  n_names_types
+	      in
+	      let rec_arg_id = List.nth n_ids (rec_arg_num - 1 ) in
+	      let expr = 
+		instantiate_lambda func_body
+		  (mkVar f_id::(List.map mkVar n_ids)) 
+	      in 
+	      start 
+		is_mes
+		rec_arg_type
+		ids
+		(snd (list_chop nparams n_ids))
+		(substl (List.map mkVar params_names) relation)
+		(rec_arg_num)
+		rec_arg_id
+		(fun hrec acc_inv g ->  
+		   (proveterminate 
+		      is_mes
+		      acc_inv 
+		      hrec
+		      (mkVar f_id)
+		      functional_ref
+		      (base_leaf_princ eq_cst)
+		      (rec_leaf_princ eq_cst branches_names)
+		      []
+		      expr
+		   )
+		     g 
+		)
+		g )
+	)
+    end
+      g
+
+
+
 VERNAC COMMAND EXTEND RecursiveDefinition
   [ "Recursive" "Definition" ident(f) constr(type_of_f) constr(r) constr(wf)
      constr(proof) integer_opt(rec_arg_num) constr(eq) ] ->
@@ -983,8 +1210,11 @@ VERNAC COMMAND EXTEND RecursiveDefinition
 	| None -> 1
 	| Some n -> n 
     in
-    recursive_definition false f type_of_f r rec_arg_num eq ]
+    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 ]
+  [ ignore(proof);ignore(wf);recursive_definition false f type_of_f r 1 eq  (fun  _ _  _ _ _ _ -> ())]
 END
+
+
+