git.iko.soy/Idris-dev
on master help sign in
Merge pull request #58 from raichoo/master
1865526Edwin Brady
contribs/tool-support/vim/indent/idris.vim+76−59
compare with master
unifiedsplit
@@ -3,7 +3,7 @@
3" Based on haskell indentation by motemen <motemen@gmail.com>
3" Based on haskell indentation by motemen <motemen@gmail.com>
4"
4"
5" author: raichoo (raichoo@googlemail.com)
5" author: raichoo (raichoo@googlemail.com)
6−" date: Sep 21 2012
6+" date: Oct 19 2012
7"
7"
8" Modify g:idris_indent_if and g:idris_indent_case to
8" Modify g:idris_indent_if and g:idris_indent_case to
9" change indentation for `if'(default 3) and `case'(default 5).
9" change indentation for `if'(default 3) and `case'(default 5).
@@ -11,92 +11,109 @@
11" > let g:idris_indent_if = 2
11" > let g:idris_indent_if = 2
12
12
13if exists('b:did_indent')
13if exists('b:did_indent')
14− finish
14+ finish
15endif
15endif
16
16
17let b:did_indent = 1
17let b:did_indent = 1
18
18
19if !exists('g:idris_indent_if')
19if !exists('g:idris_indent_if')
20− " if bool
20+ " if bool
21− " >>>then ...
21+ " >>>then ...
22− " >>>else ...
22+ " >>>else ...
23− let g:idris_indent_if = 3
23+ let g:idris_indent_if = 3
24endif
24endif
25
25
26if !exists('g:idris_indent_case')
26if !exists('g:idris_indent_case')
27− " case xs of
27+ " case xs of
28− " >>>>>[] -> ...
28+ " >>>>>[] -> ...
29− " >>>>>(y:ys) -> ...
29+ " >>>>>(y::ys) -> ...
30− let g:idris_indent_case = 5
30+ let g:idris_indent_case = 5
31+endif
32+
33+if !exists('g:idris_indent_let')
34+ " let x : Nat = O in
35+ " >>>>x
36+ let g:idris_indent_let = 4
37+endif
38+
39+if !exists('g:idris_indent_where')
40+ " where f : Nat -> Nat
41+ " >>>>>>f x = x
42+ let g:idris_indent_where = 6
43+endif
44+
45+if !exists('g:idris_indent_do')
46+ " do x <- a
47+ " >>>y <- b
48+ let g:idris_indent_do = 3
31endif
49endif
32
50
33setlocal indentexpr=GetIdrisIndent()
51setlocal indentexpr=GetIdrisIndent()
34setlocal indentkeys=!^F,o,O
52setlocal indentkeys=!^F,o,O
35
53
36function! GetIdrisIndent()
54function! GetIdrisIndent()
37− let line = substitute(getline(getpos('.')[1] - 1), '\t', repeat(' ', &tabstop), 'g')
55+ let prevline = getline(v:lnum - 1)
38
56
39− if line =~ '[!#$%&*+./<=>?@\\^|~-]$\|\<do$'
57+ if prevline =~ '[!#$%&*+./<>?@\\^|~-]\s*$'
40− return match(line, '\s*where \zs\|\S') + &shiftwidth
58+ let s = match(prevline, '[:=]')
59+ if s > 0
60+ return s + 2
61+ else
62+ return match(prevline, '\S')
41 endif
63 endif
64+ endif
42
65
43− if line =~ '{$'
66+ if prevline =~ '[{([]\s*$'
44− return match(line, '\s*where \zs\|\S') + &shiftwidth
67+ return match(prevline, '[{([]')
45− endif
68+ endif
46
69
47− if line =~ '^\s*\(data\|instance\|class\).*\&.*where$'
70+ if prevline =~ 'let\s\+.\+in\s*$'
48− return match(line, '\(data\|instance\|class\)') + &shiftwidth
71+ return match(prevline, 'let') + g:idris_indent_let
49− endif
72+ endif
50
73
51− if line =~ '^\s*using\s*(.\+)$'
74+ if prevline !~ '\<else\>'
52− return match(line, 'using') + &shiftwidth
75+ let s = match(prevline, '\<if\>.*\&.*\zs\<then\>')
76+ if s > 0
77+ return s
53 endif
78 endif
54
79
55− if line =~ '\<with\>'
80+ let s = match(prevline, '\<if\>')
56− return &shiftwidth
81+ if s > 0
82+ return s + g:idris_indent_if
57 endif
83 endif
84+ endif
58
85
59− if line =~ '^\s*data\s\+\S*\s\+=\s\+\S\+$'
86+ if prevline =~ '\(where\|do\|=\)\s*$'
60− return match(line, '=')
87+ return match(prevline, '\S') + &shiftwidth
61− endif
88+ endif
62
89
63− if line =~ '^\s*namespace\s\+\S\+$'
90+ if prevline =~ 'where\s\+\S\+.*$'
64− return match(line, 'namespace') + &shiftwidth
91+ return match(prevline, 'where') + g:idris_indent_where
65− endif
92+ endif
66
93
67− if line =~ ')$'
94+ if prevline =~ 'do\s\+\S\+.*$'
68− let pos = getpos('.')
95+ return match(prevline, 'do') + g:idris_indent_do
69− normal k$
70− let paren_end = getpos('.')
71− normal %
72− let paren_begin = getpos('.')
73− call setpos('.', pos)
74− if paren_begin[1] != paren_end[1]
75− return paren_begin[2] - 1
76− endif
77− endif
96+ endif
78
97
79− if line !~ '\<else\>'
98+ if prevline =~ '^\s*data\s\+[^=]\+\s\+=\s\+\S\+.*$'
80− let s = match(line, '\<if\>.*\&.*\zs\<then\>')
99+ return match(prevline, '=')
81− if s > 0
82− return s
83− endif
100+ endif
84
101
85− let s = match(line, '\<if\>')
102+ if prevline =~ 'with\s\+([^)]*)\s*$'
86− if s > 0
103+ return match(prevline, '\S') + &shiftwidth
87− return s + g:idris_indent_if
88− endif
89− endif
104+ endif
90
105
91− let s = match(line, '\<do\s\+\zs[^{]\|\<where\s\+\zs\w\|\<let\s\+\zs\S\|^\s*\zs|\s')
106+ if prevline =~ 'case\s\+.\+of\s*$'
92− if s > 0
107+ return match(prevline, 'case') + g:idris_indent_case
93− return s
94− endif
108+ endif
95
109
96− let s = match(line, '\<case\>')
110+ if prevline =~ '^\s*\(namespace\|data\)\s\+\S\+\s*$'
97− if s > 0
111+ return match(prevline, '\(namespace\|data\)') + &shiftwidth
98− return s + g:idris_indent_case
112+ endif
113+
114+ if prevline =~ '^\s*using\s\+([^(]*)\s*$'
115+ return match(prevline, 'using') + &shiftwidth
99− endif
116+ endif
100
117
101− return match(line, '\S')
118+ return match(prevline, '\S')
102endfunction
119endfunction
lib/base.ipkg+3−2
@@ -6,10 +6,11 @@ modules = builtins, prelude, io, system,
6 prelude.algebra, prelude.cast, prelude.nat, prelude.fin,
6 prelude.algebra, prelude.cast, prelude.nat, prelude.fin,
7 prelude.list, prelude.maybe, prelude.monad, prelude.applicative,
7 prelude.list, prelude.maybe, prelude.monad, prelude.applicative,
8 prelude.either, prelude.vect, prelude.strings, prelude.char,
8 prelude.either, prelude.vect, prelude.strings, prelude.char,
9− prelude.heap, prelude.complex,
9+ prelude.heap, prelude.complex, prelude.morphisms,
10
10
11 network.cgi,
11 network.cgi,
12
12
13 language.reflection,
13 language.reflection,
14
14
15− control.monad.identity, control.monad.state
15+ control.monad.identity, control.monad.state, control.category,
16+ control.arrow
lib/control/arrow.idrnew file+21
@@ -0,0 +1,21 @@
1+module category.arrow
2+
3+import prelude.morphisms
4+import control.category
5+
6+infixr 3 ***
7+infixr 3 &&&
8+
9+class Category arr => Arrow (arr : Set -> Set -> Set) where
10+ arrow : (a -> b) -> arr a b
11+ first : arr a b -> arr (a, c) (b, c)
12+ second : arr a b -> arr (c, a) (c, b)
13+ (***) : arr a b -> arr a' b' -> arr (a, a') (b, b')
14+ (&&&) : arr a b -> arr a b' -> arr a (b, b')
15+
16+instance Arrow Morphism where
17+ arrow f = Homo f
18+ first (Homo f) = Homo $ \(a, b) => (f a, b)
19+ second (Homo f) = Homo $ \(a, b) => (a, f b)
20+ (Homo f) *** (Homo g) = Homo $ \(a, b) => (f a, g b)
21+ (Homo f) &&& (Homo g) = Homo $ \a => (f a, g a)
lib/control/category.idrnew file+15
@@ -0,0 +1,15 @@
1+module control.category
2+
3+import prelude.morphisms
4+
5+class Category (cat : Set -> Set -> Set) where
6+ id : cat a a
7+ (.) : cat b c -> cat a b -> cat a c
8+
9+instance Category Morphism where
10+ id = Homo builtins.id
11+ (Homo f) . (Homo g) = Homo $ builtins.(.) f g
12+
13+infixr 1 >>>
14+(>>>) : Category cat => cat a b -> cat b c -> cat a c
15+f >>> g = g . f
lib/prelude/morphisms.idrnew file+7
@@ -0,0 +1,7 @@
1+module prelude.morphisms
2+
3+data Morphism : Set -> Set -> Set where
4+ Homo : (a -> b) -> Morphism a b
5+
6+($) : Morphism a b -> a -> b
7+(Homo f) $ a = f a