diff options
Diffstat (limited to 'tactics/hipattern.ml4')
| -rw-r--r-- | tactics/hipattern.ml4 | 245 |
1 files changed, 156 insertions, 89 deletions
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index 2e83ac70..9aec0e09 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*) -(* $Id: hipattern.ml4 11739 2009-01-02 19:33:19Z herbelin $ *) +(* $Id$ *) open Pp open Util @@ -32,10 +32,10 @@ open Declarations 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 + 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 @@ -50,16 +50,16 @@ 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 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 + | Ind ind -> + if not (Global.lookup_mind (fst ind)).mind_finite then + Some (hdapp,args) + else + None | _ -> None) | _ -> None @@ -69,34 +69,34 @@ let is_non_recursive_type t = op2bool (match_with_non_recursive_type t) let rec has_nodep_prod_after n c = match kind_of_term c with - | Prod (_,_,b) -> - ( n>0 || not (dependent (mkRel 1) b)) + | 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 -(* A general conjunctive type is a non-recursive with-no-indices inductive +(* 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 + it is strict if it has the form "Inductive I A1 ... An := C (_:A1) ... (_:An)" *) (* style: None = record; Some false = conjunction; Some true = strict conj *) -let match_with_one_constructor style t = - let (hdapp,args) = decompose_app t in +let match_with_one_constructor style allow_rec t = + let (hdapp,args) = decompose_app t in match kind_of_term hdapp with - | Ind ind -> + | Ind ind -> let (mib,mip) = Global.lookup_inductive ind in if (Array.length mip.mind_consnames = 1) - && (not (mis_is_recursive (ind,mib,mip))) + && (allow_rec or not (mis_is_recursive (ind,mib,mip))) && (mip.mind_nrealargs = 0) then if style = Some true (* strict conjunction *) then - let ctx = - fst (decompose_prod_assum (snd + let ctx = + (prod_assum (snd (decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))) in - if + if List.for_all (fun (_,b,c) -> b=None && c = mkRel mib.mind_nparams) ctx then @@ -104,7 +104,7 @@ let match_with_one_constructor style t = 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 + let cargs = List.map pi3 ((prod_assum ctyp)) in if style <> Some false || has_nodep_prod ctyp then (* Record or non strict conjunction *) Some (hdapp,List.rev cargs) @@ -115,10 +115,10 @@ let match_with_one_constructor style t = | _ -> None let match_with_conjunction ?(strict=false) t = - match_with_one_constructor (Some strict) t + match_with_one_constructor (Some strict) false t -let match_with_record t = - match_with_one_constructor None t +let match_with_record t = + match_with_one_constructor None false t let is_conjunction ?(strict=false) t = op2bool (match_with_conjunction ~strict t) @@ -126,20 +126,30 @@ let is_conjunction ?(strict=false) 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 + 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 + (hd,l,isrec)) t + +let is_tuple t = + op2bool (match_with_tuple t) -(* A general disjunction type is a non-recursive with-no-indices inductive +(* 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 + 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 + match (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 + let (hdapp,args) = decompose_app t in match kind_of_term hdapp with | Ind ind -> let car = mis_constr_nargs ind in @@ -157,7 +167,7 @@ let match_with_disjunction ?(strict=false) t = Array.map (fun ar -> pi2 (destProd (prod_applist ar args))) mip.mind_nf_lc in Some (hdapp,Array.to_list cargs) - else + else None | _ -> None @@ -170,12 +180,12 @@ let is_disjunction ?(strict=false) t = let match_with_empty_type t = let (hdapp,args) = decompose_app t in match (kind_of_term hdapp) with - | Ind ind -> + | Ind ind -> let (mib,mip) = Global.lookup_inductive ind in - let nconstr = Array.length mip.mind_consnames 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) (* This filters inductive types with one constructor with no arguments; @@ -184,21 +194,22 @@ let is_empty_type t = op2bool (match_with_empty_type t) let match_with_unit_or_eq_type t = let (hdapp,args) = decompose_app t in match (kind_of_term hdapp) with - | Ind ind -> + | Ind ind -> let (mib,mip) = Global.lookup_inductive ind in - let constr_types = mip.mind_nf_lc 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 = 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_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 *) + (useless) parameters, and that has no arguments in its unique + constructor *) let is_unit_type t = match match_with_conjunction t with @@ -209,75 +220,94 @@ let is_unit_type t = inductive binary relation R, so that R has only one constructor establishing its reflexivity. *) -let coq_refl_rel1_pattern = PATTERN [ forall A:_, forall x:A, _ A x x ] -let coq_refl_rel2_pattern = PATTERN [ forall x:_, _ x x ] -let coq_refl_reljm_pattern = PATTERN [ forall A:_, forall x:A, _ A x A x ] +type equation_kind = + | MonomorphicLeibnizEq of constr * constr + | PolymorphicLeibnizEq of constr * constr * constr + | HeterogenousEq of constr * constr * constr * constr + +exception NoEquationFound + +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 let match_with_equation t = - let (hdapp,args) = decompose_app t in - match (kind_of_term hdapp) with - | Ind ind -> + 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 + Some (build_coq_eq_data()),hdapp, + PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if 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 + 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 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) + if 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 + None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) + else if is_matching coq_refl_jm_pattern constr_types.(0) then + None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) + else raise NoEquationFound + else raise NoEquationFound + | _ -> raise NoEquationFound + +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 let match_with_equality_type t = let (hdapp,args) = decompose_app t in match (kind_of_term hdapp) with - | Ind ind when args <> [] -> - let (mib,mip) = Global.lookup_inductive ind in - let nconstr = Array.length mip.mind_consnames in - if nconstr = 1 && constructor_nrealargs (Global.env()) (ind,1) = 0 - then - Some (hdapp,args) - else - None - | _ -> None + | Ind ind when is_inductive_equality ind -> Some (hdapp,args) + | _ -> None + +let is_equality_type t = op2bool (match_with_equality_type t) 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" + | _ -> 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 + 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 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 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 -> + | 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 mib.mind_nparams in @@ -286,24 +316,24 @@ let match_with_nodep_ind t = if mip.mind_nrealargs=0 then args else fst (list_chop mib.mind_nparams args) in Some (hdapp,params,mip.mind_nrealargs) - else + 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 -> + | 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 (mib.mind_nparams+1) mip.mind_nf_lc.(0) then - (*allowing only 1 existential*) + (*allowing only 1 existential*) Some (hdapp,args) - else + else None | _ -> None @@ -323,21 +353,58 @@ let rec first_match matcher = function 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 = - match matches (Lazy.force eq_pat) eqn with + let pat = try Lazy.force eq_pat with _ -> raise PatternMatchingFailure in + match matches 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" + PolymorphicLeibnizEq (t,x,y) + | [(m1,t);(m2,x);(m3,t');(m4,x')] -> + assert (m1 = meta1 & m2 = meta2 & m3 = meta3 & m4 = meta4); + HeterogenousEq (t,x,t',x') + | _ -> anomaly "match_eq: an eq pattern should match 3 or 4 terms" let equalities = [coq_eq_pattern, build_coq_eq_data; + coq_jmeq_pattern, build_coq_jmeq_data; coq_identity_pattern, build_coq_identity_data] -let find_eq_data_decompose eqn = (* fails with PatternMatchingFailure *) +let find_eq_data eqn = (* fails with PatternMatchingFailure *) first_match (match_eq eqn) equalities +let extract_eq_args gl = function + | MonomorphicLeibnizEq (e1,e2) -> + let t = Tacmach.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) + 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 find_this_eq_data_decompose gl eqn = + let (lbeq,eq_args) = + try (*first_match (match_eq eqn) inversible_equalities*) + find_eq_data eqn + with PatternMatchingFailure -> + errorlabstrm "" (str "No primitive equality found.") in + let eq_args = + 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 @@ -369,7 +436,7 @@ let match_sigma ex ex_pat = 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) + first_match (match_sigma ex) [coq_existT_pattern, build_sigma_type] (* Pattern "(sig ?1 ?2)" *) @@ -407,14 +474,14 @@ let op_sum = coq_sumbool_ref let match_eqdec t = let eqonleft,op,subst = try true,op_sum,matches (Lazy.force coq_eqdec_inf_pattern) t - with PatternMatchingFailure -> + with PatternMatchingFailure -> try false,op_sum,matches (Lazy.force coq_eqdec_inf_rev_pattern) t - with PatternMatchingFailure -> + with PatternMatchingFailure -> try true,op_or,matches (Lazy.force coq_eqdec_pattern) t - with PatternMatchingFailure -> + with PatternMatchingFailure -> false,op_or,matches (Lazy.force coq_eqdec_rev_pattern) t in match subst with - | [(_,typ);(_,c1);(_,c2)] -> + | [(_,typ);(_,c1);(_,c2)] -> eqonleft, Libnames.constr_of_global (Lazy.force op), c1, c2, typ | _ -> anomaly "Unexpected pattern" |