diff options
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 62 |
1 files changed, 33 insertions, 29 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index e304725d46..77a8ed680a 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,7 +9,7 @@ (*i*) open Names open Decl_kinds -open Errors +open CErrors open Util open Glob_term open Constrexpr @@ -20,18 +20,21 @@ open Pp open Libobject open Nameops open Misctypes +open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (*i*) let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident" let declare_generalizable_ident table (loc,id) = if not (Id.equal id (root_of_id id)) then - user_err_loc(loc,"declare_generalizable_ident", - (pr_id id ++ str + user_err ~loc ~hdr:"declare_generalizable_ident" + ((pr_id id ++ str " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _")); if Id.Pred.mem id table then - user_err_loc(loc,"declare_generalizable_ident", - (pr_id id++str" is already declared as a generalizable identifier")) + user_err ~loc ~hdr:"declare_generalizable_ident" + ((pr_id id++str" is already declared as a generalizable identifier")) else Id.Pred.add id table let add_generalizable gen table = @@ -77,8 +80,8 @@ let is_freevar ids env x = (* Auxiliary functions for the inference of implicitly quantified variables. *) let ungeneralizable loc id = - user_err_loc (loc, "Generalization", - str "Unbound and ungeneralizable variable " ++ pr_id id) + user_err ~loc ~hdr:"Generalization" + (str "Unbound and ungeneralizable variable " ++ pr_id id) let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let found loc id bdvars l = @@ -111,6 +114,7 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) = let l' = free_vars_of_constr_expr c ~bound:bdvars l in aux (Id.Set.union (ids_of_list bound) bdvars) l' tl + | LocalPattern _ :: tl -> assert false | [] -> bdvars, l in aux bound l binders @@ -184,7 +188,7 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp vars let rec make_fresh ids env x = - if is_freevar ids env x then x else make_fresh ids env (Nameops.lift_subscript x) + if is_freevar ids env x then x else make_fresh ids env (Nameops.increment_subscript x) let next_name_away_from na avoid = match na with @@ -196,12 +200,12 @@ let combine_params avoid fn applied needed = List.partition (function (t, Some (loc, ExplByName id)) -> - let is_id (_, (na, _, _)) = match na with + let is_id (_, decl) = match RelDecl.get_name decl with | Name id' -> Id.equal id id' | Anonymous -> false in if not (List.exists is_id needed) then - user_err_loc (loc,"",str "Wrong argument name: " ++ Nameops.pr_id id); + user_err ~loc (str "Wrong argument name: " ++ Nameops.pr_id id); true | _ -> false) applied in @@ -209,22 +213,22 @@ let combine_params avoid fn applied needed = (fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false) named in - let is_unset (_, (_, b, _)) = match b with - | None -> true - | Some _ -> false + let is_unset (_, decl) = match decl with + | LocalAssum _ -> true + | LocalDef _ -> false in let needed = List.filter is_unset needed in let rec aux ids avoid app need = match app, need with [], [] -> List.rev ids, avoid - | app, (_, (Name id, _, _)) :: need when Id.List.mem_assoc id named -> + | app, (_, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need when Id.List.mem_assoc id named -> aux (Id.List.assoc id named :: ids) avoid app need - | (x, None) :: app, (None, (Name id, _, _)) :: need -> + | (x, None) :: app, (None, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need -> aux (x :: ids) avoid app need - | _, (Some cl, (_, _, _) as d) :: need -> + | _, (Some cl, _ as d) :: need -> let t', avoid' = fn avoid d in aux (t' :: ids) avoid' app need @@ -235,31 +239,31 @@ let combine_params avoid fn applied needed = aux (t' :: ids) avoid' app need | (x,_) :: _, [] -> - user_err_loc (Constrexpr_ops.constr_loc x,"",str "Typeclass does not expect more arguments") + user_err ~loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments") in aux [] avoid applied needed let combine_params_freevar = - fun avoid (_, (na, _, _)) -> - let id' = next_name_away_from na avoid in + fun avoid (_, decl) -> + let id' = next_name_away_from (RelDecl.get_name decl) avoid in (CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid) let destClassApp cl = match cl with - | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, List.map fst l - | CAppExpl (loc, (None, ref,_), l) -> loc, ref, l - | CRef (ref,_) -> loc_of_reference ref, ref, [] + | CApp (loc, (None, CRef (ref, inst)), l) -> loc, ref, List.map fst l, inst + | CAppExpl (loc, (None, ref, inst), l) -> loc, ref, l, inst + | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst | _ -> raise Not_found let destClassAppExpl cl = match cl with - | CApp (loc, (None, CRef (ref,_)), l) -> loc, ref, l - | CRef (ref,_) -> loc_of_reference ref, ref, [] + | CApp (loc, (None, CRef (ref, inst)), l) -> loc, ref, l, inst + | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst | _ -> raise Not_found let implicit_application env ?(allow_partial=true) f ty = let is_class = try - let (loc, r, _ as clapp) = destClassAppExpl ty in + let (_, r, _, _ as clapp) = destClassAppExpl ty in let (loc, qid) = qualid_of_reference r in let gr = Nametab.locate qid in if Typeclasses.is_class gr then Some (clapp, gr) else None @@ -267,7 +271,7 @@ let implicit_application env ?(allow_partial=true) f ty = in match is_class with | None -> ty, env - | Some ((loc, id, par), gr) -> + | Some ((loc, id, par, inst), gr) -> let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in let c, avoid = let c = class_info gr in @@ -285,7 +289,7 @@ let implicit_application env ?(allow_partial=true) f ty = end; let pars = List.rev (List.combine ci rd) in let args, avoid = combine_params avoid f par pars in - CAppExpl (loc, (None, id, None), args), avoid + CAppExpl (loc, (None, id, inst), args), avoid in c, avoid let implicits_of_glob_constr ?(with_products=true) l = @@ -309,7 +313,7 @@ let implicits_of_glob_constr ?(with_products=true) l = else let () = match bk with | Implicit -> - msg_warning (strbrk "Ignoring implicit status of product binder " ++ + Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++ pr_name na ++ strbrk " and following binders") | _ -> () in [] |