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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
|
if !exists('g:polyglot_disabled') || index(g:polyglot_disabled, 'idris') == -1
" indentation for idris (idris-lang.org)
"
" Based on haskell indentation by motemen <motemen@gmail.com>
"
" author: raichoo (raichoo@googlemail.com)
"
" Modify g:idris_indent_if and g:idris_indent_case to
" change indentation for `if'(default 3) and `case'(default 5).
" Example (in .vimrc):
" > let g:idris_indent_if = 2
if exists('b:did_indent')
finish
endif
let b:did_indent = 1
if !exists('g:idris_indent_if')
" if bool
" >>>then ...
" >>>else ...
let g:idris_indent_if = 3
endif
if !exists('g:idris_indent_case')
" case xs of
" >>>>>[] => ...
" >>>>>(y::ys) => ...
let g:idris_indent_case = 5
endif
if !exists('g:idris_indent_let')
" let x : Nat = O in
" >>>>x
let g:idris_indent_let = 4
endif
if !exists('g:idris_indent_rewrite')
" rewrite prf in expr
" >>>>>>>>x
let g:idris_indent_rewrite = 8
endif
if !exists('g:idris_indent_where')
" where f : Nat -> Nat
" >>>>>>f x = x
let g:idris_indent_where = 6
endif
if !exists('g:idris_indent_do')
" do x <- a
" >>>y <- b
let g:idris_indent_do = 3
endif
setlocal indentexpr=GetIdrisIndent()
setlocal indentkeys=!^F,o,O,}
function! GetIdrisIndent()
let prevline = getline(v:lnum - 1)
if prevline =~ '\s\+(\s*.\+\s\+:\s\+.\+\s*)\s\+->\s*$'
return match(prevline, '(')
elseif prevline =~ '\s\+{\s*.\+\s\+:\s\+.\+\s*}\s\+->\s*$'
return match(prevline, '{')
endif
if prevline =~ '[!#$%&*+./<>?@\\^|~-]\s*$'
let s = match(prevline, '[:=]')
if s > 0
return s + 2
else
return match(prevline, '\S')
endif
endif
if prevline =~ '[{([][^})\]]\+$'
return match(prevline, '[{([]')
endif
if prevline =~ '\<let\>\s\+.\+\<in\>\s*$'
return match(prevline, '\<let\>') + g:idris_indent_let
endif
if prevline =~ '\<rewrite\>\s\+.\+\<in\>\s*$'
return match(prevline, '\<rewrite\>') + g:idris_indent_rewrite
endif
if prevline !~ '\<else\>'
let s = match(prevline, '\<if\>.*\&.*\zs\<then\>')
if s > 0
return s
endif
let s = match(prevline, '\<if\>')
if s > 0
return s + g:idris_indent_if
endif
endif
if prevline =~ '\(\<where\>\|\<do\>\|=\|[{([]\)\s*$'
return match(prevline, '\S') + &shiftwidth
endif
if prevline =~ '\<where\>\s\+\S\+.*$'
return match(prevline, '\<where\>') + g:idris_indent_where
endif
if prevline =~ '\<do\>\s\+\S\+.*$'
return match(prevline, '\<do\>') + g:idris_indent_do
endif
if prevline =~ '^\s*\<\(co\)\?data\>\s\+[^=]\+\s\+=\s\+\S\+.*$'
return match(prevline, '=')
endif
if prevline =~ '\<with\>\s\+([^)]*)\s*$'
return match(prevline, '\S') + &shiftwidth
endif
if prevline =~ '\<case\>\s\+.\+\<of\>\s*$'
return match(prevline, '\<case\>') + g:idris_indent_case
endif
if prevline =~ '^\s*\(\<namespace\>\|\<\(co\)\?data\>\)\s\+\S\+\s*$'
return match(prevline, '\(\<namespace\>\|\<\(co\)\?data\>\)') + &shiftwidth
endif
if prevline =~ '^\s*\(\<using\>\|\<parameters\>\)\s*([^(]*)\s*$'
return match(prevline, '\(\<using\>\|\<parameters\>\)') + &shiftwidth
endif
if prevline =~ '^\s*\<mutual\>\s*$'
return match(prevline, '\<mutual\>') + &shiftwidth
endif
let line = getline(v:lnum)
if (line =~ '^\s*}\s*' && prevline !~ '^\s*;')
return match(prevline, '\S') - &shiftwidth
endif
return match(prevline, '\S')
endfunction
endif
|
