From d3c49a6e536006ff121f01303ddc0a43b4c90e23 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 30 Dec 2008 18:31:14 +0000 Subject: - 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 --- contrib/jprover/jprover.ml4 | 11 +++++---- lib/util.ml | 7 ++---- tactics/elim.ml | 2 +- tactics/hipattern.ml4 | 56 ++++++++++++++++++++++++++++++++------------- tactics/hipattern.mli | 3 +++ tactics/tauto.ml4 | 11 +-------- 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 -- cgit v1.2.3