summaryrefslogtreecommitdiff
path: root/tactics/hipattern.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/hipattern.ml4')
-rw-r--r--tactics/hipattern.ml4262
1 files changed, 138 insertions, 124 deletions
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index f8c1db27..4b94f420 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -1,29 +1,24 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*)
+(*i camlp4deps: "grammar/grammar.cma grammar/q_constr.cmo" i*)
open Pp
+open Errors
open Util
open Names
-open Nameops
open Term
-open Sign
open Termops
-open Reductionops
open Inductiveops
-open Evd
-open Environ
-open Clenv
-open Pattern
-open Matching
+open Constr_matching
open Coqlib
open Declarations
+open Tacmach.New
(* I implemented the following functions which test whether a term t
is an inductive but non-recursive type, a general conjuction, a
@@ -52,8 +47,8 @@ let match_with_non_recursive_type t =
| 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
+ | Ind (ind,u) ->
+ if (Global.lookup_mind (fst ind)).mind_finite == Decl_kinds.CoFinite then
Some (hdapp,args)
else
None
@@ -83,55 +78,67 @@ let has_nodep_prod = has_nodep_prod_after 0
(* style: None = record; Some false = conjunction; Some true = strict conj *)
-let match_with_one_constructor style allow_rec t =
+let is_strict_conjunction = function
+| Some true -> true
+| _ -> false
+
+let is_lax_conjunction = function
+| Some false -> true
+| _ -> false
+
+let match_with_one_constructor style onlybinary allow_rec t =
let (hdapp,args) = decompose_app t in
- match kind_of_term hdapp with
+ let res = match kind_of_term hdapp with
| Ind ind ->
- let (mib,mip) = Global.lookup_inductive ind in
- if (Array.length mip.mind_consnames = 1)
- && (allow_rec or not (mis_is_recursive (ind,mib,mip)))
- && (mip.mind_nrealargs = 0)
+ let (mib,mip) = Global.lookup_inductive (fst ind) in
+ if Int.equal (Array.length mip.mind_consnames) 1
+ && (allow_rec || not (mis_is_recursive (fst ind,mib,mip)))
+ && (Int.equal mip.mind_nrealargs 0)
then
- if style = Some true (* strict conjunction *) then
+ if is_strict_conjunction style (* strict conjunction *) then
let ctx =
(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 && isRel c && destRel c = mib.mind_nparams) ctx
+ (fun (_,b,c) -> Option.is_empty b && isRel c && Int.equal (destRel c) 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 ((prod_assum ctyp)) in
- if style <> Some false || has_nodep_prod ctyp then
+ if not (is_lax_conjunction style) || has_nodep_prod ctyp then
(* Record or non strict conjunction *)
Some (hdapp,List.rev cargs)
else
None
else
None
+ | _ -> None in
+ match res with
+ | Some (hdapp, args) when not onlybinary -> res
+ | Some (hdapp, [_; _]) -> res
| _ -> None
-let match_with_conjunction ?(strict=false) t =
- match_with_one_constructor (Some strict) false t
+let match_with_conjunction ?(strict=false) ?(onlybinary=false) t =
+ match_with_one_constructor (Some strict) onlybinary false t
let match_with_record t =
- match_with_one_constructor None false t
+ match_with_one_constructor None false false t
-let is_conjunction ?(strict=false) t =
- op2bool (match_with_conjunction ~strict t)
+let is_conjunction ?(strict=false) ?(onlybinary=false) t =
+ op2bool (match_with_conjunction ~strict ~onlybinary t)
let is_record t =
op2bool (match_with_record t)
let match_with_tuple t =
- let t = match_with_one_constructor None true t in
+ let t = match_with_one_constructor None false true t in
Option.map (fun (hd,l) ->
let ind = destInd hd in
- let (mib,mip) = Global.lookup_inductive ind in
- let isrec = mis_is_recursive (ind,mib,mip) in
+ let (mib,mip) = Global.lookup_pinductive ind in
+ let isrec = mis_is_recursive (fst ind,mib,mip) in
(hd,l,isrec)) t
let is_tuple t =
@@ -143,20 +150,20 @@ let is_tuple t =
"Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *)
let test_strict_disjunction n lc =
- array_for_all_i (fun i c ->
+ Array.for_all_i (fun i c ->
match (prod_assum (snd (decompose_prod_n_assum n c))) with
- | [_,None,c] -> isRel c && destRel c = (n - i)
+ | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i)
| _ -> false) 0 lc
-let match_with_disjunction ?(strict=false) t =
+let match_with_disjunction ?(strict=false) ?(onlybinary=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 res = match kind_of_term hdapp with
+ | Ind (ind,u) ->
+ let car = constructors_nrealargs 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))
- && (mip.mind_nrealargs = 0)
+ if Array.for_all (fun ar -> Int.equal ar 1) car
+ && not (mis_is_recursive (ind,mib,mip))
+ && (Int.equal mip.mind_nrealargs 0)
then
if strict then
if test_strict_disjunction mib.mind_nparams mip.mind_nf_lc then
@@ -170,10 +177,14 @@ let match_with_disjunction ?(strict=false) t =
Some (hdapp,Array.to_list cargs)
else
None
+ | _ -> None in
+ match res with
+ | Some (hdapp,args) when not onlybinary -> res
+ | Some (hdapp,[_; _]) -> res
| _ -> None
-let is_disjunction ?(strict=false) t =
- op2bool (match_with_disjunction ~strict t)
+let is_disjunction ?(strict=false) ?(onlybinary=false) t =
+ op2bool (match_with_disjunction ~strict ~onlybinary t)
(* An empty type is an inductive type, possible with indices, that has no
constructors *)
@@ -182,9 +193,9 @@ 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 (mib,mip) = Global.lookup_pinductive ind in
let nconstr = Array.length mip.mind_consnames in
- if nconstr = 0 then Some hdapp else None
+ if Int.equal nconstr 0 then Some hdapp else None
| _ -> None
let is_empty_type t = op2bool (match_with_empty_type t)
@@ -196,11 +207,11 @@ 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 (mib,mip) = Global.lookup_pinductive 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
- if nconstr = 1 && zero_args constr_types.(0) then
+ let zero_args c = Int.equal (nb_prod c) mib.mind_nparams in
+ if Int.equal nconstr 1 && zero_args constr_types.(0) then
Some hdapp
else
None
@@ -214,7 +225,7 @@ let is_unit_or_eq_type t = op2bool (match_with_unit_or_eq_type t)
let is_unit_type t =
match match_with_conjunction t with
- | Some (_,t) when List.length t = 0 -> true
+ | Some (_,[]) -> true
| _ -> false
(* Checks if a given term is an application of an
@@ -232,27 +243,30 @@ let coq_refl_leibniz1_pattern = PATTERN [ forall x:_, _ x x ]
let coq_refl_leibniz2_pattern = PATTERN [ forall A:_, forall x:A, _ A x x ]
let coq_refl_jm_pattern = PATTERN [ forall A:_, forall x:A, _ A x A x ]
-open Libnames
+open Globnames
+
+let is_matching x y = is_matching (Global.env ()) Evd.empty x y
+let matches x y = matches (Global.env ()) Evd.empty x y
let match_with_equation t =
if not (isApp t) then raise NoEquationFound;
let (hdapp,args) = destApp t in
match kind_of_term hdapp with
- | Ind ind ->
- if IndRef ind = glob_eq then
+ | Ind (ind,u) ->
+ if eq_gr (IndRef ind) glob_eq then
Some (build_coq_eq_data()),hdapp,
PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if IndRef ind = glob_identity then
+ else if eq_gr (IndRef ind) glob_identity then
Some (build_coq_identity_data()),hdapp,
PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
- else if IndRef ind = glob_jmeq then
+ else if eq_gr (IndRef ind) glob_jmeq then
Some (build_coq_jmeq_data()),hdapp,
HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
else
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 then
+ if Int.equal nconstr 1 then
if is_matching coq_refl_leibniz1_pattern constr_types.(0) then
None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
else if is_matching coq_refl_leibniz2_pattern constr_types.(0) then
@@ -263,25 +277,41 @@ let match_with_equation t =
else raise NoEquationFound
| _ -> raise NoEquationFound
+(* Note: An "equality type" is any type with a single argument-free
+ constructor: it captures eq, eq_dep, JMeq, eq_true, etc. but also
+ True/unit which is the degenerate equality type (isomorphic to ()=());
+ in particular, True/unit are provable by "reflexivity" *)
+
let is_inductive_equality ind =
let (mib,mip) = Global.lookup_inductive ind in
let nconstr = Array.length mip.mind_consnames in
- nconstr = 1 && constructor_nrealargs (Global.env()) (ind,1) = 0
+ Int.equal nconstr 1 && Int.equal (constructor_nrealargs (ind,1)) 0
let match_with_equality_type t =
let (hdapp,args) = decompose_app t in
match (kind_of_term hdapp) with
- | Ind ind when is_inductive_equality ind -> Some (hdapp,args)
+ | Ind (ind,_) when is_inductive_equality ind -> Some (hdapp,args)
| _ -> None
let is_equality_type t = op2bool (match_with_equality_type t)
+(* Arrows/Implication/Negation *)
+
let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ]
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 result = matches coq_arrow_pattern t in
+ match Id.Map.bindings result with
+ | [(m1,arg);(m2,mind)] ->
+ assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind)
+ | _ -> anomaly (Pp.str "Incorrect pattern matching")
+
+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 match_with_nottype t =
try
@@ -291,6 +321,8 @@ let match_with_nottype t =
let is_nottype t = op2bool (match_with_nottype t)
+(* Forall *)
+
let match_with_forall_term c=
match kind_of_term c with
| Prod (nam,a,b) -> Some (nam,a,b)
@@ -298,24 +330,17 @@ let match_with_forall_term c=
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 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
+ let (mib,mip) = Global.lookup_pinductive ind in
if Array.length (mib.mind_packets)>1 then None else
let nodep_constr = has_nodep_prod_after mib.mind_nparams in
- if array_for_all nodep_constr mip.mind_nf_lc then
+ if Array.for_all nodep_constr mip.mind_nf_lc then
let params=
- if mip.mind_nrealargs=0 then args else
- fst (list_chop mib.mind_nparams args) in
+ if Int.equal mip.mind_nrealargs 0 then args else
+ fst (List.chop mib.mind_nparams args) in
Some (hdapp,params,mip.mind_nrealargs)
else
None
@@ -327,10 +352,10 @@ 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) &&
+ let (mib,mip) = Global.lookup_pinductive ind in
+ if Int.equal (Array.length (mib.mind_packets)) 1 &&
+ (Int.equal mip.mind_nrealargs 0) &&
+ (Int.equal (Array.length mip.mind_consnames)1) &&
has_nodep_prod_after (mib.mind_nparams+1) mip.mind_nf_lc.(0) then
(*allowing only 1 existential*)
Some (hdapp,args)
@@ -344,9 +369,10 @@ let is_sigma_type t=op2bool (match_with_sigma_type t)
let rec first_match matcher = function
| [] -> raise PatternMatchingFailure
- | (pat,build_set)::l ->
- try (build_set (),matcher pat)
- with PatternMatchingFailure -> first_match matcher l
+ | (pat,check,build_set)::l when check () ->
+ (try (build_set (),matcher pat)
+ with PatternMatchingFailure -> first_match matcher l)
+ | _::l -> first_match matcher l
(*** Equality *)
@@ -355,50 +381,48 @@ let coq_eq_pattern_gen eq = lazy PATTERN [ %eq ?X1 ?X2 ?X3 ]
let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref
let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref
let coq_jmeq_pattern = lazy PATTERN [ %coq_jmeq_ref ?X1 ?X2 ?X3 ?X4 ]
-let coq_eq_true_pattern = lazy PATTERN [ %coq_eq_true_ref ?X1 ]
let match_eq eqn eq_pat =
let pat =
try Lazy.force eq_pat
with e when Errors.noncritical e -> raise PatternMatchingFailure
in
- match matches pat eqn with
+ match Id.Map.bindings (matches pat eqn) with
| [(m1,t);(m2,x);(m3,y)] ->
- assert (m1 = meta1 & m2 = meta2 & m3 = meta3);
- PolymorphicLeibnizEq (t,x,y)
+ assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
+ PolymorphicLeibnizEq (t,x,y)
| [(m1,t);(m2,x);(m3,t');(m4,x')] ->
- assert (m1 = meta1 & m2 = meta2 & m3 = meta3 & m4 = meta4);
+ assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3 && Id.equal m4 meta4);
HeterogenousEq (t,x,t',x')
- | _ -> anomaly "match_eq: an eq pattern should match 3 or 4 terms"
+ | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 or 4 terms")
+
+let no_check () = true
+let check_jmeq_loaded () = Library.library_is_loaded Coqlib.jmeq_module
let equalities =
- [coq_eq_pattern, build_coq_eq_data;
- coq_jmeq_pattern, build_coq_jmeq_data;
- coq_identity_pattern, build_coq_identity_data]
+ [coq_eq_pattern, no_check, build_coq_eq_data;
+ coq_jmeq_pattern, check_jmeq_loaded, build_coq_jmeq_data;
+ coq_identity_pattern, no_check, build_coq_identity_data]
let find_eq_data eqn = (* fails with PatternMatchingFailure *)
- first_match (match_eq eqn) equalities
+ let d,k = first_match (match_eq eqn) equalities in
+ let hd,u = destInd (fst (destApp eqn)) in
+ d,u,k
let extract_eq_args gl = function
| MonomorphicLeibnizEq (e1,e2) ->
- let t = Tacmach.pf_type_of gl e1 in (t,e1,e2)
+ let t = pf_type_of gl e1 in (t,e1,e2)
| PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
| HeterogenousEq (t1,e1,t2,e2) ->
- if Tacmach.pf_conv_x gl t1 t2 then (t1,e1,e2)
+ if pf_conv_x gl t1 t2 then (t1,e1,e2)
else raise PatternMatchingFailure
let find_eq_data_decompose gl eqn =
- let (lbeq,eq_args) = find_eq_data eqn in
- (lbeq,extract_eq_args gl eq_args)
-
-let inversible_equalities =
- [coq_eq_pattern, build_coq_inversion_eq_data;
- coq_jmeq_pattern, build_coq_inversion_jmeq_data;
- coq_identity_pattern, build_coq_inversion_identity_data;
- coq_eq_true_pattern, build_coq_inversion_eq_true_data]
+ let (lbeq,u,eq_args) = find_eq_data eqn in
+ (lbeq,u,extract_eq_args gl eq_args)
let find_this_eq_data_decompose gl eqn =
- let (lbeq,eq_args) =
+ let (lbeq,u,eq_args) =
try (*first_match (match_eq eqn) inversible_equalities*)
find_eq_data eqn
with PatternMatchingFailure ->
@@ -407,17 +431,14 @@ let find_this_eq_data_decompose gl eqn =
try extract_eq_args gl eq_args
with PatternMatchingFailure ->
error "Don't know what to do with JMeq on arguments not of same type." in
- (lbeq,eq_args)
-
-open Tacmach
-open Tacticals
+ (lbeq,u,eq_args)
let match_eq_nf gls eqn eq_pat =
- match pf_matches gls (Lazy.force eq_pat) eqn with
+ match Id.Map.bindings (pf_matches gls (Lazy.force eq_pat) eqn) with
| [(m1,t);(m2,x);(m3,y)] ->
- assert (m1 = meta1 & m2 = meta2 & m3 = meta3);
+ assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
(t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y)
- | _ -> anomaly "match_eq: an eq pattern should match 3 terms"
+ | _ -> anomaly ~label:"match_eq" (Pp.str "an eq pattern should match 3 terms")
let dest_nf_eq gls eqn =
try
@@ -427,31 +448,24 @@ let dest_nf_eq gls eqn =
(*** Sigma-types *)
-(* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *)
-let coq_ex_pattern_gen ex = lazy PATTERN [ %ex ?X1 ?X2 ?X3 ?X4 ]
-let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref
-let coq_exist_pattern = coq_ex_pattern_gen coq_exist_ref
-
-let match_sigma ex ex_pat =
- match matches (Lazy.force ex_pat) ex with
- | [(m1,a);(m2,p);(m3,car);(m4,cdr)] ->
- 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 match_sigma ex =
+ match kind_of_term ex with
+ | App (f, [| a; p; car; cdr |]) when is_global (Lazy.force coq_exist_ref) f ->
+ build_sigma (), (snd (destConstruct f), a, p, car, cdr)
+ | App (f, [| a; p; car; cdr |]) when is_global (Lazy.force coq_existT_ref) f ->
+ build_sigma_type (), (snd (destConstruct f), a, p, car, cdr)
+ | _ -> raise PatternMatchingFailure
+
let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
- first_match (match_sigma ex)
- [coq_existT_pattern, build_sigma_type;
- coq_exist_pattern, build_sigma]
+ match_sigma ex
(* Pattern "(sig ?1 ?2)" *)
let coq_sig_pattern = lazy PATTERN [ %coq_sig_ref ?X1 ?X2 ]
let match_sigma t =
- match matches (Lazy.force coq_sig_pattern) t with
+ match Id.Map.bindings (matches (Lazy.force coq_sig_pattern) t) with
| [(_,a); (_,p)] -> (a,p)
- | _ -> anomaly "Unexpected pattern"
+ | _ -> anomaly (Pp.str "Unexpected pattern")
let is_matching_sigma t = is_matching (Lazy.force coq_sig_pattern) t
@@ -486,10 +500,10 @@ let match_eqdec t =
try true,op_or,matches (Lazy.force coq_eqdec_pattern) t
with PatternMatchingFailure ->
false,op_or,matches (Lazy.force coq_eqdec_rev_pattern) t in
- match subst with
+ match Id.Map.bindings subst with
| [(_,typ);(_,c1);(_,c2)] ->
- eqonleft, Libnames.constr_of_global (Lazy.force op), c1, c2, typ
- | _ -> anomaly "Unexpected pattern"
+ eqonleft, Universes.constr_of_global (Lazy.force op), c1, c2, typ
+ | _ -> anomaly (Pp.str "Unexpected pattern")
(* Patterns "~ ?" and "? -> False" *)
let coq_not_pattern = lazy PATTERN [ ~ _ ]
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 02:54:17 +0000