open Printf
open Pp
open Environ
open Term
open Names
open Libnames
open Summary
open Libobject
open Entries
open Decl_kinds
open Errors
open Util
open Evd
open Declare
open Proof_type
open Compat

(**
   - Get types of existentials ;
   - Flatten dependency tree (prefix order) ;
   - Replace existentials by De Bruijn indices in term, applied to the right arguments ;
   - Apply term prefixed by quantification on "existentials".
*)

open Term
open Sign
open Names
open Evd
open List
open Pp
open Errors
open Util
open Proof_type

let declare_fix_ref = ref (fun _ _ _ _ _ -> assert false)
let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)

let trace s =
  if !Flags.debug then (msgnl s; msgerr s)
  else ()

let succfix (depth, fixrels) =
  (succ depth, List.map succ fixrels)

let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n

let check_evars env evm =
  List.iter
  (fun (key, evi) ->
   let (loc,k) = evar_source key evm in
     match k with
     | QuestionMark _
     | ImplicitArg (_,_,false) -> ()
     | _ ->
       Pretype_errors.error_unsolvable_implicit loc env
         evm (Evarutil.nf_evar_info evm evi) k None)
  (Evd.undefined_list evm)

type oblinfo =
  { ev_name: int * identifier;
    ev_hyps: named_context;
    ev_status: obligation_definition_status;
    ev_chop: int option;
    ev_src: hole_kind located;
    ev_typ: types;
    ev_tac: tactic option;
    ev_deps: Intset.t }

(* spiwack: Store field for internalizing ev_tac in evar_infos' evar_extra. *)
open Store.Field
let evar_tactic = Store.field ()

(** Substitute evar references in t using De Bruijn indices,
  where n binders were passed through. *)

let subst_evar_constr evs n idf t = 
  let seen = ref Intset.empty in
  let transparent = ref Idset.empty in
  let evar_info id = List.assoc id evs in
  let rec substrec (depth, fixrels) c = match kind_of_term c with
    | Evar (k, args) ->
	let { ev_name = (id, idstr) ;
	      ev_hyps = hyps ; ev_chop = chop } =
	  try evar_info k
	  with Not_found ->
	    anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
	in
        seen := Intset.add id !seen;
	  (* Evar arguments are created in inverse order,
	     and we must not apply to defined ones (i.e. LetIn's)
	  *)
	let args =
	  let n = match chop with None -> 0 | Some c -> c in
	  let (l, r) = list_chop n (List.rev (Array.to_list args)) in
	    List.rev r
	in
	let args =
	  let rec aux hyps args acc =
	     match hyps, args with
		 ((_, None, _) :: tlh), (c :: tla) ->
		   aux tlh tla ((substrec (depth, fixrels) c) :: acc)
	       | ((_, Some _, _) :: tlh), (_ :: tla) ->
		   aux tlh tla acc
	       | [], [] -> acc
	       | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
	  in aux hyps args []
	in
	  if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then
	    transparent := Idset.add idstr !transparent;
	  mkApp (idf idstr, Array.of_list args)
    | Fix _ ->
	map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c
    | _ -> map_constr_with_binders succfix substrec (depth, fixrels) c
  in
  let t' = substrec (0, []) t in
    t', !seen, !transparent


(** Substitute variable references in t using De Bruijn indices,
  where n binders were passed through. *)
let subst_vars acc n t =
  let var_index id = Util.list_index id acc in
  let rec substrec depth c = match kind_of_term c with
    | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
    | _ -> map_constr_with_binders succ substrec depth c
  in
    substrec 0 t

(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
    to a product : forall H1 : t1, ..., forall Hn : tn, concl.
    Changes evars and hypothesis references to variable references.
*)
let etype_of_evar evs hyps concl =
  let rec aux acc n = function
      (id, copt, t) :: tl ->
	let t', s, trans = subst_evar_constr evs n mkVar t in
	let t'' = subst_vars acc 0 t' in
	let rest, s', trans' = aux (id :: acc) (succ n) tl in
	let s' = Intset.union s s' in
	let trans' = Idset.union trans trans' in
	  (match copt with
	      Some c -> 
		let c', s'', trans'' = subst_evar_constr evs n mkVar c in
		let c' = subst_vars acc 0 c' in
		  mkNamedProd_or_LetIn (id, Some c', t'') rest,
		Intset.union s'' s',
		Idset.union trans'' trans'
	    | None ->
		mkNamedProd_or_LetIn (id, None, t'') rest, s', trans')
    | [] ->
	let t', s, trans = subst_evar_constr evs n mkVar concl in
	  subst_vars acc 0 t', s, trans
  in aux [] 0 (rev hyps)


open Tacticals

let trunc_named_context n ctx =
  let len = List.length ctx in
    list_firstn (len - n) ctx

let rec chop_product n t =
  if n = 0 then Some t
  else
    match kind_of_term t with
      | Prod (_, _, b) ->  if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None
      | _ -> None

let evars_of_evar_info evi =
  Intset.union (Evarutil.evars_of_term evi.evar_concl)
    (Intset.union
	(match evi.evar_body with
	| Evar_empty -> Intset.empty
	| Evar_defined b -> Evarutil.evars_of_term b)
	(Evarutil.evars_of_named_context (evar_filtered_context evi)))

let evar_dependencies evm oev =
  let one_step deps =
    Intset.fold (fun ev s ->
      let evi = Evd.find evm ev in
      let deps' = evars_of_evar_info evi in
	if Intset.mem oev deps' then
	  raise (Invalid_argument ("Ill-formed evar map: cycle detected for evar " ^ string_of_int oev))
	else Intset.union deps' s)
      deps deps
  in
  let rec aux deps =
    let deps' = one_step deps in
      if Intset.equal deps deps' then deps
      else aux deps'
  in aux (Intset.singleton oev)
      
let move_after (id, ev, deps as obl) l = 
  let rec aux restdeps = function
    | (id', _, _) as obl' :: tl -> 
	let restdeps' = Intset.remove id' restdeps in
	  if Intset.is_empty restdeps' then
	    obl' :: obl :: tl
	  else obl' :: aux restdeps' tl
    | [] -> [obl]
  in aux (Intset.remove id deps) l
    
let sort_dependencies evl =
  let rec aux l found list =
    match l with
    | (id, ev, deps) as obl :: tl ->
	let found' = Intset.union found (Intset.singleton id) in
	  if Intset.subset deps found' then
	    aux tl found' (obl :: list)
	  else aux (move_after obl tl) found list
    | [] -> List.rev list
  in aux evl Intset.empty []

let map_evar_body f = function
  | Evar_empty -> Evar_empty
  | Evar_defined c -> Evar_defined (f c)

open Environ
      
let map_evar_info f evi =
  { evi with evar_hyps = 
      val_of_named_context (map_named_context f (named_context_of_val evi.evar_hyps));
    evar_concl = f evi.evar_concl;
    evar_body = map_evar_body f evi.evar_body }
    
let eterm_obligations env name evm fs ?status t ty = 
  (* 'Serialize' the evars *)
  let nc = Environ.named_context env in
  let nc_len = Sign.named_context_length nc in
  let evm = Evarutil.nf_evar_map_undefined evm in
  let evl = List.rev (Evarutil.non_instantiated evm) in
  let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
  let sevl = sort_dependencies evl in
  let evl = List.map (fun (id, ev, _) -> id, ev) sevl in
  let evn =
    let i = ref (-1) in
      List.rev_map (fun (id, ev) -> incr i;
		      (id, (!i, id_of_string
			      (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))),
		       ev)) evl
  in
  let evts =
    (* Remove existential variables in types and build the corresponding products *)
    fold_right
      (fun (id, (n, nstr), ev) l ->
	 let hyps = Evd.evar_filtered_context ev in
	 let hyps = trunc_named_context nc_len hyps in
	 let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in
	 let evtyp, hyps, chop =
	   match chop_product fs evtyp with
	   | Some t -> t, trunc_named_context fs hyps, fs
	   | None -> evtyp, hyps, 0
	 in
	 let loc, k = evar_source id evm in
	 let status = match k with QuestionMark o -> Some o | _ -> status in
	 let status, chop = match status with
	   | Some (Define true as stat) ->
	       if chop <> fs then Define false, None
	       else stat, Some chop
	   | Some s -> s, None
	   | None -> Define true, None
	 in
	 let tac = match evar_tactic.get ev.evar_extra with
	   | Some t ->
	       if Dyn.tag t = "tactic" then
		 Some (Tacinterp.interp 
			  (Tacinterp.globTacticIn (Tacinterp.tactic_out t)))
	       else None
	   | None -> None
	 in
	 let info = { ev_name = (n, nstr);
		      ev_hyps = hyps; ev_status = status; ev_chop = chop;
		      ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = tac }
	 in (id, info) :: l)
      evn []
  in
  let t', _, transparent = (* Substitute evar refs in the term by variables *)
    subst_evar_constr evts 0 mkVar t 
  in
  let ty, _, _ = subst_evar_constr evts 0 mkVar ty in
  let evars = 
    List.map (fun (ev, info) ->
      let { ev_name = (_, name); ev_status = status;
	    ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
      in
      let status = match status with
	| Define true when Idset.mem name transparent -> Define false
	| _ -> status
      in name, typ, src, status, deps, tac) evts
  in
  let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
  let evmap f c = pi1 (subst_evar_constr evts 0 f c) in
    Array.of_list (List.rev evars), (evnames, evmap), t', ty

let tactics_module = ["Program";"Tactics"]
let safe_init_constant md name () =
  Coqlib.check_required_library ("Coq"::md);
  Coqlib.gen_constant "Obligations" md name
let fix_proto = safe_init_constant tactics_module "fix_proto"
let hide_obligation = safe_init_constant tactics_module "obligation"

let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
let pperror cmd = Errors.errorlabstrm "Program" cmd
let error s = pperror (str s)

let reduce c =
  Reductionops.clos_norm_flags Closure.betaiota (Global.env ()) Evd.empty c

exception NoObligations of identifier option

let explain_no_obligations = function
    Some ident -> str "No obligations for program " ++ str (string_of_id ident)
  | None -> str "No obligations remaining"

type obligation_info = (Names.identifier * Term.types * hole_kind located *
			  obligation_definition_status * Intset.t * tactic option) array

type obligation =
  { obl_name : identifier;
    obl_type : types;
    obl_location : hole_kind located;
    obl_body : constr option;
    obl_status : obligation_definition_status;
    obl_deps : Intset.t;
    obl_tac : tactic option;
  }

type obligations = (obligation array * int)

type fixpoint_kind =
  | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list
  | IsCoFixpoint

type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list

type program_info = {
  prg_name: identifier;
  prg_body: constr;
  prg_type: constr;
  prg_obligations: obligations;
  prg_deps : identifier list;
  prg_fixkind : fixpoint_kind option ;
  prg_implicits : (Topconstr.explicitation * (bool * bool * bool)) list;
  prg_notations : notations ;
  prg_kind : definition_kind;
  prg_reduce : constr -> constr;
  prg_hook : unit Tacexpr.declaration_hook;
}

let assumption_message id =
  Flags.if_verbose message ((string_of_id id) ^ " is assumed")

let (set_default_tactic, get_default_tactic, print_default_tactic) = 
  Tactic_option.declare_tactic_option "Program tactic"

(* true = All transparent, false = Opaque if possible *)
let proofs_transparency = ref true

let set_proofs_transparency = (:=) proofs_transparency
let get_proofs_transparency () = !proofs_transparency

open Goptions

let _ =
  declare_bool_option
    { optsync  = true;
      optdepr  = false;
      optname  = "transparency of Program obligations";
      optkey   = ["Transparent";"Obligations"];
      optread  = get_proofs_transparency;
      optwrite = set_proofs_transparency; }

(* true = hide obligations *)
let hide_obligations = ref false

let set_hide_obligations = (:=) hide_obligations
let get_hide_obligations () = !hide_obligations

open Goptions

let _ =
  declare_bool_option
    { optsync  = true;
      optdepr  = false;
      optname  = "Hidding of Program obligations";
      optkey   = ["Hide";"Obligations"];
      optread  = get_hide_obligations;
      optwrite = set_hide_obligations; }

let evar_of_obligation o = make_evar (Global.named_context_val ()) o.obl_type

let get_obligation_body expand obl =
  let c = Option.get obl.obl_body in
    if expand && obl.obl_status = Expand then
      match kind_of_term c with
      | Const c -> constant_value (Global.env ()) c
      | _ -> c
    else c

let obl_substitution expand obls deps =
  Intset.fold
    (fun x acc ->
       let xobl = obls.(x) in
       let oblb =
	 try get_obligation_body expand xobl
	 with _ -> assert(false)
       in (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
    deps []

let subst_deps expand obls deps t =
  let subst = obl_substitution expand obls deps in
    Term.replace_vars (List.map (fun (n, (_, b)) -> n, b) subst) t

let rec prod_app t n =
  match kind_of_term (strip_outer_cast t) with
    | Prod (_,_,b) -> subst1 n b
    | LetIn (_, b, t, b') -> prod_app (subst1 b b') n
    | _ ->
	errorlabstrm "prod_app"
	  (str"Needed a product, but didn't find one" ++ fnl ())


(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
let prod_applist t nL = List.fold_left prod_app t nL

let replace_appvars subst =
  let rec aux c = 
    let f, l = decompose_app c in
      if isVar f then
	try
	  let c' = List.map (map_constr aux) l in
	  let (t, b) = List.assoc (destVar f) subst in
	    mkApp (delayed_force hide_obligation, 
		   [| prod_applist t c'; applistc b c' |])
	with Not_found -> map_constr aux c
      else map_constr aux c
  in map_constr aux
       
let subst_prog expand obls ints prg =
  let subst = obl_substitution expand obls ints in
    if get_hide_obligations () then
      (replace_appvars subst prg.prg_body,
       replace_appvars subst (Termops.refresh_universes prg.prg_type))
    else 
      let subst' = List.map (fun (n, (_, b)) -> n, b) subst in
	(Term.replace_vars subst' prg.prg_body,
	 Term.replace_vars subst' (Termops.refresh_universes prg.prg_type))

let subst_deps_obl obls obl =
  let t' = subst_deps true obls obl.obl_deps obl.obl_type in
    { obl with obl_type = t' }

module ProgMap = Map.Make(struct type t = identifier let compare = compare end)

let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)

let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []

let map_cardinal m =
  let i = ref 0 in
    ProgMap.iter (fun _ _ -> incr i) m;
    !i

exception Found of program_info

let map_first m =
  try
    ProgMap.iter (fun _ v -> raise (Found v)) m;
    assert(false)
  with Found x -> x

let from_prg : program_info ProgMap.t ref = ref ProgMap.empty

let freeze () = !from_prg
let unfreeze v = from_prg := v
let init () = from_prg := ProgMap.empty

(** Beware: if this code is dynamically loaded via dynlink after the start
    of Coq, then this [init] function will not be run by [Lib.init ()].
    Luckily, here we can launch [init] at load-time. *)

let _ = init ()

let _ =
  Summary.declare_summary "program-tcc-table"
    { Summary.freeze_function = freeze;
      Summary.unfreeze_function = unfreeze;
      Summary.init_function = init }

let progmap_union = ProgMap.fold ProgMap.add

let close sec =
  if not (ProgMap.is_empty !from_prg) then
    let keys = map_keys !from_prg in
      errorlabstrm "Program" 
	(str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++
	   prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++
	   (str (if List.length keys = 1 then " has " else "have ") ++
	      str "unsolved obligations"))

let input : program_info ProgMap.t -> obj =
  declare_object
    { (default_object "Program state") with
      cache_function = (fun (na, pi) -> from_prg := pi);
      load_function = (fun _ (_, pi) -> from_prg := pi);
      discharge_function = (fun _ -> close "section"; None);
      classify_function = (fun _ -> close "module"; Dispose) }
    
open Evd

let progmap_remove prg =
  Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg))
  
let progmap_add n prg =
  Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg))

let progmap_replace prg' = 
  Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg))

let rec intset_to = function
    -1 -> Intset.empty
  | n -> Intset.add n (intset_to (pred n))

let subst_body expand prg =
  let obls, _ = prg.prg_obligations in
  let ints = intset_to (pred (Array.length obls)) in
    subst_prog expand obls ints prg

let declare_definition prg =
  let body, typ = subst_body true prg in
  let ce =
    { const_entry_body = body;
      const_entry_secctx = None;
      const_entry_type = Some typ;
      const_entry_opaque = false }
  in
    progmap_remove prg;
    !declare_definition_ref prg.prg_name prg.prg_kind ce prg.prg_implicits
      (fun local gr -> prg.prg_hook local gr; gr)

open Pp
open Ppconstr

let rec lam_index n t acc =
  match kind_of_term t with
    | Lambda (na, _, b) ->
	if na = Name n then acc
	else lam_index n b (succ acc)
    | _ -> raise Not_found

let compute_possible_guardness_evidences (n,_) fixbody fixtype =
  match n with
  | Some (loc, n) -> [lam_index n fixbody 0]
  | 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 m = Term.nb_prod fixtype in
      let ctx = fst (decompose_prod_n_assum m fixtype) in
	list_map_i (fun i _ -> i) 0 ctx

let declare_mutual_definition l =
  let len = List.length l in
  let first = List.hd l in
  let fixdefs, fixtypes, fiximps =
    list_split3
      (List.map (fun x -> 
	let subs, typ = (subst_body true x) in
	let term = snd (Reductionops.splay_lam_n (Global.env ()) Evd.empty len subs) in
	let typ = snd (Reductionops.splay_prod_n (Global.env ()) Evd.empty len typ) in
	  x.prg_reduce term, x.prg_reduce typ, x.prg_implicits) l)
  in
(*   let fixdefs = List.map reduce_fix fixdefs in *)
  let fixkind = Option.get first.prg_fixkind in
  let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
  let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
  let (local,kind) = first.prg_kind in
  let fixnames = first.prg_deps in
  let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
  let indexes, fixdecls =
    match fixkind with
      | IsFixpoint wfl ->
	  let possible_indexes =
	    list_map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in
	  let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
	    Some indexes, list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 l
      | IsCoFixpoint ->
	  None, list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l
  in
  (* Declare the recursive definitions *)
  let kns = list_map4 (!declare_fix_ref kind) fixnames fixdecls fixtypes fiximps in
    (* Declare notations *)
    List.iter Metasyntax.add_notation_interpretation first.prg_notations;
    Declare.recursive_message (fixkind<>IsCoFixpoint) indexes fixnames;
    let gr = List.hd kns in
    let kn = match gr with ConstRef kn -> kn | _ -> assert false in
      first.prg_hook local gr;
      List.iter progmap_remove l; kn
      
let declare_obligation prg obl body =
  let body = prg.prg_reduce body in
  let ty = prg.prg_reduce obl.obl_type in
  match obl.obl_status with
  | Expand -> { obl with obl_body = Some body }
  | Define opaque ->
      let opaque = if get_proofs_transparency () then false else opaque in
      let ce = 
	{ const_entry_body = body;
          const_entry_secctx = None;
	  const_entry_type = Some ty;
	  const_entry_opaque = opaque }
      in
      let constant = Declare.declare_constant obl.obl_name
	(DefinitionEntry ce,IsProof Property)
      in
	if not opaque then
	  Auto.add_hints false [string_of_id prg.prg_name]
	    (Auto.HintsUnfoldEntry [EvalConstRef constant]);
	definition_message obl.obl_name;
	{ obl with obl_body = Some (mkConst constant) }

let init_prog_info n b t deps fixkind notations obls impls kind reduce hook =
  let obls', b = 
    match b with
    | None ->
	assert(obls = [||]);
	let n = Nameops.add_suffix n "_obligation" in
	  [| { obl_name = n; obl_body = None;
	       obl_location = dummy_loc, InternalHole; obl_type = t;
	       obl_status = Expand; obl_deps = Intset.empty; obl_tac = None } |],
	mkVar n
    | Some b ->
	Array.mapi
	  (fun i (n, t, l, o, d, tac) ->
            { obl_name = n ; obl_body = None; 
	      obl_location = l; obl_type = reduce t; obl_status = o;
	      obl_deps = d; obl_tac = tac })
	  obls, b
  in
    { prg_name = n ; prg_body = b; prg_type = reduce t; 
      prg_obligations = (obls', Array.length obls');
      prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
      prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; prg_hook = hook; }

let get_prog name =
  let prg_infos = !from_prg in
    match name with
	Some n ->
	  (try ProgMap.find n prg_infos
	   with Not_found -> raise (NoObligations (Some n)))
      | None ->
	  (let n = map_cardinal prg_infos in
	     match n with
		 0 -> raise (NoObligations None)
	       | 1 -> map_first prg_infos
	       | _ -> error "More than one program with unsolved obligations")

let get_prog_err n =
  try get_prog n with NoObligations id -> pperror (explain_no_obligations id)

let obligations_solved prg = (snd prg.prg_obligations) = 0

let all_programs () =
  ProgMap.fold (fun k p l -> p :: l) !from_prg []

type progress =
    | Remain of int
    | Dependent
    | Defined of global_reference

let obligations_message rem =
  if rem > 0 then
    if rem = 1 then
      Flags.if_verbose msgnl (int rem ++ str " obligation remaining")
    else
      Flags.if_verbose msgnl (int rem ++ str " obligations remaining")
  else
    Flags.if_verbose msgnl (str "No more obligations remaining")

let update_obls prg obls rem =
  let prg' = { prg with prg_obligations = (obls, rem) } in
    progmap_replace prg';
    obligations_message rem;
    if rem > 0 then Remain rem
    else (
      match prg'.prg_deps with
      | [] ->
	  let kn = declare_definition prg' in
	    progmap_remove prg';
	    Defined kn
      | l ->
	  let progs = List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps in
	    if List.for_all (fun x -> obligations_solved x) progs then
	      let kn = declare_mutual_definition progs in
		Defined (ConstRef kn)
	    else Dependent)

let is_defined obls x = obls.(x).obl_body <> None

let deps_remaining obls deps =
  Intset.fold
    (fun x acc ->
      if is_defined obls x then acc
      else x :: acc)
    deps []

let dependencies obls n =
  let res = ref Intset.empty in
    Array.iteri
      (fun i obl ->
	if i <> n && Intset.mem n obl.obl_deps then
	  res := Intset.add i !res)
      obls;
    !res

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

let kind_of_opacity o =
  match o with
  | Define false | Expand -> goal_kind
  | _ -> goal_proof_kind

let not_transp_msg =
  str "Obligation should be transparent but was declared opaque." ++ spc () ++
    str"Use 'Defined' instead."

let warn_not_transp () = ppwarn not_transp_msg
let error_not_transp () = pperror not_transp_msg

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

(* 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 rec solve_obligation prg num tac =
  let user_num = succ num in
  let obls, rem = prg.prg_obligations in
  let obl = obls.(num) in
    if obl.obl_body <> None then
      pperror (str "Obligation" ++ spc () ++ int user_num ++ str "already" ++ spc() ++ str "solved.")
    else
      match deps_remaining obls obl.obl_deps with
      | [] ->
	  let obl = subst_deps_obl obls obl in
	    Lemmas.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
	      (fun strength gr ->
		let cst = match gr with ConstRef cst -> cst | _ -> assert false in
		let obl =
		  let transparent = evaluable_constant cst (Global.env ()) in
		  let body =
		    match obl.obl_status with
		    | Expand ->
			if not transparent then error_not_transp ()
			else constant_value (Global.env ()) cst
		    | Define opaque ->
			if not opaque && not transparent then error_not_transp ()
			else Libnames.constr_of_global gr
		  in
		    if transparent then
		      Auto.add_hints true [string_of_id prg.prg_name]
			(Auto.HintsUnfoldEntry [EvalConstRef cst]);
		    { obl with obl_body = Some body }
		in
		let obls = Array.copy obls in
		let _ = obls.(num) <- obl in
		let res = try update_obls prg obls (pred rem)
		  with e -> pperror (Errors.print (Cerrors.process_vernac_interp_error e))
		in
		  match res with
		  | Remain n when n > 0 ->
		      let deps = dependencies obls num in
			if deps <> Intset.empty then
			  ignore(auto_solve_obligations (Some prg.prg_name) None ~oblset:deps)
		  | _ -> ());
	    trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
		     Printer.pr_constr_env (Global.env ()) obl.obl_type);
	    Pfedit.by (snd (get_default_tactic ()));
	    Option.iter (fun tac -> Pfedit.set_end_tac (Tacinterp.interp tac)) tac;
	    Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
      | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) "
		      ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))

and obligation (user_num, name, typ) tac =
  let num = pred user_num in
  let prg = get_prog_err name in
  let obls, rem = prg.prg_obligations in
    if num < Array.length obls then
      let obl = obls.(num) in
	match obl.obl_body with
	    None -> solve_obligation prg num tac
	  | Some r -> error "Obligation already solved"
    else error (sprintf "Unknown obligation number %i" (succ num))


and solve_obligation_by_tac prg obls i tac =
  let obl = obls.(i) in
    match obl.obl_body with
    | Some _ -> false
    | None ->
	try
	  if deps_remaining obls obl.obl_deps = [] then
	    let obl = subst_deps_obl obls obl in
	    let tac =
	      match tac with
	      | Some t -> t
	      | None ->
		  match obl.obl_tac with
		  | Some t -> t
		  | None -> snd (get_default_tactic ())
	    in
	    let t = solve_by_tac (evar_of_obligation obl) tac in
	      obls.(i) <- declare_obligation prg obl t;
	      true
	  else false
	with
	| Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
	| Loc.Exc_located(_, Refiner.FailError (_, s))
	| Refiner.FailError (_, s) ->
	    user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
	| Errors.Anomaly _ as e -> raise e
	| e -> false

and solve_prg_obligations prg ?oblset tac =
  let obls, rem = prg.prg_obligations in
  let rem = ref rem in
  let obls' = Array.copy obls in
  let p = match oblset with
    | None -> (fun _ -> true)
    | Some s -> (fun i -> Intset.mem i s)
  in
  let _ =
    Array.iteri (fun i x ->
		 if p i && solve_obligation_by_tac prg obls' i tac then
		   decr rem)
      obls'
  in
    update_obls prg obls' !rem

and solve_obligations n tac =
  let prg = get_prog_err n in
    solve_prg_obligations prg tac

and solve_all_obligations tac =
  ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg

and try_solve_obligation n prg tac =
  let prg = get_prog prg in
  let obls, rem = prg.prg_obligations in
  let obls' = Array.copy obls in
    if solve_obligation_by_tac prg obls' n tac then
      ignore(update_obls prg obls' (pred rem));

and try_solve_obligations n tac =
  try ignore (solve_obligations n tac) with NoObligations _ -> ()

and auto_solve_obligations n ?oblset tac : progress =
  Flags.if_verbose msgnl (str "Solving obligations automatically...");
  try solve_prg_obligations (get_prog_err n) ?oblset tac with NoObligations _ -> Dependent

open Pp
let show_obligations_of_prg ?(msg=true) prg =
  let n = prg.prg_name in
  let obls, rem = prg.prg_obligations in
  let showed = ref 5 in
    if msg then msgnl (int rem ++ str " obligation(s) remaining: ");
    Array.iteri (fun i x ->
		   match x.obl_body with
		   | None ->
		       if !showed > 0 then (
			 decr showed;
			 msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
				   str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++
				   hov 1 (Printer.pr_constr_env (Global.env ()) x.obl_type ++ 
					    str "." ++ fnl ())))
		   | Some _ -> ())
      obls

let show_obligations ?(msg=true) n =
  let progs = match n with
    | None -> all_programs ()
    | Some n ->
	try [ProgMap.find n !from_prg]
	with Not_found -> raise (NoObligations (Some n))
  in List.iter (show_obligations_of_prg ~msg) progs

let show_term n =
  let prg = get_prog_err n in
  let n = prg.prg_name in
    msgnl (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++
	     Printer.pr_constr_env (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
	    ++ Printer.pr_constr_env (Global.env ()) prg.prg_body)

let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
    ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
  Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
  let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
  let obls,_ = prg.prg_obligations in
  if Array.length obls = 0 then (
    Flags.if_verbose ppnl (str ".");
    let cst = declare_definition prg in
      Defined cst)
  else (
    let len = Array.length obls in
    let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
      progmap_add n prg;
      let res = auto_solve_obligations (Some n) tactic in
	match res with
	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
	| _ -> res)

let add_mutual_definitions l ?tactic ?(kind=Global,Definition) ?(reduce=reduce)
    ?(hook=fun _ _ -> ()) notations fixkind =
  let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
    List.iter
    (fun  (n, b, t, imps, obls) ->
     let prg = init_prog_info n (Some b) t deps (Some fixkind) 
       notations obls imps kind reduce hook 
     in progmap_add n prg) l;
    let _defined =
      List.fold_left (fun finished x ->
	if finished then finished
	else
	  let res = auto_solve_obligations (Some x) tactic in
	    match res with
	    | Defined _ -> 
		(* If one definition is turned into a constant, 
		   the whole block is defined. *) true
	    | _ -> false)
	false deps
    in ()

let admit_obligations n =
  let prg = get_prog_err n in
  let obls, rem = prg.prg_obligations in
    Array.iteri 
      (fun i x ->
	match x.obl_body with
	| None ->
            let x = subst_deps_obl obls x in
	    let kn = Declare.declare_constant x.obl_name 
              (ParameterEntry (None, x.obl_type,None), IsAssumption Conjectural)
	    in
	      assumption_message x.obl_name;
	      obls.(i) <- { x with obl_body = Some (mkConst kn) }
	| Some _ -> ())
      obls;
    ignore(update_obls prg obls 0)

exception Found of int

let array_find f arr =
  try Array.iteri (fun i x -> if f x then raise (Found i)) arr;
    raise Not_found
  with Found i -> i

let next_obligation n tac =
  let prg = get_prog_err n in
  let obls, rem = prg.prg_obligations in
  let i =
    try array_find (fun x ->  x.obl_body = None && deps_remaining obls x.obl_deps = []) obls
    with Not_found -> anomaly "Could not find a solvable obligation."
  in solve_obligation prg i tac


let init_program () =
  Coqlib.check_required_library ["Coq";"Init";"Datatypes"];
  Coqlib.check_required_library ["Coq";"Init";"Specif"];
  Coqlib.check_required_library ["Coq";"Program";"Tactics"]


let set_program_mode c =
  if c then
    if !Flags.program_mode then ()
    else begin
      init_program ();
      Flags.program_mode := true;
    end