diff options
| -rw-r--r-- | parsing/astterm.ml | 22 | ||||
| -rw-r--r-- | parsing/termast.ml | 10 | ||||
| -rw-r--r-- | pretyping/classops.mli | 2 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 12 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 3 | ||||
| -rw-r--r-- | pretyping/rawterm.ml | 5 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 134 | ||||
| -rw-r--r-- | tactics/pattern.ml | 132 | ||||
| -rw-r--r-- | tactics/pattern.mli | 29 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 7 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 2 |
12 files changed, 186 insertions, 176 deletions
diff --git a/parsing/astterm.ml b/parsing/astterm.ml index fd32cda39..dd2f1b5d8 100644 --- a/parsing/astterm.ml +++ b/parsing/astterm.ml @@ -90,12 +90,14 @@ let ident_of_nvar loc s = user_err_loc (loc,"ident_of_nvar", [< 'sTR "Unexpected wildcard" >]) else (id_of_string s) +(* let rctxt_of_ctxt = Array.map (function | VAR id -> RRef (dummy_loc,RVar id) | _ -> error "Astterm: arbitrary substitution of references not yet implemented") +*) let ids_of_ctxt ctxt = Array.to_list @@ -119,7 +121,9 @@ let dbize_ctxt ctxt = let l = List.map (function - | Nvar (loc,s) -> RRef (dummy_loc,RVar (ident_of_nvar loc s)) + | Nvar (loc,s) -> + (* RRef (dummy_loc,RVar (ident_of_nvar loc s)) *) + VAR (ident_of_nvar loc s) | _ -> anomaly "Bad ast for local ctxt of a global reference") ctxt in Array.of_list l @@ -139,10 +143,10 @@ let dbize_global loc = function [< 'sTR "Bad ast for this global a reference">]) let ref_from_constr = function - | DOPN (Const sp,ctxt) -> RConst (sp,rctxt_of_ctxt ctxt) - | DOPN (Evar ev,ctxt) -> REVar (ev,rctxt_of_ctxt ctxt) - | DOPN (MutConstruct (spi,j),ctxt) -> RConstruct ((spi,j),rctxt_of_ctxt ctxt) - | DOPN (MutInd (sp,i),ctxt) -> RInd ((sp,i),rctxt_of_ctxt ctxt) + | DOPN (Const sp,ctxt) -> RConst (sp, ctxt) + | DOPN (Evar ev,ctxt) -> REVar (ev, ctxt) + | DOPN (MutConstruct (spi,j),ctxt) -> RConstruct ((spi,j), ctxt) + | DOPN (MutInd (sp,i),ctxt) -> RInd ((sp,i), ctxt) | VAR id -> RVar id (* utilisé dans trad pour coe_value (tmp) *) | _ -> anomaly "Not a reference" @@ -561,10 +565,10 @@ let ctxt_of_ids ids = Array.of_list (List.map (function id -> VAR id) ids) let rec pat_of_ref metas vars = function - | RConst (sp,ctxt) -> RConst (sp, Array.map (pat_of_raw metas vars) ctxt) - | RInd (ip,ctxt) -> RInd (ip, Array.map (pat_of_raw metas vars) ctxt) - | RConstruct(cp,ctxt) ->RConstruct(cp,Array.map (pat_of_raw metas vars) ctxt) - | REVar (n,ctxt) -> REVar (n,Array.map (pat_of_raw metas vars) ctxt) + | RConst (sp,ctxt) -> RConst (sp, ctxt) + | RInd (ip,ctxt) -> RInd (ip, ctxt) + | RConstruct(cp,ctxt) ->RConstruct(cp, ctxt) + | REVar (n,ctxt) -> REVar (n, ctxt) | RMeta n -> RMeta n | RAbst _ -> error "pattern_of_rawconstr: not implemented" | RVar _ -> assert false (* Capturé dans pattern_of_raw *) diff --git a/parsing/termast.ml b/parsing/termast.ml index bcdc21f05..3587ba01e 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -50,6 +50,7 @@ let with_coercions f = with_option print_coercions f (**********************************************************************) (* conversion of references *) +(* let ids_of_rctxt ctxt = Array.to_list (Array.map @@ -59,6 +60,7 @@ let ids_of_rctxt ctxt = error "Termast: arbitrary substitution of references not yet implemented") ctxt) +*) let ids_of_ctxt ctxt = Array.to_list @@ -122,14 +124,14 @@ let ast_of_inductive_ref ((sp,tyi) as ind_sp,ids) = let ast_of_inductive (ev,ctxt) = ast_of_inductive_ref (ev,ids_of_ctxt ctxt) let ast_of_ref = function - | RConst (sp,ctxt) -> ast_of_constant_ref (sp,ids_of_rctxt ctxt) + | RConst (sp,ctxt) -> ast_of_constant_ref (sp,ids_of_ctxt ctxt) | RAbst (sp) -> ope("ABST", (path_section dummy_loc sp) ::(List.map ast_of_ident (* on triche *) [])) - | RInd (ind,ctxt) -> ast_of_inductive_ref (ind,ids_of_rctxt ctxt) - | RConstruct (cstr,ctxt) -> ast_of_constructor_ref (cstr,ids_of_rctxt ctxt) + | RInd (ind,ctxt) -> ast_of_inductive_ref (ind,ids_of_ctxt ctxt) + | RConstruct (cstr,ctxt) -> ast_of_constructor_ref (cstr,ids_of_ctxt ctxt) | RVar id -> nvar (string_of_id id) - | REVar (ev,ctxt) -> ast_of_existential_ref (ev,ids_of_rctxt ctxt) + | REVar (ev,ctxt) -> ast_of_existential_ref (ev,ids_of_ctxt ctxt) | RMeta n -> ope("META",[num n]) (**********************************************************************) diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 98d6fce9c..ab9410cc6 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -53,7 +53,7 @@ val coercion_exists : coe_typ -> bool val coercion_info : coe_typ -> (int * coe_info_typ) val coercion_info_from_index : int -> coe_typ * coe_info_typ val coercion_params : - rawconstr array reference -> int (* raise [Not_found] if not a coercion *) + 'a array reference -> int (* raise [Not_found] if not a coercion *) val constructor_at_head : constr -> cl_typ * int (* raises [Not_found] if not convertible to a class *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 2dd49e4b7..a7c84dd3c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -315,17 +315,13 @@ let rec detype avoid env t = | IsAppL (f,args) -> RApp (dummy_loc,detype avoid env f,List.map (detype avoid env) args) | IsConst (sp,cl) -> - RRef(dummy_loc,RConst(sp,Array.map (detype avoid env) cl)) + RRef(dummy_loc,RConst(sp,cl)) | IsEvar (ev,cl) -> - RRef(dummy_loc,REVar(ev,Array.map (detype avoid env) cl)) + RRef(dummy_loc,REVar(ev,cl)) | IsAbst (sp,cl) -> anomaly "bdize: Abst should no longer occur in constr" - | IsMutInd (ind_sp,cl) -> - let ctxt = Array.map (detype avoid env) cl in - RRef (dummy_loc,RInd (ind_sp,ctxt)) - | IsMutConstruct (cstr_sp,cl) -> - let ctxt = Array.map (detype avoid env) cl in - RRef (dummy_loc,RConstruct (cstr_sp,ctxt)) + | IsMutInd (ind_sp,cl) -> RRef (dummy_loc,RInd (ind_sp,cl)) + | IsMutConstruct (cstr_sp,cl) -> RRef (dummy_loc,RConstruct (cstr_sp,cl)) | IsMutCase (annot,p,c,bl) -> let synth_type = synthetize_type () in let tomatch = detype avoid env c in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5a1a9df46..609567771 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -144,12 +144,15 @@ let transform_rec loc env sigma cl (ct,pt) = (***********************************************************************) +(* let ctxt_of_ids ids = Array.map (function | RRef (_,RVar id) -> VAR id | _ -> error "pretyping: arbitrary subst of ref not implemented") ids +*) +let ctxt_of_ids cl = cl let mt_evd = Evd.empty diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index ab3075f45..4090e5815 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -32,8 +32,9 @@ type 'ctxt reference = | REVar of int * 'ctxt | RMeta of int +(*i Pas beau ce constr dans rawconstr, mais mal compris ce ctxt des ref i*) type rawconstr = - | RRef of loc * rawconstr array reference + | RRef of loc * Term.constr array reference | RApp of loc * rawconstr * rawconstr list | RBinder of loc * binder_kind * name * rawconstr * rawconstr | RCases of loc * Term.case_style * rawconstr option * rawconstr list * @@ -73,7 +74,7 @@ let loc_of_rawconstr = function | RCast (loc,_,_) -> loc type constr_pattern = - | PRef of constr_pattern array reference + | PRef of Term.constr array reference | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of int * int list diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index f78520a16..5f67a8a92 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -32,7 +32,7 @@ type 'ctxt reference = | RMeta of int type rawconstr = - | RRef of loc * rawconstr array reference + | RRef of loc * Term.constr array reference | RApp of loc * rawconstr * rawconstr list | RBinder of loc * binder_kind * name * rawconstr * rawconstr | RCases of loc * Term.case_style * rawconstr option * rawconstr list * @@ -61,7 +61,7 @@ val dummy_loc : loc val loc_of_rawconstr : rawconstr -> loc type constr_pattern = - | PRef of constr_pattern array reference + | PRef of Term.constr array reference | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of int * int list diff --git a/tactics/equality.ml b/tactics/equality.ml index 1880b5a09..ff62150a0 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -173,10 +173,10 @@ let find_constructor env sigma c = | _ -> error "find_constructor" type leibniz_eq = { - eq : marked_pattern; - ind : marked_pattern; + eq : marked_term; + ind : marked_term; rrec : marked_pattern option; - rect : marked_pattern option; + rect : marked_term option; congr: marked_pattern; sym : marked_pattern } @@ -187,21 +187,24 @@ let eq_pattern = put_pat mmk "(eq ? ? ?)" let not_pattern = put_pat mmk "(not ?)" let imp_False_pattern = put_pat mmk "? -> False" -let pat_True = put_pat mmk "True" -let pat_False = put_pat mmk "False" -let pat_I = put_pat mmk "I" - -let eq= { eq = put_pat mmk "eq"; - ind = put_pat mmk "eq_ind" ; +let eq= { eq = put_squel mmk "eq"; + ind = put_squel mmk "eq_ind" ; rrec = Some (put_pat mmk "eq_rec"); - rect = Some (put_pat mmk "eq_rect"); + rect = Some (put_squel mmk "eq_rect"); congr = put_pat mmk "f_equal" ; sym = put_pat mmk "sym_eq" } + +let build_eq eq = get_squel eq.eq +let build_ind eq = get_squel eq.ind +let build_rect eq = + match eq.rect with + | None -> assert false + | Some sq -> get_squel sq let eqT_pattern = put_pat mmk "(eqT ? ? ?)" -let eqT= { eq = put_pat mmk "eqT"; - ind = put_pat mmk "eqT_ind" ; +let eqT= { eq = put_squel mmk "eqT"; + ind = put_squel mmk "eqT_ind" ; rrec = None; rect = None; congr = put_pat mmk "congr_eqT" ; @@ -209,16 +212,33 @@ let eqT= { eq = put_pat mmk "eqT"; let idT_pattern = put_pat mmk "(identityT ? ? ?)" -let idT = { eq = put_pat mmk "identityT"; - ind = put_pat mmk "identityT_ind" ; +let idT = { eq = put_squel mmk "identityT"; + ind = put_squel mmk "identityT_ind" ; rrec = Some (put_pat mmk "identityT_rec") ; - rect = Some (put_pat mmk "identityT_rect"); + rect = Some (put_squel mmk "identityT_rect"); congr = put_pat mmk "congr_idT" ; sym = put_pat mmk "sym_idT" } +(* List of constructions depending of the initial state *) + +(* Initialisation part *) +let squel_EmptyT = put_squel mmk "EmptyT" +let squel_True = put_squel mmk "True" +let squel_False = put_squel mmk "False" +let squel_UnitT = put_squel mmk "UnitT" +let squel_IT = put_squel mmk "IT" +let squel_I = put_squel mmk "I" + +(* Runtime part *) +let build_EmptyT () = get_squel squel_EmptyT +let build_True () = get_squel squel_True +let build_False () = get_squel squel_False +let build_UnitT () = get_squel squel_UnitT +let build_IT () = get_squel squel_IT +let build_I () = get_squel squel_I + +let pat_False = put_pat mmk "False" let pat_EmptyT = put_pat mmk "EmptyT" -let pat_UnitT = put_pat mmk "UnitT" -let pat_IT = put_pat mmk "IT" let notT_pattern = put_pat mmk "(notT ?)" let rec hd_of_prod prod = @@ -253,14 +273,14 @@ let necessary_elimination sort_arity sort = [< 'sTR "no primitive equality on proofs" >] let find_eq_pattern aritysort sort = - let mt = +(* let mt =*) match necessary_elimination aritysort sort with | Set_Type -> eq.eq | Type_Type -> idT.eq | Set_SetorProp -> eq.eq | Type_SetorProp -> eqT.eq - in - get_pat mt +(* in + get_pat mt*) (* [find_positions t1 t2] @@ -468,12 +488,11 @@ let construct_discriminator sigma env dirn c sort = let (true_0,false_0,sort_0) = match necessary_elimination arsort (destSort sort) with | Type_Type -> - get_pat pat_UnitT, get_pat pat_EmptyT, + build_UnitT (), build_EmptyT (), (DOP0(Sort (Type(dummy_univ)))) | _ -> - get_pat pat_True, get_pat pat_False, (DOP0(Sort (Prop Null))) + build_True (), build_False (), (DOP0(Sort (Prop Null))) in - let eq = find_eq_pattern arsort (destSort sort) in let p = lam_it sort_0 arsign in let bty,_ = type_case_branches env sigma indspec (type_of env sigma p) p c in let build_branch i = @@ -500,8 +519,10 @@ let rec build_discriminator sigma env dirn c sort = function let subval = build_discriminator sigma cnum_env dirn newc sort l in (match necessary_elimination arsort (destSort sort) with | Type_Type -> - kont subval (get_pat pat_EmptyT,DOP0(Sort(Type(dummy_univ)))) - | _ -> kont subval (get_pat pat_False,DOP0(Sort(Prop Null)))) + kont subval (build_EmptyT (),DOP0(Sort(Type(dummy_univ)))) + | _ -> kont subval (build_False () + +,DOP0(Sort(Prop Null)))) | _ -> assert false let dest_somatch_eq eqn eq_pat = @@ -546,11 +567,10 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls = let sort = pf_type_of gls (pf_concl gls) in match necessary_elimination (destSort(hd_of_prod arity)) (destSort sort) with | Type_Type -> - let rect = match lbeq.rect with Some x -> x | _ -> assert false in - let eq_elim = get_pat rect in - let eq_term = get_pat lbeq.eq in - let i = get_pat pat_IT in - let absurd_term = get_pat pat_EmptyT in + let eq_elim = build_rect lbeq in + let eq_term = build_eq lbeq in + let i = build_IT () in + let absurd_term = build_EmptyT () in let h = pf_get_new_id (id_of_string "HH")gls in let pred= mkNamedLambda e t (mkNamedLambda h (applist (eq_term, [t;t1;(Rel 1)])) @@ -558,9 +578,11 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls = in (applist(eq_elim, [t;t1;pred;i;t2]), absurd_term) | _ -> - let i = get_pat pat_I in - let absurd_term = get_pat pat_False in - let eq_elim = get_pat lbeq.ind in + let i = build_I () in + let absurd_term = build_False () + + in + let eq_elim = build_ind lbeq in (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term) @@ -650,29 +672,41 @@ let h_discrHyp = hide_ident_tactic "DiscrHyp" discrHyp let bind_ith na i t = lift i (DLAM(na,lift (-(i-1)) t)) -let existS_term = put_pat mmk "existS" +let existS_term = put_squel mmk "existS" let existS_pattern = put_pat mmk "(existS ? ? ? ?)" -let sigS_term = put_pat mmk "sigS" -let projS1_term = put_pat mmk "projS1" -let projS2_term = put_pat mmk "projS2" -let sigS_rec_term = put_pat mmk "sigS_rec" +let sigS_term = put_squel mmk "sigS" +let projS1_term = put_squel mmk "projS1" +let projS2_term = put_squel mmk "projS2" +let sigS_rec_term = put_squel mmk "sigS_rec" -let existT_term = put_pat mmk "existT" +let existT_term = put_squel mmk "existT" let existT_pattern = put_pat mmk "(existT ? ? ? ?)" -let sigT_term = put_pat mmk "sigT" -let projT1_term = put_pat mmk "projT1" -let projT2_term = put_pat mmk "projT2" -let sigT_rect_term = put_pat mmk "sigT_rect" +let sigT_term = put_squel mmk "sigT" +let projT1_term = put_squel mmk "projT1" +let projT2_term = put_squel mmk "projT2" +let sigT_rect_term = put_squel mmk "sigT_rect" + +let build_sigma_prop () = + (get_squel projS1_term, + get_squel projS2_term, + get_squel sigS_rec_term, + get_squel existS_term, + get_squel sigS_term) + +let build_sigma_type () = + (get_squel projT1_term, + get_squel projT2_term, + get_squel sigT_rect_term, + get_squel existT_term, + get_squel sigT_term) (* returns the sigma type (sigS, sigT) with the respective constructor depending on the sort *) let find_sigma_data s = match strip_outer_cast s with - | DOP0(Sort(Prop Pos)) -> (* Set *) - (projS1_term,projS2_term,sigS_rec_term,existS_term, sigS_term) - | DOP0(Sort(Type(_))) -> (* Type *) - (projT1_term, projT2_term, sigT_rect_term, existT_term, sigT_term) + | DOP0(Sort(Prop Pos)) -> build_sigma_prop () (* Set *) + | DOP0(Sort(Type(_))) -> build_sigma_type () (* Type *) | _ -> error "find_sigma_data" (* [make_tuple env na lind rterm rty] @@ -698,8 +732,8 @@ let make_tuple sigma env na lind rterm rty = let a = type_of env sigma (Rel lind) in let p = DOP2(Lambda,a, bind_ith (fst(lookup_rel lind env)) lind rty) in - (applist(get_pat exist_term,[a;p;(Rel lind);rterm]), - applist(get_pat sig_term,[a;p])) + (applist(exist_term,[a;p;(Rel lind);rterm]), + applist(sig_term,[a;p])) else (rterm,rty) @@ -752,7 +786,7 @@ let sig_clausale_forme env sigma sort_of_ty siglen ty = let mv = new_meta() in let rty = applist(p,[DOP0(Meta mv)]) in let (rpat,headinfo,mvenv) = sigrec_clausale_forme (siglen-1) rty in - (applist(get_pat exist_term,[a;p;DOP0(Meta mv);rpat]), + (applist(exist_term,[a;p;DOP0(Meta mv);rpat]), headinfo, (mv,a)::mvenv) in diff --git a/tactics/pattern.ml b/tactics/pattern.ml index 19d020729..04f845adc 100644 --- a/tactics/pattern.ml +++ b/tactics/pattern.ml @@ -44,15 +44,16 @@ let make_module_marker = Stock.make_module_marker (* Squeletons *) let parse_squeleton s = - Astterm.interp_constr Evd.empty (Global.env()) (parse_constr s) + let c = Astterm.interp_constr Evd.empty (Global.env()) (parse_constr s) in + (collect_metas c, c) -type marked_term = constr Stock.stocked +type marked_term = (int list * constr) Stock.stocked -let (squeleton_stock : constr Stock.stock) = +let (squeleton_stock : (int list * constr) Stock.stock) = Stock.make_stock { name = "SQUELETON"; proc = parse_squeleton } let put_squel = Stock.stock squeleton_stock -let get_squel = Stock.retrieve squeleton_stock +let get_squel_core = Stock.retrieve squeleton_stock (* Second part : Given a term with second-order variables in it, represented by Meta's, and possibly applied using XTRA[$SOAPP] to @@ -110,9 +111,11 @@ let memb_metavars m n = | (None, _) -> true | (Some mvs, n) -> List.mem n mvs +let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2 + exception PatternMatchingFailure -let somatch metavars = +let somatch_core convert metavars = let rec sorec stk sigma p t = let cT = whd_castapp t in match p,kind_of_term cT with @@ -141,16 +144,13 @@ let somatch metavars = | PRef (RVar v1), IsVar v2 when v1 = v2 -> sigma | PRef (RConst (sp1,ctxt1)), IsConst (sp2,ctxt2) - when sp1 = sp2 && Array.length ctxt1 = Array.length ctxt2 -> - array_fold_left2 (sorec stk) sigma ctxt1 ctxt2 + when sp1 = sp2 && eq_context ctxt1 ctxt2 -> sigma | PRef (RInd (sp1,ctxt1)), IsMutInd (sp2,ctxt2) - when sp1 = sp2 && Array.length ctxt1 = Array.length ctxt2 -> - array_fold_left2 (sorec stk) sigma ctxt1 ctxt2 + when sp1 = sp2 && eq_context ctxt1 ctxt2 -> sigma | PRef (RConstruct (sp1,ctxt1)), IsMutConstruct (sp2,ctxt2) - when sp1 = sp2 && Array.length ctxt1 = Array.length ctxt2 -> - array_fold_left2 (sorec stk) sigma ctxt1 ctxt2 + when sp1 = sp2 && eq_context ctxt1 ctxt2 -> sigma | PRel n1, IsRel n2 when n1 = n2 -> sigma @@ -168,6 +168,11 @@ let somatch metavars = | PBinder(BLambda,na1,c1,d1), IsLambda(na2,c2,d2) -> sorec (na2::stk) (sorec stk sigma c1 c2) d1 d2 + | PRef (RConst (sp1,ctxt1)), _ when convert <> None -> + let (env,evars) = out_some convert in + if is_conv env evars (mkConst (sp1,ctxt1)) cT then sigma + else raise PatternMatchingFailure + | _, (IsFix _ | IsMutCase _ | IsCoFix _) -> error "somatch: not implemented" @@ -175,79 +180,14 @@ let somatch metavars = in sorec [] [] -(* -let somatch metavars = - let rec sorec stk sigma p t = - let cP = whd_castapp p - and cT = whd_castapp t in - match dest_soapp_operator cP with - | Some (n,ok_args) -> - if not (memb_metavars metavars n) then error "somatch"; - let frels = Intset.elements (free_rels cT) in - if list_subset frels ok_args then - constrain (n,build_dlam ok_args stk cT) sigma - else - error "somatch" - - | None -> - match (cP,cT) with - | (DOP0(Meta n),m) -> - if not (memb_metavars metavars n) then - match m with - | DOP0(Meta m_0) -> - if n=m_0 then sigma else error "somatch" - | _ -> error "somatch" - else - let depth = List.length stk in - let frels = Intset.elements (free_rels m) in - if List.for_all (fun i -> i > depth) frels then - constrain (n,lift (-depth) m) sigma - else - error "somatch" - - | (VAR v1,VAR v2) -> - if v1 = v2 then sigma else error "somatch" - - | (Rel n1,Rel n2) -> - if n1 = n2 then sigma else error "somatch" - - | (DOP0 op1,DOP0 op2) -> - if op1 = op2 then sigma else error "somatch" - - | (DOP1(op1,c1), DOP1(op2,c2)) -> - if op1 = op2 then sorec stk sigma c1 c2 else error "somatch" - - | (DOP2(op1,c1,d1), DOP2(op2,c2,d2)) -> - if op1 = op2 then - sorec stk (sorec stk sigma c1 c2) d1 d2 - else - error "somatch" - - | (DOPN(op1,cl1), DOPN(op2,cl2)) -> - if op1 = op2 & Array.length cl1 = Array.length cl2 then - array_fold_left2 (sorec stk) sigma cl1 cl2 - else - error "somatch" - - | (DOPL(op1,cl1), DOPL(op2,cl2)) -> - if op1 = op2 & List.length cl1 = List.length cl2 then - List.fold_left2 (sorec stk) sigma cl1 cl2 - else - error "somatch" - - | (DLAM(_,c1), DLAM(na,c2)) -> - sorec (na::stk) sigma c1 c2 - - | (DLAMV(_,cl1), DLAMV(na,cl2)) -> - if Array.length cl1 = Array.length cl2 then - array_fold_left2 (sorec (na::stk)) sigma cl1 cl2 - else - error "somatch" - - | _ -> error "somatch" - in - sorec [] [] -*) + +let somatch = somatch_core None + +let dest_somatch n pat = + let mvs,m = get_pat pat in + let mvb = somatch (Some (list_uniquize mvs)) m n in + List.map (fun b -> List.assoc b mvb) mvs + let somatches n pat = let (_,m) = get_pat pat in try @@ -255,20 +195,26 @@ let somatches n pat = with e when Logic.catchable_exception e -> false -let dest_somatch n pat = +let dest_somatch_conv env sigma n pat = let mvs,m = get_pat pat in - let mvb = somatch (Some (list_uniquize mvs)) m n in - List.map (fun b -> List.assoc b mvb) mvs + somatch_core (Some (env,sigma)) (Some (list_uniquize mvs)) m n -let newsomatch n pat = let _,m = get_pat pat in somatch None m n +let somatches_conv env sigma n pat = + try + let _ = dest_somatch_conv env sigma n pat in true + with e when Logic.catchable_exception e -> + false let soinstance squel arglist = - let c = get_squel squel in - let mvs = collect_metas c in + let mvs,c = get_squel_core squel in let mvb = List.combine mvs arglist in Sosub.soexecute (Reduction.strong (fun _ _ -> Reduction.whd_meta mvb) empty_env Evd.empty c) +let get_squel m = + let mvs, c = get_squel_core m in + if mvs = [] then c else error "Not a closed squeleton, use 'soinstance'" + (* 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. @@ -425,11 +371,11 @@ let rec pattern_of_constr t = PApp (pattern_of_constr f, Array.of_list (List.map pattern_of_constr args)) | IsConst (cst_sp,ctxt) -> - PRef (RConst (cst_sp,Array.map pattern_of_constr ctxt)) + PRef (RConst (cst_sp, ctxt)) | IsMutInd (ind_sp,ctxt) -> - PRef (RInd (ind_sp,Array.map pattern_of_constr ctxt)) + PRef (RInd (ind_sp, ctxt)) | IsMutConstruct (cstr_sp,ctxt) -> - PRef (RConstruct (cstr_sp,Array.map pattern_of_constr ctxt)) + PRef (RConstruct (cstr_sp, ctxt)) | IsMutCase _ | IsFix _ | IsCoFix _ -> error "pattern_of_constr: destructors currently not supported" | IsEvar _ -> error "pattern_of_constr: an existential variable remains" diff --git a/tactics/pattern.mli b/tactics/pattern.mli index ae59ddef3..e16a8ea77 100644 --- a/tactics/pattern.mli +++ b/tactics/pattern.mli @@ -98,11 +98,38 @@ i*) (*i Devrait être une fonction de filtrage externe i*) val somatch : int list option -> Rawterm.constr_pattern -> constr -> (int * constr) list -val somatches : constr -> marked_pattern -> bool + +exception PatternMatchingFailure + +(* [dest_somatch c pat] matches [c] against [pat] and returns the resulting + assignment of metavariables; it raises [PatternMatchingFailure] if + not matchable *) + val dest_somatch : constr -> marked_pattern -> constr list +(* [somatches c pat] just tells if [c] matches against [pat] *) + +val somatches : constr -> marked_pattern -> bool + + +(* [dest_somatch_conv env sigma] matches up to conversion in + environment [(env,sgima)] when constants in pattern are concerned; + it raises [PatternMatchingFailure] if not matchable *) + +val dest_somatch_conv : + Environ.env -> 'a evar_map -> constr -> marked_pattern -> (int * constr) list + +(* [somatches_conv env sigma c pat] tells if [c] matches against [pat] + up to conversion for constants in patterns *) + +val somatches_conv : + Environ.env -> 'a evar_map -> constr -> marked_pattern -> bool + val soinstance : marked_term -> constr list -> constr +(* This works only for squeleton without metavariables *) +val get_squel : marked_term -> constr + val is_imp_term : constr -> bool (*s I implemented the following functions which test whether a term [t] diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index baae41399..6425bdc28 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -118,12 +118,9 @@ let clause_type cls gl = (* Functions concerning matching of clausal environments *) -let matches gls n m = +let matches gls n pat = let (wc,_) = startWalk gls in - try - let _ = Clenv.unify_0 [] wc m n in true - with e when Logic.catchable_exception e -> - false + somatches_conv (w_env wc) (w_Underlying wc) n pat let dest_match gls n m = let mvs = collect_metas m in diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index e7d8cff25..f863bad68 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -53,7 +53,7 @@ val matches : goal sigma -> constr -> marked_term -> bool val dest_match : goal sigma -> constr -> marked_term -> constr list *) (* The second argument is the pattern *) -val matches : goal sigma -> constr -> constr -> bool +val matches : goal sigma -> constr -> marked_pattern -> bool val dest_match : goal sigma -> constr -> constr -> constr list val allHyps : goal sigma -> clause list |