blob: 4ddf849d02c33f7dbb6ae91fb0b1219673ef8d8f (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
;; Punctuation
[ "." ";" ":"] @punctuation.delimiter
[ "(" ")" "{" "}" ] @punctuation.bracket
;; Constants
(integer) @constant.numeric.integer
; (float) @constant.numeric.float
(literal) @string
;; Pragmas and comments
(comment) @comment
(pragma) @attribute
(macro) @function.macro
;; Imports
(module_name) @namespace
(import_directive (id) @namespace)
[(module) (import) (open)] @keyword.control.import
;; Types
(typed_binding (expr) @type)
(record (expr) @type)
(data (expr) @type)
(signature (expr) @type)
(function (rhs (expr) @type))
; todo: these are too general. ideally, any nested (atom)
; https://github.com/tree-sitter/tree-sitter/issues/880
;; Variables
(untyped_binding (atom) @variable)
(typed_binding (atom) @variable)
(field_name) @variable.other.member
;; Functions
(function_name) @function
;(function (lhs
; . (atom) @function
; (atom) @variable.parameter))
; todo: currently fails to parse, upstream tree-sitter bug
;; Data
[(data_name) (record_name)] @constructor
((atom) @constant.builtin.boolean
(#any-of? @constant.builtin.boolean "true" "false" "True" "False"))
"Set" @type.builtin
; postulate
; type_signature
; pattern
; id
; bid
; typed_binding
; primitive
; private
; record_signature
; record_assignments
; field_assignment
; module_assignment
; renaming
; import_directive
; lambda
; let
; instance
; generalize
; record
; fields
; syntax
; hole_name
; data_signature
;; Keywords
[
"where"
"data"
"rewrite"
"postulate"
"public"
"private"
"tactic"
"Prop"
"quote"
"renaming"
"in"
"hiding"
"constructor"
"abstract"
"let"
"field"
"mutual"
"infix"
"infixl"
"infixr"
"record"
"overlap"
"instance"
"do"
] @keyword
[
"="
] @operator
; = | -> : ? \ .. ... λ ∀ →
; (_LAMBDA) (_FORALL) (_ARROW)
; "coinductive"
; "eta-equality"
; "field"
; "inductive"
; "interleaved"
; "macro"
; "no-eta-equality"
; "pattern"
; "primitive"
; "quoteTerm"
; "rewrite"
; "syntax"
; "unquote"
; "unquoteDecl"
; "unquoteDef"
; "using"
; "variable"
; "with"
|
