diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typeclasses.ml | 80 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 19 |
2 files changed, 85 insertions, 14 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 89e0fc93d7..128d3a6a71 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -41,6 +41,11 @@ let classes_transparent_state_ref = ref (fun () -> assert false) let register_classes_transparent_state = (:=) classes_transparent_state_ref let classes_transparent_state () = !classes_transparent_state_ref () +let solve_instanciation_problem = ref (fun _ _ _ -> assert false) + +let resolve_one_typeclass env evm t = + !solve_instanciation_problem env evm t + type rels = constr list (* This module defines type-classes *) @@ -55,8 +60,9 @@ type typeclass = { cl_props : rel_context; (* The method implementaions as projections. *) - cl_projs : (name * bool * constant option) list; + cl_projs : (name * int option option * constant option) list; } + module Gmap = Fmap.Make(RefOrdered) type typeclasses = typeclass Gmap.t @@ -68,7 +74,7 @@ type instance = { -1 for discard, 0 for none, mutable to avoid redeclarations when multiple rebuild_object happen. *) is_global: int; - is_impl: global_reference; + is_impl: global_reference; } type instances = (instance Gmap.t) Gmap.t @@ -224,6 +230,45 @@ let class_input : typeclass -> obj = let add_class cl = Lib.add_anonymous_leaf (class_input cl) +(** Build the subinstances hints. *) + +let check_instance env sigma c = + try + let (evd, c) = resolve_one_typeclass env sigma + (Retyping.get_type_of env sigma c) in + Evd.is_empty (Evd.undefined_evars evd) + with _ -> false + +let build_subclasses ~check env sigma glob pri = + let rec aux pri c = + let ty = Retyping.get_type_of env sigma c in + match class_of_constr ty with + | None -> [] + | Some (rels, (tc, args)) -> + let instapp = Reductionops.whd_beta sigma (appvectc c (Termops.extended_rel_vect 0 rels)) in + let projargs = Array.of_list (args @ [instapp]) in + let projs = list_map_filter + (fun (n, b, proj) -> + match b with + | None -> None + | Some pri' -> + let proj = Option.get proj in + let body = it_mkLambda_or_LetIn (mkApp (mkConst proj, projargs)) rels in + if check && check_instance env sigma body then None + else + let pri = + match pri, pri' with + | Some p, Some p' -> Some (p + p') + | Some p, None -> Some (p + 1) + | _, _ -> None + in + Some (ConstRef proj, pri, body)) tc.cl_projs + in + let declare_proj hints (cref, pri, body) = + let rest = aux pri body in + hints @ (pri, body) :: rest + in List.fold_left declare_proj [] projs + in aux pri (constr_of_global glob) (* * instances persistent object @@ -268,9 +313,14 @@ let discharge_instance (_, (action, inst)) = let is_local i = i.is_global = -1 +let add_instance check inst = + add_instance_hint (constr_of_global inst.is_impl) (is_local inst) inst.is_pri; + List.iter (fun (pri, c) -> add_instance_hint c (is_local inst) pri) + (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) + (Global.env ()) Evd.empty inst.is_impl inst.is_pri) + let rebuild_instance (action, inst) = - if action = AddInstance then - add_instance_hint inst.is_impl (is_local inst) inst.is_pri; + if action = AddInstance then add_instance true inst; (action, inst) let classify_instance (action, inst) = @@ -280,7 +330,7 @@ let classify_instance (action, inst) = let load_instance (_, (action, inst) as ai) = cache_instance ai; if action = AddInstance then - add_instance_hint inst.is_impl (is_local inst) inst.is_pri + add_instance_hint (constr_of_global inst.is_impl) (is_local inst) inst.is_pri let instance_input : instance_action * instance -> obj = declare_object @@ -295,12 +345,25 @@ let instance_input : instance_action * instance -> obj = let add_instance i = Lib.add_anonymous_leaf (instance_input (AddInstance, i)); - add_instance_hint i.is_impl (is_local i) i.is_pri + add_instance true i let remove_instance i = Lib.add_anonymous_leaf (instance_input (RemoveInstance, i)); remove_instance_hint i.is_impl +let declare_instance pri local glob = + let c = constr_of_global glob in + let ty = Retyping.get_type_of (Global.env ()) Evd.empty c in + match class_of_constr ty with + | Some (rels, (tc, args) as _cl) -> + add_instance (new_instance tc pri (not local) glob) +(* let path, hints = build_subclasses (not local) (Global.env ()) Evd.empty glob in *) +(* let entries = List.map (fun (path, pri, c) -> (pri, local, path, c)) hints in *) +(* Auto.add_hints local [typeclasses_db] (Auto.HintsResolveEntry entries); *) +(* Auto.add_hints local [typeclasses_db] *) +(* (Auto.HintsCutEntry (PathSeq (PathStar (PathAtom PathAny), path))) *) + | None -> () + open Declarations let add_constant_class cst = @@ -381,6 +444,7 @@ let is_implicit_arg k = | InternalHole -> true | _ -> false + (* 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] @@ -416,11 +480,7 @@ let has_typeclasses evd = evd false let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false) -let solve_instanciation_problem = ref (fun _ _ _ -> assert false) let resolve_typeclasses ?(onlyargs=false) ?(split=true) ?(fail=true) env evd = if not (has_typeclasses evd) then evd else !solve_instanciations_problem env evd onlyargs split fail - -let resolve_one_typeclass env evm t = - !solve_instanciation_problem env evm t diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index e4db68fbcd..a00d23a9b2 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -34,8 +34,9 @@ type typeclass = { (** The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions or simply undefined if - no name is provided. The boolean indicates subclasses. *) - cl_projs : (name * bool * constant option) list; + no name is provided. The [int option option] indicates subclasses whose hint has + the given priority. *) + cl_projs : (name * int option option * constant option) list; } type instance @@ -93,10 +94,20 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u val register_classes_transparent_state : (unit -> transparent_state) -> unit val classes_transparent_state : unit -> transparent_state -val register_add_instance_hint : (global_reference -> bool (* local? *) -> int option -> unit) -> unit +val register_add_instance_hint : (constr -> bool (* local? *) -> int option -> unit) -> unit val register_remove_instance_hint : (global_reference -> unit) -> unit -val add_instance_hint : global_reference -> bool -> int option -> unit +val add_instance_hint : constr -> bool -> int option -> unit val remove_instance_hint : global_reference -> unit val solve_instanciations_problem : (env -> evar_map -> bool -> bool -> bool -> evar_map) ref val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref + +val declare_instance : int option -> bool -> global_reference -> unit + + +(** Build the subinstances hints for a given typeclass object. + check tells if we should check for existence of the + subinstances and add only the missing ones. *) + +val build_subclasses : check:bool -> env -> evar_map -> global_reference -> int option (* priority *) -> + (int option * constr) list |