initial support for lean 3 (rouge-ruby#1798)

* initial support for lean 3 * incorporate keywords and operators from PR rouge-ruby#1019 * address comments * add keyword::type + other keywords
ole · Mar 5, 2022 · 776cbc4 · 776cbc4
1 parent df4477e
commit 776cbc4
Show file tree

Hide file tree

Showing 4 changed files with 289 additions and 0 deletions.
diff --git a/lib/rouge/demos/lean b/lib/rouge/demos/lean
@@ -0,0 +1,8 @@
+open nat
+
+def add : nat → nat → nat
+| m zero := m
+| m (succ n) := succ (add m n)
+
+-- encode definition as an axiom
+axiom add_zero (n : nat) : n + 0 = n
diff --git a/lib/rouge/lexers/lean.rb b/lib/rouge/lexers/lean.rb
@@ -0,0 +1,164 @@
+# -*- coding: utf-8 -*- #
+# frozen_string_literal: true
+
+# NOTE: This is for Lean 3 (community fork).
+module Rouge
+  module Lexers
+    class Lean < RegexLexer
+      title 'Lean'
+      desc 'The Lean programming language (leanprover.github.io)'
+      tag 'lean'
+      aliases 'lean'
+      filenames '*.lean'
+
+      def self.keywords
+        @keywords ||= Set.new %w(
+          abbreviation
+          add_rewrite
+          alias
+          assume
+          axiom
+          begin
+          by
+          calc
+          calc_refl
+          calc_subst
+          calc_trans
+          #check
+          coercion
+          conjecture
+          constant
+          constants
+          context
+          corollary
+          def
+          definition
+          end
+          #eval
+          example
+          export
+          expose
+          exposing
+          exit
+          extends
+          from
+          fun
+          have
+          help
+          hiding
+          hott
+          hypothesis
+          import
+          include
+          including
+          inductive
+          infix
+          infixl
+          infixr
+          inline
+          instance
+          irreducible
+          lemma
+          match
+          namespace
+          notation
+          opaque
+          opaque_hint
+          open
+          options
+          parameter
+          parameters
+          postfix
+          precedence
+          prefix
+          #print
+          private
+          protected
+          #reduce
+          reducible
+          renaming
+          repeat
+          section
+          set_option
+          show
+          tactic_hint
+          theorem
+          universe
+          universes
+          using
+          variable
+          variables
+          with
+        )
+      end
+
+      def self.types
+        @types ||= %w(
+          Sort
+          Prop
+          Type
+        )
+      end
+
+      def self.operators
+        @operators ||= %w(
+          != # & && \* \+ - / @ ! ` -\. ->
+          \. \.\. \.\.\. :: :> ; ;; <
+          <- = == > _ \| \|\| ~ => <= >=
+          /\ \/ ∀ Π λ ↔ ∧ ∨ ≠ ≤ ≥ ⊎
+          ¬ ⁻¹ ⬝ ▸ → ∃ ℕ ℤ ≈ × ⌞ ⌟ ≡ ⟨ ⟩
+        )
+      end
+
+      state :root do
+        # comments starting after some space
+        rule %r/\s*--+\s+.*?$/, Comment::Doc
+
+        rule %r/"/, Str, :string
+        rule %r/\d+/, Num::Integer
+
+        # special commands or keywords
+        rule(/#?\w+/) do |m|
+          match = m[0]
+          if self.class.keywords.include?(match)
+            token Keyword
+          elsif self.class.types.include?(match)
+            token Keyword::Type
+          else
+            token Name
+          end
+        end
+
+        # special unicode keywords
+        rule %r/[λ]/, Keyword
+
+        # ----------------
+        # operators rules
+        # ----------------
+
+        rule %r/\:=?/, Text
+        rule %r/\.[0-9]*/, Operator
+
+        rule %r(#{Lean.operators.join('|')}), Operator
+
+        # unmatched symbols
+        rule %r/[\s\(\),\[\]αβ‹›]+/, Text
+
+        # show missing matches
+        rule %r/./, Error
+
+      end
+
+      state :string do
+        rule %r/"/, Str, :pop!
+        rule %r/\\/, Str::Escape, :escape
+        rule %r/[^\\"]+/, Str
+      end
+
+      state :escape do
+        rule %r/[nrt"'\\]/, Str::Escape, :pop!
+        rule %r/x[\da-f]+/i, Str::Escape, :pop!
+      end
+    end
+  end
+end
diff --git a/spec/lexers/lean_spec.rb b/spec/lexers/lean_spec.rb
@@ -0,0 +1,15 @@
+# -*- coding: utf-8 -*- #
+# frozen_string_literal: true
+
+describe Rouge::Lexers::Lean do
+  let(:subject) { Rouge::Lexers::Lean.new }
+
+  describe 'guessing' do
+    include Support::Guessing
+
+    it 'guesses by filename' do
+      assert_guess :filename => 'file.lean'
+    end
+
+  end
+end
diff --git a/spec/visual/samples/lean b/spec/visual/samples/lean
@@ -0,0 +1,102 @@
+import data.nat.basic
+
+namespace sandbox
+
+@[derive decidable_eq]
+inductive Nat
+    | zero : Nat
+    | succ (n : Nat) : Nat
+
+open Nat
+
+-- instance
+instance : has_zero Nat := ⟨zero⟩
+
+axiom zero_is_nat : zero = 0
+
+def add : Nat → Nat → Nat
+| m 0 := m
+| m (succ n) := succ (add m n)
+
+-- Defines the + operator
+instance : has_add Nat := ⟨add⟩
+
+axiom add_zero (n : Nat) : n + 0 = n
+axiom add_succ (m n: Nat) : m + succ n = succ (m + n)
+
+lemma zero_add (n : Nat) : 0 + n = n :=
+  begin
+  induction n with d hd,
+
+  -- base
+  rw zero_is_nat,
+  rw add_zero,
+
+  -- inductive step
+  rw add_succ,
+  rw hd,
+  end
+
+-- alternative to →
+#check Nat -> Nat
+
+universe u
+
+constant list   : Type u → Type u
+constant cons   : Π α : Type u, α → list α → list α
+
+variable α : Type
+variable β : α → Type
+variable a : α
+variable b : β a
+
+#check sigma.mk a b      -- Σ (a : α), β a
+#check (sigma.mk a b).1  -- α
+#check (sigma.mk a b).2  -- β (sigma.fst (sigma.mk a b))
+
+-- show ... from ...
+constants p q : Prop
+
+lemma t1 : p → q → p :=
+assume hp : p,
+assume hq : q,
+show p, from hp
+
+#check p → q → p ∧ q
+#check ¬p → p ↔ false
+#check p ∨ q → q ∨ p
+
+#eval "String"
+#eval string.join ["\"Hello",  "\n", "World\""]
+#eval "\xF0" -- "ð"
+
+--------------------------
+-- Calculational Proofs --
+--------------------------
+
+import data.nat.basic
+
+variables (a b c d e : ℕ)
+variable h1 : a = b
+variable h2 : b = c + 1
+variable h3 : c = d
+variable h4 : e = 1 + d
+
+include h1 h2 h3 h4
+theorem T : a = e :=
+calc
+  a     = d + 1  : by rw [h1, h2, h3]
+    ... = 1 + d  : by rw add_comm
+    ... = e      : by rw h4
+
+end sandbox
+
+--------------------------------
+-- The Existential Quantifier --
+--------------------------------
+
+example : ∃ x : ℕ, x > 0 :=
+have h : 1 > 0, from zero_lt_succ 0,
+exists.intro 1 h
+
+notation `‹` p `›` := show p, by assumption