package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

doc/src/rocq-runtime.toplevel/g_toplevel.ml.html

Source file g_toplevel.ml

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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146

# 13 "toplevel/g_toplevel.mlg"
 
open Procq
open Procq.Prim
open Vernacexpr

(* Vernaculars specific to the toplevel *)
type vernac_toplevel =
  | VernacBackTo of int
  | VernacDrop
  | VernacQuit
  | VernacControl of vernac_control
  | VernacShowGoal of { gid : int; sid: int }
  | VernacShowProofDiffs of Proof_diffs.diffOpt

let vernac_toplevel = Entry.make "toplevel:vernac_toplevel"

let err () = raise Gramlib.Stream.Failure

let test_show_goal =
  let open Procq.Lookahead in
  to_entry "test_show_goal" begin
   lk_kw "Show" >> lk_kw "Goal" >> lk_nat
  end


# 29 "toplevel/g_toplevel.ml"

let _ = let () =
  Procq.grammar_extend vernac_toplevel
  (Procq.Fresh
  (Gramlib.Gramext.First, [(None, None,
                           [Procq.Production.make
                            (Procq.Rule.next (Procq.Rule.stop)
                             ((Procq.Symbol.nterm Pvernac.Vernac_.main_entry)))
                            (fun cmd loc -> 
# 53 "toplevel/g_toplevel.mlg"
                match cmd with
              | None -> None
              | Some v -> Some (VernacControl v) 
# 43 "toplevel/g_toplevel.ml"
);
                           Procq.Production.make
                           (Procq.Rule.next
                            (Procq.Rule.next
                             (Procq.Rule.next
                              (Procq.Rule.next
                               (Procq.Rule.next (Procq.Rule.stop)
                                ((Procq.Symbol.token (Tok.PIDENT (Some
                                ("Show"))))))
                               ((Procq.Symbol.token (Tok.PIDENT (Some
                               ("Proof"))))))
                              ((Procq.Symbol.token (Tok.PIDENT (Some
                              ("Diffs"))))))
                             ((Procq.Symbol.opt (Procq.Symbol.rules [Procq.Rules.make 
                                                                    (
                                                                    Procq.Rule.next_norec
                                                                    (Procq.Rule.stop)
                                                                    ((Procq.Symbol.token (Tok.PIDENT (Some
                                                                    ("removed"))))))
                                                                    (fun _
                                                                    loc -> 
                                                                    
# 49 "toplevel/g_toplevel.mlg"
                                                                                         () 
# 68 "toplevel/g_toplevel.ml"
)]))))
                            ((Procq.Symbol.token (Tok.PKEYWORD (".")))))
                           (fun _ removed _ _ _ loc -> 
# 50 "toplevel/g_toplevel.mlg"
          Some (VernacShowProofDiffs
          (if removed = None then Proof_diffs.DiffOn else Proof_diffs.DiffRemoved)) 
# 75 "toplevel/g_toplevel.ml"
);
                           Procq.Production.make
                           (Procq.Rule.next
                            (Procq.Rule.next
                             (Procq.Rule.next
                              (Procq.Rule.next
                               (Procq.Rule.next
                                (Procq.Rule.next
                                 (Procq.Rule.next (Procq.Rule.stop)
                                  ((Procq.Symbol.nterm test_show_goal)))
                                 ((Procq.Symbol.token (Tok.PIDENT (Some
                                 ("Show"))))))
                                ((Procq.Symbol.token (Tok.PIDENT (Some
                                ("Goal"))))))
                               ((Procq.Symbol.nterm natural)))
                              ((Procq.Symbol.token (Tok.PIDENT (Some
                              ("at"))))))
                             ((Procq.Symbol.nterm natural)))
                            ((Procq.Symbol.token (Tok.PKEYWORD (".")))))
                           (fun _ sid _ gid _ _ _ loc -> 
# 48 "toplevel/g_toplevel.mlg"
            Some (VernacShowGoal {gid; sid}) 
# 98 "toplevel/g_toplevel.ml"
);
                           Procq.Production.make
                           (Procq.Rule.next
                            (Procq.Rule.next
                             (Procq.Rule.next (Procq.Rule.stop)
                              ((Procq.Symbol.token (Tok.PIDENT (Some
                              ("BackTo"))))))
                             ((Procq.Symbol.nterm natural)))
                            ((Procq.Symbol.token (Tok.PKEYWORD (".")))))
                           (fun _ n _ loc -> 
# 45 "toplevel/g_toplevel.mlg"
          Some (VernacBackTo n) 
# 111 "toplevel/g_toplevel.ml"
);
                           Procq.Production.make
                           (Procq.Rule.next
                            (Procq.Rule.next (Procq.Rule.stop)
                             ((Procq.Symbol.token (Tok.PIDENT (Some
                             ("Quit"))))))
                            ((Procq.Symbol.token (Tok.PKEYWORD (".")))))
                           (fun _ _ loc -> 
# 43 "toplevel/g_toplevel.mlg"
                               Some VernacQuit 
# 122 "toplevel/g_toplevel.ml"
);
                           Procq.Production.make
                           (Procq.Rule.next
                            (Procq.Rule.next (Procq.Rule.stop)
                             ((Procq.Symbol.token (Tok.PIDENT (Some
                             ("Drop"))))))
                            ((Procq.Symbol.token (Tok.PKEYWORD (".")))))
                           (fun _ _ loc -> 
# 42 "toplevel/g_toplevel.mlg"
                               Some VernacDrop 
# 133 "toplevel/g_toplevel.ml"
)])]))
  in ()


# 61 "toplevel/g_toplevel.mlg"
 

let vernac_toplevel pm =
  Pvernac.Unsafe.set_tactic_entry pm;
  vernac_toplevel


# 146 "toplevel/g_toplevel.ml"