From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Wed, 28 Jul 2004 21:54:47 +0000 Subject: Imported Upstream version 8.0pl1 --- tactics/hipattern.ml | 366 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 366 insertions(+) create mode 100644 tactics/hipattern.ml (limited to 'tactics/hipattern.ml') diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml new file mode 100644 index 00000000..0ada5a06 --- /dev/null +++ b/tactics/hipattern.ml @@ -0,0 +1,366 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'a option + +type testing_function = constr -> bool + +let mkmeta n = Nameops.make_ident "X" (Some n) +let mkPMeta n = PMeta (Some (mkmeta n)) +let meta1 = mkmeta 1 +let meta2 = mkmeta 2 +let meta3 = mkmeta 3 +let meta4 = mkmeta 4 + +let op2bool = function Some _ -> true | None -> false + +let match_with_non_recursive_type t = + match kind_of_term t with + | App _ -> + let (hdapp,args) = decompose_app t in + (match kind_of_term hdapp with + | Ind ind -> + if not (Global.lookup_mind (fst ind)).mind_finite then + Some (hdapp,args) + else + None + | _ -> None) + | _ -> None + +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. *) + +let match_with_conjunction 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) + else + None + | _ -> None + +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. *) + +let match_with_disjunction 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 + Some (hdapp,args) + else + None + | _ -> None + +let is_disjunction t = op2bool (match_with_disjunction t) + +let match_with_empty_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 nconstr = Array.length mip.mind_consnames in + if nconstr = 0 then Some hdapp else None + | _ -> None + +let is_empty_type t = op2bool (match_with_empty_type t) + +let match_with_unit_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 = mip.mind_nparams in + if nconstr = 1 && array_for_all zero_args constr_types then + Some hdapp + else + None + | _ -> None + +let is_unit_type t = op2bool (match_with_unit_type t) + +(* Checks if a given term is an application of an + inductive binary relation R, so that R has only one constructor + establishing its reflexivity. *) + +(* ["(A : ?)(x:A)(? A x x)"] and ["(x : ?)(? x x)"] *) +let x = Name (id_of_string "x") +let y = Name (id_of_string "y") +let name_A = Name (id_of_string "A") +let coq_refl_rel1_pattern = + PProd + (name_A, PMeta None, + PProd (x, PRel 1, PApp (PMeta None, [|PRel 2; PRel 1; PRel 1|]))) +let coq_refl_rel2_pattern = + PProd (x, PMeta None, PApp (PMeta None, [|PRel 1; PRel 1|])) + +let coq_refl_reljm_pattern = +PProd + (name_A, PMeta None, + PProd (x, PRel 1, PApp (PMeta None, [|PRel 2; PRel 1; PRel 2;PRel 1|]))) + +let match_with_equation 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 + if nconstr = 1 && + (is_matching coq_refl_rel1_pattern constr_types.(0) || + is_matching coq_refl_rel2_pattern constr_types.(0) || + is_matching coq_refl_reljm_pattern constr_types.(0)) + then + Some (hdapp,args) + else + None + | _ -> None + +let is_equation t = op2bool (match_with_equation t) + +(* ["(?1 -> ?2)"] *) +let imp a b = PProd (Anonymous, a, b) +let coq_arrow_pattern = imp (mkPMeta 1) (mkPMeta 2) +let match_arrow_pattern t = + match matches coq_arrow_pattern t with + | [(m1,arg);(m2,mind)] -> assert (m1=meta1 & m2=meta2); (arg, mind) + | _ -> anomaly "Incorrect pattern matching" + +let match_with_nottype t = + try + let (arg,mind) = match_arrow_pattern t in + if is_empty_type mind then Some (mind,arg) else None + with PatternMatchingFailure -> None + +let is_nottype t = op2bool (match_with_nottype t) + +let match_with_forall_term c= + match kind_of_term c with + | Prod (nam,a,b) -> Some (nam,a,b) + | _ -> None + +let is_forall_term c = op2bool (match_with_forall_term c) + +let match_with_imp_term c= + match kind_of_term c with + | Prod (_,a,b) when not (dependent (mkRel 1) b) ->Some (a,b) + | _ -> None + +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 + | Ind ind -> + let (mib,mip) = Global.lookup_inductive ind in + if Array.length (mib.mind_packets)>1 then None else + let nodep_constr = has_nodep_prod_after mip.mind_nparams in + if array_for_all nodep_constr mip.mind_nf_lc then + let params= + if mip.mind_nrealargs=0 then args else + fst (list_chop mip.mind_nparams args) in + Some (hdapp,params,mip.mind_nrealargs) + else + None + | _ -> None + +let is_nodep_ind t=op2bool (match_with_nodep_ind t) + +let match_with_sigma_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 + if (Array.length (mib.mind_packets)=1) && + (mip.mind_nrealargs=0) && + (Array.length mip.mind_consnames=1) && + has_nodep_prod_after (mip.mind_nparams+1) mip.mind_nf_lc.(0) then + (*allowing only 1 existential*) + Some (hdapp,args) + else + None + | _ -> None + +let is_sigma_type t=op2bool (match_with_sigma_type t) + +(***** Destructing patterns bound to some theory *) + +let rec first_match matcher = function + | [] -> raise PatternMatchingFailure + | (pat,build_set)::l -> + try (build_set (),matcher pat) + with PatternMatchingFailure -> first_match matcher l + +(*** Equality *) + +(* Patterns "(eq ?1 ?2 ?3)", "(eqT ?1 ?2 ?3)" and "(idT ?1 ?2 ?3)" *) +let coq_eq_pattern_gen eq = + lazy (PApp(PRef (Lazy.force eq), [|mkPMeta 1;mkPMeta 2;mkPMeta 3|])) +let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref +(*let coq_eqT_pattern = coq_eq_pattern_gen coq_eqT_ref*) +let coq_idT_pattern = coq_eq_pattern_gen coq_idT_ref + +let match_eq eqn eq_pat = + match matches (Lazy.force eq_pat) eqn with + | [(m1,t);(m2,x);(m3,y)] -> + assert (m1 = meta1 & m2 = meta2 & m3 = meta3); + (t,x,y) + | _ -> anomaly "match_eq: an eq pattern should match 3 terms" + +let equalities = + [coq_eq_pattern, build_coq_eq_data; +(* coq_eqT_pattern, build_coq_eqT_data;*) + coq_idT_pattern, build_coq_idT_data] + +let find_eq_data_decompose eqn = (* fails with PatternMatchingFailure *) + first_match (match_eq eqn) equalities + +open Tacmach +open Tacticals + +let match_eq_nf gls eqn eq_pat = + match pf_matches gls (Lazy.force eq_pat) eqn with + | [(m1,t);(m2,x);(m3,y)] -> + assert (m1 = meta1 & m2 = meta2 & m3 = meta3); + (t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y) + | _ -> anomaly "match_eq: an eq pattern should match 3 terms" + +let dest_nf_eq gls eqn = + try + snd (first_match (match_eq_nf gls eqn) equalities) + with PatternMatchingFailure -> + error "Not an equality" + +(*** Sigma-types *) + +(* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *) +let coq_ex_pattern_gen ex = + lazy(PApp(PRef (Lazy.force ex), [|mkPMeta 1;mkPMeta 2;mkPMeta 3;mkPMeta 4|])) +let coq_existS_pattern = coq_ex_pattern_gen coq_existS_ref +let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref + +let match_sigma ex ex_pat = + match matches (Lazy.force ex_pat) ex with + | [(m1,a);(m2,p);(m3,car);(m4,cdr)] as l -> + assert (m1=meta1 & m2=meta2 & m3=meta3 & m4=meta4); + (a,p,car,cdr) + | _ -> + anomaly "match_sigma: a successful sigma pattern should match 4 terms" + +let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *) + first_match (match_sigma ex) + [coq_existS_pattern, build_sigma_set; + coq_existT_pattern, build_sigma_type] + +(* Pattern "(sig ?1 ?2)" *) +let coq_sig_pattern = + lazy (PApp (PRef (Lazy.force coq_sig_ref), [| (mkPMeta 1); (mkPMeta 2) |])) + +let match_sigma t = + match matches (Lazy.force coq_sig_pattern) t with + | [(_,a); (_,p)] -> (a,p) + | _ -> anomaly "Unexpected pattern" + +let is_matching_sigma t = is_matching (Lazy.force coq_sig_pattern) t + +(*** Decidable equalities *) + +(* Pattern "(sumbool (eq ?1 ?2 ?3) ?4)" *) +let coq_eqdec_partial_pattern = + lazy + (PApp + (PRef (Lazy.force coq_sumbool_ref), + [| Lazy.force coq_eq_pattern; (mkPMeta 4) |])) + +let match_eqdec_partial t = + match matches (Lazy.force coq_eqdec_partial_pattern) t with + | [_; (_,lhs); (_,rhs); _] -> (lhs,rhs) + | _ -> anomaly "Unexpected pattern" + +(* The expected form of the goal for the tactic Decide Equality *) + +(* Pattern "(x,y:?1){x=y}+{~(x=y)}" *) +(* i.e. "(x,y:?1)(sumbool (eq ?1 x y) ~(eq ?1 x y))" *) +let x = Name (id_of_string "x") +let y = Name (id_of_string "y") +let coq_eqdec_pattern = + lazy + (PProd (x, (mkPMeta 1), PProd (y, (mkPMeta 1), + PApp (PRef (Lazy.force coq_sumbool_ref), + [| PApp (PRef (Lazy.force coq_eq_ref), + [| (mkPMeta 1); PRel 2; PRel 1 |]); + PApp (PRef (Lazy.force coq_not_ref), + [|PApp (PRef (Lazy.force coq_eq_ref), + [| (mkPMeta 1); PRel 2; PRel 1 |])|]) |])))) + +let match_eqdec t = + match matches (Lazy.force coq_eqdec_pattern) t with + | [(_,typ)] -> typ + | _ -> anomaly "Unexpected pattern" + +(* Patterns "~ ?" and "? -> False" *) +let coq_not_pattern = lazy(PApp(PRef (Lazy.force coq_not_ref), [|PMeta None|])) +let coq_imp_False_pattern = + lazy (imp (PMeta None) (PRef (Lazy.force coq_False_ref))) + +let is_matching_not t = is_matching (Lazy.force coq_not_pattern) t +let is_matching_imp_False t = is_matching (Lazy.force coq_imp_False_pattern) t -- cgit v1.2.3