Removing Autoinstance once and for all.

5 files changed, 0 insertions, 387 deletions

diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
deleted file mode 100644
index 16e6c87f96..0000000000
--- a/toplevel/autoinstance.ml
+++ /dev/null
@@ -1,349 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       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
-open Printer
-open Names
-open Term
-open Vars
-open Context
-open Evd
-open Globnames
-(*i*)
-
-(*s
- * Automatic detection of (some) record instances
- *)
-
-(* Datatype for wannabe-instances: a signature is a typeclass along
-   with the collection of evars corresponding to the parameters/fields
-   of the class. Each evar can be uninstantiated (we're still looking
-   for them) or defined (the instance for the field is fixed) *)
-type signature = global_reference * evar list * evar_map
-
-type instance_decl_function = global_reference -> rel_context -> constr list -> unit
-
-(*
- * Search algorithm
- *)
-
-let reduce x = x
-
-let rec subst_evar evar def n c =
-  match kind_of_term c with
-    | Evar (e,_) when Evar.equal e evar -> lift n def
-    | _ -> map_constr_with_binders (fun n->n+1) (subst_evar evar def) n c
-
-let subst_evar_in_evm evar def evm =
-  let map ev evi =
-    let evar_body = match evi.evar_body with
-      | Evd.Evar_empty -> Evd.Evar_empty
-      | Evd.Evar_defined c -> Evd.Evar_defined (subst_evar evar def 0 c) in
-    let evar_concl = subst_evar evar def 0 evi.evar_concl in
-    {evi with evar_body=evar_body; evar_concl=evar_concl}
-  in
-  Evd.raw_map map evm
-
-(* Tries to define ev by c in evd. Fails if ev := c1 and c1 /= c ev :
- * T1, c : T2 and T1 /= T2. Defines recursively all evars instantiated
- * by this definition. *)
-
-let rec safe_define evm ev c =
-  if not (closedn (-1) c) then raise Termops.CannotFilter else
-(*  msgnl(str"safe_define "++pr_evar_map evm++spc()++str" |- ?"++Pp.int ev++str" := "++pr_constr c);*)
-  let evi = (Evd.find evm ev) in
-  let define_subst evm sigma =
-    Evar.Map.fold
-      ( fun ev (e,c) evm ->
-	  match kind_of_term c with Evar (i,_) when Evar.equal i ev -> evm | _ ->
-	    safe_define evm ev (lift (-List.length e) c)
-      ) sigma evm in
-  match evi.evar_body with
-    | Evd.Evar_defined def ->
-	define_subst evm (Termops.filtering [] Reduction.CUMUL def c)
-    | Evd.Evar_empty ->
-	let t = reduce (Typing.type_of (Global.env()) evm c) in
-	let u = reduce (evar_concl evi) in
-	let evm = subst_evar_in_evm ev c evm in
-	define_subst (Evd.define ev c evm) (Termops.filtering [] Reduction.CUMUL t u)
-
-let add_gen_ctx (cl,gen,evm) ctx : signature * constr list =
-  let env = Environ.empty_named_context_val in
-  let fold_new_evar evm _ = Evarutil.new_pure_evar evm env mkProp in
-  let (evm, evl) = List.fold_map fold_new_evar evm ctx in
-  let evcl = List.map (fun i -> mkEvar (i,[||])) evl in
-(*   let substl = List.rev (mksubst [] (evcl)) in *)
-(*   let ctx = List.map2 (fun s t -> substnl s 0 t) substl ctx in *)
-  (cl, evl @ gen, evm), evcl
-
-(* TODO : for full proof-irrelevance in the search, provide a real
-   compare function for constr instead of Pervasive's one! *)
-module SubstSet : Set.S with type elt = Termops.subst
-  = Set.Make (struct type t = Termops.subst
-		     let compare = Evar.Map.compare (Pervasives.compare) (** FIXME *)
-	      end)
-
-let search_concl typ = assert false
-(** FIXME: if one ever wants to maintain this code, he has to plug the Search
-    machinery into this assertion failure. *)
-
-(* searches instatiations in the library for just one evar [ev] of a
-   signature. [k] is called on each resulting signature *)
-let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) =
-  let ev_typ = reduce (evar_concl evi) in
-  let sort_is_prop = is_Prop (Typing.type_of (Global.env()) evm (evar_concl evi)) in
-(*  msgnl(str"cherche "++pr_constr ev_typ++str" pour "++Pp.int ev);*)
-  let substs = ref SubstSet.empty in
-  try List.iter
-    ( fun (gr,(pat,_),s) ->
-	let (_,genl,_) = Termops.decompose_prod_letin pat in
-	let genl = List.map (fun (_,_,t) -> t) genl in
-	let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) genl in
-	let def = applistc (Globnames.constr_of_global gr) argl in
-(*	msgnl(str"essayons  ?"++Pp.int ev++spc()++str":="++spc()
-	      ++pr_constr def++spc()++str":"++spc()++pr_constr (Global.type_of_global gr)*)
-	(*++spc()++str"dans"++spc()++pr_evar_map evm++spc());*)
-	try
- 	  let evm = safe_define evm ev def in
-	  k (cl,gen,evm);
-	  if sort_is_prop && SubstSet.mem s !substs then raise Exit;
-	  substs := SubstSet.add s !substs
-	with Termops.CannotFilter -> ()
-    ) (search_concl ev_typ)
-  with Exit -> ()
-
-let evm_fold_rev f evm acc =
-  let l = Evd.fold (fun ev evi acc -> (ev,evi)::acc) evm [] in
-  List.fold_left (fun acc (ev,evi) -> f ev evi acc) acc l
-
-exception Continue of Evd.evar * Evd.evar_info
-
-(* searches matches for all the uninstantiated evars of evd in the
-   context. For each totally instantiated evar_map found, apply
-   k. *)
-let rec complete_signature (k:signature -> unit) (cl,gen,evm:signature) =
-  try
-    evm_fold_rev
-      ( fun ev evi _ ->
-	  if not (is_defined evm ev) && not (List.mem_f Evar.equal ev gen) then
-	    raise (Continue (ev,evi))
-      ) evm (); k (cl,gen,evm)
-  with Continue (ev,evi) -> complete_evar (cl,gen,evm) (ev,evi) (complete_signature k)
-
-(* define all permutations of the evars to evd and call k on the
-   resulting evd *)
-let complete_with_evars_permut (cl,gen,evm:signature) evl c (k:signature -> unit) : unit =
-  let rec aux evm = List.iter
-    ( fun (ctx,ev) ->
-	let tyl = List.map (fun (_,_,t) -> t) ctx in
-	let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) tyl in
-	let def = applistc c argl in
-(*	msgnl(str"trouvé def ?"++Pp.int ev++str" := "++pr_constr def++str " dans "++pr_evar_map evm);*)
-	try
-	  if not (Evd.is_defined evm ev) then
-	    let evm = safe_define evm ev def in
-	    aux evm; k (cl,gen,evm)
-	with Termops.CannotFilter -> ()
-    ) evl in
-  aux evm
-
-let new_inst_no =
-  let cnt = ref 0 in
-  fun () -> incr cnt; string_of_int !cnt
-
-let make_instance_ident gr =
-  Nameops.add_suffix (Nametab.basename_of_global gr) ("_autoinstance_"^new_inst_no())
-
-let new_instance_message ident typ def =
-  Flags.if_verbose
-  msg_info (str"new instance"++spc()
-	 ++Nameops.pr_id ident++spc()++str":"++spc()
-	 ++pr_constr typ++spc()++str":="++spc()
-	 ++pr_constr def)
-
-open Entries
-
-let rec deep_refresh_universes c =
-  match kind_of_term c with
-    | Sort (Type _) -> Termops.new_Type()
-    | _ -> map_constr deep_refresh_universes c
-
-let declare_record_instance gr ctx params =
-  let ident = make_instance_ident gr in
-  let def = it_mkLambda_or_LetIn (applistc (constr_of_global gr) params) ctx in
-  let def = deep_refresh_universes def in
-  let ce = { const_entry_body= Future.from_val (def,Declareops.no_seff);
-             const_entry_secctx = None;
-	     const_entry_type=None;
-         const_entry_opaque=false;
-         const_entry_inline_code = false;
-         const_entry_feedback = None } in
-  let decl = (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in
-  let cst = Declare.declare_constant ident decl in
-  new_instance_message ident (Typeops.type_of_constant (Global.env()) cst) def
-
-let declare_class_instance gr ctx params =
-  let ident = make_instance_ident gr in
-  let cl = Typeclasses.class_info gr in
-  let (def,typ) = Typeclasses.instance_constructor cl params in
-  let (def,typ) = it_mkLambda_or_LetIn (Option.get def) ctx, it_mkProd_or_LetIn typ ctx in
-  let def = deep_refresh_universes def in
-  let typ = deep_refresh_universes typ in
-  let ce = Entries.DefinitionEntry
-    {  const_entry_type= Some typ;
-       const_entry_body= Future.from_val (def,Declareops.no_seff);
-       const_entry_secctx = None;
-       const_entry_opaque = false;
-       const_entry_inline_code = false;
-       const_entry_feedback = None } in
-  try
-  let cst = Declare.declare_constant ident
-    (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in
-  Typeclasses.add_instance (Typeclasses.new_instance cl (Some 100) true (ConstRef cst));
-  new_instance_message ident typ def
-  with e when Errors.noncritical e ->
-    msg_info (str"Error defining instance := "++pr_constr def++
-              str" : "++pr_constr typ++str"  "++Errors.print e)
-
-let rec iter_under_prod (f:rel_context->constr->unit) (ctx:rel_context) t = f ctx t;
-  match kind_of_term t with
-    | Prod (n,t,c) -> iter_under_prod f ((n,None,t)::ctx) c
-    | _ -> ()
-
-module GREMOrd =
-struct
-  type t = Globnames.global_reference * Evd.evar_map
-  let compare (gr1, _) (gr2, _) = Globnames.RefOrdered.compare gr1 gr2
-  (** ppedrot: this code was actually already broken before this modification,
-      and used polymorphic equality over evar maps, which is just bad. Now we
-      simply ignore it, which looks more sensible. *)
-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
-    GREM.add key (data :: l) map
-  with Not_found ->
-    GREM.add key [data] map
-
-(* main search function: search for total instances containing gr, and
-   apply k to each of them *)
-let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature -> unit) : unit =
-  let gr_c = Globnames.constr_of_global gr in
-  let smap = ref GREM.empty in
-  iter_under_prod
-    ( fun ctx typ ->
-	List.iter
-	  (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)
-	  (methods_matching typ)
-    ) [] deftyp;
-  GREM.iter
-    ( fun (cl,evm) evl ->
-	let f = if Typeclasses.is_class cl then
-	  declare_class_instance else declare_record_instance in
-	complete_with_evars_permut (cl,[],evm) evl gr_c
-	  (fun sign -> complete_signature (k f) sign)
-    ) !smap
-
-(*
- * Interface with other parts: hooks & declaration
- *)
-
-
-let evar_definition evi = match evar_body evi with
-    Evar_empty -> assert false | Evar_defined c -> c
-
-let gen_sort_topo l evm =
-  let iter_evar f ev =
-    let rec aux c = match kind_of_term c with
-	Evar (e,_) -> f e
-      | _ -> iter_constr aux c in
-    aux (Evd.evar_concl (Evd.find evm ev));
-    if Evd.is_defined evm ev then aux (evar_definition (Evd.find evm ev)) in
-  let r = ref [] in
-  let rec dfs ev = iter_evar dfs ev;
-    if not(List.mem_f Evar.equal ev !r) then r := ev::!r in
-  List.iter dfs l; List.rev !r
-
-(* register real typeclass instance given a totally defined evd *)
-let declare_instance (k:global_reference -> rel_context -> constr list -> unit)
-    (cl,gen,evm:signature) =
-  let evm = Evarutil.nf_evar_map evm in
-  let gen = gen_sort_topo gen evm in
-  let (evm,gen) = List.fold_right
-    (fun ev (evm,gen) ->
-       if Evd.is_defined evm ev
-       then Evd.remove evm ev,gen
-       else evm,(ev::gen))
-    gen (evm,[]) in
-(*  msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Pp.int gen++str"] : "++spc()++pr_evar_map evm);*)
-  let ngen = List.length gen in
-  let (_,ctx,evm) = List.fold_left
-    ( fun (i,ctx,evm) ev ->
-	let ctx = (Anonymous,None,lift (-i) (Evd.evar_concl(Evd.find evm ev)))::ctx in
-	let evm = subst_evar_in_evm ev (mkRel i) (Evd.remove evm ev) in
-	(i-1,ctx,evm)
-    ) (ngen,[],evm) gen in
-  let fields = List.rev (Evd.fold ( fun ev evi l -> evar_definition evi::l ) evm []) in
-  k cl ctx fields
-
-let autoinstance_opt = ref false
-
-let search_declaration gr =
-  if !autoinstance_opt &&
-    not (Lib.is_modtype()) then
-    let deftyp = Global.type_of_global gr in
-    complete_signature_with_def gr deftyp declare_instance
-
-let search_record k cons sign =
-  if !autoinstance_opt && not (Lib.is_modtype()) then
-    complete_signature (declare_instance k) (cons,[],sign)
-
-(*
-let dh_key = Profile.declare_profile "declaration_hook"
-let ch_key = Profile.declare_profile "class_decl_hook"
-let declaration_hook = Profile.profile1 dh_key declaration_hook
-let class_decl_hook = Profile.profile1 ch_key class_decl_hook
-*)
-
-(*
- *  Options and bookeeping
- *)
-
-let begin_autoinstance () =
-  if not !autoinstance_opt then (
-    autoinstance_opt := true;
-  )
-
-let end_autoinstance () =
-  if !autoinstance_opt then (
-    autoinstance_opt := false;
- )
-
-(*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()) }*)
diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli
deleted file mode 100644
index bfc9bcff27..0000000000
--- a/toplevel/autoinstance.mli
+++ /dev/null
@@ -1,32 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Term
-open Globnames
-open Evd
-open Context
-
-(** {6 Automatic detection of (some) record instances } *)
-
-(** What to do if we find an instance. Passed are : the reference
- * representing the record/class (definition or constructor) *)
-type instance_decl_function = global_reference -> rel_context -> constr list -> unit
-
-(** [search_declaration gr] Search in the library if the (new)
- * declaration gr can form an instance of a registered record/class *)
-val search_declaration : global_reference -> unit
-
-(** [search_record declf gr evm] Search the library for instances of
-   the (new) record/class declaration [gr], and register them using
-   [declf]. [evm] is the signature of the record (to avoid recomputing
-   it) *)
-val search_record : instance_decl_function -> global_reference -> evar_map -> unit
-
-(** Instance declaration for both scenarios *)
-val declare_record_instance : instance_decl_function
-val declare_class_instance : instance_decl_function
diff --git a/toplevel/command.ml b/toplevel/command.ml
index d4d40339cf..f41acaba27 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -138,7 +138,6 @@ let declare_global_definition ident ce local k imps =
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
   let () = definition_message ident in
-  let () = Autoinstance.search_declaration (ConstRef kn) in
   gr
 
 let declare_definition_hook = ref ignore
@@ -211,7 +210,6 @@ let declare_assumption is_coe (local, kind) c imps impl nl (_,ident) = match loc
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
   let () = assumption_message ident in
-  let () = Autoinstance.search_declaration (ConstRef kn) in
   let () = Typeclasses.declare_instance None false gr in
   let () = if is_coe then Class.try_add_new_coercion gr local in
   (gr,Lib.is_modtype_strict ())
@@ -400,11 +398,9 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
   let mind = Global.mind_of_delta_kn kn in
   List.iteri (fun i (indimpls, constrimpls) ->
 		   let ind = (mind,i) in
-		     Autoinstance.search_declaration (IndRef ind);
 		     maybe_declare_manual_implicits false (IndRef ind) indimpls;
 		     List.iteri
 		       (fun j impls ->
-(*	    Autoinstance.search_declaration (ConstructRef (ind,j));*)
 			  maybe_declare_manual_implicits false (ConstructRef (ind, succ j)) impls)
 		       constrimpls)
       impls;
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index fd606a6b88..8f16ad5a4b 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -181,7 +181,6 @@ let save id const do_guard (locality,kind) hook =
         | Global -> false
         in
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
-	Autoinstance.search_declaration (ConstRef kn);
 	(locality, ConstRef kn) in
   definition_message id;
   hook l r
diff --git a/toplevel/toplevel.mllib b/toplevel/toplevel.mllib
index 16cc510866..d348ce7472 100644
--- a/toplevel/toplevel.mllib
+++ b/toplevel/toplevel.mllib
@@ -5,7 +5,6 @@ Locality
 Metasyntax
 Auto_ind_decl
 Search
-Autoinstance
 Lemmas
 Indschemes
 Obligations