Added support for Coq (#2803)

components.json

@@ -280,6 +280,10 @@
 			"title": "Content-Security-Policy",
 			"owner": "ScottHelme"
 		},
+		"coq": {
+			"title": "Coq",
+			"owner": "RunDevelopment"
+		},
 		"crystal": {
 			"title": "Crystal",
 			"require": "ruby",

components/prism-coq.js

@@ -0,0 +1,54 @@
+(function (Prism) {
+
+	// https://github.com/coq/coq
+
+	var commentSource = /\(\*(?:[^(*]|\((?!\*)|\*(?!\))|<self>)*\*\)/.source;
+	for (var i = 0; i < 2; i++) {
+		commentSource = commentSource.replace(/<self>/g, function () { return commentSource; });
+	}
+	commentSource = commentSource.replace(/<self>/g, '[]');
+
+	Prism.languages.coq = {
+		'comment': RegExp(commentSource),
+		'string': {
+			pattern: /"(?:[^"]|"")*"(?!")/,
+			greedy: true
+		},
+		'attribute': [
+			{
+				pattern: RegExp(
+					/#\[(?:[^\]("]|"(?:[^"]|"")*"(?!")|\((?!\*)|<comment>)*\]/.source
+						.replace(/<comment>/g, function () { return commentSource; })
+				),
+				greedy: true,
+				alias: 'attr-name',
+				inside: {
+					'comment': RegExp(commentSource),
+					'string': {
+						pattern: /"(?:[^"]|"")*"(?!")/,
+						greedy: true
+					},
+
+					'operator': /=/,
+					'punctuation': /^#\[|\]$|[,()]/
+				}
+			},
+			{
+				pattern: /\b(?:Cumulative|Global|Local|Monomorphic|NonCumulative|Polymorphic|Private|Program)\b/,
+				alias: 'attr-name'
+			}
+		],
+
+		'keyword': /\b(?:_|Abort|About|Add|Admit|Admitted|All|apply|Arguments|as|As|Assumptions|at|Axiom|Axioms|Back|BackTo|Backtrace|Bind|BinOp|BinOpSpec|BinRel|Blacklist|by|Canonical|Case|Cd|Check|Class|Classes|Close|Coercion|Coercions|cofix|CoFixpoint|CoInductive|Collection|Combined|Compute|Conjecture|Conjectures|Constant|Constants|Constraint|Constructors|Context|Corollary|Create|CstOp|Custom|Cut|Debug|Declare|Defined|Definition|Delimit|Dependencies|Dependent|Derive|Diffs|Drop|Elimination|else|end|End|Entry|Equality|Eval|Example|Existential|Existentials|Existing|exists|exists2|Export|Extern|Extraction|Fact|Fail|Field|File|Firstorder|fix|Fixpoint|Flags|Focus|for|forall|From|fun|Funclass|Function|Functional|GC|Generalizable|Goal|Grab|Grammar|Graph|Guarded|Haskell|Heap|Hide|Hint|HintDb|Hints|Hypotheses|Hypothesis|Identity|if|IF|Immediate|Implicit|Implicits|Import|in|Include|Induction|Inductive|Infix|Info|Initial|InjTyp|Inline|Inspect|Instance|Instances|Intro|Intros|Inversion|Inversion_clear|JSON|Language|Left|Lemma|let|Let|Lia|Libraries|Library|Load|LoadPath|Locate|Ltac|Ltac2|match|Match|measure|Method|Minimality|ML|Module|Modules|Morphism|move|Next|NoInline|Notation|Number|Obligation|Obligations|OCaml|Opaque|Open|Optimize|Parameter|Parameters|Parametric|Path|Paths|Prenex|Preterm|Primitive|Print|Profile|Projections|Proof|Prop|PropBinOp|Property|PropOp|Proposition|PropUOp|Pwd|Qed|Quit|Rec|Record|Recursive|Redirect|Reduction|Register|Relation|Remark|Remove|removed|Require|Reserved|Reset|Resolve|Restart|return|Rewrite|Right|Ring|Rings|Saturate|Save|Scheme|Scope|Scopes|Search|SearchHead|SearchPattern|SearchRewrite|Section|Separate|Set|Setoid|Show|Signatures|Solve|Solver|Sort|Sortclass|Sorted|Spec|SProp|Step|Strategies|Strategy|String|struct|Structure|SubClass|Subgraph|SuchThat|Tactic|Term|TestCompile|then|Theorem|Time|Timeout|To|Transparent|Type|Typeclasses|Types|Typing|Undelimit|Undo|Unfocus|Unfocused|Unfold|Universe|Universes|UnOp|UnOpSpec|Unshelve|using|Variable|Variables|Variant|Verbose|View|Visibility|wf|where|with|Zify)\b/,
+
+		'number': /\b(?:0x[a-f0-9][a-f0-9_]*(?:\.[a-f0-9_]+)?(?:p[+-]?\d[\d_]*)?|\d[\d_]*(?:\.[\d_]+)?(?:e[+-]?\d[\d_]*)?)\b/i,
+
+		'punct': {
+			pattern: /@\{|\{\||\[=|:>/,
+			alias: 'punctuation'
+		},
+		'operator': /\/\\|\\\/|\.{2,3}|:{1,2}=|\*\*|[-=]>|<(?:->?|[+:=>]|<:)|>(?:=|->)|\|[-|]?|[-!%&*+/<=>?@^~']/,
+		'punctuation': /\.\(|`\(|@\{|`\{|\{\||\[=|:>|[:.,;(){}\[\]]/
+	};
+
+}(Prism));

examples/prism-coq.html

@@ -0,0 +1,45 @@
+<h2>Full example</h2>
+<pre><code>(* Source: https://coq.inria.fr/a-short-introduction-to-coq *)
+
+Inductive seq : nat -> Set :=
+| niln : seq 0
+| consn : forall n : nat, nat -> seq n -> seq (S n).
+
+Fixpoint length (n : nat) (s : seq n) {struct s} : nat :=
+  match s with
+  | niln => 0
+  | consn i _ s' => S (length i s')
+  end.
+
+Theorem length_corr : forall (n : nat) (s : seq n), length n s = n.
+Proof.
+  intros n s.
+
+  (* reasoning by induction over s. Then, we have two new goals
+     corresponding on the case analysis about s (either it is
+     niln or some consn *)
+  induction s.
+
+    (* We are in the case where s is void. We can reduce the
+       term: length 0 niln *)
+    simpl.
+
+    (* We obtain the goal 0 = 0. *)
+    trivial.
+
+    (* now, we treat the case s = consn n e s with induction
+       hypothesis IHs *)
+    simpl.
+
+    (* The induction hypothesis has type length n s = n.
+       So we can use it to perform some rewriting in the goal: *)
+    rewrite IHs.
+
+    (* Now the goal is the trivial equality: S n = S n *)
+    trivial.
+
+  (* Now all sub cases are closed, we perform the ultimate
+     step: typing the term built using tactics and save it as
+     a witness of the theorem. *)
+Qed.
+</code></pre>

tests/languages/coq/attribute_feature.test

@@ -0,0 +1,73 @@
+#[program]
+#[program=yes]
+#[deprecated(since="8.9.0")]
+#[local, universes(polymorphic)]
+#[universes(polymorphic(foo,bar))]
+#[canonical=yes, canonical=no]
+#[ export ]
+
+----------------------------------------------------
+
+[
+	["attribute", [
+		["punctuation", "#["],
+		"program",
+		["punctuation", "]"]
+	]],
+	["attribute", [
+		["punctuation", "#["],
+		"program",
+		["operator", "="],
+		"yes",
+		["punctuation", "]"]
+	]],
+	["attribute", [
+		["punctuation", "#["],
+		"deprecated",
+		["punctuation", "("],
+		"since",
+		["operator", "="],
+		["string", "\"8.9.0\""],
+		["punctuation", ")"],
+		["punctuation", "]"]
+	]],
+	["attribute", [
+		["punctuation", "#["],
+		"local",
+		["punctuation", ","],
+		" universes",
+		["punctuation", "("],
+		"polymorphic",
+		["punctuation", ")"],
+		["punctuation", "]"]
+	]],
+	["attribute", [
+		["punctuation", "#["],
+		"universes",
+		["punctuation", "("],
+		"polymorphic",
+		["punctuation", "("],
+		"foo",
+		["punctuation", ","],
+		"bar",
+		["punctuation", ")"],
+		["punctuation", ")"],
+		["punctuation", "]"]
+	]],
+	["attribute", [
+		["punctuation", "#["],
+		"canonical",
+		["operator", "="],
+		"yes",
+		["punctuation", ","],
+		" canonical",
+		["operator", "="],
+		"no",
+		["punctuation", "]"]
+	]],
+	["attribute", [
+		["punctuation", "#["],
+		" export ",
+		["punctuation", "]"]
+	]]
+]

tests/languages/coq/comment_feature.test

@@ -0,0 +1,17 @@
+(**)
+(* comment *)
+(*
+ comment
+ *)
+
+(* comments (* can be (* nested *) *) *)
+
+----------------------------------------------------
+
+[
+	["comment", "(**)"],
+	["comment", "(* comment *)"],
+	["comment", "(*\r\n comment\r\n *)"],
+
+	["comment", "(* comments (* can be (* nested *) *) *)"]
+]