(************************************************************************)
(*  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$ *)

open Pp
open Util
open Names
open Nameops
open Term
open Termops
open Sign
open Environ
open Evd
open Reduction
open Reductionops
open Rawterm
open Pattern
open Tacred
open Pretype_errors
open Evarutil
open Unification
open Mod_subst
open Coercion.Default

(* *)
let w_coerce env c ctyp target evd =
  let j = make_judge c ctyp in
  let tycon = mk_tycon_type target in
  let (evd',j') = inh_conv_coerce_to dummy_loc env evd j tycon in
  (evd',j'.uj_val)

let pf_env gls = Global.env_of_context gls.it.evar_hyps
let pf_type_of gls c  = Typing.type_of (pf_env gls) gls.sigma c
let pf_hnf_constr gls c = hnf_constr (pf_env gls) gls.sigma c
let pf_concl gl = gl.it.evar_concl

(******************************************************************)
(* Clausal environments *)

type clausenv = {
  env      : env;
  evd      : evar_defs;
  templval : constr freelisted;
  templtyp : constr freelisted }

let cl_env ce = ce.env
let cl_sigma ce = evars_of ce.evd

let subst_clenv sub clenv = 
  { templval = map_fl (subst_mps sub) clenv.templval;
    templtyp = map_fl (subst_mps sub) clenv.templtyp;
    evd = subst_evar_defs_light sub clenv.evd;
    env = clenv.env }

let clenv_nf_meta clenv c = nf_meta clenv.evd c
let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv
let clenv_value clenv = meta_instance clenv.evd clenv.templval
let clenv_type clenv = meta_instance clenv.evd clenv.templtyp


let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t

let clenv_get_type_of ce c =
  let metamap =
    List.map 
      (function
	 | (n,Clval(_,_,typ)) -> (n,typ.rebus)
         | (n,Cltyp (_,typ))    -> (n,typ.rebus))
      (meta_list ce.evd) in
  Retyping.get_type_of_with_meta (cl_env ce) (cl_sigma ce) metamap c

exception NotExtensibleClause

let clenv_push_prod cl =
  let typ = whd_betadeltaiota (cl_env cl) (cl_sigma cl) (clenv_type cl) in
  let rec clrec typ = match kind_of_term typ with
    | Cast (t,_,_) -> clrec t
    | Prod (na,t,u) ->
	let mv = new_meta () in
	let dep = dependent (mkRel 1) u in
	let na' = if dep then na else Anonymous in
	let e' = meta_declare mv t ~name:na' cl.evd in
	let concl = if dep then subst1 (mkMeta mv) u else u in
	let def = applist (cl.templval.rebus,[mkMeta mv]) in
	{ templval = mk_freelisted def;
	  templtyp = mk_freelisted concl;
	  evd = e';
	  env = cl.env }
    | _ -> raise NotExtensibleClause
  in clrec typ

(* Instantiate the first [bound] products of [t] with metas (all products if
   [bound] is [None]; unfold local defs *)

let clenv_environments evd bound t =
  let rec clrec (e,metas) n t =
    match n, kind_of_term t with
      | (Some 0, _) -> (e, List.rev metas, t)
      | (n, Cast (t,_,_)) -> clrec (e,metas) n t
      | (n, Prod (na,t1,t2)) ->
	  let mv = new_meta () in
	  let dep = dependent (mkRel 1) t2 in
	  let na' = if dep then na else Anonymous in
	  let e' = meta_declare mv t1 ~name:na' e in
	  clrec (e', (mkMeta mv)::metas) (option_map ((+) (-1)) n)
	    (if dep then (subst1 (mkMeta mv) t2) else t2)
      | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t)
      | (n, _) -> (e, List.rev metas, t)
  in 
  clrec (evd,[]) bound t

(* Instantiate the first [bound] products of [t] with evars (all products if
   [bound] is [None]; unfold local defs *)

let clenv_environments_evars env evd bound t =
  let rec clrec (e,ts) n t =
    match n, kind_of_term t with
      | (Some 0, _) -> (e, List.rev ts, t)
      | (n, Cast (t,_,_)) -> clrec (e,ts) n t
      | (n, Prod (na,t1,t2)) ->
          let e',constr = Evarutil.new_evar e env t1 in
	  let dep = dependent (mkRel 1) t2 in
	  clrec (e', constr::ts) (option_map ((+) (-1)) n)
	    (if dep then (subst1 constr t2) else t2)
      | (n, LetIn (na,b,_,t)) -> clrec (e,ts) n (subst1 b t)
      | (n, _) -> (e, List.rev ts, t)
  in 
  clrec (evd,[]) bound t

let clenv_conv_leq env sigma t c bound =
  let ty = Retyping.get_type_of env sigma c in
  let evd = Evd.create_evar_defs sigma in
  let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in
  let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in
  let evars,_ = Evarconv.consider_remaining_unif_problems env evars in
  let args = List.map (whd_evar (Evd.evars_of evars)) args in
  check_evars env sigma evars (applist (c,args));
  args

let mk_clenv_from_n gls n (c,cty) =
  let evd = create_evar_defs gls.sigma in
  let (env,args,concl) = clenv_environments evd n cty in
  { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
    templtyp = mk_freelisted concl;
    evd = env;
    env = Global.env_of_context gls.it.evar_hyps }

let mk_clenv_from gls = mk_clenv_from_n gls None

let mk_clenv_rename_from gls (c,t) = 
  mk_clenv_from gls (c,rename_bound_var (pf_env gls) [] t)

let mk_clenv_rename_from_n gls n (c,t) = 
  mk_clenv_from_n gls n (c,rename_bound_var (pf_env gls) [] t)

let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t)

(******************************************************************)

(* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions
 * mv0, or if one of the free vars on mv1's freelist mentions
 * mv0 *)

let mentions clenv mv0 =
  let rec menrec mv1 =
    mv0 = mv1 ||
    let mlist =
      try (fst (meta_fvalue clenv.evd mv1)).freemetas
      with Anomaly _ | Not_found -> Metaset.empty in
    meta_exists menrec mlist
  in menrec

let clenv_defined clenv mv = meta_defined clenv.evd mv

let error_incompatible_inst clenv mv  =
  let na = meta_name clenv.evd mv in
  match na with
      Name id ->
        errorlabstrm "clenv_assign"
          (str "An incompatible instantiation has already been found for " ++ 
           pr_id id)
    | _ ->
        anomaly "clenv_assign: non dependent metavar already assigned"

(* TODO: replace by clenv_unify (mkMeta mv) rhs ? *)		      
let clenv_assign mv rhs clenv =
  let rhs_fls = mk_freelisted rhs in 
  if meta_exists (mentions clenv mv) rhs_fls.freemetas then
    error "clenv_assign: circularity in unification";
  try
    if meta_defined clenv.evd mv then
      if not (eq_constr (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
        error_incompatible_inst clenv mv
      else
	clenv
    else {clenv with evd = meta_assign mv (rhs_fls.rebus,ConvUpToEta 0) clenv.evd}
  with Not_found -> 
    error "clenv_assign: undefined meta"


let clenv_wtactic f clenv = {clenv with evd = f clenv.evd }


(* [clenv_dependent hyps_only clenv]
 * returns a list of the metavars which appear in the template of clenv,
 * and which are dependent, This is computed by taking the metavars in cval,
 * in right-to-left order, and collecting the metavars which appear
 * in their types, and adding in all the metavars appearing in the
 * type of clenv.
 * If [hyps_only] then metavariables occurring in the type are _excluded_ *)

(* collects all metavar occurences, in left-to-right order, preserving
 * repetitions and all. *)

let collect_metas c = 
  let rec collrec acc c =
    match kind_of_term c with
      | Meta mv -> mv::acc
      | _         -> fold_constr collrec acc c
  in
  List.rev (collrec [] c)

(* [clenv_metavars clenv mv]
 * returns a list of the metavars which appear in the type of
 * the metavar mv.  The list is unordered. *)

let clenv_metavars clenv mv = (meta_ftype clenv mv).freemetas

let dependent_metas clenv mvs conclmetas =
  List.fold_right
    (fun mv deps ->
       Metaset.union deps (clenv_metavars clenv.evd mv))
    mvs conclmetas

let clenv_dependent hyps_only clenv =
  let mvs = collect_metas (clenv_value clenv) in
  let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
  let deps = dependent_metas clenv mvs ctyp_mvs in
  List.filter
    (fun mv -> Metaset.mem mv deps &&
               not (hyps_only && Metaset.mem mv ctyp_mvs))
    mvs

let clenv_missing ce = clenv_dependent true ce

(******************************************************************)

let clenv_unify allow_K cv_pb t1 t2 clenv =
  { clenv with evd = w_unify allow_K clenv.env cv_pb t1 t2 clenv.evd }

let clenv_unique_resolver allow_K clenv gl =
  clenv_unify allow_K CUMUL (clenv_type clenv) (pf_concl gl) clenv


(* [clenv_pose_dependent_evars clenv]
 * For each dependent evar in the clause-env which does not have a value,
 * pose a value for it by constructing a fresh evar.  We do this in
 * left-to-right order, so that every evar's type is always closed w.r.t.
 * metas. *)
let clenv_pose_dependent_evars clenv =
  let dep_mvs = clenv_dependent false clenv in
  List.fold_left
    (fun clenv mv ->
      let ty = clenv_meta_type clenv mv in
      let (evd,evar) = new_evar clenv.evd (cl_env clenv) ty in
      clenv_assign mv evar {clenv with evd=evd})
    clenv
    dep_mvs

let evar_clenv_unique_resolver clenv gls =
  clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)


(******************************************************************)

let connect_clenv gls clenv =
  { clenv with
    evd = evars_reset_evd gls.sigma clenv.evd;
    env = Global.env_of_context gls.it.evar_hyps }

(* [clenv_fchain mv clenv clenv']
 *
 * Resolves the value of "mv" (which must be undefined) in clenv to be
 * the template of clenv' be the value "c", applied to "n" fresh
 * metavars, whose types are chosen by destructing "clf", which should
 * be a clausale forme generated from the type of "c".  The process of
 * resolution can cause unification of already-existing metavars, and
 * of the fresh ones which get created.  This operation is a composite
 * of operations which pose new metavars, perform unification on
 * terms, and make bindings. 

   Otherwise said, from 

     [clenv] = [env;sigma;metas |- c:T]
     [clenv'] = [env';sigma';metas' |- d:U]
     [mv] = [mi] of type [Ti] in [metas]

   then, if the unification of [Ti] and [U] produces map [rho], the
   chaining is [env';sigma';rho'(metas),rho(metas') |- c:rho'(T)] for
   [rho'] being [rho;mi:=d].

   In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma].
*)
let clenv_fchain mv clenv nextclenv =
  (* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
  let clenv' =
    { templval = clenv.templval;
      templtyp = clenv.templtyp;
      evd = meta_merge clenv.evd nextclenv.evd;
      env = nextclenv.env } in
  (* unify the type of the template of [nextclenv] with the type of [mv] *)
  let clenv'' =
    clenv_unify true CUMUL
      (clenv_nf_meta clenv' nextclenv.templtyp.rebus)
      (clenv_meta_type clenv' mv)
      clenv' in
  (* assign the metavar *)
  let clenv''' =
    clenv_assign mv (clenv_nf_meta clenv' nextclenv.templval.rebus) clenv''
  in 
  clenv'''

(***************************************************************)
(* Bindings *)

type arg_bindings = (int * open_constr) list

(* [clenv_independent clenv]
 * returns a list of metavariables which appear in the term cval,
 * and which are not dependent.  That is, they do not appear in
 * the types of other metavars which are in cval, nor in the type
 * of cval, ctyp. *)

let clenv_independent clenv =
  let mvs = collect_metas (clenv_value clenv) in
  let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in
  let deps = dependent_metas clenv mvs ctyp_mvs in
  List.filter (fun mv -> not (Metaset.mem mv deps)) mvs

let meta_of_binder clause loc b t mvs =
  match b with
    | NamedHyp s ->
	if List.exists (fun (_,b',_) -> b=b') t then 
	  errorlabstrm ""
	    (str "The variable " ++ pr_id s ++ 
	     str " occurs more than once in binding");
        meta_with_name clause.evd s
    | AnonHyp n ->
	if List.exists (fun (_,b',_) -> b=b') t then
	  errorlabstrm ""
	    (str "The position " ++ int n ++
	    str " occurs more than once in binding");
	try List.nth mvs (n-1)
	with (Failure _|Invalid_argument _) ->
          errorlabstrm "" (str "No such binder")

let error_already_defined b =
  match b with
    | NamedHyp id ->
        errorlabstrm ""
          (str "Binder name \"" ++ pr_id id ++
           str"\" already defined with incompatible value")
    | AnonHyp n ->
        anomalylabstrm ""
          (str "Position " ++ int n ++ str" already defined")

let clenv_match_args s clause =
  let mvs = clenv_independent clause in 
  let rec matchrec clenv = function
    | [] -> clenv
    | (loc,b,(sigma,c))::t ->
	let k = meta_of_binder clenv loc b t mvs in
        if meta_defined clenv.evd k then
          if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then
            matchrec clenv t
          else error_already_defined b
        else
	  let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
	    (* nf_betaiota was before in type_of - useful to reduce
               types like (x:A)([x]P u) *)
	  let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
	  let c_typ = nf_betaiota (clenv_get_type_of clenv' c) in
	  let c_typ = clenv_hnf_constr clenv' c_typ in
	  let clenv'' =
	    (* Try to infer some Meta/Evar from the type of [c] *)
	    try clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clenv')
	    with e when precatchable_exception e ->
	    (* Try to coerce to the type of [k]; cannot merge with the
	       previous case because Coercion does not handle Meta *)
            let (evd,c') = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in
	    try clenv_unify true CONV (mkMeta k) c' { clenv' with evd = evd }
	    with PretypeError (env,CannotUnify (m,n)) ->
	      Stdpp.raise_with_loc loc
 	        (PretypeError (env,CannotUnifyBindingType (m,n)))
	  in matchrec clenv'' t
  in 
  matchrec clause s


let clenv_constrain_with_bindings bl clause =
  if bl = [] then 
    clause 
  else 
    let all_mvs = collect_metas clause.templval.rebus in
    let rec matchrec clause = function
      | []       -> clause
      | (n,(sigma,c))::t ->
          let k = 
            (try
              if n > 0 then 
		List.nth all_mvs (n-1)
              else if n < 0 then 
		List.nth (List.rev all_mvs) (-n-1)
              else error "clenv_constrain_with_bindings" 
            with Failure _ ->
              errorlabstrm "clenv_constrain_with_bindings"
                (str"Clause did not have " ++ int n ++ str"-th" ++
                str" absolute argument")) in
	  let k_typ = nf_betaiota (clenv_meta_type clause k) in
	  let cl = { clause with evd = evar_merge clause.evd sigma} in
	  let c_typ = nf_betaiota (clenv_get_type_of cl c) in 
	  matchrec
            (clenv_assign k c (clenv_unify true CUMUL c_typ k_typ clause)) t
    in 
    matchrec clause bl


(* not exported: maybe useful ? *)
let clenv_constrain_dep_args hyps_only clause = function
  | [] -> clause 
  | mlist ->
      let occlist = clenv_dependent hyps_only clause in
      if List.length occlist = List.length mlist then
	List.fold_left2
          (fun clenv k (sigma,c) ->
	    let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
	    let clenv' = { clenv with evd = evar_merge clenv.evd sigma} in
	    let c_typ = clenv_hnf_constr clenv' (clenv_get_type_of clenv' c) in
	    try
              (* faire quelque chose avec le sigma retourne ? *)
	      let evd,c' = w_coerce (cl_env clenv') c c_typ k_typ clenv'.evd in
	      clenv_unify true CONV (mkMeta k) c' { clenv' with evd = evd }
	    with _ ->
              clenv_unify true CONV (mkMeta k) c clenv')
          clause occlist mlist
      else 
	error ("Not the right number of missing arguments (expected "
	       ^(string_of_int (List.length occlist))^")")

let clenv_constrain_missing_args mlist clause =
  clenv_constrain_dep_args true clause mlist


(****************************************************************)
(* Clausal environment for an application *)

let make_clenv_binding_gen hyps_only n gls (c,t) = function
  | ImplicitBindings largs ->
      let clause = mk_clenv_from_n gls n (c,t) in
      clenv_constrain_dep_args hyps_only clause largs
  | ExplicitBindings lbind ->
      let clause = mk_clenv_rename_from_n gls n (c,t) in
      clenv_match_args lbind clause
  | NoBindings ->
      mk_clenv_from_n gls n (c,t)

let make_clenv_binding_apply gls n = make_clenv_binding_gen true n gls
let make_clenv_binding = make_clenv_binding_gen false None

(****************************************************************)
(* Pretty-print *)

let pr_clenv clenv =
  h 0
    (str"TEMPL: " ++ print_constr clenv.templval.rebus ++
     str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++
     pr_evar_defs clenv.evd)