Nettoyage reduce_to_ind et one_step_reduce

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

8 files changed, 86 insertions, 79 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 7bf6441f73..d56f92cfa5 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -90,11 +90,14 @@ let resolve_with_bindings_tac  (c,lbind) gl =
   let clause = make_clenv_binding_apply wc (c,t) lbind in 
   res_pf kONT clause gl
 
+(*
+let pf_one_step_reduce = pf_reduce Tacred.one_step_reduce
+
 let reduce_to_mind gl t = 
   let rec elimrec t l =
     let c, args = whd_stack t in
     match kind_of_term c, args with
-    | (IsMutInd _,_) -> (c,Environ.it_mkProd_or_LetIn t l)
+    | (IsMutInd ind,_) -> (ind,Environ.it_mkProd_or_LetIn t l)
     | (IsConst _,_) -> 
 	(try 
 	   let t' = pf_nf_betaiota gl (pf_one_step_reduce gl t) in elimrec t' l
@@ -117,12 +120,14 @@ let reduce_to_mind gl t =
     | _ -> error "Not an inductive product"
   in 
   elimrec t []
+*)
+
+let reduce_to_mind = pf_reduce_to_quantified_ind
 
 let constructor_tac nconstropt i lbind gl = 
   let cl = pf_concl gl in
   let (mind, redcl) = reduce_to_mind gl cl in
-  let ((x0,x1),args) as mindspec= destMutInd mind in
-  let nconstr = Global.mind_nconstr mindspec
+  let nconstr = Global.mind_nconstr mind
   and sigma = project gl in
   (match nconstropt with 
      | Some expnconstr -> 
@@ -130,7 +135,7 @@ let constructor_tac nconstropt i lbind gl =
            error "Not the expected number of constructors"
      | _ -> ());
   if i > nconstr then error "Not enough Constructors";
-  let c = mkMutConstruct (((x0,x1),i),args) in 
+  let c = mkMutConstruct (ith_constructor_of_inductive mind i) in 
   let resolve_tac = resolve_with_bindings_tac (c,lbind) in
   (tclTHEN (tclTHEN (change_in_concl redcl) intros) resolve_tac) gl
 
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 16bd2b9c74..ab09389859 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -698,12 +698,14 @@ let reduction_of_redexp = function
 
 (* Used in several tactics. *)
 
+exception NotStepReducible
+
 let one_step_reduce env sigma c = 
   let rec redrec (x, largs as s) =
     match kind_of_term x with
       | IsLambda (n,t,c)  ->
           (match decomp_stack largs with
-             | None      -> error "Not reducible 1"
+             | None      -> raise NotStepReducible
              | Some (a,rest) -> (subst1 a c, rest))
       | IsApp (f,cl) -> redrec (f, append_stack cl largs)
       | IsLetIn (_,f,_,cl) -> (subst1 f cl,largs)
@@ -711,11 +713,11 @@ let one_step_reduce env sigma c =
           (try
 	     (special_red_case env (whd_betadeltaiota_state env sigma)
 	       (ci,p,c,lf), largs)
-           with Redelimination -> error "Not reducible 2")
+           with Redelimination -> raise NotStepReducible)
       | IsFix fix ->
 	  (match reduce_fix (whd_betadeltaiota_state env sigma) fix largs with
              | Reduced s' -> s'
-	     | NotReducible -> error "Not reducible 3")
+	     | NotReducible -> raise NotStepReducible)
       | IsCast (c,_) -> redrec (c,largs)
       | _ when isEvalRef x ->
 	  let ref = destEvalRef x in
@@ -724,32 +726,35 @@ let one_step_reduce env sigma c =
            with Redelimination ->
 	     match reference_opt_value sigma env ref with
 	       | Some d -> d, largs
-	       | None -> error "Not reductible 1")
+	       | None -> raise NotStepReducible)
 
-      | _ -> error "Not reducible 3"
+      | _ -> raise NotStepReducible
   in 
   app_stack (redrec (c, empty_stack))
 
 (* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name
    return name, B and t' *)
 
-let reduce_to_mind env sigma t = 
+let reduce_to_ind_gen allow_product env sigma t = 
   let rec elimrec env t l = 
     let c, _ = whd_stack t in
     match kind_of_term c with
-      | IsMutInd (mind,args) -> ((mind,args),t,it_mkProd_or_LetIn t l)
+      | IsMutInd (mind,args) -> ((mind,args),it_mkProd_or_LetIn t l)
       | IsProd (n,ty,t') ->
-	  elimrec (push_rel_assum (n,t) env) t' ((n,None,ty)::l)
-      | _ -> 
+	  if allow_product then
+	    elimrec (push_rel_assum (n,t) env) t' ((n,None,ty)::l)
+	  else
+	     errorlabstrm "tactics__reduce_to_mind"
+	       [< 'sTR"Not an inductive definition" >]
+      | _ ->
           (try 
 	     let t' = nf_betaiota (one_step_reduce env sigma t) in 
 	     elimrec env t' l
-           with UserError _ -> errorlabstrm "tactics__reduce_to_mind"
-               [< 'sTR"Not an inductive product." >])
- in
- elimrec env t []
-
-let reduce_to_ind env sigma t =
-  let ((ind_sp,_),redt,c) = reduce_to_mind env sigma t in 
-  (Declare.path_of_inductive_path ind_sp, redt, c)
+           with NotStepReducible ->
+	     errorlabstrm "tactics__reduce_to_mind"
+               [< 'sTR"Not an inductive product" >])
+  in
+  elimrec env t []
 
+let reduce_to_quantified_ind x = reduce_to_ind_gen true x
+let reduce_to_atomic_ind x = reduce_to_ind_gen false x
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index c75f337949..fc9e55e303 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -48,13 +48,15 @@ val cbv_norm_flags : Closure.flags -> 'a reduction_function
   val cbv_betadeltaiota : 'a reduction_function
   val compute : 'a reduction_function  (* = [cbv_betadeltaiota] *)
 
-val one_step_reduce : 'a reduction_function
+(* [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)]
+   with [I] an inductive definition;
+   returns [I] and [t'] or fails with a user error *)
+val reduce_to_atomic_ind : env -> 'a evar_map -> types -> inductive * types
 
-val reduce_to_mind : 
-  env -> 'a evar_map -> constr -> inductive * constr * constr
-
-val reduce_to_ind : 
-  env -> 'a evar_map -> constr -> section_path * constr * constr
+(* [reduce_to_quantified_ind env sigma t] puts [t] in the form
+   [t'=(x1:A1)..(xn:An)(I args)] with [I] an inductive definition;
+   returns [I] and [t'] or fails with a user error *)
+val reduce_to_quantified_ind : env -> 'a evar_map -> types -> inductive * types
 
 type red_expr =
   | Red of bool    (* raise Redelimination if true otherwise UserError *)
@@ -67,4 +69,3 @@ type red_expr =
   | Pattern of (int list * constr * constr) list
 
 val reduction_of_redexp : red_expr -> 'a reduction_function
-
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 69697c809f..d2f12d3523 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -108,9 +108,8 @@ let pf_type_of                   = pf_reduce type_of
 let pf_conv_x                   = pf_reduce is_conv
 let pf_conv_x_leq               = pf_reduce is_conv_leq
 let pf_const_value              = pf_reduce (fun env _ -> constant_value env)
-let pf_one_step_reduce          = pf_reduce one_step_reduce
-let pf_reduce_to_mind           = pf_reduce reduce_to_mind
-let pf_reduce_to_ind            = pf_reduce reduce_to_ind
+let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
+let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
 let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_type_of gls)
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 721f847243..930588fcb8 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -73,11 +73,9 @@ val pf_hnf_constr              : goal sigma -> constr -> constr
 val pf_red_product             : goal sigma -> constr -> constr
 val pf_nf                      : goal sigma -> constr -> constr
 val pf_nf_betaiota             : goal sigma -> constr -> constr
-val pf_one_step_reduce         : goal sigma -> constr -> constr
-val pf_reduce_to_mind : goal sigma -> constr -> inductive * constr * constr
-val pf_reduce_to_ind  :
-  goal sigma  -> constr -> section_path * constr * constr
-val pf_compute        : goal sigma -> constr -> constr
+val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types
+val pf_reduce_to_atomic_ind     : goal sigma -> types -> inductive * types
+val pf_compute                 : goal sigma -> constr -> constr
 val pf_unfoldn    : (int list * Closure.evaluable_global_reference) list
         -> goal sigma -> constr -> constr
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9d623fe51e..c0584cd98b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1264,15 +1264,9 @@ let sub_term_with_unif cref ceq =
 	    
 (*The Rewrite in tactic*)
 let general_rewrite_in lft2rgt id (c,lb) gls =
-  let typ_id =
-    (try
-       let (_,ty) = lookup_named id (pf_env gls) in ty
-     with Not_found -> 
-       errorlabstrm "general_rewrite_in" 
-	 [< 'sTR"No such hypothesis : "; pr_id id >])
-  in
+  let typ_id = pf_get_hyp_typ gls id in
   let (wc,_) = startWalk gls
-  and (_,_,t) = reduce_to_ind (pf_env gls) (project gls) (pf_type_of gls c) in
+  and (_,t) = pf_reduce_to_quantified_ind gls (pf_type_of gls c) in
   let ctype = type_clenv_binding wc (c,t) lb in
   match (match_with_equation ctype) with
     | None -> error "The term provided does not end with an equation" 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 9d8f07d78f..234c9dcd1d 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -258,6 +258,16 @@ type branch_assumptions = {
  * (previously) defined with the same name in Tactics.ml. 
  *  --Eduardo (11/8/97) *)
 
+(* This function reduces less than Tacred.reduce_to_quantified_ind (no
+   beta/iota reduction if not induced by a constant), but since it is called
+   with types coming from pf_type_of which betaiota reduces, it should
+   behaves the same.  Moreover, the env in the call to pf_one_step_reduce
+   is not synchronous with the local environment (HH 9/9/01)
+
+   Let's try to replace it by pf_reduce_to_quantified_ind
+
+let pf_one_step_reduce = pf_reduce one_step_reduce
+
 let reduce_to_ind_goal gl t = 
   let rec elimrec t =
     let c,args = decomp_app t in
@@ -275,6 +285,9 @@ let reduce_to_ind_goal gl t =
       | _ -> error "Not an inductive product"
   in 
   elimrec t
+*)
+
+let reduce_to_ind_goal = pf_reduce_to_quantified_ind
 
 let case_sign ity i = 
   let rec analrec acc = function 
@@ -311,7 +324,7 @@ let last_arg c = match kind_of_term c with
 
 let general_elim_then_using 
   elim elim_sign_fun tac predicate (indbindings,elimbindings) c gl =
-  let ((ity,_,_),t) = reduce_to_ind_goal gl (pf_type_of gl c) in
+  let (ity,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   (* applying elimination_scheme just a little modified *)
   let (wc,kONT)  = startWalk gl in
   let indclause  = mk_clenv_from wc (c,t) in
@@ -360,8 +373,8 @@ let general_elim_then_using
 
 
 let elimination_then_using tac predicate (indbindings,elimbindings) c gl = 
-  let ((ity,path_name,_),t) = reduce_to_ind_goal gl (pf_type_of gl c) in
-  let elim = lookup_eliminator (pf_env gl) path_name (sort_of_goal gl) in
+  let (ind,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
+  let elim = lookup_eliminator (pf_env gl) ind (sort_of_goal gl) in
   general_elim_then_using
     elim elim_sign tac predicate (indbindings,elimbindings) c gl
 
@@ -371,7 +384,7 @@ let simple_elimination_then tac = elimination_then tac ([],[])
 
 let case_then_using tac predicate (indbindings,elimbindings) c gl =
   (* finding the case combinator *)
-  let ((ity,_,_),t) = reduce_to_ind_goal gl (pf_type_of gl c) in
+  let (ity,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   let sigma = project gl in 
   let sort  = sort_of_goal gl  in
   let elim  = Indrec.make_case_gen (pf_env gl) sigma ity sort in  
@@ -380,7 +393,7 @@ let case_then_using tac predicate (indbindings,elimbindings) c gl =
 
 let case_nodep_then_using tac predicate (indbindings,elimbindings) c gl =
   (* finding the case combinator *)
-  let ((ity,_,_),t) = reduce_to_ind_goal gl (pf_type_of gl c) in
+  let (ity,t) = reduce_to_ind_goal gl (pf_type_of gl c) in
   let sigma = project gl in 
   let sort  = sort_of_goal gl  in
   let elim  = Indrec.make_case_nodep (pf_env gl) sigma ity sort in  
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 12b41b6027..a7f2fb9766 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -770,13 +770,12 @@ let letin_tac with_eq name c occs gl =
 	error ("The variable "^(string_of_id x)^" is already declared") in
   let (depdecls,marks,ccl)= letin_abstract id c occs gl in 
   let t = pf_type_of gl c in
-  let heq = next_ident_away (id_of_string "Heq") used_ids in
   let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in
   let args = instance_from_named_context depdecls in
   let newcl =
     if with_eq then
       mkNamedLetIn id c t tmpcl
-    else
+    else (* To fix : add c to args, or use LetIn and clear the body *)
       mkNamedProd id t tmpcl
   in
   let lastlhyp = if marks=[] then None else snd (List.hd marks) in
@@ -947,7 +946,7 @@ let dyn_move_dep = function
 
 let constructor_checking_bound  boundopt i lbind gl =
   let cl = pf_concl gl in 
-  let (mind,_,redcl) = reduce_to_mind (pf_env gl) (project gl) cl in 
+  let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in 
   let nconstr = mis_nconstr (Global.lookup_mind_specif mind) 
   and sigma   = project gl in
   if i=0 then error "The constructors are numbered starting from 1";
@@ -966,7 +965,7 @@ let one_constructor i = (constructor_checking_bound None i)
 
 let any_constructor gl = 
   let cl = pf_concl gl in 
-  let (mind,_,redcl) = reduce_to_mind (pf_env gl) (project gl) cl in
+  let (mind,redcl) = pf_reduce_to_quantified_ind gl cl in
   let nconstr = mis_nconstr (Global.lookup_mind_specif mind)
   and sigma   = project gl in
   if nconstr = 0 then error "The type has no constructors";
@@ -1047,9 +1046,7 @@ let type_clenv_binding wc (c,t) lbind =
 let general_elim (c,lbindc) (elimc,lbindelimc) gl = 
   let (wc,kONT)  = startWalk gl in
   let ct = pf_type_of gl c in
-  let t = try let (_,_,t)    = reduce_to_ind (pf_env gl) (project gl) ct in t 
-  with UserError _ -> ct
-  in
+  let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
   let indclause  = make_clenv_binding wc (c,t) lbindc  in
   let elimt      = w_type_of wc elimc in
   let elimclause = make_clenv_binding wc (elimc,elimt) lbindelimc in 
@@ -1060,12 +1057,12 @@ let general_elim (c,lbindc) (elimc,lbindelimc) gl =
 
 let default_elim (c,lbindc)  gl = 
   let env = pf_env gl in
-  let (path,_,t) = reduce_to_ind env (project gl) (pf_type_of gl c) in
+  let (ind,t) = reduce_to_quantified_ind env (project gl) (pf_type_of gl c) in
   let s = sort_of_goal gl in
   let elimc =
-    try lookup_eliminator env path s 
+    try lookup_eliminator env ind s 
     with Not_found -> 
-      let dir, base,k = repr_path path in
+      let dir, base,k = repr_path (path_of_inductive_path (fst ind)) in
       let id = make_elimination_ident base s in
       errorlabstrm "default_elim"
 	[< 'sTR "Cannot find the elimination combinator :";
@@ -1183,16 +1180,19 @@ let induct_discharge old_style mind statuslists cname destopt avoid ra gl =
 
 let atomize_param_of_ind hyp0 gl =
   let tmptyp0 = pf_get_hyp_typ gl hyp0 in
-  let (mind,indtyp,typ0) = pf_reduce_to_mind gl tmptyp0 in
+  let (mind,typ0) = pf_reduce_to_quantified_ind gl tmptyp0 in
   let mis = Global.lookup_mind_specif mind in
   let nparams = mis_nparams mis in
+  let prods, indtyp = decompose_prod typ0 in
   let argl = snd (decomp_app indtyp) in
   let params = list_firstn nparams argl in
   (* le gl est important pour ne pas préévaluer *)
   let rec atomize_one i avoid gl =
     if i<>nparams then
       let tmphyp0 = pf_get_hyp_typ gl hyp0 in
-      let (_,indtyp,_) = pf_reduce_to_mind gl tmptyp0 in
+      (* If argl <> [], we expect typ0 not to be quantified, in order to
+         avoid bound parameters... then we call pf_reduce_to_atomic_ind *)
+      let (_,indtyp) = pf_reduce_to_atomic_ind gl tmptyp0 in
       let argl = snd (decomp_app indtyp) in
       let c = List.nth argl (i-1) in
       match kind_of_term c with
@@ -1419,11 +1419,10 @@ let induction_from_context isrec style hyp0 gl =
       [< 'sTR "Cannot generalize a global variable" >];
   let tmptyp0 =	pf_get_hyp_typ gl hyp0 in
   let env = pf_env gl in
-  let ((ind_sp,_) as mind,indtyp,typ0) = pf_reduce_to_mind gl tmptyp0 in
-  let indvars = find_atomic_param_of_ind mind indtyp in
-  let mindpath = Declare.path_of_inductive_path ind_sp in
+  let (mind,typ0) = pf_reduce_to_quantified_ind gl tmptyp0 in
+  let indvars = find_atomic_param_of_ind mind (snd (decompose_prod typ0)) in
   let elimc =
-    if isrec then lookup_eliminator env mindpath (sort_of_goal gl)
+    if isrec then lookup_eliminator env mind (sort_of_goal gl)
     else Indrec.make_case_gen env (project gl) mind (sort_of_goal gl)
   in
   let elimt = pf_type_of gl elimc in
@@ -1532,7 +1531,7 @@ let dyn_old_induct = function
 
 let general_case_analysis (c,lbindc) gl =
   let env = pf_env gl in
-  let (mind,_,_) = reduce_to_mind env (project gl) (pf_type_of gl c) in
+  let (mind,_) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
   let sigma    = project gl in 
   let sort     = sort_of_goal gl in
   let elim     = Indrec.make_case_gen env sigma mind sort in 
@@ -1585,11 +1584,9 @@ let elim_scheme_type elim t gl =
     | _ -> anomaly "elim_scheme_type"
 
 let elim_type t gl =
-  let (path_name,tind,t) = reduce_to_ind (pf_env gl) (project gl) t in
-  let elimc = lookup_eliminator (pf_env gl) path_name (sort_of_goal gl) in
-  match kind_of_term t with 
-    | IsProd (_,_,_) -> error "Not an inductive definition"
-    | _              -> elim_scheme_type elimc tind gl
+  let (ind,t) = pf_reduce_to_atomic_ind gl t in
+  let elimc = lookup_eliminator (pf_env gl) ind (sort_of_goal gl) in
+  elim_scheme_type elimc t gl
 
 let dyn_elim_type = function
   | [Constr c]    -> elim_type c
@@ -1597,15 +1594,10 @@ let dyn_elim_type = function
   | l             -> bad_tactic_args "elim_type" l
 
 let case_type t gl =
+  let (ind,t) = pf_reduce_to_atomic_ind gl t in
   let env = pf_env gl in
-  let (mind,_,t) = reduce_to_mind env (project gl) t in  
-  match kind_of_term t with 
-    | IsProd (_,_,_) -> error "Not an inductive definition"
-    | _             -> 
-        let sigma = project gl in 
-        let sort  = sort_of_goal gl in
-        let elimc = Indrec.make_case_gen env sigma mind sort in 
-        elim_scheme_type elimc t gl
+  let elimc = Indrec.make_case_gen env (project gl) ind (sort_of_goal gl) in 
+  elim_scheme_type elimc t gl
 
 let dyn_case_type = function
   | [Constr c]    -> case_type c