- Fixed bugs and compatibilities issues in

  match_conjunction/match_disjunction/array_for_all_i
- Finally activate fine-tuned unfolding of iff in tauto: it breaks at
  only one place in the user contribs (FSetAVL_dep.v).



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

6 files changed, 53 insertions, 37 deletions

diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4
index 5fd763c36..aadeb1a37 100644
--- a/contrib/jprover/jprover.ml4
+++ b/contrib/jprover/jprover.ml4
@@ -87,7 +87,9 @@ let dest_coq_and ct =
             end
       | None -> jp_error "dest_coq_and"
 
-let is_coq_or = HP.is_disjunction
+let is_coq_or ct =
+  HP.is_disjunction ~strict:true ct
+  && List.length (snd (TR.decompose_app ct)) = 2
 
 (* return two subterms *)
 let dest_coq_or ct =
@@ -170,7 +172,7 @@ let sAPP ct t =
 
 
 let is_coq_exists ct =
-  if not (HP.is_conjunction ct) then false
+  if not (HP.is_conjunction ~strict:true ct) then false
   else let (hdapp,args) = TR.decompose_app ct in
      match args with
       | _::la::[] ->
@@ -203,9 +205,8 @@ let dest_coq_exists ct =
 
 
 let is_coq_and ct =
-  if (HP.is_conjunction ct) && not (is_coq_exists ct)
-  && not (is_coq_true ct) then true
-  else false
+  (HP.is_conjunction ~strict:true ct)
+  && List.length (snd (TR.decompose_app ct)) = 2
 
 
 (* Parsing modules: *)
diff --git a/lib/util.ml b/lib/util.ml
index b7aa1fc0e..6803412fd 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -947,11 +947,8 @@ let array_for_all4 f v1 v2 v3 v4 =
     allrec (pred lv1) 
 
 let array_for_all_i f i v = 
-  let rec allrec i = function
-    | -1 -> true
-    | n -> (f i v.(n)) && (allrec (i-1) (n-1))
-  in 
-  allrec i ((Array.length v)-1) 
+  let rec allrec i n = n = Array.length v || f i v.(n) && allrec (i+1) (n+1) in 
+  allrec i 0
 
 let array_hd v = 
   match Array.length v with
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 2601cd4c5..ae6e486e2 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -128,7 +128,7 @@ let decompose_nonrec c gls =
 
 let decompose_and c gls = 
   general_decompose 
-    (fun (_,t) -> is_conjunction t)
+    (fun (_,t) -> is_record t)
     c gls
 
 let decompose_or c gls = 
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 769681155..9fb4becda 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -81,7 +81,9 @@ let has_nodep_prod = has_nodep_prod_after 0
    it is strict if it has the form 
    "Inductive I A1 ... An := C (_:A1) ... (_:An)" *)
 
-let match_with_conjunction ?(strict=false) t =
+(* style: None = record; Some false = conjunction; Some true = strict conj *)
+
+let match_with_one_constructor style t =
   let (hdapp,args) = decompose_app t in 
   match kind_of_term hdapp with
   | Ind ind -> 
@@ -90,29 +92,52 @@ let match_with_conjunction ?(strict=false) t =
 	&& (not (mis_is_recursive (ind,mib,mip)))
         && (mip.mind_nrealargs = 0)
       then
-	let is_nth_argument n (_,b,c) = b=None && c=mkRel(n+mib.mind_nparams) in
-	if strict &&
-	  list_for_all_i is_nth_argument 1 
-	    (fst (decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))
-	then
-	  Some (hdapp,args)
+	if style = Some true (* strict conjunction *) then
+	  let ctx = 
+	    fst (decompose_prod_assum (snd 
+	      (decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))) in
+	  if 
+	    List.for_all
+	      (fun (_,b,c) -> b=None && c = mkRel mib.mind_nparams) ctx
+	  then
+	    Some (hdapp,args)
+	  else None
 	else
 	  let ctyp = prod_applist mip.mind_nf_lc.(0) args in
 	  let cargs = List.map pi3 (fst (decompose_prod_assum ctyp)) in
-	  if has_nodep_prod ctyp then
+	  if style <> Some false || has_nodep_prod ctyp then
+	    (* Record or non strict conjunction *)
 	    Some (hdapp,List.rev cargs)
-	  else None
-      else None
+	  else
+	      None
+      else
+	None
   | _ -> None
 
+let match_with_conjunction ?(strict=false) t =
+  match_with_one_constructor (Some strict) t
+
+let match_with_record t = 
+  match_with_one_constructor None t
+
 let is_conjunction ?(strict=false) t =
   op2bool (match_with_conjunction ~strict t)
 
+let is_record t =
+  op2bool (match_with_record t)
+
+
 (* A general disjunction type is a non-recursive with-no-indices inductive 
    type with of which all constructors have a single argument;
    it is strict if it has the form 
    "Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *)
 
+let test_strict_disjunction n lc =
+  array_for_all_i (fun i c ->
+    match fst (decompose_prod_assum (snd (decompose_prod_n_assum n c))) with
+    | [_,None,c] -> c = mkRel (n - i)
+    | _ -> false) 0 lc
+
 let match_with_disjunction ?(strict=false) t =
   let (hdapp,args) = decompose_app t in 
   match kind_of_term hdapp with
@@ -122,12 +147,11 @@ let match_with_disjunction ?(strict=false) t =
       if array_for_all (fun ar -> ar = 1) car &&
 	not (mis_is_recursive (ind,mib,mip))
       then
-	if strict &
-	  array_for_all_i (fun i c -> 
-	    snd (decompose_prod_n_assum mib.mind_nparams c) = mkRel i) 1
-	  mip.mind_nf_lc
-	then
-	  Some (hdapp,args)
+	if strict then
+	  if test_strict_disjunction mib.mind_nparams mip.mind_nf_lc then
+	    Some (hdapp,args)
+	  else
+	    None
 	else
 	  let cargs =
 	    Array.map (fun ar -> pi2 (destProd (prod_applist ar args)))
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index b2e25b42d..9125e14ec 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -58,6 +58,9 @@ val is_disjunction         : ?strict:bool -> testing_function
 val match_with_conjunction : ?strict:bool -> (constr * constr list) matching_function
 val is_conjunction         : ?strict:bool -> testing_function 
 
+val match_with_record      : (constr * constr list) matching_function
+val is_record              : testing_function 
+
 val match_with_empty_type  : constr matching_function
 val is_empty_type          : testing_function 
 
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 1c75059b8..f7713f015 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -235,17 +235,8 @@ let rec tauto_intuit t_reduce solver ist =
     $t_solver
    ) >>
 
-  (* The unfolding of "iff" below is a priori too strong since it
-     reduces all occurrences in subterms even if not necessary to do
-     so. However we cannot renounce to them (even with iff dealt with
-     in "simplif") w/o breaking some intro naming. This is because, a
-     "and" or an "iff" can arrive in the scope of an inductive type,
-     say "{x:A|P x}" and "case"ing on a such an hypothesis will name P
-     x "a" or "i" depending on whether "P" is an "and" or a "iff".
-     (idem for "not" if "simplif" has a primitive treatment *)
-
 let reduction_not _ist =
- <:tactic< unfold Coq.Init.Logic.not, Coq.Init.Logic.iff in * >>
+ <:tactic< unfold Coq.Init.Logic.not in * >>
 
 let t_reduction_not = tacticIn reduction_not