Coq unicode improvements

lib/rouge/lexers/coq.rb

@@ -25,7 +25,7 @@ def self.coq
           Variables Class Instance Global Local Include
           Printing Notation Infix Arguments Hint Rewrite Immediate
           Qed Defined Opaque Transparent Existing
-          Compute Eval Print SearchAbout Search About Check
+          Compute Eval Print SearchAbout Search About Check Admitted
         )
       end
 
@@ -56,12 +56,6 @@ def self.terminators
         )
       end
 
-      def self.keyopts
-        @keyopts ||= Set.new %w(
-          := => -> /\\ \\/ _ ; :> : ⇒ → ↔ ⇔ ≔ ≡ ∀ ∃ ∧ ∨ ¬ ⊤ ⊥ ⊢ ⊨ ∈
-        )
-      end
-
       def self.end_sentence
         @end_sentence ||= Punctuation::Indicator
       end
@@ -82,16 +76,96 @@ def self.classify(x)
         end
       end
 
-      operator = %r([\[\];,{}_()!$%&*+./:<=>?@^|~#-]+)
-      id = /(?:[a-z][\w']*)|(?:[_a-z][\w']+)/i
-      dot_id = /\.((?:[a-z][\w']*)|(?:[_a-z][\w']+))/i
+      # https://github.com/coq/coq/blob/110921a449fcb830ec2a1cd07e3acc32319feae6/clib/unicode.ml#L67
+      # https://coq.inria.fr/refman/language/core/basic.html#grammar-token-ident
+      id_first = /\p{L}/
+      id_first_underscore = /(?:\p{L}|_)/
+      id_subsequent = /(?:\p{L}|\p{N}|_|')/ # a few missing? some mathematical ' primes and subscripts
+      id = /(?:#{id_first}#{id_subsequent}*)|(?:#{id_first_underscore}#{id_subsequent}+)/i
+      dot_id = /\.(#{id})/i
       dot_space = /\.(\s+)/
+      proof = /Proof(\s*).(\s+)/i
+      qed = /(Qed|Defined|Save|Admitted)(\s*).(\s+)/i
       module_type = /Module(\s+)Type(\s+)/
       set_options = /(Set|Unset)(\s+)(Universe|Printing|Implicit|Strict)(\s+)(Polymorphism|All|Notations|Arguments|Universes|Implicit)(\s*)\./m
 
       state :root do
-        rule %r/[(][*](?![)])/, Comment, :comment
+        mixin :begin_proof
+        mixin :sentence
+      end
+
+      state :sentence do
+        mixin :comment_whitespace
+        mixin :module_setopts
+        # After parsing the id, end up in sentence_postid
+        rule id do |m|
+          @name = m[0]
+          @id_dotted = false
+          push :sentence_postid
+          push :continue_id
+        end
+      end
+
+      state :begin_proof do
+        rule proof do |m|
+          token Keyword, "Proof"
+          token Text::Whitespace, m[1]
+          token Punctuation::Indicator, '.'
+          token Text::Whitespace, m[2]
+          push :proof_mode
+        end
+      end
+
+      state :proof_mode do
+        mixin :comment_whitespace
+        mixin :module_setopts
+        mixin :begin_proof
+        rule qed do |m|
+          token Keyword, m[1]
+          token Text::Whitespace, m[2]
+          token Punctuation::Indicator, '.'
+          token Text::Whitespace, m[3]
+          pop! # :proof_mode
+        end
+        # the whole point of parsing Proof/Qed, normally some of these will be operators
+        rule %r/(?:\-+|\++|\*+)/, Punctuation
+        rule %r/[{}]/, Punctuation
+        # toplevel_selector
+        rule %r/(!|all|par)(:)/ do
+          groups Keyword::Pseudo, Punctuation
+        end
+        # numbered goals 1: {} 1,2: {}
+        rule %r/\d+/, Num::Integer, :numeric_labels
+        # [named_goal]: { ... }
+        rule %r/(\[)(\s*)(#{id})(\s*)(\])(\s*)(:)/ do
+          groups Punctuation, Text::Whitespace, Name::Constant, Text::Whitespace, Punctuation, Text::Whitespace, Punctuation
+        end
+        # After parsing the id, end up in sentence_postid
+        rule id do |m|
+          @name = m[0]
+          @id_dotted = false
+          push :sentence_postid
+          push :continue_id
+        end
+      end
+
+      state :numeric_labels do
+        mixin :whitespace
+        rule %r/(,)(\s*)(\d+)/ do |m|
+          groups Punctuation, Text::Whitespace, Num::Integer
+        end
+        rule %r(:), Punctuation, :pop!
+      end
+
+      state :whitespace do
         rule %r/\s+/m, Text::Whitespace
+      end
+      state :comment_whitespace do
+        rule %r/[(][*](?![)])/, Comment, :comment
+        mixin :whitespace
+      end
+
+      state :module_setopts do
         rule module_type do |m|
           token Keyword , 'Module'
           token Text::Whitespace , m[1]
@@ -108,32 +182,39 @@ def self.classify(x)
           end
           token self.class.end_sentence , '.'
         end
+      end
+
+      state :sentence_postid do
+        mixin :comment_whitespace
+        mixin :module_setopts
+
+        # up here to beat the id rule for lambda
+        rule %r(:=|=>|;|:>|:|::|_), Punctuation
+        rule %r(->|/\\|\\/|;|:>|[⇒→↔⇔≔≡∀∃∧∨¬⊤⊥⊢⊨∈λ]), Operator
+
         rule id do |m|
           @name = m[0]
-          @continue = false
+          @id_dotted = false
           push :continue_id
         end
-        rule %r(/\\), Operator
-        rule %r/\\\//, Operator
+
+        # must be followed by whitespace, so that we don't match notations like sym.(a + b)
+        rule %r/\.(?=\s)/, Punctuation::Indicator, :pop! # :sentence_postid
 
         rule %r/-?\d[\d_]*(.[\d_]*)?(e[+-]?\d[\d_]*)/i, Num::Float
-        rule %r/\d[\d_]*/, Num::Integer
+        rule %r/-?\d[\d_]*/, Num::Integer
 
         rule %r/'(?:(\\[\\"'ntbr ])|(\\[0-9]{3})|(\\x\h{2}))'/, Str::Char
         rule %r/'/, Keyword
         rule %r/"/, Str::Double, :string
         rule %r/[~?]#{id}/, Name::Variable
 
-        rule %r/./ do |m|
-          match = m[0]
-          if self.class.keyopts.include? match
-            token Punctuation
-          elsif match =~ operator
-            token Operator
-          else
-            token Error
-          end
-        end
+        rule %r(`{|[{}\[\]()?|;,.]), Punctuation
+        rule %r([!@^|~#.%/]+), Operator
+        # any other combo of S (symbol), P (punctuation) and some extras just to be sure
+        rule %r((?:\p{S}|\p{Pc}|[./\:\<=>\-+*])+), Operator
+
+        rule %r/./, Error
       end
 
       state :comment do
@@ -159,30 +240,32 @@ def self.classify(x)
         rule dot_id do |m|
           token Name::Namespace , @name
           token Punctuation , '.'
-          @continue = true
+          @id_dotted = true
           @name = m[1]
         end
         rule dot_space do |m|
-          if @continue
+          if @id_dotted
             token Name::Constant , @name
           else
             token self.class.classify(@name) , @name
           end
           token self.class.end_sentence , '.'
           token Text::Whitespace , m[1]
           @name = false
-          @continue = false
-          pop!
+          @id_dotted = false
+          pop! # :continue_id
+          pop! # :sentence_postid
         end
         rule %r// do
-          if @continue
+          if @id_dotted
             token Name::Constant , @name
           else
             token self.class.classify(@name) , @name
           end
           @name = false
-          @continue = false
-          pop!
+          @id_dotted = false
+          # we finished parsing an id, drop back into the sentence_postid that was pushed first.
+          pop! # :continue_id
         end
       end
 

spec/visual/samples/coq

@@ -17,6 +17,7 @@ Notation "A /\ B" := (and A B) : type_scope.
 Theorem progress : ∀t T,
   empty ⊢ t ∈ T →
   value t ∨ ∃t', t --> t'.
+Proof. Admitted.
 
 Theorem ev_plus4 : ∀n, even n → even (4 + n).
 Proof.
@@ -25,3 +26,87 @@ Proof.
   apply ev_SS.
   apply H.
 Qed.
+
+(*
+   The iris examples here are used under this license:
+
+   > All files in this development, excluding those in docs/ and tex/, are
+   distributed under the terms of the 3-clause BSD license
+   (https://opensource.org/licenses/BSD-3-Clause), included below.
+   > Copyright: Iris developers and contributors
+*)
+
+(* Unicode next to braces, mixed ascii/unicode operators. *)
+Lemma ghost_var_update γ b' b c :
+  own γ (●E b) -∗ own γ (◯E c) ==∗ own γ (●E b') ∗ own γ (◯E b').
+Proof.
+  something (a ={n}= b).
+  - by apply case1.
+  - apply case2. eauto.
+Qed.
+
+
+(* #[], {Σ}, `{!xxx}, (?)
+   https://gitlab.mpi-sws.org/iris/iris/-/blob/f1e2242daa0e448135a5074ce99b41e6058ea1c3/iris_heap_lang/adequacy.v *)
+Definition heapΣ : gFunctors :=
+  #[invΣ; gen_heapΣ loc (option val); inv_heapΣ loc (option val); proph_mapΣ proph_id (val * val)].
+Global Instance subG_heapGpreS {Σ} : subG heapΣ Σ → heapGpreS Σ.
+Proof. solve_inG. Qed.
+
+(* (?), `{!class}, greek lettering *)
+Definition heap_adequacy Σ `{!heapGpreS Σ} s e σ φ :
+  (∀ `{!heapGS Σ}, ⊢ inv_heap_inv -∗ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
+  adequate s e σ (λ v _, φ v).
+Proof.
+  intros Hwp; eapply (wp_adequacy _ _); iIntros (? κs) "".
+  iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
+  iMod (inv_heap_init loc (option val)) as (?) ">Hi".
+  iMod (proph_map_init κs σ.(used_proph_id)) as (?) "Hp".
+  (* lambda should highlight as an operator *)
+  iModIntro. iExists
+    (λ σ κs, (gen_heap_interp σ.(heap) ∗ proph_map_interp κs σ.(used_proph_id))%I),
+    (λ _, True%I).
+  iFrame. iApply (Hwp (HeapGS _ _ _ _ _)). done.
+Qed.
+
+(* thorny ops + braces + lettering
+   https://gitlab.mpi-sws.org/iris/iris/-/blob/f1e2242daa0e448135a5074ce99b41e6058ea1c3/iris_heap_lang/primitive_laws.value
+   BSD licensed *)
+Lemma wp_rec_löb s E f x e Φ Ψ :
+  □ ( □ (∀ v, Ψ v -∗ WP (rec: f x := e)%V v @ s; E {{ Φ }}) -∗
+     ∀ v, Ψ v -∗ WP (subst' x v (subst' f (rec: f x := e) e)) @ s; E {{ Φ }}) -∗
+  ∀ v, Ψ v -∗ WP (rec: f x := e)%V v @ s; E {{ Φ }}.
+Proof.
+  iIntros "#Hrec". iLöb as "IH". iIntros (v) "HΨ".
+  (* dotted gives a path *)
+  iApply lifting.wp_pure_step_later; first done.
+  iNext. iApply ("Hrec" with "[] HΨ"). iIntros "!>" (w) "HΨ".
+  iApply ("IH" with "HΨ").
+Qed.
+
+(* unicode symbols distinct from braces and idents *)
+Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
+  ¬ ✓(dq1 ⋅ dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
+Proof. apply mapsto_frac_ne. Qed.
+
+Lemma inv_mapsto_own_acc E l v I:
+  ↑inv_heapN ⊆ E →
+  inv_heap_inv -∗ l ↦_I v ={E, E ∖ ↑inv_heapN}=∗
+    (⌜I v⌝ ∗ l ↦ v ∗ (∀ w, ⌜I w ⌝ -∗ l ↦ w ={E ∖ ↑inv_heapN, E}=∗ l ↦_I w)).
+Proof. (*snip*) Qed.
+
+Lemma mapsto_persist l dq v : l ↦{dq} v ==∗ l ↦□ v.
+Proof.
+  refine ?[named]. refine ?[named2].
+  [named]: done.
+  [named2]: { done. }
+  (* Bullets are distinct from operators, and are treated as Punctuation *)
+  - done.
+    + done.
+      -- done.
+    + apply (f -888 + 5).
+  all: nice.
+  1: { done. }
+  1,2: { done. }
+  1,2,3: { done. }
+Qed.