Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 316 insertions, 0 deletions

diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
new file mode 100644
index 00000000..b45e45c8
--- /dev/null
+++ b/toplevel/autoinstance.ml
@@ -0,0 +1,316 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id:$ *)
+
+(*i*)
+open Pp
+open Printer
+open Names
+open Term
+open Evd
+open Sign
+open Libnames
+(*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 rec subst_evar evar def n c =
+  match kind_of_term c with
+    | Evar (e,_) when 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 =
+  Evd.fold
+    (fun ev evi acc ->
+       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
+       Evd.add acc ev {evi with evar_body=evar_body; evar_concl=evar_concl}
+    ) evm empty
+
+(* 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" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*)
+  let evi = (Evd.find evm ev) in
+  let define_subst evm sigma =
+    Util.Intmap.fold
+      ( fun ev (e,c) evm ->
+	  match kind_of_term c with Evar (i,_) when 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 = Libtypes.reduce (Typing.type_of (Global.env()) evm c) in
+	let u = Libtypes.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 rec really_new_evar () =
+    let ev = Evarutil.new_untyped_evar() in
+    if Evd.is_evar evm ev then really_new_evar() else ev in
+  let add_gen_evar (cl,gen,evm) ev ty : signature =
+    let evm = Evd.add evm ev (Evd.make_evar Environ.empty_named_context_val ty) in
+    (cl,ev::gen,evm) in
+  let rec mksubst b = function
+    | [] -> []
+    | a::tl -> b::(mksubst (a::b) tl) in
+  let evl = List.map (fun _ -> really_new_evar()) 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
+  let sign = List.fold_left2 add_gen_evar (cl,gen,evm) (List.rev evl) ctx in
+  sign,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 = Util.Intmap.compare (Pervasives.compare)
+	      end)
+
+(* 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 = Libtypes.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 "++Util.pr_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 (Libnames.constr_of_global gr) argl in
+(*	msgnl(str"essayons  ?"++Util.pr_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 -> ()
+    ) (Libtypes.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 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 ?"++Util.pr_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
+  msgnl (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=def; const_entry_type=None;
+	     const_entry_opaque=false; const_entry_boxed=false } in
+  let cst = Declare.declare_constant ident
+    (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) 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 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=def;
+       const_entry_opaque=false; const_entry_boxed=false } 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 -> msgnl (str"Error defining instance := "++pr_constr def++str" : "++pr_constr typ++str"  "++Cerrors.explain_exn 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
+    | _ -> ()
+
+(* 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 = Libnames.constr_of_global gr in
+  let (smap:(Libnames.global_reference * Evd.evar_map,
+   ('a * 'b * Term.constr) list * Evd.evar)
+  Gmapl.t ref) = ref Gmapl.empty in
+  iter_under_prod
+    ( fun ctx typ ->
+	List.iter
+	  (fun ((cl,ev,evm),_,_) ->
+(*	     msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_map evm);*)
+	     smap := Gmapl.add (cl,evm) (ctx,ev) !smap)
+	  (Recordops.methods_matching typ)
+    ) [] deftyp;
+  Gmapl.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 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_evars 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";") Util.pr_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 true
+
+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.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()) }