open Closure
open RedFlags
open Declarations
open Entries
open Libobject
open Pattern
open Matching
open Pp
open Rawterm
open Sign
open Tacred
open Util
open Names
open Nameops
open Libnames
open Nametab
open Pfedit
open Proof_type
open Refiner
open Tacmach
open Tactic_debug
open Topconstr
open Term
open Termops
open Tacexpr
open Safe_typing
open Typing
open Hiddentac
open Genarg
open Decl_kinds
open Mod_subst
open Printer
open Inductiveops
open Syntax_def
open Environ
open Tactics
open Tacticals
open Tacinterp
open Vernacexpr
open Notation
open Evd
open Evarutil

module SPretyping = Subtac_pretyping.Pretyping
open Subtac_utils
open Pretyping
open Subtac_obligations

(*********************************************************************)
(* Functions to parse and interpret constructions *)

let evar_nf isevars c =
  Evarutil.nf_evar !isevars c

let interp_gen kind isevars env
               ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[]))
               c =
  let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in
  let c' = SPretyping.understand_tcc_evars isevars env kind c' in
    evar_nf isevars c'

let interp_constr isevars env c =
  interp_gen (OfType None) isevars env c

let interp_type_evars isevars env ?(impls=[]) c =
  interp_gen IsType isevars env ~impls c

let interp_casted_constr isevars env ?(impls=[]) c typ =
  interp_gen (OfType (Some typ)) isevars env ~impls c

let interp_casted_constr_evars isevars env ?(impls=[]) c typ =
  interp_gen (OfType (Some typ)) isevars env ~impls c

let interp_open_constr isevars env c =
    msgnl (str "Pretyping " ++ my_print_constr_expr c);
  let c = Constrintern.intern_constr ( !isevars) env c in
  let c' = SPretyping.understand_tcc_evars isevars env (OfType None) c in
    evar_nf isevars c'

let interp_constr_judgment isevars env c =
  let j =
    SPretyping.understand_judgment_tcc isevars env
      (Constrintern.intern_constr ( !isevars) env c)
  in
    { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }

let locate_if_isevar loc na = function
  | RHole _ ->
      (try match na with
	| Name id ->  Reserve.find_reserved_type id
	| Anonymous -> raise Not_found
      with Not_found -> RHole (loc, Evd.BinderType na))
  | x -> x

let interp_binder sigma env na t =
  let t = Constrintern.intern_gen true ( !sigma) env t in
    SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_rawconstr t) na t)

let interp_context_evars evdref env params =
  let bl = Constrintern.intern_context false ( !evdref) env params in
  let (env, par, _, impls) =
    List.fold_left
      (fun (env,params,n,impls) (na, k, b, t) ->
	match b with
	    None ->
	      let t' = locate_if_isevar (loc_of_rawconstr t) na t in
	      let t = SPretyping.understand_tcc_evars evdref env IsType t' in
	      let d = (na,None,t) in
	      let impls =
		if k = Implicit then
		  let na = match na with Name n -> Some n | Anonymous -> None in
		    (ExplByPos (n, na), (true, true, true)) :: impls
		else impls
	      in
		(push_rel d env, d::params, succ n, impls)
	  | Some b ->
	      let c = SPretyping.understand_judgment_tcc evdref env b in
	      let d = (na, Some c.uj_val, c.uj_type) in
		(push_rel d env,d::params, succ n, impls))
      (env,[],1,[]) (List.rev bl)
  in (env, par), impls

(* try to find non recursive definitions *)

let list_chop_hd i l = match list_chop i l with
  | (l1,x::l2) -> (l1,x,l2)
  | (x :: [], l2) -> ([], x, [])
  | _ -> assert(false)

let collect_non_rec env =
  let rec searchrec lnonrec lnamerec ldefrec larrec nrec =
    try
      let i =
        list_try_find_i
          (fun i f ->
             if List.for_all (fun (_, def) -> not (occur_var env f def)) ldefrec
             then i else failwith "try_find_i")
          0 lnamerec
      in
      let (lf1,f,lf2) = list_chop_hd i lnamerec in
      let (ldef1,def,ldef2) = list_chop_hd i ldefrec in
      let (lar1,ar,lar2) = list_chop_hd i larrec in
      let newlnv =
	try
	  match list_chop i nrec with
            | (lnv1,_::lnv2) -> (lnv1@lnv2)
	    | _ -> [] (* nrec=[] for cofixpoints *)
        with Failure "list_chop" -> []
      in
      searchrec ((f,def,ar)::lnonrec)
	(lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv
    with Failure "try_find_i" ->
      (List.rev lnonrec,
       (Array.of_list lnamerec, Array.of_list ldefrec,
        Array.of_list larrec, Array.of_list nrec))
  in
  searchrec []

let list_of_local_binders l =
  let rec aux acc = function
      Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl
    | Topconstr.LocalRawAssum (nl, k, c) :: tl ->
	aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl
    | [] -> List.rev acc
  in aux [] l

let lift_binders k n l =
  let rec aux n = function
    | (id, t, c) :: tl -> (id, Option.map (liftn k n) t, liftn k n c) :: aux (pred n) tl
    | [] -> []
  in aux n l

let rec gen_rels = function
    0 -> []
  | n -> mkRel n :: gen_rels (pred n)

let split_args n rel = match list_chop ((List.length rel) - n) rel with
    (l1, x :: l2) -> l1, x, l2
  | _ -> assert(false)

open Coqlib

let sigT = Lazy.lazy_from_fun build_sigma_type
let sigT_info = lazy
  { ci_ind       = destInd (Lazy.force sigT).typ;
    ci_npar      = 2;
    ci_cstr_nargs = [|2|];
    ci_pp_info   =  { ind_nargs = 0; style = LetStyle }
  }

let telescope = function
  | [] -> assert false
  | [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1
  | (n, None, t) :: tl ->
      let ty, tys, (k, constr) =
	List.fold_left
	  (fun (ty, tys, (k, constr)) (n, b, t) ->
	    let pred = mkLambda (n, t, ty) in
	    let sigty = mkApp ((Lazy.force sigT).typ, [|t; pred|]) in
	    let intro = mkApp ((Lazy.force sigT).intro, [|lift k t; lift k pred; mkRel k; constr|]) in
	      (sigty, pred :: tys, (succ k, intro)))
	  (t, [], (2, mkRel 1)) tl
      in
      let (last, subst) = List.fold_right2
	(fun pred (n, b, t) (prev, subst) ->
	  let proj1 = applistc (Lazy.force sigT).proj1 [t; pred; prev] in
	  let proj2 = applistc (Lazy.force sigT).proj2 [t; pred; prev] in
	    (lift 1 proj2, (n, Some proj1, t) :: subst))
	(List.rev tys) tl (mkRel 1, [])
      in ty, ((n, Some last, t) :: subst), constr

  | _ -> raise (Invalid_argument "telescope")

let nf_evar_context isevars ctx =
  List.map (fun (n, b, t) ->
    (n, Option.map (Evarutil.nf_evar isevars) b, Evarutil.nf_evar isevars t)) ctx

let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
  Coqlib.check_required_library ["Coq";"Program";"Wf"];
  let sigma = Evd.empty in
  let isevars = ref (Evd.create_evar_defs sigma) in
  let env = Global.env() in
  let _pr c = my_print_constr env c in
  let _prr = Printer.pr_rel_context env in
  let _prn = Printer.pr_named_context env in
  let _pr_rel env = Printer.pr_rel_context env in
  let (env', binders_rel), impls = interp_context_evars isevars env bl in
  let len = List.length binders_rel in
  let top_env = push_rel_context binders_rel env in
  let top_arity = interp_type_evars isevars top_env arityc in
  let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
  let argtyp, letbinders, make = telescope binders_rel in
  let argname = id_of_string "recarg" in
  let arg = (Name argname, None, argtyp) in
  let binders = letbinders @ [arg] in
  let binders_env = push_rel_context binders_rel env in
  let rel = interp_constr isevars env r in
  let relty = type_of env !isevars rel in
  let relargty =
    let error () =
      user_err_loc (constr_loc r,
		   "Subtac_command.build_wellfounded",
		   my_print_constr env rel ++ str " is not an homogeneous binary relation.")
    in
      try
	let ctx, ar = Reductionops.splay_prod_n env !isevars 2 relty in
	  match ctx, kind_of_term ar with
	  | [(_, None, t); (_, None, u)], Sort (Prop Null)
	      when Reductionops.is_conv env !isevars t u -> t
	  | _, _ -> error ()
      with _ -> error ()
  in
  let measure = interp_casted_constr isevars binders_env measure relargty in
  let wf_rel, wf_rel_fun, measure_fn =
    let measure_body, measure =
      it_mkLambda_or_LetIn measure letbinders,
      it_mkLambda_or_LetIn measure binders
    in
    let comb = constr_of_global (delayed_force measure_on_R_ref) in
    let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
    let wf_rel_fun x y =
      mkApp (rel, [| subst1 x measure_body;
 		     subst1 y measure_body |])
    in wf_rel, wf_rel_fun, measure
  in
  let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in
  let argid' = id_of_string (string_of_id argname ^ "'") in
  let wfarg len = (Name argid', None,
  		  mkSubset (Name argid') argtyp
		    (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
  in
  let intern_bl = wfarg 1 :: [arg] in
  let _intern_env = push_rel_context intern_bl env in
  let proj = (delayed_force sig_).Coqlib.proj1 in
  let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
  let projection = (* in wfarg :: arg :: before *)
    mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
  in
  let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in
  let intern_arity = substl [projection] top_arity_let in
  (* substitute the projection of wfarg for something,
     now intern_arity is in wfarg :: arg *)
  let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
  let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in
  let curry_fun =
    let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
    let arg = mkApp ((delayed_force sig_).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
    let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
    let rcurry = mkApp (rel, [| measure; lift len measure |]) in
    let lam = (Name (id_of_string "recproof"), None, rcurry) in
    let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in
    let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in
      (Name recname, Some body, ty)
  in
  let fun_bl = intern_fun_binder :: [arg] in
  let lift_lets = Termops.lift_rel_context 1 letbinders in
  let intern_body =
    let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in
    let (r, l, impls, scopes) =
      Constrintern.compute_internalization_data env
	Constrintern.Recursive full_arity impls 
    in
    let newimpls = [(recname, (r, l, impls @ 
      [Some (id_of_string "recproof", Impargs.Manual, (true, false))], 
			      scopes @ [None]))] in
    interp_casted_constr isevars ~impls:newimpls
      (push_rel_context ctx env) body (lift 1 top_arity)
  in
  let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
  let prop = mkLambda (Name argname, argtyp, top_arity_let) in
  let def =
    mkApp (constr_of_global (delayed_force fix_sub_ref),
	  [| argtyp ; wf_rel ;
	     make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
	     prop ; intern_body_lam |])
  in
  let _ = isevars := Evarutil.nf_evar_map !isevars in
  let binders_rel = nf_evar_context !isevars binders_rel in
  let binders = nf_evar_context !isevars binders in
  let top_arity = Evarutil.nf_evar !isevars top_arity in
  let hook, recname, typ = 
    if List.length binders_rel > 1 then
      let name = add_suffix recname "_func" in
      let hook l gr = 
	let body = it_mkLambda_or_LetIn (mkApp (constr_of_global gr, [|make|])) binders_rel in
	let ty = it_mkProd_or_LetIn top_arity binders_rel in
	let ce =
	  { const_entry_body = Evarutil.nf_evar !isevars body;
	    const_entry_type = Some ty;
	    const_entry_opaque = false;
	    const_entry_boxed = false} 
	in 
	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
	let gr = ConstRef c in
	  if Impargs.is_implicit_args () || impls <> [] then
	    Impargs.declare_manual_implicits false gr [impls]
      in
      let typ = it_mkProd_or_LetIn top_arity binders in
	hook, name, typ
    else 
      let typ = it_mkProd_or_LetIn top_arity binders_rel in
      let hook l gr = 
	if Impargs.is_implicit_args () || impls <> [] then
	  Impargs.declare_manual_implicits false gr [impls]
      in hook, recname, typ
  in
  let fullcoqc = Evarutil.nf_evar !isevars def in
  let fullctyp = Evarutil.nf_evar !isevars typ in
  let evm = evars_of_term !isevars Evd.empty fullctyp in
  let evm = evars_of_term !isevars evm fullcoqc in
  let evm = non_instanciated_map env isevars evm in
  let evars, _, evars_def, evars_typ = 
    Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp 
  in
    Subtac_obligations.add_definition recname ~term:evars_def evars_typ evars ~hook

let interp_fix_context evdref env fix =
  interp_context_evars evdref env fix.Command.fix_binders

let interp_fix_ccl evdref (env,_) fix =
  interp_type_evars evdref env fix.Command.fix_type

let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
  let env = push_rel_context ctx env_rec in
  let body = Option.map (fun c -> interp_casted_constr_evars evdref env ~impls c ccl) fix.Command.fix_body in
  Option.map (fun c -> it_mkLambda_or_LetIn c ctx) body

let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx

let prepare_recursive_declaration fixnames fixtypes fixdefs =
  let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
  let names = List.map (fun id -> Name id) fixnames in
  (Array.of_list names, Array.of_list fixtypes, Array.of_list defs)

let rel_index n ctx =
  list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx))

let rec unfold f b =
  match f b with
    | Some (x, b') -> x :: unfold f b'
    | None -> []

let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
  match n with
  | Some (loc, n) -> [rel_index n fixctx]
  | None ->
      (* If recursive argument was not given by user, we try all args.
	 An earlier approach was to look only for inductive arguments,
	 but doing it properly involves delta-reduction, and it finally
         doesn't seem to worth the effort (except for huge mutual
	 fixpoints ?) *)
      let len = List.length fixctx in
	unfold (function x when x = len -> None
	  | n -> Some (n, succ n)) 0

let push_named_context = List.fold_right push_named

let check_evars env initial_sigma evd c =
  let sigma =  evd in
  let c = nf_evar sigma c in
  let rec proc_rec c =
    match kind_of_term c with
      | Evar (evk,args) ->
          assert (Evd.mem sigma evk);
	  if not (Evd.mem initial_sigma evk) then
            let (loc,k) = evar_source evk evd in
	      (match k with
	      | QuestionMark _
	      | ImplicitArg (_, _, false) -> ()
	      | _ ->
		  let evi = nf_evar_info sigma (Evd.find sigma evk) in
		    Pretype_errors.error_unsolvable_implicit loc env sigma evi k None)
      | _ -> iter_constr proc_rec c
  in proc_rec c

let out_def = function
  | Some def -> def
  | None -> error "Program Fixpoint needs defined bodies."

let interp_recursive fixkind l boxed =
  let env = Global.env() in
  let fixl, ntnl = List.split l in
  let kind = fixkind <> IsCoFixpoint in
  let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in

  (* Interp arities allowing for unresolved types *)
  let evdref = ref Evd.empty in
  let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in
  let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
  let fixtypes = List.map2 build_fix_type fixctxs fixccls in
  let rec_sign =
    List.fold_left2 (fun env' id t ->
      let sort = Retyping.get_type_of env !evdref t in
      let fixprot =
	try mkApp (delayed_force Subtac_utils.fix_proto, [|sort; t|])
	with e -> t
      in
	(id,None,fixprot) :: env')
      [] fixnames fixtypes
  in
  let env_rec = push_named_context rec_sign env in

  (* Get interpretation metadatas *)
  let impls = Constrintern.compute_internalization_env env
    Constrintern.Recursive fixnames fixtypes fiximps
  in
  let notations = List.flatten ntnl in

  (* Interp bodies with rollback because temp use of notations/implicit *)
  let fixdefs =
    States.with_state_protection (fun () ->
      List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
      list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
      () in

  let fixdefs = List.map out_def fixdefs in

  (* Instantiate evars and check all are resolved *)
  let evd = Evarconv.consider_remaining_unif_problems env_rec !evdref in
  let evd = Typeclasses.resolve_typeclasses
    ~onlyargs:true ~split:true ~fail:false env_rec evd
  in
  let evd = Evarutil.nf_evar_map evd in
  let fixdefs = List.map (nf_evar evd) fixdefs in
  let fixtypes = List.map (nf_evar evd) fixtypes in
  let rec_sign = nf_named_context_evar evd rec_sign in

  let recdefs = List.length rec_sign in
  List.iter (check_evars env_rec Evd.empty evd) fixdefs;
  List.iter (check_evars env Evd.empty evd) fixtypes;
  Command.check_mutuality env kind (List.combine fixnames fixdefs);

  (* Russell-specific code *)

  (* Get the interesting evars, those that were not instanciated *)
  let isevars = Evd.undefined_evars evd in
  let evm =  isevars in
  (* Solve remaining evars *)
  let rec collect_evars id def typ imps =
      (* Generalize by the recursive prototypes  *)
    let def =
      Termops.it_mkNamedLambda_or_LetIn def rec_sign
    and typ =
      Termops.it_mkNamedProd_or_LetIn typ rec_sign
    in
    let evm' = Subtac_utils.evars_of_term evm Evd.empty def in
    let evm' = Subtac_utils.evars_of_term evm evm' typ in
    let evars, _, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
      (id, def, typ, imps, evars)
  in
  let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in
    (match fixkind with
      | IsFixpoint wfl ->
	  let possible_indexes =
	    list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
	  let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
	    Array.of_list fixtypes,
	    Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
	  in
	  let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
	    list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) l
      | IsCoFixpoint -> ());
    Subtac_obligations.add_mutual_definitions defs notations fixkind

let out_n = function
    Some n -> n
  | None -> raise Not_found

let build_recursive l b =
  let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
    match g, l with
	[(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
	  ignore(build_wellfounded (id, n, bl, typ, out_def def) r
		    (match n with Some n -> mkIdentC (snd n) | None ->
		      errorlabstrm "Subtac_command.build_recursive"
			(str "Recursive argument required for well-founded fixpoints"))
		    ntn false)

      | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
	  ignore(build_wellfounded (id, n, bl, typ, out_def def) (Option.default (CRef lt_ref) r)
		    m ntn false)

      | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
	  let fixl = List.map (fun (((_,id),(n,ro),bl,typ,def),ntn) ->
	    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = n;
	      Command.fix_body = def; Command.fix_type = typ},ntn)) l
	  in interp_recursive (IsFixpoint g) fixl b
      | _, _ ->
	  errorlabstrm "Subtac_command.build_recursive"
	    (str "Well-founded fixpoints not allowed in mutually recursive blocks")

let build_corecursive l b =
  let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_annot = None;
      Command.fix_body = def; Command.fix_type = typ},ntn))
    l in
  interp_recursive IsCoFixpoint fixl b