| 1 | /*
|
| 2 | Language: Coq
|
| 3 | Author: Stephan Boyer <stephan@stephanboyer.com>
|
| 4 | Category: functional
|
| 5 | Website: https://coq.inria.fr
|
| 6 | */
|
| 7 |
|
| 8 | /** @type LanguageFn */
|
| 9 | function coq(hljs) {
|
| 10 | const KEYWORDS = [
|
| 11 | "_|0",
|
| 12 | "as",
|
| 13 | "at",
|
| 14 | "cofix",
|
| 15 | "else",
|
| 16 | "end",
|
| 17 | "exists",
|
| 18 | "exists2",
|
| 19 | "fix",
|
| 20 | "for",
|
| 21 | "forall",
|
| 22 | "fun",
|
| 23 | "if",
|
| 24 | "IF",
|
| 25 | "in",
|
| 26 | "let",
|
| 27 | "match",
|
| 28 | "mod",
|
| 29 | "Prop",
|
| 30 | "return",
|
| 31 | "Set",
|
| 32 | "then",
|
| 33 | "Type",
|
| 34 | "using",
|
| 35 | "where",
|
| 36 | "with",
|
| 37 | "Abort",
|
| 38 | "About",
|
| 39 | "Add",
|
| 40 | "Admit",
|
| 41 | "Admitted",
|
| 42 | "All",
|
| 43 | "Arguments",
|
| 44 | "Assumptions",
|
| 45 | "Axiom",
|
| 46 | "Back",
|
| 47 | "BackTo",
|
| 48 | "Backtrack",
|
| 49 | "Bind",
|
| 50 | "Blacklist",
|
| 51 | "Canonical",
|
| 52 | "Cd",
|
| 53 | "Check",
|
| 54 | "Class",
|
| 55 | "Classes",
|
| 56 | "Close",
|
| 57 | "Coercion",
|
| 58 | "Coercions",
|
| 59 | "CoFixpoint",
|
| 60 | "CoInductive",
|
| 61 | "Collection",
|
| 62 | "Combined",
|
| 63 | "Compute",
|
| 64 | "Conjecture",
|
| 65 | "Conjectures",
|
| 66 | "Constant",
|
| 67 | "constr",
|
| 68 | "Constraint",
|
| 69 | "Constructors",
|
| 70 | "Context",
|
| 71 | "Corollary",
|
| 72 | "CreateHintDb",
|
| 73 | "Cut",
|
| 74 | "Declare",
|
| 75 | "Defined",
|
| 76 | "Definition",
|
| 77 | "Delimit",
|
| 78 | "Dependencies",
|
| 79 | "Dependent",
|
| 80 | "Derive",
|
| 81 | "Drop",
|
| 82 | "eauto",
|
| 83 | "End",
|
| 84 | "Equality",
|
| 85 | "Eval",
|
| 86 | "Example",
|
| 87 | "Existential",
|
| 88 | "Existentials",
|
| 89 | "Existing",
|
| 90 | "Export",
|
| 91 | "exporting",
|
| 92 | "Extern",
|
| 93 | "Extract",
|
| 94 | "Extraction",
|
| 95 | "Fact",
|
| 96 | "Field",
|
| 97 | "Fields",
|
| 98 | "File",
|
| 99 | "Fixpoint",
|
| 100 | "Focus",
|
| 101 | "for",
|
| 102 | "From",
|
| 103 | "Function",
|
| 104 | "Functional",
|
| 105 | "Generalizable",
|
| 106 | "Global",
|
| 107 | "Goal",
|
| 108 | "Grab",
|
| 109 | "Grammar",
|
| 110 | "Graph",
|
| 111 | "Guarded",
|
| 112 | "Heap",
|
| 113 | "Hint",
|
| 114 | "HintDb",
|
| 115 | "Hints",
|
| 116 | "Hypotheses",
|
| 117 | "Hypothesis",
|
| 118 | "ident",
|
| 119 | "Identity",
|
| 120 | "If",
|
| 121 | "Immediate",
|
| 122 | "Implicit",
|
| 123 | "Import",
|
| 124 | "Include",
|
| 125 | "Inductive",
|
| 126 | "Infix",
|
| 127 | "Info",
|
| 128 | "Initial",
|
| 129 | "Inline",
|
| 130 | "Inspect",
|
| 131 | "Instance",
|
| 132 | "Instances",
|
| 133 | "Intro",
|
| 134 | "Intros",
|
| 135 | "Inversion",
|
| 136 | "Inversion_clear",
|
| 137 | "Language",
|
| 138 | "Left",
|
| 139 | "Lemma",
|
| 140 | "Let",
|
| 141 | "Libraries",
|
| 142 | "Library",
|
| 143 | "Load",
|
| 144 | "LoadPath",
|
| 145 | "Local",
|
| 146 | "Locate",
|
| 147 | "Ltac",
|
| 148 | "ML",
|
| 149 | "Mode",
|
| 150 | "Module",
|
| 151 | "Modules",
|
| 152 | "Monomorphic",
|
| 153 | "Morphism",
|
| 154 | "Next",
|
| 155 | "NoInline",
|
| 156 | "Notation",
|
| 157 | "Obligation",
|
| 158 | "Obligations",
|
| 159 | "Opaque",
|
| 160 | "Open",
|
| 161 | "Optimize",
|
| 162 | "Options",
|
| 163 | "Parameter",
|
| 164 | "Parameters",
|
| 165 | "Parametric",
|
| 166 | "Path",
|
| 167 | "Paths",
|
| 168 | "pattern",
|
| 169 | "Polymorphic",
|
| 170 | "Preterm",
|
| 171 | "Print",
|
| 172 | "Printing",
|
| 173 | "Program",
|
| 174 | "Projections",
|
| 175 | "Proof",
|
| 176 | "Proposition",
|
| 177 | "Pwd",
|
| 178 | "Qed",
|
| 179 | "Quit",
|
| 180 | "Rec",
|
| 181 | "Record",
|
| 182 | "Recursive",
|
| 183 | "Redirect",
|
| 184 | "Relation",
|
| 185 | "Remark",
|
| 186 | "Remove",
|
| 187 | "Require",
|
| 188 | "Reserved",
|
| 189 | "Reset",
|
| 190 | "Resolve",
|
| 191 | "Restart",
|
| 192 | "Rewrite",
|
| 193 | "Right",
|
| 194 | "Ring",
|
| 195 | "Rings",
|
| 196 | "Save",
|
| 197 | "Scheme",
|
| 198 | "Scope",
|
| 199 | "Scopes",
|
| 200 | "Script",
|
| 201 | "Search",
|
| 202 | "SearchAbout",
|
| 203 | "SearchHead",
|
| 204 | "SearchPattern",
|
| 205 | "SearchRewrite",
|
| 206 | "Section",
|
| 207 | "Separate",
|
| 208 | "Set",
|
| 209 | "Setoid",
|
| 210 | "Show",
|
| 211 | "Solve",
|
| 212 | "Sorted",
|
| 213 | "Step",
|
| 214 | "Strategies",
|
| 215 | "Strategy",
|
| 216 | "Structure",
|
| 217 | "SubClass",
|
| 218 | "Table",
|
| 219 | "Tables",
|
| 220 | "Tactic",
|
| 221 | "Term",
|
| 222 | "Test",
|
| 223 | "Theorem",
|
| 224 | "Time",
|
| 225 | "Timeout",
|
| 226 | "Transparent",
|
| 227 | "Type",
|
| 228 | "Typeclasses",
|
| 229 | "Types",
|
| 230 | "Undelimit",
|
| 231 | "Undo",
|
| 232 | "Unfocus",
|
| 233 | "Unfocused",
|
| 234 | "Unfold",
|
| 235 | "Universe",
|
| 236 | "Universes",
|
| 237 | "Unset",
|
| 238 | "Unshelve",
|
| 239 | "using",
|
| 240 | "Variable",
|
| 241 | "Variables",
|
| 242 | "Variant",
|
| 243 | "Verbose",
|
| 244 | "Visibility",
|
| 245 | "where",
|
| 246 | "with"
|
| 247 | ];
|
| 248 | const BUILT_INS = [
|
| 249 | "abstract",
|
| 250 | "absurd",
|
| 251 | "admit",
|
| 252 | "after",
|
| 253 | "apply",
|
| 254 | "as",
|
| 255 | "assert",
|
| 256 | "assumption",
|
| 257 | "at",
|
| 258 | "auto",
|
| 259 | "autorewrite",
|
| 260 | "autounfold",
|
| 261 | "before",
|
| 262 | "bottom",
|
| 263 | "btauto",
|
| 264 | "by",
|
| 265 | "case",
|
| 266 | "case_eq",
|
| 267 | "cbn",
|
| 268 | "cbv",
|
| 269 | "change",
|
| 270 | "classical_left",
|
| 271 | "classical_right",
|
| 272 | "clear",
|
| 273 | "clearbody",
|
| 274 | "cofix",
|
| 275 | "compare",
|
| 276 | "compute",
|
| 277 | "congruence",
|
| 278 | "constr_eq",
|
| 279 | "constructor",
|
| 280 | "contradict",
|
| 281 | "contradiction",
|
| 282 | "cut",
|
| 283 | "cutrewrite",
|
| 284 | "cycle",
|
| 285 | "decide",
|
| 286 | "decompose",
|
| 287 | "dependent",
|
| 288 | "destruct",
|
| 289 | "destruction",
|
| 290 | "dintuition",
|
| 291 | "discriminate",
|
| 292 | "discrR",
|
| 293 | "do",
|
| 294 | "double",
|
| 295 | "dtauto",
|
| 296 | "eapply",
|
| 297 | "eassumption",
|
| 298 | "eauto",
|
| 299 | "ecase",
|
| 300 | "econstructor",
|
| 301 | "edestruct",
|
| 302 | "ediscriminate",
|
| 303 | "eelim",
|
| 304 | "eexact",
|
| 305 | "eexists",
|
| 306 | "einduction",
|
| 307 | "einjection",
|
| 308 | "eleft",
|
| 309 | "elim",
|
| 310 | "elimtype",
|
| 311 | "enough",
|
| 312 | "equality",
|
| 313 | "erewrite",
|
| 314 | "eright",
|
| 315 | "esimplify_eq",
|
| 316 | "esplit",
|
| 317 | "evar",
|
| 318 | "exact",
|
| 319 | "exactly_once",
|
| 320 | "exfalso",
|
| 321 | "exists",
|
| 322 | "f_equal",
|
| 323 | "fail",
|
| 324 | "field",
|
| 325 | "field_simplify",
|
| 326 | "field_simplify_eq",
|
| 327 | "first",
|
| 328 | "firstorder",
|
| 329 | "fix",
|
| 330 | "fold",
|
| 331 | "fourier",
|
| 332 | "functional",
|
| 333 | "generalize",
|
| 334 | "generalizing",
|
| 335 | "gfail",
|
| 336 | "give_up",
|
| 337 | "has_evar",
|
| 338 | "hnf",
|
| 339 | "idtac",
|
| 340 | "in",
|
| 341 | "induction",
|
| 342 | "injection",
|
| 343 | "instantiate",
|
| 344 | "intro",
|
| 345 | "intro_pattern",
|
| 346 | "intros",
|
| 347 | "intuition",
|
| 348 | "inversion",
|
| 349 | "inversion_clear",
|
| 350 | "is_evar",
|
| 351 | "is_var",
|
| 352 | "lapply",
|
| 353 | "lazy",
|
| 354 | "left",
|
| 355 | "lia",
|
| 356 | "lra",
|
| 357 | "move",
|
| 358 | "native_compute",
|
| 359 | "nia",
|
| 360 | "nsatz",
|
| 361 | "omega",
|
| 362 | "once",
|
| 363 | "pattern",
|
| 364 | "pose",
|
| 365 | "progress",
|
| 366 | "proof",
|
| 367 | "psatz",
|
| 368 | "quote",
|
| 369 | "record",
|
| 370 | "red",
|
| 371 | "refine",
|
| 372 | "reflexivity",
|
| 373 | "remember",
|
| 374 | "rename",
|
| 375 | "repeat",
|
| 376 | "replace",
|
| 377 | "revert",
|
| 378 | "revgoals",
|
| 379 | "rewrite",
|
| 380 | "rewrite_strat",
|
| 381 | "right",
|
| 382 | "ring",
|
| 383 | "ring_simplify",
|
| 384 | "rtauto",
|
| 385 | "set",
|
| 386 | "setoid_reflexivity",
|
| 387 | "setoid_replace",
|
| 388 | "setoid_rewrite",
|
| 389 | "setoid_symmetry",
|
| 390 | "setoid_transitivity",
|
| 391 | "shelve",
|
| 392 | "shelve_unifiable",
|
| 393 | "simpl",
|
| 394 | "simple",
|
| 395 | "simplify_eq",
|
| 396 | "solve",
|
| 397 | "specialize",
|
| 398 | "split",
|
| 399 | "split_Rabs",
|
| 400 | "split_Rmult",
|
| 401 | "stepl",
|
| 402 | "stepr",
|
| 403 | "subst",
|
| 404 | "sum",
|
| 405 | "swap",
|
| 406 | "symmetry",
|
| 407 | "tactic",
|
| 408 | "tauto",
|
| 409 | "time",
|
| 410 | "timeout",
|
| 411 | "top",
|
| 412 | "transitivity",
|
| 413 | "trivial",
|
| 414 | "try",
|
| 415 | "tryif",
|
| 416 | "unfold",
|
| 417 | "unify",
|
| 418 | "until",
|
| 419 | "using",
|
| 420 | "vm_compute",
|
| 421 | "with"
|
| 422 | ];
|
| 423 | return {
|
| 424 | name: 'Coq',
|
| 425 | keywords: {
|
| 426 | keyword: KEYWORDS,
|
| 427 | built_in: BUILT_INS
|
| 428 | },
|
| 429 | contains: [
|
| 430 | hljs.QUOTE_STRING_MODE,
|
| 431 | hljs.COMMENT('\\(\\*', '\\*\\)'),
|
| 432 | hljs.C_NUMBER_MODE,
|
| 433 | {
|
| 434 | className: 'type',
|
| 435 | excludeBegin: true,
|
| 436 | begin: '\\|\\s*',
|
| 437 | end: '\\w+'
|
| 438 | },
|
| 439 | { // relevance booster
|
| 440 | begin: /[-=]>/ }
|
| 441 | ]
|
| 442 | };
|
| 443 | }
|
| 444 |
|
| 445 | module.exports = coq;
|