diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typeclasses.ml | 74 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 18 |
2 files changed, 41 insertions, 51 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index c74ed19a8b..a391a785cc 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -20,6 +20,21 @@ open Typeclasses_errors open Libobject (*i*) +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 set_typeclasses_unique_solutions = + declare_bool_option + { optsync = true; + 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 (add_instance_hint, add_instance_hint_hook) = Hook.make () let add_instance_hint id = Hook.get add_instance_hint id @@ -32,10 +47,10 @@ let set_typeclass_transparency gr local c = Hook.get set_typeclass_transparency let (classes_transparent_state, classes_transparent_state_hook) = Hook.make () let classes_transparent_state () = Hook.get classes_transparent_state () -let solve_instantiation_problem = ref (fun _ _ _ -> assert false) +let solve_instantiation_problem = ref (fun _ _ _ _ -> assert false) -let resolve_one_typeclass env evm t = - !solve_instantiation_problem env evm t +let resolve_one_typeclass ?(unique=get_typeclasses_unique_solutions ()) env evm t = + !solve_instantiation_problem env evm t unique type direction = Forward | Backward @@ -54,6 +69,8 @@ type typeclass = { cl_projs : (Name.t * (direction * int option) option * constant option) list; cl_strict : bool; + + cl_unique : bool; } type typeclasses = typeclass Refmap.t @@ -177,7 +194,8 @@ let subst_class (subst,cl) = cl_context = do_subst_context cl.cl_context; cl_props = do_subst_ctx cl.cl_props; cl_projs = do_subst_projs cl.cl_projs; - cl_strict = cl.cl_strict } + cl_strict = cl.cl_strict; + cl_unique = cl.cl_unique } let discharge_class (_,cl) = let repl = Lib.replacement_context () in @@ -223,6 +241,7 @@ let discharge_class (_,cl) = cl_props = props; cl_projs = List.smartmap discharge_proj cl.cl_projs; cl_strict = cl.cl_strict; + cl_unique = cl.cl_unique } let rebuild_class cl = @@ -409,36 +428,6 @@ let add_class cl = open Declarations - -let add_constant_class cst = - let ty = Universes.unsafe_type_of_global (ConstRef cst) in - let ctx, arity = decompose_prod_assum ty in - let tc = - { cl_impl = ConstRef cst; - cl_context = (List.map (const None) ctx, ctx); - cl_props = [(Anonymous, None, arity)]; - cl_projs = []; - cl_strict = false; - } - in add_class tc; - set_typeclass_transparency (EvalConstRef cst) false false - -let add_inductive_class ind = - let mind, oneind = Global.lookup_inductive ind in - let k = - let ctx = oneind.mind_arity_ctxt in - let inst = Univ.UContext.instance mind.mind_universes in - let ty = Inductive.type_of_inductive_knowing_parameters - (push_rel_context ctx (Global.env ())) - ((mind,oneind),inst) - (Array.map (fun x -> lazy x) (Termops.extended_rel_vect 0 ctx)) - in - { cl_impl = IndRef ind; - cl_context = List.map (const None) ctx, ctx; - cl_props = [Anonymous, None, ty]; - cl_projs = []; - cl_strict = false } - in add_class k (* * interface functions @@ -497,7 +486,7 @@ let is_instance = function | _ -> false let is_implicit_arg = function -| Evar_kinds.GoalEvar _ -> false +| Evar_kinds.GoalEvar -> false | _ -> true (* match k with *) (* ImplicitArg (ref, (n, id), b) -> true *) @@ -538,10 +527,10 @@ open Evar_kinds type evar_filter = existential_key -> Evar_kinds.t -> bool let all_evars _ _ = true -let all_goals _ = function GoalEvar _ -> true | _ -> false +let all_goals _ = function GoalEvar -> true | _ -> false let no_goals ev evi = not (all_goals ev evi) let no_goals_or_obligations _ = function - | GoalEvar _ | QuestionMark _ -> false + | GoalEvar | QuestionMark _ -> false | _ -> true let mark_resolvability filter b sigma = @@ -560,15 +549,16 @@ let has_typeclasses filter evd = in Evar.Map.exists check (Evd.undefined_map evd) -let solve_instantiations_problem = ref (fun _ _ _ _ _ -> assert false) +let solve_instantiations_problem = ref (fun _ _ _ _ _ _ -> assert false) -let solve_problem env evd filter split fail = - !solve_instantiations_problem env evd filter split fail +let solve_problem env evd filter unique split fail = + !solve_instantiations_problem env evd filter unique split fail (** Profiling resolution of typeclasses *) (* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *) (* let solve_problem = Profile.profile5 solve_classeskey solve_problem *) -let resolve_typeclasses ?(filter=no_goals) ?(split=true) ?(fail=true) env evd = +let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ()) + ?(split=true) ?(fail=true) env evd = if not (has_typeclasses filter evd) then evd - else solve_problem env evd filter split fail + else solve_problem env evd filter unique split fail diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index b1f816e651..447df1da1b 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -37,6 +37,10 @@ type typeclass = { (** Whether we use matching or full unification during resolution *) cl_strict : bool; + + (** Whether we can assume that instances are unique, which allows + no backtracking and sharing of resolution. *) + cl_unique : bool; } type instance @@ -47,10 +51,6 @@ val all_instances : unit -> instance list val add_class : typeclass -> unit -val add_constant_class : constant -> unit - -val add_inductive_class : inductive -> unit - val new_instance : typeclass -> int option -> bool -> Decl_kinds.polymorphic -> global_reference -> instance val add_instance : instance -> unit @@ -104,9 +104,9 @@ val mark_resolvable : evar_info -> evar_info val is_class_evar : evar_map -> evar_info -> bool val is_class_type : evar_map -> types -> bool -val resolve_typeclasses : ?filter:evar_filter -> ?split:bool -> ?fail:bool -> - env -> evar_map -> evar_map -val resolve_one_typeclass : env -> evar_map -> types -> open_constr +val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool -> + ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map +val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> types -> open_constr val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit @@ -122,8 +122,8 @@ val add_instance_hint : global_reference_or_constr -> global_reference list -> bool -> int option -> Decl_kinds.polymorphic -> unit val remove_instance_hint : global_reference -> unit -val solve_instantiations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> evar_map) ref -val solve_instantiation_problem : (env -> evar_map -> types -> open_constr) ref +val solve_instantiations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) ref +val solve_instantiation_problem : (env -> evar_map -> types -> bool -> open_constr) ref val declare_instance : int option -> bool -> global_reference -> unit |