diff options
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 44 |
1 files changed, 25 insertions, 19 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index a1a3be70f1..b48db9ac54 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -17,12 +17,14 @@ open Glob_term open Constrexpr open Libnames open Typeclasses -open Typeclasses_errors open Pp open Libobject open Nameops open Context.Rel.Declaration +exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *) +let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m)) + module RelDecl = Context.Rel.Declaration (*i*) @@ -58,7 +60,7 @@ let in_generalizable : bool * Misctypes.lident list option -> obj = classify_function = (fun (local, _ as obj) -> if local then Dispose else Keep obj) } -let declare_generalizable local gen = +let declare_generalizable ~local gen = Lib.add_anonymous_leaf (in_generalizable (local, gen)) let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table @@ -238,13 +240,19 @@ let implicit_application env ?(allow_partial=true) f ty = let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in if not (Int.equal needlen applen) then - Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd + mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd end; let pars = List.rev (List.combine ci rd) in let args, avoid = combine_params avoid f par pars in 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 -> @@ -260,20 +268,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 DAst.get c with - | GProd (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 " ++ - Name.print na ++ strbrk " and following binders") - | _ -> () - 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) - | _ -> [] + 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 |