Merge pull request #125 from abevoelker/detect-coq-language

Add detection for the Coq language - fixes #116

lib/linguist/blob_helper.rb

@@ -511,6 +511,17 @@ module Linguist
       end
     end
 
+    # Internal: Guess language of .v files.
+    #
+    # Returns a Language
+    def guess_v_language
+      if lines.grep(/^(\/\*|\/\/|module|parameter|input|output|wire|reg|always|initial|begin|\`)/).any?
+        Language['Verilog']
+      else
+        Language['Coq']
+      end
+    end
+
     # Internal: Guess language of .gsp files.
     #
     # Returns a Language.

lib/linguist/languages.yml

@@ -220,6 +220,12 @@ Common Lisp:
   - .lisp
   - .ny
 
+Coq:
+  type: programming
+  lexer: Coq
+  extensions:
+  - .v
+
 Cpp-ObjDump:
   type: data
   lexer: cpp-objdump
@@ -1063,6 +1069,8 @@ Vala:
 Verilog:
   type: programming
   lexer: verilog
+  overrides:
+  - .v
   extensions:
   - .v
 

test/fixtures/interval_discr.v

@@ -0,0 +1,419 @@
+(** Sketch of the proof of {p:nat|p<=n} = {p:nat|p<=m} -> n=m
+
+  - preliminary results on the irrelevance of boundedness proofs
+  - introduce the notion of finite cardinal |A|
+  - prove that |{p:nat|p<=n}| = n
+  - prove that |A| = n /\ |A| = m -> n = m if equality is decidable on A
+  - prove that equality is decidable on A
+  - conclude
+*)
+
+(** * Preliminary results on [nat] and [le] *)
+
+(** Proving axiom K on [nat] *)
+
+Require Import Eqdep_dec.
+Require Import Arith.
+
+Theorem eq_rect_eq_nat :
+  forall (p:nat) (Q:nat->Type) (x:Q p) (h:p=p), x = eq_rect p Q x p h.
+Proof.
+intros.
+apply K_dec_set with (p := h).
+apply eq_nat_dec.
+reflexivity.
+Qed.
+
+(** Proving unicity of proofs of [(n<=m)%nat] *)
+
+Scheme le_ind' := Induction for le Sort Prop.
+
+Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q.
+Proof.
+induction p using le_ind'; intro q.
+ replace (le_n n) with
+  (eq_rect _ (fun n0 => n <= n0) (le_n n) _ (refl_equal n)).
+ 2:reflexivity.
+  generalize (refl_equal n).
+    pattern n at 2 4 6 10, q; case q; [intro | intros m l e].
+     rewrite <- eq_rect_eq_nat; trivial.
+     contradiction (le_Sn_n m); rewrite <- e; assumption.
+ replace (le_S n m p) with
+  (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ (refl_equal (S m))).
+ 2:reflexivity.
+  generalize (refl_equal (S m)).
+    pattern (S m) at 1 3 4 6, q; case q; [intro Heq | intros m0 l HeqS].
+     contradiction (le_Sn_n m); rewrite Heq; assumption.
+     injection HeqS; intro Heq; generalize l HeqS.
+      rewrite <- Heq; intros; rewrite <- eq_rect_eq_nat.
+      rewrite (IHp l0); reflexivity.
+Qed.
+
+(** Proving irrelevance of boundedness proofs while building
+    elements of interval *)
+
+Lemma dep_pair_intro :
+  forall (n x y:nat) (Hx : x<=n) (Hy : y<=n), x=y ->
+    exist (fun x => x <= n) x Hx = exist (fun x => x <= n) y Hy.
+Proof.
+intros n x y Hx Hy Heq.
+generalize Hy.
+rewrite <- Heq.
+intros.
+rewrite (le_uniqueness_proof x n Hx Hy0).
+reflexivity.
+Qed.
+
+(** * Proving that {p:nat|p<=n} = {p:nat|p<=m} -> n=m *)
+
+(** Definition of having finite cardinality [n+1] for a set [A] *)
+
+Definition card (A:Set) n :=
+  exists f,
+    (forall x:A, f x <= n) /\
+    (forall x y:A, f x = f y -> x = y) /\
+    (forall m, m <= n -> exists x:A, f x = m).
+
+Require Import Arith.
+
+(** Showing that the interval [0;n] has cardinality [n+1] *)
+
+Theorem card_interval : forall n, card {x:nat|x<=n} n.
+Proof.
+intro n.
+exists (fun x:{x:nat|x<=n} => proj1_sig x).
+split.
+(* bounded *)
+intro x; apply (proj2_sig x).
+split.
+(* injectivity *)
+intros (p,Hp) (q,Hq).
+simpl.
+intro Hpq.
+apply dep_pair_intro; assumption.
+(* surjectivity *)
+intros m Hmn.
+exists (exist (fun x : nat => x <= n) m Hmn).
+reflexivity.
+Qed.
+
+(** Showing that equality on the interval [0;n] is decidable *)
+
+Lemma interval_dec :
+  forall n (x y : {m:nat|m<=n}), {x=y}+{x<>y}.
+Proof.
+intros n (p,Hp).
+induction p; intros ([|q],Hq).
+left.
+  apply dep_pair_intro.
+  reflexivity.
+right.
+  intro H; discriminate H.
+right.
+  intro H; discriminate H.
+assert (Hp' : p <= n).
+  apply le_Sn_le; assumption.
+assert (Hq' : q <= n).
+  apply le_Sn_le; assumption.
+destruct (IHp Hp' (exist (fun m => m <= n) q Hq'))
+  as [Heq|Hneq].
+left.
+  injection Heq; intro Heq'.
+  apply dep_pair_intro.
+  apply eq_S.
+  assumption.
+right.
+  intro HeqS.
+  injection HeqS; intro Heq.
+  apply Hneq.
+  apply dep_pair_intro.
+  assumption.
+Qed.
+
+(** Showing that the cardinality relation is functional on decidable sets *)
+
+Lemma card_inj_aux :
+  forall (A:Type) f g n,
+    (forall x:A, f x <= 0) ->
+    (forall x y:A, f x = f y -> x = y) ->
+    (forall m, m <= S n -> exists x:A, g x = m)
+     -> False.
+Proof.
+intros A f g n Hfbound Hfinj Hgsurj.
+destruct (Hgsurj (S n) (le_n _)) as (x,Hx).
+destruct (Hgsurj n (le_S _ _ (le_n _))) as (x',Hx').
+assert (Hfx : 0 = f x).
+apply le_n_O_eq.
+apply Hfbound.
+assert (Hfx' : 0 = f x').
+apply le_n_O_eq.
+apply Hfbound.
+assert (x=x').
+apply Hfinj.
+rewrite <- Hfx.
+rewrite <- Hfx'.
+reflexivity.
+rewrite H in Hx.
+rewrite Hx' in Hx.
+apply (n_Sn _ Hx).
+Qed.
+
+(** For [dec_restrict], we use a lemma on the negation of equality
+that requires proof-irrelevance. It should be possible to avoid this
+lemma by generalizing over a first-order definition of [x<>y], say
+[neq] such that [{x=y}+{neq x y}] and [~(x=y /\ neq x y)]; for such
+[neq], unicity of proofs could be proven *)
+
+  Require Import Classical.
+  Lemma neq_dep_intro :
+   forall (A:Set) (z x y:A) (p:x<>z) (q:y<>z), x=y ->
+      exist (fun x => x <> z) x p = exist (fun x => x <> z) y q.
+  Proof.
+  intros A z x y p q Heq.
+   generalize q; clear q; rewrite <- Heq; intro q.
+   rewrite (proof_irrelevance _ p q); reflexivity.
+  Qed.
+
+Lemma dec_restrict :
+  forall (A:Set),
+    (forall x y :A, {x=y}+{x<>y}) ->
+     forall z (x y :{a:A|a<>z}), {x=y}+{x<>y}.
+Proof.
+intros A Hdec z (x,Hx) (y,Hy).
+destruct (Hdec x y) as [Heq|Hneq].
+left; apply neq_dep_intro; assumption.
+right; intro Heq; injection Heq; exact Hneq.
+Qed.
+
+Lemma pred_inj : forall n m,
+  0 <> n -> 0 <> m -> pred m = pred n -> m = n.
+Proof.
+destruct n.
+intros m H; destruct H; reflexivity.
+destruct m.
+intros _ H; destruct H; reflexivity.
+simpl; intros _ _ H.
+rewrite H.
+reflexivity.
+Qed.
+
+Lemma le_neq_lt : forall n m, n <= m -> n<>m -> n < m.
+Proof.
+intros n m Hle Hneq.
+destruct (le_lt_eq_dec n m Hle).
+assumption.
+contradiction.
+Qed.
+
+Lemma inj_restrict :
+  forall (A:Set) (f:A->nat) x y z,
+    (forall x y : A, f x = f y -> x = y)
+    -> x <> z -> f y < f z -> f z <= f x
+    -> pred (f x) = f y
+    -> False.
+
+(* Search error sans le type de f !! *)
+Proof.
+intros A f x y z Hfinj Hneqx Hfy Hfx Heq.
+assert (f z <> f x).
+  apply sym_not_eq.
+  intro Heqf.
+  apply Hneqx.
+  apply Hfinj.
+  assumption.
+assert (f x = S (f y)).
+  assert (0 < f x).
+    apply le_lt_trans with (f z).
+    apply le_O_n.
+    apply le_neq_lt; assumption.
+  apply pred_inj.
+  apply O_S.
+  apply lt_O_neq; assumption.
+  exact Heq.
+assert (f z <= f y).
+destruct (le_lt_or_eq _ _ Hfx).
+  apply lt_n_Sm_le.
+  rewrite <- H0.
+  assumption.
+  contradiction Hneqx.
+  symmetry.
+  apply Hfinj.
+  assumption.
+contradiction (lt_not_le (f y) (f z)).
+Qed.
+
+Theorem card_inj : forall m n (A:Set),
+  (forall x y :A, {x=y}+{x<>y}) ->
+  card A m -> card A n -> m = n.
+Proof.
+induction m; destruct n;
+intros A Hdec
+ (f,(Hfbound,(Hfinj,Hfsurj)))
+ (g,(Hgbound,(Hginj,Hgsurj))).
+(* 0/0 *)
+reflexivity.
+(* 0/Sm *)
+destruct (card_inj_aux _ _ _ _ Hfbound Hfinj Hgsurj).
+(* Sn/0 *)
+destruct (card_inj_aux _ _ _ _ Hgbound Hginj Hfsurj).
+(* Sn/Sm *)
+destruct (Hgsurj (S n) (le_n _)) as (xSn,HSnx).
+rewrite IHm with (n:=n) (A := {x:A|x<>xSn}).
+reflexivity.
+(* decidability of eq on {x:A|x<>xSm} *)
+apply dec_restrict.
+assumption.
+(* cardinality of {x:A|x<>xSn} is m *)
+pose (f' := fun x' : {x:A|x<>xSn} =>
+    let (x,Hneq) := x' in
+    if le_lt_dec (f xSn) (f x)
+    then pred (f x)
+    else f x).
+exists f'.
+split.
+(* f' is bounded *)
+unfold f'.
+intros (x,_).
+destruct (le_lt_dec (f xSn) (f x)) as [Hle|Hge].
+change m with (pred (S m)).
+apply le_pred.
+apply Hfbound.
+apply le_S_n.
+apply le_trans with (f xSn).
+exact Hge.
+apply Hfbound.
+split.
+(* f' is injective *)
+unfold f'.
+intros (x,Hneqx) (y,Hneqy) Heqf'.
+destruct (le_lt_dec (f xSn) (f x)) as [Hlefx|Hgefx];
+destruct (le_lt_dec (f xSn) (f y)) as [Hlefy|Hgefy].
+(* f xSn <= f x et f xSn <= f y *)
+assert (Heq : x = y).
+  apply Hfinj.
+  assert (f xSn <> f y).
+    apply sym_not_eq.
+    intro Heqf.
+    apply Hneqy.
+    apply Hfinj.
+    assumption.
+  assert (0 < f y).
+    apply le_lt_trans with (f xSn).
+    apply le_O_n.
+    apply le_neq_lt; assumption.
+  assert (f xSn <> f x).
+    apply sym_not_eq.
+    intro Heqf.
+    apply Hneqx.
+    apply Hfinj.
+    assumption.
+  assert (0 < f x).
+    apply le_lt_trans with (f xSn).
+    apply le_O_n.
+    apply le_neq_lt; assumption.
+  apply pred_inj.
+  apply lt_O_neq; assumption.
+  apply lt_O_neq; assumption.
+  assumption.
+apply neq_dep_intro; assumption.
+(* f y < f xSn <= f x *)
+destruct (inj_restrict A f x y xSn); assumption.
+(* f x < f xSn <= f y *)
+symmetry in Heqf'.
+destruct (inj_restrict A f y x xSn); assumption.
+(* f x < f xSn et f y < f xSn *)
+assert (Heq : x=y).
+  apply Hfinj; assumption.
+apply neq_dep_intro; assumption.
+(* f' is surjective *)
+intros p Hlep.
+destruct (le_lt_dec (f xSn) p) as [Hle|Hlt].
+(* case f xSn <= p *)
+destruct (Hfsurj (S p) (le_n_S _ _ Hlep)) as (x,Hx).
+assert (Hneq : x <> xSn).
+  intro Heqx.
+  rewrite Heqx in Hx.
+  rewrite Hx in Hle.
+  apply le_Sn_n with p; assumption.
+exists (exist (fun a => a<>xSn) x Hneq).
+unfold f'.
+destruct (le_lt_dec (f xSn) (f x)) as [Hle'|Hlt'].
+rewrite Hx; reflexivity.
+rewrite Hx in Hlt'.
+contradiction (le_not_lt (f xSn) p).
+apply lt_trans with (S p).
+apply lt_n_Sn.
+assumption.
+(* case p < f xSn *)
+destruct (Hfsurj p (le_S _ _ Hlep)) as (x,Hx).
+assert (Hneq : x <> xSn).
+  intro Heqx.
+  rewrite Heqx in Hx.
+  rewrite Hx in Hlt.
+  apply (lt_irrefl p).
+  assumption.
+exists (exist (fun a => a<>xSn) x Hneq).
+unfold f'.
+destruct (le_lt_dec (f xSn) (f x)) as [Hle'|Hlt'].
+  rewrite Hx in Hle'.
+  contradiction (lt_irrefl p).
+  apply lt_le_trans with (f xSn); assumption.
+  assumption.
+(* cardinality of {x:A|x<>xSn} is n *)
+pose (g' := fun x' : {x:A|x<>xSn} =>
+   let (x,Hneq) := x' in
+   if Hdec x xSn then 0 else g x).
+exists g'.
+split.
+(* g is bounded *)
+unfold g'.
+intros (x,_).
+destruct (Hdec x xSn) as [_|Hneq].
+apply le_O_n.
+assert (Hle_gx:=Hgbound x).
+destruct (le_lt_or_eq _ _ Hle_gx).
+apply lt_n_Sm_le.
+assumption.
+contradiction Hneq.
+apply Hginj.
+rewrite HSnx.
+assumption.
+split.
+(* g is injective *)
+unfold g'.
+intros (x,Hneqx) (y,Hneqy) Heqg'.
+destruct (Hdec x xSn) as [Heqx|_].
+contradiction Hneqx.
+destruct (Hdec y xSn) as [Heqy|_].
+contradiction Hneqy.
+assert (Heq : x=y).
+  apply Hginj; assumption.
+apply neq_dep_intro; assumption.
+(* g is surjective *)
+intros p Hlep.
+destruct (Hgsurj p (le_S _ _ Hlep)) as (x,Hx).
+assert (Hneq : x<>xSn).
+  intro Heq.
+  rewrite Heq in Hx.
+  rewrite Hx in HSnx.
+  rewrite HSnx in Hlep.
+  contradiction (le_Sn_n _ Hlep).
+exists (exist (fun a => a<>xSn) x Hneq).
+simpl.
+destruct (Hdec x xSn) as [Heqx|_].
+contradiction Hneq.
+assumption.
+Qed.
+
+(** Conclusion *)
+
+Theorem interval_discr :
+  forall n m, {p:nat|p<=n} = {p:nat|p<=m} -> n=m.
+Proof.
+intros n m Heq.
+apply card_inj with (A := {p:nat|p<=n}).
+apply interval_dec.
+apply card_interval.
+rewrite Heq.
+apply card_interval.
+Qed.

test/fixtures/sha-256-functions.v

@@ -0,0 +1,86 @@
+/*
+*
+* Copyright (c) 2011 fpgaminer@bitcoin-mining.com
+*
+*
+*
+* This program is free software: you can redistribute it and/or modify
+* it under the terms of the GNU General Public License as published by
+* the Free Software Foundation, either version 3 of the License, or
+* (at your option) any later version.
+*
+* This program is distributed in the hope that it will be useful,
+* but WITHOUT ANY WARRANTY; without even the implied warranty of
+* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+* GNU General Public License for more details.
+*
+* You should have received a copy of the GNU General Public License
+* along with this program.  If not, see <http://www.gnu.org/licenses/>.
+* 
+*/
+
+
+`timescale 1ns/1ps
+
+module e0 (x, y);
+
+	input [31:0] x;
+	output [31:0] y;
+
+	assign y = {x[1:0],x[31:2]} ^ {x[12:0],x[31:13]} ^ {x[21:0],x[31:22]};
+
+endmodule
+
+
+module e1 (x, y);
+
+	input [31:0] x;
+	output [31:0] y;
+
+	assign y = {x[5:0],x[31:6]} ^ {x[10:0],x[31:11]} ^ {x[24:0],x[31:25]};
+
+endmodule
+
+
+module ch (x, y, z, o);
+
+	input [31:0] x, y, z;
+	output [31:0] o;
+
+	assign o = z ^ (x & (y ^ z));
+
+endmodule
+
+
+module maj (x, y, z, o);
+
+	input [31:0] x, y, z;
+	output [31:0] o;
+
+	assign o = (x & y) | (z & (x | y));
+
+endmodule
+
+
+module s0 (x, y);
+
+	input [31:0] x;
+	output [31:0] y;
+
+	assign y[31:29] = x[6:4] ^ x[17:15];
+	assign y[28:0] = {x[3:0], x[31:7]} ^ {x[14:0],x[31:18]} ^ x[31:3];
+
+endmodule
+
+
+module s1 (x, y);
+
+	input [31:0] x;
+	output [31:0] y;
+
+	assign y[31:22] = x[16:7] ^ x[18:9];
+	assign y[21:0] = {x[6:0],x[31:17]} ^ {x[8:0],x[31:19]} ^ x[31:10];
+
+endmodule
+
+

test/test_blob.rb

@@ -306,6 +306,12 @@ class TestBlob < Test::Unit::TestCase
     assert_equal Language['Perl'],        blob("perl-test.t").language
     assert_equal Language['Turing'],      blob("turing.t").language
 
+    # .v disambiguation
+    # https://github.com/progranism/Open-Source-FPGA-Bitcoin-Miner/blob/master/src/sha-256-functions.v
+    assert_equal Language['Verilog'],     blob("sha-256-functions.v").language
+    # https://github.com/coq/coq/blob/trunk/doc/faq/interval_discr.v
+    assert_equal Language['Coq'],         blob("interval_discr.v").language
+
     # ML
     assert_equal Language['OCaml'],       blob("Foo.ml").language
     assert_equal Language['Standard ML'], blob("Foo.sig").language

test/test_language.rb

@@ -23,6 +23,9 @@ class TestLanguage < Test::Unit::TestCase
 
     assert Language.ambiguous?('.t')
     assert_equal Language['Perl'], Language.find_by_extension('t')
+
+    assert Language.ambiguous?('.v')
+    assert_equal Language['Verilog'], Language.find_by_extension('v')
   end
 
   def test_lexer
@@ -34,6 +37,7 @@ class TestLanguage < Test::Unit::TestCase
     assert_equal Lexer['C'], Language['XS'].lexer
     assert_equal Lexer['C++'], Language['C++'].lexer
     assert_equal Lexer['Coldfusion HTML'], Language['ColdFusion'].lexer
+    assert_equal Lexer['Coq'], Language['Coq'].lexer
     assert_equal Lexer['Fortran'], Language['FORTRAN'].lexer
     assert_equal Lexer['Gherkin'], Language['Cucumber'].lexer
     assert_equal Lexer['HTML'], Language['HTML'].lexer
@@ -63,6 +67,7 @@ class TestLanguage < Test::Unit::TestCase
     assert_equal Lexer['Scheme'], Language['Scheme'].lexer
     assert_equal Lexer['TeX'], Language['TeX'].lexer
     assert_equal Lexer['Text only'], Language['Text'].lexer
+    assert_equal Lexer['Verilog'], Language['Verilog'].lexer
     assert_equal Lexer['aspx-vb'], Language['ASP'].lexer
     assert_equal Lexer['haXe'], Language['HaXe'].lexer
     assert_equal Lexer['reStructuredText'], Language['reStructuredText'].lexer