(** -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)

open Evd
open Libnames
open Coqlib
open Term
open Names
open Util

let ($) f x = f x

(****************************************************************************)
(* Library linking *)

let contrib_name = "Program"

let subtac_dir = [contrib_name]
let fixsub_module = subtac_dir @ ["Wf"]
let utils_module = subtac_dir @ ["Utils"]
let tactics_module = subtac_dir @ ["Tactics"]
let init_constant dir s () = gen_constant contrib_name dir s
let init_reference dir s () = gen_reference contrib_name dir s

let safe_init_constant md name () =
  check_required_library ("Coq"::md);
  init_constant md name ()

let ex_pi1 = init_constant utils_module "ex_pi1"
let ex_pi2 = init_constant utils_module "ex_pi2"

let make_ref l s = init_reference l s
let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
let acc_ref = make_ref  ["Init";"Wf"] "Acc"
let acc_inv_ref = make_ref  ["Init";"Wf"] "Acc_inv"
let fix_sub_ref = make_ref fixsub_module "Fix_sub"
let measure_on_R_ref = make_ref fixsub_module "MR"
let fix_measure_sub_ref = make_ref fixsub_module "Fix_measure_sub"
let refl_ref = make_ref ["Init";"Logic"] "refl_equal"

let make_ref s = Qualid (dummy_loc, qualid_of_string s)
let lt_ref = make_ref "Init.Peano.lt"
let sig_ref = make_ref "Init.Specif.sig"
let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"

let build_sig () =
  { proj1 = init_constant ["Init"; "Specif"] "proj1_sig" ();
    proj2 = init_constant ["Init"; "Specif"] "proj2_sig" ();
    elim = init_constant ["Init"; "Specif"] "sig_rec" ();
    intro = init_constant ["Init"; "Specif"] "exist" ();
    typ = init_constant ["Init"; "Specif"] "sig" () }

let sig_ = build_sig

let fix_proto = safe_init_constant tactics_module "fix_proto"

let hide_obligation = safe_init_constant tactics_module "obligation"

let eq_ind = init_constant ["Init"; "Logic"] "eq"
let eq_rec = init_constant ["Init"; "Logic"] "eq_rec"
let eq_rect = init_constant ["Init"; "Logic"] "eq_rect"
let eq_refl = init_constant ["Init"; "Logic"] "refl_equal"
let eq_ind_ref = init_reference ["Init"; "Logic"] "eq"
let refl_equal_ref = init_reference ["Init"; "Logic"] "refl_equal"

let not_ref = init_constant ["Init"; "Logic"] "not"

let and_typ = Coqlib.build_coq_and

let eqdep_ind = init_constant [ "Logic";"Eqdep"] "eq_dep"
let eqdep_rec = init_constant ["Logic";"Eqdep"] "eq_dep_rec"
let eqdep_ind_ref = init_reference [ "Logic";"Eqdep"] "eq_dep"
let eqdep_intro_ref = init_reference [ "Logic";"Eqdep"] "eq_dep_intro"

let jmeq_ind =
  safe_init_constant ["Logic";"JMeq"] "JMeq"

let jmeq_rec =
  init_constant ["Logic";"JMeq"] "JMeq_rec"

let jmeq_refl =
  init_constant ["Logic";"JMeq"] "JMeq_refl"

let ex_ind = init_constant ["Init"; "Logic"] "ex"
let ex_intro = init_reference ["Init"; "Logic"] "ex_intro"

let proj1 = init_constant ["Init"; "Logic"] "proj1"
let proj2 = init_constant ["Init"; "Logic"] "proj2"

let existS = build_sigma_type

let prod = build_prod


(* orders *)
let well_founded = init_constant ["Init"; "Wf"] "well_founded"
let fix = init_constant ["Init"; "Wf"] "Fix"
let acc = init_constant ["Init"; "Wf"] "Acc"
let acc_inv = init_constant ["Init"; "Wf"] "Acc_inv"

let extconstr = Constrextern.extern_constr true (Global.env ())
let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s)

open Pp

let my_print_constr = Termops.print_constr_env
let my_print_constr_expr = Ppconstr.pr_constr_expr
let my_print_rel_context env ctx = Printer.pr_rel_context env ctx
let my_print_context = Termops.print_rel_context
let my_print_named_context = Termops.print_named_context
let my_print_env = Termops.print_env
let my_print_glob_constr = Printer.pr_glob_constr_env
let my_print_evardefs = Evd.pr_evar_map None

let my_print_tycon_type = Evarutil.pr_tycon_type

let debug_level = 2

let debug_on = true

let debug n s =
  if debug_on then
    if !Flags.debug && n >= debug_level then
      msgnl s
    else ()
  else ()

let debug_msg n s =
  if debug_on then
    if !Flags.debug  && n >= debug_level then s
    else mt ()
  else mt ()

let trace s =
  if debug_on then
    if !Flags.debug  && debug_level > 0 then msgnl s
    else ()
  else ()

let rec pp_list f = function
    [] -> mt()
  | x :: y -> f x ++ spc () ++ pp_list f y

let wf_relations = Hashtbl.create 10

let std_relations () =
  let add k v = Hashtbl.add wf_relations k v in
    add (init_constant ["Init"; "Peano"] "lt" ())
      (init_constant ["Arith"; "Wf_nat"] "lt_wf")

let std_relations = Lazy.lazy_from_fun std_relations

type binders = Topconstr.local_binder list

let app_opt c e =
  match c with
      Some constr -> constr e
    | None -> e

let print_args env args =
  Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "")

let make_existential loc ?(opaque = Define true) env isevars c =
  Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c

let no_goals_or_obligations = function
  | GoalEvar | QuestionMark _ -> false
  | _ -> true

let make_existential_expr loc env c =
  let key = Evarutil.new_untyped_evar () in
  let evar = Topconstr.CEvar (loc, key, None) in
    debug 2 (str "Constructed evar " ++ int key);
    evar

let string_of_hole_kind = function
  | ImplicitArg _ -> "ImplicitArg"
  | BinderType _ -> "BinderType"
  | QuestionMark _ -> "QuestionMark"
  | CasesType -> "CasesType"
  | InternalHole -> "InternalHole"
  | TomatchTypeParameter _ -> "TomatchTypeParameter"
  | GoalEvar -> "GoalEvar"
  | ImpossibleCase -> "ImpossibleCase"
  | MatchingVar _ -> "MatchingVar"

let evars_of_term evc init c =
  let rec evrec acc c =
    match kind_of_term c with
    | Evar (n, _) when Evd.mem evc n -> Evd.add acc n (Evd.find evc n)
    | Evar (n, _) -> assert(false)
    | _ -> fold_constr evrec acc c
  in
    evrec init c

let non_instanciated_map env evd evm =
  List.fold_left
    (fun evm (key, evi) ->
       let (loc,k) = evar_source key !evd in
	 debug 2 (str "evar " ++ int key ++ str " has kind " ++
		    str (string_of_hole_kind k));
	 match k with
	 | QuestionMark _ -> Evd.add evm key evi
	 | ImplicitArg (_,_,false) -> Evd.add evm key evi
	 | _ ->
	     debug 2 (str " and is an implicit");
	     Pretype_errors.error_unsolvable_implicit loc env evm (Evarutil.nf_evar_info evm evi) k None)
    Evd.empty (Evarutil.non_instantiated evm)

let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition

let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma
let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma

let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint
let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint

open Tactics
open Tacticals

let filter_map f l =
  let rec aux acc = function
      hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
		     | None -> aux acc tl)
    | [] -> List.rev acc
  in aux [] l

let build_dependent_sum l =
  let rec aux names conttac conttype = function
      (n, t) :: ((_ :: _) as tl) ->
	let hyptype = substl names t in
	  trace (spc () ++ str ("treating evar " ^ string_of_id n));
	  (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
	   with _ -> ());
	let tac = assert_tac (Name n) hyptype in
	let conttac =
	  (fun cont ->
	     conttac
	     (tclTHENS tac
		([intros;
		  (tclTHENSEQ
		     [constructor_tac false (Some 1) 1
			(Glob_term.ImplicitBindings [mkVar n]);
		      cont]);
		 ])))
	in
	let conttype =
	  (fun typ ->
	     let tex = mkLambda (Name n, t, typ) in
	       conttype
		 (mkApp (ex_ind (), [| t; tex |])))
	in
	  aux (mkVar n :: names) conttac conttype tl
    | (n, t) :: [] ->
	(conttac intros, conttype t)
    | [] -> raise (Invalid_argument "build_dependent_sum")
  in aux [] identity identity (List.rev l)

open Proof_type
open Tacexpr

let mkProj1 a b c =
  mkApp (delayed_force proj1, [| a; b; c |])

let mkProj2 a b c =
  mkApp (delayed_force proj2, [| a; b; c |])

let mk_ex_pi1 a b c =
  mkApp (delayed_force ex_pi1, [| a; b; c |])

let mk_ex_pi2 a b c =
  mkApp (delayed_force ex_pi2, [| a; b; c |])

let mkSubset name typ prop =
  mkApp ((delayed_force sig_).typ,
	 [| typ; mkLambda (name, typ, prop) |])

let mk_eq typ x y = mkApp (delayed_force eq_ind, [| typ; x ; y |])
let mk_eq_refl typ x = mkApp (delayed_force eq_refl, [| typ; x |])
let mk_JMeq typ x typ' y = mkApp (delayed_force jmeq_ind, [| typ; x ; typ'; y |])
let mk_JMeq_refl typ x = mkApp (delayed_force jmeq_refl, [| typ; x |])

let unsafe_fold_right f = function
    hd :: tl -> List.fold_right f tl hd
  | [] -> raise (Invalid_argument "unsafe_fold_right")

let mk_conj l =
  let conj_typ = delayed_force and_typ in
    unsafe_fold_right
      (fun c conj ->
	 mkApp (conj_typ, [| c ; conj |]))
      l

let mk_not c =
  let notc = delayed_force not_ref in
    mkApp (notc, [| c |])

let and_tac l hook =
  let andc = Coqlib.build_coq_and () in
  let rec aux ((accid, goal, tac, extract) as acc) = function
    | [] -> (* Singleton *) acc

    | (id, x, elgoal, eltac) :: tl ->
	let tac' = tclTHEN simplest_split (tclTHENLIST [tac; eltac]) in
	let proj = fun c -> mkProj2 goal elgoal c in
	let extract = List.map (fun (id, x, y, f) -> (id, x, y, (fun c -> f (mkProj1 goal elgoal c)))) extract in
	  aux ((string_of_id id) ^ "_" ^ accid, mkApp (andc, [| goal; elgoal |]), tac',
	       (id, x, elgoal, proj) :: extract) tl

  in
  let and_proof_id, and_goal, and_tac, and_extract =
    match l with
      | [] -> raise (Invalid_argument "and_tac: empty list of goals")
      | (hdid, x, hdg, hdt) :: tl ->
	  aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl
  in
  let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in
    Lemmas.start_proof and_proofid goal_kind and_goal
      (hook (fun c -> List.map (fun (id, x, t, f) -> (id, x, t, f c)) and_extract));
    trace (str "Started and proof");
    Pfedit.by and_tac;
    trace (str "Applied and tac")


let destruct_ex ext ex =
  let rec aux c acc =
    match kind_of_term c with
	App (f, args) ->
	  (match kind_of_term f with
	       Ind i when i = Term.destInd (delayed_force ex_ind) && Array.length args = 2 ->
		 let (dom, rng) =
		   try (args.(0), args.(1))
		   with _ -> assert(false)
		 in
		 let pi1 = (mk_ex_pi1 dom rng acc) in
		 let rng_body =
		   match kind_of_term rng with
		       Lambda (_, _, t) -> subst1 pi1 t
		     | t -> rng
		 in
		   pi1 :: aux rng_body (mk_ex_pi2 dom rng acc)
	     | _ -> [acc])
      | _ -> [acc]
  in aux ex ext

open Glob_term

let id_of_name = function
    Name n -> n
  | Anonymous -> raise (Invalid_argument "id_of_name")

let definition_message id =
  Nameops.pr_id id ++ str " is defined"

let recursive_message v =
  match Array.length v with
    | 0 -> error "no recursive definition"
    | 1 -> (Printer.pr_constant (Global.env ()) v.(0) ++ str " is recursively defined")
    | _ -> hov 0 (prvect_with_sep pr_comma (Printer.pr_constant (Global.env ())) v ++
		    spc () ++ str "are recursively defined")

let print_message m =
  Flags.if_verbose ppnl m

(* Solve an obligation using tactics, return the corresponding proof term *)
let solve_by_tac evi t =
  let id = id_of_string "H" in
  try
    Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl
    (fun _ _ -> ());
    Pfedit.by (tclCOMPLETE t);
    let _,(const,_,_,_) = Pfedit.cook_proof ignore in
      Pfedit.delete_current_proof (); 
      Inductiveops.control_only_guard (Global.env ())
	const.Entries.const_entry_body;
      const.Entries.const_entry_body
  with e ->
    Pfedit.delete_current_proof();
    raise e

(* let apply_tac t goal = t goal *)

(* let solve_by_tac evi t = *)
(*   let ev = 1 in *)
(*   let evm = Evd.add Evd.empty ev evi in *)
(*   let goal = {it = evi; sigma = evm } in *)
(*   let (res, valid) = apply_tac t goal in *)
(*     if res.it = [] then *)
(*       let prooftree = valid [] in *)
(*       let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *)
(* 	if obls = [] then proofterm *)
(* 	else raise Exit *)
(*     else raise Exit *)

let rec string_of_list sep f = function
    [] -> ""
  | x :: [] -> f x
  | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl

let string_of_intset d =
  string_of_list "," string_of_int (Intset.elements d)

(**********************************************************)
(* Pretty-printing *)
open Printer
open Ppconstr
open Nameops
open Evd

let pr_meta_map evd =
  let ml = meta_list evd in
  let pr_name = function
      Name id -> str"[" ++ pr_id id ++ str"]"
    | _ -> mt() in
  let pr_meta_binding = function
    | (mv,Cltyp (na,b)) ->
      	hov 0
	  (pr_meta mv ++ pr_name na ++ str " : " ++
           Termops.print_constr b.rebus ++ fnl ())
    | (mv,Clval(na,b,_)) ->
      	hov 0
	  (pr_meta mv ++ pr_name na ++ str " := " ++
             Termops.print_constr (fst b).rebus ++ fnl ())
  in
  prlist pr_meta_binding ml

let pr_idl idl = prlist_with_sep pr_spc pr_id idl

let pr_evar_info evi =
  let phyps =
    (*pr_idl (List.rev (ids_of_named_context (evar_context evi))) *)
    Printer.pr_named_context (Global.env()) (evar_context evi)
  in
  let pty = Termops.print_constr evi.evar_concl in
  let pb =
    match evi.evar_body with
      | Evar_empty -> mt ()
      | Evar_defined c -> spc() ++ str"=> "  ++ Termops.print_constr c
  in
  hov 2 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]")

let pr_evar_map sigma =
  h 0
    (prlist_with_sep pr_fnl
      (fun (ev,evi) ->
        h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
      (to_list sigma))

let pr_constraints pbs =
  h 0
    (prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
      Termops.print_constr t1 ++ spc() ++
      str (match pbty with
	| Reduction.CONV -> "=="
	| Reduction.CUMUL -> "<=") ++
      spc() ++ Termops.print_constr t2) pbs)

let pr_evar_map evd =
  let pp_evm =
    let evars =  evd in
    if evars = empty then mt() else
      str"EVARS:"++brk(0,1)++pr_evar_map evars++fnl() in
  let pp_met =
    if meta_list evd = [] then mt() else
      str"METAS:"++brk(0,1)++pr_meta_map evd in
  v 0 (pp_evm ++ pp_met)

let contrib_tactics_path =
  make_dirpath (List.map id_of_string ["Tactics";contrib_name;"Coq"])

let tactics_tac s =
  lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s))

let tactics_call tac args =
  TacArg(dummy_loc,TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args))