(************************************************************************)
(*  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 rec mksubst b = function
    | [] -> []
    | a::tl -> b::(mksubst (a::b) tl) 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 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 } 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 } 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 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()) }*)