parsing/g_proofs.ml4

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106

(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Constrexpr
open Vernacexpr
open Misctypes

open Pcoq
open Pcoq.Prim
open Pcoq.Constr
open Pcoq.Vernac_

let thm_token = G_vernac.thm_token

let hint = Gram.entry_create "hint"

(* Proof commands *)
GEXTEND Gram
  GLOBAL: hint command;

  opt_hintbases:
  [ [ -> []
    | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ]
  ;
  command:
    [ [ IDENT "Goal"; c = lconstr -> VernacGoal c
      | IDENT "Proof" -> VernacProof (None,None)
      | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn
      | IDENT "Proof"; c = lconstr -> VernacExactProof c
      | IDENT "Abort" -> VernacAbort None
      | IDENT "Abort"; IDENT "All" -> VernacAbortAll
      | IDENT "Abort"; id = identref -> VernacAbort (Some id)
      | IDENT "Existential"; n = natural; c = constr_body ->
          VernacSolveExistential (n,c)
      | IDENT "Admitted" -> VernacEndProof Admitted
      | IDENT "Qed" -> VernacEndProof (Proved (Opaque,None))
      | IDENT "Save"; id = identref ->
          VernacEndProof (Proved (Opaque, Some id))
      | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None))
      |        IDENT "Defined"; id=identref ->
          VernacEndProof (Proved (Transparent,Some id))
      | IDENT "Restart" -> VernacRestart
      | IDENT "Undo" -> VernacUndo 1
      | IDENT "Undo"; n = natural -> VernacUndo n
      | IDENT "Undo"; IDENT "To"; n = natural -> VernacUndoTo n
      | IDENT "Focus" -> VernacFocus None
      | IDENT "Focus"; n = natural -> VernacFocus (Some n)
      | IDENT "Unfocus" -> VernacUnfocus
      | IDENT "Unfocused" -> VernacUnfocused
      | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals)
      | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n))
      | IDENT "Show"; id = ident -> VernacShow (ShowGoal (GoalId id))
      | IDENT "Show"; IDENT "Script" -> VernacShow ShowScript
      | IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials
      | IDENT "Show"; IDENT "Universes" -> VernacShow ShowUniverses
      | IDENT "Show"; IDENT "Conjectures" -> VernacShow ShowProofNames
      | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof
      | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false)
      | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true)
      | IDENT "Show"; IDENT "Match"; id = reference -> VernacShow (ShowMatch id)
      | IDENT "Guarded" -> VernacCheckGuard
      (* Hints for Auto and EAuto *)
      | IDENT "Create"; IDENT "HintDb" ;
          id = IDENT ; b = [ "discriminated" -> true | -> false ] ->
            VernacCreateHintDb (id, b)
      | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases ->
          VernacRemoveHints (dbnames, ids)
      | IDENT "Hint"; h = hint;
          dbnames = opt_hintbases ->
          VernacHints (dbnames, h)
      (* Declare "Resolve" explicitly so as to be able to later extend with
         "Resolve ->" and "Resolve <-" *)
      | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; 
        info = hint_info; dbnames = opt_hintbases ->
          VernacHints (dbnames,
            HintsResolve (List.map (fun x -> (info, true, x)) lc))
      ] ];
  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 "Immediate"; lc = LIST1 reference_or_constr -> HintsImmediate lc
      | IDENT "Transparent"; lc = LIST1 global -> HintsTransparency (lc, true)
      | IDENT "Opaque"; lc = LIST1 global -> HintsTransparency (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 ] ]
    ;
  constr_body:
    [ [ ":="; c = lconstr -> c
      | ":"; t = lconstr; ":="; c = lconstr -> CAst.make ~loc:!@loc @@ CCast(c,CastConv t) ] ]
  ;
  mode:
    [ [ l = LIST1 [ "+" -> ModeInput
                  | "!" -> ModeNoHeadEvar
                  | "-" -> ModeOutput ] -> l ] ]
  ;
END