(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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 Ltac_plugin
open Util
open Pp
open Constrexpr
open Indfun_common
open Indfun
open Stdarg
open Tacarg
open Extraargs
open Tactypes
open Pcoq.Prim
open Pcoq.Constr
open Pltac

}

DECLARE PLUGIN "coq-core.plugins.funind"

{

let pr_fun_ind_using env sigma prc prlc _ opt_c =
  match opt_c with
    | None -> mt ()
    | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings (prc env sigma) (prlc env sigma) b)

(* Duplication of printing functions because "'a with_bindings" is
   (internally) not uniform in 'a: indeed constr_with_bindings at the
   "typed" level has type "open_constr with_bindings" instead of
   "constr with_bindings"; hence, its printer cannot be polymorphic in
   (prc,prlc)... *)

let pr_fun_ind_using_typed prc prlc _ opt_c =
  match opt_c with
    | None -> mt ()
    | Some b ->
      let env = Global.env () in
      let evd = Evd.from_env env in
      let (_, b) = b env evd in
      spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings (prc env evd) (prlc env evd) b)

}

ARGUMENT EXTEND fun_ind_using
  TYPED AS constr_with_bindings option
  PRINTED BY { pr_fun_ind_using_typed }
  RAW_PRINTED BY { pr_fun_ind_using env sigma }
  GLOB_PRINTED BY { pr_fun_ind_using env sigma }
| [ "using" constr_with_bindings(c) ] -> { Some c }
| [ ] -> { None }
END


TACTIC EXTEND newfuninv
| [ "functional" "inversion"  quantified_hypothesis(hyp) reference_opt(fname) ] ->
     {
       Invfun.invfun hyp fname
     }
END

{

let pr_intro_as_pat prc pat =
  match pat with
    | Some pat ->
      str "as" ++ spc () ++ Miscprint.pr_intro_pattern prc pat
    | None -> mt ()

let out_disjunctive = CAst.map (function
  | IntroAction (IntroOrAndPattern l) -> l
  | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected."))

}

ARGUMENT EXTEND with_names TYPED AS intro_pattern option
  PRINTED BY { fun prc _ _ -> pr_intro_as_pat (fun c -> prc env sigma @@ snd @@ c env sigma) }
  RAW_PRINTED BY { fun prc _ _ -> pr_intro_as_pat (prc env sigma) }
  GLOB_PRINTED BY { fun prc _ _ -> pr_intro_as_pat (prc env sigma) }
| [ "as"  simple_intropattern(ipat) ] -> { Some ipat }
| []  -> { None }
END

{

let functional_induction b c x pat =
  functional_induction true c x (Option.map out_disjunctive pat)

}

TACTIC EXTEND newfunind
| ["functional" "induction" lconstr(c) fun_ind_using(princl) with_names(pat)] ->
   {
     (Ltac_plugin.Internals.onSomeWithHoles
          (fun x -> functional_induction true c x pat) princl)
   }

END
(***** debug only ***)
TACTIC EXTEND snewfunind
| ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
     {
       let c = match cl with
         | [] -> assert false
         | [c] -> c
         | c::cl -> EConstr.applist(c,cl)
       in
       Ltac_plugin.Internals.onSomeWithHoles (fun x -> functional_induction false c x pat) princl }
END

{

let pr_constr_comma_sequence env sigma prc _ _ = prlist_with_sep pr_comma (prc env sigma)

}

ARGUMENT EXTEND constr_comma_sequence'
  TYPED AS constr list
  PRINTED BY { pr_constr_comma_sequence env sigma }
| [ constr(c) "," constr_comma_sequence'(l) ] -> { c::l }
| [ constr(c) ] -> { [c] }
END

{

let pr_auto_using env sigma prc _prlc _prt = Pptactic.pr_auto_using (prc env sigma)

}

ARGUMENT EXTEND auto_using'
  TYPED AS constr list
  PRINTED BY { pr_auto_using env sigma }
| [ "using" constr_comma_sequence'(l) ] -> { l }
| [ ] -> { [] }
END

{

module Vernac = Pvernac.Vernac_

let (wit_function_fix_definition : Vernacexpr.fixpoint_expr Loc.located Genarg.uniform_genarg_type) =
  Genarg.create_arg "function_fix_definition"

let function_fix_definition =
  Pcoq.create_generic_entry2 "function_fix_definition" (Genarg.rawwit wit_function_fix_definition)

}

GRAMMAR EXTEND Gram
  GLOBAL: function_fix_definition ;

  function_fix_definition:
    [ [ g = Vernac.fix_definition -> { Loc.tag ~loc g } ]]
    ;

END

{

let () =
  let raw_printer env sigma _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
  Pptactic.declare_extra_vernac_genarg_pprule wit_function_fix_definition raw_printer

let is_proof_termination_interactively_checked recsl =
  List.exists (function
  | _,( Vernacexpr.{ rec_order = Some { CAst.v = CMeasureRec _ } }
      | Vernacexpr.{ rec_order = Some { CAst.v = CWfRec _} }) -> true
  | _, Vernacexpr.{ rec_order = Some { CAst.v = CStructRec _ } }
  | _, Vernacexpr.{ rec_order = None } -> false) recsl

let classify_as_Fixpoint recsl =
 Vernac_classifier.classify_vernac
    (Vernacexpr.(CAst.make @@ { control = []; attrs = []; expr = VernacSynPure (VernacFixpoint(NoDischarge, List.map snd recsl))}))

let classify_funind recsl =
  match classify_as_Fixpoint recsl with
  | Vernacextend.VtSideff (ids, _)
    when is_proof_termination_interactively_checked recsl ->
      Vernacextend.(VtStartProof (GuaranteesOpacity, ids))
  | x -> x

let is_interactive recsl =
  match classify_funind recsl with
  | Vernacextend.VtStartProof _ -> true
  | _ -> false

}

(* For usability we temporarily switch off some flags during the call
   to Function. However this is not satisfactory:

 1- Function should not warn "non-recursive" and call the Definition
    mechanism instead of Fixpoint when needed

 2- Only for automatically generated names should
    unused-pattern-matching-variable be ignored. *)

VERNAC COMMAND EXTEND Function STATE CUSTOM
| ["Function" ne_function_fix_definition_list_sep(recsl,"with")]
    => { classify_funind recsl }
    -> {
    let warn = "-unused-pattern-matching-variable,-non-recursive" in
    if is_interactive recsl then
      Vernactypes.vtopenproof (fun () ->
          CWarnings.with_warn warn
            Gen_principle.do_generate_principle_interactive (List.map snd recsl))
    else
      Vernactypes.vtdefault (fun () ->
          CWarnings.with_warn warn
            Gen_principle.do_generate_principle (List.map snd recsl))
  }
END

{

let pr_fun_scheme_arg (princ_name,fun_name,s) =
  Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
  Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++
  Sorts.pr_sort_family s

}

VERNAC ARGUMENT EXTEND fun_scheme_arg
PRINTED BY { pr_fun_scheme_arg }
| [ identref(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort_family(s) ] -> { (princ_name.CAst.v,fun_name,s) }
END

{

let warning_error names e =
  match e with
  | Building_graph e ->
    let names = pr_enum Libnames.pr_qualid names in
    let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in
    Gen_principle.warn_cannot_define_graph (names,error)
  | Defining_principle e ->
    let names = pr_enum Libnames.pr_qualid names in
    let error = if do_observe () then CErrors.print e else mt () in
    Gen_principle.warn_cannot_define_principle (names,error)
  | _ -> raise e

}

VERNAC COMMAND EXTEND NewFunctionalScheme
| ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
   => { Vernacextend.(VtSideff(List.map pi1 fas, VtLater)) }
   ->
    { begin
        try
          Gen_principle.build_scheme fas
        with
        | Gen_principle.No_graph_found ->
          begin
            match fas with
            | (_,fun_name,_)::_ ->
              begin
                Gen_principle.make_graph (Smartlocate.global_with_alias fun_name);
                try Gen_principle.build_scheme fas
                with
                | Gen_principle.No_graph_found ->
                  CErrors.user_err Pp.(str "Cannot generate induction principle(s)")
                | e when CErrors.noncritical e ->
                  let names = List.map (fun (_,na,_) -> na) fas in
                  warning_error names e
              end
              | _ -> assert false (* we can only have non empty  list *)
          end
        | e when CErrors.noncritical e ->
          let names = List.map (fun (_,na,_) -> na) fas in
          warning_error names e
      end
    }
END
(***** debug only ***)

VERNAC COMMAND EXTEND NewFunctionalCase
| ["Functional" "Case" fun_scheme_arg(fas) ]
  => { Vernacextend.(VtSideff([pi1 fas], VtLater)) }
  -> { Gen_principle.build_case_scheme fas }
END

(***** debug only ***)
VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
| ["Generate" "graph" "for" reference(c)] ->
  { Gen_principle.make_graph (Smartlocate.global_with_alias c) }
END