Uniformisation des politiques de nommage de NewDestruct sur arguments recursifs et Induction style Hrec; mise en place systeme de traduction automatique; Elim/Case reconnaissent les premisses nommees du but

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

4 files changed, 120 insertions, 81 deletions

diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index c63bfb84e3..1ea4388746 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -53,14 +53,16 @@ val h_instantiate     : int -> constr -> Tacticals.clause -> tactic
 
 (* Derived basic tactics *)
 
-val h_simple_induction   : quantified_hypothesis -> tactic
+val h_simple_induction   : quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref -> tactic
 val h_simple_destruct    : quantified_hypothesis -> tactic
 val h_new_induction   :
   constr induction_arg -> constr with_bindings option ->
-    intro_pattern_expr list list -> tactic
+  case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+  -> tactic
 val h_new_destruct    :
   constr induction_arg -> constr with_bindings option -> 
-    intro_pattern_expr list list -> tactic
+  case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+  -> tactic
 val h_specialize      : int option -> constr with_bindings -> tactic
 val h_lapply          : constr -> tactic
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f6b05af45c..488e8833cc 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -625,18 +625,18 @@ let rec intern_atomic lf ist x =
   | TacDAuto (n,p) -> TacDAuto (n,p)
 
   (* Derived basic tactics *)
-  | TacSimpleInduction h ->
-      TacSimpleInduction (intern_quantified_hypothesis ist h)
-  | TacNewInduction (c,cbo,ids) ->
+  | TacSimpleInduction (h,ids) ->
+      TacSimpleInduction (intern_quantified_hypothesis ist h,ids)
+  | TacNewInduction (c,cbo,(ids,ids')) ->
       TacNewInduction (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-               intern_case_intro_pattern lf ist ids)
+               (intern_case_intro_pattern lf ist ids,ids'))
   | TacSimpleDestruct h ->
       TacSimpleDestruct (intern_quantified_hypothesis ist h)
-  | TacNewDestruct (c,cbo,ids) ->
+  | TacNewDestruct (c,cbo,(ids,ids')) ->
       TacNewDestruct (intern_induction_arg ist c,
                option_app (intern_constr_with_bindings ist) cbo,
-	       intern_case_intro_pattern lf ist ids)
+	       (intern_case_intro_pattern lf ist ids,ids'))
   | TacDoubleInduction (h1,h2) ->
       let h1 = intern_quantified_hypothesis ist h1 in
       let h2 = intern_quantified_hypothesis ist h2 in
@@ -1633,18 +1633,18 @@ and interp_atomic ist gl = function
   | TacDAuto (n,p) -> Auto.h_dauto (n,p)
 
   (* Derived basic tactics *)
-  | TacSimpleInduction h ->
-      h_simple_induction (interp_quantified_hypothesis ist gl h)
-  | TacNewInduction (c,cbo,ids) ->
+  | TacSimpleInduction (h,ids) ->
+      h_simple_induction (interp_quantified_hypothesis ist gl h,ids)
+  | TacNewInduction (c,cbo,(ids,ids')) ->
       h_new_induction (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (interp_case_intro_pattern ist ids)
+        (interp_case_intro_pattern ist ids,ids')
   | TacSimpleDestruct h ->
       h_simple_destruct (interp_quantified_hypothesis ist gl h)
-  | TacNewDestruct (c,cbo,ids) -> 
+  | TacNewDestruct (c,cbo,(ids,ids')) -> 
       h_new_destruct (interp_induction_arg ist gl c)
         (option_app (interp_constr_with_bindings ist gl) cbo)
-        (interp_case_intro_pattern ist ids)
+        (interp_case_intro_pattern ist ids,ids')
   | TacDoubleInduction (h1,h2) ->
       let h1 = interp_quantified_hypothesis ist gl h1 in
       let h2 = interp_quantified_hypothesis ist gl h2 in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 4a864bbf38..b35de35928 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -956,11 +956,16 @@ let find_eliminator c gl =
 let default_elim (c,lbindc) gl = 
   general_elim (c,lbindc) (find_eliminator c gl,NoBindings) gl
 
-let elim (c,lbindc) elim gl =
+let elim_in_context (c,_ as cx) elim gl =
   match elim with
-  | Some (elimc,lbindelimc) -> general_elim (c,lbindc) (elimc,lbindelimc) gl
-  | None -> general_elim (c,lbindc) (find_eliminator c gl,NoBindings) gl 
+  | Some (elimc,lbindelimc) -> general_elim cx (elimc,lbindelimc) gl
+  | None -> general_elim cx (find_eliminator c gl,NoBindings) gl 
 
+let elim (c,lbindc as cx) elim =
+  match kind_of_term c with
+    | Var id when lbindc = NoBindings ->
+	tclTHEN (tclTRY (intros_until_id id)) (elim_in_context cx elim)
+    | _ -> elim_in_context cx elim
 
 (* The simplest elimination tactic, with no substitutions at all. *)
 
@@ -1005,7 +1010,7 @@ let general_elim_in id (c,lbindc) (elimc,lbindelimc) gl =
 
 (* Case analysis tactics *)
 
-let general_case_analysis (c,lbindc) gl =
+let general_case_analysis_in_context (c,lbindc) gl =
   let env = pf_env gl in
   let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
   let sigma    = project gl in 
@@ -1014,7 +1019,15 @@ let general_case_analysis (c,lbindc) gl =
   else Indrec.make_case_gen in
   let elim     = case env sigma mind sort in 
   general_elim (c,lbindc) (elim,NoBindings) gl
-    
+
+let general_case_analysis (c,lbindc as cx) =
+  match kind_of_term c with
+    | Var id when lbindc = NoBindings ->
+	tclTHEN (tclTRY (intros_until_id id))
+	(general_case_analysis_in_context cx)
+    | _ ->
+	general_case_analysis_in_context cx
+
 let simplest_case c = general_case_analysis (c,NoBindings)
 
 (*****************************)
@@ -1095,12 +1108,14 @@ let rec first_name_buggy = function
   | IntroWildcard -> None
   | IntroIdentifier id -> Some id
 
-let induct_discharge statuslists destopt avoid' (avoid,ra) names gl =
+type elim_arg_kind = RecArg | IndArg | OtherArg
+
+let induct_discharge statuslists destopt avoid' (avoid,ra) (names,force,rnames) gl =
   let avoid = avoid @ avoid' in
   let (lstatus,rstatus) = statuslists in
   let tophyp = ref None in
   let rec peel_tac ra names gl = match ra with
-    | (false,recvarname) :: (true,hyprecname) :: ra' ->
+    | (RecArg,recvarname) :: (IndArg,hyprecname) :: ra' ->
         let recpat,hyprec,names = match names with
           | [] ->
               (IntroIdentifier (fresh_id avoid recvarname gl), 
@@ -1114,15 +1129,53 @@ let induct_discharge statuslists destopt avoid' (avoid,ra) names gl =
           | pat1::pat2::names -> (pat1,pat2,names) in
 	(* This is buggy for intro-or-patterns with different first hypnames *)
 	if !tophyp=None then tophyp := first_name_buggy hyprec;
+	rnames := !rnames @ [recpat; hyprec];
         tclTHENLIST
 	  [ intros_pattern destopt [recpat];
 	    intros_pattern None [hyprec];
 	    peel_tac ra' names ] gl
-    | (true,_) :: _ -> anomaly "TODO: non canonical inductive schema"
-    | (false,_) :: ra' ->
+    | (IndArg,hyprecname) :: ra' ->
+	(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
+        let pat,names = match names with
+          | [] -> IntroIdentifier (fresh_id avoid hyprecname gl), []
+	  | pat::names -> pat,names in
+	rnames := !rnames @ [pat];
+	tclTHEN (intros_pattern destopt [pat]) (peel_tac ra' names) gl
+    | (RecArg,recvarname) :: ra' ->
+        let introtac,names = match names with
+          | [] -> 
+	      let i = 
+		if !Options.v7 then IntroAvoid avoid 
+		else IntroMustBe (fresh_id avoid recvarname gl)
+	      in
+	      (* For translator *)
+	      let id = fresh_id avoid (default_id gl
+		(match kind_of_term (pf_concl gl) with
+		  | Prod (name,t,_) -> (name,None,t)
+		  | LetIn (name,b,t,_) -> (name,Some b,t) 
+		  | _ -> assert false)) gl in
+	      if Options.do_translate() & id <> fresh_id avoid recvarname gl 
+	      then force := true;
+	      rnames := !rnames @ [IntroIdentifier id];
+	      intro_gen i destopt false, []
+          | pat::names ->
+	      rnames := !rnames @ [pat];
+	      intros_pattern destopt [pat],names in
+	tclTHEN introtac (peel_tac ra' names) gl
+    | (OtherArg,_) :: ra' ->
         let introtac,names = match names with
-          | [] -> intro_gen (IntroAvoid avoid) destopt false, []
-          | pat::names -> intros_pattern destopt [pat],names in
+          | [] -> 
+	      (* For translator *)
+	      let id = fresh_id avoid (default_id gl
+		(match kind_of_term (pf_concl gl) with
+		  | Prod (name,t,_) -> (name,None,t)
+		  | LetIn (name,b,t,_) -> (name,Some b,t) 
+		  | _ -> assert false)) gl in
+	      rnames := !rnames @ [IntroIdentifier id];
+	      intro_gen (IntroAvoid avoid) destopt false, []
+          | pat::names ->
+	      rnames := !rnames @ [pat];
+	      intros_pattern destopt [pat],names in
 	tclTHEN introtac (peel_tac ra' names) gl
     | [] ->
         check_unused_names names;
@@ -1345,42 +1398,6 @@ let is_indhyp p n t =
     | Rel k when p < k & k <= p + n -> true
     | _ -> false
 
-(*
-(* We check that the eliminator has been build by Coq (usual *)
-(* eliminator _ind, _rec or _rect, or eliminator built by Scheme) *)
-let compute_elim_signature_and_roughly_check elimt mind names_info =
-  let (mib,mip) = Global.lookup_inductive mind in
-  let lra = dest_subterms mip.mind_recargs in
-  let nconstr = Array.length mip.mind_consnames in
-  let _,elimt2 = decompose_prod_n mip.mind_nparams elimt in
-  let n = nb_prod elimt2 in
-  let npred = n - nconstr - mip.mind_nrealargs - 1 in
-  let rec check_branch p c ra = match kind_of_term c, ra with
-    | Prod (_,_,c), r :: ra' ->
-	(match dest_recarg r, kind_of_term c with
-	   | Mrec i, Prod (_,t,c) when is_indhyp (p+1) npred t ->
-	       false::true::(check_branch (p+2) c ra')
-	   | _ -> false::(check_branch (p+1) c ra'))
-    | LetIn (_,_,_,c), ra' -> false::(check_branch (p+1) c ra)
-    | _, [] -> []
-    | _ ->
-	error"Not a recursive eliminator: some constructor argument is lacking"
-  in
-  let rec check_elim c n =
-    if n = nconstr then []
-    else match kind_of_term c with
-    | Prod (_,t,c) ->
-	let l = check_branch n t lra.(n) in
-	let p = List.fold_left (fun n b -> if b then n+1 else n) 0 l in
-	let recvarname, hyprecname, avoid = 
-	  make_up_names p (IndRef mind) names_info in
-	let namesign = List.map (fun b -> (b,if b then hyprecname else recvarname)) l in
-	(avoid,namesign) :: (check_elim c (n+1))
-    | _ -> error "Not an eliminator: some constructor case is lacking" in
-  let _,elimt3 = decompose_prod_n npred elimt2 in
-  mip.mind_nparams, IndRef mind, Array.of_list (check_elim elimt3 0)
-*)
-
 let chop_context n l = 
   let rec chop_aux acc = function
     | n, (_,Some _,_ as h :: t) -> chop_aux (h::acc) (n, t)
@@ -1394,6 +1411,8 @@ let error_ind_scheme s =
   let s = if s <> "" then s^" " else s in
   error ("Cannot recognise "^s^"an induction schema")
 
+(* Check that the elimination scheme has a form similar to the 
+   elimination schemes built by Coq *)
 let compute_elim_signature elimt names_info =
   let nparams = ref 0 in
   let hyps,ccl = decompose_prod_assum elimt in
@@ -1419,29 +1438,33 @@ let compute_elim_signature elimt names_info =
   | (na,None,t)::l when isSort (snd (decompose_prod_assum t)) ->
       check_elim (npred+1) l
   | l ->
-    let is_pred n c = match kind_of_term (fst (decompose_app c)) with
-    | Rel q when n < q & q <= n+npred -> true
-    | _ -> false in
+    let is_pred n c = 
+      let hd = fst (decompose_app c) in match kind_of_term hd with
+    | Rel q when n < q & q <= n+npred -> IndArg
+    | _ when hd = indhd -> RecArg
+    | _ -> OtherArg in
     let rec check_branch p c = match kind_of_term c with
     | Prod (_,t,c) -> is_pred p t :: check_branch (p+1) c
-    | LetIn (_,_,_,c) -> false :: check_branch (p+1) c
-    | App (f,_) when is_pred p f -> []
-    | _ when is_pred p c -> []
+    | LetIn (_,_,_,c) -> OtherArg :: check_branch (p+1) c
+(*    | App (f,_) when is_pred p f = IndArg -> []*)
+    | _ when is_pred p c = IndArg -> []
     | _ -> raise Exit in 
     let rec find_branches p = function
     | (_,None,t)::brs ->
 	(match try Some (check_branch p t) with Exit -> None with
 	 | Some l ->
-	     let n = List.fold_left (fun n b -> if b then n+1 else n) 0 l in
+	     let n = List.fold_left
+	       (fun n b -> if (!Options.v7 & b=IndArg) or
+		 (not !Options.v7 & b=RecArg) then n+1 else n) 0 l in
              let recvarname, hyprecname, avoid = make_up_names n indt names_info in
 	     let namesign = List.map
-	       (fun b -> (b,if b then hyprecname else recvarname)) l in
+	       (fun b -> (b,if b=IndArg then hyprecname else recvarname)) l in
 	     (avoid,namesign) :: find_branches (p+1) brs
 	 | None -> error_ind_scheme "the branches of")
     | (_,Some _,_)::_ -> error_ind_scheme "the branches of"
     | [] ->
 	(* Check again conclusion *)
-	let ccl_arg_ok = (is_pred (p + List.length realargs + 1) f) in
+	let ccl_arg_ok = is_pred (p + List.length realargs + 1) f = IndArg in
 	let ind_is_ok = 
 	  list_lastn nrealargs indargs = extended_rel_list 0 realargs in
 	if not (ccl_arg_ok & ind_is_ok) then
@@ -1467,7 +1490,7 @@ let find_elim_signature isrec style elim hyp0 gl =
   let nparams,indref,indsign = compute_elim_signature elimt name_info in
   (elimc,elimt,nparams,indref,indsign)
 
-let induction_from_context isrec elim_info hyp0 names gl =
+let induction_from_context isrec elim_info hyp0 (names,b_rnames) gl =
   (*test suivant sans doute inutile car refait par le letin_tac*)
   if List.mem hyp0 (ids_of_named_context (Global.named_context())) then
     errorlabstrm "induction" 
@@ -1480,6 +1503,12 @@ let induction_from_context isrec elim_info hyp0 names gl =
   let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars env in
   let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
   let names = compute_induction_names (Array.length indsign) names in
+  (* For translator *)
+  let names' = Array.map ref (Array.make (Array.length indsign) []) in
+  let b = ref false in
+  b_rnames := (b,Array.to_list names')::!b_rnames;
+  let names = array_map2 (fun n n' -> (n,b,n')) names names' in
+  (* End translator *)
   let dephyps = List.map (fun (id,_,_) -> id) deps in
   let args =
     List.fold_left
@@ -1549,16 +1578,22 @@ let raw_induct s = tclTHEN (intros_until_id s) (tclLAST_HYP simplest_elim)
 let raw_induct_nodep n = tclTHEN (intros_until_n n) (tclLAST_HYP simplest_elim)
 
 (* This was Induction in 6.3 (hybrid form) *)
-let induction_from_context_old_style hyp gl =
+let induction_from_context_old_style hyp b_ids gl =
   let elim_info = find_elim_signature true true None hyp gl in
-  (induction_from_context true elim_info hyp []) gl
-let simple_induct_id hyp =
-  tclORELSE (raw_induct hyp) (induction_from_context_old_style hyp)
+  let x = induction_from_context true elim_info hyp ([],b_ids) gl in
+  (* For translator *) fst (List.hd !b_ids) := true;
+  x
+
+let simple_induct_id hyp b_ids =
+  if !Options.v7 then
+    tclORELSE (raw_induct hyp) (induction_from_context_old_style hyp b_ids)
+  else
+    raw_induct hyp
 let simple_induct_nodep = raw_induct_nodep
 
 let simple_induct = function
-  | NamedHyp id -> simple_induct_id id
-  | AnonHyp n -> simple_induct_nodep n
+  | NamedHyp id,b_ids -> simple_induct_id id b_ids
+  | AnonHyp n,_ -> simple_induct_nodep n
 
 (* Destruction tactics *)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 90cb174839..f5c7619947 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -171,12 +171,13 @@ val elim          : constr with_bindings -> constr with_bindings option -> tacti
 val general_elim_in : identifier -> constr * constr bindings ->
                       constr * constr bindings -> tactic
 
-val simple_induct     : quantified_hypothesis -> tactic
+val simple_induct     : quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref -> tactic
 val general_elim_in : identifier -> constr * constr bindings ->
                       constr * constr bindings -> tactic
 
 val new_induct : constr induction_arg -> constr with_bindings option ->
-  intro_pattern_expr list list -> tactic
+  case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+  -> tactic
 
 (*s Case analysis tactics. *)
 
@@ -185,7 +186,8 @@ val simplest_case         : constr -> tactic
 
 val simple_destruct          : quantified_hypothesis -> tactic
 val new_destruct : constr induction_arg -> constr with_bindings option ->
-  intro_pattern_expr list list -> tactic
+  case_intro_pattern_expr * (bool ref * intro_pattern_expr list ref list) list ref
+  -> tactic
 
 (*s Eliminations giving the type instead of the proof. *)