(************************************************************************)
(*  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: subtac_pretyping.ml 9976 2007-07-12 11:58:30Z msozeau $ *)

open Global
open Pp
open Util
open Names
open Sign
open Evd
open Term
open Termops
open Reductionops
open Environ
open Type_errors
open Typeops
open Libnames
open Classops
open List
open Recordops 
open Evarutil
open Pretype_errors
open Rawterm
open Evarconv
open Pattern
open Dyn

open Subtac_coercion
open Subtac_utils
open Coqlib
open Printer
open Subtac_errors
open Eterm

module Pretyping = Subtac_pretyping_F.SubtacPretyping_F(Subtac_coercion.Coercion)

open Pretyping

let _ = Pretyping.allow_anonymous_refs := true

type recursion_info = {
  arg_name: name;
  arg_type: types; (* A *)
  args_after : rel_context;
  wf_relation: constr; (* R : A -> A -> Prop *)
  wf_proof: constr; (* : well_founded R *)
  f_type: types; (* f: A -> Set *)
  f_fulltype: types; (* Type with argument and wf proof product first *)
}

let my_print_rec_info env t = 
  str "Name: " ++ Nameops.pr_name t.arg_name ++ spc () ++
  str "Arg type: " ++ my_print_constr env t.arg_type ++ spc () ++
  str "Wf relation: " ++ my_print_constr env t.wf_relation ++ spc () ++
  str "Wf proof: " ++ my_print_constr env t.wf_proof ++ spc () ++
  str "Abbreviated Type: " ++ my_print_constr env t.f_type ++ spc () ++
  str "Full type: " ++ my_print_constr env t.f_fulltype
(*   trace (str "pretype for " ++ (my_print_rawconstr env c) ++ *)
(* 	   str " and tycon "++ my_print_tycon env tycon ++ *)
(* 	   str " in environment: " ++ my_print_env env); *)

let merge_evms x y = 
  Evd.fold (fun ev evi evm -> Evd.add evm ev evi) x y

let interp env isevars c tycon = 
  let j = pretype tycon env isevars ([],[]) c in
  let evm = evars_of !isevars in    
    nf_evar evm j.uj_val, nf_evar evm j.uj_type

let find_with_index x l =
  let rec aux i = function
      (y, _, _) as t :: tl -> if x = y then i, t else aux (succ i) tl
    | [] -> raise Not_found
  in aux 0 l

let list_split_at index l = 
  let rec aux i acc = function
      hd :: tl when i = index -> (List.rev acc), tl
    | hd :: tl -> aux (succ i) (hd :: acc) tl
    | [] -> failwith "list_split_at: Invalid argument"
  in aux 0 [] l

open Vernacexpr

let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env
let coqintern_type evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_type (evars_of evd) env

let env_with_binders env isevars l =
  let rec aux ((env, rels) as acc) = function
      Topconstr.LocalRawDef ((loc, name), def) :: tl -> 
	let rawdef = coqintern_constr !isevars env def in
	let coqdef, deftyp = interp env isevars rawdef empty_tycon in
	let reldecl = (name, Some coqdef, deftyp) in
	  aux  (push_rel reldecl env, reldecl :: rels) tl
    | Topconstr.LocalRawAssum (bl, typ) :: tl ->
	let rawtyp = coqintern_type !isevars env typ in
	let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in
	let acc = 
	  List.fold_left (fun (env, rels) (loc, name) -> 
			    let reldecl = (name, None, coqtyp) in
			      (push_rel reldecl env, 
			       reldecl :: rels))
	    (env, rels) bl
	in aux acc tl
    | [] -> acc
  in aux (env, []) l

let subtac_process env isevars id l c tycon =
  let c = Command.abstract_constr_expr c l in
(*   let env_binders, binders_rel = env_with_binders env isevars l in *)
  let tycon = 
    match tycon with
	None -> empty_tycon
      | Some t -> 
	  let t = Command.generalize_constr_expr t l in
	  let t = coqintern_type !isevars env t in
	  let coqt, ttyp = interp env isevars t empty_tycon in
	    mk_tycon coqt
  in    
  let c = coqintern_constr !isevars env c in
  let coqc, ctyp = interp env isevars c tycon in
(*   let _ = try trace (str "Interpreted term: " ++ my_print_constr env coqc ++ spc () ++ *)
(* 		 str "Coq type: " ++ my_print_constr env ctyp) *)
(*   with _ -> () *)
(*   in *)
(*   let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !isevars))  with _ -> () in *)
    
(*   let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel  *)
(*   and fullctyp = it_mkProd_or_LetIn ctyp binders_rel *)
(*   in *)
  let fullcoqc = Evarutil.nf_evar (evars_of !isevars) coqc in
  let fullctyp = Evarutil.nf_evar (evars_of !isevars) ctyp in
(*   let evm = evars_of_term (evars_of !isevars) Evd.empty fullctyp in *)
(*   let evm = evars_of_term (evars_of !isevars) evm fullcoqc in *)
(*   let _ = try trace (str "After evar normalization remain: " ++ spc () ++ *)
(* 		       Evd.pr_evar_map evm) *)
(*   with _ -> () *)
(*   in *)
  let evm = non_instanciated_map env isevars (evars_of !isevars) in
(*   let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm)  with _ -> () in *)
    evm, fullcoqc, fullctyp

open Subtac_obligations

let subtac_proof env isevars id l c tycon =
  let nc = named_context env in
  let nc_len = named_context_length nc in
  let evm, coqc, coqt = subtac_process env isevars id l c tycon in
  let evars, def = Eterm.eterm_obligations id nc_len !isevars evm 0 coqc (Some coqt) in
    add_definition id def coqt evars