diff options
| -rw-r--r-- | pygments/lexers/_mapping.py | 2 | ||||
| -rw-r--r-- | pygments/lexers/functional.py | 134 | ||||
| -rw-r--r-- | tests/examplefiles/test.idr | 93 |
3 files changed, 228 insertions, 1 deletions
diff --git a/pygments/lexers/_mapping.py b/pygments/lexers/_mapping.py index 7e4a33dd..443a573c 100644 --- a/pygments/lexers/_mapping.py +++ b/pygments/lexers/_mapping.py @@ -144,6 +144,7 @@ LEXERS = { 'HyLexer': ('pygments.lexers.agile', 'Hy', ('hylang',), ('*.hy',), ('text/x-hy', 'application/x-hy')), 'HybrisLexer': ('pygments.lexers.other', 'Hybris', ('hybris', 'hy'), ('*.hy', '*.hyb'), ('text/x-hybris', 'application/x-hybris')), 'IDLLexer': ('pygments.lexers.math', 'IDL', ('idl',), ('*.pro',), ('text/idl',)), + 'IdrisLexer': ('pygments.lexers.functional', 'Idris', ('idris', 'idr'), ('*.idr',), ('text/x-idris',)), 'IgorLexer': ('pygments.lexers.math', 'Igor', ('igor', 'igorpro'), ('*.ipf',), ('text/ipf',)), 'IniLexer': ('pygments.lexers.text', 'INI', ('ini', 'cfg', 'dosini'), ('*.ini', '*.cfg'), ('text/x-ini',)), 'IoLexer': ('pygments.lexers.agile', 'Io', ('io',), ('*.io',), ('text/x-iosrc',)), @@ -174,6 +175,7 @@ LEXERS = { 'LighttpdConfLexer': ('pygments.lexers.text', 'Lighttpd configuration file', ('lighty', 'lighttpd'), (), ('text/x-lighttpd-conf',)), 'LiterateAgdaLexer': ('pygments.lexers.functional', 'Literate Agda', ('lagda', 'literate-agda'), ('*.lagda',), ('text/x-literate-agda',)), 'LiterateHaskellLexer': ('pygments.lexers.functional', 'Literate Haskell', ('lhs', 'literate-haskell', 'lhaskell'), ('*.lhs',), ('text/x-literate-haskell',)), + 'LiterateIdrisLexer': ('pygments.lexers.functional', 'Literate Idris', ('lidr', 'literate-idris', 'lidris'), ('*.lidr',), ('text/x-literate-idris',)), 'LiveScriptLexer': ('pygments.lexers.web', 'LiveScript', ('live-script', 'livescript'), ('*.ls',), ('text/livescript',)), 'LlvmLexer': ('pygments.lexers.asm', 'LLVM', ('llvm',), ('*.ll',), ('text/x-llvm',)), 'LogosLexer': ('pygments.lexers.compiled', 'Logos', ('logos',), ('*.x', '*.xi', '*.xm', '*.xmi'), ('text/x-logos',)), diff --git a/pygments/lexers/functional.py b/pygments/lexers/functional.py index 07fa9d45..e3342497 100644 --- a/pygments/lexers/functional.py +++ b/pygments/lexers/functional.py @@ -19,7 +19,7 @@ __all__ = ['RacketLexer', 'SchemeLexer', 'CommonLispLexer', 'HaskellLexer', 'AgdaLexer', 'LiterateHaskellLexer', 'LiterateAgdaLexer', 'SMLLexer', 'OcamlLexer', 'ErlangLexer', 'ErlangShellLexer', 'OpaLexer', 'CoqLexer', 'NewLispLexer', 'NixLexer', 'ElixirLexer', - 'ElixirConsoleLexer', 'KokaLexer'] + 'ElixirConsoleLexer', 'KokaLexer', 'IdrisLexer', 'LiterateIdrisLexer'] line_re = re.compile('.*?\n') @@ -1017,6 +1017,115 @@ class HaskellLexer(RegexLexer): } +class IdrisLexer(RegexLexer): + """ + A lexer for the dependently typed programming language Idris. + + Based on the Haskell and Agda Lexer. + + .. versionadded:: 2.0 + """ + name = 'Idris' + aliases = ['idris', 'idr'] + filenames = ['*.idr'] + mimetypes = ['text/x-idris'] + + reserved = ['case','class','data','default','using','do','else', + 'if','in','infix[lr]?','instance','rewrite','auto', + 'namespace','codata','mutual','private','public','abstract', + 'total','partial', + 'let','proof','of','then','static','where','_','with', + 'pattern', 'term', 'syntax','prefix', + 'postulate','parameters','record','dsl','impossible','implicit', + 'tactics','intros','intro','compute','refine','exaxt','trivial'] + + ascii = ['NUL','SOH','[SE]TX','EOT','ENQ','ACK', + 'BEL','BS','HT','LF','VT','FF','CR','S[OI]','DLE', + 'DC[1-4]','NAK','SYN','ETB','CAN', + 'EM','SUB','ESC','[FGRU]S','SP','DEL'] + + annotations = ['assert_total','lib','link','include','provide','access', + 'default'] + + tokens = { + 'root': [ + # Declaration + (r'^(\s*)([^\s\(\)\{\}]+)(\s*)(:)(\s*)', + bygroups(Text, Name.Function, Text, Operator.Word, Text)), + # Comments + (r'^(\s*)(%%%s)' % '|'.join(annotations), + bygroups(Text, Keyword.Reserved)), + (r'--(?![!#$%&*+./<=>?@\^|_~:\\]).*?$', Comment.Single), + (r'{-', Comment.Multiline, 'comment'), + # Identifiers + (ur'\b(%s)(?!\')\b' % '|'.join(reserved), Keyword.Reserved), + (r'(import|module)(\s+)', bygroups(Keyword.Reserved, Text), 'module'), + (r"('')?[A-Z][\w\']*", Keyword.Type), + (r'[a-z][A-Za-z0-9_\']*', Text), + # Special Symbols + (r'(<-|::|->|=>|=)', Operator.Word), # specials + (r'([\[\]:!#$%&*+.\\/<=>?@^|~-]+)', Operator.Word), # specials + # Numbers + (r'\d+[eE][+-]?\d+', Number.Float), + (r'\d+\.\d+([eE][+-]?\d+)?', Number.Float), + (r'0[xX][\da-fA-F]+', Number.Hex), + (r'\d+', Number.Integer), + # Strings + (r"'", String.Char, 'character'), + (r'"', String, 'string'), + (r'[^\s\(\)\{\}]+', Text), + (r'\s+?', Text), # Whitespace + ], + 'module': [ + (r'\s+', Text), + (r'([A-Z][a-zA-Z0-9_.]*)(\s+)(\()', + bygroups(Name.Namespace, Text, Punctuation), 'funclist'), + (r'[A-Z][a-zA-Z0-9_.]*', Name.Namespace, '#pop'), + ], + 'funclist': [ + (r'\s+', Text), + (r'[A-Z][a-zA-Z0-9_]*', Keyword.Type), + (r'(_[\w\']+|[a-z][\w\']*)', Name.Function), + (r'--.*$', Comment.Single), + (r'{-', Comment.Multiline, 'comment'), + (r',', Punctuation), + (r'[:!#$%&*+.\\/<=>?@^|~-]+', Operator), + # (HACK, but it makes sense to push two instances, believe me) + (r'\(', Punctuation, ('funclist', 'funclist')), + (r'\)', Punctuation, '#pop:2'), + ], + # NOTE: the next four states are shared in the AgdaLexer; make sure + # any change is compatible with Agda as well or copy over and change + 'comment': [ + # Multiline Comments + (r'[^-{}]+', Comment.Multiline), + (r'{-', Comment.Multiline, '#push'), + (r'-}', Comment.Multiline, '#pop'), + (r'[-{}]', Comment.Multiline), + ], + 'character': [ + # Allows multi-chars, incorrectly. + (r"[^\\']", String.Char), + (r"\\", String.Escape, 'escape'), + ("'", String.Char, '#pop'), + ], + 'string': [ + (r'[^\\"]+', String), + (r"\\", String.Escape, 'escape'), + ('"', String, '#pop'), + ], + 'escape': [ + (r'[abfnrtv"\'&\\]', String.Escape, '#pop'), + (r'\^[][A-Z@\^_]', String.Escape, '#pop'), + ('|'.join(ascii), String.Escape, '#pop'), + (r'o[0-7]+', String.Escape, '#pop'), + (r'x[\da-fA-F]+', String.Escape, '#pop'), + (r'\d+', String.Escape, '#pop'), + (r'\s+\\', String.Escape, '#pop') + ], + } + + class AgdaLexer(RegexLexer): """ For the `Agda <http://wiki.portal.chalmers.se/agda/pmwiki.php>`_ @@ -1173,6 +1282,29 @@ class LiterateHaskellLexer(LiterateLexer): LiterateLexer.__init__(self, hslexer, **options) +class LiterateIdrisLexer(LiterateLexer): + """ + For Literate Idris (Bird-style or LaTeX) source. + + Additional options accepted: + + `litstyle` + If given, must be ``"bird"`` or ``"latex"``. If not given, the style + is autodetected: if the first non-whitespace character in the source + is a backslash or percent character, LaTeX is assumed, else Bird. + + .. versionadded:: 2.0 + """ + name = 'Literate Idris' + aliases = ['lidr', 'literate-idris', 'lidris'] + filenames = ['*.lidr'] + mimetypes = ['text/x-literate-idris'] + + def __init__(self, **options): + hslexer = IdrisLexer(**options) + LiterateLexer.__init__(self, hslexer, **options) + + class LiterateAgdaLexer(LiterateLexer): """ For Literate Agda source. diff --git a/tests/examplefiles/test.idr b/tests/examplefiles/test.idr new file mode 100644 index 00000000..f0e96d88 --- /dev/null +++ b/tests/examplefiles/test.idr @@ -0,0 +1,93 @@ +module Main + +data Ty = TyInt | TyBool | TyFun Ty Ty + +interpTy : Ty -> Type +interpTy TyInt = Int +interpTy TyBool = Bool +interpTy (TyFun s t) = interpTy s -> interpTy t + +using (G : Vect n Ty) + + data Env : Vect n Ty -> Type where + Nil : Env Nil + (::) : interpTy a -> Env G -> Env (a :: G) + + data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where + stop : HasType fZ (t :: G) t + pop : HasType k G t -> HasType (fS k) (u :: G) t + + lookup : HasType i G t -> Env G -> interpTy t + lookup stop (x :: xs) = x + lookup (pop k) (x :: xs) = lookup k xs + + data Expr : Vect n Ty -> Ty -> Type where + Var : HasType i G t -> Expr G t + Val : (x : Int) -> Expr G TyInt + Lam : Expr (a :: G) t -> Expr G (TyFun a t) + App : Expr G (TyFun a t) -> Expr G a -> Expr G t + Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b -> + Expr G c + If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a + Bind : Expr G a -> (interpTy a -> Expr G b) -> Expr G b + + dsl expr + lambda = Lam + variable = Var + index_first = stop + index_next = pop + + (<$>) : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t + (<$>) = \f, a => App f a + + pure : Expr G a -> Expr G a + pure = id + + syntax IF [x] THEN [t] ELSE [e] = If x t e + + (==) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool + (==) = Op (==) + + (<) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool + (<) = Op (<) + + instance Num (Expr G TyInt) where + (+) x y = Op (+) x y + (-) x y = Op (-) x y + (*) x y = Op (*) x y + + abs x = IF (x < 0) THEN (-x) ELSE x + + fromInteger = Val . fromInteger + + interp : Env G -> {static} Expr G t -> interpTy t + interp env (Var i) = lookup i env + interp env (Val x) = x + interp env (Lam sc) = \x => interp (x :: env) sc + interp env (App f s) = (interp env f) (interp env s) + interp env (Op op x y) = op (interp env x) (interp env y) + interp env (If x t e) = if (interp env x) then (interp env t) else (interp env e) + interp env (Bind v f) = interp env (f (interp env v)) + + eId : Expr G (TyFun TyInt TyInt) + eId = expr (\x => x) + + eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt)) + eTEST = expr (\x, y => y) + + eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt)) + eAdd = expr (\x, y => Op (+) x y) + + eDouble : Expr G (TyFun TyInt TyInt) + eDouble = expr (\x => App (App eAdd x) (Var stop)) + + eFac : Expr G (TyFun TyInt TyInt) + eFac = expr (\x => IF x == 0 THEN 1 ELSE [| eFac (x - 1) |] * x) + +testFac : Int +testFac = interp [] eFac 4 + +main : IO () +main = print testFac + + |