diff options
| -rw-r--r-- | pretyping/recordops.ml | 44 | ||||
| -rw-r--r-- | pretyping/recordops.mli | 9 | ||||
| -rw-r--r-- | toplevel/autoinstance.ml | 16 | ||||
| -rw-r--r-- | toplevel/record.ml | 6 |
4 files changed, 12 insertions, 63 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 5aced6e10..eaf7bf0aa 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -105,50 +105,6 @@ let find_projection = function | ConstRef cst -> Cmap.find cst !projection_table | _ -> raise Not_found -(* Management of a field store : each field + argument of the inferred - * records are stored in a discrimination tree *) - -let subst_id s (gr,ev,evm) = - (fst(subst_global s gr),ev,Evd.subst_evar_map s evm) - -module MethodsDnet : Term_dnet.S - with type ident = global_reference * Evd.evar * Evd.evar_map - = Term_dnet.Make - (struct - type t = global_reference * Evd.evar * Evd.evar_map - (** ppedrot: FIXME: this is surely wrong, generic equality has nothing to - do w.r.t. evar maps. *) - let compare = Pervasives.compare - let subst = subst_id - let constr_of (_,ev,evm) = Evd.evar_concl (Evd.find evm ev) - end) - (struct - let reduce c = Reductionops.head_unfold_under_prod - Names.full_transparent_state (Global.env()) Evd.empty c - let direction = true - end) - -let meth_dnet = Summary.ref MethodsDnet.empty ~name:"record-methods-state" - -open Libobject - -let load_method (_,(ty,id)) = - meth_dnet := MethodsDnet.add ty id !meth_dnet - -let in_method : constr * MethodsDnet.ident -> obj = - declare_object - { (default_object "RECMETHODS") with - load_function = (fun _ -> load_method); - cache_function = load_method; - subst_function = (fun (s,(ty,id)) -> Mod_subst.subst_mps s ty,subst_id s id); - classify_function = (fun x -> Substitute x) - } - -let methods_matching c = MethodsDnet.search_pattern !meth_dnet c - -let declare_method cons ev sign = - Lib.add_anonymous_leaf (in_method ((Evd.evar_concl (Evd.find sign ev)),(cons,ev,sign))) - (************************************************************************) (*s A canonical structure declares "canonical" conversion hints between *) (* the effective components of a structure and the projections of the *) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 11e558a76..062326505 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -45,15 +45,6 @@ val find_projection_nparams : global_reference -> int (** raise [Not_found] if not a projection *) val find_projection : global_reference -> struc_typ -(** we keep an index (dnet) of record's arguments + fields - (=methods). Here is how to declare them: *) -val declare_method : - global_reference -> Evd.evar -> Evd.evar_map -> unit - (** and here is how to search for methods matched by a given term: *) -val methods_matching : constr -> - ((global_reference*Evd.evar*Evd.evar_map) * - (constr*existential_key)*Termops.subst) list - (** {6 Canonical structures } *) (** A canonical structure declares "canonical" conversion hints between the effective components of a structure and the projections of the diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index e9601c123..b13d2ea29 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -6,6 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** ppedrot: this code has been broken for ages. It used to automagically detect + instances of classes based on the types of record fields. If anyone wishes + to fix it, she is welcome, though there is quite a lot of work to do. At + best, this should be moved to a proper plugin. *) + (*i*) open Util open Pp @@ -234,6 +239,9 @@ end module GREM = Map.Make(GREMOrd) +let methods_matching typ = assert false + (** ppedrot: used to be [Recordops.methods_matching], which I unplugged. *) + let grem_add key data map = try let l = GREM.find key map in @@ -252,7 +260,7 @@ let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature (fun ((cl,ev,evm),_,_) -> (* msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Pp.int ev++str " dans "++pr_evar_map evm);*) smap := grem_add (cl,evm) (ctx,ev) !smap) - (Recordops.methods_matching typ) + (methods_matching typ) ) [] deftyp; GREM.iter ( fun (cl,evm) evl -> @@ -304,7 +312,7 @@ let declare_instance (k:global_reference -> rel_context -> constr list -> unit) let fields = List.rev (Evd.fold ( fun ev evi l -> evar_definition evi::l ) evm []) in k cl ctx fields -let autoinstance_opt = ref true +let autoinstance_opt = ref false let search_declaration gr = if !autoinstance_opt && @@ -337,11 +345,11 @@ let end_autoinstance () = autoinstance_opt := false; ) -let _ = +(*let _ = Goptions.declare_bool_option { Goptions.optsync=true; Goptions.optdepr=false; Goptions.optkey=["Autoinstance"]; Goptions.optname="automatic typeclass instance recognition"; Goptions.optread=(fun () -> !autoinstance_opt); - Goptions.optwrite=(fun b -> if b then begin_autoinstance() else end_autoinstance()) } + Goptions.optwrite=(fun b -> if b then begin_autoinstance() else end_autoinstance()) }*) diff --git a/toplevel/record.ml b/toplevel/record.ml index 476da3d0e..5c59987aa 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -267,8 +267,6 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls let build = ConstructRef cstr in let () = if is_coe then Class.try_add_new_coercion build ~local:false in Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs); - if infer then - Evd.fold (fun ev evi () -> Recordops.declare_method (ConstructRef cstr) ev sign) sign (); rsp let implicits_of_context ctx = @@ -322,7 +320,6 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls Impargs.declare_manual_implicits false cref [paramimpls]; Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls]; Classes.set_typeclass_transparency (EvalConstRef cst) false false; - if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign (); let sub = match List.hd coers with Some b -> Some ((if b then Backward else Forward), List.hd priorities) | None -> None in cref, [Name proj_name, sub, Some proj_cst] | _ -> @@ -364,7 +361,6 @@ let interp_and_check_sort sort = else user_err_loc (constr_loc sort,"", str"Sort expected.")) sort open Vernacexpr -open Autoinstance (* [fs] corresponds to fields and [ps] to parameters; [coers] is a list telling if the corresponding fields must me declared as coercions @@ -392,7 +388,6 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil | Class def -> let gr = declare_class finite def infer (loc,idstruc) idbuild implpars params sc implfs fields is_coe coers priorities sign in - if infer then search_record declare_class_instance gr sign; gr | _ -> let arity = Option.default (Termops.new_Type ()) sc in @@ -400,5 +395,4 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in - if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign; IndRef ind |