|
|
|
|
Quelle g_obligations.mlg
Sprache: unbekannt
|
|
|
(************************************************************************)
(* * 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 GLOBAL PLUGIN
{
open Stdarg
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 tac = Option.map (fun tac -> Gentactic.intern (Global.env()) tac) tac in
f tac
let interp_gen tac =
Proofview.Goal.enter begin fun gl ->
let tac = Gentactic.intern ~strict:false (Proofview.Goal.env gl) tac in
Gentactic.interp tac
end
(* We define new entries for programs, with the use of this module
* Subtac. These entries are named Subtac.<foo>
*)
let pr_withtac env sigma = let open Pp in function
| None -> mt ()
| Some tac -> str "with" ++ spc () ++ Gentactic.print_raw env sigma tac
let generic_tactic = Pvernac.Vernac_.generic_tactic
}
VERNAC ARGUMENT EXTEND withtac PRINTED BY { pr_withtac env sigma }
| [ ] -> { None }
| [ "with" generic_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) withtac(t) ] ->
{ try_solve_obligations (Some name.CAst.v) (Option.map interp_gen t) }
| [ "Solve" "Obligations" withtac(t) ] ->
{ try_solve_obligations None (Option.map interp_gen t) }
END
VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF STATE program
| [ "Solve" "All" "Obligations" withtac(t) ] ->
{ solve_all_obligations (Option.map interp_gen t) }
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" ":=" generic_tactic(t) ] -> {
set_default_tactic
locality
(Gentactic.intern (Global.env()) t);
}
END
VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY
| [ "Show" "Obligation" "Tactic" ] -> {
Feedback.msg_notice Pp.(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
[ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
]
|
2026-03-28
|
|
|
|
|
