diff options
Diffstat (limited to 'tactics/pattern.ml')
| -rw-r--r-- | tactics/pattern.ml | 169 |
1 files changed, 135 insertions, 34 deletions
diff --git a/tactics/pattern.ml b/tactics/pattern.ml index 23b6da6e46..19d0207294 100644 --- a/tactics/pattern.ml +++ b/tactics/pattern.ml @@ -12,6 +12,7 @@ open Environ open Proof_trees open Stock open Clenv +open Rawterm (* The pattern table for tactics. *) @@ -21,33 +22,38 @@ open Clenv type module_mark = Stock.module_mark -type marked_term = constr Stock.stocked - -let rec whd_replmeta = function - | DOP0(XTRA("ISEVAR")) -> DOP0(Meta (new_meta())) - | DOP2(Cast,c,_) -> whd_replmeta c - | c -> c - -let raw_sopattern_of_compattern env com = - let c = Astterm.constr_of_com_pattern Evd.empty env com in - strong (fun _ _ -> whd_replmeta) env Evd.empty c +let parse_constr s = + try + Pcoq.parse_string Pcoq.Constr.constr_eoi s + with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) -> + error "Syntax error : not a construction" +(* Patterns *) let parse_pattern s = - let com = - try - Pcoq.parse_string Pcoq.Constr.constr_eoi s - with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) -> - error "Malformed pattern" - in - raw_sopattern_of_compattern (Global.env()) com + Astterm.interp_constrpattern Evd.empty (Global.env()) (parse_constr s) -let (pattern_stock : constr Stock.stock) = +type marked_pattern = (int list * constr_pattern) Stock.stocked + +let (pattern_stock : (int list * constr_pattern) Stock.stock) = Stock.make_stock { name = "PATTERN"; proc = parse_pattern } -let make_module_marker = Stock.make_module_marker pattern_stock let put_pat = Stock.stock pattern_stock let get_pat = Stock.retrieve pattern_stock +let make_module_marker = Stock.make_module_marker + +(* Squeletons *) +let parse_squeleton s = + Astterm.interp_constr Evd.empty (Global.env()) (parse_constr s) + +type marked_term = constr Stock.stocked + +let (squeleton_stock : 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 + (* Second part : Given a term with second-order variables in it, represented by Meta's, and possibly applied using XTRA[$SOAPP] to terms, this function will perform second-order, binding-preserving, @@ -103,7 +109,73 @@ let memb_metavars m n = match (m,n) with | (None, _) -> true | (Some mvs, n) -> List.mem n mvs - + +exception PatternMatchingFailure + +let somatch metavars = + let rec sorec stk sigma p t = + let cT = whd_castapp t in + match p,kind_of_term cT with + | PSoApp (n,relargs),m -> + assert (memb_metavars metavars n); + let frels = Intset.elements (free_rels cT) in + if list_subset frels relargs then + constrain (n,build_dlam relargs stk cT) sigma + else + raise PatternMatchingFailure + + | PMeta n, m -> + if not (memb_metavars metavars n) then + (*Ce cas est bizarre : comment les numéros pourraient-ils coincider*) + match m with + | IsMeta m0 when n=m0 -> sigma + | _ -> raise PatternMatchingFailure + else + let depth = List.length stk in + let frels = Intset.elements (free_rels cT) in + if List.for_all (fun i -> i > depth) frels then + constrain (n,lift (-depth) cT) sigma + else + raise PatternMatchingFailure + + | 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 + + | PRef (RInd (sp1,ctxt1)), IsMutInd (sp2,ctxt2) + when sp1 = sp2 && Array.length ctxt1 = Array.length ctxt2 -> + array_fold_left2 (sorec stk) sigma ctxt1 ctxt2 + + | PRef (RConstruct (sp1,ctxt1)), IsMutConstruct (sp2,ctxt2) + when sp1 = sp2 && Array.length ctxt1 = Array.length ctxt2 -> + array_fold_left2 (sorec stk) sigma ctxt1 ctxt2 + + | PRel n1, IsRel n2 when n1 = n2 -> sigma + + | PSort (RProp c1), IsSort (Prop c2) when c1 = c2 -> sigma + + | PSort RType, IsSort (Type _) -> sigma + + | PApp (c1,arg1), IsAppL (c2,arg2) -> + array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) + arg1 (Array.of_list arg2) + + | PBinder(BProd,na1,c1,d1), IsProd(na2,c2,d2) -> + sorec (na2::stk) (sorec stk sigma c1 c2) d1 d2 + + | PBinder(BLambda,na1,c1,d1), IsLambda(na2,c2,d2) -> + sorec (na2::stk) (sorec stk sigma c1 c2) d1 d2 + + | _, (IsFix _ | IsMutCase _ | IsCoFix _) -> + error "somatch: not implemented" + + | _ -> raise PatternMatchingFailure + + in + sorec [] [] +(* let somatch metavars = let rec sorec stk sigma p t = let cP = whd_castapp p @@ -175,26 +247,27 @@ let somatch metavars = | _ -> error "somatch" in sorec [] [] - +*) let somatches n pat = - let m = get_pat pat in + let (_,m) = get_pat pat in try let _ = somatch None m n in true with e when Logic.catchable_exception e -> false let dest_somatch n pat = - let m = get_pat pat in - let mvs = collect_metas m in + 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 soinstance pat arglist = - let m = get_pat pat in - let mvs = collect_metas m in +let newsomatch n pat = let _,m = get_pat pat in somatch None m n + +let soinstance squel arglist = + let c = get_squel squel in + let mvs = collect_metas c in let mvb = List.combine mvs arglist in Sosub.soexecute (Reduction.strong (fun _ _ -> Reduction.whd_meta mvb) - empty_env Evd.empty m) + empty_env Evd.empty c) (* I implemented the following functions which test whether a term t is an inductive but non-recursive type, a general conjuction, a @@ -300,18 +373,18 @@ let is_unit_type t = op2bool (match_with_unit_type t) inductive binary relation R, so that R has only one constructor stablishing its reflexivity. *) +let refl_rel_pat1 = put_pat mmk "(A : ?)(x:A)(? A x x)" +let refl_rel_pat2 = put_pat mmk "(x : ?)(? x x)" + let match_with_equation t = let (hdapp,args) = decomp_app t in match (kind_of_term hdapp) with | IsMutInd ind -> - let constr_types = - Global.mind_lc_without_abstractions ind in - let refl_rel_term1 = put_pat mmk "(A : ?)(x:A)(? A x x)" in - let refl_rel_term2 = put_pat mmk "(x : ?)(? x x)" in + let constr_types = Global.mind_lc_without_abstractions ind in let nconstr = Global.mind_nconstr ind in if nconstr = 1 && - (somatches constr_types.(0) refl_rel_term1 || - somatches constr_types.(0) refl_rel_term2) + (somatches constr_types.(0) refl_rel_pat1 || + somatches constr_types.(0) refl_rel_pat2) then Some (hdapp,args) else @@ -335,3 +408,31 @@ let is_nottype t = op2bool (match_with_nottype t) let is_imp_term = function | DOP2(Prod,_,DLAM(_,b)) -> not (dependent (Rel 1) b) | _ -> false + +let rec pattern_of_constr t = + match kind_of_term t with + | IsRel n -> PRel n + | IsMeta n -> PMeta n + | IsVar id -> PRef (RVar id) + | IsSort (Prop c) -> PSort (RProp c) + | IsSort (Type _) -> PSort RType + | IsCast (c,t) -> pattern_of_constr c + | IsProd (na,c,b) -> + PBinder (BProd,na,pattern_of_constr c,pattern_of_constr b) + | IsLambda (na,c,b) -> + PBinder (BLambda,na,pattern_of_constr c,pattern_of_constr b) + | IsAppL (f,args) -> + 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)) + | IsMutInd (ind_sp,ctxt) -> + PRef (RInd (ind_sp,Array.map pattern_of_constr ctxt)) + | IsMutConstruct (cstr_sp,ctxt) -> + PRef (RConstruct (cstr_sp,Array.map pattern_of_constr ctxt)) + | IsMutCase _ | IsFix _ | IsCoFix _ -> + error "pattern_of_constr: destructors currently not supported" + | IsEvar _ -> error "pattern_of_constr: an existential variable remains" + | IsAbst _ | IsXtra _ -> anomaly "No longer supported" + + |