diff options
author | Tim Baumann <tim@timbaumann.info> | 2013-05-19 20:58:32 +0200 |
---|---|---|
committer | Tim Baumann <tim@timbaumann.info> | 2013-05-19 20:58:32 +0200 |
commit | 91aeb371752f8c10dda0bbc156452bcb6839bd21 (patch) | |
tree | 6b92995e96056519efe0492ae1764c4e95d57eb1 | |
parent | bc00600db992c277770fd3651e8a49aca4b58303 (diff) | |
download | pygments-91aeb371752f8c10dda0bbc156452bcb6839bd21.tar.gz |
Test files for Agda and literate Agda mode
-rw-r--r-- | pygments/lexers/functional.py | 19 | ||||
-rw-r--r-- | tests/examplefiles/example.lagda | 19 | ||||
-rw-r--r-- | tests/examplefiles/test.agda | 102 |
3 files changed, 133 insertions, 7 deletions
diff --git a/pygments/lexers/functional.py b/pygments/lexers/functional.py index 41aac7a4..edd139c1 100644 --- a/pygments/lexers/functional.py +++ b/pygments/lexers/functional.py @@ -1107,11 +1107,12 @@ class AgdaLexer(RegexLexer): filenames = ['*.agda'] mimetypes = ['text/x-agda'] - reserved = ['abstract', 'codata', 'coinductive', 'data', 'field', - 'forall', 'hiding', 'in', 'inductive', 'infix', 'infixl', - 'infixr', 'let', 'open', 'pattern', 'primitive', 'private', - 'mutual', 'quote', 'quoteGoal', 'quoteTerm', 'record', - 'syntax', 'rewrite', 'unquote', 'using', 'where', 'with'] + reserved = ['abstract', 'codata', 'coinductive', 'constructor', 'data', + 'field', 'forall', 'hiding', 'in', 'inductive', 'infix', + 'infixl', 'infixr', 'let', 'open', 'pattern', 'primitive', + 'private', 'mutual', 'quote', 'quoteGoal', 'quoteTerm', + 'record', 'syntax', 'rewrite', 'unquote', 'using', 'where', + 'with'] tokens = { 'root': [ @@ -1125,8 +1126,7 @@ class AgdaLexer(RegexLexer): # Lexemes: # Identifiers (ur'\b(%s)(?!\')\b' % '|'.join(reserved), Keyword.Reserved), - (r'(import)(\s+)([A-Z][a-zA-Z0-9_.]*)', bygroups(Keyword.Reserved, Text, Name)), - (r'(module)(\s+)([A-Z][a-zA-Z0-9_.]*)', bygroups(Keyword.Reserved, Text, Name)), + (r'(import|module)(\s+)', bygroups(Keyword.Reserved, Text), 'module'), (r'\b(Set|Prop)\b', Keyword.Type), # Special Symbols (r'(\(|\)|\{|\})', Operator), @@ -1156,6 +1156,11 @@ class AgdaLexer(RegexLexer): (r'!}', Comment.Directive, '#pop'), (r'[!{}]', Comment.Directive), ], + 'module': [ + (r'{-', Comment.Multiline, 'comment'), + (r'[a-zA-Z][a-zA-Z0-9_.]*', Name, '#pop'), + (r'[^a-zA-Z]*', Text) + ], 'character': HaskellLexer.tokens['character'], 'string': HaskellLexer.tokens['string'], 'escape': HaskellLexer.tokens['escape'] diff --git a/tests/examplefiles/example.lagda b/tests/examplefiles/example.lagda new file mode 100644 index 00000000..b5476fa0 --- /dev/null +++ b/tests/examplefiles/example.lagda @@ -0,0 +1,19 @@ +\documentclass{article} +% this is a LaTeX comment +\usepackage{agda} + +\begin{document} + +Here's how you can define \emph{RGB} colors in Agda: + +\begin{code} +module example where + +open import Data.Fin +open import Data.Nat + +data Color : Set where + RGB : Fin 256 → Fin 256 → Fin 256 → Color +\end{code} + +\end{document}
\ No newline at end of file diff --git a/tests/examplefiles/test.agda b/tests/examplefiles/test.agda new file mode 100644 index 00000000..d930a77b --- /dev/null +++ b/tests/examplefiles/test.agda @@ -0,0 +1,102 @@ +-- An Agda example file + +module test where + +open import Coinduction +open import Data.Bool +open import {- pointless comment between import and module name -} Data.Char +open import Data.Nat +open import Data.Nat.Properties +open import Data.String +open import Data.List hiding ([_]) +open import Data.Vec hiding ([_]) +open import Relation.Nullary.Core +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; trans; inspect; [_]) + +open SemiringSolver + +{- this is a {- nested -} comment -} + +-- Factorial +_! : ℕ → ℕ +0 ! = 1 +(suc n) ! = (suc n) * n ! + +-- The binomial coefficient +_choose_ : ℕ → ℕ → ℕ +_ choose 0 = 1 +0 choose _ = 0 +(suc n) choose (suc m) = (n choose m) + (n choose (suc m)) -- Pascal's rule + +choose-too-many : ∀ n m → n ≤ m → n choose (suc m) ≡ 0 +choose-too-many .0 m z≤n = refl +choose-too-many (suc n) (suc m) (s≤s le) with n choose (suc m) | choose-too-many n m le | n choose (suc (suc m)) | choose-too-many n (suc m) (≤-step le) +... | .0 | refl | .0 | refl = refl + +_++'_ : ∀ {a n m} {A : Set a} → Vec A n → Vec A m → Vec A (m + n) +_++'_ {_} {n} {m} v₁ v₂ rewrite solve 2 (λ a b → b :+ a := a :+ b) refl n m = v₁ Data.Vec.++ v₂ + +++'-test : (1 ∷ 2 ∷ 3 ∷ []) ++' (4 ∷ 5 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []) +++'-test = refl + +data Coℕ : Set where + co0 : Coℕ + cosuc : ∞ Coℕ → Coℕ + +nanana : Coℕ +nanana = let two = ♯ cosuc (♯ (cosuc (♯ co0))) in cosuc two + +abstract + data VacuumCleaner : Set where + Roomba : VacuumCleaner + +pointlessLemmaAboutBoolFunctions : (f : Bool → Bool) → f (f (f true)) ≡ f true +pointlessLemmaAboutBoolFunctions f with f true | inspect f true +... | true | [ eq₁ ] = trans (cong f eq₁) eq₁ +... | false | [ eq₁ ] with f false | inspect f false +... | true | _ = eq₁ +... | false | [ eq₂ ] = eq₂ + +mutual + isEven : ℕ → Bool + isEven 0 = true + isEven (suc n) = not (isOdd n) + + isOdd : ℕ → Bool + isOdd 0 = false + isOdd (suc n) = not (isEven n) + +foo : String +foo = "Hello World!" + +nl : Char +nl = '\n' + +private + intersperseString : Char → List String → String + intersperseString c [] = "" + intersperseString c (x ∷ xs) = Data.List.foldl (λ a b → a Data.String.++ Data.String.fromList (c ∷ []) Data.String.++ b) x xs + +baz : String +baz = intersperseString nl (Data.List.replicate 5 foo) + +postulate + Float : Set + +{-# BUILTIN FLOAT Float #-} + +pi : Float +pi = 3.141593 + +-- Astronomical unit +au : Float +au = 1.496e11 -- m + +plusFloat : Float → Float → Float +plusFloat a b = {! !} + +record Subset (A : Set) (P : A → Set) : Set where + constructor _#_ + field + elem : A + .proof : P elem |