diff options
| -rw-r--r-- | pretyping/typeclasses.ml | 15 | ||||
| -rw-r--r-- | toplevel/classes.ml | 55 | ||||
| -rw-r--r-- | toplevel/classes.mli | 4 |
3 files changed, 41 insertions, 33 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index a1183c97b..febfb0494 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -219,6 +219,7 @@ let solve_instanciation_problem = ref (fun _ _ _ _ -> assert false) let resolve_typeclass env ev evi (evd, defined as acc) = try + assert(evi.evar_body = Evar_empty); !solve_instanciation_problem env evd ev evi with Exit -> acc @@ -269,16 +270,22 @@ let is_implicit_arg k = | InternalHole -> true | _ -> false +let destClassApp c = + match kind_of_term c with + | App (ki, args) when isInd ki -> + Some (destInd ki, args) + | _ when isInd c -> Some (destInd c, [||]) + | _ -> None + let resolve_typeclasses ?(check=true) env sigma evd = let evm = Evd.evars_of evd in let tc_evars = let f ev evi acc = let (l, k) = Evd.evar_source ev evd in if not check || is_implicit_arg k then - match kind_of_term evi.evar_concl with - | App(ki, args) when isInd ki -> - if is_class (destInd ki) then Evd.add acc ev evi - else acc + match destClassApp evi.evar_concl with + | Some (i, args) when is_class i -> + Evd.add acc ev evi | _ -> acc else acc in Evd.fold f evm Evd.empty diff --git a/toplevel/classes.ml b/toplevel/classes.ml index b3b7089cd..d84fb3e56 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -28,11 +28,22 @@ open Rawterm open Topconstr (*i*) +open Decl_kinds +open Entries + +let hint_db = "typeclass_instances" + +let add_instance_hint inst = + Auto.add_hints false [hint_db] (Vernacexpr.HintsResolve [CRef (Ident (dummy_loc, inst))]) + +let declare_instance (_,id) = + add_instance_hint id + let mismatched_params env n m = mismatched_ctx_inst env Parameters n m (* let mismatched_defs env n m = mismatched_ctx_inst env Definitions n m *) let mismatched_props env n m = mismatched_ctx_inst env Properties n m -type binder_list = (identifier located * constr_expr) list +type binder_list = (identifier located * bool * constr_expr) list let interp_binders_evars isevars env avoid l = List.fold_left @@ -84,7 +95,7 @@ let rec unfold n f acc = (* Declare everything in the parameters as implicit, and the class instance as well *) open Topconstr -let declare_implicit_proj c proj imps = +let declare_implicit_proj c proj imps sub = let len = List.length c.cl_context in let (ctx, _) = decompose_prod_n (len + 1) (Typeops.type_of_constant (Global.env()) proj) in let expls = @@ -98,16 +109,17 @@ let declare_implicit_proj c proj imps = aux 1 [] ctx in let expls = expls @ List.map (function (ExplByPos (i, n), f) -> (ExplByPos (succ len + i, n)), f | _ -> assert(false)) imps in + if sub then add_instance_hint (id_of_label (con_label proj)); Impargs.declare_manual_implicits true (ConstRef proj) true expls -let declare_implicits impls cl = +let declare_implicits impls subs cl = let projs = Recordops.lookup_projections cl.cl_impl in - List.iter2 - (fun c imps -> + Util.list_iter3 + (fun c imps sub -> match c with | None -> assert(false) - | Some p -> declare_implicit_proj cl p imps) - projs impls; + | Some p -> declare_implicit_proj cl p imps sub) + projs impls subs; let len = List.length cl.cl_context in let indimps = list_fold_left_i @@ -173,7 +185,7 @@ let mk_interning_data env na impls typ = let interp_fields_evars isevars env avoid l = List.fold_left - (fun (env, uimpls, ids, params, impls) ((loc, i), t) -> + (fun (env, uimpls, ids, params, impls) ((loc, i), _, t) -> let impl, t' = interp_type_evars isevars env ~impls t in let data = mk_interning_data env i impl t' in let d = (i,None,t') in @@ -240,7 +252,7 @@ let new_class id par ar sup props = let env_props, prop_impls, bound, ctx_props, _ = interp_fields_evars isevars env_params bound props in - + let subs = List.map (fun ((loc, id), b, _) -> b) props in (* Instantiate evars and check all are resolved *) let isevars,_ = Evarconv.consider_remaining_unif_problems env_props !isevars in let sigma = Evd.evars_of isevars in @@ -269,20 +281,9 @@ let new_class id par ar sup props = cl_props = ctx_props; cl_impl = kn } in - declare_implicits (List.rev prop_impls) k; + declare_implicits (List.rev prop_impls) subs k; add_class k -open Decl_kinds -open Entries - -let hint_db = "typeclass_instances" - -let add_instance_hint inst = - Auto.add_hints false [hint_db] (Vernacexpr.HintsResolve [CRef (Ident (dummy_loc, inst))]) - -let declare_instance (_,id) = - add_instance_hint id - type binder_def_list = (identifier located * identifier located list * constr_expr) list let binders_of_lidents l = @@ -394,7 +395,9 @@ let new_instance ctx (instid, bk, cl) props = App (c, args) -> let cl = Option.get (class_of_constr c) in cl, ctx, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args)) - | _ -> assert false) + | _ -> + let cl = Option.get (class_of_constr c) in + cl, ctx, []) in let env' = push_named_context ctx' env in isevars := Evarutil.nf_evar_defs !isevars; @@ -482,12 +485,10 @@ let module_qualid = qualid_of_dirpath (dirpath_of_string "Coq.Classes.Init") let tactic_qualid = make_qualid (dirpath_of_string "Coq.Classes.Init") (id_of_string "typeclass_instantiation") let tactic_expr = Tacexpr.TacArg (Tacexpr.Reference (Qualid (dummy_loc, tactic_qualid))) -let tactic = lazy (Library.require_library [(dummy_loc, module_qualid)] None; - Tacinterp.interp tactic_expr) +let tactic = lazy (Tacinterp.interp tactic_expr) let _ = Typeclasses.solve_instanciation_problem := (fun env evd ev evi -> - solve_by_tac env evd ev evi (Lazy.force tactic)) - - + Library.require_library [(dummy_loc, module_qualid)] None; (* may be inefficient *) + solve_by_tac env evd ev evi (Lazy.force tactic)) diff --git a/toplevel/classes.mli b/toplevel/classes.mli index 6444fb3d9..93fc1b552 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -23,12 +23,12 @@ open Typeclasses open Implicit_quantifiers (*i*) -type binder_list = (identifier located * constr_expr) list +type binder_list = (identifier located * bool * constr_expr) list type binder_def_list = (identifier located * identifier located list * constr_expr) list val binders_of_lidents : identifier located list -> local_binder list -val declare_implicit_proj : typeclass -> constant -> Impargs.manual_explicitation list -> unit +val declare_implicit_proj : typeclass -> constant -> Impargs.manual_explicitation list -> bool -> unit val infer_super_instances : env -> constr list -> named_context -> named_context -> types list * identifier list * named_context |