package rocq-runtime
The Rocq Prover -- Core Binaries and Tools
Install
dune-project
Dependency
Authors
Maintainers
Sources
rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20
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 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193# 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 | VernacShowGoalAt of { gid : int; sid: int } | VernacShowGoal of Vernacexpr.goal_reference | VernacShowProofDiffs of Proof_diffs.diffOpt let vernac_toplevel = Entry.make "toplevel:vernac_toplevel" let test_show_goal = let open Procq.Lookahead in to_entry "test_show_goal" begin lk_kw "Show" >> lk_kw "Goal" >> lk_nat end let test_show_natural = let open Procq.Lookahead in to_entry "test_show_natural" begin lk_kw "Show" >> lk_nat end # 34 "toplevel/g_toplevel.ml" let _ = let () = Procq.grammar_extend ~ignore_kw:false 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 -> # 61 "toplevel/g_toplevel.mlg" match cmd with | None -> None | Some v -> Some (VernacControl v) # 48 "toplevel/g_toplevel.ml" ); Procq.Production.make (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 ("Diffs")))))) ((Procq.Symbol.nterm qualid))) ((Procq.Symbol.token (Tok.PKEYWORD ("."))))) (fun _ id _ _ loc -> # 59 "toplevel/g_toplevel.mlg" Some (VernacShowGoal (GoalId id)) # 64 "toplevel/g_toplevel.ml" ); Procq.Production.make (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.next (Procq.Rule.stop) ((Procq.Symbol.nterm test_show_natural))) ((Procq.Symbol.token (Tok.PIDENT (Some ("Show")))))) ((Procq.Symbol.nterm natural))) ((Procq.Symbol.token (Tok.PKEYWORD ("."))))) (fun _ n _ _ loc -> # 58 "toplevel/g_toplevel.mlg" Some (VernacShowGoal (NthGoal n)) # 79 "toplevel/g_toplevel.ml" ); Procq.Production.make (Procq.Rule.next (Procq.Rule.next (Procq.Rule.stop) ((Procq.Symbol.token (Tok.PIDENT (Some ("Show")))))) ((Procq.Symbol.token (Tok.PKEYWORD ("."))))) (fun _ _ loc -> # 57 "toplevel/g_toplevel.mlg" Some (VernacShowGoal OpenSubgoals) # 90 "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 -> # 54 "toplevel/g_toplevel.mlg" () # 115 "toplevel/g_toplevel.ml" )])))) ((Procq.Symbol.token (Tok.PKEYWORD ("."))))) (fun _ removed _ _ _ loc -> # 55 "toplevel/g_toplevel.mlg" Some (VernacShowProofDiffs (if removed = None then Proof_diffs.DiffOn else Proof_diffs.DiffRemoved)) # 122 "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 -> # 53 "toplevel/g_toplevel.mlg" Some (VernacShowGoalAt {gid; sid}) # 145 "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 -> # 50 "toplevel/g_toplevel.mlg" Some (VernacBackTo n) # 158 "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 -> # 48 "toplevel/g_toplevel.mlg" Some VernacQuit # 169 "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 -> # 47 "toplevel/g_toplevel.mlg" Some VernacDrop # 180 "toplevel/g_toplevel.ml" )])])) in () # 69 "toplevel/g_toplevel.mlg" let vernac_toplevel pm = Pvernac.Unsafe.set_tactic_entry pm; vernac_toplevel # 193 "toplevel/g_toplevel.ml"