(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Util
open Names
open Constr
open EConstr
open Tacmach.New
open Tactics
open Tacticals.New

open Indfun_common

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

(* [revert_graph kn post_tac hid] transforme an hypothesis [hid] having type Ind(kn,num) t1 ... tn res
   when [kn] denotes a graph block  into
   f_num t1... tn = res (by applying [f_complete] to the first type) before apply post_tac on the result

   if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing
*)
let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl ->
  let sigma = project gl in
  let typ = pf_unsafe_type_of gl (mkVar hid) in
  match EConstr.kind sigma typ with
  | App(i,args) when isInd sigma i ->
    let ((kn',num) as ind'),u = destInd sigma i in
    if MutInd.equal kn kn'
    then (* We have generated a graph hypothesis so that we must change it if we can *)
      let info = match find_Function_of_graph ind' with
        | Some info -> info
        | None ->
          (* The graphs are mutually recursive but we cannot find one of them !*)
          CErrors.anomaly (Pp.str "Cannot retrieve infos about a mutual block.")
      in
      (* if we can find a completeness lemma for this function
         then we can come back to the functional form. If not, we do nothing
      *)
      match info.completeness_lemma with
      | None -> tclIDTAC
      | Some f_complete ->
        let f_args,res = Array.chop (Array.length args - 1) args in
        tclTHENLIST
          [ generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]
          ; clear [hid]
          ; Simple.intro hid
          ; post_tac hid
          ]
    else tclIDTAC
  | _ -> tclIDTAC
  )

(*
   [functional_inversion hid fconst f_correct ] is the functional version of [inversion]

   [hid] is the hypothesis to invert, [fconst] is the function to invert and  [f_correct]
   is the correctness lemma for [fconst].

   The sketch is the following~:
   \begin{enumerate}
   \item Transforms the hypothesis [hid] such that its type is now $res\ =\ f\ t_1 \ldots t_n$
   (fails if it is not possible)
   \item replace [hid] with $R\_f t_1 \ldots t_n res$ using [f_correct]
   \item apply [inversion] on [hid]
   \item finally in each branch, replace each  hypothesis [R\_f ..]  by [f ...] using [f_complete] (whenever
   such a lemma exists)
   \end{enumerate}
*)

let functional_inversion kn hid fconst f_correct = Proofview.Goal.enter (fun gl ->
  let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps gl) Id.Set.empty in
  let sigma = project gl in
  let type_of_h = pf_unsafe_type_of gl (mkVar hid) in
  match EConstr.kind sigma type_of_h with
  | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ())  ->
    let pre_tac,f_args,res =
      match EConstr.kind sigma args.(1),EConstr.kind sigma args.(2) with
      | App(f,f_args),_ when EConstr.eq_constr sigma f fconst ->
        ((fun hid -> intros_symmetry (Locusops.onHyp hid))),f_args,args.(2)
      |_,App(f,f_args) when EConstr.eq_constr sigma f fconst ->
        ((fun hid -> tclIDTAC),f_args,args.(1))
      | _ -> (fun hid -> tclFAIL 1 Pp.(mt ())),[||],args.(2)
    in
    tclTHENLIST
      [ pre_tac hid
      ; generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]
      ; clear [hid]
      ; Simple.intro hid
      ; Inv.inv Inv.FullInversion None (Tactypes.NamedHyp hid)
      ; Proofview.Goal.enter (fun gl ->
            let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps gl) in
            tclMAP (revert_graph kn pre_tac)  (hid::new_ids)
          )
      ]
  | _ -> tclFAIL 1 Pp.(mt ())
  )

let invfun qhyp f  =
  let f =
    match f with
    | GlobRef.ConstRef f -> f
    | _ ->
      CErrors.user_err Pp.(str "Not a function")
  in
  match find_Function_infos f with
  | None ->
    CErrors.user_err (Pp.str "No graph found")
  | Some finfos ->
    match finfos.correctness_lemma with
    | None ->
      CErrors.user_err (Pp.str "Cannot use equivalence with graph!")
    | Some f_correct ->
      let f_correct = mkConst f_correct
      and kn = fst finfos.graph_ind in
      Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f)  f_correct) qhyp

let invfun qhyp f =
  let exception NoFunction in
  match f with
  | Some f -> invfun qhyp f
  | None ->
    let tac_action hid gl =
      let sigma = project gl in
      let hyp_typ = pf_unsafe_type_of gl (mkVar hid)  in
      match EConstr.kind sigma hyp_typ with
      | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
        begin
          let f1,_ = decompose_app sigma args.(1) in
          try
            if not (isConst sigma f1) then raise NoFunction;
            let finfos = Option.get (find_Function_infos (fst (destConst sigma f1))) in
            let f_correct = mkConst(Option.get finfos.correctness_lemma)
            and kn = fst finfos.graph_ind
            in
            functional_inversion kn hid f1 f_correct
          with
          | NoFunction | Option.IsNone ->
            let f2,_ = decompose_app sigma args.(2) in
            if isConst sigma f2 then
              match find_Function_infos (fst (destConst sigma f2)) with
              | None ->
                if do_observe ()
                then CErrors.user_err (Pp.str "No graph found for any side of equality")
                else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
              | Some finfos ->
                match finfos.correctness_lemma with
                | None ->
                  if do_observe ()
                  then CErrors.user_err (Pp.str "Cannot use equivalence with graph for any side of the equality")
                  else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
                | Some f_correct ->
                  let f_correct = mkConst f_correct
                  and kn = fst finfos.graph_ind
                  in
                  functional_inversion kn hid  f2 f_correct
            else                (* NoFunction *)
              CErrors.user_err Pp.(str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
        end
      | _ -> CErrors.user_err Pp.(Ppconstr.pr_id hid ++ str " must be an equality ")
    in
    try_intros_until (tac_action %> Proofview.Goal.enter) qhyp