(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(*i*)
open Pp
open Printer
open Names
open Term
open Evd
open Sign
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 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" |- ?"++Pp.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 "++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 -> ()
    ) (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 ?"++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
  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_secctx = None;
	     const_entry_type=None;
	     const_entry_opaque=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 (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_secctx = None;
       const_entry_body= def;
       const_entry_opaque=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"  "++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
    | _ -> ()

(* 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:(Globnames.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 ?"++Pp.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_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 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.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()) }