Lexer for Agda

docs/Languages.md

@@ -9,6 +9,7 @@
 - ABAP (`abap`)
 - ActionScript (`actionscript`)
 - Ada (`ada`)
+- Agda (`agda`)
 - Apache (`apache`)
 - Apex (`apex`)
 - API Blueprint (`apiblueprint`)

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)

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

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

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",
+  "\"'\"'\""
+]