A lexer for F*, an ML dialect for program verification (#1409)

* A lexer for F*, an ML dialect for program verification

* Fix treatment of infix applications, e.g.

* Correct modifications

* Better lexing

* Added F* to the list of supported languages

* Add example file

* Bumped versionadded field

* Added link to language

Co-authored-by: Jonathan Protzenko <jonathan.protzenko@gmail.com>

2 files changed, 105 insertions, 6 deletions

diff --git a/pygments/lexers/_mapping.py b/pygments/lexers/_mapping.py
index 1d754ce4..bba4875b 100644
--- a/pygments/lexers/_mapping.py
+++ b/pygments/lexers/_mapping.py
@@ -152,6 +152,7 @@ LEXERS = {
     'EvoqueXmlLexer': ('pygments.lexers.templates', 'XML+Evoque', ('xml+evoque',), ('*.xml',), ('application/xml+evoque',)),
     'EzhilLexer': ('pygments.lexers.ezhil', 'Ezhil', ('ezhil',), ('*.n',), ('text/x-ezhil',)),
     'FSharpLexer': ('pygments.lexers.dotnet', 'F#', ('fsharp', 'f#'), ('*.fs', '*.fsi'), ('text/x-fsharp',)),
+    'FStarLexer': ('pygments.lexers.ml', 'FStar', ('fstar',), ('*.fst', '*.fsti'), ('text/x-fstar',)),
     'FactorLexer': ('pygments.lexers.factor', 'Factor', ('factor',), ('*.factor',), ('text/x-factor',)),
     'FancyLexer': ('pygments.lexers.ruby', 'Fancy', ('fancy', 'fy'), ('*.fy', '*.fancypack'), ('text/x-fancysrc',)),
     'FantomLexer': ('pygments.lexers.fantom', 'Fantom', ('fan',), ('*.fan',), ('application/x-fantom',)),
diff --git a/pygments/lexers/ml.py b/pygments/lexers/ml.py
index c052de7a..e9ab61e6 100644
--- a/pygments/lexers/ml.py
+++ b/pygments/lexers/ml.py
@@ -15,7 +15,7 @@ from pygments.lexer import RegexLexer, include, bygroups, default, words
 from pygments.token import Text, Comment, Operator, Keyword, Name, String, \
     Number, Punctuation, Error
 
-__all__ = ['SMLLexer', 'OcamlLexer', 'OpaLexer', 'ReasonLexer']
+__all__ = ['SMLLexer', 'OcamlLexer', 'OpaLexer', 'ReasonLexer', 'FStarLexer']
 
 
 class SMLLexer(RegexLexer):
@@ -780,11 +780,11 @@ class ReasonLexer(RegexLexer):
     mimetypes = ['text/x-reasonml']
 
     keywords = (
-    'as', 'assert', 'begin', 'class', 'constraint', 'do', 'done', 'downto', 
-    'else', 'end', 'exception', 'external', 'false', 'for', 'fun', 'esfun', 
-    'function', 'functor', 'if', 'in', 'include', 'inherit', 'initializer', 'lazy', 
-    'let', 'switch', 'module', 'pub', 'mutable', 'new', 'nonrec', 'object', 'of', 
-    'open', 'pri', 'rec', 'sig', 'struct', 'then', 'to', 'true', 'try', 
+    'as', 'assert', 'begin', 'class', 'constraint', 'do', 'done', 'downto',
+    'else', 'end', 'exception', 'external', 'false', 'for', 'fun', 'esfun',
+    'function', 'functor', 'if', 'in', 'include', 'inherit', 'initializer', 'lazy',
+    'let', 'switch', 'module', 'pub', 'mutable', 'new', 'nonrec', 'object', 'of',
+    'open', 'pri', 'rec', 'sig', 'struct', 'then', 'to', 'true', 'try',
     'type', 'val', 'virtual', 'when', 'while', 'with'
     )
     keyopts = (
@@ -857,3 +857,101 @@ class ReasonLexer(RegexLexer):
             default('#pop'),
         ],
     }
+
+
+class FStarLexer(RegexLexer):
+    """
+    For the F* language (https://www.fstar-lang.org/).
+    .. versionadded:: 2.7
+    """
+
+    name = 'FStar'
+    aliases = ['fstar']
+    filenames = ['*.fst', '*.fsti']
+    mimetypes = ['text/x-fstar']
+
+    keywords = (
+        'abstract', 'attributes', 'noeq', 'unopteq', 'and'
+        'begin', 'by', 'default', 'effect', 'else', 'end', 'ensures',
+        'exception', 'exists', 'false', 'forall', 'fun', 'function', 'if',
+        'in', 'include', 'inline', 'inline_for_extraction', 'irreducible',
+        'logic', 'match', 'module', 'mutable', 'new', 'new_effect', 'noextract',
+        'of', 'open', 'opaque', 'private', 'range_of', 'reifiable',
+        'reify', 'reflectable', 'requires', 'set_range_of', 'sub_effect',
+        'synth', 'then', 'total', 'true', 'try', 'type', 'unfold', 'unfoldable',
+        'val', 'when', 'with', 'not'
+    )
+    decl_keywords = ('let', 'rec')
+    assume_keywords = ('assume', 'admit', 'assert', 'calc')
+    keyopts = (
+        r'~', r'-', r'/\\', r'\\/', r'<:', r'<@', r'\(\|', r'\|\)', r'#', r'u#',
+        r'&', r'\(\)', r'\(', r'\)', r',', r'~>', r'->', r'<--', r'<-', r'<==>',
+        r'==>', r'\.', r'\?\.', r'\?', r'\.\[', r'\.\(\|', r'\.\(', r'\.\[\|',
+        r'\{:pattern', r':', r'::', r':=', r';;', r';', r'=', r'%\[', r'!\{',
+        r'\[@', r'\[', r'\[\|', r'\|>', r'\]', r'\|\]', r'\{', r'\|', r'\}', r'\$'
+    )
+
+    operators = r'[!$%&*+\./:<=>?@^|~-]'
+    prefix_syms = r'[!?~]'
+    infix_syms = r'[=<>@^|&+\*/$%-]'
+    primitives = ('unit', 'int', 'float', 'bool', 'string', 'char', 'list', 'array')
+
+    tokens = {
+        'escape-sequence': [
+            (r'\\[\\"\'ntbr]', String.Escape),
+            (r'\\[0-9]{3}', String.Escape),
+            (r'\\x[0-9a-fA-F]{2}', String.Escape),
+        ],
+        'root': [
+            (r'\s+', Text),
+            (r'false|true|False|True|\(\)|\[\]', Name.Builtin.Pseudo),
+            (r'\b([A-Z][\w\']*)(?=\s*\.)', Name.Namespace, 'dotted'),
+            (r'\b([A-Z][\w\']*)', Name.Class),
+            (r'\(\*(?![)])', Comment, 'comment'),
+            (r'^\/\/.+$', Comment),
+            (r'\b(%s)\b' % '|'.join(keywords), Keyword),
+            (r'\b(%s)\b' % '|'.join(assume_keywords), Name.Exception),
+            (r'\b(%s)\b' % '|'.join(decl_keywords), Keyword.Declaration),
+            (r'(%s)' % '|'.join(keyopts[::-1]), Operator),
+            (r'(%s|%s)?%s' % (infix_syms, prefix_syms, operators), Operator),
+            (r'\b(%s)\b' % '|'.join(primitives), Keyword.Type),
+
+            (r"[^\W\d][\w']*", Name),
+
+            (r'-?\d[\d_]*(.[\d_]*)?([eE][+\-]?\d[\d_]*)', Number.Float),
+            (r'0[xX][\da-fA-F][\da-fA-F_]*', Number.Hex),
+            (r'0[oO][0-7][0-7_]*', Number.Oct),
+            (r'0[bB][01][01_]*', Number.Bin),
+            (r'\d[\d_]*', Number.Integer),
+
+            (r"'(?:(\\[\\\"'ntbr ])|(\\[0-9]{3})|(\\x[0-9a-fA-F]{2}))'",
+             String.Char),
+            (r"'.'", String.Char),
+            (r"'", Keyword),  # a stray quote is another syntax element
+            (r"\`([\w\'\.]+)\`", Operator.Word),  # for infix applications
+            (r"\`", Keyword),  # for quoting
+            (r'"', String.Double, 'string'),
+
+            (r'[~?][a-z][\w\']*:', Name.Variable),
+        ],
+        'comment': [
+            (r'[^(*)]+', Comment),
+            (r'\(\*', Comment, '#push'),
+            (r'\*\)', Comment, '#pop'),
+            (r'[(*)]', Comment),
+        ],
+        'string': [
+            (r'[^\\"]+', String.Double),
+            include('escape-sequence'),
+            (r'\\\n', String.Double),
+            (r'"', String.Double, '#pop'),
+        ],
+        'dotted': [
+            (r'\s+', Text),
+            (r'\.', Punctuation),
+            (r'[A-Z][\w\']*(?=\s*\.)', Name.Namespace),
+            (r'[A-Z][\w\']*', Name.Class, '#pop'),
+            (r'[a-z_][\w\']*', Name, '#pop'),
+            default('#pop'),
+        ],
+    }