diff options
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 148 |
1 files changed, 68 insertions, 80 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 7e5815acd1..1496712bbc 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -31,19 +31,12 @@ type 'a hint_info_gen = type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen -let typeclasses_unique_solutions = ref false -let set_typeclasses_unique_solutions d = (:=) typeclasses_unique_solutions d -let get_typeclasses_unique_solutions () = !typeclasses_unique_solutions - -open Goptions - -let _ = - declare_bool_option - { optdepr = false; - optname = "check that typeclasses proof search returns unique solutions"; - optkey = ["Typeclasses";"Unique";"Solutions"]; - optread = get_typeclasses_unique_solutions; - optwrite = set_typeclasses_unique_solutions; } +let get_typeclasses_unique_solutions = + Goptions.declare_bool_option_and_ref + ~depr:false + ~name:"check that typeclasses proof search returns unique solutions" + ~key:["Typeclasses";"Unique";"Solutions"] + ~value:false let (add_instance_hint, add_instance_hint_hook) = Hook.make () let add_instance_hint id = Hook.get add_instance_hint id @@ -131,12 +124,14 @@ let typeclass_univ_instance (cl, u) = let class_info c = try GlobRef.Map.find c !classes - with Not_found -> not_a_class (Global.env()) (EConstr.of_constr (printable_constr_of_global c)) + with Not_found -> + let env = Global.env() in + not_a_class env (Evd.from_env env) (EConstr.of_constr (printable_constr_of_global c)) let global_class_of_constr env sigma c = try let gr, u = Termops.global_of_constr sigma c in - class_info gr, u - with Not_found -> not_a_class env c + GlobRef.Map.find gr !classes, u + with Not_found -> not_a_class env sigma c let dest_class_app env sigma c = let cl, args = EConstr.decompose_app sigma c in @@ -166,6 +161,21 @@ let rec is_class_type evd c = let is_class_evar evd evi = is_class_type evd evi.Evd.evar_concl +let is_class_constr sigma c = + try let gr, u = Termops.global_of_constr sigma c in + GlobRef.Map.mem gr !classes + with Not_found -> false + +let rec is_maybe_class_type evd c = + let c, _ = Termops.decompose_app_vect evd c in + match EConstr.kind evd c with + | Prod (_, _, t) -> is_maybe_class_type evd t + | Cast (t, _, _) -> is_maybe_class_type evd t + | Evar _ -> true + | _ -> is_class_constr evd c + +let () = Hook.set Evd.is_maybe_typeclass_hook (fun evd c -> is_maybe_class_type evd (EConstr.of_constr c)) + (* * classes persistent object *) @@ -279,7 +289,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = (fun () -> incr i; Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i)) in - let ty, ctx = Global.type_of_global_in_context env glob in + let ty, ctx = Typeops.type_of_global_in_context env glob in let inst, ctx = UnivGen.fresh_instance_from ctx None in let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in @@ -320,7 +330,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } = hints @ (path', info, body) :: rest in List.fold_left declare_proj [] projs in - let term = UnivGen.constr_of_global_univ (glob, inst) in + let term = Constr.mkRef (glob, inst) in (*FIXME subclasses should now get substituted for each particular instance of the polymorphic superclass *) aux pri term ty [glob] @@ -419,28 +429,40 @@ let remove_instance i = Lib.add_anonymous_leaf (instance_input (RemoveInstance, i)); remove_instance_hint i.is_impl -let declare_instance info local glob = - let ty, _ = Global.type_of_global_in_context (Global.env ()) glob in +let warning_not_a_class = + let name = "not-a-class" in + let category = "typeclasses" in + CWarnings.create ~name ~category (fun (n, ty) -> + let env = Global.env () in + let evd = Evd.from_env env in + Pp.(str "Ignored instance declaration for “" + ++ Nametab.pr_global_env Id.Set.empty n + ++ str "”: “" + ++ Termops.Internal.print_constr_env env evd (EConstr.of_constr ty) + ++ str "” is not a class") + ) + +let declare_instance ?(warn = false) info local glob = + let ty, _ = Typeops.type_of_global_in_context (Global.env ()) glob in let info = Option.default {hint_priority = None; hint_pattern = None} info in match class_of_constr Evd.empty (EConstr.of_constr ty) with | Some (rels, ((tc,_), args) as _cl) -> assert (not (isVarRef glob) || local); add_instance (new_instance tc info (not local) glob) - | None -> () + | None -> if warn then warning_not_a_class (glob, ty) let add_class cl = add_class cl; List.iter (fun (n, inst, body) -> - match inst with - | Some (Backward, info) -> - (match body with - | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") - | Some b -> declare_instance (Some info) false (ConstRef b)) - | _ -> ()) - cl.cl_projs + match inst with + | Some (Backward, info) -> + (match body with + | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance") + | Some b -> declare_instance ~warn:true (Some info) false (ConstRef b)) + | _ -> ()) + cl.cl_projs - (* * interface functions *) @@ -481,63 +503,29 @@ let instances r = let is_class gr = GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes -(* To embed a boolean for resolvability status. - This is essentially a hack to mark which evars correspond to - goals and do not need to be resolved when we have nested [resolve_all_evars] - calls (e.g. when doing apply in an External hint in typeclass_instances). - Would be solved by having real evars-as-goals. - - Nota: we will only check the resolvability status of undefined evars. - *) - -let resolvable = Proofview.Unsafe.typeclass_resolvable - -let set_resolvable s b = - if b then Store.remove s resolvable - else Store.set s resolvable () - -let is_resolvable evi = - assert (match evi.evar_body with Evar_empty -> true | _ -> false); - Option.is_empty (Store.get evi.evar_extra resolvable) - -let mark_resolvability_undef b evi = - if is_resolvable evi == (b : bool) then evi - else - let t = set_resolvable evi.evar_extra b in - { evi with evar_extra = t } - -let mark_resolvability b evi = - assert (match evi.evar_body with Evar_empty -> true | _ -> false); - mark_resolvability_undef b evi - -let mark_unresolvable evi = mark_resolvability false evi -let mark_resolvable evi = mark_resolvability true evi - open Evar_kinds -type evar_filter = Evar.t -> Evar_kinds.t -> bool +type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool + +let make_unresolvables filter evd = + let tcs = Evd.get_typeclass_evars evd in + Evd.set_typeclass_evars evd (Evar.Set.filter (fun x -> not (filter x)) tcs) let all_evars _ _ = true -let all_goals _ = function VarInstance _ | GoalEvar -> true | _ -> false +let all_goals _ source = + match Lazy.force source with + | VarInstance _ | GoalEvar -> true + | _ -> false + let no_goals ev evi = not (all_goals ev evi) -let no_goals_or_obligations _ = function +let no_goals_or_obligations _ source = + match Lazy.force source with | VarInstance _ | GoalEvar | QuestionMark _ -> false | _ -> true -let mark_resolvability filter b sigma = - let map ev evi = - if filter ev (snd evi.evar_source) then mark_resolvability_undef b evi - else evi - in - Evd.raw_map_undefined map sigma - -let mark_unresolvables ?(filter=all_evars) sigma = mark_resolvability filter false sigma -let mark_resolvables ?(filter=all_evars) sigma = mark_resolvability filter true sigma - let has_typeclasses filter evd = - let check ev evi = - filter ev (snd evi.evar_source) && is_resolvable evi && is_class_evar evd evi - in - Evar.Map.exists check (Evd.undefined_map evd) + let tcs = get_typeclass_evars evd in + let check ev = filter ev (lazy (snd (Evd.find evd ev).evar_source)) in + Evar.Set.exists check tcs let get_solve_all_instances, solve_all_instances_hook = Hook.make () @@ -548,7 +536,7 @@ let solve_all_instances env evd filter unique split fail = (* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *) (* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *) -let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) +let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) ?(split=true) ?(fail=true) env evd = - if fast_path && not (has_typeclasses filter evd) then evd + if not (has_typeclasses filter evd) then evd else solve_all_instances env evd filter unique split fail |