Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui sont supposes sans dependances en les arguments des constructeurs

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

7 files changed, 82 insertions, 76 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0c9d9a66c..7657ce445 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1825,6 +1825,7 @@ let rec raw_of_pat tenv env = function
       let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
       let k = (snd (lookup_mind_specif (Global.env()) ind)).Declarations.mind_nrealargs in
       Detyping.detype_case false (raw_of_pat tenv env)(raw_of_eqn tenv env)
+	(fun _ _ -> false (* lazy: don't try to display pattern with "if" *))
 	tenv avoid ind cs typopt k tm bv
   | PCase _ -> error "Unsupported case-analysis while printing pattern"
   | PFix f -> Detyping.detype (false,tenv) [] env (mkFix f)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index d80bacbfb..0084fce65 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -142,6 +142,7 @@ type ml_case_error =
 
 exception NotInferable of ml_case_error
 
+
 let pred_case_ml env sigma isrec (IndType (indf,realargs)) (i,ft) =
   let pred =
     let (ind,params) = dest_ind_family indf in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 67cf0d388..9666008c3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -193,13 +193,23 @@ let lookup_index_as_renamed env t n =
     | _ -> None
   in lookup n 1 t
 
-let rec dont_use_args nargs c =
-  nargs = 0 or
-  match c with
-    | RLambda (_,Anonymous,_,c) -> dont_use_args (nargs - 1) c
-    | _ -> false
-
-let detype_case computable detype detype_eqn tenv avoid indsp st p k c bl =
+let is_nondep_branch c n =
+  try
+    let _,ccl = decompose_lam_n_assum n c in
+    noccur_between 1 n ccl
+  with _ -> (* Not eta-expanded or not reduced *)
+    false
+
+let extract_nondep_branches test c b n =
+  let rec strip n r = if n=0 then r else
+    match r with
+      | RLambda (_,_,_,t) -> strip (n-1) t
+      | RLetIn (_,_,_,t) -> strip (n-1) t
+      | _ -> assert false in
+  if test c n then Some (strip n b) else None
+
+let detype_case computable detype detype_eqn testdep
+    tenv avoid indsp st p k c bl =
   let synth_type = synthetize_type () in
   let tomatch = detype c in
 
@@ -262,7 +272,7 @@ let detype_case computable detype detype_eqn tenv avoid indsp st p k c bl =
   if tag = RegularStyle then
     RCases (dummy_loc,(pred,ref newpred),[tomatch,ref (alias,aliastyp)],eqnl)
   else
-    let bl = Array.map detype bl in
+    let bl' = Array.map detype bl in
     if not !Options.v7 && tag = LetStyle && aliastyp = None then
       let rec decomp_lam_force n avoid l p =
 	if n = 0 then (List.rev l,p) else
@@ -279,12 +289,16 @@ let detype_case computable detype detype_eqn tenv avoid indsp st p k c bl =
                   match p with
                     | RApp (loc,p,l) -> RApp (loc,p,l@[a])
                     | _ -> (RApp (dummy_loc,p,[a]))) in
-      let (nal,d) = decomp_lam_force consnargsl.(0) avoid [] bl.(0) in
+      let (nal,d) = decomp_lam_force consnargsl.(0) avoid [] bl'.(0) in
       RLetTuple (dummy_loc,nal,(alias,newpred),tomatch,d)
-    else if not !Options.v7 && tag = IfStyle && aliastyp = None
-      && array_for_all2 dont_use_args consnargsl bl then
-      RIf (dummy_loc,tomatch,(alias,newpred),bl.(0),bl.(1))
     else
+    let nondepbrs =
+      array_map3 (extract_nondep_branches testdep) bl bl' consnargsl in
+    if not !Options.v7 && tag = IfStyle && aliastyp = None
+      && array_for_all ((<>) None) nondepbrs then
+      RIf (dummy_loc,tomatch,(alias,newpred),
+           out_some nondepbrs.(0),out_some nondepbrs.(1))
+    else if !Options.v7 then
       let rec remove_type avoid args c =
 	match c,args with
           | RLambda (loc,na,t,c), _::args ->
@@ -303,8 +317,11 @@ let detype_case computable detype detype_eqn tenv avoid indsp st p k c bl =
               let avoid = name_fold (fun x l -> x::l) na avoid in
               RLetIn (dummy_loc,na,h,remove_type avoid args c)
           | c, [] -> c in
-      let bl = array_map2 (remove_type avoid) consnargs bl in
-      ROrderedCase (dummy_loc,tag,pred,tomatch,bl,ref None)
+      let bl' = array_map2 (remove_type avoid) consnargs bl' in
+      ROrderedCase (dummy_loc,tag,pred,tomatch,bl',ref None)
+    else
+      RCases(dummy_loc,(pred,ref newpred),[tomatch,ref (alias,aliastyp)],eqnl)
+
 
 let rec detype tenv avoid env t =
   match kind_of_term (collapse_appl t) with
@@ -347,6 +364,7 @@ let rec detype tenv avoid env t =
 	let ind = annot.ci_ind in
 	let st = annot.ci_pp_info.style in
 	detype_case comp (detype tenv avoid env) (detype_eqn tenv avoid env)
+	  is_nondep_branch
 	  (snd tenv) avoid ind st (Some p) annot.ci_pp_info.ind_nargs c bl
     | Fix (nvn,recdef) -> detype_fix tenv avoid env nvn recdef
     | CoFix (n,recdef) -> detype_cofix tenv avoid env n recdef
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 253e0f51c..7efaf4bbc 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -26,7 +26,7 @@ val detype : bool * env -> identifier list -> names_context -> constr ->
 val detype_case : 
   bool -> ('a -> rawconstr) ->
   (constructor -> int -> 'a -> loc * identifier list * cases_pattern list *
-    rawconstr) ->
+    rawconstr) -> ('a -> int -> bool) ->
     env -> identifier list -> inductive -> case_style ->
       'a option -> int -> 'a -> 'a array -> rawconstr
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a2ea06e4e..5e8a69e0e 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -628,73 +628,44 @@ let rec pretype tycon env isevars lvar = function
 	with Not_found ->
 	  let cloc = loc_of_rawconstr c in
 	  error_case_not_inductive_loc cloc env (evars_of isevars) cj in
+      let cstrs = get_constructors env indf in 
+      if Array.length cstrs <> 2 then
+        user_err_loc (loc,"",
+	  str "If is only for inductive types with two constructors");
+
       (* Make dependencies from arity signature impossible *)
       let arsgn,_ = get_arity env indf in
       let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in
-      let psign = (na,None,build_dependent_inductive env indf)::arsgn in
       let nar = List.length arsgn in
-      let p = 
-	match po with
+      let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+      let pred,p = match po with
 	| Some p ->
-            let env_p = push_rels psign env in
-            let pj = pretype_type empty_valcon env_p isevars lvar p in
+	    let env_p = push_rels psign env in
+            let pj = pretype_type empty_valcon env isevars lvar p in
             let ccl = nf_evar (evars_of isevars) pj.utj_val in
-	    it_mkLambda_or_LetIn ccl psign
-	| None ->
-            (* get type information from type of branches *)
-	    let expbr = Cases.branch_scheme env isevars false indf in
-	    try
-	      let fj = pretype (mk_tycon expbr.(0)) env isevars lvar b1 in
-	      let pred = 
-		Cases.pred_case_ml
-                  env (evars_of isevars) false indt (0,fj.uj_type) in
-	      if has_undefined_isevars isevars pred then 
-		raise Not_found
-	      else
-(*
-                let _ = option_app (the_conv_x_leq env isevars pred) tycon in
-*)
-                pred
-	    with Cases.NotInferable _ | Not_found ->
-	    try
-	      let fj = pretype (mk_tycon expbr.(1)) env isevars lvar b2 in
-	      let pred = 
-		Cases.pred_case_ml
-                  env (evars_of isevars) false indt (1,fj.uj_type) in
-	      if has_undefined_isevars isevars pred then 
-		raise Not_found
-	      else
-(*
-                let _ = option_app (the_conv_x_leq env isevars pred) tycon in
-*)
-                pred
-	    with Cases.NotInferable _ | Not_found ->
-            (* get type information from constraint *)
-            (* warning: if the constraint comes from an evar type, it *)
-            (* may be Type while Prop or Set would be expected *)
-	    match tycon with
-	      | Some pred ->
-		  let arsgn = make_arity_signature env true indf in
-                  let pred = lift (List.length arsgn) pred in
-  		  it_mkLambda_or_LetIn (nf_evar (evars_of isevars) pred) arsgn 
-	      | None ->
-                  let sigma = evars_of isevars in
-                  error_cant_find_case_type_loc loc env sigma cj.uj_val in
-      let (bty,rsty) =
-	Indrec.type_rec_branches false
-	  env (evars_of isevars) indt p cj.uj_val in
-      let _ = option_app (the_conv_x_leq env isevars rsty) tycon in
-      if Array.length bty <> 2 then
-        user_err_loc (loc,"",
-	  str "If is only for inductive types with two constructors");
-      let bj1 = pretype (mk_tycon bty.(0)) env isevars lvar b1 in
-      let bj2 = pretype (mk_tycon bty.(1)) env isevars lvar b2 in
+	    let pred = it_mkLambda_or_LetIn ccl psign in
+	    pred, lift (- nar) (beta_applist (pred,[cj.uj_val]))
+	| None -> 
+	    let p = match tycon with
+	    | Some ty -> ty
+	    | None -> new_isevar isevars env (loc,InternalHole) (new_Type ())
+	    in
+	    it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
+      let bj1 = pretype (Some p) env isevars lvar b1 in
+      let bj2 = pretype (Some p) env isevars lvar b2 in
+      let cargs1 = cstrs.(0).cs_args and cargs2 = cstrs.(1).cs_args in
+      let lb1 = lift (rel_context_length cargs1) bj1.uj_val in
+      let b1 = it_mkLambda_or_LetIn lb1 cargs1 in
+      let lb2 = lift (rel_context_length cargs2) bj2.uj_val in
+      let b2 = it_mkLambda_or_LetIn lb2 cargs2 in
+      let pred = nf_evar (evars_of isevars) pred in
+      let p = nf_evar (evars_of isevars) p in
       let v =
 	let mis,_ = dest_ind_family indf in
 	let ci = make_default_case_info env IfStyle mis in
-	mkCase (ci, p, cj.uj_val, [|bj1.uj_val;bj2.uj_val|])
+	mkCase (ci, pred, cj.uj_val, [|b1;b2|])
       in
-      { uj_val = v; uj_type = rsty }
+      { uj_val = v; uj_type = p }
 
   | ROrderedCase (loc,st,po,c,lf,x) ->
       let isrec = (st = MatchStyle) in
@@ -821,10 +792,25 @@ let rec pretype tycon env isevars lvar = function
                       let args = List.map (fun _ -> Anonymous) params @ nal in
 		      Some (dummy_loc,ind,args) in
                   (Some rtntyopt,(List.hd na,intyp)) in
-	    if st = IfStyle & snd indnalopt = None then
+	    let rawbranches =
+	      array_map3 (fun bj b cstr ->
+		let rec strip n r = if n=0 then r else
+		  match r with
+		    | RLambda (_,_,_,t) -> strip (n-1) t
+		    | RLetIn (_,_,_,t) -> strip (n-1) t
+		    | _ -> assert false in
+		let n = rel_context_length cstr.cs_args in
+		try
+		  let _,ccl = decompose_lam_n_assum n bj.uj_val in
+		  if noccur_between 1 n ccl then Some (strip n b) else None
+		with _ -> (* Not eta-expanded or not reduced *) None)
+		lfj lf (get_constructors env indf) in
+	    if st = IfStyle & snd indnalopt = None 
+	       & rawbranches.(0) <> None && rawbranches.(1) <> None then
 	      (* Translate into a "if ... then ... else" *)
 	      (* TODO: translate into a "if" even if po is dependent *)
-	      Some (RIf (loc,c,(fst indnalopt,rtntypopt),lf.(0),lf.(1)))
+	      Some (RIf (loc,c,(fst indnalopt,rtntypopt),
+	          out_some rawbranches.(0),out_some rawbranches.(1)))
 	    else
             let detype_eqn constr construct_nargs branch =
               let name_cons = function 
diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v
index 8a15e7624..2a0b2063d 100755
--- a/theories/Bool/DecBool.v
+++ b/theories/Bool/DecBool.v
@@ -11,7 +11,7 @@
 Set Implicit Arguments.
 
 Definition ifdec (A B:Prop) (C:Set) (H:{A} + {B}) (x y:C) : C :=
-  if H then fun _ => x else fun _ => y.
+  if H then x else y.
 
 
 Theorem ifdec_left :
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index 20f39e0ef..7671b25ff 100755
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -149,7 +149,7 @@ Hypothesis eqA_dec : forall a b:A, {a = b} + {a <> b}.
 Fixpoint mem (a:A) (l:list A) {struct l} : bool :=
   match l with
   | nil => false
-  | b :: m => if eqA_dec a b then fun H => true else fun H => mem a m
+  | b :: m => if eqA_dec a b then true else mem a m
   end.
 
 Hint Unfold In.