From d399671f3f1a667a47540071feecb20baf115418 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 11 Oct 2015 11:21:23 +0200 Subject: Constr_matching: renaming misleading name stk into ctx. --- pretyping/constr_matching.ml | 92 ++++++++++++++++++++++---------------------- 1 file changed, 46 insertions(+), 46 deletions(-) (limited to 'pretyping') diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index a0493777a5..585be9c720 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -80,21 +80,21 @@ let add_binders na1 na2 (names, terms as subst) = match na1, na2 with (names, terms) | _ -> subst -let rec build_lambda vars stk m = match vars with +let rec build_lambda vars ctx m = match vars with | [] -> - let len = List.length stk in + let len = List.length ctx 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 len = List.length ctx 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 + let pre, suf = List.chop (pred n) ctx in match suf with | [] -> assert false | (_, na, t) :: suf -> @@ -108,21 +108,21 @@ let rec build_lambda vars stk m = match vars with 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 +let rec extract_bound_aux k accu frels ctx = match ctx with | [] -> accu -| (na1, na2, _) :: stk -> +| (na1, na2, _) :: ctx -> 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 + extract_bound_aux (k + 1) (Id.Set.add id accu) frels ctx | Anonymous -> raise PatternMatchingFailure end - else extract_bound_aux (k + 1) accu frels stk + else extract_bound_aux (k + 1) accu frels ctx -let extract_bound_vars frels stk = - extract_bound_aux 1 Id.Set.empty frels stk +let extract_bound_vars frels ctx = + extract_bound_aux 1 Id.Set.empty frels ctx let dummy_constr = mkProp @@ -134,20 +134,20 @@ let make_renaming ids = function end | _ -> dummy_constr -let merge_binding allow_bound_rels stk n cT subst = - let c = match stk with +let merge_binding allow_bound_rels ctx n cT subst = + let c = match ctx with | [] -> (* Optimization *) ([], cT) | _ -> let frels = free_rels cT in if allow_bound_rels then - let vars = extract_bound_vars frels stk in + let vars = extract_bound_vars frels ctx 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 + let renaming = List.map rename ctx in (ordered_vars, substl renaming cT) else - let depth = List.length stk in + let depth = List.length ctx in let min_elt = try Int.Set.min_elt frels with Not_found -> succ depth in if depth < min_elt then ([], lift (- depth) cT) @@ -168,7 +168,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c = is_conv env sigma c' c else false) in - let rec sorec stk env subst p t = + let rec sorec ctx env subst p t = let cT = strip_outer_cast t in match p,kind_of_term cT with | PSoApp (n,args),m -> @@ -181,11 +181,11 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c = 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 + constrain n ([], build_lambda relargs ctx cT) subst else raise PatternMatchingFailure - | PMeta (Some n), m -> merge_binding allow_bound_rels stk n cT subst + | PMeta (Some n), m -> merge_binding allow_bound_rels ctx n cT subst | PMeta None, m -> subst @@ -203,10 +203,10 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c = | PSort (GType _), Sort (Type _) -> subst - | PApp (p, [||]), _ -> sorec stk env subst p t + | PApp (p, [||]), _ -> sorec ctx env subst p t | PApp (PApp (h, a1), a2), _ -> - sorec stk env subst (PApp(h,Array.append a1 a2)) t + sorec ctx 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 @@ -216,13 +216,13 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c = 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 + | Some n -> merge_binding allow_bound_rels ctx n c subst in + Array.fold_left2 (sorec ctx 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 + sorec ctx env subst p term with Retyping.RetypeError _ -> raise PatternMatchingFailure) | _ -> raise PatternMatchingFailure) @@ -233,15 +233,15 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c = 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 + try Array.fold_left2 (sorec ctx env) (sorec ctx 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 + sorec ctx env subst p term with Retyping.RetypeError _ -> raise PatternMatchingFailure) | _, _ -> - try Array.fold_left2 (sorec stk env) (sorec stk env subst c1 c2) arg1 arg2 + try Array.fold_left2 (sorec ctx env) (sorec ctx env subst c1 c2) arg1 arg2 with Invalid_argument _ -> raise PatternMatchingFailure) | PApp (PRef (ConstRef c1), _), Proj (pr, c2) @@ -250,37 +250,37 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c = | PApp (c, args), Proj (pr, c2) -> (try let term = Retyping.expand_projection env sigma pr c2 [] in - sorec stk env subst p term + sorec ctx 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 + sorec ctx 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 + sorec ((na1,na2,c2)::ctx) (Environ.push_rel (na2,None,c2) env) + (add_binders na1 na2 (sorec ctx 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 + sorec ((na1,na2,c2)::ctx) (Environ.push_rel (na2,None,c2) env) + (add_binders na1 na2 (sorec ctx 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 + sorec ((na1,na2,t2)::ctx) (Environ.push_rel (na2,Some c2,t2) env) + (add_binders na1 na2 (sorec ctx 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 + let ctx_b2,b2 = decompose_lam_n_assum ci.ci_cstr_ndecls.(0) b2 in + let ctx_b2',b2' = decompose_lam_n_assum ci.ci_cstr_ndecls.(1) b2' in + let n = rel_context_length ctx_b2 in + let n' = rel_context_length ctx_b2' 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 f l (na,_,t) = (Anonymous,na,t)::l in + let ctx_br = List.fold_left f ctx ctx_b2 in + let ctx_br' = List.fold_left f ctx ctx_b2' 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' + sorec ctx_br' (Environ.push_rel_context ctx_b2' env) + (sorec ctx_br (Environ.push_rel_context ctx_b2 env) + (sorec ctx env subst a1 a2) b1 b2) b1' b2' else raise PatternMatchingFailure @@ -301,9 +301,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat 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) + sorec ctx env subst c br2.(j) in - let chk_head = sorec stk env (sorec stk env subst a1 a2) p1 p2 in + let chk_head = sorec ctx env (sorec ctx 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 -- cgit v1.2.3 From 2e07ecfce221840047b2f95c93acdb79a4fe0985 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 11 Oct 2015 13:42:11 +0200 Subject: Fixing obviously untested fold_glob_constr and iter_glob_constr. --- pretyping/glob_ops.ml | 51 +++++++++++++++++++++++---------------------------- 1 file changed, 23 insertions(+), 28 deletions(-) (limited to 'pretyping') diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 454d64f01b..5b02c8cd15 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -183,37 +183,32 @@ let map_glob_constr_left_to_right f = function let map_glob_constr = map_glob_constr_left_to_right -let fold_glob_constr f acc = - let rec fold acc = function +let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt + +let fold_glob_constr f acc = function | GVar _ -> acc - | GApp (_,c,args) -> List.fold_left fold (fold acc c) args + | GApp (_,c,args) -> List.fold_left f (f acc c) args | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) | GLetIn (_,_,b,c) -> - fold (fold acc b) c + f (f acc b) c | GCases (_,_,rtntypopt,tml,pl) -> - List.fold_left fold_pattern - (List.fold_left fold (Option.fold_left fold acc rtntypopt) (List.map fst tml)) - pl - | GLetTuple (_,_,rtntyp,b,c) -> - fold (fold (fold_return_type acc rtntyp) b) c - | GIf (_,c,rtntyp,b1,b2) -> - fold (fold (fold (fold_return_type acc rtntyp) c) b1) b2 - | GRec (_,_,_,bl,tyl,bv) -> - let acc = Array.fold_left - (List.fold_left (fun acc (na,k,bbd,bty) -> - fold (Option.fold_left fold acc bbd) bty)) acc bl in - Array.fold_left fold (Array.fold_left fold acc tyl) bv - | GCast (_,c,k) -> - let r = match k with - | CastConv t | CastVM t | CastNative t -> fold acc t | CastCoerce -> acc - in - fold r c - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc - - and fold_pattern acc (_,idl,p,c) = fold acc c - - and fold_return_type acc (na,tyopt) = Option.fold_left fold acc tyopt - - in fold acc + let fold_pattern acc (_,idl,p,c) = f acc c in + List.fold_left fold_pattern + (List.fold_left f (Option.fold_left f acc rtntypopt) (List.map fst tml)) + pl + | GLetTuple (_,_,rtntyp,b,c) -> + f (f (fold_return_type f acc rtntyp) b) c + | GIf (_,c,rtntyp,b1,b2) -> + f (f (f (fold_return_type f acc rtntyp) c) b1) b2 + | GRec (_,_,_,bl,tyl,bv) -> + let acc = Array.fold_left + (List.fold_left (fun acc (na,k,bbd,bty) -> + f (Option.fold_left f acc bbd) bty)) acc bl in + Array.fold_left f (Array.fold_left f acc tyl) bv + | GCast (_,c,k) -> + let acc = match k with + | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in + f acc c + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc let iter_glob_constr f = fold_glob_constr (fun () -> f) () -- cgit v1.2.3 From ae5305a4837cce3c7fd61b92ce8110ac66ec2750 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 11 Oct 2015 15:05:10 +0200 Subject: Refining 0c320e79ba30 in fixing interpretation of constr under binders which was broken after it became possible to have binding names themselves bound to ltac variables (2fcc458af16b). Interpretation was corrected, but error message was damaged. --- pretyping/pretyping.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6306739b7a..746b4000ee 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -322,8 +322,8 @@ let ltac_interp_name_env k0 lvar env = push_rel_context ctxt env let invert_ltac_bound_name lvar env id0 id = - let id = Id.Map.find id lvar.ltac_idents in - try mkRel (pi1 (lookup_rel_id id (rel_context env))) + let id' = Id.Map.find id lvar.ltac_idents in + try mkRel (pi1 (lookup_rel_id id' (rel_context env))) with Not_found -> errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++ str " depends on pattern variable name " ++ pr_id id ++ -- cgit v1.2.3 From e9995f6e9f9523d4738d9ee494703b6f96bf995d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 11 Oct 2015 14:36:29 +0200 Subject: Fixing untimely unexpected warning "Collision between bound variables" (#4317). Collecting the bound variables is now done on the glob_constr, before interpretation, so that only variables given explicitly by the user are used for binding bound variables. --- pretyping/constr_matching.ml | 46 ++++++++++++++++----------------- pretyping/constr_matching.mli | 9 ++++--- pretyping/glob_ops.ml | 60 +++++++++++++++++++++++++++++++++++++++++++ pretyping/glob_ops.mli | 1 + 4 files changed, 90 insertions(+), 26 deletions(-) (limited to 'pretyping') diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 585be9c720..19c85c9e27 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -56,10 +56,6 @@ let warn_bound_meta name = let warn_bound_bound name = msg_warning (str "Collision between bound variables of name " ++ pr_id name) -let warn_bound_again name = - msg_warning (str "Collision between bound variable " ++ pr_id name ++ - str " and another bound variable of same name.") - let constrain n (ids, m as x) (names, terms as subst) = try let (ids', m') = Id.Map.find n terms in @@ -69,16 +65,17 @@ let constrain n (ids, m as x) (names, terms as subst) = 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 add_binders na1 na2 binding_vars (names, terms as subst) = + match na1, na2 with + | Name id1, Name id2 when Id.Set.mem id1 binding_vars -> + 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_meta id1 in + (names, terms) + | _ -> subst let rec build_lambda vars ctx m = match vars with | [] -> @@ -155,7 +152,8 @@ let merge_binding allow_bound_rels ctx n cT subst = in constrain n c subst -let matches_core env sigma convert allow_partial_app allow_bound_rels pat c = +let matches_core env sigma convert allow_partial_app allow_bound_rels + (binding_vars,pat) c = let convref ref c = match ref, kind_of_term c with | VarRef id, Var id' -> Names.id_eq id id' @@ -258,15 +256,15 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels pat c = | PProd (na1,c1,d1), Prod(na2,c2,d2) -> sorec ((na1,na2,c2)::ctx) (Environ.push_rel (na2,None,c2) env) - (add_binders na1 na2 (sorec ctx env subst c1 c2)) d1 d2 + (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PLambda (na1,c1,d1), Lambda(na2,c2,d2) -> sorec ((na1,na2,c2)::ctx) (Environ.push_rel (na2,None,c2) env) - (add_binders na1 na2 (sorec ctx env subst c1 c2)) d1 d2 + (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) -> sorec ((na1,na2,t2)::ctx) (Environ.push_rel (na2,Some c2,t2) env) - (add_binders na1 na2 (sorec ctx env subst c1 c2)) d1 d2 + (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) -> let ctx_b2,b2 = decompose_lam_n_assum ci.ci_cstr_ndecls.(0) b2 in @@ -319,7 +317,8 @@ let matches_core_closed env sigma convert allow_partial_app pat c = 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 matches env sigma pat c = + snd (matches_core_closed env sigma false true (Id.Set.empty,pat) c) let special_meta = (-1) @@ -464,10 +463,10 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = 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_subterm env sigma pat c = sub_match env sigma (Id.Set.empty,pat) c let match_appsubterm env sigma pat c = - sub_match ~partial_app:true env sigma pat c + sub_match ~partial_app:true env sigma (Id.Set.empty,pat) c let match_subterm_gen env sigma app pat c = sub_match ~partial_app:app env sigma pat c @@ -481,11 +480,12 @@ let is_matching_head env sigma pat c = with PatternMatchingFailure -> false let is_matching_appsubterm ?(closed=true) env sigma pat c = + let pat = (Id.Set.empty,pat) in 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 matches_conv env sigma p c = + snd (matches_core_closed env sigma true false (Id.Set.empty,p) c) let is_matching_conv env sigma pat n = try let _ = matches_conv env sigma pat n in true diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 67854a893d..b9dcb0af26 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -41,7 +41,8 @@ val matches_head : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map variables or metavariables have the same name, the metavariable, or else the rightmost bound variable, takes precedence *) val extended_matches : - env -> Evd.evar_map -> constr_pattern -> constr -> bound_ident_map * extended_patvar_map + env -> Evd.evar_map -> Tacexpr.binding_bound_vars * constr_pattern -> + constr -> bound_ident_map * extended_patvar_map (** [is_matching pat c] just tells if [c] matches against [pat] *) val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool @@ -72,8 +73,10 @@ val match_subterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_ val match_appsubterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t (** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *) -val match_subterm_gen : env -> Evd.evar_map -> bool (** true = with app context *) -> - constr_pattern -> constr -> matching_result IStream.t +val match_subterm_gen : env -> Evd.evar_map -> + bool (** true = with app context *) -> + Tacexpr.binding_bound_vars * constr_pattern -> constr -> + matching_result IStream.t (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches against [pat] taking partial subterms into consideration *) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 5b02c8cd15..3a76e8bd74 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -8,6 +8,7 @@ open Util open Names +open Nameops open Globnames open Misctypes open Glob_term @@ -323,6 +324,65 @@ let free_glob_vars = let vs = vars Id.Set.empty Id.Set.empty rt in Id.Set.elements vs +let add_and_check_ident id set = + if Id.Set.mem id set then + Pp.(msg_warning + (str "Collision between bound variables of name " ++ Id.print id)); + Id.Set.add id set + +let bound_glob_vars = + let rec vars bound = function + | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_) as c -> + let bound = name_fold add_and_check_ident na bound in + fold_glob_constr vars bound c + | GCases (loc,sty,rtntypopt,tml,pl) -> + let bound = vars_option bound rtntypopt in + let bound = + List.fold_left (fun bound (tm,_) -> vars bound tm) bound tml in + List.fold_left vars_pattern bound pl + | GLetTuple (loc,nal,rtntyp,b,c) -> + let bound = vars_return_type bound rtntyp in + let bound = vars bound b in + let bound = List.fold_right (name_fold add_and_check_ident) nal bound in + vars bound c + | GIf (loc,c,rtntyp,b1,b2) -> + let bound = vars_return_type bound rtntyp in + let bound = vars bound c in + let bound = vars bound b1 in + vars bound b2 + | GRec (loc,fk,idl,bl,tyl,bv) -> + let bound = Array.fold_right Id.Set.add idl bound in + let vars_fix i bound fid = + let bound = + List.fold_left + (fun bound (na,k,bbd,bty) -> + let bound = vars_option bound bbd in + let bound = vars bound bty in + name_fold add_and_check_ident na bound + ) + bound + bl.(i) + in + let bound = vars bound tyl.(i) in + vars bound bv.(i) + in + Array.fold_left_i vars_fix bound idl + | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GVar _) -> bound + | GApp _ | GCast _ as c -> fold_glob_constr vars bound c + + and vars_pattern bound (loc,idl,p,c) = + let bound = List.fold_right add_and_check_ident idl bound in + vars bound c + + and vars_option bound = function None -> bound | Some p -> vars bound p + + and vars_return_type bound (na,tyopt) = + let bound = name_fold add_and_check_ident na bound in + vars_option bound tyopt + in + fun rt -> + vars Id.Set.empty rt + (** Mapping of names in binders *) (* spiwack: I used a smartmap-style kind of mapping here, because the diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index e514fd529e..25746323fb 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -38,6 +38,7 @@ val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit val occur_glob_constr : Id.t -> glob_constr -> bool val free_glob_vars : glob_constr -> Id.t list +val bound_glob_vars : glob_constr -> Id.Set.t val loc_of_glob_constr : glob_constr -> Loc.t (** [map_pattern_binders f m c] applies [f] to all the binding names -- cgit v1.2.3 From a479aa6e8dbd1dda1af2412f8c1e1ff40f0d5a0b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 12 Oct 2015 12:57:23 +0200 Subject: Fix rechecking of applications: it can be given ill-typed terms. Fixes math-classes. --- pretyping/evarsolve.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index a2189d5e4f..754ad8f588 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -130,6 +130,8 @@ let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd = (* We retype applications to ensure the universe constraints are collected *) +exception IllTypedInstance of env * types * types + let recheck_applications conv_algo env evdref t = let rec aux env t = match kind_of_term t with @@ -146,7 +148,7 @@ let recheck_applications conv_algo env evdref t = aux (succ i) (subst1 args.(i) codom) | UnifFailure (evd, reason) -> Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom)) - | _ -> assert false + | _ -> raise (IllTypedInstance (env, ty, argsty.(i))) else () in aux 0 fty | _ -> @@ -1134,8 +1136,6 @@ let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (e else raise (CannotProject (evd,ev1')) -exception IllTypedInstance of env * types * types - let check_evar_instance evd evk1 body conv_algo = let evi = Evd.find evd evk1 in let evenv = evar_env evi in -- cgit v1.2.3