Quelle g_proofs.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)         *)
(************************************************************************)

DECLARE GLOBAL PLUGIN

{

open Vernacexpr
open Hints

open Procq
open Procq.Prim
open Procq.Constr
open Pvernac.Vernac_

let thm_token = G_vernac.thm_token

let hint = Entry.make "hint"

let warn_deprecated_focus =
  CWarnings.create ~name:"deprecated-focus" ~category:Deprecation.Version.v8_8
    Pp.(function
      | None ->
        strbrk "The Focus command is deprecated; use bullets or focusing brackets instead."
      | Some n ->
        str "The Focus command is deprecated;" ++ spc ()
        ++ str "use '" ++ int n ++ str ": {' instead.")

let warn_deprecated_focus_n ?loc n = warn_deprecated_focus ?loc (Some n)

let warn_deprecated_focus ?loc () = warn_deprecated_focus ?loc None

let warn_deprecated_unfocus =
  CWarnings.create ~name:"deprecated-unfocus" ~category:Deprecation.Version.v8_8
         (fun () -> Pp.strbrk "The Unfocus command is deprecated")

}

(* Proof commands *)
GRAMMAR EXTEND Gram
  GLOBAL: hint command;

  opt_hintbases:
  [ [ -> { [] }
    | ":"; l = LIST1 [id = IDENT -> { id } ] -> { l } ] ]
  ;
  command: TOP
    [ [ IDENT "Goal"; c = lconstr ->
        { VernacSynPure (VernacDefinition (Decls.(NoDischarge, Definition), ((CAst.make ~loc Names.Anonymous), None), ProveBody ([], c))) }
      | IDENT "Proof" -> { VernacSynPure (VernacProof (None,None)) }
      | IDENT "Proof"; IDENT "using"; l = G_vernac.section_subset_expr ->
        { VernacSynPure (VernacProof (None,Some l)) }
      | IDENT "Proof"; "with"; ta = generic_tactic;
        l = OPT [ IDENT "using"; l = G_vernac.section_subset_expr -> { l } ] ->
          { Vernacexpr.VernacSynPure (Vernacexpr.VernacProof (Some ta, l)) }
      | IDENT "Proof"; IDENT "using"; l = G_vernac.section_subset_expr;
        "with"; ta = generic_tactic ->
          { Vernacexpr.VernacSynPure (Vernacexpr.VernacProof (Some ta,Some l)) }
      | IDENT "Proof" ; IDENT "Mode" ; mn = string -> { VernacSynterp (VernacProofMode mn) }
      | IDENT "Proof"; c = lconstr -> { VernacSynPure (VernacExactProof c) }
      | IDENT "Abort" -> { VernacSynPure VernacAbort }
      | IDENT "Abort"; IDENT "All" -> { VernacSynPure VernacAbortAll }
      | IDENT "Admitted" -> { VernacSynPure (VernacEndProof Admitted) }
      | IDENT "Qed" -> { VernacSynPure (VernacEndProof (Proved (Opaque,None))) }
      | IDENT "Save"; id = identref ->
          { VernacSynPure (VernacEndProof (Proved (Opaque, Some id))) }
      | IDENT "Defined" -> { VernacSynPure (VernacEndProof (Proved (Transparent,None))) }
      | IDENT "Defined"; id=identref ->
          { VernacSynPure (VernacEndProof (Proved (Transparent,Some id))) }
      | IDENT "Restart" -> { VernacSynPure VernacRestart }
      | IDENT "Undo" -> { VernacSynPure (VernacUndo 1) }
      | IDENT "Undo"; n = natural -> { VernacSynPure (VernacUndo n) }
      | IDENT "Undo"; IDENT "To"; n = natural -> { VernacSynPure (VernacUndoTo n) }
      | IDENT "Focus" ->
         { warn_deprecated_focus ~loc ();
         VernacSynPure (VernacFocus None) }
      | IDENT "Focus"; n = natural ->
         { warn_deprecated_focus_n n ~loc;
         VernacSynPure (VernacFocus (Some n)) }
      | IDENT "Unfocus" ->
         { warn_deprecated_unfocus ~loc ();
         VernacSynPure VernacUnfocus }
      | IDENT "Unfocused" -> { VernacSynPure VernacUnfocused }
      | IDENT "Show" -> { VernacSynPure (VernacShow (ShowGoal OpenSubgoals)) }
      | IDENT "Show"; n = natural -> { VernacSynPure (VernacShow (ShowGoal (NthGoal n))) }
      | IDENT "Show"; id = ident -> { VernacSynPure (VernacShow (ShowGoal (GoalId id))) }
      | IDENT "Show"; IDENT "Existentials" -> { VernacSynPure (VernacShow ShowExistentials) }
      | IDENT "Show"; IDENT "Universes" -> { VernacSynPure (VernacShow ShowUniverses) }
      | IDENT "Show"; IDENT "Conjectures" -> { VernacSynPure (VernacShow ShowProofNames) }
      | IDENT "Show"; IDENT "Proof" -> { VernacSynPure (VernacShow ShowProof) }
      | IDENT "Show"; IDENT "Intro" -> { VernacSynPure (VernacShow (ShowIntros false)) }
      | IDENT "Show"; IDENT "Intros" -> { VernacSynPure (VernacShow (ShowIntros true)) }
      | IDENT "Show"; IDENT "Match"; id = reference -> { VernacSynPure (VernacShow (ShowMatch id)) }
      | IDENT "Guarded" -> { VernacSynPure VernacCheckGuard }
      | IDENT "Validate"; IDENT "Proof" -> { VernacSynPure VernacValidateProof }
      (* Hints for Auto and EAuto *)
      | IDENT "Create"; IDENT "HintDb" ;
          id = IDENT ; b = [ IDENT "discriminated" -> { true } | -> { false } ] ->
            { VernacSynPure (VernacCreateHintDb (id, b)) }
      | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases ->
          { VernacSynPure (VernacRemoveHints (dbnames, ids)) }
      | IDENT "Hint"; h = hint; dbnames = opt_hintbases ->
          { VernacSynPure (VernacHints (dbnames, h)) }
      ] ];
  reference_or_constr:
   [ [ r = global -> { HintsReference r }
     | c = constr -> { HintsConstr c } ] ]
  ;
  hint:
    [ [ IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info ->
          { HintsResolve (List.map (fun x -> (info, true, x)) lc) }
      | IDENT "Resolve"; "->"; lc = LIST1 global; n = OPT natural ->
          { HintsResolveIFF (true, lc, n) }
      | IDENT "Resolve"; "<-"; lc = LIST1 global; n = OPT natural ->
          { HintsResolveIFF (false, lc, n) }
      | IDENT "Immediate"; lc = LIST1 reference_or_constr -> { HintsImmediate lc }
      | IDENT "Variables"; IDENT "Transparent" -> { HintsTransparency (HintsVariables, true) }
      | IDENT "Variables"; IDENT "Opaque" -> { HintsTransparency (HintsVariables, false) }
      | IDENT "Constants"; IDENT "Transparent" -> { HintsTransparency (HintsConstants, true) }
      | IDENT "Constants"; IDENT "Opaque" -> { HintsTransparency (HintsConstants, false) }
      | IDENT "Projections"; IDENT "Transparent" -> { HintsTransparency (HintsProjections, true) }
      | IDENT "Projections"; IDENT "Opaque" -> { HintsTransparency (HintsProjections, false) }
      | IDENT "Transparent"; lc = LIST1 global -> { HintsTransparency (HintsReferences lc, true) }
      | IDENT "Opaque"; lc = LIST1 global -> { HintsTransparency (HintsReferences lc, false) }
      | IDENT "Mode"; l = global; m = mode -> { HintsMode (l, m) }
      | IDENT "Unfold"; lqid = LIST1 global -> { HintsUnfold lqid }
      | IDENT "Constructors"; lc = LIST1 global -> { HintsConstructors lc }
      | IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
        tac = generic_tactic ->
        { Vernacexpr.HintsExtern (n,c, tac) }
  ] ]
    ;
  mode:
    [ [ l = LIST1 [ "+" -> { ModeInput }
                  | "!" -> { ModeNoHeadEvar }
                  | "-" -> { ModeOutput } ] -> { l } ] ]
  ;
END

Quelle g_proofs.mlg Sprache: unbekannt

[ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ]