diff --git a/docs/Languages.md b/docs/Languages.md index 5e72a98acf..c28de9c0c8 100644 --- a/docs/Languages.md +++ b/docs/Languages.md @@ -9,6 +9,7 @@ - ABAP (`abap`) - ActionScript (`actionscript`) - Ada (`ada`) +- Agda (`agda`) - Apache (`apache`) - Apex (`apex`) - API Blueprint (`apiblueprint`) diff --git a/lib/rouge/demos/agda b/lib/rouge/demos/agda new file mode 100644 index 0000000000..2497a0c9d7 --- /dev/null +++ b/lib/rouge/demos/agda @@ -0,0 +1,8 @@ +-- The type of natural numbers. +data Nat : Set where + zero : Nat + succ : Nat → Nat + +_+_ : Nat → Nat → Nat +zero + n = n +succ m + n = succ (m + n) diff --git a/lib/rouge/lexers/agda.rb b/lib/rouge/lexers/agda.rb new file mode 100644 index 0000000000..a243e60900 --- /dev/null +++ b/lib/rouge/lexers/agda.rb @@ -0,0 +1,181 @@ +# -*- coding: utf-8 -*- # +# frozen_string_literal: true + +module Rouge + module Lexers + class Agda < RegexLexer + title "Agda" + desc "The Agda programming language and proof assistant" + tag "agda" + filenames "*.agda" + mimetypes "text/x-agda" + + # Primary reference: https://github.com/agda/agda/blob/master/src/full/Agda/Syntax/Parser/Lexer.x + + PRAGMAS = Set.new %w( + CATCHALL COMPILE FOREIGN DISPLAY ETA ETA_EQUALITY IMPOSSIBLE + INJECTIVE INJECTIVE_FOR_INFERENCE INLINE INCOHERENT NOINLINE + NOT_PROJECTION_LIKE LINE MEASURE NO_POSITIVITY_CHECK + NO_TERMINATION_CHECK NO_UNIVERSE_CHECK NON_COVERING NON_TERMINATING + OPTIONS OVERLAPPABLE OVERLAPPING OVERLAPS POLARITY REWRITE STATIC + TERMINATING WARNING_ON_USAGE WARNING_ON_IMPORT + ) + + # These exclude the reflection builtins because there are too many + # See https://agda.readthedocs.io/en/latest/language/reflection.html + BUILTINS = Set.new %w( + UNIT SIGMA LIST MAYBE BOOL TRUE FALSE NATURAL NATPLUS NATMINUS NATTIMES + NATEQUALS NATLESS NATDIVSUCAUX NATMODSUCAUX WORD64 INTEGER INTEGERPOS + INTERGERNEGSUC FLOAT CHAR STRING EQUALITY TYPE PROP SETOMEGA LEVEL + LEVELZERO LEVELSUC LEVELMAX SIZEUNIV SIZE SIZELT SIZESUC SIZEINF + SIZEMAX INFINITY SHARP FLAT IO REWRITE FROMNAT FROMNEG FROMSTRING + ) + + RESERVED = Set.new %w( + abstract codata coinductive constructor data do eta-equality field + forall import in inductive infix infixl infixr instance interleaved let + macro module mutual no-eta-equality open overlap pattern postulate + primitive private quote quoteTerm record rewrite syntax tactic unquote + unquoteDecl unquoteDef variable where with opaque unfolding + using hiding renaming to public + ) + + ESCAPES = %r/ + a | b | f | n | r | t | v | + NUL | SOH | STX | ETX | EOT | ENQ | ACK | BEL | BS | HT | LF | VT | + FF | CR | SO | SI | DLE | DC1 | DC2 | DC3 | DC4 | NAK | SYN | ETB | + CAN | EM | SUB | ESC | FS | GS | RS | US | SP | DEL | + \^[@-_] | x\h+ | o[0-7]+ | \d+ | \\ + /x + + state :root do + # Line comments can stick behind some punctuation + rule %r/(^|[\(\)\}\.;])(--.*)$/ do + groups Punctuation, Comment + end + + # Otherwise, line comments follow spaces + rule %r/(\s+)(--.*)$/ do + groups Text, Comment + end + + # Builtin pragmas + rule %r/({-#\s*)(BUILTIN)(\s+)/ do + groups Comment::Preproc, Keyword::Pseudo, Comment::Preproc + push :builtin + end + + # Other pragmas and block comments + rule %r/{-#\s*/, Comment::Preproc, :pragma + rule %r/{-/, Comment::Multiline, :comment + rule %r/{!/, Comment::Special, :hole + + # Agda primitives (see https://agda.github.io/agda-stdlib/master/Agda.Primitive.html) + # Builtins can be renamed so there's no point lexing them all specially, + # but the sorts are predefined rather than postulated somewhere + rule %r/\b(LevelUniv)\b/, Keyword::Type + rule %r/\b(S?Set|Prop)(ω|[₀₁₂₃₄₅₆₇₈₉]*)/, Keyword::Type + + # Attributes + rule %r/@flat|@♭|@⊤/, Name::Attribute + rule %r/(@)(\()(tactic)/ do + groups Name::Attribute, Punctuation, Name::Attribute + end + + # Punctuation, including idiom brackets, instance arguments + # The way that ..., .., and . are handled could be more refined + # Should unmatched parentheses, braces, and brackets be lexical errors? + rule %r/[\(\)\{\}\.;]/, Punctuation + rule %r/\(\|\)/, Punctuation + rule %r/(\(\|)(\s+)/ do + groups Punctuation, Text + end + rule %r/(\s+)(\|\))/ do + groups Text, Punctuation + end + rule %r/(\s+)[⦇⦈⦃⦄](\s+)/ do + groups Text, Punctuation, Text + end + + # Numbers + rule %r/-?0x\h+(_\h+)*\b/, Num::Hex + rule %r/-?0b[01]+(_[01]+)*\b/, Num::Hex + rule %r/-?\d+(\.\d+)?[eE][+-]?\d+\b/, Num::Float + rule %r/-?\d+(_\d+)*\b/, Num::Integer + + # Characters and strings with escape codes + rule %r/'/, Str::Char, :char + rule %r/"/, Str, :string + + # Keywords + keywords %r/\w+/ do + rule RESERVED, Keyword::Reserved + default Name + end + + # Special operators with characters that could appear in regular names + # require spaces after them to distinguish them from names + # No name can begin with a lambda, and @ is disallowed in names + rule %r/λ|\\|@/, Operator + rule %r/(->|<-|[∀→←⊔=:_\|\?])(\s+)/ do + groups Operator, Text + end + + rule %r/[^\s\(\)\{\}\.\;\@]+/, Name + rule %r/\s+/, Text + end + + state :builtin do + keywords %r/\w+/ do + rule BUILTINS do + token Keyword::Pseudo + goto :pragma_end + end + default Error + end + end + + state :pragma do + keywords %r/\w+/ do + rule PRAGMAS do + token Keyword::Pseudo + goto :pragma_end + end + default Error + end + end + + # Pragmas aren't nested + state :pragma_end do + rule %r/[^#]+/, Comment::Preproc + rule %r/#-}/, Comment::Preproc, :pop! + rule %r/./, Comment::Preproc + end + + state :comment do + rule %r/[^{-]+/, Comment::Multiline + rule %r/-}/, Comment::Multiline, :pop! + rule %r/{-/, Comment::Multiline, :comment + rule %r/./, Comment::Multiline + end + + state :hole do + rule %r/[^{!]+/, Comment::Special + rule %r/!}/, Comment::Special, :pop! + rule %r/{!/, Comment::Special, :hole + rule %r/./, Comment::Special + end + + state :char do + rule %r/\\(#{ESCAPES}|')'/, Str::Escape, :pop! + rule %r/.'/, Str::Char, :pop! + end + + state :string do + rule %r/[^"\\]+/, Str + rule %r/\\(#{ESCAPES}|")/, Str::Escape + rule %r/"/, Str, :pop! + end + end + end +end diff --git a/spec/lexers/agda_spec.rb b/spec/lexers/agda_spec.rb new file mode 100644 index 0000000000..59bd6f2258 --- /dev/null +++ b/spec/lexers/agda_spec.rb @@ -0,0 +1,18 @@ +# -*- coding: utf-8 -*- # +# frozen_string_literal: true + +describe Rouge::Lexers::Agda do + let(:subject) { Rouge::Lexers::Agda.new } + + describe 'guessing' do + include Support::Guessing + + it 'guesses by filename' do + assert_guess :filename => 'foo.agda' + end + + it 'guesses by mimetype' do + assert_guess :mimetype => 'text/x-agda' + end + end +end diff --git a/spec/visual/samples/agda b/spec/visual/samples/agda new file mode 100644 index 0000000000..f081f2fab0 --- /dev/null +++ b/spec/visual/samples/agda @@ -0,0 +1,117 @@ +{-# OPTIONS --prop #-} +{-# OPTIONS # #- # #-} + +module agda where + +open import Level +open import Agda.Primitive + +postulate + MyLevel : LevelUniv +{-# BUILTIN LEVEL MyLevel #-} + +data Id {ℓ : Level} (A : Set ℓ) : A → A → Set ℓ where + refl : (x : A) → Id A x x + +syntax Id A x y = x =[ A ] y + +variable + ℓ ℓ′ : Level + +-- Symmetry of equality. +sym : {A : Set ℓ} {x y : A} → x =[ A ] y → y =[ A ] x +sym (refl x) = refl x + +-- Transitivity of equality. +trans : {A : Set ℓ} {x y z : A} → x =[ A ] y → y =[ A ] z → x =[ A ] z +trans (refl x) (refl x) = refl x + +-- Equality is a congruence. +cong : {A : Set ℓ} {B : Set ℓ′} {x y : A} → (f : A → B) → x =[ A ] y → f x =[ B ] f y +cong f (refl x) = refl (f x) + +data ℕ : Set where + Z : ℕ + S : ℕ → ℕ +{-# BUILTIN NATURAL ℕ #-} + +_+_ : ℕ → ℕ → ℕ +Z + n = n +S m + n = S (m + n) +{-# BUILTIN NATPLUS _+_ #-} + +big--minus : ℕ → ℕ → ℕ +big--minus = ? + +-- Left identity for addition. ++-left-id : (n : ℕ) → (Z + n) =[ ℕ ] n ++-left-id n = {! refl ! {{!! n !!}} ! } !} + +-- Right identity for addition. ++-right-id : (n : ℕ) → (n + Z) =[ ℕ ] n ++-right-id Z = refl Z ++-right-id _@(S n) = cong S (+-right-id n) + +-- Associativity of addition. +-- Make sure that the ∀ notation is lexed correctly as well. ++-assoc : ∀ m n o → ((m + n) + o) =[ ℕ ] (m + (n + o)) ++-assoc Z n o = refl (n + o) ++-assoc (S m) n o = cong S (+-assoc m n o) + +idP : ∀ {A : SProp} → A → A +idP {_} = λx → x + +{- Large identity function + The type of the argument is left implicit. -} +identity : ∀ {A : Setω} → A → A +identity = λ { x → x } -- a pattern lambda + + -- This is a comment with indented space. + +compare : Nat → Nat → Comparison +compare x y with x < y +... | false with y < x +... | false = equal +... | true = greater +compare x y | true = less + +module _ (A B : Set) (recompute : .B → .{{A}} → B) where + + _$_ : .(A → B) → .A → B + f $ x with .{f} | .(f x) | .{{x}} + ... | y = recompute y + +defaultTo : {A : Set} (x : A) → Term → TC ⊤ +defaultTo x hole = bindTC (quoteTC x) (unify hole) + +record Bools : SSet₁₈₄₄₆₇₄₄₀₇₃₇₀₉₅₅₁₆₁₅ where + constructor mkBools + field fst : Bool + @(tactic defaultTo fst)-- If `snd` is not provided, set it to `fst`. + {snd} : Bool +open Bools + +data ♭ {@♭ l : Level} (@♭ A : Set l) : Set l where + con : (@♭ x : A) → ♭ A + +some-numbers = [ + 0xdEAd_bEEf, + -0xf0ccac1a, + 0b0_1_0_1_0, + -6.02214076e+23, + 1_000_000 +] + +some-chars = [ + '\x237C', + '\b', + '\BEL', + '\'', + '"', +] + +some-strings = [ + "", + "\BEL is the same as \^G is the same as \a is the same as \x07 is the same as \o07", + "\"'\"'\"" +]