(************************************************************************)
(*         *      The Rocq Prover / The Rocq 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)         *)
(************************************************************************)

(*
  Syntax for the subtac terms and types.
  Elaborated from correctness/psyntax.ml4 by Jean-Christophe FilliÃ¢tre *)

DECLARE PLUGIN "coq-core.plugins.ltac"

{

open Stdarg
open Tacarg

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

let () =
  (* Delay to recover the tactic imperatively *)
  let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
      get_default_tactic ()
    end
  in
  Declare.Obls.default_tactic := tac

let with_tac f tac =
  let env = Genintern.empty_glob_sign ~strict:true (Global.env ()) in
  let tac = match tac with
  | None -> None
  | Some tac ->
    let tac = Genarg.in_gen (Genarg.rawwit wit_ltac) tac in
    let _, tac = Genintern.generic_intern env tac in
    Some tac
  in
  f tac

(* We define new entries for programs, with the use of this module
 * Subtac. These entries are named Subtac.<foo>
 *)

let pr_withtac env sigma = function
  | None -> Pp.mt ()
  | Some tac -> Pp.(str "with" ++ spc () ++ Pptactic.pr_raw_tactic env sigma tac)

let tactic = Pltac.tactic

}

VERNAC ARGUMENT EXTEND withtac PRINTED BY { pr_withtac env sigma }
| [ ] -> { None }
| [ "with" tactic(tac) ] -> { Some tac }
END

{

open Declare.Obls

let obligation ~pm obl tac = with_tac (fun t -> obligation ~pm obl t) tac
let next_obligation ~pm ?final obl tac = with_tac (fun t -> next_obligation ~pm ?final obl t) tac

let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))

}

VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_program
| [ "Obligation" natural(num) "of" identref(name) withtac(tac) ] ->
    { obligation (num, Some name.CAst.v) tac }
| [ "Obligation" natural(num) withtac(tac) ] ->
    { obligation (num, None) tac }
| [ "Next" "Obligation" "of" identref(name) withtac(tac) ] ->
    { next_obligation (Some name.CAst.v) tac }
| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
| [ "Final" "Obligation" "of" identref(name) withtac(tac) ] ->
    { next_obligation ~final:true (Some name.CAst.v) tac }
| [ "Final" "Obligation" withtac(tac) ] -> { next_obligation ~final:true None tac }
END

VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Solve" "Obligations" "of" identref(name) "with" tactic(t) ] ->
    { try_solve_obligations (Some name.CAst.v) (Some (Tacinterp.interp t)) }
| [ "Solve" "Obligations" "of" identref(name) ] ->
    { try_solve_obligations (Some name.CAst.v) None }
| [ "Solve" "Obligations" "with" tactic(t) ] ->
    { try_solve_obligations None (Some (Tacinterp.interp t)) }
| [ "Solve" "Obligations" ] ->
    { try_solve_obligations None None }
END

VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Solve" "All" "Obligations" "with" tactic(t) ] ->
    { solve_all_obligations (Some (Tacinterp.interp t)) }
| [ "Solve" "All" "Obligations" ] ->
    { solve_all_obligations None }
END

VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Admit" "Obligations" "of" identref(name) ] -> { admit_obligations (Some name.CAst.v) }
| [ "Admit" "Obligations" ] -> { admit_obligations None }
END

VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF
| #[ locality = Tactic_option.tac_option_locality; ] [ "Obligation" "Tactic" ":=" tactic(t) ] -> {
        set_default_tactic
          locality
          (Tacintern.glob_tactic t);
  }
END

{

open Pp

}

VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
| [ "Show" "Obligation" "Tactic" ] -> {
    Feedback.msg_notice (str"Program obligation tactic is " ++ print_default_tactic ()) }
END

VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY STATE read_program
| [ "Obligations" "of" identref(name) ] -> { fun ~pm -> show_obligations ~pm (Some name.CAst.v) }
| [ "Obligations" ] -> { fun ~pm -> show_obligations ~pm None }
END

VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY STATE read_program
| [ "Preterm" "of" identref(name) ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm (Some name.CAst.v)) }
| [ "Preterm" ] -> { fun ~pm -> Feedback.msg_notice (show_term ~pm None) }
END
