From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- pretyping/constr_matching.ml | 494 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 494 insertions(+) create mode 100644 pretyping/constr_matching.ml (limited to 'pretyping/constr_matching.ml') diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml new file mode 100644 index 00000000..a6e2bc19 --- /dev/null +++ b/pretyping/constr_matching.ml @@ -0,0 +1,494 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + let () = if Id.Map.mem n names then warn_bound_meta n in + (names, Id.Map.add n x terms) + +let add_binders na1 na2 (names, terms as subst) = match na1, na2 with +| Name id1, Name id2 -> + if Id.Map.mem id1 names then + let () = warn_bound_bound id1 in + (names, terms) + else + let names = Id.Map.add id1 id2 names in + let () = if Id.Map.mem id1 terms then warn_bound_again id1 in + (names, terms) +| _ -> subst + +let rec build_lambda vars stk m = match vars with +| [] -> + let len = List.length stk in + lift (-1 * len) m +| n :: vars -> + (* change [ x1 ... xn y z1 ... zm |- t ] into + [ x1 ... xn z1 ... zm |- lam y. t ] *) + let len = List.length stk in + let init i = + if i < pred n then mkRel (i + 2) + else if Int.equal i (pred n) then mkRel 1 + else mkRel (i + 1) + in + let m = substl (List.init len init) m in + let pre, suf = List.chop (pred n) stk in + match suf with + | [] -> assert false + | (_, na, t) :: suf -> + let map i = if i > n then pred i else i in + let vars = List.map map vars in + (** Check that the abstraction is legal *) + let frels = free_rels t in + let brels = List.fold_right Int.Set.add vars Int.Set.empty in + let () = if not (Int.Set.subset frels brels) then raise PatternMatchingFailure in + (** Create the abstraction *) + let m = mkLambda (na, t, m) in + build_lambda vars (pre @ suf) m + +let rec extract_bound_aux k accu frels stk = match stk with +| [] -> accu +| (na1, na2, _) :: stk -> + if Int.Set.mem k frels then + begin match na1 with + | Name id -> + let () = assert (match na2 with Anonymous -> false | Name _ -> true) in + let () = if Id.Set.mem id accu then raise PatternMatchingFailure in + extract_bound_aux (k + 1) (Id.Set.add id accu) frels stk + | Anonymous -> raise PatternMatchingFailure + end + else extract_bound_aux (k + 1) accu frels stk + +let extract_bound_vars frels stk = + extract_bound_aux 1 Id.Set.empty frels stk + +let dummy_constr = mkProp + +let make_renaming ids = function +| (Name id, Name _, _) -> + begin + try mkRel (List.index Id.equal id ids) + with Not_found -> dummy_constr + end +| _ -> dummy_constr + +let merge_binding allow_bound_rels stk n cT subst = + let c = match stk with + | [] -> (* Optimization *) + ([], cT) + | _ -> + let frels = free_rels cT in + if allow_bound_rels then + let vars = extract_bound_vars frels stk in + let ordered_vars = Id.Set.elements vars in + let rename binding = make_renaming ordered_vars binding in + let renaming = List.map rename stk in + (ordered_vars, substl renaming cT) + else + let depth = List.length stk in + let min_elt = try Int.Set.min_elt frels with Not_found -> succ depth in + if depth < min_elt then + ([], lift (- depth) cT) + else raise PatternMatchingFailure + in + constrain n c subst + +let matches_core env sigma convert allow_partial_app allow_bound_rels pat c = + let convref ref c = + match ref, kind_of_term c with + | VarRef id, Var id' -> Names.id_eq id id' + | ConstRef c, Const (c',_) -> Names.eq_constant c c' + | IndRef i, Ind (i', _) -> Names.eq_ind i i' + | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' + | _, _ -> + (if convert then + let sigma,c' = Evd.fresh_global env sigma ref in + is_conv env sigma c' c + else false) + in + let rec sorec stk env subst p t = + let cT = strip_outer_cast t in + match p,kind_of_term cT with + | PSoApp (n,args),m -> + let fold (ans, seen) = function + | PRel n -> + let () = if Int.Set.mem n seen then error "Non linear second-order pattern" in + (n :: ans, Int.Set.add n seen) + | _ -> error "Only bound indices allowed in second order pattern matching." + in + let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in + let frels = free_rels cT in + if Int.Set.subset frels relset then + constrain n ([], build_lambda relargs stk cT) subst + else + raise PatternMatchingFailure + + | PMeta (Some n), m -> merge_binding allow_bound_rels stk n cT subst + + | PMeta None, m -> subst + + | PRef (VarRef v1), Var v2 when Id.equal v1 v2 -> subst + + | PVar v1, Var v2 when Id.equal v1 v2 -> subst + + | PRef ref, _ when convref ref cT -> subst + + | PRel n1, Rel n2 when Int.equal n1 n2 -> subst + + | PSort GProp, Sort (Prop Null) -> subst + + | PSort GSet, Sort (Prop Pos) -> subst + + | PSort (GType _), Sort (Type _) -> subst + + | PApp (p, [||]), _ -> sorec stk env subst p t + + | PApp (PApp (h, a1), a2), _ -> + sorec stk env subst (PApp(h,Array.append a1 a2)) t + + | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app -> + (let diff = Array.length args2 - Array.length args1 in + if diff >= 0 then + let args21, args22 = Array.chop diff args2 in + let c = mkApp(c2,args21) in + let subst = + match meta with + | None -> subst + | Some n -> merge_binding allow_bound_rels stk n c subst in + Array.fold_left2 (sorec stk env) subst args1 args22 + else (* Might be a projection on the right *) + match kind_of_term c2 with + | Proj (pr, c) when not (Projection.unfolded pr) -> + (try let term = Retyping.expand_projection env sigma pr c (Array.to_list args2) in + sorec stk env subst p term + with Retyping.RetypeError _ -> raise PatternMatchingFailure) + | _ -> raise PatternMatchingFailure) + + | PApp (c1,arg1), App (c2,arg2) -> + (match c1, kind_of_term c2 with + | PRef (ConstRef r), Proj (pr,c) when not (eq_constant r (Projection.constant pr)) + || Projection.unfolded pr -> + raise PatternMatchingFailure + | PProj (pr1,c1), Proj (pr,c) -> + if Projection.equal pr1 pr then + try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c) arg1 arg2 + with Invalid_argument _ -> raise PatternMatchingFailure + else raise PatternMatchingFailure + | _, Proj (pr,c) when not (Projection.unfolded pr) -> + (try let term = Retyping.expand_projection env sigma pr c (Array.to_list arg2) in + sorec stk env subst p term + with Retyping.RetypeError _ -> raise PatternMatchingFailure) + | _, _ -> + try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2 + with Invalid_argument _ -> raise PatternMatchingFailure) + + | PApp (PRef (ConstRef c1), _), Proj (pr, c2) + when Projection.unfolded pr || not (eq_constant c1 (Projection.constant pr)) -> + raise PatternMatchingFailure + + | PApp (c, args), Proj (pr, c2) -> + (try let term = Retyping.expand_projection env sigma pr c2 [] in + sorec stk env subst p term + with Retyping.RetypeError _ -> raise PatternMatchingFailure) + + | PProj (p1,c1), Proj (p2,c2) when Projection.equal p1 p2 -> + sorec stk env subst c1 c2 + + | PProd (na1,c1,d1), Prod(na2,c2,d2) -> + sorec ((na1,na2,c2)::stk) (Environ.push_rel (na2,None,c2) env) + (add_binders na1 na2 (sorec stk env subst c1 c2)) d1 d2 + + | PLambda (na1,c1,d1), Lambda(na2,c2,d2) -> + sorec ((na1,na2,c2)::stk) (Environ.push_rel (na2,None,c2) env) + (add_binders na1 na2 (sorec stk env subst c1 c2)) d1 d2 + + | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) -> + sorec ((na1,na2,t2)::stk) (Environ.push_rel (na2,Some c2,t2) env) + (add_binders na1 na2 (sorec stk env subst c1 c2)) d1 d2 + + | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> + let ctx,b2 = decompose_lam_n_assum ci.ci_cstr_ndecls.(0) b2 in + let ctx',b2' = decompose_lam_n_assum ci.ci_cstr_ndecls.(1) b2' in + let n = rel_context_length ctx in + let n' = rel_context_length ctx' in + if noccur_between 1 n b2 && noccur_between 1 n' b2' then + let s = + List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx in + let s' = + List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx' in + let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in + sorec s' (Environ.push_rel_context ctx' env) + (sorec s (Environ.push_rel_context ctx env) (sorec stk env subst a1 a2) b1 b2) b1' b2' + else + raise PatternMatchingFailure + + | PCase (ci1,p1,a1,br1), Case (ci2,p2,a2,br2) -> + let n2 = Array.length br2 in + let () = match ci1.cip_ind with + | None -> () + | Some ind1 -> + (** ppedrot: Something spooky going here. The comparison used to be + the generic one, so I may have broken something. *) + if not (eq_ind ind1 ci2.ci_ind) then raise PatternMatchingFailure + in + let () = + if not ci1.cip_extensible && not (Int.equal (List.length br1) n2) + then raise PatternMatchingFailure + in + let chk_branch subst (j,n,c) = + (* (ind,j+1) is normally known to be a correct constructor + and br2 a correct match over the same inductive *) + assert (j < n2); + sorec stk env subst c br2.(j) + in + let chk_head = sorec stk env (sorec stk env subst a1 a2) p1 p2 in + List.fold_left chk_branch chk_head br1 + + | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst + | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst + | _ -> raise PatternMatchingFailure + + in + sorec [] env (Id.Map.empty, Id.Map.empty) pat c + +let matches_core_closed env sigma convert allow_partial_app pat c = + let names, subst = matches_core env sigma convert allow_partial_app false pat c in + (names, Id.Map.map snd subst) + +let extended_matches env sigma = matches_core env sigma false true true + +let matches env sigma pat c = snd (matches_core_closed env sigma false true pat c) + +let special_meta = (-1) + +type matching_result = + { m_sub : bound_ident_map * patvar_map; + m_ctx : constr; } + +let mkresult s c n = IStream.Cons ( { m_sub=s; m_ctx=c; } , (IStream.thunk n) ) + +let isPMeta = function PMeta _ -> true | _ -> false + +let matches_head env sigma pat c = + let head = + match pat, kind_of_term c with + | PApp (c1,arg1), App (c2,arg2) -> + if isPMeta c1 then c else + let n1 = Array.length arg1 in + if n1 < Array.length arg2 then mkApp (c2,Array.sub arg2 0 n1) else c + | c1, App (c2,arg2) when not (isPMeta c1) -> c2 + | _ -> c in + matches env sigma pat head + +(* Tells if it is an authorized occurrence and if the instance is closed *) +let authorized_occ env sigma partial_app closed pat c mk_ctx next = + try + let subst = matches_core_closed env sigma false partial_app pat c in + if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd subst) + then next () + else mkresult subst (mk_ctx (mkMeta special_meta)) next + with PatternMatchingFailure -> next () + +(* Tries to match a subterm of [c] with [pat] *) +let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = + let rec aux env c mk_ctx next = + match kind_of_term c with + | Cast (c1,k,c2) -> + let next_mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in + let next () = try_aux [env] [c1] next_mk_ctx next in + authorized_occ env sigma partial_app closed pat c mk_ctx next + | Lambda (x,c1,c2) -> + let next_mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in + let next () = + let env' = Environ.push_rel (x,None,c1) env in + try_aux [env;env'] [c1; c2] next_mk_ctx next in + authorized_occ env sigma partial_app closed pat c mk_ctx next + | Prod (x,c1,c2) -> + let next_mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in + let next () = + let env' = Environ.push_rel (x,None,c1) env in + try_aux [env;env'] [c1;c2] next_mk_ctx next in + authorized_occ env sigma partial_app closed pat c mk_ctx next + | LetIn (x,c1,t,c2) -> + let next_mk_ctx = function + | [c1;c2] -> mkLetIn (x,c1,t,c2) + | _ -> assert false + in + let next () = + let env' = Environ.push_rel (x,Some c1,t) env in + try_aux [env;env'] [c1;c2] next_mk_ctx next in + authorized_occ env sigma partial_app closed pat c mk_ctx next + | App (c1,lc) -> + let next () = + let topdown = true in + if partial_app then + if topdown then + let lc1 = Array.sub lc 0 (Array.length lc - 1) in + let app = mkApp (c1,lc1) in + let mk_ctx = function + | [app';c] -> mk_ctx (mkApp (app',[|c|])) + | _ -> assert false in + try_aux [env] [app;Array.last lc] mk_ctx next + else + let rec aux2 app args next = + match args with + | [] -> + let mk_ctx le = + mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in + try_aux [env] (c1::Array.to_list lc) mk_ctx next + | arg :: args -> + let app = mkApp (app,[|arg|]) in + let next () = aux2 app args next in + let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in + aux env app mk_ctx next in + aux2 c1 (Array.to_list lc) next + else + let mk_ctx le = + mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in + try_aux [env] (c1::Array.to_list lc) mk_ctx next + in + authorized_occ env sigma partial_app closed pat c mk_ctx next + | Case (ci,hd,c1,lc) -> + let next_mk_ctx = function + | [] -> assert false + | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) + in + let next () = try_aux [env] (c1 :: Array.to_list lc) next_mk_ctx next in + authorized_occ env sigma partial_app closed pat c mk_ctx next + | Fix (indx,(names,types,bodies)) -> + let nb_fix = Array.length types in + let next_mk_ctx le = + let (ntypes,nbodies) = CList.chop nb_fix le in + mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in + let next () = + try_aux + [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in + authorized_occ env sigma partial_app closed pat c mk_ctx next + | CoFix (i,(names,types,bodies)) -> + let nb_fix = Array.length types in + let next_mk_ctx le = + let (ntypes,nbodies) = CList.chop nb_fix le in + mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in + let next () = + try_aux [env] ((Array.to_list types)@(Array.to_list bodies)) next_mk_ctx next in + authorized_occ env sigma partial_app closed pat c mk_ctx next + | Proj (p,c') -> + let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in + let next () = + if partial_app then + try + let term = Retyping.expand_projection env sigma p c' [] in + aux env term mk_ctx next + with Retyping.RetypeError _ -> raise PatternMatchingFailure + else + try_aux [env] [c'] next_mk_ctx next in + authorized_occ env sigma partial_app closed pat c mk_ctx next + | Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ -> + authorized_occ env sigma partial_app closed pat c mk_ctx next + + (* Tries [sub_match] for all terms in the list *) + and try_aux lenv lc mk_ctx next = + let rec try_sub_match_rec lacc lenv lc = + match lenv, lc with + | _, [] -> next () + | env :: tlenv, c::tl -> + let mk_ctx ce = mk_ctx (List.rev_append lacc (ce::tl)) in + let next () = + let env' = match tlenv with [] -> lenv | _ -> tlenv in + try_sub_match_rec (c::lacc) env' tl + in + aux env c mk_ctx next + | _ -> assert false in + try_sub_match_rec [] lenv lc in + let lempty () = IStream.Nil in + let result () = aux env c (fun x -> x) lempty in + IStream.thunk result + +let match_subterm env sigma pat c = sub_match env sigma pat c + +let match_appsubterm env sigma pat c = + sub_match ~partial_app:true env sigma pat c + +let match_subterm_gen env sigma app pat c = + sub_match ~partial_app:app env sigma pat c + +let is_matching env sigma pat c = + try let _ = matches env sigma pat c in true + with PatternMatchingFailure -> false + +let is_matching_head env sigma pat c = + try let _ = matches_head env sigma pat c in true + with PatternMatchingFailure -> false + +let is_matching_appsubterm ?(closed=true) env sigma pat c = + let results = sub_match ~partial_app:true ~closed env sigma pat c in + not (IStream.is_empty results) + +let matches_conv env sigma c p = + snd (matches_core_closed env sigma true false c p) + +let is_matching_conv env sigma pat n = + try let _ = matches_conv env sigma pat n in true + with PatternMatchingFailure -> false -- cgit v1.2.3