diff options
Diffstat (limited to 'tactics/hipattern.ml4')
| -rw-r--r-- | tactics/hipattern.ml4 | 135 |
1 files changed, 86 insertions, 49 deletions
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index c796eda90..769681155 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -15,6 +15,7 @@ open Util open Names open Nameops open Term +open Sign open Termops open Reductionops open Inductiveops @@ -64,48 +65,83 @@ let match_with_non_recursive_type t = let is_non_recursive_type t = op2bool (match_with_non_recursive_type t) -(* A general conjunction type is a non-recursive inductive type with - only one constructor. *) +(* Test dependencies *) -let match_with_conjunction_size t = - let (hdapp,args) = decompose_app t in - match kind_of_term hdapp with - | Ind ind -> - let (mib,mip) = Global.lookup_inductive ind in - if (Array.length mip.mind_consnames = 1) - && (not (mis_is_recursive (ind,mib,mip))) - && (mip.mind_nrealargs = 0) - then - Some (hdapp,args,mip.mind_consnrealdecls.(0)) - else - None - | _ -> None - -let match_with_conjunction t = - match match_with_conjunction_size t with - | Some (hd,args,n) -> Some (hd,args) - | None -> None +let rec has_nodep_prod_after n c = + match kind_of_term c with + | Prod (_,_,b) -> + ( n>0 || not (dependent (mkRel 1) b)) + && (has_nodep_prod_after (n-1) b) + | _ -> true + +let has_nodep_prod = has_nodep_prod_after 0 -let is_conjunction t = op2bool (match_with_conjunction t) - -(* A general disjunction type is a non-recursive inductive type all - whose constructors have a single argument. *) +(* A general conjunctive type is a non-recursive with-no-indices inductive + type with only one constructor and no dependencies between argument; + it is strict if it has the form + "Inductive I A1 ... An := C (_:A1) ... (_:An)" *) -let match_with_disjunction t = +let match_with_conjunction ?(strict=false) t = let (hdapp,args) = decompose_app t in match kind_of_term hdapp with - | Ind ind -> - let car = mis_constr_nargs ind in - if array_for_all (fun ar -> ar = 1) car && - (let (mib,mip) = Global.lookup_inductive ind in - not (mis_is_recursive (ind,mib,mip))) - then + | Ind ind -> + let (mib,mip) = Global.lookup_inductive ind in + if (Array.length mip.mind_consnames = 1) + && (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) - else - None - | _ -> 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 + Some (hdapp,List.rev cargs) + else None + else None + | _ -> None + +let is_conjunction ?(strict=false) t = + op2bool (match_with_conjunction ~strict 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 match_with_disjunction ?(strict=false) t = + let (hdapp,args) = decompose_app t in + match kind_of_term hdapp with + | Ind ind -> + let car = mis_constr_nargs ind in + let (mib,mip) = Global.lookup_inductive ind in + 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) + else + let cargs = + Array.map (fun ar -> pi2 (destProd (prod_applist ar args))) + mip.mind_nf_lc in + Some (hdapp,Array.to_list cargs) + else + None + | _ -> None -let is_disjunction t = op2bool (match_with_disjunction t) +let is_disjunction ?(strict=false) t = + op2bool (match_with_disjunction ~strict t) + +(* An empty type is an inductive type, possible with indices, that has no + constructors *) let match_with_empty_type t = let (hdapp,args) = decompose_app t in @@ -118,22 +154,32 @@ let match_with_empty_type t = let is_empty_type t = op2bool (match_with_empty_type t) -let match_with_unit_type t = +(* This filters inductive types with one constructor with no arguments; + Parameters and indices are allowed *) + +let match_with_unit_or_eq_type t = let (hdapp,args) = decompose_app t in match (kind_of_term hdapp) with | Ind ind -> let (mib,mip) = Global.lookup_inductive ind in let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in - let zero_args c = - nb_prod c = mib.mind_nparams in + let zero_args c = nb_prod c = mib.mind_nparams in if nconstr = 1 && zero_args constr_types.(0) then Some hdapp - else + else None | _ -> None -let is_unit_type t = op2bool (match_with_unit_type t) +let is_unit_or_eq_type t = op2bool (match_with_unit_or_eq_type t) + +(* A unit type is an inductive type with no indices but possibly + (useless) parameters, and that has no constructors *) + +let is_unit_type t = + match match_with_conjunction t with + | Some (_,t) when List.length t = 0 -> true + | _ -> false (* Checks if a given term is an application of an inductive binary relation R, so that R has only one constructor @@ -204,15 +250,6 @@ let match_with_imp_term c= let is_imp_term c = op2bool (match_with_imp_term c) -let rec has_nodep_prod_after n c = - match kind_of_term c with - | Prod (_,_,b) -> - ( n>0 || not (dependent (mkRel 1) b)) - && (has_nodep_prod_after (n-1) b) - | _ -> true - -let has_nodep_prod = has_nodep_prod_after 0 - let match_with_nodep_ind t = let (hdapp,args) = decompose_app t in match (kind_of_term hdapp) with |