mirror of
https://github.com/KevinMidboe/linguist.git
synced 2025-10-29 17:50:22 +00:00
Merging github/master 0872058
This commit is contained in:
@@ -417,6 +417,17 @@ module Linguist
|
|||||||
end
|
end
|
||||||
end
|
end
|
||||||
|
|
||||||
|
# Internal: Guess language of .cls files
|
||||||
|
#
|
||||||
|
# Returns a Language.
|
||||||
|
def guess_cls_language
|
||||||
|
if lines.grep(/^(%|\\)/).any?
|
||||||
|
Language['TeX']
|
||||||
|
else
|
||||||
|
Language['OpenEdge ABL']
|
||||||
|
end
|
||||||
|
end
|
||||||
|
|
||||||
# Internal: Guess language of header files (.h).
|
# Internal: Guess language of header files (.h).
|
||||||
#
|
#
|
||||||
# Returns a Language.
|
# Returns a Language.
|
||||||
@@ -511,6 +522,17 @@ module Linguist
|
|||||||
end
|
end
|
||||||
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.
|
# Internal: Guess language of .gsp files.
|
||||||
#
|
#
|
||||||
# Returns a Language.
|
# Returns a Language.
|
||||||
|
|||||||
@@ -1,5 +1,6 @@
|
|||||||
require 'yaml'
|
require 'escape_utils'
|
||||||
require 'pygments'
|
require 'pygments'
|
||||||
|
require 'yaml'
|
||||||
|
|
||||||
module Linguist
|
module Linguist
|
||||||
# Language names that are recognizable by GitHub. Defined languages
|
# Language names that are recognizable by GitHub. Defined languages
|
||||||
@@ -322,6 +323,19 @@ module Linguist
|
|||||||
# Returns the extensions Array
|
# Returns the extensions Array
|
||||||
attr_reader :filenames
|
attr_reader :filenames
|
||||||
|
|
||||||
|
# Public: Get URL escaped name.
|
||||||
|
#
|
||||||
|
# Examples
|
||||||
|
#
|
||||||
|
# "C%23"
|
||||||
|
# "C%2B%2B"
|
||||||
|
# "Common%20Lisp"
|
||||||
|
#
|
||||||
|
# Returns the escaped String.
|
||||||
|
def escaped_name
|
||||||
|
EscapeUtils.escape_url(name).gsub('+', '%20')
|
||||||
|
end
|
||||||
|
|
||||||
# Internal: Get default alias name
|
# Internal: Get default alias name
|
||||||
#
|
#
|
||||||
# Returns the alias name String
|
# Returns the alias name String
|
||||||
|
|||||||
@@ -120,6 +120,11 @@ Brainfuck:
|
|||||||
- .b
|
- .b
|
||||||
- .bf
|
- .bf
|
||||||
|
|
||||||
|
Bro:
|
||||||
|
type: programming
|
||||||
|
extensions:
|
||||||
|
- .bro
|
||||||
|
|
||||||
C:
|
C:
|
||||||
type: programming
|
type: programming
|
||||||
overrides:
|
overrides:
|
||||||
@@ -128,6 +133,7 @@ C:
|
|||||||
extensions:
|
extensions:
|
||||||
- .c
|
- .c
|
||||||
- .h
|
- .h
|
||||||
|
- .w
|
||||||
|
|
||||||
C#:
|
C#:
|
||||||
type: programming
|
type: programming
|
||||||
@@ -162,6 +168,15 @@ C-ObjDump:
|
|||||||
extensions:
|
extensions:
|
||||||
- .c-objdump
|
- .c-objdump
|
||||||
|
|
||||||
|
C2hs Haskell:
|
||||||
|
type: programming
|
||||||
|
lexer: Haskell
|
||||||
|
group: Haskell
|
||||||
|
aliases:
|
||||||
|
- c2hs
|
||||||
|
extensions:
|
||||||
|
- .chs
|
||||||
|
|
||||||
CMake:
|
CMake:
|
||||||
extensions:
|
extensions:
|
||||||
- .cmake
|
- .cmake
|
||||||
@@ -214,6 +229,12 @@ Common Lisp:
|
|||||||
- .lisp
|
- .lisp
|
||||||
- .ny
|
- .ny
|
||||||
|
|
||||||
|
Coq:
|
||||||
|
type: programming
|
||||||
|
lexer: Coq
|
||||||
|
extensions:
|
||||||
|
- .v
|
||||||
|
|
||||||
Cpp-ObjDump:
|
Cpp-ObjDump:
|
||||||
type: data
|
type: data
|
||||||
lexer: cpp-objdump
|
lexer: cpp-objdump
|
||||||
@@ -280,6 +301,13 @@ Eiffel:
|
|||||||
extensions:
|
extensions:
|
||||||
- .e
|
- .e
|
||||||
|
|
||||||
|
Elixir:
|
||||||
|
type: programming
|
||||||
|
primary_extension: .ex
|
||||||
|
extensions:
|
||||||
|
- .ex
|
||||||
|
- .exs
|
||||||
|
|
||||||
Emacs Lisp:
|
Emacs Lisp:
|
||||||
type: programming
|
type: programming
|
||||||
lexer: Scheme
|
lexer: Scheme
|
||||||
@@ -566,6 +594,12 @@ Literate Haskell:
|
|||||||
extensions:
|
extensions:
|
||||||
- .lhs
|
- .lhs
|
||||||
|
|
||||||
|
Logtalk:
|
||||||
|
type: programming
|
||||||
|
primary_extension: .lgt
|
||||||
|
extensions:
|
||||||
|
- .lgt
|
||||||
|
|
||||||
Lua:
|
Lua:
|
||||||
type: programming
|
type: programming
|
||||||
primary_extension: .lua
|
primary_extension: .lua
|
||||||
@@ -706,6 +740,19 @@ OpenCL:
|
|||||||
extensions:
|
extensions:
|
||||||
- .cl
|
- .cl
|
||||||
|
|
||||||
|
OpenEdge ABL:
|
||||||
|
type: programming
|
||||||
|
aliases:
|
||||||
|
- progress
|
||||||
|
- openedge
|
||||||
|
- abl
|
||||||
|
primary_extension: .p
|
||||||
|
overrides:
|
||||||
|
- .cls
|
||||||
|
extensions:
|
||||||
|
- .cls
|
||||||
|
- .p
|
||||||
|
|
||||||
PHP:
|
PHP:
|
||||||
type: programming
|
type: programming
|
||||||
extensions:
|
extensions:
|
||||||
@@ -757,6 +804,15 @@ Perl:
|
|||||||
- .psgi
|
- .psgi
|
||||||
- .t
|
- .t
|
||||||
|
|
||||||
|
Powershell:
|
||||||
|
type: programming
|
||||||
|
lexer: Text only
|
||||||
|
aliases:
|
||||||
|
- posh
|
||||||
|
extensions:
|
||||||
|
- .ps1
|
||||||
|
- .psm1
|
||||||
|
|
||||||
Prolog:
|
Prolog:
|
||||||
type: programming
|
type: programming
|
||||||
extensions:
|
extensions:
|
||||||
@@ -920,6 +976,13 @@ Scheme:
|
|||||||
- .sps
|
- .sps
|
||||||
- .ss
|
- .ss
|
||||||
|
|
||||||
|
Scilab:
|
||||||
|
type: programming
|
||||||
|
primary_extension: .sci
|
||||||
|
extensions:
|
||||||
|
- .sce
|
||||||
|
- .tst
|
||||||
|
|
||||||
Self:
|
Self:
|
||||||
type: programming
|
type: programming
|
||||||
lexer: Text only
|
lexer: Text only
|
||||||
@@ -1050,6 +1113,8 @@ Vala:
|
|||||||
Verilog:
|
Verilog:
|
||||||
type: programming
|
type: programming
|
||||||
lexer: verilog
|
lexer: verilog
|
||||||
|
overrides:
|
||||||
|
- .v
|
||||||
extensions:
|
extensions:
|
||||||
- .v
|
- .v
|
||||||
|
|
||||||
|
|||||||
@@ -53,6 +53,7 @@ application/xaml+xml @xaml :8bit
|
|||||||
image/x-icns @icns
|
image/x-icns @icns
|
||||||
text/cache-manifest @manifest
|
text/cache-manifest @manifest
|
||||||
text/plain @cu,cxx
|
text/plain @cu,cxx
|
||||||
|
text/x-logtalk @lgt
|
||||||
text/x-nemerle @n
|
text/x-nemerle @n
|
||||||
text/x-nimrod @nim
|
text/x-nimrod @nim
|
||||||
text/x-ocaml @ml,mli,mll,mly,sig,sml
|
text/x-ocaml @ml,mli,mll,mly,sig,sml
|
||||||
|
|||||||
@@ -11,6 +11,6 @@ Gem::Specification.new do |s|
|
|||||||
s.add_dependency 'charlock_holmes', '~> 0.6.6'
|
s.add_dependency 'charlock_holmes', '~> 0.6.6'
|
||||||
s.add_dependency 'escape_utils', '~> 0.2.3'
|
s.add_dependency 'escape_utils', '~> 0.2.3'
|
||||||
s.add_dependency 'mime-types', '~> 1.16'
|
s.add_dependency 'mime-types', '~> 1.16'
|
||||||
s.add_dependency 'pygments.rb', '~> 0.2.3'
|
s.add_dependency 'pygments.rb', '~> 0.2.7'
|
||||||
s.add_development_dependency 'rake'
|
s.add_development_dependency 'rake'
|
||||||
end
|
end
|
||||||
|
|||||||
9
test/fixtures/foo.lgt
vendored
Normal file
9
test/fixtures/foo.lgt
vendored
Normal file
@@ -0,0 +1,9 @@
|
|||||||
|
% this is a Logtalk source file
|
||||||
|
|
||||||
|
:- object(hello_world).
|
||||||
|
|
||||||
|
% the initialization/1 directive argument is automatically executed
|
||||||
|
% when the object is loaded into memory:
|
||||||
|
:- initialization((nl, write('********** Hello World! **********'), nl)).
|
||||||
|
|
||||||
|
:- end_object.
|
||||||
2
test/fixtures/hello.ps1
vendored
Normal file
2
test/fixtures/hello.ps1
vendored
Normal file
@@ -0,0 +1,2 @@
|
|||||||
|
# Hello world in powershell
|
||||||
|
Write-Host 'Hello World'
|
||||||
5
test/fixtures/hello.psm1
vendored
Normal file
5
test/fixtures/hello.psm1
vendored
Normal file
@@ -0,0 +1,5 @@
|
|||||||
|
# Hello World powershell module
|
||||||
|
|
||||||
|
function hello() {
|
||||||
|
Write-Host 'Hello World'
|
||||||
|
}
|
||||||
419
test/fixtures/interval_discr.v
vendored
Normal file
419
test/fixtures/interval_discr.v
vendored
Normal file
@@ -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.
|
||||||
8
test/fixtures/latex.cls
vendored
Normal file
8
test/fixtures/latex.cls
vendored
Normal file
@@ -0,0 +1,8 @@
|
|||||||
|
% latex.cls
|
||||||
|
%
|
||||||
|
% A barebones LaTeX2e class file
|
||||||
|
|
||||||
|
\def\author{Abe Voelker}
|
||||||
|
\def\fileversion{0.1}
|
||||||
|
\NeedsTeXFormat{LaTeX2e}
|
||||||
|
|
||||||
10
test/fixtures/openedge.cls
vendored
Normal file
10
test/fixtures/openedge.cls
vendored
Normal file
@@ -0,0 +1,10 @@
|
|||||||
|
USING Progress.Lang.*.
|
||||||
|
|
||||||
|
CLASS HelloWorld:
|
||||||
|
|
||||||
|
CONSTRUCTOR PUBLIC HelloWorld():
|
||||||
|
SUPER().
|
||||||
|
MESSAGE "Hello, world!".
|
||||||
|
END CONSTRUCTOR.
|
||||||
|
|
||||||
|
END CLASS.
|
||||||
1
test/fixtures/openedge.p
vendored
Normal file
1
test/fixtures/openedge.p
vendored
Normal file
@@ -0,0 +1 @@
|
|||||||
|
MESSAGE "Hello, world!".
|
||||||
14
test/fixtures/scilab_function.sci
vendored
Normal file
14
test/fixtures/scilab_function.sci
vendored
Normal file
@@ -0,0 +1,14 @@
|
|||||||
|
// A comment with whites and tabulations
|
||||||
|
// Email: <scilab.support@scilab.org>
|
||||||
|
// Scilab editor: http://www.scilab.org/
|
||||||
|
function [a, b] = myfunction(d, e, f)
|
||||||
|
a = 2.71828 + %pi + f($, :);
|
||||||
|
b = cos(a) + cosh(a);
|
||||||
|
if d == e then
|
||||||
|
b = 10 - e.field;
|
||||||
|
else
|
||||||
|
b = " test " + home
|
||||||
|
return
|
||||||
|
end
|
||||||
|
myvar = 1.23e-45;
|
||||||
|
endfunction
|
||||||
2
test/fixtures/scilab_script.sce
vendored
Normal file
2
test/fixtures/scilab_script.sce
vendored
Normal file
@@ -0,0 +1,2 @@
|
|||||||
|
disp(%pi);
|
||||||
|
|
||||||
3
test/fixtures/scilab_test.tst
vendored
Normal file
3
test/fixtures/scilab_test.tst
vendored
Normal file
@@ -0,0 +1,3 @@
|
|||||||
|
assert_checkequal(1+1,2);
|
||||||
|
assert_checkfalse(%pi==%e);
|
||||||
|
|
||||||
86
test/fixtures/sha-256-functions.v
vendored
Normal file
86
test/fixtures/sha-256-functions.v
vendored
Normal file
@@ -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
|
||||||
|
|
||||||
|
|
||||||
@@ -274,6 +274,7 @@ class TestBlob < Test::Unit::TestCase
|
|||||||
assert_equal Language['C++'], blob("hello.cpp").language
|
assert_equal Language['C++'], blob("hello.cpp").language
|
||||||
assert_equal Language['C++'], blob("cuda.cu").language
|
assert_equal Language['C++'], blob("cuda.cu").language
|
||||||
assert_equal Language['GAS'], blob("hello.s").language
|
assert_equal Language['GAS'], blob("hello.s").language
|
||||||
|
assert_equal Language['Logtalk'], blob("foo.lgt").language
|
||||||
assert_equal Language['Objective-C'], blob("Foo.h").language
|
assert_equal Language['Objective-C'], blob("Foo.h").language
|
||||||
assert_equal Language['Objective-C'], blob("Foo.m").language
|
assert_equal Language['Objective-C'], blob("Foo.m").language
|
||||||
assert_equal Language['Objective-C'], blob("FooAppDelegate.h").language
|
assert_equal Language['Objective-C'], blob("FooAppDelegate.h").language
|
||||||
@@ -286,6 +287,10 @@ class TestBlob < Test::Unit::TestCase
|
|||||||
assert_equal Language['Arduino'], blob("hello.ino").language
|
assert_equal Language['Arduino'], blob("hello.ino").language
|
||||||
assert_nil blob("octocat.png").language
|
assert_nil blob("octocat.png").language
|
||||||
|
|
||||||
|
# .cls disambiguation
|
||||||
|
assert_equal Language['OpenEdge ABL'], blob("openedge.cls").language
|
||||||
|
assert_equal Language['TeX'], blob("latex.cls").language
|
||||||
|
|
||||||
# .pl disambiguation
|
# .pl disambiguation
|
||||||
assert_equal Language['Prolog'], blob("test-prolog.pl").language
|
assert_equal Language['Prolog'], blob("test-prolog.pl").language
|
||||||
assert_equal Language['Perl'], blob("test-perl.pl").language
|
assert_equal Language['Perl'], blob("test-perl.pl").language
|
||||||
@@ -305,11 +310,22 @@ class TestBlob < Test::Unit::TestCase
|
|||||||
assert_equal Language['Perl'], blob("perl-test.t").language
|
assert_equal Language['Perl'], blob("perl-test.t").language
|
||||||
assert_equal Language['Turing'], blob("turing.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
|
# ML
|
||||||
assert_equal Language['OCaml'], blob("Foo.ml").language
|
assert_equal Language['OCaml'], blob("Foo.ml").language
|
||||||
assert_equal Language['Standard ML'], blob("Foo.sig").language
|
assert_equal Language['Standard ML'], blob("Foo.sig").language
|
||||||
assert_equal Language['Standard ML'], blob("Foo.sml").language
|
assert_equal Language['Standard ML'], blob("Foo.sml").language
|
||||||
|
|
||||||
|
# Scilab
|
||||||
|
assert_equal Language['Scilab'], blob("scilab_script.sce").language
|
||||||
|
assert_equal Language['Scilab'], blob("scilab_function.sci").language
|
||||||
|
assert_equal Language['Scilab'], blob("scilab_test.tst").language
|
||||||
|
|
||||||
# Config files
|
# Config files
|
||||||
assert_equal Language['INI'], blob(".gitconfig").language
|
assert_equal Language['INI'], blob(".gitconfig").language
|
||||||
assert_equal Language['Shell'], blob(".bash_profile").language
|
assert_equal Language['Shell'], blob(".bash_profile").language
|
||||||
@@ -394,6 +410,9 @@ class TestBlob < Test::Unit::TestCase
|
|||||||
assert_equal Language['SCSS'], blob("screen.scss").language
|
assert_equal Language['SCSS'], blob("screen.scss").language
|
||||||
assert_equal Language['CSS'], blob("screen.scss").language.group
|
assert_equal Language['CSS'], blob("screen.scss").language.group
|
||||||
|
|
||||||
|
# OpenEdge ABL / Progress
|
||||||
|
assert_equal Language['OpenEdge ABL'], blob("openedge.p").language
|
||||||
|
|
||||||
# Tea
|
# Tea
|
||||||
assert_equal Language['Tea'], blob("foo.tea").language
|
assert_equal Language['Tea'], blob("foo.tea").language
|
||||||
end
|
end
|
||||||
|
|||||||
@@ -9,6 +9,9 @@ class TestLanguage < Test::Unit::TestCase
|
|||||||
Lexer = Pygments::Lexer
|
Lexer = Pygments::Lexer
|
||||||
|
|
||||||
def test_ambiguous_extensions
|
def test_ambiguous_extensions
|
||||||
|
assert Language.ambiguous?('.cls')
|
||||||
|
assert_equal Language['OpenEdge ABL'], Language.find_by_extension('cls')
|
||||||
|
|
||||||
assert Language.ambiguous?('.h')
|
assert Language.ambiguous?('.h')
|
||||||
assert_equal Language['C'], Language.find_by_extension('h')
|
assert_equal Language['C'], Language.find_by_extension('h')
|
||||||
|
|
||||||
@@ -23,6 +26,9 @@ class TestLanguage < Test::Unit::TestCase
|
|||||||
|
|
||||||
assert Language.ambiguous?('.t')
|
assert Language.ambiguous?('.t')
|
||||||
assert_equal Language['Perl'], Language.find_by_extension('t')
|
assert_equal Language['Perl'], Language.find_by_extension('t')
|
||||||
|
|
||||||
|
assert Language.ambiguous?('.v')
|
||||||
|
assert_equal Language['Verilog'], Language.find_by_extension('v')
|
||||||
end
|
end
|
||||||
|
|
||||||
def test_lexer
|
def test_lexer
|
||||||
@@ -34,6 +40,7 @@ class TestLanguage < Test::Unit::TestCase
|
|||||||
assert_equal Lexer['C'], Language['XS'].lexer
|
assert_equal Lexer['C'], Language['XS'].lexer
|
||||||
assert_equal Lexer['C++'], Language['C++'].lexer
|
assert_equal Lexer['C++'], Language['C++'].lexer
|
||||||
assert_equal Lexer['Coldfusion HTML'], Language['ColdFusion'].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['Fortran'], Language['FORTRAN'].lexer
|
||||||
assert_equal Lexer['Gherkin'], Language['Cucumber'].lexer
|
assert_equal Lexer['Gherkin'], Language['Cucumber'].lexer
|
||||||
assert_equal Lexer['HTML'], Language['HTML'].lexer
|
assert_equal Lexer['HTML'], Language['HTML'].lexer
|
||||||
@@ -49,6 +56,7 @@ class TestLanguage < Test::Unit::TestCase
|
|||||||
assert_equal Lexer['NASM'], Language['Assembly'].lexer
|
assert_equal Lexer['NASM'], Language['Assembly'].lexer
|
||||||
assert_equal Lexer['OCaml'], Language['F#'].lexer
|
assert_equal Lexer['OCaml'], Language['F#'].lexer
|
||||||
assert_equal Lexer['OCaml'], Language['OCaml'].lexer
|
assert_equal Lexer['OCaml'], Language['OCaml'].lexer
|
||||||
|
assert_equal Lexer['OpenEdge ABL'], Language['OpenEdge ABL'].lexer
|
||||||
assert_equal Lexer['Standard ML'], Language['Standard ML'].lexer
|
assert_equal Lexer['Standard ML'], Language['Standard ML'].lexer
|
||||||
assert_equal Lexer['Ooc'], Language['ooc'].lexer
|
assert_equal Lexer['Ooc'], Language['ooc'].lexer
|
||||||
assert_equal Lexer['REBOL'], Language['Rebol'].lexer
|
assert_equal Lexer['REBOL'], Language['Rebol'].lexer
|
||||||
@@ -63,6 +71,7 @@ class TestLanguage < Test::Unit::TestCase
|
|||||||
assert_equal Lexer['Scheme'], Language['Scheme'].lexer
|
assert_equal Lexer['Scheme'], Language['Scheme'].lexer
|
||||||
assert_equal Lexer['TeX'], Language['TeX'].lexer
|
assert_equal Lexer['TeX'], Language['TeX'].lexer
|
||||||
assert_equal Lexer['Text only'], Language['Text'].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['aspx-vb'], Language['ASP'].lexer
|
||||||
assert_equal Lexer['haXe'], Language['HaXe'].lexer
|
assert_equal Lexer['haXe'], Language['HaXe'].lexer
|
||||||
assert_equal Lexer['reStructuredText'], Language['reStructuredText'].lexer
|
assert_equal Lexer['reStructuredText'], Language['reStructuredText'].lexer
|
||||||
@@ -99,7 +108,11 @@ class TestLanguage < Test::Unit::TestCase
|
|||||||
assert_equal Language['JavaScript'], Language.find_by_alias('js')
|
assert_equal Language['JavaScript'], Language.find_by_alias('js')
|
||||||
assert_equal Language['Literate Haskell'], Language.find_by_alias('lhs')
|
assert_equal Language['Literate Haskell'], Language.find_by_alias('lhs')
|
||||||
assert_equal Language['Literate Haskell'], Language.find_by_alias('literate-haskell')
|
assert_equal Language['Literate Haskell'], Language.find_by_alias('literate-haskell')
|
||||||
|
assert_equal Language['OpenEdge ABL'], Language.find_by_alias('openedge')
|
||||||
|
assert_equal Language['OpenEdge ABL'], Language.find_by_alias('progress')
|
||||||
|
assert_equal Language['OpenEdge ABL'], Language.find_by_alias('abl')
|
||||||
assert_equal Language['Parrot Internal Representation'], Language.find_by_alias('pir')
|
assert_equal Language['Parrot Internal Representation'], Language.find_by_alias('pir')
|
||||||
|
assert_equal Language['Powershell'], Language.find_by_alias('posh')
|
||||||
assert_equal Language['Puppet'], Language.find_by_alias('puppet')
|
assert_equal Language['Puppet'], Language.find_by_alias('puppet')
|
||||||
assert_equal Language['Pure Data'], Language.find_by_alias('pure-data')
|
assert_equal Language['Pure Data'], Language.find_by_alias('pure-data')
|
||||||
assert_equal Language['Raw token data'], Language.find_by_alias('raw')
|
assert_equal Language['Raw token data'], Language.find_by_alias('raw')
|
||||||
@@ -183,6 +196,7 @@ class TestLanguage < Test::Unit::TestCase
|
|||||||
def test_programming
|
def test_programming
|
||||||
assert_equal :programming, Language['JavaScript'].type
|
assert_equal :programming, Language['JavaScript'].type
|
||||||
assert_equal :programming, Language['Perl'].type
|
assert_equal :programming, Language['Perl'].type
|
||||||
|
assert_equal :programming, Language['Powershell'].type
|
||||||
assert_equal :programming, Language['Python'].type
|
assert_equal :programming, Language['Python'].type
|
||||||
assert_equal :programming, Language['Ruby'].type
|
assert_equal :programming, Language['Ruby'].type
|
||||||
end
|
end
|
||||||
@@ -235,6 +249,8 @@ class TestLanguage < Test::Unit::TestCase
|
|||||||
assert_equal Language['PHP'], Language.find_by_extension('php3')
|
assert_equal Language['PHP'], Language.find_by_extension('php3')
|
||||||
assert_equal Language['PHP'], Language.find_by_extension('php4')
|
assert_equal Language['PHP'], Language.find_by_extension('php4')
|
||||||
assert_equal Language['PHP'], Language.find_by_extension('php5')
|
assert_equal Language['PHP'], Language.find_by_extension('php5')
|
||||||
|
assert_equal Language['Powershell'], Language.find_by_extension('psm1')
|
||||||
|
assert_equal Language['Powershell'], Language.find_by_extension('ps1')
|
||||||
assert_nil Language.find_by_extension('.kt')
|
assert_nil Language.find_by_extension('.kt')
|
||||||
end
|
end
|
||||||
|
|
||||||
@@ -275,6 +291,15 @@ class TestLanguage < Test::Unit::TestCase
|
|||||||
assert_equal 'Ruby', Language['Ruby'].name
|
assert_equal 'Ruby', Language['Ruby'].name
|
||||||
end
|
end
|
||||||
|
|
||||||
|
def test_escaped_name
|
||||||
|
assert_equal 'C', Language['C'].escaped_name
|
||||||
|
assert_equal 'C%23', Language['C#'].escaped_name
|
||||||
|
assert_equal 'C%2B%2B', Language['C++'].escaped_name
|
||||||
|
assert_equal 'Objective-C', Language['Objective-C'].escaped_name
|
||||||
|
assert_equal 'Common%20Lisp', Language['Common Lisp'].escaped_name
|
||||||
|
assert_equal 'Max%2FMSP', Language['Max/MSP'].escaped_name
|
||||||
|
end
|
||||||
|
|
||||||
def test_error_without_name
|
def test_error_without_name
|
||||||
assert_raise ArgumentError do
|
assert_raise ArgumentError do
|
||||||
Language.new :name => nil
|
Language.new :name => nil
|
||||||
|
|||||||
@@ -62,6 +62,7 @@ class TestMime < Test::Unit::TestCase
|
|||||||
assert_equal 'text/plain', Mime.mime_for('.hh')
|
assert_equal 'text/plain', Mime.mime_for('.hh')
|
||||||
assert_equal 'text/plain', Mime.mime_for('.hpp')
|
assert_equal 'text/plain', Mime.mime_for('.hpp')
|
||||||
assert_equal 'text/plain', Mime.mime_for('.kt')
|
assert_equal 'text/plain', Mime.mime_for('.kt')
|
||||||
|
assert_equal 'text/x-logtalk', Mime.mime_for('.lgt')
|
||||||
assert_equal 'text/x-rust', Mime.mime_for('.rs')
|
assert_equal 'text/x-rust', Mime.mime_for('.rs')
|
||||||
assert_equal 'text/x-rust', Mime.mime_for('.rc')
|
assert_equal 'text/x-rust', Mime.mime_for('.rc')
|
||||||
assert_equal 'video/quicktime', Mime.mime_for('.mov')
|
assert_equal 'video/quicktime', Mime.mime_for('.mov')
|
||||||
|
|||||||
Reference in New Issue
Block a user