summaryrefslogtreecommitdiff
path: root/tactics/hipattern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/hipattern.ml')
-rw-r--r--tactics/hipattern.ml366
1 files changed, 366 insertions, 0 deletions
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 *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id: hipattern.ml,v 1.29.2.1 2004/07/16 19:30:53 herbelin Exp $ *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Term
+open Termops
+open Reductionops
+open Inductiveops
+open Evd
+open Environ
+open Proof_trees
+open Clenv
+open Pattern
+open Matching
+open Coqlib
+open Declarations
+
+(* I implemented the following functions which test whether a term t
+ is an inductive but non-recursive type, a general conjuction, a
+ general disjunction, or a type with no constructors.
+
+ They are more general than matching with or_term, and_term, etc,
+ since they do not depend on the name of the type. Hence, they
+ also work on ad-hoc disjunctions introduced by the user.
+
+ -- Eduardo (6/8/97). *)
+
+type 'a matching_function = constr -> '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){<?1>x=y}+{~(<?1>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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 09:34:49 +0000