Skip to content

Commit

Permalink
Added support for Coq (#2803)
Browse files Browse the repository at this point in the history
  • Loading branch information
RunDevelopment authored Mar 25, 2021
1 parent 53d34b2 commit 41e25d3
Show file tree
Hide file tree
Showing 12 changed files with 902 additions and 1 deletion.
2 changes: 1 addition & 1 deletion components.js

Large diffs are not rendered by default.

4 changes: 4 additions & 0 deletions components.json
Original file line number Diff line number Diff line change
Expand Up @@ -280,6 +280,10 @@
"title": "Content-Security-Policy",
"owner": "ScottHelme"
},
"coq": {
"title": "Coq",
"owner": "RunDevelopment"
},
"crystal": {
"title": "Crystal",
"require": "ruby",
Expand Down
54 changes: 54 additions & 0 deletions components/prism-coq.js
Original file line number Diff line number Diff line change
@@ -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));
1 change: 1 addition & 0 deletions components/prism-coq.min.js

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

45 changes: 45 additions & 0 deletions examples/prism-coq.html
Original file line number Diff line number Diff line change
@@ -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>
73 changes: 73 additions & 0 deletions tests/languages/coq/attribute_feature.test
Original file line number Diff line number Diff line change
@@ -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", "]"]
]]
]
17 changes: 17 additions & 0 deletions tests/languages/coq/comment_feature.test
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
(**)
(* comment *)
(*
comment
*)

(* comments (* can be (* nested *) *) *)

----------------------------------------------------

[
["comment", "(**)"],
["comment", "(* comment *)"],
["comment", "(*\r\n comment\r\n *)"],

["comment", "(* comments (* can be (* nested *) *) *)"]
]
Loading

0 comments on commit 41e25d3

Please sign in to comment.