Unplugging Autoinstance. The code is still here if someone wishes

to fix it, but it should be eventually erased.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16774 85f007b7-540e-0410-9357-904b9bb8a0f7

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