diff options
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 201 |
1 files changed, 80 insertions, 121 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 10cfbe58..58df9abc 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) @@ -19,20 +21,21 @@ open Typeclasses_errors 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) = +let declare_generalizable_ident table {CAst.loc;v=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" + ((Id.print 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" + ((Id.print id++str" is already declared as a generalizable identifier")) else Id.Pred.add id table let add_generalizable gen table = @@ -48,7 +51,7 @@ let cache_generalizable_type (_,(local,cmd)) = let load_generalizable_type _ (_,(local,cmd)) = generalizable_table := add_generalizable cmd !generalizable_table -let in_generalizable : bool * Id.t Loc.located list option -> obj = +let in_generalizable : bool * Misctypes.lident list option -> obj = declare_object {(default_object "GENERALIZED-IDENT") with load_function = load_generalizable_type; cache_function = cache_generalizable_type; @@ -78,8 +81,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 " ++ Id.print id) let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let found loc id bdvars l = @@ -90,103 +93,51 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = else ungeneralizable loc id else l in - let rec aux bdvars l c = match c with - | CRef (Ident (loc,id),_) -> found loc id bdvars l - | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id),_) :: _, [], [])) when not (Id.Set.mem id bdvars) -> - Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c - | c -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c + let rec aux bdvars l c = match CAst.(c.v) with + | CRef ({CAst.v=Ident id},_) -> found c.CAst.loc id bdvars l + | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef ({CAst.v=Ident id},_) } :: _, [], [], [])) when not (Id.Set.mem id bdvars) -> + Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c + | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c let ids_of_names l = - List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l + List.fold_left (fun acc x -> match x.CAst.v with Name na -> na :: acc | Anonymous -> acc) [] l -let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) = +let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) = let rec aux bdvars l c = match c with - ((LocalRawAssum (n, _, c)) :: tl) -> + ((CLocalAssum (n, _, c)) :: tl) -> let bound = ids_of_names n in let l' = free_vars_of_constr_expr c ~bound:bdvars l in aux (Id.Set.union (ids_of_list bound) bdvars) l' tl - | ((LocalRawDef (n, c)) :: tl) -> - let bound = match snd n with Anonymous -> [] | Name n -> [n] in + | ((CLocalDef (n, c, t)) :: tl) -> + let bound = match n.CAst.v with Anonymous -> [] | Name n -> [n] in let l' = free_vars_of_constr_expr c ~bound:bdvars l in - aux (Id.Set.union (ids_of_list bound) bdvars) l' tl + let l'' = Option.fold_left (fun l t -> free_vars_of_constr_expr t ~bound:bdvars l) l' t in + aux (Id.Set.union (ids_of_list bound) bdvars) l'' tl - | LocalPattern _ :: tl -> assert false + | CLocalPattern _ :: tl -> assert false | [] -> bdvars, l in aux bound l binders -let add_name_to_ids set na = - match na with - | Anonymous -> set - | Name id -> Id.Set.add id set - let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) = - let rec vars bound vs = function - | GVar (loc,id) -> + let rec vars bound vs c = match DAst.get c with + | GVar id -> + let loc = c.CAst.loc in if is_freevar bound (Global.env ()) id then - if Id.List.mem_assoc id vs then vs - else (id, loc) :: vs + if List.exists (fun {CAst.v} -> Id.equal v id) vs then vs + else CAst.(make ?loc id) :: vs else vs - | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args) - | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> - let vs' = vars bound vs ty in - let bound' = add_name_to_ids bound na in - vars bound' vs' c - | GCases (loc,sty,rtntypopt,tml,pl) -> - let vs1 = vars_option bound vs rtntypopt in - let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in - List.fold_left (vars_pattern bound) vs2 pl - | GLetTuple (loc,nal,rtntyp,b,c) -> - let vs1 = vars_return_type bound vs rtntyp in - let vs2 = vars bound vs1 b in - let bound' = List.fold_left add_name_to_ids bound nal in - vars bound' vs2 c - | GIf (loc,c,rtntyp,b1,b2) -> - let vs1 = vars_return_type bound vs rtntyp in - let vs2 = vars bound vs1 c in - let vs3 = vars bound vs2 b1 in - vars bound vs3 b2 - | GRec (loc,fk,idl,bl,tyl,bv) -> - let bound' = Array.fold_right Id.Set.add idl bound in - let vars_fix i vs fid = - let vs1,bound1 = - List.fold_left - (fun (vs,bound) (na,k,bbd,bty) -> - let vs' = vars_option bound vs bbd in - let vs'' = vars bound vs' bty in - let bound' = add_name_to_ids bound na in - (vs'',bound') - ) - (vs,bound') - bl.(i) - in - let vs2 = vars bound1 vs1 tyl.(i) in - vars bound1 vs2 bv.(i) - in - Array.fold_left_i vars_fix vs idl - | GCast (loc,c,k) -> let v = vars bound vs c in - (match k with CastConv t | CastVM t -> vars bound v t | _ -> v) - | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs - - and vars_pattern bound vs (loc,idl,p,c) = - let bound' = List.fold_right Id.Set.add idl bound in - vars bound' vs c - - and vars_option bound vs = function None -> vs | Some p -> vars bound vs p - - and vars_return_type bound vs (na,tyopt) = - let bound' = add_name_to_ids bound na in - vars_option bound' vs tyopt + | _ -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c in fun rt -> let vars = List.rev (vars bound [] rt) in - List.iter (fun (id, loc) -> + List.iter (fun {CAst.loc;v=id} -> if not (Id.Set.mem id allowed || find_generalizable_ident id) then ungeneralizable loc id) vars; 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 @@ -197,18 +148,18 @@ let combine_params avoid fn applied needed = let named, applied = List.partition (function - (t, Some (loc, ExplByName id)) -> - let is_id (_, decl) = match get_name decl with + (t, Some {CAst.loc;v=ExplByName id}) -> + 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: " ++ Id.print id); true | _ -> false) applied in let named = List.map - (fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false) + (fun x -> match x with (t, Some {CAst.loc;v=ExplByName id}) -> id, t | _ -> assert false) named in let is_unset (_, decl) = match decl with @@ -237,39 +188,43 @@ 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 (_, decl) -> - let id' = next_name_away_from (get_name decl) avoid in - (CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid) + let id' = next_name_away_from (RelDecl.get_name decl) avoid in + (CAst.make @@ CRef (CAst.make @@ Ident id',None), Id.Set.add id' avoid) let destClassApp cl = - match cl with - | 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 + let open CAst in + let loc = cl.loc in + match cl.v with + | CApp ((None, { v = CRef (ref, inst) }), l) -> CAst.make ?loc (ref, List.map fst l, inst) + | CAppExpl ((None, ref, inst), l) -> CAst.make ?loc (ref, l, inst) + | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst) | _ -> raise Not_found let destClassAppExpl cl = - match cl with - | CApp (loc, (None, CRef (ref, inst)), l) -> loc, ref, l, inst - | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst + let open CAst in + let loc = cl.loc in + match cl.v with + | CApp ((None, { v = CRef (ref, inst) } ), l) -> CAst.make ?loc (ref, l, inst) + | CRef (ref, inst) -> CAst.make ?loc:cl.loc (ref, [], inst) | _ -> raise Not_found let implicit_application env ?(allow_partial=true) f ty = let is_class = try - let (_, r, _, _ as clapp) = destClassAppExpl ty in - let (loc, qid) = qualid_of_reference r in - let gr = Nametab.locate qid in + let ({CAst.v=(r, _, _)} as clapp) = destClassAppExpl ty in + let qid = qualid_of_reference r in + let gr = Nametab.locate qid.CAst.v in if Typeclasses.is_class gr then Some (clapp, gr) else None with Not_found -> None in match is_class with | None -> ty, env - | Some ((loc, id, par, inst), gr) -> + | Some ({CAst.loc;v=(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 @@ -287,9 +242,15 @@ 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, inst), args), avoid + CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid in c, avoid +let warn_ignoring_implicit_status = + CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits" + (fun na -> + strbrk "Ignoring implicit status of product binder " ++ + Name.print na ++ strbrk " and following binders") + let implicits_of_glob_constr ?(with_products=true) l = let add_impl i na bk l = match bk with | Implicit -> @@ -305,20 +266,18 @@ let implicits_of_glob_constr ?(with_products=true) l = let abs na bk b = add_impl i na bk (aux (succ i) b) in - match c with - | GProd (loc, na, bk, t, b) -> - if with_products then abs na bk b - else - let () = match bk with - | Implicit -> - Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++ - pr_name na ++ strbrk " and following binders") - | _ -> () - in [] - | GLambda (loc, na, bk, t, b) -> abs na bk b - | GLetIn (loc, na, t, b) -> aux i b - | GRec (_, fix_kind, nas, args, tys, bds) -> - let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in - List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) - | _ -> [] + match DAst.get c with + | GProd (na, bk, t, b) -> + if with_products then abs na bk b + else + let () = match bk with + | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc + | _ -> () + in [] + | GLambda (na, bk, t, b) -> abs na bk b + | GLetIn (na, b, t, c) -> aux i b + | GRec (fix_kind, nas, args, tys, bds) -> + let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in + List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) + | _ -> [] in aux 1 l |