diff options
Diffstat (limited to 'pretyping/matching.ml')
| -rw-r--r-- | pretyping/matching.ml | 29 |
1 files changed, 17 insertions, 12 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 091aa0b8b..870db85ee 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -217,36 +217,37 @@ let pmatches c p = snd (matches_core None true c p) let special_meta = (-1) (* Tells if it is an authorized occurrence and if the instance is closed *) -let authorized_occ pat c mk_ctx next = +let authorized_occ closed pat c mk_ctx next = try let sigma = extended_matches pat c in - if not (List.for_all (fun (_,c) -> closed0 c) (snd sigma)) then next () + if closed && not (List.for_all (fun (_,c) -> closed0 c) (snd sigma)) + then next () else sigma, mk_ctx (mkMeta special_meta), next with PatternMatchingFailure -> next () (* Tries to match a subterm of [c] with [pat] *) -let rec sub_match ?(partial_app=false) pat c = +let sub_match ?(partial_app=false) ?(closed=true) pat c = let rec aux c mk_ctx next = match kind_of_term c with | Cast (c1,k,c2) -> - authorized_occ pat c mk_ctx (fun () -> + authorized_occ closed pat c mk_ctx (fun () -> let mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in try_aux [c1] mk_ctx next) | Lambda (x,c1,c2) -> - authorized_occ pat c mk_ctx (fun () -> + authorized_occ closed pat c mk_ctx (fun () -> let mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in try_aux [c1;c2] mk_ctx next) | Prod (x,c1,c2) -> - authorized_occ pat c mk_ctx (fun () -> + authorized_occ closed pat c mk_ctx (fun () -> let mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in try_aux [c1;c2] mk_ctx next) | LetIn (x,c1,t,c2) -> - authorized_occ pat c mk_ctx (fun () -> + authorized_occ closed pat c mk_ctx (fun () -> let mk_ctx = function [c1;c2] -> mkLetIn (x,c1,t,c2) | _ -> assert false in try_aux [c1;c2] mk_ctx next) | App (c1,lc) -> - authorized_occ pat c mk_ctx (fun () -> + authorized_occ closed pat c mk_ctx (fun () -> let topdown = true in if partial_app then if topdown then @@ -274,13 +275,13 @@ let rec sub_match ?(partial_app=false) pat c = mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in try_aux (c1::Array.to_list lc) mk_ctx next) | Case (ci,hd,c1,lc) -> - authorized_occ pat c mk_ctx (fun () -> + authorized_occ closed pat c mk_ctx (fun () -> let mk_ctx le = mk_ctx (mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))) in try_aux (c1::Array.to_list lc) mk_ctx next) | Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> - authorized_occ pat c mk_ctx next + authorized_occ closed pat c mk_ctx next (* Tries [sub_match] for all terms in the list *) and try_aux lc mk_ctx next = @@ -302,8 +303,12 @@ let match_appsubterm pat c = sub_match ~partial_app:true pat c let match_subterm_gen app pat c = sub_match ~partial_app:app pat c -let is_matching pat n = - try let _ = matches pat n in true +let is_matching pat c = + try let _ = matches pat c in true + with PatternMatchingFailure -> false + +let is_matching_appsubterm ?(closed=true) pat c = + try let _ = sub_match ~partial_app:true ~closed pat c in true with PatternMatchingFailure -> false let matches_conv env sigma c p = |